Fix for getting values of pointers in traces in new SMT backend #6831
Conversation
NlightNFotis
requested review from
peterschrammel,
thomasspriggs,
TGWDB and
chris-ryder
as code owners
| ^EXIT=10$ | ||
| ^SIGNAL=0$ | ||
| -- | ||
| -- |
There was a problem hiding this comment.
⛏️ Missing test description - "Test printing of NULL pointer values in trace."
| @@ -44,7 +44,7 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort | |||
| { | |||
| INVARIANT( | |||
| pointer_type->get_width() == sort_width, | |||
| "Width of smt bit vector term must match the width of pointer type."); | |||
| "Width of smt bit vector term must match the width of pointer type."); | |||
There was a problem hiding this comment.
⛏️ This change appears to have been squashed into the wrong commit.
| rowt{ | ||
| smt_bit_vector_constant_termt{12, 64}, | ||
| constant_exprt( | ||
| integer2bvrep(12, 64), pointer_typet(unsignedbv_typet(64), 64))}, |
There was a problem hiding this comment.
💡 It could be a bit tidier if these pointer tests were separated out into a macro like for the BIT_VECTOR_TESTS.
💡 These tests could be made more thorough by re-running them for 32 and 64 bit pointer widths.
💡 Using a pointer to a type such as bool_typet or void_type() instead of a pointer to unsignedbv_typet(64), may help improve the readability of the test by making all instances of the number 64 relate to the width of the pointer, rather than the width of the type the pointer points to.
| } | ||
| else | ||
| { | ||
| // The reason we are mnually constructing a constant_exprt here is a |
There was a problem hiding this comment.
⛏️ Typo "mnually" should be "manually"
Codecov Report
@@ Coverage Diff @@
## develop #6831 +/- ##
===========================================
+ Coverage 77.01% 77.03% +0.01%
===========================================
Files 1594 1594
Lines 184954 185016 +62
===========================================
+ Hits 142438 142520 +82
+ Misses 42516 42496 -20
Continue to review full report at Codecov.
|
…ew SMT backend. The difference is that the previous test was effectively exercising NULL and any other pointer value (1, for instance) whereas this one specifically matches the decimal value of 0xDEADBEEF.
NlightNFotis
force-pushed
the
pointer_val_in_trace_fix
branch
from
09cc397 to
691a3df
Compare
This PR changes the code that constructs bit vector terms from solver
values so that it now supports pointers.
This allows us to now see pointer values in traces in the new SMT backend.