aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ↵xleroy2014-04-0919-186/+489
| | | | | | | | | | 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
* Support Onot operator / notl instruction. More constant propagation during ↵xleroy2014-04-0611-26/+100
| | | | | | selection. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2451 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-0619-783/+1787
| | | | | | | | | | | | | | | | | | | | | | | 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
* "->" can also be applied to array types, not just pointer types.xleroy2014-03-301-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2442 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* __builtin_absfloat can be applied to integers too.xleroy2014-03-293-22/+60
| | | | | | | | More precise classification of float results of arithmetic operations, in preparation for future work on the C/Clight static type system. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2441 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
* C: Support array initializers that are too short + default init for remainder.xleroy2014-03-2815-197/+605
| | | | | | | | Elab: Handle C99 designated initializers. C2C, Initializers: more precise intermediate AST for initializers. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2439 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):xleroy2014-03-289-1522/+672
| | | | | | | 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
* Commentsxleroy2014-03-271-0/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2437 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Move wt_instr_inv where it belongs.xleroy2014-03-274-21/+21
| | | | | | | Update Makefile and dependencies. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2436 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised division of labor between RTLtyping and Lineartyping:xleroy2014-03-277-661/+1504
| | | | | | | | | | | | | | | | | - 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 machine registers that contain a single-precision float. - Stackingproof: adapted accordingly. This addresses a defect report by D. Dickman whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2435 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Type-checking of builtin volatile write Mfloat32 was too strict, causing ↵xleroy2014-03-242-4/+4
| | | | | | type errors after optimization. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2434 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Error messages were not displayed correctly if the main() function is ↵xleroy2014-03-211-5/+5
| | | | | | missing or has the wrong type. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2433 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support array initialization lists that are too shortxleroy2014-03-182-6/+14
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2432 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use .comm to declare uninitialized BSS variables. xleroy2014-03-141-12/+24
| | | | | | | To do: check for MacOS X, Cygwin, and also ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2431 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* floatoflong_from_words, floatoflongu_from_words : proof of PowerPc ↵jjourdan2014-03-131-89/+316
| | | | | | implementation of long <-> float conversions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2430 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* floatoflong_decomp, floatoflongu_decompjjourdan2014-03-111-0/+238
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2429 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Force dependency of SelectOp on Compopts.xleroy2014-03-033-1/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2428 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Do not transform __builtin_va_arg for a struct or union type, this causesxleroy2014-02-241-31/+37
| | | | | | | | an ugly error message in the back-end. Rather, leave it as is, and let C2C handle the error. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2422 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Silence the warning "Cannot build inversion information".xleroy2014-02-241-9/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2419 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update clightgen for CompCert 2.2.v2.2xleroy2014-02-233-17/+33
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2417 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In Regalloc, dead code elimination, don't eliminate move operationsxleroy2014-02-237-4/+21
| | | | | | | | that pop the x87 FP stack (var <- FP0). Otherwise, (void) f(); where f returns a float eventually produces a FP stack overflow. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2416 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updates for release 2.2xleroy2014-02-215-11/+34
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2415 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Beautify the output.xleroy2014-02-211-3/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2414 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong type used for transforming lval = f(...)xleroy2014-02-211-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2413 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC is big-endian, dammit.xleroy2014-02-211-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2412 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Remove useless checks on type_of_global in dynamic semanticsxleroy2014-02-208-74/+15
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2411 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-1931-97/+215
| | | | | | | | Refactored compilation flags that affect the Coq part (module Compopts). Added support for C99 for loops with declarations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for 2.2, continuedxleroy2014-02-161-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated for release 2.2.xleroy2014-02-151-13/+74
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2408 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Recognize .i and .p source files as C sources not to be preprocessed.xleroy2014-02-056-4/+47
| | | | | | | Add CompCert version number and command line as comments in generated asm. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2407 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Interp.ml: in the emulation of printf(), check formats against types of ↵xleroy2014-01-123-41/+58
| | | | | | | | | arguments. Test sizeof1: adapt to the fact that alignof(double) is either 4 or 8 depending on platform. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2406 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Better printing of integer literals: add U and LL suffixes when needed.xleroy2014-01-123-10/+27
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2405 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Eradication of Mfloat64al32, continued.xleroy2014-01-123-8/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2404 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-1231-139/+80
| | | | | | | - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Introduce and use the platform-specific Archi module giving:xleroy2014-01-0313-91/+111
| | | | | | | | | | - endianness - alignment constraints for 8-byte types (which is 4 for x86 ABI and 8 for other ABIs) - NaN handling options (superceding the Nan module, removed). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2402 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for the multiple-input-needs case.xleroy2014-01-031-40/+45
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2401 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated neededness analysis for IA32.xleroy2014-01-022-38/+74
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2400 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated ARM backend wrt new static analyses and optimizations.xleroy2014-01-0222-612/+940
| | | | | | | | NeedOp, Deadcode: must have distinct needs per argument of an operator. This change remains to be propagated to IA32 and PPC. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2399 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Incomplete types are OK for 'extern' global variables.xleroy2014-01-021-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2398 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* stdarg.h: assorted fixes for PowerPCxleroy2014-01-012-7/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2397 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc: bad use of GPR0 in va_start.xleroy2014-01-012-7/+10
| | | | | | | arm: typo. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2396 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fine hair splitting depending on whether va_list is a scalar type (IA32, ↵xleroy2014-01-015-7/+15
| | | | | | ARM) or an array type (PowerPC). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2395 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Experimental support for <stdarg.h>, the GCC way. Works on IA32. To be ↵xleroy2014-01-0117-36/+755
| | | | | | tested on PowerPC and ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2394 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Catch and report Env errors arising out of some Cutil functionsxleroy2013-12-302-8/+9
| | | | | | | (incomplete_type, sizeof, etc). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2393 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union).xleroy2013-12-3011-156/+237
| | | | | | | __builtin_memcpy_aligned now supports the case sz = 0. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2392 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Elab.ml: more warnings.xleroy2013-12-302-6/+16
| | | | | | | Cutil.ml: fix sizeof calculation of structs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2391 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improved detection of variables with incomplete types.xleroy2013-12-302-5/+12
| | | | | | | Additional warnings for empty initializer braces and zero-sized arrays. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2390 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More tolerance for functions declared without a prototypexleroy2013-12-284-10/+31
| | | | | | | | (option -funprototyped, on by default). Error if call to vararg function and -fvararg-calls is off. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2389 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-05 03:33:33 +0000