#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 26 of file SMTConv.h.

Member Function Documentation

◆ castAPSInt()

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

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

inlinestatic

Definition at line 786 of file SMTConv.h.

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

Referenced by doTypeConversion().

◆ doIntTypeConversion()

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

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

inlinestatic

Definition at line 703 of file SMTConv.h.

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

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

◆ doTypeConversion()

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

inlinestatic

Definition at line 626 of file SMTConv.h.

References doFloatTypeConversion(), doIntTypeConversion(), 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()

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

inlinestatic

Definition at line 604 of file SMTConv.h.

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

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

◆ fromBinOp()

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 92 of file SMTConv.h.

References fromBinOp(), and fromUnOp().

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

◆ fromCast()

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 262 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()

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

inlinestatic

Construct an SMTSolverRef from a SymbolData.

Definition at line 325 of file SMTConv.h.

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

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

◆ fromFloatBinOp()

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 203 of file SMTConv.h.

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

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

◆ fromFloatSpecialBinOp()

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 171 of file SMTConv.h.

References fromFloatSpecialBinOp(), and fromFloatUnOp().

Referenced by fromFloatSpecialBinOp().

◆ fromFloatUnOp()

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 60 of file SMTConv.h.

References fromUnOp().

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

◆ fromNBinOp()

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 77 of file SMTConv.h.

◆ fromUnOp()

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 41 of file SMTConv.h.

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

◆ getAPSIntType()

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

inlinestatic

Definition at line 587 of file SMTConv.h.

References clang::ASTContext::CharTy, clang::ASTContext::getIntTypeForBitwidth(), clang::ASTContext::getTypeSize(), and clang::QualType::isNull().

Referenced by fixAPSInt().

◆ getBinExpr()

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 348 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()

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

inlinestatic

Definition at line 337 of file SMTConv.h.

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

Referenced by getSymExpr().

◆ getExpr()

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

inlinestatic

Definition at line 505 of file SMTConv.h.

References getSymExpr().

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

◆ getRangeExpr()

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 548 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()

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

inlinestatic

Definition at line 383 of file SMTConv.h.

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

Referenced by getSymExpr().

◆ getSymExpr()

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

inlinestatic

Definition at line 424 of file SMTConv.h.

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

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

◆ getZeroExpr()

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

inlinestatic

Definition at line 517 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(), clang::Type::isSignedIntegerOrEnumerationType(), and clang::Zero.

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

◆ mkSort()

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

inlinestatic

Definition at line 29 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()