summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml2
-rw-r--r--src/constant_fold.ml8
-rw-r--r--src/interpreter.ml139
-rw-r--r--src/isail.ml8
-rw-r--r--src/rewrites.ml1
-rw-r--r--src/sail.ml3
-rw-r--r--src/value.ml34
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)));
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-12 23:23:21 +0000