aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Coq 8.7.0 supportXavier Leroy2017-10-202-3/+8
| | | | | | configure: accept Coq 8.7.0 and 8.6.1. (Coq 8.6 became incompatible with commit b4f59c4.) Changelog: updated.
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-2015-3/+15
|\ | | | | | | Ensure FunInd or Recdef is imported if functional induction is used. This is necessary for Coq 8.7.0.
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-2015-3/+15
| | | | | | | | | | | | Coq 8.7 does not load FunInd in prelude anymore, so this is necessary. Recdef exports FunInd, so if Recdef is imported, importing FunInd is not required.
* | New support for inserting ais-annotations.Bernhard Schommer2017-10-1931-66/+180
| | | | | | | | | | | | | | | | | | | | | | | | The ais annotations can be inserted via the new ais variants of the builtin annotation. They mainly differe in that they have an address format specifier '%addr' which will be replaced by the adress in the binary. The implementation simply prints a label for the builtin call alongside a the text of the annotation as comment and inserts the annotation together as acii string in a separate section 'ais_annotations' and replaces the usages of the address format specifiers by the address of the label of the builtin call.
* | Check recursively for const for modifiable lvalues (#32)Bernhard Schommer2017-10-171-2/+15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Check recursively for const for modifiable lvalues According to 6.3.2.1 a modifiable lvalue is an lvalue that does have a const-qualified type, and if it is a union or structure it does not have any member, including any member of all contained strutures or union, with a const-qualified type. The new check for modifiable lvalue additionally checks this now instead of only testing for toplevel const. Bug 22420
* | Do not generate object files for linking.Bernhard Schommer2017-10-161-7/+14
| | | | | | | | | | | | If CompCert is called to compile and link object files should not be created. Bug 22399
* | Distinguish between long and int for cases.Bernhard Schommer2017-10-131-7/+7
| |
* | Make the list unique. Bug 22239Bernhard Schommer2017-09-261-177/+22
| |
* | Moved common buitlins to C2C gernic_builtins.Bernhard Schommer2017-09-265-34/+11
| |
* | Merge branch 'master' of github.com:AbsIntPrivate/CompCertBernhard Schommer2017-09-250-0/+0
|\ \
| * | Remove coq warnings (#28)Bernhard Schommer2017-09-2272-638/+638
| | | | | | | | | | | | Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
* | | Added dump-mnemonics option.Bernhard Schommer2017-09-258-2/+208
| | | | | | | | | | | | | | | | | | This option allows it to dump a list of all used mnemonics into a file. Bug 22239
* | | Remove coq warnings (#28)Bernhard Schommer2017-09-2272-638/+638
|/ / | | | | | | Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
* | Disallow usage of default pattern for AsmToJSON.Bernhard Schommer2017-09-221-2/+11
| | | | | | | | | | | | | | In order to ensure that no new instruction is added without adding it to the Json export we enforce warning 4 for the instruction printer and removed all default pattern matchings. Bug 22239
* | Update version to 3.1Michael Schmidt2017-09-211-1/+1
| |
* | Some lemmas.Bernhard Schommer2017-09-211-0/+14
| |
* | Typo in Makefile: "ia32" is now "x86"Xavier Leroy2017-09-191-1/+1
| |
* | Reverted reintroduced quote of compilation dir.Bernhard Schommer2017-09-191-2/+2
| |
* | Deadcode: eliminate trivial Icond instructionsXavier Leroy2017-09-182-2/+9
| | | | | | | | | | | | These are conditionals where the "ifso" and the "ifnot" successors are the same. By eliminating them here and not later, we can also eliminate the instructions that compute the arguments to the condition, if any. There is another, later point where these trivial conditional instructions are eliminated: in the Tunneling phase. The elimination done in Tunneling is more powerful in that it works not just for conditionals whose two successors are the same, but also for conditionals whose two successors lead to the same point after a series of nops. The elimination done in Deadcode is more powerful in that it eliminates the instructions that compute the arguments to the condition. Hence it is worth having both eliminations.
* | Take advantage of ARMv6T2/ARMv7 instructions even if not in Thumb2 mode (#203)Gergö Barany2017-09-189-21/+43
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Clarify that ARMv6 is in fact ARMv6T2 The ARMv6 comes in two flavors depending on the version of the Thumb instruction set supported: ARMv6 for the original Thumb, ARMv6T2 for Thumb2. CompCert only supports Thumb2, so its ARMv6 architecture should really be called ARMv6T2. This makes a difference: the GNU assembler rejects most of the instructions CompCert generates for ARMv6 with "-mthumb" if the architecture is specified as ".arch armv6" as opposed to ".arch armv6t2". This patch fixes the architecture specification in the target printer and the internal name of the architecture. It does not change the configure script's flags to avoid breaking changes. * Always use ARM movw/movt to load large immediates These move-immediate instructions used to be only emitted in Thumb mode, not in ARM mode. As far as I understand ARM's documentation, these instructions are available in *both* modes in ARMv6T2 and above. This should cover all of CompCert's ARM targets. Tested for ARMv6 and ARMv7, both with and without Thumb2. The behavior is now identical to Clang, and the GNU assembler accepts these instructions in all configurations. * Separate ARMv6 and ARMv6T2; no movw/movt on ARMv6 - define separate architecture models for ARMv6 and ARMv6T2 - introduce `Archi.move_imm` parameter on ARM to identify models with `movw`/`movt` move-immediate instructions (all except ARMv6, in both ARM and Thumb mode) * Fixes for support for architectures with Thumb2 - rename relevant parameter to `Archi.thumb2_support` - on ARMv6 without Thumb2, silently accept -marm flag (but not -mthumb) - allow generation of `sbfx` in ARM mode if Thumb2 is supported
* | Merge pull request #202 from gergo-/mla-foldingXavier Leroy2017-09-152-0/+102
|\ \ | | | | | | Strength reduction patterns for ARM mla instruction.
| * | Strength reduction patterns for ARM mla instruction.Gergö Barany2017-09-152-0/+102
|/ /
* | Update the Cygwin x86-32 portXavier Leroy2017-09-121-10/+11
| | | | | | | | Some alignments were wrong. Follow-up to [4d099ef].
* | configure for x86-32/Cygwin: ignore __attribute__Xavier Leroy2017-09-111-1/+1
| | | | | | | | Even with __GNUC__ undefined, the standard header files contain bizarre __attribute__ declarations that CompCert fails to parse.
* | Resurrect the Cygwin x86-32 portXavier Leroy2017-09-112-2/+60
| | | | | | | | It got lost during the addition of the x86-64 port in release 3.0.
* | test/*/Makefile: suppress dependencies on ../../ccompXavier Leroy2017-09-112-6/+6
| | | | | | | | | | Not very useful in practice (make clean is generally done before make all) and problematic under Cygwin where ../../ccomp is really ../../ccomp.exe
* | Makefile: chmod a-w instead of chmod -wXavier Leroy2017-09-111-1/+1
| | | | | | | | | | The latter, in conjunction with some values of the umask, gives weird messages "new permissions are ... not ...".
* | Issue #199: improve namespace management for clightgen-produced filesXavier Leroy2017-08-282-16/+6
| | | | | | | | | | Qualify imports in clightgen-produced files and in Clightdefs so that they can be used with coq -Q /path/to/compcert compcert. Remove 'Require Export' from Clightdefs as suggested in issue #199.
* | For running tests with the interpreter, use the correct -stdlib optionXavier Leroy2017-08-281-3/+2
| | | | | | | | Otherwise the interpreter uses the system's header files instead of CompCert's. This can lead to mismatches e.g. on the definition of wchar_t.
* | test/compression: use unique temporary files for testingXavier Leroy2017-08-271-7/+7
| |
* | riscV/Conventions1: in 32-bit mode, wrong size for stack-allocated arguments ↵Xavier Leroy2017-08-261-2/+5
| | | | | | | | | | | | of type Tfloat A default size of 1 was used instead of the correct "typesize ty".
* | riscV/Machregs: no printable name was associated to register X31Xavier Leroy2017-08-261-1/+1
| |
* | test/ : stop at first error in "make all"Xavier Leroy2017-08-261-1/+1
| |
* | test/: add a CCOMPOPTS make variable to pass additional compile-time flagsXavier Leroy2017-08-265-5/+5
| | | | | | | | E.g. "-Os" for testing in "optimize for size" mode, or "-mthumb" for testing ARM in Thumb2 mode.
* | Reduce the running times of the tests in test/cXavier Leroy2017-08-2630-87/+75
| | | | | | | | Running times were too long when executed on low-end ARM or PowerPC hardware, or under QEMU emulation.
* | Prefixed runtime functions.Bernhard Schommer2017-08-2560-269/+269
| | | | | | | | | | | | | | The runtime functions are prefixed with compcert in order to avoid potential clashes with runtime/builtin functions of other compilers. Bug 22062
* | Document -finline in help.Bernhard Schommer2017-08-241-0/+1
| |
* | Fixed typo.Bernhard Schommer2017-08-241-1/+1
| |
* | Extended support for the nostartfiles option.Bernhard Schommer2017-08-231-6/+11
| | | | | | | | | | For dcc one needs to pass -Ws to tell the linker that it should not link the default startfiles.
* | ARM in Thumb mode: simpler instruction sequence for Pbtbl pseudo, continuedXavier Leroy2017-08-221-1/+2
| | | | | | | | A 16-bit "nop" is needed because in "add pc, r14" pc reads as the address of the add instruction plus 4, and "add pc, r14" has a 16-bit encoding.
* | ARM in Thumb mode: simpler instruction sequence for Pbtbl pseudoXavier Leroy2017-08-222-6/+7
| | | | | | | | It is also easier to recognize than the old one for binary analysis tools.
* | Issue P #25: make sure sizeof(long double) = sizeof(double) in all contexts.Xavier Leroy2017-08-222-10/+12
| |
* | Update documentation index for release 3.1v3.1Xavier Leroy2017-08-181-23/+17
| |
* | Merge remote-tracking branch 'private/master'Xavier Leroy2017-08-188-91/+201
|\ \
| * \ Merge pull request #22 from AbsIntPrivate/arm_large_offsetsXavier Leroy2017-08-188-91/+201
| |\ \ | | | | | | | | Issue #P18: handle large offsets when accessing return address and back link in the stack frame
| | * | ARM: tweak stack layout so that back link and return address are lowerXavier Leroy2017-08-171-37/+34
| | | | | | | | | | | | | | | | This reduces the chances that back link and return address cannot be saved by a single str instruction. We generate correct code for the overflow case, but the code isn't very efficient, so let's make it uncommon.
| | * | ARM port: replace Psavelr pseudo-instruction by actual instructionsXavier Leroy2017-08-176-47/+88
| | | | | | | | | | | | | | | | | | | | | | | | Saving the return address register (R14) in the function prologue can be done either with a single "str" instruction if the offset is small enough, or by constructing the address using the R12 register as a temporary then storing with "str" relative to R12. R12 can be used as a temporary because it is marked as destroyed at function entry. We just need to tell Asmgen.translcode whether R12 still contains the back link left there by Pallocframe, or R12 was trashed. In the latter case R12 will be reloaded from the stack at the next Mgetparam instruction.
| | * | Asmgenproof0: some more useful lemmasXavier Leroy2017-08-171-0/+29
| | | | | | | | | | | | | | | | Next commit uses those lemmas in the ARM port.
| | * | ARM: Generate Pcfi_rel_offset directives directly from AsmgenXavier Leroy2017-08-174-12/+17
| | | | | | | | | | | | | | | | This is what we do for PowerPC and is more resilient to changes in code generation. We need to give Pcfi_rel_offset a dynamic semantics, but that's just a no-op.
| | * | Push correct registerMichael Schmidt2017-08-021-1/+1
| | | |
generated by cgit (git 2.34.1) at 2024-07-03 14:06:28 +0000