From 8f18fb1fd1f1f62081d51bb6c6bee8f6695af76a Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Wed, 22 Jul 2020 16:42:47 -0400 Subject: [PATCH 01/10] Structure new ILA unroller with SmtShim --- CMakeLists.txt | 2 +- include/ilang/ila-mngr/u_unroller_smt.h | 161 ++++++++++++++++++++++++ src/ila-mngr/CMakeLists.txt | 1 + src/ila-mngr/u_unroller_smt.cc | 47 +++++++ test/CMakeLists.txt | 1 + test/t_unroller_smt.cc | 34 +++++ 6 files changed, 245 insertions(+), 1 deletion(-) create mode 100644 include/ilang/ila-mngr/u_unroller_smt.h create mode 100644 src/ila-mngr/u_unroller_smt.cc create mode 100644 test/t_unroller_smt.cc diff --git a/CMakeLists.txt b/CMakeLists.txt index 4d833d1d1..5c7a36583 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -11,7 +11,7 @@ endif() # PROJECT # name version language # ---------------------------------------------------------------------------- # -project(ilang VERSION 1.1.2 +project(ilang VERSION 1.1.3 LANGUAGES CXX ) diff --git a/include/ilang/ila-mngr/u_unroller_smt.h b/include/ilang/ila-mngr/u_unroller_smt.h new file mode 100644 index 000000000..e8b69fa2b --- /dev/null +++ b/include/ilang/ila-mngr/u_unroller_smt.h @@ -0,0 +1,161 @@ +/// \file +/// Class UnrollerSmt, PathUnroller, and MonoUnroller - a collection of +/// ILA unrollers with SmtShim support. + +#ifndef ILANG_ILA_MNGR_U_UNROLLER_SMT_H__ +#define ILANG_ILA_MNRG_U_UNROLLER_SMT_H__ + +#include +#include +#include + +#include +#include +#include + +/// \namespace ilang +namespace ilang { + +/// \brief Base class for unrolling ILA execution in different settings. +template class UnrollerSmt { +public: + // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // + /// Constructor. + UnrollerSmt(SmtShim& smt_shim, const std::string& suffix) + : smt_gen_(smt_shim), unroller_suffix_(suffix) {} + + // ------------------------- METHODS -------------------------------------- // + // + // Control property/predicate beyond the transition. + // + /// Add the predicate p to be asserted globally. + inline void AssertGlobal(const ExprPtr& p) { global_pred_.insert(p); } + /// Add the predicate p to be asserted at the first step (initial condition). + inline void AssertInitial(const ExprPtr& p) { initial_pred_.insert(p); } + /// Add the predicate p to be asserted at the k-th step. + inline void AssertStep(const ExprPtr& p, const int& k) { + step_pred_[k].insert(p); + } + /// Clear all the global assertions. + inline void ClearGlobalAssertion() { global_pred_.clear(); } + /// Clear all the initial assertions. + inline void ClearInitialAssertion() { initial_pred_.clear(); } + /// Clear all the step-specific assertions. + inline void ClearStepAssertion() { step_pred_.clear(); } + + // + // Access SMT formula in the unrolled execution. + // + /// Return the SMT formula of expr at the beginning k-th step. + inline auto GetSmtCurrent(const ExprPtr& expr, const size_t& k) const { + return smt_gen_.GetShimExpr(expr, SuffixCurrent(k)); + } + /// Return the SMT formula of expr at the end of k-th step. + inline auto GetSmtNext(const ExprPtr& expr, const size_t& k) const { + return smt_gen_.GetShimExpr(expr, SuffixNext(k)); + } + /// Return the SMT function declaration of uninterpreted function func. + inline auto GetSmtFuncDecl(const FuncPtr& func) const { + return smt_gen_.GetShimFunc(func); + } + +private: + // ------------------------- MEMBERS -------------------------------------- // + /// The underlying (templated) SMT generator. + SmtShim& smt_gen_; + /// Unroller specific suffix. + const std::string unroller_suffix_; + + /// Predicates to be asserted globally. + ExprSet global_pred_; + /// Predicates to be asserted initially. + ExprSet initial_pred_; + /// Predicates to be asserted at each step. + std::map step_pred_; + + // ------------------------- HELPERS -------------------------------------- // + /// Return suffix for current state. + inline std::string SuffixCurrent(const size_t& t) const { + return std::to_string(t) + "_" + unroller_suffix_; + } + /// Return suffix for next state. + inline std::string SuffixNext(const size_t& t) const { + return std::to_string(t) + "_" + unroller_suffix_ + ".nxt"; + } + +protected: + // ------------------------- TYPES ---------------------------------------- // + typedef decltype(smt_gen_.GetShimExpr(nullptr, "")) SmtExpr; + typedef decltype(smt_gen_.GetShimFunc(nullptr)) SmtFunc; + typedef std::vector IlaExprVec; + typedef std::vector SmtExprVec; + + // ------------------------- MEMBERS -------------------------------------- // + // + IlaExprVec deciding_vars_; + // + IlaExprVec update_holder_; + // + IlaExprVec assert_holder_; + + // ------------------------- METHODS -------------------------------------- // + /// + virtual void SetDecidingVars() = 0; + + /// + virtual void MakeOneTransition(const size_t& idx) = 0; + + /// + SmtExpr Unroll_(const size_t& len, const size_t& begin); + + /// + SmtExpr UnrollWithStepsUnconnected_(const size_t& len, const size_t& begin); + +private: + // ------------------------- MEMBERS -------------------------------------- // + + // ------------------------- METHODS -------------------------------------- // + + // ------------------------- HELPERS -------------------------------------- // + +}; // class UnrollerSmt + +/// \brief Application class for unrolling a sequence of instructions. +template class PathUnroller : public UnrollerSmt { +public: + // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // + /// Constructor. + PathUnroller(SmtShim& smt_shim, const std::string& suffix = "") + : UnrollerSmt(smt_shim, suffix) {} + + // ------------------------- METHODS -------------------------------------- // + /// + auto Unroll(const InstrVec& seq, const size_t& begin = 0) { + seq_ = seq; + return this->Unroll_(seq.size(), begin); + } + + /// + auto UnrollWithStepUnconnected(const InstrVec& seq, const size_t& begin) { + seq_ = seq; + return this->UnrollWithStepsUnconnected_(seq.size(), begin); + } + +protected: + // ------------------------- METHODS -------------------------------------- // + /// + void SetDecidingVars(); + + /// + void MakeOneTransition(const size_t& idx); + +private: + // ------------------------- MEMBERS -------------------------------------- // + /// The sequence of instructions. + InstrVec seq_; + +}; // class PathUnroller + +} // namespace ilang + +#endif // ILANG_ILA_MNGR_U_UNROLLER_SMT_H__ diff --git a/src/ila-mngr/CMakeLists.txt b/src/ila-mngr/CMakeLists.txt index 8e3836c26..8c8cd824c 100644 --- a/src/ila-mngr/CMakeLists.txt +++ b/src/ila-mngr/CMakeLists.txt @@ -14,6 +14,7 @@ target_sources(${ILANG_LIB_NAME} PRIVATE ${CMAKE_CURRENT_SOURCE_DIR}/u_rewrite_expr.cc ${CMAKE_CURRENT_SOURCE_DIR}/u_rewrite_ila.cc ${CMAKE_CURRENT_SOURCE_DIR}/u_unroller.cc + ${CMAKE_CURRENT_SOURCE_DIR}/u_unroller_smt.cc ${CMAKE_CURRENT_SOURCE_DIR}/v_eq_check_crr.cc ${CMAKE_CURRENT_SOURCE_DIR}/v_eq_check_bmc.cc ${CMAKE_CURRENT_SOURCE_DIR}/v_refinement.cc diff --git a/src/ila-mngr/u_unroller_smt.cc b/src/ila-mngr/u_unroller_smt.cc new file mode 100644 index 000000000..f2d254d33 --- /dev/null +++ b/src/ila-mngr/u_unroller_smt.cc @@ -0,0 +1,47 @@ +/// \file +/// The implementation of UnrollerSmt, PathUnroller, and MonoUnroller. + +#include + +#include +#include + +namespace ilang { + +// +// UnrollerSmt +// + +template +typename UnrollerSmt::SmtExpr +UnrollerSmt::Unroll_(const size_t& len, const size_t& begin) { + return smt_gen_.GetShimExpr(nullptr, ""); // TODO +} + +template +typename UnrollerSmt::SmtExpr +UnrollerSmt::UnrollWithStepsUnconnected_(const size_t& len, + const size_t& begin) { + return smt_gen_.GetShimExpr(nullptr, ""); // TODO +} + +// +// PathUnroller +// + +template void PathUnroller::SetDecidingVars() { + // TODO +} + +template +void PathUnroller::MakeOneTransition(const size_t& idx) { + // TODO +} + +// +// Concretize SMT generators +// +template class PathUnroller; +template class PathUnroller; + +} // namespace ilang diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index c7f6b06f2..b4cad2fff 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -79,6 +79,7 @@ package_add_test(${ILANG_TEST_MAIN} t_sort.cc t_symbol.cc t_unroll_seq.cc + t_unroller_smt.cc t_util.cc t_verilog_analysis.cc t_verilog_analysis_error.cc diff --git a/test/t_unroller_smt.cc b/test/t_unroller_smt.cc new file mode 100644 index 000000000..e41a0d4cf --- /dev/null +++ b/test/t_unroller_smt.cc @@ -0,0 +1,34 @@ +/// \file +/// Unit tests for Unroller using SmtShim + +#ifdef SMTSWITCH_TEST +#include +#include +#endif // SMTSWITCH_TEST + +#include +#include +#include +#include + +#include "unit-include/util.h" + +namespace ilang { + +TEST(TestUnroller, z3) { + z3::context ctx; + Z3ExprAdapter gen(ctx); + auto shim = SmtShim(gen); + auto unroller = PathUnroller(shim); +} + +#ifdef SMTSWITCH_TEST +TEST(TestUnroller, btor) { + auto solver = smt::BoolectorSolverFactory::create(false); + auto switch_itf = SmtSwitchItf(solver); + auto shim = SmtShim(switch_itf); + auto unroller = PathUnroller(shim); +} +#endif // SMTSWITCH_TEST + +} // namespace ilang From 94d566e9dc443f73bce9330554f27039f4fc2c88 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Thu, 20 Aug 2020 21:41:53 -0400 Subject: [PATCH 02/10] Fix incorrect smt::Term construction --- src/target-smt/smt_switch_itf.cc | 36 ++++++++++++++++---------------- test/t_smt_switch_itf.cc | 12 +++++------ 2 files changed, 24 insertions(+), 24 deletions(-) diff --git a/src/target-smt/smt_switch_itf.cc b/src/target-smt/smt_switch_itf.cc index 110ca6afc..14be39119 100644 --- a/src/target-smt/smt_switch_itf.cc +++ b/src/target-smt/smt_switch_itf.cc @@ -130,20 +130,17 @@ smt::Term SmtSwitchItf::ExprConst2Term(const ExprPtr& expr) { smt::Term SmtSwitchItf::ExprOp2Term(const ExprPtr& expr, const smt::TermVec& arg_terms) { - - // XXX Boolector (maybe also others) doesn't accept INT sort for param. - // auto param_sort = solver_->make_sort(smt::INT); - auto param_sort = solver_->make_sort(smt::BV, PARAM_BIT_WIDTH); - + // construct based on the operator switch (auto expr_op_uid = asthub::GetUidExprOp(expr); expr_op_uid) { case AstUidExprOp::kNegate: { - return solver_->make_term(smt::PrimOp::Negate, arg_terms.at(0)); + return solver_->make_term(smt::PrimOp::BVNeg, arg_terms.at(0)); } case AstUidExprOp::kNot: { return solver_->make_term(smt::PrimOp::Not, arg_terms.at(0)); } case AstUidExprOp::kComplement: { - return solver_->make_term(smt::PrimOp::BVComp, arg_terms.at(0)); + // PrimOp::BVComp seems to be compare (equal) + return solver_->make_term(smt::PrimOp::BVNot, arg_terms.at(0)); } case AstUidExprOp::kAnd: { auto op = expr->is_bool() ? smt::PrimOp::And : smt::PrimOp::BVAnd; @@ -236,25 +233,28 @@ smt::Term SmtSwitchItf::ExprOp2Term(const ExprPtr& expr, arg_terms.at(1)); } case AstUidExprOp::kExtract: { - auto p0 = solver_->make_term(expr->param(0), param_sort); - auto p1 = solver_->make_term(expr->param(1), param_sort); - return solver_->make_term(smt::PrimOp::Extract, arg_terms.at(0), p0, p1); + auto op = smt::Op(smt::PrimOp::Extract, expr->param(0), expr->param(1)); + return solver_->make_term(op, arg_terms.at(0)); } case AstUidExprOp::kZeroExtend: { - auto p0 = solver_->make_term(expr->param(0), param_sort); - return solver_->make_term(smt::PrimOp::Zero_Extend, arg_terms.at(0), p0); + // the param in smt-switch (at least for btor) is the diff + auto diff = expr->param(0) - expr->arg(0)->sort()->bit_width(); + auto op = smt::Op(smt::PrimOp::Zero_Extend, diff); + return solver_->make_term(op, arg_terms.at(0)); } case AstUidExprOp::kSignedExtend: { - auto p0 = solver_->make_term(expr->param(0), param_sort); - return solver_->make_term(smt::PrimOp::Sign_Extend, arg_terms.at(0), p0); + // the param in smt-switch (at least for btor) is the diff + auto diff = expr->param(0) - expr->arg(0)->sort()->bit_width(); + auto op = smt::Op(smt::PrimOp::Sign_Extend, diff); + return solver_->make_term(op, arg_terms.at(0)); } case AstUidExprOp::kRotateLeft: { - auto p0 = solver_->make_term(expr->param(0), param_sort); - return solver_->make_term(smt::PrimOp::Rotate_Left, arg_terms.at(0), p0); + auto op = smt::Op(smt::PrimOp::Rotate_Left, expr->param(0)); + return solver_->make_term(op, arg_terms.at(0)); } case AstUidExprOp::kRotateRight: { - auto p0 = solver_->make_term(expr->param(0), param_sort); - return solver_->make_term(smt::PrimOp::Rotate_Right, arg_terms.at(0), p0); + auto op = smt::Op(smt::PrimOp::Rotate_Right, expr->param(0)); + return solver_->make_term(op, arg_terms.at(0)); } case AstUidExprOp::kImply: { return solver_->make_term(smt::PrimOp::Implies, arg_terms.at(0), diff --git a/test/t_smt_switch_itf.cc b/test/t_smt_switch_itf.cc index 60c9fa924..7965d30d5 100644 --- a/test/t_smt_switch_itf.cc +++ b/test/t_smt_switch_itf.cc @@ -60,7 +60,7 @@ TEST_F(TestSmtSwitch, OpBvNeg) { auto neg_a = -var_bv_a; auto neg_neg_a = -neg_a; auto prop = neg_neg_a != var_bv_a; - EXPECT_DEATH(CheckUnsat(prop), ".*"); + CheckUnsat(prop); } TEST_F(TestSmtSwitch, OpBoolNot) { @@ -74,7 +74,7 @@ TEST_F(TestSmtSwitch, OpBvComplement) { auto com_a = ~var_bv_a; auto com_com_a = ~com_a; auto prop = com_com_a != var_bv_a; - EXPECT_DEATH(CheckUnsat(prop), ".*"); + CheckUnsat(prop); } TEST_F(TestSmtSwitch, OpBoolAnd) { @@ -255,14 +255,14 @@ TEST_F(TestSmtSwitch, OpBvExtract) { auto a_con_b = Concat(var_bv_a, var_bv_b); auto extract_a_con_b = Extract(a_con_b, BV_SIZE - 1, 0); auto prop = extract_a_con_b != var_bv_b; - EXPECT_DEATH(CheckUnsat(prop), ".*"); + CheckUnsat(prop); } TEST_F(TestSmtSwitch, OpBvZext) { auto zext_a = ZExt(var_bv_a, 2 * BV_SIZE); auto zero_con_a = Concat(BvConst(0, BV_SIZE), var_bv_a); auto prop = zext_a != zero_con_a; - EXPECT_DEATH(CheckUnsat(prop), ".*"); + CheckUnsat(prop); } TEST_F(TestSmtSwitch, OpBvSext) { @@ -270,14 +270,14 @@ TEST_F(TestSmtSwitch, OpBvSext) { auto sext_a = SExt(pos_a, 2 * BV_SIZE); auto zero_con_a = Concat(BvConst(0, BV_SIZE), pos_a); auto prop = sext_a != zero_con_a; - EXPECT_DEATH(CheckUnsat(prop), ".*"); + CheckUnsat(prop); } TEST_F(TestSmtSwitch, OpBvRotate) { auto left_rotate_1 = LRotate(var_bv_a, 1); auto right_rotate_back = RRotate(left_rotate_1, 1); auto prop = right_rotate_back != var_bv_a; - EXPECT_DEATH(CheckUnsat(prop), ".*"); + CheckUnsat(prop); } TEST_F(TestSmtSwitch, OpBoolImply) { From c7bb40666740d12ba130ebc9990494dbbbf80f69 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Thu, 20 Aug 2020 21:48:25 -0400 Subject: [PATCH 03/10] Expose richer SmtShim interface for easy usage --- include/ilang/ilang++.h | 6 +++--- include/ilang/target-smt/smt_shim.h | 12 ++++++++++++ include/ilang/target-smt/smt_switch_itf.h | 10 ++++++++++ include/ilang/target-smt/z3_expr_adapter.h | 7 +++++++ src/ilang++.cc | 2 -- 5 files changed, 32 insertions(+), 5 deletions(-) diff --git a/include/ilang/ilang++.h b/include/ilang/ilang++.h index 1cb86cbc0..09f7d6616 100644 --- a/include/ilang/ilang++.h +++ b/include/ilang/ilang++.h @@ -11,13 +11,12 @@ #include #include - -#include - #ifdef SMTSWITCH_INTERFACE #include #endif // SMTSWITCH_INTERFACE +#include + /// \namespace ilang /// Defines the core data structure and APIs for constructing and storing ILA. namespace ilang { @@ -57,6 +56,7 @@ class Expr; class Instr; class InstrLvlAbs; class Unroller; + // forward declaration class Ila; diff --git a/include/ilang/target-smt/smt_shim.h b/include/ilang/target-smt/smt_shim.h index 45c6ff804..1d2f90a90 100644 --- a/include/ilang/target-smt/smt_shim.h +++ b/include/ilang/target-smt/smt_shim.h @@ -20,6 +20,8 @@ template class SmtShim { private: /// Reference to the underlying SMT formula generator. Generator& gen_; + /// Type alias for expression. + typedef decltype(gen_.GetShimExpr(nullptr, "")) ShimExprType; public: /// Unified interface to get expression. @@ -30,6 +32,16 @@ template class SmtShim { inline auto GetShimFunc(const FuncPtr& func) { return gen_.GetShimFunc(func); } + /// Unified interface to AND two boolean expressions. + inline auto BoolAnd(const ShimExprType& a, const ShimExprType& b) { + return gen_.BoolAnd(a, b); + } + /// Unified interface to Equal two expressions. + inline auto Equal(const ShimExprType& a, const ShimExprType& b) { + return gen_.Equal(a, b); + } + /// Return the underlying generator. + inline Generator& get() const { return gen_; } }; // class SmtShim diff --git a/include/ilang/target-smt/smt_switch_itf.h b/include/ilang/target-smt/smt_switch_itf.h index 97606130f..b75c5b118 100644 --- a/include/ilang/target-smt/smt_switch_itf.h +++ b/include/ilang/target-smt/smt_switch_itf.h @@ -30,6 +30,8 @@ class SmtSwitchItf { smt::Term GetSmtTerm(const ExprPtr& expr, const std::string& suffix = ""); /// Reset the solver and the interface. void Reset(); + /// Return the underlying SMT solver; + inline smt::SmtSolver& solver() const { return solver_; } /// Check if Term is generated. bool pre(const ExprPtr& expr); @@ -43,6 +45,14 @@ class SmtSwitchItf { } /// Unified SmtShim interface to get smt::Func. inline auto GetShimFunc(const FuncPtr& func) { return Func2Term(func); } + /// Unified SmtShim interface to AND two boolean smt::Term. + inline auto BoolAnd(const smt::Term& a, const smt::Term& b) { + return solver_->make_term(smt::PrimOp::Or, a, b); + } + /// Unified SmtShim interface to EQUAL two smt::Term. + inline auto Equal(const smt::Term& a, const smt::Term& b) { + return solver_->make_term(smt::PrimOp::Equal, a, b); + } private: /// Type for cacheing the generated expressions. diff --git a/include/ilang/target-smt/z3_expr_adapter.h b/include/ilang/target-smt/z3_expr_adapter.h index ad7184cd9..8ccfcb67a 100644 --- a/include/ilang/target-smt/z3_expr_adapter.h +++ b/include/ilang/target-smt/z3_expr_adapter.h @@ -32,6 +32,9 @@ class Z3ExprAdapter { /// Function object for getting z3 expression. void operator()(const ExprPtr& expr); + /// Return the underlying z3 context. + inline z3::context& context() const { return ctx_; } + // ------------------------- SHIM INTERFACE ------------------------------- // /// Unified SmtShim interface to get z3::expr. inline auto GetShimExpr(const ExprPtr& expr, const std::string& suffix) { @@ -41,6 +44,10 @@ class Z3ExprAdapter { inline auto GetShimFunc(const FuncPtr& func) { return func->GetZ3FuncDecl(ctx_); } + /// Unified SmtShim interface to AND two boolean z3::expr. + inline auto BoolAnd(const z3::expr& a, const z3::expr& b) { return a && b; } + /// Unified SmtShim interface to EQUAL two z3::expr. + inline auto Equal(const z3::expr& a, const z3::expr& b) { return a == b; } private: /// Type for caching the generated expressions. diff --git a/src/ilang++.cc b/src/ilang++.cc index 658702834..7a3f5aba8 100644 --- a/src/ilang++.cc +++ b/src/ilang++.cc @@ -860,14 +860,12 @@ void EnableDebug(const std::string& tag) { DebugLog::Enable(tag); } void DisableDebug(const std::string& tag) { DebugLog::Disable(tag); } #ifdef SMTSWITCH_INTERFACE - smt::Term ResetAndGetSmtTerm(smt::SmtSolver& solver, const ExprRef& expr, const std::string& suffix) { solver->reset(); auto itf = SmtSwitchItf(solver); return itf.GetSmtTerm(expr.get(), suffix); } - #endif // SMTSWITCH_INTERFACE } // namespace ilang From 08fe16745aec4d32a1864b80aebc720487de6c18 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 23 Aug 2020 13:43:08 -0400 Subject: [PATCH 04/10] Unroll instruction sequence using SmtShim --- include/ilang/ila-mngr/u_unroller_smt.h | 46 ++++++++++-- include/ilang/target-smt/smt_switch_itf.h | 2 +- src/ila-mngr/u_unroller_smt.cc | 92 ++++++++++++++++++++--- test/t_unroll_seq.cc | 5 +- test/t_unroller_smt.cc | 90 ++++++++++++++++++++-- 5 files changed, 211 insertions(+), 24 deletions(-) diff --git a/include/ilang/ila-mngr/u_unroller_smt.h b/include/ilang/ila-mngr/u_unroller_smt.h index e8b69fa2b..9496e5116 100644 --- a/include/ilang/ila-mngr/u_unroller_smt.h +++ b/include/ilang/ila-mngr/u_unroller_smt.h @@ -91,11 +91,11 @@ template class UnrollerSmt { typedef std::vector SmtExprVec; // ------------------------- MEMBERS -------------------------------------- // - // + /// IlaExprVec deciding_vars_; - // + /// IlaExprVec update_holder_; - // + /// IlaExprVec assert_holder_; // ------------------------- METHODS -------------------------------------- // @@ -112,11 +112,43 @@ template class UnrollerSmt { SmtExpr UnrollWithStepsUnconnected_(const size_t& len, const size_t& begin); private: - // ------------------------- MEMBERS -------------------------------------- // + // ------------------------- HELPERS -------------------------------------- // + /// + inline void InterpIlaExprAndAppend(const IlaExprVec& ila_expr_src, + const std::string& suffix, + SmtExprVec& smt_expr_dst) { + for (const auto& e : ila_expr_src) { + smt_expr_dst.push_back(smt_gen_.GetShimExpr(e, suffix)); + } + } - // ------------------------- METHODS -------------------------------------- // + /// + inline void InterpIlaExprAndAppend(const ExprSet& ila_expr_src, + const std::string& suffix, + SmtExprVec& smt_expr_dst) { + for (const auto& e : ila_expr_src) { + smt_expr_dst.push_back(smt_gen_.GetShimExpr(e, suffix)); + } + } - // ------------------------- HELPERS -------------------------------------- // + /// + inline void ElementWiseEqualAndAppend(const SmtExprVec& a, + const SmtExprVec& b, + SmtExprVec& smt_expr_dst) { + ILA_ASSERT(a.size() == b.size()); + for (size_t i = 0; i < a.size(); i++) { + smt_expr_dst.push_back(smt_gen_.Equal(a.at(i), b.at(i))); + } + } + + /// + inline SmtExpr ConjunctAll(const SmtExprVec& vec) const { + auto conjunct_holder = smt_gen_.GetShimExpr(asthub::BoolConst(true)); + for (const auto& e : vec) { + conjunct_holder = smt_gen_.BoolAnd(conjunct_holder, e); + } + return conjunct_holder; + } }; // class UnrollerSmt @@ -136,7 +168,7 @@ template class PathUnroller : public UnrollerSmt { } /// - auto UnrollWithStepUnconnected(const InstrVec& seq, const size_t& begin) { + auto UnrollWithStepsUnconnected(const InstrVec& seq, const size_t& begin) { seq_ = seq; return this->UnrollWithStepsUnconnected_(seq.size(), begin); } diff --git a/include/ilang/target-smt/smt_switch_itf.h b/include/ilang/target-smt/smt_switch_itf.h index b75c5b118..e7e317b69 100644 --- a/include/ilang/target-smt/smt_switch_itf.h +++ b/include/ilang/target-smt/smt_switch_itf.h @@ -47,7 +47,7 @@ class SmtSwitchItf { inline auto GetShimFunc(const FuncPtr& func) { return Func2Term(func); } /// Unified SmtShim interface to AND two boolean smt::Term. inline auto BoolAnd(const smt::Term& a, const smt::Term& b) { - return solver_->make_term(smt::PrimOp::Or, a, b); + return solver_->make_term(smt::PrimOp::And, a, b); } /// Unified SmtShim interface to EQUAL two smt::Term. inline auto Equal(const smt::Term& a, const smt::Term& b) { diff --git a/src/ila-mngr/u_unroller_smt.cc b/src/ila-mngr/u_unroller_smt.cc index f2d254d33..5665da204 100644 --- a/src/ila-mngr/u_unroller_smt.cc +++ b/src/ila-mngr/u_unroller_smt.cc @@ -3,6 +3,7 @@ #include +#include #include #include @@ -15,33 +16,104 @@ namespace ilang { template typename UnrollerSmt::SmtExpr UnrollerSmt::Unroll_(const size_t& len, const size_t& begin) { - return smt_gen_.GetShimExpr(nullptr, ""); // TODO + // reset to clean starting state + deciding_vars_.clear(); + update_holder_.clear(); + assert_holder_.clear(); + + // setup deciding variable (and the order) + SetDecidingVars(); + ILA_ASSERT(!deciding_vars_.empty()); + + // placeholder for generated SMT terms + SmtExprVec smt_holder; + + // unroll each step + for (size_t i = 0; i < len; i++) { + auto suffix = SuffixCurrent(begin + i); + auto suffix_next = SuffixCurrent(begin + i + 1); + + // proceed and update placeholders + MakeOneTransition(i); + + // append global and step-specific properties + InterpIlaExprAndAppend(global_pred_, suffix, smt_holder); + InterpIlaExprAndAppend(step_pred_[i], suffix, smt_holder); + InterpIlaExprAndAppend(assert_holder_, suffix, smt_holder); + // append initial properties + if (i == 0) { + InterpIlaExprAndAppend(initial_pred_, suffix, smt_holder); + } + + // append transition (state updates) + SmtExprVec smt_next_val; + SmtExprVec smt_next_var; + InterpIlaExprAndAppend(update_holder_, suffix, smt_next_val); + InterpIlaExprAndAppend(deciding_vars_, suffix_next, smt_next_var); + ElementWiseEqualAndAppend(smt_next_val, smt_next_var, smt_holder); + } + + { // take care of the end state + auto suffix = SuffixCurrent(len); + InterpIlaExprAndAppend(global_pred_, suffix, smt_holder); + InterpIlaExprAndAppend(step_pred_[len], suffix, smt_holder); + } + + return ConjunctAll(smt_holder); } template typename UnrollerSmt::SmtExpr UnrollerSmt::UnrollWithStepsUnconnected_(const size_t& len, const size_t& begin) { - return smt_gen_.GetShimExpr(nullptr, ""); // TODO + // TODO + ILA_CHECK(false) << "Not implemented"; + return smt_gen_.GetShimExpr(nullptr, ""); } // // PathUnroller // +// Concretize SMT generators +template class PathUnroller; +#ifdef SMTSWITCH_INTERFACE +template class PathUnroller; +#endif // SMTSWITCH_INTERFACE + template void PathUnroller::SetDecidingVars() { - // TODO + ExprSet unique_vars; + for (const auto& instr : seq_) { + AbsKnob::InsertStt(instr, unique_vars); + } + // move to global order + this->deciding_vars_.clear(); + for (const auto& s : unique_vars) { + this->deciding_vars_.push_back(s); + } } template void PathUnroller::MakeOneTransition(const size_t& idx) { - // TODO -} + ILA_ASSERT(idx < seq_.size()); + auto instr = seq_.at(idx); -// -// Concretize SMT generators -// -template class PathUnroller; -template class PathUnroller; + // update next state function + auto CompleteStateUpdate = [](const InstrPtr& instr, const ExprPtr& s) { + auto update = instr->update(s); + return (update) ? update : s; + }; + + this->update_holder_.clear(); + for (const auto& s : this->deciding_vars_) { + this->update_holder_.push_back(CompleteStateUpdate(instr, s)); + } + + // step specific property + this->assert_holder_.clear(); + auto decode = instr->decode(); + ILA_NOT_NULL(decode); + this->assert_holder_.push_back(decode); +} } // namespace ilang diff --git a/test/t_unroll_seq.cc b/test/t_unroll_seq.cc index 412fe0c36..7d56a9516 100644 --- a/test/t_unroll_seq.cc +++ b/test/t_unroll_seq.cc @@ -34,7 +34,7 @@ class TestUnroll : public ::testing::Test { EqIlaGen ila_gen_; z3::context ctx_; - ExprPtr init_mem = NULL; + ExprPtr init_mem = nullptr; }; // class TestUnroll @@ -48,6 +48,7 @@ TEST_F(TestUnroll, InstrSeqFlatSubs) { auto unroller = new PathUnroll(ctx_); auto cstr = unroller->PathSubs(seq); + delete unroller; } TEST_F(TestUnroll, InstrSeqFlatAssn) { @@ -60,6 +61,7 @@ TEST_F(TestUnroll, InstrSeqFlatAssn) { auto unroller = new PathUnroll(ctx_); auto cstr = unroller->PathAssn(seq); + delete unroller; } TEST_F(TestUnroll, InstrSeqFlatNone) { @@ -71,6 +73,7 @@ TEST_F(TestUnroll, InstrSeqFlatNone) { auto unroller = new PathUnroll(ctx_); auto cstr = unroller->PathNone(seq); + delete unroller; } TEST_F(TestUnroll, InstrSeqSolve) { diff --git a/test/t_unroller_smt.cc b/test/t_unroller_smt.cc index e41a0d4cf..86c986dd4 100644 --- a/test/t_unroller_smt.cc +++ b/test/t_unroller_smt.cc @@ -7,28 +7,108 @@ #endif // SMTSWITCH_TEST #include -#include +#include #include #include +#include "unit-include/simple_cpu.h" #include "unit-include/util.h" namespace ilang { -TEST(TestUnroller, z3) { +#define DBG_TAG "UnrollerSmt" + +class TestUnrollerSmt : public ::testing::Test { +public: + TestUnrollerSmt() {} + ~TestUnrollerSmt() {} + + void SetUp() { + DebugLog::Enable(DBG_TAG); + + MemVal init_mem_val(0); + init_mem_val.set_data(0, GenLoad(0, 0)); + init_mem_val.set_data(1, GenLoad(1, 1)); + init_mem_val.set_data(2, GenAdd(2, 0, 1)); + init_mem_val.set_data(3, GenStore(2, 2)); + init_mem = asthub::MemConst(init_mem_val, 8, 8); + } + void TearDown() { DebugLog::Disable(DBG_TAG); } + + ExprPtr init_mem = nullptr; + + template auto UnrollTestSequence(SmtShim& shim) { + using namespace asthub; + auto m = SimpleCpu("m"); + + /* + * reg0 = Load 0 + * reg1 = Load 1 + * reg2 = reg0 + reg1 + * Store reg2 2 + */ + std::vector seq = {m->instr("Load"), m->instr("Load"), + m->instr("Add"), m->instr("Store")}; + + auto unroller = new PathUnroller(shim); + + // ILA init + for (size_t i = 0; i != m->init_num(); i++) { + unroller->AssertInitial(m->init(i)); + } + { // instruction memory + auto ir = m->state("ir"); + unroller->AssertInitial(Eq(ir, init_mem)); + } + + // concretize data + unroller->AssertStep(Eq(m->state("r0"), 7), 0); + unroller->AssertStep(Eq(m->state("r1"), 7), 0); + unroller->AssertStep(Eq(Load(m->state("mem"), 0), 3), 0); + unroller->AssertStep(Eq(Load(m->state("mem"), 1), 3), 0); + + // unroll + auto exec = unroller->Unroll(seq); + auto prop = unroller->GetSmtCurrent(Ne(Load(m->state("mem"), 2), 6), 4); + auto smt_form = shim.BoolAnd(exec, prop); + + // reset + unroller->ClearGlobalAssertion(); + unroller->ClearInitialAssertion(); + unroller->ClearStepAssertion(); + delete unroller; + + return smt_form; + }; + +}; // class TestUnrollerSmt + +TEST_F(TestUnrollerSmt, z3) { z3::context ctx; Z3ExprAdapter gen(ctx); auto shim = SmtShim(gen); - auto unroller = PathUnroller(shim); + + auto p = UnrollTestSequence(shim); + + z3::solver s(ctx); + s.add(p); + auto res = s.check(); + EXPECT_EQ(res, z3::unsat); } #ifdef SMTSWITCH_TEST -TEST(TestUnroller, btor) { +TEST_F(TestUnrollerSmt, btor) { auto solver = smt::BoolectorSolverFactory::create(false); auto switch_itf = SmtSwitchItf(solver); auto shim = SmtShim(switch_itf); - auto unroller = PathUnroller(shim); + + auto p = UnrollTestSequence(shim); + + solver->assert_formula(p); + auto res = solver->check_sat(); + EXPECT_TRUE(res.is_unsat()); } + #endif // SMTSWITCH_TEST } // namespace ilang From dc382faa8e98f6fe4c5fa3eff6ed3821598c99dc Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 23 Aug 2020 21:41:49 -0400 Subject: [PATCH 05/10] Add Debug mode in AppVeyor-based CI --- appveyor.yml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/appveyor.yml b/appveyor.yml index d27d347c8..d189fb8bf 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -2,6 +2,10 @@ version: 1.0.{build} image: Ubuntu2004 clone_depth: 1 +configuration: +- Debug +- Release + install: - sudo apt update --yes - sudo apt install --yes z3 libz3-dev bison flex gcc g++ @@ -10,7 +14,7 @@ build_script: - cd $APPVEYOR_BUILD_FOLDER - mkdir -p build - cd build -- cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_COMPILER=g++-9 +- cmake .. -DCMAKE_CXX_COMPILER=g++-9 - make -j$(nproc) - sudo make install - make test From 6b0ce12f2531d03256e2f8a853444f524277f636 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 23 Aug 2020 21:54:44 -0400 Subject: [PATCH 06/10] Update README.md --- README.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 857790309..e04367cc8 100644 --- a/README.md +++ b/README.md @@ -63,6 +63,7 @@ brew install bison flex z3 | Ubuntu 16.04 (Xenial) | gcc 7.5.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.0 | Release | | Ubuntu 18.04 (Bionic) | gcc 8.4.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4 | Debug | | Ubuntu 18.04 (Bionic) | gcc 8.4.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4 | Release | +| Ubuntu 20.04 (Focal Fosa) | gcc 9.3.0 | 3.17.0 | 4.8.7 | 3.0.4 | 2.6.4 | Debug | | Ubuntu 20.04 (Focal Fosa) | gcc 9.3.0 | 3.17.0 | 4.8.7 | 3.0.4 | 2.6.4 | Release | | OSX 10.15.4 (Catalina) | Xcode 11.4.1 | 3.17.2 | 4.8.8 | 3.6.2 | 2.5.35 | Debug | | OSX 10.15.4 (Catalina) | Xcode 11.4.1 | 3.17.2 | 4.8.8 | 3.6.2 | 2.5.35 | Release | @@ -70,7 +71,7 @@ brew install bison flex z3 ### Default Build -To build ILAng with default configuration, create a build directory and execute: +To build ILAng with default configuration, create a build directory and make: ```bash mkdir -p build && cd build @@ -78,7 +79,7 @@ cmake .. make ``` -If you are using git older than `1.8.4`, init the submodule from root and disable config-time submodule update: +If you are using git older than `1.8.4`, init the submodule from root and disable config-time submodule fetching: ```bash git submodule update --init --recursive mkdir -p build && cd build @@ -86,7 +87,7 @@ cmake .. -DILANG_FETCH_DEPS=OFF make ``` -After the build complete, run unit tests and install the library. +After the build complete, run unit tests (optional) and install the library. ```bash make run_test @@ -95,11 +96,12 @@ sudo make install ### Options -- Use `-DILANG_FETCH_DEPS=OFF` to disable config-time updating submodules for in-source dependencies. +- Use `-DILANG_FETCH_DEPS=OFF` to disable config-time fetching submodules for in-source dependencies. - Use `-DILANG_BUILD_TEST=OFF` to disalbe building the unit tests. - Use `-DILANG_BUILD_SYNTH=ON` to enable building the synthesis engine. - Use `-DILANG_BUILD_INVSYN=OFF` to disable building invariant synthesis feature. - Use `-DILANG_BUILD_SWITCH=ON` to enable building [smt-switch](https://github.com/makaimann/smt-switch.git) interface support. +- Use `-DILANG_BUILD_COSIM=ON` to enable building [Xilinx cosimulation](https://www.linuxsecrets.com/xilinx/QEMU%20SystemC%20and%20TLM%20CoSimulation.html) support. - Use `-DILANG_INSTALL_DEV=ON` to install working features. ## CMake Integration From 6683828bcd7467cc4057235f7ce97ad744f4d6ba Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 23 Aug 2020 22:22:09 -0400 Subject: [PATCH 07/10] Add comments --- include/ilang/ila-mngr/u_unroller_smt.h | 27 +++++++++++-------------- 1 file changed, 12 insertions(+), 15 deletions(-) diff --git a/include/ilang/ila-mngr/u_unroller_smt.h b/include/ilang/ila-mngr/u_unroller_smt.h index 9496e5116..6b7fab9e7 100644 --- a/include/ilang/ila-mngr/u_unroller_smt.h +++ b/include/ilang/ila-mngr/u_unroller_smt.h @@ -91,29 +91,29 @@ template class UnrollerSmt { typedef std::vector SmtExprVec; // ------------------------- MEMBERS -------------------------------------- // - /// + /// Variables on which the instruction sequence depends IlaExprVec deciding_vars_; - /// + /// State update functions of the deciding variables IlaExprVec update_holder_; - /// + /// Non-execution semantics (state update) properties IlaExprVec assert_holder_; // ------------------------- METHODS -------------------------------------- // - /// + /// Setup the deciding variabels virtual void SetDecidingVars() = 0; - /// + /// Make one transition (step) and setup the update_holder_ and assert_holder_ + /// accordingly virtual void MakeOneTransition(const size_t& idx) = 0; - /// + /// Unroll the whole sequence SmtExpr Unroll_(const size_t& len, const size_t& begin); - /// + /// Unroll the whole sequence without connecting the steps SmtExpr UnrollWithStepsUnconnected_(const size_t& len, const size_t& begin); private: // ------------------------- HELPERS -------------------------------------- // - /// inline void InterpIlaExprAndAppend(const IlaExprVec& ila_expr_src, const std::string& suffix, SmtExprVec& smt_expr_dst) { @@ -122,7 +122,6 @@ template class UnrollerSmt { } } - /// inline void InterpIlaExprAndAppend(const ExprSet& ila_expr_src, const std::string& suffix, SmtExprVec& smt_expr_dst) { @@ -131,7 +130,6 @@ template class UnrollerSmt { } } - /// inline void ElementWiseEqualAndAppend(const SmtExprVec& a, const SmtExprVec& b, SmtExprVec& smt_expr_dst) { @@ -141,7 +139,6 @@ template class UnrollerSmt { } } - /// inline SmtExpr ConjunctAll(const SmtExprVec& vec) const { auto conjunct_holder = smt_gen_.GetShimExpr(asthub::BoolConst(true)); for (const auto& e : vec) { @@ -161,13 +158,13 @@ template class PathUnroller : public UnrollerSmt { : UnrollerSmt(smt_shim, suffix) {} // ------------------------- METHODS -------------------------------------- // - /// + /// Unroll the sequence auto Unroll(const InstrVec& seq, const size_t& begin = 0) { seq_ = seq; return this->Unroll_(seq.size(), begin); } - /// + /// Unroll the sequence without connecting the steps auto UnrollWithStepsUnconnected(const InstrVec& seq, const size_t& begin) { seq_ = seq; return this->UnrollWithStepsUnconnected_(seq.size(), begin); @@ -175,10 +172,10 @@ template class PathUnroller : public UnrollerSmt { protected: // ------------------------- METHODS -------------------------------------- // - /// + /// Setup the deciding variables void SetDecidingVars(); - /// + /// Make one transition and setup holders accordingly void MakeOneTransition(const size_t& idx); private: From f6fdfa0d017782f01b7d5b35c19a41da5a331f66 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Sun, 23 Aug 2020 22:24:20 -0400 Subject: [PATCH 08/10] Fix typo in header guard --- include/ilang/ila-mngr/u_unroller_smt.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/ilang/ila-mngr/u_unroller_smt.h b/include/ilang/ila-mngr/u_unroller_smt.h index 6b7fab9e7..446b71a9c 100644 --- a/include/ilang/ila-mngr/u_unroller_smt.h +++ b/include/ilang/ila-mngr/u_unroller_smt.h @@ -3,7 +3,7 @@ /// ILA unrollers with SmtShim support. #ifndef ILANG_ILA_MNGR_U_UNROLLER_SMT_H__ -#define ILANG_ILA_MNRG_U_UNROLLER_SMT_H__ +#define ILANG_ILA_MNGR_U_UNROLLER_SMT_H__ #include #include From 9db4b589a76843305b35dec0ae21d12e870fa231 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 24 Aug 2020 02:19:43 -0400 Subject: [PATCH 09/10] Update test to fixed SmtShim --- test/t_smt_shim.cc | 24 ++++++------------------ 1 file changed, 6 insertions(+), 18 deletions(-) diff --git a/test/t_smt_shim.cc b/test/t_smt_shim.cc index d55c05be6..2d158582d 100644 --- a/test/t_smt_shim.cc +++ b/test/t_smt_shim.cc @@ -78,9 +78,7 @@ TEST_F(TestSmtShim, OpBvNeg) { auto neg_neg_a = -neg_a; auto prop = neg_neg_a != var_bv_a; CheckUnsatZ3(prop); -#ifdef SMTSWITCH_TEST - EXPECT_DEATH(CheckUnsatSwitch(prop), ".*"); -#endif // SMTSWITCH_TEST + CheckUnsatSwitch(prop); } TEST_F(TestSmtShim, OpBvComplement) { @@ -88,9 +86,7 @@ TEST_F(TestSmtShim, OpBvComplement) { auto com_com_a = ~com_a; auto prop = com_com_a != var_bv_a; CheckUnsatZ3(prop); -#ifdef SMTSWITCH_TEST - EXPECT_DEATH(CheckUnsatSwitch(prop), ".*"); -#endif // SMTSWITCH_TEST + CheckUnsatSwitch(prop); } TEST_F(TestSmtShim, OpBoolAnd) { @@ -298,9 +294,7 @@ TEST_F(TestSmtShim, OpBvExtract) { auto extract_a_con_b = Extract(a_con_b, BV_SIZE - 1, 0); auto prop = extract_a_con_b != var_bv_b; CheckUnsatZ3(prop); -#ifdef SMTSWITCH_TEST - EXPECT_DEATH(CheckUnsatSwitch(prop), ".*"); -#endif // SMTSWITCH_TEST + CheckUnsatSwitch(prop); } TEST_F(TestSmtShim, OpBvZext) { @@ -308,9 +302,7 @@ TEST_F(TestSmtShim, OpBvZext) { auto zero_con_a = Concat(BvConst(0, BV_SIZE), var_bv_a); auto prop = zext_a != zero_con_a; CheckUnsatZ3(prop); -#ifdef SMTSWITCH_TEST - EXPECT_DEATH(CheckUnsatSwitch(prop), ".*"); -#endif // SMTSWITCH_TEST + CheckUnsatSwitch(prop); } TEST_F(TestSmtShim, OpBvSext) { @@ -319,9 +311,7 @@ TEST_F(TestSmtShim, OpBvSext) { auto zero_con_a = Concat(BvConst(0, BV_SIZE), pos_a); auto prop = sext_a != zero_con_a; CheckUnsatZ3(prop); -#ifdef SMTSWITCH_TEST - EXPECT_DEATH(CheckUnsatSwitch(prop), ".*"); -#endif // SMTSWITCH_TEST + CheckUnsatSwitch(prop); } TEST_F(TestSmtShim, OpBvRotate) { @@ -329,9 +319,7 @@ TEST_F(TestSmtShim, OpBvRotate) { auto right_rotate_back = RRotate(left_rotate_1, 1); auto prop = right_rotate_back != var_bv_a; CheckUnsatZ3(prop); -#ifdef SMTSWITCH_TEST - EXPECT_DEATH(CheckUnsatSwitch(prop), ".*"); -#endif // SMTSWITCH_TEST + CheckUnsatSwitch(prop); } TEST_F(TestSmtShim, OpBoolImply) { From c92b8ea8d7b95f80bd3c55c925d1a5fc6a918039 Mon Sep 17 00:00:00 2001 From: Bo-Yuan Huang Date: Mon, 24 Aug 2020 11:04:57 -0400 Subject: [PATCH 10/10] Reorder template concretization for type deduction in clang --- src/ila-mngr/u_unroller_smt.cc | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/src/ila-mngr/u_unroller_smt.cc b/src/ila-mngr/u_unroller_smt.cc index 5665da204..5bdeff788 100644 --- a/src/ila-mngr/u_unroller_smt.cc +++ b/src/ila-mngr/u_unroller_smt.cc @@ -71,16 +71,16 @@ UnrollerSmt::UnrollWithStepsUnconnected_(const size_t& len, return smt_gen_.GetShimExpr(nullptr, ""); } -// -// PathUnroller -// - // Concretize SMT generators -template class PathUnroller; +template class UnrollerSmt; #ifdef SMTSWITCH_INTERFACE -template class PathUnroller; +template class UnrollerSmt; #endif // SMTSWITCH_INTERFACE +// +// PathUnroller +// + template void PathUnroller::SetDecidingVars() { ExprSet unique_vars; for (const auto& instr : seq_) { @@ -116,4 +116,10 @@ void PathUnroller::MakeOneTransition(const size_t& idx) { this->assert_holder_.push_back(decode); } +// Concretize SMT generators +template class PathUnroller; +#ifdef SMTSWITCH_INTERFACE +template class PathUnroller; +#endif // SMTSWITCH_INTERFACE + } // namespace ilang