diff options
Diffstat (limited to 'kvx/lib/RTLpathSE_theory.v')
| -rw-r--r-- | kvx/lib/RTLpathSE_theory.v | 1336 |
1 files changed, 1336 insertions, 0 deletions
diff --git a/kvx/lib/RTLpathSE_theory.v b/kvx/lib/RTLpathSE_theory.v new file mode 100644 index 00000000..b0dcbe80 --- /dev/null +++ b/kvx/lib/RTLpathSE_theory.v @@ -0,0 +1,1336 @@ +(* 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®) 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®) 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 RTLpathLivegenproof. + +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]. +*) |