SMT: Add explicit terminators to SSA graph

Makes the graph slightly cleaner, and means we can represent
conditionals in a way that shoud allow computing path conditions much
easier.

Essentially rather than a basic block being a list of instructions
where the last instruction is a jump (or other terminator) it is now a
list of instructions combined with an explict terminator, i.e.

CF_block (instrs @ I_jump (cval, label) ==> CF_block (instrs, T_jump (n, label))

Rather than storing the cval in the T_jump it just has a number that
links to a mapping from numbers to cvals, and we represent the
negation of any cval in that table by negating its number. Therefore
at any join point in the CFG, we can efficiently check when the
joining path conditionals contain both n and minus n and remove both.

3 files changed, 112 insertions, 54 deletions

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 350f50d9..de5feca1 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1343,6 +1343,19 @@ let rmw_modify smt = function
      end
   | _ -> assert false
 
+let smt_terminator ctx =
+  let open Jib_ssa in
+  function
+  | T_end id ->
+     add_event ctx Return (Var (zencode_name id));
+     []
+
+  | T_match_failure ->
+     add_pathcond_event ctx Match;
+     []
+
+  | T_undefined _ | T_goto _ | T_jump _ | T_label _ | T_none -> []
+
 (* For a basic block (contained in a control-flow node / cfnode), we
    turn the instructions into a sequence of define-const and
    declare-const expressions. Because we are working with a SSA graph,
@@ -1421,21 +1434,11 @@ let smt_instr ctx =
      end;
      [declare_const ctx id ctyp]
 
-  | I_aux (I_end id, _) ->
-     add_event ctx Return (Var (zencode_name id));
-     []
-
   | I_aux (I_clear _, _) -> []
 
-  | I_aux (I_match_failure, _) ->
-     add_pathcond_event ctx Match;
-     []
-
-  | I_aux (I_undefined ctyp, _) -> []
-
-  (* I_jump and I_goto will only appear as terminators for basic blocks. *)
-  | I_aux ((I_jump _ | I_goto _), _) -> []
-
+  (* Should only appear as terminators for basic blocks. *)
+  | I_aux ((I_jump _ | I_goto _ | I_end _ | I_match_failure | I_undefined _), (_, l)) ->
+     Reporting.unreachable l __POS__ "SMT: Instruction should only appear as block terminator"
 
   | instr ->
      failwith ("Cannot translate: " ^ Pretty_print_sail.to_string (pp_instr instr))
@@ -1451,9 +1454,11 @@ let smt_cfnode all_cdefs ctx ssanodes =
        | _ -> declare_const ctx id ctyp
      in
      smt_reg_decs @ List.map smt_start (NameMap.bindings inits)
-  | CF_block instrs ->
+  | CF_block (instrs, terminator) ->
      let ctx = { ctx with pathcond = get_pathcond ctx ssanodes } in
-     List.concat (List.map (smt_instr ctx) instrs)
+     let smt_instrs = List.map (smt_instr ctx) instrs in
+     let smt_term = smt_terminator ctx terminator in
+     List.concat (smt_instrs @ [smt_term])
   (* We can ignore any non basic-block/start control-flow nodes *)
   | _ -> []
 
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index a4a77f9d..dfacf90a 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -53,6 +53,7 @@ open Jib
 open Jib_util
 
 module IntSet = Set.Make(struct type t = int let compare = compare end)
+module IntMap = Map.Make(struct type t = int let compare = compare end)
 
 (**************************************************************************)
 (* 1. Mutable graph type                                                  *)
@@ -60,12 +61,16 @@ module IntSet = Set.Make(struct type t = int let compare = compare end)
 
 type 'a array_graph = {
     mutable next : int;
-    mutable nodes : ('a * IntSet.t * IntSet.t) option array
+    mutable nodes : ('a * IntSet.t * IntSet.t) option array;
+    mutable next_cond : int;
+    mutable conds : cval IntMap.t
   }
 
 let make ~initial_size () = {
     next = 0;
-    nodes = Array.make initial_size None
+    nodes = Array.make initial_size None;
+    next_cond = 1;
+    conds = IntMap.empty
   }
 
 let get_vertex graph n = graph.nodes.(n)
@@ -77,6 +82,12 @@ let iter_graph f graph =
     | None -> ()
   done
 
+let add_cond cval graph =
+  let n = graph.next_cond in
+  graph.conds <- IntMap.add n cval graph.conds;
+  graph.next_cond <- n + 1;
+  n
+
 (** Add a vertex to a graph, returning the node index *)
 let add_vertex data graph =
   let n = graph.next in
@@ -187,12 +198,32 @@ let prune visited graph =
 (* 2. Mutable control flow graph                                          *)
 (**************************************************************************)
 
+type terminator =
+  | T_undefined of ctyp
+  | T_match_failure
+  | T_end of name
+  | T_goto of string
+  | T_jump of int * string
+  | T_label of string
+  | T_none
+
 type cf_node =
   | CF_label of string
-  | CF_block of instr list
-  | CF_guard of cval
+  | CF_block of instr list * terminator
+  | CF_guard of int
   | CF_start of ctyp NameMap.t
 
+let to_terminator graph = function
+  | I_label label -> T_label label
+  | I_goto label -> T_goto label
+  | I_jump (cval, label) ->
+     let n = add_cond cval graph in
+     T_jump (n, label)
+  | I_end name -> T_end name
+  | I_match_failure -> T_match_failure
+  | I_undefined ctyp -> T_undefined ctyp
+  | _ -> assert false
+
 (* For now we only generate CFGs for flat lists of instructions *)
 let control_flow_graph instrs =
   let module StringMap = Map.Make(String) in
@@ -209,46 +240,42 @@ 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_label _ | I_goto _ | I_jump _ | 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]
-      | _ -> []
+    let terminator, after = match after with
+      | I_aux (instr, _) :: after -> to_terminator graph instr, after
+      | [] -> T_none, []
     in
-    let preds = match before @ last with
-      | [] -> preds
-      | instrs ->
-         let n = add_vertex ([], CF_block instrs) graph in
+    let preds = match before, terminator with
+      | [], (T_none | T_label _) -> preds
+      | instrs, _ ->
+         let n = add_vertex ([], CF_block (instrs, terminator)) graph in
          List.iter (fun p -> add_edge p n graph) preds;
          [n]
     in
-    match after with
-    | I_aux ((I_end _ | I_match_failure | I_undefined _), _) :: after ->
+    match terminator with
+    | T_end _ | T_match_failure | T_undefined _ ->
        cfg [] after
 
-    | I_aux (I_goto label, _) :: after ->
+    | T_goto label ->
        List.iter (fun p -> add_edge p (StringMap.find label !labels) graph) preds;
        cfg [] after
 
-    | I_aux (I_jump (cval, label), _) :: after ->
-       let t = add_vertex ([], CF_guard cval) graph in
-       let f = add_vertex ([], CF_guard (V_call (Bnot, [cval]))) graph in
+    | T_jump (cond, label) ->
+       let t = add_vertex ([], CF_guard cond) graph in
+       let f = add_vertex ([], CF_guard (- cond)) graph in
        List.iter (fun p -> add_edge p t graph; add_edge p f graph) preds;
        add_edge t (StringMap.find label !labels) graph;
        cfg [f] after
 
-    | I_aux (I_label label, _) :: after ->
+    | T_label label ->
        cfg (StringMap.find label !labels :: preds) after
 
-    | I_aux (_, (_, l)) :: after ->
-       Reporting.unreachable l __POS__ "Could not add instruction to control-flow graph"
-
-    | [] -> preds
+    | T_none -> preds
   in
 
   let start = add_vertex ([], CF_start NameMap.empty) graph in
@@ -422,7 +449,7 @@ let place_phi_functions graph df =
 
   let orig_A n =
     match graph.nodes.(n) with
-    | Some ((_, CF_block instrs), _, _) ->
+    | Some ((_, CF_block (instrs, _)), _, _) ->
        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;
@@ -542,21 +569,32 @@ let rename_variables graph root children =
          counts := NameMap.add id i !counts;
          push_stack id i;
          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)
   in
 
+  let ssa_terminator = function
+    | T_jump (cond, label) ->
+       begin match IntMap.find_opt cond graph.conds with
+       | Some cval ->
+          graph.conds <- IntMap.add cond (fold_cval cval) graph.conds;
+          T_jump (cond, label)
+       | None -> assert false
+       end
+    | T_end id ->
+       let i = top_stack id in
+       T_end (ssa_name i id)
+    | terminator -> terminator
+  in
+
   let ssa_cfnode = function
     | CF_start inits -> CF_start inits
-    | CF_block instrs -> CF_block (List.map ssa_instr instrs)
+    | CF_block (instrs, terminator) ->
+       let instrs = List.map ssa_instr instrs in
+       CF_block (instrs, ssa_terminator terminator)
     | CF_label label -> CF_label label
-    | CF_guard cval -> CF_guard (fold_cval cval)
+    | CF_guard cond -> CF_guard cond
   in
 
   let ssa_ssanode = function
@@ -612,13 +650,19 @@ let rename_variables graph root children =
 
 let place_pi_functions graph start idom children =
   let get_guard = function
-    | CF_guard guard -> [guard]
+    | CF_guard cond ->
+       begin match IntMap.find_opt (abs cond) graph.conds with
+       | Some guard when cond > 0 -> [guard]
+       | Some guard -> [V_call (Bnot, [guard])]
+       | None -> assert false
+       end
     | _ -> []
   in
   let get_pi_contents ssanodes =
     List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes)
   in
 
+  (*
   let rec between_dom p n =
     if n = p then
       []
@@ -634,13 +678,13 @@ let place_pi_functions graph start idom children =
          | _, pred -> pred
          end
       | None -> assert false
-  in
+  in *)
 
   let rec go n =
     begin match graph.nodes.(n) with
     | Some ((ssa, cfnode), preds, succs) ->
        let p = idom.(n) in
-       let bd = between_dom p n in
+       let bd = [] (* between_dom p n *) in
        if p <> -1 then
          begin match graph.nodes.(p) with
          | Some ((dom_ssa, _), _, _) ->
@@ -699,9 +743,9 @@ let string_of_phis = function
 
 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_block (instrs, terminator)) -> 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 inits) -> string_of_phis phis ^ "START"
-  | (phis, CF_guard cval) -> string_of_phis phis ^ (String.escaped (Pretty_print_sail.to_string (pp_cval cval)))
+  | (phis, CF_guard cval) -> string_of_phis phis ^ string_of_int cval
 
 let vertex_color = function
   | (_, CF_start _) -> "peachpuff"
diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli
index 759e1ccb..72cf1a1e 100644
--- a/src/jib/jib_ssa.mli
+++ b/src/jib/jib_ssa.mli
@@ -77,10 +77,19 @@ exception Not_a_DAG of int
 
 val topsort : 'a array_graph -> int list
 
+type terminator =
+  | T_undefined of Jib.ctyp
+  | T_match_failure
+  | T_end of Jib.name
+  | T_goto of string
+  | T_jump of int * string
+  | T_label of string
+  | T_none
+
 type cf_node =
   | CF_label of string
-  | CF_block of Jib.instr list
-  | CF_guard of Jib.cval
+  | CF_block of Jib.instr list * terminator
+  | CF_guard of int
   | CF_start of Jib.ctyp NameMap.t
 
 val control_flow_graph : Jib.instr list -> int * int list * ('a list * cf_node) array_graph