Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Jul 30, 2025

As found by @Robotechnic, we perform an overflow check for each integer literal in the program in IntDomTuple.of_int and friends.
When this check is removed (commented out here), nothing seems to break:

  • All tests pass.
  • No unsoundness is revealed on sv-benchmarks (with 60s timeout).

This brings into question whether this check has any purpose at all. I haven't dug into its git history, but it's something we should consider at some point.

@sim642 sim642 added this to the SV-COMP 2026 milestone Jul 30, 2025
@sim642 sim642 added the cleanup Refactoring, clean-up label Jul 30, 2025
@sim642
Copy link
Member Author

sim642 commented Jul 30, 2025

This happens inside of_const in the constant evaluation in base:

| Const (CInt (num,ikind,str)) ->
(match str with Some x -> if M.tracing then M.tracel "casto" "CInt (%s, %a, %s)" (Z.to_string num) d_ikind ikind x | None -> ());
Int (ID.cast_to ikind (IntDomain.of_const (num,ikind,str)))

Notably, it's immediately followed by a cast to the created ik, so we actually do two overflow checks per integer literal.
Even if it is necessary for something I'm not yet aware of, there's definitely no reason to do it twice.

@sim642
Copy link
Member Author

sim642 commented Sep 3, 2025

CIL seems to ensure that integer constants fit their type, so neither of the overflow checks should be necessary.
Worse yet, it silently truncates some constants, so Goblint even doesn't get a chance to check their overflow: goblint/cil#194.
There, in the volatile int case, there's an explicit CastE and we report the overflow on the actual cast, not on the integer literal (which is inferred to be a ILong by some rules).

These should currently never warn anyway, but suppressing them will allow avoiding unnecessary successful checks.
@sim642 sim642 changed the base branch from master to suppress_ovwarn September 4, 2025 07:56
@sim642 sim642 added the pr-dependency Depends or builds on another PR, which should be merged before label Sep 4, 2025
@sim642 sim642 changed the title Redundant overflow check in IntDomTuple.create2_ovc Remove overflow checks for integer constants Sep 4, 2025
Base automatically changed from suppress_ovwarn to master September 22, 2025 08:05
@sim642 sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label Sep 22, 2025
@sim642 sim642 marked this pull request as ready for review September 22, 2025 08:10
@sim642 sim642 merged commit 62e97b9 into master Sep 26, 2025
18 of 21 checks passed
@sim642 sim642 deleted the create2-check_ov branch September 26, 2025 06:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

cleanup Refactoring, clean-up

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant