Skip to content

Commit

Permalink
reenable error tracer for Rosette 4
Browse files Browse the repository at this point in the history
  • Loading branch information
@sorawee
sorawee committed Jan 29, 2021
1 parent 9348350 commit e37f49b
Show file tree
Hide file tree
Showing 38 changed files with 148 additions and 128 deletions.
13 changes: 9 additions & 4 deletions rosette/base/core/bool.rkt
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
#lang racket

(require "term.rkt" "union.rkt" "exn.rkt" "result.rkt")
(require "term.rkt" "union.rkt" "exn.rkt" "result.rkt" "reporter.rkt")

(provide
;; ---- lifted boolean? operations ---- ;;
Expand Down Expand Up @@ -442,11 +442,16 @@
[(_ val msg) (syntax/loc stx ($assume val msg raise-exn:fail:svm:assume:user))]))

(define (halt-svm ex)
(halt ex (vc)))
(define result (halt ex (vc)))
((current-reporter) 'exception result)
result)

(define (halt-err ex) ; Treat an exn:fail? error as an assertion failure.
(halt (make-exn:fail:svm:assert:err (exn-message ex) (exn-continuation-marks ex))
(asserting (vc) #f)))
(define result
(halt (make-exn:fail:svm:assert:err (exn-message ex) (exn-continuation-marks ex))
(asserting (vc) #f)))
((current-reporter) 'exception result)
result)

; The with-vc form has two variants, (with-vc body) and (with-vc vc0 body).
; The former expands into (with-vc (vc) body). The latter sets the current
Expand Down
1 change: 1 addition & 0 deletions rosette/lib/trace/compile.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@
(or (not the-path)
(not (or (string-contains? the-path "rosette/base/form/module.rkt")
(string-contains? the-path "rosette/base/form/control.rkt")
(string-contains? the-path "rosette/base/core/bool.rkt")
(string-contains? the-path "rosette/query/form.rkt")
(string-contains? the-path "rosette/query/core.rkt")))))

Expand Down
23 changes: 17 additions & 6 deletions rosette/lib/trace/tool.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@
(require rosette/base/core/reporter
rosette/base/core/bool
rosette/base/core/exn
rosette/base/core/result
rosette/base/core/bool
syntax/parse/define
(only-in "../util/syntax.rkt" syntax->readable-location)
(only-in rosette/query/core [∃-solve query:solve])
Expand Down Expand Up @@ -61,15 +63,24 @@

(define reporter
(match-lambda*
[(list 'exception guard e)
(define the-pc (&& guard)) ; <-- remove reference to the PC ... this code will need updating
[(list 'exception (halt e s))
(define assumes (spec-assumes s))
(define asserts (spec-asserts s))
(define skip?
(or (exn:fail:svm:merge? e) ; <-- replace with new exn types ... this code will need updating
(or (exn:fail:svm:merge? e)
;; We skip exn:fail:svm:merge? because we already present data of
;; leave nodes.
(false? assumes)
;; Skip false? to make it match the old behavior. We can remove this
;; or add an option to conditionally filter this later.
(and (and (symbolic-trace-skip-assertion?)
(exn:fail:svm:assert? e)) ; <-- replace with new exn types ... this code will need updating
(or (exn:fail:svm:assert:user? e)
(exn:fail:svm:assume:user? e)))
(collect-stats 'assertion))
;; TODO: need to fix the name. symbolic-trace-skip-assertion?
;; doesn't make sense anymore
(and (and (symbolic-trace-skip-infeasible-solver?)
(unsat? (query:solve (list the-pc))))
(unsat? (query:solve (list assumes))))
(collect-stats 'solver))))
(unless skip?
(define entry
Expand All @@ -80,7 +91,7 @@
(continuation-mark-set->list
(exn-continuation-marks e)
'symbolic-trace:stack-key)
the-pc))
assumes))
(current-entry-handler
entry
(λ (e) (set! current-trace (cons e current-trace)))
Expand Down
5 changes: 3 additions & 2 deletions test/trace/code/ex-1-3.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,5 +3,6 @@
(define-symbolic xs integer? #:length 4)
(define (sum xs) (foldl + xs)) ; bug: missing 0 after +
(verify
#:assume (assert (positive? (sum xs)))
#:guarantee (assert (ormap positive? xs)))
(begin
(assume (positive? (sum xs)))
(assert (ormap positive? xs))))
5 changes: 3 additions & 2 deletions test/trace/code/ex-2.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,5 +10,6 @@
[else (apply + xs)]))

(verify
#:assume (assert (positive? (sum xs)))
#:guarantee (assert (ormap positive? xs)))
(begin
(assume (positive? (sum xs)))
(assert (ormap positive? xs))))
7 changes: 4 additions & 3 deletions test/trace/code/ex-3.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@
[else (select >=pivot (- n len< 1))])]))

(verify
#:assume (assert (and (<= 0 n (sub1 (length xs)))
(= k (select xs n))))
#:guarantee (assert (= k (list-ref (sort xs <) n))))
(begin
(assume (and (<= 0 n (sub1 (length xs)))
(= k (select xs n))))
(assert (= k (list-ref (sort xs <) n)))))
6 changes: 2 additions & 4 deletions test/trace/code/toplevel.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,9 @@

(define-symbolic x integer?)

(verify #:assume (1)
#:guarantee (2))
(verify (1))

(synthesize #:forall x
#:assume (1)
#:guarantee (2))

(solve (1))
(solve (3))
2 changes: 1 addition & 1 deletion test/trace/output/all/ex-1-1.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("@foldl: arity mismatch;\n the expected nu...."
(("[assert] @foldl: arity mismatch;\n the ex...."
(#%app "ex-1-1.rkt" 4 17)
((@foldl "ex-1-1.rkt" 4 17) (sum "ex-1-1.rkt" 5 19))
#t))))
2 changes: 1 addition & 1 deletion test/trace/output/all/ex-1-2.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("@foldl: arity mismatch;\n the expected nu...."
(("[assert] @foldl: arity mismatch;\n the ex...."
(#%app "ex-1-2.rkt" 4 17)
((@foldl "ex-1-2.rkt" 4 17) (sum "ex-1-2.rkt" 8 24))
#t))))
4 changes: 2 additions & 2 deletions test/trace/output/all/ex-1-3.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("@foldl: arity mismatch;\n the expected nu...."
(("[assert] @foldl: arity mismatch;\n the ex...."
(#%app "ex-1-3.rkt" 4 17)
((@foldl "ex-1-3.rkt" 4 17) (sum "ex-1-3.rkt" 6 29))
((@foldl "ex-1-3.rkt" 4 17) (sum "ex-1-3.rkt" 7 22))
#t))))
4 changes: 2 additions & 2 deletions test/trace/output/all/ex-2.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("$*: expected real? arguments\n arguments...."
(("[assert] $*: expected real? arguments\n ...."
(#%app "ex-2.rkt" 9 5)
((* "ex-2.rkt" 9 5) (sum "ex-2.rkt" 13 29))
((* "ex-2.rkt" 9 5) (sum "ex-2.rkt" 14 22))
(&& (= ...) ...)))))
14 changes: 7 additions & 7 deletions test/trace/output/all/ex-3.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,19 +1,19 @@
((#:stats #hash((assertion . 5) (solver . 1)))
((#:stats #hash((assertion . 4) (solver . 1)))
(#:trace
(("select: arity mismatch;\n the expected nu...."
(("[assert] select: arity mismatch;\n the ex...."
(#%app "ex-3.rkt" 16 24)
((select "ex-3.rkt" 16 24) (select "ex-3.rkt" 21 28))
((select "ex-3.rkt" 16 24) (select "ex-3.rkt" 22 21))
(&& (&& ...) ...))
("select: arity mismatch;\n the expected nu...."
("[assert] select: arity mismatch;\n the ex...."
(#%app "ex-3.rkt" 16 24)
((select "ex-3.rkt" 16 24)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 21 28))
(select "ex-3.rkt" 22 21))
(&& (&& ...) ...))
("select: arity mismatch;\n the expected nu...."
("[assert] select: arity mismatch;\n the ex...."
(#%app "ex-3.rkt" 16 24)
((select "ex-3.rkt" 16 24)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 21 28))
(select "ex-3.rkt" 22 21))
(&& (&& ...) ...)))))
12 changes: 6 additions & 6 deletions test/trace/output/assertion/if.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
((#:stats #hash((assertion . 1) (solver . 0)))
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("application: not a procedure;\n expected ...."
(("[assert] application: not a procedure;\n ...."
(#%app "if.rkt" 4 6)
((1 "if.rkt" 4 6))
b)
("application: not a procedure;\n expected ...."
("[assert] application: not a procedure;\n ...."
(#%app "if.rkt" 5 12)
((1 "if.rkt" 5 12))
(&& a ...))
("application: not a procedure;\n expected ...."
b)
("[assert] application: not a procedure;\n ...."
(#%app "if.rkt" 5 16)
((2 "if.rkt" 5 16))
(&& a ...)))))
(|| a ...)))))
2 changes: 1 addition & 1 deletion test/trace/output/regular/assertion.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace (("assert: bad\n" (assert "assertion.rkt" 4 9) () b))))
(#:trace (("[assert] bad\n" (assert "assertion.rkt" 4 9) () b))))
2 changes: 1 addition & 1 deletion test/trace/output/regular/core-form.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("result arity mismatch;\n expected number ...."
(("[assert] result arity mismatch;\n expecte...."
(let-values "core-form.rkt" 7 9)
((f "core-form.rkt" 11 8))
b))))
2 changes: 1 addition & 1 deletion test/trace/output/regular/error.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
((#:error "assert: both branches infeasible\n"))
((#:error "[assert] contradiction\n"))
2 changes: 1 addition & 1 deletion test/trace/output/regular/ex-1-1.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("@foldl: arity mismatch;\n the expected nu...."
(("[assert] @foldl: arity mismatch;\n the ex...."
(#%app "ex-1-1.rkt" 4 17)
((@foldl "ex-1-1.rkt" 4 17) (sum "ex-1-1.rkt" 5 19))
#t))))
2 changes: 1 addition & 1 deletion test/trace/output/regular/ex-1-2.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("@foldl: arity mismatch;\n the expected nu...."
(("[assert] @foldl: arity mismatch;\n the ex...."
(#%app "ex-1-2.rkt" 4 17)
((@foldl "ex-1-2.rkt" 4 17) (sum "ex-1-2.rkt" 8 24))
#t))))
4 changes: 2 additions & 2 deletions test/trace/output/regular/ex-1-3.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("@foldl: arity mismatch;\n the expected nu...."
(("[assert] @foldl: arity mismatch;\n the ex...."
(#%app "ex-1-3.rkt" 4 17)
((@foldl "ex-1-3.rkt" 4 17) (sum "ex-1-3.rkt" 6 29))
((@foldl "ex-1-3.rkt" 4 17) (sum "ex-1-3.rkt" 7 22))
#t))))
4 changes: 2 additions & 2 deletions test/trace/output/regular/ex-2.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("$*: expected real? arguments\n arguments...."
(("[assert] $*: expected real? arguments\n ...."
(#%app "ex-2.rkt" 9 5)
((* "ex-2.rkt" 9 5) (sum "ex-2.rkt" 13 29))
((* "ex-2.rkt" 9 5) (sum "ex-2.rkt" 14 22))
(&& (= ...) ...)))))
43 changes: 18 additions & 25 deletions test/trace/output/regular/ex-3.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,59 +1,52 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("select: arity mismatch;\n the expected nu...."
(("[assert] select: arity mismatch;\n the ex...."
(#%app "ex-3.rkt" 16 24)
((select "ex-3.rkt" 16 24) (select "ex-3.rkt" 21 28))
((select "ex-3.rkt" 16 24) (select "ex-3.rkt" 22 21))
(&& (&& ...) ...))
("assert: unexpected empty list\n"
("[assert] unexpected empty list\n"
(assert "ex-3.rkt" 8 18)
((select "ex-3.rkt" 17 18) (select "ex-3.rkt" 21 28))
((select "ex-3.rkt" 17 18) (select "ex-3.rkt" 22 21))
(&& (&& ...) ...))
("select: arity mismatch;\n the expected nu...."
("[assert] select: arity mismatch;\n the ex...."
(#%app "ex-3.rkt" 16 24)
((select "ex-3.rkt" 16 24)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 21 28))
(select "ex-3.rkt" 22 21))
(&& (&& ...) ...))
("assert: unexpected empty list\n"
("[assert] unexpected empty list\n"
(assert "ex-3.rkt" 8 18)
((select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 21 28))
(&& (|| ...) ...))
("select: arity mismatch;\n the expected nu...."
(select "ex-3.rkt" 22 21))
(&& (&& ...) ...))
("[assert] select: arity mismatch;\n the ex...."
(#%app "ex-3.rkt" 16 24)
((select "ex-3.rkt" 16 24)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 21 28))
(select "ex-3.rkt" 22 21))
(&& (&& ...) ...))
("assert: unexpected empty list\n"
("[assert] unexpected empty list\n"
(assert "ex-3.rkt" 8 18)
((select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 21 28))
(&& (|| ...) ...))
("select: arity mismatch;\n the expected nu...."
(select "ex-3.rkt" 22 21))
(&& (&& ...) ...))
("[assert] select: arity mismatch;\n the ex...."
(#%app "ex-3.rkt" 16 24)
((select "ex-3.rkt" 16 24)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 21 28))
(select "ex-3.rkt" 22 21))
(&& (&& ...) ...))
("assert: unexpected empty list\n"
("[assert] unexpected empty list\n"
(assert "ex-3.rkt" 8 18)
((select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 21 28))
(&& (&& ...) ...))
("assert: both branches infeasible\n"
(#%app "ex-3.rkt" 14 10)
((select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 17 18)
(select "ex-3.rkt" 21 28))
(select "ex-3.rkt" 22 21))
(&& (&& ...) ...)))))
2 changes: 1 addition & 1 deletion test/trace/output/regular/forall.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("rest: contract violation\n expected: (an...."
(("[assert] rest: contract violation\n expe...."
(#%app "forall.rkt" 6 2)
((@rest "forall.rkt" 6 2))
b))))
11 changes: 5 additions & 6 deletions test/trace/output/regular/if.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,15 +1,14 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("application: not a procedure;\n expected ...."
(("[assert] application: not a procedure;\n ...."
(#%app "if.rkt" 4 6)
((1 "if.rkt" 4 6))
b)
("application: not a procedure;\n expected ...."
("[assert] application: not a procedure;\n ...."
(#%app "if.rkt" 5 12)
((1 "if.rkt" 5 12))
(&& a ...))
("application: not a procedure;\n expected ...."
b)
("[assert] application: not a procedure;\n ...."
(#%app "if.rkt" 5 16)
((2 "if.rkt" 5 16))
(&& a ...))
("assert: both branches infeasible\n" (#%app "if.rkt" 5 6) () a))))
(|| a ...)))))
2 changes: 1 addition & 1 deletion test/trace/output/regular/infeasible-solver.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("@add1: arity mismatch;\n the expected num...."
(("[assert] @add1: arity mismatch;\n the exp...."
(#%app "infeasible-solver.rkt" 7 2)
((@apply "infeasible-solver.rkt" 7 2))
(&& (! ...) ...)))))
2 changes: 1 addition & 1 deletion test/trace/output/regular/list-2.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("error: bad\n"
(("[assert] error: bad\n"
(#%app "list-2.rkt" 9 13)
((error "list-2.rkt" 9 13)
(...race/code/list-2.rkt:9:5 "list-2.rkt" 6 16)
Expand Down
5 changes: 4 additions & 1 deletion test/trace/output/regular/list.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("error: bad\n" (#%app "list.rkt" 4 13) ((error "list.rkt" 4 13)) (! b)))))
(("[assert] error: bad\n"
(#%app "list.rkt" 4 13)
((error "list.rkt" 4 13))
(! b)))))
2 changes: 1 addition & 1 deletion test/trace/output/regular/macro-define.rkt.out
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
((#:stats #hash((assertion . 0) (solver . 0)))
(#:trace
(("application: not a procedure;\n expected ...."
(("[assert] application: not a procedure;\n ...."
(mac "macro-define.rkt" 4 1)
()
#t))))
Loading

0 comments on commit e37f49b

Please sign in to comment.