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, 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 (llvm::SMTSolverRef solver) const
void	print (mlir::raw_ostream &os) const

Friends
ExpressionValue	intersection (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 (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 (llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	sub (llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	mul (llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	div (llvm::SMTSolverRef solver, felt::DivFeltOp op, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	mod (llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	bitAnd (llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	shiftLeft (llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	shiftRight (llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	cmp (llvm::SMTSolverRef solver, boolean::CmpOp op, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	boolAnd (llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	boolOr (llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	boolXor (llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
ExpressionValue	fallbackBinaryOp (llvm::SMTSolverRef solver, mlir::Operation *op, const ExpressionValue &lhs, const ExpressionValue &rhs)
	Computes a solver expression based on the operation, but computes a fallback interval (which is just Entire, or unknown).
ExpressionValue	neg (llvm::SMTSolverRef solver, const ExpressionValue &val)
ExpressionValue	notOp (llvm::SMTSolverRef solver, const ExpressionValue &val)
ExpressionValue	boolNot (llvm::SMTSolverRef solver, const ExpressionValue &val)
ExpressionValue	fallbackUnaryOp (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 45 of file IntervalAnalysis.h.

Constructor & Destructor Documentation

◆ ExpressionValue() [1/4]

llzk::ExpressionValue::ExpressionValue ( )

inline

Definition at line 48 of file IntervalAnalysis.h.

◆ ExpressionValue() [2/4]

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

inlineexplicit

Definition at line 50 of file IntervalAnalysis.h.

◆ ExpressionValue() [3/4]

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

inline

Definition at line 53 of file IntervalAnalysis.h.

◆ ExpressionValue() [4/4]

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

inline

Definition at line 56 of file IntervalAnalysis.h.

Member Function Documentation

◆ getExpr()

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

inline

Definition at line 59 of file IntervalAnalysis.h.

◆ getField()

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

inline

Definition at line 63 of file IntervalAnalysis.h.

◆ getInterval()

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

inline

Definition at line 61 of file IntervalAnalysis.h.

◆ isBoolSort()

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

inline

Definition at line 86 of file IntervalAnalysis.h.

◆ join()

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

inline

Fold two expressions together when overapproximating array elements.

Definition at line 79 of file IntervalAnalysis.h.

◆ operator==()

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

Definition at line 33 of file IntervalAnalysis.cpp.

◆ print()

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

Definition at line 268 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 73 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 68 of file IntervalAnalysis.h.

◆ add

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

friend

Definition at line 59 of file IntervalAnalysis.cpp.

◆ bitAnd

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

friend

Definition at line 110 of file IntervalAnalysis.cpp.

◆ boolAnd

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

friend

Definition at line 173 of file IntervalAnalysis.cpp.

◆ boolNot

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

friend

Definition at line 232 of file IntervalAnalysis.cpp.

◆ boolOr

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

friend

Definition at line 181 of file IntervalAnalysis.cpp.

◆ boolXor

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

friend

Definition at line 189 of file IntervalAnalysis.cpp.

◆ cmp

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

friend

Definition at line 134 of file IntervalAnalysis.cpp.

◆ div

ExpressionValue div	(	llvm::SMTSolverRef	solver,
		felt::DivFeltOp	op,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Definition at line 83 of file IntervalAnalysis.cpp.

◆ fallbackBinaryOp

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

friend

Computes a solver expression based on the operation, but computes a fallback interval (which is just Entire, or unknown).

Used for currently unsupported compute-only operations.

Parameters

solver
op
lhs
rhs

Returns

◆ fallbackUnaryOp

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

friend

◆ intersection

ExpressionValue intersection	(	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 52 of file IntervalAnalysis.cpp.

◆ join

ExpressionValue join	(	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	(	llvm::SMTSolverRef	solver,
		const ExpressionValue &	lhs,
		const ExpressionValue &	rhs )

friend

Definition at line 102 of file IntervalAnalysis.cpp.

◆ mul

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

friend

Definition at line 75 of file IntervalAnalysis.cpp.

◆ neg

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

friend

Definition at line 218 of file IntervalAnalysis.cpp.

◆ notOp

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

friend

Definition at line 225 of file IntervalAnalysis.cpp.

◆ operator<<

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

friend

Definition at line 174 of file IntervalAnalysis.h.

◆ shiftLeft

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

friend

Definition at line 118 of file IntervalAnalysis.cpp.

◆ shiftRight

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

friend

Definition at line 126 of file IntervalAnalysis.cpp.

◆ sub

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

friend

Definition at line 67 of file IntervalAnalysis.cpp.

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/4]

◆ ExpressionValue() [2/4]

◆ ExpressionValue() [3/4]

◆ ExpressionValue() [4/4]

Member Function Documentation

◆ getExpr()

◆ getField()

◆ getInterval()

◆ isBoolSort()

◆ join()

◆ operator==()

◆ print()

◆ withExpression()

◆ withInterval()

Friends And Related Symbol Documentation

◆ add

◆ bitAnd

◆ boolAnd

◆ boolNot

◆ boolOr

◆ boolXor

◆ cmp

◆ div

◆ fallbackBinaryOp

◆ fallbackUnaryOp

◆ intersection

◆ join

◆ mod

◆ mul

◆ neg

◆ notOp

◆ operator<<

◆ shiftLeft

◆ shiftRight

◆ sub