Add support for function contracts in cprover_bindings. #1302

monal · 2022-06-23T23:06:23Z

Description of changes:

Implement CodeWithContract type in cprover_bindings to generate Ireps of type Code but with additional fields for handling function contracts. Adds the #spec_requires and #spec_ensures clauses to the Irep.

Call-outs:

Added a new type Spec with field clauses:Vec<Expr> to store a list of boolean expressions that would serve as pre (or post) conditions on the function. This allows us to handle required #[PartialEq] trait for the clauses.

Testing:

How is this change tested?
By running kani regression tests. As I haven't added the #[kani::requires] and #[kani::ensures] macros on the Rust side yet, it is not straightforward to add additional test cases right now.
Is this a refactor change?
No.

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 · 2022-06-23T23:11:46Z

Can you push this to a feature branch for now?

tedinski · 2022-06-23T23:54:17Z

Can you push this to a feature branch for now?

I thought this was a mergeable unit, or nearly so, so I requested the PR.

I could see merging this as-is, or possibly with a unit test for the irep generation added. We don't yet have many (any?) unit tests for cprover_bindings, so this might be the first, but we do actually want to get tests against this crate and have to start somewhere. :)

celinval · 2022-06-24T01:06:55Z

We already have unit tests in this crate. It would be great if we can add some food this code.

I would also suggest we tag the new functions with allow_dead with a link to the issue we're trying to solve.

tautschnig · 2022-06-30T18:36:34Z

I note that as of moments ago diffblue/cbmc#6799 is merged, which means that function contracts now live in symbols of their own.

monal · 2022-06-30T20:02:24Z

Thanks for linking the PR, @tautschnig! I will update my code accordingly.

monal · 2022-07-06T18:46:29Z

Summary of changes:

Add contract constructor to Symbol to create new symbols for function contracts.
Store the contract information (preconditions, postconditions, assigns, etc.) in the value field of the symbol (on the goto-program side). Hence, add Contract(Contract) to ExprValue.
During Irep generation, the contract's preconditions and postconditions are added to the type field under #spec_requires and #spec_ensures respectively.
Add LambdaExpression and Tuple to Expr. They are mathematical expressions (Expressions that do not exist immediately in C) but adding them to Expr seems to be the best option right now. We can create a separate MathematicalExpr in the future, if needed.
- The clauses in #spec_ensures(..) and #spec_requires(..) are wrapped in a lambda expression (using the as_lambda_expression method) to make sure that the contract symbol is self-contained and has a copy of the functions’ parameters. (Refer: CONTRACTS: store contracts in dedicated symbols diffblue/cbmc#6799).
- The bound variables in a lambda expression are stored as a Tuple.
Add MathematicalFunction to Type to store the type signature of lambda expressions.

cprover_bindings/src/goto_program/expr.rs

cprover_bindings/src/goto_program/symtab_transformer/transformer.rs

cprover_bindings/src/goto_program/typ.rs

cprover_bindings/src/irep/to_irep.rs

cprover_bindings/src/goto_program/expr.rs

zhassan-aws · 2022-07-06T19:23:11Z

cprover_bindings/src/goto_program/typ.rs

@@ -104,6 +146,12 @@ pub struct Parameter {
    base_name: Option<InternedString>,
 }

+/// Type for function contracts, loop contracts, etc.
+#[derive(Debug, Clone)]
+pub enum Contract {


Does this need to be an enum?

Made it an enum to support different types of contracts. Like LoopContract(...) in the future. Is there an alternative way to do this?

cprover_bindings/src/goto_program/typ.rs

…nction contracts

…mentation fixes

…or implementation fixes" This reverts commit f4afc15.

…pport function contracts" This reverts commit f7171f8.

This reverts commit ffd3ad2.

… to Type; Generate Ireps

…id misreading the type

…ration for contracts.

monal · 2022-07-08T20:40:28Z

Removed LambdaExpression and Tuple from Expr. Generating them at the Irep level now.
Added a module for Contract and introduced Spec to represent contract clauses.
Cleaned up whitespaces; added comments.

zhassan-aws

LGTM. Thanks!

danielsn · 2022-07-12T18:21:36Z

cprover_bindings/src/goto_program/contract.rs

@@ -0,0 +1,56 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+


File comment to explain what contracts are and link to documentation

Added comment + CBMC documentation link.

cprover_bindings/src/goto_program/contract.rs

danielsn · 2022-07-12T20:10:49Z

cprover_bindings/src/goto_program/symbol.rs

+        let name = name.into();
+        // Both base name and pretty name contain the name of the function that the contract is written for.
+        let base_name: InternedString = base_name.into();
+        let pretty_name = base_name;


Shouldn't this be the pretty name of the function? (We might have discussed this already)

On the CBMC side, the pretty_name is still the name of the function and not the name of the contract. Should I set it to the contract's name instead?

danielsn · 2022-07-12T20:40:28Z

cprover_bindings/src/irep/to_irep.rs

+        id: IrepId::Lambda,
+        sub: vec![
+            tuple_irep(binding_variables, mm)
+                // For binding expressions (quantifies, let, lambda), the type of the `tuple_exprt` is set to just its ID in CBMC.


Are there other cases where this is different?

The tuple_exprt has a constructor with a type argument. So, in CBMC, we can construct tuples with a specific type (and not just the ID). The binding_exprt that sits on top of a tuple_exprt always sets the type to be the ID.

…ng#1302) * Add type for "spec_ensures" and "spec_requires" clauses to support function contracts * Add transfomer code for code_with_contract; Fix comments; Minor implementation fixes * Revert "Add transfomer code for code_with_contract; Fix comments; Minor implementation fixes" This reverts commit f4afc15. * Revert "Add type for "spec_ensures" and "spec_requires" clauses to support function contracts" This reverts commit f7171f8. * Move function contract to Symbol * Revert "Move function contract to Symbol" This reverts commit ffd3ad2. * Add contract to SymbolValues * Update SymbolValues::Contract to have expressions * Add Contract type; Add Lambda and Tuple to Expr * WIP: Add LambdaExpression and Tuple to Expr; Add MathematicalFunction to Type; Generate Ireps * Update comment to explain pretty_name in contract symbol. * Change type to slice * Remove variables from FunctionContract type * Add type checking to the lambda_expression constructor * Change variables field in lambda expression to variables_tuple to avoid misreading the type * Remove type annotations * Remove LambdaExpression and Tuple * Remove FunctionContract type * Remove contracts * WIP:Move contracts to a separate module; Add spec to handle Irep generation for contracts. * WIP: Update spec to include location; Add comments * WIP: Add comments * WIP: Add location to spec * WIP: remove whitespace * WIP: Remove whitespace * Add file comment * Change Spec to always have Location * format Co-authored-by: Monal Narasimhamurthy <[email protected]>

monal requested a review from a team as a code owner June 23, 2022 23:06

monal marked this pull request as draft June 27, 2022 16:23

monal self-assigned this Jul 5, 2022

monal changed the title ~~Add CodeWithContract type to cprover_bindings for supporting function contracts.~~ Add support for function contracts in cprover_bindings. Jul 6, 2022

danielsn reviewed Jul 6, 2022

View reviewed changes

zhassan-aws reviewed Jul 6, 2022

View reviewed changes

Monal Narasimhamurthy added 18 commits July 8, 2022 12:20

Add type for "spec_ensures" and "spec_requires" clauses to support fu…

5cea135

…nction contracts

Add transfomer code for code_with_contract; Fix comments; Minor imple…

899b300

…mentation fixes

Revert "Add transfomer code for code_with_contract; Fix comments; Min…

f424956

…or implementation fixes" This reverts commit f4afc15.

Revert "Add type for "spec_ensures" and "spec_requires" clauses to su…

0f0212e

…pport function contracts" This reverts commit f7171f8.

Move function contract to Symbol

d3ebe3b

Revert "Move function contract to Symbol"

1eeba2b

This reverts commit ffd3ad2.

Add contract to SymbolValues

7a4a96d

Update SymbolValues::Contract to have expressions

6d04ada

Add Contract type; Add Lambda and Tuple to Expr

60eb6b8

WIP: Add LambdaExpression and Tuple to Expr; Add MathematicalFunction…

363ada5

… to Type; Generate Ireps

Update comment to explain pretty_name in contract symbol.

ecbf2cb

Change type to slice

e61041a

Remove variables from FunctionContract type

94cc0d5

Add type checking to the lambda_expression constructor

d00853a

Change variables field in lambda expression to variables_tuple to avo…

12f381a

…id misreading the type

Remove type annotations

d732dd4

Remove LambdaExpression and Tuple

aeb5550

Remove FunctionContract type

42e9f8e

Monal Narasimhamurthy added 7 commits July 8, 2022 12:20

Remove contracts

a705a20

WIP:Move contracts to a separate module; Add spec to handle Irep gene…

326c825

…ration for contracts.

WIP: Update spec to include location; Add comments

0ea305f

WIP: Add comments

ba1e7d3

WIP: Add location to spec

b5e956f

WIP: remove whitespace

2daa5d7

WIP: Remove whitespace

659df61

monal force-pushed the main branch from de2481a to 659df61 Compare July 8, 2022 19:20

monal marked this pull request as ready for review July 8, 2022 19:53

monal requested review from tautschnig, danielsn and zhassan-aws July 8, 2022 19:54

monal requested a review from a team July 8, 2022 20:51

zhassan-aws approved these changes Jul 8, 2022

View reviewed changes

monal changed the base branch from main to features/function-contracts July 12, 2022 18:30

monal force-pushed the main branch from dc4200a to 659df61 Compare July 12, 2022 20:30

danielsn reviewed Jul 12, 2022

View reviewed changes

Monal Narasimhamurthy and others added 4 commits July 12, 2022 21:31

Add file comment

8ba7653

Change Spec to always have Location

1759834

format

1e484d9

Merge branch 'features/function-contracts' into main

c25fbd5

monal merged commit 751ad18 into model-checking:features/function-contracts Jul 15, 2022

		@@ -0,0 +1,56 @@
		// Copyright Kani Contributors
		// SPDX-License-Identifier: Apache-2.0 OR MIT

Add support for function contracts in cprover_bindings. #1302

Add support for function contracts in cprover_bindings. #1302

Uh oh!

Conversation

monal commented Jun 23, 2022

Description of changes:

Call-outs:

Testing:

Checklist

Uh oh!

celinval commented Jun 23, 2022

Uh oh!

tedinski commented Jun 23, 2022

Uh oh!

celinval commented Jun 24, 2022

Uh oh!

tautschnig commented Jun 30, 2022

Uh oh!

monal commented Jun 30, 2022

Uh oh!

monal commented Jul 6, 2022

Uh oh!

Uh oh!

Uh oh!

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!

monal commented Jul 8, 2022

Uh oh!

zhassan-aws 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!

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!