aboutsummaryrefslogtreecommitdiffstats
path: root/arm/Asmexpand.ml
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-2/+2
|\
| * Fix wrong expansion of __builtin_memcpy_alignedXavier Leroy2021-09-231-2/+2
| | | | | | | | | | | | | | | | | | In the "small" case, there was an error in the choice of temporary registers to use when one argument is a stack location and the other is a register. The chosen temporary could conflict with the argument that resides in a register. Fixes: #412
| * Support __builtin_unreachableXavier Leroy2021-05-021-0/+4
| | | | | | | | Not yet used for optimizations.
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-011-0/+4
| | | | | | | | cfrontend/C2C.ml
* | 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
| * Changed cc_varargs to an option typeBernhard Schommer2020-12-251-2/+2
| | | | | | | | | | | | Instead of being a simple boolean we now use an option type to record the number of fixed (non-vararg) arguments. Hence, `None` means not vararg, and `Some n` means `n` fixed arguments followed with varargs.
* | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-3/+1
|\|
| * Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-1/+1
| | | | | | | | __builtin_sqrt (no "f") is the name used by GCC and Clang.
| * No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-271-2/+0
| | | | | | | | __builtin_fabs has already been expanded in backend/Selection.v .
* | seems like the ARM profiling perhaps worksDavid Monniaux2020-04-111-1/+1
|/
* 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.
* Compatibility for OCaml 4.08.1Bernhard Schommer2019-09-051-1/+1
|
* bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-121-0/+5
| | | | | | | | | | | | * Added semantic for byte swap builtins The `__builtin_bswap`, `__builtin_bswap16`, `__builtin_bswap32`, `__builtin_bswap64` builtin function are now standard builtin functions with a defined semantics. The semantics is given in terms of the decode/encode functions used for the memory model. * Added bswap64 expansion to PowerPC 32 bits. * Added bswap64 expansion for ARM.
* Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-121-4/+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
* Moved constant expansion into Asmexpand. (#40)Bernhard Schommer2017-12-141-1/+3
| | | | | 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)
* Moved arm eabi fixup to Asmexpand.Bernhard Schommer2017-11-161-0/+174
| | | | | | | | 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
* New support for inserting ais-annotations.Bernhard Schommer2017-10-191-4/+4
| | | | | | | | | | | | 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.
* ARM port: replace Psavelr pseudo-instruction by actual instructionsXavier Leroy2017-08-171-7/+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.
* ARM: Generate Pcfi_rel_offset directives directly from AsmgenXavier Leroy2017-08-171-2/+1
| | | | 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-021-17/+45
| | | | 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.
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-061-0/+14
| | | | | | | | - 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
* Use vfpv3 registers also in dwarf. Bug 20489Bernhard Schommer2016-11-291-5/+10
|
* Implement support for big endian arm targets.Bernhard Schommer2016-08-051-8/+10
| | | | | | | | 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 19318, add implementation of __builtin_ctz, __builtin_ctzl and ↵Michael Schmidt2016-07-081-0/+30
| | | | __builtin_ctzll for ARM
* 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
* Merge branch 'master' into cleanupBernhard Schommer2016-03-211-1/+1
|\
| * Add support for EF_runtime externalsXavier Leroy2016-03-061-1/+1
| | | | | | | | Also: in Events, use Senv.equiv to state invariance wrt changes of global envs.
* | Added interface for the Asmexpansion.Bernhard Schommer2016-03-161-4/+4
| | | | | | | | | | | | Hide the reference used internally behind the interface and added some functions to access the needed values. Bug 18394
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-151-1/+1
| | | | | | | | | | | | 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-2/+1
|/ | | | | Removed unused functions and avoid warnings. Bug 18394.
* bug 18168, catch cases where variadic arguments are transfered via registersMichael Schmidt2016-02-241-2/+2
|
* bug 18168, fix offset computation for var-args in ARM stacklayoutMichael Schmidt2016-02-241-1/+1
|
* ARM: bug in expansion of __builtin_clzllXavier Leroy2015-12-221-1/+1
| | | | Follow-up to commit f531d38
* Add CLZ builtins for ARM and IA32Xavier Leroy2015-12-221-1/+7
| | | | | | | ARM: add __builtin_clzl, __builtin_clzll IA32: add __builtin_clzl, __builtin_clzll, __builtin_ctzl, __builtin_ctzll Add corresponding tests in tests/regression/
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-2/+2
|
* Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-1/+1
| | | | | | | | | | The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables.
* Filled in missing functions for debug information on ia32.Bernhard Schommer2015-10-091-23/+2
| | | | | | Like for arm and ppc the functions for section names and start and end addresses of compilation units are defined and the print_annot function is moved to Asmexpandaux.ml.
* Filled in the rest of the funciton needed for thte debug info under arm.Bernhard Schommer2015-10-091-4/+46
| | | | | | The name_of_section function no returns the correct name for the debug sections, the prologue and epilogue directives are added and the labels for the live ranges are introduced in the Asmexpand pass.
* Added versions of the tranform_* functions in AST to work with functionsBernhard Schommer2015-10-081-2/+2
| | | | | | | | taking the ident as argument. This functions are currently not used inside the proven part but it is nice to have them already there, when they are used by some future pass. They also come equiped with the corresponding proofs.
* Upgrade the ARM port to the new builtins.Xavier Leroy2015-08-241-111/+179
|
* Asmexpand for ARM: fixed bug in Pfreeframe.Xavier Leroy2015-08-211-3/+3
| | | | Plus: update comments and credit Bernhard Schommer.
* Fix bugs in Asmexpand.ml for ARM.Xavier Leroy2015-08-211-8/+9
|
* Updated the branch and implemented the suggested changes.Bernhard Schommer2015-07-141-27/+30
|
* Merge branch 'asmexpand' of github.com:AbsInt/CompCertBernhard Schommer2015-06-261-3/+329
|
* Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert"Bernhard Schommer2015-06-261-329/+3
| | | | | This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1.
* Moved the rest of the ia32 builtins to asmexpand.Bernhard Schommer2015-06-221-1/+3
|
* Moved the printing of the builtin functions etc. into Asmexpand for ARM in ↵Bernhard Schommer2015-06-101-3/+327
| | | | the same way as it is done for PPC.
generated by cgit (git 2.34.1) at 2024-05-20 02:55:31 +0000