From f59ff208a301bf3f04aab350d9f0b3b217ddeac3 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 19 Jul 2021 14:20:53 +0200 Subject: Finish implem proof, need to adapt scheduler proof --- scheduling/BTL_SEimpl.v | 424 +++++++++++++++++++++++++++++----------- scheduling/BTL_Scheduler.v | 57 +++++- scheduling/BTL_Schedulerproof.v | 3 +- 3 files changed, 371 insertions(+), 113 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index b04c17fb..34f8eb1f 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -77,6 +77,30 @@ Definition smem_set_hid (sm: smem) (hid: hashcode): smem := | Sstore sm chunk addr lsv srce _ => Sstore sm chunk addr lsv srce hid end. +Lemma sval_set_hid_correct ctx x y: + sval_set_hid x unknown_hid = sval_set_hid y unknown_hid -> + sval_refines ctx x y. +Proof. + destruct x, y; intro H; inversion H; subst; simpl; auto. +Qed. +Local Hint Resolve sval_set_hid_correct: core. + +Lemma list_sval_set_hid_correct ctx x y: + list_sval_set_hid x unknown_hid = list_sval_set_hid y unknown_hid -> + list_sval_refines ctx x y. +Proof. + destruct x, y; intro H; inversion H; subst; simpl; auto. +Qed. +Local Hint Resolve list_sval_set_hid_correct: core. + +Lemma smem_set_hid_correct ctx x y: + smem_set_hid x unknown_hid = smem_set_hid y unknown_hid -> + smem_refines ctx x y. +Proof. + destruct x, y; intro H; inversion H; subst; simpl; auto. +Qed. +Local Hint Resolve smem_set_hid_correct: core. + (** Now, we build the hash-Cons value from a "hash_eq". Informal specification: @@ -474,7 +498,6 @@ Proof. - intros X; inversion REF. erewrite H1; eauto. Qed. -Global Opaque hrexec_store. Local Hint Resolve hrexec_store_correct: wlp. (** ** Assignment of registers *) @@ -788,7 +811,34 @@ Proof. rewrite ris_sreg_set_access. erewrite red_PTree_set_refines; intuition eauto. Qed. -Global Opaque hrs_sreg_set. + +Lemma hrs_ok_op_okpreserv ctx op args dest hrs: + WHEN hrs_sreg_set dest args (Rop op) hrs ~> rst THEN + ris_ok ctx rst -> ris_ok ctx hrs. +Proof. + wlp_simplify; inv H2 || inv H1; + simpl in *; econstructor; eauto. +Qed. + +Lemma hrs_ok_load_okpreserv ctx chunk addr args dest hrs: + WHEN hrs_sreg_set dest args (Rload TRAP chunk addr) hrs ~> rst THEN + ris_ok ctx rst -> ris_ok ctx hrs. +Proof. + wlp_simplify; inv H1; + simpl in *; econstructor; eauto. +Qed. + +Lemma hrs_ok_store_okpreserv ctx chunk addr args src hrs: + WHEN hrexec_store chunk addr args src hrs ~> rst THEN + ris_ok ctx rst -> ris_ok ctx hrs. +Proof. + unfold hrexec_store; wlp_simplify. + generalize H2. erewrite ok_rset_mem; intuition. + specialize H1 with (sm2 := hrs). + erewrite H1; eauto. rewrite H3. repeat autodestruct. +Qed. + +Global Opaque hrs_sreg_set hrexec_store. Local Hint Resolve hrs_sreg_set_correct: wlp. (* transfer *) @@ -800,6 +850,7 @@ Proof. split; destruct 1; econstructor; simpl in *; eauto. Qed. +(* TODO useless? Lemma hrset_red_reg_correct ctx r rsv sv hrs sis: ris_refines ctx hrs sis -> (ris_ok ctx hrs -> eval_sval ctx rsv <> None) -> @@ -814,50 +865,62 @@ Proof. erewrite red_PTree_set_refines; eauto. econstructor; eauto. Qed. + *) -Fixpoint transfer_hrs (inputs: list reg) (hrs: ristate): ristate := +Fixpoint transfer_hrs (inputs: list reg) (hrs: ristate): ?? ristate := match inputs with - | nil => {| ris_smem := hrs.(ris_smem); - ris_input_init := false; - ok_rsval := hrs.(ok_rsval); - ris_sreg:= PTree.empty _ - |} + | nil => RET {| ris_smem := hrs.(ris_smem); + ris_input_init := false; + ok_rsval := hrs.(ok_rsval); + ris_sreg:= PTree.empty _ + |} | r::l => - let hrs' := transfer_hrs l hrs in - ris_sreg_set hrs' (red_PTree_set r (ris_sreg_get hrs r) hrs') + DO hrs' <~ transfer_hrs l hrs;; + DO sv <~ hrs_sreg_get hrs r;; + RET (ris_sreg_set hrs' (red_PTree_set r sv hrs')) end. Lemma ok_transfer_hrs ctx inputs hrs: - ris_ok ctx (transfer_hrs inputs hrs) + WHEN transfer_hrs inputs hrs ~> hrs' THEN + ris_ok ctx hrs' <-> (ris_ok ctx hrs). Proof. - induction inputs as [|r l]; simpl. - + split; destruct 1; econstructor; simpl in *; intuition eauto. - + rewrite ok_hrset_red_sreg. auto. + induction inputs as [|r l]; simpl; wlp_simplify; + try (inv H; econstructor; eauto; fail). + + apply H0; rewrite <- ok_hrset_red_sreg; eauto. + + rewrite ok_hrset_red_sreg; auto. Qed. +Local Hint Resolve ok_transfer_hrs: wlp. Lemma transfer_hrs_correct ctx inputs hrs sis: + WHEN transfer_hrs inputs hrs ~> hrs' THEN ris_refines ctx hrs sis -> - ris_refines ctx (transfer_hrs inputs hrs) (transfer_sis inputs sis). + ris_refines ctx hrs' (transfer_sis inputs sis). Proof. - destruct 1; intros. - induction inputs as [|r l]. - + econstructor; eauto. - * erewrite ok_transfer_sis, ok_transfer_hrs; eauto. - * erewrite ok_transfer_hrs; eauto. - * erewrite ok_transfer_hrs; simpl; unfold ris_sreg_get; simpl; eauto. - intros; rewrite PTree.gempty. simpl; auto. - + econstructor; eauto. - * erewrite ok_transfer_sis, ok_transfer_hrs; eauto. - * erewrite ok_transfer_hrs; simpl. - intros; inversion IHl. erewrite MEM_EQ0. - - unfold transfer_sis; simpl; eauto. - - rewrite ok_transfer_hrs; simpl; eauto. - * erewrite ok_transfer_hrs; simpl. - intros H r0; inversion IHl. + unfold transfer_hrs; + induction inputs as [|r l]; wlp_simplify. + inversion H. + + constructor. + * erewrite ok_transfer_sis; split; intros X. + - constructor; simpl; rewrite OK_EQUIV in X; inv X; assumption. + - rewrite OK_EQUIV; constructor; inv X; assumption. + * intros X; inv X; simpl; apply MEM_EQ; constructor; auto. + * simpl. unfold ris_sreg_get. + intros;rewrite PTree.gempty. simpl; auto. + + constructor. + * erewrite ok_hrset_red_sreg; eauto. + inv H2. rewrite <- OK_EQUIV. + erewrite !ok_transfer_sis; reflexivity. + * intros X; inversion X; simpl in *. + rewrite ok_hrset_red_sreg in X. + inv H2; rewrite MEM_EQ; auto. + * simpl; intros X r0. inversion H2. + rewrite ok_hrset_red_sreg in X. erewrite red_PTree_set_refines; eauto. - - destruct (Pos.eq_dec); eauto. - - rewrite ok_transfer_hrs. auto. + destruct (Pos.eq_dec); auto. + inv H1. rewrite ok_transfer_sis in OK_EQUIV. + rewrite <- OK_EQUIV, OK_EQUIV0 in X. + erewrite H0; eauto. Qed. Definition tr_hrs := poly_tr (fun f tbl or => transfer_hrs (Regset.elements (pre_inputs f tbl or))). @@ -866,28 +929,140 @@ Local Hint Resolve transfer_hrs_correct ok_transfer_hrs: core. Local Opaque transfer_hrs. Lemma ok_tr_hrs ctx fi hrs: - ris_ok ctx (tr_hrs (cf ctx) fi hrs) + WHEN tr_hrs (cf ctx) fi hrs ~> hrs' THEN + ris_ok ctx hrs' <-> (ris_ok ctx hrs). Proof. destruct fi; simpl; eauto. Qed. -Lemma hrs_ok_tr_okpreserv ctx fi hrs: ris_ok ctx (tr_hrs (cf ctx) fi hrs) -> ris_ok ctx hrs. +Lemma tr_hrs_correct ctx fi hrs sis: + WHEN tr_hrs (cf ctx) fi hrs ~> hrs' THEN + ris_refines ctx hrs sis -> + ris_refines ctx hrs' (tr_sis (cf ctx) fi sis). Proof. - rewrite ok_tr_hrs; auto. + unfold tr_hrs, poly_tr; destruct fi; wlp_simplify; + exploit transfer_hrs_correct; eauto. + Unshelve. all: auto. Qed. -Lemma tr_hrs_correct ctx fi hrs sis: - ris_refines ctx hrs sis -> - ris_refines ctx (tr_hrs (cf ctx) fi hrs) (tr_sis (cf ctx) fi sis). +Fixpoint hbuiltin_arg (hrs: ristate) (arg : builtin_arg reg): ?? builtin_arg sval := + match arg with + | BA r => + DO v <~ hrs_sreg_get hrs r;; + RET (BA v) + | BA_int n => RET (BA_int n) + | BA_long n => RET (BA_long n) + | BA_float f0 => RET (BA_float f0) + | BA_single s => RET (BA_single s) + | BA_loadstack chunk ptr => RET (BA_loadstack chunk ptr) + | BA_addrstack ptr => RET (BA_addrstack ptr) + | BA_loadglobal chunk id ptr => RET (BA_loadglobal chunk id ptr) + | BA_addrglobal id ptr => RET (BA_addrglobal id ptr) + | BA_splitlong ba1 ba2 => + DO v1 <~ hbuiltin_arg hrs ba1;; + DO v2 <~ hbuiltin_arg hrs ba2;; + RET (BA_splitlong v1 v2) + | BA_addptr ba1 ba2 => + DO v1 <~ hbuiltin_arg hrs ba1;; + DO v2 <~ hbuiltin_arg hrs ba2;; + RET (BA_addptr v1 v2) + end. + +Lemma hbuiltin_arg_correct hrs arg: + WHEN hbuiltin_arg hrs arg ~> hargs THEN forall ctx (f: reg -> sval) + (RR: forall r, sval_refines ctx (hrs r) (f r)), + eval_builtin_sval ctx hargs = eval_builtin_sval ctx (builtin_arg_map f arg). Proof. - intros REF. rewrite <- tr_sis_alt_def. - destruct fi; simpl; eauto. + induction arg; wlp_simplify. + + erewrite H; eauto. + + erewrite H; eauto. + erewrite H0; eauto. + + erewrite H; eauto. + erewrite H0; eauto. +Qed. +Global Opaque hbuiltin_arg. +Local Hint Resolve hbuiltin_arg_correct: wlp. + +Fixpoint hbuiltin_args hrs (args: list (builtin_arg reg)): ?? list (builtin_arg sval) := + match args with + | nil => RET nil + | a::l => + DO ha <~ hbuiltin_arg hrs a;; + DO hl <~ hbuiltin_args hrs l;; + RET (ha::hl) + end. + +Lemma hbuiltin_args_correct hrs args: + WHEN hbuiltin_args hrs args ~> hargs THEN forall ctx (f: reg -> sval) + (RR: forall r, sval_refines ctx (hrs r) (f r)), + bargs_refines ctx hargs (List.map (builtin_arg_map f) args). +Proof. + unfold bargs_refines; induction args; wlp_simplify. + erewrite H; eauto. + erewrite H0; eauto. +Qed. +Global Opaque hbuiltin_args. +Local Hint Resolve hbuiltin_args_correct: wlp. + +Definition hsum_left hrs (ros: reg + ident): ?? (sval + ident) := + match ros with + | inl r => DO hr <~ hrs_sreg_get hrs r;; RET (inl hr) + | inr s => RET (inr s) + end. + +Lemma hsum_left_correct hrs ros: + WHEN hsum_left hrs ros ~> hsi THEN forall ctx (f: reg -> sval) + (RR: forall r, sval_refines ctx (hrs r) (f r)), + rsvident_refines ctx hsi (sum_left_map f ros). +Proof. + destruct ros; wlp_simplify; + econstructor; eauto. +Qed. +Global Opaque hsum_left. +Local Hint Resolve hsum_left_correct: wlp. + +(** * Symbolic execution of final step *) +Definition hrexec_final_sfv (i: final) hrs: ?? sfval := + match i with + | Bgoto pc => RET (Sgoto pc) + | Bcall sig ros args res pc => + DO svos <~ hsum_left hrs ros;; + DO sargs <~ hlist_args hrs args;; + RET (Scall sig svos sargs res pc) + | Btailcall sig ros args => + DO svos <~ hsum_left hrs ros;; + DO sargs <~ hlist_args hrs args;; + RET (Stailcall sig svos sargs) + | Bbuiltin ef args res pc => + DO sargs <~ hbuiltin_args hrs args;; + RET (Sbuiltin ef sargs res pc) + | Breturn or => + match or with + | Some r => DO hr <~ hrs_sreg_get hrs r;; RET (Sreturn (Some hr)) + | None => RET (Sreturn None) + end + | Bjumptable reg tbl => + DO sv <~ hrs_sreg_get hrs reg;; + RET (Sjumptable sv tbl) + end. + +Lemma hrexec_final_sfv_correct ctx fi hrs sis: + WHEN hrexec_final_sfv fi hrs ~> hrs' THEN forall + (REF: ris_refines ctx hrs sis) + (OK: ris_ok ctx hrs), + rfv_refines ctx hrs' (sexec_final_sfv fi sis). +Proof. + destruct fi; simpl; wlp_simplify; repeat econstructor; + try inversion REF; try erewrite H; eauto. Qed. Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate := match ib with - | BF fin _ => RET (Rfinal (tr_hrs f fin hrs) (sexec_final_sfv fin hrs)) + | BF fin _ => + DO sfv <~ hrexec_final_sfv fin hrs;; + DO hrs' <~ tr_hrs f fin hrs;; + RET (Rfinal hrs' sfv) (* basic instructions *) | Bnop _ => k hrs | Bop op args dst _ => @@ -916,7 +1091,7 @@ Definition hrexec f ib := DO init <~ hrs_init;; hrexec_rec f ib init (fun _ => RET Rabort). -Local Hint Resolve exec_final_refpreserv tr_hrs_correct hrs_ok_tr_okpreserv: core. +Local Hint Resolve exec_final_refpreserv ok_tr_hrs: core. Local Hint Constructors rst_refines: core. Lemma hrexec_rec_correct1 ctx ib: @@ -938,13 +1113,18 @@ Lemma hrexec_rec_correct1 ctx ib: rst_refines ctx rst st. Proof. induction ib; try (wlp_simplify; fail). + - (* BF *) + wlp_simplify; exploit tr_hrs_correct; eauto. + intros; constructor; auto. + intros X; apply H0 in X. + exploit hrexec_final_sfv_correct; eauto. - (* Bnop *) wlp_simplify; eapply CONT; eauto. - (* Bload *) destruct trap; wlp_simplify. - (* Bseq *) wlp_simplify. eapply IHib1. 3-7: eauto. + simpl. eapply sexec_rec_okpreserv; eauto. - + intros; subst. eapply IHib2; eauto. + + intros; eapply IHib2; eauto. - (* Bcond *) simpl; intros; wlp_simplify. assert (rOK: ris_ok ctx hrs). { @@ -954,9 +1134,11 @@ Proof. exploit (Refcond ctx cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1 (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k)); exploit H; eauto; intros (SEVAL & EQC); subst; auto. - all: simpl in SOUT; generalize SOUT; inversion_SOME b0; try_simplify_someHyps. - * intros; eapply IHib1; eauto. - * intros; eapply IHib2; eauto. + all: + simpl in SOUT; generalize SOUT; clear SOUT; + inversion_SOME b0; try_simplify_someHyps. + + intros; eapply IHib1; eauto. + + intros; eapply IHib2; eauto. Qed. Lemma hrexec_correct1 ctx ib sis sfv: @@ -969,23 +1151,80 @@ Proof. eapply hrexec_rec_correct1; eauto; simpl; congruence. Qed. -(*Lemma hrexec_rec_correct2 ctx ib: +Lemma hrexec_rec_okpreserv ctx ib: + forall k + (CONT: forall hrs lhrs rfv, + WHEN k hrs ~> rst THEN + get_routcome ctx rst = Some (rout lhrs rfv) -> + ris_ok ctx lhrs -> + ris_ok ctx hrs) + hrs lhrs rfv, + WHEN hrexec_rec (cf ctx) ib hrs k ~> rst THEN + get_routcome ctx rst = Some (rout lhrs rfv) -> + ris_ok ctx lhrs -> + ris_ok ctx hrs. +Proof. + induction ib; simpl; try (wlp_simplify; try_simplify_someHyps; fail). + - (* Bop *) + wlp_simplify; exploit hrs_ok_op_okpreserv; eauto. + - (* Bload *) + destruct trap; wlp_simplify; try_simplify_someHyps. + exploit hrs_ok_load_okpreserv; eauto. + - (* Bstore *) + wlp_simplify; exploit hrs_ok_store_okpreserv; eauto. + - (* Bcond *) + wlp_simplify; generalize H2; clear H2; inversion_SOME b; destruct b; try_simplify_someHyps. +Qed. +Local Hint Resolve hrexec_rec_okpreserv: wlp. + +Lemma hrexec_rec_correct2 ctx ib: forall rk k - (CONTh: forall ris lris rfv, get_routcome ctx (rk ris) = Some (rout lris rfv) -> ris_ok ctx lris -> ris_ok ctx ris) - (CONT: forall ris sis lris rfv st, - ris_refines ctx ris sis -> - rk ris = st -> - get_routcome ctx (rk ris) = Some (rout lris rfv) -> - ris_ok ctx lris -> - rst_refines ctx (rk ris) (k sis)) - ris sis lris rfv st - (REF: ris_refines ctx ris sis) - (EXEC: rexec_rec (cf ctx) ib ris rk = st) - (SOUT: get_routcome ctx st = Some (rout lris rfv)) - (OK: ris_ok ctx lris) - , rst_refines ctx st (sexec_rec (cf ctx) ib sis k). + (CONTh: forall hrs lhrs rfv, + WHEN rk hrs ~> rst THEN + get_routcome ctx rst = Some (rout lhrs rfv) -> + ris_ok ctx lhrs -> + ris_ok ctx hrs) + (CONT: forall hrs sis lhrs rfv, + ris_refines ctx hrs sis -> + WHEN rk hrs ~> rst THEN + get_routcome ctx rst = Some (rout lhrs rfv) -> + ris_ok ctx lhrs -> + rst_refines ctx rst (k sis)) + hrs sis lhrs rfv + (REF: ris_refines ctx hrs sis), + WHEN hrexec_rec (cf ctx) ib hrs rk ~> rst THEN + get_routcome ctx rst = Some (rout lhrs rfv) -> + ris_ok ctx lhrs -> + rst_refines ctx rst (sexec_rec (cf ctx) ib sis k). Proof. - Admitted.*) + induction ib; try (wlp_simplify; fail). + - (* BF *) + wlp_simplify; exploit tr_hrs_correct; eauto. + intros; constructor; auto. + intros X; apply H0 in X. + exploit hrexec_final_sfv_correct; eauto. + - (* Bnop *) wlp_simplify; eapply CONT; eauto. + - (* Bload *) destruct trap; wlp_simplify. + - (* Bseq *) + wlp_simplify. + eapply IHib1. 3-6: eauto. + + simpl; eapply hrexec_rec_okpreserv; eauto. + + intros; eapply IHib2; eauto. + - (* Bcond *) + simpl; intros; wlp_simplify. + assert (rOK: ris_ok ctx hrs). { + simpl in H2; generalize H2; inversion_SOME b0; destruct b0; try_simplify_someHyps. + } + exploit (Refcond ctx cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1 + (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k)); + exploit H; eauto; intros (SEVAL & EQC); subst; auto. + all: + simpl in H2; generalize H2; clear H2; + inversion_SOME b0; try_simplify_someHyps. + + intros; eapply IHib1; eauto. + + intros; eapply IHib2; eauto. + Unshelve. all: auto. +Qed. Lemma hrexec_correct2 ctx ib hrs rfv: WHEN hrexec (cf ctx) ib ~> rst THEN @@ -993,44 +1232,15 @@ Lemma hrexec_correct2 ctx ib hrs rfv: (ris_ok ctx hrs) -> rst_refines ctx rst (sexec (cf ctx) ib). Proof. -Admitted. - -Lemma hrexec_correct_aux ctx ib: - WHEN hrexec (cf ctx) ib ~> rst THEN - exists st, sexec (cf ctx) ib = st /\ rst_refines ctx rst st. -Proof. - unfold hrexec; wlp_simplify. - repeat eexists. -Admitted. + unfold hrexec; intros; wlp_simplify. + eapply hrexec_rec_correct2; eauto; simpl; + wlp_simplify; congruence. +Qed. Global Opaque hrexec. End CanonBuilding. -(** Correction of concrete symbolic execution wrt abstract symbolic execution *) -Theorem hrexec_correct - (hC_hsval : hashinfo sval -> ?? sval) - (hC_list_hsval : hashinfo list_sval -> ?? list_sval) - (hC_hsmem : hashinfo smem -> ?? smem) - (ctx: iblock_exec_context) - (ib: iblock): - WHEN hrexec hC_hsval hC_list_hsval hC_hsmem (cf ctx) ib ~> hrs THEN forall - (hC_hsval_correct: forall hs, - WHEN hC_hsval hs ~> hs' THEN forall ctx, - sval_refines ctx (hdata hs) hs') - (hC_list_hsval_correct: forall lh, - WHEN hC_list_hsval lh ~> lh' THEN forall ctx, - list_sval_refines ctx (hdata lh) lh') - (hC_hsmem_correct: forall hm, - WHEN hC_hsmem hm ~> hm' THEN forall ctx, - smem_refines ctx (hdata hm) hm'), - exists st : sstate, sexec (cf ctx) ib = st /\ rst_refines ctx hrs st. -Proof. - wlp_simplify. - eapply hrexec_correct_aux; eauto. -Qed. -Local Hint Resolve hrexec_correct: wlp. - (** * Implementing the simulation test with concrete hash-consed symbolic execution *) Definition phys_check {A} (x y:A) (msg: pstring): ?? unit := @@ -1267,34 +1477,30 @@ Lemma simu_check_single_correct (f1 f2: function) (ib1 ib2: iblock): symbolic_simu f1 f2 ib1 ib2. Proof. (* TODO *) unfold symbolic_simu; wlp_simplify. - exploit hrexec_correct; eauto. eapply rst_simu_correct; eauto. - + intros; eapply hrexec_correct1; eauto. - 1-3: wlp_simplify. intuition eauto. - simpl. eauto. - intuition eauto. - admit. -Admitted. + + intros; eapply hrexec_correct1; eauto; wlp_simplify. + + intros; eapply hrexec_correct2; eauto; wlp_simplify. +Qed. Global Opaque simu_check_single. Global Hint Resolve simu_check_single_correct: wlp. -Program Definition aux_simu_check (f1 f2: function) (ib1 ib2: iblock): ?? bool := +Program Definition aux_simu_check (f1 f2: function) (ibf1 ibf2: iblock_info): ?? bool := DO r <~ (TRY - simu_check_single f1 f2 ib1 ib2;; + simu_check_single f1 f2 ibf1.(entry) ibf2.(entry);; RET true CATCH_FAIL s, _ => println ("simu_check_failure:" +; s);; RET false - ENSURE (fun b => b=true -> symbolic_simu f1 f2 ib1 ib2));; + ENSURE (fun b => b=true -> ibf1.(input_regs) = ibf2.(input_regs) -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry)));; RET (`r). Obligation 1. split; wlp_simplify. discriminate. Qed. -Lemma aux_simu_check_correct (f1 f2: function) (ib1 ib2: iblock): - WHEN aux_simu_check f1 f2 ib1 ib2 ~> b THEN - b=true -> symbolic_simu f1 f2 ib1 ib2. +Lemma aux_simu_check_correct (f1 f2: function) (ibf1 ibf2: iblock_info): + WHEN aux_simu_check f1 f2 ibf1 ibf2 ~> b THEN + b=true -> ibf1.(input_regs) = ibf2.(input_regs) -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry). Proof. unfold aux_simu_check; wlp_simplify. destruct exta; simpl; auto. @@ -1304,8 +1510,8 @@ Qed. Import UnsafeImpure. -Definition simu_check (f1 f2: function) (ib1 ib2: iblock): res unit := - match unsafe_coerce (aux_simu_check f1 f2 ib1 ib2) with +Definition simu_check (f1 f2: function) (ibf1 ibf2: iblock_info): res unit := + match unsafe_coerce (aux_simu_check f1 f2 ibf1 ibf2) with | Some true => OK tt | _ => Error (msg "simu_check has failed") end. diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index 12840f62..63114125 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -2,7 +2,7 @@ Require Import Coqlib Maps. Require Import AST Integers Values Events Memory Globalenvs Smallstep. Require Import RTL Op Registers OptionMonad BTL. -Require Import Errors Linking BTL_SEtheory. +Require Import Errors Linking BTL_SEtheory BTL_SEimpl. (** External oracle *) Axiom scheduler: BTL.function -> BTL.code. @@ -48,18 +48,69 @@ Record match_function (f1 f2: BTL.function): Prop := { Local Open Scope error_monad_scope. -Definition check_symbolic_simu (f tf: BTL.function): res unit := OK tt. (* TODO: fixme *) +Fixpoint check_symbolic_simu_rec (f1 f2: BTL.function) (lpc: list node): res unit := + match lpc with + | nil => OK tt + | pc :: lpc' => + match (fn_code f1)!pc, (fn_code f2)!pc with + | Some ibf1, Some ibf2 => + do _ <- simu_check f1 f2 ibf1 ibf2; + check_symbolic_simu_rec f1 f2 lpc' + | _, _ => Error (msg "check_symbolic_simu_rec: code tree mismatch") + end + end. + +Definition check_symbolic_simu (f1 f2: BTL.function): res unit := + check_symbolic_simu_rec f1 f2 (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))). + +Lemma check_symbolic_simu_rec_input_equiv lpc: forall f1 f2 x, + check_symbolic_simu_rec f1 f2 lpc = OK x -> + lpc = (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))) -> + equiv_input_regs f1 f2. +Proof. +Admitted. +(* + unfold equiv_input_regs; induction lpc; simpl; intros f1 f2 x X EQL1. + - destruct (map _ _) eqn:EQL2; inv X; intuition; + symmetry in EQL1; apply map_eq_nil in EQL1; apply map_eq_nil in EQL2. + + destruct (fn_code f1), (fn_code f2); simpl in *; auto. + inv EQL2. + unfold PTree.elements in EQL1. + + admit. + + + destruct ((fn_code f1) ! a), ((fn_code f2) ! a); monadInv X. + eapply IHlpc; eauto. +Qed. + *) Lemma check_symbolic_simu_input_equiv x f1 f2: check_symbolic_simu f1 f2 = OK x -> equiv_input_regs f1 f2. +Proof. + unfold check_symbolic_simu; simpl; intros X. + eapply check_symbolic_simu_rec_input_equiv; eauto. +Qed. + +Lemma check_symbolic_simu_rec_correct lpc: forall f1 f2 x, + check_symbolic_simu_rec f1 f2 lpc = OK x -> + forall pc ib1, (fn_code f1)!pc = Some ib1 -> + exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2). Proof. Admitted. + (* + induction lpc; simpl; intros f1 f2 x X pc ib1 PC; try (inv X; fail). + destruct ((fn_code f1) ! pc), ((fn_code f2) ! pc); inv X. + eapply IHlpc; eauto. +Qed. + *) Lemma check_symbolic_simu_correct x f1 f2: check_symbolic_simu f1 f2 = OK x -> forall pc ib1, (fn_code f1)!pc = Some ib1 -> exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2). -Admitted. +Proof. + unfold check_symbolic_simu; intros X pc ib1 PC. + eapply check_symbolic_simu_rec_correct; eauto. +Qed. Definition transf_function (f: BTL.function) := let tf := BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) (scheduler f) (fn_entrypoint f) in diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v index 95363194..91e650e8 100644 --- a/scheduling/BTL_Schedulerproof.v +++ b/scheduling/BTL_Schedulerproof.v @@ -105,11 +105,12 @@ Lemma transf_fundef_correct f f': transf_fundef f = OK f' -> match_fundef f f'. Proof. intros TRANSF; destruct f; simpl; inv TRANSF. +Admitted. (* + exploit transf_function_correct; eauto. econstructor. intros MATCH_F. eapply match_Internal; eauto. + eapply match_External. -Qed. + Qed.*) Lemma function_ptr_preserved: forall v f, -- cgit