diff options
Diffstat (limited to 'kernel/memory/paging/table.dats')
-rw-r--r-- | kernel/memory/paging/table.dats | 68 |
1 files changed, 68 insertions, 0 deletions
diff --git a/kernel/memory/paging/table.dats b/kernel/memory/paging/table.dats new file mode 100644 index 0000000..d5029a7 --- /dev/null +++ b/kernel/memory/paging/table.dats @@ -0,0 +1,68 @@ +#define ATS_DYNLOADFLAG 0 + +#include "kernel/prelude/kernel_prelude.hats" + +staload "./table.sats" +staload "./entry.sats" + +staload "lib/SATS/valid.sats" +staload "lib/DATS/valid.dats" + +// Calculate table address of next table based on current table and index: P4->P3->P2->P1 +fn next_table_address{l:agz}(pf : !table_t@l | p : ptr(l), index : sizeLt(ENTRY_COUNT)) : Valid Ptr1 = let + val entry = p->[index] +in + if (contains_flag(entry,PRESENT) && ~contains_flag(entry,HUGE_PAGE)) then + let + val next = g1ofg0((Ptr1_to_sz(p) << 9) lor (index << 12)) + in + if next > i2sz(0) then + create_valid(sz_to_Ptr1(next)) + else + create_unvalid() + end + else + create_unvalid() +end + +implement set_zero(table) = let + implement array_foreach$fwork<entry_t><void>(entry,v) = set_unused(entry) +in + assertloc(array_foreach<entry_t>(table,i2sz(ENTRY_COUNT)) = i2sz(ENTRY_COUNT)) +end + +// UNSAFE: unsafe block +local + + staload UN = "prelude/SATS/unsafe.sats" + +in + + implement get_P4() = @{ + ptr = $UN.ptr_vtake(ulint_to_Ptr1(0xfffffffffffff000ul)), + level = (0u | ) + } + + implement next_table(tp,index) = let + val k = tp.ptr + val next = next_table_address(k.0 | k.2,index) + prval () = k.1 k.0 + in + if is_valid(next) then + let + val p = unwrap_valid(next) + in + create_valid(@{ + ptr = $UN.ptr_vtake(p), + level = ( succ(tp.level.0) | ) + }) + end + else + let + val () = destroy_unvalid(next) + in + create_unvalid() + end + end + +end |