diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_values.lem | 59 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 1 | ||||
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 6 | ||||
| -rw-r--r-- | src/pretty_print.ml | 7 |
4 files changed, 71 insertions, 2 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index ec67edb8..975c7a5e 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -50,6 +50,12 @@ let bitU_of_bit = function | Bitc_one -> I end +let bit_of_bitU = function + | O -> Bitc_zero + | I -> Bitc_one + | Undef -> failwith "bit_of_bitU: Undef" + end + let bitU_of_bit_lifted = function | Bitl_zero -> O | Bitl_one -> I @@ -683,6 +689,11 @@ let byte_lifteds_of_bitv (Vector bits length is_inc) = let bits = List.map bit_lifted_of_bitU bits in byte_lifteds_of_bit_lifteds bits +val bytes_of_bitv : vector bitU -> list byte +let bytes_of_bitv (Vector bits length is_inc) = + let bits = List.map bit_of_bitU bits in + bytes_of_bits bits + val bit_lifteds_of_bitUs : list bitU -> list bit_lifted let bit_lifteds_of_bitUs bits = List.map bit_lifted_of_bitU bits @@ -700,6 +711,11 @@ let address_lifted_of_bitv v = end in Address_lifted byte_lifteds maybe_address_integer +val address_of_bitv : vector bitU -> address +let address_of_bitv v = + let bytes = bytes_of_bitv v in + address_of_byte_list bytes + (*** Registers *) @@ -1381,3 +1397,46 @@ instance (ToFromInterpValue instruction_kind) let toInterpValue = instruction_kindToInterpValue let fromInterpValue = instruction_kindFromInterpValue end + + +let regfpToInterpValue = function + | RFull v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) + | RSlice v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) + | RSliceBit v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) + | RField v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RField") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) + end + +let rec regfpFromInterpValue v = match v with + | SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") _) _ _ v -> RFull (fromInterpValue v) + | SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") _) _ _ v -> RSlice (fromInterpValue v) + | SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") _) _ _ v -> RSliceBit (fromInterpValue v) + | SI.V_ctor (SIA.Id_aux (SIA.Id "RField") _) _ _ v -> RField (fromInterpValue v) + | SI.V_tuple [v] -> regfpFromInterpValue v + | v -> failwith ("fromInterpValue regfp: unexpected value. " ^ Interp.debug_print_value v) + end + +instance (ToFromInterpValue regfp) + let toInterpValue = regfpToInterpValue + let fromInterpValue = regfpFromInterpValue +end + +(* +let rfp_to_reg reg_info direction = function + | RFull name -> + let (start,length,direction,_) = reg_info name Nothing in + Reg name start length direction + | RSlice (name,i,j) -> + let (start,length,direction,_) = reg_info name Nothing in + let slice = extern_slice direction (natFromInteger start) (i,j) in + Reg_slice name start direction slice + | RSliceBit (name,i) -> + let (start,length,direction,_) = reg_info name Nothing in + let slice = extern_slice direction (natFromInteger start) (i,i) in + Reg_slice name start direction slice + | RField (name,field_name) -> + let (start,length,direction,span) = reg_info name (Just field_name) in + let start = natFromInteger start in + let slice = extern_slice direction start (start,span) in + Reg_field name start direction field_name slice +end + *) diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index a648b437..ea3ba154 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -203,3 +203,4 @@ val instruction_analysis : val initial_outcome_s_of_instruction : context -> interp_mode -> instruction -> Sail_impl_base.outcome_s instruction_state unit + diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 13a2dd38..86778bee 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -1400,3 +1400,9 @@ instance (Eq decode_error) let (<>) = decode_error_inequal end +type regfp = + | RFull of (string) + | RSlice of (string * integer * integer) + | RSliceBit of (string * integer) + | RField of (string * string) + diff --git a/src/pretty_print.ml b/src/pretty_print.ml index a4069caf..1ad4c632 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -2649,9 +2649,9 @@ let doc_exp_lem, doc_let_lem = | "add" -> aux "+" | "minus" -> aux "-" | "multiply" -> aux "*" - | "quot" -> aux "/" - | "modulo" -> aux "mod" + | "quot" -> aux2 "quot" + | "modulo" -> aux2 "modulo" | "add_vec" -> aux2 "add_VVV" | "add_vec_signed" -> aux2 "addS_VVV" | "add_overflow_vec" -> aux2 "addO_VVV" @@ -2790,6 +2790,9 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with | Id_aux ((Id "write_kind"),_) -> empty | Id_aux ((Id "barrier_kind"),_) -> empty | Id_aux ((Id "instruction_kind"),_) -> empty + | Id_aux ((Id "regfp"),_) -> empty + (* | Id_aux ((Id "nia"),_) -> empty + | Id_aux ((Id "dia"),_) -> empty *) | _ -> let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in let typ_pp = |