From 7bee7e21cda2d025b15aaf9a19193d8f4a52d207 Mon Sep 17 00:00:00 2001
From: Norbert Manthey <nmanthey@conp-solutions.com>
Date: Wed, 12 Jan 2022 23:24:09 +0100
Subject: [PATCH] ci,fuzzing: use modgen

... because this tool allows to generate more difficult
formulas easily.

While touching scripts, also improve ways how to call related tools.

Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
---
 CHANGELOG                   |  1 +
 tools/checker/check-drat.sh |  6 ++++--
 tools/checker/fuzz-drat.sh  | 26 +++++++++++++++++-------
 tools/checker/fuzzcheck.sh  | 40 +++++++++++++++++++++++--------------
 tools/checker/prepare.sh    | 12 +++++------
 tools/checker/toolCheck.sh  |  5 ++++-
 tools/ci.sh                 |  2 +-
 7 files changed, 59 insertions(+), 33 deletions(-)

diff --git a/CHANGELOG b/CHANGELOG
index 47944af4..378a91c0 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -7,6 +7,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [unreleased]
 
+ * testing: use modgen generator during fuzzing runs
  * fix FPU control to compile on ARM
 
 ## [v3.2.1] - 2021-12-20
diff --git a/tools/checker/check-drat.sh b/tools/checker/check-drat.sh
index 964472d8..32f70f2d 100755
--- a/tools/checker/check-drat.sh
+++ b/tools/checker/check-drat.sh
@@ -11,6 +11,8 @@ shift
 # check for file
 [ -f "$f" ] || exit 2
 
+SCRIPT_DIR="$(cd $(dirname "$0") && pwd)"
+
 # static variables
 p=p.proof
 o=drat-minimize-output.txt
@@ -20,11 +22,11 @@ if [ -n "${FUZZ_SOLVER:-}" ]
 then
 	t=$(readlink -e "${FUZZ_SOLVER:-}")
 fi
-d=$(readlink -e drat-trim)
+d=$(readlink -e "$SCRIPT_DIR"/drat-trim)
 
 # run solver
 STATUS=0
-"$t" "$f" -drup-file=$p $@ || STATUS=$?
+$t "$f" -drup-file="$p" $@ || STATUS=$?
 
 if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]
 then
diff --git a/tools/checker/fuzz-drat.sh b/tools/checker/fuzz-drat.sh
index 198ec4bd..e5df79e3 100755
--- a/tools/checker/fuzz-drat.sh
+++ b/tools/checker/fuzz-drat.sh
@@ -8,10 +8,14 @@ TIMEOUT=$2
 
 [ -n "$TIMEOUT" ] || exit 2
 
-c=$(readlink -e cnfuzz)
+SCRIPT_DIR="$(cd $(dirname "$0") && pwd)"
+
+c="$SCRIPT_DIR/modgen"
 
 I=0
-f=input.cnf
+f=fuzz_input.cnf
+declare -i found_sat=0
+declare -i found_unsat=0
 
 FAILED=0
 while true
@@ -19,22 +23,30 @@ do
 	I=$((I+1))
 	[ "$LIMIT" -ge "$I" ] || break
 	# echo "[$SECONDS] run $I ..."
-	$c > $f
+	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" ./check-drat.sh $f &> output.log || STATUS=$?
+	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" input.cnf) seed $(awk '/c seed/ {print $3}' input.cnf)"
-		mv input.cnf input.$I.cnf
+		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"
 [ "$FAILED" -eq 0 ] || exit 1
 exit 0
diff --git a/tools/checker/fuzzcheck.sh b/tools/checker/fuzzcheck.sh
index de603c92..c044aa30 100755
--- a/tools/checker/fuzzcheck.sh
+++ b/tools/checker/fuzzcheck.sh
@@ -7,19 +7,19 @@
 prg=$1
 
 # this can be initialized to a max. size of an unreduced buggy formula
-bestcls=5000
+bestcls=50000
 
-cnf=/tmp/runcnfuzz-$$.cnf
-sol=/tmp/runcnfuzz-$$.sol
-err=/tmp/runcnfuzz-$$.err
-out=/tmp/runcnfuzz-$$.out
-log=runcnfuzz-$$.log
+cnf=/dev/shm/uzz-$$.cnf
+sol=/dev/shm/fuzz-$$.sol
+err=/dev/shm/fuzz-$$.err
+out=/dev/shm/fuzz-$$.out
+log=fuzz-$$.log
 rm -f $log $cnf $sol
-echo "[runcnfuzz] running $prg"
-echo "[runcnfuzz] logging $log"
+echo "[fuzz] running $prg"
+echo "[fuzz] logging $log"
 echo "run $1 $2" > $log
-echo "[runcnfuzz] run with pid $$"
-echo "[runcnfuzz] started at $(date)"
+echo "[fuzz] run with pid $$"
+echo "[fuzz] started at $(date)"
 i=0
 
 # set limit for number of instances to be solved
@@ -31,11 +31,19 @@ fi
 test=0
 
 declare -i status=0
+declare -i found_sat=0
+declare -i found_unsat=0
 
 while [ "$test" -lt "$limit" ]
 do
   rm -f $cnf; 
-  ./cnfuzz $CNFUZZOPTIONS > $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`"
@@ -68,9 +76,11 @@ do
       continue
       ;;
     10)
+      found_sat=$((found_sat+1))
       continue
       ;;
     20)
+      found_unsat=$((found_unsat+1))
       continue
       ;;
     15)
@@ -82,8 +92,8 @@ do
   status=1
 
   head="`awk '/p cnf /{print $3, $4}' $cnf`"
-  echo "($SECONDS s) [runcnfuzz] bug-$seed $head             with exit code $res"
-  echo "($SECONDS s) To reproduce, run cnfuzz: './cnfuzz $seed > reproduce.cnf' and '$prg reproduce.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
@@ -111,12 +121,12 @@ do
 
   if [ -f "$red" ]; then
     head="`awk '/p cnf /{print $3, $4}' $red`"
-    echo "($SECONDS s) [runcnfuzz] $red $head"
+    echo "($SECONDS s) [fuzz] $red $head"
   fi
   # rm -f $bug
 done
 
-echo "($SECONDS s) "
+echo "($SECONDS s) sat: $found_sat unsat: $found_unsat"
 echo "($SECONDS s) did $test out of $limit tests"
 
 exit $status
diff --git a/tools/checker/prepare.sh b/tools/checker/prepare.sh
index 4daf62ec..0c7a5d9b 100755
--- a/tools/checker/prepare.sh
+++ b/tools/checker/prepare.sh
@@ -1,6 +1,6 @@
 #!/bin/bash
 #
-# This script sets up the checker environment (install drat-trim as well as cnfuzz)
+# This script sets up the checker environment (install drat-trim as well as modgen)
 
 # exits the script immediately if a command exits with a non-zero status
 set -e
@@ -19,12 +19,10 @@ else
 	git clone https://github.com/marijnheule/drat-trim.git drat-trim-src
 fi
 
-# get fuzz tools
-curl http://fmv.jku.at/cnfuzzdd/cnfuzzdd2013.zip > fuzz-suite.zip
-
-# build cnfuzz
-unzip -j -n fuzz-suite.zip cnfuzzdd2013/cnfuzz.c -d .
-gcc -o cnfuzz cnfuzz.c -Wall -O0 -lrt
+# get and build modgen
+git clone --depth=1 git@github.com:conp-solutions/modularityGen.git modgen-src
+make -C modgen-src
+cp modgen-src/modgen .
 
 # build drat-trim
 pushd drat-trim-src
diff --git a/tools/checker/toolCheck.sh b/tools/checker/toolCheck.sh
index 11644ce7..fe980211 100755
--- a/tools/checker/toolCheck.sh
+++ b/tools/checker/toolCheck.sh
@@ -1,3 +1,6 @@
+#!/bin/bash
+
+SCRIPT_DIR="$(cd $(dirname "$0") && pwd)"
 rm -f /tmp/verify_$$.cnf
 
 #echo "run $1 with $2" >> tmp.dat
@@ -18,7 +21,7 @@ fi
 # cat /tmp/verify.cnf
 if [ "$status" -eq "10" ]
 then
-	./verify SAT /tmp/verify_$$.cnf $2 # 2>&1 > /dev/null
+	"$SCRIPT_DIR"/verify SAT /tmp/verify_$$.cnf $2 # 2>&1 > /dev/null
 	vstat=$?
 
 	if [ "$vstat" -eq "1" ]
diff --git a/tools/ci.sh b/tools/ci.sh
index 92e52d59..8d2a9ab2 100755
--- a/tools/ci.sh
+++ b/tools/ci.sh
@@ -37,7 +37,7 @@ test_fuzzing ()
 
     # Perform a basic run, and forward its exit code
     echo "Solve and check $FUZZ_ROUNDS formulas with a 5s timeout"
-    ./fuzz-drat.sh $FUZZ_ROUNDS 5 || STATUS=$?
+    ./fuzz-drat.sh $FUZZ_ROUNDS 15 || STATUS=$?
 
     echo "Fuzz diversity rank configurations ..."
     ./fuzz-check-configurations.sh || STATUS=$?