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