diff --git a/model/hex_bits.sail b/model/hex_bits.sail deleted file mode 100644 index 81e25e155..000000000 --- a/model/hex_bits.sail +++ /dev/null @@ -1,124 +0,0 @@ -// Note: This file is temporarily copied here from the Sail compiler. It can -// be removed when Sail 0.18 is released. - -/*==========================================================================*/ -/* Sail */ -/* */ -/* Sail and the Sail architecture models here, comprising all files and */ -/* directories except the ASL-derived Sail code in the aarch64 directory, */ -/* are subject to the BSD two-clause licence below. */ -/* */ -/* The ASL derived parts of the ARMv8.3 specification in */ -/* aarch64/no_vector and aarch64/full are copyright ARM Ltd. */ -/* */ -/* Copyright (c) 2013-2021 */ -/* Kathyrn Gray */ -/* Shaked Flur */ -/* Stephen Kell */ -/* Gabriel Kerneis */ -/* Robert Norton-Wright */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alasdair Armstrong */ -/* Brian Campbell */ -/* Thomas Bauereiss */ -/* Anthony Fox */ -/* Jon French */ -/* Dominic Mulligan */ -/* Stephen Kell */ -/* Mark Wassell */ -/* Alastair Reid (Arm Ltd) */ -/* */ -/* All rights reserved. */ -/* */ -/* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous */ -/* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA */ -/* KTF funding, and donations from Arm. This project has received */ -/* funding from the European Research Council (ERC) under the European */ -/* Union’s Horizon 2020 research and innovation programme (grant */ -/* agreement No 789108, ELVER). */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") */ -/* and FA8750-10-C-0237 ("CTSRD"). */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ -/*==========================================================================*/ - -$ifndef _HEX_BITS -$define _HEX_BITS - -$include -$include - -val "parse_hex_bits" : forall 'n, 'n > 0. (int('n), string) -> bits('n) -val "valid_hex_bits" : forall 'n, 'n > 0. (int('n), string) -> bool - -val hex_bits : forall 'n, 'n > 0. bits('n) <-> (int('n), string) - -function hex_bits_forwards(bv) = (length(bv), hex_str(unsigned(bv))) -function hex_bits_forwards_matches(bv) = true - -function hex_bits_backwards(n, str) = parse_hex_bits(n, str) -function hex_bits_backwards_matches(n, str) = valid_hex_bits(n, str) - -mapping hex_bits_1 : bits(1) <-> string = { hex_bits(1, s) <-> s } -mapping hex_bits_2 : bits(2) <-> string = { hex_bits(2, s) <-> s } -mapping hex_bits_3 : bits(3) <-> string = { hex_bits(3, s) <-> s } -mapping hex_bits_4 : bits(4) <-> string = { hex_bits(4, s) <-> s } -mapping hex_bits_5 : bits(5) <-> string = { hex_bits(5, s) <-> s } -mapping hex_bits_6 : bits(6) <-> string = { hex_bits(6, s) <-> s } -mapping hex_bits_7 : bits(7) <-> string = { hex_bits(7, s) <-> s } -mapping hex_bits_8 : bits(8) <-> string = { hex_bits(8, s) <-> s } -mapping hex_bits_9 : bits(9) <-> string = { hex_bits(9, s) <-> s } - -mapping hex_bits_10 : bits(10) <-> string = { hex_bits(10, s) <-> s } -mapping hex_bits_11 : bits(11) <-> string = { hex_bits(11, s) <-> s } -mapping hex_bits_12 : bits(12) <-> string = { hex_bits(12, s) <-> s } -mapping hex_bits_13 : bits(13) <-> string = { hex_bits(13, s) <-> s } -mapping hex_bits_14 : bits(14) <-> string = { hex_bits(14, s) <-> s } -mapping hex_bits_15 : bits(15) <-> string = { hex_bits(15, s) <-> s } -mapping hex_bits_16 : bits(16) <-> string = { hex_bits(16, s) <-> s } -mapping hex_bits_17 : bits(17) <-> string = { hex_bits(17, s) <-> s } -mapping hex_bits_18 : bits(18) <-> string = { hex_bits(18, s) <-> s } -mapping hex_bits_19 : bits(19) <-> string = { hex_bits(19, s) <-> s } - -mapping hex_bits_20 : bits(20) <-> string = { hex_bits(20, s) <-> s } -mapping hex_bits_21 : bits(21) <-> string = { hex_bits(21, s) <-> s } -mapping hex_bits_22 : bits(22) <-> string = { hex_bits(22, s) <-> s } -mapping hex_bits_23 : bits(23) <-> string = { hex_bits(23, s) <-> s } -mapping hex_bits_24 : bits(24) <-> string = { hex_bits(24, s) <-> s } -mapping hex_bits_25 : bits(25) <-> string = { hex_bits(25, s) <-> s } -mapping hex_bits_26 : bits(26) <-> string = { hex_bits(26, s) <-> s } -mapping hex_bits_27 : bits(27) <-> string = { hex_bits(27, s) <-> s } -mapping hex_bits_28 : bits(28) <-> string = { hex_bits(28, s) <-> s } -mapping hex_bits_29 : bits(29) <-> string = { hex_bits(29, s) <-> s } - -mapping hex_bits_30 : bits(30) <-> string = { hex_bits(30, s) <-> s } -mapping hex_bits_31 : bits(31) <-> string = { hex_bits(31, s) <-> s } -mapping hex_bits_32 : bits(32) <-> string = { hex_bits(32, s) <-> s } - -$endif _HEX_BITS diff --git a/model/hex_bits_signed.sail b/model/hex_bits_signed.sail deleted file mode 100644 index 15bbea809..000000000 --- a/model/hex_bits_signed.sail +++ /dev/null @@ -1,141 +0,0 @@ -/*==========================================================================*/ -/* Sail */ -/* */ -/* Sail and the Sail architecture models here, comprising all files and */ -/* directories except the ASL-derived Sail code in the aarch64 directory, */ -/* are subject to the BSD two-clause licence below. */ -/* */ -/* The ASL derived parts of the ARMv8.3 specification in */ -/* aarch64/no_vector and aarch64/full are copyright ARM Ltd. */ -/* */ -/* Copyright (c) 2013-2021 */ -/* Kathyrn Gray */ -/* Shaked Flur */ -/* Stephen Kell */ -/* Gabriel Kerneis */ -/* Robert Norton-Wright */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alasdair Armstrong */ -/* Brian Campbell */ -/* Thomas Bauereiss */ -/* Anthony Fox */ -/* Jon French */ -/* Dominic Mulligan */ -/* Stephen Kell */ -/* Mark Wassell */ -/* Alastair Reid (Arm Ltd) */ -/* */ -/* All rights reserved. */ -/* */ -/* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous */ -/* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA */ -/* KTF funding, and donations from Arm. This project has received */ -/* funding from the European Research Council (ERC) under the European */ -/* Union’s Horizon 2020 research and innovation programme (grant */ -/* agreement No 789108, ELVER). */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") */ -/* and FA8750-10-C-0237 ("CTSRD"). */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ -/*==========================================================================*/ - -$ifndef _HEX_BITS_SIGNED -$define _HEX_BITS_SIGNED - -$include -$include - -val parse_hex_bits_signed : forall 'n, 'n > 0. (int('n), string) -> bits('n) -val valid_hex_bits_signed : forall 'n, 'n > 0. (int('n), string) -> bool - -val hex_bits_signed : forall 'n, 'n > 0. bits('n) <-> (int('n), string) - -function hex_bits_signed_forwards(bv) = { - if signed(bv) < 0 - then (length(bv), concat_str("-", hex_str(unsigned(not_vec(bv) + 1)))) - else (length(bv), hex_str(unsigned(bv))) -} -function hex_bits_signed_forwards_matches(bv) = true - -function parse_hex_bits_signed(n, str) = { - if string_take(str, 1) == "-" - then { - let str = string_drop(str, 1); - let bv = parse_hex_bits(n, str); - not_vec(bv) + 1 - } - else parse_hex_bits(n, str) -} - -function valid_hex_bits_signed(n, str) = { - if string_take(str, 1) == "-" - then valid_hex_bits(n, string_drop(str, 1)) - else valid_hex_bits(n, str) -} - -function hex_bits_signed_backwards(n, str) = parse_hex_bits_signed(n, str) -function hex_bits_signed_backwards_matches(n, str) = valid_hex_bits_signed(n, str) - -mapping hex_bits_signed_1 : bits(1) <-> string = { hex_bits_signed(1, s) <-> s } -mapping hex_bits_signed_2 : bits(2) <-> string = { hex_bits_signed(2, s) <-> s } -mapping hex_bits_signed_3 : bits(3) <-> string = { hex_bits_signed(3, s) <-> s } -mapping hex_bits_signed_4 : bits(4) <-> string = { hex_bits_signed(4, s) <-> s } -mapping hex_bits_signed_5 : bits(5) <-> string = { hex_bits_signed(5, s) <-> s } -mapping hex_bits_signed_6 : bits(6) <-> string = { hex_bits_signed(6, s) <-> s } -mapping hex_bits_signed_7 : bits(7) <-> string = { hex_bits_signed(7, s) <-> s } -mapping hex_bits_signed_8 : bits(8) <-> string = { hex_bits_signed(8, s) <-> s } -mapping hex_bits_signed_9 : bits(9) <-> string = { hex_bits_signed(9, s) <-> s } - -mapping hex_bits_signed_10 : bits(10) <-> string = { hex_bits_signed(10, s) <-> s } -mapping hex_bits_signed_11 : bits(11) <-> string = { hex_bits_signed(11, s) <-> s } -mapping hex_bits_signed_12 : bits(12) <-> string = { hex_bits_signed(12, s) <-> s } -mapping hex_bits_signed_13 : bits(13) <-> string = { hex_bits_signed(13, s) <-> s } -mapping hex_bits_signed_14 : bits(14) <-> string = { hex_bits_signed(14, s) <-> s } -mapping hex_bits_signed_15 : bits(15) <-> string = { hex_bits_signed(15, s) <-> s } -mapping hex_bits_signed_16 : bits(16) <-> string = { hex_bits_signed(16, s) <-> s } -mapping hex_bits_signed_17 : bits(17) <-> string = { hex_bits_signed(17, s) <-> s } -mapping hex_bits_signed_18 : bits(18) <-> string = { hex_bits_signed(18, s) <-> s } -mapping hex_bits_signed_19 : bits(19) <-> string = { hex_bits_signed(19, s) <-> s } - -mapping hex_bits_signed_20 : bits(20) <-> string = { hex_bits_signed(20, s) <-> s } -mapping hex_bits_signed_21 : bits(21) <-> string = { hex_bits_signed(21, s) <-> s } -mapping hex_bits_signed_22 : bits(22) <-> string = { hex_bits_signed(22, s) <-> s } -mapping hex_bits_signed_23 : bits(23) <-> string = { hex_bits_signed(23, s) <-> s } -mapping hex_bits_signed_24 : bits(24) <-> string = { hex_bits_signed(24, s) <-> s } -mapping hex_bits_signed_25 : bits(25) <-> string = { hex_bits_signed(25, s) <-> s } -mapping hex_bits_signed_26 : bits(26) <-> string = { hex_bits_signed(26, s) <-> s } -mapping hex_bits_signed_27 : bits(27) <-> string = { hex_bits_signed(27, s) <-> s } -mapping hex_bits_signed_28 : bits(28) <-> string = { hex_bits_signed(28, s) <-> s } -mapping hex_bits_signed_29 : bits(29) <-> string = { hex_bits_signed(29, s) <-> s } - -mapping hex_bits_signed_30 : bits(30) <-> string = { hex_bits_signed(30, s) <-> s } -mapping hex_bits_signed_31 : bits(31) <-> string = { hex_bits_signed(31, s) <-> s } -mapping hex_bits_signed_32 : bits(32) <-> string = { hex_bits_signed(32, s) <-> s } - -$endif _HEX_BITS_SIGNED diff --git a/model/mapping.sail b/model/mapping.sail deleted file mode 100644 index ec8b75979..000000000 --- a/model/mapping.sail +++ /dev/null @@ -1,136 +0,0 @@ -// Note: This file is temporarily copied here from the Sail compiler. It can -// be removed when Sail 0.18 is released. - -/*==========================================================================*/ -/* Sail */ -/* */ -/* Sail and the Sail architecture models here, comprising all files and */ -/* directories except the ASL-derived Sail code in the aarch64 directory, */ -/* are subject to the BSD two-clause licence below. */ -/* */ -/* The ASL derived parts of the ARMv8.3 specification in */ -/* aarch64/no_vector and aarch64/full are copyright ARM Ltd. */ -/* */ -/* Copyright (c) 2013-2021 */ -/* Kathyrn Gray */ -/* Shaked Flur */ -/* Stephen Kell */ -/* Gabriel Kerneis */ -/* Robert Norton-Wright */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alasdair Armstrong */ -/* Brian Campbell */ -/* Thomas Bauereiss */ -/* Anthony Fox */ -/* Jon French */ -/* Dominic Mulligan */ -/* Stephen Kell */ -/* Mark Wassell */ -/* Alastair Reid (Arm Ltd) */ -/* */ -/* All rights reserved. */ -/* */ -/* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous */ -/* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA */ -/* KTF funding, and donations from Arm. This project has received */ -/* funding from the European Research Council (ERC) under the European */ -/* Union’s Horizon 2020 research and innovation programme (grant */ -/* agreement No 789108, ELVER). */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") */ -/* and FA8750-10-C-0237 ("CTSRD"). */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ -/*==========================================================================*/ - -$ifndef _MAPPING -$define _MAPPING - -$include -$include - -val string_take = pure "string_take" : (string, nat) -> string -val string_drop = pure "string_drop" : (string, nat) -> string -val string_length = pure "string_length" : string -> nat -val string_append = pure {coq: "String.append", c: "concat_str", _: "string_append"} : (string, string) -> string -val string_startswith = pure "string_startswith" : (string, string) -> bool - -val n_leading_spaces = pure { coq: "n_leading_spaces_Z" } : string -> nat -function n_leading_spaces s = - match s { - "" => 0, - _ => match string_take(s, 1) { - " " => 1 + n_leading_spaces(string_drop(s, 1)), - _ => 0 - } - } - -/*! -In a string mapping this is treated as `[ ]+`, i.e one or more space -characters. It is printed as a single space `" "`. -*/ -val spc : unit <-> string - -function spc_forwards() = " " -function spc_forwards_matches() = true - -function spc_backwards _ = () -function spc_backwards_matches s = { - let len = string_length(s); - n_leading_spaces(s) == len & len > 0 -} - -/*! -In a string mapping this is treated as `[ ]*`, i.e. zero or more space -characters. It is printed as the empty string. -*/ -val opt_spc : unit <-> string - -function opt_spc_forwards() = "" -function opt_spc_forwards_matches() = true - -function opt_spc_backwards _ = () -function opt_spc_backwards_matches s = n_leading_spaces(s) == string_length(s) - -/*! -Like `opt_spc`, in a string mapping this is treated as `[ ]*`, i.e. zero or more space -characters. It differs however in that it is printed as a single space `" "`. -*/ -val def_spc : unit <-> string - -function def_spc_forwards() = " " -function def_spc_forwards_matches() = true - -function def_spc_backwards _ = () -function def_spc_backwards_matches s = n_leading_spaces(s) == string_length(s) - -mapping sep : unit <-> string = { - () <-> opt_spc() ^ "," ^ def_spc() -} - -$endif diff --git a/model/prelude.sail b/model/prelude.sail index 67855c5e9..8c03c58da 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -12,11 +12,11 @@ $include $include $include $include -$include "mapping.sail" +$include $include $include -$include "hex_bits.sail" -$include "hex_bits_signed.sail" +$include +$include val not_bit : bit -> bit function not_bit(b) = if b == bitone then bitzero else bitone