From 65c92a0bbd7c90c1a245c1eca72b16db7f1ecd6d Mon Sep 17 00:00:00 2001
From: Clark Coleman <clc@zephyr-software.com>
Date: Wed, 3 Mar 2021 10:23:03 -0500
Subject: [PATCH] SPARK: Use flags reg at top of short circuit expr;
parenthesize subexprs.
---
src/base/SMPBasicBlock.cpp | 58 +++++++++++++++++++++++++++++++-------
1 file changed, 48 insertions(+), 10 deletions(-)
diff --git a/src/base/SMPBasicBlock.cpp b/src/base/SMPBasicBlock.cpp
index 225b8c5c..60930dd7 100644
--- a/src/base/SMPBasicBlock.cpp
+++ b/src/base/SMPBasicBlock.cpp
@@ -719,6 +719,46 @@ void SMPBasicBlock::EmitSPARKAdaForExpression(FILE *BodyFile) {
STARSCFGBlock *CurrCFGBlock = this->GetFunc()->GetClonedCFGBlockByNum((size_t)TCFGBlockNum);
bool HeaderBlock = (!CurrCFGBlock->IsCoalesced());
+ // Emit the SPARK Ada for the left operand of the comparison.
+ // First, set up iterators and pointers.
+ std::vector<SMPInstr *>::const_reverse_iterator RevInstIter = this->GetRevInstCBegin();
+ SMPInstr *LastInst = (*RevInstIter);
+ bool UnsignedBranchOpcode = LastInst->MDIsUnsignedBranch();
+ bool SignBitSetBranch = LastInst->MDIsBranchOnSignBit();
+ bool SignBitNotSetBranch = LastInst->MDIsBranchOnNotSignBit();
+
+ // If this is the HeaderBlock, then we start with a simple reference to the flag
+ // register, which has been set based on operations in the HeaderBlock before the
+ // last inst. This approach is simple, avoids problems with cases that don't have
+ // a compare or test instruction but set the flag in another operation, and avoids
+ // erroneous code when instruction scheduling does something like:
+ //
+ // test rax,rax
+ // mov rax,rbx ; does not affect flags set by previous inst, overwrites rax
+ // jz label
+ //
+ // If generate "if (X86.RAX \= 0)" then the SPARK Ada code will be using the copy
+ // of RBX that was put into RAX by the instruction-scheduled move opcode. Incorrect.
+ if (HeaderBlock) {
+ assert(this->HasConditionalBranch());
+ bool NegateLeft = CurrCFGBlock->GetExpr()->IsLeftExprNegated();
+ if (NegateLeft) {
+ SMP_fprintf(BodyFile, "(not ");
+ }
+ LastInst->MDEmitSPARKAdaCondition(BodyFile);
+ if (NegateLeft) {
+ SMP_fprintf(BodyFile, ") ");
+ }
+
+ // Mark all instructions in the single-expr block as translated.
+ for (SMPInstr *CurrInst : this->InstVec) {
+ CurrInst->SetSPARKTranslated(true);
+ }
+ this->IncrementSPARKTranslationCount();
+ return;
+ }
+
+
// We will divide into cases: Expression block can end in signed compare instruction or
// unsigned compare (bitwise AND) instruction, and unsigned compare is often to itself
// to test for zero or non-zero value.
@@ -736,14 +776,6 @@ void SMPBasicBlock::EmitSPARKAdaForExpression(FILE *BodyFile) {
bool SignedCompareCase = (SMP_S_COMPARE == CompareOperator);
bool UnsignedSelfCompareCase = ((SMP_U_COMPARE == CompareOperator) && IsEqOp(CompareRT->GetConstRightOperandNoNorm(), CompareRT->GetConstLeftOperandNoNorm()));
- // Emit the SPARK Ada for the left operand of the comparison.
- // First, set up iterators and pointers.
- std::vector<SMPInstr *>::const_reverse_iterator RevInstIter = GetRevInstCBegin();
- SMPInstr *LastInst = (*RevInstIter);
- bool UnsignedBranchOpcode = LastInst->MDIsUnsignedBranch();
- bool SignBitSetBranch = LastInst->MDIsBranchOnSignBit();
- bool SignBitNotSetBranch = LastInst->MDIsBranchOnNotSignBit();
-
// CompareInst might be in this block or in a previous block.
STARS_ea_t CompareAddr = CompareInst->GetAddr();
SMPBasicBlock *CompareBlock;
@@ -881,8 +913,8 @@ void SMPBasicBlock::EmitSPARKAdaForExpression(FILE *BodyFile) {
}
// Mark all instructions in the single-expr block as translated.
- for (vector<SMPInstr *>::iterator InstIter = this->GetFirstInst(); InstIter != this->GetLastInst(); ++InstIter) {
- (*InstIter)->SetSPARKTranslated(true);
+ for (SMPInstr *CurrInst : this->InstVec) {
+ CurrInst->SetSPARKTranslated(true);
}
this->IncrementSPARKTranslationCount();
return;
@@ -8127,7 +8159,11 @@ void STARSCondExpr::EmitSPARKAdaShortCircuitExpr(FILE *BodyFile, const bool Inve
}
else {
// Recurse into LeftExpr
+ // Ada puts "or else" and "and then" at same precedence level; they cannot be
+ // mixed without parentheses, so we parenthesize when recursing into subexprs.
+ SMP_fprintf(BodyFile, "(");
this->GetLeftExpr()->EmitSPARKAdaShortCircuitExpr(BodyFile, false);
+ SMP_fprintf(BodyFile, ")");
}
if (this->NegateLeftExpr) { // close "not" parenthesis
SMP_fprintf(BodyFile, ") ");
@@ -8157,7 +8193,9 @@ void STARSCondExpr::EmitSPARKAdaShortCircuitExpr(FILE *BodyFile, const bool Inve
}
else {
// Recurse into RightExpr
+ SMP_fprintf(BodyFile, "(");
this->GetRightExpr()->EmitSPARKAdaShortCircuitExpr(BodyFile, false);
+ SMP_fprintf(BodyFile, ")");
}
return;
--
GitLab