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

(** 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 (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_opt ge sp (st: sistate) rs0 m0 (ois: option istate): Prop :=
  match ois with
  | Some is => ssem ge sp st rs0 m0 is
  | None => sabort ge sp st rs0 m0
  end.

Definition ssem_opt2 ge sp (ost: option sistate) rs0 m0 (ois: option istate) : Prop :=
  match ost with
  | Some st => ssem_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_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_exclude_incompatible_continue ge sp st rs m is1 is2:
  is1.(icontinue) = true ->
  is2.(icontinue) = false ->
  ssem ge sp st rs m is1 ->
  ssem ge sp st rs m is2 ->
  False.
Proof.
  Local Hint Resolve all_fallthrough_noexit: core.
  unfold ssem.
  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_determ_continue ge sp st rs m is1 is2:
   ssem ge sp st rs m is1 ->
   ssem ge sp st rs m is2 ->
   is1.(icontinue) = is2.(icontinue).
Proof.
   Local Hint Resolve ssem_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_determ ge sp st rs m is1 is2:
  ssem ge sp st rs m is1 ->
  ssem ge sp st rs m is2 ->
  istate_eq is1 is2.
Proof.
  unfold istate_eq.
  intros SEM1 SEM2. 
  exploit (ssem_determ_continue ge sp st rs m is1 is2); eauto.
  intros CONTEQ. unfold ssem 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' ->
(*   all_fallthrough ge sp (si_exits st) rs m -> *)
  sabort_local ge sp loc rs m ->
  False.
Proof.
  intros SIML (* ALLF *) ABORT. inv SIML. destruct H0 as (H0 & H0').
  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
Qed.

Lemma ssem_local_exclude_sabort_exit ge sp st ext lx rs m rs' m':
  ssem_local ge sp (si_local st) rs m rs' m' ->
  all_fallthrough ge sp (si_exits st) rs m ->
  is_tail (ext :: lx) (si_exits st) ->
  sabort_exit ge sp ext rs m ->
  False.
Proof.
  intros SSEML ALLF TAIL ABORT.
  inv ABORT.
  - exploit ALLF; eauto. congruence.
  - (* FIXME Problem : if we have a ssem_local, this means we ONLY evaluated the conditions,
    but we NEVER actually evaluated the si_elocal from the sistate_exit ! So we cannot prove
    a lack of abort on the si_elocal.. We must change the definitions *)
Abort.

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_exclude_sabort ge sp st rs m is:
  sabort ge sp st rs m ->
  ssem ge sp st rs m is -> False.
Proof.
  intros ABORT SEM.
  unfold ssem 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_opt_determ ge sp st rs m ois is:
  ssem_opt ge sp st rs m ois ->
  ssem ge sp st rs m is ->
  istate_eq_opt is ois.
Proof.
  destruct ois as [is1|]; simpl; eauto.
  - intros; eexists; intuition; eapply ssem_determ; eauto.
  - intros; exploit ssem_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 |}.


Definition sistep (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 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
      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.


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.

(* TODO - continue updating the rest *)

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 sist_set_local_preserves_sabort ge sp rs0 m0 st st' loc' pc':
  sist_set_local st pc' loc' = Some st' ->
  sabort ge sp st rs0 m0 ->
  sabort ge sp st' rs0 m0.
Proof.
  intros SSL ABORT. inv SSL. unfold sabort. simpl.
  destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)].
  - 
Abort.

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 sistep_preserves_sabort i ge sp rs m st st': 
  sistep 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 sistep_WF i st:
  sistep i st = None -> default_succ i = None.
Proof.
  destruct i; simpl; unfold sist_set_local; simpl; congruence.
Qed.

Lemma sistep_default_succ i st st':
  sistep 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 rs: forall l,
  (forall r, List.In r l -> seval_sval ge sp (si_sreg (si_local st) r) rs0 m0 = Some rs # r) ->
  seval_list_sval ge sp (list_sval_inj (map (si_sreg (si_local st)) l)) rs0 m0 = None ->
  False.
Proof.
  induction l.
  - intros. simpl in H0. 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 (si_local st) r) rs0 m0 = Some rs # r).
      { intros r INR. eapply ALLR. right. assumption. }
      intro SVALLIST. intro. eapply IHl; eauto.
    + intros. exploit (ALLR a); [constructor; eauto|]. congruence.
Qed.

Lemma sistep_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_opt2 ge sp (sistep 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, ssem_local; simpl; intuition.
        * unfold ssem. 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. 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; [|exploit seval_list_sval_inj_not_none; eauto; contradiction].
          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. 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. intros SMEM SEVAL.
          rewrite LOAD. reflexivity.
     } { 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. intro SMEM. rewrite ADD. reflexivity.
     }
  + (* STORE *)
    inversion_SOME a0; intros ADD.
    { inversion_SOME m'; intros STORE; simpl.
      - unfold ssem, 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, 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 sistep_correct_None ge sp i st rs0 m0 rs m:
  ssem_local ge sp (st.(si_local)) rs0 m0 rs m ->
  sistep i st = None -> 
  istep ge i sp rs m = None.
Proof.
  intros (PRE & MEM & REG).
  destruct i; simpl; unfold sist_set_local, ssem, ssem_local; simpl; try_simplify_someHyps.
Qed.

(** * Symbolic execution of the internal steps of a path *)
Fixpoint sisteps (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 <- sistep i st IN
    sisteps p f st1
  end.

Lemma sist_set_local_preserves_si_exits st pc loc st':
  sist_set_local st pc loc = Some st' ->
  si_exits st' = si_exits st.
Proof.
  intros. inv H. simpl. reflexivity.
Qed.

Lemma sistep_preserves_allfu ge sp ext lx rs0 m0 st st' i:
  all_fallthrough_upto_exit ge sp ext lx (si_exits st) rs0 m0 ->
  sistep 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; try discriminate; simpl in SISTEP; try (erewrite sist_set_local_preserves_si_exits; eauto; fail).
  inv SISTEP. simpl. constructor. assumption.
Qed.

Lemma sisteps_correct_false ge sp f rs0 m0 st' is:
  forall path,
  is.(icontinue)=false ->
  forall st, ssem ge sp st rs0 m0 is ->
  sisteps path f st = Some st' ->
  ssem 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 (sistep _ _) eqn:SISTEP; [|discriminate].
    eapply IHpath. 3: eapply STEQ'. eauto.
    unfold ssem in SSEM. rewrite ICF in SSEM.
    destruct SSEM as (ext & lx & SEXIT & ALLFU).
    unfold ssem. rewrite ICF. exists ext, lx.
    constructor; auto. eapply sistep_preserves_allfu; eauto.
Qed.

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

Lemma sisteps_WF path f: forall st,
  sisteps 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 (sistep i st) as [st1|] eqn: Hst1; simpl.
    - intros; erewrite sistep_default_succ; eauto.
    - intros; erewrite sistep_WF; eauto.
Qed.

Lemma sisteps_default_succ path f st': forall st,
  sisteps 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 (sistep i st) as [st1|] eqn: Hst1; simpl; try congruence.
    intros; erewrite sistep_default_succ; eauto.
Qed.

Lemma sisteps_correct_true ge sp path (f:function) rs0 m0: forall st is,
  is.(icontinue)=true ->
  ssem ge sp st rs0 m0 is -> 
  nth_default_succ (fn_code f) path st.(si_pc) <> None ->
  ssem_opt2 ge sp (sisteps path f st) rs0 m0
                         (isteps ge path f sp is.(irs) is.(imem) is.(ipc))
  .
Proof.
  Local Hint Resolve sisteps_correct_false sisteps_preserves_sabort sisteps_WF: core.
  induction path; simpl.
  + intros st is CONT INV WF;
    unfold ssem, sist_set_local in * |- *;
    try_simplify_someHyps. simpl.
    destruct is; simpl in * |- *; subst; intuition auto.
  + intros st is CONT; unfold ssem at 1; rewrite CONT.
    intros (LOCAL & PC & NYE) WF.
    rewrite <- PC.
    inversion_SOME i; intro Hi; rewrite Hi in WF |- *; simpl; auto.
    exploit sistep_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 (sisteps path f st1) as [st2|] eqn: Hst2; simpl; eauto.
        destruct WF. erewrite sistep_default_succ; eauto.
        (* try_simplify_someHyps; eauto. *)
      * destruct (sisteps path f st1) as [st2|] eqn: Hst2; simpl; eauto.
    - intros His1;rewrite His1; simpl; auto.
Qed.

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

Lemma sisteps_right_assoc_decompose f path: forall st st',
  sisteps (S path) f st = Some st' ->
  exists st0, sisteps path f st = Some st0 /\ sisteps 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 sisteps_right_assoc_compose f path: forall st st0 st',
  sisteps path f st = Some st0 ->
  sisteps 1%nat f st0 = Some st' ->
  sisteps (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 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.

Inductive sfmatch (pge: RTLpath.genv) (ge: RTL.genv) (sp:val) (st: sistate) stack (f: function) (rs0: regset) (m0: mem): sfval -> regset -> mem -> trace -> state -> Prop :=
  | exec_Snone rs m:
      sfmatch pge ge sp st stack f rs0 m0 Snone rs m E0 (State stack f sp st.(si_pc) 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 ->
      sfmatch 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)
  | exec_Stailcall stk rs m sig svos args fd m' lsv:
      sfind_function pge ge sp svos rs0 m0 = Some fd ->
      funsig fd = sig ->
      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
      seval_list_sval ge sp lsv rs0 m0 = Some args ->
      sfmatch pge ge sp st stack f rs0 m0 (Stailcall sig svos lsv) rs m
        E0 (Callstate stack fd args 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') *)
(* TODO:
  | 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_sval ge sp sv rs0 m0 | None => Some Vundef end = Some v ->
      sfmatch pge ge sp st stack f rs0 m0 (Sreturn osv) rs m 
         E0 (Returnstate stack v m')
.

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

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

(** * Symbolic execution of final step *)
Definition sfstep (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
  | Ireturn or => 
    let sor := SOME r <- or IN Some (prev.(si_sreg) r) in
    Sreturn sor
  | _ => Snone
  end.

Lemma sfstep_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 ->
  sistep i st = None -> 
  sfmatch pge ge sp st stack f rs0 m0 (sfstep i (si_local 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_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.
    - eauto.
    - erewrite seval_list_sval_inj; simpl; auto.
  + (* Ibuiltin *) admit.
  + (* Ijumptable *) admit.
  + (* Ireturn *) intros; eapply exec_Sreturn; simpl; eauto.
    destruct or; simpl; auto.
Admitted.

Lemma sfstep_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 ->
  sfmatch pge ge sp st stack f rs0 m0 (sfstep i (si_local st)) rs m t s ->
  sistep 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_set_local in Hi; 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.
  + (* 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_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 ge sp pc rs m: ssem ge sp (init_sistate pc) rs m (mk_istate true pc rs m).
Proof.
  unfold ssem, ssem_local, all_fallthrough; simpl. intuition.
Qed.

Definition sstep (f: function) (pc:node): option sstate :=
  SOME path <- (fn_path f)!pc IN
  SOME st <- sisteps path.(psize) f (init_sistate pc) IN
  SOME i <- (fn_code f)!(st.(si_pc)) IN
  Some (match sistep i st with
       | Some st' => {| internal := st'; final := Snone |}
       | None => {| internal := st; final := sfstep 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) ->
  sistep 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 [sstep]) 
(sstep is a correct over-approximation)
*)
Theorem sstep_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, sstep f pc = Some st /\ smatch pge ge sp st stack f rs m t s.
Proof.
(*    Local Hint Resolve init_ssem sistep_preserves_ssem_exits: core.
   intros PATH STEP; unfold sstep; rewrite PATH; simpl.
   lapply (final_node_path_simpl f path pc); eauto. intro WF.
   exploit (sisteps_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_opt2; destruct (sisteps _ _ _) as [st|] eqn: Hst; try congruence);
   (* intro SEM *)
   (simpl; unfold ssem; 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 sisteps_default_succ; eauto; simpl;
       intros DEF; rewrite DEF in Hi; auto 
       | clear Hi; rewrite Hi' ]);
   (* eexists *)
   (eexists; constructor; eauto).
   - (* early *)
     eapply smatch_early; eauto.
     unfold ssem; simpl; rewrite CONT.
     destruct (sistep i st) as [st'|] eqn: Hst'; simpl; eauto.
   - destruct SEM as (SEM & PC & HNYE).
     destruct (sistep 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 sistep_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 smatch_normal; simpl; eauto.
         unfold ssem in SEM.
         rewrite CONT in SEM.
         destruct SEM as (SEM & PC & HNYE).
         rewrite <- PC.
         eapply exec_Snone. }
       { eapply smatch_early; eauto. }
     + (* normal non-Snone instruction *) 
       eapply smatch_normal; eauto.
       * unfold ssem; simpl; rewrite CONT; intuition.
       * simpl. eapply sfstep_correct; eauto.
         rewrite PC; auto. *)
Admitted.

(* 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 sfmatch_equiv pge ge sp (f:function) st sv stack rs0 m0 t rs1 rs2 m s:
  sfmatch 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' /\ sfmatch 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. *) admit.
Admitted.

(* NB: each execution of a symbolic state (produced from [sstep]) represents a concrete execution
  (sstep is exact).
*)
Theorem sstep_exact f pc pge ge sp path stack st rs m t s1: 
  (fn_path f)!pc = Some path ->
  sstep f pc = Some st -> 
  smatch 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: core.
  unfold sstep; intros PATH SSTEP SEM; rewrite PATH in SSTEP.
  lapply (final_node_path_simpl f path pc); eauto. intro WF.
  exploit (sisteps_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 (sisteps path.(psize) f (init_sistate pc)) as [st0|] eqn: Hst0; simpl.
  2:{ (* absurd case *)
      exploit sisteps_WF; eauto.
      simpl; intros NDS; rewrite NDS in Hi; congruence. }
  exploit sisteps_default_succ; eauto; simpl.
  intros NDS; rewrite NDS in Hi.
  rewrite Hi in SSTEP.
  intros ISTEPS. try_simplify_someHyps.
  destruct (sistep 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 ssem_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_opt_determ; eauto.
      destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4).
      unfold ssem in SEM1.
      rewrite CONT in SEM1. destruct SEM1 as (SEM1 & PC0 & NYE0).
      exploit sfmatch_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 sfstep_complete; eauto.
      * congruence.
      * unfold ssem_local 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_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 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 RTLpathLiveproofs.

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) 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.(ipc)) = Some path 
     /\ istate_simulive (fun r => Regset.In r path.(input_regs)) srce is1 is2
     /\ srce!(is2.(ipc)) = Some is1.(ipc).

(* NOTE: a pure semantic definition on [sistate], for a total freedom in refinements *)
Definition sistate_simu (f: RTLpath.function) (srce: PTree.t node) (st1 st2: sistate): 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, ssem ge1 sp st1 rs m is1 -> 
     exists is2, ssem 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 sstate_simu f srce (s1 s2: sstate): Prop :=
       sistate_simu f srce s1.(internal) s2.(internal)
    /\ sfval_simu f srce s1.(si_pc) s2.(si_pc) s1.(final) s2.(final).

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

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