Refactor in symex #3371

romainbrenguier · 2018-11-12T07:33:18Z

This introduce no functional changes, but should make the code a bit clearer

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

tautschnig

Overall I'd largely agree with the changes. But then it's a lesson as to why PRs with 24 commits are not a good idea: a few commits require further debate or changes, and thus the overall PR is now stalled. Also there are some commits that make changes that crucially depend on changes in the very same PR, and thus those commits ought to be squashed as they could not possibly be independently reverted.

tautschnig · 2018-11-12T07:51:35Z

src/goto-symex/goto_symex.h

@@ -140,6 +130,33 @@ class goto_symext
  bool should_pause_symex;

 protected:
+
+  struct infot {


I'm not sure infot/info is a great name, I'd have chosen configurationt/configuration.

One problem: easily confused with the global config. How about symex_config?

tautschnig · 2018-11-12T07:52:39Z

src/goto-symex/goto_symex.h

+void symex_transition(
+  goto_symext::statet &,
+  goto_programt::const_targett to,
+  bool is_backwards_goto);


Why move them into the global namespace?

The name and type of this function make it hard enough to collide with something else.

tautschnig · 2018-11-12T07:53:54Z

src/goto-symex/goto_symex.h

@@ -463,6 +460,10 @@ class goto_symext
  }
 };

+nondet_symbol_exprt build_symex_nondet(typet &type, unsigned &nondet_count);


Why is this an improvement?

Better static?

It's an improvement because the type makes it clear what is the data used and modified by this function, while before it could have effect on any of the class members.
I'm not sure it can be static because it's used in several cpp files.

smowton · 2018-11-12T15:19:32Z

src/cbmc/symex_bmc.cpp

@@ -105,7 +105,7 @@ void symex_bmct::merge_goto(
    symex_coverage.covered(prev_pc, state.source.pc);
 }

-bool symex_bmct::get_unwind(
+bool symex_bmct::stop_unwind(


should_stop_unwind?

smowton · 2018-11-12T15:20:47Z

src/goto-symex/goto_symex.cpp

    simplify(expr, ns);
 }

-nondet_symbol_exprt goto_symext::build_symex_nondet(typet &type)
+nondet_symbol_exprt build_symex_nondet(typet &type, unsigned &nondet_count)


static? (This and all other functions demoted from class membership)

smowton · 2018-11-12T15:21:49Z

src/goto-symex/goto_symex.h

@@ -115,7 +93,7 @@ class goto_symext
  virtual void resume_symex_from_saved_state(
    const get_goto_functiont &get_goto_function,
    const statet &saved_state,
-    symex_target_equationt *const saved_equation,
+    symex_target_equationt * saved_equation,


Style: IIRC * attached to the var name

smowton · 2018-11-12T15:22:49Z

src/goto-symex/goto_symex.h

@@ -140,6 +130,33 @@ class goto_symext
  bool should_pause_symex;

 protected:
+
+  struct infot {


One problem: easily confused with the global config. How about symex_config?

smowton · 2018-11-12T15:24:18Z

src/goto-symex/goto_symex.h

@@ -463,6 +460,10 @@ class goto_symext
  }
 };

+nondet_symbol_exprt build_symex_nondet(typet &type, unsigned &nondet_count);


Better static?

smowton · 2018-11-12T15:26:46Z

src/goto-symex/symex_goto.cpp

@@ -32,12 +32,10 @@ void goto_symext::symex_goto(statet &state)
  state.rename(new_guard, ns);
  do_simplify(new_guard);

-  if(new_guard.is_false() ||
-     state.guard.is_false())
+  if(new_guard.is_false())


? Unintentional behaviour change? This now happens for new == false, state == false, whereas before it only happened for new == false, state != false

oh yes it should be new_guard.is_false && !state.guard.is_false

smowton · 2018-11-13T09:14:09Z

If you have utility functions that are only intended for use within goto_symext, but where you don't want to give them this because you want to bound their side-effects, how about making them private static functions?

smowton · 2018-11-13T09:16:01Z

For example,

class example {

  int will_be_changed, wont_be_changed;
  static void bounded_effects(int &can_alter) { can_alter++; }

public:

  void public_interface() {
    bounded_effects(will_be_changed);
    // We're sure wont_be_changed is unaffected
  }

};

smowton · 2018-11-13T09:17:12Z

also if there are groups of state that are often altered together, that suggests grouping them in a private inner class

romainbrenguier · 2018-11-13T16:33:45Z

@tautschnig

Overall I'd largely agree with the changes. But then it's a lesson as to why PRs with 24 commits are not a good idea: a few commits require further debate or changes, and thus the overall PR is now stalled. Also there are some commits that make changes that crucially depend on changes in the very same PR, and thus those commits ought to be squashed as they could not possibly be independently reverted.

I've split the PR, and only keep the commits that should be straightforward here. I will make follow up PRs for the ones that may generate discussions.

romainbrenguier · 2018-11-13T16:40:40Z

@smowton

If you have utility functions that are only intended for use within goto_symext, but where you don't want to give them this because you want to bound their side-effects, how about making them private static functions?

That's a relatively good solution, but I think it's not perfect. A private static function could access private static fields. If we want to prevent the function to be used outside of the module, it should be only declared in the goto_symex.cpp file. At the same time there is nothing really wrong with using these functions outside the module, we just want to avoid making it public to lighten the public interface.

tautschnig · 2018-11-14T12:04:12Z

src/goto-symex/goto_symex.h

    unsigned unwind);

  void parameter_assignments(
-    const irep_idt function_identifier,
+    irep_idt function_identifier,


Shouldn't this instead become a const reference (so add the reference, and don't remove the const).

tautschnig · 2018-11-14T12:04:30Z

src/goto-symex/goto_symex.h

    const goto_functionst::goto_functiont &,
    statet &,
    const exprt::operandst &arguments);

  void locality(
-    const irep_idt function_identifier,
+    irep_idt function_identifier,


As above, make a const reference.

tautschnig · 2018-11-14T12:05:11Z

src/goto-symex/goto_symex.h

-    const get_goto_functiont &get_goto_function,
-    const irep_idt &function_identifier,
-    goto_programt::const_targett first,
-    goto_programt::const_targett limit);


This should be squash with the preceding commit.

tautschnig · 2018-11-14T12:06:26Z

src/goto-symex/goto_symex.h

@@ -171,8 +171,6 @@ class goto_symext
  const bool allow_pointer_unsoundness;

 public:
-  // these bypass the target maps
-  virtual void symex_step_goto(statet &, bool taken);


Maybe the commit message could be made to include the names of functions being removed? These have likely been used elsewhere (Satabs comes to mind), and if we ever want to resurrect them, the git history is vital.

tautschnig · 2018-11-14T12:08:29Z

src/goto-symex/symex_goto.cpp

@@ -82,10 +82,8 @@ void goto_symext::symex_goto(statet &state)
      frame.loop_iterations[goto_programt::loop_id(*state.source.pc)].count;
    unwind++;

-    // continue unwinding?


I would recommend squashing with the prior commit. Simple test: would reverting either of these commits in isolation be meaningful? I don't think so.

tautschnig · 2018-11-14T12:09:19Z

src/pointer-analysis/value_set_dereference.h

-  void offset_sum(
-    exprt &dest,
-    const exprt &offset) const;
-


Ok, but this doesn't quite fit what the title of the PR says?!

Why not? It doesn't introduce any functional change.

If the PR title says "symex" and I find this change without much of a comment then I have to call it out as a reviewer: based on the information provided in the title, I must assume that it was accidentally included.

Oh right I see, sorry, I will be more careful next time

tautschnig · 2018-11-14T12:10:14Z

src/goto-symex/symex_builtin_functions.cpp

-    exprt nondet = build_symex_nondet(object_type);
-    code_assignt assignment(value_symbol.symbol_expr(), nondet);
+    const exprt nondet = build_symex_nondet(object_type, nondet_count);
+    const code_assignt assignment(value_symbol.symbol_expr(), nondet);


I don't think this change works in here, given the comments that have been removed from the PR.

yes thanks, it wasn't caught while rebasing.

This is prohibited.

Reduce the number of negations

Was not helping making the code clearer

More clearly describe what the return value represents.

This is clearer for expressing that the method override that of the base class. This also make comments about overloading unecessary

Makes it clearer that the methods override that of the base class.

romainbrenguier · 2018-11-16T07:57:08Z

@tautschnig I think I addressed all your comments

allredj

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

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

romainbrenguier force-pushed the refactor/symex-part1 branch from 8c2c3a1 to 908d29b Compare November 12, 2018 07:34

tautschnig requested changes Nov 12, 2018

View reviewed changes

smowton reviewed Nov 12, 2018

View reviewed changes

romainbrenguier force-pushed the refactor/symex-part1 branch from 908d29b to 93fa742 Compare November 13, 2018 09:08

romainbrenguier force-pushed the refactor/symex-part1 branch from 93fa742 to 003f41d Compare November 13, 2018 16:31

smowton approved these changes Nov 14, 2018

View reviewed changes

tautschnig reviewed Nov 14, 2018

View reviewed changes

romainbrenguier force-pushed the refactor/symex-part1 branch from 003f41d to 6165270 Compare November 15, 2018 14:46

romainbrenguier added 11 commits November 15, 2018 14:51

Remove declaration of unimplemented functions

3b24f35

Use default for trivial destructor

0d17753

Remove unused function symex_from_entry_point_of

1b22eae

Remove non-reference const in declarations

0fed6c8

Remove unused function symex_instruction_range

6f034fa

Remove unused function symex_instruction_range

5490735

Remove unused function symex_step_goto

d74f55d

Remove default argument on virtual method

1b78ec5

This is prohibited.

Use backward instead of forward

da94813

Reduce the number of negations

Remove intermediary expression variable

c0bc638

Was not helping making the code clearer

Rename method to should_stop_unwind

529fbc9

More clearly describe what the return value represents.

romainbrenguier added 6 commits November 15, 2018 14:51

Document pc

9e049ba

Use override instead of virtual

0157d77

This is clearer for expressing that the method override that of the base class. This also make comments about overloading unecessary

Remove unused field

3598f68

Add missing const

584db18

Use override instead of virtual

91b23f4

Makes it clearer that the methods override that of the base class.

Remove unused forward declaration

1f9aa83

romainbrenguier force-pushed the refactor/symex-part1 branch 2 times, most recently from 1a67555 to 1f9aa83 Compare November 16, 2018 07:56

tautschnig approved these changes Nov 16, 2018

View reviewed changes

tautschnig assigned romainbrenguier Nov 16, 2018

allredj reviewed Nov 16, 2018

View reviewed changes

romainbrenguier merged commit 10edd29 into diffblue:develop Nov 16, 2018

romainbrenguier deleted the refactor/symex-part1 branch November 16, 2018 10:10

Refactor in symex #3371

Refactor in symex #3371

Uh oh!

Conversation

romainbrenguier commented Nov 12, 2018

Uh oh!

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

smowton commented Nov 13, 2018

Uh oh!

smowton commented Nov 13, 2018

Uh oh!

smowton commented Nov 13, 2018

Uh oh!

romainbrenguier commented Nov 13, 2018

Uh oh!

romainbrenguier commented Nov 13, 2018

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 16, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!