aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Merge of branches/full-expr-4:xleroy2010-08-1856-6180/+13619
| | | | | | | | | | | | | | | | | | | | | | - Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong cast in constant_exprxleroy2010-08-041-3/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1449 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix extraction problemxleroy2010-07-142-4/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1418 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Preliminary support for gcc-style __attribute__ over typesxleroy2010-07-086-135/+168
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1377 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bug in cparser/AddCasts.ml.xleroy2010-07-084-4/+22
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1376 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Render unto Caesar... (Mention contribution by Dockins and Steward.)xleroy2010-07-081-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1375 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot to add this file. Part of the refactoring of $ARCH/$SYSTEM/Conventions.vxleroy2010-07-071-0/+251
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1372 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for inlined built-ins.xleroy2010-06-2977-1302/+1228
| | | | | | | | | | | | | AST: add ef_inline flag to external functions. Selection: recognize calls to inlined built-ins and inline them as Sbuiltin. CminorSel to Asm: added Sbuiltin/Ibuiltin instruction. PrintAsm: adapted expansion of builtins. C2Clight: adapted detection of builtins. Conventions: refactored in a machine-independent part (backend/Conventions) and a machine-dependent part (ARCH/SYS/Conventions1). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1356 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* All axioms used in the CompCert developmentxleroy2010-06-281-0/+27
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1355 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merging the Princeton implementation of the memory model. Separate axioms ↵xleroy2010-06-2812-308/+546
| | | | | | in file lib/Axioms.v. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1354 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated Caml parts to match new representation for global variables.xleroy2010-05-265-26/+57
| | | | | | | */PrintAsm.ml: watch out for large stack frames in Pallocframe. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1349 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Clean upxleroy2010-05-261-25/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1348 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo in documentationxleroy2010-05-261-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1347 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More faithful semantics for volatile reads and writes.xleroy2010-05-2336-423/+684
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1346 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-1032-351/+507
| | | | | | | | - Revised handling of volatile reads: the execution environment dictates the value read, via the trace of events. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1345 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Another regressionxleroy2010-05-103-1/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1344 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fewer float axioms.xleroy2010-05-092-6/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1343 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suppressed axioms Float.eq_zero_{true,false}, since the latter isxleroy2010-05-093-14/+8
| | | | | | | | | | wrong because of +0.0 / -0.0. Adapted Clight semantics accordingly. (Truth value of a float is defined by comparison Float.cmp Ceq with 0.0, no longer by structural equality.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised encoding/decoding of floatsxleroy2010-05-098-231/+261
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1341 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaned up handling of linker sections.xleroy2010-05-089-229/+385
| | | | | | | Minor updates on ARM code generator. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1339 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improved coalescing heuristics based on Hailperin's paper.xleroy2010-05-081-32/+49
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1338 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cosmetic: comments to mark expansions of some pseudoinstructions.xleroy2010-05-081-7/+17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1337 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updatexleroy2010-05-051-1/+24
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1336 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Strengthen chunktype inference and use it to remove some useless casts.xleroy2010-05-053-24/+142
| | | | | | | Finished proof of chunktype_compat, which was incomplete. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1335 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More theorems about sign and zero extensionsxleroy2010-05-051-0/+100
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1334 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Removed an ADMITTED that was unused, fortunatelyxleroy2010-05-051-2/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1333 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Pretty-printers for RTL and LTL. Not yet well integrated.xleroy2010-05-024-0/+235
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1332 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Compute spill costs.xleroy2010-05-021-8/+92
| | | | | | | Attempt coalescing between stack-allocated variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1331 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In compilation of Sassign, avoid systematic move from a fresh temp.xleroy2010-05-023-105/+211
| | | | | | | | | Those moves are not always coalesced during coloring. The resulting smaller RTL code also reduces the load on the rest of the back-end. RTLgenspec.v: use spiffy saturateTrans tactic to speed up proof search. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1330 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add "fabs" (floating-point absolute value) as a unary operator inxleroy2010-05-027-5/+39
| | | | | | | Clight and C#minor. Recognize __builtin_fabs and turn it into this operator. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1329 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Optimisation: addrsymbol + (expr + cst) and addrstack + (expr + cst).xleroy2010-05-022-0/+28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1328 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ARM version of Machregsauxxleroy2010-05-012-0/+59
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1327 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More struct testsxleroy2010-04-171-1/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1321 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* __builtin_memcpy, continued.xleroy2010-04-177-20/+117
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1320 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support __builtin_memcpy; use it for struct assignmentxleroy2010-04-175-30/+93
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1319 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for 1.7.1v1.7.1xleroy2010-04-131-0/+17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1317 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC: xleroy2010-04-103-3/+32
| | | | | | | | | - added __builtin_trap() - generate .size and .type directives - use natural alignment for variables git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1315 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Coloring: allow to exclude user-specified registers from allocation.xleroy2010-04-105-28/+131
| | | | | | | CPragmas (PPC/EABI only): add #pragma reserve_register git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1314 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Test bit field of size 32xleroy2010-04-093-1/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1313 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bug fix: infinite loop in cparser/ on bit field of size 32 bits.xleroy2010-04-0910-59/+53
| | | | | | | | Algorithmic efficiency: in cparser/, precompute sizeof and alignof of composites. Code cleanup: introduced Cutil.composite_info_{def,decl} git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1312 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Static initialization of structs with bitfieldsxleroy2010-04-073-1/+109
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1311 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong type for __builtin_volatile_*_int32xleroy2010-04-021-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1309 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In cparser/SimplExpr.ml:xleroy2010-04-024-12/+30
| | | | | | | | - wrong simplification of && and || in the Set case - generated nicer code for && and || in the Eval case git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1308 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser/AddCasts.ml: forgot to materialize cast at return statement.xleroy2010-04-014-13/+29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1307 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updates for release 1.7v1.7xleroy2010-03-302-9/+64
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1305 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for 1.7xleroy2010-03-302-2/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1304 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Determine endianness at run-timexleroy2010-03-301-21/+23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Options -I -D -U with a spacexleroy2010-03-301-0/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1302 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated Linux conventionsxleroy2010-03-301-3/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1301 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaner generation of .dependxleroy2010-03-302-69/+65
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-03 08:06:33 +0000