Repository navigation
Add regression tests for ArithmeticOnIntegerBot triggers - #2174
karoliineh wants to merge 11 commits into
Conversation
Apron relational domains compute rational bounds, while `EvalInt` must return integer values. A rationally feasible state can therefore have an empty integer projection. For example, 3 * b - 13 = 0 gives b = 13/3, whose rounded integer bounds are [5, 4]. Extend bound_texpr results to distinguish an empty integer result from unknown or unbounded bounds. Return integer bottom for empty results while retaining top when bounds are unavailable. Handle bottom states and exact non-integral constants consistently across the Apron and equality domains. Co-authored-by: OpenAI Codex <codex@openai.com>
| let bounds = A.bound_texpr Man.mgr d texpr1 in | ||
| let min = SharedFunctions.int_of_scalar ~round:`Ceil bounds.inf in | ||
| let max = SharedFunctions.int_of_scalar ~round:`Floor bounds.sup in | ||
| match min, max with | ||
| | Some min, Some max when Z.gt min max -> None | ||
| | min, max -> Some (min, max) |
There was a problem hiding this comment.
Apron can represent a non-bottom rational polyhedron that contains no integer points. For example, the constraint 3 * b - 13 = 0 has the rational solution b = 13/3, so Apron considers the state feasible even though b is an integer variable.
So, the conversion gives min = ceil(13/3) = 5, max = floor(13/3) = 4 -> [5,4]
Previously, these reversed bounds were passed to the integer domains, where different domain
components handled them inconsistently and eventually caused an ArithmeticOnIntegerBot exception (exposed by test 23-inverse-mul-bottom.c) .
Now, the added outer option distinguishes:
None: the expression has no possible integer value.Some (None, None): values may exist, but this domain cannot provide bounds.Some (Some min, Some max): known bounds
There was a problem hiding this comment.
All the tests still fail at b7964d4 though, does it only make a difference when combined with all the following changes?
| if t.d = None then None | ||
| else | ||
| match simplify_to_ref_and_offset t (Texpr1.to_expr texpr) with | ||
| | Some (None, offset, divisor) when Z.equal (Z.rem offset divisor) Z.zero -> let res = Z.div offset divisor in | ||
| (if M.tracing then M.tracel "bounds" "min: %a max: %a" GobZ.pretty res GobZ.pretty res; | ||
| Some res, Some res) | ||
| | _ -> None, None | ||
| | Some (None, offset, divisor) when Z.equal (Z.rem offset divisor) Z.zero -> | ||
| let res = Z.div offset divisor in ( | ||
| if M.tracing then M.tracel "bounds" "min: %a max: %a" GobZ.pretty res GobZ.pretty res; | ||
| Some (Some res, Some res) | ||
| ) | ||
| | Some (None, _, _) -> None | ||
| | _ -> Some (None, None) |
There was a problem hiding this comment.
For the affine equality domains, the added if t.d = None then None preserves a bottom relational state instead of reporting merely unknown bounds. Separating Some _ from None similarly distinguishes an exact non-integral rational constant from failure to derive a constant.
For the linear two-variable equality domain, the old t.d = None -> (None, None) also incorrectly converted bottom into unknown bounds. An exact constant offset / divisor is returned as a singleton only when it is integral; otherwise it has no integer value and returns None i.e., bottom.
Treat bottom operands, ArithmeticOnIntegerBot exceptions, and bottom refinement results as contradictions around the entire inverse integer operation. This covers multiplication, division, and modulo consistently with addition and subtraction while preserving unassume behavior.
There was a problem hiding this comment.
Check consistently for bot values around the callsites of inv_bin_int and inv_bin_float :
inv_bin_int: Handle integer arithmetic on bottom at the callsite instead of only in selected meet-operators;inv_bin_float: remove the try-with from around the match and move the exception-handling to the call-site;- At the callsite, handle cases where:
aorbare bot before refinement- refinement causes
ArithmeticOnIntegerBot a'orb'(the refined values) become bot
| if M.tracing then M.trace "queryanswers" "combined query %a answers %a and %a -> dead code" Queries.Any.pretty anyq Result.pretty a Result.pretty res; | ||
| raise Deadcode | ||
| | _ -> meet | ||
| end |
There was a problem hiding this comment.
Treat a meet of EvalInt answers that result in bottom as dead code instead of propagating it into subsequent integer arithmetic, where it may trigger ArithmeticOnIntegerBot. This handles several regressions:
- In 20,
def_excand Apron produce conflicting singleton values 0 and 1: the meet of these becomes bottom; - In 22, base returns integer bottom after a definite signed overflow under
assume_none; - In 23, Apron essentially returns integer bottom (see the other fix about rationals in apron). Meeting the bottom answer with other analysis answers remains bottom.
|
Testing the changes on sv-benchmarks (on
So some unsoundness going on here: investigating. |
Use the expression's target integer kind when CIL cannot infer a kind capable of representing an intermediate value. Thread the kind through DefExc and Enums range construction so oversized Apron bounds do not produce narrower, contradictory tuple components. Update the pinned goblint-cil revision for the optional intKindForValue result and corrected enum handling.
Fix for
|
| Inc (BISet.filter value_in_ikind xs) | ||
| else | ||
| top_of ikind | ||
| | Exc (xs, r) -> |
There was a problem hiding this comment.
A possible followup by codex:
Enums.norm currently assumes that an Exc range is already contained in the target ikind and therefore returns it unchanged.
That invariant is not guaranteed when intKindForValue successfully finds a wider kind than the target kind. For example, a bound outside a 32-bit target may still be representable by a 64-bit kind, causing min_range_sign_agnostic to construct a range wider than the target type.
This does not affect the btor2c-lazyMod.mul6.c case: 2^128 is not representable by any supported kind, so the new fallback uses the target IUInt128 range (0,128) directly. Nevertheless, Enums.norm should eventually handle the more general case. A conservative fix would be:
| Exc (_, r) when not (R.leq r (size ikind)) ->
top_of ikind
| Exc (xs, r) ->
(* existing handling *)
DrMichaelPetter
left a comment
DrMichaelPetter
left a comment
There was a problem hiding this comment.
The apron / linear equality part looks ok to me - I found minor explanation in comments helpful, though.
| | Some _ -> None | ||
| | None -> Some (None, None) |
There was a problem hiding this comment.
This confused me when reading, let's explain
| | Some _ -> None | |
| | None -> Some (None, None) | |
| | Some _ -> None (* Term is a constant but has a denominator different from one means an actual fracture -> no integer value *) | |
| | None -> Some (None, None) (* Term is not constant *) |
This branch has not been deployed
3 participants
This PR adds regression tests that trigger various paths that eventually raise
ArithmeticOnIntegerBot. These tests are creduced from several sv-benchmarks (documented in the test cases).Short descriptions for each:
20-evalint-mul-bottom.c, line 11:b * dDefExc.mulreceivesError intandUnknown int([-31,31]). Its fallback (defExcDomain.ml:434) delegates tolift2_inj. Because exactly one operand is bottom,lift2_injraisesArithmeticOnIntegerBotatdefExcDomain.ml:391. This occurs during a forwardEvalIntquery requested by Apron.21-if-overflow-bottom.c, line 5:24007455 * 128 / 824007455 * 128exceeds the signed int range, soDefExc.normreturnsBotunderassume_none(defExcDomain.ml:203-205). During backward refinement of the enclosing division,BaseInvariantcalculatesID.rem a b(baseInvariant.ml:331). Tuple rem first invokes division (intDomTuple.ml:448), soDefExc.divreceivesError intand8, delegates tolift2, andlift2raises atdefExcDomain.ml:372.22-recursive-assert-overflow-bottom.c, line 6:6 - *d * *d * *d*d, the cubic multiplication eventually overflows, soDefExc.normreturnsBotunderassume_none(defExcDomain.ml:203-205). The enclosingDefExc.subreceives6andError int(defExcDomain.ml:426), delegates tolift2_inj, andlift2_injraises atdefExcDomain.ml:391. This occurs during forwardEvalIntevaluation of the assertion expression.23-inverse-mul-bottom.c, line 20:a * bBaseInvariant.refine_bycalculatesID.div c yto refine one operand (baseInvariant.ml:318). The Interval component receives[0,4294967295]andBot.Interval.divdetects that exactly one operand is bottom and raisesArithmeticOnIntegerBotatintervalDomain.ml:357. Unlike tests 20 and 22, the failing operation is division used internally for inverse multiplication refinement.