CONTRACTS: refactor DFCC code for loop contracts #7551

remi-delmas-3000 · 2023-02-16T22:39:12Z

This PR refactors the DFCC code to make it possible to handle loop assigns clauses in #7541.

We now have a standalone class dfcc_contract_clauses_codegent which provides methods to generate GOTO programs that initialize a dynamic frame instance from an assigns clause specification or havoc the targets of an assigns clause.

Before, these code generation methods were encapsulated inside the class dfcc_contract_functionst which exclusively handles function contracts. This makes them available for loop contracts as well.

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.

martin-cs

I have not reviewed the contracts/dynamic-frames part. @remi-delmas-3000 I can if you want. The rest looks good but I notice the overlap with #7550 so it would be good to have this rebased when it is merged.

feliperodri

LGTM.

feliperodri · 2023-02-17T18:46:31Z

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

+  // TODO specialise the library functions for the max size of
+  // loop and function contracts


Shall we create a GitHub issue about this and add the link here? It might be better to track this later.

this is still work in progress this will already be addressed in the final version

But then ... haven't you resolved the "TODO" and should remove this comment?

This has to be implemented in the forthcoming loop contracts PR, this TODO is just a marker that tells you where to do it

Sorry this one is a TODO for @qinheping , my comment above applied to two other TODOs I've turned into reqs.

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp

src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp

tautschnig

Approving with a couple of comments that really need to be addressed.

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp

tautschnig · 2023-02-22T09:20:59Z

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

+  // TODO specialise the library functions for the max size of
+  // loop and function contracts


But then ... haven't you resolved the "TODO" and should remove this comment?

This has to be implemented in the forthcoming loop contracts PR, this TODO is just a marker that tells you where to do it

tautschnig · 2023-02-22T09:24:06Z

src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp

+  std::set<irep_idt> function_pointer_contracts;
+  instrument.instrument_function(function_id, function_pointer_contracts);
+  INVARIANT(
+    function_pointer_contracts.size() == 0,


You might want to use .empty() instead of .size() == 0.

src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

Allows to to inlining and loop detection directly on a goto program instead of a goto function

- Factor out some methods in dfcc_spec_functionst - Move the code generation methods from dfcc_contract_functionst to dfcc_contract_clauses_codegent. - Update Makefile with new class. - Propagate interface changes to top level class

Enable checking for the presence of dynamic allocations or deallocations in loop bodies and transitively in the functions called from loop bodies. - Adds `allow_allocate` and `allow_deallocate` flags in the write set struct - Modify `add_allocated` to fail an assertion when called on a write set with `allow_allocate` set to false. - Modify `check_deallocate` to return false when called on a write set with `allow_deallocate` set to false. - Don't treat replacement mode specially anymore, always store freeable targets in both the object map (for lookups) and in the append list (for inclusion checks).

remi-delmas-3000 added aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels Feb 16, 2023

remi-delmas-3000 self-assigned this Feb 16, 2023

remi-delmas-3000 requested review from tautschnig, feliperodri, martin-cs, chris-ryder, peterschrammel and kroening as code owners February 16, 2023 22:39

remi-delmas-3000 requested a review from qinheping February 16, 2023 22:42

martin-cs approved these changes Feb 17, 2023

View reviewed changes

remi-delmas-3000 force-pushed the contracts-codegen-loop-assigns branch 3 times, most recently from c78a3cc to bb8e8e8 Compare February 17, 2023 15:31

remi-delmas-3000 added do not merge work in progress do not review dependent - do not merge labels Feb 17, 2023

remi-delmas-3000 force-pushed the contracts-codegen-loop-assigns branch 3 times, most recently from ed8ac89 to ad9e93f Compare February 17, 2023 17:33

feliperodri approved these changes Feb 17, 2023

View reviewed changes

feliperodri assigned tautschnig and qinheping and unassigned tautschnig and qinheping Feb 17, 2023

remi-delmas-3000 marked this pull request as draft February 17, 2023 21:56

remi-delmas-3000 force-pushed the contracts-codegen-loop-assigns branch 3 times, most recently from bc8071e to 961bc8c Compare February 20, 2023 15:42

remi-delmas-3000 force-pushed the contracts-codegen-loop-assigns branch from 961bc8c to 58e87a3 Compare February 21, 2023 16:28

remi-delmas-3000 removed do not merge work in progress do not review dependent - do not merge labels Feb 21, 2023

remi-delmas-3000 marked this pull request as ready for review February 21, 2023 16:31

remi-delmas-3000 force-pushed the contracts-codegen-loop-assigns branch from 58e87a3 to f7ae59e Compare February 21, 2023 16:34

feliperodri added the aws-high label Feb 21, 2023

tautschnig approved these changes Feb 22, 2023

View reviewed changes

Remi Delmas added 5 commits February 22, 2023 16:28

CONTRACTS: new inlining and loop detection methods

1ad6ecc

Allows to to inlining and loop detection directly on a goto program instead of a goto function

CONTRACTS: rearchitecture code for loop contracts

8427b1f

- Factor out some methods in dfcc_spec_functionst - Move the code generation methods from dfcc_contract_functionst to dfcc_contract_clauses_codegent. - Update Makefile with new class. - Propagate interface changes to top level class

CONTRACTS: new c++ methods to build calls to cprover_contracts library

da85771

address review comments

fb35a17

remi-delmas-3000 force-pushed the contracts-codegen-loop-assigns branch from 1e354f7 to fb35a17 Compare February 22, 2023 16:28

remi-delmas-3000 merged commit b04cbf3 into diffblue:develop Feb 22, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

CONTRACTS: refactor DFCC code for loop contracts #7551

CONTRACTS: refactor DFCC code for loop contracts #7551

remi-delmas-3000 commented Feb 16, 2023 •

edited

Loading

martin-cs left a comment

feliperodri left a comment

feliperodri Feb 17, 2023

remi-delmas-3000 Feb 20, 2023

remi-delmas-3000 Feb 21, 2023 •

edited

Loading

tautschnig Feb 22, 2023 •

edited by remi-delmas-3000

Loading

remi-delmas-3000 Feb 22, 2023 •

edited

Loading

tautschnig left a comment

tautschnig Feb 22, 2023 •

edited by remi-delmas-3000

Loading

tautschnig Feb 22, 2023

		// TODO specialise the library functions for the max size of
		// loop and function contracts

CONTRACTS: refactor DFCC code for loop contracts #7551

CONTRACTS: refactor DFCC code for loop contracts #7551

Conversation

remi-delmas-3000 commented Feb 16, 2023 • edited Loading

martin-cs left a comment

Choose a reason for hiding this comment

feliperodri left a comment

Choose a reason for hiding this comment

feliperodri Feb 17, 2023

Choose a reason for hiding this comment

remi-delmas-3000 Feb 20, 2023

Choose a reason for hiding this comment

remi-delmas-3000 Feb 21, 2023 • edited Loading

Choose a reason for hiding this comment

tautschnig Feb 22, 2023 • edited by remi-delmas-3000 Loading

Choose a reason for hiding this comment

remi-delmas-3000 Feb 22, 2023 • edited Loading

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig Feb 22, 2023 • edited by remi-delmas-3000 Loading

Choose a reason for hiding this comment

tautschnig Feb 22, 2023

Choose a reason for hiding this comment

remi-delmas-3000 commented Feb 16, 2023 •

edited

Loading

remi-delmas-3000 Feb 21, 2023 •

edited

Loading

tautschnig Feb 22, 2023 •

edited by remi-delmas-3000

Loading

remi-delmas-3000 Feb 22, 2023 •

edited

Loading

tautschnig Feb 22, 2023 •

edited by remi-delmas-3000

Loading