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 no way to check if an assigned pointer is invalid (which
+may be the case for uninitialized pointers). We do handle NULL pointers as a
+special case, however, we do not yet have a way to handle invalid pointer.

src/goto-instrument/code_contracts.cpp

@@ -1542,11 +1542,38 @@ goto_programt assigns_clauset::havoc_code(
   goto_programt havoc_statements;
   for(assigns_clause_targett *target : targets)
   {
+    //    if(target != NULL) goto x;
+    //      havoc_statements
+    // z: skip
+
+    // create the z label
+    goto_programt tmp_z;
+    goto_programt::targett z = tmp_z.add(goto_programt::make_skip(location));
+
+    // TODO: generalize this. Currently only supports pointers
+    // See GitHub issue #6087 for further details
+    if(target->target_type == assigns_clause_targett::target_type::Scalar)
+    {
+      exprt condition = equal_exprt(
+        target->get_direct_pointer(),
+        null_pointer_exprt(
+          to_pointer_type(target->get_direct_pointer().type())));
+
+      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(target->target_type == assigns_clause_targett::target_type::Scalar)
+    {
+      // add the z label instruction
+      havoc_statements.destructive_append(tmp_z);
+    }
   }
   return havoc_statements;
 }
@@ -1595,9 +1622,23 @@ exprt assigns_clauset::compatible_expression(
     {
       if(first_iter)
       {
-        current_target_compatible =
-          target->compatible_expression(*called_target);
-        first_iter = false;
+        // TODO: generalize this. Currently only supports pointers
+        // See GitHub issue #6087 for further details
+        if(target->target_type == assigns_clause_targett::target_type::Scalar)
+        {
+          current_target_compatible = or_exprt(
+            equal_exprt(
+              called_target->get_direct_pointer(),
+              null_pointer_exprt(
+                to_pointer_type(called_target->get_direct_pointer().type()))),
+            target->compatible_expression(*called_target));
+        }
+        else
+        {
+          current_target_compatible =
+            target->compatible_expression(*called_target);
+          first_iter = false;
+        }
       }
       else
       {