From f228c2b4acfc030737fff8e169f008e6db42bb1b Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 6 Dec 2023 22:40:29 +0000 Subject: [PATCH] Add hex_bits library file --- lib/hex_bits.sail | 121 +++++++++++++++++++++++++++++++++++++ test/c/lib_hex_bits.expect | 6 ++ test/c/lib_hex_bits.sail | 31 ++++++++++ 3 files changed, 158 insertions(+) create mode 100644 lib/hex_bits.sail create mode 100644 test/c/lib_hex_bits.expect create mode 100644 test/c/lib_hex_bits.sail diff --git a/lib/hex_bits.sail b/lib/hex_bits.sail new file mode 100644 index 000000000..ea74b7f2c --- /dev/null +++ b/lib/hex_bits.sail @@ -0,0 +1,121 @@ +/*==========================================================================*/ +/* 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/test/c/lib_hex_bits.expect b/test/c/lib_hex_bits.expect new file mode 100644 index 000000000..94db9bc5f --- /dev/null +++ b/test/c/lib_hex_bits.expect @@ -0,0 +1,6 @@ +ok +ok +ok +ok +ok +ok 0xffffffff diff --git a/test/c/lib_hex_bits.sail b/test/c/lib_hex_bits.sail new file mode 100644 index 000000000..a201c145d --- /dev/null +++ b/test/c/lib_hex_bits.sail @@ -0,0 +1,31 @@ +default Order dec + +$include +$include + +function main() -> unit = { + match hex_bits_1("0x1") { + 0b1 => print_endline("ok"), + _ => print_endline("fail"), + }; + match hex_bits_1(0b1) { + "0x1" => print_endline("ok"), + _ => print_endline("fail"), + }; + match hex_bits_32("0xFFFFFFFF") { + 0xFFFF_FFFF => print_endline("ok"), + _ => print_endline("fail"), + }; + match hex_bits_32("0xffffffff") { + 0xFFFF_FFFF => print_endline("ok"), + _ => print_endline("fail"), + }; + match hex_bits_32(0xFFFF_FFFF) { + "0xffffffff" => print_endline("ok"), + s => print_endline(s), + }; + match hex_bits_32(0xFFFF_FFFF) { + "0xFFFFFFFF" => print_endline("fail"), + s => print_endline(concat_str("ok ", s)), + } +}