Goto-symex: add documentation to let-lifting and related functions

Author: smowton

src/goto-symex/goto_symex.h

@@ -274,11 +274,28 @@ class goto_symext
   /// \param expr: The expression to clean up
   /// \param state
   /// \param write
+  /// \return owning object for any let-bound variables created as part of
+  ///   cleaning this expression, and which will be killed when the object is
+  ///   allowed to die. The caller should store it or move or return it to an
+  ///   appropriate scope such that it dies only when no new references to a
+  ///   let-bound variable could be created (usually, when the enclosing
+  ///   instruction is done executing)
   NODISCARD symex_live_let_variablest
   clean_expr(exprt &expr, statet &state, bool write);
 
   void trigger_auto_object(const exprt &, statet &);
   void initialize_auto_object(const exprt &, statet &);
+
+  /// Given an expression, find the root object and the offset into it.
+  ///
+  /// The extra complication to be considered here is that the expression may
+  /// have any number of ternary expressions mixed with type casts.
+  /// \return owning object for any let-bound variables created as part of
+  ///   cleaning this expression, and which will be killed when the object is
+  ///   allowed to die. The caller should store it or move or return it to an
+  ///   appropriate scope such that it dies only when no new references to a
+  ///   let-bound variable could be created (usually, when the enclosing
+  ///   instruction is done executing)
   NODISCARD symex_live_let_variablest process_array_expr(statet &, exprt &);
   exprt make_auto_object(const typet &, statet &);
   virtual void dereference(exprt &, statet &, bool write);
@@ -498,7 +515,21 @@ class goto_symext
 
   typedef symex_targett::assignment_typet assignment_typet;
 
+  /// Execute any let expressions in \p expr using \ref symex_assign_symbol.
+  /// The assignments will be made in bottom-up topological but otherwise
+  /// arbitrary order (i.e. in `(let x = let y = 0 in x + y) + (let z = 0 in z)
+  /// we will define `y` before `x`, but `z` and `x` could come in either order)
+  /// \return owning object for any let-bound variables created, and which will
+  ///   be killed when the object is allowed to die. The caller should store it
+  ///   or move or return it to an appropriate scope such that it dies only when
+  ///   no new references to a let-bound variable could be created (usually,
+  ///   when the enclosing instruction is done executing)
   NODISCARD symex_live_let_variablest lift_lets(statet &, exprt &expr);
+
+  /// Execute a single let expression, which should not have any nested let
+  /// expressions (use \ref lift_lets instead if there might be).
+  /// The caller is responsible for killing the newly-defined variable when
+  /// appropriate.
   void lift_let(statet &state, const let_exprt &let_expr);
 
   void symex_assign_rec(