Merge pull request #2785 from danpoe/doc/goto-models

Add more documentation for goto programs

Author: danpoe

src/goto-programs/abstract_goto_model.h

@@ -34,7 +34,7 @@ class abstract_goto_modelt
   /// get_goto_functions, or the symbol table returned by get_symbol_table,
   /// so iterators pointing into either may be invalidated.
   /// \param id: function to get
-  /// \return function body
+  /// \return goto function
   virtual const goto_functionst::goto_functiont &get_goto_function(
     const irep_idt &id) = 0;
 

src/goto-programs/goto_function.cpp

@@ -8,8 +8,13 @@ Date: May 2018
 
 \*******************************************************************/
 
+/// \file
+/// Goto Function
+
 #include "goto_function.h"
 
+/// Return in \p dest the identifiers of the local variables declared in the \p
+/// goto_function and the identifiers of the paramters of the \p goto_function.
 void get_local_identifiers(
   const goto_functiont &goto_function,
   std::set<irep_idt> &dest)

src/goto-programs/goto_function.h

@@ -8,6 +8,9 @@ Date: May 2018
 
 \*******************************************************************/
 
+/// \file
+/// Goto Function
+
 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
 #define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
 
@@ -17,13 +20,24 @@ Date: May 2018
 
 #include "goto_program.h"
 
+/// A goto function, consisting of function type (see #type), function body (see
+/// #body), and parameter identifiers (see #parameter_identifiers).
 class goto_functiont
 {
 public:
   goto_programt body;
+
+  /// The type of the function, indicating the return type and parameter types
   code_typet type;
 
   typedef std::vector<irep_idt> parameter_identifierst;
+
+  /// The identifiers of the parameters of this function
+  ///
+  /// Note: This variable is currently unused and the vector is thus always
+  /// empty. In the future the code base may be refactored to fill in the
+  /// parameter identifiers here when creating a `goto_functiont`. For now the
+  /// parameter identifiers should be retrieved from the type (`code_typet`).
   parameter_identifierst parameter_identifiers;
 
   bool body_available() const

src/goto-programs/goto_functions.h

@@ -18,6 +18,7 @@ Date: June 2003
 
 #include <util/cprover_prefix.h>
 
+/// A collection of goto functions
 class goto_functionst
 {
 public:
@@ -63,6 +64,7 @@ class goto_functionst
     return *this;
   }
 
+  /// Remove function from the function map
   void unload(const irep_idt &name) { function_map.erase(name); }
 
   void clear()
@@ -99,6 +101,7 @@ class goto_functionst
     update_instructions_function();
   }
 
+  /// Get the identifier of the entry point to a goto model
   static inline irep_idt entry_point()
   {
     // do not confuse with C's "int main()"

src/goto-programs/goto_program.cpp

@@ -487,6 +487,9 @@ std::string as_string(
   }
 }
 
+/// Assign each loop in the goto program a unique index. Every backwards goto is
+/// considered a loop. The loops are numbered starting from zero and in the
+/// order they appear in the goto program.
 void goto_programt::compute_loop_numbers()
 {
   unsigned nr=0;
@@ -516,6 +519,16 @@ std::ostream &goto_programt::output(
   return out;
 }
 
+/// Assign each target (i.e., an instruction that is in the `targets` list of
+/// another instruction) a unique index.
+///
+/// Instructions that are not targets get target number instructiont::nil_target. The
+/// targets are numbered starting from one and in the order they appear in the
+/// goto program. An instruction is considered a target if it is the target of a
+/// control-flow instruction (either GOTO or START_THREAD), i.e., it is
+/// contained in the `targets` list of those instructions. Instructions that are
+/// reached via straight-line control flow (fall-through for GOTO instructions)
+/// only are not considered targets.
 void goto_programt::compute_target_numbers()
 {
   // reset marking
@@ -564,6 +577,10 @@ void goto_programt::compute_target_numbers()
   }
 }
 
+/// Copy other goto program into this goto program. The current goto program is
+/// cleared, and targets are adjusted as needed
+///
+/// \param src: the goto program to copy from
 void goto_programt::copy_from(const goto_programt &src)
 {
   // Definitions for mapping between the two programs
@@ -604,7 +621,8 @@ void goto_programt::copy_from(const goto_programt &src)
   compute_target_numbers();
 }
 
-// number them
+/// Returns true if the goto program includes an `ASSERT` instruction the guard
+/// of which is not trivially true.
 bool goto_programt::has_assertion() const
 {
   for(const auto &i : instructions)
@@ -614,6 +632,7 @@ bool goto_programt::has_assertion() const
   return false;
 }
 
+/// Compute for each instruction the set of instructions it is a successor of.
 void goto_programt::compute_incoming_edges()
 {
   for(auto &i : instructions)

src/goto-programs/goto_program.h

@@ -170,6 +170,9 @@ class goto_programt
   ///     clears all the catch clauses established as per the above in this
   ///     function?
   ///     Many analysis tools remove these instructions before they start.
+  /// - INCOMPLETE GOTO:
+  ///     goto for which the target is yet to be determined. The target set
+  ///     shall be empty
   class instructiont final
   {
   public:
@@ -421,15 +424,34 @@ class goto_programt
     return t;
   }
 
+  /// Get the id of the function that contains the instruction pointed-to by the
+  /// given instruction iterator.
+  ///
+  /// \param l: instruction iterator
+  /// \return id of the function that contains the pointed-to goto instruction
   static const irep_idt get_function_id(
     const_targett l)
   {
+    // The field `function` of an instruction may not always contain the id of
+    // the function it is currently in, due to goto program modifications such
+    // as inlining. For example, if an instruction in a function `f` is inlined
+    // into a function `g`, the instruction may, depending on the arguments to
+    // the inliner, retain the original value of `f` in the function field.
+    // However, instructions of type END_FUNCTION are never inlined into other
+    // functions, hence they contain the id of the function they are in. Thus,
+    // this function takes the END_FUNCTION instruction of the goto program and
+    // returns the value of its function field.
+
     while(!l->is_end_function())
       ++l;
 
     return l->function;
   }
 
+  /// Get the id of the function that contains the given goto program.
+  ///
+  /// \param p: the goto program
+  /// \return id of the function that contains the goto program
   static const irep_idt get_function_id(
     const goto_programt &p)
   {
@@ -474,14 +496,16 @@ class goto_programt
     instructions.splice(next, p.instructions);
   }
 
-  /// Insertion before the given target
+  /// Insertion before the instruction pointed-to by the given instruction
+  /// iterator `target`.
   /// \return newly inserted location
   targett insert_before(const_targett target)
   {
     return instructions.insert(target, instructiont());
   }
 
-  /// Insertion after the given target
+  /// Insertion after the instruction pointed-to by the given instruction
+  /// iterator `target`.
   /// \return newly inserted location
   targett insert_after(const_targett target)
   {
@@ -619,6 +643,8 @@ class goto_programt
     instructions.clear();
   }
 
+  /// Get an instruction iterator pointing to the END_FUNCTION instruction of
+  /// the goto program
   targett get_end_function()
   {
     PRECONDITION(!instructions.empty());
@@ -628,6 +654,8 @@ class goto_programt
     return end_function;
   }
 
+  /// Get an instruction iterator pointing to the END_FUNCTION instruction of
+  /// the goto program
   const_targett get_end_function() const
   {
     PRECONDITION(!instructions.empty());
@@ -653,6 +681,18 @@ class goto_programt
   bool equals(const goto_programt &other) const;
 };
 
+/// Get control-flow successors of a given instruction. The instruction is
+/// represented by a pointer `target` of type `Target`. An instruction has
+/// either 0, 1, or 2 successors (more than two successors is deprecated). For
+/// example, an `ASSUME` instruction with the `guard` being a `false_exprt` has
+/// 0 successors, and `ASSIGN` instruction has 1 successor, and a `GOTO`
+/// instruction with the `guard` not being a `true_exprt` has 2 successors.
+///
+/// \tparam Target: type used to represent a pointer to an instruction in a goto
+///   program
+/// \param target: pointer to the instruction of which to get the successors of
+/// \return List of control-flow successors of the pointed-to goto program
+///   instruction
 template <typename Target>
 std::list<Target> goto_programt::get_successors(
   Target target) const