From 87de3969856cf6a5eb5e1615ec817a015ed90d1c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 21 Jan 2022 11:48:06 +0100 Subject: Return second arg for float min/max on x86. If both arguments are zero the second argument is returned independ from their sign. Bug 32640 --- x86/Builtins1.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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. -- cgit From 38b0425d524cd3e7260ac46e13153f007e8bc00d Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 7 Feb 2022 15:10:54 +0100 Subject: Add op for float max and min for x86. The ops `Omaxf` and `Ominf` have the same semantics as `minsd` and `maxsd` instruction, i.e. if both arguments are equal the second argument is returned as well as for NaN. The operations are the used in SelectOp to implement the built-in function `__builtin_fmax` and `__builtin_fmin`. Bug 32640 --- x86/Asm.v | 6 ++++-- x86/Asmexpand.ml | 18 ------------------ x86/Asmgen.v | 6 ++++++ x86/Machregs.v | 2 ++ x86/NeedOp.v | 2 +- x86/Op.v | 36 ++++++++++++++++++++++++++++++++++++ x86/PrintOp.ml | 2 ++ x86/SelectOp.vp | 6 +++++- x86/SelectOpproof.v | 7 ++++++- x86/ValueAOp.v | 4 ++++ 10 files changed, 66 insertions(+), 23 deletions(-) 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 a1c24f2d..b76ad3a3 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 73e3263e..f8d25a50 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/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 16d75426..fde078dc 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... @@ -1290,6 +1324,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 31be8c32..99496ba1 100644 --- a/x86/SelectOp.vp +++ b/x86/SelectOp.vp @@ -579,4 +579,8 @@ Nondetfunction builtin_arg (e: 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 d8ab32a4..61cbf72b 100644 --- a/x86/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -1021,7 +1021,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 d0b8427a..298a1a58 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. -- cgit From 9d3521b4db46773239a2c5f9f6970de826075508 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 11 Feb 2022 17:49:36 +0100 Subject: Check for arguments of struct/union type passed to a vararg function If any are found, make sure that `-fstruct-passing` was given. Previously, we used to check the fixed arguments (as part of a call to `checkFunctionType`) but not the variable arguments. --- cfrontend/C2C.ml | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 3c71718c..7c6a4994 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -520,19 +520,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 = @@ -965,12 +967,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 = -- cgit