Support for requires and ensures clauses #2555

JustusAdam · 2023-06-22T20:21:51Z

Description of changes:

Adds basic support for requires and ensures function contract macros.

Testing:

Some simple test cases have been added

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

celinval · 2023-06-22T21:51:59Z

Can you please make sure the PR only include changes relevant to contract?

JustusAdam · 2023-06-22T23:12:57Z

Yeah that was because the target branch was out of date.

celinval

That's great progress! As talked offline, the focus at this point is the CBMC integration. Here is a few notes:

I think the bindings code look quite ready. :)
Is there any reason why there is no tests for requires?
For future PRs, I think it would be better if we make the compiler code more modular. We should also figure out what the user flow will be for contracts, so we can design the communication between each component.

cprover_bindings/src/goto_program/expr.rs

cprover_bindings/src/goto_program/symbol.rs

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

library/kani_macros/src/lib.rs

tests/kani/FunctionContract/arbitrary_ensures_fail.rs

JustusAdam · 2023-06-28T18:27:43Z

Is there any reason why there is no tests for requires?

For future PRs, I think it would be better if we make the compiler code more modular. We should also figure out what the user flow will be for contracts, so we can design the communication between each component.

So they are actually related. I didn't add a test case for requires because I didn't implement substitution. But I realize that I can also add a test where the verification would fail if the precondition is violated (e.g. the assume did not take hold) so I'll do that.

And wrt. flow we've discussed that in person already but for the benefit of the log: The flow is in the design phase and will be added after history variables and quantifiers.

JustusAdam · 2023-06-28T23:44:31Z

I need to mention here that this does a small change to the testing infrastructure as well. In particular a directory can now contain multiple "expected" tests. The setup is analogous to regular .rs tests but each also has an associated .expected file. The way that is implemented is that when looking for test in a directory and we find a candidate file my_file.rs then we first look for a file called my_file.expected as the expected file. If such a file exists then it will be used as the expected file, otherwise we look for a file with the name expected.

So this change is fully backwards compatible but also cuts down on potential directory spam for the "expected" tests and makes the behavior more intuitive wrt the documentation where it mentions .expected files.

tests/kani/FunctionContract/simple_ensures_pass.rs

tests/kani/FunctionContract/simple_ensures_fail.rs

tests/kani/FunctionContract/arbitrary_ensures_fail.rs

tests/kani/FunctionContract/arbitrary_ensures_pass.rs

library/kani_macros/src/lib.rs

kani-compiler/src/kani_middle/attributes.rs

cprover_bindings/src/irep/irep_id.rs

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

celinval

For the feature branch, I think this is in a fairly good shape.

For the comments that reflect code quality / organization, for this PR, I think it's OK if you create an issue to capture the work and add a TODO statement with a description and a link to the new issue.

kani-compiler/src/kani_middle/attributes.rs

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

kani-compiler/src/kani_middle/attributes.rs

kani-compiler/src/kani_middle/reachability.rs

kani-driver/src/args/common.rs

kani-driver/src/call_goto_instrument.rs

kani_metadata/src/harness.rs

feliperodri

LGTM.

feliperodri · 2023-07-11T18:35:52Z

@celinval any idea why Cargo Audit is failing here?

adpaco-aws · 2023-07-11T22:32:31Z

I think you just need to include the commit from #2581 in the source branch.

Adds pre- and postconditions

Co-authored-by: Celina G. Val <celinval@amazon.com>

Added `requires` test case Made tests `expected` tests Changes `requires_ensures` macro to function

Co-authored-by: Celina G. Val <celinval@amazon.com>

JustusAdam · 2023-07-14T21:51:19Z

I did another rebase to try and address the audit issue. Tbh I should have merged instead but oh well. I am going to squash the commits before merging anyway at least that's the plan.

JustusAdam · 2023-07-14T21:52:08Z

I'll bump the base branch next so the PR doesn't include the unrelated commits

JustusAdam · 2023-07-20T00:08:18Z

I'm having trouble with this regression stuff now. The numbering for checks seems to be platform dependent and makes the test fail as a result? When I run on my machine the expected test suite completes fine but on the ubuntu CI it doesn't. What's the best practice here to make the expected output stable? Maybe @feliperodri can help?

zhassan-aws · 2023-07-20T02:34:44Z

We don't include the check indices in the expected files to avoid those issues. Even if they're consistent across platforms, they may change with changes to the compiler or new CBMC versions. Note that compiletest checks for a substring and not an exact match for the line.

JustusAdam · 2023-07-20T23:57:47Z

Does it require ordering? Because one thing I now worry about is that the expected success/failure may not be the one with the description I am looking for. E.g. if i expected one property to succeed and another to fail what guarantees me that "Status: FAILURE" actually belongs to my "Description: fail this" test and not my "Description: succeed this"?

zhassan-aws · 2023-07-21T00:03:20Z

Does it require ordering?

Generally, no: the compiletest tool checks if each line in the expected file occurred in the output.

the expected success/failure may not be the one with the description I am looking for

If a line in the expected file ends in backslash, the following line must occur on the consecutive line in the output. This is how we achieve ordering (partially). See https://github.com/model-checking/kani/blob/main/tests/expected/assert-eq/expected for an example.

Changed tesdt runner to not leave trailing checks and to ignore whitespace around expected lines

JustusAdam · 2023-07-23T02:21:22Z

I've fixed up the test cases but unfortunately benchcomp is still failing. Is that a problem?

qinheping · 2023-07-23T04:11:37Z

There are some interesting founds in the Benchcomp CI.

The running time of format/fmt_i8 in the old variant is ~2.62 seconds. However, it the past Benchcomp run, for example https://github.com/model-checking/kani/actions/runs/5558854620/job/15059090659#step:13:71, the running time of format/fmt_i8 is ~1000seconds.
Also, the number_program_steps of the old variant of format/fmt_i8 and format_fmt/8 are much smaller than the number_program_steps of them in the table https://github.com/model-checking/kani/actions/runs/5627831808

The Benchcomp is comparing this PR with the old version after #2553 merged. So the performance regression accumulats from #2553 to now.

qinheping · 2023-07-23T04:41:02Z

After comparing the Benchomp runs of these two commits https://github.com/model-checking/kani/actions/runs/5405839079/job/14637506427 and https://github.com/model-checking/kani/actions/runs/5459160729/job/14779199972.
I confirmed that the regression of all 6 regressed benchmarks
btreeset/insert_any/main btreeset/insert_same/main format/fmt_i8 s2n-quic/quic/s2n-quic-core/sync::cursor::tests::oracle_test
s2n-quic/quic/s2n-quic-core/sync::spsc::tests::alloc_test
s2n-quic/tools/xdp/s2n-quic-xdp/task::completion_to_tx::assign::tests::assignment_test
is due to the huge toolchain upgrade 7139063.
I don't think the failed Benchcomp run blocks this PR. But I think it is worth to revisit the toolchain upgrade to see if it is possible to recover the performance of these benchmarks.

Update: the regression of fmt_i8 was noticed and tracked in this issue #2576.

JustusAdam changed the base branch from main to features/contracts June 22, 2023 20:26

JustusAdam changed the base branch from features/contracts to main June 22, 2023 23:12

JustusAdam changed the base branch from main to features/contracts June 22, 2023 23:12

celinval reviewed Jun 24, 2023

View reviewed changes

JustusAdam force-pushed the simple-requires-ensures branch from 91ee87b to 1ebba9e Compare June 28, 2023 19:40

JustusAdam marked this pull request as ready for review June 29, 2023 01:48

JustusAdam requested a review from a team as a code owner June 29, 2023 01:48

JustusAdam requested a review from feliperodri June 29, 2023 01:48

JustusAdam self-assigned this Jun 29, 2023

JustusAdam added this to the Function Contracts MVP milestone Jun 29, 2023

feliperodri requested changes Jul 6, 2023

View reviewed changes

feliperodri changed the title ~~Simple requires ensures~~ Support for requires and ensures clauses Jul 6, 2023

celinval reviewed Jul 6, 2023

View reviewed changes

feliperodri approved these changes Jul 10, 2023

View reviewed changes

feliperodri requested a review from celinval July 11, 2023 18:35

JustusAdam and others added 9 commits July 14, 2023 14:48

Basic implementation for function contracts

201302f

Adds pre- and postconditions

Documentation

b400f1c

Formatting for tests

c69bf06

Hopefully fixing clippy suggestions

46069ef

Update library/kani_macros/src/lib.rs

95fe43c

Co-authored-by: Celina G. Val <celinval@amazon.com>

Apply suggestions from code review

7ef5a58

Co-authored-by: Celina G. Val <celinval@amazon.com>

Addressing comments

c02f171

Added `requires` test case Made tests `expected` tests Changes `requires_ensures` macro to function

Fixing regression test setup

bed5def

Fixing test cases and allowing multiple .expected files

38ca8cf

JustusAdam and others added 5 commits July 14, 2023 14:48

Update kani-driver/src/call_goto_instrument.rs

787e544

Co-authored-by: Celina G. Val <celinval@amazon.com>

Alloow only one contract at a time

e0f3e58

Addressing leftover comments

8bc7532

Removing last vestiges of assigns

11d01fa

Refactoring reachabiity

26b1b97

JustusAdam force-pushed the simple-requires-ensures branch from bb0a38b to 26b1b97 Compare July 14, 2023 21:48

JustusAdam added 4 commits July 14, 2023 14:56

Fixed small import issue

8bfaae2

Fixing multi-contract and adding a test case

8b16da6

Must allow unused variables I guess

954ab56

Apparently some of the test messages had changed

3116074

JustusAdam added 4 commits July 21, 2023 13:40

Corrected expected files

9b796fa

Changed tesdt runner to not leave trailing checks and to ignore whitespace around expected lines

Actually there is a windows method

21bd441

Clippy doesn't like me

48f617b

fmt

7122fd3

JustusAdam marked this pull request as draft July 23, 2023 02:23

JustusAdam changed the base branch from features/contracts to main July 23, 2023 02:24

JustusAdam changed the base branch from main to features/contracts July 23, 2023 02:24

JustusAdam marked this pull request as ready for review July 23, 2023 02:24

feliperodri merged commit 0d632c8 into model-checking:features/contracts Jul 24, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support for requires and ensures clauses #2555

Support for requires and ensures clauses #2555

JustusAdam commented Jun 22, 2023 •

edited

Loading

celinval commented Jun 22, 2023

JustusAdam commented Jun 22, 2023

celinval left a comment

JustusAdam commented Jun 28, 2023

JustusAdam commented Jun 28, 2023 •

edited

Loading

celinval left a comment •

edited

Loading

feliperodri left a comment

feliperodri commented Jul 11, 2023

adpaco-aws commented Jul 11, 2023

JustusAdam commented Jul 14, 2023

JustusAdam commented Jul 14, 2023

JustusAdam commented Jul 20, 2023 •

edited

Loading

zhassan-aws commented Jul 20, 2023

JustusAdam commented Jul 20, 2023

zhassan-aws commented Jul 21, 2023

JustusAdam commented Jul 23, 2023

qinheping commented Jul 23, 2023 •

edited

Loading

qinheping commented Jul 23, 2023 •

edited

Loading

Support for requires and ensures clauses #2555

Support for requires and ensures clauses #2555

Conversation

JustusAdam commented Jun 22, 2023 • edited Loading

Description of changes:

Testing:

Checklist

celinval commented Jun 22, 2023

JustusAdam commented Jun 22, 2023

celinval left a comment

Choose a reason for hiding this comment

JustusAdam commented Jun 28, 2023

JustusAdam commented Jun 28, 2023 • edited Loading

celinval left a comment • edited Loading

Choose a reason for hiding this comment

feliperodri left a comment

Choose a reason for hiding this comment

feliperodri commented Jul 11, 2023

adpaco-aws commented Jul 11, 2023

JustusAdam commented Jul 14, 2023

JustusAdam commented Jul 14, 2023

JustusAdam commented Jul 20, 2023 • edited Loading

zhassan-aws commented Jul 20, 2023

JustusAdam commented Jul 20, 2023

zhassan-aws commented Jul 21, 2023

JustusAdam commented Jul 23, 2023

qinheping commented Jul 23, 2023 • edited Loading

qinheping commented Jul 23, 2023 • edited Loading

JustusAdam commented Jun 22, 2023 •

edited

Loading

JustusAdam commented Jun 28, 2023 •

edited

Loading

celinval left a comment •

edited

Loading

JustusAdam commented Jul 20, 2023 •

edited

Loading

qinheping commented Jul 23, 2023 •

edited

Loading

qinheping commented Jul 23, 2023 •

edited

Loading