1structure x64_progLib :> x64_progLib = 2struct 3 4open HolKernel boolLib bossLib 5open stateLib x64_stepLib x64_progTheory 6 7structure Parse = 8struct 9 open Parse 10 val (Type, Term) = parse_from_grammars x64_progTheory.x64_prog_grammars 11end 12 13open Parse 14 15val ERR = Feedback.mk_HOL_ERR "x64_progLib" 16 17(* ------------------------------------------------------------------------ *) 18 19val x64_proj_def = x64_progTheory.x64_proj_def 20val x64_comp_defs = x64_progTheory.component_defs 21 22fun syn n d m = HolKernel.syntax_fns {n = n, dest = d, make = m} "x64_prog" 23val x64_1 = syn 2 HolKernel.dest_monop HolKernel.mk_monop 24val x64_2 = syn 3 HolKernel.dest_binop HolKernel.mk_binop 25val byte = wordsSyntax.mk_int_word_type 8 26val word = wordsSyntax.mk_int_word_type 16 27val dword = wordsSyntax.mk_int_word_type 32 28val qword = wordsSyntax.mk_int_word_type 64 29val (_, mk_x64_RIP, _, _) = x64_1 "x64_RIP" 30val (_, mk_x64_EFLAGS, dest_x64_EFLAGS, _) = x64_2 "x64_EFLAGS" 31val (_, mk_x64_MEM, dest_x64_MEM, _) = x64_2 "x64_MEM" 32val (_, mk_x64_REG, dest_x64_REG, _) = x64_2 "x64_REG" 33val (_, mk_x64_XMM_REG, dest_x64_XMM_REG, _) = x64_2 "x64_XMM_REG" 34val (_, mk_x64_MXCSR, dest_x64_MXCSR, _) = x64_1 "x64_MXCSR" 35val (_, mk_x64_mem16, dest_x64_mem16, _) = x64_2 "x64_mem16" 36val (_, mk_x64_mem32, dest_x64_mem32, _) = x64_2 "x64_mem32" 37val (_, mk_x64_mem64, dest_x64_mem64, _) = x64_2 "x64_mem64" 38val (_, mk_x64_mem128, dest_x64_mem128, _) = x64_2 "x64_mem128" 39 40(* -- *) 41 42val x64_select_state_thms = 43 List.map (fn t => star_select_state_thm x64_proj_def [] ([], t)) 44 (x64_comp_defs @ 45 [x64_mem16_def, x64_mem32_def, x64_mem64_def, x64_mem128_def]) 46 47local 48 val opcs = 49 List.tabulate (20, fn i => Term.mk_var ("opc" ^ Int.toString i, byte)) 50 val cnv = 51 utilsLib.SRW_CONV 52 [pred_setTheory.INSERT_UNION_EQ, stateTheory.CODE_POOL, 53 x64_instr_def, x64_mem_def] 54 fun x64_pool i = 55 cnv (stateLib.list_mk_code_pool 56 (``x64_instr``, ``v: word64``, List.take (opcs, i))) 57 val select_state_pool_thm = 58 stateLib.pool_select_state_thm x64_proj_def [] o 59 x64_pool o (fn i => i + 1) 60in 61 val x64_select_state_pool_thms = List.tabulate (20, select_state_pool_thm) 62end 63 64(* -- *) 65 66val state_id = 67 utilsLib.mk_state_id_thm x64Theory.x64_state_component_equality 68 [["EFLAGS", "REG", "RIP"], 69 ["EFLAGS", "MEM", "RIP"], 70 ["EFLAGS", "RIP"], 71 ["MEM", "REG", "RIP"], 72 ["MEM", "RIP"], 73 ["REG", "RIP"], 74 ["XMM_REG"] 75 ] 76 77val x64_frame = 78 stateLib.update_frame_state_thm x64_proj_def 79 ["RIP", "REG", "MEM", "EFLAGS", "MXCSR", "XMM_REG"] 80 81(* -- *) 82 83local 84 fun is_imm_var tm = 85 case Lib.total Term.dest_var tm of 86 SOME ("imm", _) => true 87 | _ => false 88 fun is_opc_byte tm = 89 case Lib.total wordsSyntax.dest_word_extract tm of 90 SOME (_, _, i, _) => is_imm_var i 91 | NONE => (case Lib.total combinSyntax.dest_I tm of 92 SOME i => is_imm_var i 93 | NONE => wordsSyntax.is_n2w tm) 94 fun is_mem_access v tm = 95 case Lib.total boolSyntax.dest_eq tm of 96 SOME (l, r) => 97 stateLib.is_code_access ("x64$x64_state_MEM", v) l andalso 98 is_opc_byte r 99 | NONE => false 100in 101 fun mk_x64_code_pool thm = 102 let 103 val rip = stateLib.gvar "rip" (wordsSyntax.mk_int_word_type 64) 104 val rip_a = mk_x64_RIP rip 105 val (a, tm) = Thm.dest_thm thm 106 val rip_subst = Term.subst [``s.RIP`` |-> rip] 107 val a = List.map rip_subst a 108 val (m, a) = List.partition (is_mem_access rip) a 109 val m = List.map dest_code_access m 110 val m = mlibUseful.sort_map fst Int.compare m 111 in 112 (rip_a, 113 boolSyntax.rand 114 (stateLib.list_mk_code_pool (``x64_instr``, rip, List.map snd m)), 115 list_mk_imp (a, rip_subst tm)) 116 end 117end 118 119(* -- *) 120 121local 122 fun prefix tm = case boolSyntax.strip_comb tm of 123 (a, [_]) => a 124 | (a, [b, _]) => Term.mk_comb (a, b) 125 | _ => raise ERR "prefix" "" 126in 127 val psort = mlibUseful.sort_map prefix Term.compare 128end 129 130local 131 val st = Term.mk_var ("s", ``:x64_state``) 132 val MEM_tm = ``^st.MEM`` 133 fun err () = raise ERR "x64_write_footprint" "mem" 134in 135 val x64_write_footprint = 136 stateLib.write_footprint x64_1 x64_2 137 [("x64$x64_state_REG_fupd", "x64_REG", ``^st.REG``), 138 ("x64$x64_state_XMM_REG_fupd", "x64_XMM_REG", ``^st.XMM_REG``), 139 ("x64$x64_state_EFLAGS_fupd", "x64_EFLAGS", ``^st.EFLAGS``)] 140 [] 141 [("x64$x64_state_RIP_fupd", "x64_RIP"), 142 ("x64$x64_state_MXCSR_fupd", "x64_MXCSR")] 143 [("x64$x64_state_MEM_fupd", 144 fn (p, q, m) => 145 let 146 val l = 147 case combinSyntax.strip_update m of 148 ([], t) => 149 (case boolSyntax.dest_strip_comb t of 150 ("x64_step$write_mem16", [_, a, d]) => 151 [mk_x64_mem16 (a, d)] 152 | ("x64_step$write_mem32", [_, a, d]) => 153 [mk_x64_mem32 (a, d)] 154 | ("x64_step$write_mem64", [_, a, d]) => 155 [mk_x64_mem64 (a, d)] 156 | ("x64_step$write_mem128", [_, a, d]) => 157 [mk_x64_mem128 (a, d)] 158 | _ => err () 159 ) 160 | (l, t) => (t ~~ MEM_tm orelse err () 161 ; List.map mk_x64_MEM l) 162 in 163 (p, l @ q) 164 end)] 165 (K false) 166end 167 168val x64_extras = 169 [((``x64_mem16 v``, ``read_mem16 s.MEM v``), I, I), 170 ((``x64_mem32 v``, ``read_mem32 s.MEM v``), I, I), 171 ((``x64_mem64 v``, ``read_mem64 s.MEM v``), I, I), 172 ((``x64_mem128 v``, ``read_mem128 s.MEM v``), I, I) 173 ] : footprint_extra list 174 175val x64_mk_pre_post = 176 stateLib.mk_pre_post x64_progTheory.X64_MODEL_def x64_comp_defs 177 mk_x64_code_pool x64_extras x64_write_footprint psort 178 179(* ------------------------------------------------------------------------ *) 180 181local 182 val lowercase_const = utilsLib.lowercase o fst o Term.dest_const o List.hd 183 val xmm = 184 Lib.curry (op ^) "xmm" o Int.toString o wordsSyntax.uint_of_word o List.hd 185 val x64_rmap = 186 fn "x64_prog$x64_REG" => SOME lowercase_const 187 | "x64_prog$x64_EFLAGS" => SOME lowercase_const 188 | "x64_prog$x64_MXCSR" => SOME (K "mxcsr") 189 | "x64_prog$x64_XMM_REG" => SOME xmm 190 | _ => NONE 191 val x64_rename = stateLib.rename_vars (x64_rmap, []) 192 val byte_mem_intro = 193 stateLib.introduce_map_definition 194 (x64_progTheory.x64_BYTE_MEMORY_INSERT, Conv.ALL_CONV) 195 val mem_intro = 196 Conv.BETA_RULE o 197 stateLib.introduce_map_definition 198 (x64_progTheory.x64_MEMORY_INSERT, Conv.ALL_CONV) 199 val match_mem32 = fst o match_term ``pp * x64_prog$x64_mem32 a w`` 200 val w = ``w:word32`` 201 val w2w_w = ``(w2w: word64 -> word32) w`` 202 fun try_to_remove_mem32 th = 203 let 204 val i = match_mem32 (temporal_stateSyntax.dest_pre' (Thm.concl th)) 205 val th = INST [subst i w |-> w2w_w] th 206 in 207 Lib.tryfind (fn thm => MATCH_MP thm th) 208 [x64_mem32_READ_EXTEND, x64_mem32_WRITE_EXTEND, 209 x64_mem32_TEMPORAL_READ_EXTEND, x64_mem32_TEMPORAL_WRITE_EXTEND] 210 end 211 handle HOL_ERR _ => th 212in 213 val x64_rule = 214 x64_rename o 215 byte_mem_intro o 216 mem_intro o 217 try_to_remove_mem32 o 218 helperLib.PRE_POST_RULE 219 (wordsLib.WORD_SUB_CONV 220 THENC helperLib.EVERY_MATCH_MOVE_OUT_CONV ``x64_prog$x64_mem32 a b``) o 221 Conv.CONV_RULE 222 (helperLib.POST_CONV (stateLib.PC_CONV "x64_prog$x64_PC")) o 223 stateLib.introduce_triple_definition (false, x64_PC_def) 224end 225 226(* ------------------------------------------------------------------------ *) 227 228local 229 val component_11 = Drule.CONJUNCTS x64_progTheory.x64_component_11 230 val x64_rwts = 231 Thm.INST_TYPE [Type.alpha |-> ``:Zreg``] boolTheory.COND_RATOR :: 232 List.drop (utilsLib.datatype_rewrites true "x64" ["x64_state"], 1) 233 val STATE_TAC = ASM_REWRITE_TAC x64_rwts 234 val spec = 235 x64_rule o 236 stateLib.spec 237 x64_progTheory.X64_IMP_SPEC 238 x64_progTheory.X64_IMP_TEMPORAL 239 [x64_stepTheory.read_mem16, x64_stepTheory.read_mem32, 240 x64_stepTheory.read_mem64, x64_stepTheory.read_mem128, 241 combinTheory.I_THM] 242 [x64_stepTheory.write_mem16_def, x64_stepTheory.write_mem32_def, 243 x64_stepTheory.write_mem64_def, x64_stepTheory.write_mem128_def] 244 (x64_select_state_thms @ x64_select_state_pool_thms) 245 [x64_frame, state_id] 246 component_11 247 [qword, ``:Zreg``, ``:Zeflags``] 248 NO_TAC STATE_TAC 249 val disassemble1 = x64AssemblerLib.x64_disassemble1 250 val x64_spec_trace = ref 0 251 val () = Feedback.register_trace ("x64 spec", x64_spec_trace, 2) 252in 253 val x64_spec = 254 (* utilsLib.cache 2000 String.compare *) 255 (fn s => 256 let 257 val thm = x64_stepLib.x64_step_hex s 258 val t = x64_mk_pre_post thm 259 in 260 case !x64_spec_trace of 261 1 => assemblerLib.printn (s ^ " ; " ^ disassemble1 s) 262 | 2 => print (" " ^ disassemble1 s) 263 | _ => () 264 ; spec (thm, t) 265 end) 266end 267 268val x64_spec_code = List.map x64_spec o x64AssemblerLib.x64_code_no_spaces 269 270(* ------------------------------------------------------------------------ *) 271 272(* 273 274open x64_progLib 275 276val () = Feedback.set_trace "x64 spec" 1 277 278val thms = x64_spec_code 279 `ret ; c3 280 cmovb r8d, ecx ; 44 0f 42 c1 281 push rdx ; 52 282 mul r8d ; 41 f7 e0 283 cmp r8d, edx ; 41 39 d0 284 mov [rsp+rax], al ; 88 04 04 285 mov [rip+0x4], al ; 88 05 04 00 00 00 286 add r8, 0x30 ; 49 83 c0 30 287 mov dword [rax], 0x504D4F54 ; c7 00 54 4f 4d 50 288 mov r15, [rdi-0xF0] ; 4c 8b bf 10 ff ff ff 289 mov ecx, [rsi+rax*4+0x4] ; 8b 4c 86 04` 290 291x64AssemblerLib.print_x64_code `mov [rsp+rax], ax` 292 293x64AssemblerLib.print_x64_disassemble 294 `48C3 295 440F42C1 296 4852 297 41F7E0 298 4139D0 299 880404 300 880504000000 301 4983C030 302 C700544F4D50 303 4C8BBF10FFFFFF 304 8B4C8604` 305 306val () = stateLib.set_temporal false 307val () = stateLib.set_temporal true 308 309val thm = Count.apply x64_spec "48C3" 310val thm = Count.apply x64_spec "440F42C1" 311val thm = Count.apply x64_spec "4852" 312val thm = Count.apply x64_spec "41F7E0" 313val thm = Count.apply x64_spec "4139D0" 314val thm = Count.apply x64_spec "880404" 315val thm = Count.apply x64_spec "880504000000" 316val thm = Count.apply x64_spec "4983C030" 317val thm = Count.apply x64_spec "C700544F4D50" 318val thm = Count.apply x64_spec "4C8BBF10FFFFFF" 319val thm = Count.apply x64_spec "8B4C8604" 320 321val thm = Count.apply x64_spec "8345F8__" 322val thm = Count.apply x64_spec "41B8________" 323val thm = Count.apply x64_spec "48BA________________" 324 325val pos = ref 1; 326 327val () = List.app (fn s => (Count.apply x64_spec s; Portable.inc pos)) 328 (List.drop (hex_list, !pos)) 329 330val () = 331 Count.apply (List.app (fn s => General.ignore (x64_spec s))) (tl hex_list) 332 333val next_def = x64_stepTheory.NextStateX64_def 334val instr_def = x64_instr_def 335val proj_def = x64_proj_def 336val model_def = x64_progTheory.X64_MODEL_def 337val comp_defs = x64_comp_defs 338val cpool = mk_x64_code_pool 339val extras = x64_extras 340val write_fn = x64_write_footprint 341val q = [] : term list 342 343val imp_spec = X64_IMP_SPEC 344val imp_temp = x64_progTheory.X64_IMP_TEMPORAL 345val read_thms = 346 [x64_stepTheory.read_mem16, x64_stepTheory.read_mem32, 347 x64_stepTheory.read_mem64, x64_stepTheory.read_mem128, combinTheory.I_THM] 348val write_thms = 349 [x64_stepTheory.write_mem16_def, x64_stepTheory.write_mem32_def, 350 x64_stepTheory.write_mem64_def, x64_stepTheory.write_mem128_def] 351val select_state_thms = x64_select_state_thms @ x64_select_state_pool_thms 352val frame_thms = [x64_frame, state_id] 353val map_tys = [qword, ``:Zreg``, ``:Zeflags``] 354val EXTRA_TAC = NO_TAC 355val step = x64_stepLib.x64_step 356val mk_pre_post = x64_mk_pre_post 357 358fun test path = 359 let 360 val istrm = TextIO.openIn path 361 val s = TextIO.inputAll istrm before TextIO.closeIn istrm 362 in 363 s |> String.tokens (Lib.equal #"\n") 364 |> List.mapPartial 365 (fn s => 366 if String.size s = 0 orelse 367 Lib.mem (String.sub (s, 0)) [#".", #"#"] 368 then NONE 369 else SOME (x64_spec_code [QUOTE s]) 370 handle HOL_ERR _ => (print (s ^ "\n"); NONE)) 371 end 372 373*) 374 375(* ------------------------------------------------------------------------ *) 376 377end 378