aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/bootinfo/multiboot.dats67
-rw-r--r--kernel/bootinfo/multiboot.sats31
-rw-r--r--kernel/main.dats1
3 files changed, 82 insertions, 17 deletions
diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats
index 1128352..3213237 100644
--- a/kernel/bootinfo/multiboot.dats
+++ b/kernel/bootinfo/multiboot.dats
@@ -24,7 +24,11 @@ implement boot_info_init (p : Ptr1) = let
case+ type of
| 6u => (
boot_p->memory_map := $UN.ptr0_get<memory_map_t>(p);
- boot_p->memory_map.entries := ptr_add<uint>(p,4)
+ boot_p->memory_map.entries := ptr_add<uint32>(p,4)
+ )
+ | 9u => (
+ boot_p->elf_tag := $UN.ptr0_get<elf_tag_t>(p);
+ boot_p->elf_tag.headers := ptr_add<uint32>(p,5);
)
| _ => ();
@@ -43,6 +47,8 @@ end
extern castfn ui2sz (n : uint) : [n : nat] size_t n
+//------------Memory------------------------
+
implement get_memory_mappings_n(p) = let
val size = p.2->memory_map.tag.size
val n_entries = (if(size >= 16u) then (size - 16u) / p.2->memory_map.entry_size else 0u) : uint
@@ -52,13 +58,10 @@ end
// TODO: here use optional datatype (fix runtime alloc)
-implement get_memory_mapping(p,n) = let
- val size = p.2->memory_map.tag.size
- val n_entries = ui2sz (if(size >= 16u) then (size - 16u) / p.2->memory_map.entry_size else 0u)
-in
- assertloc(n < n_entries);
- $UN.ptr0_get<memory_entry_t>(ptr_add<memory_map_t>(p.2->memory_map.entries,n))
-end
+implement get_memory_mapping(p,n) = (
+ assertloc(n < get_memory_mappings_n(p));
+ $UN.ptr0_get<memory_entry_t>(ptr_add<memory_entry_t>(p.2->memory_map.entries,n))
+)
implement print_memory_mappings(p) = let
val length = get_memory_mappings_n(p)
@@ -66,18 +69,54 @@ implement print_memory_mappings(p) = let
val entry = get_memory_mapping(p,i)
in
if (entry.type = 1) then (
- print("Start Address: ");
+ print(" Start Address: ");
print_hex(entry.base_addr);
- print(" Length: ");
+ print(", Length: ");
println_hex(entry.length);
);
- if (i < n-1) then (
+ if (i < n-1) then
loop (p,succ(i),n)
- )
end
in
- if (length > 0) then
- loop(p,i2sz(0),length)
+ if (length > 0) then (
+ println!("Memory areas:");
+ loop(p,i2sz(0),length))
else
println!("No memory mappings")
end
+
+//----------------------------------------------
+
+//---------------------ELF----------------------
+
+implement get_elf_headers_n(p) = ui2sz p.2->elf_tag.num
+
+implement get_elf_header (p,n) = (
+ assertloc(n < get_elf_headers_n(p));
+ $UN.ptr0_get<elf64_shdr_t>(ptr_add<elf64_shdr_t>(p.2->elf_tag.headers,n))
+)
+
+implement print_elf_headers(p) = let
+ val length = get_elf_headers_n(p)
+ fun loop {n,i : nat | i < n} .<n-i>. (p : !bootptr, i : size_t i, n : size_t n) : void = let
+ val header = get_elf_header(p,i)
+ in
+ print(" addr: ");
+ print_hex(header.addr);
+ print(", size: ");
+ print_hex(header.size);
+ print(", flags: ");
+ println_hex(header.flags);
+ if (i < n - 1) then
+ loop(p,succ(i),n)
+ end
+in
+ if (length > 0) then (
+ println!("Elf section headers: ");
+ loop(p,i2sz(0),length))
+ else
+ println!("No elf section headers")
+end
+
+//----------------------------------------------
+
diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats
index 0507241..0d89040 100644
--- a/kernel/bootinfo/multiboot.sats
+++ b/kernel/bootinfo/multiboot.sats
@@ -7,7 +7,7 @@ typedef tag_t = @{
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,
+ 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
}
@@ -19,10 +19,31 @@ typedef memory_map_t = @{
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 = @{
- total_size = uint, // total size of boot information
- memory_map = memory_map_t
+ total_size = uint, // total size of boot information
+ memory_map = memory_map_t,
+ elf_tag = elf_tag_t
}
vtypedef bootptr = [l : agz] (boot_info_t@l , boot_info_t@l -<lin,prf> void | ptr l)
@@ -32,3 +53,7 @@ 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
+
+fn get_elf_headers_n (p : !bootptr) : [n:nat] size_t n
+fn get_elf_header (p : !bootptr, n : size_t) : elf64_shdr_t
+fn print_elf_headers (p : !bootptr) : void
diff --git a/kernel/main.dats b/kernel/main.dats
index 67afb7c..2a89603 100644
--- a/kernel/main.dats
+++ b/kernel/main.dats
@@ -27,6 +27,7 @@ implement main(p) = let
in
print_memory_mappings(bootptr);
+ print_elf_headers(bootptr);
// Initialize interrupt table
idt_init();