1/* 2 * Copyright 2019, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 */ 12#include <sel4runtime/gen_config.h> 13 14.section .text 15.global _sel4_start 16_sel4_start: 17 leaq __stack_top, %rsp 18 movq %rsp, %rbp 19 /* 20 * GCC expects that a C function is always entered via a call 21 * instruction and that the stack is 16-byte aligned before such an 22 * instruction (leaving it 16-byte aligned + 1 word from the 23 * implicit push when the function is entered). 24 * 25 * If additional items are pushed onto the stack, the stack must be 26 * manually re-aligned before the call instruction to 27 * __sel4_start_c. 28 */ 29 subq $0x8, %rsp 30 push %rbp 31 call __sel4_start_root 32 33 /* should not return */ 341: 35 jmp 1b 36 37.section .bss 38__stack_base: 39 .align 16 40 .space CONFIG_SEL4RUNTIME_ROOT_STACK 41__stack_top: 42