From 353b3cee4d08b5820bf62b7228afb67be69f10e6 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 4 Mar 2013 15:28:28 +0000
Subject: 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
---
 backend/Asmgenproof0.v | 27 ++++++++++++++++-----------
 1 file changed, 16 insertions(+), 11 deletions(-)

(limited to 'backend/Asmgenproof0.v')

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.
 
-- 
cgit