Add shadow memory get_field function #7840
Conversation
Codecov ReportPatch coverage:
Additional details and impacted files@@ Coverage Diff @@
## develop #7840 +/- ##
===========================================
- Coverage 78.81% 78.19% -0.63%
===========================================
Files 1698 1698
Lines 194821 195117 +296
===========================================
- Hits 153543 152566 -977
- Misses 41278 42551 +1273
☔ View full report in Codecov by Sentry. |
esteffin
force-pushed
the
esteffin/shadow-memory-get-field-op
branch
from
3862377
to
a8d5223
Compare
esteffin
requested review from
kroening,
tautschnig and
peterschrammel
as code owners
src/goto-symex/shadow_memory.cpp
Outdated
|
|
||
| #include "goto_symex_state.h" | ||
| #include "shadow_memory_util.h" | ||
|
|
||
| // TODO: doxygen? | ||
| static exprt | ||
| build_if_else_expr(std::vector<std::pair<exprt, exprt>> conds_values) |
There was a problem hiding this comment.
💡 Alll these static utilities should probably be moved to the _util file in order to keep the main implementation file short and concise.
src/goto-symex/shadow_memory.cpp
Outdated
|
|
||
| #include "goto_symex_state.h" | ||
| #include "shadow_memory_util.h" | ||
|
|
||
| // TODO: doxygen? |
There was a problem hiding this comment.
Yes, every function needs documentation.
src/goto-symex/shadow_memory.cpp
Outdated
| @@ -95,12 +248,323 @@ void shadow_memoryt::symex_set_field( | |||
| // To be implemented | |||
| } | |||
|
|
|||
| // TODO: doxygen? | |||
| static value_set_dereferencet::valuet get_shadow( | |||
There was a problem hiding this comment.
The naming of this function can be improved to get_shadow_dereference at least. It's not returning the "shadow" object, but the shadow object at the offset corresponding to the expr pointer.
src/goto-symex/shadow_memory.cpp
Outdated
| log_try_shadow_address(ns, log, shadowed_address); | ||
| if(!are_types_compatible(expr.type(), shadowed_address.address.type())) | ||
| { | ||
| #ifdef DEBUG_SM |
There was a problem hiding this comment.
Might be worth moving into a utility to declutter the code.
src/goto-symex/shadow_memory.cpp
Outdated
| // result += (expr_match, shadow_dereference.value) | ||
| // break; | ||
| // result += (base_match & expr_match, shadow_dereference.value) | ||
| static std::vector<std::pair<exprt, exprt>> get_field( |
There was a problem hiding this comment.
The naming of the function can be improved to get_shadow_dereference_candidates or similar.
|
|
||
| /// Given a pointer expression `address` checks if any expr in value_set is | ||
| /// compatible | ||
| bool contains_compatible_address( |
There was a problem hiding this comment.
This is misnamed and the comment above is wrong. This should be called contains_null_or_invalid.
Also, I think there's potential for simplifications as together with the invalid-by-null replacement the unknown case can probably go away (in a future PR).
| { | ||
| log.conditional_output( | ||
| log.debug(), [ns, field_name, expr](messaget::mstreamt &mstream) { | ||
| mstream << "Shadow memory: get_field: " << id2string(field_name) |
There was a problem hiding this comment.
⛏️ get_field -> get field to match the other messages
There was a problem hiding this comment.
I actually changed the others to reflect the variable name
There was a problem hiding this comment.
No, it's ok that it correctly refers to the variable.
I changed the other accordingly instead.
| #ifdef DEBUG_SM | ||
| log.conditional_output( | ||
| log.debug(), [ns, shadowed_address](messaget::mstreamt &mstream) { | ||
| mstream << "Shadow memory: trying shadowed address: " |
There was a problem hiding this comment.
⛏️ message does not match function name
| #ifdef DEBUG_SM | ||
| log.conditional_output( | ||
| log.debug(), [ns, cond_text, cond](messaget::mstreamt &mstream) { | ||
| mstream << "Shadow memory: " << cond_text << ": " << format(cond) |
There was a problem hiding this comment.
cond_text that is logged just before the : is the condition
There was a problem hiding this comment.
The condition is in cond_text before the :
esteffin
force-pushed
the
esteffin/shadow-memory-get-field-op
branch
2 times, most recently
from
de05afc
to
0d39784
Compare
Add a set of functions to shadow_memory_util.{h,cpp} that will be used
for logging purposes by `shadow_memory::symex_get_field` and its
subfunctions.
Add a set of utility functions to `shadow_memory_util.{h,cpp}` that will
be used by `shadow_memory::symex_get_field` and its subfunctions.
Add implementation to shadow_memoryt::symex_get_field also adding its subfunctions.
Function `duplicate_per_byte` checks that the `init_expr` is at max 8-bit wide. However `shadow_memoryt::initialize_shadow_memory` was removing the outer typecast to an 8-bit value, resulting in a call to `duplicate_per_byte` with an `init_expr` larger than 8-bit. This commit removes the typecast removal and fixes the issue.
esteffin
force-pushed
the
esteffin/shadow-memory-get-field-op
branch
from
0d39784
to
74f6669
Compare
Add implementation to shadow memory
symex_get_fieldfunction.Add regression tests for
symex_get_field.Fix issue with
duplicate_per_byte.To speed up integration of shadow memory functionalities improving code with proper doxygen and testing is left to a subsequent PR.