aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* Always try inlining functionsYann Herklotz2023-04-271-4/+1
|
* Change preference for new register in allocatorBernhard Schommer2023-03-061-29/+34
| | | | | | | | | | | | Currently, the register allocator picks caller-save registers in preference to callee-save registers. But for ARM in Thumb mode, more compact code is obtained if we prefer integer registers R0...R3 rather than all integer caller-save registers. This commit introduces an `allocatable_registers` function in $ARCH/Conventions1.v that determines the preferred and remaining registers to be used for register allocation.
* Ignore self assign in if-conversionBernhard Schommer2023-02-202-4/+19
| | | | | | | | A self assign `x = x` can be classified as a skip in `classify_stmt`. This helps with the if-conversion of some code that the previous passes generates, e.g. for nested C conditional expressions. Closes: #466
* Disable tail calls in variadic functionsMichael Schmidt2023-01-232-5/+6
| | | | | | | | | Variadic functions can use the stack frame to store values of registers. Hence, a pointer within the stack frame can be put in a va_list, and the stack frame should not be deallocated before a function call that may use this va_list. Fixes: #473
* Use `exfalso` instead of `elimtype False` (#470)Pierre-Marie Pédrot2022-12-222-3/+3
| | | | Adapt w.r.t. coq/coq#16904.
* Update doc commentXavier Leroy2022-12-081-2/+2
|
* Add `Declare Scope` where appropriate (#440)Xavier Leroy2022-09-193-0/+5
| | | | | | And re-enable the `undeclared-scope` warning. `Declare Scope` has been available since Coq 8.12, which is now the minimal Coq version supported.
* RTLgen: use the state and error monad for reserve_labels (#371)Pierre Nigron2022-09-193-24/+20
|
* Improved auto goal selection (#443)Andrej Dudenhefner2022-09-084-5/+5
| | | | | | Improves robustness in case of stronger (e)auto. This is in preparation of a change in Coq that will make auto and eauto stronger (https://github.com/coq/coq/pull/16293).
* Recognize more if-then-else statements that can be if-convertedXavier Leroy2022-09-052-126/+138
| | | | | | | | Ignore debug statements that could have prevented the recognition of a simple assignment. Since debug statements can formally get stuck, revise the simulation diagram to use the "eventually" modality.
* Remove unused functions.Bernhard Schommer2022-09-031-7/+0
| | | | | | | | | | The `reset_constants` was only used for ARM and there it was superfluous since the jumptables, which it additionally resets in contrast to `reset_literals`, are always empty since jumptables are handled directly in during printing of the instruction. The `exists_constants` function is now also unused since we test directly for the different sizes in `emit_constants`.
* More simplifications for literal printingBernhard Schommer2022-09-032-13/+16
| | | | | | | Use the same code to split 64 bit literals into two 32 bit halfs as is used for 64 bit initialization data and print them in PrintAsm. This removes the need for a target specific printing function for 64 bit literals.
* Refactor emitting of constants.Bernhard Schommer2022-09-032-2/+15
| | | | | | The function was the same for nearly all backends and also the way 32 bit literals are printed so we moved it to PrintAsm. The 64 bit literals however are still target specific.
* Add `iter_literal*` functions with guaranteed iteration orderXavier Leroy2022-09-031-0/+12
| | | | This makes compilation runs more reproducible.
* Support mergeable sections for fixed-size literalsXavier Leroy2022-08-293-4/+39
| | | | | | | | | | | | On platforms that support them (ELF, macOS), use mergeable sections (like `.rodata.cst8`) for 4-, 8- and 16-byte wide literals. Works only if the LITERAL section is the default one. If the user provided their own LITERAL section, all literals are put in it regardless of their sizes. Support for mergeable string sections is introduced in this commit too but needs further changes in C2C.ml .
* 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.
* 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.
* Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-032-2/+2
| | | | This avoids a new warning of Coq 8.14.
* 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
|
* Fix regression on PowerPC / DiabXavier Leroy2021-02-231-2/+7
| | | | | | | | | | | | | On PowerPC/Diab, common declarations must not be used for small data sections. Add a `~common` option to `PrintAsmaux.variable_section` to control the use of common declarations. The default is whatever is specified on the command line using the `-fcommon` and `-fno-common` options. Use `~common:false` for `Section_small_data` on PowerPC / Diab. Note that on PowerPC/Linux, GCC uses common declarations for uninitialized variables in small data section, so we keep doing this in CompCert as well.
* Section handling: finer control of variable initializationXavier Leroy2021-02-233-10/+25
| | | | | | | | | | | | | 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.
* Introduce and use PrintAsmaux.variable_sectionXavier Leroy2021-02-231-7/+12
| | | | | | | This is a generalization of the previous PrintAsmaux.common_section function that - handles initialized variables in addition to uninitialized variables; - can be used for Section_const, not just for Section_data.
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-2110-60/+60
| | | | | | | 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`.
* Improve branch tunnelingXavier Leroy2021-01-132-60/+328
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The previous branch tunneling was missing optimization opportunities introduced by the optimization of conditional branches. For example: L1: instr; branch L2 L2: if cond then branch L3 else branch L4 L3: branch L4 L4: ... was transformed into L1: instr; branch L2 L2: branch L4 L3: branch L4 L4: ... missing a tunneling opportunity (branch L2 -> branch L4). This commit improves branch tunneling so that the expected code is produced: L1: instr; branch L4 L2: branch L4 L3: branch L4 L4: ... To this end, additional equalities are introduced in the union-find data structure corresponding to optimizable conditional branches. In rare cases these additional equalities trigger new opportunities for optimizing conditional branches. Hence we iterate the analysis until no optimizable conditional branch remains.
* Revised correctness proof for record_gotoXavier Leroy2021-01-131-68/+29
| | | | | | | | | | We used to define an instrumented version record_goto' that also builds the measure f, prove it correct, then show equivalence with record_goto. The new proofs make do without the instrumented version. They prove strong existence of the measure, as in `{ f | branch_map_correct (record_goto fn) f}`.
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-2927-636/+636
| | | | | | | | | | | 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-1/+1
| | | | | | 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.
* Add support for __builtin_fabsfXavier Leroy2020-07-272-0/+6
|
* Introduce additional "branch" build information.Bernhard Schommer2020-07-081-2/+2
|
* Move shared code in new file.Bernhard Schommer2020-06-286-5/+44
| | | | | The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
* Eliminate known builtins whose result is ignoredXavier Leroy2020-06-252-40/+54
| | | | | | | | | | | | | | | A typical example is `(void) __builtin_sel(a, b, c)`. It is safe to generate zero code for these uses of builtins because builtins whose semantics are known to the compiler are pure. Other builtins with side effects (e.g. `__builtin_trap`) are not known and will remain in the compiled code. It is useful to generate zero code for these uses of builtins because some of them (e.g. `__builtin_sel`) must be transformed into proper CminorSel expressions during instruction selection. Otherwise, they propagate all the way to ExpandAsm, causing a "not implemented" error there.
* Transform non-recursive Fixpoint into DefinitionXavier Leroy2020-06-212-2/+2
| | | | | | | 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.
* Move reserved_registers to CPragmas.Bernhard Schommer2020-04-202-7/+1
| | | | | | | The list of reserved_registers is never reset between the compilation of multiple files. Instead of storing them in IRC they are moved in the CPragmas file and reset in the a new reset function for Cpragmas whic is called per file.
* Weaker ec_readonly condition over external calls (#225)Xavier Leroy2020-03-021-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, Tany64Xavier Leroy2020-03-021-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.
* Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-241-0/+67
| | | | | | | | | | | | | | The "size_arguments" function and its properties can be systematically derived from the "loc_arguments" function and its properties. Before, the RISC-V port used this derivation, and all other ports used hand-written "size_arguments" functions and proofs. This commit moves the definition of "size_arguments" to the platform-independent file backend/Conventions.v, using the systematic derivation, and removes the platform-specific definitions. This reduces code and proof size, and makes it easier to change the calling conventions.
* Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-212-2/+2
| | | | | | "open!" is the form used in the examples in the OCaml manual. Based on a quick poll it seems to be the preferred form of the OCaml core dev team.
* Refine the type of function results in AST.signatureXavier Leroy2020-02-2113-90/+101
| | | | | | | | | | Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions.
* Remove no longer needed file PrintLTLinBernhard Schommer2019-11-121-115/+0
|
* Make explicit the use of hints from OrderedType (#316)Vincent Laporte2019-10-022-8/+8
| | | | | | | Some hints will move from the core database to the `ordered_type` database (see https://github.com/coq/coq/pull/9772). This commit prepares for this move by adding `with ordered_type` to the invocations of `auto` and `eauto` that use the hints in question.
* Reworked json export.Bernhard Schommer2019-09-123-29/+37
| | | | | | | | | | | | | | The json export prints formatted json, which takes a lot of additional time, however the result is only consumed by other tools and not meant for human reading. This commit implements several small changes in order to speedup the json export: * Removal of usage of the Format Module * Replacing `fprintf` calls by calls to function that print directly, such as `output_string`, etc. * Replacing list of all instruction names by a set of all instructions
* Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-2/+2
| | | Some changes were not correctly propagated to all architectures.
* AArch64 portXavier Leroy2019-08-087-37/+97
| | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* Asmgenproof0: add predicate exec_straight0Xavier Leroy2019-08-071-0/+26
| | | | | | | | | | This is a variant of exec_straight where it is allowed to take zero steps. In other words, exec_straight0 is the "star" relation, while exec_straight is the "plus" relation. In the end we need "plus" relations in simulation diagrams, to show the absence of stuttering. But the "star" relation exec_straight0 is useful to reason about code fragments that are always preceded or followed by at least one instruction.
* Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-071-2/+0
| | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
* Improve CSE for known built-in functionsXavier Leroy2019-07-172-7/+14
| | | | Known built-in functions are guaranteed not to change memory.
generated by cgit (git 2.34.1) at 2024-05-18 03:53:49 +0000