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 | 7 | -31/+24 |
|\ | |||||
| * | Compatibilité Coq 8.13 | David Monniaux | 2021-04-28 | 3 | -8/+3 |
| | | |||||
| * | Merge remote-tracking branch 'origin/manuscript' into kvx-worksubmission_OOPSLA2021_AARCH64_KVX | Cyril SIX | 2021-04-13 | 1 | -14/+16 |
| |\ | |||||
| | * | Code simplification of get_path_map (no functionality change) | Cyril SIX | 2021-01-26 | 1 | -14/+16 |
| | | | |||||
| * | | Remove flags | Léo Gourdin | 2021-04-09 | 1 | -3/+1 |
| | | | |||||
| * | | Important commit on expansions' mini CSE, and a draft for addptrofs | Léo Gourdin | 2021-04-06 | 2 | -5/+2 |
| | | | |||||
| * | | Remove first nop when doing expansion | Léo Gourdin | 2021-03-21 | 1 | -0/+1 |
| | | | |||||
| * | | Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexp | Léo Gourdin | 2021-03-06 | 2 | -5/+5 |
| |\ \ | |||||
| | * | | Adding a mini CSE pass in the expansion oracle | Léo Gourdin | 2021-03-06 | 2 | -4/+5 |
| | | | | |||||
| * | | | Adding fp init expansions | Léo Gourdin | 2021-03-02 | 1 | -3/+3 |
| | | | | |||||
| * | | | [Admitted checker] Oracle expansion for float/float32 constant init | Léo Gourdin | 2021-03-02 | 2 | -4/+4 |
| |/ / | |||||
* / / | replacing omega with lia in some file | Léo Gourdin | 2021-03-29 | 4 | -39/+43 |
|/ / | |||||
* | | fix ci ? | Léo Gourdin | 2021-03-02 | 1 | -1/+1 |
| | | |||||
* | | Try to save values in virtual registers during expansion | Léo Gourdin | 2021-03-01 | 1 | -1/+1 |
| | | |||||
* | | Proofs finished for expansion | Léo Gourdin | 2021-03-01 | 1 | -22/+6 |
| | | |||||
* | | Debugging fake values finished | Léo Gourdin | 2021-03-01 | 1 | -10/+19 |
| | | |||||
* | | proof of fsval_proj_correct | Sylvain Boulmé | 2021-03-01 | 1 | -7/+27 |
| | | |||||
* | | Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work | Léo Gourdin | 2021-03-01 | 1 | -4/+4 |
|\ \ | |||||
| * | | bug fix ? | Sylvain Boulmé | 2021-03-01 | 1 | -4/+4 |
| | | | |||||
* | | | Proof of fsval condition cmp ok | Léo Gourdin | 2021-03-01 | 1 | -968/+18 |
| | | | |||||
* | | | [Admitted checker] Some more proof, version with buggy addirw0 | Léo Gourdin | 2021-02-25 | 1 | -18/+2 |
| | | | |||||
* | | | some more proof for fake hsval checker expansions | Léo Gourdin | 2021-02-25 | 1 | -324/+1 |
| | | | |||||
* | | | [Intermediate] Adding fake hsval for Ccomp expansion | Léo Gourdin | 2021-02-23 | 2 | -164/+68 |
| | | | |||||
* | | | Fix imports | Léo Gourdin | 2021-02-23 | 1 | -1/+1 |
| | | | |||||
* | | | Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work | Léo Gourdin | 2021-02-23 | 6 | -79/+202 |
|\| | | |||||
| * | | Merge branch 'riscv-work-rules' of ↵ | Léo Gourdin | 2021-02-23 | 1 | -2/+52 |
| |\ \ | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into riscv-work-rules | ||||
| | * | | add target_cbranch_expanse | Sylvain Boulmé | 2021-02-23 | 1 | -2/+52 |
| | | | | |||||
| * | | | Separate target_op_simplify for riscV | Léo Gourdin | 2021-02-23 | 1 | -19/+2 |
| |/ / | |||||
| * | | fix comments | Sylvain Boulmé | 2021-02-23 | 1 | -2/+5 |
| | | | |||||
| * | | starting an interface for target rewriting rules. | Sylvain Boulmé | 2021-02-23 | 1 | -9/+130 |
| | | | |||||
| * | | improved pre_output_regs | Sylvain Boulmé | 2021-02-22 | 1 | -5/+8 |
| | | | |||||
| * | | a bit more cleaning | Sylvain Boulmé | 2021-02-22 | 5 | -44/+21 |
| | | | |||||
| * | | quick fixcomments | Léo Gourdin | 2021-02-16 | 1 | -4/+1 |
| | | | |||||
* | | | others case for ccompimm | Léo Gourdin | 2021-02-23 | 1 | -53/+51 |
| | | | |||||
* | | | Some more proofs on branch expansion, using make_immed32_sound | Léo Gourdin | 2021-02-23 | 1 | -59/+221 |
| | | | |||||
* | | | Branch expansions activated and configured in the checker (but admitted) and ↵ | Léo Gourdin | 2021-02-19 | 1 | -49/+146 |
| | | | | | | | | | | | | bugfix in the expansion liveness modification | ||||
* | | | Proof of Ocmp expansions without immediate and some drafts in comment | Léo Gourdin | 2021-02-18 | 1 | -46/+471 |
| | | | |||||
* | | | Merge remote-tracking branch 'origin/CompCert_RTLpath_simuX' into riscv-work | Léo Gourdin | 2021-02-16 | 9 | -228/+405 |
|\| | | |||||
| * | | This commit gives a first try to compute pre_output_regs from the livenesss ↵ | Léo Gourdin | 2021-02-15 | 1 | -10/+19 |
| | | | | | | | | | | | | oracle | ||||
| * | | [Broken version] Some TODO eliminated | Léo Gourdin | 2021-02-15 | 3 | -153/+15 |
| | | | |||||
| * | | [Broken version] Proof of hsistate_simu_spec_correct | Léo Gourdin | 2021-02-15 | 1 | -7/+10 |
| | | | |||||
| * | | [Broken version] Intermediate local commit: pre_output_regs_correct proved | Léo Gourdin | 2021-02-15 | 1 | -17/+28 |
| | | | |||||
| * | | [Broken version] Intermediate local commit: proof of siexec_snone_por in ↵ | Léo Gourdin | 2021-02-12 | 2 | -18/+68 |
| | | | | | | | | | | | | scheduler proof | ||||
| * | | [Broken version] Intermediate local commit: proof of inst_checker_eqlive OK | Léo Gourdin | 2021-02-12 | 2 | -54/+131 |
| | | | |||||
| * | | progress in pre_output_regs_correct | Sylvain Boulmé | 2021-02-12 | 1 | -5/+53 |
| | | | |||||
| * | | improve the skeleton... | Sylvain Boulmé | 2021-02-11 | 2 | -26/+107 |
| | | | |||||
| * | | refactorize inst_checker for checking pre_output_regs | Sylvain Boulmé | 2021-02-11 | 2 | -31/+98 |
| | | | |||||
| * | | specification of pre_output_regs for the simulation checker | Sylvain Boulmé | 2021-02-11 | 6 | -125/+107 |
| | | | |||||
| * | | factorize lazy_and_Some_* lemmas | Sylvain Boulmé | 2021-02-10 | 1 | -16/+3 |
| | | | |||||
* | | | Adding a compiler option -fexpanse-rtlcond | Léo Gourdin | 2021-02-16 | 1 | -1/+3 |
| | | |