Skip to content

Commit

Permalink
Fix ICE due to mishandling of Aggregate rvalue for raw pointers to `s…
Browse files Browse the repository at this point in the history
…tr` (model-checking#3448)

We were missing a match arm for the case where a raw pointer to a string
slice was created from a thin pointer and the string size.

Resolves model-checking#3312 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
celinval authored Aug 23, 2024
1 parent 56e2a2f commit 7a28667
Show file tree
Hide file tree
Showing 5 changed files with 56 additions and 0 deletions.
8 changes: 8 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -694,6 +694,14 @@ impl<'tcx> GotocCtx<'tcx> {
let meta = self.codegen_operand_stable(&operands[1]);
slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
}
TyKind::RigidTy(RigidTy::Str) => {
let pointee_goto_typ = Type::unsigned_int(8);
// cast data to pointer with specified type
let data_cast =
data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) });
let meta = self.codegen_operand_stable(&operands[1]);
slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
}
TyKind::RigidTy(RigidTy::Adt(..)) => {
let pointee_goto_typ = self.codegen_ty_stable(pointee_ty);
let data_cast =
Expand Down
20 changes: 20 additions & 0 deletions tests/kani/Str/raw_ptr.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! Checks that Kani can handle creating pointers for slices from raw parts.
//! This used to trigger an ICE reported in <https://github.com/model-checking/kani/issues/3312>.
#![feature(ptr_metadata)]

#[derive(kani::Arbitrary)]
struct AscII {
#[safety_constraint(*inner < 128)]
inner: u8,
}

#[kani::proof]
fn check_from_raw() {
let ascii: [AscII; 5] = kani::any();
let slice_ptr: *const [AscII] = &ascii;
let (ptr, metadata) = slice_ptr.to_raw_parts();
let str_ptr: *const str = std::ptr::from_raw_parts(ptr, metadata);
assert!(unsafe { (&*str_ptr).is_ascii() });
}
11 changes: 11 additions & 0 deletions tests/perf/smol_str/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT

[package]
name = "check_smol_str"
version = "0.1.0"
edition = "2021"

[dependencies]
# Make dependency fixed to ensure the test stays the same.
smol_str = "=0.2.2"
4 changes: 4 additions & 0 deletions tests/perf/smol_str/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Checking harness check_new...
VERIFICATION:- SUCCESSFUL

Complete - 1 successfully verified harnesses, 0 failures, 1 total.
13 changes: 13 additions & 0 deletions tests/perf/smol_str/src/lib.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! Test that Kani can correctly verify the cedar implementation of `SmolStr`
//! An ICE was initially reported for this case in:
//! <https://github.com/model-checking/kani/issues/3312>
#[kani::proof]
#[kani::unwind(4)]
fn check_new() {
let data: [char; 3] = kani::any();
let input: String = data.iter().collect();
smol_str::SmolStr::new(&input);
}

0 comments on commit 7a28667

Please sign in to comment.