aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| * 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
| |
* | Merge pull request #147 from m-schmidt/masterXavier Leroy2016-10-243-0/+536
|\ \ | | | | | | Add a man page
| * | Minor improvementsMichael Schmidt2016-10-171-4/+4
| | |
| * | Update description for debugging optionsMichael Schmidt2016-10-141-4/+3
| | |
| * | Add a man-pageMichael Schmidt2016-10-143-0/+537
| | |
* | | implement checks for parameters of '__builtin_memcpy_aligned' (bug 20222)Michael Schmidt2016-10-191-4/+4
| | |
* | | implement checks for parameters of '__builtin_memcpy_aligned' (bug 20222)Michael Schmidt2016-10-191-3/+6
| | |
* | | Remove unnecessary usage of isatty.Bernhard Schommer2016-10-181-1/+1
| | |
* | | Catch errors from Unix for isatty.Bernhard Schommer2016-10-181-1/+4
| | | | | | | | | | | | | | | | | | There is a bug in the fstat implementation in ocaml 4.03 under windows. In order to prevent this we guard the isatty function with an additional try with.
* | | Document -target and -conf. Bug 20210Bernhard Schommer2016-10-181-0/+2
| | |
* | | Query menhir for location of menhir lib in config.Bernhard Schommer2016-10-182-38/+3
| | | | | | | | | | | | | | | | | | Since the menhir version required supports the --suggest-menhirLib flag we can query it already in the configure script simplifying the Makefile.menhir
* | | Refactored debugging options.Bernhard Schommer2016-10-143-31/+42
| | | | | | | | | | | | | | | | | | | | | The options controlling the generation of debugging information are now moved into the Debug module. Futhermore the -gdepth options are replaced in favor of a more gcc compatible version. Bug 20193
* | | Remove undocumented option. Bug 20193Bernhard Schommer2016-10-146-33/+10
|/ /
* | Fix minor typoMichael Schmidt2016-10-121-1/+1
| |
* | Added configure switch for merlin.Bernhard Schommer2016-10-061-0/+35
| | | | | | | | | | | | The new configure switch generates a .merlin file and adds the -bin-annot flag to the compile options. Bug 20081
* | Fixed regression in printing of floats.Bernhard Schommer2016-10-041-1/+1
|/ | | | | Commit 60402c5 breaks printing of default floats by adding support for %lf. This commit adds back support for %f.
* Keep anonymous members of anonymous structs.Bernhard Schommer2016-09-272-3/+5
| | | | | The anonymous members are kept but using them is still an error. Bug 19907
* undefine _Nullable to add some compatibility with macOS 10.12 SDKMichael Schmidt2016-09-231-1/+1
|
* Improved error messages for wrong vararg calls.Bernhard Schommer2016-09-232-4/+10
| | | | | | Now "expected at least %d" instead of "expected %d". Also improved error message for __builtin_debug. Bug 19872
* Catch case of zero in builtin debug.Bernhard Schommer2016-09-221-2/+2
|
* Merge branch 'master' of /common/repositories/git/tools/compcertBernhard Schommer2016-09-221-0/+1
|\
| * mention -Wall in help textMichael Schmidt2016-09-221-0/+1
| |
* | Added sizetyp for subarray bounds. Fix 19894Bernhard Schommer2016-09-223-21/+43
|/
* Added compcert-conformance to wall. Bug 19872Bernhard Schommer2016-09-221-0/+2
|
* Renamed pedantic to implicit-int.Bernhard Schommer2016-09-223-8/+9
| | | | | | | | The only case where compcert raise a pedantic warning was for implicit int parameters. This is the behavior of clang. However since not all other pedantic warnings are supported the behavior of gcc is adopted. Bug 19872.
* Allow %lf type specifier in printf.Bernhard Schommer2016-09-221-1/+1
| | | | | %lf is official part of the C99 standard. Bug 19877
* Reverted noisy change.Bernhard Schommer2016-09-221-1/+1
| | | | | | In order to empty declarations it is necessary to distinguish between forward declarations and empty declarations. Bug 19859
* Merge pull request #142 from maximedenes/minor-fixesXavier Leroy2016-09-213-9/+13
|\ | | | | | | | | | | Fix minor issues in some proofs and tactics. Patch by Maxime Dénès.
| * Fix minor issues in some proofs and tactics.Maxime Dénès2016-09-213-9/+13
| | | | | | | | | | These minor problems were revealed by porting CompCert to Coq 8.6, where they trigger errors.
* | Fix typo in option name. Bug 18004Bernhard Schommer2016-09-211-1/+1
| |
generated by cgit (git 2.34.1) at 2024-07-05 19:34:27 +0000