aboutsummaryrefslogtreecommitdiffstats
path: root/arm/PrintAsm.ml
Commit message (Collapse)AuthorAgeFilesLines
* Add __builtin_bswap16 and __builtin_bswap32 to all ports.xleroy2013-04-201-44/+4
| | | | | | | | | 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-70/+91
| | | | | | | | | 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
* Bug in Pbtblxleroy2013-03-011-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2133 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-3/+4
| | | | | | | | | | - 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
* Updated ARM and PowerPC ports with new handling of __builtin_annot.xleroy2013-02-241-39/+59
| | | | | | | 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-24/+4
| | | | 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-2/+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
* Remove some useless "Require".xleroy2012-12-301-2/+3
| | | | | | | Update ARM port. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2085 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-9/+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
* - 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
* Strip quotes from section names during #pragma parsing.xleroy2012-07-111-1/+1
| | | | | | | | | 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
* Updated ARM port.xleroy2012-07-101-10/+10
| | | | | | | CSE.v: removed commented-out stuff. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1966 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/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use freg <-> 2 ireg move instructions to fix up calling conventionsxleroy2012-05-181-4/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1895 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for fcmpzd instruction (float compare with +0.0)xleroy2012-03-291-5/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1858 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplified and cleaned up the passing of information from C2C to PrintAsm, ↵xleroy2012-02-221-4/+7
| | | | | | as well as the handling of sections. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1822 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-181-3/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* arm/PrintAsm: don't generate "vfd" directive, useless?xleroy2011-08-221-1/+1
| | | | | | | cparser: distinguish more carefully between lvalues and modifiable lvalues. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1722 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More builtins for ARM and PowerPCxleroy2011-08-051-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1697 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* arm/PrintAsm: bugs in expansion of new builtinsxleroy2011-08-051-3/+4
| | | | | | | test/: testing the builtins git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1696 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ARM: added reversed load/store builtins + bswap builtin (to be tested)xleroy2011-07-301-0/+36
| | | | | | | | IA32: added bswap builtin Updated Changelog git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1693 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ARM codegen ported to new ABI + VFD floatsxleroy2011-07-301-136/+139
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1692 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo in arm/PrintAsm.mlxleroy2011-07-281-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1690 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added animation of the CompCert C semantics (ccomp -interp)xleroy2011-07-281-61/+48
| | | | | | | | 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-59/+102
| | | | | | 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/+3
| | | | | | | 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-62/+89
| | | | | | | | | | (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
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).xleroy2011-05-081-18/+5
| | | | | | | | | | Added -dmach option and corresponding printer for Mach code. CleanupLabelsproof.v: fixed for ARM Driver.ml: -E sends output to stdout; support for .s and .S source files. cparser/Elab.ml: spurious comment deleted. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1648 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typosxleroy2011-04-191-8/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1640 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixed some typos.xleroy2011-04-171-13/+26
| | | | | | | Avoid generation of stubs for external functions without float arguments. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1639 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Preliminary support for 'aligned' and 'section' attributes, gcc-style. ↵xleroy2011-04-161-9/+39
| | | | | | 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-20/+11
| | | | | | | | | | | | | | - 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
* Merge of the reuse-temps branch:xleroy2010-09-021-24/+5
| | | | | | | | | | | | - 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
* Adding __builtin_annotationxleroy2010-09-011-1/+33
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Renamed C2Clight into C2Cxleroy2010-08-181-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1468 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for inlined built-ins.xleroy2010-06-291-34/+50
| | | | | | | | | | | | | 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
* Updated Caml parts to match new representation for global variables.xleroy2010-05-261-6/+15
| | | | | | | */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
* Revised encoding/decoding of floatsxleroy2010-05-091-2/+2
| | | | 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-081-11/+17
| | | | | | | Minor updates on ARM code generator. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1339 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support __builtin_memcpy; use it for struct assignmentxleroy2010-04-171-0/+29
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1319 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Pretty stringsxleroy2010-03-291-3/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1298 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated ARM asm printerxleroy2010-03-281-4/+67
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1294 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suppressed Init_pointer, now useless. Improved printing of strings in ↵xleroy2010-03-031-17/+1
| | | | | | generated .s git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1274 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated ARM asm printerxleroy2010-01-251-5/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1233 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated ARM portxleroy2010-01-251-2/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1232 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added support for jump tables.xleroy2009-11-191-0/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1181 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support Clight initializers of the form "int * x = &y;".xleroy2009-11-011-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1162 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-03 04:34:13 +0000