Value set: lift offset from numeric constants to expressions #8647
Conversation
tautschnig
force-pushed
the
value-set-offset
branch
from
9764fbe to
5d136c4
Compare
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8647 +/- ##
===========================================
+ Coverage 80.36% 80.39% +0.02%
===========================================
Files 1688 1688
Lines 207067 207129 +62
Branches 73 73
===========================================
+ Hits 166418 166516 +98
+ Misses 40649 40613 -36 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
value-set-offset
branch
from
5d136c4 to
41811ba
Compare
| @@ -981,7 +981,7 @@ normalize(const object_descriptor_exprt &expr, const namespacet &ns) | |||
| { | |||
| return expr; | |||
| } | |||
| if(expr.offset().id() == ID_unknown) | |||
| if(!expr.offset().is_constant()) | |||
There was a problem hiding this comment.
Can we get a high level description of what is the normal form we're trying to reach ?
There was a problem hiding this comment.
To root object + constant offset, as object can be an arbitrary access path into the object. Pointer equality checks become trivial then - maybe simplify_expr has become good enough in the meanwhile.
Anyways, this seems orthogonal to this PR.
| @@ -184,7 +183,7 @@ void value_sett::output(std::ostream &out, const std::string &indent) const | |||
| stream << "<" << format(o) << ", "; | |||
|
|
|||
| if(o_it->second) | |||
| stream << *o_it->second; | |||
| stream << format(*o_it->second); | |||
There was a problem hiding this comment.
now we have to print an expression instead of a mere integer
There was a problem hiding this comment.
Yes, but why is that a concern?
There was a problem hiding this comment.
I have one remaining question: Now that we have symbolic offsets for pointer expressions instead of just "constants" or "unknown", is there ay way to use that to compute more precise results in get_value_set_rec ? I know it lets us be more precise when modelling assignments, but I don't understand why we don't have a similar gain in precision when computing dereferences/traversing value_sets.
Other question: now that the value set representation "knows" that an expression array[i] has an offset of the form i * sizeof(T) could we try to take into account extra constraints about i during the value set traversal ? Let's say we're trying to resolve array[i] in the context of a basic loop invariant 0 <= i && i <= len(array), knowing range constraints about i we could maybe avoid injecting values representing OOB accesses in the value set for array[i] ?
| @@ -981,7 +981,7 @@ normalize(const object_descriptor_exprt &expr, const namespacet &ns) | |||
| { | |||
| return expr; | |||
| } | |||
| if(expr.offset().id() == ID_unknown) | |||
| if(!expr.offset().is_constant()) | |||
There was a problem hiding this comment.
To root object + constant offset, as object can be an arbitrary access path into the object. Pointer equality checks become trivial then - maybe simplify_expr has become good enough in the meanwhile.
Anyways, this seems orthogonal to this PR.
I have already seen this happen, although it isn't necessarily very obvious unless one starts examining the formula that symex produces. #8653 is a consequence of my observations: I was surprised to still find "unknown" when I had expected a known offset
I'm not sure we even do create those OOB values here? |
tautschnig
force-pushed
the
value-set-offset
branch
from
41811ba to
96844b5
Compare
The test will otherwise exhibit undefined behaviour under CBMC 6 settings (where malloc may fail). This, in turn, can cause the expected patterns not to show up in the trace.
Several branches cannot easily be tested by regression tests as existing front-ends will never create some of the expressions.
None of these should be triggered by user-provided code.
We can safely track arbitrary expressions as pointer offsets rather than limit ourselves to just constant offsets (and then treating all other expressions as "unknown").
tautschnig
force-pushed
the
value-set-offset
branch
from
96844b5 to
056be83
Compare
This release adds aarch64 va_list support (via diffblue#8572), which makes all tests pass on aarch64 Linux. We reworked expression simplification during symbolic execution (via diffblue#8642, diffblue#8647, diffblue#8627) to produce smaller and quicker-to-solve formulae for scenarios seen by our users.
This release adds aarch64 va_list support (via diffblue#8572), which makes all tests pass on aarch64 Linux. We reworked expression simplification during symbolic execution (via diffblue#8642, diffblue#8647, diffblue#8627) to produce smaller and quicker-to-solve formulae for scenarios seen by our users.
This release adds aarch64 va_list support (via diffblue#8572), which makes all tests pass on aarch64 Linux. We reworked expression simplification during symbolic execution (via diffblue#8642, diffblue#8647, diffblue#8627) to produce smaller and quicker-to-solve formulae for scenarios seen by our users.
We can safely track arbitrary expressions as pointer offsets rather than limit ourselves to just constant offsets (and then treating all other expressions as "unknown").