Verif.h File Reference

#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:

Go to the source code of 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.
	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_InvariantOpGetBody()

MLIR_CAPI_EXPORTED MlirBlock llzkVerif_InvariantOpGetBody

(

MlirOperation

op

)

Returns the body of the invariant operation.

Definition at line 122 of file Verif.cpp.

MLIR_DECLARE_CAPI_DIALECT_REGISTRATION()

MLIR_DECLARE_CAPI_DIALECT_REGISTRATION	(	Verif	,
		llzk__verif	)

Get reference to the LLZK verif dialect.