aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* ValueAnalysis: use ZTrees instead of ZMaps for abstracting contents of ↵Xavier Leroy2016-05-071-111/+61
| | | | | | | | memory blocks Trees are slightly more efficient than Maps, and avoid maintaining the invariant on the default value. lib/Maps: add a generic construction of a (partial) Tree module from an indexed type; use it to define ZTrees (trees indexed by Z integers).
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit ↵Xavier Leroy2016-04-279-1974/+1344
| | | | | | | | | | | | | | | | | | | 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.
* Compatibility with newer ocaml versions. Bug 18313.Bernhard Schommer2016-03-311-2/+2
|
* Merge branch 'master' into cleanupBernhard Schommer2016-03-2135-2017/+2020
|\
| * Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-2032-2010/+1996
| |\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-0632-2010/+1996
| | |
| * | Print floating-point numbers with more digits in debug outputsXavier Leroy2016-03-151-4/+4
| | | | | | | | | | | | | | | | | | 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.
| * | GPR#84: extend Cminor parser to handle single-precision FP operationsXavier Leroy2016-03-152-3/+20
| |/
* | Added interface for the Asmexpansion.Bernhard Schommer2016-03-162-0/+45
| | | | | | | | | | | | Hide the reference used internally behind the interface and added some functions to access the needed values. Bug 18394
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-1515-139/+139
| | | | | | | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* | Added back invariant checks for IRC.Bernhard Schommer2016-03-151-0/+36
| | | | | | | | | | | | Since the invariant checks are not currently used and they are not exported they are renamed to include a _ to avoid warning. Bug 18394
* | Code cleanup.Bernhard Schommer2016-03-1020-256/+166
|/ | | | | | 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.
* Print cfi_sections only if cfi is supported.Bernhard Schommer2015-12-151-0/+6
| | | | | | On older version of the binutils the cfi directives are not always supported so we only print cfi_sections if the corresponding .ini setting is set to true.
* Merge remote-tracking branch 'origin/master' into named-externalsBernhard Schommer2015-10-202-6/+6
|\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| * First step to implemente address ranges for the gnu backend.Bernhard Schommer2015-10-151-3/+3
| | | | | | | | | | | | | | | | | | In contrast to the dcc, the gcc uses address ranges to express non-contiguous range of addresses. As a first step we set the start and end addresses for the different address ranges for the compilation unit by using the start and end addresses of functions. Bug 17392.
| * More verbose debug printer.Bernhard Schommer2015-10-141-1/+1
| | | | | | | | | | | | | | | | Like, for example the clang, CompCert now prints a more detailed descriptions of the debug information in the assembler file. For each abbreviation and debug entry the dwarf attributes and their encodings are added. Bug 17392.
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-1451-3964/+3964
| |
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-1415-75/+75
| |
| * Changed definition of implem for debug information.Bernhard Schommer2015-10-121-2/+1
| | | | | | | | | | | | | | Instead of making each filed mutuable we use a reference to a record of type implem. Now only the default implementation and the default debug information need to be upated to add a new function. Bug 17392.
| * Changed expand_debug to emit less labels.Bernhard Schommer2015-10-121-0/+1
| | | | | | | | | | | | If a label is printed before a list of debug annotations we can use it for the debug annotations and don't need to add an extra label. Bug 17392
* | Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-2066-4038/+4038
| |
* | Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-115-255/+347
|/ | | | | | | | | | 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 missing functions for debug information on ia32.Bernhard Schommer2015-10-091-3/+24
| | | | | | Like for arm and ppc the functions for section names and start and end addresses of compilation units are defined and the print_annot function is moved to Asmexpandaux.ml.
* Moved expandation of debug information to Asmexpandaux.Bernhard Schommer2015-10-081-0/+69
| | | | | | The function is generalized to work for all backends and takes as additional arguments functions for the printing of the simple instructions and the translation function for the arguments.
* Ensure that there are file directives for all files used in the debugBernhard Schommer2015-10-041-7/+8
| | | | information.
* First try of debug information for gcc.Bernhard Schommer2015-10-023-69/+82
|
* Cleanup of now no longer needed functions.Bernhard Schommer2015-10-012-6/+0
|
* Only print locations for symbols that are present in the assembler.Bernhard Schommer2015-10-011-1/+2
|
* Removed newline in version string and add buildnr and tag if existing toBernhard Schommer2015-09-301-1/+1
| | | | Producer as well as target system.
* Add the version string to the printed asm.Bernhard Schommer2015-09-301-1/+6
|
* Change the way the debug sections are printed.Bernhard Schommer2015-09-281-10/+11
| | | | | | 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 printing the reference address for the LocRef and started refactoring oldBernhard Schommer2015-09-272-10/+1
| | | | | | | | Debuging code. The old functions to store the symbol for the Global variables and retrive this is no longer needed since the atom is stored in DebugInformation. Also the Debug.Abbrev module is no longer needed.
* Added support for the locations of stack allocated local variables.Bernhard Schommer2015-09-251-3/+5
| | | | | This commit adds furher support for location information for local variables and starts with the implementation of the debug_loc section.
* Merge branch 'debugscopes' into debug_locationsBernhard Schommer2015-09-231-5/+3
|\ | | | | | | | | Conflicts: cparser/Unblock.ml
| * Continuing experiment: track the scopes of local variables via __builtin_debugXavier Leroy2015-09-211-5/+3
| | | | | | | | | | | | | | | | | | | | | | | | As observed by B. Schommer, it is not enough to track scopes for every source line, as blocks can occur on a single line (think macros). Hence: - Revert debug annotations of kind 1 to contain only line number info. Generate them only when the line number changes. - Use debug annotations of kind 6 to record the list of active scopes (as BA_int integer arguments to __builtin_annot). Generate them before every nontrivial statement, even if on the same line as others. - Remove the generation of "variable x is declared in scope N" debug annotations. This can be tracked separately and more efficiently.
* | Record the scope structure during unblocking.Bernhard Schommer2015-09-221-0/+1
| | | | | | | | | | | | Instead of creating separate annotations for the local variables we call the Debug.add_lvar_scope and we construct a mapping from function id + scope id to scope information.
* | Merge branch 'debugscopes' into debug_locationsBernhard Schommer2015-09-217-18/+34
|\| | | | | | | | | | | Conflicts: debug/CtoDwarf.ml debug/DwarfPrinter.ml
| * Experiment: track the scopes of local variables via __builtin_debug.Xavier Leroy2015-09-203-4/+13
| | | | | | | | | | | | | | | | | | | | | | C2C: the code that insert debug builtins with the line numbers is now in Unblock. Handle calls to __builtin_debug. Unblock: generate __builtin_debug(1) for line numbers, carrying the list of active scopes as extra arguments. Generate __builtin_debug(6) for local variable declarations, carrying the corresponding scope number as extra argument. Constprop: avoid duplicating debug arguments that are constants already. PrintAsmaux: show this extra debug info as comments.
| * Isuue #50: outdated comment on type RTL.function.Xavier Leroy2015-09-151-2/+1
| |
| * Issue with ignoring the result of non-void builtin functions.Xavier Leroy2015-09-153-12/+20
| | | | | | | | In RTL and beyond, the result of a builtin function that has return type different from "void" must be BR, never BR_none. Otherwise, we get compile-time fatal errors, either in Asmexpand or in Lineartyping.
* | First version with computation of dwarf info from debug info.Bernhard Schommer2015-09-172-11/+4
| | | | | | | | | | Introduced a new dwarf generation from the information collected in the DebugInformation and removed the old CtODwarf translation.
* | Move more functionality in the new interface.Bernhard Schommer2015-09-161-7/+5
| | | | | | | | | | | | Added functions to add more information to the debuging interface, like the struct layout with offsets, bitifiled layout and removed the no longer needed mapping from stamp to atom.
* | Revert "Startet implementation of new Debug interface."Bernhard Schommer2015-09-102-2/+73
| | | | | | | | This reverts commit 861292a6c5e58b4f78bef207c717b801b3fc1fed.
* | Startet implementation of new Debug interface.Bernhard Schommer2015-09-062-73/+2
| | | | | | | | | | | | Added a new file debug/Debug.ml which will be the interface between for generating and printing the debuging information. Currently it contains only the code for the line directived.
* | XBernhard Schommer2015-09-0653-1486/+2732
|\| | | | | | | Merge branch 'master' into debug_locations
| * Upgrade the ARM port to the new builtins.Xavier Leroy2015-08-241-2/+4
| |
| * Some "feel good" proofs about avail sets.Xavier Leroy2015-08-231-0/+171
| |
| * Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-234-14/+817
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-2215-50/+55
| | | | | | | | | | | | | | | | Use EF_debug instead of EF_annot for line number annotations. Introduce PrintAsmaux.print_debug_info (very incomplete). powerpc/Asmexpand: revise expand_memcpy_small.
| * Simplify the handling of extended inline asm, taking advantage of the new, ↵Xavier Leroy2015-08-211-5/+24
| | | | | | | | structured builtin arguments and results.
generated by cgit (git 2.34.1) at 2024-06-30 23:39:08 +0000