Skip to content

Fix intKindForValue for IBool#111

Merged
sim642 merged 1 commit intodevelopfrom
intkindforvalue-bool
Sep 1, 2022
Merged

Fix intKindForValue for IBool#111
sim642 merged 1 commit intodevelopfrom
intkindforvalue-bool

Conversation

@sim642
Copy link
Copy Markdown
Member

@sim642 sim642 commented Aug 24, 2022

Upstream fix for the second issue in goblint/analyzer#827.

Technically the fix could even be moved up into truncateCilint, where IBool is already specially handled, but for some reason as never truncating. Since truncateCilint is transitively used all over the place, I didn't want to change it as the old logic might be there for some reason.

fitsInInt is used little enough to see that it isn't used with IBool anywhere previously, so no accidental behavior changes would occur.

@michael-schwarz
Copy link
Copy Markdown
Member

Could this cause issues with non-c99 code that does not expose a bool type?

@sim642
Copy link
Copy Markdown
Member Author

sim642 commented Aug 31, 2022

I don't think it can in Goblint because in other cases it could also return smaller ikinds than the program variables have, e.g. char for some value involved in int-typed variables, but that doesn't happen (it would lead to a mismatching ikind error), I suppose because we eventually cast this to a type that the program actually uses.

Another reason why this shouldn't be an issue is that we just use it for def_exc range, which is essentially an interval that may be smaller than the type's range if only small values are ever stored in such variable. The ID.t tracks the ikind (coming from the program) separately from def_exc range, so the range being tighter should be fine.

The only way I see this being a problem is if intKindForValue is used explicitly to generate some CIL AST for outputting as C code, then that ends up with _Bool being used in a program that originally might've been C99. But the same happens with any other C11 feature if used in such way.

Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

True! I think we can merge it then!

@sim642 sim642 merged commit d1e812f into develop Sep 1, 2022
@sim642 sim642 deleted the intkindforvalue-bool branch September 1, 2022 07:10
@sim642 sim642 added this to the 2.0.1 milestone Nov 21, 2022
sim642 added a commit to sim642/opam-repository that referenced this pull request Nov 23, 2022
CHANGES:

* Fix scope of enum definition in return type (goblint/cil#112, goblint/cil#113).
* Fix signed integer left shift constant folding overflow (goblint/cil#122, goblint/cil#123).
* Fix `fitsInInt` for booleans (goblint/cil#111).
* Mark more loop statement locations synthetic (goblint/cil#125).
* Optimize integer truncation (goblint/cil#115).
* Fix FrontC and Cabs2cil partial application (goblint/cil#116).
* Fix external usage of `freshLabel` (goblint/cil#121).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants