aboutsummaryrefslogtreecommitdiffstats
path: root/ia32
Commit message (Collapse)AuthorAgeFilesLines
* x86-64 MacOS X supportXavier Leroy2016-10-114-30/+51
| | | | | - Avoid absolute addressing for labels, use RIP-relative addressing - Different, RIP-relative implementation of jump tables
* Fix some 32-bit regressionsXavier Leroy2016-10-042-15/+56
| | | | 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-0411-8/+69
| | | | | | 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.
* Remove usage of do.Bernhard Schommer2016-10-042-64/+63
| | | | | | Apparently coq compiled with camlp4 has a problem with the user defined do <- ... ; ... and do. Bug 20050
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-022-29/+252
|
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-0212-51/+134
| | | | | | Implement the 'shift right extended' trick, both in the generic implementation (backend/SplitLong) and in the IA32 port. Note that now SelectDiv depends on SelectLong, and that some work was moved from SelectLong to SelectDiv.
* Support for 64-bit architectures: x86 in 64-bit modeXavier Leroy2016-10-0124-1621/+4506
| | | | | | | | | | | | | | | | | | | 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-184-50/+95
| | | | | | | | 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.
* Add interference for indirect calls.Bernhard Schommer2016-09-151-1/+5
| | | | | | Avoids problems with overwritting the registe containing the function address. Bug 19779
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-3/+2
| | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* Improved handling of "rotate left" and "rotate right" operatorsXavier Leroy2016-06-221-2/+2
| | | | | | | | - 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
* ia32/Conventions1: remove commented-out proof attemptXavier Leroy2016-05-241-17/+0
|
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-173-69/+112
| | | | | | | | | | | | | 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.
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit ↵Xavier Leroy2016-04-275-246/+134
| | | | | | | | | | | | | | | | | | | 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.
* Merge branch 'master' into cleanupBernhard Schommer2016-03-214-64/+37
|\
| * Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-203-62/+32
| |\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This pull request implements "approach A" to separate compilation in CompCert from the paper Lightweight verification of separate compilation by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis, POPL 2016, pages 178-190 In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program. This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.
| | * Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-062-61/+31
| | |
| | * 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.
| * | 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.
| * | GPR#84: add missing IA32 operators to PrintOpXavier Leroy2016-03-151-0/+3
| |/
* | Added interface for the Asmexpansion.Bernhard Schommer2016-03-161-2/+2
| | | | | | | | | | | | Hide the reference used internally behind the interface and added some functions to access the needed values. Bug 18394
* | Cleanup of AsmToJSON.Bernhard Schommer2016-03-161-0/+13
| | | | | | | | | | | | Removed unused code, factored out common functions and added an interface file. Bug 18394
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-153-11/+12
| | | | | | | | | | | | 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-103-56/+17
|/ | | | | Removed some unused functions and opens. Bug 18394
* Add CLZ builtins for ARM and IA32Xavier Leroy2015-12-222-2/+33
| | | | | | | ARM: add __builtin_clzl, __builtin_clzll IA32: add __builtin_clzl, __builtin_clzll, __builtin_ctzl, __builtin_ctzll Add corresponding tests in tests/regression/
* The return type of __builtin_clz() et al is "int", as documented and for GCC ↵v2.6Xavier Leroy2015-12-211-2/+2
| | | | compatibility, and not "unsigned int", as previously implemented.
* 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.
* bug 17752, builtin_nop for ia32Michael Schmidt2015-12-142-0/+6
|
* Also replace extern_atom by camlstring_of_coqstring for ia32/TargetPrinter.ml.Bernhard Schommer2015-10-201-2/+2
| | | | Bug 17450
* Merge remote-tracking branch 'origin/master' into named-externalsBernhard Schommer2015-10-202-11/+11
|\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-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-1414-562/+562
| |
| * bug 17392: fix typo in OS nameMichael Schmidt2015-10-141-1/+1
| |
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-143-61/+61
| |
| * 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.
* | Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-2017-621/+621
| |
* | Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-113-18/+11
|/ | | | | | | | | | 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-092-38/+63
| | | | | | 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.
* Fixed minor typos in the comments.Bernhard Schommer2015-10-041-1/+1
|
* 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.
generated by cgit (git 2.34.1) at 2024-07-01 08:26:16 +0000