Skip to content

Retrieve info for recursion tracker reliably - #3045

Merged
feliperodri merged 11 commits into
model-checking:mainfrom
feliperodri:fix-issue-3035
Mar 2, 2024
Merged

Retrieve info for recursion tracker reliably#3045
feliperodri merged 11 commits into
model-checking:mainfrom
feliperodri:fix-issue-3035

Conversation

@feliperodri

@feliperodrifeliperodri commented Feb 28, 2024

Copy link
Copy Markdown
Member

Fixes#3035.

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

@feliperodrifeliperodri self-assigned this Feb 28, 2024
@feliperodri
feliperodri requested a review from a team as a code ownerFebruary 28, 2024 00:13
@github-actionsgithub-actionsBot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Feb 28, 2024
celinval
celinval reviewed Feb 28, 2024
View reviewed changes

@celinvalcelinval left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you know why we use name instead of mangled_name

Comment threadkani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs Outdated
@feliperodri

feliperodri commented Feb 28, 2024•
edited
Loading

Copy link
Copy Markdown
MemberAuthor

Do you know why we use name instead of mangled_name

@celinval do we have available mangled name for StaticDef? The name and path are sufficient to get the correct variable.

error[E0599]: no method named `mangled_name` found for struct `StaticDef` in the current scope
--> kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:88:40
|
88 | instance_recursion_tracker.mangled_name(),
| ^^^^^^^^^^^^ method not found in `StaticDef`

@celinval

celinval commented Feb 28, 2024

Copy link
Copy Markdown
Contributor

Do you know why we use name instead of mangled_name

@celinval do we have available mangled name for StaticDef? The name and path are sufficient to get the correct variable.

error[E0599]: no method named `mangled_name` found for struct `StaticDef` in the current scope
--> kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:88:40
|
88 | instance_recursion_tracker.mangled_name(),
| ^^^^^^^^^^^^ method not found in `StaticDef`

You should invoke mangled_name in the instance, not in the StaticDef.

JustusAdam
JustusAdam suggested changes Feb 29, 2024
View reviewed changes

@JustusAdamJustusAdam left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for fixing this.

I would mention a "Closes" for the original issue that this addresses.

Comment threadkani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs Outdated
Comment threadkani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs Outdated
@feliperodri
Retrieve info for recursion tracker reliably
d5479c0
Fixesmodel-checking#3035
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
Use find instead of filter_map
5dd1253
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
Update the search for REENTRY and add documentation
569208a
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@celinval

celinval commented Feb 29, 2024

Copy link
Copy Markdown
Contributor

Hey @feliperodri, can you please make sure this code works if the contract is added to a generic function? I don't know if we already have a test for that.

@feliperodri
Add a comment to clarify not using mangled_name
e2f75fc
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
Add a test with generics and infinity recursion
96ddb5a
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
New line
4cabf21
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri

feliperodri commented Mar 1, 2024

Copy link
Copy Markdown
MemberAuthor

@celinval

You should invoke mangled_name in the instance, not in the StaticDef.

I added a comment to clarify why we can't use now mangled_name. I also reported the issue on CBMC (see diffblue/cbmc#8225).

can you please make sure this code works if the contract is added to a generic function? I don't know if we already have a test for that.

I added a test with generics and recursion. I didn't find any tests like that in our regression.

@feliperodri

feliperodri commented Mar 1, 2024

Copy link
Copy Markdown
MemberAuthor

I would mention a "Closes" for the original issue that this addresses.

@JustusAdam I added to the PR description.

JustusAdam
JustusAdam reviewed Mar 1, 2024
View reviewed changes

@JustusAdamJustusAdam left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good stuff.

Comment threadkani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs Outdated
Comment threadkani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs Outdated
Comment threadkani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
celinval
celinval reviewed Mar 1, 2024
View reviewed changes
Comment threadtests/expected/function-contract/generic_infinity_recursion.rs
celinval
celinval reviewed Mar 1, 2024
View reviewed changes

@celinvalcelinval left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good

@feliperodri
Move format outside of the loop
e3b2c35
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
Add header to test case
84674d3
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
feliperodri enabled auto-merge (squash) March 1, 2024 23:40
@feliperodri
feliperodri merged commit b4480ac into model-checking:mainMar 2, 2024
@feliperodri
feliperodri deleted the fix-issue-3035 branch March 4, 2024 16:43
@zhassan-awszhassan-aws mentioned this pull request Mar 13, 2024
Merged
zhassan-aws added a commit that referenced this pull request Mar 13, 2024
@zhassan-aws
Bump Kani version to 0.48.0 (#3075)
e004ecc
These are the original release notes for the reference:
## What's Changed
* Automatic cargo update to 2024-02-26 by @github-actions in
#3043
* Upgrade rust toolchain to 2024-02-17 by @celinval in
#3040
* Upgrade `windows-targets` crate to version 0.52.4 by @adpaco-aws in
#3049
* Fix `codegen_atomic_binop` for `atomic_ptr` by @qinheping in
#3047
* Upgrade Rust toolchain to `nightly-2024-02-25` by @adpaco-aws in
#3048
* Update s2n-quic submodule by @zhassan-aws in
#3050
* Update s2n-quic submodule weekly through dependabot by @zhassan-aws in
#3053
* Retrieve info for recursion tracker reliably by @feliperodri in
#3045
* Automatic cargo update to 2024-03-04 by @github-actions in
#3055
* Upgrade Rust toolchain to `nightly-2024-03-01` by @adpaco-aws in
#3052
* Add `--use-local-toolchain` to Kani setup by @jaisnan in
#3056
* Replace internal reverse_postorder by a stable one by @celinval in
#3064
* Add option to override `--crate-name` from `kani` by @adpaco-aws in
#3054
* cargo update and fix macos CI by @zhassan-aws in
#3067
* Bump tests/perf/s2n-quic from `d103836` to `1a7faa8` by @dependabot in
#3066
* Upgrade toolchain to 2024-03-11 by @zhassan-aws in
#3071
* Emit `dead` goto-instructions on MIR StatementDead by @karkhaz in
#3063
**Full Changelog**:
kani-0.47.0...kani-0.48.0
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@celinvalcelinvalcelinval approved these changes
+1 more reviewer
@JustusAdamJustusAdamJustusAdam approved these changes
Reviewers whose approvals may not affect merge requirements

Assignees

@feliperodrifeliperodri

Labels

Z-EndToEndBenchCITag a PR to run benchmark CI

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Regression in contract verification from 0.45.0 to 0.46.0

3 participants

@feliperodri@celinval@JustusAdam