Searched refs:eip (Results 1 - 16 of 16) sorted by relevance

/seL4-l4v-10.1.1/seL4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/
H A Dtypes.h28 seL4_Word eip, esp, eflags, eax, ebx, ecx, edx, esi, edi, ebp; member in struct:seL4_UserContext_
H A Ddeprecated.h65 seL4_Word eip; member in struct:__anon210::__anon211
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/
H A Dx86_opsemScript.sml107 (* jump_to_ea updates eip according to procedure call *)
110 (jump_to_ea ii eip (Xea_i i) = write_eip ii (eip + i)) /\
111 (jump_to_ea ii eip (Xea_r r) = seqT (read_reg ii r) (write_eip ii)) /\
112 (jump_to_ea ii eip (Xea_m a) = seqT (read_m32 ii a) (write_eip ii))`;
117 (call_dest_from_ea ii eip (Xea_i i) = constT (eip + i)) /\
118 (call_dest_from_ea ii eip (Xea_r r) = read_reg ii r) /\
119 (call_dest_from_ea ii eip (Xea_m a) = read_m32 ii a)`;
126 (* eip modifier
[all...]
H A Dx86_Script.sml27 let e = XREAD_EIP s in (* read eip *)
H A Dprog_x86Lib.sml49 val result = rs2 @ fs2 @ ws2 @ bs2 @ [``XREAD_EIP s = eip``]
103 val pre = mk_star (pre,``xPC eip``)
218 val tm = ``SPEC X86_MODEL pre {(eip,(c,w))} post``
H A Dx86_seq_monadScript.sml16 (word32) # (* - eip *)
158 (* eip reads/writes always succeed. *)
H A Dprog_x86Script.sml538 SPECL [``CODE_POOL X86_INSTR {(eip,c)} * p``,
539 ``CODE_POOL X86_INSTR {(eip,c)} * q``]) IMP_X86_SPEC_LEMMA2);
937 (xR ESI esi * xPC eip * xBYTE_MEMORY_X df f)
938 {(eip,[0xFFw;0xE6w],T)}
/seL4-l4v-10.1.1/HOL4/examples/machine-code/just-in-time/
H A Djit_basicScript.sml37 xR EBP ebp * xPC (eip + 0x6w) * xSTACK (x::xs,SUC l,p,ns)``
49 ~xR EAX * xR EDI edi * xPC eip * xSTACK2 EBP (x::xs,l)``
75 ~xR EDI * xPC (eip + 0x6w) * xSTACK2 EBP (x::xs,l) * ~xR EAX``
86 xPC eip * xSTACK (x::xs,SUC l,p,ns) * ~xR EBP``
H A Djit_incrementalScript.sml1711 val (th,goal) = SPEC_STRENGTHEN_RULE th ``xPC eip * X86_STACK (esp,w::xs,n) * ~xR ESI``
1717 val (th,goal) = SPEC_WEAKEN_RULE th ``xPC (eip+1w) * X86_STACK (esp+4w,xs,n+1) * xR ESI w``
1743 val th = Q.INST [`eip`|->`p`] th
1759 SEP_EXISTS dh dg df jw g h f j eip.
1762 xR EBP jw * ~xS * xPC eip * xCODE (xCODE_SET df f) * X86_STACK (esp,[],1) *
1763 cond (state_inv cs dh h dg g df f jw j /\ (j p = SOME eip))`;
1776 SEP_EXISTS dh dg df jw g h f j eip bs.
1779 xR EBP jw * ~xS * xPC eip * xCODE (xCODE_SET df f) * X86_STACK (esp,[],1) *
1781 ENCODES_JUMP eip t j bs /\ BYTES_IN_MEM eip d
[all...]
H A Djit_opsScript.sml494 xPC eip * xR ESP esp * ~xS * ~xM (esp - 0x4w) *
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/
H A Dlisp_opsScript.sml260 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS``
261 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * xS1 X_ZF (SOME (isDot x)) * ~xS1 X_PF * ~xS1 X_SF * ~xS1 X_AF * ~xS1 X_OF * ~xS1 X_CF``
263 val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th)
264 val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm
324 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS``
325 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * xS1 X_ZF (SOME ~(isSym x)) * ~xS1 X_PF * ~xS1 X_SF * ~xS1 X_AF * ~xS1 X_OF * ~xS1 X_CF``
327 val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th)
328 val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm
513 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip``
514 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip``
[all...]
H A Dlisp_evalScript.sml28 INST [``limit:num``|->``l:num``,mk_var("eip",``:word32``) |-> mk_var("p",``:word32``)]
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Dx86_dep.cpp679 pc = (byte*)context->uc_mcontext->ss.eip;
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_opsScript.sml489 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th)
530 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th)
571 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th)
599 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th)
639 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th)
673 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th)
703 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th)
785 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th)
826 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th)
851 val tm = find_term (can (match_term ``zPC (eip
[all...]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/
H A Dderive_specsLib.sml331 val i = [mk_var("eip",``:word32``) |-> mk_var("p",``:word32``),
/seL4-l4v-10.1.1/HOL4/examples/machine-code/decompiler/
H A DdecompilerLib.sml389 mk_var("eip",``:word32``) |-> mk_var("p",``:word32``),

Completed in 137 milliseconds