Skip to content

Instantly share code, notes, and snippets.

@whitequark
Last active February 9, 2020 07:34
Show Gist options
  • Save whitequark/1f7cc43c1cc2b179a1d4a668f0089804 to your computer and use it in GitHub Desktop.
Save whitequark/1f7cc43c1cc2b179a1d4a668f0089804 to your computer and use it in GitHub Desktop.
#lang rosette/safe
(require rosette/lib/angelic
rosette/lib/match)
(current-bitwidth #f)
(require (only-in racket list*))
; bit operations
(define (rotate-right i x)
(define s (bitvector-size (type-of x)))
(concat (extract (- i 1) 0 x) (extract (- s 1) i x)))
(define (rotate-left i x)
(define s (bitvector-size (type-of x)))
(concat (extract (- s i 1) 0 x) (extract (- s 1) (- s i) x)))
(define (replace-bit s i x y)
(define m (bvshl (bv 1 s) (integer->bitvector i s)))
(cond
[(bveq y (bv 0 1)) (bvand x (bvnot m))]
[(bveq y (bv 1 1)) (bvor x m)]
[else (assert #f)]))
; CPU state
(struct state (A C Rn) #:mutable #:transparent)
(define (state-Rn-ref S n)
(vector-ref (state-Rn S) n))
(define (state-Rn-set! S n v)
(vector-set! (state-Rn S) n v))
(define (state-R0 S) (state-Rn-ref S 0))
(define (state-R1 S) (state-Rn-ref S 1))
(define (state-R2 S) (state-Rn-ref S 2))
(define (state-R3 S) (state-Rn-ref S 3))
(define (state-R4 S) (state-Rn-ref S 4))
(define (state-R5 S) (state-Rn-ref S 5))
(define (state-R6 S) (state-Rn-ref S 6))
(define (state-R7 S) (state-Rn-ref S 7))
(define-symbolic A R0 R1 R2 R3 R4 R5 R6 R7 (bitvector 8))
(define-symbolic C (bitvector 1))
(define (make-state)
(state A C (vector R0 R1 R2 R3 R4 R5 R6 R7)))
; instructions
(struct MOV-A-Rn (n) #:transparent)
(struct MOV-Rn-A (n) #:transparent)
(struct XRL-A-Rn (n) #:transparent)
(struct XCH-A-Rn (n) #:transparent)
(struct CLR-C () #:transparent)
(struct MOV-C-An (n) #:transparent)
(struct MOV-An-C (n) #:transparent)
(struct RLC-A () #:transparent)
(struct RRC-A () #:transparent)
(struct RL-A () #:transparent)
(struct RR-A () #:transparent)
(define (print-insn insn)
(match insn
[(MOV-A-Rn n) (printf "MOV A, R~s~n" n)]
[(MOV-Rn-A n) (printf "MOV R~s, A~n" n)]
[(XRL-A-Rn n) (printf "XRL A, R~s~n" n)]
[(XCH-A-Rn n) (printf "XCH A, R~s~n" n)]
[(CLR-C) (printf "CLR C~n")]
[(MOV-C-An n) (printf "MOV C, ACC.~s~n" n)]
[(MOV-An-C n) (printf "MOV ACC.~s, C~n" n)]
[(RLC-A) (printf "RLC A~n")]
[(RRC-A) (printf "RRC A~n")]
[(RL-A) (printf "RL A~n")]
[(RR-A) (printf "RR A~n")]))
; sketches
(define (??insn)
(let ([n (choose* 0 1 2 3 4 5 6 7)])
(choose* (MOV-A-Rn n)
(MOV-Rn-A n)
(XRL-A-Rn n)
(XCH-A-Rn n)
(CLR-C)
(MOV-C-An n)
(MOV-An-C n)
(RLC-A)
(RRC-A)
(RL-A)
(RR-A)
)))
(define (??prog fuel)
(if (= fuel 0) null
(cons (??insn) (??prog (- fuel 1)))))
; symbolic interpreter
(define (run-insn S insn)
(match insn
[(MOV-A-Rn n)
(set-state-A! S (state-Rn-ref S n))]
[(MOV-Rn-A n)
(state-Rn-set! S n (state-A S))]
[(XRL-A-Rn n)
(set-state-A! S (bvxor (state-A S) (state-Rn-ref S n)))]
[(XCH-A-Rn n)
(let ([A (state-A S)] [Rn (state-Rn-ref S n)])
(set-state-A! S Rn) (state-Rn-set! S n A))]
[(CLR-C)
(set-state-C! S (bv 0 1))]
[(MOV-C-An n)
(set-state-C! S (extract n n (state-A S)))]
[(MOV-An-C n)
(set-state-A! S (replace-bit 8 n (state-A S) (state-C S)))]
[(RLC-A)
(let ([A (state-A S)] [C (state-C S)])
(set-state-A! S (concat (extract 6 0 A) C))
(set-state-C! S (extract 7 7 A)))]
[(RRC-A)
(let ([A (state-A S)] [C (state-C S)])
(set-state-A! S (concat C (extract 7 1 A)))
(set-state-C! S (extract 0 0 A)))]
[(RL-A)
(let ([A (state-A S)])
(set-state-A! S (concat (extract 6 0 A) (extract 7 7 A))))]
[(RR-A)
(let ([A (state-A S)])
(set-state-A! S (concat (extract 0 0 A) (extract 7 1 A))))]
))
; program verifier
(define (verify-prog prog asserts)
(define S (make-state))
(define S* (make-state))
(define solution
(verify
#:guarantee
(begin
(for-each (curry run-insn S*) prog)
(asserts S S*))))
(if (unsat? solution) #t
(begin
(displayln (evaluate S solution))
(displayln (evaluate S* solution))
#f)))
; program synthesizer
(define (synthesize-prog sketch asserts)
(define S (make-state))
(define S* (make-state))
(define solution
(synthesize
#:forall S
#:guarantee
(begin
(for-each (curry run-insn S*) sketch)
(asserts S S*))))
(if (unsat? solution) #f
(begin
(for-each print-insn (evaluate sketch solution))
#t)))
(define (optimize-prog max-fuel sketch-gen asserts)
(define (worker fuel)
(printf "fuel ~s~n" fuel)
(if (synthesize-prog (sketch-gen fuel) asserts) #t
(if (>= fuel max-fuel) #f
(worker (+ fuel 1)))))
(worker 0))
(define (assert-preserve S S* . regs)
(define (assert-preserve-reg n)
(assert (bveq (state-Rn-ref S n) (state-Rn-ref S* n))))
(for-each assert-preserve-reg regs))
; examples
(optimize-prog 10
(lambda (fuel)
(??prog fuel))
(lambda (S S*)
(define R10 (concat (state-R1 S ) (state-R0 S )))
(define R10* (concat (state-R1 S*) (state-R0 S*)))
(assert (bveq (rotate-right 1 R10) R10*))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment