Merge branch 'sail2' of https://github.com/rems-project/sail into sail2

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)) *)