aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * | | | dockerfilesDavid Monniaux2021-05-102-8/+9
| * | | | dockerfile for buildingDavid Monniaux2021-05-101-0/+8
| * | | | Increasing required OCaml version (Pervasives <-> Stdlib module renaming)Cyril SIX2021-05-041-2/+2
| * | | | for OCaml 4.13David Monniaux2021-04-301-1/+1
| * | | | Compatibilité Coq 8.13David Monniaux2021-04-285-8/+3
| * | | | add auxfileDavid Monniaux2021-04-271-0/+17
| * | | | Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...Léo Gourdin2021-04-2218-566/+370
| |\ \ \ \
| | * | | | fix broken link in index-kvx.htmlSylvain Boulmé2021-04-161-1/+1
| | | |_|/ | | |/| |
| | * | | Merge remote-tracking branch 'origin/manuscript' into kvx-worksubmission_OOPSLA2021_AARCH64_KVXCyril SIX2021-04-135-525/+173
| | |\ \ \
| | | * | | CleaningCyril SIX2021-04-021-2/+1
| | | * | | More efficientCyril SIX2021-04-021-8/+12
| | | * | | Outermost loop detection worksCyril SIX2021-04-021-9/+10
| | | * | | Getting all loop bodiesCyril SIX2021-04-022-2/+50
| | | * | | get_loop_headers simplification (using the new get_loop_backedges)Cyril SIX2021-04-021-39/+7
| | | * | | Simple backedge detection (modified code from get_loop_headers)Cyril SIX2021-04-023-0/+57
| | | * | | Big simplification of get_loop_infoCyril SIX2021-03-311-111/+16
| | | * | | Simplification of the Linearize heuristic (same result functionally)Cyril SIX2021-03-301-216/+6
| | | * | | Simplifications on Linearize - details belowCyril SIX2021-03-291-205/+79
| | | * | | Code simplification of get_path_map (no functionality change)Cyril SIX2021-01-261-14/+16
| | * | | | Adding more precise heuristic measuresCyril SIX2021-04-131-2/+62
| | * | | | Adding overpredictsCyril SIX2021-04-131-3/+6
| | * | | | Recording of prediction stats with COMPCERT_PROFILING_STATS environment flagCyril SIX2021-04-131-33/+93
| | * | | | Adding distinction between kvx-cos and kvx-mbr (for trapping loads)Cyril SIX2021-04-137-4/+22
| | * | | | rm spurious filesDavid Monniaux2021-04-1239-1705/+0
| | * | | | test profilingDavid Monniaux2021-04-1242-0/+1720
| | * | | | collision of registersDavid Monniaux2021-04-122-3/+3
| * | | | | moving my testsLéo Gourdin2021-04-2226-157/+0
| |/ / / /
| * | | | removing unusued proof lineLéo Gourdin2021-04-091-1/+0
| * | | | adding missing xorimm expLéo Gourdin2021-04-092-0/+77
| * | | | Merge branch 'riscv-work' into kvx-workLéo Gourdin2021-04-0921-1514/+2642
| |\ \ \ \
| | * | | | Remove flagsLéo Gourdin2021-04-094-10/+3
| | * | | | Removing expansions from AsmgenLéo Gourdin2021-04-096-1401/+49
| | | |/ / | | |/| |
| | * | | Removing addptrofs draft, next will be mergingLéo Gourdin2021-04-099-254/+104
| | * | | bugfixLéo Gourdin2021-04-082-2/+3
| | * | | Important commit on expansions' mini CSE, and a draft for addptrofsLéo Gourdin2021-04-0613-762/+1081
| | * | | a more general way to manage special registers before introducing SPLéo Gourdin2021-03-308-560/+593
| | * | | Now a more general way to perform imm operationsLéo Gourdin2021-03-309-38/+68
| | * | | Refactoring the mayundef OP to be more general...Léo Gourdin2021-03-305-201/+191
| | * | | bugfix and printOpLéo Gourdin2021-03-262-19/+29
| | * | | fix admitLéo Gourdin2021-03-261-2/+1
| | * | | Compiler options to manage expansionsLéo Gourdin2021-03-263-179/+176
| | * | | Adding more expansions, improving miniCSE, and tuning prepassLéo Gourdin2021-03-269-388/+1518
| | * | | Bugfix livenessLéo Gourdin2021-03-231-12/+8
| | * | | Remove first nop when doing expansionLéo Gourdin2021-03-212-188/+213
| | * | | fp testLéo Gourdin2021-03-101-0/+7
| | * | | Adding miniCSE here tooLéo Gourdin2021-03-081-10/+10
| | * | | Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexpLéo Gourdin2021-03-0610-187/+250
| | |\ \ \
| | | * | | some simplification in miniCSELéo Gourdin2021-03-061-17/+14
| | | * | | Adding a mini CSE pass in the expansion oracleLéo Gourdin2021-03-0610-197/+268
| | * | | | Adding a flag to test fp_init_expLéo Gourdin2021-03-023-150/+159