aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-173-3/+25
|
* Merge branch 'master' into dwarfBernhard Schommer2015-04-143-1/+5
|\
| * Harmless typo ('__' instead of '_') causing a warning at extraction time.Xavier Leroy2015-04-061-1/+1
| |
| * Missing case for the new 'annot' instruction.Xavier Leroy2015-04-062-0/+4
| |
* | Merge branch 'master' into dwarfBernhard Schommer2015-04-0247-330/+1337
|\|
| * Merge pull request #34 from AbsInt/extended-annotationsXavier Leroy2015-04-0146-327/+1332
| |\ | | | | | | Extended annotations
| | * Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-2710-73/+88
| | |
| | * Extended arguments to annotations, continued:Xavier Leroy2015-03-273-257/+133
| | | | | | | | | | | | | | | - Simplifications in RTLgen. - Updated Cexec.
| | * Extend annotations so that they can keep track of global variables and local ↵Xavier Leroy2015-03-2740-281/+1395
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-152-3/+5
| |/ | | | | | | | | | | | | | | | | | | | | 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.
* | Print all files ever encountered in the filenum.Bernhard Schommer2015-04-011-0/+7
| |
* | Added translation fucntion for declarations and fundefinitions.Bernhard Schommer2015-03-231-4/+38
| |
* | Activating the printing of the debug information for supported architecture.Bernhard Schommer2015-03-191-2/+6
| |
* | Added function to convert C types into their dwarf represnation.Bernhard Schommer2015-03-182-4/+2
| |
* | Started implementing the printing functions for the debug info. Added a ↵Bernhard Schommer2015-03-162-1/+11
| | | | | | | | global target dependend option to activate the printing only for targets wher it works.
* | Started integrating the debug printing in the common backend_printer.Bernhard Schommer2015-03-112-0/+4
| |
* | Merge remote-tracking branch 'github/backend_printer' into dwarfBernhard Schommer2015-03-103-0/+251
|\| | | | | | | | | | | | | Conflicts: arm/PrintAsm.ml ia32/PrintAsm.ml powerpc/PrintAsm.ml
| * Removed unused sel_target, changed cygwin symbol names and changed the ↵Bernhard Schommer2015-02-192-3/+2
| | | | | | | | default function aligment to be target dependent.
| * Added an elf prefix to all common elf functions in PrintAsmaux.Bernhard Schommer2015-02-182-17/+15
| |
| * Changed print_fun/var_info to be functions instead of booleans.Bernhard Schommer2015-02-182-6/+4
| |
| * Removed some style issues.Bernhard Schommer2015-02-181-65/+71
| |
| * Changed arm backend to the common backend printer.Bernhard Schommer2015-02-092-2/+2
| |
| * Changed the ia32 backend to the new Printer.Bernhard Schommer2015-02-061-0/+5
| |
| * Changed the ASM printer of the powerpc to the generalized backend.Bernhard Schommer2015-02-053-2/+119
| |
| * Moved more common functions into a seperate file.Bernhard Schommer2015-02-041-2/+46
| |
| * Started moving common backend functions into one file.Bernhard Schommer2015-02-031-0/+84
| |
* | Merge branch 'master' into dwarfBernhard Schommer2015-01-233-6/+6
|\|
| * Merge branch 'named-structs'Xavier Leroy2015-01-233-6/+6
| |\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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.
| | * Introduce symbol environments (type Senv.t) as a restricted view on global ↵Xavier Leroy2014-11-263-6/+6
| | | | | | | | | | | | environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events).
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-205-250/+273
|\| |
| * | Protect against redefinition of the __i64_xxx helper library functions.Xavier Leroy2015-01-204-244/+252
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | Follow-up to [5aecefe]: be conservative also in the case of a "common" ↵Xavier Leroy2015-01-201-6/+21
| | | | | | | | | | | | global const variable.
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-121-3/+6
|\| |
| * | More prudent analysis of uninitialized const global variables.Xavier Leroy2015-01-091-3/+6
| | | | | | | | | | | | | | | | | | | | | In the presence of separate compilation and linking, an uninitialized const global variable may be initialized elsewhere with a pointer value, falsifying the points-to analysis. Report and fix by Chung-Kil Hur and Jeehoon Kang.
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-121-0/+67
|\| | | |/ |/| | | | | Conflicts: powerpc/PrintAsm.ml
| * In -g -S mode, annotate the generated asm file with the C source code in ↵Xavier Leroy2015-01-071-0/+67
|/ | | | | | comments. Refactor printing of .loc debug directives in backend/PrintAnnot.ml
* Verification of the Unusedglob pass (removal of unreferenced static global ↵Xavier Leroy2014-11-244-95/+1401
| | | | definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
* Add Genv.public_symbol operation.Xavier Leroy2014-11-2413-56/+136
| | | | | 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-242-0/+3
| | | | For the moment, this field is ignored.
* Add flags to control individual optimization passes + flag -O0 for turning ↵Xavier Leroy2014-11-162-8/+5
| | | | them off.
* - Support "switch" statements over 64-bit integersxleroy2014-08-1713-479/+845
| | | | | | | | | | | | | (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
* Merge the various $(ARCH)/$(VARIANT)/xxx.v files into $(ARCH)/xxx.v.xleroy2014-07-231-1/+1
| | | | | | | | | The only platform where we have two variants is ARM, and it's easier to share the callling convention code between the two than to maintain both variants separately. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2540 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of "newspilling" branch:xleroy2014-07-2327-1134/+1011
| | | | | | | | | | | | | | | - 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
* Refactoring: move symbol_offset into Genv.xleroy2014-05-243-11/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-292-13/+5
| | | | | | | (Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ↵xleroy2014-04-093-32/+40
| | | | | | | | | | over booleans. Select*: more systematic constant propagation; don't CP shifts by amounts outside of [0..31]. Driver: timer for whole compilation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Reducing compilation times: (by 35% on one example)xleroy2014-04-061-20/+18
| | | | | | | | - Use a hashtable instead of an AVL set for adjSet - Inlining and algebraic simplification of spillCost into selectSpill. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2450 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch linear-typing:xleroy2014-04-066-671/+1214
| | | | | | | | | | | | | | | | | | | | | | | 1) Revised division of labor between RTLtyping and Lineartyping: - RTLtyping no longer keeps track of single-precision floats, switches from subtype-based inference to unification-based inference. - Unityping: new library for unification-based inference. - Locations: don't normalize at assignment in a stack slot - Allocation, Allocproof: simplify accordingly. - Lineartyping: add inference of locations that contain a single-precision float. - Stackingproof: adapted accordingly. This addresses a defect report whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats (see test/regression/singlefloats.c). This corresponds to commits 2435+2436 plus improvements in Lineartyping. 2) Add -dtimings option to measure compilation times. Moved call to C parser from Elab to Parse, to make it easier to measure parsing time independently of elaboration time. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2449 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Inlining: preserve all RTL regs mentioned in the function, not justxleroy2014-03-293-107/+164
| | | | | | | | those defined in the function. Semantically, both are correct, but the latter may cause RTLtyping to fail if some regs are uninitialized and a collision occurs between regs of different types. RTL: move the function resource computations there, as it could be useful for other passes some day. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2440 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):xleroy2014-03-286-1076/+661
| | | | | | | the new Lineartyping can't keep track of single floats that were spilled. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2438 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-02 01:25:36 +0000