aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Use vfpv3 registers also in dwarf. Bug 20489Bernhard Schommer2016-11-291-5/+10
|
* Reset all Hashtbls.Bernhard Schommer2016-11-252-10/+14
| | | | | A non reseted Hashtbl caused problems with multiple input files. Bug 20462
* Do not use hardcoded register number for sp.Bernhard Schommer2016-11-252-11/+11
| | | | | | Since the dwarf register names for x86_32 and x86_64 differ it is wrong to hardcode the dwarf register number for rsp to 4. Bug 20461
* Warning for C11 _Noreturn feature.Bernhard Schommer2016-11-221-4/+10
| | | | The warning for C11 features is now also triggered for _Noreturn.
* Warning for decls without name in composites.Bernhard Schommer2016-11-224-6/+15
| | | | | | The warning missing declarations is now also triggered for declarations without name in field lists of composite types if the declaration is not an anonymous composite or a bitfield member.
* C2C: revise typing and translation of __builtin_memcpy_alignedXavier Leroy2016-11-172-12/+22
| | | | | | | | | | | | | | | | | | | | This fixes two issues: 1- The 'size' and 'alignment' arguments of __builtin_memcpy_aligned were declared with type 'unsigned int', which is not good for a 64-bit platform. 2- The corresponding arguments were not cast to type 'unsigned int', causing compilation errors if e.g. the size argument is a 64-bit integer. (Reported by Michael Schmidt.) The fix: 1- Evaluate the 3rd and 4th arguments at type size_t 2- Support both Vint and Vlong as results of this evaluation 3- Declare these arguments with type 'unsigned long'. Supporting work: in lib/Camlcoq.ml, add Z.modulo and Z.is_power2 operations. Concerning part 3 of the fix, type size_t would be better for future platforms where size_t is bigger than unsigned long, but some more work is needed to delay the evaluation of C2C.builtins_generic to after Cutil.size_t_ikind() is stable, or, equivalently, to evaluate the cparser/ machine configuration before C2C initializes.
* Initializers: introduce 'constval_cast' to cast constant value to desired typeXavier Leroy2016-11-172-21/+25
| | | | This comes handy in the next commit where constval_cast is used from C2C.
* C2C: wrong translation of 'switch' over arguments of type 'long' if 'long' ↵Xavier Leroy2016-11-171-4/+5
| | | | | | | is 64 bits It was wrongly assumed that 'long' is 32 bits. (Reported by Michael Schmidt.)
* Use 64 bit address in debug information.Bernhard Schommer2016-11-107-19/+36
| | | | | Address constants need to be 64bit also in the debug information. Bug 20335
* Removed folders from .merlin.Bernhard Schommer2016-11-091-4/+0
|
* Added ${arch}_${bitsize} for x86 to .merlinBernhard Schommer2016-11-091-1/+4
|
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2016-11-081-1/+1
|\
| * x86: mark register rax as destroyed by callsXavier Leroy2016-11-081-1/+1
| | | | | | | | | | | | Calls to variadic or unprototyped functions set this register to reflect the number of arguments passed in XMM registers. Thus we must make sure that rax is not used to hold the pointer to the function being called. (Report by Michael Schmidt.)
* | fix va_arg for pointer types on 64bit targetMichael Schmidt2016-11-081-1/+7
| |
* | extend constant check for builtin_memcpy_aligned (bug 20320)Michael Schmidt2016-11-071-2/+2
|/
* extend constant check for builtin_memcpy_aligned (bug 20320)Michael Schmidt2016-11-071-0/+2
|
* allow Cow version 8.5pl3Michael Schmidt2016-11-041-1/+1
|
* update info about x86 in manpageMichael Schmidt2016-11-031-2/+2
|
* remove unused file, update tests for arch-field of configuration filesMichael Schmidt2016-11-033-20/+7
|
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2016-10-283-141/+2
|\
| * powerpc/runtime: add commentsXavier Leroy2016-10-281-1/+2
| |
| * runtime/powerpc: remove useless files, add commentsXavier Leroy2016-10-282-140/+0
| |
* | Update http to httpsMichael Schmidt2016-10-281-1/+1
|/
* Merge pull request #145 from AbsInt/64Xavier Leroy2016-10-27191-7066/+16450
|\ | | | | | | Support for 64-bit target processors + support for x86 in 64-bit mode
| * Documentation updates to mention 64-bit mode and x86_64 portXavier Leroy2016-10-272-7/+32
| |
| * Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵Xavier Leroy2016-10-2757-624/+332
| | | | | | | | | | | | | | | | | | | | | | | | -> 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).
| * i64_smulh: revert to conditional branches instead of predicated insnsXavier Leroy2016-10-251-8/+8
| | | | | | | | "subslt" changes the flags, affecting the condition of the "sbclt" that follows.
| * x86-32: make sure is_longconst and mullimm work correctly in 32 bitsXavier Leroy2016-10-252-9/+11
| | | | | | | | | | | | SelectLong.is_longconst was always returning 'false' in 32 bits. SelectLong.mullimm was generating a Omullimm insn even in 32 bits. Both functions are used by SelectDiv.
| * SplitLong: propagate constants through "longofint"Xavier Leroy2016-10-252-4/+8
| | | | | | | | | | This can make a big difference in which optimizations are triggered later. Constants were already propagated by "longofintu".
| * Update PowerPC port (not tested yet)Xavier Leroy2016-10-253-2/+144
| |
| * Update ARM port. Not tested yet.Xavier Leroy2016-10-2521-278/+535
| |
| * ia32: add support for __builtin_bswap64 + a bit of DWARF for x86-64Xavier Leroy2016-10-242-4/+53
| | | | | | | | | | __builtin_bswap64 is now available both in 32 and 64-bit mode. The DWARF bit is the numbering of registers in ia32/Asmexpand.ml.
| * cparser/PackedStructs: fix assertion that was wrong for 64-bit targetsXavier Leroy2016-10-241-1/+1
| |
| * Update the tests in test/regression, continuedXavier Leroy2016-10-242-13/+5
| |
| * driver/Interp: updateXavier Leroy2016-10-241-8/+8
| | | | | | | | | | Cherry-pick commit d1311e6 from trunk. Simplify convert_external_arg so that it works both in 32 and 64 bits.
| * Update the tests and test infrastructure in test/regressionXavier Leroy2016-10-2412-7/+132
| | | | | | | | | | Tests updated to work with x86 64 bits. Infrastructure added: script "Runtest", with ability to have different reference outputs depending on platform or bit size.
| * configure for ia32-macosx: update for MacOS 10.12Xavier Leroy2016-10-131-1/+1
| |
| * x86-64 MacOS X supportXavier Leroy2016-10-116-31/+68
| | | | | | | | | | - Avoid absolute addressing for labels, use RIP-relative addressing - Different, RIP-relative implementation of jump tables
| * Regression: handling of integer + pointer in CompCert CXavier Leroy2016-10-064-115/+112
| | | | | | | | | | | | During the experiments, the integer + pointer cases was removed from the semantics of the C addition operator. The idea was to turn integer + pointer into pointer + integer during elaboration, but it was not implemented. On second thoughts, we can restore the integer + pointer cases in the formal semantics of CompCert C at low cost. This is what this commit does.
| * Regression: compile-time evaluation of ((struct s *)0)->fieldXavier Leroy2016-10-062-4/+7
| | | | | | | | | | This somewhat useful idiom was broken when Val.add was replaced by Val.offset_ptr in the Efield case. This commit restores the previous behavior. This used to be supported (and is useful
| * 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-0429-25/+3031
| | | | | | | | | | | | 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-043-122/+121
| | | | | | | | | | | | 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-024-31/+361
| |
| * Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-0222-203/+547
| | | | | | | | | | | | 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-0131-1625/+4945
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * Support for 64-bit architectures: update the PowerPC portXavier Leroy2016-10-0116-752/+478
| | | | | | | | | | The PowerPC port remains 32-bit only, no support is added for PPC 64. This shows how much work is needed to update an existing port a minima.
| * Support for 64-bit architectures: generic supportXavier Leroy2016-10-0176-2557/+4834
| | | | | | | | | | | | | | | | | | | | | | - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
* | macosx needs all strings in degub_str.Bernhard Schommer2016-10-251-1/+2
| |
* | Pass range info to the children.Bernhard Schommer2016-10-251-1/+2
| |
generated by cgit (git 2.34.1) at 2024-07-03 01:14:28 +0000