RetroSearch Browse

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://clang.llvm.org/doxygen/SMTConv_8h_source.html below:

clang: include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h Source File

13#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H 14#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H 19#include "llvm/Support/SMTAPI.h" 27 static inline

llvm::SMTSortRef

mkSort

(llvm::SMTSolverRef &Solver,

28 const QualType

&Ty,

unsigned

BitWidth) {

30 return

Solver->getBoolSort();

33 return

Solver->getFloatSort(BitWidth);

35 return

Solver->getBitvectorSort(BitWidth);

39 static inline

llvm::SMTExprRef

fromUnOp

(llvm::SMTSolverRef &Solver,

41 const

llvm::SMTExprRef &Exp) {

44 return

Solver->mkBVNeg(Exp);

47 return

Solver->mkBVNot(Exp);

50 return

Solver->mkNot(Exp);

54

llvm_unreachable(

"Unimplemented opcode"

);

58 static inline

llvm::SMTExprRef

fromFloatUnOp

(llvm::SMTSolverRef &Solver,

60 const

llvm::SMTExprRef &Exp) {

63 return

Solver->mkFPNeg(Exp);

70

llvm_unreachable(

"Unimplemented opcode"

);

74 static inline

llvm::SMTExprRef

76 const

std::vector<llvm::SMTExprRef> &ASTs) {

77

assert(!ASTs.empty());

79 if

(Op != BO_LAnd && Op != BO_LOr)

80

llvm_unreachable(

"Unimplemented opcode"

);

82

llvm::SMTExprRef res = ASTs.front();

83 for

(std::size_t i = 1; i < ASTs.size(); ++i)

84

res = (Op == BO_LAnd) ? Solver->mkAnd(res, ASTs[i])

85

: Solver->mkOr(res, ASTs[i]);

90 static inline

llvm::SMTExprRef

fromBinOp

(llvm::SMTSolverRef &Solver,

91 const

llvm::SMTExprRef &LHS,

93 const

llvm::SMTExprRef &RHS,

95

assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&

96 "AST's must have the same sort!"

);

101 return

Solver->mkBVMul(LHS, RHS);

104 return

isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS);

107 return

isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS);

111 return

Solver->mkBVAdd(LHS, RHS);

114 return

Solver->mkBVSub(LHS, RHS);

118 return

Solver->mkBVShl(LHS, RHS);

121 return

isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS);

125 return

isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS);

128 return

isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS);

131 return

isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS);

134 return

isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS);

138 return

Solver->mkEqual(LHS, RHS);

142 fromBinOp

(Solver, LHS, BO_EQ, RHS, isSigned));

146 return

Solver->mkBVAnd(LHS, RHS);

149 return

Solver->mkBVXor(LHS, RHS);

152 return

Solver->mkBVOr(LHS, RHS);

156 return

Solver->mkAnd(LHS, RHS);

159 return

Solver->mkOr(LHS, RHS);

163

llvm_unreachable(

"Unimplemented opcode"

);

168 static inline

llvm::SMTExprRef

171 const

llvm::APFloat::fltCategory &RHS) {

176 case

llvm::APFloat::fcInfinity:

177 return

Solver->mkFPIsInfinite(LHS);

179 case

llvm::APFloat::fcNaN:

180 return

Solver->mkFPIsNaN(LHS);

182 case

llvm::APFloat::fcNormal:

183 return

Solver->mkFPIsNormal(LHS);

185 case

llvm::APFloat::fcZero:

186 return

Solver->mkFPIsZero(LHS);

197

llvm_unreachable(

"Unimplemented opcode"

);

202 const

llvm::SMTExprRef &LHS,

204 const

llvm::SMTExprRef &RHS) {

205

assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&

206 "AST's must have the same sort!"

);

211 return

Solver->mkFPMul(LHS, RHS);

214 return

Solver->mkFPDiv(LHS, RHS);

217 return

Solver->mkFPRem(LHS, RHS);

221 return

Solver->mkFPAdd(LHS, RHS);

224 return

Solver->mkFPSub(LHS, RHS);

228 return

Solver->mkFPLt(LHS, RHS);

231 return

Solver->mkFPGt(LHS, RHS);

234 return

Solver->mkFPLe(LHS, RHS);

237 return

Solver->mkFPGe(LHS, RHS);

241 return

Solver->mkFPEqual(LHS, RHS);

250 return fromBinOp

(Solver, LHS, Op, RHS,

false

);

255

llvm_unreachable(

"Unimplemented opcode"

);

260 static inline

llvm::SMTExprRef

fromCast

(llvm::SMTSolverRef &Solver,

261 const

llvm::SMTExprRef &Exp,

264

uint64_t FromBitWidth) {

272

assert(ToBitWidth > 0 &&

"BitWidth must be positive!"

);

273 return

Solver->mkIte(

274

Exp, Solver->mkBitvector(llvm::APSInt(

"1"

), ToBitWidth),

275

Solver->mkBitvector(llvm::APSInt(

"0"

), ToBitWidth));

278 if

(ToBitWidth > FromBitWidth)

280

? Solver->mkBVSignExt(ToBitWidth - FromBitWidth, Exp)

281

: Solver->mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);

283 if

(ToBitWidth < FromBitWidth)

284 return

Solver->mkBVExtract(ToBitWidth - 1, 0, Exp);

291 if

(ToBitWidth != FromBitWidth)

292 return

Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth));

298

llvm::SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);

300

? Solver->mkSBVtoFP(Exp, Sort)

301

: Solver->mkUBVtoFP(Exp, Sort);

306

? Solver->mkFPtoSBV(Exp, ToBitWidth)

307

: Solver->mkFPtoUBV(Exp, ToBitWidth);

309

llvm_unreachable(

"Unsupported explicit type cast!"

);

313 static inline

llvm::APSInt

castAPSInt

(llvm::SMTSolverRef &Solver,

316

uint64_t FromWidth) {

322 static inline

llvm::SMTExprRef

326 const

uint64_t BitWidth = Ctx.getTypeSize(Ty);

329

llvm::raw_svector_ostream

(Str);

331 return

Solver->mkSymbol(Str.c_str(),

mkSort

(Solver, Ty, BitWidth));

335 static inline

llvm::SMTExprRef

getCastExpr

(llvm::SMTSolverRef &Solver,

337 const

llvm::SMTExprRef &Exp,

339 return fromCast

(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,

340

Ctx.getTypeSize(FromTy));

345 static inline

llvm::SMTExprRef

347 const

llvm::SMTExprRef &LHS,

QualType

LTy,

350

llvm::SMTExprRef NewLHS = LHS;

351

llvm::SMTExprRef NewRHS = RHS;

369

*RetTy = Ctx.getPointerDiffType();

389 if

(

const SymIntExpr

*SIE = dyn_cast<SymIntExpr>(BSE)) {

390

llvm::SMTExprRef LHS =

391 getSymExpr

(Solver, Ctx, SIE->getLHS(), &LTy, hasComparison);

392

llvm::APSInt NewRInt;

393

std::tie(NewRInt, RTy) =

fixAPSInt

(Ctx, SIE->getRHS());

394

llvm::SMTExprRef RHS =

395

Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());

396 return getBinExpr

(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);

399 if

(

const IntSymExpr

*ISE = dyn_cast<IntSymExpr>(BSE)) {

400

llvm::APSInt NewLInt;

401

std::tie(NewLInt, LTy) =

fixAPSInt

(Ctx, ISE->getLHS());

402

llvm::SMTExprRef LHS =

403

Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());

404

llvm::SMTExprRef RHS =

405 getSymExpr

(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison);

406 return getBinExpr

(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);

409 if

(

const SymSymExpr

*SSM = dyn_cast<SymSymExpr>(BSE)) {

410

llvm::SMTExprRef LHS =

411 getSymExpr

(Solver, Ctx, SSM->getLHS(), &LTy, hasComparison);

412

llvm::SMTExprRef RHS =

413 getSymExpr

(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison);

414 return getBinExpr

(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);

417

llvm_unreachable(

"Unsupported BinarySymExpr type!"

);

422 static inline

llvm::SMTExprRef

getSymExpr

(llvm::SMTSolverRef &Solver,

425 bool

*hasComparison) {

426 if

(

const SymbolData

*SD = dyn_cast<SymbolData>(Sym)) {

433 if

(

const SymbolCast

*SC = dyn_cast<SymbolCast>(Sym)) {

438

llvm::SMTExprRef Exp =

439 getSymExpr

(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison);

445

*hasComparison =

false

;

449 if

(

const UnarySymExpr

*USE = dyn_cast<UnarySymExpr>(Sym)) {

454

llvm::SMTExprRef OperandExp =

455 getSymExpr

(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison);

456

llvm::SMTExprRef UnaryExp =

459

fromUnOp

(Solver, USE->getOpcode(), OperandExp);

465 if

(Ctx.getTypeSize(OperandTy) != Ctx.getTypeSize(Sym->

getType

())) {

467

*hasComparison =

false

;

473 if

(

const BinarySymExpr

*BSE = dyn_cast<BinarySymExpr>(Sym)) {

474

llvm::SMTExprRef Exp =

482

llvm_unreachable(

"Unsupported SymbolRef type!"

);

489 static inline

llvm::SMTExprRef

getExpr

(llvm::SMTSolverRef &Solver,

492 bool

*hasComparison =

nullptr

) {

494

*hasComparison =

false

;

497 return getSymExpr

(Solver, Ctx, Sym, RetTy, hasComparison);

501 static inline

llvm::SMTExprRef

getZeroExpr

(llvm::SMTSolverRef &Solver,

503 const

llvm::SMTExprRef &Exp,

507

llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));

509

Solver->mkFloat(Zero));

518 return

Assumption ?

fromUnOp

(Solver, UO_LNot, Exp) : Exp;

521

Solver, Exp, Assumption ? BO_EQ : BO_NE,

522

Solver->mkBitvector(llvm::APSInt(

"0"

), Ctx.getTypeSize(Ty)),

526

llvm_unreachable(

"Unsupported type for zero value!"

);

531 static inline

llvm::SMTExprRef

533 const

llvm::APSInt &From,

const

llvm::APSInt &To,

bool

InRange) {

536

llvm::APSInt NewFromInt;

537

std::tie(NewFromInt, FromTy) =

fixAPSInt

(Ctx, From);

538

llvm::SMTExprRef FromExp =

539

Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());

543

llvm::SMTExprRef Exp =

getExpr

(Solver, Ctx, Sym, &SymTy);

547 return getBinExpr

(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,

548

FromExp, FromTy,

nullptr

);

551

llvm::APSInt NewToInt;

552

std::tie(NewToInt, ToTy) =

fixAPSInt

(Ctx, To);

553

llvm::SMTExprRef ToExp =

554

Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());

555

assert(FromTy == ToTy &&

"Range values have different types!"

);

558

llvm::SMTExprRef LHS =

559 getBinExpr

(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,

561

llvm::SMTExprRef RHS =

getBinExpr

(Solver, Ctx, Exp, SymTy,

562

InRange ? BO_LE : BO_GT, ToExp, ToTy,

565 return fromBinOp

(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,

572 const

llvm::APSInt &Int) {

573 return

Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());

577 static inline

std::pair<llvm::APSInt, QualType>

584 if

(Int.getBitWidth() == 1 &&

getAPSIntType

(Ctx, Int).isNull()) {

585

NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));

597

llvm::SMTExprRef &RHS,

QualType

&LTy,

599

assert(!LTy.

isNull

() && !RTy.

isNull

() &&

"Input type is null!"

);

605

SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>(

606

Solver, Ctx, LHS, LTy, RHS, RTy);

611

SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>(

612

Solver, Ctx, LHS, LTy, RHS, RTy);

622

uint64_t LBitWidth = Ctx.getTypeSize(LTy);

623

uint64_t RBitWidth = Ctx.getTypeSize(RTy);

632

LHS =

fromCast

(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);

635

RHS =

fromCast

(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);

645

assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&

646 "Pointer types have different bitwidths!"

);

670 template

typename T

(*doCast)(llvm::SMTSolverRef &Solver,

const T

675

uint64_t LBitWidth = Ctx.getTypeSize(LTy);

676

uint64_t RBitWidth = Ctx.getTypeSize(RTy);

678

assert(!LTy.

isNull

() && !RTy.

isNull

() &&

"Input type is null!"

);

681 if

(Ctx.isPromotableIntegerType(LTy)) {

682 QualType

NewTy = Ctx.getPromotedIntegerType(LTy);

683

uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);

684

LHS = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth);

686

LBitWidth = NewBitWidth;

688 if

(Ctx.isPromotableIntegerType(RTy)) {

689 QualType

NewTy = Ctx.getPromotedIntegerType(RTy);

690

uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);

691

RHS = (*doCast)(Solver, RHS, NewTy, NewBitWidth, RTy, RBitWidth);

693

RBitWidth = NewBitWidth;

704 int

order = Ctx.getIntegerTypeOrder(LTy, RTy);

705 if

(isLSignedTy == isRSignedTy) {

708

RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);

711

LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);

714

}

else if

(order != (isLSignedTy ? 1 : -1)) {

718

RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);

721

LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);

724

}

else if

(LBitWidth != RBitWidth) {

729

RHS = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);

732

LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);

741

Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);

742

RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);

744

LHS = (doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);

752 template

typename T

(*doCast)(llvm::SMTSolverRef &Solver,

const T

757

uint64_t LBitWidth = Ctx.getTypeSize(LTy);

758

uint64_t RBitWidth = Ctx.getTypeSize(RTy);

762

LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);

764

LBitWidth = RBitWidth;

767

RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);

769

RBitWidth = LBitWidth;

778 int

order = Ctx.getFloatingTypeOrder(LTy, RTy);

780

RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);

782

}

else if

(order == 0) {

783

LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);

786

llvm_unreachable(

"Unsupported floating-point type cast!"

);

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

bool isComparisonOp() const

A (possibly-)qualified type.

bool isNull() const

Return true if this QualType doesn't point to a type yet.

QualType getCanonicalType() const

bool isBlockPointerType() 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 isVoidPointerType() const

bool isArithmeticType() const

bool isReferenceType() const

bool isIntegralOrEnumerationType() const

Determine whether this type is an integral or enumeration type.

bool isObjCObjectPointerType() const

bool isRealFloatingType() const

Floating point categories.

bool isAnyPointerType() const

bool isNullPtrType() const

A record of the "type" of an APSInt, used for conversions.

llvm::APSInt convert(const llvm::APSInt &Value) const LLVM_READONLY

Convert and return a new APSInt with the given value, but this type's bit width and signedness.

Template implementation for all binary symbolic expressions.

Represents a symbolic expression involving a binary operator.

BinaryOperator::Opcode getOpcode() const

static llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver, const QualType &Ty, unsigned BitWidth)

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

Construct an SMTSolverRef from a floating-point binary operator.

static QualType getAPSIntType(ASTContext &Ctx, const llvm::APSInt &Int)

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

static void doIntTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType &LTy, T &RHS, QualType &RTy)

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

static llvm::SMTExprRef fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op, const std::vector< llvm::SMTExprRef > &ASTs)

Construct an SMTSolverRef from a n-ary binary operator.

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

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

static void doTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, llvm::SMTExprRef &LHS, llvm::SMTExprRef &RHS, QualType &LTy, QualType &RTy)

static llvm::SMTExprRef fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::APFloat::fltCategory &RHS)

Construct an SMTSolverRef from a special floating-point binary operator.

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

Construct an SMTSolverRef from a SymbolData.

static void doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType &LTy, T &RHS, QualType &RTy)

static llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const BinarySymExpr *BSE, bool *hasComparison, QualType *RetTy)

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 llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType FromTy, QualType ToTy)

static llvm::SMTExprRef getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &LHS, QualType LTy, BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, QualType RTy, QualType *RetTy)

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

static llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &Exp, QualType ToTy, uint64_t ToBitWidth, QualType FromTy, uint64_t FromBitWidth)

Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy, and their bit widths.

static llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver, const llvm::APSInt &V, QualType ToTy, uint64_t ToWidth, QualType FromTy, uint64_t FromWidth)

static llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, const UnaryOperator::Opcode Op, const llvm::SMTExprRef &Exp)

Constructs an SMTSolverRef from a floating-point unary operator.

static llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, const UnaryOperator::Opcode Op, const llvm::SMTExprRef &Exp)

Constructs an SMTSolverRef from an unary operator.

virtual QualType getType() const =0

SymbolID getSymbolID() const

Get a unique identifier for this symbol.

Represents a cast expression.

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

virtual StringRef getKindStr() const =0

Get a string representation of the kind of the region.

Represents a symbolic expression involving a unary operator.

@ OS

Indicates that the tracking object is a descendant of a referenced-counted OSObject,...

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

const FunctionProtoType * T

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4