aboutsummaryrefslogtreecommitdiffstats
path: root/arm
Commit message (Collapse)AuthorAgeFilesLines
* 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.
* Give explicit scopes to notations a#b and a##b and a#b<-cXavier Leroy2017-02-131-4/+6
| | | | Without scopes Coq 8.6 warns, probably rightly so.
* Use "Local" as prefixXavier Leroy2017-02-133-4/+4
| | | | | Open Local becomes Local Open. This silences Coq 8.6's warning. Also: remove one useless Require-inside-a-module that caused another warning.
* ARM, PowerPC: update Asmgenproof for Coq 8.6Xavier Leroy2017-02-131-8/+8
|
* Remove unused open.Bernhard Schommer2017-02-061-1/+0
|
* Fallthrough no depends on the last instruction.Bernhard Schommer2016-12-151-4/+4
| | | | | | Since the test for emit constants has moved before the printing of the instruction the no_fallthrough of the last test should be used. Bug 20598
* Be more conservative in emiting constants.Bernhard Schommer2016-12-151-815/+827
| | | | | | | | | | Switch tables were able to screw up the book keeping for emiting constants in code. Now we estimate the size of an instruction before printing it by the safe upper bound of 12 for normal instructions, 1024 for inline assembler and (2 or 3 + length switch tbl) * 4 for switch tables depending on thumb etc. Bug 20598
* Use vfpv3 registers also in dwarf. Bug 20489Bernhard Schommer2016-11-291-5/+10
|
* Use 64 bit address in debug information.Bernhard Schommer2016-11-101-0/+2
| | | | | Address constants need to be 64bit also in the debug information. Bug 20335
* Update ARM port. Not tested yet.Xavier Leroy2016-10-2515-271/+388
|
* improve fixup code (bug 19792)Michael Schmidt2016-09-151-0/+2
|
* Add interference for indirect calls.Bernhard Schommer2016-09-151-1/+5
| | | | | | Avoids problems with overwritting the registe containing the function address. Bug 19779
* Add missing fixup-code for ARM EABI (bug 19792)Michael Schmidt2016-09-141-2/+0
|
* add missing print operatorMichael Schmidt2016-09-141-0/+1
|
* Implement support for big endian arm targets.Bernhard Schommer2016-08-055-29/+60
| | | | | | | | Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
* Merge branch 'master' of /common/repositories/git/tools/compcertBernhard Schommer2016-07-092-0/+36
|\
| * bug 19318, add implementation of __builtin_ctz, __builtin_ctzl and ↵Michael Schmidt2016-07-082-0/+36
| | | | | | | | __builtin_ctzll for ARM
* | Port to Coq 8.5pl2Xavier Leroy2016-07-084-17/+14
|/ | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* Improved handling of "rotate left" and "rotate right" operatorsXavier Leroy2016-06-221-1/+1
| | | | | | | | - Values: "rol" and "ror" are defined even if their second argument is not in the [0,31] range (for consistency with "rolm" and because the semantics is definitely well defined in this case). - NeedDomain: more precise analysis of "rol" and "rolm", could benefit the PowerPC port.
* Remove code that will is deprecated in ocaml 4.03Bernhard Schommer2016-06-212-3/+3
| | | | | | | | Most of the code can be String.uppercase usages can either be replaced by a more specialized version of coqstring_of_camlstring (which is also slightly more effecient) or by specialized checks that reject wrong code earlier. Bug 19187
* fix '__builtin_annot_val' to '__builtin_annot_intval', such that CompCert ↵Michael Schmidt2016-06-071-1/+1
| | | | can parse its own .compcert.c output, bug 18060
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-173-163/+156
| | | | | | | | | | | | | This commit changes the loc_arguments and loc_result functions that describe calling conventions so that each argument/result can be mapped either to a single location or (in the case of a 64-bit integer) to a pair of two 32-bit locations. In the current CompCert, all arguments/results of type Tlong are systematically split in two 32-bit halves. We will need to change this in the future to support 64-bit processors. The alternative approach implemented by this commit enables the loc_arguments and loc_result functions to describe precisely which arguments need splitting. Eventually, the remainder of CompCert should not assume anything about splitting 64-bit types in two halves. Summary of changes: - AST: introduce the type "rpair A" of register pairs - Conventions1, Conventions: use it when describing calling conventions - LTL, Linear, Mach, Asm: honor the new calling conventions when observing external calls - Events: suppress external_call', no longer useful - All passes from Allocation to Asmgen: adapt accordingly.
* bug 18925, fix loading of symbols for thumb: :lower16: and :upper16: are ↵Michael Schmidt2016-05-131-1/+2
| | | | restricted to 15bit signed immediate offsets
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit ↵Xavier Leroy2016-04-273-272/+157
| | | | | | | | | | | | | | | | | | | architectures The original Stacking pass and its proof hard-wire assumptions about the processor and the register allocation, namely that integer registers are 32 bit wide and that all stack slots have natural alignment 4, which precludes having stack slots of type Tlong. Those assumptions become false if the target processor has 64-bit integer registers. This commit makes minimal adjustments to the Stacking pass so as to lift these assumptions: - Stack slots of type Tlong (or more generally of natural alignment 8) are supported. For slots produced by register allocation, the alignment is validated a posteriori in Lineartyping. For slots produced by the calling conventions, alignment is proved as part of the "loc_argument_acceptable" property in Conventions1. - The code generated by Stacking to save and restore used callee-save registers no longer assumes 32-bit integer registers. Actually, it supports any combination of sizes for registers. - To support the new save/restore code, Bounds was changed to record the set of all callee-save registers used, rather than just the max index of callee-save registers used. On CompCert's current 32-bit target architectures, the new Stacking pass should generate pretty much the same code as the old one, modulo minor differences in the layout of the stack frame. (E.g. padding could be introduced at different places.) The bulk of this big commit is related to the proof of the Stacking phase. The old proof strategy was painful and not obviously adaptable to the new Stacking phase, so I rewrote Stackingproof entirely, using an approach inspired by separation logic. The new library common/Separation.v defines assertions about memory states that can be composed using a separating conjunction, just like pre- and post-conditions in separation logic. Those assertions are used in Stackingproof to describe the contents of the stack frames during the execution of the generated Mach code, and relate them with the Linear location maps. As a further simplification, the callee-save/caller-save distinction is now defined in Conventions1 by a function is_callee_save: mreg -> bool, instead of lists of registers of either kind as before. This eliminates many boring classification lemmas from Conventions1. LTL and Lineartyping were adapted accordingly. Finally, this commit introduces a new library called Decidableplus to prove some propositions by reflection as Boolean computations. It is used to further simplify the proofs in Conventions1.
* */TargetPrinter.ml: wrong comment attached to Init_float32 constantsXavier Leroy2016-04-091-1/+1
| | | | For informative purposes, the FP value of Init_float* constants is printed as a comment in the generated asm file. However, for Init_float32, it was wrongly printed as a double-precision FP instead of a single-precision FP.
generated by cgit (git 2.34.1) at 2024-06-30 23:55:14 +0000