diff --git a/include/base/SMPFunction.h b/include/base/SMPFunction.h
index 3bc7d21fb683c8f05c163781299b9e2b47df67e0..00a9fabc6ab7b1453c4500839ddc18d9defc612b 100644
--- a/include/base/SMPFunction.h
+++ b/include/base/SMPFunction.h
@@ -1017,6 +1017,7 @@ private:
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?
+ void CleanUpSPARKLoopWorkList(void); // Remove duplicate elements in this->SPARKLoopWorkList.
void UpdateStackBytesWrittenByLoop(STARS_sval_t FinalStackPtrOffset, std::size_t MemWidth, std::size_t LoopNum); // update {Nega, Posi}tiveStackBytesWrittenByLoop[LoopNum]
void EmitAnalysisProblemWarnings(FILE *HeaderFile, int LoopIndex); // LoopIndex == -1 indicates main procedure; print warnings if proofs will fail
void EmitSPARKSavedArgs(FILE *BodyFile) const; // Save incoming args as locals to preserve their values
diff --git a/include/base/SMPInstr.h b/include/base/SMPInstr.h
index 76d8cd3457c77c36419e2a83b221bb588945499f..a099b9db63645448243f194bf79b0e2a7dbd0b2f 100644
--- a/include/base/SMPInstr.h
+++ b/include/base/SMPInstr.h
@@ -58,6 +58,10 @@ class SMPProgram;
// Convert unreachable block detected by SCCP into NOPs in binary file.
#define STARS_SCCP_CONVERT_UNREACHABLE_BLOCKS 0
+// Emit SPARK loop and end loop instructions from SMPFunction::EmitSPARKAdaForLoop()
+// as opposed to various places in SMPInstr and SMPFunction.
+#define STARS_SPARK_CENTRALIZE_EMIT_LOOP 1
+
// Value to signal error in computing stack pointer alteration by instruction or RTL.
#define SMP_STACK_DELTA_ERROR_CODE 0xebfaf0fd
// Value to signal that stack pointer is bitwise ANDed to align it; unknown delta that can
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index 78fbfb5dd8a9517fa6b5c989cdbaef6b7c5832e7..1b35f3ae199aa4aefdd9ecaf1a5d67eb6d0ca093 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -2305,8 +2305,10 @@ bool SMPFunction::AnalyzeStackPointerDeltas(void) {
if (0 != (DeltaIncrement % 32)) { // 32 bytes is our alloca fudge increment
SMP_msg("WARNING: DeltaIncrement of %ld not alloca multiple for block %d at %llx\n",
(long)DeltaIncrement, CurrBlock->GetNumber(), (uint64_t) CurrBlock->GetFirstAddr());
+#if SMP_VERBOSE_DEBUG_FUNC
if ((8 >= DeltaIncrement) && (0 <= DeltaIncrement))
this->Dump();
+#endif
}
continue; // Make the loop come around and process this block again, using
// the new incoming delta. Because we do this only when it decreases
@@ -7152,7 +7154,7 @@ void SMPFunction::EmitLoopNestAnnotations(void) {
}
}
return;
-}
+} // end of SMPFunction::EmitLoopNestAnnotations()
// return -1 if no preheader (immediate predecessor that dominates header, has only header as successor)
int SMPFunction::FindLoopPreheaderBlockNum(size_t LoopIndex) const {
@@ -11420,8 +11422,14 @@ bool SMPFunction::AnalyzeCompoundConditionalStatements(void) {
// if (compound condition) then
// do_something;
// endif;
- assert(NFTBlockNum != FTBlockNum); // got to have some code in there somewhere to execute
- if (FTBlockNum == FollowBlockNum) {
+
+ // Compiler optimizations that are not cleaned up can leave worthless branches, e.g.
+ // x86 jle $+2 which goes to the next instruction (2 bytes later) regardless of whether
+ // you take the branch or fall through. This can make the FT and NFT destinations the same.
+ // No need to rearrange code for this junk.
+ bool WorthlessBranch = (NFTBlockNum == FTBlockNum);
+
+ if ((FTBlockNum == FollowBlockNum) && (!WorthlessBranch)) {
// Current structure is:
// if (compound condition) then
// goto NFTBlock;
@@ -11435,7 +11443,7 @@ bool SMPFunction::AnalyzeCompoundConditionalStatements(void) {
// [code here]
// endif;
// FTBlock:
- if (FTBlockNum > NFTBlockNum) { // follow node is IDom of condition node, RPO # is greater than if-else blocks.
+ if (FTBlockNum >= NFTBlockNum) { // follow node is IDom of condition node, RPO # is greater than if-else blocks.
STARSCondExpr *NewExpr = new STARSCondExpr();
NewExpr->SetLeftExpr(CurrExpr, false);
NewExpr->SetOperator(SMP_BITWISE_NOT); // too much trouble to introduce new operator SMP_LOGICAL_NOT
@@ -11825,8 +11833,8 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
}
#endif
- // A similar case to the above is when both branches of an if-then-else flow into a loop header block
- // for a loop that contains both branches.
+ // 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)) {
// See if we can find two blocks, each dominated by HeadBlockNum,
// each being loop tail blocks, with the same loop header block
@@ -11950,9 +11958,33 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
int BlockAlreadySeenCounter = 0;
ThenBlocksSeen.AllocateBits(this->GetNumBlocks());
ElseBlocksSeen.AllocateBits(this->GetNumBlocks());
- int ThenFollowBlockNum = this->TrackConditionalBranchTerminus(HeadBlockNum, ThenBlockNum, ThenBlocksSeen, BlockAlreadySeenCounter);
- BlockAlreadySeenCounter = 0;
- int ElseFollowBlockNum = this->TrackConditionalBranchTerminus(HeadBlockNum, ElseBlockNum, ElseBlocksSeen, BlockAlreadySeenCounter);
+
+ // If the ThenBlock is a loop header block, then the candidate ThenFollowBlock is just
+ // the follow block for that loop. We will probably end up with -1 as our final
+ // return value, as the ElseBlock will produce a different candidate.
+ int ThenFollowBlockNum;
+ SMPBasicBlock *ThenBlock = this->GetBlockByNum(ThenBlockNum);
+ if (ThenBlock->IsLoopHeaderBlock()) {
+ int ThenLoopNum = this->GetLoopNumFromHeaderBlockNum(ThenBlockNum);
+ assert(0 <= ThenLoopNum);
+ assert(((size_t) ThenLoopNum) < this->LoopFollowNodes.size());
+ ThenFollowBlockNum = this->LoopFollowNodes[(size_t) ThenLoopNum];
+ }
+ else {
+ ThenFollowBlockNum = this->TrackConditionalBranchTerminus(HeadBlockNum, ThenBlockNum, ThenBlocksSeen, BlockAlreadySeenCounter);
+ BlockAlreadySeenCounter = 0;
+ }
+ int ElseFollowBlockNum;
+ SMPBasicBlock *ElseBlock = this->GetBlockByNum(ElseBlockNum);
+ if (ElseBlock->IsLoopHeaderBlock()) {
+ int ElseLoopNum = this->GetLoopNumFromHeaderBlockNum(ElseBlockNum);
+ assert(0 <= ElseLoopNum);
+ assert(((size_t) ElseLoopNum) < this->LoopFollowNodes.size());
+ ElseFollowBlockNum = this->LoopFollowNodes[(size_t) ElseLoopNum];
+ }
+ else {
+ ElseFollowBlockNum = this->TrackConditionalBranchTerminus(HeadBlockNum, ElseBlockNum, ElseBlocksSeen, BlockAlreadySeenCounter);
+ }
if ((SMP_BLOCKNUM_UNINIT != ThenFollowBlockNum) && (SMP_BLOCKNUM_UNINIT != ElseFollowBlockNum)) {
// No errors; compute the meet function.
if ((0 <= ThenFollowBlockNum) && (0 <= ElseFollowBlockNum)) {
@@ -11969,7 +12001,7 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
else {
SMP_msg("ERROR: Inconsistent if-else termini block numbers: %d and %d for branch head: %d in func %s\n",
ThenFollowBlockNum, ElseFollowBlockNum, HeadBlockNum, this->GetFuncName());
- FollowBlockNum = SMP_BLOCKNUM_UNINIT; // error signal
+ FollowBlockNum = SMP_BLOCKNUM_UNINIT; // error signal, or branches actually don't meet
}
}
else if (0 <= ThenFollowBlockNum) {
@@ -12229,6 +12261,25 @@ bool SMPFunction::IsSPARKLoopInTranslationStack(void) const {
return FoundLoop;
} // end of SMPFunction::IsSPARKLoopInTranslationStack()
+// Remove duplicate elements in this->SPARKLoopWorkList.
+void SMPFunction::CleanUpSPARKLoopWorkList(void) {
+ STARSBitSet LoopsSeen;
+ LoopsSeen.AllocateBits(this->GetNumLoops());
+ list<pair<int, pair<int, int> > >::iterator WorkIter = this->SPARKLoopWorkList.begin();
+ while (WorkIter != this->SPARKLoopWorkList.end()) {
+ int LoopNum = (*WorkIter).first;
+ if (LoopsSeen.GetBit((size_t)LoopNum)) {
+ WorkIter = this->SPARKLoopWorkList.erase(WorkIter);
+ SMP_msg("SPARK: WARNING: LoopWorkList duplicate removed for loop %d in %s\n", LoopNum, this->GetFuncName());
+ }
+ else {
+ LoopsSeen.SetBit((size_t) LoopNum);
+ ++WorkIter;
+ }
+ }
+ return;
+} // end of SMPFunction::CleanUpSPARKLoopWorkList()
+
// Find memory writes (DEFs) with possible aliases
void SMPFunction::AliasAnalysis2(void) {
// First task: Mark which memory DEFs MIGHT be aliased because an
@@ -19006,6 +19057,7 @@ void SMPFunction::PreProcessForSPARKAdaTranslation(void) {
if (HasLoops && CurrBlock->HasMemoryWrite() && this->IsBlockInAnyLoop((int) BlockNum)) {
for (vector<SMPInstr *>::iterator InstIter = CurrBlock->GetFirstInst(); InstIter != CurrBlock->GetLastInst(); ++InstIter) {
SMPInstr *CurrInst = (*InstIter);
+ STARS_ea_t InstAddr = CurrInst->GetAddr();
STARSOpndTypePtr MemDefOp = CurrInst->GetMemDef();
STARS_ea_t offset;
size_t DataSize;
@@ -19020,10 +19072,25 @@ void SMPFunction::PreProcessForSPARKAdaTranslation(void) {
for (size_t j = 0; j < DataSize; ++j) { // offset has zero-based index into negative offset vectors
for (size_t LoopIndex = 0; LoopIndex < (size_t) this->LoopCount; ++LoopIndex) {
if (this->FuncLoopsByBlock[BlockNum].GetBit(LoopIndex)) {
- if (SignedOffset < 0)
+ bool OutOfRange = (SignedOffset < 0) ? ((offset + j) >= this->NegativeOffsetStackBytesWrittenByLoop[LoopIndex].GetNumBits())
+ : ((SignedOffset + j) >= this->PositiveOffsetStackBytesWrittenByLoop[LoopIndex].GetNumBits());
+ if (OutOfRange) {
+ if (IndexedAccess) {
+ // Index can bring offset back into range. Ignore.
+ SMP_msg("WARNING: SPARK: Imprecise range on indexed access at %llx\n", (uint64_t) InstAddr);
+ continue;
+ }
+ else {
+ SMP_msg("ERROR: SPARK: Imprecise range on non-indexed access at %llx\n", (uint64_t)InstAddr);
+ continue;
+ }
+ }
+ if (SignedOffset < 0) {
this->NegativeOffsetStackBytesWrittenByLoop[LoopIndex].SetBit(offset + j);
- else
+ }
+ else {
this->PositiveOffsetStackBytesWrittenByLoop[LoopIndex].SetBit(SignedOffset + j);
+ }
}
} // end for all loops
} // end for all bytes in DataSize of current stack write
@@ -20101,6 +20168,7 @@ void SMPFunction::EmitIncomingLoopRegExprs(FILE *OutputFile, size_t LoopNum, boo
SMP_fprintf(OutputFile, "))");
}
} // end for all this->LoopRegSourceExprPairs[LoopNum]
+ return;
} // end of SMPFunction::EmitIncomingLoopRegExprs()
// Emit Assumes and Loop_Invariants for loop BIV and mem ranges.
@@ -20116,8 +20184,6 @@ void SMPFunction::EmitSPARKLoopBIVLimits(FILE *BodyFile, STARS_ea_t LoopAddr, si
bool SPRelative = false;
STARSExpression *LowerLimitExpr = nullptr;
- PrintSPARKIndentTabs(BodyFile);
-
if (PragmaAssume) {
// Emit pragma Assume(lower_bound < upper_bound);
STARSExpression *UpperLimitExpr = nullptr;
@@ -20139,6 +20205,7 @@ void SMPFunction::EmitSPARKLoopBIVLimits(FILE *BodyFile, STARS_ea_t LoopAddr, si
// No point in an Assume on two constants
if (!BothConstExprs) {
SPRelative = LowerLimitExpr->IsStackPtrRegUsed();
+ PrintSPARKIndentTabs(BodyFile);
SMP_fprintf(BodyFile, "pragma Assume(");
if (SPRelative) {
SMP_fprintf(BodyFile, "( ");
@@ -21896,6 +21963,7 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FIL
pair<int, int> BlockItem(CurrBlockNum, ResumeBlockNum);
pair<int, pair<int, int> > WorkListItem(LoopNum, BlockItem);
this->SPARKLoopWorkList.push_back(WorkListItem);
+ this->CleanUpSPARKLoopWorkList();
}
}
else if (CurrBlock->IsLoopTailBlock()) {
@@ -21916,9 +21984,13 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FIL
SPARKTranslationCFType CurrentCFType = this->SPARKControlStack.back();
if (SPARK_LOOP == CurrentCFType) {
// Must be called from EmitSPARKAdaForLoop(); time for "end loop;" without "end if;"
+#if STARS_SPARK_CENTRALIZE_EMIT_LOOP
+ ;
+#else
--STARS_SPARK_IndentCount;
PrintSPARKIndentTabs(SPARKBodyFile);
SMP_fprintf(SPARKBodyFile, "end loop;\n\n");
+#endif
LastInst->SetSPARKTranslated();
}
else if (SPARK_ELSE_CLAUSE == CurrentCFType) {
@@ -21926,9 +21998,13 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FIL
--STARS_SPARK_IndentCount;
PrintSPARKIndentTabs(SPARKBodyFile);
SMP_fprintf(SPARKBodyFile, "end if;\n\n");
+#if STARS_SPARK_CENTRALIZE_EMIT_LOOP
+ ;
+#else
--STARS_SPARK_IndentCount;
PrintSPARKIndentTabs(SPARKBodyFile);
SMP_fprintf(SPARKBodyFile, "end loop;\n\n");
+#endif
LastInst->SetSPARKTranslated();
}
else { // mysterious
@@ -22052,6 +22128,7 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FIL
pair<int, int> BlockItem(NextBlockNum, ResumeBlockNum);
pair<int, pair<int, int> > WorkListItem(LoopNum, BlockItem);
this->SPARKLoopWorkList.push_back(WorkListItem);
+ this->CleanUpSPARKLoopWorkList();
}
}
else if ((JUMP_TO_DEFAULT_CASE == LastCFType) || (JUMP_TO_SWITCH_INDIR_JUMP == LastCFType)) {
@@ -22120,9 +22197,21 @@ void SMPFunction::EmitSPARKAdaForLoop(int HeaderBlockNum, int FollowBlockNum, FI
if (HeaderBlockNum == FollowBlockNum)
return; // end recursion if Follow Block is seen
+ assert(0 <= HeaderBlockNum);
int CurrBlockNum = HeaderBlockNum;
int ResumeBlockNum = FollowBlockNum;
this->SPARKControlStack.push_back(SPARK_LOOP);
+ SMPBasicBlock *HeaderBlock = this->GetBlockByNum((size_t) HeaderBlockNum);
+ STARS_ea_t FirstAddr = HeaderBlock->GetFirstNonMarkerAddr();
+ assert(STARS_BADADDR != FirstAddr);
+ SMPInstr *FirstInst = *(HeaderBlock->GetInstIterFromAddr(FirstAddr));
+#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);
+#endif
while ((CurrBlockNum != FollowBlockNum) && (CurrBlockNum >= 0)) {
assert((0 <= CurrBlockNum) && (CurrBlockNum < (int)this->RPOBlocks.size()));
@@ -22145,6 +22234,7 @@ void SMPFunction::EmitSPARKAdaForLoop(int HeaderBlockNum, int FollowBlockNum, FI
pair<int, int> BlockItem(CurrBlockNum, ResumeBlockNum);
pair<int, pair<int, int> > WorkListItem(LoopNum, BlockItem);
this->SPARKLoopWorkList.push_back(WorkListItem);
+ this->CleanUpSPARKLoopWorkList();
}
else if (CurrBlock->IsLoopTailBlock()) {
// We are at the end of a recursive descent into a loop. Translate the block and return.
@@ -22251,6 +22341,7 @@ void SMPFunction::EmitSPARKAdaForLoop(int HeaderBlockNum, int FollowBlockNum, FI
pair<int, int> BlockItem(NextBlockNum, ResumeBlockNum);
pair<int, pair<int, int> > WorkListItem(LoopNum, BlockItem);
this->SPARKLoopWorkList.push_back(WorkListItem);
+ this->CleanUpSPARKLoopWorkList();
}
else if ((JUMP_TO_DEFAULT_CASE == LastCFType) || (JUMP_TO_SWITCH_INDIR_JUMP == LastCFType)) {
; // jump to default case is not translated directly; ditto for jump around default case to INDIR_JUMP
@@ -22295,6 +22386,13 @@ void SMPFunction::EmitSPARKAdaForLoop(int HeaderBlockNum, int FollowBlockNum, FI
} // end while CurrBlockNum is in the loop
this->SPARKControlStack.pop_back();
+
+#if STARS_SPARK_CENTRALIZE_EMIT_LOOP
+ // We want to print "end loop;" and decrease indentation.
+ --STARS_SPARK_IndentCount;
+ PrintSPARKIndentTabs(SPARKBodyFile);
+ SMP_fprintf(SPARKBodyFile, "end loop;\n");
+#endif
return;
} // end of SMPFunction::EmitSPARKAdaForLoop()
@@ -22446,6 +22544,7 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
pair<int, int> BlockItem(CurrBlockNum, FollowBlockNum);
pair<int, pair<int, int> > WorkListItem(LoopNum, BlockItem);
this->SPARKLoopWorkList.push_back(WorkListItem);
+ this->CleanUpSPARKLoopWorkList();
--STARS_SPARK_IndentCount;
PrintSPARKIndentTabs(SPARKBodyFile);
@@ -22617,9 +22716,13 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
SMP_msg("INFO: SPARK: Not emitting end if for guarded conditional at %llx due to InvertedLoopExitCase\n",
(uint64_t) LastAddr);
if (UnknownFollowBlock) { // odd case of falling into header block loop-back
+#if STARS_SPARK_CENTRALIZE_EMIT_LOOP
+ ;
+#else
--STARS_SPARK_IndentCount;
PrintSPARKIndentTabs(SPARKBodyFile);
- SMP_fprintf(SPARKBodyFile, "end loop;\n");
+ SMP_fprintf(SPARKBodyFile, "end loop;\n\n");
+#endif
}
}
diff --git a/src/base/SMPInstr.cpp b/src/base/SMPInstr.cpp
index 2a7a371da2d4c001d70f1cd08f0b644799b7bab1..26d6fe2038b625fa0aecf299a19abb774352f7a8 100644
--- a/src/base/SMPInstr.cpp
+++ b/src/base/SMPInstr.cpp
@@ -6915,6 +6915,9 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
} while (NestingDepth > 0);
}
#endif
+#if STARS_SPARK_CENTRALIZE_EMIT_LOOP
+ ;
+#else
if (this->GetBlock()->IsLoopHeaderBlock()) {
// We want to print "loop" and increase indentation.
PrintSPARKIndentTabs(OutFile);
@@ -6922,6 +6925,7 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
++STARS_SPARK_IndentCount;
this->EmitSPARKAdaLoopInvariants(OutFile);
}
+#endif
}
ControlFlowType FuncControlFlowType;
@@ -6968,9 +6972,13 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
else if (LOOP_BACK == FuncControlFlowType) {
// We must be looping back to the loop header.
if (JUMP == CurrDataFlowType) { // simple case
+#if STARS_SPARK_CENTRALIZE_EMIT_LOOP
+ ;
+#else
--STARS_SPARK_IndentCount;
PrintSPARKIndentTabs(OutFile);
SMP_fprintf(OutFile, "end loop;\n\n");
+#endif
}
else { // conditionally loops back, might fall out of loop if condition is false.
// We want to invert the condition and exit on the inverted condition, then fall through
@@ -6985,9 +6993,13 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
// are ready for "end loop;" but in the header block case we need to fall through into
// the second block of the loop.
if (this->GetBlock()->IsLoopTailBlock()) {
+#if STARS_SPARK_CENTRALIZE_EMIT_LOOP
+ ;
+#else
--STARS_SPARK_IndentCount;
PrintSPARKIndentTabs(OutFile);
SMP_fprintf(OutFile, "end loop;\n\n");
+#endif
}
else {
assert(this->GetBlock()->IsOptimizedTopLoopTest());
@@ -7014,9 +7026,13 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
// exit when [condition];
// end loop;
if (this->GetBlock()->IsLoopTailBlock()) {
+#if STARS_SPARK_CENTRALIZE_EMIT_LOOP
+ ;
+#else
--STARS_SPARK_IndentCount;
PrintSPARKIndentTabs(OutFile);
SMP_fprintf(OutFile, "end loop;\n\n");
+#endif
}
}
else if (CASE_BREAK_TO_FOLLOW_NODE == FuncControlFlowType) {
@@ -7076,9 +7092,13 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
// exit when [condition];
// end loop;
if (this->GetBlock()->IsLoopTailBlock()) {
+#if STARS_SPARK_CENTRALIZE_EMIT_LOOP
+ ;
+#else
--STARS_SPARK_IndentCount;
PrintSPARKIndentTabs(OutFile);
SMP_fprintf(OutFile, "end loop;\n\n");
+#endif
}
}
++STARS_SPARK_IndentCount;
@@ -7328,9 +7348,13 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
} // end if (special cases) ... else ... most insts
bool DoubleTailBlock = false;
if (this->IsLastInstInOptimizedLoop(DoubleTailBlock)) {
+#if STARS_SPARK_CENTRALIZE_EMIT_LOOP
+ ;
+#else
--STARS_SPARK_IndentCount;
PrintSPARKIndentTabs(OutFile);
SMP_fprintf(OutFile, "end loop;\n\n");
+#endif
if (DoubleTailBlock) { // end the outer loop also
--STARS_SPARK_IndentCount;
PrintSPARKIndentTabs(OutFile);
diff --git a/src/base/SMPProgram.cpp b/src/base/SMPProgram.cpp
index 6dfa97f5512170b08b0c11e20d7ee17d948a37d2..85509a29baf2b48982bf3ec5af7d153370de002d 100644
--- a/src/base/SMPProgram.cpp
+++ b/src/base/SMPProgram.cpp
@@ -811,7 +811,7 @@ void SMPProgram::Analyze(ProfilerInformation *pi, FILE *AnnotFile, FILE *InfoAnn
EndTime = time(nullptr);
TimeDiff = difftime(EndTime, StartTime);
- SMP_msg("INFO: TIME: Phase 6: MetaData+InferTypes+InferFG: %7.2f InOutRegs: %7.2f UnsafeCallees: %7.2f Metadata: %7.2f InferTypes: %7.2f InferFG: %7.2f\n",
+ SMP_msg("INFO: TIME: Phase 6: MetaData+InferTypes+InferFG: %7.2f SPARKInOutRegs: %7.2f UnsafeCallees: %7.2f Metadata: %7.2f InferTypes: %7.2f InferFG: %7.2f\n",
TimeDiff, Analysis1, Analysis2, Analysis3, Analysis4, Analysis5);
SMP_msg("INFO: VMEM: Phase 6: Maximum resident memory usage in MB: %ld \n", global_stars_interface->GetMemoryInUse());
@@ -933,7 +933,7 @@ void SMPProgram::Analyze(ProfilerInformation *pi, FILE *AnnotFile, FILE *InfoAnn
SMP_msg("INFO: VMEM: Phase 7C: Maximum resident memory usage in MB: %ld \n", global_stars_interface->GetMemoryInUse());
}
- // Free memory not needed to emit annotations, now that type inference is done.
+ // Free memory that is not needed to emit annotations, now that type inference is done.
for (FuncListIter = this->PrioritizedFuncList.begin(); FuncListIter != this->PrioritizedFuncList.end(); ++FuncListIter) {
CurrFunc = (*FuncListIter);
CurrFunc->FreeUnusedMemory4();
@@ -1091,6 +1091,10 @@ bool SMPProgram::EmitProgramSPARKAda(void) {
string PackageName = global_STARS_program->GetAdaPackageName();
+ time_t Time1, Time2, StartTime, EndTime;
+ double TimeDiff1 = 0.0, TimeDiff2 = 0.0;
+ StartTime = time(nullptr);
+
// Emit the package body.
SMP_fprintf(BodyFile, "Package body %s\n", PackageName.c_str());
SMP_fprintf(BodyFile, "with SPARK_Mode \nis\n\n");
@@ -1114,6 +1118,7 @@ bool SMPProgram::EmitProgramSPARKAda(void) {
TempFunc->PreProcessForSPARKAdaTranslation();
}
} // end for all functions
+ Time1 = time(nullptr);
#if 0 // Use C_Library package instead
// Emit procedure specifications and bodies for library functions
@@ -1173,6 +1178,12 @@ bool SMPProgram::EmitProgramSPARKAda(void) {
SMP_fprintf(BodyFile, "\nend %s;\n", PackageName.c_str());
SMP_fprintf(SpecFile, "\nend %s;\n", PackageName.c_str());
+ EndTime = time(nullptr);
+ TimeDiff1 = difftime(Time1, StartTime);
+ TimeDiff2 = difftime(EndTime, StartTime);
+ SMP_msg("INFO: TIME: Phase 9: EmitSPARK: %7.2f Preprocess: %7.2f\n", TimeDiff2, TimeDiff1);
+ SMP_msg("INFO: VMEM: Phase 9: Maximum resident memory usage in MB: %ld \n", global_stars_interface->GetMemoryInUse());
+
return true;
} // end of SMPProgram::EmitProgramSPARKAda()
@@ -1197,16 +1208,13 @@ void SMPProgram::EmitAnnotations(FILE *AnnotFile, FILE *InfoAnnotFile) {
TotalUnsafeBlocks += TempFunc->GetUnsafeBlocks();
} // end for all functions
- if (global_STARS_program->ShouldSTARSTranslateToSPARKAda()) {
- (void) this->EmitProgramSPARKAda();
- }
-
EndTime = time(nullptr);
double TimeDiff = difftime(EndTime, StartTime);
SMP_msg("INFO: TIME: Phase 8: EmitAnnotations: %7.2f\n", TimeDiff);
SMP_msg("INFO: VMEM: Phase 8: Maximum resident memory usage in MB: %ld \n", global_stars_interface->GetMemoryInUse());
if (global_STARS_program->ShouldSTARSTranslateToSPARKAda()) {
+ (void) this->EmitProgramSPARKAda();
SMP_msg("SPARK: Total subword registers translated: %lu\n", SubwordRegCount);
SMP_msg("SPARK: Total subword memory accesses translated: %lu\n", SubwordMemCount);
SMP_msg("SPARK: Total subword address registers translated: %lu\n", SubwordAddressRegCount);