Searched refs:ebp (Results 1 - 25 of 29) sorted by relevance

12

/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Dx86assembly_gas32.S33 %%ebp: Points to memory used for extra registers
104 movb $index,Arg_ReturnReason(%ebp); \
119 pushl %ebp # Standard entry sequence
120 movl 8(%esp),%ebp # Address of argument vector
121 movl %esp,Arg_SaveCStack(%ebp)
126 movl Arg_StackPtr(%ebp),%esp
127 movl Arg_ExceptionPacket(%ebp),%eax
130 FRSTOR Arg_SaveFP(%ebp)
131 movl Arg_SaveRAX(%ebp),%eax # Load the registers
132 movl Arg_SaveRBX(%ebp),
[all...]
H A Dx86assembly_masm32.S27 ; ebp: Points to memory used for extra registers
82 ; The argument is the address of the MemRegisters struct and goes into ebp.
92 push ebp ; Standard entry sequence
93 mov ebp,[8+esp] ; Address of argument vector
94 mov [ArgVector.SaveCStack+ebp],esp
99 mov esp,[ArgVector.StackPtr+ebp]
100 mov eax,[ArgVector.ExceptionPacket+ebp]
103 frstor [ArgVector.SaveFP+ebp]
104 mov eax,[ArgVector.SaveRAX+ebp]
105 mov ebx,[ArgVector.SaveRBX+ebp]
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/x86/
H A Ddarwin.S44 pushl %ebp
46 movl %esp,%ebp
50 movl 16(%ebp),%ecx
57 pushl 12(%ebp)
59 call *8(%ebp)
64 call *28(%ebp)
67 movl 20(%ebp),%ecx
73 cmpl $0,24(%ebp)
128 movl 24(%ebp),%ecx
134 movl 24(%ebp),
[all...]
H A Dfreebsd.S44 pushl %ebp
46 movl %esp,%ebp
49 movl 16(%ebp),%ecx
58 pushl 12(%ebp)
60 call *8(%ebp)
65 call *28(%ebp)
68 movl 20(%ebp),%ecx
74 cmpl $0,24(%ebp)
131 movl 24(%ebp),%ecx
137 movl 24(%ebp),
[all...]
H A Dsysv.S44 pushl %ebp
46 movl %esp,%ebp
49 movl 16(%ebp),%ecx
58 pushl 12(%ebp)
60 call *8(%ebp)
65 call *28(%ebp)
68 movl 20(%ebp),%ecx
74 cmpl $0,24(%ebp)
129 movl 24(%ebp),%ecx
135 movl 24(%ebp),
[all...]
H A Dwin32.S241 lea edx, [ebp - 24]
242 mov [ebp - 12], edx ;; resp
243 lea edx, [ebp + 8]
246 lea edx, [ebp - 12]
250 mov ecx, [ebp - 12]
340 lea edx, [ebp + 12]
351 lea edx, [ebp + 8]
354 lea edx, [ebp - 24]
359 lea ecx, [ebp - 24]
433 lea edx, [ebp
[all...]
/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.h64 seL4_Word ebp; member in struct:__anon210::__anon211
/seL4-l4v-10.1.1/HOL4/examples/machine-code/just-in-time/
H A Djit_basicScript.sml25 val ((th1,_,_),_) = spec (x86_encode "mov eax,[ebp]")
26 val ((th2,_,_),_) = spec (x86_encode "lea edi,[ebp+4]")
28 val th = Q.INST [`df`|->`{ebp}`] (DISCH_ALL th)
33 val th = SPEC_BOOL_FRAME_RULE th ``ALIGNED ebp``
34 val th = HIDE_POST_RULE ``xM ebp`` th
35 val th = SPEC_FRAME_RULE th ``xLIST (ebp+4w) xs * xSPACE ebp l``
37 xR EBP ebp * xPC (eip + 0x6w) * xSTACK (x::xs,SUC l,p,ns)``
42 \\ Q.EXISTS_TAC `ebp + 4w`
47 val th = EXISTS_PRE `ebp` t
[all...]
H A Djit_incrementalScript.sml28 [(1,"eax"),(6,"ebx"),(5,"ecx"),(2,"edx"),(3,"edi"),(4,"esi"),(7,"ebp")]
38 r7 ebp - pointer to j map and temp memory
180 r7 ebp - unchanged (pointer to j map and temp memory)
194 val _ = teach_compiler "m" "lea esi, [8 * ecx + ebp]"
1729 ``x86_inc (eax,edx,edi,esi,ecx,ebx,ebp,dh,h,df,f,dg,g) =
1730 (eax,edx,edi,w,0w,ebx,ebp,dh,h3,df,f3,dg,g)`` x86_inc_th
1732 val th = DISCH ``state_inv cs dh h dg g df f ebp j /\ n < LENGTH cs /\
1733 ((h (ebp - 0x24w) = 0w) ==> cont_jump j pi cs esi (n2w n))`` th
1814 \\ Q.EXISTS_TAC `ebp`
1829 val th = QGENL [`w`,`pi`,`j`,`h3`,`h`,`g`,`f3`,`f`,`cp`,`edi`,`ebp`,`d
[all...]
H A Djit_codegenScript.sml32 [(1,"eax"),(6,"ebx"),(5,"ecx"),(2,"edx"),(3,"edi"),(4,"esi"),(7,"ebp")]
/seL4-l4v-10.1.1/seL4/libsel4/arch_include/x86/sel4/arch/
H A Dtypes.h47 seL4_Word eax, ebx, ecx, edx, esi, edi, ebp; member in struct:seL4_VCPUContext_
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/
H A DX86FOREIGNCALL.sml110 ebx, edi, esi, ebp and esp are saved by the called function.
145 if isX64 then [storeMemory(r15, ebp, memRegLocalMPointer)] (* Save heap ptr *)
156 storeMemory(esp, ebp, memRegStackPtr), (* Save ML stack and switch to C stack. *)
157 loadMemory(esp, ebp, memRegCStackPtr), (*moveRR{source=ebp, output=esp},*) (* Load the saved C stack pointer. *)
163 (X64Unix, 0) => [ loadMemory(edi, ebp, memRegThreadSelf) ]
164 | (X64Unix, 1) => [ loadMemory(edi, ebp, memRegThreadSelf), moveRR{source=eax, output=esi} ]
166 [ loadMemory(edi, ebp, memRegThreadSelf), moveRR{source=eax, output=esi}, moveRR{source=ebx, output=edx} ]
168 [ loadMemory(edi, ebp, memRegThreadSelf), moveRR{source=eax, output=esi}, moveRR{source=ebx, output=edx}, moveRR{source=r8, output=ecx} ]
169 | (X64Win, 0) => [ loadMemory(ecx, ebp, memRegThreadSel
[all...]
H A DX86CODESIG.sml39 and edi: genReg and esi: genReg and esp: genReg and ebp: genReg value
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/
H A Dprog_x86Lib.sml149 val ebp = mk_var("ebp",``:word32``) value
150 fun access_ebp tm = (tm = ebp) orelse
151 (can (match_term ``(v:word32) - n2w n``) tm andalso (ebp = (cdr o car) tm))
158 val th = DISCH ``ALIGNED ebp`` th
308 val th = x86_spec "89EE"; (* mov esi,ebp *)
311 val th = x86_spec "89EA"; (* mov edx,ebp *)
313 val th = x86_spec "89CD"; (* mov ebp,ecx *)
314 val th = x86_spec "45"; (* inc ebp *)
317 val th = x86_spec "8B2A"; (* mov ebp,[ed
[all...]
H A Dx86_Lib.sml220 val th = x86_step "FFB42DEA000000"; (* push dword [ebp + ebp + 234] *)
223 val th = x86_step "FF74AD02"; (* push dword [ebp + 4*ebp + 2] *)
224 val th = x86_step "FF746D2D"; (* push dword [ebp + 2*ebp + 45] *)
H A Dprog_x86Script.sml1028 ``(ALIGNED ebp ==>
1029 SPEC X86_MODEL (q1 * xR EBP ebp * xM (ebp - n2w n) x) c
1030 (q2 * xR EBP ebp * xM (ebp - n2w n) y)) ==>
1033 SPEC X86_MODEL (q1 * xSTACK ebp (xs ++ [x] ++ ys))
1034 c (q2 * xSTACK ebp (xs ++ [y] ++ ys))``,
H A Dx86_decoderScript.sml541 val th = EVAL ``x86_decode(bytebits "FF74AD02")``; (* push dword [ebp + 4*ebp + 2] *)
542 val th = EVAL ``x86_decode(bytebits "FF746D2D")``; (* push dword [ebp + 2*ebp + 45] *)
543 val th = EVAL ``x86_decode(bytebits "FFB42DEA000000")``; (* push dword [ebp + ebp + 234] *)
567 val th = EVAL ``x86_decode(bytebits "0FB1441500")``; (* cmpxchg [ebp + edx], eax *)
/seL4-l4v-10.1.1/seL4/src/arch/x86/32/
H A Dtraps.S29 pushl %ebp; \
370 popl %ebp
422 popl %ebp
473 pushl %ebp
519 pushl %ebp # save EBP (message register)
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/demo/
H A Dcompiler_demoScript.sml108 [(3,"eax"),(4,"ecx"),(5,"edx"),(6,"ebx"),(7,"edi"),(8,"esi"),(9,"ebp")]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/
H A Dcodegen_x86Lib.sml9 (4,"edi"), (5,"esi"), (6,"ebp")];
22 fun s i = "[ebp - " ^ int_to_string (4 * i) ^ "]"
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/
H A Dlisp_finalScript.sml399 val post = ``(let (eax,ecx,edi,esi,ebp,dh,h,df,f,dm,m,dg,g) =
400 arm_print_sexp (eax,w,ebp,dh,h,df,f,dm,m,dg,g)
403 xMEMORY dm m * xR EAX eax * xR EBP ebp * ~xR EBX * xR ECX ecx *
416 (SND (SND (arm_print_sexp (eax,w,ebp,dh,h,df,f,dm,m,dg,g)))))`
428 val th = Q.INST [`eax`|->`w1`,`ebp`|->`r9`,`r1`|->`w`] th
H A DdivideScript.sml12 [(3,"eax"),(4,"ecx"),(5,"edx"),(6,"ebx"),(7,"edi"),(8,"esi"),(10,"ebp")]
H A Dlisp_equalScript.sml18 [(3,"eax"),(4,"ecx"),(5,"edx"),(6,"ebx"),(7,"edi"),(8,"esi"),(9,"ebp")]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/
H A Darm_improved_gcScript.sml19 [(1,"eax"),(2,"ecx"),(3,"edx"),(4,"ebx"),(5,"edi"),(6,"esi"),(7,"ebp")]

Completed in 222 milliseconds

12