| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
| |
Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
|
|
|
|
|
|
|
|
| |
- Values: "rol" and "ror" are defined even if their second argument
is not in the [0,31] range (for consistency with "rolm" and because
the semantics is definitely well defined in this case).
- NeedDomain: more precise analysis of "rol" and "rolm", could
benefit the PowerPC port.
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
restricted to 15bit signed immediate offsets
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
architectures
The original Stacking pass and its proof hard-wire assumptions about the processor and the register allocation, namely that integer registers are 32 bit wide and that all stack slots have natural alignment 4, which precludes having stack slots of type Tlong. Those assumptions become false if the target processor has 64-bit integer registers.
This commit makes minimal adjustments to the Stacking pass so as to lift these assumptions:
- Stack slots of type Tlong (or more generally of natural alignment 8) are supported. For slots produced by register allocation, the alignment is validated a posteriori in Lineartyping. For slots produced by the calling conventions, alignment is proved as part of the "loc_argument_acceptable" property in Conventions1.
- The code generated by Stacking to save and restore used callee-save registers no longer assumes 32-bit integer registers. Actually, it supports any combination of sizes for registers.
- To support the new save/restore code, Bounds was changed to record the set of all callee-save registers used, rather than just the max index of callee-save registers used.
On CompCert's current 32-bit target architectures, the new Stacking pass should generate pretty much the same code as the old one, modulo minor differences in the layout of the stack frame. (E.g. padding could be introduced at different places.)
The bulk of this big commit is related to the proof of the Stacking phase. The old proof strategy was painful and not obviously adaptable to the new Stacking phase, so I rewrote Stackingproof entirely, using an approach inspired by separation logic. The new library common/Separation.v defines assertions about memory states that can be composed using a separating conjunction, just like pre- and post-conditions in separation logic. Those assertions are used in Stackingproof to describe the contents of the stack frames during the execution of the generated Mach code, and relate them with the Linear location maps.
As a further simplification, the callee-save/caller-save distinction is now defined in Conventions1 by a function is_callee_save: mreg -> bool, instead of lists of registers of either kind as before. This eliminates many boring classification lemmas from Conventions1. LTL and Lineartyping were adapted accordingly.
Finally, this commit introduces a new library called Decidableplus to prove some propositions by reflection as Boolean computations. It is used to further simplify the proofs in Conventions1.
|
|
|
|
| |
For informative purposes, the FP value of Init_float* constants is printed as a comment in the generated asm file. However, for Init_float32, it was wrongly printed as a double-precision FP instead of a single-precision FP.
|
|\ |
|
| |\
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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: 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.
|
| |
| |
| |
| |
| |
| | |
Hide the reference used internally behind the interface and added
some functions to access the needed values.
Bug 18394
|
| |
| |
| |
| |
| |
| | |
Removed unused code, factored out common functions and added an
interface file.
Bug 18394
|
| |
| |
| |
| |
| |
| | |
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
|
| |
| |
| |
| |
| | |
Removed some unused functions and opens.
Bug 18394
|
|/
|
|
|
| |
Removed unused functions and avoid warnings.
Bug 18394.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Two reasons:
- The movs is not supported if rd or rs is r13 (the stack ptr register).
Newer versions of GNU as reject it, older versions were probably
emulating it.
- The purpose of setting the "s" flag on some operations is to
enable 16-bit encoding in Thumb2 mode. However, for "mov"
it is the non-s form that has a 16-bit encoding; the s form
is never more compact.
|
|
|
|
| |
Follow-up to commit f531d38
|
|
|
|
|
|
|
| |
ARM: add __builtin_clzl, __builtin_clzll
IA32: add __builtin_clzl, __builtin_clzll,
__builtin_ctzl, __builtin_ctzll
Add corresponding tests in tests/regression/
|
|
|
|
| |
compatibility, and not "unsigned int", as previously implemented.
|
|
|
|
|
|
| |
On older version of the binutils the cfi directives are not always
supported so we only print cfi_sections if the corresponding .ini
setting is set to true.
|
|\
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Conflicts:
arm/TargetPrinter.ml
backend/CMparser.mly
backend/SelectLongproof.v
backend/Selectionproof.v
cfrontend/C2C.ml
checklink/Asm_printers.ml
checklink/Check.ml
checklink/Fuzz.ml
common/AST.v
debug/DebugInformation.ml
debug/DebugInit.ml
debug/DwarfPrinter.ml
debug/DwarfTypes.mli
debug/Dwarfgen.ml
exportclight/ExportClight.ml
ia32/TargetPrinter.ml
powerpc/Asm.v
powerpc/SelectOpproof.v
powerpc/TargetPrinter.ml
|
| |
| |
| |
| | |
Bug 17392
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The gcc produces DW_AT_ranges for non-contiguous address ranges, like
compilation units containing functions which are placed in different
ELF-sections or lexical scopes that are split up. With this commit
CompCert also uses this DWARF v3 feature for gnu backend based targets.
In order to ensure backward compability a flag is added which avoids
this and produces debug info in DWARF v2 format.
Bug 17392.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In contrast to the dcc, the gcc uses address ranges to express
non-contiguous range of addresses. As a first step we set the
start and end addresses for the different address ranges for
the compilation unit by using the start and end addresses of
functions.
Bug 17392.
|
| |
| |
| |
| | |
Bug 17392.
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| | |
GCC prints all string larger than 3 characters in the debug_str
section which reduces the size of the debug information since entries
containing the same string now map to the same string in the
debug_str sections.
Bug 17392.
|
| | |
|
|/
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
| |
Like for arm and ppc the functions for section names and start and
end addresses of compilation units are defined and the print_annot
function is moved to Asmexpandaux.ml.
|
|
|
|
|
|
| |
The name_of_section function no returns the correct name for the
debug sections, the prologue and epilogue directives are added and
the labels for the live ranges are introduced in the Asmexpand pass.
|
|
|
|
|
|
|
|
| |
taking the ident as argument.
This functions are currently not used inside the proven part but it
is nice to have them already there, when they are used by some future
pass. They also come equiped with the corresponding proofs.
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
If a user uses the #pragma use_section for functions the diab linker
requires a separate debug_info section for each entry. This commit
adds functionality to emulate this behavior.
|
|
|
|
|
|
|
|
| |
Debuging code.
The old functions to store the symbol for the Global variables and retrive this
is no longer needed since the atom is stored in DebugInformation. Also the
Debug.Abbrev module is no longer needed.
|
|
|
|
|
| |
This commit adds furher support for location information for local
variables and starts with the implementation of the debug_loc section.
|
|
|
|
|
|
| |
Instead of creating separate annotations for the local variables
we call the Debug.add_lvar_scope and we construct a mapping from
function id + scope id to scope information.
|
|
|
|
| |
This reverts commit 861292a6c5e58b4f78bef207c717b801b3fc1fed.
|
|
|
|
|
|
| |
Added a new file debug/Debug.ml which will be the interface between for
generating and printing the debuging information. Currently it contains
only the code for the line directived.
|
|\
| |
| |
| | |
Merge branch 'master' into debug_locations
|
| | |
|
|\|
| |
| |
| |
| |
| |
| | |
Conflicts:
debug/CtoDwarf.ml
debug/DwarfPrinter.ml
debug/DwarfTypes.mli
|