From 258578dcdf0963d197a0c9d7d8b379dfb1325829 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Sat, 10 Oct 2020 08:32:43 +0200 Subject: progress on hsexec_inst_correct_dyn --- kvx/lib/RTLpathSE_impl_junk.v | 179 +++++++++++++++++++++++++++++++++--------- 1 file changed, 140 insertions(+), 39 deletions(-) (limited to 'kvx') diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index dce66a5f..04e8d559 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -372,6 +372,27 @@ Definition hsistate_refines_dyn ge sp rs0 m0 (hst: hsistate) (st:sistate): Prop /\ hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st) /\ nested_sok ge sp rs0 m0 (si_local st) (si_exits st). +Lemma hsistate_refines_dyn_exits ge sp rs0 m0 hst st: + hsistate_refines_dyn ge sp rs0 m0 hst st -> hsiexits_refines_dyn ge sp rs0 m0 (hsi_exits hst) (si_exits st). +Proof. + unfold hsistate_refines_dyn; intuition. +Qed. +Local Hint Resolve hsistate_refines_dyn_exits: core. + +Lemma hsistate_refines_dyn_local ge sp rs0 m0 hst st: + hsistate_refines_dyn ge sp rs0 m0 hst st -> hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st). +Proof. + unfold hsistate_refines_dyn; intuition. +Qed. +Local Hint Resolve hsistate_refines_dyn_local: core. + +Lemma hsistate_refines_dyn_nested ge sp rs0 m0 hst st: + hsistate_refines_dyn ge sp rs0 m0 hst st -> nested_sok ge sp rs0 m0 (si_local st) (si_exits st). +Proof. + unfold hsistate_refines_dyn; intuition. +Qed. +Local Hint Resolve hsistate_refines_dyn_nested: core. + (** * Implementation of symbolic execution *) Section CanonBuilding. @@ -428,13 +449,13 @@ Definition hSop (op:operation) (lhsv: list_hsval) (hsm: hsmem): ?? hsval := hC_hsval {| hdata:=HSop op lhsv hsm unknown_hid; hcodes :=hv |}. Lemma hSop_correct op lhsv hsm: - WHEN hSop op lhsv hsm ~> hv THEN forall ge sp rs0 m0 lsv sm, - list_sval_refines ge sp rs0 m0 lhsv lsv -> - smem_refines ge sp rs0 m0 hsm sm -> + WHEN hSop op lhsv hsm ~> hv THEN forall ge sp rs0 m0 lsv sm + (LR: list_sval_refines ge sp rs0 m0 lhsv lsv) + (MR: smem_refines ge sp rs0 m0 hsm sm), sval_refines ge sp rs0 m0 hv (Sop op lsv sm). Proof. wlp_simplify. - rewrite <- H0, <- H1. + rewrite <- LR, <- MR. auto. Qed. Global Opaque hSop. @@ -453,13 +474,13 @@ Definition hSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr hC_hsval {| hdata := HSload hsm trap chunk addr lhsv unknown_hid; hcodes := hv |}. Lemma hSload_correct hsm trap chunk addr lhsv: - WHEN hSload hsm trap chunk addr lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm, - list_sval_refines ge sp rs0 m0 lhsv lsv -> - smem_refines ge sp rs0 m0 hsm sm -> + WHEN hSload hsm trap chunk addr lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm + (LR: list_sval_refines ge sp rs0 m0 lhsv lsv) + (MR: smem_refines ge sp rs0 m0 hsm sm), sval_refines ge sp rs0 m0 hv (Sload sm trap chunk addr lsv). Proof. wlp_simplify. - rewrite <- H0, <- H1. + rewrite <- LR, <- MR. auto. Qed. Global Opaque hSload. @@ -481,13 +502,13 @@ Definition hScons (hsv: hsval) (lhsv: list_hsval): ?? list_hsval := hC_list_hsval {| hdata := HScons hsv lhsv unknown_hid; hcodes := [hsval_get_hid hsv; list_hsval_get_hid lhsv] |}. Lemma hScons_correct hsv lhsv: - WHEN hScons hsv lhsv ~> lhsv' THEN forall ge sp rs0 m0 sv lsv, - sval_refines ge sp rs0 m0 hsv sv -> - list_sval_refines ge sp rs0 m0 lhsv lsv -> + WHEN hScons hsv lhsv ~> lhsv' THEN forall ge sp rs0 m0 sv lsv + (VR: sval_refines ge sp rs0 m0 hsv sv) + (LR: list_sval_refines ge sp rs0 m0 lhsv lsv), list_sval_refines ge sp rs0 m0 lhsv' (Scons sv lsv). Proof. wlp_simplify. - rewrite <- H0, <- H1. + rewrite <- VR, <- LR. auto. Qed. Global Opaque hScons. @@ -516,14 +537,14 @@ Definition hSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: hC_hsmem {| hdata := HSstore hsm chunk addr lhsv srce unknown_hid; hcodes := hv |}. Lemma hSstore_correct hsm chunk addr lhsv hsv: - WHEN hSstore hsm chunk addr lhsv hsv ~> hsm' THEN forall ge sp rs0 m0 lsv sm sv, - list_sval_refines ge sp rs0 m0 lhsv lsv -> - smem_refines ge sp rs0 m0 hsm sm -> - sval_refines ge sp rs0 m0 hsv sv -> + WHEN hSstore hsm chunk addr lhsv hsv ~> hsm' THEN forall ge sp rs0 m0 lsv sm sv + (LR: list_sval_refines ge sp rs0 m0 lhsv lsv) + (MR: smem_refines ge sp rs0 m0 hsm sm) + (VR: sval_refines ge sp rs0 m0 hsv sv), smem_refines ge sp rs0 m0 hsm' (Sstore sm chunk addr lsv sv). Proof. wlp_simplify. - rewrite <- H0, <- H1, <- H2. + rewrite <- LR, <- MR, <- VR. auto. Qed. Global Opaque hSstore. @@ -536,13 +557,11 @@ Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval := end. Lemma hsi_sreg_get_correct hst r: - WHEN hsi_sreg_get hst r ~> hsv THEN forall ge sp rs0 m0 (f: reg -> sval), - (forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0) -> + WHEN hsi_sreg_get hst r ~> hsv THEN forall ge sp rs0 m0 (f: reg -> sval) + (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0), sval_refines ge sp rs0 m0 hsv (f r). Proof. - unfold hsi_sreg_eval; wlp_simplify. - + rewrite <- H0, H. auto. - + rewrite <- H1, H. auto. + unfold hsi_sreg_eval; wlp_simplify; rewrite <- RR; try_simplify_someHyps. Qed. Global Opaque hsi_sreg_get. Local Hint Resolve hsi_sreg_get_correct: wlp. @@ -556,10 +575,9 @@ Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? list_hsval := hScons v lhsv end. - Lemma hlist_args_correct hst l: - WHEN hlist_args hst l ~> lhsv THEN forall ge sp rs0 m0 (f: reg -> sval), - (forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0) -> + WHEN hlist_args hst l ~> lhsv THEN forall ge sp rs0 m0 (f: reg -> sval) + (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0), list_sval_refines ge sp rs0 m0 lhsv (list_sval_inj (List.map f l)). Proof. induction l; wlp_simplify. @@ -625,8 +643,8 @@ Definition hslocal_store (hst: hsistate_local) chunk addr args src: ?? hsistate_ RET (hslocal_set_smem hst hm). Lemma hslocal_store_correct hst chunk addr args src: - WHEN hslocal_store hst chunk addr args src ~> hst' THEN forall ge sp rs0 m0 st, - hsilocal_refines ge sp rs0 m0 hst st -> + WHEN hslocal_store hst chunk addr args src ~> hst' THEN forall ge sp rs0 m0 st + (REF: hsilocal_refines ge sp rs0 m0 hst st), hsilocal_refines ge sp rs0 m0 hst' (slocal_store st chunk addr args src). Proof. wlp_simplify. @@ -688,15 +706,15 @@ Definition hSop_hSinit (op:operation) (lhsv: list_hsval): ?? hsval := . Lemma hSop_hSinit_correct op lhsv: - WHEN hSop_hSinit op lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm m, - seval_smem ge sp sm rs0 m0 = Some m -> - (forall b ofs, Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) -> - list_sval_refines ge sp rs0 m0 lhsv lsv -> + WHEN hSop_hSinit op lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm m + (MEM: seval_smem ge sp sm rs0 m0 = Some m) + (MVALID: forall b ofs, Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) + (LR: list_sval_refines ge sp rs0 m0 lhsv lsv), sval_refines ge sp rs0 m0 hv (Sop op lsv sm). Proof. wlp_simplify. erewrite H0; [ idtac | eauto | eauto ]. - rewrite H, H1. + rewrite H, MEM. destruct (seval_list_sval _ _ lsv _); try congruence. eapply op_valid_pointer_eq; eauto. Qed. @@ -711,9 +729,9 @@ Definition root_happly (rsv: root_sval) (lr: list reg) (hst: hsistate_local) : ? end. Lemma root_happly_correct (rsv: root_sval) lr hst: - WHEN root_happly rsv lr hst ~> hv' THEN forall ge sp rs0 m0 st, - hsilocal_refines ge sp rs0 m0 hst st -> - hsok_local ge sp rs0 m0 hst -> + WHEN root_happly rsv lr hst ~> hv' THEN forall ge sp rs0 m0 st + (REF:hsilocal_refines ge sp rs0 m0 hst st) + (OK:hsok_local ge sp rs0 m0 hst), sval_refines ge sp rs0 m0 hv' (rsv lr st). Proof. unfold hsilocal_refines, root_apply, root_happly; destruct rsv; wlp_simplify. @@ -785,10 +803,10 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs end. Lemma simplify_correct rsv lr hst: - WHEN simplify rsv lr hst ~> hv THEN forall ge sp rs0 m0 st, - hsilocal_refines ge sp rs0 m0 hst st -> - hsok_local ge sp rs0 m0 hst -> - seval_sval ge sp (rsv lr st) rs0 m0 <> None -> + WHEN simplify rsv lr hst ~> hv THEN forall ge sp rs0 m0 st + (REF: hsilocal_refines ge sp rs0 m0 hst st) + (OK0: hsok_local ge sp rs0 m0 hst) + (OK1: seval_sval ge sp (rsv lr st) rs0 m0 <> None), sval_refines ge sp rs0 m0 hv (rsv lr st). Proof. destruct rsv; simpl; auto. @@ -835,6 +853,23 @@ Proof. - rewrite PTree.gro, PTree.gso; simpl; auto. Qed. +(* TODO: a revoir --- simplifier! +Lemma sok_local_set_sreg ge sp rs0 m0 st r (rsv:root_sval) lr sv': + (sok_local ge sp rs0 m0 st -> seval_sval ge sp sv' rs0 m0 = seval_sval ge sp (rsv lr st) rs0 m0) -> + sok_local ge sp rs0 m0 (slocal_set_sreg st r sv') + <-> (sok_local ge sp rs0 m0 st /\ seval_sval ge sp sv' rs0 m0 <> None). +Proof. + unfold slocal_set_sreg, sok_local; simpl; intro SV'; split. + + intros ((SVAL0 & PRE) & SMEM & SVAL). + repeat (split; try tauto). + - intros r0; generalize (SVAL r0); clear SVAL; destruct (Pos.eq_dec r r0); try congruence. + - generalize (SVAL r); clear SVAL; destruct (Pos.eq_dec r r); try congruence. + + intros ((PRE & SMEM & SVAL0) & SVAL). + repeat (split; try tauto; eauto). + intros r0; destruct (Pos.eq_dec r r0); try congruence. +Qed. +*) + Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) (lr: list reg): ?? hsistate_local := DO ok_lhsv <~ (if may_trap rsv lr @@ -847,6 +882,25 @@ Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) (lr: hsi_ok_lsval := ok_lhsv; hsi_sreg := red_PTree_set r simp (hsi_sreg hst) |}. + +Lemma hslocal_set_sreg_correct hst r rsv lr: + WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN forall ge sp rs0 m0 st + (REF: hsilocal_refines ge sp rs0 m0 hst st), + hsilocal_refines ge sp rs0 m0 hst' (slocal_set_sreg st r (rsv lr st)). +Proof. + wlp_simplify. + + assert (X: sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st)) <-> + hsok_local ge sp rs0 m0 {| hsi_smem := hst; hsi_ok_lsval := exta :: hsi_ok_lsval hst; hsi_sreg := red_PTree_set r exta0 hst |}). + { admit . } + unfold hsilocal_refines; split; auto. + + +Admitted. +Global Opaque hslocal_set_sreg. +Local Hint Resolve hslocal_set_sreg_correct: wlp. + + + (** ** Execution of one instruction *) Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) := @@ -870,6 +924,53 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) : | _ => RET None (* TODO jumptable ? *) end. +Lemma seval_condition_refines hst st ge sp cond hargs args rs m: + hsok_local ge sp rs m hst -> + hsilocal_refines ge sp rs m hst st -> + list_sval_refines ge sp rs m hargs args -> + hseval_condition ge sp cond hargs (hsi_smem hst) rs m + = seval_condition ge sp cond args (si_smem st) rs m. + Proof. + intros HOK (_ & MEMEQ & _) LR. unfold hseval_condition, seval_condition. + rewrite LR, <- MEMEQ; auto. +Qed. + +Lemma hsiexec_inst_correct_dyn i hst: + WHEN hsiexec_inst i hst ~> o THEN forall ge sp rs0 m0 st hst' st' + (EQo: o = Some hst') + (SIEXEC: siexec_inst i st = Some st') + (REF: hsistate_refines_dyn ge sp rs0 m0 hst st), + hsistate_refines_dyn ge sp rs0 m0 hst' st'. +Proof. + destruct i; simpl; wlp_simplify; try_simplify_someHyps. + - (* Iop *) + eapply hsist_set_local_correct_dyn; eauto. + unfold sok_local; simpl; intros (PRE & MEM & REG). + intuition. + generalize (REG r0); clear REG. + destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto). + - (* Iload *) + eapply hsist_set_local_correct_dyn; eauto. + unfold sok_local; simpl; intros (PRE & MEM & REG). + intuition. + generalize (REG r0); clear REG. + destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto). + - (* Istore *) + eapply hsist_set_local_correct_dyn; eauto. + unfold sok_local; simpl; intuition. + - (* Icond *) + destruct REF as (EXREF & LREF & NEST). + split. + + constructor; simpl; auto. + constructor; simpl; auto. + intros; erewrite seval_condition_refines; eauto. + + split; simpl; auto. + destruct NEST as [|st0 se lse TOP NEST]; + econstructor; simpl; auto; constructor; auto. +Qed. +Global Opaque hsiexec_inst. +Local Hint Resolve hsiexec_inst_correct_dyn: wlp. + Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A := match o with | Some x => RET x -- cgit