From 6eabac7e12de09dc4b2a32fa2458e3b91fb34471 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 1 Feb 2021 14:34:30 +0100
Subject: define some semantics in Asm

---
 riscV/ExtValues.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'riscV/ExtValues.v')

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index 5e6ebf02..4edd2e3d 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -3,6 +3,18 @@ Require Import Integers.
 Require Import Values.
 Require Import Floats.
 
+Definition bits_of_float x :=
+  match x with
+  | Vfloat f => Vlong (Float.to_bits f)
+  | _ => Vundef
+  end.
+
+Definition bits_of_single x :=
+  match x with
+  | Vsingle f => Vint (Float32.to_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).
@@ -76,3 +88,8 @@ Proof.
   rewrite Int64.or_commut.
   apply Int64.or_zero.
 Qed.
+
+(*
+Compute (Int.unsigned (Float32.to_bits (Float32.of_int (Int.repr 4200)))).
+Compute (Int64.unsigned (Float.to_bits (Float.of_int (Int.repr 4233)))).
+*)
-- 
cgit