CONTRACTS: Add __CPROVER_frees clauses

Add the following to the front-end:
  - add `__CPROVER_frees` clause for function contracts
  - add `__CPROVER_freeable` built-in function
  - add `__CPROVER_is_freeable` built-in predicate
  - add `__CPROVER_is_freed` built-in predicate

Effective support for the new clause type and related predicates will come in a later PR.

Author: Remi Delmas

doc/cprover-manual/contracts-frees.md

@@ -0,0 +1,120 @@
+[CPROVER Manual TOC](../../)
+
+# Frees Clauses
+
+A _frees clause_ allows the user to specify a set of pointers that may be freed
+by a function. A function contract may have zero or more frees clauses.
+When no clause is provided the empty set is used as default.
+When more than one frees clause is given, the sets of pointers they contain are
+unioned together to yield a single set of pointers.
+
+## Syntax
+
+The clause has the following syntax:
+```c
+__CPROVER_frees(targets)
+```
+
+Where `targets` has the following syntax:
+```
+          targets ::= cond-target-group (';' cond-target-group)* ';'?
+cond-target-group ::= (condition ':')? target (',' target)*
+           target ::= lvalue-expr
+                    | __CPROVER_freeable(lvalue-expr)
+```
+
+A frees clause target must be eiter:
+- an lvalue expression with a pointer type,
+- a call to the built-in function `__CPROVER_freeable`
+- a call to a user-defined side effect free and deterministic function returning
+  the type `void` (itself containing direct or indirect calls to
+  `__CPROVER_freeable` or to functions that call `__CPROVER_freeable`);
+
+### Example
+
+```c
+int foo(char *arr1, char *arr2, size_t size)
+__CPROVER_frees(
+    // `arr1` is freeable only if the condition `size > 0 && arr1` holds
+    size > 0 && arr1: arr1;
+
+    // `arr2` is always freeable
+    arr2;
+)
+{
+  if(size > 0 && arr1)
+    free(arr1);
+  free(arr2);
+  return 0;
+}
+```
+
+## Semantics
+
+The set of pointers specified by the frees clause of the contract is interpreted
+at the function call-site.
+
+### For contract checking
+
+When checking a contract against a function, each pointer that the
+function attempts to free gets checked for membership in the set of
+pointers specified by the _frees clause_.
+
+### For replacement of function calls by contracts
+
+When replacing a function call by a contract, each pointer of the
+_frees clause_ is non-deterministically freed after the function call.
+
+## Specifying parametric sets of freeable pointers using C functions
+
+Users can define parametric sets of freeable pointers by writing functions that
+return the built-in type void and call the built-in function
+`__CPROVER_freeable` (directly or indirectly through some other user-defined
+function):
+
+```c
+void my_freeable_set(char **arr, size_t size)
+{
+  // The first 3 pointers are freeable
+  // if the array is at least of size 3.
+  if (arr && size > 3) {
+    __CPROVER_freeable(arr[0]);
+    __CPROVER_freeable(arr[1]);
+    __CPROVER_freeable(arr[2]);
+  }
+}
+```
+
+The built-in function:
+```c
+void __CPROVER_freeable(void *ptr);
+```
+adds the given pointer to the freeable set described by the enclosing function.
+
+Calls to such functions can be used as targets in `__CPROVER_frees` clauses:
+```c
+void my_function(char **arr, size_t size)
+__CPROVER_frees(my_freeable_set(arr, size))
+{
+  ...
+}
+```
+
+## Frees clause related predicates
+
+The predicate:
+```c
+__CPROVER_bool __CPROVER_is_freeable(void *ptr);
+```
+can only be used in pre and post conditions, in contract checking or replacement
+modes. It returns `true` if and only if the pointer satisfies the preconditions
+of the `free` function from `stdlib.h`
+([see here](https://github.com/diffblue/cbmc/blob/cf00a53bbcc388748be9668f393276f6d84b1a60/src/ansi-c/library/stdlib.c#L269)),
+that is if and only if the pointer points to a valid dynamically allocated object and has offset zero.
+
+The predicate:
+```c
+__CPROVER_bool __CPROVER_is_freed(void *ptr);
+```
+can only be used in post conditions and returns `true` if and only if the
+pointer was freed during the execution of the function under analysis.

regression/contracts/assigns_enforce_address_of/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_function_calls/main.c

@@ -13,5 +13,4 @@ int main()
 {
   int x;
   foo(&x);
-  baz(&x);
 }

regression/contracts/assigns_enforce_function_calls/test.desc

@@ -3,8 +3,8 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: expecting void return type for function 'bar' called in assigns clause$
 ^CONVERSION ERROR$
 --
 --
-Check that function call expressions are rejected in assigns clauses.
+Check that non-void function call expressions are rejected in assigns clauses.

regression/contracts/assigns_enforce_function_calls_ignored/main.c

@@ -0,0 +1,17 @@
+void bar(int *x)
+{
+  if(x)
+    __CPROVER_typed_target(x);
+}
+
+int foo(int *x) __CPROVER_assigns(bar(x))
+{
+  *x = 0;
+  return 0;
+}
+
+int main()
+{
+  int x;
+  foo(&x);
+}

regression/contracts/assigns_enforce_function_calls_ignored/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^call to function 'bar' in assigns clause not supported yet$
+^EXIT=(127|134)$
+^SIGNAL=0$
+--
+--
+Check that void function call expressions in assigns clauses make
+instrumentation fail.

regression/contracts/assigns_enforce_literal/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_side_effects_2/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_side_effects_3/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_type_checking_invalid_case_01/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
-^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
+^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
 --
 Checks whether type checking rejects literal constants in assigns clause.

regression/contracts/frees-clause-and-predicates-fail/main.c

@@ -0,0 +1,45 @@
+#include <stdlib.h>
+
+// A function defining a conditionally freeable target
+void foo_frees(char *arr, const size_t size, const size_t new_size)
+{
+  __CPROVER_freeable(arr);
+}
+
+char *foo(char *arr, const size_t size, const size_t new_size)
+  // clang-format off
+ // error is_freed cannot be used in preconditions
+__CPROVER_requires(!__CPROVER_is_freed(arr))
+__CPROVER_requires(__CPROVER_is_freeable(arr))
+__CPROVER_assigns(__CPROVER_object_whole(arr))
+__CPROVER_frees(foo_frees(arr, size, new_size))
+__CPROVER_ensures(
+  (arr && new_size > size) ==>
+    __CPROVER_is_fresh(__CPROVER_return_value, new_size))
+__CPROVER_ensures(
+  (arr && new_size > size) ==>
+    __CPROVER_is_freed(__CPROVER_old(arr)))
+__CPROVER_ensures(
+    !(arr && new_size > size) ==>
+      __CPROVER_return_value == __CPROVER_old(arr))
+// clang-format on
+{
+  if(arr && new_size > size)
+  {
+    free(arr);
+    return malloc(new_size);
+  }
+  else
+  {
+    return arr;
+  }
+}
+
+int main()
+{
+  size_t size;
+  size_t new_size;
+  char *arr = malloc(size);
+  arr = foo(arr, size, new_size);
+  return 0;
+}

regression/contracts/frees-clause-and-predicates-fail/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^main.c.* error: __CPROVER_is_freed is not allowed in preconditions.$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test checks that the front end rejects __CPROVER_is_freed in preconditions.

regression/contracts/frees-clause-and-predicates-fail2/main.c

@@ -0,0 +1,44 @@
+#include <stdlib.h>
+
+// A function defining a conditionally freeable target
+int foo_frees(char *arr, const size_t size, const size_t new_size)
+{
+  __CPROVER_freeable(arr);
+  return 0;
+}
+
+char *foo(char *arr, const size_t size, const size_t new_size)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_freeable(arr))
+__CPROVER_assigns(__CPROVER_object_whole(arr))
+__CPROVER_frees(foo_frees(arr, size, new_size))
+__CPROVER_ensures(
+  (arr && new_size > size) ==>
+    __CPROVER_is_fresh(__CPROVER_return_value, new_size))
+__CPROVER_ensures(
+  (arr && new_size > size) ==>
+    __CPROVER_is_freed(__CPROVER_old(arr)))
+__CPROVER_ensures(
+    !(arr && new_size > size) ==>
+      __CPROVER_return_value == __CPROVER_old(arr))
+// clang-format on
+{
+  if(arr && new_size > size)
+  {
+    free(arr);
+    return malloc(new_size);
+  }
+  else
+  {
+    return arr;
+  }
+}
+
+int main()
+{
+  size_t size;
+  size_t new_size;
+  char *arr = malloc(size);
+  arr = foo(arr, size, new_size);
+  return 0;
+}

regression/contracts/frees-clause-and-predicates-fail2/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-contract foo
+^main.c.* error: expecting void return type for function 'foo_frees' called in frees clause$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test checks that the front-end rejects non-void-typed
+function calls in frees clauses.

regression/contracts/frees-clause-and-predicates-is_freeable-bad-arity/main.c

@@ -0,0 +1,13 @@
+#include <stdlib.h>
+
+void foo(char *arr) __CPROVER_requires(__CPROVER_is_freeable(arr, 1))
+{
+}
+
+int main()
+{
+  size_t size;
+  char arr[size];
+  foo(arr);
+  return 0;
+}

regression/contracts/frees-clause-and-predicates-is_freeable-bad-arity/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^main.c.*error: __CPROVER_is_freeable expects one operand; 2 provided$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test checks bad uses of __CPROVER_is_freeable are rejected.

regression/contracts/frees-clause-and-predicates-is_freed-bad-arity/main.c

@@ -0,0 +1,15 @@
+#include <stdlib.h>
+
+void foo(char *arr) __CPROVER_requires(__CPROVER_is_freeable(arr))
+  __CPROVER_ensures(__CPROVER_is_freed(__CPROVER_old(arr), 1))
+{
+  free(arr);
+}
+
+int main()
+{
+  size_t size;
+  char arr[size];
+  foo(arr);
+  return 0;
+}

regression/contracts/frees-clause-and-predicates-is_freed-bad-arity/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^main.c.*error: __CPROVER_is_freed expects one operand; 2 provided$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test checks bad uses of __CPROVER_is_freed are rejected.