ForbiddenPreconditionInfluence.h File Reference

This file contains an analysis and utilities for determining if a verif precondition is dependent, via control-flow or data-flow, on forbidden sources (i.e., struct members or function return values). More...

#include "llzk/Dialect/Verif/IR/Ops.h"
#include <mlir/Dialect/SCF/IR/SCF.h>
#include <mlir/Interfaces/CallInterfaces.h>
#include <llvm/ADT/DenseMap.h>
#include <llvm/ADT/DenseSet.h>
#include <llvm/ADT/SetVector.h>
#include <llvm/ADT/SmallVector.h>
#include <optional>

Include dependency graph for ForbiddenPreconditionInfluence.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	llzk::verif::ForbiddenPreconditionInfluenceInfo
	Summary of forbidden precondition influence along with representative source locations for each forbidden kind. More...
struct	llzk::verif::detail::CallableSummaryKey
	Cache key for one interprocedural callable-result summary query. More...
struct	llzk::verif::detail::CallableSummaryKeyInfo
struct	llzk::verif::detail::IncludedContractFailure
	One included precondition that becomes illegal under a specific caller binding. More...
struct	llzk::verif::detail::IncludedContractSummary
	Summary of all included-contract precondition failures under a specific caller binding. More...
struct	llzk::verif::detail::IncludedContractSummaryKey
	Cache key for one interprocedural included-contract summary query. More...
struct	llzk::verif::detail::IncludedContractSummaryKeyInfo
class	llzk::verif::detail::ForbiddenInfluenceAnalyzer
	Interprocedural verifier-local analysis for forbidden precondition influence. More...

Namespaces
namespace	llzk
namespace	llzk::verif
namespace	llzk::verif::detail

Typedefs
using	llzk::verif::detail::Influence = ForbiddenPreconditionInfluence
using	llzk::verif::detail::InfluenceInfo = ForbiddenPreconditionInfluenceInfo

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

Functions
llvm::hash_code	llzk::verif::hash_value (const ForbiddenPreconditionInfluenceInfo &info)
ForbiddenPreconditionInfluence	llzk::verif::operator| (ForbiddenPreconditionInfluence lhs, ForbiddenPreconditionInfluence rhs)
ForbiddenPreconditionInfluence &	llzk::verif::operator|= (ForbiddenPreconditionInfluence &lhs, ForbiddenPreconditionInfluence rhs)
bool	llzk::verif::any (ForbiddenPreconditionInfluence influence)
	Return true when the influence set contains at least one classification.
bool	llzk::verif::hasInfluence (ForbiddenPreconditionInfluence influence, ForbiddenPreconditionInfluence flag)
	Return true when influence contains the requested flag.
ForbiddenPreconditionInfluenceInfo	llzk::verif::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	llzk::verif::mergeInfluenceInfo (const T &first, const T &next, Args... others)
ForbiddenPreconditionInfluenceInfo	llzk::verif::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	llzk::verif::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	llzk::verif::analyzeForbiddenPreconditionInfluence (mlir::ModuleOp module, verif::ContractOp contract, mlir::Value value)
	Analyze whether a contract value depends on forbidden precondition sources.
ForbiddenPreconditionInfluenceInfo	llzk::verif::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	llzk::verif::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	llzk::verif::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	llzk::verif::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.

Detailed Description

This file contains an analysis and utilities for determining if a verif precondition is dependent, via control-flow or data-flow, on forbidden sources (i.e., struct members or function return values).

Definition in file ForbiddenPreconditionInfluence.h.