#include "llzk-c/Support.h"
#include <mlir-c/IR.h>
#include <mlir-c/Support.h>
#include "llzk/Dialect/Verif/IR/Ops.capi.h.inc"

Include dependency graph for Verif.h:

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

Functions
	MLIR_DECLARE_CAPI_DIALECT_REGISTRATION (Verif, llzk__verif)
	Get reference to the LLZK verif dialect.
MLIR_CAPI_EXPORTED void	llzkVerif_attachInterfaces (MlirContext context)
	Attaches the interfaces defined by the verif dialect to upstream IR elements.
	LLZK_DECLARE_OP_BUILD_METHOD (Verif, ContractOp, MlirIdentifier sym_name, MlirAttribute target, MlirAttribute function_type, MlirAttribute arg_attrs)
	Build a verif.contract from explicit attributes and signature metadata.
	LLZK_DECLARE_SUFFIX_OP_BUILD_METHOD (Verif, ContractOp, FromTargetIdentifier, MlirIdentifier sym_name, MlirIdentifier target)
	Build a verif.contract with arguments and attributes derived from the target.
	LLZK_DECLARE_SUFFIX_OP_BUILD_METHOD (Verif, ContractOp, FromTargetAttr, MlirIdentifier sym_name, MlirAttribute target)
	Build a verif.contract with arguments and attributes derived from the target.
	LLZK_DECLARE_OP_BUILD_METHOD (Verif, IncludeOp, MlirAttribute callee, MlirValueRange argOperands, MlirAttribute templateParams)
	Build a verif.include with a flat list of call operands and no affine-map instantiations.
MLIR_CAPI_EXPORTED MlirType	llzkVerif_IncludeOpGetTypeSignature (MlirOperation inp)
	Return the FunctionType inferred from the arg operands of this CallOp.
	LLZK_DECLARE_OP_BUILD_METHOD (Verif, InvariantOp, MlirStringRef loopName, intptr_t numArgs, MlirType const types, MlirLocation const locs)
	Build a verif.invariant with a list of argument types and locations.
MLIR_CAPI_EXPORTED MlirBlock	llzkVerif_InvariantOpGetBody (MlirOperation op)
	Returns the body of the invariant operation.

Function Documentation

◆ LLZK_DECLARE_OP_BUILD_METHOD() [1/3]

LLZK_DECLARE_OP_BUILD_METHOD	(	Verif	,
		ContractOp	,
		MlirIdentifier	sym_name,
		MlirAttribute	target,
		MlirAttribute	function_type,
		MlirAttribute	arg_attrs )

Build a verif.contract from explicit attributes and signature metadata.

◆ LLZK_DECLARE_OP_BUILD_METHOD() [2/3]

LLZK_DECLARE_OP_BUILD_METHOD	(	Verif	,
		IncludeOp	,
		MlirAttribute	callee,
		MlirValueRange	argOperands,
		MlirAttribute	templateParams )

Build a verif.include with a flat list of call operands and no affine-map instantiations.

◆ LLZK_DECLARE_OP_BUILD_METHOD() [3/3]

LLZK_DECLARE_OP_BUILD_METHOD	(	Verif	,
		InvariantOp	,
		MlirStringRef	loopName,
		intptr_t	numArgs,
		MlirType const *	types,
		MlirLocation const *	locs )

Build a verif.invariant with a list of argument types and locations.

The pointers to the types and locations must point to the same amount of elements.

◆ LLZK_DECLARE_SUFFIX_OP_BUILD_METHOD() [1/2]

LLZK_DECLARE_SUFFIX_OP_BUILD_METHOD	(	Verif	,
		ContractOp	,
		FromTargetAttr	,
		MlirIdentifier	sym_name,
		MlirAttribute	target )

Build a verif.contract with arguments and attributes derived from the target.

◆ LLZK_DECLARE_SUFFIX_OP_BUILD_METHOD() [2/2]

LLZK_DECLARE_SUFFIX_OP_BUILD_METHOD	(	Verif	,
		ContractOp	,
		FromTargetIdentifier	,
		MlirIdentifier	sym_name,
		MlirIdentifier	target )

Build a verif.contract with arguments and attributes derived from the target.

◆ llzkVerif_attachInterfaces()

MLIR_CAPI_EXPORTED void llzkVerif_attachInterfaces ( 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.

Definition at line 31 of file Verif.cpp.

◆ llzkVerif_IncludeOpGetTypeSignature()

MLIR_CAPI_EXPORTED MlirType llzkVerif_IncludeOpGetTypeSignature ( MlirOperation inp )

Return the FunctionType inferred from the arg operands of this CallOp.

This is not necessarily the same as the callee's FunctionType but should unify with it or else IR verification will fail.

Definition at line 103 of file Verif.cpp.

◆ llzkVerif_InvariantOpGetBody()

MLIR_CAPI_EXPORTED MlirBlock llzkVerif_InvariantOpGetBody ( MlirOperation op )

Returns the body of the invariant operation.

Definition at line 126 of file Verif.cpp.

◆ MLIR_DECLARE_CAPI_DIALECT_REGISTRATION()

MLIR_DECLARE_CAPI_DIALECT_REGISTRATION	(	Verif	,
		llzk__verif	)

Get reference to the LLZK verif dialect.

Functions