Resolve duplicate crate dependencies (support multiple versions)

.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,9 +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);
-                let name = format!("{}::{:?}", crate_name, alloc_id);
+                // 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 name = format!("{}::{:?}", self.full_crate_name(), alloc_id);
                 self.codegen_allocation(alloc, |_| name.clone(), Some(name.clone()))
             }
         };

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

@@ -374,7 +374,21 @@ impl<'tcx> GotocCtx<'tcx> {
         // code.  See the implementation of pretty_print_region on line 1720 in
         // compiler/rustc_middle/src/ty/print/pretty.rs.
         let name = name.replace(" + \'static", "").replace("\'static ", "");
-        name
+
+        // Crate resolution: mangled names need to be distinct across different versions
+        // of the same crate that could be pulled in by dependencies. However, RMC's
+        // treatment of FFI C calls asssumes that we generate the same name for structs
+        // as the C name, so don't mangle in that case.
+        // TODO: this is likely insufficient if a dependent crate has two versions of
+        // linked C libraries
+        // https://github.com/model-checking/rmc/issues/450
+        if is_repr_c_adt(t) {
+            return name;
+        }
+
+        // Add unique type id
+        let id_u64 = self.tcx.type_id_hash(t);
+        format!("{}::{}", name, id_u64)
     }
 
     #[allow(dead_code)]
@@ -1201,6 +1215,14 @@ pub fn pointee_type(pointer_type: Ty<'tcx>) -> Option<Ty<'tcx>> {
     }
 }
 
+/// Is the MIR type using a C representation (marked with #[repr(C)] at the source level)?
+pub fn is_repr_c_adt(mir_type: Ty<'tcx>) -> bool {
+    match mir_type.kind() {
+        ty::Adt(def, _) => def.repr.c(),
+        _ => false,
+    }
+}
+
 impl<'tcx> GotocCtx<'tcx> {
     /// A pointer to the mir type should be a thin pointer.
     pub fn use_thin_pointer(&self, mir_type: Ty<'tcx>) -> bool {

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

@@ -21,11 +21,11 @@ use crate::gotoc::cbmc::goto_program::{
 use crate::gotoc::cbmc::utils::aggr_name;
 use crate::gotoc::cbmc::{MachineModel, RoundingMode};
 use crate::gotoc::mir_to_goto::overrides::{type_and_fn_hooks, GotocHooks, GotocTypeHooks};
+use crate::gotoc::mir_to_goto::utils::full_crate_name;
 use rustc_data_structures::owning_ref::OwningRef;
 use rustc_data_structures::rustc_erase_owner;
 use rustc_data_structures::stable_map::FxHashMap;
 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::ty::layout::{HasParamEnv, HasTyCtxt, TyAndLayout};
@@ -43,6 +43,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
@@ -61,6 +63,7 @@ impl<'tcx> GotocCtx<'tcx> {
             symbol_table,
             hooks: fhks,
             type_hooks: thks,
+            full_crate_name: full_crate_name(tcx),
             global_var_count: 0,
             alloc_map: FxHashMap::default(),
             current_fn: None,
@@ -70,10 +73,6 @@ impl<'tcx> GotocCtx<'tcx> {
 
 /// Getters
 impl<'tcx> GotocCtx<'tcx> {
-    pub fn crate_name(&self) -> String {
-        self.tcx.crate_name(LOCAL_CRATE).to_string()
-    }
-
     pub fn current_fn(&self) -> &CurrentFnCtx<'tcx> {
         self.current_fn.as_ref().unwrap()
     }
@@ -225,7 +224,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)
     }
 }
 

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/utils/names.rs

@@ -5,13 +5,25 @@
 
 use crate::gotoc::mir_to_goto::GotocCtx;
 use rustc_hir::def_id::DefId;
+use rustc_hir::def_id::LOCAL_CRATE;
 use rustc_hir::definitions::DefPathDataName;
+use rustc_middle::mir::mono::CodegenUnitNameBuilder;
 use rustc_middle::mir::Local;
 use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::{self, Instance, TyCtxt};
 use tracing::debug;
 
 impl<'tcx> GotocCtx<'tcx> {
+    /// 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) -> &str {
+        &self.full_crate_name
+    }
+
     pub fn codegen_var_base_name(&self, l: &Local) -> String {
         match self.find_debug_info(l) {
             None => format!("var_{}", l.index()),
@@ -98,6 +110,21 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 }
 
+/// 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)
+    )
+}
+
 //TODO: These were moved from hooks.rs, where they didn't have a goto context. Normalize them.
 pub fn sig_of_instance<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> ty::FnSig<'tcx> {
     let ty = instance.ty(tcx, ty::ParamEnv::reveal_all());

scripts/rmc-regression.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
@@ -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,25 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub struct Foo {
+    x: i32,
+}
+
+// Export a function that takes a struct type which differs between this crate 
+// and the other vesion
+pub fn take_foo(foo: &Foo) -> i32 {
+    foo.x
+}
+
+pub fn give_foo() -> Foo {
+    Foo { x: 1 }
+}
+
+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. The constant is also a 
+    // different value than the other version of this dependency.
+    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,13 @@
+// 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()
+}
+
+pub fn delegate_use_struct() -> i32 {
+    let foo = dependency3::give_foo();
+    dependency3::take_foo(&foo)
+}

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,13 @@
+// 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()
+}
+
+pub fn delegate_use_struct() -> i32 {
+    let foo = dependency3::give_foo();
+    dependency3::take_foo(&foo)
+}

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,24 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub struct Foo {
+    x: i32,
+    // This field only in this version.
+    y: i32,
+}
+
+// Export a function that takes a struct type which differs between this crate 
+// and the other vesion.
+pub fn take_foo(foo: &Foo) -> i32 {
+    foo.x + foo.y
+}
+
+pub fn give_foo() -> Foo {
+    Foo { x: 1, y: 2 }
+}
+
+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,14 @@
+// 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);
+
+    assert!(dependency1::delegate_use_struct() == 3);
+    assert!(dependency2::delegate_use_struct() == 1);
+}

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

@@ -0,0 +1,29 @@
+#!/usr/bin/env bash
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# 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
+
+# Convert from JSON to Gotoc 
+cd build/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
+RESULT="/tmp/dependency_test_result.txt"
+cbmc b.out &> $RESULT
+if grep -q "VERIFICATION SUCCESSFUL" $RESULT; then
+  cat $RESULT
+  echo "Successful dependency test"
+  exit 0
+else 
+  cat $RESULT
+  echo "Failed dependency test"
+  exit 1
+fi