Check parallel

Makefile.build

@@ -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 -j $(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 \

configure.ac

@@ -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

tests/regress/check.sh

@@ -38,17 +38,21 @@ usage() {
    echo "Usage: $0 <test-directory> <bin-directory> [test1] [test2] ..."
    exit
 }
-    
+
 smt2_options=
+use_parallel=
 
-while getopts "s:" o; do
+while getopts "js:" o; do
     case "$o" in
-	s)
-	    smt2_options=${OPTARG}
-	    ;;
-	*)
-	    usage
-	    ;;
+    s)
+      smt2_options=${OPTARG}
+      ;;
+    j)
+      use_parallel=yes
+      ;;
+    *)
+      usage
+      ;;
     esac
 done
 shift $((OPTIND-1))
@@ -62,13 +66,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* )
@@ -81,165 +82,83 @@ 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`
-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=()
+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
-
-    # 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
-
-    # Get the expected result
-    if [ -e "$file.gold" ]
-    then
-        gold=$file.gold
+run_parallel="no"
+if [ -n "$use_parallel" ] ; then
+    if command -v parallel &> /dev/null ; then
+        if parallel --version 2>&1 | grep GNU > /dev/null 2>&1 ; then
+            run_parallel="gnu"
+        else
+            run_parallel="more"
+        fi
     else
-        echo -n $red
-        echo FAIL: missing file: $file.gold
-        echo -n $black
-        fail=`expr $fail + 1`
-        failed_tests+=("$test_string")
-        continue
+        echo "****************************************************************"
+        echo "HINT: Install moreutils or GNU parallel to run tests in parallel"
+        echo "****************************************************************"
     fi
+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
+if [ -t 1 ] ; then
+  color_flag="-c"
+fi
 
-done
+case "$run_parallel" in
+    more)
+        parallel -i bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- $all_tests
+        ;;
+    gnu)
+        parallel -q 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
 
-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
+rm -rf "$logdir"
+exit $code