aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Trying a inductive predicate for BTL-RTL proofLéo Gourdin2021-05-031-10/+41
* more implem notes in BTLroadmapSylvain Boulmé2021-05-021-1/+8
* BTL roadmapSylvain Boulmé2021-05-021-0/+79
* debroussaillage et precisions...Sylvain Boulmé2021-05-012-23/+73
* BTLtoRTL: proof for internal/external/return statesLéo Gourdin2021-04-302-2/+27
* start the new "BTL" IR.Sylvain Boulmé2021-04-286-2/+735
* 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
generated by cgit (git 2.34.1) at 2024-07-04 09:52:09 +0000