From 0746cadf3bcdcbd3977c52e59352e5e7316b31d2 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 6 Jul 2021 11:45:52 +0200 Subject: Some advance, need to finish canonbuilding proofs --- scheduling/BTL_SEimpl.v | 283 +++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 270 insertions(+), 13 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index 6e86bebb..8f7881a5 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -1,6 +1,6 @@ Require Import Coqlib AST Maps. Require Import Op Registers. -Require Import RTL BTL. +Require Import RTL BTL Errors. Require Import BTL_SEsimuref BTL_SEtheory OptionMonad. Require Import Impure.ImpHCons. @@ -77,6 +77,95 @@ Definition smem_set_hid (sm: smem) (hid: hashcode): smem := | Sstore sm chunk addr lsv srce _ => Sstore sm chunk addr lsv 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. + + 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 sval_hash_eq (sv1 sv2: sval): ?? bool := + match sv1, sv2 with + | Sinput r1 _, Sinput r2 _ => struct_eq r1 r2 (* NB: really need a struct_eq here ? *) + | Sop op1 lsv1 _, Sop op2 lsv2 _ => + DO b1 <~ phys_eq lsv1 lsv2;; + if b1 + then struct_eq op1 op2 (* NB: really need a struct_eq here ? *) + else RET false + | Sload sm1 trap1 chk1 addr1 lsv1 _, Sload sm2 trap2 chk2 addr2 lsv2 _ => + DO b1 <~ phys_eq lsv1 lsv2;; + DO b2 <~ phys_eq sm1 sm2;; + DO b3 <~ struct_eq trap1 trap2;; + DO b4 <~ struct_eq chk1 chk2;; + if b1 && b2 && b3 && b4 + then struct_eq addr1 addr2 + else RET false + | _,_ => RET false + end. + +Lemma and_true_split a b: a && b = true <-> a = true /\ b = true. +Proof. + destruct a; simpl; intuition. +Qed. + +Lemma sval_hash_eq_correct x y: + WHEN sval_hash_eq x y ~> b THEN + b = true -> sval_set_hid x unknown_hid = sval_set_hid y unknown_hid. +Proof. + destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence. +Qed. +Global Opaque sval_hash_eq. +Local Hint Resolve sval_hash_eq_correct: wlp. + +Definition list_sval_hash_eq (lsv1 lsv2: list_sval): ?? bool := + match lsv1, lsv2 with + | Snil _, Snil _ => RET true + | Scons sv1 lsv1' _, Scons sv2 lsv2' _ => + DO b <~ phys_eq lsv1' lsv2';; + if b + then phys_eq sv1 sv2 + else RET false + | _,_ => RET false + end. + +Lemma list_sval_hash_eq_correct x y: + WHEN list_sval_hash_eq x y ~> b THEN + b = true -> list_sval_set_hid x unknown_hid = list_sval_set_hid y unknown_hid. +Proof. + destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence. +Qed. +Global Opaque list_sval_hash_eq. +Local Hint Resolve list_sval_hash_eq_correct: wlp. + +Definition smem_hash_eq (sm1 sm2: smem): ?? bool := + match sm1, sm2 with + | Sinit _, Sinit _ => RET true + | Sstore sm1 chk1 addr1 lsv1 sv1 _, Sstore sm2 chk2 addr2 lsv2 sv2 _ => + DO b1 <~ phys_eq lsv1 lsv2;; + DO b2 <~ phys_eq sm1 sm2;; + DO b3 <~ phys_eq sv1 sv2;; + DO b4 <~ struct_eq chk1 chk2;; + if b1 && b2 && b3 && b4 + then struct_eq addr1 addr2 + else RET false + | _,_ => RET false + end. + +Lemma smem_hash_eq_correct x y: + WHEN smem_hash_eq x y ~> b THEN + b = true -> smem_set_hid x unknown_hid = smem_set_hid y unknown_hid. +Proof. + destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence. +Qed. +Global Opaque smem_hash_eq. +Local Hint Resolve smem_hash_eq_correct: wlp. + +Definition hSVAL: hashP sval := {| hash_eq := sval_hash_eq; get_hid:=sval_get_hid; set_hid:=sval_set_hid |}. +Definition hLSVAL: hashP list_sval := {| hash_eq := list_sval_hash_eq; get_hid:= list_sval_get_hid; set_hid:= list_sval_set_hid |}. +Definition hSMEM: hashP smem := {| hash_eq := smem_hash_eq; get_hid:= smem_get_hid; set_hid:= smem_set_hid |}. + (** * Implementation of symbolic execution *) Section CanonBuilding. @@ -465,7 +554,7 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval := DO lsv <~ hlist_args hrs lr;; hSop op lsv (* TODO gourdinl - match target_op_simplify op lr hst with + match target_op_simplify op lr hrs with | Some fhv => fsval_proj fhv | None => hSop op lhsv @@ -715,16 +804,184 @@ Definition hrexec f ib := DO init <~ hris_init;; hrexec_rec f ib init (fun _ => RET Rabort). -Definition hsexec (f: function) (pc:node): ?? rstate := - DO path <~ some_or_fail ((fn_code f)!pc) "hsexec.internal_error.1";; - (*DO hinit <~ init_ristate;;*) - DO hst <~ hrexec f f.(fn_entrypoint);; - 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. +Lemma hrexec_rec_correct1 ctx ib: + forall rk k + (CONTh: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> si_ok ctx sis) + (CONT: forall hrs sis lsis sfv st, + ris_refines ctx hrs sis -> + k sis = st -> + get_soutcome ctx (k sis) = Some (sout lsis sfv) -> + si_ok ctx lsis -> + WHEN rk hrs ~> ris' THEN + rst_refines ctx ris' (k sis)) + hrs sis lsis sfv st + (REF: ris_refines ctx hrs sis) + (EXEC: sexec_rec (cf ctx) ib sis k = st) + (SOUT: get_soutcome ctx st = Some (sout lsis sfv)) + (OK: si_ok ctx lsis), + WHEN hrexec_rec (cf ctx) ib hrs rk ~> hrs THEN + rst_refines ctx hrs st. +Proof. + (* + induction ib; wlp_simplify. + - admit. + - eapply CONT; eauto. + - try_simplify_someHyps. intros OUT. + eapply CONT; eauto. + intuition eauto. + econstructor; intuition eauto. + inv REF. inv H2. + intuition eauto. + + + - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto. + - (* seq *) + intros; subst. + eapply IHib1. 3-6: eauto. + + simpl. eapply sexec_rec_okpreserv; eauto. + + intros; subst. eapply IHib2; eauto. + - (* cond *) + intros rk k CONTh CONT hrs sis lsis sfv st REF EXEC OUT OK. subst. + assert (rOK: ris_ok ctx hrs). { + erewrite <- OK_EQUIV. 2: eauto. + eapply sexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. + } + generalize OUT; clear OUT; simpl. + autodestruct. + intros COND; generalize COND. + erewrite <- eval_scondition_refpreserv; eauto. + econstructor; try_simplify_someHyps. + Qed.*) +Admitted. + +Definition hsexec (f: function) ib: ?? rstate := + hrexec f ib. End CanonBuilding. + +(** * Implementing the simulation test with concrete hash-consed symbolic execution *) + +Definition phys_check {A} (x y:A) (msg: pstring): ?? unit := + DO b <~ phys_eq x y;; + assert_b b msg;; + RET tt. + +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 ~> _ THEN + a = b. +Proof. wlp_simplify. Qed. +Global Opaque struct_check. +Hint Resolve struct_check_correct: wlp. + +Definition sfval_simu_check (sfv1 sfv2: sfval) := RET tt. + +Fixpoint rst_simu_check (rst1 rst2: rstate) := + match rst1, rst2 with + | Rfinal ris1 sfv1, Rfinal ris2 sfv2 => + sfval_simu_check sfv1 sfv2 + | Rcond cond1 lsv1 rsL1 rsR1, Rcond cond2 lsv2 rsL2 rsR2 => + struct_check cond1 cond2 "hsstate_simu_check: conditions do not match";; + phys_check lsv1 lsv2 "hsstate_simu_check: args do not match";; + rst_simu_check rsL1 rsL2;; + rst_simu_check rsR1 rsR2 + | _, _ => FAILWITH "hsstate_simu_check: simu_check failed" + end. + +Lemma rst_simu_check_correct rst1 rst2: + WHEN rst_simu_check rst1 rst2 ~> _ THEN + rst_simu rst1 rst2. +Proof. + induction rst1, rst2; + wlp_simplify. +Admitted. +Hint Resolve rst_simu_check_correct: wlp. +Global Opaque rst_simu_check. + +Definition simu_check_single (f1 f2: function) (ib1 ib2: iblock): ?? (option (node * node)) := + (* creating the hash-consing tables *) + DO hC_sval <~ hCons hSVAL;; + DO hC_list_hsval <~ hCons hLSVAL;; + DO hC_hsmem <~ hCons hSMEM;; + let hsexec := hsexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in + (* performing the hash-consed executions *) + DO hst1 <~ hsexec f1 ib1;; + DO hst2 <~ hsexec f2 ib2;; + (* 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. +Proof. +Admitted. +Global Opaque simu_check_single. +Global Hint Resolve simu_check_single_correct: wlp. + +Fixpoint simu_check_rec (f1 f2: function) (ibf1 ibf2: iblock_info): ?? unit := + DO res <~ simu_check_single f1 f2 ibf1.(entry) ibf2.(entry);; + let (pc1', pc2') := res in + simu_check_rec pc1' pc2'. + +Lemma simu_check_rec_correct dm f tf lm: + WHEN simu_check_rec dm f tf lm ~> _ THEN + forall pc1 pc2, In (pc2, pc1) lm -> sexec_simu dm f tf pc1 pc2. +Proof. + induction lm; wlp_simplify. + match goal with + | X: (_,_) = (_,_) |- _ => inversion X; subst + end. + subst; eauto. +Qed. +Global Opaque simu_check_rec. +Global Hint Resolve simu_check_rec_correct: wlp. + +Definition imp_simu_check (f tf: function): ?? unit := + simu_check_rec f tf ;; + DEBUG("simu_check OK!"). + +Local Hint Resolve PTree.elements_correct: core. +Lemma imp_simu_check_correct f tf: + WHEN imp_simu_check f tf ~> _ THEN + forall sexec_simu f tf. +Proof. + wlp_simplify. +Qed. +Global Opaque imp_simu_check. +Global Hint Resolve imp_simu_check_correct: wlp. + +Program Definition aux_simu_check (f tf: function): ?? bool := + DO r <~ + (TRY + imp_simu_check f tf;; + RET true + CATCH_FAIL s, _ => + println ("simu_check_failure:" +; s);; + RET false + ENSURE (sexec_simu f tf));; + RET (`r). +Obligation 1. + split; wlp_simplify. discriminate. +Qed. + +Lemma aux_simu_check_correct f tf: + WHEN aux_simu_check f tf ~> b THEN + sexec_simu f tf. +Proof. + unfold aux_simu_check; wlp_simplify. + destruct exta; simpl; auto. +Qed. + +(* Coerce aux_simu_check into a pure function (this is a little unsafe like all oracles in CompCert). *) + +Import UnsafeImpure. + +Definition simu_check (f tf: function) : res unit := + match unsafe_coerce (aux_simu_check f tf) with + | Some true => OK tt + | _ => Error (msg "simu_check has failed") + end. -- cgit