From 9e76f90bc5255d6ec933d705bf99baf3ca80d5d5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 10 Jul 2012 09:00:24 +0000 Subject: 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 --- arm/CBuiltins.ml | 8 ++++---- arm/CombineOp.v | 9 ++++++--- arm/CombineOpproof.v | 6 ------ arm/PrintAsm.ml | 20 ++++++++++---------- backend/CSE.v | 6 ------ 5 files changed, 20 insertions(+), 29 deletions(-) diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml index ea3c7df9..3be32e48 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 be9824bc..fd347c1b 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 e7080f44..c95b19ca 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 86fdf0ed..36becdc6 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 | [] -> () diff --git a/backend/CSE.v b/backend/CSE.v index e9613c92..85f46e2b 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -337,12 +337,6 @@ Definition reduce (op: A) (rl: list reg) (vl: list valnum) : A * list reg := End REDUCE. -(* -Parameter combine_cond: (valnum -> option rhs) -> condition -> list valnum -> option (condition * list valnum). -Parameter combine_addr: (valnum -> option rhs) -> addressing -> list valnum -> option (addressing * list valnum). -Parameter combine_op: (valnum -> option rhs) -> operation -> list valnum -> option (operation * list valnum). -*) - (** * The static analysis *) (** We now define a notion of satisfiability of a numbering. This semantic -- cgit