Acyclic CFA reduction

lib/passes.ml

@@ -199,6 +199,14 @@ module PassManager = struct
       invariants = Invariants.presupposes [ Params ] ~establishes:[ SSA ];
     }
 
+  let cfa_reduction =
+    {
+      name = "cfa-reduction";
+      apply = Proc Transforms.Cfa_reduction.reduce_procedure;
+      doc = "Performs reduction of acyclic CFA";
+      invariants = Invariants.presupposes [ SSA ];
+    }
+
   let remove_unreachable_blocks =
     {
       name = "remove-unreachable-block";
@@ -453,6 +461,7 @@ module PassManager = struct
       read_uninit false;
       read_uninit true;
       sssa;
+      cfa_reduction;
       sva;
       full_ssa;
       chc_infer_invariants;

lib/transforms/cfa_reduction.ml

@@ -0,0 +1,104 @@
+open Lang
+open Lang.Common
+
+(* Assumes program is in SSA, acyclic and pure. *)
+let construct_final_edge proc =
+  (* Termination condition for each edge. *)
+  let term : (IDSet.elt, Var.t) Hashtbl.t = Hashtbl.create 30 in
+  Procedure.fold_blocks_topo_fwd
+    (fun final_edge id block ->
+      let preds = Procedure.blocks_pred proc id |> Iter.to_list in
+
+      (* Compute reachability of this block. *)
+      let reachable =
+        (* Always reachable if no predecessors. *)
+        if List.is_empty preds then Expr.BasilExpr.boolconst true
+        (* Otherwise, reachability is ANY of the predecessors reachability. *)
+          else
+          Expr.BasilExpr.applyintrin ~op:`OR
+            (preds
+            |> List.filter_map (fst %> Hashtbl.get term)
+            |> List.map Expr.BasilExpr.rvar)
+      in
+
+      (* Create ITE statements from phi nodes. *)
+      let ites : Program.stmt =
+        let al =
+          block.phis
+          |> List.map (function
+            | ({ lhs; rhs = hd :: tl } : Var.t Block.phi) ->
+                let ite =
+                  List.fold_left
+                    (fun acc (in_edge, var) ->
+                      Expr.BasilExpr.ifthenelse
+                        (Expr.BasilExpr.rvar @@ Hashtbl.find term in_edge)
+                        (Expr.BasilExpr.rvar var) acc)
+                    (Expr.BasilExpr.rvar @@ snd hd)
+                    tl
+                in
+                (lhs, ite)
+            | _ -> failwith "Encountered phi node with no rhs.")
+        in
+        Stmt.Instr_Assign { attrib = Attrib.empty; al }
+      in
+
+      (* Add a fresh termination variable to assign the condition. *)
+      let termination_var = Procedure.fresh_var proc ~pure:true Types.Boolean in
+      Hashtbl.add term id termination_var;
+
+      (* Construct our termination condition by combining
+          initial reachability with any assumes along this edge. *)
+      let termination_cond =
+        Expr.BasilExpr.applyintrin ~op:`AND
+          ([ reachable ]
+          @ (Block.stmts_iter block
+            |> Iter.filter_map (function
+              | Stmt.Instr_Assume { body; branch = true } -> Some body
+              | _ -> None)
+            |> Iter.to_list))
+      in
+      let termination =
+        Stmt.Instr_Assign
+          {
+            attrib = Attrib.empty;
+            al = [ (termination_var, termination_cond) ];
+          }
+      in
+
+      (* Final edge is existing statements plus:
+          1. the ites for the new edge being merged in.
+          2. the statements for the new edge body.
+          3. an assignment to the termination variable.
+        *)
+      final_edge
+      @ List.concat
+          [
+            [ ites ];
+            (* Filter out the now unnecessary guards. *)
+            block.stmts |> Vector.to_list
+            |> List.filter (fun s ->
+                not
+                @@
+                match s with
+                | Stmt.Instr_Assume { branch = true } -> true
+                | _ -> false);
+            [ termination ];
+          ])
+    List.empty proc
+
+let reduce_procedure (proc : Program.proc) : Program.proc =
+  (* Constructed reduced edge to replace procedure blocks. *)
+  let final_edge = construct_final_edge proc in
+
+  let out_proc =
+    proc |> Procedure.iter_blocks |> Iter.map fst
+    |> Iter.fold (fun acc id -> Procedure.remove_block acc id) proc
+  in
+  let out_proc, id = Procedure.fresh_block out_proc ~stmts:final_edge () in
+
+  (* Make this the entry and return block. *)
+  let out_proc = Procedure.set_entry_block out_proc id in
+  Procedure.PG.map_graph
+    (fun g ->
+      Procedure.G.add_edge g (Procedure.Vert.End id) Procedure.Vert.Return)
+    out_proc

test/cram/cfa_reduction.il

@@ -0,0 +1,23 @@
+prog entry @f1;
+
+proc @f1(a:bv64) -> (c:bv64)
+[
+ block %a [
+  var x:bv64 := a;
+  goto(%b, %c);
+ ];
+ block %b [
+  guard(bvuge(x,0:bv64));
+  var x := bvadd(x:bv64,1:bv64);
+  goto(%exit);
+ ];
+ block %c [
+  guard(bvult(x,0:bv64));
+  var x := bvsub(x:bv64,1:bv64);
+  goto(%exit);
+ ];
+ block %exit [
+  var c:bv64 := x;
+  return;
+ ];
+];

test/cram/cfa_reduction.sexp

@@ -0,0 +1,5 @@
+(load-il "./cfa_reduction.il")
+(run-transforms "ssa")
+(run-transforms "cfa-reduction")
+(run-transforms "simplify")
+(dump-il "./out.il")

test/cram/cfa_reduction.t

@@ -0,0 +1,21 @@
+  $ bincaml script ./cfa_reduction.sexp
+  (load-il ./cfa_reduction.il)
+  (run-transforms ssa)
+  (run-transforms cfa-reduction)
+  (run-transforms simplify)
+  (dump-il ./out.il)
+  $ cat ./out.il
+  proc @f1(a:bv64)  -> (c:bv64) {  }
+
+
+  [
+     block %block [
+       var v:bool := true;
+       var v_2:bool := booland(v:bool, boolnot(bvult(a:bv64, 0x0:bv64)));
+       var x_6:bv64 := if v_2:bool then bvadd(a:bv64, 0x1:bv64) else bvsub(a:bv64,
+        0x1:bv64);
+       var c:bv64 := x_6:bv64;
+       return;
+     ]
+  ];
+  prog entry @f1;

test/cram/dune

@@ -62,6 +62,8 @@
   ll_spec.sexp
   repeated_ssa.il
   repeated_ssa.sexp
+  cfa_reduction.il
+  cfa_reduction.sexp
   ../../bin/main.exe))
 
 (cram