Add binary representation to all bitvector values in the xml trace #5425
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
thomasspriggs
requested review from
chrisr-diffblue,
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
|
Looks like the new regression test is crashing with an invariant violation? Also, you should probably update the actual XSD with this. |
thk123
approved these changes
Jul 17, 2020
src/goto-programs/xml_goto_trace.cpp
Outdated
| xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns) | ||
| { | ||
| xmlt full_lhs_value{"full_lhs_value"}; | ||
| xmlt xml{"full_lhs_value"}; |
There was a problem hiding this comment.
⛏️ Personally don't love this name either just cos the type tells you its xml /shrug
There was a problem hiding this comment.
Ok. I am going to make this value_xml instead.
peterschrammel
approved these changes
Jul 17, 2020
martin-cs
approved these changes
Jul 19, 2020
|
@hannes-steffenhagen-diffblue The xsd does not need to be updated, because it already contains the binary attribute. This was already present in the xsd because it is already present for floating point values. |
thomasspriggs
force-pushed
the
tas/bit_vector_binary
branch
from
217469f to
5066f76
Compare
Codecov Report
@@ Coverage Diff @@
## develop #5425 +/- ##
============================================
- Coverage 68.21% 48.68% -19.54%
============================================
Files 1178 945 -233
Lines 97542 82350 -15192
============================================
- Hits 66537 40090 -26447
- Misses 31005 42260 +11255
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
The purpose of this is to provide a consistent interface for getting the values of bitvector-ed types out of the trace. An existing test is updated in this commit in order for the existing to test to match new functionality and so that every commit still passes all tests. There are instances when running with `--cprover-smt2` where the type of the expression is `bitvector_typet`, but the expression is not a `constant_exprt`. By removing the printing in this case we can avoid breaking the partial functionality available with the `--cprover-smt2` option.
In order to confirm that the binary is now included in the xml trace output. Lines may be separated with `\r\n` on windows, rather than just `\n`. So we need to match both kinds of separator in order to be platform independant. As we don't require the xml elements to be on separate lines and `\s` matches both `\r` and `\n` we can let `\s*` match all the line separators as well as any indentation characters. `uint32_t` for example fully specifies that an integer is unsigned and 32 bits. But it could be implemented as a `typedef unsigned` or a `typedef unsigned long`, so long as these underlying types fulfill the requirements. Therefore the regex for this needs to match both `16u` and `16ul` as the value.
In order to disambiguate it from `step.full_lhs_value`.
To avoid repeating ourselves and because "Which value?" is clear from the context of the function.
To answer the question of why this is not a bug when reading the code. Ideally there would exist a `bvrep2binary` function, but this is out of scope of this PR.
So that the filtering is done first and we avoid building temporaries which aren't going to be used.
Because the PR checklist says that feature changes should be documented.
thomasspriggs
force-pushed
the
tas/bit_vector_binary
branch
from
02880ec to
d744e2d
Compare
hannes-steffenhagen-diffblue
approved these changes
Jul 21, 2020
| @@ -27,15 +27,15 @@ Author: Daniel Kroening | |||
|
|
|||
| xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns) | |||
| { | |||
| xmlt full_lhs_value{"full_lhs_value"}; | |||
| xmlt value_xml{"full_lhs_value"}; | |||
There was a problem hiding this comment.
I am not sure if I agree with the reasoning of this rename. I’d probably have gone for full_lhs_value_xml instead.
| if(full_lhs_value_includes_binary(step, ns)) | ||
| const auto &bv_type = type_try_dynamic_cast<bitvector_typet>(value.type()); | ||
| const auto &constant = expr_try_dynamic_cast<constant_exprt>(value); | ||
| if(bv_type && constant) |
There was a problem hiding this comment.
I did like the full_lhs_value_includes_binary name, but I suppose if the intention is to use all bitvectors for this then this is more honest.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Add binary representation to all bitvector values in the xml trace. The purpose of this is to provide a consistent interface for getting the values of bitvector-ed types out of the trace.
My commit message includes data points confirming performance improvements (if claimed).