From a7a94176f49c6ef437abc812dc918f8aa948b8e1 Mon Sep 17 00:00:00 2001
From: clc5q <clc5q@git.zephyr-software.com>
Date: Thu, 24 Sep 2015 15:19:46 +0000
Subject: [PATCH] Continue SPARK Ada translation improvements at package and
procedure level.
Former-commit-id: 2735035e70eea9a8cedc0dfc0ee4f332035e16e9
---
include/base/SMPDataFlowAnalysis.h | 3 ++
include/base/SMPFunction.h | 1 +
include/base/SMPProgram.h | 4 +++
src/base/SMPDataFlowAnalysis.cpp | 36 ++++++++++++++++++++++++
src/base/SMPFunction.cpp | 26 +++++++++++++++--
src/base/SMPProgram.cpp | 33 +++++++++++++++++++++-
src/drivers/idapro/SMPStaticAnalyzer.cpp | 2 +-
7 files changed, 101 insertions(+), 4 deletions(-)
diff --git a/include/base/SMPDataFlowAnalysis.h b/include/base/SMPDataFlowAnalysis.h
index da891dd1..001ecefe 100644
--- a/include/base/SMPDataFlowAnalysis.h
+++ b/include/base/SMPDataFlowAnalysis.h
@@ -973,4 +973,7 @@ void GetPointerArgPositionsForCallName(std::string CalleeName, unsigned int &Arg
// Utility to count bits set in an unsigned int, e.g. ArgPosBits.
unsigned int CountBitsSet(unsigned int ArgPosBits);
+// Is FuncName a standard library function name?
+bool IsLibFuncName(std::string CalleeName);
+
#endif
diff --git a/include/base/SMPFunction.h b/include/base/SMPFunction.h
index 1c48d026..c359f5ad 100644
--- a/include/base/SMPFunction.h
+++ b/include/base/SMPFunction.h
@@ -378,6 +378,7 @@ public:
bool FindReachingStackDelta(STARS_sval_t &StackDelta); // Find maximum stack delta in TempStackDeltaReachesList; return true if one consistent delta is in the list
void GatherIncomingArgTypes(void); // Use the SSA marker inst to record incoming arg types in member InArgTypes.
void EmitAnnotations(FILE *AnnotFile, FILE *InfoAnnotFile);
+ void PreProcessForSPARKAdaTranslation(void); // Perform look-ahead steps needed before translation to SPARK Ada.
void EmitFuncSPARKAda(void); // Emit SPARK Ada translation of function
void LiveVariableAnalysis(bool Recomputing); // Perform Live Variable Analysis across all blocks
void RecomputeSSA(void); // Recompute LVA and SSA and all dependent data structures now that unreachable blocks have been removed.
diff --git a/include/base/SMPProgram.h b/include/base/SMPProgram.h
index fbece3c4..a2feacf3 100644
--- a/include/base/SMPProgram.h
+++ b/include/base/SMPProgram.h
@@ -119,6 +119,8 @@ public:
inline ProfilerInformation *GetProfInfo(void) { return ProfInfo; };
SMPFunction* FindFunction(STARS_ea_t FirstAddr); // get function from first addr in function
inline std::size_t GetFuncCount(void) const { return FuncMap.size(); };
+ inline std::set<std::string>::iterator GetFirstLibraryFuncName(void) { return LibraryCallTargetNames.begin(); };
+ inline std::set<std::string>::iterator GetLastLibraryFuncName(void) { return LibraryCallTargetNames.end(); };
// Set methods
void ProfGranularityFinished(FILE *AnnotFile, FILE *InfoAnnotFile); // notification from ProfilerInformation
@@ -129,6 +131,7 @@ public:
void AddBlockToRemovalList(SMPBasicBlock *UnreachableBlock); // Add block, e.g. with "call 0" instruction, to later removal list.
std::pair<std::map<std::string, STARS_ea_t>::iterator, bool> InsertGlobalNameAddrMapEntry(std::pair<std::string, STARS_ea_t> TempPair) { return GlobalNameMap.insert(TempPair); };
void InsertGlobalVarTableEntry(std::pair<STARS_ea_t, struct GlobalVar> VarItem) { GlobalVarTable.insert(VarItem); };
+ inline std::pair<std::set<std::string>::iterator, bool> InsertLibraryFuncName(std::string FuncName) { return LibraryCallTargetNames.insert(FuncName); };
// Query methods
bool IsUnsharedFragment(STARS_ea_t InstAddr); // Does InstAddr begin an unshared function fragment?
@@ -169,6 +172,7 @@ private:
std::list<SMPInstr *> UnreachableInstList; // unreachable instructions, removed from their functions
std::list<SMPBasicBlock *> BlocksPendingRemoval; // blocks that need to be removed later as unreachable
std::set<SMPFunction *> FuncsWithBlocksRemoved;
+ std::set<std::string> LibraryCallTargetNames; // Standard library functions called by program; used in SPARK Ada translation
// Methods
void InitStaticDataTable(void); // Gather info about global static data locations
diff --git a/src/base/SMPDataFlowAnalysis.cpp b/src/base/SMPDataFlowAnalysis.cpp
index cfc7dc75..7f913ed0 100644
--- a/src/base/SMPDataFlowAnalysis.cpp
+++ b/src/base/SMPDataFlowAnalysis.cpp
@@ -4189,3 +4189,39 @@ void GetLibFuncFGInfo(string FuncName, struct FineGrainedInfo &InitFGInfo) {
} // end of GetLibFuncFGInfo()
+// Is FuncName a standard library function name?
+bool IsLibFuncName(std::string CalleeName) {
+ // Return true if we find the name in any of our function type maps.
+
+ map<string, struct FineGrainedInfo>::iterator RetTypeIter = ReturnRegisterTypeMap.find(CalleeName);
+ if (RetTypeIter != ReturnRegisterTypeMap.end()) { // found
+ return true;
+ }
+
+ map<string, unsigned int>::iterator PtrArgIter = PointerArgPositionMap.find(CalleeName);
+ if (PtrArgIter != PointerArgPositionMap.end()) { // found it
+ return true;
+ }
+
+ map<string, unsigned int>::iterator TaintIter = TaintWarningArgPositionMap.find(CalleeName);
+ if (TaintIter != TaintWarningArgPositionMap.end()) { // found it
+ return true;
+ }
+
+ map<string, unsigned int>::iterator UnsignedIter = UnsignedArgPositionMap.find(CalleeName);
+ if (UnsignedIter != UnsignedArgPositionMap.end()) { // found it
+ return true;
+ }
+
+ map<string, string>::iterator SinkIter = IntegerErrorCallSinkMap.find(CalleeName);
+ if (SinkIter != IntegerErrorCallSinkMap.end()) { // found it
+ return true;
+ }
+
+ // Put searches for additional library function names here.
+ if (0 == CalleeName.compare("setuid")) {
+ return true;
+ }
+
+ return false;
+} // end of IsLibFuncName()
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index 6a21dadf..ea5a97ef 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -8677,6 +8677,26 @@ void SMPFunction::MarkFunctionSafe() {
return;
} // end of SMPFunction::MarkFunctionSafe()
+// Perform look-ahead steps needed before translation to SPARK Ada.
+void SMPFunction::PreProcessForSPARKAdaTranslation(void) {
+ for (vector<SMPBasicBlock *>::iterator BlockIter = this->RPOBlocks.begin(); BlockIter != this->RPOBlocks.end(); ++BlockIter) {
+ SMPBasicBlock *CurrBlock = (*BlockIter);
+ if (CurrBlock->HasCallInstruction()) {
+ for (vector<SMPInstr *>::iterator InstIter = CurrBlock->GetFirstInst(); InstIter != CurrBlock->GetLastInst(); ++InstIter) {
+ SMPInstr *CurrInst = (*InstIter);
+ if (CurrInst->GetDataFlowType() == CALL) {
+ string CalledFuncName = CurrInst->GetTrimmedCalledFunctionName();
+ if (IsLibFuncName(CalledFuncName)) {
+ pair<set<string>::iterator, bool> InsertResult = this->Program->InsertLibraryFuncName(CalledFuncName);
+ }
+ }
+ }
+ }
+ }
+
+ return;
+} // end of SMPFunction::PreProcessForSPARKAdaTranslation()
+
// For debugging purposes, only emit SPARK Ada for main().
#define STARS_EMIT_ADA_FOR_MAIN_ONLY 1
@@ -8685,6 +8705,7 @@ void SMPFunction::EmitFuncSPARKAda(void) {
if (this->IsLinkerStub()) {
return;
}
+
string AdaFuncName(this->GetFuncName());
#if STARS_EMIT_ADA_FOR_MAIN_ONLY
if (0 != strcmp("main", AdaFuncName.c_str())) {
@@ -8701,9 +8722,10 @@ void SMPFunction::EmitFuncSPARKAda(void) {
// Emit beginning of function body.
SMP_fprintf(BodyFile, "procedure %s\nis\n", AdaFuncName.c_str());
- SMP_fprintf(BodyFile, "\tra0 : Unsigned8 := X86.ReadMem8(X86.RSP);\n");
+ SMP_fprintf(BodyFile, "\tSaveStackPtr : Unsigned64 := X86.RSP with Ghost;\n");
+ SMP_fprintf(BodyFile, "\tra0 : Unsigned8 := X86.ReadMem8(X86.RSP) with Ghost;\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, "\tra%u : Unsigned8 := X86.ReadMem8(X86.RSP + %u) with Ghost;\n", i, i);
}
SMP_fprintf(BodyFile, "\nbegin\n");
diff --git a/src/base/SMPProgram.cpp b/src/base/SMPProgram.cpp
index b343346a..4074c361 100644
--- a/src/base/SMPProgram.cpp
+++ b/src/base/SMPProgram.cpp
@@ -788,6 +788,7 @@ 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
+ size_t ByteWidth = global_STARS_program->GetSTARS_ISA_Bytewidth();
// Extract "foo" from "foo.exe" to get the Ada package name
string PackageName;
@@ -815,8 +816,38 @@ bool SMPProgram::EmitProgramSPARKAda(void) {
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.
+ // Loop through all functions and perform look-ahead pre-processing needed for later annotation emission.
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->PreProcessForSPARKAdaTranslation();
+ }
+ } // end for all functions
+
+ // Emit procedure specifications and bodies for library functions
+ for (set<string>::iterator NameIter = this->LibraryCallTargetNames.begin(); NameIter != this->LibraryCallTargetNames.end(); ++NameIter) {
+ string LibFuncName = (*NameIter);
+ SMP_fprintf(SpecFile, "procedure %s with\n", LibFuncName.c_str());
+ SMP_fprintf(BodyFile, "procedure %s is\nbegin\n\tX86.RSP := X86.RSP + %u;\n", LibFuncName.c_str(), ByteWidth);
+ if (0 != LibFuncName.compare("setuid")) {
+ // Emit minimal stub
+ SMP_fprintf(SpecFile, "\tGlobal => (In_Out => X86.RSP),\n");
+ SMP_fprintf(SpecFile, "\tPost => (X86.RSP = X86.RSP'Old + 8);\n\n");
+ }
+ else { // emit setuid stub
+ SMP_fprintf(SpecFile, "\tGlobal => (Input => (X86.RDI),\n");
+ SMP_fprintf(SpecFile, "\t\tIn_Out => (Dummy_Var, X86.RSP)),\n");
+ SMP_fprintf(SpecFile, "\tPre => (X86.RDI /= 0),\n");
+ SMP_fprintf(SpecFile, "\tPost => ((Dummy_Var = Dummy_Var'Old + Unsigned64(X86.EDI)) and\n");
+ SMP_fprintf(SpecFile, "\t\t(X86.RSP = X86.RSP'Old + 8));\n\n");
+ SMP_fprintf(BodyFile, "\tDummy_Var := Dummy_Var + Unsigned64(X86.EDI);\n");
+ }
+ SMP_fprintf(BodyFile, "end %s;\n\n", LibFuncName.c_str());
+ }
+
+ // Loop through all functions and emit annotations for each.
for (FuncIter = this->FuncMap.begin(); FuncIter != this->FuncMap.end(); ++FuncIter) {
SMPFunction *TempFunc = FuncIter->second;
if (TempFunc == NULL) continue;
diff --git a/src/drivers/idapro/SMPStaticAnalyzer.cpp b/src/drivers/idapro/SMPStaticAnalyzer.cpp
index 6e3bf2ff..a8c55b1c 100644
--- a/src/drivers/idapro/SMPStaticAnalyzer.cpp
+++ b/src/drivers/idapro/SMPStaticAnalyzer.cpp
@@ -62,7 +62,7 @@
using namespace std;
-#define SMP_DEBUG_DELAY 1 // for setting an early breakpoint
+#define SMP_DEBUG_DELAY 0 // for setting an early breakpoint
// Set to 1 for debugging output
#define SMP_DEBUG 1
--
GitLab