Tracks a solver expression and an interval range for that expression. More...

#include <IntervalAnalysis.h>

Classes
struct	Hash

Public Member Functions
	ExpressionValue ()
	ExpressionValue (const Field &f)
	ExpressionValue (const Field &f, llvm::SMTExprRef exprRef)
	ExpressionValue (const Field &f, llvm::SMTExprRef exprRef, const llvm::DynamicAPInt &singleVal)
	ExpressionValue (llvm::SMTExprRef exprRef, const Interval &interval)
llvm::SMTExprRef	getExpr () const
const Interval &	getInterval () const
const Field &	getField () const
ExpressionValue	withInterval (const Interval &newInterval) const
	Return the current expression with a new interval.
ExpressionValue	withExpression (const llvm::SMTExprRef &newExpr) const
	Return the current expression with a new SMT expression.
ExpressionValue &	join (const ExpressionValue &)
	Fold two expressions together when overapproximating array elements.
bool	operator== (const ExpressionValue &rhs) const
bool	isBoolSort (const llvm::SMTSolverRef &solver) const
void	print (mlir::raw_ostream &os) const

Friends
ExpressionValue	intersection (const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
	Compute the intersection of the lhs and rhs intervals, and create a solver expression that constrains both sides to be equal.
ExpressionValue	join (const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
	Compute the union of the lhs and rhs intervals, and create a solver expression that constrains both sides to be equal.
ExpressionValue	add (const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	sub (const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	mul (const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	div (const llvm::SMTSolverRef &solver, mlir::Operation *op, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	uintDiv (const llvm::SMTSolverRef &solver, mlir::Operation *op, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	sintDiv (const llvm::SMTSolverRef &solver, mlir::Operation *op, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	mod (const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	bitAnd (const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	bitOr (const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	bitXor (const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	shiftLeft (const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	shiftRight (const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	cmp (const llvm::SMTSolverRef &solver, boolean::CmpOp op, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	boolAnd (const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	boolOr (const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	boolXor (const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	neg (const llvm::SMTSolverRef &solver, const ExpressionValue &val)
ExpressionValue	notOp (const llvm::SMTSolverRef &solver, const ExpressionValue &val)
ExpressionValue	boolNot (const llvm::SMTSolverRef &solver, const ExpressionValue &val)
ExpressionValue	fallbackUnaryOp (const llvm::SMTSolverRef &solver, mlir::Operation *op, const ExpressionValue &val)
mlir::raw_ostream &	operator<< (mlir::raw_ostream &os, const ExpressionValue &e)

Detailed Description

Tracks a solver expression and an interval range for that expression.

Used as a scalar lattice value.

Definition at line 46 of file IntervalAnalysis.h.

Constructor & Destructor Documentation

◆ ExpressionValue() [1/5]

llzk::ExpressionValue::ExpressionValue ( )

inline

Definition at line 49 of file IntervalAnalysis.h.

◆ ExpressionValue() [2/5]

llzk::ExpressionValue::ExpressionValue ( const Field & f )

inlineexplicit

Definition at line 51 of file IntervalAnalysis.h.

◆ ExpressionValue() [3/5]

llzk::ExpressionValue::ExpressionValue	(	const Field &	f,
		llvm::SMTExprRef	exprRef )

inline

Definition at line 53 of file IntervalAnalysis.h.

◆ ExpressionValue() [4/5]

llzk::ExpressionValue::ExpressionValue	(	const Field &	f,
		llvm::SMTExprRef	exprRef,
		const llvm::DynamicAPInt &	singleVal )

inline

Definition at line 56 of file IntervalAnalysis.h.

◆ ExpressionValue() [5/5]

llzk::ExpressionValue::ExpressionValue	(	llvm::SMTExprRef	exprRef,
		const Interval &	interval )

inline

Definition at line 59 of file IntervalAnalysis.h.

Member Function Documentation

◆ getExpr()

llvm::SMTExprRef llzk::ExpressionValue::getExpr ( ) const

inline

Definition at line 62 of file IntervalAnalysis.h.

◆ getField()

const Field & llzk::ExpressionValue::getField ( ) const

inline

Definition at line 66 of file IntervalAnalysis.h.

◆ getInterval()

const Interval & llzk::ExpressionValue::getInterval ( ) const

inline

Definition at line 64 of file IntervalAnalysis.h.

◆ isBoolSort()

bool llzk::ExpressionValue::isBoolSort ( const llvm::SMTSolverRef & solver ) const

inline

Definition at line 89 of file IntervalAnalysis.h.

◆ join()

ExpressionValue & llzk::ExpressionValue::join ( const ExpressionValue & )

inline

Fold two expressions together when overapproximating array elements.

Definition at line 82 of file IntervalAnalysis.h.

◆ operator==()

bool llzk::ExpressionValue::operator== ( const ExpressionValue & rhs ) const

Definition at line 64 of file IntervalAnalysis.cpp.

◆ print()

void llzk::ExpressionValue::print ( mlir::raw_ostream & os ) const

Definition at line 399 of file IntervalAnalysis.cpp.

◆ withExpression()

ExpressionValue llzk::ExpressionValue::withExpression ( const llvm::SMTExprRef & newExpr ) const

inline

Return the current expression with a new SMT expression.

Definition at line 76 of file IntervalAnalysis.h.

◆ withInterval()

ExpressionValue llzk::ExpressionValue::withInterval ( const Interval & newInterval ) const

inline

Return the current expression with a new interval.

Parameters

newInterval

Returns

Definition at line 71 of file IntervalAnalysis.h.

◆ add

ExpressionValue add	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Definition at line 112 of file IntervalAnalysis.cpp.

◆ bitAnd

ExpressionValue bitAnd	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Definition at line 224 of file IntervalAnalysis.cpp.

◆ bitOr

ExpressionValue bitOr	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Definition at line 232 of file IntervalAnalysis.cpp.

◆ bitXor

ExpressionValue bitXor	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Definition at line 240 of file IntervalAnalysis.cpp.

◆ boolAnd

ExpressionValue boolAnd	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Definition at line 334 of file IntervalAnalysis.cpp.

◆ boolNot

ExpressionValue boolNot	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	val )

friend

Definition at line 374 of file IntervalAnalysis.cpp.

◆ boolOr

ExpressionValue boolOr	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Definition at line 342 of file IntervalAnalysis.cpp.

◆ boolXor

ExpressionValue boolXor	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Definition at line 350 of file IntervalAnalysis.cpp.

◆ cmp

ExpressionValue cmp	(	const llvm::SMTSolverRef &	solver,
		boolean::CmpOp	op,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Definition at line 270 of file IntervalAnalysis.cpp.

◆ div

ExpressionValue div	(	const llvm::SMTSolverRef &	solver,
		mlir::Operation *	op,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

◆ fallbackUnaryOp

ExpressionValue fallbackUnaryOp	(	const llvm::SMTSolverRef &	solver,
		mlir::Operation *	op,
		const ExpressionValue &	val )

friend

◆ intersection

ExpressionValue intersection	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Compute the intersection of the lhs and rhs intervals, and create a solver expression that constrains both sides to be equal.

Parameters

solver
lhs
rhs

Returns

Definition at line 103 of file IntervalAnalysis.cpp.

◆ join

ExpressionValue join	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Compute the union of the lhs and rhs intervals, and create a solver expression that constrains both sides to be equal.

Parameters

solver
lhs
rhs

Returns

◆ mod

ExpressionValue mod	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Definition at line 216 of file IntervalAnalysis.cpp.

◆ mul

ExpressionValue mul	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Definition at line 128 of file IntervalAnalysis.cpp.

◆ neg

ExpressionValue neg	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	val )

friend

Definition at line 360 of file IntervalAnalysis.cpp.

◆ notOp

ExpressionValue notOp	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	val )

friend

Definition at line 367 of file IntervalAnalysis.cpp.

◆ operator<<

mlir::raw_ostream & operator<<	(	mlir::raw_ostream &	os,
		const ExpressionValue &	e )

friend

Definition at line 184 of file IntervalAnalysis.h.

◆ shiftLeft

ExpressionValue shiftLeft	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Definition at line 251 of file IntervalAnalysis.cpp.

◆ shiftRight

ExpressionValue shiftRight	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Definition at line 260 of file IntervalAnalysis.cpp.

◆ sintDiv

ExpressionValue sintDiv	(	const llvm::SMTSolverRef &	solver,
		mlir::Operation *	op,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

◆ sub

ExpressionValue sub	(	const llvm::SMTSolverRef &	solver,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Definition at line 120 of file IntervalAnalysis.cpp.

◆ uintDiv

ExpressionValue uintDiv	(	const llvm::SMTSolverRef &	solver,
		mlir::Operation *	op,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

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

include/llzk/Analysis/IntervalAnalysis.h
lib/Analysis/IntervalAnalysis.cpp

Classes

Public Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

◆ ExpressionValue() [1/5]

◆ ExpressionValue() [2/5]

◆ ExpressionValue() [3/5]

◆ ExpressionValue() [4/5]

◆ ExpressionValue() [5/5]

Member Function Documentation

◆ getExpr()

◆ getField()

◆ getInterval()

◆ isBoolSort()

◆ join()

◆ operator==()

◆ print()

◆ withExpression()

◆ withInterval()

Friends And Related Symbol Documentation

◆ add

◆ bitAnd

◆ bitOr

◆ bitXor

◆ boolAnd

◆ boolNot

◆ boolOr

◆ boolXor

◆ cmp

◆ div

◆ fallbackUnaryOp

◆ intersection

◆ join

◆ mod

◆ mul

◆ neg

◆ notOp

◆ operator<<

◆ shiftLeft

◆ shiftRight

◆ sintDiv

◆ sub

◆ uintDiv