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, llvm::APSInt singleVal)

	ExpressionValue (llvm::SMTExprRef exprRef, 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 &	join (const ExpressionValue &rhs)
	Fold two expressions together when overapproximating array elements.

bool	operator== (const ExpressionValue &rhs) 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	cmp (llvm::SMTSolverRef solver, boolean::CmpOp op, 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	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 431 of file IntervalAnalysis.h.

Constructor & Destructor Documentation

◆ ExpressionValue() [1/4]

llzk::ExpressionValue::ExpressionValue ( )

inline

Definition at line 434 of file IntervalAnalysis.h.

◆ ExpressionValue() [2/4]

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

inlineexplicit

Definition at line 436 of file IntervalAnalysis.h.

◆ ExpressionValue() [3/4]

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

inline

Definition at line 439 of file IntervalAnalysis.h.

◆ ExpressionValue() [4/4]

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

inline

Definition at line 442 of file IntervalAnalysis.h.

Member Function Documentation

◆ getExpr()

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

inline

Definition at line 444 of file IntervalAnalysis.h.

◆ getField()

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

inline

Definition at line 448 of file IntervalAnalysis.h.

◆ getInterval()

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

inline

Definition at line 446 of file IntervalAnalysis.h.

◆ join()

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

inline

Fold two expressions together when overapproximating array elements.

Definition at line 459 of file IntervalAnalysis.h.

◆ operator==()

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

Definition at line 468 of file IntervalAnalysis.cpp.

◆ print()

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

Definition at line 636 of file IntervalAnalysis.cpp.

◆ withInterval()

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

inline

Return the current expression with a new interval.

Parameters

newInterval

Returns

Definition at line 453 of file IntervalAnalysis.h.

Friends And Related Symbol Documentation

◆ add

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

friend

Definition at line 486 of file IntervalAnalysis.cpp.

◆ cmp

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

friend

Definition at line 536 of file IntervalAnalysis.cpp.

◆ div

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

friend

Definition at line 510 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 479 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 528 of file IntervalAnalysis.cpp.

◆ mul

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

friend

Definition at line 502 of file IntervalAnalysis.cpp.

◆ neg

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

friend

Definition at line 585 of file IntervalAnalysis.cpp.

◆ notOp

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

friend

Definition at line 592 of file IntervalAnalysis.cpp.

◆ operator<<

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

friend

Definition at line 530 of file IntervalAnalysis.h.

◆ sub

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

friend

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

◆ join()

◆ operator==()

◆ print()

◆ withInterval()

Friends And Related Symbol Documentation

◆ add

◆ cmp

◆ div

◆ fallbackBinaryOp

◆ fallbackUnaryOp

◆ intersection

◆ join

◆ mod

◆ mul

◆ neg

◆ notOp

◆ operator<<

◆ sub