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
|
(* hack to display log messages. Syntax: LOG(0) := "log message"; *)
val extern forall Type 'a . nat -> 'a effect { wmem , rmem } LOG
register (bit[1]) GPR0
register (bit[1]) GPR1
let (vector <0, 2, inc, (register<bit[1] >)>) GPR = [ GPR0, GPR1 ]
(* if we access GPR with a bit or a nat - doing the conversion in the
caller, works as expected *)
function unit good ((bit) RA ) =
{
LOG(0) := "good";
(nat) x := GPR[RA];
}
function unit good2 ((nat) RA ) =
{
LOG(0) := "good2";
(nat) x := GPR[RA];
}
(* but here, the first to_num_inc(RA) somehow inhibits the cast,
yielding to_num_inc(GPR0) instead of to_num_inc(0b0) *)
function unit bad ((bit[1]) RA ) =
{
LOG(0) := "oldbad";
(nat) x := GPR[RA];
}
(* and now, another bug - when DCR contains registers of bits instead of bit[0] *)
register (bit) DCR0
register (bit) DCR1
let (vector <0, 2, inc, (register<bit >)>) DCR = [ DCR0, DCR1 ]
(* also fails only when passing RA as a vector, nat and bit work fine as
above;
error message is different though, and very disturbing:
"error: No matching patterns in case", corresponding to the DCR[RA]
expression *)
function unit bad2 ((bit[1]) RA ) =
{
LOG(0) := "oldbad2";
(nat) x := DCR[RA];
}
function unit main () = {
LOG(0) := "init";
GPR[0] := 0b0;
GPR[1] := 0b1;
DCR[0] := bitzero;
DCR[1] := bitone;
good(bitzero);
good2(0);
(* a first bug *)
bad(0b0);
(* another bug :-) comment out first one to see it *)
bad2(0b0);
}
|
