Merge of branch "unsigned-offsets":

- In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int.
  (Fixes issue with wrong comparison of pointers across 0x8000_0000)
- Revised Stacking pass to not use negative SP offsets.
- Add pointer validity checks to Cminor ... Mach
  to support the use of memory injections in Stacking.
- Cleaned up Stacklayout modules.
- IA32: improved code generation for Mgetparam.
- ARM: improved code generation for op-immediate instructions.


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

1 files changed, 59 insertions, 43 deletions

diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index b3412fb..a1f8d96 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -36,7 +36,7 @@ Require Import Asm.
 
 Fixpoint is_immed_arith_aux (n: nat) (x msk: int) {struct n}: bool :=
   match n with
-  | O => false
+  | Datatypes.O => false
   | Datatypes.S n' =>
       Int.eq (Int.and x (Int.not msk)) Int.zero ||
       is_immed_arith_aux n' x (Int.ror msk (Int.repr 2))
@@ -55,46 +55,65 @@ Definition is_immed_mem_float (x: int) : bool :=
   Int.eq (Int.and x (Int.repr 3)) Int.zero
   && Int.lt x (Int.repr 1024) && Int.lt (Int.repr (-1024)) x.
   
+(** Decomposition of a 32-bit integer into a list of immediate arguments,
+    whose sum or "or" or "xor" equals the integer. *)
+
+Fixpoint decompose_int_rec (N: nat) (n p: int) : list int :=
+  match N with
+  | Datatypes.O =>
+      if Int.eq_dec n Int.zero then nil else n :: nil
+  | Datatypes.S M =>
+      if Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero then
+        decompose_int_rec M n (Int.add p (Int.repr 2))
+      else
+        let m := Int.shl (Int.repr 255) p in
+        Int.and n m ::
+        decompose_int_rec M (Int.and n (Int.not m)) (Int.add p (Int.repr 2))
+  end.
+
+Definition decompose_int (n: int) : list int :=
+  match decompose_int_rec 12%nat n Int.zero with
+  | nil => Int.zero :: nil
+  | l   => l
+  end.
+
+Definition iterate_op (op1 op2: shift_op -> instruction) (l: list int) (k: code) :=
+  match l with
+  | nil =>
+      op1 (SOimm Int.zero) :: k                 (**r should never happen *)
+  | i :: l' =>
+      op1 (SOimm i) :: map (fun i => op2 (SOimm i)) l' ++ k
+  end.
+
 (** Smart constructors for integer immediate arguments. *)
 
 Definition loadimm (r: ireg) (n: int) (k: code) :=
-  if is_immed_arith n then
-    Pmov r (SOimm n) :: k
-  else if is_immed_arith (Int.not n) then
-    Pmvn r (SOimm (Int.not n)) :: k
-  else                  (* could be much improved! *)
-    Pmov r (SOimm (Int.and n (Int.repr 255))) ::
-    Porr r r (SOimm (Int.and n (Int.repr 65280))) ::
-    Porr r r (SOimm (Int.and n (Int.repr 16711680))) ::
-    Porr r r (SOimm (Int.and n (Int.repr 4278190080))) ::
-    k.
+  let d1 := decompose_int n in
+  let d2 := decompose_int (Int.not n) in
+  if le_dec (List.length d1) (List.length d2)
+  then iterate_op (Pmov r) (Porr r r) d1 k
+  else iterate_op (Pmvn r) (Pbic r r) d2 k.
 
 Definition addimm (r1 r2: ireg) (n: int) (k: code) :=
-  if is_immed_arith n then
-    Padd r1 r2 (SOimm n) :: k
-  else if is_immed_arith (Int.neg n) then
-    Psub r1 r2 (SOimm (Int.neg n)) :: k
-  else
-    Padd r1 r2 (SOimm (Int.and n (Int.repr 255))) ::
-    Padd r1 r1 (SOimm (Int.and n (Int.repr 65280))) ::
-    Padd r1 r1 (SOimm (Int.and n (Int.repr 16711680))) ::
-    Padd r1 r1 (SOimm (Int.and n (Int.repr 4278190080))) ::
-    k.
+  let d1 := decompose_int n in
+  let d2 := decompose_int (Int.neg n) in
+  if le_dec (List.length d1) (List.length d2)
+  then iterate_op (Padd r1 r2) (Padd r1 r1) d1 k
+  else iterate_op (Psub r1 r2) (Psub r1 r1) d2 k.
 
 Definition andimm (r1 r2: ireg) (n: int) (k: code) :=
-  if is_immed_arith n then
-    Pand r1 r2 (SOimm n) :: k
-  else if is_immed_arith (Int.not n) then
-    Pbic r1 r2 (SOimm (Int.not n)) :: k
-  else
-    loadimm IR14 n (Pand r1 r2 (SOreg IR14) :: k).
+  if is_immed_arith n 
+  then Pand r1 r2 (SOimm n) :: k
+  else iterate_op (Pbic r1 r2) (Pbic r1 r1) (decompose_int (Int.not n)) k.
 
-Definition makeimm (instr: ireg -> ireg -> shift_op -> instruction)
-                   (r1 r2: ireg) (n: int) (k: code) :=
-  if is_immed_arith n then
-    instr r1 r2 (SOimm n) :: k
-  else
-    loadimm IR14 n (instr r1 r2 (SOreg IR14) :: k).
+Definition rsubimm (r1 r2: ireg) (n: int) (k: code) :=
+  iterate_op (Prsb r1 r2) (Padd r1 r1) (decompose_int n) k.
+
+Definition orimm  (r1 r2: ireg) (n: int) (k: code) :=
+  iterate_op (Porr r1 r2) (Porr r1 r1) (decompose_int n) k.
+
+Definition xorimm  (r1 r2: ireg) (n: int) (k: code) :=
+  iterate_op (Peor r1 r2) (Peor r1 r1) (decompose_int n) k.
 
 (** Translation of a shift immediate operation (type [Op.shift]) *)
 
@@ -235,7 +254,7 @@ Definition transl_op
   | Orsubshift s, a1 :: a2 :: nil =>
       Prsb (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
   | Orsubimm n, a1 :: nil =>
-      makeimm Prsb (ireg_of r) (ireg_of a1) n k
+      rsubimm (ireg_of r) (ireg_of a1) n k
   | Omul, a1 :: a2 :: nil =>
       if ireg_eq (ireg_of r) (ireg_of a1)
       || ireg_eq (ireg_of r) (ireg_of a2)
@@ -256,13 +275,13 @@ Definition transl_op
   | Oorshift s, a1 :: a2 :: nil =>
       Porr (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
   | Oorimm n, a1 :: nil =>
-      makeimm Porr (ireg_of r) (ireg_of a1) n k
+      orimm (ireg_of r) (ireg_of a1) n k
   | Oxor, a1 :: a2 :: nil =>
       Peor (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k
   | Oxorshift s, a1 :: a2 :: nil =>
       Peor (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
   | Oxorimm n, a1 :: nil =>
-      makeimm Peor (ireg_of r) (ireg_of a1) n k
+      xorimm (ireg_of r) (ireg_of a1) n k
   | Obic, a1 :: a2 :: nil =>
       Pbic (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k
   | Obicshift s, a1 :: a2 :: nil =>
@@ -469,12 +488,10 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       Pblsymb symb :: k
   | Mtailcall sig (inl r) =>
       loadind_int IR13 f.(fn_retaddr_ofs) IR14
-        (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
-         :: Pbreg (ireg_of r) :: k)
+        (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg (ireg_of r) :: k)
   | Mtailcall sig (inr symb) =>
       loadind_int IR13 f.(fn_retaddr_ofs) IR14
-        (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
-         :: Pbsymb symb :: k)
+        (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb symb :: k)
   | Mbuiltin ef args res =>
       Pbuiltin ef (map preg_of args) (preg_of res) :: k
   | Mlabel lbl =>
@@ -488,8 +505,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       Pbtbl IR14 tbl :: k
   | Mreturn =>
       loadind_int IR13 f.(fn_retaddr_ofs) IR14
-        (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
-         :: Pbreg IR14 :: k)
+        (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: k)
   end.
 
 Definition transl_code (f: Mach.function) (il: list Mach.instruction) :=
@@ -501,7 +517,7 @@ Definition transl_code (f: Mach.function) (il: list Mach.instruction) :=
   around, leading to incorrect executions. *)
 
 Definition transl_function (f: Mach.function) :=
-  Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) ::
+  Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
   Pstr IR14 IR13 (SAimm f.(fn_retaddr_ofs)) ::
   transl_code f f.(fn_code).