diff --git a/.travis.yml b/.travis.yml index 0feb85480..4d1233cc1 100644 --- a/.travis.yml +++ b/.travis.yml @@ -8,27 +8,26 @@ git: depth: 1 submodules: false -sudo: required - language: cpp env: global: - secure: "RwHto3MzZ2KTsGK2LiCKCxdN/xzuWiCTO+2+zhfPjVujGMx84QdMHC5fRu94VoJ5PdZ5QHwoWy3jqQ0f2PJE7oRQe28w/ENY32yDl/ziRjY1U6k4p2pcfgYQtsyyof60mL+yG6Yzz4hlJ74uQ+arhdvyAYYvliyvUiHkLgp4XvJhmsqpogkL89pERAeZ32Xg22ajzXZD5tcWQ7CbCDVKOE0KrwktU3UG08VxMmgfjKG+rU1MKj5R8rXtwZrMzqEAzosTEK0miZYJcgO0pVStCeAC2UAZllEpWXaR2EW5plb/hXRmFjRSlWflasGzJ7VB6mZ95w4xm2DICKYgcrwPWgiMnwoEByrJBh0M7xBzU1MTFmbiqB5wSSsWfVA7zv+SLmD4mCww4HKxAkE2cDJ3MOAvK8bp1vCULBCMMmbVFNGQgBprZKoxUlpQLNn+y9C6pQoaCej9/KVdkyiSQ8SM2vXDoS4/CGnoeaOAoNpu5mkPmDk7RRjIPjdS7by9xycYXAoUVVty/EZideCrYswe1KvH87GK6Fd91XITHuhuc/Aw4Jg0zXjxx6dcHbjZKuYN5MgNMx4IWK+lNiKPyLGO1/AnFG1UP+CpOC6QE8XZNhcnvn3q4r6c+v/QbeoEE7O/XOXqJDSEumJ5b2psBuoktl52azKgUqMtDzuTWjv6BvY=" + - MATRIX_EVAL="CC=gcc-7 && CXX=g++-7" cache: directories: - $HOME/_cache -matrix: +jobs: include: - - name: "linux-gcc" + - name: "xenial" os: linux dist: xenial - compiler: gcc before_install: - gem install coveralls-lcov + - eval "${MATRIX_EVAL}" before_script: - mkdir -p $TRAVIS_BUILD_DIR/build - source $TRAVIS_BUILD_DIR/scripts/travis/clean-coverage.sh $TRAVIS_BUILD_DIR/build @@ -40,7 +39,6 @@ matrix: - name: "coverity" os: linux dist: xenial - compiler: gcc addons: coverity_scan: project: @@ -52,14 +50,18 @@ matrix: branch_pattern: coverity_scan apt: update: true + sources: + - ubuntu-toolchain-r-test packages: - flex - bison - z3 - libz3-dev + - g++-7 before_install: - - echo -n | openssl s_client -connect https://scan.coverity.com:443 | sed -ne '/-BEGIN CERTIFICATE-/,/-END CERTIFICATE-/p' | sudo tee -a /etc/ssl/certs/ca- + - echo -n | openssl s_client -connect https://scan.coverity.com:443 | sed -ne '/-BEGIN CERTIFICATE-/,/-END CERTIFICATE-/p' | sudo tee -a /etc/ssl/certs/ca- before_script: + - eval "${MATRIX_EVAL}" - source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR script: - source $TRAVIS_BUILD_DIR/scripts/travis/build-static.sh $TRAVIS_BUILD_DIR @@ -67,6 +69,8 @@ matrix: addons: apt: update: true + sources: + - ubuntu-toolchain-r-test packages: - lcov - flex @@ -74,6 +78,7 @@ addons: - libboost-all-dev - z3 - libz3-dev + - g++-7 notifications: email: false diff --git a/CMakeLists.txt b/CMakeLists.txt index e166b3b6a..397749c2a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -11,7 +11,7 @@ endif() # PROJECT # name version language # ---------------------------------------------------------------------------- # -project(ilang VERSION 1.0.5 +project(ilang VERSION 1.1.0 LANGUAGES CXX ) @@ -115,7 +115,7 @@ add_subdirectory(src) include(CMakePackageConfigHelpers) write_basic_package_version_file( ${ILANG_CMAKE_VERSION_CONFIG_FILE} - COMPATIBILITY SameMajorVersion # AnyNewVersion + COMPATIBILITY AnyNewerVersion ) ## diff --git a/README.md b/README.md index 369ea5574..3e95329c7 100644 --- a/README.md +++ b/README.md @@ -37,38 +37,38 @@ ILAng requires CMake (3.9.6 or above) and compilers with C++17 support. To install dependencies on Debian-based Linux: ```bash -apt-get install bison flex libboost-all-dev z3 libz3-dev +apt-get install bison flex z3 libz3-dev ``` To install dependencies (except z3) on Fedora-based Linux: ```bash -yum install bison flex boost boost-python boost-devel +yum install bison flex ``` To install dependencies on OSX: ```bash -brew install bison flex boost boost-python z3 +brew install bison flex z3 ``` - The [z3](https://github.com/Z3Prover/z3) SMT solver (over 4.4.0) is required. Detailed instruction for building latest z3 can be found [here](https://github.com/Z3prover/z3#building-z3-using-make-and-gccclang). - The [Boost](https://www.boost.org) package is required only if you want to build the synthesis engine (default `OFF`). -#### Regression Environments - -| OS | Compiler | CMake | z3 | Boost | Bison | Flex | Build | -| ------------------------- | ------------ | ------ | ----- | ----- | ----- | ------ | ------- | -| Ubuntu 16.04 (Xenial) | clang 7.0.0 | 3.12.4 | 4.4.1 | 1.58 | 3.0.4 | 2.6.0 | Debug | -| Ubuntu 16.04 (Xenial) | gcc 5.4.0 | 3.12.4 | 4.4.1 | 1.58 | 3.0.4 | 2.6.0 | Debug | -| Ubuntu 16.04 (Xenial) | gcc 5.4.0 | 3.17.0 | 4.4.1 | 1.58 | 3.0.4 | 2.6.0 | Release | -| Ubuntu 18.04 (Bionic) | clang 6.0.0 | 3.10.2 | 4.4.1 | 1.65 | 3.0.4 | 2.6.4 | Debug | -| Ubuntu 18.04 (Bionic) | gcc 7.5.0 | 3.10.2 | 4.4.1 | 1.65 | 3.0.4 | 2.6.4 | Debug | -| Ubuntu 18.04 (Bionic) | gcc 7.5.0 | 3.17.0 | 4.4.1 | 1.65 | 3.0.4 | 2.6.4 | Release | -| Ubuntu 20.04 (Focal Fosa) | gcc 7.4.0 | 3.17.0 | 4.4.1 | - | 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 | -| Windows Server 2016 | VS 2017 | 3.17.2 | 4.8.8 | - | 3.3.2 | 2.6.4 | Release | +#### CI Environments + +| OS | Compiler | CMake | z3 | Bison | Flex | Build | +| ------------------------- | ------------ | ------ | ----- | ----- | ------ | ------- | +| Ubuntu 16.04 (Xenial) | clang 7.0.0 | 3.12.4 | 4.4.1 | 3.0.4 | 2.6.0 | Debug | +| Ubuntu 16.04 (Xenial) | gcc 7.5.0 | 3.12.4 | 4.4.1 | 3.0.4 | 2.6.0 | Debug | +| Ubuntu 16.04 (Xenial) | gcc 7.5.0 | 3.17.0 | 4.4.1 | 3.0.4 | 2.6.0 | Release | +| Ubuntu 18.04 (Bionic) | clang 6.0.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4 | Debug | +| Ubuntu 18.04 (Bionic) | gcc 7.5.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4 | Debug | +| Ubuntu 18.04 (Bionic) | gcc 7.5.0 | 3.17.0 | 4.4.1 | 3.0.4 | 2.6.4 | Release | +| Ubuntu 20.04 (Focal Fosa) | gcc 7.4.0 | 3.17.0 | 4.4.1 | 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 | +| Windows Server 2016 | VS 2017 | 3.17.2 | 4.8.8 | 3.3.2 | 2.6.4 | Release | ### Default Build diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 3a4bfe3e3..1c03a137e 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -70,7 +70,7 @@ jobs: - script: | mkdir -p build cd build - cmake .. -DCMAKE_BUILD_TYPE=Release -DILANG_BUILD_SYNTH=ON + cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_COMPILER=g++-7 cmake --build . sudo cmake --build . --target install cmake --build . --target test @@ -91,7 +91,7 @@ jobs: - script: | mkdir -p build cd build - cmake .. -DCMAKE_BUILD_TYPE=Release -DILANG_BUILD_SYNTH=ON + cmake .. -DCMAKE_BUILD_TYPE=Release cmake --build . sudo cmake --build . --target install cmake --build . --target test diff --git a/include/ilang/ila-handler/eq_check.h b/include/ilang/ila-handler/eq_check.h deleted file mode 100644 index 8e240dcde..000000000 --- a/include/ilang/ila-handler/eq_check.h +++ /dev/null @@ -1,28 +0,0 @@ -/// \file -/// The header for checking the equivalence of two ILAs. - -#ifndef ILANG_ILA_HANDLER_EQ_CHECK_H__ -#define ILANG_ILA_HANDLER_EQ_CHECK_H__ - -#include - -/// \namespace ilang -namespace ilang { - -/// \brief Check if two ILAs have an exact same architecture, i.e., at the -/// highest level of hierarchy. -/// \param[in] a first ILA. -/// \param[in] b second ILA. -/// \param[in] update check update if true. -bool CheckEqSameArch(const Ila& a, const Ila& b, bool update = true); - -/// \brief Check if two ILAs have an exact same micro-architecture. That is, -/// they have a same architecture at every level in the hierarchy. -/// \param[in] a first ILA. -/// \param[in] b second ILA. -/// \param[in] update check update if true. -bool CheckEqSameMicroArch(const Ila& a, const Ila& b, bool update = true); - -}; // namespace ilang - -#endif // ILANG_ILA_HANDLER_EQ_CHECK_H__ diff --git a/include/ilang/ilang++.h b/include/ilang/ilang++.h index 32b306e76..92ce5615d 100644 --- a/include/ilang/ilang++.h +++ b/include/ilang/ilang++.h @@ -112,6 +112,8 @@ class ExprRef { int addr_width() const; /// Return the data bit-width if is memory; return -1 otherwise. int data_width() const; + /// Return the expression name as std::string. + std::string name() const; // ------------------------- METHODS -------------------------------------- // /****************************************************************************/ @@ -393,6 +395,10 @@ class FuncRef { /// Default destructor. ~FuncRef(); + // ------------------------- ACCESSORS/MUTATORS --------------------------- // + /// Return the function name as std::string. + std::string name() const; + // ------------------------- METHODS -------------------------------------- // /// Apply the function with no argument. ExprRef operator()() const; @@ -461,6 +467,9 @@ class InstrRef { /// Return the wrapped ILA pointer. inline InstrPtr get() const { return ptr_; } + /// Return the instruction name as std::string. + std::string name() const; + }; // class InstrRef /// \brief The wrapper of InstrLvlAbs (ILA). @@ -523,11 +532,6 @@ class Ila { /// \param[in] name child-ILA name. Ila NewChild(const std::string& name); - // ------------------------- GENERATORS --------------------------------- // - /// \brief Export an ILA as Verilog - /// \param[in] fout the output stream of the generated Verilog source. - void ExportToVerilog(std::ostream& fout) const; - // ------------------------- ACCESSORS/MUTATORS --------------------------- // /// Return the number of input variables. size_t input_num() const; @@ -570,6 +574,15 @@ class Ila { /// Return the wrapped ILA pointer. inline IlaPtr get() const { return ptr_; } + // ------------------------- UTILITIES ------------------------------------ // + /// \brief Export an ILA as Verilog + /// \param[in] fout the output stream of the generated Verilog source. + void ExportToVerilog(std::ostream& fout) const; + + /// \brief Flatten the hierarchy by lifting child-instructions as the + /// top-level parent instructions. + void FlattenHierarchy(); + }; // class Ila /******************************************************************************/ @@ -608,6 +621,9 @@ Ila ImportSynthAbstraction(const std::string& file_name, void ImportChildSynthAbstraction(const std::string& file_name, Ila& parent, const std::string& ila_name); +/// \brief Generate the SystemC simulator. +void ExportSysCSim(const Ila& ila, const std::string& dir_path); + /******************************************************************************/ // Verification. /******************************************************************************/ @@ -654,6 +670,12 @@ class IlaZ3Unroller { z3::expr UnrollPathConn(const std::vector& path, const int& init = 0); + /// \brief Unroll a path with each step connected with rewriting. + /// \param[in] path the sequence of instructions. + /// \param[in] init the starting time frame. + z3::expr UnrollPathSubs(const std::vector& path, + const int& init = 0); + /// \brief Unroll a path with each step freely defined. /// \param[in] path the sequence of instructions. /// \param[in] init the starting time frame. diff --git a/include/ilang/target-sc/ilator.h b/include/ilang/target-sc/ilator.h new file mode 100644 index 000000000..2ff338b28 --- /dev/null +++ b/include/ilang/target-sc/ilator.h @@ -0,0 +1,160 @@ +/// \file +/// The header file of ILAtor - a simulator generator of ILA models. + +#ifndef ILANG_TARGET_SC_ILATOR_H__ +#define ILANG_TARGET_SC_ILATOR_H__ + +#include +#include + +#include + +#include +#include + +/// \namespace ilang +namespace ilang { + +#define ILATOR_PRECISE_MEM + +/// \brief The ILAtor class - for CMake-based SystemC simulator generation. +class Ilator { +public: + // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // + /// Constructor with a fixed ILA model. + Ilator(const InstrLvlAbsPtr& m); + /// Destructor. + ~Ilator(); + + // ------------------------- METHODS -------------------------------------- // + /// \brief Generate the SystemC simulator. + /// \param[in] dst the directory path for the generated simulator. + void Generate(const std::string& dst); + +private: + /// Internal type of the string buffer. + typedef fmt::memory_buffer StrBuff; + /// Internal type of Expr to var name look-up table. + typedef std::unordered_map ExprVarMap; + /// Internal type to manage functions. + class CxxFunc { + public: + CxxFunc(const std::string& in_name, const ExprPtr& in_ret, + const ExprPtr& in_target = NULL) + : name(in_name), ret(in_ret), target(in_target) {} + CxxFunc(const std::string& in_name, const SortPtr& in_ret_type) + : name(in_name), ret_type(in_ret_type) {} + const std::string name = ""; + const ExprPtr ret = NULL; + const ExprPtr target = NULL; + const SortPtr ret_type = NULL; + std::vector args; + }; + + // ------------------------- MEMBERS -------------------------------------- // + /// The ILA model to generate. + InstrLvlAbsPtr m_; + + /// Generated functions (with definition). + std::map functions_; + /// Generated functions (without definition). + std::map externs_; + /// Wrapper functions to update memory values. + std::map memory_updates_; + /// Generated sources files. + std::set source_files_; + /// Constant memory that needs to be initialzied. + std::set const_mems_; + /// Global variables other than state variables. + std::set global_vars_; + + // ------------------------- HELPERS -------------------------------------- // + /// Reset all internal trackers. + void Reset(); + /// Check if the ILA model contains unsupported patterns. + bool SanityCheck() const; + /// Generation bootstrap, e.g., creating directories. + bool Bootstrap(const std::string& root); + + /// Interpret instruction semantics (decode and state updates). + bool GenerateInstrContent(const InstrPtr& instr, const std::string& dir); + /// Special handle for memory updates. + bool GenerateMemoryUpdate(const std::string& dir); + /// Special handle for constant memory. + bool GenerateConstantMemory(const std::string& dir); + /// Generate the instruction scheduler and driver. + bool GenerateExecuteKernel(const std::string& dir); + /// Generate the shared header files. + bool GenerateGlobalHeader(const std::string& dir); + /// Generate the CMake recipe and other placeholders. + bool GenerateBuildSupport(const std::string& dir); + + /// Translate expression node to SystemC statements. + bool RenderExpr(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut); + /// Translation routine entry point. + void DfsExpr(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut); + /// Translation routine for variable. + void DfsVar(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) const; + /// Translation routine for constant. + void DfsConst(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut); + /// Translation routine for operation. + void DfsOp(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut); + /// Translation routine for memory type operation. + void DfsOpMemory(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut); + /// Translation routine for function application. + void DfsOpAppFunc(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut); + /// Translation routine for non-regular operation. + void DfsOpSpecial(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut); + /// Translation routine for regular operation. + void DfsOpRegular(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) const; + + /// Request a function with the specified name and return var. + CxxFunc* RegisterFunction(const std::string& func_name, + ExprPtr return_expr = NULL); + /// Request a function simulating the uninterpreted function. + CxxFunc* RegisterExternalFunc(const FuncPtr& func); + /// Request a wrapping function for memory operation. + CxxFunc* RegisterMemoryUpdate(const ExprPtr& expr); + + /// Start function definition. + void BeginFuncDef(CxxFunc* func, StrBuff& buff) const; + /// Finish function definition. + void EndFuncDef(CxxFunc* func, StrBuff& buff) const; + /// Write function declaration. + void WriteFuncDecl(CxxFunc* func, StrBuff& buff) const; + /// Record and write the source to file. + void CommitSource(const std::string& file_name, const std::string& dir, + const StrBuff& buff); + + /// Get the project name. + inline std::string GetProjectName() const { return m_->name().str(); } + /// Create a local variable name. + static inline std::string GetLocalVar(const ExprVarMap& lut) { + return fmt::format("local_var_{}", lut.size()); + } + /// Get the type of expr in SystemC. + static inline std::string GetCxxType(const ExprPtr& expr) { + return GetCxxType(expr->sort()); + } + /// Get the type of sort in SystemC. + static std::string GetCxxType(const SortPtr& sort); + /// Get the variable name in SystemC. + static std::string GetCxxName(const ExprPtr& expr); + /// Get the decode function name of the instruction. + static std::string GetDecodeFuncName(const InstrPtr& instr); + /// Get the state update function name of the instruction. + static std::string GetUpdateFuncName(const InstrPtr& instr); + /// Get the memory update function name. + static std::string GetMemoryFuncName(const ExprPtr& expr); + /// Helper for look up variable name in the table. + inline std::string LookUp(const ExprPtr& e, const ExprVarMap& lut) const { + auto pos = lut.find(e); + ILA_ASSERT(pos != lut.end()); + return pos->second; + } + +}; // class Ilator + +} // namespace ilang + +#endif // ILANG_TARGET_SC_ILATOR_H__ diff --git a/include/ilang/util/fs.h b/include/ilang/util/fs.h index 9613cf241..2e00bd973 100644 --- a/include/ilang/util/fs.h +++ b/include/ilang/util/fs.h @@ -13,6 +13,9 @@ namespace ilang { +/// Check if path exist. +bool os_portable_exist(const std::string& path); + /// Create a dir, true -> suceeded , ow false bool os_portable_mkdir(const std::string& dir); diff --git a/scripts/travis/build.sh b/scripts/travis/build.sh index 3d4f23e38..05def505d 100644 --- a/scripts/travis/build.sh +++ b/scripts/travis/build.sh @@ -38,7 +38,7 @@ sudo make install cd $CI_BUILD_DIR mkdir -p build cd build -cmake .. -DCMAKE_BUILD_TYPE=Debug -DILANG_BUILD_COV=ON -DILANG_BUILD_SWITCH=ON -DILANG_BUILD_SYNTH=ON +cmake .. -DCMAKE_BUILD_TYPE=Debug -DILANG_BUILD_COV=ON -DILANG_BUILD_SWITCH=ON make -j$(nproc) sudo make install make run_test diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6a8d44f05..357b420cc 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -124,7 +124,7 @@ if(NOT TARGET fmt::fmt) find_package(fmt REQUIRED) endif() -target_link_libraries(${ILANG_LIB_NAME} PRIVATE fmt::fmt) +target_link_libraries(${ILANG_LIB_NAME} PUBLIC fmt::fmt) ## ## verilog parser diff --git a/src/ila-handler/CMakeLists.txt b/src/ila-handler/CMakeLists.txt deleted file mode 100644 index ab17907fe..000000000 --- a/src/ila-handler/CMakeLists.txt +++ /dev/null @@ -1,7 +0,0 @@ -# ---------------------------------------------------------------------------- # -# source -# ---------------------------------------------------------------------------- # -target_sources(${ILANG_LIB_NAME} PRIVATE - ${CMAKE_CURRENT_SOURCE_DIR}/eq_check.cc -) - diff --git a/src/ila-handler/eq_check.cc b/src/ila-handler/eq_check.cc deleted file mode 100644 index 2c8ee6a18..000000000 --- a/src/ila-handler/eq_check.cc +++ /dev/null @@ -1,89 +0,0 @@ -/// \file -/// The implementation for checking the equivalence of two ILAs. - -#include - -#include -#include -#include -#include - -namespace ilang { - -bool CheckEqSameMicroArch(const Ila& a, const Ila& b, bool update) { - auto ma = a.get(); - auto mb = b.get(); - - ILA_NOT_NULL(ma); - ILA_NOT_NULL(mb); - - if (ma->state_num() != mb->state_num()) { - ILA_INFO << "#state mismatch"; - return false; - } - - if (ma->input_num() != mb->input_num()) { - ILA_INFO << "#input mismatch"; - return false; - } - - if (ma->instr_num() != mb->instr_num()) { - ILA_INFO << "#instruction mismatch"; - return false; - } - - auto relation = RelationMap::New(); - - for (decltype(ma->input_num()) i = 0; i != ma->input_num(); i++) { - auto inp_a = ma->input(i); - auto inp_b = mb->input(inp_a->name().str()); - if (inp_b && (inp_a->sort() == inp_b->sort())) { - relation->add(ExprFuse::Eq(inp_a, inp_b)); - } else { - ILA_INFO << "No corresponding input " << inp_a << " found"; - return false; - } - } - - for (decltype(ma->state_num()) i = 0; i != ma->state_num(); i++) { - auto var_a = ma->state(i); - auto var_b = mb->state(var_a->name().str()); - if (var_b && (var_a->sort() == var_b->sort())) { - relation->add(ExprFuse::Eq(var_a, var_b)); - } else { - ILA_INFO << "No corresponding state var " << var_a << " found"; - return false; - } - } - - auto refinement_a = nullptr; - auto refinement_b = nullptr; - - auto GetFlatRefinement = [=](InstrLvlAbsPtr m, InstrPtr instr) { - // target - auto ref = RefinementMap::New(); - ref->set_tgt(instr); - - // apply - ref->set_appl(instr->decode()); - - // flush - auto has_instr = ExprFuse::BoolConst(false); - for (unsigned i = 0; i < m->instr_num(); i++) { - has_instr = ExprFuse::Or(has_instr, m->instr(i)->decode()); - } - ref->set_flush(ExprFuse::Not(has_instr)); - - // ready - // fix bound 1? - }; - - if (ma->child_num() != mb->child_num()) { - return false; - } - - return true; -} - -}; // namespace ilang - diff --git a/src/ila-mngr/u_abs_knob.cc b/src/ila-mngr/u_abs_knob.cc index 2ca229ad8..432f4b0eb 100644 --- a/src/ila-mngr/u_abs_knob.cc +++ b/src/ila-mngr/u_abs_knob.cc @@ -180,6 +180,12 @@ void InsertInstr(const InstrLvlAbsCnstPtr m, InstrVec& instrs) { } } +InstrVec GetInstr(const InstrLvlAbsCnstPtr m) { + auto instrs = InstrVec(); + InsertInstr(m, instrs); + return instrs; +} + void InsertInstrTree(const InstrLvlAbsCnstPtr top, InstrVec& instrs) { auto f = FuncObjInsertILAInstr(instrs); top->DepthFirstVisit(f); diff --git a/src/ila-mngr/u_rewrite_ila.cc b/src/ila-mngr/u_rewrite_ila.cc index b4e3d5c7f..82587d77e 100644 --- a/src/ila-mngr/u_rewrite_ila.cc +++ b/src/ila-mngr/u_rewrite_ila.cc @@ -6,6 +6,10 @@ #include #include +// enforce parent valid condition on child-decode +#define VALID_STACK +#undef VALID_STACK + namespace ilang { InstrLvlAbsPtr FuncObjRewrIla::get(const InstrLvlAbsCnstPtr m) const { @@ -58,13 +62,13 @@ void FuncObjRewrIla::post(const InstrLvlAbsCnstPtr src) const { // nothing } -// ----------------------------------------------------------------------------------------- - /// Constructor. FuncObjFlatIla::FuncObjFlatIla(const InstrLvlAbsCnstPtr& top_, const IlaMap& ila_map, const ExprMap& expr_map) : ila_map_(ila_map), expr_map_(expr_map), top_ila_(top_) { +#ifdef VALID_STACK valid_cond_stack_.push(ExprFuse::BoolConst(true)); +#endif // VALID_STACK } bool FuncObjFlatIla::pre(const InstrLvlAbsCnstPtr src) { @@ -79,14 +83,20 @@ bool FuncObjFlatIla::pre(const InstrLvlAbsCnstPtr src) { ILA_WARN << "valid condition for " << src << " is unset"; valid_cond_ = ExprFuse::BoolConst(true); } +#ifdef VALID_STACK + valid_cond_ = AbsKnob::Rewrite(valid_cond_, expr_map_); valid_cond_stack_.push(ExprFuse::And(valid_cond_stack_.top(), valid_cond_)); const auto& hierarchical_valid_cond = valid_cond_stack_.top(); +#endif // VALID_STACK // instruction && child-program for (decltype(src->instr_num()) i = 0; i != src->instr_num(); i++) { auto i_src = src->instr(i); auto i_dst = AbsKnob::DuplInstr(i_src, dst, expr_map_, ila_map_); +#ifdef VALID_STACK auto new_decode = ExprFuse::And(i_dst->decode(), hierarchical_valid_cond); + i_dst->ForceSetDecode(new_decode); +#endif // VALID_STACK } // sequence - do we need to do this? @@ -97,7 +107,9 @@ bool FuncObjFlatIla::pre(const InstrLvlAbsCnstPtr src) { void FuncObjFlatIla::post(const InstrLvlAbsCnstPtr src) { // pop the stack +#ifdef VALID_STACK valid_cond_stack_.pop(); +#endif // VALID_STACK } } // namespace ilang diff --git a/src/ila/comp_ref_rel.cc b/src/ila/comp_ref_rel.cc index 65109ea90..160e41c85 100644 --- a/src/ila/comp_ref_rel.cc +++ b/src/ila/comp_ref_rel.cc @@ -3,8 +3,8 @@ #include +#include #include -#include namespace ilang { diff --git a/src/ilang++.cc b/src/ilang++.cc index 8d5223330..c17895757 100644 --- a/src/ilang++.cc +++ b/src/ilang++.cc @@ -4,13 +4,14 @@ #include #include +#include #include +#include #include #include #include +#include #include -#include -#include #include #ifdef SMTSWITCH_INTERFACE @@ -67,6 +68,8 @@ int ExprRef::data_width() const { return ptr_->is_mem() ? ptr_->sort()->data_width() : -1; } +std::string ExprRef::name() const { return ptr_->name().str(); } + ExprRef ExprRef::Load(const ExprRef& addr) const { auto v = ExprFuse::Load(get(), addr.get()); return ExprRef(v); @@ -522,6 +525,8 @@ FuncRef::FuncRef(const std::string& name, const SortRef& range, ptr_ = Func::New(name, range.get(), args); } +std::string FuncRef::name() const { return ptr_->name().str(); } + FuncRef::~FuncRef() {} ExprRef FuncRef::operator()() const { @@ -587,6 +592,8 @@ void InstrRef::ExportToVerilogWithChild(std::ostream& fout) const { vgen.DumpToFile(fout); } +std::string InstrRef::name() const { return ptr_->name().str(); } + /******************************************************************************/ // Ila /******************************************************************************/ @@ -685,6 +692,8 @@ void Ila::ExportToVerilog(std::ostream& fout) const { vgen.DumpToFile(fout); } +void Ila::FlattenHierarchy() { AbsKnob::FlattenIla(ptr_); } + std::ostream& operator<<(std::ostream& out, const ExprRef& expr) { return out << expr.get(); } @@ -731,6 +740,11 @@ void ImportChildSynthAbstraction(const std::string& file_name, Ila& parent, #endif } +void ExportSysCSim(const Ila& ila, const std::string& dir_path) { + auto ilator = Ilator(ila.get()); + ilator.Generate(dir_path); +} + IlaZ3Unroller::IlaZ3Unroller(z3::context& ctx, const std::string& suff) : ctx_(ctx), extra_suff_(suff) { univ_ = std::make_shared(ctx); @@ -775,6 +789,17 @@ z3::expr IlaZ3Unroller::UnrollPathConn(const std::vector& path, return u->PathAssn(seq, init); } +z3::expr IlaZ3Unroller::UnrollPathSubs(const std::vector& path, + const int& init) { + auto u = std::make_shared(ctx_, extra_suff_); + InitializeUnroller(u); + std::vector seq; + for (auto& instr : path) { + seq.push_back(instr.get()); + } + return u->PathSubs(seq, init); +} + z3::expr IlaZ3Unroller::UnrollPathFree(const std::vector& path, const int& init) { auto u = std::make_shared(ctx_, extra_suff_); diff --git a/src/target-json/json_to_ila_deserializer.cc b/src/target-json/json_to_ila_deserializer.cc index 7eec9035e..67a76467f 100644 --- a/src/target-json/json_to_ila_deserializer.cc +++ b/src/target-json/json_to_ila_deserializer.cc @@ -237,7 +237,7 @@ ExprPtr J2IDes::DesExprConst(const json& j_sort, const json& j_val) const { // bit-vector case AST_UID_SORT::BV: { auto width = j_sort.at(SERDES_SORT_WIDTH).get(); - auto value = j_val.at(SERDES_CONST_VAL).get(); + auto value = j_val.at(SERDES_CONST_VAL).get(); return ExprFuse::BvConst(value, width); } // memory (array) @@ -245,7 +245,7 @@ ExprPtr J2IDes::DesExprConst(const json& j_sort, const json& j_val) const { auto addr_width = j_sort.at(SERDES_SORT_ADDR_WIDTH).get(); auto data_width = j_sort.at(SERDES_SORT_DATA_WIDTH).get(); - auto default_value = j_val.at(SERDES_CONST_DEF).get(); + auto default_value = j_val.at(SERDES_CONST_DEF).get(); auto j_value_map = j_val.at(SERDES_CONST_MAP); auto i_value_map = MemVal::MemValMap(); diff --git a/src/target-sc/CMakeLists.txt b/src/target-sc/CMakeLists.txt index 78d1eecaf..2b407f06c 100644 --- a/src/target-sc/CMakeLists.txt +++ b/src/target-sc/CMakeLists.txt @@ -4,6 +4,8 @@ target_sources(${ILANG_LIB_NAME} PRIVATE ${CMAKE_CURRENT_SOURCE_DIR}/dfs.cc ${CMAKE_CURRENT_SOURCE_DIR}/ila_sim.cc + ${CMAKE_CURRENT_SOURCE_DIR}/ilator.cc + ${CMAKE_CURRENT_SOURCE_DIR}/ilator_dfs.cc ${CMAKE_CURRENT_SOURCE_DIR}/sim_gen_decode.cc ${CMAKE_CURRENT_SOURCE_DIR}/sim_gen_execute.cc ${CMAKE_CURRENT_SOURCE_DIR}/sim_gen_init.cc diff --git a/src/target-sc/ilator.cc b/src/target-sc/ilator.cc new file mode 100644 index 000000000..a636c0877 --- /dev/null +++ b/src/target-sc/ilator.cc @@ -0,0 +1,676 @@ +/// \file +/// Implementation of the class Ilator. + +#include + +#include + +#include +#include +#include +#include + +#include + +/// \namespace ilang +namespace ilang { + +// +// static helpers/members +// + +static const std::string dir_app = "app"; +static const std::string dir_src = "src"; +static const std::string dir_include = "include"; +static const std::string dir_extern = "extern"; + +static std::unordered_map pivotal_id; + +size_t GetPivotalId(const size_t& id) { + if (auto pos = pivotal_id.find(id); pos == pivotal_id.end()) { + auto new_id = pivotal_id.size(); + pivotal_id.insert({id, new_id}); + return new_id; + } else { + return pos->second; + } +} + +void WriteFile(const std::string& file_path, const fmt::memory_buffer& buff) { + std::ofstream fw(file_path); + ILA_ASSERT(fw.is_open()) << "Fail opening file " << file_path; + fw << to_string(buff); + fw.close(); +} + +bool HasLoadFromStore(const ExprPtr& expr) { + auto monitor = false; + auto LoadFromStore = [&monitor](const ExprPtr& e) { + if (e->is_op()) { + if (auto uid = GetUidExprOp(e); uid == AST_UID_EXPR_OP::LOAD) { + monitor |= e->arg(0)->is_op(); + } + } + }; + expr->DepthFirstVisit(LoadFromStore); + return monitor; +} + +// +// Ilator implementation +// + +Ilator::Ilator(const InstrLvlAbsPtr& m) : m_(m) {} + +Ilator::~Ilator() { Reset(); } + +void Ilator::Generate(const std::string& dst) { + // sanity checks and initialize + if (!SanityCheck() || !Bootstrap(dst)) { + return; + } + + auto status = true; + ILA_INFO << "Start generating SystemC simulator of " << m_; + + // instruction semantics (decode and updates) + for (auto& instr : AbsKnob::GetInstrTree(m_)) { + status &= GenerateInstrContent(instr, os_portable_append_dir(dst, dir_src)); + } + + // memory updates + status &= GenerateMemoryUpdate(os_portable_append_dir(dst, dir_src)); + + // constant memory + status &= GenerateConstantMemory(os_portable_append_dir(dst, dir_src)); + + // execution kernel + status &= GenerateExecuteKernel(os_portable_append_dir(dst, dir_src)); + + // shared header (input, state, func., etc.) + status &= GenerateGlobalHeader(os_portable_append_dir(dst, dir_include)); + + // cmake support, e.g., recipe and templates + status &= GenerateBuildSupport(dst); + + // clean up if something went wrong + if (status) { + ILA_INFO << "Sucessfully generate SystemC simulator at " << dst; + } else { + ILA_ERROR << "Fail generating simulator at " << dst; +#ifdef NDEBUG + os_portable_remove_directory(dst); +#endif // NDEBUG + } +} + +void Ilator::Reset() { + // functions + for (auto f : functions_) { + delete f.second; + } + functions_.clear(); + + // externs + for (auto f : externs_) { + delete f.second; + } + externs_.clear(); + + // memory updates + for (auto f : memory_updates_) { + delete f.second; + } + memory_updates_.clear(); + + // others + source_files_.clear(); + const_mems_.clear(); + global_vars_.clear(); +} + +bool Ilator::SanityCheck() const { + // add new check here + return true; +} + +bool Ilator::Bootstrap(const std::string& root) { + Reset(); + + // create/structure project directory + auto res_mkdir = os_portable_mkdir(root); + res_mkdir &= os_portable_mkdir(os_portable_append_dir(root, dir_app)); + res_mkdir &= os_portable_mkdir(os_portable_append_dir(root, dir_extern)); + res_mkdir &= os_portable_mkdir(os_portable_append_dir(root, dir_include)); + res_mkdir &= os_portable_mkdir(os_portable_append_dir(root, dir_src)); + if (!res_mkdir) { + os_portable_remove_directory(root); + ILA_ERROR << "Fail structuring simulator direcory at " << root; + return false; + } + return true; +} + +bool Ilator::GenerateInstrContent(const InstrPtr& instr, + const std::string& dir) { + fmt::memory_buffer buff; + ExprVarMap lut; + + // include headers + fmt::format_to(buff, "#include <{}.h>\n", GetProjectName()); + + // decode function + auto decode_expr = instr->decode(); + auto decode_func = RegisterFunction(GetDecodeFuncName(instr), decode_expr); + BeginFuncDef(decode_func, buff); + lut.clear(); + if (!RenderExpr(decode_expr, buff, lut)) { + return false; + } + fmt::format_to(buff, "auto& {universal_name} = {local_name};\n", + fmt::arg("universal_name", GetCxxName(decode_expr)), + fmt::arg("local_name", LookUp(decode_expr, lut))); + EndFuncDef(decode_func, buff); + + // next state + auto update_func = RegisterFunction(GetUpdateFuncName(instr)); + BeginFuncDef(update_func, buff); + lut.clear(); + auto updated_states = instr->updated_states(); + for (auto& s : updated_states) { + if (auto update_expr = instr->update(s); !update_expr->is_mem()) { + if (!RenderExpr(update_expr, buff, lut)) { + return false; + } + } else { // memory (one copy for performance, need special handling) + if (HasLoadFromStore(update_expr)) { + return false; + } + auto placeholder = GetLocalVar(lut); + auto [it, status] = lut.insert({update_expr, placeholder}); + ILA_ASSERT(status); + auto mem_update_func = RegisterMemoryUpdate(update_expr); + fmt::format_to(buff, + "{mem_type} {placeholder};\n" + "{mem_update_func}({placeholder});\n", + fmt::arg("mem_type", GetCxxType(update_expr)), + fmt::arg("mem_update_func", mem_update_func->name), + fmt::arg("placeholder", placeholder)); + // dummy traverse collect related memory operation + fmt::memory_buffer dummy_buff; + ExprVarMap dummy_lut; + if (!RenderExpr(update_expr, dummy_buff, dummy_lut)) { + return false; + } + } + } + // update state + for (auto& s : updated_states) { + auto curr = instr->host()->state(s); + auto next = instr->update(s); + if (!curr->is_mem()) { + fmt::format_to(buff, "{current} = {next_value};\n", + fmt::arg("current", GetCxxName(curr)), + fmt::arg("next_value", LookUp(next, lut))); + } else { + fmt::format_to(buff, + "for (auto& it : {next_value}) {{\n" + " {current}[it.first] = it.second;\n" + "}}\n", + fmt::arg("current", GetCxxName(curr)), + fmt::arg("next_value", LookUp(next, lut))); + } + } + EndFuncDef(update_func, buff); + + // record and write to file + CommitSource(fmt::format("idu_{}.cc", instr->name().str()), dir, buff); + return true; +} + +bool Ilator::GenerateMemoryUpdate(const std::string& dir) { + fmt::memory_buffer buff; + ExprVarMap lut; + + int file_cnt = 0; + auto GetMemUpdateFile = [&file_cnt]() { + return fmt::format("memory_update_functions_{}.cc", file_cnt++); + }; + + auto StartNewFile = [this, &buff]() { + buff.clear(); + fmt::format_to(buff, "#include <{}.h>\n", GetProjectName()); + }; + + StartNewFile(); + + auto status = true; + for (auto mem_update_func_it : memory_updates_) { + auto& mem_update_func = mem_update_func_it.second; + ILA_NOT_NULL(mem_update_func); + auto& mem = mem_update_func->target; + + lut.clear(); + + BeginFuncDef(mem_update_func, buff); + + if (auto uid = GetUidExprOp(mem); uid == AST_UID_EXPR_OP::STORE) { + status &= RenderExpr(mem, buff, lut); + } else { // ite + status &= RenderExpr(mem->arg(0), buff, lut); + auto lut_copy = lut; + fmt::format_to(buff, "if ({}) {{\n", LookUp(mem->arg(0), lut_copy)); + status &= RenderExpr(mem->arg(1), buff, lut); + lut_copy.clear(); + fmt::format_to(buff, "}} else {{\n"); + status &= RenderExpr(mem->arg(2), buff, lut_copy); + fmt::format_to(buff, "}}\n"); + } + + EndFuncDef(mem_update_func, buff); + + if (buff.size() > 100000) { + CommitSource(GetMemUpdateFile(), dir, buff); + StartNewFile(); + } + } + + CommitSource(GetMemUpdateFile(), dir, buff); + // CommitSource("memory_update_functions.cc", dir, buff); + return status; +} + +bool Ilator::GenerateConstantMemory(const std::string& dir) { + fmt::memory_buffer buff; + fmt::format_to(buff, "#include <{}.h>\n", GetProjectName()); + + for (auto& mem : const_mems_) { + auto const_mem = std::dynamic_pointer_cast(mem); + const auto& val_map = const_mem->val_mem()->val_map(); + std::vector addr_data_pairs; + for (auto& it : val_map) { + addr_data_pairs.push_back(fmt::format(" {{{addr}, {data}}}", + fmt::arg("addr", it.first), + fmt::arg("data", it.second))); + } + fmt::format_to( + buff, + "{var_type} {project}::{var_name} = {{\n" + "{addr_data_pairs}\n" + "}};\n", + fmt::arg("var_type", GetCxxType(mem)), + fmt::arg("project", GetProjectName()), + fmt::arg("var_name", GetCxxName(mem)), + fmt::arg("addr_data_pairs", fmt::join(addr_data_pairs, ",\n"))); + } + + CommitSource("constant_memory_def.cc", dir, buff); + return true; +} + +bool Ilator::GenerateExecuteKernel(const std::string& dir) { + auto kernel_func = RegisterFunction("compute"); + fmt::memory_buffer buff; + + fmt::format_to( // headers + buff, + "#include \n" + "#include <{project}.h>\n", + fmt::arg("project", GetProjectName())); + + fmt::format_to( // logging + buff, + "static int instr_cntr = 0;\n" + "void {project}::LogInstrSequence(const std::string& instr_name) {{\n" + " instr_log << \"Instr No.\" << std::setw(5) << instr_cntr;\n" + " instr_log << instr_name << \" is activated\\n\";\n" + " instr_cntr++;\n" + "}}\n", + fmt::arg("project", GetProjectName())); + + BeginFuncDef(kernel_func, buff); + + // read in input value + for (size_t i = 0; i < m_->input_num(); i++) { + fmt::format_to(buff, "{input_name} = {input_name}_in.read();\n", + fmt::arg("input_name", GetCxxName(m_->input(i)))); + } + + // init TODO + + // instruction execution + auto ExecInstr = [this, &buff](const InstrPtr& instr, bool child) { + fmt::format_to( + buff, + "if ({decode_func_name}()) {{\n" + " {update_func_name}();\n" + " {child_counter}" + "#ifdef ILATOR_VERBOSE\n" + " LogInstrSequence(\"{instr_name}\");\n" + "#endif\n" + "}}\n", + fmt::arg("decode_func_name", GetDecodeFuncName(instr)), + fmt::arg("update_func_name", GetUpdateFuncName(instr)), + fmt::arg("child_counter", (child ? "schedule_counter++;\n" : "")), + fmt::arg("instr_name", instr->name().str())); + }; + + auto top_instrs = AbsKnob::GetInstr(m_); + auto all_instrs = AbsKnob::GetInstrTree(m_); + + // top-level instr + for (auto& instr : top_instrs) { + ExecInstr(instr, false); + } + + // child instr + fmt::format_to(buff, "while (1) {{\n" + " int schedule_counter = 0;\n"); + std::set tops(top_instrs.begin(), top_instrs.end()); + for (auto& instr : all_instrs) { + if (tops.find(instr) == tops.end()) { + ExecInstr(instr, true); + } + } + fmt::format_to(buff, " if (schedule_counter == 0) {{\n" + " break;\n" + " }}\n" + "}}\n"); + + // done + EndFuncDef(kernel_func, buff); + + CommitSource("compute.cc", dir, buff); + return true; +} + +bool Ilator::GenerateGlobalHeader(const std::string& dir) { + fmt::memory_buffer buff; + + fmt::format_to(buff, + "#include \n" + "#include \n" +#ifdef ILATOR_PRECISE_MEM + "#include \n" +#else + "#include \n" +#endif + "SC_MODULE({project}) {{\n" + " std::ofstream instr_log;\n" + " void LogInstrSequence(const std::string& instr_name);\n", + fmt::arg("project", GetProjectName())); + + // input + for (auto& var : AbsKnob::GetInp(m_)) { + fmt::format_to(buff, + " sc_in<{var_type}> {var_name}_in;\n" + " {var_type} {var_name};\n", + fmt::arg("var_type", GetCxxType(var)), + fmt::arg("var_name", GetCxxName(var))); + } + + // state and global vars (e.g., CONCAT) + for (auto& var : AbsKnob::GetSttTree(m_)) { + fmt::format_to(buff, " {var_type} {var_name};\n", + fmt::arg("var_type", GetCxxType(var)), + fmt::arg("var_name", GetCxxName(var))); + } + for (auto& var : global_vars_) { + fmt::format_to(buff, " {var_type} {var_name};\n", + fmt::arg("var_type", GetCxxType(var)), + fmt::arg("var_name", GetCxxName(var))); + } + + // memory constant + for (auto& mem : const_mems_) { + fmt::format_to(buff, " static {var_type} {var_name};\n", + fmt::arg("var_type", GetCxxType(mem)), + fmt::arg("var_name", GetCxxName(mem))); + } + + // function declaration + for (auto& func : functions_) { + WriteFuncDecl(func.second, buff); + } + for (auto& func : externs_) { + WriteFuncDecl(func.second, buff); + } + for (auto& func : memory_updates_) { + WriteFuncDecl(func.second, buff); + } + + // invoke + fmt::format_to(buff, + " SC_HAS_PROCESS({project});\n" + " {project}(sc_module_name name_) : sc_module(name_) {{\n" + " SC_METHOD(compute);\n" + " sensitive", + fmt::arg("project", GetProjectName())); + for (auto& var : AbsKnob::GetInp(m_)) { + fmt::format_to(buff, " << {input_name}_in", + fmt::arg("input_name", GetCxxName(var))); + } + fmt::format_to(buff, ";\n" + " }}\n"); + + // done + fmt::format_to(buff, "}};\n"); + + // write to file + auto file_path = os_portable_append_dir(dir, GetProjectName() + ".h"); + WriteFile(file_path, buff); + return true; +} + +bool Ilator::GenerateBuildSupport(const std::string& dir) { + fmt::memory_buffer buff; + + // CMakeLists.txt + std::vector src_files; + for (auto& f : source_files_) { + src_files.push_back( + fmt::format(" ${{CMAKE_CURRENT_SOURCE_DIR}}/{dir}/{file}", + fmt::arg("dir", dir_src), fmt::arg("file", f))); + } + fmt::format_to( + buff, + "# CMakeLists.txt for {project}\n" + "cmake_minimum_required(VERSION 3.14.0)\n" + "project({project} LANGUAGES CXX)\n" + "\n" + "option(ILATOR_VERBOSE \"Enable instruction sequence logging\" OFF)\n" + "option(JSON_SUPPORT \"Build JSON parser support\" OFF)\n" + "\n" + "find_package(SystemCLanguage CONFIG REQUIRED)\n" + "set(CMAKE_CXX_STANDARD ${{SystemC_CXX_STANDARD}})\n" + "\n" + "aux_source_directory(extern extern_src)\n" + "add_executable({project}\n" + " ${{CMAKE_CURRENT_SOURCE_DIR}}/{dir_app}/main.cc\n" + " ${{extern_src}}\n" + "{source_files}\n" + ")\n" + "\n" + "target_include_directories({project} PRIVATE {dir_include})\n" + "target_link_libraries({project} SystemC::systemc)\n" + "if(${{ILATOR_VERBOSE}})\n" + " target_compile_definitions({project} PRIVATE ILATOR_VERBOSE)\n" + "endif()\n" + "if(${{JSON_SUPPORT}})\n" + " include(FetchContent)\n" + " FetchContent_Declare(\n" + " json\n" + " GIT_REPOSITORY https://github.com/nlohmann/json.git\n" + " GIT_TAG v3.8.0\n" + " )\n" + " FetchContent_MakeAvailable(json)\n" + " target_link_libraries({project} nlohmann_json::nlohmann_json)\n" + "endif()\n" + // + , + fmt::arg("project", GetProjectName()), fmt::arg("dir_app", dir_app), + fmt::arg("source_files", fmt::join(src_files, "\n")), + fmt::arg("dir_include", dir_include)); + WriteFile(os_portable_append_dir(dir, "CMakeLists.txt"), buff); + + // dummy main function if not exist + auto app_template = + os_portable_append_dir(os_portable_append_dir(dir, dir_app), "main.cc"); + if (!os_portable_exist(app_template)) { + buff.clear(); + fmt::format_to(buff, + "#include <{project}.h>\n\n" + "int sc_main(int argc, char* argv[]) {{\n" + " return 0; \n" + "}}\n", + fmt::arg("project", GetProjectName())); + WriteFile(app_template, buff); + } + + return true; +} + +bool Ilator::RenderExpr(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { + try { + auto visiter = [this, &buff, &lut](const ExprPtr& e) { + DfsExpr(e, buff, lut); + }; + expr->DepthFirstVisit(visiter); + } catch (std::exception& err) { + ILA_ERROR << err.what(); + return false; + } + return true; +} + +Ilator::CxxFunc* Ilator::RegisterFunction(const std::string& func_name, + ExprPtr return_expr) { + auto func = new CxxFunc(func_name, return_expr); + auto [it, status] = functions_.insert({func->name, func}); + ILA_ASSERT(status); + return func; +} + +Ilator::CxxFunc* Ilator::RegisterExternalFunc(const FuncPtr& func) { + auto func_cxx = new CxxFunc(func->name().str(), func->out()); + auto [it, status] = externs_.insert({func_cxx->name, func_cxx}); + // uninterpreted function can have multiple occurrence + if (status) { + for (size_t i = 0; i < func->arg_num(); i++) { + it->second->args.push_back(func->arg(i)); + } + } else { + delete func_cxx; + } + return it->second; +} + +Ilator::CxxFunc* Ilator::RegisterMemoryUpdate(const ExprPtr& mem) { + auto func_cxx = new CxxFunc(GetMemoryFuncName(mem), NULL, mem); + auto [it, status] = memory_updates_.insert({func_cxx->name, func_cxx}); + // memory updates can have multiple occurrence + if (!status) { + delete func_cxx; + } + return it->second; +} + +void Ilator::BeginFuncDef(Ilator::CxxFunc* func, StrBuff& buff) const { + ILA_ASSERT(func->args.empty()); // no definition for uninterpreted funcs + + auto type = (func->ret) ? GetCxxType(func->ret) : GetCxxType(func->ret_type); + auto args = (func->target) + ? fmt::format("{}& tmp_memory", GetCxxType(func->target)) + : ""; + + fmt::format_to(buff, "{return_type} {project}::{func_name}({argument}) {{\n", + fmt::arg("return_type", type), + fmt::arg("project", GetProjectName()), + fmt::arg("func_name", func->name), fmt::arg("argument", args)); +} + +void Ilator::EndFuncDef(Ilator::CxxFunc* func, StrBuff& buff) const { + if (func->ret) { + fmt::format_to(buff, "return {};\n", GetCxxName(func->ret)); + } + fmt::format_to(buff, "}}\n"); +} + +void Ilator::WriteFuncDecl(Ilator::CxxFunc* func, StrBuff& buff) const { + auto type = (func->ret) ? GetCxxType(func->ret) : GetCxxType(func->ret_type); + auto args = (func->target) + ? fmt::format("{}& tmp_memory", GetCxxType(func->target)) + : ""; + if (!func->args.empty()) { // uninterpreted func only + ILA_NOT_NULL(func->ret_type); + std::vector arg_list; + for (const auto& a : func->args) { + arg_list.push_back(GetCxxType(a)); + } + args = fmt::format("{}", fmt::join(arg_list, ", ")); + } + + fmt::format_to(buff, " {return_type} {func_name}({argument});\n", + fmt::arg("return_type", type), + fmt::arg("func_name", func->name), fmt::arg("argument", args)); +} + +void Ilator::CommitSource(const std::string& file_name, const std::string& dir, + const StrBuff& buff) { + auto file_path = os_portable_append_dir(dir, file_name); + auto [it, ret] = source_files_.insert(file_name); + ILA_ASSERT(ret) << "Duplicated source file name " << file_name; + + WriteFile(file_path, buff); +} + +std::string Ilator::GetCxxType(const SortPtr& sort) { + if (!sort) { + return "void"; + } else if (sort->is_bool()) { + return "bool"; + } else if (sort->is_bv()) { + return fmt::format("sc_biguint<{}>", sort->bit_width()); + } else { + ILA_ASSERT(sort->is_mem()); +#ifdef ILATOR_PRECISE_MEM + return fmt::format( + "std::map, sc_biguint<{data_width}>>", + fmt::arg("addr_width", sort->addr_width()), + fmt::arg("data_width", sort->data_width())); +#else + return "std::unordered_map"; +#endif + } +} + +std::string Ilator::GetCxxName(const ExprPtr& expr) { + if (expr->is_var()) { + return fmt::format("{}_{}", expr->host()->name().str(), expr->name().str()); + } else { + return fmt::format("univ_var_{}", GetPivotalId(expr->name().id())); + } +} + +std::string Ilator::GetDecodeFuncName(const InstrPtr& instr) { + return fmt::format("decode_{host}_{instr}", + fmt::arg("host", instr->host()->name().str()), + fmt::arg("instr", instr->name().str())); +} + +std::string Ilator::GetUpdateFuncName(const InstrPtr& instr) { + return fmt::format("update_{host}_{instr}", + fmt::arg("host", instr->host()->name().str()), + fmt::arg("instr", instr->name().str())); +} + +std::string Ilator::GetMemoryFuncName(const ExprPtr& expr) { + ILA_ASSERT(expr->is_mem()); + if (auto uid = GetUidExprOp(expr); uid == AST_UID_EXPR_OP::ITE) { + return fmt::format("ite_{}", GetPivotalId(expr->name().id())); + } else { + return fmt::format("store_{}", GetPivotalId(expr->name().id())); + } +} + +} // namespace ilang diff --git a/src/target-sc/ilator_dfs.cc b/src/target-sc/ilator_dfs.cc new file mode 100644 index 000000000..697a1d694 --- /dev/null +++ b/src/target-sc/ilator_dfs.cc @@ -0,0 +1,291 @@ +/// \file +/// Implementation of DFS visitor to translate expr in Ilator. + +#include + +#include +#include + +#include + +namespace ilang { + +void Ilator::DfsExpr(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { + if (auto pos = lut.find(expr); pos == lut.end()) { + if (expr->is_var()) { + DfsVar(expr, buff, lut); + } else if (expr->is_const()) { + DfsConst(expr, buff, lut); + } else { + ILA_ASSERT(expr->is_op()); + DfsOp(expr, buff, lut); + } + } + ILA_ASSERT((expr->is_mem() && expr->is_op()) || + (lut.find(expr) != lut.end())); +} + +void Ilator::DfsVar(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) const { + auto [it, status] = lut.insert({expr, GetCxxName(expr)}); + ILA_ASSERT(status); + // no need to define new variable +} + +void Ilator::DfsConst(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { + auto local_var = GetLocalVar(lut); + auto [it, status] = lut.insert({expr, local_var}); + ILA_ASSERT(status); + + // alias for constant memory + static const char* const_mem_template = "auto& {local_var} = {const_mem};\n"; + if (expr->is_mem()) { + fmt::format_to(buff, const_mem_template, // + fmt::arg("local_var", local_var), + fmt::arg("const_mem", GetCxxName(expr))); + const_mems_.insert(expr); + return; + } + + // define new var with constant value + auto expr_const = std::dynamic_pointer_cast(expr); + std::string value = ""; + if (expr->is_bool()) { + value = expr_const->val_bool()->val() ? "true" : "false"; + } else { + ILA_ASSERT(expr->is_bv()); + value = std::to_string(expr_const->val_bv()->val()); + } + static const char* const_non_mem_template = + "{var_type} {local_var} = {const_value};\n"; + fmt::format_to(buff, const_non_mem_template, // + fmt::arg("var_type", GetCxxType(expr)), + fmt::arg("local_var", local_var), + fmt::arg("const_value", value)); +} + +void Ilator::DfsOp(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { + // store, ite-mem + if (expr->is_mem()) { + DfsOpMemory(expr, buff, lut); + return; + } + + switch (auto uid = GetUidExprOp(expr); uid) { + // apply function + case AST_UID_EXPR_OP::APP_FUNC: + DfsOpAppFunc(expr, buff, lut); + break; + // special cases + case AST_UID_EXPR_OP::LOAD: + [[fallthrough]]; + case AST_UID_EXPR_OP::CONCAT: + [[fallthrough]]; + case AST_UID_EXPR_OP::EXTRACT: + [[fallthrough]]; + case AST_UID_EXPR_OP::ZEXT: + [[fallthrough]]; + case AST_UID_EXPR_OP::SEXT: + [[fallthrough]]; + case AST_UID_EXPR_OP::IMPLY: + [[fallthrough]]; + case AST_UID_EXPR_OP::ITE: + DfsOpSpecial(expr, buff, lut); + break; + // regular operator + default: + DfsOpRegular(expr, buff, lut); + break; + }; +} + +void Ilator::DfsOpMemory(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { + + if (auto uid = GetUidExprOp(expr); uid == AST_UID_EXPR_OP::STORE) { + static const char* mem_store_template = +#ifdef ILATOR_PRECISE_MEM + "tmp_memory[{address}] = {data};\n"; +#else + "tmp_memory[{address}.to_int()] = {data}.to_int();\n"; +#endif + fmt::format_to(buff, mem_store_template, + fmt::arg("address", LookUp(expr->arg(1), lut)), + fmt::arg("data", LookUp(expr->arg(2), lut))); + } else { // ite + static const char* mem_ite_template = "{ite_update_func}(tmp_memory);\n"; + auto mem_update_func = RegisterMemoryUpdate(expr); + fmt::format_to(buff, mem_ite_template, + fmt::arg("ite_update_func", mem_update_func->name)); + } +} + +void Ilator::DfsOpAppFunc(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { + ILA_CHECK(!expr->is_mem()) << "Func returning memory not supported yet"; + + auto local_var = GetLocalVar(lut); + auto [it, status] = lut.insert({expr, local_var}); + ILA_ASSERT(status); + + // apply uninterpreted function + auto app_func = std::dynamic_pointer_cast(expr); + auto func = app_func->func(); + auto func_cxx = RegisterExternalFunc(func); + + std::vector arguments; + for (size_t i = 0; i < func->arg_num(); i++) { + arguments.push_back(LookUp(app_func->arg(i), lut)); + } + + static const char* app_func_template = + "auto {return_var} = {func_name}({argument_list});\n"; + fmt::format_to(buff, app_func_template, // + fmt::arg("return_var", local_var), + fmt::arg("func_name", func_cxx->name), + fmt::arg("argument_list", fmt::join(arguments, ", "))); +} + +void Ilator::DfsOpSpecial(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { + auto local_var = GetLocalVar(lut); + auto [it, status] = lut.insert({expr, local_var}); + ILA_ASSERT(status); + + switch (auto uid = GetUidExprOp(expr); uid) { + case AST_UID_EXPR_OP::LOAD: { + static const char* load_template = + "auto {local_var} = {memory_source}[{address}{mem_suffix}];\n"; + fmt::format_to(buff, load_template, // + fmt::arg("local_var", local_var), + fmt::arg("memory_source", LookUp(expr->arg(0), lut)), + fmt::arg("address", LookUp(expr->arg(1), lut)), +#ifdef ILATOR_PRECISE_MEM + fmt::arg("mem_suffix", "") +#else + fmt::arg("mem_suffix", ".to_int()") +#endif + ); + break; + } + case AST_UID_EXPR_OP::CONCAT: { + // concate using "," in SystemC needs to be global + auto global_var = GetCxxName(expr); + auto [itg, stg] = lut.insert_or_assign(expr, global_var); + ILA_ASSERT(!stg); + global_vars_.insert(expr); + + static const char* concat_template = + "{global_var} = ({type_0}({arg_0}), {type_1}({arg_1}));\n"; + auto arg0 = expr->arg(0); + auto arg1 = expr->arg(1); + fmt::format_to(buff, concat_template, // + fmt::arg("global_var", global_var), + fmt::arg("type_0", GetCxxType(arg0)), + fmt::arg("arg_0", LookUp(arg0, lut)), + fmt::arg("type_1", GetCxxType(arg1)), + fmt::arg("arg_1", LookUp(arg1, lut))); + break; + } + case AST_UID_EXPR_OP::EXTRACT: { + static const char* extract_template = + "auto {extract} = {origin}.range({loc_high}, {loc_low});\n"; + fmt::format_to(buff, extract_template, // + fmt::arg("extract", local_var), + fmt::arg("origin", LookUp(expr->arg(0), lut)), + fmt::arg("loc_high", expr->param(0)), + fmt::arg("loc_low", expr->param(1))); + break; + } + case AST_UID_EXPR_OP::ZEXT: + [[fallthrough]]; + case AST_UID_EXPR_OP::SEXT: { + static const char* extend_template = + "auto {extend} = ({origin}[{sign}] == 1) ? (~{origin}) : {origin};\n" + "{extend} = ({origin}[{sign}] == 1) ? (~{extend}) : {extend};\n"; + auto origin_expr = expr->arg(0); + fmt::format_to(buff, extend_template, // + fmt::arg("extend", local_var), + fmt::arg("origin", LookUp(origin_expr, lut)), + fmt::arg("sign", origin_expr->sort()->bit_width() - 1)); + break; + } + case AST_UID_EXPR_OP::IMPLY: { + static const char* imply_template = + "auto {local_var} = (!{if_var}) & {then_var};\n"; + fmt::format_to(buff, imply_template, // + fmt::arg("local_var", local_var), + fmt::arg("if_var", LookUp(expr->arg(0), lut)), + fmt::arg("then_var", LookUp(expr->arg(1), lut))); + break; + } + case AST_UID_EXPR_OP::ITE: { + static const char* ite_template = + "auto {local_var} = ({condition}) ? {true_branch} : {false_branch};\n"; + fmt::format_to(buff, ite_template, // + fmt::arg("local_var", local_var), + fmt::arg("condition", LookUp(expr->arg(0), lut)), + fmt::arg("true_branch", LookUp(expr->arg(1), lut)), + fmt::arg("false_branch", LookUp(expr->arg(2), lut))); + break; + } + default: + ILA_CHECK(false) << expr; + break; + }; +} + +static const std::unordered_map k_op_symbols = { + // unary + {AST_UID_EXPR_OP::NEG, "-"}, + {AST_UID_EXPR_OP::NOT, "!"}, + {AST_UID_EXPR_OP::COMPL, "~"}, + // binary compare + {AST_UID_EXPR_OP::EQ, "=="}, + {AST_UID_EXPR_OP::LT, "<"}, + {AST_UID_EXPR_OP::GT, ">"}, + {AST_UID_EXPR_OP::ULT, "<"}, + {AST_UID_EXPR_OP::UGT, ">"}, + // binary arith + {AST_UID_EXPR_OP::AND, "&"}, + {AST_UID_EXPR_OP::OR, "|"}, + {AST_UID_EXPR_OP::XOR, "^"}, + {AST_UID_EXPR_OP::SHL, "<<"}, + {AST_UID_EXPR_OP::LSHR, ">>"}, + {AST_UID_EXPR_OP::ASHR, ">>"}, + {AST_UID_EXPR_OP::ADD, "+"}, + {AST_UID_EXPR_OP::SUB, "-"}, + {AST_UID_EXPR_OP::MUL, "*"}, + {AST_UID_EXPR_OP::DIV, "/"}, + {AST_UID_EXPR_OP::UREM, "%"}}; + +void Ilator::DfsOpRegular(const ExprPtr& expr, StrBuff& buff, + ExprVarMap& lut) const { + auto local_var = GetLocalVar(lut); + auto [it, status] = lut.insert({expr, local_var}); + ILA_ASSERT(status); + + // get the corresponding operator symbol + auto uid = GetUidExprOp(expr); + auto pos = k_op_symbols.find(uid); + ILA_ASSERT(pos != k_op_symbols.end()) << uid; + + static const char* unary_op_template = + "{var_type} {local_var} = {unary_op}{arg_0};\n"; + static const char* binary_op_template = + "{var_type} {local_var} = ({arg_0} {binary_op} {arg_1});\n"; + + if (expr->arg_num() == 1) { + fmt::format_to(buff, unary_op_template, // + fmt::arg("var_type", GetCxxType(expr)), + fmt::arg("local_var", local_var), + fmt::arg("unary_op", pos->second), + fmt::arg("arg_0", LookUp(expr->arg(0), lut))); + } else if (expr->arg_num() == 2) { + fmt::format_to(buff, binary_op_template, // + fmt::arg("var_type", GetCxxType(expr)), + fmt::arg("local_var", local_var), + fmt::arg("arg_0", LookUp(expr->arg(0), lut)), + fmt::arg("binary_op", pos->second), + fmt::arg("arg_1", LookUp(expr->arg(1), lut))); + } + ILA_ASSERT(expr->arg_num() <= 2); +} + +} // namespace ilang diff --git a/src/util/fs.cc b/src/util/fs.cc index 0141c23b3..92db446b1 100644 --- a/src/util/fs.cc +++ b/src/util/fs.cc @@ -48,6 +48,10 @@ namespace fs = std::filesystem; namespace fs = std::experimental::filesystem; #endif // FS_INCLUDE +bool os_portable_exist(const std::string& path) { + return fs::exists(path); +} + /// Create a dir, true -> suceeded , ow false bool os_portable_mkdir(const std::string& dir) { if (fs::is_directory(dir)) { diff --git a/src/verification/CMakeLists.txt b/src/verification/CMakeLists.txt deleted file mode 100644 index d4ea52733..000000000 --- a/src/verification/CMakeLists.txt +++ /dev/null @@ -1,12 +0,0 @@ -# ---------------------------------------------------------------------------- # -# source -# ---------------------------------------------------------------------------- # -target_sources(${ILANG_LIB_NAME} PRIVATE - ${CMAKE_CURRENT_SOURCE_DIR}/abs_knob.cc - ${CMAKE_CURRENT_SOURCE_DIR}/eq_check_crr.cc - ${CMAKE_CURRENT_SOURCE_DIR}/legacy_bmc.cc - ${CMAKE_CURRENT_SOURCE_DIR}/rewrite_expr.cc - ${CMAKE_CURRENT_SOURCE_DIR}/rewrite_ila.cc - ${CMAKE_CURRENT_SOURCE_DIR}/unroller.cc -) - diff --git a/src/verification/abs_knob.cc b/src/verification/abs_knob.cc deleted file mode 100644 index a4ca243bc..000000000 --- a/src/verification/abs_knob.cc +++ /dev/null @@ -1,408 +0,0 @@ -/// \file -/// Source for a collection of ILA helpers. - -#include - -#include - -#include -#include -#include - -namespace ilang { - -class FuncObjInsertExprVar { -public: - FuncObjInsertExprVar(ExprSet& vars) : vars_(vars) {} - - void operator()(const ExprPtr e) const { - if (e->is_var()) { - vars_.insert(e); - } - } - -private: - ExprSet& vars_; - -}; // class FuncObjInsertExprVar - -class FuncObjInsertILAInp { -public: - FuncObjInsertILAInp(ExprSet& vars) : vars_(vars) {} - - void operator()(const InstrLvlAbsCnstPtr m) const { - AbsKnob::InsertInp(m, vars_); - } - -private: - ExprSet& vars_; -}; // class FuncObjInsertILAStt - -class FuncObjInsertILAStt { -public: - FuncObjInsertILAStt(ExprSet& vars) : vars_(vars) {} - - void operator()(const InstrLvlAbsCnstPtr m) const { - AbsKnob::InsertStt(m, vars_); - } - -private: - ExprSet& vars_; -}; // class FuncObjInsertILAStt - -class FuncObjInsertILAInstr { -public: - FuncObjInsertILAInstr(InstrVec& instrs) : instrs_(instrs) {} - - void operator()(const InstrLvlAbsCnstPtr m) const { - AbsKnob::InsertInstr(m, instrs_); - } - -private: - InstrVec& instrs_; - -}; // class FuncOjbInsertILAInstr - -/******************************************************************************/ -ExprSet AbsKnob::GetVar(const ExprPtr e) { - auto vars = ExprSet(); - auto func = FuncObjInsertExprVar(vars); - e->DepthFirstVisit(func); - return vars; -} - -/******************************************************************************/ -void AbsKnob::InsertStt(const InstrCnstPtr instr, ExprSet& vars) { - auto host = instr->host(); - ILA_NOT_NULL(host); - InsertStt(host, vars); -} - -void AbsKnob::InsertSttTree(const InstrCnstPtr instr, ExprSet& vars) { - auto host = instr->host(); - ILA_NOT_NULL(host); - InsertSttTree(host, vars); -} - -/******************************************************************************/ -void AbsKnob::InsertVar(const InstrLvlAbsCnstPtr m, ExprSet& vars) { - InsertStt(m, vars); - InsertInp(m, vars); -} - -void AbsKnob::InsertStt(const InstrLvlAbsCnstPtr m, ExprSet& stts) { - for (decltype(m->state_num()) i = 0; i != m->state_num(); i++) { - stts.insert(m->state(i)); - } -} - -void AbsKnob::InsertInp(const InstrLvlAbsCnstPtr m, ExprSet& inps) { - for (decltype(m->input_num()) i = 0; i != m->input_num(); i++) { - inps.insert(m->input(i)); - } -} - -void AbsKnob::InsertVarTree(const InstrLvlAbsCnstPtr top, ExprSet& vars) { - InsertSttTree(top, vars); - InsertInpTree(top, vars); -} - -void AbsKnob::InsertSttTree(const InstrLvlAbsCnstPtr top, ExprSet& stts) { - auto f = FuncObjInsertILAStt(stts); - top->DepthFirstVisit(f); -} - -void AbsKnob::InsertInpTree(const InstrLvlAbsCnstPtr top, ExprSet& inps) { - auto f = FuncObjInsertILAInp(inps); - top->DepthFirstVisit(f); -} - -ExprSet AbsKnob::GetVar(const InstrLvlAbsCnstPtr m) { - auto vars = ExprSet(); - InsertVar(m, vars); - return vars; -} - -ExprSet AbsKnob::GetStt(const InstrLvlAbsCnstPtr m) { - auto stts = ExprSet(); - InsertStt(m, stts); - return stts; -} - -ExprSet AbsKnob::GetInp(const InstrLvlAbsCnstPtr m) { - auto inps = ExprSet(); - InsertInp(m, inps); - return inps; -} - -ExprSet AbsKnob::GetVarTree(const InstrLvlAbsCnstPtr top) { - auto vars = ExprSet(); - InsertVarTree(top, vars); - return vars; -} - -ExprSet AbsKnob::GetSttTree(const InstrLvlAbsCnstPtr top) { - auto stts = ExprSet(); - InsertSttTree(top, stts); - return stts; -} - -ExprSet AbsKnob::GetInpTree(const InstrLvlAbsCnstPtr top) { - auto inps = ExprSet(); - InsertInp(top, inps); - return inps; -} - -void AbsKnob::InsertInstr(const InstrLvlAbsCnstPtr m, InstrVec& instrs) { - for (decltype(m->instr_num()) i = 0; i != m->instr_num(); i++) { - instrs.insert(instrs.end(), m->instr(i)); - } -} - -void AbsKnob::InsertInstrTree(const InstrLvlAbsCnstPtr top, InstrVec& instrs) { - auto f = FuncObjInsertILAInstr(instrs); - top->DepthFirstVisit(f); -} - -InstrVec AbsKnob::GetInstrTree(const InstrLvlAbsCnstPtr m) { - auto instrs = InstrVec(); - InsertInstrTree(m, instrs); - return instrs; -} - -/******************************************************************************/ -ExprPtr AbsKnob::Rewrite(const ExprPtr e, const ExprMap& rule) { - ILA_ASSERT(e) << "Rewriting NULL pointer"; - auto func = FuncObjRewrExpr(rule); - // rewrite all sub-trees - e->DepthFirstVisitPrePost(func); - // return rewrited/copied node - auto rewr = func.get(e); - ILA_ASSERT(rewr) << "Fail rewriting " << e; - return rewr; -} - -void AbsKnob::RewriteInstr(const InstrCnstPtr src, const InstrPtr dst, - const ExprMap& expr_map) { - // decode - auto d_src = src->decode(); - auto d_dst = AbsKnob::Rewrite(d_src, expr_map); - dst->set_decode(d_dst); - - // update - auto updated_states = src->updated_states(); - for (auto& state_name : updated_states) { - auto update_src = src->update(state_name); - if (update_src) { - auto update_dst = AbsKnob::Rewrite(update_src, expr_map); - dst->set_update(state_name, update_dst); - } - } -} - -// this function will change the input ! You can copy it first. -void AbsKnob::FlattenIla(const InstrLvlAbsPtr ila_ptr_) { - ILA_NOT_NULL(ila_ptr_); - - // let's first record all the child's input/states - auto expr_map = ExprMap(); - CnstIlaMap ila_map_; - - std::function recordInpStates = - [&](const InstrLvlAbsCnstPtr& a) { - ILA_INFO << "Traverse:" << (a->name().str()); - if (a == ila_ptr_) - return; // will not change the top - DuplInp(a, ila_ptr_, expr_map); - DuplStt(a, ila_ptr_, expr_map); - DuplInit(a, ila_ptr_, expr_map); - - ila_map_.insert({a, ila_ptr_}); - // remember to change the decode !!! to factor in the valid state - }; - - ila_ptr_->DepthFirstVisit(recordInpStates); - - FuncObjFlatIla flattener(ila_ptr_, ila_map_, expr_map); - ila_ptr_->DepthFirstVisitPrePost(flattener); -} - -InstrLvlAbsPtr AbsKnob::ExtrDeptModl(const InstrPtr instr, - const std::string& name) { - ILA_NOT_NULL(instr); - ILA_NOT_NULL(instr->host()); - - auto src = instr->host(); - auto dst = InstrLvlAbs::New(name); - - auto expr_map = ExprMap(); - - try { // Create new state/input variables in the new ILA. - DuplInp(src, dst, expr_map); - DuplStt(src, dst, expr_map); - DuplFetch(src, dst, expr_map); - DuplValid(src, dst, expr_map); - DuplInit(src, dst, expr_map); - DuplInstrSeq(src, dst); - } catch (...) { - ILA_ERROR << "Error in duplicating attr. from " << src << " to " << dst; - return src; - } - - auto ila_map = CnstIlaMap({{src, dst}}); - // target instruction, child-ILAs - auto prog_src = instr->program(); - if (prog_src) { // duplicate child-ILA - auto prog_dst = dst->NewChild(prog_src->name().str()); - ila_map.insert({prog_src, prog_dst}); - - auto func = FuncObjRewrIla(ila_map, expr_map); - try { - prog_src->DepthFirstVisitPrePost(func); - } catch (...) { - ILA_ERROR << "Error in duplicating child-program " << prog_src; - } - } - - // duplicate instruction - DuplInstr(instr, dst, expr_map, ila_map); - - return dst; -} - -InstrLvlAbsPtr AbsKnob::CopyIlaTree(const InstrLvlAbsCnstPtr src, - const std::string& dst_name) { - ILA_NOT_NULL(src); - ILA_WARN_IF(src->parent()) << "Copying non-root ILA " << src; - - auto dst = InstrLvlAbs::New(dst_name); - dst->set_spec(src->is_spec()); - - auto ila_map = CnstIlaMap({{src, dst}}); - auto expr_map = ExprMap(); - - auto func = FuncObjRewrIla(ila_map, expr_map); - src->DepthFirstVisitPrePost(func); - - return dst; -} - -/******************************************************************************/ -void AbsKnob::DuplInp(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst, - ExprMap& expr_map) { - auto inps = AbsKnob::GetInp(src); - for (auto it = inps.begin(); it != inps.end(); it++) { - // declare new input if not exist (not parent states) - auto inp_src = *it; - auto inp_dst = dst->find_input(inp_src->name()); - if (!inp_dst) { // not exist --> child-input --> create - inp_dst = DuplInp(dst, inp_src); - } - // update rewrite rule - if (expr_map.find(inp_src) == expr_map.end()) { - expr_map.insert({inp_src, inp_dst}); - } - } -} - -void AbsKnob::DuplStt(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst, - ExprMap& expr_map) { - auto stts = AbsKnob::GetStt(src); - for (auto it = stts.begin(); it != stts.end(); it++) { - auto stt_src = *it; - auto stt_dst = dst->find_state(stt_src->name()); - if (!stt_dst) { // not exist --> child-state --> create - stt_dst = DuplStt(dst, stt_src); - } - // update rewrite rule - if (expr_map.find(stt_src) == expr_map.end()) { - expr_map.insert({stt_src, stt_dst}); - } - } -} - -ExprPtr AbsKnob::DuplFetch(const InstrLvlAbsCnstPtr src, - const InstrLvlAbsPtr dst, const ExprMap& expr_map) { - auto f_src = src->fetch(); - if (!f_src) { - ILA_WARN << "Fetch not set for " << src; - return NULL; - } - auto f_dst = AbsKnob::Rewrite(f_src, expr_map); - dst->SetFetch(f_dst); - return f_dst; -} - -ExprPtr AbsKnob::DuplValid(const InstrLvlAbsCnstPtr src, - const InstrLvlAbsPtr dst, const ExprMap& expr_map) { - auto v_src = src->valid(); - if (!v_src) { - ILA_WARN << "Valid not set for " << src; - return NULL; - } - auto v_dst = AbsKnob::Rewrite(v_src, expr_map); - dst->SetValid(v_dst); - return v_dst; -} - -void AbsKnob::DuplInit(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst, - const ExprMap& expr_map) { - for (decltype(src->init_num()) i = 0; i != src->init_num(); i++) { - auto i_src = src->init(i); - auto i_dst = AbsKnob::Rewrite(i_src, expr_map); - dst->AddInit(i_dst); - } -} - -InstrPtr AbsKnob::DuplInstr(const InstrCnstPtr i_src, const InstrLvlAbsPtr dst, - const ExprMap& expr_map, - const CnstIlaMap& ila_map) { - // create - auto i_dst = dst->NewInstr(i_src->name().str()); - // rewrite - RewriteInstr(i_src, i_dst, expr_map); - // connect child-program - auto p_src = i_src->program(); - if (p_src) { - auto pos = ila_map.find(p_src); - ILA_ASSERT(pos != ila_map.end()) - << "Child-program " << p_src << " not mapped."; - auto p_dst = pos->second; - i_dst->set_program(p_dst); - } - return i_dst; -} - -void AbsKnob::DuplInstrSeq(const InstrLvlAbsCnstPtr src, - const InstrLvlAbsPtr dst) { - // ILA_WARN << "DuplInstrSeq not implemented yet."; - // TODO -} - -ExprPtr AbsKnob::DuplInp(const InstrLvlAbsPtr m, const ExprPtr inp) { - ILA_ASSERT(inp->is_var()) << "Creating input from non-var Expr."; - if (inp->is_bool()) { - return m->NewBoolInput(inp->name().str()); - } else if (inp->is_bv()) { - return m->NewBvInput(inp->name().str(), inp->sort()->bit_width()); - } else { - ILA_ASSERT(inp->is_mem()) << "Unknown sort of " << inp; - return m->NewMemInput(inp->name().str(), inp->sort()->addr_width(), - inp->sort()->data_width()); - } -} - -ExprPtr AbsKnob::DuplStt(const InstrLvlAbsPtr m, const ExprPtr stt) { - ILA_ASSERT(stt->is_var()) << "Creating state from non-var Expr."; - if (stt->is_bool()) { - return m->NewBoolState(stt->name().str()); - } else if (stt->is_bv()) { - return m->NewBvState(stt->name().str(), stt->sort()->bit_width()); - } else { - ILA_ASSERT(stt->is_mem()) << "Unkown sort of " << stt; - return m->NewMemState(stt->name().str(), stt->sort()->addr_width(), - stt->sort()->data_width()); - } -} - -} // namespace ilang diff --git a/src/verification/eq_check_crr.cc b/src/verification/eq_check_crr.cc deleted file mode 100644 index 5b9ae7890..000000000 --- a/src/verification/eq_check_crr.cc +++ /dev/null @@ -1,855 +0,0 @@ -/// \file -/// Source for generating verification condition for equivalecne checking. - -#include - -#include - -#include -#include -#include -#include - -namespace ilang { - -const std::string CommDiag::k_suff_orig_ = "org"; -const std::string CommDiag::k_suff_appl_ = "apl"; - -const std::string CommDiag::k_suff_old_ = "old"; -const std::string CommDiag::k_suff_new_ = "new"; -const std::string CommDiag::k_suff_apl_ = "apl"; - -using namespace ExprFuse; - -CommDiag::CommDiag(z3::context& ctx, const CrrPtr crr) : ctx_(ctx), crr_(crr) { - Init(); -} - -CommDiag::~CommDiag() {} - -bool CommDiag::EqCheck(const int& max) { - // refinement relation sanity check - auto sc_res = SanityCheck(); - ILA_WARN_IF(!sc_res) << "The refinement relation sanity check fail."; - - // determine the number of steps for unrolling (check valid if specified) - auto step_orig_a = DetStepOrig(crr_->refine_a(), max); - auto step_appl_a = DetStepAppl(crr_->refine_a(), max); - - auto step_orig_b = DetStepOrig(crr_->refine_b(), max); - auto step_appl_b = DetStepAppl(crr_->refine_b(), max); - - if (step_orig_a < 0 || step_appl_a < 0 || step_orig_b < 0 || - step_appl_b < 0) { - ILA_ERROR << "Fail determining unroll step."; - return false; - } - - // generate transition relation - auto cstr_tran_a = GenTranRel(crr_->refine_a(), step_orig_a, step_appl_a); - auto cstr_tran_b = GenTranRel(crr_->refine_b(), step_orig_b, step_appl_b); - - auto s = z3::solver(ctx_); - s.add(cstr_tran_a); - if (s.check() == z3::unsat) { - ILA_ERROR << "Dead transition relation."; - ILA_DLOG("Verbose-CrrEqCheck") << s; - return false; - } - s.reset(); - s.add(cstr_tran_b); - if (s.check() == z3::unsat) { - ILA_ERROR << "Dead transition relation."; - ILA_DLOG("Verbose-CrrEqCheck") << s; - return false; - } - s.reset(); - - // generate assumptions (old state equivalent) - auto cstr_assm = GenAssm(); - - // generate property to check (new state equivalent) - auto cstr_prop = GenProp(); - - // check - s.add(cstr_tran_a && cstr_tran_b && cstr_assm); - s.add(!cstr_prop); - auto res = s.check(); - if (res == z3::sat) { - ILA_DLOG("Verbose-CrrEqCheck") << s.get_model(); - } - - return (res == z3::unsat); -} - -bool CommDiag::IncCheck(const int& min, const int& max, const int& step) { - // initialization - for (UID uid : {A_OLD, A_NEW, B_OLD, B_NEW}) { - auto& uu = GetUnrlUnit(uid); - uu.lo = 0; - uu.hi = min; - } - - // apply instruction - const auto& stts_a = stts_a_; // used for marking - const auto& stts_b = stts_b_; - - auto s = z3::solver(ctx_); // solver - { // default basic condition (old/new/apply path & assm & prop) - auto appl_instr_a = GetZ3ApplInstr(stts_a, crr_->refine_a()); - auto appl_instr_b = GetZ3ApplInstr(stts_b, crr_->refine_b()); - s.add(appl_instr_a); - s.add(appl_instr_b); - s.push(); // record backtracking point - } - - auto cf = ctx_.bool_const("cmpl_flag"); // flag indicating flushing completion - // assumption and property to check - auto assm = GetZ3Assm(); - auto prop = GetZ3Prop(); - // check only if complete - assm = Z3Implies(ctx_, cf, assm); - prop = Z3Implies(ctx_, cf, prop); - - // incrementally unroll flushing - for (auto i = min; i <= max; i += step) { // if (num < i) --> already fixed - // check if complete - auto all_path_complete = true; - for (UID uid : {A_OLD, A_NEW, B_OLD, B_NEW}) { - auto& uu = GetUnrlUnit(uid); - all_path_complete = all_path_complete && (uu.hi < i); - } - if (all_path_complete) { - ILA_DLOG("Verbose-CrrEqCheck") << "Complete"; - return true; - } - - // unroll new flushing path - for (UID uid : {A_OLD, A_NEW, B_OLD, B_NEW}) { - auto& uu = GetUnrlUnit(uid); - if (uu.hi == i) { // need to unroll new step - auto tran = GetZ3IncFlsh(uid); - s.add(tran); - } - } - s.push(); // recording the current transition relation - - // accumulate completion indicator - auto cmpl_acc = ctx_.bool_val(true); - for (UID uid : {A_OLD, A_NEW, B_OLD, B_NEW}) { - auto cmpl_i = GetZ3IncCmpl(uid); - cmpl_acc = cmpl_acc && cmpl_i; - } - s.add(cf == cmpl_acc); - - // check prop - s.add(assm); - s.add(!prop); - auto res = s.check(); - ILA_INFO << "Result: " << res; - if (res == z3::sat) { - return false; - } - - // pop back to transition relation (removing marking and prop) - s.pop(); - - // push partial property - auto partial_assm = GetZ3Assm(); - auto partial_cmpl = Z3Implies(ctx_, cmpl_acc, partial_assm); - auto partial_prop = GetZ3Prop(); - s.add(Z3Implies(ctx_, partial_cmpl && partial_assm, partial_prop)); - s.push(); - - // check if num is sufficient (if not fixed yet) and increment accordingly - for (UID uid : {A_OLD, A_NEW, B_OLD, B_NEW}) { - auto& uu = GetUnrlUnit(uid); - uu.lo = uu.hi; - if (uu.hi == i) { // new step - auto cmpl_i = GetZ3IncCmpl(uid); - auto sufficient = CheckCmpl(s, cmpl_i); - uu.hi = sufficient ? uu.hi : uu.hi + step; - } - } - } - - return true; -} - -void CommDiag::Init() { - SanityCheck(); - // unroller initialized with flushing function - for (auto uid : {A_OLD, A_NEW, B_OLD, B_NEW}) { - auto& un = GetUnrl(uid); - auto ref = GetRefine(uid); - un.ClearPred(); - un.AddGlobPred(ref->flush()); - } - // state vars of each ILA - stts_a_ = AbsKnob::GetSttTree(crr_->refine_a()->ila()); - stts_b_ = AbsKnob::GetSttTree(crr_->refine_b()->ila()); -} - -CommDiag::Unroll& CommDiag::GetUnrl(const UID& uid) { - switch (uid) { - case A_OLD: - return unrl_old_; - break; - case A_NEW: - return unrl_new_; - break; - case B_OLD: - return unrl_old_; - break; - case B_NEW: - return unrl_new_; - break; - default: - ILA_ASSERT(false) << "unknon uid " << uid; - return unrl_old_; - break; - } -} - -CommDiag::Unroll& CommDiag::GetUnrlOld() { return unrl_a_old_; } - -CommDiag::Unroll& CommDiag::GetUnrlNew() { return unrl_a_new_; } - -CommDiag::Unroll& CommDiag::GetUnrlApl() { return unrl_apl_; } - -RefPtr CommDiag::GetRefine(const UID& uid) { - switch (uid) { - case A_OLD: - return crr_->refine_a(); - break; - case A_NEW: - return crr_->refine_a(); - break; - case B_OLD: - return crr_->refine_b(); - break; - case B_NEW: - return crr_->refine_b(); - break; - default: - ILA_ASSERT(false) << "unknon uid " << uid; - return NULL; - break; - } -} - -CommDiag::UnrlUnit& CommDiag::GetUnrlUnit(const UID& uid) { - switch (uid) { - case A_OLD: - return uu_a_old_; - break; - case A_NEW: - return uu_a_new_; - break; - case B_OLD: - return uu_b_old_; - break; - case B_NEW: - return uu_b_new_; - break; - default: - ILA_ASSERT(false) << "unknon uid " << uid; - return uu_a_old_; - break; - } -} - -const ExprSet& CommDiag::GetStts(const UID& uid) { - switch (uid) { - case A_OLD: - return stts_a_; - break; - case A_NEW: - return stts_a_; - break; - case B_OLD: - return stts_b_; - break; - case B_NEW: - return stts_b_; - break; - default: - ILA_ASSERT(false) << "unknon uid " << uid; - return stts_a_; - break; - } -} - -z3::expr CommDiag::GetZ3IncFlsh(const UID& uid) { - auto& un = GetUnrl(uid); - auto& uu = GetUnrlUnit(uid); - auto ref = GetRefine(uid); - auto& stts = GetStts(uid); - // transition relation - auto tran = un.MonoIncr(ref->ila(), uu.hi - uu.lo /*length*/, uu.lo /*base*/); - // mark - for (auto pos = uu.lo; pos <= uu.hi; pos++) { - auto cmpl = un.GetZ3Expr(ref->cmpl(), pos); - auto eq = ctx_.bool_val(true); - for (auto it = stts.begin(); it != stts.end(); it++) { - auto s_i = un.CurrState(*it, pos); - auto s = un.GetZ3Expr(*it); // representative - eq = eq && (s == s_i); - } - auto mark = Z3Implies(ctx_, cmpl, eq); - tran = tran && mark; - } - return tran; -} - -z3::expr CommDiag::GetZ3IncCmpl(const UID& uid) { - auto& un = GetUnrl(uid); - auto& uu = GetUnrlUnit(uid); - auto cmpl = GetRefine(uid)->cmpl(); - // OR all completion predicate - auto cmpl_acc = ctx_.bool_val(false); - for (auto i = 0; i <= uu.hi; i++) { - auto cmpl_i = un.GetZ3Expr(cmpl, i); - cmpl_acc = cmpl_acc || cmpl_i; - } - return cmpl_acc; -} - -bool CommDiag::IncEqCheck(const int& min, const int& max, const int& step) { - // sanity check - auto sc_res = SanityCheck(); // XXX need refresh - ILA_WARN_IF(!sc_res) << "Sanity check fail"; - - const auto ma = crr_->refine_a()->coi(); // representative ILA - const auto mb = crr_->refine_b()->coi(); - const auto stts_a = AbsKnob::GetSttTree(ma); // used for marking - const auto stts_b = AbsKnob::GetSttTree(mb); - - auto s = z3::solver(ctx_); // solver - { // default basic condition (old/new/apply path & assm & prop) - auto appl_instr_a = GetZ3ApplInstr(stts_a, crr_->refine_a()); - auto appl_instr_b = GetZ3ApplInstr(stts_b, crr_->refine_b()); - s.add(appl_instr_a); - s.add(appl_instr_b); - s.push(); // record backtracking point - } - - auto cf = ctx_.bool_const("cmpl_flag"); // flag indicating flushing completion - // assumption and property to check - auto assm = GetZ3Assm(); - auto prop = GetZ3Prop(); - // check only if complete - assm = Z3Implies(ctx_, cf, assm); - prop = Z3Implies(ctx_, cf, prop); - - // Incrementally unrolling and check - ILA_ASSERT(max >= min) << "Invalid range [" << min << ", " << max << "]"; - auto num_old_a = min; - auto num_new_a = min; - auto num_old_b = min; - auto num_new_b = min; - auto inc_unrl_old_a = Unroll(ctx_, k_suff_old_); - auto inc_unrl_new_a = Unroll(ctx_, k_suff_new_); - auto inc_unrl_old_b = Unroll(ctx_, k_suff_old_); - auto inc_unrl_new_b = Unroll(ctx_, k_suff_new_); - inc_unrl_old_a.AddGlobPred(crr_->refine_a()->flush()); - inc_unrl_new_a.AddGlobPred(crr_->refine_a()->flush()); - inc_unrl_old_b.AddGlobPred(crr_->refine_b()->flush()); - inc_unrl_new_b.AddGlobPred(crr_->refine_b()->flush()); - - for (auto i = min; i <= max; i += step) { // if (num < i) --> already fixed - // transition relation - if ((num_old_a < i) && (num_old_b < i) && (num_new_a < i) && - (num_new_b < i)) { - ILA_DLOG("Verbose-CrrEqCheck") << "Complete"; - return true; - } - - // unroll new flushing path - if (num_old_a == i) { // need to unroll new step - auto tran = - GetZ3IncUnrl(inc_unrl_old_a, crr_->refine_a(), i, step, stts_a); - s.add(tran); - } - if (num_new_a == i) { // need to unroll new step - auto tran = - GetZ3IncUnrl(inc_unrl_new_a, crr_->refine_a(), i, step, stts_a); - s.add(tran); - } - if (num_old_b == i) { // need to unroll new step - auto tran = - GetZ3IncUnrl(inc_unrl_old_b, crr_->refine_b(), i, step, stts_b); - s.add(tran); - } - if (num_new_b == i) { // need to unroll new step - auto tran = - GetZ3IncUnrl(inc_unrl_new_b, crr_->refine_b(), i, step, stts_b); - s.add(tran); - } - s.push(); // recording the current transition relation - - // accumulate completion indicator - auto cmpl_a = crr_->refine_a()->cmpl(); - auto cmpl_b = crr_->refine_b()->cmpl(); - // XXX only create if necessary (need cache) - auto cmpl_old_a = GetZ3Cmpl(cmpl_a, inc_unrl_old_a, 0, num_old_a); - auto cmpl_new_a = GetZ3Cmpl(cmpl_a, inc_unrl_new_a, 0, num_new_a); - auto cmpl_old_b = GetZ3Cmpl(cmpl_b, inc_unrl_old_b, 0, num_old_b); - auto cmpl_new_b = GetZ3Cmpl(cmpl_b, inc_unrl_new_b, 0, num_new_b); - s.add(cf == (cmpl_old_a && cmpl_new_a && cmpl_old_b && cmpl_new_b)); - - // check prop - s.add(assm); - s.add(!prop); - ILA_INFO << "Start checking " << num_old_a << " " << num_new_a << " " - << num_old_b << " " << num_new_b; - auto res = s.check(); - ILA_INFO << "Result: " << res; - if (res == z3::sat) { - auto m = s.get_model(); - - ILA_WARN << "Model A"; - for (auto it = stts_a.begin(); it != stts_a.end(); it++) { - auto var_expr = inc_unrl_old_a.GetZ3Expr(*it, num_old_a); - auto var_repr = inc_unrl_old_a.GetZ3Expr(*it); - ILA_WARN << var_expr << ": " << m.eval(var_expr) << "; " << var_repr - << ": " << m.eval(var_repr); - } - for (auto it = stts_a.begin(); it != stts_a.end(); it++) { - auto var_expr = inc_unrl_new_a.GetZ3Expr(*it, num_new_a); - auto var_repr = inc_unrl_new_a.GetZ3Expr(*it); - ILA_WARN << var_expr << ": " << m.eval(var_expr) << "; " << var_repr - << ": " << m.eval(var_repr); - } - - ILA_WARN << "Model B"; - for (auto it = stts_b.begin(); it != stts_b.end(); it++) { - auto var_expr = inc_unrl_old_b.GetZ3Expr(*it, num_old_b); - auto var_repr = inc_unrl_old_b.GetZ3Expr(*it); - ILA_WARN << var_expr << ": " << m.eval(var_expr) << "; " << var_repr - << ": " << m.eval(var_repr); - } - for (auto it = stts_b.begin(); it != stts_b.end(); it++) { - auto var_expr = inc_unrl_new_b.GetZ3Expr(*it, num_new_b); - auto var_repr = inc_unrl_new_b.GetZ3Expr(*it); - ILA_WARN << var_expr << ": " << m.eval(var_expr) << "; " << var_repr - << ": " << m.eval(var_repr); - } - - return false; - } - - // pop back to transition relation (removing marking and prop) - s.pop(); - - // push partial property - auto partial_assm = GetZ3Assm(); - auto partial_cmpl = - Z3Implies(ctx_, cmpl_old_a && cmpl_new_a && cmpl_old_b && cmpl_new_b, - partial_assm); - auto partial_prop = GetZ3Prop(); - s.add(Z3Implies(ctx_, partial_cmpl && partial_assm, partial_prop)); - s.push(); - - // check if num is sufficient (if not fixed yet) and increment accordingly - if (num_old_a == i) { // new step - auto sufficient = CheckCmpl(s, cmpl_old_a); - num_old_a = sufficient ? num_old_a : num_old_a + step; - } - if (num_new_a == i) { // new step - auto sufficient = CheckCmpl(s, cmpl_new_a); - num_new_a = sufficient ? num_new_a : num_new_a + step; - } - if (num_old_b == i) { // new step - auto sufficient = CheckCmpl(s, cmpl_old_b); - num_old_b = sufficient ? num_old_b : num_old_b + step; - } - if (num_new_b == i) { // new step - auto sufficient = CheckCmpl(s, cmpl_new_b); - num_new_b = sufficient ? num_new_b : num_new_b + step; - } - } - - // no bug found up to the given bound - return true; -} - -bool CommDiag::SanityCheck() { - // check refinement - auto res_a = SanityCheckRefinement(crr_->refine_a()); - auto res_b = SanityCheckRefinement(crr_->refine_b()); - - // check relation - auto res_r = SanityCheckRelation(crr_->relation(), crr_->refine_a()->coi(), - crr_->refine_b()->coi()); - - return res_a && res_b && res_r; -} - -bool CommDiag::SanityCheckRefinement(const RefPtr ref) { - ILA_NOT_NULL(ref); - - auto m = ref->coi(); - auto f = ref->flush(); - auto a = ref->appl(); - auto c = ref->cmpl(); - ILA_CHECK(m) << "Refinement target not set."; - ILA_CHECK(f) << "Flushing function not set for " << m; - ILA_CHECK(a) << "Apply function not set set for " << m; - ILA_CHECK(c) << "Complete condition not set for " << m; - - auto s = z3::solver(ctx_); - auto g = Z3ExprAdapter(ctx_); - - // check flushing and apply does not hold at the same time - auto exc = g.GetExpr(And(f, a)); - s.reset(); - s.add(exc); - if (s.check() == z3::sat) { - ILA_DLOG("Verbose-CrrEqCheck") << s.get_model(); - ILA_ERROR << "Non-exclusive flushing function and apply function."; - return false; - } - - // check flushing does not imply complete (if need to unroll) - if ((ref->step_orig() != 0) || (ref->step_appl() != 0)) { - auto cmpl_unique = g.GetExpr(Imply(f, c)); - s.reset(); - s.add(!cmpl_unique); - if (s.check() == z3::unsat) { - ILA_ERROR << "Flushing function implies completion."; - return false; - } - } - - // check flushing and apply does not affect state equivalence - auto init = GenInit(ref); - auto an = unroll_appl_.GetZ3Expr(a, 0); - // check: /\s_n, a_n -> (a_n & f_o & eq_o_n) - s.reset(); - auto appl_z3 = z3::expr_vector(ctx_); - auto appl_vars = AbsKnob::GetVar(a); - for (auto it = appl_vars.begin(); it != appl_vars.end(); it++) { - appl_z3.push_back(unroll_appl_.CurrState(*it, 0)); - } - s.add(z3::forall(appl_z3, an && !init)); - // s.add(an && !(fo && an && eq)); - if (s.check() == z3::sat) { - ILA_ERROR << "Flushing and apply function intervene state equivalence."; - ILA_DLOG("Verbose-CrrEqCheck") << s.get_model(); - return false; - } - - return true; -} - -bool CommDiag::SanityCheckRelation(const RelPtr rel, const InstrLvlAbsPtr ma, - const InstrLvlAbsPtr mb) const { - ILA_ERROR_IF(ma->name() == mb->name()) - << "Only EQ-Check ILAs with different names."; - - ILA_NOT_NULL(rel); - auto rel_expr = rel->get(); - auto rel_vars = AbsKnob::GetVar(rel_expr); - - auto ref_vars = ExprSet(); - AbsKnob::InsertStt(ma, ref_vars); - AbsKnob::InsertStt(mb, ref_vars); - - // check: rel_vars <= ref_vars - for (auto it = rel_vars.begin(); it != rel_vars.end(); it++) { - auto pos = ref_vars.find(*it); - if (pos == ref_vars.end()) { // rel has var not in ref - ILA_ERROR << "Relation depends on " << *it << " -- not in refinement."; - return false; - } - } - return true; -} - -int CommDiag::DetStepOrig(const RefPtr ref, const int& max) { - auto k = ref->step_orig(); - ILA_WARN_IF((max > 0) && (k > max)) << "Max bound < #step"; - - for (auto n = (k >= 0) ? k : 0; n <= max; n++) { - auto res = CheckStepOrig(ref, n); - if (res) { - ILA_INFO << "#orig flush (" << ref->coi() << "): " << n; - return n; - } - } - - ILA_ERROR << "#step not determined, increase max bound"; - return -1; -} - -int CommDiag::DetStepAppl(const RefPtr ref, const int& max) { - auto k = ref->step_appl(); - ILA_WARN_IF((max > 0) && (k > max)) << "Max bound < #step"; - - for (auto n = (k >= 0) ? k : 0; n <= max; n++) { - auto res = CheckStepAppl(ref, n); - if (res) { - ILA_INFO << "#appl flush (" << ref->coi() << "): " << n; - return n; - } - } - - ILA_ERROR << "#step not determined, increase max bound"; - return -1; -} - -bool CommDiag::CheckStepOrig(const RefPtr ref, const int& k) { - // ensure initial state to follow the flush && apply paradiam - auto init = GenInit(ref); - // unroll the transition relation - auto& u = unroll_orig_; - u.ClearPred(); - u.AddGlobPred(ref->flush()); - for (decltype(ref->inv_num()) i = 0; i != ref->inv_num(); i++) { - u.AddGlobPred(ref->inv(i)); - } - auto tran = u.MonoAssn(ref->coi(), k, 0); - // start checking - auto s = z3::solver(ctx_); - // sanity check on transition - s.add(init && tran); - if (s.check() == z3::unsat) { - ILA_ERROR << "Dead transition: " << ref->coi() << " #step: " << k; - ILA_DLOG("Verbose-CrrEqCheck") << s; - ILA_CHECK(false); - } - - // at least once - auto at_least_once = AtLeastOnce(u, ref->cmpl(), 0, k); - s.reset(); - s.add(init && tran && !at_least_once); - if (s.check() == z3::sat) { - return false; - } - // at most once - auto at_most_once = AtMostOnce(u, ref->cmpl(), 0, k); - s.add(init && tran && !at_most_once); - if (s.check() == z3::sat) { - return false; - } - // valid #unroll step - return true; -} - -bool CommDiag::CheckStepAppl(const RefPtr ref, const int& k) { - // ensure initial state to follow the flush && apply paradiam - auto init = GenInit(ref); - // unroll the transition relation - auto& u = unroll_appl_; - u.ClearPred(); - u.AddInitPred(ref->appl()); - for (auto i = 1; i <= k + 1; i++) { - u.AddStepPred(ref->flush(), i); - } - for (decltype(ref->inv_num()) i = 0; i != ref->inv_num(); i++) { - u.AddGlobPred(ref->inv(i)); - } - auto tran = u.MonoAssn(ref->coi(), k + 1, 0); - // start checking - auto s = z3::solver(ctx_); - // at least once - auto at_least_once = AtLeastOnce(u, ref->cmpl(), 1, k + 1); - s.reset(); - s.add(init && tran && !at_least_once); - if (s.check() == z3::sat) { - return false; - } - // at most once - auto at_most_once = AtMostOnce(u, ref->cmpl(), 1, k + 1); - s.add(init && tran && !at_most_once); - if (s.check() == z3::sat) { - return false; - } - // valid #unroll step - return true; -} - -z3::expr CommDiag::GetZ3ApplInstr(const ExprSet& stts, const RefPtr ref) { - auto acc = ctx_.bool_val(true); - { // take one step (apply) - auto& un = unrl_apl_; - un.ClearPred(); - // invariant - for (decltype(ref->inv_num()) i = 0; i != ref->inv_num(); i++) { - un.AddGlobPred(ref->inv(i)); - } - // apply - un.AddStepPred(ref->appl(), 0); - auto apply_one_step = un.MonoAssn(ref->coi(), 1 /*length*/, 0 /*base*/); - un.ClearPred(); - acc = acc && apply_one_step; - } - { // connect old/new with the apply step - auto eq = ctx_.bool_val(true); - for (auto it = stts.begin(); it != stts.end(); it++) { - // apply_0 == old_0) - auto sa_0 = unrl_apl_.CurrState(*it, 0); - auto so_0 = unrl_old_.CurrState(*it, 0); - eq = eq && (sa_0 == so_0); - // apply_1 == new_0) - auto sa_1 = unrl_apl_.CurrState(*it, 1); - auto sn_0 = unrl_new_.CurrState(*it, 0); - eq = eq && (sa_1 == sn_0); - } - acc = acc && eq; - } - // flush(old_0) - auto flush_on_old = unrl_old_.GetZ3Expr(ref->flush(), 0); - // flush(new_0) - auto flush_on_new = unrl_new_.GetZ3Expr(ref->flush(), 0); - // return - return acc && flush_on_old && flush_on_new; -} - -z3::expr CommDiag::GenInit(const RefPtr ref) { - // default equivalence: state variables (not including inputs) - auto vars = AbsKnob::GetSttTree(ref->coi()); - auto eq = ctx_.bool_val(true); - for (auto it = vars.begin(); it != vars.end(); it++) { - auto so = unroll_orig_.CurrState(*it, 0); - auto sn = unroll_appl_.CurrState(*it, 0); - eq = eq && (so == sn); - } - auto an = unroll_appl_.GetZ3Expr(ref->appl(), 0); - auto fo = unroll_orig_.GetZ3Expr(ref->flush(), 0); - return (an && fo && eq); -} - -z3::expr CommDiag::GenTranRel(const RefPtr ref, const int& k_orig, - const int& k_appl) { - auto init = GenInit(ref); - auto orig = UnrollFlush(unroll_orig_, ref, 0, k_orig, 0); - auto appl = UnrollFlush(unroll_appl_, ref, 0, k_appl + 1, 1); - return (init && orig && appl); -} - -z3::expr CommDiag::GetZ3Assm() { - auto& un = GetUnrlOld(); - auto eq = un.GetZ3Expr(crr_->relation()->get()); - return eq; -} - -z3::expr CommDiag::GetZ3Prop() { - auto& un = GetUnrlNew(); - auto eq = un.GetZ3Expr(crr_->relation()->get()); - return eq; -} - -z3::expr CommDiag::GetZ3Cmpl(const ExprPtr cmpl, MonoUnroll& un, - const int& begin, const int& end) const { - auto cmpl_acc = ctx_.bool_val(false); - for (auto i = begin; i <= end; i++) { - auto cmpl_i = un.GetZ3Expr(cmpl, i); - cmpl_acc = cmpl_acc || cmpl_i; - } - return cmpl_acc; -} - -z3::expr CommDiag::GetZ3IncUnrl(MonoUnroll& un, const RefPtr ref, - const int& begin, const int& length, - const ExprSet& stts) const { - auto tran = un.MonoIncr(ref->coi(), length /*length*/, begin /*base*/); - // mark - for (auto pos = begin; pos <= begin + length; pos++) { - auto cmpl = un.GetZ3Expr(ref->cmpl(), pos); - auto eq = ctx_.bool_val(true); - for (auto it = stts.begin(); it != stts.end(); it++) { - auto s_i = un.CurrState(*it, pos); - auto s = un.GetZ3Expr(*it); // representative - eq = eq && (s == s_i); - } - auto mark = Z3Implies(ctx_, cmpl, eq); - tran = tran && mark; - } - return tran; -} - -bool CommDiag::CheckCmpl(z3::solver& s, z3::expr& cmpl_expr) const { - s.push(); - s.add(!cmpl_expr); - auto must_cmpl = (s.check() == z3::unsat); - s.pop(); - - if (must_cmpl) { - s.add(cmpl_expr); // added - s.push(); // added - return true; - } else { - return false; - } -} - -z3::expr CommDiag::GenAssm() { - auto eq = unroll_orig_.GetZ3Expr(crr_->relation()->get()); - return eq; -} - -z3::expr CommDiag::GenProp() { - auto eq = unroll_appl_.GetZ3Expr(crr_->relation()->get()); - return eq; -} - -z3::expr CommDiag::AtLeastOnce(MonoUnroll& unroller, const ExprPtr cmpl, - const int& start, const int& end) const { - auto cstr = unroller.GetZ3Expr(BoolConst(false), 0); - for (auto i = start; i <= end; i++) { - cstr = cstr || unroller.GetZ3Expr(cmpl, i); - } - return cstr; -} - -z3::expr CommDiag::AtMostOnce(MonoUnroll& unroller, const ExprPtr cmpl, - const int& start, const int& end) const { - auto cstr = unroller.GetZ3Expr(BoolConst(true), 0); - for (auto i = start; i <= end; i++) { - auto cmpl_i = unroller.GetZ3Expr(cmpl, i); - for (auto j = i + 1; j <= end; j++) { - auto cmpl_j = unroller.GetZ3Expr(cmpl, j); - cstr = cstr && (!cmpl_i || !cmpl_j); - } - } - return cstr; -} - -z3::expr CommDiag::UnrollFlush(MonoUnroll& unroller, const RefPtr ref, - const int& base, const int& length, - const int& start) { - ILA_ASSERT(base + length >= start); - unroller.ClearPred(); - // add invariant - for (decltype(ref->inv_num()) i = 0; i != ref->inv_num(); i++) { - unroller.AddGlobPred(ref->inv(i)); - } - // add flush - for (auto i = start; i <= base + length; i++) { - unroller.AddStepPred(ref->flush(), i); - } - // unroll - auto path = unroller.MonoAssn(ref->coi(), length, base); - - auto vars = AbsKnob::GetStt(ref->coi()); - auto mark = ctx_.bool_val(true); - // mark complete step with representing state - for (auto i = start; i <= base + length; i++) { - auto cmpl_i = unroller.GetZ3Expr(ref->cmpl(), i); - auto eq = ctx_.bool_val(true); - for (auto it = vars.begin(); it != vars.end(); it++) { - auto s_i = unroller.CurrState(*it, i); - auto s = unroller.GetZ3Expr(*it); - eq = eq && (s == s_i); - } - mark = mark && Z3Implies(ctx_, cmpl_i, eq); - } - - // XXX complete proved to be one and exactly one - - return path && mark; -} - -} // namespace ilang diff --git a/src/verification/legacy_bmc.cc b/src/verification/legacy_bmc.cc deleted file mode 100644 index d7eab2278..000000000 --- a/src/verification/legacy_bmc.cc +++ /dev/null @@ -1,179 +0,0 @@ -/// \file -/// Source for bounded model checking - -#include - -#include -#include - -namespace ilang { - -LegacyBmc::LegacyBmc() {} - -LegacyBmc::~LegacyBmc() {} - -void LegacyBmc::AddInit(ExprPtr init) { inits_.push_back(init); } - -void LegacyBmc::AddInvariant(ExprPtr inv) { invs_.push_back(inv); } - -z3::check_result LegacyBmc::Check(InstrLvlAbsPtr m0, const int& k0, - InstrLvlAbsPtr m1, const int& k1) { - ILA_NOT_NULL(m0); - ILA_NOT_NULL(m1); - - auto gen = Z3ExprAdapter(ctx_); - z3::solver solver(ctx_); - - // unroll m0 - auto cnst_m0 = UnrollCmplIla(m0, k0); - solver.add(cnst_m0); - - // untoll m1 - auto cnst_m1 = UnrollCmplIla(m1, k1); - solver.add(cnst_m1); - - auto state_num_m0 = m0->state_num(); - auto suffix_init = std::to_string(0); - auto suffix_k0 = std::to_string(k0); - auto suffix_k1 = std::to_string(k1); - for (size_t i = 0; i != state_num_m0; i++) { - auto state_m0 = m0->state(i); - auto state_m1 = m1->find_state(state_m0->name()); - ILA_ASSERT(state_m1 != NULL) << "State unmatched: " << state_m0; - - // equal initial condition - auto state_m0_init = gen.GetExpr(state_m0, suffix_init); - auto state_m1_init = gen.GetExpr(state_m1, suffix_init); - auto init_cnst_i = (state_m0_init == state_m1_init); - solver.add(init_cnst_i); - - // assert equal final state - auto state_m0_final = gen.GetExpr(state_m0, suffix_k0); - auto state_m1_final = gen.GetExpr(state_m1, suffix_k1); - auto assert_i = (state_m0_final == state_m1_final); - solver.add(!assert_i); - } - - // equal input - auto input_num_m0 = m0->input_num(); - for (size_t i = 0; i != input_num_m0; i++) { - auto input_m0 = m0->input(i); - auto input_m1 = m1->find_input(input_m0->name()); - ILA_ASSERT(input_m1 != NULL) << "Input unmatched: " << input_m0; - - auto input_m0_init = gen.GetExpr(input_m0, suffix_init); - auto input_m1_init = gen.GetExpr(input_m1, suffix_init); - auto init_input = (input_m0_init == input_m1_init); - solver.add(init_input); - } - - // initial condition - for (size_t i = 0; i != inits_.size(); i++) { - auto init_i = inits_[i]; - auto init_e = gen.GetExpr(init_i, suffix_init); - solver.add(init_e); - } - - // invariants - for (size_t i = 0; i != invs_.size(); i++) { - auto inv_i = invs_[i]; - // XXX Only apply invariants on initial states. - auto inv_e = gen.GetExpr(inv_i, suffix_init); - solver.add(inv_e); - } - - auto result = solver.check(); - - if (result == z3::sat) { - auto m = solver.get_model(); - ILA_DLOG("Bmc.Legacy") << m; - } - - return result; -} - -// ------------------- PRIVATE FUNCTIONS ------------------------------------ // - -z3::expr LegacyBmc::UnrollCmplIla(InstrLvlAbsPtr m, const int& k, - const int& pos) { - ILA_NOT_NULL(m); - ILA_ASSERT(k > 0) << "Invalid unroll steps."; - ILA_ASSERT(pos >= 0) << "Negative starting frame number."; - - auto cnst = ctx_.bool_val(true); - - for (auto i = 0; i != k; i++) { - auto suf_prev = std::to_string(pos + i); - auto suf_next = std::to_string(pos + i + 1); - /// XXX May not be one hot and flat -- based on flags. - auto cnst_i = IlaOneHotFlat(m, suf_prev, suf_next); - /// XXX Use rewrite for better performance -- based on flags (or def) - cnst = cnst_i && cnst; - } - - return cnst; -} - -z3::expr LegacyBmc::Instr(const InstrPtr instr, const std::string& suffix_prev, - const std::string& suffix_next, bool complete) { - ILA_NOT_NULL(instr); - ILA_DLOG("ModelGen.Instr") - << (complete ? "Complete " : "Partial ") << "Instruction: " << instr - << " (" << suffix_prev << ", " << suffix_next << ")"; - - auto ila = instr->host(); - ILA_NOT_NULL(ila); - - auto cnst = ctx_.bool_val(true); - - auto state_num = ila->state_num(); - for (size_t i = 0; i != state_num; i++) { - auto state_n = ila->state(i); - auto update_n = instr->update(state_n); - - if (update_n != NULL) { // update function specified - auto next_val_e = gen_.GetExpr(update_n, suffix_prev); - auto next_var_e = gen_.GetExpr(state_n, suffix_next); - auto eq_cnst = (next_var_e == next_val_e); - cnst = cnst && eq_cnst; - } else if (complete == true) { - auto next_val_e = gen_.GetExpr(state_n, suffix_prev); - auto next_var_e = gen_.GetExpr(state_n, suffix_next); - auto eq_cnst = (next_var_e == next_val_e); - cnst = cnst && eq_cnst; - } - } - - auto decode_n = instr->decode(); - ILA_NOT_NULL(decode_n); - auto decode_e = gen_.GetExpr(decode_n, suffix_prev); - auto instr_cnst = Z3Implies(ctx_, decode_e, cnst); - return instr_cnst; -} - -z3::expr LegacyBmc::IlaOneHotFlat(const InstrLvlAbsPtr ila, - const std::string& suffix_prev, - const std::string& suffix_next) { - ILA_NOT_NULL(ila); - ILA_DLOG("ModelGen.IlaOneHotFlat") - << "One-hot Flat ILA: " << ila << " (" << suffix_prev << ", " - << suffix_next << ")"; - auto& gen = gen_; - auto valid_n = ila->valid(); - ILA_NOT_NULL(valid_n); - auto valid_e = gen.GetExpr(valid_n, suffix_prev); - - auto cnst = ctx_.bool_val(true); - auto instr_num = ila->instr_num(); - for (size_t i = 0; i != instr_num; i++) { - auto instr_i = ila->instr(i); - auto instr_cnst = Instr(instr_i, suffix_prev, suffix_next, true); - // Assume one-hot encoding of the instruction decode. - cnst = cnst && instr_cnst; - } - - auto ila_cnst = Z3Implies(ctx_, valid_e, cnst); - return ila_cnst; -} - -} // namespace ilang diff --git a/src/verification/rewrite_expr.cc b/src/verification/rewrite_expr.cc deleted file mode 100644 index 59f012512..000000000 --- a/src/verification/rewrite_expr.cc +++ /dev/null @@ -1,213 +0,0 @@ -/// \file -/// Source for function object for rewriting Expr. - -#include - -#include -#include - -namespace ilang { - -using namespace ExprFuse; - -bool FuncObjRewrExpr::pre(const ExprPtr e) const { - // check rewriting rule to see if defined/visited - auto pos = rule_.find(e); - return pos != rule_.end(); // if found --> break -} - -void FuncObjRewrExpr::post(const ExprPtr e) { - auto dst = Rewrite(e); - auto ok = rule_.insert({e, dst}).second; - // must not be defined, otherwise, there is a cycle. - ILA_ASSERT(ok) << "Rewriting rule redefined (exist cycle in the AST)"; -} - -ExprPtr FuncObjRewrExpr::Rewrite(const ExprPtr e) const { - if (e->is_var() || e->is_const()) { - return e; - } else { - ILA_ASSERT(e->is_op()) << "Unkown type for " << e; - return RewriteOp(e); - } -} - -ExprPtr FuncObjRewrExpr::RewriteOp(const ExprPtr e) const { - // check each type of op - auto expr_op_uid = GetUidExprOp(e); - - switch (expr_op_uid) { - case AST_UID_EXPR_OP::NEG: { - auto a = get(e->arg(0)); - return Negate(a); - } - case AST_UID_EXPR_OP::NOT: { - auto a = get(e->arg(0)); - return Not(a); - } - case AST_UID_EXPR_OP::COMPL: { - auto a = get(e->arg(0)); - return Complement(a); - } - case AST_UID_EXPR_OP::AND: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return And(a0, a1); - } - case AST_UID_EXPR_OP::OR: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Or(a0, a1); - } - case AST_UID_EXPR_OP::XOR: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Xor(a0, a1); - } - case AST_UID_EXPR_OP::SHL: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Shl(a0, a1); - } - case AST_UID_EXPR_OP::ASHR: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Ashr(a0, a1); - } - case AST_UID_EXPR_OP::LSHR: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Lshr(a0, a1); - } - case AST_UID_EXPR_OP::ADD: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Add(a0, a1); - } - case AST_UID_EXPR_OP::SUB: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Sub(a0, a1); - } - case AST_UID_EXPR_OP::DIV: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Div(a0, a1); - } -#if 0 - case AST_UID_EXPR_OP::SREM: { - // TODO - } -#endif - case AST_UID_EXPR_OP::UREM: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return URem(a0, a1); - } -#if 0 - case AST_UID_EXPR_OP::SMOD: { - // TODO - } -#endif - case AST_UID_EXPR_OP::MUL: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Mul(a0, a1); - } - case AST_UID_EXPR_OP::EQ: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Eq(a0, a1); - } - case AST_UID_EXPR_OP::LT: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Lt(a0, a1); - } - case AST_UID_EXPR_OP::GT: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Gt(a0, a1); - } - case AST_UID_EXPR_OP::ULT: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Ult(a0, a1); - } - case AST_UID_EXPR_OP::UGT: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Ugt(a0, a1); - } - case AST_UID_EXPR_OP::LOAD: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Load(a0, a1); - } - case AST_UID_EXPR_OP::STORE: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - auto a2 = get(e->arg(2)); - return Store(a0, a1, a2); - } - case AST_UID_EXPR_OP::CONCAT: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Concat(a0, a1); - } - case AST_UID_EXPR_OP::EXTRACT: { - auto a0 = get(e->arg(0)); - auto p0 = e->param(0); - auto p1 = e->param(1); - return Extract(a0, p0, p1); - } - case AST_UID_EXPR_OP::ZEXT: { - auto a0 = get(e->arg(0)); - auto p0 = e->param(0); - return ZExt(a0, p0); - } - case AST_UID_EXPR_OP::SEXT: { - auto a0 = get(e->arg(0)); - auto p0 = e->param(0); - return SExt(a0, p0); - } - case AST_UID_EXPR_OP::LROTATE: { - auto a0 = get(e->arg(0)); - auto p0 = e->param(0); - return LRotate(a0, p0); - } - case AST_UID_EXPR_OP::RROTATE: { - auto a0 = get(e->arg(0)); - auto p0 = e->param(0); - return RRotate(a0, p0); - } - case AST_UID_EXPR_OP::IMPLY: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - return Imply(a0, a1); - } - case AST_UID_EXPR_OP::ITE: { - auto a0 = get(e->arg(0)); - auto a1 = get(e->arg(1)); - auto a2 = get(e->arg(2)); - return Ite(a0, a1, a2); - } - case AST_UID_EXPR_OP::APP_FUNC: { - auto e_derive = std::static_pointer_cast(e); - ILA_NOT_NULL(e_derive); - - auto f = e_derive->func(); - ExprPtrVec args; - for (decltype(e->arg_num()) i = 0; i != e->arg_num(); i++) { - args.push_back(get(e->arg(i))); - } - return AppFunc(f, args); - } - default: { - ILA_ERROR << "Rewriting " << expr_op_uid << " not implemented"; - return NULL; - } - }; -} - -} // namespace ilang diff --git a/src/verification/rewrite_ila.cc b/src/verification/rewrite_ila.cc deleted file mode 100644 index 5ccee4d92..000000000 --- a/src/verification/rewrite_ila.cc +++ /dev/null @@ -1,103 +0,0 @@ -/// \file -/// Source for function object for rewriting ILA. - -#include - -#include -#include - -namespace ilang { - -InstrLvlAbsPtr FuncObjRewrIla::get(const InstrLvlAbsCnstPtr m) const { - auto pos = ila_map_.find(m); - ILA_ASSERT(pos != ila_map_.end()) << m << " not found"; - return pos->second; -} - -bool FuncObjRewrIla::pre(const InstrLvlAbsCnstPtr src) { - auto pos = ila_map_.find(src); - ILA_ASSERT(pos != ila_map_.end()) << "ILA dst for " << src << " not found."; - auto dst = pos->second; - ILA_ASSERT(dst->state_num() == - (dst->parent() ? dst->parent()->state_num() : 0)) - << "Rewriting ILA to partially constructed ILA not support."; - - // input - AbsKnob::DuplInp(src, dst, expr_map_); - // state - AbsKnob::DuplStt(src, dst, expr_map_); - - // child - for (decltype(src->child_num()) i = 0; i != src->child_num(); i++) { - auto c_src = src->child(i); - auto c_dst = dst->NewChild(c_src->name().str()); - c_dst->set_spec(c_src->is_spec()); - ila_map_.insert({c_src, c_dst}); - } - - // fetch - AbsKnob::DuplFetch(src, dst, expr_map_); - // valid - AbsKnob::DuplValid(src, dst, expr_map_); - // init - AbsKnob::DuplInit(src, dst, expr_map_); - - // instruction && child-program - for (decltype(src->instr_num()) i = 0; i != src->instr_num(); i++) { - auto i_src = src->instr(i); - AbsKnob::DuplInstr(i_src, dst, expr_map_, ila_map_); - } - - // sequence - AbsKnob::DuplInstrSeq(src, dst); - - return false; -} - -void FuncObjRewrIla::post(const InstrLvlAbsCnstPtr src) const { - // nothing -} - -// ----------------------------------------------------------------------------------------- - -/// Constructor. -FuncObjFlatIla::FuncObjFlatIla(const InstrLvlAbsCnstPtr& top_, - const IlaMap& ila_map, const ExprMap& expr_map) - : ila_map_(ila_map), expr_map_(expr_map), top_ila_(top_) { - valid_cond_stack_.push(ExprFuse::BoolConst(true)); -} - -bool FuncObjFlatIla::pre(const InstrLvlAbsCnstPtr src) { - if (src == top_ila_) - return false; // skip the top level ila, do nothing - auto pos = ila_map_.find(src); - ILA_ASSERT(pos != ila_map_.end()) << "ILA dst for " << src << " not found."; - auto dst = pos->second; - - auto valid_cond_ = src->valid(); - if (!valid_cond_) { - ILA_WARN << "valid condition for " << src << " is unset"; - valid_cond_ = ExprFuse::BoolConst(true); - } - valid_cond_stack_.push(ExprFuse::And(valid_cond_stack_.top(), valid_cond_)); - const auto& hierarchical_valid_cond = valid_cond_stack_.top(); - - // instruction && child-program - for (decltype(src->instr_num()) i = 0; i != src->instr_num(); i++) { - auto i_src = src->instr(i); - auto i_dst = AbsKnob::DuplInstr(i_src, dst, expr_map_, ila_map_); - auto new_decode = ExprFuse::And(i_dst->decode(), hierarchical_valid_cond); - } - - // sequence - do we need to do this? - // AbsKnob::DuplInstrSeq(src, dst); - - return false; -} - -void FuncObjFlatIla::post(const InstrLvlAbsCnstPtr src) { - // pop the stack - valid_cond_stack_.pop(); -} - -} // namespace ilang diff --git a/src/verification/unroller.cc b/src/verification/unroller.cc deleted file mode 100644 index 5886bbf61..000000000 --- a/src/verification/unroller.cc +++ /dev/null @@ -1,493 +0,0 @@ -/// \file -/// Source for unrolling ILA execution. - -#include - -#include -#include - -#include -#include - -namespace ilang { - -using namespace ExprFuse; - -typedef Unroller::ZExpr ZExpr; - -/******************************************************************************/ -// Unroller -/******************************************************************************/ -Unroller::Unroller(z3::context& ctx, const std::string& suff) - : ctx_(ctx), gen_(Z3ExprAdapter(ctx)), k_prev_z3_(ctx), k_curr_z3_(ctx), - k_next_z3_(ctx), cstr_(ctx) { - // SetExtraSuffix(suff); - extra_suff_ = suff; -} - -Unroller::~Unroller() {} - -void Unroller::AddGlobPred(const ExprPtr p) { g_pred_.push_back(p); } - -void Unroller::AddInitPred(const ExprPtr p) { i_pred_.push_back(p); } - -void Unroller::AddStepPred(const ExprPtr p, const int& k) { - s_pred_[k].push_back(p); -} - -void Unroller::ClearGlobPred() { g_pred_.clear(); } - -void Unroller::ClearInitPred() { i_pred_.clear(); } - -void Unroller::ClearStepPred() { s_pred_.clear(); } - -void Unroller::ClearPred() { - ClearGlobPred(); - ClearInitPred(); - ClearStepPred(); -} - -ZExpr Unroller::CurrState(const ExprPtr v, const int& t) { - ILA_ASSERT(v->is_var()) << "Use GetZ3Expr for non-var Expr"; - return gen().GetExpr(v, SuffCurr(t)); -} - -ZExpr Unroller::NextState(const ExprPtr v, const int& t) { - ILA_ASSERT(v->is_var()) << "Next state only exist for var"; - return gen().GetExpr(v, SuffNext(t)); -} - -ZExpr Unroller::GetZ3Expr(const ExprPtr e, const int& t) { - return gen().GetExpr(e, SuffCurr(t)); -} - -ZExpr Unroller::GetZ3Expr(const ExprPtr e) { - return gen().GetExpr(e, extra_suff_); -} - -ZExpr Unroller::Equal(const ExprPtr a, const int& ta, const ExprPtr b, - const int& tb) { - auto a_expr = gen().GetExpr(a, SuffCurr(ta)); - auto b_expr = gen().GetExpr(b, SuffCurr(tb)); - return a_expr == b_expr; -} - -ZExpr Unroller::UnrollSubs(const size_t& len, const int& pos) { - // bootstrap basic information - BootStrap(pos); - - // unroll based on g_pred, i_pred, and transition relation (with guard) - for (size_t i = 0; i != len; i++) { - // time-stamp for this time-frame - auto k_suffix = SuffCurr(pos + i); - - // get transition relation (k_next_) and step-specific predicate (k_pred_) - Transition(i); - - // the source for substitution - Clear(k_curr_z3_); - IExprToZExpr(vars_, k_suffix, k_curr_z3_); - - // alias (reference) - auto subs_src = k_curr_z3_; - auto subs_dst = k_prev_z3_; - // rewrite and assert initial predicate - if (i == 0) { - IExprToZExpr(i_pred_, k_suffix, cstr_, subs_src, subs_dst); - } - // rewrite and assert global predicate - IExprToZExpr(g_pred_, k_suffix, cstr_, subs_src, subs_dst); - // rewrite and assert step-specific predicate - IExprToZExpr(k_pred_, k_suffix, cstr_, subs_src, subs_dst); - // rewrite and assert (external) step-specific predicate - IExprToZExpr(s_pred_[i], k_suffix, cstr_, subs_src, subs_dst); - - // rewrite and add transition relation - Clear(k_next_z3_); - IExprToZExpr(k_next_, k_suffix, k_next_z3_, subs_src, subs_dst); - // update next state function to the prev for next step - CopyZExprVec(k_next_z3_, k_prev_z3_); - } - - // add constraints for transition relation (k_prev_ has the last value) - AssertEqual(k_prev_z3_, vars_, SuffCurr(len)); - - { // extend for end states (invariant and step-specific predicates) - auto k_suffix = SuffCurr(len); - IExprToZExpr(g_pred_, k_suffix, cstr_); - IExprToZExpr(s_pred_[len], k_suffix, cstr_); - } - - // accumulate all constraints and return - auto cstr = ConjPred(cstr_); - return cstr; -} - -ZExpr Unroller::UnrollAssn(const size_t& len, const int& pos, bool cache) { - // bootstrap basic information - BootStrap(pos, cache); - - // unroll based on g_pred, i_pred, and transition relation (with guard) - for (size_t i = 0; i != len; i++) { - // time-stamp for this time-frame - auto k_suffix = SuffCurr(pos + i); - - // get transition relation (k_next_) and step-specific predicate (k_pred_) - Transition(i); - - // assert initial predicate - if (i == 0) { - IExprToZExpr(i_pred_, k_suffix, cstr_); - } - // assert global predicate - IExprToZExpr(g_pred_, k_suffix, cstr_); - // assert (external) step-specific predicate - IExprToZExpr(s_pred_[i], k_suffix, cstr_); - // assert step-specific predicate - IExprToZExpr(k_pred_, k_suffix, cstr_); - - // assert transition relation - Clear(k_next_z3_); - IExprToZExpr(k_next_, k_suffix, k_next_z3_); - // assert equal between next state value and next state var - AssertEqual(k_next_z3_, vars_, SuffCurr(pos + i + 1)); - } - - { // extend for end states (invariant and step-specific predicates) - auto k_suffix = SuffCurr(len); - IExprToZExpr(g_pred_, k_suffix, cstr_); - IExprToZExpr(s_pred_[len], k_suffix, cstr_); - } - - // accumulate all constraints and return - auto cstr = ConjPred(cstr_); - return cstr; -} - -ZExpr Unroller::UnrollNone(const size_t& len, const int& pos) { - // bootstrap basic information - BootStrap(pos); - - // unroll based on g_pred, i_pred, and transition relation (with guard) - for (size_t i = 0; i != len; i++) { - // time-stamp for this time-frame - auto k_suffix = SuffCurr(pos + i); - - // get transition relation (k_next_) and step-specific predicate (k_pred_) - Transition(i); - - // assert initial predicate - if (i == 0) { - IExprToZExpr(i_pred_, k_suffix, cstr_); - } - // assert global predicate - IExprToZExpr(g_pred_, k_suffix, cstr_); - // assert step-specific predicate - IExprToZExpr(k_pred_, k_suffix, cstr_); - // assert (external) step-specific predicate - IExprToZExpr(s_pred_[i], k_suffix, cstr_); - - // assert transition relation - Clear(k_next_z3_); - IExprToZExpr(k_next_, k_suffix, k_next_z3_); - // assert equal between next state value and next state var - AssertEqual(k_next_z3_, vars_, SuffNext(pos + i)); - } - - // accumulate all constraints and return - auto cstr = ConjPred(cstr_); - return cstr; -} - -ExprPtr Unroller::StateUpdCmpl(const InstrPtr instr, const ExprPtr var) { - auto upd = instr->update(var); - return (upd) ? upd : var; -} - -ExprPtr Unroller::DecodeCmpl(const InstrPtr instr) { - auto dec = instr->decode(); - return (dec) ? dec : BoolConst(true); -} - -ExprPtr Unroller::NewFreeVar(const ExprPtr var, const std::string& name) { - auto host = var->host(); - ILA_NOT_NULL(host); - - if (var->is_bool()) { - return host->NewBoolFreeVar(name); - } else if (var->is_bv()) { - return host->NewBvFreeVar(name, var->sort()->bit_width()); - } else { - ILA_ASSERT(var->is_mem()) << "Unknown sort for " << var; - return host->NewMemFreeVar(name, var->sort()->addr_width(), - var->sort()->data_width()); - } -} - -void Unroller::BootStrap(const int& pos, bool cache) { - if (!cache) { - vars_.clear(); - k_pred_.clear(); - k_next_.clear(); - // collect dependant state variables - DefineDepVar(); - ILA_ASSERT(!vars_.empty()) << "No state variable defined."; - - Clear(k_prev_z3_); - Clear(k_curr_z3_); - Clear(k_next_z3_); - Clear(cstr_); - - // prepare the table - for (auto it = vars_.begin(); it != vars_.end(); it++) { - auto ivar = *it; - auto zvar = gen().GetExpr(ivar, SuffCurr(pos)); - k_prev_z3_.push_back(zvar); - } - } else { // cache - if (vars_.empty()) { - DefineDepVar(); - ILA_ASSERT(k_prev_z3_.empty()) << "Unexpected behavior in cacheing"; - for (auto it = vars_.begin(); it != vars_.end(); it++) { - auto ivar = *it; - auto zvar = gen().GetExpr(ivar, SuffCurr(pos)); - k_prev_z3_.push_back(zvar); - } - } - } -} - -void Unroller::AssertEqual(const ZExprVec& a, const IExprVec& b, - const std::string& suffix) { - ILA_ASSERT(a.size() == b.size()) << "Var num mismatch."; - for (unsigned i = 0; i != a.size(); i++) { - auto ai = a[i]; - auto bi = gen().GetExpr(b[i], suffix); - auto equal = (ai == bi); - cstr_.push_back(equal); - } -} - -void Unroller::Clear(ZExprVec& z3_vec) { z3_vec.resize(0); } - -void Unroller::IExprToZExpr(const IExprVec& i_expr_src, - const std::string& suffix, ZExprVec& z_expr_dst) { - for (auto it = i_expr_src.begin(); it != i_expr_src.end(); it++) { - auto i_expr = *it; - auto z_expr = gen().GetExpr(i_expr, suffix); - z_expr_dst.push_back(z_expr); - } -} - -void Unroller::IExprToZExpr(const IExprVec& i_expr_src, - const std::string& suffix, ZExprVec& z_expr_dst, - const ZExprVec& subs_src, - const ZExprVec& subs_dst) { - for (auto it = i_expr_src.begin(); it != i_expr_src.end(); it++) { - auto i_expr = *it; - auto z_expr = gen().GetExpr(i_expr, suffix); - auto z_subs = z_expr.substitute(subs_src, subs_dst); - z_expr_dst.push_back(z_subs); - } -} - -void Unroller::CopyZExprVec(const ZExprVec& src, ZExprVec& dst) { - Clear(dst); - for (unsigned i = 0; i != src.size(); i++) { - dst.push_back(src[i]); - } -} - -ZExpr Unroller::ConjPred(const ZExprVec& vec) const { - auto conj = ctx().bool_val(true); - for (size_t i = 0; i != vec.size(); i++) { - conj = (conj && vec[i]); - } - conj = conj.simplify(); - return conj; -} - -/******************************************************************************/ -// PathUnroll -/******************************************************************************/ -PathUnroll::PathUnroll(z3::context& ctx, const std::string& suff) - : Unroller(ctx, suff) {} - -PathUnroll::~PathUnroll() {} - -ZExpr PathUnroll::PathSubs(const InstrVec& seq, const int& pos) { - // set up target transition relation - seq_ = seq; - return UnrollSubs(seq.size(), pos); -} - -ZExpr PathUnroll::PathAssn(const InstrVec& seq, const int& pos) { - // set up target transition relation - seq_ = seq; - return UnrollAssn(seq.size(), pos); -} - -ZExpr PathUnroll::PathNone(const InstrVec& seq, const int& pos) { - // set up target transition relation - seq_ = seq; - return UnrollNone(seq.size(), pos); -} - -void PathUnroll::DefineDepVar() { - // collect the set of vars - auto dep_var = ExprSet(); - for (auto it = seq_.begin(); it != seq_.end(); it++) { - AbsKnob::InsertStt(*it, dep_var); - } - // update to the global set - vars_.clear(); - for (auto it = dep_var.begin(); it != dep_var.end(); it++) { - vars_.push_back(*it); - } -} - -void PathUnroll::Transition(const int& idx) { - ILA_CHECK(idx < (int)seq_.size()) << "Out-of-bound transition not defined."; - auto instr = seq_[idx]; - - // update next state function (k_next_) - k_next_.resize(0); - for (auto it = vars_.begin(); it != vars_.end(); it++) { - auto var = *it; - auto next = StateUpdCmpl(instr, var); - k_next_.push_back(next); - } - - // update step predicate (k_pred_) - k_pred_.resize(0); - auto dec = instr->decode(); - ILA_NOT_NULL(dec); - k_pred_.push_back(dec); -} - -/******************************************************************************/ -// MonoUnroll -/******************************************************************************/ -MonoUnroll::MonoUnroll(z3::context& ctx, const std::string& suff) - : Unroller(ctx, suff) {} - -MonoUnroll::~MonoUnroll() {} - -ZExpr MonoUnroll::MonoSubs(const InstrLvlAbsPtr top, const int& length, - const int& pos) { - top_ = top; - return UnrollSubs(length, pos); -} - -ZExpr MonoUnroll::MonoAssn(const InstrLvlAbsPtr top, const int& length, - const int& pos) { - top_ = top; - return UnrollAssn(length, pos); -} - -ZExpr MonoUnroll::MonoNone(const InstrLvlAbsPtr top, const int& length, - const int& pos) { - top_ = top; - return UnrollNone(length, pos); -} - -ZExpr MonoUnroll::MonoIncr(const InstrLvlAbsPtr top, const int& length, - const int& pos) { - top_ = top; - return UnrollAssn(length, pos, - false); // XXX non-cache has better performance -} - -void MonoUnroll::DefineDepVar() { - vars_.clear(); - auto dep_var = AbsKnob::GetSttTree(top_); - // update global - ILA_ASSERT(!dep_var.empty()) << "No state var found."; - for (auto it = dep_var.begin(); it != dep_var.end(); it++) { - vars_.push_back(*it); - } -} - -// - decode is embedded in the update function -// - instruction selection is encoded as step predicate -// - next state var is the representation of the update function -void MonoUnroll::Transition(const int& idx) { - // check whether the table has been generated. - if (!k_next_.empty()) { - ILA_ASSERT(k_next_.size() == vars_.size()) << "Table size mismatch."; - return; - } - - // extract the set of insturctions - auto instr_set = AbsKnob::GetInstrTree(top_); - - // create the set of selection bits - std::vector sel_bits; - for (auto it = instr_set.begin(); it != instr_set.end(); it++) { - auto instr = *it; - auto host = instr->host(); - auto sel = host->NewBoolFreeVar(instr->name().str() + ".sel"); - sel_bits.push_back(sel); - } - // dummy selection bits (used for deadlock) - auto sel_dum = top_->NewBoolFreeVar("dead.sel"); - - auto var_num = vars_.size(); - auto instr_num = instr_set.size(); - ILA_ASSERT(instr_num == sel_bits.size()); - - // next state function - for (size_t v_idx = 0; v_idx != var_num; v_idx++) { - auto var = vars_[v_idx]; - auto var_next = NewFreeVar(var, var->name().str() + ".vnxt"); - // add virtual next state to the update table - k_next_.push_back(var_next); - - // accumulate update and decode function constraints - auto not_dec = BoolConst(true); - auto acc_dec = BoolConst(true); - auto acc_upd = BoolConst(true); - // loop through all instructions - for (size_t i_idx = 0; i_idx != instr_set.size(); i_idx++) { - auto instr = instr_set.at(i_idx); - auto sel = sel_bits.at(i_idx); - // sel -> decode - auto decode = DecodeCmpl(instr); - acc_dec = And(acc_dec, Imply(sel, decode)); - not_dec = And(not_dec, Not(decode)); - // sel -> Next(v, v') - auto next = StateUpdCmpl(instr, var); - auto equal = Eq(var_next, next); - acc_upd = And(acc_upd, Imply(sel, equal)); - } - // dummy selection - acc_dec = And(acc_dec, Imply(sel_dum, not_dec)); - acc_upd = And(acc_upd, Imply(sel_dum, Eq(var_next, var))); - - // add to predicate - k_pred_.push_back(acc_dec); - k_pred_.push_back(acc_upd); - } - - // one-hot encoding (need to include dummy) - // at least one (c1 \/ c2 \/ ... \/ cm) - auto one_hot_at_least_one = sel_dum; - for (size_t i = 0; i != instr_num; i++) { - auto sel_i = sel_bits.at(i); - one_hot_at_least_one = Or(one_hot_at_least_one, sel_i); - } - k_pred_.push_back(one_hot_at_least_one); - // at most one (/\ii (!ci \/ !cj)) - auto one_hot_at_most_one = BoolConst(true); - for (size_t i = 0; i != instr_num; i++) { - auto sel_i = sel_bits.at(i); - for (size_t j = i + 1; j != instr_num; j++) { - auto sel_j = sel_bits.at(j); - auto not_both_true = Or(Not(sel_i), Not(sel_j)); - one_hot_at_most_one = And(one_hot_at_most_one, not_both_true); - } - } - k_pred_.push_back(one_hot_at_most_one); -} - -} // namespace ilang diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 5571694ef..1b6a1a0a1 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -62,6 +62,7 @@ package_add_test(${ILANG_TEST_MAIN} t_ila.cc t_ila_sim.cc t_ila_sim_cmake.cc + t_ilator.cc t_instr.cc t_instr_seq.cc t_keyvec.cc @@ -70,6 +71,7 @@ package_add_test(${ILANG_TEST_MAIN} t_main.cc t_mapset.cc t_mcm.cc + t_mngr_absknob.cc t_pass.cc t_portable.cc t_sort.cc diff --git a/test/t_api.cc b/test/t_api.cc index 28ea2b0d1..5b8aa43b5 100644 --- a/test/t_api.cc +++ b/test/t_api.cc @@ -23,6 +23,7 @@ TEST(TestApi, LogicShift) { TEST(TestApi, Construct) { Ila ila("top"); + EXPECT_EQ(ila.name(), "top"); // state auto flag = ila.NewBoolState("flag"); @@ -32,6 +33,7 @@ TEST(TestApi, Construct) { regs.push_back(ila.NewBvState(reg_name, REG_SIZE)); } auto mem = ila.NewMemState("mem", REG_SIZE, REG_SIZE); + EXPECT_EQ(mem.name(), "mem"); // input auto bool_in = ila.NewBoolInput("bool_in"); @@ -39,6 +41,8 @@ TEST(TestApi, Construct) { EXPECT_EQ(2, ila.input_num()); EXPECT_EQ(bool_in.get(), ila.input(0).get()); EXPECT_EQ(bv_in.get(), ila.input("bv_in").get()); + EXPECT_EQ(bool_in.name(), "bool_in"); + EXPECT_EQ(bv_in.name(), "bv_in"); // init auto flag_init = (flag == BoolConst(true)); @@ -61,6 +65,7 @@ TEST(TestApi, Construct) { // instr and ast { auto instr = ila.NewInstr("instr_0"); + EXPECT_EQ(instr.name(), "instr_0"); auto decode = (regs[1] < regs[2]); instr.SetDecode(decode); @@ -252,6 +257,10 @@ TEST(TestApi, Function) { FuncRef f1("f1", s_out, s_arg0); FuncRef f2("f2", s_out, s_arg0, s_arg1); FuncRef f3("f3", s_out, {s_arg0, s_arg1, s_arg2}); + EXPECT_EQ(f0.name(), "f0"); + EXPECT_EQ(f1.name(), "f1"); + EXPECT_EQ(f2.name(), "f2"); + EXPECT_EQ(f3.name(), "f3"); Ila ila("host"); auto i0 = BoolConst(true); @@ -374,7 +383,7 @@ TEST(TestApi, Unroll) { unroller.AddInitPred(m1.init(i)); } unroller.AddInitPred(init_mem == m1.state("ir")); - auto cstr11 = unroller.UnrollPathConn(path); + auto cstr11 = unroller.UnrollPathSubs(path); z3::solver s(c); s.add(cstr00); diff --git a/test/t_ilator.cc b/test/t_ilator.cc new file mode 100644 index 000000000..ff96ff537 --- /dev/null +++ b/test/t_ilator.cc @@ -0,0 +1,39 @@ +/// \file +/// Test for Ilator + +#include + +#include +#include + +#include "unit-include/config.h" +#include "unit-include/ila_sim_test.h" +#include "unit-include/util.h" + +namespace ilang { + +class TestIlator : public ::testing::Test { +public: + TestIlator() {} + ~TestIlator() {} + + void SetUp() { + out_dir = GetRandomFileName(fs::temp_directory_path()); + os_portable_mkdir(out_dir); + } + + void TearDown() { + // for CI tests, may be needed for out-of-scope build tests + os_portable_remove_directory(out_dir); + } + + fs::path out_dir; + +}; // TestIlator + +TEST_F(TestIlator, IlaSimTest) { + IlaSimTest m; + ExportSysCSim(m.model, out_dir); +} + +} // namespace ilang diff --git a/test/t_mngr_absknob.cc b/test/t_mngr_absknob.cc new file mode 100644 index 000000000..0ce7c7fbc --- /dev/null +++ b/test/t_mngr_absknob.cc @@ -0,0 +1,43 @@ +/// \file +/// Tests for ILA manager utility - AbsKnob + +#include + +#include "unit-include/util.h" + +namespace ilang { + +TEST(TestMngrAbsKnob, FlattenIla) { + // parent + auto m = Ila("parent"); + auto x = m.NewBvState("x", 8); + m.SetValid(x != 0); + auto i0 = m.NewInstr("i0"); + i0.SetDecode(x > 1); + i0.SetUpdate(x, x + 1); + + // child <- parent + auto c = m.NewChild("child"); + auto y = c.NewBvState("y", 8); + c.SetValid(y != 0); + auto i1 = c.NewInstr("i1"); + i1.SetDecode(y > 1); + i1.SetUpdate(y, y + 1); + + EXPECT_EQ(m.instr_num(), 1); + m.FlattenHierarchy(); + EXPECT_EQ(m.instr_num(), 2); + + // grand <- child <- parent + auto g = c.NewChild("grand"); + auto z = g.NewBvState("z", 8); + g.SetValid(z != 0); + auto i2 = g.NewInstr("i2"); + i2.SetDecode(z > 1); + + EXPECT_EQ(m.instr_num(), 2); + m.FlattenHierarchy(); + EXPECT_EQ(m.instr_num(), 3); +} + +} // namespace ilang