Fix the bug: Static union values can panic Kani (#4112)

This PR fixes the bug: Static union values can panic Kani.

The reason behind the bug is Kani's translation of Union type is not
consistent with its layout defined by Rust. Specifically, the size of
the Union is not just the max of its fields but that maximum should be
round up to a multiple of its alignment.
See:

https://web.mit.edu/rust-lang_v1.25/arch/amd64_ubuntu1404/share/doc/rust/html/reference/type-layout.html#:~:text=The%20layout%20of%20a%20type,also%20part%20of%20type%20layout

In this PR, I add another variant for DataComponent:
DataComponent::UnionField, with a padded_type of a Union (a struct which
contains a padding and the real field type) to fix the translated layout
and support reasoning about transmute function for union type.

Resolves #4097

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: thanhnguyen-aws

cprover_bindings/src/goto_program/typ.rs

@@ -99,6 +99,7 @@ pub enum CIntType {
 pub enum DatatypeComponent {
     Field { name: InternedString, typ: Type },
     Padding { name: InternedString, bits: u64 },
+    UnionField { name: InternedString, typ: Type, padded_typ: Type },
 }
 
 /// The formal parameters of a function.
@@ -120,40 +121,45 @@ impl DatatypeComponent {
     pub fn field_typ(&self) -> Option<&Type> {
         match self {
             Field { typ, .. } => Some(typ),
+            UnionField { typ, .. } => Some(typ),
             Padding { .. } => None,
         }
     }
 
     pub fn is_field(&self) -> bool {
         match self {
             Field { .. } => true,
+            UnionField { .. } => true,
             Padding { .. } => false,
         }
     }
 
     pub fn is_padding(&self) -> bool {
         match self {
             Field { .. } => false,
+            UnionField { .. } => false,
             Padding { .. } => true,
         }
     }
 
     pub fn name(&self) -> InternedString {
         match self {
-            Field { name, .. } | Padding { name, .. } => *name,
+            Field { name, .. } | UnionField { name, .. } | Padding { name, .. } => *name,
         }
     }
 
     pub fn sizeof_in_bits(&self, st: &SymbolTable) -> u64 {
         match self {
             Field { typ, .. } => typ.sizeof_in_bits(st),
+            UnionField { padded_typ, .. } => padded_typ.sizeof_in_bits(st),
             Padding { bits, .. } => *bits,
         }
     }
 
     pub fn typ(&self) -> Type {
         match self {
             Field { typ, .. } => typ.clone(),
+            UnionField { typ, .. } => typ.clone(),
             Padding { bits, .. } => Type::unsigned_int(*bits),
         }
     }
@@ -203,6 +209,15 @@ impl DatatypeComponent {
         Field { name, typ }
     }
 
+    pub fn unionfield<T: Into<InternedString>>(name: T, typ: Type, padded_typ: Type) -> Self {
+        let name = name.into();
+        assert!(
+            Self::typecheck_datatype_field(&typ),
+            "Illegal field.\n\tName: {name}\n\tType: {typ:?}"
+        );
+        UnionField { name, typ, padded_typ }
+    }
+
     pub fn padding<T: Into<InternedString>>(name: T, bits: u64) -> Self {
         let name = name.into();
         Padding { name, bits }
@@ -384,7 +399,7 @@ impl Type {
             StructTag(tag) => st.lookup(*tag).unwrap().typ.sizeof_in_bits(st),
             TypeDef { .. } => unreachable!("Expected concrete type."),
             Union { components, .. } => {
-                components.iter().map(|x| x.typ().sizeof_in_bits(st)).max().unwrap_or(0)
+                components.iter().map(|x| x.sizeof_in_bits(st)).max().unwrap_or(0)
             }
             UnionTag(tag) => st.lookup(*tag).unwrap().typ.sizeof_in_bits(st),
             Unsignedbv { width } => *width,
@@ -809,6 +824,7 @@ impl Type {
                     match &components[0] {
                         Padding { .. } => None,
                         Field { typ, .. } => recurse(typ, st),
+                        UnionField { typ, .. } => recurse(typ, st),
                     }
                 } else {
                     None

cprover_bindings/src/irep/to_irep.rs

@@ -136,6 +136,13 @@ impl ToIrep for DatatypeComponent {
                 (IrepId::CPrettyName, Irep::just_string_id(name.to_string())),
                 (IrepId::Type, typ.to_irep(mm)),
             ]),
+            DatatypeComponent::UnionField { name, typ: _, padded_typ } => {
+                Irep::just_named_sub(linear_map![
+                    (IrepId::Name, Irep::just_string_id(name.to_string())),
+                    (IrepId::CPrettyName, Irep::just_string_id(name.to_string())),
+                    (IrepId::Type, padded_typ.to_irep(mm)),
+                ])
+            }
             DatatypeComponent::Padding { name, bits } => Irep::just_named_sub(linear_map![
                 (IrepId::CIsPadding, Irep::one()),
                 (IrepId::Name, Irep::just_string_id(name.to_string())),

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -161,6 +161,11 @@ impl GotocCtx<'_> {
                                 debug_write_type(ctx, typ, out, indent + 2)?;
                                 writeln!(out, ",")?;
                             }
+                            DatatypeComponent::UnionField { name, typ, .. } => {
+                                write!(out, "{:indent$}{name}: ", "", indent = indent + 2)?;
+                                debug_write_type(ctx, typ, out, indent + 2)?;
+                                writeln!(out, ",")?;
+                            }
                             DatatypeComponent::Padding { bits, .. } => {
                                 writeln!(
                                     out,
@@ -197,6 +202,11 @@ impl GotocCtx<'_> {
                                 debug_write_type(ctx, typ, out, indent + 2)?;
                                 writeln!(out, ",")?;
                             }
+                            DatatypeComponent::UnionField { name, typ, .. } => {
+                                write!(out, "{:indent$}{name}: ", "", indent = indent + 2)?;
+                                debug_write_type(ctx, typ, out, indent + 2)?;
+                                writeln!(out, ",")?;
+                            }
                             DatatypeComponent::Padding { bits, .. } => {
                                 writeln!(
                                     out,
@@ -1195,15 +1205,36 @@ impl<'tcx> GotocCtx<'tcx> {
         def: &'tcx AdtDef,
         subst: &'tcx GenericArgsRef<'tcx>,
     ) -> Type {
+        let union_size = rustc_internal::stable(ty).layout().unwrap().shape().size.bits();
+        let union_name = self.ty_mangled_name(ty);
+        let union_pretty_name = self.ty_pretty_name(ty);
         self.ensure_union(self.ty_mangled_name(ty), self.ty_pretty_name(ty), |ctx, _| {
-            def.variants().raw[0]
+            let fields_info: Vec<(String, Type, u64)> = def.variants().raw[0]
                 .fields
                 .iter()
                 .map(|f| {
-                    DatatypeComponent::field(
-                        f.name.to_string(),
-                        ctx.codegen_ty(f.ty(ctx.tcx, subst)),
-                    )
+                    let ty = rustc_internal::stable(f.ty(ctx.tcx, subst));
+                    let ty_size = ty.layout().unwrap().shape().size.bits();
+                    let padding_size = union_size - ty_size;
+                    (f.name.to_string(), ctx.codegen_ty_stable(ty), padding_size as u64)
+                })
+                .collect();
+            fields_info
+                .iter()
+                .map(|(name, ty, padding)| {
+                    let struct_name = format!("{union_name}::{name}");
+                    let pretty_struct_name = format!("{union_pretty_name}::{name}");
+                    let pad_name = format!("{name}_padding");
+                    let padded_typ: Type = if *padding == 0 {
+                        ty.clone()
+                    } else {
+                        let pad =
+                            DatatypeComponent::Padding { name: pad_name.into(), bits: *padding };
+                        ctx.ensure_struct(struct_name, pretty_struct_name, |_ctx, _| {
+                            vec![DatatypeComponent::field(name, ty.clone()), pad.clone()]
+                        })
+                    };
+                    DatatypeComponent::unionfield(name, ty.clone(), padded_typ)
                 })
                 .collect()
         })

tests/expected/union/static_union.expected

@@ -0,0 +1,10 @@
+main.assertion.2\
+         - Status: SUCCESS\
+         - Description: "assertion failed: unsafe { FOO.a[1] } == 0"
+
+
+main.assertion.3\
+         - Status: SUCCESS\
+         - Description: "assertion failed: unsafe { BAR.b } == 3"\
+
+VERIFICATION:- SUCCESSFUL

tests/expected/union/static_union.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+static FOO: Data = Data { a: [0; 3] };
+
+static BAR: Data = Data { b: 3 };
+
+union Data {
+    a: [u8; 3],
+    b: u16,
+}
+
+#[kani::proof]
+fn main() {
+    let _x = &FOO;
+    assert!(unsafe { FOO.a[1] } == 0);
+    assert!(unsafe { BAR.b } == 3);
+}

tests/expected/union/static_union2.expected

@@ -0,0 +1,11 @@
+main.assertion.1\
+         - Status: SUCCESS\
+         - Description: "index out of bounds: the length is less than or equal to the given index"\
+
+Check 2: main.assertion.2\
+         - Status: FAILURE\
+         - Description: "assertion failed: unsafe { FOO.a[1] } == 5"\
+
+Failed Checks: assertion failed: unsafe { FOO.a[1] } == 5
+
+VERIFICATION:- FAILED

tests/expected/union/static_union2.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+static FOO: Data = Data { a: [0; 3] };
+
+union Data {
+    a: [u8; 3],
+    b: u16,
+}
+
+#[kani::proof]
+fn main() {
+    let _x = &FOO;
+    assert!(unsafe { FOO.a[1] } == 5);
+}

tests/expected/union/union_transmute.expected

@@ -0,0 +1,5 @@
+main.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: y == 256"
+
+VERIFICATION:- SUCCESSFUL

tests/expected/union/union_transmute.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use std::mem::transmute;
+
+static FOO: Data = Data { a: [0, 1, 0] };
+
+#[derive(Copy, Clone)]
+union Data {
+    a: [u8; 3],
+    b: u16,
+}
+
+#[kani::proof]
+fn main() {
+    let y: u32 = unsafe { transmute(FOO) };
+    assert!(y == 256);
+}