summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/constant_fold.ml5
-rw-r--r--src/interpreter.ml51
-rw-r--r--src/isail.ml19
3 files changed, 46 insertions, 29 deletions
diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index 2c46f38b..15772168 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -123,11 +123,14 @@ and is_constant_fexp (FE_aux (FE_Fexp (_, exp), _)) = is_constant exp
let rec run frame =
match frame with
| Interpreter.Done (state, v) -> v
+ | Interpreter.Fail _ ->
+ (* something went wrong, raise exception to abort constant folding *)
+ assert false
| Interpreter.Step (lazy_str, _, _, _) ->
run (Interpreter.eval_frame frame)
| Interpreter.Break frame ->
run (Interpreter.eval_frame frame)
- | Interpreter.Effect_request (st, Interpreter.Read_reg (reg, cont)) ->
+ | Interpreter.Effect_request (out, st, stack, Interpreter.Read_reg (reg, cont)) ->
(* return a dummy value to read_reg requests which we handle above
if an expression finally evals to it, but the interpreter
will fail if it tries to actually use. See value.ml *)
diff --git a/src/interpreter.ml b/src/interpreter.ml
index cad9cc00..33370816 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -142,7 +142,7 @@ type 'a response =
| Read_mem of (* read_kind : *) value * (* address : *) value * (* length : *) value * (value -> 'a)
| Write_ea of (* write_kind : *) value * (* address : *) value * (* length : *) value * (unit -> 'a)
| Excl_res of (bool -> 'a)
- | Write_memv of value * (bool -> 'a)
+ | Write_mem of (* write_kind : *) value * (* address : *) value * (* length : *) value * (* value : *) value * (bool -> 'a)
| Barrier of (* barrier_kind : *) value * (unit -> 'a)
| Read_reg of string * (value -> 'a)
| Write_reg of string * value * (unit -> 'a)
@@ -164,7 +164,7 @@ let map_response f = function
| Read_mem (rk, addr, len, cont) -> Read_mem (rk, addr, len, fun v -> f (cont v))
| Write_ea (wk, addr, len, cont) -> Write_ea (wk, addr, len, fun () -> f (cont ()))
| Excl_res cont -> Excl_res (fun b -> f (cont b))
- | Write_memv (v, cont) -> Write_memv (v, fun b -> f (cont b))
+ | Write_mem (wk, addr, len, v, cont) -> Write_mem (wk, addr, len, v, fun b -> f (cont b))
| Barrier (bk, cont) -> Barrier (bk, fun () -> f (cont ()))
| Read_reg (name, cont) -> Read_reg (name, fun v -> f (cont v))
| Write_reg (name, v, cont) -> Write_reg (name, v, fun () -> f (cont ()))
@@ -215,8 +215,8 @@ let write_ea wk addr len : unit monad =
let excl_res () : bool monad =
Yield (Excl_res (fun b -> Pure b))
-let write_memv v : bool monad =
- Yield (Write_memv (v, fun b -> Pure b))
+let write_mem wk addr len v : bool monad =
+ Yield (Write_mem (wk, addr, len, v, fun b -> Pure b))
let barrier bk : unit monad =
Yield (Barrier (bk, fun () -> Pure ()))
@@ -393,7 +393,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| _ ->
fail "Wrong number of parameters to read_mem intrinsic"
end
- | "write_ea" ->
+ | "write_mem_ea" ->
begin match evaluated with
| [wk; addr; len] ->
write_ea (value_of_exp wk) (value_of_exp addr) (value_of_exp len) >> wrap unit_exp
@@ -407,10 +407,10 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| _ ->
fail "Wrong number of parameters to excl_res intrinsic"
end
- | "write_memv" ->
+ | "write_mem" ->
begin match evaluated with
- | [v] ->
- write_memv (value_of_exp v) >>= fun b -> return (exp_of_value (V_bool b))
+ | [wk; addr; len; v] ->
+ write_mem (value_of_exp wk) (value_of_exp v) (value_of_exp len) (value_of_exp v) >>= fun b -> return (exp_of_value (V_bool b))
| _ ->
fail "Wrong number of parameters to write_memv intrinsic"
end
@@ -751,22 +751,24 @@ type frame =
| Done of state * value
| Step of string Lazy.t * state * (Type_check.tannot exp) monad * (string Lazy.t * lstate * (return_value -> (Type_check.tannot exp) monad)) list
| Break of frame
- | Effect_request of state * effect_request
+ | Effect_request of string Lazy.t * state * (string Lazy.t * lstate * (return_value -> (Type_check.tannot exp) monad)) list * effect_request
+ | Fail of string Lazy.t * state * (Type_check.tannot exp) monad * (string Lazy.t * lstate * (return_value -> (Type_check.tannot exp) monad)) list * string
(* when changing effect_request remember to also update response type above *)
and effect_request =
| Read_mem of (* read_kind : *) value * (* address : *) value * (* length : *) value * (value -> state -> frame)
| Write_ea of (* write_kind : *) value * (* address : *) value * (* length : *) value * (unit -> state -> frame)
| Excl_res of (bool -> state -> frame)
- | Write_memv of value * (bool -> state -> frame)
+ | Write_mem of (* write_kind : *) value * (* address : *) value * (* length : *) value * (* value : *) value * (bool -> state -> frame)
| Barrier of (* barrier_kind : *) value * (unit -> state -> frame)
| Read_reg of string * (value -> state -> frame)
| Write_reg of string * value * (unit -> state -> frame)
let rec eval_frame' = function
| Done (state, v) -> Done (state, v)
+ | Fail (out, state, m, stack, msg) -> Fail (out, state, m, stack, msg)
| Break frame -> Break frame
- | Effect_request (state, eff) -> Effect_request (state, eff)
+ | Effect_request (out, state, stack, eff) -> Effect_request (out, state, stack, eff)
| Step (out, state, m, stack) ->
let lstate, gstate = state in
match (m, stack) with
@@ -796,9 +798,9 @@ let rec eval_frame' = function
end
| Yield (Read_reg (name, cont)), _ ->
- Effect_request (state, Read_reg (name, fun v state' -> eval_frame' (Step (out, state', cont v, stack))))
+ Effect_request (out, state, stack, Read_reg (name, fun v state' -> eval_frame' (Step (out, state', cont v, stack))))
| Yield (Write_reg (name, v, cont)), _ ->
- Effect_request (state, Write_reg (name, v, fun () state' -> eval_frame' (Step (out, state', cont (), stack))))
+ Effect_request (out, state, stack, Write_reg (name, v, fun () state' -> eval_frame' (Step (out, state', cont (), stack))))
| Yield (Get_primop (name, cont)), _ ->
begin
try
@@ -820,22 +822,22 @@ let rec eval_frame' = function
| Yield (Get_global_letbinds cont), _ ->
eval_frame' (Step (out, state, cont gstate.letbinds, stack))
| Yield (Read_mem (rk, addr, len, cont)), _ ->
- Effect_request (state, Read_mem (rk, addr, len, fun result state' -> eval_frame' (Step (out, state', cont result, stack))))
+ Effect_request (out, state, stack, Read_mem (rk, addr, len, fun result state' -> eval_frame' (Step (out, state', cont result, stack))))
| Yield (Write_ea (wk, addr, len, cont)), _ ->
- Effect_request (state, Write_ea (wk, addr, len, fun () state' -> eval_frame' (Step (out, state', cont (), stack))))
+ Effect_request (out, state, stack, Write_ea (wk, addr, len, fun () state' -> eval_frame' (Step (out, state', cont (), stack))))
| Yield (Excl_res cont), _ ->
- Effect_request (state, Excl_res (fun b state' -> eval_frame' (Step (out, state', cont b, stack))))
- | Yield (Write_memv (v, cont)), _ ->
- Effect_request (state, Write_memv (v, fun b state' -> eval_frame' (Step (out, state', cont b, stack))))
+ Effect_request (out, state, stack, Excl_res (fun b state' -> eval_frame' (Step (out, state', cont b, stack))))
+ | Yield (Write_mem (wk, addr, len, v, cont)), _ ->
+ Effect_request (out, state, stack, Write_mem (wk, addr, len, v, fun b state' -> eval_frame' (Step (out, state', cont b, stack))))
| Yield (Barrier (bk, cont)), _ ->
- Effect_request (state, Barrier (bk, fun () state' -> eval_frame' (Step (out, state', cont (), stack))))
+ Effect_request (out, state, stack, Barrier (bk, fun () state' -> eval_frame' (Step (out, state', cont (), stack))))
| Yield (Early_return v), [] -> Done (state, v)
| Yield (Early_return v), (head :: stack') ->
Step (stack_string head, (stack_state head, gstate), stack_cont head (Return_ok v), stack')
| Yield (Assertion_failed msg), _ | Yield (Fail msg), _ ->
- failwith msg
+ Fail (out, state, m, stack, msg)
| Yield (Exception v), [] ->
- failwith ("Uncaught Exception" |> Util.cyan |> Util.clear)
+ Fail (out, state, m, stack, "Uncaught exception: " ^ string_of_value v)
| Yield (Exception v), (head :: stack') ->
Step (stack_string head, (stack_state head, gstate), stack_cont head (Return_exception v), stack')
@@ -860,10 +862,10 @@ let default_effect_interp state eff =
| Excl_res cont ->
(* always succeeds in single-threaded interpreter *)
cont true state
- | Write_memv (v, cont) ->
+ | Write_mem (wk, addr, len, v, cont) ->
begin
match gstate.last_write_ea with
- | Some (wk, addr, len) ->
+ | Some (wk', addr', len') ->
let state' = (lstate, { gstate with last_write_ea = None }) in
(* all write-kinds treated the same in single-threaded interpreter *)
let addr' = coerce_bv addr in
@@ -909,11 +911,12 @@ let default_effect_interp state eff =
let rec run_frame frame =
match frame with
| Done (state, v) -> v
+ | Fail (_, _, _, _, msg) -> failwith ("run_frame got Fail: " ^ msg)
| Step (lazy_str, _, _, _) ->
run_frame (eval_frame frame)
| Break frame ->
run_frame (eval_frame frame)
- | Effect_request (state, eff) ->
+ | Effect_request (out, state, stack, eff) ->
run_frame (default_effect_interp state eff)
let eval_exp state exp =
diff --git a/src/isail.ml b/src/isail.ml
index 30e02b36..7a33c7d1 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -120,7 +120,9 @@ let sep = "-----------------------------------------------------" |> Util.blue |
let print_program () =
match !current_mode with
| Normal | Emacs -> ()
- | Evaluation (Step (out, _, _, stack)) ->
+ | Evaluation (Step (out, _, _, stack))
+ | Evaluation (Effect_request(out, _, stack, _))
+ | Evaluation (Fail (out, _, _, stack, _)) ->
List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline (Lazy.force code); print_endline sep);
print_endline (Lazy.force out)
| Evaluation (Done (_, v)) ->
@@ -153,6 +155,9 @@ let rec run () =
interactive_state := state;
print_endline ("Result = " ^ Value.string_of_value v);
current_mode := Normal
+ | Fail (_, _, _, _, msg) ->
+ print_endline ("Error: " ^ msg);
+ current_mode := Normal
| Step (out, state, _, stack) ->
begin
try
@@ -164,7 +169,7 @@ let rec run () =
| Break frame ->
print_endline "Breakpoint";
current_mode := Evaluation frame
- | Effect_request (state, eff) ->
+ | Effect_request (out, state, stack, eff) ->
begin
try
current_mode := Evaluation (Interpreter.default_effect_interp state eff)
@@ -187,6 +192,9 @@ let rec run_steps n =
interactive_state := state;
print_endline ("Result = " ^ Value.string_of_value v);
current_mode := Normal
+ | Fail (_, _, _, _, msg) ->
+ print_endline ("Error: " ^ msg);
+ current_mode := Normal
| Step (out, state, _, stack) ->
begin
try
@@ -198,7 +206,7 @@ let rec run_steps n =
| Break frame ->
print_endline "Breakpoint";
current_mode := Evaluation frame
- | Effect_request (state, eff) ->
+ | Effect_request (out, state, stack, eff) ->
begin
try
current_mode := Evaluation (Interpreter.default_effect_interp state eff)
@@ -552,6 +560,9 @@ let handle_input' input =
interactive_state := state;
print_endline ("Result = " ^ Value.string_of_value v);
current_mode := Normal
+ | Fail (_, _, _, _, msg) ->
+ print_endline ("Error: " ^ msg);
+ current_mode := Normal
| Step (out, state, _, stack) ->
begin
try
@@ -564,7 +575,7 @@ let handle_input' input =
| Break frame ->
print_endline "Breakpoint";
current_mode := Evaluation frame
- | Effect_request (state, eff) ->
+ | Effect_request (out, state, stack, eff) ->
begin
try
interactive_state := state;
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 11:30:13 +0000