CONTRACTS: store contracts in dedicated symbols #6799

tautschnig · 2022-04-10T14:32:02Z

Contracts can now be placed on declarations or definitions, and result
in a fresh symbol being generated. That new symbol has its name prefixed
with "contracts::" to place them in a pseudo-namespace, and has
"is_property" set (which was an otherwise unused symbolt flag).

Co-authored-by: Remi Delmas [email protected]

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.
n/a 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.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2022-04-10T15:52:29Z

Codecov Report

Merging #6799 (d3ed223) into develop (897034a) will decrease coverage by 0.00%.
The diff coverage is 82.02%.

@@             Coverage Diff             @@
##           develop    #6799      +/-   ##
===========================================
- Coverage    77.83%   77.83%   -0.01%     
===========================================
  Files         1568     1569       +1     
  Lines       180365   180634     +269     
===========================================
+ Hits        140382   140589     +207     
- Misses       39983    40045      +62

Impacted Files	Coverage Δ
src/goto-instrument/contracts/contracts.h	`100.00% <ø> (ø)`
...oto-instrument/contracts/instrument_spec_assigns.h	`94.73% <ø> (ø)`
src/goto-instrument/contracts/utils.h	`100.00% <ø> (+16.07%)`	⬆️
src/goto-instrument/horn_encoding.cpp	`72.70% <0.00%> (+0.43%)`	⬆️
...c/solvers/smt2_incremental/convert_expr_to_smt.cpp	`87.71% <0.00%> (-0.62%)`	⬇️
src/solvers/smt2_incremental/smt_sorts.def	`66.66% <0.00%> (-33.34%)`	⬇️
src/util/config.h	`57.14% <ø> (ø)`
src/util/replace_symbol.cpp	`78.20% <36.95%> (-10.10%)`	⬇️
src/linking/linking.cpp	`58.96% <50.00%> (-0.03%)`	⬇️
src/util/rename_symbol.cpp	`76.82% <69.38%> (-3.00%)`	⬇️
... and 19 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 5186d6f...d3ed223. Read the comment docs.

remi-delmas-3000

It would be nice to make the contract completely self-contained by introducing fresh/prefixed names for the parameters, rewriting the contract clauses with the fresh names, and removing the body if any.

src/ansi-c/c_typecheck_base.cpp

remi-delmas-3000 · 2022-04-12T21:21:57Z

src/ansi-c/c_typecheck_base.cpp

+          for(const auto &parameter : code_type.parameters())
+          {
+            const irep_idt &identifier = parameter.get_identifier();
+
+            symbol_tablet::symbolst::const_iterator p_s_it =
+              symbol_table.symbols.find(identifier);
+            if(p_s_it != symbol_table.symbols.end())
+              symbol_table.erase(p_s_it);


Here I would rather replace the contract parameters with fresh symbols (maybe just by prefixing the function parameters with a contract:: prefix, and also rewrite the contract clauses with these new parameters using a replacet.

Later we would be able to generate a body for the contract without symbol clashes between function and contract symbols and make the contract fully self-contained.

I believe we could still choose to create those fresh symbols if and when needed: all the required information still is in the contract symbol.

remi-delmas-3000 · 2022-04-12T21:28:04Z

src/goto-instrument/contracts/contracts.cpp

+  }
+
+  const auto &type = to_code_with_contract_type(contract_sym->type);
+  if(type != function_symbol.type)


How can this equality work if the function symbol had its contract clauses removed but the contract symbol still has them ?

Would the check still work if in addition we removed the function body from the contract and renamed contract parameters ?

Maybe we could just check that the number of arguments and their types are equal.

This perhaps warrants an extra comment: the comparison works, because all the extra information is stored in comment-elements of the ireps: both the parameter identifiers as well as all the contract clauses have ID_C_... keys in the irept. Therefore, equality (but not full equality!) works out. While the body isn't there as indicated in the earlier comment, it wouldn't affect this comparison either way for it's just a comparison of the types, not the symbols' values.

src/linking/remove_internal_symbols.cpp

tautschnig · 2022-05-31T15:22:14Z

@kroening @remi-delmas-3000 I have put the additional changes to make use of lambda_exprt in a commit of its own, but it should now be working.

feliperodri

LGTM, thanks @tautschnig!

src/ansi-c/c_typecheck_base.cpp

src/goto-instrument/contracts/contracts.cpp

SaswatPadhi

LGTM overall; couple of minor comments below.

src/goto-instrument/contracts/contracts.cpp

feliperodri · 2022-06-20T23:13:20Z

@chris-ryder, @kroening, @martin-cs, and/or @peterschrammel, could we get one more review on this PR? It's missing code owner approval.

Contracts can now be placed on declarations or definitions, and result in a fresh symbol being generated. That new symbol has its name prefixed with "contracts::" to place them in a pseudo-namespace, and has "is_property" set (which was an otherwise unused symbolt flag). Co-authored-by: Remi Delmas <[email protected]>

All that was used was its source location, which we can obtain in a different way.

This makes sure contracts are self-contained in that any parameter names that may have only existed in the scope of a function declaration are now bound variables.

Contract symbols (diffblue#6799) have the same base name as the function symbol they are derived from. This causes both the function and its contract to be found when doing a lookup by base name, when resolving entry points for instance. We now filter out symbols that have the `is_property` set when resolving entry points and interrupt handlers in a goto model.

tautschnig added dependent - do not merge Code Contracts Function and loop contracts labels Apr 10, 2022

tautschnig assigned tautschnig and remi-delmas-3000 Apr 10, 2022

tautschnig force-pushed the feature/contract-symbols branch from 9646592 to f90e01b Compare April 11, 2022 14:26

tautschnig changed the title ~~CONTRACTS: store contracts in dedicated symbols [depends-on: #6796]~~ CONTRACTS: store contracts in dedicated symbols Apr 11, 2022

tautschnig removed the dependent - do not merge label Apr 11, 2022

tautschnig marked this pull request as ready for review April 11, 2022 14:26

tautschnig requested review from feliperodri, SaswatPadhi, kroening, peterschrammel and chris-ryder as code owners April 11, 2022 14:26

tautschnig assigned SaswatPadhi, kroening, feliperodri and chris-ryder and unassigned tautschnig Apr 11, 2022

tautschnig force-pushed the feature/contract-symbols branch from f90e01b to cb1a58c Compare April 11, 2022 20:02

remi-delmas-3000 reviewed Apr 12, 2022

View reviewed changes

tautschnig force-pushed the feature/contract-symbols branch 2 times, most recently from 8d40abb to 8753639 Compare April 17, 2022 20:54

jimgrundy added aws Bugs or features of importance to AWS CBMC users aws-high labels Apr 20, 2022

tautschnig force-pushed the feature/contract-symbols branch from 8753639 to 39690e1 Compare May 2, 2022 16:46

tautschnig requested a review from martin-cs as a code owner May 2, 2022 16:46

tautschnig force-pushed the feature/contract-symbols branch from 39690e1 to 1d0340c Compare May 7, 2022 21:30

tautschnig self-assigned this May 25, 2022

tautschnig force-pushed the feature/contract-symbols branch from 1d0340c to adbef76 Compare May 31, 2022 09:58

tautschnig force-pushed the feature/contract-symbols branch 2 times, most recently from c2f8b7b to a3f9db2 Compare May 31, 2022 15:20

tautschnig removed their assignment May 31, 2022

tautschnig force-pushed the feature/contract-symbols branch from a3f9db2 to 5914a14 Compare June 1, 2022 10:02

feliperodri approved these changes Jun 20, 2022

View reviewed changes

src/ansi-c/c_typecheck_base.cpp Show resolved Hide resolved

src/goto-instrument/contracts/contracts.cpp Show resolved Hide resolved

feliperodri requested a review from remi-delmas-3000 June 20, 2022 21:35

SaswatPadhi approved these changes Jun 20, 2022

View reviewed changes

src/goto-instrument/contracts/contracts.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/contracts.cpp Show resolved Hide resolved

peterschrammel approved these changes Jun 21, 2022

View reviewed changes

tautschnig assigned tautschnig and unassigned SaswatPadhi and feliperodri Jun 21, 2022

tautschnig force-pushed the feature/contract-symbols branch 2 times, most recently from d235c00 to 2a9d14c Compare June 21, 2022 19:25

tautschnig removed their assignment Jun 21, 2022

feliperodri mentioned this pull request Jun 27, 2022

Pure contacts #6773

Closed

7 tasks

tautschnig and others added 3 commits June 28, 2022 08:30

Code contracts: remove useless skip statement

b6975af

All that was used was its source location, which we can obtain in a different way.

Wrap contract expressions in a lambda

d3ed223

This makes sure contracts are self-contained in that any parameter names that may have only existed in the scope of a function declaration are now bound variables.

tautschnig force-pushed the feature/contract-symbols branch from 2a9d14c to d3ed223 Compare June 28, 2022 08:31

kroening approved these changes Jun 30, 2022

View reviewed changes

tautschnig merged commit b466503 into diffblue:develop Jun 30, 2022

tautschnig deleted the feature/contract-symbols branch June 30, 2022 18:17

This was referenced Jun 30, 2022

Add support for function contracts in cprover_bindings. model-checking/kani#1302

Merged

Code contracts: match up introducing/removing parameter map modifications #2278

Closed

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

CONTRACTS: filter out contract symbols when resolving entry points and interrupt handlers #7063

Merged

4 tasks

monal mentioned this pull request Aug 17, 2022

Add macro expansion for function contracts. model-checking/kani#1503

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

CONTRACTS: store contracts in dedicated symbols #6799

CONTRACTS: store contracts in dedicated symbols #6799

Uh oh!

tautschnig commented Apr 10, 2022

Uh oh!

codecov bot commented Apr 10, 2022 •

edited

Loading

Uh oh!

remi-delmas-3000 left a comment

Uh oh!

Uh oh!

remi-delmas-3000 Apr 12, 2022

Uh oh!

tautschnig Apr 13, 2022

Uh oh!

remi-delmas-3000 Apr 12, 2022

Uh oh!

tautschnig Apr 13, 2022

Uh oh!

Uh oh!

tautschnig commented May 31, 2022

Uh oh!

feliperodri left a comment

Uh oh!

Uh oh!

Uh oh!

SaswatPadhi left a comment

Uh oh!

Uh oh!

Uh oh!

feliperodri commented Jun 20, 2022

Uh oh!

Uh oh!

CONTRACTS: store contracts in dedicated symbols #6799

CONTRACTS: store contracts in dedicated symbols #6799

Uh oh!

Conversation

tautschnig commented Apr 10, 2022

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

remi-delmas-3000 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

remi-delmas-3000 Apr 12, 2022

Choose a reason for hiding this comment

Uh oh!

tautschnig Apr 13, 2022

Choose a reason for hiding this comment

Uh oh!

remi-delmas-3000 Apr 12, 2022

Choose a reason for hiding this comment

Uh oh!

tautschnig Apr 13, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tautschnig commented May 31, 2022

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

SaswatPadhi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

feliperodri commented Jun 20, 2022

Uh oh!

Uh oh!

codecov bot commented Apr 10, 2022 •

edited

Loading