aboutsummaryrefslogtreecommitdiffstats
path: root/ia32
Commit message (Collapse)AuthorAgeFilesLines
...
| | * | Revised semantics of comparisons between a pointer and 0.Xavier Leroy2015-03-152-3/+6
| | |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It used to be that a pointer value (Vptr) always compare unequal to the null pointer (Vint Int.zero). However, this may not be true in the final machine code when pointer addition overflows and wraps around to the bit pattern 0. This patch checks the validity of the pointer being compared with 0, and makes the comparison undefined if the pointer is out of bounds. Note: only the IA32 back-end was updated, ARM and PowerPC need updating.
* | | 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
generated by cgit (git 2.34.1) at 2024-07-03 03:07:23 +0000