Document symex_dereference

Author: smowton

src/goto-symex/symex_dereference.cpp

@@ -23,7 +23,19 @@ Author: Daniel Kroening, [email protected]
 
 #include "symex_dereference_state.h"
 
-/// Evaluate an ID_address_of expression
+/// Transforms an lvalue expression by replacing any dereference operations it
+/// contains with explicit references to the objects they may point to (using
+/// \ref goto_symext::dereference_rec), and translates `byte_extract,` `member`
+/// and `index` operations into integer offsets from a root symbol (if any).
+/// These are ultimately expressed in the form
+/// `(target_type*)((char*)(&underlying_symbol) + offset)`.
+/// \param expr: expression to replace with normalised, dereference-free form
+/// \param state: working state. See \ref goto_symext::dereference for possible
+///   side-effects of a dereference operation.
+/// \param keep_array: if true and an underlying object is an array, return
+///   its address (`&array`); otherwise return the address of its first element
+///   (`&array[0]).
+/// \return the transformed lvalue expression
 exprt goto_symext::address_arithmetic(
   const exprt &expr,
   statet &state,
@@ -178,6 +190,13 @@ exprt goto_symext::address_arithmetic(
   return result;
 }
 
+/// If \p expr is a \ref dereference_exprt, replace it with explicit references
+/// to the objects it may point to. Otherwise recursively apply this function to
+/// \p expr's operands, with special cases for address-of (handled by \ref
+/// goto_symext::address_arithmetic) and certain common expression patterns
+/// such as `&struct.flexible_array[0]` (see inline comments in code).
+/// For full details of this method's pointer replacement and potential side-
+/// effects see \ref goto_symext::dereference
 void goto_symext::dereference_rec(exprt &expr, statet &state)
 {
   if(expr.id()==ID_dereference)
@@ -294,6 +313,43 @@ void goto_symext::dereference_rec(exprt &expr, statet &state)
   }
 }
 
+/// Replace all dereference operations within \p expr with explicit references
+/// to the objects they may refer to. For example, the expression `*p1 + *p2`
+/// might be rewritten to `obj1 + (p2 == &obj2 ? obj2 : obj3)` in the case where
+/// `p1` is known to point to `obj1` and `p2` points to either `obj2` or `obj3`.
+/// The expression, and any object references introduced, are renamed to L1 in
+/// the process (so in fact we would get `obj1!0@3 + (p2!0@1 == ....` rather
+/// than the exact example given above).
+///
+/// It may have two kinds of side-effect:
+///
+/// 1. When an expression may (or must) point to something which cannot legally
+///    be dereferenced, such as a null pointer or an integer cast to a pointer,
+///    a "failed object" is created instead, via one of two routes:
+///
+///    a. if the `add_failed_symbols` pass has been run then a pointer-typed
+///       symbol `x` will have a corresponding failed symbol `x$object`. This
+///       is replicated according to L1 renaming on demand, so for example on
+///       the first failed dereference of `x!5@10` we will create
+///       `x$object!5@10` and add that to the symbol table.
+///       This addition is made by
+///       \ref symex_dereference_statet::get_or_create_failed_symbol
+///
+///    b. if such a failed symbol can't be found then symex will create one of
+///       its own, called `symex::failed_symbol` with some suffix. This is done
+///       by \ref value_set_dereferencet::dereference
+///
+///    In either case any newly-created symbol is added to \p state's symbol
+///    table and \p expr is altered to refer to it. Typically when \p expr has
+///    some legal targets as well this results in an expression like
+///    `ptr == &real_obj ? real_obj : ptr$object`.
+///
+/// 2. Any object whose base-name ends with `auto_object` is automatically
+///    initialised when dereferenced for the first time, creating a tree of
+///    pointers leading to fresh objects each time such a pointer is
+///    dereferenced. If new objects are created by this mechanism then
+///    state will be altered (by `symex_assign`) to initialise them.
+///    See \ref auto_objects.cpp for details.
 void goto_symext::dereference(exprt &expr, statet &state)
 {
   // The expression needs to be renamed to level 1

src/goto-symex/symex_dereference_state.cpp

@@ -13,6 +13,21 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/symbol_table.h>
 
+/// Get or create a failed symbol for the given pointer-typed expression. These
+/// are used as placeholders when dereferencing expressions that are illegal to
+/// dereference, such as null pointers. The \ref add_failed_symbols pass must
+/// have been run for this to do anything useful;  it annotates a pointer-typed
+/// symbol `p` with an `ID_C_failed_symbol` comment, which we then clone on
+/// demand due to L1 renaming.
+///
+/// For example, if \p expr is `p` and it has an `ID_C_failed_symbol` `p$object`
+/// (the naming convention used by `add_failed_symbols`), and the latest L1
+/// renaming of `p` is `p!2@4`, then we will create `p$object!2@4` if it doesn't
+/// already exist.
+///
+/// \param expr: expression to get or create a failed symbol for
+/// \param [out] symbol: failed symbol result
+/// \return true if we populated \p symbol
 bool symex_dereference_statet::get_or_create_failed_symbol(
   const exprt &expr,
   const symbolt *&symbol)
@@ -68,6 +83,7 @@ bool symex_dereference_statet::get_or_create_failed_symbol(
   return false;
 }
 
+/// Just forwards a value-set query to `state.value_set`
 void symex_dereference_statet::get_value_set(
   const exprt &expr,
   value_setst::valuest &value_set) const

src/goto-symex/symex_dereference_state.h

@@ -16,6 +16,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_symex.h"
 
+/// Callback object that \ref goto_symext::dereference_rec provides to
+/// \ref value_set_dereferencet to provide value sets (from goto-symex's
+/// working value set) and retrieve or create failed symbols on demand.
+/// For details of symex-dereference's operation see
+/// \ref goto_symext::dereference
 class symex_dereference_statet:
   public dereference_callbackt
 {

src/pointer-analysis/goto_program_dereference.cpp

@@ -100,7 +100,6 @@ void goto_program_dereferencet::dereference_failure(
 /// and use `dereference` on subexpressions of the form `*p`
 /// \param expr: expression in which to remove dereferences
 /// \param guard: boolean expression assumed to hold when dereferencing
-/// \param mode: unused
 void goto_program_dereferencet::dereference_rec(exprt &expr, guardt &guard)
 {
   if(!has_subexpr(expr, ID_dereference))

src/pointer-analysis/value_set_dereference.cpp

@@ -258,9 +258,10 @@ bool value_set_dereferencet::dereference_type_compare(
 /// \param pointer_expr: pointer expression that may point to `what`
 /// \return a `valuet` object containing `guard`, `value` and `ignore` fields.
 ///   The `ignore` field is true for a `null` object when `exclude_null_derefs`
-///   is true and integer addresses in java mode.
+///   is true (set by our creator when they know \p what cannot be null)
+////  and for integer addresses in java mode.
 ///   The guard is an appropriate check to determine whether `pointer_expr`
-///   really points to `what`.
+///   really points to `what`; for example `pointer_expr == &what`.
 ///   The value corresponds to the dereferenced pointer_expr assuming it is
 ///   pointing to the object described by `what`.
 ///   For example, we might return

src/pointer-analysis/value_set_dereference.h

@@ -55,8 +55,6 @@ class value_set_dereferencet
   /// \param pointer: A pointer-typed expression, to
   ///        be dereferenced.
   /// \param guard: A guard, which is assumed to hold when dereferencing.
-  /// \param mode: Indicates whether the dereferencing is a load or store
-  //    (unused).
   virtual exprt dereference(const exprt &pointer, const guardt &guard);
 
 private: