diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 4 | ||||
| -rw-r--r-- | src/interpreter.ml | 11 | ||||
| -rw-r--r-- | src/isail.ml | 11 | ||||
| -rw-r--r-- | src/value.ml | 25 |
4 files changed, 43 insertions, 8 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 206515c5..fdd20050 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -636,7 +636,9 @@ let rec string_of_exp (E_aux (exp, _)) = | E_var _ -> "INTERNAL LET" | E_internal_return exp -> "internal_return (" ^ string_of_exp exp ^ ")" | E_internal_plet (pat, exp, body) -> "internal_plet " ^ string_of_pat pat ^ " = " ^ string_of_exp exp ^ " in " ^ string_of_exp body - | _ -> "INTERNAL" + | E_nondet _ -> "NONDET" + | E_internal_value _ -> "INTERNAL VALUE" + and string_of_fexp (FE_aux (FE_Fexp (field, exp), _)) = string_of_id field ^ " = " ^ string_of_exp exp and string_of_pexp (Pat_aux (pexp, _)) = diff --git a/src/interpreter.ml b/src/interpreter.ml index e88c5e93..1a8cad90 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -393,6 +393,12 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = else failwith "Match failure" + + | E_vector_subrange (vec, n, m) -> + wrap (E_app (mk_id "vector_subrange_dec", [vec; n; m])) + | E_vector_access (vec, n) -> + wrap (E_app (mk_id "vector_access_dec", [vec; n])) + | E_vector_update (vec, n, x) -> wrap (E_app (mk_id "vector_update", [vec; n; x])) | E_vector_update_subrange (vec, n, m, x) -> @@ -506,9 +512,9 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | Local (Immutable, _) -> let chain = build_letchain id gstate.letbinds orig_exp in return chain - | Enum _ -> + | Enum _ | Union _ -> return (exp_of_value (V_ctor (string_of_id id, []))) - | _ -> failwith "id" + | _ -> failwith ("id " ^ string_of_id id) end | E_record (FES_aux (FES_Fexps (fexps, flag), fes_annot)) -> @@ -661,6 +667,7 @@ and pattern_match env (P_aux (p_aux, _) as pat) value = let matches = List.map2 (pattern_match env) pats (coerce_gv value) in List.for_all fst matches, List.fold_left (Bindings.merge combine) Bindings.empty (List.map snd matches) | P_vector_concat _ -> assert false (* TODO *) + | P_tup [pat] -> pattern_match env pat value | P_tup pats | P_list pats -> let matches = List.map2 (pattern_match env) pats (coerce_listlike value) in List.for_all fst matches, List.fold_left (Bindings.merge combine) Bindings.empty (List.map snd matches) diff --git a/src/isail.ml b/src/isail.ml index e6dcc809..31e62fb5 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -181,6 +181,8 @@ let help = function "Files containing scattered definitions must be loaded together." ] | ":u" | ":unload" -> "(:u | :unload) - Unload all loaded files." + | ":output" -> + ":output <file> - Redirect evaluating expression output to a file." | cmd -> "Either invalid command passed to help, or no documentation for " ^ cmd ^ ". Try :help :help." @@ -222,7 +224,9 @@ let handle_input' input = let typq, typ = Type_check.Env.get_val_spec (mk_id arg) !interactive_env in pretty_sail stdout (doc_binding (typq, typ)); print_newline (); - | ":q" | ":quit" -> exit 0 + | ":q" | ":quit" -> + Value.output_close (); + exit 0 | ":i" | ":infer" -> let exp = Initial_check.exp_of_string dec_ord arg in let exp = Type_check.infer_exp !interactive_env exp in @@ -239,13 +243,16 @@ let handle_input' input = else print_endline "Invalid argument for :clear, expected either :clear on or :clear off" | ":commands" -> let commands = - [ "Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :clear :commands :help"; + [ "Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :clear :commands :help :output"; "Normal mode commands - :elf :(l)oad :(u)nload"; "Evaluation mode commands - :(r)un :(s)tep :(n)ormal"; ""; ":(c)ommand can be called as either :c or :command." ] in List.iter print_endline commands + | ":output" -> + let chan = open_out arg in + Value.output_redirect chan | ":help" -> print_endline (help arg) | _ -> recognised := false end diff --git a/src/value.ml b/src/value.ml index c9c6eca6..b5f7c0c7 100644 --- a/src/value.ml +++ b/src/value.ml @@ -52,6 +52,23 @@ module Big_int = Nat_big_num module StringMap = Map.Make(String) +let print_chan = ref stdout +let print_redirected = ref false + +let output_redirect chan = + print_chan := chan; + print_redirected := true + +let output_close () = + if !print_redirected then + close_out !print_chan + else + () + +let output_endline str = + output_string !print_chan (str ^ "\n"); + flush !print_chan + type value = | V_vector of value list | V_list of value list @@ -318,7 +335,8 @@ let value_eq_anything = function | _ -> failwith "value eq_anything" let value_print = function - | [v] -> print_endline (string_of_value v |> Util.red |> Util.clear); V_unit + | [V_string str] -> output_endline str; V_unit + | [v] -> output_endline (string_of_value v |> Util.red |> Util.clear); V_unit | _ -> assert false let value_internal_pick = function @@ -344,11 +362,11 @@ let value_putchar = function | _ -> failwith "value putchar" let value_print_bits = function - | [msg; bits] -> print_endline (coerce_string msg ^ string_of_value bits); V_unit + | [msg; bits] -> output_endline (coerce_string msg ^ string_of_value bits); V_unit | _ -> failwith "value print_bits" let value_print_int = function - | [msg; n] -> print_endline (coerce_string msg ^ string_of_value n); V_unit + | [msg; n] -> output_endline (coerce_string msg ^ string_of_value n); V_unit | _ -> failwith "value print_int" let primops = @@ -407,6 +425,7 @@ let primops = ("undefined_int", fun _ -> V_int Big_int.zero); ("undefined_bool", fun _ -> V_bool false); ("undefined_vector", value_undefined_vector); + ("undefined_string", fun _ -> V_string ""); ("internal_pick", value_internal_pick); ("replicate_bits", value_replicate_bits); ("Elf_loader.elf_entry", fun _ -> V_int (!Elf_loader.opt_elf_entry)); |