Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge

7 files changed, 153 insertions, 31 deletions

diff --git a/x86/Builtins1.v b/x86/Builtins1.v
new file mode 100644
index 00000000..6103cc4c
--- /dev/null
+++ b/x86/Builtins1.v
@@ -0,0 +1,54 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, Collège de France and Inria Paris            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Platform-specific built-in functions *)
+
+Require Import String Coqlib.
+Require Import AST Integers Floats Values.
+Require Import Builtins0.
+
+Inductive platform_builtin : Type :=
+  | BI_fmin
+  | BI_fmax.
+
+Local Open Scope string_scope.
+
+Definition platform_builtin_table : list (string * platform_builtin) :=
+     ("__builtin_fmin", BI_fmin)
+  :: ("__builtin_fmax", BI_fmax)
+  :: nil.
+
+Definition platform_builtin_sig (b: platform_builtin) : signature :=
+  match b with
+  | BI_fmin | BI_fmax =>
+      mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default
+  end.
+
+Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
+  match b with
+  | BI_fmin =>
+      mkbuiltin_n2t Tfloat Tfloat Tfloat
+        (fun f1 f2 => match Float.compare f1 f2 with
+                      | Some Eq | Some Lt => f1
+                      | Some Gt | None => f2
+                      end)
+  | BI_fmax =>
+      mkbuiltin_n2t Tfloat Tfloat Tfloat
+        (fun f1 f2 => match Float.compare f1 f2 with
+                      | Some Eq | Some Gt => f1
+                      | Some Lt | None => f2
+                      end)
+  end.
+
diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml
index 69a2eb64..6fb8b697 100644
--- a/x86/CBuiltins.ml
+++ b/x86/CBuiltins.ml
@@ -26,10 +26,10 @@ let (va_list_type, va_list_scalar, size_va_list) =
     (TPtr(TVoid [], []), true, 4)
 
 let builtins = {
-  Builtins.typedefs = [
+  builtin_typedefs = [
     "__builtin_va_list", va_list_type;
   ];
-  Builtins.functions = [
+  builtin_functions = [
     (* Integer arithmetic *)
     "__builtin_bswap64",
       (TInt(IULongLong, []), [TInt(IULongLong, [])], false);
diff --git a/x86/ConstpropOp.vp b/x86/ConstpropOp.vp
index f59b9dba..ada8d54a 100644
--- a/x86/ConstpropOp.vp
+++ b/x86/ConstpropOp.vp
@@ -16,7 +16,7 @@
 Require Import Coqlib Compopts.
 Require Import AST Integers Floats.
 Require Import Op Registers.
-Require Import ValueDomain.
+Require Import ValueDomain ValueAOp.
 
 (** * Converting known values to constants *)
 
@@ -98,6 +98,15 @@ Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
       make_cmp_base c args vl
   end.
 
+Definition make_select (c: condition) (ty: typ)
+                       (r1 r2: reg) (args: list reg) (vl: list aval) :=
+  match resolve_branch (eval_static_condition c vl) with
+  | Some b => (Omove, (if b then r1 else r2) :: nil)
+  | None =>
+      let (c', args') := cond_strength_reduction c args vl in
+      (Osel c' ty, r1 :: r2 :: args')
+  end.
+
 (** For addressing modes, we need to distinguish
 - reductions that produce pointers (i.e. that produce [Aglobal], [Ainstack], [Abased] and [Abasedscaled] addressing modes), which are valid only if the pointer size is right;
 - other reductions (producing [Aindexed] or [Aindexed2] modes), which are valid independently of the pointer size.
@@ -416,6 +425,7 @@ Nondetfunction op_strength_reduction
       let (addr', args') := addr_strength_reduction_64 addr args vl in
       (Oleal addr', args')
   | Ocmp c, args, vl => make_cmp c args vl
+  | Osel c ty, r1 :: r2 :: args, v1 :: v2 :: vl => make_select c ty r1 r2 args vl
   | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2
   | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2
   | Omulfs, r1 :: r2 :: nil, v1 :: FS n2 :: nil => make_mulfsimm n2 r1 r1 r2
diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v
index 3bb0f3cd..6d2df9c1 100644
--- a/x86/ConstpropOpproof.v
+++ b/x86/ConstpropOpproof.v
@@ -14,7 +14,7 @@
 
 Require Import Coqlib Compopts.
 Require Import Integers Floats Values Memory Globalenvs Events.
-Require Import Op Registers RTL ValueDomain.
+Require Import Op Registers RTL ValueDomain ValueAOp ValueAnalysis.
 Require Import ConstpropOp.
 
 Section STRENGTH_REDUCTION.
@@ -371,6 +371,28 @@ Proof.
 - apply make_cmp_base_correct; auto.
 Qed.
 
+Lemma make_select_correct:
+  forall c ty r1 r2 args vl,
+  vl = map (fun r => AE.get r ae) args ->
+  let (op', args') := make_select c ty r1 r2 args vl in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op' e##args' m = Some v
+         /\ Val.lessdef (Val.select (eval_condition c e##args m) e#r1 e#r2 ty) v.
+Proof.
+  unfold make_select; intros.
+  destruct (resolve_branch (eval_static_condition c vl)) as [b|] eqn:RB.
+- exists (if b then e#r1 else e#r2); split.
++ simpl. destruct b; auto.
++ destruct (eval_condition c e##args m) as [b'|] eqn:EC; simpl; auto.
+  assert (b = b').
+  { eapply resolve_branch_sound; eauto. 
+    rewrite <- EC. apply eval_static_condition_sound with bc. 
+    subst vl. exact (aregs_sound _ _ _ args MATCH). }
+  subst b'. apply Val.lessdef_normalize.
+- generalize (cond_strength_reduction_correct c args vl H).
+  destruct (cond_strength_reduction c args vl) as [cond' args']; intros EQ.
+  econstructor; split. simpl; eauto. rewrite EQ; auto.
+Qed.
+
 Lemma make_addimm_correct:
   forall n r,
   let (op, args) := make_addimm n r in
@@ -905,6 +927,8 @@ Proof.
   auto.
 (* cond *)
   inv H0. apply make_cmp_correct; auto.
+(* select *)
+  inv H0. apply make_select_correct; congruence.
 (* mulf *)
   InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto.
   InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) e#r2).
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index c0434a67..d734ecc6 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -38,9 +38,13 @@
 
 Require Import Coqlib.
 Require Import Compopts.
-Require Import AST Integers Floats.
+Require Import AST Integers Floats Builtins.
 Require Import Op CminorSel.
+<<<<<<< HEAD
 Require Import OpHelpers.
+=======
+Require Archi.
+>>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
 
 Local Open Scope cminorsel_scope.
 
@@ -499,21 +503,27 @@ Nondetfunction floatofint (e: expr) :=
   end.
 
 Definition intuoffloat (e: expr) :=
-  Elet e
-    (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil)
-      (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil))
-        (intoffloat (Eletvar 1))
-        (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.
+  if Archi.splitlong then
+    Elet e
+      (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil)
+        (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil))
+          (intoffloat (Eletvar 1))
+          (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat
+  else
+    Eop Olowlong (Eop Olongoffloat (e ::: Enil) ::: Enil).
 
 Nondetfunction floatofintu (e: expr) :=
   match e with
   | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil
   | _ =>
-    let f := Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil in
-    Elet e
-      (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil))
-        (floatofint (Eletvar O))
-        (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f))
+    if Archi.splitlong then
+      let f := Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil in
+      Elet e
+        (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil))
+          (floatofint (Eletvar O))
+          (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f))
+    else
+      Eop Ofloatoflong (Eop Ocast32unsigned (e ::: Enil) ::: Enil)
   end.
 
 Definition intofsingle (e: expr) := Eop Ointofsingle (e ::: Enil).
@@ -570,9 +580,16 @@ Nondetfunction builtin_arg (e: expr) :=
   | _ => BA e
   end.
 
+<<<<<<< HEAD
 (* floats *)
 Definition divf_base (e1: expr) (e2: expr) :=
   Eop Odivf (e1 ::: e2 ::: Enil).
 
 Definition divfs_base (e1: expr) (e2: expr) :=
   Eop Odivfs (e1 ::: e2 ::: Enil).
+=======
+(** Platform-specific known builtins *)
+
+Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
+  None.
+>>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index 5e0f84e3..b59f4a87 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -13,15 +13,9 @@
 (** Correctness of instruction selection for operators *)
 
 Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Cminor.
-Require Import Op.
-Require Import CminorSel.
+Require Import AST Integers Floats.
+Require Import Values Memory Builtins Globalenvs.
+Require Import Cminor Op CminorSel.
 Require Import SelectOp.
 Require Import OpHelpers.
 Require Import OpHelpersproof.
@@ -838,7 +832,8 @@ Proof.
   intros. destruct x; simpl in H0; try discriminate.
   destruct (Float.to_intu f) as [n|] eqn:?; simpl in H0; inv H0.
   exists (Vint n); split; auto. unfold intuoffloat.
-  set (im := Int.repr Int.half_modulus).
+  destruct Archi.splitlong.
+- set (im := Int.repr Int.half_modulus).
   set (fm := Float.of_intu im).
   assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)).
     constructor. auto.
@@ -865,6 +860,11 @@ Proof.
   rewrite Int.add_neg_zero in A4.
   rewrite Int.add_zero in A4.
   auto.
+- apply Float.to_intu_to_long in Heqo. repeat econstructor. eauto.
+  simpl. rewrite Heqo; reflexivity.
+  simpl. unfold Int64.loword. rewrite Int64.unsigned_repr, Int.repr_unsigned; auto.
+  assert (Int.modulus < Int64.max_unsigned) by reflexivity. 
+  generalize (Int.unsigned_range n); omega.
 Qed.
 
 Theorem eval_floatofintu:
@@ -874,10 +874,11 @@ Theorem eval_floatofintu:
   exists v, eval_expr ge sp e m le (floatofintu a) v /\ Val.lessdef y v.
 Proof.
   intros until y; unfold floatofintu. case (floatofintu_match a); intros.
-  InvEval. TrivialExists.
-  destruct x; simpl in H0; try discriminate. inv H0.
+- InvEval. TrivialExists.
+- destruct x; simpl in H0; try discriminate. inv H0.
   exists (Vfloat (Float.of_intu i)); split; auto.
-  econstructor. eauto.
+  destruct Archi.splitlong.
++ econstructor. eauto.
   set (fm := Float.of_intu Float.ox8000_0000).
   assert (eval_expr ge sp e m (Vint i :: le) (Eletvar O) (Vint i)).
     constructor. auto.
@@ -893,6 +894,7 @@ Proof.
   constructor. EvalOp. simpl; eauto. constructor. simpl; eauto.
   fold fm. rewrite Float.of_intu_of_int_2; auto.
   rewrite Int.sub_add_opp. auto.
++ rewrite Float.of_intu_of_long. repeat econstructor. eauto. reflexivity. 
 Qed.
 
 Theorem eval_intofsingle:
@@ -1014,6 +1016,7 @@ Proof.
 - constructor; auto.
 Qed.
 
+<<<<<<< HEAD
 
 (* floating-point division without HELPERS *)
 Theorem eval_divf_base:
@@ -1035,4 +1038,18 @@ Proof.
   intros; unfold divfs_base.
   TrivialExists.
 Qed.
+=======
+(** Platform-specific known builtins *)
+
+Theorem eval_platform_builtin:
+  forall bf al a vl v le,
+  platform_builtin bf al = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  platform_builtin_sem bf vl = Some v ->
+  exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+  intros. discriminate.
+Qed.
+
+>>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
 End CMCONSTR.
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 3025d2e7..cd54e08b 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -62,8 +62,8 @@ let ireg64 oc r = output_string oc (int64_reg_name r)
 let ireg = if Archi.ptr64 then ireg64 else ireg32
 let freg oc r = output_string oc (float_reg_name r)
 
-let preg oc = function
-  | IR r -> ireg oc r
+let preg_asm oc ty = function
+  | IR r -> if ty = Tlong then ireg64 oc r else ireg32 oc r
   | FR r -> freg oc r
   | _    -> assert false
 
@@ -826,7 +826,7 @@ module Target(System: SYSTEM):TARGET =
                                (P.to_int kind) (extern_atom txt) args
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
-              print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res;
+              print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
           | _ ->
               assert false