Make goto_rw slightly less conservative [depends-on: #3769, blocks: #2677, #2694] #2646

qaphla · 2018-07-31T19:21:11Z

This addresses the issues mentioned in #748 using a slightly different approach.

The issue that arose previously was that value_set_dereference failed to translate dereferences of pointers to dynamic objects into accesses of objects, and so *x = 1 would write to x but not to *x. This change ensures that an object access is always generated, and so *x = 1 can be made to no longer write to x without influencing the correctness of analyses such as dependence_graph. This change is contained in f095e43.

In order to resolve this issue, we first had to disambiguate two different exprts which were using the same ID but were semantically distinct. This is done in 87e8ab1, and more description of how it was possible to determine which meaning was intended in each case is provided in the commit message.

The final commit (a6db625) includes a test case that was introduced by #748. This pull request does not make that test case work, but since it does resolve most of the other issues resolved by #748, it made sense to introduce the test here as well.

smowton

is_dynamic_object seems like a good change to me -- though invalid_pointer_exprt for example should then also become is_invalid_pointer_exprt? Also suggest if you're introducing such an expression to give it an exprt-derived helper class (inheriting from unary_predicate_exprt I would imagine).

I don't know enough about goto_rw to comment whether the change will have unintended consequences unfortunately, so must practically defer to @tautschnig or @peterschrammel here.

smowton · 2018-08-01T13:24:37Z

src/analyses/dependence_graph.cpp

@@ -175,7 +175,9 @@ void dep_graph_domaint::data_dependencies(
    {
      bool found=false;
      for(const auto &wr : w_range.second)
+      {


Give simple re-styles like this their own commit

smowton · 2018-08-01T13:25:48Z

src/analyses/goto_rw.cpp

+  else if(expr.id()==ID_dynamic_object)
+  {
+    // Dynamic object expressions should always have two operands.
+    PRECONDITION(expr.operands().size() == 2);


Redundant with to_dynamic_object_expr

smowton · 2018-08-01T13:26:25Z

src/analyses/goto_rw.cpp

+    // Dynamic object expressions should always have two operands.
+    PRECONDITION(expr.operands().size() == 2);
+    const auto obj_instance = to_dynamic_object_expr(expr).get_instance();
+    add(mode, "dynamic_object-" + std::to_string(obj_instance), 0, -1);


Any risk of name clash? Most analyses seem to namespace dynamic objects to avoid this

smowton · 2018-08-01T13:32:13Z

src/analyses/reaching_definitions.cpp

-    const symbolt *symbol_ptr;
-    if(ns.lookup(identifier, symbol_ptr))
+    const symbolt *symbol_ptr = nullptr;
+    if(ns.lookup(identifier, symbol_ptr) &&


Move the ns.lookup() out of the test?

smowton · 2018-08-01T13:34:14Z

src/ansi-c/expr2c.cpp

@@ -3574,7 +3574,7 @@ std::string expr2ct::convert_with_precedence(
  else if(src.id()==ID_invalid_pointer)
    return convert_function(src, "__CPROVER_invalid_pointer", precedence=16);

-  else if(src.id()==ID_dynamic_object)
+  else if(src.id()==ID_is_dynamic_object)
    return convert_function(src, "DYNAMIC_OBJECT", precedence=16);


Consider the same improvement to the pretty-printed code too? (i.e. "DYNAMIC_OBJECT" -> "IS_DYNAMIC_OBJECT")

qaphla · 2018-08-01T14:17:56Z

I agree that, for example, invalid_pointer_exprt should become is_invalid_pointer_exprt, though this seems like it's not the right set of changes for that to go with.

I've addressed the other comments in the next version of this PR.

martin-cs · 2018-08-02T20:32:27Z

src/solvers/flattening/bv_pointers.cpp

@@ -45,7 +45,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
      }
    }
  }
-  else if(expr.id()==ID_dynamic_object)
+  else if(expr.id()==ID_is_dynamic_object)
  {
    if(operands.size()==1 &&


These should probably become DATA_INVARIANTS but this is a clean up and not vital for this PR.

These being the condition operands.size() == 1 && operands[0].type().id() == ID_pointer?

Yes. They should be enforced on exprt creation with PRECONDITION, on conversion with DATA_INVARIANT (as you have done in std_expr) and then referenced / checked with DATA_INVARIANT when they are relevant for the usage (for example here).

martin-cs

I think so. Can people who care about the full slicer and have test suites for it ( @polgreen @tautschnig @danpoe @chrisr-diffblue ) have a quick run with this PR.

martin-cs · 2018-08-02T20:33:59Z

src/util/simplify_expr_pointer.cpp

-  if(expr.operands().size()!=1)
-    return true;
+  // This should hold as a result of the expr ID being is_dynamic_object.
+  PRECONDITION(expr.operands().size() == 1);


Pedantry! DATA_INVARIANT because it is something that should always be true for think kind of exprt.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 45b5508).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80810785
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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).

polgreen · 2018-08-03T07:51:10Z

I did a quick run of this PR, rebased against develop, and with PR #2642 cherry-picked on top of it.

I don't think it's introduced any new bugs for me. The full slicer does terminate with "identifier not found", but develop does too.

This commit resolves an issue where ID_dynamic_object was used to label two semantically distinct exprts. One, with a single operand, was a boolean expression meaning that the operand is a pointer to a dynamic object. This has been renamed to ID_is_dynamic_object. The second, with two operands, is an exprt representing a dynamic object itself. This has stayed ID_dynamic_object. Disambiguating which meaning was intended in each case was relatively easy, as uses of these exprts frequently come with assertions about the number of operands, and so this was used to inform which instances of ID_dynamic_object should be changed and which should be left the same.

When handling the case of pointers, goto_rw would mark both the object pointed to and the pointer itself as written. For example, if x = &i, the line `*x = 1' would yield a write set containing both x and i, instead of just i. This resolves that issue by ensuring that value_set_dereference always gives at least one object that the dereference can refer to. This also resolves a bug wherein &a is marked as reading from a by removing the ID_symbol special case from get_objects_address_of.A

This branch is not taken by symex but it is taken by the slicer. The code I've removed has no effect, as far as I can tell, and may have been left over from an old implementation from before the beginning of the git history. Note, there is a commit that splits ID_dynamic_object into two different ids. See diffblue#2646 and diffblue#3769 for more details.

owen-mc-diffblue · 2019-04-03T06:09:42Z

I've pulled out the commit "Disambiguates two exprts with the same ID." as #4479, and added a related change.

TGWDB · 2023-05-03T15:22:21Z

Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work.

qaphla requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners July 31, 2018 19:21

smowton reviewed Aug 1, 2018

View reviewed changes

qaphla force-pushed the goto_rw_fix branch from a6db625 to cf30c3f Compare August 1, 2018 14:21

martin-cs reviewed Aug 2, 2018

View reviewed changes

martin-cs approved these changes Aug 2, 2018

View reviewed changes

qaphla force-pushed the goto_rw_fix branch from cf30c3f to 45b5508 Compare August 2, 2018 20:56

allredj reviewed Aug 2, 2018

View reviewed changes

qaphla mentioned this pull request Aug 3, 2018

Improvements to code contracts [depends-on: #2646, #2676, blocks: #2712] #2677

Closed

Cleans up some loops to have braces

3e51f30

zhixing-xu pushed a commit to zhixing-xu/cbmc that referenced this pull request Aug 7, 2018

Apply patch from diffblue#2646

939f2a2

zhixing-xu mentioned this pull request Aug 7, 2018

Fix a bug where dynamic objects' dependency across function call is not recognized [depends-on: #2646] #2694

Closed

klaas added 4 commits August 9, 2018 15:21

Turns some checks into DATA_INVARIANTs

9d8cef4

Adds slice24 test.

098a9a9

qaphla force-pushed the goto_rw_fix branch from 45b5508 to 098a9a9 Compare August 9, 2018 19:22

zhixing-xu mentioned this pull request Aug 30, 2018

Loop abstraction [depends-on: #2707] #2871

Closed

tautschnig mentioned this pull request Sep 19, 2018

Error handling cleanup in solvers/smt2 #2963

Merged

tautschnig self-assigned this Nov 10, 2018

tautschnig changed the title ~~Make goto_rw slightly less conservative~~ Make goto_rw slightly less conservative [blocks: #2677] Nov 10, 2018

tautschnig added the blocker label Nov 10, 2018

tautschnig changed the title ~~Make goto_rw slightly less conservative [blocks: #2677]~~ Make goto_rw slightly less conservative [blocks: #2677, #2694] Nov 10, 2018

tautschnig changed the title ~~Make goto_rw slightly less conservative [blocks: #2677, #2694]~~ Make goto_rw slightly less conservative [depends-on: #3769, blocks: #2677, #2694] Feb 25, 2019

tautschnig added the dependent - do not merge label Feb 25, 2019

tautschnig mentioned this pull request Feb 27, 2019

Remove redundant lines in ID_dynamic_object branch in value_set_dereferencet #4291

Merged

7 tasks

owen-mc-diffblue mentioned this pull request Apr 2, 2019

disambiguate two exprts with same ID #4479

Merged

7 tasks

TGWDB closed this May 3, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Make goto_rw slightly less conservative [depends-on: #3769, blocks: #2677, #2694] #2646

Make goto_rw slightly less conservative [depends-on: #3769, blocks: #2677, #2694] #2646

qaphla commented Jul 31, 2018

smowton left a comment

smowton Aug 1, 2018

smowton Aug 1, 2018

smowton Aug 1, 2018

smowton Aug 1, 2018

smowton Aug 1, 2018

qaphla commented Aug 1, 2018

martin-cs Aug 2, 2018

qaphla Aug 2, 2018

martin-cs Aug 2, 2018

martin-cs left a comment

martin-cs Aug 2, 2018

allredj left a comment

polgreen commented Aug 3, 2018

owen-mc-diffblue commented Apr 3, 2019

TGWDB commented May 3, 2023

Make goto_rw slightly less conservative [depends-on: #3769, blocks: #2677, #2694] #2646

Make goto_rw slightly less conservative [depends-on: #3769, blocks: #2677, #2694] #2646

Conversation

qaphla commented Jul 31, 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

qaphla commented Aug 1, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

martin-cs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

polgreen commented Aug 3, 2018

owen-mc-diffblue commented Apr 3, 2019

TGWDB commented May 3, 2023