diff options
| author | Jon French | 2019-03-13 17:10:33 +0000 |
|---|---|---|
| committer | Jon French | 2019-03-13 17:10:33 +0000 |
| commit | 31acee54267e21465ba6e65dd338d61d30012aa9 (patch) | |
| tree | d69e5a3aa94e8a85c1e16a199cbf0cf17891273a /src/interpreter.ml | |
| parent | a3bc3d7221758850093827da1db030014c6d529f (diff) | |
Interpreter: return frame rather than eval-looping analyse_instruction
This is in order to allow register reads etc to be handled by RMEM
Diffstat (limited to 'src/interpreter.ml')
| -rw-r--r-- | src/interpreter.ml | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/src/interpreter.ml b/src/interpreter.ml index 577e1234..24af75e2 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -992,17 +992,13 @@ let annot_exp e_aux l env typ = annot_exp_effect e_aux l env typ no_effect let id_typ id = mk_typ (Typ_id (mk_id id)) let analyse_instruction state ast = - try - let env = (snd state).typecheck_env in - let unk = Parse_ast.Unknown in - let typed = annot_exp - (E_app (mk_id "initial_analysis", [annot_exp (E_internal_value ast) unk env (id_typ "ast")])) unk env - (tuple_typ [id_typ "regfps"; id_typ "regfps"; id_typ "regfps"; id_typ "niafps"; id_typ "diafp"; id_typ "instruction_kind"]) - in - let evaled = eval_exp state typed in - Value_success evaled - with _ as exn -> - Value_error exn + let env = (snd state).typecheck_env in + let unk = Parse_ast.Unknown in + let typed = annot_exp + (E_app (mk_id "initial_analysis", [annot_exp (E_internal_value ast) unk env (id_typ "ast")])) unk env + (tuple_typ [id_typ "regfps"; id_typ "regfps"; id_typ "regfps"; id_typ "niafps"; id_typ "diafp"; id_typ "instruction_kind"]) + in + Step (lazy (Pretty_print_sail.to_string (Pretty_print_sail.doc_exp typed)), state, return typed, []) let execute_instruction state ast = let env = (snd state).typecheck_env in |