1 2open HolKernel boolLib bossLib Parse; 3open wordsTheory bit_listTheory; 4 5open x86_coretypesTheory x86_astTheory x86_seq_monadTheory; 6 7val _ = new_theory "x86_opsem"; 8val _ = ParseExtras.temp_loose_equality() 9 10 11(* ---------------------------------------------------------------------------------- *> 12 13 We define the semantics of an instruction. 14 15<* ---------------------------------------------------------------------------------- *) 16 17 18(* assertion *) 19 20val assertT_def = Define ` 21 assertT b = if b then constT () else failureT`; 22 23val option_apply_assertT = store_thm("option_apply_assertT", 24 ``!b s f. b ==> (option_apply (assertT b s) f = f ((),s))``, 25 SIMP_TAC std_ss [assertT_def,constT_def,constT_seq_def,option_apply_def]); 26 27(* calculate effective address *) 28 29val ea_Xr_def = Define `ea_Xr (r:Xreg) = constT (Xea_r r)`; 30val ea_Xi_def = Define `ea_Xi (i:Ximm) = constT (Xea_i i)`; 31 32val ea_Xrm_base_def = Define ` 33 (ea_Xrm_base ii NONE = constT 0w) /\ 34 (ea_Xrm_base ii (SOME r) = read_reg ii r)`; 35 36val ea_Xrm_index_def = Define ` 37 (ea_Xrm_index ii NONE = constT (0w:Ximm)) /\ 38 (ea_Xrm_index ii (SOME (s:word2,r)) = 39 seqT (read_reg ii r) (\idx. constT (n2w (2 ** w2n s) * idx)))`; 40 41val ea_Xrm_def = Define ` 42 (ea_Xrm ii (Xr r) = ea_Xr r) /\ 43 (ea_Xrm ii (Xm i b d) = 44 seqT 45 (parT (ea_Xrm_index ii i) (ea_Xrm_base ii b)) 46 (\(idx,b). constT (Xea_m (idx + b + d))))`; 47 48val ea_Xdest_def = Define ` 49 (ea_Xdest ii (Xrm_i rm i) = ea_Xrm ii rm) /\ 50 (ea_Xdest ii (Xrm_r rm r) = ea_Xrm ii rm) /\ 51 (ea_Xdest ii (Xr_rm r rm) = ea_Xr r)`; 52 53val ea_Xsrc_def = Define ` 54 (ea_Xsrc ii (Xrm_i rm i) = ea_Xi i) /\ 55 (ea_Xsrc ii (Xrm_r rm r) = ea_Xr r) /\ 56 (ea_Xsrc ii (Xr_rm r rm) = ea_Xrm ii rm)`; 57 58val ea_Ximm_rm_def = Define ` 59 (ea_Ximm_rm ii (Xi_rm rm) = ea_Xrm ii rm) /\ 60 (ea_Ximm_rm ii (Xi i) = ea_Xi i)`; 61 62(* eval_ea calculates the value of an effective address *) 63 64val read_ea_def = Define ` 65 (read_ea ii (Xea_i i) = constT i) /\ 66 (read_ea ii (Xea_r r) = read_reg ii r) /\ 67 (read_ea ii (Xea_m a) = read_m32 ii a)`; 68 69val read_src_ea_def = Define ` 70 read_src_ea ii ds = seqT (ea_Xsrc ii ds) (\ea. addT ea (read_ea ii ea))`; 71 72val read_dest_ea_def = Define ` 73 read_dest_ea ii ds = seqT (ea_Xdest ii ds) (\ea. addT ea (read_ea ii ea))`; 74 75val read_reg_byte_def = Define ` 76 (read_reg_byte ii EAX = seqT (read_reg ii EAX) (\w. constT ((w2w w):word8))) /\ 77 (read_reg_byte ii EBX = seqT (read_reg ii EBX) (\w. constT (w2w w))) /\ 78 (read_reg_byte ii ECX = seqT (read_reg ii ECX) (\w. constT (w2w w))) /\ 79 (read_reg_byte ii EDX = seqT (read_reg ii EDX) (\w. constT (w2w w))) /\ 80 (read_reg_byte ii EBP = seqT (read_reg ii EAX) (\w. constT (w2w (w >>> 8)))) /\ 81 (read_reg_byte ii ESI = seqT (read_reg ii EBX) (\w. constT (w2w (w >>> 8)))) /\ 82 (read_reg_byte ii EDI = seqT (read_reg ii ECX) (\w. constT (w2w (w >>> 8)))) /\ 83 (read_reg_byte ii ESP = seqT (read_reg ii EDX) (\w. constT (w2w (w >>> 8))))`; 84 85val read_ea_byte_def = Define ` 86 (read_ea_byte ii (Xea_i i) = constT (w2w i)) /\ 87 (read_ea_byte ii (Xea_r r) = read_reg_byte ii r) /\ 88 (read_ea_byte ii (Xea_m a) = read_m8 ii a)`; 89 90val read_src_ea_byte_def = Define ` 91 read_src_ea_byte ii ds = seqT (ea_Xsrc ii ds) (\ea. addT ea (read_ea_byte ii ea))`; 92 93val read_dest_ea_byte_def = Define ` 94 read_dest_ea_byte ii ds = seqT (ea_Xdest ii ds) (\ea. addT ea (read_ea_byte ii ea))`; 95 96(* write_ea write a value to the supplied effective address *) 97 98val write_ea_def = Define ` 99 (write_ea ii (Xea_i i) x = failureT) /\ (* one cannot store into a constant *) 100 (write_ea ii (Xea_r r) x = write_reg ii r x) /\ 101 (write_ea ii (Xea_m a) x = write_m32 ii a x)`; 102 103val write_ea_byte_def = Define ` 104 (write_ea_byte ii (Xea_i i) x = failureT) /\ (* one cannot store into a constant *) 105 (write_ea_byte ii (Xea_r r) x = failureT) /\ (* not supported yet *) 106 (write_ea_byte ii (Xea_m a) x = write_m8 ii a x)`; 107 108(* jump_to_ea updates eip according to procedure call *) 109 110val jump_to_ea_def = Define ` 111 (jump_to_ea ii eip (Xea_i i) = write_eip ii (eip + i)) /\ 112 (jump_to_ea ii eip (Xea_r r) = seqT (read_reg ii r) (write_eip ii)) /\ 113 (jump_to_ea ii eip (Xea_m a) = seqT (read_m32 ii a) (write_eip ii))`; 114 115(* call_dest_from_ea finds the destination according to procedure call semantics *) 116 117val call_dest_from_ea_def = Define ` 118 (call_dest_from_ea ii eip (Xea_i i) = constT (eip + i)) /\ 119 (call_dest_from_ea ii eip (Xea_r r) = read_reg ii r) /\ 120 (call_dest_from_ea ii eip (Xea_m a) = read_m32 ii a)`; 121 122val get_ea_address_def = Define ` 123 (get_ea_address (Xea_i i) = 0w) /\ 124 (get_ea_address (Xea_r r) = 0w) /\ 125 (get_ea_address (Xea_m a) = a)`; 126 127(* eip modifiers *) 128 129val bump_eip_def = Define ` 130 bump_eip ii len rest = 131 parT_unit rest (seqT (read_eip ii) (\x. write_eip ii (x + len)))`; 132 133(* eflag updates *) 134 135val byte_parity_def = Define ` 136 byte_parity = EVEN o LENGTH o FILTER I o n2bits 8 o w2n`; 137 138val write_PF_def = Define `write_PF ii w = write_eflag ii X_PF (SOME (byte_parity w))`; 139val write_ZF_def = Define `write_ZF ii w = write_eflag ii X_ZF (SOME (w = 0w))`; 140val write_SF_def = Define `write_SF ii w = write_eflag ii X_SF (SOME (word_msb w))`; 141 142val write_logical_eflags_def = Define ` 143 write_logical_eflags ii w = 144 parT_unit (write_PF ii w) 145 (parT_unit (write_ZF ii w) 146 (parT_unit (write_SF ii w) 147 (parT_unit (write_eflag ii X_OF (SOME F)) 148 (parT_unit (write_eflag ii X_CF (SOME F)) 149 (write_eflag ii X_AF NONE)))))`; (* not modelled *) 150 151val write_arith_eflags_except_CF_OF_def = Define ` 152 write_arith_eflags_except_CF_OF ii w = 153 parT_unit (write_PF ii w) 154 (parT_unit (write_ZF ii w) 155 (parT_unit (write_SF ii w) 156 (write_eflag ii X_AF NONE)))`; 157 158val write_arith_eflags_def = Define ` 159 write_arith_eflags ii (w,c,x) = 160 parT_unit (write_eflag ii X_CF (SOME c)) 161 (parT_unit (write_eflag ii X_OF (SOME x)) 162 (write_arith_eflags_except_CF_OF ii w))`; 163 164val erase_eflags_def = Define ` 165 erase_eflags ii = 166 parT_unit (write_eflag ii X_PF NONE) 167 (parT_unit (write_eflag ii X_ZF NONE) 168 (parT_unit (write_eflag ii X_SF NONE) 169 (parT_unit (write_eflag ii X_OF NONE) 170 (parT_unit (write_eflag ii X_CF NONE) 171 (write_eflag ii X_AF NONE)))))`; 172 173(* binops *) 174 175val bool2num_def = Define `bool2num b = if b then 1 else 0`; 176 177val word_signed_overflow_add_def = Define ` 178 word_signed_overflow_add a b = 179 (word_msb a = word_msb b) /\ ~(word_msb (a + b) = word_msb a)`; 180 181val word_signed_overflow_sub_def = Define ` 182 word_signed_overflow_sub a b = 183 ~(word_msb a = word_msb b) /\ ~(word_msb (a - b) = word_msb a)`; 184 185val add_with_carry_out_def = Define ` 186 add_with_carry_out (x:Ximm) y = 187 (x + y, 2**32 <= w2n x + w2n y, word_signed_overflow_add x y)`; 188 189val sub_with_borrow_out_def = Define ` 190 sub_with_borrow_out (x:Ximm) y = 191 (x - y, x <+ y, word_signed_overflow_sub x y)`; 192 193val write_arith_result_def = Define ` 194 write_arith_result ii (w,c,x) ea = parT_unit (write_arith_eflags ii (w,c,x)) (write_ea ii ea w)`; 195 196val write_arith_result_no_CF_OF_def = Define ` 197 write_arith_result_no_CF_OF ii w ea = 198 (parT_unit (write_arith_eflags_except_CF_OF ii w) (write_ea ii ea w))`; 199 200val write_arith_result_no_write_def = Define ` 201 write_arith_result_no_write ii (w,c,x) = (write_arith_eflags ii (w,c,x))`; 202 203val write_logical_result_def = Define ` 204 write_logical_result ii w ea = (parT_unit (write_logical_eflags ii w) (write_ea ii ea w))`; 205 206val write_logical_result_no_write_def = Define ` 207 write_logical_result_no_write ii w = (write_logical_eflags ii w)`; 208 209val write_result_erase_eflags_def = Define ` 210 write_result_erase_eflags ii w ea = (parT_unit (erase_eflags ii) (write_ea ii ea w))`; 211 212val write_binop_def = Define ` 213 (write_binop ii Xadd x y ea = (write_arith_result ii (add_with_carry_out x y) ea)) /\ 214 (write_binop ii Xsub x y ea = (write_arith_result ii (sub_with_borrow_out x y) ea)) /\ 215 (write_binop ii Xcmp x y ea = (write_arith_result_no_write ii (sub_with_borrow_out x y))) /\ 216 (write_binop ii Xtest x y ea = (write_logical_result_no_write ii (x && y))) /\ 217 (write_binop ii Xand x y ea = (write_logical_result ii (x && y) ea)) /\ 218 (write_binop ii Xxor x y ea = (write_logical_result ii (x ?? y) ea)) /\ 219 (write_binop ii Xor x y ea = (write_logical_result ii (x || y) ea)) /\ 220 (write_binop ii Xshl x y ea = (write_result_erase_eflags ii (x << w2n y) ea)) /\ 221 (write_binop ii Xshr x y ea = (write_result_erase_eflags ii (x >>> w2n y) ea)) /\ 222 (write_binop ii Xsar x y ea = (write_result_erase_eflags ii (x >> w2n y) ea)) /\ 223 (write_binop ii _ x y ea = failureT)`; 224 225val write_binop_with_carry_def = Define ` 226 (write_binop_with_carry ii Xadc x y cf ea = 227 parT_unit (write_eflag ii X_CF (SOME (2**32 <= w2n x + w2n y + bool2num cf))) 228 (parT_unit (write_eflag ii X_OF NONE) 229 (write_arith_result_no_CF_OF ii (x + y + n2w (bool2num cf)) ea))) /\ 230 (write_binop_with_carry ii Xsbb x y cf ea = 231 parT_unit (write_eflag ii X_CF (SOME (w2n x < w2n y + bool2num cf))) 232 (parT_unit (write_eflag ii X_OF NONE) 233 (write_arith_result_no_CF_OF ii (x - (y + n2w (bool2num cf))) ea))) /\ 234 (write_binop_with_carry ii _ x y cf ea = failureT)`; 235 236(* monops *) 237 238val write_monop_def = Define ` 239 (write_monop ii Xnot x ea = write_ea ii ea (~x)) /\ 240 (write_monop ii Xdec x ea = write_arith_result_no_CF_OF ii (x - 1w) ea) /\ 241 (write_monop ii Xinc x ea = write_arith_result_no_CF_OF ii (x + 1w) ea) /\ 242 (write_monop ii Xneg x ea = 243 parT_unit (write_arith_result_no_CF_OF ii (0w - x) ea) 244 (write_eflag ii X_CF NONE))`; 245 246(* evaluating conditions of eflags *) 247 248val read_cond_def = Define ` 249 (read_cond ii X_ALWAYS = constT T) /\ 250 (read_cond ii X_E = read_eflag ii X_ZF) /\ 251 (read_cond ii X_S = read_eflag ii X_SF) /\ 252 (read_cond ii X_B = read_eflag ii X_CF) /\ 253 (read_cond ii X_NE = seqT (read_eflag ii X_ZF) (\b. constT (~b))) /\ 254 (read_cond ii X_NS = seqT (read_eflag ii X_SF) (\b. constT (~b))) /\ 255 (read_cond ii X_NB = seqT (read_eflag ii X_CF) (\b. constT (~b))) /\ 256 (read_cond ii X_A = seqT 257 (parT (read_eflag ii X_CF) (read_eflag ii X_ZF)) (\(c,z). constT (~c /\ ~z))) /\ 258 (read_cond ii X_NA = seqT 259 (parT (read_eflag ii X_CF) (read_eflag ii X_ZF)) (\(c,z). constT (c \/ z)))`; 260 261(* execute stack operations for non-EIP registers *) 262 263val x86_exec_pop_def = Define ` 264 x86_exec_pop ii rm = 265 seqT (seqT (read_reg ii ESP) (\esp. addT esp (write_reg ii ESP (esp + 4w)))) 266 (\(old_esp,x). seqT (parT (ea_Xrm ii rm) (read_m32 ii old_esp)) 267 (\(ea,w). write_ea ii ea w))`; 268 269val x86_exec_push_def = Define ` 270 x86_exec_push ii imm_rm = 271 (seqT 272 (parT (seqT (ea_Ximm_rm ii imm_rm) (\ea. read_ea ii ea)) 273 (seqT (read_reg ii ESP) (\w. constT (w - 4w)))) 274 (\(w,esp). parT_unit (write_m32 ii esp w) (write_reg ii ESP esp)))`; 275 276(* execute stack operations for EIP register *) 277 278val x86_exec_pop_eip_def = Define ` 279 x86_exec_pop_eip ii = 280 seqT (seqT (read_reg ii ESP) (\esp. addT esp (write_reg ii ESP (esp + 4w)))) 281 (\(old_esp,x). seqT (read_m32 ii old_esp) 282 (\w. write_eip ii w))`; 283 284val x86_exec_push_eip_def = Define ` 285 x86_exec_push_eip ii = 286 (seqT 287 (parT (read_eip ii) 288 (seqT (read_reg ii ESP) (\w. constT (w - 4w)))) 289 (\(w,esp). parT_unit (write_m32 ii esp w) (write_reg ii ESP esp)))`; 290 291(* check whether rm requires a lock, i.e. specifies a memory access *) 292 293(* execution of one instruction *) 294 295val x86_exec_def = Define ` 296 (x86_exec ii (Xbinop binop_name ds) len = bump_eip ii len 297 (if (binop_name = Xadc) \/ (binop_name = Xsbb) then 298 seqT 299 (parT (parT (read_src_ea ii ds) (read_dest_ea ii ds)) 300 (read_eflag ii X_CF)) 301 (\ (((ea_src,val_src),(ea_dest,val_dest)),val_cf). 302 write_binop_with_carry ii binop_name 303 val_dest val_src val_cf ea_dest) 304 else 305 seqT 306 (parT (read_src_ea ii ds) (read_dest_ea ii ds)) 307 (\ ((ea_src,val_src),(ea_dest,val_dest)). 308 write_binop ii binop_name val_dest val_src ea_dest))) /\ 309 (x86_exec ii (Xmonop monop_name rm) len = bump_eip ii len 310 (seqT 311 (seqT (ea_Xrm ii rm) (\ea. addT ea (read_ea ii ea))) 312 (\ (ea_dest,val_dest). 313 write_monop ii monop_name val_dest ea_dest))) /\ 314 (x86_exec ii (Xmul rm) len = bump_eip ii len 315 (seqT 316 (parT (seqT (ea_Xrm ii rm) (\ea. addT ea (read_ea ii ea))) 317 (read_reg ii EAX)) 318 (\ ((ea_src,val_src),eax). 319 parT_unit (write_reg ii EAX (eax * val_src)) 320 (parT_unit (write_reg ii EDX (n2w ((w2n eax * w2n val_src) DIV 2**32))) 321 (erase_eflags ii)) (* here erase_flag is an over approximation *)))) /\ 322 (x86_exec ii (Xdiv rm) len = bump_eip ii len 323 (seqT 324 (parT (seqT (ea_Xrm ii rm) (\ea. addT ea (read_ea ii ea))) 325 (seqT (parT (read_reg ii EAX) (read_reg ii EDX)) 326 (\ (eax,edx). constT (w2n edx * 2**32 + w2n eax)))) 327 (\ ((ea_src,val_src),n). 328 parT_unit (assertT (~(val_src = 0w) /\ n DIV (w2n val_src) < 2**32)) 329 (parT_unit (write_reg ii EAX (n2w (n DIV (w2n val_src)))) 330 (parT_unit (write_reg ii EDX (n2w (n MOD (w2n val_src)))) 331 (erase_eflags ii)))))) /\ 332 (x86_exec ii (Xxadd rm r) len = bump_eip ii len 333 (seqT 334 (parT (seqT (ea_Xrm ii rm) (\ea. addT ea (read_ea ii ea))) 335 (parT (constT (Xea_r r)) (read_reg ii r))) 336 (\ ((ea_dest,val_dest),(ea_src,val_src)). 337 seqT (write_ea ii ea_src val_dest) 338 (\x. write_binop ii Xadd val_src val_dest ea_dest)))) /\ 339 (x86_exec ii (Xxchg rm r) len = 340 (if rm_is_memory_access rm then lockT else I) 341 (bump_eip ii len 342 (if rm = (Xr r) then constT () else 343 (seqT 344 (parT (seqT (ea_Xrm ii rm) (\ea. addT ea (read_ea ii ea))) 345 (parT (constT (Xea_r r)) (read_reg ii r))) 346 (\ ((ea_dest,val_dest),(ea_src,val_src)). 347 (parT_unit (write_ea ii ea_src val_dest) 348 (write_ea ii ea_dest val_src))))))) /\ 349 (x86_exec ii (Xcmpxchg rm r) len = bump_eip ii len 350 (seqT 351 (parT (seqT (ea_Xrm ii rm) (\ea. addT ea (read_ea ii ea))) 352 (read_reg ii EAX)) 353 (\ ((dest_ea,dest_val),acc). 354 parT_unit (write_binop ii Xcmp acc dest_val (Xea_r EAX)) 355 (if acc = dest_val then 356 seqT (read_reg ii r) (\src_val. write_ea ii dest_ea src_val) 357 else 358 write_reg ii EAX dest_val)))) /\ 359 (x86_exec ii (Xpop rm) len = bump_eip ii len (x86_exec_pop ii rm)) /\ 360 (x86_exec ii (Xpush imm_rm) len = bump_eip ii len (x86_exec_push ii imm_rm)) /\ 361 (x86_exec ii (Xcall imm_rm) len = 362 seqT (parT (bump_eip ii len (constT ())) 363 (ea_Ximm_rm ii imm_rm)) (\ (x,ea). 364 seqT (parT (x86_exec_push_eip ii) 365 (read_eip ii)) (\ (x,eip). 366 jump_to_ea ii eip ea))) /\ 367 (x86_exec ii (Xret imm) len = 368 seqT (x86_exec_pop_eip ii ) (\x. 369 seqT (read_reg ii ESP) (\esp. (write_reg ii ESP (esp + imm))))) /\ 370 (x86_exec ii (Xlea ds) len = bump_eip ii len 371 (seqT 372 ((parT (ea_Xsrc ii ds) (ea_Xdest ii ds))) 373 (\ (ea_src,ea_dest). 374 write_ea ii ea_dest (get_ea_address ea_src)))) /\ 375 (x86_exec ii (Xmov c ds) len = bump_eip ii len 376 (seqT 377 ((parT (read_src_ea ii ds) 378 (parT (read_cond ii c) (ea_Xdest ii ds)))) 379 (\ ((ea_src,val_src),(g,ea_dest)). 380 if g then write_ea ii ea_dest val_src else constT ()))) /\ 381 (x86_exec ii (Xdec_byte rm) len = bump_eip ii len 382 (seqT 383 (seqT (ea_Xrm ii rm) (\ea. addT ea (read_ea_byte ii ea))) 384 (\ (ea_src,val_src). 385 parT_unit (write_ea_byte ii ea_src (val_src - 1w)) 386 (erase_eflags ii)))) /\ 387 (x86_exec ii (Xmovzx ds) len = bump_eip ii len 388 (seqT 389 (parT (read_src_ea_byte ii ds) (ea_Xdest ii ds)) 390 (\ ((ea_src,val_src),ea_dest). 391 write_ea ii ea_dest (w2w val_src)))) /\ 392 (x86_exec ii (Xmov_byte ds) len = bump_eip ii len 393 (seqT 394 (parT (read_src_ea_byte ii ds) (ea_Xdest ii ds)) 395 (\ ((ea_src,val_src),ea_dest). 396 write_ea_byte ii ea_dest val_src))) /\ 397 (x86_exec ii (Xcmp_byte ds) len = bump_eip ii len 398 (seqT 399 (parT (read_src_ea_byte ii ds) (read_dest_ea_byte ii ds)) 400 (\ ((ea_src,val_src),(ea_dest,val_dest)). 401 write_binop ii Xcmp (w2w val_dest) (w2w val_src) ea_dest))) /\ 402 (x86_exec ii (Xjcc c imm) len = ( 403 seqT 404 (parT (read_eip ii) (read_cond ii c)) 405 (\ (eip,g). write_eip ii (if g then eip + len + imm else eip + len)))) /\ 406 (x86_exec ii (Xjmp rm) len = ( 407 seqT 408 (seqT (ea_Xrm ii rm) (\ea. read_ea ii ea)) 409 (\new_eip. 410 parT_unit (write_eip ii new_eip) 411 (clear_icache ii)))) /\ 412 (x86_exec ii (Xloop c imm) len = 413 seqT (parT (read_eip ii) ( 414 parT (read_cond ii c) 415 (seqT (read_reg ii ECX) (\ecx. constT (ecx - 1w))))) 416 (\ (eip,guard,new_ecx). 417 parT_unit (write_reg ii ECX new_ecx) 418 (write_eip ii 419 (if ~(new_ecx = 0w) /\ guard 420 then eip + len + imm else eip + len)))) /\ 421 (x86_exec ii (Xpushad) len = bump_eip ii len ( 422 seqT (read_reg ii ESP) (\original_esp. 423 seqT (x86_exec_push ii (Xi_rm (Xr EAX))) (\x. 424 seqT (x86_exec_push ii (Xi_rm (Xr ECX))) (\x. 425 seqT (x86_exec_push ii (Xi_rm (Xr EDX))) (\x. 426 seqT (x86_exec_push ii (Xi_rm (Xr EBX))) (\x. 427 seqT (write_reg ii ESP original_esp) (\x. 428 seqT (x86_exec_push ii (Xi_rm (Xr EBP))) (\x. 429 seqT (x86_exec_push ii (Xi_rm (Xr ESI))) (\x. 430 (x86_exec_push ii (Xi_rm (Xr EDI))))))))))))) /\ 431 (x86_exec ii (Xpopad) len = bump_eip ii len ( 432 seqT (x86_exec_pop ii (Xr EDI)) (\x. 433 seqT (x86_exec_pop ii (Xr ESI)) (\x. 434 seqT (x86_exec_pop ii (Xr EBP)) (\x. 435 seqT (seqT (read_reg ii ESP) (\esp. write_reg ii ESP (esp + 4w))) (\x. 436 seqT (x86_exec_pop ii (Xr EBX)) (\x. 437 seqT (x86_exec_pop ii (Xr EDX)) (\x. 438 seqT (x86_exec_pop ii (Xr ECX)) (\x. 439 seqT (x86_exec_pop ii (Xr EAX)) (\x. constT ()))))))))))`; 440 441val x86_execute_def = Define ` 442 (x86_execute ii (Xprefix Xg1_none g2 i) len = x86_exec ii i len) /\ 443 (x86_execute ii (Xprefix Xlock g2 i) len = lockT (x86_exec ii i len))`; 444 445 446val _ = export_theory (); 447