progress moving to list of items

3 files changed, 233 insertions, 92 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 8cfbaaa1..46ae4aea 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -127,9 +127,6 @@ End RELATION.
 Module RB := ADD_BOTTOM(RELATION).
 Module DS := Dataflow_Solver(RB)(NodeSetForward).
 
-Inductive abst_insn_out :=
-| Abst_same : RB.t -> abst_insn_out.
-
 Inductive sym_op : Type :=
 | SOp : operation -> sym_op
 | SLoad : memory_chunk -> addressing -> sym_op.
@@ -464,28 +461,29 @@ Section OPERATIONS.
     | _ => rel
     end.
 
-  Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : abst_insn_out :=
+  Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) :=
   match instr with
-  | Inop _
-  | Icond _ _ _ _ _
-  | Ijumptable _ _ => Abst_same (Some rel)
-  | Istore chunk addr args src _ =>
-    Abst_same (Some (store tenv chunk addr args src rel))
-  | Iop op args dst _ => Abst_same (Some (oper dst (SOp op) args rel))
-  | Iload trap chunk addr args dst _ => Abst_same (Some (oper dst (SLoad chunk addr) args rel))
-  | Icall _ _ _ dst _ => Abst_same (Some (kill_reg dst (kill_mem rel)))
-  | Ibuiltin ef _ res _ => Abst_same (Some (kill_builtin_res res (apply_external_call ef rel)))
-  | Itailcall _ _ _ | Ireturn _ => Abst_same RB.bot
+  | Inop pc' => (pc', (Some rel))::nil
+  | Icond _ _ ifso ifnot _ => (ifso, (Some rel))::(ifnot, (Some rel))::nil
+  | Ijumptable _ targets => List.map (fun pc' => (pc', (Some rel))) targets
+  | Istore chunk addr args src pc' =>
+    (pc', (Some (store tenv chunk addr args src rel)))::nil
+  | Iop op args dst pc' => (pc', (Some (oper dst (SOp op) args rel)))::nil
+  | Iload trap chunk addr args dst pc' => (pc', (Some (oper dst (SLoad chunk addr) args rel)))::nil
+  | Icall _ _ _ dst pc' => (pc', (Some (kill_reg dst (kill_mem rel))))::nil
+  | Ibuiltin ef _ res pc' => (pc', (Some (kill_builtin_res res (apply_external_call ef rel))))::nil
+  | Itailcall _ _ _ | Ireturn _ => nil
   end.
   End PER_NODE.
 
-Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : abst_insn_out :=
-  match ro with
-  | None => Abst_same RB.bot
-  | Some x =>
-    match code ! pc with
-    | None => Abst_same RB.bot
-    | Some instr => apply_instr pc tenv instr x
+Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) :
+  list (node * RB.t)  :=
+  match code ! pc with
+  | None => nil
+  | Some instr => 
+    match ro with
+    | None => List.map (fun pc' => (pc', RB.bot)) (successors_instr instr)
+    | Some x => apply_instr pc tenv instr x
     end
   end.
 
@@ -507,12 +505,10 @@ Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: inva
          match PMap.get pc inv with
          | None => true
          | Some rel =>
-           match apply_instr pc tenv instr rel with
-           | Abst_same rel' =>
-             List.forallb
-               (fun pc' => relb_leb rel' (PMap.get pc' inv))
-               (RTL.successors_instr instr)
-           end
+           List.forallb
+             (fun szz =>
+                relb_leb (snd szz) (PMap.get (fst szz) inv))
+             (apply_instr pc tenv instr rel)
          end).
 (* No longer used. Incompatible with transfer functions that yield a different result depending on the successor.
 
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 10ffe760..8cc009cc 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -1288,6 +1288,7 @@ Section SOUNDNESS.
 
   Hint Resolve external_call_sound : cse3.
 
+  (*
   Section INDUCTIVENESS.
     Variable fn : RTL.function.
     Variable tenv : typing_env.
@@ -1348,4 +1349,5 @@ Section SOUNDNESS.
   End INDUCTIVENESS.
 
   Hint Resolve checked_is_inductive_allstep checked_is_inductive_entry : cse3.
+  *)
 End SOUNDNESS.
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 9a55f529..972cae5f 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -422,6 +422,7 @@ Qed.
 
 Hint Resolve sem_rel_b_top : cse3.
 
+(*
 Ltac IND_STEP :=
         match goal with
         REW: (fn_code ?fn) ! ?mpc = Some ?minstr
@@ -442,20 +443,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)))).
+  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'.
@@ -517,9 +540,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'.
@@ -576,8 +618,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.
@@ -633,8 +694,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.
@@ -691,8 +771,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.
@@ -705,8 +804,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]].
@@ -721,9 +839,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.
@@ -761,54 +899,48 @@ 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 *)
-    destruct (find_cond_in_fmap (ctx := (context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc cond args) as [bfound | ] eqn:FIND_COND.                                                                    
+    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. rewrite FIND_COND. reflexivity.
+        TR_AT. unfold transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity.
       * replace bfound with b.
         { econstructor; eauto.
-          assert (is_inductive_allstep (ctx:= (context_from_hints (snd (preanalysis tenv f)))) f tenv (fst  (preanalysis tenv f))) as IND by
-        (apply checked_is_inductive_allstep;
-         eapply transf_function_invariants_inductive; eassumption).
-         unfold is_inductive_allstep, is_inductive_step, apply_instr' in IND.
-         specialize IND with (pc:=pc) (pc':= if b then ifso else ifnot) (instr:= (Icond cond args ifso ifnot predb)).
-         cbn in IND.
-         rewrite H in IND.
-         assert (RB.ge (fst (preanalysis tenv f)) # (if b then ifso else ifnot)
-          match
-            match (fst (preanalysis tenv f)) # pc with
-            | Some x =>
-                apply_instr (ctx:=ctx) pc tenv (Icond cond args ifso ifnot predb) x
-            | None => Abst_same RB.bot
-            end
-          with
-          | Abst_same rel' => rel'
-          end) as INDUCTIVE by (destruct b; intuition).
-         clear IND.
-
-         change node with positive.
-
-         destruct ((fst (preanalysis tenv f)) # pc).
-         2: exfalso; exact REL.
-         
-         destruct ((fst (preanalysis tenv f)) # (if b then ifso else ifnot)).
-          - eapply rel_ge. exact INDUCTIVE. exact REL.
-          - cbn in INDUCTIVE. exfalso. exact INDUCTIVE.
+          admit.
         }
-        unfold find_cond_in_fmap in FIND_COND.
-        change RB.t with (option RELATION.t) in REL.
-        change Regmap.get with PMap.get in REL.
-        destruct (@PMap.get (option RELATION.t) pc
-                            (@fst invariants analysis_hints (preanalysis tenv f))) as [rel | ] eqn:FIND_REL.
-        2: discriminate.
+        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 (is_condition_present pc rel cond args).
         { rewrite COND_PRESENT_TRUE in H0 by trivial.
           congruence.
@@ -834,7 +966,8 @@ Proof.
             congruence.
           }
           unfold fmap_sem.
-          change RB.t with (option RELATION.t).
+          unfold sem_rel_b.
+          fold invs.
           rewrite FIND_REL.
           exact REL.
         }
@@ -850,20 +983,22 @@ Proof.
             destruct b; trivial; cbn in H2; discriminate.
           }
           unfold fmap_sem.
-          change RB.t with (option RELATION.t).
+          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. rewrite FIND_COND.
+        ** 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.
-       destruct b; IND_STEP.
+       admit.
       
   - (* Ijumptable *)
     econstructor. split.
@@ -872,8 +1007,7 @@ 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.
+      admit.
 
   - (* Ireturn *)
     destruct or as [arg | ].
@@ -915,9 +1049,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.
@@ -935,7 +1078,7 @@ Proof.
       apply wt_regset_assign; trivial.
       rewrite WTRES0.
       exact WTRES.
-Qed.
+Admitted.
 
 Lemma transf_initial_states:
   forall S1, RTL.initial_state prog S1 ->