diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-13 18:47:13 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-13 18:47:13 +0100 |
commit | 2e47c928161eebb252fea056495a70d22884efc9 (patch) | |
tree | 86dc9a81907bd8919987928250beb6186026e080 /backend | |
parent | c8553d8cbad6ea9c0eeba732aa199eefd6d1339f (diff) | |
download | compcert-kvx-2e47c928161eebb252fea056495a70d22884efc9.tar.gz compcert-kvx-2e47c928161eebb252fea056495a70d22884efc9.zip |
some automation
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CSE3analysisproof.v | 31 | ||||
-rw-r--r-- | backend/CSE3proof.v | 62 |
2 files changed, 64 insertions, 29 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 155fedef..cd27a506 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -189,6 +189,22 @@ Proof. eassumption. Qed. +Hint Resolve get_kills_has_lhs : cse3. + +Lemma context_from_hints_get_kills_has_lhs : + forall hints lhs sop args j, + PTree.get j (hint_eq_catalog hints) = Some {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |} -> + PSet.contains (eq_kill_reg (context_from_hints hints) lhs) j = true. +Proof. + intros; simpl. + eapply get_kills_has_lhs. + eassumption. +Qed. + +Hint Resolve context_from_hints_get_kills_has_lhs : cse3. + Lemma get_kills_has_arg : forall eqs lhs sop arg args j, PTree.get j eqs = Some {| eq_lhs := lhs; @@ -212,6 +228,21 @@ Qed. Hint Resolve get_kills_has_arg : cse3. +Lemma context_from_hints_get_kills_has_arg : + forall hints lhs sop arg args j, + PTree.get j (hint_eq_catalog hints) = Some {| eq_lhs := lhs; + eq_op := sop; + eq_args:= args |} -> + In arg args -> + PSet.contains (eq_kill_reg (context_from_hints hints) arg) j = true. +Proof. + intros. + simpl. + eapply get_kills_has_arg; eassumption. +Qed. + +Hint Resolve context_from_hints_get_kills_has_arg : cse3. + Definition eq_involves (eq : equation) (i : reg) := i = (eq_lhs eq) \/ In i (eq_args eq). diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 8d987e94..e18456d2 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -353,6 +353,37 @@ Qed. Hint Resolve rel_ge : cse3. +Lemma sem_rhs_sop : + forall sp op rs args m v, + eval_operation ge sp op rs ## args m = Some v -> + sem_rhs (genv:=ge) (sp:=sp) (SOp op) args rs m v. +Proof. + intros. simpl. + rewrite H. + reflexivity. +Qed. + +Hint Resolve sem_rhs_sop : cse3. + +Ltac IND_STEP := + match goal with + REW: (fn_code ?fn) ! ?mpc = Some ?minstr, + IND: is_inductive_allstep ?fn ?tenv ?invariants + |- + sem_rel_b ?sp ?ctx (?inv # ?mpc') ?rs ?m => + unfold is_inductive_allstep, is_inductive_step, apply_instr' in IND; + specialize IND with (pc:=mpc) (pc':=mpc') (instr:=minstr); + simpl in IND; + rewrite REW in IND; + simpl in IND; + destruct (inv # mpc') as [zinv' | ]; + destruct (inv # mpc) as [zinv | ]; + simpl in *; + intuition; + eapply rel_ge; eauto with cse3; + idtac mpc mpc' fn minstr inv + end. + Lemma step_simulation: forall S1 t S2, RTL.step ge S1 t S2 -> forall S1', match_states S1 S1' -> @@ -364,19 +395,7 @@ Proof. + apply exec_Inop; auto. TR_AT. reflexivity. + econstructor; eauto. - - unfold is_inductive_allstep, is_inductive_step, apply_instr' in IND. - specialize IND with (pc:=pc) (pc':=pc') (instr := (Inop pc')). - simpl in IND. - rewrite H in IND. - simpl in IND. - intuition. - unfold sem_rel_b in *. - destruct (invariants # pc') as [inv' | ]; - destruct (invariants # pc) as [inv | ]; - simpl in *; - try contradiction. - eapply rel_ge; eassumption. + IND_STEP. - (* Iop *) exists (State ts tf sp pc' (rs # res <- v) m). split. @@ -384,23 +403,8 @@ Proof. + econstructor; eauto. * eapply wt_exec_Iop with (f:=f); try eassumption. eauto with wt. - * unfold is_inductive_allstep, is_inductive_step, apply_instr' in IND. - specialize IND with (pc:=pc) (pc':=pc') (instr := (Iop op args res pc')). - simpl in IND. - rewrite H in IND. - simpl in IND. - intuition. - unfold sem_rel_b in *. - destruct (invariants # pc') as [inv' | ]; - destruct (invariants # pc) as [inv | ]; - simpl in *; - try contradiction. - eapply rel_ge. - eassumption. + * IND_STEP. apply oper_sound; eauto with cse3. - simpl. - rewrite H0. - trivial. - (* Iload *) exists (State ts tf sp pc' (rs # dst <- v) m). split. |