bits to float

9 files changed, 82 insertions, 5 deletions

diff --git a/riscV/Asm.v b/riscV/Asm.v
index 599002e7..d1946a06 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -256,8 +256,10 @@ Inductive instruction : Type :=
 
   (* floating point register move *)
   | Pfmv     (rd: freg) (rs: freg)                  (**r move *)
-  | Pfmvxs   (rd: ireg) (rs: freg)                  (**r move FP single to integer register *)
-  | Pfmvxd   (rd: ireg) (rs: freg)                  (**r move FP double to integer register *)
+  | Pfmvxs   (rd: ireg) (rs: freg)                  (**r bitwise move FP single to integer register *)
+  | Pfmvxd   (rd: ireg) (rs: freg)                  (**r bitwise move FP double to integer register *)
+  | Pfmvsx   (rd: freg) (rs: ireg)                  (**r bitwise move integer register to FP single *)
+  | Pfmvdx   (rd: freg) (rs: ireg)                  (**r bitwise move integer register to FP double*)
 
   (* 32-bit (single-precision) floating point *)
   | Pfls     (rd: freg) (ra: ireg) (ofs: offset)    (**r load float *)
@@ -924,6 +926,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#d <- (ExtValues.bits_of_single rs#s))) m
   | Pfmvxd d s =>
       Next (nextinstr (rs#d <- (ExtValues.bits_of_float rs#s))) m
+          
+  | Pfmvsx d s =>
+      Next (nextinstr (rs#d <- (ExtValues.single_of_bits rs#s))) m
+  | Pfmvdx d s =>
+      Next (nextinstr (rs#d <- (ExtValues.float_of_bits rs#s))) m
 
 
 (** Pseudo-instructions *)
diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v
index 86bcb2ac..47bacffa 100644
--- a/riscV/Builtins1.v
+++ b/riscV/Builtins1.v
@@ -22,23 +22,31 @@ Require ExtValues.
 
 Inductive platform_builtin : Type :=
 | BI_bits_of_float
-| BI_bits_of_double.
+| BI_bits_of_double
+| BI_float_of_bits
+| BI_double_of_bits.
 
 Local Open Scope string_scope.
 
 Definition platform_builtin_table : list (string * platform_builtin) :=
      ("__builtin_bits_of_float", BI_bits_of_float)
   :: ("__builtin_bits_of_double", BI_bits_of_double)
+  :: ("__builtin_float_of_bits", BI_float_of_bits)
+  :: ("__builtin_double_of_bits", BI_double_of_bits)
   :: nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
   match b with
   | BI_bits_of_float => mksignature (Tsingle :: nil) Tint cc_default
   | BI_bits_of_double => mksignature (Tfloat :: nil) Tlong cc_default
+  | BI_float_of_bits => mksignature (Tint :: nil) Tsingle cc_default
+  | BI_double_of_bits => mksignature (Tlong :: nil) Tfloat cc_default
   end.
 
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
   match b with
   | BI_bits_of_float => mkbuiltin_n1t Tsingle Tint Float32.to_bits
   | BI_bits_of_double => mkbuiltin_n1t Tfloat Tlong Float.to_bits
+  | BI_float_of_bits => mkbuiltin_n1t Tint Tsingle Float32.of_bits
+  | BI_double_of_bits => mkbuiltin_n1t Tlong Tfloat Float.of_bits
   end.
diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml
index 55b6bbd5..00b44fd5 100644
--- a/riscV/CBuiltins.ml
+++ b/riscV/CBuiltins.ml
@@ -50,6 +50,10 @@ let builtins = {
       (TInt(IULong, []), [TFloat(FDouble, [])], false);
     "__builtin_bits_of_float",
       (TInt(IUInt, []), [TFloat(FFloat, [])], false);
+    "__builtin_double_of_bits",
+      (TFloat(FDouble, []), [TInt(IULong, [])], false);
+    "__builtin_float_of_bits",
+      (TFloat(FFloat, []), [TInt(IUInt, [])], false);
   ]
 }
 
diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index 4edd2e3d..39070e7b 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -15,6 +15,18 @@ Definition bits_of_single x :=
   | _ => Vundef
   end.
 
+Definition float_of_bits x :=
+  match x with
+  | Vlong f => Vfloat (Float.of_bits f)
+  | _ => Vundef
+  end.
+
+Definition single_of_bits x :=
+  match x with
+  | Vint f => Vsingle (Float32.of_bits f)
+  | _ => Vundef
+  end.
+
 Definition bitwise_select_int b vtrue vfalse :=
   Val.or (Val.and (Val.neg b) vtrue)
          (Val.and (Val.sub b Vone) vfalse).
diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v
index 9a406b6f..136c157f 100644
--- a/riscV/NeedOp.v
+++ b/riscV/NeedOp.v
@@ -89,6 +89,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Ocmp c => needs_of_condition c
   | Obits_of_single => op1 (default nv)
   | Obits_of_float => op1 (default nv)
+  | Osingle_of_bits => op1 (default nv)
+  | Ofloat_of_bits => op1 (default nv)
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
diff --git a/riscV/Op.v b/riscV/Op.v
index 160e4412..21de7787 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -155,7 +155,9 @@ Inductive operation : Type :=
 (*c Boolean tests: *)
   | Ocmp (cond: condition)  (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
   | Obits_of_single
-  | Obits_of_float.
+  | Obits_of_float
+  | Osingle_of_bits
+  | Ofloat_of_bits.
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -322,6 +324,8 @@ Definition eval_operation
   | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1))
   | Obits_of_single, v1::nil => Some (ExtValues.bits_of_single v1)
   | Obits_of_float, v1::nil => Some (ExtValues.bits_of_float v1)
+  | Osingle_of_bits, v1::nil => Some (ExtValues.single_of_bits v1)
+  | Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits v1)
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
   | _, _ => None
   end.
@@ -481,6 +485,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ocmp c => (type_of_condition c, Tint)
   | Obits_of_single => (Tsingle :: nil, Tint)
   | Obits_of_float => (Tfloat :: nil, Tlong)
+  | Osingle_of_bits => (Tint :: nil, Tsingle)
+  | Ofloat_of_bits => (Tlong :: nil, Tfloat)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
@@ -690,6 +696,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* Bits_of_single, float *)
   - destruct v0; cbn; trivial.
   - destruct v0; cbn; trivial.
+  (* single, float of bits *)
+  - destruct v0; cbn; trivial.
+  - destruct v0; cbn; trivial.
 Qed.
 
 (* This should not be simplified to "false" because it breaks proofs elsewhere. *)
@@ -1259,6 +1268,9 @@ Proof.
   (* Bits_of_single, double *)
   - inv H4; simpl; auto.
   - inv H4; simpl; auto.
+  (* single, double of bits *)
+  - inv H4; simpl; auto.
+  - inv H4; simpl; auto.
 Qed.
 
 Lemma eval_addressing_inj:
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index 87e3af05..7714f12d 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -465,4 +465,6 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr
   match b with
   | BI_bits_of_float => Some (Eop Obits_of_single args)
   | BI_bits_of_double => Some (Eop Obits_of_float args)
+  | BI_float_of_bits => Some (Eop Osingle_of_bits args)
+  | BI_double_of_bits => Some (Eop Ofloat_of_bits args)
   end.
\ No newline at end of file
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 1f02ca71..4bcfa6af 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -396,6 +396,10 @@ module Target : TARGET =
          fprintf oc "	fmv.x.s	%a, %a\n"     ireg rd freg fs
       | Pfmvxd (rd,fs) ->
          fprintf oc "	fmv.x.d	%a, %a\n"     ireg rd freg fs
+      | Pfmvsx (fd,rs) ->
+         fprintf oc "	fmv.s.x	%a, %a\n"     freg fd ireg rs
+      | Pfmvdx (fd,rs) ->
+         fprintf oc "	fmv.d.x	%a, %a\n"     freg fd ireg rs
 
       (* 32-bit (single-precision) floating point *)
       | Pfls (fd, ra, ofs) ->
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index e1ba878e..f94669a2 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -54,6 +54,18 @@ Definition bits_of_float (v : aval) : aval :=
   | _ => ntop1 v
   end.
 
+Definition single_of_bits (v : aval) : aval :=
+  match v with
+  | I f => FS (Float32.of_bits f)
+  | _ => ntop1 v
+  end.
+
+Definition float_of_bits (v : aval) : aval :=
+  match v with
+  | L f => F (Float.of_bits f)
+  | _ => ntop1 v
+  end.
+
 Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   match op, vl with
   | Omove, v1::nil => v1
@@ -151,6 +163,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Ocmp c, _ => of_optbool (eval_static_condition c vl)
   | Obits_of_single, v1::nil => bits_of_single v1
   | Obits_of_float, v1::nil => bits_of_float v1
+  | Osingle_of_bits, v1::nil => single_of_bits v1
+  | Ofloat_of_bits, v1::nil => float_of_bits v1
   | _, _ => Vbot
   end.
 
@@ -174,7 +188,19 @@ Proof.
   unfold ExtValues.bits_of_float; intros. inv H; cbn; constructor.
 Qed.
 
-Hint Resolve bits_of_single_sound bits_of_float_sound : va.
+Lemma single_of_bits_sound:
+  forall v x, vmatch bc v x -> vmatch bc (ExtValues.single_of_bits v) (single_of_bits x).
+Proof.
+  unfold ExtValues.bits_of_single; intros. inv H; cbn; constructor.
+Qed.
+
+Lemma float_of_bits_sound:
+  forall v x, vmatch bc v x -> vmatch bc (ExtValues.float_of_bits v) (float_of_bits x).
+Proof.
+  unfold ExtValues.bits_of_float; intros. inv H; cbn; constructor.
+Qed.
+
+Hint Resolve bits_of_single_sound bits_of_float_sound single_of_bits_sound float_of_bits_sound : va.
 
 Theorem eval_static_condition_sound:
   forall cond vargs m aargs,