From 70cca66089896730797a71ba545c7f4e87b12975 Mon Sep 17 00:00:00 2001 From: Xander Date: Sun, 20 Aug 2023 22:57:07 +0200 Subject: implement page --- kernel/main.dats | 37 +++++++++--- kernel/memory/paging/entry.dats | 14 +++-- kernel/memory/paging/entry.sats | 4 +- kernel/memory/paging/page.dats | 117 ++++++++++++++++++++++++++++++++++++ kernel/memory/paging/page.sats | 18 ++++++ kernel/memory/paging/table.dats | 44 +++++++++++++- kernel/memory/paging/table.sats | 9 ++- kernel/prelude/SATS/safe_casts.sats | 1 + lib/DATS/valid.dats | 2 +- lib/SATS/valid.sats | 11 ++-- 10 files changed, 227 insertions(+), 30 deletions(-) create mode 100644 kernel/memory/paging/page.dats create mode 100644 kernel/memory/paging/page.sats diff --git a/kernel/main.dats b/kernel/main.dats index 65cb8df..f18c2e1 100644 --- a/kernel/main.dats +++ b/kernel/main.dats @@ -3,6 +3,12 @@ staload "kernel/interrupts/idt.sats" staload BOOT = "kernel/bootinfo/multiboot.sats" staload FRAME = "kernel/memory/frame.sats" +staload ENTRY = "kernel/memory/paging/entry.sats" +staload PAGE = "kernel/memory/paging/page.sats" + +staload "lib/SATS/valid.sats" +staload "lib/DATS/valid.dats" + staload "lib/SATS/writer.sats" #define ATS_DYNLOADFLAG 0 @@ -28,9 +34,27 @@ in end fn test() : void = let - fun loop(i : int) : void = if (i < 160) then( let val _ = $FRAME.allocate_frame() in end; loop(succ(i))) + val a = sz_to_Ptr0(i2sz(42 * 512 * 512 * 4096)); // 42th P3 entry + val page = $PAGE.containing_address(a) + val () = println!("page num: ", page.num) + val frame = $FRAME.allocate_frame() + var flags = @[$ENTRY.entry_flag]($ENTRY.WRITABLE) + val () = $PAGE.map_to(page,frame,flags,i2sz(1)) + val aframe = $PAGE.translate(a) + val frame2 = $FRAME.allocate_frame() + (* val () = println!("Map to ", frame.num) *) in - loop(0) + if (is_valid(aframe)) then + let + val vframe = unwrap_valid(aframe) + in + println!("Got ",vframe) + end + else ( + destroy_unvalid(aframe); + println!("Unvalid aframe") + ); + println!("frame2: ", frame2.num) end @@ -45,16 +69,11 @@ implement main(p) = let val () = $FRAME.init(kernel_start,kernel_end,multiboot_start,multiboot_end); in - $BOOT.print_memory_mappings(); - $BOOT.print_elf_headers(); + (* $BOOT.print_memory_mappings(); *) + (* $BOOT.print_elf_headers(); *) println!("Kernel Size: ", kernel_size(kernel_start,kernel_end)); test(); - let - val frame = $FRAME.allocate_frame() - in - println!(frame.num) - end; // Initialize interrupt table idt_init(); diff --git a/kernel/memory/paging/entry.dats b/kernel/memory/paging/entry.dats index 7fa97b9..76d6c0c 100644 --- a/kernel/memory/paging/entry.dats +++ b/kernel/memory/paging/entry.dats @@ -13,8 +13,7 @@ assume entry_type = uint64 val zero = u2u64(0u) -fn flags2entry{n:nat}(arr : &(@[entry_flag][n]), n: size_t n) : entry_t = let - implement array_foreach$fwork(f,k) = k := k lor $UN.cast{entry_t}(1 << (case+ f of +implement add_flag(entry,f) = entry lor $UN.cast{entry_t}(1 << (case+ f of | PRESENT() => 0 | WRITABLE() => 1 | USER_ACCESSIBLE() => 2 @@ -25,8 +24,11 @@ fn flags2entry{n:nat}(arr : &(@[entry_flag][n]), n: size_t n) : entry_t = let | GLOBAL() => 8 | NO_EXECUTE() => 63 )) + +fn flags2entry{n:nat}(arr : &(@[entry_flag][n]), n: size_t n) :<> entry_t = let + implement array_foreach$fwork(f,k) = k := add_flag(k,f) var k = g0ofg1(u2u64(0u)) - val _ = array_foreach_env(arr,n,k) + val _ = $effmask_all(array_foreach_env(arr,n,k)) in k end @@ -35,7 +37,7 @@ implement is_unused(entry) = entry = zero implement set_unused(entry) = entry := zero implement contains_flag(entry,flag) = (flags2entry(flags,i2sz(1)) land entry) != zero where { - var flags = @[entry_flag](PRESENT) + var flags = @[entry_flag](flag) } implement pointed_frame(entry) = @@ -44,9 +46,9 @@ implement pointed_frame(entry) = else create_unvalid() -implement entry_set(entry,frame,flags,n) = let +implement create_entry(frame,flags,n) = let val x = Ptr0_to_u64($FRAME.start_address(frame)) in assertloc((x land u2u64(0xFFF0000000000FFFu)) = zero); - entry := (x lor flags2entry(flags,n)) + (x lor flags2entry(flags,n)) end diff --git a/kernel/memory/paging/entry.sats b/kernel/memory/paging/entry.sats index 17a9f72..fc20a20 100644 --- a/kernel/memory/paging/entry.sats +++ b/kernel/memory/paging/entry.sats @@ -1,5 +1,6 @@ staload "kernel/memory/frame.sats" staload "lib/SATS/valid.sats" +staload "lib/DATS/valid.dats" abst@ype entry_type = uint64 typedef entry_t = entry_type @@ -22,4 +23,5 @@ fn set_unused(&entry_t) : void fn contains_flag(entry_t,entry_flag):<> bool fn pointed_frame(entry_t) : Valid frame_t -fn entry_set{n:nat}(&entry_t,frame_t,&(@[entry_flag][n]),size_t n) : void +fn add_flag(entry_t,entry_flag) : entry_t +fn create_entry{s:nat}(frame_t,&(@[entry_flag][s]),size_t s) : entry_t diff --git a/kernel/memory/paging/page.dats b/kernel/memory/paging/page.dats new file mode 100644 index 0000000..2880c18 --- /dev/null +++ b/kernel/memory/paging/page.dats @@ -0,0 +1,117 @@ +#define ATS_DYNLOADFLAG 0 + +#include "kernel/prelude/kernel_prelude.hats" + +staload "./page.sats" +staload FR = "kernel/memory/frame.sats" +staload "./table.sats" + +staload "lib/SATS/valid.sats" +staload "lib/DATS/valid.dats" + +datatype table_level = + | Level4 + | Level3 + | Level2 + | Level1 + +fn start_address(page : page_t) : size_t = page.num * $FR.PAGE_SIZE + +fn get_index(page: page_t,n : intLte(3)) = g1ofg0((page.num >> (27 - 9 * n)) land i2sz(511)) + +//NOTE: huge page handler not implemented +fn translate_page(page: page_t) : Valid $FR.frame_t = let + fun loop{n : nat | n < 3}.<3-n>.(table : table_t n, count : int n) : Valid $FR.frame_t = let + staload "./entry.sats" + val index = get_index(page,count) + in + if index < ENTRY_COUNT then let + val v = next_table(table,index) + in + if is_valid(v) then let + val table_next = unwrap_valid(v) + in + if count < 2 then + loop(table_next,succ(count)) + else( + consume(table_next); + frame + ) where { + val index = get_index(page,count+1) + val frame = (if index < ENTRY_COUNT then pointed_frame(table_next[index]) else create_unvalid()) : Valid $FR.frame_t + } + end + else ( + destroy_unvalid(v); + println!("Unvalid table pointer encountered: ", count); + create_unvalid()) + end + else ( + consume(table); + println!("Table index too big"); + create_unvalid()) + end +in + loop(get_P4(),0) +end + +implement translate(virtual_addr) = let + val offset = Ptr0_to_sz(virtual_addr) % i2sz($FR.PAGE_SIZE) + val vframe = translate_page(containing_address(virtual_addr)) +in + if is_valid(vframe) then let + val frame = unwrap_valid(vframe) + in + create_valid (sz_to_Ptr0(frame.num * $FR.PAGE_SIZE + offset)) + end + else ( + destroy_unvalid(vframe); + create_unvalid(); + ) +end + +implement containing_address(address) = ( + assertloc(address < ulint_to_Ptr0(0x0000800000000000ul) || + address >= ulint_to_Ptr0(0xFFFF800000000000ul)); + @{num = Ptr0_to_sz(address) / i2sz($FR.PAGE_SIZE)} +) + +// TODO: implement and_then and or_else for valid (like in rust) +implement map_to{s}(page,frame,flags,size) = let + staload "./entry.sats" + fun loop{n : nat | n < 3}.<3-n>.(table : table_t n, count : int n, flags: &(@[entry_flag][s])) : void = let + staload "lib/SATS/panic.sats" + val index = get_index(page,count) + val () = println!(index) + in + if index < ENTRY_COUNT then let + val v = next_table_create(table,index) + in + if is_valid(v) then let + val table_next = unwrap_valid(v) + in + if count < 2 then + loop(table_next,succ(count),flags) + else let + val index = get_index(page,count+1) + in + if index < ENTRY_COUNT then ( + assertloc(is_unused(table_next[index])); + table_next[index] := add_flag(create_entry(frame, flags,size),PRESENT); + ); + consume(table_next); + end + end + else ( + destroy_unvalid(v); + panic("Could not create table")) + end + else ( + consume(table); + println!("Table index too big")) + end +in + loop(get_P4(),0,flags) +end + +implement map(page,flags,size) = map_to(page,$FR.allocate_frame(),flags,size) diff --git a/kernel/memory/paging/page.sats b/kernel/memory/paging/page.sats new file mode 100644 index 0000000..1de50c6 --- /dev/null +++ b/kernel/memory/paging/page.sats @@ -0,0 +1,18 @@ +staload FRAME = "kernel/memory/frame.sats" + +staload "lib/SATS/valid.sats" +staload "./entry.sats" + +typedef vaddr = Ptr0 + +typedef page_t = @{ + num = size_t +} + +fn translate(vaddr) : Valid $FRAME.paddr + +fn containing_address(vaddr) : page_t + +fn map_to{n:nat}(page_t,$FRAME.frame_t,&(@[entry_flag][n]),size : size_t n): void + +fn map{n:nat}(page_t,&(@[entry_flag][n]),size : size_t n) : void diff --git a/kernel/memory/paging/table.dats b/kernel/memory/paging/table.dats index e636c6c..d3bfe93 100644 --- a/kernel/memory/paging/table.dats +++ b/kernel/memory/paging/table.dats @@ -28,6 +28,16 @@ in create_unvalid() end +// Checks if next table exists and returns bool +fn next_table_exists{n:int|n < 3}(table: !table_t(n),index : sizeLt(ENTRY_COUNT)):<> bool = let + val vnext = next_table_address(table,index) +in + if is_valid(vnext) then + let val _ = unwrap_valid(vnext) in true end + else + (destroy_unvalid(vnext); false) +end + implement table_get_at(table,i) = let val entry = (table.3->[i]) : entry_t in @@ -36,7 +46,8 @@ end implement table_set_at(table,i,x) = table.3->[i] := x -implement set_zero(table) = let +// Set all the entries in the table to unused (zero) +fn set_zero(table: &Table_t): void = let fun loop{i:nat | i < ENTRY_COUNT}..(i : size_t i,t : !Table_t): void = let in set_unused(t.3->[i]); @@ -54,6 +65,8 @@ local in + // TODO: define safe unique ownership for this table + // see https://os.phil-opp.com/page-tables/#safety-2 implement get_P4() = let val (pf,fpf | p) = $UN.ptr_vtake(ulint_to_Ptr1(0xfffffffffffff000ul)) in @@ -76,7 +89,32 @@ in let val () = destroy_unvalid(next) in - create_unvalid() - end; + create_unvalid(); + end + end + + implement next_table_create(table,index) = let + staload "kernel/memory/frame.sats" + in + if ~next_table_exists(table,index) then ( + println!("not exists"); + assertloc(~contains_flag(table[index],HUGE_PAGE)); + table[index] := create_entry(allocate_frame(),flags,i2sz(2)) where { + var flags = @[entry_flag](PRESENT,WRITABLE) + }; + let + val vnext = next_table(table,index) + in + if is_valid(vnext) then + let var next = unwrap_valid(vnext) in (set_zero(next); create_valid(next)) end + else ( + destroy_unvalid(vnext); + create_unvalid() + ) + end + ) else + $UN.castvwtp0(next_table(table,index)) //This is safe end + end + diff --git a/kernel/memory/paging/table.sats b/kernel/memory/paging/table.sats index 491b77e..6b8e188 100644 --- a/kernel/memory/paging/table.sats +++ b/kernel/memory/paging/table.sats @@ -17,11 +17,10 @@ fun table_set_at{n:int}(table: !table_t(n), i: sizeLt(ENTRY_COUNT), x: entry_t): overload [] with table_get_at overload [] with table_set_at -// Set all the entries in the table to unused (zero) -fn set_zero(&Table_t): void - castfn consume(Table_t): void -fun get_P4() : table_t 0 +fn get_P4() : table_t 0 + +fn next_table{n : nat | n < 3}(table_t n, index : sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1)) -fun next_table{n : nat | n < 3}(table_t n, sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1)) +fn next_table_create{n : nat | n < 3}(table_t n, index : sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1)) diff --git a/kernel/prelude/SATS/safe_casts.sats b/kernel/prelude/SATS/safe_casts.sats index 8850ef6..f93a2be 100644 --- a/kernel/prelude/SATS/safe_casts.sats +++ b/kernel/prelude/SATS/safe_casts.sats @@ -10,3 +10,4 @@ castfn ulint_to_Ptr0(v : ulint):<> Ptr0 castfn sz_to_Ptr0(v : size_t):<> Ptr0 castfn Ptr1_to_sz(v : Ptr1):<> sizeGte(1) +castfn Ptr0_to_sz(v : Ptr0):<> size_t diff --git a/lib/DATS/valid.dats b/lib/DATS/valid.dats index c13386e..7c3bbab 100644 --- a/lib/DATS/valid.dats +++ b/lib/DATS/valid.dats @@ -9,7 +9,7 @@ implement{a} create_valid(value) = (value,true) implement{a} create_unvalid() = let staload UN = "prelude/SATS/unsafe.sats" in - ($UN.ptr0_get(the_null_ptr),false) //UNSAFE: + ($extval(a,"(void *)NULL"),false) //UNSAFE: end implement{a} unwrap_valid(v) = v.0 diff --git a/lib/SATS/valid.sats b/lib/SATS/valid.sats index 83081fe..bfbbc23 100644 --- a/lib/SATS/valid.sats +++ b/lib/SATS/valid.sats @@ -8,16 +8,17 @@ absviewt@ype valid(a:viewt@ype,b:bool) = (a,bool b) viewtypedef Valid(a:viewt@ype) = [b : bool] valid(a,b) // Wraps valid value. -fn {a:viewt@ype} create_valid(a) : valid(a,true) +fn {a:viewt@ype} create_valid(a) :<> valid(a,true) // Creates unvalid type. -fn {a:viewt@ype} create_unvalid() : valid(a,false) +fn {a:viewt@ype} create_unvalid() :<> valid(a,false) // Only function that allows getting value. Only accepts valid values. -fn {a:viewt@ype} unwrap_valid(valid(a,true)) : a +fn {a:viewt@ype} unwrap_valid(valid(a,true)) :<> a -castfn destroy_unvalid{a:viewt@ype}(valid(a,false)) : void +castfn destroy_unvalid{a:viewt@ype}(valid(a,false)) :<> void // Check if value is valid -fn{a:viewt@ype} is_valid{b:bool}(!valid(a,b)) : bool b +fn{a:viewt@ype} is_valid{c:bool}(!valid(a,c) >> valid(a,b)) :<> #[b:bool] bool b + -- cgit v1.2.3