CONTRACTS: Add __CPROVER_frees clauses in the front end #7091

remi-delmas-3000 · 2022-08-31T18:30:17Z

This is extracted from the dynamic frames PR #6887 and contains the front-end modifications only.

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 the next PR.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
[n/a] My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2022-08-31T20:09:44Z

Codecov Report

Base: 77.89% // Head: 77.88% // Decreases project coverage by -0.00% ⚠️

Coverage data is based on head (d236601) compared to base (7f86707).
Patch coverage: 75.92% of modified lines in pull request are covered.

❗ Current head d236601 differs from pull request most recent head 5982243. Consider uploading reports for the commit 5982243 to get more accurate results

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7091      +/-   ##
===========================================
- Coverage    77.89%   77.88%   -0.01%     
===========================================
  Files         1616     1616              
  Lines       186701   186828     +127     
===========================================
+ Hits        145433   145516      +83     
- Misses       41268    41312      +44

Impacted Files	Coverage Δ
src/ansi-c/ansi_c_convert_type.h	`100.00% <ø> (ø)`
src/ansi-c/ansi_c_internal_additions.cpp	`90.12% <ø> (ø)`
src/ansi-c/c_typecheck_base.h	`100.00% <ø> (ø)`
src/util/replace_symbol.cpp	`76.89% <0.00%> (-1.32%)`	⬇️
src/ansi-c/parser.y	`81.09% <50.00%> (-0.17%)`	⬇️
src/goto-programs/goto_convert.cpp	`87.95% <50.00%> (-0.17%)`	⬇️
src/util/rename_symbol.cpp	`76.33% <60.00%> (-0.50%)`	⬇️
src/ansi-c/c_typecheck_code.cpp	`77.24% <68.57%> (-0.52%)`	⬇️
src/ansi-c/c_typecheck_expr.cpp	`75.51% <84.21%> (+0.09%)`	⬆️
src/ansi-c/ansi_c_convert_type.cpp	`80.96% <100.00%> (+0.26%)`	⬆️
... and 8 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

doc/cprover-manual/contracts-assigns.md

tautschnig · 2022-09-01T12:56:06Z

doc/cprover-manual/contracts-assigns.md


-### Syntax
+The set of locations described by the contract is the union of the locations


Is a "location" here a "memory location?" Also, is "contract" well defined here? There is no prior mention of this in this particular document. Also, now that I re-read this paragraph: in what way does a contract describe a set of (memory) locations? Why does that even matter?

doc/cprover-manual/contracts-assigns.md

tautschnig · 2022-09-01T12:58:54Z

doc/cprover-manual/contracts-assigns.md

-### Syntax
+The set of locations described by the contract is the union of the locations
+specified by each of its assigns clauses, or the empty set of no _assigns_
+clause is specified.


Previously, wasn't there some code that would automatically determine what to havoc, and, therefore, in a way, the memory locations being written to?

There is indeed an inference pass for loop contracts in case there isn't a user-specified clause in the loop contract.
I'll make the distinction.
We don't have inference for function contracts. Since we ultimately want to have function contracts as standalone entities we wouldn't know what instructions to infer the assigned memory locations from.

tautschnig · 2022-09-01T13:00:47Z

doc/cprover-manual/contracts-assigns.md

+specified by each of its assigns clauses, or the empty set of no _assigns_
+clause is specified.
+
+The assigns clause may only refer to locations that exist in the calling context


If a function is called in exactly two places, and both of them have a procedure-local variable x in scope, can I use &x in the assigns clause?

syntactically the targets must be expressions of function parameters or globals, but they can surely resolve to that procedure local &x at some call-site. However I'm not sure what it would mean to modify the address of a procedure local variable. Modifying the value stored at this address, yes.

Apologies, I should have used x instead of &x. I don't see where the documentation makes explicit that such expressions must be function parameters or globals?

tautschnig · 2022-09-01T13:49:51Z

src/ansi-c/c_typecheck_code.cpp

+  bool is_empty_type = target.type().id() == ID_empty;
+  bool is_assignable_typedef =
+    target.type().get(ID_C_typedef) == CPROVER_PREFIX "assignable_t";
+  // only allow void type if it is the typedef CPROVER_PREFIX "assignable_t"
+  if(target.type().id() == ID_empty && !is_assignable_typedef)
  {
    error().source_location = target.source_location();
    error() << "void-typed expressions not allowed as assigns clause targets"
            << eom;
    throw 0;
  }


What if we actually allowed void-typed expressions? Would there really be anything wrong in doing that? Wouldn't that allow us to get rid of __CPROVER_assignable_t?

The type is meant to documents the fact that the function specifies sets of assignable locations.

But mostly it is used to distinguish functions that specify assigns clauses from other void functions and process them differently when dynamic frames are involved.

I am not convinced that a typedef is the best way to address this problem. The number of permitted functions is very small, can't we just specifically check for those in each place that requires checking?

Today we only provide 4 built-ins returning __CPROVER_assignable_t,
but the dynamic frames PRs builds on top of this to allow users to write their own functions returning __CPROVER_assignable_t. These user-defined functions can call other functions returning __CPROVER_assignable_t (built-in or user-defined), so the set is not necessarily small.

I intended __CPROVER_assignable_t as an opaque type that represents a set of memory locations. It is defined as void in the front-end, and gets mapped to an actual representation by the instrumentation pass.

My two cents, but I like the __CPROVER_assignable_t approach for representing sets of memory locations.

tautschnig · 2022-09-01T13:53:06Z

src/ansi-c/c_typecheck_expr.cpp

+      if(identifier == CPROVER_PREFIX "typed_target")
+      {
+        if(expr.arguments().size() != 1)


The remainder of the code in this function sets out a poor example, but: could the body of this if be factored out into a function of its own?

thanks, will do.

tautschnig · 2022-09-01T13:53:27Z

src/ansi-c/c_typecheck_expr.cpp

+          error().source_location = f_op.source_location();
+          error() << "expected 1 argument for " << CPROVER_PREFIX "typed_target"
+                  << " found " << expr.arguments().size() << eom;
+          throw 0;


See above: invalid_source_file_exceptiont

tautschnig · 2022-09-01T13:53:33Z

src/ansi-c/c_typecheck_expr.cpp

+          error().source_location = arg0.source_location();
+          error() << "argument of " << CPROVER_PREFIX "typed_target"
+                  << "must be assignable" << eom;
+          throw 0;


See above: invalid_source_file_exceptiont

tautschnig · 2022-09-01T13:53:38Z

src/ansi-c/c_typecheck_expr.cpp

+          error().source_location = arg0.source_location();
+          error() << "sizeof not defined for argument of "
+                  << CPROVER_PREFIX "typed_target"
+                  << " of type " << to_string(arg0.type()) << eom;
+          throw 0;


See above: invalid_source_file_exceptiont

nwetzler · 2022-09-27T22:38:02Z

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

+^SIGNAL=0$
+--
+--
+This test checks that the front end rejects __CPROVER_is_freed in preconditions.


Maybe add that the intention of the code is to resize an array.

nwetzler · 2022-09-27T22:57:00Z

src/ansi-c/c_typecheck_expr.cpp

+    if(expr.arguments().size() != 1)
+    {
+      std::ostringstream error_message;
+      error_message << CPROVER_PREFIX "is_freeable expects one operand; "


Are these errors checked in regression? I don't remember seeing them in the tests.

tests added

nwetzler · 2022-09-27T23:02:22Z

src/ansi-c/c_typecheck_code.cpp

+  bool is_empty_type = target.type().id() == ID_empty;
+  bool is_assignable_typedef =
+    target.type().get(ID_C_typedef) == CPROVER_PREFIX "assignable_t";
+  // only allow void type if it is the typedef CPROVER_PREFIX "assignable_t"
+  if(target.type().id() == ID_empty && !is_assignable_typedef)
  {
    error().source_location = target.source_location();
    error() << "void-typed expressions not allowed as assigns clause targets"
            << eom;
    throw 0;
  }


My two cents, but I like the __CPROVER_assignable_t approach for representing sets of memory locations.

nwetzler · 2022-09-27T23:05:01Z

doc/cprover-manual/contracts-frees.md

+
+In a function contract:
+```c
+int foo(char *arr1, char *arr2, size_t size)


Are these examples included as regression tests? If so, perhaps there is some way to link to them.

no these are just embedded in the doc.

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

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

feliperodri · 2022-10-04T21:00:43Z

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

+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$


Does the error message says the name and the type of the parameter an user tried to use with __CPROVER_frees? It might be really helpful for debugging.

feliperodri · 2022-10-04T21:03:07Z

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

+  while(i <= size)
+    // clang-format off
+  __CPROVER_assigns(i, arr[2], __CPROVER_POINTER_OBJECT(arr))
+  __CPROVER_frees(arr)


What if I call __CPROVER_frees with a function returning void, but with no pointers in it. For example,

void foo() { int x; } ... __CPROVER_frees(foo())

feliperodri · 2022-10-04T21:06:09Z

src/ansi-c/c_typecheck_base.cpp

+        typecheck_spec_frees(code_type.frees());
+        for(auto &frees : code_type.frees())
+        {
+          lambda_exprt lambda{temporary_parameter_symbols, frees};
+          lambda.add_source_location() = frees.source_location();
+          frees.swap(lambda);
+        }


Nitpick: we might want to throw a simple warning saying there is current no implementation for it.

doc/cprover-manual/contracts-frees.md

feliperodri · 2022-10-04T21:25:34Z

doc/cprover-manual/contracts-frees.md

+
+## Frees clause related predicates
+
+The predicate:


No need for this line.

Suggested change

The predicate:

feliperodri · 2022-10-04T21:25:37Z

doc/cprover-manual/contracts-frees.md

+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:


No need for this line.

Suggested change

The predicate:

doc/cprover-manual/contracts-frees.md

feliperodri · 2022-10-05T15:47:16Z

doc/cprover-manual/contracts-frees.md

+## 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


feliperodri · 2022-10-05T15:48:33Z

doc/cprover-manual/contracts-frees.md

+
+## Frees clause related predicates
+
+The predicate:


Suggested change

The predicate:

feliperodri · 2022-10-05T15:48:41Z

doc/cprover-manual/contracts-frees.md

+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:


Suggested change

The predicate:

tautschnig

Ok in principle, but I'm confused on some occasions. Please clarify.

tautschnig · 2022-10-07T11:01:33Z

doc/cprover-manual/contracts-frees.md

+# 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.


Is that just this function that has the contract attached to it, or any function that may (transitively) be called by the function that has the contract?

transitively

tautschnig · 2022-10-07T11:01:55Z

doc/cprover-manual/contracts-frees.md

+                    | __CPROVER_freeable(lvalue-expr)
+```
+
+A frees clause target must be eiter:


s/eiter/either/

tautschnig · 2022-10-07T11:05:57Z

doc/cprover-manual/contracts-frees.md

+The set of pointers specified by the frees clause of the contract is interpreted
+at the function call-site.


At each call site of the function?

at each call site where the contract is checked or replaced

tautschnig · 2022-10-07T11:07:54Z

doc/cprover-manual/contracts-frees.md

+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


Are there any restrictions on what control flow is permitted in such functions? For example, are recursion or loops without constant bound permitted?

in this first version recursion is prohibited, the function body is going to be inlined, and any remaining loops must be unwound to completion before the analysis. Adding this to the documentation.

tautschnig · 2022-10-07T11:11:27Z

doc/cprover-manual/contracts-frees.md

+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.


Will this also work when the pointer is re-allocated after having been freed? As in:

free(p); p = malloc(1);

with the call to malloc returning the same adddress that p had before?

I'll change the name of the predicate to __CPROVER_was_freed.

In a situation like this both __CPROVER_was_freed(p) and __CPROVER_r_ok(p, 1) will hold in post.

The instrumentation keeps track of deallocation events by recording ids of deallocated objects in a map, that gets passed to the predicate as a ghost parameter for evaluation.

if we wanted instead to assert that a pointer does not point into a live object as a post we would need to track the lifetime and current size of all objects in the program separately (without nondeterminism as is currently done).

tautschnig · 2022-10-07T11:16:13Z

src/ansi-c/c_typecheck_expr.cpp

+        expr.source_location()};
+    }
+    typecheck_function_call_arguments(expr);
+    return nil_exprt();


What to make of this?

I'm using the same approach as the one used with is_fresh : return nil_exprt() so that the original expression stays in place. When do_special_function returns a non-nil expression it replaces the original expression:

exprt tmp=do_special_functions(expr); if(tmp.is_not_nil()) expr.swap(tmp); else typecheck_function_call_arguments(expr);

removing this completely since it seems like declaring the functions in cprover_builtin_headers.h and ansi_c_internal_additions.cpp suffices to have them type-checked. I don't understand why this was done like this for is_fresh

tautschnig · 2022-10-07T11:16:20Z

src/ansi-c/c_typecheck_expr.cpp

+        expr.source_location()};
+    }
+    typecheck_function_call_arguments(expr);
+    return nil_exprt();


... and this?

same as above. I am just following the pattern set by someone else with is_fresh

tautschnig · 2022-10-07T11:17:24Z

src/ansi-c/parser.y

+        | TOK_CPROVER_FREES '(' ')'
+        {
+          $$=$1;
+          set($$, ID_C_spec_frees);
+          parser_stack($$).add_to_operands(exprt(ID_target_list));
+        }


Is this case even necessary?

yes, this is meant to allows for empty frees clauses to be explicitly written in contracts instead of having to be forcibly omitted.

tautschnig · 2022-10-07T11:18:06Z

src/goto-programs/goto_convert.cpp

+  auto frees = static_cast<const unary_exprt &>(code.find(ID_C_spec_frees));
+  if(frees.is_not_nil())
+  {
+    PRECONDITION(loop->is_goto());
+    loop->condition_nonconst().add(ID_C_spec_frees).swap(frees.op());
+  }


The documentation suggested this was only permitted on function pre/post-conditions and not on loop invariants?

good catch, this is a leftover

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_was_freed` built-in predicate Effective support for the new clause type and related predicates will come in a later PR.

remi-delmas-3000 requested review from tautschnig, feliperodri, SaswatPadhi, kroening, peterschrammel and chris-ryder as code owners August 31, 2022 18:30

remi-delmas-3000 mentioned this pull request Aug 31, 2022

CONTRACTS: Front-end: frees clause improvements #7087

Closed

6 tasks

remi-delmas-3000 force-pushed the contracts-frees-clauses branch from aa4af69 to 38f3ce1 Compare August 31, 2022 19:14

remi-delmas-3000 force-pushed the contracts-frees-clauses branch 2 times, most recently from de218d2 to 20ee9e8 Compare September 1, 2022 13:53

tautschnig reviewed Sep 1, 2022

View reviewed changes

tautschnig assigned remi-delmas-3000 Sep 1, 2022

remi-delmas-3000 force-pushed the contracts-frees-clauses branch from 20ee9e8 to bcf61d0 Compare September 1, 2022 18:20

feliperodri added aws Bugs or features of importance to AWS CBMC users aws-high Code Contracts Function and loop contracts labels Sep 1, 2022

remi-delmas-3000 force-pushed the contracts-frees-clauses branch from bcf61d0 to 70acafe Compare September 1, 2022 19:25

tautschnig mentioned this pull request Sep 2, 2022

CONTRACTS: Front-end extensions for assigns clauses #7086

Merged

6 tasks

tautschnig added the dependent - do not merge label Sep 2, 2022

tautschnig marked this pull request as draft September 2, 2022 08:46

remi-delmas-3000 mentioned this pull request Sep 2, 2022

CONTRACTS: Dynamic frame condition checking #6887

Closed

SaswatPadhi removed their request for review September 17, 2022 23:57

feliperodri requested a review from nwetzler September 20, 2022 18:35

nwetzler approved these changes Sep 27, 2022

View reviewed changes

remi-delmas-3000 changed the title ~~CONTRACTS: Front-end extensions for __CPROVER_frees clauses~~ CONTRACTS: Add __CPROVER_frees clauses in the front end. Oct 4, 2022

remi-delmas-3000 force-pushed the contracts-frees-clauses branch 2 times, most recently from e2b70d7 to 063a9a0 Compare October 4, 2022 17:09

remi-delmas-3000 requested review from nwetzler and tautschnig October 4, 2022 17:35

jimgrundy assigned nwetzler Oct 4, 2022

remi-delmas-3000 marked this pull request as ready for review October 4, 2022 19:12

feliperodri requested changes Oct 4, 2022

View reviewed changes

feliperodri unassigned nwetzler Oct 4, 2022

nwetzler approved these changes Oct 5, 2022

View reviewed changes

remi-delmas-3000 force-pushed the contracts-frees-clauses branch from 063a9a0 to 0dfb3d7 Compare October 5, 2022 14:18

remi-delmas-3000 removed the dependent - do not merge label Oct 5, 2022

remi-delmas-3000 force-pushed the contracts-frees-clauses branch from 0dfb3d7 to f23c73a Compare October 5, 2022 15:29

remi-delmas-3000 requested review from nwetzler and feliperodri October 5, 2022 15:30

feliperodri approved these changes Oct 5, 2022

View reviewed changes

remi-delmas-3000 force-pushed the contracts-frees-clauses branch from f23c73a to 66a7c5d Compare October 5, 2022 15:51

jimgrundy added the C Front End label Oct 5, 2022

tautschnig self-assigned this Oct 6, 2022

feliperodri changed the title ~~CONTRACTS: Add __CPROVER_frees clauses in the front end.~~ CONTRACTS: Add __CPROVER_frees clauses in the front end Oct 6, 2022

feliperodri approved these changes Oct 6, 2022

View reviewed changes

remi-delmas-3000 force-pushed the contracts-frees-clauses branch 2 times, most recently from 74c89b3 to d236601 Compare October 6, 2022 19:42

nwetzler approved these changes Oct 6, 2022

View reviewed changes

feliperodri added the blocker label Oct 6, 2022

tautschnig approved these changes Oct 7, 2022

View reviewed changes

tautschnig removed their assignment Oct 7, 2022

diffblue deleted a comment from tautschnig Oct 7, 2022

remi-delmas-3000 force-pushed the contracts-frees-clauses branch from d236601 to 5982243 Compare October 7, 2022 18:53

feliperodri approved these changes Oct 7, 2022

View reviewed changes

remi-delmas-3000 merged commit 178df3d into diffblue:develop Oct 7, 2022


		### Syntax
		The set of locations described by the contract is the union of the locations

		The set of pointers specified by the frees clause of the contract is interpreted
		at the function call-site.

		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.

CONTRACTS: Add __CPROVER_frees clauses in the front end #7091

CONTRACTS: Add __CPROVER_frees clauses in the front end #7091

Uh oh!

Conversation

remi-delmas-3000 commented Aug 31, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov bot commented Aug 31, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tautschnig Sep 1, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

remi-delmas-3000 commented Aug 31, 2022 •

edited

Loading

codecov bot commented Aug 31, 2022 •

edited

Loading

tautschnig Sep 1, 2022 •

edited

Loading