From fc4a9f030fc633c74d46d3822d7495ee20b9f0c2 Mon Sep 17 00:00:00 2001
From: clc5q <clc5q@git.zephyr-software.com>
Date: Fri, 18 Sep 2015 13:13:39 +0000
Subject: [PATCH] More SPARK Ada translation improvements.
Former-commit-id: 7cce2c3c80b7256ce696292b50b29aa4d8f86210
---
include/base/SMPInstr.h | 1 +
src/base/SMPFunction.cpp | 24 ++++++++++++++----
src/base/SMPInstr.cpp | 31 +++++++++++++++++++++---
src/base/SMPProgram.cpp | 4 +++
src/drivers/idapro/SMPStaticAnalyzer.cpp | 2 +-
5 files changed, 52 insertions(+), 10 deletions(-)
diff --git a/include/base/SMPInstr.h b/include/base/SMPInstr.h
index 296174ce..490209fd 100644
--- a/include/base/SMPInstr.h
+++ b/include/base/SMPInstr.h
@@ -612,6 +612,7 @@ public:
void MDEmitSPARKAdaSetCondCodeIntoReg(FILE *OutFile); // emit SPARK Ada for moving a condition code value or expr into a register
void MDEmitSPARKAdaCondition(FILE *OutFile); // emit SPARK Ada for the current conditional branch
void MDEmitSPARKAdaInvertedCondition(FILE *OutFile); // Invert the condition of the current conditional branch and emit SPARK Ada equivalent.
+ void EmitSPARKAdaInvariantsForRetAddr(FILE *BodyFile) const;
void EmitSPARKAda(FILE *OutFile); // Emit SPARK-Ada translation of instruction
// Analysis methods
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index 84bf0ba0..b3824a2f 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -39,6 +39,7 @@ using namespace std;
#include <set>
#include <vector>
#include <algorithm>
+#include <iostream>
#include <cstring>
#include <cstdint>
@@ -8684,26 +8685,30 @@ void SMPFunction::EmitFuncSPARKAda(void) {
if (this->IsLinkerStub()) {
return;
}
+ string AdaFuncName(this->GetFuncName());
#if STARS_EMIT_ADA_FOR_MAIN_ONLY
- if (0 != strcmp("main", this->GetFuncName())) {
+ if (0 != strcmp("main", AdaFuncName.c_str())) {
return;
}
#endif
+ // Convert dashes to underscores in the func name to suit Ada standards.
+ replace(AdaFuncName.begin(), AdaFuncName.end(), '-', '_');
+
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, "procedure %s\nis\n", AdaFuncName.c_str());
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");
+ SMP_fprintf(BodyFile, "\nbegin\n");
// Emit procedure specification.
- SMP_fprintf(HeaderFile, "procedure %s with\n", this->GetFuncName());
+ SMP_fprintf(HeaderFile, "procedure %s with\n", AdaFuncName.c_str());
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
@@ -8754,7 +8759,13 @@ void SMPFunction::EmitFuncSPARKAda(void) {
}
}
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, "\tPre => (X86.RSP > 16#FFFFFFFF00000000# and X86.RSP < 16#FFFFFFFFFFFFFF00#");
+ if (8 == ByteWidth) {
+ SMP_fprintf(HeaderFile, "\n\t\tand X86.EDI > 0),\n"); // argc > 0 for x86_64
+ }
+ else {
+ SMP_fprintf(HeaderFile, "),\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");
@@ -8777,6 +8788,9 @@ void SMPFunction::EmitFuncSPARKAda(void) {
++InstIter;
} // end while all instrs
+ SMP_fprintf(BodyFile, "\nend %s;\n", AdaFuncName.c_str());
+ STARS_SPARK_IndentCount = 0;
+
return;
} // end of SMPFunction::EmitFuncSPARKAda()
diff --git a/src/base/SMPInstr.cpp b/src/base/SMPInstr.cpp
index 6067a3a0..33d0030f 100644
--- a/src/base/SMPInstr.cpp
+++ b/src/base/SMPInstr.cpp
@@ -1025,17 +1025,17 @@ bool SMPRegTransfer::OperandTransfersHelper(const STARSOpndTypePtr &UseOp) const
// Does RTL show LeftOp has smaller bitwidth than the right hand side operands?
bool SMPRegTransfer::IsTruncatedWidthRTL(std::size_t &LeftBitWidth) const {
bool TruncatedWidth = false;
- STARSOpndTypePtr LeftOp = this->GetLeftOperand();
+ STARSOpndTypePtr LeftOp = this->GetLeftOperandNoNorm();
std::size_t LeftOpByteWidth = (std::size_t) LeftOp->GetByteWidth();
if (LeftOpByteWidth < global_STARS_program->GetSTARS_ISA_Bytewidth()) { // Forget it unless LeftOp is reduced width.
// Search right hand side for wider operands.
LeftBitWidth = 8 * LeftOpByteWidth;
STARSOpndTypePtr RightOp = nullptr;
if (this->HasRightSubTree()) {
- RightOp = this->GetRightTree()->GetLeftOperand();
+ RightOp = this->GetRightTree()->GetLeftOperandNoNorm();
}
else {
- RightOp = this->GetRightOperand();
+ RightOp = this->GetRightOperandNoNorm();
}
if (nullptr != RightOp) {
TruncatedWidth = ((RightOp->GetByteWidth() > LeftOpByteWidth) && (RightOp->IsRegOp() || RightOp->IsMemOp()));
@@ -2630,6 +2630,27 @@ void SMPInstr::MDEmitSPARKAdaInvertedCondition(FILE *OutFile) {
return;
} // end of SMPInstr::MDEmitSPARKAdaInvertedCondition()
+void SMPInstr::EmitSPARKAdaInvariantsForRetAddr(FILE *BodyFile) const {
+ PrintSPARKIndentTabs(BodyFile);
+ SMP_fprintf(BodyFile, "pragma Loop_Invariant(X86.Memory(SaveStackPtr) = ra0);\n");
+ PrintSPARKIndentTabs(BodyFile);
+ SMP_fprintf(BodyFile, "pragma Loop_Invariant(X86.Memory(SaveStackPtr + 1) = ra1);\n");
+ PrintSPARKIndentTabs(BodyFile);
+ SMP_fprintf(BodyFile, "pragma Loop_Invariant(X86.Memory(SaveStackPtr + 2) = ra2);\n");
+ PrintSPARKIndentTabs(BodyFile);
+ SMP_fprintf(BodyFile, "pragma Loop_Invariant(X86.Memory(SaveStackPtr + 3) = ra3);\n");
+ PrintSPARKIndentTabs(BodyFile);
+ SMP_fprintf(BodyFile, "pragma Loop_Invariant(X86.Memory(SaveStackPtr + 4) = ra4);\n");
+ PrintSPARKIndentTabs(BodyFile);
+ SMP_fprintf(BodyFile, "pragma Loop_Invariant(X86.Memory(SaveStackPtr + 5) = ra5);\n");
+ PrintSPARKIndentTabs(BodyFile);
+ SMP_fprintf(BodyFile, "pragma Loop_Invariant(X86.Memory(SaveStackPtr + 6) = ra6);\n");
+ PrintSPARKIndentTabs(BodyFile);
+ SMP_fprintf(BodyFile, "pragma Loop_Invariant(X86.Memory(SaveStackPtr + 7) = ra7);\n");
+
+ return;
+}
+
// Emit SPARK-Ada translation of instruction
void SMPInstr::EmitSPARKAda(FILE *OutFile) {
// Print the disassembly as a comment before the SPARK translation.
@@ -2671,6 +2692,7 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
PrintSPARKIndentTabs(OutFile);
SMP_fprintf(OutFile, "loop \n");
++STARS_SPARK_IndentCount;
+ this->EmitSPARKAdaInvariantsForRetAddr(OutFile);
}
}
@@ -5103,6 +5125,7 @@ void SMPInstr::SetLeaMemUseOp(STARSOpndTypePtr NewLeaOperand) {
// If DefReg is not already in the DEF list, add a DEF for it.
void SMPInstr::MDAddRegDef(uint16_t DefReg, bool Shown, SMPOperandType Type) {
STARSOpndTypePtr TempDef = this->STARSInstPtr->MakeRegOpnd(DefReg);
+ CanonicalizeOpnd(TempDef);
if (!Shown)
TempDef->SetNotVisible();
this->Defs.SetRef(TempDef, Type);
@@ -7928,7 +7951,7 @@ void SMPInstr::SCCPFetchConstUseValue(const STARSOpndTypePtr &UseOp, STARS_SCCP_
#if 1
int BaseReg = (int) UseOp->GetReg();
if (MD_STACK_POINTER_REG == BaseReg) {
- // ESP BaseReg in SIB byte means no base reg for StaticMemOp
+ // ESP BaseReg in means no base reg for StaticMemOp
BaseReg = STARS_x86_R_none;
}
if (UseOp->HasSIBByte()) {
diff --git a/src/base/SMPProgram.cpp b/src/base/SMPProgram.cpp
index d4a4cc75..b343346a 100644
--- a/src/base/SMPProgram.cpp
+++ b/src/base/SMPProgram.cpp
@@ -798,6 +798,10 @@ bool SMPProgram::EmitProgramSPARKAda(void) {
return false;
}
+
+ // Convert dashes to underscores in the package name to suit Ada standards.
+ replace(PackageName.begin(), PackageName.end(), '-', '_');
+
// Emit the package body.
SMP_fprintf(BodyFile, "Package body %s\n", PackageName.c_str());
SMP_fprintf(BodyFile, "with SPARK_Mode \nis\n\n");
diff --git a/src/drivers/idapro/SMPStaticAnalyzer.cpp b/src/drivers/idapro/SMPStaticAnalyzer.cpp
index a8c55b1c..6e3bf2ff 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
--
GitLab