//== NullDerefChecker.cpp - Null dereference checker ------------*- C++ -*--==//
//
//                     The LLVM Compiler Infrastructure
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
//
// This defines NullDerefChecker, a builtin check in GRExprEngine that performs
// checks for null pointers at loads and stores.
//
//===----------------------------------------------------------------------===//

#include "clang/Analysis/PathSensitive/Checkers/DereferenceChecker.h"
#include "clang/Analysis/PathSensitive/GRExprEngine.h"
#include "clang/Analysis/PathSensitive/BugReporter.h"

using namespace clang;

void *NullDerefChecker::getTag() {
  static int x = 0;
  return &x;
}

ExplodedNode *NullDerefChecker::CheckLocation(const Stmt *S, ExplodedNode *Pred,
                                              const GRState *state, SVal V,
                                              GRExprEngine &Eng) {
  Loc *LV = dyn_cast<Loc>(&V);
  
    // If the value is not a location, don't touch the node.
  if (!LV)
    return Pred;
  
  const GRState *NotNullState = state->Assume(*LV, true);
  const GRState *NullState = state->Assume(*LV, false);
  
  GRStmtNodeBuilder &Builder = Eng.getBuilder();
  BugReporter &BR = Eng.getBugReporter();
  
    // The explicit NULL case.
  if (NullState) {
      // Use the GDM to mark in the state what lval was null.
    const SVal *PersistentLV = Eng.getBasicVals().getPersistentSVal(*LV);
    NullState = NullState->set<GRState::NullDerefTag>(PersistentLV);
    
    ExplodedNode *N = Builder.generateNode(S, NullState, Pred,
                                         ProgramPoint::PostNullCheckFailedKind);
    if (N) {
      N->markAsSink();
      
      if (!NotNullState) { // Explicit null case.
        if (!BT)
          BT = new BuiltinBug(NULL, "Null dereference",
                              "Dereference of null pointer");

        EnhancedBugReport *R =
          new EnhancedBugReport(*BT, BT->getDescription().c_str(), N);
        
        R->addVisitorCreator(bugreporter::registerTrackNullOrUndefValue,
                             bugreporter::GetDerefExpr(N));
        
        BR.EmitReport(R);
        
        return 0;
      } else // Implicit null case.
        ImplicitNullDerefNodes.push_back(N);
    }
  }
  
  if (!NotNullState)
    return 0;

  return Builder.generateNode(S, NotNullState, Pred, 
                              ProgramPoint::PostLocationChecksSucceedKind);
}


void *UndefDerefChecker::getTag() {
  static int x = 0;
  return &x;
}

ExplodedNode *UndefDerefChecker::CheckLocation(const Stmt *S, 
                                               ExplodedNode *Pred,
                                               const GRState *state, SVal V,
                                               GRExprEngine &Eng) {
  GRStmtNodeBuilder &Builder = Eng.getBuilder();
  BugReporter &BR = Eng.getBugReporter();

  if (V.isUndef()) {
    ExplodedNode *N = Builder.generateNode(S, state, Pred, 
                               ProgramPoint::PostUndefLocationCheckFailedKind);
    if (N) {
      N->markAsSink();

      if (!BT)
        BT = new BuiltinBug(0, "Undefined dereference", 
                            "Dereference of undefined pointer value");

      EnhancedBugReport *R =
        new EnhancedBugReport(*BT, BT->getDescription().c_str(), N);
      R->addVisitorCreator(bugreporter::registerTrackNullOrUndefValue,
                           bugreporter::GetDerefExpr(N));
      BR.EmitReport(R);
    }
    return 0;
  }

  return Pred;
}