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/pretty_print_coq.ml | 2 | ||||
| -rw-r--r-- | src/slice.ml | 194 | ||||
| -rw-r--r-- | src/type_check.ml | 66 | ||||
| -rw-r--r-- | src/type_check.mli | 4 |
7 files changed, 271 insertions, 21 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/pretty_print_coq.ml b/src/pretty_print_coq.ml index d323d639..42780012 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1096,7 +1096,7 @@ let condition_produces_constraint exp = dependent pair with a proof that the result is the expected integer. This is redundant for basic arithmetic functions and functions which we unfold in the constraint solver. *) -let no_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "length_mword"; "length"; +let no_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "Z.rem"; "length_mword"; "length"; "negb"; "andb"; "orb"; "Z.leb"; "Z.geb"; "Z.ltb"; "Z.gtb"; "Z.eqb"] 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 1afd9765..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; @@ -251,6 +252,25 @@ and strip_kinded_id_aux = function and strip_kind = function | K_aux (k_aux, _) -> K_aux (k_aux, Parse_ast.Unknown) +let rec typ_constraints (Typ_aux (typ_aux, l)) = + match typ_aux with + | Typ_internal_unknown -> [] + | Typ_id v -> [] + | Typ_var kid -> [] + | Typ_tup typs -> List.concat (List.map typ_constraints typs) + | Typ_app (f, args) -> List.concat (List.map typ_arg_nexps args) + | Typ_exist (kids, nc, typ) -> typ_constraints typ + | Typ_fn (arg_typs, ret_typ, _) -> + List.concat (List.map typ_constraints arg_typs) @ typ_constraints ret_typ + | Typ_bidir (typ1, typ2) -> + typ_constraints typ1 @ typ_constraints typ2 +and typ_arg_nexps (A_aux (typ_arg_aux, l)) = + match typ_arg_aux with + | A_nexp n -> [] + | A_typ typ -> typ_constraints typ + | A_bool nc -> [nc] + | A_order ord -> [] + let rec typ_nexps (Typ_aux (typ_aux, l)) = match typ_aux with | Typ_internal_unknown -> [] @@ -390,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 @@ -469,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; @@ -1040,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)); @@ -1585,6 +1612,9 @@ let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as | Typ_var v, _ when KidSet.mem v goals -> KBindings.singleton v (arg_typ typ2) + (* We need special cases for unifying range(n, m), nat, and int vs atom('n) *) + | Typ_id int, Typ_app (atom, [A_aux (A_nexp n, _)]) when string_of_id int = "int" -> KBindings.empty + | Typ_id nat, Typ_app (atom, [A_aux (A_nexp n, _)]) when string_of_id nat = "nat" -> if prove __POS__ env (nc_gteq n (nint 0)) then KBindings.empty else unify_error l (string_of_typ typ2 ^ " must be a natural number") @@ -2033,7 +2063,7 @@ let rec subtyp l env typ1 typ2 = let env = add_existential l kopts nc env in subtyp l env typ1 typ2 | None, Some (kopts, nc, typ2) -> typ_debug (lazy "Subtype check with unification"); - let typ1 = canonicalize env typ1 in + let typ1, env = bind_existential l None (canonicalize env typ1) env in let env = add_typ_vars l kopts env in let kids' = KidSet.elements (KidSet.diff (KidSet.of_list (List.map kopt_kid kopts)) (tyvars_of_typ typ2)) in if not (kids' = []) then typ_error env l "Universally quantified constraint generated" else (); @@ -3263,13 +3293,15 @@ and bind_typ_pat env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_aux (typ_aux, _) | TP_wild, _ -> env | TP_var kid, _ -> begin - match typ_nexps typ with - | [nexp] -> + match typ_nexps typ, typ_constraints typ with + | [nexp], [] -> Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l (mk_kopt K_int kid) env) - | [] -> + | [], [nc] -> + Env.add_constraint (nc_and (nc_or (nc_not nc) (nc_var kid)) (nc_or nc (nc_not (nc_var kid)))) (Env.add_typ_var l (mk_kopt K_bool kid) env) + | [], [] -> typ_error env l ("No numeric expressions in " ^ string_of_typ typ ^ " to bind " ^ string_of_kid kid ^ " to") - | nexps -> - typ_error env l ("Type " ^ string_of_typ typ ^ " has multiple numeric expressions. Cannot bind " ^ string_of_kid kid) + | _, _ -> + typ_error env l ("Type " ^ string_of_typ typ ^ " has multiple numeric or boolean expressions. Cannot bind " ^ string_of_kid kid) end | TP_app (f1, tpats), Typ_app (f2, typs) when Id.compare f1 f2 = 0 -> List.fold_left2 bind_typ_pat_arg env tpats typs @@ -4536,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)) *) |