1(* ------------------------------------------------------------------------ 2 ARM step evaluator 3 ------------------------------------------------------------------------ *) 4 5structure arm_stepLib :> arm_stepLib = 6struct 7 8open HolKernel boolLib bossLib 9 10open armTheory arm_stepTheory arm_configLib 11open state_transformerSyntax blastLib 12 13structure Parse = 14struct 15 open Parse 16 val (tyg, (tmg, _)) = 17 (I ## term_grammar.mfupdate_overload_info 18 (Overload.remove_overloaded_form "add")) 19 arm_stepTheory.arm_step_grammars 20 val (Type, Term) = parse_from_grammars (tyg, tmg) 21end 22 23open Parse 24val _ = Parse.hide "add" 25 26val ERR = Feedback.mk_HOL_ERR "arm_stepLib" 27val WARN = Feedback.HOL_WARNING "arm_stepLib" 28 29val () = show_assums := true 30 31(* ========================================================================= *) 32 33val mk_byte = bitstringSyntax.mk_vec 8 34val rhsc = utilsLib.rhsc 35fun mapl x = utilsLib.augment x [[]] 36val splitAtSpace = utilsLib.splitAtChar Char.isSpace 37val a_of = utilsLib.accessor_fns o arm_configLib.mk_arm_type 38val u_of = utilsLib.update_fns o arm_configLib.mk_arm_type 39 40val REG_CONV = REWRITE_CONV [v2w_13_15_rwts, v2w_ground4] 41val REG_RULE = Conv.CONV_RULE REG_CONV 42 43val registers = utilsLib.tab_fixedwidth 15 4 44val opcodes = utilsLib.list_mk_wordii 4 (List.tabulate (16, Lib.I)) 45val arithlogic = utilsLib.list_mk_wordii 4 [0,1,2,3,4,5,6,7,12,14] 46val testcompare = utilsLib.list_mk_wordii 4 (List.tabulate (4, fn i => i + 8)) 47 48local 49 val c_of = TypeBase.constructors_of o arm_configLib.mk_arm_type 50in 51 val arches = c_of "Architecture" 52 val isets = c_of "InstrSet" 53 val shifts = c_of "SRType" 54 (* val encs = c_of "Encoding" *) 55end 56 57(* ---------------------------- *) 58 59local 60 val state_fns = a_of "arm_state" 61 val other_fns = 62 [pairSyntax.fst_tm, pairSyntax.snd_tm, bitstringSyntax.v2w_tm, 63 ``IncPC ()``, ``PSR_IT``, ``(h >< l) : 'a word -> 'b word``] @ 64 u_of "arm_state" 65 val exc = ``SND (raise'exception e s : 'a # arm_state)`` 66in 67 val cond_thms = 68 [SIMP_CONV std_ss [] ``if a then b else if a then c else d : 'a``, 69 boolTheory.COND_ID] 70 val cond_rand_thms = utilsLib.mk_cond_rand_thms (other_fns @ state_fns) 71 val snd_exception_thms = 72 utilsLib.map_conv 73 (Drule.GEN_ALL o 74 utilsLib.SRW_CONV [cond_rand_thms, armTheory.raise'exception_def] o 75 (fn tm => Term.mk_comb (tm, exc))) state_fns 76end 77 78(* ---------------------------- *) 79 80(* ARM datatype theorems/conversions *) 81 82val not_novfp = 83 GSYM (LIST_CONJ (List.take (CONJUNCTS armTheory.VFPExtension_distinct, 3))) 84 85fun datatype_thms thms = 86 [cond_rand_thms, snd_exception_thms, FST_SWAP, not_novfp, 87 arm_stepTheory.Align, arm_stepTheory.Aligned] @ thms @ cond_thms @ 88 utilsLib.datatype_rewrites true "arm" 89 ["arm_state", "Architecture", "RName", "InstrSet", "SRType", "Encoding", 90 "PSR", "VFPNegMul", "FP"] 91 92val DATATYPE_CONV = REWRITE_CONV (datatype_thms []) 93val DATATYPE_RULE = Conv.CONV_RULE DATATYPE_CONV 94val FULL_DATATYPE_RULE = utilsLib.FULL_CONV_RULE DATATYPE_CONV 95 96val COND_UPDATE_CONV = 97 REWRITE_CONV 98 (utilsLib.qm [] ``!b. (if b then T else F) = b`` :: 99 utilsLib.mk_cond_update_thms 100 (List.map arm_configLib.mk_arm_type ["arm_state", "FP", "PSR"])) 101 102val COND_UPDATE_RULE = Conv.CONV_RULE COND_UPDATE_CONV 103 104val STATE_CONV = 105 REWRITE_CONV (utilsLib.datatype_rewrites true "arm" ["arm_state"] @ 106 [boolTheory.COND_ID, cond_rand_thms]) 107 108local 109 val cmp = computeLib.bool_compset () 110 val () = computeLib.add_thms (datatype_thms [pairTheory.FST]) cmp 111in 112 val EVAL_DATATYPE_CONV = Conv.TRY_CONV (utilsLib.CHANGE_CBV_CONV cmp) 113end 114 115fun fix_datatype tm = rhsc (Conv.QCONV DATATYPE_CONV tm) 116val fix_datatypes = List.map fix_datatype 117 118fun specialized0 m tms = 119 utilsLib.specialized m (Conv.ALL_CONV, fix_datatypes tms) 120fun specialized1 m tms = 121 utilsLib.specialized m (utilsLib.WGROUND_CONV, fix_datatypes tms) 122 123fun state_with_enc e = (st |-> fix_datatype ``^st with Encoding := ^e``) 124 125fun state_with_pre (c, e) = 126 (st |-> 127 fix_datatype 128 ``^st with <| CurrentCondition := ^c; Encoding := ^e; undefined := F |>``) 129 130local 131 val c = Term.mk_var ("c", wordsSyntax.mk_int_word_type 4) 132 fun ADD_PRECOND_RULE e thm = 133 FULL_DATATYPE_RULE (Thm.INST [state_with_pre (c, e)] thm) 134 val rwts = ref ([]: thm list) 135in 136 fun getThms e tms = 137 List.map (ADD_PRECOND_RULE e) (specialized1 "eval" tms (!rwts)) 138 |> List.filter (not o utilsLib.vacuous) 139 fun resetThms () = rwts := [] 140 fun addThms thms = (rwts := thms @ !rwts; thms) 141end 142 143val EV = utilsLib.STEP (datatype_thms, st) 144val resetEvConv = utilsLib.resetStepConv 145val setEvConv = utilsLib.setStepConv 146 147(* ========================================================================= *) 148 149val ArchVersion_CPSR_rwt = Q.prove( 150 `!s c. ArchVersion () (s with CPSR := c) = ArchVersion () s`, 151 lrw [ArchVersion_def]) |> DATATYPE_RULE 152 153val () = setEvConv utilsLib.WGROUND_CONV 154 155val SelectInstrSet_rwt = 156 EV [SelectInstrSet_def, write'ISETSTATE_def, CurrentInstrSet_rwt] 157 [] (mapl (`iset`, isets)) 158 ``SelectInstrSet iset`` 159 160(* register access *) 161 162val () = resetEvConv () 163 164val PC_rwt = 165 EV [PC_def, R_def, CurrentInstrSet_rwt, not_cond] [] [] 166 ``PC`` |> hd 167 168local 169 val RBankSelect_rwt = 170 EV [RBankSelect_def, BadMode] [] [] 171 ``RBankSelect (mode,usr,fiq,irq,svc,abt,und,mon,hyp)`` |> hd 172 173 val RfiqBankSelect_rwt = 174 EV [RfiqBankSelect_def, RBankSelect_rwt] [] [] 175 ``RfiqBankSelect (mode,usr,fiq)`` |> hd 176 177 val LookUpRName_rwt = 178 EV [LookUpRName_def, mustbe15, RfiqBankSelect_rwt, RBankSelect_rwt] [] [] 179 ``LookUpRName (n,mode)`` |> hd 180 181 val thms = [merge_cond, cond_rand_thms, isnot15, IsSecure_def, 182 CurrentInstrSet_rwt, NotMon, HaveSecurityExt_def, Rmode_def, 183 write'Rmode_def, LookUpRName_rwt, arm_stepTheory.aligned_23] 184 185 val Rmode_rwt = 186 EV thms [[``Extension_Security NOTIN ^st.Extensions``]] [] 187 ``Rmode (n, m)`` |> hd 188 189 val write'Rmode_rwt = 190 EV thms 191 [[``Extension_Security NOTIN ^st.Extensions``, ``n <> 15w: word4``, 192 ``~((n = 13w: word4) /\ ~aligned 2 (v: word32) /\ ^st.CPSR.T)``]] 193 [] 194 ``write'Rmode (v, n, m)`` 195 |> hd 196 |> utilsLib.ALL_HYP_CONV_RULE 197 (REWRITE_CONV [boolTheory.DE_MORGAN_THM, 198 GSYM boolTheory.DISJ_ASSOC]) 199 200 val in_ext = GSYM (Q.ISPEC `^st.Extensions` pred_setTheory.SPECIFICATION) 201in 202 val R_rwt = Q.prove( 203 `GoodMode (^st.CPSR.M) ==> 204 ~^st.Extensions Extension_Security ==> 205 ~^st.CPSR.J ==> 206 (R n ^st = (if n = 15w then 207 ^st.REG RName_PC + if ^st.CPSR.T then 4w else 8w 208 else ^st.REG (R_mode (^st.CPSR.M) n), ^st))`, 209 lrw [R_def, R_mode_def, CurrentInstrSet_rwt, in_ext, DISCH_ALL Rmode_rwt] 210 \\ rfs [GoodMode_def] 211 \\ blastLib.FULL_BBLAST_TAC 212 ) 213 |> funpow 3 Drule.UNDISCH 214 215 val write'R_rwt = Q.prove( 216 `GoodMode (^st.CPSR.M) ==> 217 ~^st.Extensions Extension_Security==> 218 ~^st.CPSR.J ==> 219 n <> 15w ==> 220 ((n <> 13w) \/ aligned 2 v \/ ~^st.CPSR.T) ==> 221 (write'R (v, n) ^st = 222 ^st with REG := (R_mode (^st.CPSR.M) n =+ v) ^st.REG)`, 223 rewrite_tac [in_ext] 224 \\ ntac 4 strip_tac 225 \\ DISCH_THEN 226 (fn th => IMP_RES_TAC (MATCH_MP (DISCH_ALL write'Rmode_rwt) th)) 227 \\ simp [write'R_def] 228 \\ pop_assum kall_tac 229 \\ lrw [R_mode_def, CurrentInstrSet_rwt] 230 \\ fs [GoodMode_def] 231 \\ blastLib.FULL_BBLAST_TAC 232 ) 233 |> funpow 5 Drule.UNDISCH 234 235 val R15_rwt = Q.prove( 236 `~^st.CPSR.J ==> 237 (R 15w ^st = (^st.REG RName_PC + if ^st.CPSR.T then 4w else 8w, ^st))`, 238 lrw [R_def, CurrentInstrSet_rwt] \\ fs []) |> Drule.UNDISCH 239end 240 241(* ---------------------------- *) 242 243(* write PC *) 244 245val BranchTo_rwt = 246 EV [BranchTo_def] [] [] 247 ``BranchTo imm32`` |> hd 248 249local 250 val rwt = Q.prove (`!b. ((if b then 16 else 32) = 16n) = b`, rw []) 251in 252 val IncPC_rwt = 253 EV [IncPC_def, BranchTo_rwt, ThisInstrLength_def, rwt] [] [] 254 ``IncPC ()`` 255 |> hd 256end 257 258local 259 val a = 260 ``(^st.Architecture <> ARMv4) /\ (^st.Architecture <> ARMv4T) /\ 261 (^st.Architecture <> ARMv5T) /\ (^st.Architecture <> ARMv5TE) \/ 262 aligned 2 (imm32: word32)`` 263 val rwt = a |> boolSyntax.mk_neg |> utilsLib.SRW_CONV [] |> Thm.SYM 264in 265 val BranchWritePC_rwt = 266 EV [BranchWritePC_def, CurrentInstrSet_rwt, BranchTo_rwt, 267 ArchVersion_rwts, arm_stepTheory.aligned_23, not_cond, rwt, 268 Align_LoadWritePC] 269 [[``^st.CPSR.T``], [``~^st.CPSR.T``, a]] [] 270 ``BranchWritePC imm32`` 271end 272 273local 274 val rwt = 275 utilsLib.qm [] 276 ``(c ==> b) ==> 277 ((if b then x:'a else if ~c then y else z) = (if b then x else y))`` 278 |> Drule.UNDISCH 279in 280 val BXWritePC_rwt = 281 EV ([rwt, BXWritePC_def, BranchTo_rwt, CurrentInstrSet_rwt] @ 282 SelectInstrSet_rwt) [] [] 283 ``BXWritePC imm32`` |> hd 284end 285 286val align_aligned = UNDISCH_ALL (SPEC_ALL alignmentTheory.align_aligned) 287 288local 289 val rwt = Q.prove( 290 `(^st.Architecture = ARMv4) \/ (^st.Architecture = ARMv4T) ==> 291 (^st.Architecture <> ARMv4 /\ ^st.Architecture <> ARMv4T /\ 292 ^st.Architecture <> ARMv5T /\ ^st.Architecture <> ARMv5TE \/ 293 aligned 2 (imm32: word32) = aligned 2 imm32)`, 294 lrw [] \\ lfs []) |> Drule.UNDISCH 295 296 val LoadWritePC_rwt1 = 297 EV [LoadWritePC_def, BXWritePC_rwt, CurrentInstrSet_rwt, ArchVersion_rwts] 298 [[``^st.Architecture <> ARMv4 /\ ^st.Architecture <> ARMv4T``]] [] 299 ``LoadWritePC imm32`` 300 |> hd 301 |> COND_UPDATE_RULE 302 |> REWRITE_RULE [arm_stepTheory.Align_LoadWritePC] 303 304 val LoadWritePC_rwt2 = 305 EV [LoadWritePC_def, hd (BranchWritePC_rwt), CurrentInstrSet_rwt, 306 ArchVersion_rwts, arm_stepTheory.Align_LoadWritePC] 307 [[``~(^st.Architecture <> ARMv4 /\ ^st.Architecture <> ARMv4T)``]] [] 308 ``LoadWritePC imm32`` 309 |> hd 310 |> utilsLib.ALL_HYP_CONV_RULE (SIMP_CONV bool_ss []) 311 312 val LoadWritePC_rwt3 = 313 EV [LoadWritePC_def, hd (tl (BranchWritePC_rwt)), CurrentInstrSet_rwt, 314 ArchVersion_rwts, arm_stepTheory.Align_LoadWritePC, align_aligned] 315 [[``~(^st.Architecture <> ARMv4 /\ ^st.Architecture <> ARMv4T)``]] [] 316 ``LoadWritePC imm32`` 317 |> hd 318 |> utilsLib.ALL_HYP_CONV_RULE (SIMP_CONV bool_ss []) 319 |> utilsLib.MATCH_HYP_CONV_RULE (PURE_REWRITE_CONV [rwt]) 320 ``a \/ b : bool`` 321in 322 val LoadWritePC_rwt = [LoadWritePC_rwt1, LoadWritePC_rwt2, LoadWritePC_rwt3] 323end 324 325(* ---------------------------- *) 326 327val NullCheckIfThumbEE_rwt = 328 EV [NullCheckIfThumbEE_def, CurrentInstrSet_rwt] [] [] 329 ``NullCheckIfThumbEE n`` |> hd 330 331(* read mem *) 332 333fun fixwidth_for ty = 334 bitstringTheory.fixwidth_id 335 |> Q.ISPEC `w2v (w:^(ty_antiq (wordsSyntax.mk_word_type ty)))` 336 |> REWRITE_RULE [bitstringTheory.length_w2v] 337 |> Conv.CONV_RULE (Conv.DEPTH_CONV wordsLib.SIZES_CONV) 338 |> Drule.GEN_ALL 339 340val mem_rwt = 341 EV ([mem_def, mem1_def, concat16, concat32, concat64, 342 bitstringTheory.field_fixwidth] @ 343 List.map fixwidth_for [``:8``, ``:16``, ``:32``, ``:64``]) [] 344 (mapl (`n`, [``1n``,``2n``,``4n``,``8n``])) 345 ``mem (a, n)`` 346 347val BigEndianReverse_rwt = 348 EV [BigEndianReverse_def] [] (mapl (`n`, [``1n``,``2n``,``4n``,``8n``])) 349 ``BigEndianReverse (v, n)`` 350 351local 352 val rwts = 353 [MemA_with_priv_def, cond_rand_thms, snd_exception_thms, 354 wordsTheory.WORD_ADD_0, bitstringTheory.v2w_w2v, 355 AlignedAlign, alignmentTheory.aligned_0, alignmentTheory.align_0] @ 356 mem_rwt @ BigEndianReverse_rwt 357in 358 val MemA_with_priv_1_rwt = 359 EV (rwts @ [bitstringTheory.field_fixwidth, fixwidth_for ``:8``]) 360 [] [] 361 ``MemA_with_priv (v, 1, priv) : arm_state -> word8 # arm_state`` 362 |> hd 363 364 val MemU_with_priv_1_rwt = 365 EV (tl rwts @ [MemU_with_priv_def, MemA_with_priv_1_rwt]) 366 [] [] 367 ``MemU_with_priv (v, 1, priv) : arm_state -> word8 # arm_state`` 368 |> hd 369 370 val MemA_with_priv_2_rwt = 371 EV (extract16 :: rwts) 372 [[``aligned 1 (v:word32)``]] [] 373 ``MemA_with_priv (v, 2, priv) : arm_state -> word16 # arm_state`` 374 |> hd 375 376 val MemU_with_priv_2_rwt = 377 EV ([extract16, MemU_with_priv_def, MemA_with_priv_2_rwt] @ tl rwts) 378 [[``aligned 1 (v:word32)``]] [] 379 ``MemU_with_priv (v, 2, priv) : arm_state -> word16 # arm_state`` 380 |> hd 381 382 val MemA_with_priv_4_rwt = 383 EV (extract32 :: rwts) 384 [[``aligned 2 (v:word32)``]] [] 385 ``MemA_with_priv (v, 4, priv) : arm_state -> word32 # arm_state`` 386 |> hd 387 388 val MemU_with_priv_4_rwt = 389 EV ([extract16, MemU_with_priv_def, MemA_with_priv_4_rwt] @ tl rwts) 390 [[``aligned 2 (v:word32)``]] [] 391 ``MemU_with_priv (v, 4, priv) : arm_state -> word32 # arm_state`` 392 |> hd 393 394 val MemA_with_priv_8_rwt = 395 EV (extract64 :: rwts) 396 [[``aligned 3 (v:word32)``]] [] 397 ``MemA_with_priv (v, 8, priv) : arm_state -> word64 # arm_state`` 398 |> hd 399 400 val MemU_with_priv_8_rwt = 401 EV ([extract16, MemU_with_priv_def, MemA_with_priv_8_rwt] @ tl rwts) 402 [[``aligned 3 (v:word32)``]] [] 403 ``MemU_with_priv (v, 8, priv) : arm_state -> word64 # arm_state`` 404 |> hd 405end 406 407val MemA_unpriv_1_rwt = 408 EV [MemA_unpriv_def, MemA_with_priv_1_rwt] [] [] 409 ``MemA_unpriv (v, 1) : arm_state -> word8 # arm_state`` 410 411val MemU_unpriv_1_rwt = 412 EV [MemU_unpriv_def, MemU_with_priv_1_rwt] [] [] 413 ``MemU_unpriv (v, 1) : arm_state -> word8 # arm_state`` 414 415val MemA_unpriv_2_rwt = 416 EV [MemA_unpriv_def, MemA_with_priv_2_rwt] [] [] 417 ``MemA_unpriv (v, 2) : arm_state -> word16 # arm_state`` 418 419val MemU_unpriv_2_rwt = 420 EV [MemU_unpriv_def, MemU_with_priv_2_rwt] [] [] 421 ``MemU_unpriv (v, 2) : arm_state -> word16 # arm_state`` 422 423val MemA_unpriv_4_rwt = 424 EV [MemA_unpriv_def, MemA_with_priv_4_rwt] [] [] 425 ``MemA_unpriv (v, 4) : arm_state -> word32 # arm_state`` 426 427val MemU_unpriv_4_rwt = 428 EV [MemU_unpriv_def, MemU_with_priv_4_rwt] [] [] 429 ``MemU_unpriv (v, 4) : arm_state -> word32 # arm_state`` 430 431val MemA_unpriv_8_rwt = 432 EV [MemA_unpriv_def, MemA_with_priv_8_rwt] [] [] 433 ``MemA_unpriv (v, 8) : arm_state -> word64 # arm_state`` 434 435val MemU_unpriv_8_rwt = 436 EV [MemU_unpriv_def, MemU_with_priv_8_rwt] [] [] 437 ``MemU_unpriv (v, 8) : arm_state -> word64 # arm_state`` 438 439val MemA_1_rwt = 440 EV [MemA_def, MemA_with_priv_1_rwt, CurrentModeIsNotUser_def, BadMode] [] [] 441 ``MemA (v, 1) : arm_state -> word8 # arm_state`` 442 443val MemU_1_rwt = 444 EV [MemU_def, MemU_with_priv_1_rwt, CurrentModeIsNotUser_def, BadMode] [] [] 445 ``MemU (v, 1) : arm_state -> word8 # arm_state`` 446 447val MemA_2_rwt = 448 EV [MemA_def, MemA_with_priv_2_rwt, CurrentModeIsNotUser_def, BadMode] [] [] 449 ``MemA (v, 2) : arm_state -> word16 # arm_state`` 450 451val MemU_2_rwt = 452 EV [MemU_def, MemU_with_priv_2_rwt, CurrentModeIsNotUser_def, BadMode] [] [] 453 ``MemU (v, 2) : arm_state -> word16 # arm_state`` 454 455val MemA_4_rwt = 456 EV [MemA_def, MemA_with_priv_4_rwt, CurrentModeIsNotUser_def, BadMode] [] [] 457 ``MemA (v, 4) : arm_state -> word32 # arm_state`` 458 459val MemU_4_rwt = 460 EV [MemU_def, MemU_with_priv_4_rwt, CurrentModeIsNotUser_def, BadMode] [] [] 461 ``MemU (v, 4) : arm_state -> word32 # arm_state`` 462 463val MemA_8_rwt = 464 EV [MemA_def, MemA_with_priv_8_rwt, CurrentModeIsNotUser_def, BadMode] [] [] 465 ``MemA (v, 8) : arm_state -> word64 # arm_state`` 466 467val MemU_8_rwt = 468 EV [MemU_def, MemU_with_priv_8_rwt, CurrentModeIsNotUser_def, BadMode] [] [] 469 ``MemU (v, 8) : arm_state -> word64 # arm_state`` 470 471(* ---------------------------- *) 472 473(* write mem *) 474 475val write'mem_rwt = 476 EV ([write'mem_def]) [] (mapl (`n`, [``1n``,``2n``,``4n``,``8n``])) 477 ``write'mem (v, a, n)`` 478 479local 480 val field_cond_rand = Drule.ISPEC ``field h l`` boolTheory.COND_RAND 481 val rwts = 482 [write'MemA_with_priv_def, cond_rand_thms, snd_exception_thms, 483 wordsTheory.WORD_ADD_0, bitstringTheory.v2w_w2v, field_cond_rand, 484 AlignedAlign, alignmentTheory.aligned_0, alignmentTheory.align_0] @ 485 write'mem_rwt @ BigEndianReverse_rwt 486in 487 val write'MemA_with_priv_1_rwt = 488 EV (rwts @ [fixwidth_for ``:8``, bitstringTheory.field_fixwidth]) [] [] 489 ``write'MemA_with_priv (w: word8, v, 1, priv)`` 490 |> hd 491 492 val write'MemU_with_priv_1_rwt = 493 EV (tl rwts @ 494 [write'MemU_with_priv_def, write'MemA_with_priv_1_rwt, Align]) 495 [] [] 496 ``write'MemU_with_priv (w: word8, v, 1, priv)`` 497 |> hd 498 499 val write'MemA_with_priv_2_rwt = 500 EV (field16 :: rwts) [[``aligned 1 (v:word32)``]] [] 501 ``write'MemA_with_priv (w:word16, v, 2, priv)`` 502 |> hd 503 504 val write'MemU_with_priv_2_rwt = 505 EV ([write'MemU_with_priv_def, write'MemA_with_priv_2_rwt] @ tl rwts) 506 [[``aligned 1 (v:word32)``]] [] 507 ``write'MemU_with_priv (w: word16, v, 2, priv)`` 508 |> hd 509 510 val write'MemA_with_priv_4_rwt = 511 EV (field32 :: rwts) [[``aligned 2 (v:word32)``]] [] 512 ``write'MemA_with_priv (w:word32, v, 4, priv)`` 513 |> hd 514 515 val write'MemU_with_priv_4_rwt = 516 EV ([write'MemU_with_priv_def, write'MemA_with_priv_4_rwt] @ tl rwts) 517 [[``aligned 2 (v:word32)``]] [] 518 ``write'MemU_with_priv (w: word32, v, 4, priv)`` 519 |> hd 520end 521 522val write'MemA_unpriv_1_rwt = 523 EV [write'MemA_unpriv_def, write'MemA_with_priv_1_rwt] [] [] 524 ``write'MemA_unpriv (w: word8, v, 1)`` 525 526val write'MemU_unpriv_1_rwt = 527 EV [write'MemU_unpriv_def, write'MemU_with_priv_1_rwt] [] [] 528 ``write'MemU_unpriv (w: word8, v, 1)`` 529 530val write'MemA_unpriv_2_rwt = 531 EV [write'MemA_unpriv_def, write'MemA_with_priv_2_rwt] [] [] 532 ``write'MemA_unpriv (w: word16, v, 2)`` 533 534val write'MemU_unpriv_2_rwt = 535 EV [write'MemU_unpriv_def, write'MemU_with_priv_2_rwt] [] [] 536 ``write'MemU_unpriv (w: word16, v, 2)`` 537 538val write'MemA_unpriv_4_rwt = 539 EV [write'MemA_unpriv_def, write'MemA_with_priv_4_rwt] [] [] 540 ``write'MemA_unpriv (w: word32, v, 4)`` 541 542val write'MemU_unpriv_4_rwt = 543 EV [write'MemU_unpriv_def, write'MemU_with_priv_4_rwt] [] [] 544 ``write'MemU_unpriv (w: word32, v, 4)`` 545 546val write'MemA_1_rwt = 547 EV [write'MemA_def, write'MemA_with_priv_1_rwt, CurrentModeIsNotUser_def, 548 BadMode] [] [] 549 ``write'MemA (w: word8, v, 1)`` 550 551val write'MemU_1_rwt = 552 EV [write'MemU_def, write'MemU_with_priv_1_rwt, CurrentModeIsNotUser_def, 553 BadMode] [] [] 554 ``write'MemU (w: word8, v, 1)`` 555 556val write'MemA_2_rwt = 557 EV [write'MemA_def, write'MemA_with_priv_2_rwt, CurrentModeIsNotUser_def, 558 BadMode] [] [] 559 ``write'MemA (w: word16, v, 2)`` 560 561val write'MemU_2_rwt = 562 EV [write'MemU_def, write'MemU_with_priv_2_rwt, CurrentModeIsNotUser_def, 563 BadMode] [] [] 564 ``write'MemU (w: word16, v, 2)`` 565 566val write'MemA_4_rwt = 567 EV [write'MemA_def, write'MemA_with_priv_4_rwt, CurrentModeIsNotUser_def, 568 BadMode] [] [] 569 ``write'MemA (w: word32, v, 4)`` 570 571val write'MemU_4_rwt = 572 EV [write'MemU_def, write'MemU_with_priv_4_rwt, CurrentModeIsNotUser_def, 573 BadMode] [] [] 574 ``write'MemU (w: word32, v, 4)`` 575 576; 577 578(* ---------------------------- *) 579 580fun TF (t: term frag list) = [[t |-> boolSyntax.T], [t |-> boolSyntax.F]] 581 582val npc_thm = 583 List.map (fn r => Q.INST [`d: word4` |-> r] arm_stepTheory.R_x_not_pc) 584 585val Shift_C_rwt = 586 EV [Shift_C_def, LSL_C_def, LSR_C_def, ASR_C_def, ROR_C_def, RRX_C_def] [] [] 587 ``Shift_C (value,typ,amount,carry_in) 588 : arm_state -> ('a word # bool) # arm_state`` 589 |> hd 590 |> SIMP_RULE std_ss [] 591 592val SND_Shift_C_rwt = Q.prove( 593 `!s. SND (Shift_C (value,typ,amount,carry_in) s) = s`, 594 Cases_on `typ` \\ lrw [Shift_C_rwt]) |> Drule.GEN_ALL 595 596local 597 val rwt = 598 utilsLib.qm [wordsTheory.SHIFT_ZERO] 599 ``(if n = 0 then (x: 'a word,s) else (x #>> n, ^st)) = (x #>> n, s)`` 600in 601 val ROR_rwt = 602 EV [ROR_def, ROR_C_def] [] [] 603 ``ROR (x: 'a word, n)`` 604 |> hd 605 |> SIMP_RULE bool_ss [rwt] 606end 607 608val () = setEvConv (Conv.DEPTH_CONV 609 (bitstringLib.extract_v2w_CONV 610 ORELSEC bitstringLib.v2w_eq_CONV 611 ORELSEC bitstringLib.FIX_CONV 612 ORELSEC wordsLib.SIZES_CONV)) 613 614val arm_imm_lem = Q.prove( 615 `((if n = 0 then ((w, c1), s) else ((w #>> n, c2), s)) = 616 ((w #>> n, if n = 0 then c1 else c2), s)) /\ 617 (2 * w2n (v2w [a; b; c; d] : word4) = w2n (v2w [a; b; c; d; F] : word5))`, 618 rw [] \\ wordsLib.n2w_INTRO_TAC 5 \\ blastLib.BBLAST_TAC 619 ) 620 621val ARMExpandImm_C_rwt = 622 EV [ARMExpandImm_C_def, Shift_C_rwt, arm_imm_lem] [] [] 623 ``ARMExpandImm_C (^(bitstringSyntax.mk_vec 12 0), c)`` 624 |> hd 625 |> REWRITE_RULE [wordsTheory.w2n_eq_0] 626 627(* 628val ThumbExpandImm_C_rwt = 629 EV [ThumbExpandImm_C_def, ROR_C_def, wordsTheory.w2n_eq_0, 630 bitstringTheory.word_concat_v2w_rwt, merge_cond] [] [] 631 ``ThumbExpandImm_C (^(mk_vec 12 0), c)`` 632 |> hd 633*) 634 635val () = setEvConv utilsLib.WGROUND_CONV 636 637local 638 val rwt = Q.prove( 639 `(if b then (((x, y), s): (word32 # bool) # arm_state) else ((m, n), s)) = 640 ((if b then x else m, if b then y else n), s)`, 641 rw []) 642in 643 val ExpandImm_C_rwt = 644 EV [ExpandImm_C_def, ARMExpandImm_C_rwt, rwt] 645 [[``^st.Encoding <> Encoding_Thumb2``]] [] 646 ``ExpandImm_C (^(bitstringSyntax.mk_vec 12 0), c)`` 647 |> hd 648end 649 650(* ---------------------------- *) 651 652fun regEV npcs thms ctxt s tm = 653 let 654 val npc_thms = npc_thm npcs 655 val thms = 656 [ArchVersion_rwts, IncPC_rwt, cond_rand_thms, R_rwt, write'R_rwt] @ 657 npc_thms @ thms 658 val rule = 659 REWRITE_RULE npc_thms o FULL_DATATYPE_RULE o 660 Conv.CONV_RULE 661 (Conv.DEPTH_CONV (utilsLib.INST_REWRITE_CONV [write'R_rwt])) 662 in 663 EV thms ctxt s tm 664 |> List.map rule 665 |> addThms 666 end 667 668fun memEV rl mem thms ctxt s tm = 669 let 670 val thms = [NullCheckIfThumbEE_rwt, IncPC_rwt, PC_rwt, R_rwt, 671 armTheory.offset1_case_def, 672 armTheory.offset2_case_def, 673 pairTheory.pair_case_thm, 674 Shift_C_DecodeImmShift_rwt, Shift_C_LSL_rwt, Shift_def, 675 alignmentTheory.aligned_add_sub_123] @ thms 676 in 677 List.map (fn r => EV ([r] @ thms) ctxt s tm |> List.map rl) mem 678 |> List.concat 679 |> addThms 680 end 681 682fun storeEV rl mem thms ctxt s tm = 683 let 684 val thms = [NullCheckIfThumbEE_rwt, 685 Q.INST [`d` |-> `n`] arm_stepTheory.R_x_not_pc, 686 IncPC_rwt, PCStoreValue_def, PC_rwt, Shift_C_LSL_rwt, 687 CurrentInstrSet_rwt, Shift_def, SND_Shift_C_rwt, FST_SWAP, 688 boolTheory.COND_ID, merge_cond, cond_rand_thms, 689 armTheory.offset1_case_def, 690 armTheory.offset2_case_def, 691 pairTheory.pair_case_thm, 692 R_rwt, write'R_rwt] @ thms 693 val conv = REWRITE_CONV [boolTheory.COND_ID] THENC DATATYPE_CONV 694 val rule = rl o utilsLib.ALL_HYP_CONV_RULE conv 695 in 696 List.map (fn w => EV ([w] @ thms) ctxt s tm |> List.map rule) mem 697 |> List.concat 698 |> addThms 699 end 700 701(* ---------------------------- *) 702 703fun unfold_for_loop thm = 704 thm 705 |> REWRITE_RULE [utilsLib.for_thm (14,0), BitCount] 706 |> Drule.SPEC_ALL 707 |> Conv.CONV_RULE (Conv.X_FUN_EQ_CONV st) 708 |> Drule.SPEC_ALL 709 |> Conv.RIGHT_CONV_RULE 710 (PairedLambda.GEN_BETA_CONV 711 THENC REWRITE_CONV [NullCheckIfThumbEE_rwt] 712 THENC PairedLambda.let_CONV 713 THENC REWRITE_CONV [] 714 THENC PairedLambda.GEN_LET_CONV 715 THENC PairedLambda.let_CONV 716 THENC Conv.ONCE_DEPTH_CONV PairedLambda.GEN_BETA_CONV) 717 718val abs_body = snd o Term.dest_abs 719 720local 721 fun let_body t = let val (_, _, b) = pairSyntax.dest_plet t in b end 722 fun let_val t = let val (_, b, _) = pairSyntax.dest_plet t in b end 723 fun cond_true t = let val (_, b, _) = boolSyntax.dest_cond t in b end 724 val split_memA = 725 GSYM (Q.ISPEC `MemA x s : 'a word # arm_state` pairTheory.PAIR) 726 val split_R = GSYM (Q.ISPEC `R x s` pairTheory.PAIR) 727in 728 fun simp_for_body thm = 729 thm 730 |> Drule.SPEC_ALL 731 |> rhsc |> abs_body 732 |> let_body |> cond_true |> let_body |> let_body 733 |> let_val |> Term.rand |> Term.rator 734 |> state_transformerSyntax.dest_for |> (fn (_, _, b) => b) 735 |> abs_body |> abs_body 736 |> (SIMP_CONV bool_ss 737 [Once split_memA, Once split_R, pairTheory.pair_case_thm] 738 THENC Conv.DEPTH_CONV PairedLambda.GEN_LET_CONV 739 THENC SIMP_CONV std_ss [cond_rand_thms]) 740end 741 742fun upto_enumerate thm = 743 Drule.LIST_CONJ (List.tabulate (15, fn i => 744 let 745 val t = numSyntax.term_of_int i 746 in 747 Thm.CONJ (thm |> Thm.SPEC t |> numLib.REDUCE_RULE) 748 (numLib.REDUCE_CONV ``^t + 1``) 749 end)) 750 751(* -- *) 752 753val count_list_15 = EVAL ``COUNT_LIST 15`` 754 755local 756 val LDM_UPTO_SUC = upto_enumerate arm_stepTheory.LDM_UPTO_SUC 757 758 val LDM_lem = simp_for_body dfn'LoadMultiple_def 759 val LDM_thm = unfold_for_loop dfn'LoadMultiple_def 760 761 val cond_write'R_13_rwt = Q.prove( 762 `~^st.CPSR.J ==> GoodMode (^st.CPSR.M) ==> 763 ~^st.Extensions Extension_Security ==> 764 (p ==> (aligned 2 w \/ ~^st.CPSR.T)) ==> 765 ((if p then 766 ((), a, write'R (w, 13w) s) 767 else 768 ((), s2)) = 769 (if p then 770 ((), a, s with REG := (R_mode ^st.CPSR.M 13w =+ w) ^st.REG) 771 else 772 ((), s2)))`, 773 lrw [] \\ lrw [DISCH_ALL write'R_rwt]) 774 |> Drule.UNDISCH_ALL 775 776 val rearrange = Q.prove( 777 `!p a b n s. 778 (if p then write'R (a, n) s else write'R (b, n) s) = 779 write'R (if p then a else b, n) s`, 780 lrw []) 781 782 fun FOR_BETA_CONV i tm = 783 let 784 val b = pairSyntax.dest_snd tm 785 val (b, _, _) = boolSyntax.dest_cond (abs_body (rator b)) 786 val n = fst (wordsSyntax.dest_word_bit b) 787 val _ = numLib.int_of_term n = i orelse raise ERR "FOR_BETA_CONV" "" 788 val thm = if i = 13 then cond_write'R_13_rwt else write'R_rwt 789 in 790 (Conv.RAND_CONV 791 (PairedLambda.GEN_BETA_CONV 792 THENC Conv.REWR_CONV LDM_lem 793 THENC utilsLib.INST_REWRITE_CONV [hd MemA_4_rwt, thm]) 794 THENC REWRITE_CONV [cond_rand_thms, LDM_UPTO_components, 795 LDM_UPTO_0, LDM_UPTO_SUC]) tm 796 end 797 798 val pc_conv = 799 PairedLambda.let_CONV 800 THENC utilsLib.INST_REWRITE_CONV [hd MemA_4_rwt] 801 THENC REWRITE_CONV 802 [pairTheory.pair_case_thm, EVAL ``14 + 1n``, 803 alignmentTheory.aligned_numeric, 804 alignmentTheory.aligned_add_sub_123, 805 arm_stepTheory.Aligned_concat4, 806 LDM_UPTO_components] 807 THENC Conv.RAND_CONV 808 (Conv.RAND_CONV 809 (Conv.RATOR_CONV PairedLambda.GEN_BETA_CONV 810 THENC PairedLambda.GEN_BETA_CONV) 811 THENC PairedLambda.let_CONV) 812 813 val pc_tm = ``word_bit 15 (registers: word16)`` 814 815 fun LDM ispc a i = 816 let 817 val (tm, cnv) = if ispc then (pc_tm, pc_conv) 818 else (boolSyntax.mk_neg pc_tm, ALL_CONV) 819 in 820 LDM_thm 821 |> Q.INST [`increment` |-> a, `index` |-> i] 822 |> Conv.RIGHT_CONV_RULE 823 (REWRITE_CONV [R_rwt, ASSUME tm, ASSUME ``n <> 15w: word4``] 824 THENC Conv.EVERY_CONV 825 (List.tabulate 826 (15, fn i => Conv.ONCE_DEPTH_CONV (FOR_BETA_CONV i))) 827 THENC cnv) 828 |> utilsLib.ALL_HYP_CONV_RULE 829 (utilsLib.WGROUND_CONV 830 THENC REWRITE_CONV 831 [alignmentTheory.aligned_numeric, 832 alignmentTheory.aligned_add_sub_123, 833 arm_stepTheory.Aligned_concat4, 834 LDM_UPTO_components] 835 THENC numLib.REDUCE_CONV) 836 |> REWRITE_RULE [rearrange] 837 end 838 839 val LDM_PC = LDM true 840 val LDM = LDM false 841 842 val LDMDA_PC = LDM_PC `F` `F` 843 val LDMDB_PC = LDM_PC `F` `T` 844 val LDMIA_PC = LDM_PC `T` `F` 845 val LDMIB_PC = LDM_PC `T` `T` 846 847 val LDMDA = LDM `F` `F` 848 val LDMDB = LDM `F` `T` 849 val LDMIA = LDM `T` `F` 850 val LDMIB = LDM `T` `T` 851 852 val rule = 853 REWRITE_RULE [count_list_15] o 854 utilsLib.ALL_HYP_CONV_RULE 855 (DATATYPE_CONV 856 THENC REWRITE_CONV 857 [ASSUME ``aligned 2 (^st.REG (arm_step$R_mode ^st.CPSR.M n))``, 858 alignmentTheory.aligned_numeric, 859 alignmentTheory.aligned_add_sub_123, 860 arm_stepTheory.Aligned_concat4, 861 LDM_UPTO_components]) 862in 863 fun ldmEV wb = 864 EV [LDMDA, LDMDB, LDMIA, LDMIB, LDM_UPTO_def, IncPC_rwt, LDM_UPTO_PC, 865 write'R_rwt] 866 (if wb 867 then [[``~word_bit (w2n (n:word4)) (registers:word16)``]] 868 else []) 869 [[`inc` |-> ``F``, `index` |-> ``F``], 870 [`inc` |-> ``F``, `index` |-> ``T``], 871 [`inc` |-> ``T``, `index` |-> ``F``], 872 [`inc` |-> ``T``, `index` |-> ``T``]] 873 ``dfn'LoadMultiple 874 (inc, index, ^(bitstringSyntax.mk_b wb), n, registers)`` 875 |> List.map rule 876 |> addThms 877 878 fun ldm_pcEV wb = 879 List.map (fn wpc => 880 EV [LDMDA_PC, LDMDB_PC, LDMIA_PC, LDMIB_PC, LDM_UPTO_def, wpc, 881 LDM_UPTO_PC, write'R_rwt] 882 (if wb 883 then [[``~word_bit (w2n (n:word4)) (registers:word16)``]] 884 else []) 885 [[`inc` |-> ``F``, `index` |-> ``F``], 886 [`inc` |-> ``F``, `index` |-> ``T``], 887 [`inc` |-> ``T``, `index` |-> ``F``], 888 [`inc` |-> ``T``, `index` |-> ``T``]] 889 ``dfn'LoadMultiple 890 (inc, index, ^(bitstringSyntax.mk_b wb), n, registers)`` 891 |> List.map rule) 892 LoadWritePC_rwt 893 |> List.concat 894 |> addThms 895end 896 897val () = resetThms () 898 899val LoadMultiple_wb_rwt = ldmEV true 900val LoadMultiple_nowb_rwt = ldmEV false 901 902val LoadMultiple_pc_wb_rwt = ldm_pcEV true 903val LoadMultiple_pc_nowb_rwt = ldm_pcEV false 904 905(* -- *) 906 907local 908 val STM_UPTO_SUC = upto_enumerate arm_stepTheory.STM_UPTO_SUC 909 910 val STM_lem = simp_for_body dfn'StoreMultiple_def 911 val STM_thm = unfold_for_loop dfn'StoreMultiple_def 912 913 val cond_lsb = Q.prove( 914 `i < 16 ==> 915 (wb /\ word_bit (w2n n) r ==> 916 (n2w (LowestSetBit (r: word16)) = n: word4)) ==> 917 ((if word_bit i r then 918 ((), x1, 919 if (n2w i = n) /\ wb /\ (i <> LowestSetBit r) then x2 else x3) 920 else 921 ((), x4)) = 922 (if word_bit i r then ((), x1, x3) else ((), x4)))`, 923 lrw [armTheory.LowestSetBit_def, wordsTheory.word_reverse_thm, 924 CountLeadingZeroBits16] 925 \\ lrfs [] 926 \\ lfs [] 927 ) 928 |> Drule.UNDISCH_ALL 929 930 fun FOR_BETA_CONV i tm = 931 let 932 val b = pairSyntax.dest_snd tm 933 val (b, _, _) = boolSyntax.dest_cond (abs_body (rator b)) 934 val n = fst (wordsSyntax.dest_word_bit b) 935 val _ = numLib.int_of_term n = i orelse raise ERR "FOR_BETA_CONV" "" 936 in 937 (Conv.RAND_CONV 938 (PairedLambda.GEN_BETA_CONV 939 THENC Conv.REWR_CONV STM_lem 940 THENC utilsLib.INST_REWRITE_CONV [cond_lsb] 941 THENC utilsLib.INST_REWRITE_CONV [hd write'MemA_4_rwt, R_rwt] 942 THENC utilsLib.WGROUND_CONV) 943 THENC REWRITE_CONV [cond_rand_thms, STM_UPTO_components, 944 STM_UPTO_0, STM_UPTO_SUC]) tm 945 end 946in 947 fun STM a i = 948 STM_thm 949 |> Q.INST [`increment` |-> a, `index` |-> i] 950 |> Conv.RIGHT_CONV_RULE 951 (REWRITE_CONV [R_rwt, ASSUME ``n <> 15w: word4``] 952 THENC Conv.EVERY_CONV 953 (List.tabulate 954 (15, fn i => Conv.ONCE_DEPTH_CONV (FOR_BETA_CONV i)))) 955 |> utilsLib.ALL_HYP_CONV_RULE 956 (numLib.REDUCE_CONV 957 THENC REWRITE_CONV 958 [alignmentTheory.aligned_numeric, 959 alignmentTheory.aligned_add_sub_123, 960 arm_stepTheory.Aligned_concat4, 961 STM_UPTO_components] 962 THENC utilsLib.INST_REWRITE_CONV [R_rwt] 963 THENC DATATYPE_CONV) 964 |> utilsLib.ALL_HYP_CONV_RULE (REWRITE_CONV [STM_UPTO_components]) 965end 966 967local 968 val STMDA = STM `F` `F` 969 val STMDB = STM `F` `T` 970 val STMIA = STM `T` `F` 971 val STMIB = STM `T` `T` 972 973 val add4 = wordsLib.WORD_ARITH_PROVE 974 ``(a: 'a word - 4w * b + 4w + 4w * c = a + 4w * (c - b + 1w)) /\ 975 (a - 4w * b + 4w * c = a + 4w * (c - b)) /\ 976 (a + 4w * (-1w + 1w) = a) /\ 977 (a + 4w * -1w = a - 4w)`` 978 979 val rearrange = Q.prove( 980 `(if p then 981 s with <|MEM := a; REG := b|> 982 else 983 s with <|MEM := c; REG := d|>) = 984 s with <|MEM := if p then a else c; REG := if p then b else d|>`, 985 rw []) 986in 987 val StoreMultiple_rwt = 988 EV ([STMDA, STMDB, STMIA, STMIB, STM_UPTO_def, IncPC_rwt, 989 STM_UPTO_components, PCStoreValue_def, PC_def, add4, rearrange, 990 R_rwt, write'R_rwt, hd write'MemA_4_rwt] @ npc_thm [`n`]) [] 991 [[`inc` |-> ``F``, `index` |-> ``F``], 992 [`inc` |-> ``F``, `index` |-> ``T``], 993 [`inc` |-> ``T``, `index` |-> ``F``], 994 [`inc` |-> ``T``, `index` |-> ``T``]] 995 ``dfn'StoreMultiple (inc, index, wback, n, registers)`` 996 |> List.map 997 (SIMP_RULE std_ss [count_list_15, add4, bit_count_sub] o 998 utilsLib.MATCH_HYP_CONV_RULE 999 (utilsLib.INST_REWRITE_CONV 1000 [Drule.UNDISCH (DECIDE ``b ==> (a \/ b \/ c = T)``)]) 1001 ``a \/ b \/ c : bool`` o 1002 utilsLib.ALL_HYP_CONV_RULE 1003 (DATATYPE_CONV 1004 THENC REWRITE_CONV 1005 [boolTheory.COND_ID, 1006 alignmentTheory.aligned_numeric, 1007 alignmentTheory.aligned_add_sub_123]) o 1008 utilsLib.ALL_HYP_CONV_RULE 1009 (DATATYPE_CONV 1010 THENC SIMP_CONV std_ss 1011 [pairTheory.pair_case_thm, 1012 alignmentTheory.aligned_numeric, 1013 alignmentTheory.aligned_add_sub_123] 1014 THENC utilsLib.INST_REWRITE_CONV [hd write'MemA_4_rwt])) 1015 |> addThms 1016end 1017 1018(* ----------- *) 1019 1020val word_bit_16_thms = 1021 let 1022 val v = bitstringSyntax.mk_vec 16 0 1023 fun wb i = wordsSyntax.mk_word_bit (numSyntax.term_of_int i, v) 1024 in 1025 List.tabulate (16, fn i => bitstringLib.word_bit_CONV (wb i)) 1026 end 1027 1028local 1029 val word_bit_conv = wordsLib.WORD_BIT_INDEX_CONV true 1030 val word_index_16_thms = 1031 List.map (Conv.CONV_RULE (Conv.LHS_CONV word_bit_conv)) word_bit_16_thms 1032 val suc_rule = 1033 Conv.CONV_RULE 1034 (Conv.LHS_CONV (Conv.RATOR_CONV (Conv.RAND_CONV reduceLib.SUC_CONV))) 1035 fun bit_count_thms v = 1036 let 1037 fun upto_thm i = 1038 wordsSyntax.mk_bit_count_upto (numSyntax.term_of_int i, v) 1039 fun thm i t = 1040 let 1041 val thm = wordsTheory.bit_count_upto_SUC 1042 |> Drule.ISPECL [v, numSyntax.term_of_int (i - 1)] 1043 |> suc_rule 1044 in 1045 i |> upto_thm 1046 |> (Conv.REWR_CONV thm 1047 THENC Conv.LAND_CONV (REWRITE_CONV word_index_16_thms) 1048 THENC Conv.RAND_CONV (Conv.REWR_CONV t) 1049 THENC numLib.REDUCE_CONV) 1050 end 1051 fun loop a i = if 16 < i then a else loop (thm i (hd a) :: a) (i + 1) 1052 in 1053 loop [Drule.ISPEC v wordsTheory.bit_count_upto_0] 1 1054 end 1055 val thms = ref word_bit_16_thms 1056 val c = ref (PURE_REWRITE_CONV (!thms)) 1057in 1058 fun BIT_THMS_CONV tm = (!c) tm 1059 handle Conv.UNCHANGED => 1060 let 1061 val v = 1062 HolKernel.find_term 1063 (fn t => 1064 case Lib.total bitstringSyntax.dest_v2w t of 1065 SOME (_, ty) => fcpSyntax.dest_int_numeric_type ty = 16 1066 | NONE => false) tm 1067 val () = thms := !thms @ (bit_count_thms v) 1068 val () = c := PURE_REWRITE_CONV (!thms) 1069 in 1070 (!c) tm 1071 end 1072end 1073 1074local 1075 val eq0_rwts = Q.prove( 1076 `(NUMERAL (BIT1 x) <> 0) /\ (NUMERAL (BIT2 x) <> 0)`, 1077 REWRITE_TAC [arithmeticTheory.NUMERAL_DEF, arithmeticTheory.BIT1, 1078 arithmeticTheory.BIT2] 1079 \\ DECIDE_TAC) 1080 val count15 = rhsc count_list_15 1081 val STM1 = REWRITE_RULE [wordsTheory.word_mul_n2w] STM1_def 1082 val LDM1_tm = Term.prim_mk_const {Thy = "arm_step", Name = "LDM1"} 1083 val STM1_tm = Term.prim_mk_const {Thy = "arm_step", Name = "STM1"} 1084 val f_tm = Term.mk_var ("f", ``:word4 -> RName``) 1085 val b_tm = Term.mk_var ("b", wordsSyntax.mk_int_word_type 32) 1086 val r_tm = Term.mk_var ("r", ``:RName -> word32``) 1087 val m_tm = Term.mk_var ("r", ``:word32 -> word8``) 1088 val ok = Term.term_eq count15 1089 val FOLDL1_CONV = Conv.REWR_CONV (Thm.CONJUNCT1 listTheory.FOLDL) 1090 val FOLDL2_CONV = Conv.REWR_CONV (Thm.CONJUNCT2 listTheory.FOLDL) 1091 val CONV0 = REWRITE_CONV [Thm.CONJUNCT1 wordsTheory.WORD_ADD_0, eq0_rwts] 1092 val ONCE_FOLDL_LDM1_CONV = 1093 (FOLDL2_CONV 1094 THENC Conv.RATOR_CONV (Conv.RAND_CONV 1095 (Conv.REWR_CONV LDM1_def 1096 THENC Conv.RATOR_CONV (Conv.RATOR_CONV BIT_THMS_CONV) 1097 THENC CONV0 1098 THENC (Conv.REWR_CONV combinTheory.I_THM 1099 ORELSEC Conv.RATOR_CONV (Conv.RAND_CONV 1100 (Conv.RAND_CONV 1101 (Conv.TRY_CONV BIT_THMS_CONV 1102 THENC wordsLib.WORD_EVAL_CONV) 1103 THENC PairedLambda.let_CONV)))))) 1104 val ONCE_FOLDL_STM1_CONV = 1105 (FOLDL2_CONV 1106 THENC Conv.RATOR_CONV (Conv.RAND_CONV 1107 (Conv.REWR_CONV STM1 1108 THENC Conv.RATOR_CONV (Conv.RATOR_CONV BIT_THMS_CONV) 1109 THENC CONV0 1110 THENC (Conv.REWR_CONV combinTheory.I_THM 1111 ORELSEC (Conv.RATOR_CONV 1112 (Conv.RATOR_CONV 1113 (Conv.TRY_CONV BIT_THMS_CONV 1114 THENC numLib.REDUCE_CONV) 1115 THENC PairedLambda.let_CONV) 1116 THENC PURE_REWRITE_CONV [combinTheory.o_THM]))))) 1117 val lconv = REPEATC ONCE_FOLDL_LDM1_CONV THENC FOLDL1_CONV 1118 val sconv = REPEATC ONCE_FOLDL_STM1_CONV THENC FOLDL1_CONV 1119 val lthms = ref ([]: thm list) 1120 val sthms = ref ([]: thm list) 1121 val lc = ref (PURE_REWRITE_CONV (!lthms)) 1122 val sc = ref (PURE_REWRITE_CONV (!sthms)) 1123in 1124 fun FOLDL_LDM1_CONV tm = (!lc) tm 1125 handle Conv.UNCHANGED => 1126 let 1127 val (f, r, l) = listSyntax.dest_foldl tm 1128 val (ldm, f, b, v, s) = 1129 case boolSyntax.strip_comb f of 1130 (ld, [f, b, v, s]) => (ld, f, b, v, s) 1131 | _ => raise ERR "FOLDL_LDM1_CONV" "" 1132 val _ = Term.term_eq LDM1_tm ldm andalso ok l 1133 orelse raise ERR "FOLDL_LDM1_CONV" "" 1134 val df = Term.list_mk_comb (LDM1_tm, [f_tm, b_tm, v, st]) 1135 val thm = lconv (listSyntax.mk_foldl (df, r_tm, count15)) 1136 |> Drule.GEN_ALL 1137 val () = lthms := thm :: (!lthms) 1138 val () = lc := PURE_REWRITE_CONV (!lthms) 1139 in 1140 Drule.SPECL [s, r, f, b] thm 1141 end 1142 fun FOLDL_STM1_CONV tm = (!sc) tm 1143 handle Conv.UNCHANGED => 1144 let 1145 val (f, m, l) = listSyntax.dest_foldl tm 1146 val (stm, f, b, v, s) = 1147 case boolSyntax.strip_comb f of 1148 (stm, [f, b, v, s]) => (stm, f, b, v, s) 1149 | _ => raise ERR "FOLDL_STM1_CONV" "" 1150 val _ = Term.term_eq STM1_tm stm andalso ok l 1151 orelse raise ERR "FOLDL_STM1_CONV" "" 1152 val df = Term.list_mk_comb (STM1_tm, [f_tm, b_tm, v, st]) 1153 val thm = sconv (listSyntax.mk_foldl (df, m_tm, count15)) 1154 |> Drule.GEN_ALL 1155 val () = lthms := thm :: (!lthms) 1156 val () = sc := PURE_REWRITE_CONV (!lthms) 1157 in 1158 Drule.SPECL [s, m, f, b] thm 1159 end 1160end 1161 1162local 1163 val be_tm = ``^st.CPSR.E`` 1164 val le_tm = boolSyntax.mk_neg be_tm 1165 fun endian_rule thm = 1166 REWRITE_RULE 1167 [ASSUME (if Lib.exists (Lib.equal le_tm) (Thm.hyp thm) 1168 then le_tm 1169 else be_tm)] thm 1170 fun NO_FREE_VARS_CONV tm = 1171 if List.null (Term.free_vars tm) 1172 then Conv.ALL_CONV tm 1173 else Conv.NO_CONV tm 1174 val LowestSetBit_CONV = 1175 Conv.REWR_CONV armTheory.LowestSetBit_def 1176 THENC NO_FREE_VARS_CONV 1177 THENC Conv.RAND_CONV bossLib.EVAL 1178 THENC Conv.REWR_CONV arm_stepTheory.CountLeadingZeroBits16 1179 THENC bossLib.EVAL 1180 fun BIT_COUNT_UPTO_CONV tm = 1181 case boolSyntax.dest_strip_comb tm of 1182 ("words$bit_count_upto", [_, _]) => NO_FREE_VARS_CONV tm 1183 | ("words$bit_count", [v]) => 1184 (NO_FREE_VARS_CONV 1185 THENC Conv.REWR_CONV wordsTheory.bit_count_def 1186 THENC Conv.RATOR_CONV (Conv.RAND_CONV wordsLib.SIZES_CONV)) tm 1187 | _ => Conv.NO_CONV tm 1188 val BIT_COUNT_CONV = BIT_COUNT_UPTO_CONV THENC BIT_THMS_CONV 1189 val bit_count_rule = utilsLib.FULL_CONV_RULE (Conv.DEPTH_CONV BIT_COUNT_CONV) 1190 val rule = bit_count_rule o endian_rule 1191 fun ground_mul_conv tm = 1192 case Lib.total wordsSyntax.dest_word_mul tm of 1193 SOME (a, b) => 1194 if wordsSyntax.is_word_literal a andalso 1195 wordsSyntax.is_word_literal b 1196 then wordsLib.WORD_EVAL_CONV tm 1197 else raise ERR "ground_mul_conv" "" 1198 | NONE => raise ERR "ground_mul_conv" "" 1199 val ground_mul_rule = 1200 utilsLib.FULL_CONV_RULE (Conv.DEPTH_CONV ground_mul_conv) 1201 val stm_rule1 = 1202 utilsLib.MATCH_HYP_CONV_RULE 1203 (Conv.RAND_CONV 1204 (Conv.LHS_CONV (Conv.RAND_CONV (Conv.TRY_CONV LowestSetBit_CONV)))) 1205 ``x ==> (n2w (LowestSetBit (l: word16)) = v2w q : word4)`` 1206 val mk_neq = boolSyntax.mk_neg o boolSyntax.mk_eq 1207 fun mk_stm_wb_thm t = 1208 let 1209 val l = t |> boolSyntax.lhand 1210 |> boolSyntax.rand 1211 |> bitstringSyntax.dest_v2w |> fst 1212 |> bitstringSyntax.bitlist_of_term 1213 |> List.foldl 1214 (fn (b, (i, a)) => (i - 1, if b then i :: a else a)) 1215 (15, []) 1216 |> snd |> tl 1217 val base = boolSyntax.rhs (boolSyntax.rand t) 1218 val t2 = 1219 List.map (fn i => mk_neq (base, wordsSyntax.mk_wordii (i, 4))) l 1220 |> (fn [] => boolSyntax.T | x => boolSyntax.list_mk_conj x) 1221 val eq_thm = 1222 boolSyntax.list_mk_forall 1223 (Term.free_vars base, boolSyntax.mk_eq (t, t2)) 1224 in 1225 (* 1226 set_goal ([], eq_thm) 1227 *) 1228 Tactical.prove(eq_thm, NTAC 4 Cases THEN EVAL_TAC) 1229 end 1230 fun stm_rule2 thm = 1231 case List.find boolSyntax.is_imp_only (Thm.hyp thm) of 1232 SOME t => 1233 utilsLib.MATCH_HYP_CONV_RULE 1234 (PURE_REWRITE_CONV [mk_stm_wb_thm t]) ``x ==> (a: word4 = b)`` thm 1235 | NONE => thm 1236in 1237 fun ldm_stm_rule s = 1238 let 1239 val s' = utilsLib.uppercase s 1240 in 1241 if String.isPrefix "LDM" s' 1242 then ground_mul_rule o rule o 1243 Conv.CONV_RULE (Conv.DEPTH_CONV FOLDL_LDM1_CONV) 1244 else if String.isPrefix "STM" s' 1245 then ground_mul_rule o stm_rule2 o stm_rule1 o rule o 1246 Conv.CONV_RULE (Conv.DEPTH_CONV FOLDL_STM1_CONV) 1247 else Lib.I 1248 end 1249end 1250 1251(* 1252 1253val v = rhsc (bitstringLib.n2w_v2w_CONV ``0xFFFFw: word16``) 1254 1255val tm = ``(FOLDL (LDM1 R_usr (s.REG (R_usr n) + 4w) ^v s) s.REG 1256 [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14])`` 1257 1258val tm = 1259 ``FOLDL (STM1 R_usr (s.REG (R_usr n) + 4w) ^v s) s.MEM 1260 [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14]`` 1261 1262Count.apply FOLDL_LDM1_CONV tm 1263Count.apply FOLDL_STM1_CONV tm 1264 1265*) 1266 1267(* ========================================================================= *) 1268 1269(* Fetch *) 1270 1271local 1272 val lem = Q.prove ( 1273 `(!p. ((if p then v2w [b1; b2; b3] else v2w [b4; b5; b6]) = 7w : word3) = 1274 (if p then b1 /\ b2 /\ b3 else b4 /\ b5 /\ b6)) /\ 1275 (!p. ((if p then v2w [b1; b2] else v2w [b3; b4]) = 0w : word2) = 1276 (if p then ~b1 /\ ~b2 else ~b3 /\ ~b4))`, 1277 rw_tac std_ss [] 1278 \\ CONV_TAC (Conv.LHS_CONV bitstringLib.v2w_eq_CONV) 1279 \\ decide_tac) 1280 1281 val CONC_RULE = 1282 SIMP_RULE (srw_ss()++boolSimps.LET_ss) 1283 [bitstringTheory.fixwidth_def, bitstringTheory.field_def, 1284 bitstringTheory.shiftr_def, bitstringTheory.w2w_v2w, lem] o 1285 ONCE_REWRITE_RULE [bitstringTheory.word_concat_v2w_rwt] 1286 1287 val Fetch_v4_rwt = 1288 List.map (fn m => 1289 EV [Fetch_def, CurrentInstrSet_rwt, m] 1290 [[``^st.Architecture = ARMv4``, 1291 ``^st.MEM (^st.REG RName_PC) = ^(mk_byte 0)``, 1292 ``^st.MEM (^st.REG RName_PC + 1w) = ^(mk_byte 8)``, 1293 ``^st.MEM (^st.REG RName_PC + 2w) = ^(mk_byte 16)``, 1294 ``^st.MEM (^st.REG RName_PC + 3w) = ^(mk_byte 24)``]] [] 1295 ``Fetch``) MemA_4_rwt 1296 |> List.concat 1297 |> List.map 1298 (CONC_RULE o CONC_RULE o CONC_RULE o 1299 utilsLib.ALL_HYP_CONV_RULE DATATYPE_CONV) 1300 1301 val Fetch_arm_rwt = 1302 List.map (fn m => 1303 EV [Fetch_def, CurrentInstrSet_rwt, m] 1304 [[``~^st.CPSR.T``, 1305 ``^st.MEM (^st.REG RName_PC) = ^(mk_byte 0)``, 1306 ``^st.MEM (^st.REG RName_PC + 1w) = ^(mk_byte 8)``, 1307 ``^st.MEM (^st.REG RName_PC + 2w) = ^(mk_byte 16)``, 1308 ``^st.MEM (^st.REG RName_PC + 3w) = ^(mk_byte 24)``]] [] 1309 ``Fetch``) MemA_4_rwt 1310 |> List.concat 1311 |> List.map 1312 (CONC_RULE o CONC_RULE o CONC_RULE o 1313 utilsLib.ALL_HYP_CONV_RULE DATATYPE_CONV) 1314 1315 val lem = 1316 Drule.LIST_CONJ 1317 [simpLib.SIMP_CONV (srw_ss()++wordsLib.WORD_EXTRACT_ss) [] 1318 ``(15 >< 13) (((w1:word8) @@ (w2:word8)) : word16) : word3``, 1319 simpLib.SIMP_CONV (srw_ss()++wordsLib.WORD_EXTRACT_ss) [] 1320 ``(12 >< 11) (((w1:word8) @@ (w2:word8)) : word16) : word2``, 1321 simpLib.SIMP_CONV (srw_ss()) [] ``a + 2w + 1w : word32``] 1322 1323 val rule = 1324 CONC_RULE o 1325 ASM_REWRITE_RULE [cond_rand_thms, lem, 1326 bitstringTheory.word_extract_v2w, bitstringTheory.word_bits_v2w] o 1327 utilsLib.ALL_HYP_CONV_RULE DATATYPE_CONV 1328 1329 val ALIGNED_PLUS_RULE = 1330 utilsLib.MATCH_HYP_CONV_RULE 1331 (REWRITE_CONV [alignmentTheory.aligned_numeric, 1332 alignmentTheory.aligned_add_sub_123]) 1333 ``aligned c (a + b : 'a word)`` 1334 1335 val thumb2_test_tm = 1336 fix_datatype 1337 ``((15 >< 13) (FST (MemA (^st.REG RName_PC,2) s): word16) = 7w: word3) /\ 1338 (12 >< 11) (FST (MemA (^st.REG RName_PC,2) s): word16) <> 0w: word2`` 1339 1340 val not_thumb2_test_tm = boolSyntax.mk_neg thumb2_test_tm 1341 1342 val byte_tms = List.map fix_datatype 1343 [``^st.MEM (^st.REG RName_PC) = ^(mk_byte 0)``, 1344 ``^st.MEM (^st.REG RName_PC + 1w) = ^(mk_byte 8)``, 1345 ``^st.MEM (^st.REG RName_PC + 2w) = ^(mk_byte 16)``, 1346 ``^st.MEM (^st.REG RName_PC + 3w) = ^(mk_byte 24)``] 1347 1348 val fetch_thumb_rwts = 1349 EV [Fetch_def, CurrentInstrSet_rwt] 1350 [[``^st.CPSR.T``, ``^st.Architecture <> ARMv4``, 1351 not_thumb2_test_tm], 1352 [``^st.CPSR.T``, ``^st.Architecture <> ARMv4``, 1353 thumb2_test_tm]] [] 1354 ``Fetch`` 1355 1356 fun fetch_thumb m = 1357 [fetch_thumb_rwts 1358 |> hd 1359 |> Thm.DISCH not_thumb2_test_tm 1360 |> Drule.ADD_ASSUM (List.nth (byte_tms, 0)) 1361 |> Drule.ADD_ASSUM (List.nth (byte_tms, 1)) 1362 |> Conv.CONV_RULE (utilsLib.INST_REWRITE_CONV [m]) 1363 |> rule, 1364 fetch_thumb_rwts 1365 |> tl |> hd 1366 |> Thm.DISCH thumb2_test_tm 1367 |> Drule.ADD_ASSUM (List.nth (byte_tms, 0)) 1368 |> Drule.ADD_ASSUM (List.nth (byte_tms, 1)) 1369 |> Drule.ADD_ASSUM (List.nth (byte_tms, 2)) 1370 |> Drule.ADD_ASSUM (List.nth (byte_tms, 3)) 1371 |> Conv.CONV_RULE (utilsLib.INST_REWRITE_CONV [m] THENC DATATYPE_CONV) 1372 |> ALIGNED_PLUS_RULE 1373 |> rule] 1374 1375 val Fetch_thumb_rwt = List.map fetch_thumb MemA_2_rwt |> List.concat 1376 1377 val fetch_thms = Fetch_v4_rwt @ Fetch_arm_rwt @ Fetch_thumb_rwt 1378 1379 val thumb_tm = fix_datatype ``^st.CPSR.T`` 1380 val arm_tm = boolSyntax.mk_neg thumb_tm 1381 val big_tm = fix_datatype ``^st.CPSR.E`` 1382 val little_tm = boolSyntax.mk_neg big_tm 1383 1384 val v4 = fix_datatype ``^st.Architecture = ARMv4`` 1385 val not_v4 = boolSyntax.mk_neg v4 1386 fun is_v4 thm = List.exists (Lib.can (Term.match_term v4)) (Thm.hyp thm) 1387 fun is_not_v4 thm = 1388 List.exists (Lib.can (Term.match_term not_v4)) (Thm.hyp thm) 1389 1390 fun fix_not_v4 thm = 1391 if is_not_v4 thm 1392 then ASM_REWRITE_RULE (datatype_thms []) (Thm.DISCH not_v4 thm) 1393 else thm 1394 1395 fun bytes2 l = Lib.split_after 8 l 1396 1397 fun bytes4 l = 1398 let 1399 val (b1, l) = Lib.split_after 8 l 1400 val (b2, l) = Lib.split_after 8 l 1401 val (b3, b4) = Lib.split_after 8 l 1402 in 1403 (b1, b2, b3, b4) 1404 end 1405 1406 fun build_byte n l = 1407 List.tabulate (8, 1408 fn i => (bitstringSyntax.mk_bit (7 - i + n) |-> List.nth (l, i))) 1409 1410 fun assign_thumb e = fn v => 1411 let 1412 val (b1, b2) = bytes2 (utilsLib.padLeft boolSyntax.F 16 v) 1413 in 1414 if e then build_byte 8 b2 @ build_byte 0 b1 1415 else build_byte 8 b1 @ build_byte 0 b2 1416 end 1417 1418 fun assign_thumb2 e = fn v => 1419 let 1420 val (b1, b2, b3, b4) = bytes4 v 1421 in 1422 if e then build_byte 24 b4 @ build_byte 16 b3 @ 1423 build_byte 8 b2 @ build_byte 0 b1 1424 else build_byte 24 b3 @ build_byte 16 b4 @ 1425 build_byte 8 b1 @ build_byte 0 b2 1426 end 1427 1428 fun assign_arm e = fn v => 1429 let 1430 val (l, ty) = listSyntax.dest_list v 1431 val () = ignore (ty = Type.bool andalso List.length l <= 32 orelse 1432 raise ERR "fetch" "bad opcode") 1433 val (b1, b2, b3, b4) = bytes4 (utilsLib.padLeft boolSyntax.F 32 l) 1434 in 1435 if e then build_byte 24 b4 @ build_byte 16 b3 @ 1436 build_byte 8 b2 @ build_byte 0 b1 1437 else build_byte 24 b1 @ build_byte 16 b2 @ 1438 build_byte 8 b3 @ build_byte 0 b4 1439 end 1440 1441 fun ftch_thms tms = 1442 utilsLib.specialized "fetch" 1443 (utilsLib.WGROUND_CONV THENC DATATYPE_CONV, fix_datatypes tms) 1444 fetch_thms 1445 1446 fun fetch_thm tms = 1447 case ftch_thms tms of 1448 [thm] => sumSyntax.INL (fix_not_v4 thm) 1449 | [thm1, thm2] => 1450 if is_v4 thm1 1451 then sumSyntax.INL thm1 1452 else sumSyntax.INR (fix_not_v4 thm1, fix_not_v4 thm2) 1453 | _ => raise ERR "fetch_thm" "expecting 1 or 2 theorems" 1454 1455 val rule = 1456 utilsLib.MATCH_HYP_CONV_RULE (REWRITE_CONV []) ``a /\ b : bool`` o 1457 utilsLib.MATCH_HYP_CONV_RULE (REWRITE_CONV []) ``a \/ b : bool`` 1458 1459 fun check (l, s) thm = 1460 if utilsLib.vacuous thm 1461 then raise ERR "fetch" (utilsLib.long_term_to_string l ^ " " ^ s) 1462 else thm 1463in 1464 fun fetch tms = 1465 let 1466 val tms = List.map fix_datatype tms 1467 val e = List.exists (equal big_tm) tms 1468 val thms = fetch_thm tms 1469 in 1470 fn v => 1471 case thms of 1472 sumSyntax.INL thm => Thm.INST (assign_arm e v) thm 1473 | sumSyntax.INR (thm1, thm2) => 1474 let 1475 val (l, ty) = listSyntax.dest_list v 1476 in 1477 if ty = Type.bool 1478 then if List.length l <= 16 1479 then check (v, "is a Thumb-2 prefix") 1480 (rule (Thm.INST (assign_thumb e l) thm1)) 1481 else if List.length l = 32 1482 then check (v, "is not a Thumb-2 instruction") 1483 (rule (Thm.INST (assign_thumb2 e l) thm2)) 1484 else raise ERR "fetch" "length must be 16 or 32" 1485 else raise ERR "fetch" "not a bool list" 1486 end 1487 end 1488end 1489 1490fun fetch_hex tms = 1491 let 1492 val ftch = fetch tms 1493 in 1494 ftch o bitstringSyntax.bitstring_of_hexstring 1495 end 1496 1497(* 1498 1499val ftch = fetch_hex (arm_configLib.mk_config_terms "v4,16,le") 1500val ftch = fetch_hex (arm_configLib.mk_config_terms "16,le") 1501val ftch = fetch_hex (arm_configLib.mk_config_terms "") 1502 1503Count.apply ftch "8F1FF3BF" 1504Count.apply ftch "8F1F" 1505Count.apply ftch "F3BF8F1F" 1506 1507*) 1508 1509(* ========================================================================= *) 1510 1511(* Decode *) 1512 1513val DECODE_UNPREDICTABLE_rwt = 1514 EV [DECODE_UNPREDICTABLE_def, MachineCode_case_def] 1515 [] (mapl (`mc`, [``Thumb opc``, ``ARM opc``, ``Thumb2 (opc1, opc2)``])) 1516 ``DECODE_UNPREDICTABLE (mc, e)`` 1517 |> List.map Drule.GEN_ALL 1518 1519val Do_rwt = EV [Do_def] [] [] ``Do (c, def)`` |> hd 1520 1521val ConditionPassed_rwt = 1522 EV [ConditionPassed_def, CurrentCond_def] [] [] 1523 ``ConditionPassed ()`` |> hd 1524 1525local 1526 fun ConditionPassed cond = 1527 ConditionPassed_rwt 1528 |> Thm.INST 1529 [st |-> fix_datatype ``^st with CurrentCondition := ^cond``] 1530 |> Conv.RIGHT_CONV_RULE 1531 (DATATYPE_CONV 1532 THENC Conv.DEPTH_CONV bitstringLib.word_bit_CONV 1533 THENC Conv.DEPTH_CONV bitstringLib.extract_v2w_CONV 1534 THENC Conv.DEPTH_CONV bitstringLib.v2w_eq_CONV 1535 THENC SIMP_CONV bool_ss []) 1536 fun iConditionPassed i = 1537 wordsSyntax.mk_wordii (i, 4) 1538 |> ConditionPassed |> Conv.CONV_RULE wordsLib.WORD_EVAL_CONV 1539in 1540 val iConditionPassed_rwts = List.tabulate (16, iConditionPassed) 1541end 1542 1543val UndefinedARM_rwt = 1544 EV (UndefinedARM_def :: iConditionPassed_rwts) [] 1545 (mapl (`c`, fst (Lib.front_last opcodes))) 1546 ``UndefinedARM c`` 1547 1548val Skip_rwt = EV [Skip_def] [] [] ``Skip ()`` |> hd |> GEN_ALL 1549 1550val HaveDSPSupport_rwt = 1551 EV [HaveDSPSupport_def, utilsLib.SET_CONV ``a IN {ARMv4; ARMv4T; ARMv5T}``] 1552 [] [] 1553 ``HaveDSPSupport ()`` |> hd 1554 1555val DecodeImmShift_rwt = 1556 pairTheory.PAIR 1557 |> Q.ISPEC `DecodeImmShift x` 1558 |> Thm.SYM 1559 |> Drule.GEN_ALL 1560 1561val DecodeHint_rwt = 1562 EV [DecodeHint_def, boolify8_v2w, Skip_rwt, ArchVersion_rwts, Do_rwt] [] [] 1563 ``DecodeHint (c, ^(bitstringSyntax.mk_vec 8 0))`` 1564 |> hd 1565 1566local 1567 fun hasValueIn s = 1568 fn tm => let val i = wordsSyntax.uint_of_word tm in Lib.mem i s end 1569 1570 fun selective_v2w_eq_CONV tm = 1571 let 1572 val r = boolSyntax.rhs tm 1573 in 1574 if wordsSyntax.size_of r = Arbnum.fromInt 4 1575 andalso (bitstringSyntax.is_v2w r orelse hasValueIn [13, 15] r) 1576 then raise ERR "selective_v2w_eq_CONV" "" 1577 else bitstringLib.v2w_eq_CONV tm 1578 end 1579 1580 val DecodeARM = 1581 DecodeARM_def 1582 |> Thm.SPEC (bitstringSyntax.mk_vec 32 0) 1583 |> Lib.C Thm.AP_THM st 1584 |> Conv.RIGHT_CONV_RULE 1585 (Thm.BETA_CONV 1586 THENC Conv.DEPTH_CONV bitstringLib.extract_v2w_CONV 1587 THENC REWRITE_CONV 1588 ([Do_rwt, ArchVersion_rwts, Skip_rwt, 1589 ARMExpandImm_def, ARMExpandImm_C_rwt, 1590 (* DecodeImmShift_rwt, *) 1591 HaveDSPSupport_rwt, 1592 HaveThumb2_def, DecodeHint_rwt, 1593 armTheory.boolify28_v2w, Decode_simps, 1594 Q.ISPEC `x: Extensions set` pred_setTheory.SPECIFICATION, 1595 utilsLib.SET_CONV ``a IN {ARMv6T2; ARMv7_A; ARMv7_R}``, 1596 utilsLib.SET_CONV ``a IN {ARMv6K; ARMv7_A; ARMv7_R}``, 1597 utilsLib.SET_CONV ``(n:word4) IN {13w; 15w}``] @ 1598 iConditionPassed_rwts) 1599 THENC ONCE_REWRITE_CONV [DecodeImmShift_rwt] 1600 THENC Conv.DEPTH_CONV PairedLambda.let_CONV 1601 THENC Conv.DEPTH_CONV bitstringLib.word_bit_CONV 1602 THENC Conv.DEPTH_CONV bitstringLib.extract_v2w_CONV 1603 THENC Conv.DEPTH_CONV selective_v2w_eq_CONV 1604 THENC EVAL_DATATYPE_CONV 1605 THENC REWRITE_CONV 1606 ([armTheory.boolify4_v2w, (*DecodeImmShift_rwt, *) 1607 Decode_simps, BitCount, bit_count_lt_1] @ 1608 DECODE_UNPREDICTABLE_rwt) 1609 THENC Conv.DEPTH_CONV PairedLambda.PAIRED_BETA_CONV) 1610 1611 fun inst_cond f = 1612 Thm.INST 1613 (List.tabulate (4, fn i => bitstringSyntax.mk_bit (i + 28) |-> f i)) 1614 1615 val cond_case = 1616 utilsLib.qm [] 1617 ``!z b x y. (z = if b then x:'a else y) ==> (~b ==> (z = y))`` 1618in 1619 val DecodeVFP = 1620 DecodeVFP_def 1621 |> Thm.SPEC (bitstringSyntax.mk_vec 32 0) 1622 |> Lib.C Thm.AP_THM st 1623 |> Conv.RIGHT_CONV_RULE 1624 (Thm.BETA_CONV 1625 THENC Conv.DEPTH_CONV bitstringLib.extract_v2w_CONV 1626 THENC REWRITE_CONV 1627 [armTheory.boolify28_v2w, boolTheory.literal_case_THM] 1628 THENC Conv.ONCE_DEPTH_CONV Thm.BETA_CONV 1629 THENC Conv.DEPTH_CONV PairedLambda.GEN_LET_CONV 1630 THENC REWRITE_CONV [cond_rand_thms] 1631 THENC Conv.DEPTH_CONV bitstringLib.word_bit_CONV 1632 THENC Conv.DEPTH_CONV bitstringLib.extract_v2w_CONV 1633 THENC Conv.DEPTH_CONV selective_v2w_eq_CONV 1634 THENC REWRITE_CONV 1635 [armTheory.boolify4_v2w, Decode_simps, VFPExpandImm, 1636 utilsLib.SET_CONV ``a IN {VFPv3; VFPv4}``]) 1637 1638 val DecodeARM_15 = DecodeARM |> inst_cond (K boolSyntax.T) |> REG_RULE 1639 1640 val DecodeARM_14 = 1641 DecodeARM 1642 |> inst_cond (fn i => bitstringSyntax.mk_b (0 < i)) 1643 |> REWRITE_RULE ([v2w_13_15_rwts, v2w_ground4] @ iConditionPassed_rwts) 1644 1645 val DecodeARM_other = Drule.UNDISCH (Drule.MATCH_MP cond_case DecodeARM) 1646 1647 val DecodeARM_fall = 1648 DATATYPE_RULE (Thm.INST [state_with_enc ``Encoding_ARM``] DecodeARM) 1649end 1650 1651local 1652 val rand_uncurry = utilsLib.mk_cond_rand_thms [``UNCURRY f : 'a # 'b -> 'c``] 1653 val ConditionPassed_enc = Q.prove( 1654 `!s c. 1655 ConditionPassed () 1656 (s with <|CurrentCondition := c; Encoding := Encoding_ARM |>) = 1657 ConditionPassed () (s with CurrentCondition := c)`, 1658 lrw [ConditionPassed_rwt]) |> DATATYPE_RULE 1659 val v = fst (bitstringSyntax.dest_v2w (bitstringSyntax.mk_vec 28 0)) 1660 val dual_rwt = 1661 blastLib.BBLAST_PROVE 1662 ``v2w [b2; b1; b0; F] + 1w = v2w [b2; b1; b0; T] : word4`` 1663in 1664 fun DecodeARM_rwt thm pat = 1665 let 1666 val s = state_with_enc ``Encoding_ARM`` :: fst (Term.match_term v pat) 1667 in 1668 thm |> Thm.INST s 1669 |> REWRITE_RULE [dual_rwt, v2w_13_15_rwts, v2w_ground4, DecodeVFP] 1670 |> Conv.RIGHT_CONV_RULE EVAL_DATATYPE_CONV 1671 |> SIMP_RULE bool_ss 1672 [pairTheory.UNCURRY_DEF, rand_uncurry, ConditionPassed_enc] 1673 end 1674end 1675 1676(* -- *) 1677 1678fun epattern s = utilsLib.pattern (s ^ "____") 1679 1680val arm_patterns = List.map (I ## epattern) 1681 [("BranchExchange", "FFFTFFTF____________FFFT"), 1682 ("CountLeadingZeroes", "FFFTFTTF____________FFFT"), 1683 ("BranchLinkExchangeRegister", "FFFTFFTF____________FFTT"), 1684 ("SaturatingAddSubtract", "FFFTF__F____________FTFT"), 1685 ("Signed16Multiply32Accumulate", "FFFTFFFF____________T__F"), 1686 ("Signed16x32Multiply32Accumulate", "FFFTFFTF____________T_FF"), 1687 ("Signed16x32Multiply32Result", "FFFTFFTF____________T_TF"), 1688 ("Signed16Multiply64Accumulate", "FFFTFTFF____________T__F"), 1689 ("Signed16Multiply32Result", "FFFTFTTF____________T__F"), 1690 ("ExtendByte", "FTTFT_TF____________FTTT"), 1691 ("ExtendByte16", "FTTFT_FF__________FFFTTT"), 1692 ("ExtendHalfword", "FTTFT_TT__________FFFTTT"), 1693 ("SelectBytes", "FTTFTFFF________TTTTTFTT"), 1694 ("ByteReverse", "FTTFTFTTTTTT____TTTTFFTT"), 1695 ("ByteReversePackedHalfword", "FTTFTFTTTTTT____TTTTTFTT"), 1696 ("ByteReverseSignedHalfword", "FTTFTTTTTTTT____TTTTTFTT"), 1697 ("ReverseBits", "FTTFTTTTTTTT____TTTTFFTT"), 1698 ("BitFieldExtract", "FTTTT_T______________TFT"), 1699 ("BitFieldClearOrInsert", "FTTTTTF______________FFT"), 1700 ("Register", "FFFF___________________F"), 1701 ("Register ORR/BIC", "FFFTT_F________________F"), 1702 ("ShiftImmediate", "FFFTT_T________________F"), 1703 ("TestCompareRegister", "FFFTF__T_______________F"), 1704 ("RegisterShiftedRegister", "FFFF________________F__T"), 1705 ("RegisterShiftedRegister ORR/BIC", "FFFTT_F_____________F__T"), 1706 ("ShiftRegister", "FFFTT_T_____________F__T"), 1707 ("TestCompareRegisterShiftedRegister", "FFFTF__T____________F__T"), 1708 ("Multiply32", "FFFFFFF_____________TFFT"), 1709 ("MultiplyAccumulate", "FFFFFFT_____________TFFT"), 1710 ("MultiplyLong", "FFFFT_______________TFFT"), 1711 ("Swap", "FFFTF_FF________FFFFTFFT"), 1712 ("ArithLogicImmediate", "FFTF____________________"), 1713 ("ArithLogicImmediate ORR/BIC", "FFTTT_F_________________"), 1714 ("Move", "FFTTT_T_________________"), 1715 ("TestCompareImmediate", "FFTTF__T________________"), 1716 ("MoveHalfword", "FFTTF_FF________________"), 1717 ("BranchTarget", "TFTF____________________"), 1718 ("BranchLinkExchangeImmediate (to ARM)", "TFTT____________________"), 1719 ("LoadUnprivileged (imm)", "FTFF_FTT________________"), 1720 ("LoadWord (imm,post)", "FTFF_FFT________________"), 1721 ("LoadWord (imm,pre;lit)", "FTFT_F_T________________"), 1722 ("LoadByteUnprivileged (imm)", "FTFF_TTT________________"), 1723 ("LoadByte (imm,post)", "FTFF_TFT________________"), 1724 ("LoadByte (imm,pre;lit)", "FTFT_T_T________________"), 1725 ("LoadUnprivileged (reg)", "FTTF_FTT_______________F"), 1726 ("LoadWord (reg,post)", "FTTF_FFT_______________F"), 1727 ("LoadWord (reg,pre)", "FTTT_F_T_______________F"), 1728 ("LoadByteUnprivileged (reg)", "FTTF_TTT_______________F"), 1729 ("LoadByte (reg,post)", "FTTF_TFT_______________F"), 1730 ("LoadByte (reg,pre)", "FTTT_T_T_______________F"), 1731 ("LoadHalfUnprivileged (reg)", "FFFF_FTT________FFFFT_TT"), 1732 ("LoadSignedByteUnprivileged (reg)", "FFFF_FTT________FFFFTTFT"), 1733 ("LoadHalf (reg,post)", "FFFF_FFT________FFFFT_TT"), 1734 ("LoadSignedByte (reg,post)", "FFFF_FFT________FFFFTTFT"), 1735 ("LoadHalf (reg,pre)", "FFFT_F_T________FFFFT_TT"), 1736 ("LoadSignedByte (reg,pre)", "FFFT_F_T________FFFFTTFT"), 1737 ("LoadHalfUnprivileged (imm)", "FFFF_TTT____________T_TT"), 1738 ("LoadSignedByteUnprivileged (imm)", "FFFF_TTT____________TTFT"), 1739 ("LoadHalf (imm,post)", "FFFF_TFT____________T_TT"), 1740 ("LoadSignedByte (imm,post)", "FFFF_TFT____________TTFT"), 1741 ("LoadHalf (imm,pre;lit)", "FFFT_T_T____________T_TT"), 1742 ("LoadSignedByte (imm,pre;lit)", "FFFT_T_T____________TTFT"), 1743 ("LoadDual (reg)", "FFF__F_F_______FFFFFTTFT"), 1744 ("LoadDual (imm;lit)", "FFF__T_F_______F____TTFT"), 1745 ("LoadMultiple", "TFF__F_T________________"), 1746 ("StoreUnprivileged (imm)", "FTFF_FTF________________"), 1747 ("StoreWord (imm,post)", "FTFF_FFF________________"), 1748 ("StoreWord (imm,pre)", "FTFT_F_F________________"), 1749 ("StoreByteUnprivileged (imm)", "FTFF_TTF________________"), 1750 ("StoreByte (imm,post)", "FTFF_TFF________________"), 1751 ("StoreByte (imm,pre)", "FTFT_T_F________________"), 1752 ("StoreUnprivileged (reg)", "FTTF_FTF_______________F"), 1753 ("StoreWord (reg,post)", "FTTF_FFF_______________F"), 1754 ("StoreWord (reg,pre)", "FTTT_F_F_______________F"), 1755 ("StoreByteUnprivileged (reg)", "FTTF_TTF_______________F"), 1756 ("StoreByte (reg,post)", "FTTF_TFF_______________F"), 1757 ("StoreByte (reg,pre)", "FTTT_T_F_______________F"), 1758 ("StoreHalfUnprivileged (reg)", "FFFF_FTF________FFFFTFTT"), 1759 ("StoreHalf (reg,post)", "FFFF_FFF________FFFFTFTT"), 1760 ("StoreHalf (reg,pre)", "FFFT_F_F________FFFFTFTT"), 1761 ("StoreHalfUnprivileged (imm)", "FFFF_TTF____________TFTT"), 1762 ("StoreSignedByteUnprivileged (imm)", "FFFF_TTF____________TTFT"), 1763 ("StoreHalf (imm,post)", "FFFF_TFF____________TFTT"), 1764 ("StoreHalf (imm,pre)", "FFFT_T_F____________TFTT"), 1765 ("StoreDual (reg)", "FFF__F_F_______FFFFFTTTT"), 1766 ("StoreDual (imm)", "FFF__T_F_______F____TTTT"), 1767 ("StoreMultiple", "TFF__F_F________________"), 1768 ("VFPLoadStore", "TTFT__F_________TFT_____"), 1769 ("VFPData", "TTTF____________TFT____F"), 1770 ("VFPTransfer", "TTTF____________TFTF___T"), 1771 ("VFPTransfer2", "TTFFFTF_________TFT_FF_T"), 1772 ("MoveToRegisterFromSpecial", "FFFTFFFF__________F_FFFF"), 1773 ("MoveToSpecialFromRegister", "FFFTFFTF__________F_FFFF"), 1774 ("MoveToSpecialFromImmediate", "FFTTFFTF________________"), 1775 ("Hint", "FFTTFFTFFFFFTTTTFFFF____") 1776 ] 1777 1778val arm_patterns15 = List.map (I ## epattern) 1779 [("Setend", "FFFTFFFF___T________FFFF"), 1780 ("ChangeProcessorState", "FFFTFFFF___F__________F_"), 1781 ("DataMemoryBarrier", "FTFTFTTTTTTTTTTTFFFFFTFT"), 1782 ("ReturnFromException", "TFF__F_T________________"), 1783 ("BranchLinkExchangeImmediate (to Thumb)", "TFT_____________________") 1784 ] 1785 1786(* -- *) 1787 1788datatype condition = Cond15 | Cond14 | Cond of (term, term) subst 1789 1790local 1791 val mk_bit = bitstringSyntax.mk_bit 1792 fun mk_condition l = 1793 let 1794 val cond = Lib.with_exn (List.map bitstringSyntax.dest_b) l 1795 (ERR "mk_condition" "condition code not specified") 1796 in 1797 case cond of 1798 [b31, b30, b29, b28] => 1799 if b31 andalso b30 andalso b29 1800 then if b28 then Cond15 else Cond14 1801 else Cond [mk_bit 31 |-> List.nth (l, 0), 1802 mk_bit 30 |-> List.nth (l, 1), 1803 mk_bit 29 |-> List.nth (l, 2), 1804 mk_bit 28 |-> List.nth (l, 3)] 1805 | _ => raise ERR "mk_condition" "expecting 4 element list" 1806 end 1807 val w32 = fcpSyntax.mk_int_numeric_type 32 1808 fun pad32_opcode v = 1809 let 1810 val (l, ty) = listSyntax.dest_list v 1811 val () = ignore (ty = Type.bool andalso List.length l <= 32 1812 orelse raise ERR "mk_opcode" "bad Bool list") 1813 in 1814 utilsLib.padLeft boolSyntax.F 32 l 1815 end 1816in 1817 val hex_to_bits_32 = pad32_opcode o bitstringSyntax.bitstring_of_hexstring 1818 fun mk_opcode v = 1819 let 1820 val opc = pad32_opcode v 1821 in 1822 (mk_condition (List.take (opc, 4)), 1823 bitstringSyntax.mk_v2w (listSyntax.mk_list (opc, Type.bool), w32)) 1824 end 1825 fun mk_pattern_opcode c p = 1826 listSyntax.mk_list 1827 (fst (listSyntax.dest_list (utilsLib.pattern c)) @ 1828 fst (listSyntax.dest_list p), Type.bool) 1829end 1830 1831local 1832 val arm_pats = Redblackmap.fromList String.compare arm_patterns 1833 val arm_pats15 = Redblackmap.fromList String.compare arm_patterns15 1834 val alias = 1835 fn "LoadByte (imm,pre)" => ("LoadByte (imm,pre;lit)", [true, false]) 1836 | "LoadWord (imm,pre)" => ("LoadWord (imm,pre;lit)", [true, false]) 1837 | "LoadDual (imm)" => ("LoadDual (imm;lit)", [true, false]) 1838 | "LoadByte (lit)" => ("LoadByte (imm,pre;lit)", [false, true]) 1839 | "LoadSignedByte (lit)" => ("LoadSignedByte (imm,pre;lit)", [true]) 1840 | "LoadHalf (lit)" => ("LoadHalf (imm,pre;lit)", [true]) 1841 | "LoadWord (lit)" => ("LoadWord (imm,pre;lit)", [false, true]) 1842 | "LoadDual (lit)" => ("LoadDual (imm;lit)", [false, true]) 1843 | "LoadSignedByte (imm,pre;nowb)" => 1844 ("LoadSignedByte (imm,pre;lit)", [true, false]) 1845 | "LoadHalf (imm,pre;nowb)" => ("LoadHalf (imm,pre;lit)", [true, false]) 1846 | s as "SpecialFromImmediate" => 1847 ("MoveTo" ^ s, 1848 [true, false, false, false, false, false, false, false]) 1849 | s => (s, [true]) 1850 val c14 = utilsLib.pattern "TTTF" 1851 val c15 = utilsLib.pattern "TTTT" 1852 fun unconditional c = 1853 let 1854 val cond = Term.term_eq (utilsLib.pattern c) 1855 in 1856 cond c14 orelse cond c15 1857 end 1858 fun doubleup l = List.concat (List.map (fn x => [x, x]) l) 1859in 1860 (* 1861 fun raw_pattern_opcode s = 1862 ([]: bool list, mk_pattern_opcode "TTTF" (Redblackmap.find (arm_pats, s))) 1863 *) 1864 fun mk_arm_pattern_opcode c s = 1865 let 1866 val (a, x) = alias s 1867 val v = case Redblackmap.peek (arm_pats, a) of 1868 SOME p => mk_pattern_opcode c p 1869 | NONE => 1870 (case Redblackmap.peek (arm_pats15, a) of 1871 SOME p => mk_pattern_opcode "TTTT" p 1872 | NONE => raise ERR "mk_arm_pattern_opcode" 1873 (a ^ "; not found")) 1874 in 1875 (if unconditional c then x 1876 else if s = "LoadWord (imm,post)" then 1877 [true, true, false] 1878 else doubleup x, v) 1879 end 1880end 1881 1882local 1883 val sep1 = String.tokens (Lib.equal #",") 1884 val sep2 = String.tokens (fn c => c = #"-" orelse Char.isSpace c) 1885 fun err s = raise ERR "index" ("bad index: " ^ s) 1886 fun index s = case Int.fromString s of 1887 SOME i => (i < 16 orelse err s; i) 1888 | NONE => err s 1889 fun reg_array s = 1890 let 1891 val a = Array.array (16, boolSyntax.F) 1892 fun set i = Array.update (a, i, boolSyntax.T) 1893 in 1894 List.app 1895 (fn r => case sep2 r of 1896 [i] => set (index i) 1897 | [i, j] => 1898 let 1899 val x = index i 1900 val y = index j 1901 in 1902 Lib.for_se (Int.min (x, y)) (Int.max (x, y)) set 1903 end 1904 | _ => raise ERR "reg_array" "syntax error") (sep1 s) 1905 ; a 1906 end 1907in 1908 fun reg_list_subst s = 1909 let 1910 val a = reg_array s 1911 in 1912 List.tabulate 1913 (16, fn i => Term.mk_var ("x" ^ Int.toString (i + 7), Type.bool) |-> 1914 Array.sub (a, 15 - i)) 1915 end 1916end 1917 1918local 1919 val prefix = fst o splitAtSpace 1920 fun x i = Term.mk_var ("x" ^ Int.toString i, Type.bool) 1921 fun xF i = x i |-> boolSyntax.F 1922 fun xT i = x i |-> boolSyntax.T 1923 val ast = Redblackmap.fromList String.compare 1924 [("B", ("BranchTarget", [])), 1925 ("BX", ("BranchExchange", [])), 1926 ("BX (pc)", ("BranchExchange", [xT 12, xT 13, xT 14, xT 15])), 1927 ("BL", ("BranchLinkExchangeImmediate (to ARM)", [])), 1928 ("BLX (imm)", ("BranchLinkExchangeImmediate (to Thumb)", [])), 1929 ("BLX (reg)", ("BranchLinkExchangeRegister", [])), 1930 ("CLZ", ("CountLeadingZeroes", [])), 1931 ("DMB", ("DataMemoryBarrier", [])), 1932 ("MOVT", ("MoveHalfword", [xT 0])), 1933 ("MOVW", ("MoveHalfword", [xF 0])), 1934 ("MOV (imm)", ("Move", [xF 0, xF 1])), 1935 ("MVN (imm)", ("Move", [xT 0, xF 1])), 1936 ("MOVS (imm)",("Move", [xF 0, xT 1])), 1937 ("MVNS (imm)",("Move", [xT 0, xT 1])), 1938 ("AND (imm)", ("ArithLogicImmediate", [xF 0, xF 1, xF 2, xF 3])), 1939 ("EOR (imm)", ("ArithLogicImmediate", [xF 0, xF 1, xT 2, xF 3])), 1940 ("SUB (imm)", ("ArithLogicImmediate", [xF 0, xT 1, xF 2, xF 3])), 1941 ("RSB (imm)", ("ArithLogicImmediate", [xF 0, xT 1, xT 2, xF 3])), 1942 ("ADD (imm)", ("ArithLogicImmediate", [xT 0, xF 1, xF 2, xF 3])), 1943 ("ADC (imm)", ("ArithLogicImmediate", [xT 0, xF 1, xT 2, xF 3])), 1944 ("SBC (imm)", ("ArithLogicImmediate", [xT 0, xT 1, xF 2, xF 3])), 1945 ("RSC (imm)", ("ArithLogicImmediate", [xT 0, xT 1, xT 2, xF 3])), 1946 ("ANDS (imm)",("ArithLogicImmediate", [xF 0, xF 1, xF 2, xT 3])), 1947 ("EORS (imm)",("ArithLogicImmediate", [xF 0, xF 1, xT 2, xT 3])), 1948 ("SUBS (imm)",("ArithLogicImmediate", [xF 0, xT 1, xF 2, xT 3])), 1949 ("SUBS (pc,imm)",("ArithLogicImmediate", 1950 [xF 0, xT 1, xF 2, xT 3, xT 8, xT 9, xT 10, xT 11])), 1951 ("RSBS (imm)",("ArithLogicImmediate", [xF 0, xT 1, xT 2, xT 3])), 1952 ("ADDS (imm)",("ArithLogicImmediate", [xT 0, xF 1, xF 2, xT 3])), 1953 ("ADCS (imm)",("ArithLogicImmediate", [xT 0, xF 1, xT 2, xT 3])), 1954 ("SBCS (imm)",("ArithLogicImmediate", [xT 0, xT 1, xF 2, xT 3])), 1955 ("RSCS (imm)",("ArithLogicImmediate", [xT 0, xT 1, xT 2, xT 3])), 1956 ("ORR (imm)", ("ArithLogicImmediate ORR/BIC", [xF 0, xF 1])), 1957 ("BIC (imm)", ("ArithLogicImmediate ORR/BIC", [xT 0, xF 1])), 1958 ("ORRS (imm)",("ArithLogicImmediate ORR/BIC", [xF 0, xT 1])), 1959 ("BICS (imm)",("ArithLogicImmediate ORR/BIC", [xT 0, xT 1])), 1960 ("TST (imm)", ("TestCompareImmediate", [xF 0, xF 1])), 1961 ("TEQ (imm)", ("TestCompareImmediate", [xF 0, xT 1])), 1962 ("CMP (imm)", ("TestCompareImmediate", [xT 0, xF 1])), 1963 ("CMN (imm)", ("TestCompareImmediate", [xT 0, xT 1])), 1964 ("MOV (reg)", ("ShiftImmediate", [xF 0, xF 1])), 1965 ("MVN (reg)", ("ShiftImmediate", [xT 0, xF 1])), 1966 ("MOVS (reg)",("ShiftImmediate", [xF 0, xT 1])), 1967 ("MVNS (reg)",("ShiftImmediate", [xT 0, xT 1])), 1968 ("AND (reg)", ("Register", [xF 0, xF 1, xF 2, xF 3])), 1969 ("EOR (reg)", ("Register", [xF 0, xF 1, xT 2, xF 3])), 1970 ("SUB (reg)", ("Register", [xF 0, xT 1, xF 2, xF 3])), 1971 ("RSB (reg)", ("Register", [xF 0, xT 1, xT 2, xF 3])), 1972 ("ADD (reg)", ("Register", [xT 0, xF 1, xF 2, xF 3])), 1973 ("ADC (reg)", ("Register", [xT 0, xF 1, xT 2, xF 3])), 1974 ("SBC (reg)", ("Register", [xT 0, xT 1, xF 2, xF 3])), 1975 ("RSC (reg)", ("Register", [xT 0, xT 1, xT 2, xF 3])), 1976 ("ANDS (reg)",("Register", [xF 0, xF 1, xF 2, xT 3])), 1977 ("EORS (reg)",("Register", [xF 0, xF 1, xT 2, xT 3])), 1978 ("SUBS (reg)",("Register", [xF 0, xT 1, xF 2, xT 3])), 1979 ("RSBS (reg)",("Register", [xF 0, xT 1, xT 2, xT 3])), 1980 ("ADDS (reg)",("Register", [xT 0, xF 1, xF 2, xT 3])), 1981 ("ADCS (reg)",("Register", [xT 0, xF 1, xT 2, xT 3])), 1982 ("SBCS (reg)",("Register", [xT 0, xT 1, xF 2, xT 3])), 1983 ("RSCS (reg)",("Register", [xT 0, xT 1, xT 2, xT 3])), 1984 ("ORR (reg)", ("Register ORR/BIC", [xF 0, xF 1])), 1985 ("BIC (reg)", ("Register ORR/BIC", [xT 0, xF 1])), 1986 ("ORRS (reg)",("Register ORR/BIC", [xF 0, xT 1])), 1987 ("BICS (reg)",("Register ORR/BIC", [xT 0, xT 1])), 1988 ("TST (reg)", ("TestCompareRegister", [xF 0, xF 1])), 1989 ("TEQ (reg)", ("TestCompareRegister", [xF 0, xT 1])), 1990 ("CMP (reg)", ("TestCompareRegister", [xT 0, xF 1])), 1991 ("CMN (reg)", ("TestCompareRegister", [xT 0, xT 1])), 1992 ("MOV (reg-shift)", ("ShiftRegister", [xF 0, xF 1])), 1993 ("MVN (reg-shift)", ("ShiftRegister", [xT 0, xF 1])), 1994 ("MOVS (reg-shift)",("ShiftRegister", [xF 0, xT 1])), 1995 ("MVNS (reg-shift)",("ShiftRegister", [xT 0, xT 1])), 1996 ("AND (reg-shift)", ("RegisterShiftedRegister", [xF 0, xF 1, xF 2, xF 3])), 1997 ("EOR (reg-shift)", ("RegisterShiftedRegister", [xF 0, xF 1, xT 2, xF 3])), 1998 ("SUB (reg-shift)", ("RegisterShiftedRegister", [xF 0, xT 1, xF 2, xF 3])), 1999 ("RSB (reg-shift)", ("RegisterShiftedRegister", [xF 0, xT 1, xT 2, xF 3])), 2000 ("ADD (reg-shift)", ("RegisterShiftedRegister", [xT 0, xF 1, xF 2, xF 3])), 2001 ("ADC (reg-shift)", ("RegisterShiftedRegister", [xT 0, xF 1, xT 2, xF 3])), 2002 ("SBC (reg-shift)", ("RegisterShiftedRegister", [xT 0, xT 1, xF 2, xF 3])), 2003 ("RSC (reg-shift)", ("RegisterShiftedRegister", [xT 0, xT 1, xT 2, xF 3])), 2004 ("ANDS (reg-shift)",("RegisterShiftedRegister", [xF 0, xF 1, xF 2, xT 3])), 2005 ("EORS (reg-shift)",("RegisterShiftedRegister", [xF 0, xF 1, xT 2, xT 3])), 2006 ("SUBS (reg-shift)",("RegisterShiftedRegister", [xF 0, xT 1, xF 2, xT 3])), 2007 ("RSBS (reg-shift)",("RegisterShiftedRegister", [xF 0, xT 1, xT 2, xT 3])), 2008 ("ADDS (reg-shift)",("RegisterShiftedRegister", [xT 0, xF 1, xF 2, xT 3])), 2009 ("ADCS (reg-shift)",("RegisterShiftedRegister", [xT 0, xF 1, xT 2, xT 3])), 2010 ("SBCS (reg-shift)",("RegisterShiftedRegister", [xT 0, xT 1, xF 2, xT 3])), 2011 ("RSCS (reg-shift)",("RegisterShiftedRegister", [xT 0, xT 1, xT 2, xT 3])), 2012 ("ORR (reg-shift)", ("RegisterShiftedRegister ORR/BIC", [xF 0, xF 1])), 2013 ("BIC (reg-shift)", ("RegisterShiftedRegister ORR/BIC", [xT 0, xF 1])), 2014 ("ORRS (reg-shift)",("RegisterShiftedRegister ORR/BIC", [xF 0, xT 1])), 2015 ("BICS (reg-shift)",("RegisterShiftedRegister ORR/BIC", [xT 0, xT 1])), 2016 ("TST (reg-shift)", ("TestCompareRegisterShiftedRegister", [xF 0, xF 1])), 2017 ("TEQ (reg-shift)", ("TestCompareRegisterShiftedRegister", [xF 0, xT 1])), 2018 ("CMP (reg-shift)", ("TestCompareRegisterShiftedRegister", [xT 0, xF 1])), 2019 ("CMN (reg-shift)", ("TestCompareRegisterShiftedRegister", [xT 0, xT 1])), 2020 ("MUL", ("Multiply32", [xF 0])), 2021 ("MLA", ("MultiplyAccumulate", [xF 0])), 2022 ("UMULL", ("MultiplyLong", [xF 0, xF 1, xF 2])), 2023 ("SMULL", ("MultiplyLong", [xT 0, xF 1, xF 2])), 2024 ("UMLAL", ("MultiplyLong", [xF 0, xT 1, xF 2])), 2025 ("SMLAL", ("MultiplyLong", [xT 0, xT 1, xF 2])), 2026 ("UMULLS", ("MultiplyLong", [xF 0, xF 1, xT 2])), 2027 ("SMULLS", ("MultiplyLong", [xT 0, xF 1, xT 2])), 2028 ("UMLALS", ("MultiplyLong", [xF 0, xT 1, xT 2])), 2029 ("SMLALS", ("MultiplyLong", [xT 0, xT 1, xT 2])), 2030 ("MULS", ("Multiply32", [xT 0])), 2031 ("MLAS", ("MultiplyAccumulate", [xT 0])), 2032 ("SMLA<XY>", ("Signed16Multiply32Accumulate", [])), 2033 ("SXT{A}B,UXT{A}B", ("ExtendByte", [])), 2034 ("SXT{A}B16,UXT{A}B16", ("ExtendByte16", [])), 2035 ("SXT{A}H,UXT{A}H", ("ExtendHalfword", [])), 2036 ("SEL", ("SelectBytes", [])), 2037 ("REV", ("ByteReverse", [])), 2038 ("REV16", ("ByteReversePackedHalfword", [])), 2039 ("REVSH", ("ByteReverseSignedHalfword", [])), 2040 ("RBIT", ("ReverseBits", [])), 2041 ("SBFX,UBFX", ("BitFieldExtract", [])), 2042 ("BFC", ("BitFieldClearOrInsert", [])), 2043 ("LDR (+imm,pre,wb)", ("LoadWord (imm,pre;lit)", [xT 0, xT 1])), 2044 ("LDR (-imm,pre,wb)", ("LoadWord (imm,pre;lit)", [xF 0, xT 1])), 2045 ("LDR (+imm,pre)", ("LoadWord (imm,pre)", [xT 0, xF 1])), 2046 ("LDR (-imm,pre)", ("LoadWord (imm,pre)", [xF 0, xF 1])), 2047 ("LDR (imm,post)", ("LoadWord (imm,post)", [])), 2048 ("LDR (+lit)", 2049 ("LoadWord (imm,pre;lit)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2050 ("LDR (-lit)", 2051 ("LoadWord (imm,pre;lit)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2052 ("LDR (+reg,pre,wb)", ("LoadWord (reg,pre)", [xT 0, xT 1])), 2053 ("LDR (-reg,pre,wb)", ("LoadWord (reg,pre)", [xF 0, xT 1])), 2054 ("LDR (+reg,pre)", ("LoadWord (reg,pre)", [xT 0, xF 1])), 2055 ("LDR (-reg,pre)", ("LoadWord (reg,pre)", [xF 0, xF 1])), 2056 ("LDR (+reg,pre,pc)", 2057 ("LoadWord (reg,pre)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2058 ("LDR (-reg,pre,pc)", 2059 ("LoadWord (reg,pre)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2060 ("LDR (reg,post)", ("LoadWord (reg,post)", [])), 2061 ("LDR (pc,+imm,pre,wb)", 2062 ("LoadWord (imm,pre;lit)", [xT 0, xT 1, xT 6, xT 7, xT 8, xT 9])), 2063 ("LDR (pc,-imm,pre,wb)", 2064 ("LoadWord (imm,pre;lit)", [xF 0, xT 1, xT 6, xT 7, xT 8, xT 9])), 2065 ("LDR (pc,+imm,pre)", 2066 ("LoadWord (imm,pre)", [xT 0, xF 1, xT 6, xT 7, xT 8, xT 9])), 2067 ("LDR (pc,-imm,pre)", 2068 ("LoadWord (imm,pre)", [xF 0, xF 1, xT 6, xT 7, xT 8, xT 9])), 2069 ("LDR (pc,imm,post)", 2070 ("LoadWord (imm,post)", [xT 5, xT 6, xT 7, xT 8])), 2071 ("LDR (pc,+reg,pre,wb)", 2072 ("LoadWord (reg,pre)", [xT 0, xT 1, xT 6, xT 7, xT 8, xT 9])), 2073 ("LDR (pc,-reg,pre,wb)", 2074 ("LoadWord (reg,pre)", [xF 0, xT 1, xT 6, xT 7, xT 8, xT 9])), 2075 ("LDR (pc,+reg,pre)", 2076 ("LoadWord (reg,pre)", [xT 0, xF 1, xT 6, xT 7, xT 8, xT 9])), 2077 ("LDR (pc,-reg,pre)", 2078 ("LoadWord (reg,pre)", [xF 0, xF 1, xT 6, xT 7, xT 8, xT 9])), 2079 ("LDR (pc,+reg,pre,pc)", 2080 ("LoadWord (reg,pre)", 2081 [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5, xT 6, xT 7, xT 8, xT 9])), 2082 ("LDR (pc,-reg,pre,pc)", 2083 ("LoadWord (reg,pre)", 2084 [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5, xT 6, xT 7, xT 8, xT 9])), 2085 ("LDR (pc,reg,post)", ("LoadWord (reg,post)", [])), 2086 ("LDRB (+imm,pre,wb)", ("LoadByte (imm,pre;lit)", [xT 0, xT 1])), 2087 ("LDRB (-imm,pre,wb)", ("LoadByte (imm,pre;lit)", [xF 0, xT 1])), 2088 ("LDRB (+imm,pre)", ("LoadByte (imm,pre)", [xT 0, xF 1])), 2089 ("LDRB (-imm,pre)", ("LoadByte (imm,pre)", [xF 0, xF 1])), 2090 ("LDRB (imm,post)", ("LoadByte (imm,post)", [])), 2091 ("LDRB (+lit)", 2092 ("LoadByte (imm,pre;lit)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2093 ("LDRB (-lit)", 2094 ("LoadByte (imm,pre;lit)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2095 ("LDRB (+reg,pre,wb)", ("LoadByte (reg,pre)", [xT 0, xT 1])), 2096 ("LDRB (-reg,pre,wb)", ("LoadByte (reg,pre)", [xF 0, xT 1])), 2097 ("LDRB (+reg,pre)", ("LoadByte (reg,pre)", [xT 0, xF 1])), 2098 ("LDRB (-reg,pre)", ("LoadByte (reg,pre)", [xF 0, xF 1])), 2099 ("LDRB (+reg,pre,pc)", 2100 ("LoadByte (reg,pre)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2101 ("LDRB (-reg,pre,pc)", 2102 ("LoadByte (reg,pre)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2103 ("LDRB (reg,post)", ("LoadByte (reg,post)", [])), 2104 ("LDRSB (+imm,pre,wb)", ("LoadSignedByte (imm,pre;lit)", [xT 0, xT 1])), 2105 ("LDRSB (-imm,pre,wb)", ("LoadSignedByte (imm,pre;lit)", [xF 0, xT 1])), 2106 ("LDRSB (+imm,pre)", ("LoadSignedByte (imm,pre;nowb)", [xT 0, xF 1])), 2107 ("LDRSB (-imm,pre)", ("LoadSignedByte (imm,pre;nowb)", [xF 0, xF 1])), 2108 ("LDRSB (imm,post)", ("LoadSignedByte (imm,post)", [])), 2109 ("LDRSB (+lit)", 2110 ("LoadSignedByte (lit)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2111 ("LDRSB (-lit)", 2112 ("LoadSignedByte (lit)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2113 ("LDRSB (+reg,pre,wb)", ("LoadSignedByte (reg,pre)", [xT 0, xT 1])), 2114 ("LDRSB (-reg,pre,wb)", ("LoadSignedByte (reg,pre)", [xF 0, xT 1])), 2115 ("LDRSB (+reg,pre)", ("LoadSignedByte (reg,pre)", [xT 0, xF 1])), 2116 ("LDRSB (-reg,pre)", ("LoadSignedByte (reg,pre)", [xF 0, xF 1])), 2117 ("LDRSB (+reg,pre,pc)", 2118 ("LoadSignedByte (reg,pre)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2119 ("LDRSB (-reg,pre,pc)", 2120 ("LoadSignedByte (reg,pre)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2121 ("LDRSB (reg,post)", ("LoadSignedByte (reg,post)", [])), 2122 ("LDRBT (+imm)", ("LoadByteUnprivileged (imm)", [xT 0])), 2123 ("LDRBT (-imm)", ("LoadByteUnprivileged (imm)", [xF 0])), 2124 ("LDRBT (+reg)", ("LoadByteUnprivileged (reg)", [xT 0])), 2125 ("LDRBT (-reg)", ("LoadByteUnprivileged (reg)", [xF 0])), 2126 ("LDRH (+imm,pre,wb)", ("LoadHalf (imm,pre;lit)", [xT 0, xT 1, xF 13])), 2127 ("LDRH (-imm,pre,wb)", ("LoadHalf (imm,pre;lit)", [xF 0, xT 1, xF 13])), 2128 ("LDRH (+imm,pre)", ("LoadHalf (imm,pre;nowb)", [xT 0, xF 1, xF 13])), 2129 ("LDRH (-imm,pre)", ("LoadHalf (imm,pre;nowb)", [xF 0, xF 1, xF 13])), 2130 ("LDRH (imm,post)", ("LoadHalf (imm,post)", [xF 13])), 2131 ("LDRH (+lit)", 2132 ("LoadHalf (lit)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5, xF 14])), 2133 ("LDRH (-lit)", 2134 ("LoadHalf (lit)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5, xF 14])), 2135 ("LDRH (+reg,pre,wb)", ("LoadHalf (reg,pre)", [xT 0, xT 1, xF 13])), 2136 ("LDRH (-reg,pre,wb)", ("LoadHalf (reg,pre)", [xF 0, xT 1, xF 13])), 2137 ("LDRH (+reg,pre)", ("LoadHalf (reg,pre)", [xT 0, xF 1, xF 13])), 2138 ("LDRH (-reg,pre)", ("LoadHalf (reg,pre)", [xF 0, xF 1, xF 13])), 2139 ("LDRH (+reg,pre,pc)", 2140 ("LoadHalf (reg,pre)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5, xF 10])), 2141 ("LDRH (-reg,pre,pc)", 2142 ("LoadHalf (reg,pre)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5, xF 10])), 2143 ("LDRH (reg,post)", ("LoadHalf (reg,post)", [xF 13])), 2144 ("LDRSH (+imm,pre,wb)", ("LoadHalf (imm,pre;lit)", [xT 0, xT 1, xT 13])), 2145 ("LDRSH (-imm,pre,wb)", ("LoadHalf (imm,pre;lit)", [xF 0, xT 1, xT 13])), 2146 ("LDRSH (+imm,pre)", ("LoadHalf (imm,pre;nowb)", [xT 0, xF 1, xT 13])), 2147 ("LDRSH (-imm,pre)", ("LoadHalf (imm,pre;nowb)", [xF 0, xF 1, xT 13])), 2148 ("LDRSH (imm,post)", ("LoadHalf (imm,post)", [xT 13])), 2149 ("LDRSH (+lit)", 2150 ("LoadHalf (lit)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5, xT 14])), 2151 ("LDRSH (-lit)", 2152 ("LoadHalf (lit)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5, xT 14])), 2153 ("LDRSH (+reg,pre,wb)", ("LoadHalf (reg,pre)", [xT 0, xT 1, xT 10])), 2154 ("LDRSH (-reg,pre,wb)", ("LoadHalf (reg,pre)", [xF 0, xT 1, xT 10])), 2155 ("LDRSH (+reg,pre)", ("LoadHalf (reg,pre)", [xT 0, xF 1, xT 10])), 2156 ("LDRSH (-reg,pre)", ("LoadHalf (reg,pre)", [xF 0, xF 1, xT 10])), 2157 ("LDRSH (+reg,pre,pc)", 2158 ("LoadHalf (reg,pre)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5, xT 10])), 2159 ("LDRSH (-reg,pre,pc)", 2160 ("LoadHalf (reg,pre)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5, xT 10])), 2161 ("LDRSH (reg,post)", ("LoadHalf (reg,post)", [xT 13])), 2162 ("LDRD (+imm,pre,wb)", ("LoadDual (imm;lit)", [xT 0, xT 1, xT 2])), 2163 ("LDRD (-imm,pre,wb)", ("LoadDual (imm;lit)", [xT 0, xF 1, xT 2])), 2164 ("LDRD (+imm,pre)", ("LoadDual (imm)", [xT 0, xT 1, xF 2])), 2165 ("LDRD (-imm,pre)", ("LoadDual (imm)", [xT 0, xF 1, xF 2])), 2166 ("LDRD (imm,post)", ("LoadDual (imm;lit)", [xF 0, xF 2])), 2167 ("LDRD (+lit)", 2168 ("LoadDual (imm;lit)", [xT 0, xT 1, xF 2, xT 3, xT 4, xT 5, xT 6])), 2169 ("LDRD (-lit)", 2170 ("LoadDual (imm;lit)", [xT 0, xF 1, xF 2, xT 3, xT 4, xT 5, xT 6])), 2171 ("LDRD (+reg,pre,wb)", ("LoadDual (reg)", [xT 0, xT 1, xT 2])), 2172 ("LDRD (-reg,pre,wb)", ("LoadDual (reg)", [xT 0, xF 1, xT 2])), 2173 ("LDRD (+reg,pre)", ("LoadDual (reg)", [xT 0, xT 1, xF 2])), 2174 ("LDRD (-reg,pre)", ("LoadDual (reg)", [xT 0, xF 1, xF 2])), 2175 ("LDRD (+reg,pre,pc)", 2176 ("LoadDual (reg)", [xT 0, xT 1, xF 2, xT 3, xT 4, xT 5, xT 6])), 2177 ("LDRD (-reg,pre,pc)", 2178 ("LoadDual (reg)", [xT 0, xF 1, xF 2, xT 3, xT 4, xT 5, xT 6])), 2179 ("LDRD (reg,post)", ("LoadDual (reg)", [xF 0, xF 2])), 2180 ("STR (+imm,pre,wb)", ("StoreWord (imm,pre)", [xT 0, xT 1])), 2181 ("STR (-imm,pre,wb)", ("StoreWord (imm,pre)", [xF 0, xT 1])), 2182 ("STR (+imm,pre)", ("StoreWord (imm,pre)", [xT 0, xF 1])), 2183 ("STR (-imm,pre)", ("StoreWord (imm,pre)", [xF 0, xF 1])), 2184 ("STR (+imm,pre,pc)", 2185 ("StoreWord (imm,pre)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2186 ("STR (-imm,pre,pc)", 2187 ("StoreWord (imm,pre)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2188 ("STR (imm,post)", ("StoreWord (imm,post)", [])), 2189 ("STR (+reg,pre,wb)", ("StoreWord (reg,pre)", [xT 0, xT 1])), 2190 ("STR (-reg,pre,wb)", ("StoreWord (reg,pre)", [xF 0, xT 1])), 2191 ("STR (+reg,pre)", ("StoreWord (reg,pre)", [xT 0, xF 1])), 2192 ("STR (-reg,pre)", ("StoreWord (reg,pre)", [xF 0, xF 1])), 2193 ("STR (+reg,pre,pc)", 2194 ("StoreWord (reg,pre)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2195 ("STR (-reg,pre,pc)", 2196 ("StoreWord (reg,pre)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2197 ("STR (reg,post)", ("StoreWord (reg,post)", [])), 2198 ("STRB (+imm,pre,wb)", ("StoreByte (imm,pre)", [xT 0, xT 1])), 2199 ("STRB (-imm,pre,wb)", ("StoreByte (imm,pre)", [xF 0, xT 1])), 2200 ("STRB (+imm,pre)", ("StoreByte (imm,pre)", [xT 0, xF 1])), 2201 ("STRB (-imm,pre)", ("StoreByte (imm,pre)", [xF 0, xF 1])), 2202 ("STRB (+imm,pre,pc)", 2203 ("StoreByte (imm,pre)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2204 ("STRB (-imm,pre,pc)", 2205 ("StoreByte (imm,pre)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2206 ("STRB (imm,post)", ("StoreByte (imm,post)", [])), 2207 ("STRB (+reg,pre,wb)", ("StoreByte (reg,pre)", [xT 0, xT 1])), 2208 ("STRB (-reg,pre,wb)", ("StoreByte (reg,pre)", [xF 0, xT 1])), 2209 ("STRB (+reg,pre)", ("StoreByte (reg,pre)", [xT 0, xF 1])), 2210 ("STRB (-reg,pre)", ("StoreByte (reg,pre)", [xF 0, xF 1])), 2211 ("STRB (+reg,pre,pc)", 2212 ("StoreByte (reg,pre)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2213 ("STRB (-reg,pre,pc)", 2214 ("StoreByte (reg,pre)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2215 ("STRB (reg,post)", ("StoreByte (reg,post)", [])), 2216 ("STRH (+imm,pre,wb)", ("StoreHalf (imm,pre)", [xT 0, xT 1])), 2217 ("STRH (-imm,pre,wb)", ("StoreHalf (imm,pre)", [xF 0, xT 1])), 2218 ("STRH (+imm,pre)", ("StoreHalf (imm,pre)", [xT 0, xF 1])), 2219 ("STRH (-imm,pre)", ("StoreHalf (imm,pre)", [xF 0, xF 1])), 2220 ("STRH (+imm,pre,pc)", 2221 ("StoreHalf (imm,pre)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2222 ("STRH (-imm,pre,pc)", 2223 ("StoreHalf (imm,pre)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2224 ("STRH (imm,post)", ("StoreHalf (imm,post)", [])), 2225 ("STRH (+reg,pre,wb)", ("StoreHalf (reg,pre)", [xT 0, xT 1])), 2226 ("STRH (-reg,pre,wb)", ("StoreHalf (reg,pre)", [xF 0, xT 1])), 2227 ("STRH (+reg,pre)", ("StoreHalf (reg,pre)", [xT 0, xF 1])), 2228 ("STRH (-reg,pre)", ("StoreHalf (reg,pre)", [xF 0, xF 1])), 2229 ("STRH (+reg,pre,pc)", 2230 ("StoreHalf (reg,pre)", [xT 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2231 ("STRH (-reg,pre,pc)", 2232 ("StoreHalf (reg,pre)", [xF 0, xF 1, xT 2, xT 3, xT 4, xT 5])), 2233 ("STRH (reg,post)", ("StoreHalf (reg,post)", [])), 2234 ("STRD (+imm,pre,wb)", ("StoreDual (imm)", [xT 0, xT 1, xT 2])), 2235 ("STRD (-imm,pre,wb)", ("StoreDual (imm)", [xT 0, xF 1, xT 2])), 2236 ("STRD (+imm,pre)", ("StoreDual (imm)", [xT 0, xT 1, xF 2])), 2237 ("STRD (-imm,pre)", ("StoreDual (imm)", [xT 0, xF 1, xF 2])), 2238 ("STRD (imm,post)", ("StoreDual (imm)", [xF 0, xF 2])), 2239 ("STRD (+reg,pre,wb)", ("StoreDual (reg)", [xT 0, xT 1, xT 2])), 2240 ("STRD (-reg,pre,wb)", ("StoreDual (reg)", [xT 0, xF 1, xT 2])), 2241 ("STRD (+reg,pre)", ("StoreDual (reg)", [xT 0, xT 1, xF 2])), 2242 ("STRD (-reg,pre)", ("StoreDual (reg)", [xT 0, xF 1, xF 2])), 2243 ("STRD (reg,post)", ("StoreDual (reg)", [xF 0, xF 2])), 2244 ("LDMDA", ("LoadMultiple", [xF 0, xF 1, xF 2])), 2245 ("LDMDB", ("LoadMultiple", [xT 0, xF 1, xF 2])), 2246 ("LDMIA", ("LoadMultiple", [xF 0, xT 1, xF 2])), 2247 ("LDMIB", ("LoadMultiple", [xT 0, xT 1, xF 2])), 2248 ("LDMDA (wb)", ("LoadMultiple", [xF 0, xF 1, xT 2])), 2249 ("LDMDB (wb)", ("LoadMultiple", [xT 0, xF 1, xT 2])), 2250 ("LDMIA (wb)", ("LoadMultiple", [xF 0, xT 1, xT 2])), 2251 ("LDMIB (wb)", ("LoadMultiple", [xT 0, xT 1, xT 2])), 2252 ("STMDA", ("StoreMultiple", [xF 0, xF 1, xF 2])), 2253 ("STMDB", ("StoreMultiple", [xT 0, xF 1, xF 2])), 2254 ("STMIA", ("StoreMultiple", [xF 0, xT 1, xF 2])), 2255 ("STMIB", ("StoreMultiple", [xT 0, xT 1, xF 2])), 2256 ("STMDA (wb)", ("StoreMultiple", [xF 0, xF 1, xT 2])), 2257 ("STMDB (wb)", ("StoreMultiple", [xT 0, xF 1, xT 2])), 2258 ("STMIA (wb)", ("StoreMultiple", [xF 0, xT 1, xT 2])), 2259 ("STMIB (wb)", ("StoreMultiple", [xT 0, xT 1, xT 2])), 2260 ("SWP" , ("Swap", [xF 0])), 2261 ("SWPB", ("Swap", [xT 0])), 2262 ("SETEND", ("Setend", [xF 0])), 2263 ("VADD (single)", ("VFPData", [xF 0, xT 2, xT 3, xF 12, xF 14])), 2264 ("VADD (double)", ("VFPData", [xF 0, xT 2, xT 3, xT 12, xF 14])), 2265 ("VSUB (single)", ("VFPData", [xF 0, xT 2, xT 3, xF 12, xT 14])), 2266 ("VSUB (double)", ("VFPData", [xF 0, xT 2, xT 3, xT 12, xT 14])), 2267 ("VMUL (single)", ("VFPData", [xF 0, xT 2, xF 3, xF 12, xF 14])), 2268 ("VMUL (double)", ("VFPData", [xF 0, xT 2, xF 3, xT 12, xF 14])), 2269 ("VNMUL (single)", ("VFPData", [xF 0, xT 2, xF 3, xF 12, xT 14])), 2270 ("VNMUL (double)", ("VFPData", [xF 0, xT 2, xF 3, xT 12, xT 14])), 2271 ("VMLA (single)", ("VFPData", [xF 0, xF 2, xF 3, xF 12, xF 14])), 2272 ("VMLA (double)", ("VFPData", [xF 0, xF 2, xF 3, xT 12, xF 14])), 2273 ("VMLS (single)", ("VFPData", [xF 0, xF 2, xF 3, xF 12, xT 14])), 2274 ("VMLS (double)", ("VFPData", [xF 0, xF 2, xF 3, xT 12, xT 14])), 2275 ("VNMLA (single)", ("VFPData", [xF 0, xF 2, xT 3, xF 12, xT 14])), 2276 ("VNMLA (double)", ("VFPData", [xF 0, xF 2, xT 3, xT 12, xT 14])), 2277 ("VNMLS (single)", ("VFPData", [xF 0, xF 2, xT 3, xF 12, xF 14])), 2278 ("VNMLS (double)", ("VFPData", [xF 0, xF 2, xT 3, xT 12, xF 14])), 2279 ("VFMA (single)", ("VFPData", [xT 0, xT 2, xF 3, xF 12])), 2280 ("VFMA (double)", ("VFPData", [xT 0, xT 2, xF 3, xT 12])), 2281 ("VFNMA (single)", ("VFPData", [xT 0, xF 2, xT 3, xF 12])), 2282 ("VFNMA (double)", ("VFPData", [xT 0, xF 2, xT 3, xT 12])), 2283 ("VMOV (single,reg)", 2284 ("VFPData", 2285 [xT 0, xT 2, xT 3, xF 4, xF 5, xF 6, xF 7, xF 12, xF 13, xT 14])), 2286 ("VMOV (double,reg)", 2287 ("VFPData", 2288 [xT 0, xT 2, xT 3, xF 4, xF 5, xF 6, xF 7, xT 12, xF 13, xT 14])), 2289 ("VMOV (single,imm)", ("VFPData", [xT 0, xT 2, xT 3, xF 12, xF 14])), 2290 ("VMOV (double,imm)", ("VFPData", [xT 0, xT 2, xT 3, xT 12, xF 14])), 2291 ("VCMP (single,zero)", 2292 ("VFPData", 2293 [xT 0, xT 2, xT 3, xF 4, xT 5, xF 6, xT 7, xF 12, xT 13, xT 14])), 2294 ("VCMP (double,zero)", 2295 ("VFPData", 2296 [xT 0, xT 2, xT 3, xF 4, xT 5, xF 6, xT 7, xT 12, xT 13, xT 14])), 2297 ("VCMP (single)", 2298 ("VFPData", 2299 [xT 0, xT 2, xT 3, xF 4, xT 5, xF 6, xF 7, xF 12, xT 13, xT 14])), 2300 ("VCMP (double)", 2301 ("VFPData", 2302 [xT 0, xT 2, xT 3, xF 4, xT 5, xF 6, xF 7, xT 12, xT 13, xT 14])), 2303 ("VABS (single)", 2304 ("VFPData", 2305 [xT 0, xT 2, xT 3, xF 4, xF 5, xF 6, xF 7, xF 12, xT 13, xT 14])), 2306 ("VABS (double)", 2307 ("VFPData", 2308 [xT 0, xT 2, xT 3, xF 4, xF 5, xF 6, xF 7, xT 12, xT 13, xT 14])), 2309 ("VNEG (single)", 2310 ("VFPData", 2311 [xT 0, xT 2, xT 3, xF 4, xF 5, xF 6, xT 7, xF 12, xF 13, xT 14])), 2312 ("VNEG (double)", 2313 ("VFPData", 2314 [xT 0, xT 2, xT 3, xF 4, xF 5, xF 6, xT 7, xT 12, xF 13, xT 14])), 2315 ("VSQRT (single)", 2316 ("VFPData", 2317 [xT 0, xT 2, xT 3, xF 4, xF 5, xF 6, xT 7, xF 12, xT 13, xT 14])), 2318 ("VSQRT (double)", 2319 ("VFPData", 2320 [xT 0, xT 2, xT 3, xF 4, xF 5, xF 6, xT 7, xT 12, xT 13, xT 14])), 2321 ("VDIV (single)", ("VFPData", [xT 0, xF 2, xF 3, xF 12, xF 14])), 2322 ("VDIV (double)", ("VFPData", [xT 0, xF 2, xF 3, xT 12, xF 14])), 2323 ("VCVT (single,double)", 2324 ("VFPData", 2325 [xT 0, xT 2, xT 3, xF 4, xT 5, xT 6, xT 7, xT 12, xT 13, xT 14])), 2326 ("VCVT (double,single,lo)", 2327 ("VFPData", 2328 [xT 0, xF 1, xT 2, xT 3, xF 4, xT 5, xT 6, xT 7, xF 12, xT 13, 2329 xT 14])), 2330 ("VCVT (double,single,hi)", 2331 ("VFPData", 2332 [xT 0, xT 1, xT 2, xT 3, xF 4, xT 5, xT 6, xT 7, xF 12, xT 13, 2333 xT 14])), 2334 ("VCVT (signed int,single)", 2335 ("VFPData", [xT 0, xT 2, xT 3, xT 4, xT 5, xF 6, xT 7, xF 12, xT 14])), 2336 ("VCVT (unsigned int,single)", 2337 ("VFPData", [xT 0, xT 2, xT 3, xT 4, xT 5, xF 6, xF 7, xF 12, xT 14])), 2338 ("VCVT (signed int,double)", 2339 ("VFPData", [xT 0, xT 2, xT 3, xT 4, xT 5, xF 6, xT 7, xT 12, xT 14])), 2340 ("VCVT (unsigned int,double)", 2341 ("VFPData", [xT 0, xT 2, xT 3, xT 4, xT 5, xF 6, xF 7, xT 12, xT 14])), 2342 ("VCVT (single,int)", 2343 ("VFPData", [xT 0, xT 2, xT 3, xT 4, xF 5, xF 6, xF 7, xF 12, xT 14])), 2344 ("VCVT (double,int,lo)", 2345 ("VFPData", 2346 [xT 0, xF 1, xT 2, xT 3, xT 4, xF 5, xF 6, xF 7, xT 12, xT 14])), 2347 ("VCVT (double,int,hi)", 2348 ("VFPData", 2349 [xT 0, xT 1, xT 2, xT 3, xT 4, xF 5, xF 6, xF 7, xT 12, xT 14])), 2350 ("VLDR (single,+imm)", ("VFPLoadStore", [xT 0, xT 2, xF 11])), 2351 ("VLDR (single,-imm)", ("VFPLoadStore", [xF 0, xT 2, xF 11])), 2352 ("VLDR (double,+imm)", ("VFPLoadStore", [xT 0, xT 2, xT 11])), 2353 ("VLDR (double,-imm)", ("VFPLoadStore", [xF 0, xT 2, xT 11])), 2354 ("VLDR (single,+imm,pc)", 2355 ("VFPLoadStore", [xT 0, xT 2, xT 3, xT 4, xT 5, xT 6, xF 11])), 2356 ("VLDR (single,-imm,pc)", 2357 ("VFPLoadStore", [xF 0, xT 2, xT 3, xT 4, xT 5, xT 6, xF 11])), 2358 ("VLDR (double,+imm,pc)", 2359 ("VFPLoadStore", [xT 0, xT 2, xT 3, xT 4, xT 5, xT 6, xT 11])), 2360 ("VLDR (double,-imm,pc)", 2361 ("VFPLoadStore", [xF 0, xT 2, xT 3, xT 4, xT 5, xT 6, xT 11])), 2362 ("VSTR (single,+imm)", ("VFPLoadStore", [xT 0, xF 2, xF 11])), 2363 ("VSTR (single,-imm)", ("VFPLoadStore", [xF 0, xF 2, xF 11])), 2364 ("VSTR (double,+imm)", ("VFPLoadStore", [xT 0, xF 2, xT 11])), 2365 ("VSTR (double,-imm)", ("VFPLoadStore", [xF 0, xF 2, xT 11])), 2366 ("VSTR (single,+imm,pc)", 2367 ("VFPLoadStore", [xT 0, xF 2, xT 3, xT 4, xT 5, xT 6, xF 11])), 2368 ("VSTR (single,-imm,pc)", 2369 ("VFPLoadStore", [xF 0, xF 2, xT 3, xT 4, xT 5, xT 6, xF 11])), 2370 ("VSTR (double,+imm,pc)", 2371 ("VFPLoadStore", [xT 0, xF 2, xT 3, xT 4, xT 5, xT 6, xT 11])), 2372 ("VSTR (double,-imm,pc)", 2373 ("VFPLoadStore", [xF 0, xF 2, xT 3, xT 4, xT 5, xT 6, xT 11])), 2374 ("VMOV (single from arm)", ("VFPTransfer", [xF 0, xF 1, xF 2, xF 3])), 2375 ("VMOV (single to arm)", ("VFPTransfer", [xF 0, xF 1, xF 2, xT 3])), 2376 ("VMOV (singles from arm,lo)", ("VFPTransfer2", [xF 0, xF 9, xF 10])), 2377 ("VMOV (singles from arm,hi)", ("VFPTransfer2", [xF 0, xF 9, xT 10])), 2378 ("VMOV (singles to arm,lo)", ("VFPTransfer2", [xT 0, xF 9, xF 10])), 2379 ("VMOV (singles to arm,hi)", ("VFPTransfer2", [xT 0, xF 9, xT 10])), 2380 ("VMOV (double from arm)", ("VFPTransfer2", [xF 0, xT 9])), 2381 ("VMOV (double to arm)", ("VFPTransfer2", [xT 0, xT 9])), 2382 ("VMRS (nzcv)", 2383 ("VFPTransfer", 2384 [xT 0, xT 1, xT 2, xT 3, xF 4, xF 5, xF 6, xT 7, 2385 xT 8, xT 9, xT 10, xT 11])), 2386 ("VMRS", 2387 ("VFPTransfer", [xT 0, xT 1, xT 2, xT 3, xF 4, xF 5, xF 6, xT 7])), 2388 ("VMSR", 2389 ("VFPTransfer", [xT 0, xT 1, xT 2, xF 3, xF 4, xF 5, xF 6, xT 7])), 2390 ("MRS (cpsr)", ("MoveToRegisterFromSpecial", [])), 2391 ("MSR (cpsr, reg)", ("MoveToSpecialFromRegister", [xF 3])), 2392 ("MSR (cpsr, imm)", ("SpecialFromImmediate", [xF 3])), 2393 ("MSR (cpsr, reg, control)", ("MoveToSpecialFromRegister", [xT 3])), 2394 ("MSR (cpsr, imm, control)", ("MoveToSpecialFromImmediate", [xT 3])), 2395 ("RFEDA", ("ReturnFromException", [xF 0, xF 1, xF 2])), 2396 ("RFEDB", ("ReturnFromException", [xT 0, xF 1, xF 2])), 2397 ("RFEIA", ("ReturnFromException", [xF 0, xT 1, xF 2])), 2398 ("RFEIB", ("ReturnFromException", [xT 0, xT 1, xF 2])), 2399 ("RFEDA (wb)", ("ReturnFromException", [xF 0, xF 1, xT 2])), 2400 ("RFEDB (wb)", ("ReturnFromException", [xT 0, xF 1, xT 2])), 2401 ("RFEIA (wb)", ("ReturnFromException", [xF 0, xT 1, xT 2])), 2402 ("RFEIB (wb)", ("ReturnFromException", [xT 0, xT 1, xT 2])), 2403 ("NOP", ("Hint", List.tabulate (8, xF))) 2404 ] 2405 fun list_instructions () = List.map fst (Redblackmap.listItems ast) 2406 fun printn s = TextIO.print (s ^ "\n") 2407 fun lsub s i = Char.toUpper (String.sub (s, i)) 2408 fun sharePrefix3 s1 s2 = 2409 let 2410 val n = Int.min (3, Int.min (String.size s1, String.size s2)) 2411 val f1 = lsub s1 2412 val f2 = lsub s2 2413 fun loop i = i >= n orelse f1 i = f2 i andalso loop (i + 1) 2414 in 2415 loop 0 2416 end 2417 val condMap = 2418 fn "EQ" => SOME "FFFF" 2419 | "NE" => SOME "FFFT" 2420 | "CS" => SOME "FFTF" 2421 | "CC" => SOME "FFTT" 2422 | "MI" => SOME "FTFF" 2423 | "PL" => SOME "FTFT" 2424 | "VS" => SOME "FTTF" 2425 | "VC" => SOME "FTTT" 2426 | "HI" => SOME "TFFF" 2427 | "LS" => SOME "TFFT" 2428 | "GE" => SOME "TFTF" 2429 | "LT" => SOME "TFTT" 2430 | "GT" => SOME "TTFF" 2431 | "LE" => SOME "TTFT" 2432 | "AL" => SOME "TTTF" 2433 | _ => NONE 2434 val condMapInv = 2435 fn "FFFF" => "EQ" 2436 | "FFFT" => "NE" 2437 | "FFTF" => "CS" 2438 | "FFTT" => "CC" 2439 | "FTFF" => "MI" 2440 | "FTFT" => "PL" 2441 | "FTTF" => "VS" 2442 | "FTTT" => "VC" 2443 | "TFFF" => "HI" 2444 | "TFFT" => "LS" 2445 | "TFTF" => "GE" 2446 | "TFTT" => "LT" 2447 | "TTFF" => "GT" 2448 | "TTFT" => "LE" 2449 | _ => "" 2450 fun insertCond c s = 2451 let 2452 val (a, b) = splitAtSpace s 2453 in 2454 a ^ c ^ b 2455 end 2456 fun LDM_STM s = String.isPrefix "LDM" s orelse String.isPrefix "STM" s 2457 fun comma i = 2458 let 2459 val is = Int.toString i 2460 in 2461 fn "" => is 2462 | s => is ^ "," ^ s 2463 end 2464 fun insertRegList opc s = 2465 if LDM_STM s 2466 then s ^ ";" ^ 2467 snd (List.foldr 2468 (fn (t, (i, s)) => 2469 (i + 1, if t = boolSyntax.T then comma i s else s)) 2470 (0, "") (List.drop (opc, 16))) 2471 else s 2472 val prefixes = List.rev (mlibUseful.sort_map String.size Int.compare 2473 (List.map prefix (list_instructions ()))) 2474 val splitAtSemi = utilsLib.splitAtChar (Lib.equal #";") 2475 fun splitOpcode s = 2476 let 2477 val (a, b) = 2478 (utilsLib.uppercase ## utilsLib.lowercase) (splitAtSpace s) 2479 val (a, b, c) = 2480 if b = "" 2481 then let val (a, c) = splitAtSemi a in (a, b, c) end 2482 else let val (b, c) = splitAtSemi b in (a, b, c) end 2483 val c = if c <> "" then String.extract (c, 1, NONE) else "none" 2484 val d = ("TTTF", a ^ b, c) 2485 val pfx = if String.size a = 3 andalso String.isPrefix "BL" a 2486 then SOME "B" 2487 else if String.size a = 5 andalso String.isPrefix "STRH" a 2488 then SOME "STR" 2489 else if String.size a = 5 andalso String.isPrefix "LDRH" a 2490 then SOME "LDR" 2491 else List.find (fn p => String.isPrefix p a) prefixes 2492 in 2493 case pfx of 2494 SOME p => 2495 let 2496 val a' = String.extract (a, String.size p, NONE) 2497 val n = String.size a' 2498 in 2499 if 1 < n 2500 then let 2501 val (l, r) = utilsLib.splitAtPos (n - 2) a' 2502 in 2503 case condMap r of 2504 SOME cond => (cond, p ^ l ^ b, c) 2505 | NONE => d 2506 end 2507 else d 2508 end 2509 | NONE => d 2510 end 2511 fun bit tm = if bitstringSyntax.dest_b tm then #"T" else #"F" 2512 val bitstring = String.implode o List.map bit 2513in 2514 val list_instructions = list_instructions 2515 fun print_instructions () = List.app printn (list_instructions ()) 2516 fun mk_arm_opcode s = 2517 let 2518 val (c, s, l) = splitOpcode s 2519 val lm = if LDM_STM s andalso l <> "none" then reg_list_subst l else [] 2520 in 2521 case Redblackmap.peek (ast, s) of 2522 SOME (s, m) => 2523 (I ## Term.subst (m @ lm)) (mk_arm_pattern_opcode c s) 2524 | NONE => 2525 let 2526 val p = List.filter (sharePrefix3 s) (list_instructions ()) 2527 |> Lib.commafy 2528 |> String.concat 2529 val p = if p = "" then "." else ". Try: " ^ p 2530 in 2531 raise ERR "mk_arm_opcode" ("Not found: " ^ s ^ p) 2532 end 2533 end 2534 fun arm_instruction i = 2535 let 2536 val c = bitstring (List.take (i, 4)) 2537 val opc = listSyntax.mk_list (i, Type.bool) 2538 val ins = insertCond (condMapInv c) 2539 fun mtch s = Term.match_term (snd (mk_arm_opcode (ins s))) opc 2540 in 2541 List.map (insertRegList i o ins) 2542 (List.filter (Lib.can mtch) (list_instructions())) 2543 end 2544end 2545 2546(* -- *) 2547 2548local 2549 fun f thm ps = List.map (DecodeARM_rwt thm) (List.map snd ps) 2550 val rwts_14 = f DecodeARM_14 arm_patterns 2551 val rwts_15 = f DecodeARM_15 arm_patterns15 2552 val rwts_other = f DecodeARM_other arm_patterns 2553 val undef = 2554 List.map (DATATYPE_RULE o Thm.INST [state_with_enc ``Encoding_ARM``]) 2555 UndefinedARM_rwt 2556 val se = fix_datatype ``^st with Encoding := Encoding_ARM`` 2557 val DecodeARM_tm = mk_arm_const "DecodeARM" 2558 fun mk_decode_arm t = Term.list_mk_comb (DecodeARM_tm, [t, se]) 2559 val rewrites = 2560 [v2w_13_15_rwts, v2w_ground4, boolTheory.COND_ID, 2561 bitstringLib.v2n_CONV ``v2n [F;F;F;F;F]``, 2562 blastLib.BBLAST_PROVE 2563 ``((v2w [T;T;b;T] = 13w: word4) \/ (v2w [T;T;b;T] = 15w: word4)) = T``] 2564 val COND_RULE = 2565 Conv.RIGHT_CONV_RULE (REG_CONV THENC REWRITE_CONV iConditionPassed_rwts) o 2566 utilsLib.ALL_HYP_CONV_RULE REG_CONV 2567 val raise_tm = mk_arm_const "raise'exception" 2568 val avoid = 2569 List.filter 2570 (not o Lib.can (HolKernel.find_term (Term.same_const raise_tm) o rhsc)) 2571 val FINISH_RULE = 2572 List.map 2573 (utilsLib.MATCH_HYP_CONV_RULE (Conv.REWR_CONV bool_not_pc) 2574 ``~(b3 /\ b2 /\ b1 /\ b0)`` o 2575 Conv.RIGHT_CONV_RULE 2576 (REG_CONV THENC Conv.DEPTH_CONV bitstringLib.v2n_CONV)) 2577 val rwconv = REWRITE_CONV rewrites 2578in 2579 fun arm_decode tms = 2580 let 2581 val x = (DATATYPE_CONV, fix_datatypes tms) 2582 fun gen_rws m r = rewrites @ utilsLib.specialized m x r 2583 val rw14 = REWRITE_CONV (gen_rws "decode ARM (cond = 14)" rwts_14) 2584 val rw15 = REWRITE_CONV (gen_rws "decode ARM (cond = 15)" rwts_15) 2585 val net = 2586 utilsLib.mk_rw_net utilsLib.lhsc 2587 (utilsLib.specialized 2588 "decode ARM (cond not in {14, 15})" x rwts_other) 2589 fun find_rw_other tm = 2590 Lib.singleton_of_list (utilsLib.find_rw net tm) 2591 handle HOL_ERR {message = "not found", ...} => raise Conv.UNCHANGED 2592 | HOL_ERR {message = m, 2593 origin_function = "singleton_of_list", ...} => 2594 raise ERR "arm_decode" 2595 "more than one matching decode pattern" 2596 val FALL_CONV = 2597 REWRITE_CONV 2598 (DecodeVFP :: datatype_thms [v2w_ground4] @ undef @ 2599 iConditionPassed_rwts @ 2600 gen_rws "decode ARM (fallback)" [DecodeARM_fall]) 2601 in 2602 fn (x : bool list, v) => 2603 let 2604 val (c, t) = mk_opcode v 2605 val tm = mk_decode_arm t 2606 in 2607 ((case c of 2608 Cond14 => rw14 tm 2609 | Cond15 => rw15 tm 2610 | Cond cnd => 2611 let 2612 val rwt = tm |> find_rw_other 2613 |> Thm.INST cnd 2614 |> COND_RULE 2615 in 2616 (Conv.REWR_CONV rwt THENC rwconv) tm 2617 end) 2618 handle Conv.UNCHANGED => 2619 ( WARN "arm_decode" "fallback (slow) decode" 2620 ; FALL_CONV tm )) 2621 |> utilsLib.split_conditions 2622 |> avoid 2623 |> utilsLib.pick x 2624 |> FINISH_RULE 2625 end 2626 end 2627end 2628 2629local 2630 fun uncond c = Lib.mem (Char.toUpper c) [#"E", #"F"] 2631in 2632 fun arm_decode_hex opt = 2633 let 2634 val dec = arm_decode (arm_configLib.mk_config_terms opt) 2635 in 2636 fn s => 2637 let 2638 val s = utilsLib.removeSpaces s 2639 val v = bitstringSyntax.bitstring_of_hexstring s 2640 val x = if String.size s = 8 andalso uncond (String.sub (s, 0)) 2641 then [true] 2642 else [true, true] 2643 in 2644 dec (x, v) 2645 end 2646 end 2647end 2648 2649(* ========================================================================= *) 2650 2651(* Run *) 2652 2653val NoOperation_rwt = 2654 EV [dfn'NoOperation_def, IncPC_rwt] [] [] 2655 ``dfn'NoOperation`` 2656 |> addThms 2657 2658val DataMemoryBarrier_rwt = 2659 EV [dfn'DataMemoryBarrier_def, IncPC_rwt] [] [] 2660 ``dfn'DataMemoryBarrier opt`` 2661 |> addThms 2662 2663(* ---------------------------- *) 2664 2665val Setend_rwt = 2666 EV [dfn'Setend_def, IncPC_rwt] [] [] 2667 ``dfn'Setend b`` 2668 |> addThms 2669 2670(* ---------------------------- *) 2671 2672val BranchTarget_rwts = 2673 let 2674 val thms = [dfn'BranchTarget_def, PC_rwt, not_cond, align_aligned] 2675 val tm = 2676 ``aligned 2 (s.REG RName_PC + (if s.CPSR.T then 4w else 8w) + imm32)`` 2677 in 2678 ( 2679 EV (hd BranchWritePC_rwt :: thms) [] [] 2680 ``dfn'BranchTarget imm32`` 2681 |> List.map (utilsLib.ALL_HYP_RULE 2682 (utilsLib.INST_REWRITE_RULE [Aligned_BranchTarget_thumb])) 2683 ) 2684 @ 2685 ( 2686 EV (tl BranchWritePC_rwt @ thms) [] [] 2687 ``dfn'BranchTarget imm32`` 2688 |> List.map (utilsLib.ALL_HYP_CONV_RULE 2689 (utilsLib.INST_REWRITE_CONV [ASSUME tm] 2690 THENC REWRITE_CONV [])) 2691 |> List.map (utilsLib.ALL_HYP_RULE 2692 (utilsLib.INST_REWRITE_RULE [Aligned_BranchTarget_arm])) 2693 ) 2694 |> addThms 2695 end 2696 2697(* ---------------------------- *) 2698 2699val BranchExchange_rwt = 2700 EV ([dfn'BranchExchange_def, R_rwt, BXWritePC_rwt, CurrentInstrSet_rwt, 2701 Align_LoadWritePC] @ SelectInstrSet_rwt) 2702 [[``m <> 15w: word4``]] [] 2703 ``dfn'BranchExchange m`` 2704 |> List.map COND_UPDATE_RULE 2705 |> addThms 2706 2707val BranchExchange_pc_arm_rwt = 2708 EV ([dfn'BranchExchange_def, BXWritePC_rwt, R15_rwt, 2709 arm_stepTheory.Aligned4_bit0, CurrentInstrSet_rwt] @ SelectInstrSet_rwt) 2710 [[``~^st.CPSR.T``]] [] 2711 ``dfn'BranchExchange 15w`` 2712 |> List.map 2713 (utilsLib.MATCH_HYP_CONV_RULE 2714 (utilsLib.INST_REWRITE_CONV 2715 [arm_stepTheory.Aligned4_bit0, arm_stepTheory.Aligned4_bit1] 2716 THENC REWRITE_CONV []) ``a ==> b``) 2717 |> addThms 2718 2719val BranchExchange_pc_thumb_rwt = 2720 EV ([dfn'BranchExchange_def, BXWritePC_rwt, R15_rwt, 2721 Aligned4_bit0_t, CurrentInstrSet_rwt] @ SelectInstrSet_rwt) 2722 [[``^st.CPSR.T``]] [] 2723 ``dfn'BranchExchange 15w`` 2724 |> List.map 2725 (utilsLib.MATCH_HYP_CONV_RULE 2726 (utilsLib.INST_REWRITE_CONV 2727 [arm_stepTheory.Aligned4_bit0_t, 2728 arm_stepTheory.Aligned4_bit1_t] 2729 THENC REWRITE_CONV []) ``a ==> b``) 2730 |> addThms 2731 2732(* ---------------------------- *) 2733 2734val R_x_14_not_pc = 2735 arm_stepTheory.R_x_not_pc 2736 |> Q.INST [`d` |-> `14w: word4`] 2737 |> utilsLib.ALL_HYP_CONV_RULE wordsLib.WORD_EVAL_CONV 2738 2739val BranchLinkExchangeRegister_rwt = 2740 EV ([dfn'BranchLinkExchangeRegister_def, R_rwt, write'R_rwt, PC_rwt, 2741 BXWritePC_rwt, CurrentInstrSet_rwt, write'LR_def, R_x_14_not_pc, 2742 not_cond, Align_LoadWritePC] @ SelectInstrSet_rwt) 2743 [[``m <> 15w: word4``]] [] 2744 ``dfn'BranchLinkExchangeRegister m`` 2745 |> List.map 2746 (COND_UPDATE_RULE o 2747 utilsLib.ALL_HYP_CONV_RULE 2748 (DATATYPE_CONV 2749 THENC REWRITE_CONV [PC_rwt, boolTheory.COND_ID] 2750 THENC wordsLib.WORD_EVAL_CONV) o 2751 utilsLib.SRW_RULE []) 2752 |> addThms 2753 2754(* ---------------------------- *) 2755 2756fun BranchLinkExchangeImmediate_rwt (c, t, rwt) = 2757 EV ([dfn'BranchLinkExchangeImmediate_def, write'R_rwt, PC_rwt, 2758 CurrentInstrSet_rwt, write'LR_def, R_x_14_not_pc] @ 2759 SelectInstrSet_rwt) [[c]] [] 2760 ``dfn'BranchLinkExchangeImmediate (^t, imm32)`` 2761 |> List.map 2762 (utilsLib.ALL_HYP_CONV_RULE 2763 (DATATYPE_CONV 2764 THENC REWRITE_CONV [PC_rwt, boolTheory.COND_ID] 2765 THENC wordsLib.WORD_EVAL_CONV)) 2766 |> List.map 2767 (utilsLib.MATCH_HYP_CONV_RULE 2768 (REWRITE_CONV [Aligned_Align_plus_minus]) ``a \/ b : bool`` o 2769 FULL_DATATYPE_RULE o 2770 Conv.CONV_RULE (utilsLib.INST_REWRITE_CONV [rwt])) 2771 2772val BranchLinkExchangeImmediate_thumb_arm_rwt = 2773 BranchLinkExchangeImmediate_rwt 2774 (``^st.CPSR.T``, ``InstrSet_ARM``, hd (tl BranchWritePC_rwt)) 2775 |> addThms 2776 2777val BranchLinkExchangeImmediate_thumb_thumb_rwt = 2778 BranchLinkExchangeImmediate_rwt 2779 (``^st.CPSR.T``, ``InstrSet_Thumb``, hd BranchWritePC_rwt) 2780 |> List.map 2781 (utilsLib.INST_REWRITE_RULE 2782 [AlignedPC_plus_xthumb, AlignedPC_plus_thumb]) 2783 |> addThms 2784 2785local 2786 val rule = 2787 REWRITE_RULE [blastLib.BBLAST_PROVE ``w + 8w - 4w = w + 4w: word32``] 2788in 2789 val BranchLinkExchangeImmediate_arm_arm_rwt = 2790 BranchLinkExchangeImmediate_rwt 2791 (``~^st.CPSR.T``, ``InstrSet_ARM``, hd (tl BranchWritePC_rwt)) 2792 |> List.map 2793 (rule o utilsLib.INST_REWRITE_RULE [AlignedPC_plus_align_arm]) 2794 |> addThms 2795 val BranchLinkExchangeImmediate_arm_thumb_rwt = 2796 BranchLinkExchangeImmediate_rwt 2797 (``~^st.CPSR.T``, ``InstrSet_Thumb``, hd BranchWritePC_rwt) 2798 |> List.map (rule o utilsLib.INST_REWRITE_RULE [AlignedPC_plus_xarm]) 2799 |> addThms 2800end 2801 2802(* ---------------------------- *) 2803 2804val IfThen_rwt = 2805 EV [dfn'IfThen_def, IncPC_rwt] [] [] 2806 ``dfn'IfThen (firstcond, mask)`` 2807 |> addThms 2808 2809(* ---------------------------- *) 2810 2811(* 2812val () = setEvConv (Conv.DEPTH_CONV 2813 (bitstringLib.extract_v2w_CONV 2814 ORELSEC bitstringLib.v2w_eq_CONV 2815 ORELSEC bitstringLib.word_bit_CONV)) 2816*) 2817 2818val () = setEvConv utilsLib.WGROUND_CONV 2819 2820(* 2821val DataProcessingPC_nsetflags_rwt = 2822 List.map (fn (r, w) => 2823 EV [r, addInstTag w, arm_stepTheory.R_x_not_pc, 2824 SET_RULE DataProcessingPC_def, DataProcessingALU_def, 2825 AddWithCarry, wordsTheory.FST_ADD_WITH_CARRY, 2826 ArithmeticOpcode_def, PC_rwt, IncPC_rwt, cond_rand_thms] [] 2827 (mapl (`opc`, utilsLib.tab_fixedwidth 16 4)) 2828 ``DataProcessingPC (opc, F, n, imm32)``) reg_rwts 2829 |> List.concat 2830*) 2831 2832local 2833 val x = ``x: word32 # bool`` 2834 val DataProcessing = 2835 DataProcessing_def 2836 |> Q.SPECL [`opc`, `setflags`, `d`, `n`, `FST ^x`, `SND ^x`] 2837 |> REWRITE_RULE [pairTheory.PAIR] 2838 |> utilsLib.SET_RULE 2839 val DataProcessing_rwts = 2840 List.map 2841 (fn opc => 2842 let 2843 val i = wordsSyntax.uint_of_word opc 2844 val wr = if i < 8 orelse 11 < i then [write'R_rwt] else [] 2845 in 2846 EV ([R_rwt, arm_stepTheory.R_x_not_pc, 2847 DataProcessing, DataProcessingALU_def, 2848 AddWithCarry, wordsTheory.FST_ADD_WITH_CARRY, 2849 ArithmeticOpcode_def, PC_rwt, IncPC_rwt, cond_rand_thms] @ 2850 wr) [] [[`opc` |-> opc]] 2851 ``DataProcessing (opc, setflags, d, n, imm32_c)`` 2852 end 2853 |> List.map 2854 (utilsLib.ALL_HYP_CONV_RULE 2855 (REWRITE_CONV [boolTheory.COND_ID]) o 2856 SIMP_RULE bool_ss [])) opcodes 2857in 2858 fun dp n = List.nth (DataProcessing_rwts, n) 2859end 2860 2861val mov_mvn = dp 13 @ dp 15 2862val al = List.concat (List.tabulate (8, fn i => dp i) @ [dp 12, dp 14]) 2863val tc = List.concat (List.tabulate (4, fn i => dp (8 + i))) 2864 2865(* ---------------------------- *) 2866 2867val () = setEvConv utilsLib.WGROUND_CONV 2868 2869(* 2870val AddSub_rwt = 2871 EV [dfn'AddSub_def] [] (TF `sub`) 2872 ``dfn'AddSub (sub, d, n, imm12)`` 2873 |> addThms 2874*) 2875 2876val Move_rwt = 2877 EV ([dfn'Move_def, ExpandImm_C_rwt, bitstringTheory.word_concat_v2w_rwt, 2878 utilsLib.map_conv bitstringLib.v2w_n2w_CONV 2879 [``v2w [T] : word1``, ``v2w [F] : word1``], 2880 wordsTheory.WORD_OR_CLAUSES] @ mov_mvn) 2881 [[``d <> 15w: word4``]] (TF `negate`) 2882 ``dfn'Move (setflags, negate, d, ^(bitstringSyntax.mk_vec 12 0))`` 2883 |> List.map (utilsLib.MATCH_HYP_CONV_RULE 2884 (REWRITE_CONV [wordsTheory.WORD_OR_CLAUSES]) 2885 ``a \/ b \/ c : bool``) 2886 |> addThms 2887 2888val () = setEvConv (Conv.DEPTH_CONV bitstringLib.v2w_n2w_CONV 2889 THENC utilsLib.WGROUND_CONV) 2890 2891val TestCompareImmediate_rwt = 2892 EV ([dfn'TestCompareImmediate_def, bitstringTheory.word_concat_v2w_rwt, 2893 ExpandImm_C_rwt] @ tc) [] 2894 (mapl (`op`, utilsLib.tab_fixedwidth 4 2)) 2895 ``dfn'TestCompareImmediate (op, n, ^(bitstringSyntax.mk_vec 12 0))`` 2896 |> addThms 2897 2898val ArithLogicImmediate_rwt = 2899 EV ([dfn'ArithLogicImmediate_def, bitstringTheory.word_concat_v2w_rwt, 2900 ExpandImm_C_rwt] @ al) 2901 [[``d <> 15w: word4``]] (mapl (`op`, arithlogic)) 2902 ``dfn'ArithLogicImmediate 2903 (op, setflags, d, n, ^(bitstringSyntax.mk_vec 12 0))`` 2904 |> addThms 2905 2906(* ---------------------------- *) 2907 2908val () = setEvConv utilsLib.WGROUND_CONV 2909 2910val ShiftImmediate_rwt = 2911 EV ([dfn'ShiftImmediate_def, R_rwt, doRegister_def, ArithmeticOpcode_def, 2912 Shift_C_DecodeImmShift_rwt, wordsTheory.WORD_OR_CLAUSES] @ mov_mvn) 2913 [[``d <> 15w: word4``]] (TF `negate`) 2914 ``dfn'ShiftImmediate 2915 (negate, setflags, d, m, 2916 FST (DecodeImmShift (v2w [a; b], imm5)), 2917 SND (DecodeImmShift (v2w [a; b], imm5)))`` 2918 |> List.map (utilsLib.ALL_HYP_CONV_RULE 2919 (REWRITE_CONV [wordsTheory.WORD_OR_CLAUSES]) o 2920 REWRITE_RULE []) 2921 |> addThms 2922 2923val () = setEvConv (Conv.DEPTH_CONV bitstringLib.v2w_n2w_CONV 2924 THENC utilsLib.WGROUND_CONV) 2925 2926val TestCompareRegister_rwt = 2927 EV ([dfn'TestCompareRegister_def, R_rwt, bitstringTheory.word_concat_v2w_rwt, 2928 doRegister_def, ArithmeticOpcode_def, Shift_C_DecodeImmShift_rwt] @ tc) 2929 [] 2930 (mapl (`op`, utilsLib.tab_fixedwidth 4 2)) 2931 ``dfn'TestCompareRegister 2932 (op, n, m, 2933 FST (DecodeImmShift (v2w [a; b], imm5)), 2934 SND (DecodeImmShift (v2w [a; b], imm5)))`` 2935 |> List.map (utilsLib.ALL_HYP_CONV_RULE (REWRITE_CONV []) o 2936 REWRITE_RULE []) 2937 |> addThms 2938 2939val () = setEvConv utilsLib.WGROUND_CONV 2940 2941val Register_rwt = 2942 EV ([dfn'Register_def, R_rwt, doRegister_def, ArithmeticOpcode_def, 2943 Shift_C_DecodeImmShift_rwt] @ al) 2944 [[``d <> 15w: word4``]] (mapl (`op`, arithlogic)) 2945 ``dfn'Register 2946 (op, setflags, d, n, m, 2947 FST (DecodeImmShift (v2w [a; b], imm5)), 2948 SND (DecodeImmShift (v2w [a; b], imm5)))`` 2949 |> List.map (utilsLib.ALL_HYP_CONV_RULE (REWRITE_CONV []) o 2950 REWRITE_RULE []) 2951 |> addThms 2952 2953(* ---------------------------- *) 2954 2955val () = setEvConv utilsLib.WGROUND_CONV 2956 2957val ShiftRegister_rwt = 2958 EV ([dfn'ShiftRegister_def, R_rwt, doRegisterShiftedRegister_def, 2959 ArithmeticOpcode_def, Shift_C_DecodeRegShift_rwt, 2960 wordsTheory.WORD_OR_CLAUSES] @ mov_mvn) 2961 [[``d <> 15w: word4``, ``n <> 15w: word4``, ``m <> 15w: word4``]] 2962 (TF `negate`) 2963 ``dfn'ShiftRegister 2964 (negate, setflags, d, n, DecodeRegShift (v2w [a; b]), m)`` 2965 |> List.map 2966 (utilsLib.ALL_HYP_CONV_RULE 2967 (REWRITE_CONV [Shift_C_DecodeRegShift_rwt, 2968 wordsTheory.WORD_OR_CLAUSES])) 2969 |> addThms 2970 2971val TestCompareRegisterShiftedRegister_rwt = 2972 EV ([dfn'RegisterShiftedRegister_def, R_rwt, doRegisterShiftedRegister_def, 2973 ArithmeticOpcode_def, Shift_C_DecodeRegShift_rwt] @ tc) 2974 [[``n <> 15w: word4``, ``m <> 15w: word4``, ``r <> 15w: word4``]] 2975 (mapl (`op`, testcompare)) 2976 ``dfn'RegisterShiftedRegister 2977 (op, T, d, n, m, DecodeRegShift (v2w [a; b]), r)`` 2978 |> List.map (utilsLib.ALL_HYP_CONV_RULE 2979 (REWRITE_CONV [Shift_C_DecodeRegShift_rwt])) 2980 |> addThms 2981 2982val RegisterShiftedRegister_rwt = 2983 EV ([dfn'RegisterShiftedRegister_def, R_rwt, doRegisterShiftedRegister_def, 2984 ArithmeticOpcode_def, Shift_C_DecodeRegShift_rwt] @ al) 2985 [[``d <> 15w: word4``, ``n <> 15w: word4``, ``m <> 15w: word4``, 2986 ``r <> 15w: word4``]] 2987 (mapl (`op`, arithlogic)) 2988 ``dfn'RegisterShiftedRegister 2989 (op, setflags, d, n, m, DecodeRegShift (v2w [a; b]), r)`` 2990 |> List.map (utilsLib.ALL_HYP_CONV_RULE 2991 (REWRITE_CONV [Shift_C_DecodeRegShift_rwt])) 2992 |> addThms 2993 2994(* ---------------------------- *) 2995 2996val () = resetEvConv () 2997 2998val CountLeadingZeroes_rwt = 2999 regEV [`d`] [dfn'CountLeadingZeroes_def] [] [] 3000 ``dfn'CountLeadingZeroes (d, m)`` 3001 3002val MoveHalfword_rwt = 3003 regEV [`d`] [dfn'MoveHalfword_def] [] (TF `neg`) 3004 ``dfn'MoveHalfword (neg, d, imm16)`` 3005 3006(* ---------------------------- *) 3007 3008val Multiply32_rwt = 3009 regEV [`d`] [dfn'Multiply32_def] 3010 [[``n <> 15w: word4``, ``m <> 15w: word4``]] [] 3011 ``dfn'Multiply32 (setflags, d, n, m)`` 3012 3013val MultiplyAccumulate_rwt = 3014 regEV [`d`] [dfn'MultiplyAccumulate_def] 3015 [[``n <> 15w: word4``, ``m <> 15w: word4``, ``a <> 15w: word4``]] [] 3016 ``dfn'MultiplyAccumulate (setflags, d, n, m, a)`` 3017 3018val MultiplyLong_rwt = 3019 regEV [`dhi: word4`, `dlo: word4`] [dfn'MultiplyLong_def] 3020 [[``dhi <> 15w: word4``, ``dlo <> 15w: word4``, 3021 ``n <> 15w: word4``, ``m <> 15w: word4``]] (TF `signed`) 3022 ``dfn'MultiplyLong (accumulate, signed, setflags, dhi, dlo, n, m)`` 3023 3024val Signed16Multiply32Accumulate_rwt = 3025 EV ([dfn'Signed16Multiply32Accumulate_def, IncPC_rwt, R_rwt, write'R_rwt] @ 3026 npc_thm [`d`]) 3027 [[``d <> 15w: word4``, ``n <> 15w: word4``, 3028 ``m <> 15w: word4``, ``a <> 15w: word4``]] [] 3029 ``dfn'Signed16Multiply32Accumulate (m_high, n_high, d, n, m, a)`` 3030 |> List.map (FULL_DATATYPE_RULE o COND_UPDATE_RULE) 3031 |> addThms 3032 3033(* ---------------------------- *) 3034 3035(* Media *) 3036 3037val ExtendByte_rwt = 3038 regEV [`d`] [dfn'ExtendByte_def, ROR_rwt] 3039 [[``d <> 15w: word4``, ``m <> 15w: word4``]] [] 3040 ``dfn'ExtendByte (u, d, n, m, rot)`` 3041 3042val ExtendByte16_rwt = 3043 regEV [`d`] [dfn'ExtendByte16_def, ROR_rwt] 3044 [[``d <> 15w: word4``, ``m <> 15w: word4``]] [] 3045 ``dfn'ExtendByte16 (U, d, n, m, rot)`` 3046 3047val ExtendHalfword_rwt = 3048 regEV [`d`] [dfn'ExtendHalfword_def, ROR_rwt] 3049 [[``d <> 15w: word4``, ``m <> 15w: word4``]] [] 3050 ``dfn'ExtendHalfword (u, d, n, m, rot)`` 3051 3052val SelectBytes_rwt = 3053 regEV [`d`] [dfn'SelectBytes_def] 3054 [[``d <> 15w: word4``, ``n <> 15w: word4``, ``m <> 15w: word4``]] [] 3055 ``dfn'SelectBytes (d, n, m)`` 3056 3057val ByteReverse_rwt = 3058 regEV [`d`] [dfn'ByteReverse_def] 3059 [[``d <> 15w: word4``, ``m <> 15w:word4``]] [] 3060 ``dfn'ByteReverse (d, m)`` 3061 3062val ByteReversePackedHalfword_rwt = 3063 regEV [`d`] [dfn'ByteReversePackedHalfword_def] 3064 [[``d <> 15w: word4``, ``m <> 15w:word4``]] [] 3065 ``dfn'ByteReversePackedHalfword (d, m)`` 3066 3067val ByteReverseSignedHalfword_rwt = 3068 regEV [`d`] [dfn'ByteReverseSignedHalfword_def] 3069 [[``d <> 15w: word4``, ``m <> 15w:word4``]] [] 3070 ``dfn'ByteReverseSignedHalfword (d, m)`` 3071 3072val ReverseBits_rwt = 3073 regEV [`d`] [dfn'ReverseBits_def] 3074 [[``d <> 15w: word4``, ``m <> 15w:word4``]] [] 3075 ``dfn'ReverseBits (d, m)`` 3076 3077val BitFieldExtract_rwt = 3078 regEV [`d`] [dfn'BitFieldExtract_def] 3079 [[``d <> 15w: word4``, ``n <> 15w: word4``]] [] 3080 ``dfn'BitFieldExtract (U, d, n, lsb, widthminus1)`` 3081 3082val BitFieldClearOrInsert_rwt = 3083 regEV [`d`] [dfn'BitFieldClearOrInsert_def, field_insert] 3084 [[``d <> 15w: word4``]] [] 3085 ``dfn'BitFieldClearOrInsert (d, n, lsb, msb)`` 3086 3087(* Add a few more multiplies and SIMD instructions *) 3088 3089(* ---------------------------- *) 3090 3091local 3092 local 3093 fun mapCons l (x: {redex: term frag list, residue: term}) = 3094 List.map (fn s => (x :: s)) l 3095 in 3096 fun substCases cs l = List.concat (List.map (mapCons l) cs) 3097 end 3098 3099 val immediate1 = 3100 substCases 3101 [`m` |-> ``immediate_form1 imm32``, 3102 `m` |-> ``register_form1 3103 (r, FST (DecodeImmShift (v2w [b1; b0], imm5)), 3104 SND (DecodeImmShift (v2w [b1; b0], imm5)))``] 3105 3106 val immediate2 = 3107 substCases [`m` |-> ``immediate_form2 imm32``, 3108 `m` |-> ``register_form2 r``] 3109 3110 val immediate3 = 3111 substCases 3112 [`m` |-> ``immediate_form1 imm32``, 3113 `m` |-> ``register_form1 (r, SRType_LSL, imm2)``] 3114in 3115 val addr = 3116 [[`idx` |-> ``T``, `wb` |-> ``F``, `a` |-> ``T``], 3117 [`idx` |-> ``T``, `wb` |-> ``F``, `a` |-> ``F``], 3118 [`idx` |-> ``F``, `wb` |-> ``T``], 3119 [`idx` |-> ``T``, `wb` |-> ``T``, `a` |-> ``T``], 3120 [`idx` |-> ``T``, `wb` |-> ``T``, `a` |-> ``F``]] 3121 val bpc_addr = List.take (addr, 2) 3122 val addr1 = immediate1 addr 3123 val addr2 = immediate2 addr 3124 val addr3 = immediate3 addr 3125 val bpc_addr1 = immediate1 bpc_addr 3126 val bpc_addr2 = immediate2 bpc_addr 3127 val bpc_addr3 = immediate3 bpc_addr 3128 val plain_addr1 = immediate1 [[`a` |-> ``T``], [`a` |-> ``F``]] 3129end 3130 3131(* ---------------------------- *) 3132 3133val rule_sp = 3134 utilsLib.MATCH_HYP_RULE 3135 (PURE_ASM_REWRITE_RULE [boolTheory.OR_CLAUSES] o 3136 Conv.CONV_RULE (utilsLib.INST_REWRITE_CONV [Aligned_plus_minus])) 3137 ``a \/ b \/ c : bool`` 3138 3139val rule_pc = 3140 rule_sp o 3141 FULL_DATATYPE_RULE o 3142 utilsLib.ALL_HYP_CONV_RULE 3143 (Conv.DEPTH_CONV (utilsLib.INST_REWRITE_CONV [write'R_rwt])) o 3144 Conv.CONV_RULE (utilsLib.INST_REWRITE_CONV [write'R_rwt]) o 3145 ASM_REWRITE_RULE [] 3146 3147fun rule_npc b = 3148 (if b then rule_sp else Lib.I) o 3149 REWRITE_RULE (npc_thm [`t`, `n`]) o 3150 FULL_DATATYPE_RULE o 3151 Conv.CONV_RULE (Conv.DEPTH_CONV (utilsLib.INST_REWRITE_CONV [write'R_rwt])) o 3152 ASM_REWRITE_RULE [] 3153 3154val align_base_pc_rule = 3155 utilsLib.MATCH_HYP_CONV_RULE 3156 (utilsLib.INST_REWRITE_CONV 3157 [Aligned2_base_pc_plus, Aligned2_base_pc_minus, 3158 Aligned4_base_pc_plus, Aligned4_base_pc_minus]) 3159 ``aligned n (w: word32)`` 3160 3161val rule_base_pc = 3162 align_base_pc_rule o 3163 REWRITE_RULE (npc_thm [`t`]) o 3164 FULL_DATATYPE_RULE o 3165 Conv.CONV_RULE (Conv.DEPTH_CONV (utilsLib.INST_REWRITE_CONV [write'R_rwt])) o 3166 DATATYPE_RULE o 3167 ASM_REWRITE_RULE [] 3168 3169val rule_literal_pc = 3170 utilsLib.MATCH_HYP_CONV_RULE (REWRITE_CONV [Aligned_Align_plus_minus]) 3171 ``aligned 2 (w: word32)`` o 3172 ASM_REWRITE_RULE [] 3173 3174val rule_literal = 3175 utilsLib.MATCH_HYP_CONV_RULE (REWRITE_CONV [Aligned_Align_plus_minus]) 3176 ``aligned n (w: word32)`` o 3177 utilsLib.INST_REWRITE_RULE [Align4_base_pc_plus, Align4_base_pc_minus] o 3178 REWRITE_RULE (npc_thm [`t`]) o 3179 DATATYPE_RULE o 3180 Conv.CONV_RULE (Conv.DEPTH_CONV (utilsLib.INST_REWRITE_CONV [write'R_rwt])) o 3181 ASM_REWRITE_RULE [] 3182 3183val rule_npc2 = 3184 rule_sp o 3185 utilsLib.ALL_HYP_CONV_RULE 3186 (Conv.DEPTH_CONV (utilsLib.INST_REWRITE_CONV [write'R_rwt]) 3187 THENC DATATYPE_CONV 3188 THENC REWRITE_CONV [alignmentTheory.aligned_numeric, 3189 alignmentTheory.aligned_add_sub_123]) o 3190 REWRITE_RULE (npc_thm [`t`, `t2`, `n`]) o 3191 FULL_DATATYPE_RULE o 3192 Conv.CONV_RULE (Conv.DEPTH_CONV (utilsLib.INST_REWRITE_CONV [write'R_rwt])) o 3193 ASM_REWRITE_RULE [] 3194 3195val rule_base_pc2 = 3196 utilsLib.ALL_HYP_CONV_RULE 3197 (Conv.DEPTH_CONV (utilsLib.INST_REWRITE_CONV [write'R_rwt]) 3198 THENC DATATYPE_CONV 3199 THENC REWRITE_CONV [alignmentTheory.aligned_numeric, 3200 alignmentTheory.aligned_add_sub_123] 3201 THENC utilsLib.INST_REWRITE_CONV 3202 [Aligned4_base_pc_plus, Aligned4_base_pc_minus]) o 3203 REWRITE_RULE (npc_thm [`t`, `t2`]) o 3204 FULL_DATATYPE_RULE o 3205 Conv.CONV_RULE (Conv.DEPTH_CONV (utilsLib.INST_REWRITE_CONV [write'R_rwt])) o 3206 DATATYPE_RULE o 3207 ASM_REWRITE_RULE [] 3208 3209val rule_literal2 = 3210 utilsLib.MATCH_HYP_CONV_RULE (REWRITE_CONV [Aligned_Align_plus_minus]) 3211 ``aligned n (w: word32)`` o 3212 utilsLib.INST_REWRITE_RULE [Align4_base_pc_plus, Align4_base_pc_minus] o 3213 utilsLib.ALL_HYP_CONV_RULE 3214 (Conv.DEPTH_CONV (utilsLib.INST_REWRITE_CONV [write'R_rwt]) 3215 THENC DATATYPE_CONV 3216 THENC REWRITE_CONV [alignmentTheory.aligned_numeric, 3217 alignmentTheory.aligned_add_sub_123]) o 3218 REWRITE_RULE (npc_thm [`t`, `t2`]) o 3219 FULL_DATATYPE_RULE o 3220 Conv.CONV_RULE (Conv.DEPTH_CONV (utilsLib.INST_REWRITE_CONV [write'R_rwt])) o 3221 ASM_REWRITE_RULE [] 3222 3223(* ---------------------------- *) 3224 3225val LoadWord_pc_rwt = 3226 List.map (fn wpc => 3227 memEV rule_pc MemU_4_rwt [dfn'LoadWord_def, wpc] 3228 [[``n <> 15w: word4``, ``r <> 15w: word4``]] addr1 3229 ``dfn'LoadWord (a, idx, wb, 15w, n, m)`` 3230 ) LoadWritePC_rwt 3231 |> List.concat 3232 3233val LoadWord_pc_pc_rwt = 3234 List.map (fn wpc => 3235 memEV rule_pc MemU_4_rwt [dfn'LoadWord_def, wpc] 3236 [[``r <> 15w: word4``]] bpc_addr1 3237 ``dfn'LoadWord (a, idx, wb, 15w, 15w, m)`` 3238 ) LoadWritePC_rwt 3239 |> List.concat 3240 3241val LoadWord_rwt = 3242 memEV (rule_npc true) MemU_4_rwt [dfn'LoadWord_def] 3243 [[``t <> 15w: word4``, ``n <> 15w: word4``, ``r <> 15w: word4``]] addr1 3244 ``dfn'LoadWord (a, idx, wb, t, n, m)`` 3245 3246val LoadWord_base_pc_rwt = 3247 memEV rule_base_pc MemU_4_rwt [dfn'LoadWord_def, ROR_rwt] 3248 [[``t <> 15w: word4``, ``r <> 15w: word4``]] bpc_addr1 3249 ``dfn'LoadWord (a, idx, wb, t, 15w, m)`` 3250 3251(* 3252val LoadLiteral_pc_rwt = 3253 memEV (K rule_literal_pc) MemU_4_rwt [dfn'LoadLiteral_def] [] (TF `a`) 3254 ``dfn'LoadLiteral (a, 15w, imm32)`` 3255*) 3256 3257val LoadLiteral_rwt = 3258 memEV rule_literal MemU_4_rwt [dfn'LoadLiteral_def] 3259 [[``t <> 15w: word4``]] (TF `a`) 3260 ``dfn'LoadLiteral (a, t, imm32)`` 3261 3262(* ---------------------------- *) 3263 3264val Extend_rwt = 3265 List.map (REWRITE_CONV [Extend_def]) 3266 [``Extend (T, w:'a word): 'b word``, 3267 ``Extend (F, w:'a word): 'b word``] 3268 3269val LoadByte_rwts = 3270 memEV (rule_npc false) MemU_1_rwt [dfn'LoadByte_def] 3271 [[``t <> 15w: word4``, ``n <> 15w: word4``, ``r <> 15w: word4``]] addr1 3272 ``dfn'LoadByte (u, a, idx, wb, t, n, m)`` 3273 3274val LoadByte_base_pc_rwts = 3275 memEV rule_base_pc MemU_1_rwt [dfn'LoadByte_def] 3276 [[``t <> 15w: word4``, ``r <> 15w: word4``]] bpc_addr1 3277 ``dfn'LoadByte (u, a, idx, wb, t, 15w, m)`` 3278 3279val LoadByteLiteral_rwt = 3280 memEV rule_literal MemU_1_rwt [dfn'LoadByteLiteral_def] 3281 [[``t <> 15w: word4``]] (TF `a`) 3282 ``dfn'LoadByteLiteral (u, a, t, imm32)`` 3283 3284val LoadSignedByte_rwts = 3285 memEV (rule_npc false) MemU_1_rwt (dfn'LoadByte_def :: Extend_rwt) 3286 [[``t <> 15w: word4``, ``n <> 15w: word4``, ``r <> 15w: word4``]] addr 3287 ``dfn'LoadByte 3288 (F, a, idx, wb, t, n, register_form1 (r, SRType_LSL, imm2))`` 3289 3290val LoadSignedByte_base_pc_rwts = 3291 memEV rule_base_pc MemU_1_rwt (dfn'LoadByte_def :: Extend_rwt) 3292 [[``t <> 15w: word4``, ``r <> 15w: word4``]] bpc_addr 3293 ``dfn'LoadByte 3294 (F, a, idx, wb, t, 15w, register_form1 (r, SRType_LSL, imm2))`` 3295 3296val LoadByteUnprivileged_rwts = 3297 memEV (rule_npc false) MemU_unpriv_1_rwt [dfn'LoadByteUnprivileged_def] 3298 [[``t <> 15w: word4``, ``n <> 15w: word4``, ``r <> 15w: word4``]] 3299 plain_addr1 3300 ``dfn'LoadByteUnprivileged (a, T, t, n, m)`` 3301 3302(* ---------------------------- *) 3303 3304val LoadHalf_rwts = 3305 memEV (rule_npc false) MemU_2_rwt [dfn'LoadHalf_def] 3306 [[``t <> 15w: word4``, ``n <> 15w: word4``, ``r <> 15w: word4``]] addr3 3307 ``dfn'LoadHalf (u, a, idx, wb, t, n, m)`` 3308 3309val LoadHalf_base_pc_rwts = 3310 memEV rule_base_pc MemU_2_rwt [dfn'LoadHalf_def] 3311 [[``t <> 15w: word4``, ``r <> 15w: word4``]] bpc_addr3 3312 ``dfn'LoadHalf (u, a, idx, wb, t, 15w, m)`` 3313 3314val LoadHalfLiteral_rwt = 3315 memEV rule_literal MemU_2_rwt [dfn'LoadHalfLiteral_def] 3316 [[``t <> 15w: word4``]] (TF `a`) 3317 ``dfn'LoadHalfLiteral (u, a, t, imm32)`` 3318 3319(* ---------------------------- *) 3320 3321val LoadDual_rwt = 3322 memEV rule_npc2 MemA_4_rwt [dfn'LoadDual_def] 3323 [[``t <> 15w: word4``, ``t2 <> 15w: word4``, 3324 ``n <> 15w: word4``, ``r <> 15w: word4``]] addr2 3325 ``dfn'LoadDual (a, idx, wb, t, t2, n, m)`` 3326 3327val LoadDual_base_pc_rwt = 3328 memEV rule_base_pc2 MemA_4_rwt [dfn'LoadDual_def] 3329 [[``t <> 15w: word4``, ``t2 <> 15w: word4``, ``r <> 15w: word4``]] 3330 bpc_addr2 3331 ``dfn'LoadDual (a, idx, wb, t, t2, 15w, m)`` 3332 3333val LoadDualLiteral_rwt = 3334 memEV rule_literal2 MemA_4_rwt [dfn'LoadDualLiteral_def] 3335 [[``t <> 15w: word4``, ``t2 <> 15w: word4``]] (TF `a`) 3336 ``dfn'LoadDualLiteral (a, t, t2, imm32)`` 3337 3338(* ---------------------------- *) 3339 3340val Shift_C_DecodeImmShift_rule = 3341 REWRITE_RULE [cond_rand_thms, FST_SWAP] o 3342 utilsLib.ALL_HYP_RULE 3343 (REWRITE_RULE [cond_rand_thms, FST_SWAP, Shift_C_DecodeImmShift_rwt]) 3344 3345val rule_npc = 3346 Shift_C_DecodeImmShift_rule o 3347 rule_sp o 3348 utilsLib.MATCH_HYP_CONV_RULE 3349 (utilsLib.INST_REWRITE_CONV [Aligned_plus_minus]) ``a \/ b \/ c : bool`` 3350 3351val rule_npc2 = 3352 FULL_DATATYPE_RULE o 3353 utilsLib.ALL_HYP_CONV_RULE 3354 (Conv.DEPTH_CONV (utilsLib.INST_REWRITE_CONV [R_rwt]) 3355 THENC DATATYPE_CONV 3356 THENC REWRITE_CONV [alignmentTheory.aligned_numeric, 3357 alignmentTheory.aligned_add_sub_123]) o 3358 rule_sp o 3359 utilsLib.MATCH_HYP_CONV_RULE 3360 (utilsLib.INST_REWRITE_CONV [Aligned_plus_minus]) ``a \/ b \/ c : bool`` o 3361 FULL_DATATYPE_RULE o 3362 Conv.CONV_RULE (Conv.DEPTH_CONV (utilsLib.INST_REWRITE_CONV [R_rwt])) 3363 3364(* ---------------------------- *) 3365 3366val () = resetEvConv () 3367 3368val StoreWord_rwt = 3369 storeEV rule_npc 3370 write'MemU_4_rwt [dfn'StoreWord_def] 3371 [[``Aligned (^st.REG (R_mode ^st.CPSR.M n), 4)``, 3372 ``Aligned (^st.REG (R_mode ^st.CPSR.M n) + 3373 FST (FST (Shift_C (^st.REG (R_mode ^st.CPSR.M r), 3374 FST (DecodeImmShift (v2w [b1; b0],imm5)), 3375 SND (DecodeImmShift (v2w [b1; b0],imm5)), 3376 ^st.CPSR.C) s)), 4)``, 3377 ``Aligned (^st.REG (R_mode ^st.CPSR.M n) - 3378 FST (FST (Shift_C (^st.REG (R_mode ^st.CPSR.M r), 3379 FST (DecodeImmShift (v2w [b1; b0],imm5)), 3380 SND (DecodeImmShift (v2w [b1; b0],imm5)), 3381 ^st.CPSR.C) s)), 4)``, 3382 ``Aligned (^st.REG (R_mode ^st.CPSR.M n) + imm32, 4)``, 3383 ``Aligned (^st.REG (R_mode ^st.CPSR.M n) - imm32, 4)``, 3384 ``n <> 15w: word4``, ``r <> 15w: word4``]] addr1 3385 ``dfn'StoreWord (a, idx, wb, t, n, m)`` 3386 3387val StoreWord_base_pc_rwt = 3388 storeEV (align_base_pc_rule o Shift_C_DecodeImmShift_rule) 3389 write'MemU_4_rwt [dfn'StoreWord_def] 3390 [[``Aligned (^st.REG RName_PC + (if ^st.CPSR.T then 4w else 8w) + 3391 FST (FST (Shift_C (^st.REG (R_mode ^st.CPSR.M r), 3392 FST (DecodeImmShift (v2w [b1; b0],imm5)), 3393 SND (DecodeImmShift (v2w [b1; b0],imm5)), 3394 ^st.CPSR.C) s)), 4)``, 3395 ``Aligned 3396 (^st.REG RName_PC + (if ^st.CPSR.T then 4w else 8w) + imm32, 4)``, 3397 ``Aligned (^st.REG RName_PC + (if ^st.CPSR.T then 4w else 8w) - 3398 FST (FST (Shift_C (^st.REG (R_mode ^st.CPSR.M r), 3399 FST (DecodeImmShift (v2w [b1; b0],imm5)), 3400 SND (DecodeImmShift (v2w [b1; b0],imm5)), 3401 ^st.CPSR.C) s)), 4)``, 3402 ``Aligned 3403 (^st.REG RName_PC + (if ^st.CPSR.T then 4w else 8w) - imm32, 4)``, 3404 ``r <> 15w: word4``]] bpc_addr1 3405 ``dfn'StoreWord (a, idx, wb, t, 15w, m)`` 3406 3407(* ---------------------------- *) 3408 3409val StoreByte_rwt = 3410 storeEV Lib.I write'MemU_1_rwt 3411 [dfn'StoreByte_def, Shift_C_DecodeImmShift_rwt] 3412 [[``n <> 15w: word4``, ``r <> 15w: word4``]] addr1 3413 ``dfn'StoreByte (a, idx, wb, t, n, m)`` 3414 3415val StoreByte_base_pc_rwt = 3416 storeEV Lib.I write'MemU_1_rwt 3417 [dfn'StoreByte_def, Shift_C_DecodeImmShift_rwt] 3418 [[``r <> 15w: word4``]] bpc_addr1 3419 ``dfn'StoreByte (a, idx, wb, t, 15w, m)`` 3420 3421(* ---------------------------- *) 3422 3423val extract_rwt = 3424 List.map utilsLib.EXTRACT_CONV [ 3425 ``(15 >< 8) ((15 >< 0) (w: word32) : word16) : word8``, 3426 ``(7 >< 0) ((15 >< 0) (w: word32) : word16) : word8`` 3427 ] |> Drule.LIST_CONJ 3428 3429val StoreHalf_rwt = 3430 storeEV Shift_C_DecodeImmShift_rule 3431 write'MemU_2_rwt [dfn'StoreHalf_def, extract_rwt] 3432 [[``Aligned (^st.REG (R_mode ^st.CPSR.M n),2)``, 3433 ``Aligned (^st.REG (R_mode ^st.CPSR.M n) + 3434 ^st.REG (R_mode ^st.CPSR.M r) << imm2, 2)``, 3435 ``Aligned (^st.REG (R_mode ^st.CPSR.M n) - 3436 ^st.REG (R_mode ^st.CPSR.M r) << imm2, 2)``, 3437 ``Aligned (^st.REG (R_mode ^st.CPSR.M n) + imm32, 2)``, 3438 ``Aligned (^st.REG (R_mode ^st.CPSR.M n) - imm32, 2)``, 3439 ``n <> 15w: word4``, ``r <> 15w: word4``]] addr3 3440 ``dfn'StoreHalf (a, idx, wb, t, n, m)`` 3441 3442val StoreHalf_base_pc_rwt = 3443 storeEV align_base_pc_rule 3444 write'MemU_2_rwt [dfn'StoreHalf_def, extract_rwt] 3445 [[``Aligned (^st.REG RName_PC + (if ^st.CPSR.T then 4w else 8w) + 3446 ^st.REG (R_mode ^st.CPSR.M r) << imm2, 2)``, 3447 ``Aligned 3448 (^st.REG RName_PC + (if ^st.CPSR.T then 4w else 8w) + imm32, 2)``, 3449 ``Aligned (^st.REG RName_PC + (if ^st.CPSR.T then 4w else 8w) - 3450 ^st.REG (R_mode ^st.CPSR.M r) << imm2, 2)``, 3451 ``Aligned 3452 (^st.REG RName_PC + (if ^st.CPSR.T then 4w else 8w) - imm32, 2)``, 3453 ``r <> 15w: word4``]] bpc_addr3 3454 ``dfn'StoreHalf (a, idx, wb, t, 15w, m)`` 3455 3456(* ---------------------------- *) 3457 3458val StoreDual_rwt = 3459 storeEV rule_npc2 3460 write'MemA_4_rwt [dfn'StoreDual_def, alignmentTheory.aligned_add_sub_123] 3461 [[``Aligned (^st.REG (R_mode ^st.CPSR.M n), 4)``, 3462 ``Aligned (^st.REG (R_mode ^st.CPSR.M n) + 3463 FST (FST (Shift_C (^st.REG (R_mode ^st.CPSR.M r), 3464 FST (DecodeImmShift (v2w [b1; b0],imm5)), 3465 SND (DecodeImmShift (v2w [b1; b0],imm5)), 3466 ^st.CPSR.C) s)), 4)``, 3467 ``Aligned (^st.REG (R_mode ^st.CPSR.M n) - 3468 FST (FST (Shift_C (^st.REG (R_mode ^st.CPSR.M r), 3469 FST (DecodeImmShift (v2w [b1; b0],imm5)), 3470 SND (DecodeImmShift (v2w [b1; b0],imm5)), 3471 ^st.CPSR.C) s)), 4)``, 3472 ``Aligned (^st.REG (R_mode ^st.CPSR.M n) + imm32, 4)``, 3473 ``Aligned (^st.REG (R_mode ^st.CPSR.M n) - imm32, 4)``, 3474 ``t <> 15w: word4``, ``t2 <> 15w: word4``, 3475 ``n <> 15w: word4``, ``r <> 15w: word4``]] addr2 3476 ``dfn'StoreDual (a, idx, wb, t, t2, n, m)`` 3477 3478(* ---------------------------- *) 3479 3480val Swap_rwts = 3481 EV ([R_rwt, write'R_rwt, Q.INST [`d` |-> `t`] arm_stepTheory.R_x_not_pc, 3482 dfn'Swap_def, IncPC_rwt, ROR_rwt, 3483 EVAL ``(a: word32) #>> (8 * w2n (0w: word2))``] @ 3484 MemA_1_rwt @ write'MemA_1_rwt @ MemA_4_rwt @ write'MemA_4_rwt) 3485 [[``^st.Encoding = Encoding_ARM``, ``~^st.CPSR.T``, 3486 ``t <> 15w: word4``, ``t2 <> 15w: word4``, ``n <> 15w: word4``]] 3487 (TF `b`) 3488 ``dfn'Swap (b, t, t2, n)`` 3489 |> List.map 3490 (utilsLib.ALL_HYP_RULE 3491 (PURE_ASM_REWRITE_RULE 3492 [boolTheory.COND_CLAUSES, boolTheory.NOT_CLAUSES, 3493 boolTheory.OR_CLAUSES]) o 3494 utilsLib.ALL_HYP_CONV_RULE 3495 (DATATYPE_CONV 3496 THENC REWRITE_CONV [boolTheory.COND_ID] 3497 THENC utilsLib.INST_REWRITE_CONV (MemA_1_rwt @ MemA_4_rwt) 3498 THENC DATATYPE_CONV)) 3499 |> addThms 3500 3501(* ---------------------------- *) 3502 3503(* Floating-point *) 3504 3505val fpscr_thm = Q.prove( 3506 `FPSCR a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 3507 a17 a18 a19 a20 a21 = 3508 ^st.FP.FPSCR with 3509 <|AHP := a0; C := a1; DN := a2; DZC := a3; DZE := a4; 3510 FZ := a5; IDC := a6; IDE := a7; IOC := a8; IOE := a9; 3511 IXC := a10; IXE := a11; N := a12; OFC := a13; OFE := a14; 3512 QC := a15; RMode := a16; UFC := a17; UFE := a18; V := a19; Z := a20; 3513 fpscr'rst := a21|>`, 3514 simp [FPSCR_component_equality]) 3515 3516val mov_two_singles = 3517 List.map (blastLib.BBLAST_PROVE o Term) 3518 [`(v2w [b9; b8; b7; b6; F] + 1w) // 2w = v2w [F; b9; b8; b7; b6] : word5`, 3519 `word_bit 0 (v2w [b9; b8; b7; b6; F] + 1w : word5)`, 3520 `~word_bit 0 (v2w [b9; b8; b7; b6; T] + 1w : word5)`, 3521 `v2w [F; b9; b8; b7; b6] <> (v2w [b9; b8; b7; b6; T] + 1w) // 2w : word5`, 3522 `bit_field_insert 63 32 (a : word32) 3523 (bit_field_insert 31 0 (b : word32) (c : word64)) = a @@ b`] 3524 |> Drule.LIST_CONJ 3525 3526val UnsignedSatQ_32_rwt = 3527 EV [UnsignedSatQ_def, wordsTheory.word_len_def, wordsTheory.dimindex_32, 3528 EVAL ``i2w 4294967295 : word32``] [] [] 3529 ``UnsignedSatQ (i, 32) : arm_state -> (word32 # bool) # arm_state`` 3530 |> hd 3531 3532val SignedSatQ_32_rwt = 3533 EV [SignedSatQ_def, wordsTheory.word_len_def, wordsTheory.dimindex_32, 3534 EVAL ``2147483648i - 1i``, EVAL ``i2w 2147483647i : word32``, 3535 EVAL ``i2w (-2147483648i) : word32``] [] [] 3536 ``SignedSatQ (i, 32) : arm_state -> (word32 # bool) # arm_state`` 3537 |> hd 3538 3539val ev = 3540 EV [FPToFixed32_def, FPToFixed64_def, RoundingMode, 3541 UnsignedSatQ_32_rwt, SignedSatQ_32_rwt, SatQ_def, 3542 intLib.ARITH_PROVE ``i > 4294967295i = ~(i <= 4294967295i)``, 3543 intLib.ARITH_PROVE ``i > 2147483647i = ~(i <= 2147483647i)``, 3544 intLib.ARITH_PROVE ``i < -2147483648i = ~(-2147483648i <= i)``, 3545 intLib.ARITH_PROVE ``i < 0i = ~(0i <= i)`` 3546 ] 3547 [[``fp32_to_int 3548 (if round_towards_zero then roundTowardZero 3549 else DecodeRoundingMode s.FP.FPSCR.RMode) operand = SOME i``, 3550 ``fp64_to_int 3551 (if round_towards_zero then roundTowardZero 3552 else DecodeRoundingMode s.FP.FPSCR.RMode) operand = SOME i``, 3553 ``0i <= i``, ``i <= 4294967295i``, 3554 ``-2147483648i <= i``, ``i <= 2147483647i``]] 3555 (TF `unsigned`) 3556 3557val (FPToFixed32_unsigned_rwt, FPToFixed32_signed_rwt) = 3558 ev ``FPToFixed32 (operand,unsigned,round_towards_zero)`` 3559 |> Lib.pair_of_list 3560 3561val (FPToFixed64_unsigned_rwt, FPToFixed64_signed_rwt) = 3562 ev ``FPToFixed64 (operand,unsigned,round_towards_zero)`` 3563 |> Lib.pair_of_list 3564 3565val rule = utilsLib.INST_REWRITE_RULE 3566 [arm_stepTheory.Align4_base_pc_plus, 3567 arm_stepTheory.Align4_base_pc_minus] o 3568 SIMP_RULE std_ss [] o 3569 REWRITE_RULE 3570 [GSYM arm_stepTheory.UpdateSingleOfDouble_def, 3571 GSYM arm_stepTheory.SingleOfDouble_def] o 3572 SIMP_RULE (pure_ss++wordsLib.SIZES_ss) 3573 [wordsTheory.WORD_EXTRACT_COMP_THM] o 3574 COND_UPDATE_RULE 3575 3576fun fpMemEV c tm = 3577 EV ([dfn'vldr_def, dfn'vstr_def, R_rwt, IncPC_rwt, PC_rwt, fpreg_div2, 3578 write'S_def, write'D_def, S_def, D_def, BigEndian_def] @ 3579 MemA_4_rwt @ write'MemA_4_rwt) c 3580 [[`single_reg` |-> boolSyntax.F, `add` |-> boolSyntax.F], 3581 [`single_reg` |-> boolSyntax.F, `add` |-> boolSyntax.T], 3582 [`single_reg` |-> boolSyntax.T, `add` |-> boolSyntax.F], 3583 [`single_reg` |-> boolSyntax.T, `add` |-> boolSyntax.T]] 3584 tm 3585 |> List.map (utilsLib.ALL_HYP_CONV_RULE 3586 (DATATYPE_CONV 3587 THENC REWRITE_CONV 3588 [arm_stepTheory.Aligned_Align_plus_minus, 3589 alignmentTheory.aligned_add_sub_123, 3590 alignmentTheory.aligned_numeric]) o rule) 3591 3592fun fpEV c tm = 3593 EV [dfn'vadd_def, dfn'vsub_def, dfn'vmul_def, dfn'vneg_mul_def, 3594 dfn'vmla_vmls_def, dfn'vfma_vfms_def, dfn'vfnma_vfnms_def, 3595 dfn'vdiv_def, dfn'vabs_def, dfn'vneg_def, dfn'vsqrt_def, 3596 dfn'vmov_imm_def, dfn'vmov_def, dfn'vmov_single_def, 3597 dfn'vmov_two_singles_def, dfn'vmov_double_def, dfn'vcmp_def, 3598 dfn'vcvt_float_def, dfn'vcvt_to_integer_def, dfn'vcvt_from_integer_def, 3599 IncPC_rwt, S_def, D_def, write'S_def, write'D_def, 3600 FPAdd64_def, FPAdd32_def, FPSub64_def, FPSub32_def, fpreg_div2, 3601 FPMul64_def, FPMul32_def, FPZero64_def, FPZero32_def, 3602 FixedToFP32_def, FixedToFP64_def, 3603 FPToFixed32_signed_rwt, FPToFixed32_unsigned_rwt, 3604 FPToFixed64_signed_rwt, FPToFixed64_unsigned_rwt, 3605 R_rwt, write'R_rwt, arm_stepTheory.R_x_not_pc, 3606 write'reg'FPSCR_def, fpscr_nzcv, 3607 arm_stepTheory.RoundingMode, arm_stepTheory.get_vfp_imm32, 3608 wordsTheory.word_concat_0_0, mov_two_singles, updateTheory.UPDATE_EQ] 3609 [[``^st.Encoding = Encoding_ARM``, ``~^st.CPSR.T``]] c tm 3610 |> List.map rule 3611 3612val mk_fpreg = bitstringSyntax.mk_vec 5 3613val () = setEvConv (Conv.DEPTH_CONV bitstringLib.word_bit_CONV) 3614 3615val vmov_rwt = 3616 fpEV (TF `single`) 3617 ``dfn'vmov (single, ^(mk_fpreg 0), ^(mk_fpreg 5))`` 3618 |> addThms 3619 3620val vmov_imm_rwt = 3621 fpEV [[`single` |-> boolSyntax.F], 3622 [`single` |-> boolSyntax.T, 3623 `imm64` |-> bitstringSyntax.mk_v2w 3624 (bitstringSyntax.mk_bstring 32 5, ``:64``)]] 3625 ``dfn'vmov_imm (single, ^(mk_fpreg 0), imm64)`` 3626 |> addThms 3627 3628val vmov_single_rwt = 3629 fpEV (TF `to_arm_register`) 3630 ``dfn'vmov_single (to_arm_register, t, ^(mk_fpreg 5))`` 3631 |> addThms 3632 3633val vmov_two_singles_rwt = 3634 fpEV [[`to_arm_registers` |-> boolSyntax.F, `b5` |-> boolSyntax.F], 3635 [`to_arm_registers` |-> boolSyntax.T, `b5` |-> boolSyntax.F], 3636 [`to_arm_registers` |-> boolSyntax.F, `b5` |-> boolSyntax.T], 3637 [`to_arm_registers` |-> boolSyntax.T, `b5` |-> boolSyntax.T]] 3638 ``dfn'vmov_two_singles (to_arm_registers, t, t2, ^(mk_fpreg 5))`` 3639 |> List.map (utilsLib.ALL_HYP_CONV_RULE 3640 (DATATYPE_CONV THENC REWRITE_CONV [ASSUME ``~^st.CPSR.T``]) o 3641 DATATYPE_RULE) 3642 |> addThms 3643 3644val vmov_double_rwt = 3645 fpEV (TF `to_arm_registers`) 3646 ``dfn'vmov_double (to_arm_registers, t, t2, ^(mk_fpreg 5))`` 3647 |> List.map (utilsLib.ALL_HYP_CONV_RULE 3648 (DATATYPE_CONV THENC REWRITE_CONV [ASSUME ``~^st.CPSR.T``])) 3649 |> addThms 3650 3651val vcmp_rwt = 3652 fpEV [[`dp` |-> boolSyntax.F, `m_w_z` |-> ``NONE:word5 option``], 3653 [`dp` |-> boolSyntax.T, `m_w_z` |-> ``NONE:word5 option``], 3654 [`dp` |-> boolSyntax.F, `m_w_z` |-> ``SOME (^(mk_fpreg 5))``], 3655 [`dp` |-> boolSyntax.T, `m_w_z` |-> ``SOME (^(mk_fpreg 5))``]] 3656 ``dfn'vcmp (dp, ^(mk_fpreg 0), m_w_z)`` 3657 |> addThms 3658 3659val vmrs_rwt = 3660 EV [dfn'vmrs_def, IncPC_rwt, R_rwt, write'R_rwt, reg_fpscr] 3661 [[``t <> 15w: word4``]] [] 3662 ``dfn'vmrs t`` 3663 |> List.map (utilsLib.MATCH_HYP_CONV_RULE 3664 (REWRITE_CONV [ASSUME ``~^st.CPSR.T``]) 3665 ``a \/ b \/ c : bool``) 3666 |> addThms 3667 3668val vmrs15_rwt = 3669 EV [dfn'vmrs_def, IncPC_rwt] [] [] 3670 ``dfn'vmrs 15w`` 3671 |> addThms 3672 3673val vmsr_rwt = 3674 EV [dfn'vmsr_def, IncPC_rwt, R_rwt, write'reg'FPSCR_def, 3675 REWRITE_RULE [fpscr_thm] rec'FPSCR_def] [[``~^st.CPSR.T``]] [] 3676 ``dfn'vmsr t`` 3677 |> addThms 3678 3679val vabs_rwt = 3680 fpEV (TF `dp`) 3681 ``dfn'vabs (dp, ^(mk_fpreg 0), ^(mk_fpreg 5))`` 3682 |> addThms 3683 3684val vneg_rwt = 3685 fpEV (TF `dp`) 3686 ``dfn'vneg (dp, ^(mk_fpreg 0), ^(mk_fpreg 5))`` 3687 |> addThms 3688 3689val vsqrt_rwt = 3690 fpEV (TF `dp`) 3691 ``dfn'vsqrt (dp, ^(mk_fpreg 0), ^(mk_fpreg 5))`` 3692 |> addThms 3693 3694val vadd_rwt = 3695 fpEV (TF `dp`) 3696 ``dfn'vadd (dp, ^(mk_fpreg 0), ^(mk_fpreg 5), ^(mk_fpreg 10))`` 3697 |> addThms 3698 3699val vsub_rwt = 3700 fpEV (TF `dp`) 3701 ``dfn'vsub (dp, ^(mk_fpreg 0), ^(mk_fpreg 5), ^(mk_fpreg 10))`` 3702 |> addThms 3703 3704val vmul_rwt = 3705 fpEV (TF `dp`) 3706 ``dfn'vmul (dp, ^(mk_fpreg 0), ^(mk_fpreg 5), ^(mk_fpreg 10))`` 3707 |> addThms 3708 3709val vdiv_rwt = 3710 fpEV (TF `dp`) 3711 ``dfn'vdiv (dp, ^(mk_fpreg 0), ^(mk_fpreg 5), ^(mk_fpreg 10))`` 3712 |> addThms 3713 3714val vfma_vfms_rwt = 3715 fpEV (TF `dp`) 3716 ``dfn'vfma_vfms (dp, add, ^(mk_fpreg 0), ^(mk_fpreg 5), ^(mk_fpreg 10))`` 3717 |> addThms 3718 3719val vfnma_vfnms_rwt = 3720 fpEV (TF `dp`) 3721 ``dfn'vfnma_vfnms (dp, add, ^(mk_fpreg 0), ^(mk_fpreg 5), ^(mk_fpreg 10))`` 3722 |> addThms 3723 3724val vmla_mls_rwt = 3725 fpEV [[`dp` |-> boolSyntax.F, `add` |-> boolSyntax.F], 3726 [`dp` |-> boolSyntax.F, `add` |-> boolSyntax.T], 3727 [`dp` |-> boolSyntax.T, `add` |-> boolSyntax.F], 3728 [`dp` |-> boolSyntax.T, `add` |-> boolSyntax.T]] 3729 ``dfn'vmla_vmls (dp, add, ^(mk_fpreg 0), ^(mk_fpreg 5), ^(mk_fpreg 10))`` 3730 |> addThms 3731 3732val vneg_mul_rwt = 3733 fpEV [[`dp` |-> boolSyntax.T, `typ` |-> ``VFPNegMul_VNMLA``], 3734 [`dp` |-> boolSyntax.F, `typ` |-> ``VFPNegMul_VNMLA``], 3735 [`dp` |-> boolSyntax.T, `typ` |-> ``VFPNegMul_VNMLS``], 3736 [`dp` |-> boolSyntax.F, `typ` |-> ``VFPNegMul_VNMLS``], 3737 [`dp` |-> boolSyntax.T, `typ` |-> ``VFPNegMul_VNMUL``], 3738 [`dp` |-> boolSyntax.F, `typ` |-> ``VFPNegMul_VNMUL``]] 3739 ``dfn'vneg_mul (dp, typ, ^(mk_fpreg 0), ^(mk_fpreg 5), ^(mk_fpreg 10))`` 3740 |> addThms 3741 3742val vcvt_float_rwt = 3743 fpEV [[`double_to_single` |-> boolSyntax.F, `b4` |-> boolSyntax.F], 3744 [`double_to_single` |-> boolSyntax.F, `b4` |-> boolSyntax.T], 3745 [`double_to_single` |-> boolSyntax.T]] 3746 ``dfn'vcvt_float (double_to_single, ^(mk_fpreg 0), ^(mk_fpreg 5))`` 3747 |> addThms 3748 3749val vcvt_from_integer_rwt = 3750 fpEV [[`dp` |-> boolSyntax.T, `b4` |-> boolSyntax.F], 3751 [`dp` |-> boolSyntax.T, `b4` |-> boolSyntax.T], 3752 [`dp` |-> boolSyntax.F]] 3753 ``dfn'vcvt_from_integer (dp, unsigned, ^(mk_fpreg 0), ^(mk_fpreg 5))`` 3754 |> addThms 3755 3756val vcvt_to_integer_rwt = 3757 fpEV [[`dp` |-> boolSyntax.F, `unsigned` |-> boolSyntax.F], 3758 [`dp` |-> boolSyntax.F, `unsigned` |-> boolSyntax.T], 3759 [`dp` |-> boolSyntax.T, `unsigned` |-> boolSyntax.F], 3760 [`dp` |-> boolSyntax.T, `unsigned` |-> boolSyntax.T]] 3761 ``dfn'vcvt_to_integer 3762 (dp, unsigned, round_zero, ^(mk_fpreg 0), ^(mk_fpreg 5))`` 3763 |> addThms 3764 3765val vldr_pc_rwt = 3766 fpMemEV [] ``dfn'vldr (single_reg, add, ^(mk_fpreg 0), 15w, imm32)`` 3767 |> addThms 3768 3769val vldr_npc_rwt = 3770 fpMemEV [[``n <> 15w: word4``]] 3771 ``dfn'vldr (single_reg, add, ^(mk_fpreg 0), n, imm32)`` 3772 |> addThms 3773 3774val vstr_pc_rwt = 3775 fpMemEV [] ``dfn'vstr (single_reg, add, ^(mk_fpreg 0), 15w, imm32)`` 3776 |> addThms 3777 3778val vstr_npc_rwt = 3779 fpMemEV [[``n <> 15w: word4``]] 3780 ``dfn'vstr (single_reg, add, ^(mk_fpreg 0), n, imm32)`` 3781 |> addThms 3782 3783val () = resetEvConv () 3784 3785(* ---------------------------- *) 3786 3787val COND_B_CONV = Conv.RATOR_CONV o Conv.RATOR_CONV o Conv.RAND_CONV 3788val COND_T_CONV = Conv.RATOR_CONV o Conv.RAND_CONV 3789val COND_E_CONV = Conv.RAND_CONV 3790 3791fun COND_UPDATE2_CONV l = 3792 COND_UPDATE_CONV 3793 THENC DATATYPE_CONV 3794 THENC COND_UPDATE_CONV 3795 THENC SIMP_CONV (srw_ss()) l 3796 3797val PSR_CONV = utilsLib.BIT_FIELD_INSERT_CONV "arm" "PSR" 3798val PSR_TAC = utilsLib.REC_REG_BIT_FIELD_INSERT_TAC "arm" "PSR" 3799 3800val PSR_FIELDS = Q.prove( 3801 `(!p v. 3802 rec'PSR (bit_field_insert 31 27 (v: word5) (reg'PSR p)) = 3803 p with <|N := v ' 4; Z := v ' 3; C := v ' 2; V := v ' 1; Q := v ' 0|>) /\ 3804 (!p v. 3805 rec'PSR (bit_field_insert 26 24 (v: word3) (reg'PSR p)) = 3806 p with <|IT := bit_field_insert 1 0 ((2 >< 1) v: word2) p.IT; 3807 J := v ' 0|>) /\ 3808 (!p v. 3809 rec'PSR (bit_field_insert 19 16 (v: word4) (reg'PSR p)) = 3810 p with <|GE := v|>) /\ 3811 (!p v. 3812 rec'PSR (bit_field_insert 15 10 (v: word6) (reg'PSR p)) = 3813 p with <|IT := bit_field_insert 7 2 v p.IT|>) /\ 3814 (!p v. 3815 rec'PSR (bit_field_insert 4 0 (v: word5) (reg'PSR p)) = 3816 p with <|M := bit_field_insert 4 0 v p.M|>)`, 3817 REPEAT CONJ_TAC \\ PSR_TAC `p`) 3818 3819val PSR_FLAGS = Q.prove( 3820 `(!b p v. 3821 rec'PSR (bit_field_insert 9 9 (v2w [b]: word1) (reg'PSR p)) = 3822 p with <|E := b|>) /\ 3823 (!b p v. 3824 rec'PSR (bit_field_insert 8 8 (v2w [b]: word1) (reg'PSR p)) = 3825 p with <|A := b|>) /\ 3826 (!b p v. 3827 rec'PSR (bit_field_insert 7 7 (v2w [b]: word1) (reg'PSR p)) = 3828 p with <|I := b|>) /\ 3829 (!b p v. 3830 rec'PSR (bit_field_insert 6 6 (v2w [b]: word1) (reg'PSR p)) = 3831 p with <|F := b|>) /\ 3832 (!b p v. 3833 rec'PSR (bit_field_insert 5 5 (v2w [b]: word1) (reg'PSR p)) = 3834 p with <|T := b|>)`, 3835 REPEAT CONJ_TAC \\ Cases \\ PSR_TAC `p`) 3836 3837val IT_extract = 3838 utilsLib.map_conv utilsLib.EXTRACT_CONV 3839 [``(2 >< 1) ((26 >< 24) (v: word32) : word3) : word2``, 3840 ``w2w ((15 >< 10) (w: word32) : word6) : word8``, 3841 ``w2w ((26 >< 25) (w: word32) : word2) : word8``] 3842 3843val IT_concat = Q.prove( 3844 `(!v: word6 w: word8. 3845 bit_field_insert 7 2 v w = w2w v << 2 || (w && 0b11w)) /\ 3846 (!v: word2 w: word8. 3847 bit_field_insert 1 0 v w = w2w v || (w && 0b11111100w)) /\ 3848 (!v1: word6 v2: word2 w: word8. 3849 bit_field_insert 7 2 v1 (bit_field_insert 1 0 v2 w) = v1 @@ v2)`, 3850 REPEAT strip_tac 3851 \\ rewrite_tac [wordsTheory.bit_field_insert_def] 3852 \\ blastLib.BBLAST_TAC) 3853 3854val insert_mode = Q.prove( 3855 `!w: word32. 3856 bit_field_insert 4 0 ((4 >< 0) w : word5) (v: word5) = (4 >< 0) w`, 3857 blastLib.BBLAST_TAC) 3858 3859val CPSRWriteByInstr = 3860 CPSRWriteByInstr_def 3861 |> Q.SPECL [`value`, `bytemask`, `is_exc_return`] 3862 |> (fn th => Thm.AP_THM th st) 3863 |> Conv.RIGHT_CONV_RULE 3864 (Thm.BETA_CONV 3865 THENC REWRITE_CONV 3866 [write'reg'PSR_def, CurrentModeIsNotUser_def, 3867 PSR_FIELDS, PSR_FLAGS] 3868 THENC Conv.RAND_CONV 3869 (Thm.BETA_CONV 3870 THENC PairedLambda.let_CONV 3871 THENC utilsLib.INST_REWRITE_CONV [BadMode] 3872 THENC REWRITE_CONV [] 3873 ) 3874 THENC PairedLambda.let_CONV 3875 THENC REWRITE_CONV [] 3876 THENC Conv.RAND_CONV 3877 (COND_T_CONV PairedLambda.let_CONV 3878 THENC PSR_CONV 3879 ) 3880 THENC PairedLambda.let_CONV 3881 THENC Conv.RAND_CONV 3882 (PSR_CONV 3883 THENC COND_UPDATE2_CONV [IT_extract] 3884 ) 3885 THENC PairedLambda.let_CONV 3886 THENC Conv.RAND_CONV 3887 (PSR_CONV 3888 THENC COND_T_CONV 3889 (PairedLambda.let_CONV 3890 THENC RAND_CONV DATATYPE_CONV 3891 THENC PairedLambda.let_CONV 3892 THENC DATATYPE_CONV 3893 THENC utilsLib.INST_REWRITE_CONV [IsSecure] 3894 THENC SIMP_CONV (srw_ss()) [PSR_FLAGS] 3895 ) 3896 THENC COND_UPDATE2_CONV 3897 [addressTheory.IF_IF, 3898 Q.SPEC `bytemask ' 3` CONJ_COMM] 3899 ) 3900 THENC PairedLambda.let_CONV 3901 THENC COND_T_CONV 3902 (Conv.RAND_CONV 3903 (REWRITE_CONV [PSR_FLAGS] 3904 THENC COND_UPDATE2_CONV []) 3905 THENC PairedLambda.let_CONV 3906 THENC DATATYPE_CONV 3907 THENC utilsLib.INST_REWRITE_CONV [IsSecure] 3908 THENC REWRITE_CONV [] 3909 THENC Conv.RAND_CONV 3910 (DATATYPE_CONV 3911 THENC REWRITE_CONV [PSR_FLAGS] 3912 THENC COND_UPDATE2_CONV [] 3913 ) 3914 THENC PairedLambda.let_CONV 3915 THENC Conv.RAND_CONV (COND_UPDATE2_CONV []) 3916 THENC PairedLambda.let_CONV) 3917 THENC REWRITE_CONV [PSR_FIELDS, addressTheory.IF_IF, IT_extract] 3918 THENC Conv.DEPTH_CONV (wordsLib.WORD_BIT_INDEX_CONV true)) 3919 |> utilsLib.ALL_HYP_CONV_RULE 3920 (DATATYPE_CONV THENC REWRITE_CONV [boolTheory.COND_ID]) 3921 3922val CPSRWriteByInstr_no_control = 3923 REWRITE_RULE [ASSUME ``~((bytemask: word4) ' 0)``] CPSRWriteByInstr 3924 3925val CPSRWriteByInstr_control_usr = 3926 REWRITE_RULE [ASSUME ``(bytemask: word4) ' 0``, 3927 ASSUME ``^st.CPSR.M = 16w``] CPSRWriteByInstr 3928 3929val CPSRWriteByInstr_control_not_usr = 3930 CPSRWriteByInstr 3931 |> Conv.RIGHT_CONV_RULE 3932 (REWRITE_CONV [ASSUME ``(bytemask: word4) ' 0``, 3933 ASSUME ``^st.CPSR.M <> 16w``] 3934 THENC utilsLib.INST_REWRITE_CONV [BadMode] 3935 THENC REWRITE_CONV [] 3936 THENC utilsLib.INST_REWRITE_CONV [IsSecure] 3937 THENC REWRITE_CONV [] 3938 THENC Conv.RAND_CONV PairedLambda.let_CONV 3939 THENC PairedLambda.let_CONV 3940 THENC REWRITE_CONV [] 3941 THENC PairedLambda.let_CONV 3942 THENC utilsLib.INST_REWRITE_CONV [IsSecure] 3943 THENC REWRITE_CONV [] 3944 THENC Conv.RAND_CONV PairedLambda.let_CONV 3945 THENC PairedLambda.let_CONV 3946 THENC RAND_CONV DATATYPE_CONV 3947 THENC utilsLib.INST_REWRITE_CONV [NotHyp] 3948 THENC REWRITE_CONV [] 3949 THENC PairedLambda.let_CONV 3950 THENC utilsLib.INST_REWRITE_CONV [NotHyp] 3951 THENC REWRITE_CONV [] 3952 THENC PairedLambda.let_CONV 3953 THENC DATATYPE_CONV 3954 THENC REWRITE_CONV [PSR_FIELDS]) 3955 |> utilsLib.ALL_HYP_CONV_RULE DATATYPE_CONV 3956 3957val CPSRWriteByInstr_exn_return = 3958 CPSRWriteByInstr_control_not_usr 3959 |> Q.INST [`bytemask` |-> `0b1111w`, `is_exc_return` |-> `T`] 3960 |> Conv.CONV_RULE (Conv.RHS_CONV utilsLib.WGROUND_CONV 3961 THENC REWRITE_CONV [IT_concat, insert_mode]) 3962 |> utilsLib.ALL_HYP_CONV_RULE (REWRITE_CONV [EVAL ``15w: word4 ' 0``]) 3963 3964(* Partial support for PSR updates, e.g. RFE, MRS, MSR) *) 3965 3966fun rule tm = REWRITE_RULE [] o utilsLib.INST_REWRITE_RULE [ASSUME tm] 3967val tm = bitstringSyntax.mk_vec 4 0 3968val thms = 3969 List.tabulate 3970 (4, fn i => EVAL (fcpSyntax.mk_fcp_index (tm, numLib.term_of_int i))) 3971 3972fun is_j tm = 3973 case Lib.total fcpSyntax.dest_fcp_index tm of 3974 SOME (_, i) => i = numLib.term_of_int 24 3975 | NONE => false 3976 3977fun unset_j_conv tm = 3978 let 3979 val t = HolKernel.find_term is_j tm 3980 in 3981 PURE_REWRITE_CONV [ASSUME (boolSyntax.mk_neg t)] tm 3982 end 3983 3984val ReturnFromException_le_rwts = 3985 EV [dfn'ReturnFromException_def, CurrentModeIsHyp, 3986 CurrentModeIsNotUser_def, BadMode, pairTheory.FST, CurrentInstrSet_rwt, 3987 CPSRWriteByInstr_exn_return, NotHyp, List.last BranchWritePC_rwt, 3988 rule ``~^st.CPSR.E`` (hd MemA_4_rwt), 3989 rule ``n <> 15w: word4`` R_rwt, write'R_rwt, 3990 arm_stepTheory.Align_LoadWritePC, 3991 wordsTheory.WORD_SUB_ADD, wordsTheory.WORD_ADD_SUB, 3992 simpLib.SIMP_PROVE (srw_ss()) [] 3993 ``(!w: word32. w + 4w + 4w = w + 8w) /\ 3994 (!w: word32. w - 8w + 4w = w - 4w)``] 3995 [[``^st.CPSR.M <> 16w``]] 3996 [[`inc` |-> ``F``, `wordhigher` |-> ``F``, `wback` |-> ``T``], 3997 [`inc` |-> ``F``, `wordhigher` |-> ``T``, `wback` |-> ``T``], 3998 [`inc` |-> ``T``, `wordhigher` |-> ``F``, `wback` |-> ``T``], 3999 [`inc` |-> ``T``, `wordhigher` |-> ``T``, `wback` |-> ``T``], 4000 [`inc` |-> ``F``, `wordhigher` |-> ``F``, `wback` |-> ``F``], 4001 [`inc` |-> ``F``, `wordhigher` |-> ``T``, `wback` |-> ``F``], 4002 [`inc` |-> ``T``, `wordhigher` |-> ``F``, `wback` |-> ``F``], 4003 [`inc` |-> ``T``, `wordhigher` |-> ``T``, `wback` |-> ``F``]] 4004 ``dfn'ReturnFromException (inc, wordhigher, wback, n)`` 4005 |> List.map (Conv.CONV_RULE unset_j_conv o 4006 utilsLib.ALL_HYP_CONV_RULE 4007 (DATATYPE_CONV 4008 THENC REWRITE_CONV 4009 [alignmentTheory.aligned_add_sub_123, 4010 alignmentTheory.aligned_numeric, 4011 ASSUME ``^st.CPSR.M <> 16w``])) 4012 |> addThms 4013 4014val CPSR_lem = Q.prove( 4015 `GoodMode m ==> m <> 16w ==> m <> 31w ==> 4016 ((if m = 17w then (a, s) 4017 else if m = 18w then (b, s) 4018 else if m = 19w then (c, s) 4019 else if m = 22w then (d, s) 4020 else if m = 23w then (e, s) 4021 else if m = 26w then (f, s) 4022 else if m = 27w then (g, s) 4023 else h) = 4024 (if m = 17w then a 4025 else if m = 18w then b 4026 else if m = 19w then c 4027 else if m = 22w then d 4028 else if m = 23w then e 4029 else if m = 26w then f 4030 else g, s))`, 4031 rw [GoodMode_def] 4032 ) |> UNDISCH_ALL 4033 4034val CPSR_it = Q.prove( 4035 `((if m = 17w : word5 then (7 >< 2) a.IT : word6 4036 else if m = 18w then (7 >< 2) b.IT 4037 else if m = 19w then (7 >< 2) c.IT 4038 else if m = 22w then (7 >< 2) d.IT 4039 else if m = 23w then (7 >< 2) e.IT 4040 else if m = 26w then (7 >< 2) f.IT 4041 else (7 >< 2) g.IT) @@ 4042 (if m = 17w then (1 >< 0) a.IT : word2 4043 else if m = 18w then (1 >< 0) b.IT 4044 else if m = 19w then (1 >< 0) c.IT 4045 else if m = 22w then (1 >< 0) d.IT 4046 else if m = 23w then (1 >< 0) e.IT 4047 else if m = 26w then (1 >< 0) f.IT 4048 else (1 >< 0) g.IT)) = 4049 (if m = 17w then a 4050 else if m = 18w then b 4051 else if m = 19w then c 4052 else if m = 22w then d 4053 else if m = 23w then e 4054 else if m = 26w then f 4055 else g).IT`, 4056 rw [] \\ fs [] \\ blastLib.BBLAST_TAC) 4057 4058val SPSR_rwt = EV [SPSR_def, BadMode, CPSR_lem] [] [] ``SPSR`` |> hd 4059 4060val reg'PSR = utilsLib.mk_reg_thm "arm" "PSR" 4061 4062local 4063 val l = 4064 reg'PSR 4065 |> SPEC_ALL 4066 |> utilsLib.rhsc 4067 |> HolKernel.strip_binop (Lib.total wordsSyntax.dest_word_concat) 4068 fun mk_v n a = Term.mk_var ("v" ^ Int.toString n, Term.type_of a) 4069 val tm = 4070 List.foldr 4071 (fn (t, (a, n)) => (wordsSyntax.mk_word_concat (mk_v n t, a), n + 1)) 4072 (mk_v 0 (List.last l), 1) (Lib.butlast l) |> fst 4073in 4074 val bits2625 = blastLib.BBLAST_PROVE ``(26 >< 25) ^tm = v10`` 4075 val bits1916 = blastLib.BBLAST_PROVE ``(19 >< 16) ^tm = v7`` 4076 val bits1510 = blastLib.BBLAST_PROVE ``(15 >< 10) ^tm = v6`` 4077 val bits40 = blastLib.BBLAST_PROVE ``(4 >< 0) ^tm = v0`` 4078 val bit0_word1 = blastLib.BBLAST_CONV ``(v2w [b] : word1) ' 0`` 4079end 4080 4081val concat_bit_lo = Q.prove( 4082 `n < dimindex(:'b) /\ n < dimindex(:'c) /\ 4083 FINITE (univ(:'a)) /\ FINITE (univ(:'b)) ==> 4084 ((((a : 'a word) @@ (b : 'b word)) : 'c word) ' n = b ' n)`, 4085 srw_tac [wordsLib.WORD_BIT_EQ_ss] [fcpTheory.index_sum] 4086 ) 4087 4088val concat_bit_hi = Q.prove( 4089 `dimindex(:'b) <= n /\ n < dimindex(:'c) /\ 4090 n < dimindex(:'a) + dimindex (:'b) /\ 4091 FINITE (univ(:'a)) /\ FINITE (univ(:'b)) ==> 4092 ((((a : 'a word) @@ (b : 'b word)) : 'c word) ' n = 4093 a ' (n - dimindex(:'b)))`, 4094 srw_tac [wordsLib.WORD_BIT_EQ_ss] [fcpTheory.index_sum] 4095 ) 4096 4097val SUBS_PC_rwt = 4098 EV [dfn'ArithLogicImmediate_def, utilsLib.SET_RULE DataProcessingPC_def, 4099 utilsLib.SET_RULE CurrentModeIsUserOrSystem_def, CurrentModeIsHyp, 4100 BadMode, CurrentInstrSet_rwt, ARMExpandImm_C_rwt, ExpandImm_C_rwt, 4101 R_rwt, DataProcessingALU_def, SPSR_rwt, CPSRWriteByInstr_exn_return, 4102 AddWithCarry, wordsTheory.FST_ADD_WITH_CARRY, reg'PSR, 4103 hd (tl BranchWritePC_rwt)] 4104 [[``^st.CPSR.M <> 16w``, ``^st.CPSR.M <> 31w``]] [] 4105 ``dfn'ArithLogicImmediate 4106 (2w, T, 15w, n, ^(bitstringSyntax.mk_vec 12 0))`` 4107 |> List.map (utilsLib.FULL_CONV_RULE 4108 (DATATYPE_CONV 4109 THENC SIMP_CONV (std_ss++wordsLib.SIZES_ss) 4110 [concat_bit_lo, concat_bit_hi, bit0_word1, 4111 bits2625, bits1916, bits1510, bits40, CPSR_it])) 4112 |> addThms 4113 4114val MoveToRegisterFromSpecial_cpsr_rwts = 4115 EV [dfn'MoveToRegisterFromSpecial_def, write'R_rwt, BadMode, IncPC_rwt, 4116 arm_stepTheory.R_x_not_pc, reg'PSR, CurrentModeIsUserOrSystem_def] [] [] 4117 ``dfn'MoveToRegisterFromSpecial (F, d)`` 4118 |> addThms 4119 4120fun MoveToSpecialFromImmediate_cpsr_rwts thm c = 4121 EV ([dfn'MoveToSpecialFromImmediate_def, CurrentInstrSet_rwt, IncPC_rwt] @ 4122 thm :: thms) [] c 4123 ``dfn'MoveToSpecialFromImmediate (F, imm, ^tm)`` 4124 |> List.map (utilsLib.ALL_HYP_CONV_RULE 4125 (DATATYPE_CONV THENC REWRITE_CONV thms)) 4126 |> addThms 4127 4128val MoveToSpecialFromImmediate_cpsr_no_control_rwts = 4129 MoveToSpecialFromImmediate_cpsr_rwts CPSRWriteByInstr_no_control 4130 [[`b0` |-> ``F``]] 4131 4132val MoveToSpecialFromImmediate_cpsr_control_usr_rwts = 4133 MoveToSpecialFromImmediate_cpsr_rwts CPSRWriteByInstr_control_usr 4134 [[`b0` |-> ``T``]] 4135 4136fun MoveToSpecialFromRegister_cpsr_rwts thm c = 4137 EV ([dfn'MoveToSpecialFromRegister_def, CurrentInstrSet_rwt, R_rwt, 4138 IncPC_rwt] @ thm :: thms) 4139 [[``n <> 15w: word4``]] c 4140 ``dfn'MoveToSpecialFromRegister (F, n, ^tm)`` 4141 |> List.map (utilsLib.ALL_HYP_CONV_RULE 4142 (DATATYPE_CONV THENC REWRITE_CONV thms THENC DATATYPE_CONV)) 4143 |> addThms 4144 4145val MoveToSpecialFromRegister_cpsr_no_control_rwts = 4146 MoveToSpecialFromRegister_cpsr_rwts CPSRWriteByInstr_no_control 4147 [[`b0` |-> ``F``]] 4148 4149val MoveToSpecialFromRegister_cpsr_control_usr_rwts = 4150 MoveToSpecialFromRegister_cpsr_rwts CPSRWriteByInstr_control_usr 4151 [[`b0` |-> ``T``]] 4152 4153(* ========================================================================= *) 4154 4155(* Evaluator *) 4156 4157local 4158 val lsl_0 = hd (Drule.CONJUNCTS wordsTheory.SHIFT_ZERO) 4159 val word_bit_15 = List.last word_bit_16_thms 4160 val both_rwts = [lsl_0, v2w_13_15_rwts, word_bit_15] 4161 val hyps_rwts = both_rwts 4162 val conc_rwts = [LDM_UPTO_RUN, STM_UPTO_RUN, 4163 Align_branch_immediate, Align_branch_exchange_immediate] @ 4164 Extend_rwt @ both_rwts 4165 val eval_simp_rule = 4166 REWRITE_RULE conc_rwts o 4167 utilsLib.ALL_HYP_CONV_RULE (REWRITE_CONV hyps_rwts) 4168 fun ev tm = 4169 fn rwt => 4170 let 4171 val thm = eval_simp_rule (utilsLib.INST_REWRITE_CONV1 rwt tm) 4172 in 4173 if utilsLib.vacuous thm then NONE else SOME thm 4174 end 4175in 4176 fun eval enc tms = 4177 let 4178 val net = utilsLib.mk_rw_net utilsLib.lhsc (getThms enc tms) 4179 in 4180 fn tm => 4181 (case List.mapPartial (ev tm) (utilsLib.find_rw net tm) of 4182 [] => raise ERR "eval" "no valid step theorem" 4183 | [x] => x 4184 | l => (Parse.print_term tm 4185 ; print "\n" 4186 ; raise ERR "eval" "more than one valid step theorem")) 4187 handle HOL_ERR {message = "not found", 4188 origin_function = "find_rw", ...} => 4189 raise (Parse.print_term tm 4190 ; print "\n" 4191 ; ERR "eval" "instruction instance not supported") 4192 end 4193end 4194 4195local 4196 val get_pair = pairSyntax.dest_pair o rhsc 4197 val get_val = fst o get_pair 4198 val get_state = snd o get_pair 4199 val state_exception_tm = mk_arm_const "arm_state_exception" 4200 val state_encoding_tm = mk_arm_const "arm_state_Encoding" 4201 fun mk_proj_exception r = Term.mk_comb (state_exception_tm, r) 4202 fun mk_proj_encoding r = Term.mk_comb (state_encoding_tm, r) 4203 fun mk_state e c = Term.subst [state_with_pre (c, e)] 4204 fun get_cond l = 4205 let 4206 val cond = List.take (fst (listSyntax.dest_list l), 4) 4207 in 4208 listSyntax.mk_list (cond, Type.bool) 4209 end 4210 val enc = mk_arm_const "Encoding_ARM" 4211 fun set_cond thm1 = 4212 thm1 |> get_val 4213 |> Term.rand 4214 |> bitstringSyntax.dest_v2w |> fst 4215 |> get_cond 4216 |> bitstringSyntax.num_of_term 4217 |> Arbnum.toInt 4218 |> (fn i => wordsSyntax.mk_wordii (if i = 15 then 14 else i, 4)) 4219 |> mk_state enc 4220 val default_tms = List.map fix_datatype 4221 [``~^st.CPSR.T``, ``^st.Encoding = Encoding_ARM``] 4222 val MP_Next = Drule.MATCH_MP arm_stepTheory.NextStateARM_arm 4223 val MP_Next0 = Drule.MATCH_MP arm_stepTheory.NextStateARM_arm0 4224 val Run_CONV = utilsLib.Run_CONV ("arm", st) o get_val 4225in 4226 fun arm_eval config = 4227 let 4228 val tms = 4229 Lib.mk_set (default_tms @ arm_configLib.mk_config_terms config) 4230 val ftch = fetch tms 4231 val dec = arm_decode tms 4232 val run = eval enc tms 4233 in 4234 fn (x, v) => 4235 let 4236 val thm1 = ftch v 4237 val thm2 = hd (dec (x, v)) 4238 val thm3 = Run_CONV thm2 4239 val thm4 = thm3 |> Drule.SPEC_ALL 4240 |> rhsc 4241 |> set_cond thm1 4242 |> run 4243 val r = rhsc thm4 4244 val thm5 = STATE_CONV (mk_proj_encoding r) 4245 val thm6 = STATE_CONV (mk_proj_exception r) 4246 val thm = Drule.LIST_CONJ [thm1, thm2, thm3, thm4, thm5, thm6] 4247 in 4248 MP_Next thm 4249 handle HOL_ERR {message = "different constructors", ...} => 4250 MP_Next0 thm 4251 end 4252 end 4253end 4254 4255local 4256 fun uncond c = Lib.mem (Char.toUpper c) [#"E", #"F"] 4257in 4258 fun arm_step_hex config = 4259 let 4260 val ev = arm_eval config 4261 in 4262 fn s => 4263 let 4264 val s = utilsLib.removeSpaces s 4265 val v = bitstringSyntax.bitstring_of_hexstring s 4266 in 4267 if String.size s = 8 andalso uncond (String.sub (s, 0)) 4268 then [ev ([true], v)] 4269 else [ev ([false, true], v), ev ([true, false], v)] 4270 end 4271 end 4272end 4273 4274fun arm_step_code config = 4275 let 4276 val step_hex = List.map (arm_step_hex config) 4277 open assemblerLib 4278 in 4279 fn q: string quotation => 4280 let 4281 val (code, warnings) = armAssemblerLib.arm_code_with_warnings q 4282 in 4283 if List.null warnings 4284 then () 4285 else ( printn "\n>>>> Warning: contains UNPREDICTABLE code. >>>>\n" 4286 ; printLines warnings 4287 ; printn "\n<<<<\n" 4288 ) 4289 ; step_hex code 4290 end 4291 end 4292 4293local 4294 fun cases l = 4295 let 4296 val n = List.length l 4297 in 4298 List.foldl 4299 (fn (b, (i, a)) => 4300 (i + 1, if b then List.tabulate (n, Lib.equal i) :: a else a)) 4301 (0, []) l 4302 |> snd 4303 end 4304in 4305 fun arm_step config = 4306 let 4307 val ev = arm_eval config 4308 in 4309 fn s => 4310 let 4311 val (x, v) = mk_arm_opcode s 4312 in 4313 List.map (fn x => ldm_stm_rule s (ev (x, v))) (cases x) 4314 end 4315 end 4316end 4317 4318val () = Parse.reveal "add" 4319 4320(* ---------------------------- *) 4321 4322(* 4323 4324val tms = 4325 List.map fix_datatype [``~^st.CPSR.T``, ``^st.Encoding = Encoding_ARM``] 4326 4327val dec = arm_decode tms 4328 4329val config = "" 4330val tms = arm_configLib.mk_config_terms config 4331 4332 4333dec (mk_arm_opcode "MSR (cpsr, imm, control)") 4334 4335val (x, v) = mk_arm_opcode "RFEIA" 4336val (x, v) = mk_arm_opcode "MSR (cpsr, imm, control)" 4337 4338dec (mk_arm_opcode "MSR (cpsr, imm)") 4339dec (mk_arm_opcode "RFEIA") 4340 4341val dec = arm_decode_hex "" 4342dec "E10F1000" 4343dec "E12FF001" 4344dec "E32FF0FF" 4345dec "E328F40F" 4346 4347ev "MSR (cpsr, imm)"; 4348ev "MSR (cpsr, reg)"; 4349ev "MSR (cpsr, imm, control)"; 4350ev "MSR (cpsr, reg, control)"; 4351ev "MRS (cpsr)"; 4352ev "RFEIA"; 4353ev "RFEIB"; 4354ev "RFEDA"; 4355ev "RFEDB"; 4356ev "RFEIA (wb)"; 4357ev "RFEIB (wb)"; 4358ev "RFEDA (wb)"; 4359ev "RFEDB (wb)"; 4360 4361*) 4362 4363 4364end 4365