aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* Merge ../kvx-work into kvx_fp_divisionDavid Monniaux2022-02-031-2/+2
|\
| * Merge remote-tracking branch 'absint/master' into merge_absintDavid Monniaux2022-02-021-2/+2
| |\
| | * Enforce evaluation order in IRC.add_interf and IRC.add_prefXavier Leroy2021-12-071-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As written previously, OCaml can evaluate `nodeOfVar g v1` and `nodeOfVar g v2` in any order. Consequently, `v1` and `v2` can be entered in the `varTable` hash table in different order. This can result in different (but equally valid) register allocations. It's better to enforce one evaluation order for the sake of reproducible compilations when the OCaml version changes.
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx_fp_divisionDavid Monniaux2021-12-142-3/+3
|\| |
| * | Merge remote-tracking branch 'absint/master' into towards_3.10David Monniaux2021-12-012-3/+3
| |\| | | | | | | | | | Mostly changes in PTree
| | * An improved PTree data structure (#420)Xavier Leroy2021-11-162-3/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This PR replaces the "PTree" data structure used in lib/Maps.v by the canonical binary tries data structure proposed by A. W. Appel and described in the paper "Efficient Extensional Binary Tries", https://arxiv.org/abs/2110.05063 The new implementation is more memory-efficient and a bit faster, resulting in reduced compilation times (-5% on typical C programs, up to -10% on very large C functions). It also enjoys the extensionality property (two tries mapping equal keys to equal data are equal), which simplifies some proofs.
* | | some more fixed etc. constructsDavid Monniaux2021-12-121-0/+156
|/ /
* | Merge branch 'RTL_has_loaded' into kvx-workLéo Gourdin2021-11-0223-1382/+1324
|\ \
| * | bugfixLéo Gourdin2021-11-021-2/+2
| | |
| * | being more archi-independantLéo Gourdin2021-11-028-22/+19
| | |
| * | Porting the BTL non-trap loads approach to RTLLéo Gourdin2021-11-0223-1377/+1322
| | |
* | | Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-292-2/+2
|\ \ \ | |/ / |/| / | |/
| * Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-032-2/+2
| | | | | | | | This avoids a new warning of Coq 8.14.
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-242-5/+8
|\|
| * Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-151-2/+5
| | | | | | | | | | | | 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
| * Handle the new warnings of OCaml 4.13Xavier Leroy2021-09-131-3/+3
| | | | | | | | | | | | | | | | | | | | | | Warning 69 "mutable record field is never mutated": 3 occurrences in backend/IRC.ml removed the "mutable" qualifier on these fields Warning 70 "cannot find interface file" many .ml files have no .mli no strong motivation to add the .mli files turned off the warning in Makefile.extr
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-082-8/+10
| | | | | | | | | | | | 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.
| * Emit no entry for variables without init in json.Bernhard Schommer2021-04-291-1/+7
| | | | | | | | | | | | | | Variables without init do not generated any assembly code so no entry in the json AST should be generated. They correspond to extern variables without initializer that are defined in another compilation unit. Bug 30112
| * Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-191-1/+1
| |
* | Merge branch 'kvx-work' of ↵David Monniaux2021-09-013-5/+107
|\ \ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
| * | cleanupLéo Gourdin2021-09-011-9/+0
| | |
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-workLéo Gourdin2021-09-015-89/+24
| |\ \
| * \ \ [MERGE] BTL into kvx-work (replacing RTLpath)Léo Gourdin2021-09-013-5/+116
| |\ \ \
| | * \ \ Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-1038-738/+774
| | |\ \ \
| | * | | | [disabled checker] BTL Scheduling and Renumbering OK!Léo Gourdin2021-05-271-0/+1
| | | | | |
| | * | | | Moving common tools, adding liveness input/output information to BTL ↵Léo Gourdin2021-05-243-2/+39
| | | | | | | | | | | | | | | | | | | | | | | | generation oracle
| | * | | | Changing to an opaq record in BTL info, this is a broken commitLéo Gourdin2021-05-201-0/+52
| | | | | |
| | * | | | Grouping common RTL functions, printer improvementLéo Gourdin2021-05-192-5/+2
| | | | | |
* | | | | | Merge remote-tracking branch 'origin/parameterized-cse3' into kvx-workDavid Monniaux2021-09-014-61/+79
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | |
| * | | | | more parameterizationDavid Monniaux2021-07-161-2/+0
| | | | | |
| * | | | | make operations cse3 parametricDavid Monniaux2021-07-162-6/+10
| | | | | |
| * | | | | make trivial ops parametricDavid Monniaux2021-07-162-6/+7
| | | | | |
| * | | | | make conditions a parameter in CSE3David Monniaux2021-07-162-3/+12
| | | | | |
| * | | | | rename parameterized versionsDavid Monniaux2021-07-162-38/+38
| | | | | |
| * | | | | make CSE3 condition parametricDavid Monniaux2021-07-162-29/+42
| | | | | |
| * | | | | rm condition parametrization in CSE3analysisDavid Monniaux2021-07-162-13/+6
| | | | | |
* | | | | | RTLTunneling: fix comments and authors informationSylvain Boulmé2021-08-245-89/+24
| |/ / / / |/| | | |
* | | | | remove default_notrap_load_valueSylvain Boulmé2021-07-241-1/+1
| | | | |
* | | | | Merge branch 'kvx-work' into rtl-tunnelingSylvain Boulmé2021-07-2413-25/+18
|\| | | |
| * | | | Replacing default notrap load value by Vundef everywherecsix-PhDCyril SIX2021-06-1813-25/+18
| | |/ / | |/| |
* | | | Change "Tunneling" to "LTLTunneling" everywherePierre Goutagny2021-06-175-5/+5
| | | | | | | | | | | | | | | | To respect the symmetry between RTL- and LTL-Tunneling
* | | | Use Tunnelinglibs in TunnelingauxPierre Goutagny2021-06-171-256/+81
| | | |
* | | | Simplify tunneling factorisationPierre Goutagny2021-06-172-168/+173
| | | | | | | | | | | | | | | | | | | | The recursive module definitions required unnecessarily long expicit signatures for little added legibility.
* | | | Use Tunnelinglibs in RTLTunnelingauxPierre Goutagny2021-06-162-265/+123
| | | |
* | | | Add Tunneling factorisation modulePierre Goutagny2021-06-161-0/+237
| | | |
* | | | Add RTL Tunneling as a passPierre Goutagny2021-06-142-0/+6
| | | |
* | | | Add the RTLTunneling oraclePierre Goutagny2021-06-141-0/+284
| | | |
* | | | Complete RTLTunnelingproofPierre Goutagny2021-06-111-16/+66
| | | | | | | | | | | | | | | | There is still some refactoring to do, though
* | | | Complete `tunnel_step_correct` proof up to IjumptablePierre Goutagny2021-06-101-9/+227
| | | | | | | | | | | | | | | | Excluding Icond
* | | | Starts proof for `tunnel_step_correct`Pierre Goutagny2021-06-091-15/+120
| | | |
generated by cgit (git 2.34.1) at 2024-05-08 23:53:07 +0000