Crash in Kani compiler on chrono crate #3904
Comments
zhassan-aws
added
[C] Bug
zhassan-aws
changed the title
|
It seems the problem is that #[derive(PartialEq)]
enum Numeric {
A,
B,
C
}
#[derive(PartialEq)]
enum Item<'a> {
Numeric(Numeric),
Literal(&'a str)
}
#[kani::proof]
pub fn harness() {
static FOO: &[Item<'static>] = &[Item::Numeric(Numeric::A), Item::Literal("/")];
assert!(FOO[0] == num(Numeric::A));
}Even in the absence of a smaller reproducer: the only way I found that may tell us about anonymous constants is this: --- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -219,20 +219,27 @@ fn visit_static(&mut self, def: StaticDef) -> Vec<CollectedItem> {
let _guard = debug_span!("visit_static", ?def).entered();
let mut next_items = vec![];
- // Collect drop function.
- let static_ty = def.ty();
- let instance = Instance::resolve_drop_in_place(static_ty);
- next_items
- .push(CollectedItem { item: instance.into(), reason: CollectionReason::StaticDrop });
-
- // Collect initialization.
- let alloc = def.eval_initializer().unwrap();
- for (_, prov) in alloc.provenance.ptrs {
- next_items.extend(
- collect_alloc_items(prov.0)
- .into_iter()
- .map(|item| CollectedItem { item, reason: CollectionReason::Static }),
- );
+ // Collect drop function, unless it's an anonymous static.
+ let int_def_id = rustc_internal::internal(self.tcx, def.def_id());
+ let anonymous = match self.tcx.def_kind(int_def_id) {
+ rustc_hir::def::DefKind::Static { nested, .. } => nested,
+ _ => false
+ };
+ if !anonymous {
+ let static_ty = def.ty();
+ let instance = Instance::resolve_drop_in_place(static_ty);
+ next_items
+ .push(CollectedItem { item: instance.into(), reason: CollectionReason::StaticDrop });
+
+ // Collect initialization.
+ let alloc = def.eval_initializer().unwrap();
+ for (_, prov) in alloc.provenance.ptrs {
+ next_items.extend(
+ collect_alloc_items(prov.0)
+ .into_iter()
+ .map(|item| CollectedItem { item, reason: CollectionReason::Static }),
+ );
+ }
}
next_itemsBut then this leads to problems in |
|
Thanks for looking into this @tautschnig!
What kind of problems? |
|
This code: static mut FOO: &mut u32 = &mut 42;
fn main() {
unsafe {
*FOO = 43;
}
}produces an anonymous static: Consider this slightly more complicated example, inspired by rust-lang/rust#79738 (comment), which produces See also rust-lang/rust#61345, rust-lang/rust#67000, and rust-lang/rust#116564 for inspiration/context . I extended @tautschnig's code in https://github.com/carolynzech/kani/tree/issue-3904. The two examples in this comment verify successfully if I make their I haven't made a PR for this branch yet because I want to convince myself a bit more that this is actually the right logic. Thoughts appreciated :) @zhassan-aws @tautschnig |
|
Awesome, thanks @carolynzech! I looked at your branch, and I don't see anything that looks wrong. I'm a bit confused about the part than handles interior mutability though, and why this is needed in the first place. |
+1 to everything that Zyad said: Thank you for coming up with the full fix, please include the tests that you came up with in that PR. And, yes, I am also wondering why that "except for this line" difference is needed, can you please expand the comment in the code for the version to be PR'ed? |
|
@tautschnig @zhassan-aws You're right--I was trying to make the distinction that the allocations are mutable, but that wasn't the right way to do it. I've made some changes to the approach, see #3953 |
rust-lang/rust#121644 added support for anonymous nested allocations to statics. This PR adds support for such statics to Kani. The idea is to treat an anonymous `GlobalAlloc::Static` the same as we would treat a `GlobalAlloc::Memory`, since an anonymous static is a nested memory allocation. To frame this change in terms of the tests: `pointer_to_const_alloc.rs` contains a test for the `GlobalAlloc::Memory` case, which we could already handle prior to this PR. The MIR looks like: ``` alloc3 (size: 4, align: 4) { 2a 00 00 00 │ *... } alloc1 (static: FOO, size: 16, align: 8) { ╾─────alloc3<imm>─────╼ 01 00 00 00 00 00 00 00 │ ╾──────╼........ } ``` meaning that `FOO` contains a pointer to the *immutable* allocation alloc3 (note the `alloc3<imm>`, imm standing for "immutable"). `anon_static.rs` tests the code introduced in this PR. The MIR from `example_1` looks almost identical: ``` alloc2 (static: FOO::{constant#0}, size: 4, align: 4) { 2a 00 00 00 │ *... } alloc1 (static: FOO, size: 16, align: 8) { ╾───────alloc2────────╼ 01 00 00 00 00 00 00 00 │ ╾──────╼........ } ``` Note, however, that `alloc2` is mutable, and is thus an anonymous nested static rather than a constant allocation. But we can just call `codegen_const_allocation` anyway, since it ends up checking if the allocation is indeed constant before declaring the global variable in the symbol table: https://github.com/model-checking/kani/blob/319040b8cd2cb72ec0603653fad7a8d934857d57/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs#L556 Resolves #3904 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Steps to reproduce:
cargo new foocd foocargo add chrono@0.4.39src/main.rs:using the following command line invocation:
with Kani version: f64f53e
I expected to see this happen: Verification successful
Instead, this happened: Kani crashed
The text was updated successfully, but these errors were encountered: