avoid accesses to instructiont::guard #4144

kroening · 2019-02-09T16:19:23Z

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

allredj

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

allredj

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

tautschnig · 2019-02-11T07:45:01Z

src/goto-programs/adjust_float_expressions.cpp

-    adjust_float_expressions(it->guard, ns);
+
+    if(it->has_condition())
+      adjust_float_expressions(it->guard, ns);


Add set_condition?

tautschnig · 2019-02-11T07:45:32Z

src/goto-programs/goto_convert_functions.cpp

-         last_instruction->guard.is_true())
+      if(
+        last_instruction->is_goto() &&
+        last_instruction->get_condition().is_true())


Change in wrong commit

tautschnig · 2019-02-11T07:45:43Z

src/goto-programs/goto_inline_class.cpp

      replace_location(it->code, target->source_location);
+
+      if(it->has_condition())
+        replace_location(it->guard, target->source_location);


Add set_condition?

tautschnig · 2019-02-11T07:47:45Z

src/goto-programs/link_goto_model.cpp

-    rename_symbol(iit->guard);
+
+    if(iit->has_condition())
+      rename_symbol(iit->guard);


Add set_condition?

tautschnig · 2019-02-11T07:47:53Z

src/goto-programs/link_goto_model.cpp

-        object_type_updates(iit->guard);
+
+        if(iit->has_condition())
+          object_type_updates(iit->guard);


Add set_condition?

tautschnig · 2019-02-11T07:48:00Z

src/goto-programs/remove_complex.cpp

-    remove_complex(it->guard);
+
+    if(it->has_condition())
+      remove_complex(it->guard);


Add set_condition?

tautschnig · 2019-02-11T07:48:06Z

src/goto-programs/remove_vector.cpp

-    remove_vector(it->guard);
+
+    if(it->has_condition())
+      remove_vector(it->guard);


Add set_condition?

tautschnig · 2019-02-11T07:48:13Z

src/goto-programs/rewrite_union.cpp

-    rewrite_union(it->guard);
+
+    if(it->has_condition())
+      rewrite_union(it->guard);


Add set_condition?

src/goto-programs/slice_global_inits.cpp

tautschnig · 2019-02-11T07:48:57Z

src/pointer-analysis/goto_program_dereference.cpp

@@ -301,7 +301,8 @@ void goto_program_dereferencet::dereference_instruction(
  #endif
  goto_programt::instructiont &i=*target;

-  dereference_expr(i.guard, checks_only, value_set_dereferencet::modet::READ);
+  if(i.has_condition())
+    dereference_expr(i.guard, checks_only, value_set_dereferencet::modet::READ);


Add set_condition?

smowton

Looks good except as per @tautschnig you should probably add some non-const accessor for the guard

kroening · 2019-02-11T21:45:41Z

@smowton @tautschnig I couldn't decide between non-const get_condition() or a set_condition(...). It probably makes sense to do the non-const one, in like with the other get_() methods.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: f34ad06).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100527912
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

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

tautschnig · 2019-02-12T07:32:18Z

src/goto-programs/goto_program.h

@@ -287,6 +287,13 @@ class goto_programt
      return guard;
    }

+    /// Get the condition of gotos, assume, assert
+    exprt &get_condition()


I believe we do have a lot of places where we have a const and a non-const variant with the same name, but I also think that in those cases we neither have a get_ nor a set_ prefix? What I would have used is void set_condition(exprt cond) { PRECONDITION(has_condition()); guard = std::move(cond); }, which of course requires a somewhat bigger change in that all users need to do exprt modified_condition = get_condition(); do_something(modified_condition); set_condition(std::move(modified_condition)); But certainly nothing that I intend to block on, my approval remains in place.

Indeed; I couldn't decide. To write to stuff thats returned by get_X seems to be very common in Java, but much less common in C++.
The key reason why I went for non-const get is that we have a lot of instances where we apply a transform to the guard. That would then become
exprt tmp = instr.get_condition(); TRANSFORM(tmp); instr.set_condition(tmp);
That could possibly be changed into
instr.set_condition(TRANSFORM(instr.get_condition());
if we turn all those TRANSFORM into functional style.

I'll action this.

Another option would be to offer instructiont::transform(), which would take a lambda that modifies the expressions.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: bfb5287).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100579413
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

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

This will eventually enable use to protect instructiont::guard.

This will eventually allow us to protect the guard data member.

allredj

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

kroening added the cleanup label Feb 9, 2019

kroening requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, martin-cs, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners February 9, 2019 16:19

allredj reviewed Feb 9, 2019

View reviewed changes

kroening force-pushed the instructiont-guard branch from 5779e2a to f8538c2 Compare February 9, 2019 17:52

allredj reviewed Feb 9, 2019

View reviewed changes

tautschnig approved these changes Feb 11, 2019

View reviewed changes

tautschnig assigned kroening, danpoe, chrisr-diffblue and hannes-steffenhagen-diffblue Feb 11, 2019

smowton approved these changes Feb 11, 2019

View reviewed changes

kroening force-pushed the instructiont-guard branch 2 times, most recently from 03d1517 to 17ceafd Compare February 11, 2019 22:00

allredj reviewed Feb 11, 2019

View reviewed changes

allredj reviewed Feb 12, 2019

View reviewed changes

tautschnig reviewed Feb 12, 2019

View reviewed changes

kroening force-pushed the instructiont-guard branch from 17ceafd to bfb5287 Compare February 12, 2019 08:58

kroening removed their assignment Feb 12, 2019

kroening force-pushed the instructiont-guard branch 2 times, most recently from c500aea to 09371f1 Compare February 12, 2019 09:27

allredj reviewed Feb 12, 2019

View reviewed changes

Daniel Kroening added 3 commits February 13, 2019 08:06

use instructiont::get_condition()

52dad14

This will eventually enable use to protect instructiont::guard.

introduce instructiont::has_condition()

ee7cbbd

This will eventually enable use to protect instructiont::guard.

introduce instructiont::set_condition()

d1c2749

This will eventually allow us to protect the guard data member.

kroening force-pushed the instructiont-guard branch from 09371f1 to d1c2749 Compare February 13, 2019 08:09

peterschrammel approved these changes Feb 13, 2019

View reviewed changes

allredj reviewed Feb 13, 2019

View reviewed changes

tautschnig merged commit 606a83a into develop Feb 13, 2019

tautschnig deleted the instructiont-guard branch February 13, 2019 10:38

avoid accesses to instructiont::guard #4144

avoid accesses to instructiont::guard #4144

Uh oh!

Conversation

kroening commented Feb 9, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented Feb 11, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!