| /seL4-l4v-10.1.1/seL4/include/arch/x86/arch/64/mode/machine/ |
| H A D | registerset.h | 42 RBP = 4, /* 0x20 */ enumerator in enum:_register
89 [seL4_UnknownSyscall_RBP] = RBP,\
|
| /seL4-l4v-10.1.1/seL4/src/arch/x86/64/machine/ |
| H A D | registerset.c | 22 FaultIP, RSP, FLAGS, RAX, RBX, RCX, RDX, RSI, RDI, RBP,
38 context->registers[RBP] = 0;
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
| H A D | x64_coretypesScript.sml | 16 val _ = Hol_datatype `Zreg = RAX | RBX | RCX | RDX | RSP | RBP | RSI | RDI |
40 ``ALL_DISTINCT ([RAX;RCX;RDX;RBX;RSP;RBP;RSI;RDI;zR8;zR9;zR10;zR11;
|
| H A D | x64_decoderScript.sml | 142 [RAX;RCX;RDX;RBX;RSP;RBP;RSI;RDI;zR8;zR9;zR10;zR11;zR12;zR13;zR14;zR15]):Zreg`;
153 if b2reg g "REX.B" "Base" = RBP then (* the special case indicated by "[*]" *)
155 if g "Mod" = [T;F] then Zm scaled_index (SOME RBP) (sw2sw ((b2w g "disp8"):word8)) else
156 (* g "Mod" = [F;T] *) Zm scaled_index (SOME RBP) (sw2sw ((b2w g "disp32"):word32))
491 (dsize = Z8) /\ ~(FILTER (\x. MEM x [RSP;RBP;RSI;RDI]) xs = [])`;
|
| H A D | x64_Lib.sml | 234 val old_regs = ["RAX", "RBX", "RCX", "RDX", "RSI", "RDI", "RSP", "RBP"]
306 ("RBP","00007fff5fbff2a0","00007fff5fbff2a0"),
|
| H A D | x64_encodeLib.sml | 102 zip ["RAX","RCX","RDX","RBX","RSP","RBP","RSI","RDI"] (add_reg_type 64 [0,1,2,3,4,5,6,7]) @
|
| H A D | prog_x64Lib.sml | 31 ("RSP","r4"), ("RBP","r5"), ("RSI","r6"), ("RDI","r7"),
|
| H A D | prog_x64_extraScript.sml | 970 RBP, R12 -- R15 are callee saved
|
| H A D | prog_x64Script.sml | 209 (zR 5w = zR1 RBP) /\
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/ |
| H A D | x64.sml | 13 = RAX | RCX | RDX | RBX | RSP | RBP | RSI | RDI | zR8 | zR9 | zR10
170 | 5 => RBP
287 | RBP => 5
381 | RBP => "RBP"
483 | "RBP" => RBP
934 (if have_rex orelse (not(Set.mem(r,[RSP,RBP,RSI,RDI])))
952 (if have_rex orelse (not(Set.mem(r,[RSP,RBP,RSI,RDI])))
2550 ((!REG),Cast.ZregToNat RSP,Map.lookup((!REG),Cast.ZregToNat RBP)))
[all...] |
| H A D | x64.sig | 13 = RAX | RCX | RDX | RBX | RSP | RBP | RSI | RDI | zR8 | zR9 | zR10
|
| H A D | x64Script.sml | 8 [("RAX",[]),("RCX",[]),("RDX",[]),("RBX",[]),("RSP",[]),("RBP",[]),
652 SL[LC("RSP",CTy"Zreg"),LC("RBP",CTy"Zreg"),
703 SL[LC("RSP",CTy"Zreg"),LC("RBP",CTy"Zreg"),
4720 (Call("x64_pop",ATy(qTy,qTy),Call("Zr",CTy"Zrm",LC("RBP",CTy"Zreg"))),
4729 LC("RBP",CTy"Zreg")))])))
5905 ITE(EQ(Var("base",CTy"Zreg"),LC("RBP",CTy"Zreg")),
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
| H A D | x86assembly_masm64.S | 123 ; that. RBP needs to be the original argument because we need to be able to modify
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/step/ |
| H A D | x64_stepLib.sml | 138 [``RSP``, ``RBP``, ``RSI``, ``RDI``])
762 [`r` |-> ``RSP``], [`r` |-> ``RBP``], [`r` |-> ``RSI``], [`r` |-> ``RDI``]]
770 [`r` |-> ``RSP``], [`r` |-> ``RBP``], [`r` |-> ``RSI``], [`r` |-> ``RDI``]]
|
| H A D | x64_stepScript.sml | 819 `!r b. (RexReg (b, r) = RBP) = ~b /\ (r = 5w)`,
|