(* A theory of symbolic execution on BTL

NB: an efficient implementation with hash-consing will be defined in another file (some day)

*)

Require Import Coqlib Maps Floats.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import RTL BTL OptionMonad.

(* TODO remove this, when copy-paste of RTLpathSE_theory is clearly over... *)
Ltac inversion_SOME := fail.  (* deprecated tactic of OptionMonad: use autodestruct instead *)
Ltac inversion_ASSERT := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *)

Record iblock_exec_context := Bctx {
  cge: BTL.genv;
  cstk: list stackframe;
  cf: function;
  csp: val;
  crs0: regset;
  cm0: mem
}.

(** * Syntax and semantics of symbolic values *)

(* symbolic value *)
Inductive sval :=
  | Sinput (r: reg)
  | Sop (op:operation) (lsv: list_sval)  (sm: smem)
  | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) 
with list_sval := 
  | Snil
  | Scons (sv: sval) (lsv: list_sval)
(* symbolic memory *)
with smem :=
  | Sinit 
  | Sstore (sm: smem) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (srce: sval).

Scheme sval_mut := Induction for sval Sort Prop
with list_sval_mut := Induction for list_sval Sort Prop
with smem_mut := Induction for smem Sort Prop.

Fixpoint list_sval_inj (l: list sval): list_sval :=
  match l with
  | nil => Snil
  | v::l => Scons v (list_sval_inj l)
  end.

Local Open Scope option_monad_scope.

Fixpoint eval_sval ctx (sv: sval): option val :=
  match sv with
  | Sinput r => Some ((crs0 ctx)#r)
  | Sop op l sm =>
     SOME args <- eval_list_sval ctx l IN
     SOME m <- eval_smem ctx sm IN
     eval_operation (cge ctx) (csp ctx) op args m
  | Sload sm trap chunk addr lsv =>
      match trap with
      | TRAP =>
          SOME args <- eval_list_sval 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 (default_notrap_load_value chunk)
          | Some a =>
              SOME m <- eval_smem ctx sm IN
              match (Mem.loadv chunk m a) with
              | None => Some (default_notrap_load_value chunk)
              | Some val => Some val
              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.

Lemma eval_list_sval_inj ctx l (sreg: reg -> sval) rs: 
  (forall r : reg, eval_sval ctx (sreg r) = Some (rs # r)) ->
  eval_list_sval ctx (list_sval_inj (map sreg l)) = Some (rs ## l).
Proof.
  intros H; induction l as [|r l]; simpl; repeat autodestruct; auto.
Qed.

Definition seval_condition ctx (cond: condition) (lsv: list_sval) (sm: smem) : option bool :=
  SOME args <- eval_list_sval ctx lsv IN
  SOME m <- eval_smem ctx sm IN
  eval_condition cond args m.


(** * Auxiliary definitions on Builtins *)
(* TODO: clean this. Some (cge ctx)neric stuffs could be put in [AST.v] *)

Section SEVAL_BUILTIN_ARG. (* adapted from Events.v *)

Variable ctx: iblock_exec_context.
Variable m: mem.

Inductive seval_builtin_arg: builtin_arg sval -> val -> Prop :=
  | seval_BA: forall x v,
      eval_sval ctx x = Some v ->
      seval_builtin_arg (BA x) v
  | seval_BA_int: forall n,
      seval_builtin_arg (BA_int n) (Vint n)
  | seval_BA_long: forall n,
      seval_builtin_arg (BA_long n) (Vlong n)
  | seval_BA_float: forall n,
      seval_builtin_arg (BA_float n) (Vfloat n)
  | seval_BA_single: forall n,
      seval_builtin_arg (BA_single n) (Vsingle n)
  | seval_BA_loadstack: forall chunk ofs v,
      Mem.loadv chunk m (Val.offset_ptr (csp ctx) ofs) = Some v ->
      seval_builtin_arg (BA_loadstack chunk ofs) v
  | seval_BA_addrstack: forall ofs,
      seval_builtin_arg (BA_addrstack ofs) (Val.offset_ptr (csp ctx) ofs)
  | seval_BA_loadglobal: forall chunk id ofs v,
      Mem.loadv chunk m (Senv.symbol_address (cge ctx) id ofs) = Some v ->
      seval_builtin_arg (BA_loadglobal chunk id ofs) v
  | seval_BA_addrglobal: forall id ofs,
      seval_builtin_arg (BA_addrglobal id ofs) (Senv.symbol_address (cge ctx) id ofs)
  | seval_BA_splitlong: forall hi lo vhi vlo,
      seval_builtin_arg hi vhi -> seval_builtin_arg lo vlo ->
      seval_builtin_arg (BA_splitlong hi lo) (Val.longofwords vhi vlo)
  | seval_BA_addptr: forall a1 a2 v1 v2,
      seval_builtin_arg a1 v1 -> seval_builtin_arg a2 v2 ->
      seval_builtin_arg (BA_addptr a1 a2)
                       (if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2)
.

Definition seval_builtin_args (al: list (builtin_arg sval)) (vl: list val) : Prop :=
  list_forall2 seval_builtin_arg al vl.

Lemma seval_builtin_arg_determ:
  forall a v, seval_builtin_arg a v -> forall v', seval_builtin_arg a v' -> v' = v.
Proof.
  induction 1; intros v' EV; inv EV; try congruence.
  f_equal; eauto.
  apply IHseval_builtin_arg1 in H3. apply IHseval_builtin_arg2 in H5. subst; auto. 
Qed.

Lemma eval_builtin_args_determ:
  forall al vl, seval_builtin_args al vl -> forall vl', seval_builtin_args al vl' -> vl' = vl.
Proof.
  induction 1; intros v' EV; inv EV; f_equal; eauto using seval_builtin_arg_determ.
Qed.

End SEVAL_BUILTIN_ARG.

(* NB: (cge ctx)neric function that could be put into [AST] file *)
Fixpoint builtin_arg_map {A B} (f: A -> B) (arg: builtin_arg A) : builtin_arg B :=
  match arg with
  | BA x => BA (f x)
  | BA_int n => BA_int n
  | BA_long n => BA_long n
  | BA_float f => BA_float f
  | BA_single s => BA_single s
  | BA_loadstack chunk ptr => BA_loadstack chunk ptr
  | BA_addrstack ptr => BA_addrstack ptr
  | BA_loadglobal chunk id ptr => BA_loadglobal chunk id ptr
  | BA_addrglobal id ptr => BA_addrglobal id ptr
  | BA_splitlong ba1 ba2 => BA_splitlong (builtin_arg_map f ba1) (builtin_arg_map f ba2)
  | BA_addptr ba1 ba2 => BA_addptr (builtin_arg_map f ba1) (builtin_arg_map f ba2)
  end.

Lemma seval_builtin_arg_correct ctx rs m sreg: forall arg varg,
  (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
  eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg ->
  seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg.
Proof.
  induction arg.
  all: try (intros varg SEVAL BARG; inv BARG; constructor; congruence).
  - intros varg SEVAL BARG. inv BARG. simpl. constructor.
    eapply IHarg1; eauto. eapply IHarg2; eauto.
  - intros varg SEVAL BARG. inv BARG. simpl. constructor.
    eapply IHarg1; eauto. eapply IHarg2; eauto.
Qed.

Lemma seval_builtin_args_correct ctx rs m sreg args vargs:
  (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
  eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs ->
  seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs.
Proof.
  induction 2.
  - constructor.
  - simpl. constructor; [| assumption].
    eapply seval_builtin_arg_correct; eauto.
Qed.

Lemma seval_builtin_arg_exact ctx rs m sreg: forall arg varg,
  (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
  seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg ->
  eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg.
Proof.
  induction arg.
  all: intros varg SEVAL BARG; try (inv BARG; constructor; congruence).
  - inv BARG. rewrite SEVAL in H0. inv H0. constructor.
  - inv BARG. simpl. constructor.
    eapply IHarg1; eauto. eapply IHarg2; eauto.
  - inv BARG. simpl. constructor.
    eapply IHarg1; eauto. eapply IHarg2; eauto.
Qed.

Lemma seval_builtin_args_exact ctx rs m sreg: forall args vargs,
  (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
  seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs ->
  eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs.
Proof.
  induction args.
  - simpl. intros. inv H0. constructor.
  - intros vargs SEVAL BARG. simpl in BARG. inv BARG.
    constructor; [| eapply IHargs; eauto].
    eapply seval_builtin_arg_exact; eauto.
Qed.

Fixpoint seval_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 <- seval_builtin_sval ctx sv1 IN
      SOME v2 <- seval_builtin_sval ctx sv2 IN
      Some (BA_splitlong v1 v2)
  | BA_addptr sv1 sv2 =>
      SOME v1 <- seval_builtin_sval ctx sv1 IN
      SOME v2 <- seval_builtin_sval ctx sv2 IN
      Some (BA_addptr v1 v2)
  | BA_int i => Some (BA_int i)
  | BA_long l => Some (BA_long l)
  | 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 <- seval_builtin_sval ctx bsv IN
                 SOME lv <- eval_list_builtin_sval ctx lbsv IN
                 Some (v::lv)
  end.

Lemma eval_list_builtin_sval_nil ctx lbs2:
  eval_list_builtin_sval ctx lbs2 = Some nil ->
  lbs2 = nil.
Proof.
  destruct lbs2; simpl; repeat autodestruct; congruence.
Qed.

Lemma seval_builtin_sval_arg ctx bs:
   forall ba m v, 
   seval_builtin_sval ctx bs = Some ba ->
   eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v ->
   seval_builtin_arg ctx m bs v.
Proof.
   induction bs; simpl; 
   try (intros ba m v H; inversion H; subst; clear H;
        intros H; inversion H; subst;
        econstructor; auto; fail).
   - intros ba m v; destruct (eval_sval _ _) eqn: SV;
     intros H; inversion H; subst; clear H.
     intros H; inversion H; subst.
     econstructor; auto.
   - intros ba m v. 
     destruct (seval_builtin_sval _ bs1) eqn: SV1; try congruence.
     destruct (seval_builtin_sval _ bs2) eqn: SV2; try congruence.
     intros H; inversion H; subst; clear H.
     intros H; inversion H; subst.
     econstructor; eauto.
   - intros ba m v. 
     destruct (seval_builtin_sval _ bs1) eqn: SV1; try congruence.
     destruct (seval_builtin_sval _ bs2) eqn: SV2; try congruence.
     intros H; inversion H; subst; clear H.
     intros H; inversion H; subst.
     econstructor; eauto.
Qed.

Lemma seval_builtin_arg_sval ctx m v: forall bs,
  seval_builtin_arg ctx m bs v ->
  exists ba,
    seval_builtin_sval ctx bs = Some ba
    /\ eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v.
Proof.
  induction 1.
  all: try (eexists; constructor; [simpl; reflexivity | constructor]).
  2-3: try assumption.
  - eexists. constructor.
    + simpl. rewrite H. reflexivity.
    + constructor.
  - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1).
    destruct IHseval_builtin_arg2 as (ba2 & A2 & B2).
    eexists. constructor.
    + simpl. rewrite A1. rewrite A2. reflexivity.
    + constructor; assumption. 
  - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1).
    destruct IHseval_builtin_arg2 as (ba2 & A2 & B2).
    eexists. constructor.
    + simpl. rewrite A1. rewrite A2. reflexivity.
    + constructor; assumption.
Qed.

Lemma seval_builtin_sval_args 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 ->
   seval_builtin_args ctx m lbs v.
Proof.
  unfold seval_builtin_args; induction lbs; simpl; intros lba m v.
  - intros H; inversion H; subst; clear H.
    intros H; inversion H. econstructor.
  - destruct (seval_builtin_sval _ _) eqn:SV; try congruence.
    destruct (eval_list_builtin_sval _ _) eqn: SVL; try congruence.
    intros H; inversion H; subst; clear H.
    intros H; inversion H; subst; clear H. 
    econstructor; eauto.
    eapply seval_builtin_sval_arg; eauto.
Qed.

Lemma seval_builtin_args_sval ctx m lv: forall lbs,
  seval_builtin_args 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 seval_builtin_arg_sval in H. destruct H as (ba & A' & B').
    eexists. constructor.
    + simpl. rewrite A'. rewrite A. reflexivity.
    + constructor; assumption.
Qed.

Lemma seval_builtin_sval_correct ctx m: forall bs1 v bs2,
  seval_builtin_arg ctx m bs1 v ->
  (seval_builtin_sval ctx bs1) = (seval_builtin_sval ctx bs2) ->
  seval_builtin_arg ctx m bs2 v.
Proof.
  intros. exploit seval_builtin_arg_sval; eauto.
  intros (ba & X1 & X2).
  eapply seval_builtin_sval_arg; eauto.
  congruence.
Qed.

Lemma eval_list_builtin_sval_correct ctx m vargs: forall lbs1,
  seval_builtin_args ctx m lbs1 vargs ->
  forall lbs2, (eval_list_builtin_sval ctx lbs1) = (eval_list_builtin_sval ctx lbs2) ->
  seval_builtin_args ctx m lbs2 vargs.
Proof.
  intros. exploit seval_builtin_args_sval; eauto.
  intros (ba & X1 & X2).
  eapply seval_builtin_sval_args; eauto.
  congruence.
Qed.

(** * Symbolic (final) value of a block *)

Inductive sfval :=
  | Sgoto (pc: exit)
  | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:exit)
    (* NB: [res] the return register is hard-wired ! Is it restrictive ? *)
  | Stailcall: signature -> sval + ident -> list_sval -> sfval
  | Sbuiltin (ef:external_function) (sargs: list (builtin_arg sval)) (res: builtin_res reg) (pc:exit)
  | Sjumptable (sv: sval) (tbl: list exit)
  | Sreturn: option sval -> sfval
.

Definition sfind_function 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
.

Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop :=
  | exec_Sgoto pc rs m:
      sem_sfval ctx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc rs m)
  | exec_Sreturn stk osv rs m m' v:
      (csp ctx) = (Vptr stk Ptrofs.zero) ->
      Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' ->
      match osv with Some sv => eval_sval ctx sv | None => Some Vundef end = Some v ->
      sem_sfval ctx (Sreturn osv) rs m 
         E0 (Returnstate (cstk ctx) v m')
  | exec_Scall rs m sig svos lsv args res pc fd:
      sfind_function ctx svos = Some fd ->
      funsig fd = sig ->
      eval_list_sval ctx lsv = Some args ->
      sem_sfval ctx (Scall sig svos lsv res pc) rs m
        E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc rs :: (cstk ctx)) fd args m)
  | exec_Stailcall stk rs m sig svos args fd m' lsv:
      sfind_function ctx svos = Some fd ->
      funsig fd = sig ->
      (csp ctx) = Vptr stk Ptrofs.zero ->
      Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' ->
      eval_list_sval ctx lsv = Some args ->
      sem_sfval ctx (Stailcall sig svos lsv) rs m
        E0 (Callstate (cstk ctx) fd args m')
  | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs:
      seval_builtin_args ctx m sargs vargs ->
      external_call ef (cge ctx) vargs m t vres m' ->
      sem_sfval ctx (Sbuiltin ef sargs res pc) rs m
        t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres rs) m')
  | exec_Sjumptable sv tbl pc' n rs m:
      eval_sval ctx sv = Some (Vint n) ->
      list_nth_z tbl (Int.unsigned n) = Some pc' ->
      sem_sfval ctx (Sjumptable sv tbl) rs m
        E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' rs m)
.

(** * Preservation properties *)

Section SymbValPreserved.

Variable ge ge': BTL.genv.

Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s.

Hypothesis senv_preserved_BTL: Senv.equiv ge ge'.

Lemma senv_find_symbol_preserved id:
  Senv.find_symbol ge id = Senv.find_symbol ge' id.
Proof.
  destruct senv_preserved_BTL as (A & B & C). congruence.
Qed.

Lemma senv_symbol_address_preserved id ofs:
  Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs.
Proof.
  unfold Senv.symbol_address. rewrite senv_find_symbol_preserved.
  reflexivity.
Qed.

Variable stk stk': list stackframe.
Variable f f': function.
Variable sp: val.
Variable rs0: regset.
Variable m0: mem.

Lemma eval_sval_preserved sv:
  eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv.
Proof.
  induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv)
                                   (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm); simpl; auto.
  + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto.
    rewrite IHsv0; clear IHsv0. destruct (eval_smem _ _); auto.
    erewrite eval_operation_preserved; eauto.
  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
    erewrite <- eval_addressing_preserved; eauto.
    destruct (eval_addressing _ sp _ _); auto.
    rewrite IHsv; auto.
  + rewrite IHsv; clear IHsv. destruct (eval_sval _ _); auto.
    rewrite IHsv0; auto.
  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
    erewrite <- eval_addressing_preserved; eauto.
    destruct (eval_addressing _ sp _ _); auto.
    rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto.
    rewrite IHsv1; auto.
Qed.

Lemma seval_builtin_arg_preserved m: forall bs varg,
  seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg ->
  seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) 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 seval_builtin_args_preserved m lbs vargs:
  seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs ->
  seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs.
Proof.
  induction 1; constructor; eauto.
  eapply seval_builtin_arg_preserved; auto.
Qed.

Lemma list_sval_eval_preserved lsv: 
  eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) 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 (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm.
Proof.
  induction sm; simpl; auto.
  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
  erewrite <- eval_addressing_preserved; eauto.
  destruct (eval_addressing _ sp _ _); auto.
  rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto.
  rewrite eval_sval_preserved; auto.
Qed.

Lemma seval_condition_preserved cond lsv sm:
  seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm.
Proof.
  unfold seval_condition.
  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
  rewrite smem_eval_preserved; auto.
Qed.

End SymbValPreserved.


(* Syntax and Semantics of symbolic internal states *)
(* [si_pre] is a precondition on initial 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 (st: sistate) (rs: regset) (m: mem): Prop :=
  st.(si_pre) ctx
  /\ eval_smem ctx st.(si_smem) = Some m
  /\ forall (r:reg), eval_sval ctx (st.(si_sreg) r) = Some (rs#r).

(* Remark that we need 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_determ ctx st rs1 m1 rs2 m2:
  sem_sistate ctx st rs1 m1 ->
  sem_sistate ctx st rs2 m2 ->
  (forall r, rs1#r = rs2#r) /\ m1 = m2.
Proof.
  intros (_&MEM1&REG1) (_&MEM2&REG2).
  intuition try congruence.
  generalize (REG1 r); rewrite REG2; congruence.
Qed.

(** * Symbolic execution of final step *)
Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
  match i with
  | Bgoto pc => Sgoto pc
  | Bcall sig ros args res pc => 
    let svos := sum_left_map sis.(si_sreg) ros in
    let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
    Scall sig svos sargs res pc
  | Btailcall sig ros args =>
    let svos := sum_left_map sis.(si_sreg) ros in
    let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
    Stailcall sig svos sargs
  | Bbuiltin ef args res pc =>
    let sargs := List.map (builtin_arg_map sis.(si_sreg)) args in
    Sbuiltin ef sargs res pc
  | Breturn or => 
    let sor := SOME r <- or IN Some (sis.(si_sreg) r) in
    Sreturn sor
  | Bjumptable reg tbl =>
    let sv := sis.(si_sreg) reg in
    Sjumptable sv tbl
  end.

Local Hint Constructors sem_sfval: core.

Lemma sexec_final_svf_correct ctx i sis t rs m s:
  sem_sistate ctx sis rs m ->
  final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s -> 
  sem_sfval ctx (sexec_final_sfv i sis) rs m t s.
Proof.
  intros (PRE&MEM&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 seval_builtin_args_correct; eauto.
  + (* Bjumptable *) intros. eapply exec_Sjumptable; eauto. congruence.
Qed.

Local Hint Constructors final_step: core.
Local Hint Resolve seval_builtin_args_exact: core.

Lemma sexec_final_svf_exact ctx i sis t rs m s:
  sem_sistate ctx sis rs m ->
  sem_sfval ctx (sexec_final_sfv i sis) rs m t s
  -> final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s.
Proof.
  intros (PRE&MEM&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 => Sinput r; si_smem:= Sinit |}.

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 (Sop op args sis.(si_smem)) 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; 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 (Sload sis.(si_smem) trap chunk addr args) sis.

Lemma sexec_load_TRAP_correct ctx chunk addr args dst sis rs m a v
 (EVAL: eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a)
 (LOAD: Mem.loadv chunk m a = Some v)
 (SIS: sem_sistate ctx sis rs m)
 :(sem_sistate ctx (sexec_load TRAP chunk addr 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; rewrite Regmap.gso; 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 := Sstore 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 seval_condition_eq ctx cond args sis rs m
  (SIS : sem_sistate ctx sis rs m)
  :seval_condition ctx cond (list_sval_inj (map (si_sreg sis) args)) (si_smem sis) = eval_condition cond rs ## args m.
Proof.
  destruct SIS as (PRE&MEM&REG); unfold seval_condition; simpl.
  erewrite eval_list_sval_inj; simpl; auto.
  erewrite MEM; auto.
Qed.

(** * symbolic execution of blocks *)

(* symbolic state *)
Inductive sstate :=
  | Sfinal (sis: sistate) (sfv: sfval)
  | Scond (cond: condition) (args: list_sval) (sm: smem) (ifso ifnot: sstate)
  | Sabort
 .

(* transition (t,s) produced by a sstate in initial context ctx *)
Inductive sem_sstate ctx t s: sstate -> Prop :=
  | sem_Sfinal sis sfv rs m
     (SIS: sem_sistate ctx sis rs m)
     (SFV: sem_sfval ctx sfv rs m t s)
     : sem_sstate ctx t s (Sfinal sis sfv)
  | sem_Scond b cond args sm ifso ifnot
     (SEVAL: seval_condition ctx cond args sm = Some b)
     (SELECT: sem_sstate ctx t s (if b then ifso else ifnot))
     : sem_sstate ctx t s (Scond cond args sm ifso ifnot)
  (* NB: Sabort: fails to produce a transition *) 
  .

(** * Idée de l'execution symbolique en Continuation Passing Style 

[k] ci-dessous est la continuation (c-a-d. la suite de la construction de l'arbre qu'on va appliquer dans chaque branche)

Rem: si manipuler une telle continuation s'avère compliqué dans les preuves,
il faudra faire autrement dans le modèle -- par exemple avec une structure de donnée 
pour représenter l'ensemble des chemins.
(même si on peut conserver le CPS dans l'implem finale, pour l'efficacité).

*)

Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := 
  match ib with
  | BF fin => Sfinal 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)
  | Bload NOTRAP chunk addr args dst => Sabort (* TODO *)
  | Bstore chunk addr args src => k (sexec_store chunk addr args src sis)
 (* composed instructions *)
  | Bseq ib1 ib2 =>
      sexec_rec ib1 sis (fun sis2 => sexec_rec ib2 sis2 k) 
  | Bcond cond args ifso ifnot _ =>
      let args := list_sval_inj (List.map sis.(si_sreg) args) in
      let ifso := sexec_rec ifso sis k in
      let ifnot := sexec_rec ifnot sis k in
      Scond cond args sis.(si_smem) ifso ifnot
  end
  .

Definition sexec ib := sexec_rec ib sis_init (fun _ => Sabort).

Local Hint Constructors sem_sstate: core.
Local Hint Resolve sexec_op_correct sexec_final_svf_correct 
                   sexec_load_TRAP_correct sexec_store_correct sis_init_correct: core.

Lemma sexec_rec_correct ctx 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 t s (k sis')
         | Some fin => final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s
         end),
  sem_sstate ctx t s (sexec_rec ib sis k).
Proof.
  induction ISTEP; simpl; try autodestruct; eauto.
  (* condition *)
  all: intros;
    eapply sem_Scond; eauto; [
      erewrite seval_condition_eq; eauto |
      replace (if b then sexec_rec ifso sis k else sexec_rec ifnot sis k) with (sexec_rec (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 ib t s: 
  iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s ->
  sem_sstate ctx t s (sexec ib).
Proof.
  destruct 1 as (rs' & m' & fin & ISTEP & FSTEP).
  eapply sexec_rec_correct; simpl; eauto.
Qed.


(* TODO: déplacer les trucs sur equiv_stackframe -> regmap_setres_eq dans BTL! *)
Inductive equiv_stackframe: stackframe -> stackframe -> Prop :=
  | equiv_stackframe_intro res f sp pc rs1 rs2
      (EQUIV: forall r : positive, rs1 !! r = rs2 !! r):
      equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2)
  .

Inductive equiv_state: state -> state -> Prop :=
  | State_equiv stack f sp pc rs1 m rs2
     (EQUIV: forall r, rs1#r = rs2#r): 
     equiv_state (State stack f sp pc rs1 m) (State stack f sp pc rs2 m)
  | Call_equiv stk stk' f args m
      (STACKS: list_forall2 equiv_stackframe stk stk'):
      equiv_state (Callstate stk f args m) (Callstate stk' f args m)
  | Return_equiv stk stk' v m
      (STACKS: list_forall2 equiv_stackframe stk stk'):
      equiv_state (Returnstate stk v m) (Returnstate stk' v m)
  .

Local Hint Constructors equiv_stackframe equiv_state: core.

Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf.
Proof.
  destruct stf; eauto.
Qed.

Lemma equiv_stack_refl stk: list_forall2 equiv_stackframe stk stk.
Proof.
  Local Hint Resolve equiv_stackframe_refl: core.
  induction stk; simpl; constructor; auto.
Qed.

Lemma equiv_state_refl s: equiv_state s s.
Proof.
  Local Hint Resolve equiv_stack_refl: core.
  induction s; simpl; constructor; auto.
Qed.

Lemma equiv_stackframe_trans stf1 stf2 stf3:
  equiv_stackframe stf1 stf2 -> equiv_stackframe stf2 stf3 -> equiv_stackframe stf1 stf3.
Proof.
  destruct 1; intros EQ; inv EQ; try econstructor; eauto.
  intros; eapply eq_trans; eauto.
Qed.

Lemma equiv_stack_trans stk1 stk2:
  list_forall2 equiv_stackframe stk1 stk2 -> 
  forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
  list_forall2 equiv_stackframe stk1 stk3.
Proof.
  Local Hint Resolve equiv_stackframe_trans: core.
  induction 1; intros stk3 EQ; inv EQ; econstructor; eauto.
Qed.

Lemma equiv_state_trans s1 s2 s3: equiv_state s1 s2 -> equiv_state s2 s3 -> equiv_state s1 s3.
Proof.
  Local Hint Resolve equiv_stack_trans: core.
  destruct 1; intros EQ; inv EQ; econstructor; eauto.
  intros; eapply eq_trans; eauto.
Qed.

Lemma regmap_setres_eq (rs rs': regset) res vres:
  (forall r, rs # r = rs' # r) ->
  forall r, (regmap_setres res vres rs) # r = (regmap_setres res vres rs') # r.
Proof.
  intros RSEQ r. destruct res; simpl; try congruence.
  destruct (peq x r).
  - subst. repeat (rewrite Regmap.gss). reflexivity.
  - repeat (rewrite Regmap.gso); auto.
Qed.

Lemma sem_sfval_equiv rs1 rs2 ctx sfv m t s:
  sem_sfval ctx sfv rs1 m t s ->
  (forall r, rs1#r = rs2#r) -> 
  exists s', equiv_state s s' /\  sem_sfval ctx sfv rs2 m t s'.
Proof. 
  Local Hint Resolve equiv_stack_refl equiv_state_refl regmap_setres_eq: core.
  Local Hint Constructors sem_sfval: core.
  destruct 1; eexists; split; econstructor; eauto.
  econstructor; eauto.
Qed.

Local Hint Resolve sexec_final_svf_exact: core.

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 sem_sistate_exclude_abort ctx sis rs m:
  sem_sistate ctx sis rs m ->
  abort_sistate ctx sis ->
  False.
Proof.
  intros SIS ABORT. inv SIS. destruct H0 as (H0 & H0').
  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
Qed.

Local Hint Resolve sem_sistate_exclude_abort: core.

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:
  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.

Local Hint Resolve sexec_op_preserves_abort sexec_load_preserves_abort
  sexec_store_preserves_abort: core.

Lemma sexec_exclude_abort ctx ib t s1: forall sis k
  (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k))
  (CONT: forall sis', sem_sstate ctx 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.
  - (* load *) destruct trap; eauto.
    inversion SEXEC.
  - (* 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.
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.
  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&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: core.

Lemma sexec_rec_exact ctx ib t s1: forall sis k
  (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k))
  rs m
  (SIS: sem_sistate ctx sis rs m)
  (CONT: forall sis', sem_sstate ctx 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 (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2
     | Some (out rs' m' None) => exists sis', (sem_sstate ctx 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_determ ctx sis rs m rs0 m0); eauto.
    intros (REG&MEM); subst.
    exploit (sem_sfval_equiv rs0 rs); eauto.
    intros (s2 & EQUIV & SFV').
    eexists; split; eauto.
  - (* Bop *) autodestruct; eauto.
  - destruct trap; [| inv SEXEC ].
    repeat autodestruct; eauto.
    all: intros; eapply CONT; eauto;
        eapply sexec_load_TRAP_abort; eauto;
        intros; 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 seval_condition_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 ib t s1: 
  sem_sstate ctx t s1 (sexec ib) ->
  exists s2, iblock_step (cge ctx) (cstk ctx) (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.