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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1	Cyril SIX	2021-06-01	1	-84/+113
\|\
\| *	Removing addptrofs draft, next will be merging	Léo Gourdin	2021-04-09	1	-51/+47
\| \|
\| *	Important commit on expansions' mini CSE, and a draft for addptrofs	Léo Gourdin	2021-04-06	1	-65/+68
\| \|
\| *	a more general way to manage special registers before introducing SP	Léo Gourdin	2021-03-30	1	-49/+49
\| \|
\| *	Now a more general way to perform imm operations	Léo Gourdin	2021-03-30	1	-13/+18
\| \|
\| *	Refactoring the mayundef OP to be more general...	Léo Gourdin	2021-03-30	1	-44/+23
\| \|
\| *	Adding more expansions, improving miniCSE, and tuning prepass	Léo Gourdin	2021-03-26	1	-9/+56
\| \|
\| *	Adding a mini CSE pass in the expansion oracle	Léo Gourdin	2021-03-06	1	-21/+20
\| \|
* \|	replacing omega with lia in some file	Léo Gourdin	2021-03-29	1	-2/+2
\|/
*	Merge remote-tracking branch 'origin/riscV-cmov' into riscv-work	Léo Gourdin	2021-03-02	1	-0/+107
\|\
\| *	begin implementing select	David Monniaux	2021-02-02	1	-2/+55
\| \|
\| *	bits to float	David Monniaux	2021-02-01	1	-1/+27
\| \|
\| *	Obits_of_single etc	David Monniaux	2021-02-01	1	-0/+28
\| \|
* \|	Proof of fsval condition cmp ok	Léo Gourdin	2021-03-01	1	-4/+29
\| \|
* \|	[Admitted checker] Duplicating Asm Ceq/Cne and draft checker proof	Léo Gourdin	2021-02-11	1	-21/+29
\| \|
* \|	cond and branches expanded	Léo Gourdin	2021-02-06	1	-1/+15
\| \|
* \|	All Ocmp expanded in RTL	Léo Gourdin	2021-02-03	1	-0/+7
\| \|
* \|	Ccomp for long	Léo Gourdin	2021-02-03	1	-0/+57
\| \|
* \|	Ccompu expansion	Léo Gourdin	2021-02-02	1	-2/+5
\| \|
* \|	Expansion of Ccompimm in RTL [Admitted checker]	Léo Gourdin	2021-02-02	1	-0/+44
\|/
*	risc-V now without trapping instructions	David Monniaux	2020-09-21	1	-8/+8
\|
*	moved Risc-V div ValueAOp to central location	David Monniaux	2020-09-21	1	-293/+0
\|
*	maketotal mod & div	David Monniaux	2020-09-21	1	-8/+302
\|
*	RISC-V port and assorted changes	Xavier Leroy	2017-04-28	1	-0/+218
	This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes. The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/ This port required the following additional changes: - Integers: More properties about shrx - SelectOp: now provides smart constructors for mulhs and mulhu - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu. - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library. - test/: add SIMU make variable to run tests through a simulator - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers commit da14495c01cf4f66a928c2feff5c53f09bde837f Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Thu Apr 13 17:36:10 2017 +0200 RISC-V port, continued Now working on Asmgen. commit 36f36eb3a5abfbb8805960443d087b6a83e86005 Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Wed Apr 12 17:26:39 2017 +0200 RISC-V port, first steps This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.