Merge pull request #7930 from NlightNFotis/shadow_mem_doxygen

[DOCS] Partial doxygen for shadow_memory_util

Author: NlightNFotis

src/goto-symex/shadow_memory_util.cpp

@@ -262,8 +262,6 @@ get_field_init_type(const irep_idt &field_name, const goto_symex_statet &state)
   return field_init_expr.type();
 }
 
-/// Given a pointer expression `address` checks if any expr in value_set is
-/// compatible
 bool contains_null_or_invalid(
   const std::vector<exprt> &value_set,
   const exprt &address)
@@ -350,7 +348,13 @@ static void or_elements(
   }
 }
 
-// TODO: doxygen?
+/// Translate a list of values into an or expression. Used here in the
+/// implementation of aggregation of boolean-typed fields.
+/// \param field_type The type of the values of the or expression (expected to
+///    be the same).
+/// \param values A list (std::vector) of values collected previously, passed
+///    through immediately to the constructed expression as operands.
+/// \return A newly constructed or_exprt over the possible values given.
 static exprt or_values(const exprt::operandst &values, const typet &field_type)
 {
   if(values.size() == 1)

src/goto-symex/shadow_memory_util.h

@@ -64,7 +64,9 @@ void log_value_set(
   const messaget &log,
   const std::vector<exprt> &value_set);
 
-/// Log a match between a value in the value set of a given expression, and
+/// Log a match between an address and a value the value set. This version of
+/// the function reports more details, including the base address, the pointer
+/// and the shadow value.
 void log_value_set_match(
   const namespacet &ns,
   const messaget &log,
@@ -74,7 +76,7 @@ void log_value_set_match(
   const exprt &expr,
   const value_set_dereferencet::valuet &shadow_dereference);
 
-// TODO: doxygen
+/// Logs a successful match between an address and a value within the value set.
 void log_value_set_match(
   const namespacet &ns,
   const messaget &log,
@@ -87,17 +89,27 @@ void log_try_shadow_address(
   const messaget &log,
   const shadow_memory_statet::shadowed_addresst &shadowed_address);
 
-// TODO: doxygen
+/// Generic logging function that will log depending on the configured
+/// verbosity. Will log a specific message given to it, along with an expression
+/// passed along to it.
 void log_cond(
   const namespacet &ns,
   const messaget &log,
   const char *cond_text,
   const exprt &cond);
 
-// TODO: doxygen
+/// Replace an invalid object by a null pointer. Works recursively on the
+/// operands (child nodes) of the expression, as well.
+/// \param expr The (root) expression where substitution will happen.
 void replace_invalid_object_by_null(exprt &expr);
 
-// TODO: doxygen
+/// Retrieve the expression that a field was initialised with within a given
+/// symex state.
+/// \param field_name The field whose initialisation expression we want to
+///   retrieve.
+/// \param state The goto symex state within which we want to search for the
+///   expression.
+/// \returns The expression the field was initialised with.
 const exprt &
 get_field_init_expr(const irep_idt &field_name, const goto_symex_statet &state);
 
@@ -112,45 +124,67 @@ std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
   const typet &lhs_type,
   bool &exact_match);
 
-// TODO: doxygen
+/// Retrieves the value of the initialising expression.
+/// \param field_name The name of the field whose value type we want to query.
+/// \param state The symex_state within which the query is executed (the field's
+///    value is looked up).
+/// \returns The type of the value the field was initialised with (actually,
+///    the type of the value the field currently is associated with, but it's
+///    invariant since the declaration).
 const typet &
 get_field_init_type(const irep_idt &field_name, const goto_symex_statet &state);
 
-// TODO: doxygen
+/// Given a pointer expression check to see if it can be a null pointer or an
+/// invalid object within value_set.
+/// \param address A pointer expressions that we are using as the query.
+/// \param value_set The search space for the query.
+/// \returns true if the object can be null or invalid in the value set, false
+///    otherwise.
 bool contains_null_or_invalid(
   const std::vector<exprt> &value_set,
   const exprt &address);
 
-// TODO: doxygen
+/// Performs aggregation of the shadow memory field value over multiple cells
+/// for fields whose type is _Bool.
 exprt compute_or_over_cells(
   const exprt &expr,
   const typet &field_type,
   const namespacet &ns,
   const messaget &log,
   const bool is_union);
 
-// TODO: doxygen
+/// Performs aggregation of the shadow memory field value over multiple cells
+/// for fields whose type is a signed/unsigned bitvector (where the value is
+/// arbitrary up until the max represented by the bitvector size).
 exprt compute_max_over_cells(
   const exprt &expr,
   const typet &field_type,
   const namespacet &ns,
   const messaget &log,
   const bool is_union);
 
-// TODO: doxygen?
+/// Build an if-then-else chain from a vector containing pairs of expressions.
+/// \param conds_values Contains pairs <e1, e2>, where `e1` is going to be
+///    used as an antecedent for an if_expr, and `e2` is going to be used
+///    as the consequent.
+/// \returns An if_exprt of the form `if e1 then e2 else if e3 then e4 else ...`
 exprt build_if_else_expr(
   const std::vector<std::pair<exprt, exprt>> &conds_values);
 
-// TODO: improve?
-/// returns true if we attempt to set/get a field on a NULL pointer
+/// Checks if given expression is a null pointer.
+/// \returns true if expr is a a NULL pointer within value_set.
 bool set_field_check_null(
   const namespacet &ns,
   const messaget &log,
   const std::vector<exprt> &value_set,
   const exprt &expr);
 
-// TODO: improve?
-/// Used for set_field and shadow memory copy
+/// Get shadow memory values for a given expression within a specified value
+/// set.
+/// \returns if potential values are present for that object inside the value
+///    set, then we get back an `if e1 then e2 else (if e3 else e4...`
+///    expression, where `e1`, `e3`, ... are guards (conditions) and `e2`, `e4`,
+///    etc are the possible values of the object within the value set.
 optionalt<exprt> get_shadow_memory(
   const exprt &expr,
   const std::vector<exprt> &value_set,