merge_value_sets: Avoid assignment when actually values can be moved #4169

tautschnig · 2019-02-12T18:17:48Z

We don't need the contents of the source anymore. Running on SV-COMP's
ReachSafety-ECA, this saves 741s, which is approximately 9% of the runtime of merge_goto.

Each commit message has a non-empty body, explaining why the change was made.
n/a 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).
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.

romainbrenguier · 2019-02-12T19:11:11Z

src/goto-symex/goto_symex.h

@@ -251,9 +251,9 @@ class goto_symext
  // gotos
  void merge_gotos(statet &);

-  virtual void merge_goto(const goto_statet &goto_state, statet &);
+  virtual void merge_goto(goto_statet &goto_state, statet &);


I'm not sure what's happening here because there is no documentation. If the goto_state is not supposed to be used afterwards then it would be good to make it clear, either by documenting or in the type, by forcing the argument to be movable.

Fair, I'll work on adding documentation.

Documentation added.

romainbrenguier · 2019-02-12T19:11:48Z

src/goto-symex/symex_goto.cpp

-    dest.value_set=src.value_set;
+    // we don't actually need dest.value_set anymore, leave cleanup to later
+    // cleanup of goto states
+    dest.value_set.swap(src.value_set);


Why swap and not move?

I'll try to take a look whether adding a move operator would be as easy.

Done (just required also default-declaring a copy constructor).

allredj

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

smowton

Formalise this with a move-ref and this lgtm

You may also be interested in @JohnDumbell is currently separating the concepts of fresh-l2-name (global) and current-l2-name (local), so that the L2 renaming map can be straightfowardly moved as well.

smowton · 2019-02-13T09:16:37Z

src/goto-checker/symex_bmc.h

@@ -94,7 +94,7 @@ class symex_bmct : public goto_symext
  void symex_step(const get_goto_functiont &get_goto_function, statet &state)
    override;

-  void merge_goto(const goto_statet &goto_state, statet &state) override;
+  void merge_goto(goto_statet &goto_state, statet &state) override;


If goto_state is indeed dying then we should pass a goto_statet &&

tautschnig · 2019-02-13T13:57:16Z

I have incorporated all the feedback and have now triggered another profiling run just to make sure this is still working as expected. @kroening @peterschrammel either of you will need to review this as well.

romainbrenguier · 2019-02-13T14:01:33Z

src/goto-symex/goto_symex.h

@@ -232,12 +232,15 @@ class goto_symext

  virtual void symex_assume(statet &, const exprt &cond);

-  // gotos
+  /// Merge all branches joining at the current program point at the current
+  /// program point. It will apply \ref merge_goto for each goto state (each of


The end of the first sentence is repeated.

Oops, thanks, fixed.

romainbrenguier · 2019-02-13T14:10:23Z

src/goto-symex/symex_goto.cpp

+  if(state.guard.is_false() && !goto_state.guard.is_false())
+    state.value_set = std::move(goto_state.value_set);
+  else if(!goto_state.guard.is_false())
+    state.value_set.make_union(goto_state.value_set);


It would also make sense for make_union to not take a const ref, and use move instead. But that's maybe for another pull request.

Making this impactful is a bigger task, because the internal representation of a value set is reference counted. I'll leave this for another time.

We don't need the contents of the source anymore. Running on SV-COMP's ReachSafety-ECA, this saves 741s, which is approximately 9% of the runtime of goto_symext::merge_goto.

allredj

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

tautschnig · 2019-03-01T15:35:24Z

@kroening and/or @peterschrammel would you mind taking a look at this one? It's just +25/−21 and is already coming up in other PRs (#4199).

tautschnig added Symbolic Execution Performance Optimisations labels Feb 12, 2019

tautschnig requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel and smowton as code owners February 12, 2019 18:17

tautschnig force-pushed the opt-swap branch from d951590 to 8a23c84 Compare February 12, 2019 18:19

tautschnig assigned smowton and romainbrenguier Feb 12, 2019

romainbrenguier reviewed Feb 12, 2019

View reviewed changes

tautschnig self-assigned this Feb 12, 2019

allredj reviewed Feb 12, 2019

View reviewed changes

smowton approved these changes Feb 13, 2019

View reviewed changes

tautschnig force-pushed the opt-swap branch from 8a23c84 to 6c9937c Compare February 13, 2019 13:54

tautschnig assigned kroening and peterschrammel Feb 13, 2019

romainbrenguier approved these changes Feb 13, 2019

View reviewed changes

merge_value_sets: Avoid assignment when actually values can be moved

ad16b57

We don't need the contents of the source anymore. Running on SV-COMP's ReachSafety-ECA, this saves 741s, which is approximately 9% of the runtime of goto_symext::merge_goto.

tautschnig force-pushed the opt-swap branch from 6c9937c to ad16b57 Compare February 13, 2019 15:22

tautschnig unassigned smowton, tautschnig and romainbrenguier Feb 13, 2019

allredj reviewed Feb 13, 2019

View reviewed changes

tautschnig mentioned this pull request Feb 21, 2019

Move instead of merge symex L2 renaming map when possible #4199

Merged

7 tasks

tautschnig merged commit b4f65c8 into diffblue:develop Mar 2, 2019

tautschnig deleted the opt-swap branch March 2, 2019 06:21

tautschnig restored the opt-swap branch December 27, 2020 06:41

merge_value_sets: Avoid assignment when actually values can be moved #4169

merge_value_sets: Avoid assignment when actually values can be moved #4169

Uh oh!

Conversation

tautschnig commented Feb 12, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

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!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Feb 13, 2019

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!

tautschnig commented Mar 1, 2019

Uh oh!

Uh oh!

tautschnig commented Feb 12, 2019 •

edited

Loading