diff options
Diffstat (limited to 'kvx/lib')
| -rw-r--r-- | kvx/lib/RTLpathSE_impl.v | 320 | ||||
| -rw-r--r-- | kvx/lib/RTLpathSE_impl_junk.v | 1614 | ||||
| -rw-r--r-- | kvx/lib/RTLpathSE_theory.v | 39 | ||||
| -rw-r--r-- | kvx/lib/RTLpathScheduler.v | 5 | ||||
| -rw-r--r-- | kvx/lib/RTLpathSchedulerproof.v | 28 |
5 files changed, 760 insertions, 1246 deletions
diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v index 7be12f78..a2939cba 100644 --- a/kvx/lib/RTLpathSE_impl.v +++ b/kvx/lib/RTLpathSE_impl.v @@ -49,19 +49,6 @@ Proof. unfold hsi_sreg_eval, hsi_sreg_get; destruct (PTree.get r hst); simpl; auto. Qed. -(* negation of sabort_local *) -Definition sok_local (ge: RTL.genv) (sp:val) (rs0: regset) (m0: mem) (st: sistate_local): Prop := - (st.(si_pre) ge sp rs0 m0) - /\ seval_smem ge sp st.(si_smem) rs0 m0 <> None - /\ forall (r: reg), seval_sval ge sp (si_sreg st r) rs0 m0 <> None. - -Lemma ssem_local_sok ge sp rs0 m0 st rs m: - ssem_local ge sp st rs0 m0 rs m -> sok_local ge sp rs0 m0 st. -Proof. - unfold sok_local, ssem_local. - intuition congruence. -Qed. - Definition hsok_local ge sp rs0 m0 (hst: hsistate_local) : Prop := (forall sv, List.In sv (hsi_ok_lsval hst) -> seval_sval ge sp sv rs0 m0 <> None) /\ (seval_smem ge sp hst.(hsi_smem) rs0 m0 <> None). @@ -211,15 +198,14 @@ Definition hsiexit_simu_core dm f (hse1 hse2: hsistate_exit) := and a "dynamic" part -- that depends on it *) Definition hsiexit_refines_stat (hext: hsistate_exit) (ext: sistate_exit): Prop := - hsi_cond hext = si_cond ext - /\ hsi_ifso hext = si_ifso ext. + hsi_ifso hext = si_ifso ext. Definition hsok_exit ge sp rs m hse := hsok_local ge sp rs m (hsi_elocal hse). Definition hsiexit_refines_dyn ge sp rs0 m0 (hext: hsistate_exit) (ext: sistate_exit): Prop := hsilocal_refines ge sp rs0 m0 (hsi_elocal hext) (si_elocal ext) - /\ seval_condition ge sp (hsi_cond hext) (hsi_scondargs hext) (hsi_smem (hsi_elocal hext)) rs0 m0 - = seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs0 m0. + /\ (hsok_local ge sp rs0 m0 (hsi_elocal hext) -> seval_condition ge sp (hsi_cond hext) (hsi_scondargs hext) (hsi_smem (hsi_elocal hext)) rs0 m0 + = seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs0 m0). Definition hsiexit_simu dm f (ctx: simu_proof_context f) hse1 hse2: Prop := forall se1 se2, hsiexit_refines_stat hse1 se1 -> @@ -245,32 +231,35 @@ Theorem hsiexit_simu_core_correct dm f hse1 hse2 ctx: Proof. intros SIMUC st1 st2 HREF1 HREF2 HDYN1 HDYN2. assert (SEVALC: - seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond st1) (si_scondargs st1) (si_smem (si_elocal st1)) - (the_rs0 ctx) (the_m0 ctx) = - seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond st2) (si_scondargs st2) (si_smem (si_elocal st2)) - (the_rs0 ctx) (the_m0 ctx)). - { destruct HDYN1 as (_ & SCOND1). rewrite <- SCOND1 by assumption. clear SCOND1. - destruct HDYN2 as (_ & SCOND2). rewrite <- SCOND2 by assumption. clear SCOND2. + sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal st1) -> + (seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond st1) (si_scondargs st1) (si_smem (si_elocal st1)) + (the_rs0 ctx) (the_m0 ctx)) = + (seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond st2) (si_scondargs st2) (si_smem (si_elocal st2)) + (the_rs0 ctx) (the_m0 ctx))). + { destruct HDYN1 as ((OKEQ1 & _) & SCOND1). + rewrite OKEQ1; intro OK1. rewrite <- SCOND1 by assumption. clear SCOND1. + generalize (genv_match ctx). + intro GFS; exploit hsiexit_simu_core_nofail; eauto. + destruct HDYN2 as (_ & SCOND2). intro OK2. rewrite <- SCOND2 by assumption. clear OK1 OK2 SCOND2. destruct SIMUC as ((path & _ & LSIMU) & _ & CONDEQ & ARGSEQ). destruct LSIMU as (_ & _ & MEMEQ). rewrite CONDEQ. rewrite ARGSEQ. rewrite MEMEQ. erewrite <- seval_condition_preserved; eauto. - eapply ctx. } + } constructor; [assumption|]. intros is1 ICONT SSEME. + assert (OK1: sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal st1)). { + destruct SSEME as (_ & SSEML & _). eapply ssem_local_sok; eauto. } assert (HOK1: hsok_exit (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1). { - unfold hsok_exit. destruct SSEME as (_ & SSEML & _). apply ssem_local_sok in SSEML. - destruct HDYN1 as (LREF & _). destruct LREF as (OKEQ & _ & _). rewrite <- OKEQ. assumption. } + unfold hsok_exit. destruct HDYN1 as (LREF & _). destruct LREF as (OKEQ & _ & _). rewrite <- OKEQ. assumption. } exploit hsiexit_simu_core_nofail. 2: eapply ctx. all: eauto. intro HOK2. - destruct SSEME as (SCOND & SLOC & PCEQ). destruct SIMUC as ((path & PATH & LSIMU) & REVEQ & _ & _). + destruct SSEME as (SCOND & SLOC & PCEQ). destruct SIMUC as ((path & PATH & LSIMU) & REVEQ & _ & _); eauto. destruct HDYN1 as (LREF1 & _). destruct HDYN2 as (LREF2 & _). exploit hsilocal_simu_core_correct; eauto; [apply ctx|]. simpl. intros (SSEML & EQREG). eexists (mk_istate (icontinue is1) (si_ifso st2) _ (imem is1)). simpl. constructor. - - constructor; [|constructor]; [congruence | eassumption | reflexivity]. + - constructor; intuition congruence || eauto. - unfold istate_simu. rewrite ICONT. - simpl. assert (PCEQ': hsi_ifso hse1 = ipc is1). { destruct HREF1 as (_ & IFSO). congruence. } - exists path. constructor; [|constructor]. - + congruence. - + constructor; [|constructor]; simpl; auto. - + destruct HREF2 as (_ & IFSO). congruence. + simpl. assert (PCEQ': hsi_ifso hse1 = ipc is1) by congruence. + exists path. constructor; [|constructor]; [congruence| |congruence]. + constructor; [|constructor]; simpl; auto. Qed. Remark hsiexit_simu_siexit dm f ctx hse1 hse2 se1 se2: @@ -317,9 +306,17 @@ Definition hsistate_refines_stat (hst: hsistate) (st:sistate): Prop := hsi_pc hst = si_pc st /\ hsiexits_refines_stat (hsi_exits hst) (si_exits st). +Inductive nested_sok ge sp rs0 m0: sistate_local -> list sistate_exit -> Prop := + nsok_nil st: nested_sok ge sp rs0 m0 st nil + | nsok_cons st se lse: + (sok_local ge sp rs0 m0 st -> sok_local ge sp rs0 m0 (si_elocal se)) -> + nested_sok ge sp rs0 m0 (si_elocal se) lse -> + nested_sok ge sp rs0 m0 st (se::lse). + Definition hsistate_refines_dyn ge sp rs0 m0 (hst: hsistate) (st:sistate): Prop := hsiexits_refines_dyn ge sp rs0 m0 (hsi_exits hst) (si_exits st) - /\ hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st). + /\ hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st) + /\ nested_sok ge sp rs0 m0 (si_local st) (si_exits st). Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2, hsistate_refines_stat hst1 st1 -> @@ -331,14 +328,16 @@ Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f): Lemma siexits_simu_all_fallthrough dm f ctx: forall lse1 lse2, siexits_simu dm f lse1 lse2 ctx -> all_fallthrough (the_ge1 ctx) (the_sp ctx) lse1 (the_rs0 ctx) (the_m0 ctx) -> + (forall se1, In se1 lse1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) -> all_fallthrough (the_ge2 ctx) (the_sp ctx) lse2 (the_rs0 ctx) (the_m0 ctx). Proof. - induction 1; [unfold all_fallthrough; contradiction|]. - intros X ext INEXT. eapply all_fallthrough_revcons in X. destruct X as (SEVAL & ALLFU). + induction 1; [unfold all_fallthrough; contradiction|]; simpl. + intros X OK ext INEXT. eapply all_fallthrough_revcons in X. destruct X as (SEVAL & ALLFU). apply IHlist_forall2 in ALLFU. - destruct H as (CONDSIMU & _). - inv INEXT; [|eauto]. - erewrite <- CONDSIMU; eauto. + - destruct H as (CONDSIMU & _). + inv INEXT; [|eauto]. + erewrite <- CONDSIMU; eauto. + - intros; intuition. Qed. Lemma hsiexits_simu_siexits dm f ctx lhse1 lhse2: @@ -358,23 +357,27 @@ Proof. Qed. Lemma siexits_simu_all_fallthrough_upto dm f ctx lse1 lse2: - siexits_simu dm f lse1 lse2 ctx -> forall ext1 lx1, + siexits_simu dm f lse1 lse2 ctx -> + forall ext1 lx1, + (forall se1, In se1 lx1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) -> all_fallthrough_upto_exit (the_ge1 ctx) (the_sp ctx) ext1 lx1 lse1 (the_rs0 ctx) (the_m0 ctx) -> exists ext2 lx2, all_fallthrough_upto_exit (the_ge2 ctx) (the_sp ctx) ext2 lx2 lse2 (the_rs0 ctx) (the_m0 ctx) /\ length lx1 = length lx2. Proof. induction 1. - - intros. destruct H as (ITAIL & ALLFU). eapply is_tail_false in ITAIL. contradiction. - - intros ext1 lx1 ALLFUE. + - intros ext lx1. intros OK H. destruct H as (ITAIL & ALLFU). eapply is_tail_false in ITAIL. contradiction. + - simpl; intros ext lx1 OK ALLFUE. destruct ALLFUE as (ITAIL & ALLFU). inv ITAIL. + eexists; eexists. constructor; [| eapply list_forall2_length; eauto]. constructor; [econstructor | eapply siexits_simu_all_fallthrough; eauto]. - + exploit IHlist_forall2; [constructor; eauto|]. - intros (ext2 & lx2 & ALLFUE2 & LENEQ). - eexists; eexists. constructor; eauto. - eapply all_fallthrough_upto_exit_cons; eauto. + + exploit IHlist_forall2. + * intuition. apply OK. eassumption. + * constructor; eauto. + * intros (ext2 & lx2 & ALLFUE2 & LENEQ). + eexists; eexists. constructor; eauto. + eapply all_fallthrough_upto_exit_cons; eauto. Qed. Lemma list_forall2_nth_error {A} (l1 l2: list A) P: @@ -419,13 +422,41 @@ Proof. rewrite H0; auto. Qed. +Lemma nested_sok_prop ge sp st sle rs0 m0: + nested_sok ge sp rs0 m0 st sle -> + sok_local ge sp rs0 m0 st -> + forall se, In se sle -> sok_local ge sp rs0 m0 (si_elocal se). +Proof. + induction 1; simpl; intuition (subst; eauto). +Qed. + +Lemma nested_sok_elocal ge sp rs0 m0 st2 exits: + nested_sok ge sp rs0 m0 st2 exits -> + forall st1, (sok_local ge sp rs0 m0 st1 -> sok_local ge sp rs0 m0 st2) -> + nested_sok ge sp rs0 m0 st1 exits. +Proof. + induction 1. + - intros. constructor. + - intros. constructor; auto. +Qed. + +Lemma nested_sok_tail ge sp rs0 m0 st lx exits: + is_tail lx exits -> + nested_sok ge sp rs0 m0 st exits -> + nested_sok ge sp rs0 m0 st lx. +Proof. + induction 1. + - auto. + - intros. inv H0. eapply IHis_tail. eapply nested_sok_elocal; eauto. +Qed. + Theorem hsistate_simu_core_correct dm f hst1 hst2 ctx: hsistate_simu_core dm f hst1 hst2 -> hsistate_simu dm f hst1 hst2 ctx. Proof. intros SIMUC st1 st2 HREF1 HREF2 DREF1 DREF2 is1 SEMI. destruct HREF1 as (PCREF1 & EREF1). destruct HREF2 as (PCREF2 & EREF2). - destruct DREF1 as (DEREF1 & LREF1). destruct DREF2 as (DEREF2 & LREF2). + destruct DREF1 as (DEREF1 & LREF1 & NESTED). destruct DREF2 as (DEREF2 & LREF2 & _). destruct SIMUC as (PCSIMU & ESIMU & LSIMU). exploit hsiexits_simu_core_correct; eauto. intro HESIMU. unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT. @@ -433,27 +464,36 @@ Proof. exploit hsilocal_simu_core_correct; eauto; [apply ctx|]. simpl. intro SSEML2. exists (mk_istate (icontinue is1) (si_pc st2) (irs is1) (imem is1)). constructor. + unfold ssem_internal. simpl. rewrite ICONT. constructor; [assumption | constructor; [reflexivity |]]. - eapply siexits_simu_all_fallthrough; eauto. eapply hsiexits_simu_siexits; eauto. + eapply siexits_simu_all_fallthrough; eauto. + * eapply hsiexits_simu_siexits; eauto. + * eapply nested_sok_prop; eauto. + eapply ssem_local_sok; eauto. + unfold istate_simu. rewrite ICONT. constructor; [simpl; assumption | constructor; [| reflexivity]]. constructor. - destruct SEMI as (ext & lx & SSEME & ALLFU). assert (SESIMU: siexits_simu dm f (si_exits st1) (si_exits st2) ctx) by (eapply hsiexits_simu_siexits; eauto). - exploit siexits_simu_all_fallthrough_upto; eauto. intros (ext2 & lx2 & ALLFU2 & LENEQ). - assert (EXTSIMU: siexit_simu dm f ctx ext ext2). { - eapply list_forall2_nth_error; eauto. - - destruct ALLFU as (ITAIL & _). eapply is_tail_nth_error; eauto. - - destruct ALLFU2 as (ITAIL & _). eapply is_tail_nth_error in ITAIL. - assert (LENEQ': length (si_exits st1) = length (si_exits st2)) by (eapply list_forall2_length; eauto). - congruence. } - destruct EXTSIMU as (CONDEVAL & EXTSIMU). - apply EXTSIMU in SSEME; [|assumption]. clear EXTSIMU. destruct SSEME as (is2 & SSEME2 & ISIMU). - exists (mk_istate (icontinue is1) (ipc is2) (irs is2) (imem is2)). constructor. - + unfold ssem_internal. simpl. rewrite ICONT. exists ext2, lx2. constructor; assumption. - + unfold istate_simu in *. rewrite ICONT in *. destruct ISIMU as (path & PATHEQ & ISIMULIVE & DMEQ). - destruct ISIMULIVE as (CONTEQ & REGEQ & MEMEQ). - exists path. repeat (constructor; auto). + exploit siexits_simu_all_fallthrough_upto; eauto. + * destruct ALLFU as (ITAIL & ALLF). + exploit nested_sok_tail; eauto. intros NESTED2. + inv NESTED2. destruct SSEME as (_ & SSEML & _). eapply ssem_local_sok in SSEML. + eapply nested_sok_prop; eauto. + * intros (ext2 & lx2 & ALLFU2 & LENEQ). + assert (EXTSIMU: siexit_simu dm f ctx ext ext2). { + eapply list_forall2_nth_error; eauto. + - destruct ALLFU as (ITAIL & _). eapply is_tail_nth_error; eauto. + - destruct ALLFU2 as (ITAIL & _). eapply is_tail_nth_error in ITAIL. + assert (LENEQ': length (si_exits st1) = length (si_exits st2)) by (eapply list_forall2_length; eauto). + congruence. } + destruct EXTSIMU as (CONDEVAL & EXTSIMU). + apply EXTSIMU in SSEME; [|assumption]. clear EXTSIMU. destruct SSEME as (is2 & SSEME2 & ISIMU). + exists (mk_istate (icontinue is1) (ipc is2) (irs is2) (imem is2)). constructor. + + unfold ssem_internal. simpl. rewrite ICONT. exists ext2, lx2. constructor; assumption. + + unfold istate_simu in *. rewrite ICONT in *. destruct ISIMU as (path & PATHEQ & ISIMULIVE & DMEQ). + destruct ISIMULIVE as (CONTEQ & REGEQ & MEMEQ). + exists path. repeat (constructor; auto). Qed. + (* Definition hfinal_refines hfv fv := forall pge ge sp npc stk f rs0 m0 rs' m' t s', ssem_final pge ge sp npc stk f rs0 m0 hfv rs' m' t s' <-> ssem_final pge ge sp npc stk f rs0 m0 fv rs' m' t s'. *) @@ -503,28 +543,7 @@ Theorem hfinal_simu_core_correct dm f ctx opc1 opc2 hf1 hf2 f1 f2: dm ! opc2 = Some opc1 -> sfval_simu dm f opc1 opc2 ctx f1 f2. Proof. - intros CORE FREF1 FREF2 OPCEQ. - rewrite <- FREF1. rewrite <- FREF2. clear FREF1. clear FREF2. (* FIXME - to change when the refinement is more complex *) - destruct hf1. - (* Snone *) - - simpl in CORE. rewrite <- CORE. constructor. assumption. - (* Scall *) - - simpl in CORE. destruct hf2; try contradiction. destruct CORE as (PCEQ & ? & ? & ? & ?). subst. - constructor; [assumption | apply svident_simu_refl|]. - erewrite <- list_sval_eval_preserved; [| eapply ctx]. constructor. - (* Stailcall *) - - 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]. *) 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. -Admitted. +Admitted. (** Check out more complete proof in impl_junk *) Record hsstate := { hinternal:> hsistate; hfinal: sfval }. @@ -919,9 +938,12 @@ Qed. Lemma hsist_set_local_correct_dyn ge sp rs0 m0 hst st pc hnxt nxt: hsistate_refines_dyn ge sp rs0 m0 hst st -> hsilocal_refines ge sp rs0 m0 hnxt nxt -> + (sok_local ge sp rs0 m0 nxt -> sok_local ge sp rs0 m0 (si_local st)) -> hsistate_refines_dyn ge sp rs0 m0 (hsist_set_local hst pc hnxt) (sist_set_local st pc nxt). Proof. - unfold hsistate_refines_dyn; simpl; intuition. + unfold hsistate_refines_dyn; simpl. + intros (EREF & LREF & NESTED) LREFN SOK; intuition. + destruct NESTED as [|st0 se lse TOP NEST]; econstructor; simpl; auto. Qed. (** ** Assignment of registers *) @@ -955,6 +977,17 @@ Proof. unfold negb; explore; simpl; intuition (try congruence). Qed. +Lemma seval_list_sval_length ge sp rs0 m0 l: + forall l', seval_list_sval ge sp (list_sval_inj l) rs0 m0 = Some l' -> + Datatypes.length l = Datatypes.length l'. +Proof. + induction l. + - simpl. intros. inv H. reflexivity. + - simpl. intros. destruct (seval_sval _ _ _ _ _); [|discriminate]. + destruct (seval_list_sval _ _ _ _ _) eqn:SLS; [|discriminate]. inv H. simpl. + erewrite IHl; eauto. +Qed. + Lemma may_trap_correct (ge: RTL.genv) (sp:val) (rsv: root_sval) (rs0: regset) (m0: mem) (lsv: list sval) (sm: smem): may_trap rsv lsv sm = false -> seval_list_sval ge sp (list_sval_inj lsv) rs0 m0 <> None -> @@ -965,10 +998,12 @@ Proof. - rewrite lazy_orb_negb_false. intros (TRAP1 & TRAP2) OK1 OK2. explore; try congruence. eapply is_trapping_op_sound; eauto. - admit. (* TODO *) + erewrite <- seval_list_sval_length; eauto. + apply Nat.eqb_eq in TRAP2. + assumption. - intros X OK1 OK2. explore; try congruence. -Admitted. +Qed. (* simplify a symbolic value before assignment to a register *) Definition simplify (rsv: root_sval) lsv sm: sval := @@ -1150,7 +1185,7 @@ Proof. Qed. Lemma seval_condition_refines hst st ge sp cond args rs m: - hsok_local ge sp rs m hst -> + hsok_local ge sp rs m hst -> hsilocal_refines ge sp rs m hst st -> seval_condition ge sp cond args (hsi_smem hst) rs m = seval_condition ge sp cond args (si_smem st) rs m. @@ -1171,16 +1206,19 @@ Lemma hsiexec_inst_correct_stat i hst hst' st: exists st', siexec_inst i st = Some st' /\ (hsistate_refines_stat hst st -> hsistate_refines_stat hst' st'). Proof. - destruct i; simpl; intros STEPI; inversion_clear STEPI; discriminate || eexists; split; eauto. - (* TODO *) -Admitted. + destruct i; simpl; intros STEPI; inversion_clear STEPI; discriminate || eexists; split; eauto. + intros HREF. constructor; [simpl; reflexivity|]. simpl. + destruct HREF as (PCEQ & EXREF). + constructor; [|assumption]. clear EXREF. + constructor. +Qed. Lemma refines_okargs ge sp rs0 m0 hst st l: hsistate_refines_dyn ge sp rs0 m0 hst st -> ok_args ge sp rs0 m0 (hsi_local hst) (map (hsi_sreg_get (hsi_local hst)) l). Proof. unfold ok_args. - intros (_ & HLREF) OK. + intros (_ & HLREF & _) OK. erewrite seval_list_sval_refines; eauto. destruct HLREF as (OKEQ & _ & _). rewrite <- OKEQ in OK. @@ -1199,33 +1237,51 @@ Proof. inversion_clear STEP2; discriminate || (intro REF; eauto). - (* Iop *) eapply hsist_set_local_correct_dyn; eauto. - eapply hslocal_set_sreg_correct; eauto. - simpl; intros. - erewrite seval_list_sval_refines; eauto. - erewrite seval_smem_refines; eauto. + + eapply hslocal_set_sreg_correct; eauto. + simpl; intros. + erewrite seval_list_sval_refines; eauto. + erewrite seval_smem_refines; eauto. + + unfold sok_local; simpl; intros (PRE & MEM & REG). + intuition. + generalize (REG r0); clear REG. + destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto). - (* Iload *) eapply hsist_set_local_correct_dyn; eauto. - eapply hslocal_set_sreg_correct; eauto. - simpl; intros. - erewrite seval_list_sval_refines; eauto. - erewrite seval_smem_refines; eauto. - - (* Istore *) - eapply hsist_set_local_correct_dyn; eauto. - eapply hslocal_set_mem_correct; eauto. - + simpl. simplify_SOME x. - + simpl. intros m1; simplify_SOME x. - intros. - erewrite <- Mem.storev_preserv_valid; [| eauto]. - destruct REF as (_ & _ & _ & _ & MVALID). - eauto. - + intros. simpl. + + eapply hslocal_set_sreg_correct; eauto. + simpl; intros. erewrite seval_list_sval_refines; eauto. erewrite seval_smem_refines; eauto. - erewrite seval_sval_refines; eauto. + + unfold sok_local; simpl; intros (PRE & MEM & REG). + intuition. + generalize (REG r0); clear REG. + destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto). + - (* Istore *) + eapply hsist_set_local_correct_dyn; eauto. + + eapply hslocal_set_mem_correct; eauto. + * simpl. simplify_SOME x. + * simpl. intros m1; simplify_SOME x. + intros. + erewrite <- Mem.storev_preserv_valid; [| eauto]. + destruct REF as (_ & LREF & _). + destruct LREF as (_ & _ & _ & MVALID). + eauto. + * intros. simpl. + erewrite seval_list_sval_refines; eauto. + erewrite seval_smem_refines; eauto. + erewrite seval_sval_refines; eauto. + + unfold sok_local; simpl; intuition. - (* Icond *) - admit. (* TODO *) -Admitted. - + destruct REF as (EXREF & LREF & NEST). + split. + + constructor; simpl; auto. + constructor; simpl; auto. + intros; erewrite seval_condition_refines; eauto. + unfold seval_condition. + erewrite seval_list_sval_refines; eauto. + + split; simpl; auto. + destruct NEST as [|st0 se lse TOP NEST]; + econstructor; simpl; auto; constructor; auto. +Qed. Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): option hsistate := match path with @@ -1236,22 +1292,43 @@ Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): option hsistate hsiexec_path p f hst1 end. -Lemma hsiexec_path_correct_stat ps f hst hst' st: +Lemma hsiexec_path_correct_stat f ps: forall hst hst', hsiexec_path ps f hst = Some hst' -> - hsistate_refines_stat hst st -> + forall st, hsistate_refines_stat hst st -> exists st', siexec_path ps f st = Some st' /\ hsistate_refines_stat hst' st'. Proof. -Admitted. + induction ps. + - simpl. intros. inv H. repeat (econstructor; eauto). + - simpl. intros hst hst' EPATH st HREF. + destruct HREF as (PCREF & EXREF). rewrite <- PCREF. + destruct ((fn_code f) ! (hsi_pc hst)); [|discriminate]. + destruct (hsiexec_inst i hst) eqn:HSI; [|discriminate]. + eapply (hsiexec_inst_correct_stat _ _ _ st) in HSI. destruct HSI as (st' & SI' & HREF'). + lapply HREF'; [|constructor; assumption]. clear HREF'. intro HREF'. + eapply IHps in EPATH; eauto. destruct EPATH as (st'' & SIPATH & HREF''). + exists st''. constructor; [|assumption]. + rewrite SI'. assumption. +Qed. -Lemma hsiexec_path_correct_dyn ge sp rs0 m0 ps f hst hst' st st': +Lemma hsiexec_path_correct_dyn ge sp rs0 m0 f: forall ps hst hst', hsiexec_path ps f hst = Some hst' -> + forall st st', siexec_path ps f st = Some st' -> hsistate_refines_stat hst st -> hsistate_refines_stat hst' st' -> hsistate_refines_dyn ge sp rs0 m0 hst st -> hsistate_refines_dyn ge sp rs0 m0 hst' st'. Proof. -Admitted. + induction ps; [simpl; intros; congruence|]. + intros hst hst' HPATH st st' SPATH HSTAT HSTAT' HDYN. + simpl in *. destruct HSTAT as (PCREF & EXREF). rewrite <- PCREF in SPATH. + destruct ((fn_code f) ! (hsi_pc hst)); [|discriminate]. + destruct (hsiexec_inst i hst) eqn:HSI; [|discriminate]. + exploit hsiexec_inst_correct_stat; eauto. intros (s & SI & HREF). + lapply HREF; [|constructor; eassumption]. clear HREF. intro HREF. + rewrite SI in SPATH. + eapply hsiexec_inst_correct_dyn in HSI; eauto. +Qed. Definition hsexec_final (i: instruction) (prev: hsistate_local): sfval := @@ -1343,9 +1420,10 @@ Qed. Remark init_hsistate_correct_dyn ge sp rs0 m0 pc: hsistate_refines_dyn ge sp rs0 m0 (init_hsistate pc) (init_sistate pc). Proof. - constructor; simpl; auto. + constructor; [|constructor]; simpl; auto. - apply list_forall2_nil. - apply init_hsistate_local_correct. + - constructor. Qed. Definition hsexec (f: function) (pc:node): option hsstate := @@ -1655,7 +1733,7 @@ Proof. admit. (* Sreturn *) - destruct fv2; try discriminate. destruct o; destruct o0; try discriminate. - + intro. apply sval_simub_correct in H. subst. constructor; auto. + + intro. apply sval_simub_correct in H. subst. constructor; auto. admit. + constructor; auto. Admitted. diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index 342c9f30..2ea3e1ee 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -1,8 +1,4 @@ -(** Implementation and refinement of the symbolic execution - -* a JUNK VERSION WITHOUT ANY FORMAL PROOF !!! - - *) +(** Implementation and refinement of the symbolic execution *) Require Import Coqlib Maps Floats. Require Import AST Integers Values Events Memory Globalenvs Smallstep. @@ -24,27 +20,28 @@ Local Open Scope impure. Import ListNotations. Local Open Scope list_scope. -Ltac wlp_intros varname hname := apply wlp_unfold; intros varname hname. -Ltac wlp_step_bind varname hname := apply wlp_bind; wlp_intros varname hname. +Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := RET tt. (* TO REMOVE DEBUG INFO *) +(* Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := DO s <~ k x;; println ("DEBUG simu_check:" +; s). (* TO INSERT DEBUG INFO *) *) + +Definition DEBUG (s: pstring): ?? unit := XDEBUG tt (fun _ => RET s). (** * Implementation of Data-structure use in Hash-consing *) (** ** Implementation of symbolic values/symbolic memories with hash-consing data *) Inductive hsval := - | HSinput (r: reg) (hid:hashcode) - | HSop (op:operation) (hlsv: hlist_sval) (hsm: hsmem) (hid:hashcode) - | HSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval) (hid:hashcode) -with hlist_sval := - | HSnil (hid:hashcode) - | HScons (hsv: hsval) (hlsv: hlist_sval) (hid:hashcode) -(* symbolic memory *) + | HSinput (r: reg) (hid: hashcode) + | HSop (op: operation) (lhsv: list_hsval) (hsm: hsmem) (hid: hashcode) + | HSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (hid: hashcode) +with list_hsval := + | HSnil (hid: hashcode) + | HScons (hsv: hsval) (lhsv: list_hsval) (hid: hashcode) with hsmem := - | HSinit (hid:hashcode) - | HSstore (hsm: hsmem) (chunk:memory_chunk) (addr:addressing) (hlsv:hlist_sval) (srce: hsval) (hid:hashcode). + | HSinit (hid: hashcode) + | HSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval) (hid:hashcode). Scheme hsval_mut := Induction for hsval Sort Prop -with hlist_sval_mut := Induction for hlist_sval Sort Prop +with list_hsval_mut := Induction for list_hsval Sort Prop with hsmem_mut := Induction for hsmem Sort Prop. Definition hsval_get_hid (hsv: hsval): hashcode := @@ -54,13 +51,13 @@ Definition hsval_get_hid (hsv: hsval): hashcode := | HSload _ _ _ _ _ hid => hid end. -Definition hlist_sval_get_hid (hlsv: hlist_sval): hashcode := - match hlsv with +Definition list_hsval_get_hid (lhsv: list_hsval): hashcode := + match lhsv with | HSnil hid => hid | HScons _ _ hid => hid end. -Definition hsmem_get_hid (hsm: hsmem ): hashcode := +Definition hsmem_get_hid (hsm: hsmem): hashcode := match hsm with | HSinit hid => hid | HSstore _ _ _ _ _ hid => hid @@ -69,30 +66,30 @@ Definition hsmem_get_hid (hsm: hsmem ): hashcode := Definition hsval_set_hid (hsv: hsval) (hid: hashcode): hsval := match hsv with | HSinput r _ => HSinput r hid - | HSop o hlsv hsm _ => HSop o hlsv hsm hid - | HSload hsm trap chunk addr hlsv _ => HSload hsm trap chunk addr hlsv hid + | HSop o lhsv hsm _ => HSop o lhsv hsm hid + | HSload hsm trap chunk addr lhsv _ => HSload hsm trap chunk addr lhsv hid end. -Definition hlist_sval_set_hid (hlsv: hlist_sval) (hid: hashcode): hlist_sval := - match hlsv with +Definition list_hsval_set_hid (lhsv: list_hsval) (hid: hashcode): list_hsval := + match lhsv with | HSnil _ => HSnil hid - | HScons hsv hlsv _ => HScons hsv hlsv hid + | HScons hsv lhsv _ => HScons hsv lhsv hid end. -Definition hsmem_set_hid (hsm: hsmem ) (hid: hashcode): hsmem := +Definition hsmem_set_hid (hsm: hsmem) (hid: hashcode): hsmem := match hsm with | HSinit _ => HSinit hid - | HSstore hsm chunk addr hlsv srce _ => HSstore hsm chunk addr hlsv srce hid + | HSstore hsm chunk addr lhsv srce _ => HSstore hsm chunk addr lhsv srce hid end. -(* Now, we build the hash-Cons value from a "hash_eq". -Informal specification: - [hash_eq] must be consistent with the "hashed" constructors defined above. +(** Now, we build the hash-Cons value from a "hash_eq". -We expect that hashinfo values in the code of these "hashed" constructors verify: + Informal specification: + [hash_eq] must be consistent with the "hashed" constructors defined above. - (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y) + We expect that hashinfo values in the code of these "hashed" constructors verify: + (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y) *) Definition hsval_hash_eq (sv1 sv2: hsval): ?? bool := @@ -115,7 +112,7 @@ Definition hsval_hash_eq (sv1 sv2: hsval): ?? bool := | _,_ => RET false end. -Definition hlist_sval_hash_eq (lsv1 lsv2: hlist_sval): ?? bool := +Definition list_hsval_hash_eq (lsv1 lsv2: list_hsval): ?? bool := match lsv1, lsv2 with | HSnil _, HSnil _ => RET true | HScons sv1 lsv1' _, HScons sv2 lsv2' _ => @@ -141,29 +138,31 @@ Definition hsmem_hash_eq (sm1 sm2: hsmem): ?? bool := end. Definition hSVAL: hashP hsval := {| hash_eq := hsval_hash_eq; get_hid:=hsval_get_hid; set_hid:=hsval_set_hid |}. -Definition hLSVAL: hashP hlist_sval := {| hash_eq := hlist_sval_hash_eq; get_hid:= hlist_sval_get_hid; set_hid:= hlist_sval_set_hid |}. +Definition hLSVAL: hashP list_hsval := {| hash_eq := list_hsval_hash_eq; get_hid:= list_hsval_get_hid; set_hid:= list_hsval_set_hid |}. Definition hSMEM: hashP hsmem := {| hash_eq := hsmem_hash_eq; get_hid:= hsmem_get_hid; set_hid:= hsmem_set_hid |}. Program Definition mk_hash_params: Dict.hash_params hsval := {| Dict.test_eq := phys_eq; Dict.hashing := fun (ht: hsval) => RET (hsval_get_hid ht); - Dict.log := fun _ => RET () (* NB no log *) |}. + Dict.log := fun hv => + DO hv_name <~ string_of_hashcode (hsval_get_hid hv);; + println ("unexpected undef behavior of hashcode:" +; (CamlStr hv_name)) |}. Obligation 1. wlp_simplify. Qed. -(* Symbolic final value -- from hash-consed values -It does not seem useful to hash-consed these final values (because they are final). +(** Symbolic final value -- from hash-consed values + It does not seem useful to hash-consed these final values (because they are final). *) Inductive hsfval := | HSnone - | HScall (sig:signature) (svos: hsval + ident) (lsv:hlist_sval) (res:reg) (pc:node) - | HStailcall (sig:signature) (svos: hsval + ident) (lsv:hlist_sval) - | HSbuiltin (ef:external_function) (sargs: list (builtin_arg hsval)) (res: builtin_res reg) (pc:node) + | HScall (sig: signature) (svos: hsval + ident) (lsv: list_hsval) (res: reg) (pc: node) + | HStailcall (sig: signature) (svos: hsval + ident) (lsv: list_hsval) + | HSbuiltin (ef: external_function) (sargs: list (builtin_arg hsval)) (res: builtin_res reg) (pc: node) | HSjumptable (sv: hsval) (tbl: list node) - | HSreturn (res:option hsval) + | HSreturn (res: option hsval) . (** ** Implementation of symbolic states @@ -184,7 +183,7 @@ Record hsistate_local := (* Syntax and semantics of symbolic exit states *) Record hsistate_exit := mk_hsistate_exit - { hsi_cond: condition; hsi_scondargs: hlist_sval; hsi_elocal: hsistate_local; hsi_ifso: node }. + { hsi_cond: condition; hsi_scondargs: list_hsval; hsi_elocal: hsistate_local; hsi_ifso: node }. (** ** Syntax and Semantics of symbolic internal state *) @@ -193,6 +192,8 @@ Record hsistate := { hsi_pc: node; hsi_exits: list hsistate_exit; hsi_local: hsi (** ** Syntax and Semantics of symbolic state *) Record hsstate := { hinternal:> hsistate; hfinal: hsfval }. +(** ** Refinement Definitions: from refinement of symbolic values, memories, local/exit/internal/symbolic. *) + Fixpoint hsval_proj hsv := match hsv with | HSinput r _ => Sinput r @@ -210,27 +211,163 @@ with hsmem_proj hm := | HSstore hm chk addr hl hv _ => Sstore (hsmem_proj hm) chk addr (hsval_list_proj hl) (hsval_proj hv) end. +(** We use a Notation instead a Definition, in order to get more automation "for free" *) +Local Notation "'seval_hsval' ge sp hsv" := (seval_sval ge sp (hsval_proj hsv)) + (only parsing, at level 0, ge at next level, sp at next level, hsv at next level). +Local Notation "'seval_list_hsval' ge sp lhv" := (seval_list_sval ge sp (hsval_list_proj lhv)) + (only parsing, at level 0, ge at next level, sp at next level, lhv at next level). +Local Notation "'seval_hsmem' ge sp hsm" := (seval_smem ge sp (hsmem_proj hsm)) + (only parsing, at level 0, ge at next level, sp at next level, hsm at next level). + +Lemma hseval_preserved ge ge' rs0 m0 sp hsv: + (forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s) -> + seval_hsval ge sp hsv rs0 m0 = seval_hsval ge' sp hsv rs0 m0. +Proof. + intros; eapply seval_preserved; eauto. +Qed. + +Lemma hsmem_eval_preserved ge ge' rs0 m0 sp hsm: + (forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s) -> + seval_hsmem ge sp hsm rs0 m0 = seval_hsmem ge' sp hsm rs0 m0. +Proof. + intros; eapply smem_eval_preserved; eauto. +Qed. + + +Local Notation "'sval_refines' ge sp rs0 m0 hv sv" := (seval_hsval ge sp hv rs0 m0 = seval_sval ge sp sv rs0 m0) + (only parsing, at level 0, ge at next level, sp at next level, rs0 at next level, m0 at next level, hv at next level, sv at next level). + +Local Notation "'list_sval_refines' ge sp rs0 m0 lhv lsv" := (seval_list_hsval ge sp lhv rs0 m0 = seval_list_sval ge sp lsv rs0 m0) + (only parsing, at level 0, ge at next level, sp at next level, rs0 at next level, m0 at next level, lhv at next level, lsv at next level). + +Local Notation "'smem_refines' ge sp rs0 m0 hm sm" := (seval_hsmem ge sp hm rs0 m0 = seval_smem ge sp sm rs0 m0) + (only parsing, at level 0, ge at next level, sp at next level, rs0 at next level, m0 at next level, hm at next level, sm at next level). + +Definition hsi_sreg_eval ge sp (hst: PTree.t hsval) r rs0 m0: option val := + match PTree.get r hst with + | None => Some (Regmap.get r rs0) + | Some hsv => seval_sval ge sp (hsval_proj hsv) rs0 m0 + end. + +Definition hsok_local ge sp rs0 m0 (hst: hsistate_local) : Prop := + (forall hsv, List.In hsv (hsi_ok_lsval hst) -> seval_hsval ge sp hsv rs0 m0 <> None) + /\ (seval_hsmem ge sp (hst.(hsi_smem)) rs0 m0 <> None). + +(* refinement link between a (st: sistate_local) and (hst: hsistate_local) *) +Definition hsilocal_refines ge sp rs0 m0 (hst: hsistate_local) (st: sistate_local) := + (sok_local ge sp rs0 m0 st <-> hsok_local ge sp rs0 m0 hst) + /\ (hsok_local ge sp rs0 m0 hst -> smem_refines ge sp rs0 m0 (hsi_smem hst) (st.(si_smem))) + /\ (hsok_local ge sp rs0 m0 hst -> forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0) + /\ (forall r sv, hst ! r = Some sv -> In sv (hsi_ok_lsval hst)). + +(* +Lemma ssem_local_sok ge sp rs0 m0 st rs m: + ssem_local ge sp st rs0 m0 rs m -> sok_local ge sp rs0 m0 st. +Proof. + unfold sok_local, ssem_local. + intuition congruence. +Qed. + +Lemma ssem_local_refines_hok ge sp rs0 m0 hst st rs m: + ssem_local ge sp st rs0 m0 rs m -> hsilocal_refines ge sp rs0 m0 hst st -> hsok_local ge sp rs0 m0 hst. +Proof. + intros H0 (H1 & _ & _). apply H1. eapply ssem_local_sok. eauto. +Qed. +*) + +(** NB: we split the refinement relation between a "static" part -- independendent of the initial context + and a "dynamic" part -- that depends on it +*) +Definition hsiexit_refines_stat (hext: hsistate_exit) (ext: sistate_exit): Prop := + hsi_ifso hext = si_ifso ext. + +Definition hsok_exit ge sp rs m hse := hsok_local ge sp rs m (hsi_elocal hse). + +Definition hseval_condition ge sp cond hcondargs hmem rs0 m0 := + seval_condition ge sp cond (hsval_list_proj hcondargs) (hsmem_proj hmem) rs0 m0. + +Lemma hseval_condition_preserved ge ge' sp cond args mem rs0 m0: + (forall s : ident, Genv.find_symbol ge' s = Genv.find_symbol ge s) -> + hseval_condition ge sp cond args mem rs0 m0 = hseval_condition ge' sp cond args mem rs0 m0. +Proof. + intros. unfold hseval_condition. erewrite seval_condition_preserved; [|eapply H]. + reflexivity. +Qed. + +Definition hsiexit_refines_dyn ge sp rs0 m0 (hext: hsistate_exit) (ext: sistate_exit): Prop := + hsilocal_refines ge sp rs0 m0 (hsi_elocal hext) (si_elocal ext) + /\ (hsok_local ge sp rs0 m0 (hsi_elocal hext) -> + hseval_condition ge sp (hsi_cond hext) (hsi_scondargs hext) (hsi_smem (hsi_elocal hext)) rs0 m0 + = seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs0 m0). + +Definition hsiexits_refines_stat lhse lse := + list_forall2 hsiexit_refines_stat lhse lse. + +Definition hsiexits_refines_dyn ge sp rs0 m0 lhse se := + list_forall2 (hsiexit_refines_dyn ge sp rs0 m0) lhse se. + + +Inductive nested_sok ge sp rs0 m0: sistate_local -> list sistate_exit -> Prop := + nsok_nil st: nested_sok ge sp rs0 m0 st nil + | nsok_cons st se lse: + (sok_local ge sp rs0 m0 st -> sok_local ge sp rs0 m0 (si_elocal se)) -> + nested_sok ge sp rs0 m0 (si_elocal se) lse -> + nested_sok ge sp rs0 m0 st (se::lse). + +Lemma nested_sok_prop ge sp st sle rs0 m0: + nested_sok ge sp rs0 m0 st sle -> + sok_local ge sp rs0 m0 st -> + forall se, In se sle -> sok_local ge sp rs0 m0 (si_elocal se). +Proof. + induction 1; simpl; intuition (subst; eauto). +Qed. + +Lemma nested_sok_elocal ge sp rs0 m0 st2 exits: + nested_sok ge sp rs0 m0 st2 exits -> + forall st1, (sok_local ge sp rs0 m0 st1 -> sok_local ge sp rs0 m0 st2) -> + nested_sok ge sp rs0 m0 st1 exits. +Proof. + induction 1; [intros; constructor|]. + intros. constructor; auto. +Qed. + +Lemma nested_sok_tail ge sp rs0 m0 st lx exits: + is_tail lx exits -> + nested_sok ge sp rs0 m0 st exits -> + nested_sok ge sp rs0 m0 st lx. +Proof. + induction 1; [auto|]. + intros. inv H0. eapply IHis_tail. eapply nested_sok_elocal; eauto. +Qed. + +Definition hsistate_refines_stat (hst: hsistate) (st:sistate): Prop := + hsi_pc hst = si_pc st + /\ hsiexits_refines_stat (hsi_exits hst) (si_exits st). + +Definition hsistate_refines_dyn ge sp rs0 m0 (hst: hsistate) (st:sistate): Prop := + hsiexits_refines_dyn ge sp rs0 m0 (hsi_exits hst) (si_exits st) + /\ hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st) + /\ nested_sok ge sp rs0 m0 (si_local st) (si_exits st). + + (** * Implementation of symbolic execution *) Section CanonBuilding. Variable hC_hsval: hashinfo hsval -> ?? hsval. -(** FIXME - maybe it's not what we want ? *) -Hypothesis hC_hsval_correct: forall hs rhsv, - hC_hsval hs ~~> rhsv -> - (hsval_proj (hdata hs)) = (hsval_proj rhsv). +Hypothesis hC_hsval_correct: forall hs, + WHEN hC_hsval hs ~> hs' THEN forall ge sp rs0 m0, + seval_hsval ge sp (hdata hs) rs0 m0 = seval_hsval ge sp hs' rs0 m0. -Variable hC_hlist_sval: hashinfo hlist_sval -> ?? hlist_sval. - -Hypothesis hC_hlist_sval_correct: forall hs rhsv, - hC_hlist_sval hs ~~> rhsv -> - (hsval_list_proj (hdata hs)) = (hsval_list_proj rhsv). +Variable hC_list_hsval: hashinfo list_hsval -> ?? list_hsval. +Hypothesis hC_list_hsval_correct: forall lh, + WHEN hC_list_hsval lh ~> lh' THEN forall ge sp rs0 m0, + seval_list_hsval ge sp (hdata lh) rs0 m0 = seval_list_hsval ge sp lh' rs0 m0. Variable hC_hsmem: hashinfo hsmem -> ?? hsmem. - -Hypothesis hC_hsmem_correct: forall hs rhsv, - hC_hsmem hs ~~> rhsv -> - (hsmem_proj (hdata hs)) = (hsmem_proj rhsv). +Hypothesis hC_hsmem_correct: forall hm, + WHEN hC_hsmem hm ~> hm' THEN forall ge sp rs0 m0, + seval_hsmem ge sp (hdata hm) rs0 m0 = seval_hsmem ge sp hm' rs0 m0. (* First, we wrap constructors for hashed values !*) @@ -248,50 +385,126 @@ Definition hSinput (r:reg): ?? hsval := DO hv <~ hSinput_hcodes r;; hC_hsval {| hdata:=HSinput r unknown_hid; hcodes :=hv; |}. +Lemma hSinput_correct r: + WHEN hSinput r ~> hv THEN forall ge sp rs0 m0, + sval_refines ge sp rs0 m0 hv (Sinput r). +Proof. + wlp_simplify. +Qed. +Global Opaque hSinput. +Local Hint Resolve hSinput_correct: wlp. -Definition hSop_hcodes (op:operation) (hlsv: hlist_sval) (hsm: hsmem) := +Definition hSop_hcodes (op:operation) (lhsv: list_hsval) (hsm: hsmem) := DO hc <~ hash op_hcode;; DO hv <~ hash op;; - RET [hc;hv;hlist_sval_get_hid hlsv; hsmem_get_hid hsm]. + RET [hc;hv;list_hsval_get_hid lhsv; hsmem_get_hid hsm]. Extraction Inline hSop_hcodes. -Definition hSop (op:operation) (hlsv: hlist_sval) (hsm: hsmem): ?? hsval := - DO hv <~ hSop_hcodes op hlsv hsm;; - hC_hsval {| hdata:=HSop op hlsv hsm unknown_hid; hcodes :=hv |}. +Definition hSop (op:operation) (lhsv: list_hsval) (hsm: hsmem): ?? hsval := + DO hv <~ hSop_hcodes op lhsv hsm;; + hC_hsval {| hdata:=HSop op lhsv hsm unknown_hid; hcodes :=hv |}. +Lemma hSop_correct op lhsv hsm: + WHEN hSop op lhsv hsm ~> hv THEN forall ge sp rs0 m0 lsv sm, + list_sval_refines ge sp rs0 m0 lhsv lsv -> + smem_refines ge sp rs0 m0 hsm sm -> + sval_refines ge sp rs0 m0 hv (Sop op lsv sm). +Proof. + wlp_simplify. + rewrite <- H0, <- H1. + auto. +Qed. +Global Opaque hSop. +Local Hint Resolve hSop_correct: wlp. -Definition hSload_hcodes (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval):= +Definition hSload_hcodes (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval):= DO hc <~ hash load_hcode;; DO hv1 <~ hash trap;; DO hv2 <~ hash chunk;; DO hv3 <~ hash addr;; - RET [hc;hsmem_get_hid hsm;hv1;hv2;hv3;hlist_sval_get_hid hlsv]. + RET [hc; hsmem_get_hid hsm; hv1; hv2; hv3; list_hsval_get_hid lhsv]. Extraction Inline hSload_hcodes. -Definition hSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval): ?? hsval := - DO hv <~ hSload_hcodes hsm trap chunk addr hlsv;; - hC_hsval {| hdata:=HSload hsm trap chunk addr hlsv unknown_hid; hcodes :=hv |}. +Definition hSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval): ?? hsval := + DO hv <~ hSload_hcodes hsm trap chunk addr lhsv;; + hC_hsval {| hdata := HSload hsm trap chunk addr lhsv unknown_hid; hcodes := hv |}. +Lemma hSload_correct hsm trap chunk addr lhsv: + WHEN hSload hsm trap chunk addr lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm, + list_sval_refines ge sp rs0 m0 lhsv lsv -> + smem_refines ge sp rs0 m0 hsm sm -> + sval_refines ge sp rs0 m0 hv (Sload sm trap chunk addr lsv). +Proof. + wlp_simplify. + rewrite <- H0, <- H1. + auto. +Qed. +Global Opaque hSload. +Local Hint Resolve hSload_correct: wlp. + +Definition hSnil (_: unit): ?? list_hsval := + hC_list_hsval {| hdata := HSnil unknown_hid; hcodes := nil |}. + +Lemma hSnil_correct x: + WHEN hSnil x ~> hv THEN forall ge sp rs0 m0, + list_sval_refines ge sp rs0 m0 hv Snil. +Proof. + wlp_simplify. +Qed. +Global Opaque hSnil. +Local Hint Resolve hSnil_correct: wlp. -Definition hSnil (_: unit): ?? hlist_sval := - hC_hlist_sval {| hdata:=HSnil unknown_hid; hcodes := nil |}. +Definition hScons (hsv: hsval) (lhsv: list_hsval): ?? list_hsval := + hC_list_hsval {| hdata := HScons hsv lhsv unknown_hid; hcodes := [hsval_get_hid hsv; list_hsval_get_hid lhsv] |}. -Definition hScons (hsv: hsval) (hlsv: hlist_sval): ?? hlist_sval := - hC_hlist_sval {| hdata:=HScons hsv hlsv unknown_hid; hcodes := [hsval_get_hid hsv; hlist_sval_get_hid hlsv] |}. +Lemma hScons_correct hsv lhsv: + WHEN hScons hsv lhsv ~> lhsv' THEN forall ge sp rs0 m0 sv lsv, + sval_refines ge sp rs0 m0 hsv sv -> + list_sval_refines ge sp rs0 m0 lhsv lsv -> + list_sval_refines ge sp rs0 m0 lhsv' (Scons sv lsv). +Proof. + wlp_simplify. + rewrite <- H0, <- H1. + auto. +Qed. +Global Opaque hScons. +Local Hint Resolve hScons_correct: wlp. Definition hSinit (_: unit): ?? hsmem := - hC_hsmem {| hdata:=HSinit unknown_hid; hcodes := nil |}. + hC_hsmem {| hdata := HSinit unknown_hid; hcodes := nil |}. -Definition hSstore_hcodes (hsm: hsmem) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval) (srce: hsval):= +Lemma hSinit_correct x: + WHEN hSinit x ~> hm THEN forall ge sp rs0 m0, + smem_refines ge sp rs0 m0 hm Sinit. +Proof. + wlp_simplify. +Qed. +Global Opaque hSinit. +Local Hint Resolve hSinit_correct: wlp. + +Definition hSstore_hcodes (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval):= DO hv1 <~ hash chunk;; DO hv2 <~ hash addr;; - RET [hsmem_get_hid hsm;hv1;hv2;hlist_sval_get_hid hlsv;hsval_get_hid srce]. + RET [hsmem_get_hid hsm; hv1; hv2; list_hsval_get_hid lhsv; hsval_get_hid srce]. Extraction Inline hSstore_hcodes. -Definition hSstore (hsm: hsmem) (chunk:memory_chunk) (addr:addressing) (hlsv:hlist_sval) (srce: hsval): ?? hsmem := - DO hv <~ hSstore_hcodes hsm chunk addr hlsv srce;; - hC_hsmem {| hdata:=HSstore hsm chunk addr hlsv srce unknown_hid; hcodes := hv |}. +Definition hSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval): ?? hsmem := + DO hv <~ hSstore_hcodes hsm chunk addr lhsv srce;; + hC_hsmem {| hdata := HSstore hsm chunk addr lhsv srce unknown_hid; hcodes := hv |}. +Lemma hSstore_correct hsm chunk addr lhsv hsv: + WHEN hSstore hsm chunk addr lhsv hsv ~> hsm' THEN forall ge sp rs0 m0 lsv sm sv, + list_sval_refines ge sp rs0 m0 lhsv lsv -> + smem_refines ge sp rs0 m0 hsm sm -> + sval_refines ge sp rs0 m0 hsv sv -> + smem_refines ge sp rs0 m0 hsm' (Sstore sm chunk addr lsv sv). +Proof. + wlp_simplify. + rewrite <- H0, <- H1, <- H2. + auto. +Qed. +Global Opaque hSstore. +Local Hint Resolve hSstore_correct: wlp. Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval := match PTree.get r hst with @@ -299,89 +512,198 @@ Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval := | Some sv => RET sv end. -Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? hlist_sval := +Lemma hsi_sreg_get_correct hst r: + WHEN hsi_sreg_get hst r ~> hsv THEN forall ge sp rs0 m0 (f: reg -> sval), + (forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0) -> + sval_refines ge sp rs0 m0 hsv (f r). +Proof. + unfold hsi_sreg_eval; wlp_simplify. + + rewrite <- H0, H. auto. + + rewrite <- H1, H. auto. +Qed. +Global Opaque hsi_sreg_get. +Local Hint Resolve hsi_sreg_get_correct: wlp. + +Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? list_hsval := match l with | nil => hSnil() | r::l => DO v <~ hsi_sreg_get hst r;; - DO hlsv <~ hlist_args hst l;; - hScons v hlsv + DO lhsv <~ hlist_args hst l;; + hScons v lhsv end. +Lemma hlist_args_correct hst l: + WHEN hlist_args hst l ~> lhsv THEN forall ge sp rs0 m0 (f: reg -> sval), + (forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0) -> + list_sval_refines ge sp rs0 m0 lhsv (list_sval_inj (List.map f l)). +Proof. + induction l; wlp_simplify. +Qed. +Global Opaque hlist_args. +Local Hint Resolve hlist_args_correct: wlp. + + (** ** Assignment of memory *) -Definition hslocal_store (hst:hsistate_local) chunk addr args src: ?? hsistate_local := +Definition hslocal_set_smem (hst:hsistate_local) hm := + {| hsi_smem := hm; + hsi_ok_lsval := hsi_ok_lsval hst; + hsi_sreg:= hsi_sreg hst + |}. + +Lemma sok_local_set_mem ge sp rs0 m0 st sm: + sok_local ge sp rs0 m0 (slocal_set_smem st sm) + <-> (sok_local ge sp rs0 m0 st /\ seval_smem ge sp sm rs0 m0 <> None). +Proof. + unfold slocal_set_smem, sok_local; simpl; intuition (subst; eauto). +Qed. + +Lemma hsok_local_set_mem ge sp rs0 m0 hst hsm: + (seval_hsmem ge sp (hsi_smem hst) rs0 m0 = None -> seval_hsmem ge sp hsm rs0 m0 = None) -> + hsok_local ge sp rs0 m0 (hslocal_set_smem hst hsm) + <-> (hsok_local ge sp rs0 m0 hst /\ seval_hsmem ge sp hsm rs0 m0 <> None). +Proof. + unfold hslocal_set_smem, hsok_local; simpl; intuition. +Qed. + +Lemma hslocal_set_mem_correct ge sp rs0 m0 hst st hsm sm: + (seval_hsmem ge sp (hsi_smem hst) rs0 m0 = None -> seval_hsmem ge sp hsm rs0 m0 = None) -> + hsilocal_refines ge sp rs0 m0 hst st -> + (hsok_local ge sp rs0 m0 hst -> smem_refines ge sp rs0 m0 hsm sm) -> + hsilocal_refines ge sp rs0 m0 (hslocal_set_smem hst hsm) (slocal_set_smem st sm). +Proof. + intros PRESERV (OKEQ & SMEMEQ' & REGEQ) SMEMEQ. + split; rewrite! hsok_local_set_mem; eauto; try tauto. + rewrite sok_local_set_mem. + intuition congruence. +Qed. +Local Hint Resolve hslocal_set_mem_correct: wlp. + +Definition hslocal_store (hst: hsistate_local) chunk addr args src: ?? hsistate_local := let pt := hst.(hsi_sreg) in DO hargs <~ hlist_args pt args;; DO hsrc <~ hsi_sreg_get pt src;; DO hm <~ hSstore hst chunk addr hargs hsrc;; - RET {| hsi_smem := hm; - hsi_ok_lsval := hsi_ok_lsval hst; - hsi_sreg:= hsi_sreg hst - |}. + RET (hslocal_set_smem hst hm). + +Lemma hslocal_store_correct hst chunk addr args src: + WHEN hslocal_store hst chunk addr args src ~> hst' THEN forall ge sp rs0 m0 st, + hsilocal_refines ge sp rs0 m0 hst st -> + hsilocal_refines ge sp rs0 m0 hst' (slocal_store st chunk addr args src). +Proof. + wlp_simplify. + eapply hslocal_set_mem_correct; simpl; eauto. + + intros X; erewrite H1; eauto. + rewrite X. simplify_SOME z. + + unfold hsilocal_refines in * |-; intuition eauto. +Qed. +Global Opaque hslocal_store. +Local Hint Resolve hslocal_store_correct: wlp. (** ** Assignment of local state *) Definition hsist_set_local (hst: hsistate) (pc: node) (hnxt: hsistate_local): hsistate := {| hsi_pc := pc; hsi_exits := hst.(hsi_exits); hsi_local:= hnxt |}. +Lemma hsist_set_local_correct_stat hst st pc hnxt nxt: + hsistate_refines_stat hst st -> + hsistate_refines_stat (hsist_set_local hst pc hnxt) (sist_set_local st pc nxt). +Proof. + unfold hsistate_refines_stat; simpl; intuition. +Qed. + +Lemma hsist_set_local_correct_dyn ge sp rs0 m0 hst st pc hnxt nxt: + hsistate_refines_dyn ge sp rs0 m0 hst st -> + hsilocal_refines ge sp rs0 m0 hnxt nxt -> + (sok_local ge sp rs0 m0 nxt -> sok_local ge sp rs0 m0 (si_local st)) -> + hsistate_refines_dyn ge sp rs0 m0 (hsist_set_local hst pc hnxt) (sist_set_local st pc nxt). +Proof. + unfold hsistate_refines_dyn; simpl. + intros (EREF & LREF & NESTED) LREFN SOK; intuition. + destruct NESTED as [|st0 se lse TOP NEST]; econstructor; simpl; auto. +Qed. + (** ** Assignment of registers *) -(* locally new symbolic values during symbolic execution *) +(** locally new symbolic values during symbolic execution *) Inductive root_sval: Type := -| Rop (op:operation) -| Rload (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) +| Rop (op: operation) +| Rload (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) . -Definition root_apply (rsv: root_sval) (lsv: list reg) (hst: hsistate_local) : ?? hsval := - DO hlsv <~ hlist_args hst lsv;; +Definition hSop_hSinit (op:operation) (lhsv: list_hsval): ?? hsval := + DO hsi <~ hSinit ();; + hSop op lhsv hsi (** magically remove the dependency on sm ! *) + . + +Definition root_apply (rsv: root_sval) (lr: list reg) (hst: hsistate_local) : ?? hsval := + DO lhsv <~ hlist_args hst lr;; match rsv with - | Rop op => hSop op hlsv hst - | Rload trap chunk addr => hSload hst trap chunk addr hlsv + | Rop op => hSop_hSinit op lhsv + | Rload trap chunk addr => hSload hst trap chunk addr lhsv end. Local Open Scope lazy_bool_scope. (* NB: return [false] if the rsv cannot fail *) -Definition may_trap (rsv: root_sval) (lsv: list reg): bool := +Definition may_trap (rsv: root_sval) (lr: list reg): bool := match rsv with - | Rop op => is_trapping_op op ||| negb (Nat.eqb (length lsv) (args_of_operation op)) (* cf. lemma is_trapping_op_sound *) + | Rop op => is_trapping_op op ||| negb (Nat.eqb (length lr) (args_of_operation op)) (* cf. lemma is_trapping_op_sound *) | Rload TRAP _ _ => true | _ => false end. -(* simplify a symbolic value before assignment to a register *) -Definition simplify (rsv: root_sval) (lsv: list reg) (hst: hsistate_local): ?? hsval := +Lemma lazy_orb_negb_false (b1 b2:bool): + (b1 ||| negb b2) = false <-> (b1 = false /\ b2 = true). +Proof. + unfold negb; explore; simpl; intuition (try congruence). +Qed. + +Lemma seval_list_sval_length ge sp rs0 m0 l: + forall l', seval_list_sval ge sp (list_sval_inj l) rs0 m0 = Some l' -> + Datatypes.length l = Datatypes.length l'. +Proof. + induction l. + - simpl. intros. inv H. reflexivity. + - simpl. intros. destruct (seval_sval _ _ _ _ _); [|discriminate]. + destruct (seval_list_sval _ _ _ _ _) eqn:SLS; [|discriminate]. inv H. simpl. + erewrite IHl; eauto. +Qed. + +(** simplify a symbolic value before assignment to a register *) +Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval := match rsv with | Rop op => - match is_move_operation op lsv with - | Some arg => hsi_sreg_get hst arg (* optimization of Omove *) + match is_move_operation op lr with + | Some arg => hsi_sreg_get hst arg (** optimization of Omove *) | None => - DO hsi <~ hSinit ();; - DO hlsv <~ hlist_args hst lsv;; - hSop op hlsv hsi (* magically remove the dependency on sm ! *) + DO lhsv <~ hlist_args hst lr;; + hSop_hSinit op lhsv end | Rload _ chunk addr => - DO hlsv <~ hlist_args hst lsv;; - hSload hst NOTRAP chunk addr hlsv + DO lhsv <~ hlist_args hst lr;; + hSload hst NOTRAP chunk addr lhsv end. -Definition red_PTree_set (r:reg) (sv: hsval) (hst: PTree.t hsval): PTree.t hsval := - match sv with +Definition red_PTree_set (r: reg) (hsv: hsval) (hst: PTree.t hsval): PTree.t hsval := + match hsv with | HSinput r' _ => if Pos.eq_dec r r' then PTree.remove r' hst - else PTree.set r sv hst - | _ => PTree.set r sv hst + else PTree.set r hsv hst + | _ => PTree.set r hsv hst end. -Definition hslocal_set_sreg (hst:hsistate_local) (r:reg) (rsv:root_sval) lsv: ?? hsistate_local := - DO hsiok <~ - (if may_trap rsv lsv - then DO hv <~ root_apply rsv lsv hst;; RET (hv::(hsi_ok_lsval hst)) +Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) (lr: list reg): ?? hsistate_local := + DO ok_lhsv <~ + (if may_trap rsv lr + then DO hv <~ root_apply rsv lr hst;; + XDEBUG hv (fun hv => DO hv_name <~ string_of_hashcode (hsval_get_hid hv);; RET ("-- insert undef behavior of hashcode:" +; (CamlStr hv_name))%string);; + RET (hv::(hsi_ok_lsval hst)) else RET (hsi_ok_lsval hst));; - DO simp <~ simplify rsv lsv hst;; + DO simp <~ simplify rsv lr hst;; RET {| hsi_smem := hst; - hsi_ok_lsval := hsiok; + hsi_ok_lsval := ok_lhsv; hsi_sreg := red_PTree_set r simp (hsi_sreg hst) |}. (** ** Execution of one instruction *) @@ -417,7 +739,9 @@ Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): ?? hsistate := match path with | O => RET hst | S p => - DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsiexec_path.internal_error.1";; + let pc := hst.(hsi_pc) in + XDEBUG pc (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("- sym exec node: " +; name_pc)%string);; + DO i <~ some_or_fail ((fn_code f)!pc) "hsiexec_path.internal_error.1";; DO ohst1 <~ hsiexec_inst i hst;; DO hst1 <~ some_or_fail ohst1 "hsiexec_path.internal_error.2";; hsiexec_path p f hst1 @@ -461,7 +785,51 @@ Definition hsum_left (hst: PTree.t hsval) (ros: reg + ident): ?? (hsval + ident) | inr s => RET (inr s) end. +Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval := + match i with + | Icall sig ros args res pc => + DO svos <~ hsum_left hst ros;; + DO sargs <~ hlist_args hst args;; + RET (HScall sig svos sargs res pc) + | Itailcall sig ros args => + DO svos <~ hsum_left hst ros;; + DO sargs <~ hlist_args hst args;; + RET (HStailcall sig svos sargs) + | Ibuiltin ef args res pc => + DO sargs <~ hbuiltin_args hst args;; + RET (HSbuiltin ef sargs res pc) + | Ijumptable reg tbl => + DO sv <~ hsi_sreg_get hst reg;; + RET (HSjumptable sv tbl) + | Ireturn or => + match or with + | Some r => DO hr <~ hsi_sreg_get hst r;; RET (HSreturn (Some hr)) + | None => RET (HSreturn None) + end + | _ => RET (HSnone) + end. + +Definition init_hsistate_local (_:unit): ?? hsistate_local + := DO hm <~ hSinit ();; + RET {| hsi_smem := hm; hsi_ok_lsval := nil; hsi_sreg := PTree.empty hsval |}. +Definition init_hsistate pc: ?? hsistate + := DO hst <~ init_hsistate_local ();; + RET {| hsi_pc := pc; hsi_exits := nil; hsi_local := hst |}. + +Definition hsexec (f: function) (pc:node): ?? hsstate := + DO path <~ some_or_fail ((fn_path f)!pc) "hsexec.internal_error.1";; + DO hinit <~ init_hsistate pc;; + DO hst <~ hsiexec_path path.(psize) f hinit;; + DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsexec.internal_error.2";; + DO ohst <~ hsiexec_inst i hst;; + match ohst with + | Some hst' => RET {| hinternal := hst'; hfinal := HSnone |} + | None => DO hsvf <~ hsexec_final i hst.(hsi_local);; + RET {| hinternal := hst; hfinal := hsvf |} + end. + +End CanonBuilding. (** * The simulation test of concrete hash-consed symbolic execution *) @@ -470,11 +838,18 @@ Definition phys_check {A} (x y:A) (msg: pstring): ?? unit := assert_b b msg;; RET tt. -Definition struct_check {A} (x y:A) (msg: pstring): ?? unit := +Definition struct_check {A} (x y: A) (msg: pstring): ?? unit := DO b <~ struct_eq x y;; assert_b b msg;; RET tt. +Lemma struct_check_correct {A} (a b: A) msg: + WHEN struct_check a b msg ~> tt THEN + a = b. +Proof. wlp_simplify. Qed. +Global Opaque struct_check. +Hint Resolve struct_check_correct: wlp. + Definition option_eq_check {A} (o1 o2: option A): ?? unit := match o1, o2 with | Some x1, Some x2 => phys_check x1 x2 "option_eq_check: data physically differ" @@ -487,7 +862,7 @@ Proof. wlp_simplify. Qed. Global Opaque option_eq_check. -(* Global *) Hint Resolve option_eq_check_correct:wlp. +Hint Resolve option_eq_check_correct:wlp. Import PTree. @@ -525,374 +900,23 @@ Proof. Qed. Global Opaque PTree_frame_eq_check. -(** hsilocal_simu_check and properties *) - -(* negation of sabort_local *) -Definition sok_local (ge: RTL.genv) (sp:val) (rs0: regset) (m0: mem) (st: sistate_local): Prop := - (st.(si_pre) ge sp rs0 m0) - /\ seval_smem ge sp st.(si_smem) rs0 m0 <> None - /\ forall (r: reg), seval_sval ge sp (si_sreg st r) rs0 m0 <> None. - -Lemma ssem_local_sok ge sp rs0 m0 st rs m: - ssem_local ge sp st rs0 m0 rs m -> sok_local ge sp rs0 m0 st. -Proof. - unfold sok_local, ssem_local. - intuition congruence. -Qed. - -Definition seval_hsval ge sp hsv rs0 m0 := seval_sval ge sp (hsval_proj hsv) rs0 m0. -Definition seval_hsmem ge sp hsm rs0 m0 := seval_smem ge sp (hsmem_proj hsm) rs0 m0. - -Definition hsi_sreg_eval ge sp (hst: PTree.t hsval) r rs0 m0: option val := - match PTree.get r hst with - | None => Some (Regmap.get r rs0) - | Some hsv => seval_hsval ge sp hsv rs0 m0 - end. - -Lemma hsi_sreg_eval_correct ge sp hst r rs0 m0: - WHEN hsi_sreg_get hst r ~> hv THEN - hsi_sreg_eval ge sp hst r rs0 m0 = seval_hsval ge sp hv rs0 m0. -Proof. - wlp_simplify. - - unfold hsi_sreg_eval. rewrite H. reflexivity. - - unfold hsi_sreg_eval. rewrite H. eapply hC_hsval_correct in Hexta1. - simpl in Hexta1. unfold seval_hsval. rewrite <- Hexta1. simpl. reflexivity. -Qed. -Hint Resolve hsi_sreg_eval_correct: wlp. - -Definition hsok_local ge sp rs0 m0 (hst: hsistate_local) : Prop := - (forall hsv, List.In hsv (hsi_ok_lsval hst) -> seval_hsval ge sp hsv rs0 m0 <> None). - -(* refinement link between a (st: sistate_local) and (hst: hsistate_local) *) -Definition hsilocal_refines ge sp rs0 m0 (hst: hsistate_local) (st: sistate_local) := - (sok_local ge sp rs0 m0 st <-> hsok_local ge sp rs0 m0 hst) - /\ (hsok_local ge sp rs0 m0 hst -> seval_hsmem ge sp (hsi_smem hst) rs0 m0 = seval_smem ge sp st.(si_smem) rs0 m0) - /\ (hsok_local ge sp rs0 m0 hst -> forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0) - /\ (forall r sv, hst ! r = Some sv -> In sv (hsi_ok_lsval hst)). - -Lemma ssem_local_refines_hok ge sp rs0 m0 hst st rs m: - ssem_local ge sp st rs0 m0 rs m -> hsilocal_refines ge sp rs0 m0 hst st -> hsok_local ge sp rs0 m0 hst. -Proof. - intros H0 (H1 & _ & _). apply H1. eapply ssem_local_sok. eauto. -Qed. - -Definition hsilocal_simu_core (oalive: option Regset.t) (hst1 hst2: hsistate_local) := - 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 *) - PTree.get r hst2 = PTree.get r hst1) - /\ hsi_smem hst1 = hsi_smem hst2. - -Lemma hseval_preserved ge ge' rs0 m0 sp hsv: - (forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s) -> - seval_hsval ge sp hsv rs0 m0 = seval_hsval ge' sp hsv rs0 m0. -Proof. - intros. unfold seval_hsval. erewrite seval_preserved; eauto. -Qed. - -Lemma hsmem_eval_preserved ge ge' rs0 m0 sp hsm: - (forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s) -> - seval_hsmem ge sp hsm rs0 m0 = seval_hsmem ge' sp hsm rs0 m0. -Proof. - intros. unfold seval_hsmem. erewrite smem_eval_preserved; eauto. -Qed. - -Lemma hsilocal_simu_core_nofail ge1 ge2 of sp rs0 m0 hst1 hst2: - hsilocal_simu_core of hst1 hst2 -> - (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) -> - hsok_local ge1 sp rs0 m0 hst1 -> - hsok_local ge2 sp rs0 m0 hst2. -Proof. - intros (RSOK & _ & _) GFS OKV. - intros sv INS. apply RSOK in INS. apply OKV in INS. erewrite hseval_preserved; eauto. -Qed. - -Remark istate_simulive_reflexive dm is: istate_simulive (fun _ : Regset.elt => True) dm is is. -Proof. - unfold istate_simulive. - repeat (constructor; auto). -Qed. - -Definition seval_sval_partial ge sp rs0 m0 hsv := - match seval_hsval ge sp hsv rs0 m0 with - | Some v => v - | None => Vundef - end. - -Definition select_first (ox oy: option val) := - match ox with - | Some v => Some v - | None => oy - end. - -(** If the register was computed by hrs, evaluate the symbolic value from hrs. - Else, take the value directly from rs0 *) -Definition seval_partial_regset ge sp rs0 m0 hrs := - let hrs_eval := PTree.map1 (seval_sval_partial ge sp rs0 m0) hrs in - (fst rs0, PTree.combine select_first hrs_eval (snd rs0)). - -Lemma seval_partial_regset_get ge sp rs0 m0 hrs r: - (seval_partial_regset ge sp rs0 m0 hrs) # r = - match (hrs ! r) with Some sv => seval_sval_partial ge sp rs0 m0 sv | None => (rs0 # r) end. -Proof. - unfold seval_partial_regset. unfold Regmap.get. simpl. - rewrite PTree.gcombine; [| simpl; reflexivity]. rewrite PTree.gmap1. - destruct (hrs ! r); simpl; [reflexivity|]. - destruct ((snd rs0) ! r); reflexivity. -Qed. - -Theorem hsilocal_simu_core_correct hst1 hst2 of ge1 ge2 sp rs0 m0 rs m st1 st2: - hsilocal_simu_core of hst1 hst2 -> - hsilocal_refines ge1 sp rs0 m0 hst1 st1 -> - hsilocal_refines ge2 sp rs0 m0 hst2 st2 -> - (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) -> - ssem_local ge1 sp st1 rs0 m0 rs m -> - match of with - | None => ssem_local ge2 sp st2 rs0 m0 rs m - | Some alive => - let rs' := seval_partial_regset ge2 sp rs0 m0 (hsi_sreg hst2) - in ssem_local ge2 sp st2 rs0 m0 rs' m /\ eqlive_reg (fun r => Regset.In r alive) rs rs' - end. -Proof. - intros CORE HREF1 HREF2 GFS SEML. - refine (modusponens _ _ (ssem_local_refines_hok _ _ _ _ _ _ _ _ _ _) _); eauto. - intro HOK1. - refine (modusponens _ _ (hsilocal_simu_core_nofail _ _ _ _ _ _ _ _ _ _ _) _); eauto. - intro HOK2. - destruct SEML as (PRE & MEMEQ & RSEQ). - assert (SIPRE: si_pre st2 ge2 sp rs0 m0). { destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2. } - assert (SMEMEVAL: seval_smem ge2 sp (si_smem st2) rs0 m0 = Some m). { - destruct HREF2 as (_ & MEMEQ2 & _). destruct HREF1 as (_ & MEMEQ1 & _). - destruct CORE as (_ & _ & MEMEQ3). - rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3. - erewrite hsmem_eval_preserved; [| eapply GFS]. - rewrite MEMEQ1; auto. } - destruct of as [alive |]. - - constructor. - + constructor; [assumption | constructor; [assumption|]]. - destruct HREF2 as (B & _ & A & PT). - (** B, A and PT are used for the auto below *) - assert (forall r : positive, hsi_sreg_eval ge2 sp hst2 r rs0 m0 = seval_sval ge2 sp (si_sreg st2 r) rs0 m0) by auto. - intro r. rewrite <- H. clear H. rewrite seval_partial_regset_get. unfold hsi_sreg_eval. - destruct (hst2 ! r) eqn:HST2; [| simpl; reflexivity]. - unfold seval_sval_partial. - assert (seval_hsval ge2 sp h rs0 m0 <> None) by eauto. - destruct (seval_hsval ge2 sp h rs0 m0); [reflexivity | contradiction]. - + intros r ALIVE. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _). - destruct CORE as (_ & C & _). rewrite seval_partial_regset_get. - assert (OPT: forall (x y: val), Some x = Some y -> x = y) by congruence. - destruct (hst2 ! r) eqn:HST2; apply OPT; clear OPT. - ++ 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].*) - 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. *) - - constructor; [|constructor]. - + destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2. - + destruct HREF2 as (_ & MEMEQ2 & _). destruct HREF1 as (_ & MEMEQ1 & _). - destruct CORE as (_ & _ & MEMEQ3). - 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. 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 *) - Definition hsilocal_simu_check hst1 hst2 : ?? unit := + DEBUG("? last check");; phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_simu_check: hsi_smem sets aren't equiv";; + PTree_eq_check (hsi_sreg hst1) (hsi_sreg hst2);; Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);; - PTree_eq_check (hsi_sreg hst1) (hsi_sreg hst2). + DEBUG("=> last check: OK"). -Theorem hsilocal_simu_check_correct hst1 hst2: - WHEN hsilocal_simu_check hst1 hst2 ~> tt THEN - hsilocal_simu_core None hst1 hst2. -Proof. - wlp_simplify. constructor; [|constructor]; [assumption | | congruence]. - intros. unfold hsi_sreg_get. rewrite (PTree_eq_check_correct _ hst1 hst2); [|eassumption]. - reflexivity. -Qed. -Hint Resolve hsilocal_simu_check_correct: wlp. -Global Opaque hsilocal_simu_check. +Definition revmap_check_single (dm: PTree.t node) (n tn: node) : ?? unit := + DO res <~ some_or_fail (dm ! tn) "revmap_check_single: no mapping for tn";; + struct_check n res "revmap_check_single: n and res are physically different". Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit := + DEBUG("? frame check");; phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_frame_simu_check: hsi_smem sets aren't equiv";; + PTree_frame_eq_check frame (hsi_sreg hst1) (hsi_sreg hst2);; Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);; - PTree_frame_eq_check frame (hsi_sreg hst1) (hsi_sreg hst2). - -Lemma setoid_in {A: Type} (a: A): forall l, - SetoidList.InA (fun x y => x = y) a l -> - In a l. -Proof. - induction l; intros; inv H. - - constructor. reflexivity. - - right. auto. -Qed. - -Lemma regset_elements_in r rs: - Regset.In r rs -> - In r (Regset.elements rs). -Proof. - intros. exploit Regset.elements_1; eauto. intro SIN. - 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. 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. - -Definition init_hsistate_local (_:unit): ?? hsistate_local - := DO hm <~ hSinit ();; - RET {| hsi_smem := hm; hsi_ok_lsval := nil; hsi_sreg := PTree.empty hsval |}. - -Remark hsinit_seval_hsmem ge sp rs0 m0: - WHEN hSinit () ~> init THEN - seval_hsmem ge sp init rs0 m0 = Some m0. -Proof. - wlp_simplify. unfold hSinit in Hexta. apply hC_hsmem_correct in Hexta. simpl in Hexta. - unfold seval_hsmem. rewrite <- Hexta. simpl. reflexivity. -Qed. - -Remark init_hsistate_local_correct ge sp rs0 m0: - WHEN init_hsistate_local () ~> hsl THEN - hsilocal_refines ge sp rs0 m0 hsl init_sistate_local. -Proof. - wlp_simplify. - constructor; constructor; simpl. - - intro. destruct H as (_ & SMEM & SVAL). unfold hsok_local. simpl. contradiction. - - intro. constructor; [simpl; auto|]. constructor; simpl; discriminate. - - unfold hsok_local. simpl. intros; simpl. apply hsinit_seval_hsmem. assumption. - - constructor. - + intros. simpl. unfold hsi_sreg_eval. rewrite PTree.gempty. reflexivity. - + intros r sv. rewrite PTree.gempty. discriminate. -Qed. - -(** Simulation of exits *) - -Definition hsiexit_simu_core dm f (hse1 hse2: hsistate_exit) := - (exists path, (fn_path f) ! (hsi_ifso hse1) = Some path - /\ hsilocal_simu_core (Some path.(input_regs)) (hsi_elocal hse1) (hsi_elocal hse2)) - /\ dm ! (hsi_ifso hse2) = Some (hsi_ifso hse1) - /\ hsi_cond hse1 = hsi_cond hse2 - /\ hsi_scondargs hse1 = hsi_scondargs hse2 (* FIXME - should there be something about okvals ? *). - -(** NB: we split the refinement relation between a "static" part -- independendent of the initial context - and a "dynamic" part -- that depends on it -*) -Definition hsiexit_refines_stat (hext: hsistate_exit) (ext: sistate_exit): Prop := - hsi_cond hext = si_cond ext - /\ hsi_ifso hext = si_ifso ext. - -Definition hsok_exit ge sp rs m hse := hsok_local ge sp rs m (hsi_elocal hse). - -Definition hseval_condition ge sp cond hcondargs hmem rs0 m0 := - seval_condition ge sp cond (hsval_list_proj hcondargs) (hsmem_proj hmem) rs0 m0. - -Lemma hseval_condition_preserved ge ge' sp cond args mem rs0 m0: - (forall s : ident, Genv.find_symbol ge' s = Genv.find_symbol ge s) -> - hseval_condition ge sp cond args mem rs0 m0 = hseval_condition ge' sp cond args mem rs0 m0. -Proof. - intros. unfold hseval_condition. erewrite seval_condition_preserved; [|eapply H]. - reflexivity. -Qed. - -Definition hsiexit_refines_dyn ge sp rs0 m0 (hext: hsistate_exit) (ext: sistate_exit): Prop := - hsilocal_refines ge sp rs0 m0 (hsi_elocal hext) (si_elocal ext) - /\ hseval_condition ge sp (hsi_cond hext) (hsi_scondargs hext) (hsi_smem (hsi_elocal hext)) rs0 m0 - = seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs0 m0. - -Definition hsiexit_simu dm f (ctx: simu_proof_context f) hse1 hse2: Prop := forall se1 se2, - hsiexit_refines_stat hse1 se1 -> - hsiexit_refines_stat hse2 se2 -> - hsiexit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 -> - hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 -> - siexit_simu dm f ctx se1 se2. - -Lemma hsiexit_simu_core_nofail dm f hse1 hse2 ge1 ge2 sp rs m: - hsiexit_simu_core dm f hse1 hse2 -> - (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) -> - hsok_exit ge1 sp rs m hse1 -> - hsok_exit ge2 sp rs m hse2. -Proof. - intros CORE GFS HOK1. - destruct CORE as ((p & _ & CORE') & _ & _ & _). - eapply hsilocal_simu_core_nofail; eauto. -Qed. - -Theorem hsiexit_simu_core_correct dm f hse1 hse2 ctx: - hsiexit_simu_core dm f hse1 hse2 -> - hsiexit_simu dm f ctx hse1 hse2. -Proof. - intros SIMUC st1 st2 HREF1 HREF2 HDYN1 HDYN2. - assert (SEVALC: - seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond st1) (si_scondargs st1) (si_smem (si_elocal st1)) - (the_rs0 ctx) (the_m0 ctx) = - seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond st2) (si_scondargs st2) (si_smem (si_elocal st2)) - (the_rs0 ctx) (the_m0 ctx)). - { destruct HDYN1 as (_ & SCOND1). rewrite <- SCOND1 by assumption. clear SCOND1. - destruct HDYN2 as (_ & SCOND2). rewrite <- SCOND2 by assumption. clear SCOND2. - destruct SIMUC as ((path & _ & LSIMU) & _ & CONDEQ & ARGSEQ). destruct LSIMU as (_ & _ & MEMEQ). - rewrite CONDEQ. rewrite ARGSEQ. rewrite MEMEQ. erewrite <- hseval_condition_preserved; eauto. - eapply ctx. } - constructor; [assumption|]. intros is1 ICONT SSEME. - assert (HOK1: hsok_exit (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1). { - unfold hsok_exit. destruct SSEME as (_ & SSEML & _). apply ssem_local_sok in SSEML. - destruct HDYN1 as (LREF & _). destruct LREF as (OKEQ & _ & _). rewrite <- OKEQ. assumption. } - refine (modusponens _ _ (hsiexit_simu_core_nofail _ _ _ _ _ _ _ _ _ _ _ _) _). - 2: eapply ctx. all: eauto. intro HOK2. - destruct SSEME as (SCOND & SLOC & PCEQ). destruct SIMUC as ((path & PATH & LSIMU) & REVEQ & _ & _). - destruct HDYN1 as (LREF1 & _). destruct HDYN2 as (LREF2 & _). - exploit hsilocal_simu_core_correct; eauto; [apply ctx|]. simpl. - intros (SSEML & EQREG). - eexists (mk_istate (icontinue is1) (si_ifso st2) _ (imem is1)). simpl. constructor. - - constructor; [|constructor]; [congruence | eassumption | reflexivity]. - - unfold istate_simu. rewrite ICONT. - simpl. assert (PCEQ': hsi_ifso hse1 = ipc is1). { destruct HREF1 as (_ & IFSO). congruence. } - exists path. constructor; [|constructor]; [congruence | | ]. - + constructor; [|constructor]; simpl; auto. - + destruct HREF2 as (_ & IFSO). congruence. -Qed. - -Remark hsiexit_simu_siexit dm f ctx hse1 hse2 se1 se2: - hsiexit_simu dm f ctx hse1 hse2 -> - hsiexit_refines_stat hse1 se1 -> - hsiexit_refines_stat hse2 se2 -> - hsiexit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 -> - hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 -> - siexit_simu dm f ctx se1 se2. -Proof. - auto. -Qed. - -Definition revmap_check_single (dm: PTree.t node) (n tn: node) : ?? unit := - DO res <~ some_or_fail (dm ! tn) "revmap_check_single: no mapping for tn";; - struct_check n res "revmap_check_single: n and res are physically different". + DEBUG("=> frame check: OK"). Definition hsiexit_simu_check (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit): ?? unit := struct_check (hsi_cond hse1) (hsi_cond hse2) "hsiexit_simu_check: conditions do not match";; @@ -901,37 +925,6 @@ Definition hsiexit_simu_check (dm: PTree.t node) (f: RTLpath.function) (hse1 hse DO path <~ some_or_fail ((fn_path f) ! (hsi_ifso hse1)) "hsiexit_simu_check: internal error";; hsilocal_frame_simu_check (Regset.elements path.(input_regs)) (hsi_elocal hse1) (hsi_elocal hse2). -Theorem hsiexit_simu_check_correct dm f hse1 hse2: - WHEN hsiexit_simu_check dm f hse1 hse2 ~> tt THEN - hsiexit_simu_core dm f hse1 hse2. -Proof. - wlp_simplify. constructor; [| constructor; [| constructor]]. 2-4: assumption. - exists a. constructor. 1-2: assumption. -Qed. -Hint Resolve hsiexit_simu_check_correct: wlp. -Global Opaque hsiexit_simu_check. - -Definition hsiexits_simu dm f (ctx: simu_proof_context f) lhse1 lhse2: Prop := - list_forall2 (hsiexit_simu dm f ctx) lhse1 lhse2. - -Definition hsiexits_simu_core dm f lhse1 lhse2: Prop := - list_forall2 (hsiexit_simu_core dm f) lhse1 lhse2. - -Theorem hsiexits_simu_core_correct dm f lhse1 lhse2 ctx: - hsiexits_simu_core dm f lhse1 lhse2 -> - hsiexits_simu dm f ctx lhse1 lhse2. -Proof. - induction 1; [constructor|]. - constructor; [|apply IHlist_forall2; assumption]. - apply hsiexit_simu_core_correct; assumption. -Qed. - -Definition hsiexits_refines_stat lhse lse := - list_forall2 hsiexit_refines_stat lhse lse. - -Definition hsiexits_refines_dyn ge sp rs0 m0 lhse se := - list_forall2 (hsiexit_refines_dyn ge sp rs0 m0) lhse se. - Fixpoint hsiexits_simu_check (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) := match lhse1,lhse2 with | nil, nil => RET tt @@ -941,498 +934,9 @@ Fixpoint hsiexits_simu_check (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhs | _, _ => FAILWITH "siexists_simu_check: lengths do not match" end. -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; 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. - -Definition hsistate_simu_core dm f (hse1 hse2: hsistate) := - dm ! (hsi_pc hse2) = Some (hsi_pc hse1) - /\ list_forall2 (hsiexit_simu_core dm f) (hsi_exits hse1) (hsi_exits hse2) - /\ hsilocal_simu_core None (hsi_local hse1) (hsi_local hse2). - -Definition hsistate_refines_stat (hst: hsistate) (st:sistate): Prop := - hsi_pc hst = si_pc st - /\ hsiexits_refines_stat (hsi_exits hst) (si_exits st). - -Definition hsistate_refines_dyn ge sp rs0 m0 (hst: hsistate) (st:sistate): Prop := - hsiexits_refines_dyn ge sp rs0 m0 (hsi_exits hst) (si_exits st) - /\ hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st). - -Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2, - hsistate_refines_stat hst1 st1 -> - hsistate_refines_stat hst2 st2 -> - hsistate_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 st1 -> - hsistate_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 st2 -> - sistate_simu dm f st1 st2 ctx. - -Definition init_hsistate pc: ?? hsistate - := DO hst <~ init_hsistate_local ();; - RET {| hsi_pc := pc; hsi_exits := nil; hsi_local := hst |}. - -Remark init_hsistate_correct_stat pc: - WHEN init_hsistate pc ~> hst THEN - hsistate_refines_stat hst (init_sistate pc). -Proof. - wlp_simplify. - constructor; constructor; simpl; auto. -Qed. -Hint Resolve init_hsistate_correct_stat: wlp. - -Remark init_hsistate_correct_dyn ge sp rs0 m0 pc: - WHEN init_hsistate pc ~> hst THEN - hsistate_refines_dyn ge sp rs0 m0 hst (init_sistate pc). -Proof. - unfold init_hsistate. wlp_step_bind hst HST. - wlp_simplify. - constructor; simpl; auto. - - apply list_forall2_nil. - - apply init_hsistate_local_correct. assumption. -Qed. - -Lemma siexits_simu_all_fallthrough dm f ctx: forall lse1 lse2, - siexits_simu dm f lse1 lse2 ctx -> - all_fallthrough (the_ge1 ctx) (the_sp ctx) lse1 (the_rs0 ctx) (the_m0 ctx) -> - all_fallthrough (the_ge2 ctx) (the_sp ctx) lse2 (the_rs0 ctx) (the_m0 ctx). -Proof. - induction 1; [unfold all_fallthrough; contradiction|]. - intros X ext INEXT. eapply all_fallthrough_revcons in X. destruct X as (SEVAL & ALLFU). - apply IHlist_forall2 in ALLFU. - destruct H as (CONDSIMU & _). - inv INEXT; [|eauto]. - erewrite <- CONDSIMU; eauto. -Qed. - -Lemma hsiexits_simu_siexits dm f ctx lhse1 lhse2: - hsiexits_simu dm f ctx lhse1 lhse2 -> - forall lse1 lse2, - hsiexits_refines_stat lhse1 lse1 -> - hsiexits_refines_stat lhse2 lse2 -> - hsiexits_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse1 lse1 -> - hsiexits_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse2 lse2 -> - siexits_simu dm f lse1 lse2 ctx. -Proof. - induction 1. - - intros. inv H. inv H0. constructor. - - intros lse1 lse2 SREF1 SREF2 DREF1 DREF2. inv SREF1. inv SREF2. inv DREF1. inv DREF2. - constructor; [| eapply IHlist_forall2; eauto]. - eapply hsiexit_simu_siexit; eauto. -Qed. - -Lemma siexits_simu_all_fallthrough_upto dm f ctx lse1 lse2: - siexits_simu dm f lse1 lse2 ctx -> forall ext1 lx1, - all_fallthrough_upto_exit (the_ge1 ctx) (the_sp ctx) ext1 lx1 lse1 (the_rs0 ctx) (the_m0 ctx) -> - exists ext2 lx2, - all_fallthrough_upto_exit (the_ge2 ctx) (the_sp ctx) ext2 lx2 lse2 (the_rs0 ctx) (the_m0 ctx) - /\ length lx1 = length lx2. -Proof. - induction 1. - - intros. destruct H as (ITAIL & ALLFU). eapply is_tail_false in ITAIL. contradiction. - - intros ext1 lx1 ALLFUE. - destruct ALLFUE as (ITAIL & ALLFU). inv ITAIL. - + eexists; eexists. - constructor; [| eapply list_forall2_length; eauto]. - constructor; [econstructor | eapply siexits_simu_all_fallthrough; eauto]. - + exploit IHlist_forall2; [constructor; eauto|]. - intros (ext2 & lx2 & ALLFUE2 & LENEQ). - eexists; eexists. constructor; eauto. - eapply all_fallthrough_upto_exit_cons; eauto. -Qed. - -Lemma list_forall2_nth_error {A} (l1 l2: list A) P: - list_forall2 P l1 l2 -> - forall x1 x2 n, - nth_error l1 n = Some x1 -> - nth_error l2 n = Some x2 -> - P x1 x2. -Proof. - induction 1. - - intros. rewrite nth_error_nil in H. discriminate. - - intros x1 x2 n. destruct n as [|n]; simpl. - + intros. inv H1. inv H2. assumption. - + apply IHlist_forall2. -Qed. - -Lemma is_tail_length {A} (l1 l2: list A): - is_tail l1 l2 -> - (length l1 <= length l2)%nat. -Proof. - induction l2. - - intro. destruct l1; auto. apply is_tail_false in H. contradiction. - - intros ITAIL. inv ITAIL; auto. - apply IHl2 in H1. clear IHl2. simpl. omega. -Qed. - -Lemma is_tail_nth_error {A} (l1 l2: list A) x: - is_tail (x::l1) l2 -> - nth_error l2 ((length l2) - length l1 - 1) = Some x. -Proof. - induction l2. - - intro ITAIL. apply is_tail_false in ITAIL. contradiction. - - intros ITAIL. assert (length (a::l2) = S (length l2)) by auto. rewrite H. clear H. - assert (forall n n', ((S n) - n' - 1)%nat = (n - n')%nat) by (intros; omega). rewrite H. clear H. - inv ITAIL. - + assert (forall n, (n - n)%nat = 0%nat) by (intro; omega). rewrite H. - simpl. reflexivity. - + exploit IHl2; eauto. intros. clear IHl2. - assert (forall n n', (n > n')%nat -> (n - n')%nat = S (n - n' - 1)%nat) by (intros; omega). - exploit (is_tail_length (x::l1)); eauto. intro. simpl in H2. - assert ((length l2 > length l1)%nat) by omega. clear H2. - rewrite H0; auto. -Qed. - -Theorem hsistate_simu_core_correct dm f hst1 hst2 ctx: - hsistate_simu_core dm f hst1 hst2 -> - hsistate_simu dm f hst1 hst2 ctx. -Proof. - intros SIMUC st1 st2 HREF1 HREF2 DREF1 DREF2 is1 SEMI. - destruct HREF1 as (PCREF1 & EREF1). destruct HREF2 as (PCREF2 & EREF2). - destruct DREF1 as (DEREF1 & LREF1). destruct DREF2 as (DEREF2 & LREF2). - destruct SIMUC as (PCSIMU & ESIMU & LSIMU). - exploit hsiexits_simu_core_correct; eauto. intro HESIMU. - unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT. - - destruct SEMI as (SSEML & PCEQ & ALLFU). - exploit hsilocal_simu_core_correct; eauto; [apply ctx|]. simpl. intro SSEML2. - exists (mk_istate (icontinue is1) (si_pc st2) (irs is1) (imem is1)). constructor. - + unfold ssem_internal. simpl. rewrite ICONT. constructor; [assumption | constructor; [reflexivity |]]. - eapply siexits_simu_all_fallthrough; eauto. eapply hsiexits_simu_siexits; eauto. - + unfold istate_simu. rewrite ICONT. constructor; [simpl; assumption | constructor; [| reflexivity]]. - constructor. - - destruct SEMI as (ext & lx & SSEME & ALLFU). - assert (SESIMU: siexits_simu dm f (si_exits st1) (si_exits st2) ctx) by (eapply hsiexits_simu_siexits; eauto). - exploit siexits_simu_all_fallthrough_upto; eauto. intros (ext2 & lx2 & ALLFU2 & LENEQ). - assert (EXTSIMU: siexit_simu dm f ctx ext ext2). { - eapply list_forall2_nth_error; eauto. - - destruct ALLFU as (ITAIL & _). eapply is_tail_nth_error; eauto. - - destruct ALLFU2 as (ITAIL & _). eapply is_tail_nth_error in ITAIL. - assert (LENEQ': length (si_exits st1) = length (si_exits st2)) by (eapply list_forall2_length; eauto). - congruence. } - destruct EXTSIMU as (CONDEVAL & EXTSIMU). - apply EXTSIMU in SSEME; [|assumption]. clear EXTSIMU. destruct SSEME as (is2 & SSEME2 & ISIMU). - exists (mk_istate (icontinue is1) (ipc is2) (irs is2) (imem is2)). constructor. - + unfold ssem_internal. simpl. rewrite ICONT. exists ext2, lx2. constructor; assumption. - + unfold istate_simu in *. rewrite ICONT in *. destruct ISIMU as (path & PATHEQ & ISIMULIVE & DMEQ). - destruct ISIMULIVE as (CONTEQ & REGEQ & MEMEQ). - exists path. repeat (constructor; auto). -Qed. - Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) := - revmap_check_single dm (hsi_pc hst1) (hsi_pc hst2);; - hsilocal_simu_check (hsi_local hst1) (hsi_local hst2);; - hsiexits_simu_check dm f (hsi_exits hst1) (hsi_exits hst2). - -Theorem hsistate_simu_check_correct dm f hst1 hst2: - WHEN hsistate_simu_check dm f hst1 hst2 ~> tt THEN - hsistate_simu_core dm f hst1 hst2. -Proof. - wlp_simplify. - constructor; [|constructor]. 1-3: assumption. -Qed. -Hint Resolve hsistate_simu_check_correct: wlp. -Global Opaque hsistate_simu_check. - -Definition hsi_proj (hsi: hsval + ident) := match hsi with - | inl hv => inl (hsval_proj hv) - | inr id => inr id - end. - -Fixpoint barg_proj (bhv: builtin_arg hsval) := match bhv with - | BA hv => BA (hsval_proj hv) - | BA_splitlong ba1 ba2 => BA_splitlong (barg_proj ba1) (barg_proj ba2) - | BA_addptr ba1 ba2 => BA_addptr (barg_proj ba1) (barg_proj ba2) - | BA_int i => BA_int i - | BA_long i => BA_long i - | BA_float f => BA_float f - | BA_single f32 => BA_single f32 - | BA_loadstack m p => BA_loadstack m p - | BA_addrstack p => BA_addrstack p - | BA_loadglobal c i p => BA_loadglobal c i p - | BA_addrglobal i p => BA_addrglobal i p - end. - -Fixpoint barg_list_proj lbh := match lbh with - | [] => [] - | bh::lbh => (barg_proj bh) :: (barg_list_proj lbh) - end. - -Definition option_hsval_proj oh := match oh with None => None | Some h => Some (hsval_proj h) end. - -Definition hfinal_proj hfv := match hfv with - | HSnone => Snone - | HScall s hvi hlv r pc => Scall s (hsi_proj hvi) (hsval_list_proj hlv) r pc - | HStailcall s hvi hlv => Stailcall s (hsi_proj hvi) (hsval_list_proj hlv) - | HSbuiltin ef lbh br pc => Sbuiltin ef (barg_list_proj lbh) br pc - | HSjumptable hv ln => Sjumptable (hsval_proj hv) ln - | HSreturn oh => Sreturn (option_hsval_proj oh) - end. - -Section HFINAL_REFINES. - -Variable ge: RTL.genv. -Variable sp: val. -Variable rs0: regset. -Variable m0: mem. - -Definition sval_refines (hv: hsval) (sv: sval) := seval_hsval ge sp hv rs0 m0 = seval_sval ge sp sv rs0 m0. - -Definition sum_refines (hsi: hsval + ident) (si: sval + ident) := - match hsi, si with - | inl hv, inl sv => sval_refines hv sv - | inr id, inr id' => id = id' - | _, _ => False - end. - -Inductive list_refines: hlist_sval -> list_sval -> Prop := - | hsnil_ref: forall h, list_refines (HSnil h) Snil - | hscons_ref: forall lhv lsv hv sv h, - list_refines lhv lsv -> - sval_refines hv sv -> - list_refines (HScons hv lhv h) (Scons sv lsv). - -Inductive barg_refines: builtin_arg hsval -> builtin_arg sval -> Prop := - | hba_ref: forall hsv sv, sval_refines hsv sv -> barg_refines (BA hsv) (BA sv) - | hba_splitlong: forall bha1 bha2 ba1 ba2, - barg_refines bha1 ba1 -> barg_refines bha2 ba2 -> - barg_refines (BA_splitlong bha1 bha2) (BA_splitlong ba1 ba2) - | hba_addptr: forall bha1 bha2 ba1 ba2, - barg_refines bha1 ba1 -> barg_refines bha2 ba2 -> - barg_refines (BA_addptr bha1 bha2) (BA_addptr ba1 ba2) - | hba_int: forall i, barg_refines (BA_int i) (BA_int i) - | hba_long: forall l, barg_refines (BA_long l) (BA_long l) - | hba_float: forall f, barg_refines (BA_float f) (BA_float f) - | hba_single: forall s, barg_refines (BA_single s) (BA_single s) - | hba_loadstack: forall chk ptr, barg_refines (BA_loadstack chk ptr) (BA_loadstack chk ptr) - | hba_addrstack: forall ptr, barg_refines (BA_addrstack ptr) (BA_addrstack ptr) - | hba_loadglobal: forall chk id ptr, barg_refines (BA_loadglobal chk id ptr) (BA_loadglobal chk id ptr) - | hba_addrglobal: forall id ptr, barg_refines (BA_addrglobal id ptr) (BA_addrglobal id ptr). - -Definition option_refines ohsv osv := - match ohsv, osv with - | Some hsv, Some sv => sval_refines hsv sv - | None, None => True - | _, _ => False - end. - -Inductive hfinal_refines: hsfval -> sfval -> Prop := - | hsnone_ref: hfinal_refines HSnone Snone - | hscall_ref: forall hros ros hargs args s r pc, - sum_refines hros ros -> - list_refines hargs args -> - hfinal_refines (HScall s hros hargs r pc) (Scall s ros args r pc) - | hstailcall_ref: forall hros ros hargs args s, - sum_refines hros ros -> - list_refines hargs args -> - hfinal_refines (HStailcall s hros hargs) (Stailcall s ros args) - | hsbuiltin_ref: forall ef lbha lba br pc, - list_forall2 barg_refines lbha lba -> - hfinal_refines (HSbuiltin ef lbha br pc) (Sbuiltin ef lba br pc) - | hsjumptable_ref: forall hsv sv lpc, - sval_refines hsv sv -> hfinal_refines (HSjumptable hsv lpc) (Sjumptable sv lpc) - | hsreturn_ref: forall ohsv osv, - option_refines ohsv osv -> hfinal_refines (HSreturn ohsv) (Sreturn osv). - -Remark hfinal_refines_snone: hfinal_refines HSnone Snone. -Proof. constructor. Qed. - -End HFINAL_REFINES. - -Lemma list_proj_refines_eq ge ge' sp rs0 m0: forall lsv hlsv, - (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) -> - list_refines ge sp rs0 m0 hlsv lsv -> - forall hlsv' lsv', - list_refines ge' sp rs0 m0 hlsv' lsv' -> - hsval_list_proj hlsv = hsval_list_proj hlsv' -> - seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv' rs0 m0. -Proof. - induction 2; rename H into GFS. - - simpl. intros. destruct hlsv'; try discriminate. clear H0. - inv H. simpl. reflexivity. - - simpl. intros. destruct hlsv'; try discriminate. - simpl in H2. inv H2. destruct lsv'; [inv H|]. - inv H. simpl. - assert (SVALEQ: seval_sval ge sp sv rs0 m0 = seval_sval ge' sp sv0 rs0 m0). { - rewrite <- H10. rewrite <- H1. unfold seval_hsval. erewrite <- seval_preserved; [| eapply GFS]. congruence. - } rewrite SVALEQ. - 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 => - match f2 with - | Scall sig2 svos2 lsv2 res2 pc2 => - dm ! pc2 = Some pc1 /\ sig1 = sig2 /\ svos1 = svos2 /\ lsv1 = lsv2 /\ res1 = res2 - | _ => False - end - | Sbuiltin ef1 lbs1 br1 pc1 => - match f2 with - | Sbuiltin ef2 lbs2 br2 pc2 => - dm ! pc2 = Some pc1 /\ ef1 = ef2 /\ lbs1 = lbs2 /\ br1 = br2 - | _ => False - end - | Sjumptable sv1 lpc1 => - match f2 with - | Sjumptable sv2 lpc2 => - ptree_get_list dm lpc2 = Some lpc1 /\ sv1 = sv2 - | _ => False - end - | Snone => - match f2 with - | Snone => dm ! pc2 = Some pc1 - | _ => False - end - (* Stailcall, Sreturn *) - | _ => f1 = f2 - end. - -Definition hfinal_simu_core (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (hf1 hf2: hsfval): Prop := - final_simu_core dm f pc1 pc2 (hfinal_proj hf1) (hfinal_proj hf2). - -Lemma svident_simu_refl f ctx s: - svident_simu f ctx s s. -Proof. - destruct s; constructor; [| reflexivity]. - erewrite <- seval_preserved; [| eapply ctx]. constructor. -Qed. - -Theorem hfinal_simu_core_correct dm f ctx opc1 opc2 hf1 hf2 f1 f2: - hfinal_simu_core dm f opc1 opc2 hf1 hf2 -> - hfinal_refines (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hf1 f1 -> - hfinal_refines (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hf2 f2 -> - sfval_simu dm f opc1 opc2 ctx f1 f2. -Proof. - assert (GFS: forall s : ident, Genv.find_symbol (the_ge1 ctx) s = Genv.find_symbol (the_ge2 ctx) s) by apply ctx. - intros CORE FREF1 FREF2. - destruct hf1; inv FREF1. - (* Snone *) - - destruct hf2; try contradiction. inv FREF2. - inv CORE. constructor. assumption. - (* Scall *) - - rename H5 into SREF1. rename H6 into LREF1. - destruct hf2; try contradiction. inv FREF2. - rename H5 into SREF2. rename H6 into LREF2. - destruct CORE as (PCEQ & ? & ? & ? & ?). subst. - rename H0 into SVOSEQ. rename H1 into LSVEQ. - constructor; [assumption | |]. - + destruct svos. - * 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. - (* Stailcall *) - - 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 *) - - 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 *) - - admit. -Admitted. (* TODO - prove it *) - - - -Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval := - match i with - | Icall sig ros args res pc => - DO svos <~ hsum_left hst ros;; - DO sargs <~ hlist_args hst args;; - RET (HScall sig svos sargs res pc) - | Itailcall sig ros args => - DO svos <~ hsum_left hst ros;; - DO sargs <~ hlist_args hst args;; - RET (HStailcall sig svos sargs) - | Ibuiltin ef args res pc => - DO sargs <~ hbuiltin_args hst args;; - RET (HSbuiltin ef sargs res pc) - | Ijumptable reg tbl => - DO sv <~ hsi_sreg_get hst reg;; - RET (HSjumptable sv tbl) - | Ireturn or => - match or with - | Some r => DO hr <~ hsi_sreg_get hst r;; RET (HSreturn (Some hr)) - | None => RET (HSreturn None) - end - | _ => RET (HSnone) - end. - -Lemma hsexec_final_correct ge sp rs0 m0 hsl sl i: - hsilocal_refines ge sp rs0 m0 hsl sl -> - WHEN hsexec_final i hsl ~> hsf THEN - hfinal_refines ge sp rs0 m0 hsf (sexec_final i sl). -Proof. -(* destruct i; simpl; intros HLREF; try (wlp_simplify; apply hfinal_refines_snone). - (* Scall *) - - wlp_step_bind svos SVOS. wlp_step_bind sargs SARGS. wlp_intros hsf HSF. - apply mayRet_ret in HSF. subst. unfold hfinal_refines. simpl. *) - -(* - + intro. inv H. constructor; auto. - ++ erewrite <- sfind_function_conserves; eauto. - ++ erewrite <- seval_list_sval_refines; eauto. - + intro. inv H. constructor; auto. - ++ erewrite sfind_function_conserves; eauto. - ++ erewrite seval_list_sval_refines; eauto. - (* Stailcall *) - - admit. - (* Sbuiltin *) - - admit. - (* Sjumptable *) - - admit. - (* Sreturn *) - - admit. - *)Admitted. + hsiexits_simu_check dm f (hsi_exits hst1) (hsi_exits hst2);; + hsilocal_simu_check (hsi_local hst1) (hsi_local hst2). Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): ?? unit := match ln, ln' with @@ -1471,9 +975,9 @@ Fixpoint list_builtin_arg_simu_check lbs1 lbs2 := | _, _ => FAILWITH "list_builtin_arg_simu_check: length mismatch" end. -Definition sfval_simu_check (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node) (fv1 fv2: hsfval) := +Definition sfval_simu_check (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (fv1 fv2: hsfval) := match fv1, fv2 with - | HSnone, HSnone => revmap_check_single dm opc1 opc2 + | HSnone, HSnone => revmap_check_single dm pc1 pc2 | HScall sig1 svos1 lsv1 res1 pc1, HScall sig2 svos2 lsv2 res2 pc2 => revmap_check_single dm pc1 pc2;; phys_check sig1 sig2 "sfval_simu_check: Scall different signatures";; @@ -1497,105 +1001,21 @@ Definition sfval_simu_check (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: | _, _ => FAILWITH "sfval_simu_check: structure mismatch" end. -Theorem sfval_simu_check_correct dm f opc1 opc2 fv1 fv2: - WHEN sfval_simu_check dm f opc1 opc2 fv1 fv2 ~> tt THEN - hfinal_simu_core dm f opc1 opc2 fv1 fv2. -Proof. - wlp_simplify. destruct fv1. admit. (* needs to destruct fv2 and rule out the absurd cases *) -Admitted. -Hint Resolve sfval_simu_check_correct: wlp. -Global Opaque hfinal_simu_core. - -Definition hsstate_refines (hst: hsstate) (st:sstate): Prop := - hsistate_refines_stat (hinternal hst) (internal st) - /\ (forall ge sp rs0 m0, hsistate_refines_dyn ge sp rs0 m0 (hinternal hst) (internal st) - /\ hfinal_refines ge sp rs0 m0 (hfinal hst) (final st)) -. - -Definition hsstate_simu_core (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) := - hsistate_simu_core dm f (hinternal hst1) (hinternal hst2) - /\ hfinal_simu_core dm f (hsi_pc (hinternal hst1)) (hsi_pc (hinternal hst2)) (hfinal hst1) (hfinal hst2). - -Definition hsstate_simu dm f (hst1 hst2: hsstate) ctx: Prop := - forall st1 st2, - hsstate_refines hst1 st1 -> - hsstate_refines hst2 st2 -> sstate_simu dm f st1 st2 ctx. - -Theorem hsstate_simu_core_correct dm f ctx hst1 hst2: - hsstate_simu_core dm f hst1 hst2 -> - hsstate_simu dm f hst1 hst2 ctx. -Proof. - intros (SCORE & FSIMU). intros st1 st2 HREF1 HREF2. - destruct HREF1 as (SREF1 & DREF1 & FREF1). destruct HREF2 as (SREF2 & DREF2 & FREF2). - assert (PCEQ: dm ! (hsi_pc hst2) = Some (hsi_pc hst1)) by apply SCORE. - eapply hsistate_simu_core_correct in SCORE. - eapply hfinal_simu_core_correct in FSIMU; eauto. - constructor; [apply SCORE; auto|]. 1-2: eassumption. - destruct SREF1 as (PC1 & _). destruct SREF2 as (PC2 & _). rewrite <- PC1. rewrite <- PC2. - eapply FSIMU. -Qed. - Definition hsstate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) := hsistate_simu_check dm f (hinternal hst1) (hinternal hst2);; sfval_simu_check dm f (hsi_pc hst1) (hsi_pc hst2) (hfinal hst1) (hfinal hst2). -Theorem hsstate_simu_check_correct dm f hst1 hst2: - WHEN hsstate_simu_check dm f hst1 hst2 ~> tt THEN - hsstate_simu_core dm f hst1 hst2. -Proof. - wlp_simplify. constructor. 1-2: assumption. -Qed. -Hint Resolve hsstate_simu_check_correct: wlp. -Global Opaque hsstate_simu_core. - -Definition hsexec (f: function) (pc:node): ?? hsstate := - DO path <~ some_or_fail ((fn_path f)!pc) "hsexec.internal_error.1";; - DO hinit <~ init_hsistate pc;; - DO hst <~ hsiexec_path path.(psize) f hinit;; - DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsexec.internal_error.2";; - DO ohst <~ hsiexec_inst i hst;; - match ohst with - | Some hst' => RET {| hinternal := hst'; hfinal := HSnone |} - | None => DO hsvf <~ hsexec_final i hst.(hsi_local);; - RET {| hinternal := hst; hfinal := hsvf |} - end. - -(* Local Hint Resolve init_hsistate_correct_stat init_hsistate_correct_dyn hsexec_final_correct - hsiexec_inst_correct_dyn hsiexec_path_correct_dyn hfinal_refines_snone: core. *) - -Lemma hsexec_correct f pc: - WHEN hsexec f pc ~> hst THEN - exists st, sexec f pc = Some st /\ hsstate_refines hst st. -Proof. Admitted. -(* unfold hsexec. intro. explore_hyp. - unfold sexec. - rewrite EQ. - exploit hsiexec_path_correct_stat; eauto. - intros (st0 & SPATH & REF0). - generalize REF0; intros (PC0 & XREF0). rewrite SPATH. - erewrite <- PC0. rewrite EQ1. - destruct (hsiexec_inst i h) eqn:HINST. - + exploit hsiexec_inst_correct_stat; eauto. - intros (st1 & EQ2 & PC2 & REF2). - - split; eauto. - - rewrite EQ2. - repeat (econstructor; simpl; eauto). - + erewrite hsiexec_inst_correct_None; eauto. - repeat (econstructor; simpl; eauto). - unfold hfinal_refines. simpl; eauto. -Qed. *) - -End CanonBuilding. - Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node): ?? unit := let (pc2, pc1) := m in (* creating the hash-consing tables *) DO hC_sval <~ hCons hSVAL;; - DO hC_hlist_sval <~ hCons hLSVAL;; + DO hC_list_hsval <~ hCons hLSVAL;; DO hC_hsmem <~ hCons hSMEM;; - let hsexec := hsexec hC_sval.(hC) hC_hlist_sval.(hC) hC_hsmem.(hC) in + let hsexec := hsexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in (* performing the hash-consed executions *) + XDEBUG pc1 (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("entry-point of input superblock: " +; name_pc)%string);; DO hst1 <~ hsexec f pc1;; + XDEBUG pc2 (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("entry-point of output superblock: " +; name_pc)%string);; DO hst2 <~ hsexec tf pc2;; (* comparing the executions *) hsstate_simu_check dm f hst1 hst2. @@ -1603,26 +1023,6 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa Lemma simu_check_single_correct dm tf f pc1 pc2: WHEN simu_check_single dm f tf (pc2, pc1) ~> _ THEN sexec_simu dm f tf pc1 pc2. -Proof. - unfold simu_check_single. - wlp_step_bind hC_sval HSVAL. wlp_step_bind hC_hlist_sval HLSVAL. - wlp_step_bind hC_hsmem HSMEM. wlp_step_bind hst1 HSEXEC1. wlp_step_bind hst2 HSEXEC2. - wlp_intros u HSIMU. - unfold sexec_simu. intros st1 SEXEC. explore. - assert (TODO1: forall hs rhsv, hC hC_sval hs ~~> rhsv -> hsval_proj (hdata hs) = hsval_proj rhsv) - by admit. - assert (TODO2: forall hs rhsv, hC hC_hlist_sval hs ~~> rhsv -> hsval_list_proj (hdata hs) = hsval_list_proj rhsv) - by admit. - assert (TODO3: forall hs rhsv, hC hC_hsmem hs ~~> rhsv -> hsmem_proj (hdata hs) = hsmem_proj rhsv) - by admit. - exploit hsexec_correct; eauto. - intros (st2 & SEXEC2 & REF2). - exploit hsexec_correct. 4: eapply HSEXEC1. all: eauto. - intros (st0 & SEXEC1 & REF1). - rewrite SEXEC1 in SEXEC. inv SEXEC. - eexists. split; eauto. - intros ctx. eapply hsstate_simu_check_correct in HSIMU; eauto. - eapply hsstate_simu_core_correct; eauto. Admitted. Global Opaque simu_check_single. Global Hint Resolve simu_check_single_correct: wlp. @@ -1650,7 +1050,7 @@ Global Hint Resolve simu_check_rec_correct: wlp. Definition imp_simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function): ?? unit := simu_check_rec dm f tf (PTree.elements dm);; - println("simu_check OK!"). + DEBUG("simu_check OK!"). Local Hint Resolve PTree.elements_correct: core. Lemma imp_simu_check_correct dm f tf: diff --git a/kvx/lib/RTLpathSE_theory.v b/kvx/lib/RTLpathSE_theory.v index 3ae6e713..dd0b706e 100644 --- a/kvx/lib/RTLpathSE_theory.v +++ b/kvx/lib/RTLpathSE_theory.v @@ -469,6 +469,11 @@ Definition slocal_set_smem (st:sistate_local) (sm:smem) := Definition sist_set_local (st: sistate) (pc: node) (nxt: sistate_local): sistate := {| si_pc := pc; si_exits := st.(si_exits); si_local:= nxt |}. +Definition slocal_store st chunk addr args src : sistate_local := + let args := list_sval_inj (List.map (si_sreg st) args) in + let src := si_sreg st src in + let sm := Sstore (si_smem st) chunk addr args src + in slocal_set_smem st sm. Definition siexec_inst (i: instruction) (st: sistate): option sistate := match i with @@ -485,9 +490,7 @@ Definition siexec_inst (i: instruction) (st: sistate): option sistate := let next := slocal_set_sreg prev dst (Sload prev.(si_smem) trap chunk addr vargs) in Some (sist_set_local st pc' next) | Istore chunk addr args src pc' => - let prev := st.(si_local) in - let vargs := list_sval_inj (List.map prev.(si_sreg) args) in - let next := slocal_set_smem prev (Sstore prev.(si_smem) chunk addr vargs (prev.(si_sreg) src)) in + let next := slocal_store st.(si_local) chunk addr args src in Some (sist_set_local st pc' next) | Icond cond args ifso ifnot _ => let prev := st.(si_local) in @@ -497,7 +500,6 @@ Definition siexec_inst (i: instruction) (st: sistate): option sistate := | _ => None (* TODO jumptable ? *) end. - Lemma seval_list_sval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs: (forall r : reg, seval_sval ge sp (sreg r) rs0 m0 = Some (rs # r)) -> seval_list_sval ge sp (list_sval_inj (map sreg l)) rs0 m0 = Some (rs ## l). @@ -1843,8 +1845,11 @@ Inductive sfval_simu (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node) opt_simu (seval_sval (the_ge1 ctx) (the_sp ctx) sv1 (the_rs0 ctx) (the_m0 ctx)) (seval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx)) -> sfval_simu dm f opc1 opc2 ctx (Sjumptable sv1 lpc1) (Sjumptable sv2 lpc2) - | Sreturn_simu os: - sfval_simu dm f opc1 opc2 ctx (Sreturn os) (Sreturn os). + | Sreturn_simu_none: sfval_simu dm f opc1 opc2 ctx (Sreturn None) (Sreturn None) + | Sreturn_simu_some sv1 sv2: + opt_simu (seval_sval (the_ge1 ctx) (the_sp ctx) sv1 (the_rs0 ctx) (the_m0 ctx)) + (seval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx)) -> + sfval_simu dm f opc1 opc2 ctx (Sreturn (Some sv1)) (Sreturn (Some sv2)). Definition sstate_simu dm f (s1 s2: sstate) (ctx: simu_proof_context f): Prop := sistate_simu dm f s1.(internal) s2.(internal) ctx @@ -1865,11 +1870,25 @@ Definition silocal_simu (dm: PTree.t node) (f: RTLpath.function) (sl1 sl2: sista exists is2, ssem_local (the_ge2 ctx) (the_sp ctx) sl2 (the_rs0 ctx) (the_m0 ctx) (irs is2) (imem is2) /\ istate_simu f dm is1 is2. +(* negation of sabort_local *) +Definition sok_local (ge: RTL.genv) (sp:val) (rs0: regset) (m0: mem) (st: sistate_local): Prop := + (st.(si_pre) ge sp rs0 m0) + /\ seval_smem ge sp st.(si_smem) rs0 m0 <> None + /\ forall (r: reg), seval_sval ge sp (si_sreg st r) rs0 m0 <> None. + +Lemma ssem_local_sok ge sp rs0 m0 st rs m: + ssem_local ge sp st rs0 m0 rs m -> sok_local ge sp rs0 m0 st. +Proof. + unfold sok_local, ssem_local. + intuition congruence. +Qed. + Definition siexit_simu (dm: PTree.t node) (f: RTLpath.function) (ctx: simu_proof_context f) (se1 se2: sistate_exit) := - (seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond se1) (si_scondargs se1) - (si_smem (si_elocal se1)) (the_rs0 ctx) (the_m0 ctx)) - = (seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond se2) (si_scondargs se2) - (si_smem (si_elocal se2)) (the_rs0 ctx) (the_m0 ctx)) + (sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1) -> + (seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond se1) (si_scondargs se1) + (si_smem (si_elocal se1)) (the_rs0 ctx) (the_m0 ctx)) = + (seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond se2) (si_scondargs se2) + (si_smem (si_elocal se2)) (the_rs0 ctx) (the_m0 ctx))) /\ forall is1, icontinue is1 = false -> ssem_exit (the_ge1 ctx) (the_sp ctx) se1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) (ipc is1) -> diff --git a/kvx/lib/RTLpathScheduler.v b/kvx/lib/RTLpathScheduler.v index b70c1685..0f099ce8 100644 --- a/kvx/lib/RTLpathScheduler.v +++ b/kvx/lib/RTLpathScheduler.v @@ -159,7 +159,6 @@ Definition verified_scheduler (f: RTLpath.function) : res (RTLpath.function * (P let tfr := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in do tf <- proj1_sig (function_builder tfr tpm); do tt <- function_equiv_checker dm f tf; -(* do _ <- injective_checker dm; *) OK (tf, dm). Theorem verified_scheduler_correct f tf dm: @@ -171,13 +170,12 @@ Theorem verified_scheduler_correct f tf dm: /\ (forall pc1 pc2, dm ! pc2 = Some pc1 -> path_entry (fn_path f) pc1) /\ (forall pc1 pc2, dm ! pc2 = Some pc1 -> path_entry (fn_path tf) pc2) /\ (forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2) -(* /\ is_injective dm *) . Proof. intros VERIF. unfold verified_scheduler in VERIF. explore. Local Hint Resolve function_equiv_checker_entrypoint function_equiv_checker_pathentry1 function_equiv_checker_pathentry2 - function_equiv_checker_correct (* injective_checker_correct *): core. + function_equiv_checker_correct: core. destruct (function_builder _ _) as [res H]; simpl in * |- *; auto. apply H in EQ2. rewrite EQ2. simpl. repeat (constructor; eauto). @@ -192,7 +190,6 @@ Record match_function (dupmap: PTree.t node) (f1 f2: RTLpath.function): Prop := dupmap_path_entry1: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f1) pc1; dupmap_path_entry2: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f2) pc2; dupmap_correct: forall pc1 pc2, dupmap!pc2 = Some pc1 -> sexec_simu dupmap f1 f2 pc1 pc2; -(* dupmap_injective: is_injective dupmap *) }. Program Definition transf_function (f: RTLpath.function): diff --git a/kvx/lib/RTLpathSchedulerproof.v b/kvx/lib/RTLpathSchedulerproof.v index 437f1e0a..e2344579 100644 --- a/kvx/lib/RTLpathSchedulerproof.v +++ b/kvx/lib/RTLpathSchedulerproof.v @@ -177,6 +177,23 @@ Proof. intros SEM X; eapply X; eauto. Qed. +Lemma seval_builtin_sval_preserved sp rs m: + forall bs, seval_builtin_sval ge sp bs rs m = seval_builtin_sval tge sp bs rs m. +Proof. + induction bs. + all: try (simpl; try reflexivity; erewrite seval_preserved by eapply symbols_preserved_RTL; reflexivity). + all: simpl; rewrite IHbs1; rewrite IHbs2; reflexivity. +Qed. + +Lemma seval_list_builtin_sval_preserved sp rs m: + forall lbs, + seval_list_builtin_sval ge sp lbs rs m = seval_list_builtin_sval tge sp lbs rs m. +Proof. + induction lbs; [simpl; reflexivity|]. + simpl. rewrite seval_builtin_sval_preserved. rewrite IHlbs. + reflexivity. +Qed. + Lemma ssem_final_simu dm f f' stk stk' sp st st' rs0 m0 sv sv' rs m t s (LIVE: liveness_ok_function f): match_function dm f f' -> @@ -216,7 +233,8 @@ Proof. 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 *) + intro. rewrite <- H0 by assumption. + erewrite seval_list_builtin_sval_preserved; eauto. + eapply external_call_symbols_preserved; eauto. + eapply eqlive_reg_refl. - (* Sjumptable *) @@ -228,10 +246,12 @@ Proof. + eapply eqlive_reg_refl. - (* Sreturn *) eexists; split; econstructor; eauto. + erewrite <- preserv_fnstacksize; eauto. + - (* Sreturn bis *) + eexists; split; econstructor; eauto. + erewrite <- preserv_fnstacksize; eauto. - + destruct os; auto. - erewrite <- seval_preserved; eauto. -Admitted. + + rewrite H by congruence. erewrite <- seval_preserved; eauto. +Qed. (* The main theorem on simulation of symbolic states ! *) Theorem ssem_sstate_simu dm f f' stk stk' sp st st' rs m t s: |