From b126001df39aeee42b6eb6ec7137bcc7f1362122 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Wed, 31 Jul 2024 13:12:12 -0700 Subject: [PATCH 1/3] Add missing padding needded for alignment --- .../src/codegen_cprover_gotoc/codegen/typ.rs | 18 +++++++++++++----- tests/cargo-kani/iss2857/Cargo.toml | 7 +++++++ tests/cargo-kani/iss2857/expected | 1 + tests/cargo-kani/iss2857/src/main.rs | 13 +++++++++++++ 4 files changed, 34 insertions(+), 5 deletions(-) create mode 100644 tests/cargo-kani/iss2857/Cargo.toml create mode 100644 tests/cargo-kani/iss2857/expected create mode 100644 tests/cargo-kani/iss2857/src/main.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 1703335dda51..a6ec8c07bb07 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1140,7 +1140,7 @@ impl<'tcx> GotocCtx<'tcx> { /// Mapping enums to CBMC types is rather complicated. There are a few cases to consider: /// 1. When there is only 0 or 1 variant, this is straightforward as the code shows - /// 2. When there are more variants, rust might decides to apply the typical encoding which + /// 2. When there are more variants, rust might decide to apply the typical encoding which /// regard enums as tagged union, or an optimized form, called niche encoding. /// /// The direct encoding is straightforward. Enums are just mapped to C as a struct of union of structs. @@ -1229,8 +1229,7 @@ impl<'tcx> GotocCtx<'tcx> { } let union_name = format!("{name}-union"); let union_pretty_name = format!("{pretty_name}-union"); - fields.push(DatatypeComponent::field( - "cases", + let cases = gcx.ensure_union(&union_name, &union_pretty_name, |ctx, name| { ctx.codegen_enum_cases( name, @@ -1240,8 +1239,17 @@ impl<'tcx> GotocCtx<'tcx> { variants, initial_offset, ) - }), - )); + }); + let cases_size = Size::from_bytes(cases.sizeof(&gcx.symbol_table)); + fields.push(DatatypeComponent::field("cases", cases)); + // Check if any padding is needed for alignment. This is needed for + // https://github.com/model-checking/kani/issues/2857 for example. + let bytes_so_far = initial_offset + cases_size; + if let Some(padding) = + gcx.codegen_alignment_padding(bytes_so_far, &layout, fields.len()) + { + fields.push(padding); + } fields }) } diff --git a/tests/cargo-kani/iss2857/Cargo.toml b/tests/cargo-kani/iss2857/Cargo.toml new file mode 100644 index 000000000000..7984f9a243e8 --- /dev/null +++ b/tests/cargo-kani/iss2857/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "iss2857" +version = "0.1.0" +edition = "2021" + +[dependencies] +sec1 = "0.7.3" diff --git a/tests/cargo-kani/iss2857/expected b/tests/cargo-kani/iss2857/expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/cargo-kani/iss2857/expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/iss2857/src/main.rs b/tests/cargo-kani/iss2857/src/main.rs new file mode 100644 index 000000000000..6a0ed40a006e --- /dev/null +++ b/tests/cargo-kani/iss2857/src/main.rs @@ -0,0 +1,13 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// This test checks that https://github.com/model-checking/kani/issues/2857 is +// fixed + +#[kani::proof] +fn check_der_error() { + let e = sec1::der::Error::incomplete(sec1::der::Length::ZERO); + let _ = format!("{e:?}"); +} + +fn main() {} From 714cd20c3dd92a24e2d090612e5dfd3e39e290f4 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Wed, 31 Jul 2024 13:20:26 -0700 Subject: [PATCH 2/3] copyright --- tests/cargo-kani/iss2857/Cargo.toml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/cargo-kani/iss2857/Cargo.toml b/tests/cargo-kani/iss2857/Cargo.toml index 7984f9a243e8..9f2a72342c19 100644 --- a/tests/cargo-kani/iss2857/Cargo.toml +++ b/tests/cargo-kani/iss2857/Cargo.toml @@ -1,3 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT [package] name = "iss2857" version = "0.1.0" From 3828ddf06dc9a5ee9e2dadf87429e67ca8af194c Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 1 Aug 2024 11:59:44 -0700 Subject: [PATCH 3/3] Extract variant size from layout --- .../src/codegen_cprover_gotoc/codegen/typ.rs | 25 +++++++++++++------ 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index a6ec8c07bb07..9baa3c59f4c2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1229,7 +1229,8 @@ impl<'tcx> GotocCtx<'tcx> { } let union_name = format!("{name}-union"); let union_pretty_name = format!("{pretty_name}-union"); - let cases = + fields.push(DatatypeComponent::field( + "cases", gcx.ensure_union(&union_name, &union_pretty_name, |ctx, name| { ctx.codegen_enum_cases( name, @@ -1239,15 +1240,23 @@ impl<'tcx> GotocCtx<'tcx> { variants, initial_offset, ) - }); - let cases_size = Size::from_bytes(cases.sizeof(&gcx.symbol_table)); - fields.push(DatatypeComponent::field("cases", cases)); + }), + )); // Check if any padding is needed for alignment. This is needed for // https://github.com/model-checking/kani/issues/2857 for example. - let bytes_so_far = initial_offset + cases_size; - if let Some(padding) = - gcx.codegen_alignment_padding(bytes_so_far, &layout, fields.len()) - { + // The logic for determining the maximum variant size is taken from: + // https://github.com/rust-lang/rust/blob/e60ebb2f2c1facba87e7971798f3cbdfd309cd23/compiler/rustc_session/src/code_stats.rs#L166 + let max_variant_size = variants + .iter() + .map(|l: &LayoutS| l.size) + .max() + .unwrap(); + let max_variant_size = std::cmp::max(max_variant_size, discr_offset); + if let Some(padding) = gcx.codegen_alignment_padding( + max_variant_size, + &layout, + fields.len(), + ) { fields.push(padding); } fields