Add dec_bits library file

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 <a        */
+/*  href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous          */
+/*  Engineering for Mainstream Systems</a>, 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 <option.sail>
+$include <vector.sail>
+$include <string.sail>
+
+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

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)) {

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);

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)

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 (_, _, _) = ()
 

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);
        ]
     )

test/c/lib_dec_bits.expect

@@ -0,0 +1,6 @@
+ok
+ok
+ok
+ok
+ok
+ok

test/c/lib_dec_bits.sail

@@ -0,0 +1,31 @@
+default Order dec
+
+$include <prelude.sail>
+$include <dec_bits.sail>
+
+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"),
+    };
+}