Updated ARM port.

CSE.v: removed commented-out stuff.


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

4 files changed, 20 insertions, 23 deletions

diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml
index ea3c7df..3be32e4 100644
--- a/arm/CBuiltins.ml
+++ b/arm/CBuiltins.ml
@@ -29,13 +29,13 @@ let builtins = {
     "__builtin_fsqrt",
       (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
     (* Memory accesses *)
-    "__builtin_read_int16_reversed",
+    "__builtin_read16_reversed",
       (TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false);
-    "__builtin_read_int32_reversed",
+    "__builtin_read32_reversed",
       (TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false);
-    "__builtin_write_int16_reversed",
+    "__builtin_write16_reversed",
       (TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false);
-    "__builtin_write_int32_reversed",
+    "__builtin_write32_reversed",
       (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false);
   ]
 }
diff --git a/arm/CombineOp.v b/arm/CombineOp.v
index be9824b..fd347c1 100644
--- a/arm/CombineOp.v
+++ b/arm/CombineOp.v
@@ -74,13 +74,16 @@ Function combine_cond (cond: condition) (args: list valnum) : option(condition *
   | _, _ => None
   end.
 
+(* Problem: on ARM, not all load/store instructions accept the Aindexed2
+   and Aindexed2shift addressing modes.  For the time being,
+   avoid producing them. *)
+
 Function combine_addr (addr: addressing) (args: list valnum) : option(addressing * list valnum) :=
   match addr, args with
   | Aindexed n, x::nil =>
       match get x with
-      | Some(Op (Oaddimm m) ys) => Some(Aindexed (Int.add m n), ys)
-      | Some(Op Oadd ys) => if Int.eq_dec n Int.zero then Some(Aindexed2, ys) else None
-      | Some(Op (Oaddshift s) ys) => if Int.eq_dec n Int.zero then Some(Aindexed2shift s, ys) else None
+      | Some(Op (Oaddimm m) ys) =>
+          Some(Aindexed (Int.add m n), ys)
       | _ => None
       end
   | _, _ => None
diff --git a/arm/CombineOpproof.v b/arm/CombineOpproof.v
index e7080f4..c95b19c 100644
--- a/arm/CombineOpproof.v
+++ b/arm/CombineOpproof.v
@@ -116,12 +116,6 @@ Proof.
   (* indexed - addimm *)
   exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. FuncInv.
   rewrite <- H0. rewrite Val.add_assoc. auto. 
-  (* indexed 0 - add *)
-  exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. FuncInv.
-  rewrite <- H0. destruct v; destruct v0; simpl; auto; rewrite Int.add_zero; auto.
-  (* indexed 0 - addshift *)
-  exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. FuncInv.
-  rewrite <- H0. destruct v; destruct (eval_shift s v0); simpl; auto; rewrite Int.add_zero; auto.
 Qed.
 
 Theorem combine_op_sound:
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 86fdf0e..36becdc 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -400,20 +400,20 @@ let print_builtin_inline oc name args res =
   | "__builtin_fsqrt", [FR a1], FR res ->
       fprintf oc "	fsqrtd	%a, %a\n" freg res freg a1; 1
   (* Memory accesses *)
-  | "__builtin_read_int16_reversed", [IR a1], IR res ->
+  | "__builtin_read16_reversed", [IR a1], IR res ->
       fprintf oc "	ldrh	%a, [%a, #0]\n" ireg res ireg a1;
       fprintf oc "	mov	%a, %a, lsl #8\n" ireg IR14 ireg res;
       fprintf oc "	and	%a, %a, #0xFF00\n" ireg IR14 ireg IR14;
       fprintf oc "	orr	%a, %a, %a, lsr #8\n" ireg res ireg IR14 ireg res; 4
-  | "__builtin_read_int32_reversed", [IR a1], IR res ->
+  | "__builtin_read32_reversed", [IR a1], IR res ->
       fprintf oc "	ldr	%a, [%a, #0]\n" ireg res ireg a1;
       print_bswap oc res IR14 res; 5
-  | "__builtin_write_int16_reversed", [IR a1; IR a2], _ ->
+  | "__builtin_write16_reversed", [IR a1; IR a2], _ ->
       fprintf oc "	mov	%a, %a, lsr #8\n" ireg IR14 ireg a2;
       fprintf oc "	and	%a, %a, #0xFF\n" ireg IR14 ireg IR14;
       fprintf oc "	orr	%a, %a, %a, lsl #8\n" ireg IR14 ireg IR14 ireg a2;
       fprintf oc "	strh	%a, [%a, #0]\n" ireg IR14 ireg a1; 4
-  | "__builtin_write_int32_reversed", [IR a1; IR a2], _ ->
+  | "__builtin_write32_reversed", [IR a1; IR a2], _ ->
       let tmp = if a1 = IR10 then IR12 else IR10 in
       print_bswap oc a2 IR14 tmp;
       fprintf oc "	str	%a, [%a, #0]\n" ireg tmp ireg a1; 5
@@ -671,6 +671,12 @@ let rec print_instructions oc instrs =
       end;
       print_instructions oc il
 
+(* Base-2 log of a Caml integer *)
+
+let rec log2 n =
+  assert (n > 0);
+  if n = 1 then 0 else 1 + log2 (n lsr 1)
+
 let print_function oc name fn =
   Hashtbl.clear current_function_labels;
   reset_constants();
@@ -728,12 +734,6 @@ let print_init_data oc name id =
   else
     List.iter (print_init oc) id
 
-(* Base-2 log of a Caml integer *)
-
-let rec log2 n =
-  assert (n > 0);
-  if n = 1 then 0 else 1 + log2 (n lsr 1)
-
 let print_var oc (name, v) =
   match v.gvar_init with
   | [] -> ()