1(* ------------------------------------------------------------------------ 2 x64 step evaluator 3 ------------------------------------------------------------------------ *) 4 5structure x64_stepLib :> x64_stepLib = 6struct 7 8open HolKernel boolLib bossLib 9open updateLib utilsLib x64Lib x64Theory x64_stepTheory 10 11structure Parse = 12struct 13 open Parse 14 val (Type, Term) = parse_from_grammars x64Theory.x64_grammars 15end 16 17open Parse 18 19val ERR = Feedback.mk_HOL_ERR "x64_stepLib" 20 21val () = show_assums := true 22 23(* ========================================================================= *) 24 25(* 26val print_thms = 27 List.app 28 (fn th => (Lib.with_flag (show_assums, false) print_thm th; print "\n\n")) 29*) 30 31val st = ``s: x64_state`` 32val regs = TypeBase.constructors_of ``:Zreg`` 33fun mapl x = utilsLib.augment x [[]] 34 35local 36 val state_fns = utilsLib.accessor_fns ``: x64_state`` 37 val other_fns = 38 [pairSyntax.fst_tm, pairSyntax.snd_tm, 39 wordsSyntax.w2w_tm, wordsSyntax.sw2sw_tm, 40 ``(h >< l) : 'a word -> 'b word``, 41 ``bit_field_insert h l : 'a word -> 'b word -> 'b word``] @ 42 utilsLib.update_fns ``: x64_state`` @ 43 utilsLib.accessor_fns ``: MXCSR`` @ 44 utilsLib.accessor_fns ``: binary_ieee$flags`` @ 45 utilsLib.update_fns ``: binary_ieee$flags`` 46 val exc = ``SND (raise'exception e s : 'a # x64_state)`` 47in 48 val cond_rand_thms = utilsLib.mk_cond_rand_thms (other_fns @ state_fns) 49 val snd_exception_thms = 50 utilsLib.map_conv 51 (Drule.GEN_ALL o 52 utilsLib.SRW_CONV [cond_rand_thms, x64Theory.raise'exception_def] o 53 (fn tm => Term.mk_comb (tm, exc))) state_fns 54end 55 56(* x64 datatype theorems/conversions *) 57 58local 59 fun datatype_thms thms = 60 thms @ [cond_rand_thms, snd_exception_thms] @ 61 utilsLib.datatype_rewrites true "binary_ieee" ["flags"] @ 62 utilsLib.datatype_rewrites true "x64" 63 ["x64_state", "Zreg", "Zeflags", "Zsize", "Zbase", "Zrm", "Zdest_src", 64 "Zimm_rm", "Zmonop_name", "Zbinop_name", "Zbit_test_name", "Zcond", 65 "Zea", "MXCSR", "xmm_mem", "sse_binop", "sse_logic", "sse_compare", 66 "Zinst"] 67in 68 val DATATYPE_CONV = REWRITE_CONV (datatype_thms []) 69 val COND_UPDATE_CONV = 70 REWRITE_CONV (utilsLib.mk_cond_update_thms [``:x64_state``]) 71 val EV = utilsLib.STEP (datatype_thms, st) 72 val resetEvConv = utilsLib.resetStepConv 73 val setEvConv = utilsLib.setStepConv 74end 75 76(* ------------------------------------------------------------------------ *) 77 78local 79 val cnv = Conv.REWR_CONV x64Theory.readPrefix_def 80 THENC REWRITE_CONV [prefixGroup_def] 81 THENC EVAL 82 THENC REWRITE_CONV [rec'REX_def] 83 THENC EVAL 84 fun mk_ibyte w = wordsSyntax.mk_wordii (w, 8) 85 val prefix_rwt1 = 86 utilsLib.map_conv cnv 87 (List.tabulate (256, fn i => ``readPrefix (s, p, ^(mk_ibyte i)::l)``)) 88 val prefix_rwt2 = 89 x64Theory.readPrefix_def 90 |> Q.SPEC `h::t` 91 |> SIMP_RULE (srw_ss()) [] 92 |> GEN_ALL 93in 94 val prefix_CONV = 95 Conv.CHANGED_CONV (PURE_ONCE_REWRITE_CONV [prefix_rwt1]) 96 ORELSEC (Conv.REWR_CONV prefix_rwt2 97 THENC Conv.RAND_CONV 98 (Conv.REWR_CONV x64_stepTheory.prefixGroup 99 THENC Conv.DEPTH_CONV blastLib.BBLAST_CONV 100 THENC REWRITE_CONV []) 101 THENC numLib.REDUCE_CONV 102 THENC REWRITE_CONV [rec'REX_def] 103 THENC Conv.DEPTH_CONV blastLib.BBLAST_CONV) 104end 105 106local 107 fun mk_3 w = wordsSyntax.mk_wordii (w, 3) 108 val boolify8_CONV = 109 (Conv.REWR_CONV boolify8_n2w THENC numLib.REDUCE_CONV) 110 ORELSEC (Conv.REWR_CONV boolify8_def 111 THENC Conv.DEPTH_CONV blastLib.BBLAST_CONV) 112 fun RexReg_rwt b = 113 utilsLib.map_conv (REWRITE_CONV [RexReg_def] 114 THENC EVAL 115 THENC REWRITE_CONV [num2Zreg_thm]) 116 (List.tabulate (8, fn i => ``RexReg (^b, ^(mk_3 i))``)) 117 val cmp = wordsLib.words_compset () 118 val () = 119 utilsLib.add_theory 120 ([immediate8_rwt, immediate16_rwt, immediate32_rwt, immediate64_rwt, 121 immediate8, immediate16, immediate32, immediate64, immediate_def, 122 OpSize_rwt, rbp, x64Theory.readModRM_def, readModRM_not_4_or_5, 123 readModRM_byte_not_4, readModRM_dword_not_4, 124 RexReg_rwt boolSyntax.F, RexReg_rwt boolSyntax.T], 125 utilsLib.filter_inventory ["readPrefix"] x64Theory.inventory) cmp 126 val () = utilsLib.add_base_datatypes cmp 127 val () = computeLib.add_conv 128 (bitstringSyntax.v2w_tm, 1, bitstringLib.v2w_n2w_CONV) cmp 129 val () = computeLib.add_conv (``boolify8``, 1, boolify8_CONV) cmp 130 val () = computeLib.add_conv (``readPrefix``, 1, prefix_CONV) cmp 131in 132 val x64_CONV = utilsLib.CHANGE_CBV_CONV cmp 133end 134 135val highByte = 136 utilsLib.map_conv x64_CONV 137 (List.map (fn r => ``num2Zreg (Zreg2num ^r - 4)``) 138 [``RSP``, ``RBP``, ``RSI``, ``RDI``]) 139 140local 141 val state_with_pre = (st |-> ``^st with RIP := ^st.RIP + n2w len``) 142 fun ADD_PRECOND_RULE thm = 143 thm |> Thm.INST [state_with_pre] 144 |> utilsLib.ALL_HYP_CONV_RULE DATATYPE_CONV 145 |> Conv.CONV_RULE DATATYPE_CONV 146 val rwts = ref ([]: thm list) 147in 148 fun getThms () = [highByte] @ List.map ADD_PRECOND_RULE (!rwts) 149 fun resetThms () = rwts := [] 150 fun addThms thms = (rwts := thms @ !rwts; thms) 151end 152 153(* ------------------------------------------------------------------------ *) 154 155val mem8_rwt = 156 EV [mem8_def] [[``^st.MEM a = v``]] [] 157 ``mem8 a`` 158 |> hd 159 160val write'mem8_rwt = 161 EV [write'mem8_def] [] [] 162 ``write'mem8 (d, addr)`` 163 |> hd 164 |> Drule.ADD_ASSUM ``^st.MEM addr = wv`` 165 166(* ------------------------------------------------------------------------ *) 167 168val sizes = [``Z8 have_rex``, ``Z16``, ``Z32``, ``Z64``] 169 170val Cflag_rwt = 171 EV [Eflag_def] [[``^st.EFLAGS Z_CF = SOME cflag``]] [] 172 ``Eflag Z_CF`` 173 |> hd 174 175val write'Eflag_rwt = 176 EV [write'Eflag_def] [] [] 177 ``write'Eflag (b, flag)`` 178 |> hd 179 180val FlagUnspecified_rwt = 181 EV [FlagUnspecified_def] [] [] 182 ``FlagUnspecified (flag)`` 183 |> hd 184 185val write_PF_rwt = 186 EV [write_PF_def, write'PF_def, write'Eflag_rwt] [] [] 187 ``write_PF w`` 188 |> hd 189 190val () = setEvConv (Conv.DEPTH_CONV (wordsLib.WORD_BIT_INDEX_CONV true)) 191 192val write_SF_rwt = 193 EV [write_SF_def, write'SF_def, write'Eflag_rwt, word_size_msb_def, 194 Zsize_width_def] [] 195 (mapl (`size`, sizes)) 196 ``write_SF (size, w)`` 197 198val write_ZF_rwt = 199 EV [write_ZF_def, write'ZF_def, write'Eflag_rwt] [] (mapl (`size`, sizes)) 200 ``write_ZF (size, w)`` 201 202val erase_eflags = 203 erase_eflags_def 204 |> Thm.SPEC st 205 |> REWRITE_RULE [ISPEC ``^st.EFLAGS`` eflags_none] 206 207(* ------------------------------------------------------------------------ *) 208 209val mem_addr_rwt = 210 EV [mem_addr_def, ea_index_def, ea_base_def, wordsTheory.WORD_ADD_0] [] 211 [[`m` |-> ``(NONE, ZnoBase, d)``], 212 [`m` |-> ``(NONE, ZripBase, d)``], 213 [`m` |-> ``(NONE, ZregBase r, d)``], 214 [`m` |-> ``(SOME (scale, inx), ZnoBase, d)``], 215 [`m` |-> ``(SOME (scale, inx), ZripBase, d)``], 216 [`m` |-> ``(SOME (scale, inx), ZregBase r, d)``]] 217 ``mem_addr m`` 218 219val ea_Zrm_rwt = 220 EV ([ea_Zrm_def] @ mem_addr_rwt) [] 221 [[`rm` |-> ``Zr r``], 222 [`rm` |-> ``Zm (NONE, ZnoBase, d)``], 223 [`rm` |-> ``Zm (NONE, ZripBase, d)``], 224 [`rm` |-> ``Zm (NONE, ZregBase r, d)``], 225 [`rm` |-> ``Zm (SOME (scale, inx), ZnoBase, d)``], 226 [`rm` |-> ``Zm (SOME (scale, inx), ZripBase, d)``], 227 [`rm` |-> ``Zm (SOME (scale, inx), ZregBase r, d)``]] 228 ``ea_Zrm (size, rm)`` 229 230val ea_Zdest_rwt = 231 EV (ea_Zdest_def :: ea_Zrm_rwt) [] 232 [[`ds` |-> ``Zrm_i (Zr r, x)``], 233 [`ds` |-> ``Zrm_i (Zm (NONE, ZnoBase, d), x)``], 234 [`ds` |-> ``Zrm_i (Zm (NONE, ZripBase, d), x)``], 235 [`ds` |-> ``Zrm_i (Zm (NONE, ZregBase r, d), x)``], 236 [`ds` |-> ``Zrm_i (Zm (SOME (scale, inx), ZnoBase, d), x)``], 237 [`ds` |-> ``Zrm_i (Zm (SOME (scale, inx), ZripBase, d), x)``], 238 [`ds` |-> ``Zrm_i (Zm (SOME (scale, inx), ZregBase r, d), x)``], 239 [`ds` |-> ``Zrm_r (Zr r, x)``], 240 [`ds` |-> ``Zrm_r (Zm (NONE, ZnoBase, d), x)``], 241 [`ds` |-> ``Zrm_r (Zm (NONE, ZripBase, d), x)``], 242 [`ds` |-> ``Zrm_r (Zm (NONE, ZregBase r, d), x)``], 243 [`ds` |-> ``Zrm_r (Zm (SOME (scale, inx), ZnoBase, d), x)``], 244 [`ds` |-> ``Zrm_r (Zm (SOME (scale, inx), ZripBase, d), x)``], 245 [`ds` |-> ``Zrm_r (Zm (SOME (scale, inx), ZregBase r, d), x)``], 246 [`ds` |-> ``Zr_rm (r, x)``]] 247 ``ea_Zdest (size, ds)`` 248 249val ea_Zsrc_rwt = 250 EV (ea_Zsrc_def :: ea_Zrm_rwt) [] 251 [[`ds` |-> ``Zrm_i (x, i)``], 252 [`ds` |-> ``Zrm_r (x, r)``], 253 [`ds` |-> ``Zr_rm (x, Zr r)``], 254 [`ds` |-> ``Zr_rm (x, Zm (NONE, ZnoBase, d))``], 255 [`ds` |-> ``Zr_rm (x, Zm (NONE, ZripBase, d))``], 256 [`ds` |-> ``Zr_rm (x, Zm (NONE, ZregBase r, d))``], 257 [`ds` |-> ``Zr_rm (x, Zm (SOME (scale, inx), ZnoBase, d))``], 258 [`ds` |-> ``Zr_rm (x, Zm (SOME (scale, inx), ZripBase, d))``], 259 [`ds` |-> ``Zr_rm (x, Zm (SOME (scale, inx), ZregBase r, d))``]] 260 ``ea_Zsrc (size, ds)`` 261 262val ea_Zimm_rm_rwt = 263 EV (ea_Zimm_rm_def :: ea_Zrm_rwt) [] 264 [[`irm` |-> ``Zimm (i)``], 265 [`irm` |-> ``Zrm (Zr r)``], 266 [`irm` |-> ``Zrm (Zm (NONE, ZnoBase, d))``], 267 [`irm` |-> ``Zrm (Zm (NONE, ZripBase, d))``], 268 [`irm` |-> ``Zrm (Zm (NONE, ZregBase r, d))``], 269 [`irm` |-> ``Zrm (Zm (SOME (scale, inx), ZnoBase, d))``], 270 [`irm` |-> ``Zrm (Zm (SOME (scale, inx), ZripBase, d))``], 271 [`irm` |-> ``Zrm (Zm (SOME (scale, inx), ZregBase r, d))``]] 272 ``ea_Zimm_rm (irm)`` 273 274(* ------------------------------------------------------------------------ *) 275 276val no_imm_ea = 277 [[`ea` |-> ``Zea_r (Z8 have_rex, r)``], 278 [`ea` |-> ``Zea_r (Z16, r)``], 279 [`ea` |-> ``Zea_r (Z32, r)``], 280 [`ea` |-> ``Zea_r (Z64, r)``], 281 [`ea` |-> ``Zea_m (Z8 have_rex, a)``], 282 [`ea` |-> ``Zea_m (Z16, a)``], 283 [`ea` |-> ``Zea_m (Z32, a)``], 284 [`ea` |-> ``Zea_m (Z64, a)``]] : utilsLib.cover 285 286val ea = 287 [[`ea` |-> ``Zea_i (Z8 have_rex, i)``], 288 [`ea` |-> ``Zea_i (Z16, i)``], 289 [`ea` |-> ``Zea_i (Z32, i)``], 290 [`ea` |-> ``Zea_i (Z64, i)``]] @ no_imm_ea 291 292val () = resetThms() 293 294val EA_rwt = 295 EV [EA_def, restrictSize_def, id_state_cond, pred_setTheory.IN_INSERT, 296 pred_setTheory.NOT_IN_EMPTY, mem8_rwt, mem16_rwt, mem32_rwt, mem64_rwt] 297 [] ea 298 ``EA ea`` 299 300val write'EA_rwt = 301 EV [write'EA_def, bitfield_inserts, 302 pred_setTheory.IN_INSERT, pred_setTheory.NOT_IN_EMPTY, 303 write'mem8_rwt, write'mem16_rwt, write'mem32_rwt, write'mem64_rwt] [] 304 no_imm_ea 305 ``write'EA (d, ea)`` 306 |> List.map (Conv.RIGHT_CONV_RULE 307 (utilsLib.EXTRACT_CONV THENC COND_UPDATE_CONV)) 308 309val wv_to_v = List.map (Q.INST [`wv` |-> `v`]) 310 311val write'EA_rwt_r = wv_to_v write'EA_rwt 312 313val xmm = 314 [[`xmm` |-> ``xmm_reg x``], 315 [`xmm` |-> ``xmm_mem (NONE, ZnoBase, d)``], 316 [`xmm` |-> ``xmm_mem (NONE, ZripBase, d)``], 317 [`xmm` |-> ``xmm_mem (NONE, ZregBase r, d)``], 318 [`xmm` |-> ``xmm_mem (SOME (scale, inx), ZnoBase, d)``], 319 [`xmm` |-> ``xmm_mem (SOME (scale, inx), ZripBase, d)``], 320 [`xmm` |-> ``xmm_mem (SOME (scale, inx), ZregBase r, d)``]] : utilsLib.cover 321 322val XMM_rwt = 323 EV ([XMM_def, mem128_rwt] @ mem_addr_rwt) [] xmm 324 ``XMM xmm`` 325 326val write'XMM_rwt = EV ([write'XMM_def, write'mem128_rwt] @ mem_addr_rwt) [] xmm 327 ``write'XMM (d, xmm)`` 328 329(* ------------------------------------------------------------------------ *) 330 331val write_arith_eflags_except_CF_OF_rwt = 332 EV ([write_arith_eflags_except_CF_OF_def, FlagUnspecified_rwt, 333 write_PF_rwt] @ write_SF_rwt @ write_ZF_rwt) [] (mapl (`size`, sizes)) 334 ``write_arith_eflags_except_CF_OF (size, w)`` 335 336val write_arith_eflags_rwt = 337 EV ([write_arith_eflags_def, write'CF_def, write'OF_def, write'Eflag_rwt] @ 338 write_arith_eflags_except_CF_OF_rwt) [] (mapl (`size`, sizes)) 339 ``write_arith_eflags (size, r, carry, overflow)`` 340 341val write_logical_eflags_rwt = 342 EV ([write_logical_eflags_def, write'CF_def, write'OF_def, write'Eflag_rwt] @ 343 write_arith_eflags_rwt) [] (mapl (`size`, sizes)) 344 ``write_logical_eflags (size, w)`` 345 346val () = setEvConv (Conv.DEPTH_CONV (wordsLib.WORD_BIT_INDEX_CONV true)) 347 348val ea_op = 349 [[`size1` |-> ``Z8 have_rex``, `ea` |-> ``Zea_r (Z8 have_rex, r)``], 350 [`size1` |-> ``Z16``, `ea` |-> ``Zea_r (Z16, r)``], 351 [`size1` |-> ``Z32``, `ea` |-> ``Zea_r (Z32, r)``], 352 [`size1` |-> ``Z64``, `ea` |-> ``Zea_r (Z64, r)``], 353 [`size1` |-> ``Z8 have_rex``, `ea` |-> ``Zea_m (Z8 have_rex, a)``], 354 [`size1` |-> ``Z16``, `ea` |-> ``Zea_m (Z16, a)``], 355 [`size1` |-> ``Z32``, `ea` |-> ``Zea_m (Z32, a)``], 356 [`size1` |-> ``Z64``, `ea` |-> ``Zea_m (Z64, a)``]] : utilsLib.cover 357 358val monops = TypeBase.constructors_of ``:Zmonop_name`` 359val binops = Lib.set_diff (TypeBase.constructors_of ``:Zbinop_name``) 360 [``Zrcl``, ``Zrcr``] 361 362val () = resetEvConv () 363 364val write_binop_rwt = 365 EV ([write_binop_def, write_arith_result_def, write_logical_result_def, 366 write_arith_result_no_CF_OF_def, write_result_erase_eflags_def, 367 write_arith_eflags_except_CF_OF_def, 368 add_with_carry_out_def, sub_with_borrow_def, 369 maskShift_def, ROL_def, ROR_def, SAR_def, value_width_def, 370 Zsize_width_def, word_size_msb_def, 371 word_signed_overflow_add_def, word_signed_overflow_sub_def, 372 erase_eflags, write_PF_rwt, write'CF_def, write'OF_def, 373 write'Eflag_rwt, CF_def, Cflag_rwt, FlagUnspecified_def] @ 374 write_arith_eflags_rwt @ write_logical_eflags_rwt @ write_SF_rwt @ 375 write_ZF_rwt @ write'EA_rwt) [] 376 (utilsLib.augment (`bop`, binops) ea_op) 377 ``write_binop (size1, bop, x, y, ea)`` 378 |> List.map (utilsLib.ALL_HYP_CONV_RULE DATATYPE_CONV) 379 |> addThms 380 381val write_monop_rwt = 382 EV ([write_monop_def, 383 write_arith_result_no_CF_OF_def, 384 write_arith_eflags_except_CF_OF_def, 385 write_PF_rwt, write'CF_def, write'OF_def, 386 write'Eflag_rwt, CF_def, FlagUnspecified_def] @ 387 write_SF_rwt @ write_ZF_rwt @ write'EA_rwt) [] 388 (utilsLib.augment (`mop`, monops) ea_op) 389 ``write_monop (size1, mop, x, ea)`` 390 |> List.map (utilsLib.ALL_HYP_CONV_RULE DATATYPE_CONV) 391 |> addThms 392 393(* ------------------------------------------------------------------------ *) 394 395val () = resetEvConv () 396 397val conds = TypeBase.constructors_of ``:Zcond`` 398 399val read_cond_rwts = 400 EV [read_cond_def, Eflag_def, CF_def, PF_def, AF_def, ZF_def, SF_def, OF_def, 401 id_state_cond, cond_thms] 402 [[``^st.EFLAGS (Z_CF) = SOME cflag``, 403 ``^st.EFLAGS (Z_PF) = SOME pflag``, 404 ``^st.EFLAGS (Z_AF) = SOME aflag``, 405 ``^st.EFLAGS (Z_ZF) = SOME zflag``, 406 ``^st.EFLAGS (Z_SF) = SOME sflag``, 407 ``^st.EFLAGS (Z_OF) = SOME oflag``]] 408 (mapl (`c`, conds)) 409 ``read_cond c`` 410 |> addThms 411 412val SignExtension_rwt = 413 EV [SignExtension_def] [] 414 [[`s1` |-> ``Z8 (b)``, `s2` |-> ``Z16``], 415 [`s1` |-> ``Z8 (b)``, `s2` |-> ``Z32``], 416 [`s1` |-> ``Z8 (b)``, `s2` |-> ``Z64``], 417 [`s1` |-> ``Z16``, `s2` |-> ``Z32``], 418 [`s1` |-> ``Z16``, `s2` |-> ``Z64``], 419 [`s1` |-> ``Z32``, `s2` |-> ``Z64``]] 420 ``SignExtension (w, s1, s2)`` 421 422val SignExtension64_rwt = 423 EV (SignExtension64_def :: SignExtension_rwt) [] 424 [[`sz` |-> ``Z8 (b)``], [`sz` |-> ``Z16``], 425 [`sz` |-> ``Z32``], [`sz` |-> ``Z64``]] 426 ``SignExtension64 (w, sz)`` 427 428(* ------------------------------------------------------------------------ *) 429 430val rm = 431 [[`rm` |-> ``Zr r``], 432 [`rm` |-> ``Zm (NONE, ZnoBase, d)``], 433 [`rm` |-> ``Zm (NONE, ZripBase, d)``], 434 [`rm` |-> ``Zm (NONE, ZregBase r, d)``], 435 [`rm` |-> ``Zm (SOME (scale, ix), ZnoBase, d)``], 436 [`rm` |-> ``Zm (SOME (scale, ix), ZripBase, d)``], 437 [`rm` |-> ``Zm (SOME (scale, ix), ZregBase r, d)``]]: utilsLib.cover 438 439val r_rm = 440 [[`ds` |-> ``Zr_rm (r1, Zr r2)``], 441 [`ds` |-> ``Zr_rm (r, Zm (NONE, ZnoBase, d))``], 442 [`ds` |-> ``Zr_rm (r, Zm (NONE, ZripBase, d))``], 443 [`ds` |-> ``Zr_rm (r1, Zm (NONE, ZregBase r2, d))``], 444 [`ds` |-> ``Zr_rm (r, Zm (SOME (scale, ix), ZnoBase, d))``], 445 [`ds` |-> ``Zr_rm (r, Zm (SOME (scale, ix), ZripBase, d))``], 446 [`ds` |-> ``Zr_rm (r1, Zm (SOME (scale, ix), ZregBase r2, d))``]] 447 : utilsLib.cover 448 449val rm_i = 450 [[`ds` |-> ``Zrm_i (Zr r, i)``], 451 [`ds` |-> ``Zrm_i (Zm (NONE, ZnoBase, d), i)``], 452 [`ds` |-> ``Zrm_i (Zm (NONE, ZripBase, d), i)``], 453 [`ds` |-> ``Zrm_i (Zm (NONE, ZregBase r, d), i)``], 454 [`ds` |-> ``Zrm_i (Zm (SOME (scale, ix), ZnoBase, d), i)``], 455 [`ds` |-> ``Zrm_i (Zm (SOME (scale, ix), ZripBase, d), i)``], 456 [`ds` |-> ``Zrm_i (Zm (SOME (scale, ix), ZregBase r, d), i)``]] 457 : utilsLib.cover 458 459val rm_r = 460 [[`ds` |-> ``Zrm_r (Zr r1, r2)``], 461 [`ds` |-> ``Zrm_r (Zm (NONE, ZnoBase, d), r)``], 462 [`ds` |-> ``Zrm_r (Zm (NONE, ZripBase, d), r)``], 463 [`ds` |-> ``Zrm_r (Zm (NONE, ZregBase r1, d), r2)``], 464 [`ds` |-> ``Zrm_r (Zm (SOME (scale, ix), ZnoBase, d), r)``], 465 [`ds` |-> ``Zrm_r (Zm (SOME (scale, ix), ZripBase, d), r)``], 466 [`ds` |-> ``Zrm_r (Zm (SOME (scale, ix), ZregBase r1, d), r2)``]] 467 : utilsLib.cover 468 469local 470 val l = rm_i @ rm_r @ r_rm 471 val aug_size = utilsLib.augment (`size`, sizes) 472 val aug_size_not8 = utilsLib.augment (`size`, tl sizes) 473in 474 val src_dst = aug_size l 475 val src_dst_not8 = aug_size_not8 l 476 val src_dst_not8_or_r_rm = aug_size_not8 (rm_i @ rm_r) 477 val lea = aug_size_not8 (tl r_rm) 478 val rm_cases = aug_size rm 479 val rm_cases_not8 = aug_size_not8 rm 480end 481 482val extends = 483 (* 8 -> 16, 32, 64 *) 484 utilsLib.augment (`size2`, tl sizes) 485 (utilsLib.augment (`size`, [hd sizes]) r_rm) @ 486 (* 16 -> 32, 64 *) 487 utilsLib.augment (`size2`, List.drop (sizes, 2)) 488 (utilsLib.augment (`size`, [List.nth(sizes, 1)]) r_rm) @ 489 (* 32 -> 64 *) 490 utilsLib.augment (`size2`, List.drop (sizes, 3)) 491 (utilsLib.augment (`size`, [List.nth(sizes, 2)]) r_rm) 492 493(* ------------------------------------------------------------------------ *) 494 495(* TODO: CMPXCHG, XADD *) 496 497val data_hyp_rule = 498 List.map (utilsLib.ALL_HYP_CONV_RULE 499 (INST_REWRITE_CONV EA_rwt THENC DATATYPE_CONV)) 500 501val flags_override_rule = 502 List.map 503 (CONV_RULE 504 (Conv.DEPTH_CONV 505 (updateLib.OVERRIDE_UPDATES_CONV ``:Zeflags -> bool option`` 506 (SIMP_CONV (srw_ss()) [])))) 507 508val cond_update_rule = List.map (Conv.CONV_RULE COND_UPDATE_CONV) 509 510(* 511val is_some_hyp_rule = 512 List.map 513 (utilsLib.MATCH_HYP_CONV_RULE (REWRITE_CONV [optionTheory.IS_SOME_DEF]) 514 ``IS_SOME (x: 'a word option)`` o 515 utilsLib.MATCH_HYP_RULE (ASM_REWRITE_RULE []) 516 ``IS_SOME (x: 'a word option)``) 517*) 518 519val bit_test_rwt = 520 EV ([bit_test_def, write'CF_def, Cflag_rwt, write'Eflag_rwt] @ 521 EA_rwt @ write'EA_rwt) [] 522 (utilsLib.augment 523 (`bt`, [``Zbt``, ``Zbts``, ``Zbtr``, ``Zbtc``]) 524 (List.take (tl no_imm_ea, 4))) 525 ``bit_test (bt, ea, offset)`` 526 |> data_hyp_rule 527 |> wv_to_v 528 529val Zbit_test_rwt = 530 EV ([dfn'Zbit_test_def, modSize_def] @ SignExtension64_rwt @ bit_test_rwt @ 531 ea_Zrm_rwt @ EA_rwt @ write'EA_rwt @ ea_Zsrc_rwt @ ea_Zdest_rwt) [] 532 (utilsLib.augment 533 (`bt`, [``Zbt``, ``Zbts``, ``Zbtr``, ``Zbtc``]) src_dst_not8_or_r_rm) 534 ``dfn'Zbit_test (bt, size, ds)`` 535 |> data_hyp_rule 536 |> addThms 537 538(* val Znop_rwt = EV [dfn'Znop_def] [] [] ``dfn'Znop n`` |> addThms *) 539 540val Zcmc_rwt = 541 EV [dfn'Zcmc_def, CF_def, write'CF_def, Cflag_rwt, write'Eflag_rwt] [] [] 542 ``dfn'Zcmc`` 543 |> addThms 544 545val Zclc_rwt = 546 EV [dfn'Zclc_def, CF_def, write'CF_def, write'Eflag_rwt] [] [] 547 ``dfn'Zclc`` 548 |> addThms 549 550val Zstc_rwt = 551 EV [dfn'Zstc_def, CF_def, write'CF_def, write'Eflag_rwt] [] [] 552 ``dfn'Zstc`` 553 |> addThms 554 555val Zbinop_rwts = 556 EV ([dfn'Zbinop_def, read_dest_src_ea_def] @ 557 ea_Zsrc_rwt @ ea_Zdest_rwt @ EA_rwt) [] src_dst 558 ``dfn'Zbinop (bop, size, ds)`` 559 |> addThms 560 561val Zcall_imm_rwts = 562 EV ([dfn'Zcall_def, x64_push_rip_def, x64_push_aux_def, jump_to_ea_def, 563 call_dest_from_ea_def, write'mem64_rwt] @ ea_Zimm_rm_rwt) [] [] 564 ``dfn'Zcall (Zimm imm)`` 565 |> data_hyp_rule 566 |> addThms 567 568val Zcall_rm_rwts = 569 EV ([dfn'Zcall_def, x64_push_rip_def, x64_push_aux_def, jump_to_ea_def, 570 call_dest_from_ea_def, write'mem64_rwt, mem64_rwt] @ 571 ea_Zimm_rm_rwt) [] rm 572 ``dfn'Zcall (Zrm rm)`` 573 |> data_hyp_rule 574 |> addThms 575 576val Zjcc_rwts = 577 EV ([dfn'Zjcc_def] @ read_cond_rwts) [] (mapl (`c`, conds)) 578 ``dfn'Zjcc (c, imm)`` 579 |> cond_update_rule 580 |> addThms 581 582val Zjmp_rwts = 583 EV ([dfn'Zjmp_def] @ ea_Zrm_rwt @ EA_rwt) [] rm 584 ``dfn'Zjmp rm`` 585 |> addThms 586 587val Zlea_rwts = 588 EV ([dfn'Zlea_def, get_ea_address_def] @ 589 ea_Zsrc_rwt @ ea_Zdest_rwt @ EA_rwt @ write'EA_rwt) [] lea 590 ``dfn'Zlea (size, ds)`` 591 |> addThms 592 593val Zleave_rwts = 594 EV ([dfn'Zleave_def, x64_pop_def, x64_pop_aux_def, mem64_rwt, 595 combinTheory.UPDATE_EQ] @ ea_Zrm_rwt @ write'EA_rwt) 596 [] [] 597 ``dfn'Zleave`` 598 |> addThms 599 600val Zloop_rwts = 601 EV ([dfn'Zloop_def] @ read_cond_rwts) [] 602 (mapl (`c`, [``Z_NE``, ``Z_E``, ``Z_ALWAYS``])) 603 ``dfn'Zloop (c, imm)`` 604 |> data_hyp_rule 605 |> cond_update_rule 606 |> addThms 607 608val Zmonop_rwts = 609 EV ([dfn'Zmonop_def] @ ea_Zrm_rwt @ EA_rwt) [] rm_cases 610 ``dfn'Zmonop (mop, size, rm)`` 611 |> addThms 612 613val Zmov_rwts = 614 EV ([dfn'Zmov_def] @ 615 ea_Zsrc_rwt @ ea_Zdest_rwt @ read_cond_rwts @ EA_rwt @ write'EA_rwt) 616 [] (utilsLib.augment (`c`, Lib.butlast conds) src_dst_not8 @ 617 utilsLib.augment (`c`, [``Z_ALWAYS``]) src_dst) 618 ``dfn'Zmov (c, size, ds)`` 619 (* |> is_some_hyp_rule *) 620 |> cond_update_rule 621 |> addThms 622 623val Zmovzx_rwts = 624 EV ([dfn'Zmovzx_def, cond_rand_thms, word_thms] @ 625 ea_Zsrc_rwt @ ea_Zdest_rwt @ EA_rwt @ write'EA_rwt) 626 [] extends 627 ``dfn'Zmovzx (size, ds, size2)`` 628 |> addThms 629 630val Zmovsx_rwts = 631 EV ([dfn'Zmovsx_def, cond_rand_thms, extension_thms, word_thms] @ 632 SignExtension_rwt @ ea_Zsrc_rwt @ ea_Zdest_rwt @ EA_rwt @ write'EA_rwt) 633 [] extends 634 ``dfn'Zmovsx (size, ds, size2)`` 635 |> addThms 636 637val Zmul_rwts = 638 EV ([dfn'Zmul_def, erase_eflags, value_width_def, Zsize_width_def, 639 word_mul_thms, word_mul_top] @ 640 ea_Zrm_rwt @ EA_rwt @ write'EA_rwt) [] rm_cases 641 ``dfn'Zmul (size, rm)`` 642 |> addThms 643 644val Zimul_rwts = 645 EV ([dfn'Zimul_def, erase_eflags, value_width_def, Zsize_width_def, 646 write'CF_def, write'OF_def, write'Eflag_rwt, word_thms, 647 integer_wordTheory.word_mul_i2w] @ 648 SignExtension64_rwt @ ea_Zrm_rwt @ EA_rwt @ write'EA_rwt) [] rm_cases 649 ``dfn'Zimul (size, rm)`` 650 |> flags_override_rule 651 |> addThms 652 653val Zimul2_rwts = 654 EV ([dfn'Zimul2_def, erase_eflags, value_width_def, Zsize_width_def, 655 write'CF_def, write'OF_def, write'Eflag_rwt, word_thms, 656 integer_wordTheory.word_mul_i2w] @ SignExtension64_rwt @ ea_Zrm_rwt @ 657 EA_rwt @ write'EA_rwt) [] rm_cases_not8 658 ``dfn'Zimul2 (size, d, rm)`` 659 |> flags_override_rule 660 |> addThms 661 662val Zimul3_rwts = 663 EV ([dfn'Zimul3_def, erase_eflags, value_width_def, Zsize_width_def, 664 write'CF_def, write'OF_def, write'Eflag_rwt, word_thms, 665 integer_wordTheory.word_mul_i2w] @ SignExtension64_rwt @ ea_Zrm_rwt @ 666 EA_rwt @ write'EA_rwt) [] rm_cases_not8 667 ``dfn'Zimul3 (size, d, rm, imm)`` 668 |> flags_override_rule 669 |> addThms 670 671val Zpop_rwts = 672 EV ([dfn'Zpop_def, x64_pop_def, x64_pop_aux_def, mem64_rwt] @ 673 ea_Zrm_rwt @ write'EA_rwt) 674 [] rm 675 ``dfn'Zpop rm`` 676 |> data_hyp_rule 677 |> addThms 678 679val Zpush_imm_rwts = 680 EV ([dfn'Zpush_def, x64_push_def, x64_push_aux_def, write'mem64_rwt] @ 681 ea_Zimm_rm_rwt @ EA_rwt) [] [] 682 ``dfn'Zpush (Zimm imm)`` 683 |> data_hyp_rule 684 |> addThms 685 686val Zpush_rm_rwts = 687 EV ([dfn'Zpush_def, x64_push_def, x64_push_aux_def, write'mem64_rwt] @ 688 ea_Zimm_rm_rwt @ EA_rwt) [] rm 689 ``dfn'Zpush (Zrm rm)`` 690 |> data_hyp_rule 691 |> addThms 692 693val Zret_rwts = 694 EV [dfn'Zret_def, x64_pop_rip_def, x64_pop_aux_def, x64_drop_def, mem64_rwt, 695 combinTheory.UPDATE_EQ] 696 [[``(7 >< 0) (imm: word64) = 0w: word8``]] [] 697 ``dfn'Zret imm`` 698 |> addThms 699 700val Zset_rwts = 701 EV ([dfn'Zset_def, word_thms] @ 702 read_cond_rwts @ ea_Zrm_rwt @ write'EA_rwt) [] 703 (utilsLib.augment (`c`, Lib.butlast conds) rm) 704 ``dfn'Zset (c, have_rex, rm)`` 705 |> addThms 706 707val Zxchg_rwts = 708 EV ([dfn'Zxchg_def] @ ea_Zrm_rwt @ EA_rwt @ write'EA_rwt_r) 709 [] rm_cases 710 ``dfn'Zxchg (size, rm, r2)`` 711 |> data_hyp_rule 712 (* |> is_some_hyp_rule *) 713 |> addThms 714 715val () = setEvConv (Conv.DEPTH_CONV wordsLib.SIZES_CONV) 716 717val div_ev = 718 EV ([dfn'Zdiv_def, dfn'Zidiv_def, erase_eflags, value_width_def, 719 Zsize_width_def, word_thms, wordsTheory.w2n_w2w, 720 utilsLib.map_conv EVAL 721 [``256 / 2i``, ``65536 / 2i``, ``4294967296 / 2i``, 722 ``18446744073709551616 / 2i``], 723 wordsTheory.w2n_eq_0, integer_wordTheory.w2i_eq_0] @ 724 SignExtension64_rwt @ ea_Zrm_rwt @ EA_rwt @ write'EA_rwt) 725 726fun avoid_error_rule th = 727 let 728 val ths = th |> rhsc 729 |> boolSyntax.dest_cond 730 |> #1 731 |> boolSyntax.strip_disj 732 |> List.map (Thm.ASSUME o boolSyntax.mk_neg) 733 in 734 REWRITE_RULE ths th 735 end 736 737val Zdiv_rwts = 738 div_ev [] (tl rm_cases) 739 ``dfn'Zdiv (size, rm)`` 740 |> List.map avoid_error_rule 741 |> addThms 742 743val Zidiv_rwts = 744 div_ev [] (tl rm_cases) 745 ``dfn'Zidiv (size, rm)`` 746 |> List.map avoid_error_rule 747 |> addThms 748 749val Zdiv_byte_reg_rwts_1 = 750 div_ev [] [] ``dfn'Zdiv (Z8 T, Zr r)`` 751 |> List.map avoid_error_rule 752 |> addThms 753 754val Zidiv_byte_reg_rwts_1 = 755 div_ev [] [] ``dfn'Zidiv (Z8 T, Zr r)`` 756 |> List.map avoid_error_rule 757 |> addThms 758 759val Zdiv_byte_reg_rwts_2 = 760 div_ev [] 761 [[`r` |-> ``RAX``], [`r` |-> ``RCX``], [`r` |-> ``RDX``], [`r` |-> ``RBX``], 762 [`r` |-> ``RSP``], [`r` |-> ``RBP``], [`r` |-> ``RSI``], [`r` |-> ``RDI``]] 763 ``dfn'Zdiv (Z8 F, Zr r)`` 764 |> List.map avoid_error_rule 765 |> addThms 766 767val Zidiv_byte_reg_rwts_2 = 768 div_ev [] 769 [[`r` |-> ``RAX``], [`r` |-> ``RCX``], [`r` |-> ``RDX``], [`r` |-> ``RBX``], 770 [`r` |-> ``RSP``], [`r` |-> ``RBP``], [`r` |-> ``RSI``], [`r` |-> ``RDI``]] 771 ``dfn'Zidiv (Z8 F, Zr r)`` 772 |> List.map avoid_error_rule 773 |> addThms 774 775(* ------------------------------------------------------------------------ *) 776 777(* SSE *) 778 779(* Assume: 780 - all SSE exceptions are masked 781 - don't flush to zero 782 - denormals are not treated as zero 783*) 784val mxcsr = 785 [``~^st.MXCSR.FZ``, ``^st.MXCSR.PM``, ``^st.MXCSR.UM``, ``^st.MXCSR.OM``, 786 ``^st.MXCSR.ZM``, ``^st.MXCSR.DM``, ``^st.MXCSR.IM``, ``~^st.MXCSR.DAZ``] 787 788fun process_float_flags q = 789 process_float_flags_def 790 |> Q.ISPEC q 791 |> (fn th => Thm.AP_THM th st) 792 |> SIMP_RULE (srw_ss()++boolSimps.LET_ss) 793 [Ntimes state_transformerTheory.FOREACH_def 5, 794 state_transformerTheory.BIND_DEF, 795 state_transformerTheory.UNIT_DEF, 796 pairTheory.UNCURRY, cond_rand_thms, 797 XM_exception_def, initial_ieee_flags_def] 798 |> CONV_RULE (utilsLib.INST_REWRITE_CONV (List.map ASSUME mxcsr)) 799 |> FULL_CONV_RULE DATATYPE_CONV 800 801val process_float_flags1 = process_float_flags `[f : bool # flags]` 802val process_float_flags2 = process_float_flags `[f1 : bool # flags; f2]` 803val process_float_flags4 = process_float_flags `[f1 : bool # flags; f2; f3; f4]` 804 805val lem1 = Q.prove( 806 `(!x y. 807 (if IS_SOME x then i2w (THE x) else y) = 808 case x of SOME a => i2w a | _ => y) /\ 809 (!x y. 810 (if IS_SOME x then w2w (i2w (THE x) : 'c word) else y) = 811 case x of SOME a => w2w (i2w a : 'c word) | _ => y)`, 812 strip_tac \\ Cases \\ rw []) 813 814val lem2 = Q.prove( 815 `(case x of 816 LT => s with EFLAGS := a 817 | EQ => s with EFLAGS := b 818 | GT => s with EFLAGS := c 819 | UN => s with EFLAGS := d) 820 with EFLAGS := 821 (Z_SF =+ SOME F) 822 ((Z_AF =+ SOME F) 823 ((Z_OF =+ SOME F) 824 (case x of 825 LT => s with EFLAGS := 826 (Z_CF =+ SOME T) ((Z_PF =+ SOME F) ((Z_ZF =+ SOME F) s.EFLAGS)) 827 | EQ => s with EFLAGS := 828 (Z_CF =+ SOME F) ((Z_PF =+ SOME F) ((Z_ZF =+ SOME T) s.EFLAGS)) 829 | GT => s with EFLAGS := 830 (Z_CF =+ SOME F) ((Z_PF =+ SOME F) ((Z_ZF =+ SOME F) s.EFLAGS)) 831 | UN => s with EFLAGS := 832 (Z_CF =+ SOME T) ((Z_PF =+ SOME T) ((Z_ZF =+ SOME T) s.EFLAGS)) 833 ).EFLAGS)) = 834 s with EFLAGS := 835 (Z_SF =+ SOME F) 836 ((Z_AF =+ SOME F) 837 ((Z_OF =+ SOME F) 838 ((Z_CF =+ SOME (x IN {LT; UN})) 839 ((Z_PF =+ SOME (x = UN)) 840 ((Z_ZF =+ SOME (x IN {EQ; UN})) s.EFLAGS)))))`, 841 Cases_on `x` \\ simp []) 842 843val rule = List.map (REWRITE_RULE [lem1]) 844 845fun fpEV aug = 846 let 847 val c = case aug of 848 SOME [] => rm 849 | SOME a => utilsLib.augment (`f`, a) xmm 850 | NONE => xmm 851 in 852 EV ([dfn'bin_PD_def, dfn'bin_SD_def, dfn'bin_PS_def, dfn'bin_SS_def, 853 dfn'logic_PD_def, dfn'logic_PS_def, sse_logic_def, 854 dfn'CMPPD_def, dfn'CMPSD_def, dfn'CMPPS_def, dfn'CMPSS_def, 855 dfn'SQRTPD_def, dfn'SQRTSD_def, dfn'SQRTPS_def, dfn'SQRTSS_def, 856 dfn'CVTDQ2PD_def, dfn'CVTDQ2PS_def, dfn'CVTPD2DQ_def, 857 dfn'CVTPD2PS_def, dfn'CVTPS2DQ_def, dfn'CVTPS2PD_def, 858 dfn'CVTSD2SS_def, dfn'CVTSS2SD_def, dfn'MOVUP_D_S_def, 859 dfn'CVTSD2SI_def, dfn'CVTSI2SD_def, 860 dfn'CVTSI2SS_def, dfn'CVTSS2SI_def, 861 dfn'COMISD_def, dfn'COMISS_def, dfn'MOV_D_Q_def, dfn'MOVQ_def, 862 dfn'MOVSD_def, dfn'MOVSS_def, dfn'PCMPEQQ_def, 863 write'SF_def, write'AF_def, write'OF_def, write'CF_def, 864 write'PF_def, write'ZF_def, write'Eflag_rwt, 865 RoundingMode_def, rounding_mode, sse_compare_signalling_def, 866 process_float_flags1, process_float_flags2, process_float_flags4, 867 sse_binop32_def, sse_sqrt32_def, sse_compare32_def, sse_from_int32_def, 868 sse_to_int32_def, flush_to_zero32, denormal_to_zero32_def, 869 sse_binop64_def, sse_sqrt64_def, sse_compare64_def, sse_from_int64_def, 870 sse_to_int64_def, flush_to_zero64, denormal_to_zero64_def, 871 initial_ieee_flags_def, set_precision_def, snd_with_flags, 872 pred_setTheory.IN_INSERT, pred_setTheory.NOT_IN_EMPTY, 873 ConseqConvTheory.COND_CLAUSES_FT, ConseqConvTheory.COND_CLAUSES_FF, 874 pairTheory.pair_CASE_def, word_thms, lem2] @ 875 XMM_rwt @ write'XMM_rwt @ EA_rwt @ write'EA_rwt @ ea_Zrm_rwt) [mxcsr] c 876 end 877 878val pshift = 879 EV ([dfn'PSRLW_imm_def, dfn'PSRAW_imm_def, dfn'PSLLW_imm_def, 880 dfn'PSRLD_imm_def, dfn'PSRAD_imm_def, dfn'PSLLD_imm_def, 881 dfn'PSRLQ_imm_def, dfn'PSLLQ_imm_def, dfn'PSRLDQ_def, dfn'PSLLDQ_def] @ 882 XMM_rwt @ write'XMM_rwt) [] [] 883 884val sse_bin = 885 fpEV (SOME [``sse_add``, ``sse_sub``, ``sse_mul``, ``sse_div``, 886 ``sse_min``, ``sse_max``]) 887 888val sse_logic = 889 fpEV (SOME [``sse_and``, ``sse_andn``, ``sse_or``, ``sse_xor``]) 890 891val sse_compare = 892 fpEV (SOME [``sse_eq_oq``, ``sse_lt_os``, ``sse_le_os``, ``sse_unord_q``, 893 ``sse_neq_uq``, ``sse_nlt_us``, ``sse_nle_us``, ``sse_ord_q``]) 894 895val sse = rule o fpEV NONE 896val sse_rm = fpEV (SOME []) 897 898val bin_PD = sse_bin ``dfn'bin_PD (f, dst, xmm)`` 899val bin_SD = sse_bin ``dfn'bin_SD (f, dst, xmm)`` 900val bin_PS = sse_bin ``dfn'bin_PS (f, dst, xmm)`` 901val bin_SS = sse_bin ``dfn'bin_SS (f, dst, xmm)`` 902 903val logic_PD = sse_logic ``dfn'logic_PD (f, dst, xmm)`` 904val logic_PS = sse_logic ``dfn'logic_PS (f, dst, xmm)`` 905 906val CMPPD = sse_compare ``dfn'CMPPD (f, dst, xmm)`` 907val CMPSD = sse_compare ``dfn'CMPSD (f, dst, xmm)`` 908val CMPPS = sse_compare ``dfn'CMPPS (f, dst, xmm)`` 909val CMPSS = sse_compare ``dfn'CMPSS (f, dst, xmm)`` 910 911val COMISD = sse ``dfn'COMISD (src1, xmm)`` 912val COMISS = sse ``dfn'COMISS (src1, xmm)`` 913 914val SQRTPD = sse ``dfn'SQRTPD (dst, xmm)`` 915val SQRTSD = sse ``dfn'SQRTSD (dst, xmm)`` 916val SQRTPS = sse ``dfn'SQRTPS (dst, xmm)`` 917val SQRTSS = sse ``dfn'SQRTSS (dst, xmm)`` 918 919val CVTDQ2PD = sse ``dfn'CVTDQ2PD (dst, xmm)`` 920val CVTDQ2PS = sse ``dfn'CVTDQ2PS (dst, xmm)`` 921val CVTPD2DQ = sse ``dfn'CVTPD2DQ (F, dst, xmm)`` 922val CVTTPD2DQ = sse ``dfn'CVTPD2DQ (T, dst, xmm)`` 923val CVTPD2PS = sse ``dfn'CVTPD2PS (dst, xmm)`` 924val CVTPS2DQ = sse ``dfn'CVTPS2DQ (F, dst, xmm)`` 925val CVTTPS2DQ = sse ``dfn'CVTPS2DQ (T, dst, xmm)`` 926val CVTPS2PD = sse ``dfn'CVTPS2PD (dst, xmm)`` 927val CVTSD2SS = sse ``dfn'CVTSD2SS (dst, xmm)`` 928val CVTSS2SD = sse ``dfn'CVTSS2SD (dst, xmm)`` 929val CVTSD2SI_0 = sse ``dfn'CVTSD2SI (F, T, r, xmm)`` 930val CVTSD2SI_1 = sse ``dfn'CVTSD2SI (F, F, r, xmm)`` 931val CVTTSD2SI_0 = sse ``dfn'CVTSD2SI (T, T, r, xmm)`` 932val CVTTSD2SI_1 = sse ``dfn'CVTSD2SI (T, F, r, xmm)`` 933val CVTSI2SD_0 = sse_rm ``dfn'CVTSI2SD (T, x, rm)`` 934val CVTSI2SD_1 = sse_rm ``dfn'CVTSI2SD (F, x, rm)`` 935val CVTSI2SS_0 = sse_rm ``dfn'CVTSI2SS (T, x, rm)`` 936val CVTSI2SS_1 = sse_rm ``dfn'CVTSI2SS (F, x, rm)`` 937val CVTSS2SI_0 = sse ``dfn'CVTSS2SI (F, T, r, xmm)`` 938val CVTSS2SI_1 = sse ``dfn'CVTSS2SI (F, F, r, xmm)`` 939val CVTTSS2SI_0 = sse ``dfn'CVTSS2SI (T, T, r, xmm)`` 940val CVTTSS2SI_1 = sse ``dfn'CVTSS2SI (T, F, r, xmm)`` 941 942(* TODO: MOVAP_D_S *) 943 944val MOVUP_D_S_0 = sse ``dfn'MOVUP_D_S (double, xmm_reg (dst), xmm)`` 945val MOVUP_D_S_1 = sse ``dfn'MOVUP_D_S (double, xmm, xmm_reg (src))`` |> List.tl 946 947val MOVSD_0 = sse ``dfn'MOVSD (xmm_reg (dst), xmm)`` 948val MOVSD_1 = sse ``dfn'MOVSD (xmm, xmm_reg (src))`` |> List.tl |> wv_to_v 949val MOVSS_0 = sse ``dfn'MOVSS (xmm_reg (dst), xmm)`` 950val MOVSS_1 = sse ``dfn'MOVSS (xmm, xmm_reg (src))`` |> List.tl |> wv_to_v 951 952val MOV_D_Q_0 = sse_rm ``dfn'MOV_D_Q (T, T, dst, rm)`` 953val MOV_D_Q_1 = sse_rm ``dfn'MOV_D_Q (T, F, dst, rm)`` 954val MOV_D_Q_2 = sse_rm ``dfn'MOV_D_Q (F, T, dst, rm)`` 955val MOV_D_Q_3 = sse_rm ``dfn'MOV_D_Q (F, F, dst, rm)`` 956 957val MOVQ_0 = sse ``dfn'MOVQ (xmm_reg (dst), xmm)`` 958val MOVQ_1 = sse ``dfn'MOVQ (xmm, xmm_reg (src))`` |> List.tl 959 960val PCMPEQQ = sse ``dfn'PCMPEQQ (dst, xmm)`` 961 962val PSRLW_imm = pshift ``dfn'PSRLW_imm (r, i)`` 963val PSRAW_imm = pshift ``dfn'PSRAW_imm (r, i)`` 964val PSLLW_imm = pshift ``dfn'PSLLW_imm (r, i)`` 965val PSRLD_imm = pshift ``dfn'PSRLD_imm (r, i)`` 966val PSRAD_imm = pshift ``dfn'PSRAD_imm (r, i)`` 967val PSLLD_imm = pshift ``dfn'PSLLD_imm (r, i)`` 968val PSRLQ_imm = pshift ``dfn'PSRLQ_imm (r, i)`` 969val PSLLQ_imm = pshift ``dfn'PSLLQ_imm (r, i)`` 970val PSRLDQ = pshift ``dfn'PSRLDQ (r, i)`` 971val PSLLDQ = pshift ``dfn'PSLLDQ (r, i)`` 972 973val _ = List.map addThms 974 [bin_PD, bin_SD, bin_PS, bin_SS, logic_PD, logic_PS, CMPPD, CMPSD, CMPPS, 975 CMPSS, COMISD, COMISS, SQRTPD, SQRTSD, SQRTPS, SQRTSS, CVTDQ2PD, CVTDQ2PS, 976 CVTPD2DQ, CVTTPD2DQ, CVTPD2PS, CVTPS2DQ, CVTTPS2DQ, CVTPS2PD, CVTSD2SS, 977 CVTSS2SD, CVTSD2SI_0, CVTSD2SI_1, CVTTSD2SI_0, CVTTSD2SI_1, CVTSI2SD_0, 978 CVTSI2SD_1, CVTSI2SS_0, CVTSI2SS_1, CVTSS2SI_0, CVTSS2SI_1, CVTTSS2SI_0, 979 CVTTSS2SI_1, MOVUP_D_S_0, MOVUP_D_S_1, MOV_D_Q_0, MOV_D_Q_1, MOV_D_Q_2, 980 MOV_D_Q_3, MOVQ_0, MOVQ_1, MOVSD_0, MOVSD_1, MOVSS_0, MOVSS_1, PCMPEQQ, 981 PSRLW_imm, PSRAW_imm, PSLLW_imm, PSRLD_imm, PSRAD_imm, PSLLD_imm, 982 PSRLQ_imm, PSLLQ_imm, PSRLDQ, PSLLDQ] 983 984(* ------------------------------------------------------------------------ *) 985 986local 987 fun decode_err s = ERR "x64_decode" s 988 val i8 = fcpSyntax.mk_int_numeric_type 8 989 val w8 = wordsSyntax.mk_int_word_type 8 990 val imm8_tm = combinSyntax.mk_I (Term.mk_var ("imm", w8)) 991 fun mk_extract imm n = 992 let 993 val h = numSyntax.term_of_int (n - 1) 994 val l = numSyntax.term_of_int (n - 8) 995 in 996 wordsSyntax.mk_word_extract(h, l, imm, i8) 997 end 998 fun mk_extracts n = 999 let 1000 val mk = 1001 mk_extract (Term.mk_var ("imm", wordsSyntax.mk_int_word_type n)) 1002 fun iter a n = if n < 8 then a else iter (mk n :: a) (n - 8) 1003 in 1004 iter [] n 1005 end 1006 fun mk_byte w = wordsSyntax.mk_wordi (w, 8) 1007 fun toByte (x, y) = mk_byte (Arbnum.fromHexString (String.implode [x, y])) 1008 val x64_fetch = 1009 (x64_CONV THENC REWRITE_CONV [wordsTheory.WORD_ADD_0])``x64_fetch s`` 1010 fun fetch l = 1011 List.foldl 1012 (fn (b, (i, thm)) => 1013 let 1014 val rwt = if i = 0 1015 then ``^st.MEM (^st.RIP) = ^b`` 1016 else let 1017 val j = numSyntax.term_of_int i 1018 in 1019 ``^st.MEM (^st.RIP + n2w ^j) = ^b`` 1020 end 1021 in 1022 (i + 1, PURE_REWRITE_RULE [ASSUME rwt, optionTheory.THE_DEF] thm) 1023 end) (0, x64_fetch) l |> snd 1024 val decode_tm = ``x64_decode (x64_fetch ^st)`` 1025 fun decode_thm fetch_rwt = 1026 (Conv.RAND_CONV (Conv.REWR_CONV fetch_rwt) THENC x64_CONV) decode_tm 1027 val get_list = 1028 fst o listSyntax.dest_list o optionSyntax.dest_some o #3 o 1029 Lib.triple_of_list o pairSyntax.strip_pair 1030in 1031 fun get_bytes s = 1032 let 1033 fun iter a [] = List.rev a 1034 | iter a (l as (x::y::t)) = 1035 if List.all (Lib.equal #"_") l 1036 then let 1037 val n = List.length l * 4 1038 in 1039 List.rev a @ 1040 (if n = 8 1041 then [imm8_tm] 1042 else if Lib.mem n [16, 32, 64] 1043 then mk_extracts n 1044 else raise ERR "x64_decode" 1045 ("bad immediate length: " ^ Int.toString n)) 1046 end 1047 else iter (toByte (x, y) :: a) t 1048 | iter a [_] = raise decode_err "not even" 1049 in 1050 iter [] (String.explode s) 1051 end 1052 fun x64_decode l = 1053 let 1054 val thm = decode_thm (fetch l) 1055 in 1056 case boolSyntax.dest_strip_comb (utilsLib.rhsc thm) of 1057 ("x64$Zfull_inst", [a]) => 1058 (case Lib.total get_list a of 1059 SOME l => 1060 ( List.null l orelse not (wordsSyntax.is_n2w (hd l)) 1061 orelse raise decode_err "trailing bytes" 1062 ; thm 1063 ) 1064 | NONE => raise decode_err "decode failed") 1065 | _ => (Parse.print_thm thm; raise decode_err "too few bytes") 1066 end 1067 val x64_decode_hex = x64_decode o get_bytes 1068end 1069 1070(* ------------------------------------------------------------------------ *) 1071 1072local 1073 fun is_some_wv tm = 1074 ((tm |> boolSyntax.dest_eq |> snd 1075 |> Term.dest_var |> fst) = "wv") 1076 handle HOL_ERR _ => false 1077in 1078 fun FIX_SAME_ADDRESS_RULE thm = 1079 case List.partition is_some_wv (Thm.hyp thm) of 1080 ([], _) => thm 1081 | ([t], rst) => 1082 let 1083 val (l, wv) = boolSyntax.dest_eq t 1084 val v = Term.mk_var ("v", Term.type_of wv) 1085 val tv = boolSyntax.mk_eq (l, v) 1086 in 1087 if List.exists (Lib.equal tv) rst 1088 then Thm.INST [wv |-> v] thm 1089 else thm 1090 end 1091 | _ => raise ERR "FIX_SAME_ADDRESS_RULE" "more than one" 1092end 1093 1094local 1095 val rwts = [pairTheory.FST, pairTheory.SND, combinTheory.I_THM, word_thms] 1096 val TIDY_UP_CONV = 1097 REWRITE_CONV 1098 (List.take (utilsLib.datatype_rewrites false "x64" ["Zreg"], 2) @ rwts) 1099 THENC utilsLib.WGROUND_CONV 1100 val get_strm1 = Term.rand o Term.rand o Term.rand o Term.rand o utilsLib.rhsc 1101 val get_ast = Term.rand o Term.rator o Term.rand o Term.rand o utilsLib.rhsc 1102 val state_exception_tm = 1103 Term.prim_mk_const {Thy = "x64", Name = "x64_state_exception"} 1104 fun mk_proj_exception r = Term.mk_comb (state_exception_tm, r) 1105 val twenty = numSyntax.term_of_int 20 1106 fun mk_len_thm thm1 = 1107 (Conv.RAND_CONV listLib.LENGTH_CONV THENC numLib.REDUCE_CONV) 1108 (numSyntax.mk_minus (twenty, listSyntax.mk_length (get_strm1 thm1))) 1109 fun bump_rip len = Term.subst [st |-> ``^st with RIP := ^st.RIP + n2w ^len``] 1110 val run_CONV = utilsLib.Run_CONV ("x64", st) o get_ast 1111 val run = utilsLib.ALL_HYP_CONV_RULE utilsLib.WGROUND_CONV o 1112 FIX_SAME_ADDRESS_RULE o 1113 utilsLib.ALL_HYP_CONV_RULE TIDY_UP_CONV o 1114 (INST_REWRITE_CONV (getThms ()) THENC TIDY_UP_CONV) 1115 val MP_Next = Drule.MATCH_MP x64_stepTheory.NextStateX64 1116 val MP_Next0 = Drule.MATCH_MP x64_stepTheory.NextStateX64_0 1117 val STATE_CONV = 1118 REWRITE_CONV (utilsLib.datatype_rewrites true "x64" ["x64_state"] @ 1119 [boolTheory.COND_ID, cond_rand_thms]) 1120 fun unchanged l = 1121 raise ERR "x64_step" 1122 ("Failed to evaluate: " ^ 1123 Hol_pp.term_to_string (listSyntax.mk_list (l, ``:word8``))) 1124 val cache = 1125 ref (Redblackmap.mkDict String.compare: (string, thm) Redblackmap.dict) 1126 fun addToCache (s, thm) = (cache := Redblackmap.insert (!cache, s, thm); thm) 1127 fun checkCache s = Redblackmap.peek (!cache, s) 1128 val I_intro = 1129 Drule.GEN_ALL o 1130 Conv.RIGHT_CONV_RULE (ONCE_REWRITE_CONV [GSYM combinTheory.I_THM]) o 1131 Drule.SPEC_ALL 1132in 1133 fun x64_step l = 1134 let 1135 val thm1 = x64_decode l 1136 val thm2 = mk_len_thm thm1 1137 val thm4 = run_CONV thm1 1138 val s = utilsLib.rhsc (Drule.SPEC_ALL thm4) 1139 val thm4 = if Term.is_var s then I_intro thm4 else thm4 1140 val thm5 = (thm4 |> Drule.SPEC_ALL 1141 |> utilsLib.rhsc 1142 |> bump_rip (utilsLib.rhsc thm2) 1143 |> run) 1144 handle Conv.UNCHANGED => unchanged l 1145 val r = utilsLib.rhsc thm5 1146 val thm6 = Conv.QCONV STATE_CONV (mk_proj_exception r) 1147 val thm = Drule.LIST_CONJ [thm1, thm2, thm4, thm5, thm6] 1148 in 1149 MP_Next thm 1150 handle HOL_ERR {message = "different constructors", ...} => 1151 MP_Next0 thm 1152 end 1153 fun x64_step_hex s = 1154 let 1155 val s = utilsLib.uppercase s 1156 in 1157 case checkCache s of 1158 SOME thm => thm 1159 | NONE => addToCache (s, x64_step (get_bytes s)) 1160 end 1161end 1162 1163val x64_decode_code = 1164 List.map x64_decode_hex o x64AssemblerLib.x64_code_no_spaces 1165 1166val x64_step_code = List.map x64_step_hex o x64AssemblerLib.x64_code_no_spaces 1167 1168(* 1169 1170List.length (getThms ()) 1171 1172open x64_stepLib 1173 1174val thms = Count.apply x64_step_code 1175 `nop ; 90 1176 mov [r11], al ; 41 88 03 1177 jb 0x7 ; 72 07 1178 add dword [rbp-0x8], 0x1 ; 83 45 f8 01 1179 movsxd rdx, eax ; 48 63 d0 1180 movsx eax, al ; 0f be c0 1181 movzx eax, al ; 0f b6 c0` 1182 1183Count.apply x64_step_hex "90"; 1184Count.apply x64_step_hex "418803"; 1185Count.apply x64_step_hex "487207"; 1186Count.apply x64_step_hex "8345F801"; 1187Count.apply x64_step_hex "4863D0"; 1188Count.apply x64_step_hex "0FBEC0"; 1189Count.apply x64_step_hex "0FB6C0"; 1190 1191Count.apply x64_step_hex "48BA________________"; 1192Count.apply x64_decode_hex "48BA________________" 1193 1194Count.apply x64_step_hex "41B8________"; 1195Count.apply x64_decode_hex "41B8________" 1196 1197Count.apply x64_decode_hex "8345F8__"; 1198Count.apply x64_step_hex "8345F8__" 1199 1200*) 1201 1202(* ========================================================================= *) 1203 1204end 1205