re-encode integers converted to pointers

Author: kroening

regression/cbmc-library/fprintf-01/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test-no-cp.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --no-simplify --no-propagation
 ^EXIT=0$

regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc/memory_allocation1/test.desc

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

regression/cbmc/mm_io1/test.desc

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

regression/cbmc/pointer-extra-checks/test.desc

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

src/solvers/flattening/bv_pointers.cpp

@@ -76,29 +76,29 @@ bvt bv_pointerst::object_literals(const bvt &bv, const pointer_typet &type)
   PRECONDITION(width == bv.size());
 
   const auto result = prop.new_variables(width);
-  bvt match_found;
+  bvt match_found_disjuncts;
 
   for(std::size_t i = 0; i < numbered_pointers.size(); i++)
   {
     auto cond = bv_utils.equal(
       bv,
       bv_utilst::concatenate(
         bv_utilst::build_constant(i, width - 1), {const_literal(true)}));
-    match_found.push_back(cond);
+    match_found_disjuncts.push_back(cond);
     bv_utils.cond_implies_equal(
       cond,
       bv_utilst::zero_extension(numbered_pointers[i].first, width),
       result);
   }
 
-  auto within_bounds = prop.lor(match_found);
+  auto match_found = prop.lor(match_found_disjuncts);
 
   // The top bit distinguishes 'object only' vs. 'table encoded'.
   // When outside of the table, return an invalid object.
   return bv_utils.select(
     bv.back(),
     bv_utils.select(
-      within_bounds,
+      match_found,
       result,
       bv_utilst::build_constant(pointer_logic.get_invalid_object(), width)),
     bv);
@@ -110,21 +110,28 @@ bvt bv_pointerst::offset_literals(const bvt &bv, const pointer_typet &type)
   PRECONDITION(width == bv.size());
 
   const auto result = prop.new_variables(width);
+  bvt match_found_disjuncts;
 
   for(std::size_t i = 0; i < numbered_pointers.size(); i++)
   {
     auto cond = bv_utils.equal(
       bv,
       bv_utilst::concatenate(
         bv_utilst::build_constant(i, width - 1), {const_literal(true)}));
+    match_found_disjuncts.push_back(cond);
     bv_utils.cond_implies_equal(
       cond,
       bv_utilst::sign_extension(numbered_pointers[i].second, width),
       result);
   }
 
+  auto match_found = prop.lor(match_found_disjuncts);
+
   // the top bit distinguishes 'object only' vs. 'table encoded'
-  return bv_utils.select(bv.back(), result, bv_utilst::zeros(width));
+  return bv_utils.select(
+    bv.back(),
+    bv_utils.select(match_found, result, bv_utilst::zeros(width)),
+    bv_utilst::zeros(width));
 }
 
 bvt bv_pointerst::object_offset_encoding(
@@ -436,11 +443,11 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
       op_type.id() == ID_c_enum || op_type.id() == ID_c_enum_tag)
     {
       // Cast from a bitvector type to pointer.
-      // We just do a zero extension.
-
+      // We interpret as NULL + offset, where the offset is
+      // derived from the bitvector by zero extension.
       const bvt &op_bv=convert_bv(op);
-
-      return bv_utils.zero_extension(op_bv, bits);
+      return object_offset_encoding(
+        bv_utilst::zeros(bits), bv_utilst::zero_extension(op_bv, bits), type);
     }
   }
   else if(expr.id()==ID_if)