Refactoring in goto_symex #3988

romainbrenguier · 2019-01-29T15:08:13Z

This are small refactoring commits in preparation for #3986

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.
[na] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

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

martin-cs

The pointer-analysis changes seem fine. I am unsure about the value of moving to the functional "lots of small static function" from the OO "protected utility functions". This seems an issue of style and one that risks flip-flopping depending on who is working on the code. I'm not sure here is the place to have that discussion.

martin-cs · 2019-01-29T18:18:06Z

src/goto-symex/goto_symex_state.cpp

@@ -690,18 +690,15 @@ void goto_symex_statet::rename(
    }
  }

-  if(type.id()==ID_array)
+  if(const auto &array_type = type_try_dynamic_cast<array_typet>(type))


I guess this fits more with the current way of doing things, so, yes.

I am no fan -- this doesn't improve execution speeds, but is less readable.

It provides extra validation beyond just checking the id, which depends on the type you are casting to

I am in favour of using type_try_dynamic_cast, because it means that you only need to know the name of the type you want to cast to, you don't need to know that the .id() is supposed to be ID_array for an array_typet, in order to do the cast. It also reduces the likely-hood of mismatches between the check and the cast. There is little chance of checking for ID_array and casting to bool_typet, when both operations are done by the try_cast. I would however be in favour of renaming type_try_dynamic_cast to something less verbose.

martin-cs · 2019-01-29T18:18:21Z

src/goto-symex/symex_start_thread.cpp

-      UNREACHABLE;
+    auto emplace_result = state.level1.current_names.emplace(
+      lhs.get_l1_object_identifier(), std::make_pair(lhs, 0));
+    CHECK_RETURN(emplace_result.second);


Definitely.

peterschrammel

I'm in favour of small static functions for a class that is not going to be inherited from. It makes the class interface easier to read (even if it is a drop in the ocean in goto-symex).

tautschnig · 2019-01-30T07:13:12Z

src/goto-symex/goto_symex_state.cpp

+static void set_l2_indices(
+  symex_level0t level0,
+  symex_level1t level1,
+  symex_level2t level2,


Can we please pass all these as const references? That will also show that their operator() should have been marked const (or maybe even static?), which will necessitate another commit to be added.

Done and I've marked the operator const for symex_level1t, and replaced symex_level0t by a function so it doesn't need to be passed as an argument here.

tautschnig · 2019-01-30T07:16:31Z

src/goto-symex/goto_symex_state.cpp

+/// When the type of the operands of a `with_exprt` or `if_exprt` have been
+/// renamed they could end up being different from that of the expression. We
+/// fix that by propagating the type of its operands to \p expr.
+static void fix_type(exprt &expr)


I do note that I consider this a workaround for a genuine bug, and I'd be curious to see what happens if instead of replacing we actually checked that the types already are consistent?

This should really not be necessary. We need to get rid of that renaming.

Indeed it doesn't seem necessary. I've tested adding a invariant that checks that this does not do anything and all tests in regression/cbmc passed so there doesn't seem to be a bug we need to workaround. I will remove that part.

As a matter of procedure, would you mind just dropping the commit from this PR, and create a separate PR that removes that code and replaces it by the invariant you've played with? Thank you!!

made the PR there: #3993 and dropped the commit from here ~~rebased this one on it~~

tautschnig · 2019-01-30T07:23:54Z

src/goto-symex/symex_dead.cpp

-    else
-      rhs=exprt(ID_invalid);
+    exprt rhs = [&]() -> exprt {
+      if(auto failed = get_failed_symbol(to_symbol_expr(code.symbol()), ns))


The to_symbol_expr is actually unnecessary, code.symbol() already returns a symbol_exprt.

kroening

This needs another go -- I am in particularly concerned about the "renaming fix".

kroening · 2019-01-30T08:30:45Z

src/goto-symex/goto_symex_state.cpp

+    return ns.lookup(to_struct_tag_type(type)).type;
+  return {};
+}
+


This should not be necessary.

If you mean "renaming is never needed for tagged types," I think that's untrue when we have structs with a flexible array member to rename.

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

src/goto-symex/goto_symex_state.cpp

@@ -27,6 +27,14 @@ Author: Daniel Kroening, [email protected]

 static void get_l1_name(exprt &expr);

+static void set_l2_indices(
+  symex_level0t level0,


Commented on the other PR, but can you explain the by-value passing here?

the reference was omitted by mistake, but this reveals that this level0 is actually constant, I going to replace the symex_level0t by a function

allredj

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

tautschnig · 2019-01-30T15:41:17Z

@kroening Is this looking better?

allredj

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

romainbrenguier · 2019-02-11T13:45:14Z

@kroening

I don't see value in the static function refactoring; these do remind me too much of 90ies PASCAL.

I agree with @LAJW comment on that, plus it is generally recommended to make functions non-member whenever possible
(see http://www.drdobbs.com/cpp/how-non-member-functions-improve-encapsu/184401197)
and it makes the other changes I want easier.

I am not a fan of the type_try_dynamic_cast idiom. At the very least it should be renamed, as 'dynamic_cast' has very specific meaning in C++.

See @NathanJPhillips comment on that, and renaming it would be outside the scope of this PR.

Two branches get replaced by a lambda; for most this reduces readability.

I removed these two lambda's.

The class hierarchy for the renaming levels is very intentional. I understand that the one that's replaced is trivial, but there's a point to the pattern.

I removed this commit, though I don't see the value of this, the inheritance is not used, and it initializes a map that is never used.

allredj

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

peterschrammel · 2019-02-13T10:02:47Z

I don't see value in the static function refactoring; these do remind me too much of 90ies PASCAL.

That could be considered a matter of taste. But, still, there are clear advantages of using static functions:

it declutters class declarations, makes them shorter and easier to read, and reduces the size of header files, speeding up compilation.
it makes side effects explicit, making the code easier to understand, change and refactor (and trivial to refactor for reuse).

allredj

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

smowton · 2019-02-14T11:04:58Z

src/goto-symex/goto_symex_state.cpp

@@ -231,32 +239,41 @@ void goto_symex_statet::assignment(
  #endif
 }

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


This can surely be const

smowton · 2019-02-14T11:08:32Z

src/goto-symex/goto_symex_state.cpp

-    rename(type, l1_identifier, ns, level);
-  }
-  else if(type.id() == ID_union_tag)
+  else if(const auto &followed_type = type_of_symbol_or_tag(type, ns))


This isn't a reference

smowton · 2019-02-14T11:12:06Z

src/goto-symex/goto_symex_state.cpp

+/// Return the type corresponding to a symbol or tag. Empty optional if \p type
+/// is neither a symbol or a tag.
+static optionalt<typet>
+type_of_symbol_or_tag(const typet &type, const namespacet &ns)


I think you could replace all this with type = ns.follow(type);, at the top of rename_type, as that's a no-op for non-tags.

smowton · 2019-02-14T11:12:56Z

src/goto-symex/goto_symex_state.cpp

+    return ns.lookup(to_struct_tag_type(type)).type;
+  return {};
+}
+


If you mean "renaming is never needed for tagged types," I think that's untrue when we have structs with a flexible array member to rename.

smowton · 2019-02-14T11:21:35Z

If I were you I'd drop the static-ifcation and have the try_dynamic_cast vs. id() == fight elsewhere, that way this PR will be style-war free and easier to merge :)

romainbrenguier · 2019-02-14T16:16:12Z

@smowton

If I were you I'd drop the static-ifcation and have the try_dynamic_cast vs. id() == fight elsewhere, that way this PR will be style-war free and easier to merge :)

I've dropped the dynamic_cast change, and applied your suggestion for the rename typet, but making the functions static is the main purpose of this PR.

tautschnig · 2019-02-14T16:35:25Z

src/goto-symex/goto_symex_state.cpp

@@ -688,6 +688,8 @@ void goto_symex_statet::rename(
  const namespacet &ns,
  levelt level)
 {
+  type = ns.follow(type);


I'm not even sure that compiles, but even when you make it compile: I think it should be done after requires_renaming to make sure we don't unnecessarily break sharing.

tautschnig · 2019-02-14T16:37:15Z

src/goto-symex/symex_start_thread.cpp

-                       std::make_pair(lhs, 0))).second)
-      UNREACHABLE;
+    auto emplace_result = state.level1.current_names.emplace(
+      lhs.get_l1_object_identifier(), std::make_pair(lhs, 0));


Until we have C++17 use:

auto emplace_result = state.level1.current_names.emplace( std::piecewise_construct, std::forward_as_tuple(lhs.get_l1_object_identifier()), std::forward_as_tuple(lhs, 0));

to avoid even constructing the second pair if the key already exists.

allredj

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

Make obvious the operator doesn't change the state of the object.

allredj

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

kroening · 2019-02-19T14:36:57Z

src/goto-symex/goto_symex_state.cpp

@@ -675,6 +675,8 @@ void goto_symex_statet::rename(
  if(!requires_renaming(type, ns))
    return; // no action

+  type = ns.follow(type);
+


Is that not expanding some tag types?

Intentionally so, with the idea to replace the expansion below (lines 728ff have been removed). But I might be missing something.

Ok -- I'd move below the following if block, and then add a comment such as
// expand struct and union tag types

smowton · 2019-02-19T16:27:04Z

@romainbrenguier I talked to @kroening on Slack, he said this is ok once the ns.follow is moved below the if(...) immediately below it that may return the previously renamed type and therefore render the follow pointless.

This avoids a disjunction of cases for the different type of tags and makes the rename function simpler.

Using emplace avoids a call to make_pair, and CHECK_RETURN is more adapted to the situation were we check the return value of insert/emplace.

This is more precise on the type of object returned.

romainbrenguier · 2019-02-20T06:55:17Z

@smowton @kroening done

kroening · 2019-02-20T09:28:32Z

@romainbrenguier Many thanks for the extra effort!

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

romainbrenguier force-pushed the refactor/symex-rename1 branch 3 times, most recently from 4701b68 to c3bede4 Compare January 29, 2019 16:04

allredj reviewed Jan 29, 2019

View reviewed changes

martin-cs reviewed Jan 29, 2019

View reviewed changes

peterschrammel approved these changes Jan 29, 2019

View reviewed changes

tautschnig reviewed Jan 30, 2019

View reviewed changes

tautschnig assigned romainbrenguier Jan 30, 2019

kroening requested changes Jan 30, 2019

View reviewed changes

kroening reviewed Jan 30, 2019

View reviewed changes

smowton reviewed Jan 30, 2019

View reviewed changes

romainbrenguier force-pushed the refactor/symex-rename1 branch 2 times, most recently from f5d3a86 to 466b69a Compare January 30, 2019 11:31

allredj reviewed Jan 30, 2019

View reviewed changes

romainbrenguier force-pushed the refactor/symex-rename1 branch 3 times, most recently from 51d7934 to c4d9ca4 Compare January 30, 2019 15:34

tautschnig assigned kroening Jan 30, 2019

romainbrenguier force-pushed the refactor/symex-rename1 branch from c4d9ca4 to 02c7e5b Compare January 30, 2019 16:50

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

allredj reviewed Jan 30, 2019

View reviewed changes

romainbrenguier force-pushed the refactor/symex-rename1 branch from 02c7e5b to ce7a898 Compare January 31, 2019 07:44

romainbrenguier force-pushed the refactor/symex-rename1 branch from b55e0aa to beb87d3 Compare February 11, 2019 13:35

allredj reviewed Feb 11, 2019

View reviewed changes

romainbrenguier force-pushed the refactor/symex-rename1 branch from beb87d3 to 569ecb6 Compare February 13, 2019 11:36

allredj reviewed Feb 13, 2019

View reviewed changes

smowton reviewed Feb 14, 2019

View reviewed changes

romainbrenguier force-pushed the refactor/symex-rename1 branch from 569ecb6 to 9d0dea9 Compare February 14, 2019 16:14

romainbrenguier force-pushed the refactor/symex-rename1 branch from 9d0dea9 to 19805b7 Compare February 14, 2019 16:32

tautschnig approved these changes Feb 14, 2019

View reviewed changes

romainbrenguier force-pushed the refactor/symex-rename1 branch from 19805b7 to 5e95d69 Compare February 14, 2019 16:48

allredj reviewed Feb 14, 2019

View reviewed changes

allredj reviewed Feb 15, 2019

View reviewed changes

Mark symex_level0 and level1 operator() const

69d4c5d

Make obvious the operator doesn't change the state of the object.

romainbrenguier force-pushed the refactor/symex-rename1 branch from 5e95d69 to 6bd85cf Compare February 18, 2019 12:17

allredj reviewed Feb 18, 2019

View reviewed changes

smowton approved these changes Feb 19, 2019

View reviewed changes

kroening reviewed Feb 19, 2019

View reviewed changes

romainbrenguier added 3 commits February 20, 2019 06:53

Use namespace follow on type in rename(typet)

eebe605

This avoids a disjunction of cases for the different type of tags and makes the rename function simpler.

Replace insert by emplace and UNREACHABLE by CHECK_RETURN

9945782

Using emplace avoids a call to make_pair, and CHECK_RETURN is more adapted to the situation were we check the return value of insert/emplace.

Make get_failed_symbol return optional symbol_exprt

2c74ebe

This is more precise on the type of object returned.

romainbrenguier force-pushed the refactor/symex-rename1 branch from 6bd85cf to 2c74ebe Compare February 20, 2019 06:54

kroening approved these changes Feb 20, 2019

View reviewed changes

romainbrenguier merged commit 55eec59 into diffblue:develop Feb 20, 2019

romainbrenguier deleted the refactor/symex-rename1 branch February 20, 2019 09:37

Refactoring in goto_symex #3988

Refactoring in goto_symex #3988

Conversation

romainbrenguier commented Jan 29, 2019 • edited Loading

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel 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

Choose a reason for hiding this comment

romainbrenguier 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

kroening 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

allredj left a comment

Choose a reason for hiding this comment

tautschnig commented Jan 30, 2019

allredj left a comment

Choose a reason for hiding this comment

romainbrenguier commented Feb 11, 2019

allredj left a comment

Choose a reason for hiding this comment

peterschrammel commented Feb 13, 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

smowton commented Feb 14, 2019

romainbrenguier commented Feb 14, 2019

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

allredj left a comment

Choose a reason for hiding this comment

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

smowton commented Feb 19, 2019

romainbrenguier commented Feb 20, 2019

kroening commented Feb 20, 2019

romainbrenguier commented Jan 29, 2019 •

edited

Loading

romainbrenguier Jan 30, 2019 •

edited

Loading