summaryrefslogtreecommitdiff
path: root/lib
Commit message (Collapse)AuthorAge
* Merge of the "alignas" branch.Gravatar xleroy2013-10-05
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Slightly more efficient conversion positive <-> intGravatar xleroy2013-09-26
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2335 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Small improvements in compilation times for the register allocation pass.Gravatar xleroy2013-09-20
| | | | | | | Maps.v: add a PTree.fold1 operation that doesn't maintain the key. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2329 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms Gravatar xleroy2013-09-14
| | | | | | | | | are necessary, only two parameters (default_pl and choose_binop_pl). SelectDiv: optimize FP division by a power of 2. ConstpropOp: optimize 2.0 * x and x * 2.0 into x + x. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2326 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplify LPMap by smashing bottoms.Gravatar xleroy2013-08-12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2306 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of Flocq version 2.2.0.Gravatar xleroy2013-08-02
| | | | | | | More precise modeling of NaNs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Optimize integer divisions by positive constants, turning them intoGravatar xleroy2013-07-29
| | | | | | | multiply-high and shifts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add another expansion of shrx in terms of shifts and adds (from Hacker's ↵Gravatar xleroy2013-07-28
| | | | | | Delight). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2299 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More properties about subtraction and borrow.Gravatar xleroy2013-07-15
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2298 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More accurate model of condition register flags for ARM and IA32.Gravatar xleroy2013-07-13
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2297 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of int->float conversions:Gravatar xleroy2013-07-08
| | | | | | | | | | - introduce Float.floatofint{,u} and use it in the semantics of C - prove that it is equivalent to int->double conversion followed by double->float rounding, and use this fact to justify code generation in Cshmgen. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2294 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Treat casts int64 -> float32 as primitive operations instead of twoGravatar xleroy2013-07-03
| | | | | | | | casts int64 -> float64 -> float32. The latter causes double rounding errors. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2290 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update LICENSE file and headers for dual-licensed files.Gravatar xleroy2013-06-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2280 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "princeton" branch:Gravatar xleroy2013-06-16
| | | | | | | | | | | | | | - Define type "block" as "positive" instead of "Z". - Strengthen mem_unchanged_on so that the permissions are identical, instead of possibly increasing. - Move mem_unchanged_on from Events to Memory.Mem. - Define it in terms of mem_contents rather than in terms of Mem.load. - ExportClight: try to name temporaries introduced by SimplExpr - SimplExpr: avoid reusing temporaries between different functions, instead, thread a single generator through all functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the float32 branch: Gravatar xleroy2013-05-19
| | | | | | | | - added RTL type "Tsingle" - ABI-compatible passing of single-precision floats on ARM and x86 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Coq-defined equality functions for Allocation.Gravatar xleroy2013-05-01
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2225 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Expand 64-bit integer comparisons into 32-bit integer comparisons.Gravatar xleroy2013-04-29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Decomposing 64-bit "less than" comparisons.Gravatar xleroy2013-04-29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2217 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:Gravatar xleroy2013-04-20
| | | | | | | | | 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
* Assorted changes to reduce stack and heap requirements when compiling very ↵Gravatar xleroy2013-03-16
| | | | | | big functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2151 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bind some local defs with Let, makes extracted code cleanerGravatar xleroy2013-03-12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2148 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Maps: revised TREE interface; added mucho derived properties and operations ↵Gravatar xleroy2013-03-12
| | | | | | | | | in Tree_Properties. Lattice: adapted accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2147 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Useless ImportGravatar xleroy2013-03-10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2141 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Glasnost: making transparent a number of definitions that were opaqueGravatar xleroy2013-03-10
| | | | | | | | 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 Gravatar xleroy2013-03-09
| | | | | | | | 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
* Updated PowerPC port to new integers.Gravatar xleroy2013-02-12
| | | | | | | Added options -falign-branch-targets and -falign-cond-branches (experimental). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2113 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot theorem "sign_ext_narrow".Gravatar xleroy2013-02-12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2111 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* lib/Integers.v: revised and extended, faster implementation based onGravatar xleroy2013-02-10
| | | | | | | | 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
* Some more properties. Refactored some proofs.Gravatar xleroy2013-02-04
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2109 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Camlcoq.ml: bug in conversion Z to stringGravatar xleroy2013-01-29
| | | | | | | PrintClight: forgot "$" prefix on temporary names git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2102 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.Gravatar xleroy2013-01-29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Remove some useless "Require".Gravatar xleroy2012-12-30
| | | | | | | 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:Gravatar xleroy2012-12-29
| | | | | | | | | | | | | | | | | | - 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
* Integers: specialized function to compute x mod 2^N; used in "repr" toGravatar xleroy2012-12-21
| | | | | | | | avoid the cost of a general Zmod. Memdata: updated accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2077 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)Gravatar xleroy2012-11-03
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2065 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch seq-and-or. See Changelog for details.Gravatar xleroy2012-10-06
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Micro-optimization of (x & mask) >>s amount into a rolm when mask >= 0.Gravatar xleroy2012-07-09
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1963 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Process successors in increasing order. Helps preserving the nice CFGGravatar xleroy2012-07-01
| | | | | | | | structure that we got from Cminorgen. Otherwise, the linearization heuristic can produce rather bad code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1948 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Changelog: updatedGravatar xleroy2012-06-28
| | | | | | | | | | driver/Interp.ml: clean up dead code lib/Integers.v: add shifted_or_is_add lib/Floats.v: add from_words_eq .depend: updated git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1940 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use Flocq for floatsGravatar xleroy2012-06-28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More properties on mul/div/modGravatar xleroy2012-06-09
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1918 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Memdata: cleanup continuedGravatar xleroy2012-05-26
| | | | | | | Maps: add filter1 operation (could be useful some day) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1903 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the newmem branch:Gravatar xleroy2012-05-21
| | | | | | | | | | - 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
* More aggressive common subexpression elimination (CSE) of memory loads.Gravatar xleroy2012-02-23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1823 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the nonstrict-ops branch:Gravatar xleroy2012-01-14
| | | | | | | | | | | - 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 charsGravatar xleroy2011-10-18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Changelog, doc: updated for release 1.9Gravatar xleroy2011-08-22
| | | | | | | lib/Integers, Makefile: unsuccessful experiments with coqchk git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1723 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaned up old commented-out partsGravatar xleroy2011-08-19
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1719 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch new-semantics: revised and strengthened top-level statements ↵Gravatar xleroy2011-07-15
| | | | | | of semantic preservation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Back from Oregon commit. Gravatar xleroy2011-07-05
| | | | | | | | | powerpc/*: better compilation of some comparisons; revised asmgenproof1. common/*: added Mem.storebytes; used to give semantics to memcpy builtin. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1679 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 02:21:56 +0000