From 6ae230fe3b98944eb2eb4dc1150d6a2e08b2e7fe Mon Sep 17 00:00:00 2001
From: Clark Coleman <clc@zephyr-software.com>
Date: Tue, 6 Oct 2020 23:42:09 -0400
Subject: [PATCH] SPARK: More precise analysis of loop exit to fix
SHORT_CIRCUIT_LOOP_EXIT classification errors.
---
src/base/SMPFunction.cpp | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index 6649038c..1c5aeb1e 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -11033,7 +11033,11 @@ void SMPFunction::BuildShadowCFG(void) {
void SMPFunction::CoalesceShadowBlocks(int LeftBlockNum, int RightBlockNum, bool NegateLeft, SMPoperator TopOper, int NewFTNum, int NewNFTNum) {
assert((0 <= LeftBlockNum) && (LeftBlockNum < (int)this->ShadowCFGBlocks.size()));
assert((0 <= RightBlockNum) && (RightBlockNum < (int)this->ShadowCFGBlocks.size()));
- bool LoopExitCase = this->IsBlockInAnyLoop(LeftBlockNum) && this->IsBlockInAnyLoop(RightBlockNum) && (!(this->AreBlocksInSameLoops(NewFTNum, NewNFTNum)));
+ bool InsideLoop = this->IsBlockInAnyLoop(LeftBlockNum);
+ 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)));
STARSCFGBlock *LeftCFGBlock = this->ShadowCFGBlocks[LeftBlockNum];
STARSCFGBlock *RightCFGBlock = this->ShadowCFGBlocks[RightBlockNum];
--
GitLab