numbered pointers for pointer->int

Author: kroening

regression/cbmc/Malloc15/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.i
 --32
 ^EXIT=0$

regression/cbmc/Pointer_array4/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.i
 --32
 ^EXIT=0$

regression/cbmc/printf1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG broken-smt-backend
+CORE broken-smt-backend
 main.c
 --trace
 ^EXIT=10$

regression/cbmc/trace-strings/test.desc

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

regression/cbmc/trace-values/trace-values.desc

@@ -1,4 +1,4 @@
-KNOWNBUG broken-smt-backend
+CORE broken-smt-backend
 trace-values.c
 --trace
 ^EXIT=10$

regression/cbmc/trace-values/unbounded_array.desc

@@ -1,4 +1,4 @@
-KNOWNBUG broken-smt-backend
+CORE broken-smt-backend
 unbounded_array.c
 --trace
 \{ \[0u?l?l?\]=1, \[1u?l?l?\]=2, \[\d+u?l?l?\]=42 \}

regression/cbmc/trace_address_arithmetic1/test.desc

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

src/goto-programs/goto_trace.cpp

@@ -246,7 +246,8 @@ std::string trace_numeric_value(
   {
     const auto &annotated_pointer_constant =
       to_annotated_pointer_constant_expr(expr);
-    auto width = to_pointer_type(expr.type()).get_width();
+    // pointers use double-width
+    auto width = 2 * to_pointer_type(expr.type()).get_width();
     auto &value = annotated_pointer_constant.get_value();
     auto c = constant_exprt(value, unsignedbv_typet(width));
     return numeric_representation(c, ns, options);

src/solvers/flattening/bv_pointers.cpp

@@ -729,17 +729,28 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
     expr.id() == ID_typecast &&
     to_typecast_expr(expr).op().type().id() == ID_pointer)
   {
-    // pointer to int
-    bvt op0 = convert_pointer_type(to_typecast_expr(expr).op());
+    // Pointer to int.
+    // We special-case NULL, which should always yield 0.
+    // Otherwise, we 'number' these.
+    const auto &pointer_expr = to_typecast_expr(expr).op();
+    const bvt pointer_bv = convert_pointer_type(pointer_expr);
+    const auto is_null = bv_utils.is_zero(pointer_bv);
+    const auto target_width = boolbv_width(expr.type());
+
+    if(target_width == 0)
+      return conversion_failed(expr);
 
-    // squeeze it in!
+    if(numbered_pointers.empty())
+      numbered_pointers.emplace_back(bvt{});
 
-    std::size_t width=boolbv_width(expr.type());
+    const auto number = numbered_pointers.size();
 
-    if(width==0)
-      return conversion_failed(expr);
+    numbered_pointers.push_back(pointer_bv);
 
-    return bv_utils.zero_extension(op0, width);
+    return bv_utils.select(
+      is_null,
+      bv_utils.zeros(target_width),
+      bv_utils.build_constant(number, target_width));
   }
   else if(expr.id() == ID_object_address)
   {

src/solvers/flattening/bv_pointers.h

@@ -108,6 +108,10 @@ class bv_pointerst:public boolbvt
   /// \param offset: Encoded offset
   /// \return Pointer encoding
   static bvt object_offset_encoding(const bvt &object, const bvt &offset);
+
+  /// Table that maps a 'pointer number' to its full-width bit-vector.
+  /// Used for conversion of pointers to integers.
+  std::vector<bvt> numbered_pointers;
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H