Merge pull request diffblue#3413 from owen-jones-diffblue/doc/abstract-interpretation

DOC-50: Add some documentation to abstract interpretation

Author: owen-jones-diffblue

src/analyses/ai.cpp

@@ -60,9 +60,6 @@ void ai_baset::output(
   }
 }
 
-/// Output the domains for the whole program as JSON
-/// \par parameters: The namespace and goto_functions
-/// \return The JSON object
 jsont ai_baset::output_json(
   const namespacet &ns,
   const goto_functionst &goto_functions) const
@@ -86,7 +83,10 @@ jsont ai_baset::output_json(
 }
 
 /// Output the domains for a single function as JSON
-/// \par parameters: The namespace, goto_program and it's identifier
+/// \param ns: The namespace
+/// \param goto_program: The goto program
+/// \param identifier: The identifier used to find a symbol to identify the
+///   source language
 /// \return The JSON object
 jsont ai_baset::output_json(
   const namespacet &ns,
@@ -116,9 +116,6 @@ jsont ai_baset::output_json(
   return std::move(contents);
 }
 
-/// Output the domains for the whole program as XML
-/// \par parameters: The namespace and goto_functions
-/// \return The XML object
 xmlt ai_baset::output_xml(
   const namespacet &ns,
   const goto_functionst &goto_functions) const
@@ -145,7 +142,10 @@ xmlt ai_baset::output_xml(
 }
 
 /// Output the domains for a single function as XML
-/// \par parameters: The namespace, goto_program and it's identifier
+/// \param ns: The namespace
+/// \param goto_program: The goto program
+/// \param identifier: The identifier used to find a symbol to identify the
+///   source language
 /// \return The XML object
 xmlt ai_baset::output_xml(
   const namespacet &ns,
@@ -341,7 +341,7 @@ bool ai_baset::do_function_call(
 
   if(!goto_function.body_available())
   {
-    // if we don't have a body, we just do an edige call -> return
+    // If we don't have a body, we just do an edge call -> return
     std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
     tmp_state->transform(
       calling_function_identifier,

src/analyses/ai.h

@@ -25,10 +25,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "ai_domain.h"
 
-/// The basic interface of an abstract interpreter.  This should be enough
+/// The basic interface of an abstract interpreter. This should be enough
 /// to create, run and query an abstract interpreter.
-// don't use me -- I am just a base class
-// use ait instead
+///
+/// Note: this is just a base class. \ref ait should be used instead.
 class ai_baset
 {
 public:
@@ -43,7 +43,7 @@ class ai_baset
   {
   }
 
-  /// Running the interpreter
+  /// Run abstract interpretation on a single function
   void operator()(
     const irep_idt &function_identifier,
     const goto_programt &goto_program,
@@ -56,6 +56,7 @@ class ai_baset
     finalize();
   }
 
+  /// Run abstract interpretation on a whole program
   void operator()(
     const goto_functionst &goto_functions,
     const namespacet &ns)
@@ -66,6 +67,7 @@ class ai_baset
     finalize();
   }
 
+  /// Run abstract interpretation on a whole program
   void operator()(const goto_modelt &goto_model)
   {
     const namespacet ns(goto_model.symbol_table);
@@ -75,6 +77,7 @@ class ai_baset
     finalize();
   }
 
+  /// Run abstract interpretation on a single function
   void operator()(
     const irep_idt &function_identifier,
     const goto_functionst::goto_functiont &goto_function,
@@ -87,17 +90,27 @@ class ai_baset
     finalize();
   }
 
-  /// Accessing individual domains at particular locations
-  /// (without needing to know what kind of domain or history is used)
-  /// A pointer to a copy as the method should be const and
-  /// there are some non-trivial cases including merging domains, etc.
-  /// Intended for users of the abstract interpreter; don't use internally.
-
-  /// Returns the abstract state before the given instruction
+  /// Get a copy of the abstract state before the given instruction, without
+  /// needing to know what kind of domain or history is used. Note: intended
+  /// for users of the abstract interpreter; derived classes should
+  /// use \ref get_state or \ref find_state to access the actual underlying
+  /// state.
   /// PRECONDITION(l is dereferenceable)
+  /// \param l: The location before which we want the abstract state
+  /// \return The abstract state before `l`. We return a pointer to a copy as
+  ///   the method should be const and there are some non-trivial cases
+  ///   including merging abstract states, etc.
   virtual std::unique_ptr<statet> abstract_state_before(locationt l) const = 0;
 
-  /// Returns the abstract state after the given instruction
+  /// Get a copy of the abstract state after the given instruction, without
+  /// needing to know what kind of domain or history is used. Note: intended
+  /// for users of the abstract interpreter; derived classes should
+  /// use \ref get_state or \ref find_state to access the actual underlying
+  /// state.
+  /// \param l: The location before which we want the abstract state
+  /// \return The abstract state after `l`. We return a pointer to a copy as
+  ///   the method should be const and there are some non-trivial cases
+  ///   including merging abstract states, etc.
   virtual std::unique_ptr<statet> abstract_state_after(locationt l) const
   {
     /// PRECONDITION(l is dereferenceable && std::next(l) is dereferenceable)
@@ -106,16 +119,18 @@ class ai_baset
     return abstract_state_before(std::next(l));
   }
 
-  /// Resets the domain
+  /// Reset the abstract state
   virtual void clear()
   {
   }
 
+  /// Output the abstract states for a whole program
   virtual void output(
     const namespacet &ns,
     const goto_functionst &goto_functions,
     std::ostream &out) const;
 
+  /// Output the abstract states for a whole program
   void output(
     const goto_modelt &goto_model,
     std::ostream &out) const
@@ -124,6 +139,7 @@ class ai_baset
     output(ns, goto_model.goto_functions, out);
   }
 
+  /// Output the abstract states for a function
   void output(
     const namespacet &ns,
     const goto_programt &goto_program,
@@ -132,6 +148,7 @@ class ai_baset
     output(ns, goto_program, "", out);
   }
 
+  /// Output the abstract states for a function
   void output(
     const namespacet &ns,
     const goto_functionst::goto_functiont &goto_function,
@@ -140,51 +157,57 @@ class ai_baset
     output(ns, goto_function.body, "", out);
   }
 
-
+  /// Output the abstract states for the whole program as JSON
   virtual jsont output_json(
     const namespacet &ns,
     const goto_functionst &goto_functions) const;
 
+  /// Output the abstract states for a whole program as JSON
   jsont output_json(
     const goto_modelt &goto_model) const
   {
     const namespacet ns(goto_model.symbol_table);
     return output_json(ns, goto_model.goto_functions);
   }
 
+  /// Output the abstract states for a single function as JSON
   jsont output_json(
     const namespacet &ns,
     const goto_programt &goto_program) const
   {
     return output_json(ns, goto_program, "");
   }
 
+  /// Output the abstract states for a single function as JSON
   jsont output_json(
     const namespacet &ns,
     const goto_functionst::goto_functiont &goto_function) const
   {
     return output_json(ns, goto_function.body, "");
   }
 
-
+  /// Output the abstract states for the whole program as XML
   virtual xmlt output_xml(
     const namespacet &ns,
     const goto_functionst &goto_functions) const;
 
+  /// Output the abstract states for the whole program as XML
   xmlt output_xml(
     const goto_modelt &goto_model) const
   {
     const namespacet ns(goto_model.symbol_table);
     return output_xml(ns, goto_model.goto_functions);
   }
 
+  /// Output the abstract states for a single function as XML
   xmlt output_xml(
     const namespacet &ns,
     const goto_programt &goto_program) const
   {
     return output_xml(ns, goto_program, "");
   }
 
+  /// Output the abstract states for a single function as XML
   xmlt output_xml(
     const namespacet &ns,
     const goto_functionst::goto_functiont &goto_function) const
@@ -193,37 +216,67 @@ class ai_baset
   }
 
 protected:
-  // overload to add a factory
-  virtual void initialize(const goto_programt &);
-  virtual void initialize(const goto_functionst::goto_functiont &);
-  virtual void initialize(const goto_functionst &);
+  /// Initialize all the abstract states for a single function. Override this to
+  /// do custom per-domain initialization.
+  virtual void initialize(const goto_programt &goto_program);
+
+  /// Initialize all the abstract states for a single function.
+  virtual void initialize(const goto_functionst::goto_functiont &goto_function);
+
+  /// Initialize all the abstract states for a whole program. Override this to
+  /// do custom per-analysis initialization.
+  virtual void initialize(const goto_functionst &goto_functions);
 
-  // override to add a cleanup step after fixedpoint has run
+  /// Override this to add a cleanup or post-processing step after fixedpoint
+  /// has run
   virtual void finalize();
 
-  void entry_state(const goto_programt &);
-  void entry_state(const goto_functionst &);
+  /// Set the abstract state of the entry location of a single function to the
+  /// entry state required by the analysis
+  void entry_state(const goto_programt &goto_program);
 
+  /// Set the abstract state of the entry location of a whole program to the
+  /// entry state required by the analysis
+  void entry_state(const goto_functionst &goto_functions);
+
+  /// Output the abstract states for a single function
+  /// \param ns: The namespace
+  /// \param goto_program: The goto program
+  /// \param identifier: The identifier used to find a symbol to identify the
+  ///   source language
+  /// \param out: The ostream to direct output to
   virtual void output(
     const namespacet &ns,
     const goto_programt &goto_program,
     const irep_idt &identifier,
     std::ostream &out) const;
 
+  /// Output the abstract states for a single function as JSON
+  /// \param ns: The namespace
+  /// \param goto_program: The goto program
+  /// \param identifier: The identifier used to find a symbol to identify the
+  ///   source language
+  /// \return The JSON object
   virtual jsont output_json(
     const namespacet &ns,
     const goto_programt &goto_program,
     const irep_idt &identifier) const;
 
+  /// Output the abstract states for a single function as XML
+  /// \param ns: The namespace
+  /// \param goto_program: The goto program
+  /// \param identifier: The identifier used to find a symbol to identify the
+  ///   source language
+  /// \return The XML object
   virtual xmlt output_xml(
     const namespacet &ns,
     const goto_programt &goto_program,
     const irep_idt &identifier) const;
 
-
-  // the work-queue is sorted by location number
+  /// The work queue, sorted by location number
   typedef std::map<unsigned, locationt> working_sett;
 
+  /// Get the next location from the work queue
   locationt get_next(working_sett &working_set);
 
   void put_in_working_set(
@@ -234,7 +287,8 @@ class ai_baset
       std::pair<unsigned, locationt>(l->location_number, l));
   }
 
-  // true = found something new
+  /// Run the fixedpoint algorithm until it reaches a fixed point
+  /// \return True if we found something new
   bool fixedpoint(
     const irep_idt &function_identifier,
     const goto_programt &goto_program,
@@ -253,10 +307,10 @@ class ai_baset
     const goto_functionst &goto_functions,
     const namespacet &ns);
 
-  // Visit performs one step of abstract interpretation from location l
-  // Depending on the instruction type it may compute a number of "edges"
-  // or applications of the abstract transformer
-  // true = found something new
+  /// Perform one step of abstract interpretation from location l
+  /// Depending on the instruction type it may compute a number of "edges"
+  /// or applications of the abstract transformer
+  /// \return True if the state was changed
   bool visit(
     const irep_idt &function_identifier,
     locationt l,
@@ -293,8 +347,16 @@ class ai_baset
     locationt from,
     locationt to,
     const namespacet &ns)=0;
+
+  /// Get the state for the given location, creating it in a default way if it
+  /// doesn't exist
   virtual statet &get_state(locationt l)=0;
+
+  /// Get the state for the given location if it already exists; throw an
+  /// exception if it doesn't
   virtual const statet &find_state(locationt l) const=0;
+
+  /// Make a copy of a state
   virtual std::unique_ptr<statet> make_temporary_state(const statet &s)=0;
 };
 
@@ -389,10 +451,11 @@ class ait:public ai_baset
   }
 
 private:
-  // to enforce that domainT is derived from ai_domain_baset
+  /// This function exists to enforce that `domainT` is derived from
+  /// \ref ai_domain_baset
   void dummy(const domainT &s) { const statet &x=s; (void)x; }
 
-  // not implemented in sequential analyses
+  /// This function should not be implemented in sequential analyses
   bool merge_shared(const statet &, locationt, locationt, const namespacet &)
     override
   {

src/analyses/ai_domain.cpp

@@ -35,8 +35,8 @@ xmlt ai_domain_baset::output_xml(const ai_baset &ai, const namespacet &ns) const
 /// an assignment. This for example won't simplify symbols to their values, but
 /// does simplify indices in arrays, members of structs and dereferencing of
 /// pointers
-/// \param condition: the expression to simplify
-/// \param ns: the namespace
+/// \param condition: The expression to simplify
+/// \param ns: The namespace
 /// \return True if condition did not change. False otherwise. condition will be
 ///   updated with the simplified condition if it has worked
 bool ai_domain_baset::ai_simplify_lhs(exprt &condition, const namespacet &ns)

src/analyses/ai_domain.h

@@ -46,7 +46,7 @@ class ai_domain_baset
   ///    (this also needs to set the LHS, if applicable)
   ///
   /// "this" is the domain before the instruction "from"
-  /// "from" is the instruction to be interpretted
+  /// "from" is the instruction to be interpreted
   /// "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
   ///
   /// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
@@ -78,7 +78,7 @@ class ai_domain_baset
   /// and domains may refuse to implement it.
   virtual void make_top() = 0;
 
-  /// a reasonable entry-point state
+  /// Make this domain a reasonable entry-point state
   virtual void make_entry() = 0;
 
   virtual bool is_bottom() const = 0;