synth51.rkt

#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*))))