From d7b38f160e2c6725135069549c2ef849a307ba3b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 5 Jan 2022 17:36:57 +0000
Subject: [PATCH] Value sets must not return an empty set for nondet symbols

Even when the expression type is not immediately a pointer, some
component of the type may be a pointer. As such, it could legitimately
appear in pointer dereferencing, and we should at least add "unknown" to
the value set.

This is a follow-up fix to 378967075: the regression test included
yields a spurious counterexample in versions between 378967075 and this
bugfix commit. This commit also reverts the (spurious) changes to the
double_deref/* regression tests.
---
 .../double_deref_with_pointer_arithmetic.desc     |  2 +-
 ...eref_with_pointer_arithmetic_single_alias.desc |  2 +-
 .../symex_should_exclude_null_pointers/nondet.c   | 15 +++++++++++++++
 .../nondet.desc                                   | 11 +++++++++++
 src/pointer-analysis/value_set.cpp                |  2 ++
 5 files changed, 30 insertions(+), 2 deletions(-)
 create mode 100644 regression/cbmc/symex_should_exclude_null_pointers/nondet.c
 create mode 100644 regression/cbmc/symex_should_exclude_null_pointers/nondet.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 8a037e5ffda..df655168340 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 : 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 39dcd3f91f1..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,7 +1,7 @@
 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$
 --
diff --git a/regression/cbmc/symex_should_exclude_null_pointers/nondet.c b/regression/cbmc/symex_should_exclude_null_pointers/nondet.c
new file mode 100644
index 00000000000..03a8c961b43
--- /dev/null
+++ b/regression/cbmc/symex_should_exclude_null_pointers/nondet.c
@@ -0,0 +1,15 @@
+#include <stdlib.h>
+
+struct S
+{
+  int *p;
+  int x;
+};
+
+int main()
+{
+  struct S *s = malloc(sizeof(struct S));
+  // Guard must not be removed (deemed trivially true) by try_filter_value_sets.
+  if(s->p != NULL)
+    __CPROVER_assert(s->p != NULL, "cannot be NULL");
+}
diff --git a/regression/cbmc/symex_should_exclude_null_pointers/nondet.desc b/regression/cbmc/symex_should_exclude_null_pointers/nondet.desc
new file mode 100644
index 00000000000..e62d8efa884
--- /dev/null
+++ b/regression/cbmc/symex_should_exclude_null_pointers/nondet.desc
@@ -0,0 +1,11 @@
+CORE
+nondet.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+try_filter_value_sets must not end up in a situation where it deems the guard
+trivially true. This situation arises when the value set wrongly is empty.
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 25234f31ba0..0c083ee0627 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -521,6 +521,8 @@ void value_sett::get_value_set_rec(
         exprt(ID_null_object, to_pointer_type(expr_type).subtype()),
         offsett());
     }
+    else
+      insert(dest, exprt(ID_unknown, original_type));
   }
   else if(expr.id()==ID_if)
   {