Source code for the Tutorial on Solver-Aided Programming

assert.rkt

#lang rosette

(define-symbolic* x integer?)

(assert (>= x 1)) ; adds (>= x 1) to the assertion stack
(asserts)         ; see the assertion stack

(assert (>= 2 1)) ; passes
(assert (< 2 1))  ; fails

bounded.rkt

#lang rosette

(define (factorial n g)
  (assert (>= g 0))
  (cond 
    [(= n 0) 1]
    [else (* n (factorial (- n 1) (- g 1)))]))

(define-symbolic k integer?)

(solve (assert (> (factorial k 3) 10))) ; unsat, bound too small

(solve (assert (> (factorial k 4) 10))) ; sat, k = 4

bvlang.rkt

#lang rosette

(require 
 rosette/query/debug 
 rosette/lib/render 
 rosette/lib/synthax
 (prefix-in $ (only-in rosette bveq bvslt bvsgt bvsle bvsge bvult bvugt bvule bvuge))
 (only-in racket [eval racket/eval]))

(define-namespace-anchor bvlang)
(define ns (namespace-anchor->namespace bvlang))
(define (eval form) (racket/eval form ns))

; ----- BV raw syntax -----;

; The def macro turns a BV program into a procedure that invokes the
; BV interpreter on the provided inputs.
(define-syntax-rule (def id ([idx r] ...) (out op in ...) ...)
  (define (id r ...)
    (interpret `((out op ,in ...) ...) `(,r ...))))

(define-syntax (relax-reg stx)
  (syntax-case stx ()
    [(_ in) (with-syntax ([iden (syntax/loc #'in identity)])
              (syntax/loc #'in (iden in)))]))

; The def/debug macro is the same as def, except that it marks the
; defined procedure as a candidate for debugging.
(define-syntax-rule (def/dbg id ([idx r] ...) (out op in ...) ...)
  (define/debug (id r ...)
    (interpret `((out op ,(relax-reg in) ...) ...) `(,r ...))))

; ----- BV semantics -----;

; BV comparison operators return 1/0 instead of #t/#f.
; The language is similar to the one defined in this paper:
; https://dl.acm.org/citation.cfm?id=1993506
(define int32? (bitvector 32))
(define (int32 c) (bv c int32?))
(define register? integer?)

(define-syntax-rule (bool->bv b) (if b (int32 1) (int32 0)))

(define (bvredor x)  (bveq (bveq x (int32 0)) (int32 0)))
(define (bvredand x) (bveq x (int32 -1)))

(define-syntax-rule (define-comparators [id op] ...)
  (begin
    (define (id x y) (bool->bv (op x y))) ...))

(define-comparators
  [bveq $bveq] 
  [bvslt $bvslt] [bvult $bvult]
  [bvsle $bvsle] [bvule $bvule]
  [bvsgt $bvsgt] [bvugt $bvugt]
  [bvsge $bvsge] [bvuge $bvuge])


; Global registers.
(define memory          
  (let ([m (vector)])
    (case-lambda [() m]
                 [(size) (set! m (make-vector size #f))])))

 ; Returns the contents of the register idx.    
(define (load idx)     
  (vector-ref (memory) idx))

; Stores val in the register idx.
(define (store idx val) 
  (vector-set! (memory) idx val))

; Returns the contents of the last register.   
(define (last)          
  (sub1 (vector-length (memory))))

; Creates the registers for the given program and input.
(define (make-registers prog inputs) 
  (memory (+ (length prog) (length inputs)))
  (for ([(in idx) (in-indexed inputs)])
    (store idx in)))

; The BV interpreter.
(define (interpret prog inputs)
  (make-registers prog inputs) 
  (for ([stmt prog])
    (match stmt
      [(list out opcode in ...)
       (define op (eval opcode))
       (define args (map load in))
       (store out (apply op args))]))  
  (load (last)))

; The BV verifier.
(define (ver impl spec)
  (define-symbolic* in int32? [(procedure-arity spec)])
  (evaluate in (verify (assert (equal? (apply impl in) (apply spec in))))))

; The BV debugger.
(define (dbg impl spec in)
  (render (debug [register?] (assert (equal? (apply impl in) (apply spec in))))))

; The BV synthesizer. Note that this particular implementation handles synthesis
; holes *only* in input registers; that is, instruction opcodes cannot be symbolic
; due to the use of Racket's "eval" to map opcodes to instruction procedures.
(define (syn impl spec)
  (define-symbolic* in int32? [(procedure-arity spec)])
  (print-forms
   (synthesize #:forall in
               #:guarantee (assert (equal? (apply impl in) (apply spec in))))))

; The BV angelic execution tool.
(define (sol impl spec)
  (define-symbolic* in int32? [(procedure-arity spec)])
  (evaluate in (solve (assert (equal? (apply impl in) (apply spec in))))))

; ----- BV demo -----;
(define (max x y)
  (if (equal? (bvsge x y) (int32 1)) x y))

(def/dbg bvmax 
  ([0 r0] [1 r1]) 
  (2 bvsge 0 1)
  (3 bvneg 2)
  (4 bvxor 0 2)
  (5 bvand 3 4)
  (6 bvxor 1 5))

(def bvmax??
  ([0 r0] [1 r1]) 
  (2 bvsge 0 1)
  (3 bvneg (??))
  (4 bvxor 0 (??))
  (5 bvand 3 4)
  (6 bvxor (??) 5))

; Interaction script
(ver bvmax max)

(max (bv #x7ffefbdf 32) (bv #x40000001 32))  ; spec
(bvmax (bv #x7ffefbdf 32) (bv #x40000001 32)) ; buggy impl

(dbg bvmax max (list (bv #x7ffefbdf 32) (bv #x40000001 32)))
(syn bvmax?? max)

#|
; Synthesized bvmax1
(def bvmax1
  ((0 r0) (1 r1))
  (2 bvge 0 1)
  (3 bvneg 2)
  (4 bvxor 0 1)
  (5 bvand 3 4)
  (6 bvxor 1 5))
|#

debug.rkt

#lang rosette

(require rosette/query/debug rosette/lib/render)

(define (poly x)
  (+ (* x x x x) (* 6 x x x) (* 11 x x) (* 6 x)))
 
(define/debug (fact x)
  (* x (+ x 1) (+ x 2) (+ x 2)))
 
(define (same p f x)
  (assert (= (p x) (f x))))

(render ; visualize the result
   (debug [integer?] 
     (same poly fact -6)))

finite.rkt

#lang rosette

(define (search x xs)
  (cond
    [(null? xs) #f]
    [(equal? x (car xs)) #t]
    [else (search x (cdr xs))]))

(define-symbolic xs integer? [5])
(define-symbolic xl i integer?)
(define ys (take xs xl))

(verify
 (when (<= 0 i (- xl 1)) ; <- replace with #t to get a counterexample
   (assert (search (list-ref ys i) ys))))

precision.rkt

#lang rosette

; default bitwidth is #f
(displayln "----- current-bitwidth #f -----")

(current-bitwidth)
(define-symbolic x integer?)
(solve (assert (= x 64)))
(verify (assert (not (= x 64))))

; change the bitwidth to 5
(displayln "----- current-bitwidth 5 -----")

(current-bitwidth 5)
(current-bitwidth)
(solve (assert (= x 64)))
(verify (assert (not (= x 64))))

solve.rkt

#lang rosette

(define (poly x)
  (+ (* x x x x) (* 6 x x x) (* 11 x x) (* 6 x)))

(define (fact x)
 (define-symbolic* c1 c2 c3 integer?) ; <- try define-symbolic instead
 (* (+ x c1) (+ x 1) (+ x c2) (+ x c3)))
 
(define (same p f x)
  (assert (= (p x) (f x))))

(solve (same poly fact -6)) 

(solve
 (begin
   (same poly fact -6)
   (same poly fact 12))) 

Solver-Aided-Programming-Tutorial.md

This gist contains the code examples for the Tutorial on Solver-Aided Programming presented at CAV 2019.

symbolics.rkt

#lang rosette

(define-symbolic x integer?)

(+ 1 x 2 3) ; (+ 6 x)

(define (same-x)
  (define-symbolic x integer?)
  x)

(same-x) ; x
(same-x) ; x
(eq? (same-x) (same-x)) ; #t

(define (new-x)
  (define-symbolic* x integer?)
  x)

(new-x) ; x$0
(new-x) ; x$1
(eq? (new-x) (new-x)) ; (= x$2 x$3)

(define-symbolic* xs integer? [4])
xs ; (list xs$0 xs$1 xs$2 xs$3)

(define-symbolic* len integer?)

(take xs len) ; all integer lists of length <= 4

synthax.rkt

#lang rosette

(require rosette/lib/synthax)

(define (poly x)
 (+ (* x x x x) (* 6 x x x) (* 11 x x) (* 6 x)))
 
(define (fact x)
 (* (+ x (??)) (+ x 1) (+ x (??)) (+ x (??))))
 
(define (same p f x)
 (assert (= (p x) (f x))))

(define-symbolic i integer?)

(print-forms
 (synthesize  
  #:forall i
  #:guarantee (same poly fact i)))

synthesize.rkt

#lang rosette

(define (poly x)
  (+ (* x x x x) (* 6 x x x) (* 11 x x) (* 6 x)))

(define (fact x)
 (define-symbolic c1 c2 c3 integer?) 
 (* (+ x c1) (+ x 1) (+ x c2) (+ x c3)))
 
(define (same p f x)
  (assert (= (p x) (f x))))

(define-symbolic i integer?)

(synthesize
 #:forall i
 #:guarantee (same poly fact i)) 

unbounded.rkt

#lang rosette

(define (factorial n)
  (cond [(= n 0) 1]
        [else (* n (factorial (- n 1)))]))

(factorial 3)
(factorial 4)

(define-symbolic k integer?)

(solve (assert (> (factorial k) 10)))

unsafe.rkt

#lang rosette

(define v (vector 1 2))

(define-symbolic k integer?)

(vector-ref v k) ; (ite* (⊢ (= 0 k) 1) (⊢ (= 1 k) 2)))

(define h (make-hash '((0 . 1)(1 . 2))))

(with-handlers ([exn? displayln])
  (hash-ref h k)) ; exception because hashes aren't lifted

(hash-set! h k 3) 
(hash-ref h k)    ; ok according to Racket semantics

verify.rkt

#lang rosette

(define (poly x)
  (+ (* x x x x) (* 6 x x x) (* 11 x x) (* 6 x)))
 
(define (fact x)
  (* x (+ x 1) (+ x 2) (+ x 2)))
 
(define (same p f x)
  (assert (= (p x) (f x))))

(same poly fact 0)  ; pass
(same poly fact -1) ; pass
(same poly fact -2) ; pass

(define-symbolic i integer?)

(define cex (verify (same poly fact i)))

cex               ; (model [i -6])
(evaluate i cex)  ; -6
(poly -6)         ; 360
(fact -6)         ; 480
(asserts)         ; '() 

(define-symbolic* xs integer? [4]) following code snippet throws an error, I believe it should be (define-symbolic* xs integer? #:length 4)

This tutorial is out of date: it was designed to work with Rosette 3.

Rosette 4 uses slightly different syntax and is not backward compatible with Rosette 3.

Oh! Thanks for the clarification, I loved reading your Symbolic Virtual Machine paper.