aboutsummaryrefslogtreecommitdiffstats
path: root/arm/TargetPrinter.ml
Commit message (Collapse)AuthorAgeFilesLines
* 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
| * Fixed typos in the arm and ia32 section printing.Bernhard Schommer2015-10-161-1/+1
| | | | | | | | Bug 17392
| * Implemented the usage of DW_AT_ranges for non-contiguous address ranges.Bernhard Schommer2015-10-161-0/+1
| | | | | | | | | | | | | | | | | | | | The gcc produces DW_AT_ranges for non-contiguous address ranges, like compilation units containing functions which are placed in different ELF-sections or lexical scopes that are split up. With this commit CompCert also uses this DWARF v3 feature for gnu backend based targets. In order to ensure backward compability a flag is added which avoids this and produces debug info in DWARF v2 format. Bug 17392.
| * First step to implemente address ranges for the gnu backend.Bernhard Schommer2015-10-151-7/+1
| | | | | | | | | | | | | | | | | | In contrast to the dcc, the gcc uses address ranges to express non-contiguous range of addresses. As a first step we set the start and end addresses for the different address ranges for the compilation unit by using the start and end addresses of functions. Bug 17392.
| * Use section type also for other targets.Bernhard Schommer2015-10-151-2/+2
| | | | | | | | Bug 17392.
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-141-47/+47
| |
| * Implement the usage of the debug_str section for the gcc backend.Bernhard Schommer2015-10-131-1/+1
| | | | | | | | | | | | | | | | GCC prints all string larger than 3 characters in the debug_str section which reduces the size of the debug information since entries containing the same string now map to the same string in the debug_str sections. Bug 17392.
* | Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-47/+47
| |
* | Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-2/+2
|/ | | | | | | | | | 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 the rest of the funciton needed for thte debug info under arm.Bernhard Schommer2015-10-091-5/+23
| | | | | | 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.
* Add the forgotten Fileinfo also to arm and ia32 TargetPrinter.mlBernhard Schommer2015-10-021-0/+1
|
* Cleanup of now no longer needed functions.Bernhard Schommer2015-10-011-11/+1
|
* Change the way the debug sections are printed.Bernhard Schommer2015-09-281-1/+1
| | | | | | If a user uses the #pragma use_section for functions the diab linker requires a separate debug_info section for each entry. This commit adds functionality to emulate this behavior.
* Added printing the reference address for the LocRef and started refactoring oldBernhard Schommer2015-09-271-9/+1
| | | | | | | | Debuging code. The old functions to store the symbol for the Global variables and retrive this is no longer needed since the atom is stored in DebugInformation. Also the Debug.Abbrev module is no longer needed.
* Added support for the locations of stack allocated local variables.Bernhard Schommer2015-09-251-0/+1
| | | | | This commit adds furher support for location information for local variables and starts with the implementation of the debug_loc section.
* Record the scope structure during unblocking.Bernhard Schommer2015-09-221-0/+2
| | | | | | Instead of creating separate annotations for the local variables we call the Debug.add_lvar_scope and we construct a mapping from function id + scope id to scope information.
* Revert "Startet implementation of new Debug interface."Bernhard Schommer2015-09-101-1/+0
| | | | This reverts commit 861292a6c5e58b4f78bef207c717b801b3fc1fed.
* Startet implementation of new Debug interface.Bernhard Schommer2015-09-061-0/+1
| | | | | | Added a new file debug/Debug.ml which will be the interface between for generating and printing the debuging information. Currently it contains only the code for the line directived.
* XBernhard Schommer2015-09-061-21/+11
|\ | | | | | | Merge branch 'master' into debug_locations
| * Upgrade the ARM port to the new builtins.Xavier Leroy2015-08-241-21/+11
| |
* | Added symbol functions for printing of the location for global variables.Bernhard Schommer2015-08-211-0/+6
|/
* Updated the branch and implemented the suggested changes.Bernhard Schommer2015-07-141-0/+17
|
* Merge branch 'asmexpand' of github.com:AbsInt/CompCertBernhard Schommer2015-06-261-279/+42
|
* Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert"Bernhard Schommer2015-06-261-42/+279
| | | | | This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1.
* Moved the printing of the builtin functions etc. into Asmexpand for ARM in ↵Bernhard Schommer2015-06-101-279/+42
| | | | the same way as it is done for PPC.
* Merged PrintAnnot into PrintAsmaux.Bernhard Schommer2015-05-141-4/+4
|
* Cleanups and updates for extended asm.Xavier Leroy2015-04-211-1/+1
|
* Support for GCC-style extended asm, continued:Xavier Leroy2015-04-211-1/+1
| | | | | | | | - support "r", "m" and "i" constraints - support "%Q" and "%R" modifiers for register pairs - support register clobbers - split off analysis and transformation of asm statements in cparser/ExtendedAsm.ml
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-171-2/+2
|
* Correct type of label function.Bernhard Schommer2015-04-161-1/+1
|
* Added missing dummy functions.Bernhard Schommer2015-04-161-0/+4
|
* Merge branch 'master' into dwarfBernhard Schommer2015-03-231-2/+6
|\
| * Fix .type and .size annotations: @ is comment, use % instead.Xavier Leroy2015-03-201-2/+6
| |
* | Merge branch 'master' into dwarfBernhard Schommer2015-03-161-0/+1
|\|
| * Missing initialization of current_function_sig.Xavier Leroy2015-03-141-0/+1
| |
* | Started implementing the printing functions for the debug info. Added a ↵Bernhard Schommer2015-03-161-0/+6
| | | | | | | | global target dependend option to activate the printing only for targets wher it works.
generated by cgit (git 2.34.1) at 2024-07-01 09:16:34 +0000