Fix for computing the minimum offset for an enum variant

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs

@@ -990,7 +990,20 @@ impl<'tcx> GotocCtx<'tcx> {
         variants
             .iter()
             .filter_map(|lo| {
-                if lo.fields.count() == 0 { None } else { Some(lo.fields.offset(0).bits_usize()) }
+                if lo.fields.count() == 0 {
+                    None
+                } else {
+                    // get the offset of the leftmost field, which is the one
+                    // with the least offset since we codegen fields in a struct
+                    // in the order of increasing offsets. Note that this is not
+                    // necessarily the 0th field since the compiler may reorder
+                    // fields.
+                    Some(
+                        lo.fields
+                            .offset(lo.fields.index_by_increasing_offset().nth(0).unwrap())
+                            .bits_usize(),
+                    )
+                }
             })
             .min()
     }

src/test/cbmc/Enum/min_offset.rs

@@ -0,0 +1,24 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that we properly handle structs for which the compiler reorders the
+// fields to optimize the layout. In such cases, the field with minimum offset
+// need not be the first field in the original struct (e.g. in "Foo" below, "b"
+// is the field with minimum offset even though "a" is the leftmost field in the
+// original struct).
+
+enum E {
+    Foo { a: u64, b: u16 },
+    Bar,
+}
+
+fn main() {
+    let e = E::Foo { a: 32, b: 100 };
+    match e {
+        E::Foo { a, b } => {
+            assert!(a == 32);
+            assert!(b == 100);
+        }
+        E::Bar => assert!(false),
+    }
+}