(* A theory of symbolic execution on RTLpath

NB: an efficient implementation with hash-consing will be defined in RTLpathSE_impl.v

*)

Require Import Coqlib Maps Floats.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import RTL RTLpath.
Require Import Errors Duplicate.

Local Open Scope error_monad_scope.

(* Enhanced from kvx/Asmblockgenproof.v *)
Ltac explore_hyp :=
  repeat match goal with
  | [ H : match ?var with | _ => _ end = _ |- _ ] => (let EQ1 := fresh "EQ" in (destruct var eqn:EQ1; try discriminate))
  | [ H : OK _ = OK _ |- _ ] => monadInv H
  | [ H : bind _ _ = OK _ |- _ ] => monadInv H
  | [ H : Error _ = OK _ |- _ ] => inversion H
  | [ H : Some _ = Some _ |- _ ] => inv H
  | [ x : unit |- _ ] => destruct x
  end.

Ltac explore := explore_hyp;
  repeat match goal with
  | [ |- context[if ?b then _ else _] ] => (let EQ1 := fresh "IEQ" in destruct b eqn:EQ1)
  | [ |- context[match ?m with | _ => _ end] ] => (let DEQ1 := fresh "DEQ" in destruct m eqn:DEQ1)
  | [ |- context[match ?m as _ return _ with | _ => _ end]] => (let DREQ1 := fresh "DREQ" in destruct m eqn:DREQ1)
  end.

(* Ltac explore :=
  repeat match goal with
  | [ H : match ?var with | _ => _ end = _ |- _ ] => (let EQ1 := fresh "EQ" in (destruct var eqn:EQ1; try discriminate))
  | [ H : OK _ = OK _ |- _ ] => monadInv H
  | [ |- context[if ?b then _ else _] ] => (let EQ1 := fresh "IEQ" in destruct b eqn:EQ1)
  | [ |- context[match ?m with | _ => _ end] ] => (let DEQ1 := fresh "DEQ" in destruct m eqn:DEQ1)
  | [ |- context[match ?m as _ return _ with | _ => _ end]] => (let DREQ1 := fresh "DREQ" in destruct m eqn:DREQ1)
  | [ H : bind _ _ = OK _ |- _ ] => monadInv H
  | [ H : Error _ = OK _ |- _ ] => inversion H
  | [ H : Some _ = Some _ |- _ ] => inv H
  | [ x : unit |- _ ] => destruct x
  end. *)

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

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

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

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

Local Open Scope option_monad_scope.

Fixpoint seval_sval (ge: RTL.genv) (sp:val) (sv: sval) (rs0: regset) (m0: mem): option val :=
  match sv with
  | Sinput r => Some (rs0#r)
  | Sop op l sm =>
     SOME args <- seval_list_sval ge sp l rs0 m0 IN
     SOME m <- seval_smem ge sp sm rs0 m0 IN
     eval_operation ge sp op args m
  | Sload sm trap chunk addr lsv =>
      match trap with
      | TRAP =>
          SOME args <- seval_list_sval ge sp lsv rs0 m0 IN
          SOME a <- eval_addressing ge sp addr args IN
          SOME m <- seval_smem ge sp sm rs0 m0 IN
          Mem.loadv chunk m a
      | NOTRAP =>
          SOME args <- seval_list_sval ge sp lsv rs0 m0 IN
          match (eval_addressing ge sp addr args) with
          | None => Some (default_notrap_load_value chunk)
          | Some a =>
              SOME m <- seval_smem ge sp sm rs0 m0 IN
              match (Mem.loadv chunk m a) with
              | None => Some (default_notrap_load_value chunk)
              | Some val => Some val
              end
          end
      end
  end
with seval_list_sval (ge: RTL.genv) (sp:val) (lsv: list_sval) (rs0: regset) (m0: mem): option (list val) :=
  match lsv with
  | Snil => Some nil
  | Scons sv lsv' => 
    SOME v <- seval_sval ge sp sv rs0 m0 IN
    SOME lv <- seval_list_sval ge sp lsv' rs0 m0 IN
    Some (v::lv)
  end
with seval_smem (ge: RTL.genv) (sp:val) (sm: smem) (rs0: regset) (m0: mem): option mem :=
  match sm with
  | Sinit => Some m0
  | Sstore sm chunk addr lsv srce =>
     SOME args <- seval_list_sval ge sp lsv rs0 m0 IN
     SOME a <- eval_addressing ge sp addr args IN
     SOME m <- seval_smem ge sp sm rs0 m0 IN
     SOME sv <- seval_sval ge sp srce rs0 m0 IN
     Mem.storev chunk m a sv
  end.

(* Syntax and Semantics of local symbolic internal states *)
(* [si_pre] is a precondition on initial ge, sp, rs0, m0 *)
Record sistate_local := { si_pre: RTL.genv -> val -> regset -> mem -> Prop; si_sreg: reg -> sval; si_smem: smem }.

(* Predicate on which (rs, m) is a possible final state after evaluating [st] on (rs0, m0) *)
Definition ssem_local (ge: RTL.genv) (sp:val) (st: sistate_local) (rs0: regset) (m0: mem) (rs: regset) (m: mem): Prop :=
  st.(si_pre) ge sp rs0 m0
  /\ seval_smem ge sp st.(si_smem) rs0 m0 = Some m
  /\ forall (r:reg), seval_sval ge sp (st.(si_sreg) r) rs0 m0 = Some (rs#r).

Definition sabort_local (ge: RTL.genv) (sp:val) (st: sistate_local) (rs0: regset) (m0: mem): Prop :=
  ~(st.(si_pre) ge sp rs0 m0)
  \/ seval_smem ge sp st.(si_smem) rs0 m0 = None
  \/ exists (r: reg), seval_sval ge sp (st.(si_sreg) r) rs0 m0 = None.

(* Syntax and semantics of symbolic exit states *)
Record sistate_exit := mk_sistate_exit
  { si_cond: condition; si_scondargs: list_sval; si_elocal: sistate_local; si_ifso: node }.

Definition seval_condition ge sp (cond: condition) (lsv: list_sval) (sm: smem) rs0 m0 : option bool :=
  SOME args <- seval_list_sval ge sp lsv rs0 m0 IN
  SOME m <- seval_smem ge sp sm rs0 m0 IN
  eval_condition cond args m.

Definition all_fallthrough ge sp (lx: list sistate_exit) rs0 m0: Prop :=
  forall ext, List.In ext lx ->
  seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = Some false.

Lemma all_fallthrough_revcons ge sp ext rs m lx:
  all_fallthrough ge sp (ext::lx) rs m ->
  seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs m = Some false
  /\ all_fallthrough ge sp lx rs m.
Proof.
  intros ALLFU. constructor.
  - assert (In ext (ext::lx)) by (constructor; auto). apply ALLFU in H. assumption.
  - intros ext' INEXT. assert (In ext' (ext::lx)) by (apply in_cons; auto).
    apply ALLFU in H. assumption.
Qed.

(** Semantic of an exit in pseudo code:
     if si_cond (si_condargs)
       si_elocal; goto if_so
     else ()
*)

Definition ssem_exit (ge: RTL.genv) (sp: val) (ext: sistate_exit) (rs: regset) (m: mem) rs' m' (pc': node) : Prop :=
    seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m = Some true
 /\ ssem_local ge sp (si_elocal ext) rs m rs' m'
 /\ (si_ifso ext) = pc'.

(* Either an abort on the condition evaluation OR an abort on the sistate_local IF the condition was true *)
Definition sabort_exit (ge: RTL.genv) (sp: val) (ext: sistate_exit) (rs: regset) (m: mem) : Prop :=
  let sev_cond := seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m in
  sev_cond = None
  \/ (sev_cond = Some true /\ sabort_local ge sp ext.(si_elocal) rs m).

(** * Syntax and Semantics of symbolic internal state *)
Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local }. 

Definition all_fallthrough_upto_exit ge sp ext lx' lx rs m : Prop :=
  is_tail (ext::lx') lx /\ all_fallthrough ge sp lx' rs m.

(** Semantic of a sistate in pseudo code:
     si_exit1; si_exit2; ...; si_exitn;
     si_local; goto si_pc *)

(* Note: in RTLpath, is.(icontinue) = false iff we took an early exit *)

Definition ssem_internal (ge: RTL.genv) (sp:val) (st: sistate) (rs: regset) (m: mem) (is: istate): Prop :=
  if (is.(icontinue)) 
  then 
    ssem_local ge sp st.(si_local) rs m is.(irs) is.(imem) 
    /\ st.(si_pc) = is.(ipc)
    /\ all_fallthrough ge sp st.(si_exits) rs m
  else exists ext lx,
    ssem_exit ge sp ext rs m is.(irs) is.(imem) is.(ipc)
    /\ all_fallthrough_upto_exit ge sp ext lx st.(si_exits) rs m.

Definition sabort (ge: RTL.genv) (sp: val) (st: sistate) (rs: regset) (m: mem): Prop :=
  (* No early exit was met but we aborted on the si_local *)
  (all_fallthrough ge sp st.(si_exits) rs m /\ sabort_local ge sp st.(si_local) rs m)
  (* OR we aborted on an evaluation of one of the early exits *)
  \/ (exists ext lx, all_fallthrough_upto_exit ge sp ext lx st.(si_exits) rs m /\ sabort_exit ge sp ext rs m).

Definition ssem_internal_opt ge sp (st: sistate) rs0 m0 (ois: option istate): Prop :=
  match ois with
  | Some is => ssem_internal ge sp st rs0 m0 is
  | None => sabort ge sp st rs0 m0
  end.

Definition ssem_internal_opt2 ge sp (ost: option sistate) rs0 m0 (ois: option istate) : Prop :=
  match ost with
  | Some st => ssem_internal_opt ge sp st rs0 m0 ois
  | None => ois=None
  end.

(** * An internal state represents a parallel program !

     We prove below that the semantics [ssem_internal_opt] is deterministic.

 *)

Definition istate_eq ist1 ist2 :=
  ist1.(icontinue) = ist2.(icontinue) /\
  ist1.(ipc) = ist2.(ipc) /\
  (forall r, (ist1.(irs)#r) = ist2.(irs)#r) /\ 
  ist1.(imem) = ist2.(imem).

Lemma all_fallthrough_noexit ge sp ext lx rs0 m0 rs m pc:
  ssem_exit ge sp ext rs0 m0 rs m pc ->
  In ext lx ->
  all_fallthrough ge sp lx rs0 m0 ->
  False.
Proof.
  Local Hint Resolve is_tail_in: core.
  intros SSEM INE ALLF.
  destruct SSEM as (SSEM & SSEM').
  unfold all_fallthrough in ALLF. rewrite ALLF in SSEM; eauto.
  discriminate.
Qed.

Lemma ssem_internal_exclude_incompatible_continue ge sp st rs m is1 is2:
  is1.(icontinue) = true ->
  is2.(icontinue) = false ->
  ssem_internal ge sp st rs m is1 ->
  ssem_internal ge sp st rs m is2 ->
  False.
Proof.
  Local Hint Resolve all_fallthrough_noexit: core.
  unfold ssem_internal.
  intros CONT1 CONT2.
  rewrite CONT1, CONT2; simpl.
  intuition eauto.
  destruct H0 as (ext & lx & SSEME & ALLFU).
  destruct ALLFU as (ALLFU & ALLFU').
  eapply all_fallthrough_noexit; eauto.
Qed.

Lemma ssem_internal_determ_continue ge sp st rs m is1 is2:
   ssem_internal ge sp st rs m is1 ->
   ssem_internal ge sp st rs m is2 ->
   is1.(icontinue) = is2.(icontinue).
Proof.
   Local Hint Resolve ssem_internal_exclude_incompatible_continue: core.
   destruct (Bool.bool_dec is1.(icontinue) is2.(icontinue)) as [|H]; auto.
   intros H1 H2. assert (absurd: False); intuition.
   destruct (icontinue is1) eqn: His1, (icontinue is2) eqn: His2; eauto.
Qed.

Lemma ssem_local_determ ge sp st rs0 m0 rs1 m1 rs2 m2:
  ssem_local ge sp st rs0 m0 rs1 m1 ->
  ssem_local ge sp st rs0 m0 rs2 m2 ->
  (forall r, rs1#r = rs2#r) /\ m1 = m2.
Proof.
  unfold ssem_local. intuition try congruence.
  generalize (H5 r); rewrite H4; congruence.
Qed.

(* TODO: lemma to move in Coqlib *)
Lemma is_tail_bounded_total {A} (l1 l2 l3: list A): is_tail l1 l3 -> is_tail l2 l3
  -> is_tail l1 l2 \/ is_tail l2 l1.
Proof.
  Local Hint Resolve is_tail_cons: core.
  induction 1 as [|i l1 l3 T1 IND]; simpl; auto.
  intros T2; inversion T2; subst; auto.
Qed.

Lemma exit_cond_determ ge sp rs0 m0 l1 l2: 
  is_tail l1 l2 -> forall ext1 lx1 ext2 lx2, 
  l1=(ext1 :: lx1) -> 
  l2=(ext2 :: lx2) ->
  all_fallthrough ge sp lx1 rs0 m0 ->
  seval_condition ge sp (si_cond ext1) (si_scondargs ext1) (si_smem (si_elocal ext1)) rs0 m0 = Some true ->
  all_fallthrough ge sp lx2 rs0 m0 ->
  ext1=ext2.
Proof.
  destruct 1 as [l1|i l1 l3 T1]; intros ext1 lx1 ext2 lx2 EQ1 EQ2; subst; 
  inversion EQ2; subst; auto.
  intros D1 EVAL NYE.
  Local Hint Resolve is_tail_in: core.
  unfold all_fallthrough in NYE.
  rewrite NYE in EVAL; eauto.
  try congruence.
Qed.

Lemma ssem_exit_determ ge sp ext rs0 m0 rs1 m1 pc1 rs2 m2 pc2:
  ssem_exit ge sp ext rs0 m0 rs1 m1 pc1 ->
  ssem_exit ge sp ext rs0 m0 rs2 m2 pc2 ->
  pc1 = pc2 /\ (forall r, rs1#r = rs2#r) /\ m1 = m2.
Proof.
  Local Hint Resolve exit_cond_determ eq_sym: core.
  intros SSEM1 SSEM2. destruct SSEM1 as (SEVAL1 & SLOC1 & PCEQ1). destruct SSEM2 as (SEVAL2 & SLOC2 & PCEQ2). subst.
  destruct (ssem_local_determ ge sp (si_elocal ext) rs0 m0 rs1 m1 rs2 m2); auto.
Qed.

Remark is_tail_inv_left {A: Type} (a a': A) l l':
  is_tail (a::l) (a'::l') ->
  (a = a' /\ l = l') \/ (In a l' /\ is_tail l (a'::l')).
Proof.
  intros. inv H.
  - left. eauto.
  - right. econstructor.
    + eapply is_tail_in; eauto.
    + eapply is_tail_cons_left; eauto.
Qed.

Lemma ssem_internal_determ ge sp st rs m is1 is2:
  ssem_internal ge sp st rs m is1 ->
  ssem_internal ge sp st rs m is2 ->
  istate_eq is1 is2.
Proof.
  unfold istate_eq.
  intros SEM1 SEM2. 
  exploit (ssem_internal_determ_continue ge sp st rs m is1 is2); eauto.
  intros CONTEQ. unfold ssem_internal in * |-. rewrite CONTEQ in * |- *.
  destruct (icontinue is2).
  - destruct (ssem_local_determ ge sp (si_local st) rs m (irs is1) (imem is1) (irs is2) (imem is2)); 
    intuition (try congruence).
  - destruct SEM1 as (ext1 & lx1 & SSEME1 & ALLFU1). destruct SEM2 as (ext2 & lx2 & SSEME2 & ALLFU2).
    destruct ALLFU1 as (ALLFU1 & ALLFU1'). destruct ALLFU2 as (ALLFU2 & ALLFU2').
    destruct SSEME1 as (SSEME1 & SSEME1' & SSEME1''). destruct SSEME2 as (SSEME2 & SSEME2' & SSEME2'').
    assert (X:ext1=ext2).
    { destruct (is_tail_bounded_total (ext1 :: lx1) (ext2 :: lx2) (si_exits st)) as [TAIL|TAIL]; eauto. }
    subst. destruct (ssem_local_determ ge sp (si_elocal ext2) rs m (irs is1) (imem is1) (irs is2) (imem is2)); auto.
    intuition. congruence.
Qed.

Lemma ssem_local_exclude_sabort_local ge sp loc rs m rs' m':
  ssem_local ge sp loc rs m rs' m' ->
  sabort_local ge sp loc rs m ->
  False.
Proof.
  intros SIML ABORT. inv SIML. destruct H0 as (H0 & H0').
  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
Qed.

Lemma ssem_local_exclude_sabort ge sp st rs m rs' m':
  ssem_local ge sp (si_local st) rs m rs' m' ->
  all_fallthrough ge sp (si_exits st) rs m ->
  sabort ge sp st rs m ->
  False.
Proof.
  intros SIML ALLF ABORT.
  inv ABORT.
  - intuition; eapply ssem_local_exclude_sabort_local; eauto.
  - destruct H as (ext & lx & ALLFU & SABORT).
    destruct ALLFU as (TAIL & _). eapply is_tail_in in TAIL.
    eapply ALLF in TAIL.
    destruct SABORT as [CONDFAIL | (CONDTRUE & ABORTL)]; congruence.
Qed.

Lemma ssem_exit_fallthrough_upto_exit ge sp ext ext' lx lx' exits rs m rs' m' pc':
  ssem_exit ge sp ext rs m rs' m' pc' ->
  all_fallthrough_upto_exit ge sp ext lx exits rs m ->
  all_fallthrough_upto_exit ge sp ext' lx' exits rs m ->
  is_tail (ext'::lx') (ext::lx).
Proof.
  intros SSEME ALLFU ALLFU'.
  destruct ALLFU as (ISTAIL & ALLFU). destruct ALLFU' as (ISTAIL' & ALLFU').
  destruct (is_tail_bounded_total (ext::lx) (ext'::lx') exits); eauto.
  inv H.
  - econstructor; eauto.
  - eapply is_tail_in in H2. eapply ALLFU' in H2.
    destruct SSEME as (SEVAL & _). congruence.
Qed.

Lemma ssem_exit_exclude_sabort_exit ge sp ext rs m rs' m' pc':
  ssem_exit ge sp ext rs m rs' m' pc' ->
  sabort_exit ge sp ext rs m ->
  False.
Proof.
  intros A B. destruct A as (A & A' & A''). inv B.
  - congruence.
  - destruct H as (_ & H). eapply ssem_local_exclude_sabort_local; eauto.
Qed.

Lemma ssem_exit_exclude_sabort ge sp ext st lx rs m rs' m' pc':
  ssem_exit ge sp ext rs m rs' m' pc' ->
  all_fallthrough_upto_exit ge sp ext lx (si_exits st) rs m ->
  sabort ge sp st rs m ->
  False.
Proof.
  intros SSEM ALLFU ABORT.
  inv ABORT.
  - destruct H as (ALLF & _). destruct ALLFU as (TAIL & _).
    eapply is_tail_in in TAIL.
    destruct SSEM as (SEVAL & _ & _).
    eapply ALLF in TAIL. congruence.
  - destruct H as (ext' & lx' & ALLFU' & ABORT).
    exploit ssem_exit_fallthrough_upto_exit; eauto. intros ITAIL.
    destruct ALLFU as (ALLFU1 & ALLFU2). destruct ALLFU' as (ALLFU1' & ALLFU2').
    exploit (is_tail_inv_left ext' ext lx' lx); eauto. intro. inv H.
    + inv H0. eapply ssem_exit_exclude_sabort_exit; eauto.
    + destruct H0 as (INE & TAIL). eapply ALLFU2 in INE. destruct ABORT as [ABORT | (ABORT & ABORT')]; congruence.
Qed.

Lemma ssem_internal_exclude_sabort ge sp st rs m is:
  sabort ge sp st rs m ->
  ssem_internal ge sp st rs m is -> False.
Proof.
  intros ABORT SEM.
  unfold ssem_internal in SEM. destruct icontinue.
  - destruct SEM as (SEM1 & SEM2 & SEM3).
    eapply ssem_local_exclude_sabort; eauto.
  - destruct SEM as (ext & lx & SEM1 & SEM2). eapply ssem_exit_exclude_sabort; eauto.
Qed.

Definition istate_eq_opt ist1 oist :=
  exists ist2, oist = Some ist2 /\ istate_eq ist1 ist2.

Lemma ssem_internal_opt_determ ge sp st rs m ois is:
  ssem_internal_opt ge sp st rs m ois ->
  ssem_internal ge sp st rs m is ->
  istate_eq_opt is ois.
Proof.
  destruct ois as [is1|]; simpl; eauto.
  - intros; eexists; intuition; eapply ssem_internal_determ; eauto.
  - intros; exploit ssem_internal_exclude_sabort; eauto. destruct 1.
Qed.

(** * Symbolic execution of one internal step *)

Definition slocal_set_sreg (st:sistate_local) (r:reg) (sv:sval) :=
  {| si_pre:=(fun ge sp rs m => seval_sval ge sp (st.(si_sreg) r) rs m <> None /\ (st.(si_pre) ge sp rs m));
     si_sreg:=fun y => if Pos.eq_dec r y then sv else st.(si_sreg) y;
     si_smem:= st.(si_smem)|}.

Definition slocal_set_smem (st:sistate_local) (sm:smem) :=
  {| si_pre:=(fun ge sp rs m => seval_smem ge sp st.(si_smem) rs m <> None /\ (st.(si_pre) ge sp rs m));
     si_sreg:= st.(si_sreg);
     si_smem:= sm |}.

Definition sist_set_local (st: sistate) (pc: node) (nxt: sistate_local): sistate :=
   {| si_pc := pc; si_exits := st.(si_exits); si_local:= nxt |}.

Definition slocal_store st chunk addr args src : sistate_local :=
   let args := list_sval_inj (List.map (si_sreg st) args) in
   let src := si_sreg st src in
   let sm := Sstore (si_smem st) chunk addr args src
   in slocal_set_smem st sm.

Definition siexec_inst (i: instruction) (st: sistate): option sistate := 
  match i with
  | Inop pc' => 
      Some (sist_set_local st pc' st.(si_local))
  | Iop op args dst pc' =>
      let prev := st.(si_local) in
      let vargs := list_sval_inj (List.map prev.(si_sreg) args) in
      let next := slocal_set_sreg prev dst (Sop op vargs prev.(si_smem)) in
      Some (sist_set_local st pc' next)
  | Iload trap chunk addr args dst pc' =>
      let prev := st.(si_local) in
      let vargs := list_sval_inj (List.map prev.(si_sreg) args) in
      let next := slocal_set_sreg prev dst (Sload prev.(si_smem) trap chunk addr vargs) in
      Some (sist_set_local st pc' next)
  | Istore chunk addr args src pc' =>
      let next := slocal_store st.(si_local) chunk addr args src in
      Some (sist_set_local st pc' next)
   | Icond cond args ifso ifnot _ =>
      let prev := st.(si_local) in
      let vargs := list_sval_inj (List.map prev.(si_sreg) args) in
      let ex := {| si_cond:=cond; si_scondargs:=vargs; si_elocal := prev; si_ifso := ifso |} in
      Some {| si_pc := ifnot; si_exits := ex::st.(si_exits); si_local := prev |}
  | _ => None
  end.

Lemma seval_list_sval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs: 
   (forall r : reg, seval_sval ge sp (sreg r) rs0 m0 = Some (rs # r)) ->
   seval_list_sval ge sp (list_sval_inj (map sreg l)) rs0 m0 = Some (rs ## l).
Proof.
  intros H; induction l as [|r l]; simpl; auto.
  inversion_SOME v.
  inversion_SOME lv.
  generalize (H r).
  try_simplify_someHyps.
Qed.

Lemma slocal_set_sreg_preserves_sabort_local ge sp st rs0 m0 r sv:
  sabort_local ge sp st rs0 m0 ->
  sabort_local ge sp (slocal_set_sreg st r sv) rs0 m0.
Proof.
  unfold sabort_local. simpl; intuition.
  destruct H as [r1 H]. destruct (Pos.eq_dec r r1) as [TEST|TEST] eqn: HTEST.
  - subst; rewrite H; intuition.
  - right. right. exists r1. rewrite HTEST. auto.
Qed.

Lemma slocal_set_smem_preserves_sabort_local ge sp st rs0 m0 m:
  sabort_local ge sp st rs0 m0 ->
  sabort_local ge sp (slocal_set_smem st m) rs0 m0.
Proof.
  unfold sabort_local. simpl; intuition.
Qed.

Lemma all_fallthrough_upto_exit_cons ge sp ext lx ext' exits rs m:
  all_fallthrough_upto_exit ge sp ext lx exits rs m ->
  all_fallthrough_upto_exit ge sp ext lx (ext'::exits) rs m.
Proof.
  intros. inv H. econstructor; eauto.
Qed.

Lemma all_fallthrough_cons ge sp exits rs m ext:
  all_fallthrough ge sp exits rs m ->
  seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs m = Some false ->
  all_fallthrough ge sp (ext::exits) rs m.
Proof.
  intros. unfold all_fallthrough in *. intros.
  inv H1; eauto.
Qed.

Lemma siexec_inst_preserves_sabort i ge sp rs m st st': 
  siexec_inst i st = Some st' ->
  sabort ge sp st rs m -> sabort ge sp st' rs m.
Proof.
  intros SISTEP ABORT.
  destruct i; simpl in SISTEP; try discriminate; inv SISTEP; unfold sabort; simpl.
  (* NOP *)
  * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)].
    - left. constructor; eauto.
    - right. exists ext0, lx0. constructor; eauto.
  (* OP *)
  * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)].
    - left. constructor; eauto. eapply slocal_set_sreg_preserves_sabort_local; eauto.
    - right. exists ext0, lx0. constructor; eauto.
  (* LOAD *)
  * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)].
    - left. constructor; eauto. eapply slocal_set_sreg_preserves_sabort_local; eauto.
    - right. exists ext0, lx0. constructor; eauto.
  (* STORE *)
  * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)].
    - left. constructor; eauto. eapply slocal_set_smem_preserves_sabort_local; eauto.
    - right. exists ext0, lx0. constructor; eauto.
  (* COND *)
  * remember ({| si_cond := _; si_scondargs := _; si_elocal := _; si_ifso := _ |}) as ext.
    destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)].
    - destruct (seval_condition ge sp (si_cond ext) (si_scondargs ext)
        (si_smem (si_elocal ext)) rs m) eqn:SEVAL; [destruct b|].
      (* case true *)
      + right. exists ext, (si_exits st).
        constructor.
        ++ constructor. econstructor; eauto. eauto.
        ++ unfold sabort_exit. right. constructor; eauto.
           subst. simpl. eauto.
      (* case false *)
      + left. constructor; eauto. eapply all_fallthrough_cons; eauto.
      (* case None *)
      + right. exists ext, (si_exits st). constructor.
        ++ constructor. econstructor; eauto. eauto.
        ++ unfold sabort_exit. left. eauto.
    - right. exists ext0, lx0. constructor; eauto. eapply all_fallthrough_upto_exit_cons; eauto.
Qed.

Lemma siexec_inst_WF i st:
  siexec_inst i st = None -> default_succ i = None.
Proof.
  destruct i; simpl; unfold sist_set_local; simpl; congruence.
Qed.

Lemma siexec_inst_default_succ i st st':
  siexec_inst i st = Some st' -> default_succ i = Some (st'.(si_pc)).
Proof.
  destruct i; simpl; unfold sist_set_local; simpl; try congruence;
  intro H; inversion_clear H; simpl; auto.
Qed.


Lemma seval_list_sval_inj_not_none ge sp st rs0 m0: forall l,
  (forall r, List.In r l -> seval_sval ge sp (si_sreg st r) rs0 m0 = None -> False) ->
  seval_list_sval ge sp (list_sval_inj (map (si_sreg st) l)) rs0 m0 = None -> False.
Proof.
  induction l.
  - intuition discriminate.
  - intros ALLR. simpl.
    inversion_SOME v.
    + intro SVAL. inversion_SOME lv; [discriminate|].
      assert (forall r : reg, In r l -> seval_sval ge sp (si_sreg st r) rs0 m0 = None -> False).
      { intros r INR. eapply ALLR. right. assumption. }
      intro SVALLIST. intro. eapply IHl; eauto.
    + intros. exploit (ALLR a); simpl; eauto.
Qed.

Lemma siexec_inst_correct ge sp i st rs0 m0 rs m:
  ssem_local ge sp st.(si_local) rs0 m0 rs m ->
  all_fallthrough ge sp st.(si_exits) rs0 m0 ->
  ssem_internal_opt2 ge sp (siexec_inst i st) rs0 m0 (istep ge i sp rs m).
Proof.
  intros (PRE & MEM & REG) NYE.
  destruct i; simpl; auto.
  + (* Nop *)
    constructor; [|constructor]; simpl; auto.
    constructor; auto.
  + (* Op *)
    inversion_SOME v; intros OP; simpl.
    - constructor; [|constructor]; simpl; auto.
      constructor; simpl; auto.
      * constructor; auto. congruence.
      * constructor; auto.
        intro r0. destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto].
        subst. rewrite Regmap.gss; simpl; auto.
        erewrite seval_list_sval_inj; simpl; auto.
        try_simplify_someHyps.
    - left. constructor; simpl; auto.
      unfold sabort_local. right. right.
      simpl. exists r. destruct (Pos.eq_dec r r); try congruence.
      simpl. erewrite seval_list_sval_inj; simpl; auto.
      try_simplify_someHyps.
  + (* LOAD *) 
    inversion_SOME a0; intro ADD.
    { inversion_SOME v; intros LOAD; simpl. 
      - explore_destruct; unfold ssem_internal, ssem_local; simpl; intuition.
        * unfold ssem_internal. simpl. constructor; [|constructor]; auto.
          constructor; constructor; simpl; auto. congruence. intro r0.
          destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto].
          subst; rewrite Regmap.gss; simpl.
          erewrite seval_list_sval_inj; simpl; auto.
          try_simplify_someHyps.
        * unfold ssem_internal. simpl. constructor; [|constructor]; auto.
          constructor; constructor; simpl; auto. congruence. intro r0.
          destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto].
          subst; rewrite Regmap.gss; simpl.
          inversion_SOME args; intros ARGS.
          2: { exploit seval_list_sval_inj_not_none; eauto; intuition congruence. }
          exploit seval_list_sval_inj; eauto. intro ARGS'. erewrite ARGS in ARGS'. inv ARGS'. rewrite ADD.
          inversion_SOME m2. intro SMEM.
          assert (m = m2) by congruence. subst. rewrite LOAD. reflexivity.
      - explore_destruct; unfold sabort, sabort_local; simpl.
        * unfold sabort. simpl. left. constructor; auto.
          right. right. exists r. simpl. destruct (Pos.eq_dec r r); try congruence.
          simpl. erewrite seval_list_sval_inj; simpl; auto.
          rewrite ADD; simpl; auto. try_simplify_someHyps.
        * unfold ssem_internal. simpl. constructor; [|constructor]; auto.
          constructor; constructor; simpl; auto. congruence. intro r0.
          destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto].
          subst; rewrite Regmap.gss; simpl.
          erewrite seval_list_sval_inj; simpl; auto.
          try_simplify_someHyps.
     } { rewrite ADD. destruct t.
          - simpl. left; eauto. simpl. econstructor; eauto.
            right. right. simpl. exists r. destruct (Pos.eq_dec r r); [|contradiction].
            simpl. inversion_SOME args. intro SLS.
            eapply seval_list_sval_inj in REG. rewrite REG in SLS. inv SLS.
            rewrite ADD. reflexivity.
          - simpl. constructor; [|constructor]; simpl; auto.
            constructor; simpl; constructor; auto; [congruence|].
            intro r0. destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto].
            subst. simpl. rewrite Regmap.gss.
            erewrite seval_list_sval_inj; simpl; auto.
            try_simplify_someHyps.
     }
  + (* STORE *)
    inversion_SOME a0; intros ADD.
    { inversion_SOME m'; intros STORE; simpl.
      - unfold ssem_internal, ssem_local; simpl; intuition.
        * congruence.
        * erewrite seval_list_sval_inj; simpl; auto.
          erewrite REG.
          try_simplify_someHyps.
      - unfold sabort, sabort_local; simpl.
        left. constructor; auto. right. left.
        erewrite seval_list_sval_inj; simpl; auto.
        erewrite REG.
        try_simplify_someHyps. }
    { unfold sabort, sabort_local; simpl.
      left. constructor; auto. right. left.
      erewrite seval_list_sval_inj; simpl; auto.
      erewrite ADD; simpl; auto. }
  + (* COND *)
    Local Hint Resolve is_tail_refl: core.
    Local Hint Unfold ssem_local: core.
    inversion_SOME b; intros COND.
    { destruct b; simpl; unfold ssem_internal, ssem_local; simpl.
      - remember (mk_sistate_exit _ _ _ _) as ext. exists ext, (si_exits st).
        constructor; constructor; subst; simpl; auto.
        unfold seval_condition. subst; simpl.
        erewrite seval_list_sval_inj; simpl; auto.
        try_simplify_someHyps.
      - intuition. unfold all_fallthrough in * |- *. simpl.
        intuition. subst. simpl.
        unfold seval_condition.
        erewrite seval_list_sval_inj; simpl; auto.
        try_simplify_someHyps. }
    { unfold sabort. simpl. right.
      remember (mk_sistate_exit _ _ _ _) as ext. exists ext, (si_exits st).
      constructor; [constructor; subst; simpl; auto|].
      left. subst; simpl; auto.
      unfold seval_condition.
      erewrite seval_list_sval_inj; simpl; auto.
      try_simplify_someHyps. }
Qed.


Lemma siexec_inst_correct_None ge sp i st rs0 m0 rs m:
  ssem_local ge sp (st.(si_local)) rs0 m0 rs m ->
  siexec_inst i st = None -> 
  istep ge i sp rs m = None.
Proof.
  intros (PRE & MEM & REG).
  destruct i; simpl; unfold sist_set_local, ssem_internal, ssem_local; simpl; try_simplify_someHyps.
Qed.

(** * Symbolic execution of the internal steps of a path *)
Fixpoint siexec_path (path:nat) (f: function) (st: sistate): option sistate :=
  match path with
  | O => Some st
  | S p =>
    SOME i <- (fn_code f)!(st.(si_pc)) IN
    SOME st1 <- siexec_inst i st IN
    siexec_path p f st1
  end.

Lemma siexec_inst_add_exits i st st':
  siexec_inst i st = Some st' ->
  ( si_exits st' = si_exits st \/ exists ext, si_exits st' = ext :: si_exits st ).
Proof.
  destruct i; simpl; intro SISTEP; inversion_clear SISTEP; unfold siexec_inst; simpl; (discriminate || eauto).
Qed.

Lemma siexec_inst_preserves_allfu ge sp ext lx rs0 m0 st st' i:
  all_fallthrough_upto_exit ge sp ext lx (si_exits st) rs0 m0 ->
  siexec_inst i st = Some st' ->
  all_fallthrough_upto_exit ge sp ext lx (si_exits st') rs0 m0.
Proof.
  intros ALLFU SISTEP. destruct ALLFU as (ISTAIL & ALLF).
  constructor; eauto.
  destruct i; simpl in SISTEP; inversion_clear SISTEP; simpl; (discriminate || eauto).
Qed.

Lemma siexec_path_correct_false ge sp f rs0 m0 st' is:
  forall path,
  is.(icontinue)=false ->
  forall st, ssem_internal ge sp st rs0 m0 is ->
  siexec_path path f st = Some st' ->
  ssem_internal ge sp st' rs0 m0 is.
Proof.
  induction path; simpl.
  - intros. congruence.
  - intros ICF st SSEM STEQ'.
    destruct ((fn_code f) ! (si_pc st)) eqn:FIC; [|discriminate].
    destruct (siexec_inst _ _) eqn:SISTEP; [|discriminate].
    eapply IHpath. 3: eapply STEQ'. eauto.
    unfold ssem_internal in SSEM. rewrite ICF in SSEM.
    destruct SSEM as (ext & lx & SEXIT & ALLFU).
    unfold ssem_internal. rewrite ICF. exists ext, lx.
    constructor; auto. eapply siexec_inst_preserves_allfu; eauto.
Qed.

Lemma siexec_path_preserves_sabort ge sp path f rs0 m0 st': forall st, 
  siexec_path path f st = Some st' ->
  sabort ge sp st rs0 m0 -> sabort ge sp st' rs0 m0.
Proof.
  Local Hint Resolve siexec_inst_preserves_sabort: core.
  induction path; simpl.
  + unfold sist_set_local; try_simplify_someHyps.
  + intros st; inversion_SOME i.
    inversion_SOME st1; eauto.
Qed.

Lemma siexec_path_WF path f: forall st,
  siexec_path path f st = None -> nth_default_succ (fn_code f) path st.(si_pc) = None.
Proof.
  induction path; simpl.
  + unfold sist_set_local. intuition congruence.
  + intros st; destruct ((fn_code f) ! (si_pc st)); simpl; try tauto.
    destruct (siexec_inst i st) as [st1|] eqn: Hst1; simpl.
    - intros; erewrite siexec_inst_default_succ; eauto.
    - intros; erewrite siexec_inst_WF; eauto.
Qed.

Lemma siexec_path_default_succ path f st': forall st,
  siexec_path path f st = Some st' -> nth_default_succ (fn_code f) path st.(si_pc) = Some st'.(si_pc).
Proof.
  induction path; simpl.
  + unfold sist_set_local. intros st H. inversion_clear H; simpl; try congruence.
  + intros st; destruct ((fn_code f) ! (si_pc st)); simpl; try congruence.
    destruct (siexec_inst i st) as [st1|] eqn: Hst1; simpl; try congruence.
    intros; erewrite siexec_inst_default_succ; eauto.
Qed.

Lemma siexec_path_correct_true ge sp path (f:function) rs0 m0: forall st is,
  is.(icontinue)=true ->
  ssem_internal ge sp st rs0 m0 is -> 
  nth_default_succ (fn_code f) path st.(si_pc) <> None ->
  ssem_internal_opt2 ge sp (siexec_path path f st) rs0 m0
                         (isteps ge path f sp is.(irs) is.(imem) is.(ipc))
  .
Proof.
  Local Hint Resolve siexec_path_correct_false siexec_path_preserves_sabort siexec_path_WF: core.
  induction path; simpl.
  + intros st is CONT INV WF;
    unfold ssem_internal, sist_set_local in * |- *;
    try_simplify_someHyps. simpl.
    destruct is; simpl in * |- *; subst; intuition auto.
  + intros st is CONT; unfold ssem_internal at 1; rewrite CONT.
    intros (LOCAL & PC & NYE) WF.
    rewrite <- PC.
    inversion_SOME i; intro Hi; rewrite Hi in WF |- *; simpl; auto.
    exploit siexec_inst_correct; eauto. 
    inversion_SOME st1; intros Hst1; erewrite Hst1; simpl.
    - inversion_SOME is1; intros His1;rewrite His1; simpl. 
      * destruct (icontinue is1) eqn:CONT1.
        (* icontinue is0 = true *)
        intros; eapply IHpath; eauto.
        destruct i; simpl in * |- *; unfold sist_set_local in * |- *; try_simplify_someHyps.
        (* icontinue is0 = false -> EARLY EXIT *)
        destruct (siexec_path path f st1) as [st2|] eqn: Hst2; simpl; eauto.
        destruct WF. erewrite siexec_inst_default_succ; eauto.
        (* try_simplify_someHyps; eauto. *)
      * destruct (siexec_path path f st1) as [st2|] eqn: Hst2; simpl; eauto.
    - intros His1;rewrite His1; simpl; auto.
Qed.

(** REM: in the following two unused lemmas *)

Lemma siexec_path_right_assoc_decompose f path: forall st st',
  siexec_path (S path) f st = Some st' ->
  exists st0, siexec_path path f st = Some st0 /\ siexec_path 1%nat f st0 = Some st'.
Proof.
  induction path; simpl; eauto.
  intros st st'.
  inversion_SOME i1.
  inversion_SOME st1.
  try_simplify_someHyps; eauto.
Qed.

Lemma siexec_path_right_assoc_compose f path: forall st st0 st',
  siexec_path path f st = Some st0 ->
  siexec_path 1%nat f st0 = Some st' ->
  siexec_path (S path) f st = Some st'.
Proof.
  induction path.
  + intros st st0 st' H. simpl in H.
    try_simplify_someHyps; auto.
  + intros st st0 st'.
    assert (X:exists x, x=(S path)); eauto.
    destruct X as [x X]. 
    intros H1 H2. rewrite <- X.
    generalize H1; clear H1. simpl.
    inversion_SOME i1. intros Hi1; rewrite Hi1.
    inversion_SOME st1. intros Hst1; rewrite Hst1.
    subst; eauto.
Qed.

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

Definition sfind_function (pge: RTLpath.genv) (ge: RTL.genv) (sp: val) (svos : sval + ident) (rs0: regset) (m0: mem): option fundef :=
  match svos with
  | inl sv => SOME v <- seval_sval ge sp sv rs0 m0 IN Genv.find_funct pge v
  | inr symb => SOME b <- Genv.find_symbol pge symb IN Genv.find_funct_ptr pge b
  end.

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

Variable ge: RTL.genv.
Variable sp: val.
Variable m: mem.
Variable rs0: regset.
Variable m0: mem.

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

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

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

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

End SEVAL_BUILTIN_ARG.

Inductive ssem_final (pge: RTLpath.genv) (ge: RTL.genv) (sp:val) (npc: node) stack (f: function) (rs0: regset) (m0: mem): sfval -> regset -> mem -> trace -> state -> Prop :=
  | exec_Snone rs m:
      ssem_final pge ge sp npc stack f rs0 m0 Snone rs m E0 (State stack f sp npc rs m)
  | exec_Scall rs m sig svos lsv args res pc fd:
      sfind_function pge ge sp svos rs0 m0 = Some fd ->
      funsig fd = sig ->
      seval_list_sval ge sp lsv rs0 m0 = Some args ->
      ssem_final pge ge sp npc stack f rs0 m0 (Scall sig svos lsv res pc) rs m
        E0 (Callstate (Stackframe res f sp pc rs :: stack) fd args m)
  | exec_Stailcall stk rs m sig svos args fd m' lsv:
      sfind_function pge ge sp svos rs0 m0 = Some fd ->
      funsig fd = sig ->
      sp = Vptr stk Ptrofs.zero ->
      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
      seval_list_sval ge sp lsv rs0 m0 = Some args ->
      ssem_final pge ge sp npc stack f rs0 m0 (Stailcall sig svos lsv) rs m
        E0 (Callstate stack fd args m')
  | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs:
      seval_builtin_args ge sp m rs0 m0 sargs vargs ->
      external_call ef ge vargs m t vres m' ->
      ssem_final pge ge sp npc stack f rs0 m0 (Sbuiltin ef sargs res pc) rs m
        t (State stack f sp pc (regmap_setres res vres rs) m')
  | exec_Sjumptable sv tbl pc' n rs m:
      seval_sval ge sp sv rs0 m0 = Some (Vint n) ->
      list_nth_z tbl (Int.unsigned n) = Some pc' ->
      ssem_final pge ge sp npc stack f rs0 m0 (Sjumptable sv tbl) rs m
        E0 (State stack f sp pc' rs m)
  | exec_Sreturn stk osv rs m m' v:
      sp = (Vptr stk Ptrofs.zero) ->
      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
      match osv with Some sv => seval_sval ge sp sv rs0 m0 | None => Some Vundef end = Some v ->
      ssem_final pge ge sp npc stack f rs0 m0 (Sreturn osv) rs m 
         E0 (Returnstate stack v m')
.

Record sstate := { internal:> sistate; final: sfval }.

Inductive ssem pge (ge: RTL.genv) (sp:val) (st: sstate) stack f (rs0: regset) (m0: mem): trace -> state -> Prop :=
  | ssem_early is:
     is.(icontinue) = false ->
     ssem_internal ge sp st rs0 m0 is -> 
     ssem pge ge sp st stack f rs0 m0 E0 (State stack f sp is.(ipc) is.(irs) is.(imem))
  | ssem_normal is t s:
     is.(icontinue) = true ->
     ssem_internal ge sp st rs0 m0 is ->  
     ssem_final pge ge sp st.(si_pc) stack f rs0 m0 st.(final) is.(irs) is.(imem) t s ->
     ssem pge ge sp st stack f rs0 m0 t s 
  .

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

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

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

Lemma seval_builtin_arg_complete ge sp rs m rs0 m0 sreg: forall arg varg,
  (forall r, seval_sval ge sp (sreg r) rs0 m0 = Some rs # r) ->
  seval_builtin_arg ge sp m rs0 m0 (builtin_arg_map sreg arg) varg ->
  eval_builtin_arg ge (fun r => rs # r) sp m arg varg.
Proof.
  induction arg.
  all: intros varg SEVAL BARG; try (inv BARG; constructor; congruence).
  - inv BARG. rewrite SEVAL in H0. inv H0. constructor.
  - inv BARG. simpl. constructor.
    eapply IHarg1; eauto. eapply IHarg2; eauto.
  - inv BARG. simpl. constructor.
    eapply IHarg1; eauto. eapply IHarg2; eauto.
Qed.

Lemma seval_builtin_args_complete ge sp rs m rs0 m0 sreg: forall args vargs,
  (forall r, seval_sval ge sp (sreg r) rs0 m0 = Some rs # r) ->
  seval_builtin_args ge sp m rs0 m0 (map (builtin_arg_map sreg) args) vargs ->
  eval_builtin_args ge (fun r => rs # r) sp m args vargs.
Proof.
  induction args.
  - simpl. intros. inv H0. constructor.
  - intros vargs SEVAL BARG. simpl in BARG. inv BARG.
    constructor; [| eapply IHargs; eauto].
    eapply seval_builtin_arg_complete; eauto.
Qed.

(** * Symbolic execution of final step *)
Definition sexec_final (i: instruction) (prev: sistate_local): sfval := 
  match i with
  | Icall sig ros args res pc => 
    let svos := sum_left_map prev.(si_sreg) ros in
    let sargs := list_sval_inj (List.map prev.(si_sreg) args) in
    Scall sig svos sargs res pc
  | Itailcall sig ros args =>
    let svos := sum_left_map prev.(si_sreg) ros in
    let sargs := list_sval_inj (List.map prev.(si_sreg) args) in
    Stailcall sig svos sargs
  | Ibuiltin ef args res pc =>
    let sargs := List.map (builtin_arg_map prev.(si_sreg)) args in
    Sbuiltin ef sargs res pc
  | Ireturn or => 
    let sor := SOME r <- or IN Some (prev.(si_sreg) r) in
    Sreturn sor
  | Ijumptable reg tbl =>
    let sv := prev.(si_sreg) reg in
    Sjumptable sv tbl
  | _ => Snone
  end.

Lemma sexec_final_correct pge ge sp i (f:function) pc st stack rs0 m0 t rs m s:
  (fn_code f) ! pc = Some i ->
  pc = st.(si_pc) ->
  ssem_local ge sp (si_local st) rs0 m0 rs m ->
  path_last_step ge pge stack f sp pc rs m t s ->
  siexec_inst i st = None -> 
  ssem_final pge ge sp pc stack f rs0 m0 (sexec_final i (si_local st)) rs m t s.
Proof.
  intros PC1 PC2 (PRE&MEM&REG) LAST. destruct LAST; subst; try_simplify_someHyps; simpl.
  + (* Snone *) intro Hi; destruct i; simpl in Hi |- *; unfold sist_set_local in Hi; try congruence.
  + (* Icall *) intros; eapply exec_Scall; auto.
    - destruct ros; simpl in * |- *; auto.
      rewrite REG; auto.
    - erewrite seval_list_sval_inj; simpl; auto.
  + (* Itailcall *) intros. eapply exec_Stailcall; auto.
    - destruct ros; simpl in * |- *; auto.
      rewrite REG; auto.
    - erewrite seval_list_sval_inj; simpl; auto.
  + (* Ibuiltin *) intros. eapply exec_Sbuiltin; eauto.
    eapply seval_builtin_args_correct; eauto.
  + (* Ijumptable *) intros. eapply exec_Sjumptable; eauto. congruence.
  + (* Ireturn *) intros; eapply exec_Sreturn; simpl; eauto.
    destruct or; simpl; auto.
Qed.

Lemma sexec_final_complete i (f:function) pc st ge pge sp stack rs0 m0 t rs m s:
  (fn_code f) ! pc = Some i ->
  pc = st.(si_pc) ->
  ssem_local ge sp (si_local st) rs0 m0 rs m ->
  ssem_final pge ge sp pc stack f rs0 m0 (sexec_final i (si_local st)) rs m t s ->
  siexec_inst i st = None -> 
  path_last_step ge pge stack f sp pc rs m t s.
Proof.
  intros PC1 PC2 (PRE&MEM&REG) LAST HSIS.
  destruct i as [ (* Inop *) | (* Iop *) | (* Iload *) | (* Istore *)
    | (* Icall *) sig ros args res pc'
    | (* Itailcall *) sig ros args
    | (* Ibuiltin *) ef bargs br pc'
    | (* Icond *)
    | (* Ijumptable *) jr tbl
    | (*Ireturn*) or]; 
    subst; try_simplify_someHyps; try (unfold sist_set_local in HSIS; try congruence);
    inversion LAST; subst; clear LAST; simpl in * |- *.
  + (* Icall *)
    erewrite seval_list_sval_inj in * |- ; simpl; try_simplify_someHyps; auto.
    intros; eapply exec_Icall; eauto.
    destruct ros; simpl in * |- *; auto.
    rewrite REG in * |- ; auto.
  + (* Itailcall *)
    intros HPC SMEM. erewrite seval_list_sval_inj in H10; auto. inv H10. 
    eapply exec_Itailcall; eauto.
    destruct ros; simpl in * |- *; auto.
    rewrite REG in * |- ; auto.
  + (* Ibuiltin *) intros HPC SMEM.
    eapply exec_Ibuiltin; eauto.
    eapply seval_builtin_args_complete; eauto.
  + (* Ijumptable *) intros HPC SMEM.
    eapply exec_Ijumptable; eauto.
    congruence.
  + (* Ireturn *)
    intros; subst. enough (v=regmap_optget or Vundef rs) as ->.
    * eapply exec_Ireturn; eauto.
    * intros; destruct or; simpl; congruence.
Qed.

(** * Main function of the symbolic execution *)

Definition init_sistate_local := {| si_pre:= fun _ _ _ _ => True; si_sreg:= fun r => Sinput r; si_smem:= Sinit |}.

Definition init_sistate pc := {| si_pc:= pc; si_exits:=nil; si_local:= init_sistate_local |}.

Lemma init_ssem_internal ge sp pc rs m: ssem_internal ge sp (init_sistate pc) rs m (mk_istate true pc rs m).
Proof.
  unfold ssem_internal, ssem_local, all_fallthrough; simpl. intuition.
Qed.

Definition sexec (f: function) (pc:node): option sstate :=
  SOME path <- (fn_path f)!pc IN
  SOME st <- siexec_path path.(psize) f (init_sistate pc) IN
  SOME i <- (fn_code f)!(st.(si_pc)) IN
  Some (match siexec_inst i st with
       | Some st' => {| internal := st'; final := Snone |}
       | None => {| internal := st; final := sexec_final i st.(si_local) |}
       end).

Lemma final_node_path_simpl f path pc:
   (fn_path f)!pc = Some path -> nth_default_succ_inst (fn_code f) path.(psize) pc <> None. 
Proof.
  intros; exploit final_node_path; eauto.
  intros (i & NTH & DUM).
  congruence.
Qed.

Lemma symb_path_last_step i st st' ge pge stack (f:function) sp pc rs m t s: 
  (fn_code f) ! pc = Some i ->
  pc = st.(si_pc) ->
  siexec_inst i st = Some st' ->
  path_last_step ge pge stack f sp pc rs m t s ->
  exists mk_istate, 
     istep ge i sp rs m = Some mk_istate 
  /\ t = E0 
  /\ s = (State stack f sp mk_istate.(ipc) mk_istate.(RTLpath.irs) mk_istate.(imem)).
Proof.
  intros PC1 PC2 Hst' LAST; destruct LAST; subst; try_simplify_someHyps; simpl.
Qed.

(* NB: each concrete execution can be executed on the symbolic state (produced from [sexec]) 
(sexec is a correct over-approximation)
*)
Theorem sexec_correct f pc pge ge sp path stack rs m t s: 
  (fn_path f)!pc = Some path ->
  path_step ge pge path.(psize) stack f sp rs m pc t s ->
  exists st, sexec f pc = Some st /\ ssem pge ge sp st stack f rs m t s.
Proof.
  Local Hint Resolve init_ssem_internal: core.
  intros PATH STEP; unfold sexec; rewrite PATH; simpl.
  lapply (final_node_path_simpl f path pc); eauto. intro WF.
  exploit (siexec_path_correct_true ge sp path.(psize) f rs m (init_sistate pc) (mk_istate true pc rs m)); simpl; eauto.
  { intros ABS. apply WF; unfold nth_default_succ_inst. rewrite ABS; auto. }
  (destruct (nth_default_succ_inst (fn_code f) path.(psize) pc) as [i|] eqn: Hi; [clear WF|congruence]).
  destruct STEP as [sti STEPS CONT|sti t s STEPS CONT LAST];
  (* intro Hst *)
  (rewrite STEPS; unfold ssem_internal_opt2; destruct (siexec_path _ _ _) as [st|] eqn: Hst; try congruence);
  (* intro SEM *)
  (simpl; unfold ssem_internal; simpl; rewrite CONT; intro SEM);
  (* intro Hi' *)
  ( assert (Hi': (fn_code f) ! (si_pc st) = Some i); 
    [ unfold nth_default_succ_inst in Hi; 
      exploit siexec_path_default_succ; eauto; simpl;
      intros DEF; rewrite DEF in Hi; auto 
      | clear Hi; rewrite Hi' ]);
  (* eexists *)
  (eexists; constructor; eauto).
  - (* early *)
    eapply ssem_early; eauto.
    unfold ssem_internal; simpl; rewrite CONT.
    destruct (siexec_inst i st) as [st'|] eqn: Hst'; simpl; eauto.
    destruct SEM as (ext & lx & SEM & ALLFU). exists ext, lx.
    constructor; auto. eapply siexec_inst_preserves_allfu; eauto.
  - destruct SEM as (SEM & PC & HNYE).
    destruct (siexec_inst i st) as [st'|] eqn: Hst'; simpl.
    + (* normal on Snone *)
      rewrite <- PC in LAST.
      exploit symb_path_last_step; eauto; simpl.
      intros (mk_istate & ISTEP & Ht & Hs); subst.
      exploit siexec_inst_correct; eauto. simpl.
      erewrite Hst', ISTEP; simpl.
      clear LAST CONT STEPS PC SEM HNYE Hst Hi' Hst' ISTEP st sti i.
      intro SEM; destruct (mk_istate.(icontinue)) eqn: CONT.
      { (* icontinue mk_istate = true *)
        eapply ssem_normal; simpl; eauto.
        unfold ssem_internal in SEM.
        rewrite CONT in SEM.
        destruct SEM as (SEM & PC & HNYE).
        rewrite <- PC.
        eapply exec_Snone. }
      { eapply ssem_early; eauto. }
    + (* normal non-Snone instruction *) 
      eapply ssem_normal; eauto.
      * unfold ssem_internal; simpl; rewrite CONT; intuition.
      * simpl. eapply sexec_final_correct; eauto.
        rewrite PC; auto.
Qed.

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

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

Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf.
Proof.
  destruct stf. constructor; auto.
Qed.

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

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

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

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

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

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

Lemma ssem_final_equiv pge ge sp (f:function) st sv stack rs0 m0 t rs1 rs2 m s:
  ssem_final pge ge sp st stack f rs0 m0 sv rs1 m t s ->
  (forall r, rs1#r = rs2#r) -> 
  exists s', equiv_state s s' /\ ssem_final pge ge sp st stack f rs0 m0 sv rs2 m t s'.
Proof. 
  Local Hint Resolve equiv_stack_refl: core.
  destruct 1.
  - (* Snone *) intros; eexists; econstructor.
    + eapply State_equiv; eauto.
    + eapply exec_Snone.
  - (* Scall *)
    intros; eexists; econstructor.
    2: { eapply exec_Scall; eauto. }
    apply Call_equiv; auto.
    repeat (constructor; auto).
  - (* Stailcall *)
    intros; eexists; econstructor; [| eapply exec_Stailcall; eauto].
    apply Call_equiv; auto.
  - (* Sbuiltin *)
    intros; eexists; econstructor; [| eapply exec_Sbuiltin; eauto].
    constructor. eapply regmap_setres_eq; eauto.
  - (* Sjumptable *)
    intros; eexists; econstructor; [| eapply exec_Sjumptable; eauto].
    constructor. assumption.
  - (* Sreturn *)
    intros; eexists; econstructor; [| eapply exec_Sreturn; eauto].
    eapply equiv_state_refl; eauto.
Qed.

Lemma siexec_inst_early_exit_absurd i st st' ge sp rs m rs' m' pc':
  siexec_inst i st = Some st' ->
  (exists ext lx, ssem_exit ge sp ext rs m rs' m' pc' /\
     all_fallthrough_upto_exit ge sp ext lx (si_exits st) rs m) ->
  all_fallthrough ge sp (si_exits st') rs m ->
  False.
Proof.
  intros SIEXEC (ext & lx & SSEME & ALLFU) ALLF. destruct ALLFU as (TAIL & _).
  exploit siexec_inst_add_exits; eauto. destruct 1 as [SIEQ | (ext0 & SIEQ)].
  - rewrite SIEQ in *. eapply all_fallthrough_noexit. eauto. 2: eapply ALLF. eapply is_tail_in. eassumption.
  - rewrite SIEQ in *. eapply all_fallthrough_noexit. eauto. 2: eapply ALLF. eapply is_tail_in.
    constructor. eassumption.
Qed.

Lemma is_tail_false {A: Type}: forall (l: list A) a, is_tail (a::l) nil -> False.
Proof.
  intros. eapply is_tail_incl in H. unfold incl in H. pose (H a).
  assert (In a (a::l)) by (constructor; auto). assert (In a nil) by auto. apply in_nil in H1.
  contradiction.
Qed.

Lemma cons_eq_false {A: Type}: forall (l: list A) a,
  a :: l = l -> False.
Proof.
  induction l; intros.
  - discriminate.
  - inv H. apply IHl in H2. contradiction.
Qed.

Lemma app_cons_nil_eq {A: Type}: forall l' l (a:A),
  (l' ++ a :: nil) ++ l = l' ++ a::l.
Proof.
  induction l'; intros.
  - simpl. reflexivity.
  - simpl. rewrite IHl'. reflexivity. 
Qed.

Lemma app_eq_false {A: Type}: forall l (l': list A) a,
  l' ++ a :: l = l -> False.
Proof.
  induction l; intros.
  - apply app_eq_nil in H. destruct H as (_ & H). apply cons_eq_false in H. contradiction.
  - destruct l' as [|a' l'].
    + simpl in H. apply cons_eq_false in H. contradiction.
    + rewrite <- app_comm_cons in H. inv H.
      apply (IHl (l' ++ (a0 :: nil)) a). rewrite app_cons_nil_eq. assumption.
Qed.

Lemma is_tail_false_gen {A: Type}: forall (l: list A) l' a, is_tail (l'++(a::l)) l -> False.
Proof.
  induction l.
  - intros. destruct l' as [|a' l'].
    + simpl in H. apply is_tail_false in H. contradiction.
    + rewrite <- app_comm_cons in H. apply is_tail_false in H. contradiction.
  - intros. inv H.
    + apply app_eq_false in H2. contradiction.
    + apply (IHl (l' ++ (a0 :: nil)) a). rewrite app_cons_nil_eq. assumption.
Qed.

Lemma is_tail_eq {A: Type}: forall (l l': list A),
  is_tail l' l ->
  is_tail l l' ->
  l = l'.
Proof.
  destruct l as [|a l]; intros l' ITAIL ITAIL'.
  - destruct l' as [|i' l']; auto. apply is_tail_false in ITAIL. contradiction.
  - inv ITAIL; auto.
    destruct l' as [|i' l']. { apply is_tail_false in ITAIL'. contradiction. }
    exploit is_tail_trans. eapply ITAIL'. eauto. intro ABSURD.
    apply (is_tail_false_gen l nil a) in ABSURD. contradiction.
Qed.

(* NB: each execution of a symbolic state (produced from [sexec]) represents a concrete execution
  (sexec is exact).
*)
Theorem sexec_exact f pc pge ge sp path stack st rs m t s1: 
  (fn_path f)!pc = Some path ->
  sexec f pc = Some st -> 
  ssem pge ge sp st stack f rs m t s1 ->
  exists s2, path_step ge pge path.(psize) stack f sp rs m pc t s2 /\ 
             equiv_state s1 s2.
Proof.
  Local Hint Resolve init_ssem_internal: core.
  unfold sexec; intros PATH SSTEP SEM; rewrite PATH in SSTEP.
  lapply (final_node_path_simpl f path pc); eauto. intro WF.
  exploit (siexec_path_correct_true ge sp path.(psize) f rs m (init_sistate pc) (mk_istate true pc rs m)); simpl; eauto.
  { intros ABS. apply WF; unfold nth_default_succ_inst. rewrite ABS; auto. }
  (destruct (nth_default_succ_inst (fn_code f) path.(psize) pc) as [i|] eqn: Hi; [clear WF|congruence]).
  unfold nth_default_succ_inst in Hi.
  destruct (siexec_path path.(psize) f (init_sistate pc)) as [st0|] eqn: Hst0; simpl.
  2:{ (* absurd case *)
      exploit siexec_path_WF; eauto.
      simpl; intros NDS; rewrite NDS in Hi; congruence. }
  exploit siexec_path_default_succ; eauto; simpl.
  intros NDS; rewrite NDS in Hi.
  rewrite Hi in SSTEP.
  intros ISTEPS. try_simplify_someHyps.
  destruct (siexec_inst i st0) as [st'|] eqn:Hst'; simpl.
  + (* exit on Snone instruction *)
    assert (SEM': t = E0 /\ exists is, ssem_internal ge sp st' rs m is
           /\ s1 = (State stack f sp (if (icontinue is) then (si_pc st') else (ipc is)) (irs is) (imem is))).
    {  destruct SEM as [is CONT SEM|is t s CONT SEM1 SEM2]; simpl in * |- *.
       - repeat (econstructor; eauto).
         rewrite CONT; eauto.
       - inversion SEM2. repeat (econstructor; eauto).
         rewrite CONT; eauto. }
    clear SEM; subst. destruct SEM' as [X (is & SEM & X')]; subst.
    intros.
    destruct (isteps ge (psize path) f sp rs m pc) as [is0|] eqn:RISTEPS; simpl in *.
    * unfold ssem_internal in ISTEPS. destruct (icontinue is0) eqn: ICONT0. 
      ** (* icontinue is0=true: path_step by normal_exit *)
         destruct ISTEPS as (SEMis0&H1&H2).
         rewrite H1 in * |-.
         exploit siexec_inst_correct; eauto.
         rewrite Hst'; simpl.
         intros; exploit ssem_internal_opt_determ; eauto.
         destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4).
         eexists. econstructor 1.
         *** eapply exec_normal_exit; eauto.
             eapply exec_istate; eauto.
         *** rewrite EQ1.
             enough ((ipc st) = (if icontinue st then si_pc st' else ipc is)) as ->.
             { rewrite EQ2, EQ4. eapply State_equiv; auto. }
             destruct (icontinue st) eqn:ICONT; auto.
             exploit siexec_inst_default_succ; eauto.
             erewrite istep_normal_exit; eauto.
             try_simplify_someHyps.
      ** (* The concrete execution has not reached "i" => early exit *) 
         unfold ssem_internal in SEM.
         destruct (icontinue is) eqn:ICONT.
         { destruct SEM as (SEML & SIPC & ALLF).
           exploit siexec_inst_early_exit_absurd; eauto. contradiction. }
         
         eexists. econstructor 1.
         *** eapply exec_early_exit; eauto.
         *** destruct ISTEPS as (ext & lx & SSEME & ALLFU). destruct SEM as (ext' & lx' & SSEME' & ALLFU').
             eapply siexec_inst_preserves_allfu in ALLFU; eauto.
             exploit ssem_exit_fallthrough_upto_exit; eauto.
             exploit ssem_exit_fallthrough_upto_exit. eapply SSEME. eapply ALLFU. eapply ALLFU'.
             intros ITAIL ITAIL'. apply is_tail_eq in ITAIL; auto. clear ITAIL'.
             inv ITAIL. exploit ssem_exit_determ. eapply SSEME. eapply SSEME'. intros (IPCEQ & IRSEQ & IMEMEQ).
             rewrite <- IPCEQ. rewrite <- IMEMEQ. constructor. congruence. 
    * (* The concrete execution has not reached "i" => abort case *)
      eapply siexec_inst_preserves_sabort in ISTEPS; eauto.
      exploit ssem_internal_exclude_sabort; eauto. contradiction.
  + destruct SEM as [is CONT SEM|is t s CONT SEM1 SEM2]; simpl in * |- *.
    - (* early exit *)
      intros.
      exploit ssem_internal_opt_determ; eauto.
      destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4).
      eexists. econstructor 1.
      * eapply exec_early_exit; eauto.
      * rewrite EQ2, EQ4; eapply State_equiv. auto.
    - (* normal exit non-Snone instruction *)
      intros.
      exploit ssem_internal_opt_determ; eauto.
      destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4).
      unfold ssem_internal in SEM1.
      rewrite CONT in SEM1. destruct SEM1 as (SEM1 & PC0 & NYE0).
      exploit ssem_final_equiv; eauto.
      clear SEM2; destruct 1 as (s' & Ms' & SEM2).
      rewrite ! EQ4 in * |-; clear EQ4.
      rewrite ! EQ2 in * |-; clear EQ2.
      exists s'; intuition.
      eapply exec_normal_exit; eauto.
      eapply sexec_final_complete; eauto.
      * congruence.
      * unfold ssem_local in * |- *. 
        destruct SEM1 as (A & B & C). constructor; [|constructor]; eauto.
        intro r. congruence.
      * congruence.
Qed.

(** * Simulation of RTLpath code w.r.t symbolic execution *)

Section SymbValPreserved.

Variable ge ge': RTL.genv.

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

Hypothesis senv_preserved_RTL: Senv.equiv ge ge'.

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

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

Lemma seval_preserved sp sv rs0 m0:
  seval_sval ge sp sv rs0 m0 = seval_sval ge' sp sv rs0 m0.
Proof.
  Local Hint Resolve symbols_preserved_RTL: core.
  induction sv using sval_mut with (P0 := fun lsv => seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv rs0 m0)
                                   (P1 := fun sm => seval_smem ge sp sm rs0 m0 = seval_smem ge' sp sm rs0 m0); simpl; auto.
  + rewrite IHsv; clear IHsv. destruct (seval_list_sval _ _ _ _); auto.
    rewrite IHsv0; clear IHsv0. destruct (seval_smem _ _ _ _); auto.
    erewrite eval_operation_preserved; eauto.
  + rewrite IHsv0; clear IHsv0. destruct (seval_list_sval _ _ _ _); auto.
    erewrite <- eval_addressing_preserved; eauto.
    destruct (eval_addressing _ sp _ _); auto.
    rewrite IHsv; auto.
  + rewrite IHsv; clear IHsv. destruct (seval_sval _ _ _ _); auto.
    rewrite IHsv0; auto.
  + rewrite IHsv0; clear IHsv0. destruct (seval_list_sval _ _ _ _); auto.
    erewrite <- eval_addressing_preserved; eauto.
    destruct (eval_addressing _ sp _ _); auto.
    rewrite IHsv; clear IHsv. destruct (seval_smem _ _ _ _); auto.
    rewrite IHsv1; auto.
Qed.

Lemma seval_builtin_arg_preserved sp m rs0 m0:
  forall bs varg,
  seval_builtin_arg ge sp m rs0 m0 bs varg ->
  seval_builtin_arg ge' sp m rs0 m0 bs varg.
Proof.
  induction 1.
  all: try (constructor; auto).
  - rewrite <- seval_preserved. assumption.
  - rewrite <- senv_symbol_address_preserved. assumption.
  - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal.
Qed.

Lemma seval_builtin_args_preserved sp m rs0 m0 lbs vargs:
  seval_builtin_args ge sp m rs0 m0 lbs vargs ->
  seval_builtin_args ge' sp m rs0 m0 lbs vargs.
Proof.
  induction 1; constructor; eauto.
  eapply seval_builtin_arg_preserved; auto.
Qed.

Lemma list_sval_eval_preserved sp lsv rs0 m0: 
  seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv rs0 m0.
Proof.
  induction lsv; simpl; auto.
  rewrite seval_preserved. destruct (seval_sval _ _ _ _); auto.
  rewrite IHlsv; auto.
Qed.

Lemma smem_eval_preserved sp sm rs0 m0: 
  seval_smem ge sp sm rs0 m0 = seval_smem ge' sp sm rs0 m0.
Proof.
  induction sm; simpl; auto.
  rewrite list_sval_eval_preserved. destruct (seval_list_sval _ _ _ _); auto.
  erewrite <- eval_addressing_preserved; eauto.
  destruct (eval_addressing _ sp _ _); auto.
  rewrite IHsm; clear IHsm. destruct (seval_smem _ _ _ _); auto.
  rewrite seval_preserved; auto.
Qed.

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

End SymbValPreserved.

Require Import RTLpathLivegen RTLpathLivegenproof.

(** * DEFINITION OF SIMULATION BETWEEN (ABSTRACT) SYMBOLIC EXECUTIONS
*)

Definition istate_simulive alive (srce: PTree.t node) (is1 is2: istate): Prop :=
     is1.(icontinue) = is2.(icontinue)
     /\ eqlive_reg alive is1.(irs) is2.(irs)
     /\ is1.(imem) = is2.(imem).

Definition istate_simu f (srce: PTree.t node) outframe is1 is2: Prop :=
  if is1.(icontinue) then
     istate_simulive (fun r => Regset.In r outframe) srce is1 is2
  else
     exists path, f.(fn_path)!(is1.(ipc)) = Some path 
     /\ istate_simulive (fun r => Regset.In r path.(input_regs)) srce is1 is2
     /\ srce!(is2.(ipc)) = Some is1.(ipc).

Record simu_proof_context {f1: RTLpath.function} := {
   liveness_hyps: liveness_ok_function f1;
   the_ge1: RTL.genv;
   the_ge2: RTL.genv;
   genv_match: forall s, Genv.find_symbol the_ge1 s = Genv.find_symbol the_ge2 s;
   the_sp: val;
   the_rs0: regset; 
   the_m0: mem
}.
Arguments simu_proof_context: clear implicits.

(* NOTE: a pure semantic definition on [sistate], for a total freedom in refinements *)
Definition sistate_simu (dm: PTree.t node) (f: RTLpath.function) outframe (st1 st2: sistate) (ctx: simu_proof_context f): Prop :=
  forall is1, ssem_internal (the_ge1 ctx) (the_sp ctx) st1 (the_rs0 ctx) (the_m0 ctx) is1 ->
  exists is2, ssem_internal (the_ge2 ctx) (the_sp ctx) st2 (the_rs0 ctx) (the_m0 ctx) is2
              /\ istate_simu f dm outframe is1 is2.

Inductive svident_simu (f: RTLpath.function) (ctx: simu_proof_context f): (sval + ident) -> (sval + ident) -> Prop :=
  | Sleft_simu sv1 sv2:
     (seval_sval (the_ge1 ctx) (the_sp ctx) sv1 (the_rs0 ctx) (the_m0 ctx)) = (seval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx))
     -> svident_simu f ctx (inl sv1) (inl sv2)
  | Sright_simu id1 id2:
     id1 = id2
     -> svident_simu f ctx (inr id1) (inr id2)
  .


Fixpoint ptree_get_list (pt: PTree.t node) (lp: list positive) : option (list positive) :=
  match lp with
  | nil => Some nil
  | p1::lp => SOME p2 <- pt!p1 IN
              SOME lp2 <- (ptree_get_list pt lp) IN
              Some (p2 :: lp2)
  end.

Lemma ptree_get_list_nth dm p2: forall lp2 lp1,
  ptree_get_list dm lp2 = Some lp1 ->
  forall n, list_nth_z lp2 n = Some p2 ->
  exists p1,
    list_nth_z lp1 n = Some p1 /\ dm ! p2 = Some p1.
Proof.
  induction lp2.
  - simpl. intros. inv H. simpl in *. discriminate.
  - intros lp1 PGL n LNZ. simpl in PGL. explore.
    inv LNZ. destruct (zeq n 0) eqn:ZEQ.
    + subst. inv H0. exists n0. simpl; constructor; auto.
    + exploit IHlp2; eauto. intros (p1 & LNZ & DMEQ).
      eexists. simpl. rewrite ZEQ.
      constructor; eauto.
Qed.

Lemma ptree_get_list_nth_rev dm p1: forall lp2 lp1,
  ptree_get_list dm lp2 = Some lp1 ->
  forall n, list_nth_z lp1 n = Some p1 ->
  exists p2,
    list_nth_z lp2 n = Some p2 /\ dm ! p2 = Some p1.
Proof.
  induction lp2.
  - simpl. intros. inv H. simpl in *. discriminate.
  - intros lp1 PGL n LNZ. simpl in PGL. explore.
    inv LNZ. destruct (zeq n 0) eqn:ZEQ.
    + subst. inv H0. exists a. simpl; constructor; auto.
    + exploit IHlp2; eauto. intros (p2 & LNZ & DMEQ).
      eexists. simpl. rewrite ZEQ.
      constructor; eauto. congruence.
Qed.

Fixpoint seval_builtin_sval ge sp bsv rs0 m0 :=
  match bsv with
  | BA sv => SOME v <- seval_sval ge sp sv rs0 m0 IN Some (BA v)
  | BA_splitlong sv1 sv2 =>
      SOME v1 <- seval_builtin_sval ge sp sv1 rs0 m0 IN
      SOME v2 <- seval_builtin_sval ge sp sv2 rs0 m0 IN
      Some (BA_splitlong v1 v2)
  | BA_addptr sv1 sv2 =>
      SOME v1 <- seval_builtin_sval ge sp sv1 rs0 m0 IN
      SOME v2 <- seval_builtin_sval ge sp sv2 rs0 m0 IN
      Some (BA_addptr v1 v2)
  | BA_int i => Some (BA_int i)
  | BA_long l => Some (BA_long l)
  | BA_float f => Some (BA_float f)
  | BA_single s => Some (BA_single s)
  | BA_loadstack chk ptr => Some (BA_loadstack chk ptr)
  | BA_addrstack ptr => Some (BA_addrstack ptr)
  | BA_loadglobal chk id ptr => Some (BA_loadglobal chk id ptr)
  | BA_addrglobal id ptr => Some (BA_addrglobal id ptr)
  end.


Fixpoint seval_list_builtin_sval ge sp lbsv rs0 m0 :=
  match lbsv with
  | nil => Some nil
  | bsv::lbsv => SOME v <- seval_builtin_sval ge sp bsv rs0 m0 IN
                 SOME lv <- seval_list_builtin_sval ge sp lbsv rs0 m0 IN
                 Some (v::lv)
  end.

Lemma seval_list_builtin_sval_nil ge sp rs0 m0 lbs2:
  seval_list_builtin_sval ge sp lbs2 rs0 m0 = Some nil ->
  lbs2 = nil.
Proof.
  destruct lbs2; simpl; auto.
  intros. destruct (seval_builtin_sval _ _ _ _ _);
    try destruct (seval_list_builtin_sval _ _ _ _ _); discriminate.
Qed.

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

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

Lemma seval_builtin_sval_args (ge:RTL.genv) sp rs0 m0 lbs:
   forall lba m v, 
   seval_list_builtin_sval ge sp lbs rs0 m0 = Some lba ->
   list_forall2 (eval_builtin_arg ge (fun id => id) sp m) lba v ->
   seval_builtin_args ge sp m rs0 m0 lbs v.
Proof.
  unfold seval_builtin_args; induction lbs; simpl; intros lba m v.
  - intros H; inversion H; subst; clear H.
    intros H; inversion H. econstructor.
  - destruct (seval_builtin_sval _ _ _ _ _) eqn:SV; try congruence.
    destruct (seval_list_builtin_sval _ _ _ _ _) eqn: SVL; try congruence.
    intros H; inversion H; subst; clear H.
    intros H; inversion H; subst; clear H. 
    econstructor; eauto.
    eapply seval_builtin_sval_arg; eauto.
Qed.

Lemma seval_builtin_args_sval ge sp m rs0 m0 lv: forall lbs,
  seval_builtin_args ge sp m rs0 m0 lbs lv ->
  exists lba,
    seval_list_builtin_sval ge sp lbs rs0 m0 = Some lba
    /\ list_forall2 (eval_builtin_arg ge (fun id => id) sp m) lba lv.
Proof.
  induction 1.
  - eexists. constructor.
    + simpl. reflexivity.
    + constructor.
  - destruct IHlist_forall2 as (lba & A & B).
    apply seval_builtin_arg_sval in H. destruct H as (ba & A' & B').
    eexists. constructor.
    + simpl. rewrite A'. rewrite A. reflexivity.
    + constructor; assumption.
Qed.

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

Lemma seval_list_builtin_sval_correct ge sp m rs0 m0 vargs: forall lbs1,
  seval_builtin_args ge sp m rs0 m0 lbs1 vargs ->
  forall lbs2, (seval_list_builtin_sval ge sp lbs1 rs0 m0) = (seval_list_builtin_sval ge sp lbs2 rs0 m0) ->
  seval_builtin_args ge sp m rs0 m0 lbs2 vargs.
Proof.
  intros. exploit seval_builtin_args_sval; eauto.
  intros (ba & X1 & X2).
  eapply seval_builtin_sval_args; eauto.
  congruence.
Qed.

(* NOTE: we need to mix semantical simulation and syntactic definition on [sfval] in order to abstract the [match_states] *)
Inductive sfval_simu (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node) (ctx: simu_proof_context f): sfval -> sfval -> Prop :=
  | Snone_simu: 
      dm!opc2 = Some opc1 -> 
      sfval_simu dm f opc1 opc2 ctx Snone Snone
  | Scall_simu sig svos1 svos2 lsv1 lsv2 res pc1 pc2:
      dm!pc2 = Some pc1 ->
      svident_simu f ctx svos1 svos2 ->
      (seval_list_sval (the_ge1 ctx) (the_sp ctx) lsv1 (the_rs0 ctx) (the_m0 ctx))
      = (seval_list_sval (the_ge2 ctx) (the_sp ctx) lsv2 (the_rs0 ctx) (the_m0 ctx)) ->
      sfval_simu dm f opc1 opc2 ctx (Scall sig svos1 lsv1 res pc1) (Scall sig svos2 lsv2 res pc2)
  | Stailcall_simu sig svos1 svos2 lsv1 lsv2:
      svident_simu f ctx svos1 svos2 ->
      (seval_list_sval (the_ge1 ctx) (the_sp ctx) lsv1 (the_rs0 ctx) (the_m0 ctx))
      = (seval_list_sval (the_ge2 ctx) (the_sp ctx) lsv2 (the_rs0 ctx) (the_m0 ctx)) ->
      sfval_simu dm f opc1 opc2 ctx (Stailcall sig svos1 lsv1) (Stailcall sig svos2 lsv2)
  | Sbuiltin_simu ef lbs1 lbs2 br pc1 pc2:
      dm!pc2 = Some pc1 ->
      (seval_list_builtin_sval (the_ge1 ctx) (the_sp ctx) lbs1 (the_rs0 ctx) (the_m0 ctx))
      = (seval_list_builtin_sval (the_ge2 ctx) (the_sp ctx) lbs2 (the_rs0 ctx) (the_m0 ctx)) ->
      sfval_simu dm f opc1 opc2 ctx (Sbuiltin ef lbs1 br pc1) (Sbuiltin ef lbs2 br pc2)
  | Sjumptable_simu sv1 sv2 lpc1 lpc2:
      ptree_get_list dm lpc2 = Some lpc1 ->
      (seval_sval (the_ge1 ctx) (the_sp ctx) sv1 (the_rs0 ctx) (the_m0 ctx))
      = (seval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx)) ->
      sfval_simu dm f opc1 opc2 ctx (Sjumptable sv1 lpc1) (Sjumptable sv2 lpc2)
  | Sreturn_simu_none: sfval_simu dm f opc1 opc2 ctx (Sreturn None) (Sreturn None)
  | Sreturn_simu_some sv1 sv2:
      (seval_sval (the_ge1 ctx) (the_sp ctx) sv1 (the_rs0 ctx) (the_m0 ctx))
      = (seval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx)) ->
      sfval_simu dm f opc1 opc2 ctx (Sreturn (Some sv1)) (Sreturn (Some sv2)).

Definition sstate_simu dm f outframe (s1 s2: sstate) (ctx: simu_proof_context f): Prop :=
       sistate_simu dm f outframe s1.(internal) s2.(internal) ctx
    /\ forall is1,
           ssem_internal (the_ge1 ctx) (the_sp ctx) s1 (the_rs0 ctx) (the_m0 ctx) is1 -> 
           is1.(icontinue) = true ->
           sfval_simu dm f s1.(si_pc) s2.(si_pc) ctx s1.(final) s2.(final).

Definition sexec_simu dm (f1 f2: RTLpath.function) pc1 pc2: Prop :=
    forall st1, sexec f1 pc1 = Some st1 -> 
    exists path st2, (fn_path f1)!pc1 = Some path /\ sexec f2 pc2 = Some st2 
     /\ forall ctx, sstate_simu dm f1 path.(pre_output_regs) st1 st2 ctx.