1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
typedef tag_t = @{
type = uint32, // Identifier of tag
size = [n : nat | n >= 8] uint n // Size of tag (not including padding)
}
typedef memory_area_t = @{
base_addr = Ptr, // Start of physical address
length = [n : nat | n > 0 ] size_t n , // Size of memory region in bytes (64 bits)
type = uint, // Variety of address range represented. 1: available RAM, 3: usable memory holding ACPI information,
// 4: reserved memory (preserved on hibernation), Other: reserved area
reserved = uint 0
}
typedef memory_areas_t = @{
tag = tag_t,
entry_size = [n : nat | n > 0 && n % 8 == 0] uint n,
entry_version = uint,
entries = ptr // Pointer to entries
}
typedef elf_tag_t = @{
tag = tag_t,
num = uint, // Number of elf entries
entsize = uint 64, // Size of entry
shndx = uint, // Index of the section containing the string table
headers = ptr // Pointer to entries
}
typedef elf64_shdr_t = @{
name = uint, // Index into seaction header string table
type = uint, // Type of section (code,data,symbol,...)
flags = uint64, // Attributes and flags of section
addr = Ptr1, // (virtual) address of section in memory
offset = Ptr1, // Offset of seaction in ELF executable file
size = size_t, // Size of section in bytes
link = uint, // Extra informaion
info = uint, // Additional information
addralign = uint64, // Alignment requirements of section's address
entsize = size_t 64 // Size of each entry in section
}
typedef boot_info_t = @{
address = Ptr1,
total_size = [n : int | n > 0] uint n, // total size of boot information
memory_map = memory_areas_t,
elf_tag = elf_tag_t
}
macdef invalid_area = @{
base_addr = the_null_ptr,
length = i2sz(1),
type = 0u,
reserved = 0u
}
fun init(p : Ptr1) :void
fn get_memory_mappings_n () :<!ref> size_t
fn get_memory_mapping (n : size_t) :<!ref> memory_area_t
fn print_memory_mappings () :<!ref,!wrt> void // Print all available memory area's
fn get_elf_headers_n () : size_t
fn get_elf_header (n : size_t) : elf64_shdr_t
fn print_elf_headers () : void
fn get_kernel_ranges () : (Ptr,Ptr) // (kernel start, kernel end)
fn get_multiboot_ranges () : (Ptr0,Ptr0) // (bootinfo start, bootinfo end)
|
