| /seL4-l4v-10.1.1/seL4/include/arch/x86/arch/64/mode/machine/ |
| H A D | registerset.h | 40 RAX = 2, /* 0x10 */ enumerator in enum:_register
83 [seL4_UnknownSyscall_RAX] = RAX,\
|
| /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,
32 context->registers[RAX] = 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_opsemScript.sml | 331 (parT (read_reg ii RAX) (assertT (~(s = Z8)))))
333 parT_unit (write_reg ii RAX (eax * val_src))
339 (seqT (parT (read_reg ii RAX) (read_reg ii RDX))
343 (parT_unit (write_reg ii RAX (n2w (n DIV (w2n val_src))))
366 (read_reg ii RAX))
368 parT_unit (write_binop ii s Zcmp acc dest_val (Zea_r s RAX))
372 write_reg ii RAX dest_val)))) /\
382 (parT_unit (seqT (read_reg ii RAX) (\rax. assertT (rax = 0w)))
383 (parT_unit (write_reg ii RAX ARB)
|
| H A D | x64_Lib.sml | 234 val old_regs = ["RAX", "RBX", "RCX", "RDX", "RSI", "RDI", "RSP", "RBP"]
298 val _ = x64_test "lea RAX,[R15+4*R13-400] | 4B8D84AF70FEFFFF"
299 [("RAX","dd7685b0d983e708","0f28c87c9005ada0"),
|
| H A D | x64_decoderScript.sml | 142 [RAX;RCX;RDX;RBX;RSP;RBP;RSI;RDI;zR8;zR9;zR10;zR11;zR12;zR13;zR14;zR15]):Zreg`;
146 if name = "RAX" then RAX else
164 if name = "RAX" then Zr RAX else
210 if MEM name ["r64";"m64";"r/m64";"RAX"] then Z64 else
|
| H A D | prog_x64_extraScript.sml | 971 RAX -- R11 are caller saved
983 (zPC pi * ~zR1 RAX * ~zR1 RDI * ^caller_saver_tm * ^callee_saved_tm *
985 (zPC x * zR1 RAX (HD (SNOC (~0w) (MAP w2w input))) * ~zR1 RDI *
991 (zPC po * ~zR1 RAX * zR1 RDI (w2w c) * ^caller_saver_tm * ^callee_saved_tm *
993 (zPC x * ~zR1 RAX * ~zR1 RDI * ^caller_saver_tm * ^callee_saved_tm *
|
| 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_x64Script.sml | 204 (zR 0w = zR1 RAX) /\
1190 (zR1 RAX rax * zR1 RBX rbx * zR1 RCX rcx * zR1 RDX rdx *
1193 (zR1 RAX ARB * zR1 RBX ARB * zR1 RCX ARB * zR1 RDX ARB *
|
| H A D | prog_x64Lib.sml | 30 [("RAX","r0"), ("RCX","r1"), ("RDX","r2"), ("RBX","r3"),
|
| /seL4-l4v-10.1.1/seL4/include/arch/x86/arch/64/mode/fastpath/ |
| H A D | fastpath.h | 232 : "c" (&cur_thread->tcbArch.tcbContext.registers[RAX]),
276 : "r"(&cur_thread->tcbArch.tcbContext.registers[RAX]),
|
| /seL4-l4v-10.1.1/seL4/src/arch/x86/64/ |
| H A D | traps.S | 626 # RAX : syscall number
653 push %rax # save RAX (syscall number)
|
| /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
165 0 => RAX
282 RAX => 0
376 RAX => "RAX"
478 "RAX" => RAX
2479 val ea_acc = Zea_r(size,RAX)
2494 val ea_eax = Zea_r(size,RAX)
2512 val ea_eax = Zea_r(size,RAX)
[all...] |
| H A D | x64Script.sml | 8 [("RAX",[]),("RCX",[]),("RDX",[]),("RBX",[]),("RSP",[]),("RBP",[]),
4513 LC("RAX",CTy"Zreg")])]),
4524 TP[Var("size",CTy"Zsize"),LC("RAX",CTy"Zreg")]),
4585 TP[Var("size",CTy"Zsize"),LC("RAX",CTy"Zreg")]),
4876 TP[Var("size",CTy"Zsize"),LC("RAX",CTy"Zreg")]),
4901 LC("RAX",CTy"Zreg")])]),
4932 TP[Var("size",CTy"Zsize"),LC("RAX",CTy"Zreg")]),
5006 LC("RAX",
6189 LC("RAX",
6589 LC("RAX",CT
[all...] |
| H A D | x64.sig | 13 = RAX | RCX | RDX | RBX | RSP | RBP | RSI | RDI | zR8 | zR9 | zR10
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/step/ |
| H A D | x64_stepLib.sml | 761 [[`r` |-> ``RAX``], [`r` |-> ``RCX``], [`r` |-> ``RDX``], [`r` |-> ``RBX``],
769 [[`r` |-> ``RAX``], [`r` |-> ``RCX``], [`r` |-> ``RDX``], [`r` |-> ``RBX``],
|