1(model Imm64 (type (bv 64)))
2
3(model IntCC (enum
4    (Equal #x00)
5    (NotEqual #x01)
6    (SignedGreaterThan #x02)
7    (SignedGreaterThanOrEqual #x03)
8    (SignedLessThan #x04)
9    (SignedLessThanOrEqual #x05)
10    (UnsignedGreaterThan #x06)
11    (UnsignedGreaterThanOrEqual #x07)
12    (UnsignedLessThan #x08)
13    (UnsignedLessThanOrEqual #x09)))
14
15(spec (smin x y)
16    (provide (= result (if (bvsle x y) x y))))
17(instantiate smin bv_binary_8_to_64)
18
19(spec (umin x y)
20    (provide (= result (if (bvule x y) x y))))
21(instantiate umin bv_binary_8_to_64)
22
23(spec (smax x y)
24    (provide (= result (if (bvsge x y) x y))))
25(instantiate smax bv_binary_8_to_64)
26
27(spec (umax x y)
28    (provide (= result (if (bvuge x y) x y))))
29(instantiate umax bv_binary_8_to_64)
30
31(spec (iconst arg)
32    (provide (= arg (zero_ext 64 result))))
33(instantiate iconst
34    ((args (bv 64)) (ret (bv 8)) (canon (bv 8)))
35    ((args (bv 64)) (ret (bv 16)) (canon (bv 16)))
36    ((args (bv 64)) (ret (bv 32)) (canon (bv 32)))
37    ((args (bv 64)) (ret (bv 64)) (canon (bv 64)))
38)
39
40(spec (bitselect c x y)
41    (provide (= result (bvor (bvand c x) (bvand (bvnot c) y)))))
42(instantiate bitselect bv_ternary_8_to_64)
43
44(spec (icmp c x y)
45    (provide
46        (= result
47            (switch c
48                ((IntCC.Equal) (if (= x y) #x01 #x00))
49                ((IntCC.NotEqual) (if (not (= x y)) #x01 #x00))
50                ((IntCC.SignedGreaterThan) (if (bvsgt x y) #x01 #x00))
51                ((IntCC.SignedGreaterThanOrEqual) (if (bvsge x y) #x01 #x00))
52                ((IntCC.SignedLessThan) (if (bvslt x y) #x01 #x00))
53                ((IntCC.SignedLessThanOrEqual) (if (bvsle x y) #x01 #x00))
54                ((IntCC.UnsignedGreaterThan) (if (bvugt x y) #x01 #x00))
55                ((IntCC.UnsignedGreaterThanOrEqual) (if (bvuge x y) #x01 #x00))
56                ((IntCC.UnsignedLessThan) (if (bvult x y) #x01 #x00))
57                ((IntCC.UnsignedLessThanOrEqual) (if (bvule x y) #x01 #x00)))))
58    (require
59        ;; AVH TODO: if we understand enums semantically, we can generate this
60        (or
61            (= c (IntCC.Equal))
62            (= c (IntCC.NotEqual))
63            (= c (IntCC.UnsignedGreaterThanOrEqual))
64            (= c (IntCC.UnsignedGreaterThan))
65            (= c (IntCC.UnsignedLessThanOrEqual))
66            (= c (IntCC.UnsignedLessThan))
67            (= c (IntCC.SignedGreaterThanOrEqual))
68            (= c (IntCC.SignedGreaterThan))
69            (= c (IntCC.SignedLessThanOrEqual))
70            (= c (IntCC.SignedLessThan)))))
71(instantiate icmp
72    ((args (bv 8) (bv 8) (bv 8)) (ret (bv 8)) (canon (bv 8)))
73    ((args (bv 8) (bv 16) (bv 16)) (ret (bv 8)) (canon (bv 16)))
74    ((args (bv 8) (bv 32) (bv 32)) (ret (bv 8)) (canon (bv 32)))
75    ((args (bv 8) (bv 64) (bv 64)) (ret (bv 8)) (canon (bv 64)))
76)
77
78(spec (iadd x y)
79    (provide (= result (bvadd x y))))
80(instantiate iadd bv_binary_8_to_64)
81
82(spec (isub x y)
83    (provide (= result (bvsub x y))))
84(instantiate isub bv_binary_8_to_64)
85
86(spec (ineg x)
87    (provide (= result (bvneg x))))
88(instantiate ineg bv_unary_8_to_64)
89
90(spec (iabs x)
91    (provide (= result
92                (if (bvsge x (conv_to (widthof x) #x0000000000000000))
93                    x
94                    (bvneg x)))))
95(instantiate iabs bv_unary_8_to_64)
96
97(spec (imul x y)
98    (provide (= result (bvmul x y))))
99(instantiate imul bv_binary_8_to_64)
100
101(spec (udiv x y)
102    (provide (= result (bvudiv x y)))
103    (require (not (= y (zero_ext (widthof y) #b0)))))
104(instantiate udiv bv_binary_8_to_64)
105
106(spec (sdiv x y)
107    (provide (= result (bvsdiv x y)))
108    (require (not (= y (zero_ext (widthof y) #b0)))))
109(instantiate sdiv bv_binary_8_to_64)
110
111(spec (urem x y)
112    (provide (= result (bvurem x y)))
113    (require (not (= y (zero_ext (widthof y) #b0)))))
114(instantiate urem bv_binary_8_to_64)
115
116(spec (srem x y)
117    (provide (= result (bvsrem x y)))
118    (require (not (= y (zero_ext (widthof y) #b0)))))
119(instantiate srem bv_binary_8_to_64)
120
121(spec (imul_imm x y)
122    (provide (= result (bvmul (sign_ext 64 x) y))))
123
124(spec (band x y)
125    (provide (= result (bvand x y))))
126(instantiate band bv_binary_8_to_64)
127
128(spec (bor x y)
129    (provide (= result (bvor x y))))
130(instantiate bor bv_binary_8_to_64)
131
132(spec (bxor x y)
133    (provide (= result (bvxor x y))))
134(instantiate bxor bv_binary_8_to_64)
135
136(spec (bnot x)
137    (provide (= result (bvnot x)))
138    (require (or (= (widthof x) 8) (= (widthof x) 16) (= (widthof x) 32) (= (widthof x) 64))))
139(instantiate bnot bv_unary_8_to_64)
140
141(spec (band_not x y)
142    (provide (= result (bvand x (bvnot y)))))
143(instantiate band_not bv_binary_8_to_64)
144
145(spec (rotl x y)
146    (provide (= result (rotl x y))))
147(instantiate rotl bv_binary_8_to_64)
148
149(spec (rotr x y)
150    (provide (= result (rotr x y))))
151(instantiate rotr bv_binary_8_to_64)
152
153;; fn shift_mask(&mut self, ty: Type) -> ImmLogic {
154;;     let mask = (ty.lane_bits() - 1) as u64;
155;;     ImmLogic::maybe_from_u64(mask, I32).unwrap()
156;; }
157(spec (ishl x y)
158    (provide
159        (= result
160           (bvshl x
161                  (bvand (conv_to (widthof y) (bvsub (int2bv 64 (widthof y))
162                                                     #x0000000000000001))
163                         y)))))
164(instantiate ishl bv_binary_8_to_64)
165
166(spec (ushr x y)
167    (provide
168        (= result
169           (bvlshr x
170                  (bvand (conv_to (widthof y) (bvsub (int2bv 64 (widthof y))
171                                                     #x0000000000000001))
172                         y)))))
173(instantiate ushr bv_binary_8_to_64)
174
175(spec (sshr x y)
176    (provide
177        (= result
178           (bvashr x
179                  (bvand (conv_to (widthof y) (bvsub (int2bv 64 (widthof y))
180                                                     #x0000000000000001))
181                         y)))))
182(instantiate sshr bv_binary_8_to_64)
183
184(spec (clz x)
185    (provide (= result (clz x))))
186(instantiate clz bv_unary_8_to_64)
187
188(spec (cls x)
189    (provide (= result (cls x))))
190(instantiate cls bv_unary_8_to_64)
191
192(spec (ctz x)
193    (provide (= result (clz (rev x)))))
194(instantiate ctz bv_unary_8_to_64)
195
196(spec (popcnt x)
197    (provide (= result (popcnt x))))
198(instantiate popcnt bv_unary_8_to_64)
199
200(form extend
201    ((args (bv 8)) (ret (bv 8)) (canon (bv 8)))
202    ((args (bv 8)) (ret (bv 16)) (canon (bv 8)))
203    ((args (bv 8)) (ret (bv 32)) (canon (bv 8)))
204    ((args (bv 8)) (ret (bv 64)) (canon (bv 8)))
205    ((args (bv 16)) (ret (bv 16)) (canon (bv 16)))
206    ((args (bv 16)) (ret (bv 32)) (canon (bv 16)))
207    ((args (bv 16)) (ret (bv 64)) (canon (bv 16)))
208    ((args (bv 32)) (ret (bv 32)) (canon (bv 32)))
209    ((args (bv 32)) (ret (bv 64)) (canon (bv 32)))
210    ((args (bv 64)) (ret (bv 64)) (canon (bv 64)))
211)
212
213(spec (uextend x)
214    (provide (= result (zero_ext (widthof result) x))))
215(instantiate uextend extend)
216
217(spec (sextend x)
218    (provide (= result (sign_ext (widthof result) x))))
219(instantiate sextend extend)
220
221
222(form load
223    ((args (bv 16) (bv 64) (bv 32)) (ret (bv 8)) (canon (bv 8)))
224    ((args (bv 16) (bv 64) (bv 32)) (ret (bv 16)) (canon (bv 16)))
225    ((args (bv 16) (bv 64) (bv 32)) (ret (bv 32)) (canon (bv 32)))
226    ((args (bv 16) (bv 64) (bv 32)) (ret (bv 64)) (canon (bv 64)))
227)
228(spec (load flags val offset)
229    (provide
230       (= result (load_effect flags (widthof result) (bvadd val (sign_ext 64 offset))))))
231(instantiate load load)
232
233(form store
234    ((args (bv 16) (bv 8) (bv 64) (bv 32)) (ret Unit) (canon (bv 8)))
235    ((args (bv 16) (bv 16) (bv 64) (bv 32)) (ret Unit) (canon (bv 16)))
236    ((args (bv 16) (bv 32) (bv 64) (bv 32)) (ret Unit) (canon (bv 32)))
237    ((args (bv 16) (bv 64) (bv 64) (bv 32)) (ret Unit) (canon (bv 64)))
238)
239(spec (store flags val_to_store addr offset)
240    (provide
241       (= result (store_effect flags (widthof val_to_store) val_to_store (bvadd (zero_ext 64 addr) (sign_ext 64 offset))))))
242(instantiate store store)
243