Witch of Git - jade-mouse/blob - isa-synthesis.rkt

   1 #lang rosette/safe
   2
   3 (require rosette/lib/angelic
   4          rosette/lib/match)
   5 (require "synthesis-base.rkt")
   6 (current-bitwidth #f)
   7
   8 ; Most of the setup taken from Whitequark's synthesis demo
   9 ; https://gist.github.com/whitequark/1f7cc43c1cc2b179a1d4a668f0089804
  10
  11 #;(define (rotate-right i x)
  12   (define s (bitvector-size (type-of x)))
  13   (concat (extract (- i 1) 0 x) (extract (- s 1) i x)))
  14 (define (rotate-left i x)
  15   (define s (bitvector-size (type-of x)))
  16   (concat (extract (- s i 1) 0 x) (extract (- s 1) (- s i) x)))
  17
  18 (struct state (reg mem) #:mutable #:transparent)
  19 (define (reg-ref S n) (vector-ref (state-reg S) n))
  20 (define (reg-set! S n v) (vector-set! (state-reg S) n v))
  21 (define (mem-ref S addr) (vector-ref (state-mem S) addr))
  22 (define (mem-set! S addr v) (vector-set! (state-mem S) addr v))
  23
  24 (define-symbolic R0 R1 R2 R3 M0 M1 (bitvector 8))
  25 (define (make-state)
  26   (state (vector R0 R1 R2 R3)
  27          (vector M0 M1)))
  28
  29 (define (bv8 val) (bv val 8))
  30 (define (choose-imm* w)
  31   (choose* (bv8 #x00) (bv8 #x01) (bv8 #x03) (bv8 #x07)
  32            (bv8 #x0f) (bv8 #x1f) (bv8 #x3f) (bv8 #x7f)
  33            (bv8 #xff) (bv8 #xfe) (bv8 #xfc) (bv8 #xf8)
  34            (bv8 #xf0) (bv8 #xe0) (bv8 #xc0) (bv8 #x80)))
  35 #;(define (choose-imm* w)
  36   (define-symbolic* b (bitvector w))
  37   b)
  38 (define (choose-shift*)
  39   (define-symbolic* b (bitvector 3))
  40   b)
  41 #;(define (choose-imm*)
  42   (choose* (bv8 #x01)))
  43
  44 (struct LSL (a imm) #:transparent)
  45 (struct LSR (a imm) #:transparent)
  46 (struct ASR (a imm) #:transparent)
  47 (struct ROL (a imm) #:transparent)
  48 (struct OR (a b) #:transparent)
  49 (struct ORI (a imm) #:transparent)
  50 (struct AND (a b) #:transparent)
  51 (struct ANDI (a imm) #:transparent)
  52 (struct LD0 (a addr) #:transparent)
  53 (struct ST0 (a addr) #:transparent)
  54 (struct MOV (a b) #:transparent)
  55
  56 (define (format-insn insn)
  57   (define nat bitvector->natural)
  58   (match insn
  59     [(LSL a imm) (format "r~s = r~s lsl #~s" a a (nat imm))]
  60     [(LSR a imm) (format "r~s = r~s lsr #~s" a a (nat imm))]
  61     [(ASR a imm) (format "r~s = r~s asr #~s" a a (nat imm))]
  62     [(ROL a imm) (format "r~s = r~s rol #~s" a a (nat imm))]
  63     [(OR a b) (format "r~s = r~s or r~s" a a b)]
  64     [(ORI a imm) (format "r~s = r~s or #~s" a a (nat imm))]
  65     [(AND a b) (format "r~s = r~s and r~s" a a b)]
  66     [(ANDI a imm) (format "r~s = r~s and #~s" a a (nat imm))]
  67     [(LD0 a addr) (format "r~s = [#~s]" a addr)]
  68     [(ST0 a addr) (format "[#~s] = r~s" addr a)]
  69     [(MOV a b) (format "r~s = r~s" a b)]
  70     ))
  71
  72 (define (print-insn insn)
  73   (displayln (format-insn insn)))
  74
  75 (define (print-prog prog)
  76   (for-each print-insn prog))
  77
  78 (define (??insn)
  79   (let ([a (choose* 0 1 2 3)]
  80         [b (choose* 0 1 2 3)]
  81         [imm8 (choose-imm* 8)]
  82         [addr (choose* 0)]
  83         ;[imm7 (choose-imm* 7)]
  84         ;[imm6 (choose-imm* 6)]
  85         [imm3 (choose-shift*)])
  86     (choose* (LSL a imm3)
  87              (LSR a imm3)
  88              ;(ASR a imm3)
  89              ;(ROL a imm3)
  90              (OR a b)
  91              ;(ORI a imm8)
  92              ;(AND a b)
  93              (ANDI a imm8)
  94              (LD0 a addr)
  95              (ST0 a addr)
  96              (MOV a b)
  97              )))
  98
  99 (define (run-insn S insn)
 100   (match insn
 101     [(LSL a imm)
 102      (let ([va (reg-ref S a)]
 103            [shift (zero-extend imm (bitvector 8))])
 104        (reg-set! S a (bvshl va shift)))]
 105     [(LSR a imm)
 106      (let ([va (reg-ref S a)]
 107            [shift (zero-extend imm (bitvector 8))])
 108        (reg-set! S a (bvlshr va shift)))]
 109     [(ASR a imm)
 110      (let ([va (reg-ref S a)]
 111            [shift (zero-extend imm (bitvector 8))])
 112        (reg-set! S a (bvashr va shift)))]
 113     [(ROL a imm)
 114      (let ([va (reg-ref S a)]
 115            [shift (bitvector->natural imm)])
 116        (reg-set! S a (rotate-left imm va)))]
 117     [(OR a b)
 118      (let ([va (reg-ref S a)]
 119            [vb (reg-ref S b)])
 120        (reg-set! S a (bvor va vb)))]
 121     [(ORI a imm)
 122      (let ([va (reg-ref S a)])
 123        (reg-set! S a (bvor va imm)))]
 124     [(AND a b)
 125      (let ([va (reg-ref S a)]
 126            [vb (reg-ref S b)])
 127        (reg-set! S a (bvand va vb)))]
 128     [(ANDI a imm)
 129      (let ([va (reg-ref S a)])
 130        (reg-set! S a (bvand va imm)))]
 131     [(LD0 a addr)
 132      (reg-set! S a (mem-ref S addr))]
 133     [(ST0 a addr)
 134      (mem-set! S addr (reg-ref S a))]
 135     [(MOV a b)
 136      (reg-set! S a (reg-ref S b))]
 137   ))
 138
 139 (define (assert-preserve S S* . regs)
 140   (define (assert-preserve-reg n)
 141     (assert (bveq (reg-ref S n) (reg-ref S* n))))
 142   (for-each assert-preserve-reg regs))
 143
 144 (define found-prog
 145   (optimize-prog 12 make-state run-insn
 146     (lambda (fuel) (??prog ??insn fuel))
 147     (lambda (S S*)
 148       (define R  (concat (reg-ref S  2) (reg-ref S  1) (reg-ref S  0)))
 149       (define R* (concat (reg-ref S* 2) (reg-ref S* 1) (reg-ref S* 0)))
 150       (assert (bveq (bvshl R (bv 4 24)) R*))
 151       (assert-preserve S S* 3)
 152       )))
 153
 154 (if found-prog
 155     (print-prog found-prog)
 156     (displayln "No program found!"))