aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Collapse)AuthorAgeFilesLines
...
| | * 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.
* Excessively strict validation: ofs + sz < modulus should have beenxleroy2014-08-201-4/+5
| | | | | | | ofs + sz <= modulus. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2607 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Issue with switch labels that are negative 32-bit integers.xleroy2014-08-171-0/+35
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2567 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Support "switch" statements over 64-bit integersxleroy2014-08-172-171/+264
| | | | | | | | | | | | | (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
* Add Mem.free_parallel_inject and use it to simplify Events a bit.xleroy2014-07-313-35/+50
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2556 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update "read_as_zeros" property.xleroy2014-07-231-1/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2538 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of "newspilling" branch:xleroy2014-07-238-504/+602
| | | | | | | | | | | | | | | - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add "read_as_zero" property for memory areas initialized by Init_space.xleroy2014-06-301-14/+106
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2519 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-02 23:02:50 +0000