aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* Desactivating branch predictions by defaultCyril SIX2020-03-171-7/+11
|
* more inliningDavid Monniaux2020-03-151-3/+6
|
* Fixed stupid typo bug preventing the prediction update for the RANDOM predictorCyril SIX2020-03-111-1/+1
|
* Merge branch 'mppa-work' of ↵David Monniaux2020-03-112-125/+360
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * Linearizeaux: dumb selector when cycling dependencies are foundCyril SIX2020-03-101-4/+6
| |
| * Linearizeaux, forgot to visit the rest of the nodes in dfs_visitCyril SIX2020-03-101-22/+26
| |
| * Some dependencies were not taken into account in tracelinearizeCyril SIX2020-03-101-15/+12
| |
| * Linearize: More helpful message when tracelinearize failsCyril SIX2020-03-101-4/+12
| |
| * Bug fix in ftracelinearizeCyril SIX2020-03-101-4/+15
| |
| * [BROKEN] Replacing the boolean -fduplicate option by an integerCyril SIX2020-03-091-4/+6
| | | | | | | | To control the threshold for duplication
| * Linearizeaux: forgotten printCyril SIX2020-03-091-1/+1
| |
| * Duplicate: getting rid of the annoying exception-based codeCyril SIX2020-03-091-46/+29
| |
| * Removing prints in Duplicateaux.mlCyril SIX2020-03-091-65/+20
| |
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-work-untestedCyril SIX2020-03-0921-180/+315
| |\
| * | Linearizeaux: Fixed bug where the output list was in reverse orderCyril SIX2020-03-091-4/+20
| | |
| * | Adding debug info in LinearizeauxCyril SIX2020-03-061-0/+12
| | |
| * | [UNTESTED] Sequence orderingCyril SIX2020-03-061-3/+27
| | |
| * | Linearize: Dependencies computing to decide which sequence to put firstCyril SIX2020-03-031-31/+132
| | |
| * | Linearizeaux: can_be_mergedCyril SIX2020-02-211-13/+48
| | |
| * | Linearizeaux: function try_mergeCyril SIX2020-02-211-11/+20
| | |
| * | WIP2Cyril SIX2020-02-201-16/+24
| | |
| * | WIPCyril SIX2020-02-201-0/+26
| | |
| * | First part of Hansen algorithm - build the sequencesCyril SIX2020-02-191-1/+43
| | |
* | | remet is_trivial_op dans CSE2David Monniaux2020-03-112-2/+5
| |/ |/|
* | removing some coqc 8.10 warningsSylvain Boulmé2020-03-091-1/+1
| |
* | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-035-784/+213
|\ \ | | | | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2
| * | CSE2 alias analysis for Risc-VDavid Monniaux2020-03-033-30/+2
| | |
| * | moved away x86-dependent partsDavid Monniaux2020-03-031-38/+0
| | |
| * | modularize proofDavid Monniaux2020-03-031-29/+10
| | |
| * | may_overlap_soundDavid Monniaux2020-03-031-0/+38
| | |
| * | starting to move x86 stuff to x86David Monniaux2020-03-031-201/+1
| | |
| * | offsets in globals for x86David Monniaux2020-03-032-2/+82
| | |
| * | globals alias analysis for x86David Monniaux2020-03-032-10/+59
| | |
| * | with indexed/indexed alias analysis for x86David Monniaux2020-03-032-4/+26
| | |
| * | kill_store_soundDavid Monniaux2020-03-021-10/+25
| | |
| * | kill_store1_soundDavid Monniaux2020-03-021-3/+41
| | |
| * | load_store_awayDavid Monniaux2020-03-021-1/+2
| | |
| * | swap predicateDavid Monniaux2020-03-022-13/+27
| | |
| * | works on x86 x86_64David Monniaux2020-03-021-29/+47
| | |
| * | playing with offsetsDavid Monniaux2020-03-021-1/+67
| | |
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2-naiveDavid Monniaux2020-03-0217-96/+174
| |\ \
| | * | Weaker ec_readonly condition over external calls (#225)Xavier Leroy2020-03-021-3/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Currently we require the memory to be unchanged on readonly locations. This is too strong. For example, current permissions could decrease from readonly to none. This commit weakens the ec_readonly condition to the strict minimum needed to show the correctness of value analysis for const globals.
| | * | Define IRC.class_of_type for types Tany32, Tany64Xavier Leroy2020-03-021-1/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Until now the types Tany32 and Tany64 were not used prior to register allocation, so IRC.class_of_type did not need to be defined for those types. However, there are possible uses of stack slots of type Tany32 and Tany64 to specify calling conventions. For this purpose, we need to define class_of_type for Tany32 and Tany64. We follow the informal convention that Tany32 goes in integer registers and Tany64 goes into integer registers if 64-bit wide, or FP registers otherwise.
* | | | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-0368-342/+4246
|\ \ \ \ | | |_|/ | |/| | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-142-4/+55
| |\ \ \
| | * | | Added option -ftracelinearize which linearizes based on ifnot branchesCyril SIX2020-02-122-4/+55
| | | | |
| * | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-061-3/+3
| |\| | |
| | * | | accessors for records are now not extracted it seemsDavid Monniaux2020-02-061-3/+3
| | | | |
| * | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-063-18/+593
| |\| | |
| | * | | Added flag to desactivate condition inversionCyril SIX2020-02-031-1/+2
| | | | |
generated by cgit (git 2.34.1) at 2024-07-12 05:42:30 +0000