Function contracts: preliminary support for conditional targets in assigns clauses.

Conditional targets specify memory locations that can be assigned if and only if a condition
holds when a function is invoked.

- Modify ansi-c parser and typechecker to accept the new target syntax `c ? {t1, ..., tn}`, `c ? t`
- Add an explicit expression to the internal representation of assigns clause targets
- Translate conditions expressions to clean GOTO instructions using `goto-convert::clean_expr`
- Change the validity condition of a CAR to `guard && all_deref_valid(target) && rw_ok(target, size)`
  for assigns clause checking
- Update some tests, add new tests for the feature

Author: Remi Delmas

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,32 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+bool cond()
+{
+  return true;
+}
+
+int foo(int a, int *x, int *y) __CPROVER_assigns(a && cond() ? *x)
+{
+  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 15 Check that \*x is assignable: SUCCESS$
+^\[foo\.\d+\] line 19 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,31 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.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 9 Check that \*x is assignable: SUCCESS$
+^\[foo\.\d+\] line 10 Check that \*y is assignable: FAILURE$
+^\[foo\.\d+\] line 14 Check that \*x is assignable: FAILURE$
+^\[foo\.\d+\] line 15 Check that \*y is assignable: SUCCESS$
+^\[foo\.\d+\] line 18 Check that \*x is assignable: FAILURE$
+^\[foo\.\d+\] line 19 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_elvis_1/main.c renamed to regression/contracts/assigns_enforce_conditional_lvalue_list/main.c

@@ -2,12 +2,21 @@
 #include <stdbool.h>
 #include <stdlib.h>
 
-int foo(bool a, int *x, int *y, int *z) __CPROVER_assigns(*(a ? x : y))
+int foo(bool a, int *x, int *y) __CPROVER_assigns(a ? {*x,  *y})
 {
   if(a)
+  {
     *x = 0; // must pass
-  else
     *y = 0; // must pass
+  }
+  else
+  {
+    *x = 0; // must fail
+    *y = 0; // must fail
+  }
+
+  *x = 0; // must fail
+  *y = 0; // must fail
   return 0;
 }
 
@@ -16,8 +25,7 @@ int main()
   bool a;
   int x;
   int y;
-  int z;
 
-  foo(a, &x, &y, &z);
+  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 9 Check that \*x is assignable: SUCCESS$
+^\[foo\.\d+\] line 10 Check that \*y is assignable: SUCCESS$
+^\[foo\.\d+\] line 14 Check that \*x is assignable: FAILURE$
+^\[foo\.\d+\] line 15 Check that \*y is assignable: FAILURE$
+^\[foo\.\d+\] line 18 Check that \*x is assignable: FAILURE$
+^\[foo\.\d+\] line 19 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,18 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+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/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,18 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+int foo(bool a, int *x, int *y) __CPROVER_assigns(a ? {*x + *y, *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_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,37 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.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 15 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo\.\d+\] line 16 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 20 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 21 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo\.\d+\] line 24 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 25 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,36 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.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 14 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo\.\d+\] line 15 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo\.\d+\] line 19 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 20 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 23 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo\.\d+\] line 24 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_elvis_5/main.c renamed to regression/contracts/assigns_enforce_conditional_side_effect_condition/main.c

@@ -2,16 +2,12 @@
 #include <stdbool.h>
 #include <stdlib.h>
 
-int foo(bool a, int *x, int *y) __CPROVER_assigns((a ? *x : *y))
+int foo(int a, int *x, int *y) __CPROVER_assigns(a++ ? *x)
 {
   if(a)
   {
     *x = 0;
   }
-  else
-  {
-    *y = 0;
-  }
   return 0;
 }
 
@@ -21,6 +17,6 @@ int main()
   int x;
   int y;
 
-  foo(true, &x, &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,18 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.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.