Add temporary fixes to get everything to compiledev/predicated-execution

9 files changed, 514 insertions, 45 deletions

diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 6ae2856..a4d0bde 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -185,6 +185,7 @@ Separate Extraction
          RTLBlockgen.transl_program RTLBlockInstr.successors_instr
          HTLgen.tbl_to_case_expr
          Pipeline.pipeline
+         RTLBlockInstr.sat_pred_temp
 
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 0804b0e..fcd4441 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -557,6 +557,12 @@ Fixpoint penumerate {A : Type} (p : positive) (l : list A) {struct l}
   | nil => nil
   end.
 
+Fixpoint prange {A: Type} (p1 p2: positive) (l: list A) {struct l} :=
+  match l with
+  | x :: xs => (p1, p2, x) :: prange p2 (Pos.pred p2) xs
+  | nil => nil
+  end.
+
 Lemma add_data_instr_state_incr :
   forall s n st,
     st_incr s
@@ -622,10 +628,36 @@ Definition add_control_instr (n : node) (st : stmnt) : mon unit :=
       Error (Errors.msg "HTLPargen.add_control_instr: control logic is not empty")
     end.
 
+Definition add_control_instr_force_state_incr :
+  forall s n st,
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (st_freshstate s)
+       s.(st_scldecls)
+       s.(st_arrdecls)
+       s.(st_datapath)
+       (AssocMap.set n st s.(st_controllogic))).
+Admitted.
+
+Definition add_control_instr_force (n : node) (st : stmnt) : mon unit :=
+  fun s =>
+    OK tt (mkstate
+      s.(st_st)
+      s.(st_freshreg)
+      (st_freshstate s)
+      s.(st_scldecls)
+      s.(st_arrdecls)
+      s.(st_datapath)
+      (AssocMap.set n st s.(st_controllogic)))
+   (add_control_instr_force_state_incr s n st).
+
+
 Fixpoint pred_expr (preg: reg) (p: pred_op) :=
   match p with
   | Pvar pred =>
-    Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred))
+    Vrange preg (Vlit (natToValue pred)) (Vlit (natToValue pred))
   | Pnot pred =>
     Vunop Vnot (pred_expr preg pred)
   | Pand p1 p2 =>
@@ -665,12 +697,38 @@ Definition translate_inst (fin rtrn stack preg : reg) (n : node) (i : instr)
     add_data_instr n (Vnonblock (pred_expr preg (Pvar p)) cond)
   end.
 
-Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * list instr)
-  : mon unit :=
-  let (n, li) := ni in
-  do _ <- collectlist (translate_inst fin rtrn stack preg n) li;
-  do st <- get;
-  add_control_instr n (state_goto st.(st_st) (Pos.pred n)).
+Lemma create_new_state_state_incr:
+  forall s p,
+  st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (s.(st_freshstate) + p)%positive
+       s.(st_scldecls)
+       s.(st_arrdecls)
+       s.(st_datapath)
+       s.(st_controllogic)).
+Admitted.
+
+Definition create_new_state (p: node): mon node :=
+  fun s => OK s.(st_freshstate)
+              (mkstate
+                s.(st_st)
+                s.(st_freshreg)
+                (s.(st_freshstate) + p)%positive
+                s.(st_scldecls)
+                s.(st_arrdecls)
+                s.(st_datapath)
+                s.(st_controllogic))
+              (create_new_state_state_incr s p).
+
+Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * node * list instr) :=
+  match ni with
+  | (n, p, li) =>
+    do _ <- collectlist (translate_inst fin rtrn stack preg n) li;
+    do st <- get;
+    add_control_instr n (state_goto st.(st_st) p)
+  end.
 
 Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr)
   : mon (stmnt * stmnt) :=
@@ -695,8 +753,9 @@ Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr)
     do (tc1s, tc1c) <- translate_cfi' fin rtrn stack preg c1;
     do (tc2s, tc2c) <- translate_cfi' fin rtrn stack preg c2;
     ret ((Vcond (pred_expr preg p) tc1s tc2s), (Vcond (pred_expr preg p) tc1c tc2c))
-  | RBjumptable r ln =>
-    error (Errors.msg "HTLPargen: RPjumptable not supported.")
+  | RBjumptable r tbl =>
+    do s <- get;
+    ret (Vskip, Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))
   | RBcall sig ri rl r n =>
     error (Errors.msg "HTLPargen: RPcall not supported.")
   | RBtailcall sig ri lr =>
@@ -715,10 +774,14 @@ Definition translate_cfi (fin rtrn stack preg: reg) (ni: node * cf_instr)
 Definition transf_bblock (fin rtrn stack preg: reg) (ni : node * bblock)
   : mon unit :=
   let (n, bb) := ni in
+  do nstate <- create_new_state ((poslength bb.(bb_body)))%positive;
   do _ <- collectlist (translate_inst_list fin rtrn stack preg)
-                      (penumerate n bb.(bb_body));
-  translate_cfi fin rtrn stack preg
-                ((n - poslength bb.(bb_body))%positive, bb.(bb_exit)).
+                      (prange n (nstate + poslength bb.(bb_body) - 1)%positive
+                                  bb.(bb_body));
+  match bb.(bb_body) with
+  | nil => translate_cfi fin rtrn stack preg (n, bb.(bb_exit))
+  | _ => translate_cfi fin rtrn stack preg (nstate, bb.(bb_exit))
+  end.
 
 Definition transf_module (f: function) : mon HTL.module :=
   if stack_correct f.(fn_stacksize) then
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 943e1a8..39d9fd2 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -72,21 +72,49 @@ Definition is_cond_cfi (cfi: cf_instr) :=
   | _ => false
   end.
 
-Definition find_block_with_cond (c: code) : option (node * bblock) :=
-  match List.filter (fun x => is_cond_cfi (snd x).(bb_exit)) (PTree.elements c) with
-  | (a :: b)%list => Some a
-  | nil => None
+Fixpoint any {A: Type} (f: A -> bool) (a: list A) :=
+  match a with
+  | x :: xs => f x || any f xs
+  | nil => false
   end.
 
-Definition transf_function (f: function) : function :=
-  match find_block_with_cond f.(fn_code) with
-  | Some (n, bb) =>
-    let nbb := if_convert_block f.(fn_code) 1%positive bb in
-    mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize)
-               (PTree.set n nbb f.(fn_code)) f.(fn_entrypoint)
-  | None => f
+Fixpoint all {A: Type} (f: A -> bool) (a: list A) :=
+  match a with
+  | x :: xs => f x && all f xs
+  | nil => true
   end.
 
+Definition find_backedge (nb: node * bblock) :=
+  let (n, b) := nb in
+  let succs := successors_instr b.(bb_exit) in
+  filter (fun x => Pos.ltb n x) succs.
+
+Definition find_all_backedges (c: code) : list node :=
+  List.concat (List.map find_backedge (PTree.elements c)).
+
+Definition has_backedge (entry: node) (be: list node) :=
+  any (fun x => Pos.eqb entry x) be.
+
+Definition find_blocks_with_cond (c: code) : list (node * bblock) :=
+  let backedges := find_all_backedges c in
+  List.filter (fun x => is_cond_cfi (snd x).(bb_exit) &&
+                        negb (has_backedge (fst x) backedges) &&
+                        all (fun x' => negb (has_backedge x' backedges))
+                            (successors_instr (snd x).(bb_exit))
+              ) (PTree.elements c).
+
+Definition if_convert_code (p: nat * code) (nb: node * bblock) :=
+  let (n, bb) := nb in
+  let (p', c) := p in
+  let nbb := if_convert_block c p' bb in
+  (S p', PTree.set n nbb c).
+
+Definition transf_function (f: function) : function :=
+  let (_, c) := List.fold_left if_convert_code
+                               (find_blocks_with_cond f.(fn_code))
+                               (1%nat, f.(fn_code)) in
+  mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) c f.(fn_entrypoint).
+
 Definition transf_fundef (fd: fundef) : fundef :=
   transf_fundef transf_function fd.
 
diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml
index 979ca38..ba7241b 100644
--- a/src/hls/PrintRTLBlockInstr.ml
+++ b/src/hls/PrintRTLBlockInstr.ml
@@ -10,7 +10,7 @@ let reg pp r =
   fprintf pp "x%d" (P.to_int r)
 
 let pred pp r =
-  fprintf pp "p%d" (P.to_int r)
+  fprintf pp "p%d" (Nat.to_int r)
 
 let rec regs pp = function
   | [] -> ()
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 345e73e..86f8eba 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -16,6 +16,8 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
+Require Import Coq.micromega.Lia.
+
 Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Events.
@@ -27,11 +29,12 @@ Require Import compcert.lib.Maps.
 Require Import compcert.verilog.Op.
 
 Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.Sat.
 
 Local Open Scope rtl.
 
 Definition node := positive.
-Definition predicate := positive.
+Definition predicate := nat.
 
 Inductive pred_op : Type :=
 | Pvar: predicate -> pred_op
@@ -39,6 +42,209 @@ Inductive pred_op : Type :=
 | Pand: pred_op -> pred_op -> pred_op
 | Por: pred_op -> pred_op -> pred_op.
 
+Fixpoint sat_predicate (p: pred_op) (a: asgn) : bool :=
+  match p with
+  | Pvar p' => a p'
+  | Pnot p' => negb (sat_predicate p' a)
+  | Pand p1 p2 => sat_predicate p1 a && sat_predicate p2 a
+  | Por p1 p2 => sat_predicate p1 a || sat_predicate p2 a
+  end.
+
+Fixpoint mult {A: Type} (a b: list (list A)) : list (list A) :=
+  match a with
+  | nil => nil
+  | l :: ls => mult ls b ++ (List.map (fun x => l ++ x) b)
+  end.
+
+Lemma satFormula_concat:
+  forall a b agn,
+  satFormula a agn ->
+  satFormula b agn ->
+  satFormula (a ++ b) agn.
+Proof. induction a; crush. Qed.
+
+Lemma satFormula_concat2:
+  forall a b agn,
+  satFormula (a ++ b) agn ->
+  satFormula a agn /\ satFormula b agn.
+Proof.
+  induction a; simplify;
+    try apply IHa in H1; crush.
+Qed.
+
+Lemma satClause_concat:
+  forall a a1 a0,
+  satClause a a1 ->
+  satClause (a0 ++ a) a1.
+Proof. induction a0; crush. Qed.
+
+Lemma satClause_concat2:
+  forall a a1 a0,
+  satClause a0 a1 ->
+  satClause (a0 ++ a) a1.
+Proof.
+  induction a0; crush.
+  inv H; crush.
+Qed.
+
+Lemma satClause_concat3:
+  forall a b c,
+  satClause (a ++ b) c ->
+  satClause a c \/ satClause b c.
+Proof.
+  induction a; crush.
+  inv H; crush.
+  apply IHa in H0; crush.
+  inv H0; crush.
+Qed.
+
+Lemma satFormula_mult':
+  forall p2 a a0,
+  satFormula p2 a0 \/ satClause a a0 ->
+  satFormula (map (fun x : list lit => a ++ x) p2) a0.
+Proof.
+  induction p2; crush.
+  - inv H. inv H0. apply satClause_concat. auto.
+    apply satClause_concat2; auto.
+  - apply IHp2.
+    inv H; crush; inv H0; crush.
+Qed.
+
+Lemma satFormula_mult2':
+  forall p2 a a0,
+  satFormula (map (fun x : list lit => a ++ x) p2) a0 ->
+  satClause a a0 \/ satFormula p2 a0.
+Proof.
+  induction p2; crush.
+  apply IHp2 in H1. inv H1; crush.
+  apply satClause_concat3 in H0.
+  inv H0; crush.
+Qed.
+
+Lemma satFormula_mult:
+  forall p1 p2 a,
+  satFormula p1 a \/ satFormula p2 a ->
+  satFormula (mult p1 p2) a.
+Proof.
+  induction p1; crush.
+  apply satFormula_concat; crush.
+  inv H. inv H0.
+  apply IHp1. auto.
+  apply IHp1. auto.
+  apply satFormula_mult';
+  inv H; crush.
+Qed.
+
+Lemma satFormula_mult2:
+  forall p1 p2 a,
+  satFormula (mult p1 p2) a ->
+  satFormula p1 a \/ satFormula p2 a.
+Proof.
+  induction p1; crush.
+  apply satFormula_concat2 in H; crush.
+  apply IHp1 in H0.
+  inv H0; crush.
+  apply satFormula_mult2' in H1. inv H1; crush.
+Qed.
+
+Fixpoint trans_pred_temp (bound: nat) (p: pred_op) : option formula :=
+  match bound with
+  | O => None
+  | S n =>
+    match p with
+    | Pvar p' => Some (((true, p') :: nil) :: nil)
+    | Pand p1 p2 =>
+      match trans_pred_temp n p1, trans_pred_temp n p2 with
+      | Some p1', Some p2' =>
+        Some (p1' ++ p2')
+      | _, _ => None
+      end
+    | Por p1 p2 =>
+      match trans_pred_temp n p1, trans_pred_temp n p2 with
+      | Some p1', Some p2' =>
+        Some (mult p1' p2')
+      | _, _ => None
+      end
+    | Pnot (Pvar p') => Some (((false, p') :: nil) :: nil)
+    | Pnot (Pnot p) => trans_pred_temp n p
+    | Pnot (Pand p1 p2) => trans_pred_temp n (Por (Pnot p1) (Pnot p2))
+    | Pnot (Por p1 p2) => trans_pred_temp n (Pand (Pnot p1) (Pnot p2))
+    end
+  end.
+
+Fixpoint trans_pred (bound: nat) (p: pred_op) :
+  option {fm: formula | forall a,
+           sat_predicate p a = true <-> satFormula fm a}.
+  refine
+  (match bound with
+   | O => None
+   | S n =>
+     match p with
+     | Pvar p' => Some (exist _ (((true, p') :: nil) :: nil) _)
+     | Pand p1 p2 =>
+      match trans_pred n p1, trans_pred n p2 with
+      | Some (exist p1' _), Some (exist p2' _) =>
+        Some (exist _ (p1' ++ p2') _)
+      | _, _ => None
+      end
+     | Por p1 p2 =>
+      match trans_pred n p1, trans_pred n p2 with
+      | Some (exist p1' _), Some (exist p2' _) =>
+        Some (exist _ (mult p1' p2') _)
+      | _, _ => None
+      end
+     | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _)
+     | _ => None
+     end
+   end); split; intros; simpl in *; auto.
+  - inv H. inv H0; auto.
+  - admit.
+  - admit.
+  - apply satFormula_concat.
+    apply andb_prop in H. inv H. apply i in H0. auto.
+    apply andb_prop in H. inv H. apply i0 in H1. auto.
+  - apply satFormula_concat2 in H. simplify. apply andb_true_intro.
+    split. apply i in H0. auto.
+    apply i0 in H1. auto.
+  - apply orb_prop in H. inv H; apply satFormula_mult. apply i in H0. auto.
+    apply i0 in H0. auto.
+  - apply orb_true_intro.
+    apply satFormula_mult2 in H. inv H. apply i in H0. auto.
+    apply i0 in H0. auto.
+Admitted.
+
+Definition sat_pred (bound: nat) (p: pred_op) :
+  option ({al : alist | sat_predicate p (interp_alist al) = true}
+          + {forall a : asgn, sat_predicate p a = false}).
+  refine
+  ( match trans_pred bound p with
+    | Some (exist fm _) =>
+      match boundedSat bound fm with
+      | Some (inleft (exist a _)) => Some (inleft (exist _ a _))
+      | Some (inright _) => Some (inright _)
+      | None => None
+      end
+    | None => None
+    end ).
+  - apply i in s2. auto.
+  - intros. specialize (n a). specialize (i a).
+    destruct (sat_predicate p a). exfalso.
+    apply n. apply i. auto. auto.
+Qed.
+
+Definition sat_pred_simple (bound: nat) (p: pred_op) :=
+  match sat_pred bound p with
+  | Some (inleft (exist al _)) => Some (Some al)
+  | Some (inright _) => Some None
+  | None => None
+  end.
+
+Definition sat_pred_temp (bound: nat) (p: pred_op) :=
+  match trans_pred_temp bound p with
+  | Some fm => boundedSatSimple bound fm
+  | None => None
+  end.
+
 Inductive instr : Type :=
 | RBnop : instr
 | RBop : option pred_op -> operation -> list reg -> reg -> instr
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 8ff701f..39c57df 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -683,7 +683,15 @@ Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function :
   else
     Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent.").
 
-Definition transl_fundef := transf_partial_fundef transl_function.
+Definition transl_function_temp (f: RTLBlock.function) : Errors.res RTLPar.function :=
+  let tfcode := fn_code (schedule f) in
+    Errors.OK (mkfunction f.(fn_sig)
+                          f.(fn_params)
+                          f.(fn_stacksize)
+                          tfcode
+                          f.(fn_entrypoint)).
+
+Definition transl_fundef := transf_partial_fundef transl_function_temp.
 
 Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program :=
   transform_partial_program transl_fundef p.
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index 0c953ff..b9ee741 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -33,6 +33,8 @@ open HTLgen
 open HTLMonad
 open HTLMonadExtra
 
+module SS = Set.Make(P)
+
 module IMap = Map.Make (struct
   type t = int
 
@@ -76,7 +78,7 @@ let add_dep i tree deps curr =
   match PTree.get curr tree with None -> deps | Some ip -> (ip, i) :: deps
 
 (** This function calculates the dependencies of each instruction.  The nodes correspond to previous
-   register that were allocated and show which instruction caused it.
+   registers that were allocated and show which instruction caused it.
 
    This function only gathers the RAW constraints, and will therefore only be active for operations
    that modify registers, which is this case only affects loads and operations. *)
@@ -188,7 +190,7 @@ let accumulate_WAW_mem_deps dfg curr =
 
 let rec in_predicate p p' =
   match p' with
-  | Pvar p'' -> P.eq p p''
+  | Pvar p'' -> Nat.to_int p = Nat.to_int p''
   | Pnot p'' -> in_predicate p p''
   | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2
   | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2
@@ -288,6 +290,32 @@ let assigned_vars vars = function
   | RBstore (_, _, _, _, _) -> vars
   | RBsetpred (_, _, _) -> vars
 
+let get_pred = function
+  | RBnop -> None
+  | RBop (op, _, _, _) -> op
+  | RBload (op, _, _, _, _) -> op
+  | RBstore (op, _, _, _, _) -> op
+  | RBsetpred (_, _, _) -> None
+
+let independant_pred p p' =
+  match sat_pred_temp (Nat.of_int 100000) (Pand (p, p')) with
+  | Some None -> true
+  | _ -> false
+
+let check_dependent op1 op2 =
+  match op1, op2 with
+  | Some p, Some p' -> not (independant_pred p p')
+  | _, _ -> true
+
+let remove_unnecessary_deps dfg =
+  let { edges; nodes } = dfg in
+  let is_dependent = function (i1, i2) ->
+    let instr1 = List.nth nodes i1 in
+    let instr2 = List.nth nodes i2 in
+    check_dependent (get_pred instr1) (get_pred instr2)
+  in
+  { edges = List.filter is_dependent edges; nodes }
+
 (** All the nodes in the DFG have to come after the source of the basic block, and should terminate
    before the sink of the basic block.  After that, there should be constraints for data
    dependencies between nodes. *)
@@ -322,8 +350,9 @@ let gather_bb_constraints debug bb =
   let _, dfg8 =
     List.fold_left accumulate_WAW_pred_deps (0, dfg7) bb.bb_body
   in
-  if debug then printf "DFG''''': %a\n" print_dfg dfg8 else ();
-  (List.length bb.bb_body, dfg8, successors_instr bb.bb_exit)
+  let dfg9 = remove_unnecessary_deps dfg8 in
+  if debug then printf "DFG''''': %a\n" print_dfg dfg9 else ();
+  (List.length bb.bb_body, dfg9, successors_instr bb.bb_exit)
 
 let gen_bb_name s i = sprintf "bb%d%s" (P.to_int i) s
 
@@ -471,8 +500,8 @@ let transf_rtlpar c (schedule : (int * int) list IMap.t) =
         let i_sched_tree =
           List.fold_left combine_bb_schedule IMap.empty i_sched
         in
-        printf "--------------- curr: %d, max: %d, min: %d, next: %d\n" (P.to_int i) max_state min_state (P.to_int i - max_state + min_state - 1);
-        printf "HIIIII: %d orig: %d\n" (P.to_int i - max_state + min_state - 1) (P.to_int i);
+        (*printf "--------------- curr: %d, max: %d, min: %d, next: %d\n" (P.to_int i) max_state min_state (P.to_int i - max_state + min_state - 1);
+        printf "HIIIII: %d orig: %d\n" (P.to_int i - max_state + min_state - 1) (P.to_int i);*)
         { bb_body = (IMap.to_seq i_sched_tree |> List.of_seq |> List.sort compare_tuple |> List.map snd
                            |> List.map (List.map (fun x -> List.nth bb_body' x)));
           bb_exit = ctrl_flow
@@ -483,23 +512,38 @@ let transf_rtlpar c (schedule : (int * int) list IMap.t) =
 let second = function (_, a, _) -> a
 
 let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) =
-  let debug = true in
+  let debug = false in
   let c' = PTree.map1 (gather_bb_constraints false) c in
-  let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in
+  (*let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in*)
   let _, (vars, constraints, types) =
     List.map fst (PTree.elements c') |>
     List.fold_left (fun compl ->
         gather_cfg_constraints compl c') ([], ([], "", ""))
   in
   let schedule' = solve_constraints vars constraints types in
-  IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';
+  (*IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';*)
   (*printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*)
   transf_rtlpar c schedule'
 
+let rec find_reachable_states c e =
+  match PTree.get e c with
+  | Some { bb_exit = ex; _ } ->
+    e :: List.fold_left (fun x a -> List.concat [x; find_reachable_states c a]) []
+      (successors_instr ex |> List.filter (fun x -> P.lt x e))
+  | None -> assert false
+
+let add_to_tree c nt i =
+  match PTree.get i c with
+  | Some p -> PTree.set i p nt
+  | None -> assert false
+
 let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function =
+  let scheduled = schedule f.fn_entrypoint f.fn_code in
+  let reachable = find_reachable_states scheduled f.fn_entrypoint
+                  |> List.to_seq |> SS.of_seq |> SS.to_seq |> List.of_seq in
   { fn_sig = f.fn_sig;
     fn_params = f.fn_params;
     fn_stacksize = f.fn_stacksize;
-    fn_code = schedule f.fn_entrypoint f.fn_code;
+    fn_code = List.fold_left (add_to_tree scheduled) PTree.empty reachable;
     fn_entrypoint = f.fn_entrypoint
   }
diff --git a/test/array.c b/test/array.c
index 59299a5..680acdf 100644
--- a/test/array.c
+++ b/test/array.c
@@ -1,9 +1,128 @@
-int main() {
-    int x[10] = {1, 2, 3, 4, 5, 6, 7, 8, 9, 10};
-    int sum = 0;
-    for (int i = 0; i < 10; i++) {
-        sum = sum + x[i];
-        x[i] = sum;
-    }
-    return sum;
+/* durbin.c: this file is part of PolyBench/C */
+
+#ifndef SYNTHESIS
+#include <stdio.h>
+#endif
+
+unsigned int divider(unsigned int x, unsigned int y)
+{
+    unsigned int r0, q0, y0, y1;
+
+    r0 = x;
+    q0 = 0;
+    y0 = y;
+    y1 = y;
+    do
+    {
+        y1 = 2 * y1;
+    } while (y1 <= x);
+    do
+    {
+        y1 = y1 / 2;
+        q0 = 2 * q0;
+        if (r0 >= y1)
+        {
+            r0 = r0 - y1;
+            q0 = q0 + 1;
+        }
+    } while ((int)y1 != (int)y0);
+    return q0;
+}
+
+int sdivider(int N, int D) {
+    if (D < 0) {
+        if (N < 0)
+            return divider(-N, -D);
+        else
+            return -divider(N, -D);
+    } else {
+        if (N < 0)
+            return -divider(-N, D);
+        else
+            return divider(N, D);
+    }
+}
+
+#define plus(i) i = i + ONE
+/* Include polybench common header. */
+static
+void init_array (int n,
+                 int r[ 40 + 0])
+{
+    int ONE = 1;
+    int i;
+
+    for (i = 0; i < n; plus(i))
+    {
+        r[i] = (n+ONE-i);
+    }
+}
+
+
+
+static
+int print_array(int n,
+                int y[ 40 + 0])
+
+{
+    int ONE = 1;
+    int i;
+    int res = 0;
+
+    for (i = 0; i < n; plus(i)) {
+        res  ^= y[i];
+    }
+
+#ifndef SYNTHESIS
+    printf("finished: %u\n", res);
+#endif
+
+    return res;
+}
+
+static
+void kernel_durbin(int n,
+                   int r[ 40 + 0],
+                   int y[ 40 + 0])
+{
+    int z[40];
+    int alpha;
+    int beta;
+    int sum;
+
+    int ONE = 1;
+    int i,k;
+    y[0] = -r[0];
+    beta = 1;
+    alpha = -r[0];
+
+    for (k = 1; k < n; plus(k)) {
+        beta = (ONE-alpha*alpha)*beta;
+        sum = 0;
+        for (i=0; i<k; plus(i)) {
+            sum += r[k-i-ONE]*y[i];
+        }
+        alpha = - sdivider(r[k] + sum, beta);
+
+        for (i=0; i<k; plus(i)) {
+            z[i] = y[i] + alpha*y[k-i-ONE];
+        }
+        for (i=0; i<k; plus(i)) {
+            y[i] = z[i];
+        }
+        y[k] = alpha;
+    }
+}
+
+
+int main()
+{
+    int n = 40;
+    int r[40 + 0];
+    int y[40 + 0];
+
+    init_array (n, r);
+    kernel_durbin (n, r, y);
+
+    return print_array(n, y);
 }
diff --git a/test/test_all.sh b/test/test_all.sh
index 92d3967..6b67d27 100755
--- a/test/test_all.sh
+++ b/test/test_all.sh
@@ -30,7 +30,7 @@ for cfile in $test_dir/*.c; do
     gcc -o $outbase.gcc $cfile >/dev/null 2>&1
     $outbase.gcc
     expected=$?
-    ./bin/vericert -drtl -o $outbase.v $cfile >/dev/null 2>&1
+    ./bin/vericert -fschedule -drtl -o $outbase.v $cfile >/dev/null 2>&1
     if [[ ! -f $outbase.v ]]; then
         echo "ERROR"
         continue