aboutsummaryrefslogtreecommitdiffstats
path: root/ia32
Commit message (Collapse)AuthorAgeFilesLines
* Adapt the PowerPC port to the new builtin representation.Xavier Leroy2015-08-211-2/+0
| | | | | | | __builtin_get_spr() and __builtin_set_spr() work, but horrible error message if the SPR argument is not a constant. powerpc/AsmToJSON.ml needs updating.
* Simplify the handling of extended inline asm, taking advantage of the new, ↵Xavier Leroy2015-08-211-3/+1
| | | | structured builtin arguments and results.
* Merge branch 'master' into 'new-builtins'Xavier Leroy2015-08-213-164/+170
|\
| * Asmexpand for ARM: fixed bug in Pfreeframe.Xavier Leroy2015-08-211-2/+2
| | | | | | | | Plus: update comments and credit Bernhard Schommer.
| * Consistent naming of "P" instructions and consistent ordering of argumentsXavier Leroy2015-08-213-174/+171
| | | | | | | | according to Intel convention (instr destination, argument).
| * Fixed bugs in asm expansion causing the test suite to fail.Xavier Leroy2015-08-211-13/+20
| | | | | | | | More bugs remain.
* | Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-218-161/+143
|/ | | | | | | | | | | | | | | | | | | | | | | | Before, the back-end languages had distinct instructions - Iannot for annotations, taking structured expressions (annot_arg) as arguments, and producing no results' - Ibuiltin for other builtins, using simple pseudoregs/locations/registers as arguments and results. This branch enriches Ibuiltin instructions so that they take structured expressions (builtin_arg and builtin_res) as arguments and results. This way, - Annotations fit the general pattern of builtin functions, so Iannot instructions are removed. - EF_vload_global and EF_vstore_global become useless, as the same optimization can be achieved by EF_vload/vstore taking a structured argument of the "address of global" kind. - Better code can be generated for builtin_memcpy between stack locations, or volatile accesses to stack locations. Finally, this commit also introduces a new kind of external function, EF_debug, which is like EF_annot but produces no observable events. It will be used later to transport debug info through the back-end, without preventing optimizations.
* Merge pull request #46 from AbsInt/asmexpandXavier Leroy2015-08-173-288/+520
|\ | | | | Merge branch 'asmexpand' of github.com:AbsInt/CompCert
| * Merge branch 'master' into asmexpandBernhard Schommer2015-07-141-0/+17
| |\
| * | Merge branch 'asmexpand' of github.com:AbsInt/CompCertBernhard Schommer2015-06-263-288/+520
| | |
| * | Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert"Bernhard Schommer2015-06-263-520/+288
| | | | | | | | | | | | | | | This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1.
| * | Moved the rest of the ia32 builtins to asmexpand.Bernhard Schommer2015-06-223-309/+290
| | |
| * | Started moving functions from TargetPrinter.ml to Asmexpand.ml for ia32.Bernhard Schommer2015-06-183-2/+253
| | |
* | | Value analysis: keep track of pointer values that leak through small ↵Xavier Leroy2015-07-192-29/+29
| | | | | | | | | | | | | | | | | | integers with Uns or Sgn abstract values. This is a follow-up to commit 2932b53. It adds provenance tracking to the Uns and Sgn abstract values.
* | | Value analysis: keep track of pointer values that leak through arithmetic ↵Xavier Leroy2015-07-191-3/+3
| |/ |/| | | | | | | | | operations with undefined behaviors. Consider (x ^ 1) ^ 1 where x is a intptr_t containing a pointer value. "x ^ 1" evaluates to Vundef in the CompCert semantics, hence the value analysis, in strict mode, gives abstract result Ifptr Pbot (= any number but not a pointer). In relaxed mode, we now give abstract result Ifptr (poffset p) where p is the abstraction of the pointer, thus keeping track of the actual leak of the pointer value.
* | Merge branch 'master' into json_exportBernhard Schommer2015-05-185-28/+54
|\|
| * Merged PrintAnnot into PrintAsmaux.Bernhard Schommer2015-05-141-4/+4
| |
| * Updated PrintOp for the single-precision FP operations.Xavier Leroy2015-05-091-0/+12
| |
| * Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-093-24/+38
| | | | | | | | | | | | | | | | | | | | - Treat clobbered registers as being destroyed by EF_inline_asm builtins (which is the truth, semantically). - To enable the above, represent clobbers as Coq strings rather than idents and move register_by_name from Machregsaux.ml to Machregs.v. - Side benefit: more efficient implementation of Machregsaux.name_of_register. -# Please enter the commit message for your changes. Lines starting
* | Merge branch 'master' into json_exportBernhard Schommer2015-05-051-35/+35
|\|
| * Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with ↵Xavier Leroy2015-04-301-35/+35
| | | | | | | | Val.lessdef, etc.
* | Added the first version of the sdump export to json.Bernhard Schommer2015-04-271-0/+17
|/
* Allow "scratch" (non-allocatable temporary registers) to be mentioned in asm ↵Xavier Leroy2015-04-232-0/+3
| | | | clobber lists.
* Take asm clobbers into account for determining callee-save registers used.Xavier Leroy2015-04-232-0/+8
|
* Cleanups and updates for extended asm.Xavier Leroy2015-04-211-2/+1
|
* Support for GCC-style extended asm, continued:Xavier Leroy2015-04-212-3/+3
| | | | | | | | - support "r", "m" and "i" constraints - support "%Q" and "%R" modifiers for register pairs - support register clobbers - split off analysis and transformation of asm statements in cparser/ExtendedAsm.ml
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-172-2/+7
|
* Added missing dummy functions.Bernhard Schommer2015-04-161-0/+8
|
* Merge branch 'master' into dwarfBernhard Schommer2015-04-028-62/+62
|\
| * Merge pull request #34 from AbsInt/extended-annotationsXavier Leroy2015-04-016-59/+56
| |\ | | | | | | Extended annotations
| | * Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-271-1/+1
| | |
| | * Extend annotations so that they can keep track of global variables and local ↵Xavier Leroy2015-03-275-58/+55
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | variables whose address is taken. - CminorSel, RTL: add "annot" instructions. - CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions. - AST, Events: simplify EF_annot because constants are now part of the arguments. Implementation is not complete yet.
| * | Merge pull request #31 from AbsInt/null-ptr-cmpXavier Leroy2015-04-012-3/+6
| |\ \ | | | | | | | | Revised semantics of comparisons between a pointer and 0.
| | * | 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.
generated by cgit (git 2.34.1) at 2024-07-01 06:20:12 +0000