summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/isail.ml37
-rw-r--r--src/jib/c_backend.ml4
-rw-r--r--src/sail.ml14
-rw-r--r--src/slice.ml61
-rw-r--r--src/slice.mli3
-rw-r--r--src/specialize.ml18
-rw-r--r--src/specialize.mli5
7 files changed, 87 insertions, 55 deletions
diff --git a/src/isail.ml b/src/isail.ml
index ac19eb01..51501e25 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -263,9 +263,8 @@ 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 slice_roots = ref IdSet.empty
+let slice_cuts = ref IdSet.empty
let rec describe_rewrite =
let open Rewrites in
@@ -391,7 +390,11 @@ let handle_input' input =
begin
try
let args = Str.split (Str.regexp " +") arg in
- Arg.parse_argv ~current:(ref 0) (Array.of_list ("sail" :: args)) Sail.options (fun _ -> ()) "";
+ begin match args with
+ | opt :: args ->
+ Arg.parse_argv ~current:(ref 0) (Array.of_list ["sail"; opt; String.concat " " args]) Sail.options (fun _ -> ()) "";
+ | [] -> print_endline "Must provide a valid option"
+ end
with
| Arg.Bad message | Arg.Help message -> print_endline message
end;
@@ -486,17 +489,22 @@ let handle_input' input =
()
| ":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
+ let ids = List.map mk_id args |> IdSet.of_list in
+ Specialize.add_initial_calls ids;
+ slice_roots := IdSet.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
+ let ids = List.map mk_id args |> IdSet.of_list in
+ slice_cuts := IdSet.union ids !slice_cuts
| ":slice" ->
+ let open Slice in
+ let module SliceNodeSet = Set.Make(Slice.Node) in
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
+ let roots = !slice_roots |> IdSet.elements |> List.map (fun id -> Function id) |> SliceNodeSet.of_list in
+ let cuts = !slice_cuts |> IdSet.elements |> List.map (fun id -> Function id) |> SliceNodeSet.of_list in
+ let g = G.prune roots cuts g in
+ Interactive.ast := Slice.filter_ast !slice_cuts g !Interactive.ast
| ":list_rewrites" ->
let print_rewrite (name, rw) =
print_endline (name ^ " " ^ Util.(String.concat " " (describe_rewrite rw) |> yellow |> clear))
@@ -525,18 +533,23 @@ let handle_input' input =
let rw = List.assoc rw Rewrites.all_rewrites in
let rw = parse_args rw args in
Interactive.ast := rw !Interactive.env !Interactive.ast;
- interactive_state := initial_state !Interactive.ast Value.primops;
| [] ->
failwith "Must provide the name of a rewrite, use :list_rewrites for a list of possible rewrites"
end
| ":rewrites" ->
Interactive.ast := Process_file.rewrite_ast_target arg !Interactive.env !Interactive.ast;
- interactive_state := initial_state !Interactive.ast Value.primops;
+ interactive_state := initial_state !Interactive.ast Value.primops
| ":prover_regstate" ->
let env, ast = prover_regstate (Some arg) !Interactive.ast !Interactive.env in
Interactive.env := env;
Interactive.ast := ast;
+ interactive_state := initial_state !Interactive.ast Value.primops
+ | ":recheck" ->
+ let ast, env = Type_check.check Type_check.initial_env !Interactive.ast in
+ Interactive.env := env;
+ Interactive.ast := ast;
interactive_state := initial_state !Interactive.ast Value.primops;
+ vs_ids := val_spec_ids !Interactive.ast
| ":compile" ->
let out_name = match !opt_file_out with
| None -> "out.sail"
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 4d6db514..a784b08e 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -1184,9 +1184,9 @@ let rec sgen_ctyp = function
| CT_unit -> "unit"
| CT_bit -> "fbits"
| CT_bool -> "bool"
- | CT_fbits _ -> "fbits"
+ | CT_fbits _ -> "uint64_t"
| CT_sbits _ -> "sbits"
- | CT_fint _ -> "mach_int"
+ | CT_fint _ -> "int64_t"
| CT_lint -> "sail_int"
| CT_lbits _ -> "lbits"
| CT_tup _ as tup -> "struct " ^ Util.zencode_string ("tuple_" ^ string_of_ctyp tup)
diff --git a/src/sail.ml b/src/sail.ml
index 3ab48190..b016e574 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -66,7 +66,6 @@ let opt_libs_coq = ref ([]:string list)
let opt_file_arguments = ref ([]:string list)
let opt_process_elf : string option ref = ref None
let opt_ocaml_generators = ref ([]:string list)
-let opt_slice = ref ([]:string list)
let set_target name = Arg.Unit (fun _ -> opt_target := Some name)
@@ -300,9 +299,6 @@ let options = Arg.align ([
( "-dprofile",
Arg.Set Profile.opt_profile,
" (debug) provide basic profiling information for rewriting passes within Sail");
- ( "-slice",
- Arg.String (fun s -> opt_slice := s::!opt_slice),
- "<id> produce version of input restricted to the given function");
( "-v",
Arg.Set opt_print_version,
" print version");
@@ -394,6 +390,7 @@ let target name out_name ast type_envs =
let close, output_chan = match !opt_file_out with Some f -> true, open_out (f ^ ".c") | None -> false, stdout in
Util.opt_warnings := true;
C_backend.compile_ast type_envs output_chan (!opt_includes_c) ast_c;
+ flush output_chan;
if close then close_out output_chan else ()
| Some "ir" ->
@@ -408,6 +405,7 @@ let target name out_name ast type_envs =
let cdefs, _ = C_backend.jib_of_ast type_envs ast_c in
let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_cdef cdefs) in
output_string output_chan (str ^ "\n");
+ flush output_chan;
if close then close_out output_chan else ()
| Some "lem" ->
@@ -464,14 +462,6 @@ let main () =
ignore (rewrite_ast_check type_envs ast)
else ();
- begin match !opt_slice with
- | [] -> ()
- | ids ->
- let ids = List.map Ast_util.mk_id ids in
- let ids = Ast_util.IdSet.of_list ids in
- Pretty_print_sail.pp_defs stdout (Specialize.slice_defs type_envs ast ids)
- end;
-
let type_envs, ast = prover_regstate !opt_target ast type_envs in
let ast = match !opt_target with Some tgt -> rewrite_ast_target tgt type_envs ast | None -> ast in
target !opt_target out_name ast type_envs;
diff --git a/src/slice.ml b/src/slice.ml
index 036b80d3..fa574b7f 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -184,6 +184,7 @@ let add_def_to_graph graph def =
| E_id id ->
begin match Env.lookup_id id env with
| Register _ -> graph := G.add_edge' self (Register id) !graph
+ | Enum _ -> graph := G.add_edge' self (Constructor id) !graph
| _ ->
if IdSet.mem id (Env.get_toplevel_lets env) then
graph := G.add_edge' self (Letbind id) !graph
@@ -248,8 +249,8 @@ let add_def_to_graph graph def =
IdSet.iter (fun ctor_id -> graph := G.add_edge' (Constructor ctor_id) (Type id) !graph) (snd ctor_nodes);
IdSet.iter (fun typ_id -> graph := G.add_edge' (Type id) (Type typ_id) !graph) (fst ctor_nodes);
scan_typquant (Type id) typq
- | TD_enum (id, _, _) ->
- graph := G.add_edges' (Type id) [] !graph
+ | TD_enum (id, ctors, _) ->
+ List.iter (fun ctor_id -> graph := G.add_edge' (Constructor ctor_id) (Type id) !graph) ctors
| TD_bitfield _ ->
Reporting.unreachable l __POS__ "Bitfield should be re-written"
in
@@ -268,7 +269,11 @@ let add_def_to_graph graph def =
IdSet.iter (fun id -> ignore (rewrite_let (rewriters (Letbind id)) lb)) ids
| DEF_type tdef ->
add_type_def_to_graph tdef
- | DEF_pragma _ -> ()
+ | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), _)) ->
+ IdSet.iter (fun typ_id -> graph := G.add_edge' (Register id) (Type typ_id) !graph) (typ_ids typ)
+ | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) ->
+ ignore (rewrite_exp (rewriters (Register id)) exp);
+ IdSet.iter (fun typ_id -> graph := G.add_edge' (Register id) (Type typ_id) !graph) (typ_ids typ)
| _ -> ()
end;
G.fix_leaves !graph
@@ -283,20 +288,50 @@ 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
+let id_of_typedef (TD_aux (aux, _)) =
+ match aux with
+ | TD_abbrev (id, _, _) -> id
+ | TD_record (id, _, _, _) -> id
+ | TD_variant (id, _, _, _) -> id
+ | TD_enum (id, _, _) -> id
+ | TD_bitfield (id, _, _) -> id
+
+let id_of_reg_dec (DEC_aux (aux, _)) =
+ match aux with
+ | DEC_reg (_, _, _, id) -> id
+ | DEC_config (id, _, _) -> id
+ | _ -> assert false
+
- | 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
+let filter_ast cuts g (Defs defs) =
+ let rec filter_ast' g =
+ let module NM = Map.Make(Node) in
+ function
+ | DEF_fundef fdef :: defs when IdSet.mem (id_of_fundef fdef) cuts -> filter_ast' g defs
+ | 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 :: defs -> def :: filter_ast' g defs
+ | DEF_reg_dec rdec :: defs when NM.mem (Register (id_of_reg_dec rdec)) g -> DEF_reg_dec rdec :: filter_ast' g defs
+ | DEF_reg_dec _ :: 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
-let filter_ast g (Defs defs) = Defs (filter_ast' g defs)
+ | DEF_val (LB_aux (LB_val (pat, exp), _) as lb) :: defs ->
+ let ids = pat_ids pat |> IdSet.elements in
+ if List.exists (fun id -> NM.mem (Letbind id) g) ids then
+ DEF_val lb :: filter_ast' g defs
+ else
+ filter_ast' g defs
+
+ | DEF_type tdef :: defs when NM.mem (Type (id_of_typedef tdef)) g -> DEF_type tdef :: filter_ast' g defs
+ | DEF_type _ :: defs -> filter_ast' g defs
+
+ | def :: defs -> def :: filter_ast' g defs
+
+ | [] -> []
+ in
+ Defs (filter_ast' g defs)
let dot_of_ast out_chan ast =
let module G = Graph.Make(Node) in
diff --git a/src/slice.mli b/src/slice.mli
index 0eefd087..04f140fe 100644
--- a/src/slice.mli
+++ b/src/slice.mli
@@ -49,6 +49,7 @@
(**************************************************************************)
open Ast
+open Ast_util
type node =
| Register of id
@@ -67,4 +68,4 @@ 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
+val filter_ast : IdSet.t -> Graph.Make(Node).graph -> Type_check.tannot defs -> Type_check.tannot defs
diff --git a/src/specialize.ml b/src/specialize.ml
index afce4b0f..5a7624bc 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -483,7 +483,7 @@ let specialize_id_overloads instantiations id (Defs defs) =
valspecs are then re-specialized. This process is iterated until
the whole spec is specialized. *)
-let initial_calls = IdSet.of_list
+let initial_calls = ref (IdSet.of_list
[ mk_id "main";
mk_id "__SetConfig";
mk_id "__ListConfig";
@@ -491,10 +491,12 @@ let initial_calls = IdSet.of_list
mk_id "decode";
mk_id "initialize_registers";
mk_id "append_64" (* used to construct bitvector literals in C backend *)
- ]
+ ])
-let remove_unused_valspecs ?(initial_calls=initial_calls) env ast =
- let calls = ref initial_calls in
+let add_initial_calls ids = initial_calls := IdSet.union ids !initial_calls
+
+let remove_unused_valspecs env ast =
+ let calls = ref !initial_calls in
let vs_ids = val_spec_ids ast in
let inspect_exp = function
@@ -527,14 +529,6 @@ let remove_unused_valspecs ?(initial_calls=initial_calls) env ast =
List.fold_left (fun ast id -> Defs (remove_unused ast id)) ast (IdSet.elements unused)
-let slice_defs env (Defs defs) keep_ids =
- let keep = function
- | DEF_fundef fd -> IdSet.mem (id_of_fundef fd) keep_ids
- | _ -> true
- in
- let defs = List.filter keep defs in
- remove_unused_valspecs env (Defs defs) ~initial_calls:keep_ids
-
let specialize_id spec id ast =
let instantiations = instantiations_of spec id ast in
let ast = specialize_id_valspec spec instantiations id ast in
diff --git a/src/specialize.mli b/src/specialize.mli
index 6ec8c2aa..28d118ca 100644
--- a/src/specialize.mli
+++ b/src/specialize.mli
@@ -72,6 +72,8 @@ val int_specialization_with_externs : specialization
or some combination of those. *)
val polymorphic_functions : specialization -> 'a defs -> IdSet.t
+val add_initial_calls : IdSet.t -> unit
+
(** specialize returns an AST with all the Order and Type polymorphism
removed, as well as the environment produced by type checking that
AST with [Type_check.initial_env]. The env parameter is the
@@ -88,6 +90,3 @@ val specialize' : int -> specialization -> tannot defs -> Env.t -> tannot defs *
val instantiations_of : specialization -> id -> tannot defs -> typ_arg KBindings.t list
val string_of_instantiation : typ_arg KBindings.t -> string
-
-(** Remove all function definitions except for the given set *)
-val slice_defs : Env.t -> tannot defs -> IdSet.t -> tannot defs
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 19:34:15 +0000