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