SMTAPI.h Source File (original) (raw)

14#ifndef LLVM_SUPPORT_SMTAPI_H

15#define LLVM_SUPPORT_SMTAPI_H

22#include

24namespace llvm {

28public:

64 Other.Profile(ID2);

65 return ID1 < ID2;

66 }

69 return LHS.equal_to(RHS);

70 }

74#if !defined(NDEBUG) || defined(LLVM_ENABLE_DUMP)

76#endif

78protected:

97};

101

102

104public:

107

111 Other.Profile(ID2);

112 return ID1 < ID2;

113 }

114

116

118 return LHS.equal_to(RHS);

119 }

120

122

123#if !defined(NDEBUG) || defined(LLVM_ENABLE_DUMP)

125#endif

126

127protected:

128

129

131};

132

134public:

137

140

142

143#if !defined(NDEBUG) || defined(LLVM_ENABLE_DUMP)

145#endif

146};

147

148

150

151

152

153

154

155

157public:

160

161#if !defined(NDEBUG) || defined(LLVM_ENABLE_DUMP)

163#endif

164

165

168 case 16:

170 case 32:

172 case 64:

174 case 128:

176 default:;

177 }

179 }

180

181

183

184

186

187

189

190

192

193

195

196

198

199

201

202

204

205

207

208

210

211

213

214

216

217

219

220

222

223

225

226

228

229

231

232

234

235

237

238

240

241

243

244

246

247

249

250

252

253

255

256

258

259

261

262

264

265

267

268

270

271

273

274

276

277

279

280

282

283

285

286

289

290

292

293

295

296

299

300

303

304

305

309

310

311

314

315

316

319

320

321

325

326

327

330

331

332

334

335

336

340

341

342

345

346

348

349

351

352

354

355

357

358

360

361

363

364

366

367

369

370

372

373

375

376

378

379

381

382

384

385

387

388

391

392

393

395

396

397

400

401

402

405

406

407

409

410

411

413

414

416

417

419

420

422 bool isUnsigned) = 0;

423

424

426

427

429

430

432

433

435

436

438

439

442

443

444 virtual std::optional check() const = 0;

445

446

448

449

450 virtual void pop(unsigned NumStates = 1) = 0;

451

452

454

455

457

459

460

463

464 virtual std::unique_ptr getStatistics() const = 0;

465};

466

467

469

470

472

473}

474

475#endif

assert(UImm &&(UImm !=~static_cast< T >(0)) &&"Invalid immediate!")

This file declares a class to represent arbitrary precision floating point values and provide a varie...

This file implements the APSInt class, which is a simple class that represents an arbitrary sized int...

#define LLVM_DUMP_METHOD

Mark debug helper function definitions like dump() that should not be stripped from debug builds.

static bool isSigned(unsigned int Opcode)

This file defines a hash set that can be used to remove duplication of nodes in a graph.

const SmallVectorImpl< MachineOperand > & Cond

An arbitrary precision integer that knows its signedness.

FoldingSetNodeID - This class is used to gather all the unique data bits of a node.

Generic base class for SMT exprs.

Definition SMTAPI.h:103

virtual bool equal_to(SMTExpr const &other) const =0

Query the SMT solver and returns true if two sorts are equal (same kind and bit width).

bool operator<(const SMTExpr &Other) const

Definition SMTAPI.h:108

virtual void Profile(llvm::FoldingSetNodeID &ID) const =0

friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS)

Definition SMTAPI.h:117

virtual ~SMTExpr()=default

LLVM_DUMP_METHOD void dump() const

virtual void print(raw_ostream &OS) const =0

virtual ~SMTSolverStatistics()=default

SMTSolverStatistics()=default

virtual unsigned getUnsigned(llvm::StringRef) const =0

LLVM_DUMP_METHOD void dump() const

virtual double getDouble(llvm::StringRef) const =0

virtual void print(raw_ostream &OS) const =0

virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector unsigned greater-equal-than operation.

virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector or operation.

virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float)=0

Given an expression extract the value of this operand in the model.

virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T, const SMTExprRef &F)=0

Creates a boolean ite operation.

virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector unsigned less-equal-than operation.

virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp)=0

Creates a bitvector negation operation.

virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a floating-point less-than-or-equal operation.

virtual SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp)=0

Creates a predicate that checks for overflow in a bitvector negation operation.

virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp)=0

Creates a floating-point negation operation.

virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector signed greater-than operation.

virtual ~SMTSolver()=default

virtual bool isFPSupported()=0

Checks if the solver supports floating-points.

virtual SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a predicate that checks for underflow in a signed bitvector addition operation.

virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a floating-point greater-than-or-equal operation.

virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector multiplication operation.

virtual void push()=0

Push the current solver state.

virtual SMTSortRef getBitvectorSort(const unsigned BitWidth)=0

virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector logical shift right operation.

virtual SMTSortRef getFloat128Sort()=0

virtual SMTSortRef getSort(const SMTExprRef &AST)=0

virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp)=0

Creates a floating-point isNormal operation.

virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a floating-point multiplication operation.

virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector unsigned less-than operation.

virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a floating-point greater-than operation.

virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp)=0

Creates a floating-point isInfinite operation.

virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a floating-point division operation.

virtual SMTSortRef getFloat32Sort()=0

virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector subtraction operation.

virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector unsigned greater-than operation.

virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a floating-point less-than operation.

virtual void setUnsignedParam(StringRef Key, unsigned Value)=0

virtual SMTSortRef getFloat16Sort()=0

virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector addition operation.

virtual SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0

Creates a predicate that checks for overflow in a bitvector multiplication operation.

virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector signed less-than operation.

virtual SMTExprRef mkBoolean(const bool b)=0

Constructs an SMTExprRef from a boolean.

virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp)=0

Creates a bitvector zero extension operation.

virtual void pop(unsigned NumStates=1)=0

Pop the previous solver state.

virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector and operation.

virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To)=0

Creates a floating-point conversion from unsigned bitvector to floatint-point operation.

virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp)=0

Creates a floating-point isNaN operation.

virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low, const SMTExprRef &Exp)=0

Creates a bitvector extract operation.

virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a floating-point remainder operation.

virtual SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a predicate that checks for overflow in a signed bitvector subtraction operation.

virtual SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0

Creates a predicate that checks for overflow in a bitvector addition operation.

virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector xor operation.

virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a boolean and operation.

virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a floating-point subtraction operation.

virtual SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0

Creates a predicate that checks for underflow in a bitvector subtraction operation.

virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort)=0

Creates a new symbol, given a name and a sort.

virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector unsigned modulus operation.

virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To)=0

Creates a floating-point conversion from signed bitvector to floatint-point operation.

virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a boolean or operation.

virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp)=0

Creates a bitvector sign extension operation.

virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To)=0

Creates a floating-point conversion from floatint-point to floating-point operation.

virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector arithmetic shift right operation.

virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, bool isUnsigned)=0

virtual void reset()=0

Reset the solver and remove all constraints.

virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp)=0

Creates a floating-point isZero operation.

virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector logical shift left operation.

virtual void print(raw_ostream &OS) const =0

virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int)=0

Given an expression, extract the value of this operand in the model.

virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector signed division operation.

virtual SMTExprRef mkNot(const SMTExprRef &Exp)=0

Creates a boolean not operation.

virtual bool getBoolean(const SMTExprRef &Exp)=0

virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a boolean equality operation.

LLVM_DUMP_METHOD void dump() const

virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector concat operation.

virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth)=0

Creates a floating-point conversion from floatint-point to unsigned bitvector operation.

virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector signed modulus operation.

virtual SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a predicate that checks for underflow in a signed bitvector multiplication operation.

virtual SMTSortRef getFloat64Sort()=0

virtual std::unique_ptr< SMTSolverStatistics > getStatistics() const =0

virtual void setBoolParam(StringRef Key, bool Value)=0

Sets the requested option.

virtual std::optional< bool > check() const =0

Check if the constraints are satisfiable.

virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector unsigned division operation.

virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth)=0

Constructs an SMTExprRef from an APSInt and its bit width.

virtual SMTSortRef getBoolSort()=0

SMTSortRef getFloatSort(unsigned BitWidth)

Definition SMTAPI.h:166

virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a floating-point addition operation.

virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a floating-point equality operation.

virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth)=0

Creates a floating-point conversion from floatint-point to signed bitvector operation.

virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector signed less-equal-than operation.

virtual void addConstraint(const SMTExprRef &Exp) const =0

Given a constraint, adds it to the solver.

virtual SMTExprRef getFloatRoundingMode()=0

virtual SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a predicate that checks for overflow in a signed bitvector division/modulus operation.

virtual SMTExprRef mkFloat(const llvm::APFloat Float)=0

Constructs an SMTExprRef from a finite APFloat.

virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS)=0

Creates a bitvector signed greater-equal-than operation.

virtual SMTExprRef mkBVNot(const SMTExprRef &Exp)=0

Creates a bitvector not operation.

Generic base class for SMT sorts.

Definition SMTAPI.h:27

virtual bool isBitvectorSortImpl() const =0

Query the SMT solver and checks if a sort is bitvector.

bool operator<(const SMTSort &Other) const

Definition SMTAPI.h:61

virtual void print(raw_ostream &OS) const =0

virtual bool isBitvectorSort() const

Returns true if the sort is a bitvector, calls isBitvectorSortImpl().

Definition SMTAPI.h:33

virtual unsigned getFloatSortSizeImpl() const =0

Query the SMT solver and returns the sort bit width.

virtual bool equal_to(SMTSort const &other) const =0

Query the SMT solver and returns true if two sorts are equal (same kind and bit width).

virtual bool isFloatSort() const

Returns true if the sort is a floating-point, calls isFloatSortImpl().

Definition SMTAPI.h:36

virtual unsigned getFloatSortSize() const

Returns the floating-point size, fails if the sort is not a floating-point Calls getFloatSortSizeImpl...

Definition SMTAPI.h:52

virtual unsigned getBitvectorSortSize() const

Returns the bitvector size, fails if the sort is not a bitvector Calls getBitvectorSortSizeImpl().

Definition SMTAPI.h:43

virtual ~SMTSort()=default

friend bool operator==(SMTSort const &LHS, SMTSort const &RHS)

Definition SMTAPI.h:68

virtual void Profile(llvm::FoldingSetNodeID &ID) const =0

virtual bool isFloatSortImpl() const =0

Query the SMT solver and checks if a sort is floating-point.

virtual bool isBooleanSort() const

Returns true if the sort is a boolean, calls isBooleanSortImpl().

Definition SMTAPI.h:39

LLVM_DUMP_METHOD void dump() const

virtual bool isBooleanSortImpl() const =0

Query the SMT solver and checks if a sort is boolean.

virtual unsigned getBitvectorSortSizeImpl() const =0

Query the SMT solver and returns the sort bit width.

StringRef - Represent a constant reference to a string, i.e.

LLVM Value Representation.

This class implements an extremely fast bulk output stream that can only output to a stream.

#define llvm_unreachable(msg)

Marks that the current location is not supposed to be reachable.

unsigned ID

LLVM IR allows to use arbitrary numbers as calling convention identifiers.

This is an optimization pass for GlobalISel generic memory operations.

@ Low

Lower the current thread's priority such that it does not affect foreground tasks significantly.

const SMTExpr * SMTExprRef

Shared pointer for SMTExprs, used by SMTSolver API.

Definition SMTAPI.h:149

std::shared_ptr< SMTSolver > SMTSolverRef

Shared pointer for SMTSolvers.

Definition SMTAPI.h:468

LLVM_ATTRIBUTE_VISIBILITY_DEFAULT AnalysisKey InnerAnalysisManagerProxy< AnalysisManagerT, IRUnitT, ExtraArgTs... >::Key

constexpr unsigned BitWidth

const SMTSort * SMTSortRef

Shared pointer for SMTSorts, used by SMTSolver API.

Definition SMTAPI.h:100

LLVM_ABI SMTSolverRef CreateZ3Solver()

Convenience method to create and Z3Solver object.