Fix crash when using public fns reachability #2065
Conversation
Filter roots to only collect public functions. Also, make the collection function more robust.
| } else { | ||
| warn!( | ||
| tcx.sess.warn(format!( | ||
| "Ignoring global ASM in crate {}. Verification results may be impacted.", |
There was a problem hiding this comment.
Please use {gcx.short_crate_name()} instead, which will be necessary to make clippy happy with the upcoming rust toolchain update.
There was a problem hiding this comment.
oh, I didn't know you couldn't use expressions. We'll do
There was a problem hiding this comment.
It's not working for me. I get the following error:
error: invalid format string: expected `'}'`, found `'.'`
--> kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:314:55
|
314 | "Ignoring global ASM in crate {gcx.short_crate_name()}. Verification results may be impacted.",
| - ^ expected `}` in format string
| |
| because of this opening brace
|
= note: if you intended to print `{`, you can escape it using `{{`
There was a problem hiding this comment.
Sorry, I was wrong. Expressions cannot be used.
| }); | ||
|
|
||
| // Filter items from implementation blocks. | ||
| let impl_items = crate_items.impl_items().filter_map(|impl_item| { |
There was a problem hiding this comment.
Are impl_items not included in items above?
There was a problem hiding this comment.
That was my initial though, but I was wrong. For harnesses it didn't matter much, since we don't expect associated functions with them, but for other things they might be important.
FYI, for the little test I added in this PR, here are the breakdown of items and impl_items:
### ITEMS
def_id: DefId(0:1 ~ associated_fn[18c1]::{use#0}) -- kind: Use
def_id: DefId(0:2 ~ associated_fn[18c1]::std) -- kind: ExternCrate
def_id: DefId(0:3 ~ associated_fn[18c1]::Dummy) -- kind: Struct
def_id: DefId(0:5 ~ associated_fn[18c1]::{impl#0}) -- kind: Impl
### IMPL Items
def_id: DefId(0:6 ~ associated_fn[18c1]::{impl#0}::new) -- kind: AssocFn
Ps.: associated_fn is the name of the crate where they are defined. :)
| pub static DAYS_OF_WEEK: [char; 7] = ['s', 'm', 't', 'w', 't', 'f', 's']; | ||
|
|
||
| #[no_mangle] |
There was a problem hiding this comment.
Why not kani::proof (and --harness)?
There was a problem hiding this comment.
Because the bug this change fixes was on how we were collecting starting points for the public functions reachability mode. For the harnesses reachability mode, the predicate only passes for functions.
Conflicts:
kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
2 participants
Description of changes:
Filter roots to only collect public functions. Also, make the collection function more robust and to account for associated functions.
Resolved issues:
Resolves #2047
Related RFC:
#1588
Call-outs:
Testing:
How is this change tested? New tests + I manually tested the Chrono crates.
Is this a refactor change?
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.