aboutsummaryrefslogtreecommitdiffstats
path: root/kvx/lib/RTLpathSE_impl_junk.v
diff options
context:
space:
mode:
Diffstat (limited to 'kvx/lib/RTLpathSE_impl_junk.v')
-rw-r--r--kvx/lib/RTLpathSE_impl_junk.v98
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 *)