aboutsummaryrefslogtreecommitdiffstats
path: root/arm/TargetPrinter.ml
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-2/+2
|\ | | | | | | | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
| * Introduce and use PrintAsmaux.variable_sectionXavier Leroy2021-02-231-2/+2
| | | | | | | | | | | | | | 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.
* | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-121-1/+52
|\ \
| * | seems like the ARM profiling perhaps worksDavid Monniaux2020-04-111-1/+52
| |/
| * Revert "Remove `__builtin_nop` for some architectures. (#208)"Bernhard Schommer2020-01-031-0/+2
| | | | | | | | This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
| * Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-211-2/+0
| | | | | | | | | | | | | | The `__builtin_nop` function is documented only for PowerPC. It was added to the other architectures by copy paste, but has no known uses. So, remove `__builtin_nop` from all architectures but PowerPC.
* | fixes for aarch64 arm ppc ppc64David Monniaux2020-02-241-1/+1
| |
* | fix for x86+arm unsupported thread localDavid Monniaux2020-02-241-1/+3
|/
* 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.
* 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-201-0/+6
| | | | | 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.
* Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-121-1/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | * 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
* 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.
* 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.
* 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-151-0/+2
| | | | immediates can be encoded.
* Moved constant expansion into Asmexpand. (#40)Bernhard Schommer2017-12-141-305/+167
| | | | | 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.
* Remove unused float_abi_type.Bernhard Schommer2017-11-291-12/+0
|
* Added json export for the abstract ARM AssemblerBernhard Schommer2017-11-201-61/+65
| | | | | | | 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-161-157/+30
| | | | | | | | 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
|
* New support for inserting ais-annotations.Bernhard Schommer2017-10-191-3/+11
| | | | | | | | | | | | 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.
* Take advantage of ARMv6T2/ARMv7 instructions even if not in Thumb2 mode (#203)Gergö Barany2017-09-181-4/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * 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
* 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 port: replace Psavelr pseudo-instruction by actual instructionsXavier Leroy2017-08-171-2/+0
| | | | | | 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.
* Improve stack offset addressingMichael Schmidt2017-08-021-12/+5
| | | | 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
|
* 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 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
* improve fixup code (bug 19792)Michael Schmidt2016-09-151-0/+2
|
* Add missing fixup-code for ARM EABI (bug 19792)Michael Schmidt2016-09-141-2/+0
|
* Implement support for big endian arm targets.Bernhard Schommer2016-08-051-5/+7
| | | | | | | | 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
* bug 18925, fix loading of symbols for thumb: :lower16: and :upper16: are ↵Michael Schmidt2016-05-131-1/+2
| | | | restricted to 15bit signed immediate offsets
* */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.
* Merge branch 'master' into cleanupBernhard Schommer2016-03-211-2/+2
|\
| * Print floating-point numbers with more digits in debug outputsXavier Leroy2016-03-151-2/+2
| | | | | | | | | | | | As suggested in GPR#84, use '%.15F' to force the printing of more significant digits. (The '%F' format previously used prints only 6.) This is enough to represent the FP number exactly most of the time (but not always). Once OCaml 4.03 is out and CompCert switches to this version of OCaml, we'll be able to use hexadecimal floats for printing.
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-151-5/+5
| | | | | | | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* | Cleanup of ARM dependedn code.Bernhard Schommer2016-03-101-64/+7
|/ | | | | Removed unused functions and avoid warnings. Bug 18394.
* Do not use "movs rd, rs" nor "movs rd, #imm" in Thumb2 mode.Xavier Leroy2016-02-181-2/+8
| | | | | | | | | | | Two reasons: - The movs is not supported if rd or rs is r13 (the stack ptr register). Newer versions of GNU as reject it, older versions were probably emulating it. - The purpose of setting the "s" flag on some operations is to enable 16-bit encoding in Thumb2 mode. However, for "mov" it is the non-s form that has a 16-bit encoding; the s form is never more compact.
* Print cfi_sections only if cfi is supported.Bernhard Schommer2015-12-151-1/+1
| | | | | | On older version of the binutils the cfi directives are not always supported so we only print cfi_sections if the corresponding .ini setting is set to true.
* Merge remote-tracking branch 'origin/master' into named-externalsBernhard Schommer2015-10-201-8/+3
|\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: arm/TargetPrinter.ml backend/CMparser.mly backend/SelectLongproof.v backend/Selectionproof.v cfrontend/C2C.ml checklink/Asm_printers.ml checklink/Check.ml checklink/Fuzz.ml common/AST.v debug/DebugInformation.ml debug/DebugInit.ml debug/DwarfPrinter.ml debug/DwarfTypes.mli debug/Dwarfgen.ml exportclight/ExportClight.ml ia32/TargetPrinter.ml powerpc/Asm.v powerpc/SelectOpproof.v powerpc/TargetPrinter.ml