Merge pull request #7091 from remi-delmas-3000/contracts-frees-clauses

  CONTRACTS: Add __CPROVER_frees clauses in the front end

Author: remi-delmas-3000

doc/cprover-manual/contracts-frees.md

@@ -0,0 +1,125 @@
+[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 by the function it calls, transitively.
+A function contract may have zero or more frees clauses.
+When no clause is provided the empty set is used as default.
+Contracts can also have an empty frees clause.
+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 (square brackets denote optional expressions
+`[` `]` ):
+```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 either:
+- 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 where the contract is being checked or used to abstract
+a function call.
+
+### 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). The functions must be side-effect free and deterministic,
+as well as loop-free and recursion-free.
+
+```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_was_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/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 was_freed cannot be used in preconditions
+__CPROVER_requires(!__CPROVER_was_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_was_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_was_freed is not allowed in preconditions.$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test checks that the front end rejects __CPROVER_was_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_was_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: wrong number of function arguments: expected 1, but got 2$
+^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_was_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: wrong number of function arguments: expected 1, but got 2$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test checks bad uses of __CPROVER_was_freed are rejected.

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

@@ -0,0 +1,44 @@
+#include <stdlib.h>
+
+// A function defining freeable pointers
+void foo_frees(char *arr, const size_t size, const size_t new_size)
+{
+  __CPROVER_freeable(arr);
+}
+
+// Function that resizes the array
+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_was_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 typechecks correct uses of
+- void function calls as frees clause targets
+- the predicate __CPROVER_freeable
+- the predicate __CPROVER_is_freeable
+- the predicate __CPROVER_was_freed
+
+The post condition of the contract is expected to fail because the predicates
+have no interpretation in the back-end yet.

src/ansi-c/ansi_c_convert_type.cpp

@@ -273,6 +273,14 @@ void ansi_c_convert_typet::read_rec(const typet &type)
     for(const exprt &target : to_unary_expr(as_expr).op().operands())
       assigns.push_back(target);
   }
+  else if(type.id() == ID_C_spec_frees)
+  {
+    const exprt &as_expr =
+      static_cast<const exprt &>(static_cast<const irept &>(type));
+
+    for(const exprt &target : to_unary_expr(as_expr).op().operands())
+      frees.push_back(target);
+  }
   else if(type.id() == ID_C_spec_ensures)
   {
     const exprt &as_expr =
@@ -341,6 +349,9 @@ void ansi_c_convert_typet::write(typet &type)
     if(!assigns.empty())
       to_code_with_contract_type(type).assigns() = std::move(assigns);
 
+    if(!frees.empty())
+      to_code_with_contract_type(type).frees() = std::move(frees);
+
     if(!ensures.empty())
       to_code_with_contract_type(type).ensures() = std::move(ensures);
 

src/ansi-c/ansi_c_convert_type.h

@@ -47,7 +47,7 @@ class ansi_c_convert_typet:public messaget
   bool constructor, destructor;
 
   // contracts
-  exprt::operandst assigns, ensures, requires, ensures_contract,
+  exprt::operandst assigns, frees, ensures, requires, ensures_contract,
     requires_contract;
 
   // storage spec