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
|
typedef tag_t = @{
type = uint32, // Identifier of tag
size = [n : nat | n >= 8] uint n // Size of tag (not including padding)
}
typedef memory_entry_t = @{
base_addr = Ptr1, // Start of physical address
length = uint64, // Size of memory region in bytes
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_map_t = @{
tag = tag_t,
entry_size = [n : nat | n > 0 && n % 8 == 0] uint n,
entry_version = uint,
entries = ptr // Pointer to entries
}
typedef boot_info_t = @{
total_size = uint, // total size of boot information
memory_map = memory_map_t
}
vtypedef bootptr = [l : agz] (boot_info_t@l , boot_info_t@l -<lin,prf> void | ptr l)
fun boot_info_init(p : Ptr1) : bootptr
fn get_memory_mappings_n (p : !bootptr) : [n:nat] size_t n
fn get_memory_mapping (p : !bootptr, n : size_t) : memory_entry_t
fn print_memory_mappings (p : !bootptr) : void
|
