diff --git a/smt2/make_log.sh b/smt2/make_log.sh index d0a4939b6..174b80446 100755 --- a/smt2/make_log.sh +++ b/smt2/make_log.sh @@ -1,31 +1,13 @@ -Z3_VERSION=$(z3 --version | sed -E 's/.* ([0-9]+\.[0-9]+\.[0-9]+).*/\1/g') -Z3_VERSION_REGEX="${Z3_VERSION//./\\.}" +export Z3_VERSION=${Z3_VERSION:-$(z3 --version | sed -E 's/.* ([0-9]+\.[0-9]+\.[0-9]+).*/\1/g')} +DIRNAME="$(realpath "$(dirname "$0")")" -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 - - # Check if the (non-empty) log file exists - file_hash=$(shasum -a 256 "$file" | cut -d' ' -f1) - base_name="../logs/${file%.*}" - log_file_name="$base_name-fHash-$file_hash.log" - test -s "$log_file_name" && echo "Skipping \"$file\" as \"$file_hash\" exists" && continue || true +if [ -z "$1" ]; then + mkdir -p "$DIRNAME/../logs" + cd "$DIRNAME/../logs" +else + cd "$1" +fi - # Remove old logs - rm -f "$base_name-fHash-*.log" - mkdir -p $(dirname "$log_file_name") - - echo "[.log] $file" - # Run Z3 solver for the file and save the log in the '../logs' directory. - # The memory limit is set to 15.5GB and the timeout is set to 10 seconds - # (this limits the log file size to roughly <=0.5GB). We redirect - # 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 - 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 <<< "$(find . -name "*.smt2" -type f)" +while read -r file; do + "$DIRNAME/z3.sh" "$file" +done <<< "$(find "$DIRNAME" -name "*.smt2" -type f)" diff --git a/smt2/z3.sh b/smt2/z3.sh new file mode 100755 index 000000000..25b3a93cd --- /dev/null +++ b/smt2/z3.sh @@ -0,0 +1,37 @@ +Z3_VERSION=${Z3_VERSION:-$(z3 --version | sed -E 's/.* ([0-9]+\.[0-9]+\.[0-9]+).*/\1/g')} +Z3_VERSION_REGEX="${Z3_VERSION//./\\.}" + +file_relative="${1#"$(dirname "$0")/"}" +# Check if the first line contains my Z3 version (and skip if it does) +[ "$(sed -n '/^;[^\n]*$Z3_VERSION_REGEX/p;q' "$1")" ] && echo "Skipping \"$file_relative\" as the first line contains \"$Z3_VERSION\"" && exit 0 || true + +# Check if the (non-empty) log file exists +file_hash=$(shasum -a 256 "$0" | cut -d' ' -f1) +base_name="${file_relative%.*}" +log_file_name="$base_name-fHash-$file_hash.log" +log_file_dir=$(dirname "$log_file_name") +mkdir -p $log_file_dir + +# Find files with different hash +old_files=$(find $log_file_dir -name "$(basename "$base_name")-fHash-*.log" -maxdepth 1 -type f) +while read -r old_file; do + [ -n "$old_file" ] || continue + [ "$old_file" = "$log_file_name" ] && continue + echo "Rm old \"$(basename "$old_file")\"" + # Remove old log + rm -f "$old_file" +done <<< "$old_files" +test -s "$log_file_name" && echo "Skipping \"$file_relative\" as \"$file_hash\" exists" && exit 0 || true + +echo "[.log] $file_relative" +# Run Z3 solver for the file and save the log in the '../logs' directory. +# The memory limit is set to 15.5GB and the timeout is set to 10 seconds +# (this limits the log file size to roughly <=0.5GB). We redirect +# 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 "$1" 2>&1) +echo "$output" | grep -q "timeout" || exit 0 +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_relative\""