From fac13e3c56558d2a50b69a69ec5f06b2a6db8896 Mon Sep 17 00:00:00 2001
From: Clark Coleman <clc@zephyr-software.com>
Date: Thu, 12 Nov 2020 23:57:17 -0500
Subject: [PATCH] SPARK: Nearing completion of translation of multi-exit-target
 loops and SHORT_CIRCUIT_INVERTED_LOOP_EXITs.

---
 include/base/SMPBasicBlock.h       |   8 +
 include/base/SMPDataFlowAnalysis.h |  16 +-
 include/base/SMPFunction.h         |  23 +-
 include/base/SMPInstr.h            |   4 +
 src/base/SMPBasicBlock.cpp         |  97 +++++
 src/base/SMPFunction.cpp           | 635 ++++++++++++++++++++++++-----
 src/base/SMPInstr.cpp              |  87 +++-
 src/base/SMPProgram.cpp            |  20 +-
 8 files changed, 742 insertions(+), 148 deletions(-)

diff --git a/include/base/SMPBasicBlock.h b/include/base/SMPBasicBlock.h
index 067a4782..458d4e07 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
+	std::list<SMPBasicBlock *>::const_iterator GetSuccInLoop(std::size_t LoopNumber) const; // Search successors for first conditional successor that is 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(); };
@@ -330,6 +331,7 @@ public:
 #endif
 	inline bool AreFlagsDeadBeforeFirstKill(void) const { return (booleans1 & BLOCK_SET_FLAGS_DEAD_BEFORE_FIRST_KILL); };
 	bool AllNops(void); // Are all instructions in the block no-ops?
+	bool IsSPARKTranslated(void) const;
 	inline bool MaybeAliasedWrite(void) const { return (booleans1 & BLOCK_SET_ALIASED_WRITE); };
 	inline bool IsReachesOutStale(void) const { return (booleans2 & BLOCK_SET_REACHES_OUT_STALE); };
 	inline bool IsLoopTailBlock(void) const { return (booleans2 & BLOCK_SET_LOOP_TAIL_BLOCK); };
@@ -600,6 +602,10 @@ public:
 	// Printing methods
 	void EmitSPARKAdaShortCircuitExpr(FILE *BodyFile); // Emit SPARK Ada short circuit expr for entire expression tree.
 
+	// Analysis methods
+	int GetSuccNumNotInLoop(std::size_t LoopNum) const; // Get Successor block number that is not in loop #LoopNum; for SHORT_CIRCUIT_LOOP_EXIT
+	int GetSuccNumInLoop(std::size_t LoopNum) const; // Get Successor block number that is in loop #LoopNum; for SHORT_CIRCUIT_LOOP_EXIT
+
 private:
 	SMPoperator ShortCircuitOper;  // always SMP_LOGICAL_OR or SMP_LOGICAL_AND for our purposes, except initialized to SMP_NULL_OPERATOR
 	STARSCondExpr *LeftExpr;  // NULL if left expr is just a block number
@@ -629,9 +635,11 @@ public:
 	STARSCondExpr *GetExpr(void) const { return ShortCircuitExpr; };
 	SMPFunction *GetFunc(void) const { return MyFunc; };
 	inline int GetOriginalBlockNum(void) const { return BlockNum; };
+	inline int GetCoalescedBlockNum(void) const { return CoalescedBlockNum; };
 
 	// Set methods
 	void SetCoalesced(void) { Coalesced = true; };
+	void SetCoalescedBlockNum(const int CoalescedIntoNum) { CoalescedBlockNum = CoalescedIntoNum; };
 	void SetExpr(STARSCondExpr *NewExpr) { ShortCircuitExpr = NewExpr; };
 
 private:
diff --git a/include/base/SMPDataFlowAnalysis.h b/include/base/SMPDataFlowAnalysis.h
index d455c571..1cae1eb8 100644
--- a/include/base/SMPDataFlowAnalysis.h
+++ b/include/base/SMPDataFlowAnalysis.h
@@ -673,17 +673,27 @@ enum ControlFlowType {
 	JUMP_TO_SWITCH_INDIR_JUMP = 9,  // jump around default case or preliminary calculations to INDIR_JUMP block for switch
 	SHORT_CIRCUIT_BRANCH = 10,   // any branch in short-circuit conditional evaluation
 	SHORT_CIRCUIT_LOOP_EXIT = 11,  // short-circuit compound conditional expression that exits loop when true
-	INVERTED_LOOP_EXIT = 12, // COND_BRANCH falls out of loop via headerblock, branch taken stays in loop; code layout puts headerblock at bottom
-	INVERTED_LOOP_BACK = 13 // COND_BRANCH falls through to loop headerblock of its containing innermost loop
+	INVERTED_LOOP_EXIT = 12, // COND_BRANCH falls out of loop, branch taken stays in loop; code layout puts headerblock at bottom
+	INVERTED_LOOP_BACK = 13, // COND_BRANCH falls through to loop headerblock of its containing innermost loop
+	SHORT_CIRCUIT_INVERTED_LOOP_EXIT = 14 // short-circuit compound conditional expression falls out of loop when false, stays in loop when true
 };
 
 // Strings for debug dumps of ControlFlowType.
 extern const char *CFTTypeStrings[20];
 
 inline bool IsLoopExitFlow(ControlFlowType CFType) {
-	return ((LOOP_EXIT == CFType) || (SHORT_CIRCUIT_LOOP_EXIT == CFType) || (INVERTED_LOOP_EXIT == CFType));
+	return ((LOOP_EXIT == CFType) || (SHORT_CIRCUIT_LOOP_EXIT == CFType) || (INVERTED_LOOP_EXIT == CFType) || (SHORT_CIRCUIT_INVERTED_LOOP_EXIT == CFType));
 }
 
+inline bool IsInvertedLoopExitFlow(ControlFlowType CFType) {
+	return ((INVERTED_LOOP_EXIT == CFType) || (SHORT_CIRCUIT_INVERTED_LOOP_EXIT == CFType));
+}
+
+inline bool IsShortCircuitFlow(ControlFlowType CFType) {
+	return ((SHORT_CIRCUIT_BRANCH == CFType) || (SHORT_CIRCUIT_LOOP_EXIT == CFType) || (SHORT_CIRCUIT_INVERTED_LOOP_EXIT == CFType));
+}
+
+
 class DisAsmString {
 public:
 	DisAsmString(void);
diff --git a/include/base/SMPFunction.h b/include/base/SMPFunction.h
index 81f213fc..3c841d51 100644
--- a/include/base/SMPFunction.h
+++ b/include/base/SMPFunction.h
@@ -338,6 +338,7 @@ public:
 	int GetLoopNumFromTestBlockNum(int BlockNum) const;
 	int GetInnermostLoopNum(int BlockNum) const; // find innermost loop # for BlockNum
 	int GetOutermostLoopNum(int BlockNum) const; // find outermost loop # for BlockNum
+	int GetInnermostDominatingLoopNum(const int BlockNum) const; // Find innermost loop # whose head block dominates BlockNum
 	std::size_t GetNumLoopMemWriteExprBoundsEntries(void) const { return LoopMemWriteBoundsExprs.size(); };
 	STARSExprBoundsIter GetFirstLoopMemWriteExprBoundsIter(std::size_t LoopIndex) const { return LoopMemWriteBoundsExprs[LoopIndex].cbegin(); };
 	STARSExprBoundsIter GetLastLoopMemWriteExprBoundsIter(std::size_t LoopIndex) const { return LoopMemWriteBoundsExprs[LoopIndex].cend(); };
@@ -391,6 +392,7 @@ public:
 	const std::bitset<1 + MD_LAST_REG_NO> &GetCalleePreservedRegs(void) const { return CalleePreservedRegs; };
 	uint32_t GetTaintInArgPositions(void) const { return TaintInArgPosBits; };
 	std::string GetFuncSPARKSuffixString(void) const; // produce string "_hexaddress" for first address in func
+	std::string GenerateSPARKLoopExitBooleanName(const size_t LoopNum, const int ExitTargetBlockNum) const; // e.g. STARSExitLoop2ToBlock5
 
 	// Set methods
 	void ResetJumpToFollowNodeCounter(STARS_ea_t InstAddr); // Set counter to zero, or insert zero counter if none found
@@ -547,6 +549,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(); };
+	bool DoesLoopHaveMultipleExitTargets(const size_t LoopNum) const;
 	inline bool IsNonExitingLoopBackBranch(const STARS_ea_t BranchAddr) const { return LoopBackNonExitingBranches.find(BranchAddr) != LoopBackNonExitingBranches.cend(); };
 
 	// Printing methods
@@ -789,8 +792,8 @@ private:
 	std::vector<int> LoopTypesByLoopNum; // indexed by loop number: top-testing, bottom-testing, middle-testing or infinite
 	std::vector<int> LoopTestBlocksByLoopNum; // indexed by loop number; block number of header block for top-testing or tail block for bottom-testing, -1 for middle-testing
 	std::vector<int> LoopHeadBlockNumbers; // indexed by loop number; block number of header block
-	std::vector<std::set<int> > LoopFollowNodes; // indexed by loop number; block number of follow block
-	std::vector<std::map<int, STARSBitSet> > LoopFollowNodesReachabilitySets; // indexed by LoopNum, map exit target block num to bitset of block nums downward reachable from exit block num; SPARK-useful if multiple exit block targets
+	std::vector<std::set<int> > LoopExitTargets; // indexed by loop number; block number of exit destinations
+	std::vector<std::map<int, STARSBitSet> > LoopExitTargetsReachabilitySets; // indexed by LoopNum, map exit target block num to bitset of block nums downward reachable from exit block num; SPARK-useful if multiple exit block targets
 	std::vector<bool> LoopHasMultipleExits; 
 	std::vector<bool> LoopWritesMemory; // static, indirect or indexed writes
 	std::vector<bool> LoopReadsMemory; // static, indirect or indexed reads
@@ -907,6 +910,7 @@ private:
 	std::map<STARS_ea_t, STARS_ea_t> GuardToLoopMap; // inverse map of COND_BRANCH addr of guard to loop address for guarded loop
 	std::map<STARS_ea_t, std::size_t> SwitchJumpMap; // map inst ID of indirect jump to switch statement #; switch statements are
 			// numbered starting at zero as they are encountered in a post-order traversal of the graph
+	std::map<int, std::set<int> > MultiLoopExitTargetsConvergenceMap; // map LoopNum to BlockNums of reachable nodes convergence points of all loop follow nodes
 	std::vector<struct SwitchTableInfo> SwitchInfoArray; // same index as the size_t value in SwitchJumpMap
 
 	std::vector<struct LoopComparison> EdgeExpressions; // Expressions that gate each edge in CFG
@@ -977,8 +981,10 @@ private:
 	void DetectLoopFollowBlock(const std::size_t LoopNumber); // Detect successor blocks not in loop; if not exactly one, not structured CFG.
 	void ClassifyLoop(std::size_t LoopNumber, int HeaderExitFollowNum, int TailExitFollowNum, SMPBasicBlock *CurrBlock, SMPBasicBlock *HeadBlock, bool HeaderBlockExitsLoop, bool TailBlockExitsLoop); // classify LoopNumber loop as top, middle, or bottom testing
 	bool DoesBlockExitLoop(std::size_t LoopNumber, SMPBasicBlock *LoopBlock, int &FollowBlockNum); // return true if block can exit the loop.
-	void ComputeLoopFollowNodesReachability(const std::size_t LoopNum); // populate entry in LoopFollowNodesReachabilitySets
-	void MarkReachableBlocks(const int BlockNum, STARSBitSet &ReachableSet); // Set bits of current BlockNum and its descendants in CFG
+	bool DetectMultiLevelLoopBreak(const int LoopBlockNum, const int ExitTargetBlockNum) const; // Is ExitTargetBlockNum more than 1 loop nesting level away from LoopBlockNum?
+	void ComputeLoopFollowNodesReachability(const std::size_t LoopNum); // populate entry in LoopExitTargetsReachabilitySets
+	void MarkReachableBlocks(const int BlockNum, const std::size_t LoopNum, int LoopHeadBlockNum, STARSBitSet &ReachableSet); // Set bits of current BlockNum and its descendants in CFG that are dominated by LoopHeadBlockNum
+	uint32_t GetReachableSourcesCount(const std::size_t BlockNum, const std::size_t LoopNum) const; // How many of the multiple exit targets from LoopNum reach BlockNum?
 	void DetectLoopInvariantDEFs(void); // Collect a set of loop-invariant DEFs with the inst IDs of the DEFs.
 	void DetectLoopInvariantDEFs2(void); // Collect a set of loop-invariant DEFs with the inst IDs of the DEFs.
 	bool IsUseLoopInvariantDEF(std::size_t LoopIndex, const STARSOpndTypePtr &UseOp, SMPInstr *UseInst); // Track UseOp to its DEF, see if loop-invariant for LoopIndex
@@ -1015,8 +1021,8 @@ private:
 	bool AnalyzeMemWriteSafety(void); // Try to find safe indirect memory writes
 	void UpdateLoopFollowBlockNum(int HeaderBlockNum, int FollowBlockNum);
 	int FindFollowBlockNum(SMPBasicBlock *CurrBlock, bool StartAtLastInst = false); // Based on control flow structure of CurrBlock, find Ada follow block num; -1 if no structure besides fall-through
-	bool GetLoopFollowBlockNum(const std::size_t LoopNum, int &FirstFollowBlockNum) const; // return true if loop has multiple follow blocks
-	bool IsBlockLoopFollowBlock(const std::size_t LoopNum, const int BlockNum) const; // found in LoopFollowNodes[LoopNum] set?
+	bool GetLoopFollowBlockNum(const std::size_t LoopNum, int &FollowBlockNum) const; // return true if loop has multiple follow blocks
+	bool IsBlockLoopFollowBlock(const std::size_t LoopNum, const int BlockNum) const; // found in LoopExitTargets[LoopNum] set?
 	bool AnalyzeSwitchStatement(SMPBasicBlock *CurrBlock); // Analyze switch starting at indir jump at end of CurrBlock; return false if not well-structured
 	void FindSwitchIDom(struct SwitchTableInfo &TableInfo); // Mark jumps to default case, find IDom of entire switch statement
 	void BuildShadowCFG(void); // build skeleton CFG, then use in coalescing nodes to analyze expressions
@@ -1045,11 +1051,12 @@ private:
 	std::string EmitSPARKProcForLoopHeaderBlock(int LoopIndex, int HeaderBlockNum, int FollowBlockNum, FILE *BodyFile, FILE *HeaderFile); // Create SPARK procedure for loop starting at HeaderBlockNum
 	void AnalyzeLoopGlobals(int HeaderBlockNum, int FollowBlockNum, STARS_ea_t LoopAddr, bool &MemoryInput, bool &MemoryOutput, std::bitset<1 + MD_LAST_REG_NO> &InputRegs, std::bitset<1 + MD_LAST_REG_NO> &OutputRegs, std::bitset<1 + MD_LAST_REG_NO> &CalleePreservedRegs); // Analyze reg and mem accesses in loop
 	void EmitSPARKLoopProcGlobals(FILE *BodyFile, FILE *HeaderFile, bool MemoryInput, bool MemoryOutput, const std::bitset<1 + MD_LAST_REG_NO> &InputRegs, const std::bitset<1 + MD_LAST_REG_NO> &OutputRegs, const std::bitset<1 + MD_LAST_REG_NO> &CalleePreservedRegs); // emit Input, Output, In_Out flow annotations
-	void EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FILE *SPARKBodyFile, bool ReadytoEmitSwitchDefault, bool LoopToProc = false); // recursive descent translation to SPARK Ada starting with CurrBlock, stop before Follow Block
+	void EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FILE *SPARKBodyFile, bool ReadytoEmitSwitchDefault, bool LoopToProc, const uint32_t ReachableSourcesCount = 0); // recursive descent translation to SPARK Ada starting with CurrBlock, stop before Follow Block
 	void EmitSPARKAdaForLoop(int HeaderBlockNum, int FollowBlockNum, FILE *SPARKBodyFile); // recursive descent translation of loop to SPARK Ada starting with header CurrBlock, stop before Follow Block
+	void EmitSPARKAdaForMultipleLoopExitTargets(FILE *SPARKBodyFile, std::size_t LoopNum); // translate multiple exit targets & their reachable region
 	void EmitSPARKAdaForSwitch(int HeaderBlockNum, int FollowBlockNum, FILE *SPARKBodyFile); // recursive descent translation of switch statement starting with INDIR_JUMP block, stop before Follow Block
 	void EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlockNum, FILE *SPARKBodyFile); // recursive descent translation of if-else statement starting with COND_BRANCH block, stop before Follow Block
-	void EmitSPARKAdaLoopCall(STARS_ea_t LoopAddr, std::size_t LoopIndex, FILE *SPARKBodyFile); // emit call to loop proc that will be created later starting at LoopAddr
+	bool EmitSPARKAdaLoopCall(STARS_ea_t LoopAddr, std::size_t LoopIndex, FILE *SPARKBodyFile); // emit call to loop proc that will be created later starting at LoopAddr
 	void FreeSSAMemory(void); // After SSA #s are in DEFs and USEs, free SSA data structures.
 	bool FindSwitchStatementFollowBlock(struct SwitchTableInfo &TableInfo); // return false if no consistent follow block
 	int FindCaseFollowBlock(int CaseBlockNum, int HeaderBlockNum, std::size_t IncomingEdgeCount) const; // Start at CaseBlockNum, return followblocknum with IncomingEdgeCount 
diff --git a/include/base/SMPInstr.h b/include/base/SMPInstr.h
index 84d2c8e9..08d105b3 100644
--- a/include/base/SMPInstr.h
+++ b/include/base/SMPInstr.h
@@ -46,6 +46,7 @@
 #include "interfaces/abstract/STARSInstruction.h"
 
 class SMPProgram;
+class STARSCFGBlock;
 
 // Should we emit 64-bit register manipulations for all SPARK Ada
 //  translations? If not, we will emit procedure calls to read and write
@@ -1235,6 +1236,9 @@ private:
 	bool IsMultiplyByLargeConstant(STARS_uval_t &ConstValue, unsigned short SignMask); // Multiply by large constant; overflow is probably intentional.
 	bool IsSubtractionOfLargeConstant(STARS_uval_t &ConstValue, unsigned short SignMask); // Subtraction of large constant; underflow is probably intentional.
 	bool IsAdditionOfLargeConstant(STARS_uval_t &ConstValue, unsigned short SignMask); // Addition of large constant; overflow is probably intentional.
+
+	void EmitSPARKConditionalLoopMultiExit(FILE *BodyFile, const size_t LoopNum, const bool InvertCondition, const STARSCFGBlock *CFGBlock = nullptr);
+
 	bool BuildRTL(void);   // Build RTL trees; return true if successfully built.
 	bool BuildARM64RTL(void);   // Build RTL trees for ARM64; return true if successfully built.
 	bool BuildX86RTL(void);   // Build RTL trees for X86; return true if successfully built.
diff --git a/src/base/SMPBasicBlock.cpp b/src/base/SMPBasicBlock.cpp
index dd7cbb25..1f4e750d 100644
--- a/src/base/SMPBasicBlock.cpp
+++ b/src/base/SMPBasicBlock.cpp
@@ -449,6 +449,13 @@ bool SMPBasicBlock::AllNops(void) {
 	return ((0 == GoodCount) && (0 < NopCount));
 } // end of SMPBasicBlock::AllNops()
 
+bool SMPBasicBlock::IsSPARKTranslated(void) const {
+	STARS_ea_t FirstInstAddr = this->GetFirstNonMarkerAddr();
+	SMPInstr *FirstInst = this->GetInstFromIndex(this->GetIndexFromInstAddr(FirstInstAddr));
+	assert(nullptr != FirstInst);
+	return FirstInst->HasBeenTranslatedToSPARK();
+} // end of SMPBasicBlock::IsSPARKTranslated()
+
 // Analyze basic block and fill data members.
 void SMPBasicBlock::Analyze() {
 	vector<SMPInstr *>::reverse_iterator RevInstIter = this->GetRevInstBegin();
@@ -1077,6 +1084,17 @@ std::list<SMPBasicBlock *>::const_iterator SMPBasicBlock::GetSuccNotInLoop(size_
 	return SuccIter;
 } // end of SMPBasicBlock::GetSuccNotInLoop()
 
+// Search successors for first conditional successor that is not in loop #LoopNumber
+std::list<SMPBasicBlock *>::const_iterator SMPBasicBlock::GetSuccInLoop(size_t LoopNumber) const {
+	std::list<SMPBasicBlock *>::const_iterator SuccIter;
+	for (SuccIter = this->GetFirstConstSucc(); SuccIter != this->GetLastConstSucc(); ++SuccIter) {
+		int SuccBlockNum = (*SuccIter)->GetNumber();
+		if (this->GetFunc()->IsBlockInLoop(SuccBlockNum, LoopNumber))
+			break;
+	}
+	return SuccIter;
+} // end of SMPBasicBlock::GetSuccInLoop()
+
 // 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;
@@ -7969,5 +7987,84 @@ void STARSCondExpr::EmitSPARKAdaShortCircuitExpr(FILE *BodyFile) {
 	return;
 } // end of STARSCondExpr::EmitSPARKAdaShortCircuitExpr()
 
+// Get Successor block number that is not in loop #LoopNum; for SHORT_CIRCUIT_LOOP_EXIT
+int STARSCondExpr::GetSuccNumNotInLoop(size_t LoopNum) const {
+	int SuccBlockNumOutsideLoop = SMP_BLOCKNUM_UNINIT;
+	const SMPFunction *CurrFunc = this->MyCFGBlock->GetFunc();
+	int LeftBlockNum = this->GetLeftBlockNum();
+	int RightBlockNum = this->GetRightBlockNum();
+	if (!CurrFunc->IsBlockInLoop(LeftBlockNum, LoopNum)) {
+		SuccBlockNumOutsideLoop = LeftBlockNum;
+	}
+	else if (!CurrFunc->IsBlockInLoop(RightBlockNum, LoopNum)) {
+		SuccBlockNumOutsideLoop = RightBlockNum;
+	}
+	else if (0 <= LeftBlockNum) {
+		SMPBasicBlock *LeftBlock = CurrFunc->GetBlockByNum((size_t)LeftBlockNum);
+		list<SMPBasicBlock *>::const_iterator SuccIter = LeftBlock->GetSuccNotInLoop(LoopNum);
+		if (SuccIter != LeftBlock->GetLastConstSucc()) {
+			SuccBlockNumOutsideLoop = (*SuccIter)->GetNumber();
+		}
+	}
+	if (SMP_BLOCKNUM_UNINIT == SuccBlockNumOutsideLoop) { // no success yet
+		if (0 <= RightBlockNum) {
+			SMPBasicBlock *RightBlock = CurrFunc->GetBlockByNum((size_t)RightBlockNum);
+			list<SMPBasicBlock *>::const_iterator SuccIter = RightBlock->GetSuccNotInLoop(LoopNum);
+			if (SuccIter != RightBlock->GetLastConstSucc()) {
+				SuccBlockNumOutsideLoop = (*SuccIter)->GetNumber();
+			}
+		}
+	}
+	if (SMP_BLOCKNUM_UNINIT == SuccBlockNumOutsideLoop) { // no success yet; recurse into sub-exprs
+		if ((nullptr != this->GetLeftExpr()) && (SMP_BLOCKNUM_UNINIT != (SuccBlockNumOutsideLoop = this->GetLeftExpr()->GetSuccNumNotInLoop(LoopNum)))) {
+			;
+		}
+		else if ((nullptr != this->GetRightExpr()) && (SMP_BLOCKNUM_UNINIT != (SuccBlockNumOutsideLoop = this->GetRightExpr()->GetSuccNumNotInLoop(LoopNum)))) {
+			;
+		}
+	}
+
+	return SuccBlockNumOutsideLoop;
+} // end of STARSCondExpr::GetSuccNumNotInLoop()
+
+
+// Get Successor block number that is in loop #LoopNum; for SHORT_CIRCUIT_LOOP_EXIT/SHORT_CIRCUIT_INVERTED_LOOP_EXIT
+int STARSCondExpr::GetSuccNumInLoop(size_t LoopNum) const {
+	int SuccBlockNumInsideLoop = SMP_BLOCKNUM_UNINIT;
+	const SMPFunction *CurrFunc = this->MyCFGBlock->GetFunc();
+	int LeftBlockNum = this->GetLeftBlockNum();
+	int RightBlockNum = this->GetRightBlockNum();
+	if (CurrFunc->IsBlockInLoop(LeftBlockNum, LoopNum)) {
+		SuccBlockNumInsideLoop = LeftBlockNum;
+	}
+	else if (CurrFunc->IsBlockInLoop(RightBlockNum, LoopNum)) {
+		SuccBlockNumInsideLoop = RightBlockNum;
+	}
+	else if (0 <= LeftBlockNum) {
+		SMPBasicBlock *LeftBlock = CurrFunc->GetBlockByNum((size_t)LeftBlockNum);
+		list<SMPBasicBlock *>::const_iterator SuccIter = LeftBlock->GetSuccInLoop(LoopNum);
+		if (SuccIter != LeftBlock->GetLastConstSucc()) {
+			SuccBlockNumInsideLoop = (*SuccIter)->GetNumber();
+		}
+	}
+	if (SMP_BLOCKNUM_UNINIT == SuccBlockNumInsideLoop) { // no success yet
+		if (0 <= RightBlockNum) {
+			SMPBasicBlock *RightBlock = CurrFunc->GetBlockByNum((size_t)RightBlockNum);
+			list<SMPBasicBlock *>::const_iterator SuccIter = RightBlock->GetSuccInLoop(LoopNum);
+			if (SuccIter != RightBlock->GetLastConstSucc()) {
+				SuccBlockNumInsideLoop = (*SuccIter)->GetNumber();
+			}
+		}
+	}
+	if (SMP_BLOCKNUM_UNINIT == SuccBlockNumInsideLoop) { // no success yet; recurse into sub-exprs
+		if ((nullptr != this->GetLeftExpr()) && (SMP_BLOCKNUM_UNINIT != (SuccBlockNumInsideLoop = this->GetLeftExpr()->GetSuccNumInLoop(LoopNum)))) {
+			;
+		}
+		else if ((nullptr != this->GetRightExpr()) && (SMP_BLOCKNUM_UNINIT != (SuccBlockNumInsideLoop = this->GetRightExpr()->GetSuccNumInLoop(LoopNum)))) {
+			;
+		}
+	}
 
+	return SuccBlockNumInsideLoop;
+} // end of STARSCondExpr::GetSuccNumInLoop()
 
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index a24f4989..85abc724 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -1558,7 +1558,11 @@ void SMPFunction::SetControlFlowType(STARS_ea_t InstAddr, ControlFlowType JumpTy
 	else { // old entry found; update
 		// We permit a LOOP_EXIT to become a SHORT_CIRCUIT_LOOP_EXIT
 		bool ExitCase = (SHORT_CIRCUIT_LOOP_EXIT == JumpTypeCode) && (LOOP_EXIT == MapIter->second);
-		if (ExitCase) {
+		bool InvertedExitCase = (SHORT_CIRCUIT_INVERTED_LOOP_EXIT == JumpTypeCode) && (INVERTED_LOOP_EXIT == MapIter->second);
+#if 1	// probably need to make SHORT_CIRCUIT_INVERTED_LOOP_EXIT in our caller
+		bool SuspectExitCase = (SHORT_CIRCUIT_LOOP_EXIT == JumpTypeCode) && (INVERTED_LOOP_EXIT == MapIter->second);
+#endif
+		if (ExitCase || InvertedExitCase || SuspectExitCase) {
 			MapIter->second = (unsigned short) JumpTypeCode;
 		}
 		else if (MapIter->second != ((unsigned short) JumpTypeCode)) {
@@ -4464,6 +4468,25 @@ int SMPFunction::GetOutermostLoopNum(const int BlockNum) const {
 	return LoopNum;
 }
 
+// Find innermost loop # whose head block dominates BlockNum but does not contain it
+int SMPFunction::GetInnermostDominatingLoopNum(const int BlockNum) const {
+	int InnerDominatingLoopNum = -1;
+	int MaxRPOHeadBlockNum = -1;
+	for (size_t LoopNum = 0; LoopNum < this->GetNumLoops(); ++LoopNum) {
+		int HeadBlockNum = this->LoopHeadBlockNumbers[LoopNum];
+		if (this->DoesBlockDominateBlock(HeadBlockNum, BlockNum)) {
+			if (!this->IsBlockInLoop(BlockNum, LoopNum)) {
+				if (HeadBlockNum > MaxRPOHeadBlockNum) {
+					MaxRPOHeadBlockNum = HeadBlockNum;
+					InnerDominatingLoopNum = (int)LoopNum;
+				}
+			}
+		}
+	}
+
+	return InnerDominatingLoopNum;
+} // end of SMPFunction::GetInnerMostDominatingLoopNum()
+
 // Given block # and PhiDef STARSOpndType and SSANum, return the Phi iterator or assert.
 set<SMPPhiFunction, LessPhi>::iterator SMPFunction::GetPhiIterForPhiDef(std::size_t BlockNumber, const STARSOpndTypePtr &DefOp, int SSANum) {
 	SMPBasicBlock *DefBlock = this->RPOBlocks.at(BlockNumber);
@@ -6847,8 +6870,8 @@ void SMPFunction::FindLoopHeadsAndTails(SMPBasicBlock *CurrBlock) {
 			}
 			else {
 				CurrBlock->SetLoopDoubleTailBlock();
-				SMP_msg("INFO: LoopDoubleTailBlock: block %d in func %s\n",
-					CurrBlock->GetNumber(), this->GetFuncName());
+				SMP_msg("INFO: LoopDoubleTailBlock: block %d ", CurrBlock->GetNumber());
+				this->DumpFuncNameAndAddr();
 				// Which loop header block is outermost? It dominates the other header.
 				if (this->DoesBlockDominateBlock(SuccBlockNum, CurrBlock->GetLoopHeaderNumber())) {
 					CurrBlock->SetOuterLoopHeaderBlockNumberForDoubleTailBlock(SuccBlockNum);
@@ -6865,18 +6888,18 @@ void SMPFunction::FindLoopHeadsAndTails(SMPBasicBlock *CurrBlock) {
 				//  so we can encounter loop tail blocks multiple times for a loop. We found
 				//  the LoopHeadBlockNum already in our list, so this must be one of these cases.
 				// See if we can provide a better follow node number from the current analysis.
-				assert((0 <= LoopIndex) && (LoopIndex < this->LoopFollowNodes.size()));
+				assert((0 <= LoopIndex) && (LoopIndex < this->LoopExitTargets.size()));
 			}
 			else {
 				this->LoopHeadBlockNumbers.push_back(HeaderBlockNum);
 				set<int> DummySet;
 				DummySet.insert(FollowBlockNum);
-				this->LoopFollowNodes.push_back(DummySet);
+				this->LoopExitTargets.push_back(DummySet);
 				map<int, STARSBitSet> DummyMap;
-				this->LoopFollowNodesReachabilitySets.push_back(DummyMap);
+				this->LoopExitTargetsReachabilitySets.push_back(DummyMap);
 				++this->LoopCount;
 				assert(this->LoopHeadBlockNumbers.size() == this->LoopCount);
-				assert(this->LoopFollowNodesReachabilitySets.size() == this->LoopCount);
+				assert(this->LoopExitTargetsReachabilitySets.size() == this->LoopCount);
 				// If this is a double tail block, we need to arrange Loop N == inner, loop N-1 == outer.
 				if (CurrBlock->IsDoubleLoopTailBlock()) {
 					OuterLoopHeadBlockNum = CurrBlock->GetOuterLoopHeaderNumberForDoubleTailBlock();
@@ -7253,13 +7276,15 @@ SMPFunction::ClassifyLoop(size_t LoopNumber, int HeaderExitFollowNum, int TailEx
 			if (TailExitFollowNum != HeaderExitFollowNum) {
 				if (this->HasGoodLoopFollowBlocks || VerboseOutput) {
 					if (!this->PrintedSPARKUnstructuredMsg || VerboseOutput) {
-						SMP_msg("ERROR: SPARK: Unstructured due to conflicting head and tail loop follow block nums for loop %d : %d and %d ",
+						SMP_msg("INFO: SPARK: Might be unstructured due to conflicting head and tail loop follow block nums for loop %d : %d and %d ",
 							LoopNumber, HeaderExitFollowNum, TailExitFollowNum);
 						this->DumpFuncNameAndAddr();
-						this->PrintedSPARKUnstructuredMsg = true;
 					}
 				}
+#if 0
+				this->PrintedSPARKUnstructuredMsg = true;
 				this->HasGoodLoopFollowBlocks = false; // inconsistent head and tail follow nodes, e.g. multi-level loop exit
+#endif
 			}
 		}
 		else {
@@ -7288,14 +7313,24 @@ SMPFunction::ClassifyLoop(size_t LoopNumber, int HeaderExitFollowNum, int TailEx
 // return true if block can exit the loop.
 bool SMPFunction::DoesBlockExitLoop(std::size_t LoopNumber, SMPBasicBlock *LoopBlock, int &FollowBlockNum) {
 	bool FoundExitSuccessor = false;
+	int LoopBlockNum = LoopBlock->GetNumber();
 
 	for (list<SMPBasicBlock *>::iterator SuccIter = LoopBlock->GetFirstSucc(); SuccIter != LoopBlock->GetLastSucc(); ++SuccIter) {
 		SMPBasicBlock *SuccBlock = (*SuccIter);
-		int BlockNum = SuccBlock->GetNumber();
-		if (!(this->IsBlockInLoop(BlockNum, LoopNumber))) {
+		int SuccBlockNum = SuccBlock->GetNumber();
+		if (!(this->IsBlockInLoop(SuccBlockNum, LoopNumber))) {
 			if (!LoopBlock->IsDoubleLoopTailBlock()) { // normal case
 				FoundExitSuccessor = true;
-				FollowBlockNum = BlockNum;
+				FollowBlockNum = SuccBlockNum;
+				bool MultiLoopBreak = this->DetectMultiLevelLoopBreak(LoopBlockNum, SuccBlockNum);
+				if (MultiLoopBreak) {
+					if (!this->PrintedSPARKUnstructuredMsg) {
+						SMP_msg("ERROR: SPARK: Unstructured due to multi-level loop break in Loop %zu at block %d ", LoopNumber, LoopBlockNum);
+						this->DumpFuncNameAndAddr();
+						this->PrintedSPARKUnstructuredMsg = true;
+					}
+					this->HasStructuredCFG = false; // multi-level loop break
+				}
 				break;
 			}
 			else { // Double tail block
@@ -7309,25 +7344,66 @@ bool SMPFunction::DoesBlockExitLoop(std::size_t LoopNumber, SMPBasicBlock *LoopB
 	return FoundExitSuccessor;
 } // end of SMPFunction::DoesBlockExitLoop()
 
-// Populate entry in LoopFollowNodesReachabilitySets
+// Is ExitTargetBlockNum more than 1 loop nesting level away from LoopBlockNum?
+bool SMPFunction::DetectMultiLevelLoopBreak(const int LoopBlockNum, const int ExitTargetBlockNum) const {
+	assert(0 <= LoopBlockNum);
+	assert(0 <= ExitTargetBlockNum);
+	assert((size_t)LoopBlockNum < this->FuncLoopsByBlock.size());
+	assert((size_t)ExitTargetBlockNum < this->FuncLoopsByBlock.size());
+	bool MultiLevelBreak = false;
+	STARSBitSet CommonLoops = STARSBitSetIntersection(this->FuncLoopsByBlock[(size_t)LoopBlockNum], this->FuncLoopsByBlock[(size_t)ExitTargetBlockNum]);
+	size_t LoopNestingLevel = this->FuncLoopsByBlock[(size_t)LoopBlockNum].CountSetBits();
+	size_t ExitTargetNestingLevel = this->FuncLoopsByBlock[(size_t)ExitTargetBlockNum].CountSetBits();
+	if (LoopNestingLevel != (1 + ExitTargetNestingLevel)) {
+		MultiLevelBreak = true;
+	}
+	else if (CommonLoops.CountSetBits() != ExitTargetNestingLevel) {
+		// Some sort of spaghetti code; passing the first test should indicate
+		//  only one difference between the two loop nests, with the common loop bits
+		//  being identical to the ExitTarget loop bits.
+		MultiLevelBreak = true;
+	}
+
+	return MultiLevelBreak;
+} // end of SMPFunction::DetectMultiLevelLoopBreak()
+
+// Populate entries for LoopNum in LoopExitTargetsReachabilitySets and MultiLoopExitTargetsConvergenceMap
 void SMPFunction::ComputeLoopFollowNodesReachability(const std::size_t LoopNum) {
 	// Without following back edges, record which blocks can be reached from 
 	//  each block that is the target of a loop exit (which are found in LoopFollowNodes[LoopNum]).
 	assert(LoopNum < this->GetNumLoops());
-	assert(LoopNum < this->LoopFollowNodes.size());
-	for (int FollowNodeNum : this->LoopFollowNodes[LoopNum]) {
+	assert(LoopNum < this->LoopExitTargets.size());
+	int LoopHeadBlockNum = this->LoopHeadBlockNumbers[LoopNum];
+	for (int FollowNodeNum : this->LoopExitTargets[LoopNum]) {
 		STARSBitSet Reachable;
 		Reachable.AllocateBits(this->GetNumBlocks());
-		this->MarkReachableBlocks(FollowNodeNum, Reachable);
+		this->MarkReachableBlocks(FollowNodeNum, LoopNum, LoopHeadBlockNum, Reachable);
 		pair<int, STARSBitSet> MapItem(FollowNodeNum, Reachable);
-		this->LoopFollowNodesReachabilitySets[LoopNum].insert(MapItem);
+		this->LoopExitTargetsReachabilitySets[LoopNum].insert(MapItem);
+	}
+
+	// Find out where the multiple follow nodes converge, if they do. If they all hit separate return blocks,
+	//  we use the code of -2 to signify it.
+	if (this->MultiLoopExitTargetsConvergenceMap[LoopNum].empty()) {
+		// Must have hit return blocks.
+		this->MultiLoopExitTargetsConvergenceMap[LoopNum].insert(SMP_BLOCKNUM_COMMON_RETURN);
+	}
+	else if (1 != this->MultiLoopExitTargetsConvergenceMap[LoopNum].size()) {
+		if (!this->PrintedSPARKUnstructuredMsg) {
+			SMP_msg("ERROR: SPARK: Unstructured due to no convergence of multiple follow nodes from loop %zu ", LoopNum);
+			this->DumpFuncNameAndAddr();
+			this->PrintedSPARKUnstructuredMsg = true;
+		}
+		this->HasStructuredCFG = false; // multi-exit loop has no single convergence point of follow nodes.
+		// TODO: If the multiple termination blocks all loop back to the same outer loop head block, this
+		//  is structured code and can be translated. !!!!****!!!!
 	}
 
 	return;
 } // end of SMPFunction::ComputeLoopFollowNodesReachability()
 
-// Set bits of current BlockNum and its descendants in CFG
-void SMPFunction::MarkReachableBlocks(const int BlockNum, STARSBitSet &ReachableSet) {
+// Set bits of current BlockNum and its descendants in CFG that are dominated by LoopHeadBlockNum
+void SMPFunction::MarkReachableBlocks(const int BlockNum, const size_t LoopNum, const int LoopHeadBlockNum, STARSBitSet &ReachableSet) {
 	if (!ReachableSet.GetBit((size_t)BlockNum)) { // avoid looping
 		ReachableSet.SetBit((size_t)BlockNum); // Initialize to itself being reachable
 		SMPBasicBlock *CurrBlock = this->GetBlockByNum((size_t)BlockNum);
@@ -7336,13 +7412,106 @@ void SMPFunction::MarkReachableBlocks(const int BlockNum, STARSBitSet &Reachable
 			int SuccBlockNum = (*SuccIter)->GetNumber();
 			// Weed out back edges
 			if (!this->DoesBlockDominateBlock(SuccBlockNum, BlockNum)) {
-				this->MarkReachableBlocks(SuccBlockNum, ReachableSet);
+				// It is OK to exit an inner loop into multiple blocks that are part of an enclosing
+				//  outer loop, but as we trace downwards from each such block, we cannot exit the outer
+				//  loop. In the decompilation process, we will only translate blocks within the outer loop
+				//  that were reachable from inner loop exit targets. E.g.:
+				//  
+				//  loop  -- loop 1
+				//    ...
+				//    loop  -- loop 0
+				//      ...
+				//      exit when (STARSExitLoop0ToBlock7);
+				//      ...
+				//      exit when (STARSExitLoop0ToBlock9);
+				//    end loop;  -- end loop 0
+				//    if (STARSExitLoop0ToBlock7) then
+				//       [code for block 7]
+				//    end if;
+				//    if (STARSExitLoop0ToBlock9) then
+				//       [code for block 9]
+				//    end if;
+				//  end loop; -- end loop 1
+				//  [code for block 10]
+				//  ...
+				//  Following down from block 9, we might take a LOOP_EXIT or INVERTED_LOOP_EXIT
+				//   and reach block 10. But we don't want to follow that path while translating, because
+				//   the inner loop is lifted into a separate loop procedure and only a call to it exists
+				//   in the outer loop:
+				//
+				//  loop  -- loop 1, outer loop
+				//    ...
+				//    call innerloop0;
+				//    if (STARSExitLoop0ToBlock7) then
+				//       [code for block 7]
+				//    end if;
+				//    if (STARSExitLoop0ToBlock9) then
+				//       [code for block 9]
+				//    end if;
+				//  end loop; -- end loop 1
+				//
+				// This code for loop 1 is a separate procedure, called from the main body of the 
+				//  enclosing procedure:
+				//
+				// procedure foo(argument list)
+				//   ...
+				//   call outerloop1;
+				//   [code for block 10]
+				//  ...
+				//
+				// We see that code that logically follows the "end loop;" for the outer loop 1
+				//  is placed after the "call outerloop1;" line. Likewise, the multiple exit targets
+				//  for innerloop0 get placed after the "call innerloop0;" line. So the loops themselves
+				//  are separate procedures, and the calls to them do not occur in the same procedures;
+				//  the call to outerloop1 is from foo() while the call to innerloop0 is from outerloop1.
+				// Whether there is a single exit target or multiple exit targets, their SPARK Ada translation
+				//  follows the call to their loop. We see that [code for block 10] does not end up in the
+				//  same procedure as block 9, so the reachability of block 10 from block 9 is not relevant to
+				//  our translation. Therefore we end our reachability marking when we are about to exit another
+				//  loop level. Such a multi-level trace can be detected by the existing method that detects
+				//  multi-level loop breaks, which are unstructured and need to be structured separately.
+				if (!this->DetectMultiLevelLoopBreak(LoopHeadBlockNum, SuccBlockNum)) {
+					if (this->DoesBlockDominateBlock(LoopHeadBlockNum, SuccBlockNum)) {
+						this->MarkReachableBlocks(SuccBlockNum, LoopNum, LoopHeadBlockNum, ReachableSet);
+					}
+					else {
+						// Terminating because we are escaping the region dominated by the loop head block.
+						//  This SuccBlockNum is a candidate for the true loop follow block, where we will resume
+						//  decompilation after we have processed all of the targets of loop exits and their
+						//  reachable blocks.
+						// NOTE: If the ExitTargetBlock (BlockNum) is not dominated by LoopHeadBlockNum,
+						//  then we should not be looking at its successors in the first place.
+						if (this->DoesBlockDominateBlock(LoopHeadBlockNum, BlockNum)) {
+							size_t LoopNum = this->GetLoopNumFromHeaderBlockNum(LoopHeadBlockNum);
+							this->MultiLoopExitTargetsConvergenceMap[LoopNum].insert(SuccBlockNum);
+						}
+					}
+				}
 			}
 		}
 	}
 
 	return;
-} // end if 
+} // end of SMPFunction::MarkReachableBlocks()
+
+// How many of the multiple exit targets from LoopNum reach BlockNum?
+uint32_t SMPFunction::GetReachableSourcesCount(const size_t BlockNum, const size_t LoopNum) const {
+	assert(LoopNum < this->GetNumLoops());
+	assert(BlockNum < this->GetNumBlocks());
+
+	uint32_t ReachableSourcesCounter = 0;
+
+	if (this->LoopExitTargets[LoopNum].size() > 1) {
+		assert(!this->LoopExitTargetsReachabilitySets[LoopNum].empty());
+		for (pair<int, STARSBitSet> MapItem : this->LoopExitTargetsReachabilitySets[LoopNum]) {
+			if (MapItem.second.GetBit(BlockNum)) {
+				++ReachableSourcesCounter;
+			}
+		}
+	}
+
+	return ReachableSourcesCounter;
+} // end of SMPFunction::GetReachableSourcesCount()
 
 // Collect a set of loop-variant DEFs with the inst IDs of the DEFs.
 void SMPFunction::DetectLoopInvariantDEFs(void) {
@@ -11125,7 +11294,9 @@ void SMPFunction::CoalesceShadowBlocks(int LeftBlockNum, int RightBlockNum, bool
 	int InnerMostLoopNum = InsideLoop ? this->GetInnermostLoopNum(LeftBlockNum) : -1;
 	// Are both successor blocks in the same innermost loop? If not, this is a loop exit,
 	//  Note that we could enter into a still more innermost loop as long as we don't exit the current one.
-	bool LoopExitCase =  InsideLoop && (!(this->IsBlockInLoop(NewFTNum, (size_t) InnerMostLoopNum) && this->IsBlockInLoop(NewNFTNum, (size_t) InnerMostLoopNum)));
+	bool FTExitsLoop = (!(this->IsBlockInLoop(NewFTNum, (size_t)InnerMostLoopNum)));
+	bool NFTExitsLoop = (!(this->IsBlockInLoop(NewNFTNum, (size_t)InnerMostLoopNum)));
+	bool LoopExitCase =  InsideLoop && (FTExitsLoop || NFTExitsLoop);
 	STARSCFGBlock *LeftCFGBlock = this->ShadowCFGBlocks[LeftBlockNum];
 	STARSCFGBlock *RightCFGBlock = this->ShadowCFGBlocks[RightBlockNum];
 
@@ -11158,6 +11329,7 @@ void SMPFunction::CoalesceShadowBlocks(int LeftBlockNum, int RightBlockNum, bool
 
 	// Mark RightBlockNum as coalesced.
 	RightCFGBlock->SetCoalesced();
+	RightCFGBlock->SetCoalescedBlockNum(LeftBlockNum);
 
 	// Mark the conditional branches at the end of LeftBlockNum and RightBlockNum as short circuit branches.
 	SMPBasicBlock *LeftBlock = this->RPOBlocks[LeftBlockNum];
@@ -11165,8 +11337,15 @@ void SMPFunction::CoalesceShadowBlocks(int LeftBlockNum, int RightBlockNum, bool
 	STARS_ea_t LeftLastAddr = LeftBlock->GetLastAddr();
 	STARS_ea_t RightLastAddr = RightBlock->GetLastAddr();
 	if (LoopExitCase) {
-		this->SetControlFlowType(LeftLastAddr, SHORT_CIRCUIT_LOOP_EXIT);
-		this->SetControlFlowType(RightLastAddr, SHORT_CIRCUIT_LOOP_EXIT);
+		if (NFTExitsLoop) {
+			this->SetControlFlowType(LeftLastAddr, SHORT_CIRCUIT_LOOP_EXIT);
+			this->SetControlFlowType(RightLastAddr, SHORT_CIRCUIT_LOOP_EXIT);
+		}
+		else {
+			assert(FTExitsLoop);
+			this->SetControlFlowType(LeftLastAddr, SHORT_CIRCUIT_INVERTED_LOOP_EXIT);
+			this->SetControlFlowType(RightLastAddr, SHORT_CIRCUIT_INVERTED_LOOP_EXIT);
+		}
 	}
 	else {
 		this->SetControlFlowType(LeftLastAddr, SHORT_CIRCUIT_BRANCH);
@@ -11381,7 +11560,7 @@ bool SMPFunction::AnalyzeCompoundConditionalStatements(void) {
 				//  as a part of the same compound conditional. These are shown in Figure 6-32 of
 				//  Cristina Cifuentes' Ph.D. dissertation on decompilation. With x being the condition
 				//  at the end of the first block, and y the condition at the end of the second block,
-				//  and "x" below meaning "take branch from block with condition x" and ditto for "y",
+				//  and "x" below meaning "take branch from block when condition x" and ditto for "y",
 				//  these four CFG patterns match the short-circuit evaluation of:
 				//  1. x AND y  (i.e. taking the branch from x to y and then also from y leads to a dest. block,
 				//               falling through from either one leads to a common second dest. block).
@@ -11409,7 +11588,7 @@ bool SMPFunction::AnalyzeCompoundConditionalStatements(void) {
 				//  2. NFT(1) = NFT(FT(1))  [implies FT(1) == 2]
 				//  3. FT(1) = NFT(NFT(1))  [implies NFT(1) == 2]
 				//  4. NFT(1) = FT(FT(1))   [implies FT(1) == 2]
-				// The resulting CFG and be structured for the four cases as follows, using Ada short-circuit operators:
+				// The resulting CFG can be structured for the four cases as follows, using Ada short-circuit operators:
 				// 1. if x and then y then
 				//       NFT(NFT(1))
 				//    else
@@ -11494,7 +11673,7 @@ bool SMPFunction::AnalyzeCompoundConditionalStatements(void) {
 			SMPBasicBlock *OrigBlock = this->GetBlockByNum((size_t) OrigBlockNum);
 			STARS_ea_t LastAddr = OrigBlock->GetLastAddr();
 			ControlFlowType LastCFType = this->GetControlFlowType(LastAddr);
-			if (SHORT_CIRCUIT_BRANCH == LastCFType) { // not SHORT_CIRCUIT_LOOP_EXIT
+			if (!IsLoopExitFlow(LastCFType)) { // not SHORT_CIRCUIT_LOOP_EXIT or SHORT_CIRCUIT_INVERTED_LOOP_EXIT
 				int FollowBlockNum = this->FindConditionalFollowNode((int) BlockIndex);
 				if (SMP_BLOCKNUM_UNINIT == FollowBlockNum) {
 					if (!this->PrintedSPARKUnstructuredMsg) {
@@ -11894,18 +12073,20 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
 	//   return or loop-back and does not converge into a follow node.
 
 	STARS_ea_t HeadLastAddr = HeadBlock->GetLastAddr();
+	bool HeadBlockIsInALoop = this->IsBlockInAnyLoop(HeadBlockNum);
 	ControlFlowType LastCFType = this->GetControlFlowType(HeadLastAddr);
-	bool ShortCircuit = ((LastCFType == SHORT_CIRCUIT_BRANCH) || (LastCFType == SHORT_CIRCUIT_LOOP_EXIT));
+	bool ShortCircuit = (IsShortCircuitFlow(LastCFType));
 
 	// 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);
+	for (int CurrBlockNum : this->DomTree[HeadBlockNum].second) {
 		if (2 <= this->RPOBlocks[(size_t) CurrBlockNum]->GetNumPredsMinusBackEdges()) { // candidate
 			if (!(ShortCircuit && this->ShadowCFGBlocks[(size_t)CurrBlockNum]->IsCoalesced())) {
-				FollowBlockNum = CurrBlockNum;
-				break;
+				// Follow node needs to be at the same loop nesting level as the head block, else we
+				//  could just be finding the convergence of two paths inside some unrelated loop.
+				if (this->AreBlocksInSameLoops(HeadBlockNum, CurrBlockNum)) {
+					FollowBlockNum = CurrBlockNum;
+					break;
+				}
 			}
 		}
 	}
@@ -11929,7 +12110,7 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
 	//  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)) {
+	if (HeadBlockIsInALoop) {
 		int InnerMostLoopNum = this->GetInnermostLoopNum(HeadBlockNum);
 		assert(0 <= InnerMostLoopNum);
 		int InnerMostFollowBlockNum = SMP_BLOCKNUM_UNINIT;
@@ -12030,7 +12211,7 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
 
 	// A similar case to the above is when both branches of an if-then-else flow (via back edges)
 	//   into a loop header block for a loop that contains both branches.
-	if ((SMP_BLOCKNUM_UNINIT == FollowBlockNum) && (0 < this->LoopCount)) {
+	if ((SMP_BLOCKNUM_UNINIT == FollowBlockNum) && HeadBlockIsInALoop) {
 		// See if we can find two blocks, each dominated by HeadBlockNum,
 		//  each being loop tail blocks, with the same loop header block
 		//  as a successor block, with the loop header block dominating HeadBlockNum.
@@ -12172,7 +12353,7 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
 				if (ThenBlock->IsLoopHeaderBlock()) {
 					int ThenLoopNum = this->GetLoopNumFromHeaderBlockNum(ThenBlockNum);
 					assert(0 <= ThenLoopNum);
-					assert(((size_t) ThenLoopNum) < this->LoopFollowNodes.size());
+					assert(((size_t) ThenLoopNum) < this->LoopExitTargets.size());
 					bool MultiExitThenLoop = this->GetLoopFollowBlockNum((size_t)ThenLoopNum, ThenFollowBlockNum);
 					if (MultiExitThenLoop) {
 						ThenFollowBlockNum = SMP_BLOCKNUM_UNINIT; // error
@@ -12187,7 +12368,7 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
 				if (ElseBlock->IsLoopHeaderBlock()) {
 					int ElseLoopNum = this->GetLoopNumFromHeaderBlockNum(ElseBlockNum);
 					assert(0 <= ElseLoopNum);
-					assert(((size_t) ElseLoopNum) < this->LoopFollowNodes.size());
+					assert(((size_t) ElseLoopNum) < this->LoopExitTargets.size());
 					bool MultiExitElseLoop = this->GetLoopFollowBlockNum((size_t)ElseLoopNum, ElseFollowBlockNum);
 					if (MultiExitElseLoop) {
 						ElseFollowBlockNum = SMP_BLOCKNUM_UNINIT; // error
@@ -12258,6 +12439,7 @@ int SMPFunction::TrackConditionalBranchTerminus(int BranchHeadBlockNum, int Curr
 	int TerminusBlockNum = SMP_BLOCKNUM_COMMON_RETURN;
 	SMPBasicBlock *CurrBlock = this->GetBlockByNum((size_t) CurrBlockNum);
 	assert(CurrBlock != nullptr);
+	bool BranchHeadIsInALoop = this->IsBlockInAnyLoop(BranchHeadBlockNum);
 	if (CurrBlock->HasReturn() || CurrBlock->HasNonReturningCall()) {
 		TerminusBlockNum = SMP_BLOCKNUM_COMMON_RETURN;
 	}
@@ -12281,7 +12463,7 @@ int SMPFunction::TrackConditionalBranchTerminus(int BranchHeadBlockNum, int Curr
 				}
 			}
 		}
-		else if (LastCFType == INVERTED_LOOP_EXIT) {
+		else if (IsInvertedLoopExitFlow(LastCFType) && this->AreBlocksInSameLoops(BranchHeadBlockNum, CurrBlockNum)) {
 			// COND_BRANCH taken would remain in the loop; fall-through will exit the loop.
 #if 0	// Could do INVERTED_LOOP_EXIT by falling out of any block in the loop, not just the header block.
 			assert(CurrBlock->IsLoopHeaderBlock());
@@ -12298,7 +12480,9 @@ int SMPFunction::TrackConditionalBranchTerminus(int BranchHeadBlockNum, int Curr
 		else { // add all successors to the work list
 			for (list<SMPBasicBlock *>::const_iterator SuccIter = CurrBlock->GetFirstConstSucc(); SuccIter != CurrBlock->GetLastConstSucc(); ++SuccIter) {
 				int SuccBlockNum = (*SuccIter)->GetNumber();
-				WorkListBlockNums.push_back(SuccBlockNum);
+				if (!BlocksSeen.GetBit((size_t)SuccBlockNum)) { // Don't go backwards
+					WorkListBlockNums.push_back(SuccBlockNum);
+				}
 			}
 		}
 #define STARS_COND_BRANCH_WORKLIST_LIMIT 200
@@ -12342,7 +12526,7 @@ int SMPFunction::TrackConditionalBranchTerminus(int BranchHeadBlockNum, int Curr
 			}
 
 			BlocksSeen.SetBit((size_t) SuccBlockNum);
-			bool OutsideTheLoop = (!this->AreBlocksInSameLoops(BranchHeadBlockNum, SuccBlockNum));
+			bool OutsideTheLoop = BranchHeadIsInALoop && (!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.
@@ -14352,7 +14536,7 @@ bool SMPFunction::IsBlockInAnyLoop(int BlockNum) const {
 
 // Is block (with block # BlockNum) inside loop # LoopNum?
 bool SMPFunction::IsBlockInLoop(int BlockNum, std::size_t LoopNum) const {
-	if (0 == this->LoopCount)
+	if ((0 == this->LoopCount) || (0 > BlockNum))
 		return false;
 	assert(((size_t) BlockNum) < this->GetNumBlocks());
 	return ((LoopNum < this->LoopCount) && (this->FuncLoopsByBlock.at((std::size_t) BlockNum).GetBit(LoopNum)));
@@ -16837,6 +17021,7 @@ void SMPFunction::UpdateLoopFollowBlockNum(int LoopHeadBlockNum, int FollowBlock
 	int OldFollowNum = SMP_BLOCKNUM_UNINIT;
 	bool MultiExitLoop = this->GetLoopFollowBlockNum((size_t)LoopNum, OldFollowNum);
 	bool VerboseOutput = global_stars_interface->VerboseSPARKMode();
+	bool ConvergenceComputed = (MultiExitLoop && (this->MultiLoopExitTargetsConvergenceMap.find((int)LoopNum) != this->MultiLoopExitTargetsConvergenceMap.cend()));
 
 	// 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
@@ -16854,23 +17039,39 @@ void SMPFunction::UpdateLoopFollowBlockNum(int LoopHeadBlockNum, int FollowBlock
 		this->DumpDotCFG();
 		return;
 	}
+	bool MultiLoopBreak = this->DetectMultiLevelLoopBreak(LoopHeadBlockNum, FollowBlockNum);
+	if (MultiLoopBreak) {
+		if (!this->PrintedSPARKUnstructuredMsg) {
+			SMP_msg("ERROR: SPARK: Unstructured due to multi-level loop break in Loop %zu to block %d ", LoopNum, FollowBlockNum);
+			this->DumpFuncNameAndAddr();
+		}
+		this->HasStructuredCFG = false; // multi-level loop break
+		this->PrintedSPARKUnstructuredMsg = true;
+	}
 
 	if (OldFollowNum == SMP_BLOCKNUM_UNINIT) {
-		assert(1 == this->LoopFollowNodes[LoopNum].size());
-		this->LoopFollowNodes[LoopNum].clear();
-		this->LoopFollowNodes[LoopNum].insert(FollowBlockNum);
+		bool EarlyPhaseMultiTarget = (MultiExitLoop && !ConvergenceComputed);
+		assert((1 == this->LoopExitTargets[LoopNum].size()) || EarlyPhaseMultiTarget);
+		if (!EarlyPhaseMultiTarget) {
+			// If convergence has not been computed yet, we could still be processing loops
+			//  in ClassifyLoop() and we don't want to clear the exit targets we have found.
+			this->LoopExitTargets[LoopNum].clear();
+		}
+		this->LoopExitTargets[LoopNum].insert(FollowBlockNum);
 	}
 	else if (OldFollowNum != FollowBlockNum) {
 		if (SMP_BLOCKNUM_UNINIT == FollowBlockNum) {
 			if (this->HasGoodLoopFollowBlocks || VerboseOutput) {
 				if (!this->PrintedSPARKUnstructuredMsg || VerboseOutput) {
-					SMP_msg("ERROR: SPARK: Unstructured due to conflicting loop follow block nums for loop %d : %d and %d ",
+					SMP_msg("INFO: SPARK: Might be unstructured due to conflicting loop follow block nums for loop %d : %d and %d ",
 						LoopNum, OldFollowNum, FollowBlockNum);
 					this->DumpFuncNameAndAddr();
-					this->PrintedSPARKUnstructuredMsg = true;
 				}
 			}
+#if 0
+			this->PrintedSPARKUnstructuredMsg = true;
 			this->HasGoodLoopFollowBlocks = false; // conflicting loop follow block nums
+#endif
 		}
 		else {
 			// Conflicting follow block numbers
@@ -16890,25 +17091,33 @@ void SMPFunction::UpdateLoopFollowBlockNum(int LoopHeadBlockNum, int FollowBlock
 					SMP_msg("INFO: Replaced DirectJumpOnly loop follow block %d with %d for head block %d in %s\n", OldFollowNum,
 						FollowBlockNum, LoopHeadBlockNum, this->GetFuncName());
 					success = true;
+					// Remove jump-only block num from exit targets set so that we don't create a
+					//  false appearance of a multi-exit-target loop.
+					set<int>::const_iterator OldExitTargetIter = this->LoopExitTargets[LoopNum].find(OldFollowNum);
+					if (OldExitTargetIter != this->LoopExitTargets[LoopNum].cend()) {
+						(void) this->LoopExitTargets[LoopNum].erase(OldExitTargetIter);
+					}
 				}
 			}
 			if (!success) {
 				if (this->HasGoodLoopFollowBlocks || VerboseOutput) {
 					if (!this->PrintedSPARKUnstructuredMsg) {
-						SMP_msg("ERROR: SPARK: Unstructured due to conflicting loop follow block nums for loop %d : %d and %d ",
+						SMP_msg("INFO: SPARK: Might be unstructured due to conflicting loop follow block nums for loop %d : %d and %d ",
 							LoopNum, OldFollowNum, FollowBlockNum);
 						this->DumpFuncNameAndAddr();
-						this->PrintedSPARKUnstructuredMsg = true;
 					}
 				}
 				if (this->HasGoodLoopFollowBlocks) {
+#if 0
+					this->PrintedSPARKUnstructuredMsg = true;
 					this->HasGoodLoopFollowBlocks = false; // Conflicting loop follow blocks
+#endif
 					if (VerboseOutput)
 						this->Dump();
 					this->DumpDotCFG();
 				}
 			}
-			this->LoopFollowNodes[LoopNum].insert(FollowBlockNum);
+			this->LoopExitTargets[LoopNum].insert(FollowBlockNum);
 		}
 	}
 	return;
@@ -17298,15 +17507,17 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 	} // end if LoopCount > 0 and structured CFG
 
 	if (global_STARS_program->ShouldSTARSTranslateToSPARKAda()) {
+		for (size_t LoopNum = 0; LoopNum < this->GetNumLoops(); ++LoopNum) {
+			if (1 < this->LoopExitTargets[LoopNum].size()) {
+				set<int> DummySet;
+				this->MultiLoopExitTargetsConvergenceMap[LoopNum] = DummySet;
+				this->ComputeLoopFollowNodesReachability(LoopNum);
+			}
+		}
 		if (!this->HasGoodLoopFollowBlocks) {
 			this->HasStructuredCFG = false; // Bad loop follow blocks
-			SMP_msg("ERROR: SPARK: Function %s declared unstructured because of bad loop follow blocks.\n",
+			SMP_msg("ERROR: SPARK: Function %s is unstructured due to bad loop follow blocks.\n",
 				this->GetFuncName());
-			for (size_t LoopNum = 0; LoopNum < this->GetNumLoops(); ++LoopNum) {
-				if (1 < this->LoopFollowNodes[LoopNum].size()) {
-					this->ComputeLoopFollowNodesReachability(LoopNum);
-				}
-			}
 		}
 
 		if (!StartupFunc) {
@@ -19018,19 +19229,32 @@ void SMPFunction::Dump(void) {
 					SMP_msg(" %zu", BlockNum);
 				}
 			}
-			if (!this->LoopFollowNodes.empty()) {
+			if (!this->LoopExitTargets.empty()) {
 				int FollowBlockNum = SMP_BLOCKNUM_UNINIT;
-				bool MultiExitLoop = (1 < this->LoopFollowNodes[LoopNum].size());
+				bool MultiExitLoop = (1 < this->LoopExitTargets[LoopNum].size());
 				if (!MultiExitLoop) {
-					SMP_msg(" Follow block number: %d", *(this->LoopFollowNodes[LoopNum].cbegin()));
+					SMP_msg(" Follow block number: %d", *(this->LoopExitTargets[LoopNum].cbegin()));
 				}
 				else {
-					SMP_msg(" Follow block numbers: \n");
-					for (int FollowBlockNum : this->LoopFollowNodes[LoopNum]) {
+					SMP_msg(" Exit target block numbers: \n");
+					for (int FollowBlockNum : this->LoopExitTargets[LoopNum]) {
 						SMP_msg("%d ", FollowBlockNum);
 						SMP_msg("Reachable descendants: ");
-						const STARSBitSet &CurrBitSet = this->LoopFollowNodesReachabilitySets[LoopNum][FollowBlockNum];
-						CurrBitSet.DumpBitsSet();
+						if (!this->LoopExitTargetsReachabilitySets[LoopNum].empty()) {
+							map<int, STARSBitSet>::const_iterator MapIter = this->LoopExitTargetsReachabilitySets[LoopNum].find(FollowBlockNum);
+							if (MapIter != this->LoopExitTargetsReachabilitySets[LoopNum].cend()) {
+								const STARSBitSet &CurrBitSet = this->LoopExitTargetsReachabilitySets[LoopNum][FollowBlockNum];
+								CurrBitSet.DumpBitsSet();
+							}
+						}
+						SMP_msg("\n");
+					}
+					map<int, set<int> >::const_iterator MapIter = this->MultiLoopExitTargetsConvergenceMap.find((int)LoopNum);
+					if (MapIter != this->MultiLoopExitTargetsConvergenceMap.cend()) {
+						SMP_msg(" Exit target convergence block numbers: ");
+						for (int ConvergenceBlockNum : MapIter->second) {
+							SMP_msg("%d ", ConvergenceBlockNum);
+						}
 						SMP_msg("\n");
 					}
 				}
@@ -19077,7 +19301,7 @@ void SMPFunction::Dump(void) {
 		for (size_t BlockIndex = 0; BlockIndex < this->ShadowCFGBlocks.size(); ++BlockIndex) {
 			STARSCFGBlock *CFGBlock = this->ShadowCFGBlocks[BlockIndex];
 			if (CFGBlock->IsCoalesced()) {
-				SMP_msg("SPARK: Block %d has been coalesced into CFG block %zu.\n", CFGBlock->GetOriginalBlockNum(), BlockIndex);
+				SMP_msg("SPARK: Block %d has been coalesced into CFG block %zu.\n", BlockIndex, CFGBlock->GetCoalescedBlockNum());
 			}
 		}
 	}
@@ -21903,6 +22127,22 @@ string SMPFunction::GetFuncSPARKSuffixString(void) const {
 	return FuncAddrString;
 }
 
+// Generate loop exit flow-tracking boolean name, e.g. STARSExitLoop2ToBlock5
+string SMPFunction::GenerateSPARKLoopExitBooleanName(const size_t LoopNum, const int ExitTargetBlockNum) const {
+	assert(0 < ExitTargetBlockNum);
+	assert(LoopNum < this->GetNumLoops());
+	char LoopChars[8], TargetChars[8];
+	string BoolName("STARSExitLoop");
+	SMP_snprintf(LoopChars, 7, "%zu", LoopNum);
+	SMP_snprintf(TargetChars, 7, "%d", ExitTargetBlockNum);
+	BoolName += string(LoopChars);
+	BoolName += "ToBlock";
+	BoolName += string(TargetChars);
+
+	return BoolName;
+} // end of SMPFunction::GenerateLoopExitBooleanName()
+
+
 // Save incoming args as locals to preserve their values
 void SMPFunction::EmitSPARKSavedArgs(FILE *BodyFile) const {
 	if ((0 < this->LoopCount) || (!this->InArgsUsedInMemWrites[0].empty())) {
@@ -22577,8 +22817,8 @@ void SMPFunction::EmitSPARKLoopProcGlobals(FILE *BodyFile, FILE *HeaderFile, boo
 	return;
 } // end of SMPFunction::EmitSPARKLoopProcGlobals()
 
-// 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) {
+// recursive descent translation to SPARK Ada starting with CurrBlock, stop before Follow Block or limit to blocks with the same LoopExitTargets reachability.
+void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FILE *SPARKBodyFile, bool ReadytoEmitSwitchDefault, bool LoopToProc, const uint32_t ReachableSourcesCount) {
 	PrintSPARKIndentTabs(SPARKBodyFile);
 	SMP_fprintf(SPARKBodyFile, "-- Basic block %d;\n", CurrBlockNum);
 	if (LoopToProc && (!this->IsSPARKLoopInTranslationStack())) {
@@ -22602,6 +22842,14 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FIL
 
 	// Recursive descent based on the kind of block CurrBlock is.
 	while ((CurrBlockNum != FollowBlockNum) && (CurrBlockNum >= 0)) {
+		if (0 < ReachableSourcesCount) {
+			int InnerLoopNum = this->GetInnermostDominatingLoopNum(CurrBlockNum);
+			if (0 <= InnerLoopNum) {
+				uint32_t CurrReachableSourcesCount = this->GetReachableSourcesCount((size_t)CurrBlockNum, InnerLoopNum);
+				if (CurrReachableSourcesCount != ReachableSourcesCount) // cannot follow beyond scope of current guard Boolean
+					break;
+			}
+		}
 		SMPBasicBlock *CurrBlock = this->GetBlockByNum(CurrBlockNum);
 		if (CurrBlock->IsProcessed())
 			break;
@@ -22625,9 +22873,10 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FIL
 				this->EmitSPARKAdaForLoop(CurrBlockNum, NextFollowBlockNum, SPARKBodyFile); // recurse and resume
 			}
 			else { // !LoopToProc case
-				// Generate procedure name for the loop being converted into a procedure.
-				// If loop starts at 0x8048ca0, we want ZSTLoopProc_8048ca0 as the proc name.
-				this->EmitSPARKAdaLoopCall(LoopAddr, (size_t) LoopNum, SPARKBodyFile);
+				bool MultipleExitTargets = this->EmitSPARKAdaLoopCall(LoopAddr, (size_t) LoopNum, SPARKBodyFile);
+				if (MultipleExitTargets) {
+					this->EmitSPARKAdaForMultipleLoopExitTargets(SPARKBodyFile, (size_t)LoopNum);
+				}
 				ResumeBlockNum = NextFollowBlockNum;
 				pair<int, int> BlockItem(CurrBlockNum, ResumeBlockNum);
 				pair<int, pair<int, int> > WorkListItem(LoopNum, BlockItem);
@@ -22816,10 +23065,12 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FIL
 							LastInst->SetSPARKTranslated();
 						}
 						else { // !LoopToProc case
-							// Generate procedure name for the loop being converted into a procedure.
-							// If loop starts at 0x8048ca0, we want ZSTLoopProc_8048ca0 as the proc name.
 							STARS_ea_t LoopAddr = NextBlock->GetFirstAddr();
-							this->EmitSPARKAdaLoopCall(LoopAddr, (size_t) LoopNum, SPARKBodyFile);
+							
+							bool MultipleExitTargets = this->EmitSPARKAdaLoopCall(LoopAddr, (size_t)LoopNum, SPARKBodyFile);
+							if (MultipleExitTargets) {
+								this->EmitSPARKAdaForMultipleLoopExitTargets(SPARKBodyFile, (size_t)LoopNum);
+							}
 							ResumeBlockNum = NextFollowBlockNum;
 							LastInst->SetSPARKTranslated();
 							pair<int, int> BlockItem(NextBlockNum, ResumeBlockNum);
@@ -22901,16 +23152,30 @@ void SMPFunction::EmitSPARKAdaForLoop(int HeaderBlockNum, int FollowBlockNum, FI
 	int CurrBlockNum = HeaderBlockNum;
 	int ResumeBlockNum = FollowBlockNum;
 	this->SPARKControlStack.push_back(SPARK_LOOP);
-	SMPBasicBlock *HeaderBlock = this->GetBlockByNum((size_t) HeaderBlockNum);
+	int LoopNum = this->GetLoopNumFromHeaderBlockNum(CurrBlockNum);
+	assert(0 <= LoopNum);
+	SMPBasicBlock *HeaderBlock = this->GetBlockByNum((size_t)HeaderBlockNum);
 	STARS_ea_t FirstAddr = HeaderBlock->GetFirstNonMarkerAddr();
 	assert(STARS_BADADDR != FirstAddr);
 	SMPInstr *FirstInst = *(HeaderBlock->GetInstIterFromAddr(FirstAddr));
+	bool MultipleExitTargets = this->DoesLoopHaveMultipleExitTargets((size_t) LoopNum);
+
 #if STARS_SPARK_CENTRALIZE_EMIT_LOOP
 	// We want to print "loop" and increase indentation.
 	PrintSPARKIndentTabs(SPARKBodyFile);
 	SMP_fprintf(SPARKBodyFile, "loop \n");
 	++STARS_SPARK_IndentCount;
 	FirstInst->EmitSPARKAdaLoopInvariants(SPARKBodyFile);
+
+	// Emit Booleans that track CFG flow if we have multiple exit targets.
+	if (MultipleExitTargets) {
+		// Generate the "Boolean flag = false;" declaration and initialization for each exit target block.
+		for (int ExitTargetBlockNum : this->LoopExitTargets[LoopNum]) {
+			string TargetString = this->GenerateSPARKLoopExitBooleanName(LoopNum, ExitTargetBlockNum);
+			PrintSPARKIndentTabs(SPARKBodyFile);
+			SMP_fprintf(SPARKBodyFile, "%s : Boolean := false;\n", TargetString.c_str());
+		}
+	}
 #endif
 
 	while ((CurrBlockNum != FollowBlockNum) && (CurrBlockNum >= 0)) {
@@ -22924,16 +23189,19 @@ void SMPFunction::EmitSPARKAdaForLoop(int HeaderBlockNum, int FollowBlockNum, FI
 		// Recursive descent based on the kind of block CurrBlock is.
 		if (CurrBlock->IsLoopHeaderBlock() && (!StartingLoop)) {
 			// We have fallen through to an inner loop. Emit a call to the loop proc created later, and jump past inner loop.
-			int LoopNum = this->GetLoopNumFromHeaderBlockNum(CurrBlockNum);
-			assert(0 <= LoopNum);
+			int InnerLoopNum = this->GetLoopNumFromHeaderBlockNum(CurrBlockNum);
+			assert(0 <= InnerLoopNum);
 			int NextFollowBlockNum = SMP_BLOCKNUM_UNINIT;
-			bool MultiExitLoop = this->GetLoopFollowBlockNum((size_t)LoopNum, NextFollowBlockNum);
-			bool LoopMightBeInfinite = (STARS_INFINITE_OR_MIDDLE_TESTING_LOOP == this->LoopTypesByLoopNum[LoopNum]);
+			bool MultiExitTargetsInnerLoop = this->GetLoopFollowBlockNum((size_t)InnerLoopNum, NextFollowBlockNum);
+			bool LoopMightBeInfinite = (STARS_INFINITE_OR_MIDDLE_TESTING_LOOP == this->LoopTypesByLoopNum[InnerLoopNum]);
 			// assert((SMP_BLOCKNUM_UNINIT != NextFollowBlockNum) || LoopMightBeInfinite);
-			this->EmitSPARKAdaLoopCall(CurrBlock->GetFirstAddr(), (size_t) LoopNum, SPARKBodyFile); 
+			bool MultipleExitTargets = this->EmitSPARKAdaLoopCall(CurrBlock->GetFirstAddr(), (size_t) InnerLoopNum, SPARKBodyFile); 
+			if (MultipleExitTargets) {
+				this->EmitSPARKAdaForMultipleLoopExitTargets(SPARKBodyFile, (size_t)InnerLoopNum);
+			}
 			ResumeBlockNum = NextFollowBlockNum;
 			pair<int, int> BlockItem(CurrBlockNum, ResumeBlockNum);
-			pair<int, pair<int, int> > WorkListItem(LoopNum, BlockItem);
+			pair<int, pair<int, int> > WorkListItem(InnerLoopNum, BlockItem);
 			this->SPARKLoopWorkList.push_back(WorkListItem);
 			this->CleanUpSPARKLoopWorkList();
 		}
@@ -22987,13 +23255,28 @@ void SMPFunction::EmitSPARKAdaForLoop(int HeaderBlockNum, int FollowBlockNum, FI
 						LastInst->EmitSPARKAda(SPARKBodyFile); // emit exit when (condition)
 						// We want to resume at the fall-through block, if it is in the loop,
 						//  which it should be because this is not the tail block.
-						list<SMPBasicBlock *>::const_iterator SuccIter;
-						if (INVERTED_LOOP_EXIT != LastCFType)
-							SuccIter = CurrBlock->GetFallThroughSucc();
-						else // must take the branch to stay in the loop
-							SuccIter = CurrBlock->GetCondNonFallThroughSucc();
-						assert(SuccIter != CurrBlock->GetLastConstSucc()); // COND_BRANCH must have fall through and non-fall-through
-						ResumeBlockNum = (*SuccIter)->GetNumber();
+						if (IsShortCircuitFlow(LastCFType)) {
+							// We have to follow the IsSingleExpression() descendants to get to the end of
+							//  the short-circuit expression. Then we can look at its successors and find one
+							//  that is in the loop, or set ResumeBlockNum to the loop follow node.
+							STARSCFGBlock *CurrCFGBlock = this->GetCFGBlockByNum((size_t)CurrBlockNum);
+							assert(nullptr != CurrCFGBlock);
+							int SuccBlockNum = CurrCFGBlock->GetExpr()->GetSuccNumInLoop((size_t)LoopNum);
+							if (0 <= SuccBlockNum) {
+								ResumeBlockNum = SuccBlockNum;
+							}
+							else {
+								ResumeBlockNum = FollowBlockNum; // done with loop
+							}
+						}
+						else {
+							list<SMPBasicBlock *>::const_iterator SuccIter = CurrBlock->GetSuccNotInLoop((size_t)LoopNum);
+							assert(SuccIter != CurrBlock->GetLastConstSucc()); // COND_BRANCH must have fall through and non-fall-through
+							int SuccBlockNum = (*SuccIter)->GetNumber();
+							SuccIter = CurrBlock->GetCondOtherSucc(SuccBlockNum);
+							assert(SuccIter != CurrBlock->GetLastConstSucc()); // COND_BRANCH must have fall through and non-fall-through
+							ResumeBlockNum = (*SuccIter)->GetNumber();
+						}
 					}
 					else if ((LastCFType == BRANCH_IF_THEN) || (LastCFType == BRANCH_IF_THEN_ELSE) || (LastCFType == SHORT_CIRCUIT_BRANCH)) {
 						// Translate if-else structure previously identified
@@ -23047,7 +23330,10 @@ void SMPFunction::EmitSPARKAdaForLoop(int HeaderBlockNum, int FollowBlockNum, FI
 						bool MultiExitLoop = this->GetLoopFollowBlockNum((size_t)LoopNum, 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);
+						bool MultipleExitTargets = this->EmitSPARKAdaLoopCall(NextBlock->GetFirstAddr(), (size_t) LoopNum, SPARKBodyFile);
+						if (MultipleExitTargets) {
+							this->EmitSPARKAdaForMultipleLoopExitTargets(SPARKBodyFile, (size_t)LoopNum);
+						}
 						ResumeBlockNum = NextFollowBlockNum;
 						LastInst->SetSPARKTranslated();
 						pair<int, int> BlockItem(NextBlockNum, ResumeBlockNum);
@@ -23105,9 +23391,103 @@ void SMPFunction::EmitSPARKAdaForLoop(int HeaderBlockNum, int FollowBlockNum, FI
 	PrintSPARKIndentTabs(SPARKBodyFile);
 	SMP_fprintf(SPARKBodyFile, "end loop;\n");
 #endif
+
 	return;
 } // end of SMPFunction::EmitSPARKAdaForLoop()
 
+void SMPFunction::EmitSPARKAdaForMultipleLoopExitTargets(FILE *SPARKBodyFile, size_t LoopNum) {
+	// Translate blocks that are reachable from the multiple exit
+	//  target blocks, including those exit target blocks, guarded
+	//  by checks of the CFG Boolean flags that control access to
+	//  those blocks in the original control flow.
+
+	// Start by getting the union of all block nums reachable from the exit target blocks
+	//  that are dominated by the loop head block.
+	int CurrLoopFollowBlockNum;
+	(void) this->GetLoopFollowBlockNum(LoopNum, CurrLoopFollowBlockNum);
+	STARSBitSet ReachableUnion;
+	ReachableUnion.AllocateBits(this->GetNumBlocks());
+	bool Initialized = false;
+	assert(!LoopExitTargetsReachabilitySets[LoopNum].empty());
+	for (int ExitTargetBlockNum : this->LoopExitTargets[LoopNum]) {
+		if (!Initialized) {
+			ReachableUnion = this->LoopExitTargetsReachabilitySets[LoopNum].at(ExitTargetBlockNum);
+			Initialized = true;
+		}
+		else {
+			ReachableUnion.UnionSets(this->LoopExitTargetsReachabilitySets[LoopNum].at(ExitTargetBlockNum));
+		}
+	}
+
+	// Now, generate code for each block number in ReachableUnion, guarded based on the bits in each reachability set.
+	size_t StartBlockNum = (size_t)ReachableUnion.FindLowestBitSet();
+	size_t EndBlockNum = (size_t)ReachableUnion.FindHighestBitSet();
+	assert(StartBlockNum < this->GetNumBlocks());
+	assert(EndBlockNum < this->GetNumBlocks());
+
+	for (size_t BlockNum = StartBlockNum; BlockNum <= EndBlockNum; ++BlockNum) {
+		SMPBasicBlock *CurrBlock = this->GetBlockByNum(BlockNum);
+		if (ReachableUnion.GetBit(BlockNum) && (!CurrBlock->IsProcessed()) && (!CurrBlock->IsSPARKTranslated())) {
+			bool StartedGuardOutput = false;
+			uint32_t ReachableSourceCount = 0;
+			for (const pair<int, STARSBitSet> &CurrReachablePair : this->LoopExitTargetsReachabilitySets[LoopNum]) {
+				STARSBitSet CurrBitSet;
+				CurrBitSet.AllocateBits(CurrReachablePair.second.GetNumBits());
+				CurrBitSet = CurrReachablePair.second;
+				if (CurrBitSet.GetBit(BlockNum)) {
+					if (CurrBlock->IsLoopHeaderBlock()) {
+						// We have to emit a loop call and not translate blocks in this loop.
+						STARS_ea_t LoopAddr = CurrBlock->GetFirstNonMarkerAddr();
+						size_t InnerLoopNum = this->GetLoopNumFromHeaderBlockNum((int)BlockNum);
+						bool MultipleExitTargets = this->EmitSPARKAdaLoopCall(LoopAddr, InnerLoopNum, SPARKBodyFile);
+						if (MultipleExitTargets) { // Recurse for reachable blocks from inner loop
+							this->EmitSPARKAdaForMultipleLoopExitTargets(SPARKBodyFile, InnerLoopNum);
+						}
+						int ResumeBlockNum;
+						(void) this->GetLoopFollowBlockNum(InnerLoopNum, ResumeBlockNum);
+						pair<int, int> BlockItem(BlockNum, ResumeBlockNum);
+						pair<int, pair<int, int> > WorkListItem(InnerLoopNum, BlockItem);
+						this->SPARKLoopWorkList.push_back(WorkListItem);
+						this->CleanUpSPARKLoopWorkList();
+
+						// Reset the bits in the bitsets that are within the inner loop.
+						list<size_t> InnerBlockList;
+						this->BuildLoopBlockList(InnerLoopNum, InnerBlockList);
+						for (size_t InnerLoopBlockNum : InnerBlockList) {
+							CurrBitSet.ResetBit(InnerLoopBlockNum);
+							ReachableUnion.ResetBit(InnerLoopBlockNum);
+						}
+					}
+				}
+				if (CurrBitSet.GetBit(BlockNum) && (!CurrBlock->IsProcessed()) && (!CurrBlock->IsSPARKTranslated())) {
+					int ExitTargetBlockNum = CurrReachablePair.first;
+					++ReachableSourceCount;
+					string GuardBoolString = this->GenerateSPARKLoopExitBooleanName(LoopNum, ExitTargetBlockNum);
+					if (!StartedGuardOutput) {
+						PrintSPARKIndentTabs(SPARKBodyFile);
+						SMP_fprintf(SPARKBodyFile, "-- Restructured CFG for multiple loop exit targets.\n");
+						PrintSPARKIndentTabs(SPARKBodyFile);
+						SMP_fprintf(SPARKBodyFile, "if (%s", GuardBoolString.c_str());
+						StartedGuardOutput = true;
+					}
+					else {
+						SMP_fprintf(SPARKBodyFile, " or %s", GuardBoolString.c_str());
+					}
+				}
+			} // end for each CurrReachablePair
+			if (StartedGuardOutput) {
+				SMP_fprintf(SPARKBodyFile, ") then\n");
+				++STARS_SPARK_IndentCount;
+				this->EmitSPARKAdaForBlock((int)BlockNum, CurrLoopFollowBlockNum, SPARKBodyFile, false, false, ReachableSourceCount);
+				--STARS_SPARK_IndentCount;
+				PrintSPARKIndentTabs(SPARKBodyFile);
+				SMP_fprintf(SPARKBodyFile, "end if;\n");
+			}
+		}
+	}
+	return;
+} // end of SMPFunction::EmitSPARKAdaForMultipleLoopExitTargets()
+
 // recursive descent translation of switch statement starting with INDIR_JUMP block, stop before Follow Block
 void SMPFunction::EmitSPARKAdaForSwitch(int HeaderBlockNum, int FollowBlockNum, FILE *SPARKBodyFile) {
 	assert(0 <= HeaderBlockNum);
@@ -23194,7 +23574,7 @@ void SMPFunction::EmitSPARKAdaForSwitch(int HeaderBlockNum, int FollowBlockNum,
 			}
 		} // end for all values in current case
 		// Now, translate the code inside the case.
-		this->EmitSPARKAdaForBlock(CaseBlockNum, NextFollowBlockNum, SPARKBodyFile, false);
+		this->EmitSPARKAdaForBlock(CaseBlockNum, NextFollowBlockNum, SPARKBodyFile, false, false);
 		--STARS_SPARK_IndentCount;
 	} // end for all cases
 	// Emit the default case.
@@ -23202,7 +23582,7 @@ void SMPFunction::EmitSPARKAdaForSwitch(int HeaderBlockNum, int FollowBlockNum,
 		PrintSPARKIndentTabs(SPARKBodyFile);
 		SMP_fprintf(SPARKBodyFile, "others =>\n");
 		++STARS_SPARK_IndentCount;
-		this->EmitSPARKAdaForBlock(TableInfo.DefaultCaseBlockNum, NextFollowBlockNum, SPARKBodyFile, true);
+		this->EmitSPARKAdaForBlock(TableInfo.DefaultCaseBlockNum, NextFollowBlockNum, SPARKBodyFile, true, false);
 		--STARS_SPARK_IndentCount;
 	}
 	// Emit the "end case;" statement
@@ -23273,11 +23653,15 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
 			int CurrBlockNum = LoopHeadBlock->GetNumber();
 			int LoopNum = this->GetLoopNumFromHeaderBlockNum(CurrBlockNum);
 			assert(0 <= LoopNum);
-			this->EmitSPARKAdaLoopCall(LoopAddr, (size_t) LoopNum, SPARKBodyFile);
+			bool MultipleExitTargets = this->EmitSPARKAdaLoopCall(LoopAddr, (size_t) LoopNum, SPARKBodyFile);
+			if (MultipleExitTargets) {
+				this->EmitSPARKAdaForMultipleLoopExitTargets(SPARKBodyFile, (size_t)LoopNum);
+			}
 			// Put the loop header and loop follow block numbers onto the work list
 			int LoopFollowBlockNum = SMP_BLOCKNUM_UNINIT;
 			bool MultiExitLoop = this->GetLoopFollowBlockNum((size_t)LoopNum, LoopFollowBlockNum);
-			assert(0 < LoopFollowBlockNum);
+			bool LoopFollowBlocksAreReturnBlocks = (SMP_BLOCKNUM_COMMON_RETURN == LoopFollowBlockNum);
+			assert((0 < LoopFollowBlockNum) || (LoopFollowBlocksAreReturnBlocks && MultiExitLoop));
 			pair<int, int> BlockItem(CurrBlockNum, LoopFollowBlockNum);
 			pair<int, pair<int, int> > WorkListItem(LoopNum, BlockItem);
 			this->SPARKLoopWorkList.push_back(WorkListItem);
@@ -23288,9 +23672,11 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
 			//  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.
-			SMPBasicBlock *LoopFollowBlock = this->GetBlockByNum((size_t) LoopFollowBlockNum);
-			if (!LoopFollowBlock->IsProcessed() && this->DoesBlockDominateBlock(HeaderBlockNum, LoopFollowBlockNum)) {
-				this->EmitSPARKAdaForBlock(LoopFollowBlockNum, FollowBlockNum, SPARKBodyFile, false, false);
+			if (0 < LoopFollowBlockNum) {
+				SMPBasicBlock *LoopFollowBlock = this->GetBlockByNum((size_t)LoopFollowBlockNum);
+				if (!LoopFollowBlock->IsProcessed() && this->DoesBlockDominateBlock(HeaderBlockNum, LoopFollowBlockNum)) {
+					this->EmitSPARKAdaForBlock(LoopFollowBlockNum, FollowBlockNum, SPARKBodyFile, false, false);
+				}
 			}
 
 			--STARS_SPARK_IndentCount;
@@ -23394,7 +23780,7 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
 		}
 		else {
 			this->SPARKControlStack.push_back(SPARK_THEN_CLAUSE);
-			this->EmitSPARKAdaForBlock(FallThroughBlockNum, FollowBlockNum, SPARKBodyFile, false);
+			this->EmitSPARKAdaForBlock(FallThroughBlockNum, FollowBlockNum, SPARKBodyFile, false, false);
 			this->SPARKControlStack.pop_back();
 			CheckFTBlock = (InsideLoop && UnknownFollowBlock);
 		}
@@ -23410,7 +23796,7 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
 		}
 		else {
 			this->SPARKControlStack.push_back(SPARK_ELSE_CLAUSE);
-			this->EmitSPARKAdaForBlock(DistantBlockNum, FollowBlockNum, SPARKBodyFile, false);
+			this->EmitSPARKAdaForBlock(DistantBlockNum, FollowBlockNum, SPARKBodyFile, false, false);
 			this->SPARKControlStack.pop_back();
 			CheckDistantBlock = (InsideLoop && UnknownFollowBlock);
 		}
@@ -23423,7 +23809,7 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
 	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));
+		InvertedLoopExitCase = (this->DoesBlockDominateBlock(FollowBlockNum, FallThroughBlockNum) && (IsInvertedLoopExitFlow(FollowBlockCFType)));
 	}
 #if 1
 	else if (InsideLoop) {
@@ -23485,7 +23871,9 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
 } // end of SMPFunction::EmitSPARKAdaForConditional()
 
 // emit call to loop proc that will be created later starting at LoopAddr
-void SMPFunction::EmitSPARKAdaLoopCall(STARS_ea_t LoopAddr, size_t LoopIndex, FILE *SPARKBodyFile) {
+bool SMPFunction::EmitSPARKAdaLoopCall(STARS_ea_t LoopAddr, size_t LoopIndex, FILE *SPARKBodyFile) {
+	// Generate procedure name for the loop being converted into a procedure.
+	// If loop starts at 0x8048ca0, we want ZSTLoopProc_8048ca0 as the proc name.
 	std::string ProcName("ZSTLoopProc_");
 	std::ostringstream AddrString;
 	AddrString << std::hex << LoopAddr;
@@ -23502,7 +23890,8 @@ void SMPFunction::EmitSPARKAdaLoopCall(STARS_ea_t LoopAddr, size_t LoopIndex, FI
 		SMP_fprintf(SPARKBodyFile, "%s;\n", ProcName.c_str());
 	}
 
-	return;
+	bool MultipleExitTargets = (this->LoopExitTargets[LoopIndex].size() > 1);
+	return MultipleExitTargets;
 } // end of SMPFunction::EmitSPARKAdaLoopCall()
 
 // Based on control flow structure of CurrBlock, find Ada follow block num; -1 if no structure besides fall-through
@@ -23543,12 +23932,16 @@ int SMPFunction::FindFollowBlockNum(SMPBasicBlock *CurrBlock, bool StartAtLastIn
 			if (IsLoopExitFlow(LastCFType)) {
 				// Middle exit from loop. Follow block is fall-through.
 				list<SMPBasicBlock *>::const_iterator SuccIter;
-				if (INVERTED_LOOP_EXIT != LastCFType)
+				if (!IsInvertedLoopExitFlow(LastCFType)) {
 					SuccIter = CurrBlock->GetFallThroughSucc();
-				else // must take branch to stay in the loop for INVERTED_LOOP_EXIT
+					assert(SuccIter != CurrBlock->GetLastConstSucc()); // COND_BRANCH must have fall through and non-fall-through
+					FollowBlockNum = (*SuccIter)->GetNumber();
+				}
+				else if (INVERTED_LOOP_EXIT == LastCFType) { // must take branch to stay in the loop for INVERTED_LOOP_EXIT or SHORT_CIRCUIT_INVERTED_LOOP_EXIT
 					SuccIter = CurrBlock->GetCondNonFallThroughSucc();
-				assert(SuccIter != CurrBlock->GetLastConstSucc()); // COND_BRANCH must have fall through and non-fall-through
-				FollowBlockNum = (*SuccIter)->GetNumber();
+					assert(SuccIter != CurrBlock->GetLastConstSucc()); // COND_BRANCH must have fall through and non-fall-through
+					FollowBlockNum = (*SuccIter)->GetNumber();
+				}
 			}
 			else {
 				// Handle if-else jumps here.
@@ -23568,19 +23961,39 @@ int SMPFunction::FindFollowBlockNum(SMPBasicBlock *CurrBlock, bool StartAtLastIn
 } // end of SMPFunction::FindFollowBlockNum()
 
 // return true if loop has multiple follow blocks
-bool SMPFunction::GetLoopFollowBlockNum(const size_t LoopNum, int &FirstFollowBlockNum) const {
-	assert(LoopNum < this->LoopFollowNodes.size());
-	assert(!this->LoopFollowNodes[LoopNum].empty());
-	bool MultiExitLoop = (1 < this->LoopFollowNodes[LoopNum].size());
-	FirstFollowBlockNum = *(this->LoopFollowNodes[LoopNum].cbegin());
-	return MultiExitLoop;
+bool SMPFunction::GetLoopFollowBlockNum(const size_t LoopNum, int &FollowBlockNum) const {
+	assert(LoopNum < this->LoopExitTargets.size());
+	assert(!this->LoopExitTargets[LoopNum].empty());
+	FollowBlockNum = SMP_BLOCKNUM_UNINIT;
+	bool MultiExitTargetLoop = (1 < this->LoopExitTargets[LoopNum].size());
+	if (MultiExitTargetLoop) { // Multiple exit targets; their convergence point is the follow block
+		map<int, set<int> >::const_iterator MapIter = this->MultiLoopExitTargetsConvergenceMap.find((int)LoopNum);
+		if (MapIter != this->MultiLoopExitTargetsConvergenceMap.cend()) {
+			if (1 == MapIter->second.size()) {
+				FollowBlockNum = *(MapIter->second.cbegin());
+			}
+		}
+	}
+	else { // Only one exit target; it is the follow block num
+		FollowBlockNum = *(this->LoopExitTargets[LoopNum].cbegin());
+	}
+
+	return MultiExitTargetLoop;
 } // end of SMPFunction::GetLoopFollowBlockNum()
 
+// return true if loop has multiple exit target blocks
+bool SMPFunction::DoesLoopHaveMultipleExitTargets(const size_t LoopNum) const {
+	assert(LoopNum < this->LoopExitTargets.size());
+	assert(!this->LoopExitTargets[LoopNum].empty());
+	bool MultiExitTargetLoop = (1 < this->LoopExitTargets[LoopNum].size());
+
+	return MultiExitTargetLoop;
+} // end of SMPFunction::DoesLoopHaveMultipleExitTargets()
 
 // found in LoopFollowNodes[LoopNum] set?
 bool SMPFunction::IsBlockLoopFollowBlock(const std::size_t LoopNum, const int BlockNum) const {
-	assert(LoopNum < this->LoopFollowNodes.size());
-	return (this->LoopFollowNodes[LoopNum].find(BlockNum) != this->LoopFollowNodes[LoopNum].cend());
+	assert(LoopNum < this->LoopExitTargets.size());
+	return (this->LoopExitTargets[LoopNum].find(BlockNum) != this->LoopExitTargets[LoopNum].cend());
 } // end of SMPFunction::IsBlockLoopFollowBlock()
 
 // common code for different cases in EmitFuncPtrShadowingAnnotations2()
diff --git a/src/base/SMPInstr.cpp b/src/base/SMPInstr.cpp
index 8a742f84..8ed5abf7 100644
--- a/src/base/SMPInstr.cpp
+++ b/src/base/SMPInstr.cpp
@@ -6950,13 +6950,16 @@ 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();
+	int CurrBlockNum = this->GetBlock()->GetNumber();
 	bool MightBeVisitedTwice = this->GetBlock()->IsSingleExpression() || this->GetBlock()->IsOnlyInternalDirectJump() || (InstAddr == this->GetBlock()->GetLastAddr()) || (CALL == this->GetDataFlowType());
 	bool ValidTranslation = (!this->HasBeenTranslatedToSPARK() || MightBeVisitedTwice);
+	int LoopNum = this->GetBlock()->GetFunc()->GetInnermostLoopNum(CurrBlockNum);
+	bool MultiExitTargetLoop = (LoopNum < 0) ? false : this->GetBlock()->GetFunc()->DoesLoopHaveMultipleExitTargets((size_t)LoopNum);
 	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);
+		SMP_msg("FATAL ERROR: EmitSPARKAda visiting inst at %llx in block %d twice.\n", (uint64_t) InstAddr, this->GetBlock()->GetNumber());
 	}
 	assert(ValidTranslation);
 	SMP_fprintf(OutFile, "\n");
@@ -7075,10 +7078,15 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
 				else {
 					// 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");
+					if (MultiExitTargetLoop) {
+						this->EmitSPARKConditionalLoopMultiExit(OutFile, (size_t)LoopNum, true, nullptr);
+					}
+					else {
+						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
@@ -7106,12 +7114,18 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
 				SMP_fprintf(OutFile, "exit;\n");
 			}
 			else { // conditional
-				SMP_fprintf(OutFile, "exit when ");
-				if (LOOP_EXIT == FuncControlFlowType)
-					this->MDEmitSPARKAdaCondition(OutFile);
-				else // INVERTED_LOOP_EXIT
-					this->MDEmitSPARKAdaInvertedCondition(OutFile);
-				SMP_fprintf(OutFile, ";\n");
+				bool InvertCondition = IsInvertedLoopExitFlow(FuncControlFlowType); // INVERTED_LOOP_EXIT or SHORT_CIRCUIT_INVERTED_LOOP_EXIT
+				if (MultiExitTargetLoop) {
+					this->EmitSPARKConditionalLoopMultiExit(OutFile, (size_t)LoopNum, InvertCondition, nullptr);
+				}
+				else {
+					SMP_fprintf(OutFile, "exit when ");
+					if (!InvertCondition)
+						this->MDEmitSPARKAdaCondition(OutFile);
+					else // INVERTED_LOOP_EXIT
+						this->MDEmitSPARKAdaInvertedCondition(OutFile);
+					SMP_fprintf(OutFile, ";\n");
+				}
 			}
 			// Check for bottom-testing loop case where we have:
 			// loop
@@ -7167,7 +7181,7 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
 			SMP_fprintf(OutFile, " then \n");
 			++STARS_SPARK_IndentCount;
 		}
-		else if ((SHORT_CIRCUIT_BRANCH == FuncControlFlowType) || (SHORT_CIRCUIT_LOOP_EXIT == FuncControlFlowType)) {
+		else if (IsShortCircuitFlow(FuncControlFlowType)) {
 			// Multiple short circuit condition branches have been coalesced together.
 			STARSCFGBlock *CurrCFGBlock = this->GetBlock()->GetFunc()->GetCFGBlockByNum((size_t) this->GetBlock()->GetNumber());
 			assert(nullptr != CurrCFGBlock);
@@ -7178,10 +7192,20 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
 					CurrCFGBlock->GetExpr()->EmitSPARKAdaShortCircuitExpr(OutFile);
 					SMP_fprintf(OutFile, ") then \n");
 				}
-				else { // SHORT_CIRCUIT_LOOP_EXIT
-					SMP_fprintf(OutFile, "exit when (");
-					CurrCFGBlock->GetExpr()->EmitSPARKAdaShortCircuitExpr(OutFile);
-					SMP_fprintf(OutFile, ");\n");
+				else { // SHORT_CIRCUIT_LOOP_EXIT or SHORT_CIRCUIT_INVERTED_LOOP_EXIT
+					if (MultiExitTargetLoop) {
+						this->EmitSPARKConditionalLoopMultiExit(OutFile, (size_t)LoopNum, false, CurrCFGBlock);
+					}
+					else if (SHORT_CIRCUIT_INVERTED_LOOP_EXIT == FuncControlFlowType) {
+						SMP_fprintf(OutFile, "exit when (not (");
+						CurrCFGBlock->GetExpr()->EmitSPARKAdaShortCircuitExpr(OutFile);
+						SMP_fprintf(OutFile, "));\n");
+					}
+					else {
+						SMP_fprintf(OutFile, "exit when (");
+						CurrCFGBlock->GetExpr()->EmitSPARKAdaShortCircuitExpr(OutFile);
+						SMP_fprintf(OutFile, ");\n");
+					}
 					// Check for bottom-testing loop case where we have:
 					// loop
 					//    [instructions]
@@ -7463,6 +7487,37 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
 	return;
 } // end of SMPInstr::EmitSPARKAda()
 
+// Refactored helper to emit conditional loop exits in SPARK for loops with multiple exit target blocks.
+void SMPInstr::EmitSPARKConditionalLoopMultiExit(FILE *BodyFile, const size_t LoopNum, const bool InvertCondition, const STARSCFGBlock *CFGBlock) {
+	int ExitTargetBlockNum;
+	if (nullptr == CFGBlock) {
+		list<SMPBasicBlock *>::const_iterator ExitTargetIter = this->GetBlock()->GetSuccNotInLoop((size_t)LoopNum);
+		assert(ExitTargetIter != this->GetBlock()->GetLastConstSucc());
+		ExitTargetBlockNum = (*ExitTargetIter)->GetNumber();
+	}
+	else {
+		ExitTargetBlockNum = CFGBlock->GetExpr()->GetSuccNumNotInLoop((size_t)LoopNum);
+	}
+	assert(SMP_BLOCKNUM_UNINIT != ExitTargetBlockNum);
+	string ExitFlagString = this->GetBlock()->GetFunc()->GenerateSPARKLoopExitBooleanName((size_t)LoopNum, ExitTargetBlockNum);
+	PrintSPARKIndentTabs(BodyFile);
+	SMP_fprintf(BodyFile, "%s := ", ExitFlagString.c_str());
+	if (nullptr != CFGBlock) {
+		CFGBlock->GetExpr()->EmitSPARKAdaShortCircuitExpr(BodyFile);
+	}
+	else if (InvertCondition) {
+		this->MDEmitSPARKAdaInvertedCondition(BodyFile);
+	}
+	else {
+		this->MDEmitSPARKAdaCondition(BodyFile);
+	}
+	SMP_fprintf(BodyFile, ";\n");
+	PrintSPARKIndentTabs(BodyFile);
+	SMP_fprintf(BodyFile, "exit when %s;\n", ExitFlagString.c_str());
+
+	return;
+} // end of SMPInstr::EmitSPARKConditionalLoopMultiExit()
+
 // Equality operator for SMPInstr. Key field is address.
 int SMPInstr::operator==(const SMPInstr &rhs) const {
 	if (this->GetAddr() != rhs.GetAddr())
diff --git a/src/base/SMPProgram.cpp b/src/base/SMPProgram.cpp
index 98b9cc8f..43c9d2b6 100644
--- a/src/base/SMPProgram.cpp
+++ b/src/base/SMPProgram.cpp
@@ -898,16 +898,16 @@ void SMPProgram::Analyze(ProfilerInformation *pi, FILE *AnnotFile, FILE *InfoAnn
 
 	// Loop 7B: Loop iteration and memory access analysis.
 	Time4 = time(nullptr);
-	for (FuncListIter = this->PrioritizedFuncList.begin(); FuncListIter != this->PrioritizedFuncList.end(); ++FuncListIter) {
-		CurrFunc = (*FuncListIter);
-		if (nullptr == CurrFunc) {
-			SMP_msg("ERROR: NULL Func ptr in PrioritizedFuncList\n");
-			continue;
-		}
-		if (global_STARS_program->ShouldSTARSPerformDeepLoopAnalyses()) {
-			if (CurrFunc->StackPtrAnalysisSucceeded() && CurrFunc->HasGoodRTLs() && (!CurrFunc->HasUnresolvedIndirectJumps())) {
-				CurrFunc->AnalyzeLoopIterations();
+	if (global_STARS_program->ShouldSTARSPerformDeepLoopAnalyses()) {
+		for (FuncListIter = this->PrioritizedFuncList.begin(); FuncListIter != this->PrioritizedFuncList.end(); ++FuncListIter) {
+			CurrFunc = (*FuncListIter);
+			if (nullptr == CurrFunc) {
+				SMP_msg("ERROR: NULL Func ptr in PrioritizedFuncList\n");
+				continue;
 			}
+				if (CurrFunc->StackPtrAnalysisSucceeded() && CurrFunc->HasGoodRTLs() && (!CurrFunc->HasUnresolvedIndirectJumps())) {
+					CurrFunc->AnalyzeLoopIterations();
+				}
 		}
 	}
 	Time5 = time(nullptr);
@@ -1147,7 +1147,7 @@ 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());
+		bool FuncFound = (0x4018c0 == TempFunc->GetFirstFuncAddr());
 		if (FuncFound) {
 			TempFunc->Dump();
 			TempFunc->DumpDotCFG();
-- 
GitLab