Rebase

.gitignore

@@ -80,3 +80,5 @@ src/test/rustdoc-gui/src/**.lock
 /.ninja_deps
 /.ninja_log
 /src/test/dashboard
+**Cargo.lock
+src/test/rmc-dependency-test/diamond-dependency/build

Cargo.toml

@@ -51,6 +51,8 @@ exclude = [
   "src/tools/x",
   # stdarch has its own Cargo workspace
   "library/stdarch",
+  # dependency tests have their own workspace
+  "src/test/rmc-dependency-test/dependency3"
 ]
 
 [profile.release.package.compiler_builtins]

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

@@ -4,7 +4,6 @@ use crate::gotoc::cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
 use crate::gotoc::mir_to_goto::utils::slice_fat_ptr;
 use crate::gotoc::mir_to_goto::GotocCtx;
 use rustc_ast::ast::Mutability;
-use rustc_hir::def_id::LOCAL_CRATE;
 use rustc_middle::mir::interpret::{
     read_target_uint, AllocId, Allocation, ConstValue, GlobalAlloc, Scalar,
 };
@@ -353,8 +352,10 @@ impl<'tcx> GotocCtx<'tcx> {
                 sym.clone().to_expr().address_of()
             }
             GlobalAlloc::Memory(alloc) => {
-                // crate_name added so that allocations in different crates don't clash
-                let crate_name = self.tcx.crate_name(LOCAL_CRATE);
+                // Full (mangled) crate name added so that allocations from different
+                // crates do not conflict. The name alone is insufficient becase Rust
+                // allows different versions of the same crate to be used.
+                let crate_name = self.full_crate_name();
                 let name = format!("{}::{:?}", crate_name, alloc_id);
                 self.codegen_allocation(alloc, |_| name.clone(), Some(name.clone()))
             }

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/compiler_interface.rs

@@ -80,7 +80,7 @@ impl CodegenBackend for GotocCodegenBackend {
                     MonoItem::GlobalAsm(_) => {
                         warn!(
                             "Crate {} contains global ASM, which is not handled by RMC",
-                            c.crate_name()
+                            c.short_crate_name()
                         );
                     }
                 }

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/context/goto_ctx.rs

@@ -28,6 +28,7 @@ use rustc_data_structures::sync::MetadataRef;
 use rustc_hir::def_id::LOCAL_CRATE;
 use rustc_middle::middle::cstore::MetadataLoader;
 use rustc_middle::mir::interpret::Allocation;
+use rustc_middle::mir::mono::CodegenUnitNameBuilder;
 use rustc_middle::ty::layout::{HasParamEnv, HasTyCtxt, TyAndLayout};
 use rustc_middle::ty::{self, Instance, Ty, TyCtxt};
 use rustc_session::Session;
@@ -43,6 +44,8 @@ pub struct GotocCtx<'tcx> {
     pub symbol_table: SymbolTable,
     pub hooks: GotocHooks<'tcx>,
     pub type_hooks: GotocTypeHooks<'tcx>,
+    /// the full crate name, including versioning info
+    pub full_crate_name: String,
     /// a global counter for generating unique names for global variables
     pub global_var_count: u64,
     /// map a global allocation to a name in the symbol table
@@ -54,13 +57,15 @@ pub struct GotocCtx<'tcx> {
 impl<'tcx> GotocCtx<'tcx> {
     pub fn new(tcx: TyCtxt<'tcx>) -> GotocCtx<'tcx> {
         let (thks, fhks) = type_and_fn_hooks();
+        let crate_name = full_crate_name(tcx);
         let mm = machine_model_from_session(tcx.sess);
         let symbol_table = SymbolTable::new(mm);
         GotocCtx {
             tcx,
             symbol_table,
             hooks: fhks,
             type_hooks: thks,
+            full_crate_name: crate_name,
             global_var_count: 0,
             alloc_map: FxHashMap::default(),
             current_fn: None,
@@ -70,10 +75,16 @@ impl<'tcx> GotocCtx<'tcx> {
 
 /// Getters
 impl<'tcx> GotocCtx<'tcx> {
-    pub fn crate_name(&self) -> String {
+    /// The short crate name without versioning information.
+    pub fn short_crate_name(&self) -> String {
         self.tcx.crate_name(LOCAL_CRATE).to_string()
     }
 
+    /// The full crate name including versioning info
+    pub fn full_crate_name(&self) -> String {
+        self.full_crate_name.clone()
+    }
+
     pub fn current_fn(&self) -> &CurrentFnCtx<'tcx> {
         self.current_fn.as_ref().unwrap()
     }
@@ -225,7 +236,7 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn next_global_name(&mut self) -> String {
         let c = self.global_var_count;
         self.global_var_count += 1;
-        format!("{}::global::{}::", self.tcx.crate_name(LOCAL_CRATE), c)
+        format!("{}::global::{}::", self.full_crate_name(), c)
     }
 }
 
@@ -268,6 +279,21 @@ impl MetadataLoader for GotocMetadataLoader {
     }
 }
 
+/// The full crate name should use the Codegen Unit builder to include full name resolution,
+/// for example, the versioning information if a build requires two different versions
+/// of the same crate.
+pub fn full_crate_name(tcx: TyCtxt<'tcx>) -> String {
+    format!(
+        "{}::{}",
+        CodegenUnitNameBuilder::new(tcx).build_cgu_name(
+            LOCAL_CRATE,
+            &[] as &[String; 0],
+            None as Option<String>
+        ),
+        tcx.crate_name(LOCAL_CRATE)
+    )
+}
+
 fn machine_model_from_session(sess: &Session) -> MachineModel {
     // TODO: Hardcoded values from from the ones currently used in env.rs
     // We may wish to get more of them from the session.

scripts/rmc-regression.sh

@@ -30,3 +30,13 @@ $SCRIPT_DIR/std-lib-regression.sh
 
 # Check codegen of firecracker
 $SCRIPT_DIR/codegen-firecracker.sh
+
+# Check that we can use RMC on crates with a diamond dependency graph,
+# with two different versions of the same crate.
+#
+#         dependency1
+#        /           \ v0.1.0
+#   main             dependency3
+#        \           / v0.1.1
+#         dependency2
+./src/test/rmc-dependency-test/diamond-dependency/run-dependency-test.sh

src/test/rmc-dependency-test/dependency3/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "dependency3"
+version = "0.1.0"
+edition = "2018"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

src/test/rmc-dependency-test/dependency3/src/lib.rs

@@ -0,0 +1,10 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub fn get_int() -> i32 {
+    // Use a constant to force an MIR GlobalAllocation::Memory
+    // Use a non-i32 so there will be a conflict between this
+    // version and the other version.
+    let one = &(1 as i8);
+    return *one as i32
+}

src/test/rmc-dependency-test/diamond-dependency/Cargo.toml

@@ -0,0 +1,5 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[workspace]
+members = ["main", "dependency1", "dependency2", "dependency3"]

src/test/rmc-dependency-test/diamond-dependency/dependency1/Cargo.toml

@@ -0,0 +1,12 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "dependency1"
+version = "0.1.0"
+edition = "2018"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+dependency3 = { path = "../dependency3" }

src/test/rmc-dependency-test/diamond-dependency/dependency1/src/lib.rs

@@ -0,0 +1,8 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use dependency3;
+
+pub fn delegate_get_int() -> i32 {
+    dependency3::get_int()
+}

src/test/rmc-dependency-test/diamond-dependency/dependency2/Cargo.toml

@@ -0,0 +1,12 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "dependency2"
+version = "0.1.0"
+edition = "2018"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+dependency3 = { path = "../../dependency3" }

src/test/rmc-dependency-test/diamond-dependency/dependency2/src/lib.rs

@@ -0,0 +1,8 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use dependency3;
+
+pub fn delegate_get_int() -> i32 {
+    dependency3::get_int()
+}

src/test/rmc-dependency-test/diamond-dependency/dependency3/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "dependency3"
+version = "0.1.1"
+edition = "2018"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

src/test/rmc-dependency-test/diamond-dependency/dependency3/src/lib.rs

@@ -0,0 +1,8 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub fn get_int() -> i32 {
+    // Use a constant to force an MIR GlobalAllocation::Memory
+    let zero = &0;
+    return *zero
+}

src/test/rmc-dependency-test/diamond-dependency/main/Cargo.toml

@@ -0,0 +1,13 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "main"
+version = "0.1.0"
+edition = "2018"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+dependency1 = { path = "../dependency1" }
+dependency2 = { path = "../dependency2" }

src/test/rmc-dependency-test/diamond-dependency/main/src/lib.rs

@@ -0,0 +1,11 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use dependency1;
+use dependency2;
+
+#[no_mangle]
+fn harness() {
+    assert!(dependency1::delegate_get_int() == 0);
+    assert!(dependency2::delegate_get_int() == 1);
+}

src/test/rmc-dependency-test/diamond-dependency/run-dependency-test.sh

@@ -0,0 +1,26 @@
+#!/bin/bash
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Test for platform
+platform=`uname -sp`
+if [[ $platform != "Linux x86_64" ]]; then
+  echo "Codegen script only works on Linux x86 platform"
+  exit 0
+fi
+
+# Compile crates with RMC backend
+cd $(dirname $0)
+rm -rf build
+CARGO_TARGET_DIR=build RUST_BACKTRACE=1 RUSTFLAGS="-Z codegen-backend=gotoc --cfg=rmc" RUSTC=rmc-rustc cargo build --target x86_64-unknown-linux-gnu
+
+ # Convert from JSON to Gotoc 
+cd build/x86_64-unknown-linux-gnu/debug/deps/
+ls *.json | xargs symtab2gb
+
+# Add the entry point and remove unused functions
+goto-cc --function harness *.out -o a.out      
+goto-instrument --drop-unused-functions a.out b.out
+
+# Run the solver
+cbmc b.out