summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/isail.ml119
-rw-r--r--src/rewrites.ml191
-rw-r--r--src/rewrites.mli18
-rw-r--r--src/sail.ml3
-rw-r--r--src/slice.ml15
-rw-r--r--src/slice.mli2
6 files changed, 257 insertions, 91 deletions
diff --git a/src/isail.ml b/src/isail.ml
index 3eea268d..0b8d4b84 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -233,6 +233,18 @@ let rec emacs_error l contents =
| Parse_ast.Documented (_, l) -> emacs_error l contents
| Parse_ast.Generated l -> emacs_error l contents
+module SliceNodeSet = Set.Make(Slice.Node)
+let slice_roots = ref SliceNodeSet.empty
+let slice_cuts = ref SliceNodeSet.empty
+
+let rec describe_rewrite =
+ let open Rewrites in
+ function
+ | String_rewriter rw -> "<string>" :: describe_rewrite (rw "")
+ | Bool_rewriter rw -> "<bool>" :: describe_rewrite (rw false)
+ | Literal_rewriter rw -> "<ocaml/lem/all>" :: describe_rewrite (rw (fun _ -> true))
+ | Basic_rewriter rw -> []
+
type session = {
id : string;
files : string list
@@ -434,6 +446,55 @@ let handle_input' input =
Interactive.ast := append_ast !Interactive.ast ast;
Interactive.env := env;
interactive_state := initial_state !Interactive.ast Value.primops;
+ | ":graph" ->
+ let format = if arg = "" then "svg" else arg in
+ let dotfile, out_chan = Filename.open_temp_file "sail_graph_" ".gz" in
+ let image = Filename.temp_file "sail_graph_" ("." ^ format) in
+ Slice.dot_of_ast out_chan !Interactive.ast;
+ close_out out_chan;
+ let _ = Unix.system (Printf.sprintf "dot -T%s %s -o %s" format dotfile image) in
+ let _ = Unix.system (Printf.sprintf "xdg-open %s" image) in
+ ()
+ | ":slice_roots" ->
+ let args = Str.split (Str.regexp " +") arg in
+ let ids = List.map (fun str -> Slice.Function (mk_id str)) args |> SliceNodeSet.of_list in
+ slice_roots := SliceNodeSet.union ids !slice_roots
+ | ":slice_cuts" ->
+ let args = Str.split (Str.regexp " +") arg in
+ let ids = List.map (fun str -> Slice.Function (mk_id str)) args |> SliceNodeSet.of_list in
+ slice_cuts := SliceNodeSet.union ids !slice_cuts
+ | ":slice" ->
+ let module G = Graph.Make(Slice.Node) in
+ let g = Slice.graph_of_ast !Interactive.ast in
+ let g = G.prune !slice_roots !slice_cuts g in
+ Interactive.ast := Slice.filter_ast g !Interactive.ast
+ | ":list_rewrites" ->
+ List.iter print_endline (List.map fst Rewrites.all_rewrites)
+ | ":rewrite" ->
+ let open Rewrites in
+ let args = Str.split (Str.regexp " +") arg in
+ let rec parse_args rw args =
+ match rw, args with
+ | Basic_rewriter rw, [] -> rw
+ | Bool_rewriter rw, arg :: args -> parse_args (rw (bool_of_string arg)) args
+ | String_rewriter rw, arg :: args -> parse_args (rw arg) args
+ | Literal_rewriter rw, arg :: args ->
+ begin match arg with
+ | "ocaml" -> parse_args (rw rewrite_lit_ocaml) args
+ | "lem" -> parse_args (rw rewrite_lit_lem) args
+ | "all" -> parse_args (rw (fun _ -> true)) args
+ | _ -> failwith "target for literal rewrite must be one of ocaml/lem/all"
+ end
+ | _, _ -> failwith "Invalid arguments to rewrite"
+ in
+ begin match args with
+ | rw :: args ->
+ let rw = List.assoc rw Rewrites.all_rewrites in
+ let rw = parse_args rw args in
+ Interactive.ast := rw !Interactive.env !Interactive.ast
+ | [] ->
+ failwith "Must provide the name of a rewrite, use :list_rewrites for a list of possible rewrites"
+ end
| _ -> unrecognised_command cmd
end
| Expression str ->
@@ -539,6 +600,8 @@ let handle_input' input =
let handle_input input =
try handle_input' input with
+ | Failure str ->
+ print_endline ("Error: " ^ str)
| Type_check.Type_error (env, l, err) ->
print_endline (Type_error.string_of_type_error err)
| Reporting.Fatal_error err ->
@@ -547,7 +610,7 @@ let handle_input input =
print_endline (Printexc.to_string exn)
let () =
- (* Auto complete function names based on val specs, or directories if :load command *)
+ (* Auto complete function names based on val specs, directories if :load command, or rewrites if :rewrite command *)
LNoise.set_completion_callback (
fun line_so_far ln_completions ->
let line_so_far, last_id =
@@ -561,31 +624,36 @@ let () =
let n = try String.index line_so_far ' ' with Not_found -> String.length line_so_far in
let cmd = Str.string_before line_so_far n in
if last_id <> "" then
- if cmd = ":load" || cmd = ":l" then
- begin
- let dirname, basename = Filename.dirname last_id, Filename.basename last_id in
- if Sys.file_exists last_id then
- LNoise.add_completion ln_completions (line_so_far ^ last_id);
- if (try Sys.is_directory dirname with Sys_error _ -> false) then
- let contents = Sys.readdir (Filename.concat (Sys.getcwd ()) dirname) in
- for i = 0 to Array.length contents - 1 do
- if Str.string_match (Str.regexp_string basename) contents.(i) 0 then
- let is_dir = (try Sys.is_directory (Filename.concat dirname contents.(i)) with Sys_error _ -> false) in
- LNoise.add_completion ln_completions
- (line_so_far ^ Filename.concat dirname contents.(i) ^ (if is_dir then Filename.dir_sep else ""))
- done
- end
- else if cmd = ":option" then
- List.map (fun (opt, _, _) -> opt) options
- |> List.filter (fun opt -> Str.string_match (Str.regexp_string last_id) opt 0)
- |> List.map (fun completion -> line_so_far ^ completion)
- |> List.iter (LNoise.add_completion ln_completions)
- else
+ begin match cmd with
+ | ":load" | ":l" ->
+ let dirname, basename = Filename.dirname last_id, Filename.basename last_id in
+ if Sys.file_exists last_id then
+ LNoise.add_completion ln_completions (line_so_far ^ last_id);
+ if (try Sys.is_directory dirname with Sys_error _ -> false) then
+ let contents = Sys.readdir (Filename.concat (Sys.getcwd ()) dirname) in
+ for i = 0 to Array.length contents - 1 do
+ if Str.string_match (Str.regexp_string basename) contents.(i) 0 then
+ let is_dir = (try Sys.is_directory (Filename.concat dirname contents.(i)) with Sys_error _ -> false) in
+ LNoise.add_completion ln_completions
+ (line_so_far ^ Filename.concat dirname contents.(i) ^ (if is_dir then Filename.dir_sep else ""))
+ done
+ | ":rewrite" ->
+ List.map fst Rewrites.all_rewrites
+ |> List.filter (fun opt -> Str.string_match (Str.regexp_string last_id) opt 0)
+ |> List.map (fun completion -> line_so_far ^ completion)
+ |> List.iter (LNoise.add_completion ln_completions)
+ | ":option" ->
+ List.map (fun (opt, _, _) -> opt) options
+ |> List.filter (fun opt -> Str.string_match (Str.regexp_string last_id) opt 0)
+ |> List.map (fun completion -> line_so_far ^ completion)
+ |> List.iter (LNoise.add_completion ln_completions)
+ | _ ->
IdSet.elements !vs_ids
|> List.map string_of_id
|> List.filter (fun id -> Str.string_match (Str.regexp_string last_id) id 0)
|> List.map (fun completion -> line_so_far ^ completion)
|> List.iter (LNoise.add_completion ln_completions)
+ end
else ()
);
@@ -605,6 +673,15 @@ let () =
| str ->
let args = Str.split (Str.regexp " +") str in
match args with
+ | [":rewrite"] -> hint "<rewrite>"
+ | ":rewrite" :: rw :: args ->
+ begin match List.assoc_opt rw Rewrites.all_rewrites with
+ | Some rw ->
+ let hints = describe_rewrite rw in
+ let hints = Util.drop (List.length args) hints in
+ (match hints with [] -> None | _ -> hint (String.concat " " hints))
+ | None -> None
+ end
| [":option"] -> hint "<flag>"
| [":option"; flag] ->
begin match List.find_opt (fun (opt, _, _) -> flag = opt) options with
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 502b910c..21422fe2 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -4047,7 +4047,6 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
in
Defs (List.map rewrite_def defs |> List.flatten)
-
(* Rewrite to make all pattern matches in Coq output exhaustive.
Assumes that guards, vector patterns, etc have been rewritten already,
and the scattered functions have been merged.
@@ -4761,78 +4760,138 @@ let rewrite_defs_coq = [
("recheck_defs", recheck_defs)
]
-let rewrite_defs_ocaml = [
- (* ("undefined", rewrite_undefined); *)
- ("no_effect_check", (fun _ defs -> opt_no_effects := true; defs));
- ("realise_mappings", rewrite_defs_realise_mappings);
- ("toplevel_string_append", rewrite_defs_toplevel_string_append);
- ("pat_string_append", rewrite_defs_pat_string_append);
- ("mapping_builtins", rewrite_defs_mapping_patterns);
- ("rewrite_undefined", rewrite_undefined_if_gen false);
- ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list);
- ("pat_lits", rewrite_defs_pat_lits rewrite_lit_ocaml);
- ("vector_concat_assignments", rewrite_vector_concat_assignments);
- ("tuple_assignments", rewrite_tuple_assignments);
- ("simple_assignments", rewrite_simple_assignments);
- ("remove_not_pats", rewrite_defs_not_pats);
- ("remove_vector_concat", rewrite_defs_remove_vector_concat);
- ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats);
- ("remove_numeral_pats", rewrite_defs_remove_numeral_pats);
- ("exp_lift_assign", rewrite_defs_exp_lift_assign);
- ("top_sort_defs", fun _ -> top_sort_defs);
- ("simple_types", rewrite_simple_types);
- ("overload_cast", rewrite_overload_cast);
- (* ("separate_numbs", rewrite_defs_separate_numbs) *)
+type rewriter =
+ | Basic_rewriter of (Env.t -> tannot defs -> tannot defs)
+ | Bool_rewriter of (bool -> rewriter)
+ | String_rewriter of (string -> rewriter)
+ | Literal_rewriter of ((lit -> bool) -> rewriter)
+
+type rewriter_arg =
+ | If_mono_arg
+ | Bool_arg of bool
+ | String_arg of string
+ | Literal_arg of string
+
+let instantiate_rewrite rewriter args =
+ let selector_function = function
+ | "ocaml" -> rewrite_lit_ocaml
+ | "lem" -> rewrite_lit_lem
+ | "all" -> (fun _ -> true)
+ | arg ->
+ raise (Reporting.err_general Parse_ast.Unknown ("No rewrite for literal target \"" ^ arg ^ "\", valid targets are ocaml/lem/all"))
+ in
+ let instantiate rewriter arg =
+ match rewriter, arg with
+ | Basic_rewriter rw, If_mono_arg -> Basic_rewriter (if_mono rw)
+ | Bool_rewriter rw, Bool_arg b -> rw b
+ | String_rewriter rw, String_arg str -> rw str
+ | Literal_rewriter rw, Literal_arg selector -> rw (selector_function selector)
+ | _, _ ->
+ raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Invalid rewrite argument")
+ in
+ match List.fold_left instantiate rewriter args with
+ | Basic_rewriter rw -> rw
+ | _ ->
+ raise (Reporting.err_general Parse_ast.Unknown "Rewrite not fully instantiated")
+
+let all_rewrites = [
+ ("no_effect_check", Basic_rewriter (fun _ defs -> opt_no_effects := true; defs));
+ ("recheck_defs", Basic_rewriter recheck_defs);
+ ("optimize_recheck_defs", Basic_rewriter (fun _ -> Optimize.recheck));
+ ("realise_mappings", Basic_rewriter rewrite_defs_realise_mappings);
+ ("toplevel_string_append", Basic_rewriter rewrite_defs_toplevel_string_append);
+ ("pat_string_append", Basic_rewriter rewrite_defs_pat_string_append);
+ ("mapping_builtins", Basic_rewriter rewrite_defs_mapping_patterns);
+ ("mono_rewrites", Basic_rewriter mono_rewrites);
+ ("toplevel_nexps", Basic_rewriter rewrite_toplevel_nexps);
+ ("monomorphise", Basic_rewriter monomorphise);
+ ("atoms_to_singletons", Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons));
+ ("undefined", Bool_rewriter (fun b -> Basic_rewriter (rewrite_undefined_if_gen b)));
+ ("vector_string_pats_to_bit_list", Basic_rewriter rewrite_defs_vector_string_pats_to_bit_list);
+ ("remove_not_pats", Basic_rewriter rewrite_defs_not_pats);
+ ("pattern_literals", Literal_rewriter (fun f -> Basic_rewriter (rewrite_defs_pat_lits f)));
+ ("vector_concat_assignments", Basic_rewriter rewrite_vector_concat_assignments);
+ ("tuple_assignments", Basic_rewriter rewrite_tuple_assignments);
+ ("simple_assignments", Basic_rewriter rewrite_simple_assignments);
+ ("remove_vector_concat", Basic_rewriter rewrite_defs_remove_vector_concat);
+ ("remove_bitvector_pats", Basic_rewriter rewrite_defs_remove_bitvector_pats);
+ ("remove_numeral_pats", Basic_rewriter rewrite_defs_remove_numeral_pats);
+ ("exp_lift_assign", Basic_rewriter rewrite_defs_exp_lift_assign);
+ ("merge_function_clauses", Basic_rewriter merge_funcls);
+ ("simple_types", Basic_rewriter rewrite_simple_types);
+ ("overload_cast", Basic_rewriter rewrite_overload_cast);
+ ("top_sort_defs", Basic_rewriter (fun _ -> top_sort_defs));
+ ("split", String_rewriter (fun str -> Basic_rewriter (rewrite_split_fun_ctor_pats str)))
]
-let opt_separate_execute = ref false
-
-let if_separate f env defs =
- if !opt_separate_execute then f env defs else defs
+let rewriters_ocaml = [
+ ("no_effect_check", []);
+ ("realise_mappings", []);
+ ("toplevel_string_append", []);
+ ("pat_string_append", []);
+ ("mapping_builtins", []);
+ ("undefined", [Bool_arg false]);
+ ("vector_string_pats_to_bit_list", []);
+ ("pattern_literals", [Literal_arg "ocaml"]);
+ ("vector_concat_assignments", []);
+ ("tuple_assignments", []);
+ ("simple_assignments", []);
+ ("remove_not_pats", []);
+ ("remove_vector_concat", []);
+ ("remove_bitvector_pats", []);
+ ("remove_numeral_pats", []);
+ ("exp_lift_assign", []);
+ ("top_sort_defs", []);
+ ("simple_types", []);
+ ("overload_cast", [])
+ ]
-let rewrite_defs_c = [
- ("no_effect_check", (fun _ defs -> opt_no_effects := true; defs));
+let rewriters_c = [
+ ("no_effect_check", []);
+ ("realise_mappings", []);
+ ("toplevel_string_append", []);
+ ("pat_string_append", []);
+ ("mapping_builtins", []);
+ ("mono_rewrites", [If_mono_arg]);
+ ("recheck_defs", [If_mono_arg]);
+ ("toplevel_nexps", [If_mono_arg]);
+ ("monomorphise", [If_mono_arg]);
+ ("atoms_to_singletons", [If_mono_arg]);
+ ("recheck_defs", [If_mono_arg]);
+ ("undefined", [Bool_arg false]);
+ ("vector_string_pats_to_bit_list", []);
+ ("remove_not_pats", []);
+ ("pattern_literals", [Literal_arg "all"]);
+ ("vector_concat_assignments", []);
+ ("tuple_assignments", []);
+ ("simple_assignments", []);
+ ("remove_vector_concat", []);
+ ("remove_bitvector_pats", []);
+ ("exp_lift_assign", []);
+ ("merge_function_clauses", []);
+ ("optimize_recheck_defs", [])
+ ]
- (* Remove bidirectional mappings *)
- ("realise_mappings", rewrite_defs_realise_mappings);
- ("toplevel_string_append", rewrite_defs_toplevel_string_append);
- ("pat_string_append", rewrite_defs_pat_string_append);
- ("mapping_builtins", rewrite_defs_mapping_patterns);
+let rewriters_interpreter = [
+ ("no_effect_check", []);
+ ("realise_mappings", []);
+ ("toplevel_string_append", []);
+ ("pat_string_append", []);
+ ("mapping_builtins", []);
+ ("undefined", [Bool_arg false]);
+ ("vector_concat_assignments", []);
+ ("tuple_assignments", []);
+ ("simple_assignments", [])
+ ]
- (* Monomorphisation *)
- ("mono_rewrites", if_mono mono_rewrites);
- ("recheck_defs", if_mono recheck_defs);
- ("rewrite_toplevel_nexps", if_mono rewrite_toplevel_nexps);
- ("monomorphise", if_mono monomorphise);
- ("rewrite_atoms_to_singletons", if_mono (fun _ -> Monomorphise.rewrite_atoms_to_singletons));
- ("recheck_defs", if_mono recheck_defs);
+let rewrite_defs_ocaml =
+ List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) rewriters_ocaml
- ("rewrite_undefined", rewrite_undefined_if_gen false);
- ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list);
- ("remove_not_pats", rewrite_defs_not_pats);
- ("pat_lits", rewrite_defs_pat_lits (fun _ -> true));
- ("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);
- ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats);
- ("split_execute", if_separate (rewrite_split_fun_ctor_pats "execute"));
- ("exp_lift_assign", rewrite_defs_exp_lift_assign);
- ("merge_function_clauses", merge_funcls);
- ("recheck_defs", fun _ -> Optimize.recheck)
- ]
+let rewrite_defs_c =
+ List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) rewriters_c
-let rewrite_defs_interpreter = [
- ("no_effect_check", (fun _ defs -> opt_no_effects := true; defs));
- ("realise_mappings", rewrite_defs_realise_mappings);
- ("toplevel_string_append", rewrite_defs_toplevel_string_append);
- ("pat_string_append", rewrite_defs_pat_string_append);
- ("mapping_builtins", rewrite_defs_mapping_patterns);
- ("rewrite_undefined", rewrite_undefined_if_gen false);
- ("vector_concat_assignments", rewrite_vector_concat_assignments);
- ("tuple_assignments", rewrite_tuple_assignments);
- ("simple_assignments", rewrite_simple_assignments)
- ]
+let rewrite_defs_interpreter =
+ List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) rewriters_interpreter
let rewrite_check_annot =
let check_annot exp =
diff --git a/src/rewrites.mli b/src/rewrites.mli
index 811d52e8..f5b26f3a 100644
--- a/src/rewrites.mli
+++ b/src/rewrites.mli
@@ -59,7 +59,6 @@ val opt_dmono_analysis : int ref
val opt_auto_mono : bool ref
val opt_dall_split_errors : bool ref
val opt_dmono_continue : bool ref
-val opt_separate_execute : bool ref
(* Generate a fresh id with the given prefix *)
val fresh_id : string -> l -> id
@@ -79,6 +78,23 @@ val rewrite_defs_lem : (string * (Env.t -> tannot defs -> tannot defs)) list
(* Perform rewrites to exclude AST nodes not supported for coq out*)
val rewrite_defs_coq : (string * (Env.t -> tannot defs -> tannot defs)) list
+type rewriter =
+ | Basic_rewriter of (Env.t -> tannot defs -> tannot defs)
+ | Bool_rewriter of (bool -> rewriter)
+ | String_rewriter of (string -> rewriter)
+ | Literal_rewriter of ((lit -> bool) -> rewriter)
+
+val rewrite_lit_ocaml : lit -> bool
+val rewrite_lit_lem : lit -> bool
+
+type rewriter_arg =
+ | If_mono_arg
+ | Bool_arg of bool
+ | String_arg of string
+ | Literal_arg of string
+
+val all_rewrites : (string * rewriter) list
+
(* Warn about matches where we add a default case for Coq because they're not
exhaustive *)
val opt_coq_warn_nonexhaustive : bool ref
diff --git a/src/sail.ml b/src/sail.ml
index 7da36dd9..7416aac2 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -144,9 +144,6 @@ let options = Arg.align ([
( "-c_no_rts",
Arg.Set C_backend.opt_no_rts,
" do not include the Sail runtime" );
- ( "-c_separate_execute",
- Arg.Set Rewrites.opt_separate_execute,
- " separate execute scattered function into multiple functions");
( "-c_prefix",
Arg.String (fun prefix -> C_backend.opt_prefix := prefix),
"<prefix> prefix generated C functions" );
diff --git a/src/slice.ml b/src/slice.ml
index f50104c4..036b80d3 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -283,6 +283,21 @@ let rec graph_of_ast (Defs defs) =
| [] -> G.empty
+let rec filter_ast' g =
+ let module NM = Map.Make(Node) in
+ function
+ | DEF_fundef fdef :: defs when NM.mem (Function (id_of_fundef fdef)) g -> DEF_fundef fdef :: filter_ast' g defs
+ | DEF_fundef _ :: defs -> filter_ast' g defs
+
+ | DEF_spec vs :: defs when NM.mem (Function (id_of_val_spec vs)) g -> DEF_spec vs :: filter_ast' g defs
+ | DEF_spec _ :: defs -> filter_ast' g defs
+
+ | def :: defs -> def :: filter_ast' g defs
+
+ | [] -> []
+
+let filter_ast g (Defs defs) = Defs (filter_ast' g defs)
+
let dot_of_ast out_chan ast =
let module G = Graph.Make(Node) in
let module NodeSet = Set.Make(Node) in
diff --git a/src/slice.mli b/src/slice.mli
index 09558ebf..0eefd087 100644
--- a/src/slice.mli
+++ b/src/slice.mli
@@ -66,3 +66,5 @@ end
val graph_of_ast : Type_check.tannot defs -> Graph.Make(Node).graph
val dot_of_ast : out_channel -> Type_check.tannot defs -> unit
+
+val filter_ast : Graph.Make(Node).graph -> Type_check.tannot defs -> Type_check.tannot defs
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 06:58:01 +0000