Jib: Add types to Phi functions

Add a test case to ensure variable types in l-expressions remain the
same with flow-sensitive constraints.

4 files changed, 60 insertions, 35 deletions

diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 87e0b050..15f945e5 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -824,7 +824,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let body_gs = ngensym () in
 
      let loop_var = name loop_var in
-     
+
      variable_init from_gs from_setup from_call from_cleanup
      @ variable_init to_gs to_setup to_call to_cleanup
      @ variable_init step_gs step_setup step_call step_cleanup
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index 470b646b..cbef761d 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -357,56 +357,56 @@ let dominance_frontiers graph root idom children =
 (**************************************************************************)
 
 type ssa_elem =
-  | Phi of Jib.name * Jib.name list
+  | Phi of Jib.name * Jib.ctyp * Jib.name list
   | Pi of Jib.cval list
 
 let place_phi_functions graph df =
-  let defsites = ref NameMap.empty in
+  let defsites = ref NameCTMap.empty in
 
-  let all_vars = ref NameSet.empty in
+  let all_vars = ref NameCTSet.empty in
 
   let rec all_decls = function
-    | I_aux ((I_init (_, id, _) | I_decl (_, id)), _) :: instrs ->
-       NameSet.add id (all_decls instrs)
+    | I_aux ((I_init (ctyp, id, _) | I_decl (ctyp, id)), _) :: instrs ->
+       NameCTSet.add (id, ctyp) (all_decls instrs)
     | _ :: instrs -> all_decls instrs
-    | [] -> NameSet.empty
+    | [] -> NameCTSet.empty
   in
 
   let orig_A n =
     match graph.nodes.(n) with
     | Some ((_, CF_block instrs), _, _) ->
-       let vars = List.fold_left NameSet.union NameSet.empty (List.map instr_writes instrs) in
-       let vars = NameSet.diff vars (all_decls instrs) in
-       all_vars := NameSet.union vars !all_vars;
+       let vars = List.fold_left NameCTSet.union NameCTSet.empty (List.map instr_typed_writes instrs) in
+       let vars = NameCTSet.diff vars (all_decls instrs) in
+       all_vars := NameCTSet.union vars !all_vars;
        vars
-    | Some _ -> NameSet.empty
-    | None -> NameSet.empty
+    | Some _ -> NameCTSet.empty
+    | None -> NameCTSet.empty
   in
-  let phi_A = ref NameMap.empty in
+  let phi_A = ref NameCTMap.empty in
 
   for n = 0 to graph.next - 1 do
-    NameSet.iter (fun a ->
-        let ds = match NameMap.find_opt a !defsites with Some ds -> ds | None -> IntSet.empty in
-        defsites := NameMap.add a (IntSet.add n ds) !defsites
+    NameCTSet.iter (fun a ->
+        let ds = match NameCTMap.find_opt a !defsites with Some ds -> ds | None -> IntSet.empty in
+        defsites := NameCTMap.add a (IntSet.add n ds) !defsites
       ) (orig_A n)
   done;
 
-  NameSet.iter (fun a ->
-      let workset = ref (NameMap.find a !defsites) in
+  NameCTSet.iter (fun a ->
+      let workset = ref (NameCTMap.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 NameMap.find_opt a !phi_A with Some set -> set | None -> IntSet.empty in
+            let phi_A_a = match NameCTMap.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)
+                   graph.nodes.(y) <- Some ((Phi (fst a, snd a, Util.list_init (IntSet.cardinal preds) (fun _ -> fst a)) :: phis, cfnode), preds, succs)
                 | None -> assert false
                 end;
-                phi_A := NameMap.add a (IntSet.add y phi_A_a) !phi_A;
-                if not (NameSet.mem a (orig_A y)) then
+                phi_A := NameCTMap.add a (IntSet.add y phi_A_a) !phi_A;
+                if not (NameCTSet.mem a (orig_A y)) then
                   workset := IntSet.add y !workset
               end
           ) df.(n)
@@ -433,7 +433,7 @@ let rename_variables graph root children =
     | Current_exception _ -> Current_exception i
     | Return _ -> Return i
   in
-  
+
   let rec fold_frag = function
     | F_id id ->
        let i = top_stack id in
@@ -498,22 +498,23 @@ let rename_variables graph root children =
   in
 
   let ssa_ssanode = function
-    | Phi (id, args) ->
+    | Phi (id, ctyp, args) ->
        let i = get_count id + 1 in
        counts := NameMap.add id i !counts;
        push_stack id i;
-       Phi (ssa_name i id, args)
+       Phi (ssa_name i id, ctyp, args)
     | Pi _ -> assert false (* Should not be introduced at this point *)
   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
-                      ssa_name i a
-                    else a)
-                  ids)
+    | Phi (id, ctyp, ids) ->
+       let fix_arg k a =
+         if k = j then
+           let i = top_stack a in
+           ssa_name i a
+         else a
+       in
+       Phi (id, ctyp, List.mapi fix_arg ids)
     | Pi _ -> assert false (* Should not be introduced at this point *)
   in
 
@@ -604,8 +605,8 @@ let ssa instrs =
 (* Debugging utilities for outputing Graphviz files. *)
 
 let string_of_ssainstr = function
-  | Phi (id, args) ->
-     string_of_name id ^ " = &phi;(" ^ Util.string_of_list ", " string_of_name args ^ ")"
+  | Phi (id, ctyp, args) ->
+     string_of_name id ^ " : " ^ string_of_ctyp ctyp ^ " = &phi;(" ^ Util.string_of_list ", " string_of_name args ^ ")"
   | Pi cvals ->
      "&pi;(" ^ Util.string_of_list ", " (fun (f, _) -> String.escaped (string_of_fragment ~zencode:false f)) cvals ^ ")"
 
diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli
index 8cfdb198..0dba6edf 100644
--- a/src/jib/jib_ssa.mli
+++ b/src/jib/jib_ssa.mli
@@ -79,7 +79,7 @@ val control_flow_graph : Jib.instr list -> int * int list * ('a list * cf_node)
 val immediate_dominators : 'a array_graph -> int -> int array
 
 type ssa_elem =
-  | Phi of Jib.name * Jib.name list
+  | Phi of Jib.name * Jib.ctyp * Jib.name list
   | Pi of Jib.cval list
 
 (** Convert a list of instructions into SSA form *)
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 99de19ef..3f7b14c0 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -648,6 +648,30 @@ let instr_deps = function
   | I_match_failure -> NameSet.empty, NameSet.empty
   | I_end -> NameSet.empty, NameSet.empty
 
+module NameCT = struct
+  type t = name * ctyp
+  let compare (n1, ctyp1) (n2, ctyp2) =
+    let c = Name.compare n1 n2 in
+    if c = 0 then CT.compare ctyp1 ctyp2 else c
+end
+
+module NameCTSet = Set.Make(NameCT)
+module NameCTMap = Map.Make(NameCT)
+
+let rec clexp_typed_writes = function
+  | CL_id (id, ctyp) -> NameCTSet.singleton (id, ctyp)
+  | CL_field (clexp, _) -> clexp_typed_writes clexp
+  | CL_tuple (clexp, _) -> clexp_typed_writes clexp
+  | CL_addr clexp -> clexp_typed_writes clexp
+  | CL_void -> NameCTSet.empty
+
+let instr_typed_writes (I_aux (aux, _)) =
+  match aux with
+  | I_decl (ctyp, id) | I_reset (ctyp, id) -> NameCTSet.singleton (id, ctyp)
+  | I_init (ctyp, id, _) | I_reinit (ctyp, id, _) -> NameCTSet.singleton (id, ctyp)
+  | I_funcall (clexp, _, _, _) | I_copy (clexp, _) -> clexp_typed_writes clexp
+  | _ -> NameCTSet.empty
+
 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)