bits to float

1 files changed, 27 insertions, 1 deletions

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,