From be633edff0b652a892265bb72f6a863c516937da Mon Sep 17 00:00:00 2001
From: Clark Coleman <clc@zephyr-software.com>
Date: Tue, 29 Sep 2020 21:27:39 -0400
Subject: [PATCH] SPARK: Find unstructured if-then-else statements.

---
 include/base/SMPFunction.h |   3 +-
 src/base/SMPFunction.cpp   | 196 ++++++++++++++++++++++++++++++-------
 src/base/SMPInstr.cpp      |   9 +-
 3 files changed, 168 insertions(+), 40 deletions(-)

diff --git a/include/base/SMPFunction.h b/include/base/SMPFunction.h
index 8d32f259..ddac9a6b 100644
--- a/include/base/SMPFunction.h
+++ b/include/base/SMPFunction.h
@@ -549,7 +549,7 @@ public:
 
 	// Printing methods
 	void Dump(void); // debug dump
-	void DumpDotCFG(void); // Dump CFG representation for processing by "dot" program.
+	void DumpDotCFG(void) const; // Dump CFG representation for processing by "dot" program.
 
 	// Analysis methods
 	void ResetProcessedBlocks(void); // Set Processed flag to false in all blocks
@@ -1016,6 +1016,7 @@ private:
 	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 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 FollowBlockNum) const; // Do IF and ELSE branches merge before FollowBlockNum?
 	void FindGuardedLoops(void); // Find guarded loops and fill the GuardToLoopMap and LoopToGuardMap
 
 	bool IsSPARKLoopInTranslationStack(void) const; // Are we already translating a SPARK_LOOP when we encounter another loop?
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index c48443e5..a2982101 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -764,7 +764,8 @@ bool SMPFunction::ComputeInOutRegs(bool InheritPass, bool &WritesMem, bool &Call
 											if (0 == MemWriteByteWidth) {
 												SMP_msg("ERROR: expr Inherited byte width of 0 from CalleeFunc %s ; expr dump follows.\n",
 													CalleeFunc->GetFuncName());
-												LowerExpr->Dump(0);
+												if (VerboseOutput)
+													LowerExpr->Dump(0);
 												MemWriteByteWidth = global_STARS_program->GetSTARS_ISA_Bytewidth(); // default
 											}
 
@@ -7208,12 +7209,12 @@ SMPFunction::ClassifyLoop(size_t LoopNumber, int HeaderExitFollowNum, int TailEx
 	this->DetectLoopFollowBlock(LoopNumber);
 	if (HeaderBlockExitsLoop && HeadBlock->HasIndirectJump()) {
 		this->HasStructuredCFG = false;
-		SMP_msg("ERROR: SPARK: Indirect jump head loop exit at %llx for loop %d in %s\n",
+		SMP_msg("ERROR: SPARK: Unstructured due to indirect jump head loop exit at %llx for loop %d in %s\n",
 			(uint64_t)CurrBlock->GetLastAddr(), LoopNumber, this->GetFuncName());
 	}
 	else if (TailBlockExitsLoop && CurrBlock->HasIndirectJump()) {
 		this->HasStructuredCFG = false;
-		SMP_msg("ERROR: SPARK: Indirect jump tail loop exit at %llx for loop %d in %s\n",
+		SMP_msg("ERROR: SPARK: Unstructured due to indirect jump tail loop exit at %llx for loop %d in %s\n",
 			(uint64_t)CurrBlock->GetLastAddr(), LoopNumber, this->GetFuncName());
 	}
 
@@ -7223,7 +7224,7 @@ SMPFunction::ClassifyLoop(size_t LoopNumber, int HeaderExitFollowNum, int TailEx
 			this->LoopTypesByLoopNum[LoopNumber] = STARS_BOTTOM_TESTING_LOOP;
 			if (TailExitFollowNum != HeaderExitFollowNum) {
 				this->HasGoodLoopFollowBlocks = false; // inconsistent follow nodes, e.g. multi-level loop exit
-				SMP_msg("ERROR: SPARK: Conflicting head and tail loop follow block nums for loop %d : %d and %d in %s\n",
+				SMP_msg("ERROR: SPARK: Unstructured due to conflicting head and tail loop follow block nums for loop %d : %d and %d in %s\n",
 					LoopNumber, HeaderExitFollowNum, TailExitFollowNum, this->GetFuncName());
 			}
 		}
@@ -11500,13 +11501,13 @@ bool SMPFunction::AnalyzeCompoundConditionalStatements(void) {
 							map<STARS_ea_t, int>::iterator ExistingValueIter = InsertResult.first;
 							int OldFollowBlockNum = ExistingValueIter->second;
 							if (OldFollowBlockNum != FollowBlockNum) {
-								SMP_msg("ERROR: SPARK CFG JumpFollowNodesMap conflict at %llx Old: %d New:%d\n", 
+								SMP_msg("ERROR: SPARK: Unstructured due to short-circuit CFG JumpFollowNodesMap conflict at %llx Old: %d New:%d\n", 
 									(uint64_t) LastAddr, OldFollowBlockNum, FollowBlockNum);
 								Structured = false;
 								break;
 							}
 							else {
-								SMP_msg("INFO: SPARK CFG JumpFollowNodesMap redundant update at %llx\n", (uint64_t) LastAddr);
+								SMP_msg("INFO: SPARK: short-circuit CFG JumpFollowNodesMap redundant update at %llx\n", (uint64_t) LastAddr);
 							}
 						}
 					}
@@ -11522,13 +11523,13 @@ bool SMPFunction::AnalyzeCompoundConditionalStatements(void) {
 						map<STARS_ea_t, int>::iterator ExistingValueIter = InsertResult.first;
 						int OldFollowBlockNum = ExistingValueIter->second;
 						if (OldFollowBlockNum != FollowBlockNum) {
-							SMP_msg("ERROR: SPARK CFG JumpFollowNodesMap conflict at %llx Old: %d New:%d\n",
+							SMP_msg("ERROR: SPARK: Unstructured due to short-circuit CFG JumpFollowNodesMap conflict at %llx Old: %d New:%d\n",
 								(uint64_t)LastAddr, OldFollowBlockNum, FollowBlockNum);
 							Structured = false;
 							break;
 						}
 						else {
-							SMP_msg("INFO: SPARK CFG JumpFollowNodesMap redundant update at %llx\n", (uint64_t)LastAddr);
+							SMP_msg("INFO: SPARK: short-circuit CFG JumpFollowNodesMap redundant update at %llx\n", (uint64_t)LastAddr);
 						}
 					}
 				}
@@ -11590,13 +11591,13 @@ bool SMPFunction::AnalyzeConditionalStatements(void) {
 					map<STARS_ea_t, int>::iterator ExistingValueIter = InsertResult.first;
 					int OldFollowBlockNum = ExistingValueIter->second;
 					if (OldFollowBlockNum != FollowNodeNum) {
-						SMP_msg("ERROR: SPARK CFG JumpFollowNodesMap conflict at %llx Old: %d New:%d\n",
+						SMP_msg("ERROR: SPARK: Unstructured due to CFG JumpFollowNodesMap conflict at %llx Old: %d New:%d\n",
 							(uint64_t) LastAddr, OldFollowBlockNum, FollowNodeNum);
 						StructuredConditional = false;
 						break;
 					}
 					else {
-						SMP_msg("INFO: SPARK CFG JumpFollowNodesMap redundant update at %llx\n", (uint64_t) LastAddr);
+						SMP_msg("INFO: SPARK: CFG JumpFollowNodesMap redundant update at %llx\n", (uint64_t) LastAddr);
 					}
 				}
 
@@ -11616,7 +11617,7 @@ bool SMPFunction::AnalyzeConditionalStatements(void) {
 						map<STARS_ea_t, int>::iterator ExistingValueIter = InsertResult.first;
 						int OldFollowBlockNum = ExistingValueIter->second;
 						if (OldFollowBlockNum != FollowNodeNum) {
-							SMP_msg("ERROR: SPARK CFG JumpFollowNodesMap conflict at %llx Old: %d New:%d\n",
+							SMP_msg("ERROR: SPARK: Unstructured due to CFG JumpFollowNodesMap conflict at %llx Old: %d New:%d\n",
 								(uint64_t) ElsifAddr, OldFollowBlockNum, FollowNodeNum);
 							StructuredConditional = false;
 							break;
@@ -11627,7 +11628,7 @@ bool SMPFunction::AnalyzeConditionalStatements(void) {
 					}
 				} // end for each UnresolvedBranchBlock
 				if (!UnresolvedBranchBlocks.empty()) {
-					SMP_msg("INFO: SPARK CFG Resolved to ELSIF at %llx\n", (uint64_t) LastAddr);
+					SMP_msg("INFO: SPARK: CFG Resolved to ELSIF at %llx\n", (uint64_t) LastAddr);
 				}
 				UnresolvedBranchBlocks.clear();
 			}
@@ -11652,13 +11653,13 @@ bool SMPFunction::AnalyzeConditionalStatements(void) {
 					bool OddIfThenCase = LastInst->IsOddIfThenCase();
 					if (!OddIfThenCase) {
 						if (DistantBlockNum != FollowNodeNum) {
-							SMP_msg("ERROR: DistantBlock != FollowBlock for normal if-then at %llx in %s\n",
+							SMP_msg("ERROR: SPARK: Unstructured due to DistantBlock != FollowBlock for normal if-then at %llx in %s\n",
 								(uint64_t) LastInst->GetAddr(), this->GetFuncName());
 							this->HasStructuredCFG = false;
 						}
 					}
 					else if (DistantBlockNum == FollowNodeNum) {
-						SMP_msg("ERROR: DistantBlock == FollowBlock for OddIfThenCase at %llx in %s\n",
+						SMP_msg("ERROR: SPARK: Unstructured due to DistantBlock == FollowBlock for OddIfThenCase at %llx in %s\n",
 							(uint64_t) LastInst->GetAddr(), this->GetFuncName());
 						this->HasStructuredCFG = false;
 					}
@@ -11680,13 +11681,13 @@ bool SMPFunction::AnalyzeConditionalStatements(void) {
 							map<STARS_ea_t, int>::iterator ExistingValueIter = InsertResult.first;
 							int OldFollowBlockNum = ExistingValueIter->second;
 							if (OldFollowBlockNum != FollowNodeNum) {
-								SMP_msg("ERROR: SPARK CFG JumpFollowNodesMap conflict at %llx Old: %d New:%d\n",
+								SMP_msg("ERROR: SPARK: Unstructured due to CFG JumpFollowNodesMap conflict at %llx Old: %d New:%d\n",
 									(uint64_t) ElsifAddr, OldFollowBlockNum, FollowNodeNum);
 								StructuredConditional = false;
 								break;
 							}
 							else {
-								SMP_msg("INFO: SPARK CFG JumpFollowNodesMap redundant update at %llx\n", (uint64_t) ElsifAddr);
+								SMP_msg("INFO: SPARK: CFG JumpFollowNodesMap redundant update at %llx\n", (uint64_t) ElsifAddr);
 							}
 						}
 						// Find out if the unresolved branch should be translated as beginning a nested if-then, or a nested
@@ -11710,13 +11711,13 @@ bool SMPFunction::AnalyzeConditionalStatements(void) {
 					map<STARS_ea_t, int>::iterator ExistingValueIter = InsertResult.first;
 					int OldFollowBlockNum = ExistingValueIter->second;
 					if (OldFollowBlockNum != FollowNodeNum) {
-						SMP_msg("ERROR: SPARK CFG JumpFollowNodesMap conflict at %llx Old: %d New:%d\n",
+						SMP_msg("ERROR: SPARK: Unstructured due to CFG JumpFollowNodesMap conflict at %llx Old: %d New:%d\n",
 							(uint64_t) LastAddr, OldFollowBlockNum, FollowNodeNum);
 						StructuredConditional = false;
 						break;
 					}
 					else {
-						SMP_msg("INFO: SPARK CFG JumpFollowNodesMap redundant update at %llx\n", (uint64_t) LastAddr);
+						SMP_msg("INFO: SPARK: CFG JumpFollowNodesMap redundant update at %llx\n", (uint64_t) LastAddr);
 					}
 				}
 			} // end if (bad follownode) ... else ...
@@ -11770,25 +11771,61 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
 	//  in RPO order is dominated by HeadBlockNum but has a successor that exits the loops containing
 	//  HeadBlockNum, then there is a jump that spans loops inside the conditional statement,
 	//  which cannot be structured without transformation.
-	// If we did not find a FollowBlockNum, this will be a zero-trip loop.
+	//
+	// Note that if the exiting of the loop is a branch to the FollowBlock, then we can potentially
+	//  have:
+	//  loop
+	//    if cond1 then
+	//       [code1]
+	//       exit when cond2;
+	//    else
+	//       [code2]
+	//       exit when cond3;
+	//    endif;
+	//  endloop;
+	//  This case needs analysis below and is not a problem. The conditional follow node will be the same
+	//    as the loop follow node.
+	//
 	if (this->IsBlockInAnyLoop(HeadBlockNum)) {
 		int InnerMostLoopNum = this->GetInnermostLoopNum(HeadBlockNum);
 		assert(0 <= InnerMostLoopNum);
+		int InnerMostFollowBlockNum = this->LoopFollowNodes[(size_t)InnerMostLoopNum];
+		bool HitLoopFollowBlock = false;
+		// If we did not find a FollowBlockNum, this will be a zero-trip loop.
 		for (int BlockIndex = HeadBlockNum; BlockIndex < FollowBlockNum; ++BlockIndex) {
-			SMPBasicBlock *CurrBlock = this->GetBlockByNum((size_t)BlockIndex);
-			list<SMPBasicBlock *>::const_iterator SuccIter;
-			for (SuccIter = CurrBlock->GetFirstConstSucc(); SuccIter != CurrBlock->GetLastConstSucc(); ++SuccIter) {
-				int SuccBlockNum = (*SuccIter)->GetNumber();
-				if (!this->IsBlockInLoop(SuccBlockNum, (size_t) InnerMostLoopNum)) {
-					// We are exiting the innermost loop without finding FollowBlockNum.
-					SMP_msg("ERROR: SPARK: Loop-spanning branch to block %d from block %zu in func %s\n", SuccBlockNum, BlockIndex, this->GetFuncName());
-					FollowBlockNum = SMP_BLOCKNUM_UNINIT; // error signal
-					return FollowBlockNum;
+			if (this->DoesBlockDominateBlock(HeadBlockNum, BlockIndex)) { // inside conditional
+				SMPBasicBlock *CurrBlock = this->GetBlockByNum((size_t)BlockIndex);
+				list<SMPBasicBlock *>::const_iterator SuccIter;
+				for (SuccIter = CurrBlock->GetFirstConstSucc(); SuccIter != CurrBlock->GetLastConstSucc(); ++SuccIter) {
+					int SuccBlockNum = (*SuccIter)->GetNumber();
+					if (SuccBlockNum == InnerMostFollowBlockNum) {
+						HitLoopFollowBlock = true;
+						FollowBlockNum = InnerMostFollowBlockNum;
+					}
+					else if (!this->IsBlockInLoop(SuccBlockNum, (size_t)InnerMostLoopNum)) {
+						// We are exiting the innermost loop without finding InnerMostFollowBlockNum.
+						SMP_msg("ERROR: SPARK: Unstructured due to Loop-spanning branch to block %d from block %zu in func %s\n", SuccBlockNum, BlockIndex, this->GetFuncName());
+						FollowBlockNum = SMP_BLOCKNUM_UNINIT; // error signal
+						this->DumpDotCFG();
+						this->Dump();
+						return FollowBlockNum;
+					}
 				}
+#if 0  // audit below
+				if (HitLoopFollowBlock)
+					return FollowBlockNum;
+#endif
 			}
 		}
 	}
 
+	if (0 <= FollowBlockNum) {
+		if (this->FindUnstructuredIfThenElse(HeadBlockNum, FollowBlockNum)) {
+			FollowBlockNum = SMP_BLOCKNUM_UNINIT; // error signal
+			return FollowBlockNum;
+		}
+	}
+
 #if 0
 	// If we failed, see if it was because of both branches of an if-then-else
 	//  terminating with a RETURN. A call to a function that does not return, such
@@ -11891,7 +11928,7 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
 				FollowBlockNum = SMP_BLOCKNUM_COMMON_RETURN;
 			}
 			else { // unstructured, multi-level loop back
-				SMP_msg("ERROR: SPARK: Unstructured multi-level loop backs to block %d in func %s\n", SaveLoopHeadBlockNum, this->GetFuncName());
+				SMP_msg("ERROR: SPARK: Unstructured due to multi-level loop backs to block %d in func %s\n", SaveLoopHeadBlockNum, this->GetFuncName());
 				FollowBlockNum = SMP_BLOCKNUM_UNINIT; // error signal
 				return FollowBlockNum;
 			}
@@ -12167,6 +12204,77 @@ int SMPFunction::TrackConditionalBranchTerminus(int BranchHeadBlockNum, int Curr
 	return TerminusBlockNum;
 } // end of SMPFunction::TrackConditionalBranchTerminus()
 
+// Do IF and ELSE branches merge before FollowBlockNum?
+bool SMPFunction::FindUnstructuredIfThenElse(const int HeadBlockNum, const int FollowBlockNum) const {
+	bool UnstructuredClauses = false;
+
+	STARSBitSet ThenBlocksSeen, ElseBlocksSeen;
+	int BlockAlreadySeenCounter = 0;
+	SMPBasicBlock *HeadBlock = this->GetBlockByNum((size_t) HeadBlockNum);
+	ThenBlocksSeen.AllocateBits(this->GetNumBlocks());
+	ElseBlocksSeen.AllocateBits(this->GetNumBlocks());
+
+	// Arbitrarily call the first non-back-edge successor the THEN clause, second one the ELSE clause.
+	int ElseBlockNum = HeadBlock->GetCondNonFallThroughSuccBlockNum();
+	assert(SMP_BLOCKNUM_UNINIT != ElseBlockNum);
+	list<SMPBasicBlock *>::const_iterator ThenIter = HeadBlock->GetCondOtherSucc(ElseBlockNum);
+	assert(ThenIter != HeadBlock->GetLastConstSucc());
+	SMPBasicBlock *ThenBlock = (*ThenIter);
+
+	// Follow no back edges, start at ThenBlock, stop at FollowBlockNum, record blocks seen.
+	list<int> WorkList;
+	int ThenBlockNum = ThenBlock->GetNumber();
+	WorkList.push_back(ThenBlockNum);
+	while (!WorkList.empty()) { // RPO ordering, no back edges, ensures termination
+		int CurrBlockNum = WorkList.front();
+		WorkList.pop_front();
+		SMPBasicBlock *CurrBlock = this->GetBlockByNum(CurrBlockNum);
+		for (list<SMPBasicBlock *>::const_iterator SuccIter = CurrBlock->GetFirstConstSucc(); SuccIter != CurrBlock->GetLastConstSucc(); ++SuccIter) {
+			int SuccBlockNum = (*SuccIter)->GetNumber();
+			if (!ThenBlocksSeen.GetBit((size_t)SuccBlockNum)) { // don't follow an unstructured loop
+				if (!this->DoesBlockDominateBlock(SuccBlockNum, CurrBlockNum)) { // no back edge
+					if (SuccBlockNum != FollowBlockNum) {
+						ThenBlocksSeen.SetBit((size_t)SuccBlockNum);
+						WorkList.push_back(SuccBlockNum);
+					}
+				}
+			}
+		}
+	} // end while WorkList is not empty
+
+	WorkList.push_back(ElseBlockNum);
+	while (!WorkList.empty()) { // RPO ordering, no back edges, ensures termination
+		int CurrBlockNum = WorkList.front();
+		WorkList.pop_front();
+		SMPBasicBlock *CurrBlock = this->GetBlockByNum(CurrBlockNum);
+		for (list<SMPBasicBlock *>::const_iterator SuccIter = CurrBlock->GetFirstConstSucc(); SuccIter != CurrBlock->GetLastConstSucc(); ++SuccIter) {
+			int SuccBlockNum = (*SuccIter)->GetNumber();
+			if (!ElseBlocksSeen.GetBit((size_t)SuccBlockNum)) { // don't follow an unstructured loop
+				if (!this->DoesBlockDominateBlock(SuccBlockNum, CurrBlockNum)) { // no back edge
+					if (SuccBlockNum != FollowBlockNum) {
+						ElseBlocksSeen.SetBit((size_t)SuccBlockNum);
+						WorkList.push_back(SuccBlockNum);
+					}
+				}
+			}
+		}
+	} // end while WorkList is not empty
+
+	// A structured if-then-else should have no blocks reached from both THEN and ELSE
+	//  clauses, except the FollowBlock, which we avoided marking.
+	for (size_t BitIndex = 0; BitIndex < ThenBlocksSeen.GetNumBits(); ++BitIndex) {
+		if (ThenBlocksSeen.GetBit(BitIndex) && ElseBlocksSeen.GetBit(BitIndex)) {
+			UnstructuredClauses = true;
+			SMP_msg("ERROR: SPARK: Unstructured due to THEN and ELSE clauses merge prematurely at block %zu for HeadBlock %d FollowBlock %d in %s\n",
+				BitIndex, HeadBlockNum, FollowBlockNum, this->GetFuncName());
+			this->DumpDotCFG();
+			break;
+		}
+	}
+
+	return UnstructuredClauses;
+} // end of SMPFunction::FindUnstructuredIfThenElse()
+
 // Find guarded loops and fill the GuardToLoopMap and LoopToGuardMap
 void SMPFunction::FindGuardedLoops(void) {
 	assert(this->HasStructuredControlFlow());
@@ -14787,7 +14895,9 @@ void SMPFunction::AnalyzeLoopIterations(void) {
 				else {
 					SMP_msg("ERROR: LOOP: Failure to ReplaceIVsWithInitExpr (writes) for MemListIndex %zu loop %d in function at %llx\n",
 						MemListIndex, LoopIndex, (uint64_t) this->GetFirstFuncAddr());
-					MemWriteLowerBound->Dump(0);
+					if (VerboseOutput) {
+						MemWriteLowerBound->Dump(0);
+					}
 					delete MemWriteLowerBound;
 					this->LoopAnalysisProblems[LoopIndex] = true;
 				}
@@ -16490,7 +16600,7 @@ void SMPFunction::UpdateLoopFollowBlockNum(int LoopHeadBlockNum, int FollowBlock
 		if (SMP_BLOCKNUM_UNINIT == FollowBlockNum) {
 			if (this->HasGoodLoopFollowBlocks) {
 				this->HasGoodLoopFollowBlocks = false;
-				SMP_msg("ERROR: SPARK: Conflicting loop follow block nums for loop %d : %d and %d in %s\n",
+				SMP_msg("ERROR: SPARK: Unstructured due to conflicting loop follow block nums for loop %d : %d and %d in %s\n",
 					LoopNum, OldFollowNum, FollowBlockNum, this->GetFuncName());
 			}
 		}
@@ -16517,7 +16627,7 @@ void SMPFunction::UpdateLoopFollowBlockNum(int LoopHeadBlockNum, int FollowBlock
 			if (!success) {
 				if (this->HasGoodLoopFollowBlocks) {
 					this->HasGoodLoopFollowBlocks = false;
-					SMP_msg("ERROR: SPARK: Conflicting loop follow block nums for loop %d : %d and %d in %s\n",
+					SMP_msg("ERROR: SPARK: Unstructured due to conflicting loop follow block nums for loop %d : %d and %d in %s\n",
 						LoopNum, OldFollowNum, FollowBlockNum, this->GetFuncName());
 				}
 			}
@@ -16757,7 +16867,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 			// Detect special case of a C/C++ loop continue statement. See comments in SMPFunction::FindLoopContinuePattern().
 			bool OverlappingLoops = (CurrBlock->IsLoopHeaderBlock() && CurrBlock->IsLoopTailBlock() && (!CurrBlock->IsSelfLoop()));
 			if (OverlappingLoops) {
-				this->HasStructuredCFG = false;
+				this->HasStructuredCFG = false; // might handle the loop continue case (SingleExpr) below in future.
 				if (CurrBlock->IsSingleExpression()) {
 					SMP_msg("INFO: Overlapping loops single-expr loop continue special case at block %zu in %s\n", BlockIndex, this->GetFuncName());
 				}
@@ -16774,7 +16884,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 					STARS_ea_t JumpTarget = CurrInst->GetJumpTarget();
 					if ((STARS_BADADDR == JumpTarget) || (!this->IsInstIDInFunc(JumpTarget))) {
 						this->HasStructuredCFG = false;
-						SMP_msg("ERROR: SPARK: Bad jump target at %llx in %s\n", (uint64_t) InstAddr, this->GetFuncName());
+						SMP_msg("ERROR: SPARK: Unstructured due to bad jump target at %llx in %s\n", (uint64_t) InstAddr, this->GetFuncName());
 						break; // no point in continuing if we cannot translate to SPARK Ada
 					}
 
@@ -16851,7 +16961,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 							else {
 								// Fall-through to next function, probably IDA Pro problem in func ID.
 								this->HasStructuredCFG = false;
-								SMP_msg("ERROR: SPARK: Fall-through from %llx is not in function %s\n",
+								SMP_msg("ERROR: SPARK: Unstructured due to fall-through from %llx is not in function %s\n",
 									(uint64_t)InstAddr, this->GetFuncName());
 							}
 						}
@@ -16887,7 +16997,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 					//  test block.
 					STARS_ea_t JumpTarget = CurrInst->GetJumpTarget();
 					if ((STARS_BADADDR == JumpTarget) || (!this->IsInstIDInFunc(JumpTarget))) {
-						SMP_msg("ERROR: SPARK: Bad jump target at %llx in %s\n", (uint64_t) InstAddr, this->GetFuncName());
+						SMP_msg("ERROR: SPARK: Unstructured due to bad jump target at %llx in %s\n", (uint64_t) InstAddr, this->GetFuncName());
 						this->HasStructuredCFG = false;
 						break; // no point in continuing if we cannot translate to SPARK Ada
 					}
@@ -18603,6 +18713,13 @@ void SMPFunction::Dump(void) {
 			}
 			SMP_msg("\n");
 		}
+		if (!this->LoopToGuardMap.empty()) {
+			SMP_msg("Loop guards: ");
+			for (pair<STARS_ea_t, STARS_ea_t> LoopGuardPair : this->LoopToGuardMap) {
+				SMP_msg("\nLoop at %llx has guard at %llx", (uint64_t)LoopGuardPair.first, (uint64_t)LoopGuardPair.second);
+			}
+			SMP_msg("\n");
+		}
 	}
 
 	if (!this->EdgeExprMap.empty()) {
@@ -18638,7 +18755,7 @@ void SMPFunction::Dump(void) {
 } // end of SMPFunction::Dump()
 
 // Dump CFG representation for processing by "dot" program.
-void SMPFunction::DumpDotCFG(void) {
+void SMPFunction::DumpDotCFG(void) const {
 	string DotFileName(global_STARS_program->GetRootFileName());
 	DotFileName += ".STARS.";
 	char FuncBuf[20] = { '\0', '\0', '\0', '\0', '\0', '\0', '\0', '\0', '\0', '\0', '\0', '\0', '\0', '\0', '\0', '\0', '\0', '\0', '\0', '\0' };
@@ -22771,7 +22888,10 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
 			this->CleanUpSPARKLoopWorkList();
 
 			// See if we have a loop follow block number that is inside this conditional
-			//  and recurse into it if so.
+			//  and recurse into it if so. This is for the case in which the loop is entirely
+			//  contained within the conditional. We need to NOT recurse into the loop follow block
+			//  in the case where the conditional is entirely contained within a loop; in that case,
+			//  wait until we return to EmitSPARKAdaForLoop() to go into the loop follow node.
 			int LoopFollowBlockNum = this->LoopFollowNodes[LoopNum];
 			assert(0 < LoopFollowBlockNum);
 			SMPBasicBlock *LoopFollowBlock = this->GetBlockByNum((size_t) LoopFollowBlockNum);
diff --git a/src/base/SMPInstr.cpp b/src/base/SMPInstr.cpp
index e82d6ed2..180e1692 100644
--- a/src/base/SMPInstr.cpp
+++ b/src/base/SMPInstr.cpp
@@ -6908,7 +6908,14 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
 	// Print the disassembly as a comment before the SPARK translation.
 	STARS_ea_t InstAddr = this->GetAddr();
 	bool MightBeVisitedTwice = this->GetBlock()->IsSingleExpression() || this->GetBlock()->IsOnlyInternalDirectJump() || (InstAddr == this->GetBlock()->GetLastAddr()) || (CALL == this->GetDataFlowType());
-	assert(!this->HasBeenTranslatedToSPARK() || MightBeVisitedTwice);
+	bool ValidTranslation = (!this->HasBeenTranslatedToSPARK() || MightBeVisitedTwice);
+	if (!ValidTranslation) {
+		// Produce files to speed up debugging.
+		this->GetBlock()->GetFunc()->DumpDotCFG();
+		this->GetBlock()->GetFunc()->Dump();
+		SMP_msg("FATAL ERROR: EmitSPARKAda visiting inst at %llx twice.\n", (uint64_t) InstAddr);
+	}
+	assert(ValidTranslation);
 	SMP_fprintf(OutFile, "\n");
 	PrintSPARKIndentTabs(OutFile);
 	SMP_fprintf(OutFile, " -- %llx  %s\n", (unsigned long long) InstAddr, this->GetDisasm());
-- 
GitLab