Work on if-conversion proof

3 files changed, 282 insertions, 47 deletions

diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v
index acc47ed..9e2cfc5 100644
--- a/src/hls/GibleSeq.v
+++ b/src/hls/GibleSeq.v
@@ -30,6 +30,7 @@ Require Import compcert.verilog.Op.
 
 Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.Gible.
+Require Import vericert.hls.Predicate.
 
 (*|
 ========
@@ -121,6 +122,26 @@ Proof.
   constructor; auto.
 Qed.
 
+#[local] Notation "'mki'" := (mk_instr_state) (at level 1).
+
+Lemma exec_rbexit_truthy :
+  forall A B bb ge sp rs pr m rs' pr' m' pc',
+    @SeqBB.step A B ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') (RBgoto pc')) ->
+    exists p b1 b2,
+      truthy pr' p
+      /\ bb = b1 ++ (RBexit p (RBgoto pc')) :: b2
+      /\ step_list2 (Gible.step_instr ge) sp (Iexec (mki rs pr m)) b1 (Iexec (mki rs' pr' m')).
+Proof.
+  induction bb; crush.
+  inv H. inv H.
+  - destruct state'. exploit IHbb; eauto; simplify.
+    exists x. exists (a :: x0). exists x1. simplify; auto.
+    econstructor; eauto.
+  -  inv H3.
+     exists p. exists nil. exists bb. crush.
+     constructor.
+Qed.
+
 #[local] Open Scope positive.
 
 Lemma max_pred_function_use :
@@ -130,3 +151,45 @@ Lemma max_pred_function_use :
     In p (pred_uses i) ->
     p <= max_pred_function f.
 Proof. Admitted.
+
+Ltac truthy_falsy :=
+  match goal with
+  | H: instr_falsy ?ps (RBop ?p _ _ _), H2: truthy ?ps ?p |- _ =>
+      solve [inv H2; inv H; crush]
+  | H: instr_falsy ?ps (RBload ?p _ _ _ _), H2: truthy ?ps ?p |- _ =>
+      solve [inv H2; inv H; crush]
+  | H: instr_falsy ?ps (RBstore ?p _ _ _ _), H2: truthy ?ps ?p |- _ =>
+      solve [inv H2; inv H; crush]
+  | H: instr_falsy ?ps (RBexit ?p _), H2: truthy ?ps ?p |- _ =>
+      solve [inv H2; inv H; crush]
+  | H: instr_falsy ?ps (RBsetpred ?p _ _ _), H2: truthy ?ps ?p |- _ =>
+      solve [inv H2; inv H; crush]
+  end.
+
+Lemma exec_determ :
+  forall A B ge sp s1 a s2 s2',
+    @step_instr A B ge sp s1 a s2 ->
+    step_instr ge sp s1 a s2' ->
+    s2 = s2'.
+Proof.
+  inversion 1; subst; crush.
+  - inv H0; auto.
+  - inv H2; crush; truthy_falsy.
+  - inv H3; crush. truthy_falsy.
+  - inv H3; crush. truthy_falsy.
+  - inv H2; crush. truthy_falsy.
+  - inv H1; crush. truthy_falsy.
+  - destruct st; simplify. inv H1; crush; truthy_falsy.
+Qed.
+
+Lemma append3 :
+  forall A B l0 l1 sp ge s1 s2 s3,
+    step_list2 (step_instr ge) sp s1 l0 s2 ->
+    @SeqBB.step A B ge sp s1 (l0 ++ l1) s3 ->
+    @SeqBB.step A B ge sp s2 l1 s3.
+Proof.
+  induction l0; crush. inv H. auto.
+  inv H0. inv H. assert (i1 = (Iexec state')) by (eapply exec_determ; eauto). subst. eauto.
+  inv H. assert (i1 = (Iterm state' cf)) by (eapply exec_determ; eauto). subst.
+  exfalso; eapply step_list2_false; eauto.
+Qed.
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 01801c3..db4bba6 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -59,15 +59,17 @@ Definition map_if_convert (p: option pred_op) (i: instr) :=
   | _ => i
   end.
 
-Definition if_convert_block (next: node) (b_next: SeqBB.t) (_: unit) (i: instr) :=
+Definition if_convert_block (next: node) (b_next: SeqBB.t) (i: instr) :=
   match i with
   | RBexit p (RBgoto next') =>
       if (next =? next')%positive
-      then (tt, map (map_if_convert p) b_next)
-      else (tt, i::nil)
-  | _ => (tt, i::nil)
+      then map (map_if_convert p) b_next
+      else i::nil
+  | _ => i::nil
   end.
 
+Definition wrap_unit {A B} (f: A -> B) (_: unit) (a: A) := (tt, f a).
+
 Definition predicated_store i :=
   match i with
   | RBstore _ _ _ _ _ => true
@@ -87,7 +89,7 @@ Definition if_convert (orig_c c: code) (main next: node) :=
   match orig_c ! main, orig_c ! next with
   | Some b_main, Some b_next =>
       if decide_if_convert b_next then
-        PTree.set main (snd (replace_section (if_convert_block next b_next) tt b_main)) c
+        PTree.set main (snd (replace_section (wrap_unit (if_convert_block next b_next)) tt b_main)) c
       else c
   | _, _ => c
   end.
@@ -203,12 +205,15 @@ Definition ifconv_list (headers: list node) (c: code) :=
 (*   let nbb := if_convert_block (snd p) (Pos.of_nat (fst p)) (snd nb) in *)
 (*   (S (fst p), PTree.set (fst nb) nbb (snd p)). *)
 
+Definition if_convert_code (c: code) iflist :=
+  fold_left (fun s n => if_convert c s (fst n) (snd n)) iflist c.
+
 Definition transf_function (f: function) : function :=
   let (b, _) := build_bourdoncle f in
   let b' := get_loops b in
   let iflist := ifconv_list b' f.(fn_code) in
   mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize)
-             (fold_left (fun s n => if_convert s (fst n) (snd n)) iflist f.(fn_code))
+             (if_convert_code f.(fn_code) iflist)
              f.(fn_entrypoint).
 
 Definition transf_fundef (fd: fundef) : fundef :=
diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v
index 0aac3af..de44118 100644
--- a/src/hls/IfConversionproof.v
+++ b/src/hls/IfConversionproof.v
@@ -72,13 +72,40 @@ Inductive if_conv_block_spec (c: code): SeqBB.t -> SeqBB.t -> Prop :=
     if_conv_block_spec c b' ta ->
     if_conv_block_spec c (RBexit p (RBgoto pc')::b) (map (map_if_convert p) ta++tb).
 
-Lemma transf_spec_correct :
+Lemma transf_spec_correct' :
   forall f pc b,
     f.(fn_code) ! pc = Some b ->
     exists b', (transf_function f).(fn_code) ! pc = Some b'
           /\ if_conv_block_spec f.(fn_code) b b'.
 Proof. Admitted.
 
+Inductive replace_spec_unit (f: instr -> SeqBB.t)
+  : SeqBB.t -> SeqBB.t -> Prop :=
+| replace_spec_cons : forall i b b',
+  replace_spec_unit f b b' ->
+  replace_spec_unit f (i :: b) (f i ++ b')
+| replace_spec_nil :
+  replace_spec_unit f nil nil
+.
+
+Definition if_conv_replace n nb := replace_spec_unit (if_convert_block n nb).
+
+Inductive if_conv_spec (c c': code) (pc: node): Prop :=
+| if_conv_unchanged :
+  c ! pc = c' ! pc ->
+  if_conv_spec c c' pc
+| if_conv_changed : forall b b' pc' tb,
+  if_conv_replace pc' b' b tb ->
+  c ! pc = Some b ->
+  c ! pc' = Some b' ->
+  c' ! pc = Some tb ->
+  if_conv_spec c c' pc.
+
+Lemma transf_spec_correct :
+  forall f pc,
+    if_conv_spec f.(fn_code) (transf_function f).(fn_code) pc.
+Proof. Admitted.
+
 Section CORRECTNESS.
 
   Context (prog tprog : program).
@@ -92,16 +119,28 @@ Section CORRECTNESS.
       f.(fn_code) ! pc = Some block2 ->
       SeqBB.step tge sp in_s' block2 out_s.
 
+  (* (EXT: sem_extrap tf pc0 sp (Iexec (mki rs p m)) (Iexec (mki rs0 p0 m0)) b)
+     (STAR: star step ge (State stk f sp pc0 rs0 p0 m0) E0 (State stk f sp pc rs p m))
+     (IS_B: exists b, f.(fn_code)!pc0 = Some b)
+     (SPEC: forall b_o, f.(fn_code) ! pc = Some b_o -> if_conv_block_spec f.(fn_code) b_o b),
+   *)
+
   Variant match_states : option SeqBB.t -> state -> state -> Prop :=
-    | match_state_true :
+    | match_state_some :
       forall stk stk' f tf sp pc rs p m b pc0 rs0 p0 m0
              (TF: transf_function f = tf)
              (STK: Forall2 match_stackframe stk stk')
-             (EXT: sem_extrap tf pc0 sp (Iexec (mki rs p m)) (Iexec (mki rs0 p0 m0)) b)
-             (STAR: star step ge (State stk f sp pc0 rs0 p0 m0) E0 (State stk f sp pc rs p m))
-             (IS_B: exists b, f.(fn_code)!pc0 = Some b)
-             (SPEC: forall b_o, f.(fn_code) ! pc = Some b_o -> if_conv_block_spec f.(fn_code) b_o b),
+             (* This can be improved with a recursive relation for a more general structure of the
+                if-conversion proof. *)
+             (IS_B: f.(fn_code)!pc = Some b)
+             (EXTRAP: sem_extrap tf pc0 sp (Iexec (mki rs p m)) (Iexec (mki rs0 p0 m0)) b)
+             (SIM: step ge (State stk f sp pc0 rs0 p0 m0) E0 (State stk f sp pc rs p m)),
         match_states (Some b) (State stk f sp pc rs p m) (State stk' tf sp pc0 rs0 p0 m0)
+    | match_state_none :
+      forall stk stk' f tf sp pc rs p m
+             (TF: transf_function f = tf)
+             (STK: Forall2 match_stackframe stk stk'),
+        match_states None (State stk f sp pc rs p m) (State stk' tf sp pc rs p m)
     | match_callstate :
       forall cs cs' f tf args m
              (TF: transf_fundef f = tf)
@@ -136,8 +175,8 @@ Section CORRECTNESS.
       funsig (transf_fundef f) = funsig f.
   Proof using.
     unfold transf_fundef. unfold AST.transf_fundef; intros. destruct f.
-    unfold transf_function. destruct_match; auto. auto.
-  Admitted.
+    unfold transf_function. destruct_match. auto. auto.
+  Qed.
 
   Lemma functions_translated:
     forall (v: Values.val) (f: GibleSeq.fundef),
@@ -167,7 +206,7 @@ Section CORRECTNESS.
       repeat ffts.
   Qed.
 
-(*)  Lemma transf_initial_states :
+  Lemma transf_initial_states :
     forall s1,
       initial_state prog s1 ->
       exists s2, initial_state tprog s2 /\ match_states None s1 s2.
@@ -218,22 +257,148 @@ Section CORRECTNESS.
 
   Definition measure (b: option SeqBB.t): nat :=
     match b with
-    | None => 0
-    | Some b' => 1 + length b'
+    | None => 1
+    | Some _ => 0
+    end.
+
+  Lemma sim_star :
+    forall s1 b t s,
+      (exists b' s2,
+          star step tge s1 t s2 /\ ltof _ measure b' b
+          /\ match_states b' s s2) ->
+      exists b' s2,
+        (plus step tge s1 t s2 \/
+           star step tge s1 t s2 /\ ltof _ measure b' b) /\
+          match_states b' s s2.
+  Proof. intros; simplify. do 3 econstructor; eauto. Qed.
+
+  Lemma sim_plus :
+    forall s1 b t s,
+      (exists b' s2, plus step tge s1 t s2 /\ match_states b' s s2) ->
+      exists b' s2,
+        (plus step tge s1 t s2 \/
+           star step tge s1 t s2 /\ ltof _ measure b' b) /\
+          match_states b' s s2.
+  Proof. intros; simplify. do 3 econstructor; eauto. Qed.
+
+  Lemma step_instr :
+    forall sp s s' a,
+      step_instr ge sp (Iexec s) a (Iexec s') ->
+      step_instr tge sp (Iexec s) a (Iexec s').
+  Proof.
+    inversion 1; subst; econstructor; eauto.
+    - now rewrite <- eval_op_eq.
+    - now rewrite <- eval_addressing_eq.
+    - now rewrite <- eval_addressing_eq.
+  Qed.
+
+  Lemma step_instr_term :
+    forall sp s s' a cf,
+      Gible.step_instr ge sp (Iexec s) a (Iterm s' cf) ->
+      Gible.step_instr tge sp (Iexec s) a (Iterm s' cf).
+  Proof. inversion 1; subst; constructor; auto. Qed.
+
+  Lemma seqbb_eq :
+    forall bb sp rs pr m rs' pr' m' cf,
+      SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) ->
+      SeqBB.step tge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf).
+  Proof.
+    induction bb; crush; inv H.
+    - econstructor; eauto. apply step_instr; eassumption.
+      destruct state'. eapply IHbb; eauto.
+    - constructor; apply step_instr_term; auto.
+  Qed.
+
+  Lemma fn_all_eq :
+    forall f tf,
+      transf_function f = tf ->
+      fn_stacksize f = fn_stacksize tf
+      /\ fn_sig f = fn_sig tf
+      /\ fn_params f = fn_params tf
+      /\ fn_entrypoint f = fn_entrypoint tf
+      /\ exists l, if_convert_code (fn_code f) l = fn_code tf.
+  Proof.
+    intros; simplify; unfold transf_function in *; destruct_match; inv H; auto.
+    eexists; simplify; eauto.
+  Qed.
+
+  Ltac func_info :=
+    match goal with
+      H: transf_function _ = _ |- _ =>
+        let H2 := fresh "ALL_EQ" in
+        pose proof (fn_all_eq _ _ H) as H2; simplify
     end.
 
-  Lemma temp:
-    forall c b b' sp rs pr m rs' pr' m' cf,
-      if_conv_block_spec c b b' ->
-      SeqBB.step ge sp (Iexec (mki rs pr m)) b (Iterm (mki rs' pr' m') cf) ->
-      SeqBB.step tge sp (Iexec (mki rs pr m)) b' (Iterm (mki rs' pr' m') cf)
-      \/ (exists pc' nb b'1 b'2 b'3 p,
-             c ! pc' = Some nb
-             /\ step_list2 (step_instr tge) sp (Iexec (mki rs pr m)) b'1 (Iexec (mki rs' pr' m'))
-             /\ b' = b'1 ++ map (map_if_convert p) b'2 ++ b'3
-             /\ cf = RBgoto pc'
-             /\ if_conv_block_spec c nb b'2).
-  Admitted.
+  Lemma step_cf_eq :
+    forall stk stk' f tf sp pc rs pr m cf s t,
+      step_cf_instr ge (State stk f sp pc rs pr m) cf t s ->
+      Forall2 match_stackframe stk stk' ->
+      transf_function f = tf ->
+      exists s', step_cf_instr tge (State stk' tf sp pc rs pr m) cf t s'
+                 /\ match_states None s s'.
+  Proof.
+    inversion 1; subst; simplify;
+      try solve [func_info; do 2 econstructor; econstructor; eauto].
+    - do 2 econstructor. constructor; eauto. constructor; eauto. constructor; auto.
+      constructor. auto.
+    - do 2 econstructor. constructor; eauto.
+      func_info.
+      rewrite H2 in *. rewrite H12. auto. constructor; auto.
+    - func_info. do 2 econstructor. econstructor; eauto. rewrite H2 in *.
+      eauto. econstructor; auto.
+  Qed.
+
+  (*Lemma event0_trans :
+    forall stk f sp pc rs' pr' m' cf t f0 sp0 pc0 rs0 pr0 m0 stack,
+      step_cf_instr ge (State stk f sp pc rs' pr' m') cf t (State stack f0 sp0 pc0 rs0 pr0 m0) ->
+      t = E0 /\ f = f0 /\ sp = sp0 /\ stk = stack.
+  Proof.
+    inversion 1; subst; crush.*)
+
+  Lemma cf_dec :
+    forall a pc, {a = RBgoto pc} + {a <> RBgoto pc}.
+  Proof.
+    destruct a; try solve [right; crush].
+    intros. destruct (peq n pc); subst.
+    left; auto.
+    right. unfold not in *; intros. inv H. auto.
+  Qed.
+
+  Lemma exec_if_conv :
+    forall bb sp rs pr m rs' pr' m' pc' b' tb,
+      SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') (RBgoto pc')) ->
+      if_conv_replace pc' b' bb tb ->
+      exists p b rb,
+        tb = b ++ (map (map_if_convert p) b') ++ rb
+        /\ SeqBB.step ge sp (Iexec (mki rs pr m)) b (Iexec (mki rs' pr' m')).
+  Proof.
+    Admitted.
+
+  Lemma temp2:
+    forall t s1' stk f sp pc rs m pr rs' m' bb pr' cf stk',
+      (fn_code f) ! pc = Some bb ->
+      SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) ->
+      step_cf_instr ge (State stk f sp pc rs' pr' m') cf t s1' ->
+      Forall2 match_stackframe stk stk' ->
+      exists b' s2',
+        (plus step tge (State stk' (transf_function f) sp pc rs pr m) t s2' \/
+           star step tge (State stk' (transf_function f) sp pc rs pr m) t s2'
+           /\ ltof (option SeqBB.t) measure b' None) /\
+          match_states b' s1' s2'.
+  Proof.
+    intros * H H0 H1 STK.
+    pose proof (transf_spec_correct f pc) as X; inv X.
+    - apply sim_plus. rewrite H in H2. symmetry in H2.
+      exploit step_cf_eq; eauto; simplify.
+      do 3 econstructor. apply plus_one. econstructor; eauto.
+      apply seqbb_eq; eauto. eauto.
+    - simplify.
+      destruct (cf_dec cf pc'); subst. inv H1.
+      exploit exec_if_conv; eauto; simplify.
+      exploit exec_rbexit_truthy; eauto; simplify.
+      apply sim_star. exists (Some b'). exists (State stk' (transf_function f) sp pc rs pr m).
+      simplify; try (unfold ltof; auto). apply star_refl.
+      constructor; auto. unfold sem_extrap; simplify.
 
   Lemma step_cf_matches :
     forall b s cf t s' ts,
@@ -253,22 +418,26 @@ Section CORRECTNESS.
   Proof using TRANSL.
     inversion 1; subst; simplify;
       match goal with H: context[match_states] |- _ => inv H end.
-    -
-      exploit temp; eauto; simplify. inv H3.
-      pose proof (transf_spec_correct _ _ _ H4); simplify.
-      exploit step_cf_matches; eauto.
-      econstructor; eauto. unfold sem_extrap; intros.
-      unfold sem_extrap in EXT.
-      rewrite H8 in H3; simplify.
-      do 2 econstructor. split. left. eapply plus_one. econstructor; eauto.
-      unfold sem_extrap in EXT. eapply EXT. eauto. admit.
-      instantiate (1 := State stack (transf_function f0) sp0 pc0 rs0 pr0 m0).
-      admit. constructor; eauto. admit. unfold sem_extrap. intros. admit.
-      eapply star_refl. intros. admit.
-    -
-      simplify. inv H2. do 2 econstructor. split. admit.
-      econstructor; eauto. admit. admit. intros.
-      rewrite H3 in H2. inv H2. eauto
+    - admit.
+    - eauto using temp2. Admitted.
+
+
+    (* - *)
+    (*   exploit temp; eauto; simplify. inv H3. *)
+    (*   pose proof (transf_spec_correct _ _ _ H4); simplify. *)
+    (*   exploit step_cf_matches; eauto. *)
+    (*   econstructor; eauto. unfold sem_extrap; intros. *)
+    (*   unfold sem_extrap in EXT. *)
+    (*   rewrite H8 in H3; simplify. *)
+    (*   do 2 econstructor. split. left. eapply plus_one. econstructor; eauto. *)
+    (*   unfold sem_extrap in EXT. eapply EXT. eauto. admit. *)
+    (*   instantiate (1 := State stack (transf_function f0) sp0 pc0 rs0 pr0 m0). *)
+    (*   admit. constructor; eauto. admit. unfold sem_extrap. intros. admit. *)
+    (*   eapply star_refl. intros. admit. *)
+    (* - *)
+    (*   simplify. inv H2. do 2 econstructor. split. admit. *)
+    (*   econstructor; eauto. admit. admit. intros. *)
+    (*   rewrite H3 in H2. inv H2. eauto *)
 
   Theorem transf_program_correct:
     forward_simulation (semantics prog) (semantics tprog).
@@ -285,6 +454,4 @@ Section CORRECTNESS.
     - apply senv_preserved.
   Qed.
 
-
-*)
 End CORRECTNESS.