aboutsummaryrefslogtreecommitdiffstats
path: root/ia32/TargetPrinter.ml
Commit message (Collapse)AuthorAgeFilesLines
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵Xavier Leroy2016-10-271-881/+0
| | | | | | | | | | | | -> x86/x86_32/x86_64 Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq. This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86. While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures. Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
* x86-64 MacOS X supportXavier Leroy2016-10-111-25/+44
| | | | | - Avoid absolute addressing for labels, use RIP-relative addressing - Different, RIP-relative implementation of jump tables
* Fix some 32-bit regressionsXavier Leroy2016-10-041-10/+47
| | | | While merging the 32- and 64-bit code generators, some regressions were introduced in the 32 bit case.
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-041-0/+4
| | | | | | This trick was already implemented for 32-bit integer division and modulus. Here we extend it to the 64-bit case. For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned). Tentative implementations are provided for IA32 and PowerPC, but need testing.
* Support for 64-bit architectures: x86 in 64-bit modeXavier Leroy2016-10-011-226/+282
| | | | | | | | | | | | | | | | | | | This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model. To activate x86-64 bit support, configure with "x86_64-linux". Main steps: - Enrich Op.v and Asm.v with 64-bit operations - SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers - Conventions1: support x86-64 ABI in addition to the 32-bit ABI. - Add support for the new 64-bit operations everywhere. - runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode To do: - More optimizations are possible on 64-bit integer arithmetic operations. - Could add new chunks to load, say, an unsigned byte into a 64-bit long (currently we load as a 32-bit int then zero-extend). - Implements the wrong ABI for struct passing.
* IA32: model integer division and modulus closer to the machineXavier Leroy2016-09-181-2/+2
| | | | | | | | lib/Integers.v: define division-remainder of a double word by a word ia32/Asm.v: use it to give Pdiv and Pidiv their "true" semantics like in the processor; add Pcltd as an instruction ia32/*: adapt accordingly Additional benefit: Pcltd could be used for an alternate implementation of shrximm.
* */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.
* 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
* Clean up of ia32 target dependend code.Bernhard Schommer2016-03-101-48/+11
| | | | | Removed some unused functions and opens. Bug 18394
* Do not print cfi_sections for bsd.Bernhard Schommer2015-12-171-1/+1
| | | | | The binutils in bsd seem to support cfi directives but not the cfi_sections directive.
* 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.
* Also replace extern_atom by camlstring_of_coqstring for ia32/TargetPrinter.ml.Bernhard Schommer2015-10-201-2/+2
| | | | Bug 17450
* Fixed typos in the arm and ia32 section printing.Bernhard Schommer2015-10-161-2/+2
| | | | Bug 17392
* Implemented the usage of DW_AT_ranges for non-contiguous address ranges.Bernhard Schommer2015-10-161-1/+4
| | | | | | | | | | 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-6/+0
| | | | | | | | | 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-42/+42
|
* Implement the usage of the debug_str section for the gcc backend.Bernhard Schommer2015-10-131-2/+5
| | | | | | | | 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.
* Filled in missing functions for debug information on ia32.Bernhard Schommer2015-10-091-16/+31
| | | | | | 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-1/+4
| | | | | | 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-10/+0
|
* Change the way the debug sections are printed.Bernhard Schommer2015-09-281-3/+5
| | | | | | 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-8/+0
| | | | | | | | 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-18/+6
|\ | | | | | | Merge branch 'master' into debug_locations
| * Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-231-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | SimplLocals: - record locations of stack-allocated variables with annotations (of kind 5) at the beginning of the function; - mark every assignment to non-stack-allocated variables with an annotation of kind 2. Debugvar: (new pass!) - perform availability analysis for debug annotations of kind 2 - insert "start of live range" and "end of live range" annotations (kind 3 and 4) to delimit intervals of PCs where the location of a local variable is known.
| * Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-221-12/+5
| | | | | | | | | | | | | | | | Use EF_debug instead of EF_annot for line number annotations. Introduce PrintAsmaux.print_debug_info (very incomplete). powerpc/Asmexpand: revise expand_memcpy_small.
| * Simplify the handling of extended inline asm, taking advantage of the new, ↵Xavier Leroy2015-08-211-3/+1
| | | | | | | | structured builtin arguments and results.
| * Merge branch 'master' into 'new-builtins'Xavier Leroy2015-08-211-36/+35
| |\
| * | Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-8/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Before, the back-end languages had distinct instructions - Iannot for annotations, taking structured expressions (annot_arg) as arguments, and producing no results' - Ibuiltin for other builtins, using simple pseudoregs/locations/registers as arguments and results. This branch enriches Ibuiltin instructions so that they take structured expressions (builtin_arg and builtin_res) as arguments and results. This way, - Annotations fit the general pattern of builtin functions, so Iannot instructions are removed. - EF_vload_global and EF_vstore_global become useless, as the same optimization can be achieved by EF_vload/vstore taking a structured argument of the "address of global" kind. - Better code can be generated for builtin_memcpy between stack locations, or volatile accesses to stack locations. Finally, this commit also introduces a new kind of external function, EF_debug, which is like EF_annot but produces no observable events. It will be used later to transport debug info through the back-end, without preventing optimizations.
* | | Merge branch 'master' into debug_locationsBernhard Schommer2015-08-261-36/+35
|\ \ \ | | |/ | |/| | | | | | | | | | | | | Conflicts: debug/CtoDwarf.ml debug/DwarfPrinter.ml debug/DwarfTypes.mli
| * | Consistent naming of "P" instructions and consistent ordering of argumentsXavier Leroy2015-08-211-36/+35
| |/ | | | | | | according to Intel convention (instr destination, argument).
* / Added symbol functions for printing of the location for global variables.Bernhard Schommer2015-08-211-0/+6
|/
* Merge branch 'asmexpand' of github.com:AbsInt/CompCertBernhard Schommer2015-06-261-286/+73
|
* Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert"Bernhard Schommer2015-06-261-73/+286
| | | | | This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1.
* Moved the rest of the ia32 builtins to asmexpand.Bernhard Schommer2015-06-221-287/+28
|
* Started moving functions from TargetPrinter.ml to Asmexpand.ml for ia32.Bernhard Schommer2015-06-181-0/+46
|
* Merged PrintAnnot into PrintAsmaux.Bernhard Schommer2015-05-141-4/+4
|
* Cleanups and updates for extended asm.Xavier Leroy2015-04-211-2/+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/+3
|
* Added missing dummy functions.Bernhard Schommer2015-04-161-0/+8
|
* Merge branch 'master' into dwarfBernhard Schommer2015-04-021-1/+1
|\
| * Merge pull request #34 from AbsInt/extended-annotationsXavier Leroy2015-04-011-1/+1
| |\ | | | | | | Extended annotations
| | * Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-271-1/+1
| | |
* | | Merge branch 'master' into dwarfBernhard Schommer2015-03-311-4/+15
|\| | | | | | | | | | | | | | | | | Conflicts: Makefile driver/Driver.ml
generated by cgit (git 2.34.1) at 2024-07-03 15:20:55 +0000