From 90b99e0e7a38eb8fc9bdf56279cf7300a0be1d4b Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 2 Sep 2021 21:52:01 +0000 Subject: [PATCH 1/6] Fixed function that determines the minimum offset of an enum variant --- .../src/gotoc/mir_to_goto/codegen/typ.rs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs index 9bc3b2fd4d31..abe759cb7059 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs @@ -1009,7 +1009,15 @@ 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 { + Some( + lo.fields + .offset(lo.fields.index_by_increasing_offset().nth(0).unwrap()) + .bits_usize(), + ) + } }) .min() } From 54246f040822a686b0b3901c10f8981402eb7389 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 2 Sep 2021 21:52:43 +0000 Subject: [PATCH 2/6] Added small example for #412 --- src/test/cbmc/Enum/min_offset.rs | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 src/test/cbmc/Enum/min_offset.rs diff --git a/src/test/cbmc/Enum/min_offset.rs b/src/test/cbmc/Enum/min_offset.rs new file mode 100644 index 000000000000..d59fc3104b18 --- /dev/null +++ b/src/test/cbmc/Enum/min_offset.rs @@ -0,0 +1,17 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +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), + } +} \ No newline at end of file From 4dafa60cf66fbea05c298be85278502e71c03a6e Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 2 Sep 2021 22:31:15 +0000 Subject: [PATCH 3/6] Ran rustfmt on test --- src/test/cbmc/Enum/min_offset.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/test/cbmc/Enum/min_offset.rs b/src/test/cbmc/Enum/min_offset.rs index d59fc3104b18..ffa606347340 100644 --- a/src/test/cbmc/Enum/min_offset.rs +++ b/src/test/cbmc/Enum/min_offset.rs @@ -1,17 +1,17 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT enum E { - Foo { a: u64, b: u16, }, + Foo { a: u64, b: u16 }, Bar, } fn main() { let e = E::Foo { a: 32, b: 100 }; match e { - E::Foo{ a, b } => { + E::Foo { a, b } => { assert!(a == 32); assert!(b == 100); } E::Bar => assert!(false), } -} \ No newline at end of file +} From 85d61494576218f66dedd50c08474bfbcac17002 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 3 Sep 2021 00:36:42 +0000 Subject: [PATCH 4/6] Added a comment that explains the logic for determining the minimum offset for a struct --- .../rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs index abe759cb7059..ba1a5e7a4c5b 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs @@ -1012,6 +1012,9 @@ impl<'tcx> GotocCtx<'tcx> { 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 Some( lo.fields .offset(lo.fields.index_by_increasing_offset().nth(0).unwrap()) From 54985e03ffe6562c831f5411b47df73ba87f182d Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 3 Sep 2021 01:33:48 +0000 Subject: [PATCH 5/6] Added a comment to explain the purpose of the test --- src/test/cbmc/Enum/min_offset.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/test/cbmc/Enum/min_offset.rs b/src/test/cbmc/Enum/min_offset.rs index ffa606347340..4b28179e5f33 100644 --- a/src/test/cbmc/Enum/min_offset.rs +++ b/src/test/cbmc/Enum/min_offset.rs @@ -1,5 +1,12 @@ // 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, From b8055bbb45bc9fba85a24be5c7a2d917a33a40f0 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 3 Sep 2021 01:36:23 +0000 Subject: [PATCH 6/6] Expanded previous comment that explains the logic for determining the minimum offset --- .../rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs index ba1a5e7a4c5b..10d3b29ea6ce 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs @@ -1014,7 +1014,9 @@ impl<'tcx> GotocCtx<'tcx> { } 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 + // 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())