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
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
|
Changelog
=========
Sail 0.13
---------
##### Experimental new C backend
Supports creating C code that works as a library in a more natural
way. Rather than defining lots of global state, the model state will
be packaged into a `sail_state` struct that is passed into each
generated C function. The code generation is much more configurable,
including options for fine-grained control over name-mangling (see
etc/default_config.json).
Currently the -c2 option can be used. Eventually it is planned that
this will become the default C code generation option, and the old C
code generator will be removed.
##### Improved monomorphisation
The monomorphisation pass for Isabelle and HOL4 has been improved
significantly.
##### Code coverage
There is now a code coverage tool (sailcov) in the sailcov
subdirectory of this repository
Sail 0.8
--------
##### More flexible type synonym syntax
Can now define type synonyms for kinds other than `Type`. For example:
```
type xlen : Int = 64
type xlenbits = bits(xlen)
```
the syntax is
```
type <name> : <kind> = <value>
```
for synonyms with no arguments and
```
type <name>(<arguments>)[, <constraint>] -> <kind> = <value>
```
for synonyms that take arguments. Valid kinds are `Int`, `Bool`, `Ord`, and
`Type`. `: Type` or `-> Type` can be omitted.
This can be used to define constraint synonyms, e.g.
```
type is_register_index('n : Int) = 0 <= 'n <= 31
val my_function : forall 'n, is_register_index('n). int('n) -> ...
```
Type synonyms with constraints and multiple arguments can be declared as e.g.
```
type my_type('n: Int, 'm: Int), 'n > 'm > 0 = vector('n, dec, bits('m))
```
The previous syntax for numeric constants (which was never fully implemented) of
```
constant x = <value>
```
is no longer supported.
##### Emacs mode improvements
Can now use `C-c C-s` in Emacs to start a Sail interactive
sub-process, assuming `sail` is available in `$PATH`. Using `C-c C-l`
or simply saving a changed Sail file will cause it to be checked. Type
errors will be highlighted within the Emacs buffer, and can be jumped
to using `C-c C-x`, much like Merlin for OCaml. `C-c C-c` will display
the type of the expression under the cursor for a checked Sail
file. This particular is slightly experimental and won't always
display the most precise type, although Emacs will bold the region
that sail thinks is under the cursor to make this clear. The
interactive Sail session can be ended using `C-c C-q`.
To support multiple file ISA specifications, a JSON file called
sail.json can be placed in the same directory as the .sail files. It
specifies the dependency order for the .sail files and any options
required by Sail itself. As an example, the file for v8.5 is
```json
{
"options" : "-non_lexical_flow -no_lexp_bounds_check",
"files" : [
"prelude.sail",
"no_devices.sail",
"aarch_types.sail",
"aarch_mem.sail",
"aarch64.sail",
"aarch64_float.sail",
"aarch64_vector.sail",
"aarch32.sail",
"aarch_decode.sail"
]
}
```
For this to work Sail must be build with interactive support as `make
isail`. This requires the yojson library as a new dependency (`opam
install yojson`).
##### Boolean constraints and type-variables
We now support Boolean type arguments in much the same way as numeric
type arguments. Much like the type int('n), which means an integer
equal to the type variable 'n, bool('p) now means a Boolean that is
true provided the constraint 'p holds. This enables us to do flow
typing in a less ad-hoc way, as we can now have types like
```
val operator <= : forall 'n 'm. (int('n), int('n)) -> bool('n <= 'm)
```
The main use case for this feature in specifications is to support
flags that change the range of type variables, e.g:
```
val my_op : forall 'n ('f : Bool), 0 <= 'n < 15 & ('f | 'n < 4).
(bool('f), int('n)) -> unit
function my_op(flag, index) = {
if flag then {
// 0 <= 'n < 15 holds
let x = 0xF[index]; // will fail to typecheck here
...
} else {
// 0 <= 'n < 4 holds
let x = 0xF[index]; // will typecheck here
...
}
}
```
This change is mostly backwards compatible, except in some cases extra
type annotations may be required when declaring mutable Boolean
variables, so
```
x = true // declaration of x
x = false // type error because x inferred to have type bool(true)
```
should become
```
x : bool = true // declaration of x
x = false // fine because x can have any Boolean value
```
##### Simpler implicit arguments
Function implicit arguments are now given explicitly in their type signatures so
```
val zero_extend : forall 'n 'm, 'm >= 'n. bits('n) -> bits('m)
function zero_extend(v) = zeros('m - length(v)) @ v
```
would now become
```
val zero_extend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
function zero_extend(m, v) = zeros(m - length(v)) @ v
```
This radically simplifies how we resolve such implicit arguments
during type-checking, and speeds up processing large specifications
like ARM v8.5 significantly.
There is a symbol `FEATURE_IMPLICITS` which can be used with `$ifdef`
to write both new and old-versions if desired for backwards
compatibility, as the new version is syntactically valid in older Sails,
but just doesn't typecheck.
##### Parameterised bitfields
Bitfields can now be parameterised in the following way:
```
type xlenbits = bits(xlen)
bitfield Mstatus : xlenbits = {
SD : xlen - ylen,
SXL : xlen - ylen - 1 .. xlen - ylen - 3
}
```
This bitfield would then be valid for either
```
type xlen : Int = 64
type ylen : Int = 1
```
or
```
type xlen : Int = 32
type ylen : Int = 1
```
##### Lem monad embedding changes
The monad embedding for Lem has been changed to make it more friendly
for theorem proving. This can break model-specific Lem that depends on
the definitions in [src/gen_lib](src/gen_lib).
|
