Produce annotated pointer constants in incremental SMT2 traces

regression/cbmc/trace-strings/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --trace
 ^EXIT=10$

regression/cbmc/trace_address_arithmetic1/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --trace
 ^EXIT=10$

regression/cbmc/xml-trace2/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --xml-ui
 <full_lhs_value( binary="[01]+")?>\{ 14, 0 \}</full_lhs_value>

src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp

@@ -1,27 +1,110 @@
 // Author: Diffblue Ltd.
 
 #include <util/arith_tools.h>
+#include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
+#include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/type.h>
 
 #include <solvers/smt2_incremental/ast/smt_terms.h>
 #include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
 
+/// \brief Build a symbolic pointer expression from the given
+///   \p object_expr, \p offset, and target pointer \p type, following the
+///   same approach as pointer_logict::pointer_expr in pointer_logic.cpp.
+static exprt build_pointer_expr(
+  const exprt &object_expr,
+  const mp_integer &offset,
+  const pointer_typet &type,
+  const namespacet &ns)
+{
+  typet subtype = type.base_type();
+  // Void pointers with an offset are treated as char pointers, matching
+  // GCC behavior for pointer arithmetic on void pointers.
+  if(subtype.id() == ID_empty)
+    subtype = char_type();
+  if(object_expr.id() == ID_string_constant)
+  {
+    subtype = object_expr.type();
+    // A string constant must be array-typed with fixed size.
+    const array_typet &array_type = to_array_type(object_expr.type());
+    mp_integer array_size =
+      numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
+    if(array_size > offset)
+    {
+      to_array_type(subtype).size() =
+        from_integer(array_size - offset, array_type.size().type());
+    }
+  }
+  auto deep_object_opt =
+    get_subexpression_at_offset(object_expr, offset, subtype, ns);
+  if(!deep_object_opt.has_value())
+    return nil_exprt{};
+  exprt deep_object = deep_object_opt.value();
+  simplify(deep_object, ns);
+  if(
+    deep_object.id() != ID_byte_extract_little_endian &&
+    deep_object.id() != ID_byte_extract_big_endian)
+  {
+    return typecast_exprt::conditional_cast(
+      address_of_exprt(deep_object), type);
+  }
+
+  const byte_extract_exprt &be = to_byte_extract_expr(deep_object);
+  const address_of_exprt base(be.op());
+  if(be.offset() == 0)
+    return typecast_exprt::conditional_cast(base, type);
+
+  const auto object_size = pointer_offset_size(be.op().type(), ns);
+  if(object_size.has_value() && *object_size <= 1)
+  {
+    return typecast_exprt::conditional_cast(
+      plus_exprt(base, from_integer(offset, pointer_diff_type())), type);
+  }
+  else if(object_size.has_value() && offset % *object_size == 0)
+  {
+    return typecast_exprt::conditional_cast(
+      plus_exprt(
+        base, from_integer(offset / *object_size, pointer_diff_type())),
+      type);
+  }
+  else
+  {
+    return typecast_exprt::conditional_cast(
+      plus_exprt(
+        typecast_exprt(base, pointer_type(char_type())),
+        from_integer(offset, pointer_diff_type())),
+      type);
+  }
+}
+
 class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
 {
 private:
   const typet &type_to_construct;
   const namespacet &ns;
+  const smt_object_mapt *object_map;
+  const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
+    *expression_identifiers;
   std::optional<exprt> result;
 
   explicit value_expr_from_smt_factoryt(
     const typet &type_to_construct,
-    const namespacet &ns)
-    : type_to_construct{type_to_construct}, ns{ns}, result{}
+    const namespacet &ns,
+    const smt_object_mapt *object_map = nullptr,
+    const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
+      *expression_identifiers = nullptr)
+    : type_to_construct{type_to_construct},
+      ns{ns},
+      object_map{object_map},
+      expression_identifiers{expression_identifiers},
+      result{}
   {
   }
 
@@ -53,6 +136,10 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
       {
         result = null_pointer_exprt{*pointer_type};
       }
+      else if(object_map)
+      {
+        result = build_annotated_pointer(bit_vector_constant, *pointer_type);
+      }
       else
       {
         // The reason we are manually constructing a constant_exprt here is a
@@ -97,6 +184,91 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
         type_to_construct.pretty());
   }
 
+  /// \brief Build an annotated pointer constant from a bit-vector value
+  ///   using the object map to reconstruct the symbolic pointer expression.
+  exprt build_annotated_pointer(
+    const smt_bit_vector_constant_termt &bit_vector_constant,
+    const pointer_typet &pointer_type)
+  {
+    const auto sort_width = bit_vector_constant.get_sort().bit_width();
+    const irep_idt bvrep =
+      integer2bvrep(bit_vector_constant.value(), sort_width);
+    const std::size_t object_bits = config.bv_encoding.object_bits;
+    const std::size_t pointer_width = pointer_type.get_width();
+    INVARIANT(
+      pointer_width > object_bits,
+      "Pointer width should be wider than object bits.");
+    const std::size_t offset_bits = pointer_width - object_bits;
+
+    // Extract object ID from high bits.
+    const mp_integer object_id = bit_vector_constant.value() >> offset_bits;
+
+    // Extract offset from low bits, sign-extending.
+    mp_integer offset = bit_vector_constant.value() % power(2, offset_bits);
+    if(offset >= power(2, offset_bits - 1))
+      offset -= power(2, offset_bits);
+
+    // Null object with nonzero offset.
+    if(object_id == 0)
+    {
+      null_pointer_exprt null_ptr(pointer_type);
+      exprt symbolic =
+        plus_exprt(null_ptr, from_integer(offset, pointer_diff_type()));
+      return annotated_pointer_constant_exprt{bvrep, symbolic};
+    }
+
+    // Build reverse map from unique_id to base_expression.
+    std::unordered_map<std::size_t, const decision_procedure_objectt *>
+      id_to_object;
+    for(const auto &entry : *object_map)
+      id_to_object.emplace(entry.second.unique_id, &entry.second);
+
+    const auto it = id_to_object.find(numeric_cast_v<std::size_t>(object_id));
+    if(it == id_to_object.end())
+    {
+      // Unknown object - fall back to plain constant.
+      return constant_exprt{bvrep, pointer_type};
+    }
+
+    const decision_procedure_objectt &object = *it->second;
+
+    // Invalid pointer object.
+    if(object.base_expression == make_invalid_pointer_expr())
+      return annotated_pointer_constant_exprt{
+        bvrep, constant_exprt("INVALID", pointer_type)};
+
+    // Resolve the base expression through the expression_identifiers
+    // reverse map. When string constants or other expressions are
+    // substituted with symbol_exprt identifiers during SMT conversion,
+    // the object_map tracks the substituted symbol rather than the
+    // original expression. We reverse that lookup here to recover the
+    // original expression for display in traces.
+    exprt resolved_expr = object.base_expression;
+    if(
+      expression_identifiers &&
+      expr_try_dynamic_cast<symbol_exprt>(object.base_expression))
+    {
+      const auto &sym = to_symbol_expr(object.base_expression);
+      for(const auto &entry : *expression_identifiers)
+      {
+        if(entry.second.identifier() == sym.get_identifier())
+        {
+          resolved_expr = entry.first;
+          break;
+        }
+      }
+    }
+
+    exprt symbolic =
+      build_pointer_expr(resolved_expr, offset, pointer_type, ns);
+    if(symbolic.is_nil())
+    {
+      // Could not build symbolic expression - fall back.
+      return constant_exprt{bvrep, pointer_type};
+    }
+    return annotated_pointer_constant_exprt{bvrep, symbolic};
+  }
+
   void
   visit(const smt_function_application_termt &function_application) override
   {
@@ -131,6 +303,37 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
     INVARIANT(factory.result.has_value(), "Factory must result in expr value.");
     return *factory.result;
   }
+
+  /// \brief Overload accepting an object map for annotated pointer
+  ///   construction.
+  static exprt make(
+    const smt_termt &value_term,
+    const typet &type_to_construct,
+    const namespacet &ns,
+    const smt_object_mapt &object_map)
+  {
+    value_expr_from_smt_factoryt factory{type_to_construct, ns, &object_map};
+    value_term.accept(factory);
+    INVARIANT(factory.result.has_value(), "Factory must result in expr value.");
+    return *factory.result;
+  }
+
+  /// \brief Overload accepting both an object map and expression identifiers
+  ///   for resolving substituted expressions in pointer annotation.
+  static exprt make(
+    const smt_termt &value_term,
+    const typet &type_to_construct,
+    const namespacet &ns,
+    const smt_object_mapt &object_map,
+    const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
+      &expression_identifiers)
+  {
+    value_expr_from_smt_factoryt factory{
+      type_to_construct, ns, &object_map, &expression_identifiers};
+    value_term.accept(factory);
+    INVARIANT(factory.result.has_value(), "Factory must result in expr value.");
+    return *factory.result;
+  }
 };
 
 exprt construct_value_expr_from_smt(
@@ -140,3 +343,25 @@ exprt construct_value_expr_from_smt(
 {
   return value_expr_from_smt_factoryt::make(value_term, type_to_construct, ns);
 }
+
+exprt construct_value_expr_from_smt(
+  const smt_termt &value_term,
+  const typet &type_to_construct,
+  const namespacet &ns,
+  const smt_object_mapt &object_map)
+{
+  return value_expr_from_smt_factoryt::make(
+    value_term, type_to_construct, ns, object_map);
+}
+
+exprt construct_value_expr_from_smt(
+  const smt_termt &value_term,
+  const typet &type_to_construct,
+  const namespacet &ns,
+  const smt_object_mapt &object_map,
+  const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
+    &expression_identifiers)
+{
+  return value_expr_from_smt_factoryt::make(
+    value_term, type_to_construct, ns, object_map, expression_identifiers);
+}

src/solvers/smt2_incremental/construct_value_expr_from_smt.h

@@ -5,7 +5,9 @@
 
 #include <util/expr.h>
 
-class smt_termt;
+#include <solvers/smt2_incremental/ast/smt_terms.h>
+#include <solvers/smt2_incremental/object_tracking.h>
+
 class typet;
 
 /// \brief Given a \p value_term and a \p type_to_construct, this function
@@ -32,4 +34,48 @@ exprt construct_value_expr_from_smt(
   const typet &type_to_construct,
   const namespacet &ns);
 
+/// \brief Overload that accepts an \p object_map for constructing annotated
+/// pointer constants. When the type to construct is a pointer type, the
+/// object map is used to reconstruct a symbolic pointer expression from the
+/// encoded object ID and offset in the bit-vector value.
+/// \param value_term
+///   The SMT term encoding the value.
+/// \param type_to_construct
+///   The type which the constructed expr returned is expected to have.
+/// \param ns
+///   The namespace for type lookups.
+/// \param object_map
+///   Map from base expressions to tracked object information, used to
+///   reconstruct symbolic pointer expressions for trace display.
+exprt construct_value_expr_from_smt(
+  const smt_termt &value_term,
+  const typet &type_to_construct,
+  const namespacet &ns,
+  const smt_object_mapt &object_map);
+
+/// \brief Overload that additionally accepts \p expression_identifiers to
+/// reverse identifier substitutions for pointer annotation. When the object
+/// map contains a symbol_exprt that was introduced by identifier substitution
+/// (e.g., for string constants mapped to array functions), this overload
+/// recovers the original expression for symbolic pointer display.
+/// \param value_term
+///   The SMT term encoding the value.
+/// \param type_to_construct
+///   The type which the constructed expr returned is expected to have.
+/// \param ns
+///   The namespace for type lookups.
+/// \param object_map
+///   Map from base expressions to tracked object information.
+/// \param expression_identifiers
+///   Map from original expressions to their SMT identifier terms, as used
+///   during expression-to-SMT conversion. This is used to reverse the
+///   substitution and recover the original expression for trace display.
+exprt construct_value_expr_from_smt(
+  const smt_termt &value_term,
+  const typet &type_to_construct,
+  const namespacet &ns,
+  const smt_object_mapt &object_map,
+  const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
+    &expression_identifiers);
+
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONSTRUCT_VALUE_EXPR_FROM_SMT_H

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -516,7 +516,11 @@ std::optional<exprt> smt2_incremental_decision_proceduret::get_expr(
       response.pretty()};
   }
   return construct_value_expr_from_smt(
-    get_value_response->pairs()[0].get().value(), type, ns);
+    get_value_response->pairs()[0].get().value(),
+    type,
+    ns,
+    object_map,
+    expression_identifiers);
 }
 
 // This is a fall back which builds resulting expression based on getting the