Check for validity of pointers in assigns clause

regression/contracts/assigns_replace_03/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --replace-all-calls-with-contracts
 ^EXIT=0$
@@ -7,3 +7,7 @@ main.c
 --
 --
 This test checks that a havocked variable can be constrained by a function post-condition.
+
+Known Bug:
+Currently, there is a bug when char variables are being passed to
+__CPROVER_w_ok(). See GitHub issue #6106 for further details.

regression/contracts/assigns_validity_pointer_01/main.c

@@ -0,0 +1,36 @@
+#include <assert.h>
+#include <stddef.h>
+
+int *z;
+
+void bar(int *x, int *y) __CPROVER_assigns(*x, *y) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == 3 && (y == NULL || *y == 5))
+{
+  *x = 3;
+  if(y != NULL)
+    *y = 5;
+}
+
+void baz() __CPROVER_assigns(*z) __CPROVER_ensures(z == NULL || *z == 7)
+{
+  if(z != NULL)
+    *z = 7;
+}
+
+void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == 3)
+{
+  bar(x, NULL);
+  z == NULL;
+  baz();
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  assert(n == 3);
+  assert(z == NULL || *z == 7);
+  return 0;
+}

regression/contracts/assigns_validity_pointer_01/test.desc

@@ -0,0 +1,29 @@
+CORE
+main.c
+--enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+SUCCESS
+// bar
+ASSERT \*x > 0
+IF !\(\*x == 3\) THEN GOTO \d
+IF !\(\(signed int \*\)\(void \*\)0 == \(\(signed int \*\)NULL\)\) THEN GOTO \d
+tmp_if_expr = \*\(\(signed int \*\)\(void \*\)0\) == 5 \? TRUE \: FALSE;
+tmp_if_expr\$\d = tmp_if_expr \? TRUE : FALSE;
+ASSUME tmp_if_expr\$\d
+// baz
+IF !\(z == \(\(signed int \*\)NULL\)\) THEN GOTO \d
+tmp_if_expr\$\d = \*z == 7 \? TRUE : FALSE;
+ASSUME tmp_if_expr\$\d
+// foo
+ASSUME \*tmp_cc\$\d > 0
+ASSERT \*tmp_cc\$\d == 3
+--
+\[3\] file main\.c line 6 assertion: FAILURE
+--
+Verification:
+This test checks support for a NULL pointer that is assigned to by
+a function (bar and baz). Both functions bar and baz are being replaced by
+their function contracts, while the calling function foo is being checked
+(by enforcing it's function contracts).

regression/contracts/assigns_validity_pointer_02/main.c

@@ -0,0 +1,36 @@
+#include <assert.h>
+#include <stddef.h>
+
+int *z;
+
+void bar(int *x, int *y) __CPROVER_assigns(*x, *y) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == 3 && (y == NULL || *y == 5))
+{
+  *x = 3;
+  if(y != NULL)
+    *y = 5;
+}
+
+void baz() __CPROVER_assigns(*z) __CPROVER_ensures(z == NULL || *z == 7)
+{
+  if(z != NULL)
+    *z = 7;
+}
+
+void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == 3)
+{
+  bar(x, NULL);
+  *x = 3;
+  z == NULL;
+  baz();
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  assert(n == 3);
+  return 0;
+}

regression/contracts/assigns_validity_pointer_02/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+//^([foo\.1] line 15 assertion: FAILURE)
+// foo
+ASSUME \*tmp_cc\$\d > 0
+ASSERT \*tmp_cc\$\d == 3
+--
+\[foo\.1\] line 24 assertion: FAILURE
+\[foo\.3\] line 27 assertion: FAILURE
+--
+Verification:
+This test checks support for a NULL pointer that is assigned to by
+a function (bar and baz). The calling function foo is being checked
+(by enforcing it's function contracts). As for bar and baz, their
+function contracts are ot being considered for this test.

regression/contracts/assigns_validity_pointer_03/main.c

@@ -0,0 +1,33 @@
+#include <assert.h>
+#include <stddef.h>
+
+int *z;
+
+void bar(int *x, int *y) __CPROVER_assigns(*x, *y) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == 3 && *y == 5)
+{
+}
+
+void baz() __CPROVER_assigns(*z) __CPROVER_ensures(*z == 7)
+{
+}
+
+void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == 3)
+{
+  int *y;
+  bar(x, y);
+  assert(*y == 5);
+
+  baz();
+  assert(*z == 7);
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  assert(n == 3);
+  return 0;
+}

regression/contracts/assigns_validity_pointer_03/test.desc

@@ -0,0 +1,28 @@
+KNOWNBUG
+main.c
+--enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+// bar
+ASSERT \*x > 0
+IF !\(\*x == 3\) THEN GOTO \d
+tmp_if_expr = \*y == 5 \? TRUE \: FALSE;
+ASSUME tmp_if_expr
+// baz
+ASSUME \*z == 7
+// foo
+ASSUME \*tmp_cc\$\d > 0
+ASSERT \*tmp_cc\$\d == 3
+--
+--
+Verification:
+This test checks support for an uninitialized pointer that is assigned to by
+a function (bar and baz). Both functions bar and baz are being replaced by
+their function contracts, while the calling function foo is being checked
+(by enforcing it's function contracts).
+
+Known Bug:
+Currently, there is a known issue with __CPROVER_w_ok(ptr, 0) such that it
+returns true if ptr is uninitialized. This is not the expected behavior,
+therefore, the outcome of this test case is currently incorrect.

regression/contracts/assigns_validity_pointer_04/main.c

@@ -0,0 +1,34 @@
+#include <assert.h>
+#include <stddef.h>
+
+int *z;
+
+void bar(int *x, int *y) __CPROVER_assigns(*x, *y) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == 3 && *y == 5)
+{
+}
+
+void baz() __CPROVER_assigns(*z) __CPROVER_ensures(*z == 7)
+{
+}
+
+void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == 3)
+{
+  int *y = malloc(sizeof(int));
+  bar(x, y);
+  assert(*y == 5);
+
+  z = malloc(sizeof(int));
+  baz();
+  assert(*z == 7);
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  assert(n == 3);
+  return 0;
+}

regression/contracts/assigns_validity_pointer_04/test.desc

@@ -0,0 +1,23 @@
+CORE
+main.c
+--enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+// bar
+ASSERT \*x > 0
+IF !\(\*x == 3\) THEN GOTO \d
+tmp_if_expr = \*y == 5 \? TRUE \: FALSE;
+ASSUME tmp_if_expr
+// baz
+ASSUME \*z == 7
+// foo
+ASSUME \*tmp_cc\$\d > 0
+ASSERT \*tmp_cc\$\d == 3
+--
+--
+Verification:
+This test checks support for a malloced pointer that is assigned to by
+a function (bar and baz). Both functions bar and baz are being replaced by
+their function contracts, while the calling function foo is being checked
+(by enforcing it's function contracts).

src/goto-instrument/code_contracts.cpp

@@ -1524,11 +1524,40 @@ goto_programt assigns_clauset::havoc_code(
   goto_programt havoc_statements;
   for(assigns_clause_targett *target : targets)
   {
+    // (1) If the assigned target is not a dereference,
+    // only include the havoc_statement
+
+    // (2) If the assigned target is a dereference, do the following:
+
+    // if(!__CPROVER_w_ok(target, 0)) goto z;
+    //      havoc_statements
+    // z: skip
+
+    // create the z label
+    goto_programt tmp_z;
+    goto_programt::targett z = tmp_z.add(goto_programt::make_skip(location));
+
+    const auto &target_ptr = target->get_direct_pointer();
+    if(to_address_of_expr(target_ptr).object().id() == ID_dereference)
+    {
+      // create the condition
+      exprt condition =
+        not_exprt(w_ok_exprt(target_ptr, from_integer(0, integer_typet())));
+      havoc_statements.add(goto_programt::make_goto(z, condition, location));
+    }
+
+    // create havoc_statements
     for(goto_programt::instructiont instruction :
         target->havoc_code(location).instructions)
     {
       havoc_statements.add(std::move(instruction));
     }
+
+    if(to_address_of_expr(target_ptr).object().id() == ID_dereference)
+    {
+      // add the z label instruction
+      havoc_statements.destructive_append(tmp_z);
+    }
   }
   return havoc_statements;
 }
@@ -1577,8 +1606,28 @@ exprt assigns_clauset::compatible_expression(
     {
       if(first_iter)
       {
-        current_target_compatible =
-          target->compatible_expression(*called_target);
+        // TODO: Optimize the validation below and remove code duplication
+        // See GitHub issue #6105 for further details
+
+        // Validating the called target through __CPROVER_w_ok() is
+        // only useful when the called target is a dereference
+        const auto &called_target_ptr = called_target->get_direct_pointer();
+        if(
+          to_address_of_expr(called_target_ptr).object().id() == ID_dereference)
+        {
+          // or_exprt is short-circuited, therefore
+          // target->compatible_expression(*called_target) would not be
+          // checked on invalid called_targets.
+          current_target_compatible = or_exprt(
+            not_exprt(
+              w_ok_exprt(called_target_ptr, from_integer(0, integer_typet()))),
+            target->compatible_expression(*called_target));
+        }
+        else
+        {
+          current_target_compatible =
+            target->compatible_expression(*called_target);
+        }
         first_iter = false;
       }
       else