goto_symex: implement SET_RETURN_VALUE #6436
Conversation
kroening
commented
Nov 3, 2021
kroening
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- n/a My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.
kroening
force-pushed
the
symex_set_return_value
branch
12 times, most recently
from
1096994 to
3f7cadb
Compare
kroening
requested review from
chrisr-diffblue,
martin-cs,
peterschrammel,
romainbrenguier and
tautschnig
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #6436 +/- ##
===========================================
- Coverage 76.01% 76.00% -0.01%
===========================================
Files 1527 1528 +1
Lines 164465 164469 +4
===========================================
- Hits 125013 125011 -2
- Misses 39452 39458 +6
Continue to review full report at Codecov.
|
| const auto &value_symbol = get_fresh_aux_symbol( | ||
| to_code_type(mm_io_r.type()).return_type(), | ||
| id2string(id_r) + "$value", | ||
| id2string(id_r) + "$value", | ||
| maybe_symbol->location, | ||
| maybe_symbol->mode, | ||
| symbol_table); | ||
|
|
||
| mm_io_r_value = value_symbol.symbol_expr(); | ||
| } | ||
|
|
There was a problem hiding this comment.
Why are the changes to mm_io necessary?
There was a problem hiding this comment.
The current implementation assumes that the return value is in the function#return_value variable. It needs to be changed to use the lhs in the function call.
| remove_returns(goto_model); | ||
| if( | ||
| options.get_bool_option("remove-returns") || | ||
| options.get_bool_option("string-abstraction")) |
There was a problem hiding this comment.
String abstraction was built well before return-value removal, so I wouldn't really expect a dependency here. In 425731b I noticed a need for some fixes, but I don't think that there should be a general requirement for return-value removal to make string abstraction work.
There was a problem hiding this comment.
It's unclear what the effort is. Might not be worth it, given that this feature has no known users.
This (re-)implements the goto-instruction SET_RETURN_VALUE in goto_symex. This enables dropping the requirement that SET_RETURN_INSTRUCTIONS are removed prior to invoking symex.
kroening
force-pushed
the
symex_set_return_value
branch
from
3f7cadb to
80fe6ff
Compare
