summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/constant_fold.ml10
-rw-r--r--src/interpreter.ml6
-rw-r--r--src/isail.ml12
-rw-r--r--src/process_file.ml8
-rw-r--r--src/process_file.mli16
-rw-r--r--src/sail.ml14
6 files changed, 34 insertions, 32 deletions
diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index 407bd69a..d5fffbbe 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -141,13 +141,13 @@ let rec run frame =
- Throws an exception that isn't caught.
*)
-let rec rewrite_constant_function_calls' ast =
+let rec rewrite_constant_function_calls' env ast =
let rewrite_count = ref 0 in
let ok () = incr rewrite_count in
let not_ok () = decr rewrite_count in
let lstate, gstate =
- Interpreter.initial_state ast safe_primops
+ Interpreter.initial_state ast env safe_primops
in
let gstate = { gstate with Interpreter.allow_registers = false } in
@@ -202,11 +202,11 @@ let rec rewrite_constant_function_calls' ast =
let ast = rewrite_defs_base rw_defs ast in
(* We keep iterating until we have no more re-writes to do *)
if !rewrite_count > 0
- then rewrite_constant_function_calls' ast
+ then rewrite_constant_function_calls' env ast
else ast
-let rewrite_constant_function_calls ast =
+let rewrite_constant_function_calls env ast =
if !optimize_constant_fold then
- rewrite_constant_function_calls' ast
+ rewrite_constant_function_calls' env ast
else
ast
diff --git a/src/interpreter.ml b/src/interpreter.ml
index b2b91583..167c66f5 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -61,6 +61,7 @@ type gstate =
letbinds : (Type_check.tannot letbind) list;
fundefs : (Type_check.tannot fundef) Bindings.t;
last_write_ea : (value * value * value) option;
+ typecheck_env : Type_check.Env.t;
}
type lstate =
@@ -964,13 +965,14 @@ let rec run_frame frame =
let eval_exp state exp =
run_frame (Step (lazy "", state, return exp, []))
-let initial_gstate primops ast =
+let initial_gstate primops ast env =
{ registers = Bindings.empty;
allow_registers = true;
primops = primops;
letbinds = ast_letbinds ast;
fundefs = Bindings.empty;
last_write_ea = None;
+ typecheck_env = env;
}
let rec initialize_registers gstate =
@@ -994,4 +996,4 @@ let rec initialize_registers gstate =
initialize_registers (process_def def) (Defs defs)
| Defs [] -> gstate
-let initial_state ast primops = initial_lstate, initialize_registers (initial_gstate primops ast) ast
+let initial_state ast env primops = initial_lstate, initialize_registers (initial_gstate primops ast env) ast
diff --git a/src/isail.ml b/src/isail.ml
index bdf4777d..863c4b1c 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -103,7 +103,7 @@ let sail_logo =
let vs_ids = ref (Initial_check.val_spec_ids !interactive_ast)
-let interactive_state = ref (initial_state !interactive_ast Value.primops)
+let interactive_state = ref (initial_state !interactive_ast !interactive_env Value.primops)
let print_program () =
match !current_mode with
@@ -301,13 +301,13 @@ let handle_input' input =
let ast, env = Specialize.specialize !interactive_ast !interactive_env in
interactive_ast := ast;
interactive_env := env;
- interactive_state := initial_state !interactive_ast Value.primops
+ interactive_state := initial_state !interactive_ast !interactive_env Value.primops
| ":pretty" ->
print_endline (Pretty_print_sail.to_string (Latex.latex_defs "sail_latex" !interactive_ast))
| ":bytecode" ->
let open PPrint in
let open C_backend in
- let ast = Process_file.rewrite_ast_c !interactive_ast in
+ let ast = Process_file.rewrite_ast_c !interactive_env !interactive_ast in
let ast, env = Specialize.specialize ast !interactive_env in
let ctx = initial_ctx env in
let byte_ast = bytecode_ast ctx (List.map flatten_instrs) ast in
@@ -351,15 +351,15 @@ let handle_input' input =
| ":l" | ":load" ->
let files = Util.split_on_char ' ' arg in
let (_, ast, env) = load_files !interactive_env files in
- let ast = Process_file.rewrite_ast_interpreter ast in
+ let ast = Process_file.rewrite_ast_interpreter env ast in
interactive_ast := append_ast !interactive_ast ast;
- interactive_state := initial_state !interactive_ast Value.primops;
+ interactive_state := initial_state !interactive_ast !interactive_env Value.primops;
interactive_env := env;
vs_ids := Initial_check.val_spec_ids !interactive_ast
| ":u" | ":unload" ->
interactive_ast := Ast.Defs [];
interactive_env := Type_check.initial_env;
- interactive_state := initial_state !interactive_ast Value.primops;
+ interactive_state := initial_state !interactive_ast !interactive_env Value.primops;
vs_ids := Initial_check.val_spec_ids !interactive_ast;
(* See initial_check.mli for an explanation of why we need this. *)
Initial_check.have_undefined_builtins := false
diff --git a/src/process_file.ml b/src/process_file.ml
index 2dfd9571..344c7921 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -375,7 +375,7 @@ let rewrite_step defs (name,rewriter) =
| _ -> () in
defs
-let rewrite rewriters defs =
+let rewrite rewriters env defs =
try List.fold_left rewrite_step defs rewriters with
| Type_check.Type_error (l, err) ->
raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))
@@ -385,10 +385,10 @@ let rewrite_undefined bitvectors = rewrite [("undefined", fun x -> Rewrites.rewr
let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem
let rewrite_ast_coq = rewrite Rewrites.rewrite_defs_coq
let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml
-let rewrite_ast_c ast =
+let rewrite_ast_c env ast =
ast
- |> rewrite Rewrites.rewrite_defs_c
- |> rewrite [("constant_fold", Constant_fold.rewrite_constant_function_calls)]
+ |> rewrite Rewrites.rewrite_defs_c env
+ |> rewrite [("constant_fold", Constant_fold.rewrite_constant_function_calls env)] env
let rewrite_ast_interpreter = rewrite Rewrites.rewrite_defs_interpreter
let rewrite_ast_check = rewrite Rewrites.rewrite_defs_check
diff --git a/src/process_file.mli b/src/process_file.mli
index 1ebb3014..7862c121 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -55,14 +55,14 @@ val parse_file : ?loc:Parse_ast.l -> string -> Parse_ast.defs
val convert_ast : Ast.order -> Parse_ast.defs -> unit Ast.defs
val preprocess_ast : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.defs -> Parse_ast.defs
val check_ast: Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
-val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_undefined: bool -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_coq : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_c : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_interpreter : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_check : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast: Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_undefined: bool -> Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_lem : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_coq : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_ocaml : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_c : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_interpreter : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_check : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val load_file_no_check : (Arg.key * Arg.spec * Arg.doc) list -> Ast.order -> string -> unit Ast.defs
val load_file : (Arg.key * Arg.spec * Arg.doc) list -> Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t
diff --git a/src/sail.ml b/src/sail.ml
index c1c965fe..2748cb81 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -271,7 +271,7 @@ let load_files type_envs files =
let (ast, type_envs) = check_ast type_envs ast in
- let ast = rewrite_ast ast in
+ let ast = rewrite_ast type_envs ast in
let out_name = match !opt_file_out with
| None when parsed = [] -> "out.sail"
@@ -316,11 +316,11 @@ let main() =
begin
(if !(opt_interactive)
then
- (interactive_ast := Process_file.rewrite_ast_interpreter ast; interactive_env := type_envs)
+ (interactive_ast := Process_file.rewrite_ast_interpreter type_envs ast; interactive_env := type_envs)
else ());
(if !(opt_sanity)
then
- let _ = rewrite_ast_check ast in
+ let _ = rewrite_ast_check type_envs ast in
()
else ());
(if !(opt_print_verbose)
@@ -328,13 +328,13 @@ let main() =
else ());
(if !(opt_print_ocaml)
then
- let ast_ocaml = rewrite_ast_ocaml ast in
+ let ast_ocaml = rewrite_ast_ocaml type_envs ast in
let out = match !opt_file_out with None -> "out" | Some s -> s in
Ocaml_backend.ocaml_compile out ast_ocaml ocaml_generator_info
else ());
(if !(opt_print_c)
then
- let ast_c = rewrite_ast_c ast in
+ let ast_c = rewrite_ast_c type_envs ast in
let ast_c, type_envs = Specialize.specialize ast_c type_envs in
let ast_c = Spec_analysis.top_sort_defs ast_c in
Util.opt_warnings := true;
@@ -344,13 +344,13 @@ let main() =
then
let mwords = !Pretty_print_lem.opt_mwords in
let type_envs, ast_lem = State.add_regstate_defs mwords type_envs ast in
- let ast_lem = rewrite_ast_lem ast_lem in
+ let ast_lem = rewrite_ast_lem type_envs ast_lem in
output "" (Lem_out (!opt_libs_lem)) [out_name,ast_lem]
else ());
(if !(opt_print_coq)
then
let type_envs, ast_coq = State.add_regstate_defs true type_envs ast in
- let ast_coq = rewrite_ast_coq ast_coq in
+ let ast_coq = rewrite_ast_coq type_envs ast_coq in
output "" (Coq_out (!opt_libs_coq)) [out_name,ast_coq]
else ());
(if !(opt_print_latex)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 08:19:57 +0000