SMTConstraintManager.h Source File (original) (raw)

14#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H

15#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H

22#include

24typedef llvm::ImmutableSet<

25 std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>

30namespace ento {

33 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();

35public:

39 Solver->setBoolParam("model", true);

40 Solver->setUnsignedParam("timeout", 15000 );

41 }

49 bool Assumption) override {

53 bool hasComparison;

55 llvm::SMTExprRef Exp =

62 State, Sym,

65 return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));

66 }

69 const llvm::APSInt &From,

70 const llvm::APSInt &To,

71 bool InRange) override {

75 }

78 bool Assumption) override {

80 return State;

81 }

92 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);

93 llvm::SMTExprRef Exp =

97 llvm::SMTExprRef NotExp =

102

103

105 return true;

106

107

109 return false;

110

111

113 }

114

119

120 if (const SymbolData *SD = dyn_cast(Sym)) {

123 llvm::APSInt Value(Ctx.getTypeSize(Ty),

125

126

127

128

129

131

132 Solver->reset();

134

135

136 std::optional isSat = Solver->check();

137 if (!isSat || !*isSat)

138 return nullptr;

139

140

141 if (!Solver->getInterpretation(Exp, Value))

142 return nullptr;

143

144

146 Solver, Exp, BO_NE,

148 : Solver->mkBitvector(Value, Value.getBitWidth()),

149 false);

150

151 Solver->addConstraint(NotExp);

152

153 std::optional isNotSat = Solver->check();

154 if (!isNotSat || *isNotSat)

155 return nullptr;

156

157

158 return BVF.getValue(Value).get();

159 }

160

161 if (const SymbolCast *SC = dyn_cast(Sym)) {

162 SymbolRef CastSym = SC->getOperand();

163 QualType CastTy = SC->getType();

164

166 return nullptr;

167

168 const llvm::APSInt *Value;

170 return nullptr;

172 }

173

174 if (const BinarySymExpr *BSE = dyn_cast(Sym)) {

175 const llvm::APSInt *LHS, *RHS;

176 if (const SymIntExpr *SIE = dyn_cast(BSE)) {

177 LHS = getSymVal(State, SIE->getLHS());

178 RHS = SIE->getRHS().get();

179 } else if (const IntSymExpr *ISE = dyn_cast(BSE)) {

180 LHS = ISE->getLHS().get();

181 RHS = getSymVal(State, ISE->getRHS());

182 } else if (const SymSymExpr *SSM = dyn_cast(BSE)) {

183

184 LHS = getSymVal(State, SSM->getLHS());

185 RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;

186 } else {

187 llvm_unreachable("Unsupported binary expression to get symbol value!");

188 }

189

190 if (!LHS || !RHS)

191 return nullptr;

192

193 llvm::APSInt ConvertedLHS, ConvertedRHS;

197 SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(

198 Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);

199 std::optional Res =

200 BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);

201 return Res ? Res.value().get() : nullptr;

202 }

203

204 llvm_unreachable("Unsupported expression to get symbol value!");

205 }

206

209 auto CZ = State->get();

210 auto &CZFactory = State->get_context();

211

212 for (const auto &Entry : CZ) {

213 if (SymReaper.isDead(Entry.first))

214 CZ = CZFactory.remove(CZ, Entry);

215 }

216

217 return State->set(CZ);

218 }

219

221 unsigned int Space = 0, bool IsDot = false) const override {

223

224 Indent(Out, Space, IsDot) << "\"constraints\": ";

225 if (Constraints.isEmpty()) {

226 Out << "null," << NL;

227 return;

228 }

229

230 ++Space;

231 Out << '[' << NL;

232 for (ConstraintSMTType::iterator I = Constraints.begin();

233 I != Constraints.end(); ++I) {

234 Indent(Out, Space, IsDot)

235 << "{ \"symbol\": \"" << I->first << "\", \"range\": \"";

236 I->second->print(Out);

237 Out << "\" }";

238

239 if (std::next(I) != Constraints.end())

240 Out << ',';

241 Out << NL;

242 }

243

244 --Space;

245 Indent(Out, Space, IsDot) << "],";

246 }

247

250 return S1->get() == S2->get();

251 }

252

255

256 std::optionalnonloc::SymbolVal SymVal = X.getAs<nonloc::SymbolVal>();

257 if (!SymVal)

258 return true;

259

260 const SymExpr *Sym = SymVal->getSymbol();

262

263

265 return false;

266

267

271 return false;

272

274 return Solver->isFPSupported();

275

276 if (isa(Sym))

277 return true;

278

280

281 if (const SymbolCast *SC = dyn_cast(Sym))

283

284

285 if (isa(Sym)) {

286 return false;

287 }

288

289 if (const BinarySymExpr *BSE = dyn_cast(Sym)) {

290 if (const SymIntExpr *SIE = dyn_cast(BSE))

292

293 if (const IntSymExpr *ISE = dyn_cast(BSE))

295

296 if (const SymSymExpr *SSE = dyn_cast(BSE))

299 }

300

301 llvm_unreachable("Unsupported expression to reason about!");

302 }

303

304

305 LLVM_DUMP_METHOD void dump() const { Solver->dump(); }

306

307protected:

308

310 const llvm::SMTExprRef &Exp) {

311

312 if (checkModel(State, Sym, Exp).isConstrainedTrue())

313 return State->add(std::make_pair(Sym, Exp));

314

315 return nullptr;

316 }

317

318

319

321

322 auto CZ = State->get();

323 auto I = CZ.begin(), IE = CZ.end();

324

325

326 if (I != IE) {

327 std::vectorllvm::SMTExprRef ASTs;

328

329 llvm::SMTExprRef Constraint = I++->second;

330 while (I != IE) {

331 Constraint = Solver->mkAnd(Constraint, I++->second);

332 }

333

334 Solver->addConstraint(Constraint);

335 }

336 }

337

338

340 const llvm::SMTExprRef &Exp) const {

342 State->add(std::make_pair(Sym, Exp));

343

344 llvm::FoldingSetNodeID ID;

345 NewState->get().Profile(ID);

346

347 unsigned hash = ID.ComputeHash();

348 auto I = Cached.find(hash);

349 if (I != Cached.end())

350 return I->second;

351

352 Solver->reset();

354

355 std::optional res = Solver->check();

356 if (!res)

358 else

360

362 }

363

364

365

366 mutable llvm::DenseMap<unsigned, ConditionTruthVal> Cached;

367};

368

369}

370}

371

372#endif

#define REGISTER_TRAIT_WITH_PROGRAMSTATE(Name, Type)

Declares a program state trait for type Type called Name, and introduce a type named NameTy.

llvm::ImmutableSet< std::pair< clang::ento::SymbolRef, const llvm::SMTExpr * > > ConstraintSMTType

Holds long-lived AST nodes (such as types and decls) that can be referred to throughout the semantic ...

const TargetInfo & getTargetInfo() const

A (possibly-)qualified type.

Exposes information about the current target.

const llvm::fltSemantics & getLongDoubleFormat() const

bool isBooleanType() const

bool isSignedIntegerOrEnumerationType() const

Determines whether this is an integer type that is signed or an enumeration types whose underlying ty...

bool isComplexType() const

isComplexType() does not include complex integers (a GCC extension).

bool isSpecificBuiltinType(unsigned K) const

Test for a particular builtin type.

bool isComplexIntegerType() const

bool isRealFloatingType() const

Floating point categories.

LLVM_ATTRIBUTE_RETURNS_NONNULL const APSInt * get() const

std::optional< APSIntPtr > evalAPSInt(BinaryOperator::Opcode Op, const llvm::APSInt &V1, const llvm::APSInt &V2)

ASTContext & getContext() const

APSIntPtr Convert(const llvm::APSInt &To, const llvm::APSInt &From)

Convert - Create a new persistent APSInt with the same value as 'From' but with the bitwidth and sign...

Template implementation for all binary symbolic expressions.

Represents a symbolic expression involving a binary operator.

bool isConstrainedFalse() const

Return true if the constraint is perfectly constrained to 'false'.

bool isConstrainedTrue() const

Return true if the constraint is perfectly constrained to 'true'.

SMTConstraintManager(clang::ento::ExprEngine *EE, clang::ento::SValBuilder &SB)

virtual void addStateConstraints(ProgramStateRef State) const

Given a program state, construct the logical conjunction and add it to the solver.

bool canReasonAbout(SVal X) const override

canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values.

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...

LLVM_DUMP_METHOD void dump() const

Dumps SMT formula.

ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym, const llvm::SMTExprRef &Exp) const

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.

ProgramStateRef removeDeadBindings(ProgramStateRef State, SymbolReaper &SymReaper) override

Scan all symbols referenced by the constraints.

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 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...

llvm::DenseMap< unsigned, ConditionTruthVal > Cached

virtual ~SMTConstraintManager()=default

virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym, const llvm::SMTExprRef &Exp)

void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL="\n", unsigned int Space=0, bool IsDot=false) const override

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 ...

bool haveEqualConstraints(ProgramStateRef S1, ProgramStateRef S2) const override

static llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType Ty, bool Assumption)

static llvm::SMTExprRef getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)

static llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy=nullptr, bool *hasComparison=nullptr)

static llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym)

Construct an SMTSolverRef from a SymbolData.

static llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, bool isSigned)

Construct an SMTSolverRef from a binary operator.

static std::pair< llvm::APSInt, QualType > fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int)

DefinedSVal makeSymbolVal(SymbolRef Sym)

Make an SVal that represents the given symbol.

SVal - This represents a symbolic expression, which can be either an L-value or an R-value.

SValBuilder & getSValBuilder() const

BasicValueFactory & getBasicVals() const

virtual QualType getType() const =0

Represents a cast expression.

A symbol representing data which can be stored in a memory location (region).

A class responsible for cleaning up unused symbols.

bool isDead(SymbolRef sym)

Returns whether or not a symbol has been confirmed dead.

Represents symbolic expression that isn't a location.

Defines the clang::TargetInfo interface.

The JSON file list parser is used to communicate input to InstallAPI.