[SMT] Add lowering to LLVM IR

include/circt/Conversion/Passes.h

@@ -41,6 +41,7 @@
 #include "circt/Conversion/MooreToCore.h"
 #include "circt/Conversion/PipelineToHW.h"
 #include "circt/Conversion/SCFToCalyx.h"
+#include "circt/Conversion/SMTToZ3LLVM.h"
 #include "circt/Conversion/SeqToSV.h"
 #include "circt/Conversion/SimToSV.h"
 #include "circt/Conversion/VerifToSMT.h"

include/circt/Conversion/Passes.td

@@ -729,6 +729,23 @@ def LowerArcToLLVM : Pass<"lower-arc-to-llvm", "mlir::ModuleOp"> {
   ];
 }
 
+//===----------------------------------------------------------------------===//
+// ConvertSMTToZ3LLVM
+//===----------------------------------------------------------------------===//
+
+def LowerSMTToZ3LLVM : Pass<"lower-smt-to-z3-llvm", "mlir::ModuleOp"> {
+  let summary = "Lower the SMT dialect to LLVM IR calling the Z3 API";
+  let dependentDialects = [
+    "smt::SMTDialect", "mlir::LLVM::LLVMDialect", "mlir::scf::SCFDialect",
+    "mlir::cf::ControlFlowDialect"
+  ];
+  let options = [
+    Option<"debug", "debug", "bool", "false",
+           "Insert additional printf calls printing the solver's state to "
+           "stdout (e.g. at check-sat operations) for debugging purposes">,
+  ];
+}
+
 //===----------------------------------------------------------------------===//
 // ConvertSeqToSV
 //===----------------------------------------------------------------------===//

include/circt/Conversion/SMTToZ3LLVM.h

@@ -0,0 +1,80 @@
+//===- SMTToZ3LLVM.h --------------------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_CONVERSION_SMTTOZ3LLVM_H
+#define CIRCT_CONVERSION_SMTTOZ3LLVM_H
+
+#include "circt/Support/LLVM.h"
+#include "circt/Support/Namespace.h"
+#include "mlir/Dialect/LLVMIR/LLVMDialect.h"
+#include "llvm/ADT/StringRef.h"
+#include <memory>
+
+namespace circt {
+
+#define GEN_PASS_DECL_LOWERSMTTOZ3LLVM
+#include "circt/Conversion/Passes.h.inc"
+
+/// A symbol cache for LLVM globals and functions relevant to SMT lowering
+/// patterns.
+struct SMTGlobalsHandler {
+  /// Creates the LLVM global operations to store the pointers to the solver and
+  /// the context and returns a 'SMTGlobalHandler' initialized with those new
+  /// globals.
+  static SMTGlobalsHandler create(OpBuilder &builder, ModuleOp module);
+
+  /// 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
+  /// }
+  /// ```
+  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
+  /// }
+  /// ```
+  SMTGlobalsHandler(Namespace &&names, mlir::LLVM::GlobalOp solver,
+                    mlir::LLVM::GlobalOp ctx);
+
+  /// The global storing the pointer to the SMT solver object currently active.
+  const mlir::LLVM::GlobalOp solver;
+
+  /// The global storing the pointer to the SMT context object currently active.
+  const mlir::LLVM::GlobalOp ctx;
+
+  Namespace names;
+  DenseMap<StringRef, mlir::LLVM::LLVMFuncOp> funcMap;
+  DenseMap<Block *, Value> ctxCache;
+  DenseMap<Block *, Value> solverCache;
+  DenseMap<StringRef, mlir::LLVM::GlobalOp> stringCache;
+};
+
+/// Populate the given type converter with the SMT to LLVM type conversions.
+void populateSMTToZ3LLVMTypeConverter(TypeConverter &converter);
+
+/// Add the SMT to LLVM IR conversion patterns to 'patterns'. A
+/// 'SMTGlobalHandler' object has to be passed which acts as a symbol cache for
+/// LLVM globals and functions.
+void populateSMTToZ3LLVMConversionPatterns(
+    RewritePatternSet &patterns, TypeConverter &converter,
+    SMTGlobalsHandler &globals, const LowerSMTToZ3LLVMOptions &options);
+
+} // namespace circt
+
+#endif // CIRCT_CONVERSION_SMTTOZ3LLVM_H

include/circt/Dialect/SMT/SMTOps.td

@@ -247,7 +247,7 @@ def EqOp : SMTOp<"eq", [Pure, SameTypeOperands]> {
     `and (and (= a b) (= b c)) (= c d)`.
   }];
 
-  let arguments = (ins Variadic<AnySMTType>:$inputs);
+  let arguments = (ins Variadic<AnyNonFuncSMTType>:$inputs);
   let results = (outs BoolType:$result);
 
   let builders = [
@@ -288,7 +288,7 @@ def DistinctOp : SMTOp<"distinct", [Pure, SameTypeOperands]> {
     ```
   }];
 
-  let arguments = (ins Variadic<AnySMTType>:$inputs);
+  let arguments = (ins Variadic<AnyNonFuncSMTType>:$inputs);
   let results = (outs BoolType:$result);
 
   let builders = [

integration_test/CMakeLists.txt

@@ -13,6 +13,10 @@ set(CIRCT_INTEGRATION_TEST_DEPENDS
   handshake-runner
   )
 
+if (MLIR_ENABLE_EXECUTION_ENGINE)
+  list(APPEND CIRCT_INTEGRATION_TEST_DEPENDS mlir-cpu-runner)
+endif()
+
 # If Python bindings are available to build then enable the tests.
 if(CIRCT_BINDINGS_PYTHON_ENABLED)
   list(APPEND CIRCT_INTEGRATION_TEST_DEPENDS CIRCTPythonModules)

integration_test/Dialect/SMT/basic.mlir

@@ -0,0 +1,96 @@
+// RUN: circt-opt %s --lower-smt-to-z3-llvm --canonicalize | \
+// RUN: mlir-cpu-runner -e entry -entry-point-result=void --shared-libs=%libz3 | \
+// RUN: FileCheck %s
+
+// RUN: circt-opt %s --lower-smt-to-z3-llvm=debug=true --canonicalize | \
+// RUN: mlir-cpu-runner -e entry -entry-point-result=void --shared-libs=%libz3 | \
+// RUN: FileCheck %s
+
+// REQUIRES: libz3
+// REQUIRES: mlir-cpu-runner
+
+func.func @entry() {
+  %false = llvm.mlir.constant(0 : i1) : i1
+  // CHECK: sat
+  // CHECK: Res: 1
+  smt.solver () : () -> () {
+    %c42_bv65 = smt.bv.constant #smt.bv<42> : !smt.bv<65>
+    %1 = smt.declare_fun : !smt.bv<65>
+    %2 = smt.declare_fun "a" : !smt.bv<65>
+    %3 = smt.eq %c42_bv65, %1, %2 : !smt.bv<65>
+    func.call @check(%3) : (!smt.bool) -> ()
+    smt.yield
+  }
+
+  // CHECK: sat
+  // CHECK: Res: 1
+  smt.solver () : () -> () {
+    %c0_bv8 = smt.bv.constant #smt.bv<0> : !smt.bv<8>
+    %c-1_bv8 = smt.bv.constant #smt.bv<-1> : !smt.bv<8>
+    %2 = smt.distinct %c0_bv8, %c-1_bv8 : !smt.bv<8>
+    func.call @check(%2) : (!smt.bool) -> ()
+    smt.yield
+  }
+
+  // CHECK: sat
+  // CHECK: Res: 1
+  smt.solver () : () -> () {
+    %0 = smt.declare_fun : !smt.func<(!smt.bv<4>) !smt.array<[!smt.int -> !smt.sort<"uninterpreted_sort"[!smt.bool]>]>>
+    %1 = smt.declare_fun : !smt.func<(!smt.bv<4>) !smt.array<[!smt.int -> !smt.sort<"uninterpreted_sort"[!smt.bool]>]>>
+    %c0_bv4 = smt.bv.constant #smt.bv<0> : !smt.bv<4>
+    %2 = smt.apply_func %0(%c0_bv4) : !smt.func<(!smt.bv<4>) !smt.array<[!smt.int -> !smt.sort<"uninterpreted_sort"[!smt.bool]>]>>
+    %3 = smt.apply_func %1(%c0_bv4) : !smt.func<(!smt.bv<4>) !smt.array<[!smt.int -> !smt.sort<"uninterpreted_sort"[!smt.bool]>]>>
+    %4 = smt.eq %2, %3 : !smt.array<[!smt.int -> !smt.sort<"uninterpreted_sort"[!smt.bool]>]>
+    func.call @check(%4) : (!smt.bool) -> ()
+    smt.yield
+  }
+
+  // CHECK: unsat
+  // CHECK: Res: -1
+  smt.solver (%false) : (i1) -> () {
+  ^bb0(%arg0: i1):
+    %c0_bv32 = smt.bv.constant #smt.bv<0> : !smt.bv<32>
+    %0 = scf.if %arg0 -> !smt.bv<32> {
+      %1 = smt.declare_fun : !smt.bv<32>
+      scf.yield %1 : !smt.bv<32>
+    } else {
+      %c1_bv32 = smt.bv.constant #smt.bv<-1> : !smt.bv<32>
+      scf.yield %c1_bv32 : !smt.bv<32>
+    }
+    %1 = smt.eq %c0_bv32, %0 : !smt.bv<32>
+    func.call @check(%1) : (!smt.bool) -> ()
+    smt.yield
+  }
+
+  return
+}
+
+
+func.func @check(%expr: !smt.bool) {
+  smt.assert %expr
+  %0 = smt.check sat {
+    %1 = llvm.mlir.addressof @sat : !llvm.ptr
+    llvm.call @printf(%1) vararg(!llvm.func<i32 (ptr, ...)>) : (!llvm.ptr) -> i32
+    %c1 = llvm.mlir.constant(1 : i32) : i32
+    smt.yield %c1 : i32
+  } unknown {
+    %1 = llvm.mlir.addressof @unknown : !llvm.ptr
+    llvm.call @printf(%1) vararg(!llvm.func<i32 (ptr, ...)>) : (!llvm.ptr) -> i32
+    %c0 = llvm.mlir.constant(0 : i32) : i32
+    smt.yield %c0 : i32
+  } unsat {
+    %1 = llvm.mlir.addressof @unsat : !llvm.ptr
+    llvm.call @printf(%1) vararg(!llvm.func<i32 (ptr, ...)>) : (!llvm.ptr) -> i32
+    %c-1 = llvm.mlir.constant(-1 : i32) : i32
+    smt.yield %c-1 : i32
+  } -> i32
+  %1 = llvm.mlir.addressof @res : !llvm.ptr
+  llvm.call @printf(%1, %0) vararg(!llvm.func<i32 (ptr, ...)>) : (!llvm.ptr, i32) -> i32
+  return
+}
+
+llvm.func @printf(!llvm.ptr, ...) -> i32
+llvm.mlir.global private constant @res("Res: %d\n\00") {addr_space = 0 : i32}
+llvm.mlir.global private constant @sat("sat\n\00") {addr_space = 0 : i32}
+llvm.mlir.global private constant @unsat("unsat\n\00") {addr_space = 0 : i32}
+llvm.mlir.global private constant @unknown("unknown\n\00") {addr_space = 0 : i32}

integration_test/lit.cfg.py

@@ -207,6 +207,16 @@
   tools.append('z3')
   config.available_features.add('z3')
 
+# Enable libz3 if it has been detected.
+if config.z3_library != "":
+  tools.append(ToolSubst(f"%libz3", config.z3_library))
+  config.available_features.add('libz3')
+
+# Add mlir-cpu-runner if the execution engine is built.
+if config.mlir_enable_execution_engine:
+  config.available_features.add('mlir-cpu-runner')
+  tools.append('mlir-cpu-runner')
+
 # Add circt-verilog if the Slang frontend is enabled.
 if config.slang_frontend_enabled:
   config.available_features.add('slang')

integration_test/lit.site.cfg.py.in

@@ -54,6 +54,8 @@ config.bindings_python_enabled = @CIRCT_BINDINGS_PYTHON_ENABLED@
 config.bindings_tcl_enabled = @CIRCT_BINDINGS_TCL_ENABLED@
 config.lec_enabled = "@CIRCT_LEC_ENABLED@"
 config.z3_path = "@Z3_PATH@"
+config.z3_library = "@Z3_LIBRARIES@"
+config.mlir_enable_execution_engine = "@MLIR_ENABLE_EXECUTION_ENGINE@"
 config.slang_frontend_enabled = "@CIRCT_SLANG_FRONTEND_ENABLED@"
 config.arcilator_jit_enabled = @ARCILATOR_JIT_ENABLED@
 config.driver = "@CIRCT_SOURCE_DIR@/tools/circt-rtl-sim/driver.cpp"

lib/CAPI/Conversion/CMakeLists.txt

@@ -32,6 +32,7 @@ add_mlir_public_c_api_library(CIRCTCAPIConversion
   CIRCTSCFToCalyx
   CIRCTSeqToSV
   CIRCTSimToSV
+  CIRCTSMTToZ3LLVM
   CIRCTCFToHandshake
   CIRCTVerifToSMT
   CIRCTVerifToSV

lib/Conversion/CMakeLists.txt

@@ -29,6 +29,7 @@ add_subdirectory(SeqToSV)
 add_subdirectory(SimToSV)
 add_subdirectory(CFToHandshake)
 add_subdirectory(VerifToSMT)
+add_subdirectory(SMTToZ3LLVM)
 add_subdirectory(VerifToSV)
 add_subdirectory(CalyxNative)
 

lib/Conversion/SMTToZ3LLVM/CMakeLists.txt

@@ -0,0 +1,18 @@
+add_circt_conversion_library(CIRCTSMTToZ3LLVM
+  LowerSMTToZ3LLVM.cpp
+
+  DEPENDS
+  CIRCTConversionPassIncGen
+
+  LINK_COMPONENTS
+  Core
+
+  LINK_LIBS PUBLIC
+  CIRCTSMT
+  CIRCTSupport
+  MLIRLLVMCommonConversion
+  MLIRSCFToControlFlow
+  MLIRControlFlowToLLVM
+  MLIRFuncToLLVM
+  MLIRTransforms
+)