1(* ------------------------------------------------------------------------ 2 MIPS step evaluator 3 ------------------------------------------------------------------------ *) 4 5structure mips_stepLib :> mips_stepLib = 6struct 7 8open HolKernel boolLib bossLib 9open blastLib mipsTheory mips_stepTheory 10 11local open mips in end 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 mipsTheory.mips_grammars 20 val (Type, Term) = parse_from_grammars (tyg, tmg) 21end 22open Parse 23 24val ERR = Feedback.mk_HOL_ERR "mips_stepLib" 25 26val () = show_assums := true 27 28(* ========================================================================= *) 29 30val rhsc = utilsLib.rhsc 31val st = ``s: mips_state`` 32fun mapl x = utilsLib.augment x [[]] 33 34val cond_thms = Q.prove( 35 `(!b c. (if b then T else c) = b \/ c) /\ 36 (!b c. (if b then F else c) = ~b /\ c)`, 37 rw [] 38 ) 39 40local 41 val state_fns = utilsLib.accessor_fns ``:mips_state`` 42 val other_fns = 43 [pairSyntax.fst_tm, pairSyntax.snd_tm, bitstringSyntax.v2w_tm, 44 optionSyntax.is_some_tm] @ 45 utilsLib.update_fns ``:mips_state`` @ 46 utilsLib.accessor_fns ``:CP0`` 47 val extra_fns = 48 [wordsSyntax.sw2sw_tm, wordsSyntax.w2w_tm, 49 wordsSyntax.word_add_tm, wordsSyntax.word_sub_tm, 50 wordsSyntax.word_mul_tm, 51 wordsSyntax.word_rem_tm, wordsSyntax.word_quot_tm, 52 wordsSyntax.word_mod_tm, wordsSyntax.word_div_tm, 53 wordsSyntax.word_lo_tm, wordsSyntax.word_lt_tm, 54 wordsSyntax.word_ls_tm, wordsSyntax.word_le_tm, 55 wordsSyntax.word_hi_tm, wordsSyntax.word_gt_tm, 56 wordsSyntax.word_hs_tm, wordsSyntax.word_ge_tm, 57 wordsSyntax.word_and_tm, wordsSyntax.word_or_tm, 58 wordsSyntax.word_xor_tm, wordsSyntax.word_lsl_tm, 59 wordsSyntax.word_lsr_tm, wordsSyntax.word_asr_tm, 60 wordsSyntax.word_1comp_tm, wordsSyntax.word_2comp_tm, 61 wordsSyntax.w2n_tm, 62 ``(h >< l) : 'a word -> 'b word``, 63 ``(=):'a word -> 'a word -> bool``, 64 ``word_bit n: 'a word -> bool``] 65 val exc = ``SND (raise'exception e s : 'a # mips_state)`` 66in 67 val cond_rand_thms = utilsLib.mk_cond_rand_thms (other_fns @ state_fns) 68 val extra_cond_rand_thms = utilsLib.mk_cond_rand_thms extra_fns 69 val snd_exception_thms = 70 utilsLib.map_conv 71 (Drule.GEN_ALL o 72 utilsLib.SRW_CONV [cond_rand_thms, mipsTheory.raise'exception_def] o 73 (fn tm => Term.mk_comb (tm, exc))) state_fns 74end 75 76fun mips_thms thms = 77 thms @ 78 [cond_rand_thms, cond_thms, snd_exception_thms, 79 NotWordValue0, NotWordValueCond, 80 GPR_def, write'GPR_def, CPR_def, write'CPR_def, boolTheory.COND_ID, 81 wordsLib.WORD_DECIDE ``~(a > a:'a word)``, 82 wordsLib.WORD_DECIDE ``a >= a:'a word``, 83 wordsTheory.WORD_EXTRACT_ZERO2, wordsTheory.WORD_ADD_0, 84 wordsTheory.WORD_AND_CLAUSES, wordsTheory.WORD_OR_CLAUSES, 85 wordsTheory.WORD_XOR_CLAUSES, wordsTheory.WORD_MULT_CLAUSES, 86 wordsTheory.WORD_SUB_RZERO, wordsTheory.WORD_SUB_LZERO, 87 wordsTheory.WORD_LESS_REFL, wordsTheory.WORD_LOWER_REFL, 88 wordsTheory.WORD_LESS_EQ_REFL, 89 wordsTheory.WORD_LO_word_0, wordsTheory.ZERO_SHIFT, wordsTheory.SHIFT_ZERO, 90 wordsTheory.WORD_XOR_ASSOC, wordsTheory.WORD_NEG_0, wordsTheory.WORD_NOT_0, 91 wordsTheory.sw2sw_0, wordsTheory.w2w_0, wordsTheory.word_0_n2w, 92 wordsTheory.word_bit_0, sw16_to_sw64] @ 93 utilsLib.datatype_rewrites true "mips" 94 ["mips_state", "CP0", "StatusRegister", "ExceptionType"] 95 96val COND_UPDATE_CONV = 97 REWRITE_CONV (utilsLib.mk_cond_update_thms 98 [``:mips_state``, ``:CP0``, ``:FCSR``, ``:StatusRegister``]) 99 THENC REWRITE_CONV (mips_stepTheory.cond_update_memory :: mips_thms []) 100 101val COND_UPDATE_RULE = Conv.CONV_RULE COND_UPDATE_CONV 102 103local 104 val thms = ref ([]: thm list) 105in 106 fun resetThms () = thms := [] 107 fun getThms tms = 108 utilsLib.specialized "" (utilsLib.WGROUND_CONV, tms) (!thms) 109 fun addThms ts = (thms := ts @ !thms; ts) 110end 111 112val ev = utilsLib.STEP (mips_thms, st) 113fun evr (rule:rule) thms c cvr = List.map rule o ev thms c cvr 114 115fun EVR rule thms c cvr = addThms o evr rule thms c cvr 116val EV = EVR Lib.I 117val EVC = EVR COND_UPDATE_RULE 118 119(* ------------------------------------------------------------------------- *) 120 121val () = utilsLib.setStepConv utilsLib.WGROUND_CONV 122 123val SignalException = 124 ev [SignalException_def, extra_cond_rand_thms, ExceptionCode_def] 125 [[``~^st.CP0.Status.EXL``]] [] 126 ``SignalException (ExceptionType)`` 127 |> hd 128 129val rule = 130 utilsLib.ALL_HYP_CONV_RULE (SIMP_CONV std_ss (mips_thms [])) o 131 REWRITE_RULE [] o 132 utilsLib.INST_REWRITE_RULE 133 [ASSUME ``~^st.CP0.Status.EXL``, ASSUME ``^st.exceptionSignalled = F``] 134 135val () = utilsLib.resetStepConv () 136 137fun reg i = bitstringSyntax.padded_fixedwidth_of_num (Arbnum.fromInt i, 5) 138 139val r0 = reg 0 140 141fun comb (0, _ ) = [[]] 142 | comb (_, [] ) = [] 143 | comb (m, x::xs) = map (fn y => x :: y) (comb (m-1, xs)) @ comb (m, xs) 144 145fun all_comb l = 146 List.concat (List.tabulate (List.length l + 1, fn i => comb (i, l))) 147 148val oEV = 149 EVR (rule o COND_UPDATE_RULE) 150 [dfn'ADDI_def, dfn'DADDI_def, mipsTheory.ExceptionType2num_thm, 151 SignalException, ExceptionCode_def, extra_cond_rand_thms] 152 [[``rt <> 0w: word5``, ``rs <> 0w: word5``, 153 ``~NotWordValue (^st.gpr rs)``]] 154 (all_comb [`rt` |-> r0, `rs` |-> r0]) 155 156val iEV = 157 EV [dfn'ADDIU_def, dfn'DADDIU_def, dfn'SLTI_def, dfn'SLTIU_def, 158 dfn'ANDI_def, dfn'ORI_def, dfn'XORI_def, dfn'LUI_def, 159 extra_cond_rand_thms] 160 [[``rt <> 0w: word5``, ``rs <> 0w: word5``, 161 ``~NotWordValue (^st.gpr rs)``]] 162 (all_comb [`rt` |-> r0, `rs` |-> r0]) 163 164val lEV = 165 EV [dfn'LUI_def, extra_cond_rand_thms] 166 [[``rt <> 0w: word5``]] 167 [[], [`rt` |-> r0]] 168 169val pEV = 170 EVR (rule o COND_UPDATE_RULE) 171 [dfn'ADD_def, dfn'SUB_def, dfn'DADD_def, dfn'DSUB_def, 172 dfn'MOVN_def, dfn'MOVZ_def, mipsTheory.ExceptionType2num_thm, 173 SignalException, ExceptionCode_def, extra_cond_rand_thms] 174 [[``rd <> 0w: word5``, ``rs <> 0w: word5``, ``rt <> 0w: word5``, 175 ``~NotWordValue (^st.gpr rs)``, ``~NotWordValue (^st.gpr rt)``]] 176 (all_comb [`rt` |-> r0, `rs` |-> r0, `rd` |-> r0]) 177 178val rEV = 179 EV [dfn'ADDU_def, dfn'DADDU_def, dfn'SUBU_def, dfn'DSUBU_def, dfn'SLT_def, 180 dfn'SLTU_def, dfn'AND_def, dfn'OR_def, dfn'XOR_def, dfn'NOR_def, 181 dfn'SLLV_def, dfn'SRLV_def, dfn'SRAV_def, dfn'DSLLV_def, dfn'DSRLV_def, 182 dfn'DSRAV_def, dfn'MUL_def, write'HI_def, write'LO_def, 183 extra_cond_rand_thms] 184 [[``rd <> 0w: word5``, ``rs <> 0w: word5``, ``rt <> 0w: word5``, 185 ``~NotWordValue (^st.gpr rs)``, ``~NotWordValue (^st.gpr rt)``]] 186 (all_comb [`rt` |-> r0, `rs` |-> r0, `rd` |-> r0]) 187 188val sEV = 189 EV [dfn'SLL_def, dfn'SRL_def, dfn'SRA_def, dfn'DSLL_def, dfn'DSRL_def, 190 dfn'DSRA_def, dfn'DSLL32_def, dfn'DSRL32_def, dfn'DSRA32_def, 191 extra_cond_rand_thms] 192 [[``rd <> 0w: word5``, ``rt <> 0w: word5``, 193 ``~NotWordValue (^st.gpr rt)``]] 194 (all_comb [`rt` |-> r0, `rd` |-> r0]) 195 196val hEV = 197 EVC [dfn'MFHI_def, dfn'MFLO_def, dfn'MTHI_def, dfn'MTLO_def, dfn'JALR_def, 198 write'HI_def, write'LO_def, HI_def, LO_def, extra_cond_rand_thms] 199 [[``rd <> 0w: word5``, ``^st.hi = SOME vHI``, ``^st.lo = SOME vLO``]] 200 [[], [`rd` |-> r0]] 201 202val mEV = 203 EV [dfn'MADD_def, dfn'MADDU_def, dfn'MSUB_def, dfn'MSUBU_def, 204 dfn'MULT_def, dfn'MULTU_def, dfn'DMULT_def, dfn'DMULTU_def, 205 write'HI_def, write'LO_def, HI_def, LO_def, extra_cond_rand_thms, 206 blastLib.BBLAST_PROVE 207 ``(!a:word32 b:word32. (63 >< 32) ((a @@ b) : word64) = a) /\ 208 (!a:word32 b:word32. (31 >< 0) ((a @@ b) : word64) = b)``] 209 [[``rs <> 0w: word5``, ``rt <> 0w: word5``, 210 ``~NotWordValue (^st.gpr rs)``, ``~NotWordValue (^st.gpr rt)``, 211 ``^st.hi = SOME vHI``, ``^st.lo = SOME vLO``]] 212 (all_comb [`rt` |-> r0, `rs` |-> r0]) 213 214val dEV = 215 EV [dfn'DIV_def, dfn'DIVU_def, dfn'DDIV_def, dfn'DDIVU_def, 216 write'HI_def, write'LO_def, extra_cond_rand_thms] 217 [[``rt <> 0w: word5``, ``^st.gpr (rt) <> 0w``, ``rs <> 0w: word5``, 218 ``~NotWordValue (^st.gpr rs)``, ``~NotWordValue (^st.gpr rt)``]] 219 [[], [`rs` |-> r0]] 220 221val bbEV = 222 EVC [dfn'BEQ_def, dfn'BNE_def, dfn'BEQL_def, dfn'BNEL_def, 223 ConditionalBranch_def, ConditionalBranchLikely_def] 224 [[``^st.BranchDelay = NONE``, ``rs <> 0w: word5``, ``rt <> 0w: word5``]] 225 (all_comb [`rt` |-> r0, `rs` |-> r0]) 226 227val bEV = 228 EVC [dfn'BLEZ_def, dfn'BGTZ_def, dfn'BLTZ_def, dfn'BGEZ_def, 229 dfn'BLTZAL_def, dfn'BGEZAL_def, dfn'BLEZL_def, dfn'BGTZL_def, 230 dfn'BLTZL_def, dfn'BGEZL_def, dfn'BLTZALL_def, dfn'BGEZALL_def, 231 ConditionalBranch_def, ConditionalBranchLikely_def] 232 [[``^st.CP0.Status.CU1``, ``^st.BranchDelay = NONE``, 233 ``rs <> 0w: word5``]] 234 [[], [`rs` |-> r0]] 235 236val jEV = 237 EV [dfn'J_def, dfn'JAL_def, dfn'JR_def, 238 dfn'BC1F_def, dfn'BC1FL_def, dfn'BC1T_def, dfn'BC1TL_def, 239 ConditionalBranch_def, ConditionalBranchLikely_def] 240 [[``^st.CP0.Status.CU1``]] 241 [] 242 243val fpEV = EVC 244 [dfn'ABS_D_def, dfn'ABS_S_def, dfn'NEG_D_def, dfn'NEG_S_def, 245 dfn'SQRT_D_def, dfn'SQRT_S_def, 246 dfn'ADD_D_def, dfn'ADD_S_def, dfn'SUB_D_def, dfn'SUB_S_def, 247 dfn'DIV_D_def, dfn'DIV_S_def, dfn'MUL_D_def, dfn'MUL_S_def, 248 dfn'MADD_D_def, dfn'MADD_S_def, dfn'MSUB_D_def, dfn'MSUB_S_def, 249 dfn'MOV_D_def, dfn'MOV_S_def, 250 dfn'MOVF_def, dfn'MOVF_D_def, dfn'MOVF_S_def, 251 dfn'MOVT_def, dfn'MOVT_D_def, dfn'MOVT_S_def, 252 dfn'MOVN_D_def, dfn'MOVN_S_def, dfn'MOVZ_D_def, dfn'MOVZ_S_def, 253 dfn'DMFC1_def, dfn'DMTC1_def, dfn'MFC1_def, dfn'MTC1_def, 254 dfn'C_cond_D_def, dfn'C_cond_S_def, 255 dfn'CEIL_L_D_def, dfn'CEIL_L_S_def, dfn'CEIL_W_D_def, dfn'CEIL_W_S_def, 256 dfn'FLOOR_L_D_def, dfn'FLOOR_L_S_def, dfn'FLOOR_W_D_def, dfn'FLOOR_W_S_def, 257 dfn'ROUND_L_D_def, dfn'ROUND_L_S_def, dfn'ROUND_W_D_def, dfn'ROUND_W_S_def, 258 dfn'TRUNC_L_D_def, dfn'TRUNC_L_S_def, dfn'TRUNC_W_D_def, dfn'TRUNC_W_S_def, 259 dfn'CVT_D_L_def, dfn'CVT_D_S_def, dfn'CVT_D_W_def, dfn'CVT_L_D_def, 260 dfn'CVT_L_S_def, dfn'CVT_S_D_def, dfn'CVT_S_L_def, dfn'CVT_S_W_def, 261 dfn'CVT_W_D_def, dfn'CVT_W_S_def, 262 PostOpF32_def, PostOpF64_def, FP64_Unordered_def, FP32_Unordered_def, 263 (* IntToWordMIPS_def, IntToDWordMIPS_def, *) 264 cond_word2, cond_word3, Rounding_Mode_def, extra_cond_rand_thms] 265 [[``^st.CP0.Status.CU1``, ``~NotWordValue (^st.FGR fs)``]] [] 266 267(* ------------------------------------------------------------------------- *) 268 269(* 270val () = resetThms () 271*) 272 273(* Arithmetic/Logic instructions *) 274 275val ADDI = oEV ``dfn'ADDI (rs, rt, immediate)`` 276val DADDI = oEV ``dfn'DADDI (rs, rt, immediate)`` 277 278val ADDIU = iEV ``dfn'ADDIU (rs, rt, immediate)`` 279val DADDIU = iEV ``dfn'DADDIU (rs, rt, immediate)`` 280val SLTI = iEV ``dfn'SLTI (rs, rt, immediate)`` 281val SLTIU = iEV ``dfn'SLTIU (rs, rt, immediate)`` 282val ANDI = iEV ``dfn'ANDI (rs, rt, immediate)`` 283val ORI = iEV ``dfn'ORI (rs, rt, immediate)`` 284val XORI = iEV ``dfn'XORI (rs, rt, immediate)`` 285 286val LUI = lEV ``dfn'LUI (rt, immediate)`` 287 288val ADD = pEV ``dfn'ADD (rs, rt, rd)`` 289val SUB = pEV ``dfn'SUB (rs, rt, rd)`` 290val DADD = pEV ``dfn'DADD (rs, rt, rd)`` 291val DSUB = pEV ``dfn'DSUB (rs, rt, rd)`` 292val MOVN = pEV ``dfn'MOVN (rs, rt, rd)`` 293val MOVZ = pEV ``dfn'MOVZ (rs, rt, rd)`` 294 295val ADDU = rEV ``dfn'ADDU (rs, rt, rd)`` 296val DADDU = rEV ``dfn'DADDU (rs, rt, rd)`` 297val SUBU = rEV ``dfn'SUBU (rs, rt, rd)`` 298val DSUBU = rEV ``dfn'DSUBU (rs, rt, rd)`` 299val SLT = rEV ``dfn'SLT (rs, rt, rd)`` 300val SLTU = rEV ``dfn'SLTU (rs, rt, rd)`` 301val AND = rEV ``dfn'AND (rs, rt, rd)`` 302val OR = rEV ``dfn'OR (rs, rt, rd)`` 303val XOR = rEV ``dfn'XOR (rs, rt, rd)`` 304val NOR = rEV ``dfn'NOR (rs, rt, rd)`` 305val SLLV = rEV ``dfn'SLLV (rs, rt, rd)`` 306val SRLV = rEV ``dfn'SRLV (rs, rt, rd)`` 307val SRAV = rEV ``dfn'SRAV (rs, rt, rd)`` 308val DSLLV = rEV ``dfn'DSLLV (rs, rt, rd)`` 309val DSRLV = rEV ``dfn'DSRLV (rs, rt, rd)`` 310val DSRAV = rEV ``dfn'DSRAV (rs, rt, rd)`` 311 312val SLL = sEV ``dfn'SLL (rt, rd, sa)`` 313val SRL = sEV ``dfn'SRL (rt, rd, sa)`` 314val SRA = sEV ``dfn'SRA (rt, rd, sa)`` 315val DSLL = sEV ``dfn'DSLL (rt, rd, sa)`` 316val DSRL = sEV ``dfn'DSRL (rt, rd, sa)`` 317val DSRA = sEV ``dfn'DSRA (rt, rd, sa)`` 318val DSLL32 = sEV ``dfn'DSLL32 (rt, rd, sa)`` 319val DSRL32 = sEV ``dfn'DSRL32 (rt, rd, sa)`` 320val DSRA32 = sEV ``dfn'DSRA32 (rt, rd, sa)`` 321 322val MFHI = hEV ``dfn'MFHI (rd)`` 323val MFLO = hEV ``dfn'MFLO (rd)`` 324val MTHI = hEV ``dfn'MTHI (rd)`` 325val MTLO = hEV ``dfn'MTLO (rd)`` 326 327val MUL = rEV ``dfn'MUL (rs, rt, rd)`` 328val MADD = mEV ``dfn'MADD (rs, rt)`` 329val MADDU = mEV ``dfn'MADDU (rs, rt)`` 330val MSUB = mEV ``dfn'MSUB (rs, rt)`` 331val MSUBU = mEV ``dfn'MSUBU (rs, rt)`` 332val MULT = mEV ``dfn'MULT (rs, rt)`` 333val MULTU = mEV ``dfn'MULTU (rs, rt)`` 334val DMULT = mEV ``dfn'DMULT (rs, rt)`` 335val DMULTU = mEV ``dfn'DMULTU (rs, rt)`` 336 337val DIV = dEV ``dfn'DIV (rs, rt)`` 338val DIVU = dEV ``dfn'DIVU (rs, rt)`` 339val DDIV = dEV ``dfn'DDIV (rs, rt)`` 340val DDIVU = dEV ``dfn'DDIVU (rs, rt)`` 341 342(* ------------------------------------------------------------------------- *) 343 344(* Jumps and Branches *) 345 346val J = jEV ``dfn'J (instr_index)`` 347val JAL = jEV ``dfn'JAL (instr_index)`` 348val JR = jEV ``dfn'JR (instr_index)`` 349val JALR = hEV ``dfn'JALR (rs, rd)`` 350val BEQ = bbEV ``dfn'BEQ (rs, rt, offset)`` 351val BNE = bbEV ``dfn'BNE (rs, rt, offset)`` 352val BEQL = bbEV ``dfn'BEQL (rs, rt, offset)`` 353val BNEL = bbEV ``dfn'BNEL (rs, rt, offset)`` 354val BLEZ = bEV ``dfn'BLEZ (rs, offset)`` 355val BGTZ = bEV ``dfn'BGTZ (rs, offset)`` 356val BLTZ = bEV ``dfn'BLTZ (rs, offset)`` 357val BGEZ = bEV ``dfn'BGEZ (rs, offset)`` 358val BLTZAL = bEV ``dfn'BLTZAL (rs, offset)`` 359val BGEZAL = bEV ``dfn'BGEZAL (rs, offset)`` 360val BLEZL = bEV ``dfn'BLEZL (rs, offset)`` 361val BGTZL = bEV ``dfn'BGTZL (rs, offset)`` 362val BLTZL = bEV ``dfn'BLTZL (rs, offset)`` 363val BGEZL = bEV ``dfn'BGEZL (rs, offset)`` 364val BLTZALL = bEV ``dfn'BLTZALL (rs, offset)`` 365val BGEZALL = bEV ``dfn'BGEZALL (rs, offset)`` 366 367(* Assumes EXL is high, which permits return from exception *) 368val ERET = 369 EVR (SIMP_RULE std_ss [ASSUME ``^st.CP0.Status.EXL``, satTheory.AND_INV] o 370 COND_UPDATE_RULE) 371 [dfn'ERET_def, KernelMode_def] 372 [[``^st.CP0.Status.EXL``, ``^st.BranchDelay = NONE``]] [] ``dfn'ERET`` 373 374val BC1F = jEV ``dfn'BC1F (imm, cc)`` 375val BC1FL = jEV ``dfn'BC1FL (imm, cc)`` 376val BC1T = jEV ``dfn'BC1T (imm, cc)`` 377val BC1TL = jEV ``dfn'BC1TL (imm, cc)`` 378 379(* ------------------------------------------------------------------------- *) 380 381(* Load/Store thms and tools *) 382 383val mem_thms = 384 [AddressTranslation_def, AdjustEndian_def, LoadMemory_def, ReadData_def, 385 Drule.UNDISCH (Drule.SPEC_ALL StoreMemory_byte), 386 storeWord_def, storeDoubleword_def, 387 Drule.UNDISCH_ALL StoreMemory_half, Drule.UNDISCH_ALL StoreMemory_word, 388 Drule.UNDISCH_ALL StoreMemory_doubleword, 389 ReverseEndian_def, BigEndianMem_def, BigEndianCPU_def, 390 BYTE_def, HALFWORD_def, WORD_def, DOUBLEWORD_def, 391 address_align, address_align2, cond_sign_extend, byte_address, extract_byte, 392 wordsTheory.word_concat_0_0, wordsTheory.WORD_XOR_CLAUSES, 393 cond_word1, cond_word2, cond_word3, 394 bitstringLib.v2w_n2w_CONV ``v2w [T] : word1``, 395 bitstringLib.v2w_n2w_CONV ``v2w [F] : word1``, 396 EVAL ``((3w : word2) @@ (0w : word1)) : word3``, 397 EVAL ``word_replicate 2 (0w: word1) : word2``, 398 EVAL ``word_replicate 2 (1w: word1) : word2``, 399 EVAL ``((1w:word1) @@ (0w:word2)) : word3``, 400 EVAL ``(word_replicate 2 (0w:word1) : word2 @@ (0w:word1)) : word3``, 401 EVAL ``(word_replicate 2 (1w:word1) : word2 @@ (0w:word1)) : word3``, 402 EVAL ``word_replicate 3 (0w:word1) : word3``, 403 EVAL ``word_replicate 3 (1w:word1) : word3``] 404 405val select_rule = 406 utilsLib.ALL_HYP_CONV_RULE (REWRITE_CONV [Aligned_thms]) o 407 REWRITE_RULE 408 [select_byte_le, select_byte_be, byte_address, 409 SIMP_RULE (bool_ss++boolSimps.LET_ss) [] select_parts, 410 wordsTheory.WORD_XOR_ASSOC, wordsTheory.WORD_XOR_CLAUSES] o 411 utilsLib.INST_REWRITE_RULE 412 [select_half_le, select_half_be, 413 select_word_le, select_word_be, 414 select_pc_le, select_pc_be] 415 416val memcntxts = 417 [[``~^st.CP0.Status.RE``, ``^st.CP0.Config.BE``], 418 [``~^st.CP0.Status.RE``, ``~^st.CP0.Config.BE``]] 419 420(* 421val memcntxts = 422 [[``FST (UserMode ^st)``, ``^st.CP0.Status.RE``, ``^st.CP0.Config.BE``], 423 [``~FST (UserMode ^st)``, ``^st.CP0.Status.RE``, ``^st.CP0.Config.BE``], 424 [``~^st.CP0.Status.RE``, ``^st.CP0.Config.BE``], 425 [ ``FST (UserMode ^st)``, ``^st.CP0.Status.RE``, ``~^st.CP0.Config.BE``], 426 [``~FST (UserMode ^st)``, ``^st.CP0.Status.RE``, ``~^st.CP0.Config.BE``], 427 [``~^st.CP0.Status.RE``, ``~^st.CP0.Config.BE``]] 428*) 429 430val addr = ``sw2sw (offset:word16) + if base = 0w then 0w else ^st.gpr base`` 431 432val unaligned_memcntxts = 433 List.map (fn l => [``rt <> 0w:word5``, ``~^st.exceptionSignalled``] @ l) 434 memcntxts 435 436val memcntxts = 437 List.map 438 (fn l => 439 [``rt <> 0w:word5``, 440 ``~^st.exceptionSignalled``, 441 ``Aligned (^addr, 1w)``, 442 ``Aligned (^addr, 3w)``, 443 ``Aligned (^st.PC, 3w)``] @ l) 444 memcntxts 445 446val dmemcntxts = 447 List.map (fn l => ``Aligned (^addr, 7w)`` :: l) memcntxts 448 449(* 450fun merge_cases thms = 451 let 452 fun thm i = List.nth (thms, i) 453 in 454 utilsLib.MERGE_CASES ``^st.CP0.Config.BE`` 455 (utilsLib.MERGE_CASES ``^st.CP0.Status.RE`` 456 (utilsLib.MERGE_CASES ``FST (UserMode ^st)`` (thm 0) (thm 1)) 457 (thm 2)) 458 (utilsLib.MERGE_CASES ``^st.CP0.Status.RE`` 459 (utilsLib.MERGE_CASES ``FST (UserMode ^st)`` (thm 3) (thm 4)) 460 (thm 5)) 461 end 462*) 463 464fun merge_cases thms = 465 let 466 fun thm i = List.nth (thms, i) 467 in 468 utilsLib.MERGE_CASES ``^st.CP0.Config.BE`` (thm 0) (thm 1) 469 end 470 471fun EVL l tm = 472 let 473 val thm = 474 SIMP_CONV std_ss [dfn'LB_def, dfn'LBU_def, 475 dfn'LH_def, dfn'LHU_def, 476 dfn'LW_def, dfn'LWU_def, 477 dfn'LL_def, dfn'LD_def, dfn'LLD_def] tm 478 in 479 List.map (fn th => Conv.RIGHT_CONV_RULE (REWRITE_CONV [th]) thm) l 480 |> addThms 481 end 482 483fun store_rule thms = 484 utilsLib.ALL_HYP_CONV_RULE 485 (SIMP_CONV std_ss (Aligned_thms :: cond_rand_thms :: mem_thms @ thms)) 486 487(* 488val UserMode_rule = 489 List.map 490 (utilsLib.ALL_HYP_CONV_RULE 491 (REWRITE_CONV [UserMode_def, boolTheory.DE_MORGAN_THM])) 492*) 493 494(* ------------------------------------------------------------------------- *) 495 496(* Load instructions *) 497 498val loadByte = 499 evr select_rule (loadByte_def :: mem_thms) memcntxts [] 500 ``loadByte (base, rt, offset, unsigned)`` 501 |> merge_cases 502 503val loadHalf = 504 evr select_rule (loadHalf_def :: mem_thms) memcntxts [] 505 ``loadHalf (base, rt, offset, unsigned)`` 506 507val loadWord = 508 evr select_rule (loadWord_def :: mem_thms) memcntxts [] 509 ``loadWord (link, base, rt, offset, unsigned)`` 510 511val loadDoubleword = 512 evr select_rule ([loadDoubleword_def, double_aligned] @ mem_thms) 513 dmemcntxts [] 514 ``loadDoubleword (link, base, rt, offset)`` 515 516val LB = EVL [loadByte] ``dfn'LB (base, rt, offset) ^st`` 517val LBU = EVL [loadByte] ``dfn'LBU (base, rt, offset) ^st`` 518 519val LH = EVL loadHalf ``dfn'LH (base, rt, offset) ^st`` 520val LHU = EVL loadHalf ``dfn'LHU (base, rt, offset) ^st`` 521 522val LW = EVL loadWord ``dfn'LW (base, rt, offset) ^st`` 523val LWU = EVL loadWord ``dfn'LWU (base, rt, offset) ^st`` 524val LL = EVL loadWord ``dfn'LL (base, rt, offset) ^st`` 525 526val LD = EVL loadDoubleword ``dfn'LD (base, rt, offset) ^st`` 527val LLD = EVL loadDoubleword ``dfn'LLD (base, rt, offset) ^st`` 528 529val LWL = 530 EVR select_rule (dfn'LWL_def :: mem_thms) unaligned_memcntxts [] 531 ``dfn'LWL (base, rt, offset)`` 532 533val LWR = 534 EVR select_rule (dfn'LWR_def :: mem_thms) unaligned_memcntxts [] 535 ``dfn'LWR (base, rt, offset)`` 536 537val LDL = 538 EVR select_rule (dfn'LDL_def :: mem_thms) unaligned_memcntxts [] 539 ``dfn'LDL (base, rt, offset)`` 540 541val LDR = 542 EVR select_rule (dfn'LDR_def :: mem_thms) unaligned_memcntxts [] 543 ``dfn'LDR (base, rt, offset)`` 544 545(* Store instructions *) 546 547val SB = 548 ev (dfn'SB_def :: mem_thms) memcntxts [] 549 ``dfn'SB (base, rt, offset)`` 550 |> merge_cases 551 |> Lib.list_of_singleton 552 |> addThms 553 554val SH = 555 EVR (store_rule [bit_0_2_0, bit_0_2_0_6]) 556 ([dfn'SH_def, extract_half] @ mem_thms) memcntxts [] 557 ``dfn'SH (base, rt, offset)`` 558 559val SW = 560 EVR (store_rule [bit_1_0_2_0, bit_1_0_2_0_4]) 561 ([dfn'SW_def, extract_word] @ mem_thms) memcntxts [] 562 ``dfn'SW (base, rt, offset)`` 563 564val SD = 565 EVR (store_rule []) (dfn'SD_def :: mem_thms) dmemcntxts [] 566 ``dfn'SD (base, rt, offset)`` 567 568(* 569val sc = List.map (fn l => ``^st.LLbit = SOME llbit`` :: l) 570 571val SC = 572 EVR (COND_UPDATE_RULE o store_rule [bit_1_0_2_0, bit_1_0_2_0_4]) 573 ([dfn'SC_def, extract_word] @ mem_thms) (sc memcntxts) [] 574 ``dfn'SC (base, rt, offset)`` 575 576val SCD = 577 EVR (COND_UPDATE_RULE o store_rule []) 578 ([dfn'SCD_def, extract_word] @ mem_thms) (sc dmemcntxts) [] 579 ``dfn'SCD (base, rt, offset)`` 580*) 581 582(* ------------------------------------------------------------------------- *) 583 584(* Floating-point instructions *) 585 586val ABS_D = fpEV ``dfn'ABS_D (fd, fs)`` 587val ABS_S = fpEV ``dfn'ABS_S (fd, fs)`` 588val ADD_D = fpEV ``dfn'ADD_D (fd, fs, ft)`` 589val ADD_S = fpEV ``dfn'ADD_S (fd, fs, ft)`` 590val DIV_D = fpEV ``dfn'DIV_D (fd, fs, ft)`` 591val DIV_S = fpEV ``dfn'DIV_S (fd, fs, ft)`` 592val MADD_D = fpEV ``dfn'MADD_D (fd, fr, fs, ft)`` 593val MADD_S = fpEV ``dfn'MADD_S (fd, fr, fs, ft)`` 594val MSUB_D = fpEV ``dfn'MSUB_D (fd, fr, fs, ft)`` 595val MSUB_S = fpEV ``dfn'MSUB_S (fd, fr, fs, ft)`` 596val MUL_D = fpEV ``dfn'MUL_D (fd, fs, ft)`` 597val MUL_S = fpEV ``dfn'MUL_S (fd, fs, ft)`` 598val NEG_D = fpEV ``dfn'NEG_D (fd, fs)`` 599val NEG_S = fpEV ``dfn'NEG_S (fd, fs)`` 600val SQRT_D = fpEV ``dfn'SQRT_D (fd, fs)`` 601val SQRT_S = fpEV ``dfn'SQRT_S (fd, fs)`` 602val SUB_D = fpEV ``dfn'SUB_D (fd, fs, ft)`` 603val SUB_S = fpEV ``dfn'SUB_S (fd, fs, ft)`` 604 605val C_cond_D = fpEV ``dfn'C_cond_D (fs, ft, cnd, cc)`` 606val C_cond_S = fpEV ``dfn'C_cond_S (fs, ft, cnd, cc)`` 607 608val CEIL_L_D = fpEV ``dfn'CEIL_L_D (fd, fs)`` 609val CEIL_L_S = fpEV ``dfn'CEIL_L_S (fd, fs)`` 610val CEIL_W_D = fpEV ``dfn'CEIL_W_D (fd, fs)`` 611val CEIL_W_S = fpEV ``dfn'CEIL_W_S (fd, fs)`` 612val FLOOR_L_D = fpEV ``dfn'FLOOR_L_D (fd, fs)`` 613val FLOOR_L_S = fpEV ``dfn'FLOOR_L_S (fd, fs)`` 614val FLOOR_W_D = fpEV ``dfn'FLOOR_W_D (fd, fs)`` 615val FLOOR_W_S = fpEV ``dfn'FLOOR_W_S (fd, fs)`` 616val ROUND_L_D = fpEV ``dfn'ROUND_L_D (fd, fs)`` 617val ROUND_L_S = fpEV ``dfn'ROUND_L_S (fd, fs)`` 618val ROUND_W_D = fpEV ``dfn'ROUND_W_D (fd, fs)`` 619val ROUND_W_S = fpEV ``dfn'ROUND_W_S (fd, fs)`` 620val TRUNC_L_D = fpEV ``dfn'TRUNC_L_D (fd, fs)`` 621val TRUNC_L_S = fpEV ``dfn'TRUNC_L_S (fd, fs)`` 622val TRUNC_W_D = fpEV ``dfn'TRUNC_W_D (fd, fs)`` 623val TRUNC_W_S = fpEV ``dfn'TRUNC_W_S (fd, fs)`` 624 625val CVT_D_L = fpEV ``dfn'CVT_D_L (fd, fs)`` 626val CVT_D_S = fpEV ``dfn'CVT_D_S (fd, fs)`` 627val CVT_D_W = fpEV ``dfn'CVT_D_W (fd, fs)`` 628val CVT_L_D = fpEV ``dfn'CVT_L_D (fd, fs)`` 629val CVT_L_S = fpEV ``dfn'CVT_L_S (fd, fs)`` 630val CVT_S_D = fpEV ``dfn'CVT_S_D (fd, fs)`` 631val CVT_S_L = fpEV ``dfn'CVT_S_L (fd, fs)`` 632val CVT_S_W = fpEV ``dfn'CVT_S_W (fd, fs)`` 633val CVT_W_D = fpEV ``dfn'CVT_W_D (fd, fs)`` 634val CVT_W_S = fpEV ``dfn'CVT_W_S (fd, fs)`` 635 636val MOV_D = fpEV ``dfn'MOV_D (fd, fs)`` 637val MOV_S = fpEV ``dfn'MOV_S (fd, fs)`` 638val MOVF = fpEV ``dfn'MOVF (rd, fs, cc)`` 639val MOVF_D = fpEV ``dfn'MOVF_D (fd, fs, cc)`` 640val MOVF_S = fpEV ``dfn'MOVF_S (fd, fs, cc)`` 641val MOVT = fpEV ``dfn'MOVT (rd, fs, cc)`` 642val MOVT_D = fpEV ``dfn'MOVT_D (fd, fs, cc)`` 643val MOVT_S = fpEV ``dfn'MOVT_S (fd, fs, cc)`` 644val MOVN_D = fpEV ``dfn'MOVN_D (fd, fs, cc)`` 645val MOVN_S = fpEV ``dfn'MOVN_S (fd, fs, cc)`` 646val MOVZ_D = fpEV ``dfn'MOVZ_D (fd, fs, cc)`` 647val MOVZ_S = fpEV ``dfn'MOVZ_S (fd, fs, cc)`` 648 649val DMFC1 = fpEV ``dfn'DMFC1 (rd, fs)`` 650val DMTC1 = fpEV ``dfn'DMTC1 (rd, fs)`` 651val MFC1 = fpEV ``dfn'MFC1 (rd, fs)`` 652val MTC1 = fpEV ``dfn'MTC1 (rd, fs)`` 653 654(* ------------------------------------------------------------------------- *) 655 656(* Coprocessor 0 instructions *) 657 658val cps = mapl (`rd`, List.map reg [23, 26]) : utilsLib.cover 659 660val MTC0 = 661 EV [dfn'MTC0_def, extra_cond_rand_thms] [] cps 662 ``dfn'MTC0 (rt, rd, v2w [F; F; F])`` 663 664val MFC0 = 665 EV [dfn'MFC0_def, cast_thms] [[``rt <> 0w: word5``]] cps 666 ``dfn'MFC0 (rt, rd, v2w [F; F; F])`` 667 668(* ------------------------------------------------------------------------- *) 669 670(* Fetch *) 671 672val Fetch = evr select_rule (Fetch_def :: mem_thms) memcntxts [] ``Fetch`` 673 674local 675 fun bytes4 l = 676 let 677 val (b1, l) = Lib.split_after 8 l 678 val (b2, l) = Lib.split_after 8 l 679 val (b3, b4) = Lib.split_after 8 l 680 in 681 (b1, b2, b3, b4) 682 end 683 fun build_byte n l = 684 List.tabulate 685 (8, fn i => (bitstringSyntax.mk_bit (7 - i + n) |-> List.nth (l, i))) 686 val mk_byte = bitstringSyntax.mk_vec 8 687 val conc_rule = 688 SIMP_RULE (srw_ss()++boolSimps.LET_ss) 689 [bitstringTheory.fixwidth_def, bitstringTheory.field_def, 690 bitstringTheory.shiftr_def, bitstringTheory.w2w_v2w] o 691 ONCE_REWRITE_RULE [bitstringTheory.word_concat_v2w_rwt] 692 val rule = 693 Lib.funpow 3 conc_rule o 694 REWRITE_RULE 695 (List.map ASSUME 696 [ 697 ``^st.MEM s.PC = ^(mk_byte 0)``, 698 ``^st.MEM (s.PC + 1w) = ^(mk_byte 8)``, 699 ``^st.MEM (s.PC + 2w) = ^(mk_byte 16)``, 700 ``^st.MEM (s.PC + 3w) = ^(mk_byte 24)`` 701 ]) 702 fun fetch_thm i = rule (List.nth (Fetch, i)) 703 val Fetch_be = fetch_thm 0 704 val Fetch_le = fetch_thm 1 705in 706 fun pad_opcode v = 707 let 708 val (l, ty) = listSyntax.dest_list v 709 val () = ignore (ty = Type.bool andalso List.length l <= 32 orelse 710 raise ERR "pad_opcode" "bad opcode") 711 in 712 utilsLib.padLeft boolSyntax.F 32 l 713 end 714 fun fetch be v = 715 let 716 val (b1, b2, b3, b4) = bytes4 (pad_opcode v) 717 val (thm, s) = 718 if be 719 then (Fetch_be, 720 build_byte 24 b4 @ build_byte 16 b3 @ 721 build_byte 8 b2 @ build_byte 0 b1) 722 else (Fetch_le, 723 build_byte 24 b1 @ build_byte 16 b2 @ 724 build_byte 8 b3 @ build_byte 0 b4) 725 in 726 Thm.INST s thm 727 end 728 fun fetch_hex be = fetch be o bitstringSyntax.bitstring_of_hexstring 729end 730 731(* ------------------------------------------------------------------------- *) 732 733(* Decoder *) 734 735local 736 val Decode = 737 Decode_def 738 |> Thm.SPEC (bitstringSyntax.mk_vec 32 0) 739 |> Conv.RIGHT_CONV_RULE 740 ( 741 REWRITE_CONV [mipsTheory.boolify32_v2w, mipsTheory.boolify26_v2w, 742 mipsTheory.boolify5_v2w, 743 COP1Decode_def, COP3Decode_def, MOVCIDecode_def] 744 THENC Conv.DEPTH_CONV PairedLambda.let_CONV 745 THENC Conv.DEPTH_CONV bitstringLib.extract_v2w_CONV 746 ) 747 val v = fst (bitstringSyntax.dest_v2w (bitstringSyntax.mk_vec 32 0)) 748 val unpredictable_tm = ``mips$Unpredictable`` 749 fun fix_unpredictable thm = 750 let 751 val thm = REWRITE_RULE [not31] thm 752 in 753 case Lib.total (boolSyntax.dest_cond o utilsLib.rhsc) thm of 754 SOME (b, t, _) => 755 if t = unpredictable_tm 756 then REWRITE_RULE [ASSUME (boolSyntax.mk_neg b)] thm 757 else thm 758 | _ => thm 759 end 760in 761 fun DecodeMIPS pat = 762 let 763 val s = fst (Term.match_term v pat) 764 in 765 Decode |> Thm.INST s 766 |> REWRITE_RULE [] 767 |> Conv.RIGHT_CONV_RULE (Conv.REPEATC PairedLambda.let_CONV) 768 |> fix_unpredictable 769 end 770end 771 772val mips_ipatterns = List.map (I ## utilsLib.pattern) 773 [ 774 ("ADDI", "FFTFFF__________________________"), 775 ("ADDIU", "FFTFFT__________________________"), 776 ("SLTI", "FFTFTF__________________________"), 777 ("SLTIU", "FFTFTT__________________________"), 778 ("ANDI", "FFTTFF__________________________"), 779 ("ORI", "FFTTFT__________________________"), 780 ("XORI", "FFTTTF__________________________"), 781 ("DADDI", "FTTFFF__________________________"), 782 ("DADDIU", "FTTFFT__________________________"), 783 ("MULT", "FFFFFF__________FFFFFFFFFFFTTFFF"), 784 ("MULTU", "FFFFFF__________FFFFFFFFFFFTTFFT"), 785 ("DMULT", "FFFFFF__________FFFFFFFFFFFTTTFF"), 786 ("DMULTU", "FFFFFF__________FFFFFFFFFFFTTTFT"), 787 ("MADD", "FTTTFF__________FFFFFFFFFFFFFFFF"), 788 ("MADDU", "FTTTFF__________FFFFFFFFFFFFFFFT"), 789 ("MSUB", "FTTTFF__________FFFFFFFFFFFFFTFF"), 790 ("MSUBU", "FTTTFF__________FFFFFFFFFFFFFTFT"), 791 ("MUL", "FTTTFF_______________FFFFFFFFFTF"), 792 ("BEQ", "FFFTFF__________________________"), 793 ("BNE", "FFFTFT__________________________"), 794 ("BEQL", "FTFTFF__________________________"), 795 ("BNEL", "FTFTFT__________________________") 796 ] 797 798val mips_dpatterns = List.map (I ## utilsLib.pattern) 799 [ 800 ("JALR", "FFFFFF_____FFFFF__________FFTFFT") 801 ] 802 803val mips_rpatterns = List.map (I ## utilsLib.pattern) 804 [ 805 ("SLLV", "FFFFFF_______________FFFFFFFFTFF"), 806 ("SRLV", "FFFFFF_______________FFFFFFFFTTF"), 807 ("SRAV", "FFFFFF_______________FFFFFFFFTTT"), 808 ("MOVZ", "FFFFFF_______________FFFFFFFTFTF"), 809 ("MOVN", "FFFFFF_______________FFFFFFFTFTT"), 810 ("DSLLV", "FFFFFF_______________FFFFFFTFTFF"), 811 ("DSRLV", "FFFFFF_______________FFFFFFTFTTF"), 812 ("DSRAV", "FFFFFF_______________FFFFFFTFTTT"), 813 ("ADD", "FFFFFF_______________FFFFFTFFFFF"), 814 ("ADDU", "FFFFFF_______________FFFFFTFFFFT"), 815 ("SUB", "FFFFFF_______________FFFFFTFFFTF"), 816 ("SUBU", "FFFFFF_______________FFFFFTFFFTT"), 817 ("AND", "FFFFFF_______________FFFFFTFFTFF"), 818 ("OR", "FFFFFF_______________FFFFFTFFTFT"), 819 ("XOR", "FFFFFF_______________FFFFFTFFTTF"), 820 ("NOR", "FFFFFF_______________FFFFFTFFTTT"), 821 ("SLT", "FFFFFF_______________FFFFFTFTFTF"), 822 ("SLTU", "FFFFFF_______________FFFFFTFTFTT"), 823 ("DADD", "FFFFFF_______________FFFFFTFTTFF"), 824 ("DADDU", "FFFFFF_______________FFFFFTFTTFT"), 825 ("DSUB", "FFFFFF_______________FFFFFTFTTTF"), 826 ("DSUBU", "FFFFFF_______________FFFFFTFTTTT"), 827 ("MOVF", "FFFFFF________FF_____FFFFFFFFFFT"), 828 ("MOVT", "FFFFFF________FT_____FFFFFFFFFFT") 829 ] 830 831val mips_jpatterns = List.map (I ## utilsLib.pattern) 832 [ 833 ("SLL", "FFFFFFFFFFF_______________FFFFFF"), 834 ("SRL", "FFFFFFFFFFF_______________FFFFTF"), 835 ("SRA", "FFFFFFFFFFF_______________FFFFTT"), 836 ("DSLL", "FFFFFFFFFFF_______________TTTFFF"), 837 ("DSRL", "FFFFFFFFFFF_______________TTTFTF"), 838 ("DSRA", "FFFFFFFFFFF_______________TTTFTT"), 839 ("DSLL32", "FFFFFFFFFFF_______________TTTTFF"), 840 ("DSRL32", "FFFFFFFFFFF_______________TTTTTF"), 841 ("DSRA32", "FFFFFFFFFFF_______________TTTTTT") 842 ] 843 844val mips_patterns0 = List.map (I ## utilsLib.pattern) 845 [ 846 ("LUI", "FFTTTTFFFFF_____________________"), 847 ("DIV", "FFFFFF__________FFFFFFFFFFFTTFTF"), 848 ("DIVU", "FFFFFF__________FFFFFFFFFFFTTFTT"), 849 ("DDIV", "FFFFFF__________FFFFFFFFFFFTTTTF"), 850 ("DDIVU", "FFFFFF__________FFFFFFFFFFFTTTTT"), 851 ("MTHI", "FFFFFF_____FFFFFFFFFFFFFFFFTFFFT"), 852 ("MTLO", "FFFFFF_____FFFFFFFFFFFFFFFFTFFTT"), 853 ("MFHI", "FFFFFFFFFFFFFFFF_____FFFFFFTFFFF"), 854 ("MFLO", "FFFFFFFFFFFFFFFF_____FFFFFFTFFTF"), 855 ("BLTZ", "FFFFFT_____FFFFF________________"), 856 ("BGEZ", "FFFFFT_____FFFFT________________"), 857 ("BLTZL", "FFFFFT_____FFFTF________________"), 858 ("BGEZL", "FFFFFT_____FFFTT________________"), 859 ("BLTZAL", "FFFFFT_____TFFFF________________"), 860 ("BGEZAL", "FFFFFT_____TFFFT________________"), 861 ("BLTZALL", "FFFFFT_____TFFTF________________"), 862 ("BGEZALL", "FFFFFT_____TFFTT________________"), 863 ("BLEZ", "FFFTTF_____FFFFF________________"), 864 ("BGTZ", "FFFTTT_____FFFFF________________"), 865 ("BLEZL", "FTFTTF_____FFFFF________________"), 866 ("BGTZL", "FTFTTT_____FFFFF________________"), 867 ("JR", "FFFFFF_____FFFFFFFFFF_____FFTFFF"), 868 ("MFC1", "FTFFFTFFFFF__________FFFFFFFFFFF"), 869 ("DMFC1", "FTFFFTFFFFT__________FFFFFFFFFFF"), 870 ("MTC1", "FTFFFTFFTFF__________FFFFFFFFFFF"), 871 ("DMTC1", "FTFFFTFFTFT__________FFFFFFFFFFF") 872 ] 873 874val mips_cpatterns = List.map (I ## utilsLib.pattern) 875 [ 876 ("MFC0", "FTFFFFFFFFF__________FFFFFFFF___"), 877 ("MTC0", "FTFFFFFFTFF__________FFFFFFFF___") 878 ] 879 880val mips_patterns = List.map (I ## utilsLib.pattern) 881 [ 882 ("J", "FFFFTF__________________________"), 883 ("JAL", "FFFFTT__________________________"), 884 ("LDL", "FTTFTF__________________________"), 885 ("LDR", "FTTFTT__________________________"), 886 ("LB", "TFFFFF__________________________"), 887 ("LH", "TFFFFT__________________________"), 888 ("LWL", "TFFFTF__________________________"), 889 ("LW", "TFFFTT__________________________"), 890 ("LBU", "TFFTFF__________________________"), 891 ("LHU", "TFFTFT__________________________"), 892 ("LWR", "TFFTTF__________________________"), 893 ("LWU", "TFFTTT__________________________"), 894 ("SB", "TFTFFF__________________________"), 895 ("SH", "TFTFFT__________________________"), 896 ("SW", "TFTFTT__________________________"), 897 ("LL", "TTFFFF__________________________"), 898 ("LLD", "TTFTFF__________________________"), 899 ("LD", "TTFTTT__________________________"), 900 (* ("SC", "TTTFFF__________________________"), 901 ("SCD", "TTTTFF__________________________"), *) 902 ("SD", "TTTTTT__________________________"), 903 ("ERET", "FTFFFFTFFFFFFFFFFFFFFFFFFFFTTFFF"), 904 ("BC1F", "FTFFFTFTFFF___FF________________"), 905 ("BC1T", "FTFFFTFTFFF___FT________________"), 906 ("BC1FL", "FTFFFTFTFFF___TF________________"), 907 ("BC1TL", "FTFFFTFTFFF___TT________________"), 908 ("ADD.S", "FTFFFTTFFFF_______________FFFFFF"), 909 ("SUB.S", "FTFFFTTFFFF_______________FFFFFT"), 910 ("MUL.S", "FTFFFTTFFFF_______________FFFFTF"), 911 ("DIV.S", "FTFFFTTFFFF_______________FFFFTT"), 912 ("SQRT.S", "FTFFFTTFFFFFFFFF__________FFFTFF"), 913 ("ABS.S", "FTFFFTTFFFFFFFFF__________FFFTFT"), 914 ("MOV.S", "FTFFFTTFFFFFFFFF__________FFFTTF"), 915 ("NEG.S", "FTFFFTTFFFFFFFFF__________FFFTTT"), 916 ("ROUND.L.S","FTFFFTTFFFFFFFFF__________FFTFFF"), 917 ("TRUNC.L.S","FTFFFTTFFFFFFFFF__________FFTFFT"), 918 ("CEIL.L.S", "FTFFFTTFFFFFFFFF__________FFTFTF"), 919 ("FLOOR.L.S","FTFFFTTFFFFFFFFF__________FFTFTT"), 920 ("ROUND.W.S","FTFFFTTFFFFFFFFF__________FFTTFF"), 921 ("TRUNC.W.S","FTFFFTTFFFFFFFFF__________FFTTFT"), 922 ("CEIL.W.S", "FTFFFTTFFFFFFFFF__________FFTTTF"), 923 ("FLOOR.W.S","FTFFFTTFFFFFFFFF__________FFTTTT"), 924 ("MOVF.S", "FTFFFTTFFFF___FF__________FTFFFT"), 925 ("MOVT.S", "FTFFFTTFFFF___FT__________FTFFFT"), 926 ("MOVZ.S", "FTFFFTTFFFF_______________FTFFTF"), 927 ("MOVN.S", "FTFFFTTFFFF_______________FTFFTT"), 928 ("C.cond.S", "FTFFFTTFFFF_____________FFTTF___"), 929 ("ADD.D", "FTFFFTTFFFT_______________FFFFFF"), 930 ("SUB.D", "FTFFFTTFFFT_______________FFFFFT"), 931 ("MUL.D", "FTFFFTTFFFT_______________FFFFTF"), 932 ("DIV.D", "FTFFFTTFFFT_______________FFFFTT"), 933 ("SQRT.D", "FTFFFTTFFFTFFFFF__________FFFTFF"), 934 ("ABS.D", "FTFFFTTFFFTFFFFF__________FFFTFT"), 935 ("MOV.D", "FTFFFTTFFFTFFFFF__________FFFTTF"), 936 ("NEG.D", "FTFFFTTFFFTFFFFF__________FFFTTT"), 937 ("ROUND.L.D","FTFFFTTFFFTFFFFF__________FFTFFF"), 938 ("TRUNC.L.D","FTFFFTTFFFTFFFFF__________FFTFFT"), 939 ("CEIL.L.D", "FTFFFTTFFFTFFFFF__________FFTFTF"), 940 ("FLOOR.L.D","FTFFFTTFFFTFFFFF__________FFTFTT"), 941 ("ROUND.W.D","FTFFFTTFFFTFFFFF__________FFTTFF"), 942 ("TRUNC.W.D","FTFFFTTFFFTFFFFF__________FFTTFT"), 943 ("CEIL.W.D", "FTFFFTTFFFTFFFFF__________FFTTTF"), 944 ("FLOOR.W.D","FTFFFTTFFFTFFFFF__________FFTTTT"), 945 ("MOVF.D", "FTFFFTTFFFT___FF__________FTFFFT"), 946 ("MOVT.D", "FTFFFTTFFFT___FT__________FTFFFT"), 947 ("MOVZ.D", "FTFFFTTFFFT_______________FTFFTF"), 948 ("MOVN.D", "FTFFFTTFFFT_______________FTFFTT"), 949 ("C.cond.D", "FTFFFTTFFFT_____________FFTTF___"), 950 ("CVT.S.D", "FTFFFTTFFFTFFFFF__________TFFFFF"), 951 ("CVT.S.W", "FTFFFTTFTFFFFFFF__________TFFFFF"), 952 ("CVT.S.L", "FTFFFTTFTFTFFFFF__________TFFFFF"), 953 ("CVT.D.S", "FTFFFTTFFFFFFFFF__________TFFFFT"), 954 ("CVT.D.W", "FTFFFTTFTFFFFFFF__________TFFFFT"), 955 ("CVT.D.L", "FTFFFTTFTFTFFFFF__________TFFFFT"), 956 ("CVT.W.S", "FTFFFTTFFFFFFFFF__________TFFTFF"), 957 ("CVT.W.S", "FTFFFTTFFFTFFFFF__________TFFTFF"), 958 ("CVT.L.S", "FTFFFTTFFFFFFFFF__________TFFTFT"), 959 ("CVT.L.S", "FTFFFTTFFFTFFFFF__________TFFTFT"), 960 ("MADD.S", "FTFFTT____________________TFFFFF"), 961 ("MADD.D", "FTFFTT____________________TFFFFT"), 962 ("MSUB.S", "FTFFTT____________________TFTFFF"), 963 ("MSUB.D", "FTFFTT____________________TFTFFT") 964 ] 965 966local 967 val patterns = 968 List.concat [mips_ipatterns, mips_jpatterns, mips_dpatterns, 969 mips_rpatterns, mips_patterns0, mips_cpatterns, 970 mips_patterns] 971 fun padded_opcode v = listSyntax.mk_list (pad_opcode v, Type.bool) 972 val get_opc = boolSyntax.rand o boolSyntax.rand o utilsLib.lhsc 973 fun mk_net l = 974 List.foldl 975 (fn ((s:string, p), nt) => 976 let 977 val thm = DecodeMIPS p 978 in 979 LVTermNet.insert (nt, ([], get_opc thm), (s, thm)) 980 end) 981 LVTermNet.empty l 982 fun find_opcode net = 983 let 984 fun find_opc tm = 985 case LVTermNet.match (net, tm) of 986 [(([], opc), (name, thm))] => SOME (name:string, opc, thm:thm) 987 | _ => NONE 988 in 989 fn v => 990 let 991 val pv = padded_opcode v 992 in 993 Option.map 994 (fn (name, opc, thm) => 995 (name, opc, thm, fst (Term.match_term opc pv))) 996 (find_opc pv) 997 end 998 end 999 fun x i = Term.mk_var ("x" ^ Int.toString i, Type.bool) 1000 fun assign_bits (p, i, n) = 1001 let 1002 val l = (i, n) |> (Arbnum.fromInt ## Lib.I) 1003 |> bitstringSyntax.padded_fixedwidth_of_num 1004 |> bitstringSyntax.dest_v2w |> fst 1005 |> listSyntax.dest_list |> fst 1006 in 1007 Term.subst (Lib.mapi (fn i => fn b => x (i + p) |-> b) l) 1008 end 1009 val r0 = assign_bits (0, 0, 5) 1010 val r5 = assign_bits (5, 0, 5) 1011 val r10 = assign_bits (10, 0, 5) 1012 val sel = assign_bits (10, 0, 3) 1013 val dbg = assign_bits (5, 23, 5) o sel 1014 val err = assign_bits (5, 26, 5) o sel 1015 fun fnd l = find_opcode (mk_net l) 1016 fun fnd2 l tm = Option.map (fn (s, t, _, _) => (s, t)) (fnd l tm) 1017 fun sb l = 1018 all_comb 1019 (List.map 1020 (fn (x, f:term -> term) => (fn (s, t) => (s ^ "_" ^ x, f t))) l) 1021 val fnd_sb = fnd2 ## sb 1022 val fp = fnd_sb (mips_patterns, []) 1023 val f0 = fnd_sb (mips_patterns0, [("0", r0)]) 1024 val fd = fnd_sb (mips_dpatterns, [("d0", r10)]) 1025 val fi = fnd_sb (mips_ipatterns, [("s0", r0), ("t0", r5)]) 1026 val fj = fnd_sb (mips_jpatterns, [("t0", r0), ("d0", r5)]) 1027 val fr = fnd_sb (mips_rpatterns, [("s0", r0), ("t0", r5), ("d0", r10)]) 1028 val fc = (fnd2 mips_cpatterns, 1029 [[fn (s, t) => (s ^ "_debug", dbg t)], 1030 [fn (s, t) => (s ^ "_errctl", err t)]]) 1031 fun try_patterns [] tm = [] 1032 | try_patterns ((f, l) :: r) tm = 1033 (case f tm of 1034 SOME x => List.map (List.foldl (fn (f, a) => f a) x) l 1035 | NONE => try_patterns r tm) 1036 val find_opc = try_patterns [fi, fr, fp, fj, fd, f0, fc] 1037 val mips_find_opc_ = fnd patterns 1038in 1039 val hex_to_padded_opcode = 1040 padded_opcode o bitstringSyntax.bitstring_of_hexstring 1041 fun mips_decode v = 1042 case mips_find_opc_ v of 1043 SOME (_, _, thm, s) => if List.null s then thm else Thm.INST s thm 1044 | NONE => raise ERR "decode" (utilsLib.long_term_to_string v) 1045 val mips_decode_hex = mips_decode o hex_to_padded_opcode 1046 fun mips_find_opc opc = 1047 let 1048 val l = find_opc opc 1049 in 1050 List.filter (fn (_, p) => Lib.can (Term.match_term p) opc) l 1051 end 1052 val mips_dict = Redblackmap.fromList String.compare patterns 1053 (* fun mk_mips_pattern s = Redblackmap.peek (dict, utilsLib.uppercase s) *) 1054end 1055 1056(* 1057 List.map (mips_decode o snd) (Redblackmap.listItems mips_dict) 1058*) 1059 1060(* ------------------------------------------------------------------------- *) 1061 1062(* Evaluator *) 1063 1064local 1065 val eval_simp_rule = 1066 utilsLib.ALL_HYP_CONV_RULE 1067 (Conv.DEPTH_CONV wordsLib.word_EQ_CONV 1068 THENC REWRITE_CONV [v2w_0_rwts]) 1069 fun eval0 tm rwt = 1070 let 1071 val thm = eval_simp_rule (utilsLib.INST_REWRITE_CONV1 rwt tm) 1072 in 1073 if utilsLib.vacuous thm then NONE else SOME thm 1074 end 1075 val be_tm = ``^st.CP0.Config.BE`` 1076 val le_tm = boolSyntax.mk_neg be_tm 1077 val base_tms = [``~^st.CP0.Status.RE``] 1078 fun find_thm be = 1079 let 1080 val tms = (if be then be_tm else le_tm) :: base_tms 1081 in 1082 utilsLib.find_rw (utilsLib.mk_rw_net utilsLib.lhsc (getThms tms)) 1083 end 1084in 1085 fun eval be = 1086 let 1087 val fnd = find_thm be 1088 in 1089 fn tm => 1090 let 1091 fun err s = (Parse.print_term tm; print "\n"; raise ERR "eval" s) 1092 in 1093 (case List.mapPartial (eval0 tm) (fnd tm) of 1094 [] => err "no valid step theorem" 1095 | [x] => x 1096 | l => (List.app (fn x => (Parse.print_thm x; print "\n")) l 1097 ; err "more than one valid step theorem")) 1098 handle HOL_ERR {message = "not found", 1099 origin_function = "find_rw", ...} => 1100 err "instruction instance not supported" 1101 end 1102 end 1103end 1104 1105local 1106 fun mk_mips_const n = Term.prim_mk_const {Thy = "mips", Name = n} 1107 val state_exception_tm = mk_mips_const "mips_state_exception" 1108 val state_exceptionSignalled_tm = 1109 mk_mips_const "mips_state_exceptionSignalled" 1110 val state_BranchDelay_tm = mk_mips_const "mips_state_BranchDelay" 1111 val state_BranchTo_tm = mk_mips_const "mips_state_BranchTo" 1112 fun mk_proj_exception r = Term.mk_comb (state_exception_tm, r) 1113 fun mk_proj_exceptionSignalled r = 1114 Term.mk_comb (state_exceptionSignalled_tm, r) 1115 fun mk_proj_BranchDelay r = Term.mk_comb (state_BranchDelay_tm, r) 1116 fun mk_proj_BranchTo r = Term.mk_comb (state_BranchTo_tm, r) 1117 val st_BranchDelay_tm = mk_proj_BranchDelay st 1118 val STATE_CONV = 1119 Conv.QCONV 1120 (REWRITE_CONV 1121 (utilsLib.datatype_rewrites true "mips" ["mips_state", "CP0"] @ 1122 [boolTheory.COND_ID, cond_rand_thms, 1123 ASSUME ``^st.BranchTo = NONE``])) 1124 THENC REPEATC 1125 (Conv.DEPTH_CONV Thm.BETA_CONV 1126 THENC 1127 REWRITE_CONV 1128 [boolTheory.COND_ID, wordsTheory.WORD_SUB_ADD, branch_delay, 1129 pairTheory.pair_case_def]) 1130 val BRANCH_DELAY_RULE = 1131 utilsLib.ALL_HYP_CONV_RULE 1132 (REWRITE_CONV [ASSUME ``^st.BranchDelay = SOME d``, 1133 optionTheory.NOT_SOME_NONE]) 1134 val NO_BRANCH_DELAY_RULE = 1135 CONV_RULE 1136 (Lib.funpow 4 RAND_CONV 1137 (LAND_CONV 1138 (RAND_CONV 1139 (PURE_REWRITE_CONV 1140 [boolTheory.COND_ID, ASSUME ``^st.BranchDelay = NONE``])))) 1141 val state_rule = Conv.RIGHT_CONV_RULE (Conv.RAND_CONV STATE_CONV) 1142 val exc_rule = SIMP_RULE bool_ss [] o COND_UPDATE_RULE o state_rule 1143 val MP_Next = state_rule o Drule.MATCH_MP NextStateMIPS_nodelay o 1144 NO_BRANCH_DELAY_RULE 1145 val MP_NextB = state_rule o BRANCH_DELAY_RULE o 1146 Drule.MATCH_MP NextStateMIPS_delay 1147 val MP_NextE = state_rule o Drule.MATCH_MP NextStateMIPS_exception 1148 val Run_CONV = utilsLib.Run_CONV ("mips", st) o utilsLib.rhsc 1149in 1150 fun mips_eval be = 1151 let 1152 val ftch = fetch be 1153 val run = eval be 1154 in 1155 fn v => 1156 let 1157 val thm1 = ftch v 1158 val thm2 = mips_decode v 1159 val thm3 = Drule.SPEC_ALL (Run_CONV thm2) 1160 val ethm = run (rhsc thm3) 1161 val thm3 = Conv.RIGHT_CONV_RULE (Conv.REWR_CONV ethm) thm3 1162 val tm = rhsc thm3 1163 val thms = List.map (fn f => STATE_CONV (f tm)) 1164 [mk_proj_exception, 1165 mk_proj_BranchDelay, 1166 mk_proj_BranchTo] 1167 val thm = Drule.LIST_CONJ ([thm1, thm2, thm3] @ thms) 1168 in 1169 [MP_Next thm] @ 1170 ([MP_NextB thm] handle HOL_ERR _ => []) @ 1171 ([MP_NextE thm] handle HOL_ERR _ => []) 1172 end 1173 end 1174end 1175 1176fun mips_eval_hex be = mips_eval be o bitstringSyntax.bitstring_of_hexstring 1177 1178fun ishex s = 1179 String.size s = 8 andalso List.all Char.isHexDigit (String.explode s) 1180 1181fun mips_step_code be = 1182 let 1183 val ev = mips_eval_hex be 1184 in 1185 fn s => 1186 let 1187 val h = mips.encodeInstruction s 1188 in 1189 if ishex h then ev h else raise ERR "mips_step_code" h 1190 end 1191 end 1192 1193(* ========================================================================= *) 1194 1195(* Testing 1196 1197open mips_stepLib 1198 1199val step = mips_eval false 1200fun test s = step (Redblackmap.find (mips_dict, s)) 1201fun test s = (Redblackmap.find (mips_dict, s)) 1202 1203val v = test "ADDI"; 1204val v = test "ADDU"; 1205val v = test "J"; 1206val v = test "BEQ"; 1207val v = test "BEQL"; 1208val v = test "BLTZAL"; 1209val v = test "BLTZALL"; 1210val v = test "ERET" 1211 1212val be = false 1213val v = bitstringSyntax.bitstring_of_hexstring "811BAF37" 1214val v = bitstringSyntax.bitstring_of_hexstring "00c72820" 1215val v = bitstringSyntax.bitstring_of_hexstring "07d00000" 1216 1217*) 1218 1219end 1220