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

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;
+}

regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/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_pointer_object/main.c

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

regression/contracts/assigns_enforce_conditional_pointer_object/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-contract foo
+main.c function foo
+^\[foo\.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo\.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 19 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo\.\d+\] line 22 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 23 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Check that conditional assigns clause  `c ? __CPROVER_POINTER_OBJECT((p)`
+match with control flow path conditions.

regression/contracts/assigns_enforce_conditional_pointer_object_list/main.c

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

regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-contract foo
+main.c function foo
+^\[foo\.\d+\] line 12 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo\.\d+\] line 13 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo\.\d+\] line 17 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 18 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 21 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 22 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Check that conditional assigns clause  `c ? {__CPROVER_POINTER_OBJECT((p), .. }`
+match with control flow path conditions.

regression/contracts/assigns_enforce_conditional_side_effect_condition/main.c

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

regression/contracts/assigns_enforce_conditional_side_effect_condition/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^.* error: side-effects not allowed in assigns clause conditions$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that side-effect expressions in target conditions cause hard errors.

regression/contracts/assigns_enforce_conditional_side_effect_target/main.c

@@ -0,0 +1,16 @@
+#include <stdbool.h>
+
+int foo(bool a, int *x, int *y) __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_side_effect_target/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^.* error: side-effects not allowed in assigns clause targets$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that side-effect expressions are rejected from conditional targets.