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, std::optional< UnreducedInterval > unreducedInterval=std::nullopt)
llvm::SMTExprRef	getExpr () const
const Interval &	getInterval () const
bool	hasUnreducedInterval () const
const std::optional< UnreducedInterval > &	getOptionalUnreducedInterval () const
const UnreducedInterval &	getUnreducedInterval () 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	withUnreducedInterval (const UnreducedInterval &newUnreducedInterval) const
ExpressionValue	withOptionalUnreducedInterval (std::optional< UnreducedInterval > newUnreducedInterval) const
ExpressionValue	dropUnreducedInterval () const
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 49 of file IntervalAnalysis.h.

Constructor & Destructor Documentation

◆ ExpressionValue() [1/5]

llzk::ExpressionValue::ExpressionValue ( )

inline

Definition at line 52 of file IntervalAnalysis.h.

◆ ExpressionValue() [2/5]

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

inlineexplicit

Definition at line 54 of file IntervalAnalysis.h.

◆ ExpressionValue() [3/5]

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

inline

Definition at line 57 of file IntervalAnalysis.h.

◆ ExpressionValue() [4/5]

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

inline

Definition at line 60 of file IntervalAnalysis.h.

◆ ExpressionValue() [5/5]

llzk::ExpressionValue::ExpressionValue	(	llvm::SMTExprRef	exprRef,
		const Interval &	interval,
		std::optional< UnreducedInterval >	unreducedInterval = std::nullopt )

inline

Definition at line 63 of file IntervalAnalysis.h.

Member Function Documentation

◆ dropUnreducedInterval()

ExpressionValue llzk::ExpressionValue::dropUnreducedInterval ( ) const

inline

Definition at line 105 of file IntervalAnalysis.h.

◆ getExpr()

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

inline

Definition at line 69 of file IntervalAnalysis.h.

◆ getField()

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

inline

Definition at line 82 of file IntervalAnalysis.h.

◆ getInterval()

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

inline

Definition at line 71 of file IntervalAnalysis.h.

◆ getOptionalUnreducedInterval()

const std::optional< UnreducedInterval > & llzk::ExpressionValue::getOptionalUnreducedInterval ( ) const

inline

Definition at line 75 of file IntervalAnalysis.h.

◆ getUnreducedInterval()

const UnreducedInterval & llzk::ExpressionValue::getUnreducedInterval ( ) const

inline

Definition at line 77 of file IntervalAnalysis.h.

◆ hasUnreducedInterval()

bool llzk::ExpressionValue::hasUnreducedInterval ( ) const

inline

Definition at line 73 of file IntervalAnalysis.h.

◆ isBoolSort()

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

inline

Definition at line 117 of file IntervalAnalysis.h.

◆ join()

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

inline

Fold two expressions together when overapproximating array elements.

Definition at line 109 of file IntervalAnalysis.h.

◆ operator==()

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

Definition at line 248 of file IntervalAnalysis.cpp.

◆ print()

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

Definition at line 621 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 92 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 87 of file IntervalAnalysis.h.

◆ withOptionalUnreducedInterval()

ExpressionValue llzk::ExpressionValue::withOptionalUnreducedInterval ( std::optional< UnreducedInterval > newUnreducedInterval ) const

inline

Definition at line 101 of file IntervalAnalysis.h.

◆ withUnreducedInterval()

ExpressionValue llzk::ExpressionValue::withUnreducedInterval ( const UnreducedInterval & newUnreducedInterval ) const

inline

Definition at line 96 of file IntervalAnalysis.h.

◆ add

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

friend

Definition at line 308 of file IntervalAnalysis.cpp.

◆ bitAnd

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

friend

Definition at line 431 of file IntervalAnalysis.cpp.

◆ bitOr

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

friend

Definition at line 439 of file IntervalAnalysis.cpp.

◆ bitXor

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

friend

Definition at line 447 of file IntervalAnalysis.cpp.

◆ boolAnd

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

friend

Definition at line 542 of file IntervalAnalysis.cpp.

◆ boolNot

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

friend

Definition at line 588 of file IntervalAnalysis.cpp.

◆ boolOr

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

friend

Definition at line 551 of file IntervalAnalysis.cpp.

◆ boolXor

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

friend

Definition at line 560 of file IntervalAnalysis.cpp.

◆ cmp

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

friend

Definition at line 477 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 299 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 415 of file IntervalAnalysis.cpp.

◆ mul

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

friend

Definition at line 326 of file IntervalAnalysis.cpp.

◆ neg

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

friend

Definition at line 571 of file IntervalAnalysis.cpp.

◆ notOp

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

friend

Definition at line 581 of file IntervalAnalysis.cpp.

◆ operator<<

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

friend

Definition at line 212 of file IntervalAnalysis.h.

◆ shiftLeft

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

friend

Definition at line 458 of file IntervalAnalysis.cpp.

◆ shiftRight

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

friend

Definition at line 467 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 317 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

◆ dropUnreducedInterval()

◆ getExpr()

◆ getField()

◆ getInterval()

◆ getOptionalUnreducedInterval()

◆ getUnreducedInterval()

◆ hasUnreducedInterval()

◆ isBoolSort()

◆ join()

◆ operator==()

◆ print()

◆ withExpression()

◆ withInterval()

◆ withOptionalUnreducedInterval()

◆ withUnreducedInterval()

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