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