From f96d1b09f245965f35e63900c2ba6bca79ac4822 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Fri, 14 Jan 2022 22:55:36 +0100 Subject: [PATCH] ci,tests: format scripts Apply formatting. Signed-off-by: Norbert Manthey --- tools/checker/check-drat.sh | 29 +++--- tools/checker/fuzz-drat.sh | 50 +++++------ tools/checker/fuzzcheck.sh | 171 +++++++++++++++++------------------- tools/checker/prepare.sh | 17 ++-- tools/checker/toolCheck.sh | 87 ++++++++---------- tools/ci.sh | 9 +- 6 files changed, 168 insertions(+), 195 deletions(-) diff --git a/tools/checker/check-drat.sh b/tools/checker/check-drat.sh index 32f70f2d..dae73b6a 100755 --- a/tools/checker/check-drat.sh +++ b/tools/checker/check-drat.sh @@ -18,9 +18,8 @@ p=p.proof o=drat-minimize-output.txt t=$(readlink -e ../../build/release/bin/mergesat) # allow to override the solver location via environment variable -if [ -n "${FUZZ_SOLVER:-}" ] -then - t=$(readlink -e "${FUZZ_SOLVER:-}") +if [ -n "${FUZZ_SOLVER:-}" ]; then + t=$(readlink -e "${FUZZ_SOLVER:-}") fi d=$(readlink -e "$SCRIPT_DIR"/drat-trim) @@ -28,24 +27,22 @@ d=$(readlink -e "$SCRIPT_DIR"/drat-trim) STATUS=0 $t "$f" -drup-file="$p" $@ || STATUS=$? -if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ] -then - echo "unexpected status code $STATUS" - exit $STATUS +if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]; then + echo "unexpected status code $STATUS" + exit $STATUS fi # exclude trivial unsat grep "^0$" $f && exit 0 # run the check -if [ "$STATUS" -ne 20 ] -then +if [ "$STATUS" -ne 20 ]; then exit $STATUS fi # verify binary proof format VERIFY_STATUS=0 -$d $f $p -v -v -n &> $o || exit $VERIFY_STATUS +$d $f $p -v -v -n &>$o || exit $VERIFY_STATUS echo "verify status: $VERIFY_STATUS" # for now, don't be too strict # grep " does not occur: " $o && exit 3 @@ -54,24 +51,22 @@ exit 20 # re-run with plain proof format "$t" "$f" -drup-file=$p -no-binary-proof $@ || STATUS=$? -if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ] -then - echo "unexpected status code $STATUS" - exit $STATUS +if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]; then + echo "unexpected status code $STATUS" + exit $STATUS fi # exclude trivial unsat grep "^0$" $f && exit 0 # run the check -if [ "$STATUS" -ne 20 ] -then +if [ "$STATUS" -ne 20 ]; then exit $STATUS fi # verify binary proof format VERIFY_STATUS=0 -$d $f $p -v -v -n &> $o || exit $VERIFY_STATUS +$d $f $p -v -v -n &>$o || exit $VERIFY_STATUS echo "verify status: $VERIFY_STATUS" # for now, don't be too strict # grep " does not occur: " $o && exit 3 diff --git a/tools/checker/fuzz-drat.sh b/tools/checker/fuzz-drat.sh index e5df79e3..abb2c2bb 100755 --- a/tools/checker/fuzz-drat.sh +++ b/tools/checker/fuzz-drat.sh @@ -18,33 +18,31 @@ declare -i found_sat=0 declare -i found_unsat=0 FAILED=0 -while true -do - I=$((I+1)) - [ "$LIMIT" -ge "$I" ] || break - # echo "[$SECONDS] run $I ..." - seed="$(echo $(($(date +%s%N)/1000000)))" - cls="" - while [ -z "$cls" ]; do - cls="$(bash -c 'echo $((9000 + $(date +%4N) ))' 2> /dev/null)" - done - modgen_cli_args="-s $seed -n 3500 -m $cls" - $c $modgen_cli_args > $f - STATUS=0 - timeout "$TIMEOUT" "$SCRIPT_DIR"/check-drat.sh $f &> output.log || STATUS=$? - # ignore time outs - [ "$STATUS" -ne 124 ] || continue +while true; do + I=$((I + 1)) + [ "$LIMIT" -ge "$I" ] || break + # echo "[$SECONDS] run $I ..." + seed="$(echo $(($(date +%s%N) / 1000000)))" + cls="" + while [ -z "$cls" ]; do + cls="$(bash -c 'echo $((9000 + $(date +%4N) ))' 2>/dev/null)" + done + modgen_cli_args="-s $seed -n 3500 -m $cls" + $c $modgen_cli_args >$f + STATUS=0 + timeout "$TIMEOUT" "$SCRIPT_DIR"/check-drat.sh $f &>output.log || STATUS=$? + # ignore time outs + [ "$STATUS" -ne 124 ] || continue - # make failures permanent - if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ] - then - echo "[$SECONDS] failed for try $I with status $STATUS and header $(grep "p cnf" $f) and generator: $c $modgen_cli_args" - mv $f fuzz_input.$I.cnf - mv output.log output.$I.log - FAILED=$((FAILED+1)) - fi - [ "$STATUS" -eq 10 ] && found_sat=$((found_sat+1)) - [ "$STATUS" -eq 20 ] && found_unsat=$((found_unsat+1)) + # make failures permanent + if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]; then + echo "[$SECONDS] failed for try $I with status $STATUS and header $(grep "p cnf" $f) and generator: $c $modgen_cli_args" + mv $f fuzz_input.$I.cnf + mv output.log output.$I.log + FAILED=$((FAILED + 1)) + fi + [ "$STATUS" -eq 10 ] && found_sat=$((found_sat + 1)) + [ "$STATUS" -eq 20 ] && found_unsat=$((found_unsat + 1)) done echo "failed $FAILED out of $LIMIT" echo "($SECONDS s) sat: $found_sat unsat: $found_unsat" diff --git a/tools/checker/fuzzcheck.sh b/tools/checker/fuzzcheck.sh index c044aa30..c2c51408 100755 --- a/tools/checker/fuzzcheck.sh +++ b/tools/checker/fuzzcheck.sh @@ -17,16 +17,15 @@ log=fuzz-$$.log rm -f $log $cnf $sol echo "[fuzz] running $prg" echo "[fuzz] logging $log" -echo "run $1 $2" > $log +echo "run $1 $2" >$log echo "[fuzz] run with pid $$" echo "[fuzz] started at $(date)" i=0 # set limit for number of instances to be solved limit=1 -if [ "x$2" != "x" ] -then - limit=$2 +if [ "x$2" != "x" ]; then + limit=$2 fi test=0 @@ -34,96 +33,90 @@ declare -i status=0 declare -i found_sat=0 declare -i found_unsat=0 -while [ "$test" -lt "$limit" ] -do - rm -f $cnf; - seed="$(echo $(($(date +%s%N)/1000000)))" - cls="" - while [ -z "$cls" ]; do - cls="$(bash -c 'echo $((6000 + $(date +%4N) ))' 2> /dev/null)" - done - modgen_cli_args="-s $seed -n 2800 -m $cls" - ./modgen $modgen_cli_args > $cnf - # control whether algorithm should sleep - seed=`grep 'c seed' $cnf|head -1|awk '{print $NF}'` - head="`awk '/p cnf /{print $3, $4}' $cnf`" - [ -n "${VERBOSE_FUZZING:-}" ] && printf "%d %16d %6d %6d \r" "$i" "$seed" $head - i=`expr $i + 1` - rm -f $sol - - # set limit for number of instances to be solved - if [ "x$2" != "x" ] - then - test=$(($test+1)) - fi - - thiscls=`awk '/p cnf /{print $4}' $cnf` - if [ $bestcls -ne "-1" ] - then - if [ $bestcls -le $thiscls ] - then - continue +while [ "$test" -lt "$limit" ]; do + rm -f $cnf + seed="$(echo $(($(date +%s%N) / 1000000)))" + cls="" + while [ -z "$cls" ]; do + cls="$(bash -c 'echo $((6000 + $(date +%4N) ))' 2>/dev/null)" + done + modgen_cli_args="-s $seed -n 2800 -m $cls" + ./modgen $modgen_cli_args >$cnf + # control whether algorithm should sleep + seed=$(grep 'c seed' $cnf | head -1 | awk '{print $NF}') + head="$(awk '/p cnf /{print $3, $4}' $cnf)" + [ -n "${VERBOSE_FUZZING:-}" ] && printf "%d %16d %6d %6d \r" "$i" "$seed" $head + i=$(expr $i + 1) + rm -f $sol + + # set limit for number of instances to be solved + if [ "x$2" != "x" ]; then + test=$(($test + 1)) + fi + + thiscls=$(awk '/p cnf /{print $4}' $cnf) + if [ "$bestcls" -ne "-1" ]; then + if [ "$bestcls" -le "$thiscls" ]; then + continue + fi fi - fi - ./toolCheck.sh $prg $cnf > $out 2> $err - res=$? -# echo "result $res" - case $res in + ./toolCheck.sh $prg $cnf >$out 2>$err + res=$? + # echo "result $res" + case $res in 124) - echo "($SECONDS s) timeout with $seed" > $log - mv $cnf timeout-$seed.cnf - continue - ;; + echo "($SECONDS s) timeout with $seed" >$log + mv $cnf timeout-$seed.cnf + continue + ;; 10) - found_sat=$((found_sat+1)) - continue - ;; + found_sat=$((found_sat + 1)) + continue + ;; 20) - found_unsat=$((found_unsat+1)) - continue - ;; - 15) - ;; - 25) - ;; - esac - - status=1 - - head="`awk '/p cnf /{print $3, $4}' $cnf`" - echo "($SECONDS s) [fuzz] bug-$seed $head with exit code $res" - echo "($SECONDS s) To reproduce, run modgen: './modgen $modgen_cli_args > reproduce.cnf' and '$prg reproduce.cnf'" - echo $seed >> $log - echo "($SECONDS s) out" - cat $out - echo "($SECONDS s) err" - cat $err - - # - # consider only bugs that are smaller then the ones we found already - # - if [ $bestcls -eq "-1" ] - then - bestcls=$thiscls - echo "($SECONDS s) init bestcls with $bestcls" - elif [ $bestcls -le $thiscls ] - then - echo "($SECONDS s) reject new bug with $thiscls clauses" - continue - fi - - bestcls=$thiscls # store better clause count! - echo "($SECONDS s) set bestcls to $bestcls" - red=red-$seed.cnf - bug=bug-$seed.cnf - mv $cnf $bug - - if [ -f "$red" ]; then - head="`awk '/p cnf /{print $3, $4}' $red`" - echo "($SECONDS s) [fuzz] $red $head" - fi - # rm -f $bug + found_unsat=$((found_unsat + 1)) + continue + ;; + 15) ;; + + 25) ;; + + esac + + status=1 + + head="$(awk '/p cnf /{print $3, $4}' $cnf)" + echo "($SECONDS s) [fuzz] bug-$seed $head with exit code $res" + echo "($SECONDS s) To reproduce, run modgen: './modgen $modgen_cli_args > reproduce.cnf' and '$prg reproduce.cnf'" + echo $seed >>$log + echo "($SECONDS s) out" + cat $out + echo "($SECONDS s) err" + cat $err + + # + # consider only bugs that are smaller then the ones we found already + # + if [ "$bestcls" -eq "-1" ]; then + bestcls=$thiscls + echo "($SECONDS s) init bestcls with $bestcls" + elif [ "$bestcls" -le $thiscls ]; then + echo "($SECONDS s) reject new bug with $thiscls clauses" + continue + fi + + bestcls="$thiscls" # store better clause count! + echo "($SECONDS s) set bestcls to $bestcls" + red=red-$seed.cnf + bug=bug-$seed.cnf + mv $cnf $bug + + if [ -f "$red" ]; then + head="$(awk '/p cnf /{print $3, $4}' $red)" + echo "($SECONDS s) [fuzz] $red $head" + fi + # rm -f $bug done echo "($SECONDS s) sat: $found_sat unsat: $found_unsat" diff --git a/tools/checker/prepare.sh b/tools/checker/prepare.sh index 0c7a5d9b..b19177d8 100755 --- a/tools/checker/prepare.sh +++ b/tools/checker/prepare.sh @@ -6,21 +6,20 @@ set -e # directory of this script (in repo/scripts) -script_dir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd ) +script_dir=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd) # get drat-trim -if [ -d drat-trim-src ] -then - pushd drat-trim-src - git fetch origin - git checkout origin/master - popd +if [ -d drat-trim-src ]; then + pushd drat-trim-src + git fetch origin + git checkout origin/master + popd else - git clone https://github.com/marijnheule/drat-trim.git drat-trim-src + git clone https://github.com/marijnheule/drat-trim.git drat-trim-src fi # get and build modgen -git clone --depth=1 git@github.com:conp-solutions/modularityGen.git modgen-src +git clone --depth=1 https://github.com/conp-solutions/modularityGen.git modgen-src make -C modgen-src cp modgen-src/modgen . diff --git a/tools/checker/toolCheck.sh b/tools/checker/toolCheck.sh index fe980211..9e373014 100755 --- a/tools/checker/toolCheck.sh +++ b/tools/checker/toolCheck.sh @@ -5,71 +5,62 @@ rm -f /tmp/verify_$$.cnf #echo "run $1 with $2" >> tmp.dat -timeout 10 $1 $2 > /tmp/verify_$$.cnf 2> /tmp/verify2_$$.cnf; +timeout 10 $1 $2 >/tmp/verify_$$.cnf 2>/tmp/verify2_$$.cnf status=$? # sleep 0.01 #echo "finish with state= $status" >> tmp.dat -if [ "$status" -eq "124" ] -then - # we got a timeout here! - rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf - exit 124 +if [ "$status" -eq "124" ]; then + # we got a timeout here! + rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf + exit 124 fi # cat /tmp/verify.cnf -if [ "$status" -eq "10" ] -then - "$SCRIPT_DIR"/verify SAT /tmp/verify_$$.cnf $2 # 2>&1 > /dev/null - vstat=$? +if [ "$status" -eq "10" ]; then + "$SCRIPT_DIR"/verify SAT /tmp/verify_$$.cnf $2 # 2>&1 > /dev/null + vstat="$?" - if [ "$vstat" -eq "1" ] - then - rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf - exit 10 - else - echo "solver out:" - cat /tmp/verify_$$.cnf - echo "solver err:" - cat /tmp/verify2_$$.cnf - rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf - exit 15 - fi + if [ "$vstat" -eq "1" ]; then + rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf + exit 10 + else + echo "solver out:" + cat /tmp/verify_$$.cnf + echo "solver err:" + cat /tmp/verify2_$$.cnf + rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf + exit 15 + fi else - # if the instance is unsatisfiable or another error occurred, report it -# echo "exit with $status" >> tmp.dat - + # if the instance is unsatisfiable or another error occurred, report it + # echo "exit with $status" >> tmp.dat - if [ "$status" -ne "20" ] - then - echo "solver output:" - cat /tmp/verify_$$.cnf /tmp/verify2_$$.cnf - rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf - exit $status - fi + if [ "$status" -ne "20" ]; then + echo "solver output:" + cat /tmp/verify_$$.cnf /tmp/verify2_$$.cnf + rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf + exit $status + fi + timeout 30 picosat $2 2>/dev/null 1>/dev/null + lstat=$? - timeout 30 picosat $2 2> /dev/null 1> /dev/null - lstat=$? - - if [ "$status" -eq "124" ] - then + if [ "$status" -eq "124" ]; then # we got a timeout here! - mkdir -p picosatTimeout # collect instances where lingeling performs badly + mkdir -p picosatTimeout # collect instances where lingeling performs badly mv $2 picosatTimeout - rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf + rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf exit 124 - fi + fi - if [ $lstat -ne "20" ] - then - echo "solver output:" - cat /tmp/verify_$$.cnf /tmp/verify2_$$.cnf - rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf - exit 25 - fi + if [ $lstat -ne "20" ]; then + echo "solver output:" + cat /tmp/verify_$$.cnf /tmp/verify2_$$.cnf + rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf + exit 25 + fi rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf exit 20 fi - diff --git a/tools/ci.sh b/tools/ci.sh index 8d2a9ab2..dbd31eed 100755 --- a/tools/ci.sh +++ b/tools/ci.sh @@ -27,8 +27,7 @@ CHECKERDIR=$(readlink -e tools/checker) STATUS=0 -test_fuzzing () -{ +test_fuzzing() { # Enter checker repository pushd tools/checker @@ -51,8 +50,7 @@ if [ $TESTFUZZ -eq 1 ]; then echo "[$SECONDS s] end fuzzing" fi -test_diversify () -{ +test_diversify() { # Enter checker repository pushd tools/checker @@ -83,8 +81,7 @@ STATIC_LIB=$(readlink -e build/release/lib/libmergesat.a) MERGEZIP=$(ls MergeSAT*.zip | sort -V | tail -n 1) MERGEZIP=$(readlink -e $MERGEZIP) -test_starexec () -{ +test_starexec() { [ $CLEANUP -eq 0 ] || trap 'rm -rf $TMPD' EXIT TMPD=$(mktemp -d)