Make pointers-to-member work

Change the memory-analyze to produce correct member expressions. Iterate over
the offset from gdb, e.g. `st+4` means jump to the second member component
inside `st`.

Author: petr-bauch

src/memory-analyzer/analyze_symbol.cpp

@@ -13,7 +13,10 @@ Author: Malte Mues <[email protected]>
 #include <util/c_types_util.h>
 #include <util/config.h>
 #include <util/expr_initializer.h>
+#include <util/pointer_offset_size.h>
+#include <util/string2int.h>
 #include <util/string_constant.h>
+#include <util/string_utils.h>
 
 gdb_value_extractort::gdb_value_extractort(
   const symbol_tablet &symbol_table,
@@ -167,6 +170,89 @@ exprt gdb_value_extractort::get_char_pointer_value(
   }
 }
 
+exprt gdb_value_extractort::get_pointer_to_member_value(
+  const exprt &expr,
+  const pointer_valuet &pointer_value,
+  const source_locationt &location)
+{
+  PRECONDITION(expr.type().id() == ID_pointer);
+  PRECONDITION(!is_c_char_type(expr.type().subtype()));
+  const auto &memory_location = pointer_value.address;
+  std::string memory_location_string = memory_location.string();
+  PRECONDITION(memory_location_string != "0x0");
+  PRECONDITION(!pointer_value.pointee.empty());
+
+  std::string struct_name;
+  size_t member_offset;
+  if(pointer_value.pointee.find("+") != std::string::npos)
+  {
+    std::string member_offset_string;
+    split_string(
+      pointer_value.pointee, '+', struct_name, member_offset_string, true);
+    member_offset = safe_string2size_t(member_offset_string);
+  }
+  else
+  {
+    struct_name = pointer_value.pointee;
+    member_offset = 0;
+  }
+
+  const symbolt *struct_symbol = symbol_table.lookup(struct_name);
+  DATA_INVARIANT(struct_symbol != nullptr, "unknown struct");
+  const auto maybe_struct_size =
+    pointer_offset_size(struct_symbol->symbol_expr().type(), ns);
+  bool found = false;
+  CHECK_RETURN(maybe_struct_size.has_value());
+  for(const auto &value_pair : values)
+  {
+    const auto &value_symbol_expr = value_pair.second;
+    if(
+      struct_name ==
+      id2string(to_symbol_expr(value_symbol_expr).get_identifier()))
+    {
+      found = true;
+      break;
+    }
+  }
+
+  if(!found)
+  {
+    const typet target_type = expr.type().subtype();
+
+    symbol_exprt dummy(expr.type());
+    code_blockt assignments;
+
+    const symbol_exprt new_symbol =
+      to_symbol_expr(allocate_objects.allocate_automatic_local_object(
+        assignments, dummy, target_type));
+
+    dereference_exprt dereference_expr(expr);
+
+    const auto zero_expr = zero_initializer(target_type, location, ns);
+    CHECK_RETURN(zero_expr);
+
+    // add assignment of value to newly created symbol
+    add_assignment(new_symbol, *zero_expr);
+
+    values[memory_location] = new_symbol;
+
+    const auto &struct_symbol = values.find(memory_location);
+
+    const auto maybe_member_expr = get_subexpression_at_offset(
+      struct_symbol->second, member_offset, expr.type().subtype(), ns);
+    if(maybe_member_expr.has_value())
+      return *maybe_member_expr;
+    UNREACHABLE;
+  }
+
+  const auto maybe_member_expr = get_subexpression_at_offset(
+    struct_symbol->symbol_expr(), member_offset, expr.type().subtype(), ns);
+  if(maybe_member_expr.has_value())
+    return *maybe_member_expr;
+
+  UNREACHABLE;
+}
+
 exprt gdb_value_extractort::get_non_char_pointer_value(
   const exprt &expr,
   const memory_addresst &memory_location,
@@ -212,6 +298,24 @@ exprt gdb_value_extractort::get_non_char_pointer_value(
   }
 }
 
+bool gdb_value_extractort::points_to_member(
+  const pointer_valuet &pointer_value) const
+{
+  if(pointer_value.pointee.find("+") != std::string::npos)
+    return true;
+
+  const symbolt *pointee_symbol = symbol_table.lookup(pointer_value.pointee);
+  if(pointee_symbol == nullptr)
+    return false;
+  const auto pointee_type = pointee_symbol->type;
+  if(
+    pointee_type.id() == ID_struct_tag || pointee_type.id() == ID_union_tag ||
+    pointee_type.id() == ID_array || pointee_type.id() == ID_struct ||
+    pointee_type.id() == ID_union)
+    return true;
+  return false;
+}
+
 exprt gdb_value_extractort::get_pointer_value(
   const exprt &expr,
   const exprt &zero_expr,
@@ -236,7 +340,9 @@ exprt gdb_value_extractort::get_pointer_value(
     else
     {
       const exprt target_expr =
-        get_non_char_pointer_value(expr, memory_location, location);
+        points_to_member(value)
+          ? get_pointer_to_member_value(expr, value, location)
+          : get_non_char_pointer_value(expr, memory_location, location);
 
       if(target_expr.id() == ID_nil)
       {

src/memory-analyzer/analyze_symbol.h

@@ -150,6 +150,18 @@ class gdb_value_extractort
     const exprt &zero_expr,
     const source_locationt &location);
 
+  /// Call \ref get_subexpression_at_offset to get the correct member
+  ///   expression.
+  /// \param expr: the input pointer expression (needed to get the right type)
+  /// \param pointer_value: pointer value with structure name and offset as the
+  ///   pointee member
+  /// \param location: the source location
+  /// \return \ref member_exprt that the \p pointer_value points to
+  exprt get_pointer_to_member_value(
+    const exprt &expr,
+    const pointer_valuet &pointer_value,
+    const source_locationt &location);
+
   /// Similar to \ref get_char_pointer_value. Doesn't re-call
   ///   \ref gdb_apit::get_memory, calls \ref get_expr_value on _dereferenced_
   ///   \p expr (the result of which is assigned to a new symbol).
@@ -184,6 +196,12 @@ class gdb_value_extractort
   /// \param expr: expression to be extracted
   /// \return the value as a string
   std::string get_gdb_value(const exprt &expr);
+
+  /// Analyzes the \p pointer_value to decide if it point to a struct or a
+  ///   union (or array)
+  /// \param pointer_value: pointer value to be analyzed
+  /// \return true if pointing to a member
+  bool points_to_member(const pointer_valuet &pointer_value) const;
 };
 
 #endif // CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H