aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Fix check-proof target of the Makefile after merge of Coq #6277.Pierre-Marie Pédrot2017-12-071-1/+1
| | | | We simply fully qualify the modules. This is backward compatible.
* Inlining of static functions which are only called once. (#37)Bernhard Schommer2017-12-077-13/+105
| | | | | | | | | New inlining heuristic for static functions. Static functions that are only called once can always be inlined, since they can be removed safely after inlining and no call prologue, epilogue, as well as register saving and needs to be generated.
* Optimization for division by one during constant propagation (#39)Michael Schmidt2017-12-058-36/+85
| | | | Signed and unsigned divisions by literal 1 are already optimized away during the Selection phase. This pull request also optimizes those divisions when the 1 divisor is produced by constant propagation.
* Added simple div_one Theorem variants.Bernhard Schommer2017-12-012-0/+40
|
* Remove unused float_abi_type.Bernhard Schommer2017-11-291-12/+0
|
* Merge branch 'master' of github.com:AbsIntPrivate/CompCertBernhard Schommer2017-11-270-0/+0
|\
| * Remove temporary .o files after linking (#36)Xavier Leroy2017-11-271-2/+5
| | | | | | | | | | | | | | When -c is not given, .o files are now generated in /tmp, but they are still not erased. This commit uses an "at_exit" action to erase those temporary .o files before CompCert exits. Using at_exit is easier to implement than explicit erasure (like we do for other temporary files), yet should not result in temporary files lingering in /tmp longer than strictly necessary, since the call to the linker is the last thing that CompCert does before exiting, hence temporary .o files are erased just after the linker returns.
* | Remove temporary .o files after linking (#36)Xavier Leroy2017-11-271-2/+5
|/ | | | | | | When -c is not given, .o files are now generated in /tmp, but they are still not erased. This commit uses an "at_exit" action to erase those temporary .o files before CompCert exits. Using at_exit is easier to implement than explicit erasure (like we do for other temporary files), yet should not result in temporary files lingering in /tmp longer than strictly necessary, since the call to the linker is the last thing that CompCert does before exiting, hence temporary .o files are erased just after the linker returns.
* Issue #208: make value analysis of comparisons more conservative w.r.t. ↵Xavier Leroy2017-11-242-8/+15
| | | | | | | pointers (#209) Comparisons such as "(uintptr_t) &global == 0x1234" are undefined behavior in CompCert but their status in ISO C is unclear and they may occur in real-world code. Make sure they are statically analyzed as Btop.
* Pull request #192: improve the printing of Clight intermediate codeXavier Leroy2017-11-223-10/+29
| | | | So that it looks more like valid C source.
* Added json export for the abstract ARM AssemblerBernhard Schommer2017-11-202-64/+338
| | | | | | | The json export for the abstract ARM Assembler is quite similar to it's PowerPC equivalent expect for the different instruction arguments. Bug 22472
* Moved arm eabi fixup to Asmexpand.Bernhard Schommer2017-11-163-159/+229
| | | | | | | | Instead of expanding the fixup code for incoming and outgoing registers in the TargetPrinter we expand them in Asmexpand. This simplifies the estimate size function and is a prerequisite for the json export. Bug 22472
* New json printing interface.Bernhard Schommer2017-11-144-144/+208
| | | | | The common json export functionallity is moved into an own File. Bug 22472
* Remove no longer used function. Bug 22525Bernhard Schommer2017-11-105-8/+0
|
* Removed no longer used function. Bug 22525Bernhard Schommer2017-11-095-105/+1
|
* Use address for printing address constant. Bug 22525Bernhard Schommer2017-11-091-2/+3
|
* Generalize print_init.Bernhard Schommer2017-11-091-1/+40
| | | | | | The powerpc version of print_init can be used without problems for all backends. Bug 22525
* Fix jumptable issue.Bernhard Schommer2017-11-084-5/+8
| | | | | | Instead of using reset_constants use reset_literals which avoids emptying the jumptables. Bug 22525
* Simplifiy handling of constant emmitting.Bernhard Schommer2017-11-084-92/+71
| | | | | | Instead of just storing the constants in a list, they are now stored in a hashtable. This avoids printing of duplicates. Bug 22525
* Remove superfluous function.Bernhard Schommer2017-11-066-11/+2
| | | | | The new_label function is alway equal to PrintAsmaux.new_label. Bug 22472
* Also quote \a.Bernhard Schommer2017-10-261-0/+2
| | | | | | This allows for an easier replacement of the binary address and avoids that the user specifies his own binary addresses. Bug 22468
* Fix register name of ais printing and moved label function up.Bernhard Schommer2017-10-251-4/+4
|
* Remove ais_annot_intval.Bernhard Schommer2017-10-241-13/+0
|
* Prefix ais annotations with location.Bernhard Schommer2017-10-241-2/+4
| | | | | | The file and line information are now stored as comment string at the start of each annotation. Bug 22462
* 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
generated by cgit (git 2.34.1) at 2024-07-03 04:42:28 +0000