Make pointer encoding sound wrt integer address translation (and lift object limits)

regression/cbmc/Pointer_Arithmetic12/test.desc

@@ -1,8 +1,10 @@
-CORE
+THOROUGH
 main.i
 --32 --little-endian
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+Takes around 2 minutes to run.

regression/cbmc/Pointer_Arithmetic13/test.desc

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

regression/cbmc/Pointer_Arithmetic18/main.c

@@ -0,0 +1,11 @@
+#define MB 0x00100000
+#define BASE (15 * MB)
+#define OFFSET (1 * MB)
+
+main()
+{
+  char *base = BASE;
+  int offset = OFFSET;
+  int n = 2;
+  __CPROVER_assert(&((char *)base)[offset] != 0, "no wrap-around expected");
+}

regression/cbmc/Pointer_Arithmetic18/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--32
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/Pointer_comparison1/main.c

@@ -0,0 +1,22 @@
+#include <stdlib.h>
+
+int main()
+{
+  if(sizeof(void *) != 8)
+    return 0;
+
+  char *p = malloc(1);
+  if(p == 0)
+    return 0;
+
+  if(
+    (unsigned long)p >
+    42) // unsoundly evaluates to true due to pointer encoding
+  {
+    return 0;
+  }
+
+  __CPROVER_assert(0, "");
+
+  return 0;
+}

regression/cbmc/Pointer_comparison1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/address_space_size_limit3/test.desc

@@ -1,4 +1,4 @@
-CORE
+THOROUGH
 main.i
 --32 --little-endian --object-bits 25 --pointer-check
 ^EXIT=10$

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -38,8 +38,12 @@ bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
 bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 {
   // array logic does not handle byte operators, thus lower when operating on
-  // unbounded arrays
-  if(is_unbounded_array(expr.op().type()))
+  // unbounded arrays; similarly, byte extracts over pointers are not to be
+  // handled here
+  if(
+    is_unbounded_array(expr.op().type()) ||
+    has_subtype(expr.type(), ID_pointer, ns) ||
+    has_subtype(expr.op().type(), ID_pointer, ns))
   {
     return convert_bv(lower_byte_extract(expr, ns));
   }

src/solvers/flattening/boolbv_byte_update.cpp

@@ -20,10 +20,13 @@ Author: Daniel Kroening, [email protected]
 bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 {
   // if we update (from) an unbounded array, lower the expression as the array
-  // logic does not handle byte operators
+  // logic does not handle byte operators; similarly, data types that contain
+  // pointers must not be handled here
   if(
     is_unbounded_array(expr.op().type()) ||
-    is_unbounded_array(expr.value().type()))
+    is_unbounded_array(expr.value().type()) ||
+    has_subtype(expr.value().type(), ID_pointer, ns) ||
+    has_subtype(expr.op0().type(), ID_pointer, ns))
   {
     return convert_bv(lower_byte_update(expr, ns));
   }

src/solvers/flattening/boolbv_width.cpp

@@ -11,8 +11,10 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 
 #include <util/arith_tools.h>
+#include <util/config.h>
 #include <util/exception_utils.h>
 #include <util/invariant.h>
+#include <util/namespace.h>
 #include <util/std_types.h>
 
 boolbv_widtht::boolbv_widtht(const namespacet &_ns):ns(_ns)
@@ -23,6 +25,21 @@ boolbv_widtht::~boolbv_widtht()
 {
 }
 
+std::size_t boolbv_widtht::get_object_width(const pointer_typet &type) const
+{
+  return type.get_width();
+}
+
+std::size_t boolbv_widtht::get_offset_width(const pointer_typet &type) const
+{
+  return type.get_width();
+}
+
+std::size_t boolbv_widtht::get_address_width(const pointer_typet &type) const
+{
+  return type.get_width();
+}
+
 const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
 {
   // check cache first
@@ -182,7 +199,12 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     CHECK_RETURN(entry.total_width > 0);
   }
   else if(type_id==ID_pointer)
-    entry.total_width = type_checked_cast<pointer_typet>(type).get_width();
+  {
+    const pointer_typet &t = type_checked_cast<pointer_typet>(type);
+    entry.total_width =
+      get_address_width(t) + get_object_width(t) + get_offset_width(t);
+    DATA_INVARIANT(entry.total_width != 0, "pointer must have width");
+  }
   else if(type_id==ID_struct_tag)
     entry=get_entry(ns.follow_tag(to_struct_tag_type(type)));
   else if(type_id==ID_union_tag)

src/solvers/flattening/boolbv_width.h

@@ -11,7 +11,8 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_SOLVERS_FLATTENING_BOOLBV_WIDTH_H
 
 #include <util/std_types.h>
-#include <util/namespace.h>
+
+class namespacet;
 
 class boolbv_widtht
 {
@@ -33,6 +34,10 @@ class boolbv_widtht
     const struct_typet &type,
     const irep_idt &member) const;
 
+  std::size_t get_object_width(const pointer_typet &type) const;
+  std::size_t get_offset_width(const pointer_typet &type) const;
+  std::size_t get_address_width(const pointer_typet &type) const;
+
 protected:
   const namespacet &ns;