path: root/stp/AST/Transform.cpp

/********************************************************************
 * AUTHORS: Vijay Ganesh, David L. Dill
 *
 * BEGIN DATE: November, 2005
 *
 * LICENSE: Please view LICENSE file in the home dir of this Program
 ********************************************************************/
// -*- c++ -*-

#include "AST.h"
#include <stdlib.h>
#include <stdio.h>
namespace BEEV {  
  
  //Translates signed BVDIV/BVMOD into unsigned variety
  ASTNode BeevMgr::TranslateSignedDivMod(const ASTNode& in) {
    if(!(SBVMOD == in.GetKind() || SBVDIV == in.GetKind())) {
      FatalError("TranslateSignedDivMod: input must be signed DIV/MOD\n",in);
    }

    ASTNode dividend = in[0];
    ASTNode divisor  = in[1];      
    unsigned len = in.GetValueWidth();
    if(SBVMOD == in.GetKind()) {
      //if(TopBit(dividend)==1) 
      //
      //then -BVMOD(-dividend,abs(divisor)) 
      //
      //else BVMOD(dividend,abs(divisor))

      //create the condition for the dividend
      ASTNode hi1  = CreateBVConst(32,len-1);
      ASTNode one  = CreateOneConst(1);
      ASTNode cond = CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1));

      //create the condition and conditional for the divisor
      ASTNode cond_divisor = CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,divisor,hi1,hi1));
      ASTNode pos_divisor  = CreateTerm(ITE,len,cond_divisor,CreateTerm(BVUMINUS,len,divisor),divisor);

      //create the modulus term for each case
      ASTNode modnode = CreateTerm(BVMOD,len,dividend,pos_divisor);
      ASTNode minus_modnode = CreateTerm(BVMOD,len,CreateTerm(BVUMINUS,len,dividend),pos_divisor);
      minus_modnode = CreateTerm(BVUMINUS,len,minus_modnode);

      //put everything together, simplify, and return
      ASTNode n = CreateTerm(ITE,len,cond,minus_modnode,modnode);
      return SimplifyTerm_TopLevel(n);
    }
    
    //now handle the BVDIV case
    //if topBit(dividend) is 1 and topBit(divisor) is 0
    //
    //then output is -BVDIV(-dividend,divisor)
    //
    //elseif topBit(dividend) is 0 and topBit(divisor) is 1
    //
    //then output is -BVDIV(dividend,-divisor)
    //
    //elseif topBit(dividend) is 1 and topBit(divisor) is 1
    //
    // then output is BVDIV(-dividend,-divisor)
    //
    //else simply output BVDIV(dividend,divisor)
    ASTNode hi1 = CreateBVConst(32,len-1);
    ASTNode zero = CreateZeroConst(1);
    ASTNode one = CreateOneConst(1);
    ASTNode divnode = CreateTerm(BVDIV, len, dividend, divisor);

    ASTNode cond1 = CreateNode(AND,
			       CreateNode(EQ,zero,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1)),
			       CreateNode(EQ,one, CreateTerm(BVEXTRACT,1,divisor,hi1,hi1)));
    ASTNode minus_divnode1 = CreateTerm(BVDIV,len,
					dividend,
					CreateTerm(BVUMINUS,len,divisor));
    minus_divnode1 = CreateTerm(BVUMINUS,len,minus_divnode1);

    ASTNode cond2 = CreateNode(AND,
			       CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1)),
			       CreateNode(EQ,zero,CreateTerm(BVEXTRACT,1,divisor,hi1,hi1)));
    ASTNode minus_divnode2 = CreateTerm(BVDIV,len,
					CreateTerm(BVUMINUS,len,dividend),
					divisor);
    minus_divnode2 = CreateTerm(BVUMINUS,len,minus_divnode2);

    ASTNode cond3 = CreateNode(AND,
			       CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1)),
			       CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,divisor,hi1,hi1)));
    ASTNode minus_divnode3 = CreateTerm(BVDIV,len,
					CreateTerm(BVUMINUS,len,dividend),
					CreateTerm(BVUMINUS,len,divisor));
    ASTNode n = CreateTerm(ITE,len,
			   cond1,
			   minus_divnode1,
			   CreateTerm(ITE,len,
				      cond2,
				      minus_divnode2,
				      CreateTerm(ITE,len,
						 cond3,
						 minus_divnode3,
						 divnode)));
  return SimplifyTerm_TopLevel(n);
  }//end of TranslateSignedDivMod()

  ASTNode BeevMgr::TransformFormula(const ASTNode& form) {
    ASTNode result;

    ASTNode simpleForm = form;
    Kind k = simpleForm.GetKind();
    if(!(is_Form_kind(k) && BOOLEAN_TYPE == simpleForm.GetType())) {
      //FIXME: "You have inputted a NON-formula"?
      FatalError("TransformFormula: You have input a NON-formula",simpleForm);
    }

    ASTNodeMap::iterator iter;
    if((iter = TransformMap.find(simpleForm)) != TransformMap.end())
      return iter->second;

    switch(k) {
    case TRUE:
    case FALSE: {
      result = simpleForm;
      break;
    }
    case NOT: {
      ASTVec c;
      c.push_back(TransformFormula(simpleForm[0]));
      result = CreateNode(NOT,c);      
      break;
    }
    case BVLT:
    case BVLE:
    case BVGT:
    case BVGE:
    case BVSLT:
    case BVSLE:
    case BVSGT:
    case BVSGE:      
    case NEQ: {
      ASTVec c;
      c.push_back(TransformTerm(simpleForm[0]));      
      c.push_back(TransformTerm(simpleForm[1]));
      result = CreateNode(k,c);
      break;
    }
    case EQ: {
      ASTNode term1 = TransformTerm(simpleForm[0]);      
      ASTNode term2 = TransformTerm(simpleForm[1]);
      result = CreateSimplifiedEQ(term1,term2);     
      break;
    }
    case AND:
    case OR: 
    case NAND:
    case NOR:
    case IFF:
    case XOR:
    case ITE:
    case IMPLIES: {
      ASTVec vec;
      ASTNode o;
      for (ASTVec::const_iterator it = simpleForm.begin(),itend=simpleForm.end(); it != itend; it++){
	o = TransformFormula(*it);	
	vec.push_back(o);
      }

      result = CreateNode(k, vec);
      break;
    }
    default:
      if(k == SYMBOL && BOOLEAN_TYPE == simpleForm.GetType())
	result = simpleForm;      
      else {
	cerr << "The input is: " << simpleForm << endl;
	cerr << "The valuewidth of input is : " << simpleForm.GetValueWidth() << endl;
	FatalError("TransformFormula: Illegal kind: ",ASTUndefined, k);
      }
      break;    
    } 
    //BVTypeCheck(result);
    TransformMap[simpleForm] = result;
    return result;
  } //End of TransformFormula

  ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm) {
    ASTNode result;
    ASTNode term = inputterm;

    Kind k = term.GetKind();
    if(!is_Term_kind(k))
      FatalError("TransformTerm: Illegal kind: You have input a nonterm:", inputterm, k);
    ASTNodeMap::iterator iter;
    if((iter = TransformMap.find(term)) != TransformMap.end())
      return iter->second;
    switch(k) {
    case SYMBOL: {
      // ASTNodeMap::iterator itsym;
//       if((itsym = CounterExampleMap.find(term)) != CounterExampleMap.end())	
//       	result = itsym->second;
//       else
	result = term;
      break;
    }
    case BVCONST:
      result = term;
      break;
    case WRITE:
      FatalError("TransformTerm: this kind is not supported",term);
      break;
    case READ:
      result = TransformArray(term);
      break;
    case ITE: {
      ASTNode cond = term[0];
      ASTNode thn  = term[1];
      ASTNode els  = term[2];
      cond = TransformFormula(cond);
      thn = TransformTerm(thn);
      els = TransformTerm(els);
      //result = CreateTerm(ITE,term.GetValueWidth(),cond,thn,els);
      result = CreateSimplifiedTermITE(cond,thn,els);
      result.SetIndexWidth(term.GetIndexWidth());
      break;
    }
    default: {
      ASTVec c = term.GetChildren();
      ASTVec::iterator it = c.begin();
      ASTVec::iterator itend = c.end();
      unsigned width = term.GetValueWidth();
      unsigned indexwidth = term.GetIndexWidth();
      ASTVec o;
      for(;it!=itend;it++) {
	o.push_back(TransformTerm(*it));
      }

      result = CreateTerm(k,width,o);
      result.SetIndexWidth(indexwidth);

      if(SBVDIV == result.GetKind() || SBVMOD == result.GetKind()) {
	result = TranslateSignedDivMod(result);
      }
      break;
    }
    }

    TransformMap[term] = result;
    if(term.GetValueWidth() != result.GetValueWidth())
      FatalError("TransformTerm: result and input terms are of different length", result);
    if(term.GetIndexWidth() != result.GetIndexWidth()) {
      cerr << "TransformTerm: input term is : " << term << endl;
      FatalError("TransformTerm: result and input terms have different index length", result);
    }
    return result;
  } //End of TransformTerm

  /* This function transforms Array Reads, Read over Writes, Read over
   * ITEs into flattened form.
   *
   * Transform1: Suppose there are two array reads in the input
   * Read(A,i) and Read(A,j) over the same array. Then Read(A,i) is
   * replaced with a symbolic constant, say v1, and Read(A,j) is
   * replaced with the following ITE:
   *
   * ITE(i=j,v1,v2)
   *
   * Transform2:
   * 
   * Transform3:
   */
  ASTNode BeevMgr::TransformArray(const ASTNode& term) {
    ASTNode result = term;

    unsigned int width = term.GetValueWidth();
    Kind k = term.GetKind();
    if (!is_Term_kind(k))
      FatalError("TransformArray: Illegal kind: You have input a nonterm:", ASTUndefined, k);
    ASTNodeMap::iterator iter;
    if((iter = TransformMap.find(term)) != TransformMap.end())
      return iter->second;

    switch(k) {
      //'term' is of the form READ(arrName, readIndex) 
    case READ: {
      ASTNode arrName = term[0];
      switch (arrName.GetKind()) {
      case SYMBOL: {
	/* input is of the form: READ(A, readIndex)
	 * 
	 * output is of the from: A1, if this is the first READ over A
         *                           
	 *                        ITE(previous_readIndex=readIndex,A1,A2)
	 *                        
         *                        .....
	 */

	//  Recursively transform read index, which may also contain reads.
	ASTNode readIndex = TransformTerm(term[1]);	
	ASTNode processedTerm = CreateTerm(READ,width,arrName,readIndex);
	
	//check if the 'processedTerm' has a corresponding ITE construct
	//already. if so, return it. else continue processing.
	ASTNodeMap::iterator it;
	if((it = _arrayread_ite.find(processedTerm)) != _arrayread_ite.end()) {
	  result = it->second;	
	  break;
	}
	//Constructing Symbolic variable corresponding to 'processedTerm'
	ASTNode CurrentSymbol;
	ASTNodeMap::iterator it1;
	// First, check if read index is constant and it has a constant value in the substitution map.
	if(CheckSubstitutionMap(processedTerm,CurrentSymbol)) {
	  _arrayread_symbol[processedTerm] = CurrentSymbol;
	}
	// Check if it already has an abstract variable.
	else if((it1 = _arrayread_symbol.find(processedTerm)) != _arrayread_symbol.end()) {
	  CurrentSymbol = it1->second;
	}
	else {
	  // Make up a new abstract variable.
	  // FIXME: Make this into a method (there already may BE a method) and
	  // get rid of the fixed-length buffer!
	  //build symbolic name corresponding to array read. The symbolic
	  //name has 2 components: stringname, and a count
	  const char * b = arrName.GetName();
	  std::string c(b);
	  char d[32];
	  sprintf(d,"%d",_symbol_count++);
	  std::string ccc(d);
	  c += "array_" + ccc;
	  
	  CurrentSymbol = CreateSymbol(c.c_str());
	  CurrentSymbol.SetValueWidth(processedTerm.GetValueWidth());
	  CurrentSymbol.SetIndexWidth(processedTerm.GetIndexWidth());
	  _arrayread_symbol[processedTerm] = CurrentSymbol;	  
	}
	
	//list of array-read indices corresponding to arrName, seen while
	//traversing the AST tree. we need this list to construct the ITEs
	// Dill: we hope to make this irrelevant.  Harmless for now.
	ASTVec readIndices = _arrayname_readindices[arrName];
	
	//construct the ITE structure for this array-read
	ASTNode ite = CurrentSymbol;
	_introduced_symbols.insert(CurrentSymbol);
	BVTypeCheck(ite);
	
	if(arrayread_refinement) {
	  // ite is really a variable here; it is an ite in the
	  // else-branch
	  result = ite;
	}
	else {
	  // Full Seshia transform if we're not doing read refinement.
	  //do not loop if the current readIndex is a BVCONST
	  // if(BVCONST == term[1].GetKind() && !SeenNonConstReadIndex && optimize) {
	  // 	    result = ite; 
	  // 	  }
	  // 	  else {	  
	    //else part: SET the SeenNonConstReadIndex var, and do the hard work
	    //SeenNonConstReadIndex = true;
	    ASTVec::reverse_iterator it2=readIndices.rbegin();
	    ASTVec::reverse_iterator it2end=readIndices.rend();
	    for(;it2!=it2end;it2++) {
	      ASTNode cond = CreateSimplifiedEQ(readIndex,*it2);
	      if(ASTFalse == cond)
		continue;
	      
	      ASTNode arrRead = CreateTerm(READ,width,arrName,*it2);
	      //Good idea to TypeCheck internally constructed nodes
	      BVTypeCheck(arrRead);
	      
	      ASTNode arrayreadSymbol = _arrayread_symbol[arrRead];
	      if(arrayreadSymbol.IsNull())
		FatalError("TransformArray:symbolic variable for processedTerm, p," 
			   "does not exist:p = ",arrRead);
	      ite = CreateSimplifiedTermITE(cond,arrayreadSymbol,ite);
	    }
	    result = ite;
	    //}
	}
	
	_arrayname_readindices[arrName].push_back(readIndex);	
	//save the ite corresponding to 'processedTerm'
	_arrayread_ite[processedTerm] = result;
	break;
      } //end of READ over a SYMBOL
      case WRITE:{	
	/* The input to this case is: READ((WRITE A i val) j)
	 *
	 * The output of this case is: ITE( (= i j) val (READ A i))
	 */
	
	/* 1. arrName or term[0] is infact a WRITE(A,i,val) expression
	 *
	 * 2. term[1] is the read-index j
	 *
	 * 3. arrName[0] is the new arrName i.e. A. A can be either a
              SYMBOL or a nested WRITE. no other possibility
	 *
	 * 4. arrName[1] is the WRITE index i.e. i
	 *
	 * 5. arrName[2] is the WRITE value i.e. val (val can inturn
	 *    be an array read)
	 */
	ASTNode readIndex = TransformTerm(term[1]);
	ASTNode writeIndex = TransformTerm(arrName[1]);
	ASTNode writeVal = TransformTerm(arrName[2]);
	
	if(!(SYMBOL == arrName[0].GetKind() || 
	     WRITE == arrName[0].GetKind())) 
	  FatalError("TransformArray: An array write is being attempted on a non-array:",term);
	if(ARRAY_TYPE != arrName[0].GetType())
	  FatalError("TransformArray: An array write is being attempted on a non-array:",term);
	
	ASTNode cond = CreateSimplifiedEQ(writeIndex,readIndex);
	//TypeCheck internally created node
	BVTypeCheck(cond);
	ASTNode readTerm = CreateTerm(READ,width,arrName[0],readIndex);
	//TypeCheck internally created node
	BVTypeCheck(readTerm);
	ASTNode readPushedIn = TransformArray(readTerm);
	//TypeCheck internally created node
	BVTypeCheck(readPushedIn);
	//result = CreateTerm(ITE, arrName[0].GetValueWidth(),cond,writeVal,readPushedIn);
	result = CreateSimplifiedTermITE(cond,writeVal,readPushedIn);

	//Good idea to typecheck terms created inside the system
	BVTypeCheck(result);
	break;
      } //end of READ over a WRITE
      case ITE: {
	/* READ((ITE cond thn els) j) 
	 *
	 * is transformed into
	 *
	 * (ITE cond (READ thn j) (READ els j))
	 */
	
	//(ITE cond thn els)
	ASTNode term0 = term[0];
	//READINDEX j
	ASTNode j = TransformTerm(term[1]);
	
	ASTNode cond = term0[0];
	//first array 
	ASTNode t01  = term0[1];
	//second array
	ASTNode t02  = term0[2];
	
	cond = TransformFormula(cond);
	ASTNode thn = TransformTerm(t01);
	ASTNode els = TransformTerm(t02);
	
	if(!(t01.GetValueWidth() == t02.GetValueWidth() &&
	     t01.GetValueWidth() == thn.GetValueWidth() &&
	     t01.GetValueWidth() == els.GetValueWidth()))
	  FatalError("TransformArray: length of THENbranch != length of ELSEbranch in the term t = \n",term);

	if(!(t01.GetIndexWidth() == t02.GetIndexWidth() &&
	     t01.GetIndexWidth() == thn.GetIndexWidth() &&
	     t01.GetIndexWidth() == els.GetIndexWidth()))
	  FatalError("TransformArray: length of THENbranch != length of ELSEbranch in the term t = \n",term);

	//(READ thn j)
	ASTNode thnRead = CreateTerm(READ,width,thn,j);
	BVTypeCheck(thnRead);
	thnRead = TransformArray(thnRead);
	
	//(READ els j)
	ASTNode elsRead = CreateTerm(READ,width,els,j);
	BVTypeCheck(elsRead);
	elsRead = TransformArray(elsRead);
	
	//(ITE cond (READ thn j) (READ els j))
	result = CreateSimplifiedTermITE(cond,thnRead,elsRead);
	BVTypeCheck(result);
      break;
      }
      default:
	FatalError("TransformArray: The READ is NOT over SYMBOL/WRITE/ITE",term);
	break;
      } 
      break;
    } //end of READ switch
    default:
      FatalError("TransformArray: input term is of wrong kind: ",ASTUndefined);
      break;
    }
    
    TransformMap[term] = result;
    return result;
  } //end of TransformArray()  
} //end of namespace BEEV