void ExprWalker::visit(SgInitializedName* sgn)
{
  VariableId vid = vidm.variableId(sgn);
  
  // some SgInitializedName do not have symbols
  // VariableId is not created for such SgInitializedName
  // check and return if we are processing such SgInitializedName
  if(!vid.isValid()) {
    //cerr << "WARNING: Skipping SgInitializedName sgn->get_name() = " << sgn->get_name() << " with no symbol\n";
    return;
  }

  DefUseVarsInfo rduvi;
  SgInitializer* initializer = sgn->get_initializer();
  if(initializer) {
    rduvi = getDefUseVarsInfo_rec(initializer, vidm, false);
  }

  // SgInitializedName always define a variable
  // it should always be in def_set
  VarsInfo& def_vars_info = duvi.getDefVarsInfoMod();
  
  // determine the type info
  VariableIdTypeInfo sgn_type_info = getVariableIdTypeInfo(vid, vidm);

  if(vidm.getModeVariableIdForEachArrayElement() && sgn_type_info == arrayType)
    // When defining an array, define all its elements.
    duvi.addAllArrayElements(sgn, vidm, true);
  else
    def_vars_info.first.insert(VariableIdInfo(vid, sgn_type_info));

  duvi = duvi + rduvi;
}

VariableId VariableIdMapping::variableIdOfArrayElement(VariableId arrayVar, int elemIndex) {
  int idCode = arrayVar.getIdCode();
  int elemIdCode = idCode + elemIndex;
  VariableId elemVarId;
  elemVarId.setIdCode(elemIdCode);
  return elemVarId;
}

// base case for the recursion
void SPRAY::ComputeAddressTakenInfo::OperandToVariableId::visit(SgVarRefExp *sgn)
{ 
  if(debuglevel > 0) debugPrint(sgn);
  VariableId id = cati.vidm.variableId(sgn);
  ROSE_ASSERT(id.isValid());
  // insert the id into VariableIdSet
  cati.addressTakenInfo.second.insert(id);
}

/*! 
  * \author Markus Schordan
  * \date 2012.
 */
string VariableIdMapping::uniqueShortVariableName(VariableId varId) {
  if(!isTemporaryVariableId(varId)) {
    return variableName(varId)+"_"+varId.toString().substr(1);
    //return SgNodeHelper::uniqueLongVariableName(getSymbol(varId));
  } else {
    return string("tmp")+"_"+varId.toString().substr(1);
  }
}

/*! 
  * \author Markus Schordan
  * \date 2012.
 */
VariableIdMapping::VariableIdSet VariableIdMapping::getVariableIdSet() {
  VariableIdSet set;
  for(map<SgSymbol*,size_t>::iterator i=mappingSymToVarId.begin();i!=mappingSymToVarId.end();++i) {
    size_t t=(*i).second;
    VariableId id;
    id.setIdCode(t);
    set.insert(id);
  }
  return set;
}

// Returns a valid VariableId corresponding to *ref*
// if indices in *ref* are all integers and sizes of
// all array dimensions are known.
// Returns an invalid VariableId otherwise.
VariableId VariableIdMapping::idForArrayRef(SgPntrArrRefExp* ref)
{
  assert(ref);
  VariableId result;
  result.setIdCode(-1);

  // Check failure conditions
  if(isSgPntrArrRefExp(ref->get_parent()))
    return result;
  SgExpression* varRef;
  vector<SgExpression*> subscripts;
  vector<SgExpression*>* pSubscripts = &subscripts;
  SageInterface::isArrayReference(ref, &varRef, &pSubscripts);
  SgVarRefExp* arrVar = isSgVarRefExp(varRef);
  if(!arrVar)
    return result;
  SgArrayType* arrType = isSgArrayType(SageInterface::convertRefToInitializedName(arrVar)->get_type());
  if(!arrType)
    return result;
  vector<size_t> arrayDimensions;
  size_t arrSize = getArrayDimensions(arrType, &arrayDimensions);
  if(!arrSize) {
    arrayDimensions.clear();
    arrSize = getArrayDimensionsFromInitializer(
                isSgAggregateInitializer(SageInterface::convertRefToInitializedName(arrVar)->get_initializer()), 
                &arrayDimensions);
  }
  if(!arrSize)
    return result; // Array size is unknown
  assert(arrayDimensions.size() == subscripts.size());

  // Calculate the index as below.
  // int a[M][N][K];
  // a[x][y][z] => index = x*N*K + y*K + z.
  int index = 0;
  for(unsigned i = 0; i < subscripts.size(); i++) {
    int curIndex = exprToInt(subscripts[i]);
    if(curIndex == -1)
      return result;
    int dimension_size = (i == arrayDimensions.size() - 1 ? 1 : arrayDimensions[i + 1]);
    for(unsigned d = i + 2; d < arrayDimensions.size(); d++)
      dimension_size*= arrayDimensions[d];
    index += curIndex*dimension_size;
  }

  VariableId varId = variableId(arrVar);
  result = variableIdOfArrayElement(varId, index);
  return result;
}

VariableValueRangeInfo VariableConstInfo::createVariableValueRangeInfo(VariableId varId, VarConstSetMap& map) {
    ROSE_ASSERT(map.size()>0);
    ROSE_ASSERT(varId.isValid());
    set<CppCapsuleConstIntLattice> cppCapsuleSet=map[varId];
    AType::ConstIntLattice minVal;
    AType::ConstIntLattice maxVal;
    // in case the set of collected assignments is empty, bot is returned (min and max remain bot).
    if(cppCapsuleSet.size()==0)
        return VariableValueRangeInfo(AType::ConstIntLattice(AType::Bot()));
    for(set<CppCapsuleConstIntLattice>::iterator i=cppCapsuleSet.begin(); i!=cppCapsuleSet.end(); ++i) {
        AType::ConstIntLattice aint=(*i).getValue();
        if(aint.isTop()) {
            return VariableValueRangeInfo(AType::ConstIntLattice(AType::Top()));
        }

        if(minVal.isBot() && maxVal.isBot()) {
            minVal=aint;
            maxVal=aint;
            continue;
        }
        if((aint<minVal).isTrue())
            minVal=aint;
        if((aint>maxVal).isTrue())
            maxVal=aint;
    }
    if(minVal.isBot()||maxVal.isBot())
        return VariableValueRangeInfo(AType::ConstIntLattice(AType::Bot()));
    return VariableValueRangeInfo(minVal,maxVal);
}

VariableIdMapping::VariableIdSet VariableIdMapping::variableIdsOfAstSubTree(SgNode* node) {
  VariableIdSet vset;
  RoseAst ast(node);
  for(RoseAst::iterator i=ast.begin();i!=ast.end();++i) {
    VariableId vid; // default creates intentionally an invalid id.
    if(SgVariableDeclaration* varDecl=isSgVariableDeclaration(*i)) {
      vid=variableId(varDecl);
    } else if(SgVarRefExp* varRefExp=isSgVarRefExp(*i)) {
      vid=variableId(varRefExp);
    } else if(SgInitializedName* initName=isSgInitializedName(*i)) {
      vid=variableId(initName);
    }
    if(vid.isValid())
      vset.insert(vid);
  }
  return vset;
}

/*! 
  * \author Markus Schordan
  * \date 2013.
 */
void RDTransferFunctions::transferExpression(Label lab, SgExpression* node, Lattice& element0) {
  RDLattice* element1=dynamic_cast<RDLattice*>(&element0);
  ROSE_ASSERT(element1);
  RDLattice& element=*element1;
  // update analysis information
  // this is only correct for RERS12-C programs
  // 1) remove all pairs with lhs-variableid
  // 2) add (lab,lhs.varid)

  // (for programs with pointers we require a set here)
  VariableIdSet defVarIds=AnalysisAbstractionLayer::defVariables(node,*_variableIdMapping);  
  ROSE_ASSERT(_pointerAnalysisInterface);
  if(hasDereferenceOperation(node)) {
    VariableIdSet modVarIds=_pointerAnalysisInterface->getModByPointer();
    // union sets
    defVarIds+=modVarIds;
  }
  if(defVarIds.size()>1 /* TODO: || existsArrayVarId(defVarIds)*/ ) {
    // If an unknown array element is referenced, we consider
    // all its elements modified in the same statement.
    // Here *var* is an array element if its symbol is equal to at
    // least one of those corresponding to VariableIds with next or previous ids.
    for(VariableIdMapping::VariableIdSet::iterator i=defVarIds.begin();i!=defVarIds.end();++i) {
      VariableId var = *i;
      VariableId prev_var_id;
      VariableId next_var_id;
      prev_var_id.setIdCode(var.getIdCode() - 1);
      next_var_id.setIdCode(var.getIdCode() + 1);
      SgSymbol *var_smb = _variableIdMapping->getSymbol(var);
      SgSymbol *prev_var_smb = _variableIdMapping->getSymbol(prev_var_id);
      SgSymbol *next_var_smb = _variableIdMapping->getSymbol(next_var_id);
      if((var_smb == prev_var_smb) || (var_smb == next_var_smb))
        element.removeAllPairsWithVariableId(var);
    }
    // since multiple memory locations may be modified, we cannot know which one will be updated and can only add information
    for(VariableIdMapping::VariableIdSet::iterator i=defVarIds.begin();i!=defVarIds.end();++i) {
      element.insertPair(lab,*i);
    }
  } else if(defVarIds.size()==1) {
    // one unique memory location (variable). We can remove all pairs with this variable
    VariableId var=*defVarIds.begin();
    element.removeAllPairsWithVariableId(var);
    element.insertPair(lab,var);
  }
}

void ExprWalker::visit(SgVarRefExp* sgn)
{
  // get the VariableId
  VariableId vid = vidm.variableId(sgn);
  
  ROSE_ASSERT(vid.isValid());

  // determine type info
  VariableIdTypeInfo sgn_type_info = getVariableIdTypeInfo(vid, vidm); 

  VarsInfo& def_vars_info = duvi.getDefVarsInfoMod();
  VarsInfo& use_vars_info = duvi.getUseVarsInfoMod();

  if(isModExpr) {
    def_vars_info.first.insert(VariableIdInfo(vid, sgn_type_info));
  }
  else {
    use_vars_info.first.insert(VariableIdInfo(vid, sgn_type_info));
  }
}

void ExprWalker::visit(SgVarRefExp* sgn)
{
  // get the VariableId
  VariableId vid = vidm.variableId(sgn);
  
  ROSE_ASSERT(vid.isValid());

  // determine type info
  VariableIdTypeInfo sgn_type_info = getVariableIdTypeInfo(vid, vidm); 

  VarsInfo& def_vars_info = duvi.getDefVarsInfoMod();
  VarsInfo& use_vars_info = duvi.getUseVarsInfoMod();

  if(vidm.getModeVariableIdForEachArrayElement() && sgn_type_info == arrayType) {
    // If found a reference to whole array, def/use all its elements.
    duvi.addAllArrayElements(SageInterface::convertRefToInitializedName(sgn), vidm, isModExpr);
  } else if(isModExpr) {
    def_vars_info.first.insert(VariableIdInfo(vid, sgn_type_info));
  } else {
    use_vars_info.first.insert(VariableIdInfo(vid, sgn_type_info));
  }
}

//.........这里部分代码省略.........
      SgExpression* falseBranch=condExp->get_false_exp();
      list<SingleEvalResultConstInt> falseBranchResultList=evalConstInt(falseBranch,estate,useConstraints,safeConstraintPropagation);
      return falseBranchResultList;
    }
    // dummy return value to avoid compiler warning
    cerr<<"Error: evaluating conditional operator inside expressions - unknown behavior (condition may have evaluated to bot)."<<endl;
    exit(1);
    return resultList;
  }
  if(dynamic_cast<SgBinaryOp*>(node)) {
    //cout << "BinaryOp:"<<SgNodeHelper::nodeToString(node)<<endl;

    SgNode* lhs=SgNodeHelper::getLhs(node);
    list<SingleEvalResultConstInt> lhsResultList=evalConstInt(lhs,estate,useConstraints,safeConstraintPropagation);
    SgNode* rhs=SgNodeHelper::getRhs(node);
    list<SingleEvalResultConstInt> rhsResultList=evalConstInt(rhs,estate,useConstraints,safeConstraintPropagation);
    //assert(lhsResultList.size()==1);
    //assert(rhsResultList.size()==1);
    list<SingleEvalResultConstInt> resultList;
    for(list<SingleEvalResultConstInt>::iterator liter=lhsResultList.begin();
        liter!=lhsResultList.end();
        ++liter) {
      for(list<SingleEvalResultConstInt>::iterator riter=rhsResultList.begin();
          riter!=rhsResultList.end();
          ++riter) {
        SingleEvalResultConstInt lhsResult=*liter;
        SingleEvalResultConstInt rhsResult=*riter;

        switch(node->variantT()) {
        case V_SgEqualityOp: {
          res.result=(lhsResult.result==rhsResult.result);
          res.exprConstraints=lhsResult.exprConstraints+rhsResult.exprConstraints;
          // record new constraint
          VariableId varId;
          if(variable(lhs,varId) && rhsResult.isConstInt()) {
            // if var is top add two states with opposing constraints
            if(!res.estate.pstate()->varIsConst(varId)) {
              SingleEvalResultConstInt tmpres1=res;
              SingleEvalResultConstInt tmpres2=res;
              tmpres1.exprConstraints.addConstraint(Constraint(Constraint::EQ_VAR_CONST,varId,rhsResult.value()));
              tmpres1.result=true;
              tmpres2.exprConstraints.addConstraint(Constraint(Constraint::NEQ_VAR_CONST,varId,rhsResult.value()));
              tmpres2.result=false;
              resultList.push_back(tmpres1);
              resultList.push_back(tmpres2);
              //return resultList; MS: removed 3/11/2014
              break;
            }
          }
          if(lhsResult.isConstInt() && variable(rhs,varId)) {
            // only add the equality constraint if no constant is bound to the respective variable
            if(!res.estate.pstate()->varIsConst(varId)) {
              SingleEvalResultConstInt tmpres1=res;
              SingleEvalResultConstInt tmpres2=res;
              tmpres1.exprConstraints.addConstraint(Constraint(Constraint::EQ_VAR_CONST,varId,lhsResult.value()));
              tmpres1.result=true;
              tmpres2.exprConstraints.addConstraint(Constraint(Constraint::NEQ_VAR_CONST,varId,lhsResult.value()));
              tmpres2.result=false;
              resultList.push_back(tmpres1);
              resultList.push_back(tmpres2);
              break;
            }
          }
          resultList.push_back(res);
          break;
        }

/*! 
  * \author Markus Schordan
  * \date 2012.
 */
size_t SPRAY::hash_value(const VariableId& vid) {
  return vid.getIdCode();
}

/*! 
  * \author Markus Schordan
  * \date 2012.
 */
void VariableIdMapping::generateStmtSymbolDotEdge(std::ofstream& file, SgNode* node,VariableId id) {
  file<<"_"<<node<<" "
      <<"->"
      <<id.toString()
      << endl;
}

/*! 
  * \author Markus Schordan
  * \date 2012.
 */
VariableId VariableIdMapping::variableIdFromCode(int i) {
  VariableId id;
  id.setIdCode(i);
  return id;
}