Merge of the reuse-temps branch:

- Reload temporaries are marked as destroyed (set to Vundef) across
  operations in the semantics of LTL, LTLin, Linear and Mach, 
  allowing Asmgen to reuse them.
- Added IA32 port.
- Cleaned up float conversions and axiomatization of floats.



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

1 files changed, 71 insertions, 17 deletions

diff --git a/arm/Op.v b/arm/Op.v
index 1f26a72..606281d 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -110,10 +110,8 @@ Inductive operation : Type :=
   | Odivf: operation                    (**r [rd = r1 / r2] *)
   | Osingleoffloat: operation           (**r [rd] is [r1] truncated to single-precision float *)
 (*c Conversions between int and float: *)
-  | Ointoffloat: operation              (**r [rd = int_of_float(r1)] *)
-  | Ointuoffloat: operation             (**r [rd = unsigned_int_of_float(r1)] *)
+  | Ointoffloat: operation              (**r [rd = signed_int_of_float(r1)] *)
   | Ofloatofint: operation              (**r [rd = float_of_signed_int(r1)] *)
-  | Ofloatofintu: operation             (**r [rd = float_of_unsigned_int(r1)] *)
 (*c Boolean tests: *)
   | Ocmp: condition -> operation.       (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
 
@@ -282,16 +280,9 @@ Definition eval_operation
   | Osubf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.sub f1 f2))
   | Omulf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.mul f1 f2))
   | Odivf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.div f1 f2))
-  | Osingleoffloat, v1 :: nil =>
-      Some (Val.singleoffloat v1)
-  | Ointoffloat, Vfloat f1 :: nil => 
-      Some (Vint (Float.intoffloat f1))
-  | Ointuoffloat, Vfloat f1 :: nil => 
-      Some (Vint (Float.intuoffloat f1))
-  | Ofloatofint, Vint n1 :: nil => 
-      Some (Vfloat (Float.floatofint n1))
-  | Ofloatofintu, Vint n1 :: nil => 
-      Some (Vfloat (Float.floatofintu n1))
+  | Osingleoffloat, v1 :: nil => Some (Val.singleoffloat v1)
+  | Ointoffloat, Vfloat f1 :: nil => Some (Vint (Float.intoffloat f1))
+  | Ofloatofint, Vint n1 :: nil => Some (Vfloat (Float.floatofint n1))
   | Ocmp c, _ =>
       match eval_condition c vl with
       | None => None
@@ -493,9 +484,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Odivf => (Tfloat :: Tfloat :: nil, Tfloat)
   | Osingleoffloat => (Tfloat :: nil, Tfloat)
   | Ointoffloat => (Tfloat :: nil, Tint)
-  | Ointuoffloat => (Tfloat :: nil, Tint)
   | Ofloatofint => (Tint :: nil, Tfloat)
-  | Ofloatofintu => (Tint :: nil, Tfloat)
   | Ocmp c => (type_of_condition c, Tint)
   end.
 
@@ -659,9 +648,7 @@ Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val :
   | Odivf, v1::v2::nil => Val.divf v1 v2
   | Osingleoffloat, v1::nil => Val.singleoffloat v1
   | Ointoffloat, v1::nil => Val.intoffloat v1
-  | Ointuoffloat, v1::nil => Val.intuoffloat v1
   | Ofloatofint, v1::nil => Val.floatofint v1
-  | Ofloatofintu, v1::nil => Val.floatofintu v1
   | Ocmp c, _ => eval_condition_total c vl
   | _, _ => Vundef
   end.
@@ -919,3 +906,70 @@ Lemma type_op_for_binary_addressing:
 Proof.
   intros. destruct addr; simpl in H; reflexivity || omegaContradiction.
 Qed.
+
+(** Two-address operations.  There are none in the ARM architecture. *)
+
+Definition two_address_op (op: operation) : bool := false.
+
+(** Operations that are so cheap to recompute that CSE should not factor them out. *)
+
+Definition is_trivial_op (op: operation) : bool :=
+  match op with
+  | Omove => true
+  | Ointconst _ => true
+  | Oaddrsymbol _ _ => true
+  | Oaddrstack _ => true
+  | _ => false
+  end.
+
+(** Shifting stack-relative references.  This is used in [Stacking]. *)
+
+Definition shift_stack_addressing (delta: int) (addr: addressing) :=
+  match addr with
+  | Ainstack ofs => Ainstack (Int.add delta ofs)
+  | _ => addr
+  end.
+
+Definition shift_stack_operation (delta: int) (op: operation) :=
+  match op with
+  | Oaddrstack ofs => Oaddrstack (Int.add delta ofs)
+  | _ => op
+  end.
+
+Lemma shift_stack_eval_addressing:
+  forall (F V: Type) (ge: Genv.t F V) sp addr args delta,
+  eval_addressing ge (Val.sub sp (Vint delta)) (shift_stack_addressing delta addr) args =
+  eval_addressing ge sp addr args.
+Proof.
+  intros. destruct addr; simpl; auto. 
+  destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. 
+  decEq. decEq. rewrite <- Int.add_assoc. decEq. 
+  rewrite Int.sub_add_opp. rewrite Int.add_assoc.
+  rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. 
+  rewrite Int.sub_idem. apply Int.add_zero. 
+Qed.
+
+Lemma shift_stack_eval_operation:
+  forall (F V: Type) (ge: Genv.t F V) sp op args delta,
+  eval_operation ge (Val.sub sp (Vint delta)) (shift_stack_operation delta op) args =
+  eval_operation ge sp op args.
+Proof.
+  intros. destruct op; simpl; auto.
+  destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. 
+  decEq. decEq. rewrite <- Int.add_assoc. decEq. 
+  rewrite Int.sub_add_opp. rewrite Int.add_assoc.
+  rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. 
+  rewrite Int.sub_idem. apply Int.add_zero. 
+Qed.
+
+Lemma type_shift_stack_addressing:
+  forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr.
+Proof.
+  intros. destruct addr; auto. 
+Qed.
+
+Lemma type_shift_stack_operation:
+  forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op.
+Proof.
+  intros. destruct op; auto.
+Qed.