Skip to content

Prune dominated duplicate integer overflow checks#825

Open
shaobo-he wants to merge 2 commits into
developfrom
fix-751-overflow-pruning
Open

Prune dominated duplicate integer overflow checks#825
shaobo-he wants to merge 2 commits into
developfrom
fix-751-overflow-pruning

Conversation

@shaobo-he

@shaobo-he shaobo-he commented Jul 6, 2026

Copy link
Copy Markdown
Contributor

Part of #751.

This implements a concrete dependency-analysis step for integer overflow checking.

When IntegerOverflowChecker lowers llvm.{s,u}{add,sub,mul}.with.overflow intrinsics under --check=integer-overflow, it now tracks checked operations by signedness, opcode, bitwidth, and SSA operands. If an identical checked operation already dominates a later one, the later overflow assertion is skipped and the later intrinsic overflow flag is replaced with false.

This reduces redundant overflow assertions while preserving code that observes the overflow flag. Add/mul keys are canonicalized for commuted operands; sub remains ordered.

The earlier assert-assume behavior is kept for emitted checks: after __SMACK_check_overflow(flag), SMACK emits __VERIFIER_assume(!flag), making the proven no-overflow fact available downstream.

The optimization is deliberately guarded by the existing check condition:

  • only when --check=integer-overflow is active
  • only when SmackOptions::shouldCheckFunction(F.getName()) holds

Verification:

  • cmake --build build --target llvm2bpl
  • git diff --check
  • Added test/c/targeted-checks/overflow_duplicate_pruning.c, whose @checkbpl assertion requires exactly one generated call to __SMACK_check_overflow for two dominated duplicate checked additions.
  • Ran the equivalent single-test command locally with PATH preferring the rebuilt llvm2bpl; Corral is not installed locally, but Boogie generation succeeded and the @checkbpl awk count passed.

@shaobo-he shaobo-he changed the title Assume checked arithmetic overflow does not occur Prune dominated duplicate integer overflow checks Jul 6, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant