aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Collapse)AuthorAgeFilesLines
* Prefixed runtime functions.Bernhard Schommer2017-08-251-16/+16
| | | | | | | The runtime functions are prefixed with compcert in order to avoid potential clashes with runtime/builtin functions of other compilers. Bug 22062
* SimlLocals.Sdebug_var: wrong type for 64-bit platformsXavier Leroy2017-07-091-1/+1
| | | | | | Fixes: Github issue #190. Tint was used instead of the correct Tptr.
* Early optimization of redundant *& and &* addressingsXavier Leroy2017-05-293-8/+59
| | | | | | Particularly annoying was the `*&x` sequence where `x` is a local variable, which would force stack-allocation of `x` early, generating extra loads and stores that could not always be optimized later (in CSE and Deadcode). The `*&` sequences and, by symmetry, the `&*` sequences are now eliminated early during Clight generation, via smart constructors.
* Do not generate code for "inline definitions"Bernhard Schommer2017-04-071-8/+15
| | | | | | | | | ISO C99 states that "inline defintions", functions with inline specifier that are not extern, does not provide an external definition and another compilation unit can contain an external definition. Thus in the case of non-static inline functions no code should be generated. Bug 21343
* attempt to optimize empty if/then/else statementsMichael Schmidt2017-04-063-7/+32
|
* Added gcc noinline attribute.Bernhard Schommer2017-02-191-0/+1
| | | | The noinline attribute prevents functions from inlining.
* Added unused attribute and simplified checks.Bernhard Schommer2017-02-171-1/+2
| | | | | | | | | The attribute unused can be used to indicate if a variable or parameter is unused and no warning should be emitted for it. Furthermore this commit simplifies the check by adding a generic function to traverse the program. Bug 19872
* Replace "Implicit Arguments" with "Arguments"Xavier Leroy2017-02-131-2/+2
| | | | | This silences a warning of Coq 8.6. Some "Implicit Arguments" remain in flocq/ but I'd rather not diverge from the released version of flocq if at all possible.
* Use "Local" as prefixXavier Leroy2017-02-132-3/+3
| | | | | Open Local becomes Local Open. This silences Coq 8.6's warning. Also: remove one useless Require-inside-a-module that caused another warning.
* Merge branch 'coq-8.6' of https://github.com/maximedenes/CompCert into ↵Xavier Leroy2017-02-132-7/+9
|\ | | | | | | maximedenes-coq-8.6
| * Some backward compatible Ltac fixes, necessary for 8.6.Maxime Dénès2017-01-091-5/+7
| |
| * An hypothesis has changed name.Maxime Dénès2017-01-091-1/+1
| | | | | | | | Not sure why, but it would be safer not to rely on automatic naming.
| * The subst tactic has become more powerful.Maxime Dénès2017-01-091-1/+1
| |
* | More tweaking of module 'open'Xavier Leroy2017-02-091-8/+10
| | | | | | | | I really like to have Floats and Values opened. The other opens I can live without, but Floats.Float.zero is just wrong.
* | Merge branch 'elaboration-of-attributes'Xavier Leroy2017-02-061-1/+15
|\ \
| * | Preliminary support for the "noreturn" attributeXavier Leroy2017-02-061-1/+2
| | | | | | | | | | | | | | | - Mark the "noreturn" attribute as related to function types, so that it is correctly attached to the nearest enclosing function type. - Add this attribute on functions declared / defined _Noreturn (with the C2011 keyword). The information is not used presently but could be useful later.
| * | Refactor the classification of attributesXavier Leroy2017-02-031-0/+13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | Revised elaboration of attributesXavier Leroy2017-01-311-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The treatment of attributes in the current CompCert is often surprising. For example, attribute(xxx) char * x; is parsed as "x is a pointer to a (char modified by attribute "xxx")", while for most attributes (e.g. section attributes) the expected meaning is "x, modified by attribute "xxx", has type pointer to char". CompCert's current treatment comes from the fact that attributes are processed very much like the standard type modifiers `const` and `volatile`, i.e. const char * x; is really "x is a pointer to a const char", not "x is a const pointer to char". This experiment introduces a distinction between type-related attributes (which include the standard modifiers `const` and `volatile`) and other attributes. The other, non-type-related attributes are "floated up" during elaboration so that they apply to the variable or function being declared or defined. In the examples above, attribute(xxx) char * x; // "attribute(xxx)" applies to "x" const char * x; // "const" applies to "char" This may be a step in the right direction but is not the final story. In particular, the `packed` attribute is special-cased when applied to `struct`, like it was before, and future attributes concerning calling conventions would need to be floated up to function types but not higher than that.
* | | Cleanup opensBernhard Schommer2017-02-061-69/+62
| | |
* | | Removed shadowing problems.Bernhard Schommer2017-02-061-9/+9
| | | | | | | | | | | | The clashing identifiers are now referenced explicitly.
* | | Inlined open of ASTBernhard Schommer2017-02-061-7/+6
|/ /
* / Simplified C2C.error.Bernhard Schommer2017-01-182-19/+16
|/ | | | | | | Instead of just accepting a string the function is changed to accept a format string. This removes a lot of artificial sprintfs in calls to the functions. Bug 19872
* C2C: revise typing and translation of __builtin_memcpy_alignedXavier Leroy2016-11-171-12/+16
| | | | | | | | | | | | | | | | | | | | This fixes two issues: 1- The 'size' and 'alignment' arguments of __builtin_memcpy_aligned were declared with type 'unsigned int', which is not good for a 64-bit platform. 2- The corresponding arguments were not cast to type 'unsigned int', causing compilation errors if e.g. the size argument is a 64-bit integer. (Reported by Michael Schmidt.) The fix: 1- Evaluate the 3rd and 4th arguments at type size_t 2- Support both Vint and Vlong as results of this evaluation 3- Declare these arguments with type 'unsigned long'. Supporting work: in lib/Camlcoq.ml, add Z.modulo and Z.is_power2 operations. Concerning part 3 of the fix, type size_t would be better for future platforms where size_t is bigger than unsigned long, but some more work is needed to delay the evaluation of C2C.builtins_generic to after Cutil.size_t_ikind() is stable, or, equivalently, to evaluate the cparser/ machine configuration before C2C initializes.
* Initializers: introduce 'constval_cast' to cast constant value to desired typeXavier Leroy2016-11-172-21/+25
| | | | This comes handy in the next commit where constval_cast is used from C2C.
* C2C: wrong translation of 'switch' over arguments of type 'long' if 'long' ↵Xavier Leroy2016-11-171-4/+5
| | | | | | | is 64 bits It was wrongly assumed that 'long' is 32 bits. (Reported by Michael Schmidt.)
* fix va_arg for pointer types on 64bit targetMichael Schmidt2016-11-081-1/+7
|
* extend constant check for builtin_memcpy_aligned (bug 20320)Michael Schmidt2016-11-071-2/+2
|
* extend constant check for builtin_memcpy_aligned (bug 20320)Michael Schmidt2016-11-071-0/+2
|
* Merge pull request #145 from AbsInt/64Xavier Leroy2016-10-2719-967/+1300
|\ | | | | | | Support for 64-bit target processors + support for x86 in 64-bit mode
| * Regression: handling of integer + pointer in CompCert CXavier Leroy2016-10-064-115/+112
| | | | | | | | | | | | During the experiments, the integer + pointer cases was removed from the semantics of the C addition operator. The idea was to turn integer + pointer into pointer + integer during elaboration, but it was not implemented. On second thoughts, we can restore the integer + pointer cases in the formal semantics of CompCert C at low cost. This is what this commit does.
| * Regression: compile-time evaluation of ((struct s *)0)->fieldXavier Leroy2016-10-062-4/+7
| | | | | | | | | | This somewhat useful idiom was broken when Val.add was replaced by Val.offset_ptr in the Efield case. This commit restores the previous behavior. This used to be supported (and is useful
| * Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-041-0/+8
| | | | | | | | | | | | This trick was already implemented for 32-bit integer division and modulus. Here we extend it to the 64-bit case. For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned). Tentative implementations are provided for IA32 and PowerPC, but need testing.
| * Remove usage of do.Bernhard Schommer2016-10-041-58/+58
| | | | | | | | | | | | Apparently coq compiled with camlp4 has a problem with the user defined do <- ... ; ... and do. Bug 20050
| * Support for 64-bit architectures: generic supportXavier Leroy2016-10-0119-926/+1251
| | | | | | | | | | | | | | | | | | | | | | - 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.
* | implement checks for parameters of '__builtin_memcpy_aligned' (bug 20222)Michael Schmidt2016-10-191-4/+4
| |
* | implement checks for parameters of '__builtin_memcpy_aligned' (bug 20222)Michael Schmidt2016-10-191-3/+6
|/
* Improved error messages for wrong vararg calls.Bernhard Schommer2016-09-231-2/+7
| | | | | | Now "expected at least %d" instead of "expected %d". Also improved error message for __builtin_debug. Bug 19872
* Catch case of zero in builtin debug.Bernhard Schommer2016-09-221-2/+2
|
* Merge pull request #142 from maximedenes/minor-fixesXavier Leroy2016-09-211-5/+8
|\ | | | | | | | | | | Fix minor issues in some proofs and tactics. Patch by Maxime Dénès.
| * Fix minor issues in some proofs and tactics.Maxime Dénès2016-09-211-5/+8
| | | | | | | | | | These minor problems were revealed by porting CompCert to Coq 8.6, where they trigger errors.
* | Merge pull request #139 from AbsInt/advanced-diagnosticsBernhard Schommer2016-09-202-36/+34
|\ \ | | | | | | Advanced diagnostics
| * | Readded warning about ignored volatile. Bug 18004Bernhard Schommer2016-08-311-1/+1
| | |
| * | Added missing literal. Bug 18004Bernhard Schommer2016-08-311-1/+1
| | |
| * | Fixed typos.Bernhard Schommer2016-08-311-8/+8
| | | | | | | | | | | | | | | | | | Removed duplicated of, changed string to string literal for wording than the C standard. Bug 18004
| * | bug 18004, fix some typos/grammarMichael Schmidt2016-08-301-1/+1
| | |
| * | Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-292-3/+23
| |\ \
| * | | Classified all warnings and added various options.Bernhard Schommer2016-07-292-34/+33
| | |/ | |/| | | | | | | | | | | | | | | | | | | | | | | | | 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
* | | Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpyXavier Leroy2016-09-171-31/+4
| | | | | | | | | | | | Inline directives in extraction.v make the Caml output efficient and almost nice.
* | | Removed some implict arguments.Bernhard Schommer2016-09-051-13/+5
| |/ |/| | | | | Also changed Local Open to Open Local.
* | Simplify test. Bug 19629Bernhard Schommer2016-08-251-4/+1
| |
generated by cgit (git 2.34.1) at 2024-06-29 02:04:56 +0000