Adds is_fresh predicate for function contracts #6148

feliperodri · 2021-05-25T15:23:33Z

Signed-off-by: Felipe R. Monteiro [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.
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 · 2021-05-26T10:23:56Z

( At some point before the "don't review" tag gets removed, please can this PR say what the semantics of is_fresh is. )

codecov · 2021-05-28T20:44:08Z

Codecov Report

Merging #6148 (dd27ec0) into develop (b5873c9) will increase coverage by 0.21%.
The diff coverage is 84.90%.

@@             Coverage Diff             @@
##           develop    #6148      +/-   ##
===========================================
+ Coverage    75.04%   75.26%   +0.21%     
===========================================
  Files         1450     1450              
  Lines       158276   158471     +195     
===========================================
+ Hits        118784   119277     +493     
+ Misses       39492    39194     -298

Impacted Files	Coverage Δ
src/ansi-c/c_typecheck_expr.cpp	`74.83% <55.55%> (+14.56%)`	⬆️
src/goto-instrument/code_contracts.cpp	`86.33% <85.64%> (+0.89%)`	⬆️
src/goto-instrument/code_contracts.h	`95.83% <100.00%> (+2.08%)`	⬆️
src/analyses/local_may_alias.cpp	`65.75% <0.00%> (+0.45%)`	⬆️
src/util/bitvector_expr.h	`98.26% <0.00%> (+1.29%)`	⬆️
src/ansi-c/c_expr.h	`100.00% <0.00%> (+5.12%)`	⬆️
src/ansi-c/c_typecheck_base.h	`100.00% <0.00%> (+13.33%)`	⬆️

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 9539a51...dd27ec0. Read the comment docs.

SaswatPadhi

I took a first pass over the regression tests. I left some small comments below, but here are some major ones:

The regression tests all look kind of similar. Some other corner cases that we should test (feel free to add more):
- requires(is_fresh()) should pass on whole structs and individual members
- ensures(is_fresh()) should pass on functions that perform allocation directly and return a new object
- ensures(is_fresh()) should pass on functions that call another function that does the allocation and then return the object (this is to check that we propagate freshness correctly across contracts)

I will review the implementation logic in the next pass, and finally the code style in a later pass.

One high-level issue that I am confused about:

// When enforced, this contract should pass
bool sub_ptr_values(int *x, int *y)
  __CPROVER_requires(
    __CPROVER_is_fresh(x, sizeof(int)) && __CPROVER_is_fresh(y, sizeof(int))
  )
  __CPROVER_ensures(
    __CPROVER_return_value == *x - *y
  )
{
  return *x - *y;
}

// A function that uses `sub_ptr_values`
void foo()
{
  int *n = malloc(sizeof(int));

  // When call is replaced by contract, this will cause an assertion violation?
  int diff = sub_ptr_values(n, n);
}

The question here is, how should the contract sub_ptr_values be written so as to allow possibly-aliased arguments? I see "is_fresh" as enforcing/checking fresh non-aliasing allocations.

Okay I guess one could make the aliasing explicit:

  __CPROVER_requires(
    __CPROVER_is_fresh(x, sizeof(int)) &&
    (y == x || __CPROVER_is_fresh(y, sizeof(int)))
  )

Can we add this conditional "is_fresh" case as a regression test?

src/ansi-c/library/cprover.h

regression/contracts/quantifiers-loop-02/test.desc

regression/contracts/is_unique_01_replace/main.c

src/ansi-c/cprover_builtin_headers.h

regression/contracts/test_scalar_memory_replace/test.desc

SaswatPadhi · 2021-05-28T22:52:57Z

regression/contracts/test_scalar_memory_replace/main.c

+  int o = foo(n);
+  assert(o >= 10 && o == *n + 5);
+  return 0;
+}


Missing newline at the end. Please also check other files.

Sorry, but it looks like this file is still missing a newline at the end?
I did refresh the PR page and I am looking at the current changes.

regression/contracts/test_scalar_memory_replace/main.c

regression/contracts/test_multifile_replace/main.c

feliperodri · 2021-06-09T07:21:35Z

@SaswatPadhi I addressed all your comments and added more regression tests. Could you take another look at it?

SaswatPadhi

Thanks for improving the regression tests! They were quite helpful for me to understand end-to-end behavior before reviewing the core logic.

I left a few more minor comments below. The contract implementation looks sounds to me. The only remaining major question I have is regarding data structures like lists. I am not sure how one would write a contract using is_fresh for a function that takes a linked list and say counts its length. I can see how that could be written for lists that have a constant length, but it's not obvious how to write it for bounded lists, not unbounded, but that do not have a constant length.

If inductive structures like lists are beyond the scope of this first version of code contracts, let me know.

src/ansi-c/library/contracts.c

regression/contracts/test_struct_replace/test.desc

regression/contracts/test_struct_member_enforce/test.desc

regression/contracts/test_struct_enforce/test.desc

SaswatPadhi · 2021-06-09T18:48:47Z

regression/contracts/test_scalar_memory_replace/main.c

+  int o = foo(n);
+  assert(o >= 10 && o == *n + 5);
+  return 0;
+}


Sorry, but it looks like this file is still missing a newline at the end?
I did refresh the PR page and I am looking at the current changes.

SaswatPadhi · 2021-06-09T21:11:41Z

src/ansi-c/library/contracts.c

+
+//
+// Below are templates of the functions that
+// will be instantiated for each contract function.


Are these templates used?

I might be wrong, but it looks like we generate concrete instances of these templates during instrumentation, but from scratch.

We're not using these templates at the moment, but generating concrete instances during instrumentation as you observed. I removed this for now, so we can make use of these templates on a separate PR (as discussed offline).

src/goto-instrument/code_contracts.cpp

feliperodri · 2021-06-09T21:57:16Z

@SaswatPadhi

I left a few more minor comments below. The contract implementation looks sounds to me. The only remaining major question I have is regarding data structures like lists. I am not sure how one would write a contract using is_fresh for a function that takes a linked list and say counts its length. I can see how that could be written for lists that have a constant length, but it's not obvious how to write it for bounded lists, not unbounded, but that do not have a constant length.

For inductive data structures, one needs to invoke __CPROVER_is_fresh for every node, which is not feasible for unbounded (and bounded perhaps) approaches. We could add more predicates for specific cases, e.g., __CPROVER_list_is_fresh(list) would propagate the property to every node of the list. This is difficult, because we would need to make assumption on the shape of the list.

If inductive structures like lists are beyond the scope of this first version of code contracts, let me know.

This is out of the scope for this PR; however, we should talk more about it offline to discuss ideas on how we can address this in the future.

Signed-off-by: Felipe R. Monteiro <[email protected]>

SaswatPadhi

Thanks! LGTM 😃

There are a bunch of TODOs but let's merge this first and then tackle the refactoring, documentation etc. in future PRs.

chrisr-diffblue

Nothing blocking from my point of view - though like @martin-cs it would be nice to see a clear description of the intended semantics - plus a couple of small queries/comments.

chrisr-diffblue · 2021-06-10T09:15:28Z

src/goto-instrument/code_contracts.cpp

+
+//
+//
+// Code largely copied from model_argc_argv.cpp


Is there any way to factor out the common code, rather than copying?

chrisr-diffblue · 2021-06-10T09:17:19Z

src/goto-instrument/code_contracts.cpp

+  : is_fresh_baset(_parent, _log, _fun_id)
+{
+  std::stringstream ssreq, ssensure, ssmemmap;
+  ssreq /* << CPROVER_PREFIX */ << fun_id << "_call_requires_is_fresh";


Are these commented out CPROVER_PREFIX's deliberate? is_fresh_enforcet::is_fresh_enforcet seems to insert the, but they are commented out here - just wondering which is correct, or whether both are?

feliperodri added do not review Code Contracts Function and loop contracts labels May 25, 2021

feliperodri self-assigned this May 25, 2021

feliperodri added the aws Bugs or features of importance to AWS CBMC users label May 25, 2021

feliperodri force-pushed the is-fresh branch 3 times, most recently from 93cb2c7 to 0c296af Compare May 28, 2021 19:27

SaswatPadhi reviewed May 28, 2021

View reviewed changes

feliperodri force-pushed the is-fresh branch from 0c296af to f8ac3b0 Compare June 9, 2021 07:20

feliperodri requested a review from SaswatPadhi June 9, 2021 07:21

feliperodri force-pushed the is-fresh branch from f8ac3b0 to dd47aa6 Compare June 9, 2021 07:25

SaswatPadhi suggested changes Jun 9, 2021

View reviewed changes

feliperodri force-pushed the is-fresh branch from dd47aa6 to 9002e76 Compare June 9, 2021 22:33

feliperodri removed the do not review label Jun 9, 2021

feliperodri requested a review from SaswatPadhi June 9, 2021 22:33

feliperodri marked this pull request as ready for review June 9, 2021 22:33

feliperodri requested review from chrisr-diffblue, kroening and tautschnig as code owners June 9, 2021 22:33

Adds is_fresh predicate for function contracts

dd27ec0

Signed-off-by: Felipe R. Monteiro <[email protected]>

feliperodri force-pushed the is-fresh branch from 9002e76 to dd27ec0 Compare June 9, 2021 22:38

SaswatPadhi approved these changes Jun 9, 2021

View reviewed changes

chrisr-diffblue approved these changes Jun 10, 2021

View reviewed changes

feliperodri merged commit 58a15d6 into diffblue:develop Jun 10, 2021

feliperodri deleted the is-fresh branch June 10, 2021 13:40

Adds is_fresh predicate for function contracts #6148

Adds is_fresh predicate for function contracts #6148

Uh oh!

Conversation

feliperodri commented May 25, 2021

Uh oh!

martin-cs commented May 26, 2021

Uh oh!

codecov bot commented May 28, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

SaswatPadhi 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!

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!

feliperodri commented Jun 9, 2021

Uh oh!

SaswatPadhi 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!

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!

feliperodri commented Jun 9, 2021

Uh oh!

SaswatPadhi left a comment

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue 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!

Uh oh!

codecov bot commented May 28, 2021 •

edited

Loading

SaswatPadhi left a comment •

edited

Loading

SaswatPadhi left a comment •

edited

Loading