bits 64

global process_trampoline
process_trampoline:
    extern current_process
    mov rax, [current_process]
    mov rdx, [rax + 40] ; current_process->user_rsp

    ; Keep in sync with `gdt.h` and `layout.h`
    mov rax, 0x0000000000400000
    mov rbx, 0x2B
    mov rcx, 0x202
    mov rsi, 0x23

    push rsi
    push rdx
    push rcx
    push rbx
    push rax
    iretq

global process_switch_to
; process_switch_to(uint64_t *save_rsp, uint64_t new_rsp, uint64_t new_pml4_phys)
process_switch_to:
    ; save callee-saved registers of the OUTGOING process
    push rbp
    push rbx
    push r12
    push r13
    push r14
    push r15

    ; save current rsp into *save_rsp (rdi)
    mov [rdi], rsp

    ; switch address space
    mov cr3, rdx          ; rdx = new_pml4_phys (3rd arg)

    ; switch to incoming process's stack
    mov rsp, rsi          ; rsi = new_rsp (2nd arg)

    ; restore callee-saved registers of the INCOMING process
    pop r15
    pop r14
    pop r13
    pop r12
    pop rbx
    pop rbp

    ret