aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Asmgenproof1.v
Commit message (Expand)AuthorAgeFilesLines
* PPC64: revised generation of rldic* instructionsXavier Leroy2021-10-281-1/+1
* Share code for memory access for PowerPCBernhard Schommer2021-09-061-1/+5
* Tentative first fix for offsets of ld/std.Bernhard Schommer2021-04-241-102/+169
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-7/+7
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-23/+23
* Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructionsXavier Leroy2020-12-061-12/+0
* Model GPR0 in isel (#199)Xavier Leroy2019-09-171-1/+3
* Provide a float select operation for PowerPC. (#173)Bernhard Schommer2019-05-281-3/+38
* Emulate the "isel" instruction on non-EREF PPC processorsXavier Leroy2019-05-201-2/+2
* Implement a `Osel` operation for PowerPCXavier Leroy2019-05-201-0/+35
* PowerPC: make sure evaluation of conditions do not destroy any registerXavier Leroy2019-05-201-37/+114
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-4/+5
* Use 'gpr_or_zero' for base register of indexed load/stores, bug 24776Michael Schmidt2018-10-201-3/+8
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-6/+6
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-38/+367
* Modest optimization of leaf functions (continued)Xavier Leroy2017-04-281-0/+56
* Modest optimization of leaf functionsXavier Leroy2017-04-281-11/+70
* Support for 64-bit architectures: update the PowerPC portXavier Leroy2016-10-011-43/+82
* bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-141-146/+146
* Use PowerPC 64 bits instructions (when available) for int<->FP conversions.Xavier Leroy2015-09-131-0/+12
* powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.xleroy2014-08-181-69/+58
* Merge of "newspilling" branch:xleroy2014-07-231-64/+71
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-30/+17
* Eradication of Mfloat64al32, continued.xleroy2014-01-121-4/+0
* Future-proofing: keep signature information in IA32 and PowerPC Asm, just lik...xleroy2013-12-261-1/+1
* powerpc/: new unary operation "addsymbol"xleroy2013-11-171-32/+112
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-24/+21
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-2/+3
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-935/+489
* Updated PowerPC port to new integers.xleroy2013-02-121-5/+10
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-0/+2
* Improved instruction selection for "notint".xleroy2012-02-241-0/+5
* Merge of the nonstrict-ops branch:xleroy2012-01-141-84/+130
* Cleaned up old commented-out partsxleroy2011-08-191-10/+0
* Back from Oregon commit. xleroy2011-07-051-507/+441
* Recognition of rlwimi instruction (useful for bitfield assignment)xleroy2011-06-211-1/+21
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-3/+35
* Oaddrsymbol and small data areaxleroy2011-06-071-0/+8
* Renamed Machconcr into Machsem.xleroy2011-04-091-5/+5
* Merge of branch "unsigned-offsets":xleroy2011-04-091-26/+28
* Merge of the reuse-temps branch:xleroy2010-09-021-571/+503
* Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_extxleroy2010-08-211-35/+19
* Support for inlined built-ins.xleroy2010-06-291-1/+1
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-1/+1
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-191-7/+7
* Simplified the treatment of the PowerPC small data area; now more specific to...xleroy2009-11-021-98/+72
* Preliminary support for small data area in PowerPC port.xleroy2009-11-011-33/+65
* Storing of single floats: must insert frsp instruction before store. (Tempor...xleroy2009-10-301-11/+26
* Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >...xleroy2009-02-261-5/+29
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-29/+4