From 6f8d5bdacd5accbd4aa689071304d3255792030b Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Fri, 14 Dec 2018 11:06:31 +0000
Subject: Add truncateLSB builtin useful for implementing Cheri Concentrate.
 Also add bool_of_bit and bit_of_bool in sail_lib

---
 lib/sail.c          | 10 ++++++++++
 lib/sail.h          |  1 +
 lib/vector_dec.sail | 13 +++++++++++++
 src/sail_lib.ml     | 12 +++++++++++-
 4 files changed, 35 insertions(+), 1 deletion(-)

diff --git a/lib/sail.c b/lib/sail.c
index f897fc11..0fcb5d55 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -741,6 +741,16 @@ void sail_truncate(lbits *rop, const lbits op, const sail_int len)
   normalize_lbits(rop);
 }
 
+void sail_truncateLSB(lbits *rop, const lbits op, const sail_int len)
+{
+  uint64_t rlen = mpz_get_ui(len);
+  assert(op.len >= rlen);
+  rop->len = rlen;
+  // similar to vector_subrange_lbits above -- right shift LSBs away
+  mpz_fdiv_q_2exp(*rop->bits, *op.bits, op.len - rlen);
+  normalize_lbits(rop);
+}
+
 fbits bitvector_access(const lbits op, const sail_int n_mpz)
 {
   uint64_t n = mpz_get_ui(n_mpz);
diff --git a/lib/sail.h b/lib/sail.h
index 1310dd72..53b9c6be 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -256,6 +256,7 @@ void vector_subrange_lbits(lbits *rop,
 			       const sail_int m_mpz);
 
 void sail_truncate(lbits *rop, const lbits op, const sail_int len);
+void sail_truncateLSB(lbits *rop, const lbits op, const sail_int len);
 
 fbits bitvector_access(const lbits op, const sail_int n_mpz);
 
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 6953264f..4e4bad5a 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -35,6 +35,9 @@ val sail_sign_extend = "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('
 
 val sail_zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 
+/*!
+THIS`(v, n)` truncates `v`, keeping only the _least_ significant `n` bits.
+ */
 val truncate = {
   ocaml: "vector_truncate",
   lem: "vector_truncate",
@@ -42,6 +45,16 @@ val truncate = {
   c: "sail_truncate"
 } : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
 
+/*!
+THIS`(v, n)` truncates `v`, keeping only the _most_ significant `n` bits.
+ */
+val truncateLSB = {
+  ocaml: "vector_truncateLSB",
+  lem: "vector_truncateLSB",
+  coq: "vector_truncateLSB",
+  c: "sail_truncateLSB"
+} : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
+
 val sail_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (atom('len), vector('v, dec, bit)) -> vector('len, dec, bit)
 
 function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail_zero_extend(v, len)
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 026172ec..c0bf80fa 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -160,6 +160,8 @@ let update_subrange (xs, n, m, ys) =
 
 let vector_truncate (xs, n) = List.rev (take (Big_int.to_int n) (List.rev xs))
 
+let vector_truncateLSB (xs, n) = take (Big_int.to_int n) xs
+
 let length xs = Big_int.of_int (List.length xs)
 
 let big_int_of_bit = function
@@ -359,6 +361,14 @@ let int_of_bit = function
   | B0 -> 0
   | B1 -> 1
 
+let bool_of_bit = function
+  | B0 -> false
+  | B1 -> true
+
+let bit_of_bool = function
+  | false -> B0
+  | true -> B1
+
 let bigint_of_bit b = Big_int.of_int (int_of_bit b)
 
 let string_of_hex = function
@@ -1138,7 +1148,7 @@ let rand_zvector (g : 'generators) (size : int) (order : bool) (elem_gen : 'gene
   Util.list_init size (fun _ -> elem_gen g)
 
 let rand_zbit (g : 'generators) : bit =
-  if Random.bool() then B0 else B1
+  bit_of_bool (Random.bool())
 
 let rand_zbool (g : 'generators) : bool =
   Random.bool()
-- 
cgit v1.2.3