clang  8.0.0svn
SMTConstraintManager.h
Go to the documentation of this file.
1 //== SMTConstraintManager.h -------------------------------------*- 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 // This file defines a SMT generic API, which will be the base class for
11 // every SMT solver specific class.
12 //
13 //===----------------------------------------------------------------------===//
14 
15 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
16 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
17 
20 
21 namespace clang {
22 namespace ento {
23 
24 template <typename ConstraintSMT, typename SMTExprTy>
26  SMTSolverRef &Solver;
27 
28 public:
30  SMTSolverRef &S)
31  : SimpleConstraintManager(SE, SB), Solver(S) {}
32  virtual ~SMTConstraintManager() = default;
33 
34  //===------------------------------------------------------------------===//
35  // Implementation for interface from SimpleConstraintManager.
36  //===------------------------------------------------------------------===//
37 
39  bool Assumption) override {
41 
42  QualType RetTy;
43  bool hasComparison;
44 
45  SMTExprRef Exp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
46 
47  // Create zero comparison for implicit boolean cast, with reversed
48  // assumption
49  if (!hasComparison && !RetTy->isBooleanType())
50  return assumeExpr(
51  State, Sym,
52  SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
53 
54  return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
55  }
56 
58  const llvm::APSInt &From,
59  const llvm::APSInt &To,
60  bool InRange) override {
62  return assumeExpr(
63  State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
64  }
65 
67  bool Assumption) override {
68  // Skip anything that is unsupported
69  return State;
70  }
71 
72  //===------------------------------------------------------------------===//
73  // Implementation for interface from ConstraintManager.
74  //===------------------------------------------------------------------===//
75 
78 
79  QualType RetTy;
80  // The expression may be casted, so we cannot call getZ3DataExpr() directly
81  SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
82  SMTExprRef Exp =
83  SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
84 
85  // Negate the constraint
86  SMTExprRef NotExp =
87  SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
88 
89  ConditionTruthVal isSat = checkModel(State, Sym, Exp);
90  ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp);
91 
92  // Zero is the only possible solution
93  if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
94  return true;
95 
96  // Zero is not a solution
97  if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
98  return false;
99 
100  // Zero may be a solution
101  return ConditionTruthVal();
102  }
103 
104  const llvm::APSInt *getSymVal(ProgramStateRef State,
105  SymbolRef Sym) const override {
107  ASTContext &Ctx = BVF.getContext();
108 
109  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
110  QualType Ty = Sym->getType();
111  assert(!Ty->isRealFloatingType());
112  llvm::APSInt Value(Ctx.getTypeSize(Ty),
114 
115  // TODO: this should call checkModel so we can use the cache, however,
116  // this method tries to get the interpretation (the actual value) from
117  // the solver, which is currently not cached.
118 
119  SMTExprRef Exp =
120  SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
121 
122  Solver->reset();
123  addStateConstraints(State);
124 
125  // Constraints are unsatisfiable
126  Optional<bool> isSat = Solver->check();
127  if (!isSat.hasValue() || !isSat.getValue())
128  return nullptr;
129 
130  // Model does not assign interpretation
131  if (!Solver->getInterpretation(Exp, Value))
132  return nullptr;
133 
134  // A value has been obtained, check if it is the only value
136  Solver, Exp, BO_NE,
137  Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
138  : Solver->mkBitvector(Value, Value.getBitWidth()),
139  /*isSigned=*/false);
140 
141  Solver->addConstraint(NotExp);
142 
143  Optional<bool> isNotSat = Solver->check();
144  if (!isSat.hasValue() || isNotSat.getValue())
145  return nullptr;
146 
147  // This is the only solution, store it
148  return &BVF.getValue(Value);
149  }
150 
151  if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
152  SymbolRef CastSym = SC->getOperand();
153  QualType CastTy = SC->getType();
154  // Skip the void type
155  if (CastTy->isVoidType())
156  return nullptr;
157 
158  const llvm::APSInt *Value;
159  if (!(Value = getSymVal(State, CastSym)))
160  return nullptr;
161  return &BVF.Convert(SC->getType(), *Value);
162  }
163 
164  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
165  const llvm::APSInt *LHS, *RHS;
166  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
167  LHS = getSymVal(State, SIE->getLHS());
168  RHS = &SIE->getRHS();
169  } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
170  LHS = &ISE->getLHS();
171  RHS = getSymVal(State, ISE->getRHS());
172  } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
173  // Early termination to avoid expensive call
174  LHS = getSymVal(State, SSM->getLHS());
175  RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
176  } else {
177  llvm_unreachable("Unsupported binary expression to get symbol value!");
178  }
179 
180  if (!LHS || !RHS)
181  return nullptr;
182 
183  llvm::APSInt ConvertedLHS, ConvertedRHS;
184  QualType LTy, RTy;
185  std::tie(ConvertedLHS, LTy) = SMTConv::fixAPSInt(Ctx, *LHS);
186  std::tie(ConvertedRHS, RTy) = SMTConv::fixAPSInt(Ctx, *RHS);
187  SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
188  Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
189  return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
190  }
191 
192  llvm_unreachable("Unsupported expression to get symbol value!");
193  }
194 
196  SymbolReaper &SymReaper) override {
197  auto CZ = State->get<ConstraintSMT>();
198  auto &CZFactory = State->get_context<ConstraintSMT>();
199 
200  for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
201  if (SymReaper.isDead(I->first))
202  CZ = CZFactory.remove(CZ, *I);
203  }
204 
205  return State->set<ConstraintSMT>(CZ);
206  }
207 
208  void print(ProgramStateRef St, raw_ostream &OS, const char *nl,
209  const char *sep) override {
210 
211  auto CZ = St->get<ConstraintSMT>();
212 
213  OS << nl << sep << "Constraints:";
214  for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
215  OS << nl << ' ' << I->first << " : ";
216  I->second.print(OS);
217  }
218  OS << nl;
219  }
220 
221  bool canReasonAbout(SVal X) const override {
223 
225  if (!SymVal)
226  return true;
227 
228  const SymExpr *Sym = SymVal->getSymbol();
229  QualType Ty = Sym->getType();
230 
231  // Complex types are not modeled
232  if (Ty->isComplexType() || Ty->isComplexIntegerType())
233  return false;
234 
235  // Non-IEEE 754 floating-point types are not modeled
236  if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
237  (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
238  &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
239  return false;
240 
241  if (Ty->isRealFloatingType())
242  return Solver->isFPSupported();
243 
244  if (isa<SymbolData>(Sym))
245  return true;
246 
247  SValBuilder &SVB = getSValBuilder();
248 
249  if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
250  return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
251 
252  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
253  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
254  return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
255 
256  if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
257  return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
258 
259  if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
260  return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
261  canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
262  }
263 
264  llvm_unreachable("Unsupported expression to reason about!");
265  }
266 
267  /// Dumps SMT formula
268  LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
269 
270 protected:
271  // Check whether a new model is satisfiable, and update the program state.
273  const SMTExprRef &Exp) {
274  // Check the model, avoid simplifying AST to save time
275  if (checkModel(State, Sym, Exp).isConstrainedTrue())
276  return State->add<ConstraintSMT>(
277  std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp)));
278 
279  return nullptr;
280  }
281 
282  /// Given a program state, construct the logical conjunction and add it to
283  /// the solver
285  // TODO: Don't add all the constraints, only the relevant ones
286  auto CZ = State->get<ConstraintSMT>();
287  auto I = CZ.begin(), IE = CZ.end();
288 
289  // Construct the logical AND of all the constraints
290  if (I != IE) {
291  std::vector<SMTExprRef> ASTs;
292 
293  SMTExprRef Constraint = Solver->newExprRef(I++->second);
294  while (I != IE) {
295  Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second));
296  }
297 
298  Solver->addConstraint(Constraint);
299  }
300  }
301 
302  // Generate and check a Z3 model, using the given constraint.
304  const SMTExprRef &Exp) const {
305  ProgramStateRef NewState = State->add<ConstraintSMT>(
306  std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp)));
307 
308  llvm::FoldingSetNodeID ID;
309  NewState->get<ConstraintSMT>().Profile(ID);
310 
311  unsigned hash = ID.ComputeHash();
312  auto I = Cached.find(hash);
313  if (I != Cached.end())
314  return I->second;
315 
316  Solver->reset();
317  addStateConstraints(NewState);
318 
319  Optional<bool> res = Solver->check();
320  if (!res.hasValue())
321  Cached[hash] = ConditionTruthVal();
322  else
323  Cached[hash] = ConditionTruthVal(res.getValue());
324 
325  return Cached[hash];
326  }
327 
328  // Cache the result of an SMT query (true, false, unknown). The key is the
329  // hash of the constraints in a state
330  mutable llvm::DenseMap<unsigned, ConditionTruthVal> Cached;
331 }; // end class SMTConstraintManager
332 
333 } // namespace ento
334 } // namespace clang
335 
336 #endif
bool isConstrainedFalse() const
Return true if the constraint is perfectly constrained to &#39;false&#39;.
A (possibly-)qualified type.
Definition: Type.h:642
ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym, const SMTExprRef &Exp) const
bool isDead(SymbolRef sym)
Returns whether or not a symbol has been confirmed dead.
static SMTExprRef getRangeExpr(SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)
Definition: SMTConv.h:491
bool isRealFloatingType() const
Floating point categories.
Definition: Type.cpp:1937
static SMTExprRef getZeroExpr(SMTSolverRef &Solver, ASTContext &Ctx, const SMTExprRef &Exp, QualType Ty, bool Assumption)
Definition: SMTConv.h:461
static SMTExprRef getExpr(SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy=nullptr, bool *hasComparison=nullptr)
Definition: SMTConv.h:450
ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption) override
Given a symbolic expression that can be reasoned about, assume that it is true/false and generate the...
void print(ProgramStateRef St, raw_ostream &OS, const char *nl, const char *sep) override
SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB, SMTSolverRef &S)
const TargetInfo & getTargetInfo() const
Definition: ASTContext.h:689
virtual ~SMTConstraintManager()=default
Symbolic value.
Definition: SymExpr.h:30
static std::pair< llvm::APSInt, QualType > fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int)
Definition: SMTConv.h:537
SVal makeSymbolVal(SymbolRef Sym)
Make an SVal that represents the given symbol.
Definition: SValBuilder.h:373
Holds long-lived AST nodes (such as types and decls) that can be referred to throughout the semantic ...
Definition: ASTContext.h:154
static SMTExprRef fromData(SMTSolverRef &Solver, const SymbolID ID, const QualType &Ty, uint64_t BitWidth)
Construct an SMTExprRef from a SymbolData.
Definition: SMTConv.h:319
LineState State
bool isSpecificBuiltinType(unsigned K) const
Test for a particular builtin type.
Definition: Type.h:6497
const llvm::APSInt & Convert(const llvm::APSInt &To, const llvm::APSInt &From)
Convert - Create a new persistent APSInt with the same value as &#39;From&#39; but with the bitwidth and sign...
ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override
Returns whether or not a symbol is known to be null ("true"), known to be non-null ("false")...
ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, bool Assumption) override
Given a symbolic expression that cannot be reasoned about, assume that it is zero/nonzero and add it ...
Represents a symbolic expression like &#39;x&#39; + 3.
ProgramStateRef removeDeadBindings(ProgramStateRef State, SymbolReaper &SymReaper) override
Scan all symbols referenced by the constraints.
LLVM_DUMP_METHOD void dump() const
Dumps SMT formula.
virtual QualType getType() const =0
const llvm::APSInt * getSymVal(ProgramStateRef State, SymbolRef Sym) const override
If a symbol is perfectly constrained to a constant, attempt to return the concrete value...
bool isConstrainedTrue() const
Return true if the constraint is perfectly constrained to &#39;true&#39;.
bool isComplexType() const
isComplexType() does not include complex integers (a GCC extension).
Definition: Type.cpp:481
const llvm::fltSemantics & getLongDoubleFormat() const
Definition: TargetInfo.h:575
Exposes information about the current target.
Definition: TargetInfo.h:54
virtual void addStateConstraints(ProgramStateRef State) const
Given a program state, construct the logical conjunction and add it to the solver.
BasicValueFactory & getBasicVals() const
virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym, const SMTExprRef &Exp)
Represents a cast expression.
bool canReasonAbout(SVal X) const override
canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values.
Optional< T > getAs() const
Convert to the specified SVal type, returning None if this SVal is not of the desired type...
Definition: SVals.h:112
llvm::DenseMap< unsigned, ConditionTruthVal > Cached
SVal - This represents a symbolic expression, which can be either an L-value or an R-value...
Definition: SVals.h:76
bool isSignedIntegerOrEnumerationType() const
Determines whether this is an integer type that is signed or an enumeration types whose underlying ty...
Definition: Type.cpp:1860
Represents a symbolic expression like 3 - &#39;x&#39;.
A class responsible for cleaning up unused symbols.
const llvm::APSInt * evalAPSInt(BinaryOperator::Opcode Op, const llvm::APSInt &V1, const llvm::APSInt &V2)
static SMTExprRef fromBinOp(SMTSolverRef &Solver, const SMTExprRef &LHS, const BinaryOperator::Opcode Op, const SMTExprRef &RHS, bool isSigned)
Construct an SMTExprRef from a binary operator.
Definition: SMTConv.h:91
Dataflow Directional Tag Classes.
Represents a symbolic expression involving a binary operator.
bool isBooleanType() const
Definition: Type.h:6643
Represents symbolic expression that isn&#39;t a location.
Definition: SVals.h:347
std::shared_ptr< SMTSolver > SMTSolverRef
Shared pointer for SMTSolvers.
Definition: SMTSolver.h:295
uint64_t getTypeSize(QualType T) const
Return the size of the specified (complete) type T, in bits.
Definition: ASTContext.h:2069
X
Add a minimal nested name specifier fixit hint to allow lookup of a tag name from an outer enclosing ...
Definition: SemaDecl.cpp:13956
ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) override
Given a symbolic expression within the range [From, To], assume that it is true/false and generate th...
bool isVoidType() const
Definition: Type.h:6530
bool isComplexIntegerType() const
Definition: Type.cpp:487
std::shared_ptr< SMTExpr > SMTExprRef
Shared pointer for SMTExprs, used by SMTSolver API.
Definition: SMTExpr.h:57
Represents a symbolic expression like &#39;x&#39; + &#39;y&#39;.
A symbol representing data which can be stored in a memory location (region).
Definition: SymExpr.h:117