aboutsummaryrefslogtreecommitdiffstats
path: root/backend/CSE2.v
Commit message (Collapse)AuthorAgeFilesLines
* Adding copyrightsCyril SIX2020-05-041-0/+12
|
* Merge remote-tracking branch 'origin/mppa-cse2' into mppa-cse3David Monniaux2020-04-201-3/+3
|\
| * forward moves into store sourceDavid Monniaux2020-04-201-3/+3
| |
* | CSE3: better builtin handlingDavid Monniaux2020-04-161-1/+1
| |
* | Merge remote-tracking branch 'origin/mppa-cse2' into mppa-cse3David Monniaux2020-04-161-26/+22
|\|
| * refine the rules for builtinsDavid Monniaux2020-04-161-1/+18
| |
| * progress on CSE2 builtinsDavid Monniaux2020-04-161-26/+5
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-04-081-3/+3
|\|
| * Adding info field for branching in RTL, LTL, XTL and all associated passesCyril SIX2020-03-111-3/+3
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-111-1/+1
|\|
| * remet is_trivial_op dans CSE2David Monniaux2020-03-111-1/+1
| |
* | streamlined lattice codeDavid Monniaux2020-03-051-114/+1
|/
* fixed CSE2 for mppa_k1cDavid Monniaux2020-03-031-107/+51
|\ | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2
| * CSE2 alias analysis for Risc-VDavid Monniaux2020-03-031-24/+1
| |
| * offsets in globals for x86David Monniaux2020-03-031-1/+4
| |
| * globals alias analysis for x86David Monniaux2020-03-031-0/+2
| |
| * with indexed/indexed alias analysis for x86David Monniaux2020-03-031-2/+24
| |
| * swap predicateDavid Monniaux2020-03-021-0/+8
| |
* | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-031-3/+3
|\ \ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | CSE2 with NOTRAPDavid Monniaux2020-02-031-4/+2
| | |
| * | NOTRAP in CSE2: progressDavid Monniaux2020-02-031-2/+1
| | |
| * | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert/dm-cse2 into mppa-cse2David Monniaux2020-02-031-0/+6
| |\|
| * | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2David Monniaux2020-01-281-3/+6
| | |
* | | CSE2 now uses is_trivial_opDavid Monniaux2020-02-271-1/+1
| | |
* | | progress on wellformed regDavid Monniaux2020-02-051-12/+52
| | |
* | | kill memory focusedDavid Monniaux2020-02-041-1/+1
| | |
* | | invariant guaranteedDavid Monniaux2020-02-041-1/+3
| | |
* | | wellformedness for memoryDavid Monniaux2020-02-041-4/+6
| | |
* | | begin well formednessDavid Monniaux2020-02-041-15/+32
| | |
* | | stuff information into a recordDavid Monniaux2020-02-041-26/+33
| |/ |/|
* | commentsDavid Monniaux2020-02-031-0/+6
|/
* with loads too ?David Monniaux2020-01-281-2/+52
|
* begin adding loadsDavid Monniaux2020-01-281-2/+7
|
* much better - seems to eliminate CSE not containing loadsDavid Monniaux2020-01-281-1/+1
|
* still buggyDavid Monniaux2020-01-281-20/+28
|
* CSE2 now works for expressionsDavid Monniaux2020-01-281-8/+3
|
* CSE2 split in two filesDavid Monniaux2020-01-281-827/+2
|
* progressDavid Monniaux2020-01-271-0/+467
|
* use in transformationDavid Monniaux2020-01-271-3/+21
|
* find_op_soundDavid Monniaux2020-01-271-1/+110
|
* goes to the end but does not find available opsDavid Monniaux2020-01-271-13/+5
|
* simpler definitionsDavid Monniaux2020-01-271-41/+24
|
* static analysis doneDavid Monniaux2020-01-271-20/+7
|
* kill_mem_soundDavid Monniaux2020-01-271-8/+59
|
* renamed kill_reg into kill_memDavid Monniaux2020-01-271-11/+11
|
* gen_oper_soundDavid Monniaux2020-01-271-1/+37
|
* oper_soundDavid Monniaux2020-01-271-0/+27
|
* oper1_soundDavid Monniaux2020-01-271-1/+10
|
* arg replaceDavid Monniaux2020-01-271-1/+87
|
* move soundDavid Monniaux2020-01-271-19/+85
|
generated by cgit (git 2.34.1) at 2024-05-20 08:22:27 +0000