Expanding __CPROVER_{r,w,rw}_ok must not introduce overflow [depends-on: #6616] #6656
Conversation
|
The simplifier is the wrong place to fix this. The simplifier (is meant to) works on fragments of logic, where there is no notion of overflow. All it is supposed to deliver is an expression that has the same models. This, of course, does not imply that programs using such expressions behave identically. |
Ok, but then we'll need extra care in |
Codecov Report
@@ Coverage Diff @@
## develop #6656 +/- ##
========================================
Coverage 76.74% 76.74%
========================================
Files 1579 1579
Lines 182171 182189 +18
========================================
+ Hits 139802 139823 +21
+ Misses 42369 42366 -3
Continue to review full report at Codecov.
|
We do not necessarily have any pragmas set, and therefore must be able to handle an empty stack. Surprisingly, this only seg faulted when building in exactly the way check-ubuntu-20_04-make-gcc is doing this in CI, and only on one test added in the next commit.
This is required to make the conversion of __builtin_X_overflow not generate spurious conversion checks. Fixes: diffblue#6452
tautschnig
force-pushed
the
bugfixes/simplifier-typecast-overflow
branch
from
b89ed34 to
8c3f5da
Compare
tautschnig
changed the title
I have now completely changed the implementation (and also the test to demonstrate where the original problem came from). This, however, requires #6616 to be merged first (which are the first two commits in here). |
tautschnig
changed the title
Distributing signed-to-unsigned type casts over addition can result in an unsigned overflow where previously there was no overflow. That's ok at the logic level for any expressions yield the same models. We just need to make sure that expressions generated are not subject to goto_check_ct generating additional checks: goto_check_ct generates C language checks, not ones for internally generated expressions.
tautschnig
force-pushed
the
bugfixes/simplifier-typecast-overflow
branch
from
8c3f5da to
29d63d3
Compare
| @@ -2020,6 +2047,10 @@ optionalt<exprt> goto_check_ct::rw_ok_check(exprt expr) | |||
| exprt c = conjunction(conjuncts); | |||
| if(enable_simplify) | |||
| simplify(c, ns); | |||
|
|
|||
| // this is a logic expression, C language checks no longer apply | |||
There was a problem hiding this comment.
Possible worth rewording the comment here to be super explicit?
| // this is a logic expression, C language checks no longer apply | |
| // this is an internal logic expression to support contracts, not a C language expression. | |
| // C language checks should not be applied to it |
|
Hello, additionally it would be nice to have a theorem that says that if |
Distributing signed-to-unsigned type casts over addition can result in
an unsigned overflow where previously there was no overflow. That's ok
at the logic level for any expressions yield the same models. We just
need to make sure that expressions generated are not subject to
goto_check_ct generating additional checks: goto_check_ct generates C
language checks, not ones for internally generated expressions.