From e8272f95df735bef3b41c336e66ecb5824350086 Mon Sep 17 00:00:00 2001
From: Yui5427 <785369607@qq.com>
Date: Sun, 22 Dec 2024 23:56:22 +0800
Subject: [PATCH] Add dec_bits library file
---
lib/dec_bits.sail | 70 ++++++++++++++++++++++++++++++++++++++
lib/sail.c | 52 ++++++++++++++++++++++++++++
lib/sail.h | 4 +++
src/bin/dune | 1 +
src/lib/sail_lib.ml | 25 ++++++++++++++
src/lib/value.ml | 10 ++++++
test/c/lib_dec_bits.expect | 6 ++++
test/c/lib_dec_bits.sail | 31 +++++++++++++++++
8 files changed, 199 insertions(+)
create mode 100644 lib/dec_bits.sail
create mode 100644 test/c/lib_dec_bits.expect
create mode 100644 test/c/lib_dec_bits.sail
diff --git a/lib/dec_bits.sail b/lib/dec_bits.sail
new file mode 100644
index 000000000..b4cafe9e1
--- /dev/null
+++ b/lib/dec_bits.sail
@@ -0,0 +1,70 @@
+/*==========================================================================*/
+/* 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"). */
+/* */
+/* SPDX-License-Identifier: BSD-2-Clause */
+/*==========================================================================*/
+
+$ifndef _DEC_BITS
+$define _DEC_BITS
+
+$include
+$include
+$include
+
+val "parse_dec_bits" : forall 'n, 'n > 0. (int('n), string) -> bits('n)
+
+val "valid_dec_bits" : forall 'n, 'n > 0. (int('n), string) -> bool
+
+val dec_bits : forall 'n, 'n > 0. bits('n) <-> (int('n), string)
+
+function dec_bits_forwards(bv) = (length(bv), dec_str(unsigned(bv)))
+function dec_bits_forwards_matches(bv) = true
+
+function dec_bits_backwards(n, str) = parse_dec_bits(n, str)
+function dec_bits_backwards_matches(n, str) = valid_dec_bits(n, str)
+
+mapping dec_bits_1 : bits(1) <-> string = { dec_bits(1, s) <-> s }
+mapping dec_bits_8 : bits(8) <-> string = { dec_bits(8, s) <-> s }
+mapping dec_bits_32 : bits(32) <-> string = { dec_bits(32, s) <-> s }
+
+$endif _DEC_BITS
diff --git a/lib/sail.c b/lib/sail.c
index 8db2ab1ba..3b7cb3aa4 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -1659,6 +1659,58 @@ void decimal_string_of_lbits(sail_string *str, const lbits op)
gmp_asprintf(str, "%Z", *op.bits);
}
+void parse_dec_bits(lbits *res, const mpz_t n, const_sail_string dec)
+{
+ if (!valid_dec_bits(n, dec)) {
+ goto failure;
+ }
+
+ mpz_t value;
+ mpz_init(value);
+
+ if (mpz_set_str(value, dec, 10) == 0) {
+ res->len = mpz_get_ui(n);
+ mpz_set(*(res->bits), value);
+ mpz_clear(value);
+ return;
+ }
+ mpz_clear(value);
+
+failure:
+ res->len = mpz_get_ui(n);
+ mpz_set_ui(*(res->bits), 0);
+}
+
+bool valid_dec_bits(const mpz_t n, const_sail_string dec)
+{
+ size_t len = strlen(dec);
+
+ if (len < 1) {
+ return false;
+ }
+
+ for (size_t i = 0; i < len; i++) {
+ if (!('0' <= dec[i] && dec[i] <= '9')) {
+ return false;
+ }
+ }
+
+ mpz_t value;
+ mpz_init(value);
+
+ if (mpz_set_str(value, dec, 10) != 0) {
+ mpz_clear(value);
+ return false;
+ }
+
+ size_t bit_width = mpz_sizeinbase(value, 2);
+
+ bool valid = (bit_width <= mpz_get_ui(n));
+
+ mpz_clear(value);
+ return valid;
+}
+
void parse_hex_bits(lbits *res, const mpz_t n, const_sail_string hex)
{
if (!valid_hex_bits(n, hex)) {
diff --git a/lib/sail.h b/lib/sail.h
index e035b9218..0495c2477 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -492,6 +492,10 @@ void decimal_string_of_fbits(sail_string *str, const fbits op);
/* ***** Mapping support ***** */
+void parse_dec_bits(lbits *res, const mpz_t n, const char *dec);
+
+bool valid_dec_bits(const mpz_t n, const char *dec);
+
void parse_hex_bits(lbits *stro, const mpz_t n, const_sail_string str);
bool valid_hex_bits(const mpz_t n, const_sail_string str);
diff --git a/src/bin/dune b/src/bin/dune
index 38c3f278c..10e3474e3 100644
--- a/src/bin/dune
+++ b/src/bin/dune
@@ -131,6 +131,7 @@
(%{workspace_root}/lib/isla.sail as lib/isla.sail)
(%{workspace_root}/lib/main.ml as lib/main.ml)
(%{workspace_root}/lib/mapping.sail as lib/mapping.sail)
+ (%{workspace_root}/lib/dec_bits.sail as lib/dec_bits.sail)
(%{workspace_root}/lib/hex_bits.sail as lib/hex_bits.sail)
(%{workspace_root}/lib/hex_bits_signed.sail as lib/hex_bits_signed.sail)
(%{workspace_root}/lib/mono_rewrites.sail as lib/mono_rewrites.sail)
diff --git a/src/lib/sail_lib.ml b/src/lib/sail_lib.ml
index 9e9f8c95b..f222cbbe4 100644
--- a/src/lib/sail_lib.ml
+++ b/src/lib/sail_lib.ml
@@ -1137,6 +1137,31 @@ let parse_hex_bits (n, s) =
|> Util.take (Big_int.to_int n)
|> List.rev
+let valid_dec_bits (n, s) =
+ if String.length s > 0 && s.[0] = '-' then false
+ else
+ let is_valid = ref true in
+ String.iter (fun c -> is_valid := !is_valid && ('0' <= c && c <= '9')) s;
+ if not !is_valid then false
+ else
+ let rec count_bits n =
+ if Big_int.equal n Big_int.zero then 0
+ else 1 + count_bits (Big_int.shift_right n 1)
+ in
+ let dec_value = Big_int.of_string s in
+ count_bits dec_value <= Big_int.to_int n
+
+let parse_dec_bits (n, s) =
+ let padding = zeros n in
+ if not (valid_dec_bits (n, s)) then padding
+ else
+ let dec_value = Big_int.of_string s in
+ let bits = bits_of_big_int (Big_int.to_int n) dec_value in
+ padding @ bits
+ |> List.rev
+ |> Util.take (Big_int.to_int n)
+ |> List.rev
+
let trace_memory_write (_, _, _) = ()
let trace_memory_read (_, _, _) = ()
diff --git a/src/lib/value.ml b/src/lib/value.ml
index 6c80fbddd..78e97619e 100644
--- a/src/lib/value.ml
+++ b/src/lib/value.ml
@@ -622,6 +622,14 @@ let value_parse_hex_bits = function
| [v1; v2] -> mk_vector (Sail_lib.parse_hex_bits (coerce_int v1, coerce_string v2))
| _ -> failwith "value parse_hex_bits"
+let value_valid_dec_bits = function
+ | [v1; v2] -> V_bool (Sail_lib.valid_dec_bits (coerce_int v1, coerce_string v2))
+ | _ -> failwith "value valid_dec_bits"
+
+let value_parse_dec_bits = function
+ | [v1; v2] -> mk_vector (Sail_lib.parse_dec_bits (coerce_int v1, coerce_string v2))
+ | _ -> failwith "value parse_dec_bits"
+
let value_emulator_read_mem = function
| [v1; v2; v3] -> mk_vector (Sail_lib.emulator_read_mem (coerce_int v1, coerce_bv v2, coerce_int v3))
| _ -> failwith "value emulator_read_mem"
@@ -822,6 +830,8 @@ let primops =
("hex_str_upper", value_hex_str_upper);
("parse_hex_bits", value_parse_hex_bits);
("valid_hex_bits", value_valid_hex_bits);
+ ("parse_dec_bits", value_parse_dec_bits);
+ ("valid_dec_bits", value_valid_dec_bits);
("skip", fun _ -> V_unit);
]
)
diff --git a/test/c/lib_dec_bits.expect b/test/c/lib_dec_bits.expect
new file mode 100644
index 000000000..7780b88b4
--- /dev/null
+++ b/test/c/lib_dec_bits.expect
@@ -0,0 +1,6 @@
+ok
+ok
+ok
+ok
+ok
+ok
diff --git a/test/c/lib_dec_bits.sail b/test/c/lib_dec_bits.sail
new file mode 100644
index 000000000..2050038ef
--- /dev/null
+++ b/test/c/lib_dec_bits.sail
@@ -0,0 +1,31 @@
+default Order dec
+
+$include
+$include
+
+function main() -> unit = {
+ match dec_bits_1("1") {
+ 0b1 => print_endline("ok"),
+ _ => print_endline("fail"),
+ };
+ match dec_bits_1(0b1) {
+ "1" => print_endline("ok"),
+ _ => print_endline("fail"),
+ };
+ match dec_bits_8("255") {
+ 0b1111_1111 => print_endline("ok"),
+ _ => print_endline("fail"),
+ };
+ match dec_bits_8(0b1111_1111) {
+ "255" => print_endline("ok"),
+ s => print_endline(s),
+ };
+ match dec_bits_8(0b1101_0000) {
+ "208" => print_endline("ok"),
+ s => print_endline("fail"),
+ };
+ match dec_bits_8("208") {
+ 0b1101_0000 => print_endline("ok"),
+ s => print_endline("fail"),
+ };
+}