Obits_of_single etc

1 files changed, 28 insertions, 0 deletions

diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index f4b7b4d6..e1ba878e 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -42,6 +42,18 @@ Definition eval_static_addressing (addr: addressing) (vl: list aval): aval :=
   | _, _ => Vbot
   end.
 
+Definition bits_of_single (v : aval) : aval :=
+  match v with
+  | FS f => I (Float32.to_bits f)
+  | _ => ntop1 v
+  end.
+
+Definition bits_of_float (v : aval) : aval :=
+  match v with
+  | F f => L (Float.to_bits f)
+  | _ => ntop1 v
+  end.
+
 Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   match op, vl with
   | Omove, v1::nil => v1
@@ -137,6 +149,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Osingleoflong, v1::nil => singleoflong v1
   | Osingleoflongu, v1::nil => singleoflongu v1
   | 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
   | _, _ => Vbot
   end.
 
@@ -148,6 +162,20 @@ Hypothesis GENV: genv_match bc ge.
 Variable sp: block.
 Hypothesis STACK: bc sp = BCstack.
 
+Lemma bits_of_single_sound:
+  forall v x, vmatch bc v x -> vmatch bc (ExtValues.bits_of_single v) (bits_of_single x).
+Proof.
+  unfold ExtValues.bits_of_single; intros. inv H; cbn; constructor.
+Qed.
+
+Lemma bits_of_float_sound:
+  forall v x, vmatch bc v x -> vmatch bc (ExtValues.bits_of_float v) (bits_of_float x).
+Proof.
+  unfold ExtValues.bits_of_float; intros. inv H; cbn; constructor.
+Qed.
+
+Hint Resolve bits_of_single_sound bits_of_float_sound : va.
+
 Theorem eval_static_condition_sound:
   forall cond vargs m aargs,
   list_forall2 (vmatch bc) vargs aargs ->