diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-05-26 22:04:20 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-05-26 22:04:20 +0200 |
commit | b4a08d0815342b6238d307864f0823d0f07bb691 (patch) | |
tree | 85f48254ca79a6e2bc9d7359017a5731f98f897f /kvx/Archi.v | |
parent | 490a6caea1a95cfdbddf7aca244fa6a1c83aa9a2 (diff) | |
download | compcert-kvx-b4a08d0815342b6238d307864f0823d0f07bb691.tar.gz compcert-kvx-b4a08d0815342b6238d307864f0823d0f07bb691.zip |
k1c -> kvx changes
Diffstat (limited to 'kvx/Archi.v')
-rw-r--r-- | kvx/Archi.v | 80 |
1 files changed, 80 insertions, 0 deletions
diff --git a/kvx/Archi.v b/kvx/Archi.v new file mode 100644 index 00000000..6d59a3d1 --- /dev/null +++ b/kvx/Archi.v @@ -0,0 +1,80 @@ +(* *************************************************************) +(* *) +(* 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. *) +(* *) +(* *************************************************************) + +(** Architecture-dependent parameters for MPPA KVX. Mostly copied from the Risc-V backend *) + +Require Import ZArith List. +Require Import Binary Bits. + +Definition ptr64 := true. + +Definition big_endian := false. + +Definition align_int64 := 8%Z. +Definition align_float64 := 8%Z. + +Definition splitlong := false. + +Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. +Proof. + unfold splitlong. congruence. +Qed. + +(** FIXME - Check the properties below *) + +(** Section 7.3: "Except when otherwise stated, if the result of a + floating-point operation is NaN, it is the canonical NaN. The + canonical NaN has a positive sign and all significand bits clear + except the MSB, a.k.a. the quiet bit." + We need to extend the [choose_binop_pl] functions to account for + this case. *) + +Definition default_nan_64 := (false, iter_nat 51 _ xO xH). +Definition default_nan_32 := (false, iter_nat 22 _ xO xH). + +(* Always choose the first NaN argument, if any *) + +Definition choose_nan_64 (l: list (bool * positive)) : bool * positive := + match l with nil => default_nan_64 | n :: _ => n end. + +Definition choose_nan_32 (l: list (bool * positive)) : bool * positive := + match l with nil => default_nan_32 | n :: _ => n end. + +Definition fpu_returns_default_qNaN := false. + +Lemma choose_nan_64_idem: forall n, + choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil). +Proof. auto. Qed. + +Lemma choose_nan_32_idem: forall n, + choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil). +Proof. auto. Qed. + +Definition fma_order {A: Type} (x y z: A) := (x, z, y). + +Definition fma_invalid_mul_is_nan := false. +Definition float_of_single_preserves_sNaN := false. + +Global Opaque ptr64 big_endian splitlong + default_nan_64 choose_nan_64 + default_nan_32 choose_nan_32 + fma_order fma_invalid_mul_is_nan + float_of_single_preserves_sNaN. + +(** Whether to generate position-independent code or not *) + +Parameter pic_code: unit -> bool. + +Definition has_notrap_loads := true. |