diff --git a/include/base/SMPProgram.h b/include/base/SMPProgram.h
index aa14f3cc237388d4f6880ee4c55fd05a7fa289d0..fbece3c40a7a1895eb16603c1097adc2eb88a4f6 100644
--- a/include/base/SMPProgram.h
+++ b/include/base/SMPProgram.h
@@ -142,6 +142,7 @@ public:
void AnalyzeData(void); // Analyze static data in the program.
void Analyze(ProfilerInformation* pi, FILE *AnnotFile, FILE *InfoAnnotFile); // Analyze all functions in the program
void EmitDataAnnotations(FILE *AnnotFile, FILE *InfoAnnotFile); // Emit annotations for global data
+ bool EmitProgramSPARKAda(void); // return false if error occurs
void EmitAnnotations(FILE *AnnotFile, FILE *InfoAnnotFile); // Emit annotations for all functions
bool IsInstAddrStillInFunction(STARS_ea_t InstAddr, STARS_ea_t &FirstAddrInFunc); // is InstAddr still an SMPInstr inside an SMPFunction object? (not orphaned, not dead-code-removed)
bool IsChunkUnshared(STARS_ea_t ChunkAddr, STARS_ea_t FuncHeadStart, STARS_ea_t FuncHeadEnd); // Does chunk at ChunkAddr belong exclusively to FuncHead?
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index e67aff23143c629ee13cae00f86ebb1934e55d61..b11cbf64ff2bff2dbaa081a84460ddec83bc67dd 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -3976,7 +3976,7 @@ void SMPFunction::AdvancedAnalysis(void) {
} // end if not shared chunks
else { // has shared chunks; still want to compute stack frame info
#ifdef SMP_DEBUG_FUNC
- SMP_msg(" %s has shared chunks \n", this->GetFuncName());
+ SMP_msg("INFO: %s has shared chunks \n", this->GetFuncName());
#endif
// Figure out the stack frame and related info.
this->SetStackFrameInfo();
@@ -8644,7 +8644,6 @@ void SMPFunction::MarkFunctionSafe() {
// Emit SPARK Ada translation of function
void SMPFunction::EmitFuncSPARKAda(void) {
-#if ZST_EMIT_SPARK_ADA_TRANSLATION
if (this->IsLinkerStub()) {
return;
}
@@ -8654,9 +8653,82 @@ void SMPFunction::EmitFuncSPARKAda(void) {
}
#endif
- FILE *OutFile = global_STARS_program->GetSPARKSourceFile();
+ FILE *BodyFile = global_STARS_program->GetSPARKSourceFile();
FILE *HeaderFile = global_STARS_program->GetSPARKHeaderFile();
-
+ size_t ByteWidth = global_STARS_program->GetSTARS_ISA_Bytewidth();
+
+ // Emit beginning of function body.
+ SMP_fprintf(BodyFile, "procedure %s\nis\n", this->GetFuncName());
+ SMP_fprintf(BodyFile, "\tra0 : Unsigned8 := X86.ReadMem8(X86.RSP);\n");
+ for (unsigned short i = 1; i < ByteWidth; ++i) {
+ SMP_fprintf(BodyFile, "\tra%u : Unsigned8 := X86.ReadMem8(X86.RSP + %u);\n", i, i);
+ }
+ SMP_fprintf(BodyFile, "\n");
+
+ // Emit procedure specification.
+ SMP_fprintf(HeaderFile, "procedure %s with\n", this->GetFuncName());
+ SMP_fprintf(HeaderFile, "\tGlobal => (In_Out => (X86.Memory, X86.Exit_Called, X86.CarryFlag,\n");
+ SMP_fprintf(HeaderFile, "\t\tX86.OverflowFlag, X86.SignFlag, X86.ZeroFlag,\n");
+ // Form union of regs killed, LiveOut, and LiveIn
+ std::set<STARSOpndTypePtr, LessOp> RegInOutSet(this->KillSet);
+ // RegInOutSet.insert(this->LiveOutSet.begin(), this->LiveOutSet.end()); // must be subset of KillSet already
+ RegInOutSet.insert(this->RPOBlocks.at(0)->GetFirstLiveIn(), this->RPOBlocks.at(0)->GetLastLiveIn());
+ std::set<STARSOpndTypePtr, LessOp>::iterator RegIter = RegInOutSet.begin();
+ size_t RegCount = 0; // How many reg operands did we leave in the RegInOutSet. After this count comes memory operands.
+ // NOTE: When erase() was called on the memops after the regs, a seg fault happened on some random memop even though
+ // erase() succeeded on previous memops and the end of the set had not been reached. Quick fix is to do less erase()
+ // and let RegCount be our sentinel.
+ while (RegIter != RegInOutSet.end()) {
+ bool FlagsReg = (*RegIter)->MatchesReg(MD_FLAGS_REG);
+ bool RegOp = (*RegIter)->IsRegOp();
+ if (RegOp && (!FlagsReg)) { // Keep non-flags regs in set
+ ++RegIter;
+ ++RegCount;
+ }
+ else { // delete non-regs and flags reg from the set
+ // Use C++98 erase() method, which does not return a new iterator
+ if ((RegOp && FlagsReg) || (0 == RegCount)) { // have not seen first reg, or we are looking at flags reg
+ std::set<STARSOpndTypePtr, LessOp>::iterator NextRegIter(RegIter);
+ ++NextRegIter;
+ RegInOutSet.erase(RegIter);
+ RegIter = NextRegIter;
+ }
+ else if (0 < RegCount) { // Have processed regs and now we have moved past them in the set.
+ break;
+ }
+ }
+ }
+
+ size_t OutCount = 0;
+ for (RegIter = RegInOutSet.begin(); RegIter != RegInOutSet.end(); ++RegIter) {
+ if (0 == OutCount) { // first line does not need another newline
+ SMP_fprintf(HeaderFile, "\t\t");
+ }
+ else if (0 == (OutCount % 4)) { // print 4 regs per line
+ SMP_fprintf(HeaderFile, "\n\t\t");
+ }
+ ++OutCount;
+ if (OutCount == RegCount) { // last reg needs no comma after it, but must close inner parentheses
+ SMP_fprintf(HeaderFile, " X86.%s),\n", MDGetRegName(*RegIter));
+ break;
+ }
+ else {
+ SMP_fprintf(HeaderFile, " X86.%s, ", MDGetRegName(*RegIter));
+ }
+ }
+ SMP_fprintf(HeaderFile, "\t\tInput => (X86.StackAddressSize, X86.FS, X86.GS)),\n");
+ SMP_fprintf(HeaderFile, "\tPre => (X86.RSP > 16#FFFFFFFF00000000# and X86.RSP < 16#FFFFFFFFFFFFFF00#),\n");
+ SMP_fprintf(HeaderFile, "\tPost => (X86.RSP = (X86.RSP'Old + 8)) and\n");
+ SMP_fprintf(HeaderFile, "\t\t(X86.Memory(X86.RSP'Old) = X86.Memory'Old(X86.RSP'Old)) and\n");
+ SMP_fprintf(HeaderFile, "\t\t(X86.Memory(X86.RSP'Old + 1) = X86.Memory'Old(X86.RSP'Old + 1)) and\n");
+ SMP_fprintf(HeaderFile, "\t\t(X86.Memory(X86.RSP'Old + 2) = X86.Memory'Old(X86.RSP'Old + 2)) and\n");
+ SMP_fprintf(HeaderFile, "\t\t(X86.Memory(X86.RSP'Old + 3) = X86.Memory'Old(X86.RSP'Old + 3)) and\n");
+ SMP_fprintf(HeaderFile, "\t\t(X86.Memory(X86.RSP'Old + 4) = X86.Memory'Old(X86.RSP'Old + 4)) and\n");
+ SMP_fprintf(HeaderFile, "\t\t(X86.Memory(X86.RSP'Old + 5) = X86.Memory'Old(X86.RSP'Old + 5)) and\n");
+ SMP_fprintf(HeaderFile, "\t\t(X86.Memory(X86.RSP'Old + 6) = X86.Memory'Old(X86.RSP'Old + 6)) and\n");
+ SMP_fprintf(HeaderFile, "\t\t(X86.Memory(X86.RSP'Old + 7) = X86.Memory'Old(X86.RSP'Old + 7));\n");
+
+ // Iterate through all instructions and emit SPARK Ada for each.
list<SMPInstr *>::iterator InstIter = this->Instrs.begin();
#if SMP_USE_SSA_FNOP_MARKER
++InstIter; // skip marker instruction
@@ -8664,10 +8736,10 @@ void SMPFunction::EmitFuncSPARKAda(void) {
while (InstIter != this->Instrs.end()) {
SMPInstr *CurrInst = (*InstIter);
STARS_ea_t InstAddr = CurrInst->GetAddr();
- CurrInst->EmitSPARKAda(OutFile);
+ CurrInst->EmitSPARKAda(BodyFile);
++InstIter;
} // end while all instrs
-#endif
+
return;
} // end of SMPFunction::EmitFuncSPARKAda()
diff --git a/src/base/SMPInstr.cpp b/src/base/SMPInstr.cpp
index bda2b6054b4cdd8e6344f1063d681f55d64de536..ab2647e4b0c4a2fbe854fcdbd82112cd5b9cdb68 100644
--- a/src/base/SMPInstr.cpp
+++ b/src/base/SMPInstr.cpp
@@ -2672,7 +2672,7 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
// to the jump translation.
NextAddr = InstAddr + (STARS_ea_t) this->GetSize();
PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, " X86.WriteMem%d(Unsigned%d(X86.RSP - %d), %llx );\n", STARS_ISA_Bitwidth, STARS_ISA_Bitwidth,
+ 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());
@@ -2768,7 +2768,7 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
}
NextAddr = InstAddr + (STARS_ea_t) this->GetSize();
PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, " X86.WriteMem%d(Unsigned%d(X86.RSP - %d), %llu );\n",
+ 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());
diff --git a/src/base/SMPProgram.cpp b/src/base/SMPProgram.cpp
index 4c2829394bf45ab986dfd495e3033462adbdc13f..9b9837e0ad68e2278afee999c0ccb2387c6decc9 100644
--- a/src/base/SMPProgram.cpp
+++ b/src/base/SMPProgram.cpp
@@ -39,6 +39,8 @@
#include <map>
#include <vector>
#include <algorithm>
+#include <iostream>
+#include <sstream>
#include <cstdint>
#include <cstring>
@@ -776,6 +778,50 @@ void SMPProgram::EmitDataAnnotations(FILE *AnnotFile, FILE *InfoAnnotFile) {
return;
} // SMPProgram::EmitDataAnnotations()
+bool SMPProgram::EmitProgramSPARKAda(void) {
+ FILE *BodyFile = global_STARS_program->GetSPARKSourceFile(); // SPARK Ada *.adb implementation
+ FILE *SpecFile = global_STARS_program->GetSPARKHeaderFile(); // SPARK Ada *.ads specification
+ string RootName(global_STARS_program->GetRootFileName()); // original file name without path, e.g. foo.exe
+
+ // Extract "foo" from "foo.exe" to get the Ada package name
+ string PackageName;
+ istringstream StreamRootName(RootName);
+ (void) std::getline(StreamRootName, PackageName, '.');
+ if (PackageName.empty()) {
+ SMP_msg("ERROR: Could not extract an Ada package name from the root of file name %s\n", RootName.c_str());
+ return false;
+ }
+
+ // Emit the package body.
+ SMP_fprintf(BodyFile, "Package body %s\n", PackageName.c_str());
+ SMP_fprintf(BodyFile, "with SPARK_Mode \nis\n\n");
+
+ // Emit the package specification.
+ SMP_fprintf(SpecFile, "with Interfaces;\nuse Interfaces;\nwith X86;\n\n");
+ SMP_fprintf(SpecFile, "Package %s\n", PackageName.c_str());
+ SMP_fprintf(SpecFile, "with SPARK_Mode \nis\n\n");
+ SMP_fprintf(SpecFile, "\tsubtype Unsigned64 is X86.Unsigned64;\n");
+ SMP_fprintf(SpecFile, "\tsubtype Unsigned32 is X86.Unsigned32;\n");
+ SMP_fprintf(SpecFile, "\tsubtype Unsigned16 is X86.Unsigned16;\n");
+ SMP_fprintf(SpecFile, "\tsubtype Unsigned8 is X86.Unsigned8;\n\n");
+
+ // Loop through all functions and emit annotations for each.
+ map<STARS_ea_t, SMPFunction *>::iterator FuncIter;
+ for (FuncIter = this->FuncMap.begin(); FuncIter != this->FuncMap.end(); ++FuncIter) {
+ SMPFunction *TempFunc = FuncIter->second;
+ if (TempFunc == NULL) continue;
+ if (TempFunc->HasReducibleControlFlow()) {
+ TempFunc->EmitFuncSPARKAda();
+ }
+ } // end for all functions
+
+ // Wrap up the package files.
+ SMP_fprintf(BodyFile, "\nend %s;\n", PackageName.c_str());
+ SMP_fprintf(SpecFile, "\nend %s;\n", PackageName.c_str());
+
+ return true;
+} // end of SMPProgram::EmitProgramSPARKAda()
+
// Emit all annotations for the program.
void SMPProgram::EmitAnnotations(FILE *AnnotFile, FILE *InfoAnnotFile) {
long TotalSafeBlocks = 0; // basic blocks with no unsafe writes
@@ -795,12 +841,11 @@ void SMPProgram::EmitAnnotations(FILE *AnnotFile, FILE *InfoAnnotFile) {
TempFunc->EmitAnnotations(AnnotFile, InfoAnnotFile);
TotalSafeBlocks += TempFunc->GetSafeBlocks();
TotalUnsafeBlocks += TempFunc->GetUnsafeBlocks();
+ } // end for all functions
+
#if ZST_EMIT_SPARK_ADA_TRANSLATION
- if (TempFunc->HasReducibleControlFlow()) {
- TempFunc->EmitFuncSPARKAda();
- }
+ (void) this->EmitProgramSPARKAda();
#endif
- } // end for all functions
EndTime = time(NULL);
double TimeDiff = difftime(EndTime, StartTime);
diff --git a/src/drivers/idapro/SMPStaticAnalyzer.cpp b/src/drivers/idapro/SMPStaticAnalyzer.cpp
index a8c55b1cd3f483e3fe7565d79c5daef56c911748..6e3bf2ff4442370c1a7ee9291647e3d16f037f34 100644
--- a/src/drivers/idapro/SMPStaticAnalyzer.cpp
+++ b/src/drivers/idapro/SMPStaticAnalyzer.cpp
@@ -62,7 +62,7 @@
using namespace std;
-#define SMP_DEBUG_DELAY 0 // for setting an early breakpoint
+#define SMP_DEBUG_DELAY 1 // for setting an early breakpoint
// Set to 1 for debugging output
#define SMP_DEBUG 1