Home | History | Annotate | Line # | Download | only in PathSensitive 
      1 //== SMTConstraintManager.h -------------------------------------*- C++ -*--==//
      2 //
      3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
      4 // See https://llvm.org/LICENSE.txt for license information.
      5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
      6 //
      7 //===----------------------------------------------------------------------===//
      8 //
      9 //  This file defines a SMT generic API, which will be the base class for
     10 //  every SMT solver specific class.
     11 //
     12 //===----------------------------------------------------------------------===//
     13 
     14 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
     15 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
     16 
     17 #include "clang/Basic/JsonSupport.h"
     18 #include "clang/Basic/TargetInfo.h"
     19 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
     20 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
     21 
     22 typedef llvm::ImmutableSet<
     23     std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
     24     ConstraintSMTType;
     25 REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTType)
     26 
     27 namespace clang {
     28 namespace ento {
     29 
     30 class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
     31   mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
     32 
     33 public:
     34   SMTConstraintManager(clang::ento::ExprEngine *EE,
     35                        clang::ento::SValBuilder &SB)
     36       : SimpleConstraintManager(EE, SB) {}
     37   virtual ~SMTConstraintManager() = default;
     38 
     39   //===------------------------------------------------------------------===//
     40   // Implementation for interface from SimpleConstraintManager.
     41   //===------------------------------------------------------------------===//
     42 
     43   ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
     44                             bool Assumption) override {
     45     ASTContext &Ctx = getBasicVals().getContext();
     46 
     47     QualType RetTy;
     48     bool hasComparison;
     49 
     50     llvm::SMTExprRef Exp =
     51         SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
     52 
     53     // Create zero comparison for implicit boolean cast, with reversed
     54     // assumption
     55     if (!hasComparison && !RetTy->isBooleanType())
     56       return assumeExpr(
     57           State, Sym,
     58           SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
     59 
     60     return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
     61   }
     62 
     63   ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
     64                                           const llvm::APSInt &From,
     65                                           const llvm::APSInt &To,
     66                                           bool InRange) override {
     67     ASTContext &Ctx = getBasicVals().getContext();
     68     return assumeExpr(
     69         State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
     70   }
     71 
     72   ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
     73                                        bool Assumption) override {
     74     // Skip anything that is unsupported
     75     return State;
     76   }
     77 
     78   //===------------------------------------------------------------------===//
     79   // Implementation for interface from ConstraintManager.
     80   //===------------------------------------------------------------------===//
     81 
     82   ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override {
     83     ASTContext &Ctx = getBasicVals().getContext();
     84 
     85     QualType RetTy;
     86     // The expression may be casted, so we cannot call getZ3DataExpr() directly
     87     llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
     88     llvm::SMTExprRef Exp =
     89         SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
     90 
     91     // Negate the constraint
     92     llvm::SMTExprRef NotExp =
     93         SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
     94 
     95     ConditionTruthVal isSat = checkModel(State, Sym, Exp);
     96     ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp);
     97 
     98     // Zero is the only possible solution
     99     if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
    100       return true;
    101 
    102     // Zero is not a solution
    103     if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
    104       return false;
    105 
    106     // Zero may be a solution
    107     return ConditionTruthVal();
    108   }
    109 
    110   const llvm::APSInt *getSymVal(ProgramStateRef State,
    111                                 SymbolRef Sym) const override {
    112     BasicValueFactory &BVF = getBasicVals();
    113     ASTContext &Ctx = BVF.getContext();
    114 
    115     if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
    116       QualType Ty = Sym->getType();
    117       assert(!Ty->isRealFloatingType());
    118       llvm::APSInt Value(Ctx.getTypeSize(Ty),
    119                          !Ty->isSignedIntegerOrEnumerationType());
    120 
    121       // TODO: this should call checkModel so we can use the cache, however,
    122       // this method tries to get the interpretation (the actual value) from
    123       // the solver, which is currently not cached.
    124 
    125       llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD);
    126 
    127       Solver->reset();
    128       addStateConstraints(State);
    129 
    130       // Constraints are unsatisfiable
    131       Optional<bool> isSat = Solver->check();
    132       if (!isSat.hasValue() || !isSat.getValue())
    133         return nullptr;
    134 
    135       // Model does not assign interpretation
    136       if (!Solver->getInterpretation(Exp, Value))
    137         return nullptr;
    138 
    139       // A value has been obtained, check if it is the only value
    140       llvm::SMTExprRef NotExp = SMTConv::fromBinOp(
    141           Solver, Exp, BO_NE,
    142           Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
    143                               : Solver->mkBitvector(Value, Value.getBitWidth()),
    144           /*isSigned=*/false);
    145 
    146       Solver->addConstraint(NotExp);
    147 
    148       Optional<bool> isNotSat = Solver->check();
    149       if (!isNotSat.hasValue() || isNotSat.getValue())
    150         return nullptr;
    151 
    152       // This is the only solution, store it
    153       return &BVF.getValue(Value);
    154     }
    155 
    156     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
    157       SymbolRef CastSym = SC->getOperand();
    158       QualType CastTy = SC->getType();
    159       // Skip the void type
    160       if (CastTy->isVoidType())
    161         return nullptr;
    162 
    163       const llvm::APSInt *Value;
    164       if (!(Value = getSymVal(State, CastSym)))
    165         return nullptr;
    166       return &BVF.Convert(SC->getType(), *Value);
    167     }
    168 
    169     if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
    170       const llvm::APSInt *LHS, *RHS;
    171       if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
    172         LHS = getSymVal(State, SIE->getLHS());
    173         RHS = &SIE->getRHS();
    174       } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
    175         LHS = &ISE->getLHS();
    176         RHS = getSymVal(State, ISE->getRHS());
    177       } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
    178         // Early termination to avoid expensive call
    179         LHS = getSymVal(State, SSM->getLHS());
    180         RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
    181       } else {
    182         llvm_unreachable("Unsupported binary expression to get symbol value!");
    183       }
    184 
    185       if (!LHS || !RHS)
    186         return nullptr;
    187 
    188       llvm::APSInt ConvertedLHS, ConvertedRHS;
    189       QualType LTy, RTy;
    190       std::tie(ConvertedLHS, LTy) = SMTConv::fixAPSInt(Ctx, *LHS);
    191       std::tie(ConvertedRHS, RTy) = SMTConv::fixAPSInt(Ctx, *RHS);
    192       SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
    193           Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
    194       return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
    195     }
    196 
    197     llvm_unreachable("Unsupported expression to get symbol value!");
    198   }
    199 
    200   ProgramStateRef removeDeadBindings(ProgramStateRef State,
    201                                      SymbolReaper &SymReaper) override {
    202     auto CZ = State->get<ConstraintSMT>();
    203     auto &CZFactory = State->get_context<ConstraintSMT>();
    204 
    205     for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
    206       if (SymReaper.isDead(I->first))
    207         CZ = CZFactory.remove(CZ, *I);
    208     }
    209 
    210     return State->set<ConstraintSMT>(CZ);
    211   }
    212 
    213   void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n",
    214                  unsigned int Space = 0, bool IsDot = false) const override {
    215     ConstraintSMTType Constraints = State->get<ConstraintSMT>();
    216 
    217     Indent(Out, Space, IsDot) << "\"constraints\": ";
    218     if (Constraints.isEmpty()) {
    219       Out << "null," << NL;
    220       return;
    221     }
    222 
    223     ++Space;
    224     Out << '[' << NL;
    225     for (ConstraintSMTType::iterator I = Constraints.begin();
    226          I != Constraints.end(); ++I) {
    227       Indent(Out, Space, IsDot)
    228           << "{ \"symbol\": \"" << I->first << "\", \"range\": \"";
    229       I->second->print(Out);
    230       Out << "\" }";
    231 
    232       if (std::next(I) != Constraints.end())
    233         Out << ',';
    234       Out << NL;
    235     }
    236 
    237     --Space;
    238     Indent(Out, Space, IsDot) << "],";
    239   }
    240 
    241   bool haveEqualConstraints(ProgramStateRef S1,
    242                             ProgramStateRef S2) const override {
    243     return S1->get<ConstraintSMT>() == S2->get<ConstraintSMT>();
    244   }
    245 
    246   bool canReasonAbout(SVal X) const override {
    247     const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
    248 
    249     Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
    250     if (!SymVal)
    251       return true;
    252 
    253     const SymExpr *Sym = SymVal->getSymbol();
    254     QualType Ty = Sym->getType();
    255 
    256     // Complex types are not modeled
    257     if (Ty->isComplexType() || Ty->isComplexIntegerType())
    258       return false;
    259 
    260     // Non-IEEE 754 floating-point types are not modeled
    261     if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
    262          (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
    263           &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
    264       return false;
    265 
    266     if (Ty->isRealFloatingType())
    267       return Solver->isFPSupported();
    268 
    269     if (isa<SymbolData>(Sym))
    270       return true;
    271 
    272     SValBuilder &SVB = getSValBuilder();
    273 
    274     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
    275       return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
    276 
    277     if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
    278       if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
    279         return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
    280 
    281       if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
    282         return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
    283 
    284       if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
    285         return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
    286                canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
    287     }
    288 
    289     llvm_unreachable("Unsupported expression to reason about!");
    290   }
    291 
    292   /// Dumps SMT formula
    293   LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
    294 
    295 protected:
    296   // Check whether a new model is satisfiable, and update the program state.
    297   virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
    298                                      const llvm::SMTExprRef &Exp) {
    299     // Check the model, avoid simplifying AST to save time
    300     if (checkModel(State, Sym, Exp).isConstrainedTrue())
    301       return State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
    302 
    303     return nullptr;
    304   }
    305 
    306   /// Given a program state, construct the logical conjunction and add it to
    307   /// the solver
    308   virtual void addStateConstraints(ProgramStateRef State) const {
    309     // TODO: Don't add all the constraints, only the relevant ones
    310     auto CZ = State->get<ConstraintSMT>();
    311     auto I = CZ.begin(), IE = CZ.end();
    312 
    313     // Construct the logical AND of all the constraints
    314     if (I != IE) {
    315       std::vector<llvm::SMTExprRef> ASTs;
    316 
    317       llvm::SMTExprRef Constraint = I++->second;
    318       while (I != IE) {
    319         Constraint = Solver->mkAnd(Constraint, I++->second);
    320       }
    321 
    322       Solver->addConstraint(Constraint);
    323     }
    324   }
    325 
    326   // Generate and check a Z3 model, using the given constraint.
    327   ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym,
    328                                const llvm::SMTExprRef &Exp) const {
    329     ProgramStateRef NewState =
    330         State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
    331 
    332     llvm::FoldingSetNodeID ID;
    333     NewState->get<ConstraintSMT>().Profile(ID);
    334 
    335     unsigned hash = ID.ComputeHash();
    336     auto I = Cached.find(hash);
    337     if (I != Cached.end())
    338       return I->second;
    339 
    340     Solver->reset();
    341     addStateConstraints(NewState);
    342 
    343     Optional<bool> res = Solver->check();
    344     if (!res.hasValue())
    345       Cached[hash] = ConditionTruthVal();
    346     else
    347       Cached[hash] = ConditionTruthVal(res.getValue());
    348 
    349     return Cached[hash];
    350   }
    351 
    352   // Cache the result of an SMT query (true, false, unknown). The key is the
    353   // hash of the constraints in a state
    354   mutable llvm::DenseMap<unsigned, ConditionTruthVal> Cached;
    355 }; // end class SMTConstraintManager
    356 
    357 } // namespace ento
    358 } // namespace clang
    359 
    360 #endif
    361