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