Fix for getting values of pointers in traces in new SMT backend

regression/cbmc-incr-smt2/pointers/pointer_values.c

@@ -0,0 +1,12 @@
+int main()
+{
+  int *a;
+  int *b = 0;
+  int *c;
+  __CPROVER_assume(c != 0);
+
+  __CPROVER_assert(
+    a != b, "should fail because a can be any pointer val, including NULL");
+  __CPROVER_assert(
+    a != c, "should fail because a and c can point to same object");
+}

regression/cbmc-incr-smt2/pointers/pointer_values.desc

@@ -0,0 +1,12 @@
+CORE
+pointer_values.c
+--trace
+\[main\.assertion\.1\] line \d+ should fail because a can be any pointer val, including NULL: FAILURE
+\[main\.assertion\.2\] line \d+ should fail because a and c can point to same object: FAILURE
+a=\(\(signed int \*\)NULL\)
+c=\(signed int \*\)1
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test printing of NULL pointer values in trace.

regression/cbmc-incr-smt2/pointers/pointer_values_2.c

@@ -0,0 +1,8 @@
+int main()
+{
+  int *a;
+  int *b;
+  __CPROVER_assume(a == 0xDEADBEEF);
+
+  __CPROVER_assert(a != b, "should fail as b can also be assigned 0xDEADBEEF");
+}

regression/cbmc-incr-smt2/pointers/pointer_values_2.desc

@@ -0,0 +1,12 @@
+CORE
+pointer_values_2.c
+--trace --slice-formula
+\[main\.assertion\.1\] line \d should fail as b can also be assigned 0xDEADBEEF: FAILURE
+a=\(signed int \*\)3735928559
+b=\(signed int \*\)3735928559
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+3735928559 is the decimal value of the hex constant 0xDEADBEEF that
+the pointer is assumed to point to in this example.

src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp

@@ -1,15 +1,15 @@
 // Author: Diffblue Ltd.
 
-#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
-
-#include <solvers/smt2_incremental/smt_terms.h>
-
 #include <util/arith_tools.h>
 #include <util/bitvector_types.h>
+#include <util/pointer_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/type.h>
 
+#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
+#include <solvers/smt2_incremental/smt_terms.h>
+
 class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
 {
 private:
@@ -37,13 +37,35 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
 
   void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override
   {
+    const auto sort_width = bit_vector_constant.get_sort().bit_width();
+    if(
+      const auto pointer_type =
+        type_try_dynamic_cast<pointer_typet>(type_to_construct))
+    {
+      INVARIANT(
+        pointer_type->get_width() == sort_width,
+        "Width of smt bit vector term must match the width of pointer type.");
+      if(bit_vector_constant.value() == 0)
+      {
+        result = null_pointer_exprt{*pointer_type};
+      }
+      else
+      {
+        // The reason we are manually constructing a constant_exprt here is a
+        // limitation in the design of `from_integer`, which only allows it to
+        // be used with pointer values of 0 (null pointers).
+        result = constant_exprt{
+          integer2bvrep(bit_vector_constant.value(), sort_width),
+          *pointer_type};
+      }
+      return;
+    }
     if(
       const auto bitvector_type =
         type_try_dynamic_cast<bitvector_typet>(type_to_construct))
     {
       INVARIANT(
-        bitvector_type->get_width() ==
-          bit_vector_constant.get_sort().bit_width(),
+        bitvector_type->get_width() == sort_width,
         "Width of smt bit vector term must match the width of bit vector "
         "type.");
       result = from_integer(bit_vector_constant.value(), type_to_construct);

unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp

@@ -68,6 +68,16 @@ TEST_CASE("Value expr construction from smt.", "[core][smt2_incremental]")
     rowt{smt_bool_literal_termt{false}, false_exprt{}},
     rowt{smt_bit_vector_constant_termt{0, 8}, from_integer(0, c_bool_typet(8))},
     rowt{smt_bit_vector_constant_termt{1, 8}, from_integer(1, c_bool_typet(8))},
+    rowt{
+      smt_bit_vector_constant_termt{0, 64},
+      from_integer(0, pointer_typet(void_type(), 64 /* bits */))},
+    // The reason for the more intricate elaboration of a pointer with a value
+    // of 12 is a limitation in the design of from_integer, which only handles
+    // pointers with value 0 (null pointers).
+    rowt{
+      smt_bit_vector_constant_termt{12, 64},
+      constant_exprt(
+        integer2bvrep(12, 64), pointer_typet(void_type(), 64 /* bits */))},
     UNSIGNED_BIT_VECTOR_TESTS(8),
     SIGNED_BIT_VECTOR_TESTS(8),
     UNSIGNED_BIT_VECTOR_TESTS(16),
@@ -96,23 +106,31 @@ TEST_CASE(
 
   using rowt = std::tuple<smt_termt, typet, std::string>;
   std::tie(input_term, input_type, invariant_reason) = GENERATE(
-    rowt{smt_bool_literal_termt{true},
-         unsignedbv_typet{16},
-         "Bool terms may only be used to construct bool typed expressions."},
-    rowt{smt_identifier_termt{"foo", smt_bit_vector_sortt{16}},
-         unsignedbv_typet{16},
-         "Unexpected conversion of identifier to value expression."},
+    rowt{
+      smt_bool_literal_termt{true},
+      unsignedbv_typet{16},
+      "Bool terms may only be used to construct bool typed expressions."},
+    rowt{
+      smt_identifier_termt{"foo", smt_bit_vector_sortt{16}},
+      unsignedbv_typet{16},
+      "Unexpected conversion of identifier to value expression."},
     rowt{
       smt_bit_vector_constant_termt{0, 8},
       unsignedbv_typet{16},
       "Width of smt bit vector term must match the width of bit vector type."},
-    rowt{smt_bit_vector_constant_termt{0, 8},
-         empty_typet{},
-         "construct_value_expr_from_smt for bit vector should not be applied "
-         "to unsupported type empty"},
-    rowt{smt_core_theoryt::make_not(smt_bool_literal_termt{true}),
-         unsignedbv_typet{16},
-         "Unexpected conversion of function application to value expression."});
+    rowt{
+      smt_bit_vector_constant_termt{0, 8},
+      empty_typet{},
+      "construct_value_expr_from_smt for bit vector should not be applied "
+      "to unsupported type empty"},
+    rowt{
+      smt_core_theoryt::make_not(smt_bool_literal_termt{true}),
+      unsignedbv_typet{16},
+      "Unexpected conversion of function application to value expression."},
+    rowt{
+      smt_bit_vector_constant_termt{0, 16},
+      pointer_typet{unsigned_int_type(), 0},
+      "Width of smt bit vector term must match the width of pointer type"});
   SECTION(invariant_reason)
   {
     const cbmc_invariants_should_throwt invariants_throw;