Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Feb 17, 2025

Follow-up on #1682 (comment).

The replacement is straightforward but many tests seem to have failed, so this change is not as easy as it seemed.

TODO

  • Are there pre-C11 compatibility issues? Nevermind, _Bool exists since C99.
  • Fix all tests.
  • Less hacky removal of _Bool casts? Try in LibraryFunctions.
  • Use eval_bool everywhere.
  • Merge Fix bitfield _Bool casts #1814.

Based on 00-sanity/01-assert.
Related to #1682 (comment).
This matters when applied directly to pointers: #1682 (comment).
@sim642
Copy link
Member Author

sim642 commented Feb 18, 2025

Doing the _Bool cast stripping in LibraryFunctions doesn't completely work: EvalInt query on non-integers (like pointers) returns Bot to indicate the type mismatch instead of forcing it to an integer.

Having the assert analysis query with the cast added back (but not printed) seems to fix the issue, but I don't know of good of an idea that is.
The tests don't reveal this, but some analyses answer the EvalInt query by pattern matching on some binary expression. This no longer matches if there's a cast slapped in front.

One possibility to having Queries.eval_bool only add the cast for non-integer expressions (so binary comparisons don't get one). On the other hand, this makes things less consistent.
It also brings up the question whose responsibility it is to guarantee/handle/check what: the query asker or the query answerer.

@sim642 sim642 marked this pull request as ready for review February 19, 2025 08:56
@sim642 sim642 removed their assignment Apr 17, 2025
@sim642 sim642 self-assigned this Jul 15, 2025
@michael-schwarz michael-schwarz marked this pull request as draft July 15, 2025 13:21
@sim642
Copy link
Member Author

sim642 commented Jul 23, 2025

I now merged in master and used Queries.eval_bool in place of the TODOs.

@michael-schwarz This reveals a problem in the bitfield domain. In particular, it doesn't handle casts to _Bool correctly:

[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (tests/regression/83-bitfield/08-refine-with-bitfield.c:89:5-89:31)
[Error][Assert] Assertion "a & 0x80" produces a bottom. What does that mean? (currently uninitialized arrays' content is bottom) (tests/regression/83-bitfield/08-refine-with-bitfield.c:89:5-89:31)

The overflow warning there is also spurious.

It has to do with the fact that we consider _Bool to be 1-bit, so according to the bitfield domain casting 128 to _Bool overflows and something breaks in the cast as well.

@sim642 sim642 mentioned this pull request Sep 3, 2025
@sim642 sim642 added the pr-dependency Depends or builds on another PR, which should be merged before label Sep 3, 2025
@sim642 sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label Sep 17, 2025
@sim642 sim642 added this to the v2.7.0 Bamboozled Buffalo milestone Sep 17, 2025
@sim642 sim642 marked this pull request as ready for review September 17, 2025 13:19
@sim642 sim642 merged commit aeb8b2c into master Sep 17, 2025
20 of 21 checks passed
@sim642 sim642 deleted the assert-ptr branch September 17, 2025 13:19
sim642 added a commit to sim642/opam-repository that referenced this pull request Nov 27, 2025
CHANGES:

Functionally equivalent to Goblint in SV-COMP 2026.

* Add sequential portfolio for SV-COMP (goblint/analyzer#1845, goblint/analyzer#1867, goblint/analyzer#1877).
* Add struct bitfield support (goblint/analyzer#1739, goblint/analyzer#1823).
* Improve bitwise operations for integer domains (goblint/analyzer#1739).
* Reimplement HTML output in OCaml (goblint/analyzer#1752).
* Remove YAML witness version 0.1 support (goblint/analyzer#1812, goblint/analyzer#1817, goblint/analyzer#1852, goblint/analyzer#1853, goblint/analyzer#1855).
* Fix incorrect invariants in witnesses (goblint/analyzer#1818, goblint/analyzer#1876).
* Simplify relational invariants in witnesses (goblint/analyzer#1826, goblint/analyzer#1871, goblint/analyzer#1873).
* Fix argument types in Goblint stubs (goblint/analyzer#1684, goblint/analyzer#1814, goblint/analyzer#1779, goblint/analyzer#1820).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant