From 5757c5a377b54464b37bdce6a6f9630caefef826 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 6 May 2021 17:28:07 +0200 Subject: init BTL_SEtheory (by copy/paste from RTLpathSE_theory) --- scheduling/BTL_SEtheory.v | 1831 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1831 insertions(+) create mode 100644 scheduling/BTL_SEtheory.v (limited to 'scheduling/BTL_SEtheory.v') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v new file mode 100644 index 00000000..53c00c8b --- /dev/null +++ b/scheduling/BTL_SEtheory.v @@ -0,0 +1,1831 @@ +(* A theory of symbolic execution on BTL + +NB: an efficient implementation with hash-consing will be defined in another file (some day) + +*) + +Require Import Coqlib Maps Floats. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import Op Registers. +Require Import RTL BTL OptionMonad. + +(* TODO remove this, when copy-paste of RTLpathSE_theory is clearly over... *) +Ltac inversion_SOME := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *) +Ltac inversion_ASSERT := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *) + +(** * Syntax and semantics of symbolic values *) + +(* symbolic value *) +Inductive sval := + | Sinput (r: reg) + | Sop (op:operation) (lsv: list_sval) (sm: smem) + | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) +with list_sval := + | Snil + | Scons (sv: sval) (lsv: list_sval) +(* symbolic memory *) +with smem := + | Sinit + | Sstore (sm: smem) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (srce: sval). + +Scheme sval_mut := Induction for sval Sort Prop +with list_sval_mut := Induction for list_sval Sort Prop +with smem_mut := Induction for smem Sort Prop. + +Fixpoint list_sval_inj (l: list sval): list_sval := + match l with + | nil => Snil + | v::l => Scons v (list_sval_inj l) + end. + +Local Open Scope option_monad_scope. + +Fixpoint eval_sval (ge: BTL.genv) (sp:val) (sv: sval) (rs0: regset) (m0: mem): option val := + match sv with + | Sinput r => Some (rs0#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 + | 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 + 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 + | None => Some (default_notrap_load_value chunk) + | Some a => + SOME m <- eval_smem ge sp sm rs0 m0 IN + match (Mem.loadv chunk m a) with + | None => Some (default_notrap_load_value chunk) + | Some val => Some val + end + end + end + end +with eval_list_sval (ge: BTL.genv) (sp:val) (lsv: list_sval) (rs0: regset) (m0: mem): 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::lv) + end +with eval_smem (ge: BTL.genv) (sp:val) (sm: smem) (rs0: regset) (m0: mem): option mem := + match sm with + | Sinit => Some m0 + | 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 + 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). +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 + eval_condition cond args m. + + +(** * Auxiliary definitions on Builtins *) +(* TODO: clean this. Some generic stuffs could be put in [AST.v] *) + +Section SEVAL_BUILTIN_ARG. (* adapted from Events.v *) + +Variable ge: BTL.genv. +Variable sp: val. +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 -> + seval_builtin_arg (BA x) v + | seval_BA_int: forall n, + seval_builtin_arg (BA_int n) (Vint n) + | seval_BA_long: forall n, + seval_builtin_arg (BA_long n) (Vlong n) + | seval_BA_float: forall n, + seval_builtin_arg (BA_float n) (Vfloat n) + | 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 -> + 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_BA_loadglobal: forall chunk id ofs v, + Mem.loadv chunk m (Senv.symbol_address ge 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_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). + +Definition seval_builtin_args (al: list (builtin_arg sval)) (vl: list val) : Prop := + list_forall2 seval_builtin_arg al vl. + +Lemma seval_builtin_arg_determ: + forall a v, seval_builtin_arg a v -> forall v', seval_builtin_arg a v' -> v' = v. +Proof. + induction 1; intros v' EV; inv EV; try congruence. + f_equal; eauto. + apply IHseval_builtin_arg1 in H3. apply IHseval_builtin_arg2 in H5. subst; auto. +Qed. + +Lemma eval_builtin_args_determ: + forall al vl, seval_builtin_args al vl -> forall vl', seval_builtin_args al vl' -> vl' = vl. +Proof. + induction 1; intros v' EV; inv EV; f_equal; eauto using seval_builtin_arg_determ. +Qed. + +End SEVAL_BUILTIN_ARG. + +(* NB: generic 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) + | BA_int n => BA_int n + | BA_long n => BA_long n + | BA_float f => BA_float f + | BA_single s => BA_single s + | BA_loadstack chunk ptr => BA_loadstack chunk ptr + | BA_addrstack ptr => BA_addrstack ptr + | BA_loadglobal chunk id ptr => BA_loadglobal chunk id ptr + | BA_addrglobal id ptr => BA_addrglobal id ptr + | BA_splitlong ba1 ba2 => BA_splitlong (builtin_arg_map f ba1) (builtin_arg_map f ba2) + | 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. +Proof. + induction arg. + all: try (intros varg SEVAL BARG; inv BARG; constructor; congruence). + - intros varg SEVAL BARG. inv BARG. simpl. constructor. + eapply IHarg1; eauto. eapply IHarg2; eauto. + - intros varg SEVAL BARG. inv BARG. simpl. constructor. + 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. +Proof. + induction 2. + - constructor. + - simpl. constructor; [| assumption]. + 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. +Proof. + induction arg. + all: intros varg SEVAL BARG; try (inv BARG; constructor; congruence). + - inv BARG. rewrite SEVAL in H0. inv H0. constructor. + - inv BARG. simpl. constructor. + eapply IHarg1; eauto. eapply IHarg2; eauto. + - inv BARG. simpl. constructor. + 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. +Proof. + induction args. + - simpl. intros. inv H0. constructor. + - intros vargs SEVAL BARG. simpl in BARG. inv BARG. + constructor; [| eapply IHargs; eauto]. + eapply seval_builtin_arg_complete; eauto. +Qed. + +Fixpoint seval_builtin_sval ge sp bsv rs0 m0 := + match bsv with + | BA sv => SOME v <- eval_sval ge sp sv rs0 m0 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 (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 (BA_addptr v1 v2) + | BA_int i => Some (BA_int i) + | BA_long l => Some (BA_long l) + | BA_float f => Some (BA_float f) + | BA_single s => Some (BA_single s) + | BA_loadstack chk ptr => Some (BA_loadstack chk ptr) + | BA_addrstack ptr => Some (BA_addrstack ptr) + | BA_loadglobal chk id ptr => Some (BA_loadglobal chk id ptr) + | BA_addrglobal id ptr => Some (BA_addrglobal id ptr) + end. + +Fixpoint eval_list_builtin_sval ge sp lbsv rs0 m0 := + 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 + 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 -> + lbs2 = nil. +Proof. + destruct lbs2; simpl; auto. + intros. destruct (seval_builtin_sval _ _ _ _ _); + try destruct (eval_list_builtin_sval _ _ _ _ _); discriminate. +Qed. + +Lemma seval_builtin_sval_arg ge sp rs0 m0 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. +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 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. + 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. + 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 -> + exists ba, + seval_builtin_sval ge sp bs rs0 m0 = Some ba + /\ eval_builtin_arg ge (fun id => id) sp m ba v. +Proof. + induction 1. + all: try (eexists; constructor; [simpl; reflexivity | constructor]). + 2-3: try assumption. + - eexists. constructor. + + simpl. rewrite H. reflexivity. + + constructor. + - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1). + destruct IHseval_builtin_arg2 as (ba2 & A2 & B2). + eexists. constructor. + + simpl. rewrite A1. rewrite A2. reflexivity. + + constructor; assumption. + - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1). + destruct IHseval_builtin_arg2 as (ba2 & A2 & B2). + eexists. constructor. + + simpl. rewrite A1. rewrite A2. reflexivity. + + constructor; assumption. +Qed. + +Lemma seval_builtin_sval_args ge sp rs0 m0 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. +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. + 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 -> + 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. +Proof. + induction 1. + - eexists. constructor. + + simpl. reflexivity. + + constructor. + - destruct IHlist_forall2 as (lba & A & B). + apply seval_builtin_arg_sval in H. destruct H as (ba & A' & B'). + eexists. constructor. + + simpl. rewrite A'. rewrite A. reflexivity. + + 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. +Proof. + intros. exploit seval_builtin_arg_sval; eauto. + intros (ba & X1 & X2). + eapply seval_builtin_sval_arg; eauto. + 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. +Proof. + intros. exploit seval_builtin_args_sval; eauto. + intros (ba & X1 & X2). + eapply seval_builtin_sval_args; eauto. + congruence. +Qed. + +(** * Symbolic (final) value of a block *) + +Inductive sfval := + | Sgoto (pc: exit) + | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:exit) + (* NB: [res] the return register is hard-wired ! Is it restrictive ? *) + | Stailcall: signature -> sval + ident -> list_sval -> sfval + | Sbuiltin (ef:external_function) (sargs: list (builtin_arg sval)) (res: builtin_res reg) (pc:exit) + | Sjumptable (sv: sval) (tbl: list exit) + | Sreturn: option sval -> sfval +. + +Definition sfind_function (ge: BTL.genv) (sp: val) (svos : sval + ident) (rs0: regset) (m0: mem): 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 + end +. + +Inductive sem_sfval (ge: BTL.genv) (sp:val) stack (f: function) (rs0: regset) (m0: mem): 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) + | 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') + | exec_Scall rs m sig svos lsv args res pc fd: + sfind_function ge sp svos rs0 m0 = 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) + | exec_Stailcall stk rs m sig svos args fd m' lsv: + sfind_function ge sp svos rs0 m0 = 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') + | 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') + | exec_Sjumptable sv tbl pc' n rs m: + eval_sval ge sp sv rs0 m0 = 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) +. + + +(** * 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 }. + +(* 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). + +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 + . + +(** * Symbolic execution of final step *) +Definition sexec_final_sfv (i: final) (sis: sistate): sfval := + match i with + | Bgoto pc => Sgoto pc + | Bcall sig ros args res pc => + let svos := sum_left_map sis.(si_sreg) ros in + let sargs := list_sval_inj (List.map sis.(si_sreg) args) in + Scall sig svos sargs res pc + | Btailcall sig ros args => + let svos := sum_left_map sis.(si_sreg) ros in + let sargs := list_sval_inj (List.map sis.(si_sreg) args) in + Stailcall sig svos sargs + | Bbuiltin ef args res pc => + let sargs := List.map (builtin_arg_map sis.(si_sreg)) args in + Sbuiltin ef sargs res pc + | Breturn or => + let sor := SOME r <- or IN Some (sis.(si_sreg) r) in + Sreturn sor + | Bjumptable reg tbl => + let sv := sis.(si_sreg) reg in + Sjumptable sv tbl + end. + +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. +Proof. + intros (PRE&MEM®). + destruct 1; subst; try_simplify_someHyps; simpl; intros; try autodestruct; eauto. + + (* Bcall *) intros; eapply exec_Scall; auto. + - 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. + - erewrite eval_list_sval_inj; simpl; auto. + + (* Bbuiltin *) intros. eapply exec_Sbuiltin; eauto. + eapply seval_builtin_args_correct; eauto. + + (* Bjumptable *) intros. eapply exec_Sjumptable; eauto. congruence. +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. +Proof. + intros (PRE&MEM®). + destruct i; simpl; intros LAST; inv LAST; eauto. + + (* Breturn *) + enough (v=regmap_optget res Vundef rs) as ->; eauto. + destruct res; simpl in *; congruence. + + (* Bcall *) + erewrite eval_list_sval_inj in *; try_simplify_someHyps. + intros; eapply exec_Bcall; eauto. + destruct fn; simpl in * |- *; auto. + rewrite REG in * |- ; auto. + + (* Btailcall *) + erewrite eval_list_sval_inj in *; try_simplify_someHyps. + intros; eapply exec_Btailcall; eauto. + destruct fn; simpl in * |- *; auto. + rewrite REG in * |- ; auto. + + (* Bjumptable *) + eapply exec_Bjumptable; eauto. + 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) + . + + +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