diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_operators_bitlists.lem | 177 | ||||
| -rw-r--r-- | src/gen_lib/state_bitlists.lem | 29 |
2 files changed, 177 insertions, 29 deletions
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem new file mode 100644 index 00000000..af683780 --- /dev/null +++ b/src/gen_lib/sail_operators_bitlists.lem @@ -0,0 +1,177 @@ +open import Pervasives_extra +open import Machine_word +open import Sail_impl_base +open import Sail_values +open import Sail_operators + +(* Specialisation of operators to bit lists *) + +val access_vec_inc : list bitU -> integer -> bitU +let access_vec_inc = access_bv_inc + +val access_vec_dec : list bitU -> integer -> bitU +let access_vec_dec = access_bv_dec + +val update_vec_inc : list bitU -> integer -> bitU -> list bitU +let update_vec_inc = update_bv_inc + +val update_vec_dec : list bitU -> integer -> bitU -> list bitU +let update_vec_dec = update_bv_dec + +val subrange_vec_inc : list bitU -> integer -> integer -> list bitU +let subrange_vec_inc = subrange_bv_inc + +val subrange_vec_dec : list bitU -> integer -> integer -> list bitU +let subrange_vec_dec = subrange_bv_dec + +val update_subrange_vec_inc : list bitU -> integer -> integer -> list bitU -> list bitU +let update_subrange_vec_inc = update_subrange_bv_inc + +val update_subrange_vec_dec : list bitU -> integer -> integer -> list bitU -> list bitU +let update_subrange_vec_dec = update_subrange_bv_dec + +val extz_vec : integer -> list bitU -> list bitU +let extz_vec = extz_bv + +val exts_vec : integer -> list bitU -> list bitU +let exts_vec = exts_bv + +val concat_vec : list bitU -> list bitU -> list bitU +let concat_vec = concat_bv + +val cons_vec : bitU -> list bitU -> list bitU +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 : integer -> bitU -> list bitU +let vec_of_bit = bv_of_bit + +val msb : list bitU -> bitU +let msb = most_significant + +val int_of_vec : bool -> list bitU -> integer +let int_of_vec = int_of_bv + +val and_vec : list bitU -> list bitU -> list bitU +val or_vec : list bitU -> list bitU -> list bitU +val xor_vec : list bitU -> list bitU -> list bitU +val not_vec : list bitU -> list bitU +let and_vec = and_bv +let or_vec = or_bv +let xor_vec = xor_bv +let not_vec = not_bv + +val add_vec : list bitU -> list bitU -> list bitU +val addS_vec : list bitU -> list bitU -> list bitU +val sub_vec : list bitU -> list bitU -> list bitU +val mult_vec : list bitU -> list bitU -> list bitU +val multS_vec : list bitU -> list bitU -> list bitU +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 : list bitU -> integer -> list bitU +val addS_vec_int : list bitU -> integer -> list bitU +val sub_vec_int : list bitU -> integer -> list bitU +val mult_vec_int : list bitU -> integer -> list bitU +val multS_vec_int : list bitU -> integer -> list bitU +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 : integer -> list bitU -> list bitU +val addS_int_vec : integer -> list bitU -> list bitU +val sub_int_vec : integer -> list bitU -> list bitU +val mult_int_vec : integer -> list bitU -> list bitU +val multS_int_vec : integer -> list bitU -> list bitU +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 : list bitU -> bitU -> list bitU +val addS_vec_bit : list bitU -> bitU -> list bitU +val sub_vec_bit : list bitU -> bitU -> list bitU +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 : list bitU -> list bitU -> (list bitU * bitU * bitU) +val add_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU) +val sub_overflow_vec : list bitU -> list bitU -> (list bitU * bitU * bitU) +val sub_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU) +val mult_overflow_vec : list bitU -> list bitU -> (list bitU * bitU * bitU) +val mult_overflow_vec_signed : list bitU -> list bitU -> (list bitU * 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 : list bitU -> bitU -> (list bitU * bitU * bitU) +val add_overflow_vec_bit_signed : list bitU -> bitU -> (list bitU * bitU * bitU) +val sub_overflow_vec_bit : list bitU -> bitU -> (list bitU * bitU * bitU) +val sub_overflow_vec_bit_signed : list bitU -> bitU -> (list bitU * 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 : list bitU -> integer -> list bitU +val shiftr : list bitU -> integer -> list bitU +val rotl : list bitU -> integer -> list bitU +val rotr : list bitU -> integer -> list bitU +let shiftl = shiftl_bv +let shiftr = shiftr_bv +let rotl = rotl_bv +let rotr = rotr_bv + +val mod_vec : list bitU -> list bitU -> list bitU +val quot_vec : list bitU -> list bitU -> list bitU +val quot_vec_signed : list bitU -> list bitU -> list bitU +let mod_vec = mod_bv +let quot_vec = quot_bv +let quot_vec_signed = quot_bv_signed + +val mod_vec_int : list bitU -> integer -> list bitU +val quot_vec_int : list bitU -> integer -> list bitU +let mod_vec_int = mod_bv_int +let quot_vec_int = quot_bv_int + +val replicate_bits : list bitU -> integer -> list bitU +let replicate_bits = replicate_bits_bv + +val duplicate : bitU -> integer -> list bitU +let duplicate = duplicate_bit_bv + +val eq_vec : list bitU -> list bitU -> bool +val neq_vec : list bitU -> list bitU -> bool +val ult_vec : list bitU -> list bitU -> bool +val slt_vec : list bitU -> list bitU -> bool +val ugt_vec : list bitU -> list bitU -> bool +val sgt_vec : list bitU -> list bitU -> bool +val ulteq_vec : list bitU -> list bitU -> bool +val slteq_vec : list bitU -> list bitU -> bool +val ugteq_vec : list bitU -> list bitU -> bool +val sgteq_vec : list bitU -> list bitU -> 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/state_bitlists.lem b/src/gen_lib/state_bitlists.lem deleted file mode 100644 index f1aaa7dc..00000000 --- a/src/gen_lib/state_bitlists.lem +++ /dev/null @@ -1,29 +0,0 @@ -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 |