Module BTL_SEtheory


A theory of symbolic simulation (i.e. simulation of symbolic executions) on BTL blocks.


Require Import Coqlib Maps RelationClasses.
Require Import AST Integers Values Events Memory Globalenvs.
Require Import Op Registers.
Require Import RTL BTL OptionMonad.
Require Export BTL_Invariants.
Require Import ValueDomain.
Import HConsing.

Semantics of Symbolic Values


The semantics of symbolic execution is parametrized by the context of the execution of a block
Record iblock_common_context := Bcctx {
  cge: BTL.genv;
  csp: val;
  crs0: regset;
  crs1: regset;
  cm1: mem;
  cbc: block_classification;
block classification (constant on the block).
}.

Definition crsb ctx (trg : bool) (r : reg) : val :=
  (if trg then crs1 ctx else crs0 ctx)#r.
Arguments crsb !_ _ _/.


Local Open Scope option_monad_scope.

Import ListNotations.

Semantics

Definition mem_valid_accessv (m : mem) (chk : memory_chunk) (a : val) (p : permission) : Prop :=
  match a with
  | Vptr b ofs => Mem.valid_access m chk b (Ptrofs.unsigned ofs) p
  | _ => False
  end.

Fixpoint eval_sval ctx (sv: sval): option val :=
  match sv with
  | Sinput trg r _ => Some (crsb ctx trg r)
  | Sop op l _ =>
     SOME args <- eval_list_sval ctx l IN
     eval_operation (cge ctx) (csp ctx) op args (cm1 ctx)
  | Sfoldr op l sv0 _ =>
     SOME args <- eval_list_sval ctx l IN
     SOME v0 <- eval_sval ctx sv0 IN
     fold_right (fun a ob => SOME b <- ob IN
       eval_operation (cge ctx) (csp ctx) op [a;b] (cm1 ctx)) (Some v0) args
  | 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
              | Some val => Some val
              | _ => Some Vundef
              end
          end
      end
  | SmayUndef cond sv _ =>
      SOME v <- eval_sval ctx sv IN
      Some (if eval_okclauseb ctx cond then v else Vundef)
  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 (cm1 ctx)
  | Sstore sm chunk addr lsv sinfo srce _ =>
     SOME args <- eval_list_sval ctx lsv IN
     SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN
     ASSERT (if_Some_dec (store_aaddr sinfo) (vmatch_dec (cbc ctx) a)) IN
     SOME m <- eval_smem ctx sm IN
     SOME sv <- eval_sval ctx srce IN
     Mem.storev chunk m a sv
  end
with eval_okclauseb ctx (okc : okclause) : bool :=
  match okc with
  | OKfalse _ => false
  | OKalive sv _ =>
      match eval_sval ctx sv with
      | Some _ => true
      | None => false
      end
  | OKpromotableOp op prom sargs _ =>
      match eval_list_sval ctx sargs with
      | Some vargs =>
          adp_op_promotable_dec (cge ctx) (csp ctx) (cm1 ctx) op prom vargs
      | None => false
      end
  | OKpromotableCond cond prom sargs _ =>
      match eval_list_sval ctx sargs with
      | Some vargs =>
          adp_cond_promotable_dec (cm1 ctx) cond prom vargs
      | None => false
      end
  | OKaddrMatch addr lsv av _ =>
      if_Some_dec (eval_list_sval ctx lsv) (fun vargs =>
      adp_addr_match_dec (cge ctx) (cbc ctx) (csp ctx) addr vargs av)
  | OKvalidAccess perm chk addr lsv _ =>
      ex_Some_dec (eval_list_sval ctx lsv) (fun args =>
      ex_Some_dec (eval_addressing (cge ctx) (csp ctx) addr args) (fun a =>
      match a return let P := mem_valid_accessv (cm1 ctx) chk a perm in {P}+{~P} with
      | Vptr b ofs => Mem.valid_access_dec (cm1 ctx) chk b (Ptrofs.unsigned ofs) perm
      | _ => right (fun f => f)
      end))
  end.

Lemma eval_list_sval_eq ctx lsv:
  eval_list_sval ctx lsv = map_opt (eval_sval ctx) (list_of_lsv lsv).
Proof.
  induction lsv. reflexivity.
  simpl. rewrite IHlsv. reflexivity.
Qed.

Lemma eval_list_sval_length ctx lsv lv
  (EVAL : eval_list_sval ctx lsv = Some lv):
  lsv_length lsv = Datatypes.length lv.
Proof.
  rewrite lsv_length_eq.
  rewrite eval_list_sval_eq in EVAL.
  apply map_opt_length in EVAL; auto.
Qed.


Wrapping the evaluation in the option monad
Definition eval_osv ctx (osv: option sval): option val :=
  SOME sv' <- osv IN eval_sval ctx sv'.

Notations to make lemmas more readable
Module SvalNotations.
Notation "'sval_equiv' ctx sv1 sv2" := (eval_sval ctx sv1 = eval_sval ctx sv2)
  (only parsing, at level 0, ctx at next level, sv1 at next level, sv2 at next level).

Notation "'list_sval_equiv' ctx lsv1 lsv2" := (eval_list_sval ctx lsv1 = eval_list_sval ctx lsv2)
  (only parsing, at level 0, ctx at next level, lsv1 at next level, lsv2 at next level).

Notation "'smem_equiv' ctx sm1 sm2" := (eval_smem ctx sm1 = eval_smem ctx sm2)
  (only parsing, at level 0, ctx at next level, sm1 at next level, sm2 at next level).

Notation "'alive' o" := (o = None -> False) (at level 0).

End SvalNotations.
Import SvalNotations.

Lemma elim_alive [A] [x : option A] (H : alive x):
  {y : A | x = Some y}.
Proof.
  destruct x. eauto. congruence.
Qed.

Lemma map_opt_alive [A B] (f : A -> option B) l:
  alive (map_opt f l) <-> Forall (fun x => alive (f x)) l.
Proof.
  induction l.
  - simpl. rewrite Forall_nil_iff; split; auto; congruence.
  - simpl. rewrite Forall_cons_iff, <- IHl.
    repeat autodestruct; intuition congruence.
Qed.

Evaluation of okclause as a predicate

Definition eval_okclause ctx (c : okclause) : Prop :=
  match c with
  | OKfalse _ =>
      False
  | OKalive sv _ =>
      alive (eval_sval ctx sv)
  | OKpromotableOp op prom sargs _ =>
      exists args : list val,
        eval_list_sval ctx sargs = Some args /\
        adp_op_promotable (cge ctx) (csp ctx) (cm1 ctx) op prom args
  | OKpromotableCond cond prom sargs _ =>
      exists args : list val,
        eval_list_sval ctx sargs = Some args /\
        adp_cond_promotable (cm1 ctx) cond prom args
  | OKaddrMatch addr lsv av _ =>
      if_Some (eval_list_sval ctx lsv) (fun vargs =>
      adp_addr_match (cge ctx) (cbc ctx) (csp ctx) addr vargs av)
  | OKvalidAccess perm chk addr lsv _ =>
      ex_Some (eval_list_sval ctx lsv) (fun args =>
      ex_Some (eval_addressing (cge ctx) (csp ctx) addr args) (fun a =>
      mem_valid_accessv (cm1 ctx) chk a perm))
  end.

Lemma proj_sumbool_true_iff [P] (p : {P}+{~P}):
  proj_sumbool p = true <-> P.
Proof.
  case p; simpl; split; auto; congruence.
Qed.

Lemma eval_okclauseb_iff ctx c:
  eval_okclauseb ctx c = true <-> eval_okclause ctx c.
Proof.
  destruct c; simpl;
    try (split; solve [congruence | tauto]);
    let intro_dc :=
      intro H; decompose [Logic.ex Logic.and] H in
    repeat (autodestruct; first [split; intro_dc; congruence | intro]);
    rewrite proj_sumbool_true_iff; split; intro_dc; do 2 try_simplify_someHyps.
Qed.

Lemma eval_okclauseb_spec ctx c:
  BoolSpec (eval_okclause ctx c) (~eval_okclause ctx c) (eval_okclauseb ctx c).
Proof.
  specialize (eval_okclauseb_iff ctx c) as E.
  destruct eval_okclauseb; constructor.
  - apply E; reflexivity.
  - intro H. apply E in H. congruence.
Qed.

Semantics of partial affine forms with Sfoldr

Scaling affine forms

Section Scale.

Variable scalev: val -> val.
Variable select_op: operation -> bool.

Hypothesis scalev_distr: forall ctx op v1 scv1 v2,
  select_op op = true ->
  scalev v1 = scv1 ->
  eval_operation (cge ctx) (csp ctx) op [scv1; scalev v2] (cm1 ctx) =
  SOME r <- eval_operation (cge ctx) (csp ctx) op [v1; v2] (cm1 ctx) IN Some (scalev r).

Lemma scalev_distr_list ctx op v0 scv0
  (SCALE_v0: scalev v0 = scv0)
  (OK_op: select_op op = true)
  :forall l scl
  (SCALE_l: fold_right (fun a l0 => scalev a::l0) nil l = scl),
  fold_right (fun a ob => SOME b <- ob IN
    eval_operation (cge ctx) (csp ctx) op [a;b] (cm1 ctx)) (Some scv0) scl =
  SOME r <- fold_right (fun a ob => SOME b <- ob IN
      eval_operation (cge ctx) (csp ctx) op [a;b] (cm1 ctx)) (Some v0) l IN
  Some (scalev r).
Proof.
  induction l; simpl.
  - intros; subst; simpl; auto.
  - intros lsc. clear SCALE_v0.
    intros ACC0; inv ACC0; simpl.
    rewrite IHl; clear IHl; auto.
    autodestruct. auto.
Qed.

Variable scale: sval -> sval.

Hypothesis scale_correct: forall ctx sv,
  eval_sval ctx (scale sv) = SOME v <- eval_sval ctx sv IN Some (scalev v).

Fixpoint scale_l (lsv: list_sval): list_sval :=
  match lsv with
  | Snil _ => fSnil
  | Scons sv lsv' _ => fScons (scale sv) (scale_l lsv')
  end.

Lemma scale_l_correct: forall ctx lsv,
  eval_list_sval ctx (scale_l lsv) = SOME lv <- eval_list_sval ctx lsv IN
  Some (fold_right (fun a l0 => scalev a::l0) nil lv).
Proof.
  induction lsv; simpl; auto.
  rewrite scale_correct with (sv:=sv); auto.
  autodestruct. rewrite IHlsv; auto.
  simplify_option.
Qed.

Definition rescale (sv: sval): sval :=
  match sv with
  | Sfoldr op l sv0 _ =>
      if select_op op then fSfoldr op (scale_l l) (scale sv0)
      else scale sv
  | _ => scale sv
  end.

Theorem rescale_correct ctx sv v:
  eval_sval ctx (scale sv) = Some v ->
  eval_sval ctx (rescale sv) = Some v.
Proof.
  unfold rescale. do 2 autodestruct.
  intros OP _ ; simpl.
  rewrite !scale_correct; auto.
  rewrite scale_l_correct with (lsv:=lsv); auto.
  simpl; do 3 autodestruct; intros FOLD ESV ELSV HI; inv HI.
  erewrite scalev_distr_list; auto.
  rewrite FOLD; reflexivity.
Qed.

End Scale.

Import Datatypes.

Accumulating and merging affine forms

Section Accumulate.

Variable accv: val -> val -> val.
Variable select_op: operation -> bool.

Hypothesis accv_eval: forall ctx v1 v2 op,
    select_op op = true ->
    eval_operation (cge ctx) (csp ctx) op [v1; v2] (cm1 ctx) = Some (accv v1 v2).

Hypothesis accv_commut: forall v1 v2, accv v1 v2 = accv v2 v1.

Hypothesis accv_assoc: forall v1 v2 v3, accv v1 (accv v2 v3) = accv (accv v1 v2) v3.

Lemma accv_assoc_list ctx op vl v0 accv0
  (ACC_vr: accv vl v0 = accv0)
  (OK_op: select_op op = true)
  :forall l vr
  (ACC_l: fold_right (fun a ob => SOME b <- ob IN
    eval_operation (cge ctx) (csp ctx) op [a;b] (cm1 ctx)) (Some v0) l = Some vr),
  fold_right (fun a ob => SOME b <- ob IN
    eval_operation (cge ctx) (csp ctx) op [a;b] (cm1 ctx)) (Some accv0) l =
  Some (accv vl vr).
Proof.
  induction l; simpl.
  - try_simplify_someHyps.
  - intros vr. autodestruct.
    intros FOLD. erewrite IHl; eauto.
    rewrite !accv_eval; auto.
    intros HI; inv HI.
    rewrite !accv_assoc, (accv_commut a vl); reflexivity.
Qed.

Variable merge1: sval -> sval -> option sval.
Variable acc0: sval -> sval -> sval.
Variable compare: sval -> sval -> comparison.

Hypothesis compare_correct: forall ctx sv1 sv2 sv3,
  compare sv1 sv2 = Eq ->
  merge1 sv1 sv2 = Some sv3 ->
  eval_sval ctx sv3 =
  SOME v1 <- eval_sval ctx sv1 IN
  SOME v2 <- eval_sval ctx sv2 IN Some (accv v1 v2).

Hypothesis acc0_correct: forall ctx (sv1 sv2: sval),
  eval_sval ctx (acc0 sv1 sv2) =
  SOME v1 <- eval_sval ctx sv1 IN
  SOME v2 <- eval_sval ctx sv2 IN Some (accv v1 v2).

Fixpoint merge (l1 l2: list_sval) {struct l1}: list_sval :=
  match l1 with
  | Snil _ => l2
  | Scons sv1 l1' _ =>
     (fix merge_in l2 { struct l2 } :=
     match l2 with
     | Snil _ => l1
     | Scons sv2 l2' _ =>
       match compare sv1 sv2 with
       | Lt => fScons sv1 (merge l1' l2)
       | Eq => match merge1 sv1 sv2 with
               | Some sv3 => fScons sv3 (merge l1' l2')
               | None => fScons sv1 (fScons sv2 (merge l1' l2'))
               end
       | Gt => fScons sv2 (merge_in l2')
       end
    end) l2
  end.

Theorem merge_correct ctx l1 op
  (OK_op: select_op op = true): forall l2 v1 v2 sv0_1 sv0_2 h1 h2,
  eval_sval ctx (Sfoldr op l1 sv0_1 h1) = Some v1 ->
  eval_sval ctx (Sfoldr op l2 sv0_2 h2) = Some v2 ->
  eval_sval ctx (fSfoldr op (merge l1 l2) (acc0 sv0_1 sv0_2)) = Some (accv v1 v2).
Proof.
  induction l1; simpl.
  - intros until sv0_2; intros _ _.
    autodestruct; intros EV01 HI; inv HI.
    do 2 autodestruct. rewrite acc0_correct.
    intros EV02 ELV2 FOLD. rewrite EV01, EV02.
    intros; eapply accv_assoc_list; eauto.
  - do 2 autodestruct. intros ELV1 ESV l2.
    induction l2; simpl; intros until sv0_2; intros _ _.
    + do 3 autodestruct; intros EV02 FOLD EV01 ACC0 HI; inv HI.
      rewrite ESV, ELV1, acc0_correct, EV01, EV02; trivial.
      simpl. set (vacc:=accv v0 v2).
      erewrite accv_assoc_list with (accv0:=vacc) (v0:=v0); eauto.
      rewrite accv_eval in *; auto. inv ACC0.
      rewrite <- !accv_assoc, (accv_commut v2 v3); reflexivity.
    + do 5 autodestruct; intros EV02 ELV2 ESV0 FOLD0 EV01 ACC0 FOLD1.
      revert FOLD1; simpl; autodestruct; intros FOLD1 ACC1.
      autodestruct; intros COMP.
      * generalize (IHl1 l2 v3 v6 sv0_1 sv0_2).
        simpl. rewrite ELV1, ELV2, EV01, EV02.
        intros IHl1S; exploit IHl1S; eauto; clear IHl1S.
        do 2 autodestruct.
        intros ACC2 ELVM IHl1S. autodestruct.
        -- intros MERGE1; simpl. erewrite compare_correct; eauto.
           rewrite ESV, ESV0, ELVM; simpl. rewrite IHl1S.
           erewrite accv_eval in *; eauto. inv ACC0; inv ACC1.
           rewrite !accv_assoc; do 2 f_equal.
           rewrite <- !accv_assoc, (accv_commut v3 v4); reflexivity.
        -- intros; simpl. rewrite ESV, ESV0, ELVM; simpl. rewrite IHl1S.
           erewrite !accv_eval in *; eauto. inv ACC0; inv ACC1.
           rewrite !accv_assoc; do 2 f_equal.
           rewrite <- !accv_assoc, (accv_commut v3 v4); reflexivity.
      * generalize (IHl1 (Scons sv0 l2 hid1) v3 v2 sv0_1 sv0_2).
        simpl. rewrite ELV1, ELV2, !acc0_correct, ESV, ESV0, EV01, EV02; trivial.
        intros IHl1S; exploit IHl1S; eauto; clear IHl1S.
        { simpl; rewrite FOLD1; auto. } autodestruct.
        simpl. intros ELVM IHl1S. rewrite IHl1S.
        erewrite accv_eval in *; eauto. inv ACC0; inv ACC1.
        rewrite !accv_assoc; reflexivity.
      * generalize (IHl2 v1 v6 sv0_1 sv0_2).
        simpl. rewrite !acc0_correct, ESV0, EV01, EV02; trivial.
        intros IHl2S; exploit IHl2S; eauto; clear IHl2S.
        { rewrite FOLD0; auto. }
        autodestruct.
        simpl. intros ELVM IHl2S. rewrite IHl2S.
        erewrite accv_eval in *; eauto. inv ACC0; inv ACC1.
        rewrite !accv_assoc; do 2 f_equal.
        rewrite <- accv_assoc, accv_commut; reflexivity.
Qed.

End Accumulate.

End of semantics of partial affine forms

Lemma root_apply_morph_equiv o args0 args1 sm0 sm1 ctx
  (EARGS: list_sval_equiv ctx args0 args1)
  (EMEM: smem_equiv ctx sm0 sm1):
  sval_equiv ctx (root_apply o args0 sm0) (root_apply o args1 sm1).
Proof.
  destruct o; [|destruct aaddr]; simpl; rewrite ?EARGS, ?EMEM; reflexivity.
Qed.

Inductive optsv_simu ctx: option sval -> option sval -> Prop :=
  | Ssome_simu sv1 sv2
      (SIMU: sval_equiv ctx sv1 sv2)
     :optsv_simu ctx (Some sv1) (Some sv2)
  | Snone_simu: optsv_simu ctx None None
.

Global Instance optsv_simu_Equivalence {ctx} : Equivalence (optsv_simu ctx).
Proof.
  constructor.
  - intros []; constructor; reflexivity.
  - intros ? ? []; constructor; auto.
  - intros ? ? ?; do 2 inversion 1; try constructor; auto.
    rewrite SIMU. apply SIMU0.
Qed.

Definition eval_scondition ctx (cond: condition) (lsv: list_sval): option bool :=
  SOME args <- eval_list_sval ctx lsv IN
  eval_condition cond args (cm1 ctx).

The symbolic memory preserves Mem.perm with respect to initial memory. Hence, arithmetic operations, boolean conditions and success of the loads 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, eval_scondition_eq and loadRange_preserved.
Lemma mem_perm_preserv ctx sm m b ofs k p
  (EVAL : eval_smem ctx sm = Some m):
  Mem.perm (cm1 ctx) b ofs k p <-> Mem.perm m b ofs k p.
Proof.
  revert m EVAL; induction sm; simpl; try_simplify_someHyps.
  - reflexivity.
  - unfold Mem.storev; repeat autodestruct; intros.
    erewrite IHsm by reflexivity.
    split; [eapply Mem.perm_store_1|eapply Mem.perm_store_2]; eassumption.
Qed.

Lemma valid_pointer_preserv ctx sm m b ofs
  (EVAL : eval_smem ctx sm = Some m):
  Mem.valid_pointer (cm1 ctx) b ofs = Mem.valid_pointer m b ofs.
Proof.
  apply rew_proj_sumbool_dec.
  eapply mem_perm_preserv; exact EVAL.
Qed.
Local Hint Resolve valid_pointer_preserv: core.

Lemma mem_valid_access_preserv ctx sm m chk b p perm
  (EVAL : eval_smem ctx sm = Some m):
  Mem.valid_access (cm1 ctx) chk b p perm <-> Mem.valid_access m chk b p perm.
Proof.
  unfold Mem.valid_access, Mem.range_perm.
  apply and_iff_compat_r.
  do 2 (apply Morphisms_Prop.all_iff_morphism; intro).
  eapply mem_perm_preserv, EVAL.
Qed.

Lemma mem_valid_accessv_preserv ctx sm m chk a perm
  (EVAL : eval_smem ctx sm = Some m):
  mem_valid_accessv (cm1 ctx) chk a perm <-> mem_valid_accessv m chk a perm.
Proof.
  unfold mem_valid_accessv; destruct a; try reflexivity.
  eapply mem_valid_access_preserv, EVAL.
Qed.

Map reg -> option sval

Definition sreg_ok ctx (sreg: reg -> option sval): Prop :=
  forall r sv, sreg r = Some sv -> eval_sval ctx sv <> None.

Definition match_sreg ctx (sreg: reg -> option sval) (rs: regset): Prop :=
  forall r sv, sreg r = Some sv -> eval_sval ctx sv = Some (rs#r).

Lemma match_sreg_ok ctx sreg rs:
  match_sreg ctx sreg rs -> sreg_ok ctx sreg.
Proof.
  intros MATCH r sv H; erewrite MATCH; eauto. congruence.
Qed.
Local Hint Resolve match_sreg_ok: core.

Definition sreg_eq ctx : Relation_Definitions.relation (reg -> option sval) :=
  Morphisms.pointwise_relation reg (optsv_simu ctx).

Lemma sreg_ok_morph ctx:
  forall sr0 sr1 (H : sreg_eq ctx sr0 sr1),
  sreg_ok ctx sr0 <-> sreg_ok ctx sr1.
Proof.
  symmetric_iff.
  intros sr0 sr1 H OK r sv R1.
  specialize (H r); rewrite R1 in H; inv H.
  rewrite <- SIMU.
  eapply OK; eauto.
Qed.

Definition total_sreg [A B] (rs : A -> option B) :=
  forall r, alive (rs r).

The semantics of SIs.

Section SI_Semantics.

Definition si_ok ctx (si: fpasv): Prop :=
  forall sv, List.In sv (fpa_ok si) -> eval_sval ctx sv <> None.

Lemma si_ok_eval si r sv ctx:
  si_ok ctx si -> si r=Some sv -> eval_sval ctx sv <> None.
Proof.
   intros OK H.
   apply fpa_wf in H as [[]|]; simpl; auto; congruence.
Qed.

Lemma si_ok_sreg ctx (si: fpasv):
  si_ok ctx si -> sreg_ok ctx si.
Proof.
  intros OK r sv. apply si_ok_eval; auto.
Qed.

Definition match_si ctx (si: fpasv) (rs: regset): Prop :=
  si_ok ctx si /\ match_sreg ctx si rs.

Lemma match_si_ok ctx si rs:
  match_si ctx si rs -> si_ok ctx si.
Proof.
  destruct 1; auto.
Qed.
Local Hint Resolve match_si_ok si_ok_sreg: core.

Definition match_meminv ctx (im : imem) (m : mem): Prop :=
  eval_smem ctx (imem_subst im) = Some m.

Definition match_invs ctx (csix: invariants) (src_mem : mem): Prop :=
  match_si ctx (history csix) (crs0 ctx) /\
  match_si ctx (glue csix) (crs1 ctx) /\
  match_meminv ctx (meminv csix) src_mem.

Lemma only_liveness_match_si ctx si:
  only_liveness si -> match_si ctx si (crs0 ctx).
Proof.
  intros (ONLYok & ONLY); split.
  - intros sv. rewrite ONLYok; simpl. intuition.
  - intros r sv EQ. exploit ONLY; eauto.
    intros; subst; simpl; auto.
Qed.
Local Hint Resolve only_liveness_match_si: core.

Lemma only_liveness_match_invs ctx csix:
  only_liveness (history csix) ->
  only_liveness (glue csix) ->
  meminv csix = nil ->
  crs1 ctx = crs0 ctx ->
  match_invs ctx csix (cm1 ctx).
Proof.
  unfold match_invs; intros ? ? -> ->; intuition eauto.
  reflexivity.
Qed.


Section SVDEP_CORRECT.
  Variables (ge : genv) (sp : val) (rs0 rs0' rs1 rs1' : regset) (m : mem) (bc : block_classification).
  Let ctx1 := Bcctx ge sp rs0 rs1 m bc.
  Let ctx2 := Bcctx ge sp rs0' rs1' m bc.

Lemma svdep_preserv_comb:
  let GOAL [S V] (d : S -> bool -> reg -> Prop) (e : _ -> S -> V) :=
    forall (s : S) (EQREGS : forall trg r, d s trg r -> crsb ctx1 trg r = crsb ctx2 trg r),
    e ctx1 s = e ctx2 s in
  GOAL svdep eval_sval /\
  GOAL lsvdep eval_list_sval /\
  GOAL smdep eval_smem /\
  GOAL okclausedep eval_okclauseb.
Proof.
  apply sval_mut_comb;
    intros; simpl in *; auto;
    try solve [rewrite ?H, ?H0, ?H1 by (intros; apply EQREGS; auto); reflexivity].
  - (* Sinput *)
    f_equal; apply EQREGS; auto.
Qed.

Lemma svdep_preserv sv:
  forall (EQREGS : forall trg r, svdep sv trg r -> crsb ctx1 trg r = crsb ctx2 trg r),
  eval_sval ctx1 sv = eval_sval ctx2 sv.
Proof.
apply svdep_preserv_comb. Qed.

Lemma smdep_preserv sm:
  forall (EQREGS : forall trg r, smdep sm trg r -> crsb ctx1 trg r = crsb ctx2 trg r),
  eval_smem ctx1 sm = eval_smem ctx2 sm.
Proof.
apply svdep_preserv_comb. Qed.

Lemma svfree_preserv r sv
  (EQREGS: forall r0, r0 <> r -> rs0#r0 = rs0'#r0 /\ rs1#r0 = rs1'#r0)
  (SVFREE: svfree sv r):
  eval_sval ctx1 sv = eval_sval ctx2 sv.
Proof.
  apply svdep_preserv.
  intros [|] r0 DEP; apply EQREGS;
  intros ->; exact (SVFREE _ DEP).
Qed.

End SVDEP_CORRECT.

Lemma fold_right_ext {A B} (f1 f2: A -> B -> B) b l:
  (forall x y, f1 x y = f2 x y) ->
  fold_right f1 b l = fold_right f2 b l.
Proof.
  intros EQ; induction l; simpl; auto.
  rewrite IHl, EQ; reflexivity.
Qed.

Lemma svfreem_preserv ge sp rs0 rs1 m1 bc1 m2 bc2 sv:
  let ctx1 := Bcctx ge sp rs0 rs1 m1 bc1 in
  let ctx2 := Bcctx ge sp rs0 rs1 m2 bc2 in
  svfreem sv ->
  eval_sval ctx1 sv = eval_sval ctx2 sv.
Proof.
  do 2 intro.
  induction sv using sval_mut with
    (P0 := fun lsv => lsvfreem lsv -> eval_list_sval ctx1 lsv = eval_list_sval ctx2 lsv)
    (P1 := fun sm => True)
    (P2 := fun ok => okclausefreem ok -> eval_okclauseb ctx1 ok = eval_okclauseb ctx2 ok);
    simpl in *;
    try solve [ tauto
              | intro H; decompose [ Logic.and ] H;
                rewrite ?IHsv, ?IHsv0, ?IHsv1;
                auto ].
  + intros (SMF & LSVF). rewrite IHsv; auto.
    autodestruct.
    intros; eapply op_depends_on_memory_correct; eauto.
  + intros (SMF & LSVF & SVF). rewrite IHsv, IHsv0; auto.
    do 2 autodestruct.
    intros; eapply fold_right_ext.
    intros; destruct y; auto.
    eapply op_depends_on_memory_correct; eauto.
Qed.

Lemma matchsi_update_r ge sp rs0 rs1 rs2 m bc res (csi: csasv)
  (FREE: sifree csi res)
  (ONLYLIVEr: forall sv, csi res = Some sv -> sv = fSinput false res)
  (MATCH: match_si (Bcctx ge sp rs0 rs1 m bc) (csi_remove res csi) rs2)
  :forall v, match_si (Bcctx ge sp (rs0#res <- v) (rs1#res <- v) m bc) csi (rs2#res <- v).
Proof.
  destruct FREE as (FREE_In & FREE).
  unfold match_si, sifree.
  intros v; split.
  - intros sv H H0.
    exploit match_si_ok; eauto.
    erewrite svfree_preserv; eauto.
    intros; rewrite !PMap.gso; eauto.
  - intro r; rewrite PMap.gsspec; destruct peq as [<-|DIFF].
    + intros sv EQ; exploit ONLYLIVEr; simpl; eauto.
      intros X; inv X; simpl in *.
      rewrite PMap.gss; eauto.
    + intros sv EQ.
      generalize EQ; erewrite <- csi_gro by eauto; intros EQr.
      case MATCH as (_ & <-); eauto.
      apply FREE in EQ as [[]|FREE_SV].
      * simpl. rewrite PMap.gso; eauto.
      * eapply svfree_preserv; eauto.
        intros; rewrite !PMap.gso; eauto.
Qed.

Lemma matchsi_update_m ge sp rs0 rs1 rs2 m1 bc1 m2 bc2 (si: fpasv)
  (FREEm: sifreem si)
  (MATCH: match_si (Bcctx ge sp rs0 rs1 m1 bc1) si rs2)
  :match_si (Bcctx ge sp rs0 rs1 m2 bc2) si rs2.
Proof.
  unfold sifreem in *.
  destruct MATCH as (MATCH_In & MATCH); split.
  * intros sv H H0; eapply MATCH_In; eauto.
    erewrite svfreem_preserv; eauto.
  * intros r sv H.
    erewrite svfreem_preserv; eauto.
    apply fpa_wf in H as [[]|]; simpl; eauto.
Qed.
Local Hint Resolve matchsi_update_m: core.

Lemma matchinvs_update_m ge sp rs0 rs1 m1 bc1 m1' m2 bc2 csix:
  sifreem (history csix) ->
  sifreem (glue csix) ->
  meminv csix = nil ->
  match_invs (Bcctx ge sp rs0 rs1 m1 bc1) csix m1' ->
  match_invs (Bcctx ge sp rs0 rs1 m2 bc2) csix m2.
Proof.
  unfold match_invs; simpl; intuition eauto.
  rewrite H1; reflexivity.
Qed.

Lemma clobbered_compat_sifreem csi res: clobbered_compat csi res -> sifreem csi.
Proof.
  intros [_ FREEm _]; auto.
Qed.

Lemma clobbered_compat_sifreem_remove csi res:
  clobbered_compat csi res -> sifreem (csi_remove res csi).
Proof.
  intros [_ FREEm _]; auto.
Qed.

Local Hint Resolve clobbered_compat_sifreem clobbered_compat_sifreem_remove: core.

Lemma clobbered_compat_matchsi_preserv ge sp rs0 rs1 rs2 m1 bc1 csi res:
  clobbered_compat csi res ->
  match_si (Bcctx ge sp rs0 rs1 m1 bc1) (csi_remove res csi) rs2 ->
  forall v m2 bc2, match_si (Bcctx ge sp (rs0#res <- v) (rs1#res <- v) m2 bc2) csi (rs2#res <- v).
Proof.
  intros COMPAT MATCHSI v m2 bc2; eapply matchsi_update_m; eauto.
  destruct COMPAT. eapply matchsi_update_r; eauto.
Qed.

Local Hint Resolve clobbered_compat_matchsi_preserv: core.

Lemma clobbered_compat_matchinvs_preserv ge sp rs0 rs1 m1 bc1 m0 (csix: invariants) res:
  clobbered_compat (history csix) res ->
  clobbered_compat (glue csix) res ->
  meminv csix = nil ->
  match_invs (Bcctx ge sp rs0 rs1 m1 bc1) (csix_remove res csix) m0 ->
  forall v m2 bc2, match_invs (Bcctx ge sp (rs0#res <- v) (rs1#res <- v) m2 bc2) csix m2.
Proof.
  unfold csix_remove, match_invs; simpl; intuition eauto.
  rewrite H1; reflexivity.
Qed.

Lemma match_si_rstrg_preserv ge sp rs0 rs1 rs1' rs2 m bc si:
  si_trg_free si ->
  match_si (Bcctx ge sp rs0 rs1 m bc) si rs2 ->
  match_si (Bcctx ge sp rs0 rs1' m bc) si rs2.
Proof.
  intros (FOK & FRG) (SOK & SRG).
  split.
  - intros ? HIN.
    erewrite svdep_preserv. apply SOK; auto.
    intros [|] ? DEP; first [reflexivity|exfalso].
    eapply Forall_forall in FOK; eauto.
    exact (FOK _ DEP).
  - intros ? ? SI.
    erewrite svdep_preserv. apply SRG; auto.
    intros [|] ? DEP; first [reflexivity|exfalso].
    eapply if_Some_iff in FRG; eauto.
    exact (FRG _ DEP).
Qed.

End SI_Semantics.

Symbolic (final) value of a block


Definition sfval := finalA sval.

Section MAP_FINAL.

Lemma map_builtin_arg_opt_inst: map_opt_inst builtin_arg (@map_builtin_arg_opt).
Proof.
  split.
  - induction a; simpl; rewrite ?IHa1, ?IHa2; reflexivity.
  - induction a; simpl; rewrite ?IHa1, ?IHa2; repeat (simpl; autodestruct); reflexivity.
  - induction a; intros b M0; simpl in M0; revert M0; repeat autodestruct;
    simpl; intros;
    erewrite ?E, ?IHa1, ?IHa2 by first [eassumption|reflexivity];
    exact M0.
Qed.

Lemma map_builtin_arg_opt_tot [A B] (f : A -> B) (ba : builtin_arg A):
  map_builtin_arg_opt (fun x => Some (f x)) ba = Some (map_builtin_arg f ba).
Proof.
  induction ba; simpl; rewrite ?IHba1, ?IHba2; reflexivity.
Qed.

Definition map_sum_left_opt {A B C} (f : A -> option B) (x : A + C): option (B + C) :=
  match x with
  | inl y => SOME r <- f y IN Some (inl r)
  | inr z => Some (inr z)
  end.

Definition map_option_opt [A B] (f : A -> option B) (x : option A) : option (option B) :=
  match x with
  | Some x => SOME y <- f x IN Some (Some y)
  | None => Some None
  end.

Definition map_final_opt [A B] (f : A -> option B) (fin : finalA A) : option (finalA B) :=
  match fin with
  | Bgoto pc => Some (Bgoto pc)
  | Breturn o => SOME o' <- map_option_opt f o IN Some (Breturn o')
  | Bcall sig fd args res pc =>
      SOME fd' <- map_sum_left_opt f fd IN
      SOME args' <- map_opt f args IN
      Some (Bcall sig fd' args' res pc)
  | Btailcall sig fd args =>
      SOME fd' <- map_sum_left_opt f fd IN
      SOME args' <- map_opt f args IN
      Some (Btailcall sig fd' args')
  | Bbuiltin bf args res pc =>
      SOME args' <- map_opt (map_builtin_arg_opt f) args IN
      Some (Bbuiltin bf args' res pc)
  | Bjumptable arg tbl =>
      SOME arg' <- f arg IN
      Some (Bjumptable arg' tbl)
  end.

Lemma map_final_opt_inst: map_opt_inst finalA (@map_final_opt).
Proof.
  pose proof (map_lbargs_inst := map_opt_inst_comp map_list_opt_inst map_builtin_arg_opt_inst).
  split.
  - destruct a; try destruct res; try destruct fn; simpl;
    rewrite ?(map_opt_inst_id map_list_opt_inst), ?(map_opt_inst_id map_lbargs_inst);
    reflexivity.
  - destruct a; try destruct res; try destruct fn; simpl;
    rewrite ?(map_opt_inst_bind map_list_opt_inst), ?(map_opt_inst_bind map_lbargs_inst);
    repeat (simpl; autodestruct); reflexivity.
  - destruct a; try destruct res; try destruct fn; intros; simpl in M0;
    revert M0; repeat autodestruct; intros; simpl;
    erewrite ?E, ?(map_opt_inst_ext1 map_list_opt_inst), ?(map_opt_inst_ext1 map_lbargs_inst) by eassumption;
    exact M0.
Qed.

End MAP_FINAL.


Lemma eval_builtin_arg_v [A] ge (f : A -> val) sp m ba v:
  eval_builtin_arg ge f sp m ba v <-> eval_builtin_arg ge (fun v => v) sp m (map_builtin_arg f ba) v.
Proof.
  split.
  - induction 1; simpl; constructor; auto.
  - remember (map_builtin_arg f ba) as mba eqn:ba_eq.
    intro EVAL; revert ba ba_eq.
    induction EVAL; simpl;
    intros [ ]; inversion 1; subst; constructor; eauto.
Qed.

Lemma eval_builtin_args_v [A] ge (f : A -> val) sp m args vs:
  eval_builtin_args ge f sp m args vs <->
  eval_builtin_args ge (fun v => v) sp m (map (map_builtin_arg f) args) vs.
Proof.
  unfold eval_builtin_args.
  rewrite list_forall2_map1.
  split; (intro H; eapply list_forall2_imply; [exact H|do 4 intro; rewrite eval_builtin_arg_v; auto]).
Qed.

Section ValuesSemantic.
  Variable (ge : genv).

Definition find_function_v (fp: val + qualident) : option fundef :=
  match fp with
  | inl v => Genv.find_funct ge v
  | inr symb =>
      match Genv.find_symbol ge symb with
      | None => None
      | Some b => Genv.find_funct_ptr ge b
      end
  end.

  Variables (stack : list stackframe) (f : function) (sp : val)
            (rs : regset) (m : mem) (bc : block_classification).

Inductive final_step_v : finalA val -> trace -> state -> Prop :=
  | vexec_Bgoto pc:
      final_step_v (Bgoto pc) E0 (State stack f sp pc rs m bc)
  | vexec_Breturn ov stk m' bc':
      sp = (Vptr stk Ptrofs.zero) ->
      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
      final_step_v (Breturn ov) E0 (Returnstate stack (match ov with Some v => v | None => Vundef end) m' bc')
  | vexec_Bcall sig fp args res pc' fd bc':
      find_function_v fp = Some fd ->
      funsig fd = sig ->
      final_step_v (Bcall sig fp args res pc') E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd args m bc')
  | vexec_Btailcall sig fp args stk m' bc' fd:
      find_function_v fp = Some fd ->
      funsig fd = sig ->
      sp = (Vptr stk Ptrofs.zero) ->
      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
      final_step_v (Btailcall sig fp args) E0 (Callstate stack fd args m' bc')
  | vexec_Bbuiltin ef args res pc' vargs t vres m' bc':
      eval_builtin_args ge (fun v => v) sp m args vargs ->
      external_call ef ge vargs m t vres m' ->
      final_step_v (Bbuiltin ef args res pc') t (State stack f sp pc' (regmap_setres res vres rs) m' bc')
  | vexec_Bjumptable arg tbl n pc':
      arg = Vint n ->
      list_nth_z tbl (Int.unsigned n) = Some pc' ->
      final_step_v (Bjumptable arg tbl) E0 (State stack f sp pc' rs m bc)
.

End ValuesSemantic.

Lemma find_function_iff_v (fp : reg + qualident) (rs : regset):
  exists fp_v,
    map_sum_left_opt (fun r => Some rs#r) fp = Some fp_v /\
  forall ge,
    find_function ge fp rs = find_function_v ge fp_v.
Proof.
  destruct fp; repeat esplit.
Qed.

Lemma final_step_iff_v f sp rs m bc (fin : final):
  exists fin_v,
    map_final_opt (fun r => Some rs#r) fin = Some fin_v /\
  forall ge (stk : list stackframe) (t : trace) (s : state),
    final_step ge stk f sp rs m bc fin t s <-> final_step_v ge stk f sp rs m bc fin_v t s.
Proof.
  Local Ltac slv :=
    do 2 esplit; [reflexivity|split; inversion 1; econstructor; eauto].
  destruct fin; simpl.
  3,4: ecase find_function_iff_v as (? & -> & ?);
       erewrite map_opt_tot by reflexivity.
  all: try solve [slv; congruence].
  - (* Breturn *)
    destruct res; slv.
  - (* Bbuiltin *)
    erewrite map_opt_tot by (intros ? _; erewrite map_builtin_arg_opt_tot; reflexivity).
    slv; rewrite <- eval_builtin_args_v in *; auto.
Qed.


Definition eval_builtin_sval ctx : builtin_arg sval -> option (builtin_arg val) :=
  map_builtin_arg_opt (eval_sval ctx).

Definition eval_list_builtin_sval ctx : list (builtin_arg sval) -> option (list (builtin_arg val)) :=
  map_opt (eval_builtin_sval ctx).

Definition eval_final_sval ctx : sfval -> option (finalA val) :=
  map_final_opt (eval_sval ctx).

We encapsulate the context of execution of a block in order to specify it with the associated function
Record iblock_function_context := Bfctx {
  cf: function;
  cc:> iblock_common_context
}.

Preservation properties under a simu_proof_context


Record simu_proof_context := 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;
  srs1: regset;
  sm1: mem;
  sbc: block_classification;
}.

Definition bcctx1 (ctx: simu_proof_context) := Bcctx ctx.(sge1) ctx.(ssp) ctx.(srs0) ctx.(srs1) ctx.(sm1) ctx.(sbc).
Definition bcctx2 (ctx: simu_proof_context) := Bcctx ctx.(sge2) ctx.(ssp) ctx.(srs0) ctx.(srs1) ctx.(sm1) ctx.(sbc).

Definition okpred :=
  {p : iblock_common_context -> Prop | forall pctx : simu_proof_context, p (bcctx1 pctx) <-> p (bcctx2 pctx)}.

Lemma okpred_preserved (p : okpred) (pctx : simu_proof_context):
  `p (bcctx1 pctx) <-> `p (bcctx2 pctx).
Proof.
  apply (proj2_sig p).
Qed.

Program Definition okConst (P : Prop) : okpred := fun _ => P.
Next Obligation.
reflexivity. Qed.

Section SymbValPreserved.

Hypothesis ctx: simu_proof_context.
Local Hint Resolve sge_match: core.

Lemma eval_sval_preserved_comb:
  (forall sv, eval_sval (bcctx1 ctx) sv = eval_sval (bcctx2 ctx) sv) /\
  (forall lsv, eval_list_sval (bcctx1 ctx) lsv = eval_list_sval (bcctx2 ctx) lsv) /\
  (forall sm, eval_smem (bcctx1 ctx) sm = eval_smem (bcctx2 ctx) sm) /\
  (forall ok, eval_okclauseb (bcctx1 ctx) ok = eval_okclauseb (bcctx2 ctx) ok).
Proof.
  apply sval_mut_comb;
    simpl in *; auto; unfold if_Some, ex_Some; simpl;
    repeat first [intros ->|intro];
    try solve [ repeat (
      try erewrite ?eval_addressing_preserved, ?eval_operation_preserved,
                   ?adp_addr_match_preserved, ?adp_op_promotable_preserved
                by eauto;
      first [ reflexivity | apply rew_proj_sumbool_dec
            | autodestruct; intro ] )].
Qed.

Lemma eval_sval_preserved sv:
  eval_sval (bcctx1 ctx) sv = eval_sval (bcctx2 ctx) sv.
Proof.
apply eval_sval_preserved_comb. Qed.

Lemma list_sval_eval_preserved lsv:
  eval_list_sval (bcctx1 ctx) lsv = eval_list_sval (bcctx2 ctx) lsv.
Proof.
apply eval_sval_preserved_comb. Qed.

Lemma smem_eval_preserved sm:
  eval_smem (bcctx1 ctx) sm = eval_smem (bcctx2 ctx) sm.
Proof.
apply eval_sval_preserved_comb. Qed.

Lemma eval_okclauseb_preserved ok:
  eval_okclauseb (bcctx1 ctx) ok = eval_okclauseb (bcctx2 ctx) ok.
Proof.
apply eval_sval_preserved_comb. Qed.

Lemma eval_okclause_preserved ok:
  eval_okclause (bcctx1 ctx) ok <-> eval_okclause (bcctx2 ctx) ok.
Proof.
  rewrite <-!eval_okclauseb_iff, eval_okclauseb_preserved.
  reflexivity.
Qed.

Lemma optsv_simu_preserved sv0 sv1:
  optsv_simu (bcctx1 ctx) sv0 sv1 <-> optsv_simu (bcctx2 ctx) sv0 sv1.
Proof.
  split; inversion 1; constructor; revert SIMU;
  rewrite !eval_sval_preserved; auto.
Qed.

Lemma eval_final_sval_preserved (sfv : sfval):
  eval_final_sval (bcctx1 ctx) sfv = eval_final_sval (bcctx2 ctx) sfv.
Proof.
  apply (map_opt_inst_ext map_final_opt_inst), eval_sval_preserved.
Qed.

Lemma eval_scondition_preserved cond lsv:
  eval_scondition (bcctx1 ctx) cond lsv = eval_scondition (bcctx2 ctx) cond lsv.
Proof.
  unfold eval_scondition.
  rewrite list_sval_eval_preserved. destruct eval_list_sval; auto.
Qed.

Lemma match_sreg_preserved sreg rs:
  match_sreg (bcctx1 ctx) sreg rs <-> match_sreg (bcctx2 ctx) sreg rs.
Proof.
  unfold match_sreg; setoid_rewrite eval_sval_preserved; reflexivity.
Qed.
Local Hint Resolve match_sreg_preserved: core.

Lemma match_si_preserved si rs:
  match_si (bcctx1 ctx) si rs <-> match_si (bcctx2 ctx) si rs.
Proof.
  unfold match_si, si_ok.
  setoid_rewrite eval_sval_preserved.
  rewrite match_sreg_preserved.
  reflexivity.
Qed.
Local Hint Resolve match_si_preserved: core.

Lemma match_invs_preserved csix rs:
  match_invs (bcctx1 ctx) csix rs <-> match_invs (bcctx2 ctx) csix rs.
Proof.
  unfold match_invs, match_meminv.
  rewrite !match_si_preserved, smem_eval_preserved.
  reflexivity.
Qed.

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.

End SymbValPreserved.

Syntax and Semantics of symbolic internal states


sis_hyp and sis_pre are preconditions on the initial context with the following meaning: - sis_hyp is a condition on the validity of the symbolic execution. There is no relation between the SE and the BTL semantics if this predicate is false. - sis_pre is used to defines sis_ok which is true if and only if there is an execution of the BTL iblock (that is, if the execution of the iblock does not fail).
Record sistate := {
  sis_hyp : okpred;
  sis_pre : okpred;
  sis_sreg :> reg -> option sval;
  sis_smem : smem;
}.

OK property for internal states: predicate on which there exists an execution of sis.
Record sis_ok ctx (sis: sistate): Prop := {
  OK_PRE : `sis.(sis_pre) ctx;
  OK_SMEM : eval_smem ctx sis.(sis_smem) <> None;
  OK_SREG : sreg_ok ctx sis
}.


Record sistate_eq ctx (si0 si1 : sistate) : Prop := {
  EQ_SIS_HYP : `si0.(sis_hyp) ctx <-> `si1.(sis_hyp) ctx;
  EQ_SIS_OK : sis_ok ctx si0 <-> sis_ok ctx si1;
  EQ_SIS_SREG: sreg_eq ctx si0.(sis_sreg) si1.(sis_sreg);
  EQ_SIS_SMEM: smem_equiv ctx (si0.(sis_smem)) (si1.(sis_smem))
}.

Global Instance sistate_Equivalence {ctx : iblock_common_context} : Equivalence (sistate_eq ctx).
Proof.
  constructor.
  - intros ?; constructor; reflexivity.
  - intros ? ? []; constructor; symmetry; auto.
  - intros ? ? ? [] []; constructor; etransitivity; eauto.
Qed.

Lemma intro_sistate_eq_eq_pre ctx (si0 si1 : sistate)
  (EQ_SIS_HYP : `si0.(sis_hyp) ctx <-> `si1.(sis_hyp) ctx)
  (EQ_SIS_PRE: `si0.(sis_pre) ctx <-> `si1.(sis_pre) ctx)
  (EQ_SIS_SREG: sreg_eq ctx si0.(sis_sreg) si1.(sis_sreg))
  (EQ_SIS_SMEM: smem_equiv ctx (si0.(sis_smem)) (si1.(sis_smem))):
  sistate_eq ctx si0 si1.
Proof.
  constructor; try assumption.
  split; intros [ ]; constructor; try solve [tauto | congruence];
  eapply sreg_ok_morph; eauto; symmetry; auto.
Qed.

Lemma sis_ok_morph [ctx si0 si1]
  (E : sistate_eq ctx si0 si1):
  sis_ok ctx si0 <-> sis_ok ctx si1.
Proof.
  apply E.
Qed.

Lemma sis_ok_preserved ctx sis:
  sis_ok (bcctx1 ctx) sis <-> sis_ok (bcctx2 ctx) sis.
Proof.
  split; intros H; inv H; econstructor;
  solve [ apply okpred_preserved; assumption
        | revert OK_SMEM0; rewrite smem_eval_preserved; auto
        | revert OK_SREG0; unfold sreg_ok;
          setoid_rewrite eval_sval_preserved; auto].
Qed.

Predicate on which (rs, m) is a possible final state after evaluating ss on ((crs0 ctx), (cm1 ctx))
Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop :=
  `sis.(sis_pre) ctx
  /\ eval_smem ctx sis.(sis_smem) = Some m
  /\ match_sreg ctx sis rs
.

Lemma sem_sistate_preserved ctx sis rs m:
  sem_sistate (bcctx1 ctx) sis rs m <-> sem_sistate (bcctx2 ctx) sis rs m.
Proof.
  unfold sem_sistate.
  rewrite okpred_preserved, smem_eval_preserved, match_sreg_preserved.
  reflexivity.
Qed.

Lemma sem_sis_ok ctx sis rs m:
  sem_sistate ctx sis rs m -> sis_ok ctx sis.
Proof.
  intros (PRE&MEM&REG).
  econstructor; solve [eauto | congruence].
Qed.

Lemma sem_sistate_determ_mem ctx sis rs1 m1 rs2 m2:
  sem_sistate ctx sis rs1 m1 ->
  sem_sistate ctx sis rs2 m2 ->
  m1 = m2.
Proof.
  intros H1 H2.
  destruct H1 as (_&MEM1&REG1), H2 as (_&MEM2&REG2); simpl in *.
  congruence.
Qed.


Record sis_rel (sis0 sis1 : sistate) : Prop := {
  SRL_HY: forall ctx, `sis1.(sis_hyp) ctx -> `sis0.(sis_hyp) ctx;
  SRL_OK: forall ctx, sis_ok ctx sis1 -> sis_ok ctx sis0;
  SRL_HY_SIS: forall ctx, `sis0.(sis_hyp) ctx -> ~sis_ok ctx sis0 -> `sis1.(sis_hyp) ctx;
}.

Global Instance sis_rel_PreOrder: PreOrder sis_rel.
Proof.
  constructor.
  - constructor; tauto.
  - intros ? ? ? [?] [?]; constructor; eauto.
    intro ctx.
    repeat match goal with H: forall (_ : iblock_common_context), _ |- _ => specialize (H ctx) end.
    tauto.
Qed.

Section SIS_OPERATIONS.

Local Ltac sis_rel_tac :=
  constructor; simpl; [tauto | inversion 1; try tauto; constructor; simpl in *; tauto | tauto].

Definition sis_empty: sistate :=
  {|
    sis_hyp := okConst True;
    sis_pre := okConst True;
    sis_sreg := fun r => Some (fSinput false r);
    sis_smem := fSinit
  |}.

Lemma sis_ok_empty ctx:
  sis_ok ctx sis_empty.
Proof.
  unfold sis_empty; constructor; simpl; try congruence; auto.
  inversion 1; simpl; congruence.
Qed.

Lemma sem_sistate_empty ctx:
  sem_sistate ctx sis_empty (crs0 ctx) (cm1 ctx).
Proof.
  repeat split.
  inversion 1; reflexivity.
Qed.

Lemma empty_total_sreg:
  total_sreg sis_empty.
Proof.
  discriminate 1.
Qed.


Program Definition add_hyp (hy : okpred) (sis : sistate) : sistate :=
  {|
    sis_hyp := fun ctx => sis.(sis_hyp) ctx /\ (sis_ok ctx sis -> hy ctx);
    sis_pre := sis.(sis_pre);
    sis_sreg := sis.(sis_sreg);
    sis_smem := sis.(sis_smem);
  |}.
Next Obligation.
  rewrite !okpred_preserved, sis_ok_preserved. reflexivity.
Qed.

Lemma ok_add_hyp ctx hy sis:
  sis_ok ctx (add_hyp hy sis) <-> sis_ok ctx sis.
Proof.
  split; intros []; constructor; simpl in *; assumption.
Qed.

Lemma sem_sistate_add_hyp ctx hy sis rs m:
  sem_sistate ctx (add_hyp hy sis) rs m <->
  sem_sistate ctx sis rs m.
Proof.
  unfold sem_sistate; simpl; tauto.
Qed.

Lemma add_hyp_rel sis hy:
  sis_rel sis (add_hyp hy sis).
Proof.
sis_rel_tac. Qed.


Definition abort_sis := add_hyp (okConst False).

Lemma abort_sis_not_hyp ctx sis
  (SOK : sis_ok ctx sis):
  ~proj1_sig (abort_sis sis).(sis_hyp) ctx.
Proof.
  intro HYP; apply HYP; auto.
Qed.

Lemma abort_sis_rel sis:
  sis_rel sis (abort_sis sis).
Proof.
apply add_hyp_rel. Qed.


Program Definition set_sreg (r:reg) (sv:sval) (sis:sistate): sistate :=
  {|
    sis_hyp := sis.(sis_hyp);
    sis_pre := fun ctx => sis_ok ctx sis;
    sis_sreg := fset Reg.eq r (Some sv) sis.(sis_sreg);
    sis_smem := sis.(sis_smem)
  |}.
Next Obligation.
  apply sis_ok_preserved.
Qed.

Lemma set_sreg_correct ctx dst sv sis (rs rs': regset) m
  (SIS : sem_sistate ctx sis rs m)
  (NEW : eval_sval ctx sv = Some rs' # dst)
  (OLD : forall r, r <> dst -> rs'#r = rs#r):
  sem_sistate ctx (set_sreg dst sv sis) rs' m.
Proof.
  apply sem_sis_ok in SIS as OK.
  case SIS as (PRE & MEM & REG); unfold sem_sistate; simpl.
  intuition.
  intros r' sv'; unfold fset; autodestruct; intros _; try_simplify_someHyps.
  intros; rewrite OLD; eauto.
Qed.

Lemma ok_set_sreg ctx r sv sis:
  sis_ok ctx (set_sreg r sv sis) <-> sis_ok ctx sis /\ alive (eval_sval ctx sv).
Proof.
  unfold set_sreg; split.
  - intros [OK SMEM SREG]; simpl in *; split; auto.
    eapply SREG, fset_gs.
  - intros (OK & SVAL); pose proof (OK' := OK); case OK' as [PRE SMEM SREG].
    constructor; simpl; auto.
    intros r' sv'; unfold fset; autodestruct; try_simplify_someHyps.
Qed.

Lemma set_sreg_rel sis r sv:
  sis_rel sis (set_sreg r sv sis).
Proof.
sis_rel_tac. Qed.

Lemma set_sreg_morph ctx r sv0 sv1 sis0 sis1
  (SIS_EQ : sistate_eq ctx sis0 sis1)
  (SV_EQ : sval_equiv ctx sv0 sv1):
  sistate_eq ctx (set_sreg r sv0 sis0) (set_sreg r sv1 sis1).
Proof.
  constructor; try apply SIS_EQ.
  - erewrite !ok_set_sreg, SV_EQ, sis_ok_morph by eassumption.
    reflexivity.
  - intros r'; simpl; unfold fset.
    case Reg.eq as [|].
    + constructor; simpl; tauto.
    + apply SIS_EQ.
Qed.

Lemma set_sreg_total (sis : sistate) r sv
  (TOT : total_sreg sis):
  total_sreg (set_sreg r sv sis).
Proof.
  intro; unfold set_sreg, fset; simpl; autodestruct.
Qed.


Program Definition set_smem (sm:smem) (sis:sistate): sistate :=
  {|
    sis_hyp := sis.(sis_hyp);
    sis_pre := fun ctx => sis_ok ctx sis;
    sis_sreg := sis.(sis_sreg);
    sis_smem := sm
  |}.
Next Obligation.
  apply sis_ok_preserved.
Qed.

Lemma set_smem_correct ctx sm sis rs m m'
  (SIS : sem_sistate ctx sis rs m)
  (MEM : eval_smem ctx sm = Some m'):
  sem_sistate ctx (set_smem sm sis) rs m'.
Proof.
  apply sem_sis_ok in SIS as OK.
  case SIS as (_ & _ & REG).
  unfold sem_sistate; simpl; intuition.
Qed.

Lemma ok_set_smem ctx sm sis:
  sis_ok ctx (set_smem sm sis) <-> sis_ok ctx sis /\ alive (eval_smem ctx sm).
Proof.
  split; [intros SIS; split|intros (SIS & EMEM)]; pose proof (SIS' := SIS); destruct SIS';
  try assumption; try constructor; simpl in *; tauto.
Qed.

Lemma set_smem_rel sis sm:
  sis_rel sis (set_smem sm sis).
Proof.
sis_rel_tac. Qed.

Lemma set_smem_morph ctx sm0 sm1 sis0 sis1
  (SIS_EQ : sistate_eq ctx sis0 sis1)
  (SM_EQ : smem_equiv ctx sm0 sm1):
  sistate_eq ctx (set_smem sm0 sis0) (set_smem sm1 sis1).
Proof.
  constructor; try apply SIS_EQ.
  - rewrite !ok_set_smem, SM_EQ.
    apply sis_ok_morph in SIS_EQ as ->.
    reflexivity.
  - apply SM_EQ.
Qed.


Program Definition add_pre (p : okpred) (sis : sistate): sistate :=
  {|
    sis_hyp := sis.(sis_hyp);
    sis_pre := fun ctx => sis.(sis_pre) ctx /\ p ctx;
    sis_sreg := sis.(sis_sreg);
    sis_smem := sis.(sis_smem)
  |}.
Next Obligation.
  rewrite !okpred_preserved; reflexivity.
Qed.

Lemma ok_add_pre ctx p sis:
  sis_ok ctx (add_pre p sis) <-> sis_ok ctx sis /\ `p ctx.
Proof.
  split; [intros []|intros [[] ?]]; simpl in *; intuition; constructor; simpl; auto.
Qed.

Lemma sem_sistate_add_pre ctx p sis rs m:
  sem_sistate ctx (add_pre p sis) rs m <->
  sem_sistate ctx sis rs m /\ `p ctx.
Proof.
  unfold sem_sistate; simpl; tauto.
Qed.

Lemma add_pre_rel sis p:
  sis_rel sis (add_pre p sis).
Proof.
sis_rel_tac. Qed.

Lemma add_pre_morph ctx (p0 p1 : okpred) (sis0 sis1 : sistate)
  (PRE_EQ : `p0 ctx <-> `p1 ctx)
  (SIS_EQ : sistate_eq ctx sis0 sis1):
  sistate_eq ctx (add_pre p0 sis0) (add_pre p1 sis1).
Proof.
  constructor; try apply SIS_EQ.
  rewrite !ok_add_pre, PRE_EQ.
  apply EQ_SIS_OK in SIS_EQ as ->.
  tauto.
Qed.


Definition error_sis (sis : sistate) : sistate :=
  {|
    sis_hyp := sis.(sis_hyp);
    sis_pre := okConst False;
    sis_sreg := sis.(sis_sreg);
    sis_smem := sis.(sis_smem);
  |}.

Lemma error_sis_not_ok ctx sis:
  ~sis_ok ctx (error_sis sis).
Proof.
  intros [PRE _ _]. exact PRE.
Qed.

Lemma error_sis_rel sis:
  sis_rel sis (error_sis sis).
Proof.
sis_rel_tac. Qed.

End SIS_OPERATIONS.


Symbolic final states


outcome of a symbolic execution path

Record poutcome (istate fin : Type) := sout {
   _sis: istate;
   _sfv: fin;
}.
Arguments sout {_ _}.
Arguments _sis [_ _].
Arguments _sfv [_ _].

Definition soutcome := poutcome sistate sfval.

symbolic state

Definition sstate := {f : iblock_common_context -> soutcome
                     | forall pctx : simu_proof_context, f (bcctx1 pctx) = f (bcctx2 pctx)}.

Definition get_soutcome (ctx : iblock_common_context) (s : sstate) : soutcome :=
  let (f, _) := s in
  f ctx.

Lemma get_soutcome_preserved ctx s:
  get_soutcome (bcctx1 ctx) s = get_soutcome (bcctx2 ctx) s.
Proof.
  case s as [? P]. apply P.
Qed.

Definition abort_soutcome (sis : sistate) : soutcome := sout (abort_sis sis) (Breturn None).
Program Definition abort_sstate (sis : sistate) : sstate := fun _ => abort_soutcome sis.
Definition error_soutcome (sis : sistate) : soutcome := sout (error_sis sis) (Breturn None).
Program Definition error_sstate (sis : sistate) : sstate := fun _ => error_soutcome sis.


Function to transform a list of reg into a list of symbolic values (i.e. the list_sval type). It may fail if the register does not evaluate correctly.
Fixpoint lmap_sv {A} (sreg: A -> option sval) (l: list A): option list_sval :=
  match l with
  | nil => Some (fSnil)
  | r::l' =>
     SOME sv <- sreg r IN
     SOME lsv <- lmap_sv sreg l' IN
     Some (fScons sv lsv)
  end.

Lemma lmap_sv_eq {A} sreg (l : list A):
  lmap_sv sreg l = SOME lsv <- map_opt sreg l IN Some (lsv_of_list lsv).
Proof.
  induction l; simpl. reflexivity.
  rewrite IHl. repeat autodestruct.
Qed.

Lemma eval_lmap_sv ctx sreg l rs lsv
  (MATCH : match_sreg ctx sreg rs)
  (LMAP : lmap_sv sreg l = Some lsv):
  eval_list_sval ctx lsv = Some (rs ## l).
Proof.
  revert lsv LMAP; induction l as [|r l]; simpl; intro.
  - try_simplify_someHyps.
  - repeat (autodestruct; simpl; intro).
    try_simplify_someHyps; simpl; auto.
    intros; erewrite MATCH, IHl; eauto.
Qed.


Symbolic execution of BTL blocks

Section SEXEC.

Symbolic execution of final step


Definition sexec_final_sfv (i: final) (sreg: reg -> option sval): option sfval :=
  map_final_opt sreg i.

Definition sfv_equiv (ctx : iblock_function_context) sfv rs m fin : Prop :=
  exists fin_v,
    eval_final_sval ctx sfv = Some fin_v /\
  forall stk t sf,
    final_step_v (cge ctx) stk (cf ctx) (csp ctx) rs m (cbc ctx) fin_v t sf <->
    final_step (cge ctx) stk (cf ctx) (csp ctx) rs m (cbc ctx) fin t sf.

Lemma sexec_final_sfv_correct (ctx: iblock_function_context) i sis rs m sfv
  (SEM : sem_sistate ctx sis rs m)
  (SE : sexec_final_sfv i sis = Some sfv):
  sfv_equiv ctx sfv rs m i.
Proof.
  ecase final_step_iff_v as (fin_v & MAP0 & FIN_IFF).
  exists fin_v. split. 2:symmetry; apply FIN_IFF.
  unfold eval_final_sval.
  rewrite <- MAP0; clear MAP0.
  pose proof (REW := SE); eapply (map_opt_inst_bind1 map_final_opt_inst) in REW as ->.
  apply (map_opt_inst_alive_annot map_final_opt_inst) in SE as [i_a AN].
  do 2 (pose proof (REW := AN); eapply (map_opt_inst_bind1 map_final_opt_inst) in REW as ->).
  apply (map_opt_inst_ext map_final_opt_inst).
  intros [? SIS]; simpl.
  apply elim_alive in SIS as (sv & SIS); rewrite SIS.
  apply SEM in SIS; auto.
Qed.

Symbolic execution of basic instructions


Definition istep_correct ctx (sem0 : regset -> mem -> Prop) (sis1 : sistate) : Prop :=
  (forall rs1 m1, sem0 rs1 m1 -> sem_sistate ctx sis1 rs1 m1) /\
  (sis_ok ctx sis1 -> exists rs1 m1, sem0 rs1 m1).

Let btl_istep (ctx : iblock_common_context) :=
  iblock_istep AnnotUndef (cge ctx) (csp ctx) (cbc ctx).

Local Hint Resolve AssertTrue : core.


Program Definition adp_op_okpred (op : operation) (sargs : list_sval) (iinfo : inst_info) : okpred :=
  fun ctx =>
    ex_Some (eval_list_sval ctx sargs) (fun args =>
    adp_op (cge ctx) (csp ctx) (cm1 ctx) op args iinfo).
Next Obligation.
  rewrite list_sval_eval_preserved.
  setoid_rewrite ex_Some_iff.
  setoid_rewrite adp_op_preserved at 1. reflexivity.
  apply (sge_match pctx).
Qed.

Lemma adp_op_okpred_correct ctx sis rs m op args sargs iinfo
  (SIS : sem_sistate ctx sis rs m)
  (ARGS : eval_list_sval ctx sargs = Some rs##args):
  proj1_sig (adp_op_okpred op sargs iinfo) ctx <->
  adp_op (cge ctx) (csp ctx) m op rs##args iinfo.
Proof.
  case SIS as (_ & MEM & _); simpl.
  rewrite ARGS; simpl.
  apply adp_op_valid_pointer_eq; eauto.
Qed.

Definition sexec_op op args dst iinfo (sis: sistate): option sistate :=
   SOME args <- lmap_sv sis args IN
   Some (set_sreg dst (fSop op args) (add_pre (adp_op_okpred op args iinfo) sis)).

Lemma sexec_op_correct ctx op args dst iinfo sis rs m sis1
  (SIS : sem_sistate ctx sis rs m):
  sexec_op op args dst iinfo sis = Some sis1 ->
  istep_correct ctx
    (fun rs1 m1 => btl_istep ctx rs m (Bop op args dst iinfo) rs1 m1 None)
    sis1.
Proof.
  pose proof (SIS' := SIS); case SIS' as (_ & EMEM & EREG).
  unfold sexec_op.
  destruct lmap_sv as [sargs|] eqn:ARGS; [injection 1 as <-|discriminate 1].
  eapply eval_lmap_sv in ARGS; eauto.
  set (sis1 := add_pre _ sis).
  set (sis2 := set_sreg _ _ sis1).
  assert (ESV : eval_sval ctx (fSop op sargs) = eval_operation (cge ctx) (csp ctx) op rs##args m). {
    simpl; rewrite ARGS.
    apply op_valid_pointer_eq; eauto.
  }
  split.
  - inversion 1; inv ADP.
    assert (sem_sistate ctx sis1 rs m1). {
      apply sem_sistate_add_pre.
      rewrite adp_op_okpred_correct; eauto.
    }
    eapply set_sreg_correct; eauto.
    + erewrite PMap.gss, ESV; auto.
    + intro. apply PMap.gso.
  - unfold sis2, sis1.
    rewrite ok_set_sreg, ok_add_pre, adp_op_okpred_correct, ESV; eauto.
    intros ((_ & ADP) & OP).
    apply elim_alive in OP as (res & OP).
    do 3 econstructor; eauto.
Qed.

Lemma sexec_op_rel op args dst iinfo sis sis1:
  sexec_op op args dst iinfo sis = Some sis1 ->
  sis_rel sis sis1.
Proof.
  unfold sexec_op; repeat autodestruct; try_simplify_someHyps; intros.
  rewrite <- set_sreg_rel, <- add_pre_rel.
  reflexivity.
Qed.


Definition sexec_load trap chunk addr args dst iinfo (sis: sistate): option sistate :=
   SOME args <- lmap_sv sis args IN
   Some (set_sreg dst (root_apply (Rload trap chunk addr iinfo.(addr_aval)) args sis.(sis_smem)) sis).

Lemma eval_mayundef_opt_iff ctx okc U sv v
  (OK : if_Some okc (eval_okclause ctx) <-> U):
  eval_sval ctx (fSmayUndef_opt okc sv) = Some v <->
  ex_Some (eval_sval ctx sv) (fun v0 => may_undef_prop U v0 AnnotUndef v).
Proof.
  destruct okc as [okc|]; simpl in *;
    (destruct eval_sval; simpl;
     [ etransitivity; [split; [injection 1 as E; exact E | intros <-; reflexivity] |]
     | split; first [tauto | congruence]]).
  - case (eval_okclauseb_spec ctx okc) as [E|E]; rewrite OK in E.
    + split; [intros ->; constructor; auto | inversion 1; tauto].
    + split.
      * intros <-; constructor; auto.
      * inversion 1; tauto.
  - assert U by tauto.
    split; [intros ->; constructor; auto | inversion 1; tauto].
Qed.

Lemma root_apply_load_correct ctx rs m trap chunk addr args iinfo sargs sm v
  (ARGS : eval_list_sval ctx sargs = Some rs##args)
  (MEM : eval_smem ctx sm = Some m):
  let U := udp_load (cge ctx) (cbc ctx) (csp ctx) addr rs##args iinfo in
  eval_sval ctx (root_apply (Rload trap chunk addr iinfo.(addr_aval)) sargs sm) = Some v <->
  exists v0,
    has_loaded (cge ctx) (csp ctx) rs m chunk addr args v0 trap /\
    may_undef_prop U v0 AnnotUndef v.
Proof.
  intro; simpl.
  rewrite eval_mayundef_opt_iff with (U := U); unfold U;
  cycle 1.
  - unfold udp_load.
    destruct addr_aval; simpl. 2:reflexivity.
    rewrite ARGS. reflexivity.
  - simpl.
    rewrite ARGS, MEM.
    split.
    + case trap; unfold ex_Some; repeat (autodestruct; simpl; intro; try tauto);
      (intro UDP; eexists; split; [|exact UDP]);
      solve [ eapply has_loaded_normal; eauto
            | eapply has_loaded_default; eauto; intros; congruence ].
    + intros (? & HLOAD & UDP).
      inv HLOAD.
      * rewrite EVAL, LOAD. autodestruct.
      * do 2 autodestruct. rewrite LOAD; congruence.
Qed.

Local Opaque root_apply.

Lemma sexec_load_correct ctx trap chk addr args dst iinfo sis rs m sis1
  (SIS : sem_sistate ctx sis rs m):
  sexec_load trap chk addr args dst iinfo sis = Some sis1 ->
  istep_correct ctx
    (fun rs1 m1 => btl_istep ctx rs m (Bload trap chk addr args dst iinfo) rs1 m1 None)
    sis1.
Proof.
  pose proof (SIS' := SIS); case SIS' as (_ & EMEM & EREG).
  unfold sexec_load.
  destruct lmap_sv as [sargs|] eqn:ARGS; [injection 1 as <-|discriminate 1].
  eapply eval_lmap_sv in ARGS; eauto.
  split.
  - inversion 1; subst.
    eapply set_sreg_correct; eauto.
    + rewrite PMap.gss.
      rewrite root_apply_load_correct; eauto.
    + intro; apply PMap.gso.
  - rewrite ok_set_sreg.
    intros (_ & LOAD).
    apply elim_alive in LOAD as (res & LOAD).
    eapply root_apply_load_correct in LOAD as (? & ? & ?); eauto.
    do 3 econstructor; eauto.
Qed.

Local Transparent root_apply.

Lemma sexec_load_rel trap chk addr args dst iinfo sis sis1:
  sexec_load trap chk addr args dst iinfo sis = Some sis1 ->
  sis_rel sis sis1.
Proof.
  unfold sexec_load; repeat autodestruct; try_simplify_someHyps; intros.
  apply set_sreg_rel.
Qed.


Definition sexec_store chunk addr args src iinfo (sis: sistate): option sistate :=
   SOME args <- lmap_sv sis args IN
   SOME src <- sis src IN
   Some (set_smem (fSstore sis.(sis_smem) chunk addr args (store_info_of_iinfo iinfo) src) sis).

Lemma sexec_store_correct ctx chk addr args src iinfo sis rs m sis1
  (SIS : sem_sistate ctx sis rs m):
  sexec_store chk addr args src iinfo sis = Some sis1 ->
  istep_correct ctx
    (fun rs1 m1 => btl_istep ctx rs m (Bstore chk addr args src iinfo) rs1 m1 None)
    sis1.
Proof.
  pose proof (SIS' := SIS); case SIS' as (_ & EMEM & EREG).
  unfold sexec_store.
  destruct lmap_sv as [sargs|] eqn:ARGS; [|discriminate 1].
  destruct (sis src) as [ssrc |] eqn:SRC; [injection 1 as <-|discriminate 1].
  eapply eval_lmap_sv in ARGS; eauto.
  eapply EREG in SRC.
  set (sm := fSstore _ _ _ _ _ _).
  assert (ESV : forall m1,
      eval_smem ctx sm = Some m1 <->
      ex_Some (eval_addressing (cge ctx) (csp ctx) addr rs##args) (fun a =>
        adp_store (cge ctx) (cbc ctx) (csp ctx) addr rs##args iinfo /\
        Mem.storev chk m a rs#src = Some m1)). {
    intro; unfold sm, adp_store, adp_addr_match; simpl.
    rewrite ARGS, EMEM, SRC; autodestruct; simpl. 2:solve [intuition].
    case if_Some_dec; intuition.
  }
  setoid_rewrite ex_Some_iff in ESV.
  split.
  - inversion 1; inv ADP.
    eapply set_smem_correct; eauto.
    apply ESV; eauto.
  - rewrite ok_set_smem.
    intros (_ & STORE).
    apply elim_alive in STORE as (m1 & STORE).
    apply ESV in STORE as (? & ? & ? & ?).
    do 3 econstructor; eauto.
Qed.

Lemma sexec_store_rel chk addr args src iinfo sis sis1:
  sexec_store chk addr args src iinfo sis = Some sis1 ->
  sis_rel sis sis1.
Proof.
  unfold sexec_store; repeat autodestruct; try_simplify_someHyps; intros.
  apply set_smem_rel.
Qed.


Program Definition adp_cond_okpred (cond : condition) (sargs : list_sval) (iinfo : inst_info) : okpred :=
  fun ctx =>
    ex_Some (eval_list_sval ctx sargs) (fun args =>
    adp_cond (cm1 ctx) cond args iinfo).
Next Obligation.
  rewrite list_sval_eval_preserved. reflexivity.
Qed.

Lemma adp_cond_okpred_correct ctx sis rs m cond sargs vargs iinfo
  (SIS: sem_sistate ctx sis rs m)
  (ARGS: eval_list_sval ctx sargs = Some vargs):
  proj1_sig (adp_cond_okpred cond sargs iinfo) ctx <->
  adp_cond m cond vargs iinfo.
Proof.
  case SIS as (_ & MEM & REG); simpl.
  rewrite ARGS; simpl.
  apply adp_cond_valid_pointer_eq; eauto.
Qed.

Lemma eval_scondition_eq ctx cond vargs sis rs m lsv
  (SIS : sem_sistate ctx sis rs m)
  (ARGS: eval_list_sval ctx lsv = Some vargs)
  :eval_scondition ctx cond lsv = eval_condition cond vargs m.
Proof.
  destruct SIS as (_&MEM&_); unfold eval_scondition; simpl.
  rewrite ARGS.
  eapply cond_valid_pointer_eq; eauto.
Qed.


Notation "'STBIND' X 'IN' S <- A 'IN' B" :=
  (match A with Some X => B | None => abort_sstate S end)
  (at level 200, X name, S at level 100, A at level 100, B at level 200)
  : option_monad_scope.

Program Definition sstate_final (sis : sistate) (sfv : sfval) : sstate :=
  fun _ => sout sis sfv.

Definition sstate_cond_f (cond : condition) (args : list_sval)
  (sis : sistate) (ifso : sstate) (ifnot : sstate) ctx : soutcome :=
  match eval_scondition ctx cond args with
  | Some b => if b then get_soutcome ctx ifso else get_soutcome ctx ifnot
  | None => error_soutcome sis
  end.

Program Definition sstate_cond cond args sis ifso ifnot : sstate :=
  Eval unfold sstate_cond_f in sstate_cond_f cond args sis ifso ifnot.
Next Obligation.
  unfold sstate_cond_f.
  rewrite !get_soutcome_preserved, eval_scondition_preserved.
  reflexivity.
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 ib (sis:sistate) (k: sistate -> sstate): sstate :=
  match ib with
  | BF fin _ =>
    STBIND sfv IN sis <- sexec_final_sfv fin sis IN
    sstate_final sis sfv
basic instructions
  | Bnop _ => k sis
  | Bop op args res iinfo =>
     STBIND sis' IN sis <- sexec_op op args res iinfo sis IN
     k sis'
  | Bload trap chunk addr args dst iinfo =>
     STBIND sis' IN sis <- sexec_load trap chunk addr args dst iinfo sis IN
     k sis'
  | Bstore chunk addr args src iinfo =>
     STBIND sis' IN sis <- sexec_store chunk addr args src iinfo sis IN
     k sis'
composed instructions
  | Bseq ib1 ib2 =>
      sexec_rec ib1 sis (fun sis2 => sexec_rec ib2 sis2 k)
  | Bcond cond args ifso ifnot iinfo =>
      STBIND args IN sis <- lmap_sv sis args IN
      let sis' := add_pre (adp_cond_okpred cond args iinfo) sis in
      let ifso := sexec_rec ifso sis' k in
      let ifnot := sexec_rec ifnot sis' k in
      sstate_cond cond args sis' ifso ifnot
  end
  .

Definition sexec ib sinit := sexec_rec ib sinit error_sstate.

Lemma sstate_cond_rel ctx cond sargs sis ifso ifnot sisf sfv
  (K : forall (b : bool), get_soutcome ctx (if b then ifso else ifnot) = sout sisf sfv ->
                           sis_rel sis sisf)
  (SE : get_soutcome ctx (sstate_cond cond sargs sis ifso ifnot) = sout sisf sfv):
  sis_rel sis sisf.
Proof.
  revert SE; simpl.
  case eval_scondition as [b|].
  - specialize (K b); destruct b; exact K.
  - injection 1 as <-. apply error_sis_rel.
Qed.

Lemma sexec_rec_rel ctx ib sis k sisf sfv
  (K : forall sis1, get_soutcome ctx (k sis1) = sout sisf sfv -> sis_rel sis1 sisf)
  (SE : get_soutcome ctx (sexec_rec ib sis k) = sout sisf sfv):
  sis_rel sis sisf.
Proof.
  revert sis k K SE; induction ib; do 3 intro; simpl;
  repeat autodestruct; try_simplify_someHyps; intros;
  try (injection SE as ?; subst; auto using abort_sis_rel).
  - reflexivity.
  - apply sexec_op_rel in EQ as ->; auto.
  - apply sexec_load_rel in EQ as ->; auto.
  - apply sexec_store_rel in EQ as ->; auto.
  - eapply IHib1. 2:exact SE.
    intros. eapply IHib2; eauto.
  - apply sstate_cond_rel in SE as <-.
    + apply add_pre_rel.
    + intros [|]; [apply IHib1|apply IHib2]; apply K.
Qed.

Lemma sexec_rel ctx ib sis sisf sfv:
  get_soutcome ctx (sexec ib sis) = sout sisf sfv ->
  sis_rel sis sisf.
Proof.
  apply sexec_rec_rel.
  injection 1 as <-. apply error_sis_rel.
Qed.

Lemma sexec_rec_total_sreg ctx ib (sis : sistate) k sisf sfv
  (K : forall (sis1 : sistate), total_sreg sis1 -> get_soutcome ctx (k sis1) = sout sisf sfv -> total_sreg sisf)
  (TOT : total_sreg sis)
  (SE : get_soutcome ctx (sexec_rec ib sis k) = sout sisf sfv):
  total_sreg sisf.
Proof.
  revert sis TOT k K SE; induction ib; do 4 intro;
  simpl; unfold sexec_op, sexec_load, sexec_store;
  repeat (autodestruct; intro);
  try solve [ injection 1 as <- <-; apply TOT
            | apply K; try apply set_sreg_total; apply TOT ].
  - apply IHib1; auto.
    do 2 intro; apply IHib2; auto.
  - simpl.
    case eval_scondition as [[|]|].
    + apply IHib1; auto.
    + apply IHib2; auto.
    + injection 1 as <- <-; apply TOT.
Qed.

Lemma sexec_total_sreg ctx ib (sis : sistate) sisf sfv
  (TOT : total_sreg sis)
  (SE : get_soutcome ctx (sexec ib sis) = sout sisf sfv):
  total_sreg sisf.
Proof.
  eapply sexec_rec_total_sreg; eauto.
  injection 2 as <- <-; assumption.
Qed.

Section SEXEC_CORRECT.
  Variables (ctx : iblock_function_context) (sisf : sistate) (sfv : sfval).

  Hypothesis HYPF : `sisf.(sis_hyp) ctx.

  Lemma sisf_not_abort sis
    (SOK : sis_ok ctx sis):
    ~get_soutcome ctx (abort_sstate sis) = sout sisf sfv.
  Proof.
    injection 1 as SISF. rewrite <- SISF in HYPF. apply HYPF; auto.
  Qed.

  Local Ltac abort_absurd :=
    solve [intros; exfalso; eapply sisf_not_abort; eauto using sem_sis_ok].

  Local Ltac autodestruct_STBIND :=
    autodestruct; try abort_absurd.

  Definition step_correct (sem : regset -> mem -> final -> Prop) : Prop :=
    (forall rsf mf fin, sem rsf mf fin -> sem_sistate ctx sisf rsf mf /\ sfv_equiv ctx sfv rsf mf fin) /\
    (sis_ok ctx sisf -> exists rsf mf fin, sem rsf mf fin).

  Lemma step_correct_intro_under (H : Prop) (sem : regset -> mem -> final -> Prop)
    (H0 : forall rsf mf fin, sem rsf mf fin -> H)
    (H1 : sis_ok ctx sisf -> H)
    (C : H -> step_correct sem):
    step_correct sem.
  Proof.
    split; intros; apply C; auto.
    eapply H0; eauto.
  Qed.

  Definition sexec_specP (sem : regset -> mem -> final -> Prop) sis rs m : Prop :=
    forall (SIS: sem_sistate ctx sis rs m),
    step_correct sem.

  Lemma step_correct_rew_sem sem0 sem1
    (H: forall rsf mf fin, sem1 rsf mf fin <-> sem0 rsf mf fin):
    step_correct sem0 ->
    step_correct sem1.
  Proof.
    unfold step_correct; setoid_rewrite H. auto.
  Qed.

  Lemma istep_correct_elim_exact sem0 sis1
    (E : istep_correct ctx sem0 sis1)
    (HY : `sis1.(sis_hyp) ctx)
    (OK : sis_ok ctx sis1) :
    exists rs1 m1, sem0 rs1 m1 /\ sem_sistate ctx sis1 rs1 m1.
  Proof.
    case E as (E0 & E1); auto.
    case (E1 OK) as (rs1 & m1 & ?).
    eauto.
  Qed.

  Lemma sexec_specP_istep istep sis1 k_sem
    (IE : istep_correct ctx istep sis1)
    (KS : sis_rel sis1 sisf)
    (KE : forall (rs1 : regset) (m1 : mem), sexec_specP (k_sem rs1 m1) sis1 rs1 m1):
    step_correct (fun (rsf : regset) (mf : mem) (fin : final) =>
      exists (rs1 : regset) (m1 : mem),
        istep rs1 m1 /\ k_sem rs1 m1 rsf mf fin).
  Proof.
    assert (HY: `sis1.(sis_hyp) ctx) by (apply KS; auto).
    assert (OK: sis_ok ctx sisf -> sis_ok ctx sis1) by (intro; apply KS; auto).
    split.
    + intros rsf mf fin (rs1 & m1 & ISTEP & KSTEP).
      apply IE in ISTEP as SIS1; auto.
      apply (KE _ _ SIS1); assumption.
    + intros SF.
      apply istep_correct_elim_exact in IE as (rs1 & m1 & ISTEP & SIS1); auto.
      case (KE rs1 m1) as (_ & (rsf & mf & fin & ?)); eauto.
      exists rsf, mf, fin, rs1, m1; tauto.
  Qed.

  Definition sem_cont (sem : regset -> mem -> option final -> Prop)
                      (k : regset -> mem -> regset -> mem -> final -> Prop)
                      (rsf : regset) (mf : mem) (fin : final) : Prop :=
    sem rsf mf (Some fin) \/ (exists rs m, sem rs m None /\ k rs m rsf mf fin).

  Lemma sem_cont_only_right (sem : regset -> mem -> option final -> Prop) k rs2 m2 fin
    (H : sem rs2 m2 (Some fin) -> False):
    sem_cont sem k rs2 m2 fin <-> (exists rs m, sem rs m None /\ k rs m rs2 m2 fin).
  Proof.
    unfold sem_cont; tauto.
  Qed.

  Lemma sem_cont_morph sem0 sem1 k rsf mf fin
    (H : forall rs m fin, sem0 rs m fin <-> sem1 rs m fin):
    sem_cont sem0 k rsf mf fin <-> sem_cont sem1 k rsf mf fin.
  Proof.
    unfold sem_cont; setoid_rewrite H; reflexivity.
  Qed.

  Lemma sem_cont_seq an ge sp bc rs m ib1 ib2 k_sem rsf mf fin:
    let istep := iblock_istep an ge sp bc in
    sem_cont (istep rs m (Bseq ib1 ib2)) k_sem rsf mf fin <->
    sem_cont (istep rs m ib1) (fun rs1 m1 => sem_cont (istep rs1 m1 ib2) k_sem) rsf mf fin.
  Proof.
    intro; unfold sem_cont.
    split.
    + intros [IB|(? & ? & IB & ?)]; inversion IB; subst;
      repeat (solve [left; auto] || right; repeat esplit; eauto).
    + intros [|(? & ? & ? & [|(? & ? & ? & ?)])];
      solve [(left + (right; repeat esplit; eauto)); econstructor; eauto].
  Qed.

  Theorem sexec_rec_correct ib:
    forall (k : sistate -> sstate) k_sem sis rs m
    (K : forall sis1 (GET : get_soutcome ctx (k sis1) = sout sisf sfv) rs1 m1,
                sexec_specP (k_sem rs1 m1) sis1 rs1 m1)
    (K_REL: forall sis1, get_soutcome ctx (k sis1) = sout sisf sfv -> sis_rel sis1 sisf)
    (GET : get_soutcome ctx (sexec_rec ib sis k) = sout sisf sfv),
    let m_sem := sem_cont (btl_istep ctx rs m ib) k_sem in
    sexec_specP m_sem sis rs m.
  Proof.
    induction ib; intros; unfold sexec_specP; intro SIS; revert GET; simpl.
 
    - (* BF *)
      autodestruct_STBIND.
      injection 2 as ?; subst sis s.
      apply (step_correct_rew_sem (fun rsf mf fin => fin = fi /\ rsf = rs /\ mf = m)). {
        split.
        - intros [IB|(? & ? & IB & _)]; inversion IB; tauto.
        - intros (? & ? & ?); subst. left; constructor.
      }
      unfold step_correct.
      split.
      + intros ? ? ? (? & ? & ?); subst.
        split; auto.
        eapply sexec_final_sfv_correct; eauto.
      + repeat esplit.

    - (* Bnop *)
      intro GET.
      apply (step_correct_rew_sem (k_sem rs m)). {
        split.
        - intros [IB|(? & ? & IB & ?)]; inversion IB; subst; tauto.
        - eright; repeat econstructor; assumption.
      }
      exact (K _ GET _ _ SIS).
    - (* Bop *)
      autodestruct_STBIND.
      intros OP GET.
      eapply sexec_op_correct in OP; eauto.
      eapply step_correct_rew_sem. { intros; apply sem_cont_only_right; inversion 1. }
      eapply sexec_specP_istep; eauto.
    - (* Bload *)
      autodestruct_STBIND.
      intros LOAD GET.
      eapply sexec_load_correct in LOAD; eauto.
      eapply step_correct_rew_sem. { intros; apply sem_cont_only_right; inversion 1. }
      eapply sexec_specP_istep; eauto.
    - (* Bstore *)
      autodestruct_STBIND.
      intros STORE GET.
      eapply sexec_store_correct in STORE; eauto.
      eapply step_correct_rew_sem. { intros; apply sem_cont_only_right; inversion 1. }
      eapply sexec_specP_istep; eauto.

    - (* Bseq *)
      intro GET.
      eapply IHib1 in GET as IH; cycle 1.
      { intros. eapply IHib2; eassumption. }
      { intros ? GET2. apply sexec_rec_rel in GET2; auto. }
      eapply step_correct_rew_sem. 2:apply IH; eassumption.
      intros; apply sem_cont_seq.

    - (* Bcond *)
      case lmap_sv as [sargs|] eqn:ARGS. 2:abort_absurd.
      set (sis1 := add_pre _ sis).
      intro GET.
      eapply eval_lmap_sv in ARGS. 2:apply SIS.
      apply sstate_cond_rel in GET as RL.
        2:{ intros [|]; apply sexec_rec_rel; apply K_REL. }
      simpl in GET.
      erewrite eval_scondition_eq in GET; eauto.

      apply (step_correct_intro_under
              (exists b, eval_condition cond rs##args m = Some b /\
                         adp_cond m cond rs##args iinfo)).
      { intros ? ? ? [IB|(? & ? & IB & ?)]; inversion IB; inv ADP; eauto. }
      { intro SOKF. destruct eval_condition as [b|].
        - eexists; split. reflexivity.
          eapply SRL_OK in RL as SOK2. 2:eauto.
          apply ok_add_pre in SOK2 as (_ & SOK2).
          eapply adp_cond_okpred_correct in SOK2; eauto.
        - exfalso.
          injection GET as <-.
          apply error_sis_not_ok in SOKF as []. }

      intros (b & EVAL & ADP). rewrite EVAL in GET.
      assert (SIS1 : sem_sistate ctx sis1 rs m). {
        apply sem_sistate_add_pre; split; auto.
        eapply adp_cond_okpred_correct; eauto.
      }
      eapply (step_correct_rew_sem _). {
        intros.
        eapply sem_cont_morph
          with (sem1 := btl_istep ctx rs m (if b then ib1 else ib2)).
        intros; split.
        - inversion 1; subst.
          assert (b0 = b) by congruence; subst.
          assumption.
        - econstructor; eauto.
      }
      destruct b; [eapply IHib1 | eapply IHib2]; eauto.
  Qed.
  
  Corollary sexec_correct0 ib sis rs m
    (GET : get_soutcome ctx (sexec ib sis) = sout sisf sfv):
    let m_sem := fun rs1 m1 fin =>
      btl_istep ctx rs m ib rs1 m1 (Some fin) in
    sexec_specP m_sem sis rs m.
  Proof.
    eapply sexec_rec_correct with (k_sem := fun _ _ _ _ _ => False) in GET.
      2,3:unfold sexec_specP, step_correct; injection 1 as <- <-.
    - intros m_sem SIS.
      eapply step_correct_rew_sem. 2:apply (GET SIS).
      intros; unfold m_sem, sem_cont.
      intuition. case H0 as (_ & _ & _ & []).
    - split.
      + tauto.
      + intros [[]].
    - apply error_sis_rel.
  Qed.

End SEXEC_CORRECT.

NB: each concrete execution can be executed on the symbolic state (produced from sexec) (sexec is a correct over-approximation)
Theorem sexec_correct (ctx: iblock_function_context) sinit ri mi ib rf mf fin sisf sfv
  (SE : get_soutcome ctx (sexec ib sinit) = sout sisf sfv)
  (HYP : `sisf.(sis_hyp) ctx)
  (ISTEP : btl_istep ctx ri mi ib rf mf (Some fin))
  (SIS : sem_sistate ctx sinit ri mi):
  sem_sistate ctx sisf rf mf /\
  sfv_equiv ctx sfv rf mf fin.
Proof.
  ecase sexec_correct0 as (? & _); eauto.
Qed.

NB: each execution of a symbolic state (produced from sexec) represents a concrete execution (sexec is exact).
Theorem sexec_exact (ctx:iblock_function_context) ri mi ib sinit sisf sfv
  (SE : get_soutcome ctx (sexec ib sinit) = sout sisf sfv)
  (HYP : `sisf.(sis_hyp) ctx)
  (SIS : sem_sistate ctx sinit ri mi)
  (OKF : sis_ok ctx sisf):
  exists rf mf fin,
    btl_istep ctx ri mi ib rf mf (Some fin) /\
    sem_sistate ctx sisf rf mf /\
    sfv_equiv ctx sfv rf mf fin.
Proof.
  ecase sexec_correct0 as (_ & (rf & mf & fin & ISTEP)); eauto.
  exists rf, mf, fin; split; auto.
  eapply sexec_correct; eauto.
Qed.

End SEXEC.

Simulation properties on internal states


Definition svident_simu ctx (fp0 fp1 : sval + qualident) : Prop :=
  map_sum_left_opt (eval_sval ctx) fp0 = map_sum_left_opt (eval_sval ctx) fp1.

Definition bargs_simu ctx (args1 args2: list (builtin_arg sval)): Prop :=
  eval_list_builtin_sval ctx args1 = eval_list_builtin_sval ctx args2.

Inductive sfv_simu ctx: sfval -> sfval -> Prop :=
  | Bgoto_simu pc: sfv_simu ctx (Bgoto pc) (Bgoto pc)
  | Bcall_simu sig ros1 ros2 args1 args2 r pc
      (SVID: svident_simu ctx ros1 ros2)
      (ARGS: map_opt (eval_sval ctx) args1 = map_opt (eval_sval ctx) args2)
      :sfv_simu ctx (Bcall sig ros1 args1 r pc) (Bcall sig ros2 args2 r pc)
  | Btailcall_simu sig ros1 ros2 args1 args2
      (SVID: svident_simu ctx ros1 ros2)
      (ARGS: map_opt (eval_sval ctx) args1 = map_opt (eval_sval ctx) args2)
      :sfv_simu ctx (Btailcall sig ros1 args1) (Btailcall sig ros2 args2)
  | Bbuiltin_simu ef lba1 lba2 br pc
      (BARGS: bargs_simu ctx lba1 lba2)
      :sfv_simu ctx (Bbuiltin ef lba1 br pc) (Bbuiltin ef lba2 br pc)
  | Bjumptable_simu sv1 sv2 lpc
      (VAL: eval_sval ctx sv1 = eval_sval ctx sv2)
      :sfv_simu ctx (Bjumptable sv1 lpc) (Bjumptable sv2 lpc)
  | Breturn_simu osv1 osv2
      (OPT:optsv_simu ctx osv1 osv2)
      :sfv_simu ctx (Breturn osv1) (Breturn osv2)
.

Lemma sfv_simu_eval ctx sfv0 sfv1
  (SIMU : sfv_simu ctx sfv0 sfv1):
  eval_final_sval ctx sfv0 = eval_final_sval ctx sfv1.
Proof.
  inversion SIMU; try inversion OPT; simpl;
  unfold svident_simu, bargs_simu, eval_list_builtin_sval, eval_builtin_sval in *;
  rewrite ?SVID, ?ARGS, ?BARGS, ?VAL, ?SIMU0;
  try reflexivity.
Qed.

Definition sistate_simu ctx (sis1 sis2:sistate): Prop :=
  forall rs m,
    sem_sistate ctx sis2 rs m ->
    sem_sistate ctx sis1 rs m.


Builder for the target initial state (with invariant tree in sreg

Applying symbolic invariants


Substitutions in parallel symbolic invariants We apply it only on total sistates: subst should never return None (total_sreg property). Below, we enforce here a sval result (instead of an option sval) to simplify proofs.

Fixpoint sv_subst (substm : smem) (subst : bool -> reg -> option sval) (sv: sval): sval :=
  let sv_subst := sv_subst substm subst in
  let lsv_subst := lsv_subst substm subst in
  let sm_subst := sm_subst substm subst in
  let okclause_subst := okclause_subst substm subst in
  match sv with
  | Sinput trg r _ =>
      match subst trg r with
      | Some sv' => sv'
      | None => fSinput trg r
      end
  | Sop op lsv _ =>
     let lsv' := lsv_subst lsv in
     fSop op lsv'
  | Sfoldr op lsv sv0 _ =>
     let lsv' := lsv_subst lsv in
     let sv0' := sv_subst sv0 in
     fSfoldr op lsv' sv0'
  | Sload sm trap chunk addr lsv _ =>
     let sm' := sm_subst sm in
     let lsv' := lsv_subst lsv in
     fSload sm' trap chunk addr lsv'
  | SmayUndef cond sv _ =>
     let cond' := okclause_subst cond in
     let sv' := sv_subst sv in
     fSmayUndef cond' sv'
  end
with lsv_subst substm subst (lsv0: list_sval): list_sval :=
  match lsv0 with
  | Snil _ => fSnil
  | Scons sv lsv _ =>
    let sv' := sv_subst substm subst sv in
    let lsv' := lsv_subst substm subst lsv in
    fScons sv' lsv'
  end
with sm_subst substm subst (sm0: smem): smem :=
  match sm0 with
  | Sinit _ => substm
  | Sstore sm chunk addr lsv sinfo sv _ =>
     let sm' := sm_subst substm subst sm in
     let lsv' := lsv_subst substm subst lsv in
     let sv' := sv_subst substm subst sv in
     fSstore sm' chunk addr lsv' sinfo sv'
  end
with okclause_subst substm subst ok : okclause :=
  let sv_subst := sv_subst substm subst in
  let lsv_subst := lsv_subst substm subst in
  match ok with
  | OKfalse hid =>
      OKfalse hid
  | OKalive sv hid =>
      let sv' := sv_subst sv in
      OKalive sv' hid
  | OKpromotableOp op prom lsv hid =>
      let lsv' := lsv_subst lsv in
      OKpromotableOp op prom lsv' hid
  | OKpromotableCond cond prom lsv hid =>
      let lsv' := lsv_subst lsv in
      OKpromotableCond cond prom lsv' hid
  | OKaddrMatch addr lsv av hid =>
      let lsv' := lsv_subst lsv in
      OKaddrMatch addr lsv' av hid
  | OKvalidAccess perm chk addr lsv hid =>
      let lsv' := lsv_subst lsv in
      OKvalidAccess perm chk addr lsv' hid
  end.

Lemma lsv_subst_eq sm sv lsv:
  list_of_lsv (lsv_subst sm sv lsv) = map (sv_subst sm sv) (list_of_lsv lsv).
Proof.
  induction lsv; simpl; f_equal; auto.
Qed.

Definition subst_ctx (rs0 rs1 : regset) (m : mem) (ctx : iblock_common_context) : iblock_common_context :=
  Bcctx (cge ctx) (csp ctx) rs0 rs1 m (cbc ctx).

Lemma subst_ctx_self ctx:
  subst_ctx (crs0 ctx) (crs1 ctx) (cm1 ctx) ctx = ctx.
Proof.
  destruct ctx; reflexivity.
Qed.

Section SV_SUBST_CORRECT.
  Variables (rs0 rs1 : regset) (m : mem) (ctx : iblock_common_context)
             (substm : smem) (subst : bool -> reg -> option sval).
  Hypotheses (EVAL_MEM : eval_smem ctx substm = Some m)
             (EVAL_REG : forall trg r, eval_osv ctx (subst trg r) = Some (if trg then rs1 else rs0)#r).

Lemma sv_subst_correct_comb:
  let GOAL [A B] sb (ev : iblock_common_context -> A -> B) :=
    forall (sv : A), ev ctx (sb substm subst sv) = ev (subst_ctx rs0 rs1 m ctx) sv in
  GOAL sv_subst eval_sval /\
  GOAL lsv_subst eval_list_sval /\
  GOAL sm_subst eval_smem /\
  GOAL okclause_subst eval_okclauseb.
Proof.
  apply sval_mut_comb;
    simpl; repeat first [intros ->|intro]; try reflexivity.
  - generalize (EVAL_REG trg r); do 2 autodestruct; simpl; try_simplify_someHyps.
  - autodestruct. intros; eapply op_valid_pointer_eq; eauto.
  - do 2 autodestruct. intros; eapply fold_right_ext.
    intros; destruct y; auto.
    eapply op_valid_pointer_eq; eauto.
  - rewrite EVAL_MEM; reflexivity.
  - autodestruct; intro; apply rew_proj_sumbool_dec.
    apply adp_op_promotable_valid_pointer_eq; eauto.
  - autodestruct; intro; apply rew_proj_sumbool_dec.
    apply adp_cond_promotable_valid_pointer_eq; eauto.
  - apply rew_proj_sumbool_dec.
    unfold ex_Some; repeat autodestruct; try reflexivity; intros.
    eapply mem_valid_accessv_preserv; eauto.
Qed.

Lemma sv_subst_correct sv:
  eval_sval ctx (sv_subst substm subst sv) = eval_sval (subst_ctx rs0 rs1 m ctx) sv.
Proof.
apply sv_subst_correct_comb. Qed.

Lemma sm_subst_correct sm:
  eval_smem ctx (sm_subst substm subst sm) = eval_smem (subst_ctx rs0 rs1 m ctx) sm.
Proof.
apply sv_subst_correct_comb. Qed.

End SV_SUBST_CORRECT.

Lemma sv_subst_root_apply sm sb rsv alsv asm:
  sv_subst sm sb (root_apply rsv alsv asm) = root_apply rsv (lsv_subst sm sb alsv) (sm_subst sm sb asm).
Proof.
  unfold root_apply; repeat autodestruct.
Qed.

Definition sis_sv_subst (sis : sistate) : sval -> sval :=
  sv_subst (sis_smem sis) (fun trg r => if trg then Some (fSinput true r) else sis_sreg sis r).

Definition subst_ctx_src rs m ctx := subst_ctx rs (crs1 ctx) m ctx.

Lemma sem_sis_sv_subst ctx sis rs m sv
  (SIS : sem_sistate ctx sis rs m)
  (TOT : total_sreg sis):
  eval_sval ctx (sis_sv_subst sis sv) =
  eval_sval (subst_ctx_src rs m ctx) sv.
Proof.
  apply sv_subst_correct.
  - apply SIS.
  - intros [|] r. reflexivity.
    case (elim_alive (TOT r)) as (? & R); rewrite R; simpl.
    apply SIS, R.
Qed.

Definition sis_sm_subst_trg (sis : sistate) : smem -> smem :=
  sm_subst (sis_smem sis) (fun aux r => if aux then sis_sreg sis r else Some (fSinput false r)).

Definition subst_ctx_trg rs m ctx := subst_ctx (crs0 ctx) rs m ctx.

Lemma sem_sis_sm_subst_trg ctx sis rs m sm
  (SIS : sem_sistate ctx sis rs m)
  (TOT : total_sreg sis):
  eval_smem ctx (sis_sm_subst_trg sis sm) =
  eval_smem (subst_ctx_trg rs m ctx) sm.
Proof.
  apply sm_subst_correct.
  - apply SIS.
  - intros [|] r. 2:reflexivity.
    case (elim_alive (TOT r)) as (? & R); rewrite R; simpl.
    apply SIS, R.
Qed.

Variant of the si_ok definition with substitution
Program Definition si_ok_subst (sis: sistate) (si: fpasv) : okpred := fun ctx =>
  forall sv, List.In sv (fpa_ok si) -> alive (eval_sval ctx (sis_sv_subst sis sv)).
Next Obligation.
  setoid_rewrite eval_sval_preserved.
  reflexivity.
Qed.

Lemma si_ok_subst_eval sis si r sv ctx
  (SIS_OK : sis_ok ctx sis)
  (SI_OK : proj1_sig (si_ok_subst sis si) ctx)
  (R : si r = Some sv):
  alive (eval_sval ctx (sis_sv_subst sis sv)).
Proof.
   apply fpa_wf in R as [[]|]; simpl.
   - unfold sis_sv_subst; simpl; autodestruct.
     + apply SIS_OK.
     + discriminate 2.
   - apply SI_OK; auto.
Qed.

Transfer an internal state by applying the invariant and updating the pre-condition. Here, sis_input_init indicates the default option sval.
Program Definition tr_sis (sis: sistate) (si: fpasv) (sis_input_init: option bool): sistate :=
  {|
    sis_hyp := sis.(sis_hyp);
    sis_pre := fun ctx => sis_ok ctx sis /\ proj1_sig (si_ok_subst sis si) ctx;
    sis_sreg := fun r => match si r with
                         | Some sv => Some (sis_sv_subst sis sv)
                         | None => SOME trg <- sis_input_init IN Some (fSinput trg r)
                         end;
    sis_smem := sis.(sis_smem)
  |}.
Solve All Obligations with
  (cbn beta; intros; rewrite sis_ok_preserved, okpred_preserved; reflexivity).

Lemma tr_sis_rel sis si sinit:
  sis_rel sis (tr_sis sis si sinit).
Proof.
  split; simpl; try tauto.
  intros ? [(? & _)]; tauto.
Qed.

Lemma tr_sis_total sis si trg:
  total_sreg (tr_sis sis si (Some trg)).
Proof.
  intro; simpl; autodestruct.
Qed.

Lemma ok_tr_sis ctx sis si ini:
  sis_ok ctx (tr_sis sis si ini) <-> sis_ok ctx sis /\ proj1_sig (si_ok_subst sis si) ctx.
Proof.
  split; intro OK; try apply OK; constructor; try apply OK.
  case OK as (SOK & SI).
  intros r sv; simpl.
  repeat autodestruct; try_simplify_someHyps; try congruence.
  do 2 intro; eapply si_ok_subst_eval; eauto. exact SI.
Qed.

Lemma tr_sis_elim_match_si (sis : sistate) (si : fpasv) (sinit : option bool) ctx rs0 rs1 m
  (SIS : sem_sistate ctx sis rs0 m)
  (TOT : total_sreg sis)
  (SI : match_si (subst_ctx_src rs0 m ctx) si rs1)
  (INI : if_Some sinit (fun trg => rs1 = if trg then crs1 ctx else crs0 ctx)):
  sem_sistate ctx (tr_sis sis si sinit) rs1 m.
Proof.
  split; [|split].
  - split; eauto using sem_sis_ok.
    intro.
    erewrite sem_sis_sv_subst by eauto.
    apply SI.
  - apply SIS.
  - intros r sv; simpl.
    repeat autodestruct; try_simplify_someHyps; intros.
    + erewrite sem_sis_sv_subst by eauto.
      eapply SI; eauto.
    + unfold crsb; autodestruct.
Qed.

Lemma tr_sis_intro_match_si (sis0 sis1 : sistate) (si : fpasv) sinit ctx rs0 rs1 m
  (TR : tr_sis sis0 si sinit = sis1)
  (SIS0 : sem_sistate ctx sis0 rs0 m)
  (SIS1 : sem_sistate ctx sis1 rs1 m)
  (TOT : total_sreg sis0):
  match_si (subst_ctx_src rs0 m ctx) si rs1.
Proof.
  subst sis1; split.
  - case SIS1 as ((_ & SIS1) & _ & _).
    intros sv H.
    generalize (SIS1 sv H).
    erewrite sem_sis_sv_subst; eauto.
  - intros r sv R_SI.
    assert (R_SIS : tr_sis sis0 si sinit r = Some (sis_sv_subst sis0 sv))
      by (simpl; rewrite R_SI; reflexivity).
    apply SIS1 in R_SIS as <-.
    symmetry; apply sem_sis_sv_subst; auto.
Qed.

Operations on two sistate


Section TwoStatesOp.


Definition sis_get_ireg (sis0 sis1 : sistate) (r : ireg) : option sval :=
  if r.(force_input) then sis0 r else sis1 r.

Lemma sis_get_ireg_nofail ctx sis0 sis1 r sv
  (SOK0 : sis_ok ctx sis0)
  (SOK1 : sis_ok ctx sis1)
  (GET: sis_get_ireg sis0 sis1 r = Some sv):
  alive (eval_sval ctx sv).
Proof.
  unfold sis_get_ireg in GET; case force_input in GET; [inversion SOK0|inversion SOK1];
  apply OK_SREG0 in GET; exact GET.
Qed.

Lemma lmap_sv_ir_input_of sis0 sis1 rs:
  lmap_sv (sis_get_ireg sis0 sis1) (ir_input_of rs) = lmap_sv sis0 rs.
Proof.
  unfold ir_input_of.
  rewrite !lmap_sv_eq, map_opt_map.
  reflexivity.
Qed.

Lemma sis_get_ireg_lmap_nofail ctx sis0 sis1 rs lsv
  (SOK0 : sis_ok ctx sis0)
  (SOK1 : sis_ok ctx sis1)
  (GET: lmap_sv (sis_get_ireg sis0 sis1) rs = Some lsv):
  alive (eval_list_sval ctx lsv).
Proof.
  rewrite eval_list_sval_eq.
  rewrite lmap_sv_eq in GET.
  case map_opt eqn:LSV in GET; inv GET.
  rewrite l_lsv_l.
  apply map_opt_alive, Forall_forall; intros.
  eapply map_opt_iff_forall2, list_forall2_in_right in LSV as (? & _ & GET); eauto.
  eapply sis_get_ireg_nofail in GET; eauto.
Qed.

Lemma sis_get_reg_lmap_nofail ctx sis rs lsv
  (SOK : sis_ok ctx sis)
  (GET: lmap_sv sis rs = Some lsv):
  alive (eval_list_sval ctx lsv).
Proof.
  rewrite <- lmap_sv_ir_input_of with (sis1:=sis) in GET.
  eapply sis_get_ireg_lmap_nofail; eauto.
Qed.


Definition sis_set_rop (r : reg) (rop : root_op) (lir : list ireg) (sis0 sis1 : sistate): option sistate :=
  SOME lsv <- lmap_sv (sis_get_ireg sis0 sis1) lir IN
  Some (set_sreg r (root_apply rop lsv sis0.(sis_smem)) sis1).

Definition sis_get_ival (sis0 sis1 : sistate) (iv : ival) : option sval :=
  match iv with
  | Ireg ir => sis_get_ireg sis0 sis1 ir
  | Iop rop args => SOME lsv <- lmap_sv (sis_get_ireg sis0 sis1) args IN
                    Some (root_apply rop lsv sis0.(sis_smem))
  end.

Definition sis_set_ival (r : reg) (iv : ival) (sis0 sis1 : sistate): option sistate :=
  SOME sv <- sis_get_ival sis0 sis1 iv IN
  Some (set_sreg r sv sis1).

End TwoStatesOp.

Source symbolic state builder and register/memory set functions


Section InvariantApplication.

  Variable csix : invariants.
  Variable ctx : iblock_common_context.

sis_history is obtained by applying the history invariants to the initial state

Definition sis_history := tr_sis sis_empty (history csix) (Some false).

Lemma sis_history_correct
  (MATCH_H : match_si ctx (history csix) (crs0 ctx)):
  sem_sistate ctx sis_history (crs0 ctx) (cm1 ctx).
Proof.
  apply tr_sis_elim_match_si with (rs0 := crs0 ctx);
    simpl; auto using sem_sistate_empty, empty_total_sreg.
  unfold subst_ctx_src; rewrite subst_ctx_self. exact MATCH_H.
Qed.

sis_target is obtained by applying the gluing invariants to sis_history

Definition sis_target :=
  let sis_H := sis_history in
  tr_sis sis_H (glue csix) (Some true).

Lemma sis_target_ok_sis_history:
  sis_ok ctx sis_target -> sis_ok ctx sis_history.
Proof.
  apply tr_sis_rel.
Qed.

Lemma sis_target_correct m0:
  match_invs ctx csix m0 ->
  sem_sistate ctx sis_target (crs1 ctx) (cm1 ctx).
Proof.
  intros (MATCH_H & MATCH_G & _).
  apply tr_sis_elim_match_si with (rs0 := crs0 ctx).
  - apply sis_history_correct; assumption.
  - apply tr_sis_total.
  - unfold subst_ctx_src; rewrite subst_ctx_self. exact MATCH_G.
  - reflexivity.
Qed.

sis_source has the same registers as sis_history but with the more restrictive precondition of sis_target and the memory of meminv

Program Definition sis_source :=
  let sis_H := sis_history in
  let sis_HG := sis_target in
  {|
    sis_hyp := okConst True;
    sis_pre := fun ctx => sis_ok ctx sis_HG;
    sis_sreg := sis_H.(sis_sreg);
    sis_smem := sis_sm_subst_trg sis_target (imem_subst (meminv csix));
  |}.
Next Obligation.
apply sis_ok_preserved. Qed.

Lemma sis_source_ok_sis_target:
  sis_ok ctx sis_source <->
  sis_ok ctx sis_target /\
  alive (eval_smem ctx (sis_sm_subst_trg sis_target (imem_subst (meminv csix)))).
Proof.
  split.
  - intros [PRE MEM _]. exact (conj PRE MEM).
  - intros (OK & MEM).
    apply sis_target_ok_sis_history in OK as OK0.
    constructor; solve [apply OK | apply OK0 | exact MEM].
Qed.

Lemma sis_source_correct m0:
  match_invs ctx csix m0 ->
  sem_sistate ctx sis_source (crs0 ctx) m0.
Proof.
  intros MATCH.
  apply sis_target_correct in MATCH as SIS_T.
  apply sem_sis_ok in SIS_T as OK_T.
  case MATCH as (MATCH_H & _ & MATCH_MEM).
  apply sis_history_correct in MATCH_H.
  split; [|split].
  - apply OK_T.
  - rewrite <- MATCH_MEM.
    etransitivity. eapply sem_sis_sm_subst_trg; eauto using tr_sis_total.
    unfold subst_ctx_trg; rewrite subst_ctx_self; reflexivity.
  - apply MATCH_H.
Qed.

End InvariantApplication.

Lemma sis_source_rel csix:
  sis_rel (sis_target csix) (sis_source csix).
Proof.
  constructor; simpl; try tauto.
  apply sis_source_ok_sis_target.
Qed.


Computes the set of invariants for a final symbolic value


Definition si_sfv_set [A] (gm: node -> csasv) (fin : finalA A) : Prop * (csasv -> Prop) :=
  match fin with
  | Bgoto pc =>
      (True, eq (gm pc))
  | Bcall sig svid args res pc =>
      (test_clobberable (gm pc) res = true, eq (csi_remove res (gm pc)))
  | Bbuiltin ef args bres pc =>
      match reg_builtin_res bres with
      | Some r =>
          (test_clobberable (gm pc) r = true, eq (csi_remove r (gm pc)))
      | None =>
          (test_csifreem (gm pc) = true, eq (gm pc))
      end
  | Btailcall _ _ _ | Breturn _ =>
      (True, fun _ => False)
  | Bjumptable sv lpc =>
      (True, fun si => exists pc, In pc lpc /\ gm pc = si)
  end.

Lemma si_sfv_set_morph ctx gm sfv0 sfv1:
  sfv_simu ctx sfv0 sfv1 ->
  si_sfv_set gm sfv0 = si_sfv_set gm sfv1.
Proof.
  inversion 1; reflexivity.
Qed.

Lemma si_sfv_set_map_final [A B] (f : A -> option B) gm sfv0 sfv1:
  map_final_opt f sfv0 = Some sfv1 ->
  si_sfv_set gm sfv0 = si_sfv_set gm sfv1.
Proof.
  unfold map_final_opt, si_sfv_set.
  repeat autodestruct; try_simplify_someHyps; reflexivity.
Qed.


Definition meminv_sfv_set [A] (im : node -> imem) (fin : finalA A): Prop * (imem -> Prop) :=
  match fin with
  | Bgoto pc =>
      (True, eq (im pc))
  | Bcall _ _ _ _ pc | Bbuiltin _ _ _ pc =>
      (im pc = nil, eq nil)
  | Btailcall _ _ _ | Breturn _ =>
      (True, eq nil)
  | Bjumptable sv lpc =>
      (True, fun si => exists pc, In pc lpc /\ im pc = si)
  end.

Lemma meminv_sfv_set_morph ctx gm sfv0 sfv1:
  sfv_simu ctx sfv0 sfv1 ->
  meminv_sfv_set gm sfv0 = meminv_sfv_set gm sfv1.
Proof.
  inversion 1; reflexivity.
Qed.

Lemma meminv_sfv_set_map_final [A B : Type] (f : A -> option B) ims sfv0 sfv1:
  map_final_opt f sfv0 = Some sfv1 ->
  meminv_sfv_set ims sfv0 = meminv_sfv_set ims sfv1.
Proof.
  unfold map_final_opt, meminv_sfv_set.
  repeat autodestruct; try_simplify_someHyps; reflexivity.
Qed.


High-Level specification of the symbolic simulation test as predicate match_sexec_si


NOTE: we need to mix semantical simulation and syntactic definition on sfval in order to abstract the match_states of BTL_BlockSimulation. 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.

Definition match_tr_si_sfv (ctx : iblock_common_context) (gm : node -> csasv)
                           (sis0 : sistate) (sfv : sfval) (sis1 : sistate) : Prop :=
  let (siP, siS) := si_sfv_set gm sfv in
  siP /\ forall (si : csasv), siS si ->
  let sisI := tr_sis sis0 (siof si) None in
  sistate_simu ctx sisI sis1.

Definition match_sexec_si (ctx : iblock_common_context) (gm : gluemap) ib1 ib2 pc : Prop :=
  let ss1E := sexec ib1 (sis_source (gm pc)) in
  let ss2IE := sexec ib2 (sis_target (gm pc)) in
  let (sis1E, sfv1E) := get_soutcome ctx ss1E in
  `sis1E.(sis_hyp) ctx /\ (
  sis_ok ctx sis1E ->
    let (sis2IE, sfv2IE) := get_soutcome ctx ss2IE in
    let sisE := set_smem (sis_smem sis2IE) sis1E in
    `sis2IE.(sis_hyp) ctx /\
    sis_ok ctx sis2IE /\
    sfv_simu ctx sfv1E sfv2IE /\
    match_tr_si_sfv ctx (fun pc => history (gm pc)) sisE sfv1E sisE /\
    match_tr_si_sfv ctx (fun pc => glue (gm pc)) sisE sfv1E sis2IE /\
    let (miP, miS) := meminv_sfv_set (fun pc => meminv (gm pc)) sfv1E in
    miP /\ forall (im : imem), miS im ->
    smem_equiv ctx (sis_smem sis1E) (sis_sm_subst_trg sis2IE (imem_subst im))
  ).

Instantiate and fix a context for symbolic execution
Definition match_sexec_si_all_ctx (gm : gluemap) ib1 ib2 pc : Prop :=
  forall ctx, match_sexec_si ctx gm ib1 ib2 pc.