Add work on scheduling

4 files changed, 64 insertions, 56 deletions

diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 88bb3e8..29c6e4c 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -187,6 +187,7 @@ Extract Constant GiblePargen.schedule => "Schedule.schedule_fn".
 
 (* Loop normalization *)
 Extract Constant IfConversion.build_bourdoncle => "BourdoncleAux.build_bourdoncle".
+Extract Constant IfConversion.get_if_conv_t => "(fun _ -> [Maps.PTree.empty])".
 
 (* Needed in Coq 8.4 to avoid problems with Function definitions. *)
 Set Extraction AccessOpaque.
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index 9992b1c..3001123 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -53,7 +53,8 @@ Definition reg := positive.
 Inductive resource : Set :=
 | Reg : reg -> resource
 | Pred : reg -> resource
-| Mem : resource.
+| Mem : resource
+| Exit : resource.
 
 (*|
 The following defines quite a few equality comparisons automatically, however,
@@ -79,7 +80,8 @@ Module R_indexed.
     match rs with
     | Reg r => xO (xO r)
     | Pred r => xI (xI r)
-    | Mem => 1%positive
+    | Mem => 1
+    | Exit => 2
     end.
 
   Lemma index_inj:  forall (x y: t), index x = index y -> x = y.
@@ -110,6 +112,7 @@ Inductive expression : Type :=
 | Eload : AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression
 | Estore : expression -> AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression
 | Esetpred : Op.condition -> expression_list -> expression
+| Eexit : cf_instr -> expression
 with expression_list : Type :=
 | Enil : expression_list
 | Econs : expression -> expression_list -> expression_list
@@ -303,6 +306,13 @@ with sem_mem : ctx -> expression -> Memory.mem -> Prop :=
 | Sbase_mem :
     forall ctx,
     sem_mem ctx (Ebase Mem) (ctx_mem ctx)
+with sem_exit : ctx -> expression -> option cf_instr -> Prop :=
+| Sexit :
+  forall ctx cf,
+    sem_exit ctx (Eexit cf) (Some cf)
+| Sbase_exit :
+  forall ctx,
+    sem_exit ctx (Ebase Exit) None
 with sem_val_list : ctx -> expression_list -> list val -> Prop :=
 | Snil :
     forall ctx,
@@ -351,13 +361,14 @@ Inductive sem_regset : ctx -> forest -> regset -> Prop :=
     (forall x, sem_pred_expr sem_value ctx (f # (Reg x)) (rs' !! x)) ->
     sem_regset ctx f rs'.
 
-Inductive sem : ctx -> forest -> instr_state -> Prop :=
+Inductive sem : ctx -> forest -> instr_state * cf_instr -> Prop :=
 | Sem:
-    forall ctx rs' m' f pr',
+    forall ctx rs' m' f pr' cf,
     sem_regset ctx f rs' ->
     sem_predset ctx f pr' ->
     sem_pred_expr sem_mem ctx (f # Mem) m' ->
-    sem ctx f (mk_instr_state rs' pr' m').
+    sem_pred_expr sem_exit ctx (f # Exit) (Some cf) ->
+    sem ctx f (mk_instr_state rs' pr' m', cf).
 
 End SEMANTICS.
 
@@ -381,6 +392,7 @@ Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool :=
   | Esetpred c1 el1, Esetpred c2 el2 =>
     if condition_eq c1 c2
     then beq_expression_list el1 el2 else false
+  | Eexit cf1, Eexit cf2 => if cf_instr_eq cf1 cf2 then true else false
   | _, _ => false
   end
 with beq_expression_list (el1 el2: expression_list) {struct el1} : bool :=
@@ -440,6 +452,7 @@ Proof.
     unfold not in *; intros. inv H0. rewrite beq_expression_list_refl in H; crush.
   - simplify. repeat (destruct_match; crush); subst.
   - simplify. repeat (destruct_match; crush); subst.
+  - simplify. repeat (destruct_match; crush); subst.
     apply andb_false_iff in H. inv H. unfold not in *; intros.
     inv H. rewrite beq_expression_refl in H0; discriminate.
     unfold not in *; intros. inv H. rewrite beq_expression_list_refl in H0; discriminate.
@@ -900,6 +913,8 @@ Section CORRECT.
       unfold ctx_rs, ctx_ps, ctx_mem in *; cbn in *. inv H; crush.
     - inv H0.
     - inv H0.
+    - inv H0.
+    - inv H0.
     - inv H0. econstructor.
     - inv H0. eapply IHe in H6; auto. eapply IHe0 in H8.
       econstructor; eassumption.
@@ -1185,7 +1200,7 @@ Section CORRECT.
       check fa fb = true ->
       sem ictx fa i ->
       sem octx fb i' ->
-      match_states i i'.
+      match_states (fst i) (fst i') /\ snd i = snd i'.
   Proof using HSIM.
     intros.
     unfold check, get_forest in *; intros;
@@ -1200,18 +1215,14 @@ Section CORRECT.
              | H: forall _ : Rtree.elt, _ |- _ => specialize (H (Reg x))
              end.
       repeat (destruct_match; try contradiction).
-      unfold "#" in *. rewrite Heqo in H0.
-      rewrite Heqo0 in H1. admit.
-      unfold "#" in H1. rewrite Heqo0 in H1.
-      unfold "#" in H0. rewrite Heqo in H0. admit.
-    }
+      unfold "#" in *.
 Admitted.
 
   Lemma check_correct2:
     forall (fa fb : forest) i,
       check fa fb = true ->
       sem ictx fa i ->
-      exists i', sem octx fb i' /\ match_states i i'.
+      exists i', sem octx fb i' /\ match_states (fst i) (fst i') /\ snd i = snd i'.
   Proof. Admitted.
 
 End CORRECT.
@@ -1311,22 +1322,22 @@ End BOOLEAN_EQUALITY.
 
 Lemma map1:
   forall w dst dst',
-  dst <> dst' ->
-  (empty # dst <- w) # dst' = NE.singleton (T, Ebase dst').
+    dst <> dst' ->
+    (empty # dst <- w) # dst' = NE.singleton (T, Ebase dst').
 Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply get_empty. Qed.
 
 Lemma genmap1:
   forall (f : forest) w dst dst',
-  dst <> dst' ->
-  (f # dst <- w) # dst' = f # dst'.
+    dst <> dst' ->
+    (f # dst <- w) # dst' = f # dst'.
 Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed.
 
 Lemma map2:
   forall (v : pred_expr) x rs,
-  (rs # x <- v) # x = v.
+    (rs # x <- v) # x = v.
 Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed.
 
 Lemma tri1:
   forall x y,
-  Reg x <> Reg y -> x <> y.
+    Reg x <> Reg y -> x <> y.
 Proof. crush. Qed.
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index 778e0cd..da0567b 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -167,8 +167,6 @@ This is done by multiplying the predicates together, and assigning the negation
 of the expression to the other predicates.
 |*)
 
-Definition forest_state : Type := forest * list (cf_instr * option pred_op * forest).
-
 Definition upd_pred_forest (p: option pred_op) (f: forest) :=
   match p with
   | Some p' =>
@@ -180,39 +178,42 @@ Definition upd_pred_forest (p: option pred_op) (f: forest) :=
   | None => f
   end.
 
-Definition update (flist : forest_state) (i : instr): forest_state :=
-  let (f, fl) := flist in
+Definition update (fop : option pred_op * forest) (i : instr): (option pred_op * forest) :=
+  let (pred, f) := fop in
   match i with
-  | RBnop => flist
+  | RBnop => fop
   | RBop p op rl r =>
-    (f # (Reg r) <-
-    (app_predicated p
-       (f # (Reg r))
-       (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f)))), fl)
+      (pred, f # (Reg r) <-
+             (app_predicated (combine_pred p pred)
+                             (f # (Reg r))
+                             (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f)))))
   | RBload p chunk addr rl r =>
-    (f # (Reg r) <-
-      (app_predicated p
+    (pred, f # (Reg r) <-
+      (app_predicated (combine_pred p pred)
          (f # (Reg r))
          (map_predicated
             (map_predicated (pred_ret (Eload chunk addr))
                             (merge (list_translation rl f)))
-            (f # Mem))), fl)
+            (f # Mem))))
   | RBstore p chunk addr rl r =>
-    (f # Mem <-
-      (app_predicated p
+    (pred, f # Mem <-
+      (app_predicated (combine_pred p pred)
          (f # Mem)
          (map_predicated
             (map_predicated
                (predicated_apply2 (map_predicated (pred_ret Estore)
                                                   (f # (Reg r))) chunk addr)
-               (merge (list_translation rl f))) (f # Mem))), fl)
+               (merge (list_translation rl f))) (f # Mem))))
   | RBsetpred p' c args p =>
-    (f # (Pred p) <-
-    (app_predicated p'
+    (pred, f # (Pred p) <-
+    (app_predicated (combine_pred p' pred)
        (f # (Pred p))
        (map_predicated (pred_ret (Esetpred c))
-                       (merge (list_translation args f)))), fl)
-  | RBexit p c => ((upd_pred_forest (option_map negate p) f), (c, p, upd_pred_forest p f) :: fl)
+                       (merge (list_translation args f)))))
+  | RBexit p c =>
+      (combine_pred (Option.map negate p) pred,
+        f # Exit <-
+          (app_predicated (combine_pred p pred) (f # Exit) (pred_ret (Eexit c))))
   end.
 
 (*|
@@ -223,7 +224,7 @@ code than in the RTLBlock code.
 Get a sequence from the basic block.
 |*)
 
-Fixpoint abstract_sequence (f : forest_state) (b : list instr) : forest_state :=
+Fixpoint abstract_sequence (f : option pred_op * forest) (b : list instr) : option pred_op * forest :=
   match b with
   | nil => f
   | i :: l => abstract_sequence (update f i) l
@@ -254,9 +255,8 @@ Definition empty_trees (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
   end.
 
 Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
-  forallb (fun x => match x with ((_, _, f1), (_, _, f2)) => check f1 f2 end)
-          (combine (snd (abstract_sequence (empty, nil) bb))
-                   (snd (abstract_sequence (empty, nil) (concat (concat bbt))))) &&
+  (check (snd (abstract_sequence (None, empty) bb))
+         (snd (abstract_sequence (None, empty) (concat (concat bbt))))) &&
   empty_trees bb bbt.
 
 Definition check_scheduled_trees := beq2 schedule_oracle.
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index 2abbea4..699a616 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -48,21 +48,16 @@ RTLBlock to abstract translation
 Correctness of translation from RTLBlock to the abstract interpretation language.
 |*)
 
-(*Definition is_regs i := match i with mk_instr_state rs _ => rs end.
-Definition is_mem i := match i with mk_instr_state _ m => m end.
+Definition is_regs i := match i with mk_instr_state rs _ _ => rs end.
+Definition is_mem i := match i with mk_instr_state _ _ m => m end.
+Definition is_ps i := match i with mk_instr_state _ p _ => p end.
 
 Inductive state_lessdef : instr_state -> instr_state -> Prop :=
   state_lessdef_intro :
-    forall rs1 rs2 m1,
-    (forall x, rs1 !! x = rs2 !! x) ->
-    state_lessdef (mk_instr_state rs1 m1) (mk_instr_state rs2 m1).
-
-Ltac inv_simp :=
-  repeat match goal with
-  | H: exists _, _ |- _ => inv H
-  end; simplify.
-
-*)
+    forall rs1 rs2 ps1 ps2 m1,
+      (forall x, rs1 !! x = rs2 !! x) ->
+      (forall x, ps1 !! x = ps2 !! x) ->
+      state_lessdef (mk_instr_state rs1 ps1 m1) (mk_instr_state rs2 ps2 m1).
 
 Definition check_dest i r' :=
   match i with
@@ -89,12 +84,13 @@ Proof. induction l; crush. Qed.
 Lemma check_dest_l_dec i r : {check_dest_l i r = true} + {check_dest_l i r = false}.
 Proof. destruct (check_dest_l i r); tauto. Qed.
 
-(*Lemma check_dest_update :
+Lemma check_dest_update :
   forall f i r,
   check_dest i r = false ->
-  (update f i) # (Reg r) = f # (Reg r).
+  (snd (update f i)) # (Reg r) = (snd f) # (Reg r).
 Proof.
-  destruct i; crush; try apply Pos.eqb_neq in H; apply genmap1; crush.
+  destruct i; crush; try apply Pos.eqb_neq in H; unfold update; destruct_match; crush.
+  inv Heqp.
 Qed.
 
 Lemma check_dest_l_forall2 :