Merge remote-tracking branch 'absint/master' into merge_absint

12 files changed, 86 insertions, 40 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 502108f8..3dc40a1e 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -619,19 +619,21 @@ let convertFkind k a : coq_type =
       if not !Clflags.option_flongdouble then unsupported "'long double' type";
       Tfloat (F64, a)
 
+let checkResultType env ty =
+  if (not !Clflags.option_fstruct_passing) && Cutil.is_composite_type env ty
+  then unsupported "function returning a struct or union \
+                    (consider adding option [-fstruct-passing])"
+
+let checkArgumentType env ty =
+  if (not !Clflags.option_fstruct_passing) && Cutil.is_composite_type env ty
+  then unsupported "function parameter of struct or union type \
+                    (consider adding option [-fstruct-passing])"
+
 let checkFunctionType env tres targs =
-  if not !Clflags.option_fstruct_passing then begin
-    if Cutil.is_composite_type env tres then
-      unsupported "function returning a struct or union (consider adding option [-fstruct-passing])";
-    begin match targs with
-    | None -> ()
-    | Some l ->
-        List.iter
-          (fun (id, ty) ->
-            if Cutil.is_composite_type env ty then
-              unsupported "function parameter of struct or union type (consider adding option [-fstruct-passing])")
-          l
-    end
+  checkResultType env tres;
+  begin match targs with
+  | None -> ()
+  | Some l -> List.iter (fun (id, ty) -> checkArgumentType env ty) l
   end
 
 let rec convertTyp env ?bitwidth t =
@@ -1072,12 +1074,13 @@ let rec convertExpr env e =
       | None ->
           error "wrong type for function part of a call"
       | Some(tres, targs, va) ->
-          checkFunctionType env tres targs;
           if targs = None && not !Clflags.option_funprototyped then
             unsupported "call to unprototyped function (consider adding option [-funprototyped])";
           if va && not !Clflags.option_fvararg_calls then
             unsupported "call to variable-argument function (consider adding option [-fvararg-calls])"
       end;
+      checkResultType env e.etyp;
+      List.iter (fun arg -> checkArgumentType env arg.etyp) args;
       ewrap (Ctyping.ecall (convertExpr env fn) (convertExprList env args))
 
 and convertLvalue env e =
diff --git a/x86/Asm.v b/x86/Asm.v
index 799b533e..b9c4817a 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -877,6 +877,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (compare_floats (rs r1) (rs r2) rs)) m
   | Pxorpd_f rd =>
       Next (nextinstr_nf (rs#rd <- (Vfloat Float.zero))) m
+  | Pmaxsd rd r1 =>
+      Next (nextinstr (rs#rd <- (Op.maxf rs#rd rs#r1))) m
+  | Pminsd rd r1 =>
+      Next (nextinstr (rs#rd <- (Op.minf rs#rd rs#r1))) m
   (** Arithmetic operations over single-precision floats *)
   | Padds_ff rd r1 =>
       Next (nextinstr (rs#rd <- (Val.addfs rs#rd rs#r1))) m
@@ -996,8 +1000,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfnmsub132 _ _ _
   | Pfnmsub213 _ _ _
   | Pfnmsub231 _ _ _
-  | Pmaxsd _ _
-  | Pminsd _ _
   | Pmovb_rm _ _
   | Pmovq_rf _ _
   | Pmovsq_rm _ _
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index f81b9165..09a09ada 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -408,24 +408,6 @@ let expand_builtin_inline name args res =
   (* Float arithmetic *)
   | ("__builtin_fsqrt" | "__builtin_sqrt"), [BA(FR a1)], BR(FR res) ->
      emit (Psqrtsd (res,a1))
-  | "__builtin_fmax", [BA(FR a1); BA(FR a2)], BR(FR res) ->
-     if res = a1 then
-       emit (Pmaxsd (res,a2))
-     else if res = a2 then
-       emit (Pmaxsd (res,a1))
-     else begin
-	 emit (Pmovsd_ff (res,a1));
-	 emit (Pmaxsd (res,a2))
-       end
-  | "__builtin_fmin", [BA(FR a1); BA(FR a2)], BR(FR res) ->
-     if res = a1 then
-       emit (Pminsd (res,a2))
-     else if res = a2 then
-       emit (Pminsd (res,a1))
-     else begin
-	 emit (Pmovsd_ff (res,a1));
-	 emit (Pminsd (res,a2))
-       end
   | "__builtin_fmadd",  _, _ ->
       expand_fma args res
         (fun r1 r2 r3 -> Pfmadd132(r1, r2, r3))
diff --git a/x86/Asmgen.v b/x86/Asmgen.v
index 99e9fc2b..ec97aff4 100644
--- a/x86/Asmgen.v
+++ b/x86/Asmgen.v
@@ -585,6 +585,12 @@ Definition transl_op
   | Odivf, a1 :: a2 :: nil =>
       assertion (mreg_eq a1 res);
       do r <- freg_of res; do r2 <- freg_of a2; OK (Pdivd_ff r r2 :: k)
+  | Omaxf, a1 :: a2 :: nil =>
+      assertion (mreg_eq a1 res);
+      do r <- freg_of res; do r2 <- freg_of a2; OK (Pmaxsd r r2 :: k)
+  | Ominf, a1 :: a2 :: nil =>
+      assertion (mreg_eq a1 res);
+      do r <- freg_of res; do r2 <- freg_of a2; OK (Pminsd r r2 :: k)
   | Onegfs, a1 :: nil =>
       assertion (mreg_eq a1 res);
       do r <- freg_of res; OK (Pnegs r :: k)
diff --git a/x86/Builtins1.v b/x86/Builtins1.v
index e5233ff5..7c77a488 100644
--- a/x86/Builtins1.v
+++ b/x86/Builtins1.v
@@ -42,14 +42,14 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl
   | 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
+                      | Some Lt => f1
+                      | Some Eq | 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
+                      | Some Gt => f1
+                      | Some Eq | Some Lt | None => f2
                       end)
   end.
 
diff --git a/x86/Machregs.v b/x86/Machregs.v
index a440bffc..042248a8 100644
--- a/x86/Machregs.v
+++ b/x86/Machregs.v
@@ -334,6 +334,8 @@ Definition two_address_op (op: operation) : bool :=
   | Osubf => true
   | Omulf => true
   | Odivf => true
+  | Omaxf => true
+  | Ominf => true
   | Onegfs => true
   | Oabsfs => true
   | Oaddfs => true
diff --git a/x86/NeedOp.v b/x86/NeedOp.v
index 775a23db..9c7469e9 100644
--- a/x86/NeedOp.v
+++ b/x86/NeedOp.v
@@ -113,7 +113,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Ororlimm _ => op1 (default nv)
   | Oleal addr => needs_of_addressing_64 addr nv
   | Onegf | Oabsf => op1 (default nv)
-  | Oaddf | Osubf | Omulf | Odivf => op2 (default nv)
+  | Oaddf | Osubf | Omulf | Odivf | Omaxf | Ominf => op2 (default nv)
   | Onegfs | Oabsfs => op1 (default nv)
   | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv)
   | Osingleoffloat | Ofloatofsingle => op1 (default nv)
diff --git a/x86/Op.v b/x86/Op.v
index caa63235..d96ad12c 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -149,6 +149,8 @@ Inductive operation : Type :=
   | Osubf                    (**r [rd = r1 - r2] *)
   | Omulf                    (**r [rd = r1 * r2] *)
   | Odivf                    (**r [rd = r1 / r2] *)
+  | Omaxf                    (**r [rd = max(r1,r2)] *)
+  | Ominf                    (**r [rd = min(r1,r2)] *)
   | Onegfs                   (**r [rd = - r1] *)
   | Oabsfs                   (**r [rd = abs(r1)] *)
   | Oaddfs                   (**r [rd = r1 + r2] *)
@@ -198,6 +200,32 @@ Defined.
 
 Global Opaque eq_condition eq_addressing eq_operation.
 
+(** Helper function for floating point maximum and minimum operation *)
+
+Definition float_max f1 f2 :=
+  match Float.compare f1 f2 with
+  | Some Gt => f1
+  | Some Eq | Some Lt| None => f2
+  end.
+
+Definition maxf (v1 v2: val) : val :=
+  match v1, v2 with
+  | Vfloat f1, Vfloat f2 => Vfloat (float_max f1 f2)
+  | _, _ => Vundef
+  end.
+
+Definition float_min f1 f2 :=
+  match Float.compare f1 f2 with
+  | Some Lt => f1
+  | Some Eq | Some Gt| None => f2
+  end.
+
+Definition minf (v1 v2: val) : val :=
+  match v1, v2 with
+  | Vfloat f1, Vfloat f2 => Vfloat (float_min f1 f2)
+  | _, _ => Vundef
+  end.
+
 (** In addressing modes, offsets are 32-bit signed integers, even in
     64-bit mode.  The following function checks that an addressing
     mode is valid, i.e. that the offsets are in range.
@@ -392,6 +420,8 @@ Definition eval_operation
   | Osubf, v1::v2::nil => Some(Val.subf v1 v2)
   | Omulf, v1::v2::nil => Some(Val.mulf v1 v2)
   | Odivf, v1::v2::nil => Some(Val.divf v1 v2)
+  | Omaxf, v1::v2::nil => Some (maxf v1 v2)
+  | Ominf, v1::v2::nil => Some (minf v1 v2)
   | Onegfs, v1::nil => Some(Val.negfs v1)
   | Oabsfs, v1::nil => Some(Val.absfs v1)
   | Oaddfs, v1::v2::nil => Some(Val.addfs v1 v2)
@@ -564,6 +594,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osubf => (Tfloat :: Tfloat :: nil, Tfloat)
   | Omulf => (Tfloat :: Tfloat :: nil, Tfloat)
   | Odivf => (Tfloat :: Tfloat :: nil, Tfloat)
+  | Omaxf => (Tfloat :: Tfloat :: nil, Tfloat)
+  | Ominf => (Tfloat :: Tfloat :: nil, Tfloat)
   | Onegfs => (Tsingle :: nil, Tsingle)
   | Oabsfs => (Tsingle :: nil, Tsingle)
   | Oaddfs => (Tsingle :: Tsingle :: nil, Tsingle)
@@ -722,6 +754,8 @@ Proof with (try exact I; try reflexivity).
   destruct v0; destruct v1...
   destruct v0; destruct v1...
   destruct v0; destruct v1...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1...
   destruct v0...
   destruct v0...
   destruct v0; destruct v1...
@@ -1365,6 +1399,8 @@ Proof.
   inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; inv H2; simpl; auto.
   inv H4; simpl; auto.
   inv H4; simpl; auto.
   inv H4; inv H2; simpl; auto.
diff --git a/x86/PrintOp.ml b/x86/PrintOp.ml
index 6aa4d450..ac2e8f49 100644
--- a/x86/PrintOp.ml
+++ b/x86/PrintOp.ml
@@ -147,6 +147,8 @@ let print_operation reg pp = function
   | Osubf, [r1;r2] -> fprintf pp "%a -f %a" reg r1 reg r2
   | Omulf, [r1;r2] -> fprintf pp "%a *f %a" reg r1 reg r2
   | Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2
+  | Omaxf, [r1;r2] -> fprintf pp "max(%a, %a)" reg r1 reg r2
+  | Ominf, [r1;r2] -> fprintf pp "min(%a, %a)" reg r1 reg r2
   | Onegfs, [r1] -> fprintf pp "negfs(%a)" reg r1
   | Oabsfs, [r1] -> fprintf pp "absfs(%a)" reg r1
   | Oaddfs, [r1;r2] -> fprintf pp "%a +fs %a" reg r1 reg r2
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index 2a09207b..3b64411e 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -587,4 +587,8 @@ Definition divfs_base (e1: expr) (e2: expr) :=
 (** Platform-specific known builtins *)
 
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
-  None.
+  match b, args with
+  | BI_fmax, e1 ::: e2 ::: Enil => Some (Eop Omaxf (e1 ::: e2 ::: Enil))
+  | BI_fmin, e1 ::: e2 ::: Enil => Some (Eop Ominf (e1 ::: e2 ::: Enil))
+  | _, _ => None
+  end.
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index c43beb56..f0a11780 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -1046,7 +1046,12 @@ Theorem eval_platform_builtin:
   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.
+  intros until le. intros SEL ARGS SEM.
+  destruct bf; try discriminate.
+  - inv ARGS; try discriminate. inv H0; try discriminate. inv H2; try discriminate.
+    inv SEL. inv SEM. exists (minf v1 v0); split; auto. EvalOp.
+  - inv ARGS; try discriminate. inv H0; try discriminate. inv H2; try discriminate.
+    inv SEL. inv SEM. exists (maxf v1 v0); split; auto. EvalOp.
 Qed.
 
 End CMCONSTR.
diff --git a/x86/ValueAOp.v b/x86/ValueAOp.v
index e5584b6a..e5c71d11 100644
--- a/x86/ValueAOp.v
+++ b/x86/ValueAOp.v
@@ -143,6 +143,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Osubf, v1::v2::nil => subf v1 v2
   | Omulf, v1::v2::nil => mulf v1 v2
   | Odivf, v1::v2::nil => divf v1 v2
+  | Omaxf, v1::v2::nil =>  binop_float float_max v1 v2
+  | Ominf, v1::v2::nil =>  binop_float float_min v1 v2
   | Onegfs, v1::nil => negfs v1
   | Oabsfs, v1::nil => absfs v1
   | Oaddfs, v1::v2::nil => addfs v1 v2
@@ -258,6 +260,8 @@ Proof.
   destruct (propagate_float_constants tt); constructor.
   eapply eval_static_addressing_32_sound; eauto.
   eapply eval_static_addressing_64_sound; eauto.
+  apply binop_float_sound; auto.
+  apply binop_float_sound; auto.
   apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
   apply select_sound; auto. eapply eval_static_condition_sound; eauto.
 Qed.