GRExprEngine.cpp

//===----------------------------------------------------------------------===//
// Transfer functions: Miscellaneous statements.
//===----------------------------------------------------------------------===//

void GRExprEngine::VisitCast(Expr* CastE, Expr* Ex, NodeTy* Pred, NodeSet& Dst){
  
  NodeSet S1;
  QualType T = CastE->getType();
  
  if (T->isReferenceType())
    VisitLVal(Ex, Pred, S1);
  else
    Visit(Ex, Pred, S1);
  
  // Check for redundant casts or casting to "void"
  if (T->isVoidType() ||
      Ex->getType() == T || 
      (T->isPointerType() && Ex->getType()->isFunctionType())) {
    
    for (NodeSet::iterator I1 = S1.begin(), E1 = S1.end(); I1 != E1; ++I1)
      Dst.Add(*I1);

    return;
  }
  
  for (NodeSet::iterator I1 = S1.begin(), E1 = S1.end(); I1 != E1; ++I1) {
    NodeTy* N = *I1;
    ValueState* St = GetState(N);
    
    RVal V = T->isReferenceType() ? GetLVal(St, Ex) : GetRVal(St, Ex);
    
    MakeNode(Dst, CastE, N, SetRVal(St, CastE, EvalCast(V, CastE->getType())));
  }
}

void GRExprEngine::VisitDeclStmt(DeclStmt* DS, GRExprEngine::NodeTy* Pred,
                                 GRExprEngine::NodeSet& Dst) {
  
  ValueState* St = GetState(Pred);
  
  for (const ScopedDecl* D = DS->getDecl(); D; D = D->getNextDeclarator())
    if (const VarDecl* VD = dyn_cast<VarDecl>(D)) {
      
      // FIXME: Add support for local arrays.
      if (VD->getType()->isArrayType())
        continue;
      
      const Expr* Ex = VD->getInit();
      
      if (!VD->hasGlobalStorage() || VD->getStorageClass() == VarDecl::Static) {
        
        // In this context, Static => Local variable.
        
        assert (!VD->getStorageClass() == VarDecl::Static ||
                !VD->isFileVarDecl());
        
        // If there is no initializer, set the value of the
        // variable to "Undefined".
        //
        // FIXME: static variables may have an initializer, but the second
        //  time a function is called those values may not be current.

        QualType T = VD->getType();
        
        if ( VD->getStorageClass() == VarDecl::Static) {
          
          // C99: 6.7.8 Initialization
          //  If an object that has static storage duration is not initialized
          //  explicitly, then: 
          //   —if it has pointer type, it is initialized to a null pointer; 
          //   —if it has arithmetic type, it is initialized to (positive or 
          //     unsigned) zero; 
          
          // FIXME: Handle structs.  Now we treat their values as unknown.
          
          if (T->isPointerType()) {
            
            St = SetRVal(St, lval::DeclVal(VD),
                         lval::ConcreteInt(BasicVals.getValue(0, T)));
          }
          else if (T->isIntegerType()) {
            
            St = SetRVal(St, lval::DeclVal(VD),
                         nonlval::ConcreteInt(BasicVals.getValue(0, T)));
          }
          

        }
        else {
          
          // FIXME: Handle structs.  Now we treat them as unknown.  What
          //  we need to do is treat their members as unknown.
          
          if (T->isPointerType() || T->isIntegerType())
            St = SetRVal(St, lval::DeclVal(VD),
                         Ex ? GetRVal(St, Ex) : UndefinedVal());
        }
      }
    }

  MakeNode(Dst, DS, Pred, St);
}



/// VisitSizeOfAlignOfTypeExpr - Transfer function for sizeof(type).
void GRExprEngine::VisitSizeOfAlignOfTypeExpr(SizeOfAlignOfTypeExpr* Ex,
                                              NodeTy* Pred,
                                              NodeSet& Dst) {

  QualType T = Ex->getArgumentType();
  uint64_t amt;  
  
  if (Ex->isSizeOf()) {

    // FIXME: Add support for VLAs.
    if (!T.getTypePtr()->isConstantSizeType())
      return;
    
    amt = 1;  // Handle sizeof(void)
    
    if (T != getContext().VoidTy)
      amt = getContext().getTypeSize(T) / 8;
    
  }
  else  // Get alignment of the type.
    amt = getContext().getTypeAlign(T) / 8;
  
  MakeNode(Dst, Ex, Pred,
         SetRVal(GetState(Pred), Ex,
                 NonLVal::MakeVal(BasicVals, amt, Ex->getType())));  
}

void GRExprEngine::VisitDeref(UnaryOperator* U, NodeTy* Pred,
                              NodeSet& Dst, bool GetLVal) {

  Expr* Ex = U->getSubExpr()->IgnoreParens();
    
  NodeSet DstTmp;
  
  if (isa<DeclRefExpr>(Ex))
    DstTmp.Add(Pred);
  else
    Visit(Ex, Pred, DstTmp);
  
  for (NodeSet::iterator I = DstTmp.begin(), DE = DstTmp.end(); I != DE; ++I) {

    NodeTy* N = *I;
    ValueState* St = GetState(N);
    
    // FIXME: Bifurcate when dereferencing a symbolic with no constraints?
    
    RVal V = GetRVal(St, Ex);
    
    // Check for dereferences of undefined values.
    
    if (V.isUndef()) {
      
      NodeTy* Succ = Builder->generateNode(U, St, N);
      
      if (Succ) {
        Succ->markAsSink();
        UndefDeref.insert(Succ);
      }
      
      continue;
    }
    
    // Check for dereferences of unknown values.  Treat as No-Ops.
    
    if (V.isUnknown()) {
      Dst.Add(N);
      continue;
    }
    
    // After a dereference, one of two possible situations arise:
    //  (1) A crash, because the pointer was NULL.
    //  (2) The pointer is not NULL, and the dereference works.
    // 
    // We add these assumptions.
    
    LVal LV = cast<LVal>(V);    
    bool isFeasibleNotNull;
    
    // "Assume" that the pointer is Not-NULL.
    
    ValueState* StNotNull = Assume(St, LV, true, isFeasibleNotNull);
    
    if (isFeasibleNotNull) {

      if (GetLVal) MakeNode(Dst, U, N, SetRVal(StNotNull, U, LV));
      else {
        
        // FIXME: Currently symbolic analysis "generates" new symbols
        //  for the contents of values.  We need a better approach.
      
        MakeNode(Dst, U, N, SetRVal(StNotNull, U,
                                  GetRVal(StNotNull, LV, U->getType())));
      }
    }
    
    bool isFeasibleNull;
    
    // Now "assume" that the pointer is NULL.
    
    ValueState* StNull = Assume(St, LV, false, isFeasibleNull);
    
    if (isFeasibleNull) {
      
      // We don't use "MakeNode" here because the node will be a sink
      // and we have no intention of processing it later.

      NodeTy* NullNode = Builder->generateNode(U, StNull, N);
      
      if (NullNode) {

        NullNode->markAsSink();
        
        if (isFeasibleNotNull) ImplicitNullDeref.insert(NullNode);
        else ExplicitNullDeref.insert(NullNode);
      }
    }    
  }
}

void GRExprEngine::VisitUnaryOperator(UnaryOperator* U, NodeTy* Pred,
                                      NodeSet& Dst) {
  
  NodeSet S1;
  
  assert (U->getOpcode() != UnaryOperator::Deref);
  assert (U->getOpcode() != UnaryOperator::SizeOf);
  assert (U->getOpcode() != UnaryOperator::AlignOf);
  
  bool use_GetLVal = false;
  
  switch (U->getOpcode()) {
    case UnaryOperator::PostInc:
    case UnaryOperator::PostDec:
    case UnaryOperator::PreInc:
    case UnaryOperator::PreDec:
    case UnaryOperator::AddrOf:
      // Evalue subexpression as an LVal.
      use_GetLVal = true;
      VisitLVal(U->getSubExpr(), Pred, S1);
      break;
      
    default:
      Visit(U->getSubExpr(), Pred, S1);
      break;
  }

  for (NodeSet::iterator I1 = S1.begin(), E1 = S1.end(); I1 != E1; ++I1) {

    NodeTy* N1 = *I1;
    ValueState* St = GetState(N1);
        
    RVal SubV = use_GetLVal ? GetLVal(St, U->getSubExpr()) : 
                              GetRVal(St, U->getSubExpr());
    
    if (SubV.isUnknown()) {
      Dst.Add(N1);
      continue;
    }

    if (SubV.isUndef()) {
      MakeNode(Dst, U, N1, SetRVal(St, U, SubV));
      continue;
    }
    
    if (U->isIncrementDecrementOp()) {
      
      // Handle ++ and -- (both pre- and post-increment).
      
      LVal SubLV = cast<LVal>(SubV); 
      RVal V  = GetRVal(St, SubLV, U->getType());
      
      if (V.isUnknown()) {
        Dst.Add(N1);
        continue;
      }

      // Propagate undefined values.      
      if (V.isUndef()) {
        MakeNode(Dst, U, N1, SetRVal(St, U, V));
        continue;
      }
      
      // Handle all other values.
      
      BinaryOperator::Opcode Op = U->isIncrementOp() ? BinaryOperator::Add
                                                     : BinaryOperator::Sub;
      
      RVal Result = EvalBinOp(Op, V, MakeConstantVal(1U, U));
      
      if (U->isPostfix())
        St = SetRVal(SetRVal(St, U, V), SubLV, Result);
      else
        St = SetRVal(SetRVal(St, U, Result), SubLV, Result);
        
      MakeNode(Dst, U, N1, St);
      continue;
    }    
    
    // Handle all other unary operators.
    
    switch (U->getOpcode()) {
        
      case UnaryOperator::Extension:
        St = SetRVal(St, U, SubV);
        break;

      case UnaryOperator::Minus:
        St = SetRVal(St, U, EvalMinus(U, cast<NonLVal>(SubV)));
        break;
        
      case UnaryOperator::Not:
        St = SetRVal(St, U, EvalComplement(cast<NonLVal>(SubV)));
        break;
        
      case UnaryOperator::LNot:   
        
        // C99 6.5.3.3: "The expression !E is equivalent to (0==E)."
        //
        //  Note: technically we do "E == 0", but this is the same in the
        //    transfer functions as "0 == E".

        if (isa<LVal>(SubV)) {
          lval::ConcreteInt V(BasicVals.getZeroWithPtrWidth());
          RVal Result = EvalBinOp(BinaryOperator::EQ, cast<LVal>(SubV), V);
          St = SetRVal(St, U, Result);
        }
        else {
          Expr* Ex = U->getSubExpr();
          nonlval::ConcreteInt V(BasicVals.getValue(0, Ex->getType()));
          RVal Result = EvalBinOp(BinaryOperator::EQ, cast<NonLVal>(SubV), V);
          St = SetRVal(St, U, Result);
        }
        
        break;
        
      case UnaryOperator::AddrOf: {
        assert (isa<LVal>(SubV));
        St = SetRVal(St, U, SubV);
        break;
      }
                
      default: ;
        assert (false && "Not implemented.");
    } 
    
    MakeNode(Dst, U, N1, St);
  }
}

void GRExprEngine::VisitSizeOfExpr(UnaryOperator* U, NodeTy* Pred,
                                   NodeSet& Dst) {
  
  QualType T = U->getSubExpr()->getType();
  
  // FIXME: Add support for VLAs.
  if (!T.getTypePtr()->isConstantSizeType())
    return;
  
  uint64_t size = getContext().getTypeSize(T) / 8;                
  ValueState* St = GetState(Pred);
  St = SetRVal(St, U, NonLVal::MakeVal(BasicVals, size, U->getType()));

  MakeNode(Dst, U, Pred, St);
}

void GRExprEngine::VisitLVal(Expr* Ex, NodeTy* Pred, NodeSet& Dst) {

  if (Ex != CurrentStmt && getCFG().isBlkExpr(Ex)) {
    Dst.Add(Pred);
    return;
  }
  
  Ex = Ex->IgnoreParens();
  
  if (isa<DeclRefExpr>(Ex)) {
    Dst.Add(Pred);
    return;
  }
  
  if (UnaryOperator* U = dyn_cast<UnaryOperator>(Ex))
    if (U->getOpcode() == UnaryOperator::Deref) {
      VisitDeref(U, Pred, Dst, true);
      return;
    }
  
  Visit(Ex, Pred, Dst);
}

void GRExprEngine::VisitAsmStmt(AsmStmt* A, NodeTy* Pred, NodeSet& Dst) {
  VisitAsmStmtHelperOutputs(A, A->begin_outputs(), A->end_outputs(), Pred, Dst);
}  

void GRExprEngine::VisitAsmStmtHelperOutputs(AsmStmt* A,
                                             AsmStmt::outputs_iterator I,
                                             AsmStmt::outputs_iterator E,
                                             NodeTy* Pred, NodeSet& Dst) {
  if (I == E) {
    VisitAsmStmtHelperInputs(A, A->begin_inputs(), A->end_inputs(), Pred, Dst);
    return;
  }
  
  NodeSet Tmp;
  VisitLVal(*I, Pred, Tmp);
  
  ++I;
  
  for (NodeSet::iterator NI = Tmp.begin(), NE = Tmp.end(); NI != NE; ++NI)
    VisitAsmStmtHelperOutputs(A, I, E, *NI, Dst);
}

void GRExprEngine::VisitAsmStmtHelperInputs(AsmStmt* A,
                                            AsmStmt::inputs_iterator I,
                                            AsmStmt::inputs_iterator E,
                                            NodeTy* Pred, NodeSet& Dst) {
  if (I == E) {
    
    // We have processed both the inputs and the outputs.  All of the outputs
    // should evaluate to LVals.  Nuke all of their values.
    
    // FIXME: Some day in the future it would be nice to allow a "plug-in"
    // which interprets the inline asm and stores proper results in the
    // outputs.
    
    ValueState* St = GetState(Pred);
    
    for (AsmStmt::outputs_iterator OI = A->begin_outputs(),
                                   OE = A->end_outputs(); OI != OE; ++OI) {
      
      RVal X = GetLVal(St, *OI);
      
      assert (!isa<NonLVal>(X));
      
      if (isa<LVal>(X))
        St = SetRVal(St, cast<LVal>(X), UnknownVal());
    }
    
    MakeNode(Dst, A, Pred, St);
    return;
  }
  
  NodeSet Tmp;
  Visit(*I, Pred, Tmp);
  
  ++I;
  
  for (NodeSet::iterator NI = Tmp.begin(), NE = Tmp.end(); NI != NE; ++NI)
    VisitAsmStmtHelperInputs(A, I, E, *NI, Dst);
}

void GRExprEngine::VisitReturnStmt(ReturnStmt* S, NodeTy* Pred, NodeSet& Dst) {

  Expr* R = S->getRetValue();
  
  if (!R) {
    Dst.Add(Pred);
    return;
  }
  
  QualType T = R->getType();
  
  if (T->isPointerLikeType()) {
    
    // Check if any of the return values return the address of a stack variable.
    
    NodeSet Tmp;
    Visit(R, Pred, Tmp);
    
    for (NodeSet::iterator I=Tmp.begin(), E=Tmp.end(); I!=E; ++I) {
      RVal X = GetRVal((*I)->getState(), R);

      if (isa<lval::DeclVal>(X)) {
        
        if (cast<lval::DeclVal>(X).getDecl()->hasLocalStorage()) {
        
          // Create a special node representing the v
          
          NodeTy* RetStackNode = Builder->generateNode(S, GetState(*I), *I);
          
          if (RetStackNode) {
            RetStackNode->markAsSink();
            RetsStackAddr.insert(RetStackNode);
          }
          
          continue;
        }
      }
      
      Dst.Add(*I);
    }
  }
  else
    Visit(R, Pred, Dst);
}

//===----------------------------------------------------------------------===//
// Transfer functions: Binary operators.
//===----------------------------------------------------------------------===//

void GRExprEngine::VisitBinaryOperator(BinaryOperator* B,
                                       GRExprEngine::NodeTy* Pred,
                                       GRExprEngine::NodeSet& Dst) {
  NodeSet S1;
  
  if (B->isAssignmentOp())
    VisitLVal(B->getLHS(), Pred, S1);
  else
    Visit(B->getLHS(), Pred, S1);

  for (NodeSet::iterator I1=S1.begin(), E1=S1.end(); I1 != E1; ++I1) {

    NodeTy* N1 = *I1;
    
    // When getting the value for the LHS, check if we are in an assignment.
    // In such cases, we want to (initially) treat the LHS as an LVal,
    // so we use GetLVal instead of GetRVal so that DeclRefExpr's are
    // evaluated to LValDecl's instead of to an NonLVal.

    RVal LeftV = B->isAssignmentOp() ? GetLVal(GetState(N1), B->getLHS())
                                     : GetRVal(GetState(N1), B->getLHS());
    
    // Visit the RHS...
    
    NodeSet S2;    
    Visit(B->getRHS(), N1, S2);
    
    // Process the binary operator.
  
    for (NodeSet::iterator I2 = S2.begin(), E2 = S2.end(); I2 != E2; ++I2) {

      NodeTy* N2 = *I2;
      ValueState* St = GetState(N2);
      Expr* RHS = B->getRHS();
      RVal RightV = GetRVal(St, RHS);

      BinaryOperator::Opcode Op = B->getOpcode();
      
      if ((Op == BinaryOperator::Div || Op == BinaryOperator::Rem)
          && RHS->getType()->isIntegerType()) {

        // Check if the denominator is undefined.
        
        if (!RightV.isUnknown()) {
        
          if (RightV.isUndef()) {
            NodeTy* DivUndef = Builder->generateNode(B, St, N2);
            
            if (DivUndef) {
              DivUndef->markAsSink();
              ExplicitBadDivides.insert(DivUndef);
            }
            
            continue;
          }
            
          // Check for divide/remainder-by-zero.
          //
          // First, "assume" that the denominator is 0 or undefined.
          
          bool isFeasibleZero = false;
          ValueState* ZeroSt =  Assume(St, RightV, false, isFeasibleZero);
          
          // Second, "assume" that the denominator cannot be 0.
          
          bool isFeasibleNotZero = false;
          St = Assume(St, RightV, true, isFeasibleNotZero);
          
          // Create the node for the divide-by-zero (if it occurred).
          
          if (isFeasibleZero)
            if (NodeTy* DivZeroNode = Builder->generateNode(B, ZeroSt, N2)) {
              DivZeroNode->markAsSink();
              
              if (isFeasibleNotZero)
                ImplicitBadDivides.insert(DivZeroNode);
              else
                ExplicitBadDivides.insert(DivZeroNode);

            }
          
          if (!isFeasibleNotZero)
            continue;
        }
        
        // Fall-through.  The logic below processes the divide.
      }
      
      
      if (Op <= BinaryOperator::Or) {
        
        // Process non-assignements except commas or short-circuited
        // logical expressions (LAnd and LOr).
        
        RVal Result = EvalBinOp(Op, LeftV, RightV);
        
        if (Result.isUnknown()) {
          Dst.Add(N2);
          continue;
        }
        
        if (Result.isUndef() && !LeftV.isUndef() && !RightV.isUndef()) {
          
          // The operands were not undefined, but the result is undefined.
          
          if (NodeTy* UndefNode = Builder->generateNode(B, St, N2)) {
            UndefNode->markAsSink();            
            UndefResults.insert(UndefNode);
          }
          
          continue;
        }
        
        MakeNode(Dst, B, N2, SetRVal(St, B, Result));
        continue;
      }
        
      // Process assignments.
    
      switch (Op) {        
          
        case BinaryOperator::Assign: {
          
          // Simple assignments.

          if (LeftV.isUndef()) {
            HandleUndefinedStore(B, N2);
            continue;
          }
          
          // EXPERIMENTAL: "Conjured" symbols.
          
          if (RightV.isUnknown()) {            
            unsigned Count = Builder->getCurrentBlockCount();
            SymbolID Sym = SymMgr.getConjuredSymbol(B->getRHS(), Count);
            
            RightV = B->getRHS()->getType()->isPointerType() 
                     ? cast<RVal>(lval::SymbolVal(Sym)) 
                     : cast<RVal>(nonlval::SymbolVal(Sym));            
          }
          
          // Even if the LHS evaluates to an unknown L-Value, the entire
          // expression still evaluates to the RHS.
          
          if (LeftV.isUnknown()) {
            St = SetRVal(St, B, RightV);
            break;
          }
          
          // Simulate the effects of a "store":  bind the value of the RHS
          // to the L-Value represented by the LHS.

          VisitStore(Dst, B, N2, SetRVal(St, B, RightV),
                    cast<LVal>(LeftV), RightV);
          
//          St = SetRVal(SetRVal(St, B, RightV), cast<LVal>(LeftV), RightV);
          continue;
        }

          // Compound assignment operators.
          
        default: { 
          
          assert (B->isCompoundAssignmentOp());
          
          if (Op >= BinaryOperator::AndAssign)
            ((int&) Op) -= (BinaryOperator::AndAssign - BinaryOperator::And);
          else
            ((int&) Op) -= BinaryOperator::MulAssign;  
          
          // Check if the LHS is undefined.
          
          if (LeftV.isUndef()) {
            HandleUndefinedStore(B, N2);
            continue;
          }
          
          if (LeftV.isUnknown()) {
            assert (isa<UnknownVal>(GetRVal(St, B)));
            Dst.Add(N2);
            continue;
          }
          
          // At this pointer we know that the LHS evaluates to an LVal
          // that is neither "Unknown" or "Undefined."
          
          LVal LeftLV = cast<LVal>(LeftV);
          
          // Fetch the value of the LHS (the value of the variable, etc.).
          
          RVal V = GetRVal(GetState(N1), LeftLV, B->getLHS()->getType());
          
          // Propagate undefined value (left-side).  We
          // propogate undefined values for the RHS below when
          // we also check for divide-by-zero.
          
          if (V.isUndef()) {
            St = SetRVal(St, B, V);
            break;
          }
          
          // Propagate unknown values.
          
          if (V.isUnknown()) {
            // The value bound to LeftV is unknown.  Thus we just
            // propagate the current node (as "B" is already bound to nothing).
            assert (isa<UnknownVal>(GetRVal(St, B)));
            Dst.Add(N2);
            continue;
          }
          
          if (RightV.isUnknown()) {
            assert (isa<UnknownVal>(GetRVal(St, B)));
            St = SetRVal(St, LeftLV, UnknownVal());
            break;
          }
            
          // At this point:
          //
          //  The LHS is not Undef/Unknown.
          //  The RHS is not Unknown.
          
          // Get the computation type.
          QualType CTy = cast<CompoundAssignOperator>(B)->getComputationType();
          
          // Perform promotions.
          V = EvalCast(V, CTy);
          RightV = EvalCast(RightV, CTy);
          
          // Evaluate operands and promote to result type.

          if ((Op == BinaryOperator::Div || Op == BinaryOperator::Rem)
              && RHS->getType()->isIntegerType()) {
            
            // Check if the denominator is undefined.
                
            if (RightV.isUndef()) {
              NodeTy* DivUndef = Builder->generateNode(B, St, N2);
              
              if (DivUndef) {
                DivUndef->markAsSink();
                ExplicitBadDivides.insert(DivUndef);
              }
              
              continue;
            }

            // First, "assume" that the denominator is 0.
            
            bool isFeasibleZero = false;
            ValueState* ZeroSt = Assume(St, RightV, false, isFeasibleZero);
            
            // Second, "assume" that the denominator cannot be 0.
            
            bool isFeasibleNotZero = false;
            St = Assume(St, RightV, true, isFeasibleNotZero);
            
            // Create the node for the divide-by-zero error (if it occurred).
            
            if (isFeasibleZero) {
              NodeTy* DivZeroNode = Builder->generateNode(B, ZeroSt, N2);
              
              if (DivZeroNode) {
                DivZeroNode->markAsSink();
                
                if (isFeasibleNotZero)
                  ImplicitBadDivides.insert(DivZeroNode);
                else
                  ExplicitBadDivides.insert(DivZeroNode);
              }
            }
            
            if (!isFeasibleNotZero)
              continue;
            
            // Fall-through.  The logic below processes the divide.
          }
          else {
            
            // Propagate undefined values (right-side).
            
            if (RightV.isUndef()) {
              St = SetRVal(SetRVal(St, B, RightV), LeftLV, RightV);
              break;
            }
            
          }

          RVal Result = EvalCast(EvalBinOp(Op, V, RightV), B->getType());
          
          if (Result.isUndef()) {
            
            // The operands were not undefined, but the result is undefined.
            
            if (NodeTy* UndefNode = Builder->generateNode(B, St, N2)) {
              UndefNode->markAsSink();            
              UndefResults.insert(UndefNode);
            }
            
            continue;
          }
          
          //          St = SetRVal(SetRVal(St, B, Result), LeftLV, Result);          
          VisitStore(Dst, B, N2, SetRVal(St, B, Result), LeftLV, Result);
          continue;
        }
      }
    
      MakeNode(Dst, B, N2, St);
    }
  }
}

void GRExprEngine::HandleUndefinedStore(Stmt* S, NodeTy* Pred) {  
  NodeTy* N = Builder->generateNode(S, GetState(Pred), Pred);
  N->markAsSink();
  UndefStores.insert(N);
}


//===----------------------------------------------------------------------===//
// "Assume" logic.
//===----------------------------------------------------------------------===//

ValueState* GRExprEngine::Assume(ValueState* St, LVal Cond,
                                           bool Assumption, 
                                           bool& isFeasible) {
  switch (Cond.getSubKind()) {
    default:
      assert (false && "'Assume' not implemented for this LVal.");
      return St;
      
    case lval::SymbolValKind:
      if (Assumption)
        return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
                           BasicVals.getZeroWithPtrWidth(), isFeasible);
      else
        return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
                           BasicVals.getZeroWithPtrWidth(), isFeasible);
      
      
    case lval::DeclValKind:
    case lval::FuncValKind:
    case lval::GotoLabelKind:
      isFeasible = Assumption;
      return St;

    case lval::ConcreteIntKind: {
      bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
      isFeasible = b ? Assumption : !Assumption;      
      return St;
    }
  }
}

ValueState* GRExprEngine::Assume(ValueState* St, NonLVal Cond,
                                         bool Assumption, 
                                         bool& isFeasible) {  
  switch (Cond.getSubKind()) {
    default:
      assert (false && "'Assume' not implemented for this NonLVal.");
      return St;
      
      
    case nonlval::SymbolValKind: {
      nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
      SymbolID sym = SV.getSymbol();
      
      if (Assumption)
        return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
                           isFeasible);
      else
        return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
                           isFeasible);
    }
      
    case nonlval::SymIntConstraintValKind:
      return
        AssumeSymInt(St, Assumption,
                     cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
                     isFeasible);
      
    case nonlval::ConcreteIntKind: {
      bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
      isFeasible = b ? Assumption : !Assumption;      
      return St;
    }
  }
}

ValueState*
GRExprEngine::AssumeSymNE(ValueState* St, SymbolID sym,
                         const llvm::APSInt& V, bool& isFeasible) {
  
  // First, determine if sym == X, where X != V.
  if (const llvm::APSInt* X = St->getSymVal(sym)) {
    isFeasible = *X != V;
    return St;
  }
  
  // Second, determine if sym != V.
  if (St->isNotEqual(sym, V)) {
    isFeasible = true;
    return St;
  }
      
  // If we reach here, sym is not a constant and we don't know if it is != V.
  // Make that assumption.
  
  isFeasible = true;
  return StateMgr.AddNE(St, sym, V);
}

ValueState*
GRExprEngine::AssumeSymEQ(ValueState* St, SymbolID sym,
                         const llvm::APSInt& V, bool& isFeasible) {
  
  // First, determine if sym == X, where X != V.
  if (const llvm::APSInt* X = St->getSymVal(sym)) {
    isFeasible = *X == V;
    return St;
  }
  
  // Second, determine if sym != V.
  if (St->isNotEqual(sym, V)) {
    isFeasible = false;
    return St;
  }
  
  // If we reach here, sym is not a constant and we don't know if it is == V.
  // Make that assumption.
  
  isFeasible = true;
  return StateMgr.AddEQ(St, sym, V);
}

ValueState*
GRExprEngine::AssumeSymInt(ValueState* St, bool Assumption,
                          const SymIntConstraint& C, bool& isFeasible) {
  
  switch (C.getOpcode()) {
    default:
      // No logic yet for other operators.
      isFeasible = true;
      return St;
      
    case BinaryOperator::EQ:
      if (Assumption)
        return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
      else
        return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
      
    case BinaryOperator::NE:
      if (Assumption)
        return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
      else
        return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
  }
}

//===----------------------------------------------------------------------===//
// Visualization.
//===----------------------------------------------------------------------===//

#ifndef NDEBUG
static GRExprEngine* GraphPrintCheckerState;
static SourceManager* GraphPrintSourceManager;
static ValueState::CheckerStatePrinter* GraphCheckerStatePrinter;

namespace llvm {
template<>
struct VISIBILITY_HIDDEN DOTGraphTraits<GRExprEngine::NodeTy*> :
  public DefaultDOTGraphTraits {
    
  static void PrintVarBindings(std::ostream& Out, ValueState* St) {

    Out << "Variables:\\l";
    
    bool isFirst = true;
    
    for (ValueState::vb_iterator I=St->vb_begin(), E=St->vb_end(); I!=E;++I) {        

      if (isFirst)
        isFirst = false;
      else
        Out << "\\l";
      
      Out << ' ' << I.getKey()->getName() << " : ";
      I.getData().print(Out);
    }
    
  }
    
    
  static void PrintSubExprBindings(std::ostream& Out, ValueState* St){