/seL4-l4v-10.1.1/seL4/src/arch/x86/64/ |
H A D | head.S | 73 movl $boot_pml4, %edi 77 movl %edx, (%edi) 78 addl $4, %edi 81 movl $boot_pdpt, %edi 84 movl %edx, (%edi) 85 addl $4, %edi 89 movl $boot_pdpt, %edi 94 movl %edx, (%edi) 95 movl %ebx, 4(%edi) 102 addl $8, %edi [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 | 63 seL4_Word edi; member in struct:__anon210::__anon211
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/32/ |
H A D | head.S | 56 movl %eax, %edi /* multiboot_magic */ 68 pushl %edi /* 1st parameter: multiboot_magic */ 74 popl %edi 81 pushl %edi /* 1st parameter: multiboot_magic */
|
H A D | traps.S | 30 pushl %edi; \ 369 popl %edi 421 popl %edi 438 movl %esp, %edi 439 addl $68, %edi # EDI contains ESP when exception happened 451 pushl %edi 474 pushl %edi 520 pushl %edi # save EDI (message register)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/just-in-time/ |
H A D | jit_basicScript.sml | 26 val ((th2,_,_),_) = spec (x86_encode "lea edi,[ebp+4]") 49 ~xR EAX * xR EDI edi * xPC eip * xSTACK2 EBP (x::xs,l)`` 61 val ((th1,_,_),_) = spec (x86_encode "mov [edi-4],eax") 62 val ((th2,_,_),_) = spec (x86_encode "lea ebp,[edi-4]") 64 val th = Q.INST [`df`|->`{edi-4w}`] (DISCH_ALL th) 69 val th = SPEC_BOOL_FRAME_RULE th ``ALIGNED edi`` 70 val th = SPEC_FRAME_RULE th ``xLIST edi xs * xSPACE (edi-4w) l`` 79 \\ Q.EXISTS_TAC `edi-4w` 82 val th = HIDE_PRE_RULE ``xM (edi [all...] |
H A D | jit_opsScript.sml | 20 edi - point to top of rest of stack 24 (* sub is 2B07 i.e. x86_encode "sub eax,[edi]" *) 61 SEP_EXISTS edi. xR EAX x * xR EDI edi * cond (ALIGNED edi) * 62 xLIST edi xs * xSPACE edi l)`; 144 val th = Q.INST [`df`|->`{edi}`] (DISCH_ALL th) 155 val th = Q.INST [`df`|->`{edi}`] (DISCH_ALL th) 190 val ((th1,_,_),_) = spec (x86_encode "mov eax,[edi]") [all...] |
H A D | jit_incrementalScript.sml | 28 [(1,"eax"),(6,"ebx"),(5,"ecx"),(2,"edx"),(3,"edi"),(4,"esi"),(7,"ebp")] 34 r3 edi - preserved (rest of stack) 176 r3 edi - preserved (rest of stack) 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 1731 val th = DISCH ``ALIGNED edi`` th 1749 val th = Q.SPEC `xLIST edi xs * xSPACE edi l` (MATCH_MP SPEC_FRAME th) 1804 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`ebx`,`edi`,`edx`,`x`]) 1820 \\ Q.EXISTS_TAC `edi` [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/libpolyml/ |
H A D | x86assembly_gas32.S | 35 %%edi: General register. 123 pushl %edi 136 movl Arg_SaveRDI(%ebp),%edi 149 movl %edi,Arg_SaveRDI(%ebp) 156 popl %edi 199 movl %edi,%eax # On X86_64 the argument is passed in %edi
|
H A D | x86assembly_masm32.S | 29 ; edi: General register. 96 push edi 109 mov edi,[ArgVector.SaveRDI+ebp] 121 mov [ArgVector.SaveRDI+ebp],edi 128 pop edi
|
/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. 111 We use esi to hold the argument data pointer and edi to save the ML stack pointer 150 then [moveRR{source=esp, output=edi}] (* Needed if we have to load from the stack. *) 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} ] 181 PushToStack(MemoryArg{base=edi, offset=4, index=NoIndex}), pushR ebx, pushR eax, 226 if isX64 then (r11, r13) else (ecx, edi) 256 | (X64Unix, 1) => [ moveRR{source=eax, output=edi} ] [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/l3-machine-code/x64/decompiler/ |
H A D | x64_decomp_demoScript.sml | 52 (* 20: *) 89c7 (* mov %eax,%edi *)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
H A D | lisp_finalScript.sml | 336 prog_x86Lib.x86_tools "test" [QUOTE (x86_encodeLib.x86_encode "push edi")] 340 val post = ``xSTACK (esp-4w) [edi] * xR EDI edi * xR ESP (esp - 0x4w) * xPC (p + 0x1w)`` 346 val pre = ``xSTACK (esp-4w) [w] * xR EDI edi * xR ESP esp * xPC p`` 357 prog_x86Lib.x86_tools "test" [QUOTE (x86_encodeLib.x86_encode "mov edi, [esp]")] 378 prog_x86Lib.x86_tools "test" [QUOTE (x86_encodeLib.x86_encode "pop edi")] 399 val post = ``(let (eax,ecx,edi,esi,ebp,dh,h,df,f,dm,m,dg,g) = 429 val post = ``SEP_EXISTS edi dg g dm m dh h. xR EDI edi * xSTRING edi (sexp2strin [all...] |
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")]
|
H A D | lisp_parseScript.sml | 18 [(3,"eax"),(4,"ecx"),(5,"edx"),(6,"ebx"),(7,"edi"),(8,"esi"),(9,"ebp")] 3129 ("7","edi"),("8","esi"),("9","ebp")])
|
/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/instruction-set-models/x86/ |
H A D | prog_x86Lib.sml | 326 val th = x86_spec "883E"; (* mov_byte [esi],edi *) 327 val th = x86_spec "0FB63E"; (* mov_byte edi,[esi] *) 344 val s = (x86_encode "mov [edi+400],3477")
|
H A D | x86_Lib.sml | 174 val th = x86_step "8B3E"; (* mov edi,[esi] *) 186 val th = x86_step "893E"; (* mov [esi],edi *) 187 val th = x86_step "8B3E"; (* mov edi,[esi] *)
|
H A D | x86_decoderScript.sml | 512 val th = EVAL ``x86_decode(bytebits "893E")``; (* mov [esi],edi *) 513 val th = EVAL ``x86_decode(bytebits "8B3E")``; (* mov edi,[esi] *) 566 val th = EVAL ``x86_decode(bytebits "0FB1F8")``; (* cmpxchg eax, edi *)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
H A D | codegen_x86Lib.sml | 9 (4,"edi"), (5,"esi"), (6,"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")]
|