depth/
depth.rs

1//! Where the parser's nesting limit comes from.
2//!
3//! Two numbers decide it: how deeply real specifications nest, and how much
4//! stack one level costs. Both are measured here rather than guessed.
5//!
6//! ```text
7//! cargo run --example depth -p tla-syntax -- $(find CORPUS -name '*.tla')
8//! ```
9//!
10//! Stack exhaustion aborts the process rather than unwinding, so it cannot be
11//! caught in-process. Each stack size is therefore tried in a child, and the
12//! parent reads the exit status.
13
14use std::process::Command;
15
16use tla_syntax::{Expr, Unit, parse_module};
17
18/// Set in the child to say how much stack to give the probing thread.
19const PROBE: &str = "TLA_DEPTH_PROBE_KIB";
20
21fn main() {
22    if let Ok(kib) = std::env::var(PROBE) {
23        let kib: usize = kib.parse().expect("a number of KiB");
24        let survived = std::thread::Builder::new()
25            .stack_size(kib * 1024)
26            .spawn(probe)
27            .expect("thread")
28            .join()
29            .unwrap_or(false);
30        std::process::exit(i32::from(!survived));
31    }
32
33    report_corpus_depth();
34    report_stack_need();
35}
36
37/// Parse an expression nested one past the parser's own limit, so the limit is
38/// what stops it rather than the input running out.
39fn probe() -> bool {
40    let depth = tla_syntax::DEFAULT_NESTING_LIMIT + 44;
41    let src = format!(
42        "---- MODULE M ----\nX == {}1{}\n====",
43        "(".repeat(depth),
44        ")".repeat(depth)
45    );
46    parse_module(&src).is_err()
47}
48
49fn report_corpus_depth() {
50    let mut deepest = (0usize, String::new());
51    let mut files = 0usize;
52    for path in std::env::args().skip(1) {
53        let Ok(src) = std::fs::read_to_string(&path) else {
54            continue;
55        };
56        let Ok(module) = parse_module(&src) else {
57            continue;
58        };
59        files += 1;
60        for unit in &module.units {
61            if let Unit::Def(def) = unit {
62                let d = depth(&def.body);
63                if d > deepest.0 {
64                    deepest = (d, format!("{}: {}", module.name, def.name));
65                }
66            }
67        }
68    }
69    println!(
70        "{files} modules; deepest expression nests {} ({})",
71        deepest.0, deepest.1
72    );
73}
74
75fn report_stack_need() {
76    let profile = if cfg!(debug_assertions) {
77        "unoptimised"
78    } else {
79        "optimised"
80    };
81    let me = std::env::current_exe().expect("own path");
82    for kib in [
83        128usize, 192, 256, 384, 512, 768, 1024, 1536, 2048, 3072, 4096, 5120, 6144, 7168, 8192,
84        12288, 16384,
85    ] {
86        let status = Command::new(&me)
87            .env(PROBE, kib.to_string())
88            .status()
89            .expect("the child runs");
90        if status.success() {
91            println!("{profile}: reaching the nesting limit needs {kib} KiB of stack");
92            return;
93        }
94    }
95    println!("{profile}: reaching the nesting limit needs more than 32 MiB of stack");
96}
97
98fn depth(e: &Expr) -> usize {
99    1 + children(e).iter().map(|c| depth(c)).max().unwrap_or(0)
100}
101
102fn children(e: &Expr) -> Vec<&Expr> {
103    match e {
104        Expr::Prime(x) | Expr::Field(x, _) | Expr::Unary(_, x) => vec![x],
105        Expr::Binary(_, a, b)
106        | Expr::FnSet {
107            domain: a,
108            range: b,
109        } => vec![a, b],
110        Expr::Apply(h, args) | Expr::FnApply(h, args) => {
111            let mut v = vec![&**h];
112            v.extend(args);
113            v
114        }
115        Expr::Tuple(xs) | Expr::SetEnum(xs) => xs.iter().collect(),
116        Expr::Record(fs) | Expr::RecordSet(fs) => fs.iter().map(|(_, v)| v).collect(),
117        Expr::SetFilter { pred, .. } => vec![pred],
118        Expr::SetMap { expr, .. } => vec![expr],
119        Expr::FnDef { body, .. }
120        | Expr::Quant { body, .. }
121        | Expr::Choose { body, .. }
122        | Expr::Lambda { body, .. }
123        | Expr::Let { body, .. } => vec![body],
124        Expr::Except { base, updates } => {
125            let mut v = vec![&**base];
126            v.extend(updates.iter().map(|(_, e)| e));
127            v
128        }
129        Expr::If {
130            cond,
131            then,
132            otherwise,
133        } => vec![cond, then, otherwise],
134        Expr::Case { arms, .. } => arms.iter().flat_map(|(g, r)| [g, r]).collect(),
135        Expr::ActionBox { action, .. }
136        | Expr::ActionAngle { action, .. }
137        | Expr::Fairness { action, .. } => vec![action],
138        Expr::Qualified { args, .. } => args.iter().collect(),
139        _ => Vec::new(),
140    }
141}
depth/depth.rs

depth/
depth.rs
