Class and function documentation for goto-symex-target [DOC-79] #3393

xbauch · 2018-11-13T15:25:54Z

Adding class and function documentation to goto-symex/symex_target. {h,cpp} and goto-symex/symex_target_equation.{h,cpp}.

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.
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.

majakusber

Generally looks good, a lot of useful docs added! I have mostly minor suggestions for formatting (sorry for all the fruits 🙂 first I wanted to mark all the places for the recurring comments with them but it's too much), here is a summary:

use imperative mood in function docs,
indent the overflowing lines by two spaces for better readability,
move docs of interface functions to headers,
I would suggest calling the guards preconditions and reformulating the sentence a bit (see 🍓).
There are few other comments but nothing too big.

src/goto-symex/symex_target.cpp

src/goto-symex/symex_target.h

src/goto-symex/symex_assign.cpp

majakusber · 2018-11-13T16:25:20Z

src/goto-symex/symex_target_equation.cpp

+/// \param guard: condition to take this read event
+/// \param ssa_rhs: variable to be read from
+/// \param atomic_section_id: ID of the atomic section in which this read
+/// takes place


⛏️ Indent by 2 spaces for better readability. 🍌

Done, and hopefully all the bananas.

Thanks, I think only one space is added now but that's probably enough 🙂 (maybe you ran into the same mistake I sometimes make - hitting tab right after the /// results in adding one space only but hitting tab at the place where text starts one space after the /// indents by 2 spaces then)

src/goto-symex/symex_target_equation.cpp

src/goto-symex/symex_target_equation.h

allredj

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

peterschrammel · 2018-11-13T16:06:48Z

src/goto-symex/symex_assign.cpp

@@ -91,6 +91,11 @@ void goto_symext::symex_assign(
  }
 }

+/// Store the \c what expression as the first unassigned 0th operand of the


I personally find what easier to read.

How about using \p to also make clear this refers to a parameter (and not just some arbitrary code)?

Done (throughout the PR).

A swapped backslash-c with back-ticks throughout the PR.

peterschrammel · 2018-11-13T16:07:12Z

src/goto-symex/symex_assign.cpp

@@ -91,6 +91,11 @@ void goto_symext::symex_assign(
  }
 }

+/// Store the \c what expression as the first unassigned 0th operand of the
+/// \c lhs.
+/// \param lhs non-symbol pointed-to expression


lhs: Non-... according to coding style

Done, here and elsewhere.

peterschrammel · 2018-11-13T16:07:32Z

src/goto-symex/symex_assign.cpp

+/// \c lhs.
+/// \param lhs non-symbol pointed-to expression
+/// \param what the expression to be added to the \c lhs
+/// \return the resulting expression


\return The... according to coding style

peterschrammel · 2018-11-13T16:10:28Z

src/goto-symex/symex_target.h

+  /// \param guard: condition to take this read event
+  /// \param ssa_rhs: variable to be read from
+  /// \param atomic_section_id: ID of the atomic section in which this read
+  /// takes place


It would increase readability to indent here.

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

src/goto-symex/symex_assign.cpp

@@ -91,6 +91,11 @@ void goto_symext::symex_assign(
  }
 }

+/// Store the \c what expression as the first unassigned 0th operand of the


How about using \p to also make clear this refers to a parameter (and not just some arbitrary code)?

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

src/goto-symex/symex_target.h

@@ -17,6 +17,9 @@ Author: Daniel Kroening, [email protected]
 class ssa_exprt;
 class symbol_exprt;

+/// Base class for symbolic execution. Intended as a position identifier in the


What is a "position identifier?"

I wasn't sure if we have an established term to refer to program location. To the best of my understanding symex_targett has a similar purpose to const_target which is an iterator into a list of instructions. I tried rewording the description a bit.

Oh, I see, actually a symex_targett is very different (although by now I'm not even sure it is a meaningful interface anymore, because we leak out symex_target_equationt all over the place). A symex_targett is the interface of the target container for symbolic execution to record its symbolic steps into. As far as I am aware, symex_target_equationt is the only implementation of that interface.

I hope you won't mind if I quote/paraphrase the above for the description.

symex_target_equationt is the only implementation of that interface.

Yes, afaik.

allredj

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

xbauch · 2018-11-15T15:47:52Z

I think I've addressed all the @svorenova @peterschrammel and @tautschnig comments.

majakusber

Looks good to go, I just have one question about four functions without doc. But because this is already much better than what it was before I won't block the merge.

majakusber · 2018-11-15T16:35:13Z

src/goto-symex/symex_target.h

+  /// \param cond: Condition represented by this constraint
+  /// \param msg: The message associated with this constraint
+  /// \param source: Pointer to location in the input GOTO program of this
+  ///  constraint


❓ I asked this before but it may have gotten lost - why are the last four functions below not documented?

allredj

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

peterschrammel · 2018-11-15T22:42:07Z

@xbauch, can you squash the commits please?

xbauch · 2018-11-16T08:39:27Z

Squashed.

allredj

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

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: e399467).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93174124
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 · 2018-12-01T09:03:13Z

@xbauch Could you please rebase to make sure the bot is re-triggered as the past failure was likely caused by unrelated problems?

tautschnig

A couple of suggestions and requests for changes below, but nothing blocking. The biggest item is using \copydoc to avoid duplicating the same text when functions are just implementations of an interface. In those cases please make sure the documentation genuinely was the same, else merge any missing bits into the documentation of the interface.

tautschnig · 2018-12-01T11:41:25Z

src/goto-symex/goto_symex.h

+  /// Store the \p what expression as the first unassigned 0th operand of the
+  /// \p lhs.
+  /// \param lhs: Non-symbol pointed-to expression
+  /// \param what: The expression to be added to the \c lhs


Suggested change

/// \param what: The expression to be added to the \c lhs

/// \param what: The expression to be added to the \p lhs

tautschnig · 2018-12-01T11:41:53Z

src/goto-symex/goto_symex.h

@@ -391,6 +391,11 @@ class goto_symext
    guardt &,
    assignment_typet);

+  /// Store the \p what expression as the first unassigned 0th operand of the


What is an "unassigned" operand?

tautschnig · 2018-12-01T11:42:30Z

src/goto-symex/symex_target.h

@@ -17,6 +17,9 @@ Author: Daniel Kroening, [email protected]
 class ssa_exprt;
 class symbol_exprt;

+/// The interface of the target _container_ for symbolic execution to record its
+/// symbolic steps into. Presently, symex_target_equationt is the only


Suggested change

/// symbolic steps into. Presently, symex_target_equationt is the only

/// symbolic steps into. Presently, \ref symex_target_equationt is the only

tautschnig · 2018-12-01T11:50:05Z

src/goto-symex/symex_target.h

@@ -26,6 +29,9 @@ class symex_targett

  virtual ~symex_targett() { }

+  /// Identifies source in the context of symbolic execution. Thread number


We might have to rethink the naming here - this really is a generalisation of the program counter with some additional context. But that's not for this PR.

tautschnig · 2018-12-01T11:51:12Z

src/goto-symex/symex_target.h

@@ -65,21 +71,46 @@ class symex_targett
    GUARD,
  };

-  // read event
+  /// Read from a shared variable `ssa_rhs` (which will thus become a


Suggested change

/// Read from a shared variable `ssa_rhs` (which will thus become a

/// Read from a shared variable \p ssa_rhs (which will thus become a

tautschnig · 2018-12-01T11:53:37Z

src/goto-symex/symex_target.h

+  /// \param guard: Precondition for this read event
+  /// \param ssa_rhs: Variable to be read from
+  /// \param atomic_section_id: ID of the atomic section in which this read
+  ///  takes place


Suggested change

/// takes place

/// takes place (if any)

tautschnig · 2018-12-01T11:56:04Z

src/goto-symex/symex_target.h

  virtual void shared_read(
    const exprt &guard,
    const ssa_exprt &ssa_rhs,
    unsigned atomic_section_id,
    const sourcet &source)=0;

-  // write event
+  /// Write to a shared variable `ssa_rhs` (which will thus become a
+  /// left-hand side as well): we effectively assign a value from this thread


As is done in the implementation, please rename "ssa_rhs" to "ssa_object" and then remove the parts in parentheses - this always was a left-hand side, it's not actually becoming one here.

tautschnig · 2018-12-01T11:56:17Z

src/goto-symex/symex_target.h

+  /// \param guard: Precondition for this write event
+  /// \param ssa_rhs: Variable to be written to
+  /// \param atomic_section_id: ID of the atomic section in which this write
+  ///  takes place


Suggested change

/// takes place

/// takes place (if any)

tautschnig · 2018-12-01T11:58:02Z

src/goto-symex/symex_target_equation.h

@@ -29,26 +29,55 @@ class decision_proceduret;
 class namespacet;
 class prop_convt;

+/// Inheriting the interface of symex_targett this class represents the SSA
+/// form of the input program as a list of SSA_stept. It further extends the


Suggested change

/// form of the input program as a list of SSA_stept. It further extends the

/// form of the input program as a list of \ref SSA_stept. It further extends the

tautschnig · 2018-12-01T11:58:46Z

src/goto-symex/symex_target_equation.h

+  /// \param ssa_object: Variable to be read from
+  /// \param atomic_section_id: ID of the atomic section in which this read
+  ///  takes place
+  /// \param source: Pointer to location in the input GOTO program of this read


Here and below: use \copydoc

1) Document the symex_target interface. 2) Document the symex_target_equation -- Mostly SSA_stept and the transformations into it.

allredj

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

xbauch requested review from kroening, peterschrammel and tautschnig as code owners November 13, 2018 15:25

majakusber reviewed Nov 13, 2018

View reviewed changes

allredj reviewed Nov 13, 2018

View reviewed changes

peterschrammel reviewed Nov 13, 2018

View reviewed changes

peterschrammel added the documentation label Nov 13, 2018

peterschrammel assigned xbauch Nov 13, 2018

tautschnig reviewed Nov 14, 2018

View reviewed changes

allredj reviewed Nov 15, 2018

View reviewed changes

majakusber approved these changes Nov 15, 2018

View reviewed changes

allredj reviewed Nov 15, 2018

View reviewed changes

xbauch force-pushed the docu/symex_target branch from 7d77198 to fffc954 Compare November 16, 2018 08:38

allredj reviewed Nov 16, 2018

View reviewed changes

xbauch assigned peterschrammel and unassigned xbauch Nov 19, 2018

xbauch force-pushed the docu/symex_target branch from fffc954 to e399467 Compare November 30, 2018 14:52

allredj reviewed Nov 30, 2018

View reviewed changes

tautschnig added the Needs rebase label Dec 1, 2018

tautschnig assigned xbauch and unassigned peterschrammel Dec 1, 2018

tautschnig approved these changes Dec 1, 2018

View reviewed changes

xbauch force-pushed the docu/symex_target branch from e399467 to cf97e60 Compare December 3, 2018 10:17

Class and function documentation for goto-symex/symex_target

bff5bf4

1) Document the symex_target interface. 2) Document the symex_target_equation -- Mostly SSA_stept and the transformations into it.

xbauch force-pushed the docu/symex_target branch from cf97e60 to bff5bf4 Compare December 3, 2018 11:26

allredj reviewed Dec 3, 2018

View reviewed changes

xbauch merged commit 38c8afe into diffblue:develop Dec 3, 2018

xbauch deleted the docu/symex_target branch June 10, 2019 12:28

	/// \param what: The expression to be added to the \c lhs
	/// \param what: The expression to be added to the \p lhs

	/// symbolic steps into. Presently, symex_target_equationt is the only
	/// symbolic steps into. Presently, \ref symex_target_equationt is the only

		@@ -26,6 +29,9 @@ class symex_targett

		virtual ~symex_targett() { }

		/// Identifies source in the context of symbolic execution. Thread number

	/// Read from a shared variable `ssa_rhs` (which will thus become a
	/// Read from a shared variable \p ssa_rhs (which will thus become a

	/// form of the input program as a list of SSA_stept. It further extends the
	/// form of the input program as a list of \ref SSA_stept. It further extends the

Class and function documentation for goto-symex-target [DOC-79] #3393

Class and function documentation for goto-symex-target [DOC-79] #3393

Uh oh!

Conversation

xbauch commented Nov 13, 2018

Uh oh!

majakusber left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

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!

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

xbauch commented Nov 15, 2018

Uh oh!

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

peterschrammel commented Nov 15, 2018

Uh oh!

xbauch commented Nov 16, 2018

Uh oh!

majakusber Nov 15, 2018 •

edited

Loading