aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
Commit message (Collapse)AuthorAgeFilesLines
* Changed cc_varargs to an option typeBernhard Schommer2020-12-251-2/+2
| | | | | | Instead of being a simple boolean we now use an option type to record the number of fixed (non-vararg) arguments. Hence, `None` means not vararg, and `Some n` means `n` fixed arguments followed with varargs.
* Add `string_of_ident` conversionXavier Leroy2020-10-121-0/+110
| | | | | | This is the left inverse of `ident_to_string`. Closes: #372
* Use exact arithmetic for printing positive numbersXavier Leroy2020-09-221-52/+56
| | | | | | And also for the computations in name_temporary. Overflowing OCaml's integer types is unlikely in actual use but happened in the past owing to another mistake (see issue #370).
* Fix computation of next temporary in -canonical-idents modeXavier Leroy2020-09-221-1/+12
| | | | | | | Variables were confused for temporaries, causing the temporaries introduced by this pass to be very big integers. Fixes: #370
* Introduce additional "branch" build information.Bernhard Schommer2020-07-081-0/+1
|
* clightgen: fix the printing of annotationsXavier Leroy2020-06-051-59/+8
| | | | | | | | | | | | The printing of EF_annot and EF_annot_val was missing the extra "kind" parameter introduced in commit 6a010b4. Also: the automatic translation of annotations into Coq assertions was confusing and prevented other uses of __builtin_annot statements in conjunction with clightgen. I believe it was never used. This commit removes this translation. Closes: #360
* clightgen: fix usage messageXavier Leroy2020-06-011-2/+2
| | | | Closes: #358
* clightgen -short-idents : do not use $"xxx" notation everXavier Leroy2020-06-011-1/+1
| | | | | | | | In the original code, collisions could occur: an identifier could be numbered with a number that happens to be equal to its canonical encoding. This was harmless but confusing. Closes: #358
* Add a canonical encoding of identifiers as numbers and use it in clightgen ↵Xavier Leroy2020-05-193-17/+128
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (#353) Within CompCert, identifiers (names of C functions, variables, types, etc) are represented by unique positive numbers, sometimes called "atoms". In the original implementation, atoms 1, 2, ..., N are assigned to identifiers as they are encountered. The resulting number are small and are efficient when used as keys in data structures such as PTrees. However, the mapping from C source-level identifiers to atoms differs between compilation units. This is not a problem for CompCert but complicates CompCert-based verification tools that need to combine several compilation units. This commit introduces an alternate implementation of atoms, suggested by Andrew Appel. The choice between implementations is governed by the Boolean reference `Camlcoq.use_canonical_atoms`. In the alternate implementation, identifiers are converted to bit sequences via a Huffman encoding, then the bits are represented as positive numbers. The same identifier is always represented by the same number. However, the numbers are usually bigger than in the original implementation, making PTree operations slower: lookups and updates take time linear in the length of the identifier, instead of logarithmic time in the number of identifiers encountered. The CompCert compiler (the `ccomp` executable) still uses the original implementation, but the `clightgen` tool used in conjunction with the VST program logic can use either implementations: - The alternate "canonical atoms" implementation is used by default, and also if the `-canonical-idents` option is given. - The original implementation is used if the `-short-idents` option is given. Closes: #222 Closes: #311
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-2/+10
| | | | | | | | | | Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions.
* clightgen: sanitize names of functions and global variablesXavier Leroy2019-10-281-4/+4
| | | | | A "dollar" sign in a function name or a global variable name was producing incorrect Coq identifiers. (Issue #319.)
* clightgen -dclight: print function parameters correctlyXavier Leroy2019-09-161-1/+1
| | | | | | | | | | | | | The Clight output of clightgen is Clight version 2, after SimplLocals conversion, where function parameters are temporary variables, not variables. This commit makes sure the function parameters are printed as temporary variables and not as variables. In passing, it generalizes the Clight pretty-printer so that it can print both Clight version 1 and Clight version 2. Closes: #314
* Fix tracing options for clightgen.Bernhard Schommer2019-07-151-10/+23
| | | | | | | | The clightgen tracing options did not result in printing of the intermediate files, but were ignored. Added also two new options, `-dprepro` to print the preprocessed file and `-dall` to dump all intermediate files.
* Correct typo in Clightnorm.ml (#285)Alix Trieu2019-03-271-1/+1
| | | | In the `Sswitch` case, the original expression was used instead of the result of `norm_expr`.
* clightgen: add info on configuration and platform to generated .v files (#238)Xavier Leroy2018-06-202-4/+21
| | | | | Information about the run of clightgen is added to the generated .v file as definitions within a sub-module named Info. Closes: #226.
* 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.
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-081-15/+18
| | | | | | | | | | | | | | | | | * 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-70/+15
| | | | | | 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.
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2018-01-171-3/+9
|\
| * Added type annotations for exported program. (#50)v3.2Bernhard Schommer2018-01-151-2/+2
| | | | | | | | Added types for global_definitions in order to avoid problems with implicit parameters. This should fix issue 215
| * Use Ptrofs.repr instead of Int.repr for Init_addrof. (#51)Bernhard Schommer2018-01-151-1/+7
| | | | | | | | This should fix issue 216 and also allows it to print 64 bit offsets.
* | Added missing help and common options.Bernhard Schommer2018-01-171-1/+15
|/ | | | | Clightgen also now has command line flags to control warnings as well as some other general options.
* Move machine initialization to Frontend.init function. (#49)Bernhard Schommer2018-01-111-20/+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.
* Added option -o to clightgen.Bernhard Schommer2018-01-111-5/+47
| | | Also allow preprocessed source files as input.
* Add riscv and attributes to ClightgenBernhard Schommer2018-01-101-0/+4
|
* Minor improvements.Bernhard Schommer2018-01-101-2/+2
|
* Change README to markdown.Bernhard Schommer2018-01-101-15/+14
|
* Remove all temporary files at program exit (#46)Bernhard Schommer2018-01-031-1/+1
| | | | | | | | | 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.
* Use quoted strings in clightgen.Bernhard Schommer2018-01-021-22/+24
|
* New support for inserting ais-annotations.Bernhard Schommer2017-10-191-2/+2
| | | | | | | | | | | | 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.
* Issue #199: improve namespace management for clightgen-produced filesXavier Leroy2017-08-282-16/+6
| | | | | Qualify imports in clightgen-produced files and in Clightdefs so that they can be used with coq -Q /path/to/compcert compcert. Remove 'Require Export' from Clightdefs as suggested in issue #199.
* Issue #196: excessive proof-checking times in .v files generated by clightgenXavier Leroy2017-08-152-13/+33
| | | | | | The check that "build_composite_env composites = OK (make_composite_env composites)" is taking time exponential on the number of struct/union definitions, at least on the example provided in #196. The solution implemented in this commit is to use computational reflection more efficiently, just to check that "build_composite_env composites" is of the form "OK _". From there, a new function Clightdefs.mkprogram produces the appropriate Clight.program without additional computation.
* clightgen: add option -normalize to ensure that memory loads never occur ↵Xavier Leroy2017-06-122-2/+177
| | | | | | | | | | | | | | | | | | | | | "deep" inside expressions For example, with this option, tmp = *(x + 0) + *(x + 1) in the original Clight is rewritten to tmp1 = *(x + 0) tmp2 = *(x + 1) tmp = tmp1 + tmp2 with two temporaries tmp1 and tmp2 introduced to name the intermediate results of memory loads. Squashed commit of the following: commit 3fb69dae567b1305383b74ce1707945f91369a46 commit 0071654b77a239c00bcbb92a5845447b2c4e9d2a commit c220ed303d9f3f36cc03c347a77b065a9362c0e7
* Issue #179: clightgen produces wrong abstract syntax for "switch" statementsXavier Leroy2017-04-281-3/+8
|
* Removed shadowing open.Bernhard Schommer2017-02-061-11/+11
|
* remove unused file, update tests for arch-field of configuration filesMichael Schmidt2016-11-031-1/+6
|
* Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-291-1/+3
|\
| * Implement support for big endian arm targets.Bernhard Schommer2016-08-051-1/+3
| | | | | | | | | | | | | | | | Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
* | Additional test for color output.Bernhard Schommer2016-08-051-10/+10
|/ | | | | | Color output is only enabled if stderr is a tty, and the environment variable TERM is not empty or dumb. Bug 18004
* Fixed warning 45 for ExportClight.ml.Bernhard Schommer2016-05-281-1/+1
|
* Added version string to Clightgen.Bernhard Schommer2016-05-241-2/+14
| | | | | | Clightgen now also prints a version string. Also the CompCert version string is now similar in both modes. Bug 18768.
* Escape all newlines.Bernhard Schommer2016-05-241-5/+5
| | | | Bug 18768.
* Moved shared frontend code in own file.Bernhard Schommer2016-05-241-161/+28
| | | | | | | Clightgen and CompCert share the code for preprocessing as well as parsing C files. The code as well as command line switches is moved in the new module Frontend. Bug 18768
* bug 18004, fix file extensions for dparse optionMichael Schmidt2016-04-251-1/+1
|
* Also refactor clightgen to work with new warnings. Bug 18394Bernhard Schommer2016-03-231-6/+6
|
* Merge branch 'master' into cleanupBernhard Schommer2016-03-211-0/+2
|\
| * Misc updates following the introduction of the new linking frameworkXavier Leroy2016-03-061-0/+2
| |
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-152-27/+27
| | | | | | | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* | Cleanup of Clightgen code.Bernhard Schommer2016-03-102-45/+41
|/ | | | | Removed unused code and code generating warnings. Bug 18394
* Naming of compiler-generated temporariesXavier Leroy2016-02-051-32/+76
| | | | clightgen now gives semi-readable and relatively stable names of the form _t'1, _t'2, _t'3, etc, to compiler-generated temporaries, instead of the unreadable and unstable NNN%positive notation generated previously.
generated by cgit (git 2.34.1) at 2024-06-26 18:52:01 +0000