From b126001df39aeee42b6eb6ec7137bcc7f1362122 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Wed, 31 Jul 2024 13:12:12 -0700
Subject: [PATCH] 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() {}