summaryrefslogtreecommitdiff
path: root/src/gen_lib
diff options
context:
space:
mode:
Diffstat (limited to 'src/gen_lib')
-rw-r--r--src/gen_lib/prompt.lem2
-rw-r--r--src/gen_lib/sail_values.lem152
-rw-r--r--src/gen_lib/state.lem6
3 files changed, 109 insertions, 51 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 70850dc1..0944f42b 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -78,6 +78,8 @@ let read_reg_bitfield reg regfield =
read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
return (extract_only_element v)
+let reg_deref = read_reg
+
val write_reg_aux : reg_name -> vector bitU -> M unit
let write_reg_aux reg_name v =
let regval = external_reg_value reg_name v in
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index f148c1ff..f1541466 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -11,6 +11,12 @@ type nn = natural
val pow : integer -> integer -> integer
let pow m n = m ** (natFromInteger n)
+let bool_or (l, r) = (l || r)
+let bool_and (l, r) = (l && r)
+let bool_xor (l, r) = xor l r
+
+let list_append (l, r) = l ++ r
+
let rec replace bs ((n : integer),b') = match bs with
| [] -> []
| b :: bs ->
@@ -18,6 +24,7 @@ let rec replace bs ((n : integer),b') = match bs with
else b :: replace bs (n - 1,b')
end
+let upper n = n
(*** Bits *)
type bitU = B0 | B1 | BU
@@ -39,6 +46,8 @@ let bitU_to_bool = function
| BU -> failwith "to_bool applied to BU"
end
+let cast_bit_bool = bitU_to_bool
+
let bit_lifted_of_bitU = function
| B0 -> Bitl_zero
| B1 -> Bitl_one
@@ -196,6 +205,9 @@ let access (Vector bs start is_inc) n =
if is_inc then List_extra.nth bs (natFromInteger (n - start))
else List_extra.nth bs (natFromInteger (start - n))
+let vector_access_inc (v, i) = access v i
+let vector_access_dec (v, i) = access v i
+
val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a
let update_pos v n b =
update_aux v n n [b]
@@ -238,9 +250,12 @@ let reset_bitvector_start v =
let set_bitvector_start_to_length v =
set_bitvector_start (bvlength v - 1) v
-let bitvector_concat (Bitvector bs start is_inc) (Bitvector bs' _ _) =
+let bitvector_concat (Bitvector bs start is_inc, Bitvector bs' _ _) =
Bitvector (word_concat bs bs') start is_inc
+let norm_dec = reset_bitvector_start
+let adjust_dec = reset_bitvector_start
+
let inline (^^^) = bitvector_concat
val bvslice : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b
@@ -252,6 +267,13 @@ let bvslice (Bitvector bs start is_inc) i j =
let subvector_bits = word_extract lo hi bs in
Bitvector subvector_bits i is_inc
+let bitvector_subrange_inc (v, i, j) = bvslice v i j
+let bitvector_subrange_dec (v, i, j) = bvslice v i j
+
+let vector_subrange_bl (v, i, j) =
+ let v' = slice (bvec_to_vec v) i j in
+ get_elems v'
+
(* this is for the vector slicing introduced in vector-concat patterns: i and j
index into the "raw data", the list of bits. Therefore getting the bit list is
easy, but the start index has to be transformed to match the old vector start
@@ -277,19 +299,20 @@ val bvupdate : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b
let bvupdate v i j (Bitvector bs' _ _) =
bvupdate_aux v i j bs'
-(* TODO: decide between nat/natural, change either here or in machine_word *)
-val getBit' : forall 'a. mword 'a -> nat -> bool
-let getBit' w n = getBit w (naturalFromNat n)
-
val bvaccess : forall 'a. bitvector 'a -> integer -> bitU
let bvaccess (Bitvector bs start is_inc) n = bool_to_bitU (
- if is_inc then getBit' bs (natFromInteger (n - start))
- else getBit' bs (natFromInteger (start - n)))
+ if is_inc then getBit bs (natFromInteger (n - start))
+ else getBit bs (natFromInteger (start - n)))
val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bitU -> bitvector 'a
let bvupdate_pos v n b =
bvupdate_aux v n n ((wordFromNatural (if bitU_to_bool b then 1 else 0)) : mword ty1)
+let bitvector_access_inc (v, i) = bvaccess v i
+let bitvector_access_dec (v, i) = bvaccess v i
+let bitvector_update_pos_dec (v, i, b) = bvupdate_pos v i b
+let bitvector_update_dec (v, i, j, v') = bvupdate v i j v'
+
(*** Bit vector operations *)
let extract_only_element (Vector elems _ _) = match elems with
@@ -308,6 +331,9 @@ let extract_only_bit (Bitvector elems _ _) =
else
failwith "extract_single_bit called for vector with more bits"*)
+let cast_vec_bool v = bitU_to_bool (extract_only_bit v)
+let cast_bit_vec b = vec_to_bvec (Vector [b] 0 false)
+
let pp_bitu_vector (Vector elems start inc) =
let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
"Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc
@@ -409,19 +435,25 @@ end
let add_one_bit_ignore_overflow bits =
List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
-let to_vec is_inc ((len : integer),(n : integer)) =
- let start = if is_inc then 0 else len - 1 in
+let to_vec is_inc ((n : integer)) =
+ (* Bitvector length is determined by return type *)
let bits = wordFromInteger n in
- if integerFromNat (word_length bits) = len then
+ let len = integerFromNat (word_length bits) in
+ let start = if is_inc then 0 else len - 1 in
+ (*if integerFromNat (word_length bits) = len then*)
Bitvector bits start is_inc
- else
- failwith "Vector length mismatch in to_vec"
+ (*else
+ failwith "Vector length mismatch in to_vec"*)
let to_vec_big = to_vec
let to_vec_inc = to_vec true
let to_vec_dec = to_vec false
+let cast_0_vec = to_vec_dec
+let cast_1_vec = to_vec_dec
+let cast_01_vec = to_vec_dec
+
(* TODO: Think about undefined bit(vector)s *)
let to_vec_undef is_inc (len : integer) =
Bitvector (failwith "undefined bitvector") (if is_inc then 0 else len-1) is_inc
@@ -429,19 +461,25 @@ let to_vec_undef is_inc (len : integer) =
let to_vec_inc_undef = to_vec_undef true
let to_vec_dec_undef = to_vec_undef false
-let exts (len, vec) = to_vec (bvget_dir vec) (len,signed vec)
-let extz (len, vec) = to_vec (bvget_dir vec) (len,unsigned vec)
+let exts (vec) = to_vec (bvget_dir vec) (signed vec)
+let extz (vec) = to_vec (bvget_dir vec) (unsigned vec)
+
+let exts_big (vec) = to_vec_big (bvget_dir vec) (signed_big vec)
+let extz_big (vec) = to_vec_big (bvget_dir vec) (unsigned_big vec)
-let exts_big (len, vec) = to_vec_big (bvget_dir vec) (len, signed_big vec)
-let extz_big (len, vec) = to_vec_big (bvget_dir vec) (len, unsigned_big vec)
+let extz_bl (bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false)
-let add = integerAdd
-let add_signed = integerAdd
-let minus = integerMinus
-let multiply = integerMult
-let modulo = hardware_mod
+let add (l,r) = integerAdd l r
+let add_signed (l,r) = integerAdd l r
+let sub (l,r) = integerMinus l r
+let multiply (l,r) = integerMult l r
+let quotient (l,r) = integerDiv l r
+let modulo (l,r) = hardware_mod l r
let quot = hardware_quot
-let power = integerPow
+let power (l,r) = integerPow l r
+
+let sub_int = sub
+let mul_int = multiply
(* TODO: this, and the definitions that use it, currently require Size for
to_vec, which I'd rather avoid in favour of library versions; the
@@ -449,7 +487,7 @@ let power = integerPow
let arith_op_vec op sign (size : integer) (Bitvector _ _ is_inc as l) r =
let (l',r') = (to_num sign l, to_num sign r) in
let n = op l' r' in
- to_vec is_inc (size * (bvlength l),n)
+ to_vec is_inc (n)
(* add_vec
@@ -464,9 +502,15 @@ let minus_VVV = arith_op_vec integerMinus false 1
let mult_VVV = arith_op_vec integerMult false 2
let multS_VVV = arith_op_vec integerMult true 2
+let mul_vec (l, r) = mult_VVV l r
+let mul_svec (l, r) = multS_VVV l r
+
+let add_vec (l, r) = add_VVV l r
+let sub_vec (l, r) = minus_VVV l r
+
val arith_op_vec_range : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> integer -> bitvector 'b
let arith_op_vec_range op sign size (Bitvector _ _ is_inc as l) r =
- arith_op_vec op sign size l ((to_vec is_inc (bvlength l,r)) : bitvector 'a)
+ arith_op_vec op sign size l ((to_vec is_inc (r)) : bitvector 'a)
(* add_vec_range
* add_vec_range_signed
@@ -480,9 +524,12 @@ let minus_VIV = arith_op_vec_range integerMinus false 1
let mult_VIV = arith_op_vec_range integerMult false 2
let multS_VIV = arith_op_vec_range integerMult true 2
+let add_vec_int (l, r) = add_VIV l r
+let sub_vec_int (l, r) = minus_VIV l r
+
val arith_op_range_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> integer -> bitvector 'a -> bitvector 'b
let arith_op_range_vec op sign size l (Bitvector _ _ is_inc as r) =
- arith_op_vec op sign size ((to_vec is_inc (bvlength r, l)) : bitvector 'a) r
+ arith_op_vec op sign size ((to_vec is_inc (l)) : bitvector 'a) r
(* add_range_vec
* add_range_vec_signed
@@ -528,10 +575,10 @@ let arith_op_vec_vec_range op sign l r =
let add_VVI = arith_op_vec_vec_range integerAdd false
let addS_VVI = arith_op_vec_vec_range integerAdd true
-let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l)r =
+let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l) r =
let l' = to_num sign l in
let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
- to_vec is_inc (bvlength l * size,n)
+ to_vec is_inc (n)
(* add_vec_bit
* add_vec_bit_signed
@@ -610,17 +657,19 @@ let shift_op_vec op (Bitvector bs start is_inc,(n : integer)) =
let n = natFromInteger n in
match op with
| LL_shift (*"<<"*) ->
- Bitvector (shiftLeft bs (naturalFromNat n)) start is_inc
+ Bitvector (shiftLeft bs n) start is_inc
| RR_shift (*">>"*) ->
- Bitvector (shiftRight bs (naturalFromNat n)) start is_inc
+ Bitvector (shiftRight bs n) start is_inc
| LLL_shift (*"<<<"*) ->
- Bitvector (rotateLeft (naturalFromNat n) bs) start is_inc
+ Bitvector (rotateLeft n bs) start is_inc
end
let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*)
let bitwise_rightshift = shift_op_vec RR_shift (*">>"*)
let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*)
+let shiftl = bitwise_leftshift
+
let rec arith_op_no0 (op : integer -> integer -> integer) l r =
if r = 0
then Nothing
@@ -681,19 +730,19 @@ let rec repeat xs n =
if n = 0 then []
else xs ++ repeat xs (n-1)
-(*
-let duplicate bit length =
- Vector (repeat [bit] length) (if dir then 0 else length - 1) dir
- *)
-let compare_op op (l,r) = bool_to_bitU (op l r)
+let duplicate (bit, length) =
+ vec_to_bvec (Vector (repeat [bit] length) (length - 1) false)
+
+let duplicate_to_list (bit, length) = repeat [bit] length
+
+let compare_op op (l,r) = (op l r)
let lt = compare_op (<)
let gt = compare_op (>)
let lteq = compare_op (<=)
let gteq = compare_op (>=)
-
let compare_op_vec op sign (l,r) =
let (l',r') = (to_num sign l, to_num sign r) in
compare_op op (l',r')
@@ -712,6 +761,8 @@ let gt_vec_unsigned = compare_op_vec (>) false
let lteq_vec_unsigned = compare_op_vec (<=) false
let gteq_vec_unsigned = compare_op_vec (>=) false
+let lt_svec = lt_vec_signed
+
let compare_op_vec_range op sign (l,r) =
compare_op op ((to_num sign l),r)
@@ -728,20 +779,23 @@ let gt_range_vec = compare_op_range_vec (>) true
let lteq_range_vec = compare_op_range_vec (<=) true
let gteq_range_vec = compare_op_range_vec (>=) true
-let eq (l,r) = bool_to_bitU (l = r)
-let eq_range (l,r) = bool_to_bitU (l = r)
-let eq_vec (l,r) = bool_to_bitU (l = r)
-let eq_bit (l,r) = bool_to_bitU (l = r)
+val eq : forall 'a. Eq 'a => 'a * 'a -> bool
+let eq (l,r) = (l = r)
+let eq_range (l,r) = (l = r)
+
+val eq_vec : forall 'a. bitvector 'a * bitvector 'a -> bool
+let eq_vec (l,r) = (l = r)
+let eq_bit (l,r) = (l = r)
let eq_vec_range (l,r) = eq (to_num false l,r)
let eq_range_vec (l,r) = eq (l, to_num false r)
let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
-let neq (l,r) = bitwise_not_bit (eq (l,r))
-let neq_bit (l,r) = bitwise_not_bit (eq_bit (l,r))
-let neq_range (l,r) = bitwise_not_bit (eq_range (l,r))
-let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r))
-let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r))
-let neq_range_vec (l,r) = bitwise_not_bit (eq_range_vec (l,r))
+let neq (l,r) = not (eq (l,r))
+let neq_bit (l,r) = not (eq_bit (l,r))
+let neq_range (l,r) = not (eq_range (l,r))
+let neq_vec (l,r) = not (eq_vec_vec (l,r))
+let neq_vec_range (l,r) = not (eq_vec_range (l,r))
+let neq_range_vec (l,r) = not (eq_range_vec (l,r))
val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a
@@ -757,9 +811,9 @@ let make_bitvector_undef length =
(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)
-let mask (n,bv) =
- let len = bvlength bv in
- bvslice_raw bv (len - n) (len - 1)
+(* TODO *)
+val mask : forall 'a 'b. Size 'b => bitvector 'a -> bitvector 'b
+let mask (Bitvector w i dir) = (Bitvector (zeroExtend w) i dir)
val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 709052fe..1bc1ad55 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -126,7 +126,7 @@ val read_reg : forall 'a. Size 'a => register -> M (bitvector 'a)
let read_reg reg state =
let v = get_reg state (name_of_reg reg) in
[(Left (vec_to_bvec v),state)]
-let read_reg_range reg i j state =
+(*let read_reg_range reg i j state =
let v = slice (get_reg state (name_of_reg reg)) i j in
[(Left (vec_to_bvec v),state)]
let read_reg_bit reg i state =
@@ -137,7 +137,9 @@ let read_reg_field reg regfield =
read_reg_range reg i j
let read_reg_bitfield reg regfield =
let (i,_) = register_field_indices reg regfield in
- read_reg_bit reg i
+ read_reg_bit reg i *)
+
+let reg_deref = read_reg
val write_reg : forall 'a. Size 'a => register -> bitvector 'a -> M unit
let write_reg reg v state =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 12:10:21 +0000