Expression transform #5568
Expression transform #5568
Conversation
jezhiggins
requested review from
chrisr-diffblue,
danpoe,
martin-cs,
peterschrammel and
smowton
as code owners
|
Paging @hannes-steffenhagen-diffblue : hopefully you don't mind us picking up this PR? |
There was a problem hiding this comment.
Looks reasonable. If you could squash the reverted change to the CMake file back into the relevant commit so that it doesn't touch the file at all that would be nice, otherwise this is OK.
For other reviewers : one of @jezhiggins 's next tasks is refactoring the handling of command-line arguments for VSD so it will be 'connected up' by a later PR.
jezhiggins
force-pushed
the
expression-transform
branch
from
4b846ad to
e8151e8
Compare
|
@martin-cs No problem. I'll do the same for the clang-format fixes. |
jezhiggins
force-pushed
the
expression-transform
branch
2 times, most recently
from
61c23f6 to
bd33802
Compare
This only adds the configuration option in the factory, it still doesn’t add a command line argument for this
jezhiggins
force-pushed
the
expression-transform
branch
from
bd33802 to
512734e
Compare
|
Hang on a minute this is just far enough in the past for me to give this a fair review I think. |
There was a problem hiding this comment.
For other reviewers : one of @jezhiggins 's next tasks is refactoring the handling of command-line arguments for VSD so it will be 'connected up' by a later PR.
Yeah, this is probably necessary. But clearly doesn’t need to happen here.
| @@ -83,6 +84,8 @@ struct vsd_configt | |||
| options.get_bool_option("interval"); | |||
| config.advanced_sensitivities.value_set = | |||
| options.get_bool_option("value-set"); | |||
| config.advanced_sensitivities.new_value_set = | |||
There was a problem hiding this comment.
This new_value_set shenanigans probably requires an explanation. The reason here basically is we had an initial implementation of value_set_abstract_objectt that just contained a set of abstract_object_pointert – and that looked like it worked for a couple of example programs, unfortunately that just gave us set semantics over pointers rather than the actual values in them. It also didn’t have a separate class for pointers/arrays which may require different handling.
At the time we thought it’d be bad to just throw all these changes at once in there (especially for reviewers), so we essentially came up with this approach to add a flag to turn on the new behaviour instead and just rename that to "regular value set" once we’d be done implementing it. Unfortunately we didn’t get done with it before other priorities became more pressing.
| @@ -57,6 +58,7 @@ class ContainsAllOf | |||
| { | |||
| oss << ", "; | |||
| } | |||
| first = false; | |||
There was a problem hiding this comment.
That was just a bug in the original implementation, ouch
| @@ -359,3 +361,117 @@ TEST_CASE( | |||
|
|
|||
| REQUIRE(value_set.to_constant() == value); | |||
| } | |||
|
|
|||
| static abstract_environmentt get_value_set_abstract_environment() | |||
| { | |||
There was a problem hiding this comment.
One thing I really like about variable sensitivity that at least in principle most things here are much easier to test in isolation than other parts of the codebase.
| expr.type(), | ||
| value_set_abstract_valuet::valuest{ | ||
| expr_with_evaluated_operands_filled_in}), | ||
| out_modifications); |
There was a problem hiding this comment.
For very large expressions there might be some value in exiting early here when value sets get too large and just become TOP. Not super necessary right now I don’t think, but may be worth keeping in mind if it ever turns out we’re spending a ton of time here.
| auto eval_result = environment.eval(three_plus_five, ns); | ||
| REQUIRE(eval_result != nullptr); | ||
| REQUIRE(!eval_result->is_top()); | ||
| REQUIRE(!eval_result->is_bottom()); |
There was a problem hiding this comment.
This is failing apparently? Strange, I could swear I remember this working.
There was a problem hiding this comment.
I'm investigate this now. Back soon :)
There was a problem hiding this comment.
They pass on your original branch. I'm trying to investigate further ...
There was a problem hiding this comment.
Change in the abstract_environment default constructor
This branch has
abstract_environmentt::abstract_environmentt() : bottom(true) { }
while the branch this change was originally targetting has
abstract_environmentt::abstract_environmentt() : bottom(false) { }
There was a problem hiding this comment.
Comes from this commit d9cc8ac
There was a problem hiding this comment.
If I patch the abstract_value.cpp unit test so instead of the default environment, it explicitly makes it top
auto environment = abstract_environmentt{};
environment.make_top();
return environment;
then the unit tests pass. @hannes-steffenhagen-diffblue Is this ok with you? If so, I'll fixup that last commit, and we should be good.
There was a problem hiding this comment.
Sounds reasonable to me.
jezhiggins
force-pushed
the
expression-transform
branch
from
512734e to
16300bd
Compare
Codecov Report
@@ Coverage Diff @@
## develop #5568 +/- ##
===========================================
+ Coverage 69.28% 69.29% +0.01%
===========================================
Files 1241 1241
Lines 100436 100471 +35
===========================================
+ Hits 69589 69625 +36
+ Misses 30847 30846 -1
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
This PR picks out Hannes' expression transform code from #5429 so we can apply to the mainline.
I've reinstated the -Werror flag in CMakeLists.txt and applied clang-format fixes, but otherwise the code is as it comes.