aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* 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.
* Perform constant propagation for known built-in functionsXavier Leroy2019-07-174-16/+168
| | | | | | | When an external function is a known built-in function and it is applied to compile-time integer or FP constants, we can use the known semantics of the builtin to compute the result at compile-time.
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-112/+231
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit adds mechanisms to - recognize certain built-in and run-time functions by name and signature; - associate semantics to these functions, as a partial function from list of values to values; - interpret external calls to these functions according to this semantics (pure function from values to values, memory unchanged, no observable events in the trace); - external calls to unknown built-in and run-time functions remain interpreted as generating observable events and possibly changing memory, like before. The description of the built-ins is split into a target-independent part (in common/Builtins0.v) and a target-specific part (in $ARCH/Builtins1.v). Instruction selection uses the new mechanism in order to - recognize some built-in functions and turn them into operations of the target processor. Currently, this is done for __builtin_sel and __builtin_fabs; more to come. - remove the axioms about int64 helper functions from the standard library. More precisely, the behavior of these functions is still axiomatized, but now it is specified using the more general machinery introduced in this commit, rather than ad-hoc axioms in backend/SplitLongproof. The only built-ins currently described are __builtin_fsqrt (for all platforms) and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be added later.
* Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-086-7/+6
| | | | | | | | | | | | | | | | * Do not use `Pervasives.xxx` qualified names Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`, and uses of `Pervasives` cause fatal warnings. This commit uses unqualified names instead, as no ambiguity occurs. * Clarify "open" statements OCaml 4.08.0 has stricter warnings concerning open statements that shadow module names. Closes: #300
* Rename option `-ffavor-branchless` into `-Obranchless`Xavier Leroy2019-07-051-3/+3
| | | | | Easier to type, and consistent with `-Os` (optimize for smaller code / optimize for fewer conditional branches).
* Extended asm: print register names according to their typesXavier Leroy2019-06-171-9/+14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When printing an extended asm code fragment, placeholders %n are replaced by register names. Currently we ignore the fact that some assemblers use different register names depending on the width of the data that resides in the register. For example, x86_64 uses %rax for a 64-bit quantity and %eax for a 32-bit quantity, but CompCert always prints %rax in extended asm statements. This is problematic if we want to use 32-bit integer instructions in extended asm, e.g. int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); produces addl %rax, %rdx which is syntactically incorrect. Another example is ARM FP registers: D0 is a double-precision float, but S0 is a single-precision float. This commit partially solves this issue by taking into account the Cminor type of the asm parameter when printing the corresponding register. Continuing the previous example, int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); now produces addl %eax, %edx This is not perfect yet: we use Cminor types, because this is all we have at hand, and not source C types, hence "char" and "short" parameters are still printed like "int" parameters, which is not good for x86. (I.e. we produce %eax where GCC might have produced %al or %ax.) We'll leave this issue open.
* Cminortyping: relax typechecking of function callsXavier Leroy2019-06-061-12/+15
| | | | | | | Sometimes the result of a void function is assigned to a variable. This can occur with C conditional expressions ?: at type void, e.g. the "assert" macro of MacOS. A similar relaxation was already there in RTLtyping.
* If-conversion optimizationXavier Leroy2019-06-064-72/+584
| | | | | | | | | | | | | | | | | | | | Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches.
* Type inference and type checking for CminorXavier Leroy2019-06-061-0/+797
| | | | | | | This module is similar to RTLtyping: it performs type inference and type checking, but on the Cminor intermediate representation rather than the RTL IR. For each function, it returns a mapping from variables to types. Its first use will be if-conversion optimization.
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-314-5/+5
| | | | | | This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream.
* Support a "select" operation between two valuesXavier Leroy2019-05-202-0/+86
| | | | | | | | | | `Val.select ob v1 v2 ty` is a conditional operation that chooses between the values `v1` and `v2` depending on the comparison `ob : option bool`. If `ob` is `None`, `Vundef` is returned. If the selected value does not match type `ty`, `Vundef` is returned. This operation will be used to model a "select" (or "conditional move") operation at the CminorSel/RTL/LTL/Mach level.
* Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-101-0/+8
| | | | | | | | | | The option -fcommon controls whether uninitialized global variables are placed in the COMMON section. If the option is given in the negated form, -fno-common, variables are not placed in the COMMON section. They are placed in the same sections as gcc does. If the variables are not placed in the COMMON section merging of tentative definitions is inhibited and multiple definitions lead to a linker error, as it does for gcc.
* Change to AbsInt version string.Bernhard Schommer2019-05-102-2/+2
| | | | | The AbsInt build number no longer contains "release", so it must be printed additionally.
* Expand the responsefiles earlierBernhard Schommer2019-05-102-4/+4
| | | | | | | | | * Move the expansion of response files to module Commandline, during the initialization of `Commandline.argv`. This way we're sure it's done exactly once. * Make `Commandline.argv` a `string array` instead of a `string array ref`. We no longer need to update it after initialization! * Improve reporting of errors during expansion of response files.
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-263-20/+21
| | | | | | | | | | The module Integers.Make contained lots of definitions and theorems about Z integers that were independent of the word size. These definitions and theorems are useful outside Integers.Make, but it felt unnatural to fetch them from modules Int or Int64. This commit moves the word-size-independent definitions and theorems to a new module, lib/Zbits.v, and fixes their uses in the code base.
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-235-20/+22
| | | | | Instead, use definitions and lemmas from the Coq standard library (ZArith, Znumtheory).
* Replace nat_of_Z with Z.to_natXavier Leroy2019-04-235-17/+17
| | | | | | | Use Z.to_nat theorems from the standard Coq library in preference to our theorems in lib/Coqlib.v. Simplify lib/Coqlib.v accordingly.
* Print only debug info for printed functions.Bernhard Schommer2019-04-161-1/+2
| | | | | | | | | | | Functions that are removed from the compilation unit, for example inline functions without extern, should not produce debug information. This commit reuses the mechanism used for variables in order to track additionally the printed functions. Therefore the printed variable versions are exchanged for a printed symbol version. Bug 26234
* Typo in comment about Ijumptable in RTL.vAlix Trieu2019-04-151-1/+1
|
* Fix typo in section name in Selectionproof.v Alix Trieu2019-04-151-2/+2
| | | SEL_SWITH_INT -> SEL_SWITCH_INT
* RTLgenproof: destruct too deepXavier Leroy2019-03-251-2/+2
| | | | | | | `external_call_mem_extends` returns a conjunction of 4 properties, but the destruct pattern was 5 level deep. (Reported by Jeremie Koenig in pull request #278.)
* Minor simplifications in two proofs. (#280)Vincent Laporte2019-03-251-2/+2
| | | Preparation for Coq PR 9725 that may make `eauto` stronger.
* Make the checker happy (#272)Vincent Laporte2019-02-121-6/+8
| | | Previously, the coqchk type- and proof-checker would take forever on some of CompCert's modules. This commit makes minimal changes to the problematic proofs so that all of CompCert can be checked with coqchk. Tested with Coq versions 8.8.2 and 8.9.0.
* Simplified code. Bug 24067Bernhard Schommer2018-09-121-8/+8
|
* Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-122-3/+35
| | | | | | | | | | | | | | | | | | | | | | | | | | * Generate a nop instruction after ais annotations. In order to prevent the merging of ais annotations with following Labels a nop instruction is inserted, but only if the annotation is followed immediately by a label. The insertion of nop instructions is performed during the expansion of builtin and pseudo assembler instructions and is processor independent, by inserting a __builtin_nop built-in. * Add Pnop instruction to ARM, RISC-V, and x86 ARM as well as RISC-V don't have nop instructions that can be easily encoded by for example add with zero instructions. For x86 we used to use `mov X0, X0` for nop but this may not be as efficient as the true nop instruction. * Implement __builtin_nop on all supported target architectures. This builtin is not yet made available on the C side for all architectures. Bug 24067
* Various improvements in the wording of diagnostics.Michael Schmidt2018-08-021-4/+4
| | | | | | Fix various typos in diagnostic messages and unified wording and capitalization. Bug 23850
* Treat Outgoing stack slots as caller-save in LTL/Linear semantics (#237)Xavier Leroy2018-06-176-93/+145
| | | | | | | | | | | | | | | | | | | * Outgoing stack slots are set to Vundef on return from a function call, modeling the fact that the callee could write into those stack slots. (CompCert-generated code does not do this, but code generated by other compilers sometimes does.) * Adapt Stackingproof to this new semantics. This requires tighter reasoning on how Linear's locsets are related at call points and at return points. * Most of this reasoning was moved from Stackingproof to Lineartyping, because it can be expressed purely in terms of the Linear semantics, and tracked through the wt_state predicate. * Factor out and into Conventions.v: the notion of callee-save locations, the "agree_callee_save" predicate, and useful lemmas on Locmap.setpair. Now the same "agree_callee_save" predicate is used in Allocproof and in Stackingproof.
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-018-8/+79
| | | | | | | | | | The semantics of external function calls in LTL, Linear, Mach and Asm now consider that all caller-save registers are set to Vundef by the call. This models that fact that the external function can modify those registers arbitrarily. Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes accordingly.
* Add newline directly on list in annot.Bernhard Schommer2018-03-132-4/+7
| | | | | | | This should avoid cluttering the assembler output with .ascii "\n" lines if the annotation ends with a string and make for a better readability. Bug 23169
* Print size argument of Init_space as Z not as int32Xavier Leroy2018-03-131-1/+1
| | | | | Init_space has an argument of type Z and it can exceed the range of a 32-bit integer. Reported by Frédéric Besson.
* Introduce more brackets for register annotation.Bernhard Schommer2018-03-121-4/+5
| | | | | | It seems necessary that the mulitplication for the high part of split registers is put into brackets. Bug 23169
* Do not use "Require" inside sections (#224)Xavier Leroy2018-03-121-3/+1
| | | | | | This will soon be deprecated by Coq. Manual merge of pull request #224 by vbgl. Closes: #224
* Added seperator in warning msg. Bug 23179Bernhard Schommer2018-03-091-1/+1
|
* Do not use default printer for variable names.Bernhard Schommer2018-03-091-2/+8
| | | | | | Printing variable names with the default expression printer results in newlines in the outputed error message. Bug 23169
* Perform quoting for json.Bernhard Schommer2018-03-081-1/+8
| | | | | | The strings for json need quoting of special characters such as \" and \\. Bug 22438
* Print symbols as symbols.Bernhard Schommer2018-03-082-4/+26
| | | | | | This allows us to replacing them by their address in valex and additionally checking them. Bug 22438
* Improve error messages.Bernhard Schommer2018-03-071-16/+14
| | | | | | | | Include the format specifier in error message when available in order to make it easier to spot the broken ais parameter. Futhermore introduce a new warning for unused ais parameters. Bug 22464
* Reword error message. Fix 22464Bernhard Schommer2018-03-071-2/+2
|
* Improve wording.Bernhard Schommer2018-03-071-1/+1
| | | | | Mention that it is a global memory cell. Fix 22464
generated by cgit (git 2.34.1) at 2024-06-28 19:40:47 +0000