aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling
Commit message (Expand)AuthorAgeFilesLines
* Remove flagsLéo Gourdin2021-04-091-3/+1
* Important commit on expansions' mini CSE, and a draft for addptrofsLéo Gourdin2021-04-062-5/+2
* Remove first nop when doing expansionLéo Gourdin2021-03-211-0/+1
* Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexpLéo Gourdin2021-03-062-5/+5
|\
| * Adding a mini CSE pass in the expansion oracleLéo Gourdin2021-03-062-4/+5
* | Adding fp init expansionsLéo Gourdin2021-03-021-3/+3
* | [Admitted checker] Oracle expansion for float/float32 constant initLéo Gourdin2021-03-022-4/+4
|/
* fix ci ?Léo Gourdin2021-03-021-1/+1
* Try to save values in virtual registers during expansionLéo Gourdin2021-03-011-1/+1
* Proofs finished for expansionLéo Gourdin2021-03-011-22/+6
* Debugging fake values finishedLéo Gourdin2021-03-011-10/+19
* proof of fsval_proj_correctSylvain Boulmé2021-03-011-7/+27
* Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-workLéo Gourdin2021-03-011-4/+4
|\
| * bug fix ?Sylvain Boulmé2021-03-011-4/+4
* | Proof of fsval condition cmp okLéo Gourdin2021-03-011-968/+18
* | [Admitted checker] Some more proof, version with buggy addirw0Léo Gourdin2021-02-251-18/+2
* | some more proof for fake hsval checker expansionsLéo Gourdin2021-02-251-324/+1
* | [Intermediate] Adding fake hsval for Ccomp expansionLéo Gourdin2021-02-232-164/+68
* | Fix importsLéo Gourdin2021-02-231-1/+1
* | Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-workLéo Gourdin2021-02-236-79/+202
|\|
| * Merge branch 'riscv-work-rules' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy...Léo Gourdin2021-02-231-2/+52
| |\
| | * add target_cbranch_expanseSylvain Boulmé2021-02-231-2/+52
| * | Separate target_op_simplify for riscVLéo Gourdin2021-02-231-19/+2
| |/
| * fix commentsSylvain Boulmé2021-02-231-2/+5
| * starting an interface for target rewriting rules.Sylvain Boulmé2021-02-231-9/+130
| * improved pre_output_regsSylvain Boulmé2021-02-221-5/+8
| * a bit more cleaningSylvain Boulmé2021-02-225-44/+21
| * quick fixcommentsLéo Gourdin2021-02-161-4/+1
* | others case for ccompimmLéo Gourdin2021-02-231-53/+51
* | Some more proofs on branch expansion, using make_immed32_soundLéo Gourdin2021-02-231-59/+221
* | Branch expansions activated and configured in the checker (but admitted) and ...Léo Gourdin2021-02-191-49/+146
* | Proof of Ocmp expansions without immediate and some drafts in commentLéo Gourdin2021-02-181-46/+471
* | Merge remote-tracking branch 'origin/CompCert_RTLpath_simuX' into riscv-workLéo Gourdin2021-02-169-228/+405
|\|
| * This commit gives a first try to compute pre_output_regs from the livenesss o...Léo Gourdin2021-02-151-10/+19
| * [Broken version] Some TODO eliminatedLéo Gourdin2021-02-153-153/+15
| * [Broken version] Proof of hsistate_simu_spec_correctLéo Gourdin2021-02-151-7/+10
| * [Broken version] Intermediate local commit: pre_output_regs_correct provedLéo Gourdin2021-02-151-17/+28
| * [Broken version] Intermediate local commit: proof of siexec_snone_por in sche...Léo Gourdin2021-02-122-18/+68
| * [Broken version] Intermediate local commit: proof of inst_checker_eqlive OKLéo Gourdin2021-02-122-54/+131
| * progress in pre_output_regs_correctSylvain Boulmé2021-02-121-5/+53
| * improve the skeleton...Sylvain Boulmé2021-02-112-26/+107
| * refactorize inst_checker for checking pre_output_regsSylvain Boulmé2021-02-112-31/+98
| * specification of pre_output_regs for the simulation checkerSylvain Boulmé2021-02-116-125/+107
| * factorize lazy_and_Some_* lemmasSylvain Boulmé2021-02-101-16/+3
* | Adding a compiler option -fexpanse-rtlcondLéo Gourdin2021-02-161-1/+3
* | [Admitted checker] Some more proof draftLéo Gourdin2021-02-111-97/+272
* | [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proofLéo Gourdin2021-02-111-55/+320
* | [Admitted checker] Adding cbranch expansions (without scratch) to the checkerLéo Gourdin2021-02-101-3/+93
* | [Admitted checker] Checker expansion for reg Ocmp (without scratch)Léo Gourdin2021-02-103-26/+267
* | Adding pathmap psize modification during expansion oracleLéo Gourdin2021-02-081-5/+5
generated by cgit (git 2.34.1) at 2024-06-02 17:29:34 +0000