Codegen the rest of std lib and add a regression script

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>

Author: 2 people

compiler/rustc_codegen_llvm/src/gotoc/mod.rs

@@ -102,11 +102,15 @@ impl<'tcx> GotocCtx<'tcx> {
             // https://github.com/model-checking/rmc/issues/202
             "fmt::ArgumentV1::<'a>::as_usize" => true,
             // https://github.com/model-checking/rmc/issues/204
-            x if x.ends_with("__getit") => true,
+            name if name.ends_with("__getit") => true,
             // https://github.com/model-checking/rmc/issues/205
             "panic::Location::<'a>::caller" => true,
             // https://github.com/model-checking/rmc/issues/207
             "core::slice::<impl [T]>::split_first" => true,
+            // https://github.com/model-checking/rmc/issues/281
+            name if name.starts_with("bridge::client") => true,
+            // https://github.com/model-checking/rmc/issues/282
+            "bridge::closure::Closure::<'a, A, R>::call" => true,
             _ => false,
         }
     }

compiler/rustc_codegen_llvm/src/gotoc/typ.rs

@@ -1034,6 +1034,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Check if the mir type already is a vtable fat pointer.
     pub fn is_vtable_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool {
-        pointee_type(mir_type).map_or(false, |p| self.use_vtable_fat_pointer(p))
+        self.is_ref_of_unsized(mir_type)
+            && self.use_vtable_fat_pointer(pointee_type(mir_type).unwrap())
     }
 }

scripts/rmc-regression.sh

@@ -22,3 +22,6 @@ check-cbmc-viewer-version.py --major 2 --minor 5
 # Standalone rmc tests, expected tests, and cargo tests
 ./x.py build -i --stage 1 library/std ${EXTRA_X_PY_BUILD_ARGS}
 ./x.py test -i --stage 1 cbmc firecracker prusti smack expected cargo-rmc
+
+# Check codegen for the standard library
+$SCRIPT_DIR/std-lib-regression.sh

scripts/std-lib-regression.sh

@@ -0,0 +1,42 @@
+#!/usr/bin/env 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
+
+# Get RMC root
+SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+RMC_DIR=$SCRIPT_DIR/..
+
+# Log output
+STD_LIB_LOG="/tmp/SizeAndAlignOfDstTest/log.txt"
+
+# Use a unit test that requires mutex and cell
+echo "Starting RMC codegen for the Rust standard library"
+cd /tmp
+if [ -d SizeAndAlignOfDstTest ]; then rm -rf SizeAndAlignOfDstTest; fi
+cargo new SizeAndAlignOfDstTest
+cd SizeAndAlignOfDstTest
+cp $RMC_DIR/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs src/main.rs 
+rustup component add rust-src --toolchain nightly > /dev/null 2>&1
+RUSTFLAGS="-Z trim-diagnostic-paths=no -Z codegen-backend=gotoc --cfg=rmc" RUSTC=rmc-rustc cargo +nightly build -Z build-std --target x86_64-unknown-linux-gnu 2> $STD_LIB_LOG
+
+# For now, we expect a linker error, but no modules should fail with a compiler
+# panic. 
+#
+# With https://github.com/model-checking/rmc/issues/109, this check can be
+# removed to just allow the success of the previous line to determine the 
+# success of this script (with no $STD_LIB_LOG needed)
+RESULT=$?
+if grep -q "error: internal compiler error: unexpected panic" $STD_LIB_LOG; then
+  echo "Panic on building standard library"
+  cat $STD_LIB_LOG
+  exit 1
+else 
+echo "Successful RMC codegen for the Rust standard library"
+fi