From d765f2d91cadfaa325ef623edec6caeac1729906 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 22 Apr 2020 18:13:59 +0200 Subject: Started general renaming for clearer and more understandable code --- mppa_k1c/lib/RTLpath.v | 112 ++++++------- mppa_k1c/lib/RTLpathLiveproofs.v | 34 ++-- mppa_k1c/lib/RTLpathSE_theory.v | 347 +++++++++++++++++++-------------------- 3 files changed, 243 insertions(+), 250 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/lib/RTLpath.v b/mppa_k1c/lib/RTLpath.v index 35f6e715..7134de10 100644 --- a/mppa_k1c/lib/RTLpath.v +++ b/mppa_k1c/lib/RTLpath.v @@ -141,36 +141,36 @@ Coercion program_RTL: program >-> RTL.program. (* Semantics of internal instructions (mimicking RTL semantics) *) -Record istate := ist { continue: bool; the_pc: node; the_rs: regset; the_mem: mem }. +Record istate := mk_istate { icontinue: bool; ipc: node; irs: regset; imem: mem }. (* FIXME - prediction *) (* Internal step through the path *) Definition istep (ge: RTL.genv) (i: instruction) (sp: val) (rs: regset) (m: mem): option istate := match i with - | Inop pc' => Some (ist true pc' rs m) + | Inop pc' => Some (mk_istate true pc' rs m) | Iop op args res pc' => SOME v <- eval_operation ge sp op rs##args m IN - Some (ist true pc' (rs#res <- v) m) + Some (mk_istate true pc' (rs#res <- v) m) | Iload TRAP chunk addr args dst pc' => SOME a <- eval_addressing ge sp addr rs##args IN SOME v <- Mem.loadv chunk m a IN - Some (ist true pc' (rs#dst <- v) m) + Some (mk_istate true pc' (rs#dst <- v) m) | Iload NOTRAP chunk addr args dst pc' => - let default_state := ist true pc' rs#dst <- (default_notrap_load_value chunk) m in + let default_state := mk_istate true pc' rs#dst <- (default_notrap_load_value chunk) m in match (eval_addressing ge sp addr rs##args) with | None => Some default_state | Some a => match (Mem.loadv chunk m a) with | None => Some default_state - | Some v => Some (ist true pc' (rs#dst <- v) m) + | Some v => Some (mk_istate true pc' (rs#dst <- v) m) end end | Istore chunk addr args src pc' => SOME a <- eval_addressing ge sp addr rs##args IN SOME m' <- Mem.storev chunk m a rs#src IN - Some (ist true pc' rs m') + Some (mk_istate true pc' rs m') | Icond cond args ifso ifnot _ => SOME b <- eval_condition cond rs##args m IN - Some (ist (negb b) (if b then ifso else ifnot) rs m) + Some (mk_istate (negb b) (if b then ifso else ifnot) rs m) | _ => None (* TODO jumptable ? *) end. @@ -179,12 +179,12 @@ Definition istep (ge: RTL.genv) (i: instruction) (sp: val) (rs: regset) (m: mem) (* Executes until a state [st] is reached where st.(continue) is false *) Fixpoint isteps ge (path:nat) (f: function) sp rs m pc: option istate := match path with - | O => Some (ist true pc rs m) + | O => Some (mk_istate true pc rs m) | S p => SOME i <- (fn_code f)!pc IN SOME st <- istep ge i sp rs m IN - if st.(continue) then - isteps ge p f sp st.(the_rs) st.(the_mem) st.(the_pc) + if (icontinue st) then + isteps ge p f sp (irs st) (imem st) (ipc st) else Some st end. @@ -252,7 +252,7 @@ Inductive path_last_step ge pge stack (f: function): val -> node -> regset -> me (fn_code f)!pc = Some i -> istep ge i sp rs m = Some st -> path_last_step ge pge stack f sp pc rs m - E0 (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)) + E0 (State stack f sp (ipc st) (irs st) (imem st)) | exec_Icall sp pc rs m sig ros args res pc' fd: (fn_code f)!pc = Some(Icall sig ros args res pc') -> find_function pge ros rs = Some fd -> @@ -288,12 +288,12 @@ Inductive path_last_step ge pge stack (f: function): val -> node -> regset -> me Inductive path_step ge pge (path:nat) stack f sp rs m pc: trace -> state -> Prop := | exec_early_exit st: isteps ge path f sp rs m pc = Some st -> - st.(continue) = false -> - path_step ge pge path stack f sp rs m pc E0 (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)) + (icontinue st) = false -> + path_step ge pge path stack f sp rs m pc E0 (State stack f sp (ipc st) (irs st) (imem st)) | exec_normal_exit st t s: isteps ge path f sp rs m pc = Some st -> - st.(continue) = true -> - path_last_step ge pge stack f sp st.(the_pc) st.(the_rs) st.(the_mem) t s -> + (icontinue st) = true -> + path_last_step ge pge stack f sp (ipc st) (irs st) (imem st) t s -> path_step ge pge path stack f sp rs m pc t s. (* Either internal path execution, or the usual exec_function / exec_return borrowed from RTL *) @@ -396,7 +396,7 @@ Local Hint Resolve RTL.exec_Inop RTL.exec_Iop RTL.exec_Iload RTL.exec_Istore RTL Lemma istep_correct ge i stack (f:function) sp rs m st : istep ge i sp rs m = Some st -> forall pc, (fn_code f)!pc = Some i -> - RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)). + RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(ipc) st.(irs) st.(imem)). Proof. destruct i; simpl; try congruence; simplify_SOME x. 1-3: explore_destruct; simplify_SOME x. @@ -407,12 +407,12 @@ Local Hint Resolve star_refl: core. (* isteps reflects a star relation on RTL.step *) Lemma isteps_correct ge path stack f sp: forall rs m pc st, isteps ge path f sp rs m pc = Some st -> - star RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)). + star RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(ipc) st.(irs) st.(imem)). Proof. induction path; simpl; try_simplify_someHyps. inversion_SOME i; intros Hi. inversion_SOME st0; intros Hst0. - destruct (continue st0) eqn:cont. + destruct (icontinue st0) eqn:cont. + intros; eapply star_step. - eapply istep_correct; eauto. - simpl; eauto. @@ -425,13 +425,13 @@ Qed. Lemma isteps_correct_early_exit ge path stack f sp: forall rs m pc st, isteps ge path f sp rs m pc = Some st -> - st.(continue) = false -> - plus RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)). + st.(icontinue) = false -> + plus RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(ipc) st.(irs) st.(imem)). Proof. destruct path; simpl; try_simplify_someHyps; try congruence. inversion_SOME i; intros Hi. inversion_SOME st0; intros Hst0. - destruct (continue st0) eqn:cont. + destruct (icontinue st0) eqn:cont. + intros; eapply plus_left. - eapply istep_correct; eauto. - eapply isteps_correct; eauto. @@ -609,7 +609,7 @@ Local Opaque path_entry. Lemma istep_successors ge i sp rs m st: istep ge i sp rs m = Some st -> - In (the_pc st) (successors_instr i). + In (ipc st) (successors_instr i). Proof. destruct i; simpl; try congruence; simplify_SOME x. all: explore_destruct; simplify_SOME x. @@ -617,23 +617,23 @@ Qed. Lemma istep_normal_exit ge i sp rs m st: istep ge i sp rs m = Some st -> - st.(continue) = true -> - default_succ i = Some st.(the_pc). + st.(icontinue) = true -> + default_succ i = Some st.(ipc). Proof. destruct i; simpl; try congruence; simplify_SOME x. all: explore_destruct; simplify_SOME x. Qed. Lemma isteps_normal_exit ge path f sp: forall rs m pc st, - st.(continue) = true -> + st.(icontinue) = true -> isteps ge path f sp rs m pc = Some st -> - nth_default_succ (fn_code f) path pc = Some st.(the_pc). + nth_default_succ (fn_code f) path pc = Some st.(ipc). Proof. induction path; simpl. { try_simplify_someHyps. } intros rs m pc st CONT; try_simplify_someHyps. inversion_SOME i; intros Hi. inversion_SOME st0; intros Hst0. - destruct (continue st0) eqn:X; try congruence. + destruct (icontinue st0) eqn:X; try congruence. try_simplify_someHyps. intros; erewrite istep_normal_exit; eauto. Qed. @@ -644,9 +644,9 @@ Qed. *) Lemma isteps_step_right ge path f sp: forall rs m pc st i, isteps ge path f sp rs m pc = Some st -> - st.(continue) = true -> - (fn_code f)!(st.(the_pc)) = Some i -> - istep ge i sp st.(the_rs) st.(the_mem) = isteps ge (S path) f sp rs m pc. + st.(icontinue) = true -> + (fn_code f)!(st.(ipc)) = Some i -> + istep ge i sp st.(irs) st.(imem) = isteps ge (S path) f sp rs m pc. Proof. induction path. + simpl; intros; try_simplify_someHyps. simplify_SOME st. @@ -654,25 +654,25 @@ Proof. + intros rs m pc st i H. simpl in H. generalize H; clear H; simplify_SOME xx. - destruct (continue xx0) eqn: CONTxx0. + destruct (icontinue xx0) eqn: CONTxx0. * intros; erewrite IHpath; eauto. * intros; congruence. Qed. Lemma isteps_inversion_early ge path f sp: forall rs m pc st, isteps ge path f sp rs m pc = Some st -> - (continue st)=false -> + (icontinue st)=false -> exists st0 i path0, (path > path0)%nat /\ isteps ge path0 f sp rs m pc = Some st0 /\ - st0.(continue) = true /\ - (fn_code f)!(st0.(the_pc)) = Some i /\ - istep ge i sp st0.(the_rs) st0.(the_mem) = Some st. + st0.(icontinue) = true /\ + (fn_code f)!(st0.(ipc)) = Some i /\ + istep ge i sp st0.(irs) st0.(imem) = Some st. Proof. induction path as [|path]; simpl. - intros; try_simplify_someHyps; try congruence. - intros rs m pc st; inversion_SOME i; inversion_SOME st0. - destruct (continue st0) eqn: CONT. + destruct (icontinue st0) eqn: CONT. + intros STEP PC STEPS CONT0. exploit IHpath; eauto. clear STEPS. intros (st1 & i0 & path0 & BOUND & STEP1 & CONT1 & X1 & X2); auto. @@ -687,7 +687,7 @@ Qed. Lemma isteps_resize ge path0 path1 f sp rs m pc st: (path0 <= path1)%nat -> isteps ge path0 f sp rs m pc = Some st -> - (continue st)=false -> + (icontinue st)=false -> isteps ge path1 f sp rs m pc = Some st. Proof. induction 1 as [|path1]; simpl; auto. @@ -696,7 +696,7 @@ Proof. induction path1 as [|path]; simpl; auto. - intros; try_simplify_someHyps; try congruence. - intros rs m pc st; inversion_SOME i; inversion_SOME st0; intros; try_simplify_someHyps. - destruct (continue st0) eqn: CONT0; eauto. + destruct (icontinue st0) eqn: CONT0; eauto. Qed. (* FIXME - add prediction *) @@ -707,8 +707,8 @@ Inductive is_early_exit pc: instruction -> Prop := Lemma istep_early_exit ge i sp rs m st : istep ge i sp rs m = Some st -> - st.(continue) = false -> - st.(the_rs) = rs /\ st.(the_mem) = m /\ is_early_exit st.(the_pc) i. + st.(icontinue) = false -> + st.(irs) = rs /\ st.(imem) = m /\ is_early_exit st.(ipc) i. Proof. Local Hint Resolve Icond_early_exit: core. destruct i; simpl; try congruence; simplify_SOME b; simpl; try congruence. @@ -782,7 +782,7 @@ Inductive match_inst_states_goal (idx: nat) (s1:RTL.state): state -> Prop := (fn_path f)!pc = Some path -> (idx <= path.(psize))%nat -> isteps ge (path.(psize)-idx) f sp rs m pc = Some s2 -> - s1 = State stack f sp s2.(the_pc) s2.(the_rs) s2.(the_mem) -> + s1 = State stack f sp s2.(ipc) s2.(irs) s2.(imem) -> match_inst_states_goal idx s1 (State stack f sp pc rs m). Definition match_inst_states (idx: nat) (s1:RTL.state) (s2:state): Prop := @@ -797,7 +797,7 @@ Lemma istep_complete t i stack f sp rs m pc s': RTL.step ge (State stack f sp pc rs m) t s' -> (fn_code f)!pc = Some i -> default_succ i <> None -> - t = E0 /\ exists st, istep ge i sp rs m = Some st /\ s'=(State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)). + t = E0 /\ exists st, istep ge i sp rs m = Some st /\ s'=(State stack f sp st.(ipc) st.(irs) st.(imem)). Proof. intros H X; inversion H; simpl; subst; try rewrite X in * |-; clear X; simplify_someHyps; try congruence; (split; auto); simplify_someHyps; eexists; split; simplify_someHyps; eauto. @@ -808,8 +808,8 @@ Lemma stuttering path idx stack f sp rs m pc st t s1': isteps ge (path.(psize)-(S idx)) f sp rs m pc = Some st -> (fn_path f)!pc = Some path -> (S idx <= path.(psize))%nat -> - st.(continue) = true -> - RTL.step ge (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)) t s1' -> + st.(icontinue) = true -> + RTL.step ge (State stack f sp st.(ipc) st.(irs) st.(imem)) t s1' -> t = E0 /\ match_inst_states idx s1' (State stack f sp pc rs m). Proof. intros PSTEP PATH BOUND CONT RSTEP; exploit (internal_node_path (path.(psize)-(S idx))); omega || eauto. @@ -827,11 +827,11 @@ Qed. Lemma normal_exit path stack f sp rs m pc st t s1': isteps ge path.(psize) f sp rs m pc = Some st -> (fn_path f)!pc = Some path -> - st.(continue) = true -> - RTL.step ge (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)) t s1' -> + st.(icontinue) = true -> + RTL.step ge (State stack f sp st.(ipc) st.(irs) st.(imem)) t s1' -> wf_stackframe stack -> exists s2', - (path_last_step ge pge stack f sp st.(the_pc) st.(the_rs) st.(the_mem)) t s2' + (path_last_step ge pge stack f sp st.(ipc) st.(irs) st.(imem)) t s2' /\ (exists idx', match_states idx' s1' s2'). Proof. Local Hint Resolve istep_successors list_nth_z_in: core. (* Hint for path_entry proofs *) @@ -846,7 +846,7 @@ Proof. exploit (exec_istate ge pge); eauto. eexists; intuition eauto. unfold match_states, match_inst_states; simpl. - destruct (initialize_path (*fn_code f*) (fn_path f) (the_pc st0)) as (path0 & Hpath0); eauto. + destruct (initialize_path (*fn_code f*) (fn_path f) (ipc st0)) as (path0 & Hpath0); eauto. exists (path0.(psize)); intuition eauto. econstructor; eauto. * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega. @@ -893,19 +893,19 @@ Lemma path_step_complete stack f sp rs m pc t s1' idx path st: isteps ge (path.(psize)-idx) f sp rs m pc = Some st -> (fn_path f)!pc = Some path -> (idx <= path.(psize))%nat -> - RTL.step ge (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)) t s1' -> + RTL.step ge (State stack f sp st.(ipc) st.(irs) st.(imem)) t s1' -> wf_stackframe stack -> exists idx' s2', (path_step ge pge path.(psize) stack f sp rs m pc t s2' \/ (t = E0 /\ s2'=(State stack f sp pc rs m) /\ (idx' < idx)%nat) - \/ (exists path', path_step ge pge path.(psize) stack f sp rs m pc E0 (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)) - /\ (fn_path f)!(the_pc st) = Some path' /\ path'.(psize) = O - /\ path_step ge pge path'.(psize) stack f sp st.(the_rs) st.(the_mem) st.(the_pc) t s2') + \/ (exists path', path_step ge pge path.(psize) stack f sp rs m pc E0 (State stack f sp st.(ipc) st.(irs) st.(imem)) + /\ (fn_path f)!(ipc st) = Some path' /\ path'.(psize) = O + /\ path_step ge pge path'.(psize) stack f sp st.(irs) st.(imem) st.(ipc) t s2') ) /\ match_states idx' s1' s2'. Proof. Local Hint Resolve exec_early_exit exec_normal_exit: core. - intros PSTEP PATH BOUND RSTEP WF; destruct (st.(continue)) eqn: CONT. + intros PSTEP PATH BOUND RSTEP WF; destruct (st.(icontinue)) eqn: CONT. destruct idx as [ | idx]. + (* path_step on normal_exit *) assert (path.(psize)-0=path.(psize))%nat as HH by omega. rewrite HH in PSTEP. clear HH. @@ -920,7 +920,7 @@ Proof. exploit (isteps_resize ge (path.(psize) - idx)%nat path.(psize)); eauto; try omega. clear PSTEP; intros PSTEP. (* TODO for clarification: move the assert below into a separate lemma *) - assert (HPATH0: exists path0, (fn_path f)!(the_pc st) = Some path0). + assert (HPATH0: exists path0, (fn_path f)!(ipc st) = Some path0). { clear RSTEP. exploit isteps_inversion_early; eauto. intros (st0 & i & path0 & BOUND0 & PSTEP0 & CONT0 & PC0 & STEP0). @@ -948,7 +948,7 @@ Proof. - simpl; eauto. - simpl; eauto. * (* single step case *) - exploit (stuttering path1 ps stack f sp (the_rs st) (the_mem st) (the_pc st)); simpl; auto. + exploit (stuttering path1 ps stack f sp (irs st) (imem st) (ipc st)); simpl; auto. - { rewrite Hpath1size; enough (S ps-S ps=0)%nat as ->; try omega. simpl; eauto. } - omega. - simpl; eauto. diff --git a/mppa_k1c/lib/RTLpathLiveproofs.v b/mppa_k1c/lib/RTLpathLiveproofs.v index a807279b..8e2c22cd 100644 --- a/mppa_k1c/lib/RTLpathLiveproofs.v +++ b/mppa_k1c/lib/RTLpathLiveproofs.v @@ -98,10 +98,10 @@ Proof. Qed. Record eqlive_istate alive (st1 st2: istate): Prop := - { eqlive_continue: continue st1 = continue st2; - eqlive_the_pc: the_pc st1 = the_pc st2; - eqlive_the_rs: eqlive_reg alive (the_rs st1) (the_rs st2); - eqlive_the_mem: (the_mem st1) = (the_mem st2) }. + { eqlive_continue: icontinue st1 = icontinue st2; + eqlive_ipc: ipc st1 = ipc st2; + eqlive_irs: eqlive_reg alive (irs st1) (irs st2); + eqlive_imem: (imem st1) = (imem st2) }. Lemma iinst_checker_eqlive ge sp pm alive i res rs1 rs2 m st1: eqlive_reg (ext alive) rs1 rs2 -> @@ -174,8 +174,8 @@ Qed. Lemma iinst_checker_istep_continue ge sp pm alive i res rs m st: iinst_checker pm alive i = Some res -> istep ge i sp rs m = Some st -> - continue st = true -> - (snd res)=(the_pc st). + icontinue st = true -> + (snd res)=(ipc st). Proof. intros; exploit iinst_checker_default_succ; eauto. erewrite istep_normal_exit; eauto. @@ -199,8 +199,8 @@ Lemma iinst_checker_eqlive_stopped ge sp pm alive i res rs1 rs2 m st1: eqlive_reg (ext alive) rs1 rs2 -> istep ge i sp rs1 m = Some st1 -> iinst_checker pm alive i = Some res -> - continue st1 = false -> - exists path st2, pm!(the_pc st1) = Some path /\ istep ge i sp rs2 m = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2. + icontinue st1 = false -> + exists path st2, pm!(ipc st1) = Some path /\ istep ge i sp rs2 m = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2. Proof. intros EQLIVE. set (tmp := istep ge i sp rs2). @@ -220,7 +220,7 @@ Lemma ipath_checker_eqlive_normal ge ps (f:function) sp pm: forall alive pc res eqlive_reg (ext alive) rs1 rs2 -> ipath_checker ps f pm alive pc = Some res -> isteps ge ps f sp rs1 m pc = Some st1 -> - continue st1 = true -> + icontinue st1 = true -> exists st2, isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext (fst res)) st1 st2. Proof. induction ps as [|ps]; simpl; try_simplify_someHyps. @@ -233,7 +233,7 @@ Proof. destruct 1 as (st2 & ISTEP & [CONT PC RS MEM]). try_simplify_someHyps. rewrite <- CONT, <- MEM, <- PC. - destruct (continue st0) eqn:CONT'. + destruct (icontinue st0) eqn:CONT'. * intros; exploit iinst_checker_istep_continue; eauto. rewrite <- PC; intros X; rewrite X in * |-. eauto. * try_simplify_someHyps. @@ -243,14 +243,14 @@ Qed. Lemma ipath_checker_isteps_continue ge ps (f:function) sp pm: forall alive pc res rs m st, ipath_checker ps f pm alive pc = Some res -> isteps ge ps f sp rs m pc = Some st -> - continue st = true -> - (snd res)=(the_pc st). + icontinue st = true -> + (snd res)=(ipc st). Proof. induction ps as [|ps]; simpl; try_simplify_someHyps. inversion_SOME i; try_simplify_someHyps. inversion_SOME res0. inversion_SOME st0. - destruct (continue st0) eqn:CONT'. + destruct (icontinue st0) eqn:CONT'. - intros; exploit iinst_checker_istep_continue; eauto. intros EQ; rewrite EQ in * |-; clear EQ; eauto. - try_simplify_someHyps; congruence. @@ -260,15 +260,15 @@ Lemma ipath_checker_eqlive_stopped ge ps (f:function) sp pm: forall alive pc res eqlive_reg (ext alive) rs1 rs2 -> ipath_checker ps f pm alive pc = Some res -> isteps ge ps f sp rs1 m pc = Some st1 -> - continue st1 = false -> - exists path st2, pm!(the_pc st1) = Some path /\ isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2. + icontinue st1 = false -> + exists path st2, pm!(ipc st1) = Some path /\ isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2. Proof. induction ps as [|ps]; simpl; try_simplify_someHyps; try congruence. inversion_SOME i; try_simplify_someHyps. inversion_SOME res0. inversion_SOME st0. intros. - destruct (continue st0) eqn:CONT'; try_simplify_someHyps; intros. + destruct (icontinue st0) eqn:CONT'; try_simplify_someHyps; intros. * intros; exploit iinst_checker_eqlive; eauto. destruct 1 as (st2 & ISTEP & [CONT PC RS MEM]). exploit iinst_checker_istep_continue; eauto. @@ -452,7 +452,7 @@ Proof. intros PC ISTEP. erewrite inst_checker_from_iinst_checker; eauto. inversion_SOME res. intros. - destruct (continue st1) eqn: CONT. + destruct (icontinue st1) eqn: CONT. - (* CONT => true *) exploit iinst_checker_eqlive; eauto. destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]). diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v index 1caea687..9c0c0c0a 100644 --- a/mppa_k1c/lib/RTLpathSE_theory.v +++ b/mppa_k1c/lib/RTLpathSE_theory.v @@ -47,103 +47,104 @@ Fixpoint list_sval_inj (l: list sval): list_sval := Local Open Scope option_monad_scope. (* FIXME - add non trapping load eval *) -Fixpoint sval_eval (ge: RTL.genv) (sp:val) (sv: sval) (rs0: regset) (m0: mem): option val := +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 <- list_sval_eval ge sp l rs0 m0 IN - SOME m <- smem_eval ge sp sm rs0 m0 IN + SOME args <- seval_list_sval ge sp l rs0 m0 IN + SOME m <- seval_smem ge sp sm rs0 m0 IN eval_operation ge sp op args m | Sload sm chunk addr lsv => - SOME args <- list_sval_eval ge sp lsv rs0 m0 IN + SOME args <- seval_list_sval ge sp lsv rs0 m0 IN SOME a <- eval_addressing ge sp addr args IN - SOME m <- smem_eval ge sp sm rs0 m0 IN + SOME m <- seval_smem ge sp sm rs0 m0 IN Mem.loadv chunk m a end -with list_sval_eval (ge: RTL.genv) (sp:val) (lsv: list_sval) (rs0: regset) (m0: mem): option (list val) := +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 <- sval_eval ge sp sv rs0 m0 IN - SOME lv <- list_sval_eval ge sp lsv' rs0 m0 IN + 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 smem_eval (ge: RTL.genv) (sp:val) (sm: smem) (rs0: regset) (m0: mem): option mem := +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 <- list_sval_eval ge sp lsv rs0 m0 IN + SOME args <- seval_list_sval ge sp lsv rs0 m0 IN SOME a <- eval_addressing ge sp addr args IN - SOME m <- smem_eval ge sp sm rs0 m0 IN - SOME sv <- sval_eval ge sp srce rs0 m0 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 *) -Record local_istate := { pre: RTL.genv -> val -> regset -> mem -> Prop; the_sreg: reg -> sval; the_smem: smem }. +(* [si_pre] is a precondition on initial ge, sp, rs0, m0 *) +Record sistate_local := { si_pre: RTL.genv -> val -> regset -> mem -> Prop; si_sreg: reg -> sval; si_smem: smem }. -Definition sem_local_istate (ge: RTL.genv) (sp:val) (st: local_istate) (rs0: regset) (m0: mem) (rs: regset) (m: mem): Prop := - st.(pre) ge sp rs0 m0 - /\ smem_eval ge sp st.(the_smem) rs0 m0 = Some m - /\ forall (r:reg), sval_eval ge sp (st.(the_sreg) r) rs0 m0 = Some (rs#r). +Definition smatch_local (ge: RTL.genv) (sp:val) (st: sistate_local) (rs0: regset) (m0: mem) (rs: regset) (m: mem): Prop := + st.(si_pre) ge sp rs0 m0 + /\ seval_smem ge sp st.(si_smem) rs0 m0 = Some m + /\ forall (r:reg), seval_sval ge sp (st.(si_sreg) r) rs0 m0 = Some (rs#r). -Definition has_aborted_on_basic (ge: RTL.genv) (sp:val) (st: local_istate) (rs0: regset) (m0: mem): Prop := - ~(st.(pre) ge sp rs0 m0) - \/ smem_eval ge sp st.(the_smem) rs0 m0 = None - \/ exists (r: reg), sval_eval ge sp (st.(the_sreg) r) rs0 m0 = None. +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 exit_istate := { the_cond: condition; cond_args: list_sval; exit_ist: local_istate; cond_ifso: node }. +Record sistate_exit := { si_cond: condition; si_scondargs: list_sval; si_elocal: sistate_local; si_ifso: node }. Definition seval_condition ge sp (cond: condition) (lsv: list_sval) (sm: smem) rs0 m0 : option bool := - SOME args <- list_sval_eval ge sp lsv rs0 m0 IN - SOME m <- smem_eval ge sp sm rs0 m0 IN + 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 has_not_yet_exit ge sp (lx: list exit_istate) rs0 m0: Prop := +Definition all_fallthrough ge sp (lx: list sistate_exit) rs0 m0: Prop := forall ext, List.In ext lx -> - seval_condition ge sp ext.(the_cond) ext.(cond_args) ext.(exit_ist).(the_smem) rs0 m0 = Some false. + seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = Some false. -Definition has_aborted_on_test ge sp (lx: list exit_istate) rs0 m0: Prop := +Definition sabort_exits ge sp (lx: list sistate_exit) rs0 m0: Prop := exists ext, List.In ext lx - /\ seval_condition ge sp ext.(the_cond) ext.(cond_args) ext.(exit_ist).(the_smem) rs0 m0 = None. + /\ seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = None. -Inductive sem_early_exit (ge: RTL.genv) (sp:val) (lx:list exit_istate) (rs0: regset) (m0: mem) rs m pc: Prop := - SEE_intro ext lx': +Inductive smatch_exits (ge: RTL.genv) (sp:val) (lx:list sistate_exit) (rs0: regset) (m0: mem) rs m pc: Prop := + smatch_exits_intro ext lx': is_tail (ext::lx') lx -> - has_not_yet_exit ge sp lx' rs0 m0 -> - seval_condition ge sp ext.(the_cond) ext.(cond_args) ext.(exit_ist).(the_smem) rs0 m0 = Some true -> - sem_local_istate ge sp ext.(exit_ist) rs0 m0 rs m -> - ext.(cond_ifso) = pc -> - sem_early_exit ge sp lx rs0 m0 rs m pc. + all_fallthrough ge sp lx' rs0 m0 -> + seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = Some true -> + smatch_local ge sp ext.(si_elocal) rs0 m0 rs m -> + ext.(si_ifso) = pc -> + smatch_exits ge sp lx rs0 m0 rs m pc. (** * Syntax and Semantics of symbolic internal state *) -Record s_istate := { the_pc: node; exits: list exit_istate; curr: local_istate }. +Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local }. -Definition sem_istate (ge: RTL.genv) (sp:val) (st: s_istate) (rs0: regset) (m0: mem) (is: istate): Prop := - if (is.(continue)) +Definition smatch (ge: RTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem) (is: istate): Prop := + if (is.(icontinue)) then - sem_local_istate ge sp st.(curr) rs0 m0 is.(the_rs) is.(the_mem) - /\ st.(the_pc) = is.(RTLpath.the_pc) - /\ has_not_yet_exit ge sp st.(exits) rs0 m0 - else sem_early_exit ge sp st.(exits) rs0 m0 is.(the_rs) is.(the_mem) is.(RTLpath.the_pc). + smatch_local ge sp st.(si_local) rs0 m0 is.(irs) is.(imem) + /\ st.(si_pc) = is.(ipc) + /\ all_fallthrough ge sp st.(si_exits) rs0 m0 + else smatch_exits ge sp st.(si_exits) rs0 m0 is.(irs) is.(imem) is.(ipc). -Definition has_aborted (ge: RTL.genv) (sp:val) (st: s_istate) (rs0: regset) (m0: mem): Prop := - has_aborted_on_basic ge sp st.(curr) rs0 m0 - \/ has_aborted_on_test ge sp st.(exits) rs0 m0. +Definition sabort (ge: RTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem): Prop := + sabort_local ge sp st.(si_local) rs0 m0 + \/ sabort_exits ge sp st.(si_exits) rs0 m0. -Definition sem_option_istate ge sp (st: s_istate) rs0 m0 (ois: option istate): Prop := +Definition smatch_opt ge sp (st: sistate) rs0 m0 (ois: option istate): Prop := match ois with - | Some is => sem_istate ge sp st rs0 m0 is - | None => has_aborted ge sp st rs0 m0 + | Some is => smatch ge sp st rs0 m0 is + | None => sabort ge sp st rs0 m0 end. -Definition sem_option2_istate ge sp (ost: option s_istate) rs0 m0 (ois: option istate) : Prop := +Definition smatch_opt2 ge sp (ost: option sistate) rs0 m0 (ois: option istate) : Prop := match ost with - | Some st => sem_option_istate ge sp st rs0 m0 ois + | Some st => smatch_opt ge sp st rs0 m0 ois | None => ois=None end. @@ -154,10 +155,10 @@ Definition sem_option2_istate ge sp (ost: option s_istate) rs0 m0 (ois: option i *) Definition istate_eq ist1 ist2 := - ist1.(continue) = ist2.(continue) /\ - ist1.(RTLpath.the_pc) = ist2.(RTLpath.the_pc) /\ - (forall r, (ist1.(the_rs)#r) = ist2.(the_rs)#r) /\ - ist1.(the_mem) = ist2.(the_mem). + ist1.(icontinue) = ist2.(icontinue) /\ + ist1.(ipc) = ist2.(ipc) /\ + (forall r, (ist1.(irs)#r) = ist2.(irs)#r) /\ + ist1.(imem) = ist2.(imem). (* TODO: is it useful Lemma has_not_yet_exit_cons_split ge sp ext lx rs0 m0: @@ -168,48 +169,48 @@ Proof. Qed. *) -Lemma exclude_early_NYE ge sp st rs0 m0 rs m pc: - sem_early_exit ge sp (exits st) rs0 m0 rs m pc -> - has_not_yet_exit ge sp (exits st) rs0 m0 -> +Lemma all_fallthrough_noexit ge sp st rs0 m0 rs m pc: + smatch_exits ge sp (si_exits st) rs0 m0 rs m pc -> + all_fallthrough ge sp (si_exits st) rs0 m0 -> False. Proof. Local Hint Resolve is_tail_in: core. destruct 1 as [ext lx' lc NYE' EVAL SEM PC]. subst. - unfold has_not_yet_exit; intros NYE; rewrite NYE in EVAL; eauto. + unfold all_fallthrough; intros NYE; rewrite NYE in EVAL; eauto. try congruence. Qed. -Lemma sem_istate_exclude_incompatible_continue ge sp st rs m is1 is2: - is1.(continue) = true -> - is2.(continue) = false -> - sem_istate ge sp st rs m is1 -> - sem_istate ge sp st rs m is2 -> +Lemma smatch_exclude_incompatible_continue ge sp st rs m is1 is2: + is1.(icontinue) = true -> + is2.(icontinue) = false -> + smatch ge sp st rs m is1 -> + smatch ge sp st rs m is2 -> False. Proof. - Local Hint Resolve exclude_early_NYE: core. - unfold sem_istate. + Local Hint Resolve all_fallthrough_noexit: core. + unfold smatch. intros CONT1 CONT2. rewrite CONT1, CONT2; simpl. intuition eauto. Qed. -Lemma sem_istate_determ_continue ge sp st rs m is1 is2: - sem_istate ge sp st rs m is1 -> - sem_istate ge sp st rs m is2 -> - is1.(continue) = is2.(continue). +Lemma smatch_determ_continue ge sp st rs m is1 is2: + smatch ge sp st rs m is1 -> + smatch ge sp st rs m is2 -> + is1.(icontinue) = is2.(icontinue). Proof. - Local Hint Resolve sem_istate_exclude_incompatible_continue: core. - destruct (Bool.bool_dec is1.(continue) is2.(continue)) as [|H]; auto. + Local Hint Resolve smatch_exclude_incompatible_continue: core. + destruct (Bool.bool_dec is1.(icontinue) is2.(icontinue)) as [|H]; auto. intros H1 H2. assert (absurd: False); intuition. - destruct (continue is1) eqn: His1, (continue is2) eqn: His2; eauto. + destruct (icontinue is1) eqn: His1, (icontinue is2) eqn: His2; eauto. Qed. -Lemma sem_local_istate_determ ge sp st rs0 m0 rs1 m1 rs2 m2: - sem_local_istate ge sp st rs0 m0 rs1 m1 -> - sem_local_istate ge sp st rs0 m0 rs2 m2 -> +Lemma smatch_local_determ ge sp st rs0 m0 rs1 m1 rs2 m2: + smatch_local ge sp st rs0 m0 rs1 m1 -> + smatch_local ge sp st rs0 m0 rs2 m2 -> (forall r, rs1#r = rs2#r) /\ m1 = m2. Proof. - unfold sem_local_istate. intuition try congruence. + unfold smatch_local. intuition try congruence. generalize (H5 r); rewrite H4; congruence. Qed. @@ -226,23 +227,23 @@ 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) -> - has_not_yet_exit ge sp lx1 rs0 m0 -> - seval_condition ge sp (the_cond ext1) (cond_args ext1) (the_smem (exit_ist ext1)) rs0 m0 = Some true -> - has_not_yet_exit ge sp lx2 rs0 m0 -> + 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 has_not_yet_exit in NYE. + unfold all_fallthrough in NYE. rewrite NYE in EVAL; eauto. try congruence. Qed. -Lemma sem_early_exit_determ ge sp lx rs0 m0 rs1 m1 pc1 rs2 m2 pc2 : - sem_early_exit ge sp lx rs0 m0 rs1 m1 pc1 -> - sem_early_exit ge sp lx rs0 m0 rs2 m2 pc2 -> +Lemma smatch_exits_determ ge sp lx rs0 m0 rs1 m1 pc1 rs2 m2 pc2 : + smatch_exits ge sp lx rs0 m0 rs1 m1 pc1 -> + smatch_exits ge sp lx rs0 m0 rs2 m2 pc2 -> pc1 = pc2 /\ (forall r, rs1#r = rs2#r) /\ m1 = m2. Proof. Local Hint Resolve exit_cond_determ eq_sym: core. @@ -250,31 +251,31 @@ Proof. destruct 1 as [ext2 lx2 TAIL2 NYE2 EVAL2 SEM2 PC2]; subst. assert (X:ext1=ext2). - destruct (is_tail_bounded_total (ext1 :: lx1) (ext2::lx2) lx) as [TAIL|TAIL]; eauto. - - subst. destruct (sem_local_istate_determ ge sp (exit_ist ext2) rs0 m0 rs1 m1 rs2 m2); auto. + - subst. destruct (smatch_local_determ ge sp (si_elocal ext2) rs0 m0 rs1 m1 rs2 m2); auto. Qed. -Lemma sem_istate_determ ge sp st rs m is1 is2: - sem_istate ge sp st rs m is1 -> - sem_istate ge sp st rs m is2 -> +Lemma smatch_determ ge sp st rs m is1 is2: + smatch ge sp st rs m is1 -> + smatch ge sp st rs m is2 -> istate_eq is1 is2. Proof. unfold istate_eq. intros SEM1 SEM2. - exploit (sem_istate_determ_continue ge sp st rs m is1 is2); eauto. - intros CONTEQ. unfold sem_istate in * |-. rewrite CONTEQ in * |- *. - destruct (continue is2). - - destruct (sem_local_istate_determ ge sp (curr st) rs m (the_rs is1) (the_mem is1) (the_rs is2) (the_mem is2)); + exploit (smatch_determ_continue ge sp st rs m is1 is2); eauto. + intros CONTEQ. unfold smatch in * |-. rewrite CONTEQ in * |- *. + destruct (icontinue is2). + - destruct (smatch_local_determ ge sp (si_local st) rs m (irs is1) (imem is1) (irs is2) (imem is2)); intuition (try congruence). - - destruct (sem_early_exit_determ ge sp (exits st) rs m (the_rs is1) (the_mem is1) (RTLpath.the_pc is1) (the_rs is2) (the_mem is2) (RTLpath.the_pc is2)); + - destruct (smatch_exits_determ ge sp (si_exits st) rs m (irs is1) (imem is1) (ipc is1) (irs is2) (imem is2) (ipc is2)); intuition. Qed. -Lemma sem_istate_exclude_abort_basic_continue ge sp st rs m is: - continue is = true -> - has_aborted_on_basic ge sp (curr st) rs m -> - sem_istate ge sp st rs m is -> False. +Lemma smatch_exclude_sabort_local_continue ge sp st rs m is: + icontinue is = true -> + sabort_local ge sp (si_local st) rs m -> + smatch ge sp st rs m is -> False. Proof. - intros CONT ABORT SEM. unfold sem_istate in SEM. rewrite CONT in SEM. + intros CONT ABORT SEM. unfold smatch in SEM. rewrite CONT in SEM. destruct SEM as (SEML & _ & _). inversion SEML as (SEML1 & SEML2 & SEML3); clear SEML. inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; clear ABORT. - contradiction. @@ -282,10 +283,10 @@ Proof. - inv ABORT3. rewrite SEML3 in H. discriminate. Qed. -Lemma sem_istate_exclude_abort_basic_nocontinue ge sp st rs0 m0 is: - continue is = false -> - has_aborted_on_basic ge sp (curr st) rs0 m0 -> - sem_istate ge sp st rs0 m0 is -> False. +Lemma smatch_exclude_sabort_local_nocontinue ge sp st rs0 m0 is: + icontinue is = false -> + sabort_local ge sp (si_local st) rs0 m0 -> + smatch ge sp st rs0 m0 is -> False. Proof. (* intros CONT ABORT SEM. unfold sem_istate in SEM. rewrite CONT in SEM. destruct st as [pc exits iis]. simpl in *. @@ -298,99 +299,91 @@ Proof. Admitted. -Lemma sem_istate_exclude_abort_basic ge sp st rs m is: - has_aborted_on_basic ge sp (curr st) rs m -> - sem_istate ge sp st rs m is -> False. +Lemma smatch_exclude_sabort_local ge sp st rs m is: + sabort_local ge sp (si_local st) rs m -> + smatch ge sp st rs m is -> False. Proof. - intros. destruct (continue is) eqn:CONT. - - eapply sem_istate_exclude_abort_basic_continue; eauto. - - eapply sem_istate_exclude_abort_basic_nocontinue; eauto. + intros. destruct (icontinue is) eqn:CONT. + - eapply smatch_exclude_sabort_local_continue; eauto. + - eapply smatch_exclude_sabort_local_nocontinue; eauto. Qed. -Lemma sem_istate_exclude_abort_test ge sp st rs m is: - has_aborted_on_test ge sp (exits st) rs m -> - sem_istate ge sp st rs m is -> False. +Lemma smatch_exclude_sabort_exits ge sp st rs m is: + sabort_exits ge sp (si_exits st) rs m -> + smatch ge sp st rs m is -> False. Proof. Admitted. - Lemma sem_istate_exclude_abort ge sp st rs m is: - has_aborted ge sp st rs m -> - sem_istate ge sp st rs m is -> False. - Proof. +Lemma smatch_exclude_sabort ge sp st rs m is: + sabort ge sp st rs m -> + smatch ge sp st rs m is -> False. +Proof. intros ABORT SEM. inv ABORT. - - eapply sem_istate_exclude_abort_basic; eauto. - - eapply sem_istate_exclude_abort_test; eauto. + - eapply smatch_exclude_sabort_local; eauto. + - eapply smatch_exclude_sabort_exits; eauto. Qed. - -(* - intros [[AB|[AB|AB]]|AB]; - ( unfold sem_istate, sem_local_istate; destruct (continue is) eqn: CONT; - [ intros (PRE & REG & MEM) | intros [ext lx' TAIL NYE COND (PRE®&MEM) PC] ]; intuition try congruence). - (* TODO: découper cette grosse preuve à faire en lemmes *) - Admitted. - *) - - -Definition istate_eq_option ist1 oist := +Definition istate_eq_opt ist1 oist := exists ist2, oist = Some ist2 /\ istate_eq ist1 ist2. -Lemma sem_option_istate_determ ge sp st rs m ois is: - sem_option_istate ge sp st rs m ois -> - sem_istate ge sp st rs m is -> - istate_eq_option is ois. +Lemma smatch_opt_determ ge sp st rs m ois is: + smatch_opt ge sp st rs m ois -> + smatch ge sp st rs m is -> + istate_eq_opt is ois. Proof. destruct ois as [is1|]; simpl; eauto. - - intros; eexists; intuition; eapply sem_istate_determ; eauto. - - intros; exploit sem_istate_exclude_abort; eauto. destruct 1. + - intros; eexists; intuition; eapply smatch_determ; eauto. + - intros; exploit smatch_exclude_sabort; eauto. destruct 1. Qed. (** * Symbolic execution of one internal step *) -Definition sreg_set (st:local_istate) (r:reg) (sv:sval) := - {| pre:=(fun ge sp rs m => sval_eval ge sp (st.(the_sreg) r) rs m <> None /\ (st.(pre) ge sp rs m)); - the_sreg:=fun y => if Pos.eq_dec r y then sv else st.(the_sreg) y; - the_smem:= st.(the_smem)|}. +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 smem_set (st:local_istate) (sm:smem) := - {| pre:=(fun ge sp rs m => smem_eval ge sp st.(the_smem) rs m <> None /\ (st.(pre) ge sp rs m)); - the_sreg:= st.(the_sreg); - the_smem:= sm |}. +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 (st: s_istate) (pc: node) (nxt: local_istate): option s_istate := - Some {| the_pc := pc; exits := st.(exits); curr:= nxt |}. +Definition sist_set_local (st: sistate) (pc: node) (nxt: sistate_local): option sistate := + Some {| si_pc := pc; si_exits := st.(si_exits); si_local:= nxt |}. (* FIXME - add notrap *) -Definition symb_istep (i: instruction) (st: s_istate): option s_istate := +Definition symb_istep (i: instruction) (st: sistate): option sistate := match i with | Inop pc' => - sist st pc' st.(curr) + sist_set_local st pc' st.(si_local) | Iop op args dst pc' => - let prev := st.(curr) in - let vargs := list_sval_inj (List.map prev.(the_sreg) args) in - let next := sreg_set prev dst (Sop op vargs prev.(the_smem)) in - sist st pc' next + let prev := st.(si_local) in + let vargs := list_sval_inj (List.map prev.(si_sreg) args) in + let next := slocal_set_sreg prev dst (Sop op vargs prev.(si_smem)) in + sist_set_local st pc' next | Iload _ chunk addr args dst pc' => - let prev := st.(curr) in - let vargs := list_sval_inj (List.map prev.(the_sreg) args) in - let next := sreg_set prev dst (Sload prev.(the_smem) chunk addr vargs) in - sist st pc' next + let prev := st.(si_local) in + let vargs := list_sval_inj (List.map prev.(si_sreg) args) in + let next := slocal_set_sreg prev dst (Sload prev.(si_smem) chunk addr vargs) in + sist_set_local st pc' next | Istore chunk addr args src pc' => - let prev := st.(curr) in - let vargs := list_sval_inj (List.map prev.(the_sreg) args) in - let next := smem_set prev (Sstore prev.(the_smem) chunk addr vargs (prev.(the_sreg) src)) in - sist st pc' next + 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.(curr) in - let vargs := list_sval_inj (List.map prev.(the_sreg) args) in - let ex := {| the_cond:=cond; cond_args:=vargs; exit_ist := prev; cond_ifso := ifso |} in - Some {| the_pc := ifnot; exits := ex::st.(exits); curr := prev |} + let prev := st.(si_local) in + let vargs := list_sval_inj (List.map prev.(si_sreg) args) in + let ex := {| si_cond:=cond; si_scondargs:=vargs; si_elocal := prev; si_ifso := ifso |} in + Some {| si_pc := ifnot; si_exits := ex::st.(si_exits); si_local := prev |} | _ => None (* TODO jumptable ? *) end. +(* TODO TODO - continue renaming *) + Lemma list_sval_eval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs: - (forall r : reg, sval_eval ge sp (sreg r) rs0 m0 = Some (rs # r)) -> + (forall r : reg, seval ge sp (sreg r) rs0 m0 = Some (rs # r)) -> list_sval_eval ge sp (list_sval_inj (map sreg l)) rs0 m0 = Some (rs ## l). Proof. intros H; induction l as [|r l]; simpl; auto. @@ -553,7 +546,7 @@ Fixpoint symb_isteps (path:nat) (f: function) (st: s_istate): option s_istate := end. Lemma symb_isteps_correct_false ge sp path f rs0 m0 st' is: - is.(continue)=false -> + is.(icontinue)=false -> forall st, sem_istate ge sp st rs0 m0 is -> symb_isteps path f st = Some st' -> sem_istate ge sp st' rs0 m0 is. @@ -599,7 +592,7 @@ Proof. Qed. Lemma symb_isteps_correct_true ge sp path (f:function) rs0 m0: forall st is, - is.(continue)=true -> + is.(icontinue)=true -> sem_istate ge sp st rs0 m0 is -> nth_default_succ (fn_code f) path st.(the_pc) <> None -> sem_option2_istate ge sp (symb_isteps path f st) rs0 m0 @@ -619,7 +612,7 @@ Proof. exploit symb_istep_correct; eauto. inversion_SOME st1; intros Hst1; erewrite Hst1; simpl. - inversion_SOME is1; intros His1;rewrite His1; simpl. - * destruct (continue is1) eqn:CONT1. + * destruct (icontinue is1) eqn:CONT1. (* continue is0 = true *) intros; eapply IHpath; eauto. destruct i; simpl in * |- *; unfold sist in * |- *; try_simplify_someHyps. @@ -677,7 +670,7 @@ Inductive sfval := Definition s_find_function (pge: RTLpath.genv) (ge: RTL.genv) (sp: val) (svos : sval + ident) (rs0: regset) (m0: mem): option fundef := match svos with - | inl sv => SOME v <- sval_eval ge sp sv rs0 m0 IN Genv.find_funct pge v + | inl sv => SOME v <- seval ge sp sv rs0 m0 IN Genv.find_funct pge v | inr symb => SOME b <- Genv.find_symbol pge symb IN Genv.find_funct_ptr pge b end. @@ -714,7 +707,7 @@ Inductive sfval_sem (pge: RTLpath.genv) (ge: RTL.genv) (sp:val) (st: s_istate) s | 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 => sval_eval ge sp sv rs0 m0 | None => Some Vundef end = Some v -> + match osv with Some sv => seval ge sp sv rs0 m0 | None => Some Vundef end = Some v -> sfval_sem pge ge sp st stack f rs0 m0 (Sreturn osv) rs m E0 (Returnstate stack v m') . @@ -723,11 +716,11 @@ Record s_state := { internal:> s_istate; final: sfval }. Inductive sem_state pge (ge: RTL.genv) (sp:val) (st: s_state) stack f (rs0: regset) (m0: mem): trace -> state -> Prop := | sem_early is: - is.(continue) = false -> + is.(icontinue) = false -> sem_istate ge sp st rs0 m0 is -> sem_state pge ge sp st stack f rs0 m0 E0 (State stack f sp is.(RTLpath.the_pc) is.(the_rs) is.(the_mem)) | sem_normal is t s: - is.(continue) = true -> + is.(icontinue) = true -> sem_istate ge sp st rs0 m0 is -> sfval_sem pge ge sp st stack f rs0 m0 st.(final) is.(the_rs) is.(the_mem) t s -> sem_state pge ge sp st stack f rs0 m0 t s @@ -871,7 +864,7 @@ Proof. exploit symb_istep_correct; eauto. simpl. erewrite Hst', ISTEP; simpl. clear LAST CONT STEPS PC SEM HNYE Hst Hi' Hst' ISTEP st sti i. - intro SEM; destruct (ist.(continue)) eqn: CONT. + intro SEM; destruct (ist.(icontinue)) eqn: CONT. { (* continue ist = true *) eapply sem_normal; simpl; eauto. unfold sem_istate in SEM. @@ -1026,8 +1019,8 @@ Variable ge ge': RTL.genv. Hypothesis symbols_preserved_RTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s. -Lemma sval_eval_preserved sp sv rs0 m0: - sval_eval ge sp sv rs0 m0 = sval_eval ge' sp sv rs0 m0. +Lemma seval_preserved sp sv rs0 m0: + seval ge sp sv rs0 m0 = seval ge' sp sv rs0 m0. Proof. Local Hint Resolve symbols_preserved_RTL: core. induction sv using sval_mut with (P0 := fun lsv => list_sval_eval ge sp lsv rs0 m0 = list_sval_eval ge' sp lsv rs0 m0) @@ -1039,7 +1032,7 @@ Proof. erewrite <- eval_addressing_preserved; eauto. destruct (eval_addressing _ sp _ _); auto. rewrite IHsv; auto. - + rewrite IHsv; clear IHsv. destruct (sval_eval _ _ _ _); auto. + + rewrite IHsv; clear IHsv. destruct (seval _ _ _ _); auto. rewrite IHsv0; auto. + rewrite IHsv0; clear IHsv0. destruct (list_sval_eval _ _ _ _); auto. erewrite <- eval_addressing_preserved; eauto. @@ -1052,7 +1045,7 @@ Lemma list_sval_eval_preserved sp lsv rs0 m0: list_sval_eval ge sp lsv rs0 m0 = list_sval_eval ge' sp lsv rs0 m0. Proof. induction lsv; simpl; auto. - rewrite sval_eval_preserved. destruct (sval_eval _ _ _ _); auto. + rewrite seval_preserved. destruct (seval _ _ _ _); auto. rewrite IHlsv; auto. Qed. @@ -1064,7 +1057,7 @@ Proof. erewrite <- eval_addressing_preserved; eauto. destruct (eval_addressing _ sp _ _); auto. rewrite IHsm; clear IHsm. destruct (smem_eval _ _ _ _); auto. - rewrite sval_eval_preserved; auto. + rewrite seval_preserved; auto. Qed. Lemma seval_condition_preserved sp cond lsv sm rs0 m0: @@ -1080,12 +1073,12 @@ End SymbValPreserved. Require Import RTLpathLivegen RTLpathLiveproofs. Definition istate_simulive alive (srce: PTree.t node) (is1 is2: istate): Prop := - is1.(continue) = is2.(continue) + is1.(icontinue) = is2.(icontinue) /\ eqlive_reg alive is1.(the_rs) is2.(the_rs) /\ is1.(the_mem) = is2.(the_mem). Definition istate_simu f (srce: PTree.t node) is1 is2: Prop := - if is1.(continue) then + 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 -- cgit