diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-07-02 16:25:40 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-07-17 09:17:28 +0200 |
commit | d08b080747225160b80c3f04bdfd9cd67550b425 (patch) | |
tree | 97c1c7c552783fea04ea8a7d1c30d43fa8d2f566 /arm/SelectOp.vp | |
parent | fb20aab431a768299118ed30822af59cab13325e (diff) | |
download | compcert-d08b080747225160b80c3f04bdfd9cd67550b425.tar.gz compcert-d08b080747225160b80c3f04bdfd9cd67550b425.zip |
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.
Diffstat (limited to 'arm/SelectOp.vp')
-rw-r--r-- | arm/SelectOp.vp | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index d04832d6..1220abc4 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -38,11 +38,8 @@ 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. @@ -518,3 +515,8 @@ Nondetfunction builtin_arg (e: expr) := | Eop (Oaddimm n) (e1:::Enil) => BA_addptr (BA e1) (BA_int n) | _ => BA e end. + +(** Platform-specific known builtins *) + +Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := + None. |