CONTRACTS: Front-end: frees clause improvements

Add the following to the front-end:
- 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 predicates are not yet supported in the back-end.

Author: Remi Delmas

doc/cprover-manual/contracts-frees.md

@@ -78,3 +78,59 @@ 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.
 
+# Using functions to specify parametric sets of freeable pointers
+
+Users can define parametric sets of freeable pointers by writing functions that
+return the built-in type `__CPROVER_freeable_t` and call the built-in function
+`__CPROVER_freeable` or any user-defined function returning
+`__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]);
+  }
+}
+```
+
+The built-in function:
+
+```c
+__CPROVER_freeable_t __CPROVER_freeable(void *ptr);
+```
+adds the given pointer to the freeable set described by the enclosing function.
+
+Calls to functions returning `__CPROVER_freeable_t` 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,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_whole_object(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_whole_object(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 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
+__CPROVER_requires(__CPROVER_is_freeable(arr))
+__CPROVER_assigns(__CPROVER_whole_object(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/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --apply-loop-contracts
-^main.c.*: error: frees clause target must be a pointer-typed expression$
+^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$

regression/contracts/frees-clause-function-fail/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^main.c.*: error: frees clause target must be a pointer-typed expression$
+^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$

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

@@ -1,7 +1,7 @@
 CORE
 main.c
 --apply-loop-contracts
-^main.c.*: error: frees clause target must be a pointer-typed expression$
+^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$

src/ansi-c/ansi_c_internal_additions.cpp

@@ -231,6 +231,14 @@ void ansi_c_internal_additions(std::string &code)
     CPROVER_PREFIX "assignable_t " CPROVER_PREFIX "object_from(void *ptr);\n"
     // Declares the whole object pointer to by ptr
     CPROVER_PREFIX "assignable_t " CPROVER_PREFIX "whole_object(void *ptr);\n"
+    // Type that describes sets of freeable pointers
+    "typedef void " CPROVER_PREFIX "freeable_t;\n"
+    // Declares a pointer as freeable
+    CPROVER_PREFIX "freeable_t " CPROVER_PREFIX "freeable(void *ptr);\n"
+    // True iff ptr satisfies the preconditions of the free stdlib function
+    CPROVER_PREFIX "bool " CPROVER_PREFIX "is_freeable(void *ptr);\n"
+    // True iff ptr was freed during function execution or loop execution
+    CPROVER_PREFIX "bool " CPROVER_PREFIX "is_freed(void *ptr);\n"
     "\n";
   // clang-format on
 

src/ansi-c/c_typecheck_base.cpp

@@ -791,7 +791,25 @@ void c_typecheck_baset::typecheck_declaration(
           return;
 
         error().source_location = expr.source_location();
-        error() << id2string(id) + "is not allowed in preconditions." << eom;
+        error() << id2string(id) + " is not allowed in preconditions." << eom;
+        throw 0;
+      };
+
+      auto check_is_freed = [&](const exprt &expr) {
+        const irep_idt id = CPROVER_PREFIX "is_freed";
+
+        auto pred = [&](const exprt &expr) {
+          if(!can_cast_expr<symbol_exprt>(expr))
+            return false;
+
+          return to_symbol_expr(expr).get_identifier() == id;
+        };
+
+        if(!has_subexpr(expr, pred))
+          return;
+
+        error().source_location = expr.source_location();
+        error() << id2string(id) + " is not allowed in preconditions." << eom;
         throw 0;
       };
 
@@ -852,7 +870,7 @@ void c_typecheck_baset::typecheck_declaration(
           implicit_typecast_bool(requires);
           check_history_expr(requires);
           check_return_value(requires);
-          check_return_value(requires);
+          check_is_freed(requires);
           lambda_exprt lambda{temporary_parameter_symbols, requires};
           lambda.add_source_location() = requires.source_location();
           requires.swap(lambda);

src/ansi-c/c_typecheck_code.cpp

@@ -1014,11 +1014,43 @@ void c_typecheck_baset::typecheck_spec_frees_target(exprt &target)
     // an expression with pointer-type without side effects
     throw_on_side_effects(target);
   }
+  else if(can_cast_expr<side_effect_expr_function_callt>(target))
+  {
+    // A call to a freeable_t function symbol without other side effects
+    const auto &funcall = to_side_effect_expr_function_call(target);
+
+    if(!can_cast_expr<symbol_exprt>(funcall.function()))
+    {
+      error().source_location = target.source_location();
+      error() << "function pointer calls not allowed in frees clauses" << eom;
+      throw 0;
+    }
+
+    bool has_freeable_type =
+      (type.id() == ID_empty) &&
+      (type.get(ID_C_typedef) == CPROVER_PREFIX "freeable_t");
+    if(!has_freeable_type)
+    {
+      error().source_location = target.source_location();
+      error() << "expecting " CPROVER_PREFIX
+                 "freeable_t return type for function " +
+                   id2string(
+                     to_symbol_expr(funcall.function()).get_identifier()) +
+                   " called in frees clause"
+              << eom;
+      throw 0;
+    }
+
+    for(const auto &argument : funcall.arguments())
+      throw_on_side_effects(argument);
+  }
   else
   {
     // anything else is rejected
     error().source_location = target.source_location();
-    error() << "frees clause target must be a pointer-typed expression" << eom;
+    error() << "frees clause target must be a pointer-typed expression or a "
+               "call to a function returning " CPROVER_PREFIX "freeable_t"
+            << eom;
     throw 0;
   }
 }

src/ansi-c/c_typecheck_expr.cpp

@@ -2248,6 +2248,30 @@ exprt c_typecheck_baset::do_special_functions(
     typecheck_function_call_arguments(expr);
     return nil_exprt();
   }
+  else if(identifier == CPROVER_PREFIX "is_freeable")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << CPROVER_PREFIX "is_freeable expects one operand; "
+              << expr.arguments().size() << "provided." << eom;
+      throw 0;
+    }
+    typecheck_function_call_arguments(expr);
+    return nil_exprt();
+  }
+  else if(identifier == CPROVER_PREFIX "is_freed")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << CPROVER_PREFIX "is_freed expects one operand; "
+              << expr.arguments().size() << "provided." << eom;
+      throw 0;
+    }
+    typecheck_function_call_arguments(expr);
+    return nil_exprt();
+  }
   else if(identifier == CPROVER_PREFIX "same_object")
   {
     if(expr.arguments().size()!=2)