Pure contacts

[remi-delmas-3000]

What is this needed for

This is needed to implement contracts for function pointers. A pure contract is used as a default value for a function pointer passed from the environment for which we assume a contract holds.

Pure contracts

We introduce a new built-in void __CPROVER_pure_contract() which can be used to mark a function as a pure contract:

int foo()
___CPROVER_requires(...)
___CPROVER_ensures(...)
___CPROVER_assigns(...)
{
   __CPROVER_pure_contract();
}

• The call to __CPROVER_pure_contract must be the only statement in the body of the function
• Improper uses of __CPROVER_pure_contract (i.e. in functions that contain other instructions) will trigger conversion errors
• Correct uses of the built-in get converted to an assert(false, "all calls replaced") with property class ID_pure_contract.

This essentially forces the user to replace calls to pure contracts by their actual contract. To make this easy on the user, a new goto-instrument CLI switch --replace-pure-contracts has been added, which replaces all calls to pure contracts globally.

Once replacement is done, the ID_pure_contract assertions cannot be falsified anymore.

Next steps

In a subsequent PR we will completely automate the generation of the body of the pure contract from the contract clauses and remove the --replace-pure-contracts CLI switch and assert(false, "all calls replaced") assertion.

• 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).
• 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]

Codecov Report

Merging #6773 (8653f0b) into develop (f972150) will increase coverage by 0.00%.
The diff coverage is 100.00%.

@@           Coverage Diff            @@
##           develop    #6773   +/-   ##
========================================
  Coverage    76.90%   76.91%           
========================================
  Files         1590     1590           
  Lines       183970   184026   +56     
========================================
+ Hits        141484   141542   +58     
+ Misses       42486    42484    -2     

Impacted Files	Coverage Δ
src/ansi-c/c_typecheck_base.h	100.00% <ø> (ø)
src/goto-instrument/contracts/contracts.h	100.00% <ø> (ø)
...rc/goto-instrument/goto_instrument_parse_options.h	100.00% <ø> (ø)
src/goto-programs/resolve_inherited_component.h	100.00% <ø> (ø)
src/solvers/flattening/boolbv_map.h	100.00% <ø> (ø)
src/util/expr.h	97.22% <ø> (ø)
src/ansi-c/c_typecheck_base.cpp	79.04% <100.00%> (+0.99%)	⬆️
src/ansi-c/c_typecheck_expr.cpp	77.18% <100.00%> (+0.12%)	⬆️
src/goto-instrument/contracts/contracts.cpp	93.80% <100.00%> (+0.10%)	⬆️
.../goto-instrument/goto_instrument_parse_options.cpp	69.50% <100.00%> (+0.11%)	⬆️
... and 7 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update b04b4b5...8653f0b. Read the comment docs.

[feliperodri]

This is being replaced by #6799.