diff options
author | Xander <xander@biltopia.org> | 2023-08-19 15:04:23 +0200 |
---|---|---|
committer | Xander <xander@biltopia.org> | 2023-08-19 15:19:25 +0200 |
commit | fcf755d4f03f6fba974d11307659e2e96f9696e7 (patch) | |
tree | a58d9b7b24d6ab4b80f854d6d3905246b37494bd /kernel | |
parent | d177285a761de33b86fcbde72fd718137bfa6f86 (diff) | |
download | ats-os-fcf755d4f03f6fba974d11307659e2e96f9696e7.tar.xz ats-os-fcf755d4f03f6fba974d11307659e2e96f9696e7.zip |
Implemented entry
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/memory/frame.dats | 6 | ||||
-rw-r--r-- | kernel/memory/frame.sats | 4 | ||||
-rw-r--r-- | kernel/memory/paging.dats | 36 | ||||
-rw-r--r-- | kernel/memory/paging/entry.dats | 52 | ||||
-rw-r--r-- | kernel/memory/paging/entry.sats (renamed from kernel/memory/paging.sats) | 11 | ||||
-rw-r--r-- | kernel/prelude/SATS/safe_casts.sats | 5 |
6 files changed, 69 insertions, 45 deletions
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<uint8>(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/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<entry_flag><entry_t>(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<entry_flag><entry_t>(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.sats b/kernel/memory/paging/entry.sats index 477e942..a7f91ee 100644 --- a/kernel/memory/paging.sats +++ b/kernel/memory/paging/entry.sats @@ -1,11 +1,8 @@ #define ENTRY_COUNT 512 -staload "./frame.sats" +staload "kernel/memory/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) @@ -31,5 +28,7 @@ datatype entry_flag = 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) +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 |