diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/power_extras.lem | 11 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 40 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 34 | ||||
| -rw-r--r-- | src/gen_lib/vector.lem | 24 |
4 files changed, 78 insertions, 31 deletions
diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem index f2941aff..8515a406 100644 --- a/src/gen_lib/power_extras.lem +++ b/src/gen_lib/power_extras.lem @@ -1,4 +1,5 @@ open import Pervasives +open import Vector open import State open import Sail_values @@ -33,3 +34,13 @@ let H_Sync () = return () let LW_Sync () = return () let EIEIO_Sync () = return () +let recalculate_dependency () = return () + +let trap () = () +(* this needs to change, but for that we'd have to make the type checker know about trap + * as an effect *) + +val countLeadingZeroes : vector bit * integer -> integer +let countLeadingZeroes (V bits _ _ ,n) = + let (_,bits) = List.splitAt (natFromInteger n) bits in + integerFromNat (List.length (takeWhile ((=) O) bits)) diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index b02e47cb..481a4e5b 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -25,6 +25,10 @@ let (~) = bitwise_not_bit let bitwise_not (V bs start is_inc) = V (List.map bitwise_not_bit bs) start is_inc +val is_one : integer -> bit +let is_one i = + if i = 1 then I else O + let bool_to_bit b = if b then I else O let bitwise_binop_bit op = function @@ -106,15 +110,15 @@ let rec divide_by_2 bs (i : integer) (n : integer) = then bs else if (n mod 2 = 1) - then divide_by_2 (replace bs (natFromInteger i,I)) (i - 1) (n / 2) + then divide_by_2 (replace bs (i,I)) (i - 1) (n / 2) else divide_by_2 bs (i-1) (n div 2) let rec add_one_bit bs co (i : integer) = if i < 0 then bs else match (nth bs i,co) with - | (O,false) -> replace bs (natFromInteger i,I) - | (O,true) -> add_one_bit (replace bs (natFromInteger i,I)) true (i-1) - | (I,false) -> add_one_bit (replace bs (natFromInteger i,O)) true (i-1) + | (O,false) -> replace bs (i,I) + | (O,true) -> add_one_bit (replace bs (i,I)) true (i-1) + | (I,false) -> add_one_bit (replace bs (i,O)) true (i-1) | (I,true) -> add_one_bit bs true (i-1) | _ -> failwith "add_one_bit applied to list with undefined bit" (* | Vundef,_ -> assert false*) @@ -218,6 +222,8 @@ let add_VII = arith_op_vec_range_range integerAdd false let addS_VII = arith_op_vec_range_range integerAdd true let minus_VII = arith_op_vec_range_range integerMinus false + + 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' @@ -270,7 +276,7 @@ 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 - + let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer) (V _ _ is_inc as l) r_bit = let act_size = length l * size in @@ -373,7 +379,7 @@ let arith_op_overflow_no0_vec op sign size (((V _ start is_inc) as l),r) = let quotO_VVV = arith_op_overflow_no0_vec integerDiv false 1 let quotSO_VVV = arith_op_overflow_no0_vec integerDiv true 1 -let arith_op_vec_range_no0 op sign size ((V _ _ is_inc as l),r) = +let arith_op_vec_range_no0 op sign size (V _ _ is_inc as l) r = arith_op_vec_no0 op sign size (l,to_vec is_inc (length l,r)) let mod_VIV = arith_op_vec_range_no0 integerMod false 1 @@ -438,3 +444,25 @@ let EXTS (v1,(V _ _ is_inc as v)) = to_vec is_inc (v1,signed v) let EXTZ = EXTS + +val make_indexed_vector_reg : list (integer * register) -> maybe register -> integer -> integer -> + vector register +let make_indexed_vector_reg entries default start length = + let length = natFromInteger length in + match default with + | Just v -> V (List.foldl replace (replicate length v) entries) start defaultDir + | Nothing -> failwith "make_indexed_vector used without default value" + end + +val make_indexed_vector_bit : list (integer * bit) -> maybe bit -> integer -> integer -> vector bit +let make_indexed_vector_bit entries default start length = + let length = natFromInteger length in + let default = match default with Nothing -> Undef | Just v -> v end in + V (List.foldl replace (replicate length default) entries) start defaultDir + +val make_bit_vector_undef : integer -> vector bit +let make_bitvector_undef length = + V (replicate (natFromInteger length) Undef) 0 true + + +let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 7777cf5e..f79f8eff 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -128,8 +128,8 @@ let rec foreach_dec (i,stop,by) vars body = else ((),vars) -val foreachM_inc : forall 's 'e 'vars. (nat * nat * nat) -> 'vars -> - (nat -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars) +val foreachM_inc : forall 's 'e 'vars. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars) let rec foreachM_inc (i,stop,by) vars body = if i <= stop then @@ -138,8 +138,8 @@ let rec foreachM_inc (i,stop,by) vars body = else return ((),vars) -val foreachM_dec : forall 's 'e 'vars. (nat * nat * nat) -> 'vars -> - (nat -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars) +val foreachM_dec : forall 's 'e 'vars. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars) let rec foreachM_dec (i,stop,by) vars body = if i >= stop then @@ -153,11 +153,24 @@ let read_reg_field reg rfield = uncurry (read_reg_range reg) (field_indices rfie val write_reg_field : forall 'e. register -> register_field -> vector bit -> M state 'e unit let write_reg_field reg rfield = uncurry (write_reg_range reg) (field_indices rfield) -val read_reg_field_bit : forall 'e. register -> register_field_bit -> M state 'e bit -let read_reg_field_bit reg rbit = read_reg_bit reg (field_index_bit rbit) +val read_reg_bitfield : forall 'e. register -> register_bitfield -> M state 'e bit +let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit) + +val write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> M state 'e unit +let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit) + +val write_reg_field_range : forall 'e. register -> register_field -> integer -> integer -> + vector bit -> M state 'e unit +let write_reg_field_range reg rfield i j v = + let (i',j') = field_indices rfield in + write_reg_range reg i' j' v + +val write_reg_field_bit : forall 'e. register -> register_field -> integer -> + bit -> M state 'e unit +let write_reg_field_bit reg rfield i v = + let (i',_) = field_indices rfield in + write_reg_bit reg (i + i') v -val write_reg_field_bit : forall 'e. register -> register_field_bit -> bit -> M state 'e unit -let write_reg_field_bit reg rbit = write_reg_bit reg (field_index_bit rbit) let length l = integerFromNat (length l) @@ -172,3 +185,8 @@ let write_two_regs r1 r2 vec = (if defaultDir then size - start else start - size) (if defaultDir then vsize - start else start - vsize) in write_reg r1 r1_v >> write_reg r2 r2_v + +let read_two_regs r1 r2 = + read_reg r1 >>= fun v1 -> + read_reg r2 >>= fun v2 -> + return (v1 ^^ v2) diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem index ad0ba1db..4044e23c 100644 --- a/src/gen_lib/vector.lem +++ b/src/gen_lib/vector.lem @@ -18,25 +18,15 @@ let to_bool = function let get_start (V _ s _) = s let length (V bs _ _) = length bs -let rec replace bs ((n : nat),b') = match (n,bs) with - | (_, []) -> [] - | (0, _::bs) -> b' :: bs - | (n+1, b::bs) -> b :: replace bs (n,b') +let rec replace bs ((n : integer),b') = match bs with + | [] -> [] + | b :: bs -> + if n = 0 then + b' :: bs + else + b :: replace bs (n - 1,b') end -let make_indexed_vector_reg entries default start length = - match default with - | Just v -> V (List.foldl replace (replicate length v) entries) start - | Nothing -> failwith "make_indexed_vector used without default value" - end - -let make_indexed_vector_bit entries default start length = - let default = match default with Nothing -> Undef | Just v -> v end in - V (List.foldl replace (replicate length default) entries) start - -let make_bitvector_undef length = - V (replicate length Undef) 0 true - let vector_concat (V bs start is_inc) (V bs' _ _) = V (bs ++ bs') start is_inc |