aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-243-26/+49
|\
| * For numerical builtins, support return types that are small integer typesXavier Leroy2021-09-221-25/+47
| |
| * Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-152-1/+2
| | | | | | | | | | | | Instead, add `Set Asymmetric Patterns` to the files that need it, or use `Arguments` to make inductive types work better with symmetric patterns. Closes: #403
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-0822-88/+110
| | | | | | | | | | | | The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
| * Support __builtin_unreachableXavier Leroy2021-05-021-0/+5
| | | | | | | | Not yet used for optimizations.
| * Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-192-15/+15
| |
| * Do not depend on projection parameter names (#388)Xia Li-yao2021-03-251-1/+1
| | | | | | | | | | | | coq/coq#13852 fixes an oddity in the automatically-generated names for projection parameters. There was one place in CompCert where one of these automatically-generated names was used. This commit avoids using this name.
* | [MERGE] BTL into kvx-work (replacing RTLpath)Léo Gourdin2021-09-012-5/+17
|\ \
| * | remove todos, cleanLéo Gourdin2021-07-281-0/+14
| | |
| * | Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-1022-540/+598
| |\ \
| * | | Moving common tools, adding liveness input/output information to BTL ↵Léo Gourdin2021-05-241-1/+1
| | | | | | | | | | | | | | | | generation oracle
| * | | Changing to an opaq record in BTL info, this is a broken commitLéo Gourdin2021-05-201-49/+0
| | | |
| * | | Grouping common RTL functions, printer improvementLéo Gourdin2021-05-192-4/+51
| | | |
* | | | Make prepass scheduling sensitive to register pressure, by Nicolas Nardino.David Monniaux2021-07-161-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* | | | Replacing default notrap load value by Vundef everywherecsix-PhDCyril SIX2021-06-181-2/+0
| |/ / |/| |
* | | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-011-0/+28
|\| |
| * | Merge remote-tracking branch 'origin/manuscript' into kvx-worksubmission_OOPSLA2021_AARCH64_KVXCyril SIX2021-04-131-0/+28
| |\ \
| | * | Getting all loop bodiesCyril SIX2021-04-021-0/+14
| | | |
| | * | Simple backedge detection (modified code from get_loop_headers)Cyril SIX2021-04-021-0/+14
| | | |
* | | | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-0122-104/+131
| | | | | | | | | | | | | | | | cfrontend/C2C.ml
* | | | replacing omega with lia in some fileLéo Gourdin2021-03-293-8/+11
| | | |
* | | | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-2315-428/+456
|\ \ \ \ | |/ / / |/| | / | | |/ | |/| | | | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
| * | Section handling: finer control of variable initializationXavier Leroy2021-02-232-25/+54
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Distinguish between: - uninitialized variables, which can go in COMM if supported - variables initialized with fixed, numeric quantities, which can go in a readonly section if "const" - variables initialized with symbol addresses which may need relocation, which cannot go in a readonly section even if "const", but can go in a special "const_data" section. Also: on macOS, use ".const" instead of ".literal8" for literals, as not all literals have size 8.
| * | Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-216-12/+12
| | | | | | | | | | | | | | | | | | | | | This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`.
| * | Replace `omega` tactic with `lia`Xavier Leroy2020-12-2912-382/+382
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
| * | Changed cc_varargs to an option typeBernhard Schommer2020-12-251-5/+5
| | | | | | | | | | | | | | | | | | Instead of being a simple boolean we now use an option type to record the number of fixed (non-vararg) arguments. Hence, `None` means not vararg, and `Some n` means `n` fixed arguments followed with varargs.
* | | Merge remote-tracking branch 'origin/riscV-cmov' into riscv-workLéo Gourdin2021-03-021-0/+21
|\ \ \
| * | | has_type_bDavid Monniaux2021-01-301-0/+21
| | |/ | |/|
* / | Expansion of Ccompimm in RTL [Admitted checker]Léo Gourdin2021-02-021-1/+1
|/ /
* | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2021-01-071-0/+118
|\ \
| * | Uniformizing a couple of debug print functionsCyril SIX2020-12-171-0/+118
| | |
* | | Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-071-0/+49
|/ /
* | Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-042-0/+33
|\ \ | | | | | | | | | | | | | | | Conflicts: Makefile configure
| * \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassCyril SIX2020-12-011-1/+0
| |\ \ | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: arm/Op.v common/Values.v kvx/Op.v
| | * | missing lemmasDavid Monniaux2020-11-251-0/+21
| | | |
| * | | proves op_valid_pointer_eq lemma for RISC-V (necessary for the pre-pass ↵Sylvain Boulmé2020-10-171-0/+22
| | | | | | | | | | | | | | | | scheduler)
| * | | Characterizing Op dependency on memorySylvain Boulmé2020-07-081-0/+12
| |/ /
* | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-182-1/+7
|\ \ \ | |/ / |/| / | |/
| * Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-0/+1
| | | | | | | | __builtin_sqrt (no "f") is the name used by GCC and Clang.
| * Add support for __builtin_fabsfXavier Leroy2020-07-271-0/+5
| |
| * Transform non-recursive Fixpoint into DefinitionXavier Leroy2020-06-211-1/+1
| | | | | | | | | | | | | | As detected by the new warning in Coq 8.12. The use of Fixpoint here is not warranted and either an oversight or a leftover from an earlier version.
* | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-123-15/+75
|\ \
| * | fix reverse printing problem for hashesDavid Monniaux2020-04-111-1/+8
| | |
| * | print hashesDavid Monniaux2020-04-082-3/+4
| | |
| * | begin installing profilingDavid Monniaux2020-04-083-7/+8
| | |
| * | added EF_profilingDavid Monniaux2020-04-083-14/+65
| | |
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-085-37/+108
|\| |
| * | Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-workCyril SIX2020-04-012-10/+23
| |\|
| | * Explicit error messages for ill-formed section attributes (#232)Bernhard Schommer2020-03-292-10/+23
| | | | | | | | | | | | | | | | | | | | | | | | Introduce an error message for section attributes with non string arguments,and another for multiple, ambiguous section attributes. This is more consistent with the handling of other attributes, like packed, than the old behavior of silently ignoring them.
| * | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-033-27/+85
| |\ \ | | | | | | | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2
generated by cgit (git 2.34.1) at 2024-07-14 03:38:41 +0000