From 99a21187514b328b865048785c3eda670f3f07ee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Thu, 26 Dec 2024 12:02:22 +0100 Subject: [PATCH] Add quotes everywhere to handle names with spaces --- carbon/build.sh | 2 +- carbon/run.sh | 6 +++--- carbon/tests.sh | 4 ++-- dafny/build.sh | 2 +- dafny/run.sh | 8 ++++---- dafny/tests.sh | 2 +- make_smt2.sh | 24 +++++++++++++----------- silicon/build.sh | 2 +- silicon/run.sh | 6 +++--- silicon/tests.sh | 4 ++-- smt2/make_log.sh | 12 ++++++------ 11 files changed, 37 insertions(+), 35 deletions(-) diff --git a/carbon/build.sh b/carbon/build.sh index 8e588125e..466134baa 100755 --- a/carbon/build.sh +++ b/carbon/build.sh @@ -1,4 +1,4 @@ -cd $(dirname $0)/../viper +cd "$(dirname "$0")/../viper" ./build.sh if ! type boogie > /dev/null; then diff --git a/carbon/run.sh b/carbon/run.sh index 9f8913704..98d7be7be 100755 --- a/carbon/run.sh +++ b/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-@PROC@.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 carbon -x="--disableCaching --boogieExe \"$(which boogie)\" --timeout \"$3\" --print \"$OUT.bpl\" --boogieOpt \"/proverLog:$OUT-@PROC@.smt2\"" > /dev/null diff --git a/carbon/tests.sh b/carbon/tests.sh index a5d152cb1..9c83d729d 100755 --- a/carbon/tests.sh +++ b/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 diff --git a/dafny/build.sh b/dafny/build.sh index 4d55eccee..007823e93 100755 --- a/dafny/build.sh +++ b/dafny/build.sh @@ -1,4 +1,4 @@ -cd $(dirname "$0")/dafny +cd "$(dirname "$0")/dafny" if [ ! -f Binaries/Dafny ]; then make diff --git a/dafny/run.sh b/dafny/run.sh index df4f6eecb..1276f5297 100755 --- a/dafny/run.sh +++ b/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-@PROC@.smt2 $1 +cd "$(dirname "$0")/dafny" +Binaries/Dafny /deprecation:0 /compile:0 /timeLimit:$3 /print:$OUT.bpl /vcsCores:1 /proverLog:$OUT-@PROC@.smt2 "$1" diff --git a/dafny/tests.sh b/dafny/tests.sh index 585de7c81..bc075e529 100755 --- a/dafny/tests.sh +++ b/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 diff --git a/make_smt2.sh b/make_smt2.sh index 2a41b95d4..d40feee28 100755 --- a/make_smt2.sh +++ b/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" diff --git a/silicon/build.sh b/silicon/build.sh index c5da15043..ec1982535 100755 --- a/silicon/build.sh +++ b/silicon/build.sh @@ -1,3 +1,3 @@ -cd $(dirname $0)/../viper +cd "$(dirname "$0")/../viper" ./build.sh diff --git a/silicon/run.sh b/silicon/run.sh index b6303a478..05eb8b684 100755 --- a/silicon/run.sh +++ b/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 diff --git a/silicon/tests.sh b/silicon/tests.sh index 7958ad20c..74ba5d6c0 100755 --- a/silicon/tests.sh +++ b/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 diff --git a/smt2/make_log.sh b/smt2/make_log.sh index ee4d5905d..d0a4939b6 100755 --- a/smt2/make_log.sh +++ b/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)"