blob: 7a54c3165c6736f5d7882ef66525dbe05277d41e [file] [log] [blame] [edit]
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
* Copyright 2021, HENSOLDT Cyber
*
* SPDX-License-Identifier: GPL-2.0-only
*/
#pragma once
#include <types.h>
typedef uintptr_t paddr_t;
typedef uintptr_t vaddr_t;
#define PAGE_BITS 12
#define BIT(x) (1 << (x))
#define MASK(n) (BIT(n) - 1)
#define MIN(a, b) (((a) < (b)) ? (a) : (b))
#define IS_ALIGNED(n, b) (!((n) & MASK(b)))
#define ROUND_UP(n, b) (((((n) - 1) >> (b)) + 1) << (b))
#define ROUND_DOWN(n, b) (((n) >> (b)) << (b))
#define ALIGN(n) __attribute__((__aligned__(n)))
#if __has_attribute(externally_visible)
#define VISIBLE __attribute__((externally_visible))
#else
#define VISIBLE
#endif
#define WEAK __attribute__((weak))
#define NORETURN __attribute__((noreturn))
#define UNREACHABLE() __builtin_unreachable()
#define UNUSED __attribute__((unused))
#define UNUSED_VARIABLE(x) ((void)(x))
#define ARRAY_SIZE(a) (sizeof(a)/sizeof((a)[0]))
#define NULL ((void *)0)
/*
* Information about an image we are loading.
*/
struct image_info {
/* Start/end byte of the image in physical memory. */
paddr_t phys_region_start;
paddr_t phys_region_end;
/* Start/end byte in virtual memory the image requires to be located. */
vaddr_t virt_region_start;
vaddr_t virt_region_end;
/* Virtual address of the user image's entry point. */
vaddr_t virt_entry;
/* The seL4 kernel boot interface does not have the parameter virt_entry,
* but expect a parameter with the offset between the physical and virtual
* addresses of the image, where this must hold:
* virt_address + phys_virt_offset = phys_address
* Practically, the offset is usually a positive value, because the virtual
* address is a low value and the actually physical address is much greater.
* But in general, there is no restrictions on the physical and virtual
* image location. Defining phys_virt_offset as a signed value might seem
* the intuitive choice how to handle this, but there is are two catches
* here that break the C rules. We can't cover the full integer range then
* and overflows/underflows are well defined for unsigned values only. They
* are undefined for signed values, even if such operations practically work
* in many cases due to how the compiler/machine implements negative
* integers using the two's-complement.
* Assume 32-bit system with virt_address=0xc0000000 and phys_address=0,
* then phys_virt_offset would have to be -0xc0000000. This value is not
* in the 32-bit signed integer range. With unsigned integers, calculating
* 0 - 0xc0000000 results in 0x40000000 after an underflow, the reverse
* calculation 0xc0000000 + 0x40000000 results in 0 again after overflow. If
* 0x40000000 is a signed integer, result is likely the same, but the whole
* operation is completely undefined by C rules.
*/
word_t phys_virt_offset;
};
extern struct image_info kernel_info;
extern struct image_info user_info;
extern void const *dtb;
/* Symbols defined in linker scripts. */
extern char _text[];
extern char _end[];
extern char _archive_start[];
extern char _archive_start_end[];
/* Clear BSS. */
void clear_bss(void);
/* Load images. */
int load_images(
struct image_info *kernel_info,
struct image_info *user_info,
unsigned int max_user_images,
unsigned int *num_images,
void const *bootloader_dtb,
void const **chosen_dtb,
size_t *chosen_dtb_size);
/* Platform functions */
void platform_init(void);
void init_cpus(void);
int plat_console_putchar(unsigned int c);