summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp.lem45
-rw-r--r--src/lem_interp/interp_inter_imp.lem34
-rw-r--r--src/lem_interp/interp_interface.lem4
-rw-r--r--src/lem_interp/sail_impl_base.lem42
4 files changed, 61 insertions, 64 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 95927318..4f5fb479 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -14,51 +14,6 @@ open import Instruction_extractor
type tannot = Interp_utilities.tannot
-type decode_error =
- | Unsupported_instruction_error of instruction
- | Not_an_instruction_error of opcode
- | Internal_error of string
-
-
-let decode_error_compare e1 e2 =
- match (e1, e2) with
- | (Unsupported_instruction_error i1, Unsupported_instruction_error i2)
- -> defaultCompare i1 i2
- | (Unsupported_instruction_error _, _) -> LT
- | (_, Unsupported_instruction_error _) -> GT
-
- | (Not_an_instruction_error o1, Not_an_instruction_error o2) -> defaultCompare o1 o2
- | (Not_an_instruction_error _, _) -> LT
- | (_, Not_an_instruction_error _) -> GT
-
- | (Internal_error s1, Internal_error s2) -> compare s1 s2
- (* | (Internal_error _, _) -> LT *)
- (* | (_, Internal_error _) -> GT *)
- end
-
-let decode_error_less e1 e2 = decode_error_compare e1 e2 = LT
-let decode_error_less_eq e1 e2 = decode_error_compare e1 e2 <> GT
-let decode_error_greater e1 e2 = decode_error_compare e1 e2 = GT
-let decode_error_greater_eq e1 e2 = decode_error_compare e1 e2 <> LT
-
-instance (Ord decode_error)
- let compare = decode_error_compare
- let (<) = decode_error_less
- let (<=) = decode_error_less_eq
- let (>) = decode_error_greater
- let (>=) = decode_error_greater_eq
-end
-
-let decode_error_equal e1 e2 = (decode_error_compare e1 e2) = EQ
-let decode_error_inequal e1 e2 = not (decode_error_equal e1 e2)
-
-instance (Eq decode_error)
- let (=) = decode_error_equal
- let (<>) = decode_error_inequal
-end
-
-
-
val debug_print : string -> unit
declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index cd229125..857a81a3 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -307,7 +307,7 @@ type interp_value_helper_mode = Ivh_translate | Ivh_decode | Ivh_unsupported | I
type interp_value_return =
| Ivh_value of Interp.value
| Ivh_value_after_exn of Interp.value
- | Ivh_error of Interp.decode_error
+ | Ivh_error of decode_error
let rec interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen thunk =
let errk_str = match ivh_mode with
@@ -331,18 +331,18 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
| Interp.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Ivh_value vinstr,events_out)
| Interp.V_ctor (Id_aux (Id "None") _) _ _ _ ->
(match (ivh_mode,arg) with
- | (Ivh_decode, (Just arg)) -> (Ivh_error (Interp.Not_an_instruction_error arg), events_out)
- | (Ivh_illegal, (Just arg)) -> (Ivh_error (Interp.Not_an_instruction_error arg), events_out)
- | (Ivh_unsupported, _) -> (Ivh_error (Interp.Unsupported_instruction_error instr), events_out)
+ | (Ivh_decode, (Just arg)) -> (Ivh_error (Sail_impl_base.Not_an_instruction_error arg), events_out)
+ | (Ivh_illegal, (Just arg)) -> (Ivh_error (Sail_impl_base.Not_an_instruction_error arg), events_out)
+ | (Ivh_unsupported, _) -> (Ivh_error (Sail_impl_base.Unsupported_instruction_error instr), events_out)
| _ -> Assert_extra.failwith "Reached unreachable pattern" end)
- | _ -> (Ivh_error (Interp.Internal_error ("Value not an option for " ^ errk_str)), events_out) end) end)
- | (Interp.Error l msg,_,_) -> (Ivh_error (Interp.Internal_error msg), events_out)
+ | _ -> (Ivh_error (Sail_impl_base.Internal_error ("Value not an option for " ^ errk_str)), events_out) end) end)
+ | (Interp.Error l msg,_,_) -> (Ivh_error (Sail_impl_base.Internal_error msg), events_out)
| (Interp.Action (Interp.Return value) stack,_,_) ->
interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen
(fun _ -> Interp.resume mode stack (Just value))
| (Interp.Action (Interp.Call_extern i value) stack,_,_) ->
match List.lookup i (Interp_lib.library_functions direction) with
- | Nothing -> (Ivh_error (Interp.Internal_error ("External function not available " ^ i)), events_out)
+ | Nothing -> (Ivh_error (Sail_impl_base.Internal_error ("External function not available " ^ i)), events_out)
| Just f ->
interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen
(fun _ -> Interp.resume mode stack (Just (f value)))
@@ -350,8 +350,8 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
| (Interp.Action (Interp.Fail v) stack, _, _) ->
match (Interp.detaint v) with
| Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_string s) _)) ->
- (Ivh_error (Interp.Internal_error ("Assert failed: " ^ s)), events_out)
- | _ -> (Ivh_error (Interp.Internal_error "Assert failed"), events_out) end
+ (Ivh_error (Sail_impl_base.Internal_error ("Assert failed: " ^ s)), events_out)
+ | _ -> (Ivh_error (Sail_impl_base.Internal_error "Assert failed"), events_out) end
| (Interp.Action (Interp.Exit exp) stack,_,_) ->
interp_to_value_helper arg ivh_mode err_str instr direction registers events true
(fun _ -> Interp.resume mode (Interp.set_in_context stack exp) Nothing)
@@ -361,7 +361,7 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
| Interp.SubReg (Id_aux (Id i) _) (Interp.Reg (Id_aux (Id i2) _) _ _) _ -> i2 ^ "." ^ i
| _ -> Assert_extra.failwith "Reg not following expected structure" end in
let err_value =
- (Ivh_error (Interp.Internal_error ("Register read of "^ rname^" request in a " ^ errk_str ^ " of " ^ err_str)),
+ (Ivh_error (Sail_impl_base.Internal_error ("Register read of "^ rname^" request in a " ^ errk_str ^ " of " ^ err_str)),
events_out) in
(match registers with
| Nothing -> err_value
@@ -380,14 +380,14 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
interp_to_value_helper arg ivh_mode err_str instr direction registers ((E_write_reg ext_reg reg_value)::events)
exn_seen (fun _ -> Interp.resume mode stack Nothing)
| (Interp.Action (Interp.Read_mem _ _ _) _,_,_) ->
- (Ivh_error (Interp.Internal_error ("Read memory request in a " ^ errk_str)), events_out)
+ (Ivh_error (Sail_impl_base.Internal_error ("Read memory request in a " ^ errk_str)), events_out)
| (Interp.Action (Interp.Write_mem _ _ _ _) _,_,_) ->
- (Ivh_error (Interp.Internal_error ("Write memory request in a " ^ errk_str)), events_out)
+ (Ivh_error (Sail_impl_base.Internal_error ("Write memory request in a " ^ errk_str)), events_out)
| (Interp.Action (Interp.Write_ea _ _) _,_,_) ->
- (Ivh_error (Interp.Internal_error ("Write ea request in a " ^ errk_str)), events_out)
+ (Ivh_error (Sail_impl_base.Internal_error ("Write ea request in a " ^ errk_str)), events_out)
| (Interp.Action (Interp.Write_memv _ _ _) _,_,_) ->
- (Ivh_error (Interp.Internal_error ("Write memory value request in a " ^ errk_str)), events_out)
- | _ -> (Ivh_error (Interp.Internal_error ("Non expected action in a " ^ errk_str)), events_out)
+ (Ivh_error (Sail_impl_base.Internal_error ("Write memory value request in a " ^ errk_str)), events_out)
+ | _ -> (Ivh_error (Sail_impl_base.Internal_error ("Non expected action in a " ^ errk_str)), events_out)
end
let call_external_functions direction outcome =
@@ -432,7 +432,7 @@ let translate_address top_level end_flag thunk_name registers address =
| Ivh_value_after_exn _ ->
(Nothing, events)
| Ivh_error err -> match err with
- | Interp.Internal_error msg -> Assert_extra.failwith msg
+ | Sail_impl_base.Internal_error msg -> Assert_extra.failwith msg
| _ -> Assert_extra.failwith "Not an internal error either" end
end
@@ -574,7 +574,7 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
| _ -> Assert_extra.failwith "Analysis did not return a four-tuple of lists" end)
| Ivh_value_after_exn _ -> Assert_extra.failwith "Instruction analysis failed"
| Ivh_error err -> match err with
- | Interp.Internal_error msg -> Assert_extra.failwith msg
+ | Sail_impl_base.Internal_error msg -> Assert_extra.failwith msg
| _ -> Assert_extra.failwith "Not an internal error either" end
end
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 2178bb50..ea3ba154 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -158,12 +158,12 @@ val initial_instruction_state : context -> string -> list register_value -> inst
type instruction_or_decode_error =
| IDE_instr of instruction * Interp.value
- | IDE_decode_error of Interp.decode_error
+ | IDE_decode_error of decode_error
(** propose to remove the following type and use the above instead *)
type i_state_or_error =
| Instr of instruction * instruction_state
- | Decode_error of Interp.decode_error
+ | Decode_error of decode_error
(** PS:I agree. propose to remove this: Function to decode an instruction and build the state to run it*)
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index bfa161c4..e932282c 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -1356,3 +1356,45 @@ end
type v_kind = Bitv | Bytev
+type decode_error =
+ | Unsupported_instruction_error of instruction
+ | Not_an_instruction_error of opcode
+ | Internal_error of string
+
+
+let decode_error_compare e1 e2 =
+ match (e1, e2) with
+ | (Unsupported_instruction_error i1, Unsupported_instruction_error i2)
+ -> defaultCompare i1 i2
+ | (Unsupported_instruction_error _, _) -> LT
+ | (_, Unsupported_instruction_error _) -> GT
+
+ | (Not_an_instruction_error o1, Not_an_instruction_error o2) -> defaultCompare o1 o2
+ | (Not_an_instruction_error _, _) -> LT
+ | (_, Not_an_instruction_error _) -> GT
+
+ | (Internal_error s1, Internal_error s2) -> compare s1 s2
+ (* | (Internal_error _, _) -> LT *)
+ (* | (_, Internal_error _) -> GT *)
+ end
+
+let decode_error_less e1 e2 = decode_error_compare e1 e2 = LT
+let decode_error_less_eq e1 e2 = decode_error_compare e1 e2 <> GT
+let decode_error_greater e1 e2 = decode_error_compare e1 e2 = GT
+let decode_error_greater_eq e1 e2 = decode_error_compare e1 e2 <> LT
+
+instance (Ord decode_error)
+ let compare = decode_error_compare
+ let (<) = decode_error_less
+ let (<=) = decode_error_less_eq
+ let (>) = decode_error_greater
+ let (>=) = decode_error_greater_eq
+end
+
+let decode_error_equal e1 e2 = (decode_error_compare e1 e2) = EQ
+let decode_error_inequal e1 e2 = not (decode_error_equal e1 e2)
+
+instance (Eq decode_error)
+ let (=) = decode_error_equal
+ let (<>) = decode_error_inequal
+end
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 18:30:25 +0000