diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/interpreter.ml | 193 |
1 files changed, 135 insertions, 58 deletions
diff --git a/src/interpreter.ml b/src/interpreter.ml index 2ea8bb00..407f512a 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -52,6 +52,8 @@ open Ast open Ast_util open Value + + type gstate = { registers : value Bindings.t; allow_registers : bool; (* For some uses we want to forbid touching any registers. *) @@ -123,8 +125,19 @@ type 'a response = | Exception of value | Assertion_failed of string | Call of id * value list * (return_value -> 'a) - | Gets of (state -> 'a) - | Puts of state * (unit -> 'a) + | Fail of string + (* TODO *) + (* | Read_mem of Sail2_instr_kinds.read_kind * (\* address : *\) value * (\* length : *\) value * (value -> 'a) + * | Write_ea of Sail2_instr_kinds.write_kind * (\* address : *\) value * (\* length : *\) value * (unit -> 'a) + * | Excl_res of (bool -> 'a) + * | Write_memv of value * (bool -> 'a) + * | Barrier of Sail2_instr_kinds.barrier_kind * (unit -> 'a) *) + | Read_reg of string * (value -> 'a) + | Write_reg of string * value * (unit -> 'a) + | Get_primop of string * ((value list -> value) -> 'a) + | Get_local of string * (value -> 'a) + | Put_local of string * value * (unit -> 'a) + | Get_global_letbinds of ((Type_check.tannot letbind) list -> 'a) and 'a monad = | Pure of 'a @@ -134,9 +147,20 @@ let map_response f = function | Early_return v -> Early_return v | Exception v -> Exception v | Assertion_failed str -> Assertion_failed str - | Gets g -> Gets (fun s -> f (g s)) - | Puts (s, cont) -> Puts (s, fun () -> f (cont ())) | Call (id, vals, cont) -> Call (id, vals, fun v -> f (cont v)) + | Fail s -> Fail s + (* TODO *) + (* | 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)) + * | 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 ())) + | Get_primop (name, cont) -> Get_primop (name, fun op -> f (cont op)) + | Get_local (name, cont) -> Get_local (name, fun v -> f (cont v)) + | Put_local (name, v, cont) -> Put_local (name, v, fun () -> f (cont ())) + | Get_global_letbinds cont -> Get_global_letbinds (fun lbs -> f (cont lbs)) let rec liftM f = function | Pure x -> Pure (f x) @@ -170,12 +194,43 @@ let throw v = Yield (Exception v) let call (f : id) (args : value list) : return_value monad = Yield (Call (f, args, fun v -> Pure v)) -let gets : state monad = - Yield (Gets (fun s -> Pure s)) - -let puts (s : state) : unit monad = - Yield (Puts (s, fun () -> Pure ())) - +(* TODO *) +(* let read_mem (rk, addr, len) : value monad = + * Yield (Read_mem (rk, addr, len, (fun v -> Pure v))) + * + * let write_ea (wk, addr, len) : unit monad = + * Yield (Write_ea (wk, addr, len, (fun () -> Pure ()))) + * + * 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 barrier bk : unit monad = + * Yield (Barrier (bk, fun () -> Pure ())) *) + +let read_reg name : value monad = + Yield (Read_reg (name, fun v -> Pure v)) + +let write_reg name v : unit monad = + Yield (Write_reg (name, v, fun () -> Pure ())) + +let fail s = + Yield (Fail s) + +let get_primop name : (value list -> value) monad = + Yield (Get_primop (name, fun op -> Pure op)) + +let get_local name : value monad = + Yield (Get_local (name, fun v -> Pure v)) + +let put_local name v : unit monad = + Yield (Put_local (name, v, fun () -> Pure ())) + +let get_global_letbinds () : (Type_check.tannot letbind) list monad = + Yield (Get_global_letbinds (fun lbs -> Pure lbs)) + let early_return v = Yield (Early_return v) let assertion_failed msg = Yield (Assertion_failed msg) @@ -278,7 +333,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = if matched then return (List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings)) else - failwith "Match failure" + fail "Match failure" | E_vector_subrange (vec, n, m) -> wrap (E_app (mk_id "vector_subrange_dec", [vec; n; m])) @@ -306,14 +361,9 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = let extern = get_interpreter_extern id (env_of_annot annot) in if extern = "reg_deref" then let regname = List.hd evaluated |> value_of_exp |> coerce_ref in - gets >>= fun (_, gstate) -> - if gstate.allow_registers - then return (exp_of_value (Bindings.find (mk_id regname) gstate.registers)) - else raise Not_found + read_reg regname >>= fun v -> return (exp_of_value v) else - gets >>= fun (_, gstate) -> - let primop = try StringMap.find extern gstate.primops with Not_found -> failwith ("No primop " ^ extern) in - return (exp_of_value (primop (List.map value_of_exp evaluated))) + get_primop extern >>= fun op -> return (exp_of_value (op (List.map value_of_exp evaluated))) end | [] -> call id (List.map value_of_exp evaluated) >>= @@ -370,33 +420,23 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | E_exit exp -> step exp >>= fun exp' -> wrap (E_exit exp') | E_ref id -> - gets >>= fun (lstate, gstate) -> - if Bindings.mem id gstate.registers && gstate.allow_registers then - return (exp_of_value (V_ref (string_of_id id))) - else - failwith ("Could not find register " ^ string_of_id id) + return (exp_of_value (V_ref (string_of_id id))) | E_id id -> begin let open Type_check in - gets >>= fun (lstate, gstate) -> match Env.lookup_id id (env_of_annot annot) with - | Register _ when gstate.allow_registers -> - let exp = - try exp_of_value (Bindings.find id gstate.registers) with - | Not_found -> - (* Replace with error message? *) - let exp = mk_exp (E_app (mk_id ("undefined_" ^ string_of_typ (typ_of orig_exp)), [mk_exp (E_lit (mk_lit (L_unit)))])) in - Type_check.check_exp (env_of_annot annot) exp (typ_of orig_exp) - in - return exp - | Local (Mutable, _) -> return (local_variable id lstate gstate) + | Register _ -> + read_reg (string_of_id id) >>= fun v -> return (exp_of_value v) + | Local (Mutable, _) -> get_local (string_of_id id) >>= fun v -> return (exp_of_value v) | Local (Immutable, _) -> - let chain = build_letchain id gstate.letbinds orig_exp in + (* if we get here without already having substituted, it must be a top-level letbind *) + get_global_letbinds () >>= fun lbs -> + let chain = build_letchain id lbs orig_exp in return chain | Enum _ -> return (exp_of_value (V_ctor (string_of_id id, []))) - | _ -> failwith ("Coudln't find id " ^ string_of_id id) + | _ -> fail ("Couldn't find id " ^ string_of_id id) end | E_record (FES_aux (FES_Fexps (fexps, flag), fes_annot)) -> @@ -458,25 +498,18 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | E_assign (LEXP_aux (LEXP_id id, _), exp) | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) -> begin let open Type_check in - gets >>= fun (lstate, gstate) -> match Env.lookup_id id (env_of_annot annot) with - | Register _ when gstate.allow_registers -> - puts (lstate, { gstate with registers = Bindings.add id (value_of_exp exp) gstate.registers }) >> wrap unit_exp + | Register _ -> + write_reg (string_of_id id) (value_of_exp exp) >> wrap unit_exp | Local (Mutable, _) | Unbound -> - begin - puts ({ locals = Bindings.add id (value_of_exp exp) lstate.locals }, gstate) >> wrap unit_exp - end + put_local (string_of_id id) (value_of_exp exp) >> wrap unit_exp | _ -> failwith "Assign" end | E_assign (LEXP_aux (LEXP_deref reference, annot), exp) when not (is_value reference) -> step reference >>= fun reference' -> wrap (E_assign (LEXP_aux (LEXP_deref reference', annot), exp)) | E_assign (LEXP_aux (LEXP_deref reference, annot), exp) -> let name = coerce_ref (value_of_exp reference) in - gets >>= fun (lstate, gstate) -> - if Bindings.mem (mk_id name) gstate.registers && gstate.allow_registers then - puts (lstate, { gstate with registers = Bindings.add (mk_id name) (value_of_exp exp) gstate.registers }) >> wrap unit_exp - else - failwith "Assign to nonexistent register" + write_reg name (value_of_exp exp) >> wrap unit_exp | E_assign (LEXP_aux (LEXP_tup lexps, annot), exp) -> failwith "Tuple assignment" | E_assign (LEXP_aux (LEXP_vector_concat lexps, annot), exp) -> failwith "Vector concat assignment" (* @@ -640,34 +673,78 @@ let rec eval_frame' = function | Done (state, v) -> Done (state, v) | Break frame -> Break frame | Step (out, state, m, stack) -> + let lstate, gstate = state in match (m, stack) with | Pure v, [] when is_value v -> Done (state, value_of_exp v) | Pure v, (head :: stack') when is_value v -> - Step (stack_string head, (stack_state head, snd state), stack_cont head (Return_ok (value_of_exp v)), stack') + Step (stack_string head, (stack_state head, gstate), stack_cont head (Return_ok (value_of_exp v)), stack') | Pure exp', _ -> let out' = lazy (Pretty_print_sail.to_string (Pretty_print_sail.doc_exp exp')) in Step (out', state, step exp', stack) | Yield (Call(id, vals, cont)), _ when string_of_id id = "break" -> let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in - let body = exp_of_fundef (Bindings.find id (snd state).fundefs) arg in - Break (Step (lazy "", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack)) + let body = exp_of_fundef (Bindings.find id gstate.fundefs) arg in + Break (Step (lazy "", (initial_lstate, gstate), return body, (out, lstate, cont) :: stack)) | Yield (Call(id, vals, cont)), _ -> let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in - let body = exp_of_fundef (Bindings.find id (snd state).fundefs) arg in - Step (lazy "", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack) - | Yield (Gets cont), _ -> - eval_frame' (Step (out, state, cont state, stack)) - | Yield (Puts (state', cont)), _ -> + let body = exp_of_fundef (Bindings.find id gstate.fundefs) arg in + Step (lazy "", (initial_lstate, gstate), return body, (out, lstate, cont) :: stack) + + | Yield (Read_reg (name, cont)), _ -> + begin + let gstate = gstate in + if gstate.allow_registers then + try + eval_frame' (Step (out, state, cont (Bindings.find (mk_id name) gstate.registers), stack)) + with Not_found -> + eval_frame' (Step (out, state, fail ("Read of nonexistent register: " ^ name), stack)) + else + eval_frame' (Step (out, state, fail ("Register read disallowed by allow_registers setting: " ^ name), stack)) + end + | Yield (Write_reg (name, v, cont)), _ -> + begin + let id = mk_id name in + let gstate = gstate in + if gstate.allow_registers then + (* TODO: check existence of register? would then need to initialise all to undefined below or similar *) + (* if Bindings.mem id gstate.registers then *) + let state' = (lstate, { gstate with registers = Bindings.add id v gstate.registers }) in + eval_frame' (Step (out, state', cont (), stack)) + (* else + * eval_frame' (Step (out, state, fail ("Write of nonexistent register: " ^ name), stack)) *) + else + eval_frame' (Step (out, state, fail ("Register write disallowed by allow_registers setting: " ^ name), stack)) + end + | Yield (Get_primop (name, cont)), _ -> + begin + try + let op = StringMap.find name gstate.primops in + eval_frame' (Step (out, state, cont op, stack)) + with Not_found -> + eval_frame' (Step (out, state, fail ("No such primop: " ^ name), stack)) + end + | Yield (Get_local (name, cont)), _ -> + begin + try + eval_frame' (Step (out, state, cont (Bindings.find (mk_id name) lstate.locals), stack)) + with Not_found -> + eval_frame' (Step (out, state, fail ("Local not found: " ^ name), stack)) + end + | Yield (Put_local (name, v, cont)), _ -> + let state' = ({ locals = Bindings.add (mk_id name) v lstate.locals }, gstate) in eval_frame' (Step (out, state', cont (), stack)) + | Yield (Get_global_letbinds cont), _ -> + eval_frame' (Step (out, state, cont gstate.letbinds, stack)) + | Yield (Early_return v), [] -> Done (state, v) | Yield (Early_return v), (head :: stack') -> - Step (stack_string head, (stack_state head, snd state), stack_cont head (Return_ok v), stack') - | Yield (Assertion_failed msg), _ -> + Step (stack_string head, (stack_state head, gstate), stack_cont head (Return_ok v), stack') + | Yield (Assertion_failed msg), _ | Yield (Fail msg), _ -> failwith msg | Yield (Exception v), [] -> failwith ("Uncaught Exception" |> Util.cyan |> Util.clear) | Yield (Exception v), (head :: stack') -> - Step (stack_string head, (stack_state head, snd state), stack_cont head (Return_exception v), stack') + Step (stack_string head, (stack_state head, gstate), stack_cont head (Return_exception v), stack') let eval_frame frame = try eval_frame' frame with |