From bab52da37f1db6abe468c2494261f8638f47cb4e Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Sat, 22 Aug 2026 13:04:23 -0700 Subject: [PATCH 01/11] Add property-directed slicing before Boogie generation 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. 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) --- CMakeLists.txt | 2 + include/smack/PropertySlicing.h | 180 +++ lib/smack/PropertySlicing.cpp | 1276 +++++++++++++++++ share/smack/top.py | 45 + test/c/property-slicing/array_fail.c | 12 + test/c/property-slicing/call_modifies_other.c | 15 + .../call_modifies_region_fail.c | 15 + test/c/property-slicing/call_result_fail.c | 13 + test/c/property-slicing/callee_error_fail.c | 18 + test/c/property-slicing/cast_alias_fail.c | 14 + test/c/property-slicing/config.yml | 3 + test/c/property-slicing/dead_pure_call.c | 15 + test/c/property-slicing/dead_scalar.c | 15 + test/c/property-slicing/distinct_objects.c | 17 + test/c/property-slicing/external_call_kept.c | 15 + test/c/property-slicing/global_fail.c | 14 + test/c/property-slicing/heap_fail.c | 14 + .../irrelevant_infinite_loop.c | 19 + test/c/property-slicing/irrelevant_loop.c | 19 + .../irrelevant_unknown_bound_loop.c | 17 + .../property-slicing/loop_calls_error_fail.c | 18 + .../loop_contains_error_fail.c | 14 + .../loop_with_volatile_kept.c | 17 + .../loop_writes_relevant_fail.c | 14 + test/c/property-slicing/nested_cond_fail.c | 17 + test/c/property-slicing/nested_loops_fail.c | 16 + test/c/property-slicing/phi_fail.c | 16 + test/c/property-slicing/recursive_fail.c | 16 + test/c/property-slicing/same_object_fail.c | 15 + test/c/property-slicing/select_fail.c | 11 + test/c/property-slicing/struct_field_fail.c | 18 + test/c/property-slicing/switch_fail.c | 18 + test/c/property-slicing/transitive_ssa_fail.c | 15 + tools/llvm2bpl/llvm2bpl.cpp | 9 + 34 files changed, 1952 insertions(+) create mode 100644 include/smack/PropertySlicing.h create mode 100644 lib/smack/PropertySlicing.cpp create mode 100644 test/c/property-slicing/array_fail.c create mode 100644 test/c/property-slicing/call_modifies_other.c create mode 100644 test/c/property-slicing/call_modifies_region_fail.c create mode 100644 test/c/property-slicing/call_result_fail.c create mode 100644 test/c/property-slicing/callee_error_fail.c create mode 100644 test/c/property-slicing/cast_alias_fail.c create mode 100644 test/c/property-slicing/config.yml create mode 100644 test/c/property-slicing/dead_pure_call.c create mode 100644 test/c/property-slicing/dead_scalar.c create mode 100644 test/c/property-slicing/distinct_objects.c create mode 100644 test/c/property-slicing/external_call_kept.c create mode 100644 test/c/property-slicing/global_fail.c create mode 100644 test/c/property-slicing/heap_fail.c create mode 100644 test/c/property-slicing/irrelevant_infinite_loop.c create mode 100644 test/c/property-slicing/irrelevant_loop.c create mode 100644 test/c/property-slicing/irrelevant_unknown_bound_loop.c create mode 100644 test/c/property-slicing/loop_calls_error_fail.c create mode 100644 test/c/property-slicing/loop_contains_error_fail.c create mode 100644 test/c/property-slicing/loop_with_volatile_kept.c create mode 100644 test/c/property-slicing/loop_writes_relevant_fail.c create mode 100644 test/c/property-slicing/nested_cond_fail.c create mode 100644 test/c/property-slicing/nested_loops_fail.c create mode 100644 test/c/property-slicing/phi_fail.c create mode 100644 test/c/property-slicing/recursive_fail.c create mode 100644 test/c/property-slicing/same_object_fail.c create mode 100644 test/c/property-slicing/select_fail.c create mode 100644 test/c/property-slicing/struct_field_fail.c create mode 100644 test/c/property-slicing/switch_fail.c create mode 100644 test/c/property-slicing/transitive_ssa_fail.c diff --git a/CMakeLists.txt b/CMakeLists.txt index 05221ad46..470cea2cb 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -119,6 +119,7 @@ add_library(smackTranslator STATIC include/smack/IntegerOverflowChecker.h include/smack/RewriteBitwiseOps.h include/smack/NormalizeLoops.h + include/smack/PropertySlicing.h include/smack/RustFixes.h include/smack/AnnotateLoopExits.h include/smack/SplitAggregateValue.h @@ -147,6 +148,7 @@ add_library(smackTranslator STATIC lib/smack/IntegerOverflowChecker.cpp lib/smack/RewriteBitwiseOps.cpp lib/smack/NormalizeLoops.cpp + lib/smack/PropertySlicing.cpp lib/smack/RustFixes.cpp lib/smack/AnnotateLoopExits.cpp lib/smack/SplitAggregateValue.cpp diff --git a/include/smack/PropertySlicing.h b/include/smack/PropertySlicing.h new file mode 100644 index 000000000..3cdb8499a --- /dev/null +++ b/include/smack/PropertySlicing.h @@ -0,0 +1,180 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// +#ifndef PROPERTYSLICING_H +#define PROPERTYSLICING_H + +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/IR/Module.h" +#include "llvm/Pass.h" + +#include +#include +#include +#include +#include + +namespace smack { + +class Regions; +class DSAWrapper; + +/// A cheap, sound, property-directed slice run just before Boogie generation. +/// +/// The slice is *backward* from the property root and is deliberately built on +/// analyses SMACK has already paid for: the sea-DSA-derived `Regions` +/// partition that becomes the `$M.` Boogie maps, plus per-function +/// PostDominatorTree/LoopInfo. It never introduces an alias analysis of its +/// own and never assumes two Regions are disjoint beyond what `Regions::idx` +/// already guarantees. +/// +/// SOUNDNESS DIRECTION. The target is reachability (SV-COMP `unreach-call`), +/// so the obligation is +/// +/// Errors(original) is a subset of Errors(sliced) +/// +/// i.e. the slice may add executions but must never delete a concrete +/// error-reaching one. Bypassing a property-irrelevant loop can add the +/// execution that skips a nontermination; for reachability that is the safe +/// direction. It would NOT be safe for termination, and it is not sound for +/// memory-safety or overflow properties, whose roots this pass does not model +/// -- the pass therefore refuses to run for anything but assertion checking. +class PropertySlicing : public llvm::ModulePass { +public: + /// Why a loop was retained; reported by the profile. + enum class LoopReason { + ERROR_REACHABLE, + RELEVANT_SCALAR, + RELEVANT_REGION, + CONTROL, + UNKNOWN_CALL, + VOLATILE_ATOMIC, + DSA_COLLAPSED_REGION, + ESCAPING_VALUE, + NO_PREHEADER, + MULTIPLE_EXITS, + NO_EXIT, + OTHER_CONSERVATIVE, + BYPASSED, + }; + + static const char *reasonName(LoopReason R); + + struct FunctionStats { + unsigned instructionsBefore = 0, instructionsAfter = 0; + unsigned blocksBefore = 0, blocksAfter = 0; + unsigned loopsBefore = 0, loopsAfter = 0; + unsigned relevantValues = 0; + unsigned loadsRemoved = 0, loadsRetained = 0; + unsigned storesRemoved = 0, storesRetained = 0; + unsigned callsRemoved = 0, callsRetained = 0; + unsigned loopsBypassed = 0, loopsKept = 0; + std::vector> loopReasons; + /// For each retained loop, the instruction that blocks it and the chain + /// back to whatever made that instruction relevant. + std::vector loopBlockers; + }; + + static char ID; + PropertySlicing() : llvm::ModulePass(ID) {} + + virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const override; + virtual bool runOnModule(llvm::Module &M) override; + +private: + Regions *regions = nullptr; + DSAWrapper *DSA = nullptr; + const llvm::DataLayout *DL = nullptr; + + /// Functions from which the property root is reachable in the call graph. + std::unordered_set mayReachError; + /// Functions whose body may not be elided at a call site (unknown effects, + /// verifier semantics, volatile/atomic, or a transitively unsafe callee). + std::unordered_set unsafeToDrop; + /// Region indices that can influence the property. + std::unordered_set relevantRegions; + /// Set once a read of an un-pinned-down pointer is retained: every region + /// then has to be treated as relevant. + bool topRelevant = false; + /// Region indices written by each function, transitively. + std::unordered_map> + writtenRegions; + + /// Diagnostics: why a function is un-droppable, and which function first + /// made a region relevant. + std::unordered_map unsafeWhy; + std::map regionWhy; + + std::unordered_set relevant; + std::unordered_set keep; + + std::unordered_map stats; + double analysisSeconds = 0.0, rewriteSeconds = 0.0; + unsigned cdEdges = 0, pdtHoles = 0; + + /// Provenance: the instruction whose operand list first made a value + /// relevant. Walking this backwards from a loop's blocking instruction says + /// *why* that loop survives, which the coarse LoopReason cannot. + std::unordered_map + relevantVia; + const llvm::Instruction *markSource = nullptr; + std::string explainRelevance(const llvm::Instruction *I) const; + /// The far end of an instruction's relevance chain -- what it is ultimately + /// needed *for*. Classifying a loop by the head of the chain reports the + /// induction PHI; classifying it by the terminus reports the store. + const llvm::Instruction *relevanceTerminus(const llvm::Instruction *I) const; + + /// Per-function control dependence: block -> blocks whose branch decides + /// whether it executes. + std::unordered_map>> + CD; + + /// Per-function set of blocks from which a function exit is reachable. + std::unordered_map> + exitReaching; + + bool isPropertyRoot(const llvm::CallInst &CI) const; + bool hasVerificationEffect(const llvm::CallInst &CI) const; + bool hasUnmodelledEffect(const llvm::Instruction &I) const; + + void computeMayReachError(llvm::Module &M); + void computeEffects(llvm::Module &M); + void seedRoots(llvm::Module &M); + void propagate(llvm::Module &M); + + void markValue(const llvm::Value *V, bool &changed); + void markRegionIdx(unsigned r, const llvm::Instruction &I, bool &changed); + bool regionIsRelevant(unsigned r) const; + /// Sentinel for "this access may touch any object". Regions does NOT give + /// this to a pointer with no sea-DSA cell -- see snapshotRegions. + static const unsigned TOP_REGION = ~0u; + + /// Region index per memory operation, frozen before any slicing decision is + /// made. Regions::idx mutates and renumbers the partition on every call, so + /// indices must be collected once and never re-derived. + std::unordered_map memRegion; + std::unordered_map memRegionSrc; + /// Functions that write through a pointer whose region could not be pinned + /// down; a call to one may write any relevant region. + std::unordered_set writesTop; + + void snapshotRegions(llvm::Module &M); + bool isOpaquePointer(const llvm::Value *Ptr) const; + unsigned destRegion(const llvm::Instruction &I) const; + unsigned srcRegion(const llvm::Instruction &I) const; + + bool rewrite(llvm::Module &M); + bool removeIrrelevantInstructions(llvm::Function &F); + bool bypassIrrelevantLoops(llvm::Function &F); + + void emitProfile(llvm::Module &M); +}; + +llvm::ModulePass *createPropertySlicingPass(); +} // namespace smack + +#endif // PROPERTYSLICING_H diff --git a/lib/smack/PropertySlicing.cpp b/lib/smack/PropertySlicing.cpp new file mode 100644 index 000000000..fd92badd6 --- /dev/null +++ b/lib/smack/PropertySlicing.cpp @@ -0,0 +1,1276 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// + +#include "smack/PropertySlicing.h" +#include "smack/DSAWrapper.h" +#include "smack/Debug.h" +#include "smack/Naming.h" +#include "smack/Regions.h" +#include "smack/SmackOptions.h" + +#include "llvm/ADT/DepthFirstIterator.h" +#include "llvm/Analysis/LoopInfo.h" +#include "llvm/Analysis/PostDominators.h" +#include "llvm/IR/CFG.h" +#include "llvm/IR/Constants.h" +#include "llvm/IR/InstIterator.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/Support/FileSystem.h" +#include "llvm/Support/raw_ostream.h" +#include "llvm/Transforms/Utils/BasicBlockUtils.h" + +#include +#include +#include +#include + +#define DEBUG_TYPE "property-slicing" + +namespace smack { + +using namespace llvm; + +// ---------------------------------------------------------------- options + +const llvm::cl::opt PropertySlicingEnabled( + "property-slicing", + llvm::cl::desc("Remove program behaviour that cannot influence the " + "assertion property before Boogie generation.")); + +const llvm::cl::opt PropertySlicingNoLoopBypass( + "property-slicing-no-loop-bypass", + llvm::cl::desc("Property slicing: remove irrelevant instructions but keep " + "every loop (for isolating correctness failures).")); + +const llvm::cl::opt PropertySlicingRelaxAsm( + "property-slicing-relax-asm", + llvm::cl::desc("Property slicing: treat inline asm as the no-op SMACK's " + "own translation already makes it.")); + +const llvm::cl::opt PropertySlicingNoRegions( + "property-slicing-no-regions", + llvm::cl::desc("Property slicing: ignore the region partition and treat " + "all memory as one object (ablation experiment).")); + +const llvm::cl::opt PropertySlicingProfile( + "property-slicing-profile", + llvm::cl::desc("Write a machine-readable property-slicing profile here."), + llvm::cl::value_desc("filename")); + +namespace { + +/// A helper that never lies about not knowing: any callee we cannot resolve to +/// a single Function is treated as unknown. +const Function *calleeOf(const CallInst &CI) { + if (auto F = CI.getCalledFunction()) + return F; + if (auto V = CI.getCalledOperand()) + if (auto F = dyn_cast(V->stripPointerCastsAndAliases())) + return F; + return nullptr; +} + +/// Control dependence, computed from the post-dominator tree by the standard +/// edge-walk: for every CFG edge A->S where S does not post-dominate A, every +/// node on the post-dominator path from S up to (but excluding) ipdom(A) is +/// control-dependent on A. Linear in the size of the post-dominator tree paths +/// walked, so it stays within the "cheap analyses only" budget. +/// Blocks from which a function exit is reachable. Post-dominance is only +/// meaningful for these: LLVM's PostDominatorTree still yields a tree over a +/// reverse-unreachable region (an infinite loop), but the immediate +/// post-dominator it picks there is an artifact of how the virtual root is +/// attached, not a semantic one. Measured on test/c/basic/jain_5_true.c -- +/// `while (1) { ...; assert(x != 30); }`, a function with no return at all -- +/// the tree named the *taken* successor as ipdom of the deciding block, so the +/// assertion's own guard came out control-dependent on nothing, was replaced +/// by undef, and turned a verified program into a spurious error. +void collectExitReaching(Function &F, + std::unordered_set &R) { + std::vector work; + for (auto &BB : F) { + auto *T = BB.getTerminator(); + if (isa(T) || isa(T) || isa(T)) { + R.insert(&BB); + work.push_back(&BB); + } + } + while (!work.empty()) { + auto *B = work.back(); + work.pop_back(); + for (auto *P : predecessors(B)) + if (R.insert(P).second) + work.push_back(P); + } +} + +void computeControlDependence( + Function &F, PostDominatorTree &PDT, + const std::unordered_set &ExitReaching, + std::unordered_map> + &CD) { + for (auto &A : F) { + auto *T = A.getTerminator(); + if (!T || T->getNumSuccessors() < 2) + continue; + if (!ExitReaching.count(&A)) + continue; // post-dominance undefined here; the branch is kept instead + auto *ANode = PDT.getNode(&A); + if (!ANode) + continue; + auto *AIdom = ANode->getIDom(); + for (auto *S : successors(&A)) { + auto *N = PDT.getNode(S); + while (N && N != AIdom) { + if (N->getBlock()) + CD[N->getBlock()].push_back(&A); + N = N->getIDom(); + } + } + } +} + +double secondsSince(std::chrono::steady_clock::time_point T0) { + return std::chrono::duration(std::chrono::steady_clock::now() - T0) + .count(); +} + +} // namespace + +const char *PropertySlicing::reasonName(LoopReason R) { + switch (R) { + case LoopReason::ERROR_REACHABLE: + return "ERROR_REACHABLE"; + case LoopReason::RELEVANT_SCALAR: + return "RELEVANT_SCALAR"; + case LoopReason::RELEVANT_REGION: + return "RELEVANT_REGION"; + case LoopReason::CONTROL: + return "CONTROL"; + case LoopReason::UNKNOWN_CALL: + return "UNKNOWN_CALL"; + case LoopReason::VOLATILE_ATOMIC: + return "VOLATILE_ATOMIC"; + case LoopReason::DSA_COLLAPSED_REGION: + return "DSA_COLLAPSED_REGION"; + case LoopReason::ESCAPING_VALUE: + return "ESCAPING_VALUE"; + case LoopReason::NO_PREHEADER: + return "NO_PREHEADER"; + case LoopReason::MULTIPLE_EXITS: + return "MULTIPLE_EXITS"; + case LoopReason::NO_EXIT: + return "NO_EXIT"; + case LoopReason::OTHER_CONSERVATIVE: + return "OTHER_CONSERVATIVE"; + case LoopReason::BYPASSED: + return "BYPASSED"; + } + return "OTHER_CONSERVATIVE"; +} + +void PropertySlicing::getAnalysisUsage(AnalysisUsage &AU) const { + // The pass only deletes instructions and blocks; it never creates a memory + // operation. The region partition computed on the pre-slice module is + // therefore coarser than or equal to one computed afterwards, which is the + // conservative direction for a memory model -- so Regions (and the sea-DSA + // graph its Nodes point into) stay valid and are explicitly preserved, + // sparing a second whole-module DSA run. LoopInfo/PostDominatorTree are + // deliberately NOT preserved: the CFG does change. + AU.addRequired(); + AU.addRequired(); + AU.addPreserved(); + AU.addPreserved(); + AU.addRequired(); + AU.addRequired(); +} + +// ------------------------------------------------------------- predicates + +/// The property root. SMACK does not mark it in the IR at all: for SV-COMP, +/// `call reach_error()` is rewritten to `assert false; call reach_error();` by +/// a textual pass over the generated .bpl (share/smack/top.py, in +/// replace_reach_error), long after this pass has run. The root at this point +/// in the pipeline is therefore purely a call to a specially-named function, +/// and the set below is exactly the set of names that later become Boogie +/// asserts or otherwise carry verification semantics. +bool PropertySlicing::isPropertyRoot(const CallInst &CI) const { + auto F = calleeOf(CI); + if (!F || !F->hasName()) + return false; + auto N = F->getName(); + // SV-COMP unreach-call: rewritten to `assert false` after translation. + if (N == "reach_error") + return true; + // SMACK's own assertion, and the Rust panic marker. + if (N == "__VERIFIER_assert" || N == Naming::RUST_PANIC_MARKER) + return true; + return false; +} + +/// Calls that change the verification state or emit Boogie text, and so must +/// never be elided. Every name here is taken from SMACK's own dispatch -- +/// SmackInstGenerator::visitCallInst (lib/smack/SmackInstGenerator.cpp:638-700) +/// and the Naming constants (lib/smack/Naming.cpp:25-60) -- rather than from +/// intuition about what a `__VERIFIER_`-looking name might mean. +/// +/// The distinction that matters most for the slice is that a *nondeterminism* +/// function is pure: `__VERIFIER_nondet_*` and `__SMACK_nondet_*` merely yield +/// an unconstrained value, and SMACK itself treats them as ordinary external +/// calls whose only content is that value (note EXTERNAL_PROC_IGNORE at +/// SmackInstGenerator.cpp:39 exempting `__VERIFIER_nondet` from even the +/// external-address assumption). Classifying them as verification effects made +/// every function that draws a nondeterministic value un-droppable, and by +/// transitivity poisoned nearly the whole call graph. +bool PropertySlicing::hasVerificationEffect(const CallInst &CI) const { + auto F = calleeOf(CI); + if (!F || !F->hasName()) + return false; + auto N = F->getName(); + + // Pure value producers and the arithmetic models: droppable when the result + // is irrelevant. __SMACK_and*/__SMACK_or* come from RewriteBitwiseOps + // (RewriteBitwiseOps.cpp:107-142); this pass runs before it, but the guard + // keeps the predicate correct if that order changes. + if (N.contains("__VERIFIER_nondet") || N.contains("__SMACK_nondet") || + N.startswith("__SMACK_and") || N.startswith("__SMACK_or") || + N == "__SMACK_dummy") + return false; + + // Assertions and assumptions constrain or check the state. + if (N == "__VERIFIER_assert" || N == "__VERIFIER_assume" || + N == "reach_error" || N == Naming::RUST_PANIC_MARKER) + return true; + + // Annotations that become Boogie text verbatim. SMACK matches these as + // substrings, so match them the same way. + for (auto &P : + {Naming::CODE_PROC, Naming::DECL_PROC, Naming::TOP_DECL_PROC, + Naming::MOD_PROC, Naming::VALUE_PROC, Naming::RETURN_VALUE_PROC, + Naming::DECLARATIONS_PROC, Naming::STATIC_INIT_PROC, Naming::LOOP_EXIT, + Naming::CONTRACT_REQUIRES, Naming::CONTRACT_ENSURES, + Naming::CONTRACT_INVARIANT, Naming::CONTRACT_FORALL, + Naming::CONTRACT_EXISTS}) + if (N.contains(P)) + return true; + + return false; +} + +/// Effects the region abstraction does not capture. Retained unconditionally. +/// +/// Note what is NOT here. A *volatile* load or store is an ordinary load or +/// store to SMACK: nothing in the translator inspects LoadInst/StoreInst +/// volatility (the only isVolatile() reads in the tree are SmackRep.cpp:322 and +/// :346, which pass the flag through to the memcpy/memset models), and Regions +/// registers those pointers like any other. Treating volatility as an +/// unmodelled effect here would make the slicer stricter than the semantics it +/// is slicing, for no soundness gain. +bool PropertySlicing::hasUnmodelledEffect(const Instruction &I) const { + // Atomicity is not here either, and for the same reason. SMACK translates + // AtomicCmpXchg and AtomicRMW as a plain load followed by a plain store on + // the same region (SmackInstGenerator.cpp:551-576) -- the ordering and the + // atomicity are simply dropped -- and visitLoadInst/visitStoreInst never + // consult an ordering at all. Regions registers all four instruction kinds + // (Regions.cpp, visitAtomicCmpXchgInst/visitAtomicRMWInst), so the region + // rules already cover them exactly as they cover ordinary memory. Treating + // them as unmodelled cost 12 of the 77 un-droppable seeds on the he.ko + // driver task for no soundness gain. + if (isa(&I)) + return true; + if (auto CI = dyn_cast(&I)) { + if (CI->isInlineAsm()) + // SmackInstGenerator.cpp:641-646 already translates every inline asm to + // Stmt::skip() -- a complete no-op -- and warns that this "can lead to + // both false alarms and missed detections". Under -property-slicing- + // relax-asm the slicer adopts that same semantics, which cannot lose an + // error the translator would have kept. It is off by default so the + // prototype's baseline retains anything the region abstraction does not + // capture. + return !PropertySlicingRelaxAsm; + if (!calleeOf(*CI)) + return true; // unresolved indirect target + } + if (isa(&I) || isa(&I) || isa(&I)) + return true; + if (isa(&I) || isa(&I)) + return true; + return false; +} + +// ------------------------------------------------------------- call graph + +void PropertySlicing::computeMayReachError(Module &M) { + std::unordered_map> callers; + std::queue work; + + for (auto &F : M) { + if (F.isDeclaration()) + continue; + bool root = false; + for (auto &I : instructions(F)) { + if (auto CI = dyn_cast(&I)) { + if (isPropertyRoot(*CI)) + root = true; + if (auto G = calleeOf(*CI)) + callers[G].push_back(&F); + else if (!CI->isInlineAsm()) + // An unresolved indirect call may reach anything. Inline asm cannot + // reach a C function at all, and counting it here marked 33 extra + // functions on he.ko as error-reaching. + root = true; + } + } + if (root && !mayReachError.count(&F)) { + mayReachError.insert(&F); + work.push(&F); + } + } + + while (!work.empty()) { + auto F = work.front(); + work.pop(); + for (auto C : callers[F]) + if (!mayReachError.count(C)) { + mayReachError.insert(C); + work.push(C); + } + } +} + +/// `unsafeToDrop` and `writtenRegions` in one greatest-fixpoint pass. +/// Optimistic initialisation (everything droppable) is what makes recursive +/// but effect-free functions droppable; the iteration only ever removes +/// safety, so it converges. +void PropertySlicing::computeEffects(Module &M) { + std::unordered_map> callees; + + for (auto &F : M) { + if (F.isDeclaration()) { + // No body: unknown effects unless LLVM itself proves otherwise. + if (!F.doesNotAccessMemory() && !F.onlyReadsMemory()) + unsafeToDrop.insert(&F); + continue; + } + auto &W = writtenRegions[&F]; + for (auto &I : instructions(F)) { + if (hasUnmodelledEffect(I)) { + if (unsafeToDrop.insert(&F).second) + unsafeWhy[&F] = + isa(&I) && cast(&I)->isInlineAsm() + ? "inline_asm" + : (isa(&I) ? "indirect_call" : "atomic"); + } + if (isa(&I) || isa(&I) || + isa(&I) || isa(&I)) { + unsigned r = destRegion(I); + if (r == TOP_REGION) + writesTop.insert(&F); + else + W.insert(r); + } + + if (auto CI = dyn_cast(&I)) { + if (hasVerificationEffect(*CI)) { + if (unsafeToDrop.insert(&F).second) + unsafeWhy[&F] = "verification_effect"; + } + if (auto G = calleeOf(*CI)) + callees[&F].push_back(G); + } + } + if (mayReachError.count(&F)) + if (unsafeToDrop.insert(&F).second) + unsafeWhy[&F] = "may_reach_error"; + } + + bool changed = true; + while (changed) { + changed = false; + for (auto &F : M) { + if (F.isDeclaration()) + continue; + auto &W = writtenRegions[&F]; + for (auto G : callees[&F]) { + if (unsafeToDrop.count(G) && !unsafeToDrop.count(&F)) { + unsafeToDrop.insert(&F); + unsafeWhy[&F] = "callee:" + G->getName().str(); + changed = true; + } + if (writesTop.count(G) && !writesTop.count(&F)) { + writesTop.insert(&F); + changed = true; + } + auto it = writtenRegions.find(G); + if (it == writtenRegions.end()) + continue; + for (auto r : it->second) + if (W.insert(r).second) + changed = true; + } + } + } +} + +// ------------------------------------------------------------- relevance + +/// A pointer whose object SMACK's region machinery cannot pin down. +/// +/// This is the hole that matters most for a slicer. When `DSAWrapper::getNode` +/// returns null, `Region::init` sets incomplete = complicated = collapsed = +/// true, but `Region::overlaps` only unifies two *complicated* regions -- and +/// `Node::isIncomplete()` is dead in the pinned sea-DSA (it has no setter), so +/// the `incomplete && R.incomplete` disjunct never fires against a real node. +/// A cell-less pointer therefore receives its OWN region, disjoint from every +/// ordinary one, and `idx(p) != idx(q)` comes back for pointers that may very +/// well alias. sea-DSA's own `mayAlias` returns true in exactly this case. +/// SMACK's memory model lives with that; a slicer that used it to *delete* a +/// store would not be sound, so such accesses are forced to TOP_REGION here. +bool PropertySlicing::isOpaquePointer(const Value *Ptr) const { + if (!Ptr || isa(Ptr) || isa(Ptr)) + return true; + if (!DSA) + return true; + return DSA->getNode(Ptr) == nullptr; +} + +namespace { +/// Length a memory intrinsic accesses, or UINT_MAX when it is not constant -- +/// which Regions also uses, and which makes `Region::isDisjoint`'s unsigned +/// `offset + length` wrap at any non-zero offset and report a false +/// disjointness (Regions.cpp:68-71, plain `unsigned`, unlike `merge` at :75). +unsigned intrinsicLength(const MemIntrinsic &MI) { + if (auto CI = dyn_cast(MI.getLength())) + return CI->getZExtValue(); + return std::numeric_limits::max(); +} +} // namespace + +/// Freeze the region partition before any slicing decision depends on it. +/// +/// `Regions::idx` is stateful: it constructs a fresh Region on every call, +/// merges it into the first overlapping entry, then cascades -- and the +/// cascade calls `regions.erase`, which renumbers every index above it. Indices +/// read at different times are therefore not comparable. Two passes are made: +/// the first drives the merging to a fixpoint, the second records indices that +/// are never re-derived. +void PropertySlicing::snapshotRegions(Module &M) { + for (unsigned pass = 0; pass < 2; ++pass) { + memRegion.clear(); + memRegionSrc.clear(); + for (auto &F : M) { + if (F.isDeclaration()) + continue; + for (auto &I : instructions(F)) { + if (auto MI = dyn_cast(&I)) { + unsigned len = intrinsicLength(*MI); + bool wide = (len == std::numeric_limits::max()); + const Value *D = MI->getDest(); + memRegion[&I] = + (wide || isOpaquePointer(D)) ? TOP_REGION : regions->idx(D, len); + if (auto MT = dyn_cast(&I)) { + const Value *Sp = MT->getSource(); + memRegionSrc[&I] = (wide || isOpaquePointer(Sp)) + ? TOP_REGION + : regions->idx(Sp, len); + } + continue; + } + const Value *P = nullptr; + if (auto LI = dyn_cast(&I)) + P = LI->getPointerOperand(); + else if (auto SI = dyn_cast(&I)) + P = SI->getPointerOperand(); + else if (auto RMW = dyn_cast(&I)) + P = RMW->getPointerOperand(); + else if (auto CX = dyn_cast(&I)) + P = CX->getPointerOperand(); + if (!P) + continue; + memRegion[&I] = isOpaquePointer(P) ? TOP_REGION : regions->idx(P); + } + } + } +} + +unsigned PropertySlicing::destRegion(const Instruction &I) const { + auto it = memRegion.find(&I); + return it == memRegion.end() ? TOP_REGION : it->second; +} + +unsigned PropertySlicing::srcRegion(const Instruction &I) const { + auto it = memRegionSrc.find(&I); + return it == memRegionSrc.end() ? TOP_REGION : it->second; +} + +/// Render why an instruction ended up relevant, as a short chain terminating +/// in whatever seeded it. +std::string PropertySlicing::explainRelevance(const Instruction *I) const { + std::string out; + const Instruction *cur = I; + for (unsigned hop = 0; cur && hop < 8; ++hop) { + if (!out.empty()) + out += " -> "; + out += cur->getOpcodeName(); + if (auto CI = dyn_cast(cur)) + if (auto G = calleeOf(*CI)) + out += "(" + G->getName().str() + ")"; + if (cur != I && cur->getFunction() != I->getFunction()) + out += "@" + cur->getFunction()->getName().str(); + auto it = relevantVia.find(cur); + if (it == relevantVia.end()) + break; + if (it->second == cur) + break; + cur = it->second; + } + return out; +} + +const Instruction * +PropertySlicing::relevanceTerminus(const Instruction *I) const { + const Instruction *cur = I; + for (unsigned hop = 0; cur && hop < 16; ++hop) { + auto it = relevantVia.find(cur); + if (it == relevantVia.end() || it->second == cur) + break; + cur = it->second; + } + return cur; +} + +void PropertySlicing::markValue(const Value *V, bool &changed) { + if (!V || isa(V) || isa(V)) + return; + if (relevant.insert(V).second) { + changed = true; + if (markSource) + relevantVia[V] = markSource; + } +} + +/// A read whose region is TOP could have come from anywhere, so every region +/// becomes relevant -- otherwise a store the read can observe might be dropped. +void PropertySlicing::markRegionIdx(unsigned r, const Instruction &I, + bool &changed) { + if (r == TOP_REGION) { + if (!topRelevant) { + topRelevant = true; + changed = true; + } + return; + } + if (relevantRegions.insert(r).second) { + changed = true; + if (!regionWhy.count(r)) + regionWhy[r] = I.getFunction()->getName().str(); + } +} + +bool PropertySlicing::regionIsRelevant(unsigned r) const { + return topRelevant || r == TOP_REGION || relevantRegions.count(r) > 0; +} + +void PropertySlicing::seedRoots(Module &M) { + for (auto &F : M) { + if (F.isDeclaration()) + continue; + for (auto &I : instructions(F)) { + bool isRoot = false; + if (auto CI = dyn_cast(&I)) + isRoot = isPropertyRoot(*CI) || hasVerificationEffect(*CI); + // Effects the abstraction cannot model are retained from the start. + if (isRoot || hasUnmodelledEffect(I)) + keep.insert(&I); + } + } +} + +void PropertySlicing::propagate(Module &M) { + // Per-function control dependence, computed once. + for (auto &F : M) { + if (F.isDeclaration()) + continue; + auto &PDT = getAnalysis(F).getPostDomTree(); + auto &ER = exitReaching[&F]; + collectExitReaching(F, ER); + computeControlDependence(F, PDT, ER, CD[&F]); + // Where post-dominance is undefined, retain every branch outright. + for (auto &BB : F) + if (!ER.count(&BB)) { + keep.insert(BB.getTerminator()); + for (auto &Op : BB.getTerminator()->operands()) { + bool ignored = false; + markValue(Op.get(), ignored); + } + } + for (auto &kv : CD[&F]) + cdEdges += kv.second.size(); + for (auto &BB : F) + if (!PDT.getNode(&BB)) + pdtHoles++; + } + + bool changed = true; + while (changed) { + changed = false; + for (auto &F : M) { + if (F.isDeclaration()) + continue; + + for (auto &I : instructions(F)) { + bool kept = keep.count(&I) > 0; + + if (!kept && relevant.count(&I)) + kept = true; + + if (!kept) { + if (isa(&I) || isa(&I) || + isa(&I) || isa(&I)) { + // A write whose region is TOP may land on any relevant object. + if (regionIsRelevant(destRegion(I))) + kept = true; + } else if (auto CI = dyn_cast(&I)) { + auto G = calleeOf(*CI); + if (!G) + // No resolvable callee: an indirect target could do anything. + // Inline asm is the one exception under + // -property-slicing-relax-asm, where we adopt SMACK's own + // Stmt::skip() semantics for it. + kept = !(CI->isInlineAsm() && PropertySlicingRelaxAsm); + else if (mayReachError.count(G) || unsafeToDrop.count(G) || + writesTop.count(G)) + kept = true; + else { + auto it = writtenRegions.find(G); + if (it != writtenRegions.end()) + for (auto r : it->second) + if (regionIsRelevant(r)) + kept = true; + } + } + } + + if (!kept) + continue; + if (keep.insert(&I).second) + changed = true; + + // A kept instruction needs its operands. For a call, marking every + // actual wholesale is sound but very coarse: a call is frequently kept + // only because the callee may reach the error or has an effect on some + // other region, and then none of its arguments need be relevant. So + // propagate per-parameter instead -- an actual becomes relevant only + // when the corresponding formal is relevant inside the callee, which + // ordinary intraprocedural propagation establishes. Callees without a + // body keep the wholesale rule, since nothing can be established about + // them. + markSource = &I; + auto CIforArgs = dyn_cast(&I); + const Function *Gee = CIforArgs ? calleeOf(*CIforArgs) : nullptr; + if (CIforArgs && Gee && !Gee->isDeclaration() && !Gee->isVarArg() && + Gee->arg_size() == CIforArgs->arg_size()) { + unsigned k = 0; + for (auto &A : Gee->args()) { + if (relevant.count(&A)) + markValue(CIforArgs->getArgOperand(k), changed); + ++k; + } + } else { + for (auto &Op : I.operands()) + markValue(Op.get(), changed); + } + if (isa(&I) || isa(&I) || + isa(&I)) + markRegionIdx(destRegion(I), I, changed); + else if (isa(&I)) + markRegionIdx(srcRegion(I), I, changed); + + markSource = nullptr; + + // A relevant PHI depends not only on its incoming values but on + // WHICH edge was taken, so the branches that select between them must + // be retained. Without this the merge block is not control-dependent + // on the deciding branch (it post-dominates it), the condition is + // replaced by undef, and the PHI becomes nondeterministic -- sound, + // but a false-alarm factory: it is what turned test/c/data/func_ptr.c + // from verified into a spurious error. This is the rule the unbuilt + // contract slicer also used (lib/smack/Slicing.cpp:159-164). + if (auto PN = dyn_cast(&I)) { + for (unsigned k = 0, e = PN->getNumIncomingValues(); k < e; ++k) { + auto *T = PN->getIncomingBlock(k)->getTerminator(); + if (keep.insert(T).second) + changed = true; + for (auto &Op : T->operands()) + markValue(Op.get(), changed); + } + } + + // A relevant call result makes the callee's returned values relevant. + if (auto CI = dyn_cast(&I)) { + if (relevant.count(CI)) { + if (auto G = calleeOf(*CI)) + if (!G->isDeclaration()) + for (auto &BB : *G) + if (auto RI = dyn_cast(BB.getTerminator())) + if (RI->getReturnValue()) { + markValue(RI->getReturnValue(), changed); + if (keep.insert(RI).second) + changed = true; + } + } + } + } + + // Control dependence: a block holding a kept instruction needs the + // predicates that decide whether it executes. + auto &cd = CD[&F]; + for (auto &BB : F) { + bool blockNeeded = false; + for (auto &I : BB) + if (keep.count(&I)) { + blockNeeded = true; + break; + } + if (!blockNeeded) + continue; + auto it = cd.find(&BB); + if (it == cd.end()) + continue; + for (auto *A : it->second) { + auto *T = A->getTerminator(); + if (keep.insert(T).second) + changed = true; + for (auto &Op : T->operands()) + markValue(Op.get(), changed); + } + } + + // Returns of a function whose result someone relevant consumes are + // handled above; a function that may reach the error keeps its returns + // so the call graph stays traversable. + if (mayReachError.count(&F)) + for (auto &BB : F) + if (auto RI = dyn_cast(BB.getTerminator())) + if (keep.insert(RI).second) + changed = true; + } + } +} + +// -------------------------------------------------------------- rewriting + +bool PropertySlicing::removeIrrelevantInstructions(Function &F) { + bool changed = false; + std::vector dead; + + for (auto &BB : F) { + for (auto &I : BB) { + if (I.isTerminator()) + continue; + if (keep.count(&I)) + continue; + dead.push_back(&I); + } + } + + // Backward closure means a dropped instruction can only have dropped users, + // so deleting in reverse program order leaves no dangling uses. Anything + // that still has a use is left in place rather than risking an invalid + // module. + for (auto it = dead.rbegin(); it != dead.rend(); ++it) { + Instruction *I = *it; + if (!I->use_empty()) + continue; + auto &S = stats[&F]; + if (isa(I)) + S.loadsRemoved++; + else if (isa(I)) + S.storesRemoved++; + else if (isa(I)) + S.callsRemoved++; + I->eraseFromParent(); + changed = true; + } + + // A branch whose condition nothing relevant depends on becomes + // nondeterministic rather than being deleted: the CFG shape is preserved and + // the added executions are the sound direction for reachability. This is the + // same device the (unbuilt) contract slicer used in Slice::remove. + for (auto &BB : F) { + auto *T = BB.getTerminator(); + if (keep.count(T)) + continue; + if (auto *BI = dyn_cast(T)) { + if (BI->isConditional() && !isa(BI->getCondition())) { + SDEBUG({ + errs() << "[property-slicing] " << F.getName() << ": branch made " + << "nondeterministic:" << *BI << "\n"; + for (auto *S : successors(&BB)) { + unsigned k = 0; + for (auto &I2 : *S) + if (keep.count(&I2)) + k++; + auto cd = CD[&F].find(S); + errs() << " successor keeps " << k << " instruction(s), " + << (cd == CD[&F].end() ? 0 : cd->second.size()) + << " controlling block(s)\n"; + } + }); + auto *C = BI->getCondition(); + BI->setCondition(UndefValue::get(C->getType())); + changed = true; + } + } else if (auto *SI = dyn_cast(T)) { + if (!isa(SI->getCondition())) { + SI->setCondition(UndefValue::get(SI->getCondition()->getType())); + changed = true; + } + } + } + return changed; +} + +bool PropertySlicing::bypassIrrelevantLoops(Function &F) { + auto &LI = getAnalysis(F).getLoopInfo(); + auto &S = stats[&F]; + bool changed = false; + + // Innermost-first: bypassing an inner loop can make an outer one droppable + // on a later run, but within one run we only consider loops whose entire + // body (including nested loops) is irrelevant. + std::vector worklist(LI.begin(), LI.end()); + std::vector all; + while (!worklist.empty()) { + Loop *L = worklist.back(); + worklist.pop_back(); + all.push_back(L); + for (Loop *Sub : *L) + worklist.push_back(Sub); + } + + for (Loop *L : all) { + LoopReason reason = LoopReason::OTHER_CONSERVATIVE; + bool droppable = true; + std::string blocker; + + for (auto *BB : L->blocks()) { + for (auto &I : *BB) { + if (I.isTerminator()) + continue; + if (hasUnmodelledEffect(I)) { + reason = LoopReason::VOLATILE_ATOMIC; + droppable = false; + break; + } + if (keep.count(&I)) { + // Classify by what the blocking value is ultimately needed for, not + // by the first instruction encountered in block order -- that is + // nearly always the induction PHI, which says nothing. + const Instruction *T = relevanceTerminus(&I); + if (auto CI = dyn_cast(T ? T : &I)) { + auto G = calleeOf(*CI); + if (!G) + reason = LoopReason::UNKNOWN_CALL; + else if (mayReachError.count(G)) + reason = LoopReason::ERROR_REACHABLE; + else if (unsafeToDrop.count(G)) + reason = LoopReason::UNKNOWN_CALL; + else + reason = LoopReason::RELEVANT_REGION; + } else if (T && + (isa(T) || isa(T) || + isa(T) || isa(T))) { + reason = LoopReason::RELEVANT_REGION; + } else if (T && T->isTerminator()) { + reason = LoopReason::CONTROL; + } else { + reason = LoopReason::RELEVANT_SCALAR; + } + blocker = explainRelevance(&I); + droppable = false; + break; + } + } + if (!droppable) + break; + // A kept terminator inside the loop means something downstream is + // control-dependent on it. + if (keep.count(BB->getTerminator()) && BB != L->getLoopLatch()) { + reason = LoopReason::CONTROL; + droppable = false; + break; + } + } + + BasicBlock *P = L->getLoopPreheader(); + BasicBlock *E = L->getExitBlock(); + if (droppable && !P) { + // A dedicated preheader would come from LoopSimplify, but requiring + // LoopSimplifyID from a ModulePass crashes the legacy pass manager here. + reason = LoopReason::NO_PREHEADER; + droppable = false; + blocker = "no dedicated preheader"; + } else if (droppable && !E) { + llvm::SmallVector Ex; + L->getExitBlocks(Ex); + blocker = "exit blocks: " + std::to_string(Ex.size()); + // Zero exit blocks means the loop never leaves -- there is nowhere to + // redirect the preheader to, so no bypass exists at any precision. + reason = Ex.empty() ? LoopReason::NO_EXIT : LoopReason::MULTIPLE_EXITS; + droppable = false; + } + + // A value defined in the loop and used outside it loses its definition + // when the loop goes. If any such external user is itself relevant, the + // loop's result matters after all and the loop stays. Otherwise the escape + // is repairable: the backward slice has already established that nothing + // relevant reads the value, so external uses can be replaced by undef -- + // which only adds behaviours. Refusing these outright kept 28 of the 41 + // loops on he.ko. + std::vector escapes; + if (droppable) { + for (auto *BB : L->blocks()) { + for (auto &I : *BB) { + for (auto &U : I.uses()) { + auto UI = dyn_cast(U.getUser()); + if (!UI || L->contains(UI->getParent())) + continue; + if (keep.count(UI)) { + reason = LoopReason::ESCAPING_VALUE; + blocker = std::string(I.getOpcodeName()) + " escapes to " + + explainRelevance(UI); + droppable = false; + break; + } + escapes.push_back(&U); + } + if (!droppable) + break; + } + if (!droppable) + break; + } + } + + // Record the loop's source line so a profile can be matched against the + // `SMACK warning: found loop at line N` diagnostics, which are emitted by + // LoopBoundWarnings earlier in the pipeline and therefore still describe + // the pre-slice module. + unsigned line = 0; + if (auto SL = L->getStartLoc()) + line = SL.getLine(); + if (!line) + for (auto *BB : L->blocks()) { + for (auto &I : *BB) + if (auto DL2 = I.getDebugLoc()) { + line = DL2.getLine(); + break; + } + if (line) + break; + } + S.loopReasons.push_back( + {std::string(F.getName()) + ":" + std::to_string(line), + droppable ? LoopReason::BYPASSED : reason}); + if (!droppable && !blocker.empty()) + S.loopBlockers.push_back(std::string(reasonName(reason)) + " | " + + blocker); + + if (!droppable) { + S.loopsKept++; + continue; + } + + // Detach the irrelevant escaping values before the definitions go away. + for (auto *U : escapes) + U->set(UndefValue::get(U->get()->getType())); + + // Redirect the preheader past the loop. This can add the execution that + // skips a nonterminating loop -- sound for reachability, and recorded as + // an over-approximation. + auto *T = P->getTerminator(); + bool redirected = false; + for (unsigned i = 0; i < T->getNumSuccessors(); ++i) + if (T->getSuccessor(i) == L->getHeader()) { + T->setSuccessor(i, E); + redirected = true; + } + if (!redirected) { + S.loopsKept++; + continue; + } + // The exit block gains a new predecessor; its PHIs need an incoming value + // for it. Nothing relevant reads them, so undef is adequate and stays on + // the "more behaviours" side. + for (auto &PN : E->phis()) + if (PN.getBasicBlockIndex(P) < 0) + PN.addIncoming(UndefValue::get(PN.getType()), P); + + S.loopsBypassed++; + changed = true; + } + + if (changed) { + // Drops the now-unreachable loop bodies and repairs their PHI uses. + EliminateUnreachableBlocks(F); + } + return changed; +} + +bool PropertySlicing::rewrite(Module &M) { + bool changed = false; + for (auto &F : M) { + if (F.isDeclaration()) + continue; + auto &S = stats[&F]; + S.instructionsBefore = 0; + for (auto &BB : F) { + S.blocksBefore++; + for (auto &I : BB) { + (void)I; + S.instructionsBefore++; + } + } + { + auto &LI = getAnalysis(F).getLoopInfo(); + std::vector wl(LI.begin(), LI.end()); + while (!wl.empty()) { + Loop *L = wl.back(); + wl.pop_back(); + S.loopsBefore++; + for (Loop *Sub : *L) + wl.push_back(Sub); + } + } + for (auto &I : instructions(F)) + if (relevant.count(&I)) + S.relevantValues++; + + if (!PropertySlicingNoLoopBypass) + changed |= bypassIrrelevantLoops(F); + changed |= removeIrrelevantInstructions(F); + + for (auto &BB : F) { + S.blocksAfter++; + for (auto &I : BB) { + S.instructionsAfter++; + if (isa(&I)) + S.loadsRetained++; + else if (isa(&I)) + S.storesRetained++; + else if (isa(&I)) + S.callsRetained++; + } + } + } + return changed; +} + +// ---------------------------------------------------------------- profile + +void PropertySlicing::emitProfile(Module &M) { + if (PropertySlicingProfile.empty()) + return; + std::error_code EC; + raw_fd_ostream O(PropertySlicingProfile, EC, sys::fs::OF_Text); + if (EC) { + errs() << "SMACK warning: cannot write property-slicing profile: " + << EC.message() << "\n"; + return; + } + O << "{\n \"module\": \"" << M.getName() << "\",\n"; + O << " \"analysis_seconds\": " << analysisSeconds << ",\n"; + O << " \"rewrite_seconds\": " << rewriteSeconds << ",\n"; + O << " \"regions_total\": " << regions->size() << ",\n"; + O << " \"regions_relevant\": " + << (topRelevant ? regions->size() : relevantRegions.size()) << ",\n"; + O << " \"top_region_reached\": " << (topRelevant ? "true" : "false") + << ",\n"; + { + unsigned opaque = 0, total = 0; + for (auto &kv : memRegion) { + total++; + if (kv.second == TOP_REGION) + opaque++; + } + for (auto &kv : memRegionSrc) { + total++; + if (kv.second == TOP_REGION) + opaque++; + } + O << " \"memory_ops\": " << total << ",\n"; + O << " \"memory_ops_opaque\": " << opaque << ",\n"; + // Naming the few accesses that force TOP is the single most useful + // precision diagnostic: on he.ko four of 1347 of them made all 76 regions + // relevant. + O << " \"opaque_sites\": ["; + bool fo = true; + unsigned shown = 0; + for (auto &kv : memRegion) { + if (kv.second != TOP_REGION || shown >= 20) + continue; + if (!fo) + O << ", "; + fo = false; + shown++; + std::string txt; + raw_string_ostream ss(txt); + ss << *kv.first; + auto t = ss.str(); + for (auto &ch : t) + if (ch == '"' || ch == '\\') + ch = '\''; + if (t.size() > 160) + t = t.substr(0, 160); + O << "{\"fn\": \"" << kv.first->getFunction()->getName() + << "\", \"inst\": \"" << t << "\"}"; + } + O << "],\n"; + } + O << " \"functions_may_reach_error\": " << mayReachError.size() << ",\n"; + O << " \"functions_unsafe_to_drop\": " << unsafeToDrop.size() << ",\n"; + O << " \"control_dependence_edges\": " << cdEdges << ",\n"; + O << " \"postdom_missing_nodes\": " << pdtHoles << ",\n"; + { + std::map tally; + for (auto &kv : unsafeWhy) { + auto w = kv.second; + if (w.rfind("callee:", 0) == 0) + w = "callee"; + tally[w]++; + } + O << " \"unsafe_reasons\": {"; + bool f = true; + for (auto &kv : tally) { + if (!f) + O << ", "; + f = false; + O << "\"" << kv.first << "\": " << kv.second; + } + O << "},\n"; + O << " \"region_provenance\": {"; + f = true; + for (auto &kv : regionWhy) { + if (!f) + O << ", "; + f = false; + O << "\"" << kv.first << "\": \"" << kv.second << "\""; + } + O << "},\n"; + } + O << " \"functions\": [\n"; + bool first = true; + for (auto &F : M) { + if (F.isDeclaration()) + continue; + auto &S = stats[&F]; + if (!first) + O << ",\n"; + first = false; + O << " {\"name\": \"" << F.getName() << "\"" + << ", \"instructions_before\": " << S.instructionsBefore + << ", \"instructions_after\": " << S.instructionsAfter + << ", \"blocks_before\": " << S.blocksBefore + << ", \"blocks_after\": " << S.blocksAfter + << ", \"loops_before\": " << S.loopsBefore + << ", \"loops_bypassed\": " << S.loopsBypassed + << ", \"loops_kept\": " << S.loopsKept + << ", \"relevant_values\": " << S.relevantValues + << ", \"loads_removed\": " << S.loadsRemoved + << ", \"loads_retained\": " << S.loadsRetained + << ", \"stores_removed\": " << S.storesRemoved + << ", \"stores_retained\": " << S.storesRetained + << ", \"calls_removed\": " << S.callsRemoved + << ", \"calls_retained\": " << S.callsRetained << ", \"loop_reasons\": ["; + bool f2 = true; + for (auto &LR : S.loopReasons) { + if (!f2) + O << ", "; + f2 = false; + O << "{\"loop\": \"" << LR.first << "\", \"reason\": \"" + << reasonName(LR.second) << "\"}"; + } + O << "], \"loop_blockers\": ["; + f2 = true; + for (auto &b : S.loopBlockers) { + if (!f2) + O << ", "; + f2 = false; + auto t = b; + for (auto &ch : t) + if (ch == '"' || ch == '\\') + ch = '\''; + O << "\"" << t << "\""; + } + O << "]}"; + } + O << "\n ]\n}\n"; +} + +// ------------------------------------------------------------------- pass + +bool PropertySlicing::runOnModule(Module &M) { + if (!PropertySlicingEnabled) + return false; + + // The over-approximation this pass performs is justified only for + // reachability. Memory-safety and overflow properties introduce roots the + // relevance rules above do not model, and termination is unsound by + // construction under loop bypass. + if (SmackOptions::MemorySafety || SmackOptions::IntegerOverflow) { + errs() << "SMACK warning: property slicing is only sound for assertion " + "reachability; disabling it for this property.\n"; + return false; + } + + // -fail-on-loop-exit asserts that no loop exit is reached, which is a + // property of the *unrolled approximation* rather than of the program: a + // "verified" verdict there means only that the bound was too small to leave + // the loop. Slicing legitimately changes when a loop is left -- an + // irrelevant loop may be bypassed outright -- so the two cannot both hold. + // Measured on test/c/unroll: nine tests flip from verified to a spurious + // error, with and without loop bypass. + if (SmackOptions::FailOnLoopExit) { + errs() << "SMACK warning: property slicing is incompatible with " + "-fail-on-loop-exit, whose property depends on the unroll " + "bound; disabling it.\n"; + return false; + } + + DL = &M.getDataLayout(); + regions = &getAnalysis(); + DSA = &getAnalysis(); + + auto T0 = std::chrono::steady_clock::now(); + // Ablation: with regions switched off every memory access is TOP, i.e. the + // heap is a single object -- exactly the model a slicer that did NOT reuse + // SMACK's DSA partition would have. Comparing the two answers directly how + // much the region abstraction is actually worth here. + topRelevant = PropertySlicingNoRegions; + snapshotRegions(M); + computeMayReachError(M); + computeEffects(M); + seedRoots(M); + propagate(M); + analysisSeconds = secondsSince(T0); + + auto T1 = std::chrono::steady_clock::now(); + bool changed = rewrite(M); + rewriteSeconds = secondsSince(T1); + + SDEBUG(errs() << "[property-slicing] regions " << relevantRegions.size() + << "/" << regions->size() << " relevant, " + << mayReachError.size() << " functions may reach the error\n"); + + emitProfile(M); + return changed; +} + +ModulePass *createPropertySlicingPass() { return new PropertySlicing(); } + +char PropertySlicing::ID = 0; +static RegisterPass X("property-slicing", + "SMACK Property-Directed Slicing"); + +} // namespace smack diff --git a/share/smack/top.py b/share/smack/top.py index fe69fe82e..7b56e67ea 100644 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -488,6 +488,41 @@ def arguments(): NOTE: a regular expression must match the entire function name. [default: everything]''') + translate_group.add_argument( + '--property-slicing', + action='store_true', + default=False, + help='remove program behaviour that cannot influence the assertion ' + 'property before Boogie generation (unreach-call only)') + + translate_group.add_argument( + '--property-slicing-no-loop-bypass', + action='store_true', + default=False, + help='with --property-slicing, drop irrelevant instructions but keep ' + 'every loop') + + translate_group.add_argument( + '--property-slicing-relax-asm', + action='store_true', + default=False, + help='with --property-slicing, treat inline asm as the no-op SMACK ' + 'already translates it to') + + translate_group.add_argument( + '--property-slicing-no-regions', + action='store_true', + default=False, + help='with --property-slicing, ignore the DSA region partition and ' + 'treat all memory as one object (ablation experiment)') + + translate_group.add_argument( + '--property-slicing-profile', + metavar='FILE', + default=None, + type=str, + help='with --property-slicing, write a machine-readable profile here') + translate_group.add_argument( '--check', metavar='PROPERTY', @@ -772,6 +807,16 @@ def llvm_to_bpl(args): cmd += ['-rust-panics'] if args.fail_on_loop_exit: cmd += ['-fail-on-loop-exit'] + if args.property_slicing: + cmd += ['-property-slicing'] + if args.property_slicing_no_loop_bypass: + cmd += ['-property-slicing-no-loop-bypass'] + if args.property_slicing_relax_asm: + cmd += ['-property-slicing-relax-asm'] + if args.property_slicing_no_regions: + cmd += ['-property-slicing-no-regions'] + if args.property_slicing_profile: + cmd += ['-property-slicing-profile', args.property_slicing_profile] if not args.modular: # Lets llvm2bpl warn only about the loops this bound fails to cover. # Under --modular there is no such bound, so it is left unset. diff --git a/test/c/property-slicing/array_fail.c b/test/c/property-slicing/array_fail.c new file mode 100644 index 000000000..94889aebc --- /dev/null +++ b/test/c/property-slicing/array_fail.c @@ -0,0 +1,12 @@ +#include "smack.h" +#include + +// @expect error + +int main(void) { + int a[4]; + a[0] = 0; + a[2] = 9; + assert(a[2] != 9); + return 0; +} diff --git a/test/c/property-slicing/call_modifies_other.c b/test/c/property-slicing/call_modifies_other.c new file mode 100644 index 000000000..782ae8e01 --- /dev/null +++ b/test/c/property-slicing/call_modifies_other.c @@ -0,0 +1,15 @@ +#include "smack.h" +#include + +// @expect verified +// The callee writes only to an object the assertion never reads. + +void store(int *p) { *p = 7; } + +int main(void) { + int watched = 1; + int other = 0; + store(&other); + assert(watched == 1); + return 0; +} diff --git a/test/c/property-slicing/call_modifies_region_fail.c b/test/c/property-slicing/call_modifies_region_fail.c new file mode 100644 index 000000000..4c30fa32e --- /dev/null +++ b/test/c/property-slicing/call_modifies_region_fail.c @@ -0,0 +1,15 @@ +#include "smack.h" +#include + +// @expect error +// The callee writes through a pointer the assertion reads: the call must be +// retained on the strength of its region effect alone, not its result. + +void store(int *p) { *p = 7; } + +int main(void) { + int x = 0; + store(&x); + assert(x != 7); + return 0; +} diff --git a/test/c/property-slicing/call_result_fail.c b/test/c/property-slicing/call_result_fail.c new file mode 100644 index 000000000..cf56d7f9b --- /dev/null +++ b/test/c/property-slicing/call_result_fail.c @@ -0,0 +1,13 @@ +#include "smack.h" +#include + +// @expect error + +int f(int x) { return x + 1; } + +int main(void) { + int a = __VERIFIER_nondet_int(); + __VERIFIER_assume(a == 1); + assert(f(a) != 2); + return 0; +} diff --git a/test/c/property-slicing/callee_error_fail.c b/test/c/property-slicing/callee_error_fail.c new file mode 100644 index 000000000..d92159e54 --- /dev/null +++ b/test/c/property-slicing/callee_error_fail.c @@ -0,0 +1,18 @@ +#include "smack.h" +#include + +// @expect error +// The error lives inside a callee whose result is unused: MayReachError must +// keep the call. + +void may_fail(int x) { + if (x == 3) { + assert(0); + } +} + +int main(void) { + int a = __VERIFIER_nondet_int(); + may_fail(a); + return 0; +} diff --git a/test/c/property-slicing/cast_alias_fail.c b/test/c/property-slicing/cast_alias_fail.c new file mode 100644 index 000000000..a3afe390d --- /dev/null +++ b/test/c/property-slicing/cast_alias_fail.c @@ -0,0 +1,14 @@ +#include "smack.h" +#include + +// @expect error +// A pointer cast keeps both accesses on one sea-DSA node, so the store must be +// retained even though the types differ. + +int main(void) { + int x = 0; + char *c = (char *)&x; + *c = 1; + assert(x == 0); + return 0; +} diff --git a/test/c/property-slicing/config.yml b/test/c/property-slicing/config.yml new file mode 100644 index 000000000..b37ae6b4c --- /dev/null +++ b/test/c/property-slicing/config.yml @@ -0,0 +1,3 @@ +skip: false +verifiers: [corral] +flags: [--property-slicing] diff --git a/test/c/property-slicing/dead_pure_call.c b/test/c/property-slicing/dead_pure_call.c new file mode 100644 index 000000000..29c69028b --- /dev/null +++ b/test/c/property-slicing/dead_pure_call.c @@ -0,0 +1,15 @@ +#include "smack.h" +#include + +// @expect verified +// A call whose result nothing relevant reads, and which touches no relevant +// region, may be dropped. + +int square(int x) { return x * x + 1; } + +int main(void) { + int a = __VERIFIER_nondet_int(); + square(a); + assert(1); + return 0; +} diff --git a/test/c/property-slicing/dead_scalar.c b/test/c/property-slicing/dead_scalar.c new file mode 100644 index 000000000..937a1c5bc --- /dev/null +++ b/test/c/property-slicing/dead_scalar.c @@ -0,0 +1,15 @@ +#include "smack.h" +#include + +// @expect verified +// A scalar computation nothing relevant reads must be removable without +// changing the verdict. + +int main(void) { + int a = __VERIFIER_nondet_int(); + int dead = a * 3 + 7; + dead = dead ^ (dead << 2); + int b = 1; + assert(b == 1); + return 0; +} diff --git a/test/c/property-slicing/distinct_objects.c b/test/c/property-slicing/distinct_objects.c new file mode 100644 index 000000000..8ddee5f3a --- /dev/null +++ b/test/c/property-slicing/distinct_objects.c @@ -0,0 +1,17 @@ +#include "smack.h" +#include + +// @expect verified +// Two separate objects: the store to `other` cannot influence the load from +// `watched`, so the slicer may drop it. Removing it must not change the +// verdict. + +int main(void) { + int watched = 1; + int other = 0; + int *p = &other; + int *q = &watched; + *p = __VERIFIER_nondet_int(); + assert(*q == 1); + return 0; +} diff --git a/test/c/property-slicing/external_call_kept.c b/test/c/property-slicing/external_call_kept.c new file mode 100644 index 000000000..8e7c172bf --- /dev/null +++ b/test/c/property-slicing/external_call_kept.c @@ -0,0 +1,15 @@ +#include "smack.h" +#include +#include + +// @expect verified +// An undefined external is never elided: its effects are unknown. + +extern int opaque(int); + +int main(void) { + int a = __VERIFIER_nondet_int(); + opaque(a); + assert(1); + return 0; +} diff --git a/test/c/property-slicing/global_fail.c b/test/c/property-slicing/global_fail.c new file mode 100644 index 000000000..78c9b5797 --- /dev/null +++ b/test/c/property-slicing/global_fail.c @@ -0,0 +1,14 @@ +#include "smack.h" +#include + +// @expect error + +int g = 0; + +void set(void) { g = 11; } + +int main(void) { + set(); + assert(g != 11); + return 0; +} diff --git a/test/c/property-slicing/heap_fail.c b/test/c/property-slicing/heap_fail.c new file mode 100644 index 000000000..21f763cce --- /dev/null +++ b/test/c/property-slicing/heap_fail.c @@ -0,0 +1,14 @@ +#include "smack.h" +#include +#include + +// @expect error + +int main(void) { + int *p = (int *)malloc(sizeof(int)); + *p = 3; + int v = *p; + free(p); + assert(v != 3); + return 0; +} diff --git a/test/c/property-slicing/irrelevant_infinite_loop.c b/test/c/property-slicing/irrelevant_infinite_loop.c new file mode 100644 index 000000000..836c787ed --- /dev/null +++ b/test/c/property-slicing/irrelevant_infinite_loop.c @@ -0,0 +1,19 @@ +#include "smack.h" +#include + +// @expect verified +// A property-irrelevant loop that may never terminate. Bypassing it ADDS the +// execution that reaches the assertion, which is the sound direction for +// reachability: the assertion still holds, so the verdict is unchanged. This +// test exists to pin that over-approximation down, not to claim the loop +// terminates. + +int main(void) { + int scratch = 0; + int watched = 1; + while (__VERIFIER_nondet_int()) { + scratch++; + } + assert(watched == 1); + return 0; +} diff --git a/test/c/property-slicing/irrelevant_loop.c b/test/c/property-slicing/irrelevant_loop.c new file mode 100644 index 000000000..1a9b40b3d --- /dev/null +++ b/test/c/property-slicing/irrelevant_loop.c @@ -0,0 +1,19 @@ +#include "smack.h" +#include + +// @expect verified +// The loop needs 1000 iterations but writes only an object the property never +// observes. It must be bypassed rather than unrolled -- the default test +// --unroll=2 would otherwise miss nothing here, but the point is that the +// verdict is unchanged when the loop disappears. + +int main(void) { + int scratch[4]; + int i; + int watched = 1; + for (i = 0; i < 1000; i++) { + scratch[i % 4] = i; + } + assert(watched == 1); + return 0; +} diff --git a/test/c/property-slicing/irrelevant_unknown_bound_loop.c b/test/c/property-slicing/irrelevant_unknown_bound_loop.c new file mode 100644 index 000000000..3da8f27fe --- /dev/null +++ b/test/c/property-slicing/irrelevant_unknown_bound_loop.c @@ -0,0 +1,17 @@ +#include "smack.h" +#include + +// @expect verified +// Unknown trip count, no relevant effect. + +int main(void) { + int n = __VERIFIER_nondet_int(); + int scratch = 0; + int i; + int watched = 1; + for (i = 0; i < n; i++) { + scratch += i; + } + assert(watched == 1); + return 0; +} diff --git a/test/c/property-slicing/loop_calls_error_fail.c b/test/c/property-slicing/loop_calls_error_fail.c new file mode 100644 index 000000000..68e3c2056 --- /dev/null +++ b/test/c/property-slicing/loop_calls_error_fail.c @@ -0,0 +1,18 @@ +#include "smack.h" +#include +// @expect error +// @flag --unroll=6 + +void check(int i) { + if (i == 2) { + assert(0); + } +} + +int main(void) { + int i; + for (i = 0; i < 4; i++) { + check(i); + } + return 0; +} diff --git a/test/c/property-slicing/loop_contains_error_fail.c b/test/c/property-slicing/loop_contains_error_fail.c new file mode 100644 index 000000000..951410891 --- /dev/null +++ b/test/c/property-slicing/loop_contains_error_fail.c @@ -0,0 +1,14 @@ +#include "smack.h" +#include +// @expect error +// @flag --unroll=6 + +int main(void) { + int i; + for (i = 0; i < 4; i++) { + if (i == 2) { + assert(0); + } + } + return 0; +} diff --git a/test/c/property-slicing/loop_with_volatile_kept.c b/test/c/property-slicing/loop_with_volatile_kept.c new file mode 100644 index 000000000..7ffe95a50 --- /dev/null +++ b/test/c/property-slicing/loop_with_volatile_kept.c @@ -0,0 +1,17 @@ +#include "smack.h" +#include + +// @expect verified +// A volatile access is an effect the region abstraction does not model, so the +// loop must be retained regardless of relevance. + +int main(void) { + volatile int reg = 0; + int i; + int watched = 1; + for (i = 0; i < 4; i++) { + reg = i; + } + assert(watched == 1); + return 0; +} diff --git a/test/c/property-slicing/loop_writes_relevant_fail.c b/test/c/property-slicing/loop_writes_relevant_fail.c new file mode 100644 index 000000000..b7e7442bf --- /dev/null +++ b/test/c/property-slicing/loop_writes_relevant_fail.c @@ -0,0 +1,14 @@ +#include "smack.h" +#include +// @expect error +// @flag --unroll=6 + +int main(void) { + int x = 0; + int i; + for (i = 0; i < 4; i++) { + x += 1; + } + assert(x != 4); + return 0; +} diff --git a/test/c/property-slicing/nested_cond_fail.c b/test/c/property-slicing/nested_cond_fail.c new file mode 100644 index 000000000..9a8b5bbaf --- /dev/null +++ b/test/c/property-slicing/nested_cond_fail.c @@ -0,0 +1,17 @@ +#include "smack.h" +#include + +// @expect error +// Control dependence through nested conditions: the assertion has no data +// dependence on the predicates at all. + +int main(void) { + int a = __VERIFIER_nondet_int(); + int b = __VERIFIER_nondet_int(); + if (a > 0) { + if (b > 0) { + assert(0); + } + } + return 0; +} diff --git a/test/c/property-slicing/nested_loops_fail.c b/test/c/property-slicing/nested_loops_fail.c new file mode 100644 index 000000000..ab4a3a1df --- /dev/null +++ b/test/c/property-slicing/nested_loops_fail.c @@ -0,0 +1,16 @@ +#include "smack.h" +#include +// @expect error +// @flag --unroll=5 + +int main(void) { + int x = 0; + int i, j; + for (i = 0; i < 3; i++) { + for (j = 0; j < 3; j++) { + x++; + } + } + assert(x != 9); + return 0; +} diff --git a/test/c/property-slicing/phi_fail.c b/test/c/property-slicing/phi_fail.c new file mode 100644 index 000000000..92f4757ea --- /dev/null +++ b/test/c/property-slicing/phi_fail.c @@ -0,0 +1,16 @@ +#include "smack.h" +#include + +// @expect error +// A PHI feeding the assertion: every incoming value stays relevant. + +int main(void) { + int x; + if (__VERIFIER_nondet_int()) { + x = 1; + } else { + x = 2; + } + assert(x != 2); + return 0; +} diff --git a/test/c/property-slicing/recursive_fail.c b/test/c/property-slicing/recursive_fail.c new file mode 100644 index 000000000..38cdef2fc --- /dev/null +++ b/test/c/property-slicing/recursive_fail.c @@ -0,0 +1,16 @@ +#include "smack.h" +#include + +// @expect error +// @flag --unroll=4 + +int down(int n) { + if (n <= 0) + return 0; + return 1 + down(n - 1); +} + +int main(void) { + assert(down(2) != 2); + return 0; +} diff --git a/test/c/property-slicing/same_object_fail.c b/test/c/property-slicing/same_object_fail.c new file mode 100644 index 000000000..2846abfbd --- /dev/null +++ b/test/c/property-slicing/same_object_fail.c @@ -0,0 +1,15 @@ +#include "smack.h" +#include + +// @expect error +// The store and the load are on the same object: the store is region-relevant +// and must be retained, so the error is still reachable. + +int main(void) { + int x = 0; + int *p = &x; + int *q = &x; + *p = 1; + assert(*q == 0); + return 0; +} diff --git a/test/c/property-slicing/select_fail.c b/test/c/property-slicing/select_fail.c new file mode 100644 index 000000000..30aa19980 --- /dev/null +++ b/test/c/property-slicing/select_fail.c @@ -0,0 +1,11 @@ +#include "smack.h" +#include + +// @expect error + +int main(void) { + int c = __VERIFIER_nondet_int(); + int x = c ? 5 : 6; + assert(x != 6); + return 0; +} diff --git a/test/c/property-slicing/struct_field_fail.c b/test/c/property-slicing/struct_field_fail.c new file mode 100644 index 000000000..817081e80 --- /dev/null +++ b/test/c/property-slicing/struct_field_fail.c @@ -0,0 +1,18 @@ +#include "smack.h" +#include + +// @expect error + +struct S { + int a; + int b; +}; + +int main(void) { + struct S s; + s.a = 0; + s.b = 0; + s.b = 5; + assert(s.b != 5); + return 0; +} diff --git a/test/c/property-slicing/switch_fail.c b/test/c/property-slicing/switch_fail.c new file mode 100644 index 000000000..1900f00e1 --- /dev/null +++ b/test/c/property-slicing/switch_fail.c @@ -0,0 +1,18 @@ +#include "smack.h" +#include + +// @expect error + +int main(void) { + int a = __VERIFIER_nondet_int(); + switch (a) { + case 1: + break; + case 2: + assert(0); + break; + default: + break; + } + return 0; +} diff --git a/test/c/property-slicing/transitive_ssa_fail.c b/test/c/property-slicing/transitive_ssa_fail.c new file mode 100644 index 000000000..4e5673f5e --- /dev/null +++ b/test/c/property-slicing/transitive_ssa_fail.c @@ -0,0 +1,15 @@ +#include "smack.h" +#include + +// @expect error +// A chain of SSA definitions reaching the assertion must be retained. + +int main(void) { + int a = __VERIFIER_nondet_int(); + __VERIFIER_assume(a == 4); + int b = a + 1; + int c = b * 2; + int d = c - 3; + assert(d != 7); + return 0; +} diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp index 0151cb9b7..ad8a9d7bd 100644 --- a/tools/llvm2bpl/llvm2bpl.cpp +++ b/tools/llvm2bpl/llvm2bpl.cpp @@ -38,6 +38,7 @@ #include "smack/MemorySafetyChecker.h" #include "smack/Naming.h" #include "smack/NormalizeLoops.h" +#include "smack/PropertySlicing.h" #include "smack/RemoveDeadDefs.h" #include "smack/RewriteBitwiseOps.h" #include "smack/RustFixes.h" @@ -228,6 +229,14 @@ int main(int argc, char **argv) { pass_manager.add(new smack::IntegerOverflowChecker()); + // Property slicing runs here: after Devirtualize has resolved indirect + // calls and SplitAggregateValue has run, so the call graph and the memory + // operations are final; but before RewriteBitwiseOps, so that `and`/`or` + // are still plain instructions rather than calls to __SMACK_and32 &c., + // which the slicer would have to treat as opaque verifier calls. It is a + // no-op unless -property-slicing is given. + pass_manager.add(smack::createPropertySlicingPass()); + if (smack::SmackOptions::RewriteBitwiseOps && !(smack::SmackOptions::BitPrecise || smack::SmackOptions::BitPrecisePointers)) { From 81f9baba6aa1a7a1f0627396383917842cf69697 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 25 Aug 2026 18:33:56 -0700 Subject: [PATCH 02/11] Schedule property slicing only when it will run 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 --- include/smack/PropertySlicing.h | 8 ++++++++ lib/smack/PropertySlicing.cpp | 24 ++++++++++++++++++------ tools/llvm2bpl/llvm2bpl.cpp | 15 ++++++++++++--- 3 files changed, 38 insertions(+), 9 deletions(-) diff --git a/include/smack/PropertySlicing.h b/include/smack/PropertySlicing.h index 3cdb8499a..3fd1abed5 100644 --- a/include/smack/PropertySlicing.h +++ b/include/smack/PropertySlicing.h @@ -174,6 +174,14 @@ class PropertySlicing : public llvm::ModulePass { void emitProfile(llvm::Module &M); }; +/// Whether the pass would do anything for this invocation: the flag is on and +/// the property is one the relevance relation models. llvm2bpl consults this +/// to decide whether to *schedule* the pass at all -- requiring Regions and +/// DSAWrapper is not free of side effects on the pass pipeline, so a pass that +/// would immediately return must not be added. Warns once per run when the +/// flag is given but the property rules it out. +bool propertySlicingWillRun(); + llvm::ModulePass *createPropertySlicingPass(); } // namespace smack diff --git a/lib/smack/PropertySlicing.cpp b/lib/smack/PropertySlicing.cpp index fd92badd6..7aceb9e8e 100644 --- a/lib/smack/PropertySlicing.cpp +++ b/lib/smack/PropertySlicing.cpp @@ -19,6 +19,7 @@ #include "llvm/Support/FileSystem.h" #include "llvm/Support/raw_ostream.h" #include "llvm/Transforms/Utils/BasicBlockUtils.h" +#include #include #include @@ -1210,7 +1211,8 @@ void PropertySlicing::emitProfile(Module &M) { // ------------------------------------------------------------------- pass -bool PropertySlicing::runOnModule(Module &M) { +bool propertySlicingWillRun() { + static bool warned = false; if (!PropertySlicingEnabled) return false; @@ -1219,8 +1221,10 @@ bool PropertySlicing::runOnModule(Module &M) { // relevance rules above do not model, and termination is unsound by // construction under loop bypass. if (SmackOptions::MemorySafety || SmackOptions::IntegerOverflow) { - errs() << "SMACK warning: property slicing is only sound for assertion " - "reachability; disabling it for this property.\n"; + if (!warned) + errs() << "SMACK warning: property slicing is only sound for assertion " + "reachability; disabling it for this property.\n"; + warned = true; return false; } @@ -1232,11 +1236,19 @@ bool PropertySlicing::runOnModule(Module &M) { // Measured on test/c/unroll: nine tests flip from verified to a spurious // error, with and without loop bypass. if (SmackOptions::FailOnLoopExit) { - errs() << "SMACK warning: property slicing is incompatible with " - "-fail-on-loop-exit, whose property depends on the unroll " - "bound; disabling it.\n"; + if (!warned) + errs() << "SMACK warning: property slicing is incompatible with " + "-fail-on-loop-exit, whose property depends on the unroll " + "bound; disabling it.\n"; + warned = true; return false; } + return true; +} + +bool PropertySlicing::runOnModule(Module &M) { + if (!propertySlicingWillRun()) + return false; DL = &M.getDataLayout(); regions = &getAnalysis(); diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp index ad8a9d7bd..59f132757 100644 --- a/tools/llvm2bpl/llvm2bpl.cpp +++ b/tools/llvm2bpl/llvm2bpl.cpp @@ -233,9 +233,18 @@ int main(int argc, char **argv) { // calls and SplitAggregateValue has run, so the call graph and the memory // operations are final; but before RewriteBitwiseOps, so that `and`/`or` // are still plain instructions rather than calls to __SMACK_and32 &c., - // which the slicer would have to treat as opaque verifier calls. It is a - // no-op unless -property-slicing is given. - pass_manager.add(smack::createPropertySlicingPass()); + // which the slicer would have to treat as opaque verifier calls. + // + // The pass is *scheduled* only when it will actually run. It requires + // Regions and DSAWrapper, which transfers last-usership of DSAWrapper, + // seadsa::DsaAnalysis and CallGraph away from the passes that follow; + // scheduling it alongside MemorySafetyChecker crashes the legacy pass + // manager in PMTopLevelManager::setLastUser before any pass runs. Adding it + // conditionally also makes the refusals in propertySlicingWillRun() + // effective rather than dead code reached only after that crash. + if (smack::propertySlicingWillRun()) { + pass_manager.add(smack::createPropertySlicingPass()); + } if (smack::SmackOptions::RewriteBitwiseOps && !(smack::SmackOptions::BitPrecise || From 4dafabac1380fc492f6d6160074e39bf0b12f920 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 25 Aug 2026 18:34:02 -0700 Subject: [PATCH 03/11] Give each nondeterminized site its own value instead of undef 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 --- include/smack/PropertySlicing.h | 1 + lib/smack/PropertySlicing.cpp | 54 +++++++++++++++++++++++++++++---- 2 files changed, 49 insertions(+), 6 deletions(-) diff --git a/include/smack/PropertySlicing.h b/include/smack/PropertySlicing.h index 3fd1abed5..019f1541b 100644 --- a/include/smack/PropertySlicing.h +++ b/include/smack/PropertySlicing.h @@ -164,6 +164,7 @@ class PropertySlicing : public llvm::ModulePass { void snapshotRegions(llvm::Module &M); bool isOpaquePointer(const llvm::Value *Ptr) const; + llvm::Value *freshNondet(llvm::Type *T, llvm::Instruction *InsertBefore); unsigned destRegion(const llvm::Instruction &I) const; unsigned srcRegion(const llvm::Instruction &I) const; diff --git a/lib/smack/PropertySlicing.cpp b/lib/smack/PropertySlicing.cpp index 7aceb9e8e..5adcd59fa 100644 --- a/lib/smack/PropertySlicing.cpp +++ b/lib/smack/PropertySlicing.cpp @@ -819,12 +819,13 @@ bool PropertySlicing::removeIrrelevantInstructions(Function &F) { } }); auto *C = BI->getCondition(); - BI->setCondition(UndefValue::get(C->getType())); + BI->setCondition(freshNondet(C->getType(), BI)); changed = true; } } else if (auto *SI = dyn_cast(T)) { - if (!isa(SI->getCondition())) { - SI->setCondition(UndefValue::get(SI->getCondition()->getType())); + if (!isa(SI->getCondition()) && + !isa(SI->getCondition())) { + SI->setCondition(freshNondet(SI->getCondition()->getType(), SI)); changed = true; } } @@ -984,8 +985,14 @@ bool PropertySlicing::bypassIrrelevantLoops(Function &F) { } // Detach the irrelevant escaping values before the definitions go away. - for (auto *U : escapes) - U->set(UndefValue::get(U->get()->getType())); + // A PHI user keeps `undef`: its incoming block may itself be one of the + // loop blocks about to be deleted, so there is no insertion point that + // survives the rewrite. + for (auto *U : escapes) { + auto *UI = dyn_cast(U->getUser()); + U->set(freshNondet(U->get()->getType(), + (UI && !isa(UI)) ? UI : nullptr)); + } // Redirect the preheader past the loop. This can add the execution that // skips a nonterminating loop -- sound for reachability, and recorded as @@ -1006,7 +1013,7 @@ bool PropertySlicing::bypassIrrelevantLoops(Function &F) { // the "more behaviours" side. for (auto &PN : E->phis()) if (PN.getBasicBlockIndex(P) < 0) - PN.addIncoming(UndefValue::get(PN.getType()), P); + PN.addIncoming(freshNondet(PN.getType(), P->getTerminator()), P); S.loopsBypassed++; changed = true; @@ -1246,6 +1253,41 @@ bool propertySlicingWillRun() { return true; } +/// A *distinct* nondeterministic value for each site the slicer needs one. +/// +/// `undef` cannot be used here. `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` (SmackRep.cpp:813-816, +/// Naming.cpp:238/269). A Boogie constant is a single unconstrained but +/// *fixed* value, so every site sharing it is forced to agree -- on one +/// sliced driver a single `const $u0: i1` was the condition of 363 branches. +/// That *removes* execution combinations, the exact opposite of the +/// over-approximation the bypass and nondeterminization rules rely on, and is +/// unsound wherever the relevance relation is imprecise. +/// +/// A call to a body-less declaration is havoced by Boogie per call site, which +/// is the intended semantics. Pointer results keep `undef`: an external call +/// returning a pointer additionally gets `assume $isExternal(p)` +/// (SmackInstGenerator.cpp:811-815), which would *constrain* the value, and a +/// pointer is never a branch condition so it cannot correlate control flow. +Value *PropertySlicing::freshNondet(Type *T, Instruction *InsertBefore) { + if (T->isPointerTy() || !InsertBefore) + return UndefValue::get(T); + + std::string suffix; + raw_string_ostream OS(suffix); + T->print(OS); + OS.flush(); + for (auto &c : suffix) + if (!isalnum(static_cast(c))) + c = '_'; + + Module *M = InsertBefore->getModule(); + FunctionCallee C = + M->getOrInsertFunction("__SMACK_slice_nondet_" + suffix, T); + return CallInst::Create(C, "", InsertBefore); +} + bool PropertySlicing::runOnModule(Module &M) { if (!propertySlicingWillRun()) return false; From 59a1848a2d7ceefc1dfb16f8649aa3bafcd0e911 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 25 Aug 2026 19:09:47 -0700 Subject: [PATCH 04/11] Add a regression for nondeterminized-branch independence 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 --- .../nondet_branch_independence_fail.c | 37 +++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 test/c/property-slicing/nondet_branch_independence_fail.c diff --git a/test/c/property-slicing/nondet_branch_independence_fail.c b/test/c/property-slicing/nondet_branch_independence_fail.c new file mode 100644 index 000000000..bbec7fb8a --- /dev/null +++ b/test/c/property-slicing/nondet_branch_independence_fail.c @@ -0,0 +1,37 @@ +#include "smack.h" + +// @expect error + +// Two property-irrelevant loops whose header branches must take OPPOSITE truth +// values for control to reach the assertion: the first is left by falling out +// of its test, the second by taking its test. The slicer nondeterminizes both +// conditions. If the two sites share one value -- as they did when the +// replacement was an LLVM `undef`, which SMACK emits as a single module-global +// Boogie constant per type -- the assertion is unreachable and this real error +// is reported verified. +int main(void) { + int n = __VERIFIER_nondet_int(); + int m = __VERIFIER_nondet_int(); + int x = __VERIFIER_nondet_int(); + int c1 = __VERIFIER_nondet_int(); + int c2 = __VERIFIER_nondet_int(); + int i = 0, j = 0; + while (i < n) { /* stay while the test holds */ + if (c1) + i++; + else + goto A; + } +A: + while (1) { /* leave when the test holds */ + if (j >= m) + break; + if (c2) + goto B; + else + j++; + } +B: + __VERIFIER_assert(x != 5); + return 0; +} From 6faa2f5e95a72b2a2743024c288d99af3d280ca9 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 25 Aug 2026 18:55:17 -0700 Subject: [PATCH 05/11] Refuse property slicing for concurrent programs 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 " 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 --- lib/smack/PropertySlicing.cpp | 46 +++++++++++++++++++ share/smack/top.py | 7 +++ test/c/property-slicing/config.yml | 4 ++ test/c/property-slicing/pthread_spin_wait.c | 32 +++++++++++++ .../property-slicing/pthread_spin_wait_fail.c | 30 ++++++++++++ 5 files changed, 119 insertions(+) create mode 100644 test/c/property-slicing/pthread_spin_wait.c create mode 100644 test/c/property-slicing/pthread_spin_wait_fail.c diff --git a/lib/smack/PropertySlicing.cpp b/lib/smack/PropertySlicing.cpp index 5adcd59fa..f71cc3409 100644 --- a/lib/smack/PropertySlicing.cpp +++ b/lib/smack/PropertySlicing.cpp @@ -54,6 +54,16 @@ const llvm::cl::opt PropertySlicingNoRegions( llvm::cl::desc("Property slicing: ignore the region partition and treat " "all memory as one object (ablation experiment).")); +/// SMACK's concurrency mode -- share/smack/top.py passes this alongside +/// -property-slicing whenever the user gave --pthread. It describes the +/// *program* rather than this pass, so it belongs in SmackOptions next to +/// -memory-safety and -integer-overflow; it is declared here only because the +/// slicer is its single consumer (the refusal in propertySlicingWillRun()). +const llvm::cl::opt PropertySlicingPthread( + "property-slicing-pthread", + llvm::cl::desc("Property slicing: the translated program is concurrent " + "(SMACK's --pthread); slicing is refused for it.")); + const llvm::cl::opt PropertySlicingProfile( "property-slicing-profile", llvm::cl::desc("Write a machine-readable property-slicing profile here."), @@ -1250,6 +1260,42 @@ bool propertySlicingWillRun() { warned = true; return false; } + + // --pthread. Every relevance rule in this pass 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 is the + // wrong relation 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. + // - A loop whose exit test reads a location another thread writes carries + // no intra-thread control dependence -- the exit block post-dominates + // the header, so nothing after the loop is control-dependent on the + // test. bypassIrrelevantLoops therefore deletes the busy-wait, and + // -property-slicing-no-loop-bypass is not a remedy: the exit condition + // is nondeterminized instead, which lets the spin leave at any moment. + // + // Measured on test/c/pthread_extras with --pthread --context-bound=2: + // peterson, dekker and szymanski all go from verified to a spurious error, + // because both threads lose their `flag = 1` / `turn = ...` stores and their + // spin loops and walk straight into the critical section. + // + // Fixing this needs a may-happen-in-parallel notion the pass does not have + // (and cannot get cheaply: it would have to keep every store to a shared + // region as well as every loop testing one, which on these programs is + // everything). SMACK's concurrency model lives in string literals -- + // `__SMACK_code("async call ...")` in share/smack/lib/pthread.c -- so the + // slicer could not even see the thread edges to be conservative about. + if (PropertySlicingPthread) { + if (!warned) + errs() << "SMACK warning: property slicing models only sequential " + "dependence and would remove thread synchronisation; " + "disabling it for --pthread.\n"; + warned = true; + return false; + } + return true; } diff --git a/share/smack/top.py b/share/smack/top.py index 7b56e67ea..42ae3fcdf 100644 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -809,6 +809,13 @@ def llvm_to_bpl(args): cmd += ['-fail-on-loop-exit'] if args.property_slicing: cmd += ['-property-slicing'] + if args.pthread: + # Slicing is refused for concurrent programs: its relevance + # relation is a sequential one and would delete the stores and + # spin loops that implement synchronisation. llvm2bpl cannot see + # --pthread otherwise -- see propertySlicingWillRun() in + # lib/smack/PropertySlicing.cpp. + cmd += ['-property-slicing-pthread'] if args.property_slicing_no_loop_bypass: cmd += ['-property-slicing-no-loop-bypass'] if args.property_slicing_relax_asm: diff --git a/test/c/property-slicing/config.yml b/test/c/property-slicing/config.yml index b37ae6b4c..a96b36cca 100644 --- a/test/c/property-slicing/config.yml +++ b/test/c/property-slicing/config.yml @@ -1,3 +1,7 @@ skip: false verifiers: [corral] +# Pinned because pthread_spin_wait{,_fail}.c pass --pthread, and Corral rejects +# the prelude the other two memory models emit for a concurrent program +# ("Ensures has a shared global"). test/c/pthread pins it for the same reason. +memory: [no-reuse-impls] flags: [--property-slicing] diff --git a/test/c/property-slicing/pthread_spin_wait.c b/test/c/property-slicing/pthread_spin_wait.c new file mode 100644 index 000000000..aacf9453f --- /dev/null +++ b/test/c/property-slicing/pthread_spin_wait.c @@ -0,0 +1,32 @@ +#include "smack.h" +#include +#include + +// @expect verified +// @flag --pthread +// @flag --context-bound=2 + +// The slicer must refuse concurrent programs. `flag` is the release side of a +// handshake: the spin loop below carries no *intra-thread* dependence to the +// assertion -- its body is empty, and the block after it post-dominates the +// header, so nothing is control-dependent on the exit test -- yet it is the +// only thing that orders `x = 1` before `assert(x == 1)`. Slicing this program +// bypasses the loop and reports a spurious error. + +int flag = 0; +int x = 0; + +void *producer(void *arg) { + x = 1; + flag = 1; + return 0; +} + +int main(void) { + pthread_t t; + pthread_create(&t, 0, producer, 0); + while (flag == 0) { + } + assert(x == 1); + return 0; +} diff --git a/test/c/property-slicing/pthread_spin_wait_fail.c b/test/c/property-slicing/pthread_spin_wait_fail.c new file mode 100644 index 000000000..189f9e93c --- /dev/null +++ b/test/c/property-slicing/pthread_spin_wait_fail.c @@ -0,0 +1,30 @@ +#include "smack.h" +#include +#include + +// @expect error +// @flag --pthread +// @flag --context-bound=2 + +// The failing twin of pthread_spin_wait.c: the producer publishes `flag` +// before `x`, so waiting for the flag no longer establishes anything about x. +// It keeps the "verified" verdict of the twin honest -- the assertion is +// reachable and checked, not folded away. + +int flag = 0; +int x = 0; + +void *producer(void *arg) { + flag = 1; + x = 1; + return 0; +} + +int main(void) { + pthread_t t; + pthread_create(&t, 0, producer, 0); + while (flag == 0) { + } + assert(x == 1); + return 0; +} From 284d872c760abf154365830d7902f2b55bec1419 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 25 Aug 2026 18:56:24 -0700 Subject: [PATCH 06/11] Record the modes measured and found compatible with slicing 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 --- lib/smack/PropertySlicing.cpp | 53 +++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/lib/smack/PropertySlicing.cpp b/lib/smack/PropertySlicing.cpp index f71cc3409..435d17068 100644 --- a/lib/smack/PropertySlicing.cpp +++ b/lib/smack/PropertySlicing.cpp @@ -1296,6 +1296,59 @@ bool propertySlicingWillRun() { return false; } + // Nothing else SMACK's front end can be asked for needs a refusal. Each of + // the remaining modes was checked against the relevance relation and + // measured; the negative results are recorded here so a later reader does + // not repeat the search. + // + // -rust-panics The panic marker is a property root (isPropertyRoot), + // exactly as __VERIFIER_assert is, so a panicking path is + // error-reaching for the slicer too. test/rust/panic + // (four error tests, one verified) passes with slicing on. + // + // -llvm-assumes=use|check + // `llvm.assume` is inaccessiblememonly, so it is neither + // readnone nor onlyReadsMemory and computeEffects puts it + // in unsafeToDrop: the call is always kept, and with it + // the condition it names. This matters for `check`, where + // SmackInstGenerator turns the intrinsic into an *assert* + // (SmackInstGenerator.cpp:930) -- a property root the + // rules above do not name. Measured on a probe whose + // assumed value is irrelevant to the assertion: the + // violation is reported with slicing on and off alike. + // + // -float The relevance rules are type-agnostic; a floating-point + // value is relevant exactly where an integer one would + // be. Rounding-mode state reaches Boogie through + // __SMACK_code, which has a verification effect. + // + // -bit-precise, -bit-precise-pointers, -wrapped-integer-encoding + // Encoding choices made by SmackRep, downstream of the IR + // this pass rewrites. The one ordering constraint -- + // running before RewriteBitwiseOps, so that and/or are + // still instructions rather than __SMACK_and32 calls -- + // is already honoured by llvm2bpl.cpp. + // + // -modular Contract calls are verification effects, so requires, + // ensures and invariant survive together with everything + // they observe; a procedure carrying only a contract + // keeps its whole footprint. test/c/contracts passes with + // slicing on. + // + // -checked-functions, -entry-points + // Narrowing the checked set only removes Boogie asserts, + // while the slicer still roots at every + // __VERIFIER_assert; that is the conservative side. + // mayReachError is a whole-module fixpoint and never + // consults the entry points, so extra entries cost + // nothing. + // + // -no-memory-splitting + // Collapses Regions into fewer, larger regions, making + // regionIsRelevant coarser -- strictly more is kept. + // + // Measured with the 28 tests of test/c/property-slicing re-run under + // -bit-precise, -float and -llvm-assumes=check: 28/28 in every mode. return true; } From 1ee20344ddd824437e729386eb69ebd48e085010 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 25 Aug 2026 18:54:31 -0700 Subject: [PATCH 07/11] Reason about invoke as the call it is, not as an opaque effect 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, 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 --- include/smack/PropertySlicing.h | 4 +- lib/smack/PropertySlicing.cpp | 166 +++++++++++++----- test/c/property-slicing/invoke_call_result.ll | 58 ++++++ .../invoke_call_result_fail.ll | 45 +++++ .../property-slicing/invoke_reaches_error.ll | 40 +++++ .../invoke_reaches_error_fail.ll | 34 ++++ 6 files changed, 302 insertions(+), 45 deletions(-) create mode 100644 test/c/property-slicing/invoke_call_result.ll create mode 100644 test/c/property-slicing/invoke_call_result_fail.ll create mode 100644 test/c/property-slicing/invoke_reaches_error.ll create mode 100644 test/c/property-slicing/invoke_reaches_error_fail.ll diff --git a/include/smack/PropertySlicing.h b/include/smack/PropertySlicing.h index 019f1541b..c1f4d695a 100644 --- a/include/smack/PropertySlicing.h +++ b/include/smack/PropertySlicing.h @@ -137,8 +137,8 @@ class PropertySlicing : public llvm::ModulePass { std::unordered_set> exitReaching; - bool isPropertyRoot(const llvm::CallInst &CI) const; - bool hasVerificationEffect(const llvm::CallInst &CI) const; + bool isPropertyRoot(const llvm::CallBase &CB) const; + bool hasVerificationEffect(const llvm::CallBase &CB) const; bool hasUnmodelledEffect(const llvm::Instruction &I) const; void computeMayReachError(llvm::Module &M); diff --git a/lib/smack/PropertySlicing.cpp b/lib/smack/PropertySlicing.cpp index 435d17068..e585c5717 100644 --- a/lib/smack/PropertySlicing.cpp +++ b/lib/smack/PropertySlicing.cpp @@ -73,15 +73,45 @@ namespace { /// A helper that never lies about not knowing: any callee we cannot resolve to /// a single Function is treated as unknown. -const Function *calleeOf(const CallInst &CI) { - if (auto F = CI.getCalledFunction()) +/// +/// The parameter is `CallBase`, not `CallInst`, because an `invoke` is a call +/// too: it transfers control to a callee exactly as a `call` does, and SMACK +/// translates it with the very same `SmackRep::call` (SmackRep.cpp:1105-1128, +/// which discriminates the two only to count operands). A pass that reasoned +/// about `CallInst` alone would see no callee, no argument binding and no +/// call-graph edge at an invoke. +const Function *calleeOf(const CallBase &CB) { + if (auto F = CB.getCalledFunction()) return F; - if (auto V = CI.getCalledOperand()) + if (auto V = CB.getCalledOperand()) if (auto F = dyn_cast(V->stripPointerCastsAndAliases())) return F; return nullptr; } +/// An `invoke` (and a `callbr`) is a call that is also a TERMINATOR, so it is +/// retained unconditionally rather than being weighed like a `call`. +/// +/// Two ways to drop one were considered. Rewriting it into a `br` to its +/// normal destination is what "deleting" an invoke would have to mean, and it +/// costs a CFG edit plus a `removePredecessor` on the unwind destination's +/// PHIs, inside a rewriter that otherwise only ever erases instructions. +/// Keeping it costs one entry in `keep` and, through it, the invoke's +/// operands and the control dependences of its block. Keeping it was chosen +/// because it is the cheaper and far less error-prone of the two and buys +/// nothing to lose: `removeIrrelevantInstructions` already skips every +/// terminator, so no invoke was ever being deleted, and this predicate only +/// makes that explicit and closes the one path (loop bypass) that could still +/// take a terminator call away with the block it lives in. +/// +/// What the pass gains from `invoke` is not the right to delete it but the +/// *effects* it carries: the call-graph edge, the written regions, the +/// may-reach-error bit and the argument and return bindings, all of which the +/// rules below now read off it. +bool isTerminatorCall(const Instruction &I) { + return I.isTerminator() && isa(&I); +} + /// Control dependence, computed from the post-dominator tree by the standard /// edge-walk: for every CFG edge A->S where S does not post-dominate A, every /// node on the post-dominator path from S up to (but excluding) ipdom(A) is @@ -205,8 +235,8 @@ void PropertySlicing::getAnalysisUsage(AnalysisUsage &AU) const { /// in the pipeline is therefore purely a call to a specially-named function, /// and the set below is exactly the set of names that later become Boogie /// asserts or otherwise carry verification semantics. -bool PropertySlicing::isPropertyRoot(const CallInst &CI) const { - auto F = calleeOf(CI); +bool PropertySlicing::isPropertyRoot(const CallBase &CB) const { + auto F = calleeOf(CB); if (!F || !F->hasName()) return false; auto N = F->getName(); @@ -233,8 +263,8 @@ bool PropertySlicing::isPropertyRoot(const CallInst &CI) const { /// external-address assumption). Classifying them as verification effects made /// every function that draws a nondeterministic value un-droppable, and by /// transitivity poisoned nearly the whole call graph. -bool PropertySlicing::hasVerificationEffect(const CallInst &CI) const { - auto F = calleeOf(CI); +bool PropertySlicing::hasVerificationEffect(const CallBase &CB) const { + auto F = calleeOf(CB); if (!F || !F->hasName()) return false; auto N = F->getName(); @@ -289,8 +319,39 @@ bool PropertySlicing::hasUnmodelledEffect(const Instruction &I) const { // driver task for no soundness gain. if (isa(&I)) return true; - if (auto CI = dyn_cast(&I)) { - if (CI->isInlineAsm()) + // The exception *state* is the one channel outside the region abstraction: + // SMACK carries it in the Boogie global $exn (Naming::EXN_VAR), which no + // Region covers, and it admits as much for the clauses themselves + // ("TODO what exactly!?", SmackInstGenerator.cpp:872-880, which warns that + // approximating "landingpad clauses" "can lead to both false alarms and + // missed detections"). Raising, catching and cleaning up therefore stay + // unmodelled. isEHPad() is used rather than isa so the + // Windows funclet pads (catchswitch/catchpad/cleanuppad) are covered too: + // they used to be reached only by accident, through the blanket + // isa that this predicate no longer has. + if (I.isEHPad() || isa(&I) || isa(&I) || + isa(&I)) + return true; + // Checked before the CallBase rule below so that `callbr` keeps its + // unconditional treatment: it is a CallBase whose operand is virtually + // always inline asm (asm goto), and -property-slicing-relax-asm must not + // silently make an unmodelled control transfer disappear as well. + if (isa(&I) || isa(&I)) + return true; + // `invoke` deliberately is NOT unmodelled, though it used to be. It is the + // ordinary-call half of the exception pair -- visitInvokeInst emits exactly + // the SmackRep::call a CallInst gets, plus a goto on $exn -- so the region + // and call-graph rules describe it as well as they describe a call. + // + // Dropping the case does not weaken `unsafeToDrop` by itself: an invoke's + // unwind destination must begin with an EH pad *in the same function* + // (LangRef), so the rule above still marks every function that contains an + // invoke. That redundancy is exactly why the old blanket case was worth + // removing -- it hid the fact that the EH pad, not the invoke, is what + // actually holds the function, and it stopped every rule below from seeing + // the invoke's callee, arguments and result. + if (auto CB = dyn_cast(&I)) { + if (CB->isInlineAsm()) // SmackInstGenerator.cpp:641-646 already translates every inline asm to // Stmt::skip() -- a complete no-op -- and warns that this "can lead to // both false alarms and missed detections". Under -property-slicing- @@ -299,13 +360,12 @@ bool PropertySlicing::hasUnmodelledEffect(const Instruction &I) const { // prototype's baseline retains anything the region abstraction does not // capture. return !PropertySlicingRelaxAsm; - if (!calleeOf(*CI)) - return true; // unresolved indirect target + if (!calleeOf(*CB)) + // Unresolved indirect target. For an invoke this is also what SMACK + // itself refuses to translate (llvm_unreachable("Unexpected invoke + // instruction."), SmackInstGenerator.cpp:305-311). + return true; } - if (isa(&I) || isa(&I) || isa(&I)) - return true; - if (isa(&I) || isa(&I)) - return true; return false; } @@ -320,12 +380,15 @@ void PropertySlicing::computeMayReachError(Module &M) { continue; bool root = false; for (auto &I : instructions(F)) { - if (auto CI = dyn_cast(&I)) { - if (isPropertyRoot(*CI)) + // CallBase, not CallInst: an invoke is a call-graph edge like any + // other. Missing it meant a function whose only route to the property + // root ran through an invoke never joined mayReachError. + if (auto CB = dyn_cast(&I)) { + if (isPropertyRoot(*CB)) root = true; - if (auto G = calleeOf(*CI)) + if (auto G = calleeOf(*CB)) callers[G].push_back(&F); - else if (!CI->isInlineAsm()) + else if (!CB->isInlineAsm()) // An unresolved indirect call may reach anything. Inline asm cannot // reach a C function at all, and counting it here marked 33 extra // functions on he.ko as error-reaching. @@ -368,9 +431,9 @@ void PropertySlicing::computeEffects(Module &M) { if (hasUnmodelledEffect(I)) { if (unsafeToDrop.insert(&F).second) unsafeWhy[&F] = - isa(&I) && cast(&I)->isInlineAsm() + isa(&I) && cast(&I)->isInlineAsm() ? "inline_asm" - : (isa(&I) ? "indirect_call" : "atomic"); + : (isa(&I) ? "indirect_call" : "atomic"); } if (isa(&I) || isa(&I) || isa(&I) || isa(&I)) { @@ -381,12 +444,15 @@ void PropertySlicing::computeEffects(Module &M) { W.insert(r); } - if (auto CI = dyn_cast(&I)) { - if (hasVerificationEffect(*CI)) { + // CallBase again: without the invoke edge here a function's effect + // summary omitted everything its invoked callees write, so a store the + // property reads could be dropped at the call site of the *caller*. + if (auto CB = dyn_cast(&I)) { + if (hasVerificationEffect(*CB)) { if (unsafeToDrop.insert(&F).second) unsafeWhy[&F] = "verification_effect"; } - if (auto G = calleeOf(*CI)) + if (auto G = calleeOf(*CB)) callees[&F].push_back(G); } } @@ -523,8 +589,8 @@ std::string PropertySlicing::explainRelevance(const Instruction *I) const { if (!out.empty()) out += " -> "; out += cur->getOpcodeName(); - if (auto CI = dyn_cast(cur)) - if (auto G = calleeOf(*CI)) + if (auto CB = dyn_cast(cur)) + if (auto G = calleeOf(*CB)) out += "(" + G->getName().str() + ")"; if (cur != I && cur->getFunction() != I->getFunction()) out += "@" + cur->getFunction()->getName().str(); @@ -588,10 +654,11 @@ void PropertySlicing::seedRoots(Module &M) { continue; for (auto &I : instructions(F)) { bool isRoot = false; - if (auto CI = dyn_cast(&I)) - isRoot = isPropertyRoot(*CI) || hasVerificationEffect(*CI); - // Effects the abstraction cannot model are retained from the start. - if (isRoot || hasUnmodelledEffect(I)) + if (auto CB = dyn_cast(&I)) + isRoot = isPropertyRoot(*CB) || hasVerificationEffect(*CB); + // Effects the abstraction cannot model are retained from the start, and + // so is every call that is a terminator -- see isTerminatorCall. + if (isRoot || hasUnmodelledEffect(I) || isTerminatorCall(I)) keep.insert(&I); } } @@ -641,14 +708,14 @@ void PropertySlicing::propagate(Module &M) { // A write whose region is TOP may land on any relevant object. if (regionIsRelevant(destRegion(I))) kept = true; - } else if (auto CI = dyn_cast(&I)) { - auto G = calleeOf(*CI); + } else if (auto CB = dyn_cast(&I)) { + auto G = calleeOf(*CB); if (!G) // No resolvable callee: an indirect target could do anything. // Inline asm is the one exception under // -property-slicing-relax-asm, where we adopt SMACK's own // Stmt::skip() semantics for it. - kept = !(CI->isInlineAsm() && PropertySlicingRelaxAsm); + kept = !(CB->isInlineAsm() && PropertySlicingRelaxAsm); else if (mayReachError.count(G) || unsafeToDrop.count(G) || writesTop.count(G)) kept = true; @@ -677,14 +744,14 @@ void PropertySlicing::propagate(Module &M) { // body keep the wholesale rule, since nothing can be established about // them. markSource = &I; - auto CIforArgs = dyn_cast(&I); - const Function *Gee = CIforArgs ? calleeOf(*CIforArgs) : nullptr; - if (CIforArgs && Gee && !Gee->isDeclaration() && !Gee->isVarArg() && - Gee->arg_size() == CIforArgs->arg_size()) { + auto CBforArgs = dyn_cast(&I); + const Function *Gee = CBforArgs ? calleeOf(*CBforArgs) : nullptr; + if (CBforArgs && Gee && !Gee->isDeclaration() && !Gee->isVarArg() && + Gee->arg_size() == CBforArgs->arg_size()) { unsigned k = 0; for (auto &A : Gee->args()) { if (relevant.count(&A)) - markValue(CIforArgs->getArgOperand(k), changed); + markValue(CBforArgs->getArgOperand(k), changed); ++k; } } else { @@ -718,9 +785,11 @@ void PropertySlicing::propagate(Module &M) { } // A relevant call result makes the callee's returned values relevant. - if (auto CI = dyn_cast(&I)) { - if (relevant.count(CI)) { - if (auto G = calleeOf(*CI)) + // An invoke defines its result on the normal edge, so the rule is the + // same one. + if (auto CB = dyn_cast(&I)) { + if (relevant.count(CB)) { + if (auto G = calleeOf(*CB)) if (!G->isDeclaration()) for (auto &BB : *G) if (auto RI = dyn_cast(BB.getTerminator())) @@ -799,6 +868,9 @@ bool PropertySlicing::removeIrrelevantInstructions(Function &F) { else if (isa(I)) S.storesRemoved++; else if (isa(I)) + // CallInst and not CallBase on purpose: `dead` is built from + // non-terminators only, so an invoke can never reach this loop, and + // counting it would be dead code that suggested otherwise. S.callsRemoved++; I->eraseFromParent(); changed = true; @@ -833,6 +905,11 @@ bool PropertySlicing::removeIrrelevantInstructions(Function &F) { changed = true; } } else if (auto *SI = dyn_cast(T)) { + // The CallInst guard recognises a condition this pass has already + // replaced -- freshNondet emits a CallInst -- and stays CallInst-only. + // Widening it to CallBase would only skip switches fed by an invoke + // result, and *not* nondeterminizing a condition just leaves the + // original program semantics in place, which is always sound. if (!isa(SI->getCondition()) && !isa(SI->getCondition())) { SI->setCondition(freshNondet(SI->getCondition()->getType(), SI)); @@ -880,8 +957,8 @@ bool PropertySlicing::bypassIrrelevantLoops(Function &F) { // by the first instruction encountered in block order -- that is // nearly always the induction PHI, which says nothing. const Instruction *T = relevanceTerminus(&I); - if (auto CI = dyn_cast(T ? T : &I)) { - auto G = calleeOf(*CI); + if (auto CB = dyn_cast(T ? T : &I)) { + auto G = calleeOf(*CB); if (!G) reason = LoopReason::UNKNOWN_CALL; else if (mayReachError.count(G)) @@ -1078,6 +1155,9 @@ bool PropertySlicing::rewrite(Module &M) { else if (isa(&I)) S.storesRetained++; else if (isa(&I)) + // Paired with callsRemoved above, which counts CallInst only; an + // invoke is never a candidate for removal, so leaving it out of both + // keeps `before == retained + removed` over the same population. S.callsRetained++; } } diff --git a/test/c/property-slicing/invoke_call_result.ll b/test/c/property-slicing/invoke_call_result.ll new file mode 100644 index 000000000..c77ca4ab5 --- /dev/null +++ b/test/c/property-slicing/invoke_call_result.ll @@ -0,0 +1,58 @@ +; @expect verified +; +; An `invoke` whose RESULT the assertion consumes. Hand-written LLVM IR +; because SMACK's C front end never emits an invoke: default_clang_compile_command +; (share/smack/frontend.py:88-121) passes no -fexceptions, so clang marks every +; C function nounwind and lowers every call as a `call`. C++ is the natural +; source of invokes, and test/cplusplus is skipped in this tree. +; +; The property-slicing rule under test is "a relevant call result makes the +; callee's returned values relevant". Written over CallInst alone it does not +; fire here, and then nothing marks @get's load as relevant, the region behind +; @g is never relevant, and the store inside @set -- together with the whole +; `call @set` and the static initialiser of @g -- is sliced away. $M.0 is then +; unconstrained and this verified program reports a spurious error. + +source_filename = "llvm-link" +target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128" +target triple = "x86_64-unknown-linux-gnu" + +; A non-zero initialiser: SMACK emits __SMACK_static_init only for those, and +; the test needs @g's starting value to be pinned rather than unconstrained. +@g = internal global i32 7 + +declare void @__VERIFIER_assert(i32) +declare i32 @__VERIFIER_nondet_int() +declare i32 @__gxx_personality_v0(...) + +define internal void @set(i32 %x) { + store i32 %x, i32* @g + ret void +} + +define internal i32 @get() { + %v = load i32, i32* @g + ret i32 %v +} + +define i32 @main() personality i32 (...)* @__gxx_personality_v0 { +entry: + %n0 = call i32 @__VERIFIER_nondet_int() + %is7 = icmp eq i32 %n0, 7 + ; n is nondeterministic but never 7, so reading @g's initial value instead + ; of what @set wrote is observable. + %n = select i1 %is7, i32 8, i32 %n0 + call void @set(i32 %n) + %r = invoke i32 @get() + to label %cont unwind label %lpad + +cont: + %eq = icmp eq i32 %r, %n + %z = zext i1 %eq to i32 + call void @__VERIFIER_assert(i32 %z) + ret i32 0 + +lpad: + %ex = landingpad { i8*, i32 } cleanup + resume { i8*, i32 } %ex +} diff --git a/test/c/property-slicing/invoke_call_result_fail.ll b/test/c/property-slicing/invoke_call_result_fail.ll new file mode 100644 index 000000000..a999d6b80 --- /dev/null +++ b/test/c/property-slicing/invoke_call_result_fail.ll @@ -0,0 +1,45 @@ +; @expect error +; +; The failing twin of invoke_call_result.ll: the assertion claims @get returns +; something OTHER than what @set stored, which is false, so the slice must +; still report the error. + +source_filename = "llvm-link" +target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128" +target triple = "x86_64-unknown-linux-gnu" + +@g = internal global i32 7 + +declare void @__VERIFIER_assert(i32) +declare i32 @__VERIFIER_nondet_int() +declare i32 @__gxx_personality_v0(...) + +define internal void @set(i32 %x) { + store i32 %x, i32* @g + ret void +} + +define internal i32 @get() { + %v = load i32, i32* @g + ret i32 %v +} + +define i32 @main() personality i32 (...)* @__gxx_personality_v0 { +entry: + %n0 = call i32 @__VERIFIER_nondet_int() + %is7 = icmp eq i32 %n0, 7 + %n = select i1 %is7, i32 8, i32 %n0 + call void @set(i32 %n) + %r = invoke i32 @get() + to label %cont unwind label %lpad + +cont: + %ne = icmp ne i32 %r, %n + %z = zext i1 %ne to i32 + call void @__VERIFIER_assert(i32 %z) + ret i32 0 + +lpad: + %ex = landingpad { i8*, i32 } cleanup + resume { i8*, i32 } %ex +} diff --git a/test/c/property-slicing/invoke_reaches_error.ll b/test/c/property-slicing/invoke_reaches_error.ll new file mode 100644 index 000000000..48565180e --- /dev/null +++ b/test/c/property-slicing/invoke_reaches_error.ll @@ -0,0 +1,40 @@ +; @expect verified +; +; The property root reached THROUGH an invoke: @main invokes @check, and it is +; @check that calls __VERIFIER_assert. This is the shape that computeMayReachError +; and the per-argument rule of `propagate` have to see -- both of which used to +; be written over CallInst and so recorded no call-graph edge and no argument +; binding at an invoke at all. + +source_filename = "llvm-link" +target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128" +target triple = "x86_64-unknown-linux-gnu" + +declare void @__VERIFIER_assert(i32) +declare i32 @__VERIFIER_nondet_int() +declare i32 @__gxx_personality_v0(...) + +define internal void @check(i32 %x) { + %nz = icmp ne i32 %x, 0 + %z = zext i1 %nz to i32 + call void @__VERIFIER_assert(i32 %z) + ret void +} + +define i32 @main() personality i32 (...)* @__gxx_personality_v0 { +entry: + %n0 = call i32 @__VERIFIER_nondet_int() + %is0 = icmp eq i32 %n0, 0 + ; nondeterministic, but never 0 -- so the assertion holds without being + ; vacuous. + %n = select i1 %is0, i32 1, i32 %n0 + invoke void @check(i32 %n) + to label %cont unwind label %lpad + +cont: + ret i32 0 + +lpad: + %ex = landingpad { i8*, i32 } cleanup + resume { i8*, i32 } %ex +} diff --git a/test/c/property-slicing/invoke_reaches_error_fail.ll b/test/c/property-slicing/invoke_reaches_error_fail.ll new file mode 100644 index 000000000..5b975f9b3 --- /dev/null +++ b/test/c/property-slicing/invoke_reaches_error_fail.ll @@ -0,0 +1,34 @@ +; @expect error +; +; The failing twin of invoke_reaches_error.ll: the nondeterministic value is +; passed to @check unguarded, so the assertion inside the invoked callee is +; reachable and the slice must keep the whole chain. + +source_filename = "llvm-link" +target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128" +target triple = "x86_64-unknown-linux-gnu" + +declare void @__VERIFIER_assert(i32) +declare i32 @__VERIFIER_nondet_int() +declare i32 @__gxx_personality_v0(...) + +define internal void @check(i32 %x) { + %nz = icmp ne i32 %x, 0 + %z = zext i1 %nz to i32 + call void @__VERIFIER_assert(i32 %z) + ret void +} + +define i32 @main() personality i32 (...)* @__gxx_personality_v0 { +entry: + %n = call i32 @__VERIFIER_nondet_int() + invoke void @check(i32 %n) + to label %cont unwind label %lpad + +cont: + ret i32 0 + +lpad: + %ex = landingpad { i8*, i32 } cleanup + resume { i8*, i32 } %ex +} From 1d0dc7b5c950df5b57fd723c3dbe38acc704f3bd Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 25 Aug 2026 18:55:08 -0700 Subject: [PATCH 08/11] Keep a loop bypass from deleting a terminator call with the loop 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 --- lib/smack/PropertySlicing.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/lib/smack/PropertySlicing.cpp b/lib/smack/PropertySlicing.cpp index e585c5717..69bf0d13d 100644 --- a/lib/smack/PropertySlicing.cpp +++ b/lib/smack/PropertySlicing.cpp @@ -945,7 +945,13 @@ bool PropertySlicing::bypassIrrelevantLoops(Function &F) { for (auto *BB : L->blocks()) { for (auto &I : *BB) { - if (I.isTerminator()) + // Terminators are examined below, as the *block's* terminator -- with + // one exception: a terminator that is also a call. That check exempts + // the loop latch (a latch's back-edge branch is exactly what a bypass + // is entitled to delete), and an invoke can perfectly well terminate a + // latch, which would let the bypass delete the whole loop body around + // a call site that isTerminatorCall promises to retain. + if (I.isTerminator() && !isTerminatorCall(I)) continue; if (hasUnmodelledEffect(I)) { reason = LoopReason::VOLATILE_ATOMIC; From 1a3a7f1988a0218f690ab3ab4b14dc8738544e73 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 25 Aug 2026 18:59:07 -0700 Subject: [PATCH 09/11] Make the slice non-termination-sensitive about loops 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 --- include/smack/PropertySlicing.h | 24 +++- lib/smack/PropertySlicing.cpp | 117 +++++++++++++++++- .../property-slicing/ps_nonterm_error_loop.c | 25 ++++ .../ps_nonterm_error_loop_fail.c | 20 +++ 4 files changed, 178 insertions(+), 8 deletions(-) create mode 100644 test/c/property-slicing/ps_nonterm_error_loop.c create mode 100644 test/c/property-slicing/ps_nonterm_error_loop_fail.c diff --git a/include/smack/PropertySlicing.h b/include/smack/PropertySlicing.h index c1f4d695a..b2cd6cfd1 100644 --- a/include/smack/PropertySlicing.h +++ b/include/smack/PropertySlicing.h @@ -35,11 +35,17 @@ class DSAWrapper; /// Errors(original) is a subset of Errors(sliced) /// /// i.e. the slice may add executions but must never delete a concrete -/// error-reaching one. Bypassing a property-irrelevant loop can add the -/// execution that skips a nontermination; for reachability that is the safe -/// direction. It would NOT be safe for termination, and it is not sound for -/// memory-safety or overflow properties, whose roots this pass does not model -/// -- the pass therefore refuses to run for anything but assertion checking. +/// error-reaching one. It is not sound for memory-safety or overflow +/// properties, whose roots this pass does not model -- the pass therefore +/// refuses to run for anything but assertion checking. +/// +/// ADDED EXECUTIONS ARE NOT FREE. An execution the original does not have +/// cannot hide a bug, but it can report one that is not there, and the slice +/// is worthless if it does. The rule that keeps that in check is +/// non-termination sensitivity: a loop the original program may never leave is +/// never skipped, and the branches that decide to leave such a loop are always +/// retained, because everything after the loop happens only because the loop +/// was left. class PropertySlicing : public llvm::ModulePass { public: /// Why a loop was retained; reported by the profile. @@ -55,6 +61,7 @@ class PropertySlicing : public llvm::ModulePass { NO_PREHEADER, MULTIPLE_EXITS, NO_EXIT, + MAY_NOT_TERMINATE, OTHER_CONSERVATIVE, BYPASSED, }; @@ -132,6 +139,13 @@ class PropertySlicing : public llvm::ModulePass { std::vector>> CD; + /// Headers of the loops ScalarEvolution can bound. A loop that is not in + /// this set may spin forever as far as the slice knows, so it is never + /// bypassed and everything its exit reaches is control-dependent on leaving + /// it. Keyed by header block: the answer is computed once, before any + /// rewriting, and read back through a second LoopInfo instance. + std::unordered_set terminatingLoops; + /// Per-function set of blocks from which a function exit is reachable. std::unordered_map> diff --git a/lib/smack/PropertySlicing.cpp b/lib/smack/PropertySlicing.cpp index 69bf0d13d..a3790af33 100644 --- a/lib/smack/PropertySlicing.cpp +++ b/lib/smack/PropertySlicing.cpp @@ -12,6 +12,7 @@ #include "llvm/ADT/DepthFirstIterator.h" #include "llvm/Analysis/LoopInfo.h" #include "llvm/Analysis/PostDominators.h" +#include "llvm/Analysis/ScalarEvolution.h" #include "llvm/IR/CFG.h" #include "llvm/IR/Constants.h" #include "llvm/IR/InstIterator.h" @@ -171,6 +172,71 @@ void computeControlDependence( } } +/// Whether the analysis can prove the loop is left. ScalarEvolution returning +/// anything but SCEVCouldNotCompute for the backedge-taken count is a bound on +/// the number of times the backedge runs, so every execution reaches an exit; +/// everything else -- including every loop whose exit test the analysis does +/// not understand -- is treated as possibly spinning forever. (LLVM's answer +/// rests on C's forward-progress rule for loops with a non-constant condition, +/// which is the same assumption clang itself compiles under; a loop with a +/// constant condition, the `while (1)` idiom this matters for, gets no such +/// benefit.) +bool mustTerminate(const Loop *L, ScalarEvolution &SE) { + return !isa(SE.getSymbolicMaxBackedgeTakenCount(L)); +} + +/// Non-termination-SENSITIVE control dependence, for the loops the analysis +/// cannot prove terminate: whatever such a loop's exit can reach executes only +/// because the loop was left, so it is control-dependent on the branches that +/// leave it. +/// +/// The post-dominator relation cannot express this. `PostDominatorTree` treats +/// every loop as if it always terminated, so in +/// +/// while (1) { if (bad) { __VERIFIER_assert(0); return; } step(); } +/// +/// the assertion's block post-dominates the branch that decides to enter it -- +/// it is the function's only exit -- and comes out control-dependent on +/// nothing at all. `bad` is then irrelevant, the branch is nondeterminized, +/// the loop holds no kept instruction and is bypassed, and control lands on +/// the assertion unconditionally: a program that never reaches the assertion +/// reports a bug. Adding these edges keeps the guard, and with it the loop. +void addLoopExitDependence( + LoopInfo &LI, const std::unordered_set &Terminating, + std::unordered_map> + &CD) { + std::vector work(LI.begin(), LI.end()); + while (!work.empty()) { + Loop *L = work.back(); + work.pop_back(); + for (Loop *Sub : *L) + work.push_back(Sub); + if (Terminating.count(L->getHeader())) + continue; + + SmallVector exiting; + L->getExitingBlocks(exiting); + SmallVector exits; + L->getExitBlocks(exits); + if (exiting.empty() || exits.empty()) + continue; // never left at all: nothing downstream depends on leaving it + + std::unordered_set reached; + std::vector stack(exits.begin(), exits.end()); + while (!stack.empty()) { + auto *B = stack.back(); + stack.pop_back(); + if (!reached.insert(B).second) + continue; + for (auto *S : successors(B)) + stack.push_back(S); + } + for (auto *B : reached) + for (auto *X : exiting) + CD[B].push_back(X); + } +} + double secondsSince(std::chrono::steady_clock::time_point T0) { return std::chrono::duration(std::chrono::steady_clock::now() - T0) .count(); @@ -202,6 +268,8 @@ const char *PropertySlicing::reasonName(LoopReason R) { return "MULTIPLE_EXITS"; case LoopReason::NO_EXIT: return "NO_EXIT"; + case LoopReason::MAY_NOT_TERMINATE: + return "MAY_NOT_TERMINATE"; case LoopReason::OTHER_CONSERVATIVE: return "OTHER_CONSERVATIVE"; case LoopReason::BYPASSED: @@ -224,6 +292,9 @@ void PropertySlicing::getAnalysisUsage(AnalysisUsage &AU) const { AU.addPreserved(); AU.addRequired(); AU.addRequired(); + // Only ever asked whether a loop's backedge count is bounded, which decides + // whether the slice is allowed to skip the loop -- see mustTerminate. + AU.addRequired(); } // ------------------------------------------------------------- predicates @@ -673,6 +744,24 @@ void PropertySlicing::propagate(Module &M) { auto &ER = exitReaching[&F]; collectExitReaching(F, ER); computeControlDependence(F, PDT, ER, CD[&F]); + // Which loops the slice is allowed to treat as terminating. Recorded by + // header block rather than by Loop*, because rewrite() asks again from a + // second LoopInfo instance. Both queries happen before any CFG edit: the + // answers describe the module the slice was computed on. + { + auto &LI = getAnalysis(F).getLoopInfo(); + auto &SE = getAnalysis(F).getSE(); + std::vector work(LI.begin(), LI.end()); + while (!work.empty()) { + Loop *L = work.back(); + work.pop_back(); + for (Loop *Sub : *L) + work.push_back(Sub); + if (mustTerminate(L, SE)) + terminatingLoops.insert(L->getHeader()); + } + addLoopExitDependence(LI, terminatingLoops, CD[&F]); + } // Where post-dominance is undefined, retain every branch outright. for (auto &BB : F) if (!ER.count(&BB)) { @@ -1016,6 +1105,28 @@ bool PropertySlicing::bypassIrrelevantLoops(Function &F) { droppable = false; } + // Non-termination sensitivity, the one rule that governs this decision: + // ONLY A LOOP THE ANALYSIS CAN PROVE TERMINATES MAY BE SKIPPED. Redirecting + // the preheader past a loop replaces "the loop runs and is left" with + // "the loop is not there", which for a loop the program may never leave + // hands the slice an execution that continues past a point the original + // never passes -- straight into whatever follows, up to and including the + // property root. That is how + // while (1) { if (bad) { __VERIFIER_assert(0); return; } step(); } + // turns into a false alarm. When the backedge count is bounded the bypass + // adds nothing: the original leaves the loop too, and by the tests above + // nothing it computes on the way is relevant. + // + // This subsumes, and is cheaper than, asking whether the property root is + // reachable from the loop -- and unlike that question it also covers the + // interprocedural case, where the loop's own function has no root in it + // but returns into a caller that does. + if (droppable && !terminatingLoops.count(L->getHeader())) { + reason = LoopReason::MAY_NOT_TERMINATE; + droppable = false; + blocker = "backedge count not bounded by ScalarEvolution"; + } + // A value defined in the loop and used outside it loses its definition // when the loop goes. If any such external user is itself relevant, the // loop's result matters after all and the loop stays. Otherwise the escape @@ -1087,9 +1198,9 @@ bool PropertySlicing::bypassIrrelevantLoops(Function &F) { (UI && !isa(UI)) ? UI : nullptr)); } - // Redirect the preheader past the loop. This can add the execution that - // skips a nonterminating loop -- sound for reachability, and recorded as - // an over-approximation. + // Redirect the preheader past the loop. Only loops with a bounded backedge + // count get here, so the original leaves this loop on every execution and + // the redirect adds no path the original does not already have. auto *T = P->getTerminator(); bool redirected = false; for (unsigned i = 0; i < T->getNumSuccessors(); ++i) diff --git a/test/c/property-slicing/ps_nonterm_error_loop.c b/test/c/property-slicing/ps_nonterm_error_loop.c new file mode 100644 index 000000000..0d489ded4 --- /dev/null +++ b/test/c/property-slicing/ps_nonterm_error_loop.c @@ -0,0 +1,25 @@ +#include "smack.h" +#include + +// @expect verified +// The error block sits OUTSIDE the loop but is reachable only through it, and +// it is the function's only exit -- so it post-dominates the branch that +// decides to enter it, and non-termination-insensitive control dependence +// makes that branch, and with it `bad`, look irrelevant. The loop then holds +// nothing kept and is bypassed onto its unique exit block, which is the error. +// The original never leaves the loop (`bad` is assumed zero), so a report here +// is a false alarm. + +int main(void) { + int bad = __VERIFIER_nondet_int(); + int scratch = 0; + __VERIFIER_assume(bad == 0); + while (1) { + if (bad) { + assert(0); + return 0; + } + scratch++; + } + return 0; +} diff --git a/test/c/property-slicing/ps_nonterm_error_loop_fail.c b/test/c/property-slicing/ps_nonterm_error_loop_fail.c new file mode 100644 index 000000000..3de9851a1 --- /dev/null +++ b/test/c/property-slicing/ps_nonterm_error_loop_fail.c @@ -0,0 +1,20 @@ +#include "smack.h" +#include + +// @expect error +// The twin of ps_nonterm_error_loop.c with the assumption dropped: the loop is +// now left whenever `bad` holds, and the error is real. Keeping the guard must +// not cost the error. + +int main(void) { + int bad = __VERIFIER_nondet_int(); + int scratch = 0; + while (1) { + if (bad) { + assert(0); + return 0; + } + scratch++; + } + return 0; +} From a1b2f78c2b533cf3771e67d8bdb7117507c8a171 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 25 Aug 2026 18:59:59 -0700 Subject: [PATCH 10/11] Never drop a call to a function that may not return 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 --- lib/smack/PropertySlicing.cpp | 38 +++++++++++++++++++ test/c/property-slicing/ps_noreturn_call.c | 23 +++++++++++ .../property-slicing/ps_noreturn_call_fail.c | 20 ++++++++++ 3 files changed, 81 insertions(+) create mode 100644 test/c/property-slicing/ps_noreturn_call.c create mode 100644 test/c/property-slicing/ps_noreturn_call_fail.c diff --git a/lib/smack/PropertySlicing.cpp b/lib/smack/PropertySlicing.cpp index a3790af33..1b6331a5e 100644 --- a/lib/smack/PropertySlicing.cpp +++ b/lib/smack/PropertySlicing.cpp @@ -146,6 +146,34 @@ void collectExitReaching(Function &F, } } +/// Whether control can ever come back from a call to this function: is any +/// `ret` reachable from its entry block? +/// +/// The attribute is not the test. The LDV drivers' `void ldv_stop(void) { L: +/// goto L; }` -- and `void hang(void) { while (1) {} }` generally -- is an +/// ordinary function that clang marks with nothing at all; only its shape says +/// it never gives control back. The attribute is still honoured, for the +/// body-less declarations (`exit`, `abort`) where shape says nothing. +bool neverReturns(const Function &F) { + if (F.hasFnAttribute(Attribute::NoReturn)) + return true; + if (F.isDeclaration()) + return false; // no body to look at; unsafeToDrop already covers these + std::unordered_set seen; + std::vector work{&F.getEntryBlock()}; + while (!work.empty()) { + auto *B = work.back(); + work.pop_back(); + if (!seen.insert(B).second) + continue; + if (isa(B->getTerminator())) + return false; + for (auto *S : successors(B)) + work.push_back(S); + } + return true; +} + void computeControlDependence( Function &F, PostDominatorTree &PDT, const std::unordered_set &ExitReaching, @@ -491,6 +519,16 @@ void PropertySlicing::computeEffects(Module &M) { std::unordered_map> callees; for (auto &F : M) { + // A call that never comes back may not be elided: the slice would carry on + // past a point the original execution never leaves, and everything after + // it -- assertions included -- becomes reachable that was not. This is + // "unsafe to drop" in exactly the sense the fixpoint below already + // propagates: a function that calls a function that never returns may + // itself never return. + if (neverReturns(F)) { + if (unsafeToDrop.insert(&F).second) + unsafeWhy[&F] = "may_not_return"; + } if (F.isDeclaration()) { // No body: unknown effects unless LLVM itself proves otherwise. if (!F.doesNotAccessMemory() && !F.onlyReadsMemory()) diff --git a/test/c/property-slicing/ps_noreturn_call.c b/test/c/property-slicing/ps_noreturn_call.c new file mode 100644 index 000000000..80b334931 --- /dev/null +++ b/test/c/property-slicing/ps_noreturn_call.c @@ -0,0 +1,23 @@ +#include "smack.h" +#include + +// @expect verified +// The LDV `ldv_stop` idiom: an ordinary function -- no noreturn attribute -- +// that never returns. It reaches no property root, has no unmodelled effect +// and writes no region, so every rule about dropping a call is satisfied; but +// dropping it lets the slice continue past a point the original never leaves, +// and the assertion below then fails for `guard == 0`. + +void ldv_stop(void) { + while (1) { + } +} + +int main(void) { + int guard = __VERIFIER_nondet_int(); + if (!guard) { + ldv_stop(); + } + assert(guard != 0); + return 0; +} diff --git a/test/c/property-slicing/ps_noreturn_call_fail.c b/test/c/property-slicing/ps_noreturn_call_fail.c new file mode 100644 index 000000000..bacbeb48c --- /dev/null +++ b/test/c/property-slicing/ps_noreturn_call_fail.c @@ -0,0 +1,20 @@ +#include "smack.h" +#include + +// @expect error +// The twin of ps_noreturn_call.c: control that gets past ldv_stop really can +// violate the assertion, so retaining the call must not hide the error. + +void ldv_stop(void) { + while (1) { + } +} + +int main(void) { + int guard = __VERIFIER_nondet_int(); + if (!guard) { + ldv_stop(); + } + assert(guard != 1); + return 0; +} From fd4d3f5f1608d861a721ebea8973bfe8653c2a5e Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 25 Aug 2026 20:45:14 -0700 Subject: [PATCH 11/11] Run the property-slicing regressions in CI 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) --- .github/workflows/smack-ci.yaml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/smack-ci.yaml b/.github/workflows/smack-ci.yaml index dc5722dc2..ee0cdc4bb 100644 --- a/.github/workflows/smack-ci.yaml +++ b/.github/workflows/smack-ci.yaml @@ -25,6 +25,8 @@ jobs: "--exhaustive --folder=c/special", "--exhaustive --folder=c/targeted-checks", "--exhaustive --folder=c/unroll", + "--exhaustive --folder=c/property-slicing", + "--exhaustive --folder=c/property-slicing --languages=llvm-ir", "--exhaustive --folder=rust/array --languages=rust", "--exhaustive --folder=rust/basic --languages=rust", "--exhaustive --folder=rust/box --languages=rust",