From 35f09ea5cfbd1f390ab45dcb8c5cdb9a870e72fc Mon Sep 17 00:00:00 2001
From: Clark Coleman <clc@zephyr-software.com>
Date: Mon, 28 Sep 2020 09:39:26 -0400
Subject: [PATCH] SPARK: Translate structured loop_continue code; mark
 unstructured cases as untranslatable.

---
 include/base/SMPBasicBlock.h       |   3 +-
 include/base/SMPDataFlowAnalysis.h |   1 +
 include/base/SMPFunction.h         |   2 +
 src/base/SMPBasicBlock.cpp         |  12 +++-
 src/base/SMPFunction.cpp           | 107 ++++++++++++++++++++++-------
 src/base/SMPInstr.cpp              |  53 ++++++++------
 src/base/SMPProgram.cpp            |   7 ++
 7 files changed, 137 insertions(+), 48 deletions(-)

diff --git a/include/base/SMPBasicBlock.h b/include/base/SMPBasicBlock.h
index c81ad1df..5080d4a7 100644
--- a/include/base/SMPBasicBlock.h
+++ b/include/base/SMPBasicBlock.h
@@ -176,6 +176,7 @@ public:
 	std::list<SMPBasicBlock *>::const_iterator GetCondNonFallThroughSucc(void) const; // Search successors for condition non-fall-through block, if any
 	std::list<SMPBasicBlock *>::const_iterator GetCondOtherSucc(int NotThisBlockNum) const; // Search successors for conditional successor that is not #NotThisBlockNum
 	std::list<SMPBasicBlock *>::const_iterator GetSuccNotInLoop(std::size_t LoopNumber) const; // Search successors for conditional successor that is not in loop #LoopNumber
+	int GetCondNonFallThroughSuccBlockNum(void) const; // Search successors for condition non-fall-through block, if any; return block num or -1
 
 	inline std::size_t GetNumPreds(void) const { return Predecessors.size(); };
 	inline std::size_t GetNumSuccessors(void) const { return Successors.size(); };
@@ -346,7 +347,7 @@ public:
 	inline bool HasStaticMemWrite(void) const { return (booleans3 & BLOCK_SET_HAS_STATIC_MEM_WRITE); };
 	inline bool HasIndirectMemRead(void) const { return (booleans3 & BLOCK_SET_HAS_INDIRECT_READ); };
 	inline bool HasStaticMemRead(void) const { return (booleans3 & BLOCK_SET_HAS_STATIC_MEM_READ); };
-	inline bool IsSelfLoop(void) const { return (IsLoopHeaderBlock() && IsLoopTailBlock()); };
+	inline bool IsSelfLoop(void) const { return (IsLoopHeaderBlock() && IsLoopTailBlock() && (GetCondNonFallThroughSuccBlockNum() == GetNumber())); };
 	bool IsBlockPred(int BlockNum) const; // Is BlockNum a predecessor block of this block
 	bool HasLoopHeadAsSuccessor(int &HeadBlockNum) const; // block has HeadBlockNum as successor, which is a loop header
 	bool HasLoopHeadWithInvertedExitAsSuccessor(void) const; // block has loop head successor that ends with INVERTED_LOOP_EXIT
diff --git a/include/base/SMPDataFlowAnalysis.h b/include/base/SMPDataFlowAnalysis.h
index bd22eb8e..fef5ea87 100644
--- a/include/base/SMPDataFlowAnalysis.h
+++ b/include/base/SMPDataFlowAnalysis.h
@@ -664,6 +664,7 @@ enum ControlFlowType {
 	// JUMP_BEFORE_ELSE = 3,   // at the end of then section of if-then-else and before an ensuing else block
 	LOOP_BACK = 4,  // back edge from loop tail block to loop header block
 	LOOP_EXIT = 5,  // loop exit jump, becomes exit or exit-when in Ada
+	LOOP_CONTINUE = 6, // Code pattern from C/C++ loop continue statement; COND_BRANCH to loop header, fall-through path cannot be contained in if-then
 	JUMP_INTO_LOOP_TEST = 6, // jump to loop test block for first iteration of an optimized top-testing loop with loop test moved to the bottom
 	JUMP_TO_DEFAULT_CASE = 7,  // jump to default case of a switch statement
 	CASE_BREAK_TO_FOLLOW_NODE = 8, // jump at end of case in a switch statement to reach the switch follow node
diff --git a/include/base/SMPFunction.h b/include/base/SMPFunction.h
index f1225471..8d32f259 100644
--- a/include/base/SMPFunction.h
+++ b/include/base/SMPFunction.h
@@ -545,6 +545,7 @@ public:
 	inline bool CalleeUsesInArgsForLoopMemWrites(void) const { return CalleeHasLoopInArgMemWrites; };
 	inline bool IsCriticalInArg(std::size_t ArgPos) const { return (0 != (TaintInArgPosBits & (1 << ArgPos))); };
 	inline bool DoesLoopHaveArgs(int LoopNum) const { return LoopMemRangeInArgRegsBitmap[(size_t) LoopNum].any(); };
+	inline bool IsNonExitingLoopBackBranch(const STARS_ea_t BranchAddr) const { return LoopBackNonExitingBranches.find(BranchAddr) != LoopBackNonExitingBranches.cend(); };
 
 	// Printing methods
 	void Dump(void); // debug dump
@@ -753,6 +754,7 @@ private:
 	std::set<STARS_ea_t> ReturnTargets; // instructions that this function could return to
 	std::set<STARS_ea_t> JumpTableTargets; // code addresses found in jump tables for this func
 	std::set<STARS_ea_t> ResolvedCondBranches; // conditional branches resolved to always taken or never taken
+	std::set<STARS_ea_t> LoopBackNonExitingBranches; // COND_BRANCH loops back to loop header but fall-through stays in loop.
 	std::set<SMPFunction *> UnresolvedCallers; // temp set to resolve during ComputeReturnTargets()
 	std::map<STARS_ea_t, int> JumpFollowNodesMap; // map COND_BRANCH addresses to their follow nodes when exiting if-then-elsif-else structures
 	std::map<STARS_ea_t, SMPBasicBlock *> InstBlockMap;
diff --git a/src/base/SMPBasicBlock.cpp b/src/base/SMPBasicBlock.cpp
index 1ccaffd8..d7471f75 100644
--- a/src/base/SMPBasicBlock.cpp
+++ b/src/base/SMPBasicBlock.cpp
@@ -1045,7 +1045,7 @@ list<SMPBasicBlock *>::const_iterator SMPBasicBlock::GetCondNonFallThroughSucc(v
 		assert(STARS_BADADDR != NonFallThroughAddr);
 		for (list<SMPBasicBlock *>::const_iterator SuccIter = this->GetFirstConstSucc(); SuccIter != this->GetLastConstSucc(); ++SuccIter) {
 			SMPBasicBlock *SuccBlock = (*SuccIter);
-			if (SuccBlock->GetFirstAddr() == NonFallThroughAddr) {
+			if (SuccBlock->GetFirstNonMarkerAddr() == NonFallThroughAddr) {
 				BranchTakenSuccIter = SuccIter;
 				break;
 			}
@@ -1079,6 +1079,16 @@ std::list<SMPBasicBlock *>::const_iterator SMPBasicBlock::GetSuccNotInLoop(size_
 	return SuccIter;
 } // end of SMPBasicBlock::GetSuccNotInLoop()
 
+// Search successors for condition non-fall-through block, if any; return block num or -1
+int SMPBasicBlock::GetCondNonFallThroughSuccBlockNum(void) const {
+	int NFTSuccBlockNum = SMP_BLOCKNUM_UNINIT;
+	list<SMPBasicBlock *>::const_iterator SuccIter = this->GetCondNonFallThroughSucc();
+	if (SuccIter != this->GetLastConstSucc()) {
+		NFTSuccBlockNum = (*SuccIter)->GetNumber();
+	}
+	return NFTSuccBlockNum;
+} // end of SMPBasicBlock::GetCondNonFallThroughSuccBlockNum()
+
 // Is BlockNum a predecessor block of this block
 bool SMPBasicBlock::IsBlockPred(int BlockNum) const {
 	bool FoundPred = false;
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index 533ba2a1..c48443e5 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -4424,12 +4424,12 @@ int SMPFunction::GetLoopNumFromTestBlockNum(int BlockNum) const {
 // find innermost loop # for BlockNum
 int SMPFunction::GetInnermostLoopNum(const int BlockNum) const {
 	int LoopNum = -1;
-	size_t MinBlockCount = 100000;
+	size_t MinBlockCount = this->GetNumBlocks() + 1;
 	bool FuncHasLoops = (this->LoopCount > 0);
 	if ((BlockNum >= 0) && FuncHasLoops && this->IsBlockInAnyLoop(BlockNum)) {
 		// Find loop containing this BlockNum with the fewest number of blocks.
 		for (size_t LoopIndex = 0; LoopIndex < this->FuncLoopsByBlock[(size_t) BlockNum].GetNumBits(); ++LoopIndex) {
-			if (this->FuncLoopsByBlock[(size_t) BlockNum].GetBit(LoopIndex)) {
+			if (this->FuncLoopsByBlock[(size_t) BlockNum].GetBit(LoopIndex)) { // BlockNum is in loop #LoopIndex
 				size_t CurrBlockCount = this->FuncBlocksByLoop[LoopIndex].CountSetBits();
 				if (CurrBlockCount < MinBlockCount) {
 					MinBlockCount = CurrBlockCount;
@@ -4438,10 +4438,6 @@ int SMPFunction::GetInnermostLoopNum(const int BlockNum) const {
 			}
 		}
 	}
-	// Is the answer always the lowest loop number?
-	if (FuncHasLoops && this->FuncLoopsByBlock[(size_t)BlockNum].FindHighestBitSet() != LoopNum) {
-		SMP_msg("INFO: Innermost loop num is not highest loop num for block %d in %s\n", BlockNum, this->GetFuncName());
-	}
 	return LoopNum;
 } // end of SMPFunction::GetInnermostLoopNum()
 
@@ -7093,11 +7089,11 @@ void SMPFunction::DetectLoops(void) {
 				assert(FoundHeader);
 				this->ClassifyLoop(LoopNumber, HeaderExitFollowNum, TailExitFollowNum, CurrBlock, HeadBlock, HeaderBlockExitsLoop, TailBlockExitsLoop);
 			}
-			if (!this->HasStructuredControlFlow()) {
-				SMP_msg("WARNING: After ClassifyLoop() function %s at %llx is detected as unstructured.\n",
-					this->GetFuncName(), (uint64_t) this->GetFirstFuncAddr());
-			}
 		} // end if tail block
+		if (!this->HasStructuredControlFlow()) {
+			SMP_msg("WARNING: After ClassifyLoop() function %s at %llx is detected as unstructured.\n",
+				this->GetFuncName(), (uint64_t) this->GetFirstFuncAddr());
+		}
 	} // end for all blocks
 
 	return;
@@ -11771,19 +11767,24 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
 	}
 
 	// Audit result to find unstructured code. If any block >= HeadBlockNum and < FollowBlockNum
-	//  in RPO order is dominated by HeadBlockNum but has a successor not in the same loops as
+	//  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.
-	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->AreBlocksInSameLoops(HeadBlockNum, SuccBlockNum)) {
-				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->IsBlockInAnyLoop(HeadBlockNum)) {
+		int InnerMostLoopNum = this->GetInnermostLoopNum(HeadBlockNum);
+		assert(0 <= InnerMostLoopNum);
+		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;
+				}
 			}
 		}
 	}
@@ -16648,8 +16649,26 @@ bool SMPFunction::FindLoopContinuePattern(const int BranchBlockNum) {
 	//   pattern is NOT a loop continue statement and our SPARK Ada translation just needs to know
 	//   not to treat it like a LOOP_BACK that falls out of the loop.
 
-	const int InnerMostLoopIndex = this->GetInnermostLoopNum(BranchBlockNum);
+	// Another tricky case involves a basic block that is a tail block for an outer loop
+	//  and also a header block for an inner loop. If the block is nothing but a compare-and-branch
+	//  then it can be handled as a loop continue statement with additional boolean flags added.
+	//  But if it is not a single-expression block (nothing but compare and branch) then the code
+	//  other than the compare-and-branch actually has to be part of overlapping loops and cannot
+	//  be structured. We can weed out this case before we start tracing the dominator tree for the
+	//  more common case described above.
 	const SMPBasicBlock *BranchBlock = this->GetBlockByNum((size_t)BranchBlockNum);
+	bool OverlappingLoops = (BranchBlock->IsLoopHeaderBlock() && BranchBlock->IsLoopTailBlock() && (!BranchBlock->IsSelfLoop()));
+	if (OverlappingLoops) {
+		if (BranchBlock->IsSingleExpression()) {
+			SMP_msg("INFO: Overlapping loops single-expr loop continue special case at block %d in %s\n", BranchBlockNum, this->GetFuncName());
+			return true;
+		}
+		else {
+			SMP_msg("INFO: Overlapping loops non-single-expr unstructured CFG case at block %d in %s\n", BranchBlockNum, this->GetFuncName());
+			return false;
+		}
+	}
+	const int InnerMostLoopIndex = this->GetInnermostLoopNum(BranchBlockNum);
 	this->ResetProcessedBlocks();
 
 	return this->LoopContinueHelper(BranchBlockNum, InnerMostLoopIndex, BranchBlock);
@@ -16725,6 +16744,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 		this->HasStructuredCFG = false;
 	}
 
+
 	// Detect loop-related control flow first, then switches, then simple if-else control flow.
 	if ((this->LoopCount > 0) && this->HasReducibleControlFlow() && this->HasStructuredControlFlow()) {
 		for (size_t BlockIndex = 0; (BlockIndex < (size_t)this->BlockCount) && this->HasStructuredControlFlow(); ++BlockIndex) {
@@ -16734,6 +16754,18 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 			STARS_ea_t InstAddr = CurrInst->GetAddr();
 			SMPitype CurrDataFlowType = CurrInst->GetDataFlowType();
 
+			// 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;
+				if (CurrBlock->IsSingleExpression()) {
+					SMP_msg("INFO: Overlapping loops single-expr loop continue special case at block %zu in %s\n", BlockIndex, this->GetFuncName());
+				}
+				else {
+					SMP_msg("INFO: Overlapping loops non-single-expr unstructured CFG case at block %zu in %s\n", BlockIndex, this->GetFuncName());
+				}
+			}
+
 			// Find all conditional and unconditional jumps within the function.
 			if (((JUMP == CurrDataFlowType) || (COND_BRANCH == CurrDataFlowType))
 				&& (!CurrInst->IsFixedCallJump())) {
@@ -16802,7 +16834,18 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 								else if (this->FindLoopContinuePattern((int) BlockIndex)) {
 									SMP_msg("WARNING: SPARK: LOOP_CONTINUE case detected in block %d FollowBlock %d of %s\n", 
 										CurrBlock->GetNumber(), FollowBlockNum, this->GetFuncName());
+									this->HasStructuredCFG = false;
 									this->DumpDotCFG();
+									this->SetControlFlowType(InstAddr, LOOP_CONTINUE);
+								}
+								else {
+									// LOOP_BACK, but not LOOP_CONTINUE. Translation will need to be aware
+									//  that it needs to continue translating at FollowBlockNum in order
+									//  to avoid omitting code, unlike LOOP_BACK blocks that fall out of the
+									//  loop, as FollowBlockNum is still in the loop.
+									SMP_msg("INFO: SPARK: NON_CONTINUE LOOP_BACK case detected in block %d FollowBlock %d of %s\n",
+										CurrBlock->GetNumber(), FollowBlockNum, this->GetFuncName());
+									this->LoopBackNonExitingBranches.insert(InstAddr);
 								}
 							}
 							else {
@@ -18596,7 +18639,8 @@ void SMPFunction::Dump(void) {
 
 // Dump CFG representation for processing by "dot" program.
 void SMPFunction::DumpDotCFG(void) {
-	string DotFileName("STARS.");
+	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' };
 	// itoa(this->GetFirstFuncAddr(), FuncBuf, 16);
 	SMP_snprintf(FuncBuf, 18, "%x", this->GetFirstFuncAddr());
@@ -22409,8 +22453,18 @@ void SMPFunction::EmitSPARKAdaForLoop(int HeaderBlockNum, int FollowBlockNum, FI
 		else if (CurrBlock->IsLoopTailBlock()) {
 			// We are at the end of a recursive descent into a loop. Translate the block and return.
 			// NOTE: What about one-block loops, where block is header block and tail block?   !!!!****!!!!
-			CurrBlock->EmitSPARKAdaForAllInsts(SPARKBodyFile);
-			break;
+			STARS_ea_t BranchAddr = CurrBlock->GetLastAddr();
+			bool StaysInLoop = this->IsNonExitingLoopBackBranch(BranchAddr);
+			if (StaysInLoop) {
+				// At the end of CurrBlock, emit an if-then that encloses the path from fallthrough onwards. 
+				CurrBlock->EmitSPARKAdaForFallThroughInsts(SPARKBodyFile);
+				// The code for the if-then has scope until the end of the loop; use loop FollowBlockNum.
+				this->EmitSPARKAdaForConditional(CurrBlockNum, FollowBlockNum, SPARKBodyFile);
+			}
+			else {
+				CurrBlock->EmitSPARKAdaForAllInsts(SPARKBodyFile);
+				break;
+			}
 		}
 		else if (CurrBlock->IsSwitchDefaultCase()) {
 			// Translate switch-case statement.
@@ -22741,7 +22795,8 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
 	//  For the if-then case, we emit the code for the then-block and then "end if;" and return.
 	//  For the if-then-else case, we emit the code for the then-block and then "else" etc.
 	ControlFlowType LastCFType = this->GetControlFlowType(LastAddr);
-	bool IfThenCase = (LastCFType == BRANCH_IF_THEN);
+	bool StaysInLoop = this->IsNonExitingLoopBackBranch(LastAddr);
+	bool IfThenCase = ((LastCFType == BRANCH_IF_THEN) || ((LastCFType == LOOP_BACK) && StaysInLoop));
 	bool ShortCircuitCase = (LastCFType == SHORT_CIRCUIT_BRANCH);
 	assert(IfThenCase || ShortCircuitCase || (LastCFType == BRANCH_IF_THEN_ELSE));
 	int FallThroughBlockNum = SMP_BLOCKNUM_UNINIT;
@@ -22787,7 +22842,7 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
 		this->SPARKControlStack.push_back(SPARK_THEN_CLAUSE);
 		bool OddIfThenCase = LastInst->IsOddIfThenCase();
 		if (!OddIfThenCase) { // normal case
-			assert(DistantBlockNum == FollowBlockNum); // non-fall-through block is normal follow block for if-then
+			assert(StaysInLoop || (DistantBlockNum == FollowBlockNum)); // non-fall-through block is normal follow block for if-then
 			// Avoid generating code outside the loop from THEN clause if unknown follow block.
 			if (InsideLoop && UnknownFollowBlock && this->DoesEdgeExitLoop(HeaderBlockNum, FallThroughBlockNum)) {
 				PrintSPARKIndentTabs(SPARKBodyFile);
diff --git a/src/base/SMPInstr.cpp b/src/base/SMPInstr.cpp
index e0017ff4..e82d6ed2 100644
--- a/src/base/SMPInstr.cpp
+++ b/src/base/SMPInstr.cpp
@@ -7011,29 +7011,42 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
 #endif
 				}
 				else { // conditionally loops back, might fall out of loop if condition is false.
-					// We want to invert the condition and exit on the inverted condition, then fall through
-					//  to an unconditional loop back (i.e. "end loop;") statement.
-					PrintSPARKIndentTabs(OutFile);
-					SMP_fprintf(OutFile, "exit when ");
-					this->MDEmitSPARKAdaInvertedCondition(OutFile);
-					SMP_fprintf(OutFile, ";\n");
-					// Two cases: Loop back from tail block, or loop back from optimized top-testing loop
-					//  where the header block is moved to the bottom of the loop and reached on the first
-					//  iteration by a JUMP_INTO_LOOP_TEST unconditional jump. In the tail block case, we
-					//  are ready for "end loop;" but in the header block case we need to fall through into
-					//  the second block of the loop.
-					if (this->GetBlock()->IsLoopTailBlock()) {
-#if STARS_SPARK_CENTRALIZE_EMIT_LOOP
-						;
-#else
-						--STARS_SPARK_IndentCount;
+					bool StaysInLoop = this->GetBlock()->GetFunc()->IsNonExitingLoopBackBranch(InstAddr);
+					if (StaysInLoop) {
+						// Code has been analyzed to ensure this is not a LOOP_CONTINUE case, so it is safe
+						//  to enclose the rest of the code branch inside an if-then by inverting the LOOP_BACK
+						//  condition.
 						PrintSPARKIndentTabs(OutFile);
-						SMP_fprintf(OutFile, "end loop;\n\n");
-#endif
+						SMP_fprintf(OutFile, "if ");
+						this->MDEmitSPARKAdaInvertedCondition(OutFile);
+						SMP_fprintf(OutFile, " then \n");
+						++STARS_SPARK_IndentCount;
 					}
 					else {
-						assert(this->GetBlock()->IsOptimizedTopLoopTest());
-						assert(this->GetBlock()->IsLoopHeaderBlock());
+						// We want to invert the condition and exit on the inverted condition, then fall through
+						//  to an unconditional loop back (i.e. "end loop;") statement.
+						PrintSPARKIndentTabs(OutFile);
+						SMP_fprintf(OutFile, "exit when ");
+						this->MDEmitSPARKAdaInvertedCondition(OutFile);
+						SMP_fprintf(OutFile, ";\n");
+						// Two cases: Loop back from tail block, or loop back from optimized top-testing loop
+						//  where the header block is moved to the bottom of the loop and reached on the first
+						//  iteration by a JUMP_INTO_LOOP_TEST unconditional jump. In the tail block case, we
+						//  are ready for "end loop;" but in the header block case we need to fall through into
+						//  the second block of the loop.
+						if (this->GetBlock()->IsLoopTailBlock()) {
+	#if STARS_SPARK_CENTRALIZE_EMIT_LOOP
+							;
+	#else
+							--STARS_SPARK_IndentCount;
+							PrintSPARKIndentTabs(OutFile);
+							SMP_fprintf(OutFile, "end loop;\n\n");
+	#endif
+						}
+						else {
+							assert(this->GetBlock()->IsOptimizedTopLoopTest());
+							assert(this->GetBlock()->IsLoopHeaderBlock());
+						}
 					}
 				}
 			}
diff --git a/src/base/SMPProgram.cpp b/src/base/SMPProgram.cpp
index 85509a29..c1e652e5 100644
--- a/src/base/SMPProgram.cpp
+++ b/src/base/SMPProgram.cpp
@@ -1147,6 +1147,12 @@ bool SMPProgram::EmitProgramSPARKAda(void) {
 	for (FuncIter = this->FuncMap.begin(); FuncIter != this->FuncMap.end(); ++FuncIter) {
 		SMPFunction *TempFunc = FuncIter->second;
 		if (TempFunc == nullptr) continue;
+		bool FuncFound = (0x444492 == TempFunc->GetFirstFuncAddr());
+		if (FuncFound) {
+			TempFunc->Dump();
+			TempFunc->DumpDotCFG();
+		}
+
 		if (TempFunc->HasStructuredControlFlow()) {
 			TempFunc->EmitFuncSPARKAda();
 		}
@@ -1159,6 +1165,7 @@ bool SMPProgram::EmitProgramSPARKAda(void) {
 				SMP_fprintf(SpecFile, "procedure %s with\n", TempFunc->GetFuncName());
 				SMP_fprintf(SpecFile, "\tGlobal => (In_Out => X86.RSP),\n");
 				SMP_fprintf(SpecFile, "\tPost => (X86.RSP = X86.RSP'Old + 8);\n\n");
+				SMP_fprintf(BodyFile, "-- Minimal stub emitted due to unstructured control flow.\n");
 				SMP_fprintf(BodyFile, "procedure %s is\nbegin\n\tX86.RSP := X86.RSP + %u;\n", TempFunc->GetFuncName(), ByteWidth);
 				SMP_fprintf(BodyFile, "end %s;\n\n", TempFunc->GetFuncName());
 
-- 
GitLab