Field sensitive goto-symex #2574

tautschnig · 2018-07-11T20:47:35Z

~~This is the rebased version of an old patch collection. It's likely broken at present, but should be a starting point for discussing and evaluating this.~~

@smowton Has put a lot of work into this, and this PR now reflects our combined effort. It is now ready for review.

martin-cs · 2018-07-11T21:52:53Z

+1 #doeswant

smowton

Some initial comments

smowton · 2018-07-12T08:02:59Z

src/goto-symex/field_sensitivity.cpp

+    Forall_operands(it, expr)
+      operator()(ns, *it, write);
+
+  if(expr.id()==ID_symbol &&


is_ssa_expr

smowton · 2018-07-12T08:03:12Z

src/goto-symex/field_sensitivity.cpp

+  bool write) const
+{
+#if 1
+  if(expr.id()!=ID_address_of)


Comment here why address-of is special?

smowton · 2018-07-12T08:04:55Z

src/goto-symex/field_sensitivity.cpp

+  {
+    member_exprt &member=to_member_expr(expr);
+
+    if(member.struct_op().id()==ID_symbol &&


is_ssa_expr

smowton · 2018-07-12T08:08:47Z

src/goto-symex/field_sensitivity.cpp

+
+      member.struct_op()=tmp.get_original_expr();
+
+      tmp.type()=member.type();


Does tmp retain any aspect of the original struct-op here?

src/goto-symex/field_sensitivity.cpp

smowton · 2018-07-12T08:33:01Z

src/goto-symex/field_sensitivity.cpp

+        ++it, ++number)
+    {
+      member_exprt member_rhs(lhs, it->get_name(), it->type());
+      exprt member_lhs=lhs_fs.operands()[number];


smowton · 2018-07-12T08:33:54Z

src/goto-symex/field_sensitivity.cpp

+    for(unsigned i=0; i<array_size_u; ++i)
+    {
+      index_rhs.index()=from_integer(i, index_type());
+      exprt index_lhs=lhs_fs.operands()[i];


smowton · 2018-07-12T08:35:07Z

src/goto-symex/field_sensitivity.cpp

+      field_assignments_rec(ns, state, target, member_lhs, member_rhs);
+    }
+  }
+  else if(followed_type.id()==ID_array)


Worth retaining the ability to represent a whole-array assignment compactly? String constants are the main thing that springs to mind -- then break it down into smaller pieces once the program starts making individual array cell assignments?

src/goto-symex/field_sensitivity.h

smowton · 2018-07-12T08:38:38Z

src/goto-symex/symex_assign.cpp

@@ -227,11 +227,117 @@ void goto_symext::symex_assign_symbol(
    tmp_ssa_rhs.swap(ssa_rhs);
  }

+  state.field_sensitivity(ns, ssa_rhs, false);


Unclear whether this does anything or just accrues state -- give the function name a verb

peterschrammel · 2018-08-04T17:08:42Z

src/goto-symex/field_sensitivity.cpp

+
+ Purpose:
+
+\*******************************************************************/


doxygen (entire PR)

peterschrammel · 2018-08-04T17:10:36Z

src/goto-symex/field_sensitivity.cpp

+    dest=struct_exprt(ssa_expr.type());
+    dest.reserve_operands(components.size());
+
+    for(struct_union_typet::componentst::const_iterator


ranged for (entire PR)

peterschrammel · 2018-08-04T17:11:48Z

src/goto-symex/field_sensitivity.cpp

+    const struct_union_typet::componentst &components=
+      type.components();
+
+    assert(components.empty() ||


INVARIANT (entire PR)

peterschrammel · 2018-08-04T17:12:07Z

src/goto-symex/field_sensitivity.cpp

+           (lhs_fs.has_operands() &&
+            lhs_fs.operands().size()==components.size()));
+
+    unsigned number=0;


peterschrammel · 2018-08-04T17:13:32Z

src/goto-symex/field_sensitivity.cpp

+    for(exprt::operandst::const_iterator it=lhs.operands().begin();
+        it!=lhs.operands().end();
+        ++it, ++fs_it)
+      field_assignments_rec(ns, state, target, *fs_it, *it);


peterschrammel · 2018-08-04T17:23:21Z

src/goto-symex/field_sensitivity.cpp

+    mp_integer array_size;
+    if(to_integer(type.size(), array_size))
+      assert(false);
+    unsigned array_size_u=integer2unsigned(array_size);


peterschrammel · 2018-08-04T17:30:07Z

src/goto-symex/field_sensitivity.cpp

+  exprt &expr,
+  bool write) const
+{
+#if 1


Shall we have command line options to turn on/off field-sensitivity for structs/arrays to make it easier to perform experiments with it?

peterschrammel · 2018-08-04T17:30:49Z

src/goto-symex/symex_assign.cpp

+  }
+  #endif
+
+  std::cerr << from_expr(ns, "", ssa_rhs) << std::endl;


deactivate debug output

peterschrammel · 2018-08-04T17:34:30Z

regression/cbmc/Array_Propagation1/test.desc

+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+\(Starting CEGAR Loop\|VCC(s), 0 remaining after simplification$\)


What is the CEGAR Loop here? ^^

peterschrammel · 2018-08-04T17:35:40Z

src/goto-symex/symex_assign.cpp

@@ -234,6 +234,50 @@ void goto_symext::symex_assign_symbol(

  ssa_exprt lhs_mod=lhs;

+  if(ssa_rhs.id()==ID_byte_update_little_endian ||


Is there a test that triggers this case?

owen-mc-diffblue · 2018-12-11T17:11:44Z

src/goto-symex/symex_assign.cpp

+    lhs_mod = to_ssa_expr(fs_lhs);
+  }
+#endif
+
  do_simplify(ssa_rhs);

  ssa_exprt ssa_lhs=lhs;


Suggested change

ssa_exprt ssa_lhs=lhs;

ssa_exprt ssa_lhs = lhs_mod;

This makes regression/cbmc/Anonymous_Struct2 pass, and a few others.

smowton · 2018-12-14T13:20:16Z

src/goto-symex/field_sensitivity.h

+  /// \param ns: a namespace to resolve type symbols/tag types
+  /// \param state: symbolic execution state
+  /// \param target: symbolic execution equation store
+  /// \param lhs_f: expanded symbol


smowton · 2018-12-14T13:35:43Z

src/goto-symex/goto_symex_state.cpp

@@ -453,6 +458,10 @@ bool goto_symex_statet::l2_thread_read_encoding(
    (!ns.lookup(obj_identifier).is_shared() && !(dirty)(obj_identifier)))
    return false;

+  // is it an indivisible object being accessed?


Comment here on why in that case the rest of this function is inapplicable

Skip phi assignment if one of the merged states has an uninitialised object [blocks: #35, #2574, #3486]

romainbrenguier

I've only partially reviewed the first commit and I think it should be split into several commits.

regression/cbmc/variable-access-to-constant-array/test.desc

src/goto-symex/field_sensitivity.cpp

src/goto-symex/field_sensitivity.h

src/goto-symex/field_sensitivity.cpp

src/goto-symex/field_sensitivity.h

src/goto-symex/symex_assign.cpp

src/goto-symex/symex_dereference.cpp

Ensure ssa_expr's l1-identifier is consistent with its identifier [blocks: #2574]

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 7f16d25).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107604152
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 4c23625).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107608202
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 092d8fb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107795688

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 5b86aba).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108113827

romainbrenguier · 2019-04-12T13:50:25Z

Here are the results on some benchmarks. Field sensitivity seems to scale much better. Total time was
76.41 instead of 98.24. However two benchmarks failed because of invariant violations, I will try to produce a minimal example for these failures.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 098c0cb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108161278

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 9329cc2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108198940

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 5dd0b3a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108226499

field_sensitivity::apply needs to avoid expanding struct-typed symbols into fields when they're being used as lvalues.

Struct member and array index expressions are replaced by new SSA symbols such that updates to individual fields of structs or arrays do not affect the SSA index of the remaining object. This enables more fine-grained constant propagation, which should be particularly beneficial to Java (where structs/classes prevail).

The Array_Propagation1 test is no longer solved during symex in this case.

This makes it easier to read the difference between an atomic symbol and a field of a composite.

Previously this could turn e.g. struct@x#y into struct.field@x#y, regardless of whether the L2 generation #y for that field existed or not. This meant that when an L2 name was passed through field-sensitivity expansion it could end up referring to an unbound symbol, whereas an L1 name would remain coherent (e.g. struct@x -> struct.field@x), later being renamed using the ordinary level2_names map. That means the generation numbers for structs and their fields may get out of sync, but that should be harmless so long as "latest generation" is used consistently. We can now also remove constant propagator lookup after applying field sensitivity, because field_sensitivity::apply uses state.rename to apply L2 renaming, which itself consults the constant propagator. Also make is_divisible test cheaper, at the expense that synchronisation with get_fields needs to be maintained manually.

This is because a pointer into the middle of a struct can resolve into something like &struct.field, in which case we need to rewrite that as the field-sensitive SSA symbol before any further dereferencing.

…updated Otherwise e.g. in "memset2" we had the whole object being initialised with "{0, 0}" (which is stored in const prop and then expanded to individual fields), then later any operation that needed the whole-struct representation (such as the memset-of-one-field in that test, which expanded to "whole_struct = byte_update(whole_struct, offset, int, 0)") would get the whole-struct definition stored in const-prop, disregarding any intermediate updates that were able to directly reference a single field. This avoids having two different versions of a symbol (the field-of-composite and the indivisible field versions) in the most direct way possible.

…mations The function name was previously incorrect (it did more than it said), so now I just call both transformations from symex_assign.

Otherwise while everything works correctly for the state, the target sees the field expansions before the composite definition, which is a problem if the values are non-constant and so the expansion RHSes refer to the composite!

…s already L2 For an L1 or lower expression, get_fields already recursed, e.g. to turn `x` -> `{ { x..a..g, x..a..h }, x..b }` rather than `{ x..a, a..b }` when its `a` member is itself struct-typed. However this recursion was omitted in the case where the input expression is already L2 renamed.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 8cd443c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108538361

tautschnig added the do not merge label Jul 11, 2018

tautschnig requested review from kroening, peterschrammel and a team as code owners July 11, 2018 20:47

smowton reviewed Jul 12, 2018

View reviewed changes

peterschrammel reviewed Aug 4, 2018

View reviewed changes

tautschnig self-assigned this Sep 4, 2018

tautschnig force-pushed the field-sensitivity branch 3 times, most recently from ad814f9 to d5b7a9b Compare November 1, 2018 22:48

tautschnig requested a review from pkesseli as a code owner November 1, 2018 22:48

tautschnig mentioned this pull request Dec 11, 2018

Optimize remove_level_2 #3559

Merged

5 tasks

owen-mc-diffblue reviewed Dec 11, 2018

View reviewed changes

smowton reviewed Dec 14, 2018

View reviewed changes

tautschnig force-pushed the field-sensitivity branch from d5b7a9b to 0bfb212 Compare December 14, 2018 14:42

tautschnig requested a review from martin-cs as a code owner December 14, 2018 14:42

tautschnig force-pushed the field-sensitivity branch from 0bfb212 to 705eaeb Compare December 19, 2018 17:09

tautschnig added a commit that referenced this pull request Dec 19, 2018

Merge pull request #2220 from tautschnig/phi-cleanup

a94389d

Skip phi assignment if one of the merged states has an uninitialised object [blocks: #35, #2574, #3486]

tautschnig mentioned this pull request Jan 8, 2019

Ensure ssa_expr's l1-identifier is consistent with its identifier [blocks: #2574] #3719

Merged

3 tasks

tautschnig force-pushed the field-sensitivity branch from 2b6ea5c to 04ad940 Compare January 8, 2019 13:19

tautschnig removed the do not merge label Jan 8, 2019

tautschnig assigned smowton, peterschrammel, forejtv, romainbrenguier and allredj Jan 8, 2019

romainbrenguier reviewed Jan 9, 2019

View reviewed changes

tautschnig added a commit that referenced this pull request Jan 9, 2019

Merge pull request #3719 from tautschnig/ssa-field-sensitivity-l1

af79d4e

Ensure ssa_expr's l1-identifier is consistent with its identifier [blocks: #2574]

tautschnig force-pushed the field-sensitivity branch from 7f16d25 to 4c23625 Compare April 9, 2019 09:18

allredj reviewed Apr 9, 2019

View reviewed changes

tautschnig force-pushed the field-sensitivity branch from 4c23625 to 092d8fb Compare April 10, 2019 11:43

allredj reviewed Apr 10, 2019

View reviewed changes

tautschnig force-pushed the field-sensitivity branch from 092d8fb to 63936ad Compare April 11, 2019 12:38

romainbrenguier approved these changes Apr 12, 2019

View reviewed changes

allredj reviewed Apr 12, 2019

View reviewed changes

tautschnig force-pushed the field-sensitivity branch from 5b86aba to 098c0cb Compare April 12, 2019 17:09

allredj reviewed Apr 12, 2019

View reviewed changes

tautschnig force-pushed the field-sensitivity branch from 098c0cb to 9329cc2 Compare April 12, 2019 23:40

allredj reviewed Apr 13, 2019

View reviewed changes

tautschnig force-pushed the field-sensitivity branch from 9329cc2 to 5dd0b3a Compare April 13, 2019 15:25

allredj reviewed Apr 13, 2019

View reviewed changes

kroening added the Epic label Apr 15, 2019

smowton and others added 10 commits April 16, 2019 11:55

Reinstate symex-deref's write parameter

3fb0408

field_sensitivity::apply needs to avoid expanding struct-typed symbols into fields when they're being used as lvalues.

Temporarily disable field-sensitivity for arrays

ca9fcb7

The Array_Propagation1 test is no longer solved during symex in this case.

Use .. and [[]] for SSA expression field separator

9577be9

This makes it easier to read the difference between an atomic symbol and a field of a composite.

Apply field-sensitivity expansion after removing derefs

c964e4c

This is because a pointer into the middle of a struct can resolve into something like &struct.field, in which case we need to rewrite that as the field-sensitive SSA symbol before any further dereferencing.

Comment on and clarify field-sensitivity-specific expression transfor…

3838235

…mations The function name was previously incorrect (it did more than it said), so now I just call both transformations from symex_assign.

tautschnig force-pushed the field-sensitivity branch from 5dd0b3a to 8cd443c Compare April 16, 2019 11:55

tautschnig merged commit e681845 into diffblue:develop Apr 16, 2019

tautschnig deleted the field-sensitivity branch April 16, 2019 14:56

allredj reviewed Apr 16, 2019

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Field sensitive goto-symex #2574

Field sensitive goto-symex #2574

tautschnig commented Jul 11, 2018 •

edited

Loading

martin-cs commented Jul 11, 2018

smowton left a comment

smowton Jul 12, 2018

smowton Jul 12, 2018

smowton Jul 12, 2018

smowton Jul 12, 2018

smowton Jul 12, 2018

smowton Jul 12, 2018

smowton Jul 12, 2018

smowton Jul 12, 2018

peterschrammel Aug 4, 2018

peterschrammel Aug 4, 2018

peterschrammel Aug 4, 2018

peterschrammel Aug 4, 2018

peterschrammel Aug 4, 2018

peterschrammel Aug 4, 2018

peterschrammel Aug 4, 2018

peterschrammel Aug 4, 2018

peterschrammel Aug 4, 2018

peterschrammel Aug 4, 2018

owen-mc-diffblue Dec 11, 2018

smowton Dec 14, 2018

smowton Dec 14, 2018

romainbrenguier left a comment

allredj left a comment

allredj left a comment

allredj left a comment

allredj left a comment

romainbrenguier commented Apr 12, 2019

allredj left a comment

allredj left a comment

allredj left a comment

allredj left a comment


		member.struct_op()=tmp.get_original_expr();

		tmp.type()=member.type();


		Purpose:

		\*******************************************************************/

		@@ -234,6 +234,50 @@ void goto_symext::symex_assign_symbol(

		ssa_exprt lhs_mod=lhs;

		if(ssa_rhs.id()==ID_byte_update_little_endian \|\|

Field sensitive goto-symex #2574

Field sensitive goto-symex #2574

Conversation

tautschnig commented Jul 11, 2018 • edited Loading

martin-cs commented Jul 11, 2018

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

romainbrenguier left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

romainbrenguier commented Apr 12, 2019

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

tautschnig commented Jul 11, 2018 •

edited

Loading