diff --git a/include/base/SMPFunction.h b/include/base/SMPFunction.h
index 34c3885898b2a1cd822827c1cfc2a0716dbb4cf9..27c25848bda31ebf279eb5bea2cc72115fddb6f9 100644
--- a/include/base/SMPFunction.h
+++ b/include/base/SMPFunction.h
@@ -1033,9 +1033,9 @@ private:
void CoalesceShadowBlocks(int LeftBlockNum, int RightBlockNum, bool NegateLeft, SMPoperator TopOper, int NewFTNum, int NewNFTNum); // Make LeftExpr be LeftExpr TopOper RightExpr
bool AnalyzeCompoundConditionalStatements(void); // Analyze if-statements with short-circuit operators
bool AnalyzeConditionalStatements(void); // Analyze if-then-elses starting at COND_BRANCH at end of all blocks; return false if not well-structured
- int FindConditionalFollowNode(int HeadBlockNum); // Find candidate block # for if-else follow node for HeadBlockNum; return -1 otherwise
+ int FindConditionalFollowNode(const int HeadBlockNum, bool &IfThenCase, bool &OddIfThenCase, bool &IfThenElseCase); // Find candidate block # for if-else follow node for HeadBlockNum; return -1 otherwise
int FindConditionalFollowNode2(int HeadBlockNum); // Find candidate block # for if-else follow node for HeadBlockNum; return -1 otherwise
- int FindConditionalFollowNode3(int HeadBlockNum); // Find candidate block # for if-else follow node for HeadBlockNum; return -1 otherwise
+ int FindConditionalFollowNode3(const int HeadBlockNum, bool &IfThenCase, bool &OddIfThenCase, bool &IfThenElseCase); // Find candidate block # for if-else follow node for HeadBlockNum; return -1 otherwise
bool FindNextBlockAfterReachableBlocks(const int ContainingLoopNum, const STARSBitSet &BlocksSeen, int &NextBlockNum); // Get unique successor to BlocksSeen; return false if unable to do so.
int TrackConditionalBranchTerminus(int BranchHeadBlockNum, int CurrBlockNum, STARSBitSet &BlocksSeen, int &BlockAlreadySeenCounter); // Track CurrBlockNum until we reach block that BranchHeadBlockNum doesn't dominate, or dead end. Return block num, possibly SMP_BLOCKNUM_COMMON_RETURN.
bool FindUnstructuredIfThenElse(const int HeadBlockNum, const int ThenBlockNum, const int ElseBlockNum, const int FollowBlockNum); // Do IF and ELSE branches merge before FollowBlockNum?
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index 082a456dc835319f21bb31d5a4106b296ecfc88b..f6fb4e528ccc65beadf7ee9680b27d57724e8f37 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -11765,7 +11765,10 @@ bool SMPFunction::AnalyzeCompoundConditionalStatements(void) {
STARS_ea_t LastAddr = OrigBlock->GetLastAddr();
ControlFlowType LastCFType = this->GetControlFlowType(LastAddr);
if (!IsLoopExitFlow(LastCFType)) { // not SHORT_CIRCUIT_LOOP_EXIT or SHORT_CIRCUIT_INVERTED_LOOP_EXIT
- int FollowBlockNum = this->FindConditionalFollowNode((int) BlockIndex);
+ bool BitsetIfThenCase = false;
+ bool BitsetOddIfThenCase = false;
+ bool BitsetIfThenElseCase = false;
+ int FollowBlockNum = this->FindConditionalFollowNode((int)BlockIndex, BitsetIfThenCase, BitsetOddIfThenCase, BitsetIfThenElseCase);
if (SMP_BLOCKNUM_UNINIT == FollowBlockNum) {
if (!this->PrintedSPARKUnstructuredMsg) {
SMP_msg("ERROR: SPARK: Unstructured due to: Cannot find follow block for SHORT_CIRCUIT_BRANCH in block %zu ", BlockIndex);
@@ -11787,6 +11790,12 @@ bool SMPFunction::AnalyzeCompoundConditionalStatements(void) {
bool IfThenCase = false;
if ((NFTBlockNum == FollowBlockNum) || (FTBlockNum == FollowBlockNum)) {
IfThenCase = true;
+ if (!(BitsetIfThenCase || BitsetOddIfThenCase)) {
+ SMP_msg("INFO: SPARK: BitsetIfThenCase %d IfThenCase %d BitsetOddIfThenCase %d SHORT_CIRCUIT HeadBlock %zu ",
+ BitsetIfThenCase, IfThenCase, BitsetOddIfThenCase, BlockIndex);
+ this->DumpFuncNameAndAddr();
+ this->DumpDotCFG();
+ }
// Ensure that we arrange it so that it translates directly to:
// if (compound condition) then
// do_something;
@@ -11844,6 +11853,13 @@ bool SMPFunction::AnalyzeCompoundConditionalStatements(void) {
// So, we want whichever block falls through to the FollowBlock to be either the NFTBlock
// or to be dominated by the NFTBlock (NFTBlock could start a loop or any other structure
// besides a simple basic block).
+ if (!BitsetIfThenElseCase) {
+ SMP_msg("INFO: SPARK: BitsetIfThenElseCase %d BitsetIfThenCase %d BitsetOddIfThenCase %d SHORT_CIRCUIT HeadBlock %zu ",
+ BitsetIfThenElseCase, BitsetIfThenCase, BitsetOddIfThenCase, BlockIndex);
+ this->DumpFuncNameAndAddr();
+ this->DumpDotCFG();
+ }
+
int FTPredBlockNum = this->GetFallThroughPredBlockNum(FollowBlockNum);
if (SMP_BLOCKNUM_UNINIT != FTPredBlockNum) {
// Is FTPredBlockNum equal to FTBlock, or dominated by FTBlock?
@@ -11950,7 +11966,10 @@ bool SMPFunction::AnalyzeConditionalStatements(void) {
continue;
}
int HeadBlockNum = CurrBlock->GetNumber();
- int FollowNodeNum = this->FindConditionalFollowNode(HeadBlockNum);
+ bool BitsetIfThenCase = false;
+ bool BitsetOddIfThenCase = false;
+ bool BitsetIfThenElseCase = false;
+ int FollowNodeNum = this->FindConditionalFollowNode(HeadBlockNum, BitsetIfThenCase, BitsetOddIfThenCase, BitsetIfThenElseCase);
if (FollowNodeNum == SMP_BLOCKNUM_UNINIT) {
UnresolvedBranchBlocks.push_back(HeadBlockNum);
#if 1
@@ -12024,6 +12043,12 @@ bool SMPFunction::AnalyzeConditionalStatements(void) {
SMPBasicBlock *FollowBlock = this->GetBlockByNum((size_t) FollowNodeNum);
assert(nullptr != FollowBlock);
bool IfThenCase = FollowBlock->IsBlockPred(HeadBlockNum);
+ if (IfThenCase != (BitsetIfThenCase || BitsetOddIfThenCase)) {
+ SMP_msg("INFO: SPARK: BitsetIfThenCase %d IfThenCase %d BitsetOddIfThenCase %d HeadBlock %d ",
+ BitsetIfThenCase, IfThenCase, BitsetOddIfThenCase, CurrBlock->GetNumber());
+ this->DumpFuncNameAndAddr();
+ this->DumpDotCFG();
+ }
if (IfThenCase) {
this->SetControlFlowType(LastAddr, BRANCH_IF_THEN);
if (!UnresolvedBranchBlocks.empty()) { // error; cannot have elsif branches for IfThenCase
@@ -12042,6 +12067,12 @@ bool SMPFunction::AnalyzeConditionalStatements(void) {
// follow block and branch to the then-block.
int DistantBlockNum = (*(CurrBlock->GetCondNonFallThroughSucc()))->GetNumber();
bool OddIfThenCase = LastInst->IsOddIfThenCase();
+ if (OddIfThenCase != BitsetOddIfThenCase) {
+ SMP_msg("INFO: SPARK: BitsetIfThenCase %d OddIfThenCase %d BitsetOddIfThenCase %d HeadBlock %d ",
+ BitsetIfThenCase, OddIfThenCase, BitsetOddIfThenCase, CurrBlock->GetNumber());
+ this->DumpFuncNameAndAddr();
+ this->DumpDotCFG();
+ }
if (!OddIfThenCase) {
if (DistantBlockNum != FollowNodeNum) {
if (!this->PrintedSPARKUnstructuredMsg) {
@@ -12147,13 +12178,16 @@ bool SMPFunction::AnalyzeConditionalStatements(void) {
return StructuredConditional;
} // end of SMPFunction::AnalyzeConditionalStatements()
-int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
+int SMPFunction::FindConditionalFollowNode(const int HeadBlockNum, bool &IfThenCase, bool &OddIfThenCase, bool &IfThenElseCase) {
+ IfThenCase = false;
+ OddIfThenCase = false;
+ IfThenElseCase = false;
int ReturnFollowBlockNum = SMP_BLOCKNUM_UNINIT;
int OldAlgorithmFollowNode = this->FindConditionalFollowNode2(HeadBlockNum);
#if 0
ReturnFollowBlockNum = OldAlgorithmFollowNode;
#else
- int NewAlgorithmFollowNode = this->FindConditionalFollowNode3(HeadBlockNum);
+ int NewAlgorithmFollowNode = this->FindConditionalFollowNode3(HeadBlockNum, IfThenCase, OddIfThenCase, IfThenElseCase);
bool BadOld = (OldAlgorithmFollowNode == SMP_BLOCKNUM_UNINIT);
bool BadNew = (NewAlgorithmFollowNode == SMP_BLOCKNUM_UNINIT);
if (BadOld) {
@@ -12600,7 +12634,7 @@ int SMPFunction::FindConditionalFollowNode2(int HeadBlockNum) {
} // end of SMPFunction::FindConditionalFollowNode2()
// Find candidate block # for if-else follow node for HeadBlockNum; return -1 otherwise
-int SMPFunction::FindConditionalFollowNode3(int HeadBlockNum) {
+int SMPFunction::FindConditionalFollowNode3(const int HeadBlockNum, bool &IfThenCase, bool &OddIfThenCase, bool &IfThenElseCase) {
int FollowBlockNum = SMP_BLOCKNUM_UNINIT;
int NFTBlockNum = SMP_BLOCKNUM_UNINIT;
int FTBlockNum = SMP_BLOCKNUM_UNINIT;
@@ -12643,14 +12677,52 @@ int SMPFunction::FindConditionalFollowNode3(int HeadBlockNum) {
assert(2 == HeadBlock->GetNumSuccessors());
+ // In the discussion below, FTBlockNum and NFTBlockNum are the Fall-Through and Non-Fall-Through successor
+ // RPO (Reverse Post-Order) block numbers of the COND_BRANCH block.
// The simple new algorithm depends entirely on the reachable blocks from each of the
- // two successors of the COND_BRANCH. Without following back edges, and staying within
+ // two successors of the COND_BRANCH (FTBlockNum and NFTBlockNum). Without following back edges, and staying within
// the region dominated by HeadBlockNum, we mark reachable blocks in bitsets for each
// of the two COND_BRANCH successor blocks. Then we have the following cases:
// 0. If one of the COND_BRANCH successor blocks dominates HeadBlock, we have a back edge that
// cannot be followed, so we cannot have an intersection of traces from the COND_BRANCH successor
// blocks. So, set the code for structured lack of intersection (SMP_BLOCKNUM_COMMON_RETURN) as
// the follow block.
+ // 1: Smaller RPO-numbered block out of FTBlockNum and NFTBlockNum reaches the other: The larger RPO
+ // number is the FollowBlockNum. If FTBlockNum is smaller, this is the normal IfThenCase. If NFTBlockNum
+ // is smaller, this is the OddIfThenCase. If the larger RPO block can reach the smaller RPO block, we
+ // would have a catastrophic failure of RPO numbering (assert and abort; should never happen).
+ // 2. If not case 1, we have the IfThenElseCase.
+ // 2A. If the reachability bitsets intersect, then the lowest RPO block # in the intersection is
+ // the FollowBlockNum.
+ // 2B. If the reachability bitsets do not intersect, we have SMP_BLOCKNUM_COMMON_RETURN (i.e. -2)
+ // as the FollowBlockNum.
+ // EXCEPTION: Intersection point was about to happen, but it is just out of the region dominated
+ // by HeadBlockNum, e.g. conditional join point is also a loop follow block for an enclosing loop or
+ // is a join point for an enclosing conditional. This can be detected by seeing if the end of each
+ // of the two traces has only one successor, and the successor is the same for each trace.
+ //
+ // NOTE: One consequence of the above classification is that source code that might look like an IfThenCase
+ // will be classified as an IfThenElseCase as in the following example:
+ //
+ // if (cond1) then
+ // [code here]
+ // return;
+ // end if;
+ // [continuation code here; might go for eons until end of function]
+ //
+ // Our SPARK Ada translation of this sequence, due to the return statement making the "end if;" point not
+ // reachable from the top of the THEN-clause, will be:
+ //
+ // if (cond1) then
+ // [code here]
+ // return;
+ // else
+ // [continuation code here; might go for eons until end of function]
+ // end if;
+ //
+ // This is a perfectly valid translation of the source code and its resulting assembly language code.
+
+ // Old cases before redesign:
// 1. No intersection of the two bitsets. FollowBlockNum is -2 (SMP_BLOCKNUM_COMMON_RETURN)
// indicating the lack of intersection, with each trace ending in a block with no successors
// (e.g. return instructions or calls to non-returning functions or halt instructions or LOOP_BACKs).
@@ -12679,7 +12751,8 @@ int SMPFunction::FindConditionalFollowNode3(int HeadBlockNum) {
// 5. Intersection point is not dominated by HeadBlock. Some path is joining the conditional at the
// intersection point. The intersection point is part of some other structure, such as a containing
// loop or containing conditional that shares the intersection point as a common follow node. In any case,
- // the intersection point must be the follow node for the current conditional.
+ // the intersection point must be the follow node for the current conditional. NOTE: Isn't this the EXCEPTION
+ // to Case 2 discussed above? How could it be hit down here?
if (!ShortCircuit) {
NFTBlockNum = (*(HeadBlock->GetCondNonFallThroughSucc()))->GetNumber();
@@ -12714,7 +12787,13 @@ int SMPFunction::FindConditionalFollowNode3(int HeadBlockNum) {
int LastFTReachableBlockNum = FTBlocksSeen.FindHighestBitSet();
int LastNFTReachableBlockNum = NFTBlocksSeen.FindHighestBitSet();
int LastBlockNumReached = (LastFTReachableBlockNum >= LastNFTReachableBlockNum) ? LastFTReachableBlockNum : LastNFTReachableBlockNum;
+#if 0
bool IfThenElseCase = true;
+#else
+ IfThenCase = (FirstCommonBlockNum == NFTBlockNum);
+ OddIfThenCase = (FirstCommonBlockNum == FTBlockNum);
+ IfThenElseCase = (!(IfThenCase || OddIfThenCase));
+#endif
bool Case0 = false;
// Find CFG problems that are obvious just from the reachability bitsets.
@@ -12731,6 +12810,7 @@ int SMPFunction::FindConditionalFollowNode3(int HeadBlockNum) {
int NextFTBlockNum = SMP_BLOCKNUM_UNINIT;
int NextNFTBlockNum = SMP_BLOCKNUM_UNINIT;
if (0 <= LastFTReachableBlockNum) { // FTBlock was dominated by HeadBlock
+ assert(!FTNotDominated);
bool ErrorSeen = this->FindNextBlockAfterReachableBlocks(InnerMostLoopNum, FTBlocksSeen, NextFTBlockNum);
if (ErrorSeen) {
FollowBlockNum = SMP_BLOCKNUM_UNINIT;
@@ -12741,6 +12821,7 @@ int SMPFunction::FindConditionalFollowNode3(int HeadBlockNum) {
IfThenElseCase = false;
}
if (0 <= LastNFTReachableBlockNum) { // NFTBlock was dominated by HeadBlock
+ assert(!NFTNotDominated);
bool ErrorSeen = this->FindNextBlockAfterReachableBlocks(InnerMostLoopNum, NFTBlocksSeen, NextNFTBlockNum);
if (ErrorSeen) {
FollowBlockNum = SMP_BLOCKNUM_UNINIT;
@@ -12754,6 +12835,15 @@ int SMPFunction::FindConditionalFollowNode3(int HeadBlockNum) {
bool NotLoopBack = ((NextFTBlockNum > HeadBlockNum) || (SMP_BLOCKNUM_COMMON_RETURN == NextFTBlockNum));
if ((NextFTBlockNum == NextNFTBlockNum) && NotLoopBack) { // Exception to Case 1
FollowBlockNum = NextFTBlockNum;
+ if (NFTNotDominated) {
+ IfThenCase = true;
+ }
+ else if (FTNotDominated) {
+ OddIfThenCase = true;
+ }
+ else {
+ IfThenElseCase = true;
+ }
}
if (FollowBlockNum == SMP_BLOCKNUM_COMMON_RETURN) { // Not the exception to Case 1; search for Case 0.
@@ -12773,15 +12863,22 @@ int SMPFunction::FindConditionalFollowNode3(int HeadBlockNum) {
}
}
}
- else if (FirstCommonBlockNum == NFTBlockNum) { // Case 2
+ else if (FirstCommonBlockNum == NFTBlockNum) { // Case 2; IfThenCase
FollowBlockNum = FirstCommonBlockNum;
+ IfThenCase = true;
+ OddIfThenCase = false;
IfThenElseCase = false;
}
else if (FirstCommonBlockNum == FTBlockNum) { // Case 3; OddIfThenCase
FollowBlockNum = FirstCommonBlockNum;
+ IfThenCase = false;
+ OddIfThenCase = true;
IfThenElseCase = false;
}
else { // if-then-else with at least one intersection point
+ IfThenCase = false;
+ OddIfThenCase = false;
+ IfThenElseCase = true;
if (this->DoesBlockDominateBlock(HeadBlockNum, FirstCommonBlockNum)) { // Case 4
set<int> TailBlocksSeen;
if (HeadBlockIsInALoop) {
@@ -13322,7 +13419,7 @@ bool SMPFunction::DetectConditionalReachabilityErrors(const int HeadBlockNum, co
}
if (0 < this->GetNumLoops()) {
if (!Unstructured) {
- // Ensure that any loop contained inside the then or else clauses has its exit target
+ // Ensure that any loop contained inside the FT clause has its exit target
// blocks dominated by the loop head block; a "back door" into a loop exit target block
// that does not come from the loop must be restructured.
int LowestBlockSeen = FTBlocksSeen.FindLowestBitSet();
@@ -13340,7 +13437,7 @@ bool SMPFunction::DetectConditionalReachabilityErrors(const int HeadBlockNum, co
}
}
if (!Unstructured) {
- // Ensure that any loop contained inside the then or else clauses has its exit target
+ // Ensure that any loop contained inside the NFT clause has its exit target
// blocks dominated by the loop head block; a "back door" into a loop exit target block
// that does not come from the loop must be restructured.
int LowestBlockSeen = NFTBlocksSeen.FindLowestBitSet();
@@ -13361,7 +13458,7 @@ bool SMPFunction::DetectConditionalReachabilityErrors(const int HeadBlockNum, co
// In the If-Then case, the smaller RPO block # out of FTBlockNum and NFTBlockNum begins the THEN branch,
// and the larger RPO block # must be the FollowBlockNum. Every block on the path beginning at the THEN
- // branch beginning and concluding with a dead end block or the FollowBlock (whichever is encountered first)
+ // branch and concluding with a dead end block or the FollowBlock (whichever is encountered first)
// should be present in the corresponding reachable bitset. If any block is not present in that bitset, it is
// because that block is not dominated by the HeadBlockNum, which caused MarkReachableBlocks to terminate its
// trace. That means that the THEN branch is being entered from outside the if-then statement, making the
@@ -24418,7 +24515,7 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
SMPInstr *LastInst = (*(HeaderBlock->GetRevInstBegin()));
STARS_ea_t LastAddr = LastInst->GetAddr();
- // We want to avoid exiting a loop, which can happen when the FollowBlockNum is -1
+ // We want to avoid exiting a loop, which can happen when the FollowBlockNum is -1 or -2
// so that we don't have a definite termination point.
bool UnknownFollowBlock = (0 > FollowBlockNum);
bool InsideLoop = this->IsSPARKLoopInTranslationStack();