Interpreter: de-duplicate code #2289
Conversation
tautschnig
requested review from
kroening,
peterschrammel and
smowton
as code owners
tautschnig
force-pushed
the
interpreter-deduplicate
branch
from
130596e to
54ed588
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 54ed588).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85123929
tautschnig
force-pushed
the
interpreter-deduplicate
branch
from
54ed588 to
9bae4ad
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 9bae4ad).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86270759
tautschnig
force-pushed
the
interpreter-deduplicate
branch
from
9bae4ad to
f36c08c
Compare
|
We do not have any tests of the interpreter in the code base (which is a shame), and AFAIK this changed caused some trouble. Assigning to @peterschrammel with the hope to receive some guidance, but if anyone else could contribute tests of the interpreter that would be much appreciated. |
tautschnig
added
Needs TG approval 🦉
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: f36c08c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102126796
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
There was a problem hiding this comment.
In principle looks fine (And a preliminary run of TG looks OK too) - but in the interest of helping anyone who ends up git blaming an obsecure bug this introduces could the removal of calling byte_offset_to_memory_offset be some how factored into a separate commit.
| else if(expr.id()==ID_byte_extract_little_endian || | ||
| expr.id()==ID_byte_extract_big_endian) | ||
| { | ||
| if(expr.operands().size()!=2) |
There was a problem hiding this comment.
Just noting this sanity check on byte_extract is being deleted.
| mp_integer memory_offset; | ||
| // If memory offset is found (which should normally be the case) | ||
| // extract the corresponding data from the appropriate memory location | ||
| if(!byte_offset_to_memory_offset( |
There was a problem hiding this comment.
You remove this check. No idea what it does, but it should probably be removed in a separate commit to make the move clearer.
| numeric_cast_v<std::size_t>(memory_offset + target_type_leaves)); | ||
| return; | ||
| } | ||
| // we fail |
There was a problem hiding this comment.
This comment doesn't seem quite right - we don't fail - we carry on to the next if - perhaps a throw here, or a return?
| if(!unbounded_size(expr.type())) | ||
| { | ||
| dest.resize(numeric_cast_v<std::size_t>(get_size(expr.type()))); | ||
| read(address, dest); | ||
| return; |
There was a problem hiding this comment.
This return is redundant. Probably an indication that just pulling out this whole branch into a function might make it a little easier to follow.
tautschnig
force-pushed
the
interpreter-deduplicate
branch
from
f36c08c to
936ca70
Compare
Codecov Report
@@ Coverage Diff @@
## develop #2289 +/- ##
===========================================
+ Coverage 68.53% 69.01% +0.47%
===========================================
Files 1187 1187
Lines 98262 98258 -4
===========================================
+ Hits 67346 67810 +464
+ Misses 30916 30448 -468
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
tautschnig
force-pushed
the
interpreter-deduplicate
branch
2 times, most recently
from
d9b0680 to
f30ef69
Compare
tautschnig
requested review from
chrisr-diffblue,
danpoe and
hannes-steffenhagen-diffblue
as code owners
tautschnig
force-pushed
the
interpreter-deduplicate
branch
2 times, most recently
from
266d167 to
c2f20aa
Compare
This first commit just tests that help output can be generated.
Previous help output was misleading and incomplete.
The iterator was never initialised, but still being compared to, which is undefined behaviour.
Fix basic execution as sparse vectors do not (yet) support resizing to smaller sizes (performing a clear+resize instead).
The memory map is (only) printed upon a user's request (using the "m" command). It should not be necessary to raise verbosity to debug level to see this output.
"s" without a suffix or with a suffix that is not one of [aeo0-9] previously resulted in an invariant violation. Also make "r0" actually work by fixing the assumptions about the structure of the top-level function.
evaluate_address(byte_extract) and evaluate(byte_extract) had almost the same implementation. Instead of the duplication, use `evaluate_address` to implement `evaluate` and just handle the remaining bits in `evaluate`. byte_extract still has a number of problems, as the regression test shows: addressing works at the object level, not at the level of individual bytes. Thus we can compute the correct address, but still wouldn't access the right bytes.
tautschnig
force-pushed
the
interpreter-deduplicate
branch
from
c2f20aa to
eba686f
Compare
evaluate_address(byte_extract) and evaluate(byte_extract) had almost the same
implementation.
This commit previously was part of #2165, but I suspect it is somewhat broken as #2165 previously broke test-gen. Awaiting feedback from the automatic reviewer.