From 6f58d20a4a6576c24e1e8e47bab825cec9951528 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Mon, 6 Jul 2026 00:31:58 -0700 Subject: [PATCH 1/2] Assume checked arithmetic overflow does not occur --- lib/smack/IntegerOverflowChecker.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/lib/smack/IntegerOverflowChecker.cpp b/lib/smack/IntegerOverflowChecker.cpp index 413d0c633..ba7cf5982 100644 --- a/lib/smack/IntegerOverflowChecker.cpp +++ b/lib/smack/IntegerOverflowChecker.cpp @@ -174,8 +174,11 @@ bool IntegerOverflowChecker::runOnModule(Module &m) { Value *r = createResult(ai, bits, &*I); BinaryOperator *flag = createFlag(ai, bits, isSigned, ci); if (SmackOptions::IntegerOverflow && - SmackOptions::shouldCheckFunction(F.getName())) + SmackOptions::shouldCheckFunction(F.getName())) { addCheck(co, flag, ci); + // Make the proven no-overflow fact available to later checks. + addBlockingAssume(va, flag, ci); + } for (auto U : ci->users()) { if (ExtractValueInst *ei = dyn_cast(U)) { if (ei->getNumIndices() == 1) { From 9524658cc3f1dcd49194f6bbf95afc28a40ec502 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Mon, 6 Jul 2026 08:43:06 -0700 Subject: [PATCH 2/2] Prune dominated duplicate overflow checks --- include/smack/IntegerOverflowChecker.h | 1 + lib/smack/IntegerOverflowChecker.cpp | 82 +++++++++++++++++-- .../overflow_duplicate_pruning.c | 16 ++++ 3 files changed, 93 insertions(+), 6 deletions(-) create mode 100644 test/c/targeted-checks/overflow_duplicate_pruning.c diff --git a/include/smack/IntegerOverflowChecker.h b/include/smack/IntegerOverflowChecker.h index e0012a114..c2fadf9ff 100644 --- a/include/smack/IntegerOverflowChecker.h +++ b/include/smack/IntegerOverflowChecker.h @@ -17,6 +17,7 @@ class IntegerOverflowChecker : public llvm::ModulePass { IntegerOverflowChecker() : llvm::ModulePass(ID) {} virtual llvm::StringRef getPassName() const override; virtual bool runOnModule(llvm::Module &m) override; + virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const override; private: static const std::map diff --git a/lib/smack/IntegerOverflowChecker.cpp b/lib/smack/IntegerOverflowChecker.cpp index ba7cf5982..0c1ca26cf 100644 --- a/lib/smack/IntegerOverflowChecker.cpp +++ b/lib/smack/IntegerOverflowChecker.cpp @@ -7,19 +7,23 @@ // operations, and optionally allows for the checking of overflow. // -#define DEBUG_TYPE "smack-overflow" #include "smack/IntegerOverflowChecker.h" #include "smack/Debug.h" #include "smack/Naming.h" #include "smack/SmackOptions.h" #include "llvm/ADT/APInt.h" #include "llvm/IR/Constants.h" +#include "llvm/IR/Dominators.h" #include "llvm/IR/IRBuilder.h" #include "llvm/IR/InstIterator.h" #include "llvm/IR/Module.h" #include "llvm/IR/ValueSymbolTable.h" #include "llvm/Support/Regex.h" +#include #include +#include + +#define DEBUG_TYPE "smack-overflow" namespace smack { @@ -27,6 +31,54 @@ using namespace llvm; Regex OVERFLOW_INTRINSICS("^llvm.(u|s)(add|sub|mul).with.overflow.i([0-9]+)$"); +namespace { + +struct OverflowOpKey { + bool isSigned; + Instruction::BinaryOps op; + unsigned bits; + Value *lhs; + Value *rhs; + + bool operator<(const OverflowOpKey &o) const { + if (isSigned != o.isSigned) + return isSigned < o.isSigned; + if (op != o.op) + return op < o.op; + if (bits != o.bits) + return bits < o.bits; + + std::less less; + if (lhs != o.lhs) + return less(lhs, o.lhs); + return less(rhs, o.rhs); + } +}; + +OverflowOpKey getOverflowOpKey(bool isSigned, Instruction::BinaryOps op, + unsigned bits, Value *lhs, Value *rhs) { + if ((op == Instruction::Add || op == Instruction::Mul) && + std::less()(rhs, lhs)) + std::swap(lhs, rhs); + return {isSigned, op, bits, lhs, rhs}; +} + +bool hasDominatingCheckedOp( + const std::map> &checkedOps, + const OverflowOpKey &key, Instruction *i, DominatorTree &dt) { + auto it = checkedOps.find(key); + if (it == checkedOps.end()) + return false; + + for (auto *prev : it->second) { + if (dt.dominates(prev, i)) + return true; + } + return false; +} + +} // namespace + const std::map IntegerOverflowChecker::INSTRUCTION_TABLE{{"add", Instruction::Add}, {"sub", Instruction::Sub}, @@ -117,8 +169,10 @@ bool IntegerOverflowChecker::runOnModule(Module &m) { assert(va != NULL && "Function __VERIFIER_assume should be present."); std::vector instToErase; for (auto &F : m) { - if (Naming::isSmackName(F.getName())) + if (F.isDeclaration() || Naming::isSmackName(F.getName())) continue; + auto &dt = getAnalysis(F).getDomTree(); + std::map> checkedOps; for (inst_iterator I = inst_begin(F), E = inst_end(F); I != E; ++I) { if (auto ci = dyn_cast(&*I)) { Function *f = ci->getCalledFunction(); @@ -169,15 +223,27 @@ bool IntegerOverflowChecker::runOnModule(Module &m) { SDEBUG(errs() << "Processing operator: " << op << "\n"); assert(INSTRUCTION_TABLE.count(op) != 0 && "Operator must be present in our instruction table."); + auto binOp = INSTRUCTION_TABLE.at(op); + auto key = getOverflowOpKey(isSigned, binOp, bits, + ci->getArgOperand(0), + ci->getArgOperand(1)); + bool checked = SmackOptions::IntegerOverflow && + SmackOptions::shouldCheckFunction(F.getName()); + bool alreadyChecked = + checked && hasDominatingCheckedOp(checkedOps, key, ci, dt); BinaryOperator *ai = BinaryOperator::Create( - INSTRUCTION_TABLE.at(op), eo1, eo2, "", ci); + binOp, eo1, eo2, "", ci); Value *r = createResult(ai, bits, &*I); - BinaryOperator *flag = createFlag(ai, bits, isSigned, ci); - if (SmackOptions::IntegerOverflow && - SmackOptions::shouldCheckFunction(F.getName())) { + Value *flag = nullptr; + if (alreadyChecked) + flag = ConstantInt::getFalse(F.getContext()); + else + flag = createFlag(ai, bits, isSigned, ci); + if (checked && !alreadyChecked) { addCheck(co, flag, ci); // Make the proven no-overflow fact available to later checks. addBlockingAssume(va, flag, ci); + checkedOps[key].push_back(ci); } for (auto U : ci->users()) { if (ExtractValueInst *ei = dyn_cast(U)) { @@ -207,6 +273,10 @@ bool IntegerOverflowChecker::runOnModule(Module &m) { return true; } +void IntegerOverflowChecker::getAnalysisUsage(AnalysisUsage &AU) const { + AU.addRequired(); +} + // Pass ID variable char IntegerOverflowChecker::ID = 0; diff --git a/test/c/targeted-checks/overflow_duplicate_pruning.c b/test/c/targeted-checks/overflow_duplicate_pruning.c new file mode 100644 index 000000000..b18c7dc44 --- /dev/null +++ b/test/c/targeted-checks/overflow_duplicate_pruning.c @@ -0,0 +1,16 @@ +#include "smack.h" + +// @flag --check integer-overflow +// @expect verified +// clang-format off +// @checkbpl awk "/call __SMACK_check_overflow/ { n++ } END { exit n == 1 ? 0 : 1 }" +// clang-format on + +int main(void) { + int x = __VERIFIER_nondet_int(); + __VERIFIER_assume(x < 2147483647); + int y = x + 1; + int z = x + 1; + __VERIFIER_assert(y == z); + return 0; +}