Shadow memory interface and integration hooks [blocks 7535] #7523

peterschrammel · 2023-02-04T22:02:34Z

This adds the shadow memory integration interface and integrates it into goto-symex.
The implementation is left empty and will be filled in incrementally in follow-up PRs.

No functional change to CBMC at this point.

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/
[n/a] 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.

tautschnig

Just a few initial thoughts.

src/goto-checker/multi_path_symex_only_checker.cpp

src/goto-programs/remove_returns.cpp

src/goto-symex/goto_symex.cpp

codecov · 2023-02-04T23:51:49Z

Codecov Report

Base: 78.39% // Head: 78.49% // Increases project coverage by +0.09% 🎉

Coverage data is based on head (67ce46b) compared to base (882bd0d).
Patch coverage: 77.77% of modified lines in pull request are covered.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7523      +/-   ##
===========================================
+ Coverage    78.39%   78.49%   +0.09%     
===========================================
  Files         1663     1667       +4     
  Lines       191354   191431      +77     
===========================================
+ Hits        150013   150255     +242     
+ Misses       41341    41176     -165

Impacted Files	Coverage Δ
src/goto-symex/goto_symex_state.h	`100.00% <ø> (ø)`
src/goto-symex/shadow_memory.cpp	`37.03% <37.03%> (ø)`
src/goto-symex/shadow_memory_state.h	`50.00% <50.00%> (ø)`
src/goto-symex/symex_function_call.cpp	`94.06% <76.47%> (-1.61%)`	⬇️
src/goto-checker/multi_path_symex_only_checker.cpp	`100.00% <100.00%> (ø)`
...rc/goto-checker/single_path_symex_only_checker.cpp	`98.76% <100.00%> (+0.03%)`	⬆️
src/goto-symex/goto_symex.cpp	`98.64% <100.00%> (+<0.01%)`	⬆️
src/goto-symex/goto_symex.h	`87.50% <100.00%> (+0.83%)`	⬆️
src/goto-symex/shadow_memory.h	`100.00% <100.00%> (ø)`
src/goto-symex/shadow_memory_field_definitions.h	`100.00% <100.00%> (ø)`
... and 24 more

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 at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

kroening · 2023-02-05T10:42:46Z

My standard concern: symex is already beyond the breaking point in terms of complexity. It should really be re-implemented from scratch. Furthermore, a downside of tying this into symex is that you'll never be able to use any other analyzers.

No way this can be done as a program instrumentation?

peterschrammel · 2023-02-05T11:24:07Z

The integration has only a few touchpoints with symex, which are already all fully implemented in this PR:

interpreting a couple of function calls, which is not problematic wrt complexity, IMO.
calling a function when symex processes memory allocations (4 places)
I need to symex assignments.

That's it.

Furthermore, a downside of tying this into symex is that you'll never be able to use any other analyzers. No way this can be done as a program instrumentation?

Having tried to implement that on various levels (C, goto, symex), I can say that the symex-level implementation is by far the most correct, simplest and elegant, and orders of magnitude faster. The crucial ingredient for the implementation is to replace the base objects (i.e. the original memory chunks by their shadows) in a given pointer-dereference operation. This is totally trivial in symex, but can't be reasonably emulated on goto or C level.

These will hold the shadow memory field definitions declared by the user in the C source files via shadow memory API calls.

This data structure tracks the shadow memory information during symbolic execution.

This tracks the shadow memory information required to resolve get_field and set_field shadow memory accesses.

The interface provided by the shadow memory instrumentation for integration with the symbolic execution.

tautschnig · 2023-02-13T13:14:21Z

src/goto-symex/goto_symex.h

@@ -98,16 +109,22 @@ class goto_symext
  /// having the state around afterwards.
  /// \param get_goto_function: The delegate to retrieve function bodies (see
  ///   \ref get_goto_functiont)
-  /// \return A symbol table holding the symbols added during symbolic
-  ///   execution.
+  /// \param fields The shadow memory field declarations


This change (unintentionally?) discards the \return comment.

tautschnig · 2023-02-13T13:15:38Z

src/goto-symex/shadow_memory.cpp

+    id2string(state.source.function_id),
+    SHADOW_MEMORY_PREFIX + from_expr(expr) + "__" + id2string(field_name),
+    state.source.pc->source_location(),
+    ID_C,


Is this always the right mode?

tautschnig · 2023-02-13T13:17:08Z

src/goto-symex/symex_assign.cpp

+  if(rhs.id() == ID_address_of)
+  {
+    const address_of_exprt &address_of = to_address_of_expr(rhs);
+    if(address_of.object().id() == ID_index)
+    {
+      const index_exprt &index = to_index_expr(address_of.object());


You might consider using expr_try_dynamic_cast to make this code more concise?

tautschnig · 2023-02-13T13:17:43Z

src/goto-symex/symex_assign.cpp

+      const index_exprt &index = to_index_expr(address_of.object());
+      if(
+        index.array().id() == ID_string_constant &&
+        index.index() == from_integer(0, c_index_type()))


Does any other type not work here? Could you instead use index.index().is_zero()?

The actual implementation will be added incrementally in future PRs.

Gathers the __CPROVER_field_decl* calls from the goto model. In the next step we'll pass them to goto_symex.

Initializees the shadow_memory member of the goto_symex_state that tracks the shadow memory information during symbolic execution.

Triggers allocation of global-scope shadow memory.

This will allow us to call the shadow memory instrumentation API.

This triggers the allocation of local-scope shadow memory.

This triggers the allocation of local-scope\ shadow memory.

We need to call the shadow memory instrumentation API from there.

or static variables.

Symbolically executes the respective shadow memory access calls. These produce assignments by calling symex_assign.

peterschrammel force-pushed the shadow-memory-basic branch 2 times, most recently from 3d9116b to fb7024c Compare February 4, 2023 22:17

tautschnig assigned peterschrammel Feb 4, 2023

peterschrammel force-pushed the shadow-memory-basic branch 4 times, most recently from daea9f4 to 161c60c Compare February 4, 2023 23:11

tautschnig reviewed Feb 4, 2023

View reviewed changes

src/goto-checker/multi_path_symex_only_checker.cpp Show resolved Hide resolved

src/goto-programs/remove_returns.cpp Outdated Show resolved Hide resolved

src/goto-symex/goto_symex.cpp Show resolved Hide resolved

peterschrammel force-pushed the shadow-memory-basic branch from 161c60c to 2f5bf1e Compare February 5, 2023 11:59

peterschrammel marked this pull request as ready for review February 6, 2023 09:49

peterschrammel requested review from kroening and romainbrenguier as code owners February 6, 2023 09:49

peterschrammel requested review from esteffin and TGWDB February 6, 2023 09:49

peterschrammel assigned TGWDB and esteffin and unassigned peterschrammel Feb 8, 2023

peterschrammel added 4 commits February 11, 2023 16:58

Add shadow_memory_field_definitions.h

9831522

These will hold the shadow memory field definitions declared by the user in the C source files via shadow memory API calls.

Add shadow_memory_state.h

5b0abf6

This data structure tracks the shadow memory information during symbolic execution.

Add shadow memory state to goto_symex_statet

143723a

This tracks the shadow memory information required to resolve get_field and set_field shadow memory accesses.

Add shadow_memory.h

5194a1f

The interface provided by the shadow memory instrumentation for integration with the symbolic execution.

peterschrammel force-pushed the shadow-memory-basic branch from 2f5bf1e to 9f7f2e5 Compare February 11, 2023 16:58

peterschrammel mentioned this pull request Feb 11, 2023

Gather shadow memory fields #7535

Merged

4 tasks

peterschrammel added the blocker label Feb 11, 2023

peterschrammel changed the title ~~Shadow memory interface and integration hooks~~ Shadow memory interface and integration hooks [blocks 7535] Feb 12, 2023

tautschnig approved these changes Feb 13, 2023

View reviewed changes

tautschnig assigned peterschrammel Feb 13, 2023

peterschrammel added 8 commits February 13, 2023 22:24

Add stub for shadow memory instrumentation implementation

8bea148

The actual implementation will be added incrementally in future PRs.

Preprocess shadow memory field declarations

a07dbc3

Gathers the __CPROVER_field_decl* calls from the goto model. In the next step we'll pass them to goto_symex.

Pass preprocessed shadow memory fields to goto_symex

f5f8901

Initializees the shadow_memory member of the goto_symex_state that tracks the shadow memory information during symbolic execution.

Initialize shadow memory on allocate()

4d8f92c

Triggers allocation of global-scope shadow memory.

Make shadow memory instrumentation available to goto_symex

1a9b71b

This will allow us to call the shadow memory instrumentation API.

Initialize shadow memory for locals

e9df8eb

This triggers the allocation of local-scope shadow memory.

Initialize shadow memory for function parameters

bc1869d

This triggers the allocation of local-scope\ shadow memory.

Pass shadow_memory to symex_assignt

c0dd6e8

We need to call the shadow memory instrumentation API from there.

peterschrammel force-pushed the shadow-memory-basic branch from 9f7f2e5 to 9fed50f Compare February 13, 2023 22:24

peterschrammel added 2 commits February 14, 2023 09:08

Initialize shadow memory for string constants

38b264b

or static variables.

Handle __CPROVER_set/get_field in goto_symex

67ce46b

Symbolically executes the respective shadow memory access calls. These produce assignments by calling symex_assign.

peterschrammel force-pushed the shadow-memory-basic branch from 9fed50f to 67ce46b Compare February 14, 2023 09:09

peterschrammel removed their assignment Feb 14, 2023

peterschrammel merged commit 1396782 into diffblue:develop Feb 14, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Shadow memory interface and integration hooks [blocks 7535] #7523

Shadow memory interface and integration hooks [blocks 7535] #7523

Uh oh!

peterschrammel commented Feb 4, 2023

Uh oh!

tautschnig left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

codecov bot commented Feb 4, 2023 •

edited

Loading

Uh oh!

kroening commented Feb 5, 2023

Uh oh!

peterschrammel commented Feb 5, 2023 •

edited

Loading

Uh oh!

tautschnig Feb 13, 2023

Uh oh!

tautschnig Feb 13, 2023

Uh oh!

tautschnig Feb 13, 2023

Uh oh!

tautschnig Feb 13, 2023

Uh oh!

Uh oh!

Shadow memory interface and integration hooks [blocks 7535] #7523

Shadow memory interface and integration hooks [blocks 7535] #7523

Uh oh!

Conversation

peterschrammel commented Feb 4, 2023

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

codecov bot commented Feb 4, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

kroening commented Feb 5, 2023

Uh oh!

peterschrammel commented Feb 5, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig Feb 13, 2023

Choose a reason for hiding this comment

Uh oh!

tautschnig Feb 13, 2023

Choose a reason for hiding this comment

Uh oh!

tautschnig Feb 13, 2023

Choose a reason for hiding this comment

Uh oh!

tautschnig Feb 13, 2023

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov bot commented Feb 4, 2023 •

edited

Loading

peterschrammel commented Feb 5, 2023 •

edited

Loading