#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"

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

static llvm::SMTExprRef	fromUnOp (llvm::SMTSolverRef &Solver, const UnaryOperator::Opcode Op, const llvm::SMTExprRef &Exp)
	Constructs an SMTSolverRef from an unary operator.

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	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	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	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	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 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	fromData (llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym)
	Construct an SMTSolverRef from a SymbolData.

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 llvm::SMTExprRef	getSymBinExpr (llvm::SMTSolverRef &Solver, ASTContext &Ctx, const BinarySymExpr BSE, bool hasComparison, QualType *RetTy)

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 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 QualType	getAPSIntType (ASTContext &Ctx, const llvm::APSInt &Int)

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

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

template<typename T , T(*)(llvm::SMTSolverRef &Solver, const T &, QualType, uint64_t, QualType, uint64_t) doCast>
static void	doIntTypeConversion (llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType &LTy, T &RHS, QualType &RTy)

template<typename T , T(*)(llvm::SMTSolverRef &Solver, const T &, QualType, uint64_t, QualType, uint64_t) doCast>
static void	doFloatTypeConversion (llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType &LTy, T &RHS, QualType &RTy)

Detailed Description

Definition at line 24 of file SMTConv.h.

Member Function Documentation

◆ castAPSInt()

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

inlinestatic

Definition at line 313 of file SMTConv.h.

References clang::ento::APSIntType::convert(), clang::Type::isSignedIntegerOrEnumerationType(), and V.

◆ doFloatTypeConversion()

template<typename T , T(*)(llvm::SMTSolverRef &Solver, const T &, QualType, uint64_t, QualType, uint64_t) doCast>

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

inlinestatic

Definition at line 755 of file SMTConv.h.

References clang::ASTContext::getFloatingTypeOrder(), clang::ASTContext::getTypeSize(), and clang::Type::isRealFloatingType().

◆ doIntTypeConversion()

template<typename T , T(*)(llvm::SMTSolverRef &Solver, const T &, QualType, uint64_t, QualType, uint64_t) doCast>

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

inlinestatic

Definition at line 672 of file SMTConv.h.

References clang::ASTContext::getCorrespondingUnsignedType(), clang::ASTContext::getIntegerTypeOrder(), clang::ASTContext::getPromotedIntegerType(), clang::ASTContext::getTypeSize(), clang::QualType::isNull(), clang::ASTContext::isPromotableIntegerType(), and clang::Type::isSignedIntegerOrEnumerationType().

◆ doTypeConversion()

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

inlinestatic

Definition at line 595 of file SMTConv.h.

References fromCast(), clang::QualType::getCanonicalType(), clang::ASTContext::getTypeSize(), clang::Type::isAnyPointerType(), clang::Type::isArithmeticType(), clang::Type::isBlockPointerType(), clang::Type::isIntegralOrEnumerationType(), clang::QualType::isNull(), clang::Type::isNullPtrType(), clang::Type::isObjCObjectPointerType(), clang::Type::isRealFloatingType(), clang::Type::isReferenceType(), and clang::Type::isVoidPointerType().

Referenced by getBinExpr().

◆ fixAPSInt()

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

inlinestatic

Definition at line 578 of file SMTConv.h.

References clang::ASTContext::BoolTy, getAPSIntType(), and clang::ASTContext::getTypeSize().

Referenced by getRangeExpr(), getSymBinExpr(), and clang::ento::SMTConstraintManager::getSymVal().

◆ fromBinOp()

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

inlinestatic

Construct an SMTSolverRef from a binary operator.

Definition at line 90 of file SMTConv.h.

References fromBinOp(), and fromUnOp().

Referenced by fromBinOp(), fromFloatBinOp(), getBinExpr(), getRangeExpr(), clang::ento::SMTConstraintManager::getSymVal(), and getZeroExpr().

◆ fromCast()

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

inlinestatic

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

Definition at line 260 of file SMTConv.h.

References clang::Type::isAnyPointerType(), clang::Type::isBlockPointerType(), clang::Type::isBooleanType(), clang::Type::isIntegralOrEnumerationType(), clang::Type::isRealFloatingType(), clang::Type::isReferenceType(), and clang::Type::isSignedIntegerOrEnumerationType().

Referenced by doTypeConversion(), and getCastExpr().

◆ fromData()

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

inlinestatic

Construct an SMTSolverRef from a SymbolData.

Definition at line 323 of file SMTConv.h.

References clang::ento::SymbolData::getKindStr(), clang::ento::SymbolData::getSymbolID(), clang::ento::SymExpr::getType(), clang::ASTContext::getTypeSize(), ID, mkSort(), and clang::ento::OS.

Referenced by getSymExpr(), and clang::ento::SMTConstraintManager::getSymVal().

◆ fromFloatBinOp()

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

inlinestatic

Construct an SMTSolverRef from a floating-point binary operator.

Definition at line 201 of file SMTConv.h.

References fromBinOp(), fromFloatBinOp(), and fromFloatUnOp().

Referenced by fromFloatBinOp(), getBinExpr(), and getZeroExpr().

◆ fromFloatSpecialBinOp()

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

inlinestatic

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

Definition at line 169 of file SMTConv.h.

References fromFloatSpecialBinOp(), and fromFloatUnOp().

Referenced by fromFloatSpecialBinOp().

◆ fromFloatUnOp()

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

inlinestatic

Constructs an SMTSolverRef from a floating-point unary operator.

Definition at line 58 of file SMTConv.h.

References fromUnOp().

Referenced by fromFloatBinOp(), fromFloatSpecialBinOp(), and getSymExpr().

◆ fromNBinOp()

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

inlinestatic

Construct an SMTSolverRef from a n-ary binary operator.

Definition at line 75 of file SMTConv.h.

◆ fromUnOp()

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

inlinestatic

Constructs an SMTSolverRef from an unary operator.

Definition at line 39 of file SMTConv.h.

Referenced by fromBinOp(), fromFloatUnOp(), getSymExpr(), and getZeroExpr().

◆ getAPSIntType()

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

inlinestatic

Definition at line 571 of file SMTConv.h.

References clang::ASTContext::getIntTypeForBitwidth().

Referenced by fixAPSInt().

◆ getBinExpr()

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

inlinestatic

Definition at line 346 of file SMTConv.h.

References clang::ASTContext::BoolTy, doTypeConversion(), fromBinOp(), fromFloatBinOp(), clang::ASTContext::getPointerDiffType(), clang::Type::isAnyPointerType(), clang::BinaryOperator::isComparisonOp(), clang::BinaryOperator::isLogicalOp(), clang::Type::isRealFloatingType(), and clang::Type::isSignedIntegerOrEnumerationType().

Referenced by getRangeExpr(), and getSymBinExpr().

◆ getCastExpr()

static llvm::SMTExprRef clang::ento::SMTConv::getCastExpr	(	llvm::SMTSolverRef &	Solver,
		ASTContext &	Ctx,
		const llvm::SMTExprRef &	Exp,
		QualType	FromTy,
		QualType	ToTy
	)

inlinestatic

Definition at line 335 of file SMTConv.h.

References fromCast(), and clang::ASTContext::getTypeSize().

Referenced by getSymExpr().

◆ getExpr()

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

inlinestatic

Definition at line 489 of file SMTConv.h.

References getSymExpr().

Referenced by clang::ento::SMTConstraintManager::assumeSym(), clang::ento::SMTConstraintManager::checkNull(), and getRangeExpr().

◆ getRangeExpr()

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

inlinestatic

Definition at line 532 of file SMTConv.h.

References fixAPSInt(), fromBinOp(), getBinExpr(), getExpr(), and clang::Type::isSignedIntegerOrEnumerationType().

Referenced by clang::ento::SMTConstraintManager::assumeSymInclusiveRange(), and clang::ento::Z3CrosscheckVisitor::finalizeVisitor().

◆ getSymBinExpr()

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

inlinestatic

Definition at line 381 of file SMTConv.h.

References fixAPSInt(), getBinExpr(), clang::ento::BinarySymExpr::getOpcode(), and getSymExpr().

Referenced by getSymExpr().

◆ getSymExpr()

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

inlinestatic

Definition at line 422 of file SMTConv.h.

References fromData(), fromFloatUnOp(), fromUnOp(), getCastExpr(), getSymBinExpr(), getSymExpr(), clang::ento::SymExpr::getType(), clang::ASTContext::getTypeSize(), clang::BinaryOperator::isComparisonOp(), and clang::Type::isRealFloatingType().

Referenced by getExpr(), getSymBinExpr(), and getSymExpr().

◆ getZeroExpr()

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

inlinestatic

Definition at line 501 of file SMTConv.h.

References fromBinOp(), fromFloatBinOp(), fromUnOp(), clang::ASTContext::getFloatTypeSemantics(), clang::ASTContext::getTypeSize(), clang::Type::isAnyPointerType(), clang::Type::isBlockPointerType(), clang::Type::isBooleanType(), clang::Type::isIntegralOrEnumerationType(), clang::Type::isRealFloatingType(), clang::Type::isReferenceType(), and clang::Type::isSignedIntegerOrEnumerationType().

Referenced by clang::ento::SMTConstraintManager::assumeSym(), and clang::ento::SMTConstraintManager::checkNull().

◆ mkSort()

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

inlinestatic

Definition at line 27 of file SMTConv.h.

References clang::Type::isBooleanType(), and clang::Type::isRealFloatingType().

Referenced by fromData().

The documentation for this class was generated from the following file:

include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

Static Public Member Functions

Detailed Description

Member Function Documentation

◆ castAPSInt()

◆ doFloatTypeConversion()

◆ doIntTypeConversion()

◆ doTypeConversion()

◆ fixAPSInt()

◆ fromBinOp()

◆ fromCast()

◆ fromData()

◆ fromFloatBinOp()

◆ fromFloatSpecialBinOp()

◆ fromFloatUnOp()

◆ fromNBinOp()

◆ fromUnOp()

◆ getAPSIntType()

◆ getBinExpr()

◆ getCastExpr()

◆ getExpr()

◆ getRangeExpr()

◆ getSymBinExpr()

◆ getSymExpr()

◆ getZeroExpr()

◆ mkSort()