[SwayamInSync]

#64 made the goals of a module share the terms of their assumptions, but the traversals that check a module still walked every goal as a tree. Each obligation's goal states every assumption before it, so a function's checks revisited its first assumptions once per later check, quadratic in its length.

validateObligationModule runs on every module that is built, simplified, or replayed, and it was 80% of lowering. callgrind on --lower-only --jobs=1 suite/safe_fib.cpp counts 20.4 of 25.1 billion instructions under it, mostly in:

Function	Share of the run (self)
validateLogicExpr	21.8%
validateVariableScopes, which also copies its set of bound names at every node	10.3%
string_view::find, its embedded-NUL checks	9.8%
collectRequiredFeatures	6.2%
validateLogicCalls	6.0%
collectQuantifierBinders	2.6%

This is step 2 of plan item C3 (gap G4): memoized traversals. Step 1 was #64.

Results

--lower-only --jobs=1, release build, wall-clock time and peak RSS, main (0290cc7) against this branch:

Input	main	This PR
suite/safe_fib.cpp	10.4 s, 0.51 GB	1.9 s, 0.51 GB
suite/llvm_uleb128.cpp	10.3 s, 0.35 GB	2.5 s, 0.35 GB
R24's sum of 250 int terms (gen_deep.py 250)	3.5 s, 0.51 GB	2.9 s, 0.51 GB

This meets the plan's targets for safe_fib.cpp (under 3 s) and the ULEB128 case study (under 6 s). After this PR, the run takes 6.2 billion instructions in all, of which validation is 1.8 billion (29%). The rest is mostly Z3 lowering of every query under --lower-only (34%) and passivization (14%).

Long sums (F27) barely change: their cost is the VCR copies of each overflow check's operands, not Layer 3. They are left to the later steps of C3.

With --jobs=8, --lower-only on suite/llvm_uleb128_decoder_exhaustive.cpp (UNSUPPORTED in lit) takes 23 s within 7.8 GB, against 319 s within 7.7 GB on main; the sets of checked terms take the 0.1 GB more.

Design

Checks that depend on the term alone visit each term once per module. These are the form of each node, that every application has a declaration with its signature, and the logic features the module needs. validateLogicExpr and validateLogicCalls keep the terms that passed in a set, and collectRequiredFeatures the terms whose features it has already collected. A term in the set is not checked again, whichever root reaches it.

Scope depends on where a term is, so ScopeValidator checks it in two parts:

• Binders above a term. A variable is bound or free according to the quantifiers above it.
  • A term is visited once for each set of binder names in scope at it. The sets are interned, so the key is the term and a number. Before, every node copied a std::set<std::string>.
  • A visit checks that a bound occurrence is a mathematical integer, and registers a free one in the map of free variables, whose sort must agree with every other occurrence.
  • The module's roots share one map. Each definition gets its own map, since its variables are its parameters.
• Binders elsewhere in the root. A free variable must not have the name of a binder anywhere in its root.
  • BinderSummaries computes two interned sets once for each term: the binder names it contains, and the binder names free in it. Free names are computed only after every binder name of the module is registered.
  • A root fails where its two sets meet.
  • This is how Frama-C's Qed caches each term's bound and free variables (bind and vars in src/lib/qed/term.ml), and how Lean caches each Expr's loose bound-variable range.

The reference check decides every failure. A root that fails either part is checked again by the tree walk that was the whole check before. So every error message, and which error comes first, is what it was. An assertion checks that this walk fails too: the summaries never reject what the walk accepts.

Node counts. countModuleNodes, the simplifier's statistics, counts a module's nodes as trees, as before. It now computes each shared term's count once, so the numbers are the same in linear time.

Hashing and serialization still walk trees. They run with --obligation-out, the proof cache, and Layer 3 dumps.

Tests

unittests/Verify/ObligationValidationTest.cpp (new) builds modules whose roots share terms, which archive replay cannot do, since a record does not share nodes. It covers:

• SharedTermsKeepEveryFeature: the features of shared terms.
• SharedTermsAreCheckedOnce: a goal whose terms double over 26 levels, validated within 5 s. Each term is checked once, so it takes 0 ms. main's validator walks 2^26 paths and did not finish this test with 28 levels in 600 s.
• BinderOfALaterRootCollidesWithASharedFreeVariable: a term checked first in a root without binders, then free in a root that binds its name elsewhere.
• SharedTermBoundThenFree and SharedTermFreeThenBound: one term bound in one root and free in another, in both orders.
• SharedApplicationOfNoDeclaration: an application shared by two goals that has no declaration.
• DefinitionsHaveTheirOwnVariables: a definition's parameter with a module variable's name and another sort.

Every test but SharedTermsAreCheckedOnce passes against main's validator too, with the same messages.

Each mutant below, applied alone, fails a test:

Mutant	Change	Fails
V1	a shared term is visited once whatever the binders around it	SharedTermFreeThenBound
V2	no root is checked for a free variable named as one of its binders	BinderOfALaterRoot...
V3	a quantifier's binder is left out of its term's binders	BinderOfALaterRoot...
V4	a quantifier's binder is not removed from its term's free names	SharedTermsAreCheckedOnce (82 s); the assertion with assertions on
V5	a union of name sets keeps only its left operand	BinderOfALaterRoot...
V6	definitions are checked against the module's variables	DefinitionsHaveTheirOwnVariables
V7	every occurrence counts as free	SharedTermFreeThenBound, obligation_archive.test
V8	a free occurrence is not compared with the variable's sort	SharedTermBoundThenFree, obligation_archive.test
W1	a term counts as well formed once a set is given	obligation_archive.test
W2	applications count as checked once a set is given	SharedApplicationOfNoDeclaration
W3	features count as collected once a set is given	SharedTermsKeepEveryFeature, obligation_archive.test, obligation_ir.cpp
W4	a term that passes does not join the set	SharedTermsAreCheckedOnce (102 s)

V4 and W4 survived the first sweep. They only make validation slower, since the reference walk then decides. The sharing test and the assertion were added for them.

Docs

• ARCHITECTURE.md: a section on how validation visits a shared term once, and the node count.
• Release notes: the new lowering times, in the entry on shared terms.

Checked

• Layer 3 dumps (--lower-only --jobs=1 --dump-ir=3, semantic hashes included) of all 431 .cpp sources under clang/test/Verify, main against this branch, are byte-identical, except for:
  • crash_report_url.cpp, which crashes on purpose: only the binary's name and addresses in the stack trace differ;
  • suite/llvm_uleb128_decoder_exhaustive.cpp, whose dumps are too large to compare. Its archives (--obligation-out, 238 MB) are byte-identical instead, with the same records refused for the archive's expression limit on both.
• lit of clang/test/Verify on this branch: 473 passed, 1 unsupported (darwin only), no failure.
• VerifyTests on this branch: 69 passed, and the opt-in corpus parity check skipped (it needs CPPVERIFY_PARITY_ARCHIVES).