aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* ça recompile sur x86David Monniaux2019-03-228-3/+127
|
* Merge branch 'mppa_postpass' into mppa-mulDavid Monniaux2019-03-223-8/+4
|\
| * try to be portable across archsDavid Monniaux2019-03-213-8/+4
| |
* | Merge branch 'mppa_postpass' into mppa-mulDavid Monniaux2019-03-201-7/+6
|\|
| * XLeroy's suggested fix for shared float/int register file.David Monniaux2019-03-201-3/+3
| |
| * Revert "Better fix for register allocation?"David Monniaux2019-03-201-4/+3
| | | | | | | | This reverts commit 5ad25465f77c3009eaff7e9a124c254c1e9f33cd.
* | Proof of div32/mod32/divf32/divf64 lemmasCyril SIX2019-03-201-3/+3
| |
* | la division flottante fonctionneDavid Monniaux2019-03-203-9/+12
| |
* | begin float divisionDavid Monniaux2019-03-201-3/+3
| |
* | Proving eval_divs_baseCyril SIX2019-03-202-2/+2
| |
* | added helper functions but strangeDavid Monniaux2019-03-194-89/+10
|/ | | | idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration
* Merge branch 'master' into mppa_postpassCyril SIX2019-03-131-6/+8
|\ | | | | | | | | | | Conflicts: .gitignore runtime/include/stdbool.h
| * Make the checker happy (#272)Vincent Laporte2019-02-121-6/+8
| | | | | | Previously, the coqchk type- and proof-checker would take forever on some of CompCert's modules. This commit makes minimal changes to the problematic proofs so that all of CompCert can be checked with coqchk. Tested with Coq versions 8.8.2 and 8.9.0.
* | Réactivé l'optim mulhs pour 32-bits (Omulhs n'est jamais généré)Cyril SIX2019-02-082-16/+16
| |
* | Désactivé toutes les optim division par constante --> Omulhs etc..Cyril SIX2019-02-082-26/+26
| |
* | Desactivated Omulhs 32-bits optimization (division by constant)Cyril SIX2019-02-082-8/+8
| |
* | Better fix for register allocation?Cyril SIX2019-02-061-3/+4
| |
* | compilation Asmexpandaux both for x86/ and mppa_k1c/Sylvain Boulmé2018-11-282-0/+9
| |
* | Compiles for x86 and mppa_k1c (except Asmexpandaux.ml)Sylvain Boulmé2018-11-272-9/+10
| |
* | BROKEN - works for x86, not for k1 anymoreCyril SIX2018-11-264-16/+7
| |
* | Merge tag 'v3.4' into mppa_k1cCyril SIX2018-11-2112-90/+245
|\| | | | | | | | | Conflicts: .gitignore
| * Simplified code. Bug 24067Bernhard Schommer2018-09-121-8/+8
| |
| * Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-122-3/+35
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Generate a nop instruction after ais annotations. In order to prevent the merging of ais annotations with following Labels a nop instruction is inserted, but only if the annotation is followed immediately by a label. The insertion of nop instructions is performed during the expansion of builtin and pseudo assembler instructions and is processor independent, by inserting a __builtin_nop built-in. * Add Pnop instruction to ARM, RISC-V, and x86 ARM as well as RISC-V don't have nop instructions that can be easily encoded by for example add with zero instructions. For x86 we used to use `mov X0, X0` for nop but this may not be as efficient as the true nop instruction. * Implement __builtin_nop on all supported target architectures. This builtin is not yet made available on the C side for all architectures. Bug 24067
| * Various improvements in the wording of diagnostics.Michael Schmidt2018-08-021-4/+4
| | | | | | | | | | | | Fix various typos in diagnostic messages and unified wording and capitalization. Bug 23850
| * Treat Outgoing stack slots as caller-save in LTL/Linear semantics (#237)Xavier Leroy2018-06-176-93/+145
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Outgoing stack slots are set to Vundef on return from a function call, modeling the fact that the callee could write into those stack slots. (CompCert-generated code does not do this, but code generated by other compilers sometimes does.) * Adapt Stackingproof to this new semantics. This requires tighter reasoning on how Linear's locsets are related at call points and at return points. * Most of this reasoning was moved from Stackingproof to Lineartyping, because it can be expressed purely in terms of the Linear semantics, and tracked through the wt_state predicate. * Factor out and into Conventions.v: the notion of callee-save locations, the "agree_callee_save" predicate, and useful lemmas on Locmap.setpair. Now the same "agree_callee_save" predicate is used in Allocproof and in Stackingproof.
| * Model external calls as destroying all caller-save registersXavier Leroy2018-06-018-8/+79
| | | | | | | | | | | | | | | | | | | | The semantics of external function calls in LTL, Linear, Mach and Asm now consider that all caller-save registers are set to Vundef by the call. This models that fact that the external function can modify those registers arbitrarily. Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes accordingly.
* | Extraction issueCyril SIX2018-09-061-7/+9
| |
* | MPPA - refactored instructionsCyril SIX2018-05-112-7/+7
| |
* | MPPA - Started Asm.v + Asmgen.v, commenting out some instructionsCyril SIX2018-04-041-1/+3
| |
* | MPPA - Machregs + Conventions1 + backend proof tweakingCyril SIX2018-04-042-2/+7
|/
* Add newline directly on list in annot.Bernhard Schommer2018-03-132-4/+7
| | | | | | | This should avoid cluttering the assembler output with .ascii "\n" lines if the annotation ends with a string and make for a better readability. Bug 23169
* Print size argument of Init_space as Z not as int32Xavier Leroy2018-03-131-1/+1
| | | | | Init_space has an argument of type Z and it can exceed the range of a 32-bit integer. Reported by Frédéric Besson.
* Introduce more brackets for register annotation.Bernhard Schommer2018-03-121-4/+5
| | | | | | It seems necessary that the mulitplication for the high part of split registers is put into brackets. Bug 23169
* Do not use "Require" inside sections (#224)Xavier Leroy2018-03-121-3/+1
| | | | | | This will soon be deprecated by Coq. Manual merge of pull request #224 by vbgl. Closes: #224
* Added seperator in warning msg. Bug 23179Bernhard Schommer2018-03-091-1/+1
|
* Do not use default printer for variable names.Bernhard Schommer2018-03-091-2/+8
| | | | | | Printing variable names with the default expression printer results in newlines in the outputed error message. Bug 23169
* Perform quoting for json.Bernhard Schommer2018-03-081-1/+8
| | | | | | The strings for json need quoting of special characters such as \" and \\. Bug 22438
* Print symbols as symbols.Bernhard Schommer2018-03-082-4/+26
| | | | | | This allows us to replacing them by their address in valex and additionally checking them. Bug 22438
* Improve error messages.Bernhard Schommer2018-03-071-16/+14
| | | | | | | | Include the format specifier in error message when available in order to make it easier to spot the broken ais parameter. Futhermore introduce a new warning for unused ais parameters. Bug 22464
* Reword error message. Fix 22464Bernhard Schommer2018-03-071-2/+2
|
* Improve wording.Bernhard Schommer2018-03-071-1/+1
| | | | | Mention that it is a global memory cell. Fix 22464
* Improve and simplify error messages.Bernhard Schommer2018-03-072-31/+54
| | | | | | | | The checks on the argument and format arguments are now performed during C2C translation by calling the validate_ais_annotations function and result in an error instead of a warning in the backend to be more consistent with the rest of the builtin functions.
* Reactivated and improved ais annotations.Bernhard Schommer2018-03-064-22/+204
| | | | | | | | | | | | | | | | | | The ais annotations are now handled in a separate file shared between all architectures. Also two different variants of replacements are supported, %e which expands to ais expressions and %l which also expands to an ais expression but is guaranted to be usable as l-value in the ais annotation. Otherwise the new warning is Wrong_is_parameter is generated. Also an error message is generated if floating point variables are used in ais annotations since a3 does not support them at the moment. Additionally an error message is generated for plain volatile variables used, since they will enforce a volatile load and result in the value being passed to the annotation instead of the address as other global variables.
* Change AsmToJson to be similar to other printers.Bernhard Schommer2018-01-052-1/+33
|
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-053-0/+249
| | | | | | | | | | | Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent. This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed. Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST which is not in lib/
* ValueAnalysis: remove duplicate list_forall2_in_left (#212)Jérémie Koenig2018-01-031-13/+2
| | | The lemma is now in lib/Coqlib.v.
* Introduce and use C2C.atom_inline function with 3-valued resultXavier Leroy2017-12-081-3/+6
| | | | | | Instead of two Boolean tests C2C.atom_is_{no,}inline, have a single C2C.atom_inline function that returns one of the three possible values stored in the the a_inline field.
* Remove unused code. BUg 22642Bernhard Schommer2017-12-081-2/+2
|
* Store the different inlining cases.Bernhard Schommer2017-12-081-2/+2
| | | | | | | In order to correctly support the noinline attribute we must store whether the function was specified with an inline specifer, had a noinline attribute or nothing. Bug 22642
* Do not inline varag functions. Bug 22642Bernhard Schommer2017-12-071-3/+3
|
generated by cgit (git 2.34.1) at 2024-07-12 04:17:20 +0000