1structure mips_progLib :> mips_progLib = 2struct 3 4open HolKernel boolLib bossLib 5open stateLib mips_progTheory 6 7structure Parse = 8struct 9 open Parse 10 val (Type, Term) = parse_from_grammars mips_progTheory.mips_prog_grammars 11end 12 13open Parse 14 15val ERR = Feedback.mk_HOL_ERR "mips_progLib" 16 17(* ------------------------------------------------------------------------ *) 18 19val mips_proj_def = mips_progTheory.mips_proj_def 20val mips_comp_defs = mips_progTheory.component_defs 21 22fun syn n d m = HolKernel.syntax_fns {n = n, dest = d, make = m} "mips_prog" 23val mips_1 = syn 2 HolKernel.dest_monop HolKernel.mk_monop 24val mips_2 = syn 3 HolKernel.dest_binop HolKernel.mk_binop 25val byte = wordsSyntax.mk_int_word_type 8 26val word5 = wordsSyntax.mk_int_word_type 5 27val word = wordsSyntax.mk_int_word_type 32 28val dword = wordsSyntax.mk_int_word_type 64 29val (_, _, dest_BranchTo, _) = mips_1 "mips_BranchTo" 30val (_, _, dest_BranchDelay, _) = mips_1 "mips_BranchDelay" 31val (_, mk_mips_PC, dest_mips_PC, _) = mips_1 "mips_PC" 32val (_, mk_mips_MEM, dest_mips_MEM, is_mips_MEM) = mips_2 "mips_MEM" 33val (_, mk_mips_gpr, dest_mips_gpr, is_mips_gpr) = mips_2 "mips_gpr" 34val (_, mk_mips_FGR, dest_mips_FGR, is_mips_FGR) = mips_2 "mips_FGR" 35val st = Term.mk_var ("s", ``:mips_state``) 36 37(* -- *) 38 39val mips_select_state_thms = 40 List.map (fn t => star_select_state_thm mips_proj_def [] ([], t)) 41 mips_comp_defs 42 43val mips_select_state_pool_thm = 44 pool_select_state_thm mips_proj_def [] 45 (utilsLib.SRW_CONV 46 [pred_setTheory.INSERT_UNION_EQ, stateTheory.CODE_POOL, mips_instr_def] 47 ``CODE_POOL mips_instr {(pc, opc)}``) 48 49local 50 val mips_instr_tm = 51 Term.prim_mk_const {Thy = "mips_prog", Name = "mips_instr"} 52 fun is_mem_access v tm = 53 case Lib.total boolSyntax.dest_eq tm of 54 SOME (l, r) => 55 stateLib.is_code_access ("mips$mips_state_MEM", v) l andalso 56 (wordsSyntax.is_word_literal r orelse bitstringSyntax.is_v2w r) 57 | NONE => false 58 val dest_opc = fst o listSyntax.dest_list o fst o bitstringSyntax.dest_v2w 59 val ty32 = fcpSyntax.mk_int_numeric_type 32 60 fun list_mk_concat l = 61 bitstringSyntax.mk_v2w 62 (listSyntax.mk_list 63 (List.concat (List.map dest_opc l), Type.bool), ty32) 64in 65 fun mk_mips_code_pool thm = 66 let 67 val pc = stateLib.gvar "pc" dword 68 val pc_a = mk_mips_PC pc 69 val (a, tm) = Thm.dest_thm thm 70 val pc_subst = Term.subst [``^st.PC`` |-> pc] 71 val a = List.map pc_subst a 72 val (m, a) = List.partition (is_mem_access pc) a 73 val m = List.map dest_code_access m 74 val m = mlibUseful.sort_map fst Int.compare m 75 val opc = list_mk_concat (List.map snd (List.rev m)) 76 in 77 (pc_a, 78 boolSyntax.rand (stateLib.mk_code_pool (mips_instr_tm, pc, opc)), 79 list_mk_imp (a, pc_subst tm)) 80 end 81end 82 83(* -- *) 84 85val state_id = 86 utilsLib.mk_state_id_thm mipsTheory.mips_state_component_equality 87 [["CP0", "PC", "gpr"], 88 ["CP0", "PC", "exceptionSignalled", "fcsr"], 89 ["CP0", "PC", "exceptionSignalled", "gpr"], 90 ["CP0", "PC", "exceptionSignalled"], 91 ["CP0", "PC", "exceptionSignalled", "hi"], 92 ["CP0", "PC", "exceptionSignalled", "lo"], 93 ["CP0", "PC", "exceptionSignalled", "hi", "lo"], 94 ["CP0", "PC", "exceptionSignalled", "gpr", "hi", "lo"], 95 ["CP0", "LLbit", "PC"], 96 ["CP0", "LLbit", "PC", "exceptionSignalled"], 97 ["CP0", "LLbit", "PC", "exceptionSignalled", "gpr"], 98 ["CP0", "LLbit", "PC", "gpr"], 99 ["CP0", "PC"], 100 ["CP0", "PC", "lo"], 101 ["CP0", "PC", "hi"], 102 ["CP0", "PC", "hi", "lo"], 103 ["CP0", "PC", "gpr", "hi", "lo"], 104 ["CP0", "LLbit", "MEM", "PC"], 105 ["CP0", "LLbit", "MEM", "PC", "exceptionSignalled"], 106 ["CP0", "MEM", "PC"], 107 ["CP0", "MEM", "PC", "exceptionSignalled", "gpr"], 108 ["MEM", "PC", "exceptionSignalled"], 109 ["MEM", "PC", "exceptionSignalled", "gpr"], 110 ["MEM", "PC"], 111 ["CP0", "FGR", "PC", "exceptionSignalled"], 112 ["FGR", "PC", "exceptionSignalled"], 113 ["gpr", "hi", "lo"], 114 ["gpr"], 115 ["fcsr"]] 116 117val CP0_id = 118 utilsLib.mk_state_id_thm mipsTheory.CP0_component_equality [["Status"]] 119 120val mips_frame = 121 stateLib.update_frame_state_thm mips_proj_def 122 (List.map (fn s => "CP0." ^ s) 123 ["Count", "Cause", "EPC", "Debug", "ErrCtl", "LLAddr", 124 "Status.ERL", "Status.EXL", "Status.CU1"] @ 125 ["PC", "BranchDelay", "BranchTo", "exceptionSignalled", "LLbit", 126 "hi", "lo", "gpr", "fcsr.FCC", "MEM", "FGR"]) 127 128(* -- *) 129 130local 131 fun dest_const tm = 132 Term.dest_const tm 133 handle e as HOL_ERR {message = "not a const", ...} => 134 (Parse.print_term tm; print "\n"; raise e) 135 val l = 136 [ 137 "cond", "mips_exception", "mips_exceptionSignalled", 138 "mips_CP0_Status_RE", "mips_CP0_Status_ERL", "mips_CP0_Status_EXL", 139 "mips_CP0_Status_BEV", "mips_CP0_Status_CU1", "mips_CP0_Config_BE", 140 "mips_CP0_Count", "mips_CP0_Cause", "mips_CP0_EPC", "mips_CP0_Debug", 141 "mips_CP0_ErrCtl", "mips_fcsr_FS", "mips_fcsr_RM", "mips_BranchDelay", 142 "mips_BranchTo", "mips_LLbit", "mips_hi", "mips_lo", "mips_PC" 143 ] 144 val m = ListPair.zip (l, Lib.mapi (fn i => Lib.K i) l) 145 fun other_index tm = 146 Option.getOpt 147 (Option.map snd (Lib.assoc1 (fst (dest_const (boolSyntax.rator tm))) m), 148 ~1) 149 val total_dest_lit = Lib.total wordsSyntax.dest_word_literal 150 fun word_compare (w1, w2) = 151 case (total_dest_lit w1, total_dest_lit w2) of 152 (SOME x1, SOME x2) => Arbnum.compare (x1, x2) 153 | (SOME _, NONE) => General.GREATER 154 | (NONE, SOME _) => General.LESS 155 | (NONE, NONE) => Term.compare (w1, w2) 156 val register = fst o dest_mips_gpr 157 val fp_register = fst o dest_mips_FGR 158 val address = HolKernel.strip_binop wordsSyntax.dest_word_add o 159 fst o dest_mips_MEM 160in 161 fun psort p = 162 let 163 val (m, rst) = List.partition is_mips_MEM p 164 val (r, rst) = List.partition is_mips_gpr rst 165 val (f, rst) = List.partition is_mips_FGR rst 166 in 167 mlibUseful.sort_map other_index Int.compare rst @ 168 mlibUseful.sort_map register word_compare r @ 169 mlibUseful.sort_map fp_register word_compare f @ 170 mlibUseful.sort_map address (mlibUseful.lex_list_order word_compare) m 171 end 172end 173 174local 175 val cp0_status_write_footprint = 176 stateLib.write_footprint mips_1 mips_2 [] [] 177 [("mips$StatusRegister_ERL_fupd", "mips_CP0_Status_ERL"), 178 ("mips$StatusRegister_EXL_fupd", "mips_CP0_Status_EXL")] 179 [] 180 (fn (s, l) => s = "mips$CP0_Status" andalso tml_eq l [``^st.CP0``]) 181 val cp0_write_footprint = 182 stateLib.write_footprint mips_1 mips_2 [] 183 [("mips$CP0_Cause_fupd", "mips_CP0_Cause"), 184 ("mips$CP0_EPC_fupd", "mips_CP0_EPC"), 185 ("mips$CP0_Debug_fupd", "mips_CP0_Debug"), 186 ("mips$CP0_LLAddr_fupd", "mips_CP0_LLAddr"), 187 ("mips$CP0_ErrCtl_fupd", "mips_CP0_ErrCtl")] 188 [("mips$CP0_Count_fupd", "mips_CP0_Count")] 189 [("mips$CP0_Status_fupd", cp0_status_write_footprint)] 190 (fn (s, l) => s = "mips$mips_state_CP0" andalso tml_eq l [st]) 191 val fcsr_write_footprint = 192 stateLib.write_footprint mips_1 mips_2 [] [] 193 [("mips$FCSR_FCC_fupd", "mips_fcsr_FCC")] 194 [] 195 (fn (s, l) => s = "mips$mips_state_fcsr" andalso tml_eq l [st]) 196in 197 val mips_write_footprint = 198 stateLib.write_footprint mips_1 mips_2 199 [("mips$mips_state_MEM_fupd", "mips_MEM", ``^st.MEM``), 200 ("mips$mips_state_gpr_fupd", "mips_gpr", ``^st.gpr``), 201 ("mips$mips_state_FGR_fupd", "mips_FGR", ``^st.FGR``)] 202 [("mips$mips_state_hi_fupd", "mips_hi"), 203 ("mips$mips_state_lo_fupd", "mips_lo"), 204 ("mips$mips_state_exceptionSignalled_fupd", "mips_exceptionSignalled"), 205 ("mips$mips_state_LLbit_fupd", "mips_LLbit"), 206 ("mips$mips_state_BranchTo_fupd", "mips_BranchTo")] 207 [("mips$mips_state_PC_fupd", "mips_PC"), 208 ("mips$mips_state_BranchDelay_fupd", "mips_BranchDelay")] 209 [("mips$mips_state_CP0_fupd", cp0_write_footprint), 210 ("mips$mips_state_fcsr_fupd", fcsr_write_footprint)] 211 (K false) 212end 213 214val mips_mk_pre_post = 215 stateLib.mk_pre_post 216 mips_progTheory.MIPS_MODEL_def mips_comp_defs mk_mips_code_pool [] 217 mips_write_footprint psort 218 219(* ------------------------------------------------------------------------ *) 220 221local 222 val mips_rmap = 223 Lib.total 224 (fn "mips_prog$mips_CP0_Count" => K "count" 225 | "mips_prog$mips_CP0_Cause" => K "cause" 226 | "mips_prog$mips_CP0_EPC" => K "epc" 227 | "mips_prog$mips_CP0_ErrorEPC" => K "errorpc" 228 | "mips_prog$mips_CP0_Status_ERL" => K "erl" 229 | "mips_prog$mips_CP0_Status_EXL" => K "exl" 230 | "mips_prog$mips_CP0_Status_BEV" => K "bev" 231 | "mips_prog$mips_fcsr_FS" => K "flush_to_zero" 232 | "mips_prog$mips_fcsr_RM" => K "rounding_mode" 233 | "mips_prog$mips_fcsr_FCC" => K "fcc" 234 | "mips_prog$mips_fcsr_ABS2008" => K "abs2008" 235 | "mips_prog$mips_LLbit" => K "llbit" 236 | "mips_prog$mips_hi" => K "hi" 237 | "mips_prog$mips_lo" => K "lo" 238 | "mips_prog$mips_gpr" => 239 Lib.curry (op ^) "r" o Int.toString o wordsSyntax.uint_of_word o 240 List.hd 241 | "mips_prog$mips_FGR" => 242 Lib.curry (op ^) "f" o Int.toString o wordsSyntax.uint_of_word o 243 List.hd 244 | "mips_prog$mips_MEM" => K "b" 245 | _ => fail()) 246in 247 val mips_rename = stateLib.rename_vars (mips_rmap, ["b"]) 248end 249 250fun spec_BranchTo th = 251 let 252 val p = 253 progSyntax.strip_star (temporal_stateSyntax.dest_pre' (Thm.concl th)) 254 in 255 case List.mapPartial (Lib.total dest_BranchTo) p of 256 [v] => if Term.is_var v 257 then let 258 val ty = optionSyntax.dest_option (Term.type_of v) 259 in 260 Thm.INST [v |-> optionSyntax.mk_none ty] th 261 end 262 else th 263 | _ => th 264 end 265fun tdistinct tml = HOLset.numItems (listset tml) = length tml 266local 267 fun check_unique_reg_CONV tm = 268 let 269 val p = progSyntax.strip_star (temporal_stateSyntax.dest_pre' tm) 270 val rp = List.mapPartial (Lib.total (fst o dest_mips_gpr)) p 271 val fp = List.mapPartial (Lib.total (fst o dest_mips_FGR)) p 272 in 273 if tdistinct rp andalso tdistinct fp 274 then Conv.ALL_CONV tm 275 else raise ERR "check_unique_reg_CONV" "duplicate register" 276 end 277 val PRE_CONV = Conv.RATOR_CONV o Conv.RATOR_CONV o Conv.RAND_CONV 278 fun DEPTH_COND_CONV cnv = 279 Conv.ONCE_DEPTH_CONV 280 (fn tm => 281 if progSyntax.is_cond tm 282 then Conv.RAND_CONV cnv tm 283 else raise ERR "COND_CONV" "") 284 val POST_CONV = Conv.RAND_CONV 285 val POOL_CONV = Conv.RATOR_CONV o Conv.RAND_CONV 286 val OPT_CONV = REWRITE_CONV [optionTheory.IS_SOME_DEF] 287 val OPC_CONV = POOL_CONV o Conv.RATOR_CONV o Conv.RAND_CONV o Conv.RAND_CONV 288 exception FalseTerm 289 fun NOT_F_CONV tm = 290 if Feq tm then raise FalseTerm else Conv.ALL_CONV tm 291 val WGROUND_RW_CONV = 292 Conv.DEPTH_CONV (utilsLib.cache 10 Term.compare bitstringLib.v2w_n2w_CONV) 293 THENC utilsLib.WGROUND_CONV 294 val PRE_COND_CONV = 295 PRE_CONV 296 (DEPTH_COND_CONV 297 (WGROUND_RW_CONV 298 THENC REWRITE_CONV [] 299 THENC NOT_F_CONV)) 300 val cnv = 301 check_unique_reg_CONV 302 THENC PRE_COND_CONV 303 THENC PRE_CONV WGROUND_RW_CONV 304 THENC OPC_CONV bitstringLib.v2w_n2w_CONV 305 THENC POST_CONV (WGROUND_RW_CONV THENC OPT_CONV) 306in 307 fun simp_triple_rule thm = 308 mips_rename (Conv.CONV_RULE cnv thm) 309 handle FalseTerm => raise ERR "simp_triple_rule" "condition false" 310end 311 312local 313 val rwts = 314 List.map bitstringLib.v2w_n2w_CONV 315 (List.tabulate 316 (32, fn i => bitstringSyntax.padded_fixedwidth_of_num 317 (Arbnum.fromInt i, 5))) 318in 319 val REG_CONV = Conv.QCONV (REWRITE_CONV rwts) 320end 321 322local 323 val dest_reg = dest_mips_gpr 324 val dest_fp_reg = dest_mips_FGR 325 val reg_width = 5 326 val proj_reg = NONE 327 val reg_conv = REG_CONV 328 val ok_conv = ALL_CONV 329 fun asm_rule (tm : term) = (raise ERR "" "") : thm 330 val model_tm = ``MIPS_MODEL`` 331 val reg_combinations = 332 stateLib.register_combinations 333 (dest_reg, reg_width, proj_reg, reg_conv, ok_conv, asm_rule, model_tm) 334 val fp_reg_combinations = 335 stateLib.register_combinations 336 (dest_fp_reg, reg_width, proj_reg, reg_conv, ok_conv, asm_rule, 337 model_tm) 338in 339 fun combinations thm_t = 340 case fp_reg_combinations thm_t of 341 [_] => reg_combinations thm_t 342 | l => l 343end 344 345local 346 val component_11 = Drule.CONJUNCTS mips_progTheory.mips_component_11 347 val mips_rwts = List.drop (utilsLib.datatype_rewrites true "mips" 348 ["mips_state", "CP0", "StatusRegister", 349 "FCSR"], 1) 350 val STATE_TAC = ASM_REWRITE_TAC mips_rwts 351in 352 val spec = 353 stateLib.introduce_triple_definition (false, mips_CONFIG_def) o 354 mips_rename o spec_BranchTo o 355 stateLib.spec 356 mips_progTheory.MIPS_IMP_SPEC 357 mips_progTheory.MIPS_IMP_TEMPORAL 358 [mips_stepTheory.get_bytes] 359 [] 360 (mips_select_state_pool_thm :: mips_select_state_thms) 361 [mips_frame, state_id, CP0_id] 362 component_11 363 [dword, word5] 364 ALL_TAC STATE_TAC 365 fun mips_spec_opt be = 366 let 367 val step = mips_stepLib.mips_eval be 368 in 369 fn tm => 370 let 371 val thms = step tm 372 val thm_ts = 373 List.map 374 (fn thm => 375 let 376 val t = mips_mk_pre_post thm 377 in 378 combinations (thm, t) 379 end) thms 380 in 381 List.map (fn x => (print "."; spec x)) (List.concat thm_ts) 382 end 383 end 384end 385 386local 387 val get_opcode = 388 fst o bitstringSyntax.dest_v2w o 389 snd o pairSyntax.dest_pair o 390 hd o pred_setSyntax.strip_set o 391 temporal_stateSyntax.dest_code' o 392 Thm.concl 393 val the_spec = ref (mips_spec_opt true) 394 val spec_label_set = ref (Redblackset.empty String.compare) 395 val init_net = utilsLib.mk_rw_net (fn _ => raise ERR "" "") [] 396 val spec_rwts = ref init_net 397 val add1 = utilsLib.add_to_rw_net get_opcode 398 val add_specs = List.app (fn thm => spec_rwts := add1 (thm, !spec_rwts)) 399 fun find_spec opc = Lib.total (utilsLib.find_rw (!spec_rwts)) opc 400 fun spec_spec opc thm = 401 let 402 val thm_opc = get_opcode thm 403 val a = fst (Term.match_term thm_opc opc) 404 in 405 simp_triple_rule (Thm.INST a thm) 406 end 407 fun err e s = raise ERR "mips_spec_hex" (e ^ ": " ^ s) 408 fun reverse_endian tm = 409 let 410 val (l, ty) = listSyntax.dest_list tm 411 in 412 listSyntax.mk_list (utilsLib.rev_endian l, ty) 413 end 414 val rev_endian = ref reverse_endian 415 fun thm_eq thm1 thm2 = Term.aconv (Thm.concl thm1) (Thm.concl thm2) 416 val mk_thm_set = Lib.op_mk_set thm_eq 417in 418 fun mips_config be = 419 ( the_spec := mips_spec_opt be 420 ; spec_label_set := Redblackset.empty String.compare 421 ; spec_rwts := init_net 422 ; rev_endian := (if be then reverse_endian else Lib.I) 423 ) 424 fun mips_spec s = (!the_spec) s 425 fun addInstruction (s, tm) = 426 if Redblackset.member (!spec_label_set, s) 427 then false 428 else ( print s 429 ; add_specs (mips_spec tm) 430 ; spec_label_set := Redblackset.add (!spec_label_set, s) 431 ; true) 432 fun mips_spec_hex () = 433 (* utilsLib.cache 1000 String.compare *) 434 (fn s => 435 let 436 val opc = mips_stepLib.hex_to_padded_opcode s 437 fun loop e = 438 let 439 val l = mips_stepLib.mips_find_opc opc 440 in 441 if (print "\n"; List.exists addInstruction l) 442 then mips_spec_hex () s 443 else err e s 444 end 445 val opc = !rev_endian opc 446 in 447 case find_spec opc of 448 SOME thms => 449 let 450 val l = List.mapPartial (Lib.total (spec_spec opc)) thms 451 in 452 if List.null l 453 then loop "failed to find suitable spec" 454 else mk_thm_set l 455 end 456 | NONE => loop "failed to add suitable spec" 457 end) 458 val mips_spec_hex = mips_spec_hex () 459 val mips_spec_code = mips_spec_hex o mips.encodeInstruction 460end 461 462local 463 val MIPS_PC_INTRO0 = 464 MIPS_PC_INTRO |> Q.INST [`p1`|->`emp`, `p2`|->`emp`] 465 |> PURE_REWRITE_RULE [set_sepTheory.SEP_CLAUSES] 466 fun MP_MIPS_PC_INTRO th = 467 Lib.tryfind (fn thm => MATCH_MP thm th) 468 [MIPS_PC_INTRO, MIPS_PC_INTRO0] 469in 470 val mips_pc_intro_rule = 471 Conv.CONV_RULE 472 (Conv.LAND_CONV (REWRITE_CONV [alignmentTheory.aligned_numeric]) 473 THENC (Conv.REWR_CONV 474 (Thm.CONJUNCT1 (Drule.SPEC_ALL boolTheory.IMP_CLAUSES)) 475 ORELSEC stateLib.MOVE_COND_CONV) 476 THENC helperLib.POST_CONV (stateLib.PC_CONV "mips_prog$MIPS_PC")) o 477 MP_MIPS_PC_INTRO o 478 Conv.CONV_RULE 479 (helperLib.POST_CONV 480 (helperLib.MOVE_OUT_CONV ``mips_BranchDelay`` 481 THENC helperLib.MOVE_OUT_CONV ``mips_PC``)) o 482 stateLib.introduce_triple_definition 483 (false, mips_progTheory.MIPS_PC_def) o 484 Conv.CONV_RULE 485 (stateLib.PRE_COND_CONV 486 (SIMP_CONV (bool_ss++boolSimps.CONJ_ss) 487 [alignmentTheory.aligned_numeric])) o 488 helperLib.MERGE_CONDS_RULE 489 val spec_join_rule = helperLib.SPEC_COMPOSE_RULE o Lib.list_of_pair 490end 491 492val spec_hex = 493 List.map 494 (REWRITE_RULE [GSYM mips_LE_def, GSYM mips_BE_def] o 495 Q.INST [`flush_to_zero` |-> `F`, `rounding_mode` |-> `0w`, 496 `abs2008` |-> `T`]) o 497 mips_spec_hex 498 499val split_BranchDelay = stateLib.split_cond true dest_BranchDelay 500val split_exception = stateLib.split_cond false dest_mips_PC 501 502fun mips_spec_hex2 s = 503 List.map mips_pc_intro_rule 504 (case String.tokens Char.isSpace s of 505 [s1] => 506 (case spec_hex s1 of 507 [th, _] => [List.last (split_exception th)] 508 | l => raise ERR "mips_spec2_hex" ("Expecting two theorems: " ^ s1)) 509 | [s1, s2] => 510 (case (spec_hex s1, spec_hex s2) of 511 ([th1], [_, th2]) => 512 List.map (fn t => spec_join_rule (t, th2)) (split_BranchDelay th1) 513 | _ => raise ERR "mips_spec2_hex" ("Expecting three theorems: " ^ s)) 514 | _ => raise ERR "mips_spec2_hex" ("More than two strings: " ^ s)) 515 516(* ------------------------------------------------------------------------ *) 517 518(* Testing... 519 520open mips_progLib 521 522val imp_spec = MIPS_IMP_SPEC 523val imp_temp = mips_progTheory.MIPS_IMP_TEMPORAL 524val read_thms = [mips_stepTheory.get_bytes] 525val write_thms = []: thm list 526val select_state_thms = (mips_select_state_pool_thm :: mips_select_state_thms) 527val frame_thms = [mips_frame, state_id, CP0_id] 528val map_tys = [dword, word5] 529val mk_pre_post = mips_mk_pre_post 530val write = mips_write_footprint 531val EXTRA_TAC = ALL_TAC 532 533val () = mips_config false 534val () = stateLib.set_temporal true 535 536local 537 val gen = Random.newgenseed 1.0 538 fun random_bit () = 539 if Random.range (0, 2) gen = 0 then boolSyntax.T else boolSyntax.F 540in 541 fun random_hex tm = 542 let 543 val l = Term.free_vars tm 544 val s = List.map (fn v => v |-> random_bit ()) l 545 in 546 bitstringSyntax.hexstring_of_term (Term.subst s tm) 547 end 548 fun hex s = 549 mips_spec_hex s 550 handle e as HOL_ERR _ => (print ("\n\n" ^ s ^ "\n\n"); raise e) 551end 552 553val () = mips_config false 554val be = false 555val tst = mips_spec 556val tst = Count.apply hex o random_hex 557val tst = hex o random_hex 558val dec = Conv.CONV_RULE (Conv.DEPTH_CONV bitstringLib.v2w_n2w_CONV) o 559 mips_stepLib.mips_decode_hex 560 561val d = List.filter (fn (s, _) => not (Lib.mem s ["MFC0", "MTC0"])) 562 (Redblackmap.listItems mips_stepLib.mips_dict) 563 564val l = List.map (I ## tst) d 565 566mips_stepLib.mips_find_opc (mips_stepLib.hex_to_padded_opcode "000C001E") 567 568val s = random_hex (Redblackmap.find (mips_stepLib.mips_dict, "ERET")) 569mips_spec (Redblackmap.find (mips_stepLib.mips_dict, "ERET")) 570 571mips_spec_hex s 572 573dec "9FA0AED9" 574 575*) 576 577(* ------------------------------------------------------------------------ *) 578 579end 580