| Commit message (Collapse) | Author | Age | Files | Lines |
|\ |
|
| |\
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The original presentation of forward_simulation and backward_simulation diagrams was using records containing types, relations, and properties over these. These records had to live in Type because in Prop the projections could not be defined.
This was causing problems with proofs of statements such as
(exists x, P x) -> forward_simulation sem1 sem2
because the exists could not be eliminated in a Type context.
This commit re-expresses the simulation diagrams as a record of properties (in Prop) and an inductive (in Prop too) that packs the record with the types and relations. The external interface of module Smallstep is unchanged, it's only the proofs in Smallstep and Behaviors that take a slightly different shape.
|
| | |
| | |
| | |
| | | |
Also: in Events, use Senv.equiv to state invariance wrt changes of global envs.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The commutation lemmas between program transformations and Genv operations now take separate compilation into account. For example:
Theorem find_funct_ptr_match:
forall b f,
find_funct_ptr (globalenv p) b = Some f ->
exists cunit tf,
find_funct_ptr (globalenv tp) b = Some tf
/\ match_fundef cunit f tf
/\ linkorder cunit ctx.
Note how "f" and "tf" are related wrt a compilation unit "cunit" which is not necessarily "ctx" (the context for the whole program), but can be a sub-unit of the this whole program.
The other changes in Globalenvs are a long-overdue refactoring and cleanup:
- Introduce Senv.equiv (extensional equivalence between two Senv.t) to collect (in one place) the invariance properties relevant to external functions (preservation of names, of public names, and of volatile blocks).
- Revise internal representation of Genv.t: one map ident -> globdef F V instead of two maps ident -> F and ident -> globvar V.
- More precise characterization of initial memory states: "Genv.init_mem_characterization" uniquely characterizes every byte (memval) of the representation of an initialized global variable.
- Necessary and sufficient conditions for the initial memory state to exist.
- Revised proofs about init_mem, especially init_mem_inject.
- Removed some Genv lemmas that were unused.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- Add "prog_defmap" to compute the ptree name -> global definition corresponding to a program.
- Move "match_program" to Linking.
- Clean up and simplify a bit the transf_* functions for program transformations.
- Add a new kind of external functions, "EF_runtime". Unlike "EF_external", an "EF_runtime" external function cannot be implemented by an internal function definition in another compilation unit. (Linking returns an error in this case.) We will use "EF_runtime" for the "_i64_*" helper functions, which must not be defined by the program, and instead must remain external.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This framework follows "approach A" from the paper "Lightweight Verification of Separate Compilation" by Kang, Kim, Hur, Dreyer and Vafeiadis, POPL 2016.
Syntactic linking (of compilation units and their syntactic elements) is modeled by a type class with two components:
- a partial binary operation "link" that returns the syntactic element corresponding to the act of linking together its two arguments. It may fail if the two arguments cannot be linked, e.g. are incompatible definitions of the same name.
- a partial order "linkorder x y" that holds if "x" is a sub-unit of a whole program or bigger unit "y", or in other words, if "y" can be obtained by linking "x" with other units.
Instances of this type class are provided for the type AST.program and its syntactic elements (globvar, globdef, etc).
The "match_program" predicate that provides a relational characterization of compiler passes / program transformations is extended to account for context-dependent transformations and separate compilation: the transformation of a function definition can depend on the compilation unit it occurs in (this is the context), and this compilation unit "ctx" is characterized as any unit that is in the "linkorder ctx prog" relation with the whole source program "prog".
Under mild hypotheses, we show that "match_program" commutes with linking: if a1 matches b1, a2 matches b2, and a1 and a2 link together producing a, then b1 and b2 link together, producing a b that matches a.
Finally, we extend binary linking to linking of a nonempty list of compilation units; commutation with "match_program" still holds.
|
| | |
| | |
| | |
| | |
| | | |
- Make Mem.unchanged_on transitive.
- Add Mem.drop_perm_unchanged_on.
|
| |/
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| | |
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
|
|/
|
|
|
|
| |
Removed some unused variables, functions etc. and resolved some
problems which occur if all warnings except 3,4,9 and 29 are active.
Bug 18394.
|
|\
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| | |
Instead of using a string they now take an optional string, which
should be none if the backend is not the diab backend and the
corresponding section is the text section and Some s with s being
the custom section name else.
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.
|
|
|
|
|
|
| |
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.
|
|
|
|
|
| |
This commit adds furher support for location information for local
variables and starts with the implementation of the debug_loc section.
|
|
|
|
|
|
|
|
| |
Use EF_debug instead of EF_annot for line number annotations.
Introduce PrintAsmaux.print_debug_info (very incomplete).
powerpc/Asmexpand: revise expand_memcpy_small.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Before, the back-end languages had distinct instructions
- Iannot for annotations, taking structured expressions (annot_arg)
as arguments, and producing no results'
- Ibuiltin for other builtins, using simple pseudoregs/locations/registers
as arguments and results.
This branch enriches Ibuiltin instructions so that they take structured
expressions (builtin_arg and builtin_res) as arguments and results.
This way,
- Annotations fit the general pattern of builtin functions,
so Iannot instructions are removed.
- EF_vload_global and EF_vstore_global become useless, as the
same optimization can be achieved by EF_vload/vstore taking
a structured argument of the "address of global" kind.
- Better code can be generated for builtin_memcpy between stack locations,
or volatile accesses to stack locations.
Finally, this commit also introduces a new kind of external function,
EF_debug, which is like EF_annot but produces no observable events.
It will be used later to transport debug info through the back-end,
without preventing optimizations.
|
|
|
|
| |
As noticed by R. Krebbers, an inductive type for external worlds implies that all sequences of program-world interactions are finite, which is not the case.
|
|
|
|
|
|
| |
"old-style" unprototyped.
Use this info in printing function types for Csyntax and Clight.
|
|
|
|
|
|
|
|
|
|
| |
- Treat clobbered registers as being destroyed by EF_inline_asm builtins
(which is the truth, semantically).
- To enable the above, represent clobbers as Coq strings rather than idents
and move register_by_name from Machregsaux.ml to Machregs.v.
- Side benefit: more efficient implementation of Machregsaux.name_of_register.
-# Please enter the commit message for your changes. Lines starting
|
| |
|
|
|
|
| |
Val.lessdef, etc.
|
|
|
|
|
|
|
|
| |
- support "r", "m" and "i" constraints
- support "%Q" and "%R" modifiers for register pairs
- support register clobbers
- split off analysis and transformation of asm statements in
cparser/ExtendedAsm.ml
|
| |
|
|\ |
|
| |\
| | |
| | | |
Extended annotations
|
| | | |
|
| | |
| | |
| | |
| | |
| | | |
- Simplifications in RTLgen.
- Updated Cexec.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
variables whose address is taken.
- CminorSel, RTL: add "annot" instructions.
- CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions.
- AST, Events: simplify EF_annot because constants are now part of the arguments.
Implementation is not complete yet.
|
| |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
It used to be that a pointer value (Vptr) always compare unequal to the
null pointer (Vint Int.zero). However, this may not be true in the
final machine code when pointer addition overflows and wraps around
to the bit pattern 0. This patch checks the validity of the pointer
being compared with 0, and makes the comparison undefined if the
pointer is out of bounds.
Note: only the IA32 back-end was updated, ARM and PowerPC need updating.
|
| | |
|
|/ |
|
|
|
|
|
|
|
|
| |
Instead of assuming name uniqueness for all definitions in the program,
these variants only assume uniqueness for a particular name.
Use this approach to weaken the hypotheses for match_program
and transf_program_partial_augment.
|
|\
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- Switch CompCert C / Clight AST of composite types (structs and unions)
from a structural representation to a nominal representation,
closer to concrete syntax.
- This avoids algorithmic inefficiencies due to the structural representation.
- Closes PR#4.
- Smallstep: make small-step semantics more polymorphic in the type of the
global environment.
- Globalenvs: introduce Senv.t (symbol environments) as a restricted view
on Genv.t (full global environments).
- Events, Smallstep: use Senv instead of Genv to talk about global names.
|
| |
| |
| |
| | |
environments. Use symbol environments for the part of semantics that deals with observable events.
|
| |
| |
| |
| | |
environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events).
|
|/
|
|
| |
common.
|
|
|
|
|
| |
Restrict pointer event values to public global names.
Update proofs accordingly. PowerPC and ARM need updating.
|
|
|
|
| |
For the moment, this field is ignored.
|
|
|
|
|
|
|
| |
ofs + sz <= modulus.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2607 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2567 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(in CompCert C to Cminor, included)
- Translation of "switch" to decision trees or jumptables made generic
over the sizes of integers and moved to the Cminor->CminorSel pass
instead of CminorSel->RTL as before.
- CminorSel: add "exitexpr" to support the above.
- ValueDomain: more precise analysis of comparisons against an integer
literal. E.g. "x >=u 0" is always true.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2565 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|