WIP: Start working on being able to slice single instructions out of specs

1 files changed, 194 insertions, 0 deletions

diff --git a/src/slice.ml b/src/slice.ml
new file mode 100644
index 00000000..cbf8ee5d
--- /dev/null
+++ b/src/slice.ml
@@ -0,0 +1,194 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ast
+open Ast_util
+open Rewriter
+
+type node =
+  (* In the graph we have a node Register that represents the actual
+     register, but functions get only get transitive dependencies on
+     that through Register_read, Register_write, and Register_ref
+     nodes. *)
+  | Register of id
+  | Function of id
+  | Letbind of id
+  | Type of id
+  | Overload of id
+
+let node_id = function
+  | Register id -> id
+  | Function id -> id
+  | Letbind id -> id
+  | Type id -> id
+  | Overload id -> id
+
+let node_kind = function
+  | Register _ -> 0
+  | Function _ -> 1
+  | Letbind _ -> 3
+  | Type _ -> 4
+  | Overload _ -> 5
+
+module Node = struct
+  type t = node
+  let compare n1 n2 =
+    let lex_ord c1 c2 = if c1 = 0 then c2 else c1 in
+    lex_ord (compare (node_kind n1) (node_kind n2)) (Id.compare (node_id n1) (node_id n2))
+end
+
+let node_color cuts =
+  let module NodeSet = Set.Make(Node) in
+  function
+  | node when NodeSet.mem node cuts -> "red"
+  | Register _ -> "lightpink"
+  | Function _ -> "white"
+  | Letbind _ -> "yellow"
+  | Type _ -> "springgreen"
+  | Overload _ -> "peachpuff"
+
+let node_string n = node_id n |> string_of_id |> String.escaped
+
+let edge_color from_node to_node = "black"
+
+let builtins =
+  let open Type_check in
+  IdSet.of_list (List.map fst (Bindings.bindings Env.builtin_typs))
+
+let typ_ids typ =
+  let rec typ_ids (Typ_aux (aux, _)) =
+    match aux with
+    | Typ_var _ | Typ_internal_unknown -> IdSet.empty
+    | Typ_id id -> IdSet.singleton id
+    | Typ_app (id, typs) ->
+     IdSet.add id (List.fold_left IdSet.union IdSet.empty (List.map typ_arg_ids typs))
+    | Typ_fn (typs, typ, _) ->
+       IdSet.union (typ_ids typ) (List.fold_left IdSet.union IdSet.empty (List.map typ_ids typs))
+    | Typ_bidir (typ1, typ2) ->
+       IdSet.union (typ_ids typ1) (typ_ids typ2)
+    | Typ_tup typs ->
+       List.fold_left IdSet.union IdSet.empty (List.map typ_ids typs)
+    | Typ_exist (_, _, typ) -> typ_ids typ
+  and typ_arg_ids (A_aux (aux, _)) =
+    match aux with
+    | A_typ typ -> typ_ids typ
+    | _ -> IdSet.empty
+  in
+  IdSet.diff (typ_ids typ) builtins
+
+let add_def_to_graph graph def =
+  let open Type_check in
+  let module G = Graph.Make(Node) in
+  let graph = ref graph in
+
+  let scan_exp self e_aux annot =
+    let env = env_of_annot annot in
+    begin match e_aux with
+    | E_id id ->
+       begin match Env.lookup_id id env with
+       | Register _ -> graph := G.add_edge self (Register id) !graph
+       | _ ->
+          if IdSet.mem id (Env.get_toplevel_lets env) then
+            graph := G.add_edge self (Letbind id) !graph
+          else ()
+       end
+    | E_app (id, _) ->
+       graph := G.add_edge self (Function id) !graph
+    | E_ref id ->
+       graph := G.add_edge self (Register id) !graph
+    | E_cast (typ, _) ->
+       IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (typ_ids typ)
+    | _ -> ()
+    end;
+    E_aux (e_aux, annot)
+  in
+  let rw_exp self = { id_exp_alg with e_aux = (fun (e_aux, annot) -> scan_exp self e_aux annot) } in
+
+  let rewriters self =
+    { rewriters_base with
+      rewrite_exp = (fun _ -> fold_exp (rw_exp self));
+      rewrite_let = (fun _ -> fold_letbind (rw_exp self));
+    }
+  in
+
+  begin match def with
+  | DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), _), id, _, _), _)) ->
+     graph := G.add_edges (Function id) [] !graph;
+     IdSet.iter (fun typ_id -> graph := G.add_edge (Function id) (Type typ_id) !graph) (typ_ids typ)
+  | DEF_fundef fdef ->
+     let id = id_of_fundef fdef in
+     graph := G.add_edges (Function id) [] !graph;
+     ignore (rewrite_fun (rewriters (Function id)) fdef)
+  | DEF_val (LB_aux (LB_val (pat, exp), _) as lb) ->
+     let ids = pat_ids pat in
+     IdSet.iter (fun id -> graph := G.add_edges (Letbind id) [] !graph) ids;
+     IdSet.iter (fun id -> ignore (rewrite_let (rewriters (Letbind id)) lb)) ids
+  | _ -> ()
+  end;
+  !graph
+
+let rec graph_of_ast (Defs defs) =
+  let module G = Graph.Make(Node) in
+
+  match defs with
+  | def :: defs ->
+     let g = graph_of_ast (Defs defs) in
+     add_def_to_graph g def
+
+  | [] -> G.empty
+
+let dot_of_ast ast =
+  let module G = Graph.Make(Node) in
+  let module NodeSet = Set.Make(Node) in
+  let g = graph_of_ast ast in
+  let roots = NodeSet.of_list (List.map (fun str -> Function (mk_id str)) ["execute_CGetPerm"; "execute_CSeal"]) in
+  let cuts = NodeSet.of_list (List.map (fun str -> Function (mk_id str)) ["readCapReg"; "writeCapReg"; "rGPR"; "wGPR"; "SignalException"]) in
+  let g = G.prune roots cuts g in
+  G.make_dot (node_color cuts) edge_color node_string stdout g