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, 59 insertions, 56 deletions

diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index a9cbad5..7e3217e 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -335,8 +335,4 @@ Nondetfunction addr_strength_reduction
       (addr, args)
   end.
 
-Definition builtin_strength_reduction
-               (ef: external_function) (args: list reg) (vl: list approx) :=
-  (ef, args).
-
 End STRENGTH_REDUCTION.
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index e7e6a41..c7de86d 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -450,19 +450,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.
-  (* force MATCH to be used *)
-  assert (val_match_approx (approx_reg app 1%positive) rs#(1%positive))
-    by (apply MATCH).
-  unfold builtin_strength_reduction; intros; simpl; auto.
-Qed.
-
 End STRENGTH_REDUCTION.
 
 End ANALYSIS.
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 186e327..278b6b1 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -226,9 +226,9 @@ let call_helper oc fn dst arg1 arg2 =
 
 (* 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 "sp" oc txt args
+  PrintAnnot.print_annot_stmt preg "sp" oc txt targs args
 
 let print_annot_val oc txt args res =
   fprintf oc "%s annotation: " comment;
@@ -306,50 +306,66 @@ let print_builtin_memcpy oc sz al args =
 
 (* Handling of volatile reads and writes *)
 
+let print_builtin_vload_common oc chunk args res =
+  match chunk, args, res with
+  | Mint8unsigned, [IR addr], IR res ->
+      fprintf oc "	ldrb	%a, [%a, #0]\n" ireg res ireg addr; 1
+  | Mint8signed, [IR addr], IR res ->
+      fprintf oc "	ldrsb	%a, [%a, #0]\n" ireg res ireg addr; 1
+  | Mint16unsigned, [IR addr], IR res ->
+      fprintf oc "	ldrh	%a, [%a, #0]\n" ireg res ireg addr; 1
+  | Mint16signed, [IR addr], IR res ->
+      fprintf oc "	ldrsh	%a, [%a, #0]\n" ireg res ireg addr; 1
+  | Mint32, [IR addr], IR res ->
+      fprintf oc "	ldr	%a, [%a, #0]\n" ireg res ireg addr; 1
+  | Mfloat32, [IR addr], FR res ->
+      fprintf oc "	flds	%a, [%a, #0]\n" freg_single res ireg addr;
+      fprintf oc "	fcvtds	%a, %a\n" freg res freg_single res; 2
+  | (Mfloat64 | Mfloat64al32), [IR addr], FR res ->
+      fprintf oc "	fldd	%a, [%a, #0]\n" freg res ireg addr; 1
+  | _ ->
+      assert false
+
 let print_builtin_vload oc chunk args res =
   fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
-  let n = 
-    begin match chunk, args, res with
-    | Mint8unsigned, [IR addr], IR res ->
-        fprintf oc "	ldrb	%a, [%a, #0]\n" ireg res ireg addr; 1
-    | Mint8signed, [IR addr], IR res ->
-        fprintf oc "	ldrsb	%a, [%a, #0]\n" ireg res ireg addr; 1
-    | Mint16unsigned, [IR addr], IR res ->
-        fprintf oc "	ldrh	%a, [%a, #0]\n" ireg res ireg addr; 1
-    | Mint16signed, [IR addr], IR res ->
-        fprintf oc "	ldrsh	%a, [%a, #0]\n" ireg res ireg addr; 1
-    | Mint32, [IR addr], IR res ->
-        fprintf oc "	ldr	%a, [%a, #0]\n" ireg res ireg addr; 1
-    | Mfloat32, [IR addr], FR res ->
-        fprintf oc "	flds	%a, [%a, #0]\n" freg_single res ireg addr;
-        fprintf oc "	fcvtds	%a, %a\n" freg res freg_single res; 2
-    | (Mfloat64 | Mfloat64al32), [IR addr], FR res ->
-        fprintf oc "	fldd	%a, [%a, #0]\n" freg res ireg addr; 1
-    | _ ->
-        assert false
-    end in
+  let n = print_builtin_vload_common oc chunk args res in
   fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n
 
+let print_builtin_vload_global oc chunk id ofs args res =
+  fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
+  let lbl = label_symbol id ofs in
+  fprintf oc "	ldr	%a, .L%d @ %a\n" ireg IR14 lbl print_symb_ofs (id, ofs);
+  let n = print_builtin_vload_common oc chunk [IR IR14] res in
+  fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n + 1
+
+let print_builtin_vstore_common oc chunk args =
+  match chunk, args with
+  | (Mint8signed | Mint8unsigned), [IR  addr; IR src] ->
+      fprintf oc "	strb	%a, [%a, #0]\n" ireg src ireg addr; 1
+  | (Mint16signed | Mint16unsigned), [IR  addr; IR src] ->
+      fprintf oc "	strh	%a, [%a, #0]\n" ireg src ireg addr; 1
+  | Mint32, [IR  addr; IR src] ->
+      fprintf oc "	str	%a, [%a, #0]\n" ireg src ireg addr; 1
+  | Mfloat32, [IR  addr; FR src] ->
+      fprintf oc "	fcvtsd	%a, %a\n" freg_single FR6 freg src;
+      fprintf oc "	fsts	%a, [%a, #0]\n" freg_single FR6 ireg addr; 2
+  | (Mfloat64 | Mfloat64al32), [IR  addr; FR src] ->
+      fprintf oc "	fstd	%a, [%a, #0]\n" freg src ireg addr; 1
+  | _ ->
+      assert false
+
 let print_builtin_vstore oc chunk args =
   fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
-  let n =
-    begin match chunk, args with
-    | (Mint8signed | Mint8unsigned), [IR addr; IR src] ->
-        fprintf oc "	strb	%a, [%a, #0]\n" ireg src ireg addr; 1
-    | (Mint16signed | Mint16unsigned), [IR addr; IR src] ->
-        fprintf oc "	strh	%a, [%a, #0]\n" ireg src ireg addr; 1
-    | Mint32, [IR addr; IR src] ->
-        fprintf oc "	str	%a, [%a, #0]\n" ireg src ireg addr; 1
-    | Mfloat32, [IR addr; FR src] ->
-        fprintf oc "	fcvtsd	%a, %a\n" freg_single FR6 freg src;
-        fprintf oc "	fsts	%a, [%a, #0]\n" freg_single FR6 ireg addr; 2
-    | (Mfloat64 | Mfloat64al32), [IR addr; FR src] ->
-        fprintf oc "	fstd	%a, [%a, #0]\n" freg src ireg addr; 1
-    | _ ->
-        assert false
-    end in
+  let n = print_builtin_vstore_common oc chunk args in
   fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n
 
+let print_builtin_vstore_global oc chunk id ofs args =
+  fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
+  let lbl = label_symbol id ofs in
+  fprintf oc "	ldr	%a, .L%d @ %a\n" ireg IR14 lbl print_symb_ofs (id, ofs);
+  let n = print_builtin_vstore_common oc chunk (IR IR14 :: args) in
+  fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n + 1
+
 (* Magic sequence for byte-swapping *)
 
 let print_bswap oc src tmp dst =
@@ -612,6 +628,10 @@ let print_instruction oc = function
           print_builtin_vload oc chunk args res
       | EF_vstore chunk ->
           print_builtin_vstore oc chunk args
+      | EF_vload_global(chunk, id, ofs) ->
+          print_builtin_vload_global oc chunk id ofs args res
+      | EF_vstore_global(chunk, id, ofs) ->
+          print_builtin_vstore_global oc chunk id ofs args
       | EF_memcpy(sz, al) ->
           print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz))
                                   (Int32.to_int (camlint_of_coqint al)) args
@@ -628,7 +648,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; 0
+          print_annot_stmt oc (extern_atom txt) targs args; 0
       | _ ->
           assert false
       end