diff options
| -rw-r--r-- | kernel/bootinfo/multiboot.dats | 288 | ||||
| -rw-r--r-- | kernel/bootinfo/multiboot.sats | 29 | ||||
| -rw-r--r-- | kernel/main.dats | 46 | ||||
| -rw-r--r-- | kernel/memory/frame.dats | 258 | ||||
| -rw-r--r-- | kernel/memory/frame.sats | 50 | ||||
| -rw-r--r-- | kernel/prelude/DATS/print.dats | 24 | ||||
| -rw-r--r-- | lib/DATS/init.dats | 48 | ||||
| -rw-r--r-- | lib/DATS/itoa.dats | 10 | ||||
| -rw-r--r-- | lib/DATS/writer.dats | 28 | ||||
| -rw-r--r-- | lib/SATS/init.sats | 10 | ||||
| -rw-r--r-- | lib/SATS/writer.sats | 4 |
11 files changed, 431 insertions, 364 deletions
diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats index 9eee595..0653184 100644 --- a/kernel/bootinfo/multiboot.dats +++ b/kernel/bootinfo/multiboot.dats @@ -3,150 +3,186 @@ #define ATS_DYNLOADFLAG 0 staload "./multiboot.sats" +staload "lib/SATS/init.sats" +staload "lib/DATS/init.dats" staload UN = "prelude/SATS/unsafe.sats" local -var boot_info : boot_info_t + extern castfn ui2sz (n : uint) :<> [n : nat] size_t n + extern fn _get_memory_mappings_n(boot_info : !boot_info_t):<> [n:nat] size_t n + extern fn _get_memory_mapping(boot_info : !boot_info_t,n : size_t):<> memory_area_t + extern fn _print_memory_mappings(boot_info : !boot_info_t):<!wrt> void in -implement boot_info_init (p : Ptr1) = let - extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (boot_info_t@l) // takeout proof UNSAFE: - prval (pf, fpf) = __assert (addr@boot_info) - val total_size = $UN.ptr0_get<uint>(p) - - fun loop {l : agz} (pf : !boot_info_t@l | boot_p : ptr l , p : ptr): void = let - val type = $UN.ptr0_get<uint>(p) - val size = $UN.ptr0_get<uint>(ptr_succ<uint>(p)) - val next = (if (size % 8u != 0) then size + 8u - (size % 8u) else size) : uint - in - case+ type of - | 6u => ( - boot_p->memory_map := $UN.ptr0_get<memory_areas_t>(p); - 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); - ) - | _ => (); - - if (type != 0u) then - loop(pf | boot_p, ptr_add<uint8>(p, next)) - end - -in - boot_info.total_size := total_size; - loop(pf | addr@boot_info, ptr_add<uint32>(p,2)); - - (pf , fpf | addr@boot_info) -end - -end - -extern castfn ui2sz (n : uint) :<> [n : nat] size_t n - -//------------Memory------------------------ - -implement get_memory_mappings_n(pf | p) = let - val size = p->memory_map.tag.size - val n_entries = (if(size >= 16u) then (size - 16u) / p->memory_map.entry_size else 0u) : uint -in - ui2sz n_entries -end - -// TODO: here use optional datatype (fix runtime alloc) + local + // Static variable + var _v : boot_info_t? + prval () = opt_none _v + var v = uninitialized<boot_info_t>(_v) + // Reference to writer + val bootinfo_ref = ref_make_viewptr{initializable boot_info_t} (view@v | addr@v) + in -implement get_memory_mapping(pf | p,n) = ( - (* assertloc(n < get_memory_mappings_n(pf | p)); *) - $UN.ptr0_get<memory_area_t>(ptr_add<memory_area_t>(p->memory_map.entries,n)) -) + implement init (p : Ptr1) = let + extern castfn unsafe_init(x : &boot_info_t? >> boot_info_t) :<> void + val total_size = $UN.ptr0_get<uint>(p) + + fun loop (boot_info : &boot_info_t? >> boot_info_t, p : ptr):<!wrt,!ntm> void = let + val type = $UN.ptr0_get<uint>(p) + val size = $UN.ptr0_get<uint>(ptr_succ<uint>(p)) + val next = (if (size % 8u != 0) then size + 8u - (size % 8u) else size) : uint + in + case+ type of + | 6u => ( + boot_info.memory_map := $UN.ptr0_get<memory_areas_t>(p); + boot_info.memory_map.entries := ptr_add<uint32>(p,4) + ) + | 9u => ( + boot_info.elf_tag := $UN.ptr0_get<elf_tag_t>(p); + boot_info.elf_tag.headers := ptr_add<uint32>(p,5); + ) + | _ => (); + + if (type != 0u) then + loop(boot_info,ptr_add<uint8>(p, next)) + else + unsafe_init(boot_info) + end + + val (vbox pf | boot_p) = ref_get_viewptr(bootinfo_ref) + in + if (not boot_p->initialized) then + let + prval () = opt_unnone boot_p->obj + val () = boot_p->obj.total_size := total_size + val () = loop(boot_p->obj, ptr_add<uint32>(p,2)) + val () = boot_p->initialized := true + prval () = opt_some boot_p->obj + in end + end + + implement get_memory_mappings_n() = let + implement exec$fwork<boot_info_t><size_t>(v,_) = _get_memory_mappings_n(v) + in + exec<boot_info_t>(bootinfo_ref,i2sz(0)) + end + + implement get_memory_mapping(n) = let + implement exec$fwork<boot_info_t><memory_area_t>(v,_) = _get_memory_mapping(v,n) + in + exec<boot_info_t><memory_area_t>(bootinfo_ref,invalid_area) + end + + implement print_memory_mappings() = let + implement exec_void$fwork<boot_info_t>(v) = _print_memory_mappings(v) + in + exec_void<boot_info_t>(bootinfo_ref) + end -//TODO: use foreach with fwork to loop through memory maps -implement print_memory_mappings(p) = let - val length = get_memory_mappings_n(p.0 | p.2) - fun loop {n,i : nat | i < n} .<n-i>. (p : !bootptr, i : size_t i, n : size_t n) : void = let - val entry = get_memory_mapping(p.0 | p.2 ,i) - in - if (entry.type = 1) then ( - print(" Start Address: "); - print_hex(entry.base_addr); - print(", Length: "); - println_hex(entry.length); - ); - if (i < n-1) then - loop (p,succ(i),n) end -in - if (length > 0) then ( - println!("Memory areas:"); - loop(p,i2sz(0),length)) - else - println!("No memory mappings") -end -//---------------------------------------------- + //------------Memory------------------------ -//---------------------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 get_kernel_ranges(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, min : Ptr, max : Ptr) : (Ptr,Ptr) = let - val header = get_elf_header(p,i) - val new_min = (if ((header.addr < min || min = the_null_ptr) && header.size != 0) then header.addr else min) - val end_p = ptr_add<uint8>(header.addr,header.size) - val new_max = ( - if (end_p > max && header.size != 0) - then $UN.cast2Ptr1(end_p) - else max - ) + implement _get_memory_mappings_n(boot_info) = let + val size = boot_info.memory_map.tag.size + val n_entries = (if(size >= 16u) then (size - 16u) / boot_info.memory_map.entry_size else 0u) : uint in - if (i < n - 1) then - loop(p,succ(i),n,new_min,new_max) - else - (new_min,new_max) + ui2sz n_entries end -in - if (length > 0) then - loop(p,i2sz(0),length,the_null_ptr,the_null_ptr) - else - (the_null_ptr,the_null_ptr) -end - -implement get_multiboot_ranges(p) = (p.2, $UN.cast2Ptr1(ptr_add<uint8>(p.2,p.2->total_size))) - -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) + implement _get_memory_mapping(boot_info,n) = ( + (* assertloc(n < get_memory_mappings_n(pf | p)); *) + $UN.ptr0_get<memory_area_t>(ptr_add<memory_area_t>(boot_info.memory_map.entries,n)) + ) + + //TODO: use foreach with fwork to loop through memory maps + implement _print_memory_mappings(boot_info) = let + val length = _get_memory_mappings_n(boot_info) + fun loop {n,i : nat | i < n} .<n-i>. (i : size_t i, n : size_t n):<!wrt> void = let + val entry = _get_memory_mapping(boot_info,i) + in + if (entry.type = 1) then ( + print(" Start Address: "); + print_hex(entry.base_addr); + print(", Length: "); + println_hex(entry.length); + ); + if (i < n-1) then + loop (succ(i),n) + end 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) - + if (length > 0) then ( + println!("Memory areas:"); + loop(i2sz(0),length)) + else + println!("No memory mappings") end -in - if (length > 0) then ( - println!("Elf section headers: "); - loop(p,i2sz(0),length)) - else - println!("No elf section headers") + 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 get_kernel_ranges(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, min : Ptr, max : Ptr) : (Ptr,Ptr) = let *) +(* val header = get_elf_header(p,i) *) +(* val new_min = (if ((header.addr < min || min = the_null_ptr) && header.size != 0) then header.addr else min) *) +(* val end_p = ptr_add<uint8>(header.addr,header.size) *) +(* val new_max = ( *) +(* if (end_p > max && header.size != 0) *) +(* then $UN.cast2Ptr1(end_p) *) +(* else max *) +(* ) *) +(* in *) +(* if (i < n - 1) then *) +(* loop(p,succ(i),n,new_min,new_max) *) +(* else *) +(* (new_min,new_max) *) +(* end *) +(**) +(* in *) +(* if (length > 0) then *) +(* loop(p,i2sz(0),length,the_null_ptr,the_null_ptr) *) +(* else *) +(* (the_null_ptr,the_null_ptr) *) +(* end *) +(**) +(* implement get_multiboot_ranges(p) = (p.2, $UN.cast2Ptr1(ptr_add<uint8>(p.2,p.2->total_size))) *) +(**) +(* 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 1a2e6db..cab885a 100644 --- a/kernel/bootinfo/multiboot.sats +++ b/kernel/bootinfo/multiboot.sats @@ -45,24 +45,23 @@ typedef boot_info_t = @{ elf_tag = elf_tag_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 {l : agz} (pf : !boot_info_t@l | p : ptr l) :<> [n:nat] size_t n -fn get_memory_mapping {l:agz} (pf : !boot_info_t @ l | p : ptr l, n : size_t) :<> memory_area_t -fn print_memory_mappings (p : !bootptr) : void // Print all available memory area's - -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 - -fn get_kernel_ranges (p : !bootptr) : (Ptr,Ptr) // (kernel start, kernel end) -fn get_multiboot_ranges (p : !bootptr) : (Ptr0,Ptr0) // (bootinfo start, bootinfo end) - 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 () : [n:nat] size_t n +fn get_memory_mapping (n : size_t) : memory_area_t +fn print_memory_mappings () : void // Print all available memory area's + +(* fn get_elf_headers_n () : [n:nat] size_t n *) +(* 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) *) + diff --git a/kernel/main.dats b/kernel/main.dats index dadcd2d..4c7d49a 100644 --- a/kernel/main.dats +++ b/kernel/main.dats @@ -1,7 +1,7 @@ #include "./prelude/kernel_prelude.hats" staload "kernel/interrupts/idt.sats" -staload "kernel/bootinfo/multiboot.sats" +staload BOOT = "kernel/bootinfo/multiboot.sats" staload "kernel/memory/frame.sats" staload "lib/SATS/writer.sats" @@ -13,17 +13,17 @@ staload "lib/SATS/writer.sats" //NOTE: how to make sure ats checks 2 contstraints in one if statement? //TODO: put in seperate utils module (just generic size function) -fn kernel_size(kernel_start : Ptr, kernel_end : Ptr) : size_t = let - extern castfn Ptr12size (a : Ptr1): size_t -in - if (kernel_end > the_null_ptr) then - if (kernel_start > the_null_ptr) then - Ptr12size(kernel_end) - Ptr12size(kernel_start) - else - i2sz(0) - else - i2sz(0) -end +(* fn kernel_size(kernel_start : Ptr, kernel_end : Ptr) : size_t = let *) +(* extern castfn Ptr12size (a : Ptr1): size_t *) +(* in *) +(* if (kernel_end > the_null_ptr) then *) +(* if (kernel_start > the_null_ptr) then *) +(* Ptr12size(kernel_end) - Ptr12size(kernel_start) *) +(* else *) +(* i2sz(0) *) +(* else *) +(* i2sz(0) *) +(* end *) (* fn test(allocptr : !allocptr, bootptr : !bootptr) : void = let *) (* fun loop(i : int) : void = if (i < 160) then( let val _ = allocate_frame(allocptr.0, bootptr.0 | allocptr.2, bootptr.2) in end; loop(succ(i))) *) @@ -37,19 +37,20 @@ extern fun breakpoint() :void = "mac#" extern fun entry(p : Ptr1) : void = "ext#" implement entry(p) = let - val () = clear_screen() // Initialize boot info struct - val bootptr = boot_info_init(p) - val (kernel_start,kernel_end) = get_kernel_ranges(bootptr) - val (multiboot_start,multiboot_end) = get_multiboot_ranges(bootptr) + val () = $BOOT.init(p) + + (* val (kernel_start,kernel_end) = get_kernel_ranges(bootptr) *) + (* val (multiboot_start,multiboot_end) = get_multiboot_ranges(bootptr) *) (* val allocptr = frame_allocator_init(kernel_start,kernel_end,multiboot_start,multiboot_end,bootptr) *) in - print_memory_mappings(bootptr); + clear_screen(); + $BOOT.print_memory_mappings(); - print_elf_headers(bootptr); - println!("Kernel Size: ", kernel_size(kernel_start,kernel_end)); + (* print_elf_headers(bootptr); *) + (* println!("Kernel Size: ", kernel_size(kernel_start,kernel_end)); *) (* test(allocptr,bootptr); *) (* let *) (* val frame = allocate_frame(allocptr.0, bootptr.0 | allocptr.2, bootptr.2) *) @@ -65,13 +66,6 @@ in println!("End"); - - let - prval () = bootptr.1(bootptr.0) - (* prval () = allocptr.1(allocptr.0) *) - in end - - end // Satisfy ats compiler. Should be called once to dynload files diff --git a/kernel/memory/frame.dats b/kernel/memory/frame.dats index 5a950ad..8a9160b 100644 --- a/kernel/memory/frame.dats +++ b/kernel/memory/frame.dats @@ -1,131 +1,131 @@ -#include "kernel/prelude/kernel_prelude.hats" - +(* #include "kernel/prelude/kernel_prelude.hats" *) +(**) #define ATS_DYNLOADFLAG 0 - -staload "./frame.sats" -staload "kernel/bootinfo/multiboot.sats" -staload "lib/SATS/init.sats" - -staload UN = "prelude/SATS/unsafe.sats" - -assume frame_allocator = frame_allocator_t - -implement containing_address(address): frame_t = - @{ - counter = $UN.cast{size_t}(address) / i2sz(PAGE_SIZE) - } - -fn containing_area(area : memory_area_t) :<> frame_t = containing_address(ptr_add<uint8>(area.base_addr,area.length - i2sz(1))) - -//FIX: function doesn't handle no frames left -fn choose_next_area{k : agz}(bf : !boot_info_t @ k | b : ptr k, allocator : &frame_allocator_t) :<!wrt> void = let - val length = get_memory_mappings_n(bf | b) - val next_free_frame = allocator.next_free_frame - fun loop {n,i : nat | i < n} {l : agz} .<n-i>. (bf : !boot_info_t @ l | b : ptr l, i : size_t i, n : size_t n) :<> memory_area_t = let - val entry = get_memory_mapping(bf | b ,i) - val fr = containing_area(entry) - in - if (entry.type = 1 && fr.num >= next_free_frame.num) then - entry - else if (i < n-1) then - loop (bf | b,succ(i),n) - else - entry //TODO: fix - end -in - if (length > 0) then //TODO: fix - allocator.current_area := loop(bf | b, i2sz(0), length); - - if (allocator.current_area.length > 1) then - let - val start_frame = containing_address(allocator.current_area.base_addr) - in - if (allocator.next_free_frame.num < start_frame.num) then - allocator.next_free_frame := start_frame - end -end - -local - -var allocator_static : frame_allocator_t? -prval () = opt_none allocator_static -var allocator = uninitialized<frame_allocator_t>(allocator_static) -val allocator_ref = ref_make_viewptr{initializable frame_allocator_t} (view@allocator | addr@allocator) - -in - - implement frame_allocator_init(kernel_start, kernel_end, multiboot_start, multiboot_end, b) : void = let - val allocator = @{ - next_free_frame = containing_address(the_null_ptr), - current_area = invalid_area, - kernel_start = containing_address(kernel_start), - kernel_end = containing_address(kernel_end), - multiboot_start = containing_address(multiboot_start), - multiboot_end = containing_address(multiboot_end) - } : frame_allocator_t - val (vbox pf | p) = ref_get_viewptr(allocator_ref) - in - if not p->initialized then let - prval () = opt_unnone p->obj - in - p->obj := allocator; - p->initialized := true; - (* choose_next_area(b.0 | b.2, !p); *) - let prval () = opt_some p->obj in end; - end - end - -implement allocate_frame(bf | b) : frame_t = let - val (vbox pf | p) = ref_get_viewptr(allocator_ref) - in - if p->initialized then let - (* var allocator = p->obj *) - prval () = opt_unsome p->obj - in - (* if (allocator.current_area.type != 0u) then let *) - (* val area = allocator.current_area *) - (* val frame = @{ num = allocator.next_free_frame.num } *) - (**) - (* // last frame of current area *) - (* val last_frame_area = containing_area(area) *) - (* in *) - (* if (frame.num > last_frame_area.num) then ( *) - (* // all frames of current area are used, switch to next area *) - (* choose_next_area(bf | b, allocator); *) - (* let prval () = opt_some allocator in end; *) - (* allocate_frame(bf | b) *) - (* ) else if (frame.num >= allocator.kernel_start.num && frame.num <= allocator.kernel_end.num) then ( *) - (* // frame is used by kernel *) - (* allocator.next_free_frame := @{num = allocator.kernel_end.num + 1}; *) - (* let prval () = opt_some allocator in end; *) - (* allocate_frame(bf | b) *) - (* ) else if (frame.num >= allocator.multiboot_start.num && frame.num <= allocator.multiboot_end.num) then ( *) - (* // frame is used by multiboot info structure *) - (* allocator.next_free_frame := @{num = allocator.multiboot_end.num + 1}; *) - (* let prval () = opt_some allocator in end; *) - (* allocate_frame(bf | b) *) - (* ) else ( *) - (* // frame is unused, increment `next_free_frame` and return it *) - (* allocator.next_free_frame.num := succ(allocator.next_free_frame.num); *) - (* let prval () = opt_some allocator in end; *) - (* frame *) - (* ); *) - (* end *) - (* else *) - (* let prval () = opt_some allocator in end; *) - (* @{num = i2sz(0)} // No free frames left *) - let prval () = opt_some p->obj in end; - @{num = i2sz(0)} - end - else - @{num = i2sz(0)} // No free frames left - -end - -end - -implement deallocate_frame(p) : void = let -in - -end +(**) +(* staload "./frame.sats" *) +(* staload "kernel/bootinfo/multiboot.sats" *) +(* staload "lib/SATS/init.sats" *) +(**) +(* staload UN = "prelude/SATS/unsafe.sats" *) +(**) +(* assume frame_allocator = frame_allocator_t *) +(**) +(* implement containing_address(address): frame_t = *) +(* @{ *) +(* counter = $UN.cast{size_t}(address) / i2sz(PAGE_SIZE) *) +(* } *) +(**) +(* fn containing_area(area : memory_area_t) :<> frame_t = containing_address(ptr_add<uint8>(area.base_addr,area.length - i2sz(1))) *) +(**) +(* //FIX: function doesn't handle no frames left *) +(* fn choose_next_area{k : agz}(bf : !boot_info_t @ k | b : ptr k, allocator : &frame_allocator_t) :<!wrt> void = let *) +(* val length = get_memory_mappings_n(bf | b) *) +(* val next_free_frame = allocator.next_free_frame *) +(* fun loop {n,i : nat | i < n} {l : agz} .<n-i>. (bf : !boot_info_t @ l | b : ptr l, i : size_t i, n : size_t n) :<> memory_area_t = let *) +(* val entry = get_memory_mapping(bf | b ,i) *) +(* val fr = containing_area(entry) *) +(* in *) +(* if (entry.type = 1 && fr.num >= next_free_frame.num) then *) +(* entry *) +(* else if (i < n-1) then *) +(* loop (bf | b,succ(i),n) *) +(* else *) +(* entry //TODO: fix *) +(* end *) +(* in *) +(* if (length > 0) then //TODO: fix *) +(* allocator.current_area := loop(bf | b, i2sz(0), length); *) +(**) +(* if (allocator.current_area.length > 1) then *) +(* let *) +(* val start_frame = containing_address(allocator.current_area.base_addr) *) +(* in *) +(* if (allocator.next_free_frame.num < start_frame.num) then *) +(* allocator.next_free_frame := start_frame *) +(* end *) +(* end *) +(**) +(* local *) +(**) +(* var allocator_static : frame_allocator_t? *) +(* prval () = opt_none allocator_static *) +(* var allocator = uninitialized<frame_allocator_t>(allocator_static) *) +(* val allocator_ref = ref_make_viewptr{initializable frame_allocator_t} (view@allocator | addr@allocator) *) +(**) +(* in *) +(**) +(* implement frame_allocator_init(kernel_start, kernel_end, multiboot_start, multiboot_end, b) : void = let *) +(* val allocator = @{ *) +(* next_free_frame = containing_address(the_null_ptr), *) +(* current_area = invalid_area, *) +(* kernel_start = containing_address(kernel_start), *) +(* kernel_end = containing_address(kernel_end), *) +(* multiboot_start = containing_address(multiboot_start), *) +(* multiboot_end = containing_address(multiboot_end) *) +(* } : frame_allocator_t *) +(* val (vbox pf | p) = ref_get_viewptr(allocator_ref) *) +(* in *) +(* if not p->initialized then let *) +(* prval () = opt_unnone p->obj *) +(* in *) +(* p->obj := allocator; *) +(* p->initialized := true; *) +(* (* choose_next_area(b.0 | b.2, !p); *) *) +(* let prval () = opt_some p->obj in end; *) +(* end *) +(* end *) +(**) +(* implement allocate_frame(bf | b) : frame_t = let *) +(* val (vbox pf | p) = ref_get_viewptr(allocator_ref) *) +(* in *) +(* if p->initialized then let *) +(* (* var allocator = p->obj *) *) +(* prval () = opt_unsome p->obj *) +(* in *) +(* (* if (allocator.current_area.type != 0u) then let *) *) +(* (* val area = allocator.current_area *) *) +(* (* val frame = @{ num = allocator.next_free_frame.num } *) *) +(* (**) *) +(* (* // last frame of current area *) *) +(* (* val last_frame_area = containing_area(area) *) *) +(* (* in *) *) +(* (* if (frame.num > last_frame_area.num) then ( *) *) +(* (* // all frames of current area are used, switch to next area *) *) +(* (* choose_next_area(bf | b, allocator); *) *) +(* (* let prval () = opt_some allocator in end; *) *) +(* (* allocate_frame(bf | b) *) *) +(* (* ) else if (frame.num >= allocator.kernel_start.num && frame.num <= allocator.kernel_end.num) then ( *) *) +(* (* // frame is used by kernel *) *) +(* (* allocator.next_free_frame := @{num = allocator.kernel_end.num + 1}; *) *) +(* (* let prval () = opt_some allocator in end; *) *) +(* (* allocate_frame(bf | b) *) *) +(* (* ) else if (frame.num >= allocator.multiboot_start.num && frame.num <= allocator.multiboot_end.num) then ( *) *) +(* (* // frame is used by multiboot info structure *) *) +(* (* allocator.next_free_frame := @{num = allocator.multiboot_end.num + 1}; *) *) +(* (* let prval () = opt_some allocator in end; *) *) +(* (* allocate_frame(bf | b) *) *) +(* (* ) else ( *) *) +(* (* // frame is unused, increment `next_free_frame` and return it *) *) +(* (* allocator.next_free_frame.num := succ(allocator.next_free_frame.num); *) *) +(* (* let prval () = opt_some allocator in end; *) *) +(* (* frame *) *) +(* (* ); *) *) +(* (* end *) *) +(* (* else *) *) +(* (* let prval () = opt_some allocator in end; *) *) +(* (* @{num = i2sz(0)} // No free frames left *) *) +(* let prval () = opt_some p->obj in end; *) +(* @{num = i2sz(0)} *) +(* end *) +(* else *) +(* @{num = i2sz(0)} // No free frames left *) +(* *) +(* end *) +(**) +(* end *) +(**) +(* implement deallocate_frame(p) : void = let *) +(* in *) +(* *) +(* end *) diff --git a/kernel/memory/frame.sats b/kernel/memory/frame.sats index 0de5056..0926e6c 100644 --- a/kernel/memory/frame.sats +++ b/kernel/memory/frame.sats @@ -1,25 +1,25 @@ -#define PAGE_SIZE 4096 - -staload "kernel/bootinfo/multiboot.sats" - -typedef frame_t = @{ - num = size_t -} - -typedef frame_allocator_t = @{ - next_free_frame = frame_t, - current_area = memory_area_t, - kernel_start = frame_t, - kernel_end = frame_t, - multiboot_start = frame_t, - multiboot_end = frame_t -} - -vtypedef allocptr = [l : agz] (frame_allocator_t@l , frame_allocator_t@l -<lin,prf> void | ptr l) - -abst@ype frame_allocator = frame_allocator_t - -fn containing_address {l : addr} (address : ptr l) :<> frame_t -fn allocate_frame {l : agz}{k : agz} (bf : !boot_info_t @ k | b : ptr k) :<!ref,!wrt> frame_t -fn deallocate_frame (p : !allocptr) : void -fn frame_allocator_init(kernel_start: Ptr, kernel_end: Ptr, multiboot_start:Ptr, multiboot_end: Ptr, b : !bootptr) : void +(* #define PAGE_SIZE 4096 *) +(**) +(* staload "kernel/bootinfo/multiboot.sats" *) +(**) +(* typedef frame_t = @{ *) +(* num = size_t *) +(* } *) +(**) +(* typedef frame_allocator_t = @{ *) +(* next_free_frame = frame_t, *) +(* current_area = memory_area_t, *) +(* kernel_start = frame_t, *) +(* kernel_end = frame_t, *) +(* multiboot_start = frame_t, *) +(* multiboot_end = frame_t *) +(* } *) +(**) +(* vtypedef allocptr = [l : agz] (frame_allocator_t@l , frame_allocator_t@l -<lin,prf> void | ptr l) *) +(**) +(* abst@ype frame_allocator = frame_allocator_t *) +(**) +(* fn containing_address {l : addr} (address : ptr l) :<> frame_t *) +(* fn allocate_frame {l : agz}{k : agz} (bf : !boot_info_t @ k | b : ptr k) :<!ref,!wrt> frame_t *) +(* fn deallocate_frame (p : !allocptr) : void *) +(* (* fn frame_allocator_init(kernel_start: Ptr, kernel_end: Ptr, multiboot_start:Ptr, multiboot_end: Ptr, b : !bootptr) : void *) *) diff --git a/kernel/prelude/DATS/print.dats b/kernel/prelude/DATS/print.dats index b183da5..ac864ad 100644 --- a/kernel/prelude/DATS/print.dats +++ b/kernel/prelude/DATS/print.dats @@ -7,34 +7,34 @@ staload "lib/DATS/itoa.dats" staload UN = "prelude/SATS/unsafe.sats" -extern fun print_newline() : void +extern fun print_newline() :<!wrt> void implement print_newline() = put_string("\n") -extern fun assert_errmsg(b: bool, msg: string) : void +extern fun assert_errmsg(b: bool, msg: string) :<!wrt> void implement assert_errmsg(b,msg) = if (~b) then put_string(msg) -extern fun print_int (n : int) : void +extern fun print_int (n : int) :<!wrt> void implement print_int(n) = put_string(itoa(n,10)) -extern fun print_uint32 (n : uint32) : void +extern fun print_uint32 (n : uint32) :<!wrt> void implement print_uint32 (n) = put_string(itoa($UN.cast{int}(n),10)) -extern fun print_uint16 (n : uint16) : void +extern fun print_uint16 (n : uint16) :<!wrt> void implement print_uint16 (n) = put_string(itoa($UN.cast{int}(n),10)) -extern fun print_uint8 (n : uint8) : void +extern fun print_uint8 (n : uint8) :<!wrt> void implement print_uint8 (n) = put_string(itoa($UN.cast{int}(n),10)) -extern fun print_uint64 (n : uint64) : void +extern fun print_uint64 (n : uint64) :<!wrt> void implement print_uint64 (n) = put_string(itoa($UN.cast{int}(n),10)) -extern fun print_size_t (n : size_t) : void +extern fun print_size_t (n : size_t) :<!wrt> void implement print_size_t (n) = put_string(itoa($UN.cast{int}(n),10)) -extern fun print_uint (n : uint) : void +extern fun print_uint (n : uint) :<!wrt> void implement print_uint (n) = put_string(itoa($UN.cast{int}(n),10)) -extern fun print_addr (n : Ptr) : void +extern fun print_addr (n : Ptr) :<!wrt> void implement print_addr (n) = put_string(itoa($UN.cast{int}(n),10)) overload print with put_string of 1 @@ -47,10 +47,10 @@ overload print with print_size_t of 1 overload print with print_uint of 1 overload print with print_addr of 1 -extern fun {a : t@ype} println_base {n:nat | n > 1 && n < 33} (n :a, base : int n) : void +extern fun {a : t@ype} println_base {n:nat | n > 1 && n < 33} (n :a, base : int n) :<!wrt> void implement{a} println_base(n,base) = println!(itoa($UN.cast{int}(n), base)) -extern fun {a : t@ype} print_base {n:nat | n > 1 && n < 33} (n :a, base : int n) : void +extern fun {a : t@ype} print_base {n:nat | n > 1 && n < 33} (n :a, base : int n) :<!wrt> void implement{a} print_base(n,base) = put_string(itoa($UN.cast{int}(n), base)) macdef println_hex(s) = (put_string "0x"; println_base(,(s), 16)) diff --git a/lib/DATS/init.dats b/lib/DATS/init.dats index a4c84b3..cfdc12e 100644 --- a/lib/DATS/init.dats +++ b/lib/DATS/init.dats @@ -1,3 +1,4 @@ +#include "share/atspre_staload.hats" staload "lib/SATS/init.sats" #define ATS_DYNLOADFLAG 0 @@ -9,15 +10,50 @@ in end -implement{vt} init_exec (x) = - if x.initialized then +implement{vt} exec_void (r) = let + val (vbox pf | p) = ref_get_viewptr{initializable vt}(r) +in + if p->initialized then let - prval () = opt_unsome x.obj - val () = init_exec$fwork (x.obj) - prval () = opt_some x.obj + prval () = opt_unsome p->obj + val () = exec_void$fwork (p->obj) + prval () = opt_some p->obj in end +end -implement{vt} init_exec$fwork (v) = () +implement{vt} exec_void$fwork (v) = () + +implement{vt} {a} exec (r,default) = let + val (vbox pf | p) = ref_get_viewptr{initializable vt}(r) +in + if p->initialized then + let + prval () = opt_unsome p->obj + val a = exec$fwork (p->obj,default) + prval () = opt_some p->obj + in + a + end + else + default +end +implement{vt} {a} exec$fwork (v,default) = default + +implement{vt} initialize (r) = let + val (vbox pf | p) = ref_get_viewptr{initializable vt}(r) +in + if (not p->initialized) then + let + prval () = opt_unnone p->obj + val () = p->initialized := initialize$fwork(p->obj) + in end +end + +implement{vt} initialize$fwork (v) = let + prval () = opt_none v +in + false +end diff --git a/lib/DATS/itoa.dats b/lib/DATS/itoa.dats index 2fef14c..29697b5 100644 --- a/lib/DATS/itoa.dats +++ b/lib/DATS/itoa.dats @@ -3,8 +3,8 @@ #define ATS_DYNLOADFLAG 0 -fun reverse {l : addr} {n,m:nat | n < m} (pf : !(@[char][m] @ l) | p : ptr l, n : int n) : void = let - fun loop {i,j,n:nat | i < j && j < n} (pf : !(@[char][n] @ l) | p : ptr l , i : int i, j : int j) : void = let +fn reverse {l : addr} {n,m:nat | n < m} (pf : !(@[char][m] @ l) | p : ptr l, n : int n) :<!wrt> void = let + fun loop {i,j,n:nat | i < j && j < n} .<j-i>. (pf : !(@[char][n] @ l) | p : ptr l , i : int i, j : int j) :<!wrt> void = let val tmp = p->[i] in p->[i] := p->[j]; @@ -23,7 +23,7 @@ local staload UN = "prelude/SATS/unsafe.sats" -extern castfn char_arr2string (arr : &(@[char][BUFFER_SIZE])) : [n : nat | n < BUFFER_SIZE] string n +extern castfn char_arr2string (arr : &(@[char][BUFFER_SIZE])) :<> [n : nat | n < BUFFER_SIZE] string n extern praxi __assert {l:addr} (ptr: ptr (l)): vtakeout0 (@[char][BUFFER_SIZE]@l) var buffer : @[char][BUFFER_SIZE] // Size should be BUFFER_SIZE @@ -31,12 +31,12 @@ in //TODO: make function better by handling to large number for buffer -extern fun itoa {n:nat | n > 1 && n < 33} (value : int, base : int n) : [k : nat | k < BUFFER_SIZE] string k +extern fun itoa {n:nat | n > 1 && n < 33} (value : int, base : int n) :<!wrt> [k : nat | k < BUFFER_SIZE] string k implement itoa(value,base) = let prval (pf , fpf) = __assert(addr@buffer) // Get proofs UNSAFE: val offset = (if(value < 0) then 1 else 0) : [n: nat | n == 0 || n == 1] int n - fun loop {i : nat | i < BUFFER_SIZE} {l:addr} (pf : !(@[char][BUFFER_SIZE] @ l) | p : ptr l , n : int, i : int i): void = let + fun loop {i : nat | i < BUFFER_SIZE} {l:addr} .<BUFFER_SIZE - i>. (pf : !(@[char][BUFFER_SIZE] @ l) | p : ptr l , n : int, i : int i):<!wrt> void = let val r = n % base val k = n / base in diff --git a/lib/DATS/writer.dats b/lib/DATS/writer.dats index 9b2fd78..b8625f4 100644 --- a/lib/DATS/writer.dats +++ b/lib/DATS/writer.dats @@ -97,31 +97,27 @@ in in implement put_string (str : string) : void = let - val (vbox pf | p) = ref_get_viewptr(writer_ref) - implement init_exec$fwork<writer_t>(v) = let + implement exec_void$fwork<writer_t>(v) = let implement string_foreach$fwork<writer_t> (c,env) = put_char(c,env) val _ = $effmask_all(string_foreach_env<writer_t> (g1ofg0(str),v)) in end in - init_exec<writer_t>(!p) + $effmask_ref(exec_void<writer_t>(writer_ref)) end implement clear_screen() : void = let - val (vbox pf | p) = ref_get_viewptr(writer_ref) - implement init_exec$fwork<writer_t>(v) = _clear_screen(v) + implement exec_void$fwork<writer_t>(v) = _clear_screen(v) + implement initialize$fwork<writer_t>(v) = + ( + v := @{position = 0, color_code = code_value(White,Black)}; + let prval() = opt_some v in true end + ) in - if p->initialized then - init_exec<writer_t> (!p) - else - let - prval () = opt_unnone p->obj - val () = p->obj := @{position = 0, color_code = code_value(White,Black)} - val () = p->initialized := true - val () = _clear_screen(p->obj) - prval () = opt_some p->obj - in - end + if not writer_ref->initialized then + initialize<writer_t>(writer_ref); + + exec_void<writer_t>(writer_ref) end end diff --git a/lib/SATS/init.sats b/lib/SATS/init.sats index 676657b..8219de1 100644 --- a/lib/SATS/init.sats +++ b/lib/SATS/init.sats @@ -3,6 +3,12 @@ viewtypedef initializable (vt:viewt@ype) = fun {vt:viewt@ype} uninitialized (v : opt(vt,false)): initializable vt -fun {vt:viewt@ype} init_exec (x : &(initializable vt)):<!wrt> void -fun {vt:viewt@ype} init_exec$fwork (v : &vt):<!wrt> void +fun {vt:viewt@ype} exec_void (r: ref(initializable vt)):<!refwrt> void +fun {vt:viewt@ype} exec_void$fwork (v : &vt):<!wrt> void + +fun {vt:viewt@ype} {a: t@ype} exec (r: ref(initializable vt), default: a):<!refwrt> a +fun {vt:viewt@ype} {a: t@ype} exec$fwork (v : &vt, default: a):<!wrt> a + +fun {vt:viewt@ype} initialize (r: ref(initializable vt)):<!ref,!wrt> void +fun {vt:viewt@ype} initialize$fwork (v: &vt? >> opt(vt,success)):<!wrt> #[success : bool] bool success diff --git a/lib/SATS/writer.sats b/lib/SATS/writer.sats index 14773ea..b23213f 100644 --- a/lib/SATS/writer.sats +++ b/lib/SATS/writer.sats @@ -22,5 +22,5 @@ datatype color = typedef screenChar = @{ ascii_character = char, color_code = uint8} -fun put_string (str : string) : void -fun clear_screen() : void +fn put_string (str : string) :<!wrt> void +fn clear_screen() : void |