1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7#include <config.h>
8#define __ASSEMBLER__
9#include <hardware.h>
10#include <sel4/plat/api/constants.h>
11#include <plat/machine/devices_gen.h>
12
13ENTRY(_start)
14
15KERNEL_OFFSET = KERNEL_ELF_BASE - KERNEL_ELF_PADDR_BASE;
16
17SECTIONS
18{
19    . = KERNEL_ELF_BASE;
20
21    .boot . : AT(ADDR(.boot) - KERNEL_OFFSET)
22    {
23        *(.boot.text)
24        *(.boot.rodata)
25        *(.boot.data)
26        . = ALIGN(64K);
27    }
28
29    ki_boot_end = .;
30
31    .text . : AT(ADDR(.text) - KERNEL_OFFSET)
32    {
33        /* Sit inside a large frame */
34        . = ALIGN(64K);
35        *(.vectors)
36
37        /* Fastpath code */
38        *(.vectors.fastpath_call)
39        *(.vectors.fastpath_reply_recv)
40        *(.vectors.text)
41
42        /* Anything else that should be in the vectors page. */
43        *(.vectors.*)
44
45        /* Hopefully all that fits into 4K! */
46
47        /* Standard kernel */
48        *(.text)
49    }
50
51    .rodata . : AT(ADDR(.rodata) - KERNEL_OFFSET)
52    {
53        *(.rodata)
54        *(.rodata.*)
55    }
56
57    .data . : AT(ADDR(.data) - KERNEL_OFFSET)
58    {
59        *(.data)
60    }
61
62    .bss . : AT(ADDR(.bss) - KERNEL_OFFSET)
63    {
64        *(.bss)
65        *(COMMON) /* fallback in case '-fno-common' is not used */
66
67        /* 4k breakpoint stack */
68        _breakpoint_stack_bottom = .;
69        . = . + 4K;
70        _breakpoint_stack_top = .;
71
72        /* large data such as the globals frame and global PD */
73        *(.bss.aligned)
74    }
75
76    . = ALIGN(4K);
77    ki_end = .;
78
79    /DISCARD/ :
80    {
81        *(.note.gnu.build-id)
82        *(.comment)
83    }
84}
85