aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Collapse)AuthorAgeFilesLines
...
* Improved handling of "rotate left" and "rotate right" operatorsXavier Leroy2016-06-221-4/+7
| | | | | | | | - 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.
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-172-188/+56
| | | | | | | | | | | | | 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.
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit ↵Xavier Leroy2016-04-271-0/+916
| | | | | | | | | | | | | | | | | | | 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.
* Merge branch 'master' into cleanupBernhard Schommer2016-03-218-1966/+2166
|\
| * Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-208-1964/+2164
| |\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * Put forward_simulation and backward_simulation in Prop instead of TypeXavier Leroy2016-03-062-303/+323
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * Add support for EF_runtime externalsXavier Leroy2016-03-062-52/+33
| | | | | | | | | | | | Also: in Events, use Senv.equiv to state invariance wrt changes of global envs.
| | * Globalenvs: adapt to new linking framework, and revise.Xavier Leroy2016-03-061-1146/+729
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * AST: extend and adapt to the new linking framework.Xavier Leroy2016-03-061-460/+116
| | | | | | | | | | | | | | | | | | | | | - 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.
| | * The basic framework for linking and separate compilation.Xavier Leroy2016-03-061-0/+905
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * Preliminaries: minor extensions to MemoryXavier Leroy2016-03-061-3/+58
| | | | | | | | | | | | | | | - Make Mem.unchanged_on transitive. - Add Mem.drop_perm_unchanged_on.
| * | Print floating-point numbers with more digits in debug outputsXavier Leroy2016-03-151-2/+2
| |/ | | | | | | | | | | 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.
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-151-6/+6
| | | | | | | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* | Code cleanup.Bernhard Schommer2016-03-103-9/+6
|/ | | | | | 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.
* Merge remote-tracking branch 'origin/master' into named-externalsBernhard Schommer2015-10-202-4/+8
|\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| * Implemented the usage of DW_AT_ranges for non-contiguous address ranges.Bernhard Schommer2015-10-162-0/+2
| | | | | | | | | | | | | | | | | | | | 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.
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-1414-1666/+1666
| |
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-143-8/+8
| |
| * Changed the type of the debug sections with additional string.Bernhard Schommer2015-10-132-4/+4
| | | | | | | | | | | | | | | | 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.
| * Implement the usage of the debug_str section for the gcc backend.Bernhard Schommer2015-10-132-2/+4
| | | | | | | | | | | | | | | | 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.
* | Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-2017-1673/+1673
| |
* | Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-114-25/+23
|/ | | | | | | | | | 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.
* Filled in the rest of the funciton needed for thte debug info under arm.Bernhard Schommer2015-10-092-0/+2
| | | | | | 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.
* Added versions of the tranform_* functions in AST to work with functionsBernhard Schommer2015-10-081-1/+216
| | | | | | | | 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.
* Change the way the debug sections are printed.Bernhard Schommer2015-09-282-2/+2
| | | | | | 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.
* Added support for the locations of stack allocated local variables.Bernhard Schommer2015-09-252-0/+2
| | | | | This commit adds furher support for location information for local variables and starts with the implementation of the debug_loc section.
* Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-223-16/+16
| | | | | | | | Use EF_debug instead of EF_annot for line number annotations. Introduce PrintAsmaux.print_debug_info (very incomplete). powerpc/Asmexpand: revise expand_memcpy_small.
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-213-358/+297
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* Represent external worlds by a coinductive type rather than an inductive type.Xavier Leroy2015-06-071-1/+1
| | | | 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.
* In AST.calling_conventions, record whether the original C function was ↵Xavier Leroy2015-05-221-3/+4
| | | | | | "old-style" unprototyped. Use this info in printing function types for Csyntax and Clight.
* Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-091-2/+2
| | | | | | | | | | - 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
* Typo: Val.sun_inject -> Val.sub_inject.Xavier Leroy2015-05-061-1/+1
|
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with ↵Xavier Leroy2015-04-305-111/+113
| | | | Val.lessdef, etc.
* Support for GCC-style extended asm, continued:Xavier Leroy2015-04-213-5/+6
| | | | | | | | - 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
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-173-8/+8
|
* Merge branch 'master' into dwarfBernhard Schommer2015-04-024-46/+249
|\
| * Merge pull request #34 from AbsInt/extended-annotationsXavier Leroy2015-04-014-29/+216
| |\ | | | | | | Extended annotations
| | * Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-271-2/+4
| | |
| | * Extended arguments to annotations, continued:Xavier Leroy2015-03-272-34/+6
| | | | | | | | | | | | | | | - Simplifications in RTLgen. - Updated Cexec.
| | * Extend annotations so that they can keep track of global variables and local ↵Xavier Leroy2015-03-273-29/+242
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | Revised semantics of comparisons between a pointer and 0.Xavier Leroy2015-03-151-17/+33
| |/ | | | | | | | | | | | | | | | | | | | | 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.
* | Started integrating the debug printing in the common backend_printer.Bernhard Schommer2015-03-112-2/+2
| |
* | Starting to remove the seperate printers for each backend.Bernhard Schommer2015-02-022-0/+4
|/
* Add weaker variants of theorems find_funct_ptr_exists and find_var_exists.Xavier Leroy2015-01-231-70/+122
| | | | | | | | 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.
* Merge branch 'named-structs'Xavier Leroy2015-01-234-177/+260
|\ | | | | | | | | | | | | | | | | | | | | | | | | - 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.
| * Make small-step semantics more parametric w.r.t. the type of global ↵Xavier Leroy2014-11-262-27/+42
| | | | | | | | environments. Use symbol environments for the part of semantics that deals with observable events.
| * Introduce symbol environments (type Senv.t) as a restricted view on global ↵Xavier Leroy2014-11-262-150/+218
| | | | | | | | environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events).
* | Clean up support for common symbols. Uninitialized "const" symbols can be ↵Xavier Leroy2014-12-172-8/+8
|/ | | | common.
* Add Genv.public_symbol operation.Xavier Leroy2014-11-244-180/+342
| | | | | Restrict pointer event values to public global names. Update proofs accordingly. PowerPC and ARM need updating.
* Record public global definitions via field "prog_public" in AST.program.Xavier Leroy2014-11-241-3/+25
| | | | For the moment, this field is ignored.
generated by cgit (git 2.34.1) at 2024-06-29 13:40:03 +0000