AE sort out and updates

picus-dpvl-uniqueness.rkt

@@ -20,6 +20,7 @@
 (define arg-selector "counter")
 (define arg-precondition null)
 (define arg-prop #t)
+(define arg-slv #t)
 (define arg-smt #f)
 (define arg-weak #f)
 (define arg-map #f)
@@ -51,6 +52,9 @@
     [("--noprop") "disable propagation (default: false / propagation on)"
         (set! arg-prop #f)
     ]
+    [("--nosolve") "disable solver phase (default: false / solver on)"
+        (set! arg-slv #f)
+    ]
     [("--smt") "show path to generated smt files (default: false)"
         (set! arg-smt #t)
     ]
@@ -66,7 +70,8 @@
 (printf "# solver: ~a\n" arg-solver)
 (printf "# selector: ~a\n" arg-selector)
 (printf "# precondition: ~a\n" arg-precondition)
-(printf "# propagation: ~a\n" arg-prop)
+(printf "# propagation on: ~a\n" arg-prop)
+(printf "# solver on: ~a\n" arg-slv)
 (printf "# smt: ~a\n" arg-smt)
 (printf "# weak: ~a\n" arg-weak)
 (printf "# map: ~a\n" arg-map)
@@ -155,7 +160,7 @@
     xlist opts defs cnsts
     alt-xlist alt-defs alt-cnsts
     unique-set precondition ; prior knowledge row
-    arg-selector arg-prop arg-timeout arg-smt arg-map path-sym
+    arg-selector arg-prop arg-slv arg-timeout arg-smt arg-map path-sym
     solve state-smt-path interpret-r1cs
     parse-r1cs optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1
 ))

picus/algorithms/cex.rkt

@@ -112,7 +112,7 @@
             xlist opts defs icnsts
             alt-xlist alt-defs ialt-cnsts
             unique-set precondition ; prior knowledge row
-            arg-selector arg-prop arg-timeout arg-smt path-sym
+            arg-selector arg-prop #t arg-timeout arg-smt #f path-sym
             solve state-smt-path interpret-r1cs
             parse-r1cs optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1
             #:extcnsts (model2cnsts partial-model)

picus/algorithms/dpvl.rkt

@@ -61,6 +61,7 @@
 
 (define :arg-selector null)
 (define :arg-prop null)
+(define :arg-slv null)
 (define :arg-timeout null)
 (define :arg-smt null)
 (define :arg-map null)
@@ -269,7 +270,12 @@
         [else
             ; still there's unknown target signal, continue
             ; then select and solve
-            (define-values (s0 xnew-ks xnew-us info) (dpvl-select-and-solve new-ks new-us new-us))
+            (define-values (s0 xnew-ks xnew-us info) (if :arg-slv
+                ; do solver phase
+                (dpvl-select-and-solve new-ks new-us new-us)
+                ; don't do solver phase
+                (values 'normal new-ks new-us null)
+            ))
             (cond
                 ; normal means there's no counter-example
                 [(equal? 'normal s0)
@@ -342,7 +348,7 @@
     xlist opts defs cnsts
     alt-xlist alt-defs alt-cnsts
     unique-set precondition
-    arg-selector arg-prop arg-timeout arg-smt arg-map path-sym
+    arg-selector arg-prop arg-slv arg-timeout arg-smt arg-map path-sym
     solve state-smt-path interpret-r1cs
     parse-r1cs optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1
     ; extra constraints, usually from cex module about partial model
@@ -371,6 +377,7 @@
 
     (set! :arg-selector arg-selector)
     (set! :arg-prop arg-prop)
+    (set! :arg-slv arg-slv)
     (set! :arg-timeout arg-timeout)
     (set! :arg-smt arg-smt)
     (set! :arg-map arg-map)

resources/Dockerfile@base

@@ -29,6 +29,9 @@ RUN add-apt-repository -y ppa:plt/racket && \
     apt-get update && \
     apt-get install -y racket libssl-dev curl && \
     raco pkg install --auto rosette && \
+    raco pkg install --auto csv-reading && \
+    raco pkg install --auto graph && \
+    raco pkg install --auto math-lib && \
     apt-get clean && \
     rm -rf /var/lib/apt/lists/*
 

scripts/batch-run-picus-noprop.sh

@@ -0,0 +1,27 @@
+#!/bin/bash
+# usage: this.sh <timeout:seconds> <log_path> <target_folder>
+# example: ./batch-run-picus.sh z3 600 ./logs/test/ ./benchmarks/circomlib-cff5ab6/
+
+solver=$1
+otime=$2
+logpath=$3
+targetfolder=$4
+
+mkdir -p ${logpath}
+
+for fp in ${targetfolder}/*.r1cs
+do
+	fn=$(basename ${fp})
+	bn="${fn%.*}"
+    bp="${fp%.*}"
+	echo "=================== checking: ${fn} ==================="
+	echo "====   start: $(date -u)"
+	st="$(date -u +%s)"
+
+    timeout ${otime} racket ./picus-dpvl-uniqueness.rkt --timeout 5000 --solver ${solver} --weak --noprop --r1cs ${fp} > ${logpath}/${bn}.log 2>&1
+
+	et="$(date -u +%s)"
+	echo "====     end: $(date -u)"
+	ct="$(($et-$st))"
+	echo "==== elapsed: ${ct} seconds"
+done

scripts/batch-run-picus-nosolve.sh

@@ -0,0 +1,27 @@
+#!/bin/bash
+# usage: this.sh <timeout:seconds> <log_path> <target_folder>
+# example: ./batch-run-picus.sh z3 600 ./logs/test/ ./benchmarks/circomlib-cff5ab6/
+
+solver=$1
+otime=$2
+logpath=$3
+targetfolder=$4
+
+mkdir -p ${logpath}
+
+for fp in ${targetfolder}/*.r1cs
+do
+	fn=$(basename ${fp})
+	bn="${fn%.*}"
+    bp="${fp%.*}"
+	echo "=================== checking: ${fn} ==================="
+	echo "====   start: $(date -u)"
+	st="$(date -u +%s)"
+
+    timeout ${otime} racket ./picus-dpvl-uniqueness.rkt --timeout 5000 --solver ${solver} --weak --nosolve --r1cs ${fp} > ${logpath}/${bn}.log 2>&1
+
+	et="$(date -u +%s)"
+	echo "====     end: $(date -u)"
+	ct="$(($et-$st))"
+	echo "==== elapsed: ${ct} seconds"
+done