From c4dc1f8bb414ea092c6e5f2bcbd5467a97e95ab0 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 7 Aug 2023 17:56:28 -0700 Subject: [PATCH] Fix codegen of constant byte slices --- .../src/codegen_cprover_gotoc/codegen/operand.rs | 12 +++--------- tests/cargo-kani/itoa_dep/check_unsigned.expected | 5 +---- tests/cargo-kani/itoa_dep/src/main.rs | 2 -- tests/kani/Slice/const_bytes.rs | 14 ++++++++++++++ tests/kani/Vectors/vector_extend_bytes.rs | 15 +++++++++++++++ 5 files changed, 33 insertions(+), 15 deletions(-) create mode 100644 tests/kani/Slice/const_bytes.rs create mode 100644 tests/kani/Vectors/vector_extend_bytes.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 23211f022b23..49761a8656a3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -196,17 +196,11 @@ impl<'tcx> GotocCtx<'tcx> { } ty::Slice(slice_ty) => { if let Uint(UintTy::U8) = slice_ty.kind() { - // The case where we have a slice of u8 is easy enough: make an array of u8 + let mem_var = self.codegen_const_allocation(data, None); let slice = data.inspect_with_uninit_and_ptr_outside_interpreter(start..end); - let vec_of_bytes: Vec = slice - .iter() - .map(|b| Expr::int_constant(*b, Type::unsigned_int(8))) - .collect(); - let len = vec_of_bytes.len(); - let array_expr = - Expr::array_expr(Type::unsigned_int(8).array_of(len), vec_of_bytes); - let data_expr = array_expr.array_to_ptr(); + let len = slice.len(); + let data_expr = mem_var.cast_to(Type::unsigned_int(8).to_pointer()); let len_expr = Expr::int_constant(len, Type::size_t()); return slice_fat_ptr( self.codegen_ty(lit_ty), diff --git a/tests/cargo-kani/itoa_dep/check_unsigned.expected b/tests/cargo-kani/itoa_dep/check_unsigned.expected index 0bd44abd726a..5281b6338980 100644 --- a/tests/cargo-kani/itoa_dep/check_unsigned.expected +++ b/tests/cargo-kani/itoa_dep/check_unsigned.expected @@ -1,7 +1,4 @@ Status: SUCCESS\ Description: "assertion failed: result == &output" -Status: FAILURE\ -Description: "memcpy source region readable" - -VERIFICATION:- FAILED +VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/itoa_dep/src/main.rs b/tests/cargo-kani/itoa_dep/src/main.rs index c2d1a165a409..9b92065dba06 100644 --- a/tests/cargo-kani/itoa_dep/src/main.rs +++ b/tests/cargo-kani/itoa_dep/src/main.rs @@ -2,8 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! This test checks Kani's support for the `itoa` crate -//! Currently fails with a spurious failure: -//! https://github.com/model-checking/kani/issues/2066 use itoa::{Buffer, Integer}; use std::fmt::Write; diff --git a/tests/kani/Slice/const_bytes.rs b/tests/kani/Slice/const_bytes.rs new file mode 100644 index 000000000000..58d1ded07ccb --- /dev/null +++ b/tests/kani/Slice/const_bytes.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks that byte slices are codegen correctly. This used to fail +//! in the past (see https://github.com/model-checking/kani/issues/2656). + +#[kani::proof] +fn main() { + const MY_CONSTANT: &[u8] = &[147, 211]; + let x: u8 = MY_CONSTANT[0]; + let y: u8 = MY_CONSTANT[1]; + assert_eq!(x, 147); + assert_eq!(y, 211); +} diff --git a/tests/kani/Vectors/vector_extend_bytes.rs b/tests/kani/Vectors/vector_extend_bytes.rs new file mode 100644 index 000000000000..2c48dcfc4653 --- /dev/null +++ b/tests/kani/Vectors/vector_extend_bytes.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that we propertly handle `Vec::extend` with a constant byte slice. +//! This used to fail previously (see +//! https://github.com/model-checking/kani/issues/2656). + +#[kani::proof] +fn check_extend_const_byte_slice() { + const MY_CONSTANT: &[u8] = b"Hi"; + + let mut my_vec: Vec = Vec::new(); + my_vec.extend(MY_CONSTANT); + assert_eq!(my_vec, [72, 105]); +}