enable nondeterministic pointers

This commit enables the use of nondeterministic pointers, to allow
declarative modeling of states that include pointers.

Author: kroening

regression/cbmc/Pointer14/main.c

@@ -1,6 +1,4 @@
-typedef unsigned int size_t;
-
-void *malloc(size_t size);
+void *malloc(__CPROVER_size_t);
 
 enum blockstate
 {

regression/cbmc/String_Abstraction14/pass-in-implicit.c

@@ -1,4 +1,4 @@
-void *malloc(unsigned);
+void *malloc(__CPROVER_size_t);
 
 void use_str(char *s)
 {

regression/cbmc/String_Abstraction20/structs2.c

@@ -1,4 +1,4 @@
-void *malloc(unsigned);
+void *malloc(__CPROVER_size_t);
 
 typedef struct str_struct
 {

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc

@@ -2,7 +2,7 @@ CORE
 double_deref_with_pointer_arithmetic.c
 --show-vcc
 ^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object1#3\[\[0\]\], symex_dynamic::dynamic_object1#3\[\[1\]\] \}\[cast\(mod #source_location=""\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
-^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 2 : \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)\)
+^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 2 : main::argc!0@1#1 = 1
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc

@@ -1,7 +1,7 @@
 CORE
 double_deref_with_pointer_arithmetic_single_alias.c
 --show-vcc
-\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object2\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)
+\{1\} main::argc!0@1#1 = 1
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc/nondet-pointer/nondet-pointer1.c

@@ -0,0 +1,13 @@
+int *nondet_pointer();
+
+int main()
+{
+  int x = 123;
+  int *p = &x;
+  int *q = nondet_pointer();
+
+  if(p == q)
+    __CPROVER_assert(*q == 123, "value of *q");
+
+  return 0;
+}

regression/cbmc/nondet-pointer/nondet-pointer1.desc

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

regression/cbmc/nondet-pointer/nondet-pointer2.c

@@ -0,0 +1,14 @@
+int *nondet_pointer();
+
+int main()
+{
+  int x = 123, y = 456;
+  int *px = &x;
+  int *py = &y;
+  int *q = nondet_pointer();
+
+  if(q == px || q == py)
+    __CPROVER_assert(*q == 123 || *q == 456, "value of *q");
+
+  return 0;
+}

regression/cbmc/nondet-pointer/nondet-pointer2.desc

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

regression/cbmc/nondet-pointer/nondet-pointer3.c

@@ -0,0 +1,18 @@
+int *nondet_pointer();
+
+int main()
+{
+  int some_array[10];
+  int *p = some_array;
+  int *q = nondet_pointer();
+  int index;
+
+  __CPROVER_assume(index >= 0 && index < 10);
+  __CPROVER_assume(q == p);
+
+  q[index] = 123;
+
+  __CPROVER_assert(some_array[index] == 123, "value of array[index]");
+
+  return 0;
+}

regression/cbmc/nondet-pointer/nondet-pointer3.desc

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

regression/cbmc/nondet-pointer/nondet-pointer4.c

@@ -0,0 +1,18 @@
+int *nondet_pointer();
+
+int main()
+{
+  int some_array[10];
+  int *p = some_array;
+  int *q = nondet_pointer();
+  int index;
+
+  __CPROVER_assume(index >= 0 && index < 10);
+  __CPROVER_assume(q == p + index);
+
+  *q = 123;
+
+  __CPROVER_assert(some_array[index] == 123, "value of array[index]");
+
+  return 0;
+}

regression/cbmc/nondet-pointer/nondet-pointer4.desc

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

regression/cbmc/nondet-pointer/nondet-pointer5.c

@@ -0,0 +1,19 @@
+int *nondet_pointer();
+
+int main()
+{
+  int some_array[10];
+  int *p = some_array;
+  int *q = nondet_pointer();
+  int index;
+
+  __CPROVER_assume(index >= 0 && index < 10);
+  __CPROVER_assume(__CPROVER_same_object(p, q));
+  __CPROVER_assume(__CPROVER_POINTER_OFFSET(q) == sizeof(int) * index);
+
+  *q = 123;
+
+  __CPROVER_assert(some_array[index] == 123, "value of array[index]");
+
+  return 0;
+}

regression/cbmc/nondet-pointer/nondet-pointer5.desc

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

src/pointer-analysis/value_set.cpp

@@ -505,6 +505,23 @@ void value_sett::get_value_set_rec(
     else
       insert(dest, exprt(ID_unknown, original_type));
   }
+  else if(expr.id() == ID_nondet_symbol)
+  {
+    if(expr.type().id() == ID_pointer)
+    {
+      // we'll take the union of all objects we see, with unspecified offsets
+      values.iterate([this, &dest](const irep_idt &key, const entryt &value) {
+        for(const auto &object : value.object_map.read())
+          insert(dest, object.first, offsett());
+      });
+
+      // we'll add null, in case it's not there yet
+      insert(
+        dest,
+        exprt(ID_null_object, to_pointer_type(expr_type).subtype()),
+        offsett());
+    }
+  }
   else if(expr.id()==ID_if)
   {
     get_value_set_rec(
@@ -984,7 +1001,6 @@ void value_sett::get_value_set_rec(
   }
   else
   {
-    // for example: expr.id() == ID_nondet_symbol
     insert(dest, exprt(ID_unknown, original_type));
   }