From 53af9ce7a683ee4542b8facc44edfd1e3ef64cf6 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 16 Jan 2018 19:36:16 +0000 Subject: Test the ocaml interpreter with the same tests as the ocaml compilation --- src/ast_util.ml | 4 +++- src/interpreter.ml | 11 +++++++++-- src/isail.ml | 11 +++++++++-- src/value.ml | 25 ++++++++++++++++++++++--- test/ocaml/prelude.sail | 8 +++++++- test/ocaml/reg_passing/reg_passing.sail | 3 ++- test/ocaml/run_tests.sh | 23 ++++++++++++++++++++++- 7 files changed, 74 insertions(+), 11 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 - 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)); diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail index add43eec..6b8acb44 100644 --- a/test/ocaml/prelude.sail +++ b/test/ocaml/prelude.sail @@ -18,7 +18,10 @@ val eq_string = "eq_string" : (string, string) -> bool val eq_real = "eq_real" : (real, real) -> bool -val eq_anything = "(fun (x, y) -> x = y)" : forall ('a : Type). ('a, 'a) -> bool +val eq_anything = { + ocaml: "(fun (x, y) -> x = y)", + interpreter: "eq_anything" + } : forall ('a : Type). ('a, 'a) -> bool val length = "length" : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) @@ -141,6 +144,9 @@ val __ZeroExtendSlice : forall 'm. (bits('m), int, int) -> bits('m) val cast cast_unit_vec : bit -> bits(1) +function cast_unit_vec bitone = 0b1 +and cast_unit_vec bitzero = 0b0 + val print = "print_endline" : string -> unit val putchar = "putchar" : forall ('a : Type). 'a -> unit diff --git a/test/ocaml/reg_passing/reg_passing.sail b/test/ocaml/reg_passing/reg_passing.sail index d84f98e0..35ddda93 100644 --- a/test/ocaml/reg_passing/reg_passing.sail +++ b/test/ocaml/reg_passing/reg_passing.sail @@ -5,7 +5,8 @@ register R3 : int val cast "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} val output = { - ocaml: "(fun (str, n) -> print_endline (str ^ string_of_big_int n))" + ocaml: "(fun (str, n) -> print_endline (str ^ string_of_big_int n))", + interpreter: "print_int" } : (string, int) -> unit val f : register(int) -> unit effect {rreg, wreg} diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh index ccc3889e..62fe9950 100755 --- a/test/ocaml/run_tests.sh +++ b/test/ocaml/run_tests.sh @@ -81,7 +81,7 @@ do then green "built $i" "ok" else - yellow "bad output $i" "fail" + red "bad output $i" "fail" fi; rm out; rm result; @@ -93,4 +93,25 @@ done finish_suite "Ocaml trace testing" +cd $DIR + +for i in `ls -d */`; +do + cd $DIR/$i; + if $SAILDIR/sail -is test.isail ../prelude.sail `ls *.sail` 1> /dev/null; + then + if diff expect result; + then + green "interpreted $i" "ok" + else + red "bad output $i" "fail" + fi; + rm result + else + red "interpreter crashed on $i" "fail" + fi +done + +finish_suite "Interpreter testing" + printf "\n" >> $DIR/tests.xml -- cgit v1.2.3