1(* ------------------------------------------------------------------------ 2 ARMv8 step evaluator 3 ------------------------------------------------------------------------ *) 4 5structure arm8_stepLib :> arm8_stepLib = 6struct 7 8open HolKernel boolLib bossLib 9open arm8Theory arm8_stepTheory arm8AssemblerLib 10open blastLib 11 12structure Parse = 13struct 14 open Parse 15 fun remove (s, tmg) = fst (term_grammar.mfupdate_overload_info 16 (Overload.remove_overloaded_form s) tmg) 17 val (tyg, tmg) = arm8_stepTheory.arm8_step_grammars 18 val tmg = List.foldl remove tmg ["cond", "size"] 19 val (Type, Term) = parse_from_grammars (tyg, tmg) 20end 21open Parse 22 23(* 24val _ = List.map Parse.hide ["cond", "size"] 25val () = List.map Parse.reveal ["cond", "size"] 26*) 27 28val ERR = Feedback.mk_HOL_ERR "arm8_stepLib" 29val WARN = Feedback.HOL_WARNING "arm8_stepLib" 30 31val () = show_assums := true 32 33(* ========================================================================= *) 34 35val rhsc = utilsLib.rhsc 36fun mapl x = utilsLib.augment x [[]] 37val reg_ty = wordsSyntax.mk_int_word_type 5 38fun reg_var v = Term.mk_var (v, reg_ty) 39val r31 = wordsSyntax.mk_wordii (31, 5) 40fun NetFromList l = List.foldl (Lib.uncurry Net.insert) Net.empty l 41 42val arm8_monop = HolKernel.syntax_fns1 "arm8" 43 44(* ---------------------------- *) 45 46local 47 val state_fns = utilsLib.accessor_fns ``:arm8_state`` 48 val other_fns = 49 [pairSyntax.fst_tm, pairSyntax.snd_tm, bitstringSyntax.v2w_tm, 50 ``(h >< l) : 'a word -> 'b word``] @ 51 utilsLib.update_fns ``:arm8_state`` @ 52 utilsLib.accessor_fns ``:TCR_EL1`` 53 val exc = ``SND (raise'exception e s : 'a # arm8_state)`` 54in 55 val cond_rand_thms = utilsLib.mk_cond_rand_thms (other_fns @ state_fns) 56 val snd_exception_thms = 57 utilsLib.map_conv 58 (Drule.GEN_ALL o 59 utilsLib.SRW_CONV [cond_rand_thms, arm8Theory.raise'exception_def] o 60 (fn tm => Term.mk_comb (tm, exc))) state_fns 61end 62 63(* ---------------------------- *) 64 65(* ARMv8 datatype theorems/conversions *) 66 67fun datatype_thms thms = 68 thms @ [pairTheory.FST, pairTheory.SND, wordsTheory.w2w_id, 69 cond_rand_thms, snd_exception_thms, boolTheory.COND_ID, 70 optionTheory.NOT_SOME_NONE] @ 71 utilsLib.datatype_rewrites true "arm8" 72 ["arm8_state", "MemOp", "LogicalOp", "MoveWideOp", "RevOp", 73 "ShiftType", "BranchType"] 74 75val DATATYPE_CONV = REWRITE_CONV (datatype_thms []) 76val DATATYPE_RULE = Conv.CONV_RULE DATATYPE_CONV 77val FULL_DATATYPE_RULE = utilsLib.FULL_CONV_RULE DATATYPE_CONV 78val HYP_DATATYPE_RULE = utilsLib.ALL_HYP_CONV_RULE DATATYPE_CONV 79 80val COND_UPDATE = Q.prove( 81 `!b a x y c m n f. 82 (if b then (a =+ x) ((c =+ m) f) else (a =+ y) ((c =+ n) f)) = 83 (a =+ if b then x else y) ((c =+ if b then m else n) f)`, 84 Cases 85 THEN REWRITE_TAC [combinTheory.APPLY_UPDATE_ID] 86 ) 87 88val COND_UPDATE_CONV = 89 REWRITE_CONV 90 (COND_UPDATE :: 91 utilsLib.mk_cond_update_thms [``:arm8_state``, ``:ProcState``]) 92 93val COND_UPDATE_RULE = Conv.CONV_RULE COND_UPDATE_CONV 94 95val st = ``s: arm8_state`` 96val EV0 = utilsLib.STEP (datatype_thms, st) 97 98val resetEvConv = utilsLib.resetStepConv 99val setEvConv = utilsLib.setStepConv 100 101fun SPLIT_31 d = 102 let 103 val p = boolSyntax.mk_eq (reg_var d, r31) 104 in 105 [[p], [boolSyntax.mk_neg p]] 106 end 107 108val IS_31 = hd o SPLIT_31 109val NOT_31 = hd o tl o SPLIT_31 110 111fun TF (t: term frag list) = utilsLib.augment (t, [boolSyntax.T, boolSyntax.F]) 112fun TF0 t = TF t [[]] 113 114val thms = 115 [CheckSPAlignment_rwt, SetTheFlags, AddWithCarry, 116 wordsTheory.FST_ADD_WITH_CARRY, wordsTheory.word_len_def, 117 wordsTheory.WORD_EXTRACT_ZERO2, 118 X_rwt, write'X_rwt, SP_rwt, write'SP_rwt, 119 mem1, mem2, mem4, mem8, write'mem1, write'mem2, write'mem4, write'mem8] 120 121fun EV l = utilsLib.STEP (datatype_thms, st) (l @ thms) 122 123(* ========================================================================= *) 124 125val () = Feedback.set_trace "notify type variable guesses" 0 126val () = setEvConv (Conv.DEPTH_CONV wordsLib.SIZES_CONV) 127 128(* instruction semantics *) 129 130val lem = 131 blastLib.BBLAST_PROVE 132 ``!x:word64. 133 bit_field_insert 11 0 (0w: word12) x = x && 0xFFFFFFFFFFFFF000w`` 134 135val Address_rwt = 136 EV [dfn'Address_def, lem] [NOT_31 "d"] [] 137 ``dfn'Address (page, imm, d)`` 138 139(* ---------------------------- *) 140 141val Nop_rwt = 142 EV [dfn'Hint_def] [] [] ``dfn'Hint SystemHintOp_NOP`` 143 144val AddSubCarry_rwt = 145 EV [dfn'AddSubCarry_def] (SPLIT_31 "d") (TF0 `setflags`) 146 ``dfn'AddSubCarry (sf, sub_op, setflags, m, n, d)`` 147 148val AddSubExtendRegister_rwt = 149 EV [dfn'AddSubExtendRegister_def, ExtendReg_def] 150 (SPLIT_31 "d") (TF `sub_op` (TF0 `setflags`)) 151 ``dfn'AddSubExtendRegister 152 (sf, sub_op, setflags, m, extend_type, imm3, n, d)`` 153 154val AddSubImmediate_rwt = 155 EV [dfn'AddSubImmediate_def] (SPLIT_31 "d") (TF `sub_op` (TF0 `setflags`)) 156 ``dfn'AddSubImmediate (sf, sub_op, setflags, imm, n, d)`` 157 158val AddSubShiftedRegister_rwt = 159 EV [dfn'AddSubShiftedRegister_def, ShiftReg_def] 160 (SPLIT_31 "d") (TF `sub_op` (TF0 `setflags`)) 161 ``dfn'AddSubShiftedRegister 162 (sf, sub_op, setflags, shift_type, m, imm, n, d)`` 163 164val LogicalImmediate_rwt = 165 EV [dfn'LogicalImmediate_def] (SPLIT_31 "d") (TF0 `setflags`) 166 ``dfn'LogicalImmediate (sf, opc, setflags, imm, n, d)`` 167 168val LogicalShiftedRegister_rwt = 169 EV [dfn'LogicalShiftedRegister_def, ShiftReg_def] 170 (SPLIT_31 "d") (TF0 `setflags`) 171 ``dfn'LogicalShiftedRegister 172 (sf, opc, invert, setflags, shift_type, shift_amount, m, n, d)`` 173 174val Shift_rwt = 175 EV [dfn'Shift_def, ShiftReg_def] (SPLIT_31 "d") [] 176 ``dfn'Shift (sf, shift_type, m, n, d)`` 177 178val MoveWide_rwt = 179 EV [dfn'MoveWide_def] (SPLIT_31 "d") [] 180 ``dfn'MoveWide (sf, opcode, hw, imm, d)`` 181 182val BitfieldMove_rwt = 183 EV [dfn'BitfieldMove_def, Replicate_32_64] (SPLIT_31 "d") [] 184 ``dfn'BitfieldMove (sf: word32, inzero, ext, wmask, tmask, r, s, n, d)`` @ 185 EV [dfn'BitfieldMove_def, Replicate_32_64] (SPLIT_31 "d") [] 186 ``dfn'BitfieldMove (sf: word64, inzero, ext, wmask, tmask, r, s, n, d)`` 187 188val ConditionalCompareImmediate_rwt = 189 EV [dfn'ConditionalCompareImmediate_def, ConditionHolds_def] 190 [] (TF0 `sub_op`) 191 ``dfn'ConditionalCompareImmediate 192 (sf, sub_op, imm, cond, (n, z, c, v), rn)`` 193 |> List.map COND_UPDATE_RULE 194 195val ConditionalCompareRegister_rwt = 196 EV [dfn'ConditionalCompareRegister_def, ConditionHolds_def] 197 [] (TF0 `sub_op`) 198 ``dfn'ConditionalCompareRegister 199 (sf, sub_op, cond, (n, z, c, v), rm, rn)`` 200 |> List.map COND_UPDATE_RULE 201 202val ConditionalSelect_rwt = 203 EV [dfn'ConditionalSelect_def, ConditionHolds_def] (SPLIT_31 "d") [] 204 ``dfn'ConditionalSelect (sf, else_inv, else_inc, cond, m, n, d)`` 205 206val CountLeading_rwt = 207 EV [dfn'CountLeading_def] (SPLIT_31 "d") [] 208 ``dfn'CountLeading (sf, count_clz, n, d)`` 209 210val ExtractRegister_rwt = 211 EV [dfn'ExtractRegister_def] (SPLIT_31 "d") [] 212 ``dfn'ExtractRegister (sf, imms, m, n, d)`` 213 214val Division_rwt = 215 EV [dfn'Division_def] (SPLIT_31 "d") [] 216 ``dfn'Division (sf, unsigned, m, n, d)`` 217 218val MultiplyAddSub_rwt = 219 EV [dfn'MultiplyAddSub_def] (SPLIT_31 "d") [] 220 ``dfn'MultiplyAddSub (sf, sub_op, m, a, n, d)`` 221 222val MultiplyAddSubLong_rwt = 223 EV [dfn'MultiplyAddSubLong_def] (SPLIT_31 "d") [] 224 ``dfn'MultiplyAddSubLong (sub_op, signed, m, a, n, d)`` 225 226val MultiplyHigh_rwt = 227 EV [dfn'MultiplyHigh_def] (SPLIT_31 "d") [] 228 ``dfn'MultiplyHigh (signed, m, n, d)`` 229 230val Reverse32_rwt = 231 EV [dfn'Reverse_def] (SPLIT_31 "d") [] 232 ``dfn'Reverse (sf:word32, op, n, d)`` 233 234val Reverse64_rwt = 235 EV [dfn'Reverse_def] (SPLIT_31 "d") [] 236 ``dfn'Reverse (sf:word64, op, n, d)`` 237 238val CRC_rwt = 239 EV [dfn'CRC_def] (SPLIT_31 "d") [] 240 ``dfn'CRC (sz, crc32c, m, n, d)`` 241 242(* ---------------------------- *) 243 244val map_rule = List.map (DATATYPE_RULE o COND_UPDATE_RULE o HYP_DATATYPE_RULE) 245 246val BranchImmediate_rwt = 247 EV [dfn'BranchImmediate_def, BranchTo_rwt] [] [] 248 ``dfn'BranchImmediate (offset, branch_type)`` 249 |> map_rule 250 251val BranchRegister_rwt = 252 EV [dfn'BranchRegister_def, BranchTo_rwt] [] [] 253 ``dfn'BranchRegister (n, branch_type)`` 254 |> map_rule 255 256val tm = 257 ``ConditionTest (cond,^st.PSTATE.N,^st.PSTATE.Z,^st.PSTATE.C,^st.PSTATE.V)`` 258 259val BranchConditional_rwt = 260 EV [dfn'BranchConditional_def, BranchTo_rwt, ConditionHolds_def] 261 [[tm], [boolSyntax.mk_neg tm]] [] 262 ``dfn'BranchConditional (offset, cond)`` 263 |> map_rule 264 265val CompareAndBranch_rwt = 266 EV [dfn'CompareAndBranch_def, BranchTo_rwt] 267 [[``t = 31w: word5``], 268 [``t <> 31w: word5``, ``w2w (s.REG t) = 0w: 'a word``], 269 [``t <> 31w: word5``, ``w2w (s.REG t) <> 0w: 'a word``]] [] 270 ``dfn'CompareAndBranch (sf, iszero, offset, t)`` 271 |> map_rule 272 273val tm = ``word_bit (w2n (bit_pos: word6)) (w2w (^st.REG t): 'a word)`` 274 275val TestBitAndBranch_rwt = 276 EV [dfn'TestBitAndBranch_def, BranchTo_rwt, wordsTheory.word_bit_0] 277 [[``t = 31w: word5``], 278 [``t <> 31w: word5``, tm], 279 [``t <> 31w: word5``, boolSyntax.mk_neg tm]] 280 (TF `bit_val` [[]]) 281 ``dfn'TestBitAndBranch (sf, bit_pos, bit_val, offset, t)`` 282 |> map_rule 283 284(* ---------------------------- *) 285 286val lem = Q.prove( 287 `!a:'a word b c. (if b then a else a + c) = a + (if b then 0w else c)`, 288 lrw [] 289 ) 290 291val sp_rule = 292 utilsLib.ALL_HYP_CONV_RULE 293 (DATATYPE_CONV 294 THENC SIMP_CONV std_ss [] 295 THENC utilsLib.INST_REWRITE_CONV 296 [mem1, mem2, mem4, mem8, 297 write'mem1, write'mem2, write'mem4, write'mem8] 298 THENC SIMP_CONV std_ss [] 299 THENC DATATYPE_CONV) o 300 SIMP_RULE std_ss [wordsTheory.WORD_ADD_0] o 301 COND_UPDATE_RULE 302 303val map_sp_rule = List.map sp_rule 304 305fun mk_sz i = Term.mk_var ("sz", wordsSyntax.mk_int_word_type i) 306 307val LoadStoreImmediate_rwt = 308 List.map 309 (fn i => 310 EV [dfn'LoadStoreImmediate_def, LoadStoreSingle_def, lem] 311 ((List.map (fn c => ``n <> 31w:word5`` :: c) (SPLIT_31 "t")) @ 312 (List.map (fn c => ``n = 31w:word5`` :: c) (SPLIT_31 "t"))) 313 ((TF `wback` [[`memop` |-> ``MemOp_LOAD``]]) @ 314 (TF `wback` [[`memop` |-> ``MemOp_STORE``]])) 315 ``dfn'LoadStoreImmediate 316 (^(mk_sz i), regsize_word, memop, acctype, signed, F, F, 317 wback, postindex, unsigned_offset, offset, n, t)`` 318 |> map_sp_rule) 319 [8, 16, 32, 64] 320 |> List.concat 321 322val LoadStoreRegister_rwt = 323 List.map 324 (fn i => 325 EV [dfn'LoadStoreRegister_def, LoadStoreSingle_def, ExtendReg_def, lem] 326 ((List.map (fn c => ``n <> 31w:word5`` :: c) (SPLIT_31 "t")) @ 327 (List.map (fn c => ``n = 31w:word5`` :: c) (SPLIT_31 "t"))) 328 [[`memop` |-> ``MemOp_LOAD``], [`memop` |-> ``MemOp_STORE``]] 329 ``dfn'LoadStoreRegister 330 (^(mk_sz i), regsize_word, memop, signed, m, extend_type, 331 shift, n, t)`` 332 |> List.map COND_UPDATE_RULE) 333 [8, 16, 32, 64] 334 |> List.concat 335 336val LoadLiteral_rwt = 337 List.map 338 (fn i => 339 EV [dfn'LoadLiteral_def] (SPLIT_31 "t") [[`memop` |-> ``MemOp_LOAD``]] 340 ``dfn'LoadLiteral (^(mk_sz i), memop, signed, offset, t)``) 341 [32, 64] 342 |> List.concat 343 344val map_sp_rule = 345 List.map 346 (utilsLib.ALL_HYP_CONV_RULE 347 (DATATYPE_CONV 348 THENC SIMP_CONV std_ss [alignmentTheory.aligned_numeric]) o 349 sp_rule) 350 351val LoadStorePair_rwt = 352 List.map 353 (fn i => 354 EV [dfn'LoadStorePair_def, lem] 355 [ 356 [``t = 31w:word5``, ``t2 = 31w:word5``, ``n = 31w:word5``], 357 [``t = 31w:word5``, ``t2 = 31w:word5``, ``n <> 31w:word5``], 358 [``t = 31w:word5``, ``t2 <> 31w:word5``, ``n = 31w:word5``], 359 [``t = 31w:word5``, ``t2 <> 31w:word5``, ``n <> 31w:word5``], 360 [``t <> 31w:word5``, ``t2 = 31w:word5``, ``n = 31w:word5``], 361 [``t <> 31w:word5``, ``t2 = 31w:word5``, ``n <> 31w:word5``], 362 [``t <> 31w:word5``, ``t2 <> 31w:word5``, ``n = 31w:word5``], 363 [``t <> 31w:word5``, ``t2 <> 31w:word5``, ``n <> 31w:word5``] 364 ] 365 ((TF `wback` [[`memop` |-> ``MemOp_LOAD``]]) @ 366 (TF `wback` [[`memop` |-> ``MemOp_STORE``]])) 367 ``dfn'LoadStorePair 368 (^(mk_sz i), memop, acctype, signed, F, F, 369 wback, postindex, offset, n, t, t2)`` 370 |> map_sp_rule) 371 [32, 64] 372 |> List.concat 373 374local 375 val f = UNDISCH o DECIDE o Parse.Term 376 377 val lem1 = f `(~wback \/ n <> t \/ (n = 31w: word5)) ==> 378 ~(d /\ wback /\ (n = t) /\ n <> 31w)` 379 380 val lem2 = f `(~wback \/ n <> t /\ n <> t2 \/ (n = 31w: word5)) ==> 381 ~(d /\ wback /\ ((n = t) \/ (n = t2)) /\ n <> 31w)` 382 383 fun w1 i = bitstringSyntax.fixedwidth_of_num (Arbnum.fromInt i, 1) 384 fun w2 i = bitstringSyntax.padded_fixedwidth_of_num (Arbnum.fromInt i, 2) 385 386 val () = setEvConv (Conv.DEPTH_CONV bitstringLib.word_bit_CONV) 387in 388 val LoadStoreImmediate = 389 EV [LoadStoreImmediate_def, LoadStoreImmediateN_def, lem1] [] 390 (utilsLib.augment (`sz`, List.tabulate (4, w2)) [[]]) 391 ``LoadStoreImmediate 392 (sz,v2w [x0; x1],acctype,wback,postindex,unsigned_offset, 393 offset,n,t)`` 394 val LoadStorePair = 395 EV [LoadStorePair_def, LoadStorePairN_def, lem2] 396 [[``~((memop = MemOp_LOAD) /\ (t = t2: word5))``]] 397 (utilsLib.augment (`sf`, List.tabulate (2, w1)) [[]]) 398 ``LoadStorePair 399 (sf,memop,acctype,signed,wback,postindex,offset,n,t,t2)`` 400end 401 402val () = Feedback.set_trace "notify type variable guesses" 1 403val () = setEvConv (Conv.DEPTH_CONV wordsLib.SIZES_CONV) 404 405(* ========================================================================= *) 406 407(* Fetch *) 408 409fun mk_opcode v = 410 let 411 val (l, ty) = listSyntax.dest_list v 412 val () = ignore (ty = Type.bool andalso List.length l <= 32 413 orelse raise ERR "mk_opcode" "bad Bool list") 414 in 415 listSyntax.mk_list (utilsLib.padLeft boolSyntax.F 32 l, Type.bool) 416 end 417 418local 419 val pat = bitstringSyntax.mk_bstring 32 0 420in 421 fun inst_opcode tm = Thm.INST (fst (Term.match_term pat (mk_opcode tm))) 422 val inst_branch_hint = Thm.INST [st |-> ``^st with branch_hint := NONE``] 423end 424 425val Fetch_rwt = 426 EV [Fetch_def, mem_word_def, bitstringTheory.word_concat_v2w_rwt] 427 [[ 428 ``^st.MEM s.PC = ^(bitstringSyntax.mk_vec 8 0)``, 429 ``^st.MEM (s.PC + 1w) = ^(bitstringSyntax.mk_vec 8 8)``, 430 ``^st.MEM (s.PC + 2w) = ^(bitstringSyntax.mk_vec 8 16)``, 431 ``^st.MEM (s.PC + 3w) = ^(bitstringSyntax.mk_vec 8 24)`` 432 ]] 433 [] ``Fetch`` 434 |> hd 435 |> inst_branch_hint 436 |> SIMP_RULE (srw_ss()++boolSimps.LET_ss) [bitstringTheory.fixwidth_def] 437 |> HYP_DATATYPE_RULE 438 439fun arm8_fetch tm = inst_opcode tm Fetch_rwt 440 441(* ========================================================================= *) 442 443(* Decode *) 444 445local 446 val cmp = wordsLib.words_compset() 447 val () = ( bitstringLib.add_bitstring_compset cmp 448 ; integer_wordLib.add_integer_word_compset cmp 449 ; intReduce.add_int_compset cmp 450 ; computeLib.scrub_thms 451 [wordsTheory.bit_field_insert_def, 452 wordsTheory.word_quot_def, 453 wordsTheory.word_div_def] 454 cmp 455 ; computeLib.add_thms 456 (datatype_thms 457 [DecodeShift_def, HighestSetBit_def, Ones_def, Zeros_def, 458 Replicate_def, DecodeRegExtend_def, ShiftValue_def, 459 bit_field_insert_thms, ConditionTest, ExtendWord, 460 DecodeBitMasks_def, wordsTheory.WORD_AND_CLAUSES, 461 wordsTheory.WORD_OR_CLAUSES, num2ShiftType_thm, 462 num2ExtendType_thm]) 463 cmp 464 ; computeLib.add_conv 465 (bitstringSyntax.v2w_tm, 1, bitstringLib.v2w_n2w_CONV) cmp 466 ) 467in 468 val ARM8_CONV = computeLib.CBV_CONV cmp 469end 470 471local 472 val Unallocated = Term.prim_mk_const {Name = "Unallocated", Thy = "arm8"} 473 val Reserved = Term.prim_mk_const {Name = "Reserved", Thy = "arm8"} 474 475 val asms = [arm8_stepTheory.DecodeLem, arm8_stepTheory.DecodeInzeroExtend] @ 476 List.map (ASSUME o Parse.Term) 477 [ 478 `DecodeBitMasks 479 (v2w [F],v2w [x8; x9; x10; x11; x12; x13], 480 v2w [x2; x3; x4; x5; x6; x7],T) = SOME (imm:word32, x)`, 481 `DecodeBitMasks 482 (v2w [x2],v2w [x9; x10; x11; x12; x13; x14], 483 v2w [x3; x4; x5; x6; x7; x8],T) = SOME (imm:word64, x)`, 484 `DecodeBitMasks 485 (v2w [F],v2w [F; x7; x8; x9; x10; x11], 486 v2w [F; x2; x3; x4; x5; x6],F) = SOME (imm:word32, x)`, 487 `DecodeBitMasks 488 (v2w [T],v2w [x8; x9; x10; x11; x12; x13], 489 v2w [x2; x3; x4; x5; x6; x7],F)= SOME (imm:word64, x)` 490 ] 491 492 val r_rwt = 493 utilsLib.map_conv 494 (EVAL THENC REWRITE_CONV [arm8Theory.num2SystemHintOp_thm]) 495 [``v2w [F; F; F] <+ 6w: word3``, 496 ``arm8$num2SystemHintOp (w2n (v2w [F; F; F]: word3))``] 497 498 val r1 = REWRITE_RULE [r_rwt] 499 val r2 = utilsLib.INST_REWRITE_RULE (LoadStoreImmediate @ LoadStorePair) 500 val r3 = 501 utilsLib.ALL_HYP_CONV_RULE 502 (REWRITE_CONV [GSYM arm8Theory.MemOp_distinct, 503 arm8_stepTheory.LoadCheck, 504 boolTheory.DE_MORGAN_THM]) o 505 SIMP_RULE (srw_ss()++boolSimps.LET_ss) asms 506 507 val ast_thms = 508 List.filter 509 ((fn tm => not (tm = Unallocated orelse tm = Reserved)) o rhsc) o 510 utilsLib.split_conditions o r2 o r1 511 512 exception Decode of string * thm list 513 514 fun ast_thm name thm = 515 case ast_thms thm of 516 [] => NONE 517 | [thm] => SOME (r3 thm) 518 | thms => raise Decode (name, thms) 519 520 val concat_CONV = 521 Conv.REWR_CONV bitstringTheory.word_concat_v2w_rwt THENC ARM8_CONV 522 523 val case_word2_literal = 524 Q.ISPEC `v2w [b1; b0] : word2` (Q.SPEC `f` boolTheory.literal_case_THM) 525 526 val LoadStoreRegister = 527 SIMP_RULE (std_ss++boolSimps.LET_ss) [] LoadStoreRegister_def 528 529 val Decode_rwt = 530 Decode_def 531 |> Thm.SPEC (bitstringSyntax.mk_vec 32 0) 532 |> Conv.RIGHT_CONV_RULE 533 (REWRITE_CONV 534 [DecodeLogicalOp, DecodeRevOp, arm8Theory.boolify32_v2w, 535 LoadStoreRegister, case_word2_literal] 536 THENC Conv.DEPTH_CONV PairedLambda.let_CONV 537 THENC REWRITE_CONV [bitstringTheory.ops_to_v2w, EVAL ``n2v 0``] 538 THENC Conv.DEPTH_CONV concat_CONV 539 THENC Conv.DEPTH_CONV bitstringLib.word_bit_CONV 540 THENC Conv.DEPTH_CONV BETA_CONV 541 THENC Conv.DEPTH_CONV bitstringLib.v2w_eq_CONV 542 THENC REWRITE_CONV []) 543 544 fun get_var_vars p pat = 545 List.mapPartial (fn (c, tm) => if c = #"." then SOME tm else NONE) 546 (ListPair.zip (String.explode p, fst (listSyntax.dest_list pat))) 547 548 fun all_substs acc = 549 fn [] => acc 550 | (h: Term.term) :: t => 551 all_substs 552 (List.map (fn s => (h |-> boolSyntax.T) :: s) acc @ 553 List.map (fn s => (h |-> boolSyntax.F) :: s) acc) t 554 val all_substs = all_substs [[]] 555 556 val get_opc = Term.rand o Term.rand o utilsLib.lhsc 557in 558 fun decode_thm tm = r1 (inst_opcode tm Decode_rwt) 559 fun decode_rwt (name, p) = 560 let 561 val pat = utilsLib.pattern (String.map (fn #"." => #"_" | s => s) p) 562 val thm = decode_thm pat 563 val ast = ast_thm name 564 val i = ref 0 565 fun dec s = 566 if List.null s 567 then SOME ((name, pat), Option.valOf (ast thm)) 568 else case ast (Thm.INST s thm) of 569 NONE => NONE 570 | SOME th => 571 ( Portable.inc i 572 ; SOME ((name ^ "-" ^ Int.toString (!i), get_opc th), th) 573 ) 574 in 575 List.mapPartial dec (all_substs (get_var_vars p pat)) 576 end 577end 578 579val ps = (List.concat o List.map decode_rwt) 580 [ 581 ("Address", "___TFFFF________________________"), 582 ("AddSubShiftedRegister32", "F..FTFTT__F_____F_______________"), 583 ("AddSubShiftedRegister64", "T..FTFTT__F_____________________"), 584 ("AddSubExtendRegister", "...FTFTTFFT_____________________"), 585 ("AddSubImmediate", "...TFFFTF_______________________"), 586 ("AddSubCarry", "._.TTFTFFFF_____FFFFFF__________"), 587 ("LogicalShiftedRegister32", "F..FTFTF________F_______________"), 588 ("LogicalShiftedRegister64", "T..FTFTF________________________"), 589 ("LogicalImmediate32", "F..TFFTFFF______________________"), 590 ("LogicalImmediate64", "T..TFFTFF_______________________"), 591 ("Shift", ".FFTTFTFTTF_____FFTF____________"), 592 ("MoveWide32", "F__TFFTFTF______________________"), 593 ("MoveWide64", "T__TFFTFT_______________________"), 594 ("BitfieldMove32", "F__TFFTTFFF_____F_______________"), 595 ("BitfieldMove64", "T__TFFTTFT______________________"), 596 ("ConditionalCompareImmediate", "..TTTFTFFTF_________TF_____F____"), 597 ("ConditionalCompareRegister", "..TTTFTFFTF_________FF_____F____"), 598 ("ConditionalSelect", "._FTTFTFTFF_________F___________"), 599 ("CountLeading", ".TFTTFTFTTFFFFFFFFFTF___________"), 600 ("ExtractRegister32", "FFFTFFTTTFF_____F_______________"), 601 ("ExtractRegister64", "TFFTFFTTTTF_____________________"), 602 ("Division", ".FFTTFTFTTF_____FFFFT___________"), 603 ("MultiplyAddSub", ".FFTTFTTFFF_____________________"), 604 ("MultiplyAddSubLong", "TFFTTFTT_FT_____________________"), 605 ("MultiplyHigh", "TFFTTFTT_TF_____F_______________"), 606 ("Reverse32", "FTFTTFTFTTFFFFFFFFFF____________"), 607 ("Reverse64", "TTFTTFTFTTFFFFFFFFFF____________"), 608 ("CRC8", "FFFTTFTFTTF_____FTF_FF__________"), 609 ("CRC16", "FFFTTFTFTTF_____FTF_FT__________"), 610 ("CRC32", "FFFTTFTFTTF_____FTF_TF__________"), 611 ("CRC64", "TFFTTFTFTTF_____FTF_TT__________"), 612 ("BranchConditional", "FTFTFTFF___________________F____"), 613 ("BranchImmediate", ".FFTFT__________________________"), 614 ("BranchRegisterJMP", "TTFTFTTFFFFTTTTTFFFFFF_____FFFFF"), 615 ("BranchRegisterCALL", "TTFTFTTFFFTTTTTTFFFFFF_____FFFFF"), 616 ("BranchRegisterRET", "TTFTFTTFFTFTTTTTFFFFFF_____FFFFF"), 617 ("CompareAndBranch", ".FTTFTF_________________________"), 618 ("TestBitAndBranch", ".FTTFTT.________________________"), 619 ("LoadStoreImmediate-1", "..TTTFFF..F__________.__________"), 620 ("LoadStoreImmediate-2", "..TTTFFT..______________________"), 621 ("LoadLiteral", "..FTTFFF________________________"), 622 ("LoadStoreRegister", "..TTTFFF..T______T__TF__________"), 623 ("StorePair32", "FFTFTFF_.F______________________"), 624 ("LoadPair32", "F_TFTFF_.T______________________"), 625 ("LoadStorePair64", "TFTFTFF_..______________________"), 626 ("NoOperation", "TTFTFTFTFFFFFFTTFFTFFFFFFFFTTTTT") 627 ] 628 629local 630 val ps2 = List.map fst ps 631 val d = Redblackmap.fromList String.compare 632 (List.map (utilsLib.lowercase ## I) ps2) 633 val net = NetFromList (List.map Lib.swap ps2) 634in 635 val arm8_names = List.map fst ps2 636 fun arm8_pattern s = Redblackmap.peek (d, utilsLib.lowercase s) 637 fun arm8_instruction tm = 638 case Net.match (mk_opcode tm) net of 639 [tm] => SOME tm 640 | _ => NONE 641end 642 643local 644 val (_, mk_Decode, _, _) = arm8_monop "Decode" 645 val ty32 = fcpSyntax.mk_int_numeric_type 32 646 val rwts = List.map snd ps 647 val decode_CONV = utilsLib.FULL_CONV_RULE (REWRITE_CONV []) o 648 utilsLib.INST_REWRITE_CONV rwts 649 fun fallback tm = (WARN "arm8_decode" "fallback decode"; decode_thm tm) 650in 651 fun arm8_decode v = 652 let 653 val opc = mk_opcode v 654 val tm = mk_Decode (bitstringSyntax.mk_v2w (opc, ty32)) 655 val thm = decode_CONV tm handle Conv.UNCHANGED => fallback opc 656 in 657 if utilsLib.vacuous thm then fallback opc else thm 658 end 659 fun arm8_decode_instruction s = 660 case arm8_pattern s of 661 SOME tm => arm8_decode tm 662 | NONE => raise ERR "arm8_decode_instruction" "not found" 663 val arm8_decode_hex = arm8_decode o bitstringSyntax.bitstring_of_hexstring 664end 665 666(* ========================================================================= *) 667 668(* Step *) 669 670(* 671 672 fun printer (_: int) _ (a: 'a Net.net) = PolyML.PrettyString "<net>" 673 val () = PolyML.addPrettyPrinter printer 674 675*) 676 677local 678 val mk_net = 679 NetFromList o 680 List.map (fn th => (rator (utilsLib.lhsc th), 681 FULL_DATATYPE_RULE (inst_branch_hint th))) 682 val net = mk_net 683 (Address_rwt @ AddSubCarry_rwt @ AddSubExtendRegister_rwt @ 684 AddSubImmediate_rwt @ AddSubShiftedRegister_rwt @ LogicalImmediate_rwt @ 685 LogicalShiftedRegister_rwt @ Shift_rwt @ MoveWide_rwt @ BitfieldMove_rwt @ 686 ConditionalCompareImmediate_rwt @ ConditionalCompareRegister_rwt @ 687 ConditionalSelect_rwt @ CountLeading_rwt @ ExtractRegister_rwt @ 688 Division_rwt @ MultiplyAddSub_rwt @ MultiplyAddSubLong_rwt @ 689 MultiplyHigh_rwt @ Reverse32_rwt @ Reverse64_rwt @ CRC_rwt @ 690 BranchImmediate_rwt @ BranchRegister_rwt @ BranchConditional_rwt @ 691 CompareAndBranch_rwt @ TestBitAndBranch_rwt @ LoadStoreImmediate_rwt @ 692 LoadStoreRegister_rwt @ LoadLiteral_rwt @ LoadStorePair_rwt @ Nop_rwt 693 ) 694 val get_next = Term.rator o utilsLib.lhsc 695 val r = REWRITE_RULE [] 696 fun make_match tm thm = 697 r (Drule.INST_TY_TERM (Term.match_term (get_next thm) tm) thm) 698in 699 fun arm8_next tm = 700 List.mapPartial (Lib.total (make_match tm)) (Net.match tm net) 701end 702 703local 704 val v31 = bitstringLib.v2w_n2w_CONV ``v2w [T; T; T; T; T] : word5`` 705 val cnv = REWRITE_CONV [DECIDE ``a <> b \/ (a = b: 'a)``, v31] 706 val vs = List.filter Term.is_var o fst o listSyntax.dest_list o fst o 707 bitstringSyntax.dest_v2w 708 val r31 = wordsSyntax.mk_wordii (31, 5) 709 val reg_31 = 710 List.concat o 711 List.mapPartial 712 (Option.composePartial 713 (fn (l, r) => 714 if r = r31 715 then SOME (List.map (fn v => v |-> boolSyntax.T) (vs l)) 716 else NONE, 717 Lib.total boolSyntax.dest_eq)) 718 val rule = utilsLib.ALL_HYP_CONV_RULE cnv 719in 720 fun REG_31_RULE thm = 721 let 722 val l = reg_31 (Thm.hyp thm) 723 in 724 if List.null l then thm else rule (Thm.INST l thm) 725 end 726end 727 728val remove_vacuous = List.filter (not o utilsLib.vacuous) 729 730local 731 val arm8_run = utilsLib.Run_CONV ("arm8", st) o rhsc 732 val (_, mk_exception, _, _) = arm8_monop "arm8_state_exception" 733 val arm8_exception = DATATYPE_CONV o mk_exception o utilsLib.rhsc 734 val get_next = Term.rator o utilsLib.rhsc o Drule.SPEC_ALL 735 val rule = REG_31_RULE o Conv.RIGHT_CONV_RULE DATATYPE_CONV o 736 MATCH_MP arm8_stepTheory.NextStateARM8 737in 738 fun arm8_step v = 739 let 740 val thm1 = arm8_fetch v 741 val thm2 = arm8_decode v 742 val thm3 = arm8_run thm2 743 val tm = get_next thm3 744 val thm4s = arm8_next tm 745 fun conj th = Drule.LIST_CONJ [thm1, thm2, thm3, th, arm8_exception th] 746 in 747 remove_vacuous (List.map (rule o conj) thm4s) 748 end 749end 750 751local 752 val (_, _, dest_DecodeBitMasks, _) = arm8_monop "DecodeBitMasks" 753 val is_dbm = Lib.can (dest_DecodeBitMasks o lhs) 754 val dst = pairSyntax.dest_pair o optionSyntax.dest_some 755in 756 val DecodeBitMasks_CONV = Conv.REWR_CONV DecodeBitMasks_def THENC ARM8_CONV 757 fun DecodeBitMasks_RULE th = 758 case List.filter is_dbm (Thm.hyp th) of 759 [tm] => let 760 val (vimm, vx) = dst (rhs tm) 761 val thm = DecodeBitMasks_CONV (lhs tm) 762 val th' = 763 case Lib.total dst (rhsc thm) of 764 SOME (imm, x) => Thm.INST [vimm |-> imm, vx |-> x] th 765 | NONE => th 766 in 767 utilsLib.MATCH_HYP_CONV_RULE 768 (REWRITE_CONV [optionTheory.NOT_NONE_SOME, thm]) tm th' 769 end 770 | _ => th 771end 772 773local 774 val rule = 775 DecodeBitMasks_RULE o 776 utilsLib.FULL_CONV_RULE 777 (ARM8_CONV THENC REWRITE_CONV [wordsTheory.WORD_SUB_INTRO] 778 THENC DATATYPE_CONV) 779 val step_hex = remove_vacuous o List.map rule o arm8_step o 780 bitstringSyntax.bitstring_of_hexstring 781in 782 fun arm8_step_hex s = Lib.with_exn step_hex s (ERR "arm8_step_hex" s) 783end 784 785val arm8_step_code = List.map arm8_step_hex o arm8AssemblerLib.arm8_code 786 787(* Testing... 788 789open arm8_stepLib 790 791local 792 val gen = Random.newgenseed 1.0 793 fun random_bit () = 794 if Random.range (0, 2) gen = 0 then boolSyntax.T else boolSyntax.F 795in 796 fun random_hex tm = 797 let 798 val l = Term.free_vars tm 799 val s = List.map (fn v => v |-> random_bit ()) l 800 in 801 bitstringSyntax.hexstring_of_term (Term.subst s tm) 802 end 803end 804 805val test = 806 Count.apply (arm8_step_hex o (fn s => (print (s ^ "\n"); s)) o random_hex o 807 Option.valOf o arm8_pattern) 808 809val test = arm8_step o Option.valOf o arm8_pattern 810 811val unsupported = 812 List.mapPartial (fn n => if List.null (test n) then SOME n else NONE) 813 arm8_names 814 815(* should all be pre-fetch instructions *) 816 817List.map arm8_decode_instruction unsupported 818 819*) 820 821end 822