ty_mangled_name: only use non-mangled name if -Zcffi is enabled. (#4114)

See
#4007 (comment).
Ideally, we'd have a better solution for C structs more generally, but
this solution is enough to fix this particular crash.

Before this fix, the new diamond dependency test harness crashed with:

```
------------------------------------------
stderr:
------------------------------------------
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.00s
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.00s
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.00s
   Compiling main v0.1.0 (/Users/cmzech/kani/tests/cargo-kani/dependency-test/diamond-dependency/main)

thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:887:9:
Error in struct_expr; value type does not match field type.
        StructTag("tag-dependency3::ReprCStruct")
        [Field { name: "field", typ: StructTag("tag-_14480980443891294070469871430240215039") }]
        [Expr { value: Symbol { identifier: "_RNvCslFpuY9hqlfk_11dependency113create_struct::1::var_1" }, typ: StructTag("tag-_12679625102465156734981384663764492039"), location: None, size_of_annotation: None }]
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: dependency1::create_struct
_RNvCslFpuY9hqlfk_11dependency113create_struct
[Kani] current codegen location: Loc { file: "/Users/cmzech/kani/tests/cargo-kani/dependency-test/diamond-dependency/dependency1/src/lib.rs", function: None, start_line: 15, start_col: Some(1), end_line: 15, end_col: Some(51), pragmas: [] }
error: could not compile `main` (lib)
```

Resolves #4007

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: Carolyn Zech

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -4,6 +4,7 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{DatatypeComponent, Expr, Location, Parameter, Symbol, SymbolTable, Type};
 use cbmc::utils::aggr_tag;
 use cbmc::{InternString, InternedString};
+use kani_metadata::UnstableFeature;
 use rustc_abi::{
     BackendRepr::SimdVector, FieldIdx, FieldsShape, Float, Integer, LayoutData, Primitive, Size,
     TagEncoding, TyAndLayout, VariantIdx, Variants,
@@ -487,9 +488,20 @@ impl<'tcx> GotocCtx<'tcx> {
         // This is not a restriction because C can only access non-generic types anyway.
         // TODO: Skipping name mangling is likely insufficient if a dependent crate has two versions of
         // linked C libraries
-        // https://github.com/model-checking/kani/issues/450
+        // https://github.com/model-checking/kani/issues/450.
+        // Note that #[repr(C)] types are unmangled only if the unstable c-ffi feature is enabled; otherwise,
+        // we assume that this struct is a #[repr(C)] in Rust code and mangle it,
+        // c.f. https://github.com/model-checking/kani/issues/4007.
         match t.kind() {
-            TyKind::Adt(def, args) if args.is_empty() && def.repr().c() => {
+            TyKind::Adt(def, args)
+                if args.is_empty()
+                    && def.repr().c()
+                    && self
+                        .queries
+                        .args()
+                        .unstable_features
+                        .contains(&UnstableFeature::CFfi.to_string()) =>
+            {
                 // For non-generic #[repr(C)] types, use the literal path instead of mangling it.
                 self.tcx.def_path_str(def.did()).intern()
             }

tests/cargo-kani/dependency-test/dependency3/src/lib.rs

@@ -5,8 +5,18 @@ pub struct Foo {
     x: i32,
 }
 
+pub enum Field {
+    Case1,
+    Case2,
+}
+
+#[repr(C)]
+pub struct ReprCStruct {
+    pub field: Field,
+}
+
 // Export a function that takes a struct type which differs between this crate
-// and the other vesion
+// and the other version
 pub fn take_foo(foo: &Foo) -> i32 {
     foo.x
 }

tests/cargo-kani/dependency-test/diamond-dependency/dependency1/src/lib.rs

@@ -11,3 +11,7 @@ pub fn delegate_use_struct() -> i32 {
     let foo = dependency3::give_foo();
     dependency3::take_foo(&foo)
 }
+
+pub fn create_struct() -> dependency3::ReprCStruct {
+    dependency3::ReprCStruct { field: dependency3::Field::Case1 }
+}

tests/cargo-kani/dependency-test/diamond-dependency/dependency2/src/lib.rs

@@ -11,3 +11,7 @@ pub fn delegate_use_struct() -> i32 {
     let foo = dependency3::give_foo();
     dependency3::take_foo(&foo)
 }
+
+pub fn create_struct() -> dependency3::ReprCStruct {
+    dependency3::ReprCStruct { field: dependency3::Field::Case1 }
+}

tests/cargo-kani/dependency-test/diamond-dependency/dependency3/src/lib.rs

@@ -7,8 +7,18 @@ pub struct Foo {
     y: i32,
 }
 
+pub enum Field {
+    Case1,
+    Case2,
+}
+
+#[repr(C)]
+pub struct ReprCStruct {
+    pub field: Field,
+}
+
 // Export a function that takes a struct type which differs between this crate
-// and the other vesion.
+// and the other version.
 pub fn take_foo(foo: &Foo) -> i32 {
     foo.x + foo.y
 }

tests/cargo-kani/dependency-test/diamond-dependency/main/src/lib.rs

@@ -12,3 +12,11 @@ fn harness() {
     assert!(dependency1::delegate_use_struct() == 3);
     assert!(dependency2::delegate_use_struct() == 1);
 }
+
+// Test that Kani can codegen repr(C) structs from two different versions of the same crate,
+// c.f. https://github.com/model-checking/kani/issues/4007
+#[kani::proof]
+fn reprc_harness() {
+    dependency1::create_struct();
+    dependency2::create_struct();
+}