1structure riscv_progLib :> riscv_progLib = 2struct 3 4open HolKernel boolLib bossLib 5open stateLib riscv_progTheory 6 7structure Parse = 8struct 9 open Parse 10 val (Type, Term) = 11 riscv_progTheory.riscv_prog_grammars 12 |> apsnd ParseExtras.grammar_loose_equality 13 |> parse_from_grammars 14end 15 16open Parse 17 18val ERR = Feedback.mk_HOL_ERR "riscv_progLib" 19 20(* ------------------------------------------------------------------------ *) 21 22val riscv_proj_def = riscv_progTheory.riscv_proj_def 23val riscv_comp_defs = riscv_progTheory.component_defs 24 25fun syn n d m = HolKernel.syntax_fns {n = n, dest = d, make = m} "riscv_prog" 26val riscv_1 = syn 2 HolKernel.dest_monop HolKernel.mk_monop 27val riscv_2 = syn 3 HolKernel.dest_binop HolKernel.mk_binop 28val riscv_3 = syn 4 HolKernel.dest_triop HolKernel.mk_triop 29val byte = wordsSyntax.mk_int_word_type 8 30val word5 = wordsSyntax.mk_int_word_type 5 31val half = wordsSyntax.mk_int_word_type 16 32val word = wordsSyntax.mk_int_word_type 32 33val dword = wordsSyntax.mk_int_word_type 64 34val (_, mk_riscv_procID, dest_riscv_procID, _) = riscv_1 "riscv_procID" 35val (_, _, dest_riscv_ID, is_riscv_ID) = riscv_2 "riscv_ID" 36val (_, mk_riscv_c_PC, dest_riscv_c_PC, _) = riscv_2 "riscv_c_PC" 37val (_, mk_riscv_MEM, dest_riscv_MEM, is_riscv_MEM) = riscv_2 "riscv_MEM8" 38val (_, mk_riscv_gpr, dest_riscv_gpr, is_riscv_gpr) = riscv_3 "riscv_c_gpr" 39val (_, _, dest_riscv_PC, _) = riscv_1 "riscv_PC" 40val (_, _, dest_riscv_REG, _) = riscv_2 "riscv_REG" 41val st = Term.mk_var ("s", ``:riscv_state``) 42val id_tm = ``^st.procID`` 43 44(* -- *) 45 46val riscv_select_state_thms = 47 List.map (fn t => stateLib.star_select_state_thm riscv_proj_def [] ([], t)) 48 riscv_comp_defs 49 50val riscv_select_state_pool_thm = 51 CONJ 52 (pool_select_state_thm riscv_proj_def [] 53 (utilsLib.SRW_CONV 54 [pred_setTheory.INSERT_UNION_EQ, stateTheory.CODE_POOL, riscv_instr_def] 55 ``CODE_POOL riscv_instr {(pc, [w1;w2])}``)) 56 (pool_select_state_thm riscv_proj_def [] 57 (utilsLib.SRW_CONV 58 [pred_setTheory.INSERT_UNION_EQ, stateTheory.CODE_POOL, riscv_instr_def] 59 ``CODE_POOL riscv_instr {(pc, [w1;w2;w3;w4])}``)) 60 61local 62 val riscv_instr_tm = 63 Term.prim_mk_const {Thy = "riscv_prog", Name = "riscv_instr"} 64 val strip_concat = 65 HolKernel.strip_binop wordsSyntax.dest_word_concat 66 val pc_tm = ``^st.c_PC ^id_tm`` 67 val pc_var = stateLib.gvar "pc" dword 68 fun is_mem_access tm = 69 case Lib.total boolSyntax.dest_eq tm of 70 SOME (l, r) => 71 (bitstringSyntax.is_v2w r orelse wordsSyntax.is_word_literal r) 72 andalso can (match_term ``^st.MEM8 _``) l 73 | NONE => false 74 fun hide_with_genvar (x: term) = x |-> Term.genvar (Term.type_of x) 75 fun to_hide tm = 76 case boolSyntax.dest_strip_comb tm of 77 ("riscv$riscv_state_c_update_fupd", [t, _]) => combinSyntax.dest_K_1 t 78 | ("riscv$riscv_state_log_fupd", [t, _]) => combinSyntax.dest_K_1 t 79 | _ => raise ERR "" "" 80 fun hide_hidden tm = 81 let 82 val (l, r) = boolSyntax.dest_eq tm 83 val s = optionSyntax.dest_some r 84 val sbst = List.map (hide_with_genvar o to_hide) 85 (HolKernel.find_terms (Lib.can to_hide) s) 86 in 87 boolSyntax.mk_eq (l, optionSyntax.mk_some (Term.subst sbst s)) 88 end 89 fun mem_to_int tm = 90 tm |> lhs |> rand |> rand |> rand |> numSyntax.int_of_term 91 handle HOL_ERR _ => 0 92in 93 val last_input = ref TRUTH; 94(* 95 val thm = !last_input 96*) 97 fun mk_riscv_code_pool thm = 98 let 99 val _ = (last_input := thm) 100 val id = stateLib.gvar "id" byte 101 val pc = stateLib.gvar "pc" dword 102 val pc_subst = Term.subst [id_tm |-> id, pc_tm |-> pc] 103 val thm = thm |> DISCH_ALL |> REWRITE_RULE [GSYM AND_IMP_INTRO] |> UNDISCH_ALL 104 val (a, tm) = (List.map pc_subst ## pc_subst) (Thm.dest_thm thm) 105 val (m, a) = List.partition is_mem_access a 106 val _ = length m = 2 orelse length m = 4 orelse 107 failwith "cannot find code assumptions" 108 val m = sort (fn x => fn y => mem_to_int x <= mem_to_int y) m 109 val opc = listSyntax.mk_list(map rand m,type_of (rand (hd m))) 110 in 111 (mk_riscv_c_PC (id, pc), 112 boolSyntax.rand (stateLib.mk_code_pool (riscv_instr_tm, pc, opc)), 113 boolSyntax.list_mk_imp (a, hide_hidden tm)) 114 end 115end 116 117(* -- *) 118 119local 120 val addr_eq_conv = 121 SIMP_CONV (bool_ss++wordsLib.WORD_ARITH_ss++wordsLib.WORD_ARITH_EQ_ss) [] 122in 123 val memory_introduction = 124 stateLib.introduce_map_definition 125 (riscv_progTheory.riscv_MEMORY_INSERT, addr_eq_conv) 126end 127 128(* -- *) 129 130val state_id = 131 utilsLib.mk_state_id_thm riscvTheory.riscv_state_component_equality 132 [["c_PC", "c_gpr"], 133 ["c_PC", "c_Skip", "c_gpr"], 134 ["c_Skip", "c_gpr"], 135 ["c_PC"], 136 ["c_PC","c_Skip"], 137 ["c_Skip"], 138 ["c_gpr"], 139 ["c_Skip","c_gpr"], 140 ["c_NextFetch", "c_PC"], 141 ["c_NextFetch", "c_PC", "c_gpr"], 142 ["c_NextFetch", "c_PC", "c_Skip"], 143 ["c_NextFetch", "c_PC", "c_Skip", "c_gpr"], 144 ["MEM8", "c_PC"], 145 ["MEM8", "c_PC", "c_Skip"] 146 ] 147 148val riscv_frame = 149 Thm.CONJ riscv_progTheory.c_gpr_frame 150 (stateLib.update_frame_state_thm riscv_proj_def 151 (["c_NextFetch", "c_PC", "MEM8", "c_Skip"])) 152 153val ricv_frame_hidden = 154 stateLib.update_hidden_frame_state_thm riscv_proj_def 155 [``^st with c_update := x``, 156 ``^st with log := x`` 157 ] 158 159(* -- *) 160 161local 162 fun other_index tm = 163 (case fst (boolSyntax.dest_strip_comb tm) of 164 "riscv_prog$riscv_exception" => 0 165 | "riscv_prog$riscv_procID" => 1 166 | "riscv_prog$riscv_c_NextFetch" => 16 167 | "riscv_prog$riscv_c_MCSR" => 17 168 | "riscv_prog$riscv_c_PC" => 18 169 | _ => ~1) 170 handle HOL_ERR r => (print_term tm; raise HOL_ERR r) 171 val total_dest_lit = Lib.total wordsSyntax.dest_word_literal 172 fun word_compare (w1, w2) = 173 case (total_dest_lit w1, total_dest_lit w2) of 174 (SOME x1, SOME x2) => Arbnum.compare (x1, x2) 175 | (SOME _, NONE) => General.GREATER 176 | (NONE, SOME _) => General.LESS 177 | (NONE, NONE) => Term.compare (w1, w2) 178 val register = #2 o dest_riscv_gpr 179 val address = HolKernel.strip_binop wordsSyntax.dest_word_add o 180 fst o dest_riscv_MEM 181in 182 fun psort p = 183 let 184 val (m, rst) = List.partition is_riscv_MEM p 185 val (r, rst) = List.partition is_riscv_gpr rst 186 in 187 mlibUseful.sort_map other_index Int.compare rst @ 188 mlibUseful.sort_map register Term.compare r @ 189 mlibUseful.sort_map address (mlibUseful.lex_list_order word_compare) m 190 end 191end 192 193local 194 fun fix_id (p, q) = 195 let 196 val id = case List.find (Lib.can dest_riscv_c_PC) p of 197 SOME tm => fst (dest_riscv_c_PC tm) 198 | NONE => raise ERR "riscv_write_footprint" "no PC assertion" 199 val procid = mk_riscv_procID id 200 in 201 (procid :: p, procid :: q) 202 end 203 fun c_gpr_write (p, q, v) = 204 let 205 val ((id, v1), tm) = combinSyntax.dest_update_comb v 206 val (l, gpr) = combinSyntax.strip_update v1 207 val _ = gpr ~~ Term.mk_comb (tm, id) orelse 208 raise ERR "c_gpr_write" (Hol_pp.term_to_string v) 209 val nq = List.map (fn (n, x) => mk_riscv_gpr (id, n, x)) l 210 val not_in_p = 211 List.filter 212 (fn (n, _) => 213 List.all (fn ptm => case Lib.total dest_riscv_gpr ptm of 214 SOME (id2, n2, _) => 215 not (id ~~ id2 andalso n ~~ n2) 216 | NONE => true) p) l 217 val np = List.map (fn (n, _) => mk_riscv_gpr (id, n, stateLib.vvar dword)) 218 not_in_p 219 in 220 (np @ p, nq @ q) 221 end 222in 223 val riscv_write_footprint = 224 fix_id o 225 stateLib.write_footprint riscv_1 riscv_2 226 [("riscv$riscv_state_MEM8_fupd", "riscv_MEM8", ``^st.MEM8``), 227 ("riscv$riscv_state_c_PC_fupd", "riscv_c_PC", ``^st.c_PC``), 228 ("riscv$riscv_state_c_NextFetch_fupd", "riscv_c_NextFetch", 229 ``^st.c_NextFetch``), 230 ("riscv$riscv_state_c_Skip_fupd", "riscv_c_Skip", ``^st.c_Skip``) 231 ] [] [] 232 [("riscv$riscv_state_c_gpr_fupd", c_gpr_write) 233 ] 234 (K false) 235end 236 237val riscv_mk_pre_post = 238 stateLib.mk_pre_post 239 riscv_progTheory.RISCV_MODEL_def riscv_comp_defs mk_riscv_code_pool [] 240 riscv_write_footprint psort 241 242(* ------------------------------------------------------------------------ *) 243 244local 245 val SK = Option.SOME o Lib.K 246 fun reg_index tm = 247 Lib.with_exn wordsSyntax.uint_of_word tm (ERR "reg_index" "") 248 val rname_reg = (Lib.curry (op ^) "r" o Int.toString o reg_index o List.last) 249 val riscv_rmap = 250 fn "riscv_prog$riscv_MEM8" => SK "b" 251 | "riscv_prog$riscv_c_MCSR" => SK "mcsr" 252 | "riscv_prog$riscv_c_gpr" => SOME rname_reg 253 | "riscv_prog$riscv_REG" => SOME rname_reg 254 | _ => NONE 255in 256 val riscv_rename = stateLib.rename_vars (riscv_rmap, ["b"]) 257end 258 259local 260 val rwts = 261 List.map bitstringLib.v2w_n2w_CONV 262 (List.tabulate 263 (32, fn i => bitstringSyntax.padded_fixedwidth_of_num 264 (Arbnum.fromInt i, 5))) 265 fun dest_reg tm = let val (_, n, v) = dest_riscv_gpr tm in (n, v) end 266 val reg_width = 5 267 val proj_reg = NONE : (term -> int) option 268 val reg_conv = Conv.QCONV (REWRITE_CONV rwts) 269 val ok_conv = Conv.DEPTH_CONV wordsLib.word_EQ_CONV 270 THENC Conv.QCONV (SIMP_CONV (bool_ss++boolSimps.CONJ_ss) []) 271 fun asm (tm: term) = (raise ERR "" "") : thm 272 val model_tm = ``RISCV_MODEL`` 273in 274 val combinations = 275 stateLib.register_combinations 276 (dest_reg, reg_width, proj_reg, reg_conv, ok_conv, asm, model_tm) 277end 278 279local 280 val id0 = wordsSyntax.mk_wordii (0, 8) 281 val rv64 = wordsSyntax.mk_wordii (2, 2) 282 val rv64_rule = 283 PURE_REWRITE_RULE 284 [GSYM riscv_progTheory.riscv_REG_def, GSYM riscv_progTheory.riscv_PC_def] 285 val (_, mk_mcpuid, _, _) = HolKernel.syntax_fns1 "riscv" "MachineCSR_mcpuid" 286 val (_, mk_ArchBase, _, _) = HolKernel.syntax_fns1 "riscv" "mcpuid_ArchBase" 287 val pre = progSyntax.strip_star o temporal_stateSyntax.dest_pre' o Thm.concl 288 289 290 fun specialize_to_rv64i th = 291(* 292val SOME tm = List.find is_riscv_ID (pre th) 293*) 294 case List.find is_riscv_ID (pre th) of 295 SOME tm => 296 let 297 val (id, mcsr) = dest_riscv_ID tm 298 val archbase = boolSyntax.mk_eq (mk_ArchBase (mk_mcpuid mcsr), rv64) 299 in 300 th |> Thm.INST [id |-> id0] 301 |> rv64_rule 302 |> PURE_REWRITE_RULE [ASSUME archbase] 303 |> Conv.CONV_RULE (Conv.DEPTH_CONV wordsLib.word_EQ_CONV) 304 |> REWRITE_RULE [] 305 |> Thm.DISCH archbase 306 |> Conv.CONV_RULE stateLib.MOVE_COND_CONV 307 |> helperLib.MERGE_CONDS_RULE 308 |> stateLib.introduce_triple_definition 309 (true, riscv_progTheory.riscv_RV64I_def) 310 end 311 | NONE => raise ERR "specialize_to_rv64i" "no ID assertion" 312 val to_rv64 = ref true 313in 314 fun set_to_rv64 b = to_rv64 := b 315 fun spec_to_rv64 thm = if !to_rv64 then specialize_to_rv64i thm else thm 316 fun reg_idx tm = 317 if !to_rv64 then fst (dest_riscv_REG tm) else #2 (dest_riscv_gpr tm) 318end 319 320local 321 val SPEC_IMP_RULE = 322 Conv.CONV_RULE 323 (Conv.REWR_CONV (Thm.CONJUNCT1 (Drule.SPEC_ALL boolTheory.IMP_CLAUSES)) 324 ORELSEC stateLib.MOVE_COND_CONV) 325 val rule = 326 PURE_REWRITE_RULE [set_sepTheory.SEP_CLAUSES] o 327 Q.INST [`p1`|->`emp`, `p2`|->`emp`] 328 val RISCV_PC_INTRO0 = rule RISCV_PC_INTRO 329 val RISCV_TEMPORAL_PC_INTRO0 = rule RISCV_TEMPORAL_PC_INTRO 330 fun MP_RISCV_PC_INTRO th = 331 Lib.tryfind (fn thm => MATCH_MP thm th) 332 [RISCV_PC_INTRO, RISCV_PC_INTRO0, 333 RISCV_TEMPORAL_PC_INTRO, RISCV_TEMPORAL_PC_INTRO0] 334 val cnv = REWRITE_CONV [alignmentTheory.aligned_numeric, 335 cond_branch_aligned] 336 fun RISCV_PC_bump_intro th = 337 let 338 val c = riscv_c_PC_def |> SPEC_ALL |> concl |> lhs |> repeat rator 339 in 340 if not (can (find_term (fn x => aconv x c)) (th |> concl |> rand)) then 341 th 342 else 343 th |> helperLib.HIDE_POST_RULE ``riscv_c_Skip id`` 344 |> Conv.CONV_RULE 345 (helperLib.POST_CONV (helperLib.MOVE_OUT_CONV ``riscv_c_PC id``)) 346 |> Conv.CONV_RULE 347 (helperLib.POST_CONV (helperLib.MOVE_OUT_CONV ``riscv_c_Skip id``)) 348 |> MP_RISCV_PC_INTRO 349 |> Conv.CONV_RULE (Conv.LAND_CONV cnv) 350 |> SPEC_IMP_RULE 351 end 352in 353 fun riscv_introduction th = 354 th |> PURE_REWRITE_RULE [aligned_1_intro] 355 |> riscv_rename 356 |> stateLib.introduce_triple_definition (true, riscv_progTheory.riscv_ID_def) 357 |> helperLib.HIDE_PRE_RULE ``riscv_c_Skip id`` 358 |> stateLib.introduce_triple_definition 359 (false, riscv_progTheory.riscv_ID_PC_def) 360 |> RISCV_PC_bump_intro 361 |> helperLib.MERGE_CONDS_RULE 362 |> PURE_REWRITE_RULE [jal_aligned, jalr_aligned, 363 DECIDE ``a /\ (b ==> a) = a``, 364 DECIDE ``a /\ c /\ (b ==> a) = c /\ a``] 365 |> spec_to_rv64 366 |> memory_introduction 367 |> helperLib.HIDE_POST_RULE ``riscv_RV64I`` 368 |> helperLib.HIDE_PRE_RULE ``riscv_RV64I`` 369end 370 371local 372 val component_11 = Drule.CONJUNCTS riscv_progTheory.riscv_component_11 373 val riscv_rwts = List.drop (utilsLib.datatype_rewrites true "riscv" 374 ["riscv_state"], 1) 375 val STATE_TAC = ASM_REWRITE_TAC riscv_rwts 376 val EXTRA_TAC = 377 TRY ( 378 Q.PAT_ASSUM `xxx /\ yyy` 379 (fn th => SIMP_TAC std_ss [SIMP_RULE (std_ss++boolSimps.CONJ_ss) [] th]) 380 ) 381 fun eval_Skip thm = 382 let 383 val pat = riscvTheory.Skip_def |> SPEC_ALL |> concl |> lhs 384 val tms = find_terms (can (match_term pat)) (concl thm) 385 val Skip_conv = SIMP_CONV (srw_ss()) 386 [riscvTheory.Skip_def,combinTheory.APPLY_UPDATE_THM] 387 in REWRITE_RULE (map Skip_conv tms) thm end 388 val pc_assum = ``��word_bit 0 (s.c_PC s.procID)`` 389in 390 val spec = 391 stateLib.spec 392 riscv_progTheory.RISCV_IMP_SPEC 393 riscv_progTheory.RISCV_IMP_TEMPORAL 394 [riscv_opcode_bytes, boolTheory.DE_MORGAN_THM] 395 [] 396 (riscv_select_state_pool_thm :: riscv_select_state_thms) 397 [riscv_frame, ricv_frame_hidden, state_id] 398 component_11 399 [dword, word5] 400 EXTRA_TAC STATE_TAC 401 val intro_spec = riscv_introduction o spec 402 fun riscv_spec tm = 403 let 404 val thm = riscv_stepLib.riscv_step tm 405 val thm = DISCH pc_assum thm |> UNDISCH 406 val thm = eval_Skip thm 407 val t = riscv_mk_pre_post thm 408 val thm_ts = combinations (thm, t) 409(* 410 val x = hd thm_ts 411 val th = spec x 412 val res = riscv_introduction th 413*) 414 in 415 List.map (fn x => (print "."; intro_spec x)) thm_ts 416 end 417end 418 419fun tdistinct tl = HOLset.numItems (listset tl) = length tl 420 421local 422 fun check_unique_reg_CONV tm = 423 let 424 val p = progSyntax.strip_star (temporal_stateSyntax.dest_pre' tm) 425 val rp = List.mapPartial (Lib.total reg_idx) p 426 in 427 if tdistinct rp 428 then Conv.ALL_CONV tm 429 else raise ERR "check_unique_reg_CONV" "duplicate register" 430 end 431 val PRE_CONV = Conv.RATOR_CONV o Conv.RATOR_CONV o Conv.RAND_CONV 432 fun DEPTH_COND_CONV cnv = 433 Conv.ONCE_DEPTH_CONV 434 (fn tm => 435 if progSyntax.is_cond tm 436 then Conv.RAND_CONV cnv tm 437 else raise ERR "COND_CONV" "") 438 val POST_CONV = Conv.RAND_CONV 439 val POOL_CONV = Conv.RATOR_CONV o Conv.RAND_CONV 440 fun LIST_CONV c tm = 441 if listSyntax.is_nil tm then ALL_CONV tm else 442 (RAND_CONV (LIST_CONV c) THENC RATOR_CONV (RAND_CONV c)) tm 443 val OPC_CONV = 444 POOL_CONV o Conv.RATOR_CONV o Conv.RAND_CONV o Conv.RAND_CONV o LIST_CONV 445 exception FalseTerm 446 fun NOT_F_CONV tm = 447 if Feq tm then raise FalseTerm else Conv.ALL_CONV tm 448 val WGROUND_RW_CONV = 449 Conv.DEPTH_CONV (utilsLib.cache 10 Term.compare bitstringLib.v2w_n2w_CONV) 450 THENC utilsLib.WGROUND_CONV 451 val PRE_COND_CONV = 452 helperLib.PRE_CONV 453 (DEPTH_COND_CONV 454 (WGROUND_RW_CONV 455 THENC REWRITE_CONV [] 456 THENC NOT_F_CONV) 457 THENC PURE_ONCE_REWRITE_CONV [stateTheory.cond_true_elim]) 458 val cnv = 459 check_unique_reg_CONV 460 THENC PRE_COND_CONV 461 THENC PRE_CONV WGROUND_RW_CONV 462 THENC OPC_CONV bitstringLib.v2w_n2w_CONV 463 THENC POST_CONV WGROUND_RW_CONV 464 THENC helperLib.POST_CONV (stateLib.PC_CONV "riscv_prog$riscv_PC") 465in 466 fun simp_triple_rule thm = 467 riscv_rename (Conv.CONV_RULE cnv thm) 468 handle FalseTerm => raise ERR "simp_triple_rule" "condition false" 469end 470 471local 472 fun dest_v2w_list tm = 473 listSyntax.dest_list tm 474 |> fst |> map (fst o listSyntax.dest_list o rand) 475 |> rev |> flatten |> (fn xs => listSyntax.mk_list(xs,type_of T)) 476 val get_opcode = 477 dest_v2w_list o 478 snd o pairSyntax.dest_pair o 479 hd o pred_setSyntax.strip_set o 480 temporal_stateSyntax.dest_code' o 481 Thm.concl 482 val spec_label_set = ref (Redblackset.empty String.compare) 483 val init_net = utilsLib.mk_rw_net (fn _ => raise ERR "" "") [] 484 val spec_rwts = ref init_net 485 val add1 = utilsLib.add_to_rw_net get_opcode 486 val add_specs = List.app (fn thm => spec_rwts := add1 (thm, !spec_rwts)) 487 fun find_spec opc = Lib.total (utilsLib.find_rw (!spec_rwts)) opc 488 val spec_spec_last_fail = ref (T,TRUTH) 489 (* 490 val (opc, thm) = !spec_spec_last_fail 491 *) 492 fun spec_spec opc thm = 493 let 494 val thm_opc = get_opcode thm 495 val a = fst (Term.match_term thm_opc opc) 496 val thm = Thm.INST a thm 497 in 498 simp_triple_rule thm 499 end handle HOL_ERR e => (spec_spec_last_fail := (opc,thm); raise HOL_ERR e) 500 fun err e s = raise ERR "riscv_spec_hex" (e ^ ": " ^ s) 501 fun find_opc opc = 502 List.filter (fn (_, p) => Lib.can (Term.match_term p) opc) 503 riscv_stepLib.riscv_dict 504 val split_branches = stateLib.split_cond true dest_riscv_PC 505in 506 fun riscv_config rv64 = 507 ( set_to_rv64 rv64 508 ; spec_label_set := Redblackset.empty String.compare 509 ; spec_rwts := init_net 510 ) 511(* 512val (s,tm) = hd (find_opc opc) 513*) 514 fun addInstruction (s, tm) = 515 if Redblackset.member (!spec_label_set, s) 516 then false 517 else ( print s 518 ; add_specs (riscv_spec tm) 519 ; spec_label_set := Redblackset.add (!spec_label_set, s) 520 ; true) 521 fun riscv_spec_hex () = 522 fn s => 523 let 524 val opc = riscv_stepLib.hex_to_padded_opcode s 525 fun loop e = 526 if (print "\n"; List.exists addInstruction (find_opc opc)) 527 then riscv_spec_hex () s 528 else err e s 529 in 530 case find_spec opc of 531 SOME thms => 532 (case List.mapPartial (Lib.total (spec_spec opc)) thms of 533 [] => loop "failed to find suitable spec" 534 | [th] => split_branches th 535 | _ => err "more than one spec" s) 536 | NONE => loop "failed to add suitable spec" 537 end 538 val riscv_spec_hex = riscv_spec_hex () 539end 540 541(* ------------------------------------------------------------------------ *) 542 543(* Testing... 544 545 [(2147580452, "c591", "beqz\ta1,ffffffff80017a30 <memzero+0xc>\r"), 546 (2147580454, "00053023", "sd\tzero,0(a0)\r"), 547 (2147580458, "15e1", "addi\ta1,a1,-8\r"), 548 (2147580460, "0521", "addi\ta0,a0,8\r"), 549 (2147580462, "fde5", "bnez\ta1,ffffffff80017a26 <memzero+0x2>\r"), 550 (2147580464, "8082", "ret\r")]: (int * string * string) list 551 552 [(2147580516, "ca19", "beqz\ta2,ffffffff80017a7a <memcpy+0x16>\r"), 553 (2147580518, "962a", "add\ta2,a2,a0\r"), 554 (2147580520, "87aa", "mv\ta5,a0\r"), 555 (2147580522, "0005c703", "lbu\ta4,0(a1)\r"), 556 (2147580526, "0785", "addi\ta5,a5,1\r"), 557 (2147580528, "0585", "addi\ta1,a1,1\r"), 558 (2147580530, "fee78fa3", "sb\ta4,-1(a5)\r"), 559 (2147580534, "fec79ae3", "bne\ta5,a2,ffffffff80017a6a <memcpy+0x6>\r"), 560 (2147580538, "8082", "ret\r")]: (int * string * string) list 561 562val riscv_tools = riscv_decompLib.riscv_tools 563val (riscv_spec,_,_,_) = riscv_tools 564 565riscv_progLib.riscv_spec_hex s 566 567val s = "fee78fa3"; riscv_spec_hex s; 568val s = "0005c703"; riscv_spec_hex s; 569 570val th = hd (riscv_spec_hex s) 571memory_introduction th 572 573val s = "410093"; riscv_spec_hex s; 574val s = "21180B3"; riscv_spec_hex s; 575val s = "108133"; riscv_spec_hex s; 576val s = "800000EF"; riscv_spec_hex s; 577val s = "943a"; riscv_spec_hex s; 578val s = "072a"; riscv_spec_hex s; 579val s = "e436"; riscv_spec_hex s; 580 581riscv_spec_hex "410093" 582riscv_spec_hex "21180B3" 583riscv_spec_hex "108133" 584riscv_spec_hex "FFF08093" 585riscv_spec_hex "FE008EE3" 586 587val s = "00053023" 588 589val tm = bitstringSyntax.bitstring_of_hexstring s 590val th = riscv_spec tm 591val thm = riscv_stepLib.riscv_step tm 592 593val s = "800000EF" 594val tm = bitstringSyntax.bitstring_of_hexstring s 595 596fun riscv_spec_from_hex s = let 597 val tm = bitstringSyntax.bitstring_of_hexstring s 598 in riscv_spec tm end 599 600filter (not o can riscv_spec_from_hex) vs 601 602(* currently failing: *) 603val xs = ["e436", "fc06", "f822", "e82a", "e032"] 604 605riscv_spec_hex s 606 607open riscv_progLib 608 609val imp_spec = RISCV_IMP_SPEC 610val imp_temp = riscv_progTheory.RISCV_IMP_TEMPORAL 611val read_thms = [riscv_opcode_bytes, boolTheory.DE_MORGAN_THM]: thm list 612val write_thms = []: thm list 613val select_state_thms = (riscv_select_state_pool_thm :: riscv_select_state_thms) 614val frame_thms = [riscv_frame, ricv_frame_hidden, state_id] 615val map_tys = [dword, word5] 616val mk_pre_post = riscv_mk_pre_post 617val write = riscv_write_footprint 618val EXTRA_TAC = ALL_TAC 619 620val () = riscv_config true 621val () = riscv_config false 622val () = stateLib.set_temporal true 623 624local 625 val gen = Random.newgenseed 1.0 626 fun random_bit () = 627 if Random.range (0, 2) gen = 0 then boolSyntax.T else boolSyntax.F 628in 629 fun random_hex tm = 630 let 631 val l = Term.free_vars tm 632 val s = List.map (fn v => v |-> random_bit ()) l 633 in 634 bitstringSyntax.hexstring_of_term (Term.subst s tm) 635 end 636 fun hex s = 637 riscv_spec_hex s 638 handle e as HOL_ERR _ => (print ("\n\n" ^ s ^ "\n\n"); raise e) 639end 640 641val tst = Count.apply hex o random_hex 642 643val d = List.filter (fn (s, _) => String.size s < 3 orelse 644 not (String.substring (s, 0, 3) = "JAL")) 645 riscv_stepLib.riscv_dict 646 647val l = List.map (I ## tst) d 648 649val SOME (_, tm) = Lib.assoc1 "ADD" riscv_stepLib.riscv_dict 650val s = random_hex tm 651val thms = tst tm 652 653 654val tm = bitstringSyntax.bitstring_of_hexstring "8082" 655 656*) 657 658(* ------------------------------------------------------------------------ *) 659 660end 661