1structure arm_progLib :> arm_progLib = 2struct 3 4open HolKernel boolLib bossLib 5open stateLib spec_databaseLib arm_progTheory 6 7structure Parse = 8struct 9 open Parse 10 val (Type, Term) = parse_from_grammars arm_progTheory.arm_prog_grammars 11end 12 13open Parse 14 15val ERR = Feedback.mk_HOL_ERR "arm_progLib" 16 17(* ------------------------------------------------------------------------ *) 18 19val arm_proj_def = arm_progTheory.arm_proj_def 20val arm_comp_defs = arm_progTheory.component_defs 21 22local 23 val pc = Term.prim_mk_const {Thy = "arm", Name = "RName_PC"} 24in 25 val step_1 = HolKernel.syntax_fns1 "arm_step" 26 val arm_1 = 27 HolKernel.syntax_fns 28 {n = 2, dest = HolKernel.dest_monop, make = HolKernel.mk_monop} 29 "arm_prog" 30 val arm_2 = 31 HolKernel.syntax_fns 32 {n = 3, dest = HolKernel.dest_binop, make = HolKernel.mk_binop} 33 "arm_prog" 34 val word5 = wordsSyntax.mk_int_word_type 5 35 val word = wordsSyntax.mk_int_word_type 32 36 val dword = wordsSyntax.mk_int_word_type 64 37 val (_, _, dest_arm_instr, _) = arm_1 "arm_instr" 38 val (_, _, dest_arm_CPSR_E, _) = arm_1 "arm_CPSR_E" 39 val (_, _, dest_arm_CONFIG, _) = arm_1 "arm_CONFIG" 40 val (_, _, dest_arm_MEM, is_arm_MEM) = arm_2 "arm_MEM" 41 val (_, mk_arm_REG, dest_arm_REG, is_arm_REG) = arm_2 "arm_REG" 42 val (_, _, dest_arm_FP_REG, is_arm_FP_REG) = arm_2 "arm_FP_REG" 43 val (_, _, dest_arm_Extensions, is_arm_Extensions) = arm_2 "arm_Extensions" 44 val (_, mk_rev_e, _, _) = step_1 "reverse_endian" 45 fun mk_arm_PC v = mk_arm_REG (pc, v) 46end 47 48(* -- *) 49 50val arm_select_state_thms = 51 List.map (fn t => stateLib.star_select_state_thm arm_proj_def [] ([], t)) 52 arm_comp_defs 53 54val arm_select_state_pool_thm = 55 pool_select_state_thm arm_proj_def [] 56 (utilsLib.SRW_CONV 57 [pred_setTheory.INSERT_UNION_EQ, stateTheory.CODE_POOL, arm_instr_def] 58 ``CODE_POOL arm_instr {(pc, opc)}``) 59 60(* -- *) 61 62val state_id = 63 utilsLib.mk_state_id_thm armTheory.arm_state_component_equality 64 [["REG", "undefined"], 65 ["FP", "REG", "undefined"], 66 ["CPSR", "CurrentCondition", "Encoding", "REG", "undefined"], 67 ["CPSR", "CurrentCondition", "Encoding", "undefined"], 68 ["MEM", "REG", "undefined"] 69 ] 70 71val fp_id = 72 utilsLib.mk_state_id_thm armTheory.FP_component_equality 73 [["REG"], ["FPSCR"]] 74 75val PSR_components = 76 ["N", "Z", "C", "V", "Q", "J", "T", "E", "A", "I", "F", "M", "IT", "GE", 77 "psr'rst"] 78 79val FPSCR_components = 80 ["N", "Z", "C", "V", "AHP", "DN", "DZC", "DZE", "FZ", "IDC", "IDE", "IOC", 81 "IOE", "IXC", "IXE", "OFC", "OFE", "QC", "RMode", "UFC", "UFE", "fpscr'rst"] 82 83val arm_frame = 84 stateLib.update_frame_state_thm arm_proj_def 85 (List.map (fn s => "CPSR." ^ s) PSR_components @ 86 List.map (fn s => "FP.FPSCR." ^ s) FPSCR_components @ 87 ["REG", "MEM", "FP.REG"]) 88 89val arm_frame_hidden = 90 stateLib.update_hidden_frame_state_thm arm_proj_def 91 [``s with Encoding := x``, 92 ``s with CurrentCondition := x``, 93 ``s with undefined := x``] 94 95(* -- *) 96 97local 98 val arm_instr_tm = Term.prim_mk_const {Thy = "arm_prog", Name = "arm_instr"} 99 fun is_mem_access v tm = 100 case Lib.total boolSyntax.dest_eq tm of 101 SOME (l, r) => 102 stateLib.is_code_access ("arm$arm_state_MEM", v) l andalso 103 (wordsSyntax.is_word_literal r orelse bitstringSyntax.is_v2w r) 104 | NONE => false 105 val dest_opc = fst o listSyntax.dest_list o fst o bitstringSyntax.dest_v2w 106 val ty32 = fcpSyntax.mk_int_numeric_type 32 107 fun list_mk_concat l = 108 bitstringSyntax.mk_v2w 109 (listSyntax.mk_list 110 (List.concat (List.map dest_opc l), Type.bool), ty32) 111in 112 fun mk_arm_code_pool thm = 113 let 114 val r15 = stateLib.gvar "pc" word 115 val r15_a = mk_arm_PC r15 116 val (a, tm) = Thm.dest_thm thm 117 val r15_subst = Term.subst [``s.REG RName_PC`` |-> r15] 118 val a = List.map r15_subst a 119 val (m, a) = List.partition (is_mem_access r15) a 120 val m = List.map dest_code_access m 121 val m = mlibUseful.sort_map fst Int.compare m 122 val opc = list_mk_concat (List.map snd (List.rev m)) 123 in 124 (r15_a, 125 boolSyntax.rand (stateLib.mk_code_pool (arm_instr_tm, r15, opc)), 126 list_mk_imp (a, r15_subst tm)) 127 end 128end 129 130local 131 val pc_tm = Term.mk_var ("pc", word) 132 fun is_big_end tm = 133 case Lib.total dest_arm_CPSR_E tm of 134 SOME t => t = boolSyntax.T 135 | NONE => false 136 fun is_pc_relative tm = 137 case Lib.total dest_arm_MEM tm of 138 SOME (t, _) => fst (utilsLib.strip_add_or_sub t) = pc_tm 139 | NONE => false 140 fun rwt (w, a) = 141 [Drule.SPECL [a, w] arm_progTheory.MOVE_TO_TEMPORAL_ARM_CODE_POOL, 142 Drule.SPECL [a, w] arm_progTheory.MOVE_TO_ARM_CODE_POOL] 143 fun move_to_code wa = 144 REWRITE_RULE 145 ([stateTheory.BIGUNION_IMAGE_1, stateTheory.BIGUNION_IMAGE_2, 146 set_sepTheory.STAR_ASSOC, set_sepTheory.SEP_CLAUSES, 147 arm_progTheory.disjoint_arm_instr_thms, arm_stepTheory.concat_bytes] @ 148 List.concat (List.map rwt wa)) 149 val err = ERR "DISJOINT_CONV" "" 150 val cnv = 151 LAND_CONV wordsLib.WORD_EVAL_CONV 152 THENC REWRITE_CONV [arm_progTheory.sub_intro] 153 fun split_arm_instr tm = 154 Lib.with_exn (pairSyntax.dest_pair o dest_arm_instr) tm err 155 val byte_chunks = stateLib.group_into_chunks (dest_arm_MEM, 4, false) 156 val rev_end_rule = 157 PURE_REWRITE_RULE 158 [arm_stepTheory.concat_bytes, arm_stepTheory.reverse_endian_bytes] 159 fun rev_intro x = 160 rev_end_rule o Thm.INST (List.map (fn (w, _: term) => w |-> mk_rev_e w) x) 161in 162 fun DISJOINT_CONV tm = 163 let 164 val (l, r) = Lib.with_exn pred_setSyntax.dest_disjoint tm err 165 val (a, x) = split_arm_instr l 166 val y = snd (split_arm_instr r) 167 val a = case utilsLib.strip_add_or_sub a of 168 (_, [(false, w)]) => wordsSyntax.mk_word_2comp w 169 | (_, [(false, w), (true, x)]) => 170 wordsSyntax.mk_word_add (wordsSyntax.mk_word_2comp w, x) 171 | _ => raise err 172 val thm = 173 Conv.CONV_RULE cnv 174 (Drule.SPECL [a, pc_tm, x, y] arm_progTheory.DISJOINT_arm_instr) 175 in 176 if Thm.concl thm = tm 177 then Drule.EQT_INTRO thm 178 else raise err 179 end 180 fun extend_arm_code_pool thm = 181 let 182 val (p, q) = temporal_stateSyntax.dest_pre_post' (Thm.concl thm) 183 val lp = progSyntax.strip_star p 184 in 185 if Lib.exists is_pc_relative lp 186 then let 187 val be = Lib.exists is_big_end lp 188 val (s, wa) = byte_chunks lp 189 in 190 if List.null s 191 then thm 192 else let 193 val thm' = 194 move_to_code wa (Thm.INST (List.concat s) thm) 195 in 196 if be then rev_intro wa thm' else thm' 197 end 198 end 199 else thm 200 end 201end 202 203(* -- *) 204 205fun reg_index tm = 206 case Lib.total Term.dest_thy_const tm of 207 SOME {Thy = "arm", Name = "RName_PC", ...} => 15 208 | _ => Lib.with_exn (wordsSyntax.uint_of_word o Term.rand) tm 209 (ERR "reg_index" "") 210 211local 212 fun other_index tm = 213 case fst (Term.dest_const (boolSyntax.rator tm)) of 214 "cond" => 0 215 | "arm_exception" => 1 216 | "arm_VFPExtension" => 2 217 | "arm_CPSR_A" => 3 218 | "arm_CPSR_I" => 4 219 | "arm_CPSR_F" => 5 220 | "arm_CPSR_psr'rst" => 6 221 | "arm_CPSR_IT" => 7 222 | "arm_CPSR_J" => 10 223 | "arm_CPSR_E" => 11 224 | "arm_CPSR_T" => 12 225 | "arm_CPSR_M" => 13 226 | "arm_CPSR_N" => 14 227 | "arm_CPSR_Z" => 15 228 | "arm_CPSR_C" => 16 229 | "arm_CPSR_V" => 17 230 | "arm_CPSR_Q" => 18 231 | "arm_CPSR_GE" => 19 232 | "arm_FP_FPSCR_N" => 20 233 | "arm_FP_FPSCR_Z" => 21 234 | "arm_FP_FPSCR_C" => 22 235 | "arm_FP_FPSCR_V" => 23 236 | "arm_FP_FPSCR_AHP" => 24 237 | "arm_FP_FPSCR_DN" => 25 238 | "arm_FP_FPSCR_DZC" => 26 239 | "arm_FP_FPSCR_DZE" => 27 240 | "arm_FP_FPSCR_FZ" => 28 241 | "arm_FP_FPSCR_IDC" => 29 242 | "arm_FP_FPSCR_IDE" => 30 243 | "arm_FP_FPSCR_IOC" => 31 244 | "arm_FP_FPSCR_IOE" => 32 245 | "arm_FP_FPSCR_IXC" => 33 246 | "arm_FP_FPSCR_IXE" => 34 247 | "arm_FP_FPSCR_OFC" => 35 248 | "arm_FP_FPSCR_OFE" => 36 249 | "arm_FP_FPSCR_QC" => 37 250 | "arm_FP_FPSCR_RMode" => 38 251 | "arm_FP_FPSCR_UFC" => 39 252 | "arm_FP_FPSCR_UFE" => 40 253 | "arm_FP_FPSCR_fpscr'rst" => 41 254 | _ => ~1 255 val int_of_v2w = 256 Arbnum.toInt o bitstringSyntax.num_of_term o fst o bitstringSyntax.dest_v2w 257 val total_dest_lit = Lib.total wordsSyntax.dest_word_literal 258 fun word_compare (w1, w2) = 259 case (total_dest_lit w1, total_dest_lit w2) of 260 (SOME x1, SOME x2) => Arbnum.compare (x1, x2) 261 | (SOME _, NONE) => General.GREATER 262 | (NONE, SOME _) => General.LESS 263 | (NONE, NONE) => Term.compare (w1, w2) 264 fun reg_compare (r1, r2) = 265 case (r1, r2) of 266 (mlibUseful.INL i, mlibUseful.INL j) => Int.compare (i, j) 267 | (mlibUseful.INL _, mlibUseful.INR _) => General.GREATER 268 | (mlibUseful.INR _, mlibUseful.INL _) => General.LESS 269 | (mlibUseful.INR i, mlibUseful.INR j) => Term.compare (i, j) 270 fun reg tm = 271 case Lib.total reg_index tm of 272 SOME i => mlibUseful.INL i 273 | NONE => mlibUseful.INR tm 274 val register = reg o fst o dest_arm_REG 275 fun fp_reg tm = 276 case Lib.total int_of_v2w tm of 277 SOME i => mlibUseful.INL i 278 | NONE => mlibUseful.INR tm 279 val fp_register = fp_reg o fst o dest_arm_FP_REG 280 val address = HolKernel.strip_binop (Lib.total wordsSyntax.dest_word_add) o 281 fst o dest_arm_MEM 282in 283 fun psort p = 284 let 285 val (m, rst) = List.partition is_arm_MEM p 286 val (r, rst) = List.partition is_arm_REG rst 287 val (c, rst) = List.partition is_arm_FP_REG rst 288 val (e, rst) = List.partition is_arm_Extensions rst 289 in 290 mlibUseful.sort_map other_index Int.compare rst @ 291 mlibUseful.sort_map (fst o dest_arm_Extensions) Term.compare e @ 292 mlibUseful.sort_map register reg_compare r @ 293 mlibUseful.sort_map fp_register reg_compare c @ 294 mlibUseful.sort_map address (mlibUseful.lex_list_order word_compare) m 295 end 296end 297 298local 299 val st = Term.mk_var ("s", ``:arm_state``) 300 fun mk_rec (t, c) = List.map (fn s => ("arm$" ^ t ^ "_" ^ s ^ "_fupd", 301 "arm_" ^ c ^ "_" ^ s)) 302 val cpsr_footprint = 303 stateLib.write_footprint arm_1 arm_2 [] 304 (mk_rec ("PSR", "CPSR") PSR_components) [] [] 305 (fn (s, l) => s = "arm$arm_state_CPSR" andalso l = [st]) 306 val fpscr_footprint = 307 stateLib.write_footprint arm_1 arm_2 [] 308 (mk_rec ("FPSCR", "FP_FPSCR") FPSCR_components) [] [] 309 (fn (s, l) => s = "arm$FP_FPSCR") 310 val fp_footprint = 311 stateLib.write_footprint arm_1 arm_2 312 [("arm$FP_REG_fupd", "arm_FP_REG", ``^st.FP.REG``)] [] [] 313 [("arm$FP_FPSCR_fupd", fpscr_footprint)] 314 (fn (s, l) => s = "arm$arm_state_FP" andalso l = [st]) 315in 316 val arm_write_footprint = 317 stateLib.write_footprint arm_1 arm_2 318 [("arm$arm_state_MEM_fupd", "arm_MEM", ``^st.MEM``), 319 ("arm$arm_state_REG_fupd", "arm_REG", ``^st.REG``)] 320 [] [] 321 [("arm$arm_state_FP_fupd", fp_footprint), 322 ("arm$arm_state_CPSR_fupd", cpsr_footprint), 323 ("arm$arm_state_Encoding_fupd", fn (p, q, _) => (p, q)), 324 ("arm$arm_state_undefined_fupd", fn (p, q, _) => (p, q)), 325 ("arm$arm_state_CurrentCondition_fupd", fn (p, q, _) => (p, q))] 326 (K false) 327end 328 329val arm_mk_pre_post = 330 stateLib.mk_pre_post 331 arm_progTheory.ARM_MODEL_def arm_comp_defs mk_arm_code_pool [] 332 arm_write_footprint psort 333 334(* ------------------------------------------------------------------------ *) 335 336val REG_CONV = 337 Conv.QCONV 338 (REWRITE_CONV 339 [EVAL ``R_mode mode 15w``, 340 arm_stepTheory.v2w_ground4, arm_stepTheory.v2w_ground5]) 341 342val REG_RULE = Conv.CONV_RULE REG_CONV o utilsLib.ALL_HYP_CONV_RULE REG_CONV 343 344local 345 val dest_reg = dest_arm_REG 346 val reg_width = 4 347 val proj_reg = SOME reg_index 348 val reg_conv = REG_CONV 349 val ok_conv = ALL_CONV 350 val r15 = wordsSyntax.mk_wordii (15, 4) 351 fun asm tm = Thm.ASSUME (boolSyntax.mk_neg (boolSyntax.mk_eq (tm, r15))) 352 val model_tm = ``ARM_MODEL`` 353in 354 val reg_combinations = 355 stateLib.register_combinations 356 (dest_reg, reg_width, proj_reg, reg_conv, ok_conv, asm, model_tm) 357end 358 359local 360 fun dest_reg tm = 361 let 362 val x as (r, _) = dest_arm_FP_REG tm 363 in 364 not (wordsSyntax.is_word_add r orelse wordsSyntax.is_word_div r) orelse 365 raise ERR "dest_reg" "" 366 ; x 367 end 368 val reg_width = 5 369 val proj_reg = NONE 370 val reg_conv = REG_CONV 371 val ok_conv = ALL_CONV 372 fun asm (tm: term) = (raise ERR "" ""): thm 373 val model_tm = ``ARM_MODEL`` 374in 375 val fp_combinations = 376 stateLib.register_combinations 377 (dest_reg, reg_width, proj_reg, reg_conv, ok_conv, asm, model_tm) 378end 379 380fun combinations thm_t = 381 case fp_combinations thm_t of 382 [_] => reg_combinations thm_t 383 | l => l 384 385(* ------------------------------------------------------------------------ *) 386 387local 388 val arm_rmap = 389 Lib.total 390 (fn "arm_prog$arm_CPSR_N" => K "n" 391 | "arm_prog$arm_CPSR_Z" => K "z" 392 | "arm_prog$arm_CPSR_C" => K "c" 393 | "arm_prog$arm_CPSR_V" => K "v" 394 | "arm_prog$arm_CPSR_Q" => K "q" 395 | "arm_prog$arm_CPSR_A" => K "a" 396 | "arm_prog$arm_CPSR_F" => K "f" 397 | "arm_prog$arm_CPSR_I" => K "i" 398 | "arm_prog$arm_CPSR_GE" => K "ge" 399 | "arm_prog$arm_CPSR_IT" => K "it" 400 | "arm_prog$arm_CPSR_M" => K "mode" 401 | "arm_prog$arm_CPSR_psr'rst" => K "psr_other" 402 | "arm_prog$arm_SPSR_abt" => K "spsr_abt" 403 | "arm_prog$arm_SPSR_fiq" => K "spsr_fiq" 404 | "arm_prog$arm_SPSR_hyp" => K "spsr_hyp" 405 | "arm_prog$arm_SPSR_irq" => K "spsr_irq" 406 | "arm_prog$arm_SPSR_mon" => K "spsr_mon" 407 | "arm_prog$arm_SPSR_svc" => K "spsr_svc" 408 | "arm_prog$arm_SPSR_und" => K "spsr_und" 409 | "arm_prog$arm_FP_FPSCR_N" => K "fp_n" 410 | "arm_prog$arm_FP_FPSCR_Z" => K "fp_z" 411 | "arm_prog$arm_FP_FPSCR_C" => K "fp_c" 412 | "arm_prog$arm_FP_FPSCR_V" => K "fp_v" 413 | "arm_prog$arm_FP_FPSCR_RMode" => K "rmode" 414 | "arm_prog$arm_CP15" => K "cp15" 415 | "arm_prog$arm_FP_REG" => 416 Lib.curry (op ^) "d" o Int.toString o wordsSyntax.uint_of_word o 417 List.hd 418 | "arm_prog$arm_REG" => 419 Lib.curry (op ^) "r" o Int.toString o reg_index o List.hd 420 | "arm_prog$arm_MEM" => K "b" 421 | _ => fail()) 422in 423 val arm_rename = stateLib.rename_vars (arm_rmap, ["b"]) 424end 425 426local 427 val arm_CPSR_T_F = List.map UNDISCH (CONJUNCTS arm_progTheory.arm_CPSR_T_F) 428 val MOVE_COND_RULE = Conv.CONV_RULE stateLib.MOVE_COND_CONV 429 val SPEC_IMP_RULE = 430 Conv.CONV_RULE 431 (Conv.REWR_CONV (Thm.CONJUNCT1 (Drule.SPEC_ALL boolTheory.IMP_CLAUSES)) 432 ORELSEC MOVE_COND_CONV) 433 fun TRY_DISCH_RULE thm = 434 case List.length (Thm.hyp thm) of 435 0 => thm 436 | 1 => MOVE_COND_RULE (Drule.DISCH_ALL thm) 437 | _ => thm |> Drule.DISCH_ALL 438 |> PURE_REWRITE_RULE [boolTheory.AND_IMP_INTRO] 439 |> MOVE_COND_RULE 440 val flag_introduction = 441 helperLib.MERGE_CONDS_RULE o TRY_DISCH_RULE o 442 PURE_REWRITE_RULE arm_CPSR_T_F 443 val addr_eq_conv = 444 SIMP_CONV (bool_ss++wordsLib.WORD_ARITH_ss++wordsLib.WORD_ARITH_EQ_ss) [] 445 val reg_eq_conv = PURE_REWRITE_CONV [arm_stepTheory.R_mode_11] 446 THENC Conv.DEPTH_CONV wordsLib.word_EQ_CONV 447 THENC REWRITE_CONV [] 448 val arm_PC_INTRO0 = 449 arm_PC_INTRO |> Q.INST [`p1`|->`emp`, `p2`|->`emp`] 450 |> PURE_REWRITE_RULE [set_sepTheory.SEP_CLAUSES] 451 val arm_TEMPORAL_PC_INTRO0 = 452 arm_TEMPORAL_PC_INTRO |> Q.INST [`p1`|->`emp`, `p2`|->`emp`] 453 |> PURE_REWRITE_RULE [set_sepTheory.SEP_CLAUSES] 454 fun MP_arm_PC_INTRO th = 455 Lib.tryfind (fn thm => MATCH_MP thm th) 456 [arm_PC_INTRO, arm_TEMPORAL_PC_INTRO, 457 arm_PC_INTRO0, arm_TEMPORAL_PC_INTRO0] 458 val aligned_cond_rand = 459 utilsLib.mk_cond_rand_thms [``aligned n : 'a word -> bool``] 460 val cnv = REWRITE_CONV [alignmentTheory.aligned_numeric, aligned_cond_rand, 461 arm_progTheory.Aligned_Branch, 462 alignmentTheory.aligned_align] 463 val arm_PC_bump_intro = 464 SPEC_IMP_RULE o 465 Conv.CONV_RULE (Conv.LAND_CONV cnv) o 466 MP_arm_PC_INTRO o 467 Conv.CONV_RULE 468 (helperLib.POST_CONV (helperLib.MOVE_OUT_CONV ``arm_REG RName_PC``)) 469 fun is_big_end tm = 470 case Lib.total (pairSyntax.strip_pair o dest_arm_CONFIG) tm of 471 SOME [_, _, t, _, _] => t = boolSyntax.T 472 | _ => false 473 val le_word_memory_introduction = 474 stateLib.introduce_map_definition 475 (arm_progTheory.arm_WORD_MEMORY_INSERT, addr_eq_conv) o 476 stateLib.chunks_intro false arm_progTheory.arm_WORD_def 477 val be_word_memory_introduction = 478 stateLib.introduce_map_definition 479 (arm_progTheory.arm_BE_WORD_MEMORY_INSERT, addr_eq_conv) o 480 stateLib.chunks_intro true arm_progTheory.arm_BE_WORD_def 481 val le_sep_array_introduction = 482 stateLib.sep_array_intro 483 false arm_progTheory.arm_WORD_def [arm_stepTheory.concat_bytes] 484 val be_sep_array_introduction = 485 stateLib.sep_array_intro 486 true arm_progTheory.arm_BE_WORD_def [arm_stepTheory.concat_bytes] 487 val concat_bytes_rule = 488 Conv.CONV_RULE 489 (helperLib.POST_CONV (PURE_REWRITE_CONV [arm_stepTheory.concat_bytes])) 490in 491 val memory_introduction = 492 stateLib.introduce_map_definition 493 (arm_progTheory.arm_MEMORY_INSERT, addr_eq_conv) 494 val fp_introduction = 495 concat_bytes_rule o 496 stateLib.introduce_map_definition 497 (arm_progTheory.arm_FP_REGISTERS_INSERT, Conv.ALL_CONV) 498 val gp_introduction = 499 concat_bytes_rule o 500 stateLib.introduce_map_definition 501 (arm_progTheory.arm_REGISTERS_INSERT, reg_eq_conv) 502 val sep_array_introduction = 503 stateLib.pick_endian_rule 504 (is_big_end, be_sep_array_introduction, le_sep_array_introduction) 505 val word_memory_introduction = 506 Conv.CONV_RULE 507 (stateLib.PRE_COND_CONV 508 (SIMP_CONV (bool_ss++boolSimps.CONJ_ss) 509 [aligned_cond_rand, alignmentTheory.aligned_numeric])) o 510 concat_bytes_rule o 511 stateLib.pick_endian_rule 512 (is_big_end, be_word_memory_introduction, le_word_memory_introduction) 513 val arm_intro = 514 flag_introduction o 515 arm_PC_bump_intro o 516 stateLib.introduce_triple_definition (false, arm_PC_def) o 517 stateLib.introduce_triple_definition (true, arm_CONFIG_def) o 518 extend_arm_code_pool o 519 arm_rename 520end 521 522local 523 fun is_mode tm = 524 case Lib.total wordsSyntax.dest_word_extract tm of 525 SOME (_, _, _, ty) => ty = fcpSyntax.mk_int_numeric_type 5 526 | NONE => false 527 val config0 = GSYM (SPEC_ALL arm_CONFIG_def) 528 val mode0 = ``mode: word5`` 529 val (_, mk_goodmode, _, _) = step_1 "GoodMode" 530in 531 fun change_config_rule thm = 532 let 533 val mode = HolKernel.find_term is_mode (Thm.concl thm) 534 val config = Thm.INST [mode0 |-> mode] config0 535 in 536 thm 537 |> stateLib.MOVE_COND_RULE (mk_goodmode mode) 538 |> MATCH_MP progTheory.SPEC_DUPLICATE_COND 539 |> CONV_RULE (RAND_CONV (helperLib.STAR_REWRITE_CONV config)) 540 end 541end 542 543local 544 val RName_PC_tm = Term.prim_mk_const {Thy = "arm", Name = "RName_PC"} 545 fun spec_rewrites thm tms = List.map (REWRITE_CONV [thm]) tms 546 val spec_rwts = 547 spec_rewrites armTheory.Extend_def 548 [``Extend (T, w:'a word): 'b word``, 549 ``Extend (F, w:'a word): 'b word``] @ 550 spec_rewrites arm_stepTheory.UpdateSingleOfDouble_def 551 [``UpdateSingleOfDouble T v w``, 552 ``UpdateSingleOfDouble F v w``] @ 553 spec_rewrites arm_stepTheory.SingleOfDouble_def 554 [``SingleOfDouble T w``, 555 ``SingleOfDouble F w``] 556 fun check_unique_reg_CONV tm = 557 let 558 val p = progSyntax.strip_star (temporal_stateSyntax.dest_pre' tm) 559 val rp = List.mapPartial (Lib.total (fst o dest_arm_REG)) p 560 val dp = List.mapPartial (Lib.total (fst o dest_arm_FP_REG)) p 561 in 562 if not (Lib.mem RName_PC_tm rp) andalso 563 Lib.mk_set rp = rp andalso Lib.mk_set dp = dp 564 then Conv.ALL_CONV tm 565 else raise ERR "check_unique_reg_CONV" "duplicate register" 566 end 567 exception FalseTerm 568 fun NOT_F_CONV tm = 569 if tm = boolSyntax.F then raise FalseTerm else Conv.ALL_CONV tm 570 val WGROUND_RW_CONV = 571 Conv.DEPTH_CONV (utilsLib.cache 10 Term.compare bitstringLib.v2w_n2w_CONV) 572 THENC utilsLib.WGROUND_CONV 573 val cnv = 574 REG_CONV 575 THENC check_unique_reg_CONV 576 THENC WGROUND_RW_CONV 577 THENC stateLib.PRE_COND_CONV 578 (DEPTH_CONV DISJOINT_CONV 579 THENC REWRITE_CONV [alignmentTheory.aligned_numeric] 580 THENC numLib.REDUCE_CONV 581 THENC NOT_F_CONV) 582 THENC helperLib.POST_CONV 583 (PURE_REWRITE_CONV spec_rwts 584 THENC stateLib.PC_CONV "arm_prog$arm_PC") 585in 586 fun simp_triple_rule thm = 587 arm_rename (Conv.CONV_RULE cnv thm) 588 handle FalseTerm => raise ERR "simp_triple_rule" "condition false" 589end 590 591local 592 val v3 = Term.mk_var ("x3", Type.bool) 593 val v4 = Term.mk_var ("x4", Type.bool) 594 val v5 = Term.mk_var ("x5", Type.bool) 595 val v6 = Term.mk_var ("x6", Type.bool) 596 val vn = listSyntax.mk_list ([v3, v4, v5, v6], Type.bool) 597 val vn = bitstringSyntax.mk_v2w (vn, fcpSyntax.mk_int_numeric_type 4) 598in 599 val get_stm_base = 600 Arbnum.toInt o fst o 601 mlibUseful.min Arbnum.compare o 602 List.map Arbnum.fromString o 603 String.tokens (Lib.equal #",") o snd o 604 utilsLib.splitAtChar (Char.isDigit) 605 fun stm_wb_thms base thm = 606 let 607 val (x3, x4, x5, x6) = 608 utilsLib.padLeft false 4 609 (bitstringSyntax.num_to_bitlist (Arbnum.fromInt base)) 610 |> List.map bitstringSyntax.mk_b 611 |> Lib.quadruple_of_list 612 in 613 [REG_RULE (Thm.INST [v3 |-> x3, v4 |-> x4, v5 |-> x5, v6 |-> x6] thm), 614 Drule.ADD_ASSUM 615 (boolSyntax.mk_neg 616 (boolSyntax.mk_eq (vn, wordsSyntax.mk_wordii (base, 4)))) thm] 617 end 618end 619 620datatype memory = Flat | Array | Map | Map32 621type opt = {gpr_map: bool, fpr_map: bool, mem: memory, temporal: bool} 622 623local 624 val gpr_map_options = 625 [["map-gpr", "gpr-map", "reg-map", "map-reg"], 626 ["no-map-gpr", "no-gpr-map"]] 627 val fpr_map_options = 628 [["map-fpr", "fpr-map"], 629 ["no-map-fpr", "no-fpr-map"]] 630 val mem_options = 631 [["map-mem", "mem-map", "mapped"], 632 ["map-mem32", "mem-map32", "mapped32"], 633 ["array-mem", "mem-array", "array"], 634 ["flat-map", "mem-flat", "flat"]] 635 val temporal_options = 636 [["temporal"], 637 ["not-temporal"]] 638 fun isDelim c = Char.isPunct c andalso c <> #"-" orelse Char.isSpace c 639 val memopt = 640 fn 0 => Map 641 | 1 => Map32 642 | 2 => Array 643 | 3 => Flat 644 | _ => raise ERR "process_rule_options" "" 645 val print_options = utilsLib.print_options (SOME 34) 646in 647 fun basic_opt () = 648 {gpr_map = false, fpr_map = false, mem = Flat, 649 temporal = stateLib.generate_temporal()}: opt 650 val default_opt = 651 {gpr_map = false, fpr_map = false, mem = Map, temporal = false}: opt 652 fun proj_opt ({gpr_map, fpr_map, mem, ...}: opt) = (gpr_map, fpr_map, mem) 653 fun closeness (target: opt) (opt: opt) = 654 (case (#gpr_map opt, #gpr_map target) of 655 (false, true) => 0 656 | (true, false) => ~100 657 | (_, _) => 1) + 658 (case (#fpr_map opt, #fpr_map target) of 659 (false, true) => 0 660 | (true, false) => ~100 661 | (_, _) => 1) + 662 (case (#mem opt, #mem target) of 663 (Flat, _) => 0 664 | (_, Flat) => ~100 665 | (m1, m2) => if m1 = m2 then 1 else ~10) 666 fun convert_opt_rule (opt: opt) (target: opt) = 667 (if #gpr_map target andalso not (#gpr_map opt) 668 then gp_introduction 669 else Lib.I) o 670 (if #fpr_map target andalso not (#fpr_map opt) 671 then fp_introduction 672 else Lib.I) o 673 (if #mem target = #mem opt 674 then Lib.I 675 else case #mem target of 676 Flat => Lib.I 677 | Array => sep_array_introduction 678 | Map => memory_introduction 679 | Map32 => word_memory_introduction 680 ) 681 fun process_rule_options s = 682 let 683 val l = String.tokens isDelim s 684 val l = List.map utilsLib.lowercase l 685 val (fpr_map, l) = 686 utilsLib.process_opt fpr_map_options "Introduce FPR map" 687 (#fpr_map default_opt) l (Lib.equal 0) 688 val (gpr_map, l) = 689 utilsLib.process_opt gpr_map_options "Introduce GPR map" 690 (#gpr_map default_opt) l (Lib.equal 0) 691 val (mem, l) = 692 utilsLib.process_opt mem_options "MEM type" 693 (#mem default_opt) l memopt 694 val (temporal, l) = 695 utilsLib.process_opt temporal_options "Temoporal triple" 696 (#temporal default_opt) l (Lib.equal 0) 697 in 698 if List.null l 699 then {gpr_map = gpr_map, 700 fpr_map = fpr_map, 701 mem = mem, 702 temporal = temporal}: opt 703 else ( print_options "GP Register view" gpr_map_options 704 ; print_options "FP register view" fpr_map_options 705 ; print_options "Memory view" mem_options 706 ; print_options "Temproal triple" temporal_options 707 ; raise ERR "process_options" 708 ("Unrecognized option" ^ 709 (if List.length l > 1 then "s" else "") ^ 710 ": " ^ String.concat (commafy l)) 711 ) 712 end 713end 714 715local 716 val initial_config = "vfp" 717 fun thm_eq thm1 thm2 = Term.aconv (Thm.concl thm1) (Thm.concl thm2) 718 val mk_thm_set = Lib.op_mk_set thm_eq 719 val component_11 = 720 case Drule.CONJUNCTS arm_progTheory.arm_component_11 of 721 [r, m, _, fp] => [r, m, fp] 722 | _ => raise ERR "component_11" "" 723 val sym_R_x_pc = 724 REWRITE_RULE [utilsLib.qm [] ``(a = RName_PC) = (RName_PC = a)``] 725 arm_stepTheory.R_x_pc 726 val EXTRA_TAC = 727 RULE_ASSUM_TAC (REWRITE_RULE [sym_R_x_pc, arm_stepTheory.R_x_pc]) 728 THEN ASM_REWRITE_TAC [boolTheory.DE_MORGAN_THM] 729 fun f l = tl (utilsLib.datatype_rewrites true "arm" l) 730 val arm_rwts = f ["arm_state", "PSR", "FP"] 731 val arm_rwts2 = f ["FPSCR"] 732 val STATE_TAC = ASM_REWRITE_TAC arm_rwts THEN ASM_REWRITE_TAC arm_rwts2 733 val basic_spec = 734 stateLib.spec 735 arm_progTheory.ARM_IMP_SPEC arm_progTheory.ARM_IMP_TEMPORAL 736 [arm_stepTheory.get_bytes] 737 [] 738 (arm_select_state_pool_thm :: arm_select_state_thms) 739 [arm_frame, arm_frame_hidden, state_id, fp_id] 740 component_11 741 [word, word5, ``:RName``] 742 EXTRA_TAC STATE_TAC 743 fun is_stm_wb s = 744 let 745 val s' = 746 utilsLib.lowercase (fst (utilsLib.splitAtChar (Lib.equal #";") s)) 747 in 748 String.isPrefix "stm" s' andalso String.isSuffix "(wb)" s' andalso 749 List.exists 750 (fn p => String.isPrefix p (String.extract (s', 3, NONE))) 751 ["ia", "ib", "da", "db"] 752 end 753 val get_opcode = 754 fst o bitstringSyntax.dest_v2w o 755 snd o pairSyntax.dest_pair o 756 List.last o pred_setSyntax.strip_set o 757 temporal_stateSyntax.dest_code' o 758 Thm.concl 759 val (reset_db, set_current_opt, get_current_opt, add1_pending, find_spec, 760 list_db) = 761 spec_databaseLib.mk_spec_database basic_opt default_opt proj_opt 762 closeness convert_opt_rule get_opcode (arm_intro o basic_spec) 763 val current_config = ref (arm_configLib.mk_config_terms initial_config) 764 val newline = ref "\n" 765 val the_step = ref (arm_stepLib.arm_step initial_config) 766 val spec_label_set = ref (Redblackset.empty String.compare) 767 fun reset_specs () = 768 (reset_db (); spec_label_set := Redblackset.empty String.compare) 769 val rev_endian = ref (Lib.I : term list -> term list) 770 val is_be_tm = Term.aconv ``s.CPSR.E`` 771 fun set_endian () = 772 if List.exists is_be_tm (!current_config) 773 then rev_endian := utilsLib.rev_endian 774 else rev_endian := Lib.I 775 fun configure config options = 776 let 777 val opt = process_rule_options options 778 val cfg = arm_configLib.mk_config_terms config 779 in 780 if !current_config = cfg andalso 781 #temporal (get_current_opt ()) = #temporal opt 782 then () 783 else ( reset_specs () 784 ; the_step := arm_stepLib.arm_step config 785 ) 786 ; stateLib.set_temporal (#temporal opt) 787 ; current_config := cfg 788 ; set_endian () 789 ; set_current_opt opt 790 end 791 fun arm_spec_opt config opt = 792 let 793 val () = configure config opt 794 val step = !the_step 795 in 796 fn s => 797 if is_stm_wb s 798 then let 799 val l = step s 800 val l = stm_wb_thms (get_stm_base s) (hd l) @ tl l 801 val thms_ts = List.map (fn t => (t, arm_mk_pre_post t)) l 802 in 803 List.app (fn x => (print "."; add1_pending x)) thms_ts 804 ; thms_ts 805 end 806 else let 807 val thms = step s 808 val ts = List.map arm_mk_pre_post thms 809 val thms_ts = (thms, ts) |> ListPair.zip 810 |> List.map combinations 811 |> List.concat 812 in 813 List.app (fn x => (print "."; add1_pending x)) thms_ts 814 ; thms_ts 815 end 816 end 817 val the_spec = ref (arm_spec_opt initial_config "") 818 fun spec_spec opc thm = 819 let 820 val thm_opc = get_opcode thm 821 val a = fst (Term.match_term thm_opc opc) 822 in 823 simp_triple_rule (Thm.INST a thm) 824 end 825in 826 val list_db = list_db 827 fun set_newline s = newline := s 828 fun arm_config config opt = the_spec := arm_spec_opt config opt 829 fun arm_spec s = 830 List.map (fn t => (print "+"; basic_spec t)) ((!the_spec) s) before 831 print (!newline) 832 fun addInstructionClass s = 833 ( print (" " ^ s) 834 ; if Redblackset.member (!spec_label_set, s) 835 then () 836 else ( (!the_spec) s 837 ; spec_label_set := Redblackset.add (!spec_label_set, s) 838 ) 839 ) 840 fun arm_spec_hex looped s = 841 let 842 val i = arm_stepLib.hex_to_bits_32 s 843 val opc = listSyntax.mk_list (!rev_endian i, Type.bool) 844 in 845 case find_spec opc of 846 SOME (new, thms) => 847 let 848 val l = List.mapPartial (Lib.total (spec_spec opc)) thms 849 in 850 if List.null l 851 then loop looped i "failed to find suitable spec" s 852 else (if new then print (!newline) else (); mk_thm_set l) 853 end 854 | NONE => loop looped i "failed to add suitable spec" s 855 end 856 and loop looped i e s = 857 if looped 858 then raise ERR "arm_spec_hex" (e ^ ": " ^ s) 859 else ( List.app addInstructionClass (arm_stepLib.arm_instruction i) 860 ; arm_spec_hex true s) 861 val arm_spec_hex = arm_spec_hex false 862 val arm_spec_code = 863 List.map arm_spec_hex o 864 (armAssemblerLib.arm_code: string quotation -> string list) 865end 866 867(* ------------------------------------------------------------------------ *) 868 869(* Testing... 870 871val () = arm_config "vfp" "flat" 872val () = arm_config "vfp" "array" 873val () = arm_config "vfp" "mapped" 874val () = arm_config "vfp" "mapped32" 875 876val () = arm_config "vfp" "map-fpr,flat" 877val () = arm_config "vfp" "map-fpr,array" 878val () = arm_config "vfp" "map-fpr,mapped" 879val () = arm_config "vfp" "map-fpr,mapped32" 880 881val () = arm_config "vfp" "map-reg,flat" 882val () = arm_config "vfp" "map-reg,array" 883val () = arm_config "vfp" "map-reg,mapped" 884val () = arm_config "vfp" "map-reg,mapped32" 885 886val () = arm_config "vfp,be" "flat" 887val () = arm_config "vfp,be" "array" 888val () = arm_config "vfp,be" "mapped" 889val () = arm_config "vfp,be" "mapped32" 890 891val () = arm_config "vfp,be" "map-reg,flat" 892val () = arm_config "vfp,be" "map-reg,array" 893val () = arm_config "vfp,be" "map-reg,mapped" 894val () = arm_config "vfp,be" "map-reg,mapped32" 895 896val () = arm_config "vfp" "flat,temporal" 897val () = arm_config "vfp" "array,temporal" 898val () = arm_config "vfp" "mapped,temporal" 899val () = arm_config "vfp" "mapped32,temporal" 900 901val () = arm_config "vfp" "map-reg,flat,temporal" 902val () = arm_config "vfp" "map-reg,array,temporal" 903val () = arm_config "vfp" "map-reg,mapped,temporal" 904val () = arm_config "vfp" "map-reg,mapped32,temporal" 905 906val () = arm_config "vfp,be" "flat,temporal" 907val () = arm_config "vfp,be" "array,temporal" 908val () = arm_config "vfp,be" "mapped,temporal" 909val () = arm_config "vfp,be" "mapped32,temporal" 910 911val () = arm_config "vfp,be" "map-reg,flat,temporal" 912val () = arm_config "vfp,be" "map-reg,array,temporal" 913val () = arm_config "vfp,be" "map-reg,mapped,temporal" 914val () = arm_config "vfp,be" "map-reg,mapped32,temporal" 915 916val thm = arm_intro (last (arm_spec "STMIA;3,2,1")) 917 arm_spec_hex "E881000E"; (* STMIA;3,2,1 *) 918 arm_spec_hex "E891000E"; (* LDMIA;3,2,1 *) 919 920val arm_spec = Count.apply arm_spec 921val arm_spec_hex = Count.apply arm_spec_hex 922val arm_spec_code = Count.apply arm_spec_code 923 924set_trace "stateLib.spec" 1 925 926 arm_spec_code `mrs r1, cpsr` 927 arm_spec_code `msr cpsr, r1` (* forces user mode *) 928 arm_spec_code `msr cpsr_f, r1` 929 arm_spec_code `msr cpsr_x, #0x0000ff00` 930 arm_spec_code `msr cpsr_s, #0x00ff0000` 931 arm_spec_code `msr cpsr_f, #0xf0000000` 932 933 (* The following RFE instructions change the operating mode. 934 As such, arm_CONFIG is not automatically introduced in the post-condition. 935 This is achieved with some post-processing. 936 *) 937 938 val f = List.map (List.map change_config_rule) 939 940 (f o arm_spec_code) `rfeia r1!` 941 (f o arm_spec_code) `rfeia r1` 942 943 (* 944 945 val thm = arm_spec_code `rfeia r1` |> hd |> hd 946 947 *) 948 949 arm_spec_hex "E79F2003" (* ldr r2, [pc, r3] *) 950 arm_spec_hex "E18F20D4" (* ldrd r2, r3, [pc, r4] *) 951 arm_spec_hex "E51F2018" (* ldr r2, [pc, #-24] *) 952 arm_spec_hex "E14F21D8" (* ldrd r2, r3, [pc, #-24] *) 953 954 arm_spec_hex "E59F100C" 955 Count.apply arm_spec_hex "E1CF00DC" 956 957 arm_spec "VLDR (single,+imm,pc)" 958 arm_spec "VLDR (double,+imm,pc)" 959 arm_spec "VLDR (single,-imm,pc)" 960 arm_spec "VLDR (double,-imm,pc)" 961 arm_spec "LDR (+lit)" 962 arm_spec "LDR (-lit)" 963 arm_spec "LDR (+reg,pre,pc)" 964 arm_spec "LDR (-reg,pre,pc)" 965 arm_spec "LDRD (+lit)" 966 arm_spec "LDRD (-lit)" 967 arm_spec "LDRD (+reg,pre,pc)" 968 arm_spec "LDRD (-reg,pre,pc)" 969 970 arm_spec "VMOV (single,reg)"; 971 arm_spec "VMOV (double,reg)"; 972 arm_spec "VMOV (single,imm)"; 973 arm_spec "VMOV (double,imm)"; 974 arm_spec "VMOV (single from arm)"; 975 arm_spec "VMOV (single to arm)"; 976 arm_spec "VMOV (double from arm)"; 977 arm_spec "VMOV (double to arm)"; 978 arm_spec "VMRS (nzcv)"; 979 arm_spec "VMRS"; 980 arm_spec "VMSR"; 981 arm_spec "VCMP (single,zero)"; 982 arm_spec "VCMP (double,zero)"; 983 arm_spec "VCMP (single)"; 984 arm_spec "VCMP (double)"; 985 986 arm_spec "VCVT (single,double)"; 987 arm_spec "VCVT (double,single,lo)"; 988 arm_spec "VCVT (double,single,hi)"; 989 arm_spec "VCVT (single,int)"; 990 arm_spec "VCVT (double,int,lo)"; 991 arm_spec "VCVT (double,int,hi)"; 992 (* not yet supported 993 arm_spec "VCVT (int,single)"; 994 arm_spec "VCVT (int,double)"; 995 *) 996 997 arm_spec "VADD (single)"; 998 arm_spec "VSUB (single)"; 999 arm_spec "VMUL (single)"; 1000 arm_spec "VMLA (single)"; 1001 arm_spec "VMLS (single)"; 1002 arm_spec "VNMUL (single)"; 1003 arm_spec "VNMLA (single)"; 1004 arm_spec "VNMLS (single)"; 1005 arm_spec "VLDR (single,+imm)"; 1006 arm_spec "VLDR (single,-imm)"; 1007 arm_spec "VLDR (single,+imm,pc)"; 1008 arm_spec "VLDR (single,-imm,pc)"; 1009 arm_spec "VSTR (single,+imm)"; 1010 arm_spec "VSTR (single,-imm)"; 1011 arm_spec "VSTR (single,+imm,pc)"; 1012 arm_spec "VSTR (single,-imm,pc)" 1013 1014 arm_spec "VABS (double)"; 1015 arm_spec "VNEG (double)"; 1016 arm_spec "VSQRT (double)"; 1017 arm_spec "VADD (double)"; 1018 arm_spec "VSUB (double)"; 1019 arm_spec "VMUL (double)"; 1020 arm_spec "VMLA (double)"; 1021 arm_spec "VMLS (double)"; 1022 arm_spec "VNMUL (double)"; 1023 arm_spec "VNMLA (double)"; 1024 arm_spec "VNMLS (double)"; 1025 arm_spec "VLDR (double,+imm)"; 1026 arm_spec "VLDR (double,-imm)"; 1027 arm_spec "VLDR (double,+imm,pc)"; 1028 arm_spec "VLDR (double,-imm,pc)"; 1029 arm_spec "VSTR (double,+imm)"; 1030 arm_spec "VSTR (double,-imm)"; 1031 arm_spec "VSTR (double,+imm,pc)"; 1032 arm_spec "VSTR (double,-imm,pc)" 1033 1034 arm_spec_hex "ed907a00"; (* vldr *) 1035 arm_spec_hex "edd16a00"; (* vldr *) 1036 arm_spec_hex "ee676a26"; (* vmul *) 1037 arm_spec_hex "edd15a00"; (* vldr *) 1038 arm_spec_hex "ed936a00"; (* vldr *) 1039 arm_spec_hex "ed925a00"; (* vldr *) 1040 arm_spec_hex "edd17a01"; (* vldr *) 1041 arm_spec_hex "ed817a00"; (* vstr *) 1042 arm_spec_hex "ee775a65"; (* vsub *) 1043 arm_spec_hex "ee477a05"; (* vmla *) 1044 arm_spec_hex "ee456a86"; (* vmla *) 1045 arm_spec_hex "edc17a01"; (* vstr *) 1046 arm_spec_hex "ee767aa7"; (* vadd *) 1047 arm_spec_hex "edc37a00"; (* vstr *) 1048 1049 arm_spec_hex "F1010200"; (* SETEND *) 1050 arm_spec_hex "EA000001"; (* B + *) 1051 arm_spec_hex "EAFFFFFB"; (* B - *) 1052 arm_spec_hex "EB000001"; (* BL + *) 1053 arm_spec_hex "EBFFFFFB"; (* BL - *) 1054 arm_spec_hex "E12FFF11"; (* BX *) 1055 arm_spec_hex "E12FFF1F"; (* BX pc *) 1056 arm_spec_hex "FA000001"; (* BLX + *) 1057 arm_spec_hex "FAFFFFFB"; (* BLX - *) 1058 arm_spec_hex "E12FFF31"; (* BLX *) 1059 (* arm_spec_hex "E12FFF3F"; (* BLX pc - not supported *) *) 1060 arm_spec_hex "E1A01001"; (* MOV *) 1061 arm_spec_hex "E1B01001"; (* MOVS *) 1062 arm_spec_hex "E1A01002"; (* MOV *) 1063 arm_spec_hex "E1A0100F"; (* MOV *) 1064 (* arm_spec_hex "E1A0F001"; (* MOV pc, r1 - not supported *) *) 1065 (* arm_spec_hex "E3A0F00C"; (* MOV pc, #12 - not supported *) *) 1066 arm_spec_hex "E3A0100C"; (* MOV r1, #12 *) 1067 arm_spec_hex "E3E0100C"; (* MOV r1, #-12 - needs SUB CONV? *) 1068 arm_spec_hex "E1110001"; (* TST *) 1069 arm_spec_hex "E1110002"; (* TST *) 1070 arm_spec_hex "E11F0001"; (* TST *) 1071 arm_spec_hex "E111000F"; (* TST *) 1072 arm_spec_hex "E1110001"; (* TST *) 1073 arm_spec_hex "E31100FF"; (* TST *) 1074 arm_spec_hex "E3110000"; (* TST *) 1075 arm_spec_hex "E0421002"; (* SUB *) 1076 arm_spec_hex "E0521002"; (* SUBS *) 1077 arm_spec_hex "E052100F"; (* SUBS *) 1078 arm_spec_hex "E0922212"; (* ADDS *) 1079 arm_spec_hex "E0922102"; (* ADDS *) 1080 arm_spec_hex "E0921453"; (* ADDS *) 1081 (* arm_spec_hex "E09F1453"; (* ADDS -- fail unpredictable *) *) 1082 arm_spec_hex "E0A21453"; (* ADC *) 1083 arm_spec_hex "E0B21453"; (* ADCS *) 1084 arm_spec_hex "E1B011C2"; (* ASRS *) 1085 arm_spec_hex "E0214392"; (* MLA *) 1086 arm_spec_hex "E0314392"; (* MLAS *) 1087 1088 arm_spec_hex "E5921003"; (* LDR pre *) 1089 arm_spec_hex "E5121003"; (* LDR pre *) 1090 arm_spec_hex "E5321080"; (* LDR pre wb *) 1091 arm_spec_hex "E5961080"; (* LDR pre *) 1092 arm_spec_hex "E7911001"; (* LDR pre *) 1093 arm_spec_hex "E59F1000"; (* LDR pc base *) 1094 arm_spec_hex "E79F1001"; (* LDR pre pc base *) 1095 arm_spec_hex "E7921063"; (* LDR pre reg rrx *) 1096 arm_spec_hex "E4921004"; (* LDR post imm *) 1097 arm_spec_hex "E4121004"; (* LDR post -imm *) 1098 arm_spec_hex "E6921002"; (* LDR post reg *) 1099 arm_spec_hex "E6121002"; (* LDR post -reg *) 1100 arm_spec_hex "E6121003"; (* LDR post -reg *) 1101 arm_spec_hex "E6921103"; (* LDR post reg *) 1102 1103 arm_spec_hex "E59F1020"; (* LDR (+lit) *) 1104 arm_spec_hex "E51F1020"; (* LDR (-lit) *) 1105 arm_spec_hex "E1CF02D0"; (* LDRD (+lit) *) 1106 arm_spec_hex "E14F02D0"; (* LDRD (-lit) *) 1107 1108 arm_spec_hex "E5D21004"; (* LDRB pre *) 1109 arm_spec_hex "E7D21102"; (* LDRB reg pre *) 1110 arm_spec_hex "E6D21102"; (* LDRB reg post *) 1111 arm_spec_hex "E19110D2"; (* LDRSB reg pre *) 1112 arm_spec_hex "E19110B2"; (* LDRH reg pre *) 1113 arm_spec_hex "E09210F3"; (* LDRSH reg post *) 1114 arm_spec_hex "E09210F2"; (* LDRSH reg post *) 1115 1116 arm_spec_hex "E1C200D4"; (* LDRD pre *) 1117 arm_spec_hex "E14200D4"; (* LDRD pre *) 1118 arm_spec_hex "E1E200D4"; (* LDRD pre wb *) 1119 arm_spec_hex "E0C200D4"; (* LDRD post *) 1120 arm_spec_hex "E04200D4"; (* LDRD post *) 1121 arm_spec_hex "E08200D3"; (* LDRD post reg *) 1122 arm_spec_hex "E00200D3"; (* LDRD post reg *) 1123 1124 arm_spec_hex "E5821003"; (* STR pre *) 1125 arm_spec_hex "E5021003"; (* STR pre *) 1126 arm_spec_hex "E5221080"; (* STR pre wb *) 1127 arm_spec_hex "E5861080"; (* STR pre *) 1128 arm_spec_hex "E7811001"; (* STR pre *) 1129 arm_spec_hex "E58F1000"; (* STR pc base ** NOT WORKING *) 1130 arm_spec_hex "E78F1001"; (* STR pre pc base *) 1131 arm_spec_hex "E7821063"; (* STR pre reg rrx *) 1132 arm_spec_hex "E4821004"; (* STR post imm *) 1133 arm_spec_hex "E4021004"; (* STR post -imm *) 1134 arm_spec_hex "E6821002"; (* STR post reg *) 1135 arm_spec_hex "E6021002"; (* STR post -reg *) 1136 arm_spec_hex "E6021003"; (* STR post -reg *) 1137 arm_spec_hex "E6821103"; (* STR post reg *) 1138 1139 arm_spec_hex "E5C21004"; (* STRB pre *) 1140 arm_spec_hex "E7C21102"; (* STRB reg pre *) 1141 arm_spec_hex "E6C21102"; (* STRB reg post *) 1142 arm_spec_hex "E18110B2"; (* STRH reg pre *) 1143 1144 arm_spec_hex "E1C200F4"; (* STRD pre *) 1145 arm_spec_hex "E14200F4"; (* STRD pre *) 1146 arm_spec_hex "E1E200F4"; (* STRD pre wb *) 1147 arm_spec_hex "E0C200F4"; (* STRD post *) 1148 arm_spec_hex "E04200F4"; (* STRD post *) 1149 arm_spec_hex "E08200F3"; (* STRD post reg *) 1150 arm_spec_hex "E00200F3"; (* STRD post reg *) 1151 1152 arm_spec_hex "E1031091"; (* SWP *) 1153 arm_spec_hex "E1031092"; (* SWP *) 1154 arm_spec_hex "E1431091"; (* SWPB *) 1155 arm_spec_hex "E1431092"; (* SWPB *) 1156 1157 arm_spec_hex "E891000E"; (* LDMIA;3,2,1 *) 1158 arm_spec_hex "E991000E"; (* LDMIB;3,2,1 *) 1159 arm_spec_hex "E811000E"; (* LDMDA;3,2,1 *) 1160 arm_spec_hex "E911000E"; (* LDMDB;3,2,1 *) 1161 1162 arm_spec_hex "E881000E"; (* STMIA;3,2,1 *) 1163 arm_spec_hex "E981000E"; (* STMIB;3,2,1 *) 1164 arm_spec_hex "E801000E"; (* STMDA;3,2,1 *) 1165 arm_spec_hex "E901000E"; (* STMDB;3,2,1 *) 1166 arm_spec_hex "e88c03ff"; (* STMIA;9,8,7,6,5,4,3,2,1,0 *) 1167 1168 arm_spec_hex "E8B1001C"; (* LDMIA (wb);4,3,2 *) 1169 arm_spec_hex "E8A1001C"; (* STMIA (wb);4,3,2 *) 1170 arm_spec_hex "E8A10082"; (* STMIA (wb);7,1 *) 1171 1172 arm_spec_hex "01A00000"; (* MOVEQ *) 1173 arm_spec_hex "11A00000"; (* MOVNE *) 1174 arm_spec_hex "21A00000"; (* MOVCS *) 1175 arm_spec_hex "31A00000"; (* MOVCC *) 1176 arm_spec_hex "41A00000"; (* MOVMI *) 1177 arm_spec_hex "51A00000"; (* MOVPL *) 1178 arm_spec_hex "61A00000"; (* MOVVS *) 1179 arm_spec_hex "71A00000"; (* MOVVC *) 1180 arm_spec_hex "81A00000"; (* MOVHI *) 1181 arm_spec_hex "91A00000"; (* MOVLS *) 1182 arm_spec_hex "A1A00000"; (* MOVGE *) 1183 arm_spec_hex "B1A00000"; (* MOVLT *) 1184 arm_spec_hex "C1A00000"; (* MOVGT *) 1185 arm_spec_hex "D1A00000"; (* MOVLE *) 1186 1187List.length hex_list 1188val () = Count.apply (List.app (General.ignore o arm_spec_hex)) hex_list 1189 1190val () = 1191 Count.apply (List.app 1192 (fn s => 1193 let 1194 val thm = Count.apply arm_spec_hex s 1195 val () = print (s ^ ":\n") 1196 in 1197 print_thm thm; print "\n\n" 1198 end)) 1199 hex_list 1200 1201fun exclude s = List.exists (fn e => String.isPrefix e s) ["LDM", "STM"] 1202 1203val l = List.filter (not o exclude) (arm_stepLib.list_instructions ()) 1204 1205val pos = ref 0; 1206 1207val () = List.app (fn s => (addInstructionClass s; Portable.inc pos)) 1208 (List.drop (l, !pos)) 1209 1210val () = 1211 List.app (fn s => (addInstructionClass s 1212 handle HOL_ERR _ => (fails := s::(!fails)))) l 1213 1214use "arm_tests.sml"; 1215val l = Lib.mk_set arm_tests 1216length arm_tests 1217length l 1218 1219val fails = ref ([]:string list) 1220val pos = ref 0; 1221 1222val () = 1223 (Count.apply 1224 (List.app (fn s => (arm_spec_hex s 1225 handle HOL_ERR _ => (fails := s::(!fails); [TRUTH]) 1226 ; Portable.inc pos))) 1227 (List.drop (l, !pos)) 1228 ; print "Done\n") 1229 1230fails 1231pos 1232List.length (!fails) 1233 1234val stp = arm_stepLib.arm_step_hex "" 1235val dec = arm_stepLib.arm_decode_hex "" 1236val fs = List.map (fn s => (s, Lib.total dec s)) (!fails) 1237 1238val s = List.nth (l, !pos) 1239val thm = step (List.nth (l, !pos)) 1240val thm = Count.apply arm_spec (List.nth (l, !pos)) 1241 1242(* --- *) 1243 1244val imp_spec = ARM_IMP_SPEC 1245val read_thms = [arm_stepTheory.get_bytes] 1246val write_thms = []: thm list 1247val select_state_thms = (arm_select_state_pool_thm :: arm_select_state_thms) 1248val frame_thms = [arm_frame, arm_frame_hidden, state_id, fp_id] 1249val map_tys = [word, word5, ``:RName``] 1250val mk_pre_post = arm_mk_pre_post 1251val write = arm_write_footprint 1252 1253val model_def = arm_progTheory.ARM_MODEL_def 1254val comp_defs = arm_comp_defs 1255val cpool = mk_arm_code_pool 1256val extras = []: footprint_extra list 1257val write_fn = arm_write_footprint 1258 1259*) 1260 1261(* ------------------------------------------------------------------------ *) 1262 1263end 1264