Address review comments

Will be squashed.

Author: petr-bauch

src/memory-analyzer/analyze_symbol.cpp

@@ -184,7 +184,7 @@ exprt gdb_value_extractort::get_pointer_to_member_value(
 
   std::string struct_name;
   size_t member_offset;
-  if(pointer_value.pointee.find("+") != std::string::npos)
+  if(pointer_value.has_known_offset())
   {
     std::string member_offset_string;
     split_string(
@@ -206,9 +206,7 @@ exprt gdb_value_extractort::get_pointer_to_member_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()))
+    if(to_symbol_expr(value_symbol_expr).get_identifier() == struct_name)
     {
       found = true;
       break;
@@ -219,12 +217,14 @@ exprt gdb_value_extractort::get_pointer_to_member_value(
   {
     const typet target_type = expr.type().subtype();
 
-    symbol_exprt dummy(expr.type());
+    symbol_exprt dummy("tmp", expr.type());
     code_blockt assignments;
 
-    const symbol_exprt new_symbol =
-      to_symbol_expr(allocate_objects.allocate_automatic_local_object(
+    auto emplace_pair = values.emplace(
+      memory_location,
+      allocate_objects.allocate_automatic_local_object(
         assignments, dummy, target_type));
+    const symbol_exprt &new_symbol = to_symbol_expr(emplace_pair.first->second);
 
     dereference_exprt dereference_expr(expr);
 
@@ -234,23 +234,18 @@ exprt gdb_value_extractort::get_pointer_to_member_value(
     // 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;
+    CHECK_RETURN(maybe_member_expr.has_value());
+    return *maybe_member_expr;
   }
 
   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;
+  CHECK_RETURN(maybe_member_expr.has_value());
+  return *maybe_member_expr;
 }
 
 exprt gdb_value_extractort::get_non_char_pointer_value(
@@ -294,28 +289,30 @@ exprt gdb_value_extractort::get_non_char_pointer_value(
   }
   else
   {
-    const symbol_exprt typed_symbol_value = symbol_exprt{
-      to_symbol_expr(it->second).get_identifier(), expr.type().subtype()};
-    return typed_symbol_value;
+    const auto &known_value = it->second;
+    const auto &expected_type = expr.type().subtype();
+    if(known_value.type() != expected_type)
+    {
+      return symbol_exprt{to_symbol_expr(known_value).get_identifier(),
+                          expected_type};
+    }
+    return known_value;
   }
 }
 
 bool gdb_value_extractort::points_to_member(
   const pointer_valuet &pointer_value) const
 {
-  if(pointer_value.pointee.find("+") != std::string::npos)
+  if(pointer_value.has_known_offset())
     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;
+  const auto &pointee_type = pointee_symbol->type;
+  return 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;
 }
 
 exprt gdb_value_extractort::get_pointer_value(
@@ -487,23 +484,12 @@ exprt gdb_value_extractort::get_union_value(
   exprt new_expr(zero_expr);
 
   const union_tag_typet &union_tag_type = to_union_tag_type(expr.type());
-  const union_typet union_type = ns.follow_tag(union_tag_type);
-
-  for(size_t i = 0; i < new_expr.operands().size(); ++i)
-  {
-    const union_typet::componentt &component = union_type.components()[i];
-
-    if(component.get_is_padding())
-    {
-      continue;
-    }
-
-    exprt &operand = new_expr.operands()[i];
-    member_exprt member_expr(expr, component);
-
-    operand = get_expr_value(member_expr, operand, location);
-  }
+  const union_typet &union_type = ns.follow_tag(union_tag_type);
 
+  CHECK_RETURN(new_expr.operands().size() == 1);
+  const union_typet::componentt &component = union_type.components()[0];
+  auto &operand = new_expr.operands()[0];
+  operand = get_expr_value(member_exprt{expr, component}, operand, location);
   return new_expr;
 }
 

src/memory-analyzer/gdb_api.h

@@ -19,6 +19,7 @@ Author: Malte Mues <[email protected]>
 #define CPROVER_MEMORY_ANALYZER_GDB_API_H
 #include <unistd.h>
 
+#include <algorithm>
 #include <exception>
 #include <forward_list>
 
@@ -81,6 +82,12 @@ class gdb_apit
     const std::string pointee;
     const std::string character;
     const optionalt<std::string> string;
+
+    bool has_known_offset() const
+    {
+      return std::any_of(
+        pointee.begin(), pointee.end(), [](char c) { return c == '+'; });
+    }
   };
 
   /// Create a new gdb process for analysing the binary indicated by the member