diff --git a/include/base/SMPInstr.h b/include/base/SMPInstr.h
index 8dd19acfc8608aa62d8310933594cd3849886e3c..db61f683b939205d70408124dfdb30595b12f758 100644
--- a/include/base/SMPInstr.h
+++ b/include/base/SMPInstr.h
@@ -846,6 +846,7 @@ public:
inline bool IsNop(void) const { return (booleans2 & INSTR_SET_NOP); }; // instruction is simple or complex no-op
inline bool MDIsFloatNop(void) const { return (GetIDAOpcode() == STARS_NN_fnop); };
inline bool MDIsExchange(void) const { return (GetIDAOpcode() == STARS_NN_xchg); };
+ inline bool MDIsExceptionThrow(void) const { return (GetIDAOpcode() == STARS_NN_ud2); };
bool IsMarkerInst(void) const;
bool IsDecrementRTL(void) const;
bool IsSetToZero(void) const;
@@ -994,6 +995,7 @@ public:
SMPoperator MDConvertJumpToOperator(void) const; // return SMP_GREATER_THAN for ja and jg opcodes, etc.
void EmitSPARKAdaLoopInvariants(FILE *BodyFile) const;
void EmitSPARKAda(FILE *OutFile, const bool DisAsmOnly = false); // Emit SPARK-Ada translation of instruction
+ bool MDEmitSPARKAdaSpecialOpcodes(FILE *OutFile, const bool UseFP); // Handle Ada translation of special machine reg opcodes, LOOP opcodes, etc.
// Analysis methods
STARSOpndTypePtr GetSourceOnlyOperand(void) const; // return non-flags-reg non-dest source operand
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index 2a2fa60994d607ed72fca31c70a3f3f32148c19f..7054d9c8c03d5b33e38cb301eec7cc0b3bacf99c 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -26346,7 +26346,8 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrTCFGBlockNum, const int DomTCFGBl
else {
// Nop at end of block could be for alignment, masking the control flow type of CALL
// or HALT before it.
- bool GoodCode = (((FlowType == CALL) || (FlowType == HALT) || CurrTCFGBlock->IsUnreachableBlock() || LastInst->IsNop())
+ bool SpecialLastInst = (LastInst->IsNop() || LastInst->MDIsExceptionThrow());
+ bool GoodCode = (((FlowType == CALL) || (FlowType == HALT) || CurrTCFGBlock->IsUnreachableBlock() || SpecialLastInst)
&& (0 == NumSuccessors));
if (!GoodCode) {
SMP_msg("ERROR: SPARK: Bad control flow at end of block, inst at %llx ", (uint64_t)LastInst->GetAddr());
diff --git a/src/base/SMPInstr.cpp b/src/base/SMPInstr.cpp
index f512f8e83f9858ef612895ca8a6197c5433dc392..20fdafd6c0b4804c2775199a722a55c7bcb05c75 100644
--- a/src/base/SMPInstr.cpp
+++ b/src/base/SMPInstr.cpp
@@ -1347,7 +1347,12 @@ void PrintSPARKAdaOperator(SMPoperator Oper, string &OutString, bool &PrefixProc
default:
SMP_msg("ERROR: SPARK: Cannot translate unknown operator: ");
SMP_msg(" %s \n", OperatorText[Oper]);
- OutString = "X86.StrangeArithmetic";
+ if (ShortCircuitExpr) {
+ OutString = "X86.StrangeArithmetic_Func";
+ }
+ else {
+ OutString = "X86.StrangeArithmetic";
+ }
PrefixProcCall = true;
break;
@@ -1358,7 +1363,13 @@ void PrintSPARKAdaOperator(SMPoperator Oper, string &OutString, bool &PrefixProc
case SMP_UNARY_POINTER_OPERATION:
SMP_msg("ERROR: SPARK: Cannot translate unknown operator: ");
SMP_msg(" %s \n", OperatorText[Oper]);
- OutString = "ERROR";
+ if (ShortCircuitExpr) {
+ OutString = "X86.StrangeUnaryArithmetic_Func";
+ }
+ else {
+ OutString = "X86.StrangeUnaryArithmetic";
+ }
+ PrefixUnary = true;
break;
}
return;
@@ -7047,7 +7058,6 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile, const bool DisAsmOnly) {
bool PrintOperands = false;
bool UseFP = this->GetBlock()->GetFunc()->UsesFramePointer();
SMPitype CurrDataFlowType = this->GetDataFlowType();
- std::string FuncTarget;
STARS_ea_t NextAddr;
std::size_t STARS_ISA_Bitwidth = global_STARS_program->GetSTARS_ISA_Bitwidth();
@@ -7084,6 +7094,10 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile, const bool DisAsmOnly) {
#endif
}
+ if (this->MDEmitSPARKAdaSpecialOpcodes(OutFile, UseFP)) {
+ return;
+ }
+
ControlFlowType FuncControlFlowType;
// Treat tail calls as CALL control flows, then do the RETURN aspect as a special check
// inside the CALL case. NOTE: Need special handling for conditional tail calls.
@@ -7340,13 +7354,14 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile, const bool DisAsmOnly) {
// 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();
+ std::string FuncTarget = this->GetTrimmedCalledFunctionName();
if ((0 == FuncTarget.compare("exit")) || (0 == FuncTarget.compare("abort"))) {
// The exit() call conflicts with the Ada keyword "exit."
// FuncTarget = "Zephyr_exit";
@@ -7397,6 +7412,7 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile, const bool DisAsmOnly) {
SMP_fprintf(OutFile, " return;\n");
}
break;
+ }
case INDIR_CALL:
break;
@@ -7559,6 +7575,41 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile, const bool DisAsmOnly) {
return;
} // end of SMPInstr::EmitSPARKAda()
+// Handle Ada translation of special machine reg opcodes, LOOP opcodes, etc.
+bool SMPInstr::MDEmitSPARKAdaSpecialOpcodes(FILE *OutFile, const bool UseFP) {
+ bool SpecialOpcodeTranslated = false;
+ uint16_t opcode = this->GetIDAOpcode();
+ if ((STARS_NN_rdrand == opcode) || (STARS_NN_rdseed == opcode)) {
+ STARSDefUseIter DefIter = this->GetFirstNonFlagsDef();
+ assert(this->GetLastDef() != DefIter);
+ PrintSPARKIndentTabs(OutFile);
+ this->PrintSPARKAdaOperand(DefIter->GetOp(), OutFile, true, UseFP, true, false, true);
+ SMP_fprintf(OutFile, " := Interfaces.Discrete_Random(X86.Gen);\n");
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "X86.CarryFlag = true;\n");
+ SpecialOpcodeTranslated = true;
+ }
+ else if (this->MDIsLoopInstr()) {
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "X86.RCX = X86.RCX - 1;\n");
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "exit when (X86.RCX = 0);\n");
+ // Some LOOP opcodes also check the ZeroFlag (ZF).
+ if ((STARS_NN_loope == opcode) || (STARS_NN_loope == opcode) || (STARS_NN_loopqe == opcode) || (STARS_NN_loopwe == opcode)) {
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "exit when (X86.ZeroFlag);\n");
+ }
+ else if ((STARS_NN_loopdne == opcode) || (STARS_NN_loopne == opcode) || (STARS_NN_loopqne == opcode) || (STARS_NN_loopwne == opcode)) {
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "exit when (not X86.ZeroFlag);\n");
+ }
+ SpecialOpcodeTranslated = true;
+ }
+
+
+ return SpecialOpcodeTranslated;
+} // end of SMPInstr::MDEmitSPARKAdaSpecialOpcodes()
+
// Refactored helper to emit conditional loop exits in SPARK for loops with multiple exit target blocks.
void SMPInstr::EmitSPARKConditionalLoopMultiExit(FILE *BodyFile, const size_t LoopNum, const bool InvertCondition, const STARSCFGBlock *CFGBlock) {
int ExitTargetBlockNum;