From ed0cfe4b38208f15763f2d1c0372c441a320ea56 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 17 Jun 2019 14:22:22 +0200 Subject: Extended asm: print register names according to their types When printing an extended asm code fragment, placeholders %n are replaced by register names. Currently we ignore the fact that some assemblers use different register names depending on the width of the data that resides in the register. For example, x86_64 uses %rax for a 64-bit quantity and %eax for a 32-bit quantity, but CompCert always prints %rax in extended asm statements. This is problematic if we want to use 32-bit integer instructions in extended asm, e.g. int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); produces addl %rax, %rdx which is syntactically incorrect. Another example is ARM FP registers: D0 is a double-precision float, but S0 is a single-precision float. This commit partially solves this issue by taking into account the Cminor type of the asm parameter when printing the corresponding register. Continuing the previous example, int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); now produces addl %eax, %edx This is not perfect yet: we use Cminor types, because this is all we have at hand, and not source C types, hence "char" and "short" parameters are still printed like "int" parameters, which is not good for x86. (I.e. we produce %eax where GCC might have produced %al or %ax.) We'll leave this issue open. --- riscV/TargetPrinter.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'riscV') diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 92df7a76..64bcea4c 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -93,7 +93,7 @@ module Target : TARGET = | X0 -> output_string oc "x0" | X r -> ireg oc r - let preg oc = function + let preg_asm oc ty = function | IR r -> ireg oc r | FR r -> freg oc r | _ -> assert false @@ -582,7 +582,7 @@ module Target : TARGET = (P.to_int kind) (extern_atom txt) args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; - print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res; + print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment | _ -> assert false -- cgit From 83deaa4b3a164423254008d8594de99edc491c3b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 11 Jul 2019 10:56:23 +0200 Subject: Revised specification of NaN payload behavior When an FP arithmetic instruction produces a NaN result, the payload of this NaN depends on the architecture. Before, the payload behavior was specified by 3 architecture-dependent parameters: `Archi.choose_binop_pl_64` and `Archi.choose_binop_pl_32` and `Archi.fpu_results_default_qNaN`. This was adequate for two-argument operations, but doesn't extend to FMA. In preparation for FMA support, this commit generalizes the `Archi.choose` functions from two arguments to any number of arguments. In passing, `Archi.fpu_results_default_qNaN` is no longer needed. --- riscV/Archi.v | 28 +++++++++++++++------------- 1 file changed, 15 insertions(+), 13 deletions(-) (limited to 'riscV') diff --git a/riscV/Archi.v b/riscV/Archi.v index 3758d686..e4078132 100644 --- a/riscV/Archi.v +++ b/riscV/Archi.v @@ -16,7 +16,7 @@ (** Architecture-dependent parameters for RISC-V *) -Require Import ZArith. +Require Import ZArith List. (*From Flocq*) Require Import Binary Bits. @@ -40,26 +40,28 @@ Qed. except the MSB, a.k.a. the quiet bit." Exceptions are operations manipulating signs. *) -Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } := - exist _ (B754_nan 53 1024 false (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true). +Definition default_nan_64 := (false, iter_nat 51 _ xO xH). +Definition default_nan_32 := (false, iter_nat 22 _ xO xH). -Definition choose_binop_pl_64 (pl1 pl2 : positive) := - false. (**r irrelevant *) +Definition choose_nan_64 (l: list (bool * positive)) : bool * positive := + default_nan_64. -Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } := - exist _ (B754_nan 24 128 false (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true). +Definition choose_nan_32 (l: list (bool * positive)) : bool * positive := + default_nan_32. -Definition choose_binop_pl_32 (pl1 pl2 : positive) := - false. (**r irrelevant *) +Lemma choose_nan_64_idem: forall n, + choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil). +Proof. auto. Qed. -Definition fpu_returns_default_qNaN := true. +Lemma choose_nan_32_idem: forall n, + choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil). +Proof. auto. Qed. Definition float_of_single_preserves_sNaN := false. Global Opaque ptr64 big_endian splitlong - default_nan_64 choose_binop_pl_64 - default_nan_32 choose_binop_pl_32 - fpu_returns_default_qNaN + default_nan_64 choose_nan_64 + default_nan_32 choose_nan_32 float_of_single_preserves_sNaN. (** Whether to generate position-independent code or not *) -- cgit From 8b0de52ffa302298abe8d0d6e3b6ed339a2354ba Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 12 Jul 2019 11:42:25 +0200 Subject: Add floating-point square root and fused multiply-add We just lift the corresponding functions from Flocq and add the computation of NaN payloads. NaN payloads for FMA are described in the ARM and RISC-V specifications, and were determined experimentally for x86 and for Power. --- riscV/Archi.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'riscV') diff --git a/riscV/Archi.v b/riscV/Archi.v index e4078132..61d129d0 100644 --- a/riscV/Archi.v +++ b/riscV/Archi.v @@ -57,11 +57,16 @@ 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, y, z). + +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 *) -- cgit From fb20aab431a768299118ed30822af59cab13325e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 2 Jul 2019 14:55:31 +0200 Subject: Remove the cparser/Builtins module Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`. --- riscV/CBuiltins.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'riscV') diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml index 0c981d11..edaf586d 100644 --- a/riscV/CBuiltins.ml +++ b/riscV/CBuiltins.ml @@ -18,10 +18,10 @@ open C let builtins = { - Builtins.typedefs = [ + builtin_typedefs = [ "__builtin_va_list", TPtr(TVoid [], []) ]; - Builtins.functions = [ + builtin_functions = [ (* Synchronization *) "__builtin_fence", (TVoid [], [], false); -- cgit From d08b080747225160b80c3f04bdfd9cd67550b425 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 2 Jul 2019 16:25:40 +0200 Subject: Give formal semantics to some built-in functions and run-time functions This commit adds mechanisms to - recognize certain built-in and run-time functions by name and signature; - associate semantics to these functions, as a partial function from list of values to values; - interpret external calls to these functions according to this semantics (pure function from values to values, memory unchanged, no observable events in the trace); - external calls to unknown built-in and run-time functions remain interpreted as generating observable events and possibly changing memory, like before. The description of the built-ins is split into a target-independent part (in common/Builtins0.v) and a target-specific part (in $ARCH/Builtins1.v). Instruction selection uses the new mechanism in order to - recognize some built-in functions and turn them into operations of the target processor. Currently, this is done for __builtin_sel and __builtin_fabs; more to come. - remove the axioms about int64 helper functions from the standard library. More precisely, the behavior of these functions is still axiomatized, but now it is specified using the more general machinery introduced in this commit, rather than ad-hoc axioms in backend/SplitLongproof. The only built-ins currently described are __builtin_fsqrt (for all platforms) and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be added later. --- riscV/Builtins1.v | 33 +++++++++++++++++++++++++++++++++ riscV/SelectOp.vp | 12 +++++++----- riscV/SelectOpproof.v | 28 ++++++++++++++++------------ 3 files changed, 56 insertions(+), 17 deletions(-) create mode 100644 riscV/Builtins1.v (limited to 'riscV') diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v new file mode 100644 index 00000000..f6e643d2 --- /dev/null +++ b/riscV/Builtins1.v @@ -0,0 +1,33 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, Collège de France and Inria Paris *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Platform-specific built-in functions *) + +Require Import String Coqlib. +Require Import AST Integers Floats Values. +Require Import Builtins0. + +Inductive platform_builtin : Type := . + +Local Open Scope string_scope. + +Definition platform_builtin_table : list (string * platform_builtin) := + nil. + +Definition platform_builtin_sig (b: platform_builtin) : signature := + match b with end. + +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := + match b with end. diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp index 760f06af..99806006 100644 --- a/riscV/SelectOp.vp +++ b/riscV/SelectOp.vp @@ -44,11 +44,8 @@ Require Archi. Require Import Coqlib. Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import CminorSel. +Require Import AST Integers Floats Builtins. +Require Import Op CminorSel. Local Open Scope cminorsel_scope. @@ -454,3 +451,8 @@ Nondetfunction builtin_arg (e: expr) := if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e | _ => BA e end. + +(** Platform-specific known builtins *) + +Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := + None. diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index d0e6979c..18bc5dfe 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -17,18 +17,10 @@ (** Correctness of instruction selection for operators *) -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Zbits. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Cminor. -Require Import Op. -Require Import CminorSel. +Require Import Coqlib Zbits. +Require Import AST Integers Floats. +Require Import Values Memory Builtins Globalenvs. +Require Import Cminor Op CminorSel. Require Import SelectOp. Local Open Scope cminorsel_scope. @@ -937,4 +929,16 @@ Proof. - constructor; auto. Qed. +(** Platform-specific known builtins *) + +Theorem eval_platform_builtin: + forall bf al a vl v le, + platform_builtin bf al = Some a -> + eval_exprlist ge sp e m le al vl -> + platform_builtin_sem bf vl = Some v -> + exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. +Proof. + intros. discriminate. +Qed. + End CMCONSTR. -- cgit From 4c379d48b35e7c8156f3953fede31d5e47faf8ca Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 19 Jul 2019 18:59:44 +0200 Subject: helpers broke compilation --- riscV/SelectOp.vp | 4 +--- riscV/SelectOpproof.v | 5 +---- 2 files changed, 2 insertions(+), 7 deletions(-) (limited to 'riscV') diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp index 23235d95..e9920e46 100644 --- a/riscV/SelectOp.vp +++ b/riscV/SelectOp.vp @@ -452,16 +452,14 @@ Nondetfunction builtin_arg (e: expr) := | _ => BA e end. -<<<<<<< HEAD (* floats *) Definition divf_base (e1: expr) (e2: expr) := Eop Odivf (e1 ::: e2 ::: Enil). Definition divfs_base (e1: expr) (e2: expr) := Eop Odivfs (e1 ::: e2 ::: Enil). -======= + (** Platform-specific known builtins *) Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := None. ->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index ca271342..52a535fb 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -933,8 +933,6 @@ Proof. - constructor; auto. Qed. -<<<<<<< HEAD - (* floating-point division without HELPERS *) Theorem eval_divf_base: forall le a b x y, @@ -955,7 +953,7 @@ Proof. intros; unfold divfs_base. TrivialExists. Qed. -======= + (** Platform-specific known builtins *) Theorem eval_platform_builtin: @@ -968,5 +966,4 @@ Proof. intros. discriminate. Qed. ->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf End CMCONSTR. -- cgit From 040d9c67942c73d875eec9a2ab131fbae6e8f984 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 12 Aug 2019 16:16:10 +0200 Subject: bswap builtins: give semantics to them, support bswap64 on all targets * Added semantic for byte swap builtins The `__builtin_bswap`, `__builtin_bswap16`, `__builtin_bswap32`, `__builtin_bswap64` builtin function are now standard builtin functions with a defined semantics. The semantics is given in terms of the decode/encode functions used for the memory model. * Added bswap64 expansion to PowerPC 32 bits. * Added bswap64 expansion for ARM. --- riscV/CBuiltins.ml | 3 --- 1 file changed, 3 deletions(-) (limited to 'riscV') diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml index edaf586d..a2087cb7 100644 --- a/riscV/CBuiltins.ml +++ b/riscV/CBuiltins.ml @@ -25,9 +25,6 @@ let builtins = { (* Synchronization *) "__builtin_fence", (TVoid [], [], false); - (* Integer arithmetic *) - "__builtin_bswap64", - (TInt(IULongLong, []), [TInt(IULongLong, [])], false); (* Float arithmetic *) "__builtin_fmadd", (TFloat(FDouble, []), -- cgit