diff options
| -rw-r--r-- | src/interpreter.ml | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/src/interpreter.ml b/src/interpreter.ml index 167c66f5..83f8b14e 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -997,3 +997,47 @@ let rec initialize_registers gstate = | Defs [] -> gstate let initial_state ast env primops = initial_lstate, initialize_registers (initial_gstate primops ast env) ast + +type value_result = + | Value_success of value + | Value_error of exn + +let decode_instruction state bv = + try + let env = (snd state).typecheck_env in + let untyped = mk_exp (E_app ((mk_id "decode"), [mk_exp (E_vector (List.map mk_lit_exp bv))])) in + let typed = Type_check.check_exp + env untyped (app_typ (mk_id "option") + [Typ_arg_aux (Typ_arg_typ (mk_typ (Typ_id (mk_id "ast"))), Parse_ast.Unknown)]) in + let evaled = eval_exp state typed in + match evaled with + | V_ctor ("Some", [v]) -> Value_success v + | V_ctor ("None", _) -> failwith "decode returned None" + | _ -> failwith "decode returned wrong value type" + with _ as exn -> + Value_error exn + +let annot_exp_effect e_aux l env typ effect = E_aux (e_aux, (l, Type_check.mk_tannot env typ effect)) +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 execute_instruction state ast = + let env = (snd state).typecheck_env in + let unk = Parse_ast.Unknown in + let typed = annot_exp + (E_app (mk_id "execute", [annot_exp (E_internal_value ast) unk env (id_typ "ast")])) unk env unit_typ + in + Step (lazy (Pretty_print_sail.to_string (Pretty_print_sail.doc_exp typed)), state, return typed, []) |