From e907de8f2c30e5e004941b1ff6079eed503d83c3 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 30 Jun 2021 12:42:12 +0200 Subject: Starting symbolic execution implementation --- scheduling/BTL_SEimpl.v | 314 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 314 insertions(+) create mode 100644 scheduling/BTL_SEimpl.v (limited to 'scheduling') diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v new file mode 100644 index 00000000..5c974efd --- /dev/null +++ b/scheduling/BTL_SEimpl.v @@ -0,0 +1,314 @@ +Require Import AST Maps. +Require Import Op Registers. +Require Import RTL BTL. +Require Import BTL_SEsimuref BTL_SEtheory OptionMonad. + +Require Import Impure.ImpHCons. +Import Notations. +Import HConsing. + +Local Open Scope option_monad_scope. +Local Open Scope impure. + +Import ListNotations. +Local Open Scope list_scope. + +(** Notations to make lemmas more readable *) +Notation "'sval_refines' ctx sv1 sv2" := (eval_sval ctx sv1 = eval_sval ctx sv2) + (only parsing, at level 0, ctx at next level, sv1 at next level, sv2 at next level): hse. + +Local Open Scope hse. + +Notation "'list_sval_refines' ctx lsv1 lsv2" := (eval_list_sval ctx lsv1 = eval_list_sval ctx lsv2) + (only parsing, at level 0, ctx at next level, lsv1 at next level, lsv2 at next level): hse. + +Notation "'smem_refines' ctx sm1 sm2" := (eval_smem ctx sm1 = eval_smem ctx sm2) + (only parsing, at level 0, ctx at next level, sm1 at next level, sm2 at next level): hse. + +(** Debug printer *) +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 *) + +Definition sval_get_hid (sv: sval): hashcode := + match sv with + | Sundef hid => hid + | Sinput _ hid => hid + | Sop _ _ hid => hid + | Sload _ _ _ _ _ hid => hid + end. + +Definition list_sval_get_hid (lsv: list_sval): hashcode := + match lsv with + | Snil hid => hid + | Scons _ _ hid => hid + end. + +Definition smem_get_hid (sm: smem): hashcode := + match sm with + | Sinit hid => hid + | Sstore _ _ _ _ _ hid => hid + end. + +Definition sval_set_hid (sv: sval) (hid: hashcode): sval := + match sv with + | Sundef _ => Sundef hid + | Sinput r _ => Sinput r hid + | Sop o lsv _ => Sop o lsv hid + | Sload sm trap chunk addr lsv _ => Sload sm trap chunk addr lsv hid + end. + +Definition list_sval_set_hid (lsv: list_sval) (hid: hashcode): list_sval := + match lsv with + | Snil _ => Snil hid + | Scons sv lsv _ => Scons sv lsv hid + end. + +Definition smem_set_hid (sm: smem) (hid: hashcode): smem := + match sm with + | Sinit _ => Sinit hid + | Sstore sm chunk addr lsv srce _ => Sstore sm chunk addr lsv srce hid + end. + +(** * Implementation of symbolic execution *) +Section CanonBuilding. + +Variable hC_sval: hashinfo sval -> ?? sval. + +Hypothesis hC_sval_correct: forall s, + WHEN hC_sval s ~> s' THEN forall ctx, + sval_refines ctx (hdata s) s'. + +Variable hC_list_sval: hashinfo list_sval -> ?? list_sval. +Hypothesis hC_list_sval_correct: forall lh, + WHEN hC_list_sval lh ~> lh' THEN forall ctx, + list_sval_refines ctx (hdata lh) lh'. + +Variable hC_smem: hashinfo smem -> ?? smem. +Hypothesis hC_smem_correct: forall hm, + WHEN hC_smem hm ~> hm' THEN forall ctx, + smem_refines ctx (hdata hm) hm'. + +(* First, we wrap constructors for hashed values !*) + +Definition reg_hcode := 1. +Definition op_hcode := 2. +Definition load_hcode := 3. +Definition undef_code := 4. + +Definition hSinput_hcodes (r: reg) := + DO hc <~ hash reg_hcode;; + DO hv <~ hash r;; + RET [hc;hv]. +Extraction Inline hSinput_hcodes. + +Definition hSinput (r:reg): ?? sval := + DO hv <~ hSinput_hcodes r;; + hC_sval {| hdata:=Sinput r unknown_hid; hcodes :=hv; |}. + +Lemma hSinput_correct r: + WHEN hSinput r ~> hv THEN forall ctx, + sval_refines ctx hv (Sinput r unknown_hid). +Proof. + wlp_simplify. +Qed. +Global Opaque hSinput. +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]. +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 |}. + +Lemma hSop_fSop_correct op lsv: + WHEN hSop op lsv ~> hv THEN forall ctx, + sval_refines ctx hv (fSop op lsv). +Proof. + wlp_simplify. +Qed. +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 + (LR: list_sval_refines ctx lsv1 lsv2), + sval_refines ctx hv (Sop op lsv2 unknown_hid). +Proof. + wlp_xsimplify ltac:(intuition eauto with wlp wlp_raw). + rewrite <- LR. erewrite H; eauto. +Qed. +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]. +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 |}. + +Lemma hSload_correct sm1 trap chunk addr lsv1: + WHEN hSload sm1 trap chunk addr lsv1 ~> hv THEN forall ctx lsv2 sm2 hid + (LR: list_sval_refines ctx lsv1 lsv2) + (MR: smem_refines ctx sm1 sm2), + sval_refines ctx hv (Sload sm2 trap chunk addr lsv2 hid). +Proof. + wlp_simplify. + rewrite <- LR, <- MR. + auto. +Qed. +Global Opaque hSload. +Local Hint Resolve hSload_correct: wlp. + +Definition hSundef_hcodes := + DO hc <~ hash undef_code;; + RET [hc]. +Extraction Inline hSundef_hcodes. + +Definition hSundef : ?? sval := + DO hv <~ hSundef_hcodes;; + hC_sval {| hdata:=Sundef unknown_hid; hcodes :=hv; |}. + +Lemma hSundef_correct: + WHEN hSundef ~> hv THEN forall ctx, + sval_refines ctx hv (Sundef unknown_hid). +Proof. + wlp_simplify. +Qed. +Global Opaque hSundef. +Local Hint Resolve hSundef_correct: wlp. + +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). +Proof. + wlp_simplify. +Qed. +Global Opaque hSnil. +Local Hint Resolve hSnil_correct: wlp. + +Definition hScons (sv: sval) (lsv: list_sval): ?? list_sval := + hC_list_sval {| hdata := Scons sv lsv unknown_hid; hcodes := [sval_get_hid sv; list_sval_get_hid lsv] |}. + +Lemma hScons_correct sv1 lsv1: + WHEN hScons sv1 lsv1 ~> lsv1' THEN forall ctx sv2 lsv2 + (VR: sval_refines ctx sv1 sv2) + (LR: list_sval_refines ctx lsv1 lsv2), + list_sval_refines ctx lsv1' (Scons sv2 lsv2 unknown_hid). +Proof. + wlp_simplify. + rewrite <- VR, <- LR. + auto. +Qed. +Global Opaque hScons. +Local Hint Resolve hScons_correct: wlp. + +Definition hSinit (_: unit): ?? smem := + hC_smem {| hdata := Sinit unknown_hid; hcodes := nil |}. + +Lemma hSinit_correct: + WHEN hSinit() ~> hm THEN forall ctx, + smem_refines ctx hm (Sinit unknown_hid). +Proof. + wlp_simplify. +Qed. +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]. +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 |}. + +Lemma hSstore_correct sm1 chunk addr lsv1 sv1: + WHEN hSstore sm1 chunk addr lsv1 sv1 ~> sm1' THEN forall ctx lsv2 sm2 sv2 + (LR: list_sval_refines ctx lsv1 lsv2) + (MR: smem_refines ctx sm1 sm2) + (VR: sval_refines ctx sv1 sv2), + smem_refines ctx sm1' (Sstore sm2 chunk addr lsv2 sv2 unknown_hid). +Proof. + wlp_simplify. + rewrite <- LR, <- MR, <- VR. + auto. +Qed. +Global Opaque hSstore. +Local Hint Resolve hSstore_correct: wlp. + +Definition hris_sreg_eval ctx hris r := eval_sval ctx (ris_sreg_get hris r). + +Definition hris_sreg_get (hris: ristate) r: ?? sval := + match PTree.get r hris with + | None => if ris_input_init hris then hSinput r else hSundef + | Some sv => RET sv + end. +Coercion hris_sreg_get: ristate >-> Funclass. + +Lemma hris_sreg_get_correct hris r: + WHEN hris_sreg_get hris r ~> sv THEN forall ctx (f: reg -> sval) + (RR: forall r, hris_sreg_eval ctx hris r = eval_sval ctx (f r)), + sval_refines ctx sv (f r). +Proof. + unfold hris_sreg_eval, ris_sreg_get. wlp_simplify; rewrite <- RR; rewrite H; auto; + rewrite H0, H1; simpl; auto. +Qed. +Global Opaque hris_sreg_get. +Local Hint Resolve hris_sreg_get_correct: wlp. + +Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A := + match o with + | Some x => RET x + | None => FAILWITH msg + end. + +Definition hris_init: ?? ristate + := DO hm <~ hSinit ();; + RET {| ris_smem := hm; ris_input_init := true; ok_rsval := nil; ris_sreg := PTree.empty _ |}. + +Lemma ris_init_correct: + WHEN hris_init ~> hris THEN + forall ctx, ris_refines ctx hris sis_init. +Proof. + unfold hris_init, sis_init; wlp_simplify. + econstructor; simpl in *; eauto. + + split; destruct 1; econstructor; simpl in *; + try rewrite H; try congruence; trivial. + + destruct 1; simpl in *. unfold ris_sreg_get; simpl. + intros; rewrite PTree.gempty; eauto. +Qed. + +(* +Definition hrexec f ib := hrexec_rec f ib hris_init (fun _ => Rabort). + +Definition hsexec (f: function) (pc:node): ?? ristate := + DO path <~ some_or_fail ((fn_code f)!pc) "hsexec.internal_error.1";; + DO hinit <~ init_ristate;; + 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. -- cgit