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
|
$ifndef _VECTOR_DEC
$define _VECTOR_DEC
$include <flow.sail>
type bits ('n : Int) = vector('n, dec, bit)
val eq_bit = { lem : "eq", _ : "eq_bit" } : (bit, bit) -> bool
val eq_bits = {
ocaml: "eq_list",
lem: "eq_vec",
c: "eq_bits",
coq: "eq_vec"
} : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool
overload operator == = {eq_bit, eq_bits}
val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) -> atom('n)
val vector_length = {
ocaml: "length",
lem: "length_list",
c: "length",
coq: "length_list"
} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
overload length = {bitvector_length, vector_length}
val sail_zeros = "zeros" : forall 'n. atom('n) -> bits('n)
val "print_bits" : forall 'n. (string, bits('n)) -> unit
val "prerr_bits" : forall 'n. (string, bits('n)) -> unit
val sail_sign_extend = "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
val sail_zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
val truncate = {
ocaml: "vector_truncate",
lem: "vector_truncate",
coq: "vector_truncate",
c: "truncate"
} : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
val sail_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (atom('len), vector('v, dec, bit)) -> vector('len, dec, bit)
function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail_zero_extend(v, len)
overload operator ^ = {sail_mask}
val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
(bits('n), bits('m)) -> bits('n + 'm)
overload append = {bitvector_concat}
/* Used for creating long bitvector literals in the C backend. */
val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64)
val vector_access = {
ocaml: "access",
lem: "access_list_dec",
coq: "access_list_dec",
c: "vector_access"
} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a
val vector_update = {
ocaml: "update",
lem: "update_list_dec",
coq: "update_list_dec",
c: "vector_update"
} : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
val add_bits = {
ocaml: "add_vec",
lem: "add_vec",
c: "add_bits",
coq: "add_vec"
} : forall 'n. (bits('n), bits('n)) -> bits('n)
val add_bits_int = {
ocaml: "add_vec_int",
lem: "add_vec_int",
c: "add_bits_int",
coq: "add_vec_int"
} : forall 'n. (bits('n), int) -> bits('n)
overload operator + = {add_bits, add_bits_int}
val vector_subrange = {
ocaml: "subrange",
lem: "subrange_vec_dec",
c: "vector_subrange",
coq: "subrange_vec_dec"
} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
(bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
val vector_update_subrange = {
ocaml: "update_subrange",
lem: "update_subrange_vec_dec",
c: "vector_update_subrange",
coq: "update_subrange_vec_dec"
} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
// Some ARM specific builtins
val get_slice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w)
val set_slice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) -> int
val set_slice_bits = "set_slice" : forall 'n 'm.
(atom('n), atom('m), bits('n), int, bits('m)) -> bits('n)
val slice = "slice" : forall 'n 'm 'o, 0 <= 'o < 'm & 'o + 'n <= 'm & 0 <= 'n.
(bits('m), atom('o), atom('n)) -> bits('n)
val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
val unsigned = {
ocaml: "uint",
lem: "uint",
interpreter: "uint",
c: "sail_unsigned",
coq: "unsigned"
} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
val signed = {
c: "sail_signed",
_: "sint"
} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
$endif
|
