Fix issue where array types were recorded as [x; _] and hence aliasing (rust-lang#15)

Author: danielsn

compiler/rustc_codegen_llvm/src/gotoc/typ.rs

@@ -22,6 +22,7 @@ use rustc_target::abi::{
 use std::convert::TryInto;
 use std::fmt::Debug;
 use tracing::debug;
+use ty::layout::HasParamEnv;
 /// Map the unit type to an empty struct
 ///
 /// Mapping unit to `void` works for functions with no return type but not for variables with type
@@ -301,13 +302,18 @@ impl<'tcx> GotocCtx<'tcx> {
                 }
             }
             ty::Foreign(defid) => self.codegen_foreign(ty, *defid),
-            ty::Array(et, _) => {
+            ty::Array(et, len) => {
+                let array_name = format!(
+                    "[{}; {}]",
+                    self.ty_mangled_name(et),
+                    len.try_eval_usize(self.tcx, self.param_env()).unwrap()
+                );
                 // wrap arrays into struct so that one can take advantage of struct copy in C
                 //
                 // struct [T; n] {
                 //   T _0[n];
                 // }
-                self.ensure_struct(&self.ty_mangled_name(ty), |ctx, name| {
+                self.ensure_struct(&array_name, |ctx, name| {
                     if et.is_unit() {
                         // we do not generate a struct with an array of units
                         vec![]

rust-tests/cbmc-reg/Static/table_of_pairs2.rs

@@ -0,0 +1,22 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+const SIZE1: usize = 1;
+const SIZE2: usize = 2;
+
+pub static TABLE1: [(u64, u64); SIZE1] = [(0, 1)];
+
+pub static TABLE2: [(u64, u64); SIZE2] = [(2, 3), (4, 5)];
+
+// This is to ensure that we don't just constant propagate away the assertion
+fn test_equal(a: u64, b: u64) -> bool {
+    a == b
+}
+
+fn main() {
+    let x = TABLE1[0];
+    assert!(test_equal(x.1, 1));
+    let y = TABLE2[0];
+    assert!(test_equal(y.1, 3));
+    let z = TABLE2[1];
+    assert!(test_equal(z.1, 5));
+}