]> Witch of Git - jade-mouse/blob - isa-synthesis.rkt
Add instruction program synthesis
[jade-mouse] / 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!"))