diff options
| -rw-r--r-- | language/jib.ott | 1 | ||||
| -rw-r--r-- | src/graph.ml | 2 | ||||
| -rw-r--r-- | src/jib/c_backend.ml | 47 | ||||
| -rw-r--r-- | src/jib/c_backend.mli | 9 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 12 | ||||
| -rw-r--r-- | src/jib/jib_compile.mli | 7 | ||||
| -rw-r--r-- | src/jib/jib_optimize.ml | 129 | ||||
| -rw-r--r-- | src/jib/jib_optimize.mli | 63 | ||||
| -rw-r--r-- | src/jib/jib_ssa.ml | 602 | ||||
| -rw-r--r-- | src/jib/jib_ssa.mli | 85 | ||||
| -rw-r--r-- | src/jib/jib_util.ml | 167 | ||||
| -rw-r--r-- | src/sail.ml | 2 | ||||
| -rw-r--r-- | src/sail.odocl | 1 |
13 files changed, 954 insertions, 173 deletions
diff --git a/language/jib.ott b/language/jib.ott index 7b5d0162..e54e2ea5 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -136,6 +136,7 @@ clexp :: 'CL_' ::= | current_exception : ctyp :: :: current_exception | have_exception :: :: have_exception | return : ctyp :: :: return + | void :: :: void ctype_def :: 'CTD_' ::= {{ com C type definition }} diff --git a/src/graph.ml b/src/graph.ml index 21863e47..703deba9 100644 --- a/src/graph.ml +++ b/src/graph.ml @@ -234,6 +234,6 @@ module Make(Ord: OrderedType) = struct 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; + Util.opt_colors := true end diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index aab2894e..846b619f 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -63,7 +63,6 @@ module Big_int = Nat_big_num let c_verbosity = ref 0 -let opt_debug_flow_graphs = ref false let opt_static = ref false let opt_no_main = ref false let opt_memo_cache = ref false @@ -849,48 +848,6 @@ let hoist_allocations recursive_functions = function | cdef -> [cdef] -let flat_counter = ref 0 -let flat_id () = - let id = mk_id ("local#" ^ string_of_int !flat_counter) in - incr flat_counter; - id - -let rec flatten_instrs = function - | I_aux (I_decl (ctyp, decl_id), aux) :: instrs -> - let fid = flat_id () in - I_aux (I_decl (ctyp, fid), aux) :: flatten_instrs (instrs_rename decl_id fid instrs) - - | I_aux ((I_block block | I_try_block block), _) :: instrs -> - flatten_instrs block @ flatten_instrs instrs - - | I_aux (I_if (cval, then_instrs, else_instrs, _), _) :: instrs -> - let then_label = label "then_" in - let endif_label = label "endif_" in - [ijump cval then_label] - @ flatten_instrs else_instrs - @ [igoto endif_label] - @ [ilabel then_label] - @ flatten_instrs then_instrs - @ [ilabel endif_label] - @ flatten_instrs instrs - - | I_aux (I_comment _, _) :: instrs -> flatten_instrs instrs - - | instr :: instrs -> instr :: flatten_instrs instrs - | [] -> [] - -let flatten_cdef = - function - | CDEF_fundef (function_id, heap_return, args, body) -> - flat_counter := 0; - CDEF_fundef (function_id, heap_return, args, flatten_instrs body) - - | CDEF_let (n, bindings, instrs) -> - flat_counter := 0; - CDEF_let (n, bindings, flatten_instrs instrs) - - | cdef -> cdef - let rec specialize_variants ctx prior = let unifications = ref (Bindings.empty) in @@ -1386,6 +1343,7 @@ let rec sgen_clexp = function | CL_have_exception -> "have_exception" | CL_current_exception _ -> "current_exception" | CL_return _ -> assert false + | CL_void -> assert false let rec sgen_clexp_pure = function | CL_id (id, _) -> sgen_id id @@ -1395,6 +1353,7 @@ let rec sgen_clexp_pure = function | CL_have_exception -> "have_exception" | CL_current_exception _ -> "current_exception" | CL_return _ -> assert false + | CL_void -> assert false (** Generate instructions to copy from a cval to a clexp. This will insert any needed type conversions from big integers to small @@ -2079,8 +2038,6 @@ let codegen_def' ctx = function string (Printf.sprintf "%svoid %s(%s%s *rop, %s);" static (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) | CDEF_fundef (id, ret_arg, args, instrs) as def -> - if !opt_debug_flow_graphs then make_dot id (instrs_graph instrs) else (); - (* Extract type information about the function from the environment. *) let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in let arg_typs, ret_typ = match fn_typ with diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli index 2fc5be94..7314eb5a 100644 --- a/src/jib/c_backend.mli +++ b/src/jib/c_backend.mli @@ -53,10 +53,6 @@ open Type_check (** Global compilation options *) -(** Output a dataflow graph for each generated function in Graphviz - (dot) format. *) -val opt_debug_flow_graphs : bool ref - (** Define generated functions as static *) val opt_static : bool ref @@ -109,10 +105,5 @@ val optimize_experimental : bool ref (** Convert a typ to a IR ctyp *) val ctyp_of_typ : Jib_compile.ctx -> Ast.typ -> ctyp -(** Rewriting steps for compiled ASTs *) -val flatten_instrs : instr list -> instr list - -val flatten_cdef : cdef -> cdef - val jib_of_ast : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx val compile_ast : Env.t -> out_channel -> string list -> tannot Ast.defs -> unit diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 36a28d9f..27f833d8 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -58,6 +58,7 @@ open Value2 open Anf let opt_debug_function = ref "" +let opt_debug_flow_graphs = ref false let opt_memo_cache = ref false (**************************************************************************) @@ -1174,7 +1175,16 @@ and compile_def' n total ctx = function prerr_endline (Util.header header (List.length arg_ctyps + 2)); prerr_endline (Pretty_print_sail.to_string PPrint.(separate_map hardline pp_instr instrs)) else (); - + + if !opt_debug_flow_graphs then + begin + let instrs = Jib_optimize.(instrs |> optimize_unit |> flatten_instrs) in + let cfg = Jib_ssa.ssa instrs in + let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in + Jib_ssa.make_dot out_chan cfg; + close_out out_chan; + end; + [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx | DEF_fundef (FD_aux (FD_function (_, _, _, []), (l, _))) -> diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli index 173e5c5f..f3bd8c76 100644 --- a/src/jib/jib_compile.mli +++ b/src/jib/jib_compile.mli @@ -55,10 +55,13 @@ open Ast open Ast_util open Jib open Type_check - + +(** Output a dataflow graph for each generated function in Graphviz + (dot) format. *) +val opt_debug_flow_graphs : bool ref + (** Print the IR representation of a specific function. *) val opt_debug_function : string ref - (** {2 Jib context} *) diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml new file mode 100644 index 00000000..889e650e --- /dev/null +++ b/src/jib/jib_optimize.ml @@ -0,0 +1,129 @@ +(**************************************************************************) +(* 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_util +open Jib +open Jib_util + +let optimize_unit instrs = + let unit_cval cval = + match cval_ctyp cval with + | CT_unit -> (F_lit V_unit, CT_unit) + | _ -> cval + in + let unit_instr = function + | I_aux (I_funcall (clexp, extern, id, args), annot) as instr -> + begin match clexp_ctyp clexp with + | CT_unit -> + I_aux (I_funcall (CL_void, extern, id, List.map unit_cval args), annot) + | _ -> instr + end + | I_aux (I_copy (clexp, cval), annot) as instr -> + begin match clexp_ctyp clexp with + | CT_unit -> + I_aux (I_copy (CL_void, unit_cval cval), annot) + | _ -> instr + end + | I_aux (I_alias (clexp, cval), annot) as instr -> + begin match clexp_ctyp clexp with + | CT_unit -> + I_aux (I_alias (CL_void, unit_cval cval), annot) + | _ -> instr + end + | instr -> instr + in + let non_pointless_copy (I_aux (aux, annot)) = + match aux with + | I_copy (CL_void, _) -> false + | _ -> true + in + filter_instrs non_pointless_copy (map_instr_list unit_instr instrs) + +let flat_counter = ref 0 +let flat_id () = + let id = mk_id ("local#" ^ string_of_int !flat_counter) in + incr flat_counter; + id + +let rec flatten_instrs = function + | I_aux (I_decl (ctyp, decl_id), aux) :: instrs -> + let fid = flat_id () in + I_aux (I_decl (ctyp, fid), aux) :: flatten_instrs (instrs_rename decl_id fid instrs) + + | I_aux ((I_block block | I_try_block block), _) :: instrs -> + flatten_instrs block @ flatten_instrs instrs + + | I_aux (I_if (cval, then_instrs, else_instrs, _), _) :: instrs -> + let then_label = label "then_" in + let endif_label = label "endif_" in + [ijump cval then_label] + @ flatten_instrs else_instrs + @ [igoto endif_label] + @ [ilabel then_label] + @ flatten_instrs then_instrs + @ [ilabel endif_label] + @ flatten_instrs instrs + + | I_aux (I_comment _, _) :: instrs -> flatten_instrs instrs + + | instr :: instrs -> instr :: flatten_instrs instrs + | [] -> [] + +let flatten_cdef = + function + | CDEF_fundef (function_id, heap_return, args, body) -> + flat_counter := 0; + CDEF_fundef (function_id, heap_return, args, flatten_instrs body) + + | CDEF_let (n, bindings, instrs) -> + flat_counter := 0; + CDEF_let (n, bindings, flatten_instrs instrs) + + | cdef -> cdef diff --git a/src/jib/jib_optimize.mli b/src/jib/jib_optimize.mli new file mode 100644 index 00000000..beffa81e --- /dev/null +++ b/src/jib/jib_optimize.mli @@ -0,0 +1,63 @@ +(**************************************************************************) +(* 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 Jib + +(** Remove redundant assignments and variables of type + unit. unit-typed identifiers that are assigned to are replaced with + CL_void, and cvals (which should be pure!) are replaced with unit + types are replaced by unit-literals. *) +val optimize_unit : instr list -> instr list + +(** Remove all instructions that can contain other nested + instructions, prodcing a flat list of instructions. *) +val flatten_instrs : instr list -> instr list +val flatten_cdef : cdef -> cdef + diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml new file mode 100644 index 00000000..1f477696 --- /dev/null +++ b/src/jib/jib_ssa.ml @@ -0,0 +1,602 @@ +(**************************************************************************) +(* 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_util +open Jib +open Jib_util + +module IntSet = Set.Make(struct type t = int let compare = compare end) + +(**************************************************************************) +(* 1. Mutable graph type *) +(**************************************************************************) + +type 'a array_graph = { + mutable next : int; + mutable nodes : ('a * IntSet.t * IntSet.t) option array + } + +let make ~initial_size () = { + next = 0; + nodes = Array.make initial_size None + } + +(** Add a vertex to a graph, returning the node index *) +let add_vertex data graph = + let n = graph.next in + if n >= Array.length graph.nodes then + begin + let new_nodes = Array.make (Array.length graph.nodes * 2) None in + Array.blit graph.nodes 0 new_nodes 0 (Array.length graph.nodes); + graph.nodes <- new_nodes + end; + let n = graph.next in + graph.nodes.(n) <- Some (data, IntSet.empty, IntSet.empty); + graph.next <- n + 1; + n + +(** Add an edge between two existing vertices. Raises Invalid_argument + if either of the vertices do not exist. *) +let add_edge n m graph = + begin match graph.nodes.(n) with + | Some (data, parents, children) -> + graph.nodes.(n) <- Some (data, parents, IntSet.add m children) + | None -> + raise (Invalid_argument "Parent node does not exist in graph") + end; + match graph.nodes.(m) with + | Some (data, parents, children) -> + graph.nodes.(m) <- Some (data, IntSet.add n parents, children) + | None -> + raise (Invalid_argument "Child node does not exist in graph") + +let cardinal graph = graph.next + +let reachable roots graph = + let visited = ref IntSet.empty in + + let rec reachable' n = + if IntSet.mem n !visited then () + else + begin + visited := IntSet.add n !visited; + match graph.nodes.(n) with + | Some (_, _, successors) -> + IntSet.iter reachable' successors + | None -> () + end + in + IntSet.iter reachable' roots; !visited + +let prune visited graph = + for i = 0 to graph.next - 1 do + match graph.nodes.(i) with + | Some (n, preds, succs) -> + if IntSet.mem i visited then + graph.nodes.(i) <- Some (n, IntSet.inter visited preds, IntSet.inter visited succs) + else + graph.nodes.(i) <- None + | None -> () + done + +(**************************************************************************) +(* 2. Mutable control flow graph *) +(**************************************************************************) + +type cf_node = + | CF_label of string + | CF_block of instr list + | CF_start + +let control_flow_graph instrs = + let module StringMap = Map.Make(String) in + let labels = ref StringMap.empty in + + let graph = make ~initial_size:512 () in + + iter_instr (fun (I_aux (instr, annot)) -> + match instr with + | I_label label -> + labels := StringMap.add label (add_vertex ([], CF_label label) graph) !labels + | _ -> () + ) (iblock instrs); + + let cf_split (I_aux (aux, _)) = + match aux with + | I_block _ | I_label _ | I_goto _ | I_jump _ | I_if _ | I_end | I_match_failure | I_undefined _ -> true + | _ -> false + in + + let rec cfg preds instrs = + let before, after = instr_split_at cf_split instrs in + let last = match after with + | I_aux (I_label _, _) :: _ -> [] + | instr :: _ -> [instr] + | _ -> [] + in + let preds = match before @ last with + | [] -> preds + | instrs -> + let n = add_vertex ([], CF_block instrs) graph in + List.iter (fun p -> add_edge p n graph) preds; + [n] + in + match after with + | I_aux (I_if (cond, then_instrs, else_instrs, _), _) :: after -> + let t = cfg preds then_instrs in + let e = cfg preds else_instrs in + cfg (t @ e) after + + | I_aux ((I_end | I_match_failure | I_undefined _), _) :: after -> + cfg [] after + + | I_aux (I_goto label, _) :: after -> + List.iter (fun p -> add_edge p (StringMap.find label !labels) graph) preds; + cfg [] after + + | I_aux (I_jump (cval, label), _) :: after -> + List.iter (fun p -> add_edge p (StringMap.find label !labels) graph) preds; + cfg preds after + + | I_aux (I_label label, _) :: after -> + cfg (StringMap.find label !labels :: preds) after + + | I_aux (I_block instrs, _) :: after -> + let m = cfg preds instrs in + cfg m after + + | _ :: after -> assert false + + | [] -> preds + in + + let start = add_vertex ([], CF_start) graph in + let finish = cfg [start] instrs in + + let visited = reachable (IntSet.singleton start) graph in + prune visited graph; + + start, finish, graph + +(**************************************************************************) +(* 3. Computing dominators *) +(**************************************************************************) + +(** Calculate the (immediate) dominators of a graph using the + Lengauer-Tarjan algorithm. This is the slightly less sophisticated + version from Appel's book 'Modern compiler implementation in ML' + which runs in O(n log(n)) time. *) +let immediate_dominators graph root = + let none = -1 in + let vertex = Array.make (cardinal graph) 0 in + let parent = Array.make (cardinal graph) none in + let ancestor = Array.make (cardinal graph) none in + let semi = Array.make (cardinal graph) none in + let idom = Array.make (cardinal graph) none in + let samedom = Array.make (cardinal graph) none in + let best = Array.make (cardinal graph) none in + let dfnum = Array.make (cardinal graph) 0 in + let bucket = Array.make (cardinal graph) IntSet.empty in + + let rec ancestor_with_lowest_semi v = + let a = ancestor.(v) in + if ancestor.(a) <> none then + let b = ancestor_with_lowest_semi a in + ancestor.(v) <- ancestor.(a); + if dfnum.(semi.(b)) < dfnum.(semi.(best.(v))) then + best.(v) <- b + else (); + else (); + if best.(v) <> none then best.(v) else v + in + + let link p n = + ancestor.(n) <- p; + best.(n) <- n + in + + let count = ref 0 in + + let rec dfs p n = + if dfnum.(n) = 0 then + begin + dfnum.(n) <- !count; + vertex.(!count) <- n; + parent.(n) <- p; + incr count; + match graph.nodes.(n) with + | Some (_, _, successors) -> + IntSet.iter (fun w -> dfs n w) successors + | None -> assert false + end + in + dfs none root; + + for i = !count - 1 downto 1 do + let n = vertex.(i) in + let p = parent.(n) in + let s = ref p in + + begin match graph.nodes.(n) with + | Some (_, predecessors, _) -> + IntSet.iter (fun v -> + let s' = + if dfnum.(v) <= dfnum.(n) then + v + else + semi.(ancestor_with_lowest_semi v) + in + if dfnum.(s') < dfnum.(!s) then s := s' + ) predecessors + | None -> assert false + end; + semi.(n) <- !s; + bucket.(!s) <- IntSet.add n bucket.(!s); + link p n; + IntSet.iter (fun v -> + let y = ancestor_with_lowest_semi v in + if semi.(y) = semi.(v) then + idom.(v) <- p + else + samedom.(n) <- y + ) bucket.(p); + done; + for i = 1 to !count - 1 do + let n = vertex.(i) in + if samedom.(n) <> none then + idom.(n) <- idom.(samedom.(n)) + done; + idom + +(** [(dominator_children idoms).(n)] are the nodes whose immediate dominator + (idom) is n. *) +let dominator_children idom = + let none = -1 in + let children = Array.make (Array.length idom) IntSet.empty in + + for n = 0 to Array.length idom - 1 do + let p = idom.(n) in + if p <> none then + children.(p) <- IntSet.add n (children.(p)) + done; + children + +(** [dominate idom n w] is true if n dominates w in the tree of + immediate dominators idom. *) +let rec dominate idom n w = + let none = -1 in + let p = idom.(n) in + if p = none then + false + else if p = w then + true + else + dominate idom p w + +let dominance_frontiers graph root idom children = + let df = Array.make (cardinal graph) IntSet.empty in + + let rec compute_df n = + let set = ref IntSet.empty in + + begin match graph.nodes.(n) with + | Some (content, _, succs) -> + IntSet.iter (fun y -> + if idom.(y) <> n then + set := IntSet.add y !set + ) succs + | None -> () + end; + IntSet.iter (fun c -> + compute_df c; + IntSet.iter (fun w -> + if not (dominate idom n w) then + set := IntSet.add w !set + ) (df.(c)) + ) (children.(n)); + df.(n) <- !set + in + compute_df root; + df + +(**************************************************************************) +(* 4. Conversion to SSA form *) +(**************************************************************************) + +type ssa_elem = + | Phi of Ast.id * Ast.id list + +let place_phi_functions graph df = + let defsites = ref Bindings.empty in + + let all_vars = ref IdSet.empty in + + let rec all_decls = function + | I_aux (I_decl (_, id), _) :: instrs -> + IdSet.add id (all_decls instrs) + | _ :: instrs -> all_decls instrs + | [] -> IdSet.empty + in + + let orig_A n = + match graph.nodes.(n) with + | Some ((_, CF_block instrs), _, _) -> + let vars = List.fold_left IdSet.union IdSet.empty (List.map instr_writes instrs) in + let vars = IdSet.diff vars (all_decls instrs) in + all_vars := IdSet.union vars !all_vars; + vars + | Some _ -> IdSet.empty + | None -> IdSet.empty + in + let phi_A = ref Bindings.empty in + + for n = 0 to graph.next - 1 do + IdSet.iter (fun a -> + let ds = match Bindings.find_opt a !defsites with Some ds -> ds | None -> IntSet.empty in + defsites := Bindings.add a (IntSet.add n ds) !defsites + ) (orig_A n) + done; + + IdSet.iter (fun a -> + let workset = ref (Bindings.find a !defsites) in + while not (IntSet.is_empty !workset) do + let n = IntSet.choose !workset in + workset := IntSet.remove n !workset; + IntSet.iter (fun y -> + let phi_A_a = match Bindings.find_opt a !phi_A with Some set -> set | None -> IntSet.empty in + if not (IntSet.mem y phi_A_a) then + begin + begin match graph.nodes.(y) with + | Some ((phis, cfnode), preds, succs) -> + graph.nodes.(y) <- Some ((Phi (a, Util.list_init (IntSet.cardinal preds) (fun _ -> a)) :: phis, cfnode), preds, succs) + | None -> assert false + end; + phi_A := Bindings.add a (IntSet.add y phi_A_a) !phi_A; + if not (IdSet.mem a (orig_A y)) then + workset := IntSet.add y !workset + end + ) df.(n) + done + ) !all_vars + +let rename_variables graph root children = + let counts = ref Bindings.empty in + let stacks = ref Bindings.empty in + + let get_count id = + match Bindings.find_opt id !counts with Some n -> n | None -> 0 + in + let top_stack id = + match Bindings.find_opt id !stacks with Some (x :: _) -> x | (Some [] | None) -> 0 + in + let push_stack id n = + stacks := Bindings.add id (n :: match Bindings.find_opt id !stacks with Some s -> s | None -> []) !stacks + in + + let rec fold_frag = function + | F_id id -> + let i = top_stack id in + F_id (append_id id ("_" ^ string_of_int i)) + | F_ref id -> + let i = top_stack id in + F_ref (append_id id ("_" ^ string_of_int i)) + | F_lit vl -> F_lit vl + | F_have_exception -> F_have_exception + | F_current_exception -> F_current_exception + | F_op (f1, op, f2) -> F_op (fold_frag f1, op, fold_frag f2) + | F_unary (op, f) -> F_unary (op, fold_frag f) + | F_call (id, fs) -> F_call (id, List.map fold_frag fs) + | F_field (f, field) -> F_field (fold_frag f, field) + | F_raw str -> F_raw str + | F_poly f -> F_poly (fold_frag f) + in + + let rec fold_clexp = function + | CL_id (id, ctyp) -> + let i = get_count id + 1 in + counts := Bindings.add id i !counts; + push_stack id i; + CL_id (append_id id ("_" ^ string_of_int i), ctyp) + | CL_field (clexp, field) -> CL_field (fold_clexp clexp, field) + | CL_addr clexp -> CL_addr (fold_clexp clexp) + | CL_tuple (clexp, n) -> CL_tuple (fold_clexp clexp, n) + | CL_current_exception ctyp -> CL_current_exception ctyp + | CL_have_exception -> CL_have_exception + | CL_return ctyp -> CL_return ctyp + | CL_void -> CL_void + in + + let fold_cval (f, ctyp) = (fold_frag f, ctyp) in + + let ssa_instr (I_aux (aux, annot)) = + let aux = match aux with + | I_funcall (clexp, extern, id, args) -> + let args = List.map fold_cval args in + I_funcall (fold_clexp clexp, extern, id, args) + | I_copy (clexp, cval) -> + let cval = fold_cval cval in + I_copy (fold_clexp clexp, cval) + | I_decl (ctyp, id) -> + let i = get_count id + 1 in + counts := Bindings.add id i !counts; + push_stack id i; + I_decl (ctyp, append_id id ("_" ^ string_of_int i)) + | I_init (ctyp, id, cval) -> + let cval = fold_cval cval in + let i = get_count id + 1 in + counts := Bindings.add id i !counts; + push_stack id i; + I_init (ctyp, append_id id ("_" ^ string_of_int i), cval) + | instr -> instr + in + I_aux (aux, annot) + in + + let ssa_cfnode = function + | CF_start -> CF_start + | CF_block instrs -> CF_block (List.map ssa_instr instrs) + | CF_label label -> CF_label label + in + + let ssa_ssanode = function + | Phi (id, args) -> + let i = get_count id + 1 in + counts := Bindings.add id i !counts; + push_stack id i; + Phi (append_id id ("_" ^ string_of_int i), args) + in + + let fix_phi j = function + | Phi (id, ids) -> + Phi (id, List.mapi (fun k a -> + if k = j then + let i = top_stack a in + append_id a ("_" ^ string_of_int i) + else a) + ids) + in + + let rec rename n = + let old_stacks = !stacks in + begin match graph.nodes.(n) with + | Some ((ssa, cfnode), preds, succs) -> + let ssa = List.map ssa_ssanode ssa in + graph.nodes.(n) <- Some ((ssa, ssa_cfnode cfnode), preds, succs); + List.iter (fun succ -> + match graph.nodes.(succ) with + | Some ((ssa, cfnode), preds, succs) -> + (* Suppose n is the j-th predecessor of succ *) + let rec find_j n succ = function + | pred :: preds -> + if pred = succ then n else find_j (n + 1) succ preds + | [] -> assert false + in + let j = find_j 0 n (IntSet.elements preds) in + graph.nodes.(succ) <- Some ((List.map (fix_phi j) ssa, cfnode), preds, succs) + | None -> assert false + ) (IntSet.elements succs) + | None -> assert false + end; + IntSet.iter (fun child -> rename child) (children.(n)); + stacks := old_stacks + in + rename root + +let ssa instrs = + let start, finish, cfg = control_flow_graph instrs in + let idom = immediate_dominators cfg start in + let children = dominator_children idom in + let df = dominance_frontiers cfg start idom children in + place_phi_functions cfg df; + rename_variables cfg start children; + cfg + +(* Debugging utilities for outputing Graphviz files. *) + +let string_of_phis = function + | [] -> "" + | phis -> Util.string_of_list "\\l" (fun (Phi (id, args)) -> string_of_id id ^ " = phi(" ^ Util.string_of_list ", " string_of_id args ^ ")") phis ^ "\\l" + +let string_of_node = function + | (phis, CF_label label) -> string_of_phis phis ^ label + | (phis, CF_block instrs) -> string_of_phis phis ^ Util.string_of_list "\\l" (fun instr -> String.escaped (Pretty_print_sail.to_string (pp_instr ~short:true instr))) instrs + | (phis, CF_start) -> string_of_phis phis ^ "START" + +let vertex_color = function + | (_, CF_start) -> "peachpuff" + | (_, CF_block _) -> "white" + | (_, CF_label _) -> "springgreen" + +let edge_color node_from node_to = + match node_from, node_to with + | CF_block _, CF_block _ -> "black" + | CF_label _, CF_block _ -> "red" + | CF_block _, CF_label _ -> "blue" + | _, _ -> "deeppink" + +let make_dot out_chan graph = + Util.opt_colors := false; + output_string out_chan "digraph DEPS {\n"; + let make_node i n = + output_string out_chan (Printf.sprintf " n%i [label=\"%s\";shape=box;style=filled;fillcolor=%s];\n" i (string_of_node n) (vertex_color n)) + in + let make_line i s = + output_string out_chan (Printf.sprintf " n%i -> n%i [color=black];\n" i s) + in + for i = 0 to graph.next - 1 do + match graph.nodes.(i) with + | Some (n, _, successors) -> + make_node i n; + IntSet.iter (fun s -> make_line i s) successors + | None -> () + done; + output_string out_chan "}\n"; + Util.opt_colors := true + +let make_dominators_dot out_chan idom graph = + Util.opt_colors := false; + output_string out_chan "digraph DOMS {\n"; + let make_node i n = + output_string out_chan (Printf.sprintf " n%i [label=\"%s\";shape=box;style=filled;fillcolor=%s];\n" i (string_of_node n) (vertex_color n)) + in + let make_line i s = + output_string out_chan (Printf.sprintf " n%i -> n%i [color=black];\n" i s) + in + for i = 0 to Array.length idom - 1 do + match graph.nodes.(i) with + | Some (n, _, _) -> + if idom.(i) = -1 then + make_node i n + else + (make_node i n; make_line i idom.(i)) + | None -> () + done; + output_string out_chan "}\n"; + Util.opt_colors := true diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli new file mode 100644 index 00000000..3796a114 --- /dev/null +++ b/src/jib/jib_ssa.mli @@ -0,0 +1,85 @@ +(**************************************************************************) +(* 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 Array + +(** A mutable array based graph type, with nodes indexed by integers. *) +type 'a array_graph + +(** Create an empty array_graph, specifying the initial size of the + underlying array. *) +val make : initial_size:int -> unit -> 'a array_graph + +(** Add a vertex to a graph, returning the index of the inserted + vertex. If the number of vertices exceeds the size of the + underlying array, then it is dynamically resized. *) +val add_vertex : 'a -> 'a array_graph -> int + +(** Add an edge between two existing vertices. Raises Invalid_argument + if either of the vertices do not exist. *) +val add_edge : int -> int -> 'a array_graph -> unit + +type cf_node = + | CF_label of string + | CF_block of Jib.instr list + | CF_start + +val control_flow_graph : Jib.instr list -> int * int list * ('a list * cf_node) array_graph + +type ssa_elem = + | Phi of Ast.id * Ast.id list + +(** Convert a list of instructions into SSA form *) +val ssa : Jib.instr list -> (ssa_elem list * cf_node) array_graph + +(** Output the control-flow graph in graphviz format for + debugging. Can use 'dot -Tpng X.gv -o X.png' to generate a png + image of the graph. *) +val make_dot : out_channel -> (ssa_elem list * cf_node) array_graph -> unit diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml index 17227875..81cd07ef 100644 --- a/src/jib/jib_util.ml +++ b/src/jib/jib_util.ml @@ -154,6 +154,7 @@ let rec clexp_rename from_id to_id = function | CL_current_exception ctyp -> CL_current_exception ctyp | CL_have_exception -> CL_have_exception | CL_return ctyp -> CL_return ctyp + | CL_void -> CL_void let rec instr_rename from_id to_id (I_aux (instr, aux)) = let instr = match instr with @@ -482,6 +483,7 @@ let rec pp_clexp = function | CL_current_exception ctyp -> string "current_exception : " ^^ pp_ctyp ctyp | CL_have_exception -> string "have_exception" | CL_return ctyp -> string "return : " ^^ pp_ctyp ctyp + | CL_void -> string "void" let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = match instr with @@ -581,40 +583,6 @@ let pp_cdef = function ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace ^^ hardline -(**************************************************************************) -(* 2. Dependency Graphs *) -(**************************************************************************) - -type graph_node = - | G_label of string - | G_instr of int * instr - | G_start - -let string_of_node = function - | G_label label -> label - | G_instr (n, instr) -> string_of_int n ^ ": " ^ Pretty_print_sail.to_string (pp_instr ~short:true instr) - | G_start -> "START" - -module Node = struct - type t = graph_node - let compare gn1 gn2 = - match gn1, gn2 with - | G_label str1, G_label str2 -> String.compare str1 str2 - | G_instr (n1, _), G_instr (n2, _) -> compare n1 n2 - | G_start , G_start -> 0 - | G_start , _ -> 1 - | _ , G_start -> -1 - | G_instr _, _ -> 1 - | _ , G_instr _ -> -1 -end - -module NodeGraph = Graph.Make(Node) - -module NM = Map.Make(Node) -module NS = Set.Make(Node) - -type dep_graph = NodeGraph.graph - let rec fragment_deps = function | F_id id | F_ref id -> IdSet.singleton id | F_lit _ -> IdSet.empty @@ -635,6 +603,7 @@ let rec clexp_deps = function | CL_have_exception -> IdSet.empty | CL_current_exception _ -> IdSet.empty | CL_return _ -> IdSet.empty + | CL_void -> IdSet.empty (* Return the direct, read/write dependencies of a single instruction *) let instr_deps = function @@ -646,7 +615,7 @@ let instr_deps = function | I_funcall (clexp, _, _, cvals) -> List.fold_left IdSet.union IdSet.empty (List.map cval_deps cvals), clexp_deps clexp | I_copy (clexp, cval) -> cval_deps cval, clexp_deps clexp | I_alias (clexp, cval) -> cval_deps cval, clexp_deps clexp - | I_clear (_, id) -> IdSet.singleton id, IdSet.singleton id + | I_clear (_, id) -> IdSet.singleton id, IdSet.empty | I_throw cval | I_return cval -> cval_deps cval, IdSet.empty | I_block _ | I_try_block _ -> IdSet.empty, IdSet.empty | I_comment _ | I_raw _ -> IdSet.empty, IdSet.empty @@ -656,80 +625,6 @@ let instr_deps = function | I_match_failure -> IdSet.empty, IdSet.empty | I_end -> IdSet.empty, IdSet.empty -(* instrs_graph returns the control-flow graph for a list of - instructions. *) -let instrs_graph instrs = - let icounter = ref 0 in - let graph = ref NodeGraph.empty in - - let rec add_instr last_instrs (I_aux (instr, _) as iaux) = - incr icounter; - let node = G_instr (!icounter, iaux) in - match instr with - | I_block instrs | I_try_block instrs -> - List.fold_left add_instr last_instrs instrs - | I_if (_, then_instrs, else_instrs, _) -> - List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs; - let n1 = List.fold_left add_instr [node] then_instrs in - let n2 = List.fold_left add_instr [node] else_instrs in - incr icounter; - let join = G_instr (!icounter, icomment "join") in - List.iter (fun i -> graph := NodeGraph.add_edge' i join !graph) n1; - List.iter (fun i -> graph := NodeGraph.add_edge' i join !graph) n2; - [join] - | I_return _ -> - List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs; - [] - | I_label label -> - graph := NodeGraph.add_edge' (G_label label) node !graph; - node :: last_instrs - | I_goto label -> - List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs; - graph := NodeGraph.add_edge' node (G_label label) !graph; - [] - | I_jump (cval, label) -> - List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs; - graph := NodeGraph.add_edges' (G_label label) [] !graph; - [node] - | I_match_failure -> - List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs; - [] - | _ -> - List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs; - [node] - in - ignore (List.fold_left add_instr [G_start] instrs); - let graph = NodeGraph.fix_leaves !graph in - graph - -let make_dot id graph = - Util.opt_colors := false; - let to_string node = String.escaped (string_of_node node) in - let node_color = function - | G_start -> "lightpink" - | G_instr (_, I_aux (I_decl _, _)) -> "olivedrab1" - | G_instr (_, I_aux (I_init _, _)) -> "springgreen" - | G_instr (_, I_aux (I_clear _, _)) -> "peachpuff" - | G_instr (_, I_aux (I_goto _, _)) -> "orange1" - | G_instr (_, I_aux (I_label _, _)) -> "white" - | G_instr (_, I_aux (I_raw _, _)) -> "khaki" - | G_instr (_, I_aux (I_return _, _)) -> "deeppink" - | G_instr (_, I_aux (I_undefined _, _)) -> "deeppink" - | G_instr _ -> "azure" - | G_label _ -> "lightpink" - in - let edge_color from_node to_node = - match from_node, to_node with - | G_start , _ -> "goldenrod4" - | G_label _, _ -> "darkgreen" - | _ , G_label _ -> "goldenrod4" - | G_instr _, G_instr _ -> "black" - | _ , _ -> "coral3" - in - let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in - NodeGraph.make_dot node_color edge_color to_string out_chan graph; - close_out out_chan - let rec map_clexp_ctyp f = function | CL_id (id, ctyp) -> CL_id (id, f ctyp) | CL_field (clexp, field) -> CL_field (map_clexp_ctyp f clexp, field) @@ -738,6 +633,7 @@ let rec map_clexp_ctyp f = function | CL_current_exception ctyp -> CL_current_exception (f ctyp) | CL_have_exception -> CL_have_exception | CL_return ctyp -> CL_return (f ctyp) + | CL_void -> CL_void let rec map_instr_ctyp f (I_aux (instr, aux)) = let instr = match instr with @@ -778,6 +674,18 @@ let rec map_instr f (I_aux (instr, aux)) = in f (I_aux (instr, aux)) +(** Iterate over each instruction within an instruction, bottom-up *) +let rec iter_instr f (I_aux (instr, aux)) = + match instr with + | I_decl _ | I_init _ | I_reset _ | I_reinit _ + | I_funcall _ | I_copy _ | I_alias _ | I_clear _ | I_jump _ | I_throw _ | I_return _ + | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ | I_end -> f (I_aux (instr, aux)) + | I_if (cval, instrs1, instrs2, ctyp) -> + List.iter (iter_instr f) instrs1; + List.iter (iter_instr f) instrs2 + | I_block instrs | I_try_block instrs -> + List.iter (iter_instr f) instrs + (** Map over each instruction in a cdef using map_instr *) let cdef_map_instr f = function | CDEF_reg_dec (id, ctyp, instrs) -> CDEF_reg_dec (id, ctyp, List.map (map_instr f) instrs) @@ -816,17 +724,21 @@ let rec map_instrs f (I_aux (instr, aux)) = in I_aux (instr, aux) +let map_instr_list f instrs = + List.map (map_instr f) instrs + +let map_instrs_list f instrs = + f (List.map (map_instrs f) instrs) + let rec instr_ids (I_aux (instr, _)) = let reads, writes = instr_deps instr in - IdSet.of_list (IdSet.elements reads @ IdSet.elements writes) + IdSet.union reads writes let rec instr_reads (I_aux (instr, _)) = - let reads, _ = instr_deps instr in - IdSet.of_list (IdSet.elements reads) + fst (instr_deps instr) let rec instr_writes (I_aux (instr, _)) = - let _, writes = instr_deps instr in - IdSet.of_list (IdSet.elements writes) + snd (instr_deps instr) let rec filter_instrs f instrs = let filter_instrs' = function @@ -878,6 +790,7 @@ let rec clexp_ctyp = function end | CL_have_exception -> CT_bool | CL_current_exception ctyp -> ctyp + | CL_void -> CT_unit let rec instr_ctyps (I_aux (instr, aux)) = match instr with @@ -933,3 +846,29 @@ let instr_split_at f = | instr :: instrs -> instr_split_at' f (instr :: before) instrs in instr_split_at' f [] + +let rec instrs_rename from_id to_id = + let rename id = if Id.compare id from_id = 0 then to_id else id in + let crename = cval_rename from_id to_id in + let irename instrs = instrs_rename from_id to_id instrs in + let lrename = clexp_rename from_id to_id in + function + | (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Id.compare from_id new_id = 0 -> instrs + | I_aux (I_decl (ctyp, new_id), aux) :: instrs -> I_aux (I_decl (ctyp, new_id), aux) :: irename instrs + | I_aux (I_reset (ctyp, id), aux) :: instrs -> I_aux (I_reset (ctyp, rename id), aux) :: irename instrs + | I_aux (I_init (ctyp, id, cval), aux) :: instrs -> I_aux (I_init (ctyp, rename id, crename cval), aux) :: irename instrs + | I_aux (I_reinit (ctyp, id, cval), aux) :: instrs -> I_aux (I_reinit (ctyp, rename id, crename cval), aux) :: irename instrs + | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs -> + I_aux (I_if (crename cval, irename then_instrs, irename else_instrs, ctyp), aux) :: irename instrs + | I_aux (I_jump (cval, label), aux) :: instrs -> I_aux (I_jump (crename cval, label), aux) :: irename instrs + | I_aux (I_funcall (clexp, extern, id, cvals), aux) :: instrs -> + I_aux (I_funcall (lrename clexp, extern, rename id, List.map crename cvals), aux) :: irename instrs + | I_aux (I_copy (clexp, cval), aux) :: instrs -> I_aux (I_copy (lrename clexp, crename cval), aux) :: irename instrs + | I_aux (I_alias (clexp, cval), aux) :: instrs -> I_aux (I_alias (lrename clexp, crename cval), aux) :: irename instrs + | I_aux (I_clear (ctyp, id), aux) :: instrs -> I_aux (I_clear (ctyp, rename id), aux) :: irename instrs + | I_aux (I_return cval, aux) :: instrs -> I_aux (I_return (crename cval), aux) :: irename instrs + | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (irename block), aux) :: irename instrs + | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (irename block), aux) :: irename instrs + | I_aux (I_throw cval, aux) :: instrs -> I_aux (I_throw (crename cval), aux) :: irename instrs + | (I_aux ((I_comment _ | I_raw _ | I_end | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs + | [] -> [] diff --git a/src/sail.ml b/src/sail.ml index 50719776..b654831b 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -290,7 +290,7 @@ let options = Arg.align ([ Arg.String (fun l -> opt_ddump_rewrite_ast := Some (l, 0)), "<prefix> (debug) dump the ast after each rewriting step to <prefix>_<i>.lem"); ( "-ddump_flow_graphs", - Arg.Set C_backend.opt_debug_flow_graphs, + Arg.Set Jib_compile.opt_debug_flow_graphs, " (debug) dump flow analysis for Sail functions when compiling to C"); ( "-dtc_verbose", Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity), diff --git a/src/sail.odocl b/src/sail.odocl index 4e91e22e..0a45eba3 100644 --- a/src/sail.odocl +++ b/src/sail.odocl @@ -11,6 +11,7 @@ specialize anf jib jib_compile +jib_ssa jib_util util graph
\ No newline at end of file |