Fix interpreter after re-writer change

Interpreter used a re-write (vector concat removal) that is dependent
on the vector_string_to_bit_list rewriting pass. This fixes the
interpreter to work without either vector concat removal, or turning
bitstrings into vector literals like [bitzero, bitzero, bitone]. This
has the upside of reducing the number of steps the interpreter needs
for working with bitvectors so should improve interpreter performance.

We also now test all the C compilation tests behave the same using the
interpreter. Currently the real number tests fail due to limitations
of Lem's rational library (this must be fixed in Lem). This required
supporting configuration registers in the interpreter. As such the
interpreter was refactored to more cleanly process registers when
building an initial global state. The functions are also collected
into the global state, which removes the need to search for them in
the AST every time a function call happens. This should not only
improve performance, but also removes the need to pass an AST into the
interpretation functions.

7 files changed, 137 insertions, 58 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index b6f81de6..c85d3755 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -740,7 +740,7 @@ and string_of_pat (P_aux (pat, l)) =
   | P_app (f, pats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_pat pats ^ ")"
   | P_cons (pat1, pat2) -> string_of_pat pat1 ^ " :: " ^ string_of_pat pat2
   | P_list pats -> "[||" ^ string_of_list "," string_of_pat pats ^ "||]"
-  | P_vector_concat pats -> string_of_list " : " string_of_pat pats
+  | P_vector_concat pats -> string_of_list " @ " string_of_pat pats
   | P_vector pats -> "[" ^ string_of_list ", " string_of_pat pats ^ "]"
   | P_as (pat, id) -> "(" ^ string_of_pat pat ^ " as " ^ string_of_id id ^ ")"
   | P_string_append pats -> string_of_list " ^^ " string_of_pat pats
diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index 20c0628d..e9efac68 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -116,13 +116,13 @@ let rec is_constant (E_aux (e_aux, _)) =
 and is_constant_fexp (FE_aux (FE_Fexp (_, exp), _)) = is_constant exp
 
 (* Wrapper around interpreter that repeatedly steps until done. *)
-let rec run ast frame =
+let rec run frame =
   match frame with
   | Interpreter.Done (state, v) -> v
   | Interpreter.Step (lazy_str, _, _, _) ->
-     run ast (Interpreter.eval_frame ast frame)
+     run (Interpreter.eval_frame frame)
   | Interpreter.Break frame ->
-     run ast (Interpreter.eval_frame ast frame)
+     run (Interpreter.eval_frame frame)
 
 (** This rewriting pass looks for function applications (E_app)
    expressions where every argument is a literal. It passes these
@@ -155,7 +155,7 @@ let rec rewrite_constant_function_calls' ast =
     let initial_monad = Interpreter.return (E_aux (e_aux, annot)) in
     try
       begin
-        let v = run ast (Interpreter.Step (lazy "", (lstate, gstate), initial_monad, [])) in
+        let v = run (Interpreter.Step (lazy "", (lstate, gstate), initial_monad, [])) in
         let exp = exp_of_value v in
         try (ok (); Type_check.check_exp (env_of_annot annot) exp (typ_of_annot annot)) with
         | Type_error (l, err) ->
diff --git a/src/interpreter.ml b/src/interpreter.ml
index be258e0d..59ae4409 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -58,6 +58,7 @@ type gstate =
     boxes : value StringMap.t;
     primops : (value list -> value) StringMap.t;
     letbinds : (Type_check.tannot letbind) list;
+    fundefs : (Type_check.tannot fundef) Bindings.t;
   }
 
 let box_count = ref 0
@@ -76,25 +77,6 @@ type lstate =
 
 type state = lstate * gstate
 
-let rec ast_letbinds (Defs defs) =
-  match defs with
-  | [] -> []
-  | DEF_val lb :: defs -> lb :: ast_letbinds (Defs defs)
-  | _ :: defs -> ast_letbinds (Defs defs)
-
-let initial_gstate ast primops =
-  { registers = Bindings.empty;
-    allow_registers = true;
-    boxes = StringMap.empty;
-    primops = primops;
-    letbinds = ast_letbinds ast;
-  }
-
-let initial_lstate =
-  { locals = Bindings.empty }
-
-let initial_state ast primops = initial_lstate, initial_gstate ast primops
-
 let value_of_lit (L_aux (l_aux, _)) =
   match l_aux with
   | L_unit -> V_unit
@@ -144,11 +126,15 @@ let value_of_exp = function
 (* 1. Interpreter Monad                                                   *)
 (**************************************************************************)
 
+type return_value =
+  | Return_ok of value
+  | Return_exception of value
+
 type 'a response =
   | Early_return of value
   | Exception of value
   | Assertion_failed of string
-  | Call of id * value list * (value -> 'a)
+  | Call of id * value list * (return_value -> 'a)
   | Gets of (state -> 'a)
   | Puts of state * (unit -> 'a)
 
@@ -191,11 +177,11 @@ let catch m =
   | Yield (Exception v) -> Pure (Left v)
   | Yield resp -> Yield (map_response (fun m -> liftM (fun r -> Right r) m) resp)
 
-let call (f : id) (args : value list) : value monad =
-  Yield (Call (f, args, fun v -> Pure v))
-
 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))
 
@@ -348,10 +334,15 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
               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)))
           end
-       | [] -> liftM exp_of_value (call id (List.map value_of_exp evaluated))
+       | [] ->
+          call id (List.map value_of_exp evaluated) >>=
+            (function Return_ok v -> return (exp_of_value v)
+                    | Return_exception v -> wrap (E_throw (exp_of_value v)))
      end
   | E_app_infix (x, id, y) when is_value x && is_value y ->
-     liftM exp_of_value (call id [value_of_exp x; value_of_exp y])
+     call id [value_of_exp x; value_of_exp y] >>=
+       (function Return_ok v -> return (exp_of_value v)
+               | Return_exception v -> wrap (E_throw (exp_of_value v)))
   | E_app_infix (x, id, y) when is_value x ->
      step y >>= fun y' -> wrap (E_app_infix (x, id, y'))
   | E_app_infix (x, id, y) ->
@@ -588,7 +579,7 @@ and exp_of_lexp (LEXP_aux (lexp_aux, _) as lexp) =
   | LEXP_vector_concat (lexp :: lexps) -> mk_exp (E_vector_append (exp_of_lexp lexp, exp_of_lexp (mk_lexp (LEXP_vector_concat lexps))))
   | LEXP_field (lexp, id) -> mk_exp (E_field (exp_of_lexp lexp, id))
 
-and pattern_match env (P_aux (p_aux, _) as pat) value =
+and pattern_match env (P_aux (p_aux, (l, _)) as pat) value =
   match p_aux with
   | P_lit lit -> eq_value (value_of_lit lit) value, Bindings.empty
   | P_wild -> true, Bindings.empty
@@ -627,22 +618,47 @@ and pattern_match env (P_aux (p_aux, _) as pat) value =
   | P_vector pats ->
      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_vector_concat [] -> eq_value (V_vector []) value, Bindings.empty
+  | P_vector_concat (pat :: pats) ->
+     (* We have to use the annotation on each member of the
+        vector_concat pattern to figure out it's length. Due to the
+        recursive call that has an empty_tannot we must not use the
+        annotation in the whole vector_concat pattern. *)
+     let open Type_check in
+     begin match destruct_vector (pat_env_of pat) (pat_typ_of pat) with
+     | Some (Nexp_aux (Nexp_constant n, _), _, _) ->
+        let init, rest = Util.take (Big_int.to_int n) (coerce_gv value), Util.drop (Big_int.to_int n) (coerce_gv value) in
+        let init_match, init_bind = pattern_match env pat (V_vector init) in
+        let rest_match, rest_bind = pattern_match env (P_aux (P_vector_concat pats, (l, empty_tannot))) (V_vector rest) in
+        init_match && rest_match, Bindings.merge combine init_bind rest_bind
+     | _ -> failwith ("Bad vector annotation " ^ string_of_typ (Type_check.pat_typ_of pat))
+     end
   | 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)
-  | P_cons _ -> assert false (* TODO *)
+  | P_cons (hd_pat, tl_pat) ->
+     begin match coerce_cons value with
+     | Some (hd_value, tl_values) ->
+        let hd_match, hd_bind = pattern_match env hd_pat hd_value in
+        let tl_match, tl_bind = pattern_match env tl_pat (V_list tl_values) in
+        hd_match && tl_match, Bindings.merge combine hd_bind tl_bind
+     | None -> failwith "Cannot match cons pattern against non-list"
+     end
+  | P_string_append _ -> assert false (* TODO *)
 
 let exp_of_fundef (FD_aux (FD_function (_, _, _, funcls), annot)) value =
   let pexp_of_funcl (FCL_aux (FCL_Funcl (_, pexp), _)) = pexp in
   E_aux (E_case (exp_of_value value, List.map pexp_of_funcl funcls), annot)
 
-let rec get_fundef id (Defs defs) =
+let rec ast_letbinds (Defs defs) =
   match defs with
-  | [] -> failwith (string_of_id id ^ " definition not found")
-  | (DEF_fundef fdef) :: _ when Id.compare id (id_of_fundef fdef) = 0 -> fdef
-  | _ :: defs -> get_fundef id (Defs defs)
+  | [] -> []
+  | DEF_val lb :: defs -> lb :: ast_letbinds (Defs defs)
+  | _ :: defs -> ast_letbinds (Defs defs)
+
+let initial_lstate =
+  { locals = Bindings.empty }
 
 let stack_cont (_, _, cont) = cont
 let stack_string (str, _, _) = str
@@ -650,41 +666,78 @@ let stack_state (_, lstate, _) = lstate
 
 type frame =
   | Done of state * value
-  | Step of string Lazy.t * state * (Type_check.tannot exp) monad * (string Lazy.t * lstate * (value -> (Type_check.tannot exp) monad)) list
+  | Step of string Lazy.t * state * (Type_check.tannot exp) monad * (string Lazy.t * lstate * (return_value -> (Type_check.tannot exp) monad)) list
   | Break of frame
 
-let rec eval_frame' ast = function
+let rec eval_frame' = function
   | Done (state, v) -> Done (state, v)
   | Break frame -> Break frame
   | Step (out, state, m, stack) ->
      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 (value_of_exp v), stack')
+        Step (stack_string head, (stack_state head, snd state), 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 (get_fundef id ast) arg 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))
      | 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 (get_fundef id ast) arg 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' ast (Step (out, state, cont state, stack))
+        eval_frame' (Step (out, state, cont state, stack))
      | Yield (Puts (state', cont)), _ ->
-        eval_frame' ast (Step (out, state', cont (), stack))
+        eval_frame' (Step (out, state', cont (), 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 v, stack')
+        Step (stack_string head, (stack_state head, snd state), stack_cont head (Return_ok v), stack')
      | Yield (Assertion_failed msg), _ ->
         failwith msg
-     | Yield (Exception v), _ ->
+     | 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')
 
-let eval_frame ast frame =
-  try eval_frame' ast frame with
+let eval_frame frame =
+  try eval_frame' frame with
   | Type_check.Type_error (l, err) ->
      raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))
+
+let rec run_frame frame =
+  match frame with
+  | Done (state, v) -> v
+  | Step (lazy_str, _, _, _) ->
+     run_frame (eval_frame frame)
+  | Break frame ->
+     run_frame (eval_frame frame)
+
+let eval_exp state exp =
+  run_frame (Step (lazy "", state, return exp, []))
+
+let initial_gstate primops ast =
+  { registers = Bindings.empty;
+    allow_registers = true;
+    boxes = StringMap.empty;
+    primops = primops;
+    letbinds = ast_letbinds ast;
+    fundefs = Bindings.empty;
+  }
+
+let rec initialize_registers gstate =
+  let process_def = function
+    | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) ->
+       { gstate with registers = Bindings.add id (eval_exp (initial_lstate, gstate) exp) gstate.registers }
+    | DEF_fundef fdef ->
+       { gstate with fundefs = Bindings.add (id_of_fundef fdef) fdef gstate.fundefs }
+    | _ -> gstate
+  in
+  function
+  | Defs (def :: defs) ->
+     initialize_registers (process_def def) (Defs defs)
+  | Defs [] -> gstate
+
+let initial_state ast primops = initial_lstate, initialize_registers (initial_gstate primops ast) ast
diff --git a/src/isail.ml b/src/isail.ml
index 60c35ca7..84b614a9 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -129,7 +129,7 @@ let rec run () =
        | Step (out, state, _, stack) ->
           begin
             try
-              current_mode := Evaluation (eval_frame !interactive_ast frame)
+              current_mode := Evaluation (eval_frame frame)
             with
             | Failure str -> print_endline str; current_mode := Normal
           end;
@@ -154,7 +154,7 @@ let rec run_steps n =
        | Step (out, state, _, stack) ->
           begin
             try
-              current_mode := Evaluation (eval_frame !interactive_ast frame)
+              current_mode := Evaluation (eval_frame frame)
             with
             | Failure str -> print_endline str; current_mode := Normal
           end;
@@ -331,7 +331,7 @@ let handle_input' input =
           (* An expression in normal mode is type checked, then puts
              us in evaluation mode. *)
           let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord str) in
-          current_mode := Evaluation (eval_frame !interactive_ast (Step (lazy "", !interactive_state, return exp, [])));
+          current_mode := Evaluation (eval_frame (Step (lazy "", !interactive_state, return exp, [])));
           print_program ()
        | Empty -> ()
      end
@@ -365,7 +365,7 @@ let handle_input' input =
                begin
                  try
                    interactive_state := state;
-                   current_mode := Evaluation (eval_frame !interactive_ast frame);
+                   current_mode := Evaluation (eval_frame frame);
                    print_program ()
                  with
                  | Failure str -> print_endline str; current_mode := Normal
diff --git a/src/rewrites.ml b/src/rewrites.ml
index b032e3ec..e17976c3 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -4616,7 +4616,6 @@ let rewrite_defs_interpreter = [
     ("vector_concat_assignments", rewrite_vector_concat_assignments);
     ("tuple_assignments", rewrite_tuple_assignments);
     ("simple_assignments", rewrite_simple_assignments);
-    ("remove_vector_concat", rewrite_defs_remove_vector_concat);
     ("constraint", rewrite_constraint);
     ("trivial_sizeof", rewrite_trivial_sizeof);
     ("sizeof", rewrite_sizeof);
diff --git a/src/sail.ml b/src/sail.ml
index b172a482..12df5515 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -82,6 +82,9 @@ let options = Arg.align ([
     Arg.Tuple [Arg.Set opt_interactive; Arg.Set Initial_check.opt_undefined_gen;
                Arg.String (fun s -> opt_interactive_script := Some s)],
     "<filename> start interactive interpreter and execute commands in script");
+  ( "-iout",
+    Arg.String (fun file -> Value.output_redirect (open_out file)),
+    "<filename> print interpreter output to file");
   ( "-no_warn",
     Arg.Clear Util.opt_warnings,
     " do not print warnings");
diff --git a/src/value.ml b/src/value.ml
index c00b9687..cb55aa79 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -65,6 +65,10 @@ let output_close () =
   else
     ()
 
+let output str =
+  output_string !print_chan str;
+  flush !print_chan
+
 let output_endline str =
   output_string !print_chan (str ^ "\n");
   flush !print_chan
@@ -83,6 +87,24 @@ type value =
   | V_ctor of string * value list
   | V_record of value StringMap.t
 
+let rec eq_value v1 v2 =
+  match v1, v2 with
+  | V_vector v1s, V_vector v2s when List.length v1s = List.length v2s -> List.for_all2 eq_value v1s v2s
+  | V_list v1s, V_vector v2s when List.length v1s = List.length v2s -> List.for_all2 eq_value v1s v2s
+  | V_int n, V_int m -> Big_int.equal n m
+  | V_real n, V_real m -> Rational.equal n m
+  | V_bool b1, V_bool b2 -> b1 = b2
+  | V_bit b1, V_bit b2 -> b1 = b2
+  | V_tuple v1s, V_tuple v2s when List.length v1s = List.length v2s -> List.for_all2 eq_value v1s v2s
+  | V_unit, V_unit -> true
+  | V_string str1, V_string str2 -> str1 = str2
+  | V_ref str1, V_ref str2 -> str1 = str2
+  | V_ctor (name1, fields1), V_ctor (name2, fields2) when List.length fields1 = List.length fields2 ->
+     name1 = name2 && List.for_all2 eq_value fields1 fields2
+  | V_record fields1, V_record fields2 ->
+     StringMap.equal eq_value fields1 fields2
+  | _, _ -> false
+
 let coerce_bit = function
   | V_bit b -> b
   | _ -> assert false
@@ -338,7 +360,6 @@ let is_bit = function
   | V_bit _ -> true
   | _ -> false
 
-
 let is_ctor = function
   | V_ctor _ -> true
   | _ -> false
@@ -385,13 +406,16 @@ let value_vector_truncate = function
   | [v1; v2] -> mk_vector (Sail_lib.vector_truncate (coerce_bv v1, coerce_int v2))
   | _ -> failwith "value vector_truncate"
 
-let eq_value v1 v2 = string_of_value v1 = string_of_value v2
-
 let value_eq_anything = function
   | [v1; v2] -> V_bool (eq_value v1 v2)
   | _ -> failwith "value eq_anything"
 
 let value_print = function
+  | [V_string str] -> output str; V_unit
+  | [v] -> output (string_of_value v |> Util.red |> Util.clear); V_unit
+  | _ -> assert false
+
+let value_print_endline = function
   | [V_string str] -> output_endline str; V_unit
   | [v] -> output_endline (string_of_value v |> Util.red |> Util.clear); V_unit
   | _ -> assert false
@@ -496,9 +520,9 @@ let primops =
     [ ("and_bool", and_bool);
       ("or_bool", or_bool);
       ("print", value_print);
-      ("prerr", fun vs -> (prerr_endline (string_of_value (List.hd vs)); V_unit));
+      ("prerr", fun vs -> (prerr_string (string_of_value (List.hd vs)); V_unit));
       ("dec_str", fun _ -> V_string "X");
-      ("print_endline", value_print);
+      ("print_endline", value_print_endline);
       ("prerr_endline", fun vs -> (prerr_endline (string_of_value (List.hd vs)); V_unit));
       ("putchar", value_putchar);
       ("string_of_int", fun vs -> V_string (string_of_value (List.hd vs)));