aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Collapse)AuthorAgeFilesLines
...
* | Remove coq warnings (#28)Bernhard Schommer2017-09-229-131/+131
|/ | | | Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
* Constprop strength reduction (#17)Bernhard Schommer2017-07-121-0/+21
| | | | | | | PowerPC port: add strength reduction for 64-bit operations * Added strength reduction for 64bit compare, subl, addl, mull, andl, orl, xorl, divl, shll, shrl, shrlu, shrluimm, shllimm, mullimm, divlu. (Bug 21748) * Moved shru_rolml proof to Values.
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-063-15/+20
| | | | | | This extension enables more addressing modes to be encoded as builtin arguments and used in conjunction with volatile memory accesses. Current status: x86 port only, the only new addressing mode handled is reg + offset.
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-039-271/+320
| | | | | | | | | | | | | This commit adds code generation for 64bit PowerPC architectures which execute 32bit applications. The main difference to the normal 32bit PowerPC port is that it uses the available 64bit instructions instead of using the runtime library functions. However pointers are still 32bit and the 32bit calling convention is used. In order to use this port the target architecture must be either in Server execution mode or if in Embedded execution mode the high order 32 bits of GPRs must be implemented in 32-bit mode. Furthermore the operating system must preserve the high order 32 bits of GPRs.
* Replace "Implicit Arguments" with "Arguments"Xavier Leroy2017-02-132-4/+4
| | | | | This silences a warning of Coq 8.6. Some "Implicit Arguments" remain in flocq/ but I'd rather not diverge from the released version of flocq if at all possible.
* Use "Local" as prefixXavier Leroy2017-02-132-12/+10
| | | | | Open Local becomes Local Open. This silences Coq 8.6's warning. Also: remove one useless Require-inside-a-module that caused another warning.
* Revised elaboration of attributesXavier Leroy2017-01-312-3/+2
| | | | | | | | | | | | | | | | | | | | | 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.
* remove unused file, update tests for arch-field of configuration filesMichael Schmidt2016-11-031-18/+0
|
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-041-0/+12
| | | | | | 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.
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-0/+100
| | | | | | Implement the 'shift right extended' trick, both in the generic implementation (backend/SplitLong) and in the IA32 port. Note that now SelectDiv depends on SelectLong, and that some work was moved from SelectLong to SelectDiv.
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-019-401/+1004
| | | | | | | | | | | - 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.
* Implement support for big endian arm targets.Bernhard Schommer2016-08-051-3/+4
| | | | | | | | Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
* Unwanted partial constant propagation in 64-bit integer arguments to builtinsXavier Leroy2016-07-081-1/+1
| | | | | | | | | | | | | | Here are two examples that cause an internal error in Asmexpand.ml: volatile long long x; void f(unsigned int i) { x = i; } unsigned g(unsigned i) { return __builtin_clzll(i); } The argument "i" to builtin volatile store or __builtin_clzll is turned into a BA_splitlong(BA_int 0, BA <variable i>), which Asmexpand.ml doesn't know how to handle. The fix (in AST.builtin_arg_ok) is to prevent this 'optimization' for all builtins except those of the "OK_all" kind, i.e. __builtin_annot. Regression tests were added and tested on IA32. Need to retest on ARM and PowerPC.
* Port to Coq 8.5pl2Xavier Leroy2016-07-084-33/+32
| | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* common/Determinism.v: dual-license with GPLXavier Leroy2016-06-301-0/+3
| | | | There was no good reason why Determinism.v was the only file in common/ that was not dual-licensed (GPL + noncommercial). Plus, it simplifies the wording of the LICENSE file.
* Stricter control of permissions in memory injections and extensionsXavier Leroy2016-06-222-7/+126
| | | | As suggested by Lennart Beringer, this commits strengthens memory injections and extensions so as to guarantee that the permissions of existing memory locations are not increased by the injection/extension. The only increase of permissions permitted is empty locations in the source memory state of the injection/extension being mapped to nonempty locations.
* 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
generated by cgit (git 2.34.1) at 2024-06-17 09:28:50 +0000