C: Wrap Jib identifiers

Avoids duplication between l-expressions and expressions. Also means that
special variables like current_exception and have_exception are treated
normally by functions such as instr_reads and instr_writes etc. Furthermore
we can now easily annotate Jib identifiers in ways that were not previously
possible with plain sail ids.

1 files changed, 43 insertions, 41 deletions

diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index 9ce3c3f0..470b646b 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -357,47 +357,47 @@ let dominance_frontiers graph root idom children =
 (**************************************************************************)
 
 type ssa_elem =
-  | Phi of Ast.id * Ast.id list
+  | Phi of Jib.name * Jib.name list
   | Pi of Jib.cval list
 
 let place_phi_functions graph df =
-  let defsites = ref Bindings.empty in
+  let defsites = ref NameMap.empty in
 
-  let all_vars = ref IdSet.empty in
+  let all_vars = ref NameSet.empty in
 
   let rec all_decls = function
     | I_aux ((I_init (_, id, _) | I_decl (_, id)), _) :: instrs ->
-       IdSet.add id (all_decls instrs)
+       NameSet.add id (all_decls instrs)
     | _ :: instrs -> all_decls instrs
-    | [] -> IdSet.empty
+    | [] -> NameSet.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;
+       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;
        vars
-    | Some _ -> IdSet.empty
-    | None -> IdSet.empty
+    | Some _ -> NameSet.empty
+    | None -> NameSet.empty
   in
-  let phi_A = ref Bindings.empty in
+  let phi_A = ref NameMap.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
+    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
       ) (orig_A n)
   done;
 
-  IdSet.iter (fun a ->
-      let workset = ref (Bindings.find a !defsites) in
+  NameSet.iter (fun a ->
+      let workset = ref (NameMap.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
+            let phi_A_a = match NameMap.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
@@ -405,8 +405,8 @@ let place_phi_functions graph df =
                    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
+                phi_A := NameMap.add a (IntSet.add y phi_A_a) !phi_A;
+                if not (NameSet.mem a (orig_A y)) then
                   workset := IntSet.add y !workset
               end
           ) df.(n)
@@ -414,29 +414,34 @@ let place_phi_functions graph df =
     ) !all_vars
 
 let rename_variables graph root children =
-  let counts = ref Bindings.empty in
-  let stacks = ref Bindings.empty in
+  let counts = ref NameMap.empty in
+  let stacks = ref NameMap.empty in
 
   let get_count id =
-    match Bindings.find_opt id !counts with Some n -> n | None -> 0
+    match NameMap.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
+    match NameMap.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
+    stacks := NameMap.add id (n :: match NameMap.find_opt id !stacks with Some s -> s | None -> []) !stacks
   in
 
+  let ssa_name i = function
+    | Name (id, _) -> Name (id, i)
+    | Have_exception _ -> Have_exception i
+    | Current_exception _ -> Current_exception i
+    | Return _ -> Return i
+  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_id (ssa_name i id)
     | F_ref id ->
        let i = top_stack id in
-       F_ref (append_id id ("_" ^ string_of_int i))
+       F_ref (ssa_name i id)
     | 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)
@@ -448,15 +453,12 @@ let rename_variables graph root children =
   let rec fold_clexp = function
     | CL_id (id, ctyp) ->
        let i = get_count id + 1 in
-       counts := Bindings.add id i !counts;
+       counts := NameMap.add id i !counts;
        push_stack id i;
-       CL_id (append_id id ("_" ^ string_of_int i), ctyp)
+       CL_id (ssa_name i id, 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
 
@@ -472,15 +474,15 @@ let rename_variables graph root children =
          I_copy (fold_clexp clexp, cval)
       | I_decl (ctyp, id) ->
          let i = get_count id + 1 in
-         counts := Bindings.add id i !counts;
+         counts := NameMap.add id i !counts;
          push_stack id i;
-         I_decl (ctyp, append_id id ("_" ^ string_of_int i))
+         I_decl (ctyp, ssa_name i id)
       | I_init (ctyp, id, cval) ->
          let cval = fold_cval cval in
          let i = get_count id + 1 in
-         counts := Bindings.add id i !counts;
+         counts := NameMap.add id i !counts;
          push_stack id i;
-         I_init (ctyp, append_id id ("_" ^ string_of_int i), cval)
+         I_init (ctyp, ssa_name i id, cval)
       | I_jump (cval, label) ->
          I_jump (fold_cval cval, label)
       | instr -> instr
@@ -498,9 +500,9 @@ let rename_variables graph root children =
   let ssa_ssanode = function
     | Phi (id, args) ->
        let i = get_count id + 1 in
-       counts := Bindings.add id i !counts;
+       counts := NameMap.add id i !counts;
        push_stack id i;
-       Phi (append_id id ("_" ^ string_of_int i), args)
+       Phi (ssa_name i id, args)
     | Pi _ -> assert false (* Should not be introduced at this point *)
   in
 
@@ -509,7 +511,7 @@ let rename_variables graph root children =
        Phi (id, List.mapi (fun k a ->
                     if k = j then
                       let i = top_stack a in
-                      append_id a ("_" ^ string_of_int i)
+                      ssa_name i a
                     else a)
                   ids)
     | Pi _ -> assert false (* Should not be introduced at this point *)
@@ -603,7 +605,7 @@ let ssa instrs =
 
 let string_of_ssainstr = function
   | Phi (id, args) ->
-     string_of_id id ^ " = &phi;(" ^ Util.string_of_list ", " string_of_id args ^ ")"
+     string_of_name id ^ " = &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 ^ ")"