From 18158bb1449d74ae29d2560ae00f1ac2d4e32f17 Mon Sep 17 00:00:00 2001
From: Clark Coleman <clc@zephyr-software.com>
Date: Thu, 26 Nov 2020 23:42:03 -0500
Subject: [PATCH] SPARK: More FindConditionalFollowNode() improvements.
---
include/base/SMPBasicBlock.h | 2 +
include/base/SMPFunction.h | 4 +-
src/base/SMPBasicBlock.cpp | 25 ++++++
src/base/SMPFunction.cpp | 158 ++++++++++++++++++++++++++++-------
4 files changed, 159 insertions(+), 30 deletions(-)
diff --git a/include/base/SMPBasicBlock.h b/include/base/SMPBasicBlock.h
index bba1ebec..2a6cebf3 100644
--- a/include/base/SMPBasicBlock.h
+++ b/include/base/SMPBasicBlock.h
@@ -399,6 +399,8 @@ public:
bool IsBlockReachableWithoutBackEdges(const int DestBlockNum, bool &HitDeadEnd) const; // path without back edges?
std::size_t GetNumPredsMinusBackEdges(void) const; // Compute predecessor count, excluding loop-back edges. Loop ID must occur first.
+ std::size_t GetNumSuccessorsMinusBackEdges(void) const; // Compute successor count, excluding loop-back edges.
+ int GetFirstNonBackEdgeSuccNum(void) const; // Avoid back edges; get first SuccBlockNum that is not back edge.
STARS_ea_t GetUltimateOperandSource(STARS_ea_t UseAddr, const STARSOpndTypePtr &UseOp, int UseSSANum); // trace through move and Phi defs to some defining operation.
bool GetUltimateInitValue(const STARSOpndTypePtr &UseOp, STARS_ea_t InstAddr, int SSANum, bool LocalName, STARSOpndTypePtr &DefMoveOp, STARS_uval_t &InitValue);
// Trace back to const or InArg with min const value; follow Phi USEs to before-loop locations only.
diff --git a/include/base/SMPFunction.h b/include/base/SMPFunction.h
index 3b9224d3..34c38858 100644
--- a/include/base/SMPFunction.h
+++ b/include/base/SMPFunction.h
@@ -987,7 +987,7 @@ private:
bool DoesBlockExitLoop(std::size_t LoopNumber, SMPBasicBlock *LoopBlock, int &FollowBlockNum); // return true if block can exit the loop.
bool DetectMultiLevelLoopBreak(const int LoopBlockNum, const int ExitTargetBlockNum) const; // Is ExitTargetBlockNum more than 1 loop nesting level away from LoopBlockNum?
void ComputeLoopFollowNodesReachability(const std::size_t LoopNum); // populate entry in LoopExitTargetsReachabilitySets
- void MarkReachableBlocks(const int BlockNum, const int LoopNum, int LoopHeadBlockNum, STARSBitSet &ReachableSet); // Set bits of current BlockNum and its descendants in CFG that are dominated by LoopHeadBlockNum
+ void MarkReachableBlocks(const int BlockNum, const int LoopNum, const int HeadBlockNum, STARSBitSet &ReachableSet); // Set bits of current BlockNum and its descendants in CFG that are dominated by LoopHeadBlockNum
uint32_t GetReachableSourcesCount(const std::size_t BlockNum, const std::size_t LoopNum) const; // How many of the multiple exit targets from LoopNum reach BlockNum?
void DetectLoopInvariantDEFs(void); // Collect a set of loop-invariant DEFs with the inst IDs of the DEFs.
void DetectLoopInvariantDEFs2(void); // Collect a set of loop-invariant DEFs with the inst IDs of the DEFs.
@@ -1041,7 +1041,7 @@ private:
bool FindUnstructuredIfThenElse(const int HeadBlockNum, const int ThenBlockNum, const int ElseBlockNum, const int FollowBlockNum); // Do IF and ELSE branches merge before FollowBlockNum?
bool FindUnstructuredBlockList(const std::list<std::size_t> &BlockList, const int CondHeadBlockNum, const int FollowBlockNum); // Do any blocks fail to reach their FollowBlockNum?
bool FindMultiLoopContinue(const int BranchBlockNum); // Does COND_BRANCH behave as an unstructured multi-level loop continue statement?
- bool DetectConditionalReachabilityErrors(const int HeadBlockNum, const int FTBlockNum, const int NFTBlockNum, const STARSBitSet &FTBlocksSeen, const STARSBitSet &NFTBlocksSeen, const STARSBitSet &CommonBlocksSeen);
+ bool DetectConditionalReachabilityErrors(const int HeadBlockNum, const int FTBlockNum, const int NFTBlockNum, const bool FTNotDominated, const bool NFTNotDominated, const STARSBitSet &FTBlocksSeen, const STARSBitSet &NFTBlocksSeen, const STARSBitSet &CommonBlocksSeen);
bool ConditionalReachabilityLoopErrorHelper(const int CondHeadBlockNum, const int BlockNum) const; // Back door edge into loop exit targets (for multi-exit loops)?
void FindGuardedLoops(void); // Find guarded loops and fill the GuardToLoopMap and LoopToGuardMap
diff --git a/src/base/SMPBasicBlock.cpp b/src/base/SMPBasicBlock.cpp
index 52079071..7e6e8407 100644
--- a/src/base/SMPBasicBlock.cpp
+++ b/src/base/SMPBasicBlock.cpp
@@ -456,6 +456,31 @@ size_t SMPBasicBlock::GetNumPredsMinusBackEdges(void) const {
return PredCount;
} // end of SMPBasicBlock::GetNumPredsMinusBackEdges()
+// Compute successor count, excluding loop-back edges.
+std::size_t SMPBasicBlock::GetNumSuccessorsMinusBackEdges(void) const {
+ size_t SuccCount = 0;
+ for (SMPBasicBlock *SuccBlock : this->Successors) {
+ int SuccBlockNum = SuccBlock->GetNumber();
+ if (SuccBlockNum > this->GetNumber()) { // RPO numbering identifies back edges
+ ++SuccCount;
+ }
+ }
+ return SuccCount;
+} // end of SMPBasicBlock::GetNumSuccessorsMinusBackEdges()
+
+// Avoid back edges; get first SuccBlockNum that is not back edge.
+int SMPBasicBlock::GetFirstNonBackEdgeSuccNum(void) const {
+ int DownSuccBlockNum = SMP_BLOCKNUM_UNINIT;
+ for (SMPBasicBlock *SuccBlock : this->Successors) {
+ int SuccBlockNum = SuccBlock->GetNumber();
+ if (SuccBlockNum > this->GetNumber()) { // RPO numbering identifies back edges
+ DownSuccBlockNum = SuccBlockNum;
+ break;
+ }
+ }
+ return DownSuccBlockNum;
+} // end of SMPBasicBlock::GetFirstNonBackEdgeSuccNum()
+
// Are all instructions in the block no-ops?
bool SMPBasicBlock::AllNops(void) {
size_t NopCount = 0;
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index 2ed179d5..082a456d 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -7437,19 +7437,29 @@ void SMPFunction::ComputeLoopFollowNodesReachability(const std::size_t LoopNum)
return;
} // end of SMPFunction::ComputeLoopFollowNodesReachability()
-// Set bits of current BlockNum and its descendants in CFG that are dominated by LoopHeadBlockNum
-// NOTE: LoopHeadBlockNum can be any dominating block num, with LoopNum < 0 indicating we are not in a loop.
-void SMPFunction::MarkReachableBlocks(const int BlockNum, const int LoopNum, const int LoopHeadBlockNum, STARSBitSet &ReachableSet) {
+// Set bits of current BlockNum and its descendants in CFG that are dominated by HeadBlockNum
+// NOTE: HeadBlockNum can be any dominating block num, with LoopNum < 0 indicating we are not in a loop.
+void SMPFunction::MarkReachableBlocks(const int BlockNum, const int LoopNum, const int HeadBlockNum, STARSBitSet &ReachableSet) {
bool ProperDominance = true;
#if 1
- ProperDominance = this->DoesBlockDominateBlock(LoopHeadBlockNum, BlockNum);
+ ProperDominance = this->DoesBlockDominateBlock(HeadBlockNum, BlockNum);
#endif
+
+ int ContainingLoopNum = -1;
+ // If (LoopNum < 0), we are analyzing a conditional statement. But it could be contained in a loop, and we
+ // don't want to exit that containing loop.
+ if (0 > LoopNum) { // conditional statement
+ ContainingLoopNum = this->GetInnermostLoopNum(HeadBlockNum);
+ }
+ bool ConditionalInsideLoop = (0 <= ContainingLoopNum);
+
if ((!ReachableSet.GetBit((size_t)BlockNum)) && ProperDominance) { // avoid looping and duplication of work
ReachableSet.SetBit((size_t)BlockNum); // Initialize to itself being reachable
SMPBasicBlock *CurrBlock = this->GetBlockByNum((size_t)BlockNum);
assert(nullptr != CurrBlock);
for (list<SMPBasicBlock *>::const_iterator SuccIter = CurrBlock->GetFirstConstSucc(); SuccIter != CurrBlock->GetLastConstSucc(); ++SuccIter) {
- int SuccBlockNum = (*SuccIter)->GetNumber();
+ SMPBasicBlock *SuccBlock = (*SuccIter);
+ int SuccBlockNum = SuccBlock->GetNumber();
// Weed out back edges
if (!this->DoesBlockDominateBlock(SuccBlockNum, BlockNum)) {
// It is OK to exit an inner loop into multiple blocks that are part of an enclosing
@@ -7510,10 +7520,24 @@ void SMPFunction::MarkReachableBlocks(const int BlockNum, const int LoopNum, con
// our translation. Therefore we end our reachability marking when we are about to exit another
// loop level. Such a multi-level trace can be detected by the existing method that detects
// multi-level loop breaks, which are unstructured and need to be structured separately.
- bool BadLoopBreak = (0 > LoopNum) ? false : this->DetectMultiLevelLoopBreak(LoopHeadBlockNum, SuccBlockNum);
+ bool BadLoopBreak = (0 > LoopNum) ? false : this->DetectMultiLevelLoopBreak(HeadBlockNum, SuccBlockNum);
if (!BadLoopBreak) {
- if (this->DoesBlockDominateBlock(LoopHeadBlockNum, SuccBlockNum)) {
- this->MarkReachableBlocks(SuccBlockNum, LoopNum, LoopHeadBlockNum, ReachableSet);
+ bool LocalDominance = (this->DoesBlockDominateBlock(HeadBlockNum, SuccBlockNum));
+ bool SuccInsideContainingLoop = (ConditionalInsideLoop && this->IsBlockInLoop(SuccBlockNum, (size_t)ContainingLoopNum));
+ bool ConditionalExitingLoop = (SuccInsideContainingLoop && SuccBlock->IsLoopTailBlock() && (this->GetInnermostLoopNum(SuccBlockNum) == ContainingLoopNum));
+ if (ConditionalExitingLoop) {
+ // Don't go beyond the tail block. Its successors can only be loop exit targets or the loop header.
+ if (LocalDominance) {
+ ReachableSet.SetBit((size_t)SuccBlockNum); // Loop tail block is reachable, but don't recurse.
+ }
+ continue;
+ }
+ else if (ConditionalInsideLoop && (!SuccInsideContainingLoop)) {
+ // We are already outside the containing loop if the passed-in BlockNum exits the loop.
+ continue; // Don't mark a containing loop exit target as reachable
+ }
+ if (LocalDominance) {
+ this->MarkReachableBlocks(SuccBlockNum, LoopNum, HeadBlockNum, ReachableSet);
}
else {
// Terminating because we are escaping the region dominated by the loop head block.
@@ -7523,7 +7547,7 @@ void SMPFunction::MarkReachableBlocks(const int BlockNum, const int LoopNum, con
// NOTE: If the ExitTargetBlock (BlockNum) is not dominated by LoopHeadBlockNum,
// then we should not be looking at its successors in the first place.
if (0 <= LoopNum) {
- if (this->DoesBlockDominateBlock(LoopHeadBlockNum, BlockNum)) {
+ if (this->DoesBlockDominateBlock(HeadBlockNum, BlockNum)) {
this->MultiLoopExitTargetsConvergenceMap[(size_t)LoopNum].insert(SuccBlockNum);
}
}
@@ -12652,8 +12676,10 @@ int SMPFunction::FindConditionalFollowNode3(int HeadBlockNum) {
// 4C: Conditional is inside a loop, and 2 or more loop tail blocks for that loop are reachable from the
// two traces. The decompilation of the conditional will need to continue until the loop backs and loop
// boundaries are reached, so the follow block needs to be -2 (SMP_BLOCKNUM_COMMON_RETURN).
- // 5. Intersection point is not dominated by HeadBlock. Some path is entering the conditional in the
- // middle. UNSTRUCTURED.
+ // 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.
if (!ShortCircuit) {
NFTBlockNum = (*(HeadBlock->GetCondNonFallThroughSucc()))->GetNumber();
@@ -12692,7 +12718,7 @@ int SMPFunction::FindConditionalFollowNode3(int HeadBlockNum) {
bool Case0 = false;
// Find CFG problems that are obvious just from the reachability bitsets.
- if (this->DetectConditionalReachabilityErrors(HeadBlockNum, FTBlockNum, NFTBlockNum, FTBlocksSeen, NFTBlocksSeen, CommonBlocksSeen)) {
+ if (this->DetectConditionalReachabilityErrors(HeadBlockNum, FTBlockNum, NFTBlockNum, FTNotDominated, NFTNotDominated, FTBlocksSeen, NFTBlocksSeen, CommonBlocksSeen)) {
return FollowBlockNum; // error; still set to SMP_BLOCKNUM_UNINIT
}
@@ -12725,7 +12751,7 @@ int SMPFunction::FindConditionalFollowNode3(int HeadBlockNum) {
IfThenElseCase = false;
}
- bool NotLoopBack = (NextFTBlockNum > HeadBlockNum);
+ bool NotLoopBack = ((NextFTBlockNum > HeadBlockNum) || (SMP_BLOCKNUM_COMMON_RETURN == NextFTBlockNum));
if ((NextFTBlockNum == NextNFTBlockNum) && NotLoopBack) { // Exception to Case 1
FollowBlockNum = NextFTBlockNum;
}
@@ -12757,26 +12783,26 @@ int SMPFunction::FindConditionalFollowNode3(int HeadBlockNum) {
}
else { // if-then-else with at least one intersection point
if (this->DoesBlockDominateBlock(HeadBlockNum, FirstCommonBlockNum)) { // Case 4
- uint32_t TailBlocksSeen = 0;
+ set<int> TailBlocksSeen;
if (HeadBlockIsInALoop) {
int FirstFTReachableBlockNum = FTBlocksSeen.FindLowestBitSet();
int FirstNFTReachableBlockNum = NFTBlocksSeen.FindLowestBitSet();
for (int BlockIndex = FirstFTReachableBlockNum; BlockIndex <= LastFTReachableBlockNum; ++BlockIndex) {
if (FTBlocksSeen.GetBit((size_t)BlockIndex)) {
if (this->GetBlockByNum((size_t)BlockIndex)->IsLoopTailBlock()) {
- ++TailBlocksSeen;
+ TailBlocksSeen.insert(BlockIndex);
}
}
}
for (int BlockIndex = FirstNFTReachableBlockNum; BlockIndex <= LastNFTReachableBlockNum; ++BlockIndex) {
if (NFTBlocksSeen.GetBit((size_t)BlockIndex)) {
if (this->GetBlockByNum((size_t)BlockIndex)->IsLoopTailBlock()) {
- ++TailBlocksSeen;
+ TailBlocksSeen.insert(BlockIndex);
}
}
}
}
- if (2 <= TailBlocksSeen) { // Case 4C
+ if (2 <= TailBlocksSeen.size()) { // Case 4C
FollowBlockNum = SMP_BLOCKNUM_COMMON_RETURN;
}
else if (LastFTReachableBlockNum != LastNFTReachableBlockNum) { // Case 4B
@@ -12799,7 +12825,10 @@ int SMPFunction::FindConditionalFollowNode3(int HeadBlockNum) {
}
}
else { // Case 5
- FollowBlockNum = SMP_BLOCKNUM_UNINIT;
+ // !!!!****!!!! Should we demand that all other predecessors of FirstCommonBlockNum
+ // dominate HeadBlockNum, proving that we truly have containing structures that prevented
+ // HeadBlockNum from dominating FirstCommonBlockNum?
+ FollowBlockNum = FirstCommonBlockNum;
}
}
// Detect unstructured entry points.
@@ -12841,16 +12870,18 @@ bool SMPFunction::FindNextBlockAfterReachableBlocks(const int ContainingLoopNum,
// look at the exit targets. All exit targets must be in the BlocksSeen trace. If
// the LoopFollowNode is also in the trace, continue with it and skip over the blocks
// within the loop. If not, then the LoopFollowNode is the NextBlockNum we are searching for.
+ NextBlockNum = SMP_BLOCKNUM_UNINIT;
int LowestBlockNum = BlocksSeen.FindLowestBitSet();
int HighestBlockNum = BlocksSeen.FindHighestBitSet();
int HighestNonLoopBlockNum = 0;
bool ErrorSeen = (0 > LowestBlockNum);
int BlockNum = LowestBlockNum;
bool UsedLoopFollowBlock = false;
+ bool ContainingLoopIsMultiExitTargetLoop = (ContainingLoopNum < 0) ? false : this->DoesLoopHaveMultipleExitTargets((size_t)ContainingLoopNum);
while (BlockNum <= HighestBlockNum) {
size_t BlockIndex = (size_t)BlockNum;
- int InnermostLoopNum = this->GetInnermostLoopNum(BlockNum);
if (BlocksSeen.GetBit(BlockIndex)) {
+ int InnermostLoopNum = this->GetInnermostLoopNum(BlockNum);
SMPBasicBlock *CurrBlock = this->GetBlockByNum(BlockIndex);
if (InnermostLoopNum != ContainingLoopNum) { // Entered into loop within conditional statement
if (CurrBlock->IsLoopHeaderBlock()) { // jump to follow block
@@ -12870,8 +12901,17 @@ bool SMPFunction::FindNextBlockAfterReachableBlocks(const int ContainingLoopNum,
// Loop is in current conditional branch, but its follow block is not. If the
// code is structured, it will be the case that the loop follow block is also
// the follow block for the containing conditional statement, and the SPARK Ada
- // decompilation will have "end loop;" falling directly into "end if;".
- NextBlockNum = LoopFollowBlockNum;
+ // decompilation will have "end loop;" falling directly into "end if;". The exception
+ // is the MultiExitTargetLoop inner loop case, when there is also a containing loop
+ // where the conditional needs to get a follow node of -2 to make translation stop at
+ // every path that hits a containing loop boundary, in case the follow node is shared among
+ // more than two structures.
+ if (MultiExitTargetLoop && (ContainingLoopNum >= 0)) {
+ NextBlockNum = SMP_BLOCKNUM_COMMON_RETURN;
+ }
+ else {
+ NextBlockNum = LoopFollowBlockNum;
+ }
UsedLoopFollowBlock = true;
break;
}
@@ -12892,14 +12932,22 @@ bool SMPFunction::FindNextBlockAfterReachableBlocks(const int ContainingLoopNum,
if (!ErrorSeen) {
if (!UsedLoopFollowBlock) {
- // Still need convergence point.
- SMPBasicBlock *LastBlock = this->GetBlockByNum((size_t)HighestNonLoopBlockNum);
- assert(nullptr != LastBlock);
- if (1 == LastBlock->GetNumSuccessors()) {
- NextBlockNum = (*(LastBlock->GetFirstConstSucc()))->GetNumber();
- ErrorSeen = (0 > NextBlockNum);
+ if (ContainingLoopIsMultiExitTargetLoop && (SMP_BLOCKNUM_UNINIT == NextBlockNum)) {
+ NextBlockNum = SMP_BLOCKNUM_COMMON_RETURN; // Conditional translation must stop at loop boundary.
+ }
+ else {
+ // Still need convergence point.
+ SMPBasicBlock *LastBlock = this->GetBlockByNum((size_t)HighestNonLoopBlockNum);
+ assert(nullptr != LastBlock);
+ if (1 == LastBlock->GetNumSuccessorsMinusBackEdges()) {
+ NextBlockNum = LastBlock->GetFirstNonBackEdgeSuccNum();
+ }
+ else {
+ NextBlockNum = HighestNonLoopBlockNum;
+ }
}
}
+ ErrorSeen = (SMP_BLOCKNUM_UNINIT == NextBlockNum);
}
return ErrorSeen;
@@ -13245,8 +13293,9 @@ bool SMPFunction::FindMultiLoopContinue(const int BranchBlockNum) {
} // end of SMPFunction::FindMultiLoopContinue()
// Detect conditional statement structuring errors that are obvious just from the reachability bitsets.
-bool SMPFunction::DetectConditionalReachabilityErrors(const int HeadBlockNum, const int FTBlockNum, const int NFTBlockNum, const STARSBitSet &FTBlocksSeen, const STARSBitSet &NFTBlocksSeen, const STARSBitSet &CommonBlocksSeen) {
+bool SMPFunction::DetectConditionalReachabilityErrors(const int HeadBlockNum, const int FTBlockNum, const int NFTBlockNum, const bool FTNotDominated, const bool NFTNotDominated, const STARSBitSet &FTBlocksSeen, const STARSBitSet &NFTBlocksSeen, const STARSBitSet &CommonBlocksSeen) {
bool Unstructured = false;
+ bool IfThenElseCaseDom = (!(FTNotDominated || NFTNotDominated));
// All blocks reachable by either FTBlock or NFTBlock should either precede the intersection point or
// should be in CommonBlocksSeen (i.e. RPO block number greater than intersection point RPO number
@@ -13259,6 +13308,7 @@ bool SMPFunction::DetectConditionalReachabilityErrors(const int HeadBlockNum, co
bool OddIfThenCase = (IntersectionBlockNum == FTBlockNum);
bool IfThenElseCase = (!(IfThenCase || OddIfThenCase));
if (IfThenElseCase) {
+ assert(IfThenElseCaseDom);
for (size_t BlockNum = (size_t)(IntersectionBlockNum + 1); BlockNum < this->GetNumBlocks(); ++BlockNum) {
if (FTBlocksSeen.GetBit(BlockNum)) {
bool success = NFTBlocksSeen.GetBit(BlockNum);
@@ -13309,6 +13359,58 @@ bool SMPFunction::DetectConditionalReachabilityErrors(const int HeadBlockNum, co
}
} // end if we have loops
+ // 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)
+ // 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
+ // CFG unstructured.
+ if (!IfThenElseCaseDom && (!Unstructured)) {
+ bool OddIfThenCase = FTNotDominated; // FTBlock is FollowNode
+ int LowestBlockNum = OddIfThenCase ? NFTBlockNum : FTBlockNum;
+ int HighestBlockNum = OddIfThenCase ? FTBlockNum : NFTBlockNum;
+ list<int> WorkList;
+ WorkList.push_front(LowestBlockNum);
+ STARSBitSet WorkListBlocksSeen;
+ WorkListBlocksSeen.AllocateBits(this->GetNumBlocks());
+ while (!WorkList.empty()) {
+ int BlockNum = WorkList.front();
+ WorkList.pop_front();
+ size_t BlockIndex = (size_t)BlockNum;
+ if (WorkListBlocksSeen.GetBit(BlockIndex)) { // already processed (we see join points more than once)
+ continue;
+ }
+ else {
+ WorkListBlocksSeen.SetBit(BlockIndex);
+ }
+ bool BlockReached = OddIfThenCase ? NFTBlocksSeen.GetBit(BlockIndex) : FTBlocksSeen.GetBit(BlockIndex);
+ if (BlockReached) {
+ SMPBasicBlock *CurrBlock = this->GetBlockByNum(BlockIndex);
+ // Add non-back-edge successors to the WorkList, limited by HighestBlockNum.
+ for (list<SMPBasicBlock *>::const_iterator SuccIter = CurrBlock->GetFirstConstSucc();
+ SuccIter != CurrBlock->GetLastConstSucc();
+ ++SuccIter) {
+ int SuccBlockNum = (*SuccIter)->GetNumber();
+ // Only successors between the current block and the follow node go onto the work list.
+ if ((SuccBlockNum > BlockNum) && (SuccBlockNum < HighestBlockNum)) {
+ WorkList.push_back(SuccBlockNum);
+ }
+ } // end for all successor blocks
+ }
+ else {
+ Unstructured = true;
+ if (!this->PrintedSPARKUnstructuredMsg) {
+ SMP_msg("ERROR: SPARK: Unstructured due to then-branch block %d not dominated and reached from head block %d ",
+ BlockNum, HeadBlockNum);
+ this->DumpFuncNameAndAddr();
+ this->PrintedSPARKUnstructuredMsg = true;
+ }
+ break; // break out of while loop
+ }
+ } // end while WorkList is not empty
+ }
+
return Unstructured;
} // end of SMPFunction::DetectConditionalReachabilityErrors()
--
GitLab