From 2acc7d161c8061d203e00d00ea81706ef2f7149c Mon Sep 17 00:00:00 2001
From: clc5q <clc5q@git.zephyr-software.com>
Date: Tue, 2 Sep 2014 14:55:40 +0000
Subject: [PATCH] Emit SPARK Ada loops.
---
SMPFunction.cpp | 12 ++---
SMPInstr.cpp | 135 +++++++++++++++++++++++++++++++++++++++++++++++-
SMPInstr.h | 1 +
3 files changed, 141 insertions(+), 7 deletions(-)
diff --git a/SMPFunction.cpp b/SMPFunction.cpp
index 3e532639..305faa12 100644
--- a/SMPFunction.cpp
+++ b/SMPFunction.cpp
@@ -3519,8 +3519,8 @@ bool SMPFunction::WritesAboveLocalFrame(op_t DestOp, bool OpNormalized, ea_t Ins
|| (EBPrelative && (SignedOffset > 0));
if (InArgWrite && OpNormalized && (0 == SignedOffset)) {
- SMP_msg("DANGER: Write to saved return address detected at %lx in function that begins at %lx\n",
- InstAddr, (unsigned long) this->FirstEA);
+ SMP_msg("DANGER: Write to saved return address detected at %llx in function that begins at %llx\n",
+ (unsigned long long) InstAddr, (unsigned long long) this->FirstEA);
this->SetUnsafeForFastReturns(true, RETURN_ADDRESS_WRITE);
}
@@ -3560,13 +3560,13 @@ bool SMPFunction::AccessAboveLocalFrame(op_t StackOp, bool OpNormalized, ea_t In
if (InArgAccess && OpNormalized && (0 == SignedOffset)) {
if (WriteAccess) {
- SMP_msg("DANGER: Write to saved return address detected at %lx in function that begins at %lx\n",
- InstAddr, (unsigned long) this->FirstEA);
+ SMP_msg("DANGER: Write to saved return address detected at %llx in function that begins at %llx\n",
+ (unsigned long long) InstAddr, (unsigned long long) this->FirstEA);
this->SetUnsafeForFastReturns(true, RETURN_ADDRESS_WRITE);
}
else {
- SMP_msg("INFO: Read of saved return address detected at %lx in function that begins at %lx\n",
- InstAddr, (unsigned long) this->FirstEA);
+ SMP_msg("INFO: Read of saved return address detected at %llx in function that begins at %llx\n",
+ (unsigned long long) InstAddr, (unsigned long long) this->FirstEA);
this->SetUnsafeForFastReturns(true, RETURN_ADDRESS_READ);
}
}
diff --git a/SMPInstr.cpp b/SMPInstr.cpp
index 16785c0d..011a4b5f 100644
--- a/SMPInstr.cpp
+++ b/SMPInstr.cpp
@@ -1942,6 +1942,111 @@ void SMPInstr::PrintDeadRegs(FILE *OutputFile) {
return;
} // end of SMPInstr::PrintDeadRegs()
+// Invert the condition of the current conditional branch and emit SPARK Ada equivalent.
+void SMPInstr::MDEmitSPARKAdaInvertedCondition(FILE *OutFile) {
+ ushort opcode = this->SMPcmd.itype;
+ switch (opcode) {
+ NN_ja: // Jump if Above (CF=0 & ZF=0)
+ NN_jnbe: // Jump if Not Below or Equal (CF=0 & ZF=0)
+ SMP_fprintf(OutFile, "(CarryFlag or ZeroFlag)");
+ break;
+
+ NN_jae: // Jump if Above or Equal (CF=0)
+ NN_jnb: // Jump if Not Below (CF=0)
+ NN_jnc: // Jump if Not Carry (CF=0)
+ SMP_fprintf(OutFile, "(CarryFlag)");
+ break;
+
+ NN_jb: // Jump if Below (CF=1)
+ NN_jc: // Jump if Carry (CF=1)
+ NN_jnae: // Jump if Not Above or Equal (CF=1)
+ SMP_fprintf(OutFile, "(not CarryFlag)");
+ break;
+
+ NN_jbe: // Jump if Below or Equal (CF=1 | ZF=1)
+ NN_jna: // Jump if Not Above (CF=1 | ZF=1)
+ SMP_fprintf(OutFile, "(not (CarryFlag or ZeroFlag))");
+ break;
+
+ NN_jcxz: // Jump if CX is 0
+ SMP_fprintf(OutFile, "(CX /= 0)");
+ break;
+
+ NN_jecxz: // Jump if ECX is 0
+ SMP_fprintf(OutFile, "(ECX /= 0)");
+ break;
+
+ NN_jrcxz: // Jump if RCX is 0
+ SMP_fprintf(OutFile, "(RCX /= 0)");
+ break;
+
+ NN_je: // Jump if Equal (ZF=1)
+ NN_jz: // Jump if Zero (ZF=1)
+ SMP_fprintf(OutFile, "(not ZeroFlag)");
+ break;
+
+
+ NN_jg: // Jump if Greater (ZF=0 & SF=OF)
+ NN_jnle: // Jump if Not Less or Equal (ZF=0 & SF=OF)
+ SMP_fprintf(OutFile, "(ZeroFlag or (SignFlag \\= OverflowFlag))");
+ break;
+
+ NN_jge: // Jump if Greater or Equal (SF=OF)
+ NN_jnl: // Jump if Not Less (SF=OF)
+ SMP_fprintf(OutFile, "(SignFlag \\= OverflowFlag)");
+ break;
+
+ NN_jl: // Jump if Less (SF!=OF)
+ SMP_fprintf(OutFile, "(SignFlag = OverflowFlag)");
+ break;
+
+ NN_jle: // Jump if Less or Equal (ZF=1 | SF!=OF)
+ NN_jng: // Jump if Not Greater (ZF=1 | SF!=OF)
+ SMP_fprintf(OutFile, "((not Zeroflag) and (SignFlag = OverflowFlag))");
+ break;
+
+ NN_jne: // Jump if Not Equal (ZF=0)
+ NN_jnz: // Jump if Not Zero (ZF=0)
+ SMP_fprintf(OutFile, "(ZeroFlag)");
+ break;
+
+ NN_jnge: // Jump if Not Greater or Equal (ZF=1)
+ SMP_fprintf(OutFile, "(not ZeroFlag)");
+ break;
+
+ NN_jno: // Jump if Not Overflow (OF=0)
+ SMP_fprintf(OutFile, "(OverflowFlag)");
+ break;
+
+ NN_jnp: // Jump if Not Parity (PF=0)
+ NN_jpo: // Jump if Parity Odd (PF=0)
+ SMP_fprintf(OutFile, "(ParityFlag)");
+ break;
+
+ NN_jns: // Jump if Not Sign (SF=0)
+ SMP_fprintf(OutFile, "(SignFlag)");
+ break;
+
+ NN_jo: // Jump if Overflow (OF=1)
+ SMP_fprintf(OutFile, "(not OverflowFlag)");
+ break;
+
+ NN_jp: // Jump if Parity (PF=1)
+ NN_jpe: // Jump if Parity Even (PF=1)
+ SMP_fprintf(OutFile, "(not ParityFlag)");
+ break;
+
+ NN_js: // Jump if Sign (SF=1)
+ SMP_fprintf(OutFile, "(not SignFlag)");
+ break;
+
+ default:
+ SMP_fprintf(OutFile, "ERROR: Unknown conditional branch opcode at %llx %s\n", (unsigned long long) this->GetAddr(), this->GetDisasm());
+ break;
+ }
+ return;
+} // end of SMPInstr::MDEmitSPARKAdaInvertedCondition()
+
// Emit SPARK-Ada translation of instruction
void SMPInstr::EmitSPARKAda(FILE *OutFile) {
if (this->IsNop()) {
@@ -1950,13 +2055,21 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
// Print the disassembly as a comment before the SPARK translation.
PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, " -- %s\n", this->GetDisasm());
+ SMP_fprintf(OutFile, " -- %lx %s\n", (unsigned long) this->GetAddr(), this->GetDisasm());
bool PrintOperands = false;
SMPitype CurrDataFlowType = this->GetDataFlowType();
std::string FuncTarget;
ea_t NextAddr;
+ // Detect start of a loop.
+ if (this->IsFirstInBlock() && this->GetBlock()->IsLoopHeaderBlock()) {
+ // We want to print "loop" and increase indentation.
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "loop \n");
+ ++STARS_SPARK_IndentCount;
+ }
+
switch (CurrDataFlowType) {
case DEFAULT:
case LABEL:
@@ -1966,6 +2079,26 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
case JUMP:
case COND_BRANCH:
+ // Detect loop-related control flow first, then simple if-else control flow otherwise.
+ if (this->GetBlock()->IsLoopTailBlock()) {
+ // We must be looping back to the loop header.
+ if (JUMP == CurrDataFlowType) { // simple case
+ --STARS_SPARK_IndentCount;
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "end loop;\n\n");
+ }
+ else { // conditionally loops back, might fall out of loop if condition is false.
+ // 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");
+ --STARS_SPARK_IndentCount;
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "end loop;\n\n");
+ }
+ }
break;
case INDIR_JUMP:
diff --git a/SMPInstr.h b/SMPInstr.h
index 89cb8381..022660e6 100644
--- a/SMPInstr.h
+++ b/SMPInstr.h
@@ -572,6 +572,7 @@ public:
char *DestString(int OptType);
void PrintDeadRegs(FILE *OutputFile); // print the registers that are dead right before this instruction.
void Dump(void); // Complete debug print, with DEF/USE list, SSA #s, RTL
+ void MDEmitSPARKAdaInvertedCondition(FILE *OutFile); // Invert the condition of the current conditional branch and emit SPARK Ada equivalent.
void EmitSPARKAda(FILE *OutFile); // Emit SPARK-Ada translation of instruction
// Analysis methods
--
GitLab