From 47217508d25a83d97773592a141a40854003f893 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 26 Aug 2020 11:51:54 +0200 Subject: Avancement divers --- kvx/lib/RTLpathSE_impl.v | 10 ++-- kvx/lib/RTLpathSE_impl_junk.v | 98 ++++++++++++++++++++++++++----------- kvx/lib/RTLpathSE_theory.v | 105 +++++++++++++++++++++++++++++++++++++++- kvx/lib/RTLpathSchedulerproof.v | 4 +- 4 files changed, 183 insertions(+), 34 deletions(-) (limited to 'kvx') diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v index a18678b8..4bf4b03a 100644 --- a/kvx/lib/RTLpathSE_impl.v +++ b/kvx/lib/RTLpathSE_impl.v @@ -513,15 +513,15 @@ Proof. - simpl in CORE. rewrite <- CORE. constructor; [apply svident_simu_refl|]. erewrite <- list_sval_eval_preserved; [| eapply ctx]. constructor. (* Sbuiltin *) - - simpl in CORE. destruct hf2; try contradiction. destruct CORE as (PCEQ & ? & ? & ?). subst. - constructor; [assumption | reflexivity]. + - (* simpl in CORE. destruct hf2; try contradiction. destruct CORE as (PCEQ & ? & ? & ?). subst. + constructor; [assumption | reflexivity]. *) admit. (* Sjumptable *) - simpl in CORE. destruct hf2; try contradiction. destruct CORE as (PCEQ & ?). subst. constructor; [assumption|]. erewrite <- seval_preserved; [| eapply ctx]. constructor. (* Sreturn *) - simpl in CORE. subst. constructor. -Qed. +Admitted. Record hsstate := { hinternal:> hsistate; hfinal: sfval }. @@ -1611,9 +1611,9 @@ Proof. + admit. + admit. (* Sbuiltin *) - - destruct fv2; try discriminate. intro. explore. + - (* destruct fv2; try discriminate. intro. explore. apply revmap_check_single_correct in EQ1. apply list_builtin_arg_simub_correct in EQ2. - subst. constructor; auto. + subst. constructor; auto. *) admit. (* Sjumptable *) - destruct fv2; try discriminate. intro. explore. apply revmap_check_list_correct in EQ. apply sval_simub_correct in EQ0. subst. 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 *) diff --git a/kvx/lib/RTLpathSE_theory.v b/kvx/lib/RTLpathSE_theory.v index ad8d899e..3ae6e713 100644 --- a/kvx/lib/RTLpathSE_theory.v +++ b/kvx/lib/RTLpathSE_theory.v @@ -1715,6 +1715,108 @@ Proof. constructor; eauto. congruence. Qed. +Fixpoint seval_builtin_sval ge sp bsv rs0 m0 := match bsv with + | BA sv => SOME v <- seval_sval ge sp sv rs0 m0 IN Some (BA v) + | BA_splitlong sv1 sv2 => + SOME v1 <- seval_builtin_sval ge sp sv1 rs0 m0 IN + SOME v2 <- seval_builtin_sval ge sp sv2 rs0 m0 IN + Some (BA_splitlong v1 v2) + | BA_addptr sv1 sv2 => + SOME v1 <- seval_builtin_sval ge sp sv1 rs0 m0 IN + SOME v2 <- seval_builtin_sval ge sp sv2 rs0 m0 IN + Some (BA_addptr v1 v2) + | BA_int i => Some (BA_int i) + | BA_long l => Some (BA_long l) + | BA_float f => Some (BA_float f) + | BA_single s => Some (BA_single s) + | BA_loadstack chk ptr => Some (BA_loadstack chk ptr) + | BA_addrstack ptr => Some (BA_addrstack ptr) + | BA_loadglobal chk id ptr => Some (BA_loadglobal chk id ptr) + | BA_addrglobal id ptr => Some (BA_addrglobal id ptr) + end. + +Fixpoint seval_list_builtin_sval ge sp lbsv rs0 m0 := match lbsv with + | nil => Some nil + | bsv::lbsv => SOME v <- seval_builtin_sval ge sp bsv rs0 m0 IN + SOME lv <- seval_list_builtin_sval ge sp lbsv rs0 m0 IN + Some (v::lv) + end. + +Lemma seval_list_builtin_sval_nil ge sp rs0 m0 lbs2: + seval_list_builtin_sval ge sp lbs2 rs0 m0 = Some nil -> + lbs2 = nil. +Proof. + destruct lbs2; simpl; auto. + intros. destruct (seval_builtin_sval _ _ _ _ _); + try destruct (seval_list_builtin_sval _ _ _ _ _); discriminate. +Qed. + +Lemma seval_builtin_arg_sval ge sp m rs0 m0 v: forall bs, + seval_builtin_arg ge sp m rs0 m0 bs v -> + exists ba, + seval_builtin_sval ge sp bs rs0 m0 = Some ba + /\ eval_builtin_arg ge (fun id => id) sp m ba v. +Proof. + induction 1. + all: try (eexists; constructor; [simpl; reflexivity | constructor]). + 2-3: try assumption. + - eexists. constructor. + + simpl. rewrite H. reflexivity. + + constructor. + - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1). + destruct IHseval_builtin_arg2 as (ba2 & A2 & B2). + eexists. constructor. + + simpl. rewrite A1. rewrite A2. reflexivity. + + constructor; assumption. + - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1). + destruct IHseval_builtin_arg2 as (ba2 & A2 & B2). + eexists. constructor. + + simpl. rewrite A1. rewrite A2. reflexivity. + + constructor; assumption. +Qed. + +Lemma seval_builtin_args_sval ge sp m rs0 m0 lv: forall lbs, + seval_builtin_args ge sp m rs0 m0 lbs lv -> + exists lba, + seval_list_builtin_sval ge sp lbs rs0 m0 = Some lba + /\ list_forall2 (eval_builtin_arg ge (fun id => id) sp m) lba lv. +Proof. + induction 1. + - eexists. constructor. + + simpl. reflexivity. + + constructor. + - destruct IHlist_forall2 as (lba & A & B). + apply seval_builtin_arg_sval in H. destruct H as (ba & A' & B'). + eexists. constructor. + + simpl. rewrite A'. rewrite A. reflexivity. + + constructor; assumption. +Qed. + +Lemma seval_builtin_sval_correct ge sp m rs0 m0 v bs2: forall bs1, + seval_builtin_arg ge sp m rs0 m0 bs1 v -> + opt_simu (seval_builtin_sval ge sp bs1 rs0 m0) (seval_builtin_sval ge sp bs2 rs0 m0) -> + seval_builtin_arg ge sp m rs0 m0 bs2 v. +Proof. + induction 1. + - simpl. rewrite H. intros. lapply H0; [| discriminate]; clear H0; intro H0. +Admitted. + +Lemma seval_list_builtin_sval_correct ge sp m rs0 m0 vargs: forall lbs1, + seval_builtin_args ge sp m rs0 m0 lbs1 vargs -> + forall lbs2, opt_simu (seval_list_builtin_sval ge sp lbs1 rs0 m0) (seval_list_builtin_sval ge sp lbs2 rs0 m0) -> + seval_builtin_args ge sp m rs0 m0 lbs2 vargs. +Proof. + induction 1. + - simpl. intros. unfold opt_simu in H. lapply H; [|discriminate]; clear H; intro H. + exploit seval_list_builtin_sval_nil; eauto. intro. subst. constructor. + - eapply seval_builtin_arg_sval in H. destruct H as (ba & A & B). + eapply seval_builtin_args_sval in H0. destruct H0 as (lba & A' & B'). + intros. destruct lbs2. + + simpl in H. rewrite A in H. rewrite A' in H. lapply H; [|discriminate]; clear H; intro H. + discriminate. + + constructor. 2: apply IHlist_forall2. 2: admit. +Admitted. + (* NOTE: we need to mix semantical simulation and syntactic definition on [sfval] in order to abstract the [match_states] *) Inductive sfval_simu (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node) (ctx: simu_proof_context f): sfval -> sfval -> Prop := | Snone_simu: @@ -1733,7 +1835,8 @@ Inductive sfval_simu (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node) sfval_simu dm f opc1 opc2 ctx (Stailcall sig svos1 lsv1) (Stailcall sig svos2 lsv2) | Sbuiltin_simu ef lbs1 lbs2 br pc1 pc2: dm!pc2 = Some pc1 -> - lbs1 = lbs2 -> (* FIXME: TOO STRONG *) + opt_simu (seval_list_builtin_sval (the_ge1 ctx) (the_sp ctx) lbs1 (the_rs0 ctx) (the_m0 ctx)) + (seval_list_builtin_sval (the_ge2 ctx) (the_sp ctx) lbs2 (the_rs0 ctx) (the_m0 ctx)) -> sfval_simu dm f opc1 opc2 ctx (Sbuiltin ef lbs1 br pc1) (Sbuiltin ef lbs2 br pc2) | Sjumptable_simu sv1 sv2 lpc1 lpc2: ptree_get_list dm lpc2 = Some lpc1 -> diff --git a/kvx/lib/RTLpathSchedulerproof.v b/kvx/lib/RTLpathSchedulerproof.v index 5c32847e..437f1e0a 100644 --- a/kvx/lib/RTLpathSchedulerproof.v +++ b/kvx/lib/RTLpathSchedulerproof.v @@ -215,6 +215,8 @@ Proof. intros (path & PATH). eexists; split; econstructor; eauto. + eapply seval_builtin_args_preserved; eauto. + eapply seval_list_builtin_sval_correct; eauto. + admit. (* something like seval_list_builtin_sval_preserved *) + eapply external_call_symbols_preserved; eauto. + eapply eqlive_reg_refl. - (* Sjumptable *) @@ -229,7 +231,7 @@ Proof. + erewrite <- preserv_fnstacksize; eauto. + destruct os; auto. erewrite <- seval_preserved; eauto. -Qed. +Admitted. (* The main theorem on simulation of symbolic states ! *) Theorem ssem_sstate_simu dm f f' stk stk' sp st st' rs m t s: -- cgit