include "../../../arch/x64/Vale.X64.InsBasic.vaf" include "../../../arch/x64/Vale.X64.InsMem.vaf" include "../../../arch/x64/Vale.X64.InsStack.vaf" include "../../../arch/x64/Vale.X64.InsVector.vaf" module Vale.X64.Stack #verbatim{:interface}{:implementation} //open Vale.Def.Opaque_s open FStar.Seq open Vale.Def.Words_s open Vale.Def.Words.Seq_s open Vale.Def.Types_s open Vale.Arch.Types //open Vale.AES.GCM_helpers open Vale.X64.Machine_s open Vale.X64.Memory open Vale.X64.Stack_i open Vale.X64.State open Vale.X64.Decls open Vale.X64.InsBasic open Vale.X64.InsMem open Vale.X64.InsStack open Vale.X64.InsVector open Vale.X64.QuickCode open Vale.X64.QuickCodes open Vale.X64.CPU_Features_s #reset-options "--z3rlimit 30" #endverbatim procedure Callee_save_registers(inline win:bool) {:public} {:quick} requires rsp == init_rsp(stack); // This function should only be called in the prolog, at the very beginning of the function reads rbx; rbp; rdi; rsi; r12; r13; r14; r15; xmm6; xmm7; xmm8; xmm9; xmm10; xmm11; xmm12; xmm13; xmm14; xmm15; modifies stack; rsp; rax; stackTaint; requires sse_enabled; ensures forall(i) (old(valid_src_stack64(i, stack)) && rsp + (if win then 224 else 64) <= i) ==> load_stack64(i, stack) == old(load_stack64(i, stack)); rbx == load_stack64(rsp, stack); rbp == load_stack64(rsp + 8, stack); rdi == load_stack64(rsp + 16, stack); rsi == load_stack64(rsp + 24, stack); r12 == load_stack64(rsp + 32, stack); r13 == load_stack64(rsp + 40, stack); r14 == load_stack64(rsp + 48, stack); r15 == load_stack64(rsp + 56, stack); win ==> hi64(xmm6) == load_stack64(rsp + 64, stack); win ==> lo64(xmm6) == load_stack64(rsp + 72, stack); win ==> hi64(xmm7) == load_stack64(rsp + 80, stack); win ==> lo64(xmm7) == load_stack64(rsp + 88, stack); win ==> hi64(xmm8) == load_stack64(rsp + 96, stack); win ==> lo64(xmm8) == load_stack64(rsp + 104, stack); win ==> hi64(xmm9) == load_stack64(rsp + 112, stack); win ==> lo64(xmm9) == load_stack64(rsp + 120, stack); win ==> hi64(xmm10) == load_stack64(rsp + 128, stack); win ==> lo64(xmm10) == load_stack64(rsp + 136, stack); win ==> hi64(xmm11) == load_stack64(rsp + 144, stack); win ==> lo64(xmm11) == load_stack64(rsp + 152, stack); win ==> hi64(xmm12) == load_stack64(rsp + 160, stack); win ==> lo64(xmm12) == load_stack64(rsp + 168, stack); win ==> hi64(xmm13) == load_stack64(rsp + 176, stack); win ==> lo64(xmm13) == load_stack64(rsp + 184, stack); win ==> hi64(xmm14) == load_stack64(rsp + 192, stack); win ==> lo64(xmm14) == load_stack64(rsp + 200, stack); win ==> hi64(xmm15) == load_stack64(rsp + 208, stack); win ==> lo64(xmm15) == load_stack64(rsp + 216, stack); { inline if (win) { PushXmm(xmm15, rax); PushXmm(xmm14, rax); PushXmm(xmm13, rax); PushXmm(xmm12, rax); PushXmm(xmm11, rax); PushXmm(xmm10, rax); PushXmm(xmm9, rax); PushXmm(xmm8, rax); PushXmm(xmm7, rax); PushXmm(xmm6, rax); } Push(r15); Push(r14); Push(r13); Push(r12); Push(rsi); Push(rdi); Push(rbp); Push(rbx); } procedure Callee_restore_registers( inline win:bool, ghost old_xmm6:quad32, ghost old_xmm7:quad32, ghost old_xmm8:quad32, ghost old_xmm9:quad32, ghost old_xmm10:quad32, ghost old_xmm11:quad32, ghost old_xmm12:quad32, ghost old_xmm13:quad32, ghost old_xmm14:quad32, ghost old_xmm15:quad32) {:public} {:quick} requires sse_enabled; forall(i) rsp <= i <= rsp + (if win then 216 else 56) ==> valid_stack_slot64(i, stack, Public, stackTaint); rsp >= init_rsp(stack) - 4096; rsp + (if win then 224 else 64) <= init_rsp(stack); win ==> hi64(old_xmm6) == load_stack64(rsp + 64, stack); win ==> lo64(old_xmm6) == load_stack64(rsp + 72, stack); win ==> hi64(old_xmm7) == load_stack64(rsp + 80, stack); win ==> lo64(old_xmm7) == load_stack64(rsp + 88, stack); win ==> hi64(old_xmm8) == load_stack64(rsp + 96, stack); win ==> lo64(old_xmm8) == load_stack64(rsp + 104, stack); win ==> hi64(old_xmm9) == load_stack64(rsp + 112, stack); win ==> lo64(old_xmm9) == load_stack64(rsp + 120, stack); win ==> hi64(old_xmm10) == load_stack64(rsp + 128, stack); win ==> lo64(old_xmm10) == load_stack64(rsp + 136, stack); win ==> hi64(old_xmm11) == load_stack64(rsp + 144, stack); win ==> lo64(old_xmm11) == load_stack64(rsp + 152, stack); win ==> hi64(old_xmm12) == load_stack64(rsp + 160, stack); win ==> lo64(old_xmm12) == load_stack64(rsp + 168, stack); win ==> hi64(old_xmm13) == load_stack64(rsp + 176, stack); win ==> lo64(old_xmm13) == load_stack64(rsp + 184, stack); win ==> hi64(old_xmm14) == load_stack64(rsp + 192, stack); win ==> lo64(old_xmm14) == load_stack64(rsp + 200, stack); win ==> hi64(old_xmm15) == load_stack64(rsp + 208, stack); win ==> lo64(old_xmm15) == load_stack64(rsp + 216, stack); reads stackTaint; modifies rax; rbx; rbp; rdi; rsi; r12; r13; r14; r15; xmm6; xmm7; xmm8; xmm9; xmm10; xmm11; xmm12; xmm13; xmm14; xmm15; rsp; stack; ensures rbx == old(load_stack64(rsp, stack)); rbp == old(load_stack64(rsp + 8, stack)); rdi == old(load_stack64(rsp + 16, stack)); rsi == old(load_stack64(rsp + 24, stack)); r12 == old(load_stack64(rsp + 32, stack)); r13 == old(load_stack64(rsp + 40, stack)); r14 == old(load_stack64(rsp + 48, stack)); r15 == old(load_stack64(rsp + 56, stack)); win ==> xmm6 == old_xmm6; win ==> xmm7 == old_xmm7; win ==> xmm8 == old_xmm8; win ==> xmm9 == old_xmm9; win ==> xmm10 == old_xmm10; win ==> xmm11 == old_xmm11; win ==> xmm12 == old_xmm12; win ==> xmm13 == old_xmm13; win ==> xmm14 == old_xmm14; win ==> xmm15 == old_xmm15; rsp == old(rsp) + (if win then 224 else 64); stack == old(free_stack64(rsp, rsp+ (if win then 224 else 64), stack)); { Pop(rbx); Pop(rbp); Pop(rdi); Pop(rsi); Pop(r12); Pop(r13); Pop(r14); Pop(r15); inline if (win) { PopXmm(xmm6, rax, old_xmm6); PopXmm(xmm7, rax, old_xmm7); PopXmm(xmm8, rax, old_xmm8); PopXmm(xmm9, rax, old_xmm9); PopXmm(xmm10, rax, old_xmm10); PopXmm(xmm11, rax, old_xmm11); PopXmm(xmm12, rax, old_xmm12); PopXmm(xmm13, rax, old_xmm13); PopXmm(xmm14, rax, old_xmm14); PopXmm(xmm15, rax, old_xmm15); } }