Adds support for null pointers passed as function call parameter.

This adds support for the cases where a null pointer is passed as
a parameter to a function that may assign to it. We add checks in
goto program to handle such instances as special cases of assigns
clause handling.

Author: ArenBabikian

regression/contracts/assigns_validity_pointer_01/main.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+#include <stddef.h>
+
+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 foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == 3)
+{
+  bar(x, NULL);
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  assert(n == 3);
+  return 0;
+}

regression/contracts/assigns_validity_pointer_01/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-contract foo --replace-call-with-contract bar
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks support for a NULL pointer passed as a parameter to a
+function that may assign to it. The NULL pointer is passed to function
+bar which has been replaced by it's 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,26 @@
+#include <assert.h>
+#include <stddef.h>
+
+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 foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == 3)
+{
+  bar(x, NULL);
+  *x = 3;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  assert(n == 3);
+  return 0;
+}

regression/contracts/assigns_validity_pointer_02/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks support for a NULL pointer passed as a parameter to a
+function that may assign to it. The NULL pointer is passed to function
+bar, while the calling function foo is being checked (by enforcing
+it's function contracts).

regression/contracts/assigns_validity_pointer_03/main.c

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

regression/contracts/assigns_validity_pointer_03/test.desc

@@ -0,0 +1,18 @@
+KNOWNBUG
+main.c
+--enforce-contract foo --replace-call-with-contract bar
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks support for an uninitialized pointer passed as a parameter
+to a function that may assign to it. The uninitialized pointer is passed to
+function bar which has been replaced by it's 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,24 @@
+#include <assert.h>
+#include <stddef.h>
+
+void bar(int *x, int *y) __CPROVER_assigns(*x, *y) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == 3 && *y == 5)
+{
+}
+
+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);
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  assert(n == 3);
+  return 0;
+}

regression/contracts/assigns_validity_pointer_04/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-contract foo --replace-call-with-contract bar
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks support for a malloced pointer passed as a parameter
+to a function that may assign to it. The malloced pointer is passed to
+function bar which has been replaced by it's function contracts, while the
+calling function foo is being checked (by enforcing it's function contracts).
+

src/goto-instrument/code_contracts.cpp

@@ -1542,11 +1542,43 @@ 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));
+
+    if(
+      to_address_of_expr(target->get_direct_pointer()).object().id() ==
+      ID_dereference)
+    {
+      // create the condition
+      exprt condition = not_exprt(w_ok_exprt(
+        target->get_direct_pointer(), 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->get_direct_pointer()).object().id() ==
+      ID_dereference)
+    {
+      // add the z label instruction
+      havoc_statements.destructive_append(tmp_z);
+    }
   }
   return havoc_statements;
 }
@@ -1595,8 +1627,27 @@ 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
+        if(
+          to_address_of_expr(called_target->get_direct_pointer())
+            .object()
+            .id() == ID_dereference)
+        {
+          current_target_compatible = or_exprt(
+            not_exprt(w_ok_exprt(
+              called_target->get_direct_pointer(),
+              from_integer(0, integer_typet()))),
+            target->compatible_expression(*called_target));
+        }
+        else
+        {
+          current_target_compatible =
+            target->compatible_expression(*called_target);
+        }
         first_iter = false;
       }
       else