summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--aarch64/aarch64_extras_embed_sequential.lem18
-rw-r--r--aarch64/prelude.sail8
-rw-r--r--lib/isabelle/Makefile6
-rw-r--r--lib/isabelle/ROOT3
-rw-r--r--riscv/prelude.sail8
-rw-r--r--riscv/riscv_extras_embed_sequential.lem22
-rw-r--r--src/gen_lib/sail_operators.lem283
-rw-r--r--src/gen_lib/sail_operators_mwords.lem770
-rw-r--r--src/gen_lib/sail_values.lem131
-rw-r--r--src/gen_lib/state_bitlists.lem29
-rw-r--r--src/process_file.ml5
11 files changed, 458 insertions, 825 deletions
diff --git a/aarch64/aarch64_extras_embed_sequential.lem b/aarch64/aarch64_extras_embed_sequential.lem
index a9e2e9e3..4f9e0fe3 100644
--- a/aarch64/aarch64_extras_embed_sequential.lem
+++ b/aarch64/aarch64_extras_embed_sequential.lem
@@ -1,10 +1,9 @@
open import Pervasives_extra
open import Sail_impl_base
open import Sail_values
-open import Sail_operators
+open import Sail_operators_bitlists
open import State
-
type ty2048
instance (Size ty2048) let size = 2048 end
declare isabelle target_rep type ty2048 = `2048`
@@ -20,12 +19,16 @@ val putchar : integer -> unit
let putchar _ = ()
declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
-let inline uint = unsigned
-let inline sint = signed
+val uint : list bitU -> integer
+let uint = unsigned
+val sint : list bitU -> integer
+let sint = signed
+val slice : list bitU -> integer -> integer -> list bitU
let slice v lo len =
subrange_vec_dec v (lo + len - 1) lo
+val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU
let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
update_subrange_vec_dec out (n + slice_len - 1) n v
@@ -35,8 +38,10 @@ let get_slice_int_bl len n lo =
let bits = bits_of_int (hi + 1) n in
get_bits false bits hi lo
+val get_slice_int : integer -> integer -> integer -> list bitU
let get_slice_int len n lo = of_bits (get_slice_int_bl len n lo)
+val set_slice_int : integer -> integer -> integer -> list bitU -> integer
let set_slice_int len n lo v =
let hi = lo + len - 1 in
let bits = bitlist_of_int n in
@@ -48,7 +53,9 @@ let ext_slice signed v i j =
let len = length v in
let bits = get_bits false (bits_of v) i j in
of_bits (if signed then exts_bits len bits else extz_bits len bits)
+val exts_slice : list bitU -> integer -> integer -> list bitU
let exts_slice v i j = ext_slice true v i j
+val extz_slice : list bitU -> integer -> integer -> list bitU
let extz_slice v i j = ext_slice false v i j
val shr_int : ii -> ii -> ii
@@ -90,6 +97,7 @@ let hexstring_to_bits s =
| _ -> failwith "hexstring_to_bits called with unexpected string"
end
+val hex_slice : string -> integer -> integer -> list bitU
let hex_slice v len lo =
let hi = len + lo - 1 in
let bits = extz_bits (len + lo) (hexstring_to_bits v) in
@@ -101,7 +109,9 @@ let undefined_string () = ""
let undefined_unit () = ()
let undefined_int () = (0:ii)
let undefined_bool () = false
+val undefined_vector : forall 'a. integer -> 'a -> list 'a
let undefined_vector len u = repeat [u] len
+val undefined_bitvector : integer -> list bitU
let undefined_bitvector len = duplicate B0 len
let undefined_bits len = undefined_bitvector len
let undefined_bit () = B0
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 8851b7aa..a09209d6 100644
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -87,17 +87,17 @@ function neq_anything (x, y) = not_bool(x == y)
overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
-val builtin_and_vec = {ocaml: "and_vec", lem: "Sail_operators.and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val builtin_and_vec = {ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-val and_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
+val and_vec = {lem: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
function and_vec (xs, ys) = builtin_and_vec(xs, ys)
overload operator & = {and_bool, and_vec}
-val builtin_or_vec = {ocaml: "or_vec", lem: "Sail_operators.or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-val or_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
+val or_vec = {lem: "or_vec"}: forall 'n. (bits('n), bits('n)) -> bits('n)
function or_vec (xs, ys) = builtin_or_vec(xs, ys)
diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index 407e6871..84af5d75 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -1,4 +1,5 @@
THYS = Sail_impl_base.thy Sail_values.thy Sail_operators.thy \
+ Sail_operators_mwords.thy Sail_operators_bitlists.thy \
State_monad.thy State.thy Prompt_monad.thy Prompt.thy
EXTRA_THYS = State_monad_extras.thy Prompt_monad_extras.thy
@@ -22,7 +23,10 @@ Sail_values.thy: ../../src/gen_lib/sail_values.lem Sail_impl_base.thy
Sail_operators.thy: ../../src/gen_lib/sail_operators.lem Sail_values.thy
lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
-Sail_operators_mwords.thy: ../../src/gen_lib/sail_operators_mwords.lem Sail_values.thy
+Sail_operators_mwords.thy: ../../src/gen_lib/sail_operators_mwords.lem Sail_operators.thy
+ lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
+
+Sail_operators_bitlists.thy: ../../src/gen_lib/sail_operators_bitlists.lem Sail_operators.thy
lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
State_monad.thy: ../../src/gen_lib/state_monad.lem Sail_values.thy
diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT
index 2062b64b..c798447e 100644
--- a/lib/isabelle/ROOT
+++ b/lib/isabelle/ROOT
@@ -4,7 +4,8 @@ session "Sail" = "LEM" +
Sail_values
State
Prompt
- Sail_operators
+ Sail_operators_mwords
+ Sail_operators_bitlists
(*session "Sail" = "Sail_Base" +
options [document = false]
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 370f9370..754a5cec 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -90,9 +90,9 @@ overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
val and_bool = "and_bool" : (bool, bool) -> bool
-val builtin_and_vec = {ocaml: "and_vec", lem: "Sail_operators.and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val builtin_and_vec = {ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-val and_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
+val and_vec = {lem: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
function and_vec (xs, ys) = builtin_and_vec(xs, ys)
@@ -100,9 +100,9 @@ overload operator & = {and_bool, and_vec}
val or_bool = "or_bool" : (bool, bool) -> bool
-val builtin_or_vec = {ocaml: "or_vec", lem: "Sail_operators.or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-val or_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
+val or_vec = {lem: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
function or_vec (xs, ys) = builtin_or_vec(xs, ys)
diff --git a/riscv/riscv_extras_embed_sequential.lem b/riscv/riscv_extras_embed_sequential.lem
index 2d28f3c2..4ef3ed36 100644
--- a/riscv/riscv_extras_embed_sequential.lem
+++ b/riscv/riscv_extras_embed_sequential.lem
@@ -2,10 +2,12 @@ open import Pervasives
open import Pervasives_extra
open import Sail_impl_base
open import Sail_values
-open import Sail_operators
+open import Sail_operators_mwords
open import State
open import State_monad
+type bitvector 'a = mword 'a
+
let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw
let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw
let MEM_fence_r_r () = barrier Barrier_RISCV_r_r
@@ -13,6 +15,13 @@ let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w
let MEM_fence_w_w () = barrier Barrier_RISCV_w_w
let MEM_fence_i () = barrier Barrier_RISCV_i
+val MEMea : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
+val MEMea_release : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
+val MEMea_strong_release : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
+val MEMea_conditional : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
+val MEMea_conditional_release : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
+val MEMea_conditional_strong_release : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
+
let MEMea addr size = write_mem_ea Write_plain addr size
let MEMea_release addr size = write_mem_ea Write_RISCV_release addr size
let MEMea_strong_release addr size = write_mem_ea Write_RISCV_strong_release addr size
@@ -21,26 +30,35 @@ let MEMea_conditional_release addr size = write_mem_ea Write_RISCV_conditional_
let MEMea_conditional_strong_release addr size
= write_mem_ea Write_RISCV_conditional_strong_release addr size
+val write_ram : forall 'a 'b 'r 'e. Size 'a, Size 'b =>
+ integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> M 'r unit 'e
let write_ram addrsize size hexRAM address value =
write_mem_ea Write_plain address size >>
write_mem_val value >>= fun _ ->
return ()
+val read_ram : forall 'a 'b 'r 'e. Size 'a, Size 'b =>
+ integer -> integer -> bitvector 'a -> bitvector 'a -> M 'r (bitvector 'b) 'e
let read_ram addrsize size hexRAM address =
read_mem Read_plain address size
let speculate_conditional_success () = excl_result ()
+val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> bitvector 'a
let get_slice_int len n lo =
(* TODO: Is this the intended behaviour? *)
let hi = lo + len - 1 in
let bits = bits_of_int (hi + 1) n in
of_bits (get_bits false bits hi lo)
+val sign_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> bitvector 'b
let sign_extend v len = exts_vec len v
+val zero_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> bitvector 'b
let zero_extend v len = extz_vec len v
+val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
let shift_bits_right v m = shiftr v (unsigned m)
+val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
let shift_bits_left v m = shiftl v (unsigned m)
val prerr_endline : string -> unit
@@ -50,7 +68,7 @@ declare ocaml target_rep function prerr_endline = `prerr_endline`
val print_int : string -> integer -> unit
let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
-val print_bits : forall 'a. Bitvector 'a => string -> 'a -> unit
+val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
let print_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs)))
val putchar : integer -> unit
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 230ab84e..b84e659d 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -5,53 +5,22 @@ open import Sail_values
(*** Bit vector operations *)
-val concat_vec : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b, Bitvector 'c => 'a -> 'b -> 'c
-let concat_vec l r = of_bits (bits_of l ++ bits_of r)
+val concat_bv : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b, Bitvector 'c => 'a -> 'b -> 'c
+let concat_bv l r = of_bits (bits_of l ++ bits_of r)
-val cons_vec : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b => bitU -> 'a -> 'b
-let cons_vec b v = of_bits (b :: bits_of v)
+val cons_bv : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b => bitU -> 'a -> 'b
+let cons_bv b v = of_bits (b :: bits_of v)
-let bool_of_vec v = extract_only_element (bits_of v)
-let vec_of_bit len b = of_bits (extz_bits len [b])
-let cast_unit_vec b = of_bits [b]
+let bool_of_bv v = extract_only_element (bits_of v)
+let cast_unit_bv b = of_bits [b]
+let bv_of_bit len b = of_bits (extz_bits len [b])
+let int_of_bv sign = if sign then signed else unsigned
let most_significant v = match bits_of v with
| b :: _ -> b
| _ -> failwith "most_significant applied to empty vector"
end
-let hardware_mod (a: integer) (b:integer) : integer =
- if a < 0 && b < 0
- then (abs a) mod (abs b)
- else if (a < 0 && b >= 0)
- then (a mod b) - b
- else a mod b
-
-(* There are different possible answers for integer divide regarding
-rounding behaviour on negative operands. Positive operands always
-round down so derive the one we want (trucation towards zero) from
-that *)
-let hardware_quot (a:integer) (b:integer) : integer =
- let q = (abs a) / (abs b) in
- if ((a<0) = (b<0)) then
- q (* same sign -- result positive *)
- else
- ~q (* different sign -- result negative *)
-
-let int_of_vec sign = if sign then signed else unsigned
-let vec_of_int len n = of_bits (bits_of_int len n)
-
-let max_64u = (integerPow 2 64) - 1
-let max_64 = (integerPow 2 63) - 1
-let min_64 = 0 - (integerPow 2 63)
-let max_32u = (4294967295 : integer)
-let max_32 = (2147483647 : integer)
-let min_32 = (0 - 2147483648 : integer)
-let max_8 = (127 : integer)
-let min_8 = (0 - 128 : integer)
-let max_5 = (31 : integer)
-let min_5 = (0 - 32 : integer)
-
let get_max_representable_in sign (n : integer) : integer =
if (n = 64) then match sign with | true -> max_64 | false -> max_64u end
else if (n=32) then match sign with | true -> max_32 | false -> max_32u end
@@ -68,106 +37,106 @@ let get_min_representable_in _ (n : integer) : integer =
else if n = 5 then min_5
else 0 - (integerPow 2 (natFromInteger n))
-val bitwise_binop_vec : forall 'a. Bitvector 'a =>
+val bitwise_binop_bv : forall 'a. Bitvector 'a =>
(bool -> bool -> bool) -> 'a -> 'a -> 'a
-let bitwise_binop_vec op l r = of_bits (binop_bits op (bits_of l) (bits_of r))
+let bitwise_binop_bv op l r = of_bits (binop_bits op (bits_of l) (bits_of r))
-let and_vec = bitwise_binop_vec (&&)
-let or_vec = bitwise_binop_vec (||)
-let xor_vec = bitwise_binop_vec xor
-let not_vec v = of_bits (not_bits (bits_of v))
+let and_bv = bitwise_binop_bv (&&)
+let or_bv = bitwise_binop_bv (||)
+let xor_bv = bitwise_binop_bv xor
+let not_bv v = of_bits (not_bits (bits_of v))
-val arith_op_vec : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+val arith_op_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
(integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> 'b
-let arith_op_vec op sign size l r =
- let (l',r') = (int_of_vec sign l, int_of_vec sign r) in
+let arith_op_bv op sign size l r =
+ let (l',r') = (int_of_bv sign l, int_of_bv sign r) in
let n = op l' r' in
- of_bits (bits_of_int (size * length l) n)
+ of_int (size * length l) n
-let add_vec = arith_op_vec integerAdd false 1
-let addS_vec = arith_op_vec integerAdd true 1
-let sub_vec = arith_op_vec integerMinus false 1
-let mult_vec = arith_op_vec integerMult false 2
-let multS_vec = arith_op_vec integerMult true 2
+let add_bv = arith_op_bv integerAdd false 1
+let addS_bv = arith_op_bv integerAdd true 1
+let sub_bv = arith_op_bv integerMinus false 1
+let mult_bv = arith_op_bv integerMult false 2
+let multS_bv = arith_op_bv integerMult true 2
let inline add_mword = Machine_word.plus
let inline sub_mword = Machine_word.minus
val mult_mword : forall 'a 'b. Size 'b => mword 'a -> mword 'a -> mword 'b
let mult_mword l r = times (zeroExtend l) (zeroExtend r)
-val arith_op_vec_int : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+val arith_op_bv_int : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
(integer -> integer -> integer) -> bool -> integer -> 'a -> integer -> 'b
-let arith_op_vec_int op sign size l r =
- let l' = int_of_vec sign l in
+let arith_op_bv_int op sign size l r =
+ let l' = int_of_bv sign l in
let n = op l' r in
- of_bits (bits_of_int (size * length l) n)
+ of_int (size * length l) n
-let add_vec_int = arith_op_vec_int integerAdd false 1
-let addS_vec_int = arith_op_vec_int integerAdd true 1
-let sub_vec_int = arith_op_vec_int integerMinus false 1
-let mult_vec_int = arith_op_vec_int integerMult false 2
-let multS_vec_int = arith_op_vec_int integerMult true 2
+let add_bv_int = arith_op_bv_int integerAdd false 1
+let addS_bv_int = arith_op_bv_int integerAdd true 1
+let sub_bv_int = arith_op_bv_int integerMinus false 1
+let mult_bv_int = arith_op_bv_int integerMult false 2
+let multS_bv_int = arith_op_bv_int integerMult true 2
-val arith_op_int_vec : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+val arith_op_int_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
(integer -> integer -> integer) -> bool -> integer -> integer -> 'a -> 'b
-let arith_op_int_vec op sign size l r =
- let r' = int_of_vec sign r in
+let arith_op_int_bv op sign size l r =
+ let r' = int_of_bv sign r in
let n = op l r' in
- of_bits (bits_of_int (size * length r) n)
+ of_int (size * length r) n
-let add_int_vec = arith_op_int_vec integerAdd false 1
-let addS_int_vec = arith_op_int_vec integerAdd true 1
-let sub_int_vec = arith_op_int_vec integerMinus false 1
-let mult_int_vec = arith_op_int_vec integerMult false 2
-let multS_int_vec = arith_op_int_vec integerMult true 2
+let add_int_bv = arith_op_int_bv integerAdd false 1
+let addS_int_bv = arith_op_int_bv integerAdd true 1
+let sub_int_bv = arith_op_int_bv integerMinus false 1
+let mult_int_bv = arith_op_int_bv integerMult false 2
+let multS_int_bv = arith_op_int_bv integerMult true 2
-let arith_op_vec_bit op sign (size : integer) l r =
- let l' = int_of_vec sign l in
+let arith_op_bv_bit op sign (size : integer) l r =
+ let l' = int_of_bv sign l in
let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
- of_bits (bits_of_int (size * length l) n)
+ of_int (size * length l) n
-let add_vec_bit = arith_op_vec_bit integerAdd false 1
-let addS_vec_bit = arith_op_vec_bit integerAdd true 1
-let sub_vec_bit = arith_op_vec_bit integerMinus true 1
+let add_bv_bit = arith_op_bv_bit integerAdd false 1
+let addS_bv_bit = arith_op_bv_bit integerAdd true 1
+let sub_bv_bit = arith_op_bv_bit integerMinus true 1
-val arith_op_overflow_vec : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+val arith_op_overflow_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
(integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> ('b * bitU * bitU)
-let arith_op_overflow_vec op sign size l r =
+let arith_op_overflow_bv op sign size l r =
let len = length l in
let act_size = len * size in
- let (l_sign,r_sign) = (int_of_vec sign l,int_of_vec sign r) in
- let (l_unsign,r_unsign) = (int_of_vec false l,int_of_vec false r) in
+ let (l_sign,r_sign) = (int_of_bv sign l,int_of_bv sign r) in
+ let (l_unsign,r_unsign) = (int_of_bv false l,int_of_bv false r) in
let n = op l_sign r_sign in
let n_unsign = op l_unsign r_unsign in
- let correct_size = bits_of_int act_size n in
+ let correct_size = of_int act_size n in
let one_more_size_u = bits_of_int (act_size + 1) n_unsign in
let overflow =
if n <= get_max_representable_in sign len &&
n >= get_min_representable_in sign len
then B0 else B1 in
let c_out = most_significant one_more_size_u in
- (of_bits correct_size,overflow,c_out)
+ (correct_size,overflow,c_out)
-let add_overflow_vec = arith_op_overflow_vec integerAdd false 1
-let add_overflow_vec_signed = arith_op_overflow_vec integerAdd true 1
-let sub_overflow_vec = arith_op_overflow_vec integerMinus false 1
-let sub_overflow_vec_signed = arith_op_overflow_vec integerMinus true 1
-let mult_overflow_vec = arith_op_overflow_vec integerMult false 2
-let mult_overflow_vec_signed = arith_op_overflow_vec integerMult true 2
+let add_overflow_bv = arith_op_overflow_bv integerAdd false 1
+let add_overflow_bv_signed = arith_op_overflow_bv integerAdd true 1
+let sub_overflow_bv = arith_op_overflow_bv integerMinus false 1
+let sub_overflow_bv_signed = arith_op_overflow_bv integerMinus true 1
+let mult_overflow_bv = arith_op_overflow_bv integerMult false 2
+let mult_overflow_bv_signed = arith_op_overflow_bv integerMult true 2
-val arith_op_overflow_vec_bit : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+val arith_op_overflow_bv_bit : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
(integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> ('b * bitU * bitU)
-let arith_op_overflow_vec_bit op sign size l r_bit =
+let arith_op_overflow_bv_bit op sign size l r_bit =
let act_size = length l * size in
- let l' = int_of_vec sign l in
- let l_u = int_of_vec false l in
+ let l' = int_of_bv sign l in
+ let l_u = int_of_bv false l in
let (n,nu,changed) = match r_bit with
| B1 -> (op l' 1, op l_u 1, true)
| B0 -> (l',l_u,false)
- | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
+ | BU -> failwith "arith_op_overflow_bv_bit applied to undefined bit"
end in
- let correct_size = bits_of_int act_size n in
+ let correct_size = of_int act_size n in
let one_larger = bits_of_int (act_size + 1) nu in
let overflow =
if changed
@@ -175,32 +144,34 @@ let arith_op_overflow_vec_bit op sign size l r_bit =
if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
then B0 else B1
else B0 in
- (of_bits correct_size,overflow,most_significant one_larger)
+ (correct_size,overflow,most_significant one_larger)
-let add_overflow_vec_bit = arith_op_overflow_vec_bit integerAdd false 1
-let add_overflow_vec_bit_signed = arith_op_overflow_vec_bit integerAdd true 1
-let sub_overflow_vec_bit = arith_op_overflow_vec_bit integerMinus false 1
-let sub_overflow_vec_bit_signed = arith_op_overflow_vec_bit integerMinus true 1
+let add_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd false 1
+let add_overflow_bv_bit_signed = arith_op_overflow_bv_bit integerAdd true 1
+let sub_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus false 1
+let sub_overflow_bv_bit_signed = arith_op_overflow_bv_bit integerMinus true 1
-type shift = LL_shift | RR_shift | LL_rot | RR_rot
+type shift = LL_shift | RR_shift | RR_shift_arith | LL_rot | RR_rot
-val shift_op_vec : forall 'a. Bitvector 'a => shift -> 'a -> integer -> 'a
-let shift_op_vec op v n =
+val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> integer -> 'a
+let shift_op_bv op v n =
match op with
| LL_shift ->
of_bits (get_bits true v n (length v - 1) ++ repeat [B0] n)
| RR_shift ->
of_bits (repeat [B0] n ++ get_bits true v 0 (length v - n - 1))
+ | RR_shift_arith ->
+ of_bits (repeat [most_significant v] n ++ get_bits true v 0 (length v - n - 1))
| LL_rot ->
of_bits (get_bits true v n (length v - 1) ++ get_bits true v 0 (n - 1))
| RR_rot ->
of_bits (get_bits false v 0 (n - 1) ++ get_bits false v n (length v - 1))
end
-let shiftl = shift_op_vec LL_shift (*"<<"*)
-let shiftr = shift_op_vec RR_shift (*">>"*)
-let rotl = shift_op_vec LL_rot (*"<<<"*)
-let rotr = shift_op_vec LL_rot (*">>>"*)
+let shiftl_bv = shift_op_bv LL_shift (*"<<"*)
+let shiftr_bv = shift_op_bv RR_shift (*">>"*)
+let rotl_bv = shift_op_bv LL_rot (*"<<<"*)
+let rotr_bv = shift_op_bv LL_rot (*">>>"*)
let shiftl_mword w n = Machine_word.shiftLeft w (natFromInteger n)
let shiftr_mword w n = Machine_word.shiftRight w (natFromInteger n)
@@ -212,11 +183,11 @@ let rec arith_op_no0 (op : integer -> integer -> integer) l r =
then Nothing
else Just (op l r)
-val arith_op_vec_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+val arith_op_bv_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
(integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> 'b
-let arith_op_vec_no0 op sign size l r =
+let arith_op_bv_no0 op sign size l r =
let act_size = length l * size in
- let (l',r') = (int_of_vec sign l,int_of_vec sign r) in
+ let (l',r') = (int_of_bv sign l,int_of_bv sign r) in
let n = arith_op_no0 op l' r' in
let (representable,n') =
match n with
@@ -225,80 +196,42 @@ let arith_op_vec_no0 op sign size l r =
n' >= get_min_representable_in sign act_size, n')
| _ -> (false,0)
end in
- of_bits (if representable then bits_of_int act_size n' else repeat [BU] act_size)
+ if representable then (of_int act_size n') else (of_bits (repeat [BU] act_size))
-let mod_vec = arith_op_vec_no0 hardware_mod false 1
-let quot_vec = arith_op_vec_no0 hardware_quot false 1
-let quot_vec_signed = arith_op_vec_no0 hardware_quot true 1
+let mod_bv = arith_op_bv_no0 hardware_mod false 1
+let quot_bv = arith_op_bv_no0 hardware_quot false 1
+let quot_bv_signed = arith_op_bv_no0 hardware_quot true 1
let mod_mword = Machine_word.modulo
let quot_mword = Machine_word.unsignedDivide
let quot_mword_signed = Machine_word.signedDivide
-val arith_op_overflow_vec_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
- (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> ('b * bitU * bitU)
-let arith_op_overflow_vec_no0 op sign size l r =
- let rep_size = length r * size in
- let act_size = length l * size in
- let (l',r') = (int_of_vec sign l,int_of_vec sign r) in
- let (l_u,r_u) = (int_of_vec false l,int_of_vec false r) in
- let n = arith_op_no0 op l' r' in
- let n_u = arith_op_no0 op l_u r_u in
- let (representable,n',n_u') =
- match (n, n_u) with
- | (Just n',Just n_u') ->
- ((n' <= get_max_representable_in sign rep_size &&
- n' >= (get_min_representable_in sign rep_size)), n', n_u')
- | _ -> (true,0,0)
- end in
- let (correct_size,one_more) =
- if representable then
- (bits_of_int act_size n', bits_of_int (act_size + 1) n_u')
- else
- (repeat [BU] act_size, repeat [BU] (act_size + 1)) in
- let overflow = if representable then B0 else B1 in
- (of_bits correct_size,overflow,most_significant one_more)
-
-let quot_overflow_vec = arith_op_overflow_vec_no0 hardware_quot false 1
-let quot_overflow_vec_signed = arith_op_overflow_vec_no0 hardware_quot true 1
-
-let arith_op_vec_int_no0 op sign size l r =
- arith_op_vec_no0 op sign size l (of_bits (bits_of_int (length l) r))
-
-let quot_vec_int = arith_op_vec_int_no0 hardware_quot false 1
-let mod_vec_int = arith_op_vec_int_no0 hardware_mod false 1
-
-let replicate_bits v count = of_bits (repeat v count)
-let duplicate bit len = replicate_bits [bit] len
-
-let lt = (<)
-let gt = (>)
-let lteq = (<=)
-let gteq = (>=)
+let arith_op_bv_int_no0 op sign size l r =
+ arith_op_bv_no0 op sign size l (of_int (length l) r)
-val eq : forall 'a. Eq 'a => 'a -> 'a -> bool
-let eq l r = (l = r)
+let quot_bv_int = arith_op_bv_int_no0 hardware_quot false 1
+let mod_bv_int = arith_op_bv_int_no0 hardware_mod false 1
-val eq_vec : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let eq_vec l r = (unsigned l = unsigned r)
+let replicate_bits_bv v count = of_bits (repeat (bits_of v) count)
+let duplicate_bit_bv bit len = replicate_bits_bv [bit] len
-val neq : forall 'a. Eq 'a => 'a -> 'a -> bool
-let neq l r = (l <> r)
+val eq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
+let eq_bv l r = (unsigned l = unsigned r)
-val neq_vec : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let neq_vec l r = (unsigned l <> unsigned r)
+val neq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
+let neq_bv l r = (unsigned l <> unsigned r)
-val ucmp_vec : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool
-let ucmp_vec cmp l r = cmp (unsigned l) (unsigned r)
+val ucmp_bv : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool
+let ucmp_bv cmp l r = cmp (unsigned l) (unsigned r)
-val scmp_vec : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool
-let scmp_vec cmp l r = cmp (signed l) (signed r)
+val scmp_bv : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool
+let scmp_bv cmp l r = cmp (signed l) (signed r)
-let ult_vec = ucmp_vec (<)
-let slt_vec = scmp_vec (<)
-let ugt_vec = ucmp_vec (>)
-let sgt_vec = scmp_vec (>)
-let ulteq_vec = ucmp_vec (<=)
-let slteq_vec = scmp_vec (<=)
-let ugteq_vec = ucmp_vec (>=)
-let sgteq_vec = scmp_vec (>=)
+let ult_bv = ucmp_bv (<)
+let slt_bv = scmp_bv (<)
+let ugt_bv = ucmp_bv (>)
+let sgt_bv = scmp_bv (>)
+let ulteq_bv = ucmp_bv (<=)
+let slteq_bv = scmp_bv (<=)
+let ugteq_bv = ucmp_bv (>=)
+let sgteq_bv = scmp_bv (>=)
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index ff25c37b..3762eb7f 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -2,600 +2,176 @@ open import Pervasives_extra
open import Machine_word
open import Sail_impl_base
open import Sail_values
-
-(* Translating between a type level number (itself 'n) and an integer *)
-
-let size_itself_int x = integerFromNat (size_itself x)
-
-(* NB: the corresponding sail type is forall 'n. atom('n) -> itself('n),
- the actual integer is ignored. *)
-
-val make_the_value : forall 'n. integer -> itself 'n
-let inline make_the_value x = the_value
-
-(*** Bit vector operations *)
-
-let bitvector_length bs = integerFromNat (word_length bs)
-
-(*val set_bitvector_start : forall 'a. (integer * bitvector 'a) -> bitvector 'a
-let set_bitvector_start (new_start, Bitvector bs _ is_inc) =
- Bitvector bs new_start is_inc
-
-let reset_bitvector_start v =
- set_bitvector_start (if (bvget_dir v) then 0 else (bvlength v - 1), 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' _ _) =
- Bitvector (word_concat bs bs') start is_inc*)
-
-let bitvector_concat (bs, bs') = word_concat bs bs'
-
-let inline (^^^) = bitvector_concat
-
-val bvslice : forall 'a 'b. Size 'a => bool -> integer -> bitvector 'a -> integer -> integer -> bitvector 'b
-let bvslice is_inc start bs i j =
- let iN = natFromInteger i in
- let jN = natFromInteger j in
- let startN = natFromInteger start in
- let top = word_length bs - 1 in
- let (hi,lo) = if is_inc then (top+startN-iN,top+startN-jN) else (top-startN+iN,top-startN+jN) in
- word_extract lo hi bs
-
-let bitvector_subrange_inc (start, v, i, j) = bvslice true start v i j
-let bitvector_subrange_dec (start, v, i, j) = bvslice false start v i j
-
-let vector_subrange_bl_dec (start, v, i, j) =
- let v' = slice (bvec_to_vec false start 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
-and the direction. *)
-val bvslice_raw : forall 'a 'b. Size 'b => bitvector 'a -> integer -> integer -> bitvector 'b
-let bvslice_raw bs i j =
- let iN = natFromInteger i in
- let jN = natFromInteger j in
- (*let bits =*) word_extract iN jN bs (*in
- let len = integerFromNat (word_length bits) in
- Bitvector bits (if is_inc then 0 else len - 1) is_inc*)
-
-val bvupdate_aux : forall 'a 'b. Size 'a => bool -> integer -> bitvector 'a -> integer -> integer -> list bitU -> bitvector 'a
-let bvupdate_aux is_inc start bs i j bs' =
- let bits = update_aux is_inc start (List.map to_bitU (bitlistFromWord bs)) i j bs' in
- wordFromBitlist (List.map of_bitU bits)
- (*let iN = natFromInteger i in
- let jN = natFromInteger j in
- let startN = natFromInteger start in
- let top = word_length bs - 1 in
- let (hi,lo) = if is_inc then (top+startN-iN,top+startN-jN) else (top-startN+iN,top-startN+jN) in
- word_update bs lo hi bs'*)
-
-val bvupdate : forall 'a 'b. Size 'a => bool -> integer -> bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a
-let bvupdate is_inc start bs i j bs' =
- bvupdate_aux is_inc start bs i j (List.map to_bitU (bitlistFromWord bs'))
-
-val bvaccess : forall 'a. Size 'a => bool -> integer -> bitvector 'a -> integer -> bitU
-let bvaccess is_inc start bs n = bool_to_bitU (
- let top = integerFromNat (word_length bs) - 1 in
- if is_inc then getBit bs (natFromInteger (top + start - n))
- else getBit bs (natFromInteger (top + n - start)))
-
-val bvupdate_pos : forall 'a. Size 'a => bool -> integer -> bitvector 'a -> integer -> bitU -> bitvector 'a
-let bvupdate_pos is_inc start v n b =
- bvupdate_aux is_inc start v n n [b]
-
-let bitvector_access_inc (start, v, i) = bvaccess true start v i
-let bitvector_access_dec (start, v, i) = bvaccess false start v i
-let bitvector_update_pos_dec (start, v, i, b) = bvupdate_pos false start v i b
-let bitvector_update_subrange_dec (start, v, i, j, v') = bvupdate false start v i j v'
-
-val extract_only_bit : bitvector ty1 -> bitU
-let extract_only_bit elems =
- let l = word_length elems in
- if l = 1 then
- bool_to_bitU (msb elems)
- else if l = 0 then
- failwith "extract_single_bit called for empty vector"
- else
- failwith "extract_single_bit called for vector with more bits"
-
-
-let norm_dec v = v (*reset_bitvector_start*)
-let adjust_start_index (start, v) = v (*set_bitvector_start (start, v)*)
-
-let cast_vec_bool v = bitU_to_bool (extract_only_bit v)
-let cast_bit_vec_basic (start, len, b) = vec_to_bvec (Vector [b] start false)
-let cast_boolvec_bitvec (Vector bs start inc) =
- vec_to_bvec (Vector (List.map bool_to_bitU bs) start inc)
-let cast_vec_bl v = List.map bool_to_bitU (bitlistFromWord v)
-let cast_int_vec n = wordFromInteger n
-let cast_bl_vec (start, len, bs) = wordFromBitlist (List.map bitU_to_bool bs)
-let cast_bl_svec (start, len, bs) = cast_int_vec (bitlist_to_signed bs)
-
-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
-
-
-let most_significant v =
- if word_length v = 0 then
- failwith "most_significant applied to empty vector"
- else
- bool_to_bitU (msb v)
-
-let bitwise_not_bitlist = List.map bitwise_not_bit
-
-let bitwise_not bs = lNot bs
-
-let bitwise_binop op (bsl, bsr) = (op bsl bsr)
-
-let bitwise_and x = bitwise_binop lAnd x
-let bitwise_or x = bitwise_binop lOr x
-let bitwise_xor x = bitwise_binop lXor x
-
-(*let unsigned bs : integer = unsignedIntegerFromWord bs*)
-let unsigned_big = unsigned
-
-let signed v : integer = signedIntegerFromWord v
-
-let hardware_mod (a: integer) (b:integer) : integer =
- if a < 0 && b < 0
- then (abs a) mod (abs b)
- else if (a < 0 && b >= 0)
- then (a mod b) - b
- else a mod b
-
-(* There are different possible answers for integer divide regarding
-rounding behaviour on negative operands. Positive operands always
-round down so derive the one we want (trucation towards zero) from
-that *)
-let hardware_quot (a:integer) (b:integer) : integer =
- let q = (abs a) / (abs b) in
- if ((a<0) = (b<0)) then
- q (* same sign -- result positive *)
- else
- ~q (* different sign -- result negative *)
-
-let quot_signed = hardware_quot
-
-
-let signed_big = signed
-
-let to_num sign = if sign then signed else unsigned
-
-let max_64u = (integerPow 2 64) - 1
-let max_64 = (integerPow 2 63) - 1
-let min_64 = 0 - (integerPow 2 63)
-let max_32u = (4294967295 : integer)
-let max_32 = (2147483647 : integer)
-let min_32 = (0 - 2147483648 : integer)
-let max_8 = (127 : integer)
-let min_8 = (0 - 128 : integer)
-let max_5 = (31 : integer)
-let min_5 = (0 - 32 : integer)
-
-let get_max_representable_in sign (n : integer) : integer =
- if (n = 64) then match sign with | true -> max_64 | false -> max_64u end
- else if (n=32) then match sign with | true -> max_32 | false -> max_32u end
- else if (n=8) then max_8
- else if (n=5) then max_5
- else match sign with | true -> integerPow 2 ((natFromInteger n) -1)
- | false -> integerPow 2 (natFromInteger n)
- end
-
-let get_min_representable_in _ (n : integer) : integer =
- if n = 64 then min_64
- else if n = 32 then min_32
- else if n = 8 then min_8
- else if n = 5 then min_5
- else 0 - (integerPow 2 (natFromInteger n))
-
-val to_bin_aux : natural -> list bitU
-let rec to_bin_aux x =
- if x = 0 then []
- else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
-let to_bin n = List.reverse (to_bin_aux n)
-
-val pad_zero : list bitU -> integer -> list bitU
-let rec pad_zero bits n =
- if n = 0 then bits else pad_zero (B0 :: bits) (n -1)
-
-
-let rec add_one_bit_ignore_overflow_aux bits = match bits with
- | [] -> []
- | B0 :: bits -> B1 :: bits
- | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
- | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
-end
-
-let add_one_bit_ignore_overflow bits =
- List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
-
-val to_norm_vec : forall 'a. Size 'a => integer -> bitvector 'a
-let to_norm_vec (n : integer) = wordFromInteger n
-(*
- (* Bitvector length is determined by return type *)
- let bits = wordFromInteger n in
- 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"*)
-*)
-
-let to_vec_big = to_norm_vec
-
-let to_vec_inc (start, len, n) = to_norm_vec n
-let to_vec_norm_inc (len, n) = to_norm_vec n
-let to_vec_dec (start, len, n) = to_norm_vec n
-let to_vec_norm_dec (len, n) = to_norm_vec n
-
-(* 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 *)
-
-let to_vec_inc_undef = to_vec_undef true
-let to_vec_dec_undef = to_vec_undef false
-
-let exts (start, len, vec) = to_norm_vec (signed vec)
-val extz : forall 'a 'b. Size 'a, Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b
-let extz (start, len, vec) = to_norm_vec (unsigned vec)
-
-let exts_big (start, len, vec) = to_vec_big (signed_big vec)
-let extz_big (start, len, vec) = to_vec_big (unsigned_big vec)
-
-let quot = hardware_quot
-let modulo (l,r) = hardware_mod l r
-
-(* 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
- double-size results for multiplication may be a problem *)
-let arith_op_vec op sign (size : integer) l r =
- let (l',r') = (to_num sign l, to_num sign r) in
- let n = op l' r' in
- to_norm_vec n
-
-
-(* add_vec
- * add_vec_signed
- * minus_vec
- * multiply_vec
- * multiply_vec_signed
- *)
-let add_VVV = arith_op_vec integerAdd false 1
-let addS_VVV = arith_op_vec integerAdd true 1
-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 mult_vec (l, r) = mult_VVV l r
-let mult_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 l r =
- arith_op_vec op sign size l ((to_norm_vec r) : bitvector 'a)
-
-(* add_vec_range
- * add_vec_range_signed
- * minus_vec_range
- * mult_vec_range
- * mult_vec_range_signed
- *)
-let add_VIV = arith_op_vec_range integerAdd false 1
-let addS_VIV = arith_op_vec_range integerAdd true 1
-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 r =
- arith_op_vec op sign size ((to_norm_vec l) : bitvector 'a) r
-
-(* add_range_vec
- * add_range_vec_signed
- * minus_range_vec
- * mult_range_vec
- * mult_range_vec_signed
- *)
-let add_IVV = arith_op_range_vec integerAdd false 1
-let addS_IVV = arith_op_range_vec integerAdd true 1
-let minus_IVV = arith_op_range_vec integerMinus false 1
-let mult_IVV = arith_op_range_vec integerMult false 2
-let multS_IVV = arith_op_range_vec integerMult true 2
-
-let arith_op_range_vec_range op sign l r = op l (to_num sign r)
-
-(* add_range_vec_range
- * add_range_vec_range_signed
- * minus_range_vec_range
- *)
-let add_IVI x = arith_op_range_vec_range integerAdd false x
-let addS_IVI x = arith_op_range_vec_range integerAdd true x
-let minus_IVI x = arith_op_range_vec_range integerMinus false x
-
-let arith_op_vec_range_range op sign l r = op (to_num sign l) r
-
-(* add_vec_range_range
- * add_vec_range_range_signed
- * minus_vec_range_range
- *)
-let add_VII x = arith_op_vec_range_range integerAdd false x
-let addS_VII x = arith_op_vec_range_range integerAdd true x
-let minus_VII x = arith_op_vec_range_range integerMinus false x
-
-
-
-let arith_op_vec_vec_range op sign l r =
- let (l',r') = (to_num sign l,to_num sign r) in
- op l' r'
-
-(* add_vec_vec_range
- * add_vec_vec_range_signed
- *)
-let add_VVI x = arith_op_vec_vec_range integerAdd false x
-let addS_VVI x = arith_op_vec_vec_range integerAdd true x
-
-let arith_op_vec_bit op sign (size : integer) l r =
- let l' = to_num sign l in
- let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
- to_norm_vec n
-
-(* add_vec_bit
- * add_vec_bit_signed
- * minus_vec_bit_signed
- *)
-let add_VBV x = arith_op_vec_bit integerAdd false 1 x
-let addS_VBV x = arith_op_vec_bit integerAdd true 1 x
-let minus_VBV x = arith_op_vec_bit integerMinus true 1 x
-
-(* TODO: these can't be done directly in Lem because of the one_more size calculation
-val arith_op_overflow_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b * bitU * bool
-let rec arith_op_overflow_vec op sign size (Bitvector _ _ is_inc as l) r =
- let len = bvlength l in
- let act_size = len * size in
- let (l_sign,r_sign) = (to_num sign l,to_num sign r) in
- let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
- let n = op l_sign r_sign in
- let n_unsign = op l_unsign r_unsign in
- let correct_size_num = to_vec_ord is_inc (act_size,n) in
- let one_more_size_u = to_vec_ord is_inc (act_size + 1,n_unsign) in
- let overflow =
- if n <= get_max_representable_in sign len &&
- n >= get_min_representable_in sign len
- then B0 else B1 in
- let c_out = most_significant one_more_size_u in
- (correct_size_num,overflow,c_out)
-
-(* add_overflow_vec
- * add_overflow_vec_signed
- * minus_overflow_vec
- * minus_overflow_vec_signed
- * mult_overflow_vec
- * mult_overflow_vec_signed
- *)
-let addO_VVV = arith_op_overflow_vec integerAdd false 1
-let addSO_VVV = arith_op_overflow_vec integerAdd true 1
-let minusO_VVV = arith_op_overflow_vec integerMinus false 1
-let minusSO_VVV = arith_op_overflow_vec integerMinus true 1
-let multO_VVV = arith_op_overflow_vec integerMult false 2
-let multSO_VVV = arith_op_overflow_vec integerMult true 2
-
-val arith_op_overflow_vec_bit : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer ->
- bitvector 'a -> bitU -> bitvector 'b * bitU * bool
-let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer)
- (Bitvector _ _ is_inc as l) r_bit =
- let act_size = bvlength l * size in
- let l' = to_num sign l in
- let l_u = to_num false l in
- let (n,nu,changed) = match r_bit with
- | B1 -> (op l' 1, op l_u 1, true)
- | B0 -> (l',l_u,false)
- | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
- end in
-(* | _ -> assert false *)
- let correct_size_num = to_vec_ord is_inc (act_size,n) in
- let one_larger = to_vec_ord is_inc (act_size + 1,nu) in
- let overflow =
- if changed
- then
- if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
- then B0 else B1
- else B0 in
- (correct_size_num,overflow,most_significant one_larger)
-
-(* add_overflow_vec_bit_signed
- * minus_overflow_vec_bit
- * minus_overflow_vec_bit_signed
- *)
-let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1
-let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1
-let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1
-*)
-type shift = LL_shift | RR_shift | LLL_shift
-
-let shift_op_vec op (bs, (n : integer)) =
- let n = natFromInteger n in
- match op with
- | LL_shift (*"<<"*) ->
- shiftLeft bs n
- | RR_shift (*">>"*) ->
- shiftRight bs n
- | LLL_shift (*"<<<"*) ->
- rotateLeft n bs
- end
-
-let bitwise_leftshift x = shift_op_vec LL_shift x (*"<<"*)
-let bitwise_rightshift x = shift_op_vec RR_shift x (*">>"*)
-let bitwise_rotate x = shift_op_vec LLL_shift x (*"<<<"*)
-
-let shiftl = bitwise_leftshift
-let shiftr = bitwise_rightshift
-
-let rec arith_op_no0 (op : integer -> integer -> integer) l r =
- if r = 0
- then Nothing
- else Just (op l r)
-(* TODO
-let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Bitvector _ start is_inc) as l) r =
- let act_size = bvlength l * size in
- let (l',r') = (to_num sign l,to_num sign r) in
- let n = arith_op_no0 op l' r' in
- let (representable,n') =
- match n with
- | Just n' ->
- (n' <= get_max_representable_in sign act_size &&
- n' >= get_min_representable_in sign act_size, n')
- | _ -> (false,0)
- end in
- if representable
- then to_vec_ord is_inc (act_size,n')
- else Vector (List.replicate (natFromInteger act_size) BU) start is_inc
-
-let mod_VVV = arith_op_vec_no0 hardware_mod false 1
-let quot_VVV = arith_op_vec_no0 hardware_quot false 1
-let quotS_VVV = arith_op_vec_no0 hardware_quot true 1
-
-let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r =
- let rep_size = length r * size in
- let act_size = length l * size in
- let (l',r') = (to_num sign l,to_num sign r) in
- let (l_u,r_u) = (to_num false l,to_num false r) in
- let n = arith_op_no0 op l' r' in
- let n_u = arith_op_no0 op l_u r_u in
- let (representable,n',n_u') =
- match (n, n_u) with
- | (Just n',Just n_u') ->
- ((n' <= get_max_representable_in sign rep_size &&
- n' >= (get_min_representable_in sign rep_size)), n', n_u')
- | _ -> (true,0,0)
- end in
- let (correct_size_num,one_more) =
- if representable then
- (to_vec_ord is_inc (act_size,n'),to_vec_ord is_inc (act_size + 1,n_u'))
- else
- (Vector (List.replicate (natFromInteger act_size) BU) start is_inc,
- Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in
- let overflow = if representable then B0 else B1 in
- (correct_size_num,overflow,most_significant one_more)
-
-let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1
-let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1
-
-let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r =
- arith_op_vec_no0 op sign size l (to_vec_ord is_inc (length l,r))
-
-let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1
-*)
-
-let duplicate (bit, length) =
- vec_to_bvec (Vector (repeat [bit] length) (length - 1) false)
-
-(* TODO: replace with better native versions *)
-let replicate_bits (v, count) =
- let v = bvec_to_vec true 0 v in
- vec_to_bvec (Vector (repeat (get_elems v) count) ((length v * count) - 1) false)
-
-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')
-
-let lt_vec x = compare_op_vec (<) true x
-let gt_vec x = compare_op_vec (>) true x
-let lteq_vec x = compare_op_vec (<=) true x
-let gteq_vec x = compare_op_vec (>=) true x
-
-let lt_vec_signed x = compare_op_vec (<) true x
-let gt_vec_signed x = compare_op_vec (>) true x
-let lteq_vec_signed x = compare_op_vec (<=) true x
-let gteq_vec_signed x = compare_op_vec (>=) true x
-let lt_vec_unsigned x = compare_op_vec (<) false x
-let gt_vec_unsigned x = compare_op_vec (>) false x
-let lteq_vec_unsigned x = compare_op_vec (<=) false x
-let gteq_vec_unsigned x = compare_op_vec (>=) false x
-
-let lt_svec = lt_vec_signed
-
-let compare_op_vec_range op sign (l,r) =
- compare_op op ((to_num sign l),r)
-
-let lt_vec_range x = compare_op_vec_range (<) true x
-let gt_vec_range x = compare_op_vec_range (>) true x
-let lteq_vec_range x = compare_op_vec_range (<=) true x
-let gteq_vec_range x = compare_op_vec_range (>=) true x
-
-let compare_op_range_vec op sign (l,r) =
- compare_op op (l, (to_num sign r))
-
-let lt_range_vec x = compare_op_range_vec (<) true x
-let gt_range_vec x = compare_op_range_vec (>) true x
-let lteq_range_vec x = compare_op_range_vec (<=) true x
-let gteq_range_vec x = compare_op_range_vec (>=) true x
-
-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. Size 'a => bitvector 'a * bitvector 'a -> bool
-let eq_vec (l,r) = eq (to_num false l, to_num false r)
-let eq_bit (l,r) = eq (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) = 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 (l,r))
-(*let neq_vec_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
-let make_indexed_vector entries default start length dir =
- let length = natFromInteger length in
- Vector (List.foldl replace (replicate length default) entries) start dir
-
-(*
-val make_bit_vector_undef : integer -> vector bitU
-let make_bitvector_undef length =
- Vector (replicate (natFromInteger length) BU) 0 true
- *)
-
-(* let bitwise_not_range_bit n = bitwise_not (to_vec_ord defaultDir n) *)
-
-(* TODO *)
-val mask : forall 'a 'b. Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b
-let mask (start, _, w) = (zeroExtend w)
-
-(* Register operations *)
-
-(*let update_reg_range reg i j reg_val new_val = bvupdate (reg.reg_is_inc) (reg.reg_start) reg_val i j new_val
-let update_reg_pos reg i reg_val bit = bvupdate_pos (reg.reg_is_inc) (reg.reg_start) reg_val i bit
-let update_reg_field_range regfield i j reg_val new_val =
- let current_field_value = regfield.get_field reg_val in
- let new_field_value = bvupdate (regfield.field_is_inc) (regfield.field_start) current_field_value i j new_val in
- regfield.set_field reg_val new_field_value
-(*let write_reg_field_pos regfield i reg_val bit =
- let current_field_value = regfield.get_field reg_val in
- let new_field_value = bvupdate_pos (regfield.field_is_inc) (regfield.field_start) current_field_value i bit in
- regfield.set_field reg_val new_field_value*)*)
+open import Sail_operators
+
+(* Specialisation of operators to machine words *)
+
+val access_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU
+let access_vec_inc = access_bv_inc
+
+val access_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU
+let access_vec_dec = access_bv_dec
+
+val update_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a
+let update_vec_inc = update_bv_inc
+
+val update_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a
+let update_vec_dec = update_bv_dec
+
+val subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
+let subrange_vec_inc = subrange_bv_inc
+
+val subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
+let subrange_vec_dec = subrange_bv_dec
+
+val update_subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a
+let update_subrange_vec_inc = update_subrange_bv_inc
+
+val update_subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a
+let update_subrange_vec_dec = update_subrange_bv_dec
+
+val extz_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
+let extz_vec = extz_bv
+
+val exts_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
+let exts_vec = exts_bv
+
+val concat_vec : forall 'a 'b 'c. Size 'a, Size 'b, Size 'c => mword 'a -> mword 'b -> mword 'c
+let concat_vec = concat_bv
+
+val cons_vec : forall 'a 'b 'c. Size 'a, Size 'b => bitU -> mword 'a -> mword 'b
+let cons_vec = cons_bv
+
+val bool_of_vec : mword ty1 -> bitU
+let bool_of_vec = bool_of_bv
+
+val cast_unit_vec : bitU -> mword ty1
+let cast_unit_vec = cast_unit_bv
+
+val vec_of_bit : forall 'a. Size 'a => integer -> bitU -> mword 'a
+let vec_of_bit = bv_of_bit
+
+val msb : forall 'a. Size 'a => mword 'a -> bitU
+let msb = most_significant
+
+val int_of_vec : forall 'a. Size 'a => bool -> mword 'a -> integer
+let int_of_vec = int_of_bv
+
+val and_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val or_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val xor_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val not_vec : forall 'a. Size 'a => mword 'a -> mword 'a
+let and_vec = and_bv
+let or_vec = or_bv
+let xor_vec = xor_bv
+let not_vec = not_bv
+
+val add_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val addS_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val sub_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val mult_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b
+val multS_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b
+let add_vec = add_bv
+let addS_vec = addS_bv
+let sub_vec = sub_bv
+let mult_vec = mult_bv
+let multS_vec = multS_bv
+
+val add_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val addS_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val sub_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
+val multS_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
+let add_vec_int = add_bv_int
+let addS_vec_int = addS_bv_int
+let sub_vec_int = sub_bv_int
+let mult_vec_int = mult_bv_int
+let multS_vec_int = multS_bv_int
+
+val add_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val addS_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val sub_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
+val multS_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
+let add_int_vec = add_int_bv
+let addS_int_vec = addS_int_bv
+let sub_int_vec = sub_int_bv
+let mult_int_vec = mult_int_bv
+let multS_int_vec = multS_int_bv
+
+val add_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
+val addS_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
+val sub_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
+let add_vec_bit = add_bv_bit
+let addS_vec_bit = addS_bv_bit
+let sub_vec_bit = sub_bv_bit
+
+val add_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+val add_overflow_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+val sub_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+val sub_overflow_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+val mult_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+val mult_overflow_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+let add_overflow_vec = add_overflow_bv
+let add_overflow_vec_signed = add_overflow_bv_signed
+let sub_overflow_vec = sub_overflow_bv
+let sub_overflow_vec_signed = sub_overflow_bv_signed
+let mult_overflow_vec = mult_overflow_bv
+let mult_overflow_vec_signed = mult_overflow_bv_signed
+
+val add_overflow_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+val add_overflow_vec_bit_signed : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+val sub_overflow_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+val sub_overflow_vec_bit_signed : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+let add_overflow_vec_bit = add_overflow_bv_bit
+let add_overflow_vec_bit_signed = add_overflow_bv_bit_signed
+let sub_overflow_vec_bit = sub_overflow_bv_bit
+let sub_overflow_vec_bit_signed = sub_overflow_bv_bit_signed
+
+val shiftl : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val rotl : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val rotr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+let shiftl = shiftl_bv
+let shiftr = shiftr_bv
+let rotl = rotl_bv
+let rotr = rotr_bv
+
+val mod_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val quot_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val quot_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+let mod_vec = mod_bv
+let quot_vec = quot_bv
+let quot_vec_signed = quot_bv_signed
+
+val mod_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val quot_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+let mod_vec_int = mod_bv_int
+let quot_vec_int = quot_bv_int
+
+val replicate_bits : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
+let replicate_bits = replicate_bits_bv
+
+val duplicate : forall 'a. Size 'a => bitU -> integer -> mword 'a
+let duplicate = duplicate_bit_bv
+
+val eq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val neq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val ult_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val slt_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val ugt_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val sgt_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val ulteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val slteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val ugteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val sgteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+let eq_vec = eq_bv
+let neq_vec = neq_bv
+let ult_vec = ult_bv
+let slt_vec = slt_bv
+let ugt_vec = ugt_bv
+let sgt_vec = sgt_bv
+let ulteq_vec = ulteq_bv
+let slteq_vec = slteq_bv
+let ugteq_vec = ugteq_bv
+let sgteq_vec = sgteq_bv
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 8aee556d..92ef7037 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -13,6 +13,17 @@ let pow m n = m ** (natFromInteger n)
let pow2 n = pow 2 n
+let inline lt = (<)
+let inline gt = (>)
+let inline lteq = (<=)
+let inline gteq = (>=)
+
+val eq : forall 'a. Eq 'a => 'a -> 'a -> bool
+let inline eq l r = (l = r)
+
+val neq : forall 'a. Eq 'a => 'a -> 'a -> bool
+let inline neq l r = (l <> r)
+
(*let add_int l r = integerAdd l r
let add_signed l r = integerAdd l r
let sub_int l r = integerMinus l r
@@ -58,6 +69,35 @@ let rec replace bs (n : integer) b' = match bs with
let upper n = n
+let hardware_mod (a: integer) (b:integer) : integer =
+ if a < 0 && b < 0
+ then (abs a) mod (abs b)
+ else if (a < 0 && b >= 0)
+ then (a mod b) - b
+ else a mod b
+
+(* There are different possible answers for integer divide regarding
+rounding behaviour on negative operands. Positive operands always
+round down so derive the one we want (trucation towards zero) from
+that *)
+let hardware_quot (a:integer) (b:integer) : integer =
+ let q = (abs a) / (abs b) in
+ if ((a<0) = (b<0)) then
+ q (* same sign -- result positive *)
+ else
+ ~q (* different sign -- result negative *)
+
+let max_64u = (integerPow 2 64) - 1
+let max_64 = (integerPow 2 63) - 1
+let min_64 = 0 - (integerPow 2 63)
+let max_32u = (4294967295 : integer)
+let max_32 = (2147483647 : integer)
+let min_32 = (0 - 2147483648 : integer)
+let max_8 = (127 : integer)
+let min_8 = (0 - 128 : integer)
+let max_5 = (31 : integer)
+let min_5 = (0 - 32 : integer)
+
(*** Bits *)
type bitU = B0 | B1 | BU
@@ -83,7 +123,7 @@ end
let bool_of_bitU = function
| B0 -> false
- | B1 -> true
+ | B1 -> true
| BU -> failwith "bool_of_bitU applied to BU"
end
@@ -272,34 +312,34 @@ let show_bitlist bs =
let inline (^^) = append_list
-val slice_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a
-let slice_list_inc xs i j =
+val subrange_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a
+let subrange_list_inc xs i j =
let (toJ,_suffix) = List.splitAt (natFromInteger j + 1) xs in
let (_prefix,fromItoJ) = List.splitAt (natFromInteger i) toJ in
fromItoJ
-val slice_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a
-let slice_list_dec xs i j =
+val subrange_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a
+let subrange_list_dec xs i j =
let top = (length_list xs) - 1 in
- slice_list_inc xs (top - i) (top - j)
+ subrange_list_inc xs (top - i) (top - j)
-val slice_list : forall 'a. bool -> list 'a -> integer -> integer -> list 'a
-let slice_list is_inc xs i j = if is_inc then slice_list_inc xs i j else slice_list_dec xs i j
+val subrange_list : forall 'a. bool -> list 'a -> integer -> integer -> list 'a
+let subrange_list is_inc xs i j = if is_inc then subrange_list_inc xs i j else subrange_list_dec xs i j
-val update_slice_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a
-let update_slice_list_inc xs i j xs' =
+val update_subrange_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a
+let update_subrange_list_inc xs i j xs' =
let (toJ,suffix) = List.splitAt (natFromInteger j + 1) xs in
let (prefix,_fromItoJ) = List.splitAt (natFromInteger i) toJ in
prefix ++ xs' ++ suffix
-val update_slice_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a
-let update_slice_list_dec xs i j xs' =
+val update_subrange_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a
+let update_subrange_list_dec xs i j xs' =
let top = (length_list xs) - 1 in
- update_slice_list_inc xs (top - i) (top - j) xs'
+ update_subrange_list_inc xs (top - i) (top - j) xs'
-val update_slice_list : forall 'a. bool -> list 'a -> integer -> integer -> list 'a -> list 'a
-let update_slice_list is_inc xs i j xs' =
- if is_inc then update_slice_list_inc xs i j xs' else update_slice_list_dec xs i j xs'
+val update_subrange_list : forall 'a. bool -> list 'a -> integer -> integer -> list 'a -> list 'a
+let update_subrange_list is_inc xs i j xs' =
+ if is_inc then update_subrange_list_inc xs i j xs' else update_subrange_list_dec xs i j xs'
val access_list_inc : forall 'a. list 'a -> integer -> 'a
let access_list_inc xs n = List_extra.nth xs (natFromInteger n)
@@ -383,11 +423,28 @@ val update_mword : forall 'a. bool -> mword 'a -> integer -> bitU -> mword 'a
let update_mword is_inc w n b =
if is_inc then update_mword_inc w n b else update_mword_dec w n b
+val mword_of_int : forall 'a. Size 'a => integer -> integer -> mword 'a
+let mword_of_int len n =
+ let w = wordFromInteger n in
+ if (length_mword w = len) then w else failwith "unexpected word length"
+
+(* Translating between a type level number (itself 'n) and an integer *)
+
+let size_itself_int x = integerFromNat (size_itself x)
+
+(* NB: the corresponding sail type is forall 'n. atom('n) -> itself('n),
+ the actual integer is ignored. *)
+
+val make_the_value : forall 'n. integer -> itself 'n
+let inline make_the_value x = the_value
+
(*** Bitvectors *)
class (Bitvector 'a)
val bits_of : 'a -> list bitU
val of_bits : list bitU -> 'a
+ (* The first parameter specifies the desired length of the bitvector *)
+ val of_int : integer -> integer -> 'a
val length : 'a -> integer
val unsigned : 'a -> integer
val signed : 'a -> integer
@@ -401,44 +458,46 @@ end
instance forall 'a. BitU 'a => (Bitvector (list 'a))
let bits_of v = List.map to_bitU v
let of_bits v = List.map of_bitU v
- let length v = length_list v
+ let of_int len n = List.map of_bitU (bits_of_int len n)
+ let length = length_list
let unsigned v = unsigned_of_bits (List.map to_bitU v)
let signed v = signed_of_bits (List.map to_bitU v)
let get_bit is_inc v n = to_bitU (access_list is_inc v n)
let set_bit is_inc v n b = update_list is_inc v n (of_bitU b)
- let get_bits is_inc v i j = List.map to_bitU (slice_list is_inc v i j)
- let set_bits is_inc v i j v' = update_slice_list is_inc v i j (List.map of_bitU v')
+ let get_bits is_inc v i j = List.map to_bitU (subrange_list is_inc v i j)
+ let set_bits is_inc v i j v' = update_subrange_list is_inc v i j (List.map of_bitU v')
end
instance forall 'a. Size 'a => (Bitvector (mword 'a))
let bits_of v = List.map to_bitU (bitlistFromWord v)
let of_bits v = wordFromBitlist (List.map of_bitU v)
+ let of_int = mword_of_int
let length v = integerFromNat (word_length v)
- let unsigned v = unsignedIntegerFromWord v
- let signed v = signedIntegerFromWord v
+ let unsigned = unsignedIntegerFromWord
+ let signed = signedIntegerFromWord
let get_bit = access_mword
let set_bit = update_mword
let get_bits is_inc v i j = get_bits is_inc (bitlistFromWord v) i j
let set_bits is_inc v i j v' = wordFromBitlist (set_bits is_inc (bitlistFromWord v) i j v')
end
-let access_vec_inc v n = get_bit true v n
-let access_vec_dec v n = get_bit false v n
+let access_bv_inc v n = get_bit true v n
+let access_bv_dec v n = get_bit false v n
-let update_vec_inc v n b = set_bit true v n b
-let update_vec_dec v n b = set_bit false v n b
+let update_bv_inc v n b = set_bit true v n b
+let update_bv_dec v n b = set_bit false v n b
-let subrange_vec_inc v i j = of_bits (get_bits true v i j)
-let subrange_vec_dec v i j = of_bits (get_bits false v i j)
+let subrange_bv_inc v i j = of_bits (get_bits true v i j)
+let subrange_bv_dec v i j = of_bits (get_bits false v i j)
-let update_subrange_vec_inc v i j v' = set_bits true v i j (bits_of v')
-let update_subrange_vec_dec v i j v' = set_bits false v i j (bits_of v')
+let update_subrange_bv_inc v i j v' = set_bits true v i j (bits_of v')
+let update_subrange_bv_dec v i j v' = set_bits false v i j (bits_of v')
-val extz_vec : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b
-let extz_vec n v = of_bits (extz_bits n (bits_of v))
+val extz_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b
+let extz_bv n v = of_bits (extz_bits n (bits_of v))
-val exts_vec : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b
-let exts_vec n v = of_bits (exts_bits n (bits_of v))
+val exts_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b
+let exts_bv n v = of_bits (exts_bits n (bits_of v))
(*** Bytes and addresses *)
@@ -584,13 +643,13 @@ let rec external_reg_value reg_name v =
match reg_name with
| Reg _ start size dir ->
(start, (if dir = D_increasing then start else (start - (size +1))), dir)
- | Reg_slice _ reg_start dir (slice_start, slice_end) ->
+ | Reg_slice _ reg_start dir (slice_start, _) ->
((if dir = D_increasing then slice_start else (reg_start - slice_start)),
slice_start, dir)
- | Reg_field _ reg_start dir _ (slice_start, slice_end) ->
+ | Reg_field _ reg_start dir _ (slice_start, _) ->
((if dir = D_increasing then slice_start else (reg_start - slice_start)),
slice_start, dir)
- | Reg_f_slice _ reg_start dir _ _ (slice_start, slice_end) ->
+ | Reg_f_slice _ reg_start dir _ _ (slice_start, _) ->
((if dir = D_increasing then slice_start else (reg_start - slice_start)),
slice_start, dir)
end in
diff --git a/src/gen_lib/state_bitlists.lem b/src/gen_lib/state_bitlists.lem
new file mode 100644
index 00000000..f1aaa7dc
--- /dev/null
+++ b/src/gen_lib/state_bitlists.lem
@@ -0,0 +1,29 @@
+open import Pervasives_extra
+open import Sail_impl_base
+open import Sail_values
+open import Sail_operators
+open import State
+
+val write_reg : forall 'regs 'a. register_ref 'regs 'a -> 'a -> M 'regs unit
+let write_reg reg v state =
+ [(Left (), <| state with regstate = reg.write_to state.regstate v |>)]
+val update_reg : forall 'regs 'a 'b. register_ref 'regs 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit
+let update_reg reg f v state =
+ let current_value = get_reg state reg in
+ let new_value = f current_value v in
+ [(Left (), set_reg state reg new_value)]
+let write_reg_range reg i j = update_reg reg (update_reg_range i j)
+let write_reg_pos reg i = update_reg reg (update_reg_pos i)
+let write_reg_field reg regfield = update_reg reg regfield.set_field
+let write_reg_field_range reg regfield i j =
+ let upd regval v =
+ let current_field_value = regfield.get_field regval in
+ let new_field_value = update current_field_value i j v in
+ regfield.set_field regval new_field_value in
+ update_reg reg upd
+let write_reg_field_pos reg regfield i =
+ let upd regval v =
+ let current_field_value = regfield.get_field regval in
+ let new_field_value = update_pos current_field_value i v in
+ regfield.set_field regval new_field_value in
+ update_reg reg upd
diff --git a/src/process_file.ml b/src/process_file.ml
index 9ff208ca..1da893c3 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -232,7 +232,10 @@ let output_lem filename libs defs =
if !Pretty_print_lem.opt_sequential
then ["State_monad"; "State"]
else ["Prompt_monad"; "Prompt"] in
- let operators_module = "Sail_operators" (* if !Pretty_print_lem.opt_mwords then "Sail_operators_mwords" else "Sail_operators" *) in
+ let operators_module =
+ if !Pretty_print_lem.opt_mwords
+ then "Sail_operators_mwords"
+ else "Sail_operators_bitlists" in
let libs = List.map (fun lib -> lib ^ seq_suffix) libs in
let base_imports = [
"Pervasives_extra";
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:38:02 +0000