aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* add version.h, prims.cDavid Monniaux2019-06-063-1/+1160
|
* Merge branch 'mppa-work' of ↵David Monniaux2019-06-051-1/+1
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * Fix for #134 Pjumptable not recognizedCyril SIX2019-06-051-1/+1
| |
* | disable large benchmarks that rely on heap saturation and other limitsDavid Monniaux2019-06-052-10/+14
|/
* fixed reservation table for cmoveDavid Monniaux2019-06-051-1/+5
|
* move with immediatesDavid Monniaux2019-06-042-1/+31
|
* osel immDavid Monniaux2019-06-048-23/+117
|
* begin osel immDavid Monniaux2019-06-043-3/+57
|
* added immediate cmoveDavid Monniaux2019-06-046-38/+80
|
* shortcuts for cmoveDavid Monniaux2019-06-043-21/+41
|
* shortcut cmove worksDavid Monniaux2019-06-042-89/+7
|
* why doesn't it work?David Monniaux2019-06-042-7/+265
|
* little restructuringDavid Monniaux2019-06-041-3/+4
|
* keep the .s filesDavid Monniaux2019-06-041-0/+2
|
* remove old "ternary" stuffDavid Monniaux2019-06-045-47/+10
|
* start to have whole path if-conversion?David Monniaux2019-06-043-3/+18
|
* Osel -> assembleurDavid Monniaux2019-06-043-104/+112
|
* Osel is output = 1st inputDavid Monniaux2019-06-041-0/+1
|
* Osel operation (not yet compiled)David Monniaux2019-06-043-31/+39
|
* rm old select/selectl/selectf/selectfsDavid Monniaux2019-06-0314-914/+47
|
* Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-03158-9521/+14486
|\ | | | | | | mppa-if-conversion
| * ARM: select is not supported at type TlongXavier Leroy2019-06-013-4/+14
| |
| * If-conversion optimizationXavier Leroy2019-05-3110-75/+746
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches.
| * Type inference and type checking for CminorXavier Leroy2019-05-312-1/+799
| | | | | | | | | | | | | | This module is similar to RTLtyping: it performs type inference and type checking, but on the Cminor intermediate representation rather than the RTL IR. For each function, it returns a mapping from variables to types. Its first use will be if-conversion optimization.
| * Additional simulation diagrams for determinate source languagesXavier Leroy2019-05-311-0/+173
| | | | | | | | | | If the source language is determinate, it can take several steps (not just one) before the "match_state" invariant is reinstated.
| * Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-3121-31/+31
| | | | | | | | | | | | This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream.
| * Provide a float select operation for PowerPC. (#173)Bernhard Schommer2019-05-289-7/+101
| | | | | | | | | | | | The FP select for PowerPC stores both addresses in two subsequent stack slots and loads them using an offset created from the result of the comparison.
| * PowerPC: add SelectOp.select functionXavier Leroy2019-05-262-0/+31
| | | | | | | | | | This function and its proof should have been part of commit 43e7b67. They are already there for the other ports.
| * ARM: Fix expansion of FP conditional moveXavier Leroy2019-05-261-2/+2
| | | | | | | | | | The "vmov" instruction (Advanced SIMD) cannot be conditional. The "vmov.f64" instruction (VFPv2) can be conditional.
| * Coq 8.9.1 supportXavier Leroy2019-05-211-3/+3
| | | | | | | | It works fine with the current sources.
| * Csyntax.v: Fix a typo in a documentation comment (#292)Bart Jacobs2019-05-211-1/+1
| |
| * Add a check for the args of unprototyped calls.Bernhard Schommer2019-05-201-3/+8
| | | | | | | | | | | | The arguments that are passed to an unprototyped function must also be checked to be valid types passed to a function, i.e. they must be complete types after argument conversion.
| * Provide a default "select" operation for the RiscV portXavier Leroy2019-05-202-0/+20
| | | | | | | | | | No `Osel` operation for this port, so `SelectOp.select` always returns None.
| * Implement a `Osel` operation for ARMXavier Leroy2019-05-2012-7/+115
| | | | | | | | | | The operation comples down to conditional moves. Both integer and floating-point conditional moves are supported.
| * Implement a `Osel` operation for x86Xavier Leroy2019-05-2011-38/+298
| | | | | | | | The operation compiles down to conditional moves.
| * Emulate the "isel" instruction on non-EREF PPC processorsXavier Leroy2019-05-203-22/+42
| | | | | | | | | | On non-EREF processors it expands to instructions that destroy GPR0. Reflect this in the Asm semantics for Pisel.
| * Implement a `Osel` operation for PowerPCXavier Leroy2019-05-207-9/+106
| | | | | | | | | | This operation compiles down to an `isel` instruction (conditional move). The semantics is given by `Val.select`.
| * Give a semantics to the Pisel instructionXavier Leroy2019-05-201-1/+7
| |
| * Support a "select" operation between two valuesXavier Leroy2019-05-203-0/+212
| | | | | | | | | | | | | | | | | | | | `Val.select ob v1 v2 ty` is a conditional operation that chooses between the values `v1` and `v2` depending on the comparison `ob : option bool`. If `ob` is `None`, `Vundef` is returned. If the selected value does not match type `ty`, `Vundef` is returned. This operation will be used to model a "select" (or "conditional move") operation at the CminorSel/RTL/LTL/Mach level.
| * PowerPC: make sure evaluation of conditions do not destroy any registerXavier Leroy2019-05-204-54/+155
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This will be useful to implement a "select" (conditional move) operation later. - Introduce `Asmgen.loadimm64_notemp` to load a 64-bit integer constant into a register without going through memory and without needing a temporary register. - Use `Asmgen.loadimm64_notemp` instead of `Asmgen.loadimm64` in the compilation of conditions, so that GPR12 is no longer needed as a temporary. - Share code and proofs common to the two `Asmgen.loadimm64_` functions as the `Asmgen.loadimm64_32s` function.
| * Prepend $(DESTDIR) to the installation target (#169)Bernhard Schommer2019-05-172-16/+16
| | | | | | | | | | | | | | | | Following the gnu Makefile Conventions the variable $(DESTDIR) should be prepended to all installation commands. This allows staged installs.
| * Reworked elaboration of declarations/definitions.Bernhard Schommer2019-05-101-140/+138
| | | | | | | | | | | | | | | | | | | | | | | | Since a definition/declaration is completed with after the separator to the next init group member it is also possible to use it for example in the next init group member: char s[]="miaou", buf[sizeof s]; In order to ensure that this works the declarations are added to the environment directly during the elaboration of the init member group instead of later.
| * Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-108-15/+41
| | | | | | | | | | | | | | | | | | | | The option -fcommon controls whether uninitialized global variables are placed in the COMMON section. If the option is given in the negated form, -fno-common, variables are not placed in the COMMON section. They are placed in the same sections as gcc does. If the variables are not placed in the COMMON section merging of tentative definitions is inhibited and multiple definitions lead to a linker error, as it does for gcc.
| * Change to AbsInt version string.Bernhard Schommer2019-05-105-6/+6
| | | | | | | | | | The AbsInt build number no longer contains "release", so it must be printed additionally.
| * Check for reserved keywords.Bernhard Schommer2019-05-101-1/+8
| | | | | | | | | | | | `_Complex` and `_Imaginary` are reserved keywords. Since CompCert does not support these types they could be used as identifiers. However the standard requires to reject this.
| * Fix various scoping issues (#163)Bernhard Schommer2019-05-101-51/+56
| | | | | | | | | | | | | | | | | | Pass the environment to all expr eval functions since the functions themselve may be called recursively and modify the environment. The other change introduces new scopes that are strict subsets of their surrounding scopes for if, switch, while, do and for statement, as prescribed by ISO C standards.
| * Ensure flushing of the error formatter.Bernhard Schommer2019-05-101-0/+4
| | | | | | | | | | Since the error formatter is not automatically flushed at program exit we need to ensure that it is flushed at exit.
| * Expand the responsefiles earlierBernhard Schommer2019-05-105-17/+17
| | | | | | | | | | | | | | | | | | * Move the expansion of response files to module Commandline, during the initialization of `Commandline.argv`. This way we're sure it's done exactly once. * Make `Commandline.argv` a `string array` instead of a `string array ref`. We no longer need to update it after initialization! * Improve reporting of errors during expansion of response files.
| * Check for alignment of command-line switches.Bernhard Schommer2019-05-102-6/+10
| | | | | | | | | | | | Add a check for alignment on command-line switches `-falign-*`. The check is similar to the one for the alignment attribute and ensures that only powers of two can be specified.
| * More efficient test for powers of twoXavier Leroy2019-05-092-26/+105
| | | | | | | | | | | | The previous implementation used to build the full powers-of-two decomposition of the number. The present implementation recognizes powers of two directly, then takes the log2.
generated by cgit (git 2.34.1) at 2024-07-11 23:14:26 +0000