From 08f65aad9bdb57dd1867b3206c9ffcd30666f2d3 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 6 Mar 2019 17:44:54 +0000 Subject: Improve AST slicing --- src/slice.ml | 158 ++++++++++++++++++++++++++++++++++++++++++++++------------ src/slice.mli | 68 +++++++++++++++++++++++++ 2 files changed, 195 insertions(+), 31 deletions(-) create mode 100644 src/slice.mli (limited to 'src') diff --git a/src/slice.ml b/src/slice.ml index c1829f7d..f50104c4 100644 --- a/src/slice.ml +++ b/src/slice.ml @@ -53,15 +53,12 @@ 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 + | Constructor of id let node_id = function | Register id -> id @@ -69,6 +66,7 @@ let node_id = function | Letbind id -> id | Type id -> id | Overload id -> id + | Constructor id -> id let node_kind = function | Register _ -> 0 @@ -76,6 +74,7 @@ let node_kind = function | Letbind _ -> 3 | Type _ -> 4 | Overload _ -> 5 + | Constructor _ -> 6 module Node = struct type t = node @@ -93,6 +92,7 @@ let node_color cuts = | Letbind _ -> "yellow" | Type _ -> "springgreen" | Overload _ -> "peachpuff" + | Constructor _ -> "lightslateblue" let node_string n = node_id n |> string_of_id |> String.escaped @@ -102,32 +102,82 @@ 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 rec constraint_ids' (NC_aux (aux, _)) = + match aux with + | NC_equal (n1, n2) | NC_bounded_le (n1, n2) | NC_bounded_ge (n1, n2) | NC_not_equal (n1, n2) -> + IdSet.union (nexp_ids' n1) (nexp_ids' n2) + | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> + IdSet.union (constraint_ids' nc1) (constraint_ids' nc2) + | NC_var _ | NC_true | NC_false | NC_set _ -> IdSet.empty + | NC_app (id, args) -> + IdSet.add id (List.fold_left IdSet.union IdSet.empty (List.map typ_arg_ids' args)) + +and nexp_ids' (Nexp_aux (aux, _)) = + match aux with + | Nexp_id id -> IdSet.singleton id + | Nexp_app (id, nexps) -> + IdSet.add id (List.fold_left IdSet.union IdSet.empty (List.map nexp_ids' nexps)) + | Nexp_var _ | Nexp_constant _ -> IdSet.empty + | Nexp_exp n | Nexp_neg n -> nexp_ids' n + | Nexp_times (n1, n2) | Nexp_sum (n1, n2) | Nexp_minus (n1, n2) -> + IdSet.union (nexp_ids' n1) (nexp_ids' n2) + +and typ_ids' (Typ_aux (aux, _)) = + match aux with + | Typ_var _ | Typ_internal_unknown -> IdSet.empty + | Typ_id id -> IdSet.singleton id + | Typ_app (id, args) -> + IdSet.add id (List.fold_left IdSet.union IdSet.empty (List.map typ_arg_ids' args)) + | 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 + | A_nexp nexp -> nexp_ids' nexp + | A_bool nc -> constraint_ids' nc + | A_order _ -> IdSet.empty + +let constraint_ids nc = IdSet.diff (constraint_ids' nc) builtins +let nexp_ids nc = IdSet.diff (constraint_ids' nc) builtins +and typ_ids typ = IdSet.diff (typ_ids' typ) builtins +let typ_arg_ids nc = IdSet.diff (typ_arg_ids' nc) 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_pat self p_aux annot = + let env = env_of_annot annot in + begin match p_aux with + | P_app (id, _) -> + graph := G.add_edge' self (Constructor id) !graph + | P_typ (typ, _) -> + IdSet.iter (fun id -> graph := G.add_edge' self (Type id) !graph) (typ_ids typ) + | _ -> () + end; + P_aux (p_aux, annot) + in + let rw_pat self = { id_pat_alg with p_aux = (fun (p_aux, annot) -> scan_pat self p_aux annot) } in + + let scan_lexp self lexp_aux annot = + let env = env_of_annot annot in + begin match lexp_aux with + | LEXP_cast (typ, _) -> + IdSet.iter (fun id -> graph := G.add_edge' self (Type id) !graph) (typ_ids typ) + | LEXP_memory (id, _) -> + graph := G.add_edge' self (Function id) !graph + | _ -> () + end; + LEXP_aux (lexp_aux, annot) + in + let scan_exp self e_aux annot = let env = env_of_annot annot in begin match e_aux with @@ -140,7 +190,10 @@ let add_def_to_graph graph def = else () end | E_app (id, _) -> - graph := G.add_edge' self (Function id) !graph + if Env.is_union_constructor id env then + graph := G.add_edge' self (Constructor id) !graph + else + graph := G.add_edge' self (Function id) !graph | E_ref id -> graph := G.add_edge' self (Register id) !graph | E_cast (typ, _) -> @@ -149,15 +202,58 @@ let add_def_to_graph graph def = 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 rw_exp self = { id_exp_alg with e_aux = (fun (e_aux, annot) -> scan_exp self e_aux annot); + pat_alg = rw_pat self } in let rewriters self = { rewriters_base with rewrite_exp = (fun _ -> fold_exp (rw_exp self)); + rewrite_pat = (fun _ -> fold_pat (rw_pat self)); rewrite_let = (fun _ -> fold_letbind (rw_exp self)); } in + let scan_quant_item self (QI_aux (aux, _)) = + match aux with + | QI_id _ -> () + | QI_const nc -> + IdSet.iter (fun id -> graph := G.add_edge' self (Type id) !graph) (constraint_ids nc) + in + + let scan_typquant self (TypQ_aux (aux, _)) = + match aux with + | TypQ_no_forall -> () + | TypQ_tq quants -> List.iter (scan_quant_item self) quants + in + + let add_type_def_to_graph (TD_aux (aux, (l, _))) = + match aux with + | TD_abbrev (id, typq, arg) -> + graph := G.add_edges' (Type id) (List.map (fun id -> Type id) (IdSet.elements (typ_arg_ids arg))) !graph; + scan_typquant (Type id) typq + | TD_record (id, typq, fields, _) -> + let field_nodes = + List.map (fun (typ, _) -> typ_ids typ) fields + |> List.fold_left IdSet.union IdSet.empty + |> IdSet.elements + |> List.map (fun id -> Type id) + in + graph := G.add_edges' (Type id) field_nodes !graph; + scan_typquant (Type id) typq + | TD_variant (id, typq, ctors, _) -> + let ctor_nodes = + List.map (fun (Tu_aux (Tu_ty_id (typ, id), _)) -> (typ_ids typ, id)) ctors + |> List.fold_left (fun (ids, ctors) (ids', ctor) -> (IdSet.union ids ids', IdSet.add ctor ctors)) (IdSet.empty, IdSet.empty) + in + 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_bitfield _ -> + Reporting.unreachable l __POS__ "Bitfield should be re-written" + 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; @@ -170,6 +266,9 @@ let add_def_to_graph graph def = 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 + | DEF_type tdef -> + add_type_def_to_graph tdef + | DEF_pragma _ -> () | _ -> () end; G.fix_leaves !graph @@ -184,11 +283,8 @@ let rec graph_of_ast (Defs defs) = | [] -> G.empty -let dot_of_ast ast = +let dot_of_ast out_chan 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 + G.make_dot (node_color NodeSet.empty) edge_color node_string out_chan g diff --git a/src/slice.mli b/src/slice.mli new file mode 100644 index 00000000..09558ebf --- /dev/null +++ b/src/slice.mli @@ -0,0 +1,68 @@ +(**************************************************************************) +(* 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 + +type node = + | Register of id + | Function of id + | Letbind of id + | Type of id + | Overload of id + | Constructor of id + +module Node : sig + type t = node + val compare : node -> node -> int +end + +val graph_of_ast : Type_check.tannot defs -> Graph.Make(Node).graph + +val dot_of_ast : out_channel -> Type_check.tannot defs -> unit -- cgit v1.2.3