Rewriter: Expose rewrite passes to interactive mode

Rather than each rewrite being an opaque function, with separate lists
of rewrites for each backend, instead put all the rewrites into a
single list then have each backend define which of those rewrites it
wants to use and in what order.

For example, rather than having

let rewrite_defs_ocaml = [
    ...
    ("rewrite_undefined", rewrite_undefined_if_gen false);
    ...
  ]

we would now have

let all_rewrites = [
    ...
    ("undefined", Bool_rewriter (fun b -> Basic_rewriter (rewrite_undefined_if_gen b)));
    ...
  ]

let rewriters_ocaml = [
    ...
    ("undefined", [Bool_arg false]);
    ...
  ]

let rewrite_defs_ocaml =
  List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) rewriters_ocaml

This means we can introspect on the arguments required for each
rewrite, allowing a :rewrite command in the interactive mode which can
parse the arguments required for each rewrite, so we can invoke the
above rewrite as

sail> :rewrite undefined false

with completion for the rewrite name based on all_rewrites, and hints
for any arguments.

The idea behind this is if we want to generate a very custom slice of
a specification, we can set it up as a sequence of interpreter
commands, e.g.

...
:rewrite split execute
:slice_roots execute_LOAD
:slice_cuts rX wX
:slice
:rewrite tuple_assignments
...

where we slice a spec just after splitting the execute function. This
should help in avoiding an endless proliferation of additional options
and flags on the command line.

1 files changed, 15 insertions, 0 deletions

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