From 202bc495442a1a8fa184b73ac0063bdbbbcdf846 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 24 Feb 2013 09:01:28 +0000
Subject: Constant propagation within __builtin_annot.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 ia32/ConstpropOp.vp     | 11 -----------
 ia32/ConstpropOpproof.v | 18 ------------------
 ia32/PrintAsm.ml        | 30 +++++-------------------------
 3 files changed, 5 insertions(+), 54 deletions(-)

(limited to 'ia32')

diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index 8a612f0..e6ba98a 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -307,15 +307,4 @@ Nondetfunction op_strength_reduction
   | _, _, _ => (op, args)
   end.
 
-Nondetfunction builtin_strength_reduction
-               (ef: external_function) (args: list reg) (vl: list approx) :=
-  match ef, args, vl with
-  | EF_vload chunk, r1 :: nil, G symb n1 :: nil =>
-      (EF_vload_global chunk symb n1, nil)
-  | EF_vstore chunk, r1 :: r2 :: nil, G symb n1 :: v2 :: nil =>
-      (EF_vstore_global chunk symb n1, r2 :: nil)
-  | _, _, _ =>
-      (ef, args)
-  end.
-
 End STRENGTH_REDUCTION.
diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index 9003743..d792d8a 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -421,24 +421,6 @@ Proof.
   exists v; auto.
 Qed.
 
-Lemma builtin_strength_reduction_correct:
-  forall ef args vl m t vres m',
-  vl = approx_regs app args ->
-  external_call ef ge rs##args m t vres m' ->
-  let (ef', args') := builtin_strength_reduction ef args vl in
-  external_call ef' ge rs##args' m t vres m'.
-Proof.
-  intros until m'. unfold builtin_strength_reduction.
-  destruct (builtin_strength_reduction_match ef args vl); simpl; intros; InvApproxRegs; SimplVMA.
-  unfold symbol_address in H. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H in H0.
-  rewrite volatile_load_global_charact. exists b; auto. 
-  inv H0.
-  unfold symbol_address in H1. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H1 in H0.
-  rewrite volatile_store_global_charact. exists b; auto. 
-  inv H0.
-  auto.
-Qed.
-
 End STRENGTH_REDUCTION.
 
 End ANALYSIS.
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 0074405..4f62640 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -231,33 +231,13 @@ let need_masks = ref false
 
 (* Handling of annotations *)
 
-let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
-
-let print_annot_text print_arg oc txt args =
-  fprintf oc "%s annotation: " comment;
-  let print_fragment = function
-  | Str.Text s ->
-      output_string oc s
-  | Str.Delim "%%" ->
-      output_char oc '%'
-  | Str.Delim s ->
-      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
-      try
-        print_arg oc (List.nth args (n-1))
-      with Failure _ ->
-        fprintf oc "<bad parameter %s>" s in
-  List.iter print_fragment (Str.full_split re_annot_param txt);
-  fprintf oc "\n"
-
 let print_annot_stmt oc txt args =
-  let print_annot_param oc = function
-  | APreg r -> preg oc r
-  | APstack(chunk, ofs) ->
-      fprintf oc "mem(ESP + %a, %a)" coqint ofs coqint (size_chunk chunk) in
-  print_annot_text print_annot_param oc txt args
+  fprintf oc "%s annotation: " comment;
+  PrintAnnot.print_annot_stmt preg "ESP" oc txt args
 
 let print_annot_val oc txt args res =
-  print_annot_text preg oc txt args;
+  fprintf oc "%s annotation: " comment;
+  PrintAnnot.print_annot_val preg oc txt args;
   match args, res with
   | IR src :: _, IR dst ->
       if dst <> src then fprintf oc "	movl	%a, %a\n" ireg src ireg dst
@@ -723,7 +703,7 @@ let print_instruction oc = function
   | Pannot(ef, args) ->
       begin match ef with
       | EF_annot(txt, targs) ->
-          print_annot_stmt oc (extern_atom txt) args
+          print_annot_stmt oc (extern_atom txt) targs args
       | _ ->
           assert false
       end
-- 
cgit v1.2.3