Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Retrieve info for recursion tracker reliably #3045

Merged
merged 11 commits into from
Mar 2, 2024
Merged

Retrieve info for recursion tracker reliably #3045

merged 11 commits into from
Mar 2, 2024

Conversation

feliperodri
Copy link
Contributor

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.

@feliperodri feliperodri self-assigned this Feb 28, 2024
@feliperodri feliperodri requested a review from a team as a code owner February 28, 2024 00:13
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Feb 28, 2024
celinval
celinval reviewed Feb 28, 2024
View reviewed changes
Copy link
Contributor

@celinval celinval left a comment

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

kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs Outdated Show resolved Hide resolved
@feliperodri
Copy link
Contributor Author

feliperodri commented Feb 28, 2024 •
edited
Loading

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
Copy link
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
Copy link
Contributor

@JustusAdam JustusAdam left a comment

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.

kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs Outdated Show resolved Hide resolved
@feliperodri
Retrieve info for recursion tracker reliably
d5479c0 
Fixes model-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
Copy link
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
Copy link
Contributor Author

@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
Copy link
Contributor Author

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
Copy link
Contributor

@JustusAdam JustusAdam left a comment

Choose a reason for hiding this comment

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

Good stuff.

kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs Show resolved Hide resolved
celinval
celinval reviewed Mar 1, 2024
View reviewed changes
Copy link
Contributor

@celinval celinval left a comment

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:main Mar 2, 2024
20 checks passed
@feliperodri feliperodri deleted the fix-issue-3035 branch March 4, 2024 16:43
@zhassan-aws zhassan-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 free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@JustusAdam JustusAdam JustusAdam approved these changes

@celinval celinval celinval approved these changes

Assignees

@feliperodri feliperodri

Labels
Z-BenchCI Tag 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