bitmap.bend

bend-osdev-algo@0.1.0.0 · 72 lines · 8 definitions

1# bend-osdev-algo, bitmaps: a bitmap is a List<&2, U32> of words, bit i in
2# word i / 32 at position i mod 32, as the kernel lays out its bitmaps.
3# next_set and next_clear find the next set or clear bit at or after an
4# index and below a size, and answer the size when there is none (the
5# kernel's find_next_bit and find_next_zero_bit).
6import Base
7import bend-osdev-algo@0.1.0.0/algo.bend as A
8
9# Bit sequences
10
11# bit i (False past the end)
12def bitseq.at(bs: List<&2, Bool>, i: Nat) -> Bool:
13  match bs i:
14    case Nil{} _:
15      False{}
16    case Con{h, t} 0n:
17      h
18    case Con{h, t} 1n+j:
19      bitseq.at(t, j)
20
21# the least i with start <= i < size whose bit is want, or size if there is
22# none (bits past the end of bs are clear)
23def bitseq.next(size: Nat, start: Nat, want: Bool, bs: List<&2, Bool>) -> Nat:
24  match size:
25    case 0n:
26      0n
27    case 1n+s:
28      match start want bs:
29        case 1n+st w Nil{}:
30          1n+bitseq.next(s, st, w, Nil{})
31        case 1n+st w Con{h, t}:
32          1n+bitseq.next(s, st, w, t)
33        case 0n False{} Nil{}:
34          0n
35        case 0n True{} Nil{}:
36          1n+s
37        case 0n True{} Con{True{}, t}:
38          0n
39        case 0n False{} Con{False{}, t}:
40          0n
41        case 0n True{} Con{False{}, t}:
42          1n+bitseq.next(s, 0n, True{}, t)
43        case 0n False{} Con{True{}, t}:
44          1n+bitseq.next(s, 0n, False{}, t)
45
46# Bitmaps
47
48# the bits of the words, bit 0 of the first word first
49def bitmap.bits(words: List<&2, U32>) -> List<&2, Bool>:
50  match words:
51    case Nil{}:
52      Nil{}
53    case Con{x, t}:
54      A.bitw.to_list(32n, A.bits32.word(x), bitmap.bits(t))
55
56# bit i of the bitmap (False past its end)
57def bitmap.test(words: List<&2, U32>, i: Nat) -> Bool:
58  bitseq.at(bitmap.bits(words), i)
59
60# the first set bit at or after start and below size, or size
61def bitmap.next_set(words: List<&2, U32>, size: Nat, start: Nat) -> Nat:
62  bitseq.next(size, start, True{}, bitmap.bits(words))
63
64# the first clear bit at or after start and below size, or size
65def bitmap.next_clear(words: List<&2, U32>, size: Nat, start: Nat) -> Nat:
66  bitseq.next(size, start, False{}, bitmap.bits(words))
67
68def bitmap.first_set(words: List<&2, U32>, size: Nat) -> Nat:
69  bitmap.next_set(words, size, 0n)
70
71def bitmap.first_clear(words: List<&2, U32>, size: Nat) -> Nat:
72  bitmap.next_clear(words, size, 0n)