CONTRACTS: Front-end extensions for __CPROVER_frees clauses

Add the following to the front-end:
- add __CPROVER_frees as a new contract clause
  for functons and loops
- add `__CPROVER_freeable_t` built-in type
- add `__CPROVER_freeable` built-in function
- allow calls to `__CPROVER_freeable_t` functions
  in frees clauses
- add `__CPROVER_is_freeable` built-in predicate
- add `__CPROVER_is_freed` built-in predicate

The __CPROVER_frees clause and predicates are
not yet supported in the back-end.

Author: Remi Delmas

doc/cprover-manual/contracts-frees.md

@@ -0,0 +1,149 @@
+[CPROVER Manual TOC](../../)
+
+# Frees Clauses
+
+A _frees clause_ lets the user specify the set of pointers that may be freed
+by a function or a loop.
+
+The _frees clause_ may only refer to locations that exist in the calling context
+of the function or before entering the loop, i.e. that are part of the _frame_
+of the function call or loop execution.
+## Syntax
+
+```c
+__CPROVER_frees(*targets*)
+```
+
+Where targets have the following syntax:
+
+```
+targets ::= conditional-target-group (';' conditional-target-group)* ';'?
+conditional-target-group ::= (condition ':')? target (',' target)*
+target ::= pointer-typed-expression
+        | f(args)
+```
+Where `f` is a built-in or user-defined function returning the built-in type
+`__CPROVER_freeable_t`.
+
+### Pointer-typed targets
+
+Pointer-typed targets can be directly listed in the clause.
+
+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;
+}
+```
+
+## Using calls to __CPROVER_freable_t functions as targets
+
+Users can define parametric sets of freeable pointers by writing functions that
+return the built-in type `__CPROVER_freeable_t`. 
+
+```c
+__CPROVER_freeable_t my_freeable_set(char **arr, size_t size)
+{
+  if (arr && size > 3) {
+    __CPROVER_freeable(arr[0]);
+    __CPROVER_freeable(arr[1]);
+    __CPROVER_freeable(arr[2]);
+  }
+}
+```
+
+In such functions, calls to the built-in function:
+
+```c
+__CPROVER_freeable_t __CPROVER_freeable(void *ptr);
+```
+
+add the given pointer to the freeable set described by the enclosing function.
+One can also call user-defined functions returning `__CPROVER_freeable_t`, which
+also add their targets to the set defined by the enclosing function.
+
+Calls to `__CPROVER_freeable_t` functions are accepted as targets in
+`__CPROVER_frees` clauses:
+
+```c
+void my_function(char **arr, size_t size)
+// adds the locations defined by my_freeable_set to the freeable locations for
+// my_function.
+__CPROVER_frees(my_freeable_set(arr, size))
+{
+  ...
+}
+```
+## 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.
+
+
+# Frees clauses related predicates
+Two predicates meant to express pre and post conditions about freeable pointers
+are provided to the user.
+
+## For preconditions
+
+```c
+__CPROVER_bool __CPROVER_is_freeable(void *ptr);
+```
+can only be used in preconditions, 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.
+
+## For postconditions
+
+```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 effectively freed during the execution of the function or the
+loop under analysis.
+

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

@@ -0,0 +1,46 @@
+#include <stdlib.h>
+
+// A function defining a conditionally freeable target
+__CPROVER_freeable_t
+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,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-fail2/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-contract foo
+^main.c.* error: expecting __CPROVER_freeable_t 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-__CPROVER_freeable_t-typed
+function calls in frees clauses.

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

@@ -0,0 +1,44 @@
+#include <stdlib.h>
+
+// A function defining a freeable target
+__CPROVER_freeable_t
+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:
+- __CPROVER_freeable_t 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 __CPROVER_freeable_t$
+^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.