define some semantics in Asm

2 files changed, 24 insertions, 3 deletions

diff --git a/riscV/Asm.v b/riscV/Asm.v
index dc410a3b..599002e7 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -30,6 +30,7 @@ Require Import Smallstep.
 Require Import Locations.
 Require Stacklayout.
 Require Import Conventions.
+Require ExtValues.
 
 (** * Abstract syntax *)
 
@@ -918,6 +919,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#d <- (Val.floatofsingle rs#s))) m
   | Pfcvtsd d s =>
       Next (nextinstr (rs#d <- (Val.singleoffloat rs#s))) m
+          
+  | Pfmvxs d s =>
+      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
+
 
 (** Pseudo-instructions *)
   | Pallocframe sz pos =>
@@ -968,9 +975,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       so we do not model them. *)
   | Pfence
 
-  | Pfmvxs _ _
-  | Pfmvxd _ _
-
   | Pfmins _ _ _
   | Pfmaxs _ _ _
   | Pfsqrts _ _
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)))).
+*)