Core/PathSensitive/SMTConstraintManager.h

0001 //== SMTConstraintManager.h -------------------------------------*- C++ -*--==//
0002 //
0003 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
0004 // See https://llvm.org/LICENSE.txt for license information.
0005 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
0006 //
0007 //===----------------------------------------------------------------------===//
0008 //
0009 //  This file defines a SMT generic API, which will be the base class for
0010 //  every SMT solver specific class.
0011 //
0012 //===----------------------------------------------------------------------===//
0013
0014 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
0015 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
0016
0017 #include "clang/Basic/JsonSupport.h"
0018 #include "clang/Basic/TargetInfo.h"
0019 #include "clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h"
0020 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
0021 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
0022 #include <optional>
0023
0024 typedef llvm::ImmutableSet<
0025     std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
0026     ConstraintSMTType;
0027 REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTType)
0028
0029 namespace clang {
0030 namespace ento {
0031
0032 class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
0033   mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
0034
0035 public:
0036   SMTConstraintManager(clang::ento::ExprEngine *EE,
0037                        clang::ento::SValBuilder &SB)
0038       : SimpleConstraintManager(EE, SB) {
0039     Solver->setBoolParam("model", true); // Enable model finding
0040     Solver->setUnsignedParam("timeout", 15000 /*milliseconds*/);
0041   }
0042   virtual ~SMTConstraintManager() = default;
0043
0044   //===------------------------------------------------------------------===//
0045   // Implementation for interface from SimpleConstraintManager.
0046   //===------------------------------------------------------------------===//
0047
0048   ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
0049                             bool Assumption) override {
0050     ASTContext &Ctx = getBasicVals().getContext();
0051
0052     QualType RetTy;
0053     bool hasComparison;
0054
0055     llvm::SMTExprRef Exp =
0056         SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
0057
0058     // Create zero comparison for implicit boolean cast, with reversed
0059     // assumption
0060     if (!hasComparison && !RetTy->isBooleanType())
0061       return assumeExpr(
0062           State, Sym,
0063           SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
0064
0065     return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
0066   }
0067
0068   ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
0069                                           const llvm::APSInt &From,
0070                                           const llvm::APSInt &To,
0071                                           bool InRange) override {
0072     ASTContext &Ctx = getBasicVals().getContext();
0073     return assumeExpr(
0074         State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
0075   }
0076
0077   ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
0078                                        bool Assumption) override {
0079     // Skip anything that is unsupported
0080     return State;
0081   }
0082
0083   //===------------------------------------------------------------------===//
0084   // Implementation for interface from ConstraintManager.
0085   //===------------------------------------------------------------------===//
0086
0087   ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override {
0088     ASTContext &Ctx = getBasicVals().getContext();
0089
0090     QualType RetTy;
0091     // The expression may be casted, so we cannot call getZ3DataExpr() directly
0092     llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
0093     llvm::SMTExprRef Exp =
0094         SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
0095
0096     // Negate the constraint
0097     llvm::SMTExprRef NotExp =
0098         SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
0099
0100     ConditionTruthVal isSat = checkModel(State, Sym, Exp);
0101     ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp);
0102
0103     // Zero is the only possible solution
0104     if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
0105       return true;
0106
0107     // Zero is not a solution
0108     if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
0109       return false;
0110
0111     // Zero may be a solution
0112     return ConditionTruthVal();
0113   }
0114
0115   const llvm::APSInt *getSymVal(ProgramStateRef State,
0116                                 SymbolRef Sym) const override {
0117     BasicValueFactory &BVF = getBasicVals();
0118     ASTContext &Ctx = BVF.getContext();
0119
0120     if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
0121       QualType Ty = Sym->getType();
0122       assert(!Ty->isRealFloatingType());
0123       llvm::APSInt Value(Ctx.getTypeSize(Ty),
0124                          !Ty->isSignedIntegerOrEnumerationType());
0125
0126       // TODO: this should call checkModel so we can use the cache, however,
0127       // this method tries to get the interpretation (the actual value) from
0128       // the solver, which is currently not cached.
0129
0130       llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD);
0131
0132       Solver->reset();
0133       addStateConstraints(State);
0134
0135       // Constraints are unsatisfiable
0136       std::optional<bool> isSat = Solver->check();
0137       if (!isSat || !*isSat)
0138         return nullptr;
0139
0140       // Model does not assign interpretation
0141       if (!Solver->getInterpretation(Exp, Value))
0142         return nullptr;
0143
0144       // A value has been obtained, check if it is the only value
0145       llvm::SMTExprRef NotExp = SMTConv::fromBinOp(
0146           Solver, Exp, BO_NE,
0147           Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
0148                               : Solver->mkBitvector(Value, Value.getBitWidth()),
0149           /*isSigned=*/false);
0150
0151       Solver->addConstraint(NotExp);
0152
0153       std::optional<bool> isNotSat = Solver->check();
0154       if (!isNotSat || *isNotSat)
0155         return nullptr;
0156
0157       // This is the only solution, store it
0158       return BVF.getValue(Value).get();
0159     }
0160
0161     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
0162       SymbolRef CastSym = SC->getOperand();
0163       QualType CastTy = SC->getType();
0164       // Skip the void type
0165       if (CastTy->isVoidType())
0166         return nullptr;
0167
0168       const llvm::APSInt *Value;
0169       if (!(Value = getSymVal(State, CastSym)))
0170         return nullptr;
0171       return BVF.Convert(SC->getType(), *Value).get();
0172     }
0173
0174     if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
0175       const llvm::APSInt *LHS, *RHS;
0176       if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
0177         LHS = getSymVal(State, SIE->getLHS());
0178         RHS = SIE->getRHS().get();
0179       } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
0180         LHS = ISE->getLHS().get();
0181         RHS = getSymVal(State, ISE->getRHS());
0182       } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
0183         // Early termination to avoid expensive call
0184         LHS = getSymVal(State, SSM->getLHS());
0185         RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
0186       } else {
0187         llvm_unreachable("Unsupported binary expression to get symbol value!");
0188       }
0189
0190       if (!LHS || !RHS)
0191         return nullptr;
0192
0193       llvm::APSInt ConvertedLHS, ConvertedRHS;
0194       QualType LTy, RTy;
0195       std::tie(ConvertedLHS, LTy) = SMTConv::fixAPSInt(Ctx, *LHS);
0196       std::tie(ConvertedRHS, RTy) = SMTConv::fixAPSInt(Ctx, *RHS);
0197       SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
0198           Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
0199       std::optional<APSIntPtr> Res =
0200           BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
0201       return Res ? Res.value().get() : nullptr;
0202     }
0203
0204     llvm_unreachable("Unsupported expression to get symbol value!");
0205   }
0206
0207   ProgramStateRef removeDeadBindings(ProgramStateRef State,
0208                                      SymbolReaper &SymReaper) override {
0209     auto CZ = State->get<ConstraintSMT>();
0210     auto &CZFactory = State->get_context<ConstraintSMT>();
0211
0212     for (const auto &Entry : CZ) {
0213       if (SymReaper.isDead(Entry.first))
0214         CZ = CZFactory.remove(CZ, Entry);
0215     }
0216
0217     return State->set<ConstraintSMT>(CZ);
0218   }
0219
0220   void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n",
0221                  unsigned int Space = 0, bool IsDot = false) const override {
0222     ConstraintSMTType Constraints = State->get<ConstraintSMT>();
0223
0224     Indent(Out, Space, IsDot) << "\"constraints\": ";
0225     if (Constraints.isEmpty()) {
0226       Out << "null," << NL;
0227       return;
0228     }
0229
0230     ++Space;
0231     Out << '[' << NL;
0232     for (ConstraintSMTType::iterator I = Constraints.begin();
0233          I != Constraints.end(); ++I) {
0234       Indent(Out, Space, IsDot)
0235           << "{ \"symbol\": \"" << I->first << "\", \"range\": \"";
0236       I->second->print(Out);
0237       Out << "\" }";
0238
0239       if (std::next(I) != Constraints.end())
0240         Out << ',';
0241       Out << NL;
0242     }
0243
0244     --Space;
0245     Indent(Out, Space, IsDot) << "],";
0246   }
0247
0248   bool haveEqualConstraints(ProgramStateRef S1,
0249                             ProgramStateRef S2) const override {
0250     return S1->get<ConstraintSMT>() == S2->get<ConstraintSMT>();
0251   }
0252
0253   bool canReasonAbout(SVal X) const override {
0254     const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
0255
0256     std::optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
0257     if (!SymVal)
0258       return true;
0259
0260     const SymExpr *Sym = SymVal->getSymbol();
0261     QualType Ty = Sym->getType();
0262
0263     // Complex types are not modeled
0264     if (Ty->isComplexType() || Ty->isComplexIntegerType())
0265       return false;
0266
0267     // Non-IEEE 754 floating-point types are not modeled
0268     if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
0269          (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
0270           &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
0271       return false;
0272
0273     if (Ty->isRealFloatingType())
0274       return Solver->isFPSupported();
0275
0276     if (isa<SymbolData>(Sym))
0277       return true;
0278
0279     SValBuilder &SVB = getSValBuilder();
0280
0281     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
0282       return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
0283
0284     // UnarySymExpr support is not yet implemented in the Z3 wrapper.
0285     if (isa<UnarySymExpr>(Sym)) {
0286       return false;
0287     }
0288
0289     if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
0290       if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
0291         return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
0292
0293       if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
0294         return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
0295
0296       if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
0297         return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
0298                canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
0299     }
0300
0301     llvm_unreachable("Unsupported expression to reason about!");
0302   }
0303
0304   /// Dumps SMT formula
0305   LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
0306
0307 protected:
0308   // Check whether a new model is satisfiable, and update the program state.
0309   virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
0310                                      const llvm::SMTExprRef &Exp) {
0311     // Check the model, avoid simplifying AST to save time
0312     if (checkModel(State, Sym, Exp).isConstrainedTrue())
0313       return State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
0314
0315     return nullptr;
0316   }
0317
0318   /// Given a program state, construct the logical conjunction and add it to
0319   /// the solver
0320   virtual void addStateConstraints(ProgramStateRef State) const {
0321     // TODO: Don't add all the constraints, only the relevant ones
0322     auto CZ = State->get<ConstraintSMT>();
0323     auto I = CZ.begin(), IE = CZ.end();
0324
0325     // Construct the logical AND of all the constraints
0326     if (I != IE) {
0327       std::vector<llvm::SMTExprRef> ASTs;
0328
0329       llvm::SMTExprRef Constraint = I++->second;
0330       while (I != IE) {
0331         Constraint = Solver->mkAnd(Constraint, I++->second);
0332       }
0333
0334       Solver->addConstraint(Constraint);
0335     }
0336   }
0337
0338   // Generate and check a Z3 model, using the given constraint.
0339   ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym,
0340                                const llvm::SMTExprRef &Exp) const {
0341     ProgramStateRef NewState =
0342         State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
0343
0344     llvm::FoldingSetNodeID ID;
0345     NewState->get<ConstraintSMT>().Profile(ID);
0346
0347     unsigned hash = ID.ComputeHash();
0348     auto I = Cached.find(hash);
0349     if (I != Cached.end())
0350       return I->second;
0351
0352     Solver->reset();
0353     addStateConstraints(NewState);
0354
0355     std::optional<bool> res = Solver->check();
0356     if (!res)
0357       Cached[hash] = ConditionTruthVal();
0358     else
0359       Cached[hash] = ConditionTruthVal(*res);
0360
0361     return Cached[hash];
0362   }
0363
0364   // Cache the result of an SMT query (true, false, unknown). The key is the
0365   // hash of the constraints in a state
0366   mutable llvm::DenseMap<unsigned, ConditionTruthVal> Cached;
0367 }; // end class SMTConstraintManager
0368
0369 } // namespace ento
0370 } // namespace clang
0371
0372 #endif