1
2open HolKernel boolLib bossLib Parse;
3open wordsTheory bit_listTheory;
4
5open ppc_coretypesTheory ppc_astTheory;
6
7open ppc_seq_monadTheory;
8
9val _ = new_theory "ppc_opsem";
10
11
12(* ---------------------------------------------------------------------------------- *>
13
14  We define the semantics of an instruction.
15
16<* ---------------------------------------------------------------------------------- *)
17
18val ppc_sint_cmp_def = Define `
19  ppc_sint_cmp ii (a:word32) (b:word32) =
20    (parT_unit (write_status ii (PPC_CR0 0w) (SOME (a < b)))
21    (parT_unit (write_status ii (PPC_CR0 1w) (SOME (b < a)))
22    (parT_unit (write_status ii (PPC_CR0 2w) (SOME (a = b)))
23               (write_status ii (PPC_CR0 3w) NONE))))`;
24
25val ppc_uint_cmp_def = Define `
26  ppc_uint_cmp ii (a:word32) (b:word32) =
27    (parT_unit (write_status ii (PPC_CR0 0w) (SOME (a <+ b)))
28    (parT_unit (write_status ii (PPC_CR0 1w) (SOME (b <+ a)))
29    (parT_unit (write_status ii (PPC_CR0 2w) (SOME (a = b)))
30               (write_status ii (PPC_CR0 3w) NONE))))`;
31
32val ppc_clear_CR0_def = Define `
33  ppc_clear_CR0 ii =
34    (parT_unit (write_status ii (PPC_CR0 0w) NONE)
35    (parT_unit (write_status ii (PPC_CR0 1w) NONE)
36    (parT_unit (write_status ii (PPC_CR0 2w) NONE)
37               (write_status ii (PPC_CR0 3w) NONE))))`;
38
39val OK_nextinstr_def = Define `
40  OK_nextinstr ii f =
41    parT_unit f (seqT (read_reg ii PPC_PC) (\x. write_reg ii PPC_PC (x + 4w)))`;
42
43val reg_update_def = Define `
44  reg_update ii rd f s1 s2 =
45    seqT (parT s1 s2) (\(x,y). write_reg ii (PPC_IR rd) (f x y))`;
46
47val uint_reg_update_def = Define `
48  uint_reg_update ii rd f s1 s2 =
49    seqT (parT s1 s2)
50         (\(x,y). parT_unit (write_reg ii (PPC_IR rd) (f x y)) (ppc_uint_cmp ii (f x y) 0w))`;
51
52val sint_reg_update_def = Define `
53  sint_reg_update ii rd f s1 s2 =
54    seqT (parT s1 s2)
55         (\(x,y). parT_unit (write_reg ii (PPC_IR rd) (f x y)) (ppc_sint_cmp ii (f x y) 0w))`;
56
57val uint_compare_def = Define `
58  uint_compare ii s1 s2 =
59    seqT (parT s1 s2) (\(x,y). ppc_uint_cmp ii x y)`;
60
61val sint_compare_def = Define `
62  sint_compare ii s1 s2 =
63    seqT (parT s1 s2) (\(x,y). ppc_sint_cmp ii x y)`;
64
65val bit_update_def = Define `
66  bit_update ii bd (f:bool->bool->bool) s1 s2 =
67    seqT (parT s1 s2) (\(x,y). write_status ii bd (SOME (f x y)))`;
68
69val const_low_s_def  = Define `const_low_s w = constT ((sw2sw:word16->word32) w)`;
70val const_high_s_def = Define `const_high_s w = constT (((sw2sw:word16->word32) w) << 16)`;
71
72val const_low_def        = Define `const_low w = constT ((w2w:word16->word32) w)`;
73val const_high_def       = Define `const_high w = constT ((w2w:word16->word32) w << 16)`;
74
75val conditional_def = Define `conditional x y z = if x then y else z`;
76
77val read_bit_word_def = Define `
78  read_bit_word ii bit =
79    seqT (read_status ii bit) (\x. constT (conditional x 1w 0w))`;
80
81val read_ireg_def = Define `
82  read_ireg ii rd = read_reg ii (PPC_IR rd)`;
83
84val gpr_or_zero_def = Define `gpr_or_zero ii d = if d = 0w then const_low 0w else read_ireg ii d`;
85
86val no_carry_def = Define `
87  no_carry ii = write_status ii PPC_CARRY NONE`;
88
89val goto_label_def = Define `
90  goto_label ii l =
91    seqT (read_reg ii PPC_PC) (\x. write_reg ii PPC_PC (x + sw2sw l * 4w))`;
92
93val PREAD_M_LIST_def = Define `
94  PREAD_M_LIST n a s =
95    if n = 0 then [] else PREAD_M a s :: PREAD_M_LIST (n-1) (a+1w) s`;
96
97val PWRITE_M_LIST_def = Define `
98  (PWRITE_M_LIST a [] s = s) /\
99  (PWRITE_M_LIST a (b::bs) s = PWRITE_M a (SOME b) (PWRITE_M_LIST (a+1w) bs s))`;
100
101val effective_address_def = Define `
102  effective_address s1 s2 = seqT (parT s1 s2) (\(x:word32,y:word32). constT (x + y))`;
103
104val assertT_def = Define `
105  assertT b f = seqT (if b then constT () else failureT) (\x. f)`;
106
107val ppc_write_mem_aux_def = Define `
108  (ppc_write_mem_aux ii addr [] = constT ()) /\
109  (ppc_write_mem_aux ii addr (b::bytes) =
110     parT_unit (write_mem ii addr b)
111               (ppc_write_mem_aux ii (addr+1w) bytes))`;
112
113val reg_store_def = Define `
114  reg_store ii size rd s1 s2 =
115    seqT (parT (effective_address s1 s2) (read_ireg ii rd))
116         (\(addr,x). assertT (address_aligned size addr)
117                             (ppc_write_mem_aux ii addr (REVERSE (word2bytes size x))))`;
118
119val read_mem_aux_def = Define `
120  read_mem_aux ii size addr =
121    if size = 1 then
122      seqT (read_mem ii addr)
123           (\x. constT ((bytes2word [x]):word32))
124    else if size = 2 then
125      seqT (parT (read_mem ii addr) (read_mem ii (addr+1w)))
126           (\(x0,x1). constT (bytes2word [x1;x0]))
127    else
128      seqT (parT (parT (read_mem ii (addr+0w)) (read_mem ii (addr+1w)))
129                 (parT (read_mem ii (addr+2w)) (read_mem ii (addr+3w))))
130           (\((x0,x1),(x2,x3)). constT (bytes2word [x3;x2;x1;x0]))`;
131
132val load_word_def = Define `
133  load_word ii size addr =
134    assertT (address_aligned size addr) (read_mem_aux ii size addr)`;
135
136val reg_load_def = Define `
137  reg_load ii size rd s1 s2 =
138    seqT (effective_address s1 s2)
139         (\addr. seqT (load_word ii size addr)
140                      (write_reg ii (PPC_IR rd)))`;
141
142val ppc_branch_condition_def = Define `
143  ppc_branch_condition (b0:word5) b =
144    if b0 && 16w = 16w then T else
145    if b0 && 8w = 8w then (b = T) else
146    (* b0 && 4w = 4w then *) (b = F)`;
147
148val ppc_exec_instr_def = Define `
149  (ppc_exec_instr ii (Padd rd r1 r2) =
150       OK_nextinstr ii (reg_update ii rd $+ (read_ireg ii r1) (read_ireg ii r2))) /\
151
152  (ppc_exec_instr ii (Padde rd r1 r2) =
153       OK_nextinstr ii
154         (seqT (parT (read_ireg ii r1) (parT (read_ireg ii r2) (read_status ii PPC_CARRY)))
155            (\(w1,w2,c1). parT_unit (write_reg ii (PPC_IR rd) (FST (add_with_carry (w1,w2,c1))))
156                                    (write_status ii PPC_CARRY (SOME (FST (SND (add_with_carry (w1,w2,c1))))))))) /\
157
158  (ppc_exec_instr ii (Paddi rd r1 cst) =
159       OK_nextinstr ii (reg_update ii rd $+ (gpr_or_zero ii r1) (const_low_s cst))) /\
160
161  (ppc_exec_instr ii (Paddis rd r1 cst ) =
162       OK_nextinstr ii (reg_update ii rd $+ (gpr_or_zero ii r1) (const_high_s cst))) /\
163
164  (ppc_exec_instr ii (Paddze rd r1) =
165       OK_nextinstr ii (reg_update ii rd $+ (read_ireg ii r1) (read_bit_word ii PPC_CARRY))) /\
166
167  (ppc_exec_instr ii (Pand_ rd r1 r2) =
168       OK_nextinstr ii (sint_reg_update ii rd $&& (read_ireg ii r1) (read_ireg ii r2))) /\
169
170  (ppc_exec_instr ii (Pandc rd r1 r2) =
171       OK_nextinstr ii (reg_update ii rd (\x y. x && ~y) (read_ireg ii r1) (read_ireg ii r2))) /\
172
173  (ppc_exec_instr ii (Pandi_ rd r1 cst) =
174       OK_nextinstr ii (sint_reg_update ii rd $&& (read_ireg ii r1) (const_low cst))) /\
175
176  (ppc_exec_instr ii (Pandis_ rd r1 cst) =
177       OK_nextinstr ii (sint_reg_update ii rd $&& (read_ireg ii r1) (const_high cst))) /\
178
179  (ppc_exec_instr ii (Pb lbl) =
180       goto_label ii lbl) /\
181
182  (ppc_exec_instr ii (Pbc b0 bi lb1) =
183       seqT (read_status ii (PPC_CR0 bi))
184            (\b. if ppc_branch_condition b0 b then goto_label ii lb1 else OK_nextinstr ii (constT ()))) /\
185
186  (ppc_exec_instr ii (Pbctr) =
187       seqT (read_reg ii PPC_CTR) (write_reg ii PPC_PC)) /\
188
189  (ppc_exec_instr ii (Pbctrl) =
190       seqT (parT (read_reg ii PPC_PC) (read_reg ii PPC_CTR))
191            (\(pc,ctr). parT_unit (write_reg ii PPC_PC ctr) (write_reg ii PPC_LR (pc + 4w)))) /\
192
193  (ppc_exec_instr ii (Pbl ident) =
194       seqT (read_reg ii PPC_PC)
195            (\x. parT_unit (write_reg ii PPC_PC (x + sw2sw ident * 4w)) (write_reg ii PPC_LR (x + 4w)))) /\
196
197  (ppc_exec_instr ii (Pblr) =
198       seqT (read_reg ii PPC_LR) (write_reg ii PPC_PC)) /\
199
200  (ppc_exec_instr ii (Pcmplw r1 r2) =
201      OK_nextinstr ii (uint_compare ii (read_ireg ii r1) (read_ireg ii r2))) /\
202
203  (ppc_exec_instr ii (Pcmplwi r1 cst) =
204      OK_nextinstr ii (uint_compare ii (read_ireg ii r1) (const_low cst))) /\
205
206  (ppc_exec_instr ii (Pcmpw r1 r2) =
207      OK_nextinstr ii (sint_compare ii (read_ireg ii r1) (read_ireg ii r2))) /\
208
209  (ppc_exec_instr ii (Pcmpwi r1 cst) =
210      OK_nextinstr ii (sint_compare ii (read_ireg ii r1) (const_low_s cst))) /\
211
212  (ppc_exec_instr ii (Pcror bd b1 b2) =
213      OK_nextinstr ii (bit_update ii (PPC_CR0 bd) $\/
214         (read_status ii (PPC_CR0 b1)) (read_status ii (PPC_CR0 b2)))) /\
215
216  (ppc_exec_instr ii (Pdivw rd r1 r2) = failureT) /\
217
218  (ppc_exec_instr ii (Pdivwu rd r1 r2) =
219      OK_nextinstr ii (reg_update ii rd (\x y. n2w (w2n x DIV w2n y))
220        (read_ireg ii r1) (read_ireg ii r2))) /\
221
222  (ppc_exec_instr ii (Peqv rd r1 r2) =
223      OK_nextinstr ii (reg_update ii rd (\x y. ~(x ?? y)) (read_ireg ii r1) (read_ireg ii r2))) /\
224
225  (ppc_exec_instr ii (Pextsb rd r1) =
226      OK_nextinstr ii (reg_update ii rd (\x y. sw2sw ((w2w x):word8))
227          (read_ireg ii r1) (constT ()))) /\
228
229  (ppc_exec_instr ii (Pextsh rd r1) =
230      OK_nextinstr ii (reg_update ii rd (\x y. sw2sw ((w2w x):word16))
231        (read_ireg ii r1) (constT ()))) /\
232
233  (ppc_exec_instr ii (Pfabs rd r1) = failureT) /\
234
235  (ppc_exec_instr ii (Pfadd rd r1 r2) = failureT) /\
236
237  (ppc_exec_instr ii (Pfcmpu r1 r2) = failureT) /\
238
239  (ppc_exec_instr ii (Pfcti rd r1) = failureT) /\
240
241  (ppc_exec_instr ii (Pfdiv rd r1 r2) = failureT) /\
242
243  (ppc_exec_instr ii (Pfmadd rd r1 r2 r3) = failureT) /\
244
245  (ppc_exec_instr ii (Pfmr rd r1) = failureT) /\
246
247  (ppc_exec_instr ii (Pfmsub rd r1 r2 r3) = failureT) /\
248
249  (ppc_exec_instr ii (Pfmul rd r1 r2) = failureT) /\
250
251  (ppc_exec_instr ii (Pfneg rd r1) = failureT) /\
252
253  (ppc_exec_instr ii (Pfrsp rd r1) = failureT) /\
254
255  (ppc_exec_instr ii (Pfsub rd r1 r2) = failureT) /\
256
257  (ppc_exec_instr ii (Pictf rd r1) = failureT) /\
258
259  (ppc_exec_instr ii (Piuctf rd r1) = failureT) /\
260
261  (ppc_exec_instr ii (Plbz rd cst r1) =
262      OK_nextinstr ii (reg_load ii 1 rd (gpr_or_zero ii r1) (const_low_s cst))) /\
263
264  (ppc_exec_instr ii (Plbzx rd r1 r2) =
265      OK_nextinstr ii (reg_load ii 1 rd (gpr_or_zero ii r1) (read_ireg ii r2))) /\
266
267  (ppc_exec_instr ii (Plfd rd cst r1) = failureT) /\
268
269  (ppc_exec_instr ii (Plfdx rd r1 r2) = failureT) /\
270
271  (ppc_exec_instr ii (Plfs rd cst r1) = failureT) /\
272
273  (ppc_exec_instr ii (Plfsx rd r1 r2) = failureT) /\
274
275  (ppc_exec_instr ii (Plha rd cst r1) =
276      OK_nextinstr ii (reg_load ii 2 rd (gpr_or_zero ii r1) (const_low_s cst))) /\
277
278  (ppc_exec_instr ii (Plhax rd r1 r2) =
279      OK_nextinstr ii (reg_load ii 2 rd (gpr_or_zero ii r1) (read_ireg ii r2))) /\
280
281  (ppc_exec_instr ii (Plhz rd cst r1) =
282      OK_nextinstr ii (reg_load ii 2 rd (gpr_or_zero ii r1) (const_low_s cst))) /\
283
284  (ppc_exec_instr ii (Plhzx rd r1 r2) =
285      OK_nextinstr ii (reg_load ii 2 rd (gpr_or_zero ii r1) (read_ireg ii r2))) /\
286
287  (ppc_exec_instr ii (Plwz rd cst r1) =
288      OK_nextinstr ii (reg_load ii 4 rd (gpr_or_zero ii r1) (const_low_s cst))) /\
289
290  (ppc_exec_instr ii (Plwzx rd r1 r2) =
291      OK_nextinstr ii (reg_load ii 4 rd (gpr_or_zero ii r1) (read_ireg ii r2))) /\
292
293  (ppc_exec_instr ii (Pmfcrbit v162 v163) = failureT) /\
294
295  (ppc_exec_instr ii (Pmflr rd) =
296      OK_nextinstr ii (seqT (read_reg ii PPC_LR) (write_reg ii (PPC_IR rd)))) /\
297
298  (ppc_exec_instr ii (Pmr rd r1) =
299      OK_nextinstr ii (seqT (read_ireg ii r1) (write_reg ii (PPC_IR rd)))) /\
300
301  (ppc_exec_instr ii (Pmtctr r1) =
302      OK_nextinstr ii (seqT (read_ireg ii r1) (write_reg ii PPC_CTR))) /\
303
304  (ppc_exec_instr ii (Pmtlr r1) =
305      OK_nextinstr ii (seqT (read_ireg ii r1) (write_reg ii PPC_LR))) /\
306
307  (ppc_exec_instr ii (Pmulli rd r1 cst) =
308      OK_nextinstr ii (reg_update ii rd $* (read_ireg ii r1) (const_low_s cst))) /\
309
310  (ppc_exec_instr ii (Pmullw rd r1 r2) =
311      OK_nextinstr ii (reg_update ii rd $* (read_ireg ii r1) (read_ireg ii r2))) /\
312
313  (ppc_exec_instr ii (Pnand rd r1 r2) =
314      OK_nextinstr ii (reg_update ii rd (\x y. ~(x && y)) (read_ireg ii r1) (read_ireg ii r2))) /\
315
316  (ppc_exec_instr ii (Pnor rd r1 r2) =
317      OK_nextinstr ii (reg_update ii rd (\x y. ~(x || y)) (read_ireg ii r1) (read_ireg ii r2))) /\
318
319  (ppc_exec_instr ii (Por rd r1 r2) =
320      OK_nextinstr ii (reg_update ii rd $|| (read_ireg ii r1) (read_ireg ii r2))) /\
321
322  (ppc_exec_instr ii (Porc rd r1 r2) =
323      OK_nextinstr ii (reg_update ii rd (\x y. x || ~y) (read_ireg ii r1) (read_ireg ii r2))) /\
324
325  (ppc_exec_instr ii (Pori rd r1 cst) =
326      OK_nextinstr ii (reg_update ii rd $|| (read_ireg ii r1) (const_low cst))) /\
327
328  (ppc_exec_instr ii (Poris rd r1 cst) =
329      OK_nextinstr ii (reg_update ii rd $|| (read_ireg ii r1) (const_high cst))) /\
330
331  (ppc_exec_instr ii (Prlwinm rd r1 sh mb me) = failureT) /\
332
333  (ppc_exec_instr ii (Pslw rd r1 r2) =
334      OK_nextinstr ii (reg_update ii rd (\x y. x << w2n ((w2w y):word6)) (read_ireg ii r1) (read_ireg ii r2))) /\
335
336  (ppc_exec_instr ii (Psraw rd r1 r2) =
337      OK_nextinstr ii (parT_unit (reg_update ii rd (\x y. x >>> w2n ((w2w y):word6)) (read_ireg ii r1) (read_ireg ii r2))
338                                 (no_carry ii))) /\
339
340  (ppc_exec_instr ii (Psrawi rd r1 sh) =
341      OK_nextinstr ii (parT_unit (reg_update ii rd (\x:word32 y:word32. x >>> w2n ((w2w y):word6)) (read_ireg ii r1) (constT (w2w sh)))
342                                 (no_carry ii))) /\
343
344  (ppc_exec_instr ii (Psrw rd r1 r2) =
345      OK_nextinstr ii (reg_update ii rd (\x y. x >> w2n ((w2w y):word6)) (read_ireg ii r1) (read_ireg ii r2))) /\
346
347  (ppc_exec_instr ii (Pstb rd cst r1) =
348      OK_nextinstr ii (reg_store ii 1 rd (gpr_or_zero ii r1) (const_low_s cst))) /\
349
350  (ppc_exec_instr ii (Pstbx rd r1 r2) =
351      OK_nextinstr ii (reg_store ii 1 rd (gpr_or_zero ii r1) (read_ireg ii r2))) /\
352
353  (ppc_exec_instr ii (Pstfd rd cst r1) = failureT) /\
354
355  (ppc_exec_instr ii (Pstfdx rd r1 r2) = failureT) /\
356
357  (ppc_exec_instr ii (Pstfs rd cst r1) = failureT) /\
358
359  (ppc_exec_instr ii (Pstfsx rd r1 r2) = failureT) /\
360
361  (ppc_exec_instr ii (Psth rd cst r1) =
362      OK_nextinstr ii (reg_store ii 2 rd (gpr_or_zero ii r1) (const_low_s cst))) /\
363
364  (ppc_exec_instr ii (Psthx rd r1 r2) =
365      OK_nextinstr ii (reg_store ii 2 rd (gpr_or_zero ii r1) (read_ireg ii r2))) /\
366
367  (ppc_exec_instr ii (Pstw rd cst r1) =
368      OK_nextinstr ii (reg_store ii 4 rd (gpr_or_zero ii r1) (const_low_s cst))) /\
369
370  (ppc_exec_instr ii (Pstwx rd r1 r2) =
371      OK_nextinstr ii (reg_store ii 4 rd (gpr_or_zero ii r1) (read_ireg ii r2))) /\
372
373  (ppc_exec_instr ii (Psubfc rd r1 r2) =
374      OK_nextinstr ii (parT_unit (reg_update ii rd $- (read_ireg ii r2) (read_ireg ii r1))
375                                 (no_carry ii))) /\
376
377  (ppc_exec_instr ii (Psubfic rd r1 cst) =
378      OK_nextinstr ii (parT_unit (reg_update ii rd $- (const_low_s cst) (read_ireg ii r1))
379                                 (no_carry ii))) /\
380
381  (ppc_exec_instr ii (Psubfe rd r1 r2) =
382       OK_nextinstr ii
383         (seqT (parT (read_ireg ii r1) (parT (read_ireg ii r2) (read_status ii PPC_CARRY)))
384            (\(w1,w2,c1). parT_unit (write_reg ii (PPC_IR rd) (FST (add_with_carry (w2,~w1,c1))))
385                                    (write_status ii PPC_CARRY (SOME (FST (SND (add_with_carry (w2,~w1,c1))))))))) /\
386
387  (ppc_exec_instr ii (Pxor rd r1 r2) =
388      OK_nextinstr ii (reg_update ii rd $?? (read_ireg ii r1) (read_ireg ii r2))) /\
389
390  (ppc_exec_instr ii (Pxori rd r1 cst) =
391      OK_nextinstr ii (reg_update ii rd $?? (read_ireg ii r1) (const_low cst))) /\
392
393  (ppc_exec_instr ii (Pxoris rd r1 cst ) =
394      OK_nextinstr ii (reg_update ii rd $?? (read_ireg ii r1) (const_high cst)))`;
395
396
397val ppc_assertT_lemma = store_thm("ppc_assertT_lemma",
398  ``!b f. b ==> (assertT b (f:'a ppc_M) = f)``,
399  SIMP_TAC std_ss [assertT_def,seqT_def,constT_def,seq_monad_thm,FUN_EQ_THM]);
400
401val _ = export_theory ();
402