(** 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 _ =>
      SOME args <- eval_list_sval ctx lsv IN
      SOME m <- eval_smem ctx sm IN
      match trap with
      | TRAP =>
          SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN
          Mem.loadv chunk m a
      | NOTRAP =>
          match eval_addressing (cge ctx) (csp ctx) addr args with
          | None => Some Vundef
          | Some a =>
              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&REG).
  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&REG).
  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&REG) 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&REG) 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&REG).
    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&REG).
    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&REG).
    rewrite Regmap.gss; simpl; auto.
    erewrite eval_list_sval_inj; simpl; auto.
    rewrite MEM; simpl. autodestruct. rewrite 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&REG).
  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&REG); 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&REG1).
  destruct H2 as (_&MEM2&REG2); 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&REG) 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&REG).
  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&REG).
  erewrite eval_list_sval_inj; simpl; auto.
  rewrite MEM; simpl; 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&REG) 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&REG).
  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. 
    autodestruct; intros.
    erewrite IHsv; do 2 autodestruct;
    erewrite eval_addressing_preserved; eauto.
  + 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.