From 1b2f22146c02233a41c3ed2bf17a86a0474049db Mon Sep 17 00:00:00 2001
From: Clark Coleman <clc@zephyr-software.com>
Date: Sun, 4 Oct 2020 20:15:12 -0400
Subject: [PATCH] SPARK: Translate fall-through block after conditional tail
call.
---
include/base/SMPFunction.h | 3 +-
src/base/SMPFunction.cpp | 96 +++++++++++++++++++++++++++++++++++---
2 files changed, 92 insertions(+), 7 deletions(-)
diff --git a/include/base/SMPFunction.h b/include/base/SMPFunction.h
index 525a6521..e1387ed1 100644
--- a/include/base/SMPFunction.h
+++ b/include/base/SMPFunction.h
@@ -600,7 +600,7 @@ public:
bool IsBlockInLoop(int BlockNum, std::size_t LoopNum) const; // 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 BuildLoopList(int BlockNum, std::list<std::size_t> &LoopList) const; // 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
STARSExpression *CreateMemoryAddressExpr(const STARSOpndTypePtr &MemDefOp, SMPInstr *WriteInst); // create expression for the memory address computation in MemDefOp
@@ -1017,6 +1017,7 @@ private:
int FindConditionalFollowNode(int HeadBlockNum); // Find candidate block # for if-else follow node for HeadBlockNum; return -1 otherwise
int TrackConditionalBranchTerminus(int BranchHeadBlockNum, int CurrBlockNum, STARSBitSet &BlocksSeen, int &BlockAlreadySeenCounter); // Track CurrBlockNum until we reach block that BranchHeadBlockNum doesn't dominate, or dead end. Return block num, possibly SMP_BLOCKNUM_COMMON_RETURN.
bool FindUnstructuredIfThenElse(const int HeadBlockNum, const int FollowBlockNum) const; // Do IF and ELSE branches merge before FollowBlockNum?
+ bool FindMultiLoopContinue(const int BranchBlockNum) const; // Does COND_BRANCH behave as an unstructured multi-level loop continue statement?
void FindGuardedLoops(void); // Find guarded loops and fill the GuardToLoopMap and LoopToGuardMap
bool IsSPARKLoopInTranslationStack(void) const; // Are we already translating a SPARK_LOOP when we encounter another loop?
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index 342a3df4..8642815e 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -593,11 +593,13 @@ bool SMPFunction::ComputeInOutRegs(bool InheritPass, bool &WritesMem, bool &Call
bool Changed = false;
bool MemoryInput = false;
bool MemoryOutput = false;
- bool VerboseOutput = global_stars_interface->VerboseLoopsMode();
+ bool VerboseOutput = global_stars_interface->VerboseSPARKMode();
CallChainNonReturning = false;
if (InheritPass) {
- SMP_msg("INFO: InheritPass for ComputeInOutRegs(), function %s at %llx\n", this->GetFuncName(), (uint64_t) this->GetFirstFuncAddr());
+ if (VerboseOutput) {
+ SMP_msg("INFO: InheritPass for ComputeInOutRegs(), function %s at %llx\n", this->GetFuncName(), (uint64_t) this->GetFirstFuncAddr());
+ }
// Look at all callees and union their bitsets in.
size_t OldInputBitCount = this->InputRegs.count();
size_t OldOutputBitCount = this->OutputRegs.count();
@@ -11567,7 +11569,7 @@ bool SMPFunction::AnalyzeConditionalStatements(void) {
SMPitype FlowType = LastInst->GetDataFlowType();
if (FlowType == COND_BRANCH) {
ControlFlowType LastCFType = this->GetControlFlowType(LastAddr);
- if (FALL_THROUGH != LastCFType) { // already part of some loop or switch structure
+ if (FALL_THROUGH != LastCFType) { // already part of some compound conditional, loop or switch structure
continue;
}
int HeadBlockNum = CurrBlock->GetNumber();
@@ -11743,6 +11745,11 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
return FollowBlockNum;
}
+ // Screen out branches that go outside their current loop in an unstructured way.
+ if (this->FindMultiLoopContinue(HeadBlockNum)) {
+ return FollowBlockNum;
+ }
+
// A well-structured candidate would be the biggest RPO-number block that has >= 2 predecessors
// and has HeadBlockNum as its IDom.
// EXCEPTION #1: Return and loop-back instructions interrupt control flow. See below.
@@ -12277,6 +12284,67 @@ bool SMPFunction::FindUnstructuredIfThenElse(const int HeadBlockNum, const int F
return UnstructuredClauses;
} // end of SMPFunction::FindUnstructuredIfThenElse()
+// Does COND_BRANCH behave as an unstructured multi-level loop continue statement?
+bool SMPFunction::FindMultiLoopContinue(const int BranchBlockNum) const {
+ assert(0 <= BranchBlockNum);
+ bool Unstructured = false;
+ if (!this->IsBlockInAnyLoop(BranchBlockNum))
+ return Unstructured;
+
+ int InnerMostLoopNum = this->GetInnermostLoopNum(BranchBlockNum);
+ SMPBasicBlock *BranchBlock = this->GetBlockByNum((size_t)BranchBlockNum);
+ assert(0 <= InnerMostLoopNum);
+
+ // Each successor of the COND_BRANCH at the end of BranchBlock
+ // must be in one of the following three categories:
+ // A) Inside the innermost loop containing BranchBlock.
+ // B) The follow block for the innermost loop containing BranchBlock.
+ // C) The header block for an outer loop that has the same follow block as the
+ // innermost loop.
+ //
+ // The SPARK Ada translations of these cases are straightforward:
+ // A) if-then-else within the innermost loop.
+ // B) exit when (condition) or exit when (inverted condition).
+ // C) if (inverted condition) then ... endif; endloop; endloop;
+ //
+ // Note that category C precludes having any code inside the endif-endloop-endloop series.
+ // This condition is guaranteed by having the same follow nodes; a follow node comes
+ // right after an endloop, so if an inner loop has the same follow node as an outer loop,
+ // their endloop statements are consecutive.
+ //
+ // An example of a COND_BRANCH inside a loop that is not in categories A or B but is within
+ // category C is seen at the end of basic block #5 in the func at 0x4031b0 in bzip2.psexe.
+ // An example that fails all three category tests, and is thus an unstructured multi-level
+ // loop continue statement, is seen at basic block #8 in the func at 0x437bf3 in busybox.psexe.
+
+ int InnerLoopFollowBlockNum = this->LoopFollowNodes[(size_t)InnerMostLoopNum];
+ for (list<SMPBasicBlock *>::const_iterator SuccIter = BranchBlock->GetFirstConstSucc(); SuccIter != BranchBlock->GetLastConstSucc(); ++SuccIter) {
+ SMPBasicBlock *SuccBlock = (*SuccIter);
+ int SuccBlockNum = SuccBlock->GetNumber();
+ if (!this->IsBlockInLoop(SuccBlockNum, (size_t)InnerMostLoopNum)) {
+ // Failed category A test.
+ if (SuccBlockNum != InnerLoopFollowBlockNum) {
+ // Failed category B test. Needs to be header block for outer loop.
+ int OuterLoopFollowBlockNum = SMP_BLOCKNUM_UNINIT;
+ if (SuccBlock->IsLoopHeaderBlock()) {
+ int OuterLoopNum = this->GetLoopNumFromHeaderBlockNum(SuccBlockNum);
+ assert(0 <= OuterLoopNum);
+ OuterLoopFollowBlockNum = this->LoopFollowNodes[(size_t)OuterLoopNum];
+ }
+ if (OuterLoopFollowBlockNum != InnerLoopFollowBlockNum) {
+ // Failed category C test.
+ Unstructured = true;
+ SMP_msg("ERROR: SPARK: Unstructured due to multi-level loop continue statement at %llx in %s\n",
+ (uint64_t)BranchBlock->GetLastAddr(), this->GetFuncName());
+ break;
+ }
+ }
+ }
+ } // end for all successors to BranchBlock
+
+ return Unstructured;
+} // end of SMPFunction::FindMultiLoopContinue()
+
// Find guarded loops and fill the GuardToLoopMap and LoopToGuardMap
void SMPFunction::FindGuardedLoops(void) {
assert(this->HasStructuredControlFlow());
@@ -14135,7 +14203,7 @@ bool SMPFunction::DoesEdgeExitLoop(const int BlockNum1, const int BlockNum2) con
} // end of SMPFunction::DoesEdgeExitLoop()
// build list of loop numbers that BlockNum is part of.
-void SMPFunction::BuildLoopList(int BlockNum, list<std::size_t> &LoopList) {
+void SMPFunction::BuildLoopList(int BlockNum, list<std::size_t> &LoopList) const {
std::size_t LoopIndex;
assert((BlockNum >= 0) && (BlockNum < this->BlockCount));
for (LoopIndex = 0; LoopIndex < this->LoopCount; ++LoopIndex) {
@@ -16883,6 +16951,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
else {
SMP_msg("INFO: Overlapping loops non-single-expr unstructured CFG case at block %zu in %s\n", BlockIndex, this->GetFuncName());
}
+ break; // no point in continuing if we cannot translate to SPARK Ada
}
// Find all conditional and unconditional jumps within the function.
@@ -16897,6 +16966,11 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
break; // no point in continuing if we cannot translate to SPARK Ada
}
+ if (this->FindMultiLoopContinue((int) BlockIndex)) {
+ this->HasStructuredCFG = false;
+ break; // no point in continuing if we cannot translate to SPARK Ada
+ }
+
int FollowBlockNum;
if (!InvertedExit) {
this->SetControlFlowType(InstAddr, LOOP_EXIT);
@@ -22512,7 +22586,10 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FIL
else if (FlowType == RETURN) {
LastInst->EmitSPARKAda(SPARKBodyFile);
// Handle possible tail call case
- ;
+ if ((FALL_THROUGH == LastCFType) && (1 == CurrBlock->GetNumSuccessors())) {
+ assert(LastInst->IsCondTailCall());
+ ResumeBlockNum = (*(CurrBlock->GetFirstConstSucc()))->GetNumber();
+ }
}
else if ((FlowType == CALL) || (FlowType == INDIR_CALL)) {
LastInst->EmitSPARKAda(SPARKBodyFile);
@@ -22894,8 +22971,15 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
// that guards the loop could be separated from the loop header by a block of
// straight-line (fallthrough-only) code, or not. We need to detect this case.
- SMPBasicBlock *FallThroughBlock = *(HeaderBlock->GetFallThroughSucc()); // !!!!****!!!! Could there be an inverted guard loop case?
+ SMPBasicBlock *FallThroughBlock = *(HeaderBlock->GetFallThroughSucc());
int FallThroughBlockNum = FallThroughBlock->GetNumber();
+ bool InvertedCase = LastInst->IsOddIfThenCase();
+ if (InvertedCase) {
+ // Guard jumps to the THEN case.
+ assert(FallThroughBlockNum == FollowBlockNum);
+ FallThroughBlock = *(HeaderBlock->GetCondNonFallThroughSucc());
+ FallThroughBlockNum = FallThroughBlock->GetNumber();
+ }
STARS_ea_t LoopAddr = GuardIter->second;
bool SeparatedCase = (!FallThroughBlock->IsLoopHeaderBlock());
SMPBasicBlock *LoopHeadBlock = this->GetBlockFromInstAddr(LoopAddr);
--
GitLab