From 409f4a9ce76e38f79a4de73dbc3b0fc838d8bfad Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 16 Aug 2024 18:51:41 -0700 Subject: [PATCH 1/3] Fix aggregate handling for raw pointer to str We were handling aggregate of string as we handle thin slices due to a missing match arm. Added the new handling. --- .../src/codegen_cprover_gotoc/codegen/rvalue.rs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index a30eeb7639ce..fddc654a4aaf 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -694,6 +694,15 @@ 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.clone()) }); + debug!(?res_ty, ?typ, ?pointee_goto_typ, "** AGG **"); + 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 = From e2f73b733a3edbbfb4ed6754cdf7032d3109c28f Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 16 Aug 2024 19:31:21 -0700 Subject: [PATCH 2/3] Add tests --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 1 - tests/kani/Str/raw_ptr.rs | 20 +++++++++++++++++++ tests/perf/smol_str/Cargo.toml | 11 ++++++++++ tests/perf/smol_str/expected | 4 ++++ tests/perf/smol_str/src/lib.rs | 13 ++++++++++++ 5 files changed, 48 insertions(+), 1 deletion(-) create mode 100644 tests/kani/Str/raw_ptr.rs create mode 100644 tests/perf/smol_str/Cargo.toml create mode 100644 tests/perf/smol_str/expected create mode 100644 tests/perf/smol_str/src/lib.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index fddc654a4aaf..f16d9bf721e0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -699,7 +699,6 @@ impl<'tcx> GotocCtx<'tcx> { // cast data to pointer with specified type let data_cast = data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ.clone()) }); - debug!(?res_ty, ?typ, ?pointee_goto_typ, "** AGG **"); let meta = self.codegen_operand_stable(&operands[1]); slice_fat_ptr(typ, data_cast, meta, &self.symbol_table) } diff --git a/tests/kani/Str/raw_ptr.rs b/tests/kani/Str/raw_ptr.rs new file mode 100644 index 000000000000..84d33bc608cc --- /dev/null +++ b/tests/kani/Str/raw_ptr.rs @@ -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 . +#![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() }); +} diff --git a/tests/perf/smol_str/Cargo.toml b/tests/perf/smol_str/Cargo.toml new file mode 100644 index 000000000000..2edab49870ea --- /dev/null +++ b/tests/perf/smol_str/Cargo.toml @@ -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" diff --git a/tests/perf/smol_str/expected b/tests/perf/smol_str/expected new file mode 100644 index 000000000000..af045d69d75b --- /dev/null +++ b/tests/perf/smol_str/expected @@ -0,0 +1,4 @@ +Checking harness check_new... +VERIFICATION:- SUCCESSFUL + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/perf/smol_str/src/lib.rs b/tests/perf/smol_str/src/lib.rs new file mode 100644 index 000000000000..7fe771c1fc07 --- /dev/null +++ b/tests/perf/smol_str/src/lib.rs @@ -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: +//! + +#[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); +} From 9fbc4e5cc76c9741a0aa95c93f5420bc3e27cbcb Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 21 Aug 2024 13:21:57 -0700 Subject: [PATCH 3/3] Update kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs --- kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index f16d9bf721e0..e8f1424f09a3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -698,7 +698,7 @@ impl<'tcx> GotocCtx<'tcx> { 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.clone()) }); + 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) }