Rename spec? -> vc? and spec-* -> vc-*.

emina · Feb 3, 2021 · 7f1d498 · 7f1d498
1 parent 119c42b
commit 7f1d498
Show file tree

Hide file tree

Showing 16 changed files with 215 additions and 214 deletions.
diff --git a/rosette/base/base.rkt b/rosette/base/base.rkt
@@ -16,7 +16,7 @@
   (filtered-out drop@ 
     (combine-out
      ; core/bool.rkt
-     vc with-vc vc-clear! spec? vc-true? vc-true spec-assumes spec-asserts
+     vc with-vc vc-clear! vc? vc-true? vc-true vc-assumes vc-asserts
      @assert @assume
      @boolean? @false? @! @&& @=> @<=> @forall @exists
      ; core/real.rkt

diff --git a/rosette/base/core/bool.rkt b/rosette/base/core/bool.rkt
@@ -9,8 +9,8 @@
  and-&& or-|| instance-of? T*->boolean?
  ;; ---- VC generation ---- ;;       
  @assert @assume $assert $assume
- (rename-out [vc-get vc]) vc-clear! with-vc vc-merge!
- spec? spec-assumes spec-asserts
+ (rename-out [vc-get vc]) vc-clear! vc-merge! with-vc 
+ vc? vc-assumes vc-asserts
  vc-true vc-true?)
 
 ;; ----------------- Boolean type ----------------- ;; 
@@ -287,36 +287,38 @@
 
 ;; ----------------- VC generation ----------------- ;;
 
-; A spec consists of two (symbolic or concrete) @boolean?
-; values representing the assumptions and assertions issued
-; so far. A spec is legal if at least one of its assumes or
-; asserts is true under all models.
-(struct spec (assumes asserts) #:transparent)
+; A verification condition (VC) consists of two @boolean?
+; values representing assumptions and assertions issued
+; during execution. A VC is legal if at least one of its
+; constituent fields is true under all models.
 
-; The true (top) spec.
-(define vc-true (spec #t #t))
+(struct vc (assumes asserts) #:transparent)
+
+; The true verification condition.
+(define vc-true (vc #t #t))
 
 (define (vc-true? s) (equal? s vc-true))
 
-; Returns (spec (s.assumes && (s.asserts => g) s.asserts). 
+; Returns (vc (s.assumes && (s.asserts => g)) s.asserts). 
 (define (assuming s g)  ; g must be a symbolic or concrete boolean
-  (spec (&& (spec-assumes s) (=> (spec-asserts s) g)) (spec-asserts s)))
+  (vc (&& (vc-assumes s) (=> (vc-asserts s) g)) (vc-asserts s)))
 
-; Returns (spec s.assumes (s.asserts && (s.assumes => g))). 
+; Returns (vc s.assumes (s.asserts && (s.assumes => g))). 
 (define (asserting s g) ; g must be a symbolic or concrete boolean 
-  (spec (spec-assumes s) (&& (spec-asserts s) (=> (spec-assumes s) g))))
+  (vc (vc-assumes s) (&& (vc-asserts s) (=> (vc-assumes s) g))))
 
-; The vc parameter keeps track of the current verification condition,
-; which is an instance of spec?. The default vc is the true spec.
-(define vc (make-parameter
-            vc-true
-            (lambda (v) (unless (spec? v) (raise-argument-error 'vc "spec?" v)) v)))
+; The current-vc parameter keeps track of the current verification condition,
+; which is an instance of vc?. The default value for this parameter is vc-true.
+(define current-vc
+  (make-parameter
+   vc-true
+   (lambda (v) (unless (vc? v) (raise-argument-error 'vc "vc?" v)) v)))
 
 ; Returns the current vc, without exposing the parameter outside the module. 
-(define (vc-get) (vc))
+(define (vc-get) (current-vc))
 
 ; Clears the current vc by setting it to the true spec.
-(define (vc-clear!) (vc vc-true))
+(define (vc-clear!) (current-vc vc-true))
 
 ; Returns #t if x && (g => y) is equivalent to x according to the embedded
 ; rewrite rules. Otherwise returns #f.
@@ -355,48 +357,48 @@
 ;     (apply && gs=>ys)]
 ;    [_ (apply && xf gs=>ys)]))
 
-; Takes as input a list of n guards and n specs and sets the current vc
-; to (vc) && (spec-guard guard1 specs1) && ... && (spec-guard guardn specn).
-; Then, it checks if either the assumes or the asserts of the resulting spec
+; Takes as input a list of n guards and n vcs and sets the current vc
+; to (current-vc) && (vc-guard guard1 vc1) && ... && (vc-guard guardn vcn).
+; Then, it checks if either the assumes or the asserts of the resulting vc
 ; are false? and if so, throws either an exn:fail:svm:assume? or
 ; exn:fail:svm:assert? exception. This procedure makes the following assumptions:
 ; * at most one of the given guards is true in any model,
-; * (spec-assumes specs[i]) => (spec-assumes (vc)) for all i, and 
-; * (spec-asserts specs[i]) => (spec-asserts (vc)) for all i.
-(define (vc-merge! guards specs)
-  (unless (null? specs)
-    (define specm
-      (spec (merge-field spec-assumes (vc) guards specs)
-            (merge-field spec-asserts (vc) guards specs)))
-    (vc specm)
-    (when (false? (spec-assumes specm))
+; * (vc-assumes specs[i]) => (vc-assumes (current-vc)) for all i, and 
+; * (vc-asserts specs[i]) => (vc-asserts (current-vc)) for all i.
+(define (vc-merge! guards vcs)
+  (unless (null? vcs)
+    (define vc*
+      (vc (merge-field vc-assumes (current-vc) guards vcs)
+          (merge-field vc-asserts (current-vc) guards vcs)))
+    (current-vc vc*)
+    (when (false? (vc-assumes vc*))
       (raise-exn:fail:svm:assume:core "contradiction"))
-    (when (false? (spec-asserts specm))
+    (when (false? (vc-asserts vc*))
       (raise-exn:fail:svm:assert:core "contradiction"))))
 
-; Sets the current vc to (spec-proc (vc) g) where g is (@true? val).
-; If g is #f or the resulting vc's spec-field value is #f,
+; Sets the current vc to (vc-proc (current-vc) g) where g is (@true? val).
+; If g is #f or the resulting vc's vc-field value is #f,
 ; uses raise-exn throws an exn:fail:svm exception. 
-(define-syntax-rule (vc-set! val msg spec-proc spec-field raise-exn)
+(define-syntax-rule (vc-set! val msg vc-proc vc-field raise-exn)
   (let* ([guard (@true? val)]
-         [specg (spec-proc (vc) guard)])
-    (vc specg)
+         [vc* (vc-proc (current-vc) guard)])
+    (current-vc vc*)
     (when (false? guard)
       (raise-exn msg))
-    (when (false? (spec-field specg))
+    (when (false? (vc-field vc*))
       (raise-exn "contradiction"))))
 
-; Sets the current vc to (asserting (vc) g) where g is (@true? val).
+; Sets the current vc to (asserting (current-vc) g) where g is (@true? val).
 ; If g is #f or the resulting vc's asserts field is #f, throws an
 ; exn:fail:svm:assert exception of the given kind.  
 (define-syntax-rule (vc-assert! val msg raise-kind)
-  (vc-set! val msg asserting spec-asserts raise-kind))
+  (vc-set! val msg asserting vc-asserts raise-kind))
 
-; Sets the current vc to (assuming (vc) g) where g is (@true? val).
+; Sets the current vc to (assuming (current-vc) g) where g is (@true? val).
 ; If g is #f or the resulting vc's assumes field is #f, throws an
 ; exn:fail:svm:assume exception of the given kind. 
 (define-syntax-rule (vc-assume! val msg raise-kind)
-  (vc-set! val msg assuming spec-assumes raise-kind))
+  (vc-set! val msg assuming vc-assumes raise-kind))
 
 ; The $assert form has three variants: ($assert val), ($assert val msg),
 ; and ($assert val msg kind), where val is the value being asserted, msg
@@ -406,7 +408,7 @@
 ; The first two variants of this form are used for issuing assertions from
 ; within the Rosette core. The third variant is used to implement the @assert
 ; form that is exposed to user code. An $assert call modifies the current vc to
-; reflect the issued assertion. If the issued assertion or the spec-assert of the
+; reflect the issued assertion. If the issued assertion or the vc-assert of the
 ; current vc reduce to #f, the call throws an exception of the given kind after
 ; updating the vc.
 (define-syntax ($assert stx)
@@ -442,38 +444,37 @@
     [(_ val msg) (syntax/loc stx ($assume val msg raise-exn:fail:svm:assume:user))]))
 
 (define (halt-svm ex)
-  (define result (halt ex (vc)))
+  (define result (halt ex (current-vc)))
   ((current-reporter) 'exception result)
   result)
 
 (define (halt-err ex) ; Treat an exn:fail? error as an assertion failure.
   (define result
     (halt (make-exn:fail:svm:assert:err (exn-message ex) (exn-continuation-marks ex))
-          (asserting (vc) #f)))
+          (asserting (current-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
-; vc to vc0, evaluates the given body, returns the result, and reverts vc
+; The former expands into (with-vc (current-vc) body). The latter sets the current
+; vc to vc0, evaluates the given body, returns the result, and reverts current-vc
 ; to the value it held before the call to with-vc.
 ;
 ; If the evaluation of the body terminates normally, (with-vc vc0 body)
-; outputs (ans v s) where v is the value computed by the body, and s is 
-; the specification (i.e., assumes and asserts) generated during the evaluation,
-; with v0 as the initial specification. 
+; outputs (ans v vc*) where v is the value computed by the body, and vc* is 
+; the vc (i.e., assumes and asserts) generated during the evaluation,
+; with vc0 as the initial vc. 
 ;
 ; If the evaluation of the body terminates abnormally with an exn:fail? exception,
-; (with-vc vc0 body) outputs (halt v s) where v is an exn:fail:svm? exception
-; that represents the cause of the abnormal termination, and s is the specification
-; (i.e., assumes and asserts) generated during the evaluation, with v0 as
-; the initial specification.
+; (with-vc vc0 body) outputs (halt v vc*) where v is an exn:fail:svm? exception
+; that represents the cause of the abnormal termination, and vc* is the vc
+; generated during the evaluation, with vc0 as the initial vc.
 (define-syntax (with-vc stx)
   (syntax-case stx ()
-    [(_ body) (syntax/loc stx (with-vc (vc) body))]
+    [(_ body) (syntax/loc stx (with-vc (current-vc) body))]
     [(_ vc0 body)
      (syntax/loc stx
-       (parameterize ([vc vc0])
+       (parameterize ([current-vc vc0])
          (with-handlers ([exn:fail:svm? halt-svm]
                          [exn:fail?     halt-err])
-           (ans body (vc)))))]))
+           (ans body (current-vc)))))]))
diff --git a/rosette/guide/scribble/essentials/essentials-log.txt b/rosette/guide/scribble/essentials/essentials-log.txt
@@ -79,11 +79,11 @@
  #"")
 ((assert #t) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((assert #f) ((3) 0 () 0 () () (q exn "[assert] failed")) #"" #"")
-((spec-asserts (vc)) ((3) 0 () 0 () () (q values #f)) #"" #"")
+((vc-asserts (vc)) ((3) 0 () 0 () () (q values #f)) #"" #"")
 ((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
-((spec-asserts (vc)) ((3) 0 () 0 () () (q values #t)) #"" #"")
+((vc-asserts (vc)) ((3) 0 () 0 () () (q values #t)) #"" #"")
 ((assert (not b)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
-((spec-asserts (vc))
+((vc-asserts (vc))
  ((3)
   1
   (((lib "rosette/guide/scribble/util/lifted.rkt")
@@ -97,13 +97,13 @@
  #"")
 ((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((assume #t) ((3) 0 () 0 () () (c values c (void))) #"" #"")
-((spec-assumes (vc)) ((3) 0 () 0 () () (q values #t)) #"" #"")
+((vc-assumes (vc)) ((3) 0 () 0 () () (q values #t)) #"" #"")
 ((assume #f) ((3) 0 () 0 () () (q exn "[assume] failed")) #"" #"")
-((spec-assumes (vc)) ((3) 0 () 0 () () (q values #f)) #"" #"")
+((vc-assumes (vc)) ((3) 0 () 0 () () (q values #f)) #"" #"")
 ((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((define-symbolic i j integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((assume (> j 0)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
-((spec-assumes (vc))
+((vc-assumes (vc))
  ((3)
   1
   (((lib "rosette/guide/scribble/util/lifted.rkt")
@@ -116,7 +116,7 @@
  #""
  #"")
 ((assert (< (- i j) i)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
-((spec-asserts (vc))
+((vc-asserts (vc))
  ((3)
   1
   (((lib "rosette/guide/scribble/util/lifted.rkt")
@@ -130,7 +130,7 @@
  #"")
 ((pretty-print (vc))
  ((3) 0 () 0 () () (c values c (void)))
- #"(spec (< 0 j) (|| (! (< 0 j)) (< (+ i (- j)) i)))\n"
+ #"(vc (< 0 j) (|| (! (< 0 j)) (< (+ i (- j)) i)))\n"
  #"")
 ((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((define int32? (bitvector 32)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
@@ -422,7 +422,7 @@
    values
    c
    (0 (u . "(model\n [l (bv #x394f0402 32)]\n [h (bv #x529e7c00 32)])"))))
- #"cpu time: 1 real time: 38 gc time: 0\n"
+ #"cpu time: 2 real time: 38 gc time: 0\n"
  #"")
 ((time (verify (check-mid-slow bvmid l h)))
  ((3)
@@ -437,7 +437,7 @@
    values
    c
    (0 (u . "(model\n [l (bv #x2faef9a1 32)]\n [h (bv #x5eefb8dd 32)])"))))
- #"cpu time: 4 real time: 183 gc time: 0\n"
+ #"cpu time: 3 real time: 174 gc time: 0\n"
  #"")
 ((time (verify (check-mid bvmid-no-overflow l h)))
  ((3)
@@ -449,7 +449,7 @@
   ()
   ()
   (c values c (0 (u . "(unsat)"))))
- #"cpu time: 1 real time: 159 gc time: 0\n"
+ #"cpu time: 1 real time: 156 gc time: 0\n"
  #"")
 ((error 'call-with-deep-time-limit "out of time")
  ((3) 0 () 0 () () (q exn "call-with-deep-time-limit: out of time"))
@@ -470,7 +470,7 @@
    values
    c
    (0 (u . "(model\n [l (bv #x00000001 32)]\n [h (bv #x7fffffff 32)])"))))
- #"cpu time: 3 real time: 24 gc time: 0\n"
+ #"cpu time: 3 real time: 25 gc time: 0\n"
  #"")
 ((time (verify (check-mid-slow bvmid-no-overflow l h)))
  ((3)
@@ -482,7 +482,7 @@
   ()
   ()
   (c values c (0 (u . "(unsat)"))))
- #"cpu time: 1 real time: 159 gc time: 0\n"
+ #"cpu time: 1 real time: 155 gc time: 0\n"
  #"")
 ((current-bitwidth 32) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((time (verify (check-mid-slow bvmid l h)))
@@ -510,7 +510,7 @@
    values
    c
    (0 (u . "(model\n [l (bv #x71979fa3 32)]\n [h (bv #x76b91b88 32)])"))))
- #"cpu time: 1 real time: 151 gc time: 0\n"
+ #"cpu time: 1 real time: 150 gc time: 0\n"
  #"")
 ((current-bitwidth 512) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((time (verify (check-mid-slow bvmid l h)))
@@ -526,7 +526,7 @@
    values
    c
    (0 (u . "(model\n [l (bv #x70000006 32)]\n [h (bv #x73fffffa 32)])"))))
- #"cpu time: 1 real time: 381 gc time: 0\n"
+ #"cpu time: 1 real time: 377 gc time: 0\n"
  #"")
 ((time (verify (check-mid-slow bvmid-no-overflow l h)))
  ((3)
@@ -538,7 +538,7 @@
   ()
   ()
   (c values c (0 (u . "(unsat)"))))
- #"cpu time: 1 real time: 438 gc time: 0\n"
+ #"cpu time: 1 real time: 428 gc time: 0\n"
  #"")
 ((current-bitwidth #f) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((require rosette/solver/smt/z3)
@@ -562,7 +562,7 @@
    values
    c
    (0 (u . "(model\n [l (bv #x394f0402 32)]\n [h (bv #x529e7c00 32)])"))))
- #"cpu time: 5 real time: 36 gc time: 0\n"
+ #"cpu time: 4 real time: 34 gc time: 0\n"
  #"")
 ((time (verify (check-mid-slow bvmid l h)))
  ((3)
@@ -749,7 +749,7 @@
  #"")
 ((define cex (time (verify (check-sqrt bvsqrt l))))
  ((3) 0 () 0 () () (c values c (void)))
- #"cpu time: 6 real time: 1039 gc time: 0\n"
+ #"cpu time: 7 real time: 1019 gc time: 0\n"
  #"")
 ((bvsqrt (evaluate l cex))
  ((3) 0 () 0 () () (q exn "[assert] Out of fuel."))
@@ -767,5 +767,5 @@
   ()
   ()
   (c values c (0 (u . "(unsat)"))))
- #"cpu time: 15 real time: 69086 gc time: 10\n"
+ #"cpu time: 4 real time: 67739 gc time: 0\n"
  #"")