Split the rename function according to the level and pass expression by copy instead of reference #3996

romainbrenguier · 2019-01-30T17:00:57Z

~~This is based on #3988 and~~ This is an intermediary step towards #3986
We split the rename functions according to there level, so that we can later make them return types which reflects the transformation.

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.
[na] 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).
[na] My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig · 2019-01-30T17:35:26Z

src/goto-symex/goto_symex_state.cpp

@@ -280,14 +280,12 @@ static void set_l2_indices(
  ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
 }

-void goto_symex_statet::rename_level0(exprt &expr, const namespacet &ns)
+exprt goto_symex_statet::rename_level0(exprt expr, const namespacet &ns)


The parameter should be const exprt &expr

In the follow up PR I will make this return another type, and then having the argument passed by copy allow to move the argument, potentially saving a copy. I also refactored the code so that this will not get called recursively.

tautschnig · 2019-01-30T17:39:48Z

src/goto-symex/goto_symex_state.cpp

@@ -280,6 +280,46 @@ static void set_l2_indices(
  ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
 }

+void goto_symex_statet::rename_level0(exprt &expr, const namespacet &ns)


I would expect that adding this function goes together with removing the same code from another function. As-is, it's difficult to assess whether this code does the same as the old one.

romainbrenguier · 2019-02-20T09:40:04Z

@tautschnig @smowton this is ready for review

allredj

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

tautschnig · 2019-02-26T16:53:51Z

The problem is that there is no equivalent of this function for L2 (it would not always return an ssa_exprt because of constant propagation). So either we will get an template that only works for level=L0, or L1 which I think is confusing. Or we need to return a type which depends on the level, which will involve a bit more template coding. What do you think?

Isn't it possible to delete a specialization? I think you should be able to do

template<> ssa_exprt rename<L2>(ssa_exprt, const namespacet &) = delete;

and the compiler should then happily use exprt rename<L2>(...) even when you pass in an ssa_exprt as first argument. But maybe I'm too optimistic about C++ here?

The rename<L0> function will normally be used with ssa symbols, we add that function to avoid unecessary decision making.

The level argument is always known from the call site (except for rename recursive calls), and there are only 3 possible values, so it makes sense to have it as a template argument. This will be useful in particular, when we want the return type to depend on the level.

This can be useful when we now from the caller that the expression is already is in SSA form.

In places where rename<L1> is known to be called on an ssa_exprt, we replace the call by a call to rename_level1_ssa to avoid unecessary decision making and show more information in the return type.

This makes the interface clearer as there is no argument that is both an input and an output. This also corresponds to how the function was used in a lot of occurences, in which case the code is now simpler. In the cases where we actually want the transformation to happen in-place, we can use std::move.

romainbrenguier · 2019-02-27T08:23:36Z

@tautschnig

Isn't it possible to delete a specialization? I think you should be able to do

template<> ssa_exprt rename<L2>(ssa_exprt, const namespacet &) = delete;

and the compiler should then happily use exprt rename<L2>(...) even when you pass in an ssa_exprt as first argument. But maybe I'm too optimistic about C++ here? use of deleted function

In that case I get the error: use of deleted function ‘ssa_exprt goto_symex_statet::rename(ssa_exprt, const namespacet&) [with goto_symex_statet::levelt level = (goto_symex_statet::levelt)2u]’
when calling rename<L2>

tautschnig · 2019-02-27T09:06:59Z

In that case I get the error: use of deleted function ‘ssa_exprt goto_symex_statet::rename(ssa_exprt, const namespacet&) [with goto_symex_statet::levelt level = (goto_symex_statet::levelt)2u]’
when calling rename<L2>

Hmm, too bad. Maybe we should just not use templates here at all? Just have functions rename_l0, rename_l1, rename_l2? For rename_l0 and rename_l1 we would then have polymorphic variants exprt -> exprt and ssa_exprt -> ssa_exprt, while for rename_l2 we would only have exprt -> exprt, or maybe ssa_exprt -> exprt?

romainbrenguier · 2019-02-27T09:22:05Z

@tautschnig

Hmm, too bad. Maybe we should just not use templates here at all? Just have functions rename_l0, rename_l1, rename_l2? For rename_l0 and rename_l1 we would then have polymorphic variants exprt -> exprt and ssa_exprt -> ssa_exprt, while for rename_l2 we would only have exprt -> exprt, or maybe ssa_exprt -> exprt?

The goal in having a template for the non SSA case was to avoid code duplication, because the version for three levels have a lot in common.
I think the current version of the interface is fine, the user can always use rename<level>, and the rename_level0/1_ssa is there only if they want to avoid using to_ssa_expr on the return value (and avoid some unnecessary condition checks in the called function).
I could replace the two functions by a template rename_ssa<levelt> if you think that's better (the L2 version would be deleted).

tautschnig · 2019-02-27T09:25:19Z

I could replace the two functions by a template rename_ssa<levelt> if you think that's better (the L2 version would be deleted).

Ok, that's probably the best approach. It makes functions that do the same (though slightly more performant for ssa_exprt) (almost) look the same.

romainbrenguier · 2019-02-27T10:40:49Z

@tautschnig @smowton I added a commit to merge the SSA function into one template

allredj

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

tautschnig · 2019-02-27T13:39:33Z

src/goto-symex/goto_symex_state.cpp

-    expr=ssa_exprt(expr);
-    rename<level>(expr, ns);
+    else
+      expr = rename<level>(ssa_exprt(expr), ns);


Nit pick: you otherwise aim to use {...} in constructor calls, so do ssa_exprt{expr} here as well.

tautschnig · 2019-02-27T13:43:37Z

src/goto-symex/goto_symex_state.cpp

+  else if(level == L1)
+    set_l1_indices(ssa, ns);
+  else
+    UNREACHABLE;


How about doing a full specialization here? It would do away with the static_assert and all the branching (that really isn't one, because the compiler has to remove it anyway). But that's a nit-pick, up to you.

This version avoids a bit a code duplication, so I would leave it like that. I think the static assert gives an error message that is clearer than getting a linker error.

tautschnig · 2019-02-27T13:45:24Z

src/goto-symex/goto_symex_state.cpp

      expr = rename<level>(ssa_exprt(expr), ns);
+    else // No SSA version for level2
+      expr = rename<level>((exprt)ssa_exprt(expr), ns);


Is this still necessary, given they ssa vs. non-ssa functions have different names? It if is, use static_cast, not (exprt).

tautschnig · 2019-02-27T13:46:05Z

src/goto-symex/symex_function_call.cpp

-    ssa_exprt ssa =
-      state.rename_level0_ssa(ssa_exprt(ns.lookup(*it).symbol_expr()), ns);
+    ssa_exprt ssa = state.rename_ssa<goto_symex_statet::L0>(
+      ssa_exprt(ns.lookup(*it).symbol_expr()), ns);


Use ssa_exprt{...}

tautschnig · 2019-02-27T13:47:02Z

Any idea about performance differences (if any)?

We merge rename_level0_ssa and rename_level1_ssa in one template rename_ssa<level> since the code is similar and their usage would be similar.

allredj

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

romainbrenguier · 2019-02-27T14:45:09Z

@tautschnig

Any idea about performance differences (if any)?

I ran symex on 70 functions, the time before the changes was 102.72 and after 100.88.

romainbrenguier added In progress do not review labels Jan 30, 2019

romainbrenguier requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners January 30, 2019 17:00

tautschnig reviewed Jan 30, 2019

View reviewed changes

tautschnig assigned romainbrenguier Jan 31, 2019

tautschnig added the Symbolic Execution label Feb 4, 2019

romainbrenguier force-pushed the refactor/symex-rename-copy branch from ea30965 to 4fe31a8 Compare February 7, 2019 15:25

romainbrenguier force-pushed the refactor/symex-rename-copy branch from 4fe31a8 to eee9d61 Compare February 18, 2019 15:48

romainbrenguier requested review from danpoe and hannes-steffenhagen-diffblue as code owners February 18, 2019 15:48

romainbrenguier removed In progress do not review labels Feb 18, 2019

romainbrenguier force-pushed the refactor/symex-rename-copy branch 8 times, most recently from db16730 to d52823b Compare February 20, 2019 09:39

romainbrenguier assigned smowton and tautschnig and unassigned romainbrenguier Feb 20, 2019

romainbrenguier assigned tautschnig and unassigned romainbrenguier Feb 26, 2019

allredj reviewed Feb 26, 2019

View reviewed changes

romainbrenguier added 5 commits February 27, 2019 08:11

Extract a rename_level0_ssa function

cf26fd0

The rename<L0> function will normally be used with ssa symbols, we add that function to avoid unecessary decision making.

Extract a rename_level1_ssa function

7553ca7

This can be useful when we now from the caller that the expression is already is in SSA form.

Use rename_level1_ssa where possible

9d18229

In places where rename<L1> is known to be called on an ssa_exprt, we replace the call by a call to rename_level1_ssa to avoid unecessary decision making and show more information in the return type.

romainbrenguier force-pushed the refactor/symex-rename-copy branch from 3333db0 to 44f1d42 Compare February 27, 2019 10:38

romainbrenguier force-pushed the refactor/symex-rename-copy branch from 44f1d42 to a3fe467 Compare February 27, 2019 11:55

allredj reviewed Feb 27, 2019

View reviewed changes

tautschnig approved these changes Feb 27, 2019

View reviewed changes

tautschnig assigned peterschrammel, romainbrenguier and chrisr-diffblue and unassigned tautschnig Feb 27, 2019

Merge the two rename_ssa functions

7da918f

We merge rename_level0_ssa and rename_level1_ssa in one template rename_ssa<level> since the code is similar and their usage would be similar.

romainbrenguier force-pushed the refactor/symex-rename-copy branch from a3fe467 to 7da918f Compare February 27, 2019 13:57

tautschnig mentioned this pull request Feb 27, 2019

Do not unnecessarily break sharing during renaming #4286

Closed

4 tasks

allredj reviewed Feb 27, 2019

View reviewed changes

chrisr-diffblue approved these changes Feb 27, 2019

View reviewed changes

tautschnig merged commit dc4611f into diffblue:develop Feb 27, 2019

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Split the rename function according to the level and pass expression by copy instead of reference #3996

Split the rename function according to the level and pass expression by copy instead of reference #3996

romainbrenguier commented Jan 30, 2019 •

edited

Loading

tautschnig Jan 30, 2019

romainbrenguier Feb 20, 2019

tautschnig Jan 30, 2019

romainbrenguier commented Feb 20, 2019

allredj left a comment

tautschnig commented Feb 26, 2019

romainbrenguier commented Feb 27, 2019 •

edited

Loading

tautschnig commented Feb 27, 2019

romainbrenguier commented Feb 27, 2019

tautschnig commented Feb 27, 2019

romainbrenguier commented Feb 27, 2019

allredj left a comment

tautschnig Feb 27, 2019

tautschnig Feb 27, 2019

romainbrenguier Feb 27, 2019

tautschnig Feb 27, 2019

tautschnig Feb 27, 2019

tautschnig commented Feb 27, 2019

allredj left a comment

romainbrenguier commented Feb 27, 2019

Split the rename function according to the level and pass expression by copy instead of reference #3996

Split the rename function according to the level and pass expression by copy instead of reference #3996

Conversation

romainbrenguier commented Jan 30, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

romainbrenguier commented Feb 20, 2019

allredj left a comment

Choose a reason for hiding this comment

tautschnig commented Feb 26, 2019

romainbrenguier commented Feb 27, 2019 • edited Loading

tautschnig commented Feb 27, 2019

romainbrenguier commented Feb 27, 2019

tautschnig commented Feb 27, 2019

romainbrenguier commented Feb 27, 2019

allredj 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

tautschnig commented Feb 27, 2019

allredj left a comment

Choose a reason for hiding this comment

romainbrenguier commented Feb 27, 2019

romainbrenguier commented Jan 30, 2019 •

edited

Loading

romainbrenguier commented Feb 27, 2019 •

edited

Loading