[BROKEN] Added wf predicate sistate - simatch_exclude_abort proven, need to modify some functions

1 files changed, 121 insertions, 77 deletions

diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v
index e38e66dd..c503936b 100644
--- a/mppa_k1c/lib/RTLpathSE_theory.v
+++ b/mppa_k1c/lib/RTLpathSE_theory.v
@@ -110,24 +110,32 @@ Definition sabort_exits ge sp (lx: list sistate_exit) rs0 m0: Prop :=
   exists ext,  List.In ext lx
     /\ seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = None.
 
-
-Inductive simatch_exits (ge: RTL.genv) (sp:val) (lx:list sistate_exit) (rs0: regset) (m0: mem) rs m pc: Prop :=
-  simatch_exits_intro ext lx':
-    is_tail (ext::lx') lx ->
-    all_fallthrough ge sp lx' rs0 m0 ->
-    seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = Some true ->
-    simatch_local ge sp ext.(si_elocal) rs0 m0 rs m ->
-    ext.(si_ifso) = pc ->
-    simatch_exits ge sp lx rs0 m0 rs m pc.
-
+Inductive simatch_exits (ge: RTL.genv) (sp: val) (lx: list sistate_exit) (rs: regset) (m: mem) rs' m' (pc': node) : Prop :=
+  simatch_exits_intro: forall ext lx',
+    lx = ext::lx' ->
+    all_fallthrough ge sp lx' rs m ->
+    seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m = Some true ->
+    simatch_local ge sp (si_elocal ext) rs m rs' m' ->
+    (si_ifso ext) = pc' ->
+    simatch_exits ge sp lx rs m rs' m' pc'.
+
+(* Ensuring there isn't more sistate_local after taking a branch *)
+Inductive simatch_exits_bind (ext: sistate_exit) (loc: sistate_local) : Prop :=
+  simatch_exits_bind_intro:
+    (forall ge sp lx rs m rs' m' pc', simatch_exits ge sp (ext::lx) rs m rs' m' pc' -> si_elocal ext = loc) ->
+    simatch_exits_bind ext loc.
+
+Definition sistate_wf exits loc :=
+  exists ext lx, exits = ext::lx /\ simatch_exits_bind ext loc.
 
 (** * Syntax and Semantics of symbolic internal state *)
-Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local }. 
+Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local;
+                    si_wf: sistate_wf si_exits si_local }. 
 
 Definition simatch (ge: RTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem) (is: istate): Prop :=
   if (is.(icontinue)) 
   then 
-    simatch_local ge sp st.(si_local) rs0 m0 is.(irs) is.(imem)
+    simatch_local ge sp st.(si_local) rs0 m0 is.(irs) is.(imem) 
     /\ st.(si_pc) = is.(ipc)
     /\ all_fallthrough ge sp st.(si_exits) rs0 m0
   else simatch_exits ge sp st.(si_exits) rs0 m0 is.(irs) is.(imem) is.(ipc).
@@ -162,7 +170,7 @@ Definition istate_eq ist1 ist2 :=
 
 (* TODO: is it useful 
 Lemma has_not_yet_exit_cons_split ge sp ext lx rs0 m0:
-   all_fallthrough ge sp (ext::lx) rs0 m0 <->
+   all_fallthrough ge sp (ext::lx) rs0 m0 <-> 
     (seval_condition ge sp ext.(the_cond) ext.(cond_args) ext.(exit_ist).(si_smem) rs0 m0 = Some false /\ all_fallthrough ge sp lx rs0 m0).
 Proof.
   unfold all_fallthrough; simpl; intuition (subst; auto).
@@ -177,7 +185,7 @@ Proof.
   Local Hint Resolve is_tail_in: core.
   destruct 1 as [ext lx' lc NYE' EVAL SEM PC]. subst.
   unfold all_fallthrough; intros NYE; rewrite NYE in EVAL; eauto.
-  try congruence.
+  try congruence. rewrite lc. econstructor; eauto.
 Qed.
 
 Lemma simatch_exclude_incompatible_continue ge sp st rs m is1 is2:
@@ -249,9 +257,9 @@ Proof.
   Local Hint Resolve exit_cond_determ eq_sym: core.
   destruct 1 as [ext1 lx1 TAIL1 NYE1 EVAL1 SEM1 PC1]; subst.
   destruct 1 as [ext2 lx2 TAIL2 NYE2 EVAL2 SEM2 PC2]; subst.
-  assert (X:ext1=ext2).
-  - destruct (is_tail_bounded_total (ext1 :: lx1) (ext2::lx2) lx) as [TAIL|TAIL]; eauto.
-  - subst. destruct (simatch_local_determ ge sp (si_elocal ext2) rs0 m0 rs1 m1 rs2 m2); auto.
+  assert (X:ext1=ext2) by congruence.
+(*{ destruct (is_tail_bounded_total (ext1 :: lx1) (ext2::lx2) lx) as [TAIL|TAIL]; eauto. } *)
+  subst. destruct (simatch_local_determ ge sp (si_elocal ext2) rs0 m0 rs1 m1 rs2 m2); auto.
 Qed.
 
 Lemma simatch_determ ge sp st rs m is1 is2:
@@ -270,58 +278,94 @@ Proof.
     intuition.
 Qed.
 
-Lemma simatch_exclude_sabort_local_continue ge sp st rs m is:
-  icontinue is = true ->
+Lemma simatch_local_exclude_sabort_local ge sp st rs m rs' m':
+  simatch_local ge sp (si_local st) rs m rs' m' ->
+  all_fallthrough ge sp (si_exits st) rs m ->
   sabort_local ge sp (si_local st) rs m ->
-  simatch ge sp st rs m is -> False.
+  False.
 Proof.
-  intros CONT ABORT SEM. unfold simatch in SEM. rewrite CONT in SEM.
-  destruct SEM as (SEML & _ & _). inversion SEML as (SEML1 & SEML2 & SEML3); clear SEML.
-  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; clear ABORT.
-  - contradiction.
-  - rewrite SEML2 in ABORT2. discriminate.
-  - inv ABORT3. rewrite SEML3 in H. discriminate.
+  intros SIML ALLF ABORT. inv SIML. destruct H0 as (H0 & H0').
+  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
 Qed.
 
-Lemma simatch_exclude_sabort_local_nocontinue ge sp st rs0 m0 is:
-  icontinue is = false ->
-  sabort_local ge sp (si_local st) rs0 m0 ->
-  simatch ge sp st rs0 m0 is -> False.
+Lemma simatch_local_exclude_sabort_exits ge sp st rs m rs' m':
+  simatch_local ge sp (si_local st) rs m rs' m' ->
+  all_fallthrough ge sp (si_exits st) rs m ->
+  sabort_exits ge sp (si_exits st) rs m ->
+  False.
 Proof.
-(*   intros CONT ABORT SEM. unfold simatch in SEM. rewrite CONT in SEM.
-  destruct st as [pc si_exits iis]. simpl in *.
-  destruct is as [cont pc' rs' m']. simpl in *.
-  inv SEM. inversion H2 as (SEML1 & SEML2 & SEML3); clear H2.
-  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; clear ABORT.
-  - Search iis.
-  - rewrite SEML2 in ABORT2. discriminate.
-  - inv ABORT3. rewrite SEML3 in H. discriminate. *)
-Admitted.
+  intros SIML ALLF ABORT. inv ABORT. inv H.
+  unfold all_fallthrough in ALLF. apply ALLF in H0. congruence.
+Qed.
 
+Lemma simatch_local_exclude_sabort ge sp st rs m rs' m':
+  simatch_local ge sp (si_local st) rs m rs' m' ->
+  all_fallthrough ge sp (si_exits st) rs m ->
+  sabort ge sp st rs m ->
+  False.
+Proof.
+  intros SIML ALLF ABORT.
+  inv ABORT.
+  - eapply simatch_local_exclude_sabort_local; eauto.
+  - eapply simatch_local_exclude_sabort_exits; eauto.
+Qed.
 
-Lemma simatch_exclude_sabort_local ge sp st rs m is:
+Lemma simatch_exits_exclude_sabort_local ge sp st rs m rs' m' pc':
+  simatch_exits ge sp (si_exits st) rs m rs' m' pc' ->
   sabort_local ge sp (si_local st) rs m ->
-  simatch ge sp st rs m is -> False.
+  False.
 Proof.
-  intros. destruct (icontinue is) eqn:CONT.
-  - eapply simatch_exclude_sabort_local_continue; eauto.
-  - eapply simatch_exclude_sabort_local_nocontinue; eauto.
+  destruct st as [spc exits loc SISTWF]. simpl.
+  intros SIMEX ABORT. inv SISTWF. inv H. inv H0.
+  inversion SIMEX. subst. inv H.
+  inv H1. eapply H in SIMEX. subst. clear H.
+  inv H3. destruct H1 as (H1 & H1').
+  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
 Qed.
 
-Lemma simatch_exclude_sabort_exits ge sp st rs m is:
-  sabort_exits ge sp (si_exits st) rs m ->
-  simatch ge sp st rs m is -> False.
+(* Weaker version if we don't have the simatch_exits_bind - not used anymore, couldn't get any use from it *)
+Remark simatch_exits_exclude_sabort_local' ge sp rs m rs' m' pc' exits ext:
+  simatch_exits ge sp (ext::exits) rs m rs' m' pc' ->
+  sabort_local ge sp (si_elocal ext) rs m ->
+  False.
 Proof.
-Admitted.
+  intros SIMEX ABORT.
+  inv SIMEX. inv H. inv H2. destruct H3 as (H3 & H3').
+  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
+Qed.
+
+Lemma simatch_exits_exclude_sabort_exits ge sp exits rs m rs' m' pc':
+  simatch_exits ge sp exits rs m rs' m' pc' ->
+  sabort_exits ge sp exits rs m ->
+  False.
+Proof.
+  intros SIMEX ABORT.
+  inv ABORT. inv H. inv SIMEX. unfold all_fallthrough in H2.
+  inv H0.
+  - congruence.
+  - apply H2 in H. congruence.
+Qed.
+
+Lemma simatch_exits_exclude_sabort ge sp st rs m rs' m' pc':
+  simatch_exits ge sp (si_exits st) rs m rs' m' pc' ->
+  sabort ge sp st rs m ->
+  False.
+Proof.
+  intros SIME ABORT.
+  inv ABORT.
+  - eapply simatch_exits_exclude_sabort_local; eauto.
+  - eapply simatch_exits_exclude_sabort_exits; eauto.
+Qed.
 
 Lemma simatch_exclude_sabort ge sp st rs m is:
   sabort ge sp st rs m ->
   simatch ge sp st rs m is -> False.
 Proof.
   intros ABORT SEM.
-  inv ABORT.
-  - eapply simatch_exclude_sabort_local; eauto.
-  - eapply simatch_exclude_sabort_exits; eauto.
+  unfold simatch in SEM. destruct icontinue.
+  - destruct SEM as (SEM1 & SEM2 & SEM3).
+    eapply simatch_local_exclude_sabort; eauto.
+  - eapply simatch_exits_exclude_sabort; eauto.
 Qed.
 
 Definition istate_eq_opt ist1 oist :=
@@ -353,7 +397,7 @@ Definition sist_set_local (st: sistate) (pc: node) (nxt: sistate_local): option
    Some {| si_pc := pc; si_exits := st.(si_exits); si_local:= nxt |}.
 
 (* FIXME - add notrap *)
-Definition sistep (i: instruction) (st: sistate): option sistate :=
+Definition sistep (i: instruction) (st: sistate): option sistate := 
   match i with
   | Inop pc' => 
       sist_set_local st pc' st.(si_local)
@@ -420,7 +464,7 @@ Proof.
   unfold sabort_local. simpl; intuition.
 Qed.
 
-Lemma sistep_preserves_sabort i ge sp rs0 m0 st st':
+Lemma sistep_preserves_sabort i ge sp rs0 m0 st st': 
   sistep i st = Some st' ->
   sabort ge sp st rs0 m0 -> sabort ge sp st' rs0 m0.
 Proof.
@@ -463,7 +507,7 @@ Proof.
         subst; rewrite Regmap.gss; simpl; auto.
         erewrite seval_list_sval_inj; simpl; auto.
         try_simplify_someHyps.
-    - unfold sabort, sabort_local; simpl.
+    - unfold sabort, sabort_local; simpl. 
       left. right. right.
       exists r. destruct (Pos.eq_dec r r); try congruence.
       simpl. erewrite seval_list_sval_inj; simpl; auto.
@@ -482,7 +526,7 @@ Proof.
         exists r. destruct (Pos.eq_dec r r); try congruence.
         simpl. erewrite seval_list_sval_inj; simpl; auto.
         try_simplify_someHyps. }
-    { unfold sabort, sabort_local; simpl.
+    { unfold sabort, sabort_local; simpl. 
       left. right. right.
       exists r. destruct (Pos.eq_dec r r); try congruence.
       simpl. erewrite seval_list_sval_inj; simpl; auto.
@@ -527,7 +571,7 @@ Admitted.
 
 Lemma sistep_correct_None ge sp i st rs0 m0 rs m:
   simatch_local ge sp (st.(si_local)) rs0 m0 rs m ->
-  sistep i st = None ->
+  sistep i st = None -> 
   istep ge i sp rs m = None.
 Proof.
   intros (PRE & MEM & REG).
@@ -544,9 +588,9 @@ Fixpoint sisteps (path:nat) (f: function) (st: sistate): option sistate :=
     sisteps p f st1
   end.
 
-Lemma sisteps_correct_false ge sp path f rs0 m0 st' is:
+Lemma sisteps_correct_false ge sp path f rs0 m0 st' is: 
   is.(icontinue)=false ->
-  forall st, simatch ge sp st rs0 m0 is ->
+  forall st, simatch ge sp st rs0 m0 is -> 
   sisteps path f st = Some st' ->
   simatch ge sp st' rs0 m0 is.
 Proof.
@@ -558,7 +602,7 @@ Proof.
     inversion_SOME st1; eauto.
 Qed.
 
-Lemma sisteps_preserves_sabort ge sp path f rs0 m0 st': forall st,
+Lemma sisteps_preserves_sabort ge sp path f rs0 m0 st': forall st, 
   sisteps path f st = Some st' ->
   sabort ge sp st rs0 m0 -> sabort ge sp st' rs0 m0.
 Proof.
@@ -592,7 +636,7 @@ Qed.
 
 Lemma sisteps_correct_true ge sp path (f:function) rs0 m0: forall st is,
   is.(icontinue)=true ->
-  simatch ge sp st rs0 m0 is ->
+  simatch ge sp st rs0 m0 is -> 
   nth_default_succ (fn_code f) path st.(si_pc) <> None ->
   simatch_opt2 ge sp (sisteps path f st) rs0 m0
                          (isteps ge path f sp is.(irs) is.(imem) is.(ipc))
@@ -608,7 +652,7 @@ Proof.
     intros (LOCAL & PC & NYE) WF.
     rewrite <- PC.
     inversion_SOME i; intro Hi; rewrite Hi in WF |- *; simpl; auto.
-    exploit sistep_correct; eauto.
+    exploit sistep_correct; eauto. 
     inversion_SOME st1; intros Hst1; erewrite Hst1; simpl.
     - inversion_SOME is1; intros His1;rewrite His1; simpl. 
       * destruct (icontinue is1) eqn:CONT1.
@@ -707,7 +751,7 @@ Inductive sfmatch (pge: RTLpath.genv) (ge: RTL.genv) (sp:val) (st: sistate) stac
       sp = (Vptr stk Ptrofs.zero) ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       match osv with Some sv => seval_sval ge sp sv rs0 m0 | None => Some Vundef end = Some v ->
-      sfmatch pge ge sp st stack f rs0 m0 (Sreturn osv) rs m
+      sfmatch pge ge sp st stack f rs0 m0 (Sreturn osv) rs m 
          E0 (Returnstate stack v m')
 .
 
@@ -716,17 +760,17 @@ Record sstate := { internal:> sistate; final: sfval }.
 Inductive smatch pge (ge: RTL.genv) (sp:val) (st: sstate) stack f (rs0: regset) (m0: mem): trace -> state -> Prop :=
   | smatch_early is:
      is.(icontinue) = false ->
-     simatch ge sp st rs0 m0 is ->
+     simatch ge sp st rs0 m0 is -> 
      smatch pge ge sp st stack f rs0 m0 E0 (State stack f sp is.(ipc) is.(irs) is.(imem))
   | smatch_normal is t s:
      is.(icontinue) = true ->
-     simatch ge sp st rs0 m0 is ->
+     simatch ge sp st rs0 m0 is ->  
      sfmatch pge ge sp st stack f rs0 m0 st.(final) is.(irs) is.(imem) t s ->
-     smatch pge ge sp st stack f rs0 m0 t s
+     smatch pge ge sp st stack f rs0 m0 t s 
   .
 
 (** * Symbolic execution of final step *)
-Definition sfstep (i: instruction) (prev: sistate_local): sfval :=
+Definition sfstep (i: instruction) (prev: sistate_local): sfval := 
   match i with
   | Icall sig ros args res pc => 
     let svos := sum_left_map prev.(si_sreg) ros in
@@ -743,7 +787,7 @@ Lemma sfstep_correct pge ge sp i (f:function) pc st stack rs0 m0 t rs m s:
   pc = st.(si_pc) ->
   simatch_local ge sp (si_local st) rs0 m0 rs m ->
   path_last_step ge pge stack f sp pc rs m t s ->
-  sistep i st = None ->
+  sistep i st = None -> 
   sfmatch pge ge sp st stack f rs0 m0 (sfstep i (si_local st)) rs m t s.
 Proof.
   intros PC1 PC2 (PRE&MEM&REG) LAST Hi. destruct LAST; subst; try_simplify_someHyps; simpl.
@@ -818,9 +862,9 @@ Lemma symb_path_last_step i st st' ge pge stack (f:function) sp pc rs m t s:
   pc = st.(si_pc) ->
   sistep i st = Some st' ->
   path_last_step ge pge stack f sp pc rs m t s ->
-  exists mk_istate,
-     istep ge i sp rs m = Some mk_istate
-  /\ t = E0
+  exists mk_istate, 
+     istep ge i sp rs m = Some mk_istate 
+  /\ t = E0 
   /\ s = (State stack f sp mk_istate.(ipc) mk_istate.(RTLpath.irs) mk_istate.(imem)).
 Proof.
   intros PC1 PC2 Hst' LAST; destruct LAST; subst; try_simplify_someHyps; simpl.
@@ -829,7 +873,7 @@ Qed.
 (* NB: each concrete execution can be executed on the symbolic state (produced from [sstep]) 
 (sstep is a correct over-approximation)
 *)
-Theorem sstep_correct f pc pge ge sp path stack rs m t s:
+Theorem sstep_correct f pc pge ge sp path stack rs m t s: 
   (fn_path f)!pc = Some path ->
   path_step ge pge path.(psize) stack f sp rs m pc t s ->
   exists st, sstep f pc = Some st /\ smatch pge ge sp st stack f rs m t s.
@@ -846,7 +890,7 @@ Proof.
    (* intro SEM *)
    (simpl; unfold simatch; simpl; rewrite CONT; intro SEM);
    (* intro Hi' *)
-   ( assert (Hi': (fn_code f) ! (si_pc st) = Some i);
+   ( assert (Hi': (fn_code f) ! (si_pc st) = Some i); 
      [ unfold nth_default_succ_inst in Hi; 
        exploit sisteps_default_succ; eauto; simpl;
        intros DEF; rewrite DEF in Hi; auto 
@@ -963,9 +1007,9 @@ Qed.
 (* NB: each execution of a symbolic state (produced from [sstep]) represents a concrete execution
   (sstep is exact).
 *)
-Theorem sstep_exact f pc pge ge sp path stack st rs m t s1:
+Theorem sstep_exact f pc pge ge sp path stack st rs m t s1: 
   (fn_path f)!pc = Some path ->
-  sstep f pc = Some st ->
+  sstep f pc = Some st -> 
   smatch pge ge sp st stack f rs m t s1 ->
   exists s2, path_step ge pge path.(psize) stack f sp rs m pc t s2 /\ 
              equiv_state s1 s2.
@@ -1087,7 +1131,7 @@ Definition istate_simu f (srce: PTree.t node) is1 is2: Prop :=
         sur la dernière instruction du superblock. *)
      istate_simulive (fun _ => True) srce is1 is2
   else
-     exists path, f.(fn_path)!(is1.(ipc)) = Some path
+     exists path, f.(fn_path)!(is1.(ipc)) = Some path 
      /\ istate_simulive (fun r => Regset.In r path.(input_regs)) srce is1 is2
      /\ srce!(is2.(ipc)) = Some is1.(ipc).
 
@@ -1096,7 +1140,7 @@ Definition sistate_simu (f: RTLpath.function) (srce: PTree.t node) (st1 st2: sis
   forall sp ge1 ge2, 
   (forall s, Genv.find_symbol ge2 s = Genv.find_symbol ge1 s) ->
   liveness_ok_function f ->
-  forall rs m is1, simatch ge1 sp st1 rs m is1 ->
+  forall rs m is1, simatch ge1 sp st1 rs m is1 -> 
      exists is2, simatch ge2 sp st2 rs m is2 /\ istate_simu f srce is1 is2.
 
 (* NOTE: a syntactic definition on [sfval] in order to abstract the [match_states] *)
@@ -1115,7 +1159,7 @@ Definition sstate_simu f srce (s1 s2: sstate): Prop :=
     /\ sfval_simu f srce s1.(si_pc) s2.(si_pc) s1.(final) s2.(final).
 
 Definition sstep_simu srce (f1 f2: RTLpath.function) pc1 pc2: Prop :=
-    forall st1, sstep f1 pc1 = Some st1 ->
+    forall st1, sstep f1 pc1 = Some st1 -> 
     exists st2, sstep f2 pc2 = Some st2 /\ sstate_simu f1 srce st1 st2.
 
 (* IDEA: we will provide an efficient test for checking "sstep_simu" property, by hash-consing.