Skip to content

Commit 23f1820

Browse files
Timmmmbillmcspadden-riscv
Timmmm
authored and
billmcspadden-riscv
committed
Simplify prelude.sail by including generic_equality.sail and mapping.sail
This change includes `generic_equality.sail` and `mapping.sail` from the Sail standard library which defines a lot of things that were defined in `prelude.sail`. I also removed `reg_deref` which is no longer required. The `mapping.sail` and `hex_bits.sail` files are in Sail 0.18 which is not yet released, so they have been temporarily copied here.
1 parent e7c369d commit 23f1820

File tree

7 files changed

+268
-863
lines changed

7 files changed

+268
-863
lines changed

‎Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@ SAIL_VM_SRCS += $(SAIL_RV64_VM_SRCS)
8282
endif
8383

8484
# Non-instruction sources
85-
PRELUDE = prelude.sail prelude_mapping.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail
85+
PRELUDE = prelude.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail
8686

8787
SAIL_REGS_SRCS = riscv_reg_type.sail riscv_freg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail
8888
SAIL_REGS_SRCS += riscv_pmp_regs.sail riscv_pmp_control.sail

‎model/hex_bits.sail‎

Lines changed: 124 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
1+
// Note: This file is temporarily copied here from the Sail compiler. It can
2+
// be removed when Sail 0.18 is released.
3+
4+
/*==========================================================================*/
5+
/* Sail */
6+
/* */
7+
/* Sail and the Sail architecture models here, comprising all files and */
8+
/* directories except the ASL-derived Sail code in the aarch64 directory, */
9+
/* are subject to the BSD two-clause licence below. */
10+
/* */
11+
/* The ASL derived parts of the ARMv8.3 specification in */
12+
/* aarch64/no_vector and aarch64/full are copyright ARM Ltd. */
13+
/* */
14+
/* Copyright (c) 2013-2021 */
15+
/* Kathyrn Gray */
16+
/* Shaked Flur */
17+
/* Stephen Kell */
18+
/* Gabriel Kerneis */
19+
/* Robert Norton-Wright */
20+
/* Christopher Pulte */
21+
/* Peter Sewell */
22+
/* Alasdair Armstrong */
23+
/* Brian Campbell */
24+
/* Thomas Bauereiss */
25+
/* Anthony Fox */
26+
/* Jon French */
27+
/* Dominic Mulligan */
28+
/* Stephen Kell */
29+
/* Mark Wassell */
30+
/* Alastair Reid (Arm Ltd) */
31+
/* */
32+
/* All rights reserved. */
33+
/* */
34+
/* This work was partially supported by EPSRC grant EP/K008528/1 <a */
35+
/* href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous */
36+
/* Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA */
37+
/* KTF funding, and donations from Arm. This project has received */
38+
/* funding from the European Research Council (ERC) under the European */
39+
/* Union’s Horizon 2020 research and innovation programme (grant */
40+
/* agreement No 789108, ELVER). */
41+
/* */
42+
/* This software was developed by SRI International and the University of */
43+
/* Cambridge Computer Laboratory (Department of Computer Science and */
44+
/* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") */
45+
/* and FA8750-10-C-0237 ("CTSRD"). */
46+
/* */
47+
/* Redistribution and use in source and binary forms, with or without */
48+
/* modification, are permitted provided that the following conditions */
49+
/* are met: */
50+
/* 1. Redistributions of source code must retain the above copyright */
51+
/* notice, this list of conditions and the following disclaimer. */
52+
/* 2. Redistributions in binary form must reproduce the above copyright */
53+
/* notice, this list of conditions and the following disclaimer in */
54+
/* the documentation and/or other materials provided with the */
55+
/* distribution. */
56+
/* */
57+
/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */
58+
/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */
59+
/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */
60+
/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */
61+
/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */
62+
/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */
63+
/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */
64+
/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */
65+
/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */
66+
/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */
67+
/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */
68+
/* SUCH DAMAGE. */
69+
/*==========================================================================*/
70+
71+
$ifndef _HEX_BITS
72+
$define _HEX_BITS
73+
74+
$include <vector.sail>
75+
$include <string.sail>
76+
77+
val "parse_hex_bits" : forall 'n, 'n > 0. (int('n), string) -> bits('n)
78+
val "valid_hex_bits" : forall 'n, 'n > 0. (int('n), string) -> bool
79+
80+
val hex_bits : forall 'n, 'n > 0. bits('n) <-> (int('n), string)
81+
82+
function hex_bits_forwards(bv) = (length(bv), hex_str(unsigned(bv)))
83+
function hex_bits_forwards_matches(bv) = true
84+
85+
function hex_bits_backwards(n, str) = parse_hex_bits(n, str)
86+
function hex_bits_backwards_matches(n, str) = valid_hex_bits(n, str)
87+
88+
mapping hex_bits_1 : bits(1) <-> string = { hex_bits(1, s) <-> s }
89+
mapping hex_bits_2 : bits(2) <-> string = { hex_bits(2, s) <-> s }
90+
mapping hex_bits_3 : bits(3) <-> string = { hex_bits(3, s) <-> s }
91+
mapping hex_bits_4 : bits(4) <-> string = { hex_bits(4, s) <-> s }
92+
mapping hex_bits_5 : bits(5) <-> string = { hex_bits(5, s) <-> s }
93+
mapping hex_bits_6 : bits(6) <-> string = { hex_bits(6, s) <-> s }
94+
mapping hex_bits_7 : bits(7) <-> string = { hex_bits(7, s) <-> s }
95+
mapping hex_bits_8 : bits(8) <-> string = { hex_bits(8, s) <-> s }
96+
mapping hex_bits_9 : bits(9) <-> string = { hex_bits(9, s) <-> s }
97+
98+
mapping hex_bits_10 : bits(10) <-> string = { hex_bits(10, s) <-> s }
99+
mapping hex_bits_11 : bits(11) <-> string = { hex_bits(11, s) <-> s }
100+
mapping hex_bits_12 : bits(12) <-> string = { hex_bits(12, s) <-> s }
101+
mapping hex_bits_13 : bits(13) <-> string = { hex_bits(13, s) <-> s }
102+
mapping hex_bits_14 : bits(14) <-> string = { hex_bits(14, s) <-> s }
103+
mapping hex_bits_15 : bits(15) <-> string = { hex_bits(15, s) <-> s }
104+
mapping hex_bits_16 : bits(16) <-> string = { hex_bits(16, s) <-> s }
105+
mapping hex_bits_17 : bits(17) <-> string = { hex_bits(17, s) <-> s }
106+
mapping hex_bits_18 : bits(18) <-> string = { hex_bits(18, s) <-> s }
107+
mapping hex_bits_19 : bits(19) <-> string = { hex_bits(19, s) <-> s }
108+
109+
mapping hex_bits_20 : bits(20) <-> string = { hex_bits(20, s) <-> s }
110+
mapping hex_bits_21 : bits(21) <-> string = { hex_bits(21, s) <-> s }
111+
mapping hex_bits_22 : bits(22) <-> string = { hex_bits(22, s) <-> s }
112+
mapping hex_bits_23 : bits(23) <-> string = { hex_bits(23, s) <-> s }
113+
mapping hex_bits_24 : bits(24) <-> string = { hex_bits(24, s) <-> s }
114+
mapping hex_bits_25 : bits(25) <-> string = { hex_bits(25, s) <-> s }
115+
mapping hex_bits_26 : bits(26) <-> string = { hex_bits(26, s) <-> s }
116+
mapping hex_bits_27 : bits(27) <-> string = { hex_bits(27, s) <-> s }
117+
mapping hex_bits_28 : bits(28) <-> string = { hex_bits(28, s) <-> s }
118+
mapping hex_bits_29 : bits(29) <-> string = { hex_bits(29, s) <-> s }
119+
120+
mapping hex_bits_30 : bits(30) <-> string = { hex_bits(30, s) <-> s }
121+
mapping hex_bits_31 : bits(31) <-> string = { hex_bits(31, s) <-> s }
122+
mapping hex_bits_32 : bits(32) <-> string = { hex_bits(32, s) <-> s }
123+
124+
$endif _HEX_BITS

‎model/mapping.sail‎

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
// Note: This file is temporarily copied here from the Sail compiler. It can
2+
// be removed when Sail 0.18 is released.
3+
4+
/*==========================================================================*/
5+
/* Sail */
6+
/* */
7+
/* Sail and the Sail architecture models here, comprising all files and */
8+
/* directories except the ASL-derived Sail code in the aarch64 directory, */
9+
/* are subject to the BSD two-clause licence below. */
10+
/* */
11+
/* The ASL derived parts of the ARMv8.3 specification in */
12+
/* aarch64/no_vector and aarch64/full are copyright ARM Ltd. */
13+
/* */
14+
/* Copyright (c) 2013-2021 */
15+
/* Kathyrn Gray */
16+
/* Shaked Flur */
17+
/* Stephen Kell */
18+
/* Gabriel Kerneis */
19+
/* Robert Norton-Wright */
20+
/* Christopher Pulte */
21+
/* Peter Sewell */
22+
/* Alasdair Armstrong */
23+
/* Brian Campbell */
24+
/* Thomas Bauereiss */
25+
/* Anthony Fox */
26+
/* Jon French */
27+
/* Dominic Mulligan */
28+
/* Stephen Kell */
29+
/* Mark Wassell */
30+
/* Alastair Reid (Arm Ltd) */
31+
/* */
32+
/* All rights reserved. */
33+
/* */
34+
/* This work was partially supported by EPSRC grant EP/K008528/1 <a */
35+
/* href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous */
36+
/* Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA */
37+
/* KTF funding, and donations from Arm. This project has received */
38+
/* funding from the European Research Council (ERC) under the European */
39+
/* Union’s Horizon 2020 research and innovation programme (grant */
40+
/* agreement No 789108, ELVER). */
41+
/* */
42+
/* This software was developed by SRI International and the University of */
43+
/* Cambridge Computer Laboratory (Department of Computer Science and */
44+
/* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") */
45+
/* and FA8750-10-C-0237 ("CTSRD"). */
46+
/* */
47+
/* Redistribution and use in source and binary forms, with or without */
48+
/* modification, are permitted provided that the following conditions */
49+
/* are met: */
50+
/* 1. Redistributions of source code must retain the above copyright */
51+
/* notice, this list of conditions and the following disclaimer. */
52+
/* 2. Redistributions in binary form must reproduce the above copyright */
53+
/* notice, this list of conditions and the following disclaimer in */
54+
/* the documentation and/or other materials provided with the */
55+
/* distribution. */
56+
/* */
57+
/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */
58+
/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */
59+
/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */
60+
/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */
61+
/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */
62+
/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */
63+
/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */
64+
/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */
65+
/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */
66+
/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */
67+
/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */
68+
/* SUCH DAMAGE. */
69+
/*==========================================================================*/
70+
71+
$ifndef _MAPPING
72+
$define _MAPPING
73+
74+
$include <arith.sail>
75+
$include <option.sail>
76+
77+
val string_take = pure "string_take" : (string, nat) -> string
78+
val string_drop = pure "string_drop" : (string, nat) -> string
79+
val string_length = pure "string_length" : string -> nat
80+
val string_append = pure {coq: "String.append", c: "concat_str", _: "string_append"} : (string, string) -> string
81+
val string_startswith = pure "string_startswith" : (string, string) -> bool
82+
83+
val n_leading_spaces = pure { coq: "n_leading_spaces_Z" } : string -> nat
84+
function n_leading_spaces s =
85+
match s {
86+
"" => 0,
87+
_ => match string_take(s, 1) {
88+
" " => 1 + n_leading_spaces(string_drop(s, 1)),
89+
_ => 0
90+
}
91+
}
92+
93+
/*!
94+
In a string mapping this is treated as `[ ]+`, i.e one or more space
95+
characters. It is printed as a single space `" "`.
96+
*/
97+
val spc : unit <-> string
98+
99+
function spc_forwards() = " "
100+
function spc_forwards_matches() = true
101+
102+
function spc_backwards _ = ()
103+
function spc_backwards_matches s = {
104+
let len = string_length(s);
105+
n_leading_spaces(s) == len & len > 0
106+
}
107+
108+
/*!
109+
In a string mapping this is treated as `[ ]*`, i.e. zero or more space
110+
characters. It is printed as the empty string.
111+
*/
112+
val opt_spc : unit <-> string
113+
114+
function opt_spc_forwards() = ""
115+
function opt_spc_forwards_matches() = true
116+
117+
function opt_spc_backwards _ = ()
118+
function opt_spc_backwards_matches s = n_leading_spaces(s) == string_length(s)
119+
120+
/*!
121+
Like `opt_spc`, in a string mapping this is treated as `[ ]*`, i.e. zero or more space
122+
characters. It differs however in that it is printed as a single space `" "`.
123+
*/
124+
val def_spc : unit <-> string
125+
126+
function def_spc_forwards() = " "
127+
function def_spc_forwards_matches() = true
128+
129+
function def_spc_backwards _ = ()
130+
function def_spc_backwards_matches s = n_leading_spaces(s) == string_length(s)
131+
132+
mapping sep : unit <-> string = {
133+
() <-> opt_spc() ^ "," ^ def_spc()
134+
}
135+
136+
$endif

‎model/prelude.sail‎

Lines changed: 6 additions & 85 deletions
Original file line numberDiff line numberDiff line change
@@ -74,53 +74,21 @@ $include <smt.sail>
7474
$include <option.sail>
7575
$include <arith.sail>
7676
$include <string.sail>
77+
$include "mapping.sail"
7778
$include <vector_dec.sail>
7879
$include <regfp.sail>
80+
$include <generic_equality.sail>
81+
$include "hex_bits.sail"
7982

80-
val string_startswith = "string_startswith" : (string, string) -> bool
81-
val string_drop = "string_drop" : (string, nat) -> string
82-
val string_take = "string_take" : (string, nat) -> string
83-
val string_length = "string_length" : string -> nat
84-
val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string
85-
86-
val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq", c: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
87-
88-
overload operator == = {eq_string, eq_anything}
89-
90-
val "reg_deref" : forall ('a : Type). register('a) -> 'a
91-
/* sneaky deref with no effect necessary for bitfield writes */
92-
val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
93-
94-
val any_vector_update = {ocaml: "update", lem: "update_list_dec", coq: "vector_update"} : forall 'n ('a : Type).
95-
(vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
96-
97-
overload vector_update = {any_vector_update}
98-
99-
val update_subrange = {ocaml: "update_subrange", interpreter: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
100-
(bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
101-
102-
val vector_concat = {ocaml: "append", lem: "append_list", coq: "vec_concat"} : forall ('n : Int) ('m : Int) ('a : Type).
103-
(vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
104-
105-
overload append = {vector_concat}
10683

10784
val not_bit : bit -> bit
108-
10985
function not_bit(b) = if b == bitone then bitzero else bitone
11086

11187
overload ~ = {not_bool, not_vec, not_bit}
11288

113-
val not = pure {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> bool(not('p))
114-
115-
val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
116-
117-
function neq_vec (x, y) = not_bool(eq_bits(x, y))
118-
119-
val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool
120-
121-
function neq_anything (x, y) = not_bool(x == y)
122-
123-
overload operator != = {neq_vec, neq_anything}
89+
// not_bool alias.
90+
val not : forall ('p : Bool). bool('p) -> bool(not('p))
91+
function not(b) = not_bool(b)
12492

12593
overload operator & = {and_vec}
12694

@@ -284,53 +252,6 @@ function reverse_bits_in_byte (xs : bits(8)) -> bits(8) = {
284252

285253
overload reverse = {reverse_bits_in_byte}
286254

287-
/* helpers for mappings */
288-
289-
val spc : unit <-> string
290-
val opt_spc : unit <-> string
291-
val def_spc : unit <-> string
292-
293-
val "decimal_string_of_bits" : forall 'n. bits('n) -> string
294-
val hex_bits : forall 'n . (atom('n), bits('n)) <-> string
295-
296-
val n_leading_spaces : string -> nat
297-
function n_leading_spaces s =
298-
match s {
299-
"" => 0,
300-
_ => match string_take(s, 1) {
301-
" " => 1 + n_leading_spaces(string_drop(s, 1)),
302-
_ => 0
303-
}
304-
}
305-
306-
val spc_forwards : unit -> string
307-
function spc_forwards () = " "
308-
val spc_backwards : string -> unit
309-
function spc_backwards s = ()
310-
val spc_matches_prefix : string -> option((unit, nat))
311-
function spc_matches_prefix s = {
312-
let n = n_leading_spaces(s);
313-
match n {
314-
0 => None(),
315-
_ => Some((), n)
316-
}
317-
}
318-
319-
val opt_spc_forwards : unit -> string
320-
function opt_spc_forwards () = ""
321-
val opt_spc_backwards : string -> unit
322-
function opt_spc_backwards s = ()
323-
val opt_spc_matches_prefix : string -> option((unit, nat))
324-
function opt_spc_matches_prefix s =
325-
Some((), n_leading_spaces(s))
326-
327-
val def_spc_forwards : unit -> string
328-
function def_spc_forwards () = " "
329-
val def_spc_backwards : string -> unit
330-
function def_spc_backwards s = ()
331-
val def_spc_matches_prefix : string -> option((unit, nat))
332-
function def_spc_matches_prefix s = opt_spc_matches_prefix(s)
333-
334255
overload operator / = {quot_round_zero}
335256
overload operator * = {mult_atom, mult_int}
336257

0 commit comments

Comments
 (0)