From 5955f24c579250be7701a8f351be4b627d670b81 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 14 Jun 2011 09:58:40 +0000
Subject: Add preference for annot_val builtin

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1674 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Coloring.v      |  9 ++++++++-
 backend/Coloringproof.v | 16 +++++++++++++---
 2 files changed, 21 insertions(+), 4 deletions(-)

(limited to 'backend')

diff --git a/backend/Coloring.v b/backend/Coloring.v
index 6d34e2c..a23bf55 100644
--- a/backend/Coloring.v
+++ b/backend/Coloring.v
@@ -139,6 +139,13 @@ Fixpoint add_prefs_call
   | _, _ => g
   end.
 
+Definition add_prefs_builtin (ef: external_function)
+                            (args: list reg) (res: reg) (g: graph) : graph :=
+  match ef, args with
+  | EF_annot_val txt targ, arg1 :: _ => add_pref arg1 res g
+  | _, _ => g
+  end.
+
 Definition add_interf_entry
     (params: list reg) (live: Regset.t) (g: graph): graph :=
   List.fold_left (fun g r => add_interf_op r live g) params g.
@@ -184,7 +191,7 @@ Definition add_edges_instr
       add_prefs_call args largs
         (add_interf_call ros largs g)
   | Ibuiltin ef args res s =>
-      add_interf_op res live g
+      add_prefs_builtin ef args res (add_interf_op res live g)
   | Ireturn (Some r) =>
       add_pref_mreg r (loc_result sig) g
   | _ => g
diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v
index ca0637a..8ebc87e 100644
--- a/backend/Coloringproof.v
+++ b/backend/Coloringproof.v
@@ -263,7 +263,6 @@ Proof.
   apply add_interfs_indirect_call_correct. auto.
 Qed.
 
-
 Lemma add_prefs_call_incl:
   forall args locs g,
   graph_incl g (add_prefs_call args locs g).
@@ -276,6 +275,16 @@ Proof.
   auto.
 Qed.
 
+Lemma add_prefs_builtin_incl:
+  forall ef args res g,
+  graph_incl g (add_prefs_builtin ef args res g).
+Proof.
+  intros. unfold add_prefs_builtin. 
+  destruct ef; try apply graph_incl_refl.
+  destruct args; try apply graph_incl_refl.
+  apply add_pref_incl. 
+Qed.
+
 Lemma add_interf_entry_incl:
   forall params live g,
   graph_incl g (add_interf_entry params live g).
@@ -384,7 +393,7 @@ Proof.
   apply add_interf_destroyed_incl.
   eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
   apply add_interfs_call_incl.
-  apply add_interf_op_incl.
+  eapply graph_incl_trans. apply add_interf_op_incl. apply add_prefs_builtin_incl.
   destruct o.
   apply add_pref_mreg_incl.
   apply graph_incl_refl.
@@ -508,7 +517,8 @@ Proof.
   apply add_interfs_call_correct. auto.
 
   (* Ibuiltin *)
-  intros. apply add_interf_op_correct; auto. 
+  intros. eapply interfere_incl. apply add_prefs_builtin_incl. 
+  apply add_interf_op_correct; auto. 
 Qed.
 
 Lemma add_edges_instrs_correct:
-- 
cgit v1.2.3