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.

	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.

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.

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

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

Namespace	names

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

DenseMap< Block *, Value >	ctxCache

DenseMap< Block *, Value >	solverCache

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

llvm::DenseSet< StringAttr >	traceFunctionNames
	Names of outlined solver functions that emit BMC counterexamples.

llvm::DenseSet< StringAttr >	traceEmissionFunctionNames
	Names of outlined solver functions whose final argument points to the generated flag tracking whether a counterexample was already emitted.

Detailed Description

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

Definition at line 26 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 87 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 82 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 52 of file LowerSMTToZ3LLVM.cpp.

References circt::Namespace::add(), circt::SymbolCacheBase::addDefinitions(), names, 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 60 of file SMTToZ3LLVM.h.

◆ ctxCache

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

Definition at line 64 of file SMTToZ3LLVM.h.

◆ funcMap

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

Definition at line 63 of file SMTToZ3LLVM.h.

◆ names

Namespace circt::SMTGlobalsHandler::names

Definition at line 62 of file SMTToZ3LLVM.h.

Referenced by create(), and SMTGlobalsHandler().

◆ solver

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

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

Definition at line 57 of file SMTToZ3LLVM.h.

◆ solverCache

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

Definition at line 65 of file SMTToZ3LLVM.h.

◆ stringCache

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

Definition at line 66 of file SMTToZ3LLVM.h.

◆ traceEmissionFunctionNames

llvm::DenseSet<StringAttr> circt::SMTGlobalsHandler::traceEmissionFunctionNames

Names of outlined solver functions whose final argument points to the generated flag tracking whether a counterexample was already emitted.

This is a subset of traceFunctionNames.

Definition at line 73 of file SMTToZ3LLVM.h.

◆ traceFunctionNames

llvm::DenseSet<StringAttr> circt::SMTGlobalsHandler::traceFunctionNames

Names of outlined solver functions that emit BMC counterexamples.

Names remain stable when func.func operations are converted to llvm.func.

Definition at line 69 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