DOC-70: Description of `rd_range_domaint` of reaching_definitions.h(cpp) module. #3399

marek-trtik · 2018-11-13T17:11:40Z

No description provided.

chrisr-diffblue

This looks really great, and a huge improvement. A few minor comments, but otherwise very happy, thanks!

chrisr-diffblue · 2018-11-13T17:20:37Z

src/analyses/README.md

+#### Struct `reaching_definitiont`
+
+Identifies a GOTO instruction where a given variable is defined (i.e. it is set
+a certain value). In consists of these data:


"a certain value" -> "to a certain value"

chrisr-diffblue · 2018-11-13T17:25:21Z

src/analyses/README.md

+
+There is defined an order of instances of this structure. But its purpose is
+only for to be able to use instances as keys in ordered containers, like
+`std::map`.


I wonder if this paragraph might be better phrased as something like this?

In order to use instances of this structure as keys in ordered containers, such as std::map, an ordering is defined.

chrisr-diffblue · 2018-11-13T17:27:09Z

src/analyses/README.md

+inserted `reaching_definitionst` instance. Internally, the class holds two data
+members:
+
+- `value_map` It is (an unordered) map from names of program variables to a set


'It is (an unordered) map' -> 'is an unordered map'

chrisr-diffblue · 2018-11-13T17:32:19Z

src/analyses/README.md

+- `value_map` It is (an unordered) map from names of program variables to a set
+  of pairs (`reaching_definitiont`, `ID`). Formally, the map is defined as
+  `value_map: var_names -> (reaching_definitionst -> ID)`.
+- `values` It is a map from an `ID` to the corresponding `reaching_definitiont`


'It is a map' -> 'is a map'

chrisr-diffblue · 2018-11-13T17:33:13Z

src/analyses/README.md

+
+- `has_value` This (three value logic) flag determines, whether the instance
+  represents `top`, `bottom`, or any other element of the lattice, by values
+  `TRUE`, `FALSE`, and `UNKNOW` respectively. Initially it is set to `FALSE`.


UNKNOW -> UNKNOWN

chrisr-diffblue · 2018-11-13T17:36:33Z

src/analyses/README.md

+   all `rd_range_domaint` instances. NOTE: `reaching_definitions_analysist`
+   inherits from `sparse_bitvector_analysist<reaching_definitiont>` and so
+   `this` is passed to `set_bitvector_container` for all instances.  
+- `values` It is (an ordered) map from program variable names to `ID`s of


'It is (an ordered) map' -> 'is an ordered map'

chrisr-diffblue · 2018-11-13T17:37:14Z

src/analyses/README.md

+  `reaching_definitiont` instances stored in map pointed to by `bv_container`.
+  The map is not empty only if `has_value` is `UNKNOWN`. Variables in the map
+  are all those which are live at the associated instruction.
+- `export_cache` It is a helper data structure. It consists of data already


'It is a helper' -> 'is a helper'

chrisr-diffblue · 2018-11-13T17:38:05Z

src/analyses/README.md

+  are all those which are live at the associated instruction.
+- `export_cache` It is a helper data structure. It consists of data already
+  stored in `values` and `bv_container`. The purpose of this structure is to
+  provide a boost for certain operations (discussed below). It is basically


What type of boost? runtime improvement? memory usage improvement?

chrisr-diffblue · 2018-11-13T17:39:33Z

src/analyses/README.md

+NOTE: The operation actually does not produce a new `join` element. The element
+`a` is modified to become the `join` element. 
+
+NOTE: When union of `a.values[v]` and `b.values[v]` is computed, then `v` must


'then v must' -> 'then v must be'

fixed as well.

chrisr-diffblue · 2018-11-13T17:41:01Z

src/analyses/README.md

+new reaching definition record, for a passed variable name, written in given
+GOTO instruction (identified by an iterator), at same range of bits.
+
+##### Method `polulate_cache`


'polulate_cache' -> 'populate_cache'

allredj

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

tautschnig · 2018-11-13T20:03:21Z

src/analyses/README.md

+Identifies a GOTO instruction where a given variable is defined (i.e. it is set
+a certain value). In consists of these data:
+- `identifier` The name of the variable which was defined.
+- `definition_at` The iterator to the GOTO instruction where the variable is


where the variable has been written to

tautschnig · 2018-11-13T20:03:59Z

src/analyses/README.md

+- `bit_begin` and `bit_end` These two integers define a range of bits (i.e. the
+  begin and end bit indices) which represent the value of the variable. Clearly,
+  `0 <= bit_begin < bit_end`. However, `bit_end` can also be set a special value
+  `-`, which means infinite/unknown index.


-1, not just -

tautschnig · 2018-11-13T20:04:23Z

src/analyses/README.md

+- `definition_at` The iterator to the GOTO instruction where the variable is
+- `bit_begin` and `bit_end` These two integers define a range of bits (i.e. the
+  begin and end bit indices) which represent the value of the variable. Clearly,
+  `0 <= bit_begin < bit_end`. However, `bit_end` can also be set a special value


Maybe talk about a half-open interval?

peterschrammel · 2018-11-13T22:08:10Z

src/analyses/README.md

+these classes there are more data structures necessary in the computation.
+We discuss all of them in the following sub-sections.   
+
+#### Struct `reaching_definitiont`


🚫I think this detailed documentation should be moved to the source and header files. Only a conceptual overview with refs to the code should be given here.

I could certainly do that. Perhaps in the next doc day?

It's probably half an hour work to copy the text into the right places. I'd prefer it to be done now.

marek-trtik · 2018-11-14T10:45:50Z

Requested updates are available.

danpoe · 2018-11-14T11:16:40Z

src/analyses/README.md

+#### Class `sparse_bitvector_analysist`
+
+An instance of this class provides an assignment of unique numeric `ID` to each
+inserted `reaching_definitionst` instance. Internally, the class holds two data


reaching_definitionst -> reaching_definitiont

danpoe · 2018-11-14T11:16:45Z

src/analyses/README.md

+
+- `value_map` is an unordered map from names of program variables to a set
+  of pairs (`reaching_definitiont`, `ID`). Formally, the map is defined as
+  `value_map: var_names -> (reaching_definitionst -> ID)`.


reaching_definitionst -> reaching_definitiont

danpoe · 2018-11-14T11:16:53Z

src/analyses/README.md

+- `values` is a map from an `ID` to the corresponding `reaching_definitiont`
+  instance inside the map `value_map`. Namely, the map is implemented as an 
+  `std::vector` of iterators to elements of the map `value_map`. An index to
+  `values` vector is the `ID` of the related `reaching_definitionst` instance.


reaching_definitionst -> reaching_definitiont

danpoe · 2018-11-14T11:25:29Z

src/analyses/README.md

+  `reaching_definitiont` instances stored in map pointed to by `bv_container`.
+  The map is not empty only if `has_value` is `UNKNOWN`. Variables in the map
+  are all those which are live at the associated instruction.
+- `export_cache` is a helper data structure. It consists of data already


As far as I've seen the export cache is only populated when rd_range_domaint::output() is called (output() calls get() which in turn calls populate_cache()). Thus, initially when the analysis is run the export cache is always empty. I think the code could be refactored to remove the modifications of the export cache in methods merge(), kill(), etc.

I would recommend not documenting the export cache in detail and only say that it is used when printing output and open an issue for refactoring the use of the export cache instead.

marek-trtik · 2018-11-15T18:19:07Z

Requested updates are available.

danpoe

LGTM

allredj

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

marek-trtik · 2018-11-30T17:22:06Z

@peterschrammel Requested updates are available.

tautschnig

Looks fine except a complaint by cpp-lint (see below) and one by Doxygen that I cannot really make sense of as the parameters do seem to be documented.

tautschnig · 2018-12-01T12:12:39Z

src/analyses/reaching_definitions.cpp

@@ -35,6 +35,14 @@ reaching_definitions_analysist::reaching_definitions_analysist(

 reaching_definitions_analysist::~reaching_definitions_analysist()=default;

+/// Given the passed variable name `identifier` it collects data from


Suggested change

/// Given the passed variable name `identifier` it collects data from

/// Given \p identifier, collect data from

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

src/analyses/reaching_definitions.cpp

@@ -35,6 +35,14 @@ reaching_definitions_analysist::reaching_definitions_analysist(

 reaching_definitions_analysist::~reaching_definitions_analysist()=default;

+/// Given the passed variable name `identifier` it collects data from
+/// `bv_container` for each `ID` in `values[identifier]` and stores them into


Suggested change

/// `bv_container` for each `ID` in `values[identifier]` and stores them into

/// `bv_container` for each `ID` in `values[identifier]` and store them into

tautschnig · 2018-12-01T12:14:42Z

src/analyses/reaching_definitions.h

  irep_idt identifier;
+  /// The iterator to the GOTO instruction where the variable has been written to.


cpp-lint complains: line is too long

johnnonweiler · 2018-12-03T09:14:39Z

src/analyses/reaching_definitions.h

+  /// Computes an instance obtained from the instance `*this` by transformation
+  /// over a GOTO instruction referenced by `from`. The method implements a
+  /// switch according to a type of the instruction and then calls a dedicated
+  /// transform_*` method for the recognised instruction.


Doxygen is getting confused because of a missing backtick at the beginning of line 154. Adding the backtick should fix the warnings. (@marek-trtik It's easy to see this problem by looking at the documentation produced by Doxygen. I suggest reviewing what the generated documentation looks like in doc/html.)

Suggested change

/// transform_*` method for the recognised instruction.

/// `transform_*` method for the recognised instruction.

Thanks! Fixed.

peterschrammel · 2018-12-03T11:16:08Z

@marek-trtik, please squash the commits.

Updates requested in the review: Bug-fixes, typos, rephrasing. Updates requested in the review: Typos, and `export_cache` issue. Updates requested in the review: Moving comments from doc file to code. Bugfixes: to long line; missing backtick

marek-trtik · 2018-12-03T11:46:37Z

@peterschrammel Done.

allredj

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

marek-trtik added the documentation label Nov 13, 2018

marek-trtik self-assigned this Nov 13, 2018

marek-trtik requested review from peterschrammel, danpoe and chrisr-diffblue November 13, 2018 17:11

marek-trtik requested review from martin-cs, smowton and thk123 as code owners November 13, 2018 17:11

chrisr-diffblue reviewed Nov 13, 2018

View reviewed changes

allredj reviewed Nov 13, 2018

View reviewed changes

tautschnig approved these changes Nov 13, 2018

View reviewed changes

peterschrammel reviewed Nov 13, 2018

View reviewed changes

danpoe reviewed Nov 14, 2018

View reviewed changes

danpoe approved these changes Nov 15, 2018

View reviewed changes

allredj reviewed Nov 15, 2018

View reviewed changes

marek-trtik force-pushed the doc_reach_defs branch from 2752f0b to 41a1446 Compare November 30, 2018 17:21

tautschnig approved these changes Dec 1, 2018

View reviewed changes

tautschnig assigned smowton, peterschrammel and chrisr-diffblue Dec 1, 2018

johnnonweiler reviewed Dec 3, 2018

View reviewed changes

johnnonweiler unassigned smowton, peterschrammel and chrisr-diffblue Dec 3, 2018

marek-trtik force-pushed the doc_reach_defs branch from 41a1446 to 9254419 Compare December 3, 2018 10:27

peterschrammel approved these changes Dec 3, 2018

View reviewed changes

marek-trtik force-pushed the doc_reach_defs branch from 9254419 to 1fe3b1a Compare December 3, 2018 11:46

allredj reviewed Dec 3, 2018

View reviewed changes

tautschnig merged commit f0b08e5 into diffblue:develop Dec 3, 2018

		@@ -35,6 +35,14 @@ reaching_definitions_analysist::reaching_definitions_analysist(

		reaching_definitions_analysist::~reaching_definitions_analysist()=default;

		/// Given the passed variable name `identifier` it collects data from

	/// Given the passed variable name `identifier` it collects data from
	/// Given \p identifier, collect data from

	/// `bv_container` for each `ID` in `values[identifier]` and stores them into
	/// `bv_container` for each `ID` in `values[identifier]` and store them into

		irep_idt identifier;
		/// The iterator to the GOTO instruction where the variable has been written to.

	/// transform_*` method for the recognised instruction.
	/// `transform_*` method for the recognised instruction.

DOC-70: Description of rd_range_domaint of reaching_definitions.h(cpp) module. #3399

DOC-70: Description of rd_range_domaint of reaching_definitions.h(cpp) module. #3399

Uh oh!

Conversation

marek-trtik commented Nov 13, 2018

Uh oh!

chrisr-diffblue 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!

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!

marek-trtik commented Nov 14, 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!

marek-trtik commented Nov 15, 2018

Uh oh!

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

marek-trtik commented Nov 30, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

DOC-70: Description of `rd_range_domaint` of reaching_definitions.h(cpp) module. #3399

DOC-70: Description of `rd_range_domaint` of reaching_definitions.h(cpp) module. #3399

marek-trtik commented Nov 30, 2018 •

edited

Loading