fix assembly syntax

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) ->