From b4a08d0815342b6238d307864f0823d0f07bb691 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 26 May 2020 22:04:20 +0200 Subject: k1c -> kvx changes --- kvx/ExtFloats.v | 54 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 54 insertions(+) create mode 100644 kvx/ExtFloats.v (limited to 'kvx/ExtFloats.v') diff --git a/kvx/ExtFloats.v b/kvx/ExtFloats.v new file mode 100644 index 00000000..b08503a5 --- /dev/null +++ b/kvx/ExtFloats.v @@ -0,0 +1,54 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +Require Import Floats Integers ZArith. + +Module ExtFloat. +(** TODO check with the actual KVX; + this is what happens on x86 and may be inappropriate. *) + +Definition min (x : float) (y : float) : float := + match Float.compare x y with + | Some Eq | Some Lt => x + | Some Gt | None => y + end. + +Definition max (x : float) (y : float) : float := + match Float.compare x y with + | Some Eq | Some Gt => x + | Some Lt | None => y + end. +End ExtFloat. + +Module ExtFloat32. +(** TODO check with the actual KVX *) + +Definition min (x : float32) (y : float32) : float32 := + match Float32.compare x y with + | Some Eq | Some Lt => x + | Some Gt | None => y + end. + +Definition max (x : float32) (y : float32) : float32 := + match Float32.compare x y with + | Some Eq | Some Gt => x + | Some Lt | None => y + end. + +Definition one := Float32.of_int (Int.repr (1%Z)). +Definition inv (x : float32) : float32 := + Float32.div one x. + +End ExtFloat32. -- cgit