Skip to content

Commit 4b452f8

Browse files
AlasdairAlasdair
committed
Refactor internal only flag
1 parent 91dc2b3 commit 4b452f8

38 files changed

+347
-59
lines changed

‎aarch64/mono/mono_rewrites.sail‎

Lines changed: 0 additions & 1 deletion
This file was deleted.

‎aarch64/mono/mono_rewrites.sail‎

Lines changed: 296 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,296 @@
1+
/*==========================================================================*/
2+
/* Sail */
3+
/* */
4+
/* Sail and the Sail architecture models here, comprising all files and */
5+
/* directories except the ASL-derived Sail code in the aarch64 directory, */
6+
/* are subject to the BSD two-clause licence below. */
7+
/* */
8+
/* The ASL derived parts of the ARMv8.3 specification in */
9+
/* aarch64/no_vector and aarch64/full are copyright ARM Ltd. */
10+
/* */
11+
/* Copyright (c) 2013-2021 */
12+
/* Kathyrn Gray */
13+
/* Shaked Flur */
14+
/* Stephen Kell */
15+
/* Gabriel Kerneis */
16+
/* Robert Norton-Wright */
17+
/* Christopher Pulte */
18+
/* Peter Sewell */
19+
/* Alasdair Armstrong */
20+
/* Brian Campbell */
21+
/* Thomas Bauereiss */
22+
/* Anthony Fox */
23+
/* Jon French */
24+
/* Dominic Mulligan */
25+
/* Stephen Kell */
26+
/* Mark Wassell */
27+
/* Alastair Reid (Arm Ltd) */
28+
/* */
29+
/* All rights reserved. */
30+
/* */
31+
/* This work was partially supported by EPSRC grant EP/K008528/1 <a */
32+
/* href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous */
33+
/* Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA */
34+
/* KTF funding, and donations from Arm. This project has received */
35+
/* funding from the European Research Council (ERC) under the European */
36+
/* Union’s Horizon 2020 research and innovation programme (grant */
37+
/* agreement No 789108, ELVER). */
38+
/* */
39+
/* This software was developed by SRI International and the University of */
40+
/* Cambridge Computer Laboratory (Department of Computer Science and */
41+
/* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") */
42+
/* and FA8750-10-C-0237 ("CTSRD"). */
43+
/* */
44+
/* SPDX-License-Identifier: BSD-2-Clause */
45+
/*==========================================================================*/
46+
47+
$ifndef _MONO_REWRITES
48+
$define _MONO_REWRITES
49+
50+
/* Definitions for use with the -mono_rewrites option */
51+
52+
$include <arith.sail>
53+
$include <vector_dec.sail>
54+
55+
/* External definitions not in the usual asl prelude */
56+
57+
val extzv = pure {lem: "extz_vec"} : forall 'n 'm, 'm >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec)
58+
function extzv(m, v) = {
59+
if m < 'n then truncate(v, m) else sail_zero_extend(v, m)
60+
}
61+
62+
val extsv = pure {lem: "exts_vec"} : forall 'n 'm, 'm >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec)
63+
function extsv(m, v) = {
64+
if m < 'n then truncate(v, m) else sail_sign_extend(v, m)
65+
}
66+
67+
/* This is generated internally to deal with case splits which reveal the size
68+
of a bitvector */
69+
val bitvector_cast_in = pure "zeroExtend" : forall 'n. bits('n) -> bits('n)
70+
val bitvector_cast_out = pure "zeroExtend" : forall 'n. bits('n) -> bits('n)
71+
72+
/* Builtins for the rewrites */
73+
val string_of_bits_subrange = pure "string_of_bits_subrange" : forall 'n. (bits('n), int, int) -> string
74+
75+
/* Definitions for the rewrites */
76+
77+
val is_zero_subrange : forall 'n, 'n >= 0.
78+
(bits('n), int, int) -> bool
79+
80+
function is_zero_subrange (xs, i, j) = {
81+
(xs & slice_mask(j, i-j+1)) == extzv([bitzero] : bits(1))
82+
}
83+
84+
val is_zeros_slice : forall 'n, 'n >= 0.
85+
(bits('n), int, int) -> bool
86+
87+
function is_zeros_slice (xs, i, l) = {
88+
(xs & slice_mask(i, l)) == extzv([bitzero] : bits(1))
89+
}
90+
91+
val is_ones_subrange : forall 'n, 'n >= 0.
92+
(bits('n), int, int) -> bool
93+
94+
function is_ones_subrange (xs, i, j) = {
95+
let m : bits('n) = slice_mask(j,i-j+1) in
96+
(xs & m) == m
97+
}
98+
99+
val is_ones_slice : forall 'n, 'n >= 0.
100+
(bits('n), int, int) -> bool
101+
102+
function is_ones_slice (xs, i, j) = {
103+
let m : bits('n) = slice_mask(i,j) in
104+
(xs & m) == m
105+
}
106+
107+
val slice_slice_concat : forall 'n 'm 'r, 'n >= 0 & 'm >= 0 & 'r >= 0.
108+
(implicit('r), bits('n), int, int, bits('m), int, int) -> bits('r)
109+
110+
function slice_slice_concat (r, xs, i, l, ys, i', l') = {
111+
let xs = sail_shiftright(xs & slice_mask(i,l), i) in
112+
let ys = sail_shiftright(ys & slice_mask(i',l'), i') in
113+
sail_shiftleft(extzv(r, xs), l') | extzv(r, ys)
114+
}
115+
116+
val slice_zeros_concat : forall 'n 'p 'q, 'n >= 0 & 'p + 'q >= 0.
117+
(bits('n), int, atom('p), atom('q)) -> bits('p + 'q)
118+
119+
function slice_zeros_concat (xs, i, l, l') = {
120+
let xs = sail_shiftright(xs & slice_mask(i,l), i) in
121+
sail_shiftleft(extzv(l + l', xs), l')
122+
}
123+
124+
val subrange_zeros_concat : forall 'n 'hi 'lo 'q, 'n >= 0 & 'hi - 'lo + 1 + 'q >= 0.
125+
(bits('n), atom('hi), atom('lo), atom('q)) -> bits('hi - 'lo + 1 + 'q)
126+
127+
function subrange_zeros_concat (xs, hi, lo, l') =
128+
slice_zeros_concat(xs, lo, hi - lo + 1, l')
129+
130+
/* Assumes initial vectors are of equal size */
131+
132+
val subrange_subrange_eq : forall 'n, 'n >= 0.
133+
(bits('n), int, int, bits('n), int, int) -> bool
134+
135+
function subrange_subrange_eq (xs, i, j, ys, i', j') = {
136+
let xs = sail_shiftright(xs & slice_mask(j,i-j+1), j) in
137+
let ys = sail_shiftright(ys & slice_mask(j',i'-j'+1), j') in
138+
xs == ys
139+
}
140+
141+
val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's >= 0 & 'n >= 0 & 'm >= 0.
142+
(implicit('s), bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s)
143+
144+
function subrange_subrange_concat (s, xs, i, j, ys, i', j') = {
145+
let xs = sail_shiftright(xs & slice_mask(j,i-j+1), j) in
146+
let ys = sail_shiftright(ys & slice_mask(j',i'-j'+1), j') in
147+
sail_shiftleft(extzv(s, xs), i' - j' + 1) | extzv(s, ys)
148+
}
149+
150+
val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
151+
(implicit('m), bits('n), int, int, int) -> bits('m)
152+
153+
function place_subrange(m,xs,i,j,shift) = {
154+
let xs = sail_shiftright(xs & slice_mask(j,i-j+1), j) in
155+
sail_shiftleft(extzv(m, xs), shift)
156+
}
157+
158+
val place_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
159+
(implicit('m), bits('n), int, int, int) -> bits('m)
160+
161+
function place_slice(m,xs,i,l,shift) = {
162+
let xs = sail_shiftright(xs & slice_mask(i,l), i) in
163+
sail_shiftleft(extzv(m, xs), shift)
164+
}
165+
166+
val set_slice_zeros : forall 'n, 'n >= 0.
167+
(implicit('n), bits('n), int, int) -> bits('n)
168+
169+
function set_slice_zeros(n, xs, i, l) = {
170+
let ys : bits('n) = slice_mask(n, i, l) in
171+
xs & not_vec(ys)
172+
}
173+
174+
val set_subrange_zeros : forall 'n, 'n >= 0.
175+
(implicit('n), bits('n), int, int) -> bits('n)
176+
177+
function set_subrange_zeros(n, xs, hi, lo) =
178+
set_slice_zeros(n, xs, lo, hi - lo + 1)
179+
180+
val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
181+
(implicit('m), bits('n), int, int) -> bits('m)
182+
183+
function zext_slice(m,xs,i,l) = {
184+
let xs = sail_shiftright(xs & slice_mask(i,l), i) in
185+
extzv(m, xs)
186+
}
187+
188+
val zext_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
189+
(implicit('m), bits('n), int, int) -> bits('m)
190+
191+
function zext_subrange(m, xs, i, j) = zext_slice(m, xs, j, i - j + 1)
192+
193+
val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
194+
(implicit('m), bits('n), int, int) -> bits('m)
195+
196+
function sext_slice(m,xs,i,l) = {
197+
let xs = sail_arith_shiftright(sail_shiftleft((xs & slice_mask(i,l)), ('n - i - l)), 'n - l) in
198+
extsv(m, xs)
199+
}
200+
201+
val sext_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
202+
(implicit('m), bits('n), int, int) -> bits('m)
203+
204+
function sext_subrange(m, xs, i, j) = sext_slice(m, xs, j, i - j + 1)
205+
206+
val place_slice_signed : forall 'n 'm, 'n >= 0 & 'm >= 0.
207+
(implicit('m), bits('n), int, int, int) -> bits('m)
208+
209+
function place_slice_signed(m,xs,i,l,shift) = {
210+
sail_shiftleft(sext_slice(m, xs, i, l), shift)
211+
}
212+
213+
val place_subrange_signed : forall 'n 'm, 'n >= 0 & 'm >= 0.
214+
(implicit('m), bits('n), int, int, int) -> bits('m)
215+
216+
function place_subrange_signed(m,xs,i,j,shift) = {
217+
place_slice_signed(m, xs, j, i-j+1, shift)
218+
}
219+
220+
/* This has different names in the aarch64 prelude (UInt) and the other
221+
preludes (unsigned). To avoid variable name clashes, we redeclare it
222+
here with a suitably awkward name. */
223+
val _builtin_unsigned = pure {
224+
ocaml: "uint",
225+
lem: "uint",
226+
interpreter: "uint",
227+
c: "sail_unsigned",
228+
cpp: "sail_unsigned",
229+
coq: "uint",
230+
lean: "BitVec.toNat"
231+
} : forall 'n. bits('n) -> {'m, 0 <= 'm < 2 ^ 'n. int('m)}
232+
233+
/* There are different implementation choices for division and remainder, but
234+
they agree on positive values. We use this here to give more precise return
235+
types for unsigned_slice and unsigned_subrange. */
236+
237+
val _builtin_mod_nat = pure {
238+
smt: "mod",
239+
ocaml: "modulus",
240+
lem: "integerMod",
241+
c: "tmod_int",
242+
cpp: "tmod_int",
243+
coq: "Z.rem",
244+
lean: "Nat.mod"
245+
} : forall 'n 'm, 'n >= 0 & 'm >= 0. (int('n), int('m)) -> {'r, 0 <= 'r < 'm. int('r)}
246+
247+
/* Below we need the fact that 2 ^ 'n >= 0, so we axiomatise it in the return
248+
type of pow2, as SMT solvers tend to have problems with exponentiation. */
249+
val _builtin_pow2 = pure "pow2" : forall 'n, 'n >= 0. int('n) -> {'m, 'm == 2 ^ 'n & 'm >= 0. int('m)}
250+
251+
val unsigned_slice : forall 'n 'l, 'n >= 0 & 'l >= 0.
252+
(bits('n), int, int('l)) -> {'m, 0 <= 'm < 2 ^ 'l. int('m)}
253+
254+
function unsigned_slice(xs,i,l) = {
255+
let xs = sail_shiftright(xs & slice_mask(i,l), i) in
256+
_builtin_mod_nat(_builtin_unsigned(xs), _builtin_pow2(l))
257+
}
258+
259+
val unsigned_subrange : forall 'n 'i 'j, 'n >= 0 & ('i - 'j) >= 0.
260+
(bits('n), int('i), int('j)) -> {'m, 0 <= 'm < 2 ^ ('i - 'j + 1). int('m)}
261+
262+
function unsigned_subrange(xs,i,j) = {
263+
let xs = sail_shiftright(xs & slice_mask(j,i-j+1), i) in
264+
_builtin_mod_nat(_builtin_unsigned(xs), _builtin_pow2(i - j + 1))
265+
}
266+
267+
268+
val zext_ones : forall 'n, 'n >= 0. (implicit('n), int) -> bits('n)
269+
270+
function zext_ones(n, m) = {
271+
let v : bits('n) = extsv([bitone] : bits(1)) in
272+
sail_shiftright(v, n - m)
273+
}
274+
275+
276+
val vector_update_subrange_from_subrange : forall 'n1 's1 'e1 'n2 's2 'e2,
277+
0 <= 'e1 <= 's1 < 'n1 & 0 <= 'e2 <= 's2 < 'n2 & 's1 - 'e1 == 's2 - 'e2.
278+
(implicit('n1), bits('n1), int('s1), int('e1), bits('n2), int('s2), int('e2)) -> bits('n1)
279+
280+
function vector_update_subrange_from_subrange(n,v1,s1,e1,v2,s2,e2) = {
281+
let xs = sail_shiftright(v2 & slice_mask(e2,s2-e2+1), e2) in
282+
let xs = sail_shiftleft(extzv(n, xs), e1) in
283+
let ys = v1 & not_vec(slice_mask(e1,s1-e1+1)) in
284+
xs | ys
285+
}
286+
287+
val vector_update_subrange_from_integer_subrange : forall 'n1 's1 'e1 's2 'e2,
288+
0 <= 'e1 <= 's1 < 'n1 & 0 <= 'e2 <= 's2 & 's1 - 'e1 == 's2 - 'e2.
289+
(implicit('n1), bits('n1), int('s1), int('e1), int, int('s2), int('e2)) -> bits('n1)
290+
291+
function vector_update_subrange_from_integer_subrange(n1, v1, s1, e1, i, s2, e2) = {
292+
let v2 : bits('n1) = get_slice_int(n1, i, e2) in
293+
vector_update_subrange_from_subrange(n1, v1, s1, e1, v2, s2 - e2, 0)
294+
}
295+
296+
$endif

‎doc/asciidoc/usage.adoc‎

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -277,13 +277,6 @@ plugins. These options are all prefixed with `d`.
277277
re-writing pass. The output from each pass is placed in a file
278278
starting with `prefix`.
279279

280-
* `--dmagic-hash` Allow the `#` symbol in identifiers. It's
281-
currently used as a magic symbol to separate generated identifiers
282-
from those the user can write, so this option allows for the output
283-
of the various other debugging options to be fed back into Sail. The
284-
name comes from the GHC option with the same purpose:
285-
https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/magic_hash.html
286-
287280
=== Passing options via SAIL_FLAGS
288281

289282
The `SAIL_FLAGS` environment variable can be used to pass additional

‎doc/old/usage.tex‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -344,7 +344,7 @@ \subsection{Other options}
344344
345345
\item \verb+-dsanity+ Perform extra sanity checks on the AST.
346346
347-
\item \verb+-dmagic_hash+ Allow the \# symbol in identifiers. It's
347+
\item \verb+--dallow-internal+ Allow the \# symbol in identifiers. It's
348348
currently used as a magic symbol to separate generated identifiers
349349
from those the user can write, so this option allows for the output
350350
of the various other debugging options to be fed back into Sail.

‎src/bin/sail.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -398,7 +398,7 @@ let rec options =
398398
Arg.String (fun str -> Callgraph.opt_debug_callgraph := Some str),
399399
"<file> (debug) dump callgraph to file"
400400
);
401-
("-dmagic_hash", Arg.Set Initial_check.opt_magic_hash, " (debug) allow special character # in identifiers");
401+
("-dallow_internal", Arg.Set Initial_check.opt_allow_internal, " (debug) allow special character # in identifiers");
402402
("-dno_error_filenames", Arg.Set Error_format.opt_debug_no_filenames, " (debug) do not print filenames in errors");
403403
( "-dprofile",
404404
Arg.Set Profile.opt_profile,

0 commit comments

Comments
 (0)