From 86858a61463690d0a1072cc0aa7d6ecb13032b59 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 21 May 2019 19:47:14 +0000
Subject: [PATCH] Fix value-set construction for non-deterministic pointer
 values

The value-set based filtering (rightfully) expects a value-set to be
non-empty. As we previously ignored some right-hand sides, notably
non-det symbols, this wasn't guaranteed.

This entails changes to the tests of let-expression use in dereferencing
as some of those tests have non-deterministically initialised arrays.
Changes as discussed with @smowton.
---
 .../double_deref_with_pointer_arithmetic.desc         |  2 +-
 ...le_deref_with_pointer_arithmetic_single_alias.desc |  4 +---
 regression/cbmc/null5/main.c                          | 10 ++++++++++
 regression/cbmc/null5/test.desc                       | 11 +++++++++++
 src/pointer-analysis/value_set.cpp                    |  5 ++---
 5 files changed, 25 insertions(+), 7 deletions(-)
 create mode 100644 regression/cbmc/null5/main.c
 create mode 100644 regression/cbmc/null5/test.desc

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 4328a111fa9..22f1388d331 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\[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 : main::argc!0@1#1 = 1\)
+^\{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\)\)
 ^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 596be52269b..cf6fda8319a 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,10 +1,8 @@
 CORE
 double_deref_with_pointer_arithmetic_single_alias.c
 --show-vcc
-\{1\} main::argc!0@1#1 = 1
+\{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\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
-derefd_pointer::derefd_pointer
---
 See README for details about these tests
diff --git a/regression/cbmc/null5/main.c b/regression/cbmc/null5/main.c
new file mode 100644
index 00000000000..0b1734064cc
--- /dev/null
+++ b/regression/cbmc/null5/main.c
@@ -0,0 +1,10 @@
+int *nondet_ptr();
+
+int main()
+{
+  int *ptr;
+  ptr = nondet_ptr();
+  if(ptr == 0)
+    return;
+  __CPROVER_assert(ptr != 0, "pointer cannot be null");
+}
diff --git a/regression/cbmc/null5/test.desc b/regression/cbmc/null5/test.desc
new file mode 100644
index 00000000000..926be8072d2
--- /dev/null
+++ b/regression/cbmc/null5/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Pull request #4444 introduced optimisations during symbolic execution that
+caused this test to spuriously fail (as the branch `ptr == 0` was removed).
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 352fdab1c50..1a4f426c236 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -976,9 +976,8 @@ void value_sett::get_value_set_rec(
   }
   else
   {
-    #if 0
-    std::cout << "WARNING: not doing " << expr.id() << '\n';
-    #endif
+    // for example: expr.id() == ID_nondet_symbol
+    insert(dest, exprt(ID_unknown, original_type));
   }
 
   #ifdef DEBUG