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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Merge branch 'master' into merge_master_8.13.1	Sylvain Boulmé	2021-03-23	1	-1/+1
\|\ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
\| *	Replace `omega` tactic with `lia`	Xavier Leroy	2020-12-29	1	-1/+1
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
* \|	quick fixcomments	Léo Gourdin	2021-02-16	1	-1/+1
\| \|
* \|	Adding fp stores pair	Léo Gourdin	2021-01-20	1	-3/+4
\| \|
* \|	Adding fp loads pair	Léo Gourdin	2021-01-20	1	-7/+20
\| \|
* \|	Val_cmp* -> Val.mxcmp*	Sylvain Boulmé	2021-01-07	1	-60/+6
\| \|
* \|	Merge branch 'kvx-work' into aarch64-peephole	Sylvain Boulmé	2020-12-17	1	-2/+8
\|\\|
\| *	AArch64 modeling of registers destroyed by pseudo-instructions	Xavier Leroy	2020-12-06	1	-4/+4
\| \| \| \| \| \| \| \| \| \| \| \|	Pfmovimms, Pfmovimmd destroy X16 Pbtbl preserves X17 Inlined built-in functions destroy X16 and X30
\| *	Added implementation for fmin/fmax for aarch64.	Bernhard Schommer	2020-11-06	1	-0/+4
\| \| \| \| \| \| \| \| \| \|	The two built-in function map to the fmax and fmin instruction. Bug 30035
\| *	AArch64 implementation of __builtin_ctz*	Xavier Leroy	2020-07-27	1	-0/+2
\| \| \| \| \| \| \| \|	Using the "rbit" instruction (reverse bits).
* \|	Big improvment in peephole, changing LDP/STP semantics	Léo Gourdin	2020-12-10	1	-20/+20
\| \|
* \|	a first working draft on ldp/stp peephole	Léo Gourdin	2020-12-04	1	-18/+46
\| \|
* \|	Adding semantics for Pldp	Léo Gourdin	2020-12-02	1	-3/+27
\| \| \| \| \| \|	This commit prepare the backend for a peephole optimization in Asmblock.
* \|	Proof of Pfmovimm fine tuned OK, moving float checks in Asm	Léo Gourdin	2020-11-26	1	-3/+41
\| \| \| \| \| \|	Also some simplifications in Asmblockdeps
* \|	fix the semantics ?	Sylvain Boulmé	2020-11-18	1	-2/+2
\| \|
* \|	Preparation for postpass in aarch64 and refactoring	Léo Gourdin	2020-11-02	1	-10/+10
\| \|
* \|	aarch64 compiles again (but ccomp generates incorrect assembly)	Sylvain Boulmé	2020-10-23	1	-9/+530
\| \|
* \|	Prove exec_body_dont_move_PC	Justus Fasse	2020-08-18	1	-4/+4
\| \| \| \| \| \| \| \| \| \| \| \|	Modify Asmblock.preg to combine iregsp and freg into dreg (dreg might be a misnomer since not all iregs are data regs) TODO: Adjust names of PArithP, PArithPP and the like
* \|	Add dynamically checked assumption to simplify Asmgenproof	Justus Fasse	2020-07-21	1	-1/+1
\| \| \| \| \| \| \| \| \| \|	Previously Asmblock.label_pos and Asm.label_pos could point to different memory location for the same label.
* \|	aarch64/Asm: Fix `Error: Pattern "PC" is redundant in this clause.`	Justus Fasse	2020-07-06	1	-1/+1
\| \| \| \| \| \| \| \|	Introduced by changed definition of preg in aarch64/Asmblock
* \|	[WIP: Coq compilation broken] Stub for Asmgen	Sylvain Boulmé	2020-06-21	1	-498/+32
\|/
*	Revert "Remove `__builtin_nop` for some architectures. (#208)"	Bernhard Schommer	2020-01-03	1	-1/+3
\| \| \| \|	This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
*	Remove `__builtin_nop` for some architectures. (#208)	Bernhard Schommer	2019-12-21	1	-3/+1
\| \| \| \| \| \| \|	The `__builtin_nop` function is documented only for PowerPC. It was added to the other architectures by copy paste, but has no known uses. So, remove `__builtin_nop` from all architectures but PowerPC.
*	AArch64 port	Xavier Leroy	2019-08-08	1	-0/+1312
	This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.