aboutsummaryrefslogtreecommitdiffstats
path: root/arm
Commit message (Collapse)AuthorAgeFilesLines
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-15/+55
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Remove the cparser/Builtins moduleXavier Leroy2019-07-171-2/+2
| | | | | | | | | Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`.
* Add floating-point square root and fused multiply-addXavier Leroy2019-07-171-0/+5
| | | | | | | | We just lift the corresponding functions from Flocq and add the computation of NaN payloads. NaN payloads for FMA are described in the ARM and RISC-V specifications, and were determined experimentally for x86 and for Power.
* Revised specification of NaN payload behaviorXavier Leroy2019-07-121-17/+39
| | | | | | | | | | | | | | When an FP arithmetic instruction produces a NaN result, the payload of this NaN depends on the architecture. Before, the payload behavior was specified by 3 architecture-dependent parameters: `Archi.choose_binop_pl_64` and `Archi.choose_binop_pl_32` and `Archi.fpu_results_default_qNaN`. This was adequate for two-argument operations, but doesn't extend to FMA. In preparation for FMA support, this commit generalizes the `Archi.choose` functions from two arguments to any number of arguments. In passing, `Archi.fpu_results_default_qNaN` is no longer needed.
* Extended asm: print register names according to their typesXavier Leroy2019-06-171-3/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Perform constant propagation and strength reduction on conditional movesXavier Leroy2019-06-172-2/+36
| | | | | A conditional move whose condition is statically known becomes a regular move. Otherwise, the condition can sometimes be simplified by strength reduction.
* Added Pfmovite to list of known mnemonic names.Bernhard Schommer2019-06-061-1/+1
|
* ARM: select is not supported at type TlongXavier Leroy2019-06-062-2/+11
|
* ARM: Fix expansion of FP conditional moveXavier Leroy2019-05-261-2/+2
| | | | | The "vmov" instruction (Advanced SIMD) cannot be conditional. The "vmov.f64" instruction (VFPv2) can be conditional.
* Implement a `Osel` operation for ARMXavier Leroy2019-05-2012-7/+115
| | | | | The operation comples down to conditional moves. Both integer and floating-point conditional moves are supported.
* Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-101-2/+2
| | | | | | | | | | 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.
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-1/+2
| | | | | | | | | | 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-231-1/+1
| | | | | Instead, use definitions and lemmas from the Coq standard library (ZArith, Znumtheory).
* Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-14/+15
| | | | | | | | | | | | Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully).
* Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-124-6/+10
| | | | | | | | | | | | | | | | | | | | | | | | | | * 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
* Import prim token notations before using them, continuedXavier Leroy2018-08-271-0/+1
| | | | | Follow-up to f6f537d. "list" scope must be opened to counterbalance opening of "string" scope.
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-012-3/+12
| | | | | | | | | | 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.
* Print symbols as symbols.Bernhard Schommer2018-03-081-16/+16
| | | | | | This allows us to replacing them by their address in valex and additionally checking them. Bug 22438
* Fix register naming for stack pointer.Bernhard Schommer2018-03-081-1/+1
| | | | | | It should be 'esp' respectively 'rsp' for x86, 'r13' for arm and 'sp' for riscV. Bug 23176.
* Also use binary output for arm. Fix 23172Bernhard Schommer2018-03-071-1/+1
|
* Fix arm compile broken by merge problems.Bernhard Schommer2018-03-061-4/+2
|
* Reactivated and improved ais annotations.Bernhard Schommer2018-03-061-5/+6
| | | | | | | | | | | | | | | | | | The ais annotations are now handled in a separate file shared between all architectures. Also two different variants of replacements are supported, %e which expands to ais expressions and %l which also expands to an ais expression but is guaranted to be usable as l-value in the ais annotation. Otherwise the new warning is Wrong_is_parameter is generated. Also an error message is generated if floating point variables are used in ais annotations since a3 does not support them at the moment. Additionally an error message is generated for plain volatile variables used, since they will enforce a volatile load and result in the value being passed to the annotation instead of the address as other global variables.
* Improve strength reduction of unsigned comparisons x ==u 0, x !=u 0, etc (#59)Xavier Leroy2018-02-162-15/+49
| | | | | | | | | | | | | | | | | | | When x is known to be either 0 or 1, comparisons such as x == 0 x != 0 x == 1 x != 1 can be optimized away. This optimization was already performed for signed comparisons. This commit extends the optimization to unsigned comparisons as well. Additionally, for PowerPC only, some unsigned (dis)equality comparisons are turned into signed comparisons when we know it makes no difference, i.e. when both arguments are guaranteed not to be pointers. The reason is that Asmgen can produce shorter instruction sequences for some signed equality comparisons than for the corresponding unsigned comparisons. It's important to optimize unsigned integer comparisons because casts to the C99 type _Bool are compiled as x !=u 0 unsigned comparisons. In particular, cascades of casts to _Bool are now reduced to a single cast much more often than before.
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-081-1/+1
| | | | | | | | | | | | | | | | | * Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/ * Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the Diagnostics module. * Raise on error before calling external tools. * Added diagnostics to clightgen. * Fix error handling of AsmToJson. * Cleanup error handling of Elab and C2C. *The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
* Remove mnemonics not exported to JSON from mnemonics listMichael Schmidt2018-01-091-4/+4
|
* Change AsmToJson to be similar to other printers.Bernhard Schommer2018-01-052-5/+17
|
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-051-0/+3
| | | | | | | | | | | Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent. This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed. Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST which is not in lib/
* Reintroduce informative comments for Pflid_lbl/Pflis_lbl in target printerMichael Schmidt2017-12-151-3/+6
|
* Reintroduce informative comment for Ploadsymbol_lbl in target printerMichael Schmidt2017-12-151-2/+2
|
* Introduce 'cmn' instruction and optimize compare-with-immediate when negated ↵Michael Schmidt2017-12-156-1/+27
| | | | immediates can be encoded.
* Moved constant expansion into Asmexpand. (#40)Bernhard Schommer2017-12-145-318/+419
| | | | | This commit introduces a new pass which is run after the expansion of the builtin functions which performs the expansion and placement of constants inside the function code.
* Use instructions with immediate operands that don't need replacement by the ↵Michael Schmidt2017-12-141-4/+3
| | | | assembler (add ra, rb, #-1 --> sub ra, rb, #1)
* Export configured architecture to JSON (#38)Michael Schmidt2017-12-131-3/+3
| | | The architecture which was configured is now exported in a new top-level json field.
* Optimization for division by one during constant propagation (#39)Michael Schmidt2017-12-052-10/+24
| | | | Signed and unsigned divisions by literal 1 are already optimized away during the Selection phase. This pull request also optimizes those divisions when the 1 divisor is produced by constant propagation.
* Remove unused float_abi_type.Bernhard Schommer2017-11-291-12/+0
|
* Added json export for the abstract ARM AssemblerBernhard Schommer2017-11-202-64/+338
| | | | | | | The json export for the abstract ARM Assembler is quite similar to it's PowerPC equivalent expect for the different instruction arguments. Bug 22472
* Moved arm eabi fixup to Asmexpand.Bernhard Schommer2017-11-163-159/+229
| | | | | | | | Instead of expanding the fixup code for incoming and outgoing registers in the TargetPrinter we expand them in Asmexpand. This simplifies the estimate size function and is a prerequisite for the json export. Bug 22472
* Removed no longer used function. Bug 22525Bernhard Schommer2017-11-091-25/+1
|
* Remove superfluous function.Bernhard Schommer2017-11-061-2/+0
| | | | | The new_label function is alway equal to PrintAsmaux.new_label. Bug 22472
* Fix register name of ais printing and moved label function up.Bernhard Schommer2017-10-251-4/+4
|
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-201-0/+1
|\ | | | | | | Ensure FunInd or Recdef is imported if functional induction is used. This is necessary for Coq 8.7.0.
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-201-0/+1
| | | | | | | | | | | | Coq 8.7 does not load FunInd in prelude anymore, so this is necessary. Recdef exports FunInd, so if Recdef is imported, importing FunInd is not required.
* | New support for inserting ais-annotations.Bernhard Schommer2017-10-193-8/+16
| | | | | | | | | | | | | | | | | | | | | | | | The ais annotations can be inserted via the new ais variants of the builtin annotation. They mainly differe in that they have an address format specifier '%addr' which will be replaced by the adress in the binary. The implementation simply prints a label for the builtin call alongside a the text of the annotation as comment and inserts the annotation together as acii string in a separate section 'ais_annotations' and replaces the usages of the address format specifiers by the address of the label of the builtin call.
* | Moved common buitlins to C2C gernic_builtins.Bernhard Schommer2017-09-261-9/+0
| |
* | Added dump-mnemonics option.Bernhard Schommer2017-09-252-0/+4
| | | | | | | | | | | | This option allows it to dump a list of all used mnemonics into a file. Bug 22239
* | Remove coq warnings (#28)Bernhard Schommer2017-09-224-35/+35
| | | | | | | | Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
* | Take advantage of ARMv6T2/ARMv7 instructions even if not in Thumb2 mode (#203)Gergö Barany2017-09-186-16/+25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Clarify that ARMv6 is in fact ARMv6T2 The ARMv6 comes in two flavors depending on the version of the Thumb instruction set supported: ARMv6 for the original Thumb, ARMv6T2 for Thumb2. CompCert only supports Thumb2, so its ARMv6 architecture should really be called ARMv6T2. This makes a difference: the GNU assembler rejects most of the instructions CompCert generates for ARMv6 with "-mthumb" if the architecture is specified as ".arch armv6" as opposed to ".arch armv6t2". This patch fixes the architecture specification in the target printer and the internal name of the architecture. It does not change the configure script's flags to avoid breaking changes. * Always use ARM movw/movt to load large immediates These move-immediate instructions used to be only emitted in Thumb mode, not in ARM mode. As far as I understand ARM's documentation, these instructions are available in *both* modes in ARMv6T2 and above. This should cover all of CompCert's ARM targets. Tested for ARMv6 and ARMv7, both with and without Thumb2. The behavior is now identical to Clang, and the GNU assembler accepts these instructions in all configurations. * Separate ARMv6 and ARMv6T2; no movw/movt on ARMv6 - define separate architecture models for ARMv6 and ARMv6T2 - introduce `Archi.move_imm` parameter on ARM to identify models with `movw`/`movt` move-immediate instructions (all except ARMv6, in both ARM and Thumb mode) * Fixes for support for architectures with Thumb2 - rename relevant parameter to `Archi.thumb2_support` - on ARMv6 without Thumb2, silently accept -marm flag (but not -mthumb) - allow generation of `sbfx` in ARM mode if Thumb2 is supported
* | Strength reduction patterns for ARM mla instruction.Gergö Barany2017-09-152-0/+102
| |
* | ARM in Thumb mode: simpler instruction sequence for Pbtbl pseudo, continuedXavier Leroy2017-08-221-1/+2
| | | | | | | | A 16-bit "nop" is needed because in "add pc, r14" pc reads as the address of the add instruction plus 4, and "add pc, r14" has a 16-bit encoding.
* | ARM in Thumb mode: simpler instruction sequence for Pbtbl pseudoXavier Leroy2017-08-221-6/+3
| | | | | | | | It is also easier to recognize than the old one for binary analysis tools.
generated by cgit (git 2.34.1) at 2024-06-28 23:38:34 +0000