Conditions now propagated by CSE3

Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work

1 files changed, 362 insertions, 32 deletions

diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 2257b4de..0722f904 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -352,6 +352,23 @@ Qed.
 
 Hint Resolve rel_ge : cse3.
 
+Lemma relb_ge:
+  forall inv inv'
+         (GE : RB.ge inv' inv)
+         ctx sp rs m
+         (REL: sem_rel_b sp ctx inv rs m),
+  sem_rel_b sp ctx inv' rs m.
+Proof.
+  intros.
+  destruct inv; cbn in *.
+  2: contradiction.
+  destruct inv'; cbn in *.
+  2: assumption.
+  eapply rel_ge; eassumption.
+Qed.
+
+Hint Resolve relb_ge : cse3.
+
 Lemma sem_rhs_sop :
   forall sp op rs args m v,
   eval_operation ge sp op rs ## args m = Some v ->
@@ -422,6 +439,7 @@ Qed.
 
 Hint Resolve sem_rel_b_top : cse3.
 
+(*
 Ltac IND_STEP :=
         match goal with
         REW: (fn_code ?fn) ! ?mpc = Some ?minstr
@@ -442,19 +460,42 @@ Ltac IND_STEP :=
         eapply rel_ge; eauto with cse3 (* ; for printing
         idtac mpc mpc' fn minstr *)
       end.
-
+ *)
+  
 Lemma step_simulation:
   forall S1 t S2, RTL.step ge S1 t S2 -> 
   forall S1', match_states S1 S1' ->
               exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
 Proof.
   induction 1; intros S1' MS; inv MS.
+  all: try set (ctx := (context_from_hints (snd (preanalysis tenv f)))) in *.
+  all: try set (invs := (fst (preanalysis tenv f))) in *.
   - (* Inop *)
     exists (State ts tf sp pc' rs m). split.
     + apply exec_Inop; auto.
       TR_AT. reflexivity.
     + econstructor; eauto.
-      IND_STEP.
+      
+      (* BEGIN INVARIANT *)
+      fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      unfold sem_rel_b.
+      apply (rel_ge inv_pc inv_pc'); auto.
+      (* END INVARIANT *)
+      
   - (* Iop *)
     exists (State ts tf sp pc' (rs # res <- v) m). split.
     + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iop op args res pc')) as instr'.
@@ -516,9 +557,28 @@ Proof.
     + econstructor; eauto.
       * eapply wt_exec_Iop with (f:=f); try eassumption.
         eauto with wt.
-      * IND_STEP.
-        apply oper_sound; eauto with cse3.
-
+      *
+        (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      rewrite rel_leb_correct in *.
+      eapply rel_ge.
+      eassumption.
+      apply oper_sound; unfold ctx; eauto with cse3.
+      (* END INVARIANT *)
   - (* Iload *)
     exists (State ts tf sp pc' (rs # dst <- v) m). split.
     + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'.
@@ -575,8 +635,27 @@ Proof.
     + econstructor; eauto.
       * eapply wt_exec_Iload with (f:=f); try eassumption.
         eauto with wt.
-      * IND_STEP.
-        apply oper_sound; eauto with cse3.
+      *         (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      rewrite rel_leb_correct in *.
+      eapply rel_ge.
+      eassumption.
+      apply oper_sound; unfold ctx; eauto with cse3.
+      (* END INVARIANT *)
         
   - (* Iload notrap1 *)
     exists (State ts tf sp pc' (rs # dst <- Vundef) m). split.
@@ -632,8 +711,27 @@ Proof.
            assumption.
     + econstructor; eauto.
       * apply wt_undef; assumption.
-      * IND_STEP.
-        apply oper_sound; eauto with cse3.
+      *          (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      rewrite rel_leb_correct in *.
+      eapply rel_ge.
+      eassumption.
+      apply oper_sound; unfold ctx; eauto with cse3.
+      (* END INVARIANT *)
         
   - (* Iload notrap2 *)
     exists (State ts tf sp pc' (rs # dst <- Vundef) m). split.
@@ -690,8 +788,27 @@ Proof.
            assumption.
     + econstructor; eauto.
       * apply wt_undef; assumption.
-      * IND_STEP.
-        apply oper_sound; eauto with cse3.
+      *  (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      rewrite rel_leb_correct in *.
+      eapply rel_ge.
+      eassumption.
+      apply oper_sound; unfold ctx; eauto with cse3.
+      (* END INVARIANT *)
 
   - (* Istore *)
     exists (State ts tf sp pc' rs m'). split.
@@ -704,8 +821,27 @@ Proof.
       * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial.
         assumption.
     + econstructor; eauto.
-      IND_STEP.
-      apply store_sound with (a0:=a) (m0:=m); eauto with cse3.
+  (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      rewrite rel_leb_correct in *.
+      eapply rel_ge.
+      eassumption.
+      apply store_sound with (a0:=a) (m0:=m); unfold ctx; eauto with cse3.
+      (* END INVARIANT *)
       
   - (* Icall *)
     destruct (find_function_translated ros rs fd H0) as [tfd [HTFD1 HTFD2]].
@@ -720,9 +856,29 @@ Proof.
       * econstructor; eauto.
         ** rewrite sig_preserved with (f:=fd); assumption.
         ** intros.
-           IND_STEP.
-           apply kill_reg_sound; eauto with cse3.
-           eapply kill_mem_sound; eauto with cse3.
+
+            (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      rewrite rel_leb_correct in *.
+      eapply rel_ge.
+      eassumption.
+      (* END INVARIANT *)
+      { apply kill_reg_sound; unfold ctx; eauto with cse3.
+           eapply kill_mem_sound; unfold ctx; eauto with cse3. }
       * rewrite sig_preserved with (f:=fd) by trivial.
         rewrite <- H7.
         apply wt_regset_list; auto.
@@ -760,19 +916,159 @@ Proof.
       * eapply external_call_symbols_preserved; eauto. apply senv_preserved.
     + econstructor; eauto.
       * eapply wt_exec_Ibuiltin with (f:=f); eauto with wt.
-      * IND_STEP.
-        apply kill_builtin_res_sound; eauto with cse3.
-        eapply external_call_sound; eauto with cse3.
+      *   (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+      2: discriminate.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me.
+      rewrite rel_leb_correct in *.
+      eapply rel_ge.
+      eassumption.
+      (* END INVARIANT *)
+
+        apply kill_builtin_res_sound; unfold ctx; eauto with cse3.
+        eapply external_call_sound; unfold ctx; eauto with cse3.
         
   - (* Icond *)
-    econstructor. split.
-    + eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption.
-      * TR_AT. reflexivity.
-      * rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial.
-        eassumption.
-      * reflexivity.
-    + econstructor; eauto.
-      destruct b; IND_STEP.
+    destruct (find_cond_in_fmap (ctx := ctx) invs pc cond args) as [bfound | ] eqn:FIND_COND.                                                                    
+    + econstructor; split.
+      * eapply exec_Inop; try eassumption.
+        TR_AT. unfold transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity.
+      * replace bfound with b.
+        { econstructor; eauto.
+          (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      rewrite andb_true_iff in IND_step_me.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me as [IND_so [IND_not ZOT]].
+      clear ZOT.
+      rewrite relb_leb_correct in IND_so.
+      rewrite relb_leb_correct in IND_not.
+      
+      destruct b.
+      { eapply relb_ge. eassumption. apply apply_cond_sound; auto. }
+      eapply relb_ge. eassumption. apply apply_cond_sound; trivial.
+      rewrite eval_negate_condition.
+      rewrite H0.
+      reflexivity.
+      (* END INVARIANT *)
+        }
+        unfold sem_rel_b in REL.
+        destruct (invs # pc) as [rel | ] eqn:FIND_REL.
+        2: contradiction.
+        pose proof (is_condition_present_sound pc rel cond args rs m REL) as COND_PRESENT_TRUE.
+        pose proof (is_condition_present_sound pc rel (negate_condition cond) args rs m REL) as COND_PRESENT_FALSE.
+        rewrite eval_negate_condition in COND_PRESENT_FALSE.
+        unfold find_cond_in_fmap in FIND_COND.
+        change (@PMap.get (option RELATION.t)) with (@Regmap.get RB.t) in FIND_COND.
+        rewrite FIND_REL in FIND_COND.
+        destruct (Compopts.optim_CSE3_conditions tt).
+        2: discriminate.
+        destruct (is_condition_present pc rel cond args).
+        { rewrite COND_PRESENT_TRUE in H0 by trivial.
+          congruence.
+        }
+        destruct (is_condition_present pc rel (negate_condition cond) args).
+        { destruct (eval_condition cond rs ## args m) as [b0 | ].
+          2: discriminate.
+          inv H0.
+          cbn in COND_PRESENT_FALSE.
+          intuition.
+          inv H0.
+          inv FIND_COND.
+          destruct b; trivial; cbn in H2; discriminate.
+        }
+        clear COND_PRESENT_TRUE COND_PRESENT_FALSE.
+        pose proof (is_condition_present_sound pc rel cond (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) rs m REL) as COND_PRESENT_TRUE.
+        pose proof (is_condition_present_sound pc rel (negate_condition cond) (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) rs m REL) as COND_PRESENT_FALSE.
+        rewrite eval_negate_condition in COND_PRESENT_FALSE.
+        
+        destruct is_condition_present.
+        { rewrite subst_args_ok with (sp:=sp) (m:=m) in COND_PRESENT_TRUE.
+          { rewrite COND_PRESENT_TRUE in H0 by trivial.
+            congruence.
+          }
+          unfold fmap_sem.
+          unfold sem_rel_b.
+          fold invs.
+          rewrite FIND_REL.
+          exact REL.
+        }
+        destruct is_condition_present.
+        { rewrite subst_args_ok with (sp:=sp) (m:=m) in COND_PRESENT_FALSE.
+          { destruct (eval_condition cond rs ## args m) as [b0 | ].
+            2: discriminate.
+            inv H0.
+            cbn in COND_PRESENT_FALSE.
+            intuition.
+            inv H0.
+            inv FIND_COND.
+            destruct b; trivial; cbn in H2; discriminate.
+          }
+          unfold fmap_sem.
+          unfold sem_rel_b.
+          fold invs.
+          rewrite FIND_REL.
+          exact REL.          
+        }
+        discriminate.
+   + econstructor; split.        
+      * eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption.
+        ** TR_AT. unfold transf_instr. fold invs. fold ctx.
+           rewrite FIND_COND.
+           reflexivity.
+        ** rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial.
+           eassumption.
+        ** reflexivity.
+     * econstructor; eauto.
+
+          (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      rewrite andb_true_iff in IND_step_me.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me as [IND_so [IND_not ZOT]].
+      clear ZOT.
+      rewrite relb_leb_correct in IND_so.
+      rewrite relb_leb_correct in IND_not.
+      
+      destruct b.
+      { eapply relb_ge. eassumption. apply apply_cond_sound; auto. }
+      eapply relb_ge. eassumption. apply apply_cond_sound; trivial.
+      rewrite eval_negate_condition.
+      rewrite H0.
+      reflexivity.
+      (* END INVARIANT *)
       
   - (* Ijumptable *)
     econstructor. split.
@@ -781,8 +1077,33 @@ Proof.
       * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial.
         assumption.
     + econstructor; eauto.
-      assert (In pc' tbl) as IN_LIST by (eapply list_nth_z_in; eassumption).
-      IND_STEP.
+      
+      (* BEGIN INVARIANT *)
+      fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      rewrite forallb_forall in IND_step_me.
+      assert (RB.ge (invs # pc') (Some inv_pc)) as GE.
+      {
+        apply relb_leb_correct.
+        specialize IND_step_me with (pc', Some inv_pc).
+        apply IND_step_me.
+        apply (in_map (fun pc'0 : node => (pc'0, Some inv_pc))).
+        eapply list_nth_z_in.
+        eassumption.
+      }
+      destruct (invs # pc'); cbn in *.
+      2: contradiction.
+      eapply rel_ge; eauto.
+      (* END INVARIANT *)
 
   - (* Ireturn *)
     destruct or as [arg | ].
@@ -824,9 +1145,18 @@ Proof.
         apply wt_init_regs.
         rewrite <- wt_params in WTARGS.
         assumption.
-      * rewrite @checked_is_inductive_entry with (tenv:=tenv) (ctx:=(context_from_hints (snd (preanalysis tenv f)))).
-        ** apply sem_rel_b_top.
-        ** apply transf_function_invariants_inductive with (tf:=tf); auto.
+      * assert ((check_inductiveness f tenv (fst (preanalysis tenv f)))=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+        unfold check_inductiveness in IND.
+        rewrite andb_true_iff in IND.
+        destruct IND as [IND_entry IND_step].
+        clear IND_step.
+        apply RB.beq_correct in IND_entry.
+        unfold RB.eq in *.
+        destruct ((fst (preanalysis tenv f)) # (fn_entrypoint f)).
+        2: contradiction.
+        cbn.
+        rewrite <- IND_entry.
+        apply sem_rel_top.
            
   - (* external *)
     simpl in FUN.