Add quotes everywhere to handle names with spaces

carbon/build.sh

@@ -1,4 +1,4 @@
-cd $(dirname $0)/../viper
+cd "$(dirname "$0")/../viper"
 
 ./build.sh
 if ! type boogie > /dev/null; then

carbon/run.sh

@@ -1,3 +1,3 @@
-OUT=$(pwd)/${2%.*}
-mkdir -p $(dirname "$OUT")
-python $(dirname $0)/../viper/viper_client/client.py -j bulk -p 50424 -f $1 -v carbon -x="--disableCaching --boogieExe=$(which boogie) --timeout $3 --print \"$OUT.bpl\" --boogieOpt \"/proverLog:$OUT-@[email protected]\"" > /dev/null
+OUT="$(pwd)/${2%.*}"
+mkdir -p "$(dirname "$OUT")"
+python "$(dirname "$0")/../viper/viper_client/client.py" -j bulk -p 50424 -f "$1" -v carbon -x="--disableCaching --boogieExe \"$(which boogie)\" --timeout \"$3\" --print \"$OUT.bpl\" --boogieOpt \"/proverLog:$OUT-@[email protected]\"" > /dev/null

carbon/tests.sh

@@ -1,3 +1,3 @@
-DIRNAME=$(dirname $0)
+DIRNAME=$(dirname "$0")
 DIRNAME=$(realpath "$DIRNAME/../viper/viperserver")
-find $DIRNAME/carbon/src/test/resources $DIRNAME/carbon/silver/src/test/resources -name "*.vpr" -type f
+find "$DIRNAME/carbon/src/test/resources" "$DIRNAME/carbon/silver/src/test/resources" -name "*.vpr" -type f

dafny/build.sh

@@ -1,4 +1,4 @@
-cd $(dirname "$0")/dafny
+cd "$(dirname "$0")/dafny"
 
 if [ ! -f Binaries/Dafny ]; then
     make

dafny/run.sh

@@ -1,5 +1,5 @@
-OUT=$(pwd)/${2%.*}
-mkdir -p $(dirname "$OUT")
+OUT="$(pwd)/$(echo "${2%.*}" | sed 's/ /_/g')"
+mkdir -p "$(dirname "$OUT")"
 
-cd $(dirname "$0")/dafny
-Binaries/Dafny /deprecation:0 /compile:0 /timeLimit:$3 /print:$OUT.bpl /vcsCores:1 /proverLog:$OUT-@[email protected] $1
+cd "$(dirname "$0")/dafny"
+Binaries/Dafny /deprecation:0 /compile:0 /timeLimit:$3 /print:$OUT.bpl /vcsCores:1 /proverLog:$OUT-@[email protected] "$1"

dafny/tests.sh

@@ -1 +1 @@
-find $(realpath "$0" | xargs dirname)/dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest -name "*.dfy" -type f
+find "$(realpath "$0" | xargs dirname)/dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest" -name "*.dfy" -type f

make_smt2.sh

@@ -1,27 +1,29 @@
 # Can pass in a list of verifiers to run, or defaults to all
 # Can set TIMEOUT to change the timeout for each verifier
 
-VERIFIERS=$@
+VERIFIERS="$@"
 if [ -z "$VERIFIERS" ]; then
     VERIFIERS="silicon carbon dafny"
 fi
 
 git submodule update --init --recursive &> /dev/null
 
-DIRNAME=$(realpath $0 | xargs dirname)
-VERIFIERS="$DIRNAME/$(echo $VERIFIERS | sed "s| | $DIRNAME/|g")"
-for verifier in $VERIFIERS; do
+DIRNAME=$(realpath "$0" | xargs dirname)
+VERIFIERS="$DIRNAME/$(echo "$VERIFIERS" | sed "s| |\n$DIRNAME/|g")"
+while read -r verifier; do
     echo "[Running $verifier]"
-    cd $verifier
+    cd "$verifier"
     ./build.sh
-    VERIFIER=$(basename $verifier)
-    for file in `./tests.sh`; do
-        no_prefix=$(echo $file | perl -pe "s|.*?/$VERIFIER/||")
+    VERIFIER=$(basename "$verifier")
+    # Split on '\n' with `while` instead of potentially ' ' in filename with `for`
+    while read -r file; do
+        # This requires that 
+        no_prefix=$(echo "$file" | perl -pe "s|.*?/$VERIFIER/||")
         if [ "$file" == "$no_prefix" ]; then
             echo "Could not strip prefix (.*/$VERIFIER/): $no_prefix"
             exit 1
         fi
         echo "[.smt2] $no_prefix"
-        ./run.sh $file ../smt2/$VERIFIER/$no_prefix ${TIMEOUT:-10}
-    done
-done
+        ./run.sh "$file" "../smt2/$VERIFIER/$no_prefix" "${TIMEOUT:-10}"
+    done <<< "$(./tests.sh)"
+done <<< "$VERIFIERS"

silicon/build.sh

@@ -1,3 +1,3 @@
-cd $(dirname $0)/../viper
+cd "$(dirname "$0")/../viper"
 
 ./build.sh

silicon/run.sh

@@ -1,3 +1,3 @@
-OUT=$(pwd)/${2%.*}
-mkdir -p $(dirname "$OUT")
-python $(dirname $0)/../viper/viper_client/client.py -j bulk -p 50424 -f $1 -v silicon -x="--disableCaching --timeout $3 --numberOfParallelVerifiers 1 --proverLogFile \"$OUT.smt2\"" > /dev/null
+OUT="$(pwd)/${2%.*}"
+mkdir -p "$(dirname "$OUT")"
+python "$(dirname "$0")/../viper/viper_client/client.py" -j bulk -p 50424 -f "$1" -v silicon -x="--disableCaching --timeout \"$3\" --numberOfParallelVerifiers 1 --proverLogFile \"$OUT.smt2\"" > /dev/null

silicon/tests.sh

@@ -1,3 +1,3 @@
-DIRNAME=$(dirname $0)
+DIRNAME=$(dirname "$0")
 DIRNAME=$(realpath "$DIRNAME/../viper/viperserver")
-find $DIRNAME/silicon/src/test/resources $DIRNAME/silicon/silver/src/test/resources -name "*.vpr" -type f
+find "$DIRNAME/silicon/src/test/resources" "$DIRNAME/silicon/silver/src/test/resources" -name "*.vpr" -type f

smt2/make_log.sh

@@ -1,10 +1,10 @@
 Z3_VERSION=$(z3 --version | sed -E 's/.* ([0-9]+\.[0-9]+\.[0-9]+).*/\1/g')
 Z3_VERSION_REGEX="${Z3_VERSION//./\\.}"
 
-cd ${1-$(dirname $0)}
-for file in `find . -name "*.smt2" -type f`; do
+cd "${1-$(dirname $0)}"
+while read -r file; do
     # Check if the first line contains my Z3 version (and skip if it does)
-    [ "$(sed -n '/^;[^\n]*$Z3_VERSION_REGEX/p;q' $file)" ] && echo "Skipping \"$file\" as the first line contains \"$Z3_VERSION\"" && continue || true
+    [ "$(sed -n '/^;[^\n]*$Z3_VERSION_REGEX/p;q' "$file")" ] && echo "Skipping \"$file\" as the first line contains \"$Z3_VERSION\"" && continue || true
 
     # Check if the (non-empty) log file exists
     file_hash=$(shasum -a 256 "$file" | cut -d' ' -f1)
@@ -23,9 +23,9 @@ for file in `find . -name "*.smt2" -type f`; do
     # the output so that it doesn't get printed and listen for a
     # timeout message in which case we remove the last line of the log
     # file since it may be incomplete (and cause parsing errors).
-    output=$(z3 trace=true proof=true -memory:15872 -T:10 trace-file-name=$log_file_name ./$file)
-    echo $output | grep -q "timeout" || continue
+    output=$(z3 trace=true proof=true -memory:15872 -T:10 trace-file-name=$log_file_name "./$file")
+    echo "$output" | grep -q "timeout" || continue
     echo "[Timeout] Removing last line of logfile"
     tail -n 1 "$log_file_name" | wc -c | xargs -I {} truncate -s -{} "$log_file_name"
     test -s "$log_file_name" || echo "!!! Log file not created for \"$file\""
-done
+done <<<  "$(find . -name "*.smt2" -type f)"