Description of rd_range_domaint of reaching_definitions.h(cpp) module.

Author: marek-trtik

src/analyses/README.md

@@ -121,6 +121,144 @@ is covered in a separate subsection.
 
 A basic description for how a natural loop works is here: https://web.cs.wpi.edu/~kal/PLT/PLT8.6.4.html
 
+### Reaching definitions
+
+This module implements the reaching definitions data-flow analysis
+(see https://en.wikipedia.org/wiki/Reaching_definition for basic introduction)
+on multi-threaded GOTO programs.
+
+The domain element is defined in a class `rd_range_domaint` and the actual
+analysis is implemented in a class `reaching_definitions_analysist`. Beside
+these classes there are more data structures necessary in the computation.
+We discuss all of them in the following sub-sections.   
+
+#### 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:
+- `identifier` The name of the variable which was defined.
+- `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
+  `-`, which means infinite/unknown index.
+
+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`.
+
+#### 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
+members:
+
+- `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`
+  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.
+
+#### Class `rd_range_domaint`
+
+Because the class is inherited from `ai_domain_baset`, its instance represents
+an element of a domain of the reaching definitions abstract interpretation
+analysis. Each instance is thus associated with exactly one instruction in
+an analysed GOTO program. And so, the instance holds information for individual
+program variables about their reaching definitions, at that instruction. The
+information is held in these data members:
+
+- `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`.
+- `bv_container` It is a pointer to a
+   `sparse_bitvector_analysist<reaching_definitiont>` instance. It holds the
+   actual reaching definitions data of individual program variables. This
+   pointer is initially `nullptr` and it is later set (by
+   `reaching_definitions_analysist` instance using the method
+   `set_bitvector_container`) to a valid pointer, which is actually shared by
+   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
+  `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
+  stored in `values` and `bv_container`. The purpose of this structure is to
+  provide a boost for certain operations (discussed below). It is basically
+  (an ordered) map from (a subset of) variables in `values` to iterators to
+  GOTO instructions where the variables are defined. Moreover, each such
+  iterator is also associated with a range of bits defining the value of that
+  variable at that GOTO instruction. Both the iterators and the corresponding
+  bit ranges are simply taken from `reaching_definitiont` instances obtained
+  for `ID`s in `values[var_name]`.
+
+##### Method `merge`
+
+Implements the `join` operation of two instances `a` and `b`. It operates only
+on `a.values` and `b.values`. The keys in the resulting map is the union of
+variable names in both `a.values` and `b.values`. And for each variable
+`v` appearing in both maps `a.values` and `b.values` the resulting mapped set
+of `ID`s is the set union of `a.values[v]` and `b.values[v]`.
+
+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
+removed from the cache `export_cache` 
+
+##### Method `transform`
+
+Computes an instance obtained from a source instance `a` by transformation over
+a passed GOTO instruction. The method implements a switch according to a type of
+instruction and then calls a dedicated `transform_*` method for the recognised
+instruction. The dedicated methods are described below.
+  
+
+##### Method `transform_dead`
+
+Computes an instance obtained from a source instance `a` by transformation over
+`DEAD v` GOTO instruction. The operation simply removes `v` from `a.values` (an
+from the `export_cache`).
+
+##### Method `transform_start_thread`
+
+TODO!
+
+##### Method `transform_function_call`
+
+TODO!
+
+##### Method `transform_end_function`
+
+TODO!
+
+##### Method `transform_assign`
+
+TODO!
+
+##### Method `kill`
+
+TODO!
+
+##### Method `gen`
+
+A utility function which updates internal data structures by inserting a
+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`
+
+Given a variable name `v` it collects data from `bv_container` for each `ID`
+in `values[v]` and stores them into `export_cache[v]`. Namely, for each
+`reaching_definitiont` instance `rd` obtained from `bv_container` it associates
+`rd.definition_at` with the bit-range `(rd.bit_begin, rd.bit_end)`.
+
+### Class `reaching_definitions_analysist`
+
 \subsection analyses-reaching-definitions Reaching definitions (reaching_definitions_analysist)
 
 To be documented.