aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
Commit message (Collapse)AuthorAgeFilesLines
...
| * If-conversion optimizationXavier Leroy2019-06-061-0/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches.
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-031-5/+6
|\ \ | | | | | | | | | mppa-if-conversion
| * | If-conversion optimizationXavier Leroy2019-05-311-0/+1
| |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches.
| * Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-5/+5
| | | | | | | | | | | | | | | | | | | | | | | | Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully).
* | option -faddx (off by default until questions cleared)David Monniaux2019-05-111-4/+6
| |
* | -fcoalesce-memDavid Monniaux2019-05-031-0/+2
| |
* | command line options (still incomplete)David Monniaux2019-05-021-0/+6
| |
* | -fpostpass-ilpDavid Monniaux2019-03-121-3/+1
| |
* | Added a flag for changing the scheduler (not any choice available right now)Cyril SIX2019-03-121-1/+3
| |
* | -O0 will not perform postpass schedulingCyril SIX2019-01-181-1/+4
| |
* | compilation Asmexpandaux both for x86/ and mppa_k1c/Sylvain Boulmé2018-11-281-1/+2
| |
* | BROKEN - works for x86, not for k1 anymoreCyril SIX2018-11-261-1/+0
| |
* | Asmblock & cie - ça compileCyril SIX2018-09-061-2/+1
| |
* | Extraction issueCyril SIX2018-09-061-1/+2
| |
* | MPPA - Optimized branch generation for word compare to 0Cyril SIX2018-04-091-87/+0
| |
* | MPPA - 32-bits immediate eq/neq branchesCyril SIX2018-04-041-0/+16
| |
* | MPPA - fixed typos in extraction/debug/Asmgen.mlCyril SIX2018-04-041-3/+2
| |
* | MPPA Added debug pretty printer for transl_instrCyril SIX2018-04-041-0/+31
| |
* | MPPA Moved debug/Asmgen.ml to extraction/debug/Asmgen.mlCyril SIX2018-04-041-0/+167
| |
* | MPPA - The project compiles.Cyril SIX2018-04-041-0/+1
|/ | | | | | | | | | | | | Supports very simple programs that load integer immediates. It starts the main, loads integer in registers, and return correctly. Addition in Mach not yet supported, but should not be hard to add them. Function calls are not yet supported. The ABI for now is the same as the RiscV, with a small twist: $ra is first loaded in a user register, then this user register is pushed (instead of pushing $ra straight away).
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-051-0/+3
| | | | | | | | | | | Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent. This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed. Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST which is not in lib/
* Inlining of static functions which are only called once. (#37)Bernhard Schommer2017-12-071-0/+2
| | | | | | | | | New inlining heuristic for static functions. Static functions that are only called once can always be inlined, since they can be removed safely after inlining and no call prologue, epilogue, as well as register saving and needs to be generated.
* Pull request #192: improve the printing of Clight intermediate codeXavier Leroy2017-11-221-0/+1
| | | | So that it looks more like valid C source.
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-1/+1
| | | | | | | | | | | | | 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.
* Inline fst and snd from Datatypes.Bernhard Schommer2017-02-061-0/+4
| | | | | This avoids nameclashes with the Pervasives version of these functions.
* Removed Cabshelper open and avoided shadowing.Bernhard Schommer2017-02-031-1/+1
| | | | | | | | The Cabshelper is only used in 4 places, so we don't need a global open. Furhtermore the String.t type is now inlined for Cabs to avoid shadowing problems in Elab.ml Bug 19872
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-0/+1
| | | | | | | | | | | - 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.
* Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpyXavier Leroy2016-09-171-0/+7
| | | | Inline directives in extraction.v make the Caml output efficient and almost nice.
* Add interference for indirect calls.Bernhard Schommer2016-09-151-2/+3
| | | | | | Avoids problems with overwritting the registe containing the function address. Bug 19779
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-0/+2
| | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit ↵Xavier Leroy2016-04-271-0/+2
| | | | | | | | | | | | | | | | | | | 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.
* Misc updates following the introduction of the new linking frameworkXavier Leroy2016-03-061-2/+1
|
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-1/+1
|
* Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-4/+0
| | | | | | | | | | 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.
* Added versions of the tranform_* functions in AST to work with functionsBernhard Schommer2015-10-081-0/+1
| | | | | | | | 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.
* Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-231-0/+2
| | | | | | | | | | | | | | SimplLocals: - record locations of stack-allocated variables with annotations (of kind 5) at the beginning of the function; - mark every assignment to non-stack-allocated variables with an annotation of kind 2. Debugvar: (new pass!) - perform availability analysis for debug annotations of kind 2 - insert "start of live range" and "end of live range" annotations (kind 3 and 4) to delimit intervals of PCs where the location of a local variable is known.
* Ctyping: better typing of conditional expressions.Xavier Leroy2015-05-211-2/+2
| | | | | | | | | | | | Ctyping: define a typechecker for whole programs. Csyntax: introduce the type "pre-program" (non-dependent). C2C: use Ctyping.econdition instead of Ctyping.econdition'. Note: Ctyping.typecheck_program could be used as the first step in the verified compilation pipeline. Then, retyping would no longer be performed in C2C. We keep it this way (for the time being) because retyping errors are reported more precisely in C2C than in Ctyping.
* Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-091-3/+0
| | | | | | | | | | - 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
* Take asm clobbers into account for determining callee-save registers used.Xavier Leroy2015-04-231-0/+4
|
* Merge branch 'named-structs'Xavier Leroy2015-01-231-1/+7
|\ | | | | | | | | | | | | | | | | | | | | | | | | - 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.
| * Add a type system for CompCert C and type-checking constructor functions.Xavier Leroy2014-12-311-0/+3
| | | | | | | | | | Use these constructor functions in C2C to rely less on the types produced by the unverified elaborator.
| * Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-221-1/+4
| |
* | Protect against redefinition of the __i64_xxx helper library functions.Xavier Leroy2015-01-201-6/+0
|/ | | | | | | | | | This is achieved by declaring these functions in C2C.ml, then re-checking their declarations in the global environment during the Selection pass. In passing, the "hf" parameter for SelectLong functions was removed and replaced by fixed identifiers corresponding to the actual names of the helper functions.
* Add flags to control individual optimization passes + flag -O0 for turning ↵Xavier Leroy2014-11-161-1/+7
| | | | them off.
* Moved the timing facility to a seperate file.Bernhard Schommer2014-09-291-1/+1
|
* Add .gitignore files.Xavier Leroy2014-09-211-0/+5
|
* Rename "-fthumb" option into "-mthumb" for GCC compatibility.xleroy2014-08-191-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2572 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-2/+3
| | | | | | | | | | | | | (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
* PowerPC port: refactored the expansion of built-in functions andxleroy2014-07-281-0/+1
| | | | | | | | | | pseudo-instructions so that it does not need to be re-done in cchecklink. cchecklink: updated accordingly. testsuite: compile with -sdump and run cchecklink if supported. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2553 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ARM port: add support for Thumb2. To be tested.xleroy2014-07-271-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2549 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-05-20 07:17:53 +0000