From c9cb80f008c919d543212dc69b5fbcd7a0d73df8 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 8 Jul 2021 11:17:45 +0200 Subject: hrexec_correct1 --- scheduling/BTL_SEimpl.v | 73 ++++++++++++++++++++++++++++++++----------------- 1 file changed, 48 insertions(+), 25 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index 25819ffa..b04c17fb 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -657,7 +657,8 @@ Lemma cbranch_expanse_correct hrs c l: (REF : ris_refines ctx hrs sis) (OK: ris_ok ctx hrs), eval_scondition ctx (fst r) (snd r) = - eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l)). + eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l)) + /\ (fst r) = c. Proof. unfold cbranch_expanse. wlp_simplify; inv REF. @@ -687,6 +688,8 @@ Proof. + destruct 1; simpl in *. unfold ris_sreg_get; simpl. intros; rewrite PTree.gempty; eauto. Qed. +Local Hint Resolve hrs_init_correct: wlp. +Global Opaque hrs_init. Definition hrs_sreg_set r lr rsv (hrs: ristate): ?? ristate := DO ok_lsv <~ @@ -935,26 +938,26 @@ Lemma hrexec_rec_correct1 ctx ib: rst_refines ctx rst st. Proof. induction ib; try (wlp_simplify; fail). - - wlp_simplify; eapply CONT; eauto. - - destruct trap; wlp_simplify. - - (* seq *) + - (* Bnop *) wlp_simplify; eapply CONT; eauto. + - (* Bload *) destruct trap; wlp_simplify. + - (* Bseq *) wlp_simplify. eapply IHib1. 3-7: eauto. + simpl. eapply sexec_rec_okpreserv; eauto. + intros; subst. eapply IHib2; eauto. - - (* cond *) + - (* Bcond *) simpl; intros; wlp_simplify. assert (rOK: ris_ok ctx hrs). { erewrite <- OK_EQUIV. 2: eauto. eapply sexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. } - generalize OUT; clear OUT; simpl. - autodestruct. - intros COND; generalize COND. - erewrite <- eval_scondition_refpreserv; eauto. - econstructor; try_simplify_someHyps. - Qed.*) -Admitted. + exploit (Refcond ctx cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1 + (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k)); + exploit H; eauto; intros (SEVAL & EQC); subst; auto. + all: simpl in SOUT; generalize SOUT; inversion_SOME b0; try_simplify_someHyps. + * intros; eapply IHib1; eauto. + * intros; eapply IHib2; eauto. +Qed. Lemma hrexec_correct1 ctx ib sis sfv: get_soutcome ctx (sexec (cf ctx) ib) = Some (sout sis sfv) -> @@ -963,14 +966,7 @@ Lemma hrexec_correct1 ctx ib sis sfv: rst_refines ctx rst (sexec (cf ctx) ib). Proof. unfold sexec; intros; wlp_simplify. - eapply hrexec_rec_correct1; eauto; simpl; try congruence; split. - - intuition eauto. - + inv H2; constructor; auto; simpl; congruence. - + inv H2; split; simpl in *; try congruence; trivial. - - intros X; simpl in *; auto. - - intros X r; inv X; simpl in *. - unfold ris_sreg_get; simpl; rewrite PTree.gempty; simpl. - reflexivity. + eapply hrexec_rec_correct1; eauto; simpl; congruence. Qed. (*Lemma hrexec_rec_correct2 ctx ib: @@ -999,7 +995,7 @@ Lemma hrexec_correct2 ctx ib hrs rfv: Proof. Admitted. -Lemma hrexec_simu_correct ctx ib: +Lemma hrexec_correct_aux ctx ib: WHEN hrexec (cf ctx) ib ~> rst THEN exists st, sexec (cf ctx) ib = st /\ rst_refines ctx rst st. Proof. @@ -1007,8 +1003,34 @@ Proof. repeat eexists. Admitted. +Global Opaque hrexec. + End CanonBuilding. +(** Correction of concrete symbolic execution wrt abstract symbolic execution *) +Theorem hrexec_correct + (hC_hsval : hashinfo sval -> ?? sval) + (hC_list_hsval : hashinfo list_sval -> ?? list_sval) + (hC_hsmem : hashinfo smem -> ?? smem) + (ctx: iblock_exec_context) + (ib: iblock): + WHEN hrexec hC_hsval hC_list_hsval hC_hsmem (cf ctx) ib ~> hrs THEN forall + (hC_hsval_correct: forall hs, + WHEN hC_hsval hs ~> hs' THEN forall ctx, + sval_refines ctx (hdata hs) hs') + (hC_list_hsval_correct: forall lh, + WHEN hC_list_hsval lh ~> lh' THEN forall ctx, + list_sval_refines ctx (hdata lh) lh') + (hC_hsmem_correct: forall hm, + WHEN hC_hsmem hm ~> hm' THEN forall ctx, + smem_refines ctx (hdata hm) hm'), + exists st : sstate, sexec (cf ctx) ib = st /\ rst_refines ctx hrs st. +Proof. + wlp_simplify. + eapply hrexec_correct_aux; eauto. +Qed. +Local Hint Resolve hrexec_correct: wlp. + (** * Implementing the simulation test with concrete hash-consed symbolic execution *) Definition phys_check {A} (x y:A) (msg: pstring): ?? unit := @@ -1233,10 +1255,10 @@ Definition simu_check_single (f1 f2: function) (ib1 ib2: iblock): ?? unit := DO hC_sval <~ hCons hSVAL;; DO hC_list_hsval <~ hCons hLSVAL;; DO hC_hsmem <~ hCons hSMEM;; - let hsexec := hrexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in + let hrexec := hrexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in (* performing the hash-consed executions *) - DO hst1 <~ hsexec f1 ib1;; - DO hst2 <~ hsexec f2 ib2;; + DO hst1 <~ hrexec f1 ib1;; + DO hst2 <~ hrexec f2 ib2;; (* comparing the executions *) rst_simu_check hst1 hst2. @@ -1245,9 +1267,10 @@ Lemma simu_check_single_correct (f1 f2: function) (ib1 ib2: iblock): symbolic_simu f1 f2 ib1 ib2. Proof. (* TODO *) unfold symbolic_simu; wlp_simplify. + exploit hrexec_correct; eauto. eapply rst_simu_correct; eauto. + intros; eapply hrexec_correct1; eauto. - 1-3: wlp_simplify. unfold hrexec. + 1-3: wlp_simplify. intuition eauto. simpl. eauto. intuition eauto. admit. -- cgit