diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-04 15:28:28 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-04 15:28:28 +0000 |
| commit | 353b3cee4d08b5820bf62b7228afb67be69f10e6 (patch) | |
| tree | 84cd627b917b6a29a69ec440ef1a2342b6226390 /backend/Asmgenproof0.v | |
| parent | 6acc8ded7cd7e6605fcf27bdbd209d94571f45f4 (diff) | |
| download | compcert-kvx-353b3cee4d08b5820bf62b7228afb67be69f10e6.tar.gz compcert-kvx-353b3cee4d08b5820bf62b7228afb67be69f10e6.zip | |
Finished backtracking (cf previous commit) for ARM and PowerPC.
ARM: slightly shorter code generated for indirect memory accesses.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2137 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Asmgenproof0.v')
| -rw-r--r-- | backend/Asmgenproof0.v | 27 |
1 files changed, 16 insertions, 11 deletions
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 324e1f79..e1a3abcc 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -607,7 +607,8 @@ Qed. - the "code is tail of" property - correct translation of labels. *) -Definition tail_nolabel (k c: code) : Prop := is_tail k c /\ forall lbl, find_label lbl c = find_label lbl k. +Definition tail_nolabel (k c: code) : Prop := + is_tail k c /\ forall lbl, find_label lbl c = find_label lbl k. Lemma tail_nolabel_refl: forall c, tail_nolabel c c. @@ -616,17 +617,21 @@ Proof. Qed. Lemma tail_nolabel_trans: - forall c1 c2 c3, tail_nolabel c1 c2 -> tail_nolabel c2 c3 -> tail_nolabel c1 c3. + forall c1 c2 c3, tail_nolabel c2 c3 -> tail_nolabel c1 c2 -> tail_nolabel c1 c3. Proof. intros. destruct H; destruct H0; split. eapply is_tail_trans; eauto. - intros. rewrite H2; auto. + intros. rewrite H1; auto. Qed. +Definition nolabel (i: instruction) := + match i with Plabel _ => False | _ => True end. + +Hint Extern 1 (nolabel _) => exact I : labels. + Lemma tail_nolabel_cons: forall i c k, - match i with Plabel _ => False | _ => True end -> - tail_nolabel k c -> tail_nolabel k (i :: c). + nolabel i -> tail_nolabel k c -> tail_nolabel k (i :: c). Proof. intros. destruct H0. split. constructor; auto. @@ -635,15 +640,15 @@ Qed. Hint Resolve tail_nolabel_refl: labels. -Ltac TailNoLabels := +Ltac TailNoLabel := eauto with labels; match goal with - | [ |- tail_nolabel _ (_ :: _) ] => apply tail_nolabel_cons; [exact I | TailNoLabels] + | [ |- tail_nolabel _ (_ :: _) ] => apply tail_nolabel_cons; [auto; exact I | TailNoLabel] | [ H: Error _ = OK _ |- _ ] => discriminate - | [ H: OK _ = OK _ |- _ ] => inv H; TailNoLabels - | [ H: bind _ _ = OK _ |- _ ] => monadInv H; TailNoLabels - | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; TailNoLabels - | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; TailNoLabels + | [ H: OK _ = OK _ |- _ ] => inv H; TailNoLabel + | [ H: bind _ _ = OK _ |- _ ] => monadInv H; TailNoLabel + | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; TailNoLabel + | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; TailNoLabel | _ => idtac end. |