From 37896707577e2073bcfd5d35ee2d09786eafb36b Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 1 Sep 2021 13:27:26 +0100
Subject: [PATCH] enable nondeterministic pointers

This commit enables the use of nondeterministic pointers, to allow
declarative modeling of states that include pointers.
---
 regression/cbmc/Pointer14/main.c              |  4 +---
 .../String_Abstraction14/pass-in-implicit.c   |  2 +-
 .../cbmc/String_Abstraction20/structs2.c      |  2 +-
 .../double_deref_with_pointer_arithmetic.desc |  2 +-
 ..._with_pointer_arithmetic_single_alias.desc |  2 +-
 .../cbmc/nondet-pointer/nondet-pointer1.c     | 13 +++++++++++++
 .../cbmc/nondet-pointer/nondet-pointer1.desc  |  8 ++++++++
 .../cbmc/nondet-pointer/nondet-pointer2.c     | 14 ++++++++++++++
 .../cbmc/nondet-pointer/nondet-pointer2.desc  |  8 ++++++++
 .../cbmc/nondet-pointer/nondet-pointer3.c     | 18 ++++++++++++++++++
 .../cbmc/nondet-pointer/nondet-pointer3.desc  |  8 ++++++++
 .../cbmc/nondet-pointer/nondet-pointer4.c     | 18 ++++++++++++++++++
 .../cbmc/nondet-pointer/nondet-pointer4.desc  |  8 ++++++++
 .../cbmc/nondet-pointer/nondet-pointer5.c     | 19 +++++++++++++++++++
 .../cbmc/nondet-pointer/nondet-pointer5.desc  |  8 ++++++++
 src/pointer-analysis/value_set.cpp            | 18 +++++++++++++++++-
 16 files changed, 144 insertions(+), 8 deletions(-)
 create mode 100644 regression/cbmc/nondet-pointer/nondet-pointer1.c
 create mode 100644 regression/cbmc/nondet-pointer/nondet-pointer1.desc
 create mode 100644 regression/cbmc/nondet-pointer/nondet-pointer2.c
 create mode 100644 regression/cbmc/nondet-pointer/nondet-pointer2.desc
 create mode 100644 regression/cbmc/nondet-pointer/nondet-pointer3.c
 create mode 100644 regression/cbmc/nondet-pointer/nondet-pointer3.desc
 create mode 100644 regression/cbmc/nondet-pointer/nondet-pointer4.c
 create mode 100644 regression/cbmc/nondet-pointer/nondet-pointer4.desc
 create mode 100644 regression/cbmc/nondet-pointer/nondet-pointer5.c
 create mode 100644 regression/cbmc/nondet-pointer/nondet-pointer5.desc

diff --git a/regression/cbmc/Pointer14/main.c b/regression/cbmc/Pointer14/main.c
index fdcba62bc34..5f6543f7bef 100644
--- a/regression/cbmc/Pointer14/main.c
+++ b/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
 {
diff --git a/regression/cbmc/String_Abstraction14/pass-in-implicit.c b/regression/cbmc/String_Abstraction14/pass-in-implicit.c
index 547422d0649..3c2c5feb988 100644
--- a/regression/cbmc/String_Abstraction14/pass-in-implicit.c
+++ b/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)
 {
diff --git a/regression/cbmc/String_Abstraction20/structs2.c b/regression/cbmc/String_Abstraction20/structs2.c
index dd295ed05fd..e190cd0efc2 100644
--- a/regression/cbmc/String_Abstraction20/structs2.c
+++ b/regression/cbmc/String_Abstraction20/structs2.c
@@ -1,4 +1,4 @@
-void *malloc(unsigned);
+void *malloc(__CPROVER_size_t);
 
 typedef struct str_struct
 {
diff --git a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc
index df655168340..8a037e5ffda 100644
--- a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc
+++ b/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$
 --
diff --git a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc
index cf6fda8319a..39dcd3f91f1 100644
--- a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc
+++ b/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$
 --
diff --git a/regression/cbmc/nondet-pointer/nondet-pointer1.c b/regression/cbmc/nondet-pointer/nondet-pointer1.c
new file mode 100644
index 00000000000..d4378f7ac14
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/nondet-pointer/nondet-pointer1.desc b/regression/cbmc/nondet-pointer/nondet-pointer1.desc
new file mode 100644
index 00000000000..d4834e848eb
--- /dev/null
+++ b/regression/cbmc/nondet-pointer/nondet-pointer1.desc
@@ -0,0 +1,8 @@
+CORE
+nondet-pointer1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/nondet-pointer/nondet-pointer2.c b/regression/cbmc/nondet-pointer/nondet-pointer2.c
new file mode 100644
index 00000000000..d56fb806444
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/nondet-pointer/nondet-pointer2.desc b/regression/cbmc/nondet-pointer/nondet-pointer2.desc
new file mode 100644
index 00000000000..d4834e848eb
--- /dev/null
+++ b/regression/cbmc/nondet-pointer/nondet-pointer2.desc
@@ -0,0 +1,8 @@
+CORE
+nondet-pointer1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/nondet-pointer/nondet-pointer3.c b/regression/cbmc/nondet-pointer/nondet-pointer3.c
new file mode 100644
index 00000000000..d2bf7113643
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/nondet-pointer/nondet-pointer3.desc b/regression/cbmc/nondet-pointer/nondet-pointer3.desc
new file mode 100644
index 00000000000..d4834e848eb
--- /dev/null
+++ b/regression/cbmc/nondet-pointer/nondet-pointer3.desc
@@ -0,0 +1,8 @@
+CORE
+nondet-pointer1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/nondet-pointer/nondet-pointer4.c b/regression/cbmc/nondet-pointer/nondet-pointer4.c
new file mode 100644
index 00000000000..347f9e037c7
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/nondet-pointer/nondet-pointer4.desc b/regression/cbmc/nondet-pointer/nondet-pointer4.desc
new file mode 100644
index 00000000000..d4834e848eb
--- /dev/null
+++ b/regression/cbmc/nondet-pointer/nondet-pointer4.desc
@@ -0,0 +1,8 @@
+CORE
+nondet-pointer1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/nondet-pointer/nondet-pointer5.c b/regression/cbmc/nondet-pointer/nondet-pointer5.c
new file mode 100644
index 00000000000..fdd1e153055
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/nondet-pointer/nondet-pointer5.desc b/regression/cbmc/nondet-pointer/nondet-pointer5.desc
new file mode 100644
index 00000000000..d4834e848eb
--- /dev/null
+++ b/regression/cbmc/nondet-pointer/nondet-pointer5.desc
@@ -0,0 +1,8 @@
+CORE
+nondet-pointer1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 2deee5085ae..25234f31ba0 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/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));
   }