From 6eabac7e12de09dc4b2a32fa2458e3b91fb34471 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 1 Feb 2021 14:34:30 +0100 Subject: define some semantics in Asm --- riscV/Asm.v | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'riscV/Asm.v') 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 _ _ -- cgit