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;
REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT,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 (!isSat.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