Make rmc-rustc errors more user friendly (rust-lang#606)

and also build rmc library as part of the regression script.

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

Author: 2 people

scripts/rmc-regression.sh

@@ -20,8 +20,11 @@ check-cbmc-viewer-version.py --major 2 --minor 5
 # Formatting check
 ./x.py fmt --check
 
-# Standalone rmc tests, expected tests, and cargo tests
+# Build RMC and RMC library
 ./x.py build -i --stage 1 library/std ${EXTRA_X_PY_BUILD_ARGS}
+./scripts/setup/build_rmc_lib.sh
+
+# Standalone rmc tests, expected tests, and cargo tests
 ./x.py test -i --stage 1 rmc firecracker prusti smack expected cargo-rmc
 ./x.py test -i --stage 0 compiler/cbmc
 

scripts/rmc-rustc

@@ -12,52 +12,59 @@ set -eu
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 REPO_DIR="$(dirname $SCRIPT_DIR)"
 
-get_rmc_path() {
-    shopt -s nullglob
-    RMC_CANDIDATES=("$REPO_DIR"/build/*/stage1/bin/rustc)
+RMC_PATH=${RMC_PATH:-""}
+RMC_LIB_PATH=${RMC_LIB_PATH:-""}
 
-    if [[ ${#RMC_CANDIDATES[@]} -ne 1 ]]; then
-        echo "ERROR: Could not find RMC binary."
-        echo "Looked for: $REPO_DIR/build/*/stage1/bin/rustc"
-        echo "Was RMC successfully built first?"
-        exit 1
+shopt -s nullglob
+set_rmc_path() {
+    local RMC_CANDIDATES=("$REPO_DIR"/build/*/stage1/bin/rustc)
+
+    if [ -z "${RMC_PATH}" ]
+    then
+        if [[ -z ${RMC_CANDIDATES:-""} ]] || [[ ${#RMC_CANDIDATES[@]} -ne 1 ]]
+        then
+            echo "ERROR: Could not find RMC binary."
+            echo "Looked for: $REPO_DIR/build/*/stage1/bin/rustc"
+            echo "Was RMC successfully built first?"
+            exit 1
+        fi
+        RMC_PATH=${RMC_CANDIDATES[0]}
     fi
-    echo ${RMC_CANDIDATES[0]}
 }
 
-get_rmc_lib_path() {
-    if [ -z "${RMC_LIB_PATH:-""}" ]
+set_rmc_lib_path() {
+    if [ -z "${RMC_LIB_PATH}" ]
     then
-        RMC_LIB_CANDIDATES=("$REPO_DIR"/target/*/librmc.rlib)
-        if [[ ${#RMC_LIB_CANDIDATES[@]} -ne 1 ]]; then
+        local RMC_LIB_CANDIDATES=("$REPO_DIR"/target/*/librmc.rlib)
+        if [[ -z ${RMC_LIB_CANDIDATES:-""} ]] || [[ ${#RMC_LIB_CANDIDATES[@]} -ne 1 ]]
+        then
             echo "ERROR: Could not find RMC library."
             echo "Looked for: \"$REPO_DIR/target/*/librmc.rlib\""
             echo "Was RMC library successfully built first?"
             exit 1
         fi
-        echo $(dirname ${RMC_LIB_CANDIDATES[0]})
-    else
-        echo ${RMC_LIB_PATH}
+        RMC_LIB_PATH=$(dirname ${RMC_LIB_CANDIDATES[0]})
     fi
 }
 
-RMC_PATH=$(get_rmc_path)
-
-RMC_FLAGS="--crate-type=lib \
-        -Z codegen-backend=gotoc \
-        -Z trim-diagnostic-paths=no \
-        -Z human_readable_cgu_names \
-        --cfg=rmc \
-        -L $(get_rmc_lib_path) \
-        --extern rmc"
-
-if [ "${1:-''}" == "--rmc-flags" ]
-then
-    echo ${RMC_FLAGS}
-elif [ "${1:-''}" == "--rmc-path" ]
+set_rmc_path
+if [ "${1:-''}" == "--rmc-path" ]
 then
     echo ${RMC_PATH}
 else
-    # Execute rmc
-   "${RMC_PATH}" ${RMC_FLAGS} "$@"
+    set_rmc_lib_path
+    RMC_FLAGS="--crate-type=lib \
+            -Z codegen-backend=gotoc \
+            -Z trim-diagnostic-paths=no \
+            -Z human_readable_cgu_names \
+            --cfg=rmc \
+            -L ${RMC_LIB_PATH} \
+            --extern rmc"
+    if [ "${1:-''}" == "--rmc-flags" ]
+    then
+        echo ${RMC_FLAGS}
+    else
+        # Execute rmc
+       "${RMC_PATH}" ${RMC_FLAGS} "$@"
+    fi
 fi