fix: handle interrupt correctly

picus-cex-uniqueness.rkt

@@ -70,7 +70,6 @@
 ; =================================================
 ; ======== resolve solver specific methods ========
 ; =================================================
-(define state-smt-path (solver:state-smt-path arg-solver))
 (define solve (solver:solve arg-solver))
 (define parse-r1cs (solver:parse-r1cs arg-solver))
 (define expand-r1cs (solver:expand-r1cs arg-solver))
@@ -152,7 +151,7 @@
     alt-xlist alt-defs alt-cnsts
     unique-set precondition ; prior knowledge row
     arg-selector arg-prop arg-timeout arg-smt path-sym
-    solve state-smt-path interpret-r1cs
+    solve interpret-r1cs
     parse-r1cs optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1
 ))
 (printf "# final unknown set ~a.\n" res-us)
@@ -161,4 +160,4 @@
     (printf "# strong uniqueness: ~a.\n" res)
 )
 (when (equal? 'unsafe res)
-    (printf "# counter-example:\n  ~a.\n" res-info))
+    (printf "# counter-example:\n  ~a.\n" res-info))

picus.rkt

@@ -80,7 +80,6 @@
 ; =================================================
 ; ======== resolve solver specific methods ========
 ; =================================================
-(define state-smt-path (solver:state-smt-path arg-solver))
 (define solve (solver:solve arg-solver))
 (define parse-r1cs (solver:parse-r1cs arg-solver))
 (define expand-r1cs (solver:expand-r1cs arg-solver))
@@ -164,7 +163,7 @@
    alt-varlist alt-defs alt-cnsts
    unique-set precondition ; prior knowledge row
    arg-selector arg-prop arg-slv arg-timeout arg-smt arg-cex-verbose path-sym
-   solve state-smt-path interpret-r1cs
+   solve interpret-r1cs
    optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1))
 (printf "# final unknown set ~a.\n" res-us)
 (if arg-weak

picus/algorithms/cex.rkt

@@ -30,7 +30,7 @@
     alt-xlist alt-defs alt-cnsts
     unique-set precondition
     arg-selector arg-prop arg-timeout arg-smt path-sym
-    solve state-smt-path interpret-r1cs
+    solve interpret-r1cs
     parse-r1cs optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1
     )
 
@@ -113,7 +113,7 @@
             alt-xlist alt-defs ialt-cnsts
             unique-set precondition ; prior knowledge row
             arg-selector arg-prop #t arg-timeout arg-smt #f path-sym
-            solve state-smt-path interpret-r1cs
+            solve interpret-r1cs
             parse-r1cs optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1
             #:extcnsts (model2cnsts partial-model)
             #:skip-query? (equal? i 2) ; (debug)
@@ -140,4 +140,4 @@
     ; return
     (values 'unsafe null null partial-model)
 
-)
+)

picus/algorithms/cex0.rkt

@@ -30,7 +30,7 @@
     alt-xlist alt-defs alt-cnsts
     unique-set precondition
     arg-selector arg-prop arg-timeout arg-smt path-sym
-    solve state-smt-path interpret-r1cs
+    solve interpret-r1cs
     parse-r1cs optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1
     )
 
@@ -87,7 +87,7 @@
             alt-xlist alt-defs i-alt-cnsts
             unique-set precondition ; prior knowledge row
             arg-selector arg-prop arg-timeout arg-smt path-sym
-            solve state-smt-path interpret-r1cs
+            solve interpret-r1cs
             parse-r1cs optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1
             #:extcnsts (model2cnsts partial-model)
         ))
@@ -111,4 +111,4 @@
         ; (todo) if success, need to update exclude-scopes
     )
 
-)
+)

picus/algorithms/dpvl.rkt

@@ -59,7 +59,6 @@
 (define :precondition null)
 
 (define :solve null)
-(define :state-smt-path null)
 (define :interpret-r1cs null)
 
 (define :optimize-r1cs-p0 null)
@@ -119,7 +118,7 @@
                       (r1cs:rsolve))))))
   ; perform optimization
   (define final-str (:interpret-r1cs (r1cs:rcmds-append :opts final-cmds)))
-  (define res (:solve final-str :arg-timeout #:output-smt? #f))
+  (define-values (res smt-path) (:solve final-str :arg-timeout #:output-smt? #f))
   (define solved? (cond
                     [(equal? 'unsat (car res))
                      (printf "verified.\n")
@@ -147,7 +146,7 @@
                      ; possibly timeout in small step, result is unknown
                      'skip]))
   (when :arg-smt
-    (printf "    # smt path: ~a\n" (:state-smt-path)))
+    (printf "    # smt path: ~a\n" smt-path))
   (values solved? (cdr res)))
 
 ; select and solve
@@ -337,7 +336,7 @@
          alt-varlist alt-defs alt-cnsts
          unique-set precondition
          arg-selector arg-prop arg-slv arg-timeout arg-smt arg-cex-verbose path-sym
-         solve state-smt-path interpret-r1cs
+         solve interpret-r1cs
          optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1
          ; extra constraints, usually from cex module about partial model
          #:extcnsts [extcnsts (r1cs:rcmds (list ))]
@@ -374,7 +373,6 @@
   (set! :precondition precondition)
 
   (set! :solve solve)
-  (set! :state-smt-path state-smt-path)
   (set! :interpret-r1cs interpret-r1cs)
 
   (set! :optimize-r1cs-p0 optimize-r1cs-p0)

picus/solver.rkt

@@ -29,7 +29,6 @@
     (prefix-in cvc5-ab0: "./optimizers/r1cs-cvc5-ab0-optimizer.rkt")
 )
 (provide (rename-out
-    [state-smt-path state-smt-path]
     [solve solve]
     [parse-r1cs parse-r1cs]
     [expand-r1cs expand-r1cs]
@@ -39,14 +38,6 @@
     [interpret-r1cs interpret-r1cs]
 ))
 
-(define (state-smt-path arg-solver)
-    (cond
-        [(equal? "z3" arg-solver) (lambda () z3-solver:state-smt-path)]
-        [(equal? "cvc4" arg-solver) (lambda () cvc4-solver:state-smt-path)]
-        [(equal? "cvc5" arg-solver) (lambda () cvc5-solver:state-smt-path)]
-        [else (tokamak:exit "you can't reach here")]
-    )
-)
 (define (solve arg-solver)
     (cond
         [(equal? "z3" arg-solver) z3-solver:solve]
@@ -104,4 +95,4 @@
         [(equal? "cvc5" arg-solver) cvc5-rint:interpret-r1cs]
         [else (tokamak:exit "you can't reach here")]
     )
-)
+)

picus/solvers/common.rkt

@@ -0,0 +1,179 @@
+#lang racket/base
+
+(provide make-solve)
+(require racket/string
+         racket/port
+         racket/match
+         racket/engine
+         (prefix-in tokamak: "../tokamak.rkt")
+         (prefix-in config: "../config.rkt"))
+
+(define ((make-solve #:executable executable
+                     #:options [options '()])
+         smt-str timeout #:verbose? [verbose? #f] #:output-smt? [output-smt? #f])
+  (define temp-folder (find-system-path 'temp-dir))
+  (define temp-file (format "picus~a.smt2"
+                            (string-replace (format "~a" (current-inexact-milliseconds)) "." "")))
+  (define temp-path (build-path temp-folder temp-file))
+  (with-output-to-file temp-path
+    (λ () (display smt-str)))
+  (when (or verbose? output-smt?)
+    (printf "(written to: ~a)\n" temp-path))
+
+  (when verbose?
+    (printf "# solving...\n"))
+  (define-values (sp out in err)
+    ; (note) use `apply` to expand the last argument
+    ; (apply subprocess #f #f #f (find-executable-path "cvc5") (list temp-path))
+    (apply subprocess #f #f #f (find-executable-path executable) temp-path options))
+
+  (close-output-port in)
+
+  (define engine0
+    (engine
+     (lambda (_)
+       (define out-str (port->string out #:close? #t))
+       (define err-str (port->string err #:close? #t))
+       (subprocess-wait sp)
+       (cons out-str err-str))))
+
+  (define (kill-process)
+    (subprocess-kill sp #t)
+    (close-input-port out)
+    (close-input-port err)
+    (values (cons 'timeout "") temp-path))
+
+  (define eres
+    (call-with-exception-handler
+     (λ (exn)
+       (when (exn:break? exn)
+         (kill-process)))
+     (λ () (engine-run timeout engine0))))
+
+  (cond
+    [eres
+     (match-define (cons out-str err-str) (engine-result engine0))
+     (when verbose?
+       (printf "# stdout:\n~a\n" out-str)
+       (printf "# stderr:\n~a\n" err-str))
+     (values (cond
+               [(non-empty-string? err-str) (cons 'error err-str)] ; something wrong, not solved
+               [(string-prefix? out-str "unsat") (cons 'unsat out-str)]
+               [(string-prefix? out-str "sat") (cons 'sat (parse-model out-str))]
+               [(string-prefix? out-str "unknown") (cons 'unknown out-str)]
+               [else (cons 'else out-str)])
+             temp-path)]
+    [else (kill-process)]))
+
+; example cvc5 string:
+; sat
+; (
+; (define-fun x0 () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617) 0)
+; (define-fun x1 () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617) 0)
+; (define-fun x2 () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617) -1)
+; (define-fun x3 () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617) 0)
+; (define-fun x4 () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617) 0)
+; (define-fun p () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617) 0)
+; (define-fun ps1 () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617) -1)
+; (define-fun ps2 () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617) -2)
+; (define-fun ps3 () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617) -3)
+; (define-fun ps4 () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617) -4)
+; (define-fun ps5 () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617) -5)
+; (define-fun zero () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617) 0)
+; (define-fun one () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617) 1)
+; (define-fun y1 () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617) 1)
+; (define-fun y2 () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617) -1)
+; )
+;
+; example z3 string:
+;   sat
+; (
+;   (define-fun ps2 () Int
+;     21888242871839275222246405745257275088548364400416034343698204186575808495615)
+;   (define-fun x2 () Int
+;     0)
+;   (define-fun zero () Int
+;     0)
+;   (define-fun y1 () Int
+;     1)
+;   (define-fun ps3 () Int
+;     21888242871839275222246405745257275088548364400416034343698204186575808495614)
+;   (define-fun x3 () Int
+;     0)
+;   (define-fun x0 () Int
+;     0)
+;   (define-fun one () Int
+;     1)
+;   (define-fun p () Int
+;     21888242871839275222246405745257275088548364400416034343698204186575808495617)
+;   (define-fun x4 () Int
+;     0)
+;   (define-fun y2 () Int
+;     0)
+;   (define-fun y3 () Int
+;     1)
+;   (define-fun ps4 () Int
+;     21888242871839275222246405745257275088548364400416034343698204186575808495613)
+;   (define-fun x1 () Int
+;     0)
+;   (define-fun ps1 () Int
+;     21888242871839275222246405745257275088548364400416034343698204186575808495616)
+;   (define-fun ps5 () Int
+;     21888242871839275222246405745257275088548364400416034343698204186575808495612)
+; )
+;
+; example cvc4 string:
+;  sat
+; (model
+; (define-fun x0 () Int 0)
+; (define-fun x1 () Int 1)
+; (define-fun x2 () Int 0)
+; (define-fun x3 () Int 1)
+; (define-fun x4 () Int 0)
+; (define-fun p () Int 21888242871839275222246405745257275088548364400416034343698204186575808495617)
+; (define-fun ps1 () Int 21888242871839275222246405745257275088548364400416034343698204186575808495616)
+; (define-fun ps2 () Int 21888242871839275222246405745257275088548364400416034343698204186575808495615)
+; (define-fun ps3 () Int 21888242871839275222246405745257275088548364400416034343698204186575808495614)
+; (define-fun ps4 () Int 21888242871839275222246405745257275088548364400416034343698204186575808495613)
+; (define-fun ps5 () Int 21888242871839275222246405745257275088548364400416034343698204186575808495612)
+; (define-fun zero () Int 0)
+; (define-fun one () Int 1)
+; (define-fun y1 () Int 0)
+; (define-fun y2 () Int 0)
+; (define-fun y3 () Int 0)
+; )
+
+(define readtable-for-parsing
+  ;; Since 368f3c3, cvc5 can produce a finite field literal, in the format:
+  ;;   #f <value> m <mod-value>
+  ;; See https://github.com/cvc5/cvc5/commit/368f3c3ed695e925f0eea1b9d6a8280cdfa9f64c
+  ;; Here, we simply want to extract the value.
+  (make-readtable #f #\f 'dispatch-macro
+                  (λ (_ port src line col pos)
+                    (match (symbol->string (read port))
+                      ;; we have already consumed "#f" from the dispatch macro
+                      ;; so here, we consume the rest of the token: <value> m <mod-value>
+                      [(pregexp #px"^(\\d+)m\\d+$" (list _ (app string->number val)))
+                       val]))))
+
+(define (parse-model arg-str)
+  (define port (open-input-string arg-str))
+  ;; this consumes the sat token
+  (read port)
+  ;; this consumes ( (define-fun) ... )
+  (define raw-model
+    (parameterize ([current-readtable readtable-for-parsing])
+      (read port)))
+  (define model (make-hash))
+  (for ([binding (in-list raw-model)])
+    (match binding
+      ;; check that val is a number so that non-number will get reported below.
+      [`(define-fun ,var () #;type ,_ ,(? number? val))
+       ; update model
+       (hash-set! model (symbol->string var)
+                  (if (< val 0)
+                      (+ config:p val) ; remap to field
+                      val))]
+      [_ (tokamak:exit "model parsing error, check: ~a" binding)]))
+  ; return the model
+  model)