path: root/mppa_k1c/lib/RTLpathSE_theory.v

(* A theory of symbolic execution on RTLpath

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

*)

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

(* NOTE for the implementation of the symbolic execution.
   It is important to remove dependency of Op on memory.
   Here is an way to formalize this 

Parameter mem_irrel: operation -> bool.
Hypothesis eval_operation_mem_irrel: forall (ge: RTL.genv) sp o args m1 m2, mem_irrel o = true -> eval_operation ge sp o args m1 = eval_operation ge sp o args m2.

*)

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

(* FIXME - might have to add non trapping loads *)
(* symbolic value *)
Inductive sval :=
  | Sinput (r: reg)
  | Sop (op:operation) (lsv: list_sval)  (sm: smem) (* TODO for the implementation: add an additionnal case without dependency on sm*)
  | Sload (sm: smem) (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.

(* FIXME - add non trapping load eval *)
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 chunk addr lsv =>
     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 
  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 }.

Definition smatch_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 := { 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.


Definition sabort_exits ge sp (lx: list sistate_exit) rs0 m0: Prop :=
  exists ext,  List.In ext lx
    /\ seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = None.


Inductive smatch_exits (ge: RTL.genv) (sp:val) (lx:list sistate_exit) (rs0: regset) (m0: mem) rs m pc: Prop :=
  smatch_exits_intro ext lx':
    is_tail (ext::lx') lx ->
    all_fallthrough ge sp lx' rs0 m0 ->
    seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = Some true ->
    smatch_local ge sp ext.(si_elocal) rs0 m0 rs m ->
    ext.(si_ifso) = pc ->
    smatch_exits ge sp lx rs0 m0 rs m pc.


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

Definition smatch (ge: RTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem) (is: istate): Prop :=
  if (is.(icontinue)) 
  then 
    smatch_local ge sp st.(si_local) rs0 m0 is.(irs) is.(imem) 
    /\ st.(si_pc) = is.(ipc)
    /\ all_fallthrough ge sp st.(si_exits) rs0 m0
  else smatch_exits ge sp st.(si_exits) rs0 m0 is.(irs) is.(imem) is.(ipc).

Definition sabort (ge: RTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem): Prop :=
    sabort_local ge sp st.(si_local) rs0 m0
 \/ sabort_exits ge sp st.(si_exits) rs0 m0.

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

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

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

     We prove below that the semantics [sem_option_istate] 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).

(* TODO: is it useful 
Lemma has_not_yet_exit_cons_split ge sp ext lx rs0 m0:
   has_not_yet_exit ge sp (ext::lx) rs0 m0 <-> 
    (seval_condition ge sp ext.(the_cond) ext.(cond_args) ext.(exit_ist).(the_smem) rs0 m0 = Some false /\ has_not_yet_exit ge sp lx rs0 m0).
Proof.
  unfold has_not_yet_exit; simpl; intuition (subst; auto).
Qed.
*)

Lemma all_fallthrough_noexit ge sp st rs0 m0 rs m pc:
  smatch_exits ge sp (si_exits st) rs0 m0 rs m pc ->
  all_fallthrough ge sp (si_exits st) rs0 m0 ->
  False.
Proof.
  Local Hint Resolve is_tail_in: core.
  destruct 1 as [ext lx' lc NYE' EVAL SEM PC]. subst.
  unfold all_fallthrough; intros NYE; rewrite NYE in EVAL; eauto.
  try congruence.
Qed.

Lemma smatch_exclude_incompatible_continue ge sp st rs m is1 is2:
  is1.(icontinue) = true ->
  is2.(icontinue) = false ->
  smatch ge sp st rs m is1 ->
  smatch ge sp st rs m is2 ->
  False.
Proof.
  Local Hint Resolve all_fallthrough_noexit: core.
  unfold smatch.
  intros CONT1 CONT2.
  rewrite CONT1, CONT2; simpl.
  intuition eauto.
Qed.

Lemma smatch_determ_continue ge sp st rs m is1 is2:
   smatch ge sp st rs m is1 ->
   smatch ge sp st rs m is2 ->
   is1.(icontinue) = is2.(icontinue).
Proof.
   Local Hint Resolve smatch_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 smatch_local_determ ge sp st rs0 m0 rs1 m1 rs2 m2:
  smatch_local ge sp st rs0 m0 rs1 m1 ->
  smatch_local ge sp st rs0 m0 rs2 m2 ->
  (forall r, rs1#r = rs2#r) /\ m1 = m2.
Proof.
  unfold smatch_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 smatch_exits_determ ge sp lx rs0 m0 rs1 m1 pc1 rs2 m2 pc2 :
  smatch_exits ge sp lx rs0 m0 rs1 m1 pc1 ->
  smatch_exits ge sp lx 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.
  destruct 1 as [ext1 lx1 TAIL1 NYE1 EVAL1 SEM1 PC1]; subst.
  destruct 1 as [ext2 lx2 TAIL2 NYE2 EVAL2 SEM2 PC2]; subst.
  assert (X:ext1=ext2).
  - destruct (is_tail_bounded_total (ext1 :: lx1) (ext2::lx2) lx) as [TAIL|TAIL]; eauto.
  - subst. destruct (smatch_local_determ ge sp (si_elocal ext2) rs0 m0 rs1 m1 rs2 m2); auto.
Qed.

Lemma smatch_determ ge sp st rs m is1 is2:
  smatch ge sp st rs m is1 ->
  smatch ge sp st rs m is2 ->
  istate_eq is1 is2.
Proof.
  unfold istate_eq.
  intros SEM1 SEM2. 
  exploit (smatch_determ_continue ge sp st rs m is1 is2); eauto.
  intros CONTEQ. unfold smatch in * |-. rewrite CONTEQ in * |- *.
  destruct (icontinue is2).
  - destruct (smatch_local_determ ge sp (si_local st) rs m (irs is1) (imem is1) (irs is2) (imem is2)); 
    intuition (try congruence).
  - destruct (smatch_exits_determ ge sp (si_exits st) rs m (irs is1) (imem is1) (ipc is1) (irs is2) (imem is2) (ipc is2));
    intuition.
Qed.

Lemma smatch_exclude_sabort_local_continue ge sp st rs m is:
  icontinue is = true ->
  sabort_local ge sp (si_local st) rs m ->
  smatch ge sp st rs m is -> False.
Proof.
  intros CONT ABORT SEM. unfold smatch in SEM. rewrite CONT in SEM.
  destruct SEM as (SEML & _ & _). inversion SEML as (SEML1 & SEML2 & SEML3); clear SEML.
  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; clear ABORT.
  - contradiction.
  - rewrite SEML2 in ABORT2. discriminate.
  - inv ABORT3. rewrite SEML3 in H. discriminate.
Qed.

Lemma smatch_exclude_sabort_local_nocontinue ge sp st rs0 m0 is:
  icontinue is = false ->
  sabort_local ge sp (si_local st) rs0 m0 ->
  smatch ge sp st rs0 m0 is -> False.
Proof.
(*   intros CONT ABORT SEM. unfold sem_istate in SEM. rewrite CONT in SEM.
  destruct st as [pc exits iis]. simpl in *.
  destruct is as [cont pc' rs' m']. simpl in *.
  inv SEM. inversion H2 as (SEML1 & SEML2 & SEML3); clear H2.
  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; clear ABORT.
  - Search iis.
  - rewrite SEML2 in ABORT2. discriminate.
  - inv ABORT3. rewrite SEML3 in H. discriminate. *)
Admitted.


Lemma smatch_exclude_sabort_local ge sp st rs m is:
  sabort_local ge sp (si_local st) rs m ->
  smatch ge sp st rs m is -> False.
Proof.
  intros. destruct (icontinue is) eqn:CONT.
  - eapply smatch_exclude_sabort_local_continue; eauto.
  - eapply smatch_exclude_sabort_local_nocontinue; eauto.
Qed.

Lemma smatch_exclude_sabort_exits ge sp st rs m is:
  sabort_exits ge sp (si_exits st) rs m ->
  smatch ge sp st rs m is -> False.
Proof.
Admitted.

Lemma smatch_exclude_sabort ge sp st rs m is:
  sabort ge sp st rs m ->
  smatch ge sp st rs m is -> False.
Proof.
  intros ABORT SEM.
  inv ABORT.
  - eapply smatch_exclude_sabort_local; eauto.
  - eapply smatch_exclude_sabort_exits; eauto.
Qed.

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

Lemma smatch_opt_determ ge sp st rs m ois is:
  smatch_opt ge sp st rs m ois ->
  smatch ge sp st rs m is ->
  istate_eq_opt is ois.
Proof.
  destruct ois as [is1|]; simpl; eauto.
  - intros; eexists; intuition; eapply smatch_determ; eauto.
  - intros; exploit smatch_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): option sistate :=
   Some {| si_pc := pc; si_exits := st.(si_exits); si_local:= nxt |}.

(* FIXME - add notrap *)
Definition symb_istep (i: instruction) (st: sistate): option sistate := 
  match i with
  | Inop pc' => 
      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
      sist_set_local st pc' next
  | Iload _ 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) chunk addr vargs) in
      sist_set_local st pc' next
  | Istore chunk addr args src pc' =>
      let prev := st.(si_local) in
      let vargs := list_sval_inj (List.map prev.(si_sreg) args) in
      let next := slocal_set_smem prev (Sstore prev.(si_smem) chunk addr vargs (prev.(si_sreg) src)) in
      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 (* TODO jumptable ? *)
  end.

(* TODO TODO - continue renaming *)

Lemma list_sval_eval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs: 
   (forall r : reg, seval ge sp (sreg r) rs0 m0 = Some (rs # r)) ->
   list_sval_eval 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 symb_istep_preserv_early_exits i ge sp st rs0 m0 rs m pc st':
  sem_early_exit ge sp st.(exits) rs0 m0 rs m pc ->
  symb_istep i st = Some st' ->
  sem_early_exit ge sp st'.(exits) rs0 m0 rs m pc.
Proof.
  intros H.
  destruct i; simpl; unfold sist, sem_istate, sem_local_istate; simpl; try_simplify_someHyps.
  destruct H as [ext lx TAIL NYE COND INV PC].
  econstructor; try (eapply is_tail_cons; eapply TAIL); eauto.
Qed.

Lemma sreg_set_preserv_has_aborted ge sp st rs0 m0 r sv:
  has_aborted_on_basic ge sp st rs0 m0 ->
  has_aborted_on_basic ge sp (sreg_set st r sv) rs0 m0.
Proof.
  unfold has_aborted_on_basic. 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 smem_set_preserv_has_aborted ge sp st rs0 m0 m:
  has_aborted_on_basic ge sp st rs0 m0 ->
  has_aborted_on_basic ge sp (smem_set st m) rs0 m0.
Proof.
  unfold has_aborted_on_basic. simpl; intuition.
Qed.

Lemma symb_istep_preserv_has_aborted i ge sp rs0 m0 st st': 
  symb_istep i st = Some st' ->
  has_aborted ge sp st rs0 m0 -> has_aborted ge sp st' rs0 m0.
Proof.
  Local Hint Resolve sreg_set_preserv_has_aborted smem_set_preserv_has_aborted: core.
  unfold has_aborted.
  destruct i; simpl; unfold sist, sem_istate, sem_local_istate; simpl; try_simplify_someHyps; intuition eauto.
  (* COND *)
  right. unfold has_aborted_on_test in * |- *.
  destruct H as (ext & H1 & H2).
  simpl; exists ext; intuition.
Qed.

Lemma symb_istep_WF i st:
  symb_istep i st = None -> default_succ i = None.
Proof.
  destruct i; simpl; unfold sist; simpl; congruence.
Qed.

Lemma symb_istep_default_succ i st st':
  symb_istep i st = Some st' -> default_succ i = Some (st'.(the_pc)).
Proof.
  destruct i; simpl; unfold sist; simpl; try congruence;
  intro H; inversion_clear H; simpl; auto.
Qed.

Lemma symb_istep_correct ge sp i st rs0 m0 rs m:
  sem_local_istate ge sp st.(curr) rs0 m0 rs m ->
  has_not_yet_exit ge sp st.(exits) rs0 m0 ->
  sem_option2_istate ge sp (symb_istep i st) rs0 m0 (istep ge i sp rs m).
Proof.
  intros (PRE & MEM & REG) NYE.
  destruct i; simpl; auto.
  + (* Nop *)
    unfold sem_istate, sem_local_istate; simpl; try_simplify_someHyps.
  + (* Op *)
    inversion_SOME v; intros OP; simpl.
    - unfold sem_istate, sem_local_istate; simpl; intuition.
      * exploit REG. try_simplify_someHyps.
      * destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto].
        subst; rewrite Regmap.gss; simpl; auto.
        erewrite list_sval_eval_inj; simpl; auto.
        try_simplify_someHyps.
    - unfold has_aborted, has_aborted_on_basic; simpl. 
      left. right. right.
      exists r. destruct (Pos.eq_dec r r); try congruence.
      simpl. erewrite list_sval_eval_inj; simpl; auto.
      try_simplify_someHyps.
  + (* LOAD *) admit. (* FIXME *)
(*     inversion_SOME a0; intros ADD.
    { inversion_SOME v; intros LOAD; simpl.
      - explore_destruct; unfold sem_istate, sem_local_istate; simpl; intuition.
        * exploit REG. try_simplify_someHyps.
        * destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto].
          subst; rewrite Regmap.gss; simpl.
          erewrite list_sval_eval_inj; simpl; auto.
          try_simplify_someHyps.
      - unfold has_aborted, has_aborted_on_basic; simpl.
        left. right. right.
        exists r. destruct (Pos.eq_dec r r); try congruence.
        simpl. erewrite list_sval_eval_inj; simpl; auto.
        try_simplify_someHyps. }
    { unfold has_aborted, has_aborted_on_basic; simpl. 
      left. right. right.
      exists r. destruct (Pos.eq_dec r r); try congruence.
      simpl. erewrite list_sval_eval_inj; simpl; auto.
      rewrite ADD; simpl; auto. } *)
   + (* STORE *)
    inversion_SOME a0; intros ADD.
    { inversion_SOME m'; intros STORE; simpl.
      - unfold sem_istate, sem_local_istate; simpl; intuition.
        * congruence.
        * erewrite list_sval_eval_inj; simpl; auto.
          erewrite REG.
          try_simplify_someHyps.
      - unfold has_aborted, has_aborted_on_basic; simpl.
        left. right. left.
        erewrite list_sval_eval_inj; simpl; auto.
        erewrite REG.
        try_simplify_someHyps. }
    { unfold has_aborted, has_aborted_on_basic; simpl.
      left. right. left.
      erewrite list_sval_eval_inj; simpl; auto.
      erewrite ADD; simpl; auto. }
   + (* COND *)
    Local Hint Resolve is_tail_refl: core.
    Local Hint Unfold sem_local_istate: core.
    inversion_SOME b; intros COND.
    { destruct b; simpl; unfold sem_istate, sem_local_istate; simpl.
      - intros; econstructor; eauto; simpl.
        unfold seval_condition.
        erewrite list_sval_eval_inj; simpl; auto.
        try_simplify_someHyps.
      - intuition. unfold has_not_yet_exit in * |- *. simpl.
        intuition. subst. simpl.
        unfold seval_condition.
        erewrite list_sval_eval_inj; simpl; auto.
        try_simplify_someHyps. }
    { unfold has_aborted, has_aborted_on_test; simpl.
      right. eexists; intuition eauto. simpl.
        unfold seval_condition.
        erewrite list_sval_eval_inj; simpl; auto.
        try_simplify_someHyps. }
Admitted.

Lemma symb_istep_correct_None ge sp i st rs0 m0 rs m:
  sem_local_istate ge sp (st.(curr)) rs0 m0 rs m ->
  symb_istep i st = None -> 
  istep ge i sp rs m = None.
Proof.
  intros (PRE & MEM & REG).
  destruct i; simpl; unfold sist, sem_istate, sem_local_istate; simpl; try_simplify_someHyps.
Qed.

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

Lemma symb_isteps_correct_false ge sp path f rs0 m0 st' is: 
  is.(icontinue)=false ->
  forall st, sem_istate ge sp st rs0 m0 is -> 
  symb_isteps path f st = Some st' ->
  sem_istate ge sp st' rs0 m0 is.
Proof.
  Local Hint Resolve symb_istep_preserv_early_exits: core.
  intros CONT; unfold sem_istate; rewrite CONT.
  induction path; simpl.
  + unfold sist; try_simplify_someHyps.
  + intros st; inversion_SOME i.
    inversion_SOME st1; eauto.
Qed.

Lemma symb_isteps_preserv_has_aborted ge sp path f rs0 m0 st': forall st, 
  symb_isteps path f st = Some st' ->
  has_aborted ge sp st rs0 m0 -> has_aborted ge sp st' rs0 m0.
Proof.
  Local Hint Resolve symb_istep_preserv_has_aborted: core.
  induction path; simpl.
  + unfold sist; try_simplify_someHyps.
  + intros st; inversion_SOME i.
    inversion_SOME st1; eauto.
Qed.

Lemma symb_isteps_WF path f: forall st,
  symb_isteps path f st = None -> nth_default_succ (fn_code f) path st.(the_pc) = None.
Proof.
  induction path; simpl.
  + unfold sist. intuition congruence.
  + intros st; destruct ((fn_code f) ! (the_pc st)); simpl; try tauto.
    destruct (symb_istep i st) as [st1|] eqn: Hst1; simpl.
    - intros; erewrite symb_istep_default_succ; eauto.
    - intros; erewrite symb_istep_WF; eauto.
Qed.

Lemma symb_isteps_default_succ path f st': forall st,
  symb_isteps path f st = Some st' -> nth_default_succ (fn_code f) path st.(the_pc) = Some st'.(the_pc).
Proof.
  induction path; simpl.
  + unfold sist. intros st H. inversion_clear H; simpl; try congruence.
  + intros st; destruct ((fn_code f) ! (the_pc st)); simpl; try congruence.
    destruct (symb_istep i st) as [st1|] eqn: Hst1; simpl; try congruence.
    intros; erewrite symb_istep_default_succ; eauto.
Qed.

Lemma symb_isteps_correct_true ge sp path (f:function) rs0 m0: forall st is,
  is.(icontinue)=true ->
  sem_istate ge sp st rs0 m0 is -> 
  nth_default_succ (fn_code f) path st.(the_pc) <> None ->
  sem_option2_istate ge sp (symb_isteps path f st) rs0 m0
                         (isteps ge path f sp is.(the_rs) is.(the_mem) is.(RTLpath.the_pc))
  .
Proof.
  Local Hint Resolve symb_isteps_correct_false symb_isteps_preserv_has_aborted symb_isteps_WF: core.
  induction path; simpl.
  + intros st is CONT INV WF;
    unfold sem_istate, sist in * |- *;
    try_simplify_someHyps. simpl.
    destruct is; simpl in * |- *; subst; intuition auto.
  + intros st is CONT; unfold sem_istate at 1; rewrite CONT.
    intros (LOCAL & PC & NYE) WF.
    rewrite <- PC.
    inversion_SOME i; intro Hi; rewrite Hi in WF |- *; simpl; auto.
    exploit symb_istep_correct; eauto. 
    inversion_SOME st1; intros Hst1; erewrite Hst1; simpl.
    - inversion_SOME is1; intros His1;rewrite His1; simpl. 
      * destruct (icontinue is1) eqn:CONT1.
        (* continue is0 = true *)
        intros; eapply IHpath; eauto.
        destruct i; simpl in * |- *; unfold sist in * |- *; try_simplify_someHyps.
        (* continue is0 = false -> EARLY EXIT *)
        destruct (symb_isteps path f st1) as [st2|] eqn: Hst2; simpl; eauto.
        destruct WF. erewrite symb_istep_default_succ; eauto.
        (* try_simplify_someHyps; eauto. *)
      * destruct (symb_isteps path f st1) as [st2|] eqn: Hst2; simpl; eauto.
    - intros His1;rewrite His1; simpl; auto.
Qed.

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

Lemma symb_isteps_right_assoc_decompose f path: forall st st',
  symb_isteps (S path) f st = Some st' ->
  exists st0, symb_isteps path f st = Some st0 /\ symb_isteps 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 symb_isteps_right_assoc_compose f path: forall st st0 st',
  symb_isteps path f st = Some st0 ->
  symb_isteps 1%nat f st0 = Some st' ->
  symb_isteps (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: external_function -> list (builtin_arg sval) -> builtin_res sval -> sfval
  | Sjumptable: sval -> list node -> sfval
*)
  | Sreturn: option sval -> sfval
.

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

Inductive sfval_sem (pge: RTLpath.genv) (ge: RTL.genv) (sp:val) (st: s_istate) stack (f: function) (rs0: regset) (m0: mem): sfval -> regset -> mem -> trace -> state -> Prop :=
  | exec_Snone rs m:
      sfval_sem pge ge sp st stack f rs0 m0 Snone rs m E0 (State stack f sp st.(the_pc) rs m)
  | exec_Scall rs m sig svos lsv args res pc fd:
      s_find_function pge ge sp svos rs0 m0 = Some fd ->
      funsig fd = sig ->
      list_sval_eval ge sp lsv rs0 m0 = Some args ->
      sfval_sem pge ge sp st stack f rs0 m0 (Scall sig svos lsv res pc) rs m
        E0 (Callstate (Stackframe res f sp pc rs :: stack) fd args m)
(* TODO:
  | exec_Itailcall stk pc rs m sig ros args fd m':
      (fn_code f)!pc = Some(Itailcall sig ros args) ->
      find_function pge ros rs = Some fd ->
      funsig fd = sig ->
      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
      path_last_step ge pge stack f (Vptr stk Ptrofs.zero) pc rs m
        E0 (Callstate stack fd rs##args m')
  | exec_Ibuiltin sp pc rs m ef args res pc' vargs t vres m':
      (fn_code f)!pc = Some(Ibuiltin ef args res pc') ->
      eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
      external_call ef ge vargs m t vres m' ->
      path_last_step ge pge stack f sp pc rs m
         t (State stack f sp pc' (regmap_setres res vres rs) m')
  | exec_Ijumptable sp pc rs m arg tbl n pc': (* TODO remove jumptable from here ? *)
      (fn_code f)!pc = Some(Ijumptable arg tbl) ->
      rs#arg = Vint n ->
      list_nth_z tbl (Int.unsigned n) = Some pc' ->
      path_last_step ge pge stack f sp pc 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 ge sp sv rs0 m0 | None => Some Vundef end = Some v ->
      sfval_sem pge ge sp st stack f rs0 m0 (Sreturn osv) rs m 
         E0 (Returnstate stack v m')
.

Record s_state := { internal:> s_istate; final: sfval }.

Inductive sem_state pge (ge: RTL.genv) (sp:val) (st: s_state) stack f (rs0: regset) (m0: mem): trace -> state -> Prop :=
  | sem_early is:
     is.(icontinue) = false ->
     sem_istate ge sp st rs0 m0 is -> 
     sem_state pge ge sp st stack f rs0 m0 E0 (State stack f sp is.(RTLpath.the_pc) is.(the_rs) is.(the_mem))
  | sem_normal is t s:
     is.(icontinue) = true ->
     sem_istate ge sp st rs0 m0 is ->  
     sfval_sem pge ge sp st stack f rs0 m0 st.(final) is.(the_rs) is.(the_mem) t s ->
     sem_state pge ge sp st stack f rs0 m0 t s 
  .

(** * Symbolic execution of final step *)
Definition symb_fstep (i: instruction) (prev: local_istate): sfval := 
  match i with
  | Icall sig ros args res pc => 
    let svos := sum_left_map prev.(the_sreg) ros in
    let sargs := list_sval_inj (List.map prev.(the_sreg) args) in
    Scall sig svos sargs res pc
  | Ireturn or => 
    let sor := SOME r <- or IN Some (prev.(the_sreg) r) in
    Sreturn sor
  | _ => Snone
  end.

Lemma symb_fstep_correct pge ge sp i (f:function) pc st stack rs0 m0 t rs m s:
  (fn_code f) ! pc = Some i ->
  pc = st.(the_pc) ->
  sem_local_istate ge sp (curr st) rs0 m0 rs m ->
  path_last_step ge pge stack f sp pc rs m t s ->
  symb_istep i st = None -> 
  sfval_sem pge ge sp st stack f rs0 m0 (symb_fstep i (curr st)) rs m t s.
Proof.
  intros PC1 PC2 (PRE&MEM&REG) LAST Hi. destruct LAST; subst; try_simplify_someHyps; simpl.
  + (* Snone *) destruct i; simpl in Hi |- *; unfold sist in Hi; try congruence.
  + (* Icall *) intros; eapply exec_Scall; auto.
    - destruct ros; simpl in * |- *; auto.
      rewrite REG; auto.
    - erewrite list_sval_eval_inj; simpl; auto.
  + (* Itaillcall *) admit.
  + (* Ibuiltin *) admit.
  + (* Ijumptable *) admit.
  + (* Ireturn *) intros; eapply exec_Sreturn; simpl; eauto.
    destruct or; simpl; auto.
Admitted.

Lemma symb_fstep_complete i (f:function) pc st ge pge sp stack rs0 m0 t rs m s:
  (fn_code f) ! pc = Some i ->
  pc = st.(the_pc) ->
  sem_local_istate ge sp (curr st) rs0 m0 rs m ->
  sfval_sem pge ge sp st stack f rs0 m0 (symb_fstep i (curr st)) rs m t s ->
  symb_istep i st = None -> 
  path_last_step ge pge stack f sp pc rs m t s.
Proof.
  intros PC1 PC2 (PRE&MEM&REG) LAST Hi. 
  destruct i as [ | | | |(*Icall*)sig ros args res pc'| | | | |(*Ireturn*)or]; 
  subst; try_simplify_someHyps; try (unfold sist in Hi; try congruence); inversion LAST; subst; clear LAST; simpl in * |- *.
  + (* Icall *)
    erewrite list_sval_eval_inj in * |- ; simpl; try_simplify_someHyps; auto.
    intros; eapply exec_Icall; eauto.
    destruct ros; simpl in * |- *; auto.
    rewrite REG in * |- ; auto.
  + (* Itaillcall *) admit.
  + (* Ibuiltin *) admit.
  + (* Ijumptable *) admit.
  + (* Ireturn *)
    intros; subst. enough (v=regmap_optget or Vundef rs) as ->.
    * eapply exec_Ireturn; eauto.
    * intros; destruct or; simpl; congruence.
Admitted.


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

Definition init_local_istate := {| pre:= fun _ _ _ _ => True; the_sreg:= fun r => Sinput r; the_smem:= Sinit |}.

Definition init_istate pc := {| the_pc:= pc; exits:=nil; curr:= init_local_istate |}.

Lemma init_sem_istate ge sp pc rs m: sem_istate ge sp (init_istate pc) rs m (ist true pc rs m).
Proof.
  unfold sem_istate, sem_local_istate, has_not_yet_exit; simpl. intuition.
Qed.

Definition symb_step (f: function) (pc:node): option s_state :=
  SOME path <- (fn_path f)!pc IN
  SOME st <- symb_isteps path.(psize) f (init_istate pc) IN
  SOME i <- (fn_code f)!(st.(the_pc)) IN
  Some (match symb_istep i st with
       | Some st' => {| internal := st'; final := Snone |}
       | None => {| internal := st; final := symb_fstep i st.(curr) |}
       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.(the_pc) ->
  symb_istep i st = Some st' ->
  path_last_step ge pge stack f sp pc rs m t s ->
  exists ist, istep ge i sp rs m = Some ist /\ t = E0 /\ s = (State stack f sp ist.(RTLpath.the_pc) ist.(RTLpath.the_rs) ist.(the_mem)).
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 [symb_step]) 
(symb_step is a correct over-approximation)
*)
Theorem symb_step_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, symb_step f pc = Some st /\ sem_state pge ge sp st stack f rs m t s.
Proof.
   Local Hint Resolve init_sem_istate symb_istep_preserv_early_exits: core.
   intros PATH STEP; unfold symb_step; rewrite PATH; simpl.
   lapply (final_node_path_simpl f path pc); eauto. intro WF.
   exploit (symb_isteps_correct_true ge sp path.(psize) f rs m (init_istate pc) (ist 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 sem_option2_istate; destruct (symb_isteps _ _ _) as [st|] eqn: Hst; try congruence);
   (* intro SEM *)
   (simpl; unfold sem_istate; simpl; rewrite CONT; intro SEM);
   (* intro Hi' *)
   ( assert (Hi': (fn_code f) ! (the_pc st) = Some i); 
     [ unfold nth_default_succ_inst in Hi; 
       exploit symb_isteps_default_succ; eauto; simpl;
       intros DEF; rewrite DEF in Hi; auto 
       | clear Hi; rewrite Hi' ]);
   (* eexists *)
   (eexists; constructor; eauto).
   - (* early *)
     eapply sem_early; eauto.
     unfold sem_istate; simpl; rewrite CONT.
     destruct (symb_istep i st) as [st'|] eqn: Hst'; simpl; eauto.
   - destruct SEM as (SEM & PC & HNYE).
     destruct (symb_istep i st) as [st'|] eqn: Hst'; simpl.
     + (* normal on Snone *)
       rewrite <- PC in LAST.
       exploit symb_path_last_step; eauto; simpl.
       intros (ist & ISTEP & Ht & Hs); subst.
       exploit symb_istep_correct; eauto. simpl.
       erewrite Hst', ISTEP; simpl.
       clear LAST CONT STEPS PC SEM HNYE Hst Hi' Hst' ISTEP st sti i.
       intro SEM; destruct (ist.(icontinue)) eqn: CONT.
       { (* continue ist = true *)
         eapply sem_normal; simpl; eauto.
         unfold sem_istate in SEM.
         rewrite CONT in SEM.
         destruct SEM as (SEM & PC & HNYE).
         rewrite <- PC.
         eapply exec_Snone. }
       { eapply sem_early; eauto. }
     + (* normal non-Snone instruction *) 
       eapply sem_normal; eauto.
       * unfold sem_istate; simpl; rewrite CONT; intuition.
       * simpl. eapply symb_fstep_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 sfval_sem_equiv pge ge sp (f:function) st sv stack rs0 m0 t rs1 rs2 m s:
  sfval_sem 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' /\ sfval_sem 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).
  - (* Sreturn *) intros; eexists; econstructor.
    + eapply equiv_state_refl; eauto.
    + eapply exec_Sreturn; eauto.
Qed.

(* NB: each execution of a symbolic state (produced from [symb_step]) represents a concrete execution
  (symb_step is exact).
*)
Theorem symb_step_exact f pc pge ge sp path stack st rs m t s1: 
  (fn_path f)!pc = Some path ->
  symb_step f pc = Some st -> 
  sem_state 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_sem_istate: core.
  unfold symb_step; intros PATH SSTEP SEM; rewrite PATH in SSTEP.
  lapply (final_node_path_simpl f path pc); eauto. intro WF.
  exploit (symb_isteps_correct_true ge sp path.(psize) f rs m (init_istate pc) (ist 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 (symb_isteps path.(psize) f (init_istate pc)) as [st0|] eqn: Hst0; simpl.
  2:{ (* absurd case *)
      exploit symb_isteps_WF; eauto.
      simpl; intros NDS; rewrite NDS in Hi; congruence. }
  exploit symb_isteps_default_succ; eauto; simpl.
  intros NDS; rewrite NDS in Hi.
  rewrite Hi in SSTEP.
  intros ISTEPS. try_simplify_someHyps.
  destruct (symb_istep i st0) as [st'|] eqn: Hst'; simpl.
  + (* normal exit on Snone instruction *)
    admit.
  + destruct SEM as [is CONT SEM|is t s CONT SEM1 SEM2]; simpl in * |- *.
    - (* early exit *)
      intros.
      exploit sem_option_istate_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 sem_option_istate_determ; eauto.
      destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4).
      unfold sem_istate in SEM1.
      rewrite CONT in SEM1. destruct SEM1 as (SEM1 & PC0 & NYE0).
      exploit sfval_sem_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 symb_fstep_complete; eauto.
      * congruence.
      * unfold sem_local_istate in * |- *. intuition try congruence.
Admitted.

(** * 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.

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

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

Lemma smem_eval_preserved sp sm rs0 m0: 
  smem_eval ge sp sm rs0 m0 = smem_eval ge' sp sm rs0 m0.
Proof.
  induction sm; simpl; auto.
  rewrite list_sval_eval_preserved. destruct (list_sval_eval _ _ _ _); auto.
  erewrite <- eval_addressing_preserved; eauto.
  destruct (eval_addressing _ sp _ _); auto.
  rewrite IHsm; clear IHsm. destruct (smem_eval _ _ _ _); 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 (list_sval_eval _ _ _ _); auto.
  rewrite smem_eval_preserved; auto.
Qed.

End SymbValPreserved.

Require Import RTLpathLivegen RTLpathLiveproofs.

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

Definition istate_simu f (srce: PTree.t node) is1 is2: Prop :=
  if is1.(icontinue) then
     (* TODO: il faudra raffiner le (fun _ => True) si on veut autoriser l'oracle à
        ajouter du "code mort" sur des registres non utilisés (loop invariant code motion à la David)
        Typiquement, pour connaître la frame des registres vivants, il faudra faire une propagation en arrière
        sur la dernière instruction du superblock. *)
     istate_simulive (fun _ => True) srce is1 is2
  else
     exists path, f.(fn_path)!(is1.(RTLpath.the_pc)) = Some path 
     /\ istate_simulive (fun r => Regset.In r path.(input_regs)) srce is1 is2
     /\ srce!(is2.(RTLpath.the_pc)) = Some is1.(RTLpath.the_pc).

(* NOTE: a pure semantic definition on [s_istate], for a total freedom in refinements *)
Definition s_istate_simu (f: RTLpath.function) (srce: PTree.t node) (st1 st2: s_istate): Prop :=
  forall sp ge1 ge2, 
  (forall s, Genv.find_symbol ge2 s = Genv.find_symbol ge1 s) ->
  liveness_ok_function f ->
  forall rs m is1, sem_istate ge1 sp st1 rs m is1 -> 
     exists is2, sem_istate ge2 sp st2 rs m is2 /\ istate_simu f srce is1 is2.

(* NOTE: a syntactic definition on [sfval] in order to abstract the [match_states] *)
Inductive sfval_simu (f: RTLpath.function) (srce: PTree.t node) (opc1 opc2: node): sfval -> sfval -> Prop :=
  | Snone_simu: 
      srce!opc2 = Some opc1 -> 
      sfval_simu f srce opc1 opc2 Snone Snone
  | Scall_simu sig svos lsv res pc1 pc2:
     srce!pc2 = Some pc1 ->
     sfval_simu f srce opc1 opc2 (Scall sig svos lsv res pc1) (Scall sig svos lsv res pc2)
  | Sreturn_simu os:
     sfval_simu f srce opc1 opc2 (Sreturn os) (Sreturn os).

Definition s_state_simu f srce (s1 s2: s_state): Prop :=
       s_istate_simu f srce s1.(internal) s2.(internal)
    /\ sfval_simu f srce s1.(the_pc) s2.(the_pc) s1.(final) s2.(final).

Definition symb_step_simu srce (f1 f2: RTLpath.function) pc1 pc2: Prop :=
    forall st1, symb_step f1 pc1 = Some st1 -> 
    exists st2, symb_step f2 pc2 = Some st2 /\ s_state_simu f1 srce st1 st2.

(* IDEA: we will provide an efficient test for checking "symb_step_simu" property, by hash-consing.
   See usage of [symb_step_simu] in [RTLpathScheduler].
*)