Added doxygen to all shadow memory util functions

Author: Enrico Steffinlongo

src/goto-symex/shadow_memory_util.cpp

@@ -138,6 +138,9 @@ void log_value_set(
 #endif
 }
 
+/// 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,
@@ -185,6 +188,9 @@ void log_value_set_match(
 #endif
 }
 
+/// Log trying out a match between an object and a (target) shadow address.
+/// @param shadowed_address The address for which we're currently attempting to
+///   match.
 void log_try_shadow_address(
   const namespacet &ns,
   const messaget &log,
@@ -199,6 +205,9 @@ void log_try_shadow_address(
 #endif
 }
 
+/// 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,
@@ -294,7 +303,9 @@ bool contains_null_or_invalid(
   return false;
 }
 
-// TODO: doxygen?
+/// Casts a given (float) bitvector expression to an unsigned bitvector.
+/// \param value The expression that we are to conditionally cast.
+/// \return An unsigned bitvector expression if eligible - `id` otherwise.
 static exprt conditional_cast_floatbv_to_unsignedbv(const exprt &value)
 {
   if(value.type().id() != ID_floatbv)
@@ -307,7 +318,13 @@ static exprt conditional_cast_floatbv_to_unsignedbv(const exprt &value)
     unsignedbv_typet(to_bitvector_type(value.type()).get_width()));
 }
 
-// TODO: doxygen?
+/// Extract byte-sized elements from the input bitvector-typed expression value
+/// and places them into the array values.
+/// \param value the bitvector typed expression to extract the bytes from
+/// \param type the type of the expression expr (it must be bitvector)
+/// \param field_type the type of the shadow memory
+/// \param values the vector where all the extracted bytes of value will be
+///   placed.
 static void extract_bytes_of_bv(
   const exprt &value,
   const typet &type,
@@ -327,7 +344,16 @@ static void extract_bytes_of_bv(
   }
 }
 
-// TODO: doxygen?
+/// Extract the components from the input expression value and places them into
+/// the array values.
+/// \param element the expression to extract the bytes from
+/// \param field_type the type of the shadow memory
+/// \param ns the namespace within which we're going to perform symbol lookups
+/// \param log the message log to which we're going to print debugging messages,
+///   if debugging is set
+/// \param is_union true if the expression element is part of a union
+/// \param values the vector where all the extracted components of element will
+///   be placed.
 static void extract_bytes_of_expr(
   exprt element,
   const typet &field_type,
@@ -556,7 +582,6 @@ exprt compute_max_over_bytes(
   return max_expr;
 }
 
-// TODO: doxygen?
 exprt build_if_else_expr(
   const std::vector<std::pair<exprt, exprt>> &conds_values)
 {
@@ -577,7 +602,12 @@ exprt build_if_else_expr(
   return result;
 }
 
-// TODO: doxygen?
+/// @brief Checks given types (object type and shadow memory field type) for
+///   equality. We're inspecting only pointer types here - if the two types
+///   given are not pointer types, then we assume it to be vacuously true.
+/// @param expr_type The type of the real object.
+/// @param shadow_type The type of the shadow memory field's value.
+/// @return True if types equal, false otherwise.
 static bool
 are_types_compatible(const typet &expr_type, const typet &shadow_type)
 {
@@ -607,9 +637,9 @@ are_types_compatible(const typet &expr_type, const typet &shadow_type)
   return true;
 }
 
-// TODO: doxygen?
-/// We simplify &string_constant[0] to &string_constant to facilitate expression
+/// Simplify &string_constant[0] to &string_constant to facilitate expression
 /// equality for exact matching.
+/// \note expression expr will be changed.
 static void clean_string_constant(exprt &expr)
 {
   const auto *index_expr = expr_try_dynamic_cast<index_exprt>(expr);
@@ -621,7 +651,10 @@ static void clean_string_constant(exprt &expr)
   }
 }
 
-// TODO: doxygen?
+/// Flattens type of the form `pointer_type(array_type(element_type))` to
+/// `pointer_type(element_type)` and `pointer_type(string_constant_type)` to
+/// `pointer_type(char)`.
+/// \note type `type` will be changed.
 static void adjust_array_types(typet &type)
 {
   auto *pointer_type = type_try_dynamic_cast<pointer_typet>(type);
@@ -641,7 +674,12 @@ static void adjust_array_types(typet &type)
   }
 }
 
-// TODO: doxygen?
+/// Function that compares the two arguments shadowed_address and
+/// matched_base_address, simplifies the comparison expression and if the lhs
+/// and rhs are structurally identical returns true, otherwise returns the
+/// comparison.
+/// \return the comparison expression of shadowed_address and
+/// matched_base_address (or a true_exprt if identical modulo simplification).
 static exprt get_matched_base_cond(
   const exprt &shadowed_address,
   const exprt &matched_base_address,
@@ -676,7 +714,11 @@ static exprt get_matched_base_cond(
   return base_cond;
 }
 
-// TODO: doxygen?
+/// Function that compares the two arguments dereference_pointer and expr,
+/// simplifies the comparison expression and if the lhs and rhs are structurally
+/// identical returns true, otherwise returns the comparison.
+/// \return the comparison expression of dereference_pointer and expr (or a
+/// true_exprt if identical modulo simplification).
 static exprt get_matched_expr_cond(
   const exprt &dereference_pointer,
   const exprt &expr,
@@ -738,7 +780,6 @@ static value_set_dereferencet::valuet get_shadow_dereference(
   return shadow_dereference;
 }
 
-// TODO: doxygen?
 /* foreach shadowed_address in SM:
  *   if(incompatible(shadow.object, object)) continue; // Type incompatibility
  *   base_match = object == shadow_object; // Do the base obj match the SM obj
@@ -886,7 +927,6 @@ std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
   return result;
 }
 
-// TODO: doxygen?
 // Unfortunately.
 static object_descriptor_exprt
 normalize(const object_descriptor_exprt &expr, const namespacet &ns)

src/goto-symex/shadow_memory_util.h

@@ -39,7 +39,8 @@ irep_idt extract_field_name(const exprt &string_expr);
 /// \param type The followed type of expr.
 void clean_pointer_expr(exprt &expr, const typet &type);
 
-/// Converts a given expression into a dereference_exprt.
+/// Wraps a given expression into a `dereference_exprt` unless it is an
+/// `address_of_exprt` in which case it just unboxes it and returns its content.
 exprt deref_expr(const exprt &expr);
 
 /// Logs setting a value to a given shadow field. Mainly for use for
@@ -51,8 +52,8 @@ void log_set_field(
   const exprt &expr,
   const exprt &value);
 
-/// Logs setting a value to a given shadow field. Mainly for use for
-/// debugging purposes.
+/// Logs getting a value corresponding to a shadow memory field. Mainly for
+/// use for debugging purposes.
 void log_get_field(
   const namespacet &ns,
   const messaget &log,
@@ -85,7 +86,9 @@ void log_value_set_match(
   const exprt &address,
   const exprt &expr);
 
-// TODO: doxygen
+/// Log trying out a match between an object and a (target) shadow address.
+/// @param shadowed_address The address for which we're currently attempting to
+///   match.
 void log_try_shadow_address(
   const namespacet &ns,
   const messaget &log,
@@ -115,7 +118,11 @@ void replace_invalid_object_by_null(exprt &expr);
 const exprt &
 get_field_init_expr(const irep_idt &field_name, const goto_symex_statet &state);
 
-// TODO: doxygen?
+/// Get a list of `(condition, value)` pairs for a certain pointer from
+/// the shadow memory, where each pair denotes the `value` of the pointer
+/// expression if the `condition` evaluates to `true`.
+/// \return A vector of pair<expr, expr> corresponding to a condition and value.
+///    (See above for explanation).
 std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
   const namespacet &ns,
   const messaget &log,
@@ -126,7 +133,8 @@ std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
   const typet &lhs_type,
   bool &exact_match);
 
-/// Retrieves the value of the initialising expression.
+/// Retrieves the type of the shadow memory by returning the type of the shadow
+/// memory initializer value.
 /// \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).
@@ -146,8 +154,15 @@ bool contains_null_or_invalid(
   const std::vector<exprt> &value_set,
   const exprt &address);
 
-/// Performs aggregation of the shadow memory field value over multiple cells
+/// Performs aggregation of the shadow memory field value over multiple bytes
 /// for fields whose type is _Bool.
+/// \param expr the type to compute the or over each of its bytes
+/// \param field_type the type of the shadow memory (must be `c_bool` or `bool`)
+/// \param ns the namespace within which we're going to perform symbol lookups
+/// \param log the message log to which we're going to print debugging messages,
+///   if debugging is set
+/// \param is_union `true` if the expression expr is part of a union.
+/// \return the aggregated `or` byte-sized value contained in expr
 exprt compute_or_over_bytes(
   const exprt &expr,
   const typet &field_type,
@@ -173,11 +188,20 @@ exprt compute_max_over_bytes(
 ///    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 ...`
+/// \note the expression created will not have the first condition as the first
+///    element will serve fallback if all the other conditions are `false`.
 exprt build_if_else_expr(
   const std::vector<std::pair<exprt, exprt>> &conds_values);
 
-/// Checks if given expression is a null pointer.
-/// \returns true if expr is a a NULL pointer within value_set.
+/// Checks if value_set contains only a `NULL` pointer expression of the same
+///   type of expr.
+/// \param ns the namespace within which we're going to perform symbol lookups
+/// \param log the message log to which we're going to print debugging messages,
+///   if debugging is set
+/// \param value_set the collection to check if it contains *only* the `NULL`
+///   pointer
+/// \param expr a pointer-typed expression
+/// \return `true` if value_set contains only a `NULL` pointer expression
 bool check_value_set_contains_only_null_ptr(
   const namespacet &ns,
   const messaget &log,