CONTRACTS: Add __CPROVER_frees clauses

Add the following to the front-end:
  - add `__CPROVER_frees` clause for function and loop contracts
    in the parser and internal data structures
  - 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,147 @@
+[CPROVER Manual TOC](../../)
+
+# Frees Clauses
+
+A _frees clause_ allows the user to specify a set of pointers that may be freed
+by a function or the body of a loop. A function or loop contract 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
+
+```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`);
+
+
+### Examples
+
+In a function contract
+```c
+int foo(char *arr1, char *arr2, size_t size)
+__CPROVER_frees(
+    // arr1 freeable only if the condition holds
+    size > 0 && arr1: arr1;
+    // arr2 always freeable
+    arr2
+)
+{
+  if(size > 0 && arr1)
+    free(arr1);
+  free(arr2);
+  return 0;
+}
+```
+
+In a loop contract:
+
+```c
+int main()
+{
+  size_t size = 10;
+  char *arr = malloc(size);
+
+  for(size_t i = 0; i <= size; i++)
+    // clang-format off
+  __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(arr))
+  __CPROVER_frees(arr)
+    // clang-format on2
+    {
+      if(i < size)
+        arr[i] = 0;
+      else
+        free(arr);
+    }
+  return 0;
+}
+```
+
+## Semantics
+
+The set of pointers specified by the frees clause of the contract is interpreted
+at the function call-site for function contracts, and right before entering the
+loop for loop contracts.
+
+### For contract checking
+When checking a contract against a function or a loop, each pointer that the
+function or loop body attempts to free gets checked for membership in the set of
+pointers specified by the contract.
+
+### For replacement of function calls or loops by contracts
+When replacing a function call or a loop by a contract, each pointer of the
+_frees_ clause is non-deterministically freed after the function call
+or after the loop.
+
+## 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)
+{
+  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 functions returning void can then 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`, 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 or the loop under
+analysis.

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/main.c

@@ -0,0 +1,43 @@
+#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
+__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/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-contract foo
+^\[foo.postcondition.\d+\] line \d+ Check ensures clause: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test checks that the front end parses and typchecks correct uses of:
+- void function calls as frees clause targets
+- the predicate __CPROVER_freeable
+- the predicate __CPROVER_is_freeable
+- the predicate __CPROVER_is_freed
+
+The post condition of the contract is expected to fail because the predicates
+have no interpretation in the back-end yet.

regression/contracts/frees-clause-for-loop-fail/main.c

@@ -0,0 +1,19 @@
+#include <stdlib.h>
+int main()
+{
+  size_t size = 10;
+  char *arr = malloc(size);
+
+  for(size_t i = 0; i <= size; i++)
+    // clang-format off
+  __CPROVER_assigns(i, arr[2], __CPROVER_POINTER_OBJECT(arr))
+  __CPROVER_frees(arr[2])
+    // clang-format on
+    {
+      if(i == 2)
+        arr[i] = 0;
+      if(i == size)
+        free(arr);
+    }
+  return 0;
+}

regression/contracts/frees-clause-for-loop-fail/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--apply-loop-contracts
+^main.c.* error: frees clause target must be a pointer-typed expression or a call to a function returning void$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test is expected trigger a typchecking error on a frees clause target.

regression/contracts/frees-clause-for-loop-pass/main.c

@@ -0,0 +1,19 @@
+#include <stdlib.h>
+int main()
+{
+  size_t size = 10;
+  char *arr = malloc(size);
+
+  for(size_t i = 0; i <= size; i++)
+    // clang-format off
+  __CPROVER_assigns(i, arr[2], __CPROVER_POINTER_OBJECT(arr))
+  __CPROVER_frees(arr)
+    // clang-format on
+    {
+      if(i == 2)
+        arr[i] = 0;
+      if(i == size)
+        free(arr);
+    }
+  return 0;
+}

regression/contracts/frees-clause-for-loop-pass/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--apply-loop-contracts
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test checks that frees clauses are parsed and typechecked for for loops.