From 8bcada5be5fc93c5526d6381b5d034558e48de03 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 7 Jul 2021 09:58:49 +0200 Subject: progress in simulation test --- scheduling/BTL_SEimpl.v | 307 +++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 250 insertions(+), 57 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index 8f7881a5..94d7375d 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -166,6 +166,17 @@ Definition hSVAL: hashP sval := {| hash_eq := sval_hash_eq; get_hid:=sval_get_hi 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 |}. +Program Definition mk_hash_params: Dict.hash_params sval := + {| + Dict.test_eq := phys_eq; + Dict.hashing := fun (sv: sval) => RET (sval_get_hid sv); + Dict.log := fun sv => + DO sv_name <~ string_of_hashcode (sval_get_hid sv);; + println ("unexpected undef behavior of hashcode:" +; (CamlStr sv_name)) |}. +Obligation 1. + wlp_simplify. +Qed. + (** * Implementation of symbolic execution *) Section CanonBuilding. @@ -194,17 +205,17 @@ Definition undef_code := 4. Definition hSinput_hcodes (r: reg) := DO hc <~ hash reg_hcode;; - DO hv <~ hash r;; - RET [hc;hv]. + DO sv <~ hash r;; + RET [hc;sv]. Extraction Inline hSinput_hcodes. Definition hSinput (r:reg): ?? sval := - DO hv <~ hSinput_hcodes r;; - hC_sval {| hdata:=Sinput r unknown_hid; hcodes :=hv; |}. + DO sv <~ hSinput_hcodes r;; + hC_sval {| hdata:=Sinput r unknown_hid; hcodes :=sv; |}. Lemma hSinput_correct r: - WHEN hSinput r ~> hv THEN forall ctx, - sval_refines ctx hv (Sinput r unknown_hid). + WHEN hSinput r ~> sv THEN forall ctx, + sval_refines ctx sv (Sinput r unknown_hid). Proof. wlp_simplify. Qed. @@ -213,17 +224,17 @@ Local Hint Resolve hSinput_correct: wlp. Definition hSop_hcodes (op:operation) (lsv: list_sval) := DO hc <~ hash op_hcode;; - DO hv <~ hash op;; - RET [hc;hv;list_sval_get_hid lsv]. + DO sv <~ hash op;; + RET [hc;sv;list_sval_get_hid lsv]. Extraction Inline hSop_hcodes. Definition hSop (op:operation) (lsv: list_sval): ?? sval := - DO hv <~ hSop_hcodes op lsv;; - hC_sval {| hdata:=Sop op lsv unknown_hid; hcodes :=hv |}. + DO sv <~ hSop_hcodes op lsv;; + hC_sval {| hdata:=Sop op lsv unknown_hid; hcodes :=sv |}. Lemma hSop_fSop_correct op lsv: - WHEN hSop op lsv ~> hv THEN forall ctx, - sval_refines ctx hv (fSop op lsv). + WHEN hSop op lsv ~> sv THEN forall ctx, + sval_refines ctx sv (fSop op lsv). Proof. wlp_simplify. Qed. @@ -231,9 +242,9 @@ Global Opaque hSop. Local Hint Resolve hSop_fSop_correct: wlp_raw. Lemma hSop_correct op lsv1: - WHEN hSop op lsv1 ~> hv THEN forall ctx lsv2 + WHEN hSop op lsv1 ~> sv THEN forall ctx lsv2 (LR: list_sval_refines ctx lsv1 lsv2), - sval_refines ctx hv (Sop op lsv2 unknown_hid). + sval_refines ctx sv (Sop op lsv2 unknown_hid). Proof. wlp_xsimplify ltac:(intuition eauto with wlp wlp_raw). rewrite <- LR. erewrite H; eauto. @@ -242,21 +253,21 @@ Local Hint Resolve hSop_correct: wlp. Definition hSload_hcodes (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval):= DO hc <~ hash load_hcode;; - DO hv1 <~ hash trap;; - DO hv2 <~ hash chunk;; - DO hv3 <~ hash addr;; - RET [hc; smem_get_hid sm; hv1; hv2; hv3; list_sval_get_hid lsv]. + DO sv1 <~ hash trap;; + DO sv2 <~ hash chunk;; + DO sv3 <~ hash addr;; + RET [hc; smem_get_hid sm; sv1; sv2; sv3; list_sval_get_hid lsv]. Extraction Inline hSload_hcodes. Definition hSload (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval): ?? sval := - DO hv <~ hSload_hcodes sm trap chunk addr lsv;; - hC_sval {| hdata := Sload sm trap chunk addr lsv unknown_hid; hcodes := hv |}. + DO sv <~ hSload_hcodes sm trap chunk addr lsv;; + hC_sval {| hdata := Sload sm trap chunk addr lsv unknown_hid; hcodes := sv |}. Lemma hSload_correct sm1 trap chunk addr lsv1: - WHEN hSload sm1 trap chunk addr lsv1 ~> hv THEN forall ctx lsv2 sm2 + WHEN hSload sm1 trap chunk addr lsv1 ~> sv THEN forall ctx lsv2 sm2 (LR: list_sval_refines ctx lsv1 lsv2) (MR: smem_refines ctx sm1 sm2), - sval_refines ctx hv (Sload sm2 trap chunk addr lsv2 unknown_hid). + sval_refines ctx sv (Sload sm2 trap chunk addr lsv2 unknown_hid). Proof. wlp_simplify. rewrite <- LR, <- MR. @@ -271,12 +282,12 @@ Definition hSundef_hcodes := Extraction Inline hSundef_hcodes. Definition hSundef : ?? sval := - DO hv <~ hSundef_hcodes;; - hC_sval {| hdata:=Sundef unknown_hid; hcodes :=hv; |}. + DO sv <~ hSundef_hcodes;; + hC_sval {| hdata:=Sundef unknown_hid; hcodes :=sv; |}. Lemma hSundef_correct: - WHEN hSundef ~> hv THEN forall ctx, - sval_refines ctx hv (Sundef unknown_hid). + WHEN hSundef ~> sv THEN forall ctx, + sval_refines ctx sv (Sundef unknown_hid). Proof. wlp_simplify. Qed. @@ -287,8 +298,8 @@ Definition hSnil (_: unit): ?? list_sval := hC_list_sval {| hdata := Snil unknown_hid; hcodes := nil |}. Lemma hSnil_correct: - WHEN hSnil() ~> hv THEN forall ctx, - list_sval_refines ctx hv (Snil unknown_hid). + WHEN hSnil() ~> sv THEN forall ctx, + list_sval_refines ctx sv (Snil unknown_hid). Proof. wlp_simplify. Qed. @@ -324,14 +335,14 @@ Global Opaque hSinit. Local Hint Resolve hSinit_correct: wlp. Definition hSstore_hcodes (sm: smem) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) (srce: sval):= - DO hv1 <~ hash chunk;; - DO hv2 <~ hash addr;; - RET [smem_get_hid sm; hv1; hv2; list_sval_get_hid lsv; sval_get_hid srce]. + DO sv1 <~ hash chunk;; + DO sv2 <~ hash addr;; + RET [smem_get_hid sm; sv1; sv2; list_sval_get_hid lsv; sval_get_hid srce]. Extraction Inline hSstore_hcodes. Definition hSstore (sm: smem) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) (srce: sval): ?? smem := - DO hv <~ hSstore_hcodes sm chunk addr lsv srce;; - hC_smem {| hdata := Sstore sm chunk addr lsv srce unknown_hid; hcodes := hv |}. + DO sv <~ hSstore_hcodes sm chunk addr lsv srce;; + hC_smem {| hdata := Sstore sm chunk addr lsv srce unknown_hid; hcodes := sv |}. Lemma hSstore_correct sm1 chunk addr lsv1 sv1: WHEN hSstore sm1 chunk addr lsv1 sv1 ~> sm1' THEN forall ctx lsv2 sm2 sv2 @@ -408,12 +419,12 @@ with fsval_list_proj sl: ?? list_sval := DO b <~ phys_eq hc unknown_hid;; if b then hSnil() (* was not yet really hash-consed *) else RET sl (* already hash-consed *) - | Scons hv hl hc => + | Scons sv hl hc => DO b <~ phys_eq hc unknown_hid;; if b then (* was not yet really hash-consed *) - DO hv' <~ fsval_proj hv;; + DO sv' <~ fsval_proj sv;; DO hl' <~ fsval_list_proj hl;; - hScons hv' hl' + hScons sv' hl' else RET sl (* already hash-consed *) end. @@ -555,7 +566,7 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval := hSop op lsv (* TODO gourdinl match target_op_simplify op lr hrs with - | Some fhv => fsval_proj fhv + | Some fsv => fsval_proj fsv | None => hSop op lhsv end*) @@ -566,11 +577,11 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval := end. Lemma simplify_correct rsv lr hrs: - WHEN simplify rsv lr hrs ~> hv THEN forall ctx sis + WHEN simplify rsv lr hrs ~> sv THEN forall ctx sis (REF: ris_refines ctx hrs sis) (OK0: ris_ok ctx hrs) (OK1: eval_sval ctx (rsv lr sis) <> None), - sval_refines ctx hv (rsv lr sis). + sval_refines ctx sv (rsv lr sis). Proof. destruct rsv; simpl; auto. - (* Rop *) @@ -678,9 +689,9 @@ Qed. Definition hrset_sreg r lr rsv (hrs: ristate): ?? ristate := DO ok_lsv <~ (if may_trap rsv lr - then DO hv <~ root_happly rsv lr hrs;; - XDEBUG hv (fun hv => DO hv_name <~ string_of_hashcode (sval_get_hid hv);; RET ("-- insert undef behavior of hashcode:" +; (CamlStr hv_name))%string);; - RET (hv::(ok_rsval hrs)) + then DO sv <~ root_happly rsv lr hrs;; + XDEBUG sv (fun sv => DO sv_name <~ string_of_hashcode (sval_get_hid sv);; RET ("-- insert undef behavior of hashcode:" +; (CamlStr sv_name))%string);; + RET (sv::(ok_rsval hrs)) else RET (ok_rsval hrs));; DO simp <~ simplify rsv lr hrs;; RET {| ris_smem := hrs.(ris_smem); @@ -878,11 +889,186 @@ Proof. wlp_simplify. Qed. Global Opaque struct_check. Hint Resolve struct_check_correct: wlp. -Definition sfval_simu_check (sfv1 sfv2: sfval) := RET tt. +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" + | None, None => RET tt + | _, _ => FAILWITH "option_eq_check: structure differs" + end. -Fixpoint rst_simu_check (rst1 rst2: rstate) := +Lemma option_eq_check_correct A (o1 o2: option A): WHEN option_eq_check o1 o2 ~> _ THEN o1=o2. +Proof. + wlp_simplify. +Qed. +Global Opaque option_eq_check. +Hint Resolve option_eq_check_correct:wlp. + +Import PTree. + +Fixpoint PTree_eq_check {A} (d1 d2: PTree.t A): ?? unit := + match d1, d2 with + | Leaf, Leaf => RET tt + | Node l1 o1 r1, Node l2 o2 r2 => + option_eq_check o1 o2;; + PTree_eq_check l1 l2;; + PTree_eq_check r1 r2 + | _, _ => FAILWITH "PTree_eq_check: some key is absent" + end. + +Lemma PTree_eq_check_correct A d1: forall (d2: t A), + WHEN PTree_eq_check d1 d2 ~> _ THEN forall x, PTree.get x d1 = PTree.get x d2. +Proof. + induction d1 as [|l1 Hl1 o1 r1 Hr1]; destruct d2 as [|l2 o2 r2]; simpl; + wlp_simplify. destruct x; simpl; auto. +Qed. +Global Opaque PTree_eq_check. +Local Hint Resolve PTree_eq_check_correct: wlp. + +Definition hrs_simu_check (hrs1 hrs2: ristate) : ?? unit := + DEBUG("? hrs_simu_check");; + phys_check (ris_smem hrs1) (ris_smem hrs2) "hrs_simu_check: ris_smem sets aren't equiv";; + phys_check (ris_input_init hrs1) (ris_input_init hrs2) "hrs_simu_check: ris_input_init bools aren't equiv";; + PTree_eq_check (ris_sreg hrs1) (ris_sreg hrs2);; + Sets.assert_list_incl mk_hash_params (ok_rsval hrs2) (ok_rsval hrs1);; + DEBUG("=> hrs_simu_check: OK"). + +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 regset_elements_in: core. + +Lemma hrs_simu_check_correct hrs1 hrs2: + WHEN hrs_simu_check hrs1 hrs2 ~> _ THEN + ris_simu hrs1 hrs2. +Proof. + wlp_simplify; constructor; auto. + unfold ris_sreg_get; intros r; rewrite H, H1; reflexivity. +Qed. +Hint Resolve hrs_simu_check_correct: wlp. +Global Opaque hrs_simu_check. + +Definition svos_simu_check (svos1 svos2: sval + ident) := + match svos1, svos2 with + | inl sv1, inl sv2 => phys_check sv1 sv2 "svos_simu_check: sval mismatch" + | inr id1, inr id2 => phys_check id1 id2 "svos_simu_check: symbol mismatch" + | _, _ => FAILWITH "svos_simu_check: type mismatch" + end. + +Lemma svos_simu_check_correct svos1 svos2: + WHEN svos_simu_check svos1 svos2 ~> _ THEN + svos1 = svos2. +Proof. + destruct svos1; destruct svos2; wlp_simplify. +Qed. +Global Opaque svos_simu_check. +Hint Resolve svos_simu_check_correct: wlp. + +Fixpoint builtin_arg_simu_check (bs bs': builtin_arg sval) := + match bs with + | BA sv => + match bs' with + | BA sv' => phys_check sv sv' "builtin_arg_simu_check: sval mismatch" + | _ => FAILWITH "builtin_arg_simu_check: BA mismatch" + end + | BA_splitlong lo hi => + match bs' with + | BA_splitlong lo' hi' => + builtin_arg_simu_check lo lo';; + builtin_arg_simu_check hi hi' + | _ => FAILWITH "builtin_arg_simu_check: BA_splitlong mismatch" + end + | BA_addptr b1 b2 => + match bs' with + | BA_addptr b1' b2' => + builtin_arg_simu_check b1 b1';; + builtin_arg_simu_check b2 b2' + | _ => FAILWITH "builtin_arg_simu_check: BA_addptr mismatch" + end + | bs => struct_check bs bs' "builtin_arg_simu_check: basic mismatch" + end. + +Lemma builtin_arg_simu_check_correct: forall bs1 bs2, + WHEN builtin_arg_simu_check bs1 bs2 ~> _ THEN + bs1 = bs2. +Proof. + induction bs1. + all: try (wlp_simplify; subst; reflexivity). + all: destruct bs2; wlp_simplify; congruence. +Qed. +Global Opaque builtin_arg_simu_check. +Hint Resolve builtin_arg_simu_check_correct: wlp. + +Fixpoint list_builtin_arg_simu_check lbs1 lbs2 := + match lbs1, lbs2 with + | nil, nil => RET tt + | bs1::lbs1, bs2::lbs2 => + builtin_arg_simu_check bs1 bs2;; + list_builtin_arg_simu_check lbs1 lbs2 + | _, _ => FAILWITH "list_builtin_arg_simu_check: length mismatch" + end. + +Lemma list_builtin_arg_simu_check_correct: forall lbs1 lbs2, + WHEN list_builtin_arg_simu_check lbs1 lbs2 ~> _ THEN + lbs1 = lbs2. +Proof. + induction lbs1; destruct lbs2; wlp_simplify. congruence. +Qed. +Global Opaque list_builtin_arg_simu_check. +Hint Resolve list_builtin_arg_simu_check_correct: wlp. + +Definition sfval_simu_check (sfv1 sfv2: sfval): ?? unit := + match sfv1, sfv2 with + | Sgoto e1, Sgoto e2 => + phys_check e1 e2 "sfval_simu_check: Sgoto successors do not match" + | Scall sig1 svos1 lsv1 res1 e1, Scall sig2 svos2 lsv2 res2 e2 => + phys_check e1 e2 "sfval_simu_check: Scall successors do not match";; + phys_check sig1 sig2 "sfval_simu_check: Scall different signatures";; + phys_check res1 res2 "sfval_simu_check: Scall res do not match";; + svos_simu_check svos1 svos2;; + phys_check lsv1 lsv2 "sfval_simu_check: Scall args do not match" + | Stailcall sig1 svos1 lsv1, Stailcall sig2 svos2 lsv2 => + phys_check sig1 sig2 "sfval_simu_check: Stailcall different signatures";; + svos_simu_check svos1 svos2;; + phys_check lsv1 lsv2 "sfval_simu_check: Stailcall args do not match" + | Sbuiltin ef1 lbs1 br1 e1, Sbuiltin ef2 lbs2 br2 e2 => + phys_check e1 e2 "sfval_simu_check: Sbuiltin successors do not match";; + phys_check ef1 ef2 "sfval_simu_check: Sbuiltin ef do not match";; + phys_check br1 br2 "sfval_simu_check: Sbuiltin br do not match";; + list_builtin_arg_simu_check lbs1 lbs2 + | Sjumptable sv1 le1, Sjumptable sv2 le2 => + phys_check le1 le2 "sfval_simu_check: Sjumptable successors do not match";; + phys_check sv1 sv2 "sfval_simu_check: Sjumptable sval do not match" + | Sreturn osv1, Sreturn osv2 => + option_eq_check osv1 osv2 + | _, _ => FAILWITH "sfval_simu_check: structure mismatch" + end. + +Lemma sfval_simu_check_correct sfv1 sfv2: + WHEN sfval_simu_check sfv1 sfv2 ~> _ THEN + rfv_simu sfv1 sfv2. +Proof. + destruct sfv1; destruct sfv2; simpl; wlp_simplify; try congruence. +Qed. +Hint Resolve sfval_simu_check_correct: wlp. +Global Opaque sfval_simu_check. + +Fixpoint rst_simu_check (rst1 rst2: rstate) {struct rst1} := match rst1, rst2 with - | Rfinal ris1 sfv1, Rfinal ris2 sfv2 => + | Rfinal hrs1 sfv1, Rfinal hrs2 sfv2 => + hrs_simu_check hrs1 hrs2;; 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";; @@ -892,17 +1078,18 @@ Fixpoint rst_simu_check (rst1 rst2: rstate) := | _, _ => FAILWITH "hsstate_simu_check: simu_check failed" end. -Lemma rst_simu_check_correct rst1 rst2: +Lemma rst_simu_check_correct rst1: forall rst2, WHEN rst_simu_check rst1 rst2 ~> _ THEN rst_simu rst1 rst2. Proof. - induction rst1, rst2; - wlp_simplify. -Admitted. + induction rst1; destruct rst2; + wlp_simplify; constructor; auto. +Qed. 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)) := +(* TODO do we really need both functions *) +Definition simu_check_single (f1 f2: function) (ib1 ib2: iblock): ?? unit := (* creating the hash-consing tables *) DO hC_sval <~ hCons hSVAL;; DO hC_list_hsval <~ hCons hLSVAL;; @@ -918,18 +1105,24 @@ 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. + unfold symbolic_simu; wlp_simplify. 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'. +Fixpoint simu_check_rec (f1 f2: function) (blks: list node): ?? unit := + match blks with + | nil => RET tt + | pc :: blk' => + DO ibf1 <~ some_or_fail (fn_code f1)!pc "simu_check_rec: incorrect PTree for f1";; + DO ibf2 <~ some_or_fail (fn_code f2)!pc "simu_check_rec: incorrect PTree for f2";; + DO res <~ simu_check_single f1 f2 ibf1.(entry) ibf2.(entry);; + simu_check_rec f1 f2 blk' + end. -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. +Lemma simu_check_rec_correct f1 f2: + WHEN simu_check_rec f1 f2 (PTree.elements (fn_code f1)) ~> _ THEN + symbolic_simu f1 f2 . Proof. induction lm; wlp_simplify. match goal with -- cgit