| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
| |
With FP arithmetic, the negation of "x < y" is not "x >= y". For this reason, the back-end intermediate languages of CompCert used to have both "Ccompf c" and "Cnotcompf c" comparison operators, where "c" is of type Integers.comparison and "Cnotcompf c" denotes the negation of FP comparison c.
There are some problems with this approach:
- Beyond Cnotcompf we also need Cnotcompfs (for single precision FP) and, in case of ARM, special forms for not-comparison against 0.0. This duplication of comparison constructors inevitably causes some code and proof duplication.
- Cnotcompf Ceq is really Ccompf Cne, and likewise Cnotcompf Cne is really Ccompf Ceq, hence the representation of FP comparisons is not canonical, adding to the code and proof duplication mentioned above.
- Cnotcompf is introduced in CminorSel, but in Cminor we don't have it, making it impossible to express some transformations over comparisons at the machine-independent Cminor level.
This commit develops an alternate approach, whereas FP comparisons have their own type, defined as Floats.fp_comparison, and which includes constructors for "not <", "not <=", "not >" and "not >=". Hence this type is closed under boolean negation, so to speak, and there is no longer a need for "Cnotcompf", given that "Ccompf" takes a fp_comparison and can therefore express all FP comparisons of interest.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
As written in the comment, ZF should be set if the two floats are
equal or unordered. The "or unordered" case was missing in the
original modeling of FP comparisons.
- Set ZF flag correctly in the Asm.compare_floats and Asm.compare_floats32 functions.
- Update the proofs in Asmgenproof1 accordingly.
No change required to the code generated for FP comparisons: this code
already anticipated the "or unordered" case.
Problem reported by Alix Trieu.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Generate a nop instruction after ais annotations.
In order to prevent the merging of ais annotations with following
Labels a nop instruction is inserted, but only if the annotation
is followed immediately by a label.
The insertion of nop instructions is performed during the
expansion of builtin and pseudo assembler instructions and is
processor independent, by inserting a __builtin_nop built-in.
* Add Pnop instruction to ARM, RISC-V, and x86
ARM as well as RISC-V don't have nop instructions that can
be easily encoded by for example add with zero instructions.
For x86 we used to use `mov X0, X0` for nop but this may
not be as efficient as the true nop instruction.
* Implement __builtin_nop on all supported target architectures.
This builtin is not yet made available on the C side for all architectures.
Bug 24067
|
| |
|
|
|
|
|
|
|
|
| |
The semantics of external function calls in LTL, Linear, Mach and Asm
now consider that all caller-save registers are set to Vundef by the call.
This models that fact that the external function can modify those registers
arbitrarily.
Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes
accordingly.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.
The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.
In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.
|
| |
|
|
| |
Without scopes Coq 8.6 warns, probably rightly so.
|
|
|
-> x86/x86_32/x86_64
Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq.
This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86.
While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures.
Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
|
