aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Op.v
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-291-15/+24
|\
| * PPC64: revised generation of rldic* instructionsXavier Leroy2021-10-281-15/+24
| | | | | | | | | | | | | | | | | | | | | | | | In Op.v, the definitions of is_rldl_mask and is_rldr_mask mask were swapped: - rldl is for [00001111] masks that clear on the left, hence start with 1s and finish with 0s; - rldr is for [11110000] masks that clear on the right, hence start with 0s and finish with 1s. In Asmgen.v, the case for masks of the form [00011111100] that can generate a rldic instruction was incorrectly detected.
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-081-2/+1
|\ \
| * | rm instructions now unusedDavid Monniaux2020-12-081-2/+1
| | |
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-081-17/+1
|\| |
| * | Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-081-17/+1
| |\|
| | * Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructionsXavier Leroy2020-12-061-17/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Also remove the Ofloatofint, Ofloatofintu, and Ointuoffloat PowerPC operations. The pseudoinstructions were used to implement these operations, as follows: Pfcfi : Ofloatofint i.e. the conversion signed int32 -> float64 Pfcfiu : Ofloatofintu i.e. the conversion unsigned int32 -> float64 Pfctiu : Ointuoffloat i.e. the conversion float64 -> unsigned int32 These pseudoinstructions were expanded (in Asmexpand.ml) in terms of Pfcfid : signed int64 -> float64 Pfctidz : float64 -> signed int64 and int32/int64 conversions. This commit performs this expansion during instruction selection (SelectOp.vp): floatofint(n) becomes floatoflong(longofint(n)) floatofintu(n) becomes floatoflong(longuofint(n)) intuoffloat(n) becomes cast32unsigned(longoffloat(n)) Then there is no need for the 3 removed operations and the 3 removed pseudoinstructions. More importantly, the correctness of these expansions is now proved as part of instruction selection, using the corresponding results from Floats.v.
| * | op_valid_pointer_eq ppcDavid Monniaux2020-10-191-0/+14
| | |
* | | cond_depends_onDavid Monniaux2020-12-021-7/+7
| | |
* | | cond_valid_pointer_eqDavid Monniaux2020-11-251-0/+10
| | |
* | | pointer_eq copiedDavid Monniaux2020-11-251-0/+14
|/ /
* | porting to ppc riscV x86David Monniaux2020-04-011-3/+9
| |
* | trapping opsDavid Monniaux2019-09-241-0/+24
| |
* | PowerPC compilesDavid Monniaux2019-09-071-0/+42
|/
* Implement a `Osel` operation for PowerPCXavier Leroy2019-05-201-9/+34
| | | | | This operation compiles down to an `isel` instruction (conditional move). The semantics is given by `Val.select`.
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-1/+1
| | | | Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-061-0/+23
| | | | | | | | - Add support for PowerPC, with all addressing modes. - Add support for ARM, with "reg + ofs" addressing mode. - Add support for RISC-V, with the one addressing mode. - Constprop.v: forgot to recurse in BA_addptr - volatile4 test: more tests
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-26/+252
| | | | | | | | | | | | | This commit adds code generation for 64bit PowerPC architectures which execute 32bit applications. The main difference to the normal 32bit PowerPC port is that it uses the available 64bit instructions instead of using the runtime library functions. However pointers are still 32bit and the 32bit calling convention is used. In order to use this port the target architecture must be either in Server execution mode or if in Embedded execution mode the high order 32 bits of GPRs must be implemented in 32-bit mode. Furthermore the operating system must preserve the high order 32 bits of GPRs.
* Replace 'decide equality' in powerpc/Op.v. Bug 21332Bernhard Schommer2017-04-031-4/+5
|
* Support for 64-bit architectures: update the PowerPC portXavier Leroy2016-10-011-74/+89
| | | | | The PowerPC port remains 32-bit only, no support is added for PPC 64. This shows how much work is needed to update an existing port a minima.
* bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-141-29/+29
|
* Use PowerPC 64 bits instructions (when available) for int<->FP conversions.Xavier Leroy2015-09-131-0/+16
| | | | | | Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence. Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-".
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with ↵Xavier Leroy2015-04-301-35/+35
| | | | Val.lessdef, etc.
* Ccompuimm now depends on the memory, this is needed to proof the Lemma ↵Bernhard Schommer2015-04-021-2/+3
| | | | op_depends_on_memory_correct.
* Update PowerPC port.Xavier Leroy2014-11-241-17/+39
|
* Merge of "newspilling" branch:xleroy2014-07-231-90/+47
| | | | | | | | | | | | | | | - 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-241-21/+15
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch value-analysis.xleroy2013-12-201-4/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/: new unary operation "addsymbol"xleroy2013-11-171-3/+13
| | | | | | | | Support far-data addressing in sections. (Currently ignored in checklink.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2368 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-0/+10
| | | | | | | multiply-high and shifts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "princeton" branch:xleroy2013-06-161-2/+2
| | | | | | | | | | | | | | - Define type "block" as "positive" instead of "Z". - Strengthen mem_unchanged_on so that the permissions are identical, instead of possibly increasing. - Move mem_unchanged_on from Events to Memory.Mem. - Define it in terms of mem_contents rather than in terms of Mem.load. - ExportClight: try to name temporaries introduced by SimplExpr - SimplExpr: avoid reusing temporaries between different functions, instead, thread a single generator through all functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the float32 branch: xleroy2013-05-191-17/+4
| | | | | | | | - added RTL type "Tsingle" - ABI-compatible passing of single-precision floats on ARM and x86 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Coq-defined equality functions for Allocation. (continued)xleroy2013-05-011-3/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2226 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-10/+45
| | | | | | | | | 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
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-2/+4
| | | | | | | | for no good reason. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2140 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Pointers one pastxleroy2013-02-151-50/+34
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated PowerPC port to new integers.xleroy2013-02-121-2/+1
| | | | | | | Added options -falign-branch-targets and -falign-cond-branches (experimental). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2113 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-8/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Remove some useless "Require".xleroy2012-12-301-1/+0
| | | | | | | Update ARM port. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2085 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Make min_int / -1 and min_int % -1 semantically undefinedxleroy2012-06-091-2/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1919 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* CSE: add recognition of some combined operators, conditions, and addressing ↵xleroy2012-05-261-13/+11
| | | | | | | | | | modes (cf. CombineOp.v) Memory model: cleaning up Memdata Inlining and new Constprop: updated for ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1902 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC: remove the fmadd and fmsub operators/Asm instructionsxleroy2012-03-071-10/+0
| | | | | | | | (definitely not semantics-preserving; hard to justify). CPragmas: make sure SDAs are not recognized on MacOSX. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1836 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improved instruction selection for "notint".xleroy2012-02-241-0/+15
| | | | | | | powerpc/PrintAsm.ml: fixed MacOS X problems with malloc and free git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1824 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More aggressive common subexpression elimination (CSE) of memory loads.xleroy2012-02-231-0/+55
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1823 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the nonstrict-ops branch:xleroy2012-01-141-660/+605
| | | | | | | | | | | - Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Recognition of rlwimi instruction (useful for bitfield assignment)xleroy2011-06-211-3/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1676 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch "unsigned-offsets":xleroy2011-04-091-97/+230
| | | | | | | | | | | | | | - 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
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-281-1/+4
| | | | | | | (May fail if float is too big to be converted.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1544 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the reuse-temps branch:xleroy2010-09-021-15/+75
| | | | | | | | | | | | - 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
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-26/+15
| | | | | | | | | | - Revised memory model with concrete representation of ints & floats, and per-byte access permissions - Revised Globalenvs implementation - Matching changes in all languages and proofs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-05-20 04:00:08 +0000