contrib/llvm/tools/clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp

   1 //== SMTConstraintManager.cpp -----------------------------------*- C++ -*--==//
   2 //
   3 //                     The LLVM Compiler Infrastructure
   4 //
   5 // This file is distributed under the University of Illinois Open Source
   6 // License. See LICENSE.TXT for details.
   7 //
   8 //===----------------------------------------------------------------------===//
   9
  10 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
  11 #include "clang/Basic/TargetInfo.h"
  12 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
  13 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
  14
  15 using namespace clang;
  16 using namespace ento;
  17
  18 ProgramStateRef SMTConstraintManager::assumeSym(ProgramStateRef State,
  19                                                 SymbolRef Sym,
  20                                                 bool Assumption) {
  21   ASTContext &Ctx = getBasicVals().getContext();
  22
  23   QualType RetTy;
  24   bool hasComparison;
  25
  26   SMTExprRef Exp = Solver->getExpr(Ctx, Sym, &RetTy, &hasComparison);
  27
  28   // Create zero comparison for implicit boolean cast, with reversed assumption
  29   if (!hasComparison && !RetTy->isBooleanType())
  30     return assumeExpr(State, Sym,
  31                       Solver->getZeroExpr(Ctx, Exp, RetTy, !Assumption));
  32
  33   return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
  34 }
  35
  36 ProgramStateRef SMTConstraintManager::assumeSymInclusiveRange(
  37     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
  38     const llvm::APSInt &To, bool InRange) {
  39   ASTContext &Ctx = getBasicVals().getContext();
  40   return assumeExpr(State, Sym,
  41                     Solver->getRangeExpr(Ctx, Sym, From, To, InRange));
  42 }
  43
  44 ProgramStateRef
  45 SMTConstraintManager::assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
  46                                            bool Assumption) {
  47   // Skip anything that is unsupported
  48   return State;
  49 }
  50
  51 ConditionTruthVal SMTConstraintManager::checkNull(ProgramStateRef State,
  52                                                   SymbolRef Sym) {
  53   ASTContext &Ctx = getBasicVals().getContext();
  54
  55   QualType RetTy;
  56   // The expression may be casted, so we cannot call getZ3DataExpr() directly
  57   SMTExprRef VarExp = Solver->getExpr(Ctx, Sym, &RetTy);
  58   SMTExprRef Exp = Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/true);
  59
  60   // Negate the constraint
  61   SMTExprRef NotExp =
  62       Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/false);
  63
  64   Solver->reset();
  65   addStateConstraints(State);
  66
  67   Solver->push();
  68   Solver->addConstraint(Exp);
  69   ConditionTruthVal isSat = Solver->check();
  70
  71   Solver->pop();
  72   Solver->addConstraint(NotExp);
  73   ConditionTruthVal isNotSat = Solver->check();
  74
  75   // Zero is the only possible solution
  76   if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
  77     return true;
  78
  79   // Zero is not a solution
  80   if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
  81     return false;
  82
  83   // Zero may be a solution
  84   return ConditionTruthVal();
  85 }
  86
  87 const llvm::APSInt *SMTConstraintManager::getSymVal(ProgramStateRef State,
  88                                                     SymbolRef Sym) const {
  89   BasicValueFactory &BVF = getBasicVals();
  90   ASTContext &Ctx = BVF.getContext();
  91
  92   if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
  93     QualType Ty = Sym->getType();
  94     assert(!Ty->isRealFloatingType());
  95     llvm::APSInt Value(Ctx.getTypeSize(Ty),
  96                        !Ty->isSignedIntegerOrEnumerationType());
  97
  98     SMTExprRef Exp =
  99         Solver->fromData(SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
 100
 101     Solver->reset();
 102     addStateConstraints(State);
 103
 104     // Constraints are unsatisfiable
 105     ConditionTruthVal isSat = Solver->check();
 106     if (!isSat.isConstrainedTrue())
 107       return nullptr;
 108
 109     // Model does not assign interpretation
 110     if (!Solver->getInterpretation(Exp, Value))
 111       return nullptr;
 112
 113     // A value has been obtained, check if it is the only value
 114     SMTExprRef NotExp = Solver->fromBinOp(
 115         Exp, BO_NE,
 116         Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue())
 117                             : Solver->fromAPSInt(Value),
 118         false);
 119
 120     Solver->addConstraint(NotExp);
 121
 122     ConditionTruthVal isNotSat = Solver->check();
 123     if (isNotSat.isConstrainedTrue())
 124       return nullptr;
 125
 126     // This is the only solution, store it
 127     return &BVF.getValue(Value);
 128   }
 129
 130   if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
 131     SymbolRef CastSym = SC->getOperand();
 132     QualType CastTy = SC->getType();
 133     // Skip the void type
 134     if (CastTy->isVoidType())
 135       return nullptr;
 136
 137     const llvm::APSInt *Value;
 138     if (!(Value = getSymVal(State, CastSym)))
 139       return nullptr;
 140     return &BVF.Convert(SC->getType(), *Value);
 141   }
 142
 143   if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
 144     const llvm::APSInt *LHS, *RHS;
 145     if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
 146       LHS = getSymVal(State, SIE->getLHS());
 147       RHS = &SIE->getRHS();
 148     } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
 149       LHS = &ISE->getLHS();
 150       RHS = getSymVal(State, ISE->getRHS());
 151     } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
 152       // Early termination to avoid expensive call
 153       LHS = getSymVal(State, SSM->getLHS());
 154       RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
 155     } else {
 156       llvm_unreachable("Unsupported binary expression to get symbol value!");
 157     }
 158
 159     if (!LHS || !RHS)
 160       return nullptr;
 161
 162     llvm::APSInt ConvertedLHS, ConvertedRHS;
 163     QualType LTy, RTy;
 164     std::tie(ConvertedLHS, LTy) = Solver->fixAPSInt(Ctx, *LHS);
 165     std::tie(ConvertedRHS, RTy) = Solver->fixAPSInt(Ctx, *RHS);
 166     Solver->doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>(
 167         Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
 168     return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
 169   }
 170
 171   llvm_unreachable("Unsupported expression to get symbol value!");
 172 }
 173
 174 ConditionTruthVal
 175 SMTConstraintManager::checkModel(ProgramStateRef State,
 176                                  const SMTExprRef &Exp) const {
 177   Solver->reset();
 178   Solver->addConstraint(Exp);
 179   addStateConstraints(State);
 180   return Solver->check();
 181 }