diff options
Diffstat (limited to 'kvx/lib/RTLpathSE_impl_junk.v')
-rw-r--r-- | kvx/lib/RTLpathSE_impl_junk.v | 98 |
1 files changed, 71 insertions, 27 deletions
diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index 7a017047..342c9f30 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -577,9 +577,9 @@ Proof. Qed. Definition hsilocal_simu_core (oalive: option Regset.t) (hst1 hst2: hsistate_local) := -(* is_subset (hsi_lsmem hst2) (hsi_lsmem hst1) *) incl (hsi_ok_lsval hst2) (hsi_ok_lsval hst1) - /\ (forall r, (match oalive with Some alive => Regset.In r alive | _ => True end) -> hsi_sreg_get hst2 r = hsi_sreg_get hst1 r) + /\ (forall r, (match oalive with Some alive => Regset.In r alive | _ => True end) -> (* hsi_sreg_get hst2 r = hsi_sreg_get hst1 r *) + PTree.get r hst2 = PTree.get r hst1) /\ hsi_smem hst1 = hsi_smem hst2. Lemma hseval_preserved ge ge' rs0 m0 sp hsv: @@ -621,7 +621,7 @@ Definition seval_sval_partial ge sp rs0 m0 hsv := Definition select_first (ox oy: option val) := match ox with | Some v => Some v - | None => SOME v <- oy IN Some v + | None => oy end. (** If the register was computed by hrs, evaluate the symbolic value from hrs. @@ -684,16 +684,21 @@ Proof. ++ unfold seval_sval_partial. assert (seval_hsval ge2 sp h rs0 m0 = hsi_sreg_eval ge2 sp hst2 r rs0 m0). { unfold hsi_sreg_eval. rewrite HST2. reflexivity. } - rewrite H. clear H. assert (TODO: exists hv, hsi_sreg_get hst2 r ~~> hv) by admit. - destruct TODO as (hv & HGET2). rewrite hsi_sreg_eval_correct; [|eassumption]. - rewrite C in HGET2; [|assumption]. erewrite hseval_preserved; [| eapply GFS]. - rewrite <- hsi_sreg_eval_correct; [|eassumption]. rewrite B; [|assumption]. - rewrite RSEQ. reflexivity. - ++ rewrite <- RSEQ. rewrite <- B; [|assumption]. - assert (TODO: exists hv, hsi_sreg_get hst1 r ~~> hv) by admit. + rewrite H. clear H. (*assert (TODO: exists hv, hsi_sreg_get hst2 r ~~> hv) by admit. + destruct TODO as (hv & HGET2). rewrite hsi_sreg_eval_correct; [|eassumption].*) + unfold hsi_sreg_eval. rewrite HST2. + erewrite hseval_preserved; [| eapply GFS]. + unfold hsi_sreg_eval in B. + generalize (B HOK1 r); clear B; intro B. + rewrite <- C in B; eauto. + rewrite HST2 in B. + rewrite B, RSEQ. + reflexivity. + ++ rewrite <- RSEQ. rewrite <- B; [|assumption]. admit. (* FIXME *) +(* assert (TODO: exists hv, hsi_sreg_get hst1 r ~~> hv) by admit. destruct TODO as (hv & HGET1). rewrite hsi_sreg_eval_correct; [|eassumption]. rewrite <- C in HGET1; [|assumption]. rewrite <- hsi_sreg_eval_correct; [|eassumption]. - unfold hsi_sreg_eval. rewrite HST2. reflexivity. + unfold hsi_sreg_eval. rewrite HST2. reflexivity. *) - constructor; [|constructor]. + destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2. + destruct HREF2 as (_ & MEMEQ2 & _). destruct HREF1 as (_ & MEMEQ1 & _). @@ -701,13 +706,13 @@ Proof. rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3. erewrite hsmem_eval_preserved; [| eapply GFS]. rewrite MEMEQ1; auto. + intro r. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _). - destruct CORE as (_ & C & _). rewrite <- A; auto. - assert (TODO: exists hv, hsi_sreg_get hst2 r ~~> hv) by admit. destruct TODO as (hv & HGET2). + destruct CORE as (_ & C & _). rewrite <- A; auto. admit. (* FIXME *) +(* assert (TODO: exists hv, hsi_sreg_get hst2 r ~~> hv) by admit. destruct TODO as (hv & HGET2). rewrite hsi_sreg_eval_correct; [|eassumption]. rewrite C in HGET2; [|auto]. erewrite hseval_preserved; [| eapply GFS]. rewrite <- hsi_sreg_eval_correct; [|eassumption]. rewrite B; auto. -Admitted. (** FIXME - requires to add some hypothesis that hsi_sreg_get may return something *) + *)Admitted. (** FIXME - requires to add some hypothesis that hsi_sreg_get may return something *) Definition hsilocal_simu_check hst1 hst2 : ?? unit := phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_simu_check: hsi_smem sets aren't equiv";; @@ -747,14 +752,17 @@ Proof. apply setoid_in. assumption. Qed. +Local Hint Resolve PTree_frame_eq_check_correct: wlp. +Local Hint Resolve regset_elements_in: core. + Theorem hsilocal_frame_simu_check_correct hst1 hst2 alive: WHEN hsilocal_frame_simu_check (Regset.elements alive) hst1 hst2 ~> tt THEN hsilocal_simu_core (Some alive) hst1 hst2. Proof. wlp_simplify. constructor; [|constructor]; [assumption | | congruence]. - intros. unfold hsi_sreg_get. - rewrite (PTree_frame_eq_check_correct _ (Regset.elements alive) hst1 hst2); [reflexivity | eassumption | ]. - apply regset_elements_in. assumption. + intros. symmetry. eauto. +(* rewrite (PTree_frame_eq_check_correct _ (Regset.elements alive) hst1 hst2); [reflexivity | eassumption | ]. + apply regset_elements_in. assumption. *) Qed. Hint Resolve hsilocal_frame_simu_check_correct: wlp. Global Opaque hsilocal_frame_simu_check. @@ -937,14 +945,11 @@ Theorem hsiexits_simu_check_correct dm f: forall le1 le2, WHEN hsiexits_simu_check dm f le1 le2 ~> tt THEN hsiexits_simu_core dm f le1 le2. Proof. - induction le1; intros; wlp_simplify. - - destruct le2; [constructor|]. simpl in Hexta. (* Absurd case *) admit. - - destruct le2. - + (* Absurd case again *) admit. - + assert (hsiexit_simu_check dm f a h ~~> tt /\ hsiexits_simu_check dm f le1 le2 ~~> exta). { admit. } - destruct H as (A & B). apply hsiexit_simu_check_correct in A. - constructor; [assumption|]. apply IHle1 in B. assumption. -Admitted. + induction le1; simpl. + - destruct le2; wlp_simplify. constructor. + - destruct le2; wlp_simplify. constructor; [assumption|]. + eapply IHle1. eassumption. +Qed. Hint Resolve hsiexits_simu_check_correct: wlp. Global Opaque hsiexits_simu_check. @@ -1258,6 +1263,27 @@ Proof. erewrite IHlist_refines; eauto. Qed. +Lemma barg_proj_refines_eq ge ge' sp rs0 m0: forall lsv lhsv, + (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) -> + list_forall2 (barg_refines ge sp rs0 m0) lhsv lsv -> + forall lhsv' lsv', + list_forall2 (barg_refines ge' sp rs0 m0) lhsv' lsv' -> + barg_list_proj lhsv = barg_list_proj lhsv' -> + seval_list_builtin_sval ge sp lsv rs0 m0 = seval_list_builtin_sval ge' sp lsv' rs0 m0. +Proof. + induction 2; rename H into GFS. + - simpl. intros. destruct lhsv'; try discriminate. clear H0. + inv H. simpl. reflexivity. + - simpl. intros. destruct lhsv'; try discriminate. + simpl in H2. inv H2. destruct lsv'; [inv H|]. + inv H. simpl. + assert (SVALEQ: seval_builtin_sval ge sp b1 rs0 m0 = seval_builtin_sval ge' sp b0 rs0 m0). { + admit. +(* rewrite <- H10. rewrite <- H1. unfold seval_hsval. erewrite <- seval_preserved; [| eapply GFS]. congruence. *) + } rewrite SVALEQ. + erewrite IHlist_forall2; eauto. +Admitted. + Definition final_simu_core (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (f1 f2: sfval): Prop := match f1 with | Scall sig1 svos1 lsv1 res1 pc1 => @@ -1328,9 +1354,27 @@ Proof. simpl in SVOSEQ. inv SVOSEQ. congruence. + erewrite list_proj_refines_eq; eauto. constructor. (* Stailcall *) - - admit. + - rename H3 into SREF1. rename H4 into LREF1. + destruct hf2; try (inv CORE; fail). inv FREF2. + rename H4 into LREF2. rename H3 into SREF2. + inv CORE. rename H1 into SVOSEQ. rename H2 into LSVEQ. + constructor. + + destruct svos. (** Copy-paste from Scall *) + * destruct svos0; try discriminate. destruct ros; try contradiction. + destruct ros0; try contradiction. constructor. + simpl in SVOSEQ. inv SVOSEQ. + simpl in SREF1. simpl in SREF2. + rewrite <- SREF1. rewrite <- SREF2. unfold seval_hsval. + erewrite <- seval_preserved; [| eapply GFS]. congruence. + * destruct svos0; try discriminate. destruct ros; try contradiction. + destruct ros0; try contradiction. constructor. + simpl in SVOSEQ. inv SVOSEQ. congruence. + + erewrite list_proj_refines_eq; eauto. constructor. (* Sbuiltin *) - - admit. + - rename H4 into BREF1. destruct hf2; try (inv CORE; fail). inv FREF2. + rename H4 into BREF2. inv CORE. destruct H0 as (? & ? & ?). subst. + rename H into PCEQ. rename H1 into ARGSEQ. constructor; [assumption|]. clear PCEQ. + admit. (* too strong to prove *) (* Sjumptable *) - admit. (* Sreturn *) |