aboutsummaryrefslogtreecommitdiff
path: root/kernel/memory/paging.sats
blob: 477e9425f48a63971a3a97a2da2b337ba64b7b13 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
#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)