aboutsummaryrefslogtreecommitdiffstats
path: root/ia32/PrintAsm.ml
Commit message (Collapse)AuthorAgeFilesLines
* Add __builtin_bswap16 and __builtin_bswap32 to all ports.xleroy2013-04-201-23/+5
| | | | | | | | | Remove __builtin_{read,write}_reversed from IA32 and ARM ports. Machregs: tighten destroyed_by_builtin Packedstructs: use bswap if read/write-reversed not available. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2208 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-83/+81
| | | | | | | | | 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
* Updated ARM and PowerPC ports with new handling of __builtin_annot.xleroy2013-02-241-2/+2
| | | | | | | ARM: add support for builtin_volatile_{read,write}_global, after all. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2127 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Constant propagation within __builtin_annot.xleroy2013-02-241-25/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Errors for excessively large global variables or stack frames.xleroy2013-02-021-3/+2
| | | | | | | test/: update Makefiles so that "all" is the default target. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2107 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for inline assembly (asm statements).xleroy2012-12-181-0/+4
| | | | | | | 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-121-8/+8
| | | | | | | | | | | 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-061-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixed 2 errors in revised builtin_vstore. xleroy2012-08-221-2/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2035 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong usage of temps in builtin_volatile_write.xleroy2012-08-171-12/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2030 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-2/+2
| | | | | | | | | | 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-1/+1
| | | | | | | 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-0/+20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1978 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Strip quotes from section names during #pragma parsing.xleroy2012-07-111-3/+3
| | | | | | | | | Reinstall the quotes when printing asm. The idea is that .sdump files now contain unquoted section names, which is easier on cchecklink. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1967 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added option -falign-functionsxleroy2012-07-011-1/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use Flocq for floatsxleroy2012-06-281-4/+8
| | | | 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-11/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1919 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplified and cleaned up the passing of information from C2C to PrintAsm, ↵xleroy2012-02-221-8/+10
| | | | | | as well as the handling of sections. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1822 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added volatile_read_global and volatile_store_global builtins.xleroy2012-01-151-30/+67
| | | | | | | Finished updating IA32 and ARM ports. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1792 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-181-5/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised emulation of packed structsxleroy2011-10-161-4/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1729 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Watch out for min_int / -1xleroy2011-08-271-1/+11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1727 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More careful treatment of 'load immediate 0' as 'xor self'xleroy2011-08-181-12/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1718 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot to update: adding xchg instructionxleroy2011-08-161-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1712 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* IA32 PrintAsm.ml: wrong moves generated in print_builtin_memcpy_bigxleroy2011-08-101-8/+20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1706 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaned up handling of composite conditionsxleroy2011-08-051-31/+16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1699 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ARM: added reversed load/store builtins + bswap builtin (to be tested)xleroy2011-07-301-0/+5
| | | | | | | | IA32: added bswap builtin Updated Changelog git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1693 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added animation of the CompCert C semantics (ccomp -interp)xleroy2011-07-281-64/+45
| | | | | | | | test/regression: int main() so that interpretation works Revised once more implementation of __builtin_memcpy (to check for PPC & ARM) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1688 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of annotation statements, and more generally built-in ↵xleroy2011-06-131-40/+82
| | | | | | functions, and more generally external functions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Nicer printing of annotations.xleroy2011-05-231-5/+30
| | | | | | | ia32: support builtins for reversed reads and writes (facilitates testing). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1655 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser/StructAssign: always use __builtin_memcpy + alignment indicationxleroy2011-05-111-48/+101
| | | | | | | | | | (simpler and globally more efficient) cfrontend/C2C.ml: specialization of __builtin_memcpy over size */PrintAsm.ml: revised expansion of __builtin_memcpy_* ia32/Asm.ml: typo in comment git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1649 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added pass CleanupLabels to remove unreferenced labels in a proved way.xleroy2011-05-081-16/+3
| | | | | | | | | | ia32/PrintAsm.ml: simplified accordingly; other PrintAsm.ml to be fixed. ia32/Asm.v: Pmov_ri can undef flags (if translated to xor) cparser/Ceval.ml: treat ~ in constant exprs git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser/Elab: __attribute, not attributexleroy2011-04-161-2/+2
| | | | | | | | ia32/PrintAsm: wrong section name regression: added test attribs1 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1636 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Preliminary support for 'aligned' and 'section' attributes, gcc-style. ↵xleroy2011-04-161-23/+47
| | | | | | New-style handling of sections for IA32 and ARM. Work in progress, to be tested. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1635 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch "unsigned-offsets":xleroy2011-04-091-10/+10
| | | | | | | | | | | | | | - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use movapd instead of movsd for xmm reg-reg move: it avoids partial register ↵xleroy2010-11-281-1/+1
| | | | | | stalls, resulting in tiny speedups. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1556 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improvements for int8 and int16 storesxleroy2010-09-101-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1507 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updates for IA32-Cygwin.xleroy2010-09-081-9/+9
| | | | | | | | cparser/Elab.ml: tolerate changes in qualifiers in ?: cfrontend/C2C.ml: revise info attached to atoms; treat inline functions as static. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1506 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update: adding __builtin_annotationxleroy2010-09-041-1/+36
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for __builtin_fmax and __builtin_fminxleroy2010-09-041-1/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1501 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the reuse-temps branch:xleroy2010-09-021-0/+625
- Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-03 01:29:59 +0000