compcert-kvx - Unnamed repository; edit this file 'description' to name the repository.

	Commit message (Collapse)	Author	Age	Files	Lines
*	__builtin_expect seems to work	David Monniaux	2020-04-07	1	-2/+3
\|
*	ça recompile sur x86	David Monniaux	2019-03-22	1	-0/+1
\|
*	added helper functions but strange	David Monniaux	2019-03-19	1	-30/+0
\| \| \| \|	idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration
*	Hybrid 64bit/32bit PowerPC port	Bernhard Schommer	2017-05-03	1	-2/+2
\| \| \| \| \| \| \| \| \| \| \| \| \|	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.
*	SplitLong: propagate constants through "longofint"	Xavier Leroy	2016-10-25	1	-2/+5
\| \| \| \| \|	This can make a big difference in which optimizations are triggered later. Constants were already propagated by "longofintu".
*	Update ARM port. Not tested yet.	Xavier Leroy	2016-10-25	1	-3/+3
\|
*	Turn 64-bit integer division and modulus by constants into multiply-high	Xavier Leroy	2016-10-04	1	-1/+8
\| \| \| \| \| \|	This trick was already implemented for 32-bit integer division and modulus. Here we extend it to the 64-bit case. For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned). Tentative implementations are provided for IA32 and PowerPC, but need testing.
*	Improve code generation for 64-bit signed integer division	Xavier Leroy	2016-10-02	1	-32/+11
\| \| \| \| \| \|	Implement the 'shift right extended' trick, both in the generic implementation (backend/SplitLong) and in the IA32 port. Note that now SelectDiv depends on SelectLong, and that some work was moved from SelectLong to SelectDiv.
*	Support for 64-bit architectures: generic support	Xavier Leroy	2016-10-01	1	-0/+352
	- Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.