aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* Coq-defined equality functions for Allocation.xleroy2013-05-012-26/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2225 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Removing modules now unusedxleroy2013-05-016-2822/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2224 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-2910-249/+506
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-2060-7040/+9462
| | | | | | | | | 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* RTLtyping: now performed entirely in Coq, no need for an external Caml ↵xleroy2013-03-222-371/+713
| | | | | | oracle + a validator. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2157 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More aggressive CSE across Ibuiltin.xleroy2013-03-172-7/+34
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2152 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Assorted changes to reduce stack and heap requirements when compiling very ↵xleroy2013-03-1624-207/+389
| | | | | | big functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2151 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Machsem: no longer useful.xleroy2013-03-141-259/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2150 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-106-22/+12
| | | | | | | | for no good reason. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2140 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in xleroy2013-03-091-0/+4
| | | | | | | | submodules. (Extraction does not remove them, then.) common/Switch: replaced use of FMaps by our own Maps. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2139 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Finished backtracking (cf previous commit) for ARM and PowerPC.xleroy2013-03-041-11/+16
| | | | | | | ARM: slightly shorter code generated for indirect memory accesses. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2137 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Partial backtracking on previous commit: the "hole in Mach stack frame" xleroy2013-03-033-574/+522
| | | | | | | | trick prevents a future mapping of the Mach/Asm call stack as a single block. IA32 is fixed, PowerPC and ARM remains to be done. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2136 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-015-523/+1371
| | | | | | | | | | - no more prediction of return addresses (Asmgenretaddr is gone) - instead, punch a hole for the retaddr in Mach stack frame and fill this hole with the return address in the Asmgen proof. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Constant propagation within __builtin_annot.xleroy2013-02-244-7/+185
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Pointers one pastxleroy2013-02-154-12/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* lib/Integers.v: revised and extended, faster implementation based onxleroy2013-02-101-5/+5
| | | | | | | | bit-level operations provided by ZArith in Coq 8.4. Other modules: adapted accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2110 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-2919-120/+104
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Quote idents for safe re-parsingxleroy2013-01-081-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2096 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update Cminor parser and printer so that the parser can parse the whole ↵xleroy2013-01-073-32/+101
| | | | | | Cminor language and can reparse the output of the printer. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2090 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* RTLgenaux: heuristic to orient if-then-else statements based on sizes.xleroy2012-12-311-1/+58
| | | | | | | Makefile: coqchk notes git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2086 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Remove some useless "Require".xleroy2012-12-3045-90/+6
| | | | | | | Update ARM port. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2085 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the clightgen branch:xleroy2012-12-299-138/+148
| | | | | | | | | | | | | | | | | | - Alternate semantics for Clight where function parameters are temporaries, not variables - New pass SimplLocals that turns non-addressed local variables into temporaries - Simplified Csharpminor, Cshmgen and Cminorgen accordingly - SimplExpr starts its temporaries above variable names, therefoe Cminorgen no longer needs to encode variable names and temps names. - Simplified Cminor parser & printer, as well as Errors, accordingly. - New tool clightgen to produce Clight AST in Coq-parsable .v files. - Removed side condition "return type is void" on rules skip_seq in the semantics of CompCert C, Clight, C#minor, Cminor. - Adapted RTLgenproof accordingly (now uses a memory extension). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2083 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Separate interference graphs for ints and floats, i.e. don't record ↵xleroy2012-12-201-13/+16
| | | | | | interference edges between nodes of different types: this is useless and falsifies the heuristics based on node degree. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-1218-148/+127
| | | | | | | | | | | function definition, so that comparisons between function pointers are correctly defined. AST, Globalenvs, and many other files: represent programs as a list of (function or variable) definitions instead of two lists, one for functions and the other for variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-0612-521/+114
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Define useful functions instr_defs and instr_usesxleroy2012-08-101-0/+35
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2020 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Remove Val.is_true and Val.is_false, no longer used.xleroy2012-08-061-16/+6
| | | | | | | Simplified definition of Val.bool_of_val. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2015 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated documentationxleroy2012-08-021-28/+19
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1989 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More aggressive elimination of conditional branches during constantxleroy2012-08-012-201/+228
| | | | | | | | | propagation, taking better advantage of inferred constants. Helps with the compilation of && and || operators. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1987 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-235-4/+12
| | | | | | | | | | injections compose (Values, Memdata, Memory) - Memory chunks: Mfloat64 now has alignment 8; introduced Mfloat64al32 that works like old Mfloat64 (i.e. has alignment 4); simplified handling of memcpy builtin accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1983 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for indirect symbols under MacOS X (final).xleroy2012-07-141-0/+11
| | | | | | | Remove stdio hack in runtime/ git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1979 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for MacOS X's indirect symbols. (first try)xleroy2012-07-131-11/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1978 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated ARM port.xleroy2012-07-101-6/+0
| | | | | | | CSE.v: removed commented-out stuff. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1966 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use Flocq for floatsxleroy2012-06-283-9/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* CSE: add recognition of some combined operators, conditions, and addressing ↵xleroy2012-05-266-83/+213
| | | | | | | | | | modes (cf. CombineOp.v) Memory model: cleaning up Memdata Inlining and new Constprop: updated for ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1902 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More efficient implementation of reg_valnumxleroy2012-05-222-90/+168
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1900 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the newmem branch:xleroy2012-05-2119-258/+3659
| | | | | | | | | | - Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Minor updatesxleroy2012-03-111-1/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1848 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Proof didn't go through for ARMxleroy2012-03-111-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1847 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Another update from Andrew Tolmachxleroy2012-03-091-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1840 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PrintCminor: printing Sskipxleroy2012-03-091-1/+1
| | | | | | | test/cminor: updating git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1839 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of Andrew Tolmach's HASP-related changesxleroy2012-03-094-20/+120
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1838 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Take advantage of Cmaskzero and Cmasknotzero.xleroy2012-02-242-11/+14
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1825 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More aggressive common subexpression elimination (CSE) of memory loads.xleroy2012-02-232-224/+357
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1823 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "volatile" branch:xleroy2012-02-046-2/+66
| | | | | | | | | | | | - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/SelectOp: optimize the pattern ((x >>s N) & N1) & N2 common in a ↵xleroy2012-01-211-11/+28
| | | | | | | | | certain customer's code backend/Coloringaux: avoid spilling the dummy result registers for built-ins that have no result. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1799 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added volatile_read_global and volatile_store_global builtins.xleroy2012-01-152-3/+10
| | | | | | | Finished updating IA32 and ARM ports. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1792 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the nonstrict-ops branch:xleroy2012-01-1416-1300/+570
| | | | | | | | | | | - Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-188-24/+23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Harden proof script against empty destroyed_at_movexleroy2011-08-221-7/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1721 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-29 03:39:16 +0000