CONTRACTS: Support bounded user defined memory-predicates #7401

remi-delmas-3000 · 2022-11-29T21:40:32Z

Users can now write their own pointer predicates in terms of:

__CPROVER_is_fresh(ptr, size)
__CPROVER_pointer_in_range(lb, ptr, ub)
__CPROVER_obeys_contract(ptr, target)

A rewriting pass lifts these user-defined pointer predicates
into predicates that take pointer by reference and can
make the predicates hold in assumption contexts
using side-effects, and check the predicates in assertion
contexts.

Limitiations:
User-defined predicates can be self-recursive but not mutually
recursive, and their evaluation needs to be terminate, i.e. they
can only describe bounded data structures.

The doxygen user and developer manuals and has been updated to describe the feature and its implementation.
Tests were added, and existing tests cleaned-up.

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 · 2022-11-30T09:12:26Z

Codecov Report

Base: 78.38% // Head: 78.41% // Increases project coverage by +0.03% 🎉

Coverage data is based on head (3618d8a) compared to base (bb9d8e3).
Patch coverage: 91.69% of modified lines in pull request are covered.

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

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7401      +/-   ##
===========================================
+ Coverage    78.38%   78.41%   +0.03%     
===========================================
  Files         1651     1655       +4     
  Lines       190045   190264     +219     
===========================================
+ Hits        148961   149201     +240     
+ Misses       41084    41063      -21

Impacted Files	Coverage Δ
...contracts/dynamic-frames/dfcc_contract_handler.cpp	`100.00% <ø> (ø)`
...t/contracts/dynamic-frames/dfcc_contract_handler.h	`100.00% <ø> (ø)`
...strument/contracts/dynamic-frames/dfcc_library.cpp	`95.54% <ø> (ø)`
...t/contracts/dynamic-frames/dfcc_spec_functions.cpp	`89.54% <ø> (+15.88%)`	⬆️
...ent/contracts/dynamic-frames/dfcc_spec_functions.h	`100.00% <ø> (ø)`
src/libcprover-cpp/api.h	`100.00% <ø> (ø)`
...cts/dynamic-frames/dfcc_lift_memory_predicates.cpp	`89.60% <89.60%> (ø)`
src/ansi-c/c_typecheck_expr.cpp	`75.68% <100.00%> (+0.08%)`	⬆️
.../goto-instrument/contracts/dynamic-frames/dfcc.cpp	`97.68% <100.00%> (+0.12%)`	⬆️
...ument/contracts/dynamic-frames/dfcc_instrument.cpp	`81.44% <100.00%> (+0.15%)`	⬆️
... and 6 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

Only some minor changes before approval.

src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h

src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md

src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md

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

remi-delmas-3000 · 2022-12-07T21:21:06Z

A reader might believe that __CPROVER_is_in_range ought to apply to types other than pointers, e.g., integers, or floating-point numbers. It may make sense to make that predicate polymorphic. Can you simply use __CPROVER_pointer_in_range?

Will fix.

EDIT:
My instrumentation pass maps predicate calls to built-in predicates to special implementations that takes the dynamic frame as parameter and to make it context-aware (assert vs. assume).

Right now the front-end maps __CPROVER_pointer_in_range calls to pointer_in_range_exprt expressions that get lowered during goto-conversion, so when my pass happens pointer_in_range_exprt is not there for me to match and replace anymore.

@tautschnig is currently working on moving the lowering of built-ins to the back end #7395, which would solve my problem by keeping pointer_in_range_exprt intact out of goto-conversion.

The best I can do for the moment is to temporarily rename my __CPROVER_is_in_range predicate to __CPROVER_pointer_in_range_dfcc so it does not get lowered during goto conversion and my pass can still work.

I'll update my code to pointer_in_range_exprt when #7395 gets merged.

@kroening Would that work for you ?

regression/contracts-dfcc/memory-predicates-is-in-range-requires/test.desc

regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/test.desc

regression/contracts-dfcc/memory-predicates-is-in-range-several-targets/main.c

tautschnig · 2022-12-07T22:37:48Z

src/ansi-c/c_typecheck_expr.cpp

+  else if(identifier == CPROVER_PREFIX "is_in_range")
+  {
+    // same as pointer_in_range with experimental feature for DFCC contracts
+    // -- do not use
+    if(expr.arguments().size() != 3)
+    {
+      throw invalid_source_file_exceptiont{
+        "is_in_range expects three arguments", expr.source_location()};
+    }
+
+    for(const auto &arg : expr.arguments())
+    {
+      if(arg.type().id() != ID_pointer)
+      {
+        throw invalid_source_file_exceptiont{
+          "is_in_range expects pointer-typed arguments", arg.source_location()};
+      }
+    }
+    return nil_exprt();
+  }


Can this (and any other support for __CPROVER_is_in_range) please go in a commit of its own? #7395 should make it completely unnecessary.

I think this would be in line with what's suggested in #7401 (comment) (except it would make the follow-up work very easy to identify).

I moved all pointer_in_range related code to a separate commit

src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md

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

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

src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h

Users can now write their own pointer predicates in terms of: - __CPROVER_is_fresh(ptr, size) - __CPROVER_obeys_contract(ptr, target) A rewriting pass lifts these user-defined pointer predicates into predicates that take pointers by reference and can make the predicates hold in assumption contexts using side-effects, and check the predicates in assertion contexts. Limitiations: User-defined predicates can be self-recursive but not mutually recursive, and their evaluation needs to be terminate, i.e. they can only describe bounded data structures.

remi-delmas-3000 · 2022-12-08T16:08:54Z

@feliperodri all requested changes were applied

feliperodri

LGTM

regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc

Adds support for pointer_in_range_dfcc in ensures and requires clauses and user-defined predicates. This is a temporary workaround to the fact that pointer_in_range is lowered by the front-end.

CBMC 5.72.1 point release for #7401

remi-delmas-3000 requested review from tautschnig, feliperodri, martin-cs, chris-ryder, peterschrammel and kroening as code owners November 29, 2022 21:40

remi-delmas-3000 added new feature aws Bugs or features of importance to AWS CBMC users aws-high Code Contracts Function and loop contracts labels Nov 29, 2022

remi-delmas-3000 force-pushed the contracts-lift-memory-predicates branch 4 times, most recently from 030f804 to bf18bd4 Compare November 29, 2022 21:50

remi-delmas-3000 added do not merge work in progress labels Nov 29, 2022

remi-delmas-3000 force-pushed the contracts-lift-memory-predicates branch 7 times, most recently from f84fdc9 to 1ace3d4 Compare November 30, 2022 08:07

remi-delmas-3000 self-assigned this Nov 30, 2022

remi-delmas-3000 force-pushed the contracts-lift-memory-predicates branch 2 times, most recently from 3815192 to 0d242c2 Compare December 2, 2022 21:56

This was referenced Dec 5, 2022

Allow let bindings in function contracts #7201

Closed

Predicate to describe overlapping pointers #7194

Closed

feliperodri changed the title ~~CONTRACTS: support bounded user defined memory-predicates~~ CONTRACTS: Support bounded user defined memory-predicates Dec 5, 2022

feliperodri requested changes Dec 7, 2022

View reviewed changes

remi-delmas-3000 force-pushed the contracts-lift-memory-predicates branch from 4929b83 to 2dda6a0 Compare December 7, 2022 19:03

remi-delmas-3000 requested review from NlightNFotis, thomasspriggs, esteffin and TGWDB as code owners December 7, 2022 19:03

remi-delmas-3000 force-pushed the contracts-lift-memory-predicates branch from 2dda6a0 to eda68f4 Compare December 7, 2022 20:56

remi-delmas-3000 force-pushed the contracts-lift-memory-predicates branch from eda68f4 to cf6fd73 Compare December 7, 2022 21:38

tautschnig reviewed Dec 7, 2022

View reviewed changes

remi-delmas-3000 force-pushed the contracts-lift-memory-predicates branch 8 times, most recently from 7d57611 to e0643b4 Compare December 8, 2022 15:15

tautschnig approved these changes Dec 8, 2022

View reviewed changes

src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h Outdated Show resolved Hide resolved

remi-delmas-3000 force-pushed the contracts-lift-memory-predicates branch from e0643b4 to 3618d8a Compare December 8, 2022 16:00

remi-delmas-3000 force-pushed the contracts-lift-memory-predicates branch from 3618d8a to df1551e Compare December 8, 2022 16:07

feliperodri approved these changes Dec 8, 2022

View reviewed changes

regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc Outdated Show resolved Hide resolved

remi-delmas-3000 force-pushed the contracts-lift-memory-predicates branch from df1551e to 2653d78 Compare December 8, 2022 16:17

CONTRACTS: support pointer_in_range_dfcc predicate

c144993

Adds support for pointer_in_range_dfcc in ensures and requires clauses and user-defined predicates. This is a temporary workaround to the fact that pointer_in_range is lowered by the front-end.

remi-delmas-3000 force-pushed the contracts-lift-memory-predicates branch from 2653d78 to c144993 Compare December 8, 2022 16:24

remi-delmas-3000 merged commit 8f8d169 into diffblue:develop Dec 8, 2022

TGWDB added a commit to TGWDB/cbmc that referenced this pull request Dec 8, 2022

CBMC point release for diffblue#7401

61c0372

NlightNFotis added a commit that referenced this pull request Dec 9, 2022

Merge pull request #7422 from TGWDB/20221208-cbmc-5.72.1

de504f5

CBMC 5.72.1 point release for #7401

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

CONTRACTS: Support bounded user defined memory-predicates #7401

CONTRACTS: Support bounded user defined memory-predicates #7401

remi-delmas-3000 commented Nov 29, 2022 •

edited

Loading

codecov bot commented Nov 30, 2022 •

edited

Loading

feliperodri left a comment

remi-delmas-3000 commented Dec 7, 2022 •

edited

Loading

tautschnig Dec 7, 2022

tautschnig Dec 7, 2022

remi-delmas-3000 Dec 8, 2022

remi-delmas-3000 commented Dec 8, 2022

feliperodri left a comment

CONTRACTS: Support bounded user defined memory-predicates #7401

CONTRACTS: Support bounded user defined memory-predicates #7401

Conversation

remi-delmas-3000 commented Nov 29, 2022 • edited Loading

codecov bot commented Nov 30, 2022 • edited Loading

Codecov Report

feliperodri left a comment

Choose a reason for hiding this comment

remi-delmas-3000 commented Dec 7, 2022 • edited Loading

tautschnig Dec 7, 2022

Choose a reason for hiding this comment

tautschnig Dec 7, 2022

Choose a reason for hiding this comment

remi-delmas-3000 Dec 8, 2022

Choose a reason for hiding this comment

remi-delmas-3000 commented Dec 8, 2022

feliperodri left a comment

Choose a reason for hiding this comment

remi-delmas-3000 commented Nov 29, 2022 •

edited

Loading

codecov bot commented Nov 30, 2022 •

edited

Loading

remi-delmas-3000 commented Dec 7, 2022 •

edited

Loading