1(* ------------------------------------------------------------------------ 2 ARMv6-M step evaluator 3 ------------------------------------------------------------------------ *) 4 5structure m0_stepLib :> m0_stepLib = 6struct 7 8open HolKernel boolLib bossLib 9 10open m0Theory m0_stepTheory 11open state_transformerSyntax blastLib 12 13structure Parse = 14struct 15 open Parse 16 val (Type, Term) = parse_from_grammars m0_stepTheory.m0_step_grammars 17end 18open Parse 19 20val ERR = Feedback.mk_HOL_ERR "m0_stepLib" 21val WARN = Feedback.HOL_WARNING "m0_stepLib" 22 23val () = show_assums := true 24 25(* ========================================================================= *) 26 27val mk_byte = bitstringSyntax.mk_vec 8 28val rhsc = utilsLib.rhsc 29fun mapl x = utilsLib.augment x [[]] 30 31fun MATCH_HYP_RW l = utilsLib.MATCH_HYP_CONV_RULE (REWRITE_CONV l) 32val REG_CONV = REWRITE_CONV [v2w_13_15_rwts, v2w_ground4] 33 34val opcodes = utilsLib.list_mk_wordii 4 (List.tabulate (16, Lib.I)) 35val arithlogic = utilsLib.list_mk_wordii 4 [0,1,2,3,4,5,6,7,12,14] 36val testcompare = utilsLib.list_mk_wordii 2 [0,2,3] 37 38val st = Term.mk_var ("s", Type.mk_type ("m0_state", [])) 39 40fun mk_arm_const n = Term.prim_mk_const {Thy = "m0", Name = n} 41fun mk_arm_type n = Type.mk_thy_type {Thy = "m0", Tyop = n, Args = []} 42 43(* ---------------------------- *) 44 45local 46 val a_of = utilsLib.accessor_fns o mk_arm_type 47 val u_of = utilsLib.update_fns o mk_arm_type 48 val state_fns = a_of "m0_state" 49 val other_fns = 50 [pairSyntax.fst_tm, pairSyntax.snd_tm, bitstringSyntax.v2w_tm, 51 ``IncPC ()``, ``(h >< l) : 'a word -> 'b word``] @ u_of "m0_state" 52 val exc = ``SND (raise'exception e s : 'a # m0_state)`` 53in 54 val cond_rand_thms = utilsLib.mk_cond_rand_thms (other_fns @ state_fns) 55 val snd_exception_thms = 56 utilsLib.map_conv 57 (Drule.GEN_ALL o 58 utilsLib.SRW_CONV [cond_rand_thms, m0Theory.raise'exception_def] o 59 (fn tm => Term.mk_comb (tm, exc))) state_fns 60end 61 62(* ---------------------------- *) 63 64(* ARM datatype theorems/conversions *) 65 66fun datatype_thms thms = 67 thms @ [cond_rand_thms, snd_exception_thms, FST_SWAP, 68 m0_stepTheory.Align, m0_stepTheory.Aligned] @ 69 utilsLib.datatype_rewrites true "m0" ["m0_state", "RName", "SRType", "PSR"] 70 71val DATATYPE_CONV = REWRITE_CONV (datatype_thms []) 72val DATATYPE_RULE = Conv.CONV_RULE DATATYPE_CONV 73val FULL_DATATYPE_RULE = utilsLib.FULL_CONV_RULE DATATYPE_CONV 74 75val COND_UPDATE_CONV = 76 REWRITE_CONV 77 (utilsLib.qm [] ``!b. (if b then T else F) = b`` :: 78 utilsLib.mk_cond_update_thms (List.map mk_arm_type ["m0_state", "PSR"])) 79 80val COND_UPDATE_RULE = Conv.CONV_RULE COND_UPDATE_CONV 81 82val STATE_CONV = 83 REWRITE_CONV (utilsLib.datatype_rewrites true "m0" ["m0_state"] @ 84 [boolTheory.COND_ID, cond_rand_thms]) 85 86local 87 val cmp = computeLib.bool_compset () 88 val () = computeLib.add_thms (datatype_thms [pairTheory.FST]) cmp 89in 90 val EVAL_DATATYPE_CONV = Conv.TRY_CONV (utilsLib.CHANGE_CBV_CONV cmp) 91end 92 93fun fix_datatype tm = rhsc (Conv.QCONV DATATYPE_CONV tm) 94val fix_datatypes = List.map fix_datatype 95 96local 97 val big_tm = fix_datatype ``^st.AIRCR.ENDIANNESS`` 98 val little_tm = boolSyntax.mk_neg big_tm 99 val spsel_tm = fix_datatype ``^st.CONTROL.SPSEL`` 100 val nspsel_tm = boolSyntax.mk_neg spsel_tm 101in 102 fun endian be = [if be then big_tm else little_tm] 103 fun spsel sel = [if sel then spsel_tm else nspsel_tm] 104end 105 106fun specialized0 m tms = 107 utilsLib.specialized m (Conv.ALL_CONV, fix_datatypes tms) 108fun specialized1 m tms = 109 utilsLib.specialized m (utilsLib.WGROUND_CONV, fix_datatypes tms) 110 111fun state_with_pcinc e = (st |-> fix_datatype ``^st with pcinc := ^e``) 112 113local 114 fun ADD_PRECOND_RULE e thm = 115 FULL_DATATYPE_RULE (Thm.INST [state_with_pcinc e] thm) 116 val rwts = ref ([]: thm list) 117in 118 fun getThms e tms = 119 List.map (ADD_PRECOND_RULE e) (specialized1 "eval" tms (!rwts)) 120 |> List.filter (not o utilsLib.vacuous) 121 fun resetThms () = rwts := [] 122 fun addThms thms = (rwts := thms @ !rwts; thms) 123end 124 125val EV = utilsLib.STEP (datatype_thms, st) 126val resetEvConv = utilsLib.resetStepConv 127val setEvConv = utilsLib.setStepConv 128 129(* ========================================================================= *) 130 131(* register access *) 132 133val () = setEvConv utilsLib.WGROUND_CONV 134 135val PC_rwt = 136 EV [PC_def, R_def] [] [] 137 ``PC`` |> hd 138 139val () = resetEvConv () 140 141val write'PC_rwt = 142 EV [write'PC_def] [] [] 143 ``write'PC x`` |> hd 144 145local 146 val mask_sp = 147 blastLib.BBLAST_PROVE 148 ``d && 0xFFFFFFFCw : word32 = ((31 >< 2) d : word30) @@ (0w: word2)`` 149 150 fun r_rwt t = Q.prove(t, 151 wordsLib.Cases_on_word_value `n` 152 \\ simp [write'R_def, R_def, R_name_def, LookUpSP_def, num2RName_thm, 153 mask_sp] 154 ) 155 |> Drule.UNDISCH 156in 157 val R_name_rwt = r_rwt 158 `n <> 15w ==> (R n ^st = ^st.REG (R_name ^st.CONTROL.SPSEL n))` 159 160 val write'R_name_rwt = r_rwt 161 `n <> 15w ==> 162 (write'R (d, n) ^st = 163 ^st with REG := 164 (R_name ^st.CONTROL.SPSEL n =+ 165 if n = 13w then d && 0xFFFFFFFCw else d) ^st.REG)` 166 167 val RName_LR_rwt = EVAL ``m0_step$R_name x 14w`` 168end 169 170(* ---------------------------- *) 171 172(* write PC *) 173 174val BranchTo_rwt = 175 EV [BranchTo_def, write'PC_rwt] [] [] 176 ``BranchTo imm32`` |> hd 177 178val IncPC_rwt = 179 EV [IncPC_def, BranchTo_rwt] [] [] 180 ``IncPC ()`` |> hd 181 182val BranchWritePC_rwt = 183 EV [BranchWritePC_def, BranchTo_rwt] [] [] 184 ``BranchWritePC imm32`` |> hd 185 186val BXWritePC_rwt = 187 EV [BXWritePC_def, BranchTo_rwt] 188 [[``^st.CurrentMode <> Mode_Handler``, ``word_bit 0 (imm32:word32)``]] [] 189 ``BXWritePC imm32`` |> hd 190 191val BLXWritePC_rwt = 192 EV [BLXWritePC_def, BranchTo_rwt] [[``word_bit 0 (imm32:word32)``]] [] 193 ``BLXWritePC imm32`` |> hd 194 195val LoadWritePC_rwt = 196 EV [LoadWritePC_def, BXWritePC_rwt] [] [] 197 ``LoadWritePC imm32`` |> hd 198 199val ALUWritePC_rwt = 200 EV [ALUWritePC_def, BranchWritePC_rwt] [] [] 201 ``ALUWritePC d`` |> hd 202 203(* ---------------------------- *) 204 205(* read mem *) 206 207fun fixwidth_for ty = 208 bitstringTheory.fixwidth_id 209 |> Q.ISPEC `w2v (w:^(ty_antiq (wordsSyntax.mk_word_type ty)))` 210 |> REWRITE_RULE [bitstringTheory.length_w2v] 211 |> Conv.CONV_RULE (Conv.DEPTH_CONV wordsLib.SIZES_CONV) 212 |> Drule.GEN_ALL 213 214val mem_rwt = 215 EV ([mem_def, mem1_def, concat16, concat32, bitstringTheory.field_fixwidth] @ 216 List.map fixwidth_for [``:8``, ``:16``, ``:32``]) [] 217 (mapl (`n`, [``1n``,``2n``,``4n``])) 218 ``mem (a, n)`` 219 220val BigEndianReverse_rwt = 221 EV [BigEndianReverse_def] [] (mapl (`n`, [``1n``,``2n``,``4n``])) 222 ``BigEndianReverse (v, n)`` 223 224local 225 val rwts = 226 [MemA_def, cond_rand_thms, snd_exception_thms, alignmentTheory.aligned_0, 227 wordsTheory.WORD_ADD_0, bitstringTheory.v2w_w2v] @ 228 mem_rwt @ BigEndianReverse_rwt 229in 230 val MemA_1_rwt = 231 EV (rwts @ [bitstringTheory.field_fixwidth, fixwidth_for ``:8``]) [] [] 232 ``MemA (v, 1) : m0_state -> word8 # m0_state`` 233 |> hd 234 235 val MemA_2_rwt = 236 EV (extract16 :: rwts) [[``aligned 1 (v:word32)``]] [] 237 ``MemA (v, 2) : m0_state -> word16 # m0_state`` 238 |> hd 239 240 val MemA_4_rwt = 241 EV (extract32 :: rwts) [[``aligned 2 (v:word32)``]] [] 242 ``MemA (v, 4) : m0_state -> word32 # m0_state`` 243 |> hd 244 245 val MemU_1_rwt = 246 EV [MemU_def, MemA_1_rwt] [] [] 247 ``MemU (v, 1) : m0_state -> word8 # m0_state`` 248 |> hd 249 250 val MemU_2_rwt = 251 EV [MemU_def, MemA_2_rwt] [] [] 252 ``MemU (v, 2) : m0_state -> word16 # m0_state`` 253 |> hd 254 255 val MemU_4_rwt = 256 EV [MemU_def, MemA_4_rwt] [] [] 257 ``MemU (v, 4) : m0_state -> word32 # m0_state`` 258 |> hd 259end 260 261(* ---------------------------- *) 262 263(* write mem *) 264 265val write'mem_rwt = 266 EV ([write'mem_def]) [] (mapl (`n`, [``1n``,``2n``,``4n``])) 267 ``write'mem (v, a, n)`` 268 269local 270 val field_cond_rand = Drule.ISPEC ``field h l`` boolTheory.COND_RAND 271 val rwts = 272 [write'MemA_def, cond_rand_thms, snd_exception_thms, 273 wordsTheory.WORD_ADD_0, bitstringTheory.v2w_w2v, 274 alignmentTheory.aligned_0, field_cond_rand] @ 275 write'mem_rwt @ BigEndianReverse_rwt 276in 277 val write'MemA_1_rwt = 278 EV (rwts @ [fixwidth_for ``:8``, bitstringTheory.field_fixwidth]) [] [] 279 ``write'MemA (w: word8, v, 1)`` 280 |> hd 281 282 val write'MemA_2_rwt = 283 EV (field16 :: rwts) [[``aligned 1 (v:word32)``]] [] 284 ``write'MemA (w:word16, v, 2)`` 285 |> hd 286 287 val write'MemA_4_rwt = 288 EV (field32 :: rwts) [[``aligned 2 (v:word32)``]] [] 289 ``write'MemA (w:word32, v, 4)`` 290 |> hd 291 292 val write'MemU_1_rwt = 293 EV [write'MemU_def, write'MemA_1_rwt] [] [] 294 ``write'MemU (w: word8, v, 1)`` 295 |> hd 296 297 val write'MemU_2_rwt = 298 EV [write'MemU_def, write'MemA_2_rwt] [] [] 299 ``write'MemU (w: word16, v, 2)`` 300 |> hd 301 302 val write'MemU_4_rwt = 303 EV [write'MemU_def, write'MemA_4_rwt] [] [] 304 ``write'MemU (w: word32, v, 4)`` 305 |> hd 306end 307 308; 309 310(* ---------------------------- *) 311 312fun Shift_C_typ a b = 313 Shift_C_DecodeRegShift_rwt 314 |> Q.SPECL [a, b] 315 |> Drule.SPEC_ALL 316 |> REWRITE_RULE [] 317 |> Conv.CONV_RULE 318 (Conv.LHS_CONV (Conv.DEPTH_CONV bitstringLib.v2w_n2w_CONV) 319 THENC REWRITE_CONV [DecodeRegShift_rwt]) 320 321val Shift_C_LSL_rwt = 322 EV [Shift_C_def, LSL_C_def] [] [] 323 ``Shift_C (value,SRType_LSL,0,carry_in) 324 : m0_state -> ('a word # bool) # m0_state`` 325 |> hd 326 327val Shift_C_rwt = 328 EV [Shift_C_def, LSL_C_def, LSR_C_def, ASR_C_def, ROR_C_def, RRX_C_def] [] [] 329 ``Shift_C (value,typ,amount,carry_in) 330 : m0_state -> ('a word # bool) # m0_state`` 331 |> hd 332 |> SIMP_RULE std_ss [] 333 334val SND_Shift_C_rwt = Q.prove( 335 `!s. SND (Shift_C (value,typ,amount,carry_in) s) = s`, 336 Cases_on `typ` \\ lrw [Shift_C_rwt]) |> Drule.GEN_ALL 337 338(* ---------------------------- *) 339 340fun unfold_for_loop n thm = 341 thm 342 |> REWRITE_RULE [utilsLib.for_thm (n,0), BitCount] 343 |> Drule.SPEC_ALL 344 |> Conv.CONV_RULE (Conv.X_FUN_EQ_CONV st) 345 |> Drule.SPEC_ALL 346 |> Conv.RIGHT_CONV_RULE 347 (PairedLambda.GEN_BETA_CONV 348 THENC PairedLambda.let_CONV 349 THENC PairedLambda.let_CONV 350 THENC REWRITE_CONV [] 351 THENC Conv.ONCE_DEPTH_CONV PairedLambda.GEN_BETA_CONV 352 ) 353 354val abs_body = snd o Term.dest_abs 355 356local 357 fun let_body t = let val (_, _, b) = pairSyntax.dest_plet t in b end 358 fun let_val t = let val (_, b, _) = pairSyntax.dest_plet t in b end 359 fun cond_true t = let val (_, b, _) = boolSyntax.dest_cond t in b end 360 val split_memA = 361 GSYM (Q.ISPEC `MemA x s : 'a word # m0_state` pairTheory.PAIR) 362 val dest_for = (fn (_, _, b) => b) o state_transformerSyntax.dest_for o 363 Term.rator 364in 365 fun simp_for_body thm = 366 thm 367 |> Drule.SPEC_ALL 368 |> rhsc |> abs_body 369 |> let_body 370 |> let_body 371 |> let_val 372 |> Term.rand 373 |> dest_for 374 |> abs_body |> abs_body 375 |> (SIMP_CONV bool_ss [Once split_memA, pairTheory.pair_case_thm] 376 THENC Conv.DEPTH_CONV PairedLambda.GEN_LET_CONV 377 THENC SIMP_CONV std_ss [cond_rand_thms]) 378end 379 380fun upto_enumerate n thm = 381 Drule.LIST_CONJ (List.tabulate (n, fn i => 382 let 383 val t = numSyntax.term_of_int i 384 in 385 Thm.CONJ (thm |> Thm.SPEC t |> numLib.REDUCE_RULE) 386 (numLib.REDUCE_CONV ``^t + 1``) 387 end)) 388 389(* -- *) 390 391val count_list_8 = EVAL ``COUNT_LIST 8`` 392val count_list_9 = EVAL ``COUNT_LIST 9`` 393 394val () = resetThms () 395 396local 397 val LDM_UPTO_SUC = upto_enumerate 7 m0_stepTheory.LDM_UPTO_SUC 398 val LDM_lem = simp_for_body dfn'LoadMultiple_def 399 val LDM_thm = unfold_for_loop 7 dfn'LoadMultiple_def 400 401 fun FOR_BETA_CONV i tm = 402 let 403 val b = pairSyntax.dest_snd tm 404 val (b, _, _) = boolSyntax.dest_cond (abs_body (rator b)) 405 val n = fst (wordsSyntax.dest_word_bit b) 406 val _ = numLib.int_of_term n = i orelse raise ERR "FOR_BETA_CONV" "" 407 val thm = 408 write'R_name_rwt 409 |> Q.INST [`n` |-> `n2w ^n`] 410 |> utilsLib.FULL_CONV_RULE wordsLib.WORD_EVAL_CONV 411 in 412 (Conv.RAND_CONV 413 (PairedLambda.GEN_BETA_CONV 414 THENC Conv.REWR_CONV LDM_lem 415 THENC utilsLib.INST_REWRITE_CONV [MemA_4_rwt, thm]) 416 THENC REWRITE_CONV [cond_rand_thms, LDM_UPTO_components, 417 LDM_UPTO_0, LDM_UPTO_SUC]) tm 418 end 419 420 val LDM = 421 LDM_thm 422 |> Conv.RIGHT_CONV_RULE 423 (REWRITE_CONV [R_name_rwt, ASSUME ``n <> 15w: word4``] 424 THENC Conv.EVERY_CONV 425 (List.tabulate 426 (8, fn i => Conv.ONCE_DEPTH_CONV (FOR_BETA_CONV i)))) 427 |> utilsLib.ALL_HYP_CONV_RULE 428 (utilsLib.WGROUND_CONV 429 THENC REWRITE_CONV 430 [alignmentTheory.aligned_add_sub_123, Aligned_concat4, 431 LDM_UPTO_components] 432 THENC numLib.REDUCE_CONV) 433 434 val lem = Q.prove( 435 `!registers:word9. ~word_bit (w2n (13w: word4)) registers`, 436 simp [wordsTheory.word_bit_def] 437 ) 438in 439 val POP_rwt = 440 EV [LDM, LDM_UPTO_def, IncPC_rwt, LDM_UPTO_PC, write'R_name_rwt, 441 Aligned_SP, LoadWritePC_rwt, MemA_4_rwt, lem] 442 [[``~word_bit 8 (registers: word9)``], 443 [``word_bit 8 (registers: word9)``]] [] 444 ``dfn'LoadMultiple (T, 13w, registers)`` 445 |> List.map (REWRITE_RULE [count_list_8, wordsTheory.word_mul_n2w] o 446 utilsLib.MATCH_HYP_CONV_RULE wordsLib.WORD_EVAL_CONV 447 ``n2w a <> n2w b: word4`` o 448 utilsLib.ALL_HYP_CONV_RULE 449 (DATATYPE_CONV 450 THENC SIMP_CONV std_ss 451 [alignmentTheory.aligned_add_sub_123, 452 word_bit_0_of_load, wordsTheory.word_mul_n2w] 453 THENC DATATYPE_CONV)) 454 |> addThms 455 val LoadMultiple_rwt = 456 EV [LDM, LDM_UPTO_def, IncPC_rwt, LDM_UPTO_PC, write'R_name_rwt, 457 Aligned_SP] 458 [[``~word_bit 8 (registers: word9)``, 459 ``b = ~word_bit (w2n (n: word4)) (registers: word9)``]] [] 460 ``dfn'LoadMultiple (b, n, registers)`` 461 |> List.map 462 (Drule.ADD_ASSUM ``n <> 13w: word4`` o 463 REWRITE_RULE 464 ([boolTheory.COND_ID, count_list_8] @ 465 List.drop 466 (utilsLib.mk_cond_update_thms [``:m0_state``], 3))) 467 |> addThms 468end 469 470(* -- *) 471 472local 473 val STM_UPTO_SUC = 474 m0_stepTheory.STM_UPTO_SUC 475 |> Thm.INST_TYPE [Type.alpha |-> ``:8``] 476 |> SIMP_RULE (srw_ss()) [] 477 |> upto_enumerate 7 478 479 val PUSH_UPTO_SUC = 480 m0_stepTheory.STM_UPTO_SUC 481 |> Thm.INST_TYPE [Type.alpha |-> ``:9``] 482 |> SIMP_RULE (srw_ss()) [] 483 |> upto_enumerate 7 484 485 val STM_thm = unfold_for_loop 7 dfn'StoreMultiple_def 486 val PUSH_thm = Conv.RIGHT_CONV_RULE PairedLambda.let_CONV 487 (unfold_for_loop 8 dfn'Push_def) 488 489 val cond_lsb = Q.prove( 490 `i < 8 ==> 491 (word_bit (w2n n) r ==> 492 (n2w (LowestSetBit (r: word8)) = n: word4)) ==> 493 ((if word_bit i r then 494 (x1, if (n2w i = n) /\ (i <> LowestSetBit r) then x2 else x3) 495 else 496 x4) = 497 (if word_bit i r then (x1, x3) else x4))`, 498 lrw [m0Theory.LowestSetBit_def, wordsTheory.word_reverse_thm, 499 CountLeadingZeroBits8] 500 \\ lrfs [] 501 \\ lfs [] 502 ) 503 |> Drule.UNDISCH_ALL 504 505 fun FOR_BETA_CONV i tm = 506 let 507 val b = pairSyntax.dest_snd tm 508 val (b, _, _) = 509 boolSyntax.dest_cond 510 (snd (pairSyntax.dest_pair (abs_body (rator b)))) 511 val n = fst (wordsSyntax.dest_word_bit b) 512 val _ = numLib.int_of_term n = i orelse raise ERR "FOR_BETA_CONV" "" 513 in 514 (Conv.RAND_CONV 515 (PairedLambda.GEN_BETA_CONV 516 THENC utilsLib.INST_REWRITE_CONV [cond_lsb] 517 THENC utilsLib.INST_REWRITE_CONV [write'MemA_4_rwt, R_name_rwt] 518 THENC REWRITE_CONV []) 519 THENC numLib.REDUCE_CONV 520 THENC REWRITE_CONV [cond_rand_thms, STM_UPTO_components, 521 STM_UPTO_0, STM_UPTO_SUC, PUSH_UPTO_SUC]) tm 522 end 523 524 fun rule thm = 525 thm 526 |> Conv.RIGHT_CONV_RULE 527 (REWRITE_CONV [R_name_rwt, SP_def, ASSUME ``n <> 15w: word4``] 528 THENC Conv.EVERY_CONV 529 (List.tabulate 530 (8, fn i => Conv.ONCE_DEPTH_CONV (FOR_BETA_CONV i)))) 531 |> utilsLib.ALL_HYP_CONV_RULE 532 (numLib.REDUCE_CONV 533 THENC REWRITE_CONV 534 [alignmentTheory.aligned_add_sub_123, Aligned_concat4, 535 STM_UPTO_components] 536 THENC wordsLib.WORD_EVAL_CONV) 537 538 val STM = rule STM_thm 539 val PUSH = rule PUSH_thm 540in 541 val StoreMultiple_rwt = 542 EV [STM, STM_UPTO_def, IncPC_rwt, write'R_name_rwt, 543 m0_stepTheory.R_x_not_pc, count_list_8] [[``n <> 13w: word4``]] [] 544 ``dfn'StoreMultiple (n, registers)`` 545 |> addThms 546 val Push_rwt = 547 EV [PUSH, STM_UPTO_def, IncPC_rwt, LR_def, R_name_rwt, write'R_name_rwt, 548 write'MemA_4_rwt, write'SP_def, m0_stepTheory.R_x_not_pc, 549 count_list_8] [] [] 550 ``dfn'Push (registers)`` 551 |> List.map 552 (utilsLib.ALL_HYP_CONV_RULE 553 (REWRITE_CONV [alignmentTheory.aligned_add_sub_123] 554 THENC wordsLib.WORD_EVAL_CONV) o 555 SIMP_RULE bool_ss 556 [wordsTheory.WORD_MULT_CLAUSES, wordsTheory.word_mul_n2w, 557 bit_count_9_m_8] o 558 REWRITE_RULE 559 (boolTheory.COND_ID :: 560 List.drop 561 (utilsLib.mk_cond_update_thms [``:m0_state``], 3))) 562 |> addThms 563end 564 565(* ----------- *) 566 567local 568 val word_bit_conv = wordsLib.WORD_BIT_INDEX_CONV true 569 val map_word_bit_rule = 570 List.map (Conv.CONV_RULE (Conv.LHS_CONV word_bit_conv)) 571 fun word_bit_thms n = 572 let 573 val v = bitstringSyntax.mk_vec n 0 574 fun wb i = wordsSyntax.mk_word_bit (numSyntax.term_of_int i, v) 575 in 576 List.tabulate (n, fn i => bitstringLib.word_bit_CONV (wb i)) 577 end 578 val suc_rule = 579 Conv.CONV_RULE 580 (Conv.LHS_CONV (Conv.RATOR_CONV (Conv.RAND_CONV reduceLib.SUC_CONV))) 581in 582 fun BIT_THMS_CONV n = 583 let 584 val wbit_thms = word_bit_thms n 585 val widx_thms = map_word_bit_rule wbit_thms 586 (* val dim_thm = 587 wordsLib.SIZES_CONV 588 (wordsSyntax.mk_dimindex (fcpSyntax.mk_int_numeric_type n)) 589 val thms = ref ([dim_thm, wordsTheory.bit_count_def] @ wbit_thms) *) 590 val thms = ref wbit_thms 591 val c = ref (PURE_REWRITE_CONV (!thms)) 592 fun bit_count_thms v = 593 let 594 fun upto_thm i = 595 wordsSyntax.mk_bit_count_upto (numSyntax.term_of_int i, v) 596 fun thm i t = 597 let 598 val thm = 599 wordsTheory.bit_count_upto_SUC 600 |> Drule.ISPECL [v, numSyntax.term_of_int (i - 1)] 601 |> suc_rule 602 in 603 i |> upto_thm 604 |> (Conv.REWR_CONV thm 605 THENC Conv.LAND_CONV (REWRITE_CONV widx_thms) 606 THENC Conv.RAND_CONV (Conv.REWR_CONV t) 607 THENC numLib.REDUCE_CONV) 608 end 609 fun loop a i = 610 if n < i then a else loop (thm i (hd a) :: a) (i + 1) 611 in 612 loop [Drule.ISPEC v wordsTheory.bit_count_upto_0] 1 613 end 614 in 615 fn tm => 616 (!c) tm 617 handle Conv.UNCHANGED => 618 let 619 val v = 620 HolKernel.find_term 621 (fn t => 622 case Lib.total bitstringSyntax.dest_v2w t of 623 SOME (_, ty) => 624 fcpSyntax.dest_int_numeric_type ty = n andalso 625 List.null (Term.free_vars t) 626 | NONE => false) tm 627 val () = thms := !thms @ (bit_count_thms v) 628 val () = c := PURE_REWRITE_CONV (!thms) 629 in 630 (!c) tm 631 end 632 end 633end 634 635val BIT_THMS_CONV_9 = BIT_THMS_CONV 9 636val BIT_THMS_CONV_8 = BIT_THMS_CONV 8 ORELSEC BIT_THMS_CONV_9 637 638local 639 val eq0_rwts = Q.prove( 640 `(NUMERAL (BIT1 x) <> 0) /\ (NUMERAL (BIT2 x) <> 0)`, 641 REWRITE_TAC [arithmeticTheory.NUMERAL_DEF, arithmeticTheory.BIT1, 642 arithmeticTheory.BIT2] 643 \\ DECIDE_TAC) 644 val count8 = rhsc count_list_8 645 (* val count9 = rhsc count_list_9 *) 646 val ok8 = Term.term_eq count8 647 (* val ok9 = Term.term_eq count9 *) 648 val STM1 = REWRITE_RULE [wordsTheory.word_mul_n2w] STM1_def 649 val LDM1_tm = Term.prim_mk_const {Thy = "m0_step", Name = "LDM1"} 650 val STM1_tm = Term.prim_mk_const {Thy = "m0_step", Name = "STM1"} 651 val f_tm = Term.mk_var ("f", Term.type_of ``m0_step$R_name b``) 652 val b_tm = Term.mk_var ("b", wordsSyntax.mk_int_word_type 32) 653 val r_tm = Term.mk_var ("r", ``:RName -> word32``) 654 val m_tm = Term.mk_var ("r", ``:word32 -> word8``) 655 val FOLDL1_CONV = Conv.REWR_CONV (Thm.CONJUNCT1 listTheory.FOLDL) 656 val FOLDL2_CONV = Conv.REWR_CONV (Thm.CONJUNCT2 listTheory.FOLDL) 657 val CONV0 = REWRITE_CONV [Thm.CONJUNCT1 wordsTheory.WORD_ADD_0, eq0_rwts] 658 val ONCE_FOLDL_LDM1_CONV = 659 (FOLDL2_CONV 660 THENC Conv.RATOR_CONV (Conv.RAND_CONV 661 (Conv.REWR_CONV LDM1_def 662 THENC Conv.RATOR_CONV (Conv.RATOR_CONV BIT_THMS_CONV_9) 663 THENC CONV0 664 THENC (Conv.REWR_CONV combinTheory.I_THM 665 ORELSEC Conv.RATOR_CONV (Conv.RAND_CONV 666 (Conv.RAND_CONV 667 (Conv.TRY_CONV BIT_THMS_CONV_9 668 THENC wordsLib.WORD_EVAL_CONV) 669 THENC PairedLambda.let_CONV)))))) 670 val ONCE_FOLDL_STM1_CONV = 671 (FOLDL2_CONV 672 THENC Conv.RATOR_CONV (Conv.RAND_CONV 673 (Conv.REWR_CONV STM1 674 THENC Conv.RATOR_CONV (Conv.RATOR_CONV BIT_THMS_CONV_8) 675 THENC CONV0 676 THENC (Conv.REWR_CONV combinTheory.I_THM 677 ORELSEC (Conv.RATOR_CONV 678 (Conv.RATOR_CONV 679 (Conv.TRY_CONV BIT_THMS_CONV_8 680 THENC numLib.REDUCE_CONV) 681 THENC PairedLambda.let_CONV) 682 THENC PURE_REWRITE_CONV [combinTheory.o_THM]))))) 683 val lconv = REPEATC ONCE_FOLDL_LDM1_CONV THENC FOLDL1_CONV 684 val sconv = REPEATC ONCE_FOLDL_STM1_CONV THENC FOLDL1_CONV 685 val lthms = ref ([]: thm list) 686 val sthms = ref ([]: thm list) 687 val lc = ref (PURE_REWRITE_CONV (!lthms)) 688 val sc = ref (PURE_REWRITE_CONV (!sthms)) 689in 690 fun FOLDL_LDM1_CONV tm = (!lc) tm 691 handle Conv.UNCHANGED => 692 let 693 val (f, r, l) = listSyntax.dest_foldl tm 694 val (ldm, f, b, v, s) = 695 case boolSyntax.strip_comb f of 696 (ld, [f, b, v, s]) => (ld, f, b, v, s) 697 | _ => raise ERR "FOLDL_LDM1_CONV" "" 698 val _ = Term.term_eq LDM1_tm ldm andalso ok8 l 699 orelse raise ERR "FOLDL_LDM1_CONV" "" 700 val df = Term.list_mk_comb (LDM1_tm, [f_tm, b_tm, v, st]) 701 val thm = lconv (listSyntax.mk_foldl (df, r_tm, count8)) 702 |> Drule.GEN_ALL 703 val () = lthms := thm :: (!lthms) 704 val () = lc := PURE_REWRITE_CONV (!lthms) 705 in 706 Drule.SPECL [s, r, f, b] thm 707 end 708 fun FOLDL_STM1_CONV tm = (!sc) tm 709 handle Conv.UNCHANGED => 710 let 711 val (f, m, l) = listSyntax.dest_foldl tm 712 val (stm, f, b, v, s) = 713 case boolSyntax.strip_comb f of 714 (stm, [f, b, v, s]) => (stm, f, b, v, s) 715 | _ => raise ERR "FOLDL_STM1_CONV" "" 716 val _ = Term.same_const STM1_tm stm andalso ok8 l 717 orelse raise ERR "FOLDL_STM1_CONV" "" 718 val df = Term.list_mk_comb (stm, [f_tm, b_tm, v, st]) 719 val thm = sconv (listSyntax.mk_foldl (df, m_tm, count8)) 720 |> Drule.GEN_ALL 721 val () = lthms := thm :: (!lthms) 722 val () = sc := PURE_REWRITE_CONV (!lthms) 723 in 724 Drule.SPECL [s, m, f, b] thm 725 end 726end 727 728local 729 val word_bit_tm = ``word_bit a (v2w b : word9)`` 730 val wb_cond_tm = ``if ~^word_bit_tm then r1 else r2: RName -> word32`` 731 val wb_match = Lib.can (Term.match_term wb_cond_tm) 732 val wb_rule = 733 utilsLib.MATCH_HYP_CONV_RULE 734 (REWRITE_CONV [boolTheory.DE_MORGAN_THM, word_bit_9_expand]) 735 val wb_rule_wb = wb_rule ``~^word_bit_tm`` 736 val wb_rule_nowb = wb_rule word_bit_tm 737in 738 fun split_wb_cond_rule wb thm = 739 let 740 val tm = rhsc thm 741 in 742 case Lib.total (HolKernel.find_term wb_match) tm of 743 SOME c => 744 let 745 val (c, _, _) = boolSyntax.dest_cond c 746 in 747 if wb 748 then wb_rule_wb (REWRITE_RULE [ASSUME c] thm) 749 else wb_rule_nowb 750 (REWRITE_RULE [ASSUME (boolSyntax.dest_neg c)] thm) 751 end 752 | NONE => thm 753 end 754end 755 756local 757 val be_tm = hd (endian true) 758 val le_tm = hd (endian false) 759 fun endian_rule thm = 760 REWRITE_RULE 761 [ASSUME (if Lib.exists (Lib.equal le_tm) (Thm.hyp thm) 762 then le_tm 763 else be_tm)] thm 764 fun NO_FREE_VARS_CONV tm = 765 if List.null (Term.free_vars tm) 766 then Conv.ALL_CONV tm 767 else Conv.NO_CONV tm 768 val LowestSetBit_CONV = 769 Conv.REWR_CONV m0Theory.LowestSetBit_def 770 THENC NO_FREE_VARS_CONV 771 THENC Conv.RAND_CONV bossLib.EVAL 772 THENC Conv.REWR_CONV m0_stepTheory.CountLeadingZeroBits8 773 THENC bossLib.EVAL 774 val BIT_COUNT_CONV = 775 Conv.REWR_CONV wordsTheory.bit_count_def 776 THENC Conv.RATOR_CONV (Conv.RAND_CONV wordsLib.SIZES_CONV) 777 THENC NO_FREE_VARS_CONV 778 THENC BIT_THMS_CONV_8 779 val bit_count_rule = 780 utilsLib.MATCH_HYP_CONV_RULE numLib.REDUCE_CONV ``~(a < 1n)`` o 781 utilsLib.FULL_CONV_RULE (Conv.DEPTH_CONV BIT_COUNT_CONV) 782 val word_bit_rule = 783 utilsLib.FULL_CONV_RULE 784 (utilsLib.WGROUND_CONV 785 THENC TRY_CONV BIT_THMS_CONV_8 786 THENC REWRITE_CONV []) 787 val mk_neq = boolSyntax.mk_neg o boolSyntax.mk_eq 788 fun mk_stm_wb_thm t = 789 let 790 val l = t |> boolSyntax.lhand 791 |> boolSyntax.rand 792 |> bitstringSyntax.dest_v2w |> fst 793 |> bitstringSyntax.bitlist_of_term 794 |> List.foldl 795 (fn (b, (i, a)) => (i - 1, if b then i :: a else a)) 796 (7, []) 797 |> snd |> tl 798 val base = boolSyntax.rhs (boolSyntax.rand t) 799 val t2 = 800 List.map (fn i => mk_neq (base, wordsSyntax.mk_wordii (i, 4))) l 801 |> (fn [] => boolSyntax.T | x => boolSyntax.list_mk_conj x) 802 val eq_thm = 803 boolSyntax.list_mk_forall 804 (Term.free_vars base, boolSyntax.mk_eq (t, t2)) 805 in 806 (* 807 set_goal ([], eq_thm) 808 *) 809 Tactical.prove(eq_thm, REPEAT Cases THEN EVAL_TAC) 810 end 811 val stm_rule1 = 812 utilsLib.MATCH_HYP_CONV_RULE 813 (Conv.RAND_CONV 814 (Conv.LHS_CONV (Conv.RAND_CONV (Conv.TRY_CONV LowestSetBit_CONV)))) 815 ``x ==> (n2w (LowestSetBit (l: word8)) = v2w q : word4)`` 816 fun stm_rule2 thm = 817 case List.find boolSyntax.is_imp_only (Thm.hyp thm) of 818 SOME t => 819 (case Lib.total mk_stm_wb_thm t of 820 SOME rwt => 821 utilsLib.MATCH_HYP_CONV_RULE 822 (PURE_REWRITE_CONV [rwt]) ``x ==> (a: word4 = b)`` thm 823 | NONE => thm) 824 | NONE => thm 825in 826 fun ldm_stm_rule s = 827 let 828 val s' = utilsLib.uppercase s 829 val ld = String.isPrefix "LDM" s' 830 in 831 if ld orelse String.isPrefix "POP" s' 832 then utilsLib.FULL_CONV_RULE numLib.REDUCE_CONV o endian_rule o 833 Conv.CONV_RULE (Conv.DEPTH_CONV FOLDL_LDM1_CONV) o 834 bit_count_rule o 835 word_bit_rule o 836 (if ld andalso s' <> "LDM" 837 then split_wb_cond_rule (String.isSubstring "(WB)" s') 838 else Lib.I) 839 else if String.isPrefix "STM" s' orelse String.isPrefix "PUSH" s' 840 then numLib.REDUCE_RULE o stm_rule2 o stm_rule1 o bit_count_rule o 841 endian_rule o 842 Conv.CONV_RULE (Conv.DEPTH_CONV FOLDL_STM1_CONV) o 843 word_bit_rule 844 else Lib.I 845 end 846end 847 848(* 849 850val v8 = rhsc (bitstringLib.n2w_v2w_CONV ``0x1w: word8``) 851val v8 = rhsc (bitstringLib.n2w_v2w_CONV ``0xFFw: word8``) 852 853val v9 = rhsc (bitstringLib.n2w_v2w_CONV ``0x1w: word9``) 854val v9 = rhsc (bitstringLib.n2w_v2w_CONV ``0x1FFw: word9``) 855 856val tm = 857 ``(FOLDL (m0_step$LDM1 f (s.REG (f n) + 4w) ^v9 s) s.REG 858 [0; 1; 2; 3; 4; 5; 6; 7])`` 859 860val tm = 861 ``FOLDL (m0_step$STM1 f (s.REG (f n) + 4w) ^v8 s) s.MEM 862 [0; 1; 2; 3; 4; 5; 6; 7]`` 863 864Count.apply FOLDL_LDM1_CONV tm 865Count.apply FOLDL_STM1_CONV tm 866 867*) 868 869(* ========================================================================= *) 870 871(* Fetch *) 872 873fun mk_bool_list l = listSyntax.mk_list (l, Type.bool) 874 875local 876 val err = ERR "dest_bool_list" "bad Bool list" 877in 878 fun dest_bool_list tm = 879 case Lib.total listSyntax.dest_list tm of 880 SOME (l, ty) => (ty = Type.bool orelse raise err; l) 881 | NONE => raise err 882end 883 884local 885 fun pad_opcode n = 886 let 887 val wty = fcpSyntax.mk_int_numeric_type n 888 in 889 fn v => 890 let 891 val l = dest_bool_list v 892 val () = ignore (List.length l <= n 893 orelse raise ERR "pad_opcode" "bad Bool list") 894 in 895 (utilsLib.padLeft boolSyntax.F n l, wty) 896 end 897 end 898 fun mk_thumb2_pair l = 899 let 900 val l1 = mk_bool_list (List.take (l, 16)) 901 val l2 = mk_bool_list (List.drop (l, 16)) 902 in 903 pairSyntax.mk_pair (l1, l2) 904 end 905 val pad_16 = pad_opcode 16 906 val pad_32 = pad_opcode 32 907 val hex_to_bits_16 = 908 mk_bool_list o fst o pad_16 o bitstringSyntax.bitstring_of_hexstring 909 val hex_to_bits_16x2 = 910 mk_thumb2_pair o fst o pad_32 o bitstringSyntax.bitstring_of_hexstring 911in 912 val split_thumb2_pat = mk_thumb2_pair o dest_bool_list 913 fun hex_to_bits s = 914 hex_to_bits_16 s 915 handle HOL_ERR {message = "bad Bool list", ...} => 916 hex_to_bits_16x2 s 917 fun mk_opcode v = 918 case Lib.total pairSyntax.dest_pair v of 919 SOME (l, r) => 920 let 921 val (opc1, ty) = pad_16 l 922 val (opc2, _) = pad_16 r 923 in 924 pairSyntax.mk_pair 925 (bitstringSyntax.mk_v2w (mk_bool_list opc1, ty), 926 bitstringSyntax.mk_v2w (mk_bool_list opc2, ty)) 927 end 928 | NONE => 929 let 930 val (opc, ty) = pad_16 v 931 in 932 bitstringSyntax.mk_v2w (mk_bool_list opc, ty) 933 end 934end 935 936local 937 val lem = Q.prove ( 938 `(!p. ((if p then v2w [b1; b2; b3] else v2w [b4; b5; b6]) = 7w : word3) = 939 (if p then b1 /\ b2 /\ b3 else b4 /\ b5 /\ b6)) /\ 940 (!p. ((if p then v2w [b1; b2] else v2w [b3; b4]) = 0w : word2) = 941 (if p then ~b1 /\ ~b2 else ~b3 /\ ~b4))`, 942 lrw [] 943 \\ CONV_TAC (Conv.LHS_CONV bitstringLib.v2w_eq_CONV) 944 \\ decide_tac) 945 946 val CONC_RULE = 947 SIMP_RULE (srw_ss()++boolSimps.LET_ss) 948 [bitstringTheory.fixwidth_def, bitstringTheory.field_def, 949 bitstringTheory.shiftr_def, bitstringTheory.w2w_v2w, lem] o 950 ONCE_REWRITE_RULE [bitstringTheory.word_concat_v2w_rwt] 951 952 val lem = 953 Drule.LIST_CONJ 954 [simpLib.SIMP_CONV (srw_ss()++wordsLib.WORD_EXTRACT_ss) [] 955 ``(15 >< 13) (((w1:word8) @@ (w2:word8)) : word16) : word3``, 956 simpLib.SIMP_CONV (srw_ss()++wordsLib.WORD_EXTRACT_ss) [] 957 ``(12 >< 11) (((w1:word8) @@ (w2:word8)) : word16) : word2``, 958 simpLib.SIMP_CONV (srw_ss()) [] ``a + 2w + 1w : word32``] 959 960 val rule = 961 CONC_RULE o 962 ASM_REWRITE_RULE [cond_rand_thms, lem, 963 bitstringTheory.word_extract_v2w, bitstringTheory.word_bits_v2w] 964 965 val ALIGNED_PLUS_RULE = 966 MATCH_HYP_RW [alignmentTheory.aligned_add_sub_123, 967 alignmentTheory.aligned_numeric] 968 ``aligned c (a + b : 'a word)`` 969 970 val thumb2_test_tm = 971 fix_datatype 972 ``((15 >< 13) (FST (MemA (^st.REG RName_PC,2) s): word16) = 7w: word3) /\ 973 (12 >< 11) (FST (MemA (^st.REG RName_PC,2) s): word16) <> 0w: word2`` 974 975 val not_thumb2_test_tm = boolSyntax.mk_neg thumb2_test_tm 976 977 val byte_tms = List.map fix_datatype 978 [``^st.MEM (^st.REG RName_PC) = ^(mk_byte 0)``, 979 ``^st.MEM (^st.REG RName_PC + 1w) = ^(mk_byte 8)``, 980 ``^st.MEM (^st.REG RName_PC + 2w) = ^(mk_byte 16)``, 981 ``^st.MEM (^st.REG RName_PC + 3w) = ^(mk_byte 24)``] 982 983 val fetch_thumb_rwts = 984 EV [Fetch_def, MemA_2_rwt] [[not_thumb2_test_tm], [thumb2_test_tm]] [] 985 ``Fetch`` 986 987 val fetch_thms = 988 [fetch_thumb_rwts 989 |> hd 990 |> Thm.DISCH not_thumb2_test_tm 991 |> Drule.ADD_ASSUM (List.nth (byte_tms, 0)) 992 |> Drule.ADD_ASSUM (List.nth (byte_tms, 1)) 993 |> Conv.CONV_RULE (utilsLib.INST_REWRITE_CONV [MemA_2_rwt]) 994 |> rule, 995 fetch_thumb_rwts 996 |> tl |> hd 997 |> Thm.DISCH thumb2_test_tm 998 |> Drule.ADD_ASSUM (List.nth (byte_tms, 0)) 999 |> Drule.ADD_ASSUM (List.nth (byte_tms, 1)) 1000 |> Drule.ADD_ASSUM (List.nth (byte_tms, 2)) 1001 |> Drule.ADD_ASSUM (List.nth (byte_tms, 3)) 1002 |> Conv.CONV_RULE 1003 (utilsLib.INST_REWRITE_CONV [MemA_2_rwt] THENC DATATYPE_CONV) 1004 |> ALIGNED_PLUS_RULE 1005 |> rule] 1006 1007 fun bytes2 l = Lib.split_after 8 l 1008 1009 fun bytes4 l = 1010 let 1011 val (b1, l) = Lib.split_after 8 l 1012 val (b2, l) = Lib.split_after 8 l 1013 val (b3, b4) = Lib.split_after 8 l 1014 in 1015 (b1, b2, b3, b4) 1016 end 1017 1018 fun build_byte n l = 1019 List.tabulate (8, 1020 fn i => (bitstringSyntax.mk_bit (7 - i + n) |-> List.nth (l, i))) 1021 1022 fun assign_thumb e = fn v => 1023 let 1024 val (b1, b2) = bytes2 (utilsLib.padLeft boolSyntax.F 16 v) 1025 in 1026 if e then build_byte 8 b2 @ build_byte 0 b1 1027 else build_byte 8 b1 @ build_byte 0 b2 1028 end 1029 1030 fun assign_thumb2 e = fn v => 1031 let 1032 val (b1, b2, b3, b4) = bytes4 v 1033 in 1034 if e then build_byte 24 b4 @ build_byte 16 b3 @ 1035 build_byte 8 b2 @ build_byte 0 b1 1036 else build_byte 24 b3 @ build_byte 16 b4 @ 1037 build_byte 8 b1 @ build_byte 0 b2 1038 end 1039 1040 fun ftch_thms tms = 1041 utilsLib.specialized "fetch" 1042 (utilsLib.WGROUND_CONV THENC DATATYPE_CONV, fix_datatypes tms) 1043 fetch_thms 1044 1045 fun fetch_thm tms = 1046 case ftch_thms tms of 1047 [thm1, thm2] => (thm1, thm2) 1048 | _ => raise ERR "fetch_thm" "expecting 1 or 2 theorems" 1049 1050 val rule = 1051 MATCH_HYP_RW [] ``a /\ b: bool`` o MATCH_HYP_RW [] ``a \/ b: bool`` 1052 1053 fun check (l, s) thm = 1054 if utilsLib.vacuous thm 1055 then raise ERR "fetch" (utilsLib.long_term_to_string l ^ " " ^ s) 1056 else thm 1057in 1058 fun fetch e = 1059 let 1060 val (thm1, thm2) = fetch_thm (endian e) 1061 in 1062 fn v => 1063 let 1064 val l = dest_bool_list v 1065 handle e as HOL_ERR {message = "bad Bool list", ...} => 1066 let 1067 val (l1, l2) = Lib.with_exn pairSyntax.dest_pair v e 1068 in 1069 dest_bool_list l1 @ dest_bool_list l2 1070 end 1071 in 1072 if List.length l <= 16 1073 then check (v, "is a Thumb-2 prefix") 1074 (rule (Thm.INST (assign_thumb e l) thm1)) 1075 else if List.length l = 32 1076 then check (v, "is not a Thumb-2 instruction") 1077 (rule (Thm.INST (assign_thumb2 e l) thm2)) 1078 else raise ERR "fetch" "length must be 16 or 32" 1079 end 1080 end 1081end 1082 1083fun fetch_hex tms = 1084 let 1085 val ftch = fetch tms 1086 in 1087 ftch o hex_to_bits 1088 end 1089 1090(* 1091 1092val ftch = fetch_hex true 1093val ftch = fetch_hex false 1094 1095Count.apply ftch "8F1FF3BF" 1096Count.apply ftch "8F1F" 1097Count.apply ftch "F3BF8F1F" 1098Count.apply ftch "F000BFFE" 1099 1100*) 1101 1102(* ========================================================================= *) 1103 1104(* Decode *) 1105 1106val DECODE_UNPREDICTABLE_rwt = 1107 EV [DECODE_UNPREDICTABLE_def, MachineCode_case_def] 1108 [] (mapl (`mc`, [``Thumb opc``, ``Thumb2 (opc1, opc2)``])) 1109 ``DECODE_UNPREDICTABLE (mc, e)`` 1110 |> List.map Drule.GEN_ALL 1111 1112val ConditionPassed_rwt = 1113 EV [ConditionPassed_def] [] [] 1114 ``ConditionPassed c`` |> hd 1115 1116local 1117 fun ConditionPassed cond = 1118 ConditionPassed_rwt 1119 |> Thm.INST [``c:word4`` |-> ``^cond``] 1120 |> Conv.RIGHT_CONV_RULE 1121 (DATATYPE_CONV 1122 THENC Conv.DEPTH_CONV bitstringLib.word_bit_CONV 1123 THENC Conv.DEPTH_CONV bitstringLib.extract_v2w_CONV 1124 THENC Conv.DEPTH_CONV bitstringLib.v2w_eq_CONV 1125 THENC SIMP_CONV bool_ss []) 1126 fun iConditionPassed i = 1127 wordsSyntax.mk_wordii (i, 4) 1128 |> ConditionPassed |> Conv.CONV_RULE wordsLib.WORD_EVAL_CONV 1129in 1130 val iConditionPassed_rwts = List.tabulate (16, iConditionPassed) 1131end 1132 1133local 1134 val DecodeImmShift_rwt = 1135 pairTheory.PAIR 1136 |> Q.ISPEC `DecodeImmShift x` 1137 |> Thm.SYM 1138 |> Drule.GEN_ALL 1139 fun selective_v2w_eq_CONV tm = 1140 let 1141 val r = boolSyntax.rhs tm 1142 in 1143 if wordsSyntax.size_of r = Arbnum.fromInt 4 1144 then raise ERR "selective_v2w_eq_CONV" "" 1145 else bitstringLib.v2w_eq_CONV tm 1146 end 1147in 1148 val DecodeThumb = 1149 DecodeThumb_def 1150 |> Thm.SPEC (bitstringSyntax.mk_vec 16 0) 1151 |> Lib.C Thm.AP_THM st 1152 |> Conv.RIGHT_CONV_RULE 1153 (Thm.BETA_CONV 1154 THENC REWRITE_CONV [m0Theory.boolify16_v2w, Decode_simps] 1155 THENC ONCE_REWRITE_CONV [DecodeImmShift_rwt] 1156 THENC Conv.DEPTH_CONV PairedLambda.let_CONV 1157 THENC Conv.DEPTH_CONV selective_v2w_eq_CONV 1158 THENC SIMP_CONV bool_ss 1159 ([pairTheory.FST, Decode_simps, BitCount, 1160 bit_count_lt_1] @ DECODE_UNPREDICTABLE_rwt) 1161 THENC Conv.DEPTH_CONV utilsLib.WGROUND_CONV 1162 THENC REWRITE_CONV [DecodeRegShift_rwt] 1163 THENC Conv.DEPTH_CONV PairedLambda.PAIRED_BETA_CONV) 1164end 1165 1166val DecodeThumb2 = 1167 DecodeThumb2_def 1168 |> Thm.SPEC 1169 (pairSyntax.mk_pair 1170 (bitstringSyntax.mk_vec 16 16, bitstringSyntax.mk_vec 16 0)) 1171 |> Lib.C Thm.AP_THM st 1172 |> Conv.RIGHT_CONV_RULE 1173 (Thm.BETA_CONV 1174 THENC PURE_REWRITE_CONV [pairTheory.FST, pairTheory.SND] 1175 THENC REWRITE_CONV [m0Theory.boolify16_v2w, Decode_simps] 1176 THENC Conv.DEPTH_CONV PairedLambda.let_CONV 1177 THENC Conv.DEPTH_CONV bitstringLib.v2w_eq_CONV 1178 THENC SIMP_CONV bool_ss DECODE_UNPREDICTABLE_rwt) 1179 1180local 1181 val v1 = fst (bitstringSyntax.dest_v2w (bitstringSyntax.mk_vec 16 0)) 1182 val v2 = fst (bitstringSyntax.dest_v2w (bitstringSyntax.mk_vec 32 0)) 1183 val lem = utilsLib.SRW_CONV [] ``(s with pcinc := x).PSR`` 1184 val rule = 1185 Conv.RIGHT_CONV_RULE 1186 (REWRITE_CONV [v2w_ground2, v2w_ground4] 1187 THENC utilsLib.WGROUND_CONV 1188 THENC REWRITE_CONV (lem :: iConditionPassed_rwts)) 1189in 1190 fun DecodeThumb_rwt pat = 1191 let 1192 val (thm, s) = 1193 (DecodeThumb, 1194 state_with_pcinc ``2w:word32`` :: fst (Term.match_term v1 pat)) 1195 handle HOL_ERR {message = "different constructors", 1196 origin_function = "raw_match_term", ...} => 1197 (DecodeThumb2, 1198 state_with_pcinc ``4w:word32`` :: fst (Term.match_term v2 pat)) 1199 in 1200 rule (Thm.INST s thm) 1201 end 1202end 1203 1204(* -- *) 1205 1206val thumb_patterns = List.map (I ## utilsLib.pattern) 1207 [("ADDS", "FFFTTFF_________"), 1208 ("SUBS", "FFFTTFT_________"), 1209 ("ADDS (imm3)", "FFFTTTF_________"), 1210 ("SUBS (imm3)", "FFFTTTT_________"), 1211 ("LSLS (imm)", "FFFFF___________"), 1212 ("LSRS (imm)", "FFFFT___________"), 1213 ("ASRS (imm)", "FFFTF___________"), 1214 ("MOVS", "FFTFF___________"), 1215 ("CMP (imm)", "FFTFT___________"), 1216 ("ADDS (imm)", "FFTTF___________"), 1217 ("SUBS (imm)", "FFTTT___________"), 1218 ("ANDS", "FTFFFFFFFF______"), 1219 ("EORS", "FTFFFFFFFT______"), 1220 ("LSLS", "FTFFFFFFTF______"), 1221 ("LSRS", "FTFFFFFFTT______"), 1222 ("ASRS", "FTFFFFFTFF______"), 1223 ("ADCS", "FTFFFFFTFT______"), 1224 ("SBCS", "FTFFFFFTTF______"), 1225 ("RORS", "FTFFFFFTTT______"), 1226 ("TST", "FTFFFFTFFF______"), 1227 ("RSBS", "FTFFFFTFFT______"), 1228 ("CMP", "FTFFFFTFTF______"), 1229 ("CMN", "FTFFFFTFTT______"), 1230 ("ORRS", "FTFFFFTTFF______"), 1231 ("MULS", "FTFFFFTTFT______"), 1232 ("BICS", "FTFFFFTTTF______"), 1233 ("MVNS", "FTFFFFTTTT______"), 1234 ("ADD", "FTFFFTFF________"), 1235 ("ADD (pc)", "FTFFFTFFT____TTT"), 1236 ("CMP (high)", "FTFFFTFT________"), 1237 ("MOV", "FTFFFTTF________"), 1238 ("MOV (pc)", "FTFFFTTFT____TTT"), 1239 ("BX", "FTFFFTTTF_______"), 1240 ("BLX", "FTFFFTTTT_______"), 1241 ("LDR (lit)", "FTFFT___________"), 1242 ("STR", "FTFTFFF_________"), 1243 ("STRH", "FTFTFFT_________"), 1244 ("STRB", "FTFTFTF_________"), 1245 ("LDRSB", "FTFTFTT_________"), 1246 ("LDR", "FTFTTFF_________"), 1247 ("LDRH", "FTFTTFT_________"), 1248 ("LDRB", "FTFTTTF_________"), 1249 ("LDRSH", "FTFTTTT_________"), 1250 ("STR (imm)", "FTTFF___________"), 1251 ("LDR (imm)", "FTTFT___________"), 1252 ("STRB (imm)", "FTTTF___________"), 1253 ("LDRB (imm)", "FTTTT___________"), 1254 ("STRH (imm)", "TFFFF___________"), 1255 ("LDRH (imm)", "TFFFT___________"), 1256 ("STR (sp)", "TFFTF___________"), 1257 ("LDR (sp)", "TFFTT___________"), 1258(* ("ADD (reg,pc)", "TFTFF___________"), *) 1259 ("ADD (sp)", "TFTFT___________"), 1260 ("ADD (sp,sp)", "TFTTFFFFF_______"), 1261 ("SUB (sp,sp)", "TFTTFFFFT_______"), 1262 ("SXTH", "TFTTFFTFFF______"), 1263 ("UXTH", "TFTTFFTFTF______"), 1264 ("SXTB", "TFTTFFTFFT______"), 1265 ("UXTB", "TFTTFFTFTT______"), 1266 ("PUSH", "TFTTFTF_________"), 1267 ("REV", "TFTTTFTFFF______"), 1268 ("REV16", "TFTTTFTFFT______"), 1269 ("REVSH", "TFTTTFTFTT______"), 1270 ("POP", "TFTTTTFF________"), 1271 ("POP (pc)", "TFTTTTFT________"), 1272 ("NOP", "TFTTTTTTFFFFFFFF"), 1273 ("STM", "TTFFF___________"), 1274 ("LDM", "TTFFT___________"), 1275 ("BEQ", "TTFTFFFF________"), 1276 ("BNE", "TTFTFFFT________"), 1277 ("BCS", "TTFTFFTF________"), 1278 ("BCC", "TTFTFFTT________"), 1279 ("BMI", "TTFTFTFF________"), 1280 ("BPL", "TTFTFTFT________"), 1281 ("BVS", "TTFTFTTF________"), 1282 ("BVC", "TTFTFTTT________"), 1283 ("BHI", "TTFTTFFF________"), 1284 ("BLS", "TTFTTFFT________"), 1285 ("BGE", "TTFTTFTF________"), 1286 ("BLT", "TTFTTFTT________"), 1287 ("BGT", "TTFTTTFF________"), 1288 ("BLE", "TTFTTTFT________"), 1289 ("B", "TTTFF___________") 1290 ] 1291 1292val thumb2_patterns = List.map (I ## utilsLib.pattern) 1293 [("BL", "TTTTF___________TT_T____________") 1294 ] 1295 1296(* -- *) 1297 1298local 1299 val sep1 = String.tokens (Lib.equal #",") 1300 val sep2 = String.tokens (fn c => c = #"-" orelse Char.isSpace c) 1301 fun err s = raise ERR "index" ("bad index: " ^ s) 1302 fun index s = case Int.fromString s of 1303 SOME i => (i < 16 orelse err s; i) 1304 | NONE => err s 1305 fun reg_array s = 1306 let 1307 val a = Array.array (16, boolSyntax.F) 1308 fun set i = Array.update (a, i, boolSyntax.T) 1309 in 1310 List.app 1311 (fn r => case sep2 r of 1312 [i] => set (index i) 1313 | [i, j] => 1314 let 1315 val x = index i 1316 val y = index j 1317 in 1318 Lib.for_se (Int.min (x, y)) (Int.max (x, y)) set 1319 end 1320 | _ => raise ERR "reg_array" "syntax error") (sep1 s) 1321 ; a 1322 end 1323in 1324 fun reg_list_subst (n, p) s = 1325 let 1326 val a = reg_array s 1327 in 1328 List.tabulate 1329 (n, fn i => Term.mk_var ("x" ^ Int.toString (i + p), Type.bool) |-> 1330 Array.sub (a, n - 1 - i)) 1331 end 1332end 1333 1334local 1335 val thumb_pats = 1336 Redblackmap.fromList String.compare 1337 (thumb_patterns @ List.map (I ## split_thumb2_pat) thumb2_patterns) 1338 fun printn s = TextIO.print (s ^ "\n") 1339 fun lsub s i = Char.toUpper (String.sub (s, i)) 1340 val splitAtSemi = utilsLib.splitAtChar (Lib.equal #";") 1341 fun sharePrefix3 s1 s2 = 1342 let 1343 val n = Int.min (3, Int.min (String.size s1, String.size s2)) 1344 val f1 = lsub s1 1345 val f2 = lsub s2 1346 fun loop i = i >= n orelse f1 i = f2 i andalso loop (i + 1) 1347 in 1348 loop 0 1349 end 1350 fun LDM_STM s = String.isPrefix "LDM" s orelse String.isPrefix "STM" s 1351 fun comma i = 1352 let 1353 val is = Int.toString i 1354 in 1355 fn "" => is 1356 | s => is ^ "," ^ s 1357 end 1358 val reglist = 1359 snd o 1360 List.foldr 1361 (fn (t, (i, s)) => 1362 (i + 1, if t = boolSyntax.T then comma i s else s)) (0, "") 1363 fun insertRegList i = 1364 fn "PUSH" => let 1365 val l = List.drop (i, 7) 1366 val lr = bitstringSyntax.dest_b (hd l) 1367 in 1368 "PUSH;" ^ (if lr then "14," else "") ^ reglist (tl l) 1369 end 1370 | "LDM" => let 1371 val l = List.drop (i, 5) 1372 val rn = List.take (l, 3) 1373 |> List.map bitstringSyntax.dest_b 1374 |> bitstringSyntax.bitlist_to_num 1375 |> Arbnum.toInt 1376 val registers = List.drop (l, 3) 1377 val wb = not (bitstringSyntax.dest_b 1378 (List.nth (registers, 7 - rn))) 1379 in 1380 (if wb then "LDM (wb);" else "LDM;") ^ reglist registers 1381 end 1382 | s => if Lib.mem s ["POP", "POP (pc)", "STM"] 1383 then s ^ ";" ^ reglist (List.drop (i, 8)) 1384 else s 1385in 1386 fun list_instructions () = Redblackmap.listItems thumb_pats 1387 val list_mnemonics = List.map fst o list_instructions 1388 val print_instructions = List.app printn o list_mnemonics 1389 fun mk_thumb_opcode s = 1390 let 1391 val (s1, s2) = splitAtSemi s 1392 val s1 = if s1 = "LDM (wb)" then "LDM" else s1 1393 val m = if s2 = "" 1394 then [] 1395 else let 1396 val s3 = String.extract (s2, 1, NONE) 1397 in 1398 if LDM_STM s1 1399 then reg_list_subst (8, 3) s3 1400 else if s1 = "PUSH" 1401 then [hd (reg_list_subst (15, 0) s3)] @ 1402 reg_list_subst (8, 1) s3 1403 else if String.isPrefix "POP" s1 1404 then reg_list_subst (8, 0) s3 1405 else raise ERR "mk_thumb_opcode" ("bad suffix: " ^ s) 1406 end 1407 in 1408 case Redblackmap.peek (thumb_pats, s1) of 1409 SOME pat => Term.subst m pat 1410 | NONE => 1411 let 1412 val p = list_mnemonics () 1413 |> List.filter (sharePrefix3 s1) 1414 |> Lib.commafy 1415 |> String.concat 1416 val p = if p = "" then "." else ". Try: " ^ p 1417 in 1418 raise ERR "mk_arm_opcode" ("Not found: " ^ s1 ^ p) 1419 end 1420 end 1421 fun thumb_instruction opc = 1422 let 1423 val f = case Lib.total listSyntax.dest_list opc of 1424 SOME (i, _) => insertRegList i 1425 | NONE => Lib.I 1426 fun mtch s = Term.match_term (mk_thumb_opcode s) opc 1427 in 1428 case List.filter (Lib.can mtch) (list_mnemonics()) of 1429 [] => raise ERR "thumb_instruction" "no match found" 1430 | [s] => f s 1431 | ["ADD", s as "ADD (pc)"] => s 1432 | ["MOV", s as "MOV (pc)"] => s 1433 | _ => raise ERR "thumb_instruction" "more than one match!" 1434 end 1435end 1436 1437(* -- *) 1438 1439local 1440 fun f ps = List.map (DecodeThumb_rwt o snd) ps 1441 val rwts_16 = f thumb_patterns 1442 val rwts_32 = f thumb2_patterns 1443 val pcinc2 = fix_datatype ``^st with pcinc := 2w`` 1444 val pcinc4 = fix_datatype ``^st with pcinc := 4w`` 1445 val DecodeThumb_tm = mk_arm_const "DecodeThumb" 1446 val DecodeThumb2_tm = mk_arm_const "DecodeThumb2" 1447 fun mk_decode_thumb t = 1448 Term.list_mk_comb (DecodeThumb_tm, [t, pcinc2]) 1449 handle HOL_ERR {message = "incompatible types", ...} => 1450 Term.list_mk_comb (DecodeThumb2_tm, [t, pcinc4]) 1451 val rewrites = 1452 [v2w_13_15_rwts, 1453 bitstringLib.v2n_CONV ``v2n [F;F;F;F;F]``, 1454 blastLib.BBLAST_PROVE 1455 ``((v2w [T;T;b;T] = 13w: word4) \/ (v2w [T;T;b;T] = 15w: word4)) = T``] 1456 val raise_tm = mk_arm_const "raise'exception" 1457 val avoid = 1458 List.filter 1459 (not o Lib.can (HolKernel.find_term (Term.same_const raise_tm) o rhsc)) 1460 val FINISH_RULE = 1461 List.map 1462 (utilsLib.ALL_HYP_CONV_RULE (REWRITE_CONV [boolTheory.DE_MORGAN_THM]) o 1463 Conv.RIGHT_CONV_RULE 1464 (REG_CONV THENC Conv.DEPTH_CONV bitstringLib.v2n_CONV)) 1465 val rwconv = REWRITE_CONV rewrites 1466in 1467 fun thumb_decode be = 1468 let 1469 val tms = endian be 1470 val x = (DATATYPE_CONV, fix_datatypes tms) 1471 fun gen_rws m r = rewrites @ utilsLib.specialized m x r 1472 val rw = REWRITE_CONV (gen_rws "decode Thumb" rwts_16 @ 1473 gen_rws "decode Thumb-2" rwts_32) 1474 val FALL_CONV = 1475 REWRITE_CONV 1476 (datatype_thms [v2w_ground4] @ 1477 gen_rws "decode Thumb (fallback)" [DecodeThumb] @ 1478 gen_rws "decode Thumb-2 (fallback)" [DecodeThumb2]) 1479 in 1480 fn v => 1481 let 1482 val tm = mk_decode_thumb (mk_opcode v) 1483 in 1484 (rw tm 1485 handle Conv.UNCHANGED => 1486 (WARN "arm_decode" "fallback (slow) decode" 1487 ; FALL_CONV tm)) 1488 |> utilsLib.split_conditions 1489 |> avoid 1490 |> FINISH_RULE 1491 |> (fn l => if List.null l 1492 then raise ERR "thumb_decode" 1493 ("unpredictable: " ^ 1494 utilsLib.long_term_to_string v) 1495 else l) 1496 end 1497 end 1498end 1499 1500fun thumb_decode_hex be = 1501 let 1502 val dec = thumb_decode be 1503 in 1504 dec o hex_to_bits 1505 end 1506 1507(* 1508 1509val be = false 1510val tst = Count.apply (thumb_decode true o mk_thumb_opcode) 1511val tst = Count.apply (thumb_decode_hex true) 1512 1513tst "CMP" 1514 1515tst "450F" 1516tst "9876" 1517tst "be01" 1518tst "B422" 1519tst "F000BFFE" 1520 1521tst "ADDS"; 1522tst "ADDS (imm3)"; 1523tst "SUBS"; 1524tst "SUBS (imm3)"; 1525tst "ANDS"; 1526tst "ADD"; 1527tst "CMP"; 1528tst "BEQ"; 1529 1530tst "PUSH"; 1531tst "POP"; 1532tst "STM"; 1533tst "LDM"; 1534 1535tst "MOV" 1536tst "MOVS" 1537 1538 1539*) 1540 1541(* ========================================================================= *) 1542 1543(* Run *) 1544 1545val NoOperation_rwt = 1546 EV [dfn'NoOperation_def, IncPC_rwt] [] [] 1547 ``dfn'NoOperation()`` 1548 |> addThms 1549 1550(* ---------------------------- *) 1551 1552local 1553 val f = rand o rand o rand o rator o utilsLib.lhsc 1554 val cnv = REWRITE_CONV [alignmentTheory.aligned_add_sub_123, 1555 alignmentTheory.aligned_numeric] 1556 in 1557 val BranchTarget_rwt = 1558 EV [dfn'BranchTarget_def, PC_rwt, BranchWritePC_rwt, 1559 Aligned_Branch9, Aligned_Branch12, Aligned_Branch_Wide6, 1560 Aligned_Branch_Wide10] [] 1561 [[`imm32` |-> f Aligned_Branch9], 1562 [`imm32` |-> f Aligned_Branch12], 1563 [`imm32` |-> f Aligned_Branch_Wide6], 1564 [`imm32` |-> f Aligned_Branch_Wide10]] 1565 ``dfn'BranchTarget imm32`` 1566 |> List.map (utilsLib.ALL_HYP_CONV_RULE cnv) 1567 |> addThms 1568 val BranchLinkImmediate_rwt = 1569 EV [dfn'BranchLinkImmediate_def, BranchWritePC_rwt, R_name_rwt, 1570 write'LR_def, write'R_name_rwt, PC_rwt, R_x_pc, RName_LR_rwt, 1571 Aligned_Branch_Wide10, Aligned_BranchLink] [] 1572 [[`imm32` |-> f Aligned_Branch_Wide10]] 1573 ``dfn'BranchLinkImmediate imm32`` 1574 |> List.map (utilsLib.ALL_HYP_CONV_RULE 1575 (EVAL_DATATYPE_CONV 1576 THENC REWRITE_CONV [R_x_pc] 1577 THENC utilsLib.WGROUND_CONV 1578 THENC cnv) o 1579 utilsLib.MATCH_HYP_CONV_RULE wordsLib.WORD_EVAL_CONV 1580 ``~(n2w a = b: word4)``) 1581 |> addThms 1582end 1583 1584(* ---------------------------- *) 1585 1586val BranchExchange_rwt = 1587 EV [dfn'BranchExchange_def, BXWritePC_rwt, R_name_rwt] 1588 [] [] 1589 ``dfn'BranchExchange m`` 1590 |> List.map (MATCH_HYP_RW [] ``word_bit x (y: word32)``) 1591 |> addThms 1592 1593(* ---------------------------- *) 1594 1595val BranchLinkExchangeRegister_rwt = 1596 EV [dfn'BranchLinkExchangeRegister_def, BLXWritePC_rwt, R_name_rwt, 1597 write'LR_def, write'R_name_rwt, PC_rwt, RName_LR_rwt, 1598 Aligned_BranchLinkEx] [] [] 1599 ``dfn'BranchLinkExchangeRegister m`` 1600 |> List.map (utilsLib.ALL_HYP_CONV_RULE (REWRITE_CONV []) o 1601 utilsLib.MATCH_HYP_CONV_RULE wordsLib.WORD_EVAL_CONV 1602 ``~(n2w a = b: word4)``) 1603 |> addThms 1604 1605(* ---------------------------- *) 1606 1607local 1608 val rwt = 1609 utilsLib.qm [wordsTheory.SHIFT_ZERO] 1610 ``(if n = 0 then (x: 'a word,s) else (x #>> n, ^st)) = (x #>> n, s)`` 1611in 1612 val ROR_rwt = 1613 EV [ROR_def, ROR_C_def] [] [] 1614 ``ROR (x: 'a word, n)`` 1615 |> hd 1616 |> SIMP_RULE bool_ss [rwt] 1617end 1618 1619(* ---------------------------- *) 1620 1621val () = setEvConv utilsLib.WGROUND_CONV 1622 1623local 1624 val DataProcessing_rwts = 1625 List.map 1626 (fn opc => 1627 let 1628 val i = wordsSyntax.uint_of_word opc 1629 val w = if 8 <= i andalso i <= 11 then [] else [write'R_name_rwt] 1630 in 1631 EV ([R_name_rwt, m0_stepTheory.R_x_not_pc, 1632 utilsLib.SET_RULE DataProcessing_def, DataProcessingALU_def, 1633 AddWithCarry, wordsTheory.FST_ADD_WITH_CARRY, 1634 ArithmeticOpcode_def, PC_rwt, IncPC_rwt, cond_rand_thms] @ 1635 w) 1636 [] [[`opc` |-> opc]] 1637 ``DataProcessing (opc, setflags, d, n, imm32, c)`` 1638 |> List.map (DATATYPE_RULE o COND_UPDATE_RULE) 1639 end) opcodes 1640in 1641 fun dp n = hd (List.nth (DataProcessing_rwts, n)) 1642end 1643 1644val tst = dp 8 1645val cmp = dp 10 1646val cmn = dp 11 1647val mov = dp 13 1648val mvn = dp 15 1649fun al () = List.tabulate (8, fn i => dp i) @ [dp 12, dp 14] 1650 1651(* ---------------------------- *) 1652 1653val psr_id = 1654 Thm.CONJ 1655 (utilsLib.mk_state_id_thm m0Theory.PSR_component_equality 1656 [["C", "N", "Z"], ["N"], ["Z"], ["C"], ["V"]]) 1657 (utilsLib.mk_state_id_thm m0Theory.m0_state_component_equality 1658 [["PSR", "REG", "count"], 1659 ["PSR", "REG", "count", "pcinc"]]) 1660 1661val Move_rwt = 1662 EV [dfn'Move_def, mov, bitstringTheory.word_concat_v2w_rwt, 1663 wordsTheory.WORD_OR_CLAUSES, psr_id] [[``d <> 13w:word4``]] [] 1664 ``dfn'Move (d, imm32)`` 1665 |> addThms 1666 1667val CompareImmediate_rwt = 1668 EV [dfn'CompareImmediate_def, cmp, bitstringTheory.word_concat_v2w_rwt] [] [] 1669 ``dfn'CompareImmediate (n, imm32)`` 1670 |> addThms 1671 1672val ArithLogicImmediate_rwt = 1673 EV ([dfn'ArithLogicImmediate_def, bitstringTheory.word_concat_v2w_rwt, 1674 psr_id] @ al()) [] (mapl (`op`, arithlogic)) 1675 ``dfn'ArithLogicImmediate (op, s, d, n, imm32)`` 1676 |> addThms 1677 1678val ShiftImmediate_rwt = 1679 EV [dfn'ShiftImmediate_def, R_name_rwt, mov, 1680 doRegister_def, ArithmeticOpcode_def, Shift_C_DecodeImmShift_rwt, 1681 wordsTheory.WORD_OR_CLAUSES] [[``d <> 13w:word4``]] 1682 [[`a` |-> boolSyntax.F, `b` |-> boolSyntax.F], 1683 [`a` |-> boolSyntax.F, `b` |-> boolSyntax.T], 1684 [`a` |-> boolSyntax.T, `b` |-> boolSyntax.F]] 1685 ``dfn'ShiftImmediate 1686 (F, T, d, m, 1687 FST (DecodeImmShift (v2w [a; b], imm5)), 1688 SND (DecodeImmShift (v2w [a; b], imm5)))`` 1689 |> List.map 1690 (Conv.CONV_RULE 1691 (Conv.LHS_CONV 1692 (REWRITE_CONV [] 1693 THENC Conv.DEPTH_CONV bitstringLib.v2w_n2w_CONV))) 1694 |> addThms 1695 1696val MoveRegister_rwt = 1697 EV [dfn'ShiftImmediate_def, R_name_rwt, mov, psr_id, 1698 doRegister_def, ArithmeticOpcode_def, 1699 Shift_C_LSL_rwt, SND_Shift_C_rwt] [[``d <> 15w:word4``]] [] 1700 ``dfn'ShiftImmediate (F, F, d, m, SRType_LSL, 0)`` 1701 |> addThms 1702 1703val MoveRegister_pc_rwt = 1704 EV [dfn'ShiftImmediate_def, R_name_rwt, ALUWritePC_rwt, 1705 doRegister_def, DataProcessingPC_def, DataProcessingALU_def, 1706 Shift_C_LSL_rwt, SND_Shift_C_rwt] [] [] 1707 ``dfn'ShiftImmediate (F, F, 15w, m, SRType_LSL, 0)`` 1708 |> addThms 1709 1710val MoveNegRegister_rwt = 1711 EV [dfn'ShiftImmediate_def, R_name_rwt, mvn, psr_id, 1712 doRegister_def, ArithmeticOpcode_def, 1713 Shift_C_LSL_rwt, SND_Shift_C_rwt] [[``d <> 13w:word4``]] [] 1714 ``dfn'ShiftImmediate (T, T, d, m, SRType_LSL, 0)`` 1715 |> addThms 1716 1717val Register_rwt = 1718 EV ([dfn'Register_def, R_name_rwt, doRegister_def, ArithmeticOpcode_def, 1719 Shift_C_LSL_rwt, psr_id] @ al()) 1720 [[``d <> 15w:word4``]] (mapl (`op`, arithlogic)) 1721 ``dfn'Register (op, setflags, d, n, m)`` 1722 |> addThms 1723 1724val Register_add_pc_rwt = 1725 EV [dfn'Register_def, R_name_rwt, doRegister_def, ALUWritePC_rwt, PC_rwt, 1726 DataProcessingPC_def, DataProcessingALU_def, Shift_C_LSL_rwt, 1727 AddWithCarry, wordsTheory.FST_ADD_WITH_CARRY] 1728 [] [] 1729 ``dfn'Register (4w, F, 15w, 15w, m)`` 1730 |> addThms 1731 1732val TestCompareRegister_rwt = 1733 EV ([dfn'TestCompareRegister_def, R_name_rwt, doRegister_def, 1734 ArithmeticOpcode_def, Shift_C_LSL_rwt, psr_id, cmp, tst, cmn] @ al()) 1735 [] (mapl (`op`, testcompare)) 1736 ``dfn'TestCompareRegister (op, n, m)`` 1737 |> addThms 1738 1739val ShiftRegister_rwt = 1740 EV [dfn'ShiftRegister_def, R_name_rwt, mov, mvn, ArithmeticOpcode_def, 1741 Shift_C_typ `F` `F`, Shift_C_typ `F` `T`, 1742 Shift_C_typ `T` `F`, Shift_C_typ `T` `T`] 1743 [[``d <> 13w:word4``]] 1744 (mapl (`typ`, [``SRType_LSL``, ``SRType_LSR``, 1745 ``SRType_ASR``, ``SRType_ROR``])) 1746 ``dfn'ShiftRegister (d, n, typ, m)`` 1747 |> addThms 1748 1749(* ---------------------------- *) 1750 1751val Multiply32_rwt = 1752 EV [dfn'Multiply32_def, R_name_rwt, write'R_name_rwt, 1753 m0_stepTheory.R_x_not_pc, IncPC_rwt] 1754 [[``d <> 13w:word4``]] [] 1755 ``dfn'Multiply32 (d, n, m)`` 1756 |> addThms 1757 1758(* ---------------------------- *) 1759 1760val ExtendByte_rwt = 1761 EV [dfn'ExtendByte_def, R_name_rwt, write'R_name_rwt, 1762 m0_stepTheory.R_x_not_pc, IncPC_rwt] 1763 [[``d <> 13w:word4``]] [] 1764 ``dfn'ExtendByte (u, d, m)`` 1765 |> addThms 1766 1767val ExtendHalfword_rwt = 1768 EV [dfn'ExtendHalfword_def, R_name_rwt, write'R_name_rwt, 1769 m0_stepTheory.R_x_not_pc, IncPC_rwt] 1770 [[``d <> 13w:word4``]] [] 1771 ``dfn'ExtendHalfword (u, d, m)`` 1772 |> addThms 1773 1774val ByteReverse_rwt = 1775 EV [dfn'ByteReverse_def, R_name_rwt, write'R_name_rwt, 1776 m0_stepTheory.R_x_not_pc, IncPC_rwt] 1777 [[``d <> 13w:word4``]] [] 1778 ``dfn'ByteReverse (d, m)`` 1779 |> addThms 1780 1781val ByteReversePackedHalfword_rwt = 1782 EV [dfn'ByteReversePackedHalfword_def, R_name_rwt, 1783 m0_stepTheory.R_x_not_pc, write'R_name_rwt, 1784 IncPC_rwt] [[``d <> 13w:word4``]] [] 1785 ``dfn'ByteReversePackedHalfword (d, m)`` 1786 |> addThms 1787 1788val ByteReverseSignedHalfword_rwt = 1789 EV [dfn'ByteReverseSignedHalfword_def, R_name_rwt, 1790 m0_stepTheory.R_x_not_pc, write'R_name_rwt, 1791 IncPC_rwt] [[``d <> 13w:word4``]] [] 1792 ``dfn'ByteReverseSignedHalfword (d, m)`` 1793 |> addThms 1794 1795(* ---------------------------- *) 1796 1797val Extend_rwt = 1798 utilsLib.map_conv (REWRITE_CONV [Extend_def]) 1799 [``Extend (T, w:'a word): 'b word``, 1800 ``Extend (F, w:'a word): 'b word``] 1801 1802val Extract_rwt = 1803 utilsLib.map_conv utilsLib.EXTRACT_CONV 1804 [``(15 >< 8) ((15 >< 0) (w: word32) : word16) : word8``, 1805 ``(7 >< 0) ((15 >< 0) (w: word32) : word16) : word8``] 1806 1807fun memEV ctxt tm = 1808 EV [dfn'LoadWord_def, dfn'LoadLiteral_def, 1809 dfn'LoadByte_def, dfn'LoadHalf_def, 1810 dfn'StoreWord_def, dfn'StoreByte_def, dfn'StoreHalf_def, 1811 MemU_1_rwt, MemU_2_rwt, MemU_4_rwt, 1812 write'MemU_1_rwt, write'MemU_2_rwt, write'MemU_4_rwt, 1813 PC_rwt, IncPC_rwt, write'R_name_rwt, R_name_rwt, 1814 m0_stepTheory.R_x_not_pc, m0Theory.offset_case_def, 1815 pairTheory.pair_case_thm, Shift_C_DecodeImmShift_rwt, Shift_C_LSL_rwt, 1816 alignmentTheory.aligned_add_sub_123, Shift_def, Extend_rwt, Extract_rwt] 1817 [[``t <> 13w:word4``]] ctxt tm 1818 |> List.map (utilsLib.ALL_HYP_CONV_RULE 1819 (REWRITE_CONV [] 1820 THENC utilsLib.INST_REWRITE_CONV [Aligned4_base_pc])) 1821 |> addThms 1822 1823(* ---------------------------- *) 1824 1825val LoadWord_rwt = 1826 memEV [[`mode` |-> ``immediate_form imm32``], 1827 [`mode` |-> ``register_form m``]] 1828 ``dfn'LoadWord (t, n, mode)`` 1829 1830val LoadLiteral_rwt = 1831 memEV [] 1832 ``dfn'LoadLiteral 1833 (t, w2w (v2w [b7; b6; b5; b4; b3; b2; b1; b0; F; F] : word10))`` 1834 1835(* ---------------------------- *) 1836 1837val LoadByte_rwts = 1838 memEV [[`mode` |-> ``immediate_form imm32``], 1839 [`mode` |-> ``register_form m``]] 1840 ``dfn'LoadByte (T, t, n, mode)`` 1841 1842val LoadSignedByte_rwts = 1843 memEV [[`mode` |-> ``immediate_form imm32``], 1844 [`mode` |-> ``register_form m``]] 1845 ``dfn'LoadByte (F, t, n, mode)`` 1846 1847(* ---------------------------- *) 1848 1849val LoadHalf_rwts = 1850 memEV [[`mode` |-> ``immediate_form imm32``], 1851 [`mode` |-> ``register_form m``]] 1852 ``dfn'LoadHalf (T, t, n, mode)`` 1853 1854val LoadSignedHalf_rwts = 1855 memEV [[`mode` |-> ``immediate_form imm32``], 1856 [`mode` |-> ``register_form m``]] 1857 ``dfn'LoadHalf (F, t, n, mode)`` 1858 1859(* ---------------------------- *) 1860 1861val StoreWord_rwt = 1862 memEV [[`mode` |-> ``immediate_form imm32``], 1863 [`mode` |-> ``register_form m``]] 1864 ``dfn'StoreWord (t, n, mode)`` 1865 1866(* ---------------------------- *) 1867 1868val StoreByte_rwt = 1869 memEV [[`mode` |-> ``immediate_form imm32``], 1870 [`mode` |-> ``register_form m``]] 1871 ``dfn'StoreByte (t, n, mode)`` 1872 1873(* ---------------------------- *) 1874 1875val StoreHalf_rwt = 1876 memEV [[`mode` |-> ``immediate_form imm32``], 1877 [`mode` |-> ``register_form m``]] 1878 ``dfn'StoreHalf (t, n, mode)`` 1879 1880val () = resetEvConv () 1881 1882(* ========================================================================= *) 1883 1884(* Evaluator *) 1885 1886local 1887 val word_bit_8 = 1888 bitstringLib.word_bit_CONV 1889 ``word_bit 8 (v2w [b8; b7; b6; b5; b4; b3; b2; b1; b0] : word9)`` 1890 val both_rwts = [v2w_13_15_rwts] 1891 val hyps_rwts = word_bit_8 :: both_rwts 1892 val conc_rwts = [LDM_UPTO_RUN, STM_UPTO_RUN, Extend_rwt, psr_id] @ both_rwts 1893 val eval_simp_rule = 1894 REWRITE_RULE conc_rwts o 1895 utilsLib.ALL_HYP_CONV_RULE (REWRITE_CONV hyps_rwts) 1896 fun ev tm = 1897 fn rwt => 1898 let 1899 val thm = eval_simp_rule (utilsLib.INST_REWRITE_CONV1 rwt tm) 1900 in 1901 if utilsLib.vacuous thm then NONE else SOME thm 1902 end 1903in 1904 fun eval pcinc tms = 1905 let 1906 val net = utilsLib.mk_rw_net utilsLib.lhsc (getThms pcinc tms) 1907 in 1908 fn tm => 1909 (case List.mapPartial (ev tm) (utilsLib.find_rw net tm) of 1910 [] => raise ERR "eval" "no valid step theorem" 1911 | [x] => x 1912 | l => (Parse.print_term tm 1913 ; print "\n" 1914 ; raise ERR "eval" "more than one valid step theorem")) 1915 handle HOL_ERR {message = "not found", 1916 origin_function = "find_rw", ...} => 1917 raise (Parse.print_term tm 1918 ; print "\n" 1919 ; ERR "eval" "instruction instance not supported") 1920 end 1921end 1922 1923local 1924 val u2 = wordsSyntax.mk_wordii (2, 32) 1925 val u4 = wordsSyntax.mk_wordii (4, 32) 1926 val get_val = fst o pairSyntax.dest_pair o rhsc 1927 val get_state = rhsc 1928 val state_exception_tm = mk_arm_const "m0_state_exception" 1929 fun mk_proj_exception r = Term.mk_comb (state_exception_tm, r) 1930 val MP_Next1 = Drule.MATCH_MP m0_stepTheory.NextStateM0_thumb 1931 val MP_Next2 = Drule.MATCH_MP m0_stepTheory.NextStateM0_thumb2 1932 val Run_CONV = utilsLib.Run_CONV ("m0", st) o get_val 1933 fun is_ineq tm = 1934 boolSyntax.is_eq (boolSyntax.dest_neg tm) handle HOL_ERR _ => false 1935in 1936 fun eval_thumb (be, sel) = 1937 let 1938 val tms = endian be @ spsel sel 1939 val ftch = fetch be 1940 val dec = thumb_decode be 1941 val run1 = (MP_Next1, eval u2 tms o Term.subst [state_with_pcinc u2]) 1942 val run2 = (MP_Next2, eval u4 tms o Term.subst [state_with_pcinc u4]) 1943 in 1944 fn n => fn v => 1945 let 1946 val (mp, run) = if pairSyntax.is_pair v then run2 else run1 1947 val thm1 = ftch v 1948 val thm2 = List.nth (dec v, n) 1949 val thm3 = Run_CONV thm2 1950 val thm4 = thm3 |> Drule.SPEC_ALL |> rhsc |> run 1951 val ineq_hyps = 1952 List.mapPartial 1953 (fn tm => if is_ineq tm then SOME (ASSUME tm) else NONE) 1954 (Thm.hyp thm4) 1955 val (thm2, thm4) = 1956 if List.null ineq_hyps 1957 then (thm2, thm4) 1958 else 1959 (utilsLib.ALL_HYP_CONV_RULE (REWRITE_CONV ineq_hyps) thm2, 1960 REWRITE_RULE ineq_hyps thm4) 1961 val r = get_state thm4 1962 handle HOL_ERR {origin_function = "dest_pair", ...} => 1963 (Parse.print_thm thm4 1964 ; print "\n" 1965 ; raise ERR "eval_thumb" "failed to fully evaluate") 1966 val thm5 = STATE_CONV (mk_proj_exception r) 1967 val thm = Drule.LIST_CONJ [thm1, thm2, thm3, thm4, thm5] 1968 in 1969 mp thm 1970 end 1971 end 1972end 1973 1974local 1975 val conditional = Redblackset.fromList String.compare 1976 ["BEQ", "BNE", "BCS", "BCC", "BMI", "BPL", "BVS", 1977 "BVC", "BHI", "BLS", "BGE", "BLT", "BGT", "BLE"] 1978 fun isConditional s = 1979 3 <= String.size s andalso 1980 Redblackset.member (conditional, String.extract (s, 0, SOME 3)) 1981 fun mk_ev config = 1982 let 1983 val ev = eval_thumb config 1984 in 1985 fn (s, v) => 1986 if isConditional s 1987 then [ev 1 v, ev 0 v] 1988 else [ldm_stm_rule s (ev 0 v)] 1989 end 1990in 1991 fun thumb_step config = 1992 let 1993 val ev = mk_ev config 1994 in 1995 fn s => 1996 let 1997 val v = mk_thumb_opcode s 1998 in 1999 ev (s, v) 2000 end 2001 end 2002 fun thumb_step_hex config = 2003 let 2004 val ev = mk_ev config 2005 in 2006 fn h => 2007 let 2008 val v = hex_to_bits h 2009 in 2010 ev (thumb_instruction v, v) 2011 end 2012 end 2013end 2014 2015fun thumb_step_code config = 2016 List.map (thumb_step_hex config) o 2017 (m0AssemblerLib.m0_code: string quotation -> string list) 2018 2019(* ---------------------------- *) 2020 2021(* testing: 2022 2023open m0_stepLib 2024 2025val be = true 2026val sel = true 2027val config = (be, sel) 2028val n = 0 2029val v = mk_thumb_opcode "POP" 2030 2031val fails = ref ([] : string list) 2032val ok = ref ([] : string list) 2033 2034val evs = Lib.total (Count.apply (thumb_step (true, true))) 2035val dec = thumb_decode true o mk_thumb_opcode 2036fun tst s = case evs s of 2037 SOME thm => (ok := s :: (!ok); SOME (s, thm)) 2038 | NONE => (fails := s :: (!fails); NONE) 2039 2040val l = 2041 (fails := [] 2042 ; ok := [] 2043 ; List.mapPartial (tst o fst) (list_instructions())) 2044 2045 (!ok) 2046 (!fails) 2047 2048val evs = Count.apply (thumb_step (false, false)) 2049 2050evs "POP" 2051evs "POP (pc)" 2052evs "POP; 1, 0" 2053evs "POP (pc); 1, 0" 2054evs "LDM (wb);5,0" 2055evs "STM; 3, 1" 2056evs "STM; 3, 1" 2057evs "LDM" 2058evs "LDM; 4, 2" 2059evs "LDM (wb); 4, 2" 2060evs "BVS"; 2061 2062*) 2063 2064end 2065