Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Desactivating branch predictions by default | Cyril SIX | 2020-03-17 | 1 | -7/+11 |
| | |||||
* | more inlining | David Monniaux | 2020-03-15 | 1 | -3/+6 |
| | |||||
* | Fixed stupid typo bug preventing the prediction update for the RANDOM predictor | Cyril SIX | 2020-03-11 | 1 | -1/+1 |
| | |||||
* | Merge branch 'mppa-work' of ↵ | David Monniaux | 2020-03-11 | 2 | -125/+360 |
|\ | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work | ||||
| * | Linearizeaux: dumb selector when cycling dependencies are found | Cyril SIX | 2020-03-10 | 1 | -4/+6 |
| | | |||||
| * | Linearizeaux, forgot to visit the rest of the nodes in dfs_visit | Cyril SIX | 2020-03-10 | 1 | -22/+26 |
| | | |||||
| * | Some dependencies were not taken into account in tracelinearize | Cyril SIX | 2020-03-10 | 1 | -15/+12 |
| | | |||||
| * | Linearize: More helpful message when tracelinearize fails | Cyril SIX | 2020-03-10 | 1 | -4/+12 |
| | | |||||
| * | Bug fix in ftracelinearize | Cyril SIX | 2020-03-10 | 1 | -4/+15 |
| | | |||||
| * | [BROKEN] Replacing the boolean -fduplicate option by an integer | Cyril SIX | 2020-03-09 | 1 | -4/+6 |
| | | | | | | | | To control the threshold for duplication | ||||
| * | Linearizeaux: forgotten print | Cyril SIX | 2020-03-09 | 1 | -1/+1 |
| | | |||||
| * | Duplicate: getting rid of the annoying exception-based code | Cyril SIX | 2020-03-09 | 1 | -46/+29 |
| | | |||||
| * | Removing prints in Duplicateaux.ml | Cyril SIX | 2020-03-09 | 1 | -65/+20 |
| | | |||||
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-untested | Cyril SIX | 2020-03-09 | 21 | -180/+315 |
| |\ | |||||
| * | | Linearizeaux: Fixed bug where the output list was in reverse order | Cyril SIX | 2020-03-09 | 1 | -4/+20 |
| | | | |||||
| * | | Adding debug info in Linearizeaux | Cyril SIX | 2020-03-06 | 1 | -0/+12 |
| | | | |||||
| * | | [UNTESTED] Sequence ordering | Cyril SIX | 2020-03-06 | 1 | -3/+27 |
| | | | |||||
| * | | Linearize: Dependencies computing to decide which sequence to put first | Cyril SIX | 2020-03-03 | 1 | -31/+132 |
| | | | |||||
| * | | Linearizeaux: can_be_merged | Cyril SIX | 2020-02-21 | 1 | -13/+48 |
| | | | |||||
| * | | Linearizeaux: function try_merge | Cyril SIX | 2020-02-21 | 1 | -11/+20 |
| | | | |||||
| * | | WIP2 | Cyril SIX | 2020-02-20 | 1 | -16/+24 |
| | | | |||||
| * | | WIP | Cyril SIX | 2020-02-20 | 1 | -0/+26 |
| | | | |||||
| * | | First part of Hansen algorithm - build the sequences | Cyril SIX | 2020-02-19 | 1 | -1/+43 |
| | | | |||||
* | | | remet is_trivial_op dans CSE2 | David Monniaux | 2020-03-11 | 2 | -2/+5 |
| |/ |/| | |||||
* | | removing some coqc 8.10 warnings | Sylvain Boulmé | 2020-03-09 | 1 | -1/+1 |
| | | |||||
* | | fixed CSE2 for mppa_k1c | David Monniaux | 2020-03-03 | 5 | -784/+213 |
|\ \ | | | | | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2 | ||||
| * | | CSE2 alias analysis for Risc-V | David Monniaux | 2020-03-03 | 3 | -30/+2 |
| | | | |||||
| * | | moved away x86-dependent parts | David Monniaux | 2020-03-03 | 1 | -38/+0 |
| | | | |||||
| * | | modularize proof | David Monniaux | 2020-03-03 | 1 | -29/+10 |
| | | | |||||
| * | | may_overlap_sound | David Monniaux | 2020-03-03 | 1 | -0/+38 |
| | | | |||||
| * | | starting to move x86 stuff to x86 | David Monniaux | 2020-03-03 | 1 | -201/+1 |
| | | | |||||
| * | | offsets in globals for x86 | David Monniaux | 2020-03-03 | 2 | -2/+82 |
| | | | |||||
| * | | globals alias analysis for x86 | David Monniaux | 2020-03-03 | 2 | -10/+59 |
| | | | |||||
| * | | with indexed/indexed alias analysis for x86 | David Monniaux | 2020-03-03 | 2 | -4/+26 |
| | | | |||||
| * | | kill_store_sound | David Monniaux | 2020-03-02 | 1 | -10/+25 |
| | | | |||||
| * | | kill_store1_sound | David Monniaux | 2020-03-02 | 1 | -3/+41 |
| | | | |||||
| * | | load_store_away | David Monniaux | 2020-03-02 | 1 | -1/+2 |
| | | | |||||
| * | | swap predicate | David Monniaux | 2020-03-02 | 2 | -13/+27 |
| | | | |||||
| * | | works on x86 x86_64 | David Monniaux | 2020-03-02 | 1 | -29/+47 |
| | | | |||||
| * | | playing with offsets | David Monniaux | 2020-03-02 | 1 | -1/+67 |
| | | | |||||
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2-naive | David Monniaux | 2020-03-02 | 17 | -96/+174 |
| |\ \ | |||||
| | * | | Weaker ec_readonly condition over external calls (#225) | Xavier Leroy | 2020-03-02 | 1 | -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, Tany64 | Xavier Leroy | 2020-03-02 | 1 | -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 Monniaux | 2020-03-03 | 68 | -342/+4246 |
|\ \ \ \ | | |_|/ | |/| | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work | ||||
| * | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-02-14 | 2 | -4/+55 |
| |\ \ \ | |||||
| | * | | | Added option -ftracelinearize which linearizes based on ifnot branches | Cyril SIX | 2020-02-12 | 2 | -4/+55 |
| | | | | | |||||
| * | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-02-06 | 1 | -3/+3 |
| |\| | | | |||||
| | * | | | accessors for records are now not extracted it seems | David Monniaux | 2020-02-06 | 1 | -3/+3 |
| | | | | | |||||
| * | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-02-06 | 3 | -18/+593 |
| |\| | | | |||||
| | * | | | Added flag to desactivate condition inversion | Cyril SIX | 2020-02-03 | 1 | -1/+2 |
| | | | | |