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 => Teq 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 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 tml_eq 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 (aconv 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, _) => Teq 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 HOLset.numItems (listset rp) = length rp then Conv.ALL_CONV tm 394 else raise ERR "check_unique_reg_CONV" "duplicate register" 395 end 396 fun DEPTH_COND_CONV cnv = 397 Conv.ONCE_DEPTH_CONV 398 (fn tm => 399 if progSyntax.is_cond tm 400 then Conv.RAND_CONV cnv tm 401 else raise ERR "COND_CONV" "") 402 val POOL_CONV = Conv.RATOR_CONV o Conv.RAND_CONV 403 val OPC_CONV = POOL_CONV o Conv.RATOR_CONV o Conv.RAND_CONV o Conv.RAND_CONV 404 exception FalseTerm 405 fun NOT_F_CONV tm = 406 if Feq tm then raise FalseTerm else Conv.ALL_CONV tm 407 val WGROUND_RW_CONV = 408 Conv.DEPTH_CONV (utilsLib.cache 10 Term.compare bitstringLib.v2w_n2w_CONV) 409 THENC utilsLib.WGROUND_CONV 410 val PRE_COND_CONV = 411 helperLib.PRE_CONV 412 (DEPTH_COND_CONV 413 (REWRITE_CONV [alignmentTheory.aligned_numeric] 414 THENC NOT_F_CONV) 415 THENC PURE_ONCE_REWRITE_CONV [stateTheory.cond_true_elim]) 416 val cnv = 417 REG_CONV 418 THENC check_unique_reg_CONV 419 THENC WGROUND_RW_CONV 420 THENC PRE_COND_CONV 421 THENC helperLib.POST_CONV (stateLib.PC_CONV "m0_prog$m0_PC") 422in 423 fun simp_triple_rule thm = 424 m0_rename (Conv.CONV_RULE cnv thm) 425 handle FalseTerm => raise ERR "simp_triple_rule" "condition false" 426end 427 428local 429 fun mk_bool_list l = listSyntax.mk_list (l, Type.bool) 430 fun reverse_end b l = 431 mk_bool_list (if b then List.drop (l, 8) @ List.take (l, 8) else l) 432in 433 fun mk_thumb2_pair bigend tm = 434 let 435 val t = fst (bitstringSyntax.dest_v2w tm) 436 val l = fst (listSyntax.dest_list t) 437 val r = reverse_end bigend 438 in 439 if 16 < List.length l 440 then let 441 val l1 = List.take (l, 16) 442 val l2 = List.drop (l, 16) 443 in 444 pairSyntax.mk_pair (r l1, r l2) 445 end 446 else if bigend 447 then r l 448 else t 449 end 450 val get_code = snd o pairSyntax.dest_pair o List.last o 451 pred_setSyntax.strip_set o 452 temporal_stateSyntax.dest_code' o Thm.concl 453 fun get_opcode bigend = mk_thumb2_pair bigend o boolSyntax.rand o get_code 454end 455 456datatype memory = Flat | Array | Map 457type opt = {gpr_map: bool, mem: memory, temporal: bool} 458 459local 460 val gpr_map_options = 461 [["map-gpr", "gpr-map", "reg-map", "map-reg"], 462 ["no-map-gpr", "no-gpr-map"]] 463 val mem_options = 464 [["map-mem", "mem-map", "mapped"], 465 ["array-mem", "mem-array", "array"], 466 ["flat-map", "mem-flat", "flat"]] 467 val temporal_options = 468 [["temporal"], 469 ["not-temporal"]] 470 fun isDelim c = Char.isPunct c andalso c <> #"-" orelse Char.isSpace c 471 val memopt = 472 fn 0 => Map 473 | 1 => Array 474 | 2 => Flat 475 | _ => raise ERR "process_rule_options" "" 476 val print_options = utilsLib.print_options (SOME 24) 477in 478 fun basic_opt () = 479 {gpr_map = false, mem = Flat, 480 temporal = stateLib.generate_temporal()}: opt 481 val default_opt = {gpr_map = false, mem = Map, temporal = false}: opt 482 fun proj_opt ({gpr_map, mem, ...}: opt) = (gpr_map, mem) 483 fun closeness (target: opt) (opt: opt) = 484 (case (#gpr_map opt, #gpr_map target) of 485 (false, true) => 0 486 | (true, false) => ~100 487 | (_, _) => 1) + 488 (case (#mem opt, #mem target) of 489 (Flat, _) => 0 490 | (_, Flat) => ~100 491 | (m1, m2) => if m1 = m2 then 1 else ~10) 492 fun convert_opt_rule (opt: opt) (target: opt) = 493 (if #gpr_map target andalso not (#gpr_map opt) 494 then register_introduction 495 else Lib.I) o 496 (if #mem target = #mem opt 497 then Lib.I 498 else case #mem target of 499 Flat => Lib.I 500 | Array => sep_array_introduction 501 | Map => memory_introduction) 502 fun process_rule_options s = 503 let 504 val l = String.tokens isDelim s 505 val l = List.map utilsLib.lowercase l 506 val (gpr_map, l) = 507 utilsLib.process_opt gpr_map_options "Introduce GPR map" 508 (#gpr_map default_opt) l (Lib.equal 0) 509 val (mem, l) = 510 utilsLib.process_opt mem_options "MEM type" 511 (#mem default_opt) l memopt 512 val (temporal, l) = 513 utilsLib.process_opt temporal_options "Temoporal triple" 514 (#temporal default_opt) l (Lib.equal 0) 515 in 516 if List.null l 517 then {gpr_map = gpr_map, mem = mem, temporal = temporal}: opt 518 else ( print_options "Register view" gpr_map_options 519 ; print_options "Memory view" mem_options 520 ; print_options "Temporal triple" temporal_options 521 ; raise ERR "process_options" 522 ("Unrecognized option" ^ 523 (if List.length l > 1 then "s" else "") ^ 524 ": " ^ String.concat (commafy l)) 525 ) 526 end 527end 528 529local 530 val component_11 = 531 (case Drule.CONJUNCTS m0_progTheory.m0_component_11 of 532 [r, _, m, _] => [r, m] 533 | _ => raise ERR "component_11" "") 534 val sym_R_x_pc = 535 REWRITE_RULE [utilsLib.qm [] ``(a = RName_PC) = (RName_PC = a)``] 536 m0_stepTheory.R_x_pc 537 val EXTRA_TAC = 538 RULE_ASSUM_TAC (REWRITE_RULE [sym_R_x_pc, m0_stepTheory.R_x_pc]) 539 THEN ASM_REWRITE_TAC [boolTheory.DE_MORGAN_THM] 540 val m0_rwts = tl (utilsLib.datatype_rewrites true "m0" ["m0_state", "PSR"]) 541 val STATE_TAC = ASM_REWRITE_TAC m0_rwts 542 val spec = 543 stateLib.spec 544 m0_progTheory.M0_IMP_SPEC 545 m0_progTheory.M0_IMP_TEMPORAL_NEXT 546 [m0_stepTheory.get_bytes] 547 [] 548 (m0_select_state_pool_thm :: m0_select_state_thms) 549 [m0_frame, m0_frame_hidden, state_id] 550 component_11 551 [word, ``:RName``] 552 EXTRA_TAC STATE_TAC 553 val newline = ref "\n" 554 fun x n = Term.mk_var ("x" ^ Int.toString n, Type.bool) 555 fun stm_base s = 556 if String.isPrefix "STM" s 557 then let 558 val (x0,x1,x2) = 559 s |> utilsLib.splitAtChar (Char.isDigit) 560 |> snd 561 |> String.tokens (Lib.equal #",") 562 |> List.map Arbnum.fromString 563 |> mlibUseful.min Arbnum.compare 564 |> fst 565 |> bitstringSyntax.num_to_bitlist 566 |> utilsLib.padLeft false 3 567 |> List.map bitstringSyntax.mk_b 568 |> Lib.triple_of_list 569 in 570 SOME [x 0 |-> x0, x 1 |-> x1, x 2 |-> x2] 571 end 572 handle General.Size => raise ERR "stm_base" "base too large" 573 else NONE 574 val bigend = ref false 575 fun get_opc thm = get_opcode (!bigend) thm 576 val (reset_db, set_current_opt, get_current_opt, add1_pending, find_spec, 577 list_db) = 578 spec_databaseLib.mk_spec_database basic_opt default_opt proj_opt 579 closeness convert_opt_rule get_opc (m0_introduction o spec) 580 val the_step = ref (m0_stepLib.thumb_step (!bigend, false)) 581 val spec_label_set = ref (Redblackset.empty String.compare) 582 fun reset_specs () = 583 (reset_db (); spec_label_set := Redblackset.empty String.compare) 584 fun configure be options = 585 let 586 val opt = process_rule_options options 587 in 588 if !bigend = be andalso #temporal (get_current_opt ()) = #temporal opt 589 then () 590 else ( reset_specs () 591 ; bigend := be 592 ; the_step := m0_stepLib.thumb_step (be, false) 593 ) 594 ; stateLib.set_temporal (#temporal opt) 595 ; set_current_opt opt 596 end 597 fun m0_spec_opt be opt = 598 let 599 val () = configure be opt 600 val step = !the_step 601 in 602 fn s => 603 let 604 val thms = step s 605 val thms = case (thms, stm_base s) of 606 ([thm], SOME m) => 607 [REG_RULE (Thm.INST m thm), thm] 608 | _ => thms 609 val ts = List.map m0_mk_pre_post thms 610 val thms_ts = 611 List.concat 612 (List.map combinations (ListPair.zip (thms, ts))) 613 in 614 List.map (fn x => (print "."; add1_pending x)) thms_ts 615 ; thms_ts 616 end 617 end 618 val the_spec = ref (m0_spec_opt (!bigend) "") 619 fun spec_spec opc thm = 620 let 621 val thm_opc = get_opc thm 622 val a = fst (Term.match_term thm_opc opc) 623 in 624 simp_triple_rule (Thm.INST a thm) 625 end 626in 627 val list_db = list_db 628 fun set_newline s = newline := s 629 fun m0_config be opt = the_spec := m0_spec_opt be opt 630 fun m0_spec s = List.map spec ((!the_spec) s) 631 fun addInstructionClass s = 632 if Redblackset.member (!spec_label_set, s) 633 then false 634 else (print (" " ^ s) 635 ; (!the_spec) s 636 ; spec_label_set := Redblackset.add (!spec_label_set, s) 637 ; true) 638 fun m0_spec_hex looped s = 639 let 640 val opc = m0_stepLib.hex_to_bits s 641 in 642 case find_spec opc of 643 SOME (new, thms) => 644 let 645 val l = List.mapPartial (Lib.total (spec_spec opc)) thms 646 in 647 if List.null l 648 then loop looped opc "failed to find suitable spec" s 649 else (if new then print (!newline) else (); l) 650 end 651 | NONE => loop looped opc "failed to add suitable spec" s 652 end 653 and loop looped opc e s = 654 if looped orelse 655 not (addInstructionClass (m0_stepLib.thumb_instruction opc)) 656 then raise ERR "m0_spec_hex" (e ^ ": " ^ s) 657 else m0_spec_hex true s 658 val m0_spec_hex = m0_spec_hex false 659 val m0_spec_code = List.map m0_spec_hex o 660 (m0AssemblerLib.m0_code: string quotation -> string list) 661end 662 663(* ------------------------------------------------------------------------ *) 664 665(* Testing... 666 667open m0_progLib 668 669m0_config false "flat" 670m0_config false "array" 671m0_config false "mapped" 672m0_config false "reg-map,flat" 673m0_config false "reg-map,array" 674m0_config false "reg-map,mapped" 675 676m0_config true "flat" 677m0_config true "array" 678m0_config true "mapped" 679m0_config true "reg-map,flat" 680m0_config true "reg-map,array" 681m0_config true "reg-map,mapped" 682 683m0_config false "temporal,flat" 684m0_config false "temporal,array" 685m0_config false "temporal,mapped" 686m0_config false "temporal,reg-map,flat" 687m0_config false "temporal,reg-map,array" 688m0_config false "temporal,reg-map,mapped" 689 690m0_config true "temporal,flat" 691m0_config true "temporal,array" 692m0_config true "temporal,mapped" 693m0_config true "temporal,reg-map,flat" 694m0_config true "temporal,reg-map,array" 695m0_config true "temporal,reg-map,mapped" 696 697m0_spec_hex "4906" (* ldr r1, [pc, #24] *) 698m0_spec_hex "B406" (* push {r1, r2} *) 699 700list_db () 701 702local 703 val gen = Random.newgenseed 1.0 704 fun random_bit () = 705 if Random.range (0, 2) gen = 0 then boolSyntax.T else boolSyntax.F 706 val d_list = fst o listSyntax.dest_list 707 fun mk_hextstring tm = 708 case Lib.total pairSyntax.dest_pair tm of 709 SOME (l, r) => 710 bitstringSyntax.hexstring_of_term 711 (listSyntax.mk_list (d_list l @ d_list r, Type.bool)) 712 | NONE => bitstringSyntax.hexstring_of_term tm 713in 714 fun random_hex tm = 715 let 716 val l = Term.free_vars tm 717 val s = List.map (fn v => v |-> random_bit ()) l 718 in 719 mk_hextstring (Term.subst s tm) 720 end 721end 722 723val l = m0_stepLib.list_instructions() 724 |> List.filter (fn (s, _) => s <> "ADD (pc)") 725 |> List.map (random_hex o snd) 726 727val tst = Count.apply (fn s => case Lib.total m0_spec_hex s of 728 SOME l => mlibUseful.INL (s, l) 729 | NONE => mlibUseful.INR s) 730 731val results = List.map tst l 732 733val ok = List.mapPartial (fn mlibUseful.INL (s, _) => SOME s | _ => NONE) results 734val failing = List.mapPartial (fn mlibUseful.INR s => SOME s | _ => NONE) results 735 736val step = m0_stepLib.thumb_step (false, false) 737val step_hex = m0_stepLib.thumb_step_hex (false, false) 738val dec_hex = m0_stepLib.thumb_decode_hex false 739step_hex "C205" 740dec_hex "C205" 741m0_spec_hex "C205" 742val s = m0_stepLib.thumb_instruction (m0_stepLib.hex_to_bits ("C205")) 743step s 744 745m0_config (false, false) 746m0_config (true, true) 747 748m0_spec "B.W" 749 750m0_spec "BL" 751m0_spec "B.W" 752 753m0_spec "ADCS" 754m0_spec_hex "416B" 755 756m0_spec_hex "F302B3DA" 757val s = "PUSH;7,6,4,3,2,1,0" 758 759val ev = m0_stepLib.thumb_step (false, false) 760val ev = m0_stepLib.thumb_step_hex (false, false) 761ev "451F" (* unredictable *) 762ev "CF21" (* not supported?? ldmia r7!, {r0, r5} *) 763 764ev "LDM (wb); 0, 5" 765 766ok 767failing 768List.length ok 769List.length failing 770 771val imp_spec = M0_IMP_SPEC 772val read_thms = [m0_stepTheory.get_bytes] 773val write_thms = []: thm list 774val select_state_thms = (m0_select_state_pool_thm :: m0_select_state_thms) 775val frame_thms = [m0_frame, m0_frame_hidden, state_id] 776val map_tys = [word, ``:RName``] 777val mk_pre_post = m0_mk_pre_post 778val write = m0_write_footprint 779 780*) 781 782(* ------------------------------------------------------------------------ *) 783 784end 785