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,43 @@ 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()));
+  std::string memory_location = pointer_value.address.string();
+  PRECONDITION(memory_location != "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_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 +252,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 +294,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