Fix the bug: Static union values can panic Kani

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);
+}