head	1.1;
branch	1.1.1;
access;
symbols
	netbsd-11-0-RC4:1.1.1.5
	netbsd-11-0-RC3:1.1.1.5
	netbsd-11-0-RC2:1.1.1.5
	netbsd-11-0-RC1:1.1.1.5
	perseant-exfatfs-base-20250801:1.1.1.5
	netbsd-11:1.1.1.5.0.10
	netbsd-11-base:1.1.1.5
	netbsd-10-1-RELEASE:1.1.1.5
	perseant-exfatfs-base-20240630:1.1.1.5
	perseant-exfatfs:1.1.1.5.0.8
	perseant-exfatfs-base:1.1.1.5
	netbsd-8-3-RELEASE:1.1.1.4
	netbsd-9-4-RELEASE:1.1.1.4
	netbsd-10-0-RELEASE:1.1.1.5
	netbsd-10-0-RC6:1.1.1.5
	netbsd-10-0-RC5:1.1.1.5
	netbsd-10-0-RC4:1.1.1.5
	netbsd-10-0-RC3:1.1.1.5
	netbsd-10-0-RC2:1.1.1.5
	netbsd-10-0-RC1:1.1.1.5
	netbsd-10:1.1.1.5.0.6
	netbsd-10-base:1.1.1.5
	netbsd-9-3-RELEASE:1.1.1.4
	cjep_sun2x:1.1.1.5.0.4
	cjep_sun2x-base:1.1.1.5
	cjep_staticlib_x-base1:1.1.1.5
	netbsd-9-2-RELEASE:1.1.1.4
	cjep_staticlib_x:1.1.1.5.0.2
	cjep_staticlib_x-base:1.1.1.5
	netbsd-9-1-RELEASE:1.1.1.4
	phil-wifi-20200421:1.1.1.5
	phil-wifi-20200411:1.1.1.5
	phil-wifi-20200406:1.1.1.5
	netbsd-8-2-RELEASE:1.1.1.4
	netbsd-9-0-RELEASE:1.1.1.4
	netbsd-9-0-RC2:1.1.1.4
	netbsd-9-0-RC1:1.1.1.4
	netbsd-9:1.1.1.4.0.18
	netbsd-9-base:1.1.1.4
	phil-wifi-20190609:1.1.1.4
	netbsd-8-1-RELEASE:1.1.1.4
	netbsd-8-1-RC1:1.1.1.4
	pgoyette-compat-merge-20190127:1.1.1.4
	pgoyette-compat-20190127:1.1.1.4
	pgoyette-compat-20190118:1.1.1.4
	pgoyette-compat-1226:1.1.1.4
	pgoyette-compat-1126:1.1.1.4
	pgoyette-compat-1020:1.1.1.4
	pgoyette-compat-0930:1.1.1.4
	pgoyette-compat-0906:1.1.1.4
	netbsd-7-2-RELEASE:1.1.1.3
	pgoyette-compat-0728:1.1.1.4
	clang-337282:1.1.1.4
	netbsd-8-0-RELEASE:1.1.1.4
	phil-wifi:1.1.1.4.0.16
	phil-wifi-base:1.1.1.4
	pgoyette-compat-0625:1.1.1.4
	netbsd-8-0-RC2:1.1.1.4
	pgoyette-compat-0521:1.1.1.4
	pgoyette-compat-0502:1.1.1.4
	pgoyette-compat-0422:1.1.1.4
	netbsd-8-0-RC1:1.1.1.4
	pgoyette-compat-0415:1.1.1.4
	pgoyette-compat-0407:1.1.1.4
	pgoyette-compat-0330:1.1.1.4
	pgoyette-compat-0322:1.1.1.4
	pgoyette-compat-0315:1.1.1.4
	netbsd-7-1-2-RELEASE:1.1.1.3
	pgoyette-compat:1.1.1.4.0.14
	pgoyette-compat-base:1.1.1.4
	netbsd-7-1-1-RELEASE:1.1.1.3
	clang-319952:1.1.1.4
	matt-nb8-mediatek:1.1.1.4.0.12
	matt-nb8-mediatek-base:1.1.1.4
	clang-309604:1.1.1.4
	perseant-stdc-iso10646:1.1.1.4.0.10
	perseant-stdc-iso10646-base:1.1.1.4
	netbsd-8:1.1.1.4.0.8
	netbsd-8-base:1.1.1.4
	prg-localcount2-base3:1.1.1.4
	prg-localcount2-base2:1.1.1.4
	prg-localcount2-base1:1.1.1.4
	prg-localcount2:1.1.1.4.0.6
	prg-localcount2-base:1.1.1.4
	pgoyette-localcount-20170426:1.1.1.4
	bouyer-socketcan-base1:1.1.1.4
	pgoyette-localcount-20170320:1.1.1.4
	netbsd-7-1:1.1.1.3.0.10
	netbsd-7-1-RELEASE:1.1.1.3
	netbsd-7-1-RC2:1.1.1.3
	clang-294123:1.1.1.4
	netbsd-7-nhusb-base-20170116:1.1.1.3
	bouyer-socketcan:1.1.1.4.0.4
	bouyer-socketcan-base:1.1.1.4
	clang-291444:1.1.1.4
	pgoyette-localcount-20170107:1.1.1.4
	netbsd-7-1-RC1:1.1.1.3
	pgoyette-localcount-20161104:1.1.1.4
	netbsd-7-0-2-RELEASE:1.1.1.3
	localcount-20160914:1.1.1.4
	netbsd-7-nhusb:1.1.1.3.0.8
	netbsd-7-nhusb-base:1.1.1.3
	clang-280599:1.1.1.4
	pgoyette-localcount-20160806:1.1.1.4
	pgoyette-localcount-20160726:1.1.1.4
	pgoyette-localcount:1.1.1.4.0.2
	pgoyette-localcount-base:1.1.1.4
	netbsd-7-0-1-RELEASE:1.1.1.3
	clang-261930:1.1.1.4
	netbsd-7-0:1.1.1.3.0.6
	netbsd-7-0-RELEASE:1.1.1.3
	netbsd-7-0-RC3:1.1.1.3
	netbsd-7-0-RC2:1.1.1.3
	netbsd-7-0-RC1:1.1.1.3
	clang-237755:1.1.1.3
	clang-232565:1.1.1.3
	clang-227398:1.1.1.3
	tls-maxphys-base:1.1.1.3
	tls-maxphys:1.1.1.3.0.4
	netbsd-7:1.1.1.3.0.2
	netbsd-7-base:1.1.1.3
	clang-215315:1.1.1.3
	clang-209886:1.1.1.3
	yamt-pagecache:1.1.1.2.0.4
	yamt-pagecache-base9:1.1.1.2
	tls-earlyentropy:1.1.1.2.0.2
	tls-earlyentropy-base:1.1.1.3
	riastradh-xf86-video-intel-2-7-1-pre-2-21-15:1.1.1.2
	riastradh-drm2-base3:1.1.1.2
	clang-202566:1.1.1.2
	clang-201163:1.1.1.1
	clang-199312:1.1.1.1
	clang-198450:1.1.1.1
	clang-196603:1.1.1.1
	clang-195771:1.1.1.1
	LLVM:1.1.1;
locks; strict;
comment	@// @;


1.1
date	2013.11.28.14.14.52;	author joerg;	state Exp;
branches
	1.1.1.1;
next	;
commitid	ow8OybrawrB1f3fx;

1.1.1.1
date	2013.11.28.14.14.52;	author joerg;	state Exp;
branches;
next	1.1.1.2;
commitid	ow8OybrawrB1f3fx;

1.1.1.2
date	2014.03.04.19.55.00;	author joerg;	state Exp;
branches
	1.1.1.2.2.1
	1.1.1.2.4.1;
next	1.1.1.3;
commitid	29z1hJonZISIXprx;

1.1.1.3
date	2014.05.30.18.14.44;	author joerg;	state Exp;
branches
	1.1.1.3.4.1;
next	1.1.1.4;
commitid	8q0kdlBlCn09GACx;

1.1.1.4
date	2016.02.27.22.12.06;	author joerg;	state Exp;
branches
	1.1.1.4.16.1;
next	1.1.1.5;
commitid	tIimz3oDlh1NpBWy;

1.1.1.5
date	2019.11.13.22.19.28;	author joerg;	state dead;
branches;
next	;
commitid	QD8YATxuNG34YJKB;

1.1.1.2.2.1
date	2014.08.10.07.08.10;	author tls;	state Exp;
branches;
next	;
commitid	t01A1TLTYxkpGMLx;

1.1.1.2.4.1
date	2014.03.04.19.55.00;	author yamt;	state dead;
branches;
next	1.1.1.2.4.2;
commitid	WSrDtL5nYAUyiyBx;

1.1.1.2.4.2
date	2014.05.22.16.18.30;	author yamt;	state Exp;
branches;
next	;
commitid	WSrDtL5nYAUyiyBx;

1.1.1.3.4.1
date	2014.05.30.18.14.44;	author tls;	state dead;
branches;
next	1.1.1.3.4.2;
commitid	jTnpym9Qu0o4R1Nx;

1.1.1.3.4.2
date	2014.08.19.23.47.31;	author tls;	state Exp;
branches;
next	;
commitid	jTnpym9Qu0o4R1Nx;

1.1.1.4.16.1
date	2020.04.13.07.46.38;	author martin;	state dead;
branches;
next	;
commitid	X01YhRUPVUDaec4C;


desc
@@


1.1
log
@Initial revision
@
text
@//== BoolAssignmentChecker.cpp - Boolean assignment 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 BoolAssignmentChecker, a builtin check in ExprEngine that
// performs checks for assignment of non-Boolean values to Boolean variables.
//
//===----------------------------------------------------------------------===//

#include "ClangSACheckers.h"
#include "clang/StaticAnalyzer/Core/BugReporter/BugType.h"
#include "clang/StaticAnalyzer/Core/Checker.h"
#include "clang/StaticAnalyzer/Core/CheckerManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"

using namespace clang;
using namespace ento;

namespace {
  class BoolAssignmentChecker : public Checker< check::Bind > {
    mutable OwningPtr<BuiltinBug> BT;
    void emitReport(ProgramStateRef state, CheckerContext &C) const;
  public:
    void checkBind(SVal loc, SVal val, const Stmt *S, CheckerContext &C) const;
  };
} // end anonymous namespace

void BoolAssignmentChecker::emitReport(ProgramStateRef state,
                                       CheckerContext &C) const {
  if (ExplodedNode *N = C.addTransition(state)) {
    if (!BT)
      BT.reset(new BuiltinBug("Assignment of a non-Boolean value"));    
    C.emitReport(new BugReport(*BT, BT->getDescription(), N));
  }
}

static bool isBooleanType(QualType Ty) {
  if (Ty->isBooleanType()) // C++ or C99
    return true;
  
  if (const TypedefType *TT = Ty->getAs<TypedefType>())
    return TT->getDecl()->getName() == "BOOL"   || // Objective-C
           TT->getDecl()->getName() == "_Bool"  || // stdbool.h < C99
           TT->getDecl()->getName() == "Boolean";  // MacTypes.h
  
  return false;
}

void BoolAssignmentChecker::checkBind(SVal loc, SVal val, const Stmt *S,
                                      CheckerContext &C) const {
  
  // We are only interested in stores into Booleans.
  const TypedValueRegion *TR =
    dyn_cast_or_null<TypedValueRegion>(loc.getAsRegion());
  
  if (!TR)
    return;
  
  QualType valTy = TR->getValueType();
  
  if (!isBooleanType(valTy))
    return;
  
  // Get the value of the right-hand side.  We only care about values
  // that are defined (UnknownVals and UndefinedVals are handled by other
  // checkers).
  Optional<DefinedSVal> DV = val.getAs<DefinedSVal>();
  if (!DV)
    return;
    
  // Check if the assigned value meets our criteria for correctness.  It must
  // be a value that is either 0 or 1.  One way to check this is to see if
  // the value is possibly < 0 (for a negative value) or greater than 1.
  ProgramStateRef state = C.getState(); 
  SValBuilder &svalBuilder = C.getSValBuilder();
  ConstraintManager &CM = C.getConstraintManager();
  
  // First, ensure that the value is >= 0.  
  DefinedSVal zeroVal = svalBuilder.makeIntVal(0, valTy);
  SVal greaterThanOrEqualToZeroVal =
    svalBuilder.evalBinOp(state, BO_GE, *DV, zeroVal,
                          svalBuilder.getConditionType());

  Optional<DefinedSVal> greaterThanEqualToZero =
      greaterThanOrEqualToZeroVal.getAs<DefinedSVal>();

  if (!greaterThanEqualToZero) {
    // The SValBuilder cannot construct a valid SVal for this condition.
    // This means we cannot properly reason about it.    
    return;
  }
  
  ProgramStateRef stateLT, stateGE;
  llvm::tie(stateGE, stateLT) = CM.assumeDual(state, *greaterThanEqualToZero);
  
  // Is it possible for the value to be less than zero?
  if (stateLT) {
    // It is possible for the value to be less than zero.  We only
    // want to emit a warning, however, if that value is fully constrained.
    // If it it possible for the value to be >= 0, then essentially the
    // value is underconstrained and there is nothing left to be done.
    if (!stateGE)
      emitReport(stateLT, C);
    
    // In either case, we are done.
    return;
  }
  
  // If we reach here, it must be the case that the value is constrained
  // to only be >= 0.
  assert(stateGE == state);
  
  // At this point we know that the value is >= 0.
  // Now check to ensure that the value is <= 1.
  DefinedSVal OneVal = svalBuilder.makeIntVal(1, valTy);
  SVal lessThanEqToOneVal =
    svalBuilder.evalBinOp(state, BO_LE, *DV, OneVal,
                          svalBuilder.getConditionType());

  Optional<DefinedSVal> lessThanEqToOne =
      lessThanEqToOneVal.getAs<DefinedSVal>();

  if (!lessThanEqToOne) {
    // The SValBuilder cannot construct a valid SVal for this condition.
    // This means we cannot properly reason about it.    
    return;
  }
  
  ProgramStateRef stateGT, stateLE;
  llvm::tie(stateLE, stateGT) = CM.assumeDual(state, *lessThanEqToOne);
  
  // Is it possible for the value to be greater than one?
  if (stateGT) {
    // It is possible for the value to be greater than one.  We only
    // want to emit a warning, however, if that value is fully constrained.
    // If it is possible for the value to be <= 1, then essentially the
    // value is underconstrained and there is nothing left to be done.
    if (!stateLE)
      emitReport(stateGT, C);
    
    // In either case, we are done.
    return;
  }
  
  // If we reach here, it must be the case that the value is constrained
  // to only be <= 1.
  assert(stateLE == state);
}

void ento::registerBoolAssignmentChecker(CheckerManager &mgr) {
    mgr.registerChecker<BoolAssignmentChecker>();
}
@


1.1.1.1
log
@Import Clang 3.4rc1 r195771.
@
text
@@


1.1.1.2
log
@Import Clang 3.5svn r202566.
@
text
@d37 1
a37 1
      BT.reset(new BuiltinBug(this, "Assignment of a non-Boolean value"));
@


1.1.1.2.2.1
log
@Rebase.
@
text
@d26 1
a26 1
    mutable std::unique_ptr<BuiltinBug> BT;
d99 1
a99 1
  std::tie(stateGE, stateLT) = CM.assumeDual(state, *greaterThanEqualToZero);
d135 1
a135 1
  std::tie(stateLE, stateGT) = CM.assumeDual(state, *lessThanEqToOne);
@


1.1.1.3
log
@Import Clang 3.5svn r209886.
@
text
@d26 1
a26 1
    mutable std::unique_ptr<BuiltinBug> BT;
d99 1
a99 1
  std::tie(stateGE, stateLT) = CM.assumeDual(state, *greaterThanEqualToZero);
d135 1
a135 1
  std::tie(stateLE, stateGT) = CM.assumeDual(state, *lessThanEqToOne);
@


1.1.1.4
log
@Import Clang 3.8.0rc3 r261930.
@
text
@d35 1
a35 1
  if (ExplodedNode *N = C.generateNonFatalErrorNode(state)) {
d38 1
a38 1
    C.emitReport(llvm::make_unique<BugReport>(*BT, BT->getDescription(), N));
d45 1
a45 1

d50 1
a50 1

d56 1
a56 1

d60 1
a60 1

d63 1
a63 1

d65 1
a65 1

d68 1
a68 1

d75 1
a75 1

d79 1
a79 1
  ProgramStateRef state = C.getState();
d82 2
a83 2

  // First, ensure that the value is >= 0.
d94 1
a94 1
    // This means we cannot properly reason about it.
d97 1
a97 1

d100 1
a100 1

d109 1
a109 1

d113 1
a113 1

d117 1
a117 1

d130 1
a130 1
    // This means we cannot properly reason about it.
d133 1
a133 1

d136 1
a136 1

d145 1
a145 1

d149 1
a149 1

@


1.1.1.4.16.1
log
@Mostly merge changes from HEAD upto 20200411
@
text
@@


1.1.1.5
log
@Mark old LLVM instance as dead.
@
text
@@


1.1.1.3.4.1
log
@file BoolAssignmentChecker.cpp was added on branch tls-maxphys on 2014-08-19 23:47:31 +0000
@
text
@d1 157
@


1.1.1.3.4.2
log
@Rebase to HEAD as of a few days ago.
@
text
@a0 157
//== BoolAssignmentChecker.cpp - Boolean assignment 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 BoolAssignmentChecker, a builtin check in ExprEngine that
// performs checks for assignment of non-Boolean values to Boolean variables.
//
//===----------------------------------------------------------------------===//

#include "ClangSACheckers.h"
#include "clang/StaticAnalyzer/Core/BugReporter/BugType.h"
#include "clang/StaticAnalyzer/Core/Checker.h"
#include "clang/StaticAnalyzer/Core/CheckerManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"

using namespace clang;
using namespace ento;

namespace {
  class BoolAssignmentChecker : public Checker< check::Bind > {
    mutable std::unique_ptr<BuiltinBug> BT;
    void emitReport(ProgramStateRef state, CheckerContext &C) const;
  public:
    void checkBind(SVal loc, SVal val, const Stmt *S, CheckerContext &C) const;
  };
} // end anonymous namespace

void BoolAssignmentChecker::emitReport(ProgramStateRef state,
                                       CheckerContext &C) const {
  if (ExplodedNode *N = C.addTransition(state)) {
    if (!BT)
      BT.reset(new BuiltinBug(this, "Assignment of a non-Boolean value"));
    C.emitReport(new BugReport(*BT, BT->getDescription(), N));
  }
}

static bool isBooleanType(QualType Ty) {
  if (Ty->isBooleanType()) // C++ or C99
    return true;
  
  if (const TypedefType *TT = Ty->getAs<TypedefType>())
    return TT->getDecl()->getName() == "BOOL"   || // Objective-C
           TT->getDecl()->getName() == "_Bool"  || // stdbool.h < C99
           TT->getDecl()->getName() == "Boolean";  // MacTypes.h
  
  return false;
}

void BoolAssignmentChecker::checkBind(SVal loc, SVal val, const Stmt *S,
                                      CheckerContext &C) const {
  
  // We are only interested in stores into Booleans.
  const TypedValueRegion *TR =
    dyn_cast_or_null<TypedValueRegion>(loc.getAsRegion());
  
  if (!TR)
    return;
  
  QualType valTy = TR->getValueType();
  
  if (!isBooleanType(valTy))
    return;
  
  // Get the value of the right-hand side.  We only care about values
  // that are defined (UnknownVals and UndefinedVals are handled by other
  // checkers).
  Optional<DefinedSVal> DV = val.getAs<DefinedSVal>();
  if (!DV)
    return;
    
  // Check if the assigned value meets our criteria for correctness.  It must
  // be a value that is either 0 or 1.  One way to check this is to see if
  // the value is possibly < 0 (for a negative value) or greater than 1.
  ProgramStateRef state = C.getState(); 
  SValBuilder &svalBuilder = C.getSValBuilder();
  ConstraintManager &CM = C.getConstraintManager();
  
  // First, ensure that the value is >= 0.  
  DefinedSVal zeroVal = svalBuilder.makeIntVal(0, valTy);
  SVal greaterThanOrEqualToZeroVal =
    svalBuilder.evalBinOp(state, BO_GE, *DV, zeroVal,
                          svalBuilder.getConditionType());

  Optional<DefinedSVal> greaterThanEqualToZero =
      greaterThanOrEqualToZeroVal.getAs<DefinedSVal>();

  if (!greaterThanEqualToZero) {
    // The SValBuilder cannot construct a valid SVal for this condition.
    // This means we cannot properly reason about it.    
    return;
  }
  
  ProgramStateRef stateLT, stateGE;
  std::tie(stateGE, stateLT) = CM.assumeDual(state, *greaterThanEqualToZero);
  
  // Is it possible for the value to be less than zero?
  if (stateLT) {
    // It is possible for the value to be less than zero.  We only
    // want to emit a warning, however, if that value is fully constrained.
    // If it it possible for the value to be >= 0, then essentially the
    // value is underconstrained and there is nothing left to be done.
    if (!stateGE)
      emitReport(stateLT, C);
    
    // In either case, we are done.
    return;
  }
  
  // If we reach here, it must be the case that the value is constrained
  // to only be >= 0.
  assert(stateGE == state);
  
  // At this point we know that the value is >= 0.
  // Now check to ensure that the value is <= 1.
  DefinedSVal OneVal = svalBuilder.makeIntVal(1, valTy);
  SVal lessThanEqToOneVal =
    svalBuilder.evalBinOp(state, BO_LE, *DV, OneVal,
                          svalBuilder.getConditionType());

  Optional<DefinedSVal> lessThanEqToOne =
      lessThanEqToOneVal.getAs<DefinedSVal>();

  if (!lessThanEqToOne) {
    // The SValBuilder cannot construct a valid SVal for this condition.
    // This means we cannot properly reason about it.    
    return;
  }
  
  ProgramStateRef stateGT, stateLE;
  std::tie(stateLE, stateGT) = CM.assumeDual(state, *lessThanEqToOne);
  
  // Is it possible for the value to be greater than one?
  if (stateGT) {
    // It is possible for the value to be greater than one.  We only
    // want to emit a warning, however, if that value is fully constrained.
    // If it is possible for the value to be <= 1, then essentially the
    // value is underconstrained and there is nothing left to be done.
    if (!stateLE)
      emitReport(stateGT, C);
    
    // In either case, we are done.
    return;
  }
  
  // If we reach here, it must be the case that the value is constrained
  // to only be <= 1.
  assert(stateLE == state);
}

void ento::registerBoolAssignmentChecker(CheckerManager &mgr) {
    mgr.registerChecker<BoolAssignmentChecker>();
}
@


1.1.1.2.4.1
log
@file BoolAssignmentChecker.cpp was added on branch yamt-pagecache on 2014-05-22 16:18:30 +0000
@
text
@d1 157
@


1.1.1.2.4.2
log
@sync with head.

for a reference, the tree before this commit was tagged
as yamt-pagecache-tag8.

this commit was splitted into small chunks to avoid
a limitation of cvs.  ("Protocol error: too many arguments")
@
text
@a0 157
//== BoolAssignmentChecker.cpp - Boolean assignment 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 BoolAssignmentChecker, a builtin check in ExprEngine that
// performs checks for assignment of non-Boolean values to Boolean variables.
//
//===----------------------------------------------------------------------===//

#include "ClangSACheckers.h"
#include "clang/StaticAnalyzer/Core/BugReporter/BugType.h"
#include "clang/StaticAnalyzer/Core/Checker.h"
#include "clang/StaticAnalyzer/Core/CheckerManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"

using namespace clang;
using namespace ento;

namespace {
  class BoolAssignmentChecker : public Checker< check::Bind > {
    mutable OwningPtr<BuiltinBug> BT;
    void emitReport(ProgramStateRef state, CheckerContext &C) const;
  public:
    void checkBind(SVal loc, SVal val, const Stmt *S, CheckerContext &C) const;
  };
} // end anonymous namespace

void BoolAssignmentChecker::emitReport(ProgramStateRef state,
                                       CheckerContext &C) const {
  if (ExplodedNode *N = C.addTransition(state)) {
    if (!BT)
      BT.reset(new BuiltinBug(this, "Assignment of a non-Boolean value"));
    C.emitReport(new BugReport(*BT, BT->getDescription(), N));
  }
}

static bool isBooleanType(QualType Ty) {
  if (Ty->isBooleanType()) // C++ or C99
    return true;
  
  if (const TypedefType *TT = Ty->getAs<TypedefType>())
    return TT->getDecl()->getName() == "BOOL"   || // Objective-C
           TT->getDecl()->getName() == "_Bool"  || // stdbool.h < C99
           TT->getDecl()->getName() == "Boolean";  // MacTypes.h
  
  return false;
}

void BoolAssignmentChecker::checkBind(SVal loc, SVal val, const Stmt *S,
                                      CheckerContext &C) const {
  
  // We are only interested in stores into Booleans.
  const TypedValueRegion *TR =
    dyn_cast_or_null<TypedValueRegion>(loc.getAsRegion());
  
  if (!TR)
    return;
  
  QualType valTy = TR->getValueType();
  
  if (!isBooleanType(valTy))
    return;
  
  // Get the value of the right-hand side.  We only care about values
  // that are defined (UnknownVals and UndefinedVals are handled by other
  // checkers).
  Optional<DefinedSVal> DV = val.getAs<DefinedSVal>();
  if (!DV)
    return;
    
  // Check if the assigned value meets our criteria for correctness.  It must
  // be a value that is either 0 or 1.  One way to check this is to see if
  // the value is possibly < 0 (for a negative value) or greater than 1.
  ProgramStateRef state = C.getState(); 
  SValBuilder &svalBuilder = C.getSValBuilder();
  ConstraintManager &CM = C.getConstraintManager();
  
  // First, ensure that the value is >= 0.  
  DefinedSVal zeroVal = svalBuilder.makeIntVal(0, valTy);
  SVal greaterThanOrEqualToZeroVal =
    svalBuilder.evalBinOp(state, BO_GE, *DV, zeroVal,
                          svalBuilder.getConditionType());

  Optional<DefinedSVal> greaterThanEqualToZero =
      greaterThanOrEqualToZeroVal.getAs<DefinedSVal>();

  if (!greaterThanEqualToZero) {
    // The SValBuilder cannot construct a valid SVal for this condition.
    // This means we cannot properly reason about it.    
    return;
  }
  
  ProgramStateRef stateLT, stateGE;
  llvm::tie(stateGE, stateLT) = CM.assumeDual(state, *greaterThanEqualToZero);
  
  // Is it possible for the value to be less than zero?
  if (stateLT) {
    // It is possible for the value to be less than zero.  We only
    // want to emit a warning, however, if that value is fully constrained.
    // If it it possible for the value to be >= 0, then essentially the
    // value is underconstrained and there is nothing left to be done.
    if (!stateGE)
      emitReport(stateLT, C);
    
    // In either case, we are done.
    return;
  }
  
  // If we reach here, it must be the case that the value is constrained
  // to only be >= 0.
  assert(stateGE == state);
  
  // At this point we know that the value is >= 0.
  // Now check to ensure that the value is <= 1.
  DefinedSVal OneVal = svalBuilder.makeIntVal(1, valTy);
  SVal lessThanEqToOneVal =
    svalBuilder.evalBinOp(state, BO_LE, *DV, OneVal,
                          svalBuilder.getConditionType());

  Optional<DefinedSVal> lessThanEqToOne =
      lessThanEqToOneVal.getAs<DefinedSVal>();

  if (!lessThanEqToOne) {
    // The SValBuilder cannot construct a valid SVal for this condition.
    // This means we cannot properly reason about it.    
    return;
  }
  
  ProgramStateRef stateGT, stateLE;
  llvm::tie(stateLE, stateGT) = CM.assumeDual(state, *lessThanEqToOne);
  
  // Is it possible for the value to be greater than one?
  if (stateGT) {
    // It is possible for the value to be greater than one.  We only
    // want to emit a warning, however, if that value is fully constrained.
    // If it is possible for the value to be <= 1, then essentially the
    // value is underconstrained and there is nothing left to be done.
    if (!stateLE)
      emitReport(stateGT, C);
    
    // In either case, we are done.
    return;
  }
  
  // If we reach here, it must be the case that the value is constrained
  // to only be <= 1.
  assert(stateLE == state);
}

void ento::registerBoolAssignmentChecker(CheckerManager &mgr) {
    mgr.registerChecker<BoolAssignmentChecker>();
}
@


