Updated ARM and PowerPC ports with new handling of __builtin_annot.

ARM: add support for builtin_volatile_{read,write}_global, after all.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2127 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 3 insertions, 32 deletions

diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 973be925..9131a466 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -293,15 +293,4 @@ Nondetfunction addr_strength_reduction
       (addr, 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/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 7d557c6d..84e1e5bb 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -430,24 +430,6 @@ Proof.
   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/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 9c0f471d..c9203ec6 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -231,9 +231,9 @@ let rolm_mask n =
 
 (* Handling of annotations *)
 
-let print_annot_stmt oc txt args =
+let print_annot_stmt oc txt targs args =
   fprintf oc "%s annotation: " comment;
-  PrintAnnot.print_annot_stmt preg "R1" oc txt args
+  PrintAnnot.print_annot_stmt preg "R1" oc txt targs args
 
 let print_annot_val oc txt args res =
   fprintf oc "%s annotation: " comment;
@@ -737,7 +737,7 @@ let print_instruction oc tbl pc fallthrough = 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