Add automated overflow/underflow checks for bitvector and floating-point arithmetic

[tautschnig]

Motivation

Arithmetic overflow is a major source of bugs in systems code. Signed integer overflow is undefined behavior in C/C++, unsigned overflow silently wraps, and floating-point overflow silently produces infinity. Unlike division-by-zero (added in #510), these errors are easy to miss in code review and hard to trigger in testing.

This PR extends Strata's automated verification to catch arithmetic overflow at every use site — the same way #510 catches every division by zero — so that front-end languages like Laurel (and future C/Java front-ends) get overflow checking for free, without any source-level instrumentation.

Approach

Following the pattern established by #510 for division-by-zero:

1. Safe operator variants (e.g., Bv32.SafeAdd) carry built-in preconditions asserting that overflow does not occur.
2. The existing PrecondElim transform automatically generates verification conditions at each use site.
3. Front-end translators emit safe variants instead of unchecked ones — no language-level instrumentation required.

This keeps the architecture uniform: the same mechanism handles division-by-zero, signed overflow, unsigned overflow, signed division overflow (INT_MIN / -1), and floating-point overflow to infinity.

What's covered

Signed bitvector overflow (all sizes: bv1, bv2, bv8, bv16, bv32, bv64):

• SafeAdd/SafeSub/SafeMul/SafeNeg with preconditions using SMT-LIB's bvsaddo/bvssubo/bvsmulo/bvnego

Signed division overflow (INT_MIN / -1):

• SafeSDiv/SafeSMod with dual preconditions: divisor ≠ 0 AND ¬(dividend = INT_MIN ∧ divisor = −1)

Unsigned bitvector overflow (configurable via unsignedOverflowCheck option):

• SafeUAdd/SafeUSub/SafeUMul/SafeUNeg with unsigned overflow predicates

IEEE 754 Float64:

• New float64 type in the SMT layer, encoded as (_ FloatingPoint 11 53)
• Float64.SafeAdd/SafeSub/SafeMul/SafeDiv with overflow predicates
• Overflow = finite inputs producing ±infinity (following CBMC's float_overflow_check)
• Laurel's TFloat64 now translates to real Float64 (was "Float64IsNotSupportedYet")

GOTO backend:

• Overflow predicates translate to CBMC's native overflow-+, overflow--, overflow-*, overflow-unary- expressions
• Safe operators translate to the same GOTO operations as their unchecked counterparts

Key design decisions

• Safe variants are opt-in at the Core level — Bv32.Add (wrapping) and Bv32.SafeAdd (checked) coexist. Front-end translators choose which to emit.
• Unsigned overflow is off by default — wrapping is the intended semantics in most languages. Enable with unsignedOverflowCheck := true.
• Signed overflow is always checked when using safe variants — this matches C/C++ undefined behavior semantics.
• The GOTO backend uses CBMC's native overflow expressions rather than the SMT encoding, so CBMC's solver infrastructure handles them natively.

Description of changes:

New arithmeticOverflow property type alongside the existing divisionByZero, with SARIF classification, display labels, and check mode handling. Overflow predicates and safe operators for all BV sizes generated via Lean4 macros. SMT encoding for signed overflow uses SMT-LIB builtins; unsigned and Float64 use custom encodings. Comprehensive unit tests verify factory presence, WF obligation generation, and GOTO translation.

Co-authored-by: Kiro kiro-agent@users.noreply.github.com

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[Copilot]

Pull request overview

This PR extends Strata’s “safe operator + PrecondElim” verification pipeline (previously used for division-by-zero) to also generate verification conditions for arithmetic overflow/underflow across bitvector operations and (newly supported) Float64, with a new arithmeticOverflow property type surfaced through reporting/SARIF and supported in the CBMC GOTO backend.

Changes:

• Introduces new Core bitvector overflow predicate functions and corresponding Safe* operators intended to carry overflow preconditions (plus special handling for signed div overflow).
• Adds an SMT-layer float64 sort and Float64 operators/predicates, and updates Laurel’s TFloat64 translation to use real Float64 operators.
• Adds reporting/plumbing for the new arithmeticOverflow property type (labels/emojis/SARIF classification) and adds/updates tests for factory presence and backend translation.

Reviewed changes

Copilot reviewed 28 out of 28 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
StrataTest/Languages/Core/Tests/ProgramTypeTests.lean	Updates expected environment dump to include new Float64/BV overflow/safe functions.
StrataTest/Languages/Core/Tests/ProcedureEvalTests.lean	Updates expected prelude with new Float64/BV overflow/safe functions.
StrataTest/Languages/Core/Tests/OverflowCheckTest.lean	Adds unit tests for presence of safe ops/predicates and WF obligation generation.
StrataTest/Languages/Core/Examples/TypeDecl.lean	Updates expected reserved-type list to include float64.
StrataTest/Backends/CBMC/GOTO/LambdaToCProverGOTO.lean	Adds tests for mapping overflow predicates and safe ops to CBMC identifiers.
Strata/Transform/PrecondElim.lean	Classifies safe BV/Float64 preconditions as arithmeticOverflow for SARIF/reporting.
Strata/Languages/Laurel/LaurelToCoreTranslator.lean	Translates Laurel Float64 types/ops to Core Float64 (and uses Float64 safe ops for arithmetic).
Strata/Languages/Laurel/HeapParameterizationConstants.lean	Removes the old placeholder Float64IsNotSupportedYet datatype.
Strata/Languages/Core/Verifier.lean	Extends minimal/full label+emoji logic to include arithmeticOverflow.
Strata/Languages/Core/StatementEval.lean	Maps MetaData.propertyType strings to the new .arithmeticOverflow PropertyType.
Strata/Languages/Core/SarifOutput.lean	Adds SARIF classification string for arithmeticOverflow and updates unreachable handling comment.
Strata/Languages/Core/SMTEncoder.lean	Adds SMT encoding for float64 sort/ops, float overflow predicates, signed overflow builtins, and unsigned overflow encodings.
Strata/Languages/Core/Options.lean	Adds unsignedOverflowCheck option field (default false).
Strata/Languages/Core/Factory.lean	Adds float64 to known types; generates BV overflow predicates and BV safe ops; adds Float64 functions to the factory.
Strata/Languages/Core/DDMTransform/ASTtoCST.lean	Extends CST translation mappings for safe BV ops (and attempts overflow predicate handling).
Strata/DL/Util/BitVec.lean	Adds BitVec.unegOverflow.
Strata/DL/SMT/Translate.lean	Rejects float64 sort in Lean-denotation translation.
Strata/DL/SMT/TermType.lean	Adds float64 to SMT term primitive types.
Strata/DL/SMT/Term.lean	Adds rounding-mode primitive rne and its typing.
Strata/DL/SMT/Op.lean	Adds SMT-LIB floating-point ops (fp.add/sub/mul/div, etc.) and abbrev generation.
Strata/DL/SMT/Denote.lean	Marks float64 as having no Lean denotation.
Strata/DL/SMT/DDMTransform/Translate.lean	Emits SMT-LIB (_ FloatingPoint 11 53) for float64 and emits RNE constant.
Strata/DL/Lambda/LTy.lean	Adds LMonoTy.float64.
Strata/DL/Lambda/IntBoolFactory.lean	Extends unaryOp helper to accept preconditions (for safe operator construction).
Strata/DL/Imperative/MetaData.lean	Adds MetaData.arithmeticOverflow classification string constant.
Strata/DL/Imperative/EvalContext.lean	Adds PropertyType.arithmeticOverflow and integrates it into formatting/unreachable semantics.
Strata/Backends/CBMC/GOTO/LambdaToCProverGOTO.lean	Maps safe ops and overflow predicates to CBMC GOTO overflow IDs and marks them as signed BV ops where appropriate.
Strata/Backends/CBMC/GOTO/Expr.lean	Adds CBMC expression identifiers for minus/mult/unary-minus overflow and helper constructors.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[keyboardDrummer]

I think floats in the Laurel source languages, Java and Python, implement IEEE 754 so they do allow overflows for floating point operations, so I think Laurel's translation of floating ops should not use the 'safe' floating point operators in Core.

I think we could define a subset type for float64 that does not have positive or negative infinity as a value, and then something like var x: finiteFloat64 := a * b would simplify to

var x: float64 := 
  var t := a * b; 
  assert t != Infinity && t != -Infinity; 
  t

But it would be up to the user to indicate when they want to use a finiteFloat64 instead of a float64.

[tautschnig]

Agreed — IEEE 754 defines overflow to ±∞ as valid behavior, so unconditionally inserting overflow assertions for Laurel float ops would produce false positives for standard Java/Python programs.

Fixed in 5cae06b: the Laurel translator now uses the non-safe float operators by default. I also took the opportunity to unify the approach across all overflow check categories. There's now an OverflowChecks structure in Core.Options:

structure OverflowChecks where
  signedBV   : Bool := true   -- C: signed overflow is UB
  unsignedBV : Bool := false  -- C: unsigned wraps (defined)
  float64    : Bool := false  -- IEEE 754: overflow to ±∞ (defined)

This replaces the previous (unused) unsignedOverflowCheck flag. The config is threaded through LaurelTranslateOptions → TranslateState and exposed via --overflow-checks signed,unsigned,float64 on the CLI. Users who want finite-float checking can opt in with --overflow-checks float64.

The finiteFloat64 subset type idea is interesting for a future iteration — it would let users express the constraint at the type level rather than as a global flag.

[shigoel]

I haven't looked at this PR deeply, but I'd recommend removing FP support in Strata's SMT dialect from this PR and keeping it focused only on integers for now. Let's go back to the design board before we use SMTLib's FP theory.