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