Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make test runner script a little more resiliant #1117

Merged
merged 6 commits into from
Dec 6, 2024
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
85 changes: 36 additions & 49 deletions tests/run.sh
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
#!/bin/bash
#!/usr/bin/env bash

# Prints usage.
function print_usage {
cat <<EOF
Usage: `basename $0` <DIR> <CMD>
Usage: $(basename "$0") <DIR> <CMD>
with
* <DIR> the test directory
* <CMD> the Kind 2 command to test
Expand All @@ -17,6 +17,19 @@ structured as follows. Directory
EOF
}

# Prints an error taking the lines as argument.
# Exit with exit code 2.
function print_error {
print_usage
echo
echo -e "\033[31mError\033[0m:"
for line in "$@"; do
echo " $line"
done
echo
exit 2
}

# Print usage if asked.
for arg in "$@"; do
if [[ "$arg" = "-h" || "$arg" = "--help" ]]; then
Expand All @@ -25,20 +38,18 @@ for arg in "$@"; do
fi
done

test_dir=`echo "$1" | sed 's:/$::'`
test_dir=$(echo "$1" | sed 's:/$::')

# Make sure folder exists.
if [ ! -d "$test_dir" ]; then
print_error "directory \"$test_dir\" does not exist"
fi

contract_dir="${test_dir}/contracts"

shift
k2_args="$@"
k2_args="$*"

basic_k2_cmd="$k2_args --color false --check_subproperties true --check_sat_assume false --enforce_func_congruence true"
contract_k2_cmd="$basic_k2_cmd --modular true --compositional true"

success_code="0"
falsifiable_code="40"
Expand All @@ -51,20 +62,6 @@ error_dir="error"

tests_ok="true"

# Prints an error taking the lines as argument.
# Exit with exit code 2.
function print_error {
print_usage
echo
echo -e "\033[31mError\033[0m:"
for line in "$@"; do
echo " $line"
done
echo
exit 2
}


# Returns the log file corresponding to a file.
# Simply appends ".log" at the end of the path.
function log_file_of {
Expand All @@ -74,7 +71,7 @@ function log_file_of {

# Returns a string version of an exit code.
function str_of_code {
if [ "$1" -eq "$success_code" ] ; then
if [ "$1" -eq "$success_code" ]; then
echo "success ($success_code)"
elif [ "$1" -eq "$falsifiable_code" ]; then
echo "falsifiable ($falsifiable_code)"
Expand All @@ -86,7 +83,7 @@ function str_of_code {
}

function name_of_path {
echo $1 | sed -e 's:.*/::g'
echo "$1" | sed -e 's:.*/::g'
}

# Runs a test on a file, takes the file path, the expected exit code and the
Expand All @@ -96,23 +93,23 @@ function run_one {
shift
expected_code="$1"
shift
full_kind2_cmd="$@ $file_path"
expected_code_str=`str_of_code "$expected_code"`
full_kind2_cmd="$* $file_path"
expected_code_str=$(str_of_code "$expected_code")

printf "| %-40s ... " "`name_of_path $file_path`"
log_file_path=`log_file_of "$file_path"`
$full_kind2_cmd &> $log_file_path
printf "| %-40s ... " "$(name_of_path "$file_path")"
log_file_path=$(log_file_of "$file_path")
$full_kind2_cmd &>"$log_file_path"
exit_code="$?"
if [ "$exit_code" -ne "$expected_code" ]; then
tests_ok="false"
exit_code_str=`str_of_code "$exit_code"`
exit_code_str=$(str_of_code "$exit_code")
echo -e "\033[31merror\033[0m"
echo -e "\033[31m!\033[0m expected $expected_code_str"
echo -e "\033[31m!\033[0m but got $exit_code_str"
echo -e "\033[31m!\033[0m See log in \"$log_file_path\"."
else
echo -e "\033[32mok\033[0m"
rm $log_file_path
rm "$log_file_path"
fi
}

Expand All @@ -126,28 +123,28 @@ function find_tests {
function run_in {
work_dir="$1"
shift
kind2_cmd="$@"
kind2_cmd="$*"
# Falsifiable
find_cmd=`find_tests $work_dir $falsifiable_dir`
file_count=`eval $find_cmd | wc -l | tr -d ' '`
find_cmd=$(find_tests "$work_dir" $falsifiable_dir)
file_count=$(eval "$find_cmd" | wc -l | tr -d ' ')
echo "| Running \"falsifiable\" ($file_count files)"
for file in `eval $find_cmd`; do
for file in $(eval "$find_cmd"); do
run_one "$file" "$falsifiable_code" "$kind2_cmd"
done

# Success
find_cmd=`find_tests "$work_dir" "$success_dir"`
file_count=`eval $find_cmd | wc -l | tr -d ' '`
find_cmd=$(find_tests "$work_dir" "$success_dir")
file_count=$(eval "$find_cmd" | wc -l | tr -d ' ')
echo "| Running \"success\" ($file_count files)"
for file in `eval $find_cmd`; do
for file in $(eval "$find_cmd"); do
run_one "$file" "$success_code" "$kind2_cmd"
done

# Error
find_cmd=`find_tests $work_dir $error_dir`
file_count=`eval $find_cmd | wc -l | tr -d ' '`
find_cmd=$(find_tests "$work_dir" $error_dir)
file_count=$(eval "$find_cmd" | wc -l | tr -d ' ')
echo "| Running \"error\" ($file_count files)"
for file in `eval $find_cmd`; do
for file in $(eval "$find_cmd"); do
run_one "$file" "$error_code" "$kind2_cmd --lus_strict true"
done
}
Expand All @@ -162,18 +159,8 @@ function run_all {
run_in "$test_dir" "$basic_k2_cmd"
echo "|===| Done."
echo

# echo "|===| Running contract tests."
# echo -e "| > \033[1m$contract_k2_cmd\033[0m"
# echo "|"
# run_in "$contract_dir" "$contract_k2_cmd"
# echo "|===| Done."
# echo
}




# Running tests.
run_all

Expand Down
Loading