diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.mli | 1 | ||||
| -rw-r--r-- | src/graph.ml | 21 | ||||
| -rw-r--r-- | src/graph.mli | 4 | ||||
| -rw-r--r-- | src/slice.ml | 194 | ||||
| -rw-r--r-- | src/type_check.ml | 30 | ||||
| -rw-r--r-- | src/type_check.mli | 4 |
6 files changed, 240 insertions, 14 deletions
diff --git a/src/ast_util.mli b/src/ast_util.mli index 823fcebb..0c42d9d3 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -403,6 +403,7 @@ val ids_of_def : 'a def -> IdSet.t val ids_of_defs : 'a defs -> IdSet.t val pat_ids : 'a pat -> IdSet.t + val subst : id -> 'a exp -> 'a exp -> 'a exp val hex_to_bin : string -> string diff --git a/src/graph.ml b/src/graph.ml index 2fc09014..e3af0b97 100644 --- a/src/graph.ml +++ b/src/graph.ml @@ -88,6 +88,8 @@ module type S = (** Topologically sort a graph. Throws Not_a_DAG if the graph is not directed acyclic. *) val topsort : graph -> node list + + val make_dot : (node -> string) -> (node -> node -> string) -> (node -> string) -> out_channel -> graph -> unit end module Make(Ord: OrderedType) = struct @@ -152,7 +154,9 @@ module Make(Ord: OrderedType) = struct let prune roots cuts cg = let rs = reachable roots cuts cg in - fix_leaves (NM.filter (fun fn _ -> NS.mem fn rs) cg) + let cg = NM.filter (fun fn _ -> NS.mem fn rs) cg in + let cg = NM.mapi (fun fn children -> if NS.mem fn cuts then NS.empty else children) cg in + fix_leaves cg let remove_self_loops cg = NM.mapi (fun fn callees -> NS.remove fn callees) cg @@ -206,4 +210,19 @@ module Make(Ord: OrderedType) = struct in topsort' (); !list + let make_dot node_color edge_color string_of_node out_chan graph = + Util.opt_colors := false; + let to_string node = String.escaped (string_of_node node) in + output_string out_chan "digraph DEPS {\n"; + let make_node from_node = + output_string out_chan (Printf.sprintf " \"%s\" [fillcolor=%s;style=filled];\n" (to_string from_node) (node_color from_node)) + in + let make_line from_node to_node = + output_string out_chan (Printf.sprintf " \"%s\" -> \"%s\" [color=%s];\n" (to_string from_node) (to_string to_node) (edge_color from_node to_node)) + in + NM.bindings graph |> List.iter (fun (from_node, _) -> make_node from_node); + NM.bindings graph |> List.iter (fun (from_node, to_nodes) -> NS.iter (make_line from_node) to_nodes); + output_string out_chan "}\n"; + Util.opt_colors := true; + end diff --git a/src/graph.mli b/src/graph.mli index 11ea63dc..09b78304 100644 --- a/src/graph.mli +++ b/src/graph.mli @@ -90,9 +90,11 @@ module type S = (** Topologically sort a graph. Throws Not_a_DAG if the graph is not directed acyclic. *) val topsort : graph -> node list + + val make_dot : (node -> string) -> (node -> node -> string) -> (node -> string) -> out_channel -> graph -> unit end module Make(Ord: OrderedType) : S with type node = Ord.t and type node_set = Set.Make(Ord).t - and type graph = Set.Make(Ord).t Map.Make(Ord).t + and type graph = Set.Make(Ord).t Map.Make(Ord).t 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 diff --git a/src/type_check.ml b/src/type_check.ml index 02339842..5bc3cc2d 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -105,6 +105,7 @@ type env = { top_val_specs : (typquant * typ) Bindings.t; defined_val_specs : IdSet.t; locals : (mut * typ) Bindings.t; + top_letbinds : IdSet.t; union_ids : (typquant * typ) Bindings.t; registers : (effect * effect * typ) Bindings.t; variants : (typquant * type_union list) Bindings.t; @@ -409,6 +410,8 @@ module Env : sig val get_accessor : id -> id -> t -> typquant * typ * typ * effect val add_local : id -> mut * typ -> t -> t val get_locals : t -> (mut * typ) Bindings.t + val add_toplevel_lets : IdSet.t -> t -> t + val get_toplevel_lets : t -> IdSet.t val add_variant : id -> typquant * type_union list -> t -> t val add_scattered_variant : id -> typquant -> t -> t val add_variant_clause : id -> type_union -> t -> t @@ -488,6 +491,7 @@ end = struct { top_val_specs = Bindings.empty; defined_val_specs = IdSet.empty; locals = Bindings.empty; + top_letbinds = IdSet.empty; union_ids = Bindings.empty; registers = Bindings.empty; variants = Bindings.empty; @@ -1059,15 +1063,19 @@ end = struct | Mutable -> "ref<" ^ string_of_typ typ ^ ">" let add_local id mtyp env = - begin - if not env.allow_bindings then typ_error env (id_loc id) "Bindings are not allowed in this context" else (); - wf_typ env (snd mtyp); - if Bindings.mem id env.top_val_specs then - typ_error env (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name") - else (); - typ_print (lazy (adding ^ "local binding " ^ string_of_id id ^ " : " ^ string_of_mtyp mtyp)); - { env with locals = Bindings.add id mtyp env.locals } - end + if not env.allow_bindings then typ_error env (id_loc id) "Bindings are not allowed in this context" else (); + wf_typ env (snd mtyp); + if Bindings.mem id env.top_val_specs then + typ_error env (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name") + else (); + typ_print (lazy (adding ^ "local binding " ^ string_of_id id ^ " : " ^ string_of_mtyp mtyp)); + { env with locals = Bindings.add id mtyp env.locals; + top_letbinds = IdSet.remove id env.top_letbinds } + + let add_toplevel_lets ids env = + { env with top_letbinds = IdSet.union ids env.top_letbinds } + + let get_toplevel_lets env = env.top_letbinds let add_variant id variant env = typ_print (lazy (adding ^ "variant " ^ string_of_id id)); @@ -4560,14 +4568,14 @@ let check_letdef orig_env (LB_aux (letbind, (l, _))) = let tpat, env = bind_pat_no_guard orig_env (strip_pat pat) typ_annot in if (BESet.is_empty (effect_set (effect_of checked_bind)) || !opt_no_effects) then - [DEF_val (LB_aux (LB_val (tpat, checked_bind), (l, None)))], env + [DEF_val (LB_aux (LB_val (tpat, checked_bind), (l, None)))], Env.add_toplevel_lets (pat_ids tpat) env else typ_error env l ("Top-level definition with effects " ^ string_of_effect (effect_of checked_bind)) | LB_val (pat, bind) -> let inferred_bind = propagate_exp_effect (irule infer_exp orig_env (strip_exp bind)) in let tpat, env = bind_pat_no_guard orig_env (strip_pat pat) (typ_of inferred_bind) in if (BESet.is_empty (effect_set (effect_of inferred_bind)) || !opt_no_effects) then - [DEF_val (LB_aux (LB_val (tpat, inferred_bind), (l, None)))], env + [DEF_val (LB_aux (LB_val (tpat, inferred_bind), (l, None)))], Env.add_toplevel_lets (pat_ids tpat) env else typ_error env l ("Top-level definition with effects " ^ string_of_effect (effect_of inferred_bind)) end diff --git a/src/type_check.mli b/src/type_check.mli index cfdfa2c6..15110b37 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -171,6 +171,8 @@ module Env : sig up the type without any flow typing modifiers. *) val lookup_id : ?raw:bool -> id -> t -> typ lvar + val get_toplevel_lets : t -> IdSet.t + val is_union_constructor : id -> t -> bool (** Check if the id is both a constructor, and the only constructor of that @@ -189,7 +191,7 @@ module Env : sig val expand_constraint_synonyms : t -> n_constraint -> n_constraint val expand_nexp_synonyms : t -> nexp -> nexp - + val expand_synonyms : t -> typ -> typ (** Expand type synonyms and remove register annotations (i.e. register<t> -> t)) *) |