aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
Commit message (Collapse)AuthorAgeFilesLines
* Check for alignment of command-line switches.Bernhard Schommer2019-05-101-3/+7
| | | | | | 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.
* Various improvements in the wording of diagnostics.Michael Schmidt2018-08-021-1/+1
| | | | | | Fix various typos in diagnostic messages and unified wording and capitalization. Bug 23850
* 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-081-26/+20
| | | | | | | | | | | | | | | | | * 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-291-61/+16
| | | | | | 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-111-22/+1
| | | | | 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-041-1/+3
| | | | | 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-031-18/+6
| | | | | | | | | 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-071-1/+4
| | | | | | | | | 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.
* 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
|
* 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-261-2/+9
| | | | | | The additional compilation information contains the file, command line (after @-file expansion) and the current working directory. Bug 21690
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-071-0/+1
| | | | | | 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 #170 from AbsInt/remove_cminorXavier Leroy2017-02-151-65/+0
|\ | | | | | | | | | | Remove CompCert's ability to parse and compile source files written in Cminor This facility is no longer used (as far as we know) and is painful to maintain.
| * Removed CMinor import. Bug 20992Bernhard Schommer2017-02-141-65/+0
| |
* | Removed superfluous semicolon.Bernhard Schommer2017-02-141-1/+1
|/
* Remove Optionsprinter. Bug 20993Bernhard Schommer2017-02-141-14/+1
|
* Refactor the classification of attributesXavier Leroy2017-02-031-0/+1
| | | | | | | | | | | | | | | Introduce Cutil.class_of_attribute to return the class of the given attribute: one among Attr_type attribute related to types (e.g. "aligned") Attr_struct attribute related to struct/union/enum types (e.g. "packed") Attr_function attribute related to function types (e.g. "noreturn") Attr_name attribute related to variable and function declarations (e.g. "section") Attr_unknown attribute was not declared Cutil.declare_attribute is used to associate a class to a custom attribute. Standard attributes (const, volatile, _Alignas, etc) are Attr_type. cfronted/C2C.ml: declare the few attributes that CompCert honors currently. cparser/GCC.ml: a bigger list of attributes taken from GCC, for reference only.
* Fixed indention of help.Bernhard Schommer2017-01-271-3/+3
|
* Allow .sx files for preprocessed assembler files.Bernhard Schommer2017-01-251-0/+3
| | | | | GCC treats files with .sx extension in the same way as it treats files with .S suffix.
* Use quoted strings.Bernhard Schommer2017-01-181-74/+79
| | | | | | Instead of escaping all newlines etc for the help options use quoted strings. Bug 19872
* Added backtrace handler.Bernhard Schommer2017-01-171-0/+2
| | | | | | | | If CompCert crashes because of an uncaught exception the exception is caught toplevel and the backtrace is printed plus an additional message to include the backtrace in a support request, if buildnr and tag are available. Bug 20681.
* add parameter to enforce a specific compcert build number for QSKs (bug 20595)Michael Schmidt2016-12-161-2/+14
|
* Also exit on errors. Bug 19872Bernhard Schommer2016-12-151-1/+1
|
* Check errors at the end. Bug 19872Bernhard Schommer2016-12-151-0/+1
|
* Merge pull request #145 from AbsInt/64Xavier Leroy2016-10-271-3/+6
|\ | | | | | | Support for 64-bit target processors + support for x86 in 64-bit mode
| * Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵Xavier Leroy2016-10-271-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | -> x86/x86_32/x86_64 Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq. This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86. While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures. Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
| * Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-3/+6
| | | | | | | | | | | | | | | | | | | | | | - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
* | Document -target and -conf. Bug 20210Bernhard Schommer2016-10-181-0/+2
| |
* | Refactored debugging options.Bernhard Schommer2016-10-141-28/+5
| | | | | | | | | | | | | | The options controlling the generation of debugging information are now moved into the Debug module. Futhermore the -gdepth options are replaced in favor of a more gcc compatible version. Bug 20193
* | Remove undocumented option. Bug 20193Bernhard Schommer2016-10-141-6/+2
| |
* | Fix minor typoMichael Schmidt2016-10-121-1/+1
|/
* Merge pull request #139 from AbsInt/advanced-diagnosticsBernhard Schommer2016-09-201-31/+34
|\ | | | | Advanced diagnostics
| * Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-291-2/+17
| |\
| * | Additional test for color output.Bernhard Schommer2016-08-051-26/+27
| | | | | | | | | | | | | | | | | | Color output is only enabled if stderr is a tty, and the environment variable TERM is not empty or dumb. Bug 18004
| * | Classified all warnings and added various options.Bernhard Schommer2016-07-291-5/+7
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now each warning either has a name and can be turned on/off, made into an error,etc. or is a warning that always will be triggered. The message of the warnings are similar to the ones emited by gcc/clang and all fit into one line. Furthermore the diagnostics are now colored if colored output is available. Bug 18004
* | | Added option to specify sdump folder. Fix 19816.Bernhard Schommer2016-09-161-2/+7
| |/ |/|
* | fix merge conflictsMichael Schmidt2016-08-171-0/+1
|\ \
| * \ Merge pull request #107 from AbsInt/add-fileXavier Leroy2016-08-171-0/+1
| |\ \ | | | | | | | | Add support for response files
| | * | Added responsefile support for commandline.Bernhard Schommer2016-07-081-0/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Commandline can now be passed in a file specifed with @file on the Commandline. The quoting convention is similar to the one used by gcc, etc. Options are separated by whitespaces and options with whitespaecs need to be quoted. Bug 18303
generated by cgit (git 2.34.1) at 2024-06-29 14:20:47 +0000