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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Adding fp stores pair	Léo Gourdin	2021-01-20	1	-6/+12
\|
*	Adding fp loads pair	Léo Gourdin	2021-01-20	1	-13/+30
\|
*	Val_cmp* -> Val.mxcmp*	Sylvain Boulmé	2021-01-07	1	-6/+6
\|
*	Fix the Asmblock/Asm proof	Léo Gourdin	2020-12-20	1	-7/+7
\|
*	Merge branch 'kvx-work' into aarch64-peephole	Sylvain Boulmé	2020-12-17	1	-1/+3
\|
*	Big improvment in peephole, changing LDP/STP semantics	Léo Gourdin	2020-12-10	1	-92/+110
\|
*	Asmgen proof completely proved with ldp/stp	Léo Gourdin	2020-12-06	1	-2/+3
\|
*	a first working draft on ldp/stp peephole	Léo Gourdin	2020-12-04	1	-52/+227
\|
*	Adding semantics for Pldp	Léo Gourdin	2020-12-02	1	-33/+38
\| \| \|	This commit prepare the backend for a peephole optimization in Asmblock.
*	Some optimizations again	Léo Gourdin	2020-11-28	1	-27/+30
\|
*	Optimizing Asmblockdeps proof	Léo Gourdin	2020-11-28	1	-58/+92
\| \| \|	Proof is now two times faster (from 60 to 30 seconds)
*	Proof of Pfmovimm fine tuned OK, moving float checks in Asm	Léo Gourdin	2020-11-26	1	-240/+96
\| \| \|	Also some simplifications in Asmblockdeps
*	Fine tuning for Pfmovimm	Léo Gourdin	2020-11-26	1	-3/+5
\| \| \| \|	- Functions to check a float logical immediate were translated from ocaml target printer in coq Asmblock - Some proof are admitted for now (we'll see if it is a good idea after some tests)
*	Main part of postpasssch proof now completed	Léo Gourdin	2020-11-24	1	-1/+1
\|
*	Asmblockdeps is now finished	Léo Gourdin	2020-11-24	1	-226/+42
\|
*	Start of the postpasschedproof, redefining verify schedule lemmas	Léo Gourdin	2020-11-23	1	-36/+42
\|
*	a step forward in bblock_simu_reduce	Sylvain Boulmé	2020-11-23	1	-40/+34
\|
*	Trying to finish the bisimu reduce proof for builtin (last case admitted)	Léo Gourdin	2020-11-20	1	-29/+76
\|
*	draft of the exec_bblock Asmblockdeps proof	Léo Gourdin	2020-11-20	1	-29/+116
\|
*	Postpass scheduling OK	Léo Gourdin	2020-11-18	1	-164/+29
\| \| \| \| \| \|	- Modifying Asmblockdeps to adapt to Pfmovimm new specification - Changing the Asmgenproof to adapt PArith in consequence - Modifying the oracle to specify correct wlocs - Cleaning everywhere
*	Merge remote-tracking branch 'origin/aarch64-postpass' into aarch64-postpass	Léo Gourdin	2020-11-17	1	-7/+56
\|\
\| *	extend the aarch64 scheduling verifier to check builtins.	Sylvain Boulmé	2020-11-17	1	-7/+56
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	NB 1: the equality is purely syntactical on builtins. This should not be a limit for our scheduler. NB 2: the correctness proof remains to be done (only a skeleton is given).
* \|	Builtin mem spec in scheduler and some needed proof in Postpasssch.v	Léo Gourdin	2020-11-17	1	-2/+2
\|/
*	Remaining ctl insts except Pbuiltin (maps to error)	Léo Gourdin	2020-11-16	1	-369/+493
\|
*	Lemma for bisimu with potential builtins, alloc and constant	Léo Gourdin	2020-11-13	1	-65/+132
\|
*	Loads and stores op	Léo Gourdin	2020-11-13	1	-5/+203
\|
*	Arith inst OK for the verifier	Léo Gourdin	2020-11-12	1	-61/+191
\|
*	Finishing PArith cases in abb, and linking the pass to compile	Léo Gourdin	2020-11-11	1	-387/+479
\|
*	PArithCmpR0R in checker	Léo Gourdin	2020-11-11	1	-36/+130
\|
*	PArithComparison special lemmas and adaptations	Léo Gourdin	2020-11-10	1	-17/+315
\|
*	Simplifications using ltacs and XZR special case	Léo Gourdin	2020-11-10	1	-33/+150
\|
*	First version of the oracle checker, does not compile yet	Léo Gourdin	2020-11-09	1	-832/+576
\|
*	Preparation for postpass in aarch64 and refactoring	Léo Gourdin	2020-11-02	1	-0/+1841