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

	Commit message (Collapse)	Author	Age	Files	Lines
*	For numerical builtins, support return types that are small integer types	Xavier Leroy	2021-09-22	1	-25/+47
\|
*	Use the LGPL instead of the GPL for dual-licensed files	Xavier Leroy	2021-05-08	1	-4/+5
\| \| \| \| \| \|	The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
*	Support __builtin_unreachable	Xavier Leroy	2021-05-02	1	-0/+5
\| \| \| \|	Not yet used for optimizations.
*	Add __builtin_sqrt as synonymous for __builtin_fsqrt	Xavier Leroy	2020-07-27	1	-0/+1
\| \| \| \|	__builtin_sqrt (no "f") is the name used by GCC and Clang.
*	Add support for __builtin_fabsf	Xavier Leroy	2020-07-27	1	-0/+5
\|
*	Refine the type of function results in AST.signature	Xavier Leroy	2020-02-21	1	-32/+32
\| \| \| \| \| \| \| \| \| \|	Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions.
*	bswap builtins: give semantics to them, support bswap64 on all targets	Bernhard Schommer	2019-08-12	1	-1/+23
\| \| \| \| \| \| \| \| \| \| \| \|	* 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.
*	Give formal semantics to some built-in functions and run-time functions	Xavier Leroy	2019-07-17	1	-0/+509
	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.