| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
| |
The naming of anonymous structs is performed by an additional step
in elab_struct_or_union_info instead of in elab_field_group.
Also the aux functions are renamed to access.
Bug 20003
|
| |
|
|
|
|
| |
Instead of using idents the anonymous fileds get names of the
for <anon>_c where c is a counter of all anonymous members.
Bug 20003
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
The arm dwarf float registers constants are larger than 2 bytes.
Bug 20489
|
| | |
|
| |
|
|
|
| |
A non reseted Hashtbl caused problems with multiple input files.
Bug 20462
|
| |
|
|
|
|
| |
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
|
| |
|
|
| |
The warning for C11 features is now also triggered for _Noreturn.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
This comes handy in the next commit where constval_cast is used from C2C.
|
| |
|
|
|
|
|
| |
is 64 bits
It was wrongly assumed that 'long' is 32 bits.
(Reported by Michael Schmidt.)
|
| |
|
|
|
| |
Address constants need to be 64bit also in the debug information.
Bug 20335
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
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.)
|
| | | |
|
| |/ |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| |/ |
|
| |\
| |
| |
| | |
Support for 64-bit target processors + support for x86 in 64-bit mode
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
-> 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).
|
| | |
| |
| |
| | |
"subslt" changes the flags, affecting the condition of the "sbclt" that follows.
|
| | |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| | |
This can make a big difference in which optimizations are triggered later.
Constants were already propagated by "longofintu".
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
__builtin_bswap64 is now available both in 32 and 64-bit mode.
The DWARF bit is the numbering of registers in ia32/Asmexpand.ml.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
Cherry-pick commit d1311e6 from trunk.
Simplify convert_external_arg so that it works both in 32 and 64 bits.
|
| | |
| |
| |
| |
| | |
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.
|
| | | |
|
| | |
| |
| |
| |
| | |
- Avoid absolute addressing for labels, use RIP-relative addressing
- Different, RIP-relative implementation of jump tables
|
| | |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| | |
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
|
| | |
| |
| |
| | |
While merging the 32- and 64-bit code generators, some regressions were introduced in the 32 bit case.
|
| | |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| | |
Apparently coq compiled with camlp4 has a problem with the user
defined do <- ... ; ... and do.
Bug 20050
|
| | | |
|
