1structure m0_progLib :> m0_progLib = 2struct 3 4open HolKernel boolLib bossLib 5open stateLib spec_databaseLib m0_progTheory 6 7structure Parse = 8struct 9 open Parse 10 val (Type, Term) = parse_from_grammars m0_progTheory.m0_prog_grammars 11end 12 13open Parse 14 15val ERR = Feedback.mk_HOL_ERR "m0_progLib" 16 17(* ------------------------------------------------------------------------ *) 18 19val m0_proj_def = m0_progTheory.m0_proj_def 20val m0_comp_defs = m0_progTheory.component_defs 21 22local 23 val pc = Term.prim_mk_const {Thy = "m0", Name = "RName_PC"} 24 val step_1 = HolKernel.syntax_fns1 "m0_step" 25 fun syn n d m = HolKernel.syntax_fns {n = n, dest = d, make = m} "m0_prog" 26 val m0_0 = syn 1 HolKernel.dest_monop HolKernel.mk_monop 27in 28 val m0_1 = syn 2 HolKernel.dest_monop HolKernel.mk_monop 29 val m0_2 = syn 3 HolKernel.dest_binop HolKernel.mk_binop 30 val byte = wordsSyntax.mk_int_word_type 8 31 val half = wordsSyntax.mk_int_word_type 16 32 val word = wordsSyntax.mk_int_word_type 32 33 val (_, _, dest_m0_AIRCR_ENDIANNESS, _) = m0_1 "m0_AIRCR_ENDIANNESS" 34 val (_, _, dest_m0_CONFIG, _) = m0_1 "m0_CONFIG" 35 val (_, mk_data_to_thumb2, _, _) = m0_0 "data_to_thumb2" 36 val (_, mk_m0_MEM, dest_m0_MEM, is_m0_MEM) = m0_2 "m0_MEM" 37 val (_, mk_m0_REG, dest_m0_REG, is_m0_REG) = m0_2 "m0_REG" 38 val (_, mk_rev_e, _, _) = step_1 "reverse_endian" 39 fun mk_m0_PC v = mk_m0_REG (pc, v) 40end 41 42(* -- *) 43 44val m0_select_state_thms = 45 List.map (fn t => stateLib.star_select_state_thm m0_proj_def [] ([], t)) 46 m0_comp_defs 47 48val m0_select_state_pool_thm = 49 utilsLib.map_conv 50 (pool_select_state_thm m0_proj_def [] o 51 utilsLib.SRW_CONV 52 [pred_setTheory.INSERT_UNION_EQ, stateTheory.CODE_POOL, m0_instr_def]) 53 [``CODE_POOL m0_instr {(pc, INL opc)}``, 54 ``CODE_POOL m0_instr {(pc, INR opc)}``] 55 56(* -- *) 57 58val state_id = 59 utilsLib.mk_state_id_thm m0Theory.m0_state_component_equality 60 [["PSR", "REG", "count", "pcinc"], 61 ["MEM", "REG", "count", "pcinc"], 62 ["REG", "count", "pcinc"] 63 ] 64 65val m0_frame = 66 stateLib.update_frame_state_thm m0_proj_def 67 ["PSR.N", "PSR.Z", "PSR.C", "PSR.V", "count", "REG", "MEM"] 68 69val m0_frame_hidden = 70 stateLib.update_hidden_frame_state_thm m0_proj_def 71 [``s with pcinc := x``] 72 73(* -- *) 74 75local 76 val m0_instr_tm = Term.prim_mk_const {Thy = "m0_prog", Name = "m0_instr"} 77 fun is_mem_access v tm = 78 case Lib.total boolSyntax.dest_eq tm of 79 SOME (l, r) => 80 stateLib.is_code_access ("m0$m0_state_MEM", v) l andalso 81 (wordsSyntax.is_word_literal r orelse bitstringSyntax.is_v2w r) 82 | NONE => false 83 val dest_opc = fst o listSyntax.dest_list o fst o bitstringSyntax.dest_v2w 84 val ty16 = fcpSyntax.mk_int_numeric_type 16 85 val ty32 = fcpSyntax.mk_int_numeric_type 32 86 fun list_mk_concat ty l = 87 bitstringSyntax.mk_v2w 88 (listSyntax.mk_list 89 (List.concat (List.map dest_opc l), Type.bool), ty) 90 val rearrange = fn [a, b, c, d] => [c, d, a, b] | l => l 91 fun mk_inl_or_inr l = 92 if List.length l = 2 93 then sumSyntax.mk_inl (list_mk_concat ty16 l, word) 94 else sumSyntax.mk_inr (list_mk_concat ty32 (rearrange l), half) 95in 96 fun mk_m0_code_pool thm = 97 let 98 val r15 = stateLib.gvar "pc" word 99 val r15_a = mk_m0_PC r15 100 val (a, tm) = Thm.dest_thm thm 101 val r15_subst = Term.subst [``s.REG RName_PC`` |-> r15] 102 val a = List.map r15_subst a 103 val (m, a) = List.partition (is_mem_access r15) a 104 val m = List.map dest_code_access m 105 val m = mlibUseful.sort_map fst Int.compare m 106 val opc = mk_inl_or_inr (List.map snd (List.rev m)) 107 in 108 (r15_a, 109 boolSyntax.rand (stateLib.mk_code_pool (m0_instr_tm, r15, opc)), 110 list_mk_imp (a, r15_subst tm)) 111 end 112end 113 114local 115 val pc_tm = ``alignment$align 2 (pc + 4w: word32)`` 116 fun is_pc_relative tm = 117 case Lib.total dest_m0_MEM tm of 118 SOME (t, _) => fst (utilsLib.strip_add_or_sub t) = pc_tm 119 | NONE => false 120 fun is_big_end tm = 121 case Lib.total dest_m0_AIRCR_ENDIANNESS tm of 122 SOME t => t = boolSyntax.T 123 | NONE => false 124 val byte_chunks = stateLib.group_into_chunks (dest_m0_MEM, 4, false) 125 fun rwt (w, a) = 126 [Drule.SPECL [a, w] m0_progTheory.MOVE_TO_TEMPORAL_M0_CODE_POOL, 127 Drule.SPECL [a, w] m0_progTheory.MOVE_TO_M0_CODE_POOL] 128 fun move_to_code wa = 129 REWRITE_RULE 130 ([stateTheory.BIGUNION_IMAGE_1, stateTheory.BIGUNION_IMAGE_2, 131 set_sepTheory.STAR_ASSOC, set_sepTheory.SEP_CLAUSES, 132 m0_progTheory.disjoint_m0_instr_thms, m0_stepTheory.concat_bytes] @ 133 List.concat (List.map rwt wa)) 134 val rev_end_rule = 135 PURE_REWRITE_RULE 136 [m0_stepTheory.concat_bytes, m0_stepTheory.reverse_endian_bytes] 137 fun rev_intro x = 138 rev_end_rule o Thm.INST (List.map (fn (w, _: term) => w |-> mk_rev_e w) x) 139in 140 fun extend_m0_code_pool thm = 141 let 142 val (p, q) = temporal_stateSyntax.dest_pre_post' (Thm.concl thm) 143 val lp = progSyntax.strip_star p 144 in 145 if Lib.exists is_pc_relative lp 146 then let 147 val be = List.exists is_big_end lp 148 val (s, wa) = byte_chunks lp 149 in 150 if List.null s 151 then thm 152 else let 153 val thm' = 154 move_to_code wa (Thm.INST (List.concat s) thm) 155 in 156 if be then rev_intro wa thm' else thm' 157 end 158 end 159 else thm 160 end 161end 162 163(* -- *) 164 165fun reg_index tm = 166 case Term.dest_thy_const tm of 167 {Thy = "m0", Name = "RName_0", ...} => 0 168 | {Thy = "m0", Name = "RName_1", ...} => 1 169 | {Thy = "m0", Name = "RName_2", ...} => 2 170 | {Thy = "m0", Name = "RName_3", ...} => 3 171 | {Thy = "m0", Name = "RName_4", ...} => 4 172 | {Thy = "m0", Name = "RName_5", ...} => 5 173 | {Thy = "m0", Name = "RName_6", ...} => 6 174 | {Thy = "m0", Name = "RName_7", ...} => 7 175 | {Thy = "m0", Name = "RName_8", ...} => 8 176 | {Thy = "m0", Name = "RName_9", ...} => 9 177 | {Thy = "m0", Name = "RName_10", ...} => 10 178 | {Thy = "m0", Name = "RName_11", ...} => 11 179 | {Thy = "m0", Name = "RName_12", ...} => 12 180 | {Thy = "m0", Name = "RName_SP_main", ...} => 13 181 | {Thy = "m0", Name = "RName_SP_process", ...} => 13 182 | {Thy = "m0", Name = "RName_LR", ...} => 14 183 | {Thy = "m0", Name = "RName_PC", ...} => 15 184 | _ => raise ERR "reg_index" "" 185 186local 187 fun other_index tm = 188 case fst (Term.dest_const (boolSyntax.rator tm)) of 189 "m0_exception" => 0 190 | "m0_CONTROL_SPSEL" => 1 191 | "m0_AIRCR" => 2 192 | "m0_count" => 3 193 | "m0_PSR_N" => 9 194 | "m0_PSR_Z" => 10 195 | "m0_PSR_C" => 11 196 | "m0_PSR_V" => 12 197 | _ => ~1 198 val int_of_v2w = 199 Arbnum.toInt o bitstringSyntax.num_of_term o fst o bitstringSyntax.dest_v2w 200 val total_dest_lit = Lib.total wordsSyntax.dest_word_literal 201 val total_dest_reg = Lib.total (wordsSyntax.uint_of_word o Term.rand) 202 fun word_compare (w1, w2) = 203 case (total_dest_lit w1, total_dest_lit w2) of 204 (SOME x1, SOME x2) => Arbnum.compare (x1, x2) 205 | (SOME _, NONE) => General.GREATER 206 | (NONE, SOME _) => General.LESS 207 | (NONE, NONE) => Term.compare (w1, w2) 208 fun reg_compare (r1, r2) = 209 case (r1, r2) of 210 (mlibUseful.INL i, mlibUseful.INL j) => Int.compare (i, j) 211 | (mlibUseful.INL _, mlibUseful.INR _) => General.GREATER 212 | (mlibUseful.INR _, mlibUseful.INL _) => General.LESS 213 | (mlibUseful.INR i, mlibUseful.INR j) => Term.compare (i, j) 214 fun reg tm = 215 case Lib.total reg_index tm of 216 SOME i => mlibUseful.INL i 217 | NONE => (case total_dest_reg tm of 218 SOME i => mlibUseful.INL i 219 | NONE => mlibUseful.INR tm) 220 val register = reg o fst o dest_m0_REG 221 val address = HolKernel.strip_binop (Lib.total wordsSyntax.dest_word_add) o 222 fst o dest_m0_MEM 223in 224 fun psort p = 225 let 226 val (m, rst) = List.partition is_m0_MEM p 227 val (r, rst) = List.partition is_m0_REG rst 228 in 229 mlibUseful.sort_map other_index Int.compare rst @ 230 mlibUseful.sort_map register reg_compare r @ 231 mlibUseful.sort_map address (mlibUseful.lex_list_order word_compare) m 232 end 233end 234 235local 236 val st = Term.mk_var ("s", ``:m0_state``) 237 val psr_footprint = 238 stateLib.write_footprint m0_1 m0_2 [] 239 [("m0$PSR_N_fupd", "m0_PSR_N"), 240 ("m0$PSR_Z_fupd", "m0_PSR_Z"), 241 ("m0$PSR_C_fupd", "m0_PSR_C"), 242 ("m0$PSR_V_fupd", "m0_PSR_V")] [] [] 243 (fn (s, l) => s = "m0$m0_state_PSR" andalso l = [st]) 244in 245 val m0_write_footprint = 246 stateLib.write_footprint m0_1 m0_2 247 [("m0$m0_state_MEM_fupd", "m0_MEM", ``^st.MEM``), 248 ("m0$m0_state_REG_fupd", "m0_REG", ``^st.REG``)] 249 [("m0$m0_state_count_fupd", "m0_count")] [] 250 [("m0$m0_state_PSR_fupd", psr_footprint), 251 ("m0$m0_state_pcinc_fupd", fn (p, q, _) => (p, q))] 252 (K false) 253end 254 255val m0_mk_pre_post = 256 stateLib.mk_pre_post 257 m0_progTheory.M0_MODEL_def m0_comp_defs mk_m0_code_pool [] 258 m0_write_footprint psort 259 260(* ------------------------------------------------------------------------ *) 261 262local 263 val sp = wordsSyntax.mk_wordii (13, 4) 264 val registers = List.tabulate (16, fn i => wordsSyntax.mk_wordii (i, 4)) 265 |> Lib.pluck (Lib.equal sp) |> snd 266 val R_name_tm = Term.prim_mk_const {Thy = "m0_step", Name = "R_name"} 267 val R_name_b_tm = Term.mk_comb (R_name_tm, Term.mk_var ("b", Type.bool)) 268 val mk_R_main = Lib.curry Term.mk_comb R_name_b_tm 269 val R_main = 270 utilsLib.map_conv 271 (SIMP_CONV (srw_ss()) [m0_stepTheory.R_name_def]) 272 (List.map mk_R_main registers @ 273 [``^R_name_tm F ^sp``, ``^R_name_tm T ^sp``]) 274 val rwts = List.take (utilsLib.datatype_rewrites false "m0" ["RName"], 2) 275in 276 val REG_CONV = 277 Conv.QCONV (REWRITE_CONV (rwts @ [R_main, m0_stepTheory.v2w_ground4])) 278 val REG_RULE = Conv.CONV_RULE REG_CONV o utilsLib.ALL_HYP_CONV_RULE REG_CONV 279end 280 281local 282 val dest_reg = dest_m0_REG 283 val reg_width = 4 284 val proj_reg = SOME reg_index 285 val reg_conv = REG_CONV 286 val ok_conv = ALL_CONV 287 val r15 = wordsSyntax.mk_wordii (15, 4) 288 fun asm tm = Thm.ASSUME (boolSyntax.mk_neg (boolSyntax.mk_eq (tm, r15))) 289 val model_tm = ``M0_MODEL`` 290in 291 val combinations = 292 stateLib.register_combinations 293 (dest_reg, reg_width, proj_reg, reg_conv, ok_conv, asm, model_tm) 294end 295 296(* ------------------------------------------------------------------------ *) 297 298local 299 val m0_rmap = 300 Lib.total 301 (fn "m0_prog$m0_PSR_N" => K "n" 302 | "m0_prog$m0_PSR_Z" => K "z" 303 | "m0_prog$m0_PSR_C" => K "c" 304 | "m0_prog$m0_PSR_V" => K "v" 305 | "m0_prog$m0_AIRCR_ENDIANNESS" => K "endianness" 306 | "m0_prog$m0_CurrentMode" => K "mode" 307 | "m0_prog$m0_count" => K "count" 308 | "m0_prog$m0_REG" => 309 Lib.curry (op ^) "r" o Int.toString o reg_index o List.hd 310 | "m0_prog$m0_MEM" => K "b" 311 | _ => fail()) 312in 313 val m0_rename = stateLib.rename_vars (m0_rmap, ["b"]) 314end 315 316local 317 val m0_PSR_T_F = List.map UNDISCH (CONJUNCTS m0_progTheory.m0_PSR_T_F) 318 val MOVE_COND_RULE = Conv.CONV_RULE stateLib.MOVE_COND_CONV 319 val SPEC_IMP_RULE = 320 Conv.CONV_RULE 321 (Conv.REWR_CONV (Thm.CONJUNCT1 (Drule.SPEC_ALL boolTheory.IMP_CLAUSES)) 322 ORELSEC MOVE_COND_CONV) 323 fun TRY_DISCH_RULE thm = 324 case List.length (Thm.hyp thm) of 325 0 => thm 326 | 1 => MOVE_COND_RULE (Drule.DISCH_ALL thm) 327 | _ => thm |> Drule.DISCH_ALL 328 |> PURE_REWRITE_RULE [boolTheory.AND_IMP_INTRO] 329 |> MOVE_COND_RULE 330 val flag_introduction = 331 helperLib.MERGE_CONDS_RULE o TRY_DISCH_RULE o PURE_REWRITE_RULE m0_PSR_T_F 332 val addr_eq_conv = 333 SIMP_CONV (bool_ss++wordsLib.WORD_ARITH_ss++wordsLib.WORD_ARITH_EQ_ss) [] 334 val m0_PC_INTRO0 = 335 m0_PC_INTRO |> Q.INST [`p1`|->`emp`, `p2`|->`emp`] 336 |> PURE_REWRITE_RULE [set_sepTheory.SEP_CLAUSES] 337 val m0_TEMPORAL_PC_INTRO0 = 338 m0_TEMPORAL_PC_INTRO |> Q.INST [`p1`|->`emp`, `p2`|->`emp`] 339 |> PURE_REWRITE_RULE [set_sepTheory.SEP_CLAUSES] 340 fun MP_m0_PC_INTRO th = 341 Lib.tryfind (fn thm => MATCH_MP thm th) 342 [m0_PC_INTRO, m0_TEMPORAL_PC_INTRO, 343 m0_PC_INTRO0, m0_TEMPORAL_PC_INTRO0] 344 val cnv = 345 REWRITE_CONV [alignmentTheory.aligned_numeric, 346 m0_stepTheory.Aligned_Branch, 347 m0_stepTheory.Aligned_LoadStore] 348 val m0_PC_bump_intro = 349 SPEC_IMP_RULE o 350 Conv.CONV_RULE (Conv.LAND_CONV cnv) o 351 MP_m0_PC_INTRO o 352 Conv.CONV_RULE 353 (helperLib.POST_CONV (helperLib.MOVE_OUT_CONV ``m0_REG RName_PC``)) 354 fun is_big_end tm = 355 case Lib.total (pairSyntax.dest_pair o dest_m0_CONFIG) tm of 356 SOME (t, _) => t = boolSyntax.T 357 | _ => false 358 val le_sep_array_introduction = 359 stateLib.sep_array_intro 360 false m0_progTheory.m0_WORD_def [m0_stepTheory.concat_bytes] 361 val be_sep_array_introduction = 362 stateLib.sep_array_intro 363 true m0_progTheory.m0_BE_WORD_def [m0_stepTheory.concat_bytes] 364 val concat_bytes_rule = 365 Conv.CONV_RULE 366 (helperLib.POST_CONV (PURE_REWRITE_CONV [m0_stepTheory.concat_bytes])) 367in 368 val memory_introduction = 369 stateLib.introduce_map_definition 370 (m0_progTheory.m0_MEMORY_INSERT, addr_eq_conv) 371 val register_introduction = 372 concat_bytes_rule o 373 stateLib.introduce_map_definition 374 (m0_progTheory.m0_REGISTERS_INSERT, REG_CONV) 375 val sep_array_introduction = 376 stateLib.pick_endian_rule 377 (is_big_end, be_sep_array_introduction, le_sep_array_introduction) 378 val m0_introduction = 379 flag_introduction o 380 m0_PC_bump_intro o 381 stateLib.introduce_triple_definition (false, m0_PC_def) o 382 stateLib.introduce_triple_definition (true, m0_CONFIG_def) o 383 extend_m0_code_pool o 384 m0_rename 385end 386 387local 388 fun check_unique_reg_CONV tm = 389 let 390 val p = progSyntax.strip_star (temporal_stateSyntax.dest_pre' tm) 391 val rp = List.mapPartial (Lib.total (fst o dest_m0_REG)) p 392 in 393 if Lib.mk_set rp = rp 394 then Conv.ALL_CONV tm 395 else raise ERR "check_unique_reg_CONV" "duplicate register" 396 end 397 fun DEPTH_COND_CONV cnv = 398 Conv.ONCE_DEPTH_CONV 399 (fn tm => 400 if progSyntax.is_cond tm 401 then Conv.RAND_CONV cnv tm 402 else raise ERR "COND_CONV" "") 403 val POOL_CONV = Conv.RATOR_CONV o Conv.RAND_CONV 404 val OPC_CONV = POOL_CONV o Conv.RATOR_CONV o Conv.RAND_CONV o Conv.RAND_CONV 405 exception FalseTerm 406 fun NOT_F_CONV tm = 407 if tm = boolSyntax.F then raise FalseTerm else Conv.ALL_CONV tm 408 val WGROUND_RW_CONV = 409 Conv.DEPTH_CONV (utilsLib.cache 10 Term.compare bitstringLib.v2w_n2w_CONV) 410 THENC utilsLib.WGROUND_CONV 411 val PRE_COND_CONV = 412 helperLib.PRE_CONV 413 (DEPTH_COND_CONV 414 (REWRITE_CONV [alignmentTheory.aligned_numeric] 415 THENC NOT_F_CONV) 416 THENC PURE_ONCE_REWRITE_CONV [stateTheory.cond_true_elim]) 417 val cnv = 418 REG_CONV 419 THENC check_unique_reg_CONV 420 THENC WGROUND_RW_CONV 421 THENC PRE_COND_CONV 422 THENC helperLib.POST_CONV (stateLib.PC_CONV "m0_prog$m0_PC") 423in 424 fun simp_triple_rule thm = 425 m0_rename (Conv.CONV_RULE cnv thm) 426 handle FalseTerm => raise ERR "simp_triple_rule" "condition false" 427end 428 429local 430 fun mk_bool_list l = listSyntax.mk_list (l, Type.bool) 431 fun reverse_end b l = 432 mk_bool_list (if b then List.drop (l, 8) @ List.take (l, 8) else l) 433in 434 fun mk_thumb2_pair bigend tm = 435 let 436 val t = fst (bitstringSyntax.dest_v2w tm) 437 val l = fst (listSyntax.dest_list t) 438 val r = reverse_end bigend 439 in 440 if 16 < List.length l 441 then let 442 val l1 = List.take (l, 16) 443 val l2 = List.drop (l, 16) 444 in 445 pairSyntax.mk_pair (r l1, r l2) 446 end 447 else if bigend 448 then r l 449 else t 450 end 451 val get_code = snd o pairSyntax.dest_pair o List.last o 452 pred_setSyntax.strip_set o 453 temporal_stateSyntax.dest_code' o Thm.concl 454 fun get_opcode bigend = mk_thumb2_pair bigend o boolSyntax.rand o get_code 455end 456 457datatype memory = Flat | Array | Map 458type opt = {gpr_map: bool, mem: memory, temporal: bool} 459 460local 461 val gpr_map_options = 462 [["map-gpr", "gpr-map", "reg-map", "map-reg"], 463 ["no-map-gpr", "no-gpr-map"]] 464 val mem_options = 465 [["map-mem", "mem-map", "mapped"], 466 ["array-mem", "mem-array", "array"], 467 ["flat-map", "mem-flat", "flat"]] 468 val temporal_options = 469 [["temporal"], 470 ["not-temporal"]] 471 fun isDelim c = Char.isPunct c andalso c <> #"-" orelse Char.isSpace c 472 val memopt = 473 fn 0 => Map 474 | 1 => Array 475 | 2 => Flat 476 | _ => raise ERR "process_rule_options" "" 477 val print_options = utilsLib.print_options (SOME 24) 478in 479 fun basic_opt () = 480 {gpr_map = false, mem = Flat, 481 temporal = stateLib.generate_temporal()}: opt 482 val default_opt = {gpr_map = false, mem = Map, temporal = false}: opt 483 fun proj_opt ({gpr_map, mem, ...}: opt) = (gpr_map, mem) 484 fun closeness (target: opt) (opt: opt) = 485 (case (#gpr_map opt, #gpr_map target) of 486 (false, true) => 0 487 | (true, false) => ~100 488 | (_, _) => 1) + 489 (case (#mem opt, #mem target) of 490 (Flat, _) => 0 491 | (_, Flat) => ~100 492 | (m1, m2) => if m1 = m2 then 1 else ~10) 493 fun convert_opt_rule (opt: opt) (target: opt) = 494 (if #gpr_map target andalso not (#gpr_map opt) 495 then register_introduction 496 else Lib.I) o 497 (if #mem target = #mem opt 498 then Lib.I 499 else case #mem target of 500 Flat => Lib.I 501 | Array => sep_array_introduction 502 | Map => memory_introduction) 503 fun process_rule_options s = 504 let 505 val l = String.tokens isDelim s 506 val l = List.map utilsLib.lowercase l 507 val (gpr_map, l) = 508 utilsLib.process_opt gpr_map_options "Introduce GPR map" 509 (#gpr_map default_opt) l (Lib.equal 0) 510 val (mem, l) = 511 utilsLib.process_opt mem_options "MEM type" 512 (#mem default_opt) l memopt 513 val (temporal, l) = 514 utilsLib.process_opt temporal_options "Temoporal triple" 515 (#temporal default_opt) l (Lib.equal 0) 516 in 517 if List.null l 518 then {gpr_map = gpr_map, mem = mem, temporal = temporal}: opt 519 else ( print_options "Register view" gpr_map_options 520 ; print_options "Memory view" mem_options 521 ; print_options "Temporal triple" temporal_options 522 ; raise ERR "process_options" 523 ("Unrecognized option" ^ 524 (if List.length l > 1 then "s" else "") ^ 525 ": " ^ String.concat (commafy l)) 526 ) 527 end 528end 529 530local 531 val component_11 = 532 (case Drule.CONJUNCTS m0_progTheory.m0_component_11 of 533 [r, _, m, _] => [r, m] 534 | _ => raise ERR "component_11" "") 535 val sym_R_x_pc = 536 REWRITE_RULE [utilsLib.qm [] ``(a = RName_PC) = (RName_PC = a)``] 537 m0_stepTheory.R_x_pc 538 val EXTRA_TAC = 539 RULE_ASSUM_TAC (REWRITE_RULE [sym_R_x_pc, m0_stepTheory.R_x_pc]) 540 THEN ASM_REWRITE_TAC [boolTheory.DE_MORGAN_THM] 541 val m0_rwts = tl (utilsLib.datatype_rewrites true "m0" ["m0_state", "PSR"]) 542 val STATE_TAC = ASM_REWRITE_TAC m0_rwts 543 val spec = 544 stateLib.spec 545 m0_progTheory.M0_IMP_SPEC 546 m0_progTheory.M0_IMP_TEMPORAL_NEXT 547 [m0_stepTheory.get_bytes] 548 [] 549 (m0_select_state_pool_thm :: m0_select_state_thms) 550 [m0_frame, m0_frame_hidden, state_id] 551 component_11 552 [word, ``:RName``] 553 EXTRA_TAC STATE_TAC 554 val newline = ref "\n" 555 fun x n = Term.mk_var ("x" ^ Int.toString n, Type.bool) 556 fun stm_base s = 557 if String.isPrefix "STM" s 558 then let 559 val (x0,x1,x2) = 560 s |> utilsLib.splitAtChar (Char.isDigit) 561 |> snd 562 |> String.tokens (Lib.equal #",") 563 |> List.map Arbnum.fromString 564 |> mlibUseful.min Arbnum.compare 565 |> fst 566 |> bitstringSyntax.num_to_bitlist 567 |> utilsLib.padLeft false 3 568 |> List.map bitstringSyntax.mk_b 569 |> Lib.triple_of_list 570 in 571 SOME [x 0 |-> x0, x 1 |-> x1, x 2 |-> x2] 572 end 573 handle General.Size => raise ERR "stm_base" "base too large" 574 else NONE 575 val bigend = ref false 576 fun get_opc thm = get_opcode (!bigend) thm 577 val (reset_db, set_current_opt, get_current_opt, add1_pending, find_spec, 578 list_db) = 579 spec_databaseLib.mk_spec_database basic_opt default_opt proj_opt 580 closeness convert_opt_rule get_opc (m0_introduction o spec) 581 val the_step = ref (m0_stepLib.thumb_step (!bigend, false)) 582 val spec_label_set = ref (Redblackset.empty String.compare) 583 fun reset_specs () = 584 (reset_db (); spec_label_set := Redblackset.empty String.compare) 585 fun configure be options = 586 let 587 val opt = process_rule_options options 588 in 589 if !bigend = be andalso #temporal (get_current_opt ()) = #temporal opt 590 then () 591 else ( reset_specs () 592 ; bigend := be 593 ; the_step := m0_stepLib.thumb_step (be, false) 594 ) 595 ; stateLib.set_temporal (#temporal opt) 596 ; set_current_opt opt 597 end 598 fun m0_spec_opt be opt = 599 let 600 val () = configure be opt 601 val step = !the_step 602 in 603 fn s => 604 let 605 val thms = step s 606 val thms = case (thms, stm_base s) of 607 ([thm], SOME m) => 608 [REG_RULE (Thm.INST m thm), thm] 609 | _ => thms 610 val ts = List.map m0_mk_pre_post thms 611 val thms_ts = 612 List.concat 613 (List.map combinations (ListPair.zip (thms, ts))) 614 in 615 List.map (fn x => (print "."; add1_pending x)) thms_ts 616 ; thms_ts 617 end 618 end 619 val the_spec = ref (m0_spec_opt (!bigend) "") 620 fun spec_spec opc thm = 621 let 622 val thm_opc = get_opc thm 623 val a = fst (Term.match_term thm_opc opc) 624 in 625 simp_triple_rule (Thm.INST a thm) 626 end 627in 628 val list_db = list_db 629 fun set_newline s = newline := s 630 fun m0_config be opt = the_spec := m0_spec_opt be opt 631 fun m0_spec s = List.map spec ((!the_spec) s) 632 fun addInstructionClass s = 633 if Redblackset.member (!spec_label_set, s) 634 then false 635 else (print (" " ^ s) 636 ; (!the_spec) s 637 ; spec_label_set := Redblackset.add (!spec_label_set, s) 638 ; true) 639 fun m0_spec_hex looped s = 640 let 641 val opc = m0_stepLib.hex_to_bits s 642 in 643 case find_spec opc of 644 SOME (new, thms) => 645 let 646 val l = List.mapPartial (Lib.total (spec_spec opc)) thms 647 in 648 if List.null l 649 then loop looped opc "failed to find suitable spec" s 650 else (if new then print (!newline) else (); l) 651 end 652 | NONE => loop looped opc "failed to add suitable spec" s 653 end 654 and loop looped opc e s = 655 if looped orelse 656 not (addInstructionClass (m0_stepLib.thumb_instruction opc)) 657 then raise ERR "m0_spec_hex" (e ^ ": " ^ s) 658 else m0_spec_hex true s 659 val m0_spec_hex = m0_spec_hex false 660 val m0_spec_code = List.map m0_spec_hex o 661 (m0AssemblerLib.m0_code: string quotation -> string list) 662end 663 664(* ------------------------------------------------------------------------ *) 665 666(* Testing... 667 668open m0_progLib 669 670m0_config false "flat" 671m0_config false "array" 672m0_config false "mapped" 673m0_config false "reg-map,flat" 674m0_config false "reg-map,array" 675m0_config false "reg-map,mapped" 676 677m0_config true "flat" 678m0_config true "array" 679m0_config true "mapped" 680m0_config true "reg-map,flat" 681m0_config true "reg-map,array" 682m0_config true "reg-map,mapped" 683 684m0_config false "temporal,flat" 685m0_config false "temporal,array" 686m0_config false "temporal,mapped" 687m0_config false "temporal,reg-map,flat" 688m0_config false "temporal,reg-map,array" 689m0_config false "temporal,reg-map,mapped" 690 691m0_config true "temporal,flat" 692m0_config true "temporal,array" 693m0_config true "temporal,mapped" 694m0_config true "temporal,reg-map,flat" 695m0_config true "temporal,reg-map,array" 696m0_config true "temporal,reg-map,mapped" 697 698m0_spec_hex "4906" (* ldr r1, [pc, #24] *) 699m0_spec_hex "B406" (* push {r1, r2} *) 700 701list_db () 702 703local 704 val gen = Random.newgenseed 1.0 705 fun random_bit () = 706 if Random.range (0, 2) gen = 0 then boolSyntax.T else boolSyntax.F 707 val d_list = fst o listSyntax.dest_list 708 fun mk_hextstring tm = 709 case Lib.total pairSyntax.dest_pair tm of 710 SOME (l, r) => 711 bitstringSyntax.hexstring_of_term 712 (listSyntax.mk_list (d_list l @ d_list r, Type.bool)) 713 | NONE => bitstringSyntax.hexstring_of_term tm 714in 715 fun random_hex tm = 716 let 717 val l = Term.free_vars tm 718 val s = List.map (fn v => v |-> random_bit ()) l 719 in 720 mk_hextstring (Term.subst s tm) 721 end 722end 723 724val l = m0_stepLib.list_instructions() 725 |> List.filter (fn (s, _) => s <> "ADD (pc)") 726 |> List.map (random_hex o snd) 727 728val tst = Count.apply (fn s => case Lib.total m0_spec_hex s of 729 SOME l => mlibUseful.INL (s, l) 730 | NONE => mlibUseful.INR s) 731 732val results = List.map tst l 733 734val ok = List.mapPartial (fn mlibUseful.INL (s, _) => SOME s | _ => NONE) results 735val failing = List.mapPartial (fn mlibUseful.INR s => SOME s | _ => NONE) results 736 737val step = m0_stepLib.thumb_step (false, false) 738val step_hex = m0_stepLib.thumb_step_hex (false, false) 739val dec_hex = m0_stepLib.thumb_decode_hex false 740step_hex "C205" 741dec_hex "C205" 742m0_spec_hex "C205" 743val s = m0_stepLib.thumb_instruction (m0_stepLib.hex_to_bits ("C205")) 744step s 745 746m0_config (false, false) 747m0_config (true, true) 748 749m0_spec "B.W" 750 751m0_spec "BL" 752m0_spec "B.W" 753 754m0_spec "ADCS" 755m0_spec_hex "416B" 756 757m0_spec_hex "F302B3DA" 758val s = "PUSH;7,6,4,3,2,1,0" 759 760val ev = m0_stepLib.thumb_step (false, false) 761val ev = m0_stepLib.thumb_step_hex (false, false) 762ev "451F" (* unredictable *) 763ev "CF21" (* not supported?? ldmia r7!, {r0, r5} *) 764 765ev "LDM (wb); 0, 5" 766 767ok 768failing 769List.length ok 770List.length failing 771 772val imp_spec = M0_IMP_SPEC 773val read_thms = [m0_stepTheory.get_bytes] 774val write_thms = []: thm list 775val select_state_thms = (m0_select_state_pool_thm :: m0_select_state_thms) 776val frame_thms = [m0_frame, m0_frame_hidden, state_id] 777val map_tys = [word, ``:RName``] 778val mk_pre_post = m0_mk_pre_post 779val write = m0_write_footprint 780 781*) 782 783(* ------------------------------------------------------------------------ *) 784 785end 786