aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
Commit message (Collapse)AuthorAgeFilesLines
* Make prepass scheduling sensitive to register pressure, by Nicolas Nardino.David Monniaux2021-07-161-5/+9
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Squashed commit of the following: commit cf033ec29391d5358dea1d3b25da1738957478c4 Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 18:01:03 2021 +0200 comment for authors commit 2ff766a18432fd75739abab0b5741ded6b67a2a5 Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 15:29:25 2021 +0200 activate register pressure by default commit 67f4ae2b702cc95ed7cef67b726e15abbf18e768 Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 15:26:03 2021 +0200 use a more recognizable option name commit 6121be54b80a55fdadd8b64dfad53357148c9090 Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 14:13:50 2021 +0200 fix for KVX commit 43d4932e8ba9e00eb8c8788c86f56b6bddd46392 Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 13:28:26 2021 +0200 setup registers commit 169a221104c37737f12abe79711009fc0d88ce09 Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 13:00:56 2021 +0200 rm useless code commit d6a846b641787ea6a5ed113b1d7275ffb5028d9c Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 12:54:19 2021 +0200 rm "Admitted" commit fd4d085aa988a6044f89fc17e8422be23bc87f9d Merge: 70f5867e 56498b64 Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 12:30:25 2021 +0200 Merge remote-tracking branch 'origin/kvx-work' into kvx-sched-w-reg-press commit 70f5867e441e253869cb3b432af77636a186d1cb Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 12:26:27 2021 +0200 rm TODO commit f86f5df47b69053702661671340b0fcb31506aa3 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Thu Jul 8 11:22:17 2021 +0200 add more debug info commit a4a0b36f56a94c19da301265a4e3acad1fbdf6c4 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Thu Jul 8 11:20:49 2021 +0200 Deactivate sched validator (i think) commit af97fca0f1d824f3becf9c6895f44ad234e262f8 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jul 6 15:32:35 2021 +0200 Add debug info commit b96a48de58e1969535865b7b345514a24f7178a6 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Mon Jun 28 16:04:44 2021 +0200 Change temporary solution (see prev commits), and add option for it commit 9ac49c465f9c8969fba00e6242da0c188a6a3080 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Fri Jun 25 09:42:41 2021 +0200 Changed printfs into debugs commit dfa09586ae40c70769eeda688a0e7f59f611749f Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Thu Jun 24 18:33:20 2021 +0200 Another scheduler commit c5e8595480604c78260017cc771b0e4195fdd182 Merge: 10cbe4b2 cf2aa686 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jun 22 15:58:10 2021 +0200 Merge branch 'kvx-sched-w-reg-press' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-sched-w-reg-press commit 10cbe4b28ef6dc5d02c9a5d4d369484e4943a18d Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jun 22 15:57:21 2021 +0200 Changed default threshold value following tests commit cf2aa686bcf9a823562fe977df6dd778d5467985 Merge: eddbce33 fe557bf6 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Thu Jun 17 17:05:30 2021 +0200 Merge branch 'kvx-sched-w-reg-press' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-sched-w-reg-press commit eddbce33e28c49bf7b9e83ebd5dbf6cb0d770090 Merge: 8f399dfa fae8d9b5 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Thu Jun 17 17:05:20 2021 +0200 Merge branch 'kvx-sched-w-reg-press' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-sched-w-reg-press commit 8f399dfa9d794f2f728f523ff1aa7788cc3599b2 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Thu Jun 17 17:04:52 2021 +0200 fix for Risc-V commit fe557bf65ec738eaa078bc5e398ff690eb1f2b9e Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Thu Jun 17 17:03:53 2021 +0200 changed type of schedule_seq in x86 for compatibility commit fae8d9b5c5f93d5eda36f800eb0ca1837b237cba Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Thu Jun 17 17:00:57 2021 +0200 fix riscv/Machregsaux.mli commit 9759e94256fd09f4995418b67b7aedbcf84b4b10 Merge: 4413c27d 04b2489d Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Thu Jun 17 16:52:09 2021 +0200 Merge remote-tracking branch 'origin/kvx-work' into kvx-sched-w-reg-press commit 4413c27d6c6a3d69df34955d9d453c38b32174c7 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Thu Jun 17 15:38:13 2021 +0200 Add option to set thresold and support for riscv commit 21278bd87e89210bcc287116f6e35fc1b52d0df2 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Wed Jun 16 20:27:31 2021 +0200 Now working, tests show a decrease in spillage Should still find a proper way to treat the case mentioned in earlier commits commit 87c82b6fcf2bf825a8c60fc6a95498aac9f826d4 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jun 15 14:44:56 2021 +0200 kinda fixed Spills are definitely reduced, but lots of arbitrary in there: See previous commit: need to determine what to do if pressure is too high but no schedulable instruction can reduce it. For now, advance time for at most 5 cycles, if still no suitable instruction, go back to CSP commit 19464b3992eadf7670acc7231896103ab54885e5 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jun 15 12:07:43 2021 +0200 fixing Still need to find what to do when pressure is high but there are no instructions available that decrease it commit bff4e6ff0b782619b6fcc18751fa575cbb11de68 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Mon Jun 14 17:39:58 2021 +0200 was very wrong, fixing commit 3eb3751f84348a20b7ce211fdbf1d01a9c4685a8 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Mon Jun 14 14:46:01 2021 +0200 One fewer spill with new sched on `test/.../spille_forw.c` commit 66e15205c40de54639387a4c9b1cc78994525d55 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Mon Jun 14 13:53:08 2021 +0200 scheduler written, need to test now commit 2b814b1f9bb30d9c8b59a713f69bced808bca7c7 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Sat Jun 12 10:52:59 2021 +0200 work on the scheduler commit 1701e43316ee8e69e794a025a8c9979af6bb8c93 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Thu Jun 10 16:31:51 2021 +0200 Work on new schedluer Renamed a test file, wrote function to compute pressure deltas, Still need to pass the info in some way; beginning of the actual scheduler function commit 386b9053177bb4ef2801cec00b717c400a828139 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jun 8 16:53:19 2021 +0200 Fix RTLpathScheduleraux.get_live_regs_entry commit 9b6247b7996f3e0181d27ec0e20daffd28e0884f Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jun 8 16:06:36 2021 +0200 Another test : one spill when scheduled forward, none if not commit 52378f0600652a94edcc8c78e4b426243f717a89 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jun 8 15:11:03 2021 +0200 Add some tests commit 2249f3c7771c285ccd25f6e94478be388a741da5 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Sun Jun 6 20:49:34 2021 +0200 Adding debug info commit 9118878bd14e24cc04c2f36cab7aa7271a0f1852 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Sun Jun 6 12:11:15 2021 +0200 Fixing scope error, and non-exhaustive pattern matching commit 599823a6410f1629f2b8704291839e0974bce83b Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Sat Jun 5 19:52:59 2021 +0200 function written, now needs testing commit 98a7a04258f2cf6caf9f18925cbeeae2f5b17be4 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Fri Jun 4 16:56:32 2021 +0200 computing live regs at sb entry from its live output regs commit 7ae1fb0faea68ce5cfe04a232e49659247c244e9 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Fri Jun 4 14:24:07 2021 +0200 Passing info of live regs to scheduler: beginning
* Adding both RV expansion methods in kvx-workLéo Gourdin2021-05-191-0/+2
|
* Remove flagsLéo Gourdin2021-04-091-2/+0
|
* Compiler options to manage expansionsLéo Gourdin2021-03-261-1/+1
|
* Adding a flag to test fp_init_expLéo Gourdin2021-03-021-0/+1
|
* Adding a compiler option -fexpanse-rtlcondLéo Gourdin2021-02-161-0/+1
|
* Conditions now propagated by CSE3David Monniaux2021-01-201-0/+2
|\ | | | | | | Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work
| * begin implementing -fcse3-conditionsDavid Monniaux2020-12-091-0/+2
| |
* | Fix --help for prepass (new options)Léo Gourdin2021-01-141-1/+1
| |
* | Fix --help for prepass (default on)Léo Gourdin2021-01-141-1/+1
|/
* Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-081-0/+2
|\
| * Error when using -main without -interpXavier Leroy2020-12-061-0/+2
| | | | | | | | | | | | Outside of -interp mode, -main has no (known) effect but could be confused for a linker option that sets the program's entrypoint, say. It's safer to reject the option.
* | Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-041-1/+8
|\ \ | | | | | | | | | | | | | | | Conflicts: Makefile configure
| * \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-031-0/+3
| |\ \
| * \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-311-0/+2
| |\ \ \
| * \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-271-0/+2
| |\ \ \ \
| * | | | | -mtune=David Monniaux2020-10-221-1/+3
| | | | | |
| * | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-181-11/+11
| |\ \ \ \ \
| * | | | | | command line selection of prepass schedulerDavid Monniaux2020-07-111-0/+3
| | | | | | |
| * | | | | | use a command-line optionDavid Monniaux2020-07-081-1/+3
| | | | | | |
* | | | | | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-11/+4
|\ \ \ \ \ \ \ | |_|_|_|_|/ / |/| | | | | / | | |_|_|_|/ | |/| | | |
| * | | | | Add -main option to specify entrypoint function in interpreter mode (#374)Xavier Leroy2020-10-301-1/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When running unit tests with the CompCert reference interpreter, it's nice to be able to start execution at a given test function instead of having to write a main function. This PR adds a -main command-line option to give the name of the entry point function. The default is still main. Frama-C has a similar option. The function specified with -main is called with no arguments. If its return type is int, its return value is the exit status of the program. Otherwise, its return value is ignored and the program exits with status 0.
| * | | | | Remove no longer needed option enforce-buildnrBernhard Schommer2020-07-081-10/+1
| | | | | |
* | | | | | Loop Rotate with -flooprotateCyril SIX2020-11-031-0/+3
| |_|_|_|/ |/| | | |
* | | | | refining CSE3 nodesDavid Monniaux2020-10-311-0/+2
| |_|_|/ |/| | |
* | | | new option for CSE3 (trivial ops)David Monniaux2020-10-271-0/+2
| |_|/ |/| |
* | | Loop body unrolling with -funrollbody nCyril SIX2020-10-161-0/+2
| | |
* | | -O0 desactivates -fpredict and -ftracelinearizeCyril SIX2020-10-141-0/+1
| | |
* | | Updated --helpCyril SIX2020-10-141-9/+5
| | |
* | | new flags: -fpredict, -ftailduplicate n, -funrollsingle n instead of just ↵Cyril SIX2020-10-091-2/+3
| |/ |/| | | | | -fduplicate n
* | -fcse3-glbDavid Monniaux2020-05-061-0/+2
| |
* | CSE3 across mergesDavid Monniaux2020-05-061-0/+2
| |
* | Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-231-1/+4
|\ \
| * | CSE3 across callsDavid Monniaux2020-04-231-1/+3
| | |
| * | Merge remote-tracking branch 'origin/mppa-cse3' into mppa-licmDavid Monniaux2020-04-231-0/+1
| |\ \
| | * | make tracing output optionalDavid Monniaux2020-04-231-0/+1
| | | |
* | | | Merge remote-tracking branch 'origin/mppa-fast-div' into mppa-featuresDavid Monniaux2020-04-201-0/+6
|\ \ \ \
| * \ \ \ Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2020-04-201-10/+46
| |\ \ \ \ | | | | | | | | | | | | | | | | | | (unfinished)
| * | | | | added -fdiv-i32 and -fdiv-i64 optionsDavid Monniaux2019-05-291-3/+9
| | | | | |
* | | | | | Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-201-0/+4
|\ \ \ \ \ \ | | |_|/ / / | |/| | | |
| * | | | | add options for controlling madd and notrap selectionDavid Monniaux2020-04-191-0/+2
| | | | | |
| * | | | | begin adapting for LICM phaseDavid Monniaux2020-04-011-0/+2
| | |_|/ / | |/| | |
* | | | | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-121-2/+8
|\ \ \ \ \ | |/ / / / |/| | | |
| * | | | -fbranch-probabilitiesDavid Monniaux2020-04-081-1/+2
| | | | |
| * | | | reloading and exploiting seems to workDavid Monniaux2020-04-081-1/+3
| | | | |
| * | | | fixed a bug in support libraries; reload profiling infoDavid Monniaux2020-04-081-0/+1
| | | | |
| * | | | begin installing profilingDavid Monniaux2020-04-081-1/+3
| | |/ / | |/| |
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-171-1/+5
|\| | |
| * | | Desactivating branch predictions by defaultCyril SIX2020-03-171-1/+5
| | | |
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-151-0/+2
|\| | |
generated by cgit (git 2.34.1) at 2024-05-19 23:56:24 +0000