Module RTLpathSE_theory


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

Local Open Scope error_monad_scope.

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

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


Syntax and semantics of symbolic values


Inductive sval :=
  | Sinput (r: reg)
  | Sop (op:operation) (lsv: list_sval) (sm: smem)
  | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval)
with list_sval :=
  | Snil
  | Scons (sv: sval) (lsv: list_sval)
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 Vundef
          | Some a =>
              SOME m <- seval_smem ge sp sm rs0 m0 IN
              match (Mem.loadv chunk m a) with
              | None => Some Vundef
              | 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.

Record sistate_local := { si_pre: RTL.genv -> val -> regset -> mem -> Prop; si_sreg: reg -> sval; si_smem: smem }.

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.

Record sistate_exit := mk_sistate_exit
  { si_cond: condition; si_scondargs: list_sval; si_elocal: sistate_local; si_ifso: node }.

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

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

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

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

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

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


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

Definition sabort (ge: RTL.genv) (sp: val) (st: sistate) (rs: regset) (m: mem): Prop :=
  (all_fallthrough ge sp st.(si_exits) rs m /\ sabort_local ge sp st.(si_local) rs m)
  \/ (exists ext lx, all_fallthrough_upto_exit ge sp ext lx st.(si_exits) rs m /\ sabort_exit ge sp ext rs m).

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

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

An internal state represents a parallel program ! We prove below that the semantics ssem_internal_opt is deterministic.


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Symbolic execution of one internal step


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

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

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

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

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

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

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

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

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

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

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

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

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


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

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


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

Symbolic execution of the internal steps of a path

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

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

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

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

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

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

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

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

REM: in the following two unused lemmas

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

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

Symbolic (final) value of a path

Inductive sfval :=
  | Snone
  | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:node)
  | Stailcall: signature -> sval + ident -> list_sval -> sfval
  | Sbuiltin (ef:external_function) (sargs: list (builtin_arg sval)) (res: builtin_res reg) (pc:node)
  | Sjumptable (sv: sval) (tbl: list node)
  | Sreturn: option sval -> sfval
.

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

Section SEVAL_BUILTIN_ARG.

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

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

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

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

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

End SEVAL_BUILTIN_ARG.

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

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

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

Fixpoint builtin_arg_map {A B} (f: A -> B) (arg: builtin_arg A) : builtin_arg B :=
  match arg with
  | BA x => BA (f x)
  | BA_int n => BA_int n
  | BA_long n => BA_long n
  | BA_float f => BA_float f
  | BA_single s => BA_single s
  | BA_loadstack chunk ptr => BA_loadstack chunk ptr
  | BA_addrstack ptr => BA_addrstack ptr
  | BA_loadglobal chunk id ptr => BA_loadglobal chunk id ptr
  | BA_addrglobal id ptr => BA_addrglobal id ptr
  | BA_splitlong ba1 ba2 => BA_splitlong (builtin_arg_map f ba1) (builtin_arg_map f ba2)
  | BA_addptr ba1 ba2 => BA_addptr (builtin_arg_map f ba1) (builtin_arg_map f ba2)
  end.

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

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

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

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

Symbolic execution of final step

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

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

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

Main function of the symbolic execution


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Simulation of RTLpath code w.r.t symbolic execution


Section SymbValPreserved.

Variable ge ge': RTL.genv.

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

Hypothesis senv_preserved_RTL: Senv.equiv ge ge'.

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

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

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

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

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

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

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

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

End SymbValPreserved.

Require Import RTLpathLivegen RTLpathLivegenproof.

DEFINITION OF SIMULATION BETWEEN (ABSTRACT) SYMBOLIC EXECUTIONS


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

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

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

Definition sistate_simu (dm: PTree.t node) (f: RTLpath.function) outframe (st1 st2: sistate) (ctx: simu_proof_context f): Prop :=
  forall is1, ssem_internal (the_ge1 ctx) (the_sp ctx) st1 (the_rs0 ctx) (the_m0 ctx) is1 ->
  exists is2, ssem_internal (the_ge2 ctx) (the_sp ctx) st2 (the_rs0 ctx) (the_m0 ctx) is2
              /\ istate_simu f dm outframe is1 is2.

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


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

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

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

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


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

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

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

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

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

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

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

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

Inductive sfval_simu (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node) (ctx: simu_proof_context f): sfval -> sfval -> Prop :=
  | Snone_simu:
      dm!opc2 = Some opc1 ->
      sfval_simu dm f opc1 opc2 ctx Snone Snone
  | Scall_simu sig svos1 svos2 lsv1 lsv2 res pc1 pc2:
      dm!pc2 = Some pc1 ->
      svident_simu f ctx svos1 svos2 ->
      (seval_list_sval (the_ge1 ctx) (the_sp ctx) lsv1 (the_rs0 ctx) (the_m0 ctx))
      = (seval_list_sval (the_ge2 ctx) (the_sp ctx) lsv2 (the_rs0 ctx) (the_m0 ctx)) ->
      sfval_simu dm f opc1 opc2 ctx (Scall sig svos1 lsv1 res pc1) (Scall sig svos2 lsv2 res pc2)
  | Stailcall_simu sig svos1 svos2 lsv1 lsv2:
      svident_simu f ctx svos1 svos2 ->
      (seval_list_sval (the_ge1 ctx) (the_sp ctx) lsv1 (the_rs0 ctx) (the_m0 ctx))
      = (seval_list_sval (the_ge2 ctx) (the_sp ctx) lsv2 (the_rs0 ctx) (the_m0 ctx)) ->
      sfval_simu dm f opc1 opc2 ctx (Stailcall sig svos1 lsv1) (Stailcall sig svos2 lsv2)
  | Sbuiltin_simu ef lbs1 lbs2 br pc1 pc2:
      dm!pc2 = Some pc1 ->
      (seval_list_builtin_sval (the_ge1 ctx) (the_sp ctx) lbs1 (the_rs0 ctx) (the_m0 ctx))
      = (seval_list_builtin_sval (the_ge2 ctx) (the_sp ctx) lbs2 (the_rs0 ctx) (the_m0 ctx)) ->
      sfval_simu dm f opc1 opc2 ctx (Sbuiltin ef lbs1 br pc1) (Sbuiltin ef lbs2 br pc2)
  | Sjumptable_simu sv1 sv2 lpc1 lpc2:
      ptree_get_list dm lpc2 = Some lpc1 ->
      (seval_sval (the_ge1 ctx) (the_sp ctx) sv1 (the_rs0 ctx) (the_m0 ctx))
      = (seval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx)) ->
      sfval_simu dm f opc1 opc2 ctx (Sjumptable sv1 lpc1) (Sjumptable sv2 lpc2)
  | Sreturn_simu_none: sfval_simu dm f opc1 opc2 ctx (Sreturn None) (Sreturn None)
  | Sreturn_simu_some sv1 sv2:
      (seval_sval (the_ge1 ctx) (the_sp ctx) sv1 (the_rs0 ctx) (the_m0 ctx))
      = (seval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx)) ->
      sfval_simu dm f opc1 opc2 ctx (Sreturn (Some sv1)) (Sreturn (Some sv2)).

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

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