aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight/ExportClight.ml
Commit message (Collapse)AuthorAgeFilesLines
* better failDavid Monniaux2021-09-271-1/+1
|
* fix clightgenDavid Monniaux2021-09-271-0/+3
|
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-011-5/+8
| | | | cfrontend/C2C.ml
* 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.
* 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).
* 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 -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-191-14/+21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (#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: add info on configuration and platform to generated .v files (#238)Xavier Leroy2018-06-201-3/+19
| | | | | 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.
* 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.
* 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-281-5/+4
| | | | | 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-151-8/+9
| | | | | | 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.
* Issue #179: clightgen produces wrong abstract syntax for "switch" statementsXavier Leroy2017-04-281-3/+8
|
* Removed shadowing open.Bernhard Schommer2017-02-061-11/+11
|
* Fixed warning 45 for ExportClight.ml.Bernhard Schommer2016-05-281-1/+1
|
* Escape all newlines.Bernhard Schommer2016-05-241-5/+5
| | | | Bug 18768.
* 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-151-25/+25
| | | | | | | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* | Cleanup of Clightgen code.Bernhard Schommer2016-03-101-42/+39
|/ | | | | 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.
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-6/+6
|
* Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-13/+13
| | | | | | | | | | The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables.
* Upgrade to reflect changes in type external_function.Xavier Leroy2015-10-111-4/+2
|
* Update clightgen w.r.t. teh calling_conventions record (new field cc_unproto).Xavier Leroy2015-08-171-1/+2
|
* Update clightgen w.r.t. EF_inline_asm (type of the clobber list).Xavier Leroy2015-08-171-1/+6
|
* Update clightgen to the new annotations and the new inline asm.Xavier Leroy2015-04-231-24/+9
|
* Update clightgen with respect to new representation of composites.Xavier Leroy2015-02-201-132/+38
|
* Refactoring in the printing of FP numbers.Xavier Leroy2014-09-241-8/+2
|
* Upgrade clightgen with the new features of CompCert 2.4 (single floats, etc).Xavier Leroy2014-09-241-7/+20
|
* Merge of "newspilling" branch:xleroy2014-07-231-3/+3
| | | | | | | | | | | | | | | - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update clightgen for CompCert 2.2.v2.2xleroy2014-02-231-14/+26
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2417 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-1/+0
| | | | | | | - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "alignas" branch.xleroy2013-10-051-4/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "princeton" branch:xleroy2013-06-161-4/+54
| | | | | | | | | | | | | | - Define type "block" as "positive" instead of "Z". - Strengthen mem_unchanged_on so that the permissions are identical, instead of possibly increasing. - Move mem_unchanged_on from Events to Memory.Mem. - Define it in terms of mem_contents rather than in terms of Mem.load. - ExportClight: try to name temporaries introduced by SimplExpr - SimplExpr: avoid reusing temporaries between different functions, instead, thread a single generator through all functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-1/+19
| | | | | | | | | 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* List.iteri not in OCaml < 4.00, better not use it.xleroy2013-04-081-2/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update clightgen to changes in Camlcoq and in AST.xleroy2013-03-201-14/+32
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2156 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Put clighgen files in exportclight/xleroy2013-01-051-0/+503
Short doc in exportclight/README git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2089 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-05-20 07:20:23 +0000