aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Collapse)AuthorAgeFilesLines
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-125-23/+16
| | | | | | | - 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-032-26/+26
| | | | | | | | | | - 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
* Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union).xleroy2013-12-302-21/+111
| | | | | | | __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
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-282-26/+44
| | | | | | | | | | | | | | - C function types and Cminor signatures annotated by calling conventions. esp. vararg / not vararg - Cshmgen: generate correct code for function call where there are more arguments than listed in the function prototype. This is still undefined behavior according to the formal semantics, but correct code is generated. - C2C, */PrintAsm.ml: remove "printf$iif" hack. - powerpc/, checklink/: don't generate stubs for variadic functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch value-analysis.xleroy2013-12-203-68/+157
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised semantics of external functions, continued:xleroy2013-11-181-3/+10
| | | | | | | | | - Also axiomatize the semantics of inline asm - In Cexec, revised parameterization over do_external_function - In Interp.ml, matching changes + suppression of Interp_ext.ml git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2370 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised modeling of external functions and built-in functions: just axiomatizexleroy2013-11-171-114/+25
| | | | | | | them. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2369 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/: new unary operation "addsymbol"xleroy2013-11-172-18/+28
| | | | | | | | Support far-data addressing in sections. (Currently ignored in checklink.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2368 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cminor parsing and printing (from Andrew Tolmach)xleroy2013-10-161-4/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2345 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of Flocq version 2.2.0.xleroy2013-08-021-5/+0
| | | | | | | More precise modeling of NaNs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Alternate characterization of alignment constraints in memory injection, ↵xleroy2013-07-311-107/+108
| | | | | | which works better than the old one for the VST project. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2302 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-0/+12
| | | | | | | multiply-high and shifts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More accurate model of condition register flags for ARM and IA32.xleroy2013-07-131-0/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2297 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Treat casts int64 -> float32 as primitive operations instead of twoxleroy2013-07-031-0/+12
| | | | | | | | 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
* Merge of the "princeton" branch:xleroy2013-06-165-613/+689
| | | | | | | | | | | | | | - 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: xleroy2013-05-196-43/+967
| | | | | | | | - 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
* Refactoring: move definition of chunk_of_type to AST.v.xleroy2013-05-061-0/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2238 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Coq-defined equality functions for Allocation.xleroy2013-05-011-3/+20
| | | | 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.xleroy2013-04-291-4/+4
| | | | 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-208-70/+741
| | | | | | | | | 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
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-103-22/+22
| | | | | | | | 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-093-51/+79
| | | | | | | | 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
* Constant propagation within __builtin_annot.xleroy2013-02-242-9/+30
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Pointers one pastxleroy2013-02-154-65/+334
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated PowerPC port to new integers.xleroy2013-02-121-1/+1
| | | | | | | 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
* lib/Integers.v: revised and extended, faster implementation based onxleroy2013-02-102-23/+24
| | | | | | | | 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-295-66/+66
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated documentationv1.12xleroy2013-01-111-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2098 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update Cminor parser and printer so that the parser can parse the whole ↵xleroy2013-01-071-4/+4
| | | | | | 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
* Remove some useless "Require".xleroy2012-12-304-4/+0
| | | | | | | 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-291-1/+1
| | | | | | | | | | | | | | | | | | - 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
* Composition properties between injections and extensions.xleroy2012-12-291-8/+80
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2081 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integers: specialized function to compute x mod 2^N; used in "repr" toxleroy2012-12-211-1/+2
| | | | | | | | 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
* Support for inline assembly (asm statements).xleroy2012-12-183-1/+12
| | | | | | | cparser: add primitive support for enum types. bitfield emulation: for bitfields with enum type, choose signed/unsigned as appropriate git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2074 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-122-1227/+979
| | | | | | | | | | | 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
* Remove Val.is_true and Val.is_false, no longer used.xleroy2012-08-061-67/+62
| | | | | | | Simplified definition of Val.bool_of_val. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2015 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Removed old, commented-out definitions.xleroy2012-08-011-292/+30
| | | | | | | Removed axiom "traceinf_determ" and show uniqueness of behaviors up to similarity of infinite traces. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1988 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-237-107/+240
| | | | | | | | | | 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
* Revert unintentional commit #1955xleroy2012-07-061-3/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1957 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout trunk CompCertblazy2012-07-041-0/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1955 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use Flocq for floatsxleroy2012-06-281-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Make min_int / -1 and min_int % -1 semantically undefinedxleroy2012-06-091-4/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1919 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Memdata: cleanup continuedxleroy2012-05-261-178/+105
| | | | | | | 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
* CSE: add recognition of some combined operators, conditions, and addressing ↵xleroy2012-05-264-313/+174
| | | | | | | | | | 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
* Merge of the newmem branch:xleroy2012-05-214-1355/+1182
| | | | | | | | | | - 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
* Hack with nxorxleroy2012-05-181-0/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1898 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: first import of Valentin Robert's validator for asm and linkxleroy2012-03-282-4/+2
| | | | | | | cparser: renamed Errors to Cerrors; removed packing into Cparser. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJ docv1.10xleroy2012-03-121-0/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1850 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Minor updatesxleroy2012-03-111-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1848 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of Andrew Tolmach's HASP-related changesxleroy2012-03-095-105/+782
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1838 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-30 22:35:04 +0000