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
|
default Order dec
$include <prelude.sail>
val extz : forall 'm 'n, 'm >= 0 & 'n >= 0. (implicit('n), bits('m)) -> bits('n)
function extz(n, v) = sail_mask(n, v)
/* Test monomorphisation control dependencies */
val f : (bool,bool) -> unit
function f(nosplit,split) = {
if nosplit then {
let 'x : {'x, 'x >= 0. int('x)} = if split then 16 else 32 in
let v : bits('x) = extz(0b0) in
()
} else ()
}
val g : (bool,bool) -> unit
function g(split,nosplit) = {
x : {'x, 'x >= 0. int('x)} = 16;
y : {'y, 'y >= 0. int('y)} = 16;
if split then
x = 32
else
();
if nosplit then
y = 32
else
();
let 'z : {'z, 'z >= 0. int('z)} = x in
let v : bits('z)= extz(0b0) in
()
}
type exception = unit
val h : bool -> unit
/* Note: we don't really need to split on b, but it's awkward to avoid.
The important bit is not to overreact to the exception. */
function h(b) = {
let 'x : {'x, 'x >= 0. int('x)} =
if b then 16 else throw () in
let v : bits('x) = extz(0b0) in
()
}
// A common pattern in current Arm decode functions (where undefined is
// actually implementation defined)
val i : bool -> unit
function i(b) = {
x : {16,32} = 16;
if b then {
x = 32;
} else {
if undefined then {
x = 16;
} else {
throw ();
}
};
let 'x = x;
let v : bits('x) = extz(0b0) in
()
}
val run : unit -> unit
function run () = {
assert(true);
f(false,false);
f(false,true);
g(false,false);
g(false,true);
h(true);
i(true);
}
|
