aboutsummaryrefslogtreecommitdiffstats
path: root/ia32
Commit message (Collapse)AuthorAgeFilesLines
...
* | | Merge branch 'master' into dwarfBernhard Schommer2015-03-311-4/+15
|\| | | | | | | | | | | | | | | | | Conflicts: Makefile driver/Driver.ml
| * | Missing initialization of current_function_sig.Xavier Leroy2015-03-141-1/+3
| | |
| * | Merge branch 'master' into struct-passingXavier Leroy2015-03-143-1080/+993
| |\ \ | | | | | | | | | | | | | | | | Conflicts: ia32/PrintAsm.ml
| * \ \ Merge branch 'master' into struct-passingXavier Leroy2015-03-141-18/+10
| |\ \ \
| | * | | Removed the MinGW port.Bernhard Schommer2015-02-191-53/+3
| | | | |
| | * | | Merge github.com:AbsInt/CompCertBernhard Schommer2015-02-191-7/+7
| | |\ \ \
| | | * | | Added back symbol functions in the different printer, since they are still ↵Bernhard Schommer2015-02-191-3/+10
| | | | | | | | | | | | | | | | | | | | | | | | needed.
| | | * | | Changed the symbol function back to its old definition.Bernhard Schommer2015-02-191-10/+3
| | | | | |
| | * | | | Use lcomm instead of .local for Mingw.Bernhard Schommer2015-02-101-2/+2
| | | | | |
| | * | | | Added new Mingw Printer. Currently the only difference to the Cygwin printer ↵Bernhard Schommer2015-02-101-13/+55
| | |/ / / | | | | | | | | | | | | | | | is that every symbol must start with an "_".
| * / / / ABI compatibility for struct/union function arguments passed by value.Xavier Leroy2015-01-271-3/+14
| |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The passing of struct/union arguments by value implemented in the verified part of CompCert is not compatible with the ARM, PowerPC and x86 ABI. Here we enrich the StructReturn source-to-source emulation pass so that it implements the calling conventions defined in these ABIs. Plus: for x86, implement the returning of struct/union results by value in a way compatible with the ABI.
* | | | Merge branch 'master' into dwarfBernhard Schommer2015-03-161-1/+3
|\ \ \ \ | | |_|/ | |/| |
| * | | Missing initialization of current_function_sig.Xavier Leroy2015-03-141-1/+3
| | |/ | |/|
* | | Started implementing the printing functions for the debug info. Added a ↵Bernhard Schommer2015-03-161-0/+6
| | | | | | | | | | | | global target dependend option to activate the printing only for targets wher it works.
* | | Started integrating the debug printing in the common backend_printer.Bernhard Schommer2015-03-111-0/+7
|/ /
* | Removed unused sel_target, changed cygwin symbol names and changed the ↵Bernhard Schommer2015-02-191-3/+6
| | | | | | | | default function aligment to be target dependent.
* | Added an elf prefix to all common elf functions in PrintAsmaux.Bernhard Schommer2015-02-181-10/+13
| |
* | Changed print_fun/var_info to be functions instead of booleans.Bernhard Schommer2015-02-181-8/+8
| |
* | Removed some style issues.Bernhard Schommer2015-02-181-9/+9
| |
* | Changed arm backend to the common backend printer.Bernhard Schommer2015-02-091-1/+1
| |
* | Changed the ia32 backend to the new Printer.Bernhard Schommer2015-02-063-1030/+976
| |
* | Moved more common functions into a seperate file.Bernhard Schommer2015-02-041-56/+9
|/
* In -g -S mode, annotate the generated asm file with the C source code in ↵Xavier Leroy2015-01-071-22/+9
| | | | | | comments. Refactor printing of .loc debug directives in backend/PrintAnnot.ml
* Clean up support for common symbols. Uninitialized "const" symbols can be ↵Xavier Leroy2014-12-171-14/+44
| | | | common.
* Update the IA32/MacOS X port.Xavier Leroy2014-12-111-4/+6
| | | | | | - Prefix symbols with _ - Print indirect symbol definitions - Suppress __asm() macros in system header files
* Prevent constant propagation on Oindirectsymbol addresses.Xavier Leroy2014-12-111-2/+11
| | | | | (Otherwise they are turned into Oaddrsymbol or global addressing modes, causing linking issues on MacOS X.)
* Verification of the Unusedglob pass (removal of unreferenced static global ↵Xavier Leroy2014-11-242-67/+44
| | | | definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-4/+12
| | | | | Restrict pointer event values to public global names. Update proofs accordingly. PowerPC and ARM need updating.
* Refactored the code of ia32/PrintAsm.ml by moving the functions depending on ↵Bernhard Schommer2014-10-081-138/+220
| | | | the target system in a seperate module.
* Rename __builtin_cntlz to __builtin_clz.xleroy2014-08-272-0/+9
| | | | | | | IA32: add __builtin_clz, __builtin_ctz. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* All targets: add __builtin_membarxleroy2014-07-281-0/+3
| | | | | | | ARM: add __builtin_dsb __builtin_isb git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2554 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC port: refactored the expansion of built-in functions andxleroy2014-07-281-0/+18
| | | | | | | | | | pseudo-instructions so that it does not need to be re-done in cchecklink. cchecklink: updated accordingly. testsuite: compile with -sdump and run cchecklink if supported. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2553 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM.xleroy2014-07-281-1/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2550 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update with _a memory accessesxleroy2014-07-231-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2542 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge the various $(ARCH)/$(VARIANT)/xxx.v files into $(ARCH)/xxx.v.xleroy2014-07-232-0/+5
| | | | | | | | | The only platform where we have two variants is ARM, and it's easier to share the callling convention code between the two than to maintain both variants separately. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2540 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of "newspilling" branch:xleroy2014-07-2317-324/+698
| | | | | | | | | | | | | | | - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Refactoring: move symbol_offset into Genv.xleroy2014-05-247-75/+50
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fused multiply-add for IA32.xleroy2014-05-052-0/+35
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2481 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ia32/Select*: complete the modifications to shifts.xleroy2014-04-112-12/+20
| | | | | | | | | Makefile: missing "clean" actions. Makefile/pg/coq: honor $COQBIN if set (as suggested by P. Boutillier) to facilitate testing with different Coq versions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2453 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ↵xleroy2014-04-094-86/+138
| | | | | | | | | | over booleans. Select*: more systematic constant propagation; don't CP shifts by amounts outside of [0..31]. Driver: timer for whole compilation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support Onot operator / notl instruction. More constant propagation during ↵xleroy2014-04-0611-26/+100
| | | | | | selection. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2451 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use .comm to declare uninitialized BSS variables. xleroy2014-03-141-12/+24
| | | | | | | To do: check for MacOS X, Cygwin, and also ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2431 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Force dependency of SelectOp on Compopts.xleroy2014-03-031-0/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2428 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In Regalloc, dead code elimination, don't eliminate move operationsxleroy2014-02-231-0/+3
| | | | | | | | that pop the x87 FP stack (var <- FP0). Otherwise, (void) f(); where f returns a float eventually produces a FP stack overflow. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2416 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-193-0/+3
| | | | | | | | Refactored compilation flags that affect the Coq part (module Compopts). Added support for C99 for loops with declarations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Recognize .i and .p source files as C sources not to be preprocessed.xleroy2014-02-051-0/+1
| | | | | | | Add CompCert version number and command line as comments in generated asm. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2407 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-125-17/+9
| | | | | | | - 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-031-5/+13
| | | | | | | | | | - 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
* Updated neededness analysis for IA32.xleroy2014-01-021-37/+60
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2400 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated ARM backend wrt new static analyses and optimizations.xleroy2014-01-021-0/+12
| | | | | | | | NeedOp, Deadcode: must have distinct needs per argument of an operator. This change remains to be propagated to IA32 and PPC. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2399 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-02 23:24:24 +0000