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/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 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 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..446b71a9c --- /dev/null +++ b/include/ilang/ila-mngr/u_unroller_smt.h @@ -0,0 +1,190 @@ +/// \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_MNGR_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 -------------------------------------- // + /// 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) { + for (const auto& e : ila_expr_src) { + smt_expr_dst.push_back(smt_gen_.GetShimExpr(e, suffix)); + } + } + + 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)); + } + } + + 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 + +/// \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 -------------------------------------- // + /// 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); + } + +protected: + // ------------------------- METHODS -------------------------------------- // + /// Setup the deciding variables + void SetDecidingVars(); + + /// Make one transition and setup holders accordingly + 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/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..e7e317b69 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::And, 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/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..5bdeff788 --- /dev/null +++ b/src/ila-mngr/u_unroller_smt.cc @@ -0,0 +1,125 @@ +/// \file +/// The implementation of UnrollerSmt, PathUnroller, and MonoUnroller. + +#include + +#include +#include +#include + +namespace ilang { + +// +// UnrollerSmt +// + +template +typename UnrollerSmt::SmtExpr +UnrollerSmt::Unroll_(const size_t& len, const size_t& begin) { + // 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) { + // TODO + ILA_CHECK(false) << "Not implemented"; + return smt_gen_.GetShimExpr(nullptr, ""); +} + +// Concretize SMT generators +template class UnrollerSmt; +#ifdef SMTSWITCH_INTERFACE +template class UnrollerSmt; +#endif // SMTSWITCH_INTERFACE + +// +// PathUnroller +// + +template void PathUnroller::SetDecidingVars() { + 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) { + ILA_ASSERT(idx < seq_.size()); + auto instr = seq_.at(idx); + + // 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); +} + +// Concretize SMT generators +template class PathUnroller; +#ifdef SMTSWITCH_INTERFACE +template class PathUnroller; +#endif // SMTSWITCH_INTERFACE + +} // namespace ilang 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 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/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_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) { 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) { 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 new file mode 100644 index 000000000..86c986dd4 --- /dev/null +++ b/test/t_unroller_smt.cc @@ -0,0 +1,114 @@ +/// \file +/// Unit tests for Unroller using SmtShim + +#ifdef SMTSWITCH_TEST +#include +#include +#endif // SMTSWITCH_TEST + +#include +#include +#include +#include + +#include "unit-include/simple_cpu.h" +#include "unit-include/util.h" + +namespace ilang { + +#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 p = UnrollTestSequence(shim); + + z3::solver s(ctx); + s.add(p); + auto res = s.check(); + EXPECT_EQ(res, z3::unsat); +} + +#ifdef SMTSWITCH_TEST +TEST_F(TestUnrollerSmt, btor) { + auto solver = smt::BoolectorSolverFactory::create(false); + auto switch_itf = SmtSwitchItf(solver); + auto shim = SmtShim(switch_itf); + + auto p = UnrollTestSequence(shim); + + solver->assert_formula(p); + auto res = solver->check_sat(); + EXPECT_TRUE(res.is_unsat()); +} + +#endif // SMTSWITCH_TEST + +} // namespace ilang