Gather shadow memory fields #7535
Conversation
Codecov ReportPatch coverage:
Additional details and impacted files@@ Coverage Diff @@
## develop #7535 +/- ##
========================================
Coverage 78.50% 78.50%
========================================
Files 1670 1671 +1
Lines 191795 191837 +42
========================================
+ Hits 150567 150610 +43
+ Misses 41228 41227 -1
Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here. ☔ View full report in Codecov by Sentry. |
peterschrammel
force-pushed
the
shadow-memory-basic2
branch
from
b6f4ffa
to
3286ae3
Compare
peterschrammel
changed the title
peterschrammel
changed the title
peterschrammel
force-pushed
the
shadow-memory-basic2
branch
2 times, most recently
from
7606203
to
4266acf
Compare
peterschrammel
force-pushed
the
shadow-memory-basic2
branch
from
4266acf
to
f474505
Compare
peterschrammel
changed the title
peterschrammel
force-pushed
the
shadow-memory-basic2
branch
from
f474505
to
5986dcd
Compare
peterschrammel
requested review from
kroening,
tautschnig and
romainbrenguier
as code owners
| if(!can_cast_type<bitvector_typet>(expr.type())) | ||
| { | ||
| throw unsupported_operation_exceptiont( | ||
| "A shadow memory field must be of a bitvector type."); | ||
| } | ||
| if(to_bitvector_type(expr.type()).get_width() > 8) | ||
| { | ||
| throw unsupported_operation_exceptiont( | ||
| "A shadow memory field must not be larger than 8 bits."); | ||
| } |
There was a problem hiding this comment.
Could we please catch this in the front-end and just have a DATA_INVARIANT here?
There was a problem hiding this comment.
This would be doable, but it would mean splitting up the logic over multiple modules, i.e. there will be shadow memory-specific logic in the front end - I tried to avoid that by postponing these checks, but I can of course change this if preferred.
There was a problem hiding this comment.
I think it would be more user-friendly to catch problems early. If the front-end can tell the user that something will necessarily fail then IMHO it should do so.
| } | ||
|
|
||
| // record the field's initial value (and type) | ||
| fields[field_name] = expr; |
There was a problem hiding this comment.
Probably a matter of style, but I'd prefer this method to return a pair (field_name, expr) and have the caller put this in place (the caller might choose insert or firmly replace).
esteffin
force-pushed
the
shadow-memory-basic2
branch
2 times, most recently
from
444b48c
to
1921cff
Compare
|
|
||
| messaget log(message_handler); | ||
| log.debug() << "Shadow memory: declare " << (is_global ? "global " : "local ") | ||
| << "field " << id2string(field_name) << " of type " |
There was a problem hiding this comment.
Nit pick: no need for id2string here.
| else if(string_expr.id() == ID_string_constant) | ||
| { | ||
| return string_expr.get(ID_value); | ||
| } |
There was a problem hiding this comment.
Nit pick: is there a reason for using braces (just!) here?
One of the utility functions that we are going to need in the shadow memory instrumentation implementation. We put these utility functions into a separate in order not to bloat the shadow_memory.cpp file.
Gathers the available shadow memory field definitions (__CPROVER_field_decl calls) from the goto model and stores them in a shadow_memory_field_definitionst.
Check that right/wrong shadow memory declarations are accepted/rejected.
esteffin
force-pushed
the
shadow-memory-basic2
branch
from
1921cff
to
addef03
Compare
Implements shadow_memoryt::gather field declarations.
Next steps: