diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index 1c5aeb1e992cd227a1da4ce4116c3d4026cea26d..cfb8550df630d0103533031ed2e85646726d461e 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -10966,7 +10966,7 @@ void SMPFunction::FindSwitchIDom(struct SwitchTableInfo &TableInfo) {
// We need to find the IDom of all blocks that jump to the default case, if any, and
// then the IDom of {that IDom and the indir jump block}.
if (TableInfo.DefaultJumpAddr == STARS_BADADDR) {
- // Simplest case: No default cases, no blocks jump to a default case, so INDIR_JUMP block is IDom
+ // Simplest case: No default cases, no prior blocks jump to a default case, so INDIR_JUMP block is IDom
// for the whole switch statement.
TableInfo.IDomBlockNum = TableInfo.IndirJumpBlockNum;
}
@@ -10982,8 +10982,26 @@ void SMPFunction::FindSwitchIDom(struct SwitchTableInfo &TableInfo) {
SMPInstr *LastInst = (*(--PredBlock->GetLastInst()));
assert(nullptr != LastInst);
SMPitype FlowType = LastInst->GetDataFlowType();
- if ((COND_BRANCH == FlowType) || (JUMP == FlowType)) {
- this->SetControlFlowType(LastInst->GetAddr(), JUMP_TO_DEFAULT_CASE);
+ STARS_ea_t LastAddr = LastInst->GetAddr();
+ if (JUMP == FlowType) {
+ this->SetControlFlowType(LastAddr, JUMP_TO_DEFAULT_CASE);
+ }
+ else if (COND_BRANCH == FlowType) {
+ // Detect the inverted case, in which a COND_BRANCH falls through to the default case
+ // and branches to the indirect jump block.
+ int TargetBlockNum = PredBlock->GetCondNonFallThroughSuccBlockNum();
+ if (TableInfo.DefaultCaseBlockNum == TargetBlockNum) {
+ this->SetControlFlowType(LastAddr, JUMP_TO_DEFAULT_CASE);
+ }
+ else if (TableInfo.IndirJumpBlockNum == TargetBlockNum) {
+ this->SetControlFlowType(LastAddr, JUMP_TO_SWITCH_INDIR_JUMP);
+ }
+ else {
+ // Not sure what is going on.
+ SMP_msg("ERROR: SPARK: Unstructured due to switch control flow at %llx in %s\n",
+ (uint64_t)LastAddr, this->GetFuncName());
+ this->HasStructuredCFG = false;
+ }
}
else if ((INDIR_JUMP == FlowType) && (PredBlock->GetNumber() == TableInfo.IndirJumpBlockNum)) {
// skip over switch table jumps to the default case
@@ -22512,10 +22530,12 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FIL
}
else if (FlowType == COND_BRANCH) {
if (LastCFType == JUMP_TO_SWITCH_INDIR_JUMP) {
- // conditional branch to INDIR_JUMP is not well-structured; should not occur
- SMP_msg("FATAL ERROR: COND_BRANCH of type JUMP_TO_SWITCH_INDIR_JUMP at %llx\n",
- (unsigned long long) LastAddr);
- assert(LastCFType != JUMP_TO_SWITCH_INDIR_JUMP);
+ // Should fall through to default case block. Resume translation there,
+ // which will cause use to emit the entire switch statement.
+ list<SMPBasicBlock *>::const_iterator FallThroughIter = CurrBlock->GetFallThroughSucc();
+ assert(FallThroughIter != CurrBlock->GetLastConstSucc()); // COND_BRANCH always has a fall-through
+ ResumeBlockNum = (*FallThroughIter)->GetNumber();
+ LastInst->SetSPARKTranslated();
}
else if (LastCFType == JUMP_TO_DEFAULT_CASE) {
// jump to default case is not translated directly
@@ -22796,7 +22816,7 @@ void SMPFunction::EmitSPARKAdaForLoop(int HeaderBlockNum, int FollowBlockNum, FI
list<SMPBasicBlock *>::const_iterator FallThroughIter = CurrBlock->GetFallThroughSucc();
assert(FallThroughIter != CurrBlock->GetLastConstSucc()); // COND_BRANCH always has a fall-through
ResumeBlockNum = (*FallThroughIter)->GetNumber();
- LastInst->SetSPARKTranslated();
+ LastInst->SetSPARKTranslated(); // Ada "others ==>" clause subsumes all COND_BRANCHes to default case.
}
}
else if (FlowType == JUMP) {
@@ -22883,6 +22903,7 @@ void SMPFunction::EmitSPARKAdaForSwitch(int HeaderBlockNum, int FollowBlockNum,
size_t SwitchIndex;
SMPInstr *LastInst;
+ STARS_ea_t LastAddr;
if (HeaderBlock->IsSwitchDefaultCase()) {
// Encountered default case first, but we want to emit Ada code for it last.
STARS_ea_t DefaultCaseAddr = HeaderBlock->GetFirstAddr();
@@ -22891,12 +22912,13 @@ void SMPFunction::EmitSPARKAdaForSwitch(int HeaderBlockNum, int FollowBlockNum,
HeaderBlock = this->GetBlockByNum(this->SwitchInfoArray[SwitchIndex].IndirJumpBlockNum);
assert(nullptr != HeaderBlock);
LastInst = (*(--(HeaderBlock->GetLastInst())));
+ LastAddr = LastInst->GetAddr();
}
else {
vector<SMPInstr *>::iterator LastInstIter = --(HeaderBlock->GetLastInst());
LastInst = (*LastInstIter);
- STARS_ea_t LastAddr = LastInst->GetAddr();
+ LastAddr = LastInst->GetAddr();
SMPitype FlowType = LastInst->GetDataFlowType();
assert(FlowType == INDIR_JUMP);
map<STARS_ea_t, size_t>::iterator MapIter = this->SwitchJumpMap.find(LastAddr);
@@ -22915,7 +22937,20 @@ void SMPFunction::EmitSPARKAdaForSwitch(int HeaderBlockNum, int FollowBlockNum,
int NextFollowBlockNum = TableInfo.FollowNodeNum;
assert(NextFollowBlockNum == FollowBlockNum);
// Emit Ada case statement.
- LastInst->EmitSPARKAda(SPARKBodyFile); // INDIR_JUMP is handled here
+ STARS_ea_t FirstInstAddr = HeaderBlock->GetFirstNonMarkerAddr();
+ if (FirstInstAddr != LastAddr) { // Might have untranslated insts before INDIR_JUMP
+ SMPInstr *FirstInst = this->GetInstFromAddr(FirstInstAddr);
+ if (!FirstInst->HasBeenTranslatedToSPARK()) {
+ HeaderBlock->EmitSPARKAdaForAllInsts(SPARKBodyFile);
+ }
+ else {
+ LastInst->EmitSPARKAda(SPARKBodyFile); // INDIR_JUMP is handled here
+ }
+ }
+ else {
+ LastInst->EmitSPARKAda(SPARKBodyFile); // INDIR_JUMP is handled here
+ }
+ HeaderBlock->SetProcessed(true);
// Loop through jump table, emitting code for each case.
assert(!TableInfo.CaseBlockNums.empty());
for (size_t CaseIndex = 0; CaseIndex < TableInfo.CaseBlockNums.size(); ++CaseIndex) {
diff --git a/src/base/SMPInstr.cpp b/src/base/SMPInstr.cpp
index b94aa3822c3c0b1df477feb232ce8d1f4e1662c4..f6fcc0a0fe1072cd546743596af7e3ffe80ca05b 100644
--- a/src/base/SMPInstr.cpp
+++ b/src/base/SMPInstr.cpp
@@ -6981,303 +6981,306 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
}
switch (CurrDataFlowType) {
- case DEFAULT:
- case LABEL:
- case CASE:
- PrintOperands = true;
- break;
+ case DEFAULT:
+ case LABEL:
+ case CASE:
+ PrintOperands = true;
+ break;
- case JUMP:
- case COND_BRANCH:
- // Special case first: a call instruction within a function, used as a jump
- // (perhaps as an internal thunk).
- if (this->IsCallUsedAsJump()) {
- // We need to translate the implicit push of the return address before falling through
- // to the jump translation.
- NextAddr = InstAddr + (STARS_ea_t) this->GetSize();
+ case JUMP:
+ case COND_BRANCH:
+ // Special case first: a call instruction within a function, used as a jump
+ // (perhaps as an internal thunk).
+ if (this->IsCallUsedAsJump()) {
+ // We need to translate the implicit push of the return address before falling through
+ // to the jump translation.
+ NextAddr = InstAddr + (STARS_ea_t) this->GetSize();
+ PrintSPARKIndentTabs(OutFile);
+ // Comment out memory write of return address to speed up prover.
+ SMP_fprintf(OutFile, " -- X86.WriteMem%d(Unsigned%d(X86.RSP - %d), 16#%llx# );\n", STARS_ISA_Bitwidth, STARS_ISA_Bitwidth,
+ global_STARS_program->GetSTARS_ISA_Bytewidth(), (unsigned long long) NextAddr);
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, " X86.RSP := X86.RSP - %d;\n", global_STARS_program->GetSTARS_ISA_Bytewidth());
+ }
+ // Detect loop-related control flow first, then simple if-else control flow otherwise.
+ FuncControlFlowType = this->GetBlock()->GetFunc()->GetControlFlowType(InstAddr);
+ if (FALL_THROUGH == FuncControlFlowType) {
+ if (COND_BRANCH == CurrDataFlowType) {
+ SMP_fprintf(OutFile, "ERROR: Jump instruction of unknown control flow.\n");
+ }
+ else { // JUMP
PrintSPARKIndentTabs(OutFile);
- // Comment out memory write of return address to speed up prover.
- SMP_fprintf(OutFile, " -- X86.WriteMem%d(Unsigned%d(X86.RSP - %d), 16#%llx# );\n", STARS_ISA_Bitwidth, STARS_ISA_Bitwidth,
- global_STARS_program->GetSTARS_ISA_Bytewidth(), (unsigned long long) NextAddr);
+ SMP_fprintf(OutFile, "null;\n");
+ ; // jumps around else clauses are handled in SMPFunction::EmitSPARKAdaForConditional()
+ }
+ }
+ else if ((LOOP_BACK == FuncControlFlowType) || (INVERTED_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, " X86.RSP := X86.RSP - %d;\n", global_STARS_program->GetSTARS_ISA_Bytewidth());
+ SMP_fprintf(OutFile, "end loop;\n\n");
+#endif
}
- // Detect loop-related control flow first, then simple if-else control flow otherwise.
- FuncControlFlowType = this->GetBlock()->GetFunc()->GetControlFlowType(InstAddr);
- if (FALL_THROUGH == FuncControlFlowType) {
- if (COND_BRANCH == CurrDataFlowType) {
- SMP_fprintf(OutFile, "ERROR: Jump instruction of unknown control flow.\n");
- }
- else { // JUMP
+ else { // conditionally loops back, might fall out of loop if condition is false.
+ bool StaysInLoop = this->GetBlock()->GetFunc()->IsNonExitingLoopBackBranch(InstAddr);
+ if (StaysInLoop) {
+ // Code has been analyzed to ensure this is not a LOOP_CONTINUE case, so it is safe
+ // to enclose the rest of the code branch inside an if-then by inverting the LOOP_BACK
+ // condition.
PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, "null;\n");
- ; // jumps around else clauses are handled in SMPFunction::EmitSPARKAdaForConditional()
+ SMP_fprintf(OutFile, "if ");
+ this->MDEmitSPARKAdaInvertedCondition(OutFile);
+ SMP_fprintf(OutFile, " then \n");
+ ++STARS_SPARK_IndentCount;
}
- }
- else if ((LOOP_BACK == FuncControlFlowType) || (INVERTED_LOOP_BACK == FuncControlFlowType)) {
- // We must be looping back to the loop header.
- if (JUMP == CurrDataFlowType) { // simple case
+ 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");
+ // 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
+ // 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 { // conditionally loops back, might fall out of loop if condition is false.
- bool StaysInLoop = this->GetBlock()->GetFunc()->IsNonExitingLoopBackBranch(InstAddr);
- if (StaysInLoop) {
- // Code has been analyzed to ensure this is not a LOOP_CONTINUE case, so it is safe
- // to enclose the rest of the code branch inside an if-then by inverting the LOOP_BACK
- // condition.
+ --STARS_SPARK_IndentCount;
PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, "if ");
- this->MDEmitSPARKAdaInvertedCondition(OutFile);
- SMP_fprintf(OutFile, " then \n");
- ++STARS_SPARK_IndentCount;
+ SMP_fprintf(OutFile, "end loop;\n\n");
+#endif
}
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");
- // 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
- // 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());
- assert(this->GetBlock()->IsLoopHeaderBlock());
- }
+ assert(this->GetBlock()->IsOptimizedTopLoopTest());
+ assert(this->GetBlock()->IsLoopHeaderBlock());
}
}
}
- else if ((LOOP_EXIT == FuncControlFlowType) || (INVERTED_LOOP_EXIT == FuncControlFlowType)) {
- PrintSPARKIndentTabs(OutFile);
- if (JUMP == CurrDataFlowType) {
- 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");
- }
- // Check for bottom-testing loop case where we have:
- // loop
- // [instructions]
- // exit when [condition];
- // end loop;
- if (this->GetBlock()->IsLoopTailBlock()) {
+ }
+ else if ((LOOP_EXIT == FuncControlFlowType) || (INVERTED_LOOP_EXIT == FuncControlFlowType)) {
+ PrintSPARKIndentTabs(OutFile);
+ if (JUMP == CurrDataFlowType) {
+ 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");
+ }
+ // Check for bottom-testing loop case where we have:
+ // loop
+ // [instructions]
+ // 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) {
- ; // No Ada translation; next "when" keyword starts new case with implicit jump before it
- }
- else if (JUMP_TO_DEFAULT_CASE == FuncControlFlowType) {
- ; // No Ada translation; the "others" keyword grabs all default case values
- }
- else if ((BRANCH_IF_THEN == FuncControlFlowType) || (BRANCH_IF_THEN_ELSE == FuncControlFlowType)) {
- // ASM looks like:
- // test or compare to set condition codes
- // conditionally jump around the code in the if-then
- // We want SPARK Ada:
- // if (negated condition) then
- // EXCEPTION: An odd case for if-then is to branch to the then-block, which jumps back to the follow-block.
- // In this odd case, we do not invert the condition:
- // if (cond) goto then-code
- // L1: follow-block
- // code fragment elsewhere: then-code
- // goto L1
- // This needs to translate to:
- // if (cond) then ; do not invert the condition
- // then-code
- // endif
- // This odd case is detected by noticing that the fall-through block has more than 1 predecessor (the extra
- // predecessor is the unconditional jump from the then-code to it).
- bool OddIfThenCase = this->IsOddIfThenCase();
+ --STARS_SPARK_IndentCount;
PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, "if ");
- if (!OddIfThenCase) {
- this->MDEmitSPARKAdaInvertedCondition(OutFile);
- }
- else {
- this->MDEmitSPARKAdaCondition(OutFile);
- }
- SMP_fprintf(OutFile, " then \n");
- ++STARS_SPARK_IndentCount;
+ SMP_fprintf(OutFile, "end loop;\n\n");
+#endif
}
- else if ((SHORT_CIRCUIT_BRANCH == FuncControlFlowType) || (SHORT_CIRCUIT_LOOP_EXIT == FuncControlFlowType)) {
- // Multiple short circuit condition branches have been coalesced together.
- STARSCFGBlock *CurrCFGBlock = this->GetBlock()->GetFunc()->GetCFGBlockByNum((size_t) this->GetBlock()->GetNumber());
- assert(nullptr != CurrCFGBlock);
- if (!CurrCFGBlock->IsCoalesced()) { // must be header block of compound conditional; header block is where we emit output
- PrintSPARKIndentTabs(OutFile);
- if (SHORT_CIRCUIT_BRANCH == FuncControlFlowType) {
- SMP_fprintf(OutFile, "if not (");
- 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");
- // Check for bottom-testing loop case where we have:
- // loop
- // [instructions]
- // exit when [condition];
- // end loop;
- if (this->GetBlock()->IsLoopTailBlock()) {
+ }
+ else if (CASE_BREAK_TO_FOLLOW_NODE == FuncControlFlowType) {
+ ; // No Ada translation; next "when" keyword starts new case with implicit jump before it
+ }
+ else if (JUMP_TO_DEFAULT_CASE == FuncControlFlowType) {
+ ; // No Ada translation; the "others" keyword grabs all default case values
+ }
+ else if (JUMP_TO_SWITCH_INDIR_JUMP == FuncControlFlowType) {
+ ; // Inverted case; falls through to default block. No Ada translation. ????
+ }
+ else if ((BRANCH_IF_THEN == FuncControlFlowType) || (BRANCH_IF_THEN_ELSE == FuncControlFlowType)) {
+ // ASM looks like:
+ // test or compare to set condition codes
+ // conditionally jump around the code in the if-then
+ // We want SPARK Ada:
+ // if (negated condition) then
+ // EXCEPTION: An odd case for if-then is to branch to the then-block, which jumps back to the follow-block.
+ // In this odd case, we do not invert the condition:
+ // if (cond) goto then-code
+ // L1: follow-block
+ // code fragment elsewhere: then-code
+ // goto L1
+ // This needs to translate to:
+ // if (cond) then ; do not invert the condition
+ // then-code
+ // endif
+ // This odd case is detected by noticing that the fall-through block has more than 1 predecessor (the extra
+ // predecessor is the unconditional jump from the then-code to it).
+ bool OddIfThenCase = this->IsOddIfThenCase();
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "if ");
+ if (!OddIfThenCase) {
+ this->MDEmitSPARKAdaInvertedCondition(OutFile);
+ }
+ else {
+ this->MDEmitSPARKAdaCondition(OutFile);
+ }
+ SMP_fprintf(OutFile, " then \n");
+ ++STARS_SPARK_IndentCount;
+ }
+ else if ((SHORT_CIRCUIT_BRANCH == FuncControlFlowType) || (SHORT_CIRCUIT_LOOP_EXIT == FuncControlFlowType)) {
+ // Multiple short circuit condition branches have been coalesced together.
+ STARSCFGBlock *CurrCFGBlock = this->GetBlock()->GetFunc()->GetCFGBlockByNum((size_t) this->GetBlock()->GetNumber());
+ assert(nullptr != CurrCFGBlock);
+ if (!CurrCFGBlock->IsCoalesced()) { // must be header block of compound conditional; header block is where we emit output
+ PrintSPARKIndentTabs(OutFile);
+ if (SHORT_CIRCUIT_BRANCH == FuncControlFlowType) {
+ SMP_fprintf(OutFile, "if not (");
+ 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");
+ // Check for bottom-testing loop case where we have:
+ // loop
+ // [instructions]
+ // 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");
+ --STARS_SPARK_IndentCount;
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "end loop;\n\n");
#endif
- }
}
- ++STARS_SPARK_IndentCount;
}
- }
-#if 0
- else if (JUMP_BEFORE_ELSE == FuncControlFlowType) {
- // ASM looks like:
- // unconditional jump around the else block to the follow block
- // We want to print SPARK Ada:
- // else
- // Then we want to increment the counter of jumps to the follow node.
- --STARS_SPARK_IndentCount;
- PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, "else\n");
- ++STARS_SPARK_IndentCount;
- this->GetBlock()->GetFunc()->IncrementJumpToFollowNodeCounter(InstAddr);
- }
- else if (JUMP_BEFORE_ELSIF == FuncControlFlowType) {
- // ASM looks like:
- // unconditional jump around the rest of the if-then-elsif-elsif-...-else structure to the follow node.
- // Currently, we treat this the same as JUMP_BEFORE_ELSE. We might pretty it up in the future.
- --STARS_SPARK_IndentCount;
- PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, "else\n");
++STARS_SPARK_IndentCount;
- this->GetBlock()->GetFunc()->IncrementJumpToFollowNodeCounter(InstAddr);
}
+ }
+#if 0
+ else if (JUMP_BEFORE_ELSE == FuncControlFlowType) {
+ // ASM looks like:
+ // unconditional jump around the else block to the follow block
+ // We want to print SPARK Ada:
+ // else
+ // Then we want to increment the counter of jumps to the follow node.
+ --STARS_SPARK_IndentCount;
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "else\n");
+ ++STARS_SPARK_IndentCount;
+ this->GetBlock()->GetFunc()->IncrementJumpToFollowNodeCounter(InstAddr);
+ }
+ else if (JUMP_BEFORE_ELSIF == FuncControlFlowType) {
+ // ASM looks like:
+ // unconditional jump around the rest of the if-then-elsif-elsif-...-else structure to the follow node.
+ // Currently, we treat this the same as JUMP_BEFORE_ELSE. We might pretty it up in the future.
+ --STARS_SPARK_IndentCount;
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "else\n");
+ ++STARS_SPARK_IndentCount;
+ this->GetBlock()->GetFunc()->IncrementJumpToFollowNodeCounter(InstAddr);
+ }
#endif
- else {
- SMP_fprintf(OutFile, "ERROR: Jump instruction of unknown control flow.\n");
- }
+ else {
+ SMP_fprintf(OutFile, "ERROR: Jump instruction of unknown control flow.\n");
+ }
- break;
+ break;
- case INDIR_JUMP:
- // Start switch table translation.
- PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, "case ");
- this->PrintSPARKAdaOperand(this->RTL.GetRT(0)->GetConstRightOperandNoNorm(), OutFile, false, UseFP, true, false);
- SMP_fprintf(OutFile, " is\n");
- ++STARS_SPARK_IndentCount;
- break;
+ case INDIR_JUMP:
+ // Start switch table translation.
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "case ");
+ this->PrintSPARKAdaOperand(this->RTL.GetRT(0)->GetConstRightOperandNoNorm(), OutFile, false, UseFP, true, false);
+ SMP_fprintf(OutFile, " is\n");
+ ++STARS_SPARK_IndentCount;
+ break;
- case CALL:
- // We emit a "call foo" ASM instruction as a sequence of three SPARK Ada statements:
- // write return address on the stack
- // decrement the stack pointer
- // foo; (Ada form of a call to foo()
- NextAddr = InstAddr + (STARS_ea_t) this->GetSize();
+ case CALL:
+ // We emit a "call foo" ASM instruction as a sequence of three SPARK Ada statements:
+ // write return address on the stack
+ // decrement the stack pointer
+ // foo; (Ada form of a call to foo()
+ NextAddr = InstAddr + (STARS_ea_t) this->GetSize();
+ PrintSPARKIndentTabs(OutFile);
+ // Comment out memory write of return address to speed up prover.
+ SMP_fprintf(OutFile, " -- X86.WriteMem%d((X86.RSP - %d), 16#%llx# );\n",
+ STARS_ISA_Bitwidth, global_STARS_program->GetSTARS_ISA_Bytewidth(), (unsigned long long) NextAddr);
+
+ FuncTarget = this->GetTrimmedCalledFunctionName();
+ if ((0 == FuncTarget.compare("exit")) || (0 == FuncTarget.compare("abort"))) {
+ // The exit() call conflicts with the Ada keyword "exit."
+ // FuncTarget = "Zephyr_exit";
+ // We want to set Exit_Called and return up the call chain.
PrintSPARKIndentTabs(OutFile);
- // Comment out memory write of return address to speed up prover.
- SMP_fprintf(OutFile, " -- X86.WriteMem%d((X86.RSP - %d), 16#%llx# );\n",
- STARS_ISA_Bitwidth, global_STARS_program->GetSTARS_ISA_Bytewidth(), (unsigned long long) NextAddr);
-
- FuncTarget = this->GetTrimmedCalledFunctionName();
- if ((0 == FuncTarget.compare("exit")) || (0 == FuncTarget.compare("abort"))) {
- // The exit() call conflicts with the Ada keyword "exit."
- // FuncTarget = "Zephyr_exit";
- // We want to set Exit_Called and return up the call chain.
- PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, " X86.Exit_Called := true;\n");
- PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, " X86.RSP := X86.RSP + 8;\n");
- PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, " return;\n");
+ SMP_fprintf(OutFile, " X86.Exit_Called := true;\n");
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, " X86.RSP := X86.RSP + 8;\n");
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, " return;\n");
+ }
+ else {
+ if (IsLibFuncName(FuncTarget)) {
+ FuncTarget = "C_Library." + FuncTarget; // Use C_Library Ada package that we created.
}
- else {
- if (IsLibFuncName(FuncTarget)) {
- FuncTarget = "C_Library." + FuncTarget; // Use C_Library Ada package that we created.
- }
- PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, " X86.RSP := X86.RSP - %d;\n", global_STARS_program->GetSTARS_ISA_Bytewidth());
- PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, " %s ;\n", FuncTarget.c_str());
-
- // See if we are calling a function that might call abort() or exit(), et al., somewhere
- // in its call chain.
- STARS_ea_t TargetAddr = this->GetCallTarget();
- if (STARS_BADADDR != TargetAddr) {
- SMPBasicBlock *CurrBlock = this->GetBlock();
- SMPFunction *TargetFunc = CurrBlock->GetFunc()->GetProg()->FindFunction(TargetAddr);
- if (nullptr != TargetFunc) {
- if ((!TargetFunc->FuncReturnsToCaller()) || TargetFunc->HasCallToNonReturningFunc() || TargetFunc->HasCalleeChainWithNonReturningFunc()) {
- // Call chain could have set X86.Exit_Called, signalling that exit() or something similar was called.
- PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, " if X86.Exit_Called then \n");
- PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, "\t return;\n");
- PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, " end if;\n");
- }
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, " X86.RSP := X86.RSP - %d;\n", global_STARS_program->GetSTARS_ISA_Bytewidth());
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, " %s ;\n", FuncTarget.c_str());
+
+ // See if we are calling a function that might call abort() or exit(), et al., somewhere
+ // in its call chain.
+ STARS_ea_t TargetAddr = this->GetCallTarget();
+ if (STARS_BADADDR != TargetAddr) {
+ SMPBasicBlock *CurrBlock = this->GetBlock();
+ SMPFunction *TargetFunc = CurrBlock->GetFunc()->GetProg()->FindFunction(TargetAddr);
+ if (nullptr != TargetFunc) {
+ if ((!TargetFunc->FuncReturnsToCaller()) || TargetFunc->HasCallToNonReturningFunc() || TargetFunc->HasCalleeChainWithNonReturningFunc()) {
+ // Call chain could have set X86.Exit_Called, signalling that exit() or something similar was called.
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, " if X86.Exit_Called then \n");
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "\t return;\n");
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, " end if;\n");
}
}
}
+ }
- // Handle tail calls, whose data-flow type was altered from RETURN to CALL.
- if (this->IsTailCall() || this->IsCondTailCall()) {
- // We increase the stack size by 8 to swallow the return address, then
- // execute a SPARK Ada return instruction.
- PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, " X86.RSP := X86.RSP + %d;\n", global_STARS_program->GetSTARS_ISA_Bytewidth());
- PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, " return;\n");
- }
- break;
-
- case INDIR_CALL:
- break;
-
- case RETURN:
+ // Handle tail calls, whose data-flow type was altered from RETURN to CALL.
+ if (this->IsTailCall() || this->IsCondTailCall()) {
// We increase the stack size by 8 to swallow the return address, then
// execute a SPARK Ada return instruction.
PrintSPARKIndentTabs(OutFile);
SMP_fprintf(OutFile, " X86.RSP := X86.RSP + %d;\n", global_STARS_program->GetSTARS_ISA_Bytewidth());
PrintSPARKIndentTabs(OutFile);
SMP_fprintf(OutFile, " return;\n");
- break;
+ }
+ break;
- case HALT:
- break;
+ case INDIR_CALL:
+ break;
+
+ case RETURN:
+ // We increase the stack size by 8 to swallow the return address, then
+ // execute a SPARK Ada return instruction.
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, " X86.RSP := X86.RSP + %d;\n", global_STARS_program->GetSTARS_ISA_Bytewidth());
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, " return;\n");
+ break;
+
+ case HALT:
+ break;
}
if (PrintOperands) {
diff --git a/src/base/SMPProgram.cpp b/src/base/SMPProgram.cpp
index c1e652e5aec2a28f77aac49f6d9ede8c91aa49a2..9477d9755ec2c7b1523e0ff5b32258840bf095a4 100644
--- a/src/base/SMPProgram.cpp
+++ b/src/base/SMPProgram.cpp
@@ -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 = (0x402a30 == TempFunc->GetFirstFuncAddr());
if (FuncFound) {
TempFunc->Dump();
TempFunc->DumpDotCFG();