llzk::verif Namespace Reference

Namespaces
namespace	detail
	Common interface for precondition and postcondition operations.

Classes
class	AssumeDetOp
class	AssumeDetOpAdaptor
class	AssumeDetOpGenericAdaptor
class	ConditionOpInterface
class	ContractEndOp
class	ContractEndOpAdaptor
class	ContractEndOpGenericAdaptor
class	ContractOp
class	ContractOpAdaptor
class	ContractOpGenericAdaptor
class	ContractTargetOpInterface
class	DecreasesOp
class	DecreasesOpAdaptor
class	DecreasesOpGenericAdaptor
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	IncreasesOp
class	IncreasesOpAdaptor
class	IncreasesOpGenericAdaptor
class	InvariantOp
class	InvariantOpAdaptor
class	InvariantOpGenericAdaptor
class	InvariantTargetOpInterface
class	OldOp
class	OldOpAdaptor
class	OldOpGenericAdaptor
class	PostconditionOpInterface
class	PreconditionOpInterface
class	ProveDetOp
class	ProveDetOpAdaptor
class	ProveDetOpGenericAdaptor
class	RequireComputeOp
class	RequireComputeOpAdaptor
class	RequireComputeOpGenericAdaptor
class	RequireConstrainOp
class	RequireConstrainOpAdaptor
class	RequireConstrainOpGenericAdaptor
class	StepOp
class	StepOpAdaptor
class	StepOpGenericAdaptor
class	StepYieldOp
class	StepYieldOpAdaptor
class	StepYieldOpGenericAdaptor
class	VerifAssertOp
class	VerifAssertOpAdaptor
class	VerifAssertOpGenericAdaptor
class	VerifDialect
	LLZK verification dialect for encoding specifications for functions and structs. More...
class	VerifProveOp
class	VerifProveOpAdaptor
class	VerifProveOpGenericAdaptor
class	VerifSMTProveOp
class	VerifSMTProveOpAdaptor
class	VerifSMTProveOpGenericAdaptor

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

Functions
void	attachInterfaces (mlir::MLIRContext &context)
	Attaches the interfaces defined by the verif dialect to upstream IR elements.
void	registerExtensions (mlir::DialectRegistry &registry)
	Registers dialect extensions for the verif dialect.
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, const 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 369 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 381 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 357 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 346 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 338 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 323 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 331 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.

attachInterfaces()

void llzk::verif::attachInterfaces

(

mlir::MLIRContext &

context

)

Attaches the interfaces defined by the verif dialect to upstream IR elements.

Attempting to use those interfaces without calling this function first will result in an error.

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, const 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.

registerExtensions()

void llzk::verif::registerExtensions

(

mlir::DialectRegistry &

registry

)

Registers dialect extensions for the verif dialect.

Definition at line 107 of file Dialect.cpp.