diff options
| -rwxr-xr-x | configure | 2 | ||||
| -rw-r--r-- | mppa_k1c/lib/RTLpathLivegen.v | 11 | ||||
| -rw-r--r-- | mppa_k1c/lib/RTLpathLiveproofs.v | 54 |
3 files changed, 47 insertions, 20 deletions
@@ -849,7 +849,7 @@ ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure EXECUTE=k1-cluster --syscall=libstd_scalls.so -- CFLAGS= -D __K1C_COS__ SIMU=k1-cluster -- -BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v RTLpath.v RTLpathLivegen.v RTLpathLiveproofs.v RTLpathSE_theory.v\\ +BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v RTLpath.v RTLpathLivegen.v RTLpathLiveproofs.v RTLpathSE_theory.v RTLpathScheduler.v\\ Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\ diff --git a/mppa_k1c/lib/RTLpathLivegen.v b/mppa_k1c/lib/RTLpathLivegen.v index 4ec854d3..1db90271 100644 --- a/mppa_k1c/lib/RTLpathLivegen.v +++ b/mppa_k1c/lib/RTLpathLivegen.v @@ -112,10 +112,11 @@ Definition reg_option_mem (or: option reg) (alive: Regset.t) := Definition reg_sum_mem (ros: reg + ident) (alive: Regset.t) := match ros with inl r => Regset.mem r alive | inr s => true end. -Fixpoint reg_list_add (rl: list reg) (alive: Regset.t) {struct rl} : Regset.t := - match rl with - | nil => alive - | r1 :: rs => reg_list_add rs (Regset.add r1 alive) +(* NB: definition following [regmap_setres] in [RTL.step] semantics *) +Definition reg_builtin_res (res: builtin_res reg) (alive: Regset.t): Regset.t := + match res with + | BR r => Regset.add r alive + | _ => alive end. Fixpoint exit_list_checker (pm: path_map) (alive: Regset.t) (l: list node): bool := @@ -160,7 +161,7 @@ Definition inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): optio Some tt | Ibuiltin ef args res pc' => ASSERT list_mem (params_of_builtin_args args) alive IN - exit_checker pm (reg_list_add (params_of_builtin_res res) alive) pc' tt + exit_checker pm (reg_builtin_res res alive) pc' tt | Ijumptable arg tbl => ASSERT Regset.mem arg alive IN ASSERT exit_list_checker pm alive tbl IN diff --git a/mppa_k1c/lib/RTLpathLiveproofs.v b/mppa_k1c/lib/RTLpathLiveproofs.v index 2d2456ae..1cdd6168 100644 --- a/mppa_k1c/lib/RTLpathLiveproofs.v +++ b/mppa_k1c/lib/RTLpathLiveproofs.v @@ -45,16 +45,6 @@ Proof. unfold eqlive_reg; intros H0 H1 r H. rewrite H0; eauto. Qed. -(* -Lemma eqlive_reg_notin alive rs r v: ~(alive r) -> eqlive_reg alive rs (rs # r <- v). -Proof. - unfold eqlive_reg; intros NOTALIVE r0 ALIVE. - destruct (Pos.eq_dec r r0) as [H|H]. - - subst; tauto. - - rewrite Regmap.gso; auto. -Qed. -*) - Lemma eqlive_reg_update (alive: Regset.elt -> Prop) rs1 rs2 r v: eqlive_reg (fun r1 => r1 <> r /\ alive r1) rs1 rs2 -> eqlive_reg alive (rs1 # r <- v) (rs2 # r <- v). Proof. unfold eqlive_reg; intros EQLIVE r0 ALIVE. @@ -358,18 +348,54 @@ Proof. rewrite regset_add_spec. intuition subst. Qed. +Local Hint Resolve in_or_app: local. Lemma eqlive_eval_builtin_args alive rs1 rs2 sp m args vargs: eqlive_reg alive rs1 rs2 -> - (forall r, List.In r (params_of_builtin_args args) -> alive r) -> Events.eval_builtin_args ge (fun r => rs1 # r) sp m args vargs -> + (forall r, List.In r (params_of_builtin_args args) -> alive r) -> Events.eval_builtin_args ge (fun r => rs2 # r) sp m args vargs. -Admitted. +Proof. + unfold Events.eval_builtin_args. + intros EQLIVE; induction 1 as [|a1 al b1 bl EVAL1 EVALL]; simpl. + { econstructor; eauto. } + intro X. + assert (X1: eqlive_reg (fun r => In r (params_of_builtin_arg a1)) rs1 rs2). + { eapply eqlive_reg_monotonic; eauto with local. } + lapply IHEVALL; eauto with local. + clear X IHEVALL; intro X. econstructor; eauto. + generalize X1; clear EVALL X1 X. + induction EVAL1; simpl; try (econstructor; eauto; fail). + - intros X1; erewrite X1; [ econstructor; eauto | eauto ]. + - intros; econstructor. + + eapply IHEVAL1_1; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. + + eapply IHEVAL1_2; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. + - intros; econstructor. + + eapply IHEVAL1_1; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. + + eapply IHEVAL1_2; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. +Qed. Lemma exit_checker_eqlive_builtin_res (pm: path_map) (alive: Regset.t) (pc: node) rs1 rs2 (res:builtin_res reg): - exit_checker pm (reg_list_add (params_of_builtin_res res) alive) pc tt = Some tt -> + exit_checker pm (reg_builtin_res res alive) pc tt = Some tt -> eqlive_reg (ext alive) rs1 rs2 -> exists path, pm!pc = Some path /\ (forall vres, eqlive_reg (ext path.(input_regs)) (regmap_setres res vres rs1) (regmap_setres res vres rs2)). -Admitted. +Proof. + destruct res; simpl. + - intros; exploit exit_checker_eqlive_ext1; eauto. + - intros; exploit exit_checker_eqlive; eauto. + intros (path & PATH & EQLIVE). + eexists; intuition eauto. + - intros; exploit exit_checker_eqlive; eauto. + intros (path & PATH & EQLIVE). + eexists; intuition eauto. +Qed. Lemma exit_list_checker_eqlive (pm: path_map) (alive: Regset.t) (tbl: list node) rs1 rs2 pc: forall n, exit_list_checker pm alive tbl = true -> |