Merge pull request #6546 from remi-delmas-3000/guarded-assigns-targets

Function contracts: preliminary support for conditional targets in assigns clause checking

Author: remi-delmas-3000

regression/contracts/assigns_enforce_address_of/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: non-lvalue target in assigns clause$
+^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_conditional_function_call_condition/main.c

@@ -0,0 +1,33 @@
+#include <stdbool.h>
+
+bool cond()
+{
+  return true;
+}
+
+int foo(int a, int *x, int *y)
+  // clang-format off
+__CPROVER_assigns(a && cond() : *x)
+// clang-format on
+{
+  if(a)
+  {
+    if(cond())
+      *x = 0; // must pass
+  }
+  else
+  {
+    *x = 0; // must fail
+  }
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+
+  foo(a, &x, &y);
+  return 0;
+}

regression/contracts/assigns_enforce_conditional_function_call_condition/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-contract foo
+^main.c function foo$
+^\[foo\.\d+\] line 16 Check that \*x is assignable: SUCCESS$
+^\[foo\.\d+\] line 20 Check that \*x is assignable: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that function calls are allowed in conditions.
+Remark: we allow function calls without further checks for now because they
+are mandatory for some applications.
+The next step must be to check that the called functions have a contract
+with an empty assigns clause and that they indeed satisfy their contract
+using a CI check.

regression/contracts/assigns_enforce_conditional_lvalue/main.c

@@ -0,0 +1,29 @@
+#include <stdbool.h>
+
+int foo(bool a, int *x, int *y) __CPROVER_assigns(a : *x; !a : *y)
+{
+  if(a)
+  {
+    *x = 0; // must pass
+    *y = 0; // must fail
+  }
+  else
+  {
+    *x = 0; // must fail
+    *y = 0; // must pass
+  }
+
+  *x = 0; // must fail
+  *y = 0; // must fail
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+
+  foo(a, &x, &y);
+  return 0;
+}

regression/contracts/assigns_enforce_conditional_lvalue/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-contract foo
+main.c function foo
+^\[foo\.\d+\] line 7 Check that \*x is assignable: SUCCESS$
+^\[foo\.\d+\] line 8 Check that \*y is assignable: FAILURE$
+^\[foo\.\d+\] line 12 Check that \*x is assignable: FAILURE$
+^\[foo\.\d+\] line 13 Check that \*y is assignable: SUCCESS$
+^\[foo\.\d+\] line 16 Check that \*x is assignable: FAILURE$
+^\[foo\.\d+\] line 17 Check that \*y is assignable: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Check that lvalue conditional assigns clause targets
+match with control flow path conditions.

regression/contracts/assigns_enforce_conditional_lvalue_list/main.c

@@ -0,0 +1,29 @@
+#include <stdbool.h>
+
+int foo(bool a, int *x, int *y) __CPROVER_assigns(a : *x, *y)
+{
+  if(a)
+  {
+    *x = 0; // must pass
+    *y = 0; // must pass
+  }
+  else
+  {
+    *x = 0; // must fail
+    *y = 0; // must fail
+  }
+
+  *x = 0; // must fail
+  *y = 0; // must fail
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+
+  foo(a, &x, &y);
+  return 0;
+}

regression/contracts/assigns_enforce_conditional_lvalue_list/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-contract foo
+main.c function foo
+^\[foo\.\d+\] line 7 Check that \*x is assignable: SUCCESS$
+^\[foo\.\d+\] line 8 Check that \*y is assignable: SUCCESS$
+^\[foo\.\d+\] line 12 Check that \*x is assignable: FAILURE$
+^\[foo\.\d+\] line 13 Check that \*y is assignable: FAILURE$
+^\[foo\.\d+\] line 16 Check that \*x is assignable: FAILURE$
+^\[foo\.\d+\] line 17 Check that \*y is assignable: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Check that conditional assigns clause  `c ? {lvalue, ..}`
+match with control flow path conditions.

regression/contracts/assigns_enforce_conditional_non_lvalue_target/main.c

@@ -0,0 +1,21 @@
+#include <stdbool.h>
+
+int *identity(int *ptr)
+{
+  return ptr;
+}
+
+int foo(bool a, int *x, int offset) __CPROVER_assigns(a : !x)
+{
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+
+  foo(a, &x, &y);
+  return 0;
+}

regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
+^CONVERSION ERROR
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that non-lvalue targets are rejected from conditional targets.

regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/main.c

@@ -0,0 +1,21 @@
+#include <stdbool.h>
+
+int *identity(int *ptr)
+{
+  return ptr;
+}
+
+int foo(bool a, int *x, int *y) __CPROVER_assigns(a : !x, *y)
+{
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+
+  foo(a, &x, &y);
+  return 0;
+}