A symbol cache for LLVM globals and functions relevant to SMT lowering patterns. More...

#include <SMTToZ3LLVM.h>

Collaboration diagram for circt::SMTGlobalsHandler:

[legend]

Public Member Functions
	SMTGlobalsHandler (ModuleOp module, mlir::LLVM::GlobalOp solver, mlir::LLVM::GlobalOp ctx)
	Initializes the caches and keeps track of the given globals to store the pointers to the SMT solver and context. More...

	SMTGlobalsHandler (Namespace &&names, mlir::LLVM::GlobalOp solver, mlir::LLVM::GlobalOp ctx)
	Initializes the caches and keeps track of the given globals to store the pointers to the SMT solver and context. More...

Static Public Member Functions
static SMTGlobalsHandler	create (OpBuilder &builder, ModuleOp module)
	Creates the LLVM global operations to store the pointers to the solver and the context and returns a 'SMTGlobalHandler' initialized with those new globals. More...

Public Attributes
const mlir::LLVM::GlobalOp	solver
	The global storing the pointer to the SMT solver object currently active. More...

const mlir::LLVM::GlobalOp	ctx
	The global storing the pointer to the SMT context object currently active. More...

Namespace	names

DenseMap< StringAttr, mlir::LLVM::LLVMFuncOp >	funcMap

DenseMap< Block *, Value >	ctxCache

DenseMap< Block *, Value >	solverCache

DenseMap< StringAttr, mlir::LLVM::GlobalOp >	stringCache

Detailed Description

A symbol cache for LLVM globals and functions relevant to SMT lowering patterns.

Definition at line 25 of file SMTToZ3LLVM.h.

Constructor & Destructor Documentation

◆ SMTGlobalsHandler() [1/2]

SMTGlobalsHandler::SMTGlobalsHandler	(	ModuleOp	module,
		mlir::LLVM::GlobalOp	solver,
		mlir::LLVM::GlobalOp	ctx
	)

Initializes the caches and keeps track of the given globals to store the pointers to the SMT solver and context.

It is assumed that the passed global operations are of the correct (or at least compatible) form. E.g.,

llvm.mlir.global internal @ctx() {alignment = 8 : i64} : !llvm.ptr {
  %0 = llvm.mlir.zero : !llvm.ptr
  llvm.return %0 : !llvm.ptr
}

Definition at line 80 of file LowerSMTToZ3LLVM.cpp.

References circt::Namespace::add(), circt::SymbolCacheBase::addDefinitions(), and names.

◆ SMTGlobalsHandler() [2/2]

SMTGlobalsHandler::SMTGlobalsHandler	(	Namespace &&	names,
		mlir::LLVM::GlobalOp	solver,
		mlir::LLVM::GlobalOp	ctx
	)

Initializes the caches and keeps track of the given globals to store the pointers to the SMT solver and context.

It is assumed that the passed global operations are of the correct (or at least compatible) form. E.g.,

llvm.mlir.global internal @ctx() {alignment = 8 : i64} : !llvm.ptr {
  %0 = llvm.mlir.zero : !llvm.ptr
  llvm.return %0 : !llvm.ptr
}

Definition at line 75 of file LowerSMTToZ3LLVM.cpp.

Member Function Documentation

◆ create()

SMTGlobalsHandler SMTGlobalsHandler::create	(	OpBuilder &	builder,
		ModuleOp	module
	)

static

Creates the LLVM global operations to store the pointers to the solver and the context and returns a 'SMTGlobalHandler' initialized with those new globals.

Definition at line 45 of file LowerSMTToZ3LLVM.cpp.

References circt::Namespace::add(), circt::SymbolCacheBase::addDefinitions(), circt::calyx::direction::get(), and circt::Namespace::newName().

Member Data Documentation

◆ ctx

const mlir::LLVM::GlobalOp circt::SMTGlobalsHandler::ctx

The global storing the pointer to the SMT context object currently active.

Definition at line 59 of file SMTToZ3LLVM.h.

◆ ctxCache

DenseMap<Block *, Value> circt::SMTGlobalsHandler::ctxCache

Definition at line 63 of file SMTToZ3LLVM.h.

◆ funcMap

DenseMap<StringAttr, mlir::LLVM::LLVMFuncOp> circt::SMTGlobalsHandler::funcMap

Definition at line 62 of file SMTToZ3LLVM.h.

◆ names

Namespace circt::SMTGlobalsHandler::names

Definition at line 61 of file SMTToZ3LLVM.h.

Referenced by SMTGlobalsHandler().

◆ solver

const mlir::LLVM::GlobalOp circt::SMTGlobalsHandler::solver

The global storing the pointer to the SMT solver object currently active.

Definition at line 56 of file SMTToZ3LLVM.h.

◆ solverCache

DenseMap<Block *, Value> circt::SMTGlobalsHandler::solverCache

Definition at line 64 of file SMTToZ3LLVM.h.

◆ stringCache

DenseMap<StringAttr, mlir::LLVM::GlobalOp> circt::SMTGlobalsHandler::stringCache

Definition at line 65 of file SMTToZ3LLVM.h.

The documentation for this struct was generated from the following files:

/home/runner/work/circt-www/circt-www/circt_src/include/circt/Conversion/SMTToZ3LLVM.h
/home/runner/work/circt-www/circt-www/circt_src/lib/Conversion/SMTToZ3LLVM/LowerSMTToZ3LLVM.cpp

Public Member Functions

Static Public Member Functions

Public Attributes