diff options
Diffstat (limited to 'scheduling/BTL_SEtheory.v')
| -rw-r--r-- | scheduling/BTL_SEtheory.v | 1336 |
1 files changed, 1336 insertions, 0 deletions
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v new file mode 100644 index 00000000..033ed843 --- /dev/null +++ b/scheduling/BTL_SEtheory.v @@ -0,0 +1,1336 @@ +(** A theory of symbolic simulation (i.e. simulation of symbolic executions) on BTL blocks. + +NB: an efficient implementation with hash-consing will be defined in another file (some day) + +The main theorem of this file is [symbolic_simu_correct] stating +that the abstract definition of symbolic simulation of two BTL blocks +implies the simulation for BTL.fsem block-steps. + + +*) + +Require Import Coqlib Maps Floats. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import Op Registers. +Require Import RTL BTL OptionMonad. +Require Export Impure.ImpHCons. +Import HConsing. + +(** * Syntax and semantics of symbolic values *) + +(** The semantics of symbolic execution is parametrized by the context of the execution of a block *) +Record iblock_exec_context := Bctx { + cge: BTL.genv; (** usual environment for identifiers *) + cf: function; (** ambient function of the block *) + csp: val; (** stack pointer *) + crs0: regset; (** initial state of registers (at the block entry) *) + cm0: mem (** initial memory state *) +}. + + +(** symbolic value *) +Inductive sval := + | Sundef (hid: hashcode) + | Sinput (r: reg) (hid: hashcode) + | Sop (op:operation) (lsv: list_sval) (hid: hashcode) + | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (hid: hashcode) +(** list of symbolic values *) +with list_sval := + | Snil (hid: hashcode) + | Scons (sv: sval) (lsv: list_sval) (hid: hashcode) +(** symbolic memory *) +with smem := + | Sinit (hid: hashcode) + | Sstore (sm: smem) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (srce: sval) (hid: hashcode) +. + +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. + +(** "fake" smart-constructors using an [unknown_hid] instead of the one provided by hash-consing. +These smart-constructors are those used in the abstract model of symbolic execution. +They will also appear in the implementation of rewriting rules (in order to avoid hash-consing handling +in proofs of rewriting rules). +*) + +Definition fSundef := Sundef unknown_hid. +Definition fSinput (r: reg) := Sinput r unknown_hid. +Definition fSop (op:operation) (lsv: list_sval) := Sop op lsv unknown_hid. +Definition fSload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) + := Sload sm trap chunk addr lsv unknown_hid. + +Definition fSnil := Snil unknown_hid. +Definition fScons (sv: sval) (lsv: list_sval) := Scons sv lsv unknown_hid. + +Definition fSinit := Sinit unknown_hid. +Definition fSstore (sm: smem) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (srce: sval) + := Sstore sm chunk addr lsv srce unknown_hid. + +Fixpoint list_sval_inj (l: list sval): list_sval := + match l with + | nil => fSnil + | v::l => fScons v (list_sval_inj l) + end. + +Local Open Scope option_monad_scope. + +(** Semantics *) +Fixpoint eval_sval ctx (sv: sval): option val := + match sv with + | Sundef _ => Some Vundef + | Sinput r _ => Some ((crs0 ctx)#r) + | Sop op l _ => + SOME args <- eval_list_sval ctx l IN + eval_operation (cge ctx) (csp ctx) op args (cm0 ctx) + | Sload sm trap chunk addr lsv _ => + match trap with + | TRAP => + 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 ctx lsv IN + match (eval_addressing (cge ctx) (csp ctx) addr args) with + | None => Some Vundef + | Some a => + SOME m <- eval_smem ctx sm IN + match (Mem.loadv chunk m a) with + | None => Some Vundef + | Some val => Some val + end + end + end + end +with eval_list_sval ctx (lsv: list_sval): option (list val) := + match lsv with + | Snil _ => Some nil + | Scons sv lsv' _ => + SOME v <- eval_sval ctx sv IN + SOME lv <- eval_list_sval ctx lsv' IN + Some (v::lv) + end +with eval_smem ctx (sm: smem): option mem := + match sm with + | Sinit _ => Some (cm0 ctx) + | Sstore sm chunk addr lsv srce _ => + 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. + +(** The symbolic memory preserves predicate Mem.valid_pointer with respect to initial memory. + Hence, arithmetic operations and Boolean conditions do not depend on the current memory of the block + (their semantics only depends on the initial memory of the block). + + The correctness of this idea is proved on lemmas [sexec_op_correct] and [eval_scondition_eq]. +*) +Lemma valid_pointer_preserv ctx sm: + forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer (cm0 ctx) b ofs = Mem.valid_pointer m b ofs. +Proof. + induction sm; simpl; intros; try_simplify_someHyps; auto. + repeat autodestruct; intros; erewrite IHsm by reflexivity. + eapply Mem.storev_preserv_valid; eauto. +Qed. +Local Hint Resolve valid_pointer_preserv: core. + +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 eval_scondition ctx (cond: condition) (lsv: list_sval): option bool := + SOME args <- eval_list_sval ctx lsv IN + eval_condition cond args (cm0 ctx). + + +(** * Auxiliary definitions on Builtins *) +(* TODO: clean this. Some generic stuffs could be put in [AST.v] *) + +Section EVAL_BUILTIN_SARG. (* adapted from Events.v *) + +Variable ctx: iblock_exec_context. +Variable m: mem. + +Inductive eval_builtin_sarg: builtin_arg sval -> val -> Prop := + | seval_BA: forall x v, + eval_sval ctx x = Some v -> + eval_builtin_sarg (BA x) v + | seval_BA_int: forall n, + eval_builtin_sarg (BA_int n) (Vint n) + | seval_BA_long: forall n, + eval_builtin_sarg (BA_long n) (Vlong n) + | seval_BA_float: forall n, + eval_builtin_sarg (BA_float n) (Vfloat n) + | seval_BA_single: forall n, + eval_builtin_sarg (BA_single n) (Vsingle n) + | seval_BA_loadstack: forall chunk ofs v, + Mem.loadv chunk m (Val.offset_ptr (csp ctx) ofs) = Some v -> + eval_builtin_sarg (BA_loadstack chunk ofs) v + | seval_BA_addrstack: forall ofs, + eval_builtin_sarg (BA_addrstack ofs) (Val.offset_ptr (csp ctx) ofs) + | seval_BA_loadglobal: forall chunk id ofs v, + Mem.loadv chunk m (Senv.symbol_address (cge ctx) id ofs) = Some v -> + eval_builtin_sarg (BA_loadglobal chunk id ofs) v + | seval_BA_addrglobal: forall id ofs, + eval_builtin_sarg (BA_addrglobal id ofs) (Senv.symbol_address (cge ctx) id ofs) + | seval_BA_splitlong: forall hi lo vhi vlo, + eval_builtin_sarg hi vhi -> eval_builtin_sarg lo vlo -> + eval_builtin_sarg (BA_splitlong hi lo) (Val.longofwords vhi vlo) + | seval_BA_addptr: forall a1 a2 v1 v2, + eval_builtin_sarg a1 v1 -> eval_builtin_sarg a2 v2 -> + eval_builtin_sarg (BA_addptr a1 a2) + (if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2) +. + +Definition eval_builtin_sargs (al: list (builtin_arg sval)) (vl: list val) : Prop := + list_forall2 eval_builtin_sarg al vl. + +Lemma eval_builtin_sarg_determ: + forall a v, eval_builtin_sarg a v -> forall v', eval_builtin_sarg a v' -> v' = v. +Proof. + induction 1; intros v' EV; inv EV; try congruence. + f_equal; eauto. + apply IHeval_builtin_sarg1 in H3. apply IHeval_builtin_sarg2 in H5. subst; auto. +Qed. + +Lemma eval_builtin_sargs_determ: + forall al vl, eval_builtin_sargs al vl -> forall vl', eval_builtin_sargs al vl' -> vl' = vl. +Proof. + induction 1; intros v' EV; inv EV; f_equal; eauto using eval_builtin_sarg_determ. +Qed. + +End EVAL_BUILTIN_SARG. + +(* 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 eval_builtin_sarg_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 -> + eval_builtin_sarg ctx m (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 eval_builtin_sargs_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 -> + eval_builtin_sargs ctx m (map (builtin_arg_map sreg) args) vargs. +Proof. + induction 2. + - constructor. + - simpl. constructor; [| assumption]. + eapply eval_builtin_sarg_correct; eauto. +Qed. + +Lemma eval_builtin_sarg_exact ctx rs m sreg: forall arg varg, + (forall r, eval_sval ctx (sreg r) = Some rs # r) -> + eval_builtin_sarg 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). + - 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 eval_builtin_sargs_exact ctx rs m sreg: forall args vargs, + (forall r, eval_sval ctx (sreg r) = Some rs # r) -> + eval_builtin_sargs 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. + - intros vargs SEVAL BARG. simpl in BARG. inv BARG. + constructor; [| eapply IHargs; eauto]. + eapply eval_builtin_sarg_exact; eauto. +Qed. + +Fixpoint eval_builtin_sval ctx bsv := + match bsv with + | BA sv => SOME v <- eval_sval ctx sv IN Some (BA v) + | BA_splitlong sv1 sv2 => + SOME v1 <- eval_builtin_sval ctx sv1 IN + SOME v2 <- eval_builtin_sval ctx sv2 IN + Some (BA_splitlong v1 v2) + | BA_addptr sv1 sv2 => + SOME v1 <- eval_builtin_sval ctx sv1 IN + SOME v2 <- eval_builtin_sval ctx sv2 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 ctx lbsv := + match lbsv with + | nil => Some nil + | bsv::lbsv => SOME v <- eval_builtin_sval ctx bsv IN + SOME lv <- eval_list_builtin_sval ctx lbsv IN + Some (v::lv) + end. + +Lemma eval_list_builtin_sval_nil ctx lbs2: + eval_list_builtin_sval ctx lbs2 = Some nil -> + lbs2 = nil. +Proof. + destruct lbs2; simpl; repeat autodestruct; congruence. +Qed. + +Lemma eval_builtin_sval_arg ctx bs: + forall ba m v, + eval_builtin_sval ctx bs = Some ba -> + eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v -> + eval_builtin_sarg 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 H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; auto. + - intros ba m v. + destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (eval_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 (eval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence. + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; eauto. +Qed. + +Lemma eval_builtin_sarg_sval ctx m v: forall bs, + eval_builtin_sarg ctx m bs v -> + exists ba, + eval_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]). + 2-3: try assumption. + - eexists. constructor. + + simpl. rewrite H. reflexivity. + + constructor. + - destruct IHeval_builtin_sarg1 as (ba1 & A1 & B1). + destruct IHeval_builtin_sarg2 as (ba2 & A2 & B2). + eexists. constructor. + + simpl. rewrite A1. rewrite A2. reflexivity. + + constructor; assumption. + - destruct IHeval_builtin_sarg1 as (ba1 & A1 & B1). + destruct IHeval_builtin_sarg2 as (ba2 & A2 & B2). + eexists. constructor. + + simpl. rewrite A1. rewrite A2. reflexivity. + + constructor; assumption. +Qed. + +Lemma eval_builtin_sval_args ctx lbs: + forall lba m v, + eval_list_builtin_sval ctx lbs = Some lba -> + list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba v -> + eval_builtin_sargs ctx m lbs v. +Proof. + unfold eval_builtin_sargs; induction lbs; simpl; intros lba m v. + - intros H; inversion H; subst; clear H. + intros H; inversion H. econstructor. + - destruct (eval_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 eval_builtin_sval_arg; eauto. +Qed. + +Lemma eval_builtin_sargs_sval ctx m lv: forall lbs, + eval_builtin_sargs ctx m lbs lv -> + exists lba, + 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. + + simpl. reflexivity. + + constructor. + - destruct IHlist_forall2 as (lba & A & B). + apply eval_builtin_sarg_sval in H. destruct H as (ba & A' & B'). + eexists. constructor. + + simpl. rewrite A'. rewrite A. reflexivity. + + constructor; assumption. +Qed. + +Lemma eval_builtin_sval_correct ctx m: forall bs1 v bs2, + eval_builtin_sarg ctx m bs1 v -> + (eval_builtin_sval ctx bs1) = (eval_builtin_sval ctx bs2) -> + eval_builtin_sarg ctx m bs2 v. +Proof. + intros. exploit eval_builtin_sarg_sval; eauto. + intros (ba & X1 & X2). + eapply eval_builtin_sval_arg; eauto. + congruence. +Qed. + +Lemma eval_list_builtin_sval_correct ctx m vargs: forall lbs1, + eval_builtin_sargs ctx m lbs1 vargs -> + forall lbs2, (eval_list_builtin_sval ctx lbs1) = (eval_list_builtin_sval ctx lbs2) -> + eval_builtin_sargs ctx m lbs2 vargs. +Proof. + intros. exploit eval_builtin_sargs_sval; eauto. + intros (ba & X1 & X2). + eapply eval_builtin_sval_args; eauto. + congruence. +Qed. + +(** * Symbolic (final) value of a block *) + +(** TODO: faut-il hash-conser les valeurs symboliques finales. Pas très utile si pas de join interne. +Mais peut être utile dans le cas contraire. *) + +Inductive sfval := + | Sgoto (pc: exit) + | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:exit) + | 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 ctx (svos : sval + ident): option fundef := + match svos with + | 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 +. + +Import ListNotations. +Local Open Scope list_scope. + +Inductive sem_sfval ctx stk: sfval -> regset -> mem -> trace -> state -> Prop := + | exec_Sgoto pc rs m: + sem_sfval ctx stk (Sgoto pc) rs m E0 (State stk (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] None rs) m) + | exec_Sreturn pstk osv rs m m' v: + (csp ctx) = (Vptr pstk Ptrofs.zero) -> + Mem.free m pstk 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 stk (Sreturn osv) rs m + E0 (Returnstate stk v m') + | exec_Scall rs m sig svos lsv args res pc fd: + sfind_function ctx svos = Some fd -> + funsig fd = sig -> + eval_list_sval ctx lsv = Some args -> + sem_sfval ctx stk (Scall sig svos lsv res pc) rs m + E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] (Some res) rs)::stk) fd args m) + | exec_Stailcall pstk rs m sig svos args fd m' lsv: + sfind_function ctx svos = Some fd -> + funsig fd = sig -> + (csp ctx) = Vptr pstk Ptrofs.zero -> + Mem.free m pstk 0 (cf ctx).(fn_stacksize) = Some m' -> + eval_list_sval ctx lsv = Some args -> + sem_sfval ctx stk (Stailcall sig svos lsv) rs m + E0 (Callstate stk fd args m') + | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs: + eval_builtin_sargs ctx m sargs vargs -> + external_call ef (cge ctx) vargs m t vres m' -> + sem_sfval ctx stk (Sbuiltin ef sargs res pc) rs m + t (State stk (cf ctx) (csp ctx) pc (regmap_setres res vres (tr_inputs (cf ctx) [pc] (reg_builtin_res res) rs)) m') + | exec_Sjumptable sv tbl pc' n rs m: + eval_sval ctx sv = Some (Vint n) -> + list_nth_z tbl (Int.unsigned n) = Some pc' -> + sem_sfval ctx stk (Sjumptable sv tbl) rs m + E0 (State stk (cf ctx) (csp ctx) pc' (tr_inputs ctx.(cf) tbl None rs) m) +. + +(* Syntax and Semantics of symbolic internal states *) +(* [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 ((crs0 ctx), (cm0 ctx)) *) +Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop := + sis.(si_pre) ctx + /\ eval_smem ctx sis.(si_smem) = Some m + /\ forall (r:reg), eval_sval ctx (sis.(si_sreg) r) = Some (rs#r). + +(** * Symbolic execution of final step *) +Definition sexec_final_sfv (i: final) (sreg: reg -> sval): sfval := + match i with + | Bgoto pc => Sgoto pc + | Bcall sig ros args res pc => + let svos := sum_left_map sreg ros in + let sargs := list_sval_inj (List.map sreg args) in + Scall sig svos sargs res pc + | Btailcall sig ros args => + let svos := sum_left_map sreg ros in + let sargs := list_sval_inj (List.map sreg args) in + Stailcall sig svos sargs + | Bbuiltin ef args res pc => + let sargs := List.map (builtin_arg_map sreg) args in + Sbuiltin ef sargs res pc + | Breturn or => + let sor := SOME r <- or IN Some (sreg r) in + Sreturn sor + | Bjumptable reg tbl => + let sv := sreg reg in + Sjumptable sv tbl + end. + +Local Hint Constructors sem_sfval: core. + +Lemma sexec_final_sfv_correct ctx stk i sis t rs m s: + sem_sistate ctx sis rs m -> + final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs m i t s -> + sem_sfval ctx stk (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; eauto. + - destruct ros; simpl in * |- *; eauto. + rewrite REG; eauto. + - erewrite eval_list_sval_inj; simpl; auto. + + (* Bbuiltin *) intros. eapply exec_Sbuiltin; eauto. + eapply eval_builtin_sargs_correct; eauto. + + (* Bjumptable *) intros. eapply exec_Sjumptable; eauto. congruence. +Qed. + +Local Hint Constructors final_step: core. +Local Hint Resolve eval_builtin_sargs_exact: core. + +Lemma sexec_final_sfv_exact ctx stk i sis t rs m s: + sem_sistate ctx sis rs m -> + sem_sfval ctx stk (sexec_final_sfv i sis) rs m t s + -> final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) 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. + +(** * symbolic execution of basic instructions *) + +Definition sis_init : sistate := {| si_pre:= fun _ => True; si_sreg:= fun r => fSinput r; si_smem:= fSinit |}. + +Lemma sis_init_correct ctx: + sem_sistate ctx sis_init (crs0 ctx) (cm0 ctx). +Proof. + unfold sis_init, sem_sistate; simpl; intuition eauto. +Qed. + +Definition set_sreg (r:reg) (sv:sval) (sis:sistate): sistate := + {| si_pre:=(fun ctx => eval_sval ctx (sis.(si_sreg) r) <> None /\ (sis.(si_pre) ctx)); + si_sreg:=fun y => if Pos.eq_dec r y then sv else sis.(si_sreg) y; + si_smem:= sis.(si_smem)|}. + +Lemma set_sreg_correct ctx dst sv sis (rs rs': regset) m: + sem_sistate ctx sis rs m -> + (eval_sval ctx sv = Some rs' # dst) -> + (forall r, r <> dst -> rs'#r = rs#r) -> + sem_sistate ctx (set_sreg dst sv sis) rs' m. +Proof. + intros (PRE&MEM®) NEW OLD. + unfold sem_sistate; simpl. + intuition. + - rewrite REG in *; congruence. + - destruct (Pos.eq_dec dst r); simpl; subst; eauto. + rewrite REG in *. rewrite OLD; eauto. +Qed. + +Definition set_smem (sm:smem) (sis:sistate): sistate := + {| si_pre:=(fun ctx => eval_smem ctx sis.(si_smem) <> None /\ (sis.(si_pre) ctx)); + si_sreg:= sis.(si_sreg); + si_smem:= sm |}. + +Lemma set_smem_correct ctx sm sis rs m m': + sem_sistate ctx sis rs m -> + eval_smem ctx sm = Some m' -> + sem_sistate ctx (set_smem sm sis) rs m'. +Proof. + intros (PRE&MEM®) NEW. + unfold sem_sistate; simpl. + intuition. + rewrite MEM in *; congruence. +Qed. + +Definition sexec_op op args dst sis: sistate := + let args := list_sval_inj (List.map sis.(si_sreg) args) in + set_sreg dst (fSop op args) sis. + +Lemma sexec_op_correct ctx op args dst sis rs m v + (EVAL: eval_operation (cge ctx) (csp ctx) op rs ## args m = Some v) + (SIS: sem_sistate ctx sis rs m) + :(sem_sistate ctx (sexec_op op args dst sis) (rs#dst <- v) m). +Proof. + eapply set_sreg_correct; eauto. + - simpl. destruct SIS as (PRE&MEM®). + rewrite Regmap.gss; simpl; auto. + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + intros; erewrite op_valid_pointer_eq; eauto. + - intros; rewrite Regmap.gso; auto. +Qed. + +Definition sexec_load trap chunk addr args dst sis: sistate := + let args := list_sval_inj (List.map sis.(si_sreg) args) in + set_sreg dst (fSload sis.(si_smem) trap chunk addr args) sis. + +Lemma sexec_load_correct ctx chunk addr args dst sis rs m v trap + (HLOAD: has_loaded (cge ctx) (csp ctx) rs m chunk addr args v trap) + (SIS: sem_sistate ctx sis rs m) + :(sem_sistate ctx (sexec_load trap chunk addr args dst sis) (rs#dst <- v) m). +Proof. + inv HLOAD; eapply set_sreg_correct; eauto. + 2,4: intros; rewrite Regmap.gso; auto. + - simpl. destruct SIS as (PRE&MEM®). + destruct trap; rewrite Regmap.gss; simpl; auto; + erewrite eval_list_sval_inj; simpl; auto; + try_simplify_someHyps. + intros. rewrite LOAD; auto. + - simpl. destruct SIS as (PRE&MEM®). + rewrite Regmap.gss; simpl; auto. + erewrite eval_list_sval_inj; simpl; auto. + autodestruct; rewrite MEM, LOAD; auto. +Qed. + +Definition sexec_store chunk addr args src sis: sistate := + let args := list_sval_inj (List.map sis.(si_sreg) args) in + let src := sis.(si_sreg) src in + let sm := fSstore sis.(si_smem) chunk addr args src in + set_smem sm sis. + +Lemma sexec_store_correct ctx chunk addr args src sis rs m m' a + (EVAL: eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a) + (STORE: Mem.storev chunk m a (rs # src) = Some m') + (SIS: sem_sistate ctx sis rs m) + :(sem_sistate ctx (sexec_store chunk addr args src sis) rs m'). +Proof. + eapply set_smem_correct; eauto. + simpl. destruct SIS as (PRE&MEM®). + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + rewrite REG; auto. +Qed. + +Lemma eval_scondition_eq ctx cond args sis rs m + (SIS : sem_sistate ctx sis rs m) + :eval_scondition ctx cond (list_sval_inj (map (si_sreg sis) args)) = eval_condition cond rs ## args m. +Proof. + destruct SIS as (PRE&MEM®); unfold eval_scondition; simpl. + erewrite eval_list_sval_inj; simpl; auto. + eapply cond_valid_pointer_eq; eauto. +Qed. + +(** * Compute sistate associated to final values *) +Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval := + match inputs with + | nil => fun r => fSundef + | r1::l => fun r => if Pos.eq_dec r1 r then sreg r1 else transfer_sreg l sreg r + end. + +Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (pre_inputs f tbl or)). + +Lemma str_inputs_correct ctx sis rs tbl or r: + (forall r : reg, eval_sval ctx (si_sreg sis r) = Some rs # r) -> + eval_sval ctx (str_inputs (cf ctx) tbl or (si_sreg sis) r) = Some (tr_inputs (cf ctx) tbl or rs) # r. +Proof. + intros H. + unfold str_inputs, tr_inputs, transfer_regs. + induction (Regset.elements _) as [|x l]; simpl. + + rewrite Regmap.gi; auto. + + autodestruct; intros; subst. + * rewrite Regmap.gss; auto. + * rewrite Regmap.gso; eauto. +Qed. + +Local Hint Resolve str_inputs_correct: core. + +Definition tr_sis f (fi: final) (sis: sistate) := + {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None); + si_sreg := poly_tr str_inputs f fi sis.(si_sreg); + si_smem := sis.(si_smem) |}. + +Lemma tr_sis_regs_correct_aux ctx fin sis rs m: + sem_sistate ctx sis rs m -> + (forall r, eval_sval ctx (tr_sis (cf ctx) fin sis r) = Some (tr_regs (cf ctx) fin rs) # r). +Proof. + Local Opaque str_inputs. + simpl. destruct 1 as (_ & _ & REG). + destruct fin; simpl; eauto. +Qed. + +Lemma tr_sis_regs_correct ctx fin sis rs m: + sem_sistate ctx sis rs m -> + sem_sistate ctx (tr_sis (cf ctx) fin sis) (tr_regs (cf ctx) fin rs) m. +Proof. + intros H. + generalize (tr_sis_regs_correct_aux _ fin _ _ _ H). + destruct H as (PRE & MEM & REG). + econstructor; simpl; intuition eauto || congruence. +Qed. + +Definition poly_str {A} (tr: function -> list exit -> option reg -> A) f (sfv: sfval): A := + match sfv with + | Sgoto pc => tr f [pc] None + | Scall _ _ _ res pc => tr f [pc] (Some res) + | Stailcall _ _ args => tr f [] None + | Sbuiltin _ _ res pc => tr f [pc] (reg_builtin_res res) + | Sreturn _ => tr f [] None + | Sjumptable _ tbl => tr f tbl None + end. + +Definition str_regs: function -> sfval -> regset -> regset := + poly_str tr_inputs. + +Lemma str_tr_regs_equiv f fin sis: + str_regs f (sexec_final_sfv fin sis) = tr_regs f fin. +Proof. + destruct fin; simpl; auto. +Qed. + +(** * symbolic execution of blocks *) + +(* symbolic state *) +Inductive sstate := + | Sfinal (sis: sistate) (sfv: sfval) + | Scond (cond: condition) (args: list_sval) (ifso ifnot: sstate) + | Sabort + . + +(* outcome of a symbolic execution path *) +Record soutcome := sout { + _sis: sistate; + _sfv: sfval; +}. + +Fixpoint get_soutcome ctx (st:sstate): option soutcome := + match st with + | Sfinal sis sfv => Some (sout sis sfv) + | Scond cond args ifso ifnot => + SOME b <- eval_scondition ctx cond args IN + get_soutcome ctx (if b then ifso else ifnot) + | Sabort => None + end. + +(* transition (t,s) produced by a sstate in initial context ctx *) +Inductive sem_sstate ctx stk t s: sstate -> Prop := + | sem_Sfinal sis sfv rs m + (SIS: sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m) + (SFV: sem_sfval ctx stk sfv rs m t s) + : sem_sstate ctx stk t s (Sfinal sis sfv) + | sem_Scond b cond args ifso ifnot + (SEVAL: eval_scondition ctx cond args = Some b) + (SELECT: sem_sstate ctx stk t s (if b then ifso else ifnot)) + : sem_sstate ctx stk t s (Scond cond args ifso ifnot) + (* NB: Sabort: fails to produce a transition *) + . + +Lemma sem_sstate_run ctx stk st t s: + sem_sstate ctx stk t s st -> + exists sis sfv rs m, + get_soutcome ctx st = Some (sout sis sfv) + /\ sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m + /\ sem_sfval ctx stk sfv rs m t s + . +Proof. + induction 1; simpl; try_simplify_someHyps; do 4 eexists; intuition eauto. +Qed. + +Local Hint Resolve sem_Sfinal: core. + +Lemma run_sem_sstate ctx st sis sfv: + get_soutcome ctx st = Some (sout sis sfv) -> + forall rs m stk s t, + sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m -> + sem_sfval ctx stk sfv rs m t s -> + sem_sstate ctx stk t s st + . +Proof. + induction st; simpl; try_simplify_someHyps. + autodestruct; intros; econstructor; eauto. + autodestruct; eauto. +Qed. + + +(** * Model of Symbolic Execution with Continuation Passing Style + +Parameter [k] is the continuation, i.e. the [sstate] construction that will be applied in each execution branch. +Its input parameter is the symbolic internal state of the branch. + +*) + +Fixpoint sexec_rec f ib sis (k: sistate -> sstate): sstate := + match ib with + | BF fin _ => Sfinal (tr_sis f fin sis) (sexec_final_sfv fin sis) + (* basic instructions *) + | Bnop _ => k sis + | Bop op args res _ => k (sexec_op op args res sis) + | Bload trap chunk addr args dst _ => k (sexec_load trap chunk addr args dst sis) + | Bstore chunk addr args src _ => k (sexec_store chunk addr args src sis) + (* composed instructions *) + | Bseq ib1 ib2 => + sexec_rec f ib1 sis (fun sis2 => sexec_rec f ib2 sis2 k) + | Bcond cond args ifso ifnot _ => + let args := list_sval_inj (List.map sis.(si_sreg) args) in + let ifso := sexec_rec f ifso sis k in + let ifnot := sexec_rec f ifnot sis k in + Scond cond args ifso ifnot + end + . + +Definition sexec f ib := sexec_rec f ib sis_init (fun _ => Sabort). + +Local Hint Constructors sem_sstate: core. +Local Hint Resolve sexec_op_correct sexec_final_sfv_correct tr_sis_regs_correct_aux tr_sis_regs_correct + sexec_load_correct sexec_store_correct sis_init_correct: core. + +Lemma sexec_rec_correct ctx stk t s ib rs m rs1 m1 ofin + (ISTEP: iblock_istep (cge ctx) (csp ctx) rs m ib rs1 m1 ofin): forall sis k + (SIS: sem_sistate ctx sis rs m) + (CONT: match ofin with + | None => forall sis', sem_sistate ctx sis' rs1 m1 -> sem_sstate ctx stk t s (k sis') + | Some fin => final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs1 m1 fin t s + end), + sem_sstate ctx stk t s (sexec_rec (cf ctx) ib sis k). +Proof. + induction ISTEP; simpl; try autodestruct; eauto. + (* final value *) + intros; econstructor; eauto. + rewrite str_tr_regs_equiv; eauto. + (* condition *) + all: intros; + eapply sem_Scond; eauto; [ + erewrite eval_scondition_eq; eauto | + replace (if b then sexec_rec (cf ctx) ifso sis k else sexec_rec (cf ctx) ifnot sis k) with (sexec_rec (cf ctx) (if b then ifso else ifnot) sis k); + try autodestruct; eauto ]. +Qed. + + +(* NB: each concrete execution can be executed on the symbolic state (produced from [sexec]) + (sexec is a correct over-approximation) +*) +Theorem sexec_correct ctx stk ib t s: + iblock_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s -> + sem_sstate ctx stk t s (sexec (cf ctx) ib). +Proof. + destruct 1 as (rs' & m' & fin & ISTEP & FSTEP). + eapply sexec_rec_correct; simpl; eauto. +Qed. + +(* Remark that we want to reason modulo "extensionality" wrt Regmap.get about regsets. + And, nothing in their representation as (val * PTree.t val) enforces that + (forall r, rs1#r = rs2#r) -> rs1 = rs2 +*) +Lemma sem_sistate_tr_sis_determ ctx sis rs1 m1 fi rs2 m2: + sem_sistate ctx sis rs1 m1 -> + sem_sistate ctx (tr_sis (cf ctx) fi sis) rs2 m2 -> + (forall r, rs2#r = (tr_regs (cf ctx) fi rs1)#r) + /\ m1 = m2. +Proof. + intros H1 H2. + lapply (tr_sis_regs_correct_aux ctx fi sis rs1 m1); eauto. + intros X. + destruct H1 as (_&MEM1®1). + destruct H2 as (_&MEM2®2); simpl in *. + intuition try congruence. + cut (Some rs2 # r = Some (tr_regs (cf ctx) fi rs1)#r). + { congruence. } + rewrite <- REG2, X. auto. +Qed. + +Local Hint Constructors equiv_stackframe list_forall2: core. +Local Hint Resolve regmap_setres_eq equiv_stack_refl equiv_stack_refl: core. + +Lemma sem_sfval_equiv rs1 rs2 ctx stk sfv m t s: + sem_sfval ctx stk sfv rs1 m t s -> + (forall r, (str_regs (cf ctx) sfv rs1)#r = (str_regs (cf ctx) sfv rs2)#r) -> + exists s', sem_sfval ctx stk sfv rs2 m t s' /\ equiv_state s s'. +Proof. + unfold str_regs. + destruct 1; simpl in *; intros; subst; eexists; split; econstructor; eauto; try congruence. +Qed. + +Definition abort_sistate ctx (sis: sistate): Prop := + ~(sis.(si_pre) ctx) + \/ eval_smem ctx sis.(si_smem) = None + \/ exists (r: reg), eval_sval ctx (sis.(si_sreg) r) = None. + +Lemma set_sreg_preserves_abort ctx sv dst sis: + abort_sistate ctx sis -> + abort_sistate ctx (set_sreg dst sv sis). +Proof. + unfold abort_sistate; simpl; intros [PRE|[MEM|REG]]; try tauto. + destruct REG as [r REG]. + destruct (Pos.eq_dec dst r) as [TEST|TEST] eqn: HTEST. + - subst; rewrite REG; tauto. + - right. right. eexists; rewrite HTEST. auto. +Qed. + +Lemma sexec_op_preserves_abort ctx op args dest sis: + abort_sistate ctx sis + -> abort_sistate ctx (sexec_op op args dest sis). +Proof. + intros; eapply set_sreg_preserves_abort; eauto. +Qed. + +Lemma sexec_load_preserves_abort ctx chunk addr args dest sis trap: + abort_sistate ctx sis + -> abort_sistate ctx (sexec_load trap chunk addr args dest sis). +Proof. + intros; eapply set_sreg_preserves_abort; eauto. +Qed. + +Lemma set_smem_preserves_abort ctx sm sis: + abort_sistate ctx sis -> + abort_sistate ctx (set_smem sm sis). +Proof. + unfold abort_sistate; simpl; try tauto. +Qed. + +Lemma sexec_store_preserves_abort ctx chunk addr args src sis: + abort_sistate ctx sis + -> abort_sistate ctx (sexec_store chunk addr args src sis). +Proof. + intros; eapply set_smem_preserves_abort; eauto. +Qed. + +Lemma sem_sistate_tr_sis_exclude_abort ctx sis fi rs m: + sem_sistate ctx (tr_sis (cf ctx) fi sis) rs m -> + abort_sistate ctx sis -> + False. +Proof. + intros ((PRE1 & PRE2) & MEM & REG); simpl in *. + intros [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; try congruence. +Qed. + +Local Hint Resolve sexec_op_preserves_abort sexec_load_preserves_abort + sexec_store_preserves_abort sem_sistate_tr_sis_exclude_abort: core. + +Lemma sexec_exclude_abort ctx stk ib t s1: forall sis k + (SEXEC: sem_sstate ctx stk t s1 (sexec_rec (cf ctx) ib sis k)) + (CONT: forall sis', sem_sstate ctx stk t s1 (k sis') -> (abort_sistate ctx sis') -> False) + (ABORT: abort_sistate ctx sis), + False. +Proof. + induction ib; simpl; intros; eauto. + - (* final *) inversion SEXEC; subst; eauto. + - (* seq *) + eapply IHib1; eauto. + simpl. eauto. + - (* cond *) + inversion SEXEC; subst; eauto. clear SEXEC. + destruct b; eauto. +Qed. + +Lemma set_sreg_abort ctx dst sv sis rs m: + sem_sistate ctx sis rs m -> + (eval_sval ctx sv = None) -> + abort_sistate ctx (set_sreg dst sv sis). +Proof. + intros (PRE&MEM®) NEW. + unfold sem_sistate, abort_sistate; simpl. + right; right. + exists dst; destruct (Pos.eq_dec dst dst); simpl; try congruence. +Qed. + +Lemma sexec_op_abort ctx sis op args dest rs m + (EVAL: eval_operation (cge ctx) (csp ctx) op rs ## args m = None) + (SIS: sem_sistate ctx sis rs m) + : abort_sistate ctx (sexec_op op args dest sis). +Proof. + eapply set_sreg_abort; eauto. + simpl. destruct SIS as (PRE&MEM®). + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + intros; erewrite op_valid_pointer_eq; eauto. +Qed. + +Lemma sexec_load_TRAP_abort ctx chunk addr args dst sis rs m + (EVAL: forall a, eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a -> Mem.loadv chunk m a = None) + (SIS: sem_sistate ctx sis rs m) + : abort_sistate ctx (sexec_load TRAP chunk addr args dst sis). +Proof. + eapply set_sreg_abort; eauto. + simpl. destruct SIS as (PRE&MEM®). + erewrite eval_list_sval_inj; simpl; auto. + intros; autodestruct; try_simplify_someHyps. +Qed. + +Lemma set_smem_abort ctx sm sis rs m: + sem_sistate ctx sis rs m -> + eval_smem ctx sm = None -> + abort_sistate ctx (set_smem sm sis). +Proof. + intros (PRE&MEM®) NEW. + unfold abort_sistate; simpl. + tauto. +Qed. + +Lemma sexec_store_abort ctx chunk addr args src sis rs m + (EVAL: forall a, eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a -> Mem.storev chunk m a (rs # src) = None) + (SIS: sem_sistate ctx sis rs m) + :abort_sistate ctx (sexec_store chunk addr args src sis). +Proof. + eapply set_smem_abort; eauto. + simpl. destruct SIS as (PRE&MEM®). + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + intros; rewrite REG; autodestruct; try_simplify_someHyps. +Qed. + +Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort sexec_final_sfv_exact: core. + +Lemma sexec_rec_exact ctx stk ib t s1: forall sis k + (SEXEC: sem_sstate ctx stk t s1 (sexec_rec (cf ctx) ib sis k)) + rs m + (SIS: sem_sistate ctx sis rs m) + (CONT: forall sis', sem_sstate ctx stk t s1 (k sis') -> (abort_sistate ctx sis') -> False) + , + match iblock_istep_run (cge ctx) (csp ctx) ib rs m with + | Some (out rs' m' (Some fin)) => + exists s2, final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2 + | Some (out rs' m' None) => exists sis', (sem_sstate ctx stk t s1 (k sis')) /\ (sem_sistate ctx sis' rs' m') + | None => False + end. +Proof. + induction ib; simpl; intros; eauto. + - (* final *) + inv SEXEC. + exploit (sem_sistate_tr_sis_determ ctx sis rs m fi); eauto. + intros (REG&MEM); subst. + exploit (sem_sfval_equiv rs0 rs); eauto. + * intros; rewrite REG, str_tr_regs_equiv; auto. + * intros (s2 & EQUIV & SFV'); eauto. + - (* Bop *) autodestruct; eauto. + - destruct trap. + + repeat autodestruct. + { eexists; split; eauto. + eapply sexec_load_correct; eauto. + econstructor; eauto. } + all: + intros; eapply CONT; eauto; + eapply sexec_load_TRAP_abort; eauto; + intros; try_simplify_someHyps. + + repeat autodestruct; + eexists; split; eauto; + eapply sexec_load_correct; eauto; + try (econstructor; eauto; fail). + all: eapply has_loaded_default; auto; try_simplify_someHyps. + - repeat autodestruct; eauto. + all: intros; eapply CONT; eauto; + eapply sexec_store_abort; eauto; + intros; try_simplify_someHyps. + - (* Bseq *) + exploit IHib1; eauto. clear sis SEXEC SIS. + { simpl; intros; eapply sexec_exclude_abort; eauto. } + destruct (iblock_istep_run _ _ _ _ _) eqn: ISTEP; auto. + destruct o. + destruct _fin eqn: OFIN; simpl; eauto. + intros (sis1 & SEXEC1 & SIS1). + exploit IHib2; eauto. + - (* Bcond *) + inv SEXEC. + erewrite eval_scondition_eq in SEVAL; eauto. + rewrite SEVAL. + destruct b. + + exploit IHib1; eauto. + + exploit IHib2; eauto. +Qed. + + +(* NB: each execution of a symbolic state (produced from [sexec]) represents a concrete execution + (sexec is exact). +*) +Theorem sexec_exact ctx stk ib t s1: + sem_sstate ctx stk t s1 (sexec (cf ctx) ib) -> + exists s2, iblock_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2 + /\ equiv_state s1 s2. +Proof. + intros; exploit sexec_rec_exact; eauto. + { intros sis' SEXEC; inversion SEXEC. } + repeat autodestruct; simpl; try tauto. + - intros D1 D2 ISTEP (s2 & FSTEP & EQSTEP); subst. + eexists; split; eauto. + repeat eexists; eauto. + erewrite iblock_istep_run_equiv; eauto. + - intros D1 D2 ISTEP (sis & SEXEC & _); subst. + inversion SEXEC. +Qed. + +(** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *) + +Record simu_proof_context {f1 f2: BTL.function} := Sctx { + sge1: BTL.genv; + sge2: BTL.genv; + sge_match: forall s, Genv.find_symbol sge1 s = Genv.find_symbol sge2 s; + ssp: val; + srs0: regset; + sm0: mem +}. +Arguments simu_proof_context: clear implicits. + +Definition bctx1 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge1) f1 ctx.(ssp) ctx.(srs0) ctx.(sm0). +Definition bctx2 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge2) f2 ctx.(ssp) ctx.(srs0) ctx.(sm0). + +(* NOTE: we need to mix semantical simulation and syntactic definition on [sfval] in order to abstract + the [match_states] of BTL_Schedulerproof. + + Indeed, the [match_states] involves [match_function] in [match_stackframe]. + And, here, we aim to define a notion of simulation for defining [match_function]. + + A syntactic definition of the simulation on [sfval] avoids the circularity issue. + +*) + +Inductive optsv_simu {f1 f2: function} (ctx: simu_proof_context f1 f2): (option sval) -> (option sval) -> Prop := + | Ssome_simu sv1 sv2 + (SIMU:eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2) + :optsv_simu ctx (Some sv1) (Some sv2) + | Snone_simu: optsv_simu ctx None None + . + +Inductive svident_simu {f1 f2: function} (ctx: simu_proof_context f1 f2): (sval + ident) -> (sval + ident) -> Prop := + | Sleft_simu sv1 sv2 + (SIMU:eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2) + :svident_simu ctx (inl sv1) (inl sv2) + | Sright_simu id1 id2 + (IDSIMU: id1 = id2) + :svident_simu ctx (inr id1) (inr id2) + . + +Definition bargs_simu {f1 f2: function} (ctx: simu_proof_context f1 f2) (args1 args2: list (builtin_arg sval)): Prop := + eval_list_builtin_sval (bctx1 ctx) args1 = eval_list_builtin_sval (bctx2 ctx) args2. + +Inductive sfv_simu {f1 f2} (ctx: simu_proof_context f1 f2): sfval -> sfval -> Prop := + | Sgoto_simu pc: sfv_simu ctx (Sgoto pc) (Sgoto pc) + | Scall_simu sig ros1 ros2 args1 args2 r pc + (SVID: svident_simu ctx ros1 ros2) + (ARGS:eval_list_sval (bctx1 ctx) args1 = eval_list_sval (bctx2 ctx) args2) + :sfv_simu ctx (Scall sig ros1 args1 r pc) (Scall sig ros2 args2 r pc) + | Stailcall_simu sig ros1 ros2 args1 args2 + (SVID: svident_simu ctx ros1 ros2) + (ARGS:eval_list_sval (bctx1 ctx) args1 = eval_list_sval (bctx2 ctx) args2) + :sfv_simu ctx (Stailcall sig ros1 args1) (Stailcall sig ros2 args2) + | Sbuiltin_simu ef lba1 lba2 br pc + (BARGS: bargs_simu ctx lba1 lba2) + :sfv_simu ctx (Sbuiltin ef lba1 br pc) (Sbuiltin ef lba2 br pc) + | Sjumptable_simu sv1 sv2 lpc + (VAL: eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2) + :sfv_simu ctx (Sjumptable sv1 lpc) (Sjumptable sv2 lpc) + | simu_Sreturn osv1 osv2 + (OPT:optsv_simu ctx osv1 osv2) + :sfv_simu ctx (Sreturn osv1) (Sreturn osv2) +. + +Definition sistate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (sis1 sis2:sistate): Prop := + forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sem_sistate (bctx2 ctx) sis2 rs m. + +Record si_ok ctx (sis: sistate): Prop := { + OK_PRE: (sis.(si_pre) ctx); + OK_SMEM: eval_smem ctx sis.(si_smem) <> None; + OK_SREG: forall (r: reg), eval_sval ctx (si_sreg sis r) <> None +}. + +Lemma sem_si_ok ctx sis rs m: + sem_sistate ctx sis rs m -> si_ok ctx sis. +Proof. + unfold sem_sistate; + econstructor; + intuition congruence. +Qed. + +Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2:sstate): Prop := + forall sis1 sfv1, get_soutcome (bctx1 ctx) st1 = Some (sout sis1 sfv1) -> si_ok (bctx1 ctx) sis1 -> + exists sis2 sfv2, get_soutcome (bctx2 ctx) st2 = Some (sout sis2 sfv2) + /\ sistate_simu ctx sis1 sis2 + /\ (forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sfv_simu ctx sfv1 sfv2) + . + +Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall (ctx: simu_proof_context f1 f2), sstate_simu ctx (sexec f1 ib1) (sexec f2 ib2). + +(* REM. L'approche suivie initialement ne marche pas !!! +*) +(* +Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2: sstate) := + forall t s1, sem_sstate (bctx1 ctx) t s1 st1 -> + exists s2, sem_sstate (bctx2 ctx) t s2 st2 /\ equiv_state s1 s2. + +Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall (ctx: simu_proof_context f1 f2), sstate_simu ctx (sexec f1 ib1) (sexec f2 ib2). + +Theorem symbolic_simu_correct f1 f2 ib1 ib2: + symbolic_simu f1 f2 ib1 ib2 -> + forall (ctx: simu_proof_context f1 f2) t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 -> + exists s2, iblock_step tr_inputs (sge2 ctx) (sstk2 ctx) f2 (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s2 /\ equiv_state s1 s2. +Proof. + unfold symbolic_simu, sstate_simu. + intros SIMU ctx t s1 STEP1. + exploit (sexec_correct (bctx1 ctx)); simpl; eauto. + intros; exploit SIMU; eauto. + intros (s2 & SEM1 & EQ1). + exploit (sexec_exact (bctx2 ctx)); simpl; eauto. + intros (s3 & STEP2 & EQ2). + clear STEP1; eexists; split; eauto. + eapply equiv_state_trans; eauto. +Qed. +*) + +(** * Preservation properties under a [simu_proof_context] *) + +Section SymbValPreserved. + +Variable f1 f2: function. + +Hypothesis ctx: simu_proof_context f1 f2. +Local Hint Resolve sge_match: core. + +Lemma eval_sval_preserved sv: + eval_sval (bctx1 ctx) sv = eval_sval (bctx2 ctx) sv. +Proof. + induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (bctx1 ctx) lsv = eval_list_sval (bctx2 ctx) lsv) + (P1 := fun sm => eval_smem (bctx1 ctx) sm = eval_smem (bctx2 ctx) sm); simpl; auto. + + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto. + erewrite eval_operation_preserved; eauto. + + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto. + erewrite eval_addressing_preserved; eauto. + destruct (eval_addressing _ _ _ _); 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 _ _ _ _); auto. + rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto. + rewrite IHsv1; auto. +Qed. + +Lemma list_sval_eval_preserved lsv: + eval_list_sval (bctx1 ctx) lsv = eval_list_sval (bctx2 ctx) lsv. +Proof. + induction lsv; simpl; auto. + rewrite eval_sval_preserved. destruct (eval_sval _ _); auto. + rewrite IHlsv; auto. +Qed. + +Lemma smem_eval_preserved sm: + eval_smem (bctx1 ctx) sm = eval_smem (bctx2 ctx) sm. +Proof. + induction sm; simpl; auto. + rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. + erewrite eval_addressing_preserved; eauto. + destruct (eval_addressing _ _ _ _); auto. + rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto. + rewrite eval_sval_preserved; auto. +Qed. + +Lemma eval_builtin_sval_preserved sv: + eval_builtin_sval (bctx1 ctx) sv = eval_builtin_sval (bctx2 ctx) sv. +Proof. + induction sv; simpl; auto. + all: try (erewrite eval_sval_preserved by eauto); trivial. + all: erewrite IHsv1 by eauto; erewrite IHsv2 by eauto; reflexivity. +Qed. + +Lemma eval_list_builtin_sval_preserved lsv: + eval_list_builtin_sval (bctx1 ctx) lsv = eval_list_builtin_sval (bctx2 ctx) lsv. +Proof. + induction lsv; simpl; auto. + erewrite eval_builtin_sval_preserved by eauto. + erewrite IHlsv by eauto. + reflexivity. +Qed. + +Lemma eval_scondition_preserved cond lsv: + eval_scondition (bctx1 ctx) cond lsv = eval_scondition (bctx2 ctx) cond lsv. +Proof. + unfold eval_scondition. + rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. +Qed. + +(* additional preservation properties under this additional hypothesis *) +Hypothesis senv_preserved_BTL: Senv.equiv (sge1 ctx) (sge2 ctx). + +Lemma senv_find_symbol_preserved id: + Senv.find_symbol (sge1 ctx) id = Senv.find_symbol (sge2 ctx) id. +Proof. + destruct senv_preserved_BTL as (A & B & C). congruence. +Qed. + +Lemma senv_symbol_address_preserved id ofs: + Senv.symbol_address (sge1 ctx) id ofs = Senv.symbol_address (sge2 ctx) id ofs. +Proof. + unfold Senv.symbol_address. rewrite senv_find_symbol_preserved. + reflexivity. +Qed. + +Lemma eval_builtin_sarg_preserved m: forall bs varg, + eval_builtin_sarg (bctx1 ctx) m bs varg -> + eval_builtin_sarg (bctx2 ctx) m bs varg. +Proof. + induction 1; simpl. + 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 eval_builtin_sargs_preserved m lbs vargs: + eval_builtin_sargs (bctx1 ctx) m lbs vargs -> + eval_builtin_sargs (bctx2 ctx) m lbs vargs. +Proof. + induction 1; constructor; eauto. + eapply eval_builtin_sarg_preserved; auto. +Qed. + +End SymbValPreserved. + |