Encode integer addresses together with pointer object/offset

Instead of encoding pointers with the same bit width a pointer on a given
platform has, just widen the bit-blasted encoding to include both the previous
object/offset encoding as well as an (integer) address. The encoding is thus
also trivially extended to handle larger numbers of objects and offsets of the
same width as the address.

Furthermore clean up the code to encapsulate encoding properly, and make in-code
layout of pointer encoding more natural (it's now object, offset,
integer-address).

Fixes: diffblue#436
Fixes: diffblue#311
Fixes: diffblue#94

Author: tautschnig

regression/cbmc/Pointer_Arithmetic12/test.desc

@@ -1,8 +1,10 @@
-CORE
+THOROUGH
 main.c
 --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_Arithmetic14/main.c

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

regression/cbmc/Pointer_Arithmetic14/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,19 @@
+#include <stdlib.h>
+
+int main()
+{
+  if(sizeof(void*)!=8)
+    return 0;
+
+  char* p=malloc(1);
+  if(p==0)
+    return 0;
+
+  unsigned long x=0xFFFFFFFF;
+  if((unsigned long)p > x) // 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_limit1/test.c

@@ -194,7 +194,10 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     // no width
   }
   else if(type_id==ID_pointer)
-    entry.total_width = type_checked_cast<pointer_typet>(type).get_width();
+  {
+    entry.total_width = 3 * type_checked_cast<pointer_typet>(type).get_width();
+    DATA_INVARIANT(entry.total_width != 0, "pointer must have width");
+  }
   else if(type_id==ID_symbol)
     entry=get_entry(ns.follow(type));
   else if(type_id==ID_struct_tag)