C: Add identifier to end instruction

Allows us to track the last version of the return variable when the AST
in in SSA form.

5 files changed, 40 insertions, 21 deletions

diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index a784b08e..0e73fed8 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -624,7 +624,7 @@ let fix_early_heap_return ret ret_ctyp instrs =
   let end_function_label = label "end_function_" in
   let is_return_recur (I_aux (instr, _)) =
     match instr with
-    | I_if _ | I_block _ | I_end | I_funcall _ | I_copy _ | I_undefined _ -> true
+    | I_if _ | I_block _ | I_end _ | I_funcall _ | I_copy _ | I_undefined _ -> true
     | _ -> false
   in
   let rec rewrite_return instrs =
@@ -646,7 +646,7 @@ let fix_early_heap_return ret ret_ctyp instrs =
        before
        @ [I_aux (I_copy (CL_addr (CL_id (ret, CT_ref ctyp)), cval), aux)]
        @ rewrite_return after
-    | before, I_aux ((I_end | I_undefined _), _) :: after ->
+    | before, I_aux ((I_end _ | I_undefined _), _) :: after ->
        before
        @ [igoto end_function_label]
        @ rewrite_return after
@@ -661,7 +661,7 @@ let fix_early_heap_return ret ret_ctyp instrs =
 let fix_early_stack_return ret ret_ctyp instrs =
   let is_return_recur (I_aux (instr, _)) =
     match instr with
-    | I_if _ | I_block _ | I_end | I_funcall _ | I_copy _ -> true
+    | I_if _ | I_block _ | I_end _ | I_funcall _ | I_copy _ -> true
     | _ -> false
   in
   let rec rewrite_return instrs =
@@ -683,7 +683,7 @@ let fix_early_stack_return ret ret_ctyp instrs =
        before
        @ [I_aux (I_copy (CL_id (ret, ctyp), cval), aux)]
        @ rewrite_return after
-    | before, I_aux (I_end, _) :: after ->
+    | before, I_aux (I_end _, _) :: after ->
        before
        @ [ireturn (F_id ret, ret_ctyp)]
        @ rewrite_return after
@@ -1468,7 +1468,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
   | I_raw str ->
      string ("  " ^ str)
 
-  | I_end -> assert false
+  | I_end _ -> assert false
 
   | I_match_failure ->
      string ("  sail_match_failure(\"" ^ String.escaped (string_of_id fid) ^ "\");")
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index c13b814f..d74d3c0b 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -974,7 +974,7 @@ let rec map_try_block f (I_aux (instr, aux)) =
     | I_funcall _ | I_copy _ | I_clear _ | I_throw _ | I_return _ -> instr
     | I_block instrs -> I_block (List.map (map_try_block f) instrs)
     | I_try_block instrs -> I_try_block (f (List.map (map_try_block f) instrs))
-    | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_jump _ | I_match_failure | I_undefined _ | I_end -> instr
+    | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_jump _ | I_match_failure | I_undefined _ | I_end _ -> instr
   in
   I_aux (instr, aux)
 
@@ -1194,7 +1194,7 @@ and compile_def' n total ctx = function
          let instrs = Jib_optimize.(instrs |> optimize_unit |> flatten_instrs) in
          let root, _, cfg = Jib_ssa.control_flow_graph instrs in
          let idom = Jib_ssa.immediate_dominators cfg root in
-         let cfg = Jib_ssa.ssa 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;
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index cbef761d..e0ff4849 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -68,6 +68,15 @@ let make ~initial_size () = {
     nodes = Array.make initial_size None
   }
 
+let get_vertex graph n = graph.nodes.(n)
+
+let iter_graph f graph =
+  for n = 0 to graph.next - 1 do
+    match graph.nodes.(n) with
+    | Some (x, y, z) -> f x y z
+    | None -> ()
+  done
+                       
 (** Add a vertex to a graph, returning the node index *)
 let add_vertex data graph =
   let n = graph.next in
@@ -153,7 +162,7 @@ let control_flow_graph 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
+    | I_block _ | I_label _ | I_goto _ | I_jump _ | I_if _ | I_end _ | I_match_failure | I_undefined _ -> true
     | _ -> false
   in
 
@@ -177,7 +186,7 @@ let control_flow_graph instrs =
        let e = cfg preds else_instrs in
        cfg (t @ e) after
 
-    | I_aux ((I_end | I_match_failure | I_undefined _), _) :: after ->
+    | I_aux ((I_end _ | I_match_failure | I_undefined _), _) :: after ->
        cfg [] after
 
     | I_aux (I_goto label, _) :: after ->
@@ -485,6 +494,9 @@ let rename_variables graph root children =
          I_init (ctyp, ssa_name i id, cval)
       | I_jump (cval, label) ->
          I_jump (fold_cval cval, label)
+      | I_end id ->
+         let i = top_stack id in
+         I_end (ssa_name i id)
       | instr -> instr
     in
     I_aux (aux, annot)
@@ -600,7 +612,7 @@ let ssa instrs =
   rename_variables cfg start children;
   place_pi_functions cfg start idom children;
   (* remove_guard_nodes (function CF_guard _ -> true | CF_label _ -> true | _ -> false) cfg; *)
-  cfg
+  start, cfg
 
 (* Debugging utilities for outputing Graphviz files. *)
 
diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli
index 0dba6edf..b146861c 100644
--- a/src/jib/jib_ssa.mli
+++ b/src/jib/jib_ssa.mli
@@ -57,6 +57,12 @@ type 'a array_graph
    underlying array. *)
 val make : initial_size:int -> unit -> 'a array_graph
 
+module IntSet : Set.S with type elt = int
+  
+val get_vertex : 'a array_graph -> int -> ('a * IntSet.t * IntSet.t) option
+
+val iter_graph : ('a -> IntSet.t -> IntSet.t -> unit) -> 'a array_graph -> unit
+  
 (** 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. *)
@@ -83,7 +89,7 @@ type ssa_elem =
   | Pi of Jib.cval list
 
 (** Convert a list of instructions into SSA form *)
-val ssa : Jib.instr list -> (ssa_elem list * cf_node) array_graph
+val ssa : Jib.instr list -> int * (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
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 3f7b14c0..76d7b5d2 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -95,7 +95,7 @@ let ireturn ?loc:(l=Parse_ast.Unknown) cval =
   I_aux (I_return cval, (instr_number (), l))
 
 let iend ?loc:(l=Parse_ast.Unknown) () =
-  I_aux (I_end, (instr_number (), l))
+  I_aux (I_end (Return (-1)), (instr_number (), l))
 
 let iblock ?loc:(l=Parse_ast.Unknown) instrs =
   I_aux (I_block instrs, (instr_number (), l))
@@ -226,7 +226,8 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) =
 
     | I_match_failure -> I_match_failure
 
-    | I_end -> I_end
+    | I_end id when Name.compare id from_id = 0 -> I_end to_id
+    | I_end id -> I_end id
 
     | I_reset (ctyp, id) when Name.compare id from_id = 0 -> I_reset (ctyp, to_id)
     | I_reset (ctyp, id) -> I_reset (ctyp, id)
@@ -563,7 +564,7 @@ let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) =
      pp_keyword "goto" ^^ string (str |> Util.blue |> Util.clear)
   | I_match_failure ->
      pp_keyword "match_failure"
-  | I_end ->
+  | I_end _ ->
      pp_keyword "end"
   | I_undefined ctyp ->
      pp_keyword "undefined" ^^ pp_ctyp ctyp
@@ -646,7 +647,7 @@ let instr_deps = function
   | I_goto label -> NameSet.empty, NameSet.empty
   | I_undefined _ -> NameSet.empty, NameSet.empty
   | I_match_failure -> NameSet.empty, NameSet.empty
-  | I_end -> NameSet.empty, NameSet.empty
+  | I_end id -> NameSet.singleton id, NameSet.empty
 
 module NameCT = struct
   type t = name * ctyp
@@ -697,7 +698,7 @@ let rec map_instr_ctyp f (I_aux (instr, aux)) =
     | I_undefined ctyp -> I_undefined (f ctyp)
     | I_reset (ctyp, id) -> I_reset (f ctyp, id)
     | I_reinit (ctyp1, id, (frag, ctyp2)) -> I_reinit (f ctyp1, id, (frag, f ctyp2))
-    | I_end -> I_end
+    | I_end id -> I_end id
     | (I_comment _ | I_raw _ | I_label _ | I_goto _ | I_match_failure) as instr -> instr
   in
   I_aux (instr, aux)
@@ -707,7 +708,7 @@ let rec map_instr f (I_aux (instr, aux)) =
   let instr = match instr with
     | I_decl _ | I_init _ | I_reset _ | I_reinit _
       | I_funcall _ | I_copy _ | I_clear _ | I_jump _ | I_throw _ | I_return _
-      | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ | I_end -> instr
+      | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ | I_end _ -> instr
     | I_if (cval, instrs1, instrs2, ctyp) ->
        I_if (cval, List.map (map_instr f) instrs1, List.map (map_instr f) instrs2, ctyp)
     | I_block instrs ->
@@ -722,7 +723,7 @@ 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_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_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
@@ -763,7 +764,7 @@ let rec map_instrs f (I_aux (instr, aux)) =
     | I_funcall _ | I_copy _ | I_clear _ | I_jump _ | I_throw _ | I_return _ -> instr
     | I_block instrs -> I_block (f (List.map (map_instrs f) instrs))
     | I_try_block instrs -> I_try_block (f (List.map (map_instrs f) instrs))
-    | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _  | I_end -> instr
+    | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _  | I_end _ -> instr
   in
   I_aux (instr, aux)
 
@@ -851,7 +852,7 @@ let rec instr_ctyps (I_aux (instr, aux)) =
      instrs_ctyps instrs
   | I_throw cval | I_jump (cval, _) | I_return cval ->
      CTSet.singleton (cval_ctyp cval)
-  | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_end ->
+  | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_end _ ->
      CTSet.empty
 
 and instrs_ctyps instrs = List.fold_left CTSet.union CTSet.empty (List.map instr_ctyps instrs)
@@ -909,5 +910,5 @@ let rec instrs_rename from_id to_id =
   | 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
+  | (I_aux ((I_comment _ | I_raw _ | I_end _ | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs
   | [] -> []