From 7fce269442cb37810a14d088ea4a61d040ec3066 Mon Sep 17 00:00:00 2001 From: Xander Date: Sun, 20 Aug 2023 14:15:29 +0200 Subject: Rewrite table --- kernel/memory/paging/table.sats | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) (limited to 'kernel/memory/paging/table.sats') diff --git a/kernel/memory/paging/table.sats b/kernel/memory/paging/table.sats index 9a103f4..491b77e 100644 --- a/kernel/memory/paging/table.sats +++ b/kernel/memory/paging/table.sats @@ -4,16 +4,24 @@ staload "./entry.sats" staload "lib/SATS/valid.sats" staload "lib/DATS/valid.dats" -typedef table_t = @[entry_t][ENTRY_COUNT] +vtypedef tablePtr1(level : int) = [l : agz] (@[entry_t][ENTRY_COUNT]@l , @[entry_t][ENTRY_COUNT]@l - void, uint level | ptr l) -vtypedef tablePtr1(c : int) = @{ - ptr = [l : agz] (table_t@l , table_t@l - void | ptr l), - level = (uint c | ) - } +absvt@ype table_t(level:int) = tablePtr1 level + +vtypedef Table_t = [level:nat | level < 4] table_t(level) + +fun table_get_at{n:int}(table: !table_t(n), i: sizeLt(ENTRY_COUNT)):<> entry_t + +fun table_set_at{n:int}(table: !table_t(n), i: sizeLt(ENTRY_COUNT), x: entry_t): void + +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 +fn set_zero(&Table_t): void + +castfn consume(Table_t): void -fun get_P4() : tablePtr1(0) +fun get_P4() : table_t 0 -fun next_table{n : nat | n < 3}(tablePtr1(n), sizeLt(ENTRY_COUNT)) : Valid (tablePtr1(n+1)) +fun next_table{n : nat | n < 3}(table_t n, sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1)) -- cgit v1.2.3