1 //== SMTConstraintManager.cpp -----------------------------------*- 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 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
11 #include "clang/Basic/TargetInfo.h"
12 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
13 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
14 
15 using namespace clang;
16 using namespace ento;
17 
18 ProgramStateRef SMTConstraintManager::assumeSym(ProgramStateRef State,
19                                                 SymbolRef Sym,
20                                                 bool Assumption) {
21   ASTContext &Ctx = getBasicVals().getContext();
22 
23   QualType RetTy;
24   bool hasComparison;
25 
26   SMTExprRef Exp = Solver->getExpr(Ctx, Sym, &RetTy, &hasComparison);
27 
28   // Create zero comparison for implicit boolean cast, with reversed assumption
29   if (!hasComparison && !RetTy->isBooleanType())
30     return assumeExpr(State, Sym,
31                       Solver->getZeroExpr(Ctx, Exp, RetTy, !Assumption));
32 
33   return assumeExpr(State, Sym,
34                     Assumption ? Exp : Solver->fromUnOp(UO_LNot, Exp));
35 }
36 
37 ProgramStateRef SMTConstraintManager::assumeSymInclusiveRange(
38     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
39     const llvm::APSInt &To, bool InRange) {
40   ASTContext &Ctx = getBasicVals().getContext();
41   return assumeExpr(State, Sym,
42                     Solver->getRangeExpr(Ctx, Sym, From, To, InRange));
43 }
44 
45 ProgramStateRef
46 SMTConstraintManager::assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
47                                            bool Assumption) {
48   // Skip anything that is unsupported
49   return State;
50 }
51 
52 ConditionTruthVal SMTConstraintManager::checkNull(ProgramStateRef State,
53                                                   SymbolRef Sym) {
54   ASTContext &Ctx = getBasicVals().getContext();
55 
56   QualType RetTy;
57   // The expression may be casted, so we cannot call getZ3DataExpr() directly
58   SMTExprRef VarExp = Solver->getExpr(Ctx, Sym, &RetTy);
59   SMTExprRef Exp = Solver->getZeroExpr(Ctx, VarExp, RetTy, true);
60 
61   // Negate the constraint
62   SMTExprRef NotExp = Solver->getZeroExpr(Ctx, VarExp, RetTy, false);
63 
64   Solver->reset();
65   addStateConstraints(State);
66 
67   Solver->push();
68   Solver->addConstraint(Exp);
69   ConditionTruthVal isSat = Solver->check();
70 
71   Solver->pop();
72   Solver->addConstraint(NotExp);
73   ConditionTruthVal isNotSat = Solver->check();
74 
75   // Zero is the only possible solution
76   if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
77     return true;
78 
79   // Zero is not a solution
80   if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
81     return false;
82 
83   // Zero may be a solution
84   return ConditionTruthVal();
85 }
86 
87 const llvm::APSInt *SMTConstraintManager::getSymVal(ProgramStateRef State,
88                                                     SymbolRef Sym) const {
89   BasicValueFactory &BVF = getBasicVals();
90   ASTContext &Ctx = BVF.getContext();
91 
92   if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
93     QualType Ty = Sym->getType();
94     assert(!Ty->isRealFloatingType());
95     llvm::APSInt Value(Ctx.getTypeSize(Ty),
96                        !Ty->isSignedIntegerOrEnumerationType());
97 
98     SMTExprRef Exp = Solver->getDataExpr(Ctx, SD->getSymbolID(), Ty);
99 
100     Solver->reset();
101     addStateConstraints(State);
102 
103     // Constraints are unsatisfiable
104     ConditionTruthVal isSat = Solver->check();
105     if (!isSat.isConstrainedTrue())
106       return nullptr;
107 
108     // Model does not assign interpretation
109     if (!Solver->getInterpretation(Exp, Value))
110       return nullptr;
111 
112     // A value has been obtained, check if it is the only value
113     SMTExprRef NotExp = Solver->fromBinOp(
114         Exp, BO_NE,
115         Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue())
116                             : Solver->fromAPSInt(Value),
117         false);
118 
119     Solver->addConstraint(NotExp);
120 
121     ConditionTruthVal isNotSat = Solver->check();
122     if (isNotSat.isConstrainedTrue())
123       return nullptr;
124 
125     // This is the only solution, store it
126     return &BVF.getValue(Value);
127   }
128 
129   if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
130     SymbolRef CastSym = SC->getOperand();
131     QualType CastTy = SC->getType();
132     // Skip the void type
133     if (CastTy->isVoidType())
134       return nullptr;
135 
136     const llvm::APSInt *Value;
137     if (!(Value = getSymVal(State, CastSym)))
138       return nullptr;
139     return &BVF.Convert(SC->getType(), *Value);
140   }
141 
142   if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
143     const llvm::APSInt *LHS, *RHS;
144     if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
145       LHS = getSymVal(State, SIE->getLHS());
146       RHS = &SIE->getRHS();
147     } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
148       LHS = &ISE->getLHS();
149       RHS = getSymVal(State, ISE->getRHS());
150     } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
151       // Early termination to avoid expensive call
152       LHS = getSymVal(State, SSM->getLHS());
153       RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
154     } else {
155       llvm_unreachable("Unsupported binary expression to get symbol value!");
156     }
157 
158     if (!LHS || !RHS)
159       return nullptr;
160 
161     llvm::APSInt ConvertedLHS, ConvertedRHS;
162     QualType LTy, RTy;
163     std::tie(ConvertedLHS, LTy) = Solver->fixAPSInt(Ctx, *LHS);
164     std::tie(ConvertedRHS, RTy) = Solver->fixAPSInt(Ctx, *RHS);
165     Solver->doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>(
166         Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
167     return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
168   }
169 
170   llvm_unreachable("Unsupported expression to get symbol value!");
171 }
172 
173 ConditionTruthVal
174 SMTConstraintManager::checkModel(ProgramStateRef State,
175                                  const SMTExprRef &Exp) const {
176   Solver->reset();
177   Solver->addConstraint(Exp);
178   addStateConstraints(State);
179   return Solver->check();
180 }
181