From fd74f68479c340351641093e5aa9a884f74d3651 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 6 May 2021 18:58:28 +0200 Subject: refactorisation + 1ere version de sstate --- scheduling/BTL_SEtheory.v | 1630 +++++---------------------------------------- 1 file changed, 169 insertions(+), 1461 deletions(-) (limited to 'scheduling/BTL_SEtheory.v') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 53c00c8b..7025b90c 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -13,6 +13,16 @@ Require Import RTL BTL OptionMonad. Ltac inversion_SOME := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *) Ltac inversion_ASSERT := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *) + +Record iblock_exec_context := { + cge: BTL.genv; + csp: val; + cstk: list stackframe; + cf: function; + crs0: regset; + cm0: mem +}. + (** * Syntax and semantics of symbolic values *) (* symbolic value *) @@ -40,26 +50,26 @@ Fixpoint list_sval_inj (l: list sval): list_sval := Local Open Scope option_monad_scope. -Fixpoint eval_sval (ge: BTL.genv) (sp:val) (sv: sval) (rs0: regset) (m0: mem): option val := +Fixpoint eval_sval ctx (sv: sval): option val := match sv with - | Sinput r => Some (rs0#r) + | Sinput r => Some ((crs0 ctx)#r) | Sop op l sm => - SOME args <- eval_list_sval ge sp l rs0 m0 IN - SOME m <- eval_smem ge sp sm rs0 m0 IN - eval_operation ge sp op args m + SOME args <- eval_list_sval ctx l IN + SOME m <- eval_smem ctx sm IN + eval_operation (cge ctx) (csp ctx) op args m | Sload sm trap chunk addr lsv => match trap with | TRAP => - SOME args <- eval_list_sval ge sp lsv rs0 m0 IN - SOME a <- eval_addressing ge sp addr args IN - SOME m <- eval_smem ge sp sm rs0 m0 IN + SOME args <- eval_list_sval ctx lsv IN + SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN + SOME m <- eval_smem ctx sm IN Mem.loadv chunk m a | NOTRAP => - SOME args <- eval_list_sval ge sp lsv rs0 m0 IN - match (eval_addressing ge sp addr args) with + SOME args <- eval_list_sval ctx lsv IN + match (eval_addressing (cge ctx) (csp ctx) addr args) with | None => Some (default_notrap_load_value chunk) | Some a => - SOME m <- eval_smem ge sp sm rs0 m0 IN + SOME m <- eval_smem ctx sm IN match (Mem.loadv chunk m a) with | None => Some (default_notrap_load_value chunk) | Some val => Some val @@ -67,52 +77,49 @@ Fixpoint eval_sval (ge: BTL.genv) (sp:val) (sv: sval) (rs0: regset) (m0: mem): o end end end -with eval_list_sval (ge: BTL.genv) (sp:val) (lsv: list_sval) (rs0: regset) (m0: mem): option (list val) := +with eval_list_sval ctx (lsv: list_sval): option (list val) := match lsv with | Snil => Some nil | Scons sv lsv' => - SOME v <- eval_sval ge sp sv rs0 m0 IN - SOME lv <- eval_list_sval ge sp lsv' rs0 m0 IN + SOME v <- eval_sval ctx sv IN + SOME lv <- eval_list_sval ctx lsv' IN Some (v::lv) end -with eval_smem (ge: BTL.genv) (sp:val) (sm: smem) (rs0: regset) (m0: mem): option mem := +with eval_smem ctx (sm: smem): option mem := match sm with - | Sinit => Some m0 + | Sinit => Some (cm0 ctx) | Sstore sm chunk addr lsv srce => - SOME args <- eval_list_sval ge sp lsv rs0 m0 IN - SOME a <- eval_addressing ge sp addr args IN - SOME m <- eval_smem ge sp sm rs0 m0 IN - SOME sv <- eval_sval ge sp srce rs0 m0 IN + SOME args <- eval_list_sval ctx lsv IN + SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN + SOME m <- eval_smem ctx sm IN + SOME sv <- eval_sval ctx srce IN Mem.storev chunk m a sv end. -Lemma eval_list_sval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs: - (forall r : reg, eval_sval ge sp (sreg r) rs0 m0 = Some (rs # r)) -> - eval_list_sval ge sp (list_sval_inj (map sreg l)) rs0 m0 = Some (rs ## l). +Lemma eval_list_sval_inj ctx l (sreg: reg -> sval) rs: + (forall r : reg, eval_sval ctx (sreg r) = Some (rs # r)) -> + eval_list_sval ctx (list_sval_inj (map sreg l)) = Some (rs ## l). Proof. intros H; induction l as [|r l]; simpl; repeat autodestruct; auto. Qed. -Definition seval_condition ge sp (cond: condition) (lsv: list_sval) (sm: smem) rs0 m0 : option bool := - SOME args <- eval_list_sval ge sp lsv rs0 m0 IN - SOME m <- eval_smem ge sp sm rs0 m0 IN +Definition seval_condition ctx (cond: condition) (lsv: list_sval) (sm: smem) : option bool := + SOME args <- eval_list_sval ctx lsv IN + SOME m <- eval_smem ctx sm IN eval_condition cond args m. (** * Auxiliary definitions on Builtins *) -(* TODO: clean this. Some generic stuffs could be put in [AST.v] *) +(* TODO: clean this. Some (cge ctx)neric stuffs could be put in [AST.v] *) Section SEVAL_BUILTIN_ARG. (* adapted from Events.v *) -Variable ge: BTL.genv. -Variable sp: val. +Variable ctx: iblock_exec_context. Variable m: mem. -Variable rs0: regset. -Variable m0: mem. Inductive seval_builtin_arg: builtin_arg sval -> val -> Prop := | seval_BA: forall x v, - eval_sval ge sp x rs0 m0 = Some v -> + eval_sval ctx x = Some v -> seval_builtin_arg (BA x) v | seval_BA_int: forall n, seval_builtin_arg (BA_int n) (Vint n) @@ -123,22 +130,23 @@ Inductive seval_builtin_arg: builtin_arg sval -> val -> Prop := | seval_BA_single: forall n, seval_builtin_arg (BA_single n) (Vsingle n) | seval_BA_loadstack: forall chunk ofs v, - Mem.loadv chunk m (Val.offset_ptr sp ofs) = Some v -> + Mem.loadv chunk m (Val.offset_ptr (csp ctx) ofs) = Some v -> seval_builtin_arg (BA_loadstack chunk ofs) v | seval_BA_addrstack: forall ofs, - seval_builtin_arg (BA_addrstack ofs) (Val.offset_ptr sp ofs) + seval_builtin_arg (BA_addrstack ofs) (Val.offset_ptr (csp ctx) ofs) | seval_BA_loadglobal: forall chunk id ofs v, - Mem.loadv chunk m (Senv.symbol_address ge id ofs) = Some v -> + Mem.loadv chunk m (Senv.symbol_address (cge ctx) id ofs) = Some v -> seval_builtin_arg (BA_loadglobal chunk id ofs) v | seval_BA_addrglobal: forall id ofs, - seval_builtin_arg (BA_addrglobal id ofs) (Senv.symbol_address ge id ofs) + seval_builtin_arg (BA_addrglobal id ofs) (Senv.symbol_address (cge ctx) id ofs) | seval_BA_splitlong: forall hi lo vhi vlo, seval_builtin_arg hi vhi -> seval_builtin_arg lo vlo -> seval_builtin_arg (BA_splitlong hi lo) (Val.longofwords vhi vlo) | seval_BA_addptr: forall a1 a2 v1 v2, seval_builtin_arg a1 v1 -> seval_builtin_arg a2 v2 -> seval_builtin_arg (BA_addptr a1 a2) - (if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2). + (if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2) +. Definition seval_builtin_args (al: list (builtin_arg sval)) (vl: list val) : Prop := list_forall2 seval_builtin_arg al vl. @@ -159,7 +167,7 @@ Qed. End SEVAL_BUILTIN_ARG. -(* NB: generic function that could be put into [AST] file *) +(* NB: (cge ctx)neric function that could be put into [AST] file *) Fixpoint builtin_arg_map {A B} (f: A -> B) (arg: builtin_arg A) : builtin_arg B := match arg with | BA x => BA (f x) @@ -175,10 +183,10 @@ Fixpoint builtin_arg_map {A B} (f: A -> B) (arg: builtin_arg A) : builtin_arg B | BA_addptr ba1 ba2 => BA_addptr (builtin_arg_map f ba1) (builtin_arg_map f ba2) end. -Lemma seval_builtin_arg_correct ge sp rs m rs0 m0 sreg: forall arg varg, - (forall r, eval_sval ge sp (sreg r) rs0 m0 = Some rs # r) -> - eval_builtin_arg ge (fun r => rs # r) sp m arg varg -> - seval_builtin_arg ge sp m rs0 m0 (builtin_arg_map sreg arg) varg. +Lemma seval_builtin_arg_correct ctx rs m sreg: forall arg varg, + (forall r, eval_sval ctx (sreg r) = Some rs # r) -> + eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg -> + seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg. Proof. induction arg. all: try (intros varg SEVAL BARG; inv BARG; constructor; congruence). @@ -188,10 +196,10 @@ Proof. eapply IHarg1; eauto. eapply IHarg2; eauto. Qed. -Lemma seval_builtin_args_correct ge sp rs m rs0 m0 sreg args vargs: - (forall r, eval_sval ge sp (sreg r) rs0 m0 = Some rs # r) -> - eval_builtin_args ge (fun r => rs # r) sp m args vargs -> - seval_builtin_args ge sp m rs0 m0 (map (builtin_arg_map sreg) args) vargs. +Lemma seval_builtin_args_correct ctx rs m sreg args vargs: + (forall r, eval_sval ctx (sreg r) = Some rs # r) -> + eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs -> + seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs. Proof. induction 2. - constructor. @@ -199,10 +207,10 @@ Proof. eapply seval_builtin_arg_correct; eauto. Qed. -Lemma seval_builtin_arg_complete ge sp rs m rs0 m0 sreg: forall arg varg, - (forall r, eval_sval ge sp (sreg r) rs0 m0 = Some rs # r) -> - seval_builtin_arg ge sp m rs0 m0 (builtin_arg_map sreg arg) varg -> - eval_builtin_arg ge (fun r => rs # r) sp m arg varg. +Lemma seval_builtin_arg_complete ctx rs m sreg: forall arg varg, + (forall r, eval_sval ctx (sreg r) = Some rs # r) -> + seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg -> + eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg. Proof. induction arg. all: intros varg SEVAL BARG; try (inv BARG; constructor; congruence). @@ -213,10 +221,10 @@ Proof. eapply IHarg1; eauto. eapply IHarg2; eauto. Qed. -Lemma seval_builtin_args_complete ge sp rs m rs0 m0 sreg: forall args vargs, - (forall r, eval_sval ge sp (sreg r) rs0 m0 = Some rs # r) -> - seval_builtin_args ge sp m rs0 m0 (map (builtin_arg_map sreg) args) vargs -> - eval_builtin_args ge (fun r => rs # r) sp m args vargs. +Lemma seval_builtin_args_complete ctx rs m sreg: forall args vargs, + (forall r, eval_sval ctx (sreg r) = Some rs # r) -> + seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs -> + eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs. Proof. induction args. - simpl. intros. inv H0. constructor. @@ -225,16 +233,16 @@ Proof. eapply seval_builtin_arg_complete; eauto. Qed. -Fixpoint seval_builtin_sval ge sp bsv rs0 m0 := +Fixpoint seval_builtin_sval ctx bsv := match bsv with - | BA sv => SOME v <- eval_sval ge sp sv rs0 m0 IN Some (BA v) + | BA sv => SOME v <- eval_sval ctx sv IN Some (BA v) | BA_splitlong sv1 sv2 => - SOME v1 <- seval_builtin_sval ge sp sv1 rs0 m0 IN - SOME v2 <- seval_builtin_sval ge sp sv2 rs0 m0 IN + SOME v1 <- seval_builtin_sval ctx sv1 IN + SOME v2 <- seval_builtin_sval ctx sv2 IN Some (BA_splitlong v1 v2) | BA_addptr sv1 sv2 => - SOME v1 <- seval_builtin_sval ge sp sv1 rs0 m0 IN - SOME v2 <- seval_builtin_sval ge sp sv2 rs0 m0 IN + SOME v1 <- seval_builtin_sval ctx sv1 IN + SOME v2 <- seval_builtin_sval ctx sv2 IN Some (BA_addptr v1 v2) | BA_int i => Some (BA_int i) | BA_long l => Some (BA_long l) @@ -246,56 +254,54 @@ Fixpoint seval_builtin_sval ge sp bsv rs0 m0 := | BA_addrglobal id ptr => Some (BA_addrglobal id ptr) end. -Fixpoint eval_list_builtin_sval ge sp lbsv rs0 m0 := +Fixpoint eval_list_builtin_sval ctx lbsv := match lbsv with | nil => Some nil - | bsv::lbsv => SOME v <- seval_builtin_sval ge sp bsv rs0 m0 IN - SOME lv <- eval_list_builtin_sval ge sp lbsv rs0 m0 IN + | bsv::lbsv => SOME v <- seval_builtin_sval ctx bsv IN + SOME lv <- eval_list_builtin_sval ctx lbsv IN Some (v::lv) end. -Lemma eval_list_builtin_sval_nil ge sp rs0 m0 lbs2: - eval_list_builtin_sval ge sp lbs2 rs0 m0 = Some nil -> +Lemma eval_list_builtin_sval_nil ctx lbs2: + eval_list_builtin_sval ctx lbs2 = Some nil -> lbs2 = nil. Proof. - destruct lbs2; simpl; auto. - intros. destruct (seval_builtin_sval _ _ _ _ _); - try destruct (eval_list_builtin_sval _ _ _ _ _); discriminate. + destruct lbs2; simpl; repeat autodestruct; congruence. Qed. -Lemma seval_builtin_sval_arg ge sp rs0 m0 bs: +Lemma seval_builtin_sval_arg ctx bs: forall ba m v, - seval_builtin_sval ge sp bs rs0 m0 = Some ba -> - eval_builtin_arg ge (fun id => id) sp m ba v -> - seval_builtin_arg ge sp m rs0 m0 bs v. + seval_builtin_sval ctx bs = Some ba -> + eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v -> + seval_builtin_arg ctx m bs v. Proof. induction bs; simpl; try (intros ba m v H; inversion H; subst; clear H; intros H; inversion H; subst; econstructor; auto; fail). - - intros ba m v; destruct (eval_sval _ _ _ _ _) eqn: SV; + - intros ba m v; destruct (eval_sval _ _) eqn: SV; intros H; inversion H; subst; clear H. intros H; inversion H; subst. econstructor; auto. - intros ba m v. - destruct (seval_builtin_sval _ _ bs1 _ _) eqn: SV1; try congruence. - destruct (seval_builtin_sval _ _ bs2 _ _) eqn: SV2; try congruence. + destruct (seval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (seval_builtin_sval _ bs2) eqn: SV2; try congruence. intros H; inversion H; subst; clear H. intros H; inversion H; subst. econstructor; eauto. - intros ba m v. - destruct (seval_builtin_sval _ _ bs1 _ _) eqn: SV1; try congruence. - destruct (seval_builtin_sval _ _ bs2 _ _) eqn: SV2; try congruence. + destruct (seval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (seval_builtin_sval _ bs2) eqn: SV2; try congruence. intros H; inversion H; subst; clear H. intros H; inversion H; subst. econstructor; eauto. Qed. -Lemma seval_builtin_arg_sval ge sp m rs0 m0 v: forall bs, - seval_builtin_arg ge sp m rs0 m0 bs v -> +Lemma seval_builtin_arg_sval ctx m v: forall bs, + seval_builtin_arg ctx m bs v -> exists ba, - seval_builtin_sval ge sp bs rs0 m0 = Some ba - /\ eval_builtin_arg ge (fun id => id) sp m ba v. + seval_builtin_sval ctx bs = Some ba + /\ eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v. Proof. induction 1. all: try (eexists; constructor; [simpl; reflexivity | constructor]). @@ -315,28 +321,28 @@ Proof. + constructor; assumption. Qed. -Lemma seval_builtin_sval_args ge sp rs0 m0 lbs: +Lemma seval_builtin_sval_args ctx lbs: forall lba m v, - eval_list_builtin_sval ge sp lbs rs0 m0 = Some lba -> - list_forall2 (eval_builtin_arg ge (fun id => id) sp m) lba v -> - seval_builtin_args ge sp m rs0 m0 lbs v. + eval_list_builtin_sval ctx lbs = Some lba -> + list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba v -> + seval_builtin_args ctx m lbs v. Proof. unfold seval_builtin_args; induction lbs; simpl; intros lba m v. - intros H; inversion H; subst; clear H. intros H; inversion H. econstructor. - - destruct (seval_builtin_sval _ _ _ _ _) eqn:SV; try congruence. - destruct (eval_list_builtin_sval _ _ _ _ _) eqn: SVL; try congruence. + - destruct (seval_builtin_sval _ _) eqn:SV; try congruence. + destruct (eval_list_builtin_sval _ _) eqn: SVL; try congruence. intros H; inversion H; subst; clear H. intros H; inversion H; subst; clear H. econstructor; eauto. eapply seval_builtin_sval_arg; eauto. Qed. -Lemma seval_builtin_args_sval ge sp m rs0 m0 lv: forall lbs, - seval_builtin_args ge sp m rs0 m0 lbs lv -> +Lemma seval_builtin_args_sval ctx m lv: forall lbs, + seval_builtin_args ctx m lbs lv -> exists lba, - eval_list_builtin_sval ge sp lbs rs0 m0 = Some lba - /\ list_forall2 (eval_builtin_arg ge (fun id => id) sp m) lba lv. + eval_list_builtin_sval ctx lbs = Some lba + /\ list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba lv. Proof. induction 1. - eexists. constructor. @@ -349,10 +355,10 @@ Proof. + constructor; assumption. Qed. -Lemma seval_builtin_sval_correct ge sp m rs0 m0: forall bs1 v bs2, - seval_builtin_arg ge sp m rs0 m0 bs1 v -> - (seval_builtin_sval ge sp bs1 rs0 m0) = (seval_builtin_sval ge sp bs2 rs0 m0) -> - seval_builtin_arg ge sp m rs0 m0 bs2 v. +Lemma seval_builtin_sval_correct ctx m: forall bs1 v bs2, + seval_builtin_arg ctx m bs1 v -> + (seval_builtin_sval ctx bs1) = (seval_builtin_sval ctx bs2) -> + seval_builtin_arg ctx m bs2 v. Proof. intros. exploit seval_builtin_arg_sval; eauto. intros (ba & X1 & X2). @@ -360,10 +366,10 @@ Proof. congruence. Qed. -Lemma eval_list_builtin_sval_correct ge sp m rs0 m0 vargs: forall lbs1, - seval_builtin_args ge sp m rs0 m0 lbs1 vargs -> - forall lbs2, (eval_list_builtin_sval ge sp lbs1 rs0 m0) = (eval_list_builtin_sval ge sp lbs2 rs0 m0) -> - seval_builtin_args ge sp m rs0 m0 lbs2 vargs. +Lemma eval_list_builtin_sval_correct ctx m vargs: forall lbs1, + seval_builtin_args ctx m lbs1 vargs -> + forall lbs2, (eval_list_builtin_sval ctx lbs1) = (eval_list_builtin_sval ctx lbs2) -> + seval_builtin_args ctx m lbs2 vargs. Proof. intros. exploit seval_builtin_args_sval; eauto. intros (ba & X1 & X2). @@ -383,164 +389,64 @@ Inductive sfval := | Sreturn: option sval -> sfval . -Definition sfind_function (ge: BTL.genv) (sp: val) (svos : sval + ident) (rs0: regset) (m0: mem): option fundef := +Definition sfind_function ctx (svos : sval + ident): option fundef := match svos with - | inl sv => SOME v <- eval_sval ge sp sv rs0 m0 IN Genv.find_funct ge v - | inr symb => SOME b <- Genv.find_symbol ge symb IN Genv.find_funct_ptr ge b + | inl sv => SOME v <- eval_sval ctx sv IN Genv.find_funct (cge ctx) v + | inr symb => SOME b <- Genv.find_symbol (cge ctx) symb IN Genv.find_funct_ptr (cge ctx) b end . -Inductive sem_sfval (ge: BTL.genv) (sp:val) stack (f: function) (rs0: regset) (m0: mem): sfval -> regset -> mem -> trace -> state -> Prop := +Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop := | exec_Sgoto pc rs m: - sem_sfval ge sp stack f rs0 m0 (Sgoto pc) rs m E0 (State stack f sp pc rs m) + sem_sfval ctx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc rs m) | exec_Sreturn stk osv rs m m' v: - sp = (Vptr stk Ptrofs.zero) -> - Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - match osv with Some sv => eval_sval ge sp sv rs0 m0 | None => Some Vundef end = Some v -> - sem_sfval ge sp stack f rs0 m0 (Sreturn osv) rs m - E0 (Returnstate stack v m') + (csp ctx) = (Vptr stk Ptrofs.zero) -> + Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' -> + match osv with Some sv => eval_sval ctx sv | None => Some Vundef end = Some v -> + sem_sfval ctx (Sreturn osv) rs m + E0 (Returnstate (cstk ctx) v m') | exec_Scall rs m sig svos lsv args res pc fd: - sfind_function ge sp svos rs0 m0 = Some fd -> + sfind_function ctx svos = Some fd -> funsig fd = sig -> - eval_list_sval ge sp lsv rs0 m0 = Some args -> - sem_sfval ge sp stack f rs0 m0 (Scall sig svos lsv res pc) rs m - E0 (Callstate (Stackframe res f sp pc rs :: stack) fd args m) + eval_list_sval ctx lsv = Some args -> + sem_sfval ctx (Scall sig svos lsv res pc) rs m + E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc rs :: (cstk ctx)) fd args m) | exec_Stailcall stk rs m sig svos args fd m' lsv: - sfind_function ge sp svos rs0 m0 = Some fd -> + sfind_function ctx svos = Some fd -> funsig fd = sig -> - sp = Vptr stk Ptrofs.zero -> - Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - eval_list_sval ge sp lsv rs0 m0 = Some args -> - sem_sfval ge sp stack f rs0 m0 (Stailcall sig svos lsv) rs m - E0 (Callstate stack fd args m') + (csp ctx) = Vptr stk Ptrofs.zero -> + Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' -> + eval_list_sval ctx lsv = Some args -> + sem_sfval ctx (Stailcall sig svos lsv) rs m + E0 (Callstate (cstk ctx) fd args m') | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs: - seval_builtin_args ge sp m rs0 m0 sargs vargs -> - external_call ef ge vargs m t vres m' -> - sem_sfval ge sp stack f rs0 m0 (Sbuiltin ef sargs res pc) rs m - t (State stack f sp pc (regmap_setres res vres rs) m') + seval_builtin_args ctx m sargs vargs -> + external_call ef (cge ctx) vargs m t vres m' -> + sem_sfval ctx (Sbuiltin ef sargs res pc) rs m + t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres rs) m') | exec_Sjumptable sv tbl pc' n rs m: - eval_sval ge sp sv rs0 m0 = Some (Vint n) -> + eval_sval ctx sv = Some (Vint n) -> list_nth_z tbl (Int.unsigned n) = Some pc' -> - sem_sfval ge sp stack f rs0 m0 (Sjumptable sv tbl) rs m - E0 (State stack f sp pc' rs m) + sem_sfval ctx (Sjumptable sv tbl) rs m + E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' rs m) . -(** * Preservation properties *) - -Section SymbValPreserved. - -Variable ge ge': BTL.genv. - -Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s. - -Hypothesis senv_preserved_BTL: Senv.equiv ge ge'. - -Lemma senv_find_symbol_preserved id: - Senv.find_symbol ge id = Senv.find_symbol ge' id. -Proof. - destruct senv_preserved_BTL as (A & B & C). congruence. -Qed. - -Lemma senv_symbol_address_preserved id ofs: - Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs. -Proof. - unfold Senv.symbol_address. rewrite senv_find_symbol_preserved. - reflexivity. -Qed. - -Lemma eval_sval_preserved sp sv rs0 m0: - eval_sval ge sp sv rs0 m0 = eval_sval ge' sp sv rs0 m0. -Proof. - induction sv using sval_mut with (P0 := fun lsv => eval_list_sval ge sp lsv rs0 m0 = eval_list_sval ge' sp lsv rs0 m0) - (P1 := fun sm => eval_smem ge sp sm rs0 m0 = eval_smem ge' sp sm rs0 m0); simpl; auto. - + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _ _ _); auto. - rewrite IHsv0; clear IHsv0. destruct (eval_smem _ _ _ _); auto. - erewrite eval_operation_preserved; eauto. - + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _ _ _); auto. - erewrite <- eval_addressing_preserved; eauto. - destruct (eval_addressing _ sp _ _); auto. - rewrite IHsv; auto. - + rewrite IHsv; clear IHsv. destruct (eval_sval _ _ _ _); auto. - rewrite IHsv0; auto. - + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _ _ _); auto. - erewrite <- eval_addressing_preserved; eauto. - destruct (eval_addressing _ sp _ _); auto. - rewrite IHsv; clear IHsv. destruct (eval_smem _ _ _ _); auto. - rewrite IHsv1; auto. -Qed. - -Lemma seval_builtin_arg_preserved sp m rs0 m0: - forall bs varg, - seval_builtin_arg ge sp m rs0 m0 bs varg -> - seval_builtin_arg ge' sp m rs0 m0 bs varg. -Proof. - induction 1. - all: try (constructor; auto). - - rewrite <- eval_sval_preserved. assumption. - - rewrite <- senv_symbol_address_preserved. assumption. - - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal. -Qed. - -Lemma seval_builtin_args_preserved sp m rs0 m0 lbs vargs: - seval_builtin_args ge sp m rs0 m0 lbs vargs -> - seval_builtin_args ge' sp m rs0 m0 lbs vargs. -Proof. - induction 1; constructor; eauto. - eapply seval_builtin_arg_preserved; auto. -Qed. - -Lemma list_sval_eval_preserved sp lsv rs0 m0: - eval_list_sval ge sp lsv rs0 m0 = eval_list_sval ge' sp lsv rs0 m0. -Proof. - induction lsv; simpl; auto. - rewrite eval_sval_preserved. destruct (eval_sval _ _ _ _); auto. - rewrite IHlsv; auto. -Qed. - -Lemma smem_eval_preserved sp sm rs0 m0: - eval_smem ge sp sm rs0 m0 = eval_smem ge' sp sm rs0 m0. -Proof. - induction sm; simpl; auto. - rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _ _ _); auto. - erewrite <- eval_addressing_preserved; eauto. - destruct (eval_addressing _ sp _ _); auto. - rewrite IHsm; clear IHsm. destruct (eval_smem _ _ _ _); auto. - rewrite eval_sval_preserved; auto. -Qed. - -Lemma seval_condition_preserved sp cond lsv sm rs0 m0: - seval_condition ge sp cond lsv sm rs0 m0 = seval_condition ge' sp cond lsv sm rs0 m0. -Proof. - unfold seval_condition. - rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _ _ _); auto. - rewrite smem_eval_preserved; auto. -Qed. - -End SymbValPreserved. - (* Syntax and Semantics of symbolic internal states *) -(* [si_pre] is a precondition on initial ge, sp, rs0, m0 *) -Record sistate := { si_pre: BTL.genv -> val -> regset -> mem -> Prop; si_sreg: reg -> sval; si_smem: smem }. +(* [si_pre] is a precondition on initial context *) +Record sistate := { si_pre: iblock_exec_context -> Prop; si_sreg: reg -> sval; si_smem: smem }. -(* Predicate on which (rs, m) is a possible final state after evaluating [st] on (rs0, m0) *) -Definition sem_sistate (ge: BTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem) (rs: regset) (m: mem): Prop := - st.(si_pre) ge sp rs0 m0 - /\ eval_smem ge sp st.(si_smem) rs0 m0 = Some m - /\ forall (r:reg), eval_sval ge sp (st.(si_sreg) r) rs0 m0 = Some (rs#r). +(* Predicate on which (rs, m) is a possible final state after evaluating [st] on ((crs0 ctx), (cm0 ctx)) *) +Definition sem_sistate ctx (st: sistate) (rs: regset) (m: mem): Prop := + st.(si_pre) ctx + /\ eval_smem ctx st.(si_smem) = Some m + /\ forall (r:reg), eval_sval ctx (st.(si_sreg) r) = Some (rs#r). -Definition abort_sistate (ge: BTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem): Prop := - ~(st.(si_pre) ge sp rs0 m0) - \/ eval_smem ge sp st.(si_smem) rs0 m0 = None - \/ exists (r: reg), eval_sval ge sp (st.(si_sreg) r) rs0 m0 = None. - -Record sstate_exit := { se_sis:> sistate; se_sfv: sfval }. - -Definition sem_sexit ge (sp:val) (st: sstate_exit) stack f (rs0: regset) (m0: mem) rs m (t: trace) (s:BTL.state) := - sem_sistate ge sp st rs0 m0 rs m /\ - sem_sfval ge sp stack f rs0 m0 st.(se_sfv) rs m t s - . +Definition abort_sistate ctx (st: sistate): Prop := + ~(st.(si_pre) ctx) + \/ eval_smem ctx st.(si_smem) = None + \/ exists (r: reg), eval_sval ctx (st.(si_sreg) r) = None. (** * Symbolic execution of final step *) Definition sexec_final_sfv (i: final) (sis: sistate): sfval := @@ -567,10 +473,10 @@ Definition sexec_final_sfv (i: final) (sis: sistate): sfval := Local Hint Constructors sem_sfval: core. -Lemma sexec_final_svf_correct ge sp i f sis stack rs0 m0 t rs m s: - sem_sistate ge sp sis rs0 m0 rs m -> - final_step ge stack f sp rs m i t s -> - sem_sfval ge sp stack f rs0 m0 (sexec_final_sfv i sis) rs m t s. +Lemma sexec_final_svf_correct ctx i sis t rs m s: + sem_sistate ctx sis rs m -> + final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s -> + sem_sfval ctx (sexec_final_sfv i sis) rs m t s. Proof. intros (PRE&MEM®). destruct 1; subst; try_simplify_someHyps; simpl; intros; try autodestruct; eauto. @@ -578,9 +484,9 @@ Proof. - destruct ros; simpl in * |- *; auto. rewrite REG; auto. - erewrite eval_list_sval_inj; simpl; auto. - + (* Btailcall *) intros. eapply exec_Stailcall; auto. - - destruct ros; simpl in * |- *; auto. - rewrite REG; auto. + + (* Btailcall *) intros. eapply exec_Stailcall; eauto. + - destruct ros; simpl in * |- *; eauto. + rewrite REG; eauto. - erewrite eval_list_sval_inj; simpl; auto. + (* Bbuiltin *) intros. eapply exec_Sbuiltin; eauto. eapply seval_builtin_args_correct; eauto. @@ -590,10 +496,10 @@ Qed. Local Hint Constructors final_step: core. Local Hint Resolve seval_builtin_args_complete: core. -Lemma sexec_final_svf_complete ge sp i f sis stack rs0 m0 t rs m s: - sem_sistate ge sp sis rs0 m0 rs m -> - sem_sfval ge sp stack f rs0 m0 (sexec_final_sfv i sis) rs m t s - -> final_step ge stack f sp rs m i t s. +Lemma sexec_final_svf_complete ctx i sis t rs m s: + sem_sistate ctx sis rs m -> + sem_sfval ctx (sexec_final_sfv i sis) rs m t s + -> final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s. Proof. intros (PRE&MEM®). destruct i; simpl; intros LAST; inv LAST; eauto. @@ -615,1217 +521,19 @@ Proof. congruence. Qed. - -(* TODO: clean/recover this COPY-PASTE OF RTLpathSE_theory.v - - -(* Syntax and semantics of symbolic exit states *) - -Definition all_fallthrough ge sp (lx: list sistate_exit) rs0 m0: Prop := - forall ext, List.In ext lx -> - seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = Some false. - -Lemma all_fallthrough_revcons ge sp ext rs m lx: - all_fallthrough ge sp (ext::lx) rs m -> - seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs m = Some false - /\ all_fallthrough ge sp lx rs m. -Proof. - intros ALLFU. constructor. - - assert (In ext (ext::lx)) by (constructor; auto). apply ALLFU in H. assumption. - - intros ext' INEXT. assert (In ext' (ext::lx)) by (apply in_cons; auto). - apply ALLFU in H. assumption. -Qed. - -(** Semantic of an exit in pseudo code: - if si_cond (si_condargs) - si_elocal; goto if_so - else () -*) - -Definition ssem_exit (ge: RTL.genv) (sp: val) (ext: sistate_exit) (rs: regset) (m: mem) rs' m' (pc': node) : Prop := - seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m = Some true - /\ ssem_local ge sp (si_elocal ext) rs m rs' m' - /\ (si_ifso ext) = pc'. - -(* Either an abort on the condition evaluation OR an abort on the sistate_local IF the condition was true *) -Definition sabort_exit (ge: RTL.genv) (sp: val) (ext: sistate_exit) (rs: regset) (m: mem) : Prop := - let sev_cond := seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m in - sev_cond = None - \/ (sev_cond = Some true /\ sabort_local ge sp ext.(si_elocal) rs m). - -(** * Syntax and Semantics of symbolic internal state *) -Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local }. - -Definition all_fallthrough_upto_exit ge sp ext lx' lx rs m : Prop := - is_tail (ext::lx') lx /\ all_fallthrough ge sp lx' rs m. - -(** Semantic of a sistate in pseudo code: - si_exit1; si_exit2; ...; si_exitn; - si_local; goto si_pc *) - -(* Note: in RTLpath, is.(icontinue) = false iff we took an early exit *) - -Definition ssem_internal (ge: RTL.genv) (sp:val) (st: sistate) (rs: regset) (m: mem) (is: istate): Prop := - if (is.(icontinue)) - then - ssem_local ge sp st.(si_local) rs m is.(irs) is.(imem) - /\ st.(si_pc) = is.(ipc) - /\ all_fallthrough ge sp st.(si_exits) rs m - else exists ext lx, - ssem_exit ge sp ext rs m is.(irs) is.(imem) is.(ipc) - /\ all_fallthrough_upto_exit ge sp ext lx st.(si_exits) rs m. - -Definition sabort (ge: RTL.genv) (sp: val) (st: sistate) (rs: regset) (m: mem): Prop := - (* No early exit was met but we aborted on the si_local *) - (all_fallthrough ge sp st.(si_exits) rs m /\ sabort_local ge sp st.(si_local) rs m) - (* OR we aborted on an evaluation of one of the early exits *) - \/ (exists ext lx, all_fallthrough_upto_exit ge sp ext lx st.(si_exits) rs m /\ sabort_exit ge sp ext rs m). - -Definition ssem_internal_opt ge sp (st: sistate) rs0 m0 (ois: option istate): Prop := - match ois with - | Some is => ssem_internal ge sp st rs0 m0 is - | None => sabort ge sp st rs0 m0 - end. - -Definition ssem_internal_opt2 ge sp (ost: option sistate) rs0 m0 (ois: option istate) : Prop := - match ost with - | Some st => ssem_internal_opt ge sp st rs0 m0 ois - | None => ois=None - end. - -(** * An internal state represents a parallel program ! - - We prove below that the semantics [ssem_internal_opt] is deterministic. - - *) - -Definition istate_eq ist1 ist2 := - ist1.(icontinue) = ist2.(icontinue) /\ - ist1.(ipc) = ist2.(ipc) /\ - (forall r, (ist1.(irs)#r) = ist2.(irs)#r) /\ - ist1.(imem) = ist2.(imem). - -Lemma all_fallthrough_noexit ge sp ext lx rs0 m0 rs m pc: - ssem_exit ge sp ext rs0 m0 rs m pc -> - In ext lx -> - all_fallthrough ge sp lx rs0 m0 -> - False. -Proof. - Local Hint Resolve is_tail_in: core. - intros SSEM INE ALLF. - destruct SSEM as (SSEM & SSEM'). - unfold all_fallthrough in ALLF. rewrite ALLF in SSEM; eauto. - discriminate. -Qed. - -Lemma ssem_internal_exclude_incompatible_continue ge sp st rs m is1 is2: - is1.(icontinue) = true -> - is2.(icontinue) = false -> - ssem_internal ge sp st rs m is1 -> - ssem_internal ge sp st rs m is2 -> - False. -Proof. - Local Hint Resolve all_fallthrough_noexit: core. - unfold ssem_internal. - intros CONT1 CONT2. - rewrite CONT1, CONT2; simpl. - intuition eauto. - destruct H0 as (ext & lx & SSEME & ALLFU). - destruct ALLFU as (ALLFU & ALLFU'). - eapply all_fallthrough_noexit; eauto. -Qed. - -Lemma ssem_internal_determ_continue ge sp st rs m is1 is2: - ssem_internal ge sp st rs m is1 -> - ssem_internal ge sp st rs m is2 -> - is1.(icontinue) = is2.(icontinue). -Proof. - Local Hint Resolve ssem_internal_exclude_incompatible_continue: core. - destruct (Bool.bool_dec is1.(icontinue) is2.(icontinue)) as [|H]; auto. - intros H1 H2. assert (absurd: False); intuition. - destruct (icontinue is1) eqn: His1, (icontinue is2) eqn: His2; eauto. -Qed. - -Lemma ssem_local_determ ge sp st rs0 m0 rs1 m1 rs2 m2: - ssem_local ge sp st rs0 m0 rs1 m1 -> - ssem_local ge sp st rs0 m0 rs2 m2 -> - (forall r, rs1#r = rs2#r) /\ m1 = m2. -Proof. - unfold ssem_local. intuition try congruence. - generalize (H5 r); rewrite H4; congruence. -Qed. - -(* TODO: lemma to move in Coqlib *) -Lemma is_tail_bounded_total {A} (l1 l2 l3: list A): is_tail l1 l3 -> is_tail l2 l3 - -> is_tail l1 l2 \/ is_tail l2 l1. -Proof. - Local Hint Resolve is_tail_cons: core. - induction 1 as [|i l1 l3 T1 IND]; simpl; auto. - intros T2; inversion T2; subst; auto. -Qed. - -Lemma exit_cond_determ ge sp rs0 m0 l1 l2: - is_tail l1 l2 -> forall ext1 lx1 ext2 lx2, - l1=(ext1 :: lx1) -> - l2=(ext2 :: lx2) -> - all_fallthrough ge sp lx1 rs0 m0 -> - seval_condition ge sp (si_cond ext1) (si_scondargs ext1) (si_smem (si_elocal ext1)) rs0 m0 = Some true -> - all_fallthrough ge sp lx2 rs0 m0 -> - ext1=ext2. -Proof. - destruct 1 as [l1|i l1 l3 T1]; intros ext1 lx1 ext2 lx2 EQ1 EQ2; subst; - inversion EQ2; subst; auto. - intros D1 EVAL NYE. - Local Hint Resolve is_tail_in: core. - unfold all_fallthrough in NYE. - rewrite NYE in EVAL; eauto. - try congruence. -Qed. - -Lemma ssem_exit_determ ge sp ext rs0 m0 rs1 m1 pc1 rs2 m2 pc2: - ssem_exit ge sp ext rs0 m0 rs1 m1 pc1 -> - ssem_exit ge sp ext rs0 m0 rs2 m2 pc2 -> - pc1 = pc2 /\ (forall r, rs1#r = rs2#r) /\ m1 = m2. -Proof. - Local Hint Resolve exit_cond_determ eq_sym: core. - intros SSEM1 SSEM2. destruct SSEM1 as (SEVAL1 & SLOC1 & PCEQ1). destruct SSEM2 as (SEVAL2 & SLOC2 & PCEQ2). subst. - destruct (ssem_local_determ ge sp (si_elocal ext) rs0 m0 rs1 m1 rs2 m2); auto. -Qed. - -Remark is_tail_inv_left {A: Type} (a a': A) l l': - is_tail (a::l) (a'::l') -> - (a = a' /\ l = l') \/ (In a l' /\ is_tail l (a'::l')). -Proof. - intros. inv H. - - left. eauto. - - right. econstructor. - + eapply is_tail_in; eauto. - + eapply is_tail_cons_left; eauto. -Qed. - -Lemma ssem_internal_determ ge sp st rs m is1 is2: - ssem_internal ge sp st rs m is1 -> - ssem_internal ge sp st rs m is2 -> - istate_eq is1 is2. -Proof. - unfold istate_eq. - intros SEM1 SEM2. - exploit (ssem_internal_determ_continue ge sp st rs m is1 is2); eauto. - intros CONTEQ. unfold ssem_internal in * |-. rewrite CONTEQ in * |- *. - destruct (icontinue is2). - - destruct (ssem_local_determ ge sp (si_local st) rs m (irs is1) (imem is1) (irs is2) (imem is2)); - intuition (try congruence). - - destruct SEM1 as (ext1 & lx1 & SSEME1 & ALLFU1). destruct SEM2 as (ext2 & lx2 & SSEME2 & ALLFU2). - destruct ALLFU1 as (ALLFU1 & ALLFU1'). destruct ALLFU2 as (ALLFU2 & ALLFU2'). - destruct SSEME1 as (SSEME1 & SSEME1' & SSEME1''). destruct SSEME2 as (SSEME2 & SSEME2' & SSEME2''). - assert (X:ext1=ext2). - { destruct (is_tail_bounded_total (ext1 :: lx1) (ext2 :: lx2) (si_exits st)) as [TAIL|TAIL]; eauto. } - subst. destruct (ssem_local_determ ge sp (si_elocal ext2) rs m (irs is1) (imem is1) (irs is2) (imem is2)); auto. - intuition. congruence. -Qed. - -Lemma ssem_local_exclude_sabort_local ge sp loc rs m rs' m': - ssem_local ge sp loc rs m rs' m' -> - sabort_local ge sp loc rs m -> - False. -Proof. - intros SIML ABORT. inv SIML. destruct H0 as (H0 & H0'). - inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence. -Qed. - -Lemma ssem_local_exclude_sabort ge sp st rs m rs' m': - ssem_local ge sp (si_local st) rs m rs' m' -> - all_fallthrough ge sp (si_exits st) rs m -> - sabort ge sp st rs m -> - False. -Proof. - intros SIML ALLF ABORT. - inv ABORT. - - intuition; eapply ssem_local_exclude_sabort_local; eauto. - - destruct H as (ext & lx & ALLFU & SABORT). - destruct ALLFU as (TAIL & _). eapply is_tail_in in TAIL. - eapply ALLF in TAIL. - destruct SABORT as [CONDFAIL | (CONDTRUE & ABORTL)]; congruence. -Qed. - -Lemma ssem_exit_fallthrough_upto_exit ge sp ext ext' lx lx' exits rs m rs' m' pc': - ssem_exit ge sp ext rs m rs' m' pc' -> - all_fallthrough_upto_exit ge sp ext lx exits rs m -> - all_fallthrough_upto_exit ge sp ext' lx' exits rs m -> - is_tail (ext'::lx') (ext::lx). -Proof. - intros SSEME ALLFU ALLFU'. - destruct ALLFU as (ISTAIL & ALLFU). destruct ALLFU' as (ISTAIL' & ALLFU'). - destruct (is_tail_bounded_total (ext::lx) (ext'::lx') exits); eauto. - inv H. - - econstructor; eauto. - - eapply is_tail_in in H2. eapply ALLFU' in H2. - destruct SSEME as (SEVAL & _). congruence. -Qed. - -Lemma ssem_exit_exclude_sabort_exit ge sp ext rs m rs' m' pc': - ssem_exit ge sp ext rs m rs' m' pc' -> - sabort_exit ge sp ext rs m -> - False. -Proof. - intros A B. destruct A as (A & A' & A''). inv B. - - congruence. - - destruct H as (_ & H). eapply ssem_local_exclude_sabort_local; eauto. -Qed. - -Lemma ssem_exit_exclude_sabort ge sp ext st lx rs m rs' m' pc': - ssem_exit ge sp ext rs m rs' m' pc' -> - all_fallthrough_upto_exit ge sp ext lx (si_exits st) rs m -> - sabort ge sp st rs m -> - False. -Proof. - intros SSEM ALLFU ABORT. - inv ABORT. - - destruct H as (ALLF & _). destruct ALLFU as (TAIL & _). - eapply is_tail_in in TAIL. - destruct SSEM as (SEVAL & _ & _). - eapply ALLF in TAIL. congruence. - - destruct H as (ext' & lx' & ALLFU' & ABORT). - exploit ssem_exit_fallthrough_upto_exit; eauto. intros ITAIL. - destruct ALLFU as (ALLFU1 & ALLFU2). destruct ALLFU' as (ALLFU1' & ALLFU2'). - exploit (is_tail_inv_left ext' ext lx' lx); eauto. intro. inv H. - + inv H0. eapply ssem_exit_exclude_sabort_exit; eauto. - + destruct H0 as (INE & TAIL). eapply ALLFU2 in INE. destruct ABORT as [ABORT | (ABORT & ABORT')]; congruence. -Qed. - -Lemma ssem_internal_exclude_sabort ge sp st rs m is: - sabort ge sp st rs m -> - ssem_internal ge sp st rs m is -> False. -Proof. - intros ABORT SEM. - unfold ssem_internal in SEM. destruct icontinue. - - destruct SEM as (SEM1 & SEM2 & SEM3). - eapply ssem_local_exclude_sabort; eauto. - - destruct SEM as (ext & lx & SEM1 & SEM2). eapply ssem_exit_exclude_sabort; eauto. -Qed. - -Definition istate_eq_opt ist1 oist := - exists ist2, oist = Some ist2 /\ istate_eq ist1 ist2. - -Lemma ssem_internal_opt_determ ge sp st rs m ois is: - ssem_internal_opt ge sp st rs m ois -> - ssem_internal ge sp st rs m is -> - istate_eq_opt is ois. -Proof. - destruct ois as [is1|]; simpl; eauto. - - intros; eexists; intuition; eapply ssem_internal_determ; eauto. - - intros; exploit ssem_internal_exclude_sabort; eauto. destruct 1. -Qed. - -(** * Symbolic execution of one internal step *) - -Definition slocal_set_sreg (st:sistate_local) (r:reg) (sv:sval) := - {| si_pre:=(fun ge sp rs m => eval_sval ge sp (st.(si_sreg) r) rs m <> None /\ (st.(si_pre) ge sp rs m)); - si_sreg:=fun y => if Pos.eq_dec r y then sv else st.(si_sreg) y; - si_smem:= st.(si_smem)|}. - -Definition slocal_set_smem (st:sistate_local) (sm:smem) := - {| si_pre:=(fun ge sp rs m => eval_smem ge sp st.(si_smem) rs m <> None /\ (st.(si_pre) ge sp rs m)); - si_sreg:= st.(si_sreg); - si_smem:= sm |}. - -Definition sist_set_local (st: sistate) (pc: node) (nxt: sistate_local): sistate := - {| si_pc := pc; si_exits := st.(si_exits); si_local:= nxt |}. - -Definition slocal_store st chunk addr args src : sistate_local := - let args := list_sval_inj (List.map (si_sreg st) args) in - let src := si_sreg st src in - let sm := Sstore (si_smem st) chunk addr args src - in slocal_set_smem st sm. - -Definition siexec_inst (i: instruction) (st: sistate): option sistate := - match i with - | Inop pc' => - Some (sist_set_local st pc' st.(si_local)) - | Iop op args dst pc' => - let prev := st.(si_local) in - let vargs := list_sval_inj (List.map prev.(si_sreg) args) in - let next := slocal_set_sreg prev dst (Sop op vargs prev.(si_smem)) in - Some (sist_set_local st pc' next) - | Iload trap chunk addr args dst pc' => - let prev := st.(si_local) in - let vargs := list_sval_inj (List.map prev.(si_sreg) args) in - let next := slocal_set_sreg prev dst (Sload prev.(si_smem) trap chunk addr vargs) in - Some (sist_set_local st pc' next) - | Istore chunk addr args src pc' => - let next := slocal_store st.(si_local) chunk addr args src in - Some (sist_set_local st pc' next) - | Icond cond args ifso ifnot _ => - let prev := st.(si_local) in - let vargs := list_sval_inj (List.map prev.(si_sreg) args) in - let ex := {| si_cond:=cond; si_scondargs:=vargs; si_elocal := prev; si_ifso := ifso |} in - Some {| si_pc := ifnot; si_exits := ex::st.(si_exits); si_local := prev |} - | _ => None - end. - -Lemma slocal_set_sreg_preserves_sabort_local ge sp st rs0 m0 r sv: - sabort_local ge sp st rs0 m0 -> - sabort_local ge sp (slocal_set_sreg st r sv) rs0 m0. -Proof. - unfold sabort_local. simpl; intuition. - destruct H as [r1 H]. destruct (Pos.eq_dec r r1) as [TEST|TEST] eqn: HTEST. - - subst; rewrite H; intuition. - - right. right. exists r1. rewrite HTEST. auto. -Qed. - -Lemma slocal_set_smem_preserves_sabort_local ge sp st rs0 m0 m: - sabort_local ge sp st rs0 m0 -> - sabort_local ge sp (slocal_set_smem st m) rs0 m0. -Proof. - unfold sabort_local. simpl; intuition. -Qed. - -Lemma all_fallthrough_upto_exit_cons ge sp ext lx ext' exits rs m: - all_fallthrough_upto_exit ge sp ext lx exits rs m -> - all_fallthrough_upto_exit ge sp ext lx (ext'::exits) rs m. -Proof. - intros. inv H. econstructor; eauto. -Qed. - -Lemma all_fallthrough_cons ge sp exits rs m ext: - all_fallthrough ge sp exits rs m -> - seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs m = Some false -> - all_fallthrough ge sp (ext::exits) rs m. -Proof. - intros. unfold all_fallthrough in *. intros. - inv H1; eauto. -Qed. - -Lemma siexec_inst_preserves_sabort i ge sp rs m st st': - siexec_inst i st = Some st' -> - sabort ge sp st rs m -> sabort ge sp st' rs m. -Proof. - intros SISTEP ABORT. - destruct i; simpl in SISTEP; try discriminate; inv SISTEP; unfold sabort; simpl. - (* NOP *) - * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)]. - - left. constructor; eauto. - - right. exists ext0, lx0. constructor; eauto. - (* OP *) - * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)]. - - left. constructor; eauto. eapply slocal_set_sreg_preserves_sabort_local; eauto. - - right. exists ext0, lx0. constructor; eauto. - (* LOAD *) - * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)]. - - left. constructor; eauto. eapply slocal_set_sreg_preserves_sabort_local; eauto. - - right. exists ext0, lx0. constructor; eauto. - (* STORE *) - * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)]. - - left. constructor; eauto. eapply slocal_set_smem_preserves_sabort_local; eauto. - - right. exists ext0, lx0. constructor; eauto. - (* COND *) - * remember ({| si_cond := _; si_scondargs := _; si_elocal := _; si_ifso := _ |}) as ext. - destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)]. - - destruct (seval_condition ge sp (si_cond ext) (si_scondargs ext) - (si_smem (si_elocal ext)) rs m) eqn:SEVAL; [destruct b|]. - (* case true *) - + right. exists ext, (si_exits st). - constructor. - ++ constructor. econstructor; eauto. eauto. - ++ unfold sabort_exit. right. constructor; eauto. - subst. simpl. eauto. - (* case false *) - + left. constructor; eauto. eapply all_fallthrough_cons; eauto. - (* case None *) - + right. exists ext, (si_exits st). constructor. - ++ constructor. econstructor; eauto. eauto. - ++ unfold sabort_exit. left. eauto. - - right. exists ext0, lx0. constructor; eauto. eapply all_fallthrough_upto_exit_cons; eauto. -Qed. - -Lemma siexec_inst_WF i st: - siexec_inst i st = None -> default_succ i = None. -Proof. - destruct i; simpl; unfold sist_set_local; simpl; congruence. -Qed. - -Lemma siexec_inst_default_succ i st st': - siexec_inst i st = Some st' -> default_succ i = Some (st'.(si_pc)). -Proof. - destruct i; simpl; unfold sist_set_local; simpl; try congruence; - intro H; inversion_clear H; simpl; auto. -Qed. - - -Lemma eval_list_sval_inj_not_none ge sp st rs0 m0: forall l, - (forall r, List.In r l -> eval_sval ge sp (si_sreg st r) rs0 m0 = None -> False) -> - eval_list_sval ge sp (list_sval_inj (map (si_sreg st) l)) rs0 m0 = None -> False. -Proof. - induction l. - - intuition discriminate. - - intros ALLR. simpl. - inversion_SOME v. - + intro SVAL. inversion_SOME lv; [discriminate|]. - assert (forall r : reg, In r l -> eval_sval ge sp (si_sreg st r) rs0 m0 = None -> False). - { intros r INR. eapply ALLR. right. assumption. } - intro SVALLIST. intro. eapply IHl; eauto. - + intros. exploit (ALLR a); simpl; eauto. -Qed. - -Lemma siexec_inst_correct ge sp i st rs0 m0 rs m: - ssem_local ge sp st.(si_local) rs0 m0 rs m -> - all_fallthrough ge sp st.(si_exits) rs0 m0 -> - ssem_internal_opt2 ge sp (siexec_inst i st) rs0 m0 (istep ge i sp rs m). -Proof. - intros (PRE & MEM & REG) NYE. - destruct i; simpl; auto. - + (* Nop *) - constructor; [|constructor]; simpl; auto. - constructor; auto. - + (* Op *) - inversion_SOME v; intros OP; simpl. - - constructor; [|constructor]; simpl; auto. - constructor; simpl; auto. - * constructor; auto. congruence. - * constructor; auto. - intro r0. destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. - subst. rewrite Regmap.gss; simpl; auto. - erewrite eval_list_sval_inj; simpl; auto. - try_simplify_someHyps. - - left. constructor; simpl; auto. - unfold sabort_local. right. right. - simpl. exists r. destruct (Pos.eq_dec r r); try congruence. - simpl. erewrite eval_list_sval_inj; simpl; auto. - try_simplify_someHyps. - + (* LOAD *) - inversion_SOME a0; intro ADD. - { inversion_SOME v; intros LOAD; simpl. - - explore_destruct; unfold ssem_internal, ssem_local; simpl; intuition. - * unfold ssem_internal. simpl. constructor; [|constructor]; auto. - constructor; constructor; simpl; auto. congruence. intro r0. - destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. - subst; rewrite Regmap.gss; simpl. - erewrite eval_list_sval_inj; simpl; auto. - try_simplify_someHyps. - * unfold ssem_internal. simpl. constructor; [|constructor]; auto. - constructor; constructor; simpl; auto. congruence. intro r0. - destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. - subst; rewrite Regmap.gss; simpl. - inversion_SOME args; intros ARGS. - 2: { exploit eval_list_sval_inj_not_none; eauto; intuition congruence. } - exploit eval_list_sval_inj; eauto. intro ARGS'. erewrite ARGS in ARGS'. inv ARGS'. rewrite ADD. - inversion_SOME m2. intro SMEM. - assert (m = m2) by congruence. subst. rewrite LOAD. reflexivity. - - explore_destruct; unfold sabort, sabort_local; simpl. - * unfold sabort. simpl. left. constructor; auto. - right. right. exists r. simpl. destruct (Pos.eq_dec r r); try congruence. - simpl. erewrite eval_list_sval_inj; simpl; auto. - rewrite ADD; simpl; auto. try_simplify_eval_svalsomeHyps. - * unfold ssem_internal. simpl. constructor; [|constructor]; auto. - constructor; constructor; simpl; auto. congruence. intro r0. - destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. - subst; rewrite Regmap.gss; simpl. - erewrite eval_list_sval_inj; simpl; auto. - try_simplify_someHyps. - } { rewrite ADD. destruct t. - - simpl. left; eauto. simpl. econstructor; eauto. - right. right. simpl. exists r. destruct (Pos.eq_dec r r); [|contradiction]. - simpl. inversion_SOME args. intro SLS. - eapply eval_list_sval_inj in REG. rewrite REG in SLS. inv SLS. - rewrite ADD. reflexivity. - - simpl. constructor; [|constructor]; simpl; auto. - constructor; simpl; constructor; auto; [congruence|]. - intro r0. destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. - subst. simpl. rewrite Regmap.gss. - erewrite eval_list_sval_inj; simpl; auto. - try_simplify_someHyps. - } - + (* STORE *) - inversion_SOME a0; intros ADD. - { inversion_SOME m'; intros STORE; simpl. - - unfold ssem_internal, ssem_local; simpl; intuition. - * congruence. - * erewrite eval_list_sval_inj; simpl; auto. - erewrite REG. - try_simplify_someHyps. - - unfold sabort, sabort_local; simpl. - left. constructor; auto. right. left. - erewrite eval_list_sval_inj; simpl; auto. - erewrite REG. - try_simplify_someHyps. } - { unfold sabort, sabort_local; simpl. - left. constructor; auto. right. left.eval_sval - erewrite eval_list_sval_inj; simpl; auto. - erewrite ADD; simpl; auto. } - + (* COND *) - Local Hint Resolve is_tail_refl: core. - Local Hint Unfold ssem_local: core. - inversion_SOME b; intros COND. - { destruct b; simpl; unfold ssem_internal, ssem_local; simpl. - - remember (mk_sistate_exit _ _ _ _) as ext. exists ext, (si_exits st). - constructor; constructor; subst; simpl; auto. - unfold seval_condition. subst; simpl. - erewrite eval_list_sval_inj; simpl; auto. - try_simplify_someHyps. - - intuition. unfold all_fallthrough in * |- *. simpl. - intuition. subst. simpl. - unfold seval_condition. - erewrite eval_list_sval_inj; simpl; auto. - try_simplify_someHyps. } - { unfold sabort. simpl. right. - remember (mk_sistate_exit _ _ _ _) as ext. exists ext, (si_exits st). - constructor; [constructor; subst; simpl; auto|]. - left. subst; simpl; auto. - unfold seval_condition. - erewrite eval_list_sval_inj; simpl; auto. - try_simplify_someHyps. } -Qed. - - -Lemma siexec_inst_correct_None ge sp i st rs0 m0 rs m: - ssem_local ge sp (st.(si_local)) rs0 m0 rs m -> - siexec_inst i st = None -> - istep ge i sp rs m = None. -Proof. - intros (PRE & MEM & REG). - destruct i; simpl; unfold sist_set_local, ssem_internal, ssem_local; simpl; try_simplify_someHyps. -Qed. - -(** * Symbolic execution of the internal steps of a path *) -Fixpoint siexec_path (path:nat) (f: function) (st: sistate): option sistate := - match path with - | O => Some st - | S p => - SOME i <- (fn_code f)!(st.(si_pc)) IN - SOME st1 <- siexec_inst i st IN - siexec_path p f st1 - end. - -Lemma siexec_inst_add_exits i st st': - siexec_inst i st = Some st' -> - ( si_exits st' = si_exits st \/ exists ext, si_exits st' = ext :: si_exits st ). -Proof. - destruct i; simpl; intro SISTEP; inversion_clear SISTEP; unfold siexec_inst; simpl; (discriminate || eauto). -Qed. - -Lemma siexec_inst_preserves_allfu ge sp ext lx rs0 m0 st st' i: - all_fallthrough_upto_exit ge sp ext lx (si_exits st) rs0 m0 -> - siexec_inst i st = Some st' -> - all_fallthrough_upto_exit ge sp ext lx (si_exits st') rs0 m0. -Proof. - intros ALLFU SISTEP. destruct ALLFU as (ISTAIL & ALLF). - constructor; eauto. - destruct i; simpl in SISTEP; inversion_clear SISTEP; simpl; (discriminate || eauto). -Qed. - -Lemma siexec_path_correct_false ge sp f rs0 m0 st' is: - forall path, - is.(icontinue)=false -> - forall st, ssem_internal ge sp st rs0 m0 is -> - siexec_path path f st = Some st' -> - ssem_internal ge sp st' rs0 m0 is. -Proof. - induction path; simpl. - - intros. congruence. - - intros ICF st SSEM STEQ'. - destruct ((fn_code f) ! (si_pc st)) eqn:FIC; [|discriminate]. - destruct (siexec_inst _ _) eqn:SISTEP; [|discriminate]. - eapply IHpath. 3: eapply STEQ'. eauto. - unfold ssem_internal in SSEM. rewrite ICF in SSEM. - destruct SSEM as (ext & lx & SEXIT & ALLFU). - unfold ssem_internal. rewrite ICF. exists ext, lx. - constructor; auto. eapply siexec_inst_preserves_allfu; eauto. -Qed. - -Lemma siexec_path_preserves_sabort ge sp path f rs0 m0 st': forall st, - siexec_path path f st = Some st' -> - sabort ge sp st rs0 m0 -> sabort ge sp st' rs0 m0. -Proof. - Local Hint Resolve siexec_inst_preserves_sabort: core. - induction path; simpl. - + unfold sist_set_local; try_simplify_someHyps. - + intros st; inversion_SOME i. - inversion_SOME st1; eauto. -Qed. - -Lemma siexec_path_WF path f: forall st, - siexec_path path f st = None -> nth_default_succ (fn_code f) path st.(si_pc) = None. -Proof. - induction path; simpl. - + unfold sist_set_local. intuition congruence. - + intros st; destruct ((fn_code f) ! (si_pc st)); simpl; try tauto. - destruct (siexec_inst i st) as [st1|] eqn: Hst1; simpl. - - intros; erewrite siexec_inst_default_succ; eauto. - - intros; erewrite siexec_inst_WF; eauto. -Qed. - -Lemma siexec_path_default_succ path f st': forall st, - siexec_path path f st = Some st' -> nth_default_succ (fn_code f) path st.(si_pc) = Some st'.(si_pc). -Proof. - induction path; simpl. - + unfold sist_set_local. intros st H. inversion_clear H; simpl; try congruence. - + intros st; destruct ((fn_code f) ! (si_pc st)); simpl; try congruence. - destruct (siexec_inst i st) as [st1|] eqn: Hst1; simpl; try congruence. - intros; erewrite siexec_inst_default_succ; eauto. -Qed. - -Lemma siexec_path_correct_true ge sp path (f:function) rs0 m0: forall st is, - is.(icontinue)=true -> - ssem_internal ge sp st rs0 m0 is -> - nth_default_succ (fn_code f) path st.(si_pc) <> None -> - ssem_internal_opt2 ge sp (siexec_path path f st) rs0 m0 - (isteps ge path f sp is.(irs) is.(imem) is.(ipc)) - . -Proof. - Local Hint Resolve siexec_path_correct_false siexec_path_preserves_sabort siexec_path_WF: core. - induction path; simpl. - + intros st is CONT INV WF; - unfold ssem_internal, sist_set_local in * |- *; - try_simplify_someHyps. simpl. - destruct is; simpl in * |- *; subst; intuition auto. - + intros st is CONT; unfold ssem_internal at 1; rewrite CONT. - intros (LOCAL & PC & NYE) WF. - rewrite <- PC. - inversion_SOME i; intro Hi; rewrite Hi in WF |- *; simpl; auto. - exploit siexec_inst_correct; eauto. - inversion_SOME st1; intros Hst1; erewrite Hst1; simpl. - - inversion_SOME is1; intros His1;rewrite His1; simpl. - * destruct (icontinue is1) eqn:CONT1. - (* icontinue is0 = true *) - intros; eapply IHpath; eauto. - destruct i; simpl in * |- *; unfold sist_set_local in * |- *; try_simplify_someHyps. - (* icontinue is0 = false -> EARLY EXIT *) - destruct (siexec_path path f st1) as [st2|] eqn: Hst2; simpl; eauto. - destruct WF. erewrite siexec_inst_default_succ; eauto. - (* try_simplify_someHyps; eauto. *) - * destruct (siexec_path path f st1) as [st2|] eqn: Hst2; simpl; eauto. - - intros His1;rewrite His1; simpl; auto. -Qed. - -(** REM: in the following two unused lemmas *) - -Lemma siexec_path_right_assoc_decompose f path: forall st st', - siexec_path (S path) f st = Some st' -> - exists st0, siexec_path path f st = Some st0 /\ siexec_path 1%nat f st0 = Some st'. -Proof. - induction path; simpl; eauto. - intros st st'. - inversion_SOME i1. - inversion_SOME st1. - try_simplify_someHyps; eauto. -Qed. - -Lemma siexec_path_right_assoc_compose f path: forall st st0 st', - siexec_path path f st = Some st0 -> - siexec_path 1%nat f st0 = Some st' -> - siexec_path (S path) f st = Some st'. -Proof. - induction path. - + intros st st0 st' H. simpl in H. - try_simplify_someHyps; auto. - + intros st st0 st'. - assert (X:exists x, x=(S path)); eauto. - destruct X as [x X]. - intros H1 H2. rewrite <- X. - generalize H1; clear H1. simpl. - inversion_SOME i1. intros Hi1; rewrite Hi1. - inversion_SOME st1. intros Hst1; rewrite Hst1. - subst; eauto. -Qed. - - -(** * Main function of the symbolic execution *) - -Definition init_sistate_local := {| si_pre:= fun _ _ _ _ => True; si_sreg:= fun r => Sinput r; si_smem:= Sinit |}. - -Definition init_sistate pc := {| si_pc:= pc; si_exits:=nil; si_local:= init_sistate_local |}. - -Lemma init_ssem_internal ge sp pc rs m: ssem_internal ge sp (init_sistate pc) rs m (mk_istate true pc rs m). -Proof. - unfold ssem_internal, ssem_local, all_fallthrough; simpl. intuition. -Qed. - -Definition sexec (f: function) (pc:node): option sstate := - SOME path <- (fn_path f)!pc IN - SOME st <- siexec_path path.(psize) f (init_sistate pc) IN - SOME i <- (fn_code f)!(st.(si_pc)) IN - Some (match siexec_inst i st with - | Some st' => {| internal := st'; final := Snone |} - | None => {| internal := st; final := sexec_final i st.(si_local) |} - end). - -Lemma final_node_path_simpl f path pc: - (fn_path f)!pc = Some path -> nth_default_succ_inst (fn_code f) path.(psize) pc <> None. -Proof. - intros; exploit final_node_path; eauto. - intros (i & NTH & DUM). - congruence. -Qed. - -Lemma symb_path_last_step i st st' ge pge stack (f:function) sp pc rs m t s: - (fn_code f) ! pc = Some i -> - pc = st.(si_pc) -> - siexec_inst i st = Some st' -> - path_last_step ge pge stack f sp pc rs m t s -> - exists mk_istate, - istep ge i sp rs m = Some mk_istate - /\ t = E0 - /\ s = (State stack f sp mk_istate.(ipc) mk_istate.(RTLpath.irs) mk_istate.(imem)). -Proof. - intros PC1 PC2 Hst' LAST; destruct LAST; subst; try_simplify_someHyps; simpl. -Qed. - -(* NB: each concrete execution can be executed on the symbolic state (produced from [sexec]) -(sexec is a correct over-approximation) -*) -Theorem sexec_correct f pc pge ge sp path stack rs m t s: - (fn_path f)!pc = Some path -> - path_step ge pge path.(psize) stack f sp rs m pc t s -> - exists st, sexec f pc = Some st /\ ssem pge ge sp st stack f rs m t s. -Proof. - Local Hint Resolve init_ssem_internal: core. - intros PATH STEP; unfold sexec; rewrite PATH; simpl. - lapply (final_node_path_simpl f path pc); eauto. intro WF. - exploit (siexec_path_correct_true ge sp path.(psize) f rs m (init_sistate pc) (mk_istate true pc rs m)); simpl; eauto. - { intros ABS. apply WF; unfold nth_default_succ_inst. rewrite ABS; auto. } - (destruct (nth_default_succ_inst (fn_code f) path.(psize) pc) as [i|] eqn: Hi; [clear WF|congruence]). - destruct STEP as [sti STEPS CONT|sti t s STEPS CONT LAST]; - (* intro Hst *) - (rewrite STEPS; unfold ssem_internal_opt2; destruct (siexec_path _ _ _) as [st|] eqn: Hst; try congruence); - (* intro SEM *) - (simpl; unfold ssem_internal; simpl; rewrite CONT; intro SEM); - (* intro Hi' *) - ( assert (Hi': (fn_code f) ! (si_pc st) = Some i); - [ unfold nth_default_succ_inst in Hi; - exploit siexec_path_default_succ; eauto; simpl; - intros DEF; rewrite DEF in Hi; auto - | clear Hi; rewrite Hi' ]); - (* eexists *) - (eexists; constructor; eauto). - - (* early *) - eapply ssem_early; eauto. - unfold ssem_internal; simpl; rewrite CONT. - destruct (siexec_inst i st) as [st'|] eqn: Hst'; simpl; eauto. - destruct SEM as (ext & lx & SEM & ALLFU). exists ext, lx. - constructor; auto. eapply siexec_inst_preserves_allfu; eauto. - - destruct SEM as (SEM & PC & HNYE). - destruct (siexec_inst i st) as [st'|] eqn: Hst'; simpl. - + (* normal on Snone *) - rewrite <- PC in LAST. - exploit symb_path_last_step; eauto; simpl. - intros (mk_istate & ISTEP & Ht & Hs); subst. - exploit siexec_inst_correct; eauto. simpl. - erewrite Hst', ISTEP; simpl. - clear LAST CONT STEPS PC SEM HNYE Hst Hi' Hst' ISTEP st sti i. - intro SEM; destruct (mk_istate.(icontinue)) eqn: CONT. - { (* icontinue mk_istate = true *) - eapply ssem_normal; simpl; eauto. - unfold ssem_internal in SEM. - rewrite CONT in SEM.eval_sval - destruct SEM as (SEM & PC & HNYE). - rewrite <- PC. - eapply exec_Snone. } - { eapply ssem_early; eauto. } - + (* normal non-Snone instruction *) - eapply ssem_normal; eauto. - * unfold ssem_internal; simpl; rewrite CONT; intuition. - * simpl. eapply sexec_final_correct; eauto. - rewrite PC; auto. -Qed. - -(* TODO: déplacer les trucs sur equiv_stackframe dans RTLpath ? *) -Inductive equiv_stackframe: stackframe -> stackframe -> Prop := - | equiv_stackframe_intro res f sp pc rs1 rs2 - (EQUIV: forall r : positive, rs1 !! r = rs2 !! r): - equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2). - -Inductive equiv_state: state -> state -> Prop := - | State_equiv stack f sp pc rs1 m rs2 - (EQUIV: forall r, rs1#r = rs2#r): - equiv_state (State stack f sp pc rs1 m) (State stack f sp pc rs2 m) - | Call_equiv stk stk' f args m - (STACKS: list_forall2 equiv_stackframe stk stk'): - equiv_state (Callstate stk f args m) (Callstate stk' f args m) - | Return_equiv stk stk' v m - (STACKS: list_forall2 equiv_stackframe stk stk'): - equiv_state (Returnstate stk v m) (Returnstate stk' v m). - -Lemma equiv_stackframe_refl stf: equiv_stackframeeval_sval stf stf. -Proof. - destruct stf. constructor; auto. -Qed. - -Lemma equiv_stack_refl stk: list_forall2 equiv_stackframe stk stk. -Proof. - Local Hint Resolve equiv_stackframe_refl: core. - induction stk; simpl; constructor; auto. -Qed.eval_sval - -Lemma equiv_state_refl s: equiv_state s s. -Proof. - Local Hint Resolve equiv_stack_refl: core. - induction s; simpl; constructor; auto. -Qed. - -(* -Lemma equiv_stackframe_trans stf1 stf2 stf3: - equiv_stackframe stf1 stf2 -> equiv_stackframe stf2 stf3 -> equiv_stackframe stf1 stf3. -Proof. - destruct 1; intros EQ; inv EQ; try econstructor; eauto. - intros; eapply eq_trans; eauto. -Qed. - -Lemma equiv_stack_trans stk1 stk2: - list_forall2 equiv_stackframe stk1 stk2 -> - forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> - list_forall2 equiv_stackframe stk1 stk3. -Proof. - Local Hint Resolve equiv_stackframe_trans. - induction 1; intros stk3 EQ; inv EQ; econstructor; eauto. -Qed. - -Lemma equiv_state_trans s1 s2 s3: equiv_state s1 s2 -> equiv_state s2 s3 -> equiv_state s1 s3. -Proof. - Local Hint Resolve equiv_stack_trans. - destruct 1; intros EQ; inv EQ; econstructor; eauto. - intros; eapply eq_trans; eauto. -Qed. -*) - -Lemma regmap_setres_eq (rs rs': regset) res vres: - (forall r, rs # r = rs' # r) -> - forall r, (regmap_setres res vres rs) # r = (regmap_setres res vres rs') # r. -Proof. - intros RSEQ r. destruct res; simpl; try congruence. - destruct (peq x r). - - subst. repeat (rewrite Regmap.gss). reflexivity. - - repeat (rewrite Regmap.gso); auto. -Qed. - -Lemma sem_sfval_equiv pge ge sp (f:function) st sv stack rs0 m0 t rs1 rs2 m s: - sem_sfval pge ge sp st stack f rs0 m0 sv rs1 m t s -> - (forall r, rs1#r = rs2#r) -> - exists s', equiv_state s s' /\ sem_sfval pge ge sp st stack f rs0 m0 sv rs2 m t s'. -Proof. eval_sval - Local Hint Resolve equiv_stack_refl: core. - destruct 1. - - (* Snone *) intros; eexists; econstructor. - + eapply State_equiv; eauto. - + eapply exec_Snone. - - (* Scall *) - intros; eexists; econstructor. - 2: { eapply exec_Scall; eauto. } - apply Call_equiv; auto. - repeat (constructor; auto). - - (* Stailcall *) - intros; eexists; econstructor; [| eapply exec_Stailcall; eauto]. - apply Call_equiv; auto. - - (* Sbuiltin *) - intros; eexists; econstructor; [| eapply exec_Sbuiltin; eauto]. - constructor. eapply regmap_setres_eq; eauto. - - (* Sjumptable *) - intros; eexists; econstructor; [| eapply exec_Sjumptable; eauto]. - constructor. assumption. - - (* Sreturn *) - intros; eexists; econstructor; [| eapply exec_Sreturn; eauto]. - eapply equiv_state_refl; eauto. -Qed. - -Lemma siexec_inst_early_exit_absurd i st st' ge sp rs m rs' m' pc': - siexec_inst i st = Some st' -> - (exists ext lx, ssem_exit ge sp ext rs m rs' m' pc' /\ - all_fallthrough_upto_exit ge sp ext lx (si_exits st) rs m) -> - all_fallthrough ge sp (si_exits st') rs m -> - False. -Proof. - intros SIEXEC (ext & lx & SSEME & ALLFU) ALLF. destruct ALLFU as (TAIL & _). - exploit siexec_inst_add_exits; eauto. destruct 1 as [SIEQ | (ext0 & SIEQ)]. - - rewrite SIEQ in *. eapply all_fallthrough_noexit. eauto. 2: eapply ALLF. eapply is_tail_in. eassumption. - - rewrite SIEQ in *. eapply all_fallthrough_noexit. eauto. 2: eapply ALLF. eapply is_tail_in. - constructor. eassumption. -Qed. -eval_sval -Lemma is_tail_false {A: Type}: forall (l: list A) a, is_tail (a::l) nil -> False. -Proof. - intros. eapply is_tail_incl in H. unfold incl in H. pose (H a). - assert (In a (a::l)) by (constructor; auto). assert (In a nil) by auto. apply in_nil in H1. - contradiction. -Qed. - -Lemma cons_eq_false {A: Type}: forall (l: list A) a, - a :: l = l -> False. -Proof. - induction l; intros. - - discriminate. - - inv H. apply IHl in H2. contradiction. -Qed. - -Lemma app_cons_nil_eq {A: Type}: forall l' l (a:A), - (l' ++ a :: nil) ++ l = l' ++ a::l. -Proof. - induction l'; intros. - - simpl. reflexivity. - - simpl. rewrite IHl'. reflexivity. -Qed. - -Lemma app_eq_false {A: Type}: forall l (l': list A) a, - l' ++ a :: l = l -> False. -Proof. - induction l; intros. - - apply app_eq_nil in H. destruct H as (_ & H). apply cons_eq_false in H. contradiction. - - destruct l' as [|a' l']. - + simpl in H. apply cons_eq_false in H. contradiction. - + rewrite <- app_comm_cons in H. inv H. - apply (IHl (l' ++ (a0 :: nil)) a). rewrite app_cons_nil_eq. assumption. -Qed. - -Lemma is_tail_false_gen {A: Type}: forall (l: list A) l' a, is_tail (l'++(a::l)) l -> False. -Proof. - induction l. - - intros. destruct l' as [|a' l']. - + simpl in H. apply is_tail_false in H. contradiction. - + rewrite <- app_comm_cons in H. apply is_tail_false in H. contradiction. - - intros. inv H. - + apply app_eq_false in H2. contradiction. - + apply (IHl (l' ++ (a0 :: nil)) a). rewrite app_cons_nil_eq. assumption. -Qed. - -Lemma is_tail_eq {A: Type}: forall (l l': list A), - is_tail l' l -> - is_tail l l' -> - l = l'. -Proof. - destruct l as [|a l]; intros l' ITAIL ITAIL'. - - destruct l' as [|i' l']; auto. apply is_tail_false in ITAIL. contradiction. - - inv ITAIL; auto. - destruct l' as [|i' l']. { apply is_tail_false in ITAIL'. contradiction. } - exploit is_tail_trans. eapply ITAIL'. eauto. intro ABSURD. - apply (is_tail_false_gen l nil a) in ABSURD. contradiction. -Qed. - -(* NB: each execution of a symbolic state (produced from [sexec]) represents a concrete execution - (sexec is exact). -*) -Theorem sexec_exact f pc pge ge sp path stack st rs m t s1: - (fn_path f)!pc = Some path -> - sexec f pc = Some st -> - ssem pge ge sp st stack f rs m t s1 -> - exists s2, path_step ge pge path.(psize) stack f sp rs m pc t s2 /\ - equiv_state s1 s2. -Proof. - Local Hint Resolve init_ssem_internal: core. - unfold sexec; intros PATH SSTEP SEM; rewrite PATH in SSTEP. - lapply (final_node_path_simpl f path pc); eauto. intro WF. - exploit (siexec_path_correct_true ge sp path.(psize) f rs m (init_sistate pc) (mk_istate true pc rs m)); simpl; eauto. - { intros ABS. apply WF; unfold nth_default_succ_inst. rewrite ABS; auto. } - (destruct (nth_default_succ_inst (fn_code f) path.(psize) pc) as [i|] eqn: Hi; [clear WF|congruence]). - unfold nth_default_succ_inst in Hi. - destruct (siexec_path path.(psize) f (init_sistate pc)) as [st0|] eqn: Hst0; simpl. - 2:{ (* absurd case *) - exploit siexec_path_WF; eauto. - simpl; intros NDS; rewrite NDS in Hi; congruence. } - exploit siexec_path_default_succ;eval_sval eauto; simpl. - intros NDS; rewrite NDS in Hi. - rewrite Hi in SSTEP. - intros ISTEPS. try_simplify_someHyps. - destruct (siexec_inst i st0) as [st'|] eqn:Hst'; simpl. - + (* exit on Snone instruction *) - assert (SEM': t = E0 /\ exists is, ssem_internal ge sp st' rs m is - /\ s1 = (State stack f sp (if (icontinue is) then (si_pc st') else (ipc is)) (irs is) (imem is))). - { destruct SEM as [is CONT SEM|is t s CONT SEM1 SEM2]; simpl in * |- *. - - repeat (econstructor; eauto). - rewrite CONT; eauto. - - inversion SEM2. repeat (econstructor; eauto). - rewrite CONT; eauto. } - clear SEM; subst. destruct SEM' as [X (is & SEM & X')]; subst. - intros. - destruct (isteps ge (psize path) f sp rs m pc) as [is0|] eqn:RISTEPS; simpl in *. - * unfold ssem_internal in ISTEPS. destruct (icontinue is0) eqn: ICONT0. - ** (* icontinue is0=true: path_step by normal_exit *) - destruct ISTEPS as (SEMis0&H1&H2). - rewrite H1 in * |-. - exploit siexec_inst_correct; eauto. - rewrite Hst'; simpl. - intros; exploit ssem_internal_opt_determ; eauto. - destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4). - eexists. econstructor 1. - *** eapply exec_normal_exit; eauto. - eapply exec_istate; eauto. - *** rewrite EQ1. - enough ((ipc st) = (if icontinue st then si_pc st' else ipc is)) as ->. - { rewrite EQ2, EQ4. eapply State_equiv; auto. } - destruct (icontinue st) eqn:ICONT; auto. - exploit siexec_inst_default_succ; eauto. - erewrite istep_normal_exit; eauto. - try_simplify_someHyps. - ** (* The concrete execution has not reached "i" => early exit *) - unfold ssem_internal in SEM. - destruct (icontinue is) eqn:ICONT. - { destruct SEM as (SEML & SIPC & ALLF). - exploit siexec_inst_early_exit_absurd; eauto. contradiction. } - - eexists. econstructor 1. - *** eapply exec_early_exit; eauto. - *** destruct ISTEPS as (ext & lx & SSEME & ALLFU). destruct SEM as (ext' & lx' & SSEME' & ALLFU'). - eapply siexec_inst_preserves_allfu in ALLFU; eauto. - exploit ssem_exit_fallthrough_upto_exit; eauto. - exploit ssem_exit_fallthrough_upto_exit. eapply SSEME. eapply ALLFU. eapply ALLFU'. - intros ITAIL ITAIL'. apply is_tail_eq in ITAIL; auto. clear ITAIL'. - inv ITAIL. exploit ssem_exit_determ. eapply SSEME. eapply SSEME'. intros (IPCEQ & IRSEQ & IMEMEQ). - rewrite <- IPCEQ. rewrite <- IMEMEQ. constructor. congruence. - * (* The concrete execution has not reached "i" => abort case *) - eapply siexec_inst_preserves_sabort in ISTEPS; eauto. - exploit ssem_internal_exclude_sabort; eauto. contradiction. - + destruct SEM as [is CONT SEM|is t s CONT SEM1 SEM2]; simpl in * |- *. - - (* early exit *) - intros. - exploit ssem_internal_opt_determ; eauto. - destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4). - eexists. econstructor 1. - * eapply exec_early_exit; eauto. - * rewrite EQ2, EQ4; eapply State_equiv. auto. - - (* normal exit non-Snone instruction *) - intros. - exploit ssem_internal_opt_determ; eauto. - destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4). - unfold ssem_internal in SEM1. - rewrite CONT in SEM1. destruct SEM1 as (SEM1 & PC0 & NYE0). - exploit sem_sfval_equiv; eauto. - clear SEM2; destruct 1 as (s' & Ms' & SEM2). - rewrite ! EQ4 in * |-; clear EQ4. - rewrite ! EQ2 in * |-; clear EQ2. - exists s'; intuition. - eapply exec_normal_exit; eauto. - eapply sexec_final_complete; eauto. - * congruence. - * unfold ssem_local in * |- *. - destruct SEM1 as (A & B & C). constructor; [|constructor]; eauto. - intro r. congruence. - * congruence. -Qed. - -Require Import RTLpathLivegen RTLpathLivegenproof. - -(** * DEFINITION OF SIMULATION BETWEEN (ABSTRACT) SYMBOLIC EXECUTIONS -*) - -Definition istate_simulive alive (srce: PTree.t node) (is1 is2: istate): Prop := - is1.(icontinue) = is2.(icontinue) - /\ eqlive_reg alive is1.(irs) is2.(irs) - /\ is1.(imem) = is2.(imem). - -Definition istate_simu f (srce: PTree.t node) outframe is1 is2: Prop := - if is1.(icontinue) then - istate_simulive (fun r => Regset.In r outframe) srce is1 is2 - else - exists path, f.(fn_path)!(is1.(ipc)) = Some path - /\ istate_simulive (fun r => Regset.In r path.(input_regs)) srce is1 is2 - /\ srce!(is2.(ipc)) = Some is1.(ipc). - -Record simu_proof_context {f1: RTLpath.function} := { - liveness_hyps: liveness_ok_function f1; - the_ge1: RTL.genv; - the_ge2: RTL.genv; - genv_match: forall s, Genv.find_symbol the_ge1 s = Genv.find_symbol the_ge2 s; - the_sp: val; - the_rs0: regset; - the_m0: mem -}. -Arguments simu_proof_context: clear implicits. - -(* NOTE: a pure semantic definition on [sistate], for a total freedom in refinements *) -Definition sistate_simu (dm: PTree.t node) (f: RTLpath.function) outframe (st1 st2: sistate) (ctx: simu_proof_context f): Prop := - forall is1, ssem_internal (the_ge1 ctx) (the_sp ctx) st1 (the_rs0 ctx) (the_m0 ctx) is1 -> - exists is2, ssem_internal (the_ge2 ctx) (the_sp ctx) st2 (the_rs0 ctx) (the_m0 ctx) is2 - /\ istate_simu f dm outframe is1 is2. - -Inductive svident_simu (f: RTLpath.function) (ctx: simu_proof_context f): (sval + ident) -> (sval + ident) -> Prop := - | Sleft_simu sv1 sv2: - (eval_sval (the_ge1 ctx) (the_sp ctx) sv1 (the_rs0 ctx) (the_m0 ctx)) = (eval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx)) - -> svident_simu f ctx (inl sv1) (inl sv2) - | Sright_simu id1 id2: - id1 = id2 - -> svident_simu f ctx (inr id1) (inr id2) +(* symbolic state *) +Inductive sstate := + | Sfinal (sis: sistate) (sfv: sfval) + | Scond (cond: condition) (args: list_sval) (sm: smem) (ifso ifnot: sstate) + . + +Inductive sem_internal_sstate ctx rs m t s: sstate -> Prop := + | sem_Sfinal sis sfv + (SIS: sem_sistate ctx sis rs m) + (SFV: sem_sfval ctx sfv rs m t s) + : sem_internal_sstate ctx rs m t s (Sfinal sis sfv) + | sem_Scond b cond args sm ifso ifnot + (SEVAL: seval_condition ctx cond args sm = Some b) + (SELECT: sem_internal_sstate ctx rs m t s (if b then ifso else ifnot)) + : sem_internal_sstate ctx rs m t s (Scond cond args sm ifso ifnot) . - - -Fixpoint ptree_get_list (pt: PTree.t node) (lp: list positive) : option (list positive) := - match lp with - | nil => Some nil - | p1::lp => SOME p2 <- pt!p1 IN - SOME lp2 <- (ptree_get_list pt lp) IN - Some (p2 :: lp2) - end. - -Lemma ptree_get_list_nth dm p2: forall lp2 lp1, - ptree_get_list dm lp2 = Some lp1 -> - forall n, list_nth_z lp2 n = Some p2 -> - exists p1, - list_nth_z lp1 n = Some p1 /\ dm ! p2 = Some p1. -Proof. - induction lp2. - - simpl. intros. inv H. simpl in *. discriminate. - - intros lp1 PGL n LNZ. simpl in PGL. explore. - inv LNZ. destruct (zeq n 0) eqn:ZEQ. - + subst. inv H0. exists n0. simpl; constructor; auto. - + exploit IHlp2; eauto. intros (p1 & LNZ & DMEQ). - eexists. simpl. rewrite ZEQ. - constructor; eauto. -Qed. - -Lemma ptree_get_list_nth_rev dm p1: forall lp2 lp1, - ptree_get_list dm lp2 = Some lp1 -> - forall n, list_nth_z lp1 n = Some p1 -> - exists p2, - list_nth_z lp2 n = Some p2 /\ dm ! p2 = Some p1. -Proof. - induction lp2. - - simpl. intros. inv H. simpl in *. discriminate. - - intros lp1 PGL n LNZ. simpl in PGL. explore. - inv LNZ. destruct (zeq n 0) eqn:ZEQ. - + subst. inv H0. exists a. simpl; constructor; auto. - + exploit IHlp2; eauto. intros (p2 & LNZ & DMEQ). - eexists. simpl. rewrite ZEQ. - constructor; eauto. congruence. -Qed. - -(* NOTE: we need to mix semantical simulation and syntactic definition on [sfval] in order to abstract the [match_states] *) -Inductive sfval_simu (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node) (ctx: simu_proof_context f): sfval -> sfval -> Prop := - | Snone_simu: - dm!opc2 = Some opc1 -> - sfval_simu dm f opc1 opc2 ctx Snone Snone - | Scall_simu sig svos1 svos2 lsv1 lsv2 res pc1 pc2: - dm!pc2 = Some pc1 -> - svident_simu f ctx svos1 svos2 -> - (eval_list_sval (the_ge1 ctx) (the_sp ctx) lsv1 (the_rs0 ctx) (the_m0 ctx)) - = (eval_list_sval (the_ge2 ctx) (the_sp ctx) lsv2 (the_rs0 ctx) (the_m0 ctx)) -> - sfval_simu dm f opc1 opc2 ctx (Scall sig svos1 lsv1 res pc1) (Scall sig svos2 lsv2 res pc2) - | Stailcall_simu sig svos1 svos2 lsv1 lsv2: - svident_simu f ctx svos1 svos2 -> - (eval_list_sval (the_ge1 ctx) (the_sp ctx) lsv1 (the_rs0 ctx) (the_m0 ctx)) - = (eval_list_sval (the_ge2 ctx) (the_sp ctx) lsv2 (the_rs0 ctx) (the_m0 ctx)) -> - sfval_simu dm f opc1 opc2 ctx (Stailcall sig svos1 lsv1) (Stailcall sig svos2 lsv2) - | Sbuiltin_simu ef lbs1 lbs2 br pc1 pc2: - dm!pc2 = Some pc1 -> - (eval_list_builtin_sval (the_ge1 ctx) (the_sp ctx) lbs1 (the_rs0 ctx) (the_m0 ctx)) - = (eval_list_builtin_sval (the_ge2 ctx) (the_sp ctx) lbs2 (the_rs0 ctx) (the_m0 ctx)) -> - sfval_simu dm f opc1 opc2 ctx (Sbuiltin ef lbs1 br pc1) (Sbuiltin ef lbs2 br pc2) - | Sjumptable_simu sv1 sv2 lpc1 lpc2: - ptree_get_list dm lpc2 = Some lpc1 -> - (eval_sval (the_ge1 ctx) (the_sp ctx) sv1 (the_rs0 ctx) (the_m0 ctx)) - = (eval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx)) -> - sfval_simu dm f opc1 opc2 ctx (Sjumptable sv1 lpc1) (Sjumptable sv2 lpc2) - | Sreturn_simu_none: sfval_simu dm f opc1 opc2 ctx (Sreturn None) (Sreturn None) - | Sreturn_simu_some sv1 sv2: - (eval_sval (the_ge1 ctx) (the_sp ctx) sv1 (the_rs0 ctx) (the_m0 ctx)) - = (eval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx)) -> - sfval_simu dm f opc1 opc2 ctx (Sreturn (Some sv1)) (Sreturn (Some sv2)). - -Definition sstate_simu dm f outframe (s1 s2: sstate) (ctx: simu_proof_context f): Prop := - sistate_simu dm f outframe s1.(internal) s2.(internal) ctx - /\ forall is1, - ssem_internal (the_ge1 ctx) (the_sp ctx) s1 (the_rs0 ctx) (the_m0 ctx) is1 -> - is1.(icontinue) = true -> - sfval_simu dm f s1.(si_pc) s2.(si_pc) ctx s1.(final) s2.(final). - -Definition sexec_simu dm (f1 f2: RTLpath.function) pc1 pc2: Prop := - forall st1, sexec f1 pc1 = Some st1 -> - exists path st2, (fn_path f1)!pc1 = Some path /\ sexec f2 pc2 = Some st2 - /\ forall ctx, sstate_simu dm f1 path.(pre_output_regs) st1 st2 ctx. - -*) \ No newline at end of file -- cgit