CIRCT  19.0.0git
Public Member Functions | Static Public Member Functions | Public Attributes | List of all members
circt::SMTGlobalsHandler Struct Reference

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

#include <SMTToZ3LLVM.h>

Collaboration diagram for circt::SMTGlobalsHandler:
Collaboration graph
[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
}
const mlir::LLVM::GlobalOp ctx
The global storing the pointer to the SMT context object currently active.
Definition: SMTToZ3LLVM.h:59

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: