From a9c90fe3354f65340283dc79431bc6915ed1ad90 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Jul 2021 10:17:46 +0200 Subject: proof for symbolic simu, need to finish equiv_inputs --- scheduling/BTL_SEimpl.v | 29 +++++++++++++++++++---------- scheduling/BTL_Scheduler.v | 17 +++++++++-------- scheduling/BTL_Schedulerproof.v | 8 +++----- 3 files changed, 31 insertions(+), 23 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index 34f8eb1f..d6cdff59 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -1459,22 +1459,21 @@ Qed. Hint Resolve rst_simu_check_correct: wlp. Global Opaque rst_simu_check. -(* TODO do we really need both functions *) -Definition simu_check_single (f1 f2: function) (ib1 ib2: iblock): ?? unit := +Definition simu_check_single (f1 f2: function) (ibf1 ibf2: iblock_info): ?? unit := (* creating the hash-consing tables *) DO hC_sval <~ hCons hSVAL;; DO hC_list_hsval <~ hCons hLSVAL;; DO hC_hsmem <~ hCons hSMEM;; let hrexec := hrexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in (* performing the hash-consed executions *) - DO hst1 <~ hrexec f1 ib1;; - DO hst2 <~ hrexec f2 ib2;; + DO hst1 <~ hrexec f1 ibf1.(entry);; + DO hst2 <~ hrexec f2 ibf2.(entry);; (* comparing the executions *) rst_simu_check hst1 hst2. -Lemma simu_check_single_correct (f1 f2: function) (ib1 ib2: iblock): - WHEN simu_check_single f1 f2 ib1 ib2 ~> _ THEN - symbolic_simu f1 f2 ib1 ib2. +Lemma simu_check_single_correct (f1 f2: function) (ibf1 ibf2: iblock_info): + WHEN simu_check_single f1 f2 ibf1 ibf2 ~> _ THEN + symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry). Proof. (* TODO *) unfold symbolic_simu; wlp_simplify. eapply rst_simu_correct; eauto. @@ -1487,12 +1486,12 @@ Global Hint Resolve simu_check_single_correct: wlp. Program Definition aux_simu_check (f1 f2: function) (ibf1 ibf2: iblock_info): ?? bool := DO r <~ (TRY - simu_check_single f1 f2 ibf1.(entry) ibf2.(entry);; + simu_check_single f1 f2 ibf1 ibf2;; RET true CATCH_FAIL s, _ => println ("simu_check_failure:" +; s);; RET false - ENSURE (fun b => b=true -> ibf1.(input_regs) = ibf2.(input_regs) -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry)));; + ENSURE (fun b => b=true -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry)));; RET (`r). Obligation 1. split; wlp_simplify. discriminate. @@ -1500,7 +1499,7 @@ Qed. 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). + b=true -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry). Proof. unfold aux_simu_check; wlp_simplify. destruct exta; simpl; auto. @@ -1515,3 +1514,13 @@ Definition simu_check (f1 f2: function) (ibf1 ibf2: iblock_info): res unit := | Some true => OK tt | _ => Error (msg "simu_check has failed") end. + +Lemma simu_check_correct f1 f2 ibf1 ibf2: + simu_check f1 f2 ibf1 ibf2 = OK tt -> + symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry). +Proof. + unfold simu_check. + destruct (unsafe_coerce (aux_simu_check f1 f2 ibf1 ibf2)) as [[|]|] eqn:Hres; simpl; try discriminate. + intros; eapply aux_simu_check_correct; eauto. + eapply unsafe_coerce_not_really_correct; eauto. +Qed. diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index 63114125..e7d2b37f 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -92,16 +92,16 @@ 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 -> + forall pc ib1, (fn_code f1)!pc = Some ib1 /\ In pc lpc -> 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. + induction lpc; simpl; intros f1 f2 x X pc ib1 (PC & HIN); try contradiction. + destruct HIN; subst. + - rewrite PC in X; destruct ((fn_code f2)!pc); monadInv X. + exists i; split; auto. destruct x0. eapply simu_check_correct; eauto. + - destruct ((fn_code f1)!a), ((fn_code f2)!a); monadInv X. + eapply IHlpc; eauto. Qed. - *) Lemma check_symbolic_simu_correct x f1 f2: check_symbolic_simu f1 f2 = OK x -> @@ -109,7 +109,8 @@ Lemma check_symbolic_simu_correct x f1 f2: exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2). Proof. unfold check_symbolic_simu; intros X pc ib1 PC. - eapply check_symbolic_simu_rec_correct; eauto. + eapply check_symbolic_simu_rec_correct; intuition eauto. + apply PTree.elements_correct in PC. eapply (in_map fst) in PC; auto. Qed. Definition transf_function (f: BTL.function) := diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v index 91e650e8..05028f11 100644 --- a/scheduling/BTL_Schedulerproof.v +++ b/scheduling/BTL_Schedulerproof.v @@ -105,12 +105,10 @@ 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. + + monadInv H0. exploit transf_function_correct; eauto. + constructor; auto. + eapply match_External. - Qed.*) +Qed. Lemma function_ptr_preserved: forall v f, -- cgit