diff --git a/include/base/SMPDataFlowAnalysis.h b/include/base/SMPDataFlowAnalysis.h
index 8cddee777eeb8e4a23355e8963591839f99e49c5..2132304e905feaf81441743ecca776213c8bb9fd 100644
--- a/include/base/SMPDataFlowAnalysis.h
+++ b/include/base/SMPDataFlowAnalysis.h
@@ -174,7 +174,7 @@ STARSOpndTypePtr CloneIfNecessary(const STARSOpndTypePtr &CurrOp, bool UseFP);
void PrintDefUse(unsigned long feature, int OpNum);
void PrintSIB(const STARSOpndTypePtr &Opnd);
void AnnotPrintSIB(const STARSOpndTypePtr &Opnd, bool HasOffset, FILE *OutFile, char OutString[STARS_MAXSTR], bool Has64BitOperands);
-void SPARKAnnotPrintSIB(const STARSOpndTypePtr &Opnd, bool HasOffset, FILE *OutFile, STARS_regnum_t SegReg, bool UseFP, bool Has64BitOperands);
+void SPARKAnnotPrintSIB(const STARSOpndTypePtr &Opnd, bool HasOffset, FILE *OutFile, STARS_regnum_t SegReg, bool UseFP, bool Has64BitOperands, bool UseSavedStackPtr);
void SPARKAnnotSIBToString(const STARSOpndTypePtr &Opnd, bool HasOffset, std::string &OutString, STARS_regnum_t SegReg, bool UseFP, bool Has64BitOperands);
void PrintOneOperand(const STARSOpndTypePtr &Opnd, uint32_t features, int OpNum);
void PrintListOperand(const STARSOpndTypePtr &Opnd, int SSANum = SMP_SSA_UNINIT);
diff --git a/include/base/SMPFunction.h b/include/base/SMPFunction.h
index cd4683a26a93d040e430686f397418029bcd0419..9976d56514d5ad11e20c07fcc1447f59b823105e 100644
--- a/include/base/SMPFunction.h
+++ b/include/base/SMPFunction.h
@@ -851,6 +851,7 @@ private:
void EmitSPARKArgs(FILE *BodyFile, FILE *HeaderFile, bool Signature, std::size_t LoopIndex) const; // Emit loop function args, as Signature to HeaderFile or proc call to BodyFile.
void EmitSPARKProcPrePostMemConditions(FILE *BodyFile, FILE *HeaderFile, bool PreconditionSection); // Emit mem writing ranges for pre- and post-conditions
bool NeedsSPARKPreconditions(bool &HasLoopMemWrites, bool &HasNonLoopInArgMemWrites, bool &HasCalleeMemWrites); // Determine if any mem writes (or callee mem writes) are not just to the stack frame locals.
+ bool LoopRequiresNonStackPreconditions(size_t LoopIndex) const; // Loop indirect writes require pre-conditions
std::string EmitSPARKProcForLoopHeaderBlock(int LoopIndex, int HeaderBlockNum, int FollowBlockNum, FILE *BodyFile, FILE *HeaderFile); // Create SPARK procedure for loop starting at HeaderBlockNum
void AnalyzeLoopGlobals(int HeaderBlockNum, int FollowBlockNum, bool &MemoryInput, bool &MemoryOutput, std::bitset<1 + MD_LAST_REG_NO> &InputRegs, std::bitset<1 + MD_LAST_REG_NO> &OutputRegs); // Analyze reg and mem accesses in loop
void EmitSPARKLoopProcGlobals(FILE *BodyFile, FILE *HeaderFile, bool MemoryInput, bool MemoryOutput, const std::bitset<1 + MD_LAST_REG_NO> &InputRegs, const std::bitset<1 + MD_LAST_REG_NO> &OutputRegs); // emit Input, Output, In_Out flow annotations
diff --git a/include/base/SMPInstr.h b/include/base/SMPInstr.h
index 562e3f0478d3334b36d5de37dc7b4f0a09a08d0e..634c7a34220f013819f9cd86a5da19201cd9ef2e 100644
--- a/include/base/SMPInstr.h
+++ b/include/base/SMPInstr.h
@@ -175,6 +175,10 @@ inline bool IsRelationalOperator(SMPoperator Oper) {
return ((Oper >= SMP_LESS_THAN) && (Oper <= SMP_ABOVE_EQUAL));
};
+inline bool IsIntegerAddOrSubOperator(SMPoperator Oper) {
+ return ((Oper >= SMP_DECREMENT) && (Oper <= SMP_SUBTRACT_BORROW));
+};
+
// Take RelationalOperator from a comparison instruction, as determined by its matching jump,
// and convert it to the operator needed if the comparison operands are swapped.
// E.g.: cmp rax,rbx followed by ja label1 produces SMP_GREATER_THAN operator.
@@ -401,10 +405,11 @@ public:
inline bool HasRightSubTree(void) const { return (booleans1 & EXPR_SET_RIGHT_SUBTREE); };
inline bool HasLeftSubTree(void) const { return (booleans1 & EXPR_SET_LEFT_SUBTREE); };
bool IsEqualExpr(const STARSExpression *OtherExpr) const; // are exprs identical in operands and operators?
+ bool IsStackPtrPlusOffset(void) const; // Is Expr just the stack pointer plus optional offset constant?
// Printing methods
void Dump(const std::size_t TabCount = 0) const;
- void EmitSPARKAda(FILE *OutputFile, bool ProcessingLoop, bool OldSuffix, bool OffByOne, bool HasLoopArgs = false) const; // Emit SPARK Ada translation of expression to OutputFile, perhaps with Reg'Old suffix.
+ void EmitSPARKAda(FILE *OutputFile, bool ProcessingLoop, bool OldSuffix, bool OffByOne, bool HasLoopArgs, bool UseSavedStackPtr = false) const; // Emit SPARK Ada translation of expression to OutputFile, perhaps with Reg'Old suffix.
void EmitSPARKAdaString(std::string &OutString, bool ProcessingLoop, bool OldSuffix, bool OffByOne) const; // Emit SPARK Ada translation of expression to OutString, perhaps with Reg'Old suffix.
void EmitSPARKInSafeRegion64(FILE *OutputFile, size_t MemWidth) const; // Emit X86.InSafeRegion64(..., X86.RSP) for each byte in memory expr
void PrintSPARKArgLocationStrings(FILE *OutputFile, bool LoopInvariant); // create vector of strings matching loop-function parameters to their incoming locations
@@ -815,9 +820,9 @@ public:
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
// Print an operand in SPARK-Ada form.
- void PrintSPARKAdaOperand(const STARSOpndTypePtr &Opnd, FILE *OutFile, bool LeftHandSide, bool UseFP, bool UseMachinePrefix, bool OmitTrailingSpace);
+ void PrintSPARKAdaOperand(const STARSOpndTypePtr &Opnd, FILE *OutFile, bool LeftHandSide, bool UseFP, bool UseMachinePrefix, bool OmitTrailingSpace, bool UseSavedStackPtr = false);
void SPARKAdaOperandToString(const STARSOpndTypePtr &Opnd, std::string &OutString, bool LeftHandSide, bool UseFP, bool UseMachinePrefix, bool OmitTrailingSpace);
- void PrintSPARKAdaAddressExpr(const STARSOpndTypePtr &Opnd, FILE *OutFile, bool UseFP); // e.g. for [RBP-8] print RBP-8 only
+ void PrintSPARKAdaAddressExpr(const STARSOpndTypePtr &Opnd, FILE *OutFile, bool UseFP, bool UseSavedStackPtr); // e.g. for [RBP-8] print RBP-8 only
void MDEmitSPARKAdaStringOperation(FILE *OutFile); // emit SPARK Ada for string operation, perhaps with repeat prefix that makes it a loop.
void MDEmitSPARKAdaCompareOrTest(FILE *OutFile); // emit SPARK Ada for setting flags only (compare or test opcodes)
void MDEmitSPARKAdaArithmeticSetsCondCodes(FILE *OutFile); // emit SPARK Ada for ops that set flags (add, sub, etc.)
diff --git a/src/base/SMPDataFlowAnalysis.cpp b/src/base/SMPDataFlowAnalysis.cpp
index 0c504fd83837c9e57fcd8b30cbf5de7b23cc8b9e..5c9bb80884f4af5ceccd9102209676ac7bf1944f 100644
--- a/src/base/SMPDataFlowAnalysis.cpp
+++ b/src/base/SMPDataFlowAnalysis.cpp
@@ -840,7 +840,7 @@ void AnnotPrintSIB(const STARSOpndTypePtr &Opnd, bool HasOffset, FILE *OutFile,
} // end AnnotPrintSIB()
// Annotations: concisely print SIB info for an operand.
-void SPARKAnnotPrintSIB(const STARSOpndTypePtr &Opnd, bool HasOffset, FILE *OutFile, STARS_regnum_t SegReg, bool UseFP, bool Has64BitOperands) {
+void SPARKAnnotPrintSIB(const STARSOpndTypePtr &Opnd, bool HasOffset, FILE *OutFile, STARS_regnum_t SegReg, bool UseFP, bool Has64BitOperands, bool UseSavedStackPtr) {
int BaseReg;
int IndexReg;
uint16_t ScaleFactor;
@@ -880,15 +880,25 @@ void SPARKAnnotPrintSIB(const STARSOpndTypePtr &Opnd, bool HasOffset, FILE *OutF
(void) SMP_strncat(OutString, " + ", STARS_MAXSTR-1);
}
#endif
- (void) SMP_strncat(OutString, "X86.", STARS_MAXSTR-1);
- (void) SMP_strncat(OutString, MDGetRegNumName((STARS_regnum_t) BaseReg, ByteWidth), STARS_MAXSTR - 1);
+ if (!(UseSavedStackPtr && (BaseReg == MD_STACK_POINTER_REG))) {
+ (void) SMP_strncat(OutString, "X86.", STARS_MAXSTR - 1);
+ (void) SMP_strncat(OutString, MDGetRegNumName((STARS_regnum_t)BaseReg, ByteWidth), STARS_MAXSTR - 1);
+ }
+ else {
+ (void) SMP_strncat(OutString, "SaveStackPtr", STARS_MAXSTR - 1);
+ }
if (global_STARS_program->GetSTARS_ISA_Bytewidth() > ByteWidth) {
++SubwordAddressRegCount;
}
if (IndexReg != STARS_x86_R_none) {
- (void) SMP_strncat(OutString, " + ", STARS_MAXSTR-1);
- (void) SMP_strncat(OutString, "X86.", STARS_MAXSTR-1);
- (void) SMP_strncat(OutString, MDGetRegNumName((STARS_regnum_t) IndexReg, ByteWidth), STARS_MAXSTR - 1);
+ (void) SMP_strncat(OutString, " + ", STARS_MAXSTR - 1);
+ if (!(UseSavedStackPtr && (IndexReg == MD_STACK_POINTER_REG))) {
+ (void) SMP_strncat(OutString, "X86.", STARS_MAXSTR - 1);
+ (void) SMP_strncat(OutString, MDGetRegNumName((STARS_regnum_t) IndexReg, ByteWidth), STARS_MAXSTR - 1);
+ }
+ else {
+ (void) SMP_strncat(OutString, "SaveStackPtr", STARS_MAXSTR - 1);
+ }
if (global_STARS_program->GetSTARS_ISA_Bytewidth() > ByteWidth) {
++SubwordAddressRegCount;
}
@@ -904,8 +914,13 @@ void SPARKAnnotPrintSIB(const STARSOpndTypePtr &Opnd, bool HasOffset, FILE *OutF
(void) SMP_strncat(OutString, " + ", STARS_MAXSTR-1);
}
#endif
- (void) SMP_strncat(OutString, "X86.", STARS_MAXSTR-1);
- (void) SMP_strncat(OutString, MDGetRegNumName((STARS_regnum_t) IndexReg, ByteWidth), STARS_MAXSTR - 1);
+ if (!(UseSavedStackPtr && (IndexReg == MD_STACK_POINTER_REG))) {
+ (void)SMP_strncat(OutString, "X86.", STARS_MAXSTR - 1);
+ (void)SMP_strncat(OutString, MDGetRegNumName((STARS_regnum_t)IndexReg, ByteWidth), STARS_MAXSTR - 1);
+ }
+ else {
+ (void)SMP_strncat(OutString, "SaveStackPtr", STARS_MAXSTR - 1);
+ }
if (global_STARS_program->GetSTARS_ISA_Bytewidth() > ByteWidth) {
++SubwordAddressRegCount;
}
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index 1fb0d67adabab670c098e1b21edbc18d1fe4f140..232dd83f2b8c56ab615b81d83c0deff21a0a69a5 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -6796,11 +6796,11 @@ STARSExpression* SMPFunction::CreateIterationsExpr(std::size_t LoopIndex, const
// For now, we will limit ourselves to BIVars with a loop update of BIV += 1 or BIV -= 1.
bool SimpleBIV = (IVFamily.BasicInductionVar.Multiplier.GetOp()->IsImmedOp()
&& (IVFamily.BasicInductionVar.Multiplier.GetOp()->GetImmedValue() == 1)
- && IVFamily.BasicInductionVar.Addend.GetOp()->IsImmedOp()
- && (1 == IVFamily.BasicInductionVar.Addend.GetOp()->GetImmedValue()));
+ && IVFamily.BasicInductionVar.Addend.GetOp()->IsImmedOp());
if (!SimpleBIV)
return nullptr;
+ STARS_uval_t IncDecValue = IVFamily.BasicInductionVar.Addend.GetOp()->GetImmedValue();
bool PositiveIncrement = (!IVFamily.BasicInductionVar.SubtractAddend);
bool BottomTestingLoop = (this->LoopTypesByLoopNum[LoopIndex] == STARS_BOTTOM_TESTING_LOOP);
@@ -6812,24 +6812,40 @@ STARSExpression* SMPFunction::CreateIterationsExpr(std::size_t LoopIndex, const
// Y Y >= (Limit - Init) / 1
// Y Y < undefined
// Y Y <= undefined
+ // Y Y == (Limit - Init) / 1
+ // Y Y != undefined
// Y N > undefined
// Y N >= undefined
// Y N < (Limit - Init) / 1
// Y N <= (Limit + 1 - Init) / 1
- // N Y > (Limit + 2 - Init) / 1
- // N Y >= (Limit + 1 - Init) / 1
+ // Y N == undefined
+ // Y N != (Limit - Init) / 1
+ // N Y > (Limit + 1 - Init) / 1
+ // N Y >= (Limit - Init) / 1
// N Y < undefined
// N Y <= undefined
+ // N Y == (Limit - Init) / 1
+ // N Y != undefined
// N N > undefined
// N N >= undefined
- // N N < (Limit + 1 - Init) / 1
- // N N <= (Limit + 2 - Init) / 1
+ // N N < (Limit - Init) / 1
+ // N N <= (Limit + 1 - Init) / 1
+ // N N == undefined
+ // N N != (Limit - Init) / 1
//
- // We see that certain COND_BRANCH relational operators add 1 to the iteration count, and
- // bottom-testing loops execute once more than top-testing loops with the same COND_BRANCH.
+ // We see that certain COND_BRANCH relational operators add 1 to the iteration count.
// Certain combinations make no sense, e.g. counting up by 1 from Init to Limit while exiting
// the loop when BIV < Limit. Some of these cases could be zero-trip loops that we will analyze
// in greater depth later.
+ // NOTE: There is no difference between top-testing and bottom-testing loops in the table.
+ // That is because the only difference in practice is the possibility that a top-testing loop
+ // executes zero iterations, while the bottom-testing version of the loop would execute one
+ // iteration in that case. If we have security properties that depend on identifying zero-trip
+ // loops, we will need a separate analysis later.
+ // NOTE: In these tables, we assume that == and != are used properly. There is the possibility
+ // that someone could write code such as: for (i = 0; i != limit; i += 8) and have a limit
+ // that is not a multiple of 8. Again, we will need a special-case analysis if we want to detect
+ // the possibility of such an infinite loop.
// For loops with a BIV that counts downward by 1:
//
@@ -6848,6 +6864,10 @@ STARSExpression* SMPFunction::CreateIterationsExpr(std::size_t LoopIndex, const
// N N == undefined
// N N != (Init - Limit) / 1
+ // We can generalize the formulae above to allow increment or decrement by values other than 1.
+ // Whenever we add 1 in the numerator, just add the increment or decrement value.
+ // Whenever we divide by 1 in the denominator, divide by the increment or decrement value.
+
// Weed out undefined cases.
bool Undefined = false;
assert(LoopIndex < this->LoopComparisonExprs.size());
@@ -6855,11 +6875,11 @@ STARSExpression* SMPFunction::CreateIterationsExpr(std::size_t LoopIndex, const
if (PositiveIncrement) {
if (this->LoopComparisonExprs[LoopIndex].ExitsLoop) {
Undefined = ((BranchOperator != SMP_GREATER_THAN) && (BranchOperator != SMP_GREATER_EQUAL)
- && (BranchOperator != SMP_ABOVE) && (BranchOperator != SMP_ABOVE_EQUAL));
+ && (BranchOperator != SMP_ABOVE) && (BranchOperator != SMP_ABOVE_EQUAL) && (BranchOperator != SMP_EQUAL));
}
else {
Undefined = ((BranchOperator != SMP_LESS_THAN) && (BranchOperator != SMP_LESS_EQUAL)
- && (BranchOperator != SMP_BELOW) && (BranchOperator != SMP_BELOW_EQUAL));
+ && (BranchOperator != SMP_BELOW) && (BranchOperator != SMP_BELOW_EQUAL) && (BranchOperator != SMP_NOT_EQUAL));
}
}
else { // Decrement by one on each iteration
@@ -6875,39 +6895,39 @@ STARSExpression* SMPFunction::CreateIterationsExpr(std::size_t LoopIndex, const
if (Undefined)
return nullptr;
+ STARSOpndTypePtr IncDecOp = InitExpr->GetParentInst()->MakeImmediateOpnd(IncDecValue);
STARS_sval_t LimitIncrease = 0;
if (PositiveIncrement) {
- if (BottomTestingLoop) {
- LimitIncrease += 1;
- }
if ((BranchOperator == SMP_LESS_EQUAL) || (BranchOperator == SMP_GREATER_THAN)
|| (BranchOperator == SMP_BELOW_EQUAL) || (BranchOperator == SMP_ABOVE)) {
- LimitIncrease += 1; // only because we weeded out some undefined cases; change if we redefine those cases.
+ LimitIncrease += IncDecValue; // only because we weeded out some undefined cases; change if we redefine those cases.
}
}
else { // Decrement
if ((BranchOperator == SMP_LESS_THAN) || (BranchOperator == SMP_GREATER_EQUAL)
|| (BranchOperator == SMP_BELOW) || (BranchOperator == SMP_ABOVE_EQUAL)) {
- LimitIncrease += 1;
+ LimitIncrease += IncDecValue;
}
}
bool NeedLimitIncrease = (0 != LimitIncrease);
- // At this point, the iteration count is (Limit + LimitIncrease - Init) / 1 for the SimpleBIV cases
- // with PositiveIncrement, and (Init + LimitIncrease - Limit) / 1 for the Decrement case.
- // We will omit the division by 1, of course, although SimplifyExpr() should remove it.
+ // At this point, the iteration count is (Limit + LimitIncrease - Init) / IncDecValue for the SimpleBIV cases
+ // with PositiveIncrement, and (Init + LimitIncrease - Limit) / IncDecValue for the Decrement case.
+ // We will omit the division by 1 case, of course, although SimplifyExpr() should remove it.
// If Init is a constant, then we can fold (LimitIncrease - Init) or (Init + LimitIncrease) into a constant operand.
STARSExpression *IterationsExpr = new STARSExpression();
IterationsExpr->SetParentInst(LimitExpr->GetParentInst());
IterationsExpr->SetParentFunc(this);
+ bool LimitIncreaseFolded = false;
if (PositiveIncrement) {
if ((InitExpr->GetOperator() == SMP_ASSIGN) && InitExpr->GetLeftOperand()->IsImmedOp()) {
// Only LeftOperand is valid, and it is a constant.
- STARS_sval_t InitValue = (STARS_sval_t)InitExpr->GetLeftOperand()->GetImmedValue();
+ STARS_sval_t InitValue = (STARS_sval_t) InitExpr->GetLeftOperand()->GetImmedValue();
LimitIncrease -= InitValue;
- STARSOpndTypePtr RightOp = InitExpr->GetParentInst()->MakeImmediateOpnd((STARS_uval_t)LimitIncrease);
+ STARSOpndTypePtr RightOp = InitExpr->GetParentInst()->MakeImmediateOpnd((STARS_uval_t) LimitIncrease);
IterationsExpr->SetRightOperand(RightOp);
+ LimitIncreaseFolded = true;
NeedLimitIncrease = false; // already in IterationsExpr
}
else { // non-constant InitExpr
@@ -6939,7 +6959,7 @@ STARSExpression* SMPFunction::CreateIterationsExpr(std::size_t LoopIndex, const
}
IterationsExpr->SetLeftTree(LeftExpr);
}
- else { // just need LimitExpr right hand side as left tree or operand.
+ else if (LimitIncreaseFolded) { // just need LimitExpr right hand side as left tree or operand.
IterationsExpr->SetOperator(SMP_ADD); // LimitExpr RHS + (folded LimitIncrease - InitExpr)
// If LimitExpr RHS is just an operand, make it the LeftOperand, else make it the LeftTree.
if (!LimitExpr->HasRightSubTree()) { // just RightOperand
@@ -6951,6 +6971,10 @@ STARSExpression* SMPFunction::CreateIterationsExpr(std::size_t LoopIndex, const
IterationsExpr->SetLeftTree(LimitExpr->GetRightTree());
}
}
+ else { // never folded, no LimitIncrease, just LimitExpr - InitExpr
+ IterationsExpr->SetOperator(SMP_SUBTRACT);
+ IterationsExpr->SetLeftTree(LimitExpr);
+ }
} // end if PositiveIncrement
else { // decrement case
if ((InitExpr->GetOperator() == SMP_ASSIGN) && InitExpr->GetLeftOperand()->IsImmedOp()) {
@@ -6959,6 +6983,7 @@ STARSExpression* SMPFunction::CreateIterationsExpr(std::size_t LoopIndex, const
LimitIncrease += InitValue;
STARSOpndTypePtr LeftOp = InitExpr->GetParentInst()->MakeImmediateOpnd((STARS_uval_t) LimitIncrease);
IterationsExpr->SetLeftOperand(LeftOp);
+ LimitIncreaseFolded = true;
NeedLimitIncrease = false; // already in IterationsExpr
}
else { // non-constant InitExpr
@@ -7003,7 +7028,26 @@ STARSExpression* SMPFunction::CreateIterationsExpr(std::size_t LoopIndex, const
}
} // end .. else decrement case
- return IterationsExpr;
+ // We want to simplify the resulting expression before we divide by IncDecValue.
+ // The division otherwise might have to have complex simplifications. E.g. if we
+ // have InitExpr of RSP-200 and LimitExpr of RSP-100 and IncDecValue of 4, we prefer
+ // to simplify ((RSP - 100) - (RSP - 200)) to 100 and then return 100 / 4. Our
+ // caller will call SimplifyExpr() on the expr we return.
+ assert(nullptr != IterationsExpr);
+ bool Simplified = IterationsExpr->SimplifyExpr(nullptr);
+ if (IncDecValue != 1) {
+ // Divide by IncDecOp.
+ STARSExpression *NewIterExpr = new STARSExpression();
+ NewIterExpr->SetParentInst(LimitExpr->GetParentInst());
+ NewIterExpr->SetParentFunc(this);
+ NewIterExpr->SetOperator(SMP_U_DIVIDE);
+ NewIterExpr->SetRightOperand(IncDecOp);
+ NewIterExpr->SetLeftTree(IterationsExpr);
+ return NewIterExpr;
+ }
+ else {
+ return IterationsExpr;
+ }
} // end of SMPFunction::CreateIterationsExpr()
// Create a Memory range expression for indirect or indexed memory writes in the loop
@@ -14223,174 +14267,10 @@ void SMPFunction::EmitFuncSPARKAda(void) {
}
SMP_fprintf(HeaderFile, "),\n"); // close Globals section parenthesis
- // Emit memory writing range pre-conditions.
+ // Emit memory writing range pre-conditions and post-conditions.
bool HasLoopMemWrites = ((this->LoopCount > 0) && this->MemRangeRegsBitmap.any());
-#if 1
this->EmitSPARKProcPrePostMemConditions(BodyFile, HeaderFile, true);
-#else
- bool HasLoopMemWrites = ((this->LoopCount > 0) && this->MemRangeRegsBitmap.any());
- bool HasNonLoopInArgMemWrites = (!this->InArgsUsedInMemWrites.empty());
- bool HasCalleeMemWrites = (!this->MemAddrExprsFromCallees.empty());
- if (!HasNonLoopInArgMemWrites) {
- size_t OutputCount = 0;
- if (HasLoopMemWrites) {
- SMP_fprintf(HeaderFile, "\tPre => (for all i in Unsigned64 => (if X86.InMemoryRange(i, ");
- for (size_t LoopIndex = 0; LoopIndex < this->LoopCount; ++LoopIndex) {
- if (0 < OutputCount) {
- SMP_fprintf(HeaderFile, "\n\t\t or X86.InMemoryRange(i, ");
- }
- this->LoopMemWriteLowerBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, false, false);
- SMP_fprintf(HeaderFile, ", ");
- this->LoopMemWriteUpperBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, false, false);
- SMP_fprintf(HeaderFile, ") ");
- ++OutputCount;
- }
- }
- if (HasCalleeMemWrites) {
- if (0 == OutputCount) {
- SMP_fprintf(HeaderFile, "\tPre => (for all i in Unsigned64 => (");
- }
- for (size_t i = 0; i < this->MemAddrExprWidthsFromCallees.size(); ++i) {
- // Easier in this loop to use X86.InRange64(i, X86.RAX, 8) than to use X86.InMemoryRange(i, X86.RAX, X86.RAX+8)
- // which would require printing the same operand twice.
- if (0 < OutputCount) {
- SMP_fprintf(HeaderFile, "\n\t\t or X86.InRange64(i, ");
- }
- else {
- SMP_fprintf(HeaderFile, "if X86.InRange64(i, ");
- }
- (*this->MemAddrExprWidthsFromCallees[i].first)->EmitSPARKAda(HeaderFile, false, false, false);
- SMP_fprintf(HeaderFile, ", %u)", this->MemAddrExprWidthsFromCallees[i].second);
- ++OutputCount;
- }
- }
- if (0 < OutputCount) {
- SMP_fprintf(HeaderFile, " then\n\t\tX86.InSafeRegion64(i, X86.RSP))),\n");
- }
- }
- else {
- SMP_fprintf(HeaderFile, "\tPre => (for all i in Unsigned64 => (");
- size_t OutputCount = 0;
- if (HasLoopMemWrites) {
- for (size_t LoopIndex = 0; LoopIndex < this->LoopCount; ++LoopIndex) {
- if (0 < OutputCount) {
- SMP_fprintf(HeaderFile, "\n\t\t or X86.InMemoryRange(i, ");
- }
- else {
- SMP_fprintf(HeaderFile, "if X86.InMemoryRange(i, ");
- }
- this->LoopMemWriteLowerBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, false, false);
- SMP_fprintf(HeaderFile, ", ");
- this->LoopMemWriteUpperBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, false, false);
- SMP_fprintf(HeaderFile, ") ");
- ++OutputCount;
- }
- }
-
- STARSExpression *PreviousExpr = nullptr;
- for (size_t i = 0; i < this->InArgsUsedInMemWrites.size(); ++i) {
- STARSExpression *InArgExpr = this->InArgsUsedInMemWrites[i];
- // Avoid duplicate output.
- if (nullptr == PreviousExpr) {
- PreviousExpr = InArgExpr;
- }
- else if (PreviousExpr->IsEqualExpr(InArgExpr)) {
- continue;
- }
- else {
- PreviousExpr = InArgExpr;
- }
-
- // Easier in this loop to use X86.InRange64(i, X86.RAX, 8) than to use X86.InMemoryRange(i, X86.RAX, X86.RAX+8)
- // which would require printing the same operand twice.
- if (0 < OutputCount) {
- SMP_fprintf(HeaderFile, "\n\t\t or X86.InRange64(i, ");
- }
- else {
- SMP_fprintf(HeaderFile, "if X86.InRange64(i, ");
- }
- InArgExpr->EmitSPARKAda(HeaderFile, false, false, false);
- SMP_fprintf(HeaderFile, ", %u)", this->InArgsUsedInMemWriteByteWidths[i]);
- ++OutputCount;
- }
-
- if (HasCalleeMemWrites) {
- if (0 == OutputCount) {
- SMP_fprintf(HeaderFile, "\tPre => (for all i in Unsigned64 => (");
- }
- for (size_t i = 0; i < this->MemAddrExprWidthsFromCallees.size(); ++i) {
- // Easier in this loop to use X86.InRange64(i, X86.RAX, 8) than to use X86.InMemoryRange(i, X86.RAX, X86.RAX+8)
- // which would require printing the same operand twice.
- if (0 < OutputCount) {
- SMP_fprintf(HeaderFile, "\n\t\t or X86.InRange64(i, ");
- }
- else {
- SMP_fprintf(HeaderFile, "if X86.InRange64(i, ");
- }
- (*this->MemAddrExprWidthsFromCallees[i].first)->EmitSPARKAda(HeaderFile, false, false, false);
- SMP_fprintf(HeaderFile, ", %u)", this->MemAddrExprWidthsFromCallees[i].second);
- ++OutputCount;
- }
- }
-
- SMP_fprintf(HeaderFile, " then\n\t\tX86.InSafeRegion64(i, X86.RSP))),\n");
- }
-#endif
-
-#if 1
this->EmitSPARKProcPrePostMemConditions(BodyFile, HeaderFile, false);
-#else
- if (this->AltersSPARKMemory()) {
- 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))");
- }
- else {
- SMP_fprintf(HeaderFile, "\tPost => (X86.RSP = (X86.RSP'Old + 8))");
- }
- if (this->PreservedRegsBitmap.any()) {
- size_t RegLimit = this->PreservedRegsBitmap.size();
- if (RegLimit > STARS_x86_R_r15) {
- RegLimit = STARS_x86_R_r15; // last full-width general purpose reg
- }
- for (size_t RegIndex = 0; RegIndex <= RegLimit; ++RegIndex) {
- if (this->IsRegPreserved(RegIndex)) {
- const char *RegName = MDGetSPARKRegNumName((STARS_regnum_t) RegIndex, ByteWidth);
- SMP_fprintf(HeaderFile, " and\n\t\t(X86.%s = X86.%s'Old)", RegName, RegName);
- }
- }
- }
-
- // Emit memory writing range post-conditions.
- if (HasLoopMemWrites) {
- size_t OutputCount = 0;
- SMP_fprintf(HeaderFile, "\tand \n\t(for all i in Unsigned64 => (if not X86.InMemoryRange(i, ");
- for (size_t LoopIndex = 0; LoopIndex < this->LoopCount; ++LoopIndex) {
- if (0 < OutputCount) {
- SMP_fprintf(HeaderFile, "\n\t\t and not X86.InMemoryRange(i, ");
- }
- this->LoopMemWriteLowerBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, true, false);
- SMP_fprintf(HeaderFile, ", ");
- this->LoopMemWriteUpperBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, true, false);
- SMP_fprintf(HeaderFile, ") ");
- ++OutputCount;
- }
- SMP_fprintf(HeaderFile, "\n\t\tand X86.InSafeRegion64(i, X86.RSP'Old)");
- SMP_fprintf(HeaderFile, " then\n\t\t(X86.Memory(i) = X86.Memory'Old(i))))");
- }
- else if (this->AltersSPARKMemory()) {
- SMP_fprintf(HeaderFile, "\tand \n\t(for all i in Unsigned64 => (if X86.InSafeRegion64(i, X86.RSP'Old)");
- SMP_fprintf(HeaderFile, " then\n\t\t(X86.Memory(i) = X86.Memory'Old(i))))");
- }
-
- SMP_fprintf(HeaderFile, ";\n\n"); // terminate the postcondition section
-#endif
// Begin recursive descent translation with entry block.
SMPBasicBlock *CurrBlock = this->RPOBlocks[0];
@@ -14523,9 +14403,9 @@ void SMPFunction::EmitSPARKProcPrePostMemConditions(FILE *BodyFile, FILE *Header
else
SMP_fprintf(HeaderFile, "\n\t\t and not X86.InMemoryRange(i, ");
}
- this->LoopMemWriteLowerBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false);
+ this->LoopMemWriteLowerBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false, false);
SMP_fprintf(HeaderFile, ", ");
- this->LoopMemWriteUpperBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false);
+ this->LoopMemWriteUpperBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false, false);
SMP_fprintf(HeaderFile, ") ");
++OutputCount;
}
@@ -14546,7 +14426,7 @@ void SMPFunction::EmitSPARKProcPrePostMemConditions(FILE *BodyFile, FILE *Header
assert(PreconditionSection);
SMP_fprintf(HeaderFile, "if X86.InRange64(i, ");
}
- (*this->MemAddrExprWidthsFromCallees[i].first)->EmitSPARKAda(HeaderFile, false, false, false);
+ (*this->MemAddrExprWidthsFromCallees[i].first)->EmitSPARKAda(HeaderFile, false, false, false, false);
SMP_fprintf(HeaderFile, ", %u)", this->MemAddrExprWidthsFromCallees[i].second);
++OutputCount;
}
@@ -14573,9 +14453,9 @@ void SMPFunction::EmitSPARKProcPrePostMemConditions(FILE *BodyFile, FILE *Header
assert(PreconditionSection);
SMP_fprintf(HeaderFile, "if X86.InMemoryRange(i, ");
}
- this->LoopMemWriteLowerBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false);
+ this->LoopMemWriteLowerBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false, false);
SMP_fprintf(HeaderFile, ", ");
- this->LoopMemWriteUpperBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false);
+ this->LoopMemWriteUpperBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false, false);
SMP_fprintf(HeaderFile, ") ");
++OutputCount;
}
@@ -14609,7 +14489,7 @@ void SMPFunction::EmitSPARKProcPrePostMemConditions(FILE *BodyFile, FILE *Header
assert(PreconditionSection);
SMP_fprintf(HeaderFile, "if X86.InRange64(i, ");
}
- InArgExpr->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false);
+ InArgExpr->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false, false);
SMP_fprintf(HeaderFile, ", %u)", this->InArgsUsedInMemWriteByteWidths[i]);
++OutputCount;
}
@@ -14629,7 +14509,7 @@ void SMPFunction::EmitSPARKProcPrePostMemConditions(FILE *BodyFile, FILE *Header
assert(PreconditionSection);
SMP_fprintf(HeaderFile, "if X86.InRange64(i, ");
}
- (*this->MemAddrExprWidthsFromCallees[i].first)->EmitSPARKAda(HeaderFile, false, false, false);
+ (*this->MemAddrExprWidthsFromCallees[i].first)->EmitSPARKAda(HeaderFile, false, false, false, false);
SMP_fprintf(HeaderFile, ", %u)", this->MemAddrExprWidthsFromCallees[i].second);
++OutputCount;
}
@@ -14745,9 +14625,9 @@ void SMPFunction::EmitSPARKProcPrePostMemConditions(FILE *BodyFile, FILE *Header
else
SMP_fprintf(HeaderFile, "\n\t\t and not X86.InMemoryRange(i, ");
}
- this->LoopMemWriteLowerBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false);
+ this->LoopMemWriteLowerBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false, false);
SMP_fprintf(HeaderFile, ", ");
- this->LoopMemWriteUpperBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false);
+ this->LoopMemWriteUpperBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false, false);
SMP_fprintf(HeaderFile, ") ");
++OutputCount;
}
@@ -14774,7 +14654,7 @@ void SMPFunction::EmitSPARKProcPrePostMemConditions(FILE *BodyFile, FILE *Header
(*this->MemAddrExprWidthsFromCallees[i].first)->EmitSPARKInSafeRegion64(HeaderFile, MemWidth);
}
else {
- (*this->MemAddrExprWidthsFromCallees[i].first)->EmitSPARKAda(HeaderFile, false, false, false);
+ (*this->MemAddrExprWidthsFromCallees[i].first)->EmitSPARKAda(HeaderFile, false, false, false, false);
SMP_fprintf(HeaderFile, ", %u)", this->MemAddrExprWidthsFromCallees[i].second);
}
++OutputCount;
@@ -14805,9 +14685,9 @@ void SMPFunction::EmitSPARKProcPrePostMemConditions(FILE *BodyFile, FILE *Header
assert(PreconditionSection);
SMP_fprintf(HeaderFile, "if X86.InMemoryRange(i, ");
}
- this->LoopMemWriteLowerBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false);
+ this->LoopMemWriteLowerBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false, false);
SMP_fprintf(HeaderFile, ", ");
- this->LoopMemWriteUpperBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false);
+ this->LoopMemWriteUpperBoundsExprs[LoopIndex]->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false, false);
SMP_fprintf(HeaderFile, ") ");
++OutputCount;
}
@@ -14847,7 +14727,7 @@ void SMPFunction::EmitSPARKProcPrePostMemConditions(FILE *BodyFile, FILE *Header
InArgExpr->EmitSPARKInSafeRegion64(HeaderFile, MemWidth);
}
else {
- InArgExpr->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false);
+ InArgExpr->EmitSPARKAda(HeaderFile, false, !PreconditionSection, false, false);
SMP_fprintf(HeaderFile, ", %u)", this->InArgsUsedInMemWriteByteWidths[i]);
}
++OutputCount;
@@ -14872,7 +14752,7 @@ void SMPFunction::EmitSPARKProcPrePostMemConditions(FILE *BodyFile, FILE *Header
(*this->MemAddrExprWidthsFromCallees[i].first)->EmitSPARKInSafeRegion64(HeaderFile, MemWidth);
}
else {
- (*this->MemAddrExprWidthsFromCallees[i].first)->EmitSPARKAda(HeaderFile, false, false, false);
+ (*this->MemAddrExprWidthsFromCallees[i].first)->EmitSPARKAda(HeaderFile, false, false, false, false);
SMP_fprintf(HeaderFile, ", %u)", this->MemAddrExprWidthsFromCallees[i].second);
}
++OutputCount;
@@ -15068,9 +14948,9 @@ string SMPFunction::EmitSPARKProcForLoopHeaderBlock(int LoopIndex, int HeaderBlo
STARS_sval_t IncomingStackDelta = FirstInst->GetStackPtrOffset();
if (UsesStackPtrRegs) {
if (0 != IncomingStackDelta)
- SMP_fprintf(BodyFile, "\tentryRSP : Unsigned64 := X86.RSP + %d with Ghost;\n", (0 - IncomingStackDelta));
+ SMP_fprintf(BodyFile, "\tSaveStackPtr : Unsigned64 := X86.RSP + %d with Ghost;\n", (0 - IncomingStackDelta));
else
- SMP_fprintf(BodyFile, "\tentryRSP : Unsigned64 := X86.RSP with Ghost;\n");
+ SMP_fprintf(BodyFile, "\tSaveStackPtr : Unsigned64 := X86.RSP with Ghost;\n");
if (UseFP) {
SMP_fprintf(BodyFile, "\tsavedRBP : Unsigned64 := X86.ReadMem64(X86.RBP) with Ghost;");
}
@@ -15092,7 +14972,7 @@ string SMPFunction::EmitSPARKProcForLoopHeaderBlock(int LoopIndex, int HeaderBlo
this->EmitSPARKLoopProcGlobals(BodyFile, HeaderFile, MemoryInput, MemoryOutput, LoopInputRegs, LoopOutputRegs);
// Emit pre-conditions.
- bool HasNonStackPreconditions = ((nullptr != this->LoopIterationsInitExprs[LoopIndex]) && (nullptr != this->LoopMemWriteLowerBoundsExprs[LoopIndex]));
+ bool HasNonStackPreconditions = this->LoopRequiresNonStackPreconditions(LoopIndex);
bool HasPreconditions = (HasNonStackPreconditions || (UseFP && UsesStackPtrRegs));
this->LoopHasPreconditions[LoopIndex] = HasPreconditions;
if (HasPreconditions) {
@@ -15105,13 +14985,15 @@ string SMPFunction::EmitSPARKProcForLoopHeaderBlock(int LoopIndex, int HeaderBlo
else {
SMP_fprintf(HeaderFile, "(X86.RBP = X86.RSP + %d)", RBPRSPDelta);
}
- }
- if (!HasNonStackPreconditions) {
- SMP_fprintf(HeaderFile, ",\n"); // finished with preconditions
+ if (!HasNonStackPreconditions) {
+ SMP_fprintf(HeaderFile, ",\n"); // finished with preconditions
+ }
+ else {
+ SMP_fprintf(HeaderFile, " and \n\t"); // prepare for more preconditions
+ }
}
else { // Need preconditions for memory writing range
- if ((nullptr != this->LoopIterationsInitExprs[LoopIndex]) && (nullptr != this->LoopMemWriteLowerBoundsExprs[LoopIndex])) {
- SMP_fprintf(HeaderFile, " and \n\t (");
+ if (HasNonStackPreconditions) {
STARSInductionVarFamilyList::const_iterator BIVIter = this->LoopAnalyzedBIVIters[LoopIndex];
assert(BIVIter != this->LoopInductionVars[LoopIndex].cend());
STARS_ea_t BIVInitAddr = BIVIter->BIVIncomingDefAddr;
@@ -15119,6 +15001,7 @@ string SMPFunction::EmitSPARKProcForLoopHeaderBlock(int LoopIndex, int HeaderBlo
SMPInstr *BIVInitInst = this->GetInstFromAddr(BIVInitAddr);
assert(nullptr != BIVInitInst);
STARSOpndTypePtr BIVDefOp = BIVInitInst->GetFirstLeftOperandNoNorm();
+ SMP_fprintf(HeaderFile, " (");
FirstInst->PrintSPARKAdaOperand(BIVDefOp, HeaderFile, false, UseFP, true, false);
SMP_fprintf(HeaderFile, "= ");
this->LoopIterationsInitExprs[LoopIndex]->EmitSPARKAda(HeaderFile, true, false, false, HasArgs);
@@ -15141,6 +15024,18 @@ string SMPFunction::EmitSPARKProcForLoopHeaderBlock(int LoopIndex, int HeaderBlo
return ProcName;
} // end of SMPFunction::EmitSPARKProcForLoopHeaderBlock()
+bool SMPFunction::LoopRequiresNonStackPreconditions(size_t LoopIndex) const {
+ bool LoopWritePreconditions = ((nullptr != this->LoopIterationsInitExprs[LoopIndex])
+ && (nullptr != this->LoopMemWriteLowerBoundsExprs[LoopIndex])
+ && (nullptr != this->LoopMemWriteUpperBoundsExprs[LoopIndex]));
+ if (LoopWritePreconditions) {
+ LoopWritePreconditions = ((!this->LoopIterationsInitExprs[LoopIndex]->IsStackPtrPlusOffset())
+ && (!this->LoopMemWriteLowerBoundsExprs[LoopIndex]->IsStackPtrPlusOffset())
+ && (!this->LoopMemWriteUpperBoundsExprs[LoopIndex]->IsStackPtrPlusOffset()));
+ }
+ return LoopWritePreconditions;
+} // end of SMPFunction::LoopRequiresNonStackPreconditions()
+
// Analyze reg and mem accesses in loop
void SMPFunction::AnalyzeLoopGlobals(int HeaderBlockNum, int FollowBlockNum, bool &MemoryInput, bool &MemoryOutput, std::bitset<1 + MD_LAST_REG_NO> &InputRegs, std::bitset<1 + MD_LAST_REG_NO> &OutputRegs) {
assert((0 <= HeaderBlockNum) && (HeaderBlockNum < this->RPOBlocks.size()));
diff --git a/src/base/SMPInstr.cpp b/src/base/SMPInstr.cpp
index a359ffcb87b0c125732e33e488e7d37015640336..bc4a120abe6f7f2fe2777c92ccca1a1c71839b02 100644
--- a/src/base/SMPInstr.cpp
+++ b/src/base/SMPInstr.cpp
@@ -437,7 +437,7 @@ void PrintSPARKIndentTabs(FILE *OutFile) {
}
// Print an operand in SPARK-Ada form.
-void SMPInstr::PrintSPARKAdaOperand(const STARSOpndTypePtr &Opnd, FILE *OutFile, bool LeftHandSide, bool UseFP, bool UseMachinePrefix, bool OmitTrailingSpace) {
+void SMPInstr::PrintSPARKAdaOperand(const STARSOpndTypePtr &Opnd, FILE *OutFile, bool LeftHandSide, bool UseFP, bool UseMachinePrefix, bool OmitTrailingSpace, bool UseSavedStackPtr) {
std::size_t OpndByteWidth = Opnd->GetByteWidth();
bool MemOpnd = IsMemOperand(Opnd);
bool SubwordWidth = (global_STARS_program->GetSTARS_ISA_Bytewidth() > OpndByteWidth);
@@ -457,7 +457,7 @@ void SMPInstr::PrintSPARKAdaOperand(const STARSOpndTypePtr &Opnd, FILE *OutFile,
if (Opnd->IsStaticMemOp()) {
if (Opnd->HasSIBByte()) {
SMP_fprintf(OutFile, " %s ", MemWriteString);
- SPARKAnnotPrintSIB(Opnd, true, OutFile, Opnd->GetSegReg(), UseFP, this->MDHas64BitOperands());
+ SPARKAnnotPrintSIB(Opnd, true, OutFile, Opnd->GetSegReg(), UseFP, this->MDHas64BitOperands(), UseSavedStackPtr);
SMP_fprintf(OutFile, " + 16#%llx# )", (unsigned long long) Opnd->GetAddr());
}
else {
@@ -470,7 +470,7 @@ void SMPInstr::PrintSPARKAdaOperand(const STARSOpndTypePtr &Opnd, FILE *OutFile,
else if (Opnd->IsMemNoDisplacementOp()) {
if (Opnd->HasSIBByte()) { // has SIB info
SMP_fprintf(OutFile, " %s ", MemWriteString);
- SPARKAnnotPrintSIB(Opnd, false, OutFile, Opnd->GetSegReg(), UseFP, this->MDHas64BitOperands());
+ SPARKAnnotPrintSIB(Opnd, false, OutFile, Opnd->GetSegReg(), UseFP, this->MDHas64BitOperands(), UseSavedStackPtr);
}
else { // no SIB info
STARS_regnum_t BaseReg = Opnd->GetReg();
@@ -486,7 +486,12 @@ void SMPInstr::PrintSPARKAdaOperand(const STARSOpndTypePtr &Opnd, FILE *OutFile,
}
else {
#endif
- SMP_fprintf(OutFile, " %s X86.%s ", MemWriteString, MDGetRegName(BaseOp));
+ if (!(UseSavedStackPtr && (BaseReg == MD_STACK_POINTER_REG))) {
+ SMP_fprintf(OutFile, " %s X86.%s ", MemWriteString, MDGetRegName(BaseOp));
+ }
+ else {
+ SMP_fprintf(OutFile, " %s SaveStackPtr ", MemWriteString);
+ }
#if STARS_SPARK_EMIT_SEGMENT_REGS
}
#endif
@@ -506,7 +511,7 @@ void SMPInstr::PrintSPARKAdaOperand(const STARSOpndTypePtr &Opnd, FILE *OutFile,
int SignedOffset = (int) offset;
if (Opnd->HasSIBByte()) {
SMP_fprintf(OutFile, " %s ", MemWriteString);
- SPARKAnnotPrintSIB(Opnd, (SignedOffset != 0), OutFile, Opnd->GetSegReg(), UseFP, this->MDHas64BitOperands());
+ SPARKAnnotPrintSIB(Opnd, (SignedOffset != 0), OutFile, Opnd->GetSegReg(), UseFP, this->MDHas64BitOperands(), false);
if (SignedOffset > 0) // print plus sign
SMP_fprintf(OutFile, "+ 16#%x# )", (unsigned int) SignedOffset);
else if (SignedOffset < 0) // minus sign will print automatically
@@ -527,7 +532,12 @@ void SMPInstr::PrintSPARKAdaOperand(const STARSOpndTypePtr &Opnd, FILE *OutFile,
}
else {
#endif
- SMP_fprintf(OutFile, " %s X86.%s ", MemWriteString, MDGetRegName(BaseOp));
+ if (!(UseSavedStackPtr && (BaseReg == MD_STACK_POINTER_REG))) {
+ SMP_fprintf(OutFile, " %s X86.%s ", MemWriteString, MDGetRegName(BaseOp));
+ }
+ else {
+ SMP_fprintf(OutFile, " %s SaveStackPtr ", MemWriteString);
+ }
#if STARS_SPARK_EMIT_SEGMENT_REGS
}
#endif
@@ -544,7 +554,11 @@ void SMPInstr::PrintSPARKAdaOperand(const STARSOpndTypePtr &Opnd, FILE *OutFile,
}
}
else if (Opnd->IsRegOp()) {
- if (SubwordWidth && LeftHandSide) {
+ if (UseSavedStackPtr && Opnd->MatchesReg(MD_STACK_POINTER_REG)) {
+ assert(!LeftHandSide);
+ SMP_fprintf(OutFile, " SaveStackPtr");
+ }
+ else if (SubwordWidth && LeftHandSide) {
// Subword reg writes are procedure calls, e.g. Write_EDI(...
SMP_fprintf(OutFile, " X86.Write_%s(", MDGetRegName(Opnd));
}
@@ -788,14 +802,14 @@ void SMPInstr::SPARKAdaOperandToString(const STARSOpndTypePtr &Opnd, std::string
} // end of SMPInstr::SPARKAdaOperandToString()
// Print just the addressing expression for a memory operand in SPARK-Ada form.
-void SMPInstr::PrintSPARKAdaAddressExpr(const STARSOpndTypePtr &Opnd, FILE *OutFile, bool UseFP) {
+void SMPInstr::PrintSPARKAdaAddressExpr(const STARSOpndTypePtr &Opnd, FILE *OutFile, bool UseFP, bool UseSavedStackPtr) {
bool MemOpnd = IsMemOperand(Opnd);
assert(MemOpnd);
if (Opnd->IsStaticMemOp()) {
if (Opnd->HasSIBByte()) {
- SPARKAnnotPrintSIB(Opnd, true, OutFile, Opnd->GetSegReg(), UseFP, this->MDHas64BitOperands());
+ SPARKAnnotPrintSIB(Opnd, true, OutFile, Opnd->GetSegReg(), UseFP, this->MDHas64BitOperands(), UseSavedStackPtr);
SMP_fprintf(OutFile, " + 16#%llx# )", (uint64_t) Opnd->GetAddr());
}
else {
@@ -804,7 +818,7 @@ void SMPInstr::PrintSPARKAdaAddressExpr(const STARSOpndTypePtr &Opnd, FILE *OutF
}
else if (Opnd->IsMemNoDisplacementOp()) {
if (Opnd->HasSIBByte()) { // has SIB info
- SPARKAnnotPrintSIB(Opnd, false, OutFile, Opnd->GetSegReg(), UseFP, this->MDHas64BitOperands());
+ SPARKAnnotPrintSIB(Opnd, false, OutFile, Opnd->GetSegReg(), UseFP, this->MDHas64BitOperands(), UseSavedStackPtr);
}
else { // no SIB info
STARS_regnum_t BaseReg = Opnd->GetReg();
@@ -820,7 +834,12 @@ void SMPInstr::PrintSPARKAdaAddressExpr(const STARSOpndTypePtr &Opnd, FILE *OutF
}
else {
#endif
- SMP_fprintf(OutFile, " X86.%s ", MDGetRegName(BaseOp));
+ if (!(UseSavedStackPtr && BaseOp->MatchesReg(MD_STACK_POINTER_REG))) {
+ SMP_fprintf(OutFile, " X86.%s ", MDGetRegName(BaseOp));
+ }
+ else {
+ SMP_fprintf(OutFile, " SaveStackPtr ");
+ }
#if STARS_SPARK_EMIT_SEGMENT_REGS
}
#endif
@@ -833,7 +852,7 @@ void SMPInstr::PrintSPARKAdaAddressExpr(const STARSOpndTypePtr &Opnd, FILE *OutF
STARS_ea_t offset = Opnd->GetAddr();
int SignedOffset = (int) offset;
if (Opnd->HasSIBByte()) {
- SPARKAnnotPrintSIB(Opnd, (SignedOffset != 0), OutFile, Opnd->GetSegReg(), UseFP, this->MDHas64BitOperands());
+ SPARKAnnotPrintSIB(Opnd, (SignedOffset != 0), OutFile, Opnd->GetSegReg(), UseFP, this->MDHas64BitOperands(), UseSavedStackPtr);
if (SignedOffset > 0) // print plus sign
SMP_fprintf(OutFile, "+ 16#%x# )", (unsigned int) SignedOffset);
else if (SignedOffset < 0) // minus sign will print automatically
@@ -853,7 +872,12 @@ void SMPInstr::PrintSPARKAdaAddressExpr(const STARSOpndTypePtr &Opnd, FILE *OutF
}
else {
#endif
- SMP_fprintf(OutFile, " X86.%s ", MDGetRegName(BaseOp));
+ if (!(UseSavedStackPtr && BaseOp->MatchesReg(MD_STACK_POINTER_REG))) {
+ SMP_fprintf(OutFile, " X86.%s ", MDGetRegName(BaseOp));
+ }
+ else {
+ SMP_fprintf(OutFile, " SaveStackPtr ");
+ }
#if STARS_SPARK_EMIT_SEGMENT_REGS
}
#endif
@@ -2229,7 +2253,7 @@ void STARSExpression::Dump(const std::size_t TabCount) const {
// Emit SPARK Ada translation of expression to OutputFile, perhaps with Reg'Old suffix.
// OffByOne should never be true for subtrees, only certain parent trees.
-void STARSExpression::EmitSPARKAda(FILE *OutputFile, bool ProcessingLoop, bool OldSuffix, bool OffByOne, bool HasLoopArgs) const {
+void STARSExpression::EmitSPARKAda(FILE *OutputFile, bool ProcessingLoop, bool OldSuffix, bool OffByOne, bool HasLoopArgs, bool UseSavedStackPtr) const {
bool UseFP = this->GetParentFunc()->UsesFramePointer();
bool PrefixProcCall = false;
@@ -2272,7 +2296,7 @@ void STARSExpression::EmitSPARKAda(FILE *OutputFile, bool ProcessingLoop, bool O
// Left operand or subtree
if (this->HasLeftSubTree()) {
SMP_fprintf(OutputFile, "(");
- this->GetLeftTree()->EmitSPARKAda(OutputFile, ProcessingLoop, OldSuffix, false, HasLoopArgs);
+ this->GetLeftTree()->EmitSPARKAda(OutputFile, ProcessingLoop, OldSuffix, false, HasLoopArgs, UseSavedStackPtr);
SMP_fprintf(OutputFile, ")");
}
else if ((nullptr != this->GetLeftOperand()) && (!this->GetLeftOperand()->IsVoidOp())) {
@@ -2282,7 +2306,7 @@ void STARSExpression::EmitSPARKAda(FILE *OutputFile, bool ProcessingLoop, bool O
if (MDIsDirectStackAccessOpnd(LeftOp, UseFP)) {
this->GetParentInst()->MDGetUnnormalizedOp(LeftOp);
}
- this->GetParentInst()->PrintSPARKAdaOperand(LeftOp, OutputFile, false, UseFP, !(ProcessingLoop && HasLoopArgs), OmitTrailingSpace);
+ this->GetParentInst()->PrintSPARKAdaOperand(LeftOp, OutputFile, false, UseFP, !(ProcessingLoop && HasLoopArgs), OmitTrailingSpace, UseSavedStackPtr);
if (ProcessingLoop && IsRegOp && HasLoopArgs && (STARS_BADADDR != this->GetLeftPreLoopDefAddr())) { // LiveIn to loop, traced back to InArg
std::ostringstream AddrString;
AddrString << std::hex << this->GetParentFunc()->GetFirstFuncAddr();
@@ -2310,7 +2334,7 @@ void STARSExpression::EmitSPARKAda(FILE *OutputFile, bool ProcessingLoop, bool O
// then the right operand or subtree
if (this->HasRightSubTree()) {
SMP_fprintf(OutputFile, "(");
- this->GetRightTree()->EmitSPARKAda(OutputFile, ProcessingLoop, OldSuffix, false, HasLoopArgs);
+ this->GetRightTree()->EmitSPARKAda(OutputFile, ProcessingLoop, OldSuffix, false, HasLoopArgs, UseSavedStackPtr);
SMP_fprintf(OutputFile, ")");
}
else if ((nullptr != this->GetRightOperand()) && (!this->GetRightOperand()->IsVoidOp())) {
@@ -2320,7 +2344,7 @@ void STARSExpression::EmitSPARKAda(FILE *OutputFile, bool ProcessingLoop, bool O
if (MDIsDirectStackAccessOpnd(RightOp, UseFP)) {
this->GetParentInst()->MDGetUnnormalizedOp(RightOp);
}
- this->GetParentInst()->PrintSPARKAdaOperand(RightOp, OutputFile, false, UseFP, !(ProcessingLoop && HasLoopArgs), OmitTrailingSpace);
+ this->GetParentInst()->PrintSPARKAdaOperand(RightOp, OutputFile, false, UseFP, !(ProcessingLoop && HasLoopArgs), OmitTrailingSpace, UseSavedStackPtr);
if (ProcessingLoop && IsRegOp && HasLoopArgs && (STARS_BADADDR != this->GetRightPreLoopDefAddr())) { // LiveIn to loop, traced back to InArg
std::ostringstream AddrString;
AddrString << std::hex << this->GetParentFunc()->GetFirstFuncAddr();
@@ -2494,8 +2518,7 @@ void STARSExpression::EmitSPARKInSafeRegion64(FILE *OutputFile, size_t MemWidth)
void STARSExpression::PrintSPARKArgLocationStrings(FILE *OutputFile, bool LoopInvariant) {
// Walk the expression tree and find non-constant leaves. These must be incoming arguments or basic induction variables (BIVs).
// This method should not be called on expressions that were expanded with the StopOnIV option flag, so we will assume that
- // any non-constant leaf operand is an incoming argument.
-
+ // any non-constant leaf operand is an incoming argument. EXCEPTION: The stack ptr reg is never made into an incoming arg.
if (this->HasLeftSubTree()) {
this->GetLeftTree()->PrintSPARKArgLocationStrings(OutputFile, LoopInvariant);
}
@@ -2524,49 +2547,51 @@ void STARSExpression::PrintSPARKArgLocationStrings(FILE *OutputFile, bool LoopIn
} // end of STARSExpression::CreateSPARKArgLocationStrings()
void STARSExpression::PrintSPARKArgLocationStringsHelper(FILE *OutputFile, bool LoopInvariant, const STARSOpndTypePtr &LeafOp, STARS_ea_t PreLoopDefAddr) {
- bool UseFP = this->GetParentFunc()->UsesFramePointer();
- std::ostringstream AddrString;
- AddrString << std::hex << this->GetParentFunc()->GetFirstFuncAddr();
- if ((STARS_BADADDR != PreLoopDefAddr) && (!STARS_IsBlockNumPseudoID(PreLoopDefAddr)) && (!STARS_IsBlockNumPseudoID(PreLoopDefAddr))) {
- if (STARS_IsSSAMarkerPseudoID(PreLoopDefAddr)) {
- // InArg from calling function was unchanged and LiveIn to loop.
- // We want a string like: "RDI_400586 = RDI"
- if (LoopInvariant) {
- PrintSPARKIndentTabs(OutputFile);
- SMP_fprintf(OutputFile, "pragma Loop_Invariant(");
- this->GetParentInst()->PrintSPARKAdaOperand(LeafOp, OutputFile, false, UseFP, false, true);
- SMP_fprintf(OutputFile, "_%s = ", AddrString.str().c_str());
- this->GetParentInst()->PrintSPARKAdaOperand(LeafOp, OutputFile, false, UseFP, true, false);
- SMP_fprintf(OutputFile, ");\n");
- }
- else {
- SMP_fprintf(OutputFile, " and\n\t(");
- this->GetParentInst()->PrintSPARKAdaOperand(LeafOp, OutputFile, false, UseFP, false, true);
- SMP_fprintf(OutputFile, "_%s = ", AddrString.str().c_str());
- this->GetParentInst()->PrintSPARKAdaOperand(LeafOp, OutputFile, false, UseFP, true, false);
- SMP_fprintf(OutputFile, ")");
- }
- }
- else { // A regular instruction is at PreLoopDefAddr
- // We want a string like: "RDI_400586 = X86.ReadMem64(X86.RBP-8)"
- SMPInstr *PreLoopInst = this->GetParentFunc()->GetInstFromAddr(PreLoopDefAddr);
- assert(nullptr != PreLoopInst);
- STARSOpndTypePtr PreLoopDefOp = PreLoopInst->GetFirstLeftOperandNoNorm();
- assert((nullptr != PreLoopDefOp) && (!PreLoopDefOp->IsVoidOp()));
- if (LoopInvariant) {
- PrintSPARKIndentTabs(OutputFile);
- SMP_fprintf(OutputFile, "pragma Loop_Invariant(");
- this->GetParentInst()->PrintSPARKAdaOperand(LeafOp, OutputFile, false, UseFP, false, true);
- SMP_fprintf(OutputFile, "_%s = ", AddrString.str().c_str());
- this->GetParentInst()->PrintSPARKAdaOperand(PreLoopDefOp, OutputFile, false, UseFP, true, false);
- SMP_fprintf(OutputFile, ");\n");
- }
- else {
- SMP_fprintf(OutputFile, " and\n\t(");
- this->GetParentInst()->PrintSPARKAdaOperand(LeafOp, OutputFile, false, UseFP, false, true);
- SMP_fprintf(OutputFile, "_%s = ", AddrString.str().c_str());
- this->GetParentInst()->PrintSPARKAdaOperand(PreLoopDefOp, OutputFile, false, UseFP, true, false);
- SMP_fprintf(OutputFile, ")");
+ if (!(LeafOp->IsRegOp() && LeafOp->MatchesReg(MD_STACK_POINTER_REG))) {
+ bool UseFP = this->GetParentFunc()->UsesFramePointer();
+ std::ostringstream AddrString;
+ AddrString << std::hex << this->GetParentFunc()->GetFirstFuncAddr();
+ if ((STARS_BADADDR != PreLoopDefAddr) && (!STARS_IsBlockNumPseudoID(PreLoopDefAddr)) && (!STARS_IsBlockNumPseudoID(PreLoopDefAddr))) {
+ if (STARS_IsSSAMarkerPseudoID(PreLoopDefAddr)) {
+ // InArg from calling function was unchanged and LiveIn to loop.
+ // We want a string like: "RDI_400586 = RDI"
+ if (LoopInvariant) {
+ PrintSPARKIndentTabs(OutputFile);
+ SMP_fprintf(OutputFile, "pragma Loop_Invariant(");
+ this->GetParentInst()->PrintSPARKAdaOperand(LeafOp, OutputFile, false, UseFP, false, true);
+ SMP_fprintf(OutputFile, "_%s = ", AddrString.str().c_str());
+ this->GetParentInst()->PrintSPARKAdaOperand(LeafOp, OutputFile, false, UseFP, true, false);
+ SMP_fprintf(OutputFile, ");\n");
+ }
+ else {
+ SMP_fprintf(OutputFile, " and\n\t(");
+ this->GetParentInst()->PrintSPARKAdaOperand(LeafOp, OutputFile, false, UseFP, false, true);
+ SMP_fprintf(OutputFile, "_%s = ", AddrString.str().c_str());
+ this->GetParentInst()->PrintSPARKAdaOperand(LeafOp, OutputFile, false, UseFP, true, false);
+ SMP_fprintf(OutputFile, ")");
+ }
+ }
+ else { // A regular instruction is at PreLoopDefAddr
+ // We want a string like: "RDI_400586 = X86.ReadMem64(X86.RBP-8)"
+ SMPInstr *PreLoopInst = this->GetParentFunc()->GetInstFromAddr(PreLoopDefAddr);
+ assert(nullptr != PreLoopInst);
+ STARSOpndTypePtr PreLoopDefOp = PreLoopInst->GetFirstLeftOperandNoNorm();
+ assert((nullptr != PreLoopDefOp) && (!PreLoopDefOp->IsVoidOp()));
+ if (LoopInvariant) {
+ PrintSPARKIndentTabs(OutputFile);
+ SMP_fprintf(OutputFile, "pragma Loop_Invariant(");
+ this->GetParentInst()->PrintSPARKAdaOperand(LeafOp, OutputFile, false, UseFP, false, true);
+ SMP_fprintf(OutputFile, "_%s = ", AddrString.str().c_str());
+ this->GetParentInst()->PrintSPARKAdaOperand(PreLoopDefOp, OutputFile, false, UseFP, true, false);
+ SMP_fprintf(OutputFile, ");\n");
+ }
+ else {
+ SMP_fprintf(OutputFile, " and\n\t(");
+ this->GetParentInst()->PrintSPARKAdaOperand(LeafOp, OutputFile, false, UseFP, false, true);
+ SMP_fprintf(OutputFile, "_%s = ", AddrString.str().c_str());
+ this->GetParentInst()->PrintSPARKAdaOperand(PreLoopDefOp, OutputFile, false, UseFP, true, false);
+ SMP_fprintf(OutputFile, ")");
+ }
}
}
}
@@ -2920,6 +2945,79 @@ bool STARSExpression::SimplifyExpr(STARSExpression *ParentExpr) {
} // end of cascading additions and subtractions
}
}
+ } // end if (LeftNullTree || RightNullTree)
+ else {
+ // Look for the special case of simplifying address ranges, e.g. if we loop from
+ // RDI + 4 up to RDI + 128, then the iteration count expr will be ((RDI + 128) - (RDI + 4)).
+ // The address register drops out of the expr and the final answer is 124.
+ if (SMP_SUBTRACT == this->GetOperator() && (!this->GetLeftTree()->HasRightSubTree()) && (!this->GetRightTree()->HasRightSubTree())) {
+ // Check for the LeftTree and RightTree having the same LeftOperand register.
+ if (this->GetLeftTree()->GetLeftOperand()->IsRegOp() && this->GetRightTree()->GetLeftOperand()->IsRegOp()) {
+ STARS_regnum_t LeftReg = this->GetLeftTree()->GetLeftOperand()->GetReg();
+ STARS_regnum_t RightReg = this->GetRightTree()->GetLeftOperand()->GetReg();
+ if (LeftReg == RightReg) {
+ // The registers will drop out of the expression.
+ // We have ((Reg op RightOp1) - (Reg op RightOp2))
+ // What to do next depends on the operators and whether we have immediate RightOps
+ SMPoperator LeftOperator = this->GetLeftTree()->GetOperator();
+ SMPoperator RightOperator = this->GetRightTree()->GetOperator();
+ if (SMP_ADD == LeftOperator) {
+ // We need RightOp1 - RightOp2 if RightOperator is addition,
+ // and RightOp1 + RightOp2 if RightOperator is subtraction.
+ if ((SMP_ADD == RightOperator) || (SMP_SUBTRACT == RightOperator)) {
+ // Make the LeftTree->RightOperand into the new left tree,
+ // and the RightTree->RightOperand into the new right tree,
+ // leaving SMP_SUBTRACT as the parent operator.
+ LeftOperandLifted = this->GetLeftTree()->ElevateRightSide(this);
+ RightOperandLifted = this->GetRightTree()->ElevateRightSide(this);
+ assert(LeftOperandLifted && RightOperandLifted);
+ if (SMP_SUBTRACT == RightOperator) {
+ // We simplified ((Reg + RightOp1) - (Reg - RightOp2))
+ // so the answer is (RightOp1 + RightOp2). Change parent operator
+ // to SMP_ADD.
+ this->SetOperator(SMP_ADD);
+ }
+ }
+ }
+ else if (SMP_SUBTRACT == LeftOperator) {
+ // We need (-RightOp1) - RightOp2 if RightOperator is addition,
+ // and RightOp2 - RightOp1 if RightOperator is subtraction.
+ // We will only deal with the negation case if we have a constant RightOp1.
+ if (SMP_SUBTRACT == RightOperator) {
+ // Make the LeftTree->RightOperand into the new right operand,
+ // and the RightTree->RightOperand into the new left operand,
+ // leaving SMP_SUBTRACT as the parent operator.
+ STARSOpndTypePtr LeftRightOp = this->GetLeftTree()->GetRightOperand()->clone();
+ STARSOpndTypePtr RightRightOp = this->GetRightTree()->GetRightOperand()->clone();
+ this->SetLeftOperand(RightRightOp);
+ this->SetRightOperand(LeftRightOp);
+ LeftOperandLifted = RightOperandLifted = true;
+ }
+ else if ((SMP_ADD == RightOperator) && this->GetLeftTree()->GetRightOperand()->IsImmedOp()) {
+ // Take ((Reg - immed) - (Reg + operand)) and produce (-immed - operand) by negating the
+ // left immediate value, substituting it for the left tree, and raising the right tree's
+ // right operand and leaving the parent operator as SMP_SUBTRACT.
+ STARS_uval_t LeftRightValue = this->GetLeftTree()->GetRightOperand()->GetImmedValue();
+ LeftRightValue = (0 - LeftRightValue); // negate RightOp1
+ STARSOpndTypePtr NewLeftOp = this->GetLeftTree()->GetParentInst()->MakeImmediateOpnd(LeftRightValue);
+ RightOperandLifted = this->GetRightTree()->ElevateRightSide(this);
+ assert(RightOperandLifted);
+ this->SetLeftOperand(NewLeftOp);
+ LeftOperandLifted = true;
+ }
+ }
+ }
+ }
+ if (LeftOperandLifted || RightOperandLifted) {
+ // See if our simplifications left us with constants.
+ if (!this->HasLeftSubTree() && (!this->HasRightSubTree())) {
+ if (this->GetLeftOperand()->IsImmedOp() && this->GetLeftOperand()->IsImmedOp()) {
+ bool success = this->SimplifyExpr(ParentExpr);
+ assert(success);
+ }
+ }
+ }
+ }
}
return (LeftOperandLifted || RightOperandLifted || RootLeftExprLifted);
@@ -3292,6 +3390,21 @@ bool STARSExpression::UsesInArgReg(void) const {
return false;
} // end of STARSExpression::UsesInArgReg()
+// Is Expr just the stack pointer plus optional offset constant?
+bool STARSExpression::IsStackPtrPlusOffset(void) const {
+ SMPoperator CurrOper = this->GetOperator();
+ bool LeftSPOpnd = (!this->HasLeftSubTree()) && this->GetLeftOperand()->IsRegOp() && this->GetLeftOperand()->MatchesReg(MD_STACK_POINTER_REG);
+ bool SPPlusOffset = false;
+ bool JustStackPtr = (CurrOper == SMP_ASSIGN) && LeftSPOpnd;
+ if (!JustStackPtr && LeftSPOpnd && IsIntegerAddOrSubOperator(CurrOper)) {
+ const STARSOpndTypePtr RightOp = this->GetRightOperand();
+ bool HasRightTree = this->HasRightSubTree();
+ bool ImmedRightOp = (nullptr != RightOp) && RightOp->IsImmedOp() && (!HasRightTree);
+ SPPlusOffset = ImmedRightOp;
+ }
+ return (JustStackPtr || SPPlusOffset);
+} // end of STARSExpression::IsStackPtrPlusOffset()
+
// If expr is SP+offset, add offset to CurrentStackPtrOffset to get FinalStackPtrOffset and return true.
// CurrentStackPtrOffset should be relative to function entry and will generally be negative.
bool STARSExpression::IsStackPtrOffset(const STARS_sval_t CurrentStackPtrOffset, STARS_sval_t &FinalStackPtrOffset) const {
@@ -5332,7 +5445,7 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
if ((!TargetFunc->FuncReturnsToCaller()) || TargetFunc->HasCallToNonReturningFunc() || TargetFunc->HasCalleeChainWithNonReturningFunc()) {
// Call chain could have set X86.Exit_Called, signalling that exit() or something similar was called.
PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, " if X86.Exit_Called then ;\n");
+ SMP_fprintf(OutFile, " if X86.Exit_Called then \n");
PrintSPARKIndentTabs(OutFile);
SMP_fprintf(OutFile, "\t return;\n");
PrintSPARKIndentTabs(OutFile);
@@ -5360,6 +5473,77 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
}
if (PrintOperands) {
+ if (this->HasIndirectMemoryWrite()) {
+ // If we are in a loop, we need to emit an assertion that the memory address expression is in bounds.
+ int BlockNum = this->GetBlock()->GetNumber();
+ int InnerLoopNum = this->GetBlock()->GetFunc()->GetInnermostLoopNum(BlockNum);
+ STARSOpndTypePtr MemDefOp = this->GetMemDef();
+ bool UseFP = this->GetBlock()->GetFunc()->UsesFramePointer();
+ size_t ByteWidth = MemDefOp->GetByteWidth();
+ if (0 <= InnerLoopNum) {
+ // Inst is in a loop. Did we analyze memory bounds for the loop?
+ size_t LoopIndex = (size_t)InnerLoopNum;
+ STARSExpression *LowerExpr = this->GetBlock()->GetFunc()->GetLoopMemWriteLowerBoundExpr(LoopIndex);
+ STARSExpression *UpperExpr = this->GetBlock()->GetFunc()->GetLoopMemWriteUpperBoundExpr(LoopIndex);
+ if ((nullptr != LowerExpr) && (nullptr != UpperExpr)) {
+ bool HasArgs = this->GetBlock()->GetFunc()->DoesLoopHaveArgs(InnerLoopNum);
+ for (size_t ByteIndex = 0; ByteIndex < ByteWidth; ++ByteIndex) {
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "pragma Assert(X86.InMemoryRange(");
+ this->PrintSPARKAdaAddressExpr(MemDefOp, OutFile, UseFP, true);
+ if (0 < ByteIndex)
+ SMP_fprintf(OutFile, "+%u", ByteIndex);
+ SMP_fprintf(OutFile, ", ");
+ LowerExpr->EmitSPARKAda(OutFile, true, false, false, HasArgs, true);
+ SMP_fprintf(OutFile, ", ");
+ UpperExpr->EmitSPARKAda(OutFile, true, false, false, HasArgs, true);
+ SMP_fprintf(OutFile, "));\n");
+ }
+ }
+ // Regardless of whether we analyzed the loop, we want to assert that
+ // the memory write is in the safe stack region, unless it is a stack frame write.
+ if (!MDIsStackAccessOpnd(MemDefOp, UseFP)) {
+ for (size_t ByteIndex = 0; ByteIndex < ByteWidth; ++ByteIndex) {
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "pragma Assert(X86.InSafeRegion64(");
+ this->PrintSPARKAdaAddressExpr(MemDefOp, OutFile, UseFP, true);
+ if (0 < ByteIndex)
+ SMP_fprintf(OutFile, "+%u", ByteIndex);
+ SMP_fprintf(OutFile, ", SaveStackPtr));\n");
+ }
+ }
+ }
+ else {
+ // For indirect writes outside of loops, see if we mapped the address reg operand back to an incoming arg.
+ // If so, emit an assert that the address reg is just a copy of the InArg.
+ STARSInArgMap::const_iterator AddrRegInArgMapIter = this->GetBlock()->GetFunc()->GetAddressRegToInArgMapping(InstAddr);
+ if (AddrRegInArgMapIter != this->GetBlock()->GetFunc()->GetLastAddressRegToInArgMapping()) {
+ // If RBX maps to saved InArg RDI in a func that starts at 0x400788, we want to emit:
+ // pragma Assert(X86.RBX = RDI_400788);
+ // The InArg RDI will have been saved in a Ghost variable called RDI_400788 at function entry.
+ STARSOpndTypePtr AddrRegOp = (*AddrRegInArgMapIter).second.first;
+ STARSOpndTypePtr InArgOp = (*AddrRegInArgMapIter).second.second;
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "pragma Assert(");
+ this->PrintSPARKAdaOperand(AddrRegOp, OutFile, false, UseFP, true, false);
+ SMP_fprintf(OutFile, "=");
+ this->PrintSPARKAdaOperand(InArgOp, OutFile, false, UseFP, false, true);
+ // At this point, we have "pragma Assert(RBX = RDI" and we need the "_400788" suffix
+ SMP_fprintf(OutFile, "%s );\n", this->GetBlock()->GetFunc()->GetFuncSPARKSuffixString().c_str());
+ // In addition to being a copy of the InArg, we want to assert that
+ // the memory write is in the safe stack region.
+ for (size_t ByteIndex = 0; ByteIndex < ByteWidth; ++ByteIndex) {
+ PrintSPARKIndentTabs(OutFile);
+ SMP_fprintf(OutFile, "pragma Assert(X86.InSafeRegion64(");
+ this->PrintSPARKAdaAddressExpr(MemDefOp, OutFile, UseFP, true);
+ if (0 < ByteIndex)
+ SMP_fprintf(OutFile, "+%u", ByteIndex);
+ SMP_fprintf(OutFile, ", SaveStackPtr));\n");
+ }
+ }
+ }
+ } // end if indirect memory write
+
if (this->MDIsCompareOrTest()) {
this->MDEmitSPARKAdaCompareOrTest(OutFile);
}
@@ -5382,54 +5566,6 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile) {
SMP_fprintf(OutFile, " then \n");
++STARS_SPARK_IndentCount;
}
- if (this->HasIndirectMemoryWrite()) {
- // If we are in a loop, we need to emit an assertion that the memory address expression is in bounds.
- int BlockNum = this->GetBlock()->GetNumber();
- int InnerLoopNum = this->GetBlock()->GetFunc()->GetInnermostLoopNum(BlockNum);
- if (0 <= InnerLoopNum) {
- // Inst is in a loop. Did we analyze memory bounds for the loop?
- size_t LoopIndex = (size_t) InnerLoopNum;
- STARSExpression *LowerExpr = this->GetBlock()->GetFunc()->GetLoopMemWriteLowerBoundExpr(LoopIndex);
- STARSExpression *UpperExpr = this->GetBlock()->GetFunc()->GetLoopMemWriteUpperBoundExpr(LoopIndex);
- if ((nullptr != LowerExpr) && (nullptr != UpperExpr)) {
- STARSOpndTypePtr MemDefOp = this->GetMemDef();
- bool UseFP = this->GetBlock()->GetFunc()->UsesFramePointer();
- size_t ByteWidth = MemDefOp->GetByteWidth();
- bool HasArgs = this->GetBlock()->GetFunc()->DoesLoopHaveArgs(InnerLoopNum);
- for (size_t ByteIndex = 0; ByteIndex < ByteWidth; ++ByteIndex) {
- PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, "pragma Assert(X86.InMemoryRange(");
- this->PrintSPARKAdaAddressExpr(MemDefOp, OutFile, UseFP);
- if (0 < ByteIndex)
- SMP_fprintf(OutFile, "+%u", ByteIndex);
- SMP_fprintf(OutFile, ", ");
- LowerExpr->EmitSPARKAda(OutFile, true, false, false, HasArgs);
- SMP_fprintf(OutFile, ", ");
- UpperExpr->EmitSPARKAda(OutFile, true, false, false, HasArgs);
- SMP_fprintf(OutFile, "));\n");
- }
- }
- }
- else {
- // For indirect writes outside of loops, see if we mapped the address reg operand back to an incoming arg.
- // If so, emit an assert that the address reg is just a copy of the InArg.
- STARSInArgMap::const_iterator AddrRegInArgMapIter = this->GetBlock()->GetFunc()->GetAddressRegToInArgMapping(InstAddr);
- if (AddrRegInArgMapIter != this->GetBlock()->GetFunc()->GetLastAddressRegToInArgMapping()) {
- // If RBX maps to saved InArg RDI in a func that starts at 0x400788, we want to emit:
- // pragma Assert(X86.RBX = RDI_400788);
- // The InArg RDI will have been saved in a Ghost variable called RDI_400788 at function entry.
- STARSOpndTypePtr AddrRegOp = (*AddrRegInArgMapIter).second.first;
- STARSOpndTypePtr InArgOp = (*AddrRegInArgMapIter).second.second;
- PrintSPARKIndentTabs(OutFile);
- SMP_fprintf(OutFile, "pragma Assert(");
- this->PrintSPARKAdaOperand(AddrRegOp, OutFile, false, UseFP, true, false);
- SMP_fprintf(OutFile, "=");
- this->PrintSPARKAdaOperand(InArgOp, OutFile, false, UseFP, true, true);
- // At this point, we have "pragma Assert(RBX = RDI" and we need the "_400788" suffix
- SMP_fprintf(OutFile, "%s );\n", this->GetBlock()->GetFunc()->GetFuncSPARKSuffixString().c_str());
- }
- }
- } // end if indirect memory write
SMPRegTransfer *CurrRT;
for (std::size_t RTLindex = 0; RTLindex < this->RTL.GetCount(); ++RTLindex) {