1473def sm121LowerExpand =
1474 (lambda unrestricted context : (family SM121LowerContext) .
1475 (lambda unrestricted index : Nat .
1476 (lambda unrestricted targets : (family SM121LowerRegisters) .
1477 (lambda unrestricted item : (family SM121LowerDecoded) .
1478 (eliminate
1479 SM121LowerContext
1480 (lambda unrestricted current : (family SM121LowerContext) . (family SM121LowerExpansion))
1481 context
1482 (branch SM121LowerContextValue barrier free freePair count addressing waitAll .
1483 (eliminate
1484 SM121LowerDecoded
1485 (lambda unrestricted current : (family SM121LowerDecoded) . (family SM121LowerExpansion))
1486 item
1487 (branch SM121LowerDecodedValue low high guardReads shape .
1488 (eliminate
1489 SM121LowerShape
1490 (lambda unrestricted current : (family SM121LowerShape) . (family SM121LowerExpansion))
1491 shape
1492 (branch SM121LowerShapeValue rule class reads writes predicateWrites .
1493 -- the first op an instruction lowers to carries its label, and
1494 -- the join mark when a branch targets it
1495 (let unrestricted label = (succ index) in
1496 (let unrestricted join = (sm121LowerHas targets index) in
1497 (let unrestricted plainWith =
1498 (lambda unrestricted opLabel : Nat .
1499 (lambda unrestricted opJoin : Nat .
1500 (lambda unrestricted opTarget : Nat .
1501 (lambda unrestricted opLow : Nat .
1502 (lambda unrestricted opHigh : Nat .
1503 (lambda unrestricted opReads : (family SM121LowerRegisters) .
1504 (constructor SM121LowerOp SM121LowerOpValue opLow opHigh class opReads writes
1505 guardReads predicateWrites zero opLabel opJoin opTarget))))))) in
1506 (let unrestricted plain = (plainWith label join zero) in
1507 (let unrestricted plainAfter = (plainWith zero zero zero) in
1508 -- LDC / LDC.64 Rd, c[bank][offset], under the instruction's
1509 -- guard, on the free scoreboard; it keeps the instruction's
1510 -- waits: it writes the destination before the instruction did
1511 (let unrestricted constantLoad =
1512 (lambda unrestricted width : Nat .
1513 (lambda unrestricted target : Nat .
1514 (constructor SM121LowerOp SM121LowerOpValue
1515 (nat-add
1516 (nat-add
1517 (nat-add sm121LowerOpcodeConstantLoad
1518 (nat-multiply (sm121LowerField low sm121LowerGuardPlace sm121LowerGuardSpan) sm121LowerGuardPlace))
1519 (nat-add (nat-multiply target sm121LowerDestinationPlace)
1520 (nat-multiply sm121LowerZeroRegister sm121LowerSourcePlace)))
1521 (nat-add
1522 (nat-multiply
1523 (sm121LowerField low sm121LowerConstantOffsetPlace sm121LowerConstantOffsetSpan)
1524 sm121LowerConstantOffsetPlace)
1525 (nat-multiply
1526 (sm121LowerField low sm121LowerConstantBankPlace sm121LowerConstantBankSpan)
1527 sm121LowerConstantBankPlace)))
1528 (nat-add
1529 (nat-add
1530 (nat-add (nat-multiply width sm121LowerConstantWidthPlace)
1531 (nat-multiply (sm121LowerMaximum 1 (sm121LowerStall high)) sm121LowerStallPlace))
1532 (nat-add
1533 (nat-multiply (sm121LowerField high sm121LowerYieldPlace sm121LowerYieldSpan)
1534 sm121LowerYieldPlace)
1535 (nat-multiply barrier sm121LowerWriteBarrierPlace)))
1536 (nat-add
1537 (nat-multiply sm121LowerNoBarrier sm121LowerReadBarrierPlace)
1538 (nat-multiply (sm121LowerField high sm121LowerWaitPlace sm121LowerWaitSpan)
1539 sm121LowerWaitPlace)))
1540 (constructor SM121LowerClass SM121LowerVariable)
1541 sm121LowerNone
1542 (sm121LowerSpan target (nat-subtract width sm121LowerConstantWidthBase))
1543 guardReads
1544 sm121LowerNone
1545 1
1546 label join zero))) in
1547 (let unrestricted destination =
1548 (sm121LowerField low sm121LowerDestinationPlace sm121LowerRegisterSpan) in
1549 (eliminate
1550 SM121LowerRule
1551 (lambda unrestricted current : (family SM121LowerRule) . (family SM121LowerExpansion))
1552 rule
1553 (branch SM121LowerRuleSame . (sm121LowerOnly (plain low high reads)))
1554 (branch SM121LowerRuleConstantMove .
1555 (sm121LowerOnly (constantLoad sm121LowerConstantWord destination)))
1556 (branch SM121LowerRuleConstantMultiplyAdd .
1557 (let unrestricted clash = (sm121LowerHas reads destination) in
1558 (let unrestricted target = (naturalSelect clash free destination) in
1559 (sm121LowerSelectLazy (family SM121LowerExpansion)
1560 (naturalAnd clash (naturalEqual free count))
1561 (lambda unrestricted u : Nat . (sm121LowerRefuse (constructor SM121LowerRefusal SM121LowerRefusedNoFreeRegister)))
1562 (lambda unrestricted u : Nat . (sm121LowerPair
1563 (constantLoad sm121LowerConstantWord target)
1564 (plainAfter
1565 (sm121LowerWithField
1566 (sm121LowerRegisterForm low sm121LowerOpcodeMultiplyAddRegister)
1567 sm121LowerSecondSourcePlace sm121LowerRegisterSpan target)
1568 high
1569 (sm121LowerCons target reads))))))))
1570 (branch SM121LowerRuleConstantMultiplyAddWide .
1571 (let unrestricted clash =
1572 (naturalOr (sm121LowerHas reads destination) (sm121LowerHas reads (succ destination))) in
1573 (let unrestricted target = (naturalSelect clash freePair destination) in
1574 (sm121LowerSelectLazy (family SM121LowerExpansion)
1575 (naturalAnd clash (naturalEqual freePair (nat-subtract count 1)))
1576 (lambda unrestricted u : Nat . (sm121LowerRefuse (constructor SM121LowerRefusal SM121LowerRefusedNoFreePair)))
1577 (lambda unrestricted u : Nat . (sm121LowerPair
1578 (constantLoad sm121LowerConstantPair target)
1579 (plainAfter
1580 (sm121LowerWithField
1581 (sm121LowerRegisterForm low sm121LowerOpcodeMultiplyAddWideRegister)
1582 sm121LowerSecondSourcePlace sm121LowerRegisterSpan
1583 (sm121LowerField high sm121LowerThirdSourcePlace sm121LowerRegisterSpan))
1584 (sm121LowerWithField high sm121LowerThirdSourcePlace sm121LowerRegisterSpan target)
1585 (sm121LowerCons target (sm121LowerCons (succ target) reads)))))))))
1586 (branch SM121LowerRuleReduction .
1587 (sm121LowerOnly
1588 (plain
1589 (sm121LowerWithField low 1 sm121LowerOpcodeSpan sm121LowerOpcodeReduceGlobal)
1590 (sm121LowerWithField high 1 sm121LowerHalfWordSpan sm121LowerReduceGlobalModifiers)
1591 reads)))
1592 (branch SM121LowerRuleShared .
1593 (sm121LowerRebaseShared low
1594 (eliminate
1595 SM121SharedAddressing
1596 (lambda unrestricted current : (family SM121SharedAddressing) . Nat)
1597 addressing
1598 (branch SM121SharedAddressScaled . high)
1599 (branch SM121SharedAddressBytes .
1600 (sm121LowerWithField high sm121LowerSharedScalePlace 2 zero)))
1601 plain reads))
1602 (branch SM121LowerRuleSharedMatrix . (sm121LowerRebaseShared low high plain reads))
1603 (branch SM121LowerRuleAsyncCopy .
1604 (let unrestricted offset =
1605 (nat-add sm121LowerSharedBase
1606 (sm121LowerField low sm121LowerAsyncCopyOffsetPlace sm121LowerAsyncCopyOffsetSpan)) in
1607 (sm121LowerSelect (family SM121LowerExpansion)
1608 (nat-less-than offset sm121LowerAsyncCopyOffsetLimit)
1609 (sm121LowerOnly
1610 (plain
1611 (sm121LowerWithField low sm121LowerAsyncCopyOffsetPlace sm121LowerAsyncCopyOffsetSpan offset)
1612 (sm121LowerWithField
1613 (sm121LowerWithField
1614 (sm121LowerWithField high sm121LowerAsyncCopyDescriptorEnable 2 zero)
1615 sm121LowerAsyncCopyLegacyBit 2 zero)
1616 sm121LowerAsyncCopyDescriptorBit 2 1)
1617 reads))
1618 (sm121LowerRefuse (constructor SM121LowerRefusal SM121LowerRefusedSharedOffset)))))
1619 -- a branch keeps its SM86 word until the schedule has placed
1620 -- its target (sm121LowerRelocate re-encodes the
1621 -- displacement); it is a join
1622 (branch SM121LowerRuleBranch .
1623 (let unrestricted targetMark = (sm121LowerBranchTarget low high index) in
1624 (sm121LowerSelect (family SM121LowerExpansion)
1625 (naturalIsZero targetMark)
1626 (sm121LowerRefuse (constructor SM121LowerRefusal SM121LowerRefusedBranchTarget))
1627 (sm121LowerOnly (plainWith label 1 targetMark low high reads)))))))))))))))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.