From dca4d9d8264051a1bd711a32bbae433e27e519f9 Mon Sep 17 00:00:00 2001
From: Clark Coleman <clc@zephyr-software.com>
Date: Tue, 8 Sep 2020 13:38:59 -0400
Subject: [PATCH] SPARK Ada translation fixes.

---
 include/base/SMPBasicBlock.h |   1 +
 include/base/SMPFunction.h   |   4 +-
 include/base/SMPInstr.h      |   1 +
 src/base/SMPBasicBlock.cpp   |  37 ++++
 src/base/SMPFunction.cpp     | 405 ++++++++++++++++++++++++++++-------
 src/base/SMPInstr.cpp        |   2 +
 src/base/SMPProgram.cpp      |   1 +
 7 files changed, 373 insertions(+), 78 deletions(-)

diff --git a/include/base/SMPBasicBlock.h b/include/base/SMPBasicBlock.h
index cf871f35..9799c228 100644
--- a/include/base/SMPBasicBlock.h
+++ b/include/base/SMPBasicBlock.h
@@ -389,6 +389,7 @@ public:
 	bool AllPredecessorsProcessed(void);
 	void DepthFirstMark(bool MarkIBTBlocks); // Depth-first traversal, mark as processed.
 	void DepthFirstMarkNonBackEdgeSuccessors(void); // Depth-first, but do not follow back edges.
+	bool IsBlockReachableWithoutBackEdges(const int DestBlockNum) const; // path without back edges?
 	std::size_t GetNumPredsMinusBackEdges(void) const; // Compute predecessor count, excluding loop-back edges. Loop ID must occur first.
 	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);
diff --git a/include/base/SMPFunction.h b/include/base/SMPFunction.h
index 2f8f2739..3bc7d21f 100644
--- a/include/base/SMPFunction.h
+++ b/include/base/SMPFunction.h
@@ -555,6 +555,7 @@ public:
 	void MarkDominatedBlocks(int CurrBlockNum); // Set Processed flag for all blocks below CurrBlockNum in DomTree.
 	void ResetSCCPVisitedBlocks(void); // Set SCCPVisited flag to false in all blocks
 	void RPONumberBlocks(void); // Number basic blocks in reverse post-order and place pointers in RPOBlocks.
+	int FindLastBlockProcessedInChain(const int StartingBlockNum) const; // Find greatest RPO block in chain from StartingBlockNum, no back edges followed.
 	int GetFallThroughPredBlockNum(int CurrBlockNum); // return block # of block that falls through to CurrBlockNum; SMP_BLOCKNUM_UNINIT if none
 	void RemoveBlock(SMPBasicBlock *CurrBlock, std::list<SMPBasicBlock *>::iterator &BlockIter, bool IBTarget = false); // Remove a basic block and its instructions.
 	void RemoveCallingBlocks(void) const; // Func is empty, so add all blocks that call it to Program->BlocksPendingRemoval.
@@ -597,6 +598,7 @@ public:
 	bool IsBlockInAnyLoop(int BlockNum) const; // Is block (with block # BlockNum) inside any loop?
 	bool IsBlockInLoop(int BlockNum, std::size_t LoopNum); // Is block (with block # BlockNum) inside loop # LoopNum?
 	bool AreBlocksInSameLoops(const int BlockNum1, const int BlockNum2) const;
+	bool DoesEdgeExitLoop(const int BlockNum1, const int BlockNum2) const; // Does going from BlockNum1 to BlockNum2 exit a loop?
 	void BuildLoopList(int BlockNum, std::list<std::size_t> &LoopList); // build list of loop numbers that BlockNum is part of.
 	void BuildLoopBlockList(const size_t LoopNum, std::list<std::size_t> &BlockList); // build list of Block numbers contained in LoopNum.
 	void AnalyzeLoopIterations(void); // analyze how many times each loop iterates
@@ -977,7 +979,7 @@ private:
 	void FindDependentInductionVar(std::size_t LoopIndex, struct DependentInductionVar &DIV, STARSOpndTypePtr Add1, STARSOpndTypePtr Add2, STARSOpndTypePtr Mult1, STARSOpndTypePtr Mult2, SMPoperator RhsOperator, SMPInstr *DefInst); // pass in results of DefInst::IsDependentInductionVarArithmetic()
 	bool ReplaceLoopRegWithConst(std::size_t LoopIndex, STARSOpndTypePtr &RegOp, SMPInstr *UseInst); // If RegOp USE in UseInst is an SCCP constant, create an immediate operand for it.
 
-	void AddEdgeExpression(const int SourceBlockNum, const int TargetBlockNum, struct LoopComparison GuardExpr); // Add to EdgeExpressions vector and map
+	void AddEdgeExpression(const int SourceBlockNum, const int TargetBlockNum, const struct LoopComparison GuardExpr); // Add to EdgeExpressions vector and map
 
 	void ComputeInArgConstValues(void); // Fill InArgConstValues with SCCP values from call sites.
 	STARSExpression *CreateLimitExpr(const std::size_t &LoopIndex, const struct InductionVarFamily &IVFamily, const struct LoopComparison &LoopCompExpr); // Create loop limit expr: BIVOpnd relationaloperator Opnd2
diff --git a/include/base/SMPInstr.h b/include/base/SMPInstr.h
index 1ff69622..76d8cd34 100644
--- a/include/base/SMPInstr.h
+++ b/include/base/SMPInstr.h
@@ -812,6 +812,7 @@ public:
 	bool IsOddIfThenCase(void) const; // is poorly-optimized if-then COND_BRANCH with extra jumps
 	inline bool IsNop(void) const { return (booleans2 & INSTR_SET_NOP); }; // instruction is simple or complex no-op
 	inline bool MDIsFloatNop(void) const { return (GetIDAOpcode() == STARS_NN_fnop); };
+	inline bool MDIsExchange(void) const { return (GetIDAOpcode() == STARS_NN_xchg); };
 	bool IsMarkerInst(void) const;
 	bool IsDecrementRTL(void) const;
 	bool IsSetToZero(void) const;
diff --git a/src/base/SMPBasicBlock.cpp b/src/base/SMPBasicBlock.cpp
index 8854ed18..9d4035a3 100644
--- a/src/base/SMPBasicBlock.cpp
+++ b/src/base/SMPBasicBlock.cpp
@@ -383,6 +383,33 @@ void SMPBasicBlock::DepthFirstMarkNonBackEdgeSuccessors(void) {
 	return;
 } // end of SMPBasicBlock::DepthFirstMark()
 
+// Mark as processed, recurse into successors depth-first, do not follow back edges.
+bool SMPBasicBlock::IsBlockReachableWithoutBackEdges(const int DestBlockNum) const {
+	bool Found = false;
+	list<SMPBasicBlock *>::const_iterator CurrSucc;
+	int CurrBlockNum = this->GetNumber();
+	for (CurrSucc = this->GetFirstConstSucc(); CurrSucc != this->GetLastConstSucc(); ++CurrSucc) {
+		SMPBasicBlock *SuccBlock = (*CurrSucc);
+		int SuccBlockNum = SuccBlock->GetNumber();
+		if (SuccBlockNum > CurrBlockNum) { // not back edge
+			if (SuccBlockNum == DestBlockNum) {
+				Found = true;
+			}
+			else if (SuccBlockNum > DestBlockNum) {
+				// RPO ordering means we can no longer reach DestBlockNum without a back edge.
+				break; // return false
+			}
+			else {
+				Found = SuccBlock->IsBlockReachableWithoutBackEdges(DestBlockNum); // recurse, depth-first
+			}
+			if (Found)
+				break;
+		}
+	}
+
+	return Found;
+} // end of SMPBasicBlock::IsBlockReachableWithoutBackEdges()
+
 // Compute predecessor count, excluding loop-back edges. Loop ID must occur first.
 size_t SMPBasicBlock::GetNumPredsMinusBackEdges(void) const {
 	size_t PredCount = this->GetNumPreds();
@@ -531,6 +558,8 @@ void SMPBasicBlock::Dump(void) {
 
 // Call SMPInstr::EmitSPARKAda() until we hit a control flow inst.
 void SMPBasicBlock::EmitSPARKAdaForFallThroughInsts(FILE *BodyFile) {
+	PrintSPARKIndentTabs(BodyFile);
+	SMP_fprintf(BodyFile, "-- Block number %d\n", this->GetNumber());
 	STARS_ea_t LastID = this->GetLastAddr();
 	for (vector<SMPInstr *>::iterator InstIter = this->GetFirstInst(); InstIter != this->GetLastInst(); ++InstIter) {
 		SMPInstr *CurrInst = (*InstIter);
@@ -553,6 +582,8 @@ void SMPBasicBlock::EmitSPARKAdaForFallThroughInsts(FILE *BodyFile) {
 
 // Call SMPInstr::EmitSPARKAda() for all insts in block.
 void SMPBasicBlock::EmitSPARKAdaForAllInsts(FILE *BodyFile) {
+	PrintSPARKIndentTabs(BodyFile);
+	SMP_fprintf(BodyFile, "-- Block number %d\n", this->GetNumber());
 	for (vector<SMPInstr *>::iterator InstIter = this->GetFirstInst(); InstIter != this->GetLastInst(); ++InstIter) {
 		SMPInstr *CurrInst = (*InstIter);
 		bool Untranslatable = CurrInst->IsMarkerInst() || (!CurrInst->IsAnalyzeable());
@@ -728,6 +759,12 @@ bool SMPBasicBlock::EmitSPARKAdaForExprUse(FILE *BodyFile, vector<SMPInstr *>::c
 				Printed = false;
 				return true;
 			}
+			else if (CurrInst->MDIsExchange()) {
+				SMP_msg("ERROR: Not translating conditional move at %llx\n", (uint64_t)CurrAddr);
+				SMP_fprintf(BodyFile, "ERROR ");
+				Printed = false;
+				return true;
+			}
 			else {
 				SMPRegTransfer *DefRT = CurrInst->GetRT(0);
 				assert(IsEqOp(DefRT->GetConstLeftOperandNoNorm(), UseOp));
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index f74d212f..ef1ec5f5 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -377,6 +377,7 @@ SMPFunction::SMPFunction(STARS_Function_t *Info, SMPProgram* pgm) {
 	this->LiveOutSet.clear();
 	this->KillSet.clear();
 	this->GlobalDefAddrBySSA.clear();
+	this->EdgeExpressions.clear();
 
 	struct FineGrainedInfo TempFG;
 	TempFG.SignMiscInfo = 0;
@@ -592,6 +593,7 @@ bool SMPFunction::ComputeInOutRegs(bool InheritPass, bool &WritesMem, bool &Call
 	bool Changed = false;
 	bool MemoryInput = false;
 	bool MemoryOutput = false;
+	bool VerboseOutput = global_stars_interface->VerboseLoopsMode();
 	CallChainNonReturning = false;
 
 	if (InheritPass) {
@@ -708,7 +710,9 @@ bool SMPFunction::ComputeInOutRegs(bool InheritPass, bool &WritesMem, bool &Call
 					if (STARS_BADADDR != CalleeAddr) {
 						SMPFunction *CalleeFunc = this->GetProg()->FindFunction(CalleeAddr);
 						if ((nullptr != CalleeFunc) && CalleeFunc->StackPtrAnalysisSucceeded() && CalleeFunc->HasStructuredControlFlow()) {
-							SMP_msg("INFO: SPARK: Function %s inheriting mem exprs from callee %s\n", CurrFuncName.c_str(), CalleeFunc->GetFuncName());
+							if (VerboseOutput) {
+								SMP_msg("INFO: SPARK: Function %s inheriting mem exprs from callee %s\n", CurrFuncName.c_str(), CalleeFunc->GetFuncName());
+							}
 							size_t NumCalleeLoops = CalleeFunc->GetNumLoops();
 							for (size_t CalleeLoopIndexPlusOne = 0; CalleeLoopIndexPlusOne <= NumCalleeLoops; ++CalleeLoopIndexPlusOne) {
 								// Get non-loop mem write exprs that trace back to InArgs, trace them back from actual arg in this function.
@@ -779,8 +783,10 @@ bool SMPFunction::ComputeInOutRegs(bool InheritPass, bool &WritesMem, bool &Call
 									assert(nullptr != TempStringRangeExpr);
 									STARSExpression *CalleeStringRangeExpr = TempStringRangeExpr->Clone();
 									size_t MemWriteByteWidth = CalleeFunc->GetStringMemWriteRangeWidth(LoopIndexPlusOne, i);
-									SMP_msg("INFO: SPARK: Inheriting CalleeStringRangeExpr from CalleeAddr %llx at CallAddr %llx\n",
-										(uint64_t) CalleeAddr, (uint64_t) InstAddr);
+									if (VerboseOutput) {
+										SMP_msg("INFO: SPARK: Inheriting CalleeStringRangeExpr from CalleeAddr %llx at CallAddr %llx\n",
+											(uint64_t)CalleeAddr, (uint64_t)InstAddr);
+									}
 									Changed |= this->InheritCalleeMemRangeExpr(CalleeStringRangeExpr, CurrInst, MemWriteByteWidth, LoopNumOffsetByOne, LoopList);
 								}
 							} // end for all loops in CalleeFunc
@@ -4852,10 +4858,12 @@ void SMPFunction::EmitStackFrameAnnotations(FILE *AnnotFile, SMPInstr *Instr) {
 					STARS_asize_t TempOutArgsSize = (STARS_asize_t) this->OutgoingArgsSize;
 					if (this->GetLocalVarsSize() != (TempRegionBytes + TempOutArgsSize)) {
 						if (!this->HasPushAfterFrameAlloc()) {
+							// Suspect incorrect function boundaries in most of these cases.
 							SMP_msg("ERROR: LocalVarsSize: %lu not sum of CurrentRegionBytes: %lu  and OutArgsSize: %lu at %llx\n",
 								(unsigned long) this->GetLocalVarsSize(), (unsigned long)TempRegionBytes, (unsigned long)TempOutArgsSize, (uint64_t)addr);
 #if 1
 							this->Dump();
+							this->DumpDotCFG();
 #endif
 						}
 					}
@@ -7305,6 +7313,8 @@ void SMPFunction::DetectLoopInvariantDEFs(void) {
 						}
 						else {
 							// Assume memory operands are loop variant until we have full alias analysis.
+							// NOTE: This can cause mysterious annotation differences between SPARK mode
+							//  and non-SPARK mode, as the LoopInVariantDefs are used in induction var analysis.
 							UnanalyzableUse = UseOp->IsMemOp() || (UseOp->GetReg() == STARS_x86_R_ip);
 						}
 						if (UnanalyzableUse) {
@@ -7997,6 +8007,7 @@ bool SMPFunction::FindIVLiveRangeClosure(const size_t LoopIndex, const PhiSetIte
 void SMPFunction::DetectLoopInductionVars2(void) {
 	bool UseFP = this->UsesFramePointer();
 	bool VerboseOutput = global_stars_interface->VerboseLoopsMode();
+	bool AlreadyDumped = false; // prevent multiple debug dumps
 
 	// Initialize induction var vector with entries that have BIV*0 and SMP_SSA_UNINIT as markers
 	this->LoopInductionVars.resize(this->LoopCount);
@@ -8184,8 +8195,11 @@ void SMPFunction::DetectLoopInductionVars2(void) {
 										SMP_msg("\nExisting BIV candidate: ");
 										DumpInductionVar(CurrentFamily.BasicInductionVar);
 										SMP_msg("\n");
-										if (VerboseOutput)
+										if (VerboseOutput && (!AlreadyDumped)) {
 											this->Dump();
+											this->DumpDotCFG();
+											AlreadyDumped = true;
+										}
 										break;
 									}
 								}
@@ -8621,7 +8635,7 @@ bool SMPFunction::ReplaceLoopRegWithConst(std::size_t LoopIndex, STARSOpndTypePt
 } // end of SMPFunction::ReplaceRegWithConst()
 
 // Add edge expr to EdgeExpressions and EdgeExprMap.
-void SMPFunction::AddEdgeExpression(const int SourceBlockNum, const int TargetBlockNum, struct LoopComparison GuardExpr) {
+void SMPFunction::AddEdgeExpression(const int SourceBlockNum, const int TargetBlockNum, const struct LoopComparison GuardExpr) {
 	assert(0 <= SourceBlockNum);
 	assert(0 <= TargetBlockNum);
 	uint32_t EdgeHashIndex = (((uint32_t) SourceBlockNum << 16) | ((uint32_t) TargetBlockNum));
@@ -8660,16 +8674,32 @@ bool SMPFunction::ComputeEdgeExpressions(void) {
 	for (size_t BlockNum = 0; BlockNum < this->RPOBlocks.size(); ++BlockNum) {
 		SMPBasicBlock *CurrBlock = this->RPOBlocks[BlockNum];
 		if (CurrBlock->HasConditionalBranch()) {
-			int TestBlockNum = CurrBlock->GetNumber();
+			int BranchBlockNum = CurrBlock->GetNumber();
 			struct LoopComparison BranchExpr;
+
+			list<SMPBasicBlock *>::const_iterator BranchTakenIter = CurrBlock->GetCondNonFallThroughSucc();
+			bool ValidTakenEdge = (BranchTakenIter != CurrBlock->GetLastConstSucc());
+			list<SMPBasicBlock *>::const_iterator BranchNotTakenIter = CurrBlock->GetFallThroughSucc();
+			bool ValidFallThroughEdge = (BranchNotTakenIter != CurrBlock->GetLastConstSucc());
+			int TakenBlockNumber = ValidTakenEdge ? ((*BranchTakenIter)->GetNumber()) : SMP_BLOCKNUM_UNINIT;
+			int NotTakenBlockNumber = ValidFallThroughEdge ? ((*BranchNotTakenIter)->GetNumber()) : SMP_BLOCKNUM_UNINIT;
+			bool TakenBackEdge = ValidTakenEdge && this->DoesBlockDominateBlock(TakenBlockNumber, BranchBlockNum);
+			bool FallThroughBackEdge = ValidFallThroughEdge && this->DoesBlockDominateBlock(NotTakenBlockNumber, BranchBlockNum);
+
+			// Some idiotic code has a block ending with jz $+2, i.e. jump-on-zero to the very next
+			//  instruction, else fall through to the same instruction. Perhaps this is the result of an
+			//  optimization that was not followed by proper clean-up of the code. The result is that 
+			//  there is no need to compute an expression for the edge, as the edge is always taken.
+			bool LoneSuccessorCase = (TakenBlockNumber == NotTakenBlockNumber);
+			if (LoneSuccessorCase)
+				continue;
+
 			// Separate back edges from all others.
 			//  An edge from block A to block B is a back edge if B dominates A.
 			//  If the branch-taken edge is a back edge, we invert the branch expression
 			//  and record the fall-through edge. If the fall-through edge is a back edge,
 			//  we have a compiler-optimized code layout that requires us to record only
 			//  the branch-taken edge.
-			bool FallThroughBackEdge = false;
-			bool TakenBackEdge = false;
 
 			SMPoperator BranchOperator = SMP_NULL_OPERATOR;
 			STARS_ea_t DecrementAddr = STARS_BADADDR;
@@ -8681,62 +8711,65 @@ bool SMPFunction::ComputeEdgeExpressions(void) {
 					success = false;
 					break;
 				}
-				BranchExpr.CompareOperator = BranchOperator; // should be redundant
+				BranchExpr.CompareOperator = BranchOperator;
 				BranchExpr.CompareAddr = CompareOrTestInst->GetAddr();
+				// Transform RAX == RAX to RAX == 0; and RAX != RAX to RAX != 0; RAX >= RAX to RAX >= 0; etc.
+				//  We got SMP_EQUAL or SMP_NOT_EQUAL from the conditional branch instruction.
+				//  We want to transform the sequence:
+				//   test rax,rax
+				//   jz targetaddr
+				//
+				//  into: RAX == 0 as the edge expression.
+				if (IsEqOp(BranchExpr.Operand1.GetOp(), BranchExpr.Operand2.GetOp())) { // self-compare
+					STARSOpndTypePtr ZeroOp = CompareOrTestInst->MakeImmediateOpnd(0);
+					DefOrUse ZeroUse(ZeroOp);
+					BranchExpr.Operand2 = ZeroUse;
+				}
 			}
 			else if (STARS_BADADDR != DecrementAddr) {
 				// Found a decrement rather than a compare or test.
 				SMPInstr *DecrementInst = this->GetInstFromAddr(DecrementAddr);
 				assert(nullptr != DecrementInst);
-				if ((BranchOperator == SMP_EQUAL) || (BranchOperator == SMP_NOT_EQUAL)) {
-					BranchExpr.CompareOperator = BranchOperator;
-					BranchExpr.CompareAddr = DecrementAddr;
+				BranchExpr.CompareAddr = DecrementAddr;
+				BranchExpr.CompareOperator = BranchOperator;
+				if (IsRelationalOperator(BranchOperator)) {
+					// Branch will depend on how decremented value compares to zero. Transform as above.
 					STARSDefUseIter DecrementDEF = DecrementInst->GetFirstNonFlagsDef();
 					BranchExpr.Operand1 = (*DecrementDEF);
 					STARSOpndTypePtr ZeroOp = DecrementInst->MakeImmediateOpnd(0);
 					DefOrUse ZeroUse(ZeroOp);
 					BranchExpr.Operand2 = ZeroUse;
-
 				}
 				else {
 					SMP_msg("ERROR: COND_BRANCH: Decrement with BranchOperator %d in test block %d DecrementAddr %llx in func %s at %llx\n",
-						BranchOperator, TestBlockNum, (uint64_t)DecrementAddr, this->GetFuncName(), (uint64_t) this->GetFirstFuncAddr());
+						BranchOperator, BranchBlockNum, (uint64_t)DecrementAddr, this->GetFuncName(), (uint64_t) this->GetFirstFuncAddr());
 					success = false;
 					break;
 				}
-
-				// At this point, BranchExpr should be valid. Unless a loop back edge is
-				//  detected, we need to record the BranchExpr for the branch-taken edge
-				//  and the inverse of the BranchExpr for the fall-through edge.
-				// We have to deal with special cases in which we branch outside the current function
-				//  (might be incorrect grouping of instructions into functions) or even fall-through
-				//  to another function (also might be incorrect disassembly).
-				list<SMPBasicBlock *>::const_iterator BranchTakenIter = CurrBlock->GetCondNonFallThroughSucc();
-				bool ValidTakenEdge = (BranchTakenIter != CurrBlock->GetLastConstSucc());
-				list<SMPBasicBlock *>::const_iterator BranchNotTakenIter = CurrBlock->GetFallThroughSucc();
-				bool ValidFallThroughEdge = (BranchNotTakenIter != CurrBlock->GetLastConstSucc());
-				int TakenBlockNumber = ValidTakenEdge ? ((*BranchTakenIter)->GetNumber()) : SMP_BLOCKNUM_UNINIT;
-				int NotTakenBlockNumber = ValidFallThroughEdge ? ((*BranchNotTakenIter)->GetNumber()) : SMP_BLOCKNUM_UNINIT;
-				TakenBackEdge = ValidTakenEdge && this->DoesBlockDominateBlock(TakenBlockNumber, TestBlockNum);
-				FallThroughBackEdge = ValidFallThroughEdge && this->DoesBlockDominateBlock(NotTakenBlockNumber, TestBlockNum);
-
-				if (ValidTakenEdge && (!TakenBackEdge)) {
-					// Add guard expression for the taken edge.
-					this->AddEdgeExpression(TestBlockNum, TakenBlockNumber, BranchExpr);
-				}
-				if (ValidFallThroughEdge && (!FallThroughBackEdge)) {
-					// Add inverted guard expression for the fall-through edge.
-					struct LoopComparison InvertedBranchExpr = BranchExpr;
-					InvertedBranchExpr.CompareOperator = InvertRelationalOperator(BranchExpr.CompareOperator);
-					this->AddEdgeExpression(TestBlockNum, NotTakenBlockNumber, InvertedBranchExpr);
-				}
 			}
 			else {
 				SMP_msg("ERROR: COND_BRANCH: Could not find compare or test in test block %d in func %s at %llx\n",
-					TestBlockNum, this->GetFuncName(), (uint64_t) this->GetFirstFuncAddr());
+					BranchBlockNum, this->GetFuncName(), (uint64_t) this->GetFirstFuncAddr());
 				success = false;
 				break;
 			}
+
+			// At this point, BranchExpr should be valid. Unless a loop back edge is
+			//  detected, we need to record the BranchExpr for the branch-taken edge
+			//  and the inverse of the BranchExpr for the fall-through edge.
+			// We have to deal with special cases in which we branch outside the current function
+			//  (might be incorrect grouping of instructions into functions) or even fall-through
+			//  to another function (also might be incorrect disassembly).
+			if (ValidTakenEdge && (!TakenBackEdge)) {
+				// Add guard expression for the taken edge.
+				this->AddEdgeExpression(BranchBlockNum, TakenBlockNumber, BranchExpr);
+			}
+			if (ValidFallThroughEdge && (!FallThroughBackEdge)) {
+				// Add inverted guard expression for the fall-through edge.
+				struct LoopComparison InvertedBranchExpr = BranchExpr;
+				InvertedBranchExpr.CompareOperator = InvertRelationalOperator(BranchExpr.CompareOperator);
+				this->AddEdgeExpression(BranchBlockNum, NotTakenBlockNumber, InvertedBranchExpr);
+			}
 		}
 		else if (CurrBlock->HasIndirectJump()) {
 			// stub out for now
@@ -11701,29 +11734,47 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
 
 	// A well-structured candidate would be the biggest RPO-number block that has >= 2 predecessors
 	//  and has HeadBlockNum as its IDom. 
-	// EXCEPTION #1: Return instructions interrupt control flow. See below.
+	// EXCEPTION #1: Return and loop-back instructions interrupt control flow. See below.
 	// EXCEPTION #2: Short circuit conditionals can trick the IDom algorithm into choosing
-	//   one of the blocks in the short circuit expression as the follow node, when the follow
-	//   node should come after the entire short circuit expr.
+	//   one of the coalesced blocks in the short circuit expression as the follow node, when the follow
+	//   node should come after the entire short circuit expr. This happens if one branch ends in a 
+	//   return or loop-back and does not converge into a follow node.
 
 	STARS_ea_t HeadLastAddr = HeadBlock->GetLastAddr();
 	ControlFlowType LastCFType = this->GetControlFlowType(HeadLastAddr);
 	bool ShortCircuit = ((LastCFType == SHORT_CIRCUIT_BRANCH) || (LastCFType == SHORT_CIRCUIT_LOOP_EXIT));
 
-	if (!ShortCircuit) {
-		// Go through IDoms in reverse order until we find a well-structured candidate or hit HeadBlockNum.
-		int IDomIndex = (int) this->IDom.size() - 1;
-		while (IDomIndex > HeadBlockNum) {
-			if (this->IDom[IDomIndex] == HeadBlockNum) {
-				// COND_BRANCH block is the IDom for block # IDomIndex.
-				if (2 <= this->RPOBlocks[IDomIndex]->GetNumPredsMinusBackEdges()) { // success
-					FollowBlockNum = IDomIndex;
-					break;
-				}
+	// Go through DomTree[HeadBlockNum] in reverse order until we find a well-structured candidate or fail.
+	for (list<int>::const_reverse_iterator BlockIter = this->DomTree[HeadBlockNum].second.crbegin();
+		BlockIter != this->DomTree[HeadBlockNum].second.crend(); 
+		++BlockIter) {
+		int CurrBlockNum = (*BlockIter);
+		if (2 <= this->RPOBlocks[(size_t) CurrBlockNum]->GetNumPredsMinusBackEdges()) { // candidate
+			if (!(ShortCircuit && this->ShadowCFGBlocks[(size_t)CurrBlockNum]->IsCoalesced())) {
+				FollowBlockNum = CurrBlockNum;
+				break;
+			}
+		}
+	}
+
+	// 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
+	//  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;
 			}
-			--IDomIndex;
 		}
 	}
+
 #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
@@ -11789,7 +11840,8 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
 			SMPBasicBlock *CurrBlock = this->RPOBlocks[(size_t)BlockNum];
 			if (CurrBlock->IsLoopTailBlock() && this->DoesBlockDominateBlock(HeadBlockNum, BlockNum)) {
 				if (CurrBlock->HasLoopHeadAsSuccessor(LoopHeadBlockNum)) {
-					if (this->DoesBlockDominateBlock(LoopHeadBlockNum, BlockNum)) {
+					// Are we looping back to the loop that contains our conditional HeadBlockNum?
+					if (this->DoesBlockDominateBlock(LoopHeadBlockNum, HeadBlockNum)) {
 						if (0 == LoopBackCounter) {
 							SaveLoopHeadBlockNum = LoopHeadBlockNum;
 						}
@@ -11809,12 +11861,26 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
 						}
 						++LoopBackCounter;
 					}
+					else {
+						; // Test for loop being an inner loop within conditional??
+					}
 				}
 			}
 			--BlockNum;
 		} // end of while (BlockNum > HeadBlockNum)
 		if (2 <= LoopBackCounter) { // success; 2 or more if-elsif-else branches loop back to loop header
-			FollowBlockNum = SaveLoopHeadBlockNum;
+			// Screen out unstructured code. If we are jumping outside the loop containing the
+			//  conditional HeadBlockNum from two or more blocks dominated by HeadBlockNum, then
+			//  the code is doing a multi-level loop back, which is unstructured.
+			if (this->AreBlocksInSameLoops(HeadBlockNum, SaveLoopHeadBlockNum)) {
+				// FollowBlockNum = SaveLoopHeadBlockNum;
+				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());
+				FollowBlockNum = SMP_BLOCKNUM_UNINIT; // error signal
+				return FollowBlockNum;
+			}
 		}
 	}
 
@@ -11854,6 +11920,19 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
 			int ThenIDom = this->IDom[(size_t)ThenBlockNum];
 			int ElseIDom = this->IDom[(size_t)ElseBlockNum];
 			bool IfThenElseCase = ((ThenIDom == ElseIDom) && (ThenIDom == HeadBlockNum));
+			if (IfThenElseCase) {
+				// Screen out remaining if-then cases by ensuring that neither branch
+				//  can reach the other without following a back edge. It is sufficient
+				//  to check whether the lower RPO-numbered block can reach the other.
+				if (ThenBlockNum < ElseBlockNum) {
+					SMPBasicBlock *ThenBlock = this->GetBlockByNum(ThenBlockNum);
+					IfThenElseCase = (!ThenBlock->IsBlockReachableWithoutBackEdges(ElseBlockNum));
+				}
+				else {
+					SMPBasicBlock *ElseBlock = this->GetBlockByNum(ElseBlockNum);
+					IfThenElseCase = (!ElseBlock->IsBlockReachableWithoutBackEdges(ThenBlockNum));
+				}
+			}
 			if (!IfThenElseCase) {
 				// See if we fit the pattern above.
 				if (ThenIDom == HeadBlockNum)
@@ -12006,7 +12085,7 @@ int SMPFunction::TrackConditionalBranchTerminus(int BranchHeadBlockNum, int Curr
 			}
 
 			BlocksSeen.SetBit((size_t) SuccBlockNum);
-			bool OutsideTheLoop = this->AreBlocksInSameLoops(BranchHeadBlockNum, SuccBlockNum);
+			bool OutsideTheLoop = (!this->AreBlocksInSameLoops(BranchHeadBlockNum, SuccBlockNum));
 			if (OutsideTheLoop || (!this->DoesBlockDominateBlock(BranchHeadBlockNum, SuccBlockNum))) {
 				// We reached a block that is not dominated by BranchHeadBlockNum, or exited the loop.
 				//  Check for consistency with previous such blocks.
@@ -13172,6 +13251,34 @@ void SMPFunction::RPONumberBlocks(void) {
 	return;
 } // end of SMPFunction::RPONumberBlocks()
 
+// Find greatest RPO block in chain from StartingBlockNum, no back edges followed.
+int SMPFunction::FindLastBlockProcessedInChain(const int StartingBlockNum) const {
+	assert(0 <= StartingBlockNum);
+	assert(((size_t)StartingBlockNum) < this->GetNumBlocks());
+	int HighestRPOBlockFound = StartingBlockNum;
+
+	// Follow all successors, find highest block that IsProcessed().
+	SMPBasicBlock *StartingBlock = this->GetBlockByNum((size_t) StartingBlockNum);
+	assert(StartingBlock->IsProcessed());
+
+	for (list<SMPBasicBlock *>::const_iterator SuccIter = StartingBlock->GetFirstConstSucc();
+		SuccIter != StartingBlock->GetLastConstSucc();
+		++SuccIter) {
+		SMPBasicBlock *SuccBlock = (*SuccIter);
+		if (SuccBlock->IsProcessed()) {
+			int SuccBlockNum = SuccBlock->GetNumber();
+			if (SuccBlockNum <= StartingBlockNum) // back edge
+				continue;
+			int TempHighestFound = this->FindLastBlockProcessedInChain(SuccBlockNum);
+			if (HighestRPOBlockFound < TempHighestFound)
+				HighestRPOBlockFound = TempHighestFound;
+		}
+	}
+
+	return HighestRPOBlockFound;
+} // end of SMPFunction::FindLastBlockProcessedInChain()
+
+
 // return block # of block that falls through to CurrBlockNum; SMP_BLOCKNUM_UNINIT if none
 int SMPFunction::GetFallThroughPredBlockNum(int CurrBlockNum) {
 	assert((0 <= CurrBlockNum) && (CurrBlockNum < (int)this->RPOBlocks.size()));
@@ -13833,11 +13940,30 @@ bool SMPFunction::AreBlocksInSameLoops(const int BlockNum1, const int BlockNum2)
 		return true;
 	assert(((size_t) BlockNum1) < this->GetNumBlocks());
 	assert(((size_t) BlockNum2) < this->GetNumBlocks());
+	// Valid short cut based on how we detect and number loops?
 	bool SameLoops = (this->FuncLoopsByBlock[(std::size_t) BlockNum1].FindLowestBitSet() == this->FuncLoopsByBlock[(std::size_t) BlockNum2].FindLowestBitSet())
 		&& (this->FuncLoopsByBlock[(std::size_t) BlockNum1].FindHighestBitSet() == this->FuncLoopsByBlock[(std::size_t) BlockNum2].FindHighestBitSet());
 	return SameLoops;
 } // end of SMPFunction::AreBlocksInSameLoops()
 
+// Does going from BlockNum1 to BlockNum2 exit a loop?
+bool SMPFunction::DoesEdgeExitLoop(const int BlockNum1, const int BlockNum2) const {
+	bool ExitsLoop = false;
+	if (0 == this->GetNumLoops())
+		return ExitsLoop;
+	assert(((size_t)BlockNum1) < this->GetNumBlocks());
+	assert(((size_t)BlockNum2) < this->GetNumBlocks());
+	for (size_t LoopIndex = 0; LoopIndex < this->GetNumLoops(); ++LoopIndex) {
+		if (this->FuncLoopsByBlock[(size_t)BlockNum1].GetBit(LoopIndex)) {
+			if (!this->FuncLoopsByBlock[(size_t)BlockNum2].GetBit(LoopIndex)) {
+				ExitsLoop = true;
+				break;
+			}
+		}
+	}
+	return ExitsLoop;
+} // end of SMPFunction::DoesEdgeExitLoop()
+
 // build list of loop numbers that BlockNum is part of.
 void SMPFunction::BuildLoopList(int BlockNum, list<std::size_t> &LoopList) {
 	std::size_t LoopIndex;
@@ -16276,6 +16402,23 @@ void SMPFunction::UpdateLoopFollowBlockNum(int LoopHeadBlockNum, int FollowBlock
 	assert(SMP_BLOCKNUM_UNINIT != LoopHeadBlockNum);
 	size_t LoopNum = this->FindLoopNumFromHeadBlockNum(LoopHeadBlockNum);
 	int OldFollowNum = this->LoopFollowNodes[LoopNum];
+
+	// Safeguard against infinite loops. If our follow node is inside our loop,
+	//  we want to leave SMP_BLOCKNUM_UNINIT as the follow node. Ditto, if the follow node
+	//  dominates our LoopHeadBlockNum, SPARK translation will loop infinitely.
+	bool FollowDominatesHead = this->DoesBlockDominateBlock(FollowBlockNum, LoopHeadBlockNum);
+	if (FollowDominatesHead) {
+		SMP_msg("ERROR: SPARK: UpdateLoopFollowBlockNum() ignoring follow block %d which dominates loop head block %d in func %s at %llx loop %zu\n",
+			FollowBlockNum, LoopHeadBlockNum, this->GetFuncName(), (uint64_t) this->GetFirstFuncAddr(), LoopNum);
+		return;
+	}
+	bool FollowInsideLoop = this->IsBlockInLoop(FollowBlockNum, LoopNum);
+	if (FollowInsideLoop) {
+		SMP_msg("ERROR: SPARK: UpdateLoopFollowBlockNum() ignoring follow block %d inside loop with head block %d in func %s at %llx loop %zu\n",
+			FollowBlockNum, LoopHeadBlockNum, this->GetFuncName(), (uint64_t) this->GetFirstFuncAddr(), LoopNum);
+		return;
+	}
+
 	if (OldFollowNum == SMP_BLOCKNUM_UNINIT) {
 		this->LoopFollowNodes[LoopNum] = FollowBlockNum;
 	}
@@ -18191,10 +18334,6 @@ void SMPFunction::Dump(void) {
 			SMP_msg("\n");
 		}
 	}
-	for (CurrBlock = this->Blocks.begin(); CurrBlock != this->Blocks.end(); ++CurrBlock) {
-		// Dump out the block number and data flow sets before the instructions.
-		(*CurrBlock)->Dump();
-	}
 
 	if (!this->EdgeExprMap.empty()) {
 		SMP_msg(" Edge expressions:\n");
@@ -18202,7 +18341,7 @@ void SMPFunction::Dump(void) {
 			uint32_t EdgeHashIndex = EdgeMapEntry.first;
 			size_t EdgeVectorIndex = EdgeMapEntry.second;
 			uint32_t TargetBlockNum = EdgeHashIndex & 0x0000ffff;
-			uint32_t SourceBlockNum = EdgeHashIndex & 0xffff0000;
+			uint32_t SourceBlockNum = ((EdgeHashIndex & 0xffff0000) >> 16);
 			SMP_msg("  From block %u to block %u : ", SourceBlockNum, TargetBlockNum);
 			assert(EdgeVectorIndex < this->EdgeExpressions.size());
 			DumpLoopComparison(this->EdgeExpressions[EdgeVectorIndex]);
@@ -18210,6 +18349,10 @@ void SMPFunction::Dump(void) {
 		SMP_msg("\n");
 	}
 	
+	for (CurrBlock = this->Blocks.begin(); CurrBlock != this->Blocks.end(); ++CurrBlock) {
+		// Dump out the block number and data flow sets before the instructions.
+		(*CurrBlock)->Dump();
+	}
 
 	SMP_msg("End of debug dump for function: %s\n", this->GetFuncName());
 	return;
@@ -21289,6 +21432,11 @@ string SMPFunction::EmitSPARKProcForLoopHeaderBlock(int LoopIndex, int HeaderBlo
 				for (size_t VecIndex = 0; VecIndex < VectorLimit; ++VecIndex) {
 					// Print lower bound mem expr.
 					STARSExpression *MemExpr = (*(this->TempRangeExprWidthIters[VecIndex].first));
+					if (nullptr == MemExpr) {
+						SMP_msg("ERROR: SPARK: nullptr for lower bound mem expr in EmitSPARKProcForLoopHeaderBlock() in func %s at %llx loop %d VecIndex %zu\n",
+							this->GetFuncName(), (uint64_t) this->GetFirstFuncAddr(), LoopIndex, VecIndex);
+						continue;
+					}
 					MemExpr->PrintSPARKArgLocationStrings(HeaderFile, false, LoopNum, OutputCount, RegsPrinted);
 					// Print upper bound mem expr; if nullptr, print maximum limit.
 					MemExpr = (*(this->TempRangeExprWidthIters[VecIndex].second));
@@ -21680,6 +21828,8 @@ void SMPFunction::EmitSPARKLoopProcGlobals(FILE *BodyFile, FILE *HeaderFile, boo
 
 // recursive descent translation to SPARK Ada starting with CurrBlock, stop before Follow Block
 void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FILE *SPARKBodyFile, bool ReadytoEmitSwitchDefault, bool LoopToProc) {
+	PrintSPARKIndentTabs(SPARKBodyFile);
+	SMP_fprintf(SPARKBodyFile, "-- Basic block %d;\n", CurrBlockNum);
 	if (LoopToProc && (!this->IsSPARKLoopInTranslationStack())) {
 		// See if we are beginning to translate a guarded loop.
 		SMPBasicBlock *CurrBlock = this->GetBlockByNum(CurrBlockNum);
@@ -21716,7 +21866,7 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FIL
 			//  Could be an infinite loop. Otherwise, we should have a follow block.
 			bool FuncMightNotReturn = ((!this->FuncReturnsToCaller()) || this->HasCallToNonReturningFunc());
 			bool LoopMightBeInfinite = (STARS_INFINITE_OR_MIDDLE_TESTING_LOOP == this->LoopTypesByLoopNum[LoopNum]);
-			assert((SMP_BLOCKNUM_UNINIT != NextFollowBlockNum) || FuncMightNotReturn || LoopMightBeInfinite);
+			// assert((SMP_BLOCKNUM_UNINIT != NextFollowBlockNum) || FuncMightNotReturn || LoopMightBeInfinite);
 
 			if (LoopToProc) {
 				assert(TranslatingGuardedLoop || (ResumeBlockNum == NextFollowBlockNum)); // should be passed in as loop follow block number
@@ -21829,6 +21979,24 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FIL
 					else if (IsLoopExitFlow(LastCFType)) {
 						// Middle exit, else it would be loop header or tail handled above.
 						LastInst->EmitSPARKAda(SPARKBodyFile); // emit exit when (condition)
+						// If we conditionally exit the loop but the other successor is inside the loop,
+						//  we need to resume with the other successor.
+						list<SMPBasicBlock *>::const_iterator FallThroughIter = CurrBlock->GetFallThroughSucc();
+						assert(FallThroughIter != CurrBlock->GetLastConstSucc()); // COND_BRANCH always has a fall-through
+						SMPBasicBlock *FTBlock = (*FallThroughIter);
+						int FTBlockNum = FTBlock->GetNumber();
+						if (this->DoesEdgeExitLoop(CurrBlockNum, FTBlockNum)) {
+							// We want to resume with the block that does NOT exit the loop.
+							list<SMPBasicBlock *>::const_iterator NonFallThroughIter = CurrBlock->GetCondNonFallThroughSucc();
+							assert(NonFallThroughIter != CurrBlock->GetLastConstSucc()); // COND_BRANCH always has a fall-through
+							int NFTBlockNum = (*NonFallThroughIter)->GetNumber();
+							if ((!this->DoesEdgeExitLoop(CurrBlockNum, NFTBlockNum)) && !(*NonFallThroughIter)->IsProcessed()) {
+								ResumeBlockNum = NFTBlockNum;
+							}
+						}
+						else if (!FTBlock->IsProcessed()) {
+							ResumeBlockNum = FTBlockNum;
+						}
 					}
 					else {
 						assert((LastCFType == BRANCH_IF_THEN) || (LastCFType == BRANCH_IF_THEN_ELSE) || (LastCFType == SHORT_CIRCUIT_BRANCH));
@@ -21851,7 +22019,8 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FIL
 						int LoopNum = this->GetLoopNumFromHeaderBlockNum(NextBlockNum);
 						assert(0 <= LoopNum);
 						int NextFollowBlockNum = this->LoopFollowNodes[LoopNum];
-						assert(SMP_BLOCKNUM_UNINIT != NextFollowBlockNum);
+						bool LoopMightBeInfinite = (STARS_INFINITE_OR_MIDDLE_TESTING_LOOP == this->LoopTypesByLoopNum[LoopNum]);
+						// assert((SMP_BLOCKNUM_UNINIT != NextFollowBlockNum) || LoopMightBeInfinite);
 						if (LoopToProc) {
 							this->EmitSPARKAdaForLoop(NextBlockNum, NextFollowBlockNum, SPARKBodyFile); // recurse and return
 							ResumeBlockNum = NextFollowBlockNum;
@@ -21953,7 +22122,8 @@ void SMPFunction::EmitSPARKAdaForLoop(int HeaderBlockNum, int FollowBlockNum, FI
 			int LoopNum = this->GetLoopNumFromHeaderBlockNum(CurrBlockNum);
 			assert(0 <= LoopNum);
 			int NextFollowBlockNum = this->LoopFollowNodes[LoopNum];
-			assert(SMP_BLOCKNUM_UNINIT != NextFollowBlockNum);
+			bool LoopMightBeInfinite = (STARS_INFINITE_OR_MIDDLE_TESTING_LOOP == this->LoopTypesByLoopNum[LoopNum]);
+			// assert((SMP_BLOCKNUM_UNINIT != NextFollowBlockNum) || LoopMightBeInfinite);
 			this->EmitSPARKAdaLoopCall(CurrBlock->GetFirstAddr(), (size_t) LoopNum, SPARKBodyFile); 
 			ResumeBlockNum = NextFollowBlockNum;
 			pair<int, int> BlockItem(CurrBlockNum, ResumeBlockNum);
@@ -22057,7 +22227,8 @@ void SMPFunction::EmitSPARKAdaForLoop(int HeaderBlockNum, int FollowBlockNum, FI
 						int LoopNum = this->GetLoopNumFromHeaderBlockNum(NextBlockNum);
 						assert(0 <= LoopNum);
 						int NextFollowBlockNum = this->LoopFollowNodes[LoopNum];
-						assert(SMP_BLOCKNUM_UNINIT != NextFollowBlockNum);
+						bool LoopMightBeInfinite = (STARS_INFINITE_OR_MIDDLE_TESTING_LOOP == this->LoopTypesByLoopNum[LoopNum]);
+						// assert((SMP_BLOCKNUM_UNINIT != NextFollowBlockNum) || LoopMightBeInfinite);
 						this->EmitSPARKAdaLoopCall(NextBlock->GetFirstAddr(), (size_t) LoopNum, SPARKBodyFile);
 						ResumeBlockNum = NextFollowBlockNum;
 						LastInst->SetSPARKTranslated();
@@ -22210,6 +22381,11 @@ 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
+	//  so that we don't have a definite termination point.
+	bool UnknownFollowBlock = (0 > FollowBlockNum);
+	bool InsideLoop = this->IsSPARKLoopInTranslationStack();
+
 	// We need to detect the case in which we are beginning a guarded loop, i.e.
 	//  if cond then loop ... end loop; end if;
 	// For guarded loops, we save the COND_BRANCH location on the loop work list
@@ -22297,6 +22473,8 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
 		FallThroughBlockNum = (*SuccIter)->GetNumber();
 	}
 	SMPBasicBlock *ThenBlock = this->RPOBlocks[(size_t) FallThroughBlockNum];
+	bool CheckFTBlock = false; // check for falling out of loop?
+	bool CheckDistantBlock = false; // check for falling out of loop?
 	if (IfThenCase) {
 		// The common case is to jump around the ThenBlock, which can then fall-through to the FollowBlock:
 		//  if (cond) then goto L1;
@@ -22316,36 +22494,103 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
 		bool OddIfThenCase = LastInst->IsOddIfThenCase();
 		if (!OddIfThenCase) { // normal case
 			assert(DistantBlockNum == FollowBlockNum); // non-fall-through block is normal follow block for if-then
-			this->EmitSPARKAdaForBlock(FallThroughBlockNum, FollowBlockNum, SPARKBodyFile, false, (TranslatingGuardedLoop && !SaveAndReturn));
+			// Avoid generating code outside the loop from THEN clause if unknown follow block.
+			if (InsideLoop && UnknownFollowBlock && this->DoesEdgeExitLoop(HeaderBlockNum, FallThroughBlockNum)) {
+				PrintSPARKIndentTabs(SPARKBodyFile);
+				SMP_fprintf(SPARKBodyFile, "exit;\n");
+			}
+			else {
+				this->EmitSPARKAdaForBlock(FallThroughBlockNum, FollowBlockNum, SPARKBodyFile, false, (TranslatingGuardedLoop && !SaveAndReturn));
+			}
 		}
 		else {
 			// Need to generate the code for the ThenBlock == DistantBlock first.
-			this->EmitSPARKAdaForBlock(DistantBlockNum, FollowBlockNum, SPARKBodyFile, false, (TranslatingGuardedLoop && !SaveAndReturn));
+			// Avoid generating code outside the loop from THEN clause if unknown follow block.
+			if (InsideLoop && UnknownFollowBlock && this->DoesEdgeExitLoop(HeaderBlockNum, DistantBlockNum)) {
+				PrintSPARKIndentTabs(SPARKBodyFile);
+				SMP_fprintf(SPARKBodyFile, "exit;\n");
+			}
+			else {
+				this->EmitSPARKAdaForBlock(DistantBlockNum, DistantBlockNum, SPARKBodyFile, false, (TranslatingGuardedLoop && !SaveAndReturn));
+			}
 		}
+		this->SPARKControlStack.pop_back();
 	}
 	else {
-		this->SPARKControlStack.push_back(SPARK_THEN_CLAUSE);
-		this->EmitSPARKAdaForBlock(FallThroughBlockNum, FollowBlockNum, SPARKBodyFile, false);
-		this->SPARKControlStack.pop_back();
+		// Avoid generating code outside the loop from THEN clause if unknown follow block.
+		if (InsideLoop && UnknownFollowBlock && this->DoesEdgeExitLoop(HeaderBlockNum, FallThroughBlockNum)) {
+			PrintSPARKIndentTabs(SPARKBodyFile);
+			SMP_fprintf(SPARKBodyFile, "exit;\n");
+		}
+		else {
+			this->SPARKControlStack.push_back(SPARK_THEN_CLAUSE);
+			this->EmitSPARKAdaForBlock(FallThroughBlockNum, FollowBlockNum, SPARKBodyFile, false);
+			this->SPARKControlStack.pop_back();
+			CheckFTBlock = (InsideLoop && UnknownFollowBlock);
+		}
 		// SMPBasicBlock *ElseBlock = this->RPOBlocks[(size_t) DistantBlockNum];
 		--STARS_SPARK_IndentCount;
 		PrintSPARKIndentTabs(SPARKBodyFile);
 		SMP_fprintf(SPARKBodyFile, "else\n");
 		++STARS_SPARK_IndentCount;
-		this->SPARKControlStack.push_back(SPARK_ELSE_CLAUSE);
-		this->EmitSPARKAdaForBlock(DistantBlockNum, FollowBlockNum, SPARKBodyFile, false);
-		this->SPARKControlStack.pop_back();
+		// Avoid generating code outside the loop from ELSE clause if unknown follow block.
+		if (InsideLoop && UnknownFollowBlock && this->DoesEdgeExitLoop(HeaderBlockNum, DistantBlockNum)) {
+			PrintSPARKIndentTabs(SPARKBodyFile);
+			SMP_fprintf(SPARKBodyFile, "exit;\n");
+		}
+		else {
+			this->SPARKControlStack.push_back(SPARK_ELSE_CLAUSE);
+			this->EmitSPARKAdaForBlock(DistantBlockNum, FollowBlockNum, SPARKBodyFile, false);
+			this->SPARKControlStack.pop_back();
+			CheckDistantBlock = (InsideLoop && UnknownFollowBlock);
+		}
 	}
 
 	// We need to detect the odd case of falling through to a loop header with INVERTED_LOOP_EXIT,
 	//  i.e. we are doing a LOOP_BACK of sorts by falling out of the conditional,
 	//  in which case the "end if;" already was emitted before "end loop;" inside EmitSPARKAdaForBlock().
 	bool InvertedLoopExitCase = false;
-	if (FollowBlockNum >= 0) {
+	if (!UnknownFollowBlock) {
 		SMPBasicBlock *FollowBlock = this->GetBlockByNum((size_t) FollowBlockNum); // will be loop header that includes conditional in InvertedLoopExitCase
 		ControlFlowType FollowBlockCFType = FollowBlock->GetLastInstCFType();
 		InvertedLoopExitCase = (this->DoesBlockDominateBlock(FollowBlockNum, FallThroughBlockNum) && (INVERTED_LOOP_EXIT == FollowBlockCFType));
 	}
+#if 1
+	else if (InsideLoop) {
+		int LastBlockEmittedNum = this->FindLastBlockProcessedInChain(HeaderBlockNum);
+		SMPBasicBlock *LastBlockEmitted = this->GetBlockByNum((size_t) LastBlockEmittedNum);
+		assert(nullptr != LastBlockEmitted);
+		ControlFlowType LastCFType = LastBlockEmitted->GetLastInstCFType();
+		list<SMPBasicBlock *>::const_iterator FTSuccIter = LastBlockEmitted->GetFallThroughSucc();
+		if (FTSuccIter != LastBlockEmitted->GetLastConstSucc()) {
+			// Ended translation with a fall-through. Was it falling through to the top of the loop?
+			if (LastBlockEmittedNum > (*FTSuccIter)->GetNumber()) { // back edge
+				InvertedLoopExitCase = true;
+			}
+		}
+	}
+#else
+	else if (CheckDistantBlock) {
+		SMPBasicBlock *DistantBlock = this->GetBlockByNum((size_t)DistantBlockNum); // will be loop header that includes conditional in InvertedLoopExitCase
+		ControlFlowType DistantBlockCFType = DistantBlock->GetLastInstCFType();
+		if (INVERTED_LOOP_EXIT == DistantBlockCFType) {
+			SMPBasicBlock *LoopHeadBlock = *(DistantBlock->GetFallThroughSucc());
+			assert(nullptr != LoopHeadBlock);
+			assert(LoopHeadBlock->IsLoopHeaderBlock());
+			InvertedLoopExitCase = (this->DoesBlockDominateBlock(LoopHeadBlock->GetNumber(), DistantBlockNum));
+		}
+	}
+	if (!InvertedLoopExitCase && CheckFTBlock) {
+		SMPBasicBlock *FTBlock = this->GetBlockByNum((size_t)FallThroughBlockNum); // will be loop header that includes conditional in InvertedLoopExitCase
+		ControlFlowType FTBlockCFType = FTBlock->GetLastInstCFType();
+		if (INVERTED_LOOP_EXIT == FTBlockCFType) {
+			SMPBasicBlock *LoopHeadBlock = *(FTBlock->GetCondNonFallThroughSucc());
+			assert(nullptr != LoopHeadBlock);
+			assert(LoopHeadBlock->IsLoopHeaderBlock());
+			InvertedLoopExitCase = (this->DoesBlockDominateBlock(LoopHeadBlock->GetNumber(), FallThroughBlockNum));
+		}
+	}
+#endif
 	// Now we just need to emit the "end if;"
 	if (!InvertedLoopExitCase) {
 		--STARS_SPARK_IndentCount;
@@ -22355,6 +22600,11 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
 	else {
 		SMP_msg("INFO: SPARK: Not emitting end if for guarded conditional at %llx due to InvertedLoopExitCase\n",
 			(uint64_t) LastAddr);
+		if (UnknownFollowBlock) { // odd case of falling into header block loop-back
+			--STARS_SPARK_IndentCount;
+			PrintSPARKIndentTabs(SPARKBodyFile);
+			SMP_fprintf(SPARKBodyFile, "end loop;\n");
+		}
 	}
 
 	return;
@@ -22388,8 +22638,9 @@ int SMPFunction::FindFollowBlockNum(SMPBasicBlock *CurrBlock, bool StartAtLastIn
 		if (CurrBlock->IsLoopHeaderBlock()) {
 			int LoopNum = this->GetLoopNumFromHeaderBlockNum(CurrBlock->GetNumber());
 			assert(0 <= LoopNum);
+			bool LoopMightBeInfinite = (STARS_INFINITE_OR_MIDDLE_TESTING_LOOP == this->LoopTypesByLoopNum[LoopNum]);
 			FollowBlockNum = this->LoopFollowNodes[LoopNum];
-			assert(0 <= FollowBlockNum);
+			// assert((0 <= FollowBlockNum) || LoopMightBeInfinite);
 		}
 		else if (CurrBlock->IsSwitchDefaultCase()) {
 			STARS_ea_t DefaultCaseAddr = CurrBlock->GetFirstAddr();
diff --git a/src/base/SMPInstr.cpp b/src/base/SMPInstr.cpp
index 3b9cf6db..2a7a371d 100644
--- a/src/base/SMPInstr.cpp
+++ b/src/base/SMPInstr.cpp
@@ -6877,6 +6877,8 @@ void SMPInstr::EmitSPARKAdaLoopInvariants(FILE *BodyFile) const {
 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);
 	SMP_fprintf(OutFile, "\n");
 	PrintSPARKIndentTabs(OutFile);
 	SMP_fprintf(OutFile, " -- %llx  %s\n", (unsigned long long) InstAddr, this->GetDisasm());
diff --git a/src/base/SMPProgram.cpp b/src/base/SMPProgram.cpp
index ec6ed4fb..6dfa97f5 100644
--- a/src/base/SMPProgram.cpp
+++ b/src/base/SMPProgram.cpp
@@ -1162,6 +1162,7 @@ bool SMPProgram::EmitProgramSPARKAda(void) {
 					bool EdgeSuccess = TempFunc->ComputeEdgeExpressions();
 					if (global_stars_interface->VerboseLoopsMode()) {
 						TempFunc->Dump();
+						TempFunc->DumpDotCFG();
 					}
 				}
 			}
-- 
GitLab