/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | x86assembly_gas32.S | 33 %%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 D | x86assembly_masm32.S | 27 ; 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 D | darwin.S | 44 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 D | freebsd.S | 44 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 D | sysv.S | 44 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 D | win32.S | 241 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 D | types.h | 28 seL4_Word eip, esp, eflags, eax, ebx, ecx, edx, esi, edi, ebp; member in struct:seL4_UserContext_
|
H A D | deprecated.h | 64 seL4_Word ebp; member in struct:__anon210::__anon211
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/just-in-time/ |
H A D | jit_basicScript.sml | 25 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 D | jit_incrementalScript.sml | 28 [(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 D | jit_codegenScript.sml | 32 [(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 D | types.h | 47 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 D | X86FOREIGNCALL.sml | 110 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 D | X86CODESIG.sml | 39 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 D | prog_x86Lib.sml | 149 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 D | x86_Lib.sml | 220 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 D | prog_x86Script.sml | 1028 ``(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 D | x86_decoderScript.sml | 541 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 D | traps.S | 29 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 D | compiler_demoScript.sml | 108 [(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 D | codegen_x86Lib.sml | 9 (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 D | lisp_finalScript.sml | 399 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 D | divideScript.sml | 12 [(3,"eax"),(4,"ecx"),(5,"edx"),(6,"ebx"),(7,"edi"),(8,"esi"),(10,"ebp")]
|
H A D | lisp_equalScript.sml | 18 [(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 D | arm_improved_gcScript.sml | 19 [(1,"eax"),(2,"ecx"),(3,"edx"),(4,"ebx"),(5,"edi"),(6,"esi"),(7,"ebp")]
|