SMPInstr.cpp

/* SMPInstr.cpp - <see below>.
 *
 * Copyright (c) 2000, 2001, 2010 - University of Virginia 
 *
 * This file is part of the Memory Error Detection System (MEDS) infrastructure.
 * This file may be used and modified for non-commercial purposes as long as 
 * all copyright, permission, and nonwarranty notices are preserved.  
 * Redistribution is prohibited without prior written consent from the University 
 * of Virginia.
 *
 * Please contact the authors for restrictions applying to commercial use.
 *
 * THIS SOURCE IS PROVIDED "AS IS" AND WITHOUT ANY EXPRESS OR IMPLIED
 * WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED WARRANTIES OF
 * MERCHANTIBILITY AND FITNESS FOR A PARTICULAR PURPOSE.
 *
 * Author: University of Virginia
 * e-mail: jwd@virginia.com
 * URL   : http://www.cs.virginia.edu/
 *
 * Additional copyrights 2010, 2011, 2012, 2013, 2014, 2015 by Zephyr Software LLC
 * e-mail: {clc,jwd}@zephyr-software.com
 * URL   : http://www.zephyr-software.com/
 *
 */

//
// SMPInstr.cpp
//
// This module performs the instruction level analyses needed for the
//   SMP project (Software Memory Protection).
//

using namespace std;

#include <memory>
#include <string>
#include <iostream>
#include <sstream>
#include <iomanip>

#include <cstring>
#include <cstddef>
#include <cassert>

#include "interfaces/STARSTypes.h"
#include "interfaces/SMPDBInterface.h"
#include "base/SMPDataFlowAnalysis.h"
#include "base/SMPInstr.h"
#include "base/SMPProgram.h"
#include "base/ProfilerInformation.h"

#include "interfaces/abstract/STARSInstruction.h"
#include "interfaces/abstract/STARSOp.h"

// Set to 1 for debugging output
#define SMP_DEBUG 1
#define SMP_DEBUG2 0   // verbose
#define SMP_DEBUG_XOR 0
#define SMP_DEBUG_BUILD_RTL  1   // should be left on, serious errors!
#define SMP_VERBOSE_DEBUG_BUILD_RTL  0
#define SMP_VERBOSE_DEBUG_BUILD_RTL_DEF_USE 0
#define SMP_VERBOSE_DEBUG_INFER_TYPES 0
#define SMP_VERBOSE_DUMP 0
#define SMP_VERBOSE_FIND_POINTERS 0
#define STARS_DUMP_FG_INFO 1  // show signedness of DEFs and USEs in dump
#define STARS_DEBUG_STATIC_MEM_OPS 0

#define SMP_BASEREG_POINTER_TYPE 1  // Initialize Base Register USEs to type POINTER?
#define SMP_OPTIMIZE_ADD_TO_NUMERIC 0 // optimizing annotation type -5
#define SMP_IDENTIFY_POINTER_ADDRESS_REG 0 // optimizing annotation POINTER
#define SMP_CHILDACCESS_ALL_CODE 0 // CHILDACCESS annotations for all funcs, or just analyzed funcs?
#define SPECIAL_CASE_CARRY_BORROW 0 // Treat sbb/adc different from sub/add annotations?
#define SMP_BUILD_SPECIAL_ADC_SBB_RTL 0 // Explicit RTL subtree for carry flag?
#define SMP_AGGRESSIVE_TYPE_INFERENCE 1  // Shorten iterations by quick propagation in InferOperatorType()
#define SMP_ANNOTATE_ALL_MEMORY_OPERANDS 0 // Info annotation for all memory read and write operands?
#define SMP_AGGRESSIVE_SIGN_TRANSFER 1  // More transfer of signedness across instructions
#define STARS_NO_SHIFT_SIGNEDNESS_IN_SCALEFACTOR 1  // unsigned left shift for scale factors is really unknownsign multiply
#define STARS_USE_NUMERIC_ERROR_BLACKLISTING 1  // Only instrument for numeric errors if DEF leads to a blacklisted (important) sink
#define STARS_CONSERVATIVE_DEADREGS 1  // debug DEADREGS annotations by being ultra-conservative at call sites

#define STARS_EXPR_CALL_DEPTH_LIMIT 50 // Limit on number of invocations of ExpandExpr(), ExpandOperand(), and ExpandOperandHelper()

// Text to be printed in each optimizing annotation explaining why
//  the annotation was emitted.
#define LAST_TYPE_CATEGORY 15
static const char *OptExplanation[LAST_TYPE_CATEGORY + 1] =
	{ "NoOpt", "NoMetaUpdate", "AlwaysNUM", "NUMVia2ndSrcIMMEDNUM",
	  "Always1stSrc", "1stSrcVia2ndSrcIMMEDNUM", "AlwaysPtr",
	  "AlwaysNUM", "AlwaysNUM", "NUMViaFPRegDest", "NumericSources",
	  "StackMemoryTracking", "NumericSources", "NumericMemDest",
	  "NeverMemDest", "SafeIfNoIndexing"
	};

const char *OperatorText[LAST_SMP_OPERATOR + 1] = 
{ 	"SMP_NULL_OPERATOR", "SMP_CALL", "SMP_INPUT", "SMP_OUTPUT", "SMP_ADDRESS_OF",
	"SMP_U_LEFT_SHIFT", "SMP_S_LEFT_SHIFT", "SMP_U_RIGHT_SHIFT", "SMP_S_RIGHT_SHIFT",
	"SMP_ROTATE_LEFT", "SMP_ROTATE_LEFT_CARRY", "SMP_ROTATE_RIGHT", "SMP_ROTATE_RIGHT_CARRY",
	"SMP_DECREMENT", "SMP_INCREMENT",
	"SMP_ADD", "SMP_ADD_CARRY", "SMP_SUBTRACT", "SMP_SUBTRACT_BORROW", "SMP_U_MULTIPLY",
	"SMP_S_MULTIPLY", "SMP_U_DIVIDE", "SMP_S_DIVIDE", "SMP_U_REMAINDER",
	"SMP_SIGN_EXTEND", "SMP_ZERO_EXTEND", "SMP_ASSIGN", "SMP_BITWISE_AND",
	"SMP_BITWISE_OR", "SMP_BITWISE_NOT", "SMP_BITWISE_XOR", "SMP_BITWISE_AND_NOT", "SMP_NEGATE", 
	"SMP_S_COMPARE", "SMP_U_COMPARE", "SMP_GENERAL_COMPARE", "SMP_LESS_THAN", "SMP_GREATER_THAN",
	"SMP_LESS_EQUAL", "SMP_GREATER_EQUAL", "SMP_EQUAL", "SMP_NOT_EQUAL",
	"SMP_BELOW", "SMP_BELOW_EQUAL", "SMP_ABOVE", "SMP_ABOVE_EQUAL",
	"SMP_CARRY", "SMP_NOT_CARRY", "SMP_PARITY", "SMP_NOT_PARITY",
	"SMP_OVERFLOW", "SMP_NOT_OVERFLOW", "SMP_SIGN_BIT_SET", "SMP_NOT_SIGN_BIT_SET",
	"SMP_LOGICAL_AND", "SMP_LOGICAL_OR", "SMP_UNARY_NUMERIC_OPERATION",
	"SMP_BINARY_NUMERIC_OPERATION", "SMP_SYSTEM_OPERATION",
	"SMP_UNARY_FLOATING_ARITHMETIC", "SMP_BINARY_FLOATING_ARITHMETIC",
	"SMP_FLOATING_ADD", "SMP_FLOATING_SUBTRACT",
	"SMP_FLOATING_MULTIPLY", "SMP_FLOATING_DIVIDE", "SMP_FLOATING_NEGATE_AND_ADD",
	"SMP_REVERSE_SHIFT_U", "SMP_SHUFFLE", "SMP_COMPARE_EQ_AND_SET",
	"SMP_COMPARE_NE_AND_SET", "SMP_COMPARE_GT_AND_SET", 
	"SMP_COMPARE_GE_AND_SET", "SMP_COMPARE_LT_AND_SET", "SMP_COMPARE_LE_AND_SET",
	"SMP_PACK_SIGNED", "SMP_PACK_UNSIGNED",
	"SMP_AVERAGE_UNSIGNED", "SMP_MULTIPLY_AND_ADD", "SMP_SUM_OF_DIFFS",
	"SMP_MAX_S", "SMP_MAX_U", "SMP_MIN_S", "SMP_MIN_U", "SMP_ABS_VALUE",
	"SMP_CONVERT_INT_TO_FP", "SMP_CONVERT_FP_TO_INT", "SMP_CREATE_MASK",
	"SMP_INTERLEAVE", "SMP_CONCATENATE", "SMP_EXTRACT_ZERO_EXTEND", 
	"SMP_ENCRYPTION_OPERATION", "SMP_UNARY_POINTER_OPERATION", "X86.ReadMem64", "SMP_SIGNAL"
};

// 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.
//  If we did cmp rbx,rax then the operator would logically be SMP_LESS_THAN.
//  Used in STARSExpression tree flips.
SMPoperator InvertRelationalOperator(SMPoperator RelationalOperator) {
	switch (RelationalOperator) {
	case SMP_LESS_THAN:
		RelationalOperator = SMP_GREATER_THAN;
		break;

	case SMP_GREATER_THAN:
		RelationalOperator = SMP_LESS_THAN;
		break;

	case SMP_LESS_EQUAL:
		RelationalOperator = SMP_GREATER_EQUAL;
		break;

	case SMP_GREATER_EQUAL:
		RelationalOperator = SMP_LESS_EQUAL;
		break;

	case SMP_EQUAL:
		RelationalOperator = SMP_EQUAL;
		break;

	case SMP_NOT_EQUAL:
		RelationalOperator = SMP_NOT_EQUAL;
		break;

	case SMP_BELOW:   // unsigned comparison operators BELOW, BELOW_EQUAL, ABOVE, ABOVE_EQUAL
		RelationalOperator = SMP_ABOVE;
		break;

	case SMP_BELOW_EQUAL:
		RelationalOperator = SMP_ABOVE_EQUAL;
		break;

	case SMP_ABOVE:
		RelationalOperator = SMP_BELOW;
		break;

	case SMP_ABOVE_EQUAL:
		RelationalOperator = SMP_BELOW_EQUAL;
		break;

	case SMP_CARRY:  // should only be used in Guard RTLs
		RelationalOperator = SMP_NOT_CARRY;
		break;

	case SMP_NOT_CARRY:  // should only be used in Guard RTLs
		RelationalOperator = SMP_CARRY;
		break;

	case SMP_PARITY:  // should only be used in Guard RTLs
		RelationalOperator = SMP_NOT_PARITY;
		break;

	case SMP_NOT_PARITY:  // should only be used in Guard RTLs
		RelationalOperator = SMP_PARITY;
		break;

	case SMP_OVERFLOW:  // should only be used in Guard RTLs
		RelationalOperator = SMP_NOT_OVERFLOW;
		break;

	case SMP_NOT_OVERFLOW:  // should only be used in Guard RTLs
		RelationalOperator = SMP_OVERFLOW;
		break;

	case SMP_SIGN_BIT_SET:  // should only be used in Guard RTLs
		RelationalOperator = SMP_NOT_SIGN_BIT_SET;
		break;

	case SMP_NOT_SIGN_BIT_SET:  // should only be used in Guard RTLs
		RelationalOperator = SMP_SIGN_BIT_SET;
		break;

	default:
		SMP_msg("ERROR: Non-relational operator %d in call to InvertRelationalOperator()\n", RelationalOperator);
		break;
	}

	return RelationalOperator;
} // end of InvertRelationalOperator()

// Is the given memory range just a local frame write?
bool IsLocalStackFrameExprPair(const STARSExpression *LowerExpr, const STARSExpression *UpperExpr) {
	bool StackFrameAccess = false;
	if ((nullptr != LowerExpr) && (nullptr != UpperExpr)) {
		STARS_sval_t CurrentStackOffset = LowerExpr->GetOriginalParentInst()->GetStackPtrOffset();
		STARS_sval_t FinalStackOffset;
		if (UpperExpr->IsStackPtrOffset(CurrentStackOffset, FinalStackOffset)) {
			StackFrameAccess = (0 > FinalStackOffset);
		}
	}
	return StackFrameAccess;
} // end of IsLocalStackFrameExprPair()


#if 0
// Does the CurrOperator definitely indicate a signed or unsigned operation?
bool OperatorHasSignedness(SMPoperator CurrOperator) {
	bool DetectedSignedness;

	switch (CurrOperator) {
		case SMP_NULL_OPERATOR:
			DetectedSignedness = false;
			break;

		case SMP_CALL:  // CALL instruction
			DetectedSignedness = true;
			break;

		case SMP_INPUT:  // input from port
		case SMP_OUTPUT: // output to port
		case SMP_ADDRESS_OF: // take effective address
		case SMP_GENERAL_COMPARE:
			DetectedSignedness = false;
			break;

		case SMP_U_LEFT_SHIFT: // unsigned left shift
		case SMP_U_RIGHT_SHIFT: // unsigned right shift
		case SMP_ROTATE_LEFT:
		case SMP_ROTATE_LEFT_CARRY: // rotate left through carry
		case SMP_ROTATE_RIGHT:
		case SMP_ROTATE_RIGHT_CARRY: // rotate right through carry
		case SMP_U_MULTIPLY:
		case SMP_U_DIVIDE:
		case SMP_U_REMAINDER:
		case SMP_ZERO_EXTEND:
		case SMP_BITWISE_NOT: // unary operator
		case SMP_BITWISE_XOR:
		case SMP_BITWISE_AND_NOT:
		case SMP_U_COMPARE: // unsigned compare (AND-based)
		case SMP_UNARY_POINTER_OPERATION:
			DetectedSignedness = true;
			break;

		case SMP_S_LEFT_SHIFT: // signed left shift
		case SMP_S_RIGHT_SHIFT: // signed right shift
		case SMP_S_MULTIPLY:
		case SMP_S_DIVIDE:
		case SMP_SIGN_EXTEND:
		case SMP_NEGATE:    // unary negation
		case SMP_S_COMPARE: // signed compare (subtraction-based)
		case SMP_LESS_THAN: // boolean test operators
		case SMP_GREATER_THAN:
		case SMP_LESS_EQUAL:
		case SMP_GREATER_EQUAL:
		case SMP_BELOW:
		case SMP_BELOW_EQUAL:
		case SMP_ABOVE:
		case SMP_ABOVE_EQUAL:
			DetectedSignedness = true;
			break;

		case SMP_DECREMENT:
		case SMP_INCREMENT:
		case SMP_ADD:
		case SMP_ADD_CARRY:   // add with carry
		case SMP_SUBTRACT:
		case SMP_SUBTRACT_BORROW:  // subtract with borrow
		case SMP_ASSIGN:
		case SMP_BITWISE_AND:
		case SMP_BITWISE_OR:
		case SMP_EQUAL:
		case SMP_NOT_EQUAL:
		case SMP_LOGICAL_AND:
		case SMP_LOGICAL_OR:
		case SMP_UNARY_NUMERIC_OPERATION:  // miscellaneous; produces NUMERIC result
		case SMP_BINARY_NUMERIC_OPERATION:  // miscellaneous; produces NUMERIC result
		case SMP_SYSTEM_OPERATION:   // for instructions such as CPUID, RDTSC, etc.; NUMERIC
		case SMP_SHUFFLE: // Shuffle bytes, words, etc. within destination operation per source mask
		case SMP_SIGNAL: // signal or raise exception
			DetectedSignedness = false;
			break;

		case SMP_UNARY_FLOATING_ARITHMETIC:  // all the same to our type system; all NUMERIC
		case SMP_BINARY_FLOATING_ARITHMETIC:  // all the same to our type system; all NUMERIC
		case SMP_FLOATING_ADD:
		case SMP_FLOATING_SUBTRACT:
		case SMP_FLOATING_MULTIPLY:   // floating-point multiplication of any precision; all NUMERIC
		case SMP_FLOATING_DIVIDE:     // floating-point division of any precision; all NUMERIC
		case SMP_FLOATING_NEGATE_AND_ADD: // floating negate left operand and add to right, any precision; NUMERIC
			DetectedSignedness = true;
			break;

		case SMP_REVERSE_SHIFT_U: // Shift right operand by bit count in left operand
		case SMP_COMPARE_EQ_AND_SET: // Compare for equality and set fields to all 1's or all 0's
		case SMP_COMPARE_NE_AND_SET: // Compare for inequality and set fields to all 1's or all 0's
		case SMP_COMPARE_GT_AND_SET: // Compare for greater-than and set fields to all 1's or all 0's
		case SMP_COMPARE_GE_AND_SET: // Compare for greater-than-or-equal and set fields to all 1's or all 0's
		case SMP_COMPARE_LT_AND_SET: // Compare for less-than and set fields to all 1's or all 0's
		case SMP_COMPARE_LE_AND_SET: // Compare for less-than-or-equal and set fields to all 1's or all 0's
		case SMP_PACK_S:  // Pack operands into extended-precision register, signed saturation for loss of precision
		case SMP_PACK_U:  // Pack operands into extended-precision register, unsigned saturation for loss of precision
		case SMP_AVERAGE_U: // Average of unsigned operands
		case SMP_MULTIPLY_AND_ADD: // multiply and add (or multiply and accumulate)
		case SMP_SUM_OF_DIFFS: // sum over two vectors of absolute values of differences of their elements
		case SMP_MAX_S: // dest := signed_max(dest, src)
		case SMP_MAX_U: // dest := unsigned_max(dest, src)
		case SMP_MIN_S: // dest := signed_min(dest, src)
		case SMP_MIN_U: // dest := unsigned_min(dest, src)
		case SMP_ABSOLUTE_VALUE: // take absolute value
		case SMP_CONVERT_INT_TO_FP: // convert integer to floating point
		case SMP_CONVERT_FP_TO_INT: // convert floating point to integer
		case SMP_INTERLEAVE: // extended-precision interleaving of bytes or words or dwords etc.; NUMERIC
		case SMP_CONCATENATE:     // extended-precision concatenation; NUMERIC
			DetectedSignedness = true;
			break;

		default:
			DetectedSignedness = false;
			SMP_msg("ERROR: Unknown operator in OperatorHasSignedness: %d\n", CurrOperator);
			break;
	} // end switch on operator

	return DetectedSignedness;
} // end of OperatorHasSignedness()
#endif

// Print the SPARK Ada procedure suffix for the operand, e.g. reg32 or mem16 or const32
void PrintOperandSPARKAdaSuffix(const STARSOpndTypePtr &Opnd, FILE *OutFile) {
	bool ErrorFlag = false;
	if (Opnd->IsRegOp()) {
		SMP_fprintf(OutFile, "_reg");
	}
	else if (IsMemOperand(Opnd)) {
		SMP_fprintf(OutFile, "_mem");
	}
	else if (Opnd->IsImmedOp()) {
		SMP_fprintf(OutFile, "_const");
	}
	else {
		ErrorFlag = true;
		SMP_fprintf(OutFile, "_ERROR");
	}

	// Append the bit width.
	if (!ErrorFlag) {
		std::size_t ByteWidth = Opnd->GetByteWidth();
		std::size_t BitWidth = ByteWidth * 8;
		char WidthStr[12];
		SMP_snprintf(WidthStr, 5, "%z", BitWidth);
		SMP_fprintf(OutFile, "%s", WidthStr);
	}

	return;
} // end of PrintOperandSPARKAdaSuffix()

// Construct SPARK memory write procedure call, including open parenthesis for arg list.
void GetSPARKMemWriteProcString(std::size_t OpndByteWidth, char *MemWriteString) {
	if (OpndByteWidth == 8) {
		SMP_snprintf(MemWriteString, 30, "X86.WriteMem64((");
	}
	else if (OpndByteWidth == 4) {
		SMP_snprintf(MemWriteString, 30, "X86.WriteMem32(Unsigned64(");
	}
	else if (OpndByteWidth == 2) {
		SMP_snprintf(MemWriteString, 30, "X86.WriteMem16(Unsigned64(");
	}
	else if (OpndByteWidth == 1) {
		SMP_snprintf(MemWriteString, 30, "X86.WriteMem8(Unsigned64(");
	}
	else if (OpndByteWidth == 10) {
		SMP_snprintf(MemWriteString, 30, "X86.WriteMem80(Unsigned64(");
	}

	return;
} // end of GetSPARKMemWriteProcString()

// Construct SPARK memory read procedure call, including open parenthesis for arg list.
void GetSPARKMemReadProcString(std::size_t OpndByteWidth, char *MemReadString) {
	if (OpndByteWidth == 8) {
		SMP_snprintf(MemReadString, 30, "X86.ReadMem64((");
	}
	else if (OpndByteWidth == 4) {
		SMP_snprintf(MemReadString, 30, "X86.ReadMem32(Unsigned64(");
	}
	else if (OpndByteWidth == 2) {
		SMP_snprintf(MemReadString, 30, "X86.ReadMem16(Unsigned64(");
	}
	else if (OpndByteWidth == 1) {
		SMP_snprintf(MemReadString, 30, "X86.ReadMem8(Unsigned64(");
	}
	else if (OpndByteWidth == 10) {
		SMP_snprintf(MemReadString, 30, "X86.ReadMem80(Unsigned64(");
	}

	return;
} // end of GetSPARKMemReadProcString()

// Construct SPARK bitwidth cast string. e.g. Unsigned32.
void GetSPARKWidthCastString(std::size_t OpndByteWidth, char *CastString) {
	if (OpndByteWidth == 8) {
		SMP_snprintf(CastString, 15, "Unsigned64");
	}
	else if (OpndByteWidth == 4) {
		SMP_snprintf(CastString, 15, "Unsigned32");
	}
	else if (OpndByteWidth == 2) {
		SMP_snprintf(CastString, 15, "Unsigned16");
	}
	else if (OpndByteWidth == 1) {
		SMP_snprintf(CastString, 15, "Unsigned8");
	}
	else if (OpndByteWidth == 10) {
		SMP_snprintf(CastString, 15, "Unsigned80");
	}


	return;
} // end of GetSPARKWidthCastString()

void PrintSPARKIndentTabs(FILE *OutFile) {
#define DEBUG_STARS_TABS 1
#if DEBUG_STARS_TABS
	if (STARS_SPARK_IndentCount > 8) {
		SMP_msg("ERROR: Indentation level out of range: %u\n", STARS_SPARK_IndentCount);
		STARS_SPARK_IndentCount = 8;
	}
#endif

	for (std::size_t Counter = 0; Counter < STARS_SPARK_IndentCount; ++Counter) {
		SMP_fprintf(OutFile, "\t");
	}
	return;
}

// Print an operand in SPARK-Ada form.
void SMPInstr::PrintSPARKAdaOperand(const STARSOpndTypePtr &Opnd, FILE *OutFile, bool LeftHandSide, bool UseFP, bool UseMachinePrefix, bool OmitTrailingSpace, bool UseSavedStackPtr) {
#if 1
	std::string OutString;
	this->SPARKAdaOperandToString(Opnd, OutString, LeftHandSide, UseFP, UseMachinePrefix, OmitTrailingSpace, UseSavedStackPtr);
	SMP_fprintf(OutFile, "%s", OutString.c_str());
#else
	std::size_t OpndByteWidth = Opnd->GetByteWidth();
	bool MemOpnd = IsMemOperand(Opnd);
	bool SubwordWidth = (global_STARS_program->GetSTARS_ISA_Bytewidth() > OpndByteWidth);
	bool MemWrite = LeftHandSide && MemOpnd;
	bool MemRead = MemOpnd && (!LeftHandSide);
	char MemWriteString[40] = { '\0' };

	++SPARKOperandCount;

	if (MemWrite) {
		GetSPARKMemWriteProcString(OpndByteWidth, MemWriteString);
	}
	else if (MemRead) {
		GetSPARKMemReadProcString(OpndByteWidth, MemWriteString);
	}

	if (Opnd->IsStaticMemOp()) {
		if (Opnd->HasSIBByte()) {
			SMP_fprintf(OutFile, " %s ", MemWriteString);
			SPARKAnnotPrintSIB(Opnd, true, OutFile, Opnd->GetSegReg(), UseFP, this->MDIsAddressing64bit(), UseSavedStackPtr);
			SMP_fprintf(OutFile, " + 16#%llx# )", (uint64_t) Opnd->GetAddr());
		}
		else {
			SMP_fprintf(OutFile, " %s 16#%llx# ", MemWriteString, (uint64_t) Opnd->GetAddr());
		}
		if (SubwordWidth) {
			++SubwordMemCount;
		}
	}
	else if (Opnd->IsMemNoDisplacementOp()) {
		if (Opnd->HasSIBByte()) { // has SIB info
			SMP_fprintf(OutFile, " %s ", MemWriteString);
			SPARKAnnotPrintSIB(Opnd, false, OutFile, Opnd->GetSegReg(), UseFP, this->MDIsAddressing64bit(), UseSavedStackPtr);
		}
		else { // no SIB info
			STARS_regnum_t BaseReg = Opnd->GetReg();
			STARSOpndTypePtr BaseOp = this->STARSInstPtr->MakeRegOpnd(BaseReg);
			if (this->MDIsAddressing64bit()) {
				BaseOp->SetByteWidth(8);
			}
#if STARS_SPARK_EMIT_SEGMENT_REGS
			if (Opnd->HasSegReg() && (!((STARS_x86_R_ss == Opnd->GetSegReg()) && MDIsStackAccessOpnd(Opnd, UseFP)))) {
				// We have a segment selector that is not just a redundant SS: selector for an RSP-relative access.
				STARSOpndTypePtr SegRegOp = this->STARSInstPtr->MakeRegOpnd(Opnd->GetSegReg());
				SMP_fprintf(OutFile, " %s X86.%s + X86.%s ", MemWriteString, MDGetRegName(SegRegOp), MDGetRegName(BaseOp));
			}
			else {
#endif
				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
			if (global_STARS_program->GetSTARS_ISA_Bytewidth() > BaseOp->GetByteWidth()) {
				++SubwordAddressRegCount;
			}
		}
		if (Opnd->GetAddr() != 0) {
			SMP_msg(" \n WARNING: addr for o_phrase type: %llx\n", (unsigned long long) Opnd->GetAddr());
		}
		if (SubwordWidth) {
			++SubwordMemCount;
		}
	}
	else if (Opnd->IsMemDisplacementOp()) {
		STARS_ea_t offset = Opnd->GetAddr();
		int SignedOffset = (int) offset;
		if (Opnd->HasSIBByte()) {
			SMP_fprintf(OutFile, " %s ", MemWriteString);
			SPARKAnnotPrintSIB(Opnd, (SignedOffset != 0), OutFile, Opnd->GetSegReg(), UseFP, this->MDIsAddressing64bit(), false);
			if (SignedOffset > 0) // print plus sign
				SMP_fprintf(OutFile, "+ 16#%x# )", (unsigned int) SignedOffset);
			else if (SignedOffset < 0) {
				SMP_fprintf(OutFile, "- 16#%x# )", (unsigned int) (0 - SignedOffset));
			}
		}
		else {
			STARS_regnum_t BaseReg = Opnd->GetReg();
			STARSOpndTypePtr BaseOp = this->STARSInstPtr->MakeRegOpnd(BaseReg);
			if (this->MDIsAddressing64bit()) {
				BaseOp->SetByteWidth(8);
			}
#if STARS_SPARK_EMIT_SEGMENT_REGS
			if (Opnd->HasSegReg() && (!((STARS_x86_R_ss == Opnd->GetSegReg()) && MDIsStackAccessOpnd(Opnd, UseFP)))) {
				// We have a segment selector that is not just a redundant SS: selector for an RSP-relative access.
				STARSOpndTypePtr SegRegOp = this->STARSInstPtr->MakeRegOpnd(Opnd->GetSegReg());
				SMP_fprintf(OutFile, " %s X86.%s + X86.%s ", MemWriteString, MDGetRegName(SegRegOp), MDGetRegName(BaseOp));
			}
			else {
#endif
				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
			if (SignedOffset >= 0) // print plus sign
				SMP_fprintf(OutFile, "+ 16#%x# ", (unsigned int) SignedOffset);
			else {
				SMP_fprintf(OutFile, "- 16#%x# ", (unsigned int) (0 - SignedOffset));
			}
			if (global_STARS_program->GetSTARS_ISA_Bytewidth() > BaseOp->GetByteWidth()) {
				++SubwordAddressRegCount;
			}
		}
		if (SubwordWidth) {
			++SubwordMemCount;
		}
	}
	else if (Opnd->IsRegOp()) {
		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));
		}
		else if (UseMachinePrefix) {
			SMP_fprintf(OutFile, " X86.%s", MDGetRegName(Opnd));
		}
		else {
			SMP_fprintf(OutFile, " %s", MDGetRegName(Opnd));
		}
		if (!OmitTrailingSpace) { // parameters to loop functions will get a suffix; all others need a space now
			SMP_fprintf(OutFile, " ");
		}
		if (SubwordWidth) {
			++SubwordRegCount;
		}
	}
	else if (Opnd->IsFloatingPointRegOp()) {
		bool FPStackTop = (STARS_x86_R_st0 == Opnd->GetReg());
		if (UseMachinePrefix) {
			if (FPStackTop)
				SMP_fprintf(OutFile, " X86.FloatingPointStackDummy ");
			else
				SMP_fprintf(OutFile, " X86.FloatingPointStackDummy1 ");
		}
		else {
			if (FPStackTop)
				SMP_fprintf(OutFile, " FloatingPointStackDummy ");
			else
				SMP_fprintf(OutFile, " FloatingPointStackDummy1 ");
		}
	}
	else if (Opnd->IsImmedOp()) {
		STARS_sval_t SignedImmedValue = (STARS_sval_t) Opnd->GetImmedValue();
		if (0 > SignedImmedValue) { // enclose unary minus in parentheses for Ada
			SMP_fprintf(OutFile, " (%lld) ", (long long) SignedImmedValue);
		}
		else {
			SMP_fprintf(OutFile, " 16#%llx# ", (unsigned long long) SignedImmedValue);
		}
	}
	else if (Opnd->IsFarPointer() || Opnd->IsNearPointer()) {
		SMP_fprintf(OutFile, " 16#%llx# ", (unsigned long long) Opnd->GetAddr());
	}
	else if (Opnd->IsVoidOp()) {
		; // nothing to print
	}
	else {
		SMP_fprintf(OutFile, " ERROROP");
	}

	if (MemWrite) { // close the procedure call address arg cast parentheses
		SMP_fprintf(OutFile, "), "); // e.g. MemWrite32(Unsigned64(Opnd),  
	}
	else if (MemRead) {
		SMP_fprintf(OutFile, ")) "); // e.g. MemRead8(Unsigned64(Opnd))
	}
#endif
	return;
} // end of PrintSPARKAdaOperand()

void SMPInstr::SPARKAdaOperandToString(const STARSOpndTypePtr &Opnd, std::string &OutString, 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);
	bool MemWrite = LeftHandSide && MemOpnd;
	bool MemRead = MemOpnd && (!LeftHandSide);
	char MemWriteString[40] = { '\0' };
	char TempString[40] = { '\0' };
	string SIBString;

	++SPARKOperandCount;

	if (MemWrite) {
		GetSPARKMemWriteProcString(OpndByteWidth, MemWriteString);
	}
	else if (MemRead) {
		GetSPARKMemReadProcString(OpndByteWidth, MemWriteString);
	}

	if (Opnd->IsStaticMemOp()) {
		OutString.append(" ");
		OutString.append(MemWriteString);
		if (Opnd->HasSIBByte()) {
			SPARKAnnotSIBToString(Opnd, true, SIBString, Opnd->GetSegReg(), UseFP, this->MDIsAddressing64bit(), UseSavedStackPtr);
			OutString.append(" ");
			OutString.append(SIBString);
			(void) SMP_snprintf(TempString, 20, " + 16#%llx# )", (unsigned long long) Opnd->GetAddr());
		}
		else {
			(void) SMP_snprintf(TempString, 20, " 16#%llx# ", (unsigned long long) Opnd->GetAddr());
		}
		OutString.append(" ");
		OutString.append(TempString);

		if (SubwordWidth) {
			++SubwordMemCount;
//			OutString.append(")"); // close cast parenthesis
		}
	}
	else if (Opnd->IsMemNoDisplacementOp()) {
		OutString.append(" ");
		OutString.append(MemWriteString);
		if (Opnd->HasSIBByte()) {
			SPARKAnnotSIBToString(Opnd, false, SIBString, Opnd->GetSegReg(), UseFP, this->MDIsAddressing64bit(), UseSavedStackPtr);
			OutString.append(" ");
			OutString.append(SIBString);
		}
		else { // no SIB info
			STARS_regnum_t BaseReg = Opnd->GetReg();
			STARSOpndTypePtr BaseOp = this->STARSInstPtr->MakeRegOpnd(BaseReg);
			if (this->MDIsAddressing64bit()) {
				BaseOp->SetByteWidth(8);
			}
#if STARS_SPARK_EMIT_SEGMENT_REGS
			if (Opnd->HasSegReg() && (!((STARS_x86_R_ss == Opnd->GetSegReg()) && MDIsStackAccessOpnd(Opnd, UseFP)))) {
				// We have a segment selector that is not just a redundant SS: selector for an RSP-relative access.
				STARSOpndTypePtr SegRegOp = this->STARSInstPtr->MakeRegOpnd(Opnd->GetSegReg());
				SMP_fprintf(OutFile, " %s X86.%s + X86.%s ", MemWriteString, MDGetRegName(SegRegOp), MDGetRegName(BaseOp));
			}
			else {
#endif
				if (!(UseSavedStackPtr && (BaseReg == MD_STACK_POINTER_REG))) {
					OutString.append(" X86.");
					OutString.append(MDGetRegName(BaseOp));
					OutString.append(" ");
				}
				else {
					OutString.append(" SaveStackPtr ");
				}
#if STARS_SPARK_EMIT_SEGMENT_REGS
			}
#endif
			if (global_STARS_program->GetSTARS_ISA_Bytewidth() > BaseOp->GetByteWidth()) {
				++SubwordAddressRegCount;
			}
		}
		if (Opnd->GetAddr() != 0) {
			SMP_msg(" \n WARNING: addr for o_phrase type: %llx\n", (unsigned long long) Opnd->GetAddr());
		}
		if (SubwordWidth) {
			++SubwordMemCount;
//			OutString.append(")"); // close cast parenthesis
		}
	}
	else if (Opnd->IsMemDisplacementOp()) {
		STARS_ea_t offset = Opnd->GetAddr();
		int SignedOffset = (int) offset;
		OutString.append(" ");
		OutString.append(MemWriteString);
		if (Opnd->HasSIBByte()) {
			SPARKAnnotSIBToString(Opnd, true, SIBString, Opnd->GetSegReg(), UseFP, this->MDIsAddressing64bit(), false);
			OutString.append(" ");
			OutString.append(SIBString);
			if (SignedOffset > 0) // print plus sign
				SMP_snprintf(TempString, 20, "+ 16#%x# )", (unsigned int) SignedOffset);
			else if (SignedOffset < 0) 
				SMP_snprintf(TempString, 20, "- 16#%x# )", (unsigned int) (0 - SignedOffset));
			OutString.append(TempString);
		}
		else {
			STARS_regnum_t BaseReg = Opnd->GetReg();
			STARSOpndTypePtr BaseOp = this->STARSInstPtr->MakeRegOpnd(BaseReg);
			if (this->MDIsAddressing64bit()) {
				BaseOp->SetByteWidth(8);
			}
#if STARS_SPARK_EMIT_SEGMENT_REGS
			if (Opnd->HasSegReg() && (!((STARS_x86_R_ss == Opnd->GetSegReg()) && MDIsStackAccessOpnd(Opnd, UseFP)))) {
				// We have a segment selector that is not just a redundant SS: selector for an RSP-relative access.
				STARSOpndTypePtr SegRegOp = this->STARSInstPtr->MakeRegOpnd(Opnd->GetSegReg());
				SMP_fprintf(OutFile, " %s X86.%s + X86.%s ", MemWriteString, MDGetRegName(SegRegOp), MDGetRegName(BaseOp));
			}
			else {
#endif
				if (!(UseSavedStackPtr && (BaseReg == MD_STACK_POINTER_REG))) {
					OutString.append(" X86.");
					OutString.append(MDGetRegName(BaseOp));
					OutString.append(" ");
				}
				else {
					OutString.append(" SaveStackPtr ");
				}
#if STARS_SPARK_EMIT_SEGMENT_REGS
			}
#endif
			if (SignedOffset > 0) // print plus sign
				SMP_snprintf(TempString, 20, "+ 16#%x# ", (unsigned int) SignedOffset);
			else if (SignedOffset < 0)
				SMP_snprintf(TempString, 20, "- 16#%x# ", (unsigned int) (0 - SignedOffset));
			OutString.append(TempString);
			if (global_STARS_program->GetSTARS_ISA_Bytewidth() > BaseOp->GetByteWidth()) {
				++SubwordAddressRegCount;
			}
		}
		if (SubwordWidth) {
			++SubwordMemCount;
//			OutString.append(")"); // close cast parenthesis
		}
	}
	else if (Opnd->IsRegOp()) {
		if (UseSavedStackPtr && Opnd->MatchesReg(MD_STACK_POINTER_REG)) {
			assert(!LeftHandSide);
			SMP_snprintf(TempString, 20, " SaveStackPtr");
		}
		else if (SubwordWidth && LeftHandSide) {
			// Subword reg writes are procedure calls, e.g. Write_EDI(...
			SMP_snprintf(TempString, 20, " X86.Write_%s(", MDGetRegName(Opnd));
		}
		else if (UseMachinePrefix) {
			SMP_snprintf(TempString, 20, " X86.%s", MDGetRegName(Opnd));
		}
		else {
			SMP_snprintf(TempString, 20, " %s", MDGetRegName(Opnd));
		}
		OutString.append(TempString);
		if (!OmitTrailingSpace) { // parameters to loop functions will get a suffix; all others need a space now
			OutString.append(" ");
		}
		if (SubwordWidth) {
			++SubwordRegCount;
		}
	}
	else if (Opnd->IsFloatingPointRegOp()) {
		bool FPStackTop = (STARS_x86_R_st0 == Opnd->GetReg());
		if (UseMachinePrefix) {
			if (FPStackTop)
				OutString.append(" X86.FloatingPointStackDummy ");
			else
				OutString.append(" X86.FloatingPointStackDummy1 ");
		}
		else {
			if (FPStackTop)
				OutString.append(" X86.FloatingPointStackDummy ");
			else
				OutString.append(" X86.FloatingPointStackDummy1 ");
		}
	}
	else if (Opnd->IsImmedOp()) {
		STARS_sval_t SignedImmedValue = (STARS_sval_t)Opnd->GetImmedValue();
		if (0 > SignedImmedValue) { // enclose unary minus in parentheses for Ada
			SMP_snprintf(TempString, 20, " (%lld) ", (long long) SignedImmedValue);
		}
		else {
			SMP_snprintf(TempString, 20, " 16#%llx# ", (unsigned long long) SignedImmedValue);
		}
		OutString.append(TempString);
	}
	else if (Opnd->IsFarPointer() || Opnd->IsNearPointer()) {
		SMP_snprintf(TempString, 20, " 16#%llx# ", (unsigned long long) Opnd->GetAddr());
		OutString.append(TempString);
	}
	else if (Opnd->IsVoidOp()) {
		; // nothing to print
	}
	else {
		OutString.append(" ERROROP");
	}

	if (MemWrite) { // close the procedure call address arg cast parentheses
		OutString.append("), "); // e.g. MemWrite32(Unsigned64(Opnd),  
	}
	else if (MemRead) {
		OutString.append(")) "); // e.g. MemRead8(Unsigned64(Opnd))
	}
	return;
} // 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, bool UseSavedStackPtr) {
	bool MemOpnd = IsMemOperand(Opnd);

	assert(MemOpnd);

	if (Opnd->IsStaticMemOp()) {
		if (Opnd->HasSIBByte()) {
			SPARKAnnotPrintSIB(Opnd, true, OutFile, Opnd->GetSegReg(), UseFP, this->MDIsAddressing64bit(), UseSavedStackPtr);
			SMP_fprintf(OutFile, " + 16#%llx# )", (uint64_t) Opnd->GetAddr());
		}
		else {
			SMP_fprintf(OutFile, " 16#%llx# ", (uint64_t) Opnd->GetAddr());
		}
	}
	else if (Opnd->IsMemNoDisplacementOp()) {
		if (Opnd->HasSIBByte()) { // has SIB info
			SPARKAnnotPrintSIB(Opnd, false, OutFile, Opnd->GetSegReg(), UseFP, this->MDIsAddressing64bit(), UseSavedStackPtr);
		}
		else { // no SIB info
			STARS_regnum_t BaseReg = Opnd->GetReg();
			STARSOpndTypePtr BaseOp = this->STARSInstPtr->MakeRegOpnd(BaseReg);
			if (this->MDIsAddressing64bit()) {
				BaseOp->SetByteWidth(8);
			}
#if STARS_SPARK_EMIT_SEGMENT_REGS
			if (Opnd->HasSegReg() && (!((STARS_x86_R_ss == Opnd->GetSegReg()) && MDIsStackAccessOpnd(Opnd, UseFP)))) {
				// We have a segment selector that is not just a redundant SS: selector for an RSP-relative access.
				STARSOpndTypePtr SegRegOp = this->STARSInstPtr->MakeRegOpnd(Opnd->GetSegReg());
				SMP_fprintf(OutFile, " X86.%s + X86.%s ", MDGetRegName(SegRegOp), MDGetRegName(BaseOp));
			}
			else {
#endif
				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
		}
		if (Opnd->GetAddr() != 0) {
			SMP_msg(" \n WARNING: addr for o_phrase type: %llx\n", (uint64_t) Opnd->GetAddr());
		}
	}
	else if (Opnd->IsMemDisplacementOp()) {
		STARS_ea_t offset = Opnd->GetAddr();
		int SignedOffset = (int) offset;
		if (Opnd->HasSIBByte()) {
			SPARKAnnotPrintSIB(Opnd, (SignedOffset != 0), OutFile, Opnd->GetSegReg(), UseFP, this->MDIsAddressing64bit(), UseSavedStackPtr);
			if (SignedOffset > 0) // print plus sign
				SMP_fprintf(OutFile, "+ 16#%x# )", (unsigned int) SignedOffset);
			else if (SignedOffset < 0) // minus sign will print automatically
				SMP_fprintf(OutFile, "%d )", SignedOffset);
		}
		else {
			STARS_regnum_t BaseReg = Opnd->GetReg();
			STARSOpndTypePtr BaseOp = this->STARSInstPtr->MakeRegOpnd(BaseReg);
			if (this->MDIsAddressing64bit()) {
				BaseOp->SetByteWidth(8);
			}
#if STARS_SPARK_EMIT_SEGMENT_REGS
			if (Opnd->HasSegReg() && (!((STARS_x86_R_ss == Opnd->GetSegReg()) && MDIsStackAccessOpnd(Opnd, UseFP)))) {
				// We have a segment selector that is not just a redundant SS: selector for an RSP-relative access.
				STARSOpndTypePtr SegRegOp = this->STARSInstPtr->MakeRegOpnd(Opnd->GetSegReg());
				SMP_fprintf(OutFile, " X86.%s + X86.%s ", MDGetRegName(SegRegOp), MDGetRegName(BaseOp));
			}
			else {
#endif
				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
			if (SignedOffset >= 0) // print plus sign
				SMP_fprintf(OutFile, "+ 16#%x# ", (unsigned int) SignedOffset);
			else // minus sign will print automatically
				SMP_fprintf(OutFile, "%d ", SignedOffset);
		}
	}
	else {
		SMP_fprintf(OutFile, " ERROROP");
	}

	return;
} // end of PrintSPARKAdaAddressExpr()

// Print an operator in SPARK-Ada form.
void PrintSPARKAdaOperator(SMPoperator Oper, string &OutString, bool &PrefixProcCall, bool &PrefixUnary, bool ConstFollows) {
	PrefixProcCall = false;
	PrefixUnary = false;

	switch (Oper) {
		case SMP_NULL_OPERATOR: 
		case SMP_INPUT:  // input from port
		case SMP_OUTPUT: // output to port
		case SMP_ADDRESS_OF: // take effective address
		case SMP_S_LEFT_SHIFT: // signed left shift
		case SMP_ROTATE_LEFT_CARRY: // rotate left through carry
		case SMP_ROTATE_RIGHT_CARRY: // rotate right through carry
			SMP_msg("ERROR: SPARK: Cannot translate operator: ");
			SMP_msg(" %s \n", OperatorText[Oper]);
			OutString = "ERROR";
			break;

		case SMP_ADD_CARRY:   // add with carry
			OutString = " X86.adc";
			PrefixProcCall = true;
			break;

		case SMP_SUBTRACT_BORROW:  // subtract with borrow
			OutString = " X86.sbb";
			PrefixProcCall = true;
			break;

		case SMP_CALL:  // CALL instruction
			break;

		case SMP_U_LEFT_SHIFT: // unsigned left shift
		case SMP_REVERSE_SHIFT_U: // Shift right operand by bit count in left operand
			OutString = " Interfaces.Shift_Left";
			PrefixProcCall = true;
			break;

		case SMP_U_RIGHT_SHIFT: // unsigned right shift
			OutString = " Interfaces.Shift_Right";
			PrefixProcCall = true;
			break;

		case SMP_S_RIGHT_SHIFT: // signed right shift
			OutString = " Interfaces.Shift_Right_Arithmetic";
			PrefixProcCall = true;
			break;

		case SMP_ROTATE_LEFT:
			OutString = " Interfaces.Rotate_Left";
			PrefixProcCall = true;
			break;

		case SMP_ROTATE_RIGHT:
			OutString = " Interfaces.Rotate_Right";
			PrefixProcCall = true;
			break;