Make return type of set_l*_indices be a renamedt [blocks: #4333] #3986

romainbrenguier · 2019-01-29T13:27:44Z

This makes it easier to track through which kind of renaming the symbols have been through.
This is an intermediary step, for getting all renamed expression use this types (the next step would be to do the same for all the rename_* functions)

Edit: I have changed the title of the PR to better reflect its content now that it has been rebased on the preliminary PR introducing the renamedt type

Each commit message has a non-empty body, explaining why the change was made.
[na] 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.
[na] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

martin-cs

This seems like quite a big step. How does this interact with the validity checks for programs, expressions, etc. that is being developed to capture those system invariants?

smowton · 2019-01-30T09:56:18Z

src/goto-symex/goto_symex_state.cpp

@@ -237,11 +237,13 @@ void goto_symex_statet::assignment(
  #endif
 }

-void goto_symex_statet::set_l0_indices(
+static void set_l0_indices(
+  symex_level0t level0,


Should probably be by-ref?

smowton · 2019-01-30T10:08:06Z

src/goto-symex/goto_symex_state.cpp

  }
 }

+ssa_exprt
+goto_symex_statet::rename_level0(const symbol_exprt &expr, const namespacet &ns)


Shouldn't that be specifically an ssa_exprt, considering we still explicitly convert symbol_exprt -> ssa_exprt in rename_*?

smowton · 2019-01-30T10:26:26Z

I think the template argument for level0t et al would always have to be ssa_exprt, so I'd recommend just making these subclasses of exprt. Note I would keep the type-incompatibility of l0_ssa_exprt and l1_ssa_exprt, since it's important that an L1 expr can't be silently cast to an L0 expr.

smowton · 2019-01-30T10:27:48Z

@martin-cs these would presumably render such invariants unnecessary when we can enforce with the type system, similar to how we would pass a struct_typet around and not constantly re-verify that it meets the required structure of such a type (that was checked by to_struct_typet)

romainbrenguier · 2019-01-30T15:58:26Z

@smowton

I think the template argument for level0t et al would always have to be ssa_exprt, so I'd recommend just making these subclasses of exprt. Note I would keep the type-incompatibility of l0_ssa_exprt and l1_ssa_exprt, since it's important that an L1 expr can't be silently cast to an L0 expr.

The argument sometimes needs to be exprt because for instance we have if_exprt or others which have been renamed. On the other hand ssa_exprt can only represent symbols.

allredj

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

tautschnig · 2019-03-05T16:43:45Z

src/goto-symex/goto_symex_state.cpp


  // in case we happen to be multi-threaded, record the memory access
-  bool is_shared=l2_thread_write_encoding(lhs, ns);
+  bool is_shared = l2_thread_write_encoding(l2_lhs.get(), ns);


It seems lhs == l2_lhs.get(), so why can't you just keep using lhs here (and below)?

tautschnig · 2019-03-05T16:43:51Z

src/goto-symex/renaming_level.cpp

+    !l0_expr.get().get_level_2().empty())
+  {
+    // TODO reaching here means the information that l0_expr was L1 or L2 has
+    // TODO been lost somewhere during execution, which should be avoided


Use UNREACHABLE (here and below)?

Unfortunately it is reachable. There are even cases where level 2 is set but not level 1.

Level 2 being set without level 1 is expected for objects with static lifetime, but maybe there are also actually buggy cases?

That's good to know. I think it will be easier to see if something is done wrong once the renamedt type is used everywhere in goto_symex_state. (just to be clear, we do not change the behaviour here, the ignoring of the non-empty case was just done in the caller of this function).

allredj

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

tautschnig · 2019-03-06T09:25:57Z

I think these commits either need squashing or forcibly updated dates - reviewing commit-by-commit on GitHub is not meaningful at the moment, and I'm also finding it very hard to figure out from the commit subjects where I might have to start.
I don't think that a seemingly nicely working code should newly be littered with TODOs. That's not an improvement. If there is a problem, then it should be debugged and fixed.

romainbrenguier · 2019-03-06T09:51:55Z

@tautschnig I squashed three commits, the order looks fine for me now. I removed the TODOs since it seems there is nothing wrong there.

tautschnig

Certainly adds clarity, but I think we can reduce the size of the change quite a bit as indicated below. And some parts are still unclear to me.

tautschnig · 2019-03-06T10:15:05Z

src/goto-symex/goto_symex_state.cpp

-    set_l0_indices(ssa, ns);
+  {
+    const renamedt<ssa_exprt, L0> ssa_l0 = set_l0_indices(std::move(ssa), ns);
+    ssa = ssa_l0.get();


Does the temporary really add value? I think it's pretty clear what set_l0_indices does. Therefore I'd prefer ssa = set_l0_indices(std::move(ssa), ns).get();

tautschnig · 2019-03-06T10:15:55Z

src/goto-symex/goto_symex_state.cpp

-    set_l1_indices(ssa, ns);
+  {
+    const renamedt<ssa_exprt, L1> ssa_l1 = set_l1_indices(std::move(ssa), ns);
+    ssa = ssa_l1.get();


Like for the level-0 case, I'd prefer ssa = set_l1_indices(std::move(ssa), ns).get();

tautschnig · 2019-03-06T10:16:18Z

src/goto-symex/goto_symex_state.cpp

@@ -312,7 +308,8 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
    }
    else if(level==L2)
    {
-      set_l1_indices(ssa, ns);
+      const renamedt<ssa_exprt, L1> ssa_l1 = set_l1_indices(std::move(ssa), ns);
+      ssa = ssa_l1.get();


As above, ssa_l1 is not necessary.

tautschnig · 2019-03-06T10:16:26Z

src/goto-symex/goto_symex_state.cpp

-    set_l1_indices(ssa, ns);
-
+    const renamedt<ssa_exprt, L1> ssa_l1 = set_l1_indices(std::move(ssa), ns);
+    ssa = ssa_l1.get();


tautschnig · 2019-03-06T10:19:09Z

src/goto-symex/renaming_level.cpp

-  if(!l0_expr.get().get_level_1().empty())
+  if(
+    !l0_expr.get().get_level_1().empty() ||
+    !l0_expr.get().get_level_2().empty())


To make sure there is no change in behaviour this will require an INVARIANT that !l0_expr.get().get_level_2().empty() implies !l0_expr.get().get_level_1().empty(). And I'm not convinced that holds, because a global variable would not need L1 renaming, even when L2 is non-empty.

Yes this does not hold, so we can't add an invariant. The reason this does not change the behaviour is that it is only called from set_l1_indices which had the same check until this commit.

tautschnig · 2019-03-06T10:22:39Z

src/goto-symex/goto_symex_state.cpp


-    to_ssa_expr(tmp.false_case()).set_level_2(a_s_read.first);
+    if_exprt tmp{cond.as_expr(), l2_true_case.get(), l2_false_case.get()};


Maybe we can delay the construction even further and just use l2_true_case, l2_false_case in the branches below? Overall your changes here indeed make the code much nicer!

tautschnig · 2019-03-06T10:23:08Z

src/goto-symex/goto_symex_state.cpp

-    expr=ssa_l1;
+    const renamedt<ssa_exprt, L2> ssa_l2 =
+      set_l2_indices(std::move(ssa_l1), ns);
+    expr = ssa_l2.get();


As above: get rid of ssa_l2.

tautschnig · 2019-03-06T10:23:25Z

src/goto-symex/goto_symex_state.cpp

-    expr=ssa_l1;
+    const renamedt<ssa_exprt, L2> ssa_l2 =
+      set_l2_indices(std::move(ssa_l1), ns);
+    expr = ssa_l2.get();


No need for ssa_l2.

tautschnig · 2019-03-06T10:23:33Z

src/goto-symex/goto_symex_state.cpp

-  set_l2_indices(ssa_l1, ns);
-  expr=ssa_l1;
+  const renamedt<ssa_exprt, L2> ssa_l2 = set_l2_indices(std::move(ssa_l1), ns);
+  expr = ssa_l2.get();


tautschnig · 2019-03-06T10:24:50Z

src/goto-symex/renaming_level.cpp

@@ -67,6 +67,8 @@ operator()(renamedt<ssa_exprt, L0> l0_expr) const
 renamedt<ssa_exprt, L2> symex_level2t::
 operator()(renamedt<ssa_exprt, L1> l1_expr) const
 {
+  if(!l1_expr.get().get_level_2().empty())
+    return renamedt<ssa_exprt, L2>{std::move(l1_expr.value)};


This change seems surprising to me, but I'm likely just missing something. Would you mind explaining?

As for the symex_level1t case, it does not change the behaviour because it is only called from set_l2_indices which had the same check until this commit. We need the check to be here and not in set_l2_indices, because set_l2_indices cannot create renamedt expression, the constructor is private, this ensures we cannot make a renamedt without checking it has the right indices set.

This makes explicit that the result is a renamed expression and can be propagated in through other functions.

This carries the information about which renaming the expression has been through. This requires a change in symex_level1t::operator() so that it takes care of the non-empty level 2 case.

This captures the information of which renaming the expression has been through. This requires making symex_level2t::operator() handle non-empty L2. This was handled by set_l2_indices, but it is neccessary to handle it in symex_level2t for making set_l2_indices return a renamedt.

allredj

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

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

romainbrenguier requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners January 29, 2019 13:27

romainbrenguier force-pushed the refactor/symex-rename branch from a1c6c4d to 8784834 Compare January 29, 2019 15:00

romainbrenguier mentioned this pull request Jan 29, 2019

Refactoring in goto_symex #3988

Merged

4 tasks

martin-cs reviewed Jan 29, 2019

View reviewed changes

smowton reviewed Jan 30, 2019

View reviewed changes

romainbrenguier force-pushed the refactor/symex-rename branch from 8784834 to 14e6432 Compare January 30, 2019 10:43

romainbrenguier force-pushed the refactor/symex-rename branch from 14e6432 to 192d01e Compare January 30, 2019 16:49

romainbrenguier mentioned this pull request Jan 30, 2019

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

Merged

5 tasks

peterschrammel mentioned this pull request Jan 27, 2019

Integrate fault localizer into goto checker [blocks: 4215] #3970

Merged

7 tasks

tautschnig added the Symbolic Execution label Feb 4, 2019

romainbrenguier force-pushed the refactor/symex-rename branch from 192d01e to 9beb633 Compare February 26, 2019 09:49

romainbrenguier requested review from danpoe and hannes-steffenhagen-diffblue as code owners February 26, 2019 09:49

romainbrenguier force-pushed the refactor/symex-rename branch from 9beb633 to a445e5a Compare February 26, 2019 10:52

tautschnig assigned romainbrenguier Feb 26, 2019

romainbrenguier force-pushed the refactor/symex-rename branch from a445e5a to caa3289 Compare February 28, 2019 08:06

This was referenced Feb 28, 2019

Move goto_statet and framet to their own files [blocks: #4302] #4294

Merged

Introduce a renamedt type for renamed expressions in symex #4305

Merged

romainbrenguier force-pushed the refactor/symex-rename branch from caa3289 to 9a0f990 Compare March 5, 2019 06:38

romainbrenguier force-pushed the refactor/symex-rename branch 2 times, most recently from 6ebefbb to f13a946 Compare March 5, 2019 15:46

allredj reviewed Mar 5, 2019

View reviewed changes

romainbrenguier changed the title ~~Introduce types for result of rename functions~~ Make return type of set_l*_indices be a renamedt Mar 5, 2019

tautschnig reviewed Mar 5, 2019

View reviewed changes

romainbrenguier removed In progress do not review labels Mar 5, 2019

romainbrenguier force-pushed the refactor/symex-rename branch from f13a946 to d723b64 Compare March 5, 2019 17:08

romainbrenguier removed their assignment Mar 5, 2019

allredj reviewed Mar 5, 2019

View reviewed changes

romainbrenguier mentioned this pull request Mar 6, 2019

Make set_indices a template #4333

Merged

4 tasks

tautschnig added the blocker label Mar 6, 2019

tautschnig changed the title ~~Make return type of set_l*_indices be a renamedt~~ Make return type of set_l*_indices be a renamedt [blocks: #4333] Mar 6, 2019

tautschnig assigned romainbrenguier Mar 6, 2019

romainbrenguier force-pushed the refactor/symex-rename branch from d723b64 to 5162021 Compare March 6, 2019 09:50

romainbrenguier removed their assignment Mar 6, 2019

tautschnig approved these changes Mar 6, 2019

View reviewed changes

danpoe approved these changes Mar 6, 2019

View reviewed changes

romainbrenguier added 2 commits March 6, 2019 11:46

Make set_l0_indices return a renamedt

b49354d

This makes explicit that the result is a renamed expression and can be propagated in through other functions.

Make set_l1_indices return a renamedt

2265305

This carries the information about which renaming the expression has been through. This requires a change in symex_level1t::operator() so that it takes care of the non-empty level 2 case.

romainbrenguier force-pushed the refactor/symex-rename branch from 5162021 to c91db70 Compare March 6, 2019 11:56

romainbrenguier force-pushed the refactor/symex-rename branch from c91db70 to 1bb05b6 Compare March 6, 2019 12:01

allredj reviewed Mar 6, 2019

View reviewed changes

romainbrenguier merged commit 00f125f into diffblue:develop Mar 6, 2019

romainbrenguier deleted the refactor/symex-rename branch March 6, 2019 13:11

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Make return type of set_l*_indices be a renamedt [blocks: #4333] #3986

Make return type of set_l*_indices be a renamedt [blocks: #4333] #3986

romainbrenguier commented Jan 29, 2019 •

edited

Loading

martin-cs left a comment

smowton Jan 30, 2019

smowton Jan 30, 2019

smowton commented Jan 30, 2019

smowton commented Jan 30, 2019

romainbrenguier commented Jan 30, 2019

allredj left a comment

tautschnig Mar 5, 2019

tautschnig Mar 5, 2019

romainbrenguier Mar 5, 2019

tautschnig Mar 5, 2019

romainbrenguier Mar 6, 2019

allredj left a comment

tautschnig commented Mar 6, 2019

romainbrenguier commented Mar 6, 2019

tautschnig left a comment

tautschnig Mar 6, 2019

tautschnig Mar 6, 2019

tautschnig Mar 6, 2019

tautschnig Mar 6, 2019

tautschnig Mar 6, 2019

romainbrenguier Mar 6, 2019 •

edited

Loading

tautschnig Mar 6, 2019

tautschnig Mar 6, 2019

tautschnig Mar 6, 2019

tautschnig Mar 6, 2019

tautschnig Mar 6, 2019

romainbrenguier Mar 6, 2019

allredj left a comment


		to_ssa_expr(tmp.false_case()).set_level_2(a_s_read.first);
		if_exprt tmp{cond.as_expr(), l2_true_case.get(), l2_false_case.get()};

Make return type of set_l*_indices be a renamedt [blocks: #4333] #3986

Make return type of set_l*_indices be a renamedt [blocks: #4333] #3986

Conversation

romainbrenguier commented Jan 29, 2019 • edited Loading

martin-cs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton commented Jan 30, 2019

smowton commented Jan 30, 2019

romainbrenguier commented Jan 30, 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

allredj left a comment

Choose a reason for hiding this comment

tautschnig commented Mar 6, 2019

romainbrenguier commented Mar 6, 2019

tautschnig 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

romainbrenguier Mar 6, 2019 • edited Loading

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

allredj left a comment

Choose a reason for hiding this comment

romainbrenguier commented Jan 29, 2019 •

edited

Loading

romainbrenguier Mar 6, 2019 •

edited

Loading