llzk::verif Namespace Reference

Namespaces
namespace	detail

Classes
class	ConditionOpInterface
class	ContractEndOp
class	ContractEndOpAdaptor
class	ContractEndOpGenericAdaptor
class	ContractOp
class	ContractOpAdaptor
class	ContractOpGenericAdaptor
class	EnsureComputeOp
class	EnsureComputeOpAdaptor
class	EnsureComputeOpGenericAdaptor
class	EnsureConstrainOp
class	EnsureConstrainOpAdaptor
class	EnsureConstrainOpGenericAdaptor
struct	ForbiddenPreconditionInfluenceInfo
	Summary of forbidden precondition influence along with representative source locations for each forbidden kind. More...
class	IncludeOp
class	IncludeOpAdaptor
class	IncludeOpGenericAdaptor
class	PostconditionOpInterface
class	PreconditionOpInterface
class	RequireComputeOp
class	RequireComputeOpAdaptor
class	RequireComputeOpGenericAdaptor
class	RequireConstrainOp
class	RequireConstrainOpAdaptor
class	RequireConstrainOpGenericAdaptor
class	VerifDialect

Enumerations
enum class	ForbiddenPreconditionInfluence : uint8_t { None = 0 , StructMember = 1 << 0 , FunctionReturn = 1 << 1 }
	Sources of information that are not allowed in contract preconditions. More...

Functions
llvm::hash_code	hash_value (const ForbiddenPreconditionInfluenceInfo &info)
ForbiddenPreconditionInfluence	operator| (ForbiddenPreconditionInfluence lhs, ForbiddenPreconditionInfluence rhs)
ForbiddenPreconditionInfluence &	operator|= (ForbiddenPreconditionInfluence &lhs, ForbiddenPreconditionInfluence rhs)
bool	any (ForbiddenPreconditionInfluence influence)
	Return true when the influence set contains at least one classification.
bool	hasInfluence (ForbiddenPreconditionInfluence influence, ForbiddenPreconditionInfluence flag)
	Return true when influence contains the requested flag.
ForbiddenPreconditionInfluenceInfo	mergeInfluenceInfo (ForbiddenPreconditionInfluenceInfo lhs, const ForbiddenPreconditionInfluenceInfo &rhs)
	Merge two forbidden-influence summaries, preserving the first known source location for each forbidden kind.
template<typename T, typename... Args>
ForbiddenPreconditionInfluenceInfo	mergeInfluenceInfo (const T &first, const T &next, Args... others)
ForbiddenPreconditionInfluenceInfo	analyzeForbiddenPreconditionInfluenceInfo (mlir::ModuleOp module, verif::ContractOp contract, mlir::Value value)
	Analyze whether a contract value depends on forbidden precondition sources and recover representative source locations for any forbidden influence.
ForbiddenPreconditionInfluenceInfo	analyzeForbiddenPreconditionOpInfluenceInfo (mlir::ModuleOp module, verif::ContractOp contract, verif::PreconditionOpInterface preCondOp)
	Analyze whether a precondition op depends on forbidden sources, including both its condition operand and enclosing SCF control ancestors.
ForbiddenPreconditionInfluence	analyzeForbiddenPreconditionInfluence (mlir::ModuleOp module, verif::ContractOp contract, mlir::Value value)
	Analyze whether a contract value depends on forbidden precondition sources.
ForbiddenPreconditionInfluenceInfo	analyzeForbiddenPreconditionCallableResultInfo (mlir::ModuleOp module, mlir::CallableOpInterface callableOp, llvm::ArrayRef< ForbiddenPreconditionInfluenceInfo > argInfluences, unsigned resultNumber)
	Analyze whether a callable result depends on forbidden precondition sources under a caller-provided argument influence summary.
ForbiddenPreconditionInfluence	analyzeForbiddenPreconditionCallableResult (mlir::ModuleOp module, mlir::CallableOpInterface callableOp, llvm::ArrayRef< ForbiddenPreconditionInfluenceInfo > argInfluences, unsigned resultNumber)
	Analyze whether a callable result depends on forbidden precondition sources under a caller-provided argument influence summary.
detail::IncludedContractSummary	analyzeForbiddenIncludedContractSummary (mlir::ModuleOp module, verif::ContractOp calleeContract, llvm::ArrayRef< ForbiddenPreconditionInfluenceInfo > argInfluences)
	Analyze whether including a contract with caller-provided operand influence summaries would trigger a forbidden precondition failure in the callee.
detail::IncludedContractSummary	analyzeForbiddenIncludedOpSummary (mlir::ModuleOp module, verif::ContractOp contract, verif::IncludeOp includeOp)
	Analyze whether a specific include op triggers forbidden preconditions in the callee, including both caller operand bindings and caller-side SCF control ancestors.

Enumeration Type Documentation

ForbiddenPreconditionInfluence

enum class llzk::verif::ForbiddenPreconditionInfluence : uint8_t

strong

Sources of information that are not allowed in contract preconditions.

These are generally results of the target, so having preconditions over them doesn't make sense.

Enumerator
None
StructMember
FunctionReturn

Definition at line 36 of file ForbiddenPreconditionInfluence.h.

Function Documentation

analyzeForbiddenIncludedContractSummary()

detail::IncludedContractSummary llzk::verif::analyzeForbiddenIncludedContractSummary ( mlir::ModuleOp module, verif::ContractOp calleeContract, llvm::ArrayRef< ForbiddenPreconditionInfluenceInfo > argInfluences )

inline

Analyze whether including a contract with caller-provided operand influence summaries would trigger a forbidden precondition failure in the callee.

Definition at line 385 of file ForbiddenPreconditionInfluence.h.

analyzeForbiddenIncludedOpSummary()

detail::IncludedContractSummary llzk::verif::analyzeForbiddenIncludedOpSummary ( mlir::ModuleOp module, verif::ContractOp contract, verif::IncludeOp includeOp )

inline

Analyze whether a specific include op triggers forbidden preconditions in the callee, including both caller operand bindings and caller-side SCF control ancestors.

Definition at line 397 of file ForbiddenPreconditionInfluence.h.

analyzeForbiddenPreconditionCallableResult()

ForbiddenPreconditionInfluence llzk::verif::analyzeForbiddenPreconditionCallableResult ( mlir::ModuleOp module, mlir::CallableOpInterface callableOp, llvm::ArrayRef< ForbiddenPreconditionInfluenceInfo > argInfluences, unsigned resultNumber )

inline

Analyze whether a callable result depends on forbidden precondition sources under a caller-provided argument influence summary.

Definition at line 373 of file ForbiddenPreconditionInfluence.h.

analyzeForbiddenPreconditionCallableResultInfo()

ForbiddenPreconditionInfluenceInfo llzk::verif::analyzeForbiddenPreconditionCallableResultInfo ( mlir::ModuleOp module, mlir::CallableOpInterface callableOp, llvm::ArrayRef< ForbiddenPreconditionInfluenceInfo > argInfluences, unsigned resultNumber )

inline

Analyze whether a callable result depends on forbidden precondition sources under a caller-provided argument influence summary.

Definition at line 362 of file ForbiddenPreconditionInfluence.h.

analyzeForbiddenPreconditionInfluence()

ForbiddenPreconditionInfluence llzk::verif::analyzeForbiddenPreconditionInfluence ( mlir::ModuleOp module, verif::ContractOp contract, mlir::Value value )

inline

Analyze whether a contract value depends on forbidden precondition sources.

Definition at line 354 of file ForbiddenPreconditionInfluence.h.

analyzeForbiddenPreconditionInfluenceInfo()

ForbiddenPreconditionInfluenceInfo llzk::verif::analyzeForbiddenPreconditionInfluenceInfo ( mlir::ModuleOp module, verif::ContractOp contract, mlir::Value value )

inline

Analyze whether a contract value depends on forbidden precondition sources and recover representative source locations for any forbidden influence.

Definition at line 339 of file ForbiddenPreconditionInfluence.h.

analyzeForbiddenPreconditionOpInfluenceInfo()

ForbiddenPreconditionInfluenceInfo llzk::verif::analyzeForbiddenPreconditionOpInfluenceInfo ( mlir::ModuleOp module, verif::ContractOp contract, verif::PreconditionOpInterface preCondOp )

inline

Analyze whether a precondition op depends on forbidden sources, including both its condition operand and enclosing SCF control ancestors.

Definition at line 347 of file ForbiddenPreconditionInfluence.h.

any()

bool llzk::verif::any ( ForbiddenPreconditionInfluence influence )

inline

Return true when the influence set contains at least one classification.

Definition at line 84 of file ForbiddenPreconditionInfluence.h.

hash_value()

llvm::hash_code llzk::verif::hash_value ( const ForbiddenPreconditionInfluenceInfo & info )

inline

Definition at line 63 of file ForbiddenPreconditionInfluence.h.

hasInfluence()

bool llzk::verif::hasInfluence ( ForbiddenPreconditionInfluence influence, ForbiddenPreconditionInfluence flag )

inline

Return true when influence contains the requested flag.

Definition at line 90 of file ForbiddenPreconditionInfluence.h.

mergeInfluenceInfo() [1/2]

template<typename T, typename... Args>

ForbiddenPreconditionInfluenceInfo llzk::verif::mergeInfluenceInfo ( const T & first, const T & next, Args... others )

inline

Definition at line 106 of file ForbiddenPreconditionInfluence.h.

mergeInfluenceInfo() [2/2]

ForbiddenPreconditionInfluenceInfo llzk::verif::mergeInfluenceInfo ( ForbiddenPreconditionInfluenceInfo lhs, const ForbiddenPreconditionInfluenceInfo & rhs )

inline

Merge two forbidden-influence summaries, preserving the first known source location for each forbidden kind.

Definition at line 96 of file ForbiddenPreconditionInfluence.h.

operator|()

ForbiddenPreconditionInfluence llzk::verif::operator| ( ForbiddenPreconditionInfluence lhs, ForbiddenPreconditionInfluence rhs )

inline

Definition at line 71 of file ForbiddenPreconditionInfluence.h.

operator|=()

ForbiddenPreconditionInfluence & llzk::verif::operator|= ( ForbiddenPreconditionInfluence & lhs, ForbiddenPreconditionInfluence rhs )

inline

Definition at line 78 of file ForbiddenPreconditionInfluence.h.