diff options
-rw-r--r-- | kvx/Builtins1.v | 10 | ||||
-rw-r--r-- | kvx/CBuiltins.ml | 4 | ||||
-rw-r--r-- | kvx/SelectOp.vp | 2 | ||||
-rw-r--r-- | kvx/SelectOpproof.v | 8 | ||||
-rw-r--r-- | kvx/TargetPrinter.ml | 8 |
5 files changed, 27 insertions, 5 deletions
diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v index 441345bf..de0d9885 100644 --- a/kvx/Builtins1.v +++ b/kvx/Builtins1.v @@ -25,7 +25,9 @@ Inductive platform_builtin : Type := | BI_fminf | BI_fmaxf | BI_fma -| BI_fmaf. +| BI_fmaf +| BI_lround_ne +| BI_luround_ne. Local Open Scope string_scope. @@ -36,6 +38,8 @@ Definition platform_builtin_table : list (string * platform_builtin) := :: ("__builtin_fmaxf", BI_fmaxf) :: ("__builtin_fma", BI_fma) :: ("__builtin_fmaf", BI_fmaf) + :: ("__builtin_lround_ne", BI_lround_ne) + :: ("__builtin_luround_ne", BI_luround_ne) :: nil. Definition platform_builtin_sig (b: platform_builtin) : signature := @@ -48,6 +52,8 @@ Definition platform_builtin_sig (b: platform_builtin) : signature := mksignature (Tfloat :: Tfloat :: Tfloat :: nil) Tfloat cc_default | BI_fmaf => mksignature (Tsingle :: Tsingle :: Tsingle :: nil) Tsingle cc_default + | BI_lround_ne | BI_luround_ne => + mksignature (Tfloat :: nil) Tlong cc_default end. Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := @@ -58,4 +64,6 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl | BI_fmaxf => mkbuiltin_n2t Tsingle Tsingle Tsingle ExtFloat32.max | BI_fma => mkbuiltin_n3t Tfloat Tfloat Tfloat Tfloat Float.fma | BI_fmaf => mkbuiltin_n3t Tsingle Tsingle Tsingle Tsingle Float32.fma + | BI_lround_ne => mkbuiltin_n1p Tfloat Tlong Float.to_long_ne + | BI_luround_ne => mkbuiltin_n1p Tfloat Tlong Float.to_longu_ne end. diff --git a/kvx/CBuiltins.ml b/kvx/CBuiltins.ml index 7398e0f4..f2b7b09e 100644 --- a/kvx/CBuiltins.ml +++ b/kvx/CBuiltins.ml @@ -133,6 +133,10 @@ let builtins = { "__builtin_fmaf", (TFloat(FFloat, []), [TFloat(FFloat, []); TFloat(FFloat, []); TFloat(FFloat, [])], false); + "__builtin_lround_ne", + (TInt(ILong, []), [TFloat(FDouble, [])], false); + "__builtin_luround_ne", + (TInt(IULong, []), [TFloat(FDouble, [])], false); ] } diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp index 4e1087f9..f529907d 100644 --- a/kvx/SelectOp.vp +++ b/kvx/SelectOp.vp @@ -750,6 +750,8 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr | BI_fmaxf => Some (Eop Omaxfs args) | BI_fma => gen_fma args | BI_fmaf => gen_fmaf args + | BI_lround_ne => Some (Eop Olongoffloat_ne args) + | BI_luround_ne => Some (Eop Olonguoffloat_ne args) end. End SELECT. diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index 0ede1e2d..a374ec54 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -1896,6 +1896,14 @@ Proof. repeat (try econstructor; try eassumption)). - apply eval_fma; assumption. - apply eval_fmaf; assumption. + - cbn in *; + destruct vl; trivial. destruct vl; trivial. + destruct v0; try discriminate; + cbn; rewrite H0; reflexivity. + - cbn in *; + destruct vl; trivial. destruct vl; trivial. + destruct v0; try discriminate; + cbn; rewrite H0; reflexivity. Qed. End CMCONSTR. diff --git a/kvx/TargetPrinter.ml b/kvx/TargetPrinter.ml index 40e2be55..01733858 100644 --- a/kvx/TargetPrinter.ml +++ b/kvx/TargetPrinter.ml @@ -587,13 +587,13 @@ module Target (*: TARGET*) = | Pfixedudrzz(rd, rs) | Pfixedudrzz_i32(rd, rs) -> fprintf oc " fixedud.rz %a = %a, 0\n" ireg rd ireg rs | Pfixedudrne(rd, rs) -> - fprintf oc " fixedud.ne %a = %a, 0\n" ireg rd ireg rs + fprintf oc " fixedud.rn %a = %a, 0\n" ireg rd ireg rs | Pfixeddrne(rd, rs) -> - fprintf oc " fixedd.ne %a = %a, 0\n" ireg rd ireg rs + fprintf oc " fixedd.rn %a = %a, 0\n" ireg rd ireg rs | Pfixeduwrne(rd, rs) -> - fprintf oc " fixeduw.ne %a = %a, 0\n" ireg rd ireg rs + fprintf oc " fixeduw.rn %a = %a, 0\n" ireg rd ireg rs | Pfixedwrne(rd, rs) -> - fprintf oc " fixedw.ne %a = %a, 0\n" ireg rd ireg rs + fprintf oc " fixedw.rn %a = %a, 0\n" ireg rd ireg rs (* Arith RI32 instructions *) | Pmake (rd, imm) -> |