bits to float

1 files changed, 13 insertions, 1 deletions

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: