Move symex state levels to a new file #3434

romainbrenguier · 2018-11-16T12:35:56Z

No functional change.
The goal is to reduce the complexity of goto_symex_state by extracting a module which takes care of the renaming levels.

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/
[na] 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.

allredj

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

peterschrammel · 2018-11-16T16:19:18Z

src/goto-symex/renaming_level.h

+#include <util/irep.h>
+#include <util/ssa_expr.h>
+
+struct renaming_levelt


Would be good to add also some documentation at this occasion.

I added some documentation now.

allredj

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

antlechner

I'm not familiar with this part of the code but it's all refactoring and the changes look good to me! Just a few comments and questions before I can approve.

antlechner · 2018-11-19T17:34:50Z

src/goto-symex/renaming_level.h

+
+struct renaming_levelt
+{
+  virtual ~renaming_levelt() = default;


⛏️ It would have been helpful to have the moving part and making changes in separate commits.

Yes sorry about that I think I had a commit before the moving that I removed by mistake before rebasing

antlechner · 2018-11-19T17:37:31Z

src/goto-symex/renaming_level.h

+
+  void get_variables(std::unordered_set<ssa_exprt, irep_hash> &vars) const
+  {
+    for(const auto &pair : current_names)


⛏️ Can you think of a more meaningful name than pair?

antlechner · 2018-11-19T17:40:21Z

src/goto-symex/renaming_level.h

+  operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr);
+
+  symex_level0t() = default;
+  ~symex_level0t() override = default;


❓ Why is this line needed? 🐴

There may subtleties I don't fully understand there, as to why there are needed. The constructor and destructor were defined before so I left the declaration, but then clion recommends to use = default instead of {} because it is more explicit (for the compiler in particular). Tagging @LAJW in case he can bring more insight here.

It just looks a bit strange that we're overriding a method to do exactly what its parent method does, but if it was the same before then any decision to change it can be made in a future PR.

antlechner · 2018-11-19T17:40:36Z

src/goto-symex/renaming_level.h

+  }
+
+  symex_level1t() = default;
+  ~symex_level1t() override = default;


antlechner · 2018-11-19T17:40:42Z

src/goto-symex/renaming_level.h

+struct symex_level2t : public renaming_levelt
+{
+  symex_level2t() = default;
+  ~symex_level2t() override = default;


antlechner · 2018-11-19T18:29:44Z

src/goto-instrument/accelerate/scratch_program.cpp

@@ -35,7 +35,7 @@ bool scratch_programt::check_sat(bool do_slice)
  output(ns, "scratch", std::cout);
 #endif

-  goto_symex_statet::propagationt::valuest constants;


❓ This doesn't actually seem to be used anywhere, can it be removed?

👍 good catch

antlechner · 2018-11-19T18:35:50Z

src/goto-symex/goto_symex_state.cpp

      rename(expr.type(), ssa.get_identifier(), ns, level);
      ssa.update_type();
    }
    else if(level==L2)
    {
-      set_ssa_indices(ssa, ns, L1);
+      set_l1_indices(ssa, ns);


💡 "If L2 then use the L1 version" is quite confusing. I see that it was the same before your changes, but if you know the reason, could you explain it here?

I agree it's a bit confusing and I don't know exactly how it works, but I think the idea is that doing the renaming for one level you should also take care of the lower levels (for level1 we also do level0 and for level2 we do level0 and level1)

We do the L2 renaming below, but first need to make sure the expression has all L1 levels set correctly, in particular in the type.

antlechner · 2018-11-19T18:38:58Z

src/goto-symex/renaming_level.cpp

@@ -48,7 +48,7 @@ void symex_level1t::operator()(ssa_exprt &ssa_expr)

  const irep_idt l0_name = ssa_expr.get_l1_object_identifier();

-  current_namest::const_iterator it = current_names.find(l0_name);
+  auto it = current_names.find(l0_name);


❓ Shouldn't these be const?

antlechner · 2018-11-19T18:41:26Z

src/goto-symex/renaming_level.h

-// level 0 -- threads!
-// renaming built for one particular interleaving
+/// Functor to set the level 0 renaming of SSA expressions.
+/// Level 0 corresponds to threads.


antlechner · 2018-11-19T18:42:01Z

src/goto-symex/renaming_level.h

@@ -18,34 +18,41 @@ Author: Romain Brenguier, [email protected]
 #include <util/irep.h>
 #include <util/ssa_expr.h>

+/// Wrapper for a \c current_names map, which maps each identifier to an SSA


❓ What do we use this map for? Could you explain a bit more about the context of this?

romainbrenguier · 2018-11-20T08:09:24Z

@antlechner ready for rereview

antlechner

LGTM

This was just a wrapper around a map, which was making access to the map heavier without any benefit.

The level is already known when we call this function so the cases can be kept in different functions.

This can avoid confusing with renamings used in other modules.

allredj

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

tautschnig

I think this is good, and probably doesn't affect performance. Given SV-COMP deadlines, right now is either the perfect time to merge this or a very bad time.

romainbrenguier requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel and tautschnig as code owners November 16, 2018 12:35

romainbrenguier force-pushed the refactor/symex-state-levels branch 3 times, most recently from 6efd44c to f08782b Compare November 16, 2018 14:14

allredj reviewed Nov 16, 2018

View reviewed changes

peterschrammel approved these changes Nov 16, 2018

View reviewed changes

romainbrenguier force-pushed the refactor/symex-state-levels branch from f0a40b4 to be65d15 Compare November 19, 2018 09:38

allredj reviewed Nov 19, 2018

View reviewed changes

antlechner reviewed Nov 19, 2018

View reviewed changes

romainbrenguier force-pushed the refactor/symex-state-levels branch 2 times, most recently from 0d6e750 to d679724 Compare November 20, 2018 07:57

antlechner approved these changes Nov 20, 2018

View reviewed changes

romainbrenguier added 13 commits November 22, 2018 06:36

Remove unused typedef

5666c71

Remove typedef used only once

bbadc52

Use auto for iterator type

c6bc894

Use ranged-for instead of iterators

75355f5

Use default for trivial constructors/destructors

9362457

Use ranged-for instead of iterator

141c998

Use ranged-for instead of iterators

2d12c6b

Move renaming_level classes to a new file

b08fad7

Remove unused propagation operator

1b2eca6

Remove unused propogationt::valuest variable

91f7830

Remove definition of propagationt

dd3dcc1

This was just a wrapper around a map, which was making access to the map heavier without any benefit.

Split set_ssa_indices function

de3aa2d

The level is already known when we call this function so the cases can be kept in different functions.

Replace iterator types by auto

96332d6

romainbrenguier added 3 commits November 22, 2018 06:36

Move restore_from definition to cpp file

ada420d

Document renaming_level struct

9d231f7

Rename renaming_levelt to symex_renaming_levelt

b265f7f

This can avoid confusing with renamings used in other modules.

romainbrenguier force-pushed the refactor/symex-state-levels branch from d679724 to b265f7f Compare November 22, 2018 06:37

allredj reviewed Nov 22, 2018

View reviewed changes

tautschnig approved these changes Nov 22, 2018

View reviewed changes

tautschnig merged commit d7c7434 into diffblue:develop Nov 22, 2018

Move symex state levels to a new file #3434

Move symex state levels to a new file #3434

Uh oh!

Conversation

romainbrenguier commented Nov 16, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

antlechner 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!

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!

romainbrenguier commented Nov 20, 2018

Uh oh!

antlechner 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 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

romainbrenguier commented Nov 16, 2018 •

edited

Loading