blob: 09457daeb203be00a9ffc7cb6aba56c3e5e986a7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
|
(*Generated by Sail from riscv.*)
Require Import Sail.Base.
Require Import Sail.Real.
Require Import riscv_types.
Import ListNotations.
Open Scope string.
Open Scope bool.
Open Scope Z.
Definition is_none {a : Type} (opt : option a) : bool :=
match opt with | Some _ => false | None => true end.
Definition is_some {a : Type} (opt : option a) : bool :=
match opt with | Some _ => true | None => false end.
Definition eq_unit (_ : unit) (_ : unit) : {_bool : bool & ArithFact (_bool)} := build_ex (true).
Definition neq_int (x : Z) (y : Z) : {_bool : bool & ArithFact (Bool.eqb (negb (x =? y)) _bool)} :=
build_ex (negb (Z.eqb x y)).
Definition neq_bool (x : bool) (y : bool) : bool := negb (Bool.eqb x y).
Definition __id (x : Z) : {_retval : Z & ArithFact (_retval =? x)} := build_ex (x).
Definition fdiv_int (n : Z) (m : Z) : Z :=
if sumbool_of_bool (andb (Z.ltb n 0) (Z.gtb m 0)) then Z.sub (Z.quot (Z.add n 1) m) 1
else if sumbool_of_bool (andb (Z.gtb n 0) (Z.ltb m 0)) then Z.sub (Z.quot (Z.sub n 1) m) 1
else Z.quot n m.
Definition fmod_int (n : Z) (m : Z) : Z := Z.sub n (Z.mul m (fdiv_int n m)).
Definition concat_str_bits {n : Z} (str : string) (x : mword n) : string :=
String.append str (string_of_bits x).
Definition concat_str_dec (str : string) (x : Z) : string := String.append str (dec_str x).
Definition sail_mask {v0 : Z} (len : Z) (v : mword v0) `{ArithFact ((len >=? 0) && (v0 >=? 0))}
: mword len :=
if sumbool_of_bool (Z.leb len (length_mword v)) then vector_truncate v len else zero_extend v len.
Definition sail_ones (n : Z) `{ArithFact (n >=? 0)} : mword n := not_vec (zeros n).
Definition slice_mask (n : Z) (i : Z) (l : Z) `{ArithFact (n >=? 0)} : mword n :=
if sumbool_of_bool (Z.geb l n) then shiftl (sail_ones n) i
else
let one : bits n := sail_mask n ('b"1" : bits 1) in
shiftl (sub_vec (shiftl one l) one) i.
Definition EXTS {n : Z} (m : Z) (v : mword n) `{ArithFact (m >=? n)} : mword m := sign_extend v m.
Definition EXTZ {n : Z} (m : Z) (v : mword n) `{ArithFact (m >=? n)} : mword m := zero_extend v m.
Definition zero_reg : regtype := EXTZ 64 (Ox"0" : mword 4).
Hint Unfold zero_reg : sail.
Definition regval_from_reg (r : mword 64) : mword 64 := r.
Definition regval_into_reg (v : mword 64) : mword 64 := v.
Definition rX (r : Z) `{ArithFact ((0 <=? r) && (r <? 32))} : M (mword 64) :=
let l__32 := r in
(if sumbool_of_bool (Z.eqb l__32 0) then returnm zero_reg
else if sumbool_of_bool (Z.eqb l__32 1) then ((read_reg x1_ref) : M (mword 64)) : M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 2) then ((read_reg x2_ref) : M (mword 64)) : M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 3) then ((read_reg x3_ref) : M (mword 64)) : M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 4) then ((read_reg x4_ref) : M (mword 64)) : M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 5) then ((read_reg x5_ref) : M (mword 64)) : M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 6) then ((read_reg x6_ref) : M (mword 64)) : M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 7) then ((read_reg x7_ref) : M (mword 64)) : M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 8) then ((read_reg x8_ref) : M (mword 64)) : M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 9) then ((read_reg x9_ref) : M (mword 64)) : M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 10) then
((read_reg x10_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 11) then
((read_reg x11_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 12) then
((read_reg x12_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 13) then
((read_reg x13_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 14) then
((read_reg x14_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 15) then
((read_reg x15_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 16) then
((read_reg x16_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 17) then
((read_reg x17_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 18) then
((read_reg x18_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 19) then
((read_reg x19_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 20) then
((read_reg x20_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 21) then
((read_reg x21_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 22) then
((read_reg x22_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 23) then
((read_reg x23_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 24) then
((read_reg x24_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 25) then
((read_reg x25_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 26) then
((read_reg x26_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 27) then
((read_reg x27_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 28) then
((read_reg x28_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 29) then
((read_reg x29_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 30) then
((read_reg x30_ref) : M (mword 64))
: M (mword 64)
else if sumbool_of_bool (Z.eqb l__32 31) then
((read_reg x31_ref) : M (mword 64))
: M (mword 64)
else assert_exp' false "invalid register number" >>= fun _ => exit tt) >>= fun v : regtype =>
returnm (regval_from_reg v).
Definition wX (r : Z) (in_v : mword 64) `{ArithFact ((0 <=? r) && (r <? 32))} : M (unit) :=
let v := regval_into_reg in_v in
let l__0 := r in
(if sumbool_of_bool (Z.eqb l__0 0) then returnm tt
else if sumbool_of_bool (Z.eqb l__0 1) then write_reg x1_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 2) then write_reg x2_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 3) then write_reg x3_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 4) then write_reg x4_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 5) then write_reg x5_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 6) then write_reg x6_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 7) then write_reg x7_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 8) then write_reg x8_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 9) then write_reg x9_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 10) then write_reg x10_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 11) then write_reg x11_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 12) then write_reg x12_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 13) then write_reg x13_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 14) then write_reg x14_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 15) then write_reg x15_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 16) then write_reg x16_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 17) then write_reg x17_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 18) then write_reg x18_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 19) then write_reg x19_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 20) then write_reg x20_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 21) then write_reg x21_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 22) then write_reg x22_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 23) then write_reg x23_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 24) then write_reg x24_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 25) then write_reg x25_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 26) then write_reg x26_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 27) then write_reg x27_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 28) then write_reg x28_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 29) then write_reg x29_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 30) then write_reg x30_ref v : M (unit)
else if sumbool_of_bool (Z.eqb l__0 31) then write_reg x31_ref v : M (unit)
else assert_exp' false "invalid register number" >>= fun _ => exit tt)
: M (unit).
Definition rX_bits (i : mword 5) : M (mword 64) := (rX (projT1 (uint i))) : M (mword 64).
Definition wX_bits (i : mword 5) (data : mword 64) : M (unit) :=
(wX (projT1 (uint i)) data) : M (unit).
Definition reg_name_abi (r : mword 5) : M (string) :=
let b__0 := r in
(if eq_vec b__0 ('b"00000" : mword 5) then returnm "zero"
else if eq_vec b__0 ('b"00001" : mword 5) then returnm "ra"
else if eq_vec b__0 ('b"00010" : mword 5) then returnm "sp"
else if eq_vec b__0 ('b"00011" : mword 5) then returnm "gp"
else if eq_vec b__0 ('b"00100" : mword 5) then returnm "tp"
else if eq_vec b__0 ('b"00101" : mword 5) then returnm "t0"
else if eq_vec b__0 ('b"00110" : mword 5) then returnm "t1"
else if eq_vec b__0 ('b"00111" : mword 5) then returnm "t2"
else if eq_vec b__0 ('b"01000" : mword 5) then returnm "fp"
else if eq_vec b__0 ('b"01001" : mword 5) then returnm "s1"
else if eq_vec b__0 ('b"01010" : mword 5) then returnm "a0"
else if eq_vec b__0 ('b"01011" : mword 5) then returnm "a1"
else if eq_vec b__0 ('b"01100" : mword 5) then returnm "a2"
else if eq_vec b__0 ('b"01101" : mword 5) then returnm "a3"
else if eq_vec b__0 ('b"01110" : mword 5) then returnm "a4"
else if eq_vec b__0 ('b"01111" : mword 5) then returnm "a5"
else if eq_vec b__0 ('b"10000" : mword 5) then returnm "a6"
else if eq_vec b__0 ('b"10001" : mword 5) then returnm "a7"
else if eq_vec b__0 ('b"10010" : mword 5) then returnm "s2"
else if eq_vec b__0 ('b"10011" : mword 5) then returnm "s3"
else if eq_vec b__0 ('b"10100" : mword 5) then returnm "s4"
else if eq_vec b__0 ('b"10101" : mword 5) then returnm "s5"
else if eq_vec b__0 ('b"10110" : mword 5) then returnm "s6"
else if eq_vec b__0 ('b"10111" : mword 5) then returnm "s7"
else if eq_vec b__0 ('b"11000" : mword 5) then returnm "s8"
else if eq_vec b__0 ('b"11001" : mword 5) then returnm "s9"
else if eq_vec b__0 ('b"11010" : mword 5) then returnm "s10"
else if eq_vec b__0 ('b"11011" : mword 5) then returnm "s11"
else if eq_vec b__0 ('b"11100" : mword 5) then returnm "t3"
else if eq_vec b__0 ('b"11101" : mword 5) then returnm "t4"
else if eq_vec b__0 ('b"11110" : mword 5) then returnm "t5"
else if eq_vec b__0 ('b"11111" : mword 5) then returnm "t6"
else
assert_exp' false "Pattern match failure at riscv_regs.sail 160:2 - 193:3" >>= fun _ =>
exit tt)
: M (string).
Definition init_base_regs '(tt : unit) : M (unit) :=
write_reg x1_ref zero_reg >>
write_reg x2_ref zero_reg >>
write_reg x3_ref zero_reg >>
write_reg x4_ref zero_reg >>
write_reg x5_ref zero_reg >>
write_reg x6_ref zero_reg >>
write_reg x7_ref zero_reg >>
write_reg x8_ref zero_reg >>
write_reg x9_ref zero_reg >>
write_reg x10_ref zero_reg >>
write_reg x11_ref zero_reg >>
write_reg x12_ref zero_reg >>
write_reg x13_ref zero_reg >>
write_reg x14_ref zero_reg >>
write_reg x15_ref zero_reg >>
write_reg x16_ref zero_reg >>
write_reg x17_ref zero_reg >>
write_reg x18_ref zero_reg >>
write_reg x19_ref zero_reg >>
write_reg x20_ref zero_reg >>
write_reg x21_ref zero_reg >>
write_reg x22_ref zero_reg >>
write_reg x23_ref zero_reg >>
write_reg x24_ref zero_reg >>
write_reg x25_ref zero_reg >>
write_reg x26_ref zero_reg >>
write_reg x27_ref zero_reg >>
write_reg x28_ref zero_reg >>
write_reg x29_ref zero_reg >>
write_reg x30_ref zero_reg >> write_reg x31_ref zero_reg : M (unit).
Definition initial_regstate : regstate :=
{| x31 := (Ox"0000000000000000" : mword 64);
x30 := (Ox"0000000000000000" : mword 64);
x29 := (Ox"0000000000000000" : mword 64);
x28 := (Ox"0000000000000000" : mword 64);
x27 := (Ox"0000000000000000" : mword 64);
x26 := (Ox"0000000000000000" : mword 64);
x25 := (Ox"0000000000000000" : mword 64);
x24 := (Ox"0000000000000000" : mword 64);
x23 := (Ox"0000000000000000" : mword 64);
x22 := (Ox"0000000000000000" : mword 64);
x21 := (Ox"0000000000000000" : mword 64);
x20 := (Ox"0000000000000000" : mword 64);
x19 := (Ox"0000000000000000" : mword 64);
x18 := (Ox"0000000000000000" : mword 64);
x17 := (Ox"0000000000000000" : mword 64);
x16 := (Ox"0000000000000000" : mword 64);
x15 := (Ox"0000000000000000" : mword 64);
x14 := (Ox"0000000000000000" : mword 64);
x13 := (Ox"0000000000000000" : mword 64);
x12 := (Ox"0000000000000000" : mword 64);
x11 := (Ox"0000000000000000" : mword 64);
x10 := (Ox"0000000000000000" : mword 64);
x9 := (Ox"0000000000000000" : mword 64);
x8 := (Ox"0000000000000000" : mword 64);
x7 := (Ox"0000000000000000" : mword 64);
x6 := (Ox"0000000000000000" : mword 64);
x5 := (Ox"0000000000000000" : mword 64);
x4 := (Ox"0000000000000000" : mword 64);
x3 := (Ox"0000000000000000" : mword 64);
x2 := (Ox"0000000000000000" : mword 64);
x1 := (Ox"0000000000000000" : mword 64);
instbits := (Ox"0000000000000000" : mword 64);
nextPC := (Ox"0000000000000000" : mword 64);
PC := (Ox"0000000000000000" : mword 64) |}.
Hint Unfold initial_regstate : sail.
|
