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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
|
val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
/* *** Register reference list example *** */
type regno ('n : Int), 0 <= 'n < 4 = atom('n)
/* regiser x0 : bits(32) is always 0 */
register x1 : bits(32)
register x2 : bits(32)
register x3 : bits(32)
let GPRs : vector(3, dec, register(bits(32))) =
[ ref x3, ref x2, ref x1 ]
val rGPR : forall 'n, 0 <= 'n < 4. regno('n) -> bits(32) effect {rreg}
function rGPR 0 = 0x00000000
and rGPR (r if r > 0) = reg_deref(GPRs[r - 1])
val wGPR : forall 'n, 1 <= 'n < 4. (regno('n), bits(32)) -> unit effect {wreg}
function wGPR (r, v) = {
print_int("Register ", r);
print_bits("Assigning ", v);
(*GPRs[r - 1]) = v
}
overload _mod_GPR = { rGPR, wGPR }
/* *** Power style vector slicing *** */
/* Create a new type which is a pair of a bitvector and a start index
slice('n, 'm) is equivalent to old-sail vector('n, 'm, dec, bit) */
newtype slice ('n : Int, 'm : Int) = MkSlice : (atom('n), bits('m))
/* Extract the bitvector from a slice */
val slice_bits : forall 'n 'm. slice('n, 'm) -> bits('m)
function slice_bits MkSlice(_, xs) = xs
/* Take a slice from a bitvector */
val vector_slice : forall 'n 'm 'o, 0 <= 'm <= 'o < 'n.
(bits('n), atom('o), atom('m)) -> slice('m, 'o - ('m - 1))
function vector_slice (v, to, from) = MkSlice(from, v[to .. from])
val slice_slice : forall 'n 'm 'o 'p, 0 <= 'p <= 'm <= 'o & 'o - 'p < 'n.
(slice('p, 'n), atom('o), atom('m)) -> slice('m, 'o - ('m - 1))
function slice_slice (MkSlice(start, v), to, from) = MkSlice(from, v[to - start .. from - start])
/* We can update a bitvector from another bitvector or a slice */
val _set_slice : forall 'n 'm 'o, 0 <= 'm <= 'o < 'n.
(register(bits('n)), atom('o), atom('m), bits('o - ('m - 1))) -> unit effect {wreg, rreg}
function _set_slice (v, stop, start, update) = {
v2 = reg_deref(v);
v2[stop .. start] = update;
(*v) = v2;
}
val _set_slice2 : forall 'n 'm 'o 'p, 0 <= 'm <= 'o < 'n.
(register(bits('n)), atom('o), atom('m), slice('p, 'o - ('m - 1))) -> unit effect {wreg, rreg}
function _set_slice2 (v, stop, start, MkSlice(_, update)) = _set_slice(v, stop, start, update)
val slice_bit : forall 'n. slice('n, 1) -> bit
function slice_bit MkSlice(_, [b]) = b
/* Overload slice modifier */
overload _mod_slice = {_set_slice, _set_slice2, vector_slice, slice_slice}
/* Set up a struct with an aliased LT bit in CR0, mimicing old-style syntax */
infix 1 ...
type operator ...('n : Int, 'm : Int) = slice('m, 'n - ('m - 1))
struct cr = {
CR0 : 7 ... 4,
/* 7 : LT; 6 : GT; 5 : EQ; 4 : SO; */
CR1 : 3 ... 2,
CR3 : 1 ... 0,
}
register CR : cr
val _get_LT : cr -> bit
val _set_LT : (register(cr), bit) -> unit effect {rreg, wreg}
function _get_LT cr = slice_bit(cr.CR0.slice(7, 7))
function _set_LT (cr_ref, b) = {
cr = reg_deref(cr_ref);
cr.CR0 = MkSlice(4, [slice_bits(cr.CR0) with (7 - 4) = b]);
(*cr_ref) = cr;
}
overload _mod_LT = {_get_LT, _set_LT}
/* *** Test Program *** */
val main : unit -> unit effect {wreg, rreg}
val print_regs : unit -> unit effect {rreg}
function print_regs () = {
print_bits("1 = ", rGPR(1));
print_bits("2 = ", rGPR(2));
print_bits("3 = ", rGPR(3));
}
register b : bits(5)
function main () = {
print("Testing register references");
wGPR(1) = 0x00000000;
wGPR(2) = 0x00000000;
wGPR(3) = 0x00000000;
print_regs ();
/* Assign to lowest assignable register */
wGPR(1) = 0xCAFEBEEF;
print_regs ();
/* Reading to variable */
print("Reading 1 to variable");
v = rGPR(1);
print_bits("v = ", v);
/* Assign to highest register */
wGPR(3) = 0x00BEEF00;
print_regs ();
print("Reading zero register");
print_bits("0 = ", rGPR(0));
/* Test overloaded version */
_mod_GPR(2) = 0xDEADCAFE;
print_bits("2 = ", _mod_GPR(2));
/* Method syntax */
print("Assigning register 2 to register 1");
2.GPR() = 1.GPR();
print_regs();
/* Slice testing */
print("\nTesting slicing");
let s = 0b01110.slice(3, 1);
print_bits("s = ", slice_bits(s));
let s = 0b01110.slice(4, 0);
print_bits("s = ", slice_bits(s));
let s = 0b01110.slice(3, 0);
print_bits("s = ", slice_bits(s));
/* Updating slices */
b = 0b01110;
print_bits("b = ", b);
b->slice(3, 1) = 0b101;
print_bits("b = ", b);
b->slice(2, 0) = 0xFF.slice(5, 3);
print_bits("b = ", b);
/* Bit aliasing */
print("\nTesting bit aliasing");
print_bits("CR0 = ", slice_bits(CR.CR0));
print_bits("LT = ", [CR.LT()]);
print("Setting LT to bitone");
CR->LT() = bitone;
print_bits("CR0 = ", slice_bits(CR.CR0));
print_bits("LT = ", [CR.LT()]);
print("Setting CR0 to 0b0111");
CR.CR0 = MkSlice(4, 0b0111);
print_bits("CR0 = ", slice_bits(CR.CR0));
print_bits("LT = ", [CR.LT()]);
}
|
