CONTRACTS: Front-end extensions for assigns clauses #7086

remi-delmas-3000 · 2022-08-25T16:45:43Z

The first commit tags some JBMC tests as THOROUGH because they seem to exceed resources available for the ubuntu 18.04 target when building this PR

Add new functions to specify assignable targets in assigns clauses:

add polymorhpic builtin __CPROVER_typed_target
add builtin __CPROVER_assignable
add builtin __CPROVER_object_whole
add builtin __CPROVER_object_from
add builtin __CPROVER_object_upto
allow function call expressions as assigns
clause targets as long as they are one of
the new built-ins

Using __CPROVER_POINTER_OBJECT in assigns clauses is still allowed for now (needed for loop contracts),
will be deprecated in #7127.

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-25T22:42:20Z

Codecov Report

Base: 77.88% // Head: 77.89% // Increases project coverage by +0.00% 🎉

Coverage data is based on head (45c677e) compared to base (6d6319f).
Patch coverage: 86.23% of modified lines in pull request are covered.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #7086   +/-   ##
========================================
  Coverage    77.88%   77.89%           
========================================
  Files         1576     1576           
  Lines       181859   181913   +54     
========================================
+ Hits        141648   141699   +51     
- Misses       40211    40214    +3

Impacted Files	Coverage Δ
src/ansi-c/ansi_c_internal_additions.cpp	`90.12% <ø> (ø)`
src/ansi-c/c_typecheck_base.h	`100.00% <ø> (ø)`
src/ansi-c/c_typecheck_expr.cpp	`74.15% <81.25%> (-0.05%)`	⬇️
src/ansi-c/c_typecheck_code.cpp	`77.75% <82.14%> (+0.60%)`	⬆️
...o-instrument/contracts/instrument_spec_assigns.cpp	`98.77% <85.71%> (-0.59%)`	⬇️
src/ansi-c/ansi_c_entry_point.cpp	`89.57% <100.00%> (ø)`
src/ansi-c/c_typecheck_base.cpp	`82.99% <100.00%> (+0.49%)`	⬆️
src/linking/remove_internal_symbols.cpp	`100.00% <100.00%> (ø)`
... and 2 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.

feliperodri

I'd suggest that future PRs could be break down into smaller commits and maybe you wanna move everything related to frees clauses to the next PR (which would remove the dependency from the other PR and make both of them much cleaner). Apart from that, only small comments. Great improvement!!!

doc/cprover-manual/contracts-assigns.md

doc/cprover-manual/contracts-frees.md

regression/contracts/reject_return_value_in_frees_clause/main.c

regression/contracts/reject_return_value_in_preconditions/main.c

regression/contracts/typed_target_fail_wrong_nof_operand/main.c

feliperodri · 2022-08-30T22:19:33Z

regression/contracts/typed_target_fail_wrong_nof_operand/test.desc

+^SIGNAL=0$
+--
+--
+This test checks that __CPROVER_old occurences in assigns clauses


Not true, update the description.

regression/contracts/typed_target_pointer/main.c

feliperodri

A few more comments but it should be good to go.

feliperodri · 2022-09-01T19:31:14Z

regression/contracts/typed_target_fail_wrong_nof_operand/test.desc

+^SIGNAL=0$
+--
+--
+This test checks that __CPROVER_old occurences in assigns clauses


src/ansi-c/c_typecheck_code.cpp

feliperodri · 2022-09-01T19:34:43Z

src/ansi-c/c_typecheck_code.cpp

+    {
+      must_throw = true;
+      error().source_location = target.source_location();
+      error() << "expected ID_conditional_target_group expression in " +


Do we want to inform users about ID_conditional_target_group? Perhaps we could have a more informative message.

The syntax section of the manual defines a conditional target group as :

conditional-target-group ::= (condition ':')? target (',' target)*

How about using conditional target group instead of ID_conditional_target_group to make it more human-readable ?

src/ansi-c/c_typecheck_expr.cpp

doc/cprover-manual/contracts-assigns.md

tautschnig · 2022-09-02T08:45:59Z

Just noting that I posted a bunch of comments in #7091 that apply to the second commit of this PR. Apologies for not noticing that I should have reviewed this one first. Will re-review this one once the updates have been made.

remi-delmas-3000 · 2022-09-12T19:34:06Z

@tautschnig the typedef void __CPROVER_assignable_t has been removed as suggested.

feliperodri

Only minor comments.

regression/contracts/assigns_enforce_arrays_02/test.desc

doc/cprover-manual/contracts-assigns.md

feliperodri

LGTM! @tautschnig I think this PR is ready for your final review.

tautschnig · 2022-09-16T21:22:59Z

doc/cprover-manual/contracts-assigns.md


-## In Function Contracts
+An _assigns clause_ lets the user to specify which memory locations may be


tautschnig · 2022-09-16T21:24:22Z

doc/cprover-manual/contracts-assigns.md


-## In Function Contracts
+An _assigns clause_ lets the user to specify which memory locations may be
+assigned to by a function or a loop.


Perhaps a sentence or two can be added why assigns clauses are useful/required? The above says what they describe, but (naively speaking) life would be easier if one didn't have to write any such clauses.

doc/cprover-manual/contracts-assigns.md

tautschnig · 2022-09-16T21:27:01Z

doc/cprover-manual/contracts-assigns.md

+the set of locations assigned by the loop from the loop body,
+and then checks that the inferred set is correct (as if specified by the user).


So why couldn't we do this for functions as well? Conversely, is it a desirable feature to have this difference in semantics of an unspecified assigns clause? Should we perhaps have a keyword auto that's permitted in loop assigns clauses only?

Thinking about it, I think we can do it today for loops because the assigns clause inference, the loop abstraction and the verification of the inferred clause all happen at the same time in the same analysis.

For function contracts we operate either in contract checking or contract replacement mode and we cannot infer check and replace the assigns clause in a single run.

In a later version we could introduce something like '__CPROVER_assigns(auto)` which would mean "when this contract is used to replace some function call, infer the set of memory locations from the code of the function, check that the result is correct in a separate analysis, and use that inferred clause to havoc state at the replacement site"

One way to figure out the side effects of a particular function could be to check it under an empty assigns clause and to turn all reported violations into an assigns clause.

doc/cprover-manual/contracts-assigns.md

src/ansi-c/ansi_c_internal_additions.cpp

src/ansi-c/c_typecheck_base.cpp

src/ansi-c/c_typecheck_code.cpp

src/ansi-c/c_typecheck_expr.cpp

src/goto-instrument/contracts/instrument_spec_assigns.cpp

nwetzler · 2022-09-26T23:35:54Z

src/goto-instrument/contracts/instrument_spec_assigns.cpp

+          minus_exprt(
+            typecast_exprt::conditional_cast(ptr, pointer_type(char_type())),
+            pointer_offset(ptr)),
+          typecast_exprt::conditional_cast(object_size(ptr), size_type()),


src/ansi-c/c_typecheck_code.cpp

doc/cprover-manual/contracts-assigns.md

regression/contracts/reject_history_expr_in_assigns_clause/test.desc

Add new functions to specify assignable targets in assigns clauses: - add polymorhpic builtin __CPROVER_typed_target - add builtin __CPROVER_assignable - add builtin __CPROVER_object_whole - add builtin __CPROVER_object_from - add builtin __CPROVER_object_upto - allow function call expressions as assigns clause targets as long as they are one of the new built-ins Using __CPROVER_POINTER_OBJECT is still allowed (for loop contracts), will be deprecated in an ulterior PR.

remi-delmas-3000 requested review from tautschnig, feliperodri, SaswatPadhi, kroening, peterschrammel and chris-ryder as code owners August 25, 2022 16:45

This was referenced Aug 25, 2022

CONTRACTS: Front-end: frees clause improvements #7087

Closed

CONTRACTS: Dynamic frame condition checking #6887

Closed

remi-delmas-3000 force-pushed the assignable_t-builtins-frees-clause branch from 9d1e966 to 399a2c2 Compare August 25, 2022 21:34

remi-delmas-3000 force-pushed the assignable_t-builtins-frees-clause branch 3 times, most recently from d450da6 to 9614c1b Compare August 26, 2022 04:18

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

remi-delmas-3000 force-pushed the assignable_t-builtins-frees-clause branch 2 times, most recently from 7baf31d to 0d8b076 Compare August 30, 2022 21:55

feliperodri requested changes Aug 30, 2022

View reviewed changes

feliperodri assigned remi-delmas-3000 and SaswatPadhi Aug 30, 2022

remi-delmas-3000 force-pushed the assignable_t-builtins-frees-clause branch 3 times, most recently from 80d3b26 to 52313ad Compare August 31, 2022 17:29

remi-delmas-3000 changed the title ~~CONTRACTS: Front-end extensions for assigns clauses and frees clauses.~~ CONTRACTS: Front-end extensions for assigns clauses Aug 31, 2022

remi-delmas-3000 force-pushed the assignable_t-builtins-frees-clause branch from 52313ad to 60f8feb Compare August 31, 2022 18:34

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

CONTRACTS: Add __CPROVER_frees clauses in the front end #7091

Merged

6 tasks

remi-delmas-3000 force-pushed the assignable_t-builtins-frees-clause branch from 60f8feb to 13e3332 Compare September 1, 2022 17:58

feliperodri approved these changes Sep 1, 2022

View reviewed changes

tautschnig self-assigned this Sep 7, 2022

remi-delmas-3000 force-pushed the assignable_t-builtins-frees-clause branch from 13e3332 to e851cf4 Compare September 12, 2022 19:33

remi-delmas-3000 force-pushed the assignable_t-builtins-frees-clause branch from e851cf4 to a118518 Compare September 12, 2022 20:17

feliperodri approved these changes Sep 12, 2022

View reviewed changes

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

CONTRACTS: Support slice targets in loop assigns clauses #7127

Merged

7 tasks

remi-delmas-3000 force-pushed the assignable_t-builtins-frees-clause branch from a118518 to 21dbb9b Compare September 13, 2022 22:29

feliperodri approved these changes Sep 14, 2022

View reviewed changes

feliperodri unassigned SaswatPadhi Sep 14, 2022

tautschnig reviewed Sep 16, 2022

View reviewed changes

tautschnig reviewed Sep 17, 2022

View reviewed changes

tautschnig removed their assignment Sep 17, 2022

SaswatPadhi removed their request for review September 17, 2022 09:27

remi-delmas-3000 force-pushed the assignable_t-builtins-frees-clause branch 2 times, most recently from 2f53348 to 6bac320 Compare September 23, 2022 15:20

jimgrundy requested a review from nwetzler September 25, 2022 21:19

nwetzler approved these changes Sep 26, 2022

View reviewed changes

nwetzler reviewed Sep 27, 2022

View reviewed changes

regression/contracts/reject_history_expr_in_assigns_clause/test.desc Show resolved Hide resolved

tautschnig approved these changes Sep 28, 2022

View reviewed changes

remi-delmas-3000 force-pushed the assignable_t-builtins-frees-clause branch from 6bac320 to 45c677e Compare September 28, 2022 14:02

remi-delmas-3000 merged commit f23120d into diffblue:develop Sep 28, 2022


		## In Function Contracts
		An _assigns clause_ lets the user to specify which memory locations may be

		the set of locations assigned by the loop from the loop body,
		and then checks that the inferred set is correct (as if specified by the user).

CONTRACTS: Front-end extensions for assigns clauses #7086

CONTRACTS: Front-end extensions for assigns clauses #7086

Uh oh!

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

feliperodri left a comment • 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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

feliperodri left a comment

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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tautschnig commented Sep 2, 2022

Uh oh!

remi-delmas-3000 commented Sep 12, 2022

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

feliperodri left a comment

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!

Choose a reason for hiding this comment

Uh oh!

remi-delmas-3000 Sep 22, 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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

remi-delmas-3000 commented Aug 25, 2022 •

edited

Loading

codecov bot commented Aug 25, 2022 •

edited

Loading

feliperodri left a comment •

edited

Loading

remi-delmas-3000 Sep 22, 2022 •

edited

Loading