aboutsummaryrefslogtreecommitdiffstats
path: root/driver
Commit message (Collapse)AuthorAgeFilesLines
* -fpostpass-ilpDavid Monniaux2019-03-122-4/+0
|
* Merge branch 'mppa_postpass' of ↵David Monniaux2019-03-122-0/+4
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * Added cascaded_scheduler but the flag does not workCyril SIX2019-03-121-2/+3
| |
| * Added a flag for changing the scheduler (not any choice available right now)Cyril SIX2019-03-123-0/+6
| |
* | -fpostpass-ilpDavid Monniaux2019-03-122-0/+3
|/
* Added long double = double by default on Kalray architectureCyril SIX2019-03-011-1/+1
|
* -O0 will not perform postpass schedulingCyril SIX2019-01-183-1/+7
|
* Compiles for x86 and mppa_k1c (except Asmexpandaux.ml)Sylvain Boulmé2018-11-271-1/+1
|
* BROKEN - works for x86, not for k1 anymoreCyril SIX2018-11-261-1/+1
|
* Moved some files to mppa_k1c/lib ; reworked configure and Makefile to allow thatCyril SIX2018-11-261-322/+0
|
* Merge tag 'v3.4' into mppa_k1cCyril SIX2018-11-219-93/+202
|\ | | | | | | | | Conflicts: .gitignore
| * Fix passing of -u to linker.Bernhard Schommer2018-08-211-1/+1
| | | | | | | | | | | | Instead of just passing -u to the linker also pass the value of the option to the linker. Bug 24316
| * Add sizeof_reg and new Machine configurations (#129)Bernhard Schommer2018-08-201-4/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | Since the size of integer registers is not identical to the size of pointers for the ppc64 and e5500 model the check for register pairs in ExtendedAsm does not work correctly. In order to avoid this a new field sizeof_intreg is introduced in the Machine configuration which describes the size of integer registers. New configurations for the ppc64 and e5500 model are added and used. Bug 24273
| * Various improvements in the wording of diagnostics.Michael Schmidt2018-08-026-12/+12
| | | | | | | | | | | | Fix various typos in diagnostic messages and unified wording and capitalization. Bug 23850
| * Typo in -iquote preprocessing option (#239)Frédéric Besson2018-06-201-1/+1
| | | | | | The `-iquote` option was passed to the GNU preprocessor as `-iquore`
| * Simplify module Complements and add separate compilation (#121)Xavier Leroy2018-05-291-74/+172
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Simplify the theorems about preservation of specifications (section 2) There were three theorems, transf_c_program_preserves_spec, _safety_spec, and _liveness_spec) with the first being needlessly general and the last being hard to understand. Plus, the "liveness" and "safety" terminology wasn't very good. Replaced by two theorems: - transf_c_program_preserves_spec, which is the theorem previously named _safety_spec and talks about specifications that exclude going-wrong behaviors; - transf_c_program_preserves_initial_trace, which is an instance of the theorem previously named _liveness_spec, and now talks about a single initial trace of interest rather than a set of such traces. Added named definitions for properties of interest. Added more explanations. * Added theorems that talk about separate compilation (section 3) These are the theorems from section 1 and 2 but reformulated in terms of multiple C source compilation units being separately compiled to Asm units then linked together.
| * Define C11 conditional feature macros (#77)Bernhard Schommer2018-04-061-1/+10
| | | | | | | | | | | | | | | | These macros can be defined to indicate that variable length arrays, the _Complex type, atomics and threads are not supported. Since the _Complex type is not supported, we also need to undefine __STDC_IEC_559_COMPLEX__ Bug 23408
* | Rajout d'un return_address_offset. Besoin de changer forward_simu de mach ↵Cyril SIX2018-09-061-1/+1
| | | | | | | | machblock
* | Machblock: some renaming and proof simplificationsCyril SIX2018-09-061-15/+15
| |
* | Machblock: adaptation to the generalized ForwardSimulationBlockSylvain Boulmé2018-09-061-8/+103
| |
* | Generalization of ForwardSimulationBlockSylvain Boulmé2018-09-061-33/+24
| |
* | Machblock: Mach language with basic blocksCyril SIX2018-09-061-0/+236
| |
* | Hook for MPPA_K1c (generates Risc-V code for now)Cyril SIX2018-04-042-1/+2
|/
* Removed struct passing/return from ConfigurationsBernhard Schommer2018-02-162-49/+0
|
* Move struct passing/return style to Machine.Bernhard Schommer2018-02-161-1/+5
| | | | | | Since the used configuration for passing and returning values struct values is pretty much static it can be hardwired into the machine settings.
* Added error summary in case of fatal error.Bernhard Schommer2018-02-091-1/+1
|
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-088-70/+64
| | | | | | | | | | | | | | | | | * Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/ * Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the Diagnostics module. * Raise on error before calling external tools. * Added diagnostics to clightgen. * Fix error handling of AsmToJson. * Cleanup error handling of Elab and C2C. *The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
* Share code for common options.Bernhard Schommer2018-01-292-61/+105
| | | | | | In order to avoid more divergence between the command line options of clightgen and ccomp the code for the common options, the language support options, the version string and the general options.
* Move machine initialization to Frontend.init function. (#49)Bernhard Schommer2018-01-113-22/+29
| | | | | The initialization of Machine.config, as well as the calls to various initialization functions for the C front-end, are now performed by the new `Frontend.init` function. This avoids code duplication in driver/Driver.ml and exportclight/Clightgen.ml.
* Change AsmToJson to be similar to other printers.Bernhard Schommer2018-01-051-45/+3
|
* Added toolchain specific option for dcc. (#47)Bernhard Schommer2018-01-051-1/+16
| | | | | | CompCert now accepts the target configuration option of the diab data compiler and passes it on to the preprocessor, assembler and linker. Bug 20521
* Handle dcompcertc and dparsedc like all dump opts.Bernhard Schommer2018-01-042-13/+5
| | | | | This time with the correct place for setting the destination files. Bug 20521
* Remove duplicated code. Bug 20521Bernhard Schommer2018-01-041-46/+26
|
* Remove all temporary files at program exit (#46)Bernhard Schommer2018-01-033-18/+16
| | | | | | | | | Replaced calls to Filename.temp_file by own version Driveraux.tmp_file. The Driveraux.tmp_file function takes care that the temporary files are removed at exit. Consequently there is no need to explicitly remove temp files in Driver.
* Export configured architecture to JSON (#38)Michael Schmidt2017-12-131-0/+6
| | | The architecture which was configured is now exported in a new top-level json field.
* Inlining of static functions which are only called once. (#37)Bernhard Schommer2017-12-072-1/+5
| | | | | | | | | 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.
* 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.
* New support for inserting ais-annotations.Bernhard Schommer2017-10-192-0/+5
| | | | | | | | | | | | 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.
* 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
* Added dump-mnemonics option.Bernhard Schommer2017-09-251-2/+12
| | | | | | This option allows it to dump a list of all used mnemonics into a file. Bug 22239
* Take advantage of ARMv6T2/ARMv7 instructions even if not in Thumb2 mode (#203)Gergö Barany2017-09-181-3/+7
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * 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
* Document -finline in help.Bernhard Schommer2017-08-241-0/+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.
* Formatted json printing.Bernhard Schommer2017-06-281-8/+23
| | | | | | | | | Instead of just dumping the json output it is now a little bit formatted for better reading. Furthermore the AsmToJson function for the non powerpc targets now prints the json value "null" sucht that the resulting json file is valid json.
* Added a little bit more compilation info to sdump.Bernhard Schommer2017-06-263-4/+16
| | | | | | The additional compilation information contains the file, command line (after @-file expansion) and the current working directory. Bug 21690
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-032-7/+7
| | | | | | | | | | | | | This commit adds code generation for 64bit PowerPC architectures which execute 32bit applications. The main difference to the normal 32bit PowerPC port is that it uses the available 64bit instructions instead of using the runtime library functions. However pointers are still 32bit and the 32bit calling convention is used. In order to use this port the target architecture must be either in Server execution mode or if in Embedded execution mode the high order 32 bits of GPRs must be implemented in 32-bit mode. Furthermore the operating system must preserve the high order 32 bits of GPRs.
* RISC-V port and assorted changesXavier Leroy2017-04-282-1/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes. The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/ This port required the following additional changes: - Integers: More properties about shrx - SelectOp: now provides smart constructors for mulhs and mulhu - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu. - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library. - test/: add SIMU make variable to run tests through a simulator - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers commit da14495c01cf4f66a928c2feff5c53f09bde837f Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Thu Apr 13 17:36:10 2017 +0200 RISC-V port, continued Now working on Asmgen. commit 36f36eb3a5abfbb8805960443d087b6a83e86005 Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Wed Apr 12 17:26:39 2017 +0200 RISC-V port, first steps This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.
* Add optimization option finline.Bernhard Schommer2017-04-072-0/+2
| | | | | | The new option f(no-)inline controlls whether inlining is active or not. Bug 21343.
* Added missing dltl to dall.Bernhard Schommer2017-03-081-0/+1
|
* Merge pull request #167 from AbsInt/pipe_prerequisiteXavier Leroy2017-02-157-28/+21
|\ | | | | Introduced configuration variable for gnu systems.
generated by cgit (git 2.34.1) at 2024-07-06 17:30:15 +0000