goto symex member cleanup #3221

karkhaz · 2018-10-23T12:39:54Z

This patch-set aims to const-ify every member of goto_symext and related classes that only serve as a cache for an optionst option, and to make those members protected if appropriate. The fact that they were public and/or non-const was rather confusing.

The first commit in the patch-set allows to set options of an optionst while it is being constructed, so that other classes can read from the optionst object while they are being constructed. This means that we no longer need to do many of the symex.member = options.get_option("member"); inside the bodies of a constructor, instead doing member(options.get_option("member")) inside the constructor for goto_symext and therefore making member const and protected.

allredj

Passed Diffblue compatibility checks (cbmc commit: 0c909fd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88847152

smowton · 2018-10-24T08:53:51Z

src/goto-instrument/accelerate/scratch_program.h

@@ -43,16 +43,17 @@ class scratch_programt:public goto_programt
      ns(symbol_table, symex_symbol_table),
      equation(),
      path_storage(),
-      options(),
+      options(
+        {{"propagation", true},


Why the new propagation setting?

smowton · 2018-10-24T09:09:45Z

So symex currently has a weird mixture of directly querying the optionst it has stored by reference and querying it in the constructor and storing the results in fields (or previously, having its users do that for it). I suggest we should decide on one style and do that consistently -- personally I'd favour removing the const optionst &options from goto_symext entirely and querying and storing every option we're interested in during the constructor. That will lead to the more intuitive behaviour that the object is configured at construction time and subsequent changes to options will not affect it.

smowton · 2018-10-24T09:12:23Z

Also I'm not a fan of the new constructor for optionst because it's awkward to specify e.g. a single string option (optionst({}, {}, {}, {"hello", "world"})). Instead how about constructing the scratch_programt options using a static function, so the initializer looks something like options(get_default_options())?

allredj

Passed Diffblue compatibility checks (cbmc commit: 56b4872).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/89037402

karkhaz · 2018-10-24T23:30:23Z

@smowton thanks for the comments, agreed with all of them. I've reverted the optionst constructor and replaced it with a commit to construct scratch_programt's optionst with a static function. I've also added a new commit which introduces a bunch of members to goto_symext, caching the remaining options that it was using.

I notice that clang-format errors now cause the CI to fail. Is the preferred way to apply clang-format to have one single commit for the whole patch series as I've done above, or is it better to apply clang-format on each commit? CODING_STANDARD.md doesn't take a strong stance on the issue...

smowton

Change the static default_options into a local, otherwise LGTM, thanks for the improvements! re: clang-format it's best to do it per commit if possible, since that results in a more accurate git blame

smowton · 2018-10-25T08:17:22Z

src/goto-instrument/accelerate/scratch_program.cpp

@@ -203,3 +203,10 @@ void scratch_programt::append_loop(
    }
  }
 }
+
+optionst scratch_programt::default_options;


Just declare this as a local in get_default_options

karkhaz · 2018-10-25T10:37:11Z

Thanks, I did as you asked and applied the clang-format changes to the right commits. (I've also squashed the clang-format changes into its commit in #3220).

allredj

Passed Diffblue compatibility checks (cbmc commit: 2fc5dab).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/89137416

This is so that the optionst object that gets passed to scratch_programt::symex has the right options for initializing the symex object.

This member is never written to.

This member is never written to and serves merely as a cache for a front-end option, so this commit makes it const and protected.

This goto_symext member is never written to and serves merely as a cache for a front-end option, so this commit makes it const and protected.

This member is never written to and serves merely as a cache for a front-end option, so this commit makes it const.

goto_symext no longer has a reference to a optionst object. Instead, the options that goto_symext needs to read from an optionst are read during construction and cached in const members.

allredj

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

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

This looks good. Also, I have manually checked that this causes no trouble with test-gen. Compatibility warnings are due to some previous failure and can be disregarded.

chrisr-diffblue

That looks a lot cleaner to me - and thanks for constructing an easy-to-review PR :-)

karkhaz · 2018-11-05T14:41:33Z

@chrisr-diffblue I'm trying to accumulate good karma to cash in for a 4k line PR that is on the horizon...:upside_down_face:

karkhaz requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners October 23, 2018 12:39

allredj reviewed Oct 23, 2018

View reviewed changes

smowton reviewed Oct 24, 2018

View reviewed changes

karkhaz force-pushed the kk-goto-symex-member-cleanup branch from 0c909fd to 3a9711d Compare October 24, 2018 14:11

allredj reviewed Oct 24, 2018

View reviewed changes

smowton approved these changes Oct 25, 2018

View reviewed changes

karkhaz force-pushed the kk-goto-symex-member-cleanup branch from 56b4872 to 2fc5dab Compare October 25, 2018 09:39

smowton assigned tautschnig, peterschrammel and kroening Oct 25, 2018

allredj reviewed Oct 25, 2018

View reviewed changes

tautschnig approved these changes Oct 29, 2018

View reviewed changes

tautschnig assigned martin-cs and chrisr-diffblue and unassigned tautschnig and kroening Oct 29, 2018

karkhaz added 4 commits October 30, 2018 08:41

Set scratch_programt optionst on construction

eb3a9f0

This is so that the optionst object that gets passed to scratch_programt::symex has the right options for initializing the symex object.

constify goto_symext::guard_identifier

1b86931

This member is never written to.

const & protect goto_symext::constant_propagation

ddf416f

This member is never written to and serves merely as a cache for a front-end option, so this commit makes it const and protected.

const and protect self_loops_to_assumptions

698aebd

This goto_symext member is never written to and serves merely as a cache for a front-end option, so this commit makes it const and protected.

constify symex_bmct::record_coverage

2ef8499

This member is never written to and serves merely as a cache for a front-end option, so this commit makes it const.

karkhaz force-pushed the kk-goto-symex-member-cleanup branch from 2fc5dab to 65e017d Compare October 30, 2018 08:53

Replace goto_symext::options with const members

622940c

goto_symext no longer has a reference to a optionst object. Instead, the options that goto_symext needs to read from an optionst are read during construction and cached in const members.

karkhaz force-pushed the kk-goto-symex-member-cleanup branch from 65e017d to 622940c Compare October 30, 2018 08:55

allredj reviewed Oct 30, 2018

View reviewed changes

allredj approved these changes Oct 30, 2018

View reviewed changes

chrisr-diffblue approved these changes Nov 5, 2018

View reviewed changes

chrisr-diffblue removed their assignment Nov 5, 2018

tautschnig merged commit 51236f2 into diffblue:develop Nov 5, 2018

karkhaz deleted the kk-goto-symex-member-cleanup branch November 5, 2018 14:38

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

goto symex member cleanup #3221

goto symex member cleanup #3221

Uh oh!

karkhaz commented Oct 23, 2018

Uh oh!

allredj left a comment

Uh oh!

smowton Oct 24, 2018

Uh oh!

smowton commented Oct 24, 2018

Uh oh!

smowton commented Oct 24, 2018

Uh oh!

allredj left a comment

Uh oh!

karkhaz commented Oct 24, 2018

Uh oh!

smowton left a comment

Uh oh!

smowton Oct 25, 2018

Uh oh!

karkhaz commented Oct 25, 2018

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

chrisr-diffblue left a comment

Uh oh!

karkhaz commented Nov 5, 2018

Uh oh!

Uh oh!

goto symex member cleanup #3221

goto symex member cleanup #3221

Uh oh!

Conversation

karkhaz commented Oct 23, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton Oct 24, 2018

Choose a reason for hiding this comment

Uh oh!

smowton commented Oct 24, 2018

Uh oh!

smowton commented Oct 24, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

karkhaz commented Oct 24, 2018

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

smowton Oct 25, 2018

Choose a reason for hiding this comment

Uh oh!

karkhaz commented Oct 25, 2018

Uh oh!

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

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

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

karkhaz commented Nov 5, 2018

Uh oh!

Uh oh!