| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
This comes handy in the next commit where constval_cast is used from C2C.
|
|
|
|
|
|
|
| |
is 64 bits
It was wrongly assumed that 'long' is 32 bits.
(Reported by Michael Schmidt.)
|
| |
|
| |
|
| |
|
|\
| |
| |
| | |
Support for 64-bit target processors + support for x86 in 64-bit mode
|
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| | |
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
|
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| | |
Apparently coq compiled with camlp4 has a problem with the user
defined do <- ... ; ... and do.
Bug 20050
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- 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.
|
| | |
|
|/ |
|
|
|
|
|
|
| |
Now "expected at least %d" instead of "expected %d". Also improved
error message for __builtin_debug.
Bug 19872
|
| |
|
|\
| |
| |
| |
| |
| | |
Fix minor issues in some proofs and tactics.
Patch by Maxime Dénès.
|
| |
| |
| |
| |
| | |
These minor problems were revealed by porting CompCert to Coq 8.6, where
they trigger errors.
|
|\ \
| | |
| | | |
Advanced diagnostics
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
Removed duplicated of, changed string to string literal for
wording than the C standard.
Bug 18004
|
| | | |
|
| |\ \ |
|
| | |/
| |/|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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
|
| | |
| | |
| | |
| | | |
Inline directives in extraction.v make the Caml output efficient and almost nice.
|
| |/
|/|
| |
| | |
Also changed Local Open to Open Local.
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
The test is extended for integer constants smaller than 0. Also the
default constant used for the error is no longer 0 since this is
not a positive number.
Bug 19629
|
| |
| |
| |
| |
| |
| | |
The declarations of malloc and free should also be printed for
CompCert C.
Bug 19616.
|
| |
| |
| |
| |
| |
| | |
The PrintCsyntax now first emits declarations for all functions
and variables in order to allow foward declarations.
Bug 19598.
|
|/ |
|
|
|
|
|
| |
Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
|
|
|
|
|
|
|
|
| |
Most of the code can be String.uppercase usages can either be
replaced by a more specialized version of coqstring_of_camlstring
(which is also slightly more effecient) or by specialized checks
that reject wrong code earlier.
Bug 19187
|
|
|
|
| |
can parse its own .compcert.c output, bug 18060
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit changes the loc_arguments and loc_result functions that describe calling conventions so that each argument/result can be mapped either to a single location or (in the case of a 64-bit integer) to a pair of two 32-bit locations.
In the current CompCert, all arguments/results of type Tlong are systematically split in two 32-bit halves. We will need to change this in the future to support 64-bit processors. The alternative approach implemented by this commit enables the loc_arguments and loc_result functions to describe precisely which arguments need splitting. Eventually, the remainder of CompCert should not assume anything about splitting 64-bit types in two halves.
Summary of changes:
- AST: introduce the type "rpair A" of register pairs
- Conventions1, Conventions: use it when describing calling conventions
- LTL, Linear, Mach, Asm: honor the new calling conventions when observing external calls
- Events: suppress external_call', no longer useful
- All passes from Allocation to Asmgen: adapt accordingly.
|
|\ |
|
| |\
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This pull request implements "approach A" to separate compilation in CompCert from the paper
Lightweight verification of separate compilation
by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis,
POPL 2016, pages 178-190
In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program.
This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.
|
| | | |
|
| | |
| | |
| | |
| | | |
Also: factor out the type "program" between Csyntax and Clight, putting it in Ctypes.
|
| | |
| | |
| | |
| | | |
Also: in Events, use Senv.equiv to state invariance wrt changes of global envs.
|
| | |
| | |
| | |
| | |
| | |
| | | |
As suggested in GPR#84, use '%.15F' to force the printing of more significant digits. (The '%F' format previously used prints only 6.) This is enough to represent the FP number exactly most of the time (but not always).
Once OCaml 4.03 is out and CompCert switches to this version of OCaml, we'll be able to use hexadecimal floats for printing.
|
| |\ \
| | | |
| | | | |
Make casts of pointers to _Bool semantically well defined
|
| | |/
| | |
| | |
| | |
| | |
| | | |
In compCert 2.5 the semantics of pointer comparisons against the NULL pointer was made more accurate by making it undefined if the pointer is invalid (outside bounds). Technical difficulties prevented this change from being propagated to the semantics of casts from pointer types to the _Bool type, which involves an implicit pointer comparison against NULL. Hence, this kind of casts was temporarily given undefined semantics.
This commit makes pointer-to-_Bool casts semantically defined (again), provided the pointer is valid. This reinstates the equivalence between casts to _Bool and comparisons != 0. The technical difficulties mentioned above came from the translation of assignments in a value context in the SimplExpr pass. The pass was lightly modified to work around the issue.
|
| |/
| |
| |
| |
| |
| | |
Support <pointer> +/- <integer> where the pointer value is actually an integer (Vint) that has been converted to pointer type.
Such arithmetic, while not defined in ISO C, appears in the wild. If present in static initializers, it used to cause a compile-time failure ("not a compile-time constant"). Hence this relaxation.
|
| |
| |
| |
| |
| |
| | |
The functions for naming string and wstring literals no longer need
an env.
Bug 18394
|
| |
| |
| |
| |
| |
| | |
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
|
| |
| |
| |
| | |
This reverts commit bac2a0854ea51217690bc6f225da62053ed7ac06.
|