Add property-directed slicing before Boogie generation - #847
Open
shaobo-he wants to merge 11 commits into
Open
Conversation
Adds an optional `-property-slicing` pass that removes program behaviour
which cannot influence the assertion property, run after Devirtualize has
resolved indirect calls and before RewriteBitwiseOps and
SmackModuleGenerator, so nothing removed becomes a Boogie CFG, a memory
operation, or a VC.
The slice is backward from the property root and reuses analyses the
translator already pays for: the sea-DSA-derived Regions partition that
becomes the $M.<k> maps, plus per-function PostDominatorTree and LoopInfo.
It introduces no alias analysis and never assumes two Regions are disjoint
beyond what Regions::idx already guarantees.
Soundness is one-directional -- Errors(original) is a subset of
Errors(sliced) -- so the slice may add executions but never deletes an
error-reaching one. Bypassing a property-irrelevant loop can add the
execution that skips a nontermination, which is the safe direction for
reachability but not for termination; the pass therefore refuses to run
under -memory-safety, -integer-overflow, and -fail-on-loop-exit, whose
roots this relevance relation does not model.
Three properties of the existing region machinery are guarded rather than
assumed. A pointer with no sea-DSA cell receives its own region rather than
aliasing everything, because Region::overlaps only unifies two *complicated*
regions and Node::isIncomplete() is never set; such accesses are forced to a
TOP sentinel. Region::isDisjoint adds offset + length in plain unsigned, so
a UINT_MAX length wraps and reports overlapping intervals disjoint; memory
intrinsics with a non-constant length are likewise forced to TOP. And
Regions::idx mutates and renumbers the partition on every call, so indices
are snapshotted once before any slicing decision and never re-derived.
Flags:
-property-slicing enable (off by default)
-property-slicing-relax-asm adopt SMACK's own Stmt::skip() semantics
for inline asm
-property-slicing-no-loop-bypass drop instructions but keep every loop
-property-slicing-no-regions ignore the region partition (ablation)
-property-slicing-profile FILE machine-readable profile
Adds 28 regression tests covering SSA relevance, region relevance through
loads and stores, call and effect rules, and loop bypass, 19 of which must
still report an error.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The pass requires Regions and DSAWrapper. Adding it to the pipeline transfers last-usership of DSAWrapper, seadsa::DsaAnalysis and CallGraph away from the passes that follow, and scheduling it alongside MemorySafetyChecker crashed the legacy pass manager in PMTopLevelManager::setLastUser before any pass ran: every --check=memory-safety, valid-deref and valid-free translation segfaulted, with or without -property-slicing, on all 31 memory-safety regression tests that translate fine on develop. llvm2bpl now consults propertySlicingWillRun() and adds the pass only when the flag is on and the property is one the relevance relation models. That also makes the refusals effective: they previously lived in runOnModule, which the crash meant was never reached. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
UndefValue::get(T) is uniqued per type and Naming::get caches by Value *, so SmackRep emits every undef of a type as one module-global Boogie const. A Boogie constant is a single unconstrained but fixed value, so every site sharing it is forced to agree: on kbfiltr_false a single 'const $u0: i1' was the condition of 363 branches. That removes execution combinations -- the opposite of the over-approximation the branch nondeterminization and loop bypass rely on -- and is unsound wherever the relevance relation is imprecise. Each site now calls a body-less declaration, which Boogie havocs per call: 329 distinct branch conditions on the same driver. Pointer results keep undef, since an external call returning a pointer also gets an assume $isExternal(p) that would constrain the value, and a pointer is never a branch condition. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The two irrelevant loops need opposite truth values at their header branches; with a shared replacement value the assertion is unreachable and the error is missed. Fails (verified) on the pre-fix pass, errors after. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The relevance relation this pass computes is a *sequential* dependence: an
instruction is kept when the property's value depends on it along the
thread's own control flow. Under an interleaved semantics that relation is
wrong in both directions.
- A store that no later instruction of this thread reads is still read by
another thread. The slicer drops it, and the protocol it implemented is
gone with it.
- A busy-wait loop carries no intra-thread control dependence: its body is
empty and its exit block post-dominates the header, so nothing after the
loop is control-dependent on the exit test. bypassIrrelevantLoops
therefore deletes the spin outright.
Measured on test/c/pthread_extras with --pthread --context-bound=2 (Corral
1.1.8, unroll 4): peterson, dekker and szymanski all go from verified to a
spurious error. In peterson's thr1 three of the four stores -- flag1 = 1,
turn = 1 and flag1 = 0 -- and the whole `while (flag2 == 1 && turn == 1)`
loop are gone, leaving the thread walking straight into its critical
section.
-property-slicing-no-loop-bypass is not a remedy, which is why this is a
refusal rather than a narrower loop rule: with loop bypass off all three
still report a spurious error, because the exit condition is nondeterminized
instead (the spin may leave at any moment) and the protocol stores are
dropped by removeIrrelevantInstructions regardless. Keeping "every loop
whose exit test reads a location another thread may write" would therefore
also have to keep every store to such a location and every load feeding such
a test -- on these programs, everything -- and SMACK's thread edges live
inside `__SMACK_code("async call ...")` string literals in
share/smack/lib/pthread.c, which this pass cannot read.
llvm2bpl has no notion of --pthread, so top.py passes the new
-property-slicing-pthread alongside -property-slicing. The option is
declared in PropertySlicing.cpp only because the slicer is its single
consumer; it describes the program, and belongs in SmackOptions next to
-memory-safety once this pass lands.
With the refusal, --pthread --property-slicing emits a Boogie file
byte-identical to --pthread alone (modulo the "// via <argv>" header), and
the three tests verify again with the same procedure-inlining counts as the
unsliced baseline (55/62/59).
The new tests are a spin-wait handshake and its failing twin: with the
refusal both pass; with the PR as it stood, pthread_spin_wait.c reports a
spurious error. The folder's memory model is pinned because Corral rejects
the prelude the other two emit for a concurrent program ("Ensures has a
shared global") -- test/c/pthread pins it for the same reason.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The refusal list is only useful if a reader can tell what is missing from it on purpose. Every other mode SMACK's front end offers -- the remaining --check properties, and the translate-group flags --modular, --rust-panics, --float, --llvm-assumes and --bit-precise -- was checked against the relevance relation and measured; none needs a refusal, so the reasoning goes in a comment rather than in code. The one that came closest is -llvm-assumes=check, where SmackInstGenerator.cpp:930 turns llvm.assume into an *assert* -- a property root isPropertyRoot() does not name. It survives anyway, and not by accident: llvm.assume is inaccessiblememonly, so computeEffects() puts it in unsafeToDrop and propagate() keeps the call along with the condition it names. Measured with a probe whose assumed value is irrelevant to the assertion (`int x = nondet(); __builtin_assume(x > 0); assert(watched == 1);`): the violation is reported with slicing on and off alike. Also measured: test/c/contracts under --modular (9/9), test/rust/panic under --check=rust-panics (5/5, four of them error tests), and the 28 tests of test/c/property-slicing re-run under -bit-precise, -float and -llvm-assumes=check (28/28 in each). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Every rule in the property slicer that reasoned about a call was written over CallInst, which is not the class of "a call" in LLVM -- CallBase is. An `invoke` is a call that happens to also be a terminator, and SMACK translates it through the very same SmackRep::call a CallInst goes through (SmackInstGenerator::visitInvokeInst, SmackRep.cpp:1105-1128, which tells the two apart only to count operands, then adds a goto on $exn). So the slicer saw, at an invoke: no callee, no call-graph edge, no written-region summary, no argument binding and no returned value. The pass was not visibly unsound today only because hasUnmodelledEffect listed InvokeInst outright, which made every function containing one un-droppable and, through the callee rule of computeEffects, every caller of it too. That is an accident, and it is not even the accident it looks like: an invoke's unwind destination must begin with an EH pad in the same function (LangRef), and the EH pad is unmodelled as well, so removing InvokeInst from that predicate costs nothing in unsafeToDrop while letting every rule below finally see the call. What was actually broken is the rule "a relevant call result makes the callee's returned values relevant". Written over CallInst it does not fire at an invoke, so nothing marks the callee's returned load relevant, the region behind it never becomes relevant, and the store that feeds it -- along with the call that performs the store and the global's static initialiser -- is sliced away. test/c/property-slicing/invoke_call_result.ll is that program: verified with the flag off, and reported as an error by the slicer before this commit because $M.0 was left unconstrained. Converted to CallBase: calleeOf, isPropertyRoot, hasVerificationEffect, the hasUnmodelledEffect inline-asm/unresolved-callee test, computeMayReachError's root and edge detection, computeEffects' unsafe classification and callee edges, explainRelevance, seedRoots, the propagate keep rule, the per-argument rule, the callee-return rule and the loop-blocker classification. Deliberately left as CallInst, each with a comment saying why: the callsRemoved/callsRetained statistics (an invoke is a terminator and is never a removal candidate, so counting it in one and not the other would make the two disagree), and the switch-condition guard in removeIrrelevantInstructions (it recognises the nondet call freshNondet itself emits, which is always a CallInst). Two further adjustments the conversion requires: - An invoke can never be *dropped* the way a call can. Deleting one would mean rewriting it into a br to the normal destination and repairing the unwind destination's PHIs, inside a rewriter that otherwise only erases instructions; and it buys nothing, because removeIrrelevantInstructions already skips every terminator, so no invoke was ever being deleted. isTerminatorCall makes that explicit and seedRoots retains such call sites unconditionally. Only their effects take part in the analysis. - hasUnmodelledEffect now tests I.isEHPad() rather than isa<LandingPadInst>, and adds catchret/cleanupret. The Windows funclet pads used to be caught only via the blanket InvokeInst case that this commit removes; naming them directly keeps that coverage instead of inheriting it by accident. MEASURED, install-b4 vs a build of the parent commit: the C corpus never produces an invoke at all (share/smack/frontend.py:88-121 passes no -fexceptions, so clang marks every C function nounwind), hence the four hand-written .ll tests; test/c/basic and test/c/property-slicing translate byte-identically with the flag on and off. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The loop-droppability scan in bypassIrrelevantLoops skips every terminator inside the loop and instead checks the block's terminator afterwards -- but that later check exempts the latch, because the latch's back-edge branch is exactly what a bypass is entitled to delete. For an ordinary loop that is right. It stops being right once a terminator can also be a call: an invoke may terminate the latch, and then neither test looks at it, the loop is declared droppable, and EliminateUnreachableBlocks takes the call site away with the rest of the body. Nothing else in the rewriter can delete an invoke, so this was the one path that could. The scan now examines a terminator that is also a call as if it were an ordinary instruction, which puts it back under both the hasUnmodelledEffect test and the keep test -- and seedRoots always keeps such a call, so any loop containing one is retained. HYPOTHESIS, not measured: I could not build a program that actually reaches this. An invoke whose unwind destination lies outside the loop gives the loop a second exit block, so getExitBlock() returns null and the bypass is refused as MULTIPLE_EXITS; one whose unwind destination lies inside the loop brings an EH pad in with it, which the scan does see and which hasUnmodelledEffect retains. The guard is therefore cheap insurance against those two accidents ever being weakened, not a fix for an observed failure -- but it costs one predicate call per instruction and the alternative is a silently deleted call site. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Control dependence here came from LLVM's PostDominatorTree, which treats
every loop as if it always terminated. For
while (1) { if (bad) { __VERIFIER_assert(0); return; } step(); }
the error block is the function's only exit, so it post-dominates the
branch that decides to enter it and comes out control-dependent on
nothing: `bad` is irrelevant, the branch is replaced by a nondeterministic
one, the loop body then holds no kept instruction, and bypassIrrelevantLoops
redirects the preheader onto the loop's unique exit block -- which is the
error block. A program that never reaches the assertion reports a bug.
Both halves of that are the same missing fact: everything after a loop
the program may never leave happens only because the loop was left.
- mustTerminate(): ScalarEvolution bounds the backedge count. Nothing
else in the pass can distinguish `for (i = 0; i < 1000; i++)` from
`while (1)`, and the difference is exactly what decides whether
skipping the loop adds an execution the original does not have.
- addLoopExitDependence(): for a loop that is not known to terminate,
every block its exit can reach is control-dependent on the loop's
exiting branches. The guard survives; so does the loop that computes
it.
- bypassIrrelevantLoops(): only a loop with a bounded backedge count is
bypassed. This is stronger than refusing loops from which the property
root is reachable, and simpler: it also covers the interprocedural
case, where the loop's own function contains no root but returns into
a caller that reaches one. The comment claiming the bypass "can add
the execution that skips a nonterminating loop -- sound for
reachability" was the false premise; an added execution cannot hide a
bug but can report one that is not there.
Measured on test/c/property-slicing with -property-slicing-profile: the
28 pre-existing tests keep byte-identical instruction counts, and both
irrelevant_loop.c (constant trip count) and irrelevant_unknown_bound_loop.c
(`i < n`) are still BYPASSED -- ScalarEvolution bounds both. The new
ps_nonterm_error_loop.c goes from BYPASSED (verdict: error) to kept
(verdict: verified); its _fail twin still finds the real error.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A call was kept only when the callee may reach the error, is unsafe to
drop, or writes a relevant region. The LDV drivers' stop idiom --
void ldv_stop(void) { L: goto L; }
-- satisfies none of the three: it reaches no property root, has no
unmodelled effect, and writes nothing. So `if (c) ldv_stop();` lost its
call and the slice carried on past a point the original execution never
leaves, making everything after it -- assertions included -- reachable
that was not. That is a false alarm on precisely the driver family this
pass was written for.
The attribute is not the test: ldv_stop is an ordinary function that
clang marks with nothing at all, and only its shape says it never gives
control back. neverReturns() asks whether any `ret` is reachable from the
entry block, and honours `noreturn` as well for the body-less
declarations (exit, abort) where shape says nothing.
The result feeds unsafeToDrop, which is what "the body may not be elided
at a call site" already means and which the existing greatest-fixpoint
already propagates along call edges -- so a function that calls a
function that may not return inherits the property, as it should.
The companion to this is the non-termination rule in the previous commit:
keeping the call would buy nothing if the callee's own infinite loop were
then bypassed and made to fall through.
Measured: ps_noreturn_call.c reports `error` with -property-slicing on
the prior build and `verified` with this one, matching the flag-off
verdict; its _fail twin reports the real error in both.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The folder was added with the pass but never entered the matrix, so none of its tests -- including the four that discriminate the fixes for the non-termination, noreturn, pthread and invoke defects -- ran on a pull request. The .ll tests need their own entry because --languages rejects a comma-separated list despite its help text. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds an optional
-property-slicingpass that removes program behaviour which cannot influence the assertion property, run after Devirtualize has resolved indirect calls and before RewriteBitwiseOps and SmackModuleGenerator, so nothing removed becomes a Boogie CFG, a memory operation, or a VC.The slice is backward from the property root and reuses analyses the translator already pays for: the sea-DSA-derived Regions partition that becomes the $M. maps, plus per-function PostDominatorTree and LoopInfo. It introduces no alias analysis and never assumes two Regions are disjoint beyond what Regions::idx already guarantees.
Soundness is one-directional -- Errors(original) is a subset of Errors(sliced) -- so the slice may add executions but never deletes an error-reaching one. Bypassing a property-irrelevant loop can add the execution that skips a nontermination, which is the safe direction for reachability but not for termination; the pass therefore refuses to run under -memory-safety, -integer-overflow, and -fail-on-loop-exit, whose roots this relevance relation does not model.
Three properties of the existing region machinery are guarded rather than assumed. A pointer with no sea-DSA cell receives its own region rather than aliasing everything, because Region::overlaps only unifies two complicated regions and Node::isIncomplete() is never set; such accesses are forced to a TOP sentinel. Region::isDisjoint adds offset + length in plain unsigned, so a UINT_MAX length wraps and reports overlapping intervals disjoint; memory intrinsics with a non-constant length are likewise forced to TOP. And Regions::idx mutates and renumbers the partition on every call, so indices are snapshotted once before any slicing decision and never re-derived.
Flags:
-property-slicing enable (off by default)
-property-slicing-relax-asm adopt SMACK's own Stmt::skip() semantics
for inline asm
-property-slicing-no-loop-bypass drop instructions but keep every loop
-property-slicing-no-regions ignore the region partition (ablation)
-property-slicing-profile FILE machine-readable profile
Adds 28 regression tests covering SSA relevance, region relevance through loads and stores, call and effect rules, and loop bypass, 19 of which must still report an error.