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

Check parallel #488

Merged
merged 15 commits into from
Feb 21, 2024
4 changes: 2 additions & 2 deletions Makefile.build
Original file line number Diff line number Diff line change
Expand Up @@ -309,14 +309,14 @@ regress: build_subdirs version
@ echo "=== Building binaries ==="
@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) bin
@ echo "=== Running regressions ==="
@ $(regressdir)/check.sh $(regressdir) $(build_dir)/bin
+@ $(regressdir)/check.sh $(regressdir) $(build_dir)/bin


static-regress: static_build_subdirs version
@ echo "=== Building binaries ==="
@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) static-bin
@ echo "=== Running regressions ==="
@ $(regressdir)/check.sh $(regressdir) $(build_dir)/static_bin
@ $(regressdir)/check.sh -j $(regressdir) $(build_dir)/static_bin


.PHONY: all obj static-obj lib static-lib bin static-bin test static-test \
Expand Down
2 changes: 1 addition & 1 deletion configure.ac
Original file line number Diff line number Diff line change
Expand Up @@ -578,7 +578,7 @@ if test -z "$1"; then
if test -f $ldir/libgmp.a; then
AC_MSG_RESULT(found)
testlib=$ldir/libgmp.a
CSL_CHECK_GMP($testlib,$testincludedir)
CSL_CHECK_GMP($testlib,$testincludedir)
if test $run_ok = yes; then
STATIC_GMP=$testlib
STATIC_GMP_INCLUDE_DIR=$testincludedir
Expand Down
239 changes: 100 additions & 139 deletions tests/regress/check.sh
Original file line number Diff line number Diff line change
Expand Up @@ -38,17 +38,25 @@ usage() {
echo "Usage: $0 <test-directory> <bin-directory> [test1] [test2] ..."
exit
}


cleanup() {
[[ -n "$logdir" ]] && rm -rf "$logdir"
}

smt2_options=
j_option=

while getopts "s:" o; do
while getopts "js:" o; do
case "$o" in
s)
smt2_options=${OPTARG}
;;
*)
usage
;;
s)
smt2_options=${OPTARG}
;;
j)
j_option=yes
;;
*)
usage
;;
esac
done
shift $((OPTIND-1))
Expand All @@ -62,13 +70,10 @@ bin_dir=$2
shift 2
all_tests="$@"

# Make sure fatal errors go to stderr
export LIBC_FATAL_STDERR_=1

#
# System-dependent configuration
#
os_name=`uname 2>/dev/null` || os_name=unknown
os_name=$(uname 2>/dev/null) || os_name=unknown

case "$os_name" in
*Darwin* )
Expand All @@ -81,165 +86,121 @@ case "$os_name" in

esac

#
# We try bash's builtin time command
#
TIMEFORMAT="%U"


#
# Output colors
#
red=
green=
black=
if test -t 1 ; then
red=`tput setaf 1`
green=`tput setaf 2`
black=`tput sgr0`
parallel_tool=
if command -v parallel &> /dev/null ; then
if parallel --version 2>&1 | grep GNU > /dev/null 2>&1 ; then
parallel_tool="gnu"
else
parallel_tool="more"
fi
fi

#
# The temp file for output
#
outfile=`$mktemp_cmd` || { echo "Can't create temp file" ; exit 1 ; }
timefile=`$mktemp_cmd` || { echo "Can't create temp file" ; exit 1 ; }

fail=0
pass=0

failed_tests=()
trap cleanup EXIT
logdir=$($mktemp_cmd -d) || { echo "Can't create temp folder" ; exit 1 ; }

if [[ -z "$REGRESS_FILTER" ]];
then
REGRESS_FILTER="."
REGRESS_FILTER="."
fi

if [[ -z "$TIME_LIMIT" ]];
then
TIME_LIMIT=60
fi


#
# Check if MCSAT is supported
#
./$bin_dir/yices_smt2 --mcsat >& /dev/null < /dev/null
./"$bin_dir"/yices_smt2 --mcsat >& /dev/null < /dev/null
if [ $? -ne 0 ]
then
MCSAT_FILTER="-v mcsat"
else
MCSAT_FILTER="."
fi

if test -z "$all_tests"; then
if [ -z "$all_tests" ] ; then
all_tests=$(
find "$regress_dir" -name '*.smt' -or -name '*.smt2' -or -name '*.ys' |
grep $REGRESS_FILTER | grep $MCSAT_FILTER |
sort
find "$regress_dir" -name '*.smt' -or -name '*.smt2' -or -name '*.ys' |
grep $REGRESS_FILTER | grep $MCSAT_FILTER |
sort
)
fi

for file in $all_tests; do

echo -n $file

# Get the binary based on the filename
filename=`basename "$file"`

options=

case $filename in
*.smt2)
binary=yices_smt2
options=$smt2_options
;;
*.smt)
binary=yices_smtcomp
;;
*.ys)
binary=yices
;;
*)
echo FAIL: unknown extension for $filename
fail=`expr $fail + 1`
continue
esac
if [ -t 1 ] ; then
color_flag="-c"
fi

# Get the options
if [ -e "$file.options" ]
then
options="$options `cat $file.options`"
echo " [ $options ]"
test_string="$file [ $options ]"
else
test_string="$file"
echo
fi
# job_count 1: serial execution, 0: unrestricted parallel, n>1: n processes
job_count=1

#check if we are in a make run with -j N
if [[ -n "$j_option" ]]; then
job_count=0
elif [[ "$MAKEFLAGS" =~ --jobserver-(fds|auth)=([0-9]+),([0-9]+) ]]; then
# greedy get as many tokens as possible
fdR=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-(fds\|auth)=([0-9]+),([0-9]+).*|\2|")
fdW=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-(fds\|auth)=([0-9]+),([0-9]+).*|\3|")
while IFS= read -r -d '' -t 1 -n 1 <&"$fdR"; do
job_count=$((job_count+1))
done
elif [[ "$MAKEFLAGS" =~ --jobserver-auth=fifo:([^ ]+) ]]; then
fifo=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-auth=fifo:([^ ]+).*|\1|")
while IFS= read -r -d '' -t 1 -n 1 <"$fifo"; do
job_count=$((job_count+1))
done
elif [[ "$MAKEFLAGS" =~ (^|[ ])-?j($|[ ]) ]]; then
job_count=0
fi

# Get the expected result
if [ -e "$file.gold" ]
then
gold=$file.gold
else
echo -n $red
echo FAIL: missing file: $file.gold
echo -n $black
fail=`expr $fail + 1`
failed_tests+=("$test_string")
continue
fi
if [[ $job_count != 1 ]] && [[ -z "$parallel_tool" ]]; then
echo "**********************************************************"
echo "Install moreutils or GNU parallel to run tests in parallel"
echo "**********************************************************"
else
case $job_count in
0) echo "Running in parallel";;
1) echo "Running sequentially";;
*) echo "Running with $job_count parallel jobs";;
esac
fi

# Run the binary
(
ulimit -S -t $TIME_LIMIT &> /dev/null
ulimit -H -t $((1+$TIME_LIMIT)) &> /dev/null
(time ./$bin_dir/$binary $options ./$file >& $outfile ) >& $timefile
)
status=$?
thetime=`cat $timefile`

# Do the diff
DIFF=`diff -w $outfile $gold`

if [ $? -eq 0 ] && [ $status -eq 0 ]
then
echo -n $green
echo PASS [${thetime} s]
echo -n $black
pass=`expr $pass + 1`
else
echo -n $red
echo FAIL
echo -n $black
fail=`expr $fail + 1`
failed_tests+=("$test_string"$'\n'"$DIFF")
fi
j_param="-j$job_count"
if [[ $job_count == 0 ]]; then j_param=""; fi

case "$parallel_tool" in
more)
parallel -i $j_param bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- $all_tests
;;
gnu)
parallel -q $j_param bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" ::: $all_tests
;;
*)
for file in $all_tests; do
bash "${BASH_SOURCE%/*}"/run_test.sh $color_flag -s "$smt2_options" "$file" "$bin_dir" "$logdir"
done
;;
esac

# give back tokens
while [[ $job_count -gt 1 ]]; do
[[ -n $fdW ]] && echo -n '+' >&"$fdW"
[[ -n $fifo ]] && echo -n '+' >"$fifo"
job_count=$((job_count-1))
done

rm $outfile
rm $timefile
pass=$(find "$logdir" -type f -name "*.pass" | wc -l)
fail=$(find "$logdir" -type f -name "*.error" | wc -l)

if [ $fail -eq 0 ]
then
echo -n $green
echo Pass: $pass
echo Fail: $fail
echo -n $black
else
echo -n $red
echo Pass: $pass
echo Fail: $fail
echo -n $black
fi
echo "Pass: $pass"
echo "Fail: $fail"

if [ $fail -eq 0 ]
then
exit 0
if [ "$fail" -eq 0 ] ; then
code=0
else
for i in "${!failed_tests[@]}"; do echo "$((i+1)). ${failed_tests[$i]}"; done
exit 1
for f in "$logdir"/*.error ; do
cat "$f"
echo
done
code=1
fi

echo -n $black
exit $code
Loading
Loading