From 63eb0fec03610229d90e0c184bf4503d61cf3c64 Mon Sep 17 00:00:00 2001
From: Clark Coleman <clc@zephyr-software.com>
Date: Fri, 28 Aug 2020 23:49:57 -0400
Subject: [PATCH] SPARK crash fixes for sks and mplayer binaries.
---
src/base/SMPFunction.cpp | 41 ++++++++++++++++++++++++++++++++--------
src/base/SMPInstr.cpp | 5 +++++
2 files changed, 38 insertions(+), 8 deletions(-)
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index 50649601..f74d212f 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -11123,14 +11123,24 @@ bool SMPFunction::FindSwitchStatementFollowBlock(struct SwitchTableInfo &TableIn
return ConsistentFollowBlock;
} // end of SMPFunction::FindSwitchStatementFollowBlock()
-// Start at CaseBlockNum, return followblocknum with IncomingEdgeCount
+// Start at CaseBlockNum, return followblocknum with >=IncomingEdgeCount predecessors
int SMPFunction::FindCaseFollowBlock(int CaseBlockNum, int HeaderBlockNum, std::size_t IncomingEdgeCount) const {
int FollowBlockNum = SMP_BLOCKNUM_UNINIT;
// We define a well-structured switch statement suh that it is forbidden to have one case fall through to another.
// Our algorithm would need to be modified to handle fall-throughs, which would require special translation to SPARK Ada
// as such case fall-throughs are not permitted in SPARK Ada.
- // Algorithm: Traverse CFG from CaseBlockNum until we find a block with IncomingEdgeCount that is dominated by HeaderBlockNum.
+ // What blocks have already been processed (i.e. follow block determinations from other cases)?
+ STARSBitSet ProcessedOutsideThisCase;
+ ProcessedOutsideThisCase.AllocateBits(this->GetNumBlocks());
+ for (size_t BlockIndex = 0; BlockIndex < this->GetNumBlocks(); ++BlockIndex)
+ if (this->GetBlockByNum(BlockIndex)->IsProcessed())
+ ProcessedOutsideThisCase.SetBit(BlockIndex);
+ // Using this bitset, we can differentiate between hitting a follow block multiple times from within this case
+ // (e.g. short-circuit branches out to it) and hitting it across different cases.
+
+ // Algorithm: Traverse CFG from CaseBlockNum until we find a block with IncomingEdgeCount that is dominated by HeaderBlockNum
+ // but is NOT dominated by CaseBlockNum.
// If we encounter an already processed block, stop and return -2 as the block number to signal this condition.
// If one of our successors finds a follow block and the others all return -2, return the follow block number.
// If we reach a block not dominated by HeaderBlockNum before finding a follow block or a visited block, return -1.
@@ -11140,22 +11150,32 @@ int SMPFunction::FindCaseFollowBlock(int CaseBlockNum, int HeaderBlockNum, std::
for (list<SMPBasicBlock *>::iterator SuccIter = CaseBlock->GetFirstSucc(); SuccIter != CaseBlock->GetLastSucc(); ++SuccIter) {
SMPBasicBlock *SuccBlock = (*SuccIter);
int SuccBlockNum = SuccBlock->GetNumber();
+
+ // Screen out back edges.
+ if (this->DoesBlockDominateBlock(SuccBlockNum, CaseBlockNum))
+ continue;
+
// NOTE: We have to screen out nested switch statements' follow blocks.
STARS_ea_t LastBlockAddr = SuccBlock->GetLastAddr();
ControlFlowType SuccBranchType = this->GetControlFlowType(LastBlockAddr);
+
+ // NOTE: Need more precise determination of nested switches?
bool NestedSwitch = (SuccBranchType == CASE_BREAK_TO_FOLLOW_NODE); // avoid being deceived by nested follow nodes
- // Possibilities: already visited; not dominated by HeaderBlockNum; has IncomingEdgeCount; or needs recursion
+
+ // Possibilities: already visited; not dominated by HeaderBlockNum; has >=IncomingEdgeCount; or needs recursion
if (this->DoesBlockDominateBlock(HeaderBlockNum, SuccBlockNum)) {
- if (SuccBlock->IsProcessed()) {
+ bool DomWithinCase = this->DoesBlockDominateBlock(CaseBlockNum, SuccBlockNum);
+
+ if (SuccBlock->IsProcessed() && ProcessedOutsideThisCase.GetBit((size_t) SuccBlockNum)) {
if (FollowBlockNum == SMP_BLOCKNUM_UNINIT)
- FollowBlockNum = -2; // record first already-visited block
+ FollowBlockNum = -2; // record first already-visited follow block
}
- else if (!NestedSwitch && (SuccBlock->GetNumPreds() == IncomingEdgeCount)) {
+ else if (!NestedSwitch && (SuccBlock->GetNumPreds() >= IncomingEdgeCount) && (!DomWithinCase)) {
// follow block found.
SuccBlock->SetProcessed(true);
FollowBlockNum = SuccBlockNum;
}
- else { // need to recurse into successor block
+ else if (DomWithinCase) { // need to recurse into successor block
int SuccFollowBlockNum = this->FindCaseFollowBlock(SuccBlockNum, HeaderBlockNum, IncomingEdgeCount);
// Meet function for existing FollowBlockNum and SuccFollowBlockNum
if ((FollowBlockNum == SMP_BLOCKNUM_UNINIT) || (FollowBlockNum == -2)) {
@@ -11177,6 +11197,11 @@ int SMPFunction::FindCaseFollowBlock(int CaseBlockNum, int HeaderBlockNum, std::
}
}
}
+ else {
+ // Wandered out of our case without finding follow block; unstructured.
+ FollowBlockNum = SMP_BLOCKNUM_UNINIT;
+ break;
+ }
}
else { // cannot be structured switch statement; wandered out of switch without finding good follow block.
FollowBlockNum = SMP_BLOCKNUM_UNINIT;
@@ -13697,7 +13722,7 @@ void SMPFunction::BuildDominatorTree(void) {
bool SMPFunction::DoesBlockDominateBlock(int HeadBlockNum, int TailBlockNum) const {
if (HeadBlockNum == TailBlockNum)
return true;
- else if ((HeadBlockNum == SMP_BLOCKNUM_UNINIT) || (TailBlockNum == SMP_BLOCKNUM_UNINIT)) {
+ else if ((HeadBlockNum < 0) || (TailBlockNum < 0)) {
return false;
}
else {
diff --git a/src/base/SMPInstr.cpp b/src/base/SMPInstr.cpp
index 0e98b8d4..3b9cf6db 100644
--- a/src/base/SMPInstr.cpp
+++ b/src/base/SMPInstr.cpp
@@ -2047,6 +2047,11 @@ void SMPRegTransfer::EmitSPARKAda(FILE *OutFile) {
}
SMPoperator CurrOper = this->GetOperator();
+ if ((SMP_INPUT == CurrOper) || (SMP_OUTPUT == CurrOper)) {
+ SMP_fprintf(OutFile, "\nERROR\n");
+ SMP_msg("ERROR: SPARK: Cannot translate operator SMP_INPUT or SMP_OUTPUT at %llx\n", (uint64_t) this->GetParentInst()->GetAddr());
+ return;
+ }
assert(CurrOper == SMP_ASSIGN);
bool X86ProcCall = this->GetParentInst()->MDIsArithmeticUsingCarryFlag();
uint16_t LeftByteWidth = LeftOp->GetByteWidth();
--
GitLab