rapx/
limit.rs

1//! Central home for every numeric limit / bound used across the analysis and
2//! verification pipeline.
3//!
4//! Before this module, each limit lived as a module-local `const`/`static` next
5//! to its consumer, so thresholds were duplicated (the `16`-block inline cap
6//! appeared in both the path graph and the runtime inliner) and hard to audit.
7//! Keeping them all here mirrors [`crate::def_id`]: one flat, well-documented
8//! location where a knob can be found and tuned without grepping the crate.
9//!
10//! Everything is `pub(crate)`; names that would otherwise collide across
11//! modules (the two `VISIT_LIMIT`s, the two `MAX_DEPTH`s) are prefixed with
12//! their owning analysis.
13
14// ─────────────────────────────────────────────────────────────────────────────
15// Path enumeration
16// ─────────────────────────────────────────────────────────────────────────────
17
18use std::sync::atomic::{AtomicUsize, Ordering};
19
20/// Maximum number of paths collected per search — both whole-CFG enumeration
21/// and per-checkpoint prefix collection. Overridable via the `--path-limit`
22/// CLI flag.
23pub(crate) const PATH_LIMIT: usize = 512;
24
25/// Runtime override for [`PATH_LIMIT`], set from `--path-limit`. `0` means
26/// "not overridden" (the default above applies).
27static PATH_LIMIT_OVERRIDE: AtomicUsize = AtomicUsize::new(0);
28
29/// Set the `--path-limit` override; `0` restores [`PATH_LIMIT`].
30pub(crate) fn set_path_limit(n: usize) {
31    PATH_LIMIT_OVERRIDE.store(n, Ordering::Relaxed);
32}
33
34/// The effective path cap (override, or [`PATH_LIMIT`]).
35pub(crate) fn path_limit() -> usize {
36    match PATH_LIMIT_OVERRIDE.load(Ordering::Relaxed) {
37        0 => PATH_LIMIT,
38        n => n,
39    }
40}
41
42/// Maximum DFS depth for whole-CFG path enumeration.
43pub(crate) const WHOLE_CFG_PATH_DEPTH_LIMIT: usize = 256;
44
45/// Bounded cache size for SCC path enumeration.
46pub(crate) const SCC_PATH_CACHE_LIMIT: usize = 2048;
47
48/// Maximum DFS depth for intra-SCC path enumeration.
49pub(crate) const SCC_MAX_DEPTH: usize = 128;
50
51/// Maximum number of distinct paths collected per SCC.
52pub(crate) const SCC_MAX_SEEN_PATHS: usize = 128;
53
54/// Maximum path length within an SCC traversal.
55pub(crate) const SCC_MAX_PATH_LEN: usize = 200;
56
57// ─────────────────────────────────────────────────────────────────────────────
58// Inlining
59// ─────────────────────────────────────────────────────────────────────────────
60
61/// A local callee is inlined into the path CFG only when its MIR is at most
62/// this many basic blocks. This is a *transitive* shape bound: local inlining
63/// recurses into the callee's own calls, so every inlined body multiplies the
64/// path-graph size. Cross-crate callees are exempt — they are inlined a single
65/// level and never recursed into, so their size is not bounded here.
66pub(crate) const LOCAL_INLINE_BLOCK_LIMIT: usize = 32;
67
68/// Recursion depth bound for runtime inlining
69/// ([`crate::verify::vm::call::exec_inline_call`]). Recursive inlining unwinds
70/// through the Rust call stack, so this caps nesting.
71pub(crate) const MAX_INLINE_DEPTH: usize = 5;
72
73// ─────────────────────────────────────────────────────────────────────────────
74// Loop sensitivity / postfix repeat
75// ─────────────────────────────────────────────────────────────────────────────
76
77/// Caps how many times a loop body is unrolled during path enumeration;
78/// loop-heavy functions (e.g. UTF-16 decoders) scale super-linearly with it.
79/// Lower it to speed up verification at the cost of loop sensitivity (bugs that
80/// only manifest after more iterations can be missed).
81pub(crate) const MAX_AUTO_REPEAT: usize = 8;
82
83/// Fallback loop-carried distance used when a sink is loop-sensitive but the
84/// local transfer graph is too imprecise to calculate a better distance.
85///
86/// Three backedges calibrates to `allow_repeat = 2`, which is the first depth
87/// needed by the delayed pointer/state cases in `loop_repeat_threshold`.
88pub(crate) const DEFAULT_LOOP_CARRIED_BACKEDGES: usize = 3;
89
90/// Conservative first numeric witness when an index obligation is known to be
91/// induction-sensitive but the current summary cannot yet recover a concrete
92/// symbolic bound.
93pub(crate) const DEFAULT_NUMERIC_WITNESS_ITERATION: usize = 4;
94
95/// The first repeat depth that reliably exposes the existing delayed
96/// loop-carried pointer/state fixtures.
97pub(crate) const MIN_DATAFLOW_REPEAT: usize = 2;
98
99// ─────────────────────────────────────────────────────────────────────────────
100// Points-to / alias
101// ─────────────────────────────────────────────────────────────────────────────
102
103/// Hard cap on the number of values a single points-to path may materialize.
104pub(crate) const MAX_VALUES_PER_PATH: usize = 1000;
105
106/// Recursion cap on nested field projection while building a points-to graph.
107pub(crate) const MAX_FIELD_DEPTH: usize = 5;
108
109/// Recursion cap on nested dereferences while building a points-to graph.
110pub(crate) const MAX_DEREF_DEPTH: usize = 3;
111
112/// Visit cap for the alias-graph DFS/iteration in the default alias analysis.
113pub(crate) const ALIAS_VISIT_LIMIT: usize = 80;
114
115// ─────────────────────────────────────────────────────────────────────────────
116// SafeDrop
117// ─────────────────────────────────────────────────────────────────────────────
118
119/// Visit cap for the SafeDrop graph DFS.
120pub(crate) const SAFEDROP_VISIT_LIMIT: usize = 1000;
121
122// ─────────────────────────────────────────────────────────────────────────────
123// Call-summary recognition (interprocedural)
124// ─────────────────────────────────────────────────────────────────────────────
125
126/// Max basic-block count for a local callee to be recognized as a
127/// pointer-arithmetic (add/sub) wrapper summary.
128pub(crate) const POINTER_ARITH_WRAPPER_BLOCK_LIMIT: usize = 16;
129
130/// Max basic-block count for a local callee to be recognized as a
131/// `from_raw_parts` wrapper summary.
132pub(crate) const FROM_RAW_PARTS_WRAPPER_BLOCK_LIMIT: usize = 8;
133
134/// Max basic-block count for a local callee to be recognized as a pure
135/// field-load (`_0 = (*_1).field`) summary.
136pub(crate) const FIELD_LOAD_EFFECT_BLOCK_LIMIT: usize = 4;
137
138/// Max basic-block count for a local callee to be recognized as a
139/// slice-bounded return summary.
140pub(crate) const SLICE_BOUNDED_RETURN_BLOCK_LIMIT: usize = 12;
141
142// ─────────────────────────────────────────────────────────────────────────────
143// API dependency
144// ─────────────────────────────────────────────────────────────────────────────
145
146/// Upper bound on type complexity accepted when resolving API-dependency
147/// output types.
148pub(crate) const MAX_TY_COMPLX: usize = 5;
149
150/// Cap on the number of monomorphization steps retained per API-dependency
151/// resolution.
152pub(crate) const MAX_STEP_SET_SIZE: usize = 1000;
153
154/// Recursion depth cap for the fuzzable-type predicate.
155pub(crate) const FUZZABLE_MAX_DEPTH: usize = 64;
rapx/limit.rs

rapx/
limit.rs
