aboutsummaryrefslogtreecommitdiffstats
path: root/arm
Commit message (Collapse)AuthorAgeFilesLines
* 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.
* | ARM: tweak stack layout so that back link and return address are lowerXavier Leroy2017-08-171-37/+34
| | | | | | | | This reduces the chances that back link and return address cannot be saved by a single str instruction. We generate correct code for the overflow case, but the code isn't very efficient, so let's make it uncommon.
* | ARM port: replace Psavelr pseudo-instruction by actual instructionsXavier Leroy2017-08-176-47/+88
| | | | | | | | | | | | Saving the return address register (R14) in the function prologue can be done either with a single "str" instruction if the offset is small enough, or by constructing the address using the R12 register as a temporary then storing with "str" relative to R12. R12 can be used as a temporary because it is marked as destroyed at function entry. We just need to tell Asmgen.translcode whether R12 still contains the back link left there by Pallocframe, or R12 was trashed. In the latter case R12 will be reloaded from the stack at the next Mgetparam instruction.
* | ARM: Generate Pcfi_rel_offset directives directly from AsmgenXavier Leroy2017-08-174-12/+17
| | | | | | | | This is what we do for PowerPC and is more resilient to changes in code generation. We need to give Pcfi_rel_offset a dynamic semantics, but that's just a no-op.
* | Push correct registerMichael Schmidt2017-08-021-1/+1
| |
* | Improve stack offset addressingMichael Schmidt2017-08-025-35/+73
| | | | | | | | Functions which require large amounts of stack for spilling and/or arguments for function calls lead to stackframe offsets that exceed the 12bit limit of immediate constants in ARM instructions. This patch fixes the stack-offsets in the function prolog/epilog.
* | Integrated fixup code in estimated size.Bernhard Schommer2017-07-261-0/+3
| | | | | | | | | | | | | | 12 was a too small overaproximation for call which require fixup code for arguments and result. The new constant is 72, which consists of 4 for the branch instruction, 16 * 4 for the arguments and 4 for the result.
* | Print_annot should produce a string.Bernhard Schommer2017-07-191-3/+8
|/
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-065-2/+37
| | | | | | | | - Add support for PowerPC, with all addressing modes. - Add support for ARM, with "reg + ofs" addressing mode. - Add support for RISC-V, with the one addressing mode. - Constprop.v: forgot to recurse in BA_addptr - volatile4 test: more tests
* Formatted json printing.Bernhard Schommer2017-06-282-3/+3
| | | | | | | | | Instead of just dumping the json output it is now a little bit formatted for better reading. Furthermore the AsmToJson function for the non powerpc targets now prints the json value "null" sucht that the resulting json file is valid json.
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-038-27/+32
| | | | | | | | | | | | | This commit adds code generation for 64bit PowerPC architectures which execute 32bit applications. The main difference to the normal 32bit PowerPC port is that it uses the available 64bit instructions instead of using the runtime library functions. However pointers are still 32bit and the 32bit calling convention is used. In order to use this port the target architecture must be either in Server execution mode or if in Embedded execution mode the high order 32 bits of GPRs must be implemented in 32-bit mode. Furthermore the operating system must preserve the high order 32 bits of GPRs.
* RISC-V port and assorted changesXavier Leroy2017-04-282-0/+13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes. The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/ This port required the following additional changes: - Integers: More properties about shrx - SelectOp: now provides smart constructors for mulhs and mulhu - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu. - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library. - test/: add SIMU make variable to run tests through a simulator - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers commit da14495c01cf4f66a928c2feff5c53f09bde837f Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Thu Apr 13 17:36:10 2017 +0200 RISC-V port, continued Now working on Asmgen. commit 36f36eb3a5abfbb8805960443d087b6a83e86005 Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Wed Apr 12 17:26:39 2017 +0200 RISC-V port, first steps This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.
generated by cgit (git 2.34.1) at 2024-06-26 18:59:28 +0000