Add conversion of overflow expressions into terms for the new incremental SMT support #6736
Conversation
Codecov Report
@@ Coverage Diff @@
## develop #6736 +/- ##
===========================================
+ Coverage 76.87% 76.89% +0.02%
===========================================
Files 1590 1590
Lines 183887 183974 +87
===========================================
+ Hits 141364 141472 +108
+ Misses 42523 42502 -21
Continue to review full report at Codecov.
|
src/util/bitvector_expr.h
Outdated
| @@ -735,6 +735,9 @@ class binary_overflow_exprt : public binary_predicate_exprt | |||
| { | |||
| check(expr, vm); | |||
| } | |||
|
|
|||
| protected: | |||
| using binary_predicate_exprt::binary_predicate_exprt; | |||
There was a problem hiding this comment.
Why did this turn out to be necessary?
There was a problem hiding this comment.
Strictly speaking it isn't. I could have reused the existing constructor of binary_overflow_exprt, in the constructors of the new sub-classes. This would have required specifying the kind as "plus" rather than ID_overflow_plus for example. So the constructor would have been converting c-string -> irep_idt -> std::string -> string concatenation -> irep_idt. The way I have implemented this uses the end result irep_idt directly, which saves the aforementioned conversions and makes it easier for readers of the sub-class to work out what the constructor sets the id to.
Note that constructors of sub-classes need to be able to explicitly construct their base classes if no default constructor is available and that even public constructors are not available for the construction of derived classes by default. Adding using binary_predicate_exprt::binary_predicate_exprt; allows me to use the constructor of binary_predicate_exprt to construct binary_overflow_exprt, without writing a whole constructor just to forward its arguments onto the base constructor.
There was a problem hiding this comment.
The approach I outlined here doesn't actually work, due to the constructor of binary_overflow_exprt hiding the constructor of binary_predicate_exprt. This has been bug fixed in the separated PR - #6744
src/util/bitvector_expr.h
Outdated
| { | ||
| return base.id() == ID_overflow_shl; | ||
| } | ||
|
|
There was a problem hiding this comment.
Thank you for adding these. But then these are missing some unary_minus_overflow_exprt (which is a unary_overflow_exprt).
There was a problem hiding this comment.
Thank-you for the reminder. This could do with adding for completeness. However I have found that C examples with unary minus can be handled by cbmc being run with the new --incremental-smt2-solver argument, without supporting them in the new decision procedure, due to the checks being expressed in terms of more fundamental bit vector expressions in goto_check_c -
cbmc/src/ansi-c/goto_check_c.cpp
Line 859 in a50ef65
As I read the code in goto_check_c and the code in the decision procedure, it seems that the implementation of the overflow checks is split / duplicated between these two different places. Do you know if there are any plans to change how this is structured?
thomasspriggs
force-pushed
the
tas/smt_overflow
branch
from
40dcadc to
2386d4b
Compare
thomasspriggs
force-pushed
the
tas/smt_overflow
branch
from
2386d4b to
d6a2413
Compare
thomasspriggs
force-pushed
the
tas/smt_overflow
branch
from
d6a2413 to
efd4635
Compare
thomasspriggs
requested review from
peterschrammel,
TGWDB and
chris-ryder
as code owners
Noted. I think this is just missing for the multiply operation. The other places should either be commented already, or fairly self explanatory. |
I found the codes ones ok to work out, but slower and a bit harder than the ones with nice comments as well as code. |
This PR adds conversion of overflow expressions into terms for the new incremental SMT support.