Merge pull request diffblue#275 from diffblue/smowton/docs/lvsa

Document LVSA

Author: owen-jones-diffblue

src/pointer-analysis/local_value_set.cpp

@@ -13,6 +13,9 @@
 
 #include <boost/range/algorithm.hpp>
 
+// For documentation of members of `local_value_sett`, see the corresponding
+// header file, `local_value_set.h`.
+
 void local_value_sett::make_union_adjusting_evs_types(
   object_mapt &dest,
   const object_mapt &src,
@@ -73,14 +76,35 @@ void local_value_sett::get_value_set(
   baset::get_value_set(tmp, dest, ns, true);
 }
 
+/// Value-set analysis accrues a `suffix` as it walks down an expression tree--
+/// for example, it transforms a `get_value_set_rec(x.y.z)` into
+/// `get_value_set_rec(x, suffix = "y.z")`. This function recovers the type
+/// information lost in so doing by examining the type of the root expression
+/// and each subsequent member.
+/// The suffix may also contain the string "[]", which indicates a pointer
+/// dereference or array indexing operation.
+/// \param original_type: Type of root object (in the above example, `x.type()`)
+/// \param suffix: Suffix, a sequence of member and array operators
+/// \param ns: global namespace
+/// \param [out] parent_type: Type of the object referred to excluding the
+/// suffix's last period-delimited element. For example, if suffix is
+/// `x.y[].z[][]`, then this gives the result for `x.y[]`. If there is only
+/// one element in `suffix` (e.g. `.a[]`) then  `parent_type` is simply
+/// `original_type`. If suffix is empty then `parent_type` is not assigned.
+/// \param [out] suffix_without_supertypes: is assigned `suffix` with any
+/// leading `[email protected]` accessors removed. For example, if
+/// `suffix` is `[email protected][email protected]` then `suffix_without_supertypes`
+/// will be assigned `.z`.
+/// \return Type of expression `root.suffix`, where `root` has type
+/// `original_type`
 static const typet &type_from_suffix(
   const typet &original_type,
   const std::string &suffix,
   const namespacet &ns,
   typet &parent_type,
-  std::string &suffix_without_subtypes)
+  std::string &suffix_without_supertypes)
 {
-  suffix_without_subtypes=suffix;
+  suffix_without_supertypes=suffix;
   const typet* ret=&original_type;
   size_t next_member=1; // Skip initial '.'
   if(suffix.size()!=0)
@@ -93,7 +117,8 @@ static const typet &type_from_suffix(
     // of pending members or similar.
     if(suffix[next_member]=='@')
     {
-      // This path is (believed to be, supposed to be) Java-specific.
+      // This accesses either special fields @class_identifier or @lock,
+      // or a superclass field, which has a name like @package.Classname.
       if(has_infix(suffix, "@lock", next_member) ||
          has_infix(suffix, "@class_identifier", next_member))
         return static_cast<const typet&>(get_nil_irep());
@@ -104,10 +129,12 @@ static const typet &type_from_suffix(
       assert(has_infix(suffix, subclass_name, next_member));
       ret=&subclass_comp.type();
       next_member+=(subclass_name.size()+1);
-      suffix_without_subtypes=suffix.substr(next_member-1);
+      suffix_without_supertypes=suffix.substr(next_member-1);
     }
     else
     {
+      // This accesses a struct member and then dereferences it one or more
+      // times (for example, .x[][] gets field x and then derefs it twice)
       size_t member_after=suffix.find('.', next_member);
       if(member_after==std::string::npos)
         member_after=suffix.size();
@@ -135,7 +162,6 @@ static const typet &type_from_suffix(
   return *ret;
 }
 
-// Override value_sett to provide behaviour for external value sets
 void local_value_sett::get_value_set_rec(
   const exprt &expr,
   object_mapt &dest,
@@ -197,6 +223,10 @@ void local_value_sett::get_value_set_rec(
         "[]" :
         suffix_without_subtype;
       const auto &extinit=to_external_value_set(expr);
+
+      // If we're reading from `EVS(A.b)` then initialize an entry for that
+      // EVS containing an initializer (e.g.
+      // `external_objects.A.b <- { EVS(A.b) }`.
       access_path_entry_exprt newentry(
         access_path_suffix,
         function,
@@ -228,9 +258,6 @@ void local_value_sett::get_value_set_rec(
   }
 }
 
-/// Applying side effects needed in Recency Analysis.
-/// \param rhs: Right-hand-side of an assignment code expression.
-/// \param ns: Namespace.
 void local_value_sett::apply_side_effects(
   const exprt &rhs,
   const namespacet &ns)

src/pointer-analysis/local_value_set.h

@@ -15,57 +15,100 @@ class local_value_sett:public value_sett
 public:
   typedef value_sett baset;
 
-  #ifdef USE_DSTRING
-  typedef std::map<idt, typet> declared_on_type_mapt;
-  #else
-  typedef std::unordered_map<idt, typet, string_hash> declared_on_type_mapt;
-  #endif
-
-  declared_on_type_mapt declared_on_types;
   mutable bool use_precise_evs=true;
 
+  /// Clone of `value_sett::make_union`, with the exception that any external
+  /// value-set expressions in `src` have their type updated before insertion
+  /// into `dest`. This is used because we need to keep track of typecasts
+  /// and other implicit casts affecting EVSes in order to know the actual
+  /// types accessed by future member accesses.
+  /// For example, if we have `class A { Object o; }`, then in the expression
+  /// `((B)some_parameter.o).bfield`, `some_parameter.o` evaluates to `EVS(A.o)`
+  /// with its natural type `Object`, but `(B)some_parameter.o` evaluates to
+  /// `(B)EVS(A.o)`, represented by changing the EVS' type to `B`. This is
+  /// then used to interpret the access `.bfield` with respect to type `B`.
+  /// \param [out] dest: value-set RHS to merge into
+  /// \param src: value-set RHS to merge in
+  /// \param new_evs_type: new type for EVS expressions entering `dest`
   void make_union_adjusting_evs_types(
     object_mapt &dest,
     const object_mapt &src,
     const typet&) const;
 
+  /// Gets or creates a value-set entry corresponding to an external value set
+  /// expression, which initially contains the EVS itself. For example, given
+  /// EVS(A.x), representing all `x` fields of objects of type `A`, this would
+  /// create an entry `external_objects.A.x <- EVS(A.x)` if it didn't already
+  /// exist and return an iterator pointing to it.
+  /// \param evse: external value set whose entry to create
+  /// \return a la `std::map::insert`, a pair of an iterator pointing to the
+  ///   relevant entry and a boolean indicating if it is new.
   std::pair<valuest::iterator, bool> init_external_value_set(
     const external_value_set_exprt& evse);
 
+  // For all the overrides below, see the base type for parameter-level docs
+  // as their meanings are unchanged.
+
+  /// Overrides `value_sett::get_value_set` to ensure casts between identical
+  /// structs (e.g. `(struct Empty*)&also_empty_struct_of_different_type`
+  /// should result in values of type `Empty*`, not the RHS' type)
   void get_value_set(
     const exprt &expr,
     object_mapt &dest,
     const namespacet &ns,
     bool is_simplified) const override;
 
+  /// Overrides `value_sett::assign` to (a) tag all external-value-set
+  /// expressions from `rhs` indicating they have been assigned, and (b)
+  /// apply side-effects of this assignment to the whole domain, which currently
+  /// means demoting recent dynamic object operations to general ones when
+  /// passing over that same dynamic object's allocation site.
   void assign(
     const exprt &lhs,
     const exprt &rhs,
     const namespacet &ns,
     bool is_simplified,
     bool add_to_sets) override;
 
+  /// Overrides `value_sett::apply_code` to erase `dead` statements and ignore
+  /// intrinsic instructions that manipulate abstract taint but don't cause
+  /// any actual data flow.
   void apply_code(
     const codet &,
     const namespacet &) override;
 
+  /// Union data structures in this value-set besides the actual `values`
+  /// with those in `other`.
   void make_union_bookkeeping_data_structures(const local_value_sett &other);
 
 protected:
+  /// Overrides `value_sett::get_value_set_rec` to (a) handle reads from
+  /// external value sets and (b) ensure reads from Java allocation sites pick
+  /// up the correct dynamic object ID.
   void get_value_set_rec(
     const exprt &expr,
     object_mapt &dest,
     const std::string &suffix,
     const typet &original_type,
     const namespacet &ns) const override;
 
+  /// Overrides `value_sett::assign_rec` to (a) handle writes to external value
+  /// sets and (b) record `declared_on_type` entries for all symbols and
+  /// dynamic objects, making it easier for external value sets to be matched
+  /// against them when applying a function summary at a callsite.
   void assign_rec(
     const exprt &lhs,
     const object_mapt &values_rhs,
     const std::string &suffix,
     const namespacet &ns,
     bool add_to_sets) override;
 
+  /// Applies side-effects stemming from reading from `rhs`. At the moment this
+  /// only happens when we pass an allocation site, at which recent dynamic
+  /// objects (representing the most recent allocation at this site) are merged
+  /// into the general dynamic object representing the same site.
+  /// \param rhs: RHS of an assignment
+  /// \param ns: global namespace
   void apply_side_effects(
     const exprt &rhs,
     const namespacet &ns);