Additional goto-symex documentation #3975

JohnDumbell · 2019-01-28T12:40:26Z

Added some comments around areas in symex where it wasn't immediately obvious from a relative newcomer to the code about what precisely they did and why it was important (I was the newcomer in this situation). The field rename touches quite a bit of code, but there's nothing in there beside the rename and required clang-format changes.

Feel free to mention if there's another important area that I should try and document, as I mostly focused on areas that would've been useful to me when I originally started looking around.

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.
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).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig

Looks good except for the "loop id" part. It may also be worth linking to the documentation that @johanneskloos has put together about symbolic execution, where the SSA renaming is already being explained (doc/architectural/background-concepts.md).

tautschnig · 2019-01-28T13:03:26Z

src/goto-symex/goto_symex_state.h

  guardt guard{true_exprt{}};
  symex_targett::sourcet source;
  symex_target_equationt *symex_target;

  // we remember all L1 renamings
  std::set<irep_idt> l1_history;

+  // Objects which hold the separate renaming logic for each level that a
+  // symex variable can be on. L0 relates to thread ID, L1 relates to loop ID,


No, L1 is the frame id (the number of times a function has been called).

tautschnig · 2019-01-28T13:03:37Z

src/goto-symex/goto_symex_state.h

+  // symex variable can be on. L0 relates to thread ID, L1 relates to loop ID,
+  // and L2 relates to generation ID.
+  //
+  // If looking at the VCC they are shown as !{threadID}@{loopID}#{generationID}


s/loopID/frameID/

martin-cs

Patch 1, the comment changes, are good and I would support. Patch 2, s/pc/program_counter/ TBH I'm not sure it is worth the churn. Would a comment / description where it is declared suffice? I'm not sure that there are many people who know what a program counter is but don't know that it is often abbreviated to PC.

JohnDumbell · 2019-01-28T15:41:34Z

It helps in reading the code if you don't know the terminology but are relatively comfortable with how code like this should work. Just reading 'pc' as you scan a method gives very little information, but 'program_counter' combined with it being an iterator gives a few solid guesses about what it's doing without going any deeper.

This may be a niche situation though, and once you know the abbreviation you're all good anyway. I have no strong opinions either way - I just felt it helped clarity.

smowton · 2019-01-28T16:20:48Z

src/analyses/dirty.h

@@ -20,6 +20,10 @@ Date: March 2013
 #include <util/invariant.h>
 #include <goto-programs/goto_functions.h>

+/// Dirty variables are ones which have their address taken so we can't
+/// reliably work out where they may be assigned. All variables of this sort
+/// escape their local scope and are also considered shared state in the


Nitpick: usually "escape" would mean live longer than the scope, which isn't true here -- they just might be accessed indirectly and/or by callees

smowton

Some nitpickery otherwise lgtm

smowton · 2019-01-28T16:21:45Z

src/goto-symex/goto_symex_state.h

+/// executes. As we walk over each instruction, state will be updated reflecting
+/// their effects until a branch occurs (such as an if), where parts of the
+/// state will be copied into a \ref goto_statet, stored in a map for later
+/// reference and then merged again once it reaches a control-flow graph


Mention the name of the merge function

smowton · 2019-01-28T16:34:02Z

src/goto-symex/goto_symex_state.h

-  // Map L1 names to (L2) constants
+  // Map L1 names to (L2) constants. Values will be evicted from this map
+  // when they become non-constant. This is used to propagate values that have
+  // been worked out to only have one viable value.


viable -> possible

smowton · 2019-01-28T16:34:48Z

src/goto-symex/goto_symex_state.h

+  //
+  // "constants" can include symbols, but only in the context of an address-of
+  // op (i.e. &x can be propagated), and an address-taken thing should only be
+  // L1. Actual integer literals (for example) aren't symbols, and so aren't


I'd drop the mention of integer literals, it adds more confusion than it removes imo

smowton · 2019-01-28T16:35:42Z

src/goto-symex/goto_symex_state.h

+  ///         guards, dynamic objects and anything not considered thread-local)
+  ///     L1. Applies a suffix giving the current loop iteration or recursive
+  ///         function invocation.
+  ///     L2. Applies a suffix giving the latest generation of this variable.


strike "latest" (writes are always to the latest / fresh generation, but reads can be from past generations, especially in phi nodes)

src/goto-symex/goto_symex_state.h

smowton · 2019-01-28T16:37:41Z

src/goto-symex/goto_symex_state.h

@@ -115,6 +156,10 @@ class goto_symex_statet final
  // do dereferencing
  value_sett value_set;

+  /// Container for data that varies per program point, e.g. the constant
+  /// propagator state, when state needs to branch. This is copied out of
+  /// goto_symex_statet at a control-flow fork and then back into it (at some


back into it at a control-flow merge

Strike "and not the other way around," since we've just said state goes into it and out of it

allredj

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

peterschrammel

Please separate the pc renaming into another PR - that's a breaking change.

JohnDumbell · 2019-01-29T10:52:18Z

@peterschrammel Done.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: c352c90).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98957513
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: 663f6e3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98983334
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: dd518a9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99143224

allredj

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

JohnDumbell self-assigned this Jan 28, 2019

JohnDumbell requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners January 28, 2019 12:40

tautschnig approved these changes Jan 28, 2019

View reviewed changes

tautschnig assigned smowton, peterschrammel and chrisr-diffblue Jan 28, 2019

JohnDumbell force-pushed the jd/doc/symex branch from dc04d7e to 1a9a2ad Compare January 28, 2019 13:42

martin-cs reviewed Jan 28, 2019

View reviewed changes

JohnDumbell force-pushed the jd/doc/symex branch from 1a9a2ad to a16bf20 Compare January 28, 2019 15:49

smowton reviewed Jan 28, 2019

View reviewed changes

smowton approved these changes Jan 28, 2019

View reviewed changes

JohnDumbell force-pushed the jd/doc/symex branch from a16bf20 to 956d240 Compare January 28, 2019 17:13

allredj reviewed Jan 28, 2019

View reviewed changes

peterschrammel requested changes Jan 28, 2019

View reviewed changes

JohnDumbell force-pushed the jd/doc/symex branch from 956d240 to 7e9158d Compare January 29, 2019 10:50

JohnDumbell force-pushed the jd/doc/symex branch from 7e9158d to c352c90 Compare January 29, 2019 11:02

allredj reviewed Jan 29, 2019

View reviewed changes

JohnDumbell force-pushed the jd/doc/symex branch from c352c90 to 663f6e3 Compare January 29, 2019 13:42

allredj reviewed Jan 29, 2019

View reviewed changes

JohnDumbell force-pushed the jd/doc/symex branch from 663f6e3 to dd518a9 Compare January 30, 2019 14:32

allredj reviewed Jan 30, 2019

View reviewed changes

peterschrammel approved these changes Feb 1, 2019

View reviewed changes

Adding additional symex documentation

20a84fb

JohnDumbell force-pushed the jd/doc/symex branch from dd518a9 to 20a84fb Compare February 1, 2019 17:01

allredj reviewed Feb 1, 2019

View reviewed changes

tautschnig merged commit d7bb1d4 into diffblue:develop Feb 2, 2019

Additional goto-symex documentation #3975

Additional goto-symex documentation #3975

Uh oh!

Conversation

JohnDumbell commented Jan 28, 2019

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!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

JohnDumbell commented Jan 28, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

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!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

JohnDumbell commented Jan 29, 2019

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!

Uh oh!

JohnDumbell commented Jan 28, 2019 •

edited

Loading