From fcf755d4f03f6fba974d11307659e2e96f9696e7 Mon Sep 17 00:00:00 2001 From: Xander Date: Sat, 19 Aug 2023 15:04:23 +0200 Subject: Implemented entry --- kernel/memory/frame.dats | 6 +++-- kernel/memory/frame.sats | 4 +++ kernel/memory/paging.dats | 36 ------------------------- kernel/memory/paging.sats | 35 ------------------------- kernel/memory/paging/entry.dats | 52 +++++++++++++++++++++++++++++++++++++ kernel/memory/paging/entry.sats | 34 ++++++++++++++++++++++++ kernel/prelude/SATS/safe_casts.sats | 5 +++- 7 files changed, 98 insertions(+), 74 deletions(-) delete mode 100644 kernel/memory/paging.dats delete mode 100644 kernel/memory/paging.sats create mode 100644 kernel/memory/paging/entry.dats create mode 100644 kernel/memory/paging/entry.sats diff --git a/kernel/memory/frame.dats b/kernel/memory/frame.dats index aa02134..867096a 100644 --- a/kernel/memory/frame.dats +++ b/kernel/memory/frame.dats @@ -12,8 +12,10 @@ staload UN = "prelude/SATS/unsafe.sats" implement containing_address(address) = @{ - counter = $UN.cast{size_t}(address) / i2sz(PAGE_SIZE) - } + num = $UN.cast{size_t}(address) / i2sz(PAGE_SIZE) + } + +implement start_address(frame) = sz_to_Ptr0(frame.num * PAGE_SIZE) fn containing_area(area : $BOOT.memory_area_t) :<> frame_t = containing_address(ptr_add(area.base_addr,area.length - i2sz(1))) diff --git a/kernel/memory/frame.sats b/kernel/memory/frame.sats index dfd422e..6580ab0 100644 --- a/kernel/memory/frame.sats +++ b/kernel/memory/frame.sats @@ -2,6 +2,9 @@ staload "kernel/bootinfo/multiboot.sats" +// Physical address type +typedef paddr = Ptr0 + typedef frame_t = @{ num = size_t } @@ -16,6 +19,7 @@ typedef frame_allocator_t = @{ } fn containing_address{l:addr}(ptr l):<> frame_t +fn start_address(frame_t):<> paddr fn allocate_frame () : frame_t fn deallocate_frame () : void diff --git a/kernel/memory/paging.dats b/kernel/memory/paging.dats deleted file mode 100644 index 84a8bf4..0000000 --- a/kernel/memory/paging.dats +++ /dev/null @@ -1,36 +0,0 @@ -#define ATS_DYNLOADFLAG 0 - -#include "kernel/prelude/kernel_prelude.hats" - -staload UN = "prelude/SATS/unsafe.sats" - -staload "./paging.sats" -staload "./frame.sats" -staload "lib/SATS/valid.sats" - -assume entry_type = uint64 - -val zero = u2uint64(0u) - -implement is_unused(entry) = entry = zero -implement set_unused(entry) = entry := zero - -implement flag_contains(entry,flag) = - (entry land $UN.cast{uint64}(1 << (case+ flag of - | PRESENT() => 0 - | WRITABLE() => 1 - | USER_ACCESSIBLE() => 2 - | WRITE_THROUGH() => 3 - | NO_CACHE() => 4 - | ACCESSED() => 5 - | DIRTY() => 6 - | HUGE_PAGE() => 7 - | GLOBAL() => 8 - | NO_EXECUTE() => 63 - ))) != zero - -(* implement test() = let *) -(* in *) -(* (5,true) *) -(* end *) - diff --git a/kernel/memory/paging.sats b/kernel/memory/paging.sats deleted file mode 100644 index 477e942..0000000 --- a/kernel/memory/paging.sats +++ /dev/null @@ -1,35 +0,0 @@ -#define ENTRY_COUNT 512 - -staload "./frame.sats" -staload "lib/SATS/valid.sats" - -abstype paddr_type(l:addr) = ptr(l) -typedef paddr(l:addr) = paddr_type(l) - -abstype vaddr_type(l:addr) = ptr(l) -typedef vaddr(l:addr) = vaddr_type(l) - -abst@ype entry_type = uint64 -typedef entry_t = entry_type - -typedef page_t = @{ - num = size_t -} - -datatype entry_flag = - | PRESENT - | WRITABLE - | USER_ACCESSIBLE - | WRITE_THROUGH - | NO_CACHE - | ACCESSED - | DIRTY - | HUGE_PAGE - | GLOBAL - | NO_EXECUTE - -fn is_unused(entry_t) : bool -fn set_unused(&entry_t) : void - -fn flag_contains(entry_t,entry_flag) : bool -fn test() : [b : bool] valid(int,b) diff --git a/kernel/memory/paging/entry.dats b/kernel/memory/paging/entry.dats new file mode 100644 index 0000000..7fa97b9 --- /dev/null +++ b/kernel/memory/paging/entry.dats @@ -0,0 +1,52 @@ +#define ATS_DYNLOADFLAG 0 + +#include "kernel/prelude/kernel_prelude.hats" + +staload UN = "prelude/SATS/unsafe.sats" + +staload "./entry.sats" +staload FRAME = "kernel/memory/frame.sats" +staload "lib/SATS/valid.sats" +staload "lib/DATS/valid.dats" + +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 + | PRESENT() => 0 + | WRITABLE() => 1 + | USER_ACCESSIBLE() => 2 + | WRITE_THROUGH() => 3 | NO_CACHE() => 4 + | ACCESSED() => 5 + | DIRTY() => 6 + | HUGE_PAGE() => 7 + | GLOBAL() => 8 + | NO_EXECUTE() => 63 + )) + var k = g0ofg1(u2u64(0u)) + val _ = array_foreach_env(arr,n,k) +in + k +end + +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) +} + +implement pointed_frame(entry) = + if contains_flag(entry,PRESENT) then + create_valid($FRAME.containing_address(u64_to_Ptr0(entry land u2u64(0x000FFFFFFFFFF000u)))) + else + create_unvalid() + +implement entry_set(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)) +end diff --git a/kernel/memory/paging/entry.sats b/kernel/memory/paging/entry.sats new file mode 100644 index 0000000..a7f91ee --- /dev/null +++ b/kernel/memory/paging/entry.sats @@ -0,0 +1,34 @@ +#define ENTRY_COUNT 512 + +staload "kernel/memory/frame.sats" +staload "lib/SATS/valid.sats" + +abstype vaddr_type(l:addr) = ptr(l) +typedef vaddr(l:addr) = vaddr_type(l) + +abst@ype entry_type = uint64 +typedef entry_t = entry_type + +typedef page_t = @{ + num = size_t +} + +datatype entry_flag = + | PRESENT + | WRITABLE + | USER_ACCESSIBLE + | WRITE_THROUGH + | NO_CACHE + | ACCESSED + | DIRTY + | HUGE_PAGE + | GLOBAL + | NO_EXECUTE + +fn is_unused(entry_t) : bool +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 diff --git a/kernel/prelude/SATS/safe_casts.sats b/kernel/prelude/SATS/safe_casts.sats index 50a68a8..f8e34db 100644 --- a/kernel/prelude/SATS/safe_casts.sats +++ b/kernel/prelude/SATS/safe_casts.sats @@ -1 +1,4 @@ -castfn u2uint64{v : nat | v <= 0xFFFFFFFFFFFFFFFF}(v : uint v) : uint64 v +castfn u2u64{v : nat | v <= 0xFFFFFFFFFFFFFFFF}(v : uint v) :<> uint64 v +castfn u64_to_Ptr0(v : uint64):<> Ptr0 +castfn Ptr0_to_u64(v : Ptr0):<> uint64 +castfn sz_to_Ptr0(v : size_t):<> Ptr0 -- cgit v1.2.3