diff --git a/.semaphore/semaphore.yml b/.semaphore/semaphore.yml index 1e1c1c1fe..91c4d4c66 100644 --- a/.semaphore/semaphore.yml +++ b/.semaphore/semaphore.yml @@ -14,12 +14,12 @@ blocks: - name: build_install_test commands: - sudo apt-get update - - sudo apt-get install -y bison flex libboost-all-dev z3 libz3-dev - - export CC=gcc-7 - - export CXX=g++-7 + - sudo apt-get install -y bison flex z3 libz3-dev + - export CC=gcc-8 + - export CXX=g++-8 - mkdir build - cd build - - cmake .. -DCMAKE_BUILD_TYPE=Debug -DILANG_BUILD_SYNTH=ON + - cmake .. -DCMAKE_BUILD_TYPE=Debug - make -j$(nproc) - sudo make install - make run_test diff --git a/.travis.yml b/.travis.yml index 4d1233cc1..6d39ff479 100644 --- a/.travis.yml +++ b/.travis.yml @@ -60,8 +60,8 @@ jobs: - 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- - before_script: - eval "${MATRIX_EVAL}" + before_script: - 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 @@ -75,7 +75,6 @@ addons: - lcov - flex - bison - - libboost-all-dev - z3 - libz3-dev - g++-7 diff --git a/CMakeLists.txt b/CMakeLists.txt index 397749c2a..d0255502b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -11,7 +11,7 @@ endif() # PROJECT # name version language # ---------------------------------------------------------------------------- # -project(ilang VERSION 1.1.0 +project(ilang VERSION 1.1.1 LANGUAGES CXX ) diff --git a/README.md b/README.md index 3e95329c7..857790309 100644 --- a/README.md +++ b/README.md @@ -59,13 +59,11 @@ brew install bison flex z3 | 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 | +| Ubuntu 16.04 (Xenial) | gcc 7.5.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.0 | Release | +| Ubuntu 18.04 (Bionic) | gcc 8.4.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4 | Debug | +| Ubuntu 18.04 (Bionic) | gcc 8.4.0 | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4 | Release | +| Ubuntu 20.04 (Focal Fosa) | gcc 9.3.0 | 3.17.0 | 4.8.7 | 3.0.4 | 2.6.4 | 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 | diff --git a/appveyor.yml b/appveyor.yml index ccb6613be..d27d347c8 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -10,7 +10,7 @@ build_script: - cd $APPVEYOR_BUILD_FOLDER - mkdir -p build - cd build -- cmake .. -DCMAKE_BUILD_TYPE=Release +- cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_COMPILER=g++-9 - make -j$(nproc) - sudo make install - make test diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 1c03a137e..e87518651 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -63,7 +63,6 @@ jobs: sudo apt-get update sudo apt-get install bison sudo apt-get install flex - sudo apt-get install libboost-all-dev sudo apt-get install z3 sudo apt-get install libz3-dev displayName: 'package' @@ -84,14 +83,13 @@ jobs: sudo apt-get update sudo apt-get install bison sudo apt-get install flex - sudo apt-get install libboost-all-dev sudo apt-get install z3 sudo apt-get install libz3-dev displayName: 'package' - script: | mkdir -p build cd build - cmake .. -DCMAKE_BUILD_TYPE=Release + cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_COMPILER=g++-8 cmake --build . sudo cmake --build . --target install cmake --build . --target test diff --git a/include/ilang/ila-mngr/pass.h b/include/ilang/ila-mngr/pass.h index e2b3e989e..949b414e4 100644 --- a/include/ilang/ila-mngr/pass.h +++ b/include/ilang/ila-mngr/pass.h @@ -11,28 +11,38 @@ /// \namespace ilang namespace ilang { +/// \namespace pass +namespace pass { + /// Infer the control flow graph among the child-instructions (instr. seq.) -bool PassInferChildProgCFG(const InstrLvlAbsPtr& m); +bool InferChildProgCFG(const InstrLvlAbsPtr& m); /// Map the child program (and its entry point) to the parent instruction -bool PassMapChildProgEntryPoint(const InstrLvlAbsPtr& m); +bool MapChildProgEntryPoint(const InstrLvlAbsPtr& m); /// Rewrite the conditional STORE in the AST. -bool PassRewriteConditionalStore(const InstrLvlAbsPtr& m); +bool RewriteConditionalStore(const InstrLvlAbsPtr& m); /// Rewrite the STORE-LOAD pattern in the AST. -bool PassRewriteStoreLoad(const InstrLvlAbsPtr& m); +bool RewriteStoreLoad(const InstrLvlAbsPtr& m); /// A pass template for rewriting AST in an ILA. /// \param[in] m The target ILA. /// \param[in] Rewr The pass-specific rewriting function. -bool PassRewriteGeneric(const InstrLvlAbsPtr& m, - std::function Rewr); +bool RewriteGeneric(const InstrLvlAbsPtr& m, + std::function Rewr); -/// Simplify instruction state updates. -/// \param[in] m The target ILA. +/// \brief Simplify instructions (across the hierarchy) semantically (z3). +/// \param[in] m The top-level ILA. /// \param[in] timeout Max time (ms) for each SMT query. (-1 for default) -bool PassSimplifyInstrUpdate(const InstrLvlAbsPtr& m, const int& timeout = -1); +bool SimplifySemantic(const InstrLvlAbsCnstPtr& m, const int& timeout = -1); + +/// \brief Simplify instructions (across the hierarchy) syntactically. +/// (Light-weight simplification, no SMT query.) +/// \param[in] m The top-level ILA. +bool SimplifySyntactic(const InstrLvlAbsPtr& m); + +} // namespace pass }; // namespace ilang diff --git a/include/ilang/ila-mngr/u_rewriter.h b/include/ilang/ila-mngr/u_rewriter.h index a698c9e1a..8e141db11 100644 --- a/include/ilang/ila-mngr/u_rewriter.h +++ b/include/ilang/ila-mngr/u_rewriter.h @@ -15,41 +15,42 @@ class FuncObjRewrExpr { FuncObjRewrExpr(const ExprMap& rule) : rule_(rule) {} /// Return the rewritten result. - ExprPtr get(const ExprPtr e) const; + ExprPtr get(const ExprPtr& e) const; /// Pre-process: return true (break) if the node has been visited. - bool pre(const ExprPtr e) const; + bool pre(const ExprPtr& e) const; /// Post-process: update the rewriting rule map. - void post(const ExprPtr e); + void post(const ExprPtr& e); protected: /// Internal rewriting table. ExprMap rule_; /// Rewrite all sorts of Expr. - virtual ExprPtr Rewrite(const ExprPtr e) const; + virtual ExprPtr Rewrite(const ExprPtr& e) const; /// Rewrite Operation sorted Expr. - virtual ExprPtr RewriteOp(const ExprPtr e) const; + virtual ExprPtr RewriteOp(const ExprPtr& e) const; }; // class FuncObjRewrExpr /// \brief Function object for rewriting ILA tree. class FuncObjRewrIla { -public: +private: /// Type for storing ILA to ILA mapping. typedef CnstIlaMap IlaMap; +public: /// Constructor. FuncObjRewrIla(const IlaMap& ila_map, const ExprMap& expr_map) : ila_map_(ila_map), expr_map_(expr_map) {} /// Return the mapped ILA. - InstrLvlAbsPtr get(const InstrLvlAbsCnstPtr m) const; + InstrLvlAbsPtr get(const InstrLvlAbsCnstPtr& m) const; /// Pre-processing: create new ILA based on the given source. - bool pre(const InstrLvlAbsCnstPtr src); + bool pre(const InstrLvlAbsCnstPtr& src); /// Nothing. - void post(const InstrLvlAbsCnstPtr src) const; + void post(const InstrLvlAbsCnstPtr& src) const; private: /// ILA mapping. @@ -71,21 +72,24 @@ class FuncObjFlatIla { - Hongce */ -public: +private: /// Type for storing ILA to ILA mapping. typedef CnstIlaMap IlaMap; - typedef std::stack ValidCondStack; +public: /// Constructor. FuncObjFlatIla(const InstrLvlAbsCnstPtr& top_, const IlaMap& ila_map, const ExprMap& expr_map); /// Pre-processing: create new ILA based on the given source. - bool pre(const InstrLvlAbsCnstPtr src); + bool pre(const InstrLvlAbsCnstPtr& src); /// Nothing. - void post(const InstrLvlAbsCnstPtr src); + void post(const InstrLvlAbsCnstPtr& src); private: + /// Type for holding valid condition stack across the hierarchy. + typedef std::stack ValidCondStack; + /// ILA mapping. IlaMap ila_map_; /// Expr mapping. diff --git a/include/ilang/ila-mngr/u_smt_switch.h b/include/ilang/ila-mngr/u_smt_switch.h index e8b80ec7c..edf9e2d48 100644 --- a/include/ilang/ila-mngr/u_smt_switch.h +++ b/include/ilang/ila-mngr/u_smt_switch.h @@ -55,8 +55,6 @@ class SmtSwitchItf { // ------------------------- HELPERS -------------------------------------- // /// Insert the SMT Term of the given node into the map. void PopulateExprMap(const ExprPtr expr); - /// Make Term of expr based on its argument terms. - smt::Term Expr2Term(const ExprPtr expr, const smt::TermVec& arg_terms); /// Make Term of expr variable. smt::Term ExprVar2Term(const ExprPtr expr); /// Make Term of expr constant. diff --git a/include/ilang/ila-mngr/u_unroller.h b/include/ilang/ila-mngr/u_unroller.h index ae5f4be21..1ea75747b 100644 --- a/include/ilang/ila-mngr/u_unroller.h +++ b/include/ilang/ila-mngr/u_unroller.h @@ -57,6 +57,8 @@ class Unroller { ZExpr GetZ3Expr(const ExprPtr e); /// Return the z3::expr representing a and b are equal at their time. ZExpr Equal(const ExprPtr va, const int& ta, const ExprPtr vb, const int& tb); + /// Return the z3::func_decl representing f. + z3::func_decl GetZ3FuncDecl(const FuncPtr& f) const; protected: // ------------------------- MEMBERS -------------------------------------- // diff --git a/include/ilang/ila/hash_ast.h b/include/ilang/ila/hash_ast.h index b562ddf22..9ed2ec154 100644 --- a/include/ilang/ila/hash_ast.h +++ b/include/ilang/ila/hash_ast.h @@ -14,17 +14,15 @@ namespace ilang { /// \brief Simplifier for AST trees by sharing nodes based on the hash value. class ExprMngr { public: + /// Pointer type for passing shared ast simplifier. + typedef std::shared_ptr ExprMngrPtr; + // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // /// Default constructor. ExprMngr(); /// Default destructor. ~ExprMngr(); - /// Pointer type for passing shared ast simplifier. - typedef std::shared_ptr ExprMngrPtr; - /// Type for cacheing the AST node hashing. - typedef std::unordered_map HashTable; - // ------------------------- HELPERS -------------------------------------- // /// \brief Create an object and return the pointer. Used for hiding /// implementation specific types. @@ -36,18 +34,18 @@ class ExprMngr { // ------------------------- METHODS -------------------------------------- // /// Return the AST node representative. - ExprPtr GetRep(const ExprPtr node); + ExprPtr GetRep(const ExprPtr& node); /// Function object for sharing ast nodes. - void operator()(const ExprPtr node); + void operator()(const ExprPtr& node); private: // ------------------------- MEMBERS -------------------------------------- // /// The map for AST nodes. - HashTable map_; + std::unordered_map map_; // ------------------------- HELPER FUNCTIONS ----------------------------- // /// Hash function. - size_t Hash(const ExprPtr node) const; + static std::string Hash(const ExprPtr& node); }; // class ExprMngr diff --git a/include/ilang/ilang++.h b/include/ilang/ilang++.h index 92ce5615d..3554657cd 100644 --- a/include/ilang/ilang++.h +++ b/include/ilang/ilang++.h @@ -398,6 +398,8 @@ class FuncRef { // ------------------------- ACCESSORS/MUTATORS --------------------------- // /// Return the function name as std::string. std::string name() const; + /// Return the wrapped Func pointer. + inline FuncPtr get() const { return ptr_; } // ------------------------- METHODS -------------------------------------- // /// Apply the function with no argument. @@ -409,11 +411,6 @@ class FuncRef { /// Apply the function with multiple arguments. ExprRef operator()(const std::vector& argvec) const; -private: - // ------------------------- ACCESSORS/MUTATORS --------------------------- // - /// Return the wrapped Func pointer. - inline FuncPtr get() const { return ptr_; } - }; // class FuncRef /// \brief The wrapper of Instr (instruction). @@ -583,6 +580,18 @@ class Ila { /// top-level parent instructions. void FlattenHierarchy(); + /// \brief Supported pass ID. + typedef enum PassID { + SIMPLIFY_SYNTACTIC = 0, + SIMPLIFY_SEMANTIC, + REWRITE_CONDITIONAL_STORE, + REWRITE_LOAD_FROM_STORE + } PassID; + + /// \brief Execute the specified passes in order. + /// \param[in] passes the list of passes to execute. + bool ExecutePass(const std::vector& passes) const; + }; // class Ila /******************************************************************************/ @@ -607,6 +616,7 @@ bool ExportIlaPortable(const Ila& ila, const std::string& file_name); /// \param[in] file_name the name of the ILA portable (JSON) file to import. Ila ImportIlaPortable(const std::string& file_name); +#ifdef SYNTH_INTERFACE /// \brief Import the synthesized abstraction from file. /// \param[in] file_name the name of the synthesized abstraction (.ila) file. /// \param[in] ila_name the name of the generated ILA. @@ -620,9 +630,14 @@ Ila ImportSynthAbstraction(const std::string& file_name, /// \param[in] ila_name the name pf the generated child-ILA. void ImportChildSynthAbstraction(const std::string& file_name, Ila& parent, const std::string& ila_name); +#endif // SYNTH_INTERFACE /// \brief Generate the SystemC simulator. -void ExportSysCSim(const Ila& ila, const std::string& dir_path); +/// \param [in] ila the top-level ILA to generate. +/// \param [in] dir_path directory path of the generated simulator. +/// \param [in] optimize set true to enable optimization. +void ExportSysCSim(const Ila& ila, const std::string& dir_path, + bool optimize = false); /******************************************************************************/ // Verification. @@ -692,6 +707,8 @@ class IlaZ3Unroller { /// Return the z3::expr representing a and b are equal at their time. z3::expr Equal(const ExprRef& va, const int& ta, const ExprRef& vb, const int& tb); + /// Return the z3::func_decl representing f. + z3::func_decl GetZ3FuncDecl(const FuncRef& f) const; private: // ------------------------- MEMBERS -------------------------------------- // diff --git a/include/ilang/target-sc/ilator.h b/include/ilang/target-sc/ilator.h index 2ff338b28..2eae3ee9b 100644 --- a/include/ilang/target-sc/ilator.h +++ b/include/ilang/target-sc/ilator.h @@ -29,7 +29,8 @@ class Ilator { // ------------------------- METHODS -------------------------------------- // /// \brief Generate the SystemC simulator. /// \param[in] dst the directory path for the generated simulator. - void Generate(const std::string& dst); + /// \param[in] opt set true to enable optimization. + void Generate(const std::string& dst, bool opt); private: /// Internal type of the string buffer. @@ -74,7 +75,7 @@ class Ilator { /// Check if the ILA model contains unsupported patterns. bool SanityCheck() const; /// Generation bootstrap, e.g., creating directories. - bool Bootstrap(const std::string& root); + bool Bootstrap(const std::string& root, bool opt); /// Interpret instruction semantics (decode and state updates). bool GenerateInstrContent(const InstrPtr& instr, const std::string& dir); @@ -82,6 +83,8 @@ class Ilator { bool GenerateMemoryUpdate(const std::string& dir); /// Special handle for constant memory. bool GenerateConstantMemory(const std::string& dir); + /// Generate setup function for initial condition. + bool GenerateInitialSetup(const std::string& dir); /// Generate the instruction scheduler and driver. bool GenerateExecuteKernel(const std::string& dir); /// Generate the shared header files. @@ -91,7 +94,7 @@ class Ilator { /// Translate expression node to SystemC statements. bool RenderExpr(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut); - /// Translation routine entry point. + /// Translation routine for entrypoint. void DfsExpr(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut); /// Translation routine for variable. void DfsVar(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) const; diff --git a/include/ilang/util/container.h b/include/ilang/util/container.h index fe432f0a6..c4e33fcf1 100644 --- a/include/ilang/util/container.h +++ b/include/ilang/util/container.h @@ -64,11 +64,11 @@ template class KeyVec { /// Push back a data member. The name MUST NOT be registerd before. bool push_back(const Key& key, const T& data) { auto idx = vec_.size(); - auto res = map_.emplace(key, idx); - if (res.second) { + auto [it, status] = map_.try_emplace(key, idx); + if (status) { vec_.push_back(data); } - return res.second; + return status; } /// Get the data by index. diff --git a/include/ilang/verification/abs_knob.h b/include/ilang/verification/abs_knob.h deleted file mode 100644 index 5f2c50773..000000000 --- a/include/ilang/verification/abs_knob.h +++ /dev/null @@ -1,126 +0,0 @@ -/// \file -/// Header for a collection of ILA helpers. - -#ifndef ILANG_VERIFICATION_ABS_KNOB_H__ -#define ILANG_VERIFICATION_ABS_KNOB_H__ - -#include - -namespace ilang { - -class AbsKnob { -public: - /****************************************************************************/ - /// Add all dependent vars of the expr to the set. - static void InsertVar(const ExprPtr e, ExprSet& vars); - /// Get the set of all dependent vars of the expr. - static ExprSet GetVar(const ExprPtr e); - - /****************************************************************************/ - /// Add all state vars of the host (excluding child) to the set. - static void InsertStt(const InstrCnstPtr instrs, ExprSet& stts); - /// Add all state vars of the host (including child) to the set. - static void InsertSttTree(const InstrCnstPtr instrs, ExprSet& stts); - - /****************************************************************************/ - /// Add all vars of the ILA (excluding child) to the set. - static void InsertVar(const InstrLvlAbsCnstPtr m, ExprSet& vars); - /// Add all state vars of the ILA (excluding child) to the set. - static void InsertStt(const InstrLvlAbsCnstPtr m, ExprSet& stts); - /// Add all input vars of the ILA (excluding child) to the set. - static void InsertInp(const InstrLvlAbsCnstPtr m, ExprSet& inps); - /// Add all vars of the ILA (including child) to the set. - static void InsertVarTree(const InstrLvlAbsCnstPtr top, ExprSet& vars); - /// Add all state vars of the ILA (including child) to the set. - static void InsertSttTree(const InstrLvlAbsCnstPtr top, ExprSet& stts); - /// Add all input vars of the ILA (including child) to the set. - static void InsertInpTree(const InstrLvlAbsCnstPtr top, ExprSet& inps); - - /// Get the set of all vars of the ILA (excluding child). - static ExprSet GetVar(const InstrLvlAbsCnstPtr m); - /// Get the set of all state vars of the ILA (excluding child). - static ExprSet GetStt(const InstrLvlAbsCnstPtr m); - /// Get the set of all input vars of the ILA (excluding child). - static ExprSet GetInp(const InstrLvlAbsCnstPtr m); - /// Get the set of all vars of the ILA (including child). - static ExprSet GetVarTree(const InstrLvlAbsCnstPtr top); - /// Get the set of all state vars of the ILA (including child). - static ExprSet GetSttTree(const InstrLvlAbsCnstPtr top); - /// Get the set of all input vars of the ILA (including child). - static ExprSet GetInpTree(const InstrLvlAbsCnstPtr top); - - static void DuplInp(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst); - static void DuplStt(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst); - - /// Add all instructions of the ILA (excluding child) to the set. - static void InsertInstr(const InstrLvlAbsCnstPtr m, InstrVec& instrs); - /// Add all instructions of the ILA (including child) to the set. - static void InsertInstrTree(const InstrLvlAbsCnstPtr top, InstrVec& instrs); - - /// Get the set of instructions of the ILA (excluding child). - static InstrVec GetInstr(const InstrLvlAbsCnstPtr m); - /// Get the set of instructions of the ILA (including child). - static InstrVec GetInstrTree(const InstrLvlAbsCnstPtr top); - - /****************************************************************************/ - /// \brief Rewrite an expression by replacing based on the rule. - /// - If leaves contain non-var nodes, will replace with no further traverse. - static ExprPtr Rewrite(const ExprPtr e, const ExprMap& rule); - - /// \brief Rewrite an instruction by replacing based on the rule. - static void RewriteInstr(const InstrCnstPtr instr_src, - const InstrPtr instr_dst, const ExprMap& expr_map); - - /// \brief Flatten the given ILA, the initial conditions will be added to the - /// top the child instructions will also be added to the top, but their - /// (hierarchical) valid conditions will be added to their decode condition - /// Some usage hint: this function is intended to generate an ILA for Verilog - /// generator or other verification model generator. You can first use - /// ExtrDeptModl to extract the dependent model and use this to flatten the - /// that model and send to the generator - static void FlattenIla(const InstrLvlAbsPtr ila_ptr_); - - /// \brief Return a new ILA that contains the dependant instructions and - /// child-ILAs of an instruction (defined by sub-programs). - static InstrLvlAbsPtr ExtrDeptModl(const InstrPtr instr, - const std::string& name); - - /// Copy and ILA (including child). - static InstrLvlAbsPtr CopyIlaTree(const InstrLvlAbsCnstPtr src, - const std::string& dst_name); - - /****************************************************************************/ - /// Duplicate input vars from src to dst while updating the mapping. - static void DuplInp(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst, - ExprMap& expr_map); - /// Duplicate state vars from src to dst while updating the mapping. - static void DuplStt(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst, - ExprMap& expr_map); - /// Duplicate fetch from src to dst if defined (rewritten w.r.t. mapping). - static ExprPtr DuplFetch(const InstrLvlAbsCnstPtr src, - const InstrLvlAbsPtr dst, const ExprMap& expr_map); - /// Duplicate valid from src to dst if defined (rewritten w.r.t. mapping). - static ExprPtr DuplValid(const InstrLvlAbsCnstPtr src, - const InstrLvlAbsPtr dst, const ExprMap& expr_map); - /// Duplicate initial conditions from src to dst (rewritten w.r.t. mapping). - static void DuplInit(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst, - const ExprMap& expr_map); - /// Duplicate an instruction to dst (rewritten w.r.t. mapping). - static InstrPtr DuplInstr(const InstrCnstPtr instr_src, - const InstrLvlAbsPtr dst, const ExprMap& expr_map, - const CnstIlaMap& ila_map); - /// Duplicate instruction sequence to dst. NOT IMPLEMENTED YET. - static void DuplInstrSeq(const InstrLvlAbsCnstPtr src, - const InstrLvlAbsPtr dst); - -private: - /// Duplicate/create the input var in m. - static ExprPtr DuplInp(const InstrLvlAbsPtr m, const ExprPtr inp); - /// Duplicate/create the state var in m. - static ExprPtr DuplStt(const InstrLvlAbsPtr m, const ExprPtr stt); - -}; // class AbsKnob - -} // namespace ilang - -#endif // ILANG_VERIFICATION_ABS_KNOB_H__ diff --git a/include/ilang/verification/eq_check_crr.h b/include/ilang/verification/eq_check_crr.h deleted file mode 100644 index 40264651d..000000000 --- a/include/ilang/verification/eq_check_crr.h +++ /dev/null @@ -1,127 +0,0 @@ -/// \file -/// Header for generating verification condition for equivalence checking. - -#ifndef ILANG_VERIFICATION_EQ_CHECK_CRR_H__ -#define ILANG_VERIFICATION_EQ_CHECK_CRR_H__ - -#include "z3++.h" -#include -#include -#include - -/// \namespace ilang -namespace ilang { - -/// \brief Generator for commutating diagram-based equivalence checking. -class CommDiag { -public: - // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // - /// Default constructor. - CommDiag(z3::context& ctx, const CrrPtr crr); - /// Default destructor. - ~CommDiag(); - - // ------------------------- METHODS -------------------------------------- // - /// \brief Check equivalence between two models based on the refinement - /// relation up to the given unrolling bound. - /// \param[in] max unrolling bound. - bool EqCheck(const int& max = 10); - - /// \brief Incrementally checking equivalence between two models based on - /// the refinement relation up to the given unrolling bound. - /// \param[in] min #step of unrolling. - /// \param[in] max #step of unrolling. - bool IncEqCheck(const int& min = 0, const int& max = 10, const int& step = 1); - - bool IncCheck(const int& min = 0, const int& max = 10, const int& step = 1); - - typedef MonoUnroll Unroll; - -private: - // ------------------------- MEMBERS -------------------------------------- // - /// The underlying z3 context. - z3::context& ctx_; - /// The refinement relation. - CrrPtr crr_; - - // ------------------------- IncCheck ------------------------------------- // - - void Init(); - - enum UID { A_OLD, A_NEW, B_OLD, B_NEW }; - - struct UnrlUnit { - int lo = 0; - int hi = 0; - } uu_a_old_, uu_a_new_, uu_b_old_, uu_b_new_; - - Unroll unrl_a_old_ = Unroll(ctx_, k_suff_old_); - Unroll unrl_a_new_ = Unroll(ctx_, k_suff_new_); - Unroll unrl_b_old_ = Unroll(ctx_, k_suff_old_); - Unroll unrl_b_new_ = Unroll(ctx_, k_suff_new_); - - ExprSet stts_a_; - ExprSet stts_b_; - - Unroll& GetUnrl(const UID& uid); - Unroll& GetUnrlOld(); - Unroll& GetUnrlNew(); - Unroll& GetUnrlApl(); - - RefPtr GetRefine(const UID& uid); - UnrlUnit& GetUnrlUnit(const UID& uid); - const ExprSet& GetStts(const UID& uid); - - z3::expr GetZ3IncFlsh(const UID& uid); - z3::expr GetZ3IncCmpl(const UID& uid); - - // ------------------------- IncEqCheck ----------------------------------- // - static const std::string k_suff_old_; - static const std::string k_suff_new_; - static const std::string k_suff_apl_; - MonoUnroll unrl_old_ = MonoUnroll(ctx_, k_suff_old_); - MonoUnroll unrl_new_ = MonoUnroll(ctx_, k_suff_new_); - MonoUnroll unrl_apl_ = MonoUnroll(ctx_, k_suff_apl_); - - z3::expr GetZ3ApplInstr(const ExprSet& stts, const RefPtr ref); - z3::expr GetZ3Assm(); - z3::expr GetZ3Prop(); - z3::expr GetZ3Cmpl(const ExprPtr cmpl, MonoUnroll& un, const int& begin, - const int& end) const; - z3::expr GetZ3IncUnrl(MonoUnroll& un, const RefPtr ref, const int& begin, - const int& length, const ExprSet& stts) const; - bool CheckCmpl(z3::solver& s, z3::expr& cmpl_expr) const; - - // ------------------------- MonoCheck ------------------------------------ // - static const std::string k_suff_orig_; - static const std::string k_suff_appl_; - MonoUnroll unroll_appl_ = MonoUnroll(ctx_, k_suff_appl_); - MonoUnroll unroll_orig_ = MonoUnroll(ctx_, k_suff_orig_); - - bool SanityCheck(); - bool SanityCheckRefinement(const RefPtr ref); - bool SanityCheckRelation(const RelPtr rel, const InstrLvlAbsPtr ma, - const InstrLvlAbsPtr mb) const; - - int DetStepOrig(const RefPtr ref, const int& max); - int DetStepAppl(const RefPtr ref, const int& max); - bool CheckStepOrig(const RefPtr ref, const int& k); - bool CheckStepAppl(const RefPtr ref, const int& k); - - z3::expr GenInit(const RefPtr ref); - z3::expr GenTranRel(const RefPtr ref, const int& k_orig, const int& k_appl); - z3::expr GenAssm(); - z3::expr GenProp(); - - z3::expr AtLeastOnce(MonoUnroll& unroller, const ExprPtr cmpl, - const int& start, const int& end) const; - z3::expr AtMostOnce(MonoUnroll& unroller, const ExprPtr cmpl, - const int& start, const int& end) const; - z3::expr UnrollFlush(MonoUnroll& unroller, const RefPtr ref, const int& base, - const int& length, const int& start); - -}; // class CommDiag - -} // namespace ilang - -#endif // ILANG_VERIFICATION_EQ_CHECK_CRR_H__ diff --git a/include/ilang/verification/legacy_bmc.h b/include/ilang/verification/legacy_bmc.h deleted file mode 100644 index 0690099c5..000000000 --- a/include/ilang/verification/legacy_bmc.h +++ /dev/null @@ -1,82 +0,0 @@ -/// \file -/// Header for bounded model checking - -#ifndef ILANG_VERIFICATION_LEGACY_BMC_H__ -#define ILANG_VERIFICATION_LEGACY_BMC_H__ - -#include - -#include "z3++.h" -#include -#include -#include - -/// \namespace ilang -namespace ilang { - -/// \brief Simplified bounded model checking engine for ILAs. -class LegacyBmc { -public: - // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // - /// Default constructor. - LegacyBmc(); - /// Default destructor. - ~LegacyBmc(); - - // ------------------------- METHODS -------------------------------------- // - /// \brief Add initial condition to the solver. - void AddInit(ExprPtr init); - - /// \brief Add invariant to the solver. - void AddInvariant(ExprPtr inv); - - /// \brief Add property of one ILA. - void AddProperty(ExprPtr prop); - - /// \brief Legacy BMC where two ILAs are unrolled and compared monolithically. - z3::check_result Check(InstrLvlAbsPtr m0, const int& k0, InstrLvlAbsPtr m1, - const int& k1); - -private: - // ------------------------- MEMBERS -------------------------------------- // - /// z3 context. - z3::context ctx_; - /// Z3 expr generator. - Z3ExprAdapter gen_ = Z3ExprAdapter(ctx_); - - /// The set of invariants. - ExprPtrVec invs_; - /// The set of initial condition. - // - ExprPtrVec inits_; - - /// Automatically add default transition (unchanged) for un-specified states - /// if set to true. - bool def_tran_ = false; - - // ------------------------- HELPERS -------------------------------------- // - /// Unroll an ILA for k steps - /// \param[in] m pointer to the ILA to unroll. - /// \param[in] k number of steps to unroll. - /// \param[in] pos starting frame number (default 0). - /// \return the z3 expression representing the constraints. - z3::expr UnrollCmplIla(InstrLvlAbsPtr m, const int& k, const int& pos = 0); - - /// \brief Get the set of z3 expression (constraints) for the instruction. - /// - States with no update functions are encoded as unchanged. - z3::expr Instr(const InstrPtr instr, const std::string& suffix_prev, - const std::string& suffix_next, bool complete); - - /// \brief Get the set of z3 expression (constraints) for the ILA. - /// - Assume no child-ILAs (not considered). - /// - States with no update functions are encoded as unchanged. - /// - Assume one-hot encoding of all instructions. - z3::expr IlaOneHotFlat(const InstrLvlAbsPtr ila, - const std::string& suffix_prev, - const std::string& suffix_next); - -}; // class LegacyBmc - -} // namespace ilang - -#endif // ILANG_VERIFICATION_LEGACY_BMC_H__ diff --git a/include/ilang/verification/rewrite_expr.h b/include/ilang/verification/rewrite_expr.h deleted file mode 100644 index bc65d879b..000000000 --- a/include/ilang/verification/rewrite_expr.h +++ /dev/null @@ -1,43 +0,0 @@ -/// \file -/// Header for function object for rewriting Expr. - -#ifndef ILANG_VERIFICATION_REWRITE_EXPR_H__ -#define ILANG_VERIFICATION_REWRITE_EXPR_H__ - -#include -#include - -namespace ilang { - -/// \brief Function object for rewriting Expr. -class FuncObjRewrExpr { -public: - /// Constructor, initialize rewriting rule. - FuncObjRewrExpr(const ExprMap& rule) : rule_(rule) {} - - /// Return the rewritten result. - inline ExprPtr get(const ExprPtr e) const { - auto pos = rule_.find(e); - ILA_ASSERT(pos != rule_.end()) << e << " not found"; - return pos->second; - } - - /// Pre-process: return true (break) if the node has been visited. - bool pre(const ExprPtr e) const; - /// Post-process: update the rewriting rule map. - void post(const ExprPtr e); - -private: - /// Internal rewriting table. - ExprMap rule_; - - /// Rewrite all sorts of Expr. - ExprPtr Rewrite(const ExprPtr e) const; - /// Rewrite Operation sorted Expr. - ExprPtr RewriteOp(const ExprPtr e) const; - -}; // class FuncObjRewrExpr - -} // namespace ilang - -#endif // ILANG_VERIFICATION_REWRITE_EXPR_H__ diff --git a/include/ilang/verification/rewrite_ila.h b/include/ilang/verification/rewrite_ila.h deleted file mode 100644 index 1307bc157..000000000 --- a/include/ilang/verification/rewrite_ila.h +++ /dev/null @@ -1,75 +0,0 @@ -/// \file -/// Header for function object for rewriting ILA. - -#ifndef ILANG_VERIFICATION_REWRITE_ILA_H__ -#define ILANG_VERIFICATION_REWRITE_ILA_H__ - -#include - -namespace ilang { - -/// \brief Function object for rewriting ILA tree. -class FuncObjRewrIla { -public: - /// Type for storing ILA to ILA mapping. - typedef CnstIlaMap IlaMap; - - /// Constructor. - FuncObjRewrIla(const IlaMap& ila_map, const ExprMap& expr_map) - : ila_map_(ila_map), expr_map_(expr_map) {} - - /// Return the mapped ILA. - InstrLvlAbsPtr get(const InstrLvlAbsCnstPtr m) const; - - /// Pre-processing: create new ILA based on the given source. - bool pre(const InstrLvlAbsCnstPtr src); - /// Nothing. - void post(const InstrLvlAbsCnstPtr src) const; - -private: - /// ILA mapping. - IlaMap ila_map_; - /// Expr mapping. - ExprMap expr_map_; - -}; // FuncObjRewrIla - -/// \brief Function object for flatten ILA tree. -/// There is currently a problem: -/// this func obj calls duplInst -/// which in turn uses rewriteExpr -/// and rewriteExpr does not change the host of -/// of state variables, so the flatten expression -/// still has the host pointed to their original -/// ILA. This is fine for Verilog Gen, which only -/// depends on variable names to generate variables -/// but may not be good enough for other purpose. -class FuncObjFlatIla { -public: - /// Type for storing ILA to ILA mapping. - typedef CnstIlaMap IlaMap; - typedef std::stack ValidCondStack; - - /// Constructor. - FuncObjFlatIla(const InstrLvlAbsCnstPtr& top_, const IlaMap& ila_map, - const ExprMap& expr_map); - - /// Pre-processing: create new ILA based on the given source. - bool pre(const InstrLvlAbsCnstPtr src); - /// Nothing. - void post(const InstrLvlAbsCnstPtr src); - -private: - /// ILA mapping. - IlaMap ila_map_; - /// Expr mapping. - ExprMap expr_map_; - /// A stack to keep track of the hierarchical valid condition - ValidCondStack valid_cond_stack_; - /// Record which ila is the top level one - InstrLvlAbsCnstPtr top_ila_; -}; // FuncObjRewrIla - -} // namespace ilang - -#endif // ILANG_VERIFICATION_REWRITE_ILA_H__ diff --git a/include/ilang/verification/unroller.h b/include/ilang/verification/unroller.h deleted file mode 100644 index 95a8f0ddd..000000000 --- a/include/ilang/verification/unroller.h +++ /dev/null @@ -1,289 +0,0 @@ -/// \file -/// Header for unrolling ILA execution. - -#ifndef ILANG_VERIFICATION_UNROLLER_H__ -#define ILANG_VERIFICATION_UNROLLER_H__ - -#include -#include - -#include "z3++.h" -#include -#include - -/// \namespace ilang -namespace ilang { - -/// \brief Base class for unrolling ILA execution in different settings. -class Unroller { -public: - /// Type alias for z3::expr. - typedef z3::expr ZExpr; - /// Type for containing a set of z3::expr. - typedef z3::expr_vector ZExprVec; - /// Type alias for a set of ExprPtr. - typedef ExprPtrVec IExprVec; - - // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // - /// Default constructor - Unroller(z3::context& ctx, const std::string& suffix); - /// Default virtual destructor. - virtual ~Unroller(); - - // ------------------------- METHODS -------------------------------------- // - /// Add a predicate that should be asserted globally. - void AddGlobPred(const ExprPtr p); - /// Add a predicate that should be asserted in the initial condition. - void AddInitPred(const ExprPtr p); - /// Add a predicate that should be asserted at the k-th step. - void AddStepPred(const ExprPtr p, const int& k); - /// Clear the global predicates. - void ClearGlobPred(); - /// Clear the initial predicates. - void ClearInitPred(); - /// Clear the step-specific predicates. - void ClearStepPred(); - /// Clear all predicates. - void ClearPred(); - - // ------------------------- HELPERS -------------------------------------- // - /// Return the z3::expr representing the current state at the time. - ZExpr CurrState(const ExprPtr v, const int& t); - /// Return the z3::expr representing the next state at the time. - ZExpr NextState(const ExprPtr v, const int& t); - /// Return the z3::expr representing the current-based Expr at the time. - ZExpr GetZ3Expr(const ExprPtr e, const int& t); - /// Return the z3::expr representing a unique Expr (regardless of time). - ZExpr GetZ3Expr(const ExprPtr e); - /// Return the z3::expr representing a and b are equal at their time. - ZExpr Equal(const ExprPtr va, const int& ta, const ExprPtr vb, const int& tb); - -protected: - // ------------------------- MEMBERS -------------------------------------- // - /// The set of dependant state variables. - IExprVec vars_; - /// The set of predicates to be asserted of each step. - IExprVec k_pred_; - /// The set of state update functions of each step. - IExprVec k_next_; - - // ------------------------- METHODS -------------------------------------- // - /// \brief [Application-specific] Define dependant state variables. - /// - "vars_" should be assigned with the state vars uniquely. - /// - "vars_" will be cleared before caling this function. - /// = The var order stored in "vars_" will be the globally agree-upon order. - virtual void DefineDepVar() = 0; - - /// \brief [Application-specific] Define next state update functions. - /// - "k_next_" should be assigned with the next state expression. - /// - "k_next_" follows the global order as stored in "vars_". - /// - "k_next_" will NOT be cleared before calling (is the only modifier). - /// - "k_pred_" can be used to store step-specific predicates, e.g. decode. - /// - "k_pred_" will NOT be cleared before calling (is the only modifier). - virtual void Transition(const int& idx) = 0; - - /// Unroll while substituting internal expression. - ZExpr UnrollSubs(const size_t& len, const int& pos); - /// Unroll without substituting internal expression. - ZExpr UnrollAssn(const size_t& len, const int& pos, bool cache = false); - /// Unroll without asserting state equality between each step. - ZExpr UnrollNone(const size_t& len, const int& pos); - - // ------------------------- HELPERS -------------------------------------- // - /// Return the state update function (unchanged if not defined). - static ExprPtr StateUpdCmpl(const InstrPtr instr, const ExprPtr var); - /// Return the decode function (true if not defined). - static ExprPtr DecodeCmpl(const InstrPtr instr); - - /// Create a new free variable (with same sort) under the same host. - static ExprPtr NewFreeVar(const ExprPtr var, const std::string& name); - -private: - // ------------------------- MEMBERS -------------------------------------- // - /// z3::context of the unroller. - z3::context& ctx_; - /// z3 expression generator. - Z3ExprAdapter gen_; - - /// Extra suffix for customized applications. - std::string extra_suff_ = ""; - - /// The set of global predicates. - IExprVec g_pred_; - /// The set of initial predicates. - IExprVec i_pred_; - /// The mapping of (external) step-specific predicates. - std::map s_pred_; - - /// The set of z3::expr representing the latest states of previous steps. - ZExprVec k_prev_z3_; - /// The set of z3::expr representing the current states. - ZExprVec k_curr_z3_; - /// The set of z3::expr representing the next states. - ZExprVec k_next_z3_; - - /// The set of constraints that should be asserted. - ZExprVec cstr_; - - // ------------------------- ACCESSORS/MUTATORS --------------------------- // - /// Return the underlying z3::context. - inline z3::context& ctx() const { return ctx_; } - /// Return the z3::expr generator. - inline Z3ExprAdapter& gen() { return gen_; } - - // ------------------------- HELPERS -------------------------------------- // - /// \brief Boot-strapping information needed for unrolling. - /// - collect dependant state variables - /// - prepare rewriting table - void BootStrap(const int& pos, bool cache = false); - - /// Assert equal between the z3::expr and the Expr w.r.t the suffix. - void AssertEqual(const ZExprVec& z, const IExprVec& e, - const std::string& suffix); - - /// Clear the z3::epxr container. - inline void Clear(ZExprVec& z3_vec); - - /// Generate and append the z3::expr for the set of Expr w.r.t. the suffix. - void IExprToZExpr(const IExprVec& i_expr_src, const std::string& suffix, - ZExprVec& z_expr_dst); - /// \brief Generate and append the z3::expr for the set of Expr w.r.t. the - /// suffix while substituting internal expressions. - void IExprToZExpr(const IExprVec& i_expr_src, const std::string& suffix, - ZExprVec& z_expr_dst, const ZExprVec& subs_src, - const ZExprVec& subs_dst); - - /// Wrapper for assigning (copying) z3::expr_vector from src to dst. - void CopyZExprVec(const ZExprVec& src, ZExprVec& dst); - - /// Conjunct (AND) all the predicates in the set. - ZExpr ConjPred(const ZExprVec& vec) const; - - /// Suffix generator for current state expressions of each step. - inline std::string SuffCurr(const int& t) const { - return std::to_string(t) + "_" + extra_suff_; - } - /// Suffix generator for next state symbol of each step. - inline std::string SuffNext(const int& t) const { - return std::to_string(t) + "_" + extra_suff_ + ".nxt"; - } - -}; // class Unroller - -/// \brief Application class for unrolling a path of instruction sequence. -class PathUnroll : public Unroller { -public: - /// Type of a list of instruction sequence. - typedef std::vector InstrVec; - - // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // - /// Default constructor. - PathUnroll(z3::context& ctx, const std::string& suff = ""); - /// Default destructor. - ~PathUnroll(); - - // ------------------------- METHODS -------------------------------------- // - /// \brief Unroll a sequence of instructions with internal states substituted. - /// \param[in] seq the sequence of instructions. - /// \param[in] pos the starting time frame. - ZExpr PathSubs(const std::vector& seq, const int& pos = 0); - - /// \brief Unroll a sequence of instructions while asserting states are equal - /// between each step. - /// \param[in] seq the sequence of instructions. - /// \param[in] pos the starting time frame. - ZExpr PathAssn(const std::vector& seq, const int& pos = 0); - - /// \brief Unroll a sequence of instructions without asserting states - /// relations between steps. "N(var_i) == var_i.nxt_suff" - /// \param[in] seq the sequence of instructions. - /// \param[in] pos the starting time frame. - ZExpr PathNone(const std::vector& seq, const int& pos = 0); - -protected: - // ------------------------- METHODS -------------------------------------- // - /// \brief [Application-specific] Define dependant state variables. - /// - "vars_" should be assigned with the state vars uniquely. - /// - "vars_" will be cleared before caling this function. - /// = The var order stored in "vars_" will be the globally agree-upon order. - void DefineDepVar(); - - /// \brief [Application-specific] Define next state update functions. - /// - "k_next_" should be assigned with the next state expression. - /// - "k_next_" follows the global order as stored in "vars_". - /// - "k_next_" will NOT be cleared before calling (is the only modifier). - /// - "k_pred_" can be used to store step-specific predicates, e.g. decode. - /// - "k_pred_" will NOT be cleared before calling (is the only modifier). - void Transition(const int& idx); - -private: - // ------------------------- MEMBERS -------------------------------------- // - /// The sequence of instructions. - InstrVec seq_; -}; // class PathUnroll - -/// \brief Application class for unrolling the ILA as a monolithic transition -/// system. -class MonoUnroll : public Unroller { -public: - // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- // - /// Default constructor. - MonoUnroll(z3::context& ctx, const std::string& suff = ""); - /// Default destructor. - ~MonoUnroll(); - - // ------------------------- METHODS -------------------------------------- // - /// \brief Unroll the ILA with internal states substituted. - /// \param[in] top the top-level ILA. - /// \param[in] length number of steps to unroll. - /// \param[in] pos the starting time frame. - ZExpr MonoSubs(const InstrLvlAbsPtr top, const int& length, - const int& pos = 0); - - /// \brief Unroll the ILA while asserting states are equal between each step. - /// \param[in] top the top-level ILA. - /// \param[in] length number of steps to unroll. - /// \param[in] pos the starting time frame. - ZExpr MonoAssn(const InstrLvlAbsPtr top, const int& length, - const int& pos = 0); - - /// \brief Unroll the ILA without asserting states relations between steps. - /// \param[in] top the top-level ILA. - /// \param[in] length number of steps to unroll. - /// \param[in] pos the starting time frame. - ZExpr MonoNone(const InstrLvlAbsPtr top, const int& length, - const int& pos = 0); - - /// \brief Incrementally unrolling the ILA using MonoAssn (with transition - /// relation being cached). - /// \param[in] top the top-level ILA. - /// \param[in] length number of steps to unroll. - /// \param[in] pos the starting time frame. - ZExpr MonoIncr(const InstrLvlAbsPtr top, const int& length, const int& pos); - -protected: - // ------------------------- METHODS -------------------------------------- // - /// \brief [Application-specific] Define dependant state variables. - /// - "vars_" should be assigned with the state vars uniquely. - /// - "vars_" will be cleared before caling this function. - /// - The var order stored in "vars_" will be the globally agree-upon order. - void DefineDepVar(); - - /// \brief [Application-specific] Define next state update functions. - /// - "k_next_" should be assigned with the next state expression. - /// - "k_next_" follows the global order as stored in "vars_". - /// - "k_next_" will NOT be cleared before calling (is the only modifier). - /// - "k_pred_" can be used to store step-specific predicates, e.g. decode. - /// - "k_pred_" will NOT be cleared before calling (is the only modifier). - void Transition(const int& idx); - -private: - // ------------------------- MEMBERS -------------------------------------- // - /// The sequence of instructions. - InstrLvlAbsPtr top_; - -}; // class MonoUnroll - -} // namespace ilang - -#endif // ILANG_VERIFICATION_UNROLLER_H__ diff --git a/scripts/travis/install-externs.sh b/scripts/travis/install-externs.sh index 6922f7c21..028776c4e 100644 --- a/scripts/travis/install-externs.sh +++ b/scripts/travis/install-externs.sh @@ -47,12 +47,6 @@ cd $CI_BUILD_DIR/extern/vlog-parser/build cmake .. -DCMAKE_INSTALL_PREFIX=$CI_BUILD_DIR/local cmake --build . --target install -# tmpl-synth -mkdir -p $CI_BUILD_DIR/extern/tmpl-synth/build -cd $CI_BUILD_DIR/extern/tmpl-synth/build -cmake .. -DCMAKE_INSTALL_PREFIX=$CI_BUILD_DIR/local -cmake --build . --target install - # smt-switch with Boolector cd $CI_BUILD_DIR/extern/smt-switch source contrib/setup-btor.sh diff --git a/src/ila-mngr/CMakeLists.txt b/src/ila-mngr/CMakeLists.txt index 013bd7ba6..957ffae4e 100644 --- a/src/ila-mngr/CMakeLists.txt +++ b/src/ila-mngr/CMakeLists.txt @@ -7,7 +7,8 @@ target_sources(${ILANG_LIB_NAME} PRIVATE ${CMAKE_CURRENT_SOURCE_DIR}/p_rewrite_conditional_store.cc ${CMAKE_CURRENT_SOURCE_DIR}/p_rewrite_generic.cc ${CMAKE_CURRENT_SOURCE_DIR}/p_rewrite_store_load.cc - ${CMAKE_CURRENT_SOURCE_DIR}/p_simplify_instr_update.cc + ${CMAKE_CURRENT_SOURCE_DIR}/p_simplify_semantic.cc + ${CMAKE_CURRENT_SOURCE_DIR}/p_simplify_syntactic.cc ${CMAKE_CURRENT_SOURCE_DIR}/u_abs_knob.cc ${CMAKE_CURRENT_SOURCE_DIR}/u_rewrite_expr.cc ${CMAKE_CURRENT_SOURCE_DIR}/u_rewrite_ila.cc diff --git a/src/ila-mngr/p_infer_child_prog_cfg.cc b/src/ila-mngr/p_infer_child_prog_cfg.cc index 556bbc326..caab1c596 100644 --- a/src/ila-mngr/p_infer_child_prog_cfg.cc +++ b/src/ila-mngr/p_infer_child_prog_cfg.cc @@ -8,8 +8,11 @@ namespace ilang { -bool PassInferChildProgCFG(const InstrLvlAbsPtr& m) { +namespace pass { + +bool InferChildProgCFG(const InstrLvlAbsPtr& m) { ILA_NOT_NULL(m); + ILA_INFO << "Start pass: infer child program control-flow"; // iterate through child-ILAs for (size_t i = 0; i < m->child_num(); i++) { @@ -51,10 +54,12 @@ bool PassInferChildProgCFG(const InstrLvlAbsPtr& m) { ILA_WARN_IF(!child->instr_seq()) << "Fail to infer CFG for " << child; // traverse the hierarchy - PassInferChildProgCFG(child); + InferChildProgCFG(child); } return true; } -}; // namespace ilang +} // namespace pass + +} // namespace ilang diff --git a/src/ila-mngr/p_map_child_prog_entry.cc b/src/ila-mngr/p_map_child_prog_entry.cc index c4b47e87b..6a6640a28 100644 --- a/src/ila-mngr/p_map_child_prog_entry.cc +++ b/src/ila-mngr/p_map_child_prog_entry.cc @@ -8,8 +8,11 @@ namespace ilang { -bool PassMapChildProgEntryPoint(const InstrLvlAbsPtr& m) { +namespace pass { + +bool MapChildProgEntryPoint(const InstrLvlAbsPtr& m) { ILA_NOT_NULL(m); + ILA_INFO << "Start pass: mapping child program entry"; // check if a can trigger b auto CheckCausality = [=](InstrPtr a, InstrPtr b) { @@ -93,4 +96,6 @@ bool PassMapChildProgEntryPoint(const InstrLvlAbsPtr& m) { return true; } -}; // namespace ilang +} // namespace pass + +} // namespace ilang diff --git a/src/ila-mngr/p_rewrite_conditional_store.cc b/src/ila-mngr/p_rewrite_conditional_store.cc index 118341923..e6101597a 100644 --- a/src/ila-mngr/p_rewrite_conditional_store.cc +++ b/src/ila-mngr/p_rewrite_conditional_store.cc @@ -10,6 +10,8 @@ namespace ilang { +namespace pass { + class FuncObjRewrCondStore : public FuncObjRewrExpr { public: FuncObjRewrCondStore() : FuncObjRewrExpr({}) {} @@ -107,8 +109,9 @@ class FuncObjRewrCondStore : public FuncObjRewrExpr { }; // class FuncObjRewrCondStore -bool PassRewriteConditionalStore(const InstrLvlAbsPtr& m) { +bool RewriteConditionalStore(const InstrLvlAbsPtr& m) { ILA_NOT_NULL(m); + ILA_INFO << "Start pass: rewrite conditional store"; auto func = FuncObjRewrCondStore(); auto Rewr = [=, &func](const ExprPtr e) { @@ -119,7 +122,9 @@ bool PassRewriteConditionalStore(const InstrLvlAbsPtr& m) { return e; }; - return PassRewriteGeneric(m, Rewr); + return RewriteGeneric(m, Rewr); } -}; // namespace ilang +} // namespace pass + +} // namespace ilang diff --git a/src/ila-mngr/p_rewrite_generic.cc b/src/ila-mngr/p_rewrite_generic.cc index f7495c4a2..056887c9a 100644 --- a/src/ila-mngr/p_rewrite_generic.cc +++ b/src/ila-mngr/p_rewrite_generic.cc @@ -7,20 +7,20 @@ namespace ilang { -bool PassRewriteGeneric(const InstrLvlAbsPtr& m, - std::function Rewr) { +namespace pass { + +bool RewriteGeneric(const InstrLvlAbsPtr& m, + std::function Rewr) { ILA_NOT_NULL(m); // rewrite valid - auto new_valid = Rewr(m->valid()); - if (new_valid) { - m->ForceSetValid(new_valid); + if (m->valid()) { + m->ForceSetValid(Rewr(m->valid())); } // rewrite fetch - auto new_fetch = Rewr(m->fetch()); - if (new_fetch) { - m->ForceSetFetch(new_fetch); + if (m->fetch()) { + m->ForceSetFetch(Rewr(m->fetch())); } // TODO rewrite init @@ -30,26 +30,23 @@ bool PassRewriteGeneric(const InstrLvlAbsPtr& m, auto instr = m->instr(i); // rewrite decode - auto new_decode = Rewr(instr->decode()); - if (new_decode) { - instr->ForceSetDecode(new_decode); - } + ILA_NOT_NULL(instr->decode()); + instr->ForceSetDecode(Rewr(instr->decode())); // rewrite updates - for (size_t s = 0; s < m->state_num(); s++) { - auto new_update = Rewr(instr->update(m->state(s))); - if (new_update) { - instr->ForceAddUpdate(m->state(s)->name().str(), new_update); - } + for (const auto& state : instr->updated_states()) { + instr->ForceAddUpdate(state, Rewr(instr->update(state))); } } // traverse the ILA hierarchy for (size_t c = 0; c < m->child_num(); c++) { - PassRewriteGeneric(m->child(c), Rewr); + RewriteGeneric(m->child(c), Rewr); } return true; } -}; // namespace ilang +} // namespace pass + +} // namespace ilang diff --git a/src/ila-mngr/p_rewrite_store_load.cc b/src/ila-mngr/p_rewrite_store_load.cc index 6609a82ab..d5865557f 100644 --- a/src/ila-mngr/p_rewrite_store_load.cc +++ b/src/ila-mngr/p_rewrite_store_load.cc @@ -9,31 +9,7 @@ namespace ilang { -#if 0 -class FuncObjStoreStore { -public: - inline const ExprPtrVec& addr() const { return addr_; } - inline const ExprPtrVec& data() const { return data_; } - - bool pre(const ExprPtr e) { - // ILA_ASSERT(GetUidExprOp(e) == AST_UID_EXPR_OP::LOAD); - // can be load from store/var/const/ite - - addr_.push_back(e->arg(1)); - data_.push_back(e->arg(2)); - - // return true if is store to store - return e->arg(0)->is_op(); - } - - void post(const ExprPtr e) {} - -private: - ExprPtrVec addr_; - ExprPtrVec data_; - -}; // class FuncObjStoreStore -#endif +namespace pass { class FuncObjRewrStoreLoad : public FuncObjRewrExpr { public: @@ -97,8 +73,9 @@ class FuncObjRewrStoreLoad : public FuncObjRewrExpr { }; // class FuncObjRewrStoreLoad -bool PassRewriteStoreLoad(const InstrLvlAbsPtr& m) { +bool RewriteStoreLoad(const InstrLvlAbsPtr& m) { ILA_NOT_NULL(m); + ILA_INFO << "Start pass: rewrite store-load pattern"; auto func = FuncObjRewrStoreLoad(); auto Rewr = [=, &func](const ExprPtr e) { @@ -109,7 +86,9 @@ bool PassRewriteStoreLoad(const InstrLvlAbsPtr& m) { return e; }; - return PassRewriteGeneric(m, Rewr); + return RewriteGeneric(m, Rewr); } -}; // namespace ilang +} // namespace pass + +} // namespace ilang diff --git a/src/ila-mngr/p_simplify_instr_update.cc b/src/ila-mngr/p_simplify_semantic.cc similarity index 69% rename from src/ila-mngr/p_simplify_instr_update.cc rename to src/ila-mngr/p_simplify_semantic.cc index e0f1504cd..7f07a5715 100644 --- a/src/ila-mngr/p_simplify_instr_update.cc +++ b/src/ila-mngr/p_simplify_semantic.cc @@ -8,29 +8,7 @@ namespace ilang { -bool SimplifyInstrUpdateTemplate( - const InstrLvlAbsPtr& m, - std::function Simp) { - ILA_NOT_NULL(m); - - // for each instruction - for (size_t i = 0; i < m->instr_num(); i++) { - // for each state - for (size_t s = 0; s < m->state_num(); s++) { - auto state_var = m->state(s); - auto new_update = Simp(m->instr(i)->update(state_var), m->instr(i)); - if (new_update) { - m->instr(i)->ForceAddUpdate(state_var->name().str(), new_update); - } - } - } - - for (size_t c = 0; c < m->child_num(); c++) { - SimplifyInstrUpdateTemplate(m->child(c), Simp); - } - - return true; -} +namespace pass { class FuncObjEqSubtree { public: @@ -50,7 +28,7 @@ class FuncObjEqSubtree { void post(const ExprPtr e) { auto dst = Rewrite(e); - rule_.insert({e, dst}).second; + rule_.insert({e, dst}); } private: @@ -92,8 +70,9 @@ class FuncObjEqSubtree { }; // class FuncObjSimpInstrUpdateRedundant -bool PassSimplifyInstrUpdate(const InstrLvlAbsPtr& m, const int& timeout) { +bool SimplifySemantic(const InstrLvlAbsCnstPtr& m, const int& timeout) { ILA_NOT_NULL(m); + ILA_INFO << "Start pass: semantic simplification"; // pattern - equivalent sub-tree modulo valid and decode auto SimpEqSubtree = [=](const ExprPtr e, const InstrPtr i) { @@ -111,7 +90,7 @@ bool PassSimplifyInstrUpdate(const InstrLvlAbsPtr& m, const int& timeout) { auto new_update = func.get(e); if (new_update != e) { - ILA_DLOG("PassSimpInstrUpdate") << "Equivalent sub-tree of " << i; + ILA_DLOG("PassSimpSemantic") << "Equivalent sub-tree of " << i; } return new_update; }; @@ -119,10 +98,33 @@ bool PassSimplifyInstrUpdate(const InstrLvlAbsPtr& m, const int& timeout) { if (timeout > 0) { z3::set_param("timeout", timeout); } - auto res = SimplifyInstrUpdateTemplate(m, SimpEqSubtree); + + auto visiter = [&SimpEqSubtree](const InstrLvlAbsCnstPtr& current) { + try { + // only simplify instructions + for (size_t i = 0; i < current->instr_num(); i++) { + auto instr = current->instr(i); + // decode + ILA_NOT_NULL(instr->decode()); + instr->ForceSetDecode(SimpEqSubtree(instr->decode(), instr)); + // state updates + for (const auto& state : instr->updated_states()) { + instr->ForceAddUpdate(state, + SimpEqSubtree(instr->update(state), instr)); + } + } + } catch (...) { + ILA_ERROR << "Fail simplify " << current; + } + }; + + m->DepthFirstVisit(visiter); + z3::reset_params(); - return res; + return true; } -}; // namespace ilang +} // namespace pass + +} // namespace ilang diff --git a/src/ila-mngr/p_simplify_syntactic.cc b/src/ila-mngr/p_simplify_syntactic.cc new file mode 100644 index 000000000..b4f8d5ea5 --- /dev/null +++ b/src/ila-mngr/p_simplify_syntactic.cc @@ -0,0 +1,28 @@ +/// \file +/// Simplify Expr node syntactically (structurally). + +#include + +#include +#include + +namespace ilang { + +namespace pass { + +bool SimplifySyntactic(const InstrLvlAbsPtr& m) { + ILA_NOT_NULL(m); + ILA_INFO << "Start pass: syntactic simplification"; + + auto mngr = ExprMngr::New(); + auto Rewr = [&mngr](const ExprPtr& expr) { return mngr->GetRep(expr); }; + try { + return RewriteGeneric(m, Rewr); + } catch (...) { + return false; + } +} + +} // namespace pass + +} // namespace ilang diff --git a/src/ila-mngr/u_abs_knob.cc b/src/ila-mngr/u_abs_knob.cc index 432f4b0eb..d64cbaabb 100644 --- a/src/ila-mngr/u_abs_knob.cc +++ b/src/ila-mngr/u_abs_knob.cc @@ -217,36 +217,33 @@ void RewriteInstr(const InstrCnstPtr src, const InstrPtr dst, 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 = Rewrite(update_src, expr_map); - dst->set_update(state_name, update_dst); - } + for (const auto& state : src->updated_states()) { + auto update_src = src->update(state); + auto update_dst = Rewrite(update_src, expr_map); + dst->set_update(state, update_dst); } } // this function will change the input ! You can copy it first. void FlattenIla(const InstrLvlAbsPtr ila_ptr_) { ILA_NOT_NULL(ila_ptr_); + ILA_INFO << "Flatten " << 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); + auto recordInpStates = [&](const InstrLvlAbsCnstPtr& a) { + 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_map_.insert({a, ila_ptr_}); + // remember to change the decode !!! to factor in the valid state + }; ila_ptr_->DepthFirstVisit(recordInpStates); @@ -316,34 +313,26 @@ InstrLvlAbsPtr CopyIlaTree(const InstrLvlAbsCnstPtr src, /******************************************************************************/ void DuplInp(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst, ExprMap& expr_map) { - auto inps = GetInp(src); - for (auto it = inps.begin(); it != inps.end(); it++) { + for (const auto& inp_src : GetInp(src)) { // 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}); - } + expr_map.try_emplace(inp_src, inp_dst); } } void DuplStt(const InstrLvlAbsCnstPtr src, const InstrLvlAbsPtr dst, ExprMap& expr_map) { - auto stts = GetStt(src); - for (auto it = stts.begin(); it != stts.end(); it++) { - auto stt_src = *it; + for (const auto& stt_src : GetStt(src)) { 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}); - } + expr_map.try_emplace(stt_src, stt_dst); } } diff --git a/src/ila-mngr/u_rewrite_expr.cc b/src/ila-mngr/u_rewrite_expr.cc index f9e19626e..bdfcb34d5 100644 --- a/src/ila-mngr/u_rewrite_expr.cc +++ b/src/ila-mngr/u_rewrite_expr.cc @@ -11,26 +11,26 @@ namespace ilang { using namespace ExprFuse; -ExprPtr FuncObjRewrExpr::get(const ExprPtr e) const { +ExprPtr FuncObjRewrExpr::get(const ExprPtr& e) const { auto pos = rule_.find(e); ILA_CHECK(pos != rule_.end()) << e << " not found"; return pos->second; } -bool FuncObjRewrExpr::pre(const ExprPtr e) const { +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) { +void FuncObjRewrExpr::post(const ExprPtr& e) { auto dst = Rewrite(e); - auto ok = rule_.insert({e, dst}).second; + auto [it, ok] = rule_.emplace(e, dst); // 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 { +ExprPtr FuncObjRewrExpr::Rewrite(const ExprPtr& e) const { if (e->is_var() || e->is_const()) { return e; } else { @@ -39,11 +39,8 @@ ExprPtr FuncObjRewrExpr::Rewrite(const ExprPtr e) const { } } -ExprPtr FuncObjRewrExpr::RewriteOp(const ExprPtr e) const { - // check each type of op - auto expr_op_uid = GetUidExprOp(e); - - switch (expr_op_uid) { +ExprPtr FuncObjRewrExpr::RewriteOp(const ExprPtr& e) const { + switch (auto expr_op_uid = GetUidExprOp(e); expr_op_uid) { case AST_UID_EXPR_OP::NEG: { auto a = get(e->arg(0)); return Negate(a); diff --git a/src/ila-mngr/u_rewrite_ila.cc b/src/ila-mngr/u_rewrite_ila.cc index 82587d77e..6afbb9352 100644 --- a/src/ila-mngr/u_rewrite_ila.cc +++ b/src/ila-mngr/u_rewrite_ila.cc @@ -12,13 +12,13 @@ namespace ilang { -InstrLvlAbsPtr FuncObjRewrIla::get(const InstrLvlAbsCnstPtr m) const { +InstrLvlAbsPtr FuncObjRewrIla::get(const InstrLvlAbsCnstPtr& m) const { auto pos = ila_map_.find(m); ILA_CHECK(pos != ila_map_.end()) << m << " not found"; return pos->second; } -bool FuncObjRewrIla::pre(const InstrLvlAbsCnstPtr src) { +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; @@ -58,7 +58,7 @@ bool FuncObjRewrIla::pre(const InstrLvlAbsCnstPtr src) { return false; } -void FuncObjRewrIla::post(const InstrLvlAbsCnstPtr src) const { +void FuncObjRewrIla::post(const InstrLvlAbsCnstPtr& src) const { // nothing } @@ -71,7 +71,7 @@ FuncObjFlatIla::FuncObjFlatIla(const InstrLvlAbsCnstPtr& top_, #endif // VALID_STACK } -bool FuncObjFlatIla::pre(const InstrLvlAbsCnstPtr src) { +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); @@ -105,7 +105,7 @@ bool FuncObjFlatIla::pre(const InstrLvlAbsCnstPtr src) { return false; } -void FuncObjFlatIla::post(const InstrLvlAbsCnstPtr src) { +void FuncObjFlatIla::post(const InstrLvlAbsCnstPtr& src) { // pop the stack #ifdef VALID_STACK valid_cond_stack_.pop(); diff --git a/src/ila-mngr/u_smt_switch.cc b/src/ila-mngr/u_smt_switch.cc index 9d35c3f0d..52fc464af 100644 --- a/src/ila-mngr/u_smt_switch.cc +++ b/src/ila-mngr/u_smt_switch.cc @@ -72,33 +72,27 @@ void SmtSwitchItf::PopulateExprMap(const ExprPtr expr) { } // get the Term based on its ast node type + auto Expr2Term = [this](const ExprPtr& e, const smt::TermVec& args) { + switch (auto uid = GetUidExpr(e); uid) { + case AST_UID_EXPR::VAR: { + return ExprVar2Term(e); + } + case AST_UID_EXPR::CONST: { + return ExprConst2Term(e); + } + default: { + ILA_ASSERT(uid == AST_UID_EXPR::OP); + return ExprOp2Term(e, args); + } + }; // switch uid + }; + auto res = Expr2Term(expr, arg_terms); // update the Term cache expr_map_.insert({expr, res}); } -smt::Term SmtSwitchItf::Expr2Term(const ExprPtr expr, - const smt::TermVec& arg_terms) { - auto expr_uid = GetUidExpr(expr); - - switch (expr_uid) { - case AST_UID_EXPR::VAR: { - return ExprVar2Term(expr); - } - case AST_UID_EXPR::CONST: { - return ExprConst2Term(expr); - } - case AST_UID_EXPR::OP: { - return ExprOp2Term(expr, arg_terms); - } - default: { - ILA_CHECK(false) << fmt::format("Unknown type {} for ", expr_uid) << expr; - return solver_->make_term(true); - } - }; // switch expr_uid -} - smt::Term SmtSwitchItf::ExprVar2Term(const ExprPtr expr) { // for z3 compatibility auto prefix = (expr->host()) ? expr->host()->GetRootName() : ""; @@ -110,9 +104,8 @@ smt::Term SmtSwitchItf::ExprVar2Term(const ExprPtr expr) { smt::Term SmtSwitchItf::ExprConst2Term(const ExprPtr expr) { auto expr_const = std::static_pointer_cast(expr); - auto sort_uid = GetUidSort(expr->sort()); - switch (sort_uid) { + switch (auto sort_uid = GetUidSort(expr->sort()); sort_uid) { case AST_UID_SORT::BOOL: { return solver_->make_term(expr_const->val_bool()->val()); } @@ -121,7 +114,8 @@ smt::Term SmtSwitchItf::ExprConst2Term(const ExprPtr expr) { return solver_->make_term(expr_const->val_bv()->val(), solver_->make_sort(smt::BV, bw)); } - case AST_UID_SORT::MEM: { + default: { + ILA_ASSERT(sort_uid == AST_UID_SORT::MEM); auto addr_sort = solver_->make_sort(smt::BV, expr->sort()->addr_width()); auto data_sort = solver_->make_sort(smt::BV, expr->sort()->data_width()); auto mem_sort = solver_->make_sort(smt::ARRAY, addr_sort, data_sort); @@ -143,10 +137,6 @@ smt::Term SmtSwitchItf::ExprConst2Term(const ExprPtr expr) { return const_memory; } - default: { - ILA_CHECK(false) << fmt::format("Unknown sort {} for ", sort_uid) << expr; - return solver_->make_term(true); - } }; // switch sort_uid } @@ -156,9 +146,8 @@ smt::Term SmtSwitchItf::ExprOp2Term(const ExprPtr expr, // XXX Boolector (maybe also others) doesn't accept INT sort for param. // auto param_sort = solver_->make_sort(smt::INT); auto param_sort = solver_->make_sort(smt::BV, PARAM_BIT_WIDTH); - auto expr_op_uid = GetUidExprOp(expr); - switch (expr_op_uid) { + switch (auto expr_op_uid = GetUidExprOp(expr); expr_op_uid) { case AST_UID_EXPR_OP::NEG: { ILA_WARN << "Negate not fully supported in smt-switch."; return solver_->make_term(smt::PrimOp::Negate, arg_terms.at(0)); @@ -327,8 +316,8 @@ smt::Term SmtSwitchItf::ExprOp2Term(const ExprPtr expr, } // apply func - for (size_t i = 0; i != arg_terms.size(); i++) { - func_arg_terms.push_back(arg_terms.at(i)); + for (auto arg_i : arg_terms) { + func_arg_terms.push_back(arg_i); } return solver_->make_term(smt::PrimOp::Apply, func_arg_terms); } @@ -340,24 +329,20 @@ smt::Term SmtSwitchItf::ExprOp2Term(const ExprPtr expr, } smt::Sort SmtSwitchItf::IlaSort2SmtSort(const SortPtr s) { - auto sort_uid = GetUidSort(s); - switch (sort_uid) { + switch (auto sort_uid = GetUidSort(s); sort_uid) { case AST_UID_SORT::BOOL: { return solver_->make_sort(smt::BOOL); } case AST_UID_SORT::BV: { return solver_->make_sort(smt::BV, s->bit_width()); } - case AST_UID_SORT::MEM: { + default: { + ILA_ASSERT(sort_uid == AST_UID_SORT::MEM); return solver_->make_sort(smt::ARRAY, solver_->make_sort(smt::BV, s->addr_width()), solver_->make_sort(smt::BV, s->data_width())); } - default: { - ILA_CHECK(false) << "Unknown sort " << sort_uid; - return solver_->make_sort(smt::BOOL); - } - }; // switch sort uid @ lambda Sort2Term + }; // switch sort uid } }; // namespace ilang diff --git a/src/ila-mngr/u_unroller.cc b/src/ila-mngr/u_unroller.cc index f21fdb478..1a6a5f108 100644 --- a/src/ila-mngr/u_unroller.cc +++ b/src/ila-mngr/u_unroller.cc @@ -72,6 +72,10 @@ ZExpr Unroller::Equal(const ExprPtr a, const int& ta, const ExprPtr b, return a_expr == b_expr; } +z3::func_decl Unroller::GetZ3FuncDecl(const FuncPtr& f) const { + return f->GetZ3FuncDecl(ctx_); +} + ZExpr Unroller::UnrollSubs(const size_t& len, const int& pos) { // bootstrap basic information BootStrap(pos); diff --git a/src/ila/ast/expr_var.cc b/src/ila/ast/expr_var.cc index 24c407a9e..c53d93e44 100644 --- a/src/ila/ast/expr_var.cc +++ b/src/ila/ast/expr_var.cc @@ -3,6 +3,8 @@ #include +#include + #include #include @@ -47,12 +49,12 @@ std::ostream& ExprVar::PrintBool(std::ostream& out) const { } std::ostream& ExprVar::PrintBv(std::ostream& out) const { - return out << name().str() + "(" + std::to_string(sort()->bit_width()) + ")"; + return out << fmt::format("{}({})", name().str(), sort()->bit_width()); } std::ostream& ExprVar::PrintMem(std::ostream& out) const { - return out << name().str() + "(" + std::to_string(sort()->addr_width()) + - ", " + std::to_string(sort()->data_width()) + ")"; + return out << fmt::format("{}({}, {})", name().str(), sort()->addr_width(), + sort()->data_width()); } } // namespace ilang diff --git a/src/ila/hash_ast.cc b/src/ila/hash_ast.cc index 93598f239..00933f4fe 100644 --- a/src/ila/hash_ast.cc +++ b/src/ila/hash_ast.cc @@ -1,12 +1,12 @@ /// \file /// Source for the class ExprMngr and the corresponding hash -// XXX Current replacing is not efficient. - #include +#include #include +#include #include namespace ilang { @@ -19,7 +19,7 @@ ExprMngrPtr ExprMngr::New() { return std::make_shared(); } void ExprMngr::clear() { map_.clear(); } -ExprPtr ExprMngr::GetRep(const ExprPtr node) { +ExprPtr ExprMngr::GetRep(const ExprPtr& node) { node->DepthFirstVisit(*this); auto pos = map_.find(Hash(node)); @@ -30,7 +30,7 @@ ExprPtr ExprMngr::GetRep(const ExprPtr node) { return pos->second; } -void ExprMngr::operator()(const ExprPtr node) { +void ExprMngr::operator()(const ExprPtr& node) { ExprPtrVec reps; // replace child (must exist) for (size_t i = 0; i != node->arg_num(); i++) { @@ -49,44 +49,63 @@ void ExprMngr::operator()(const ExprPtr node) { auto pos = map_.find(hash); // new node if (pos == map_.end()) { - map_.insert({hash, node}); + map_.emplace(hash, node); } } -static std::hash ptr_hash_fn; -static std::hash str_hash_fn; -static std::hash int_hash_fn; +std::string ExprMngr::Hash(const ExprPtr& expr) { + static const char* template_var = "var::{sort}::{id}"; + static const char* template_const = "const::{sort}::{value}"; + static const char* template_op = "op::{sort}::{op}::{arg_list}::{param_list}"; + static const char* template_sort = "{type}_{bit}_{addr}_{data}"; + + auto GetSortHash = [](const SortPtr& sort) { + return fmt::format( + template_sort, fmt::arg("type", GetUidSort(sort)), + fmt::arg("bit", sort->is_bv() ? sort->bit_width() : 0), + fmt::arg("addr", sort->is_mem() ? sort->addr_width() : 0), + fmt::arg("data", sort->is_mem() ? sort->data_width() : 0)); + }; + + if (expr->is_var()) { + return fmt::format(template_var, + fmt::arg("sort", GetSortHash(expr->sort())), + fmt::arg("id", expr->name().id())); + + } else if (expr->is_const()) { + auto const_expr = std::static_pointer_cast(expr); + + std::string value = std::to_string(expr->name().id()); + if (expr->is_bool()) { + value = const_expr->val_bool()->str(); + } else if (expr->is_bv()) { + value = const_expr->val_bv()->str(); + } + // skip sharing memory constants -size_t ExprMngr::Hash(const ExprPtr n) const { - if (n->is_op()) { // ExprOp - auto n_op = std::static_pointer_cast(n); + return fmt::format(template_const, + fmt::arg("sort", GetSortHash(expr->sort())), + fmt::arg("value", value)); + } else { + ILA_ASSERT(expr->is_op()); - std::string op_name_str = n_op->op_name(); - auto hash = str_hash_fn(op_name_str); - for (size_t i = 0; i != n->arg_num(); i++) { - hash ^= (ptr_hash_fn(n->arg(i)) << (i * 8)); + std::vector arg_list; + for (size_t i = 0; i < expr->arg_num(); i++) { + arg_list.push_back(expr->arg(i)->name().id()); } - for (size_t i = 0; i != n->param_num(); i++) { - hash ^= (int_hash_fn(n->param(i)) << (i * 8)); + if (auto app_func = std::dynamic_pointer_cast(expr)) { + arg_list.push_back(app_func->func()->name().id()); } - return hash; - } else if (n->is_var()) { // ExprVar - return n->name().id(); - } else { // ExprConst - ILA_ASSERT(n->is_const()) << "Unrecognized expr type"; - auto n_const = std::static_pointer_cast(n); - - if (n_const->is_bool()) { - return str_hash_fn(n_const->val_bool()->str()); - } else if (n_const->is_bv()) { - auto bv_str = n_const->val_bv()->str() + "_" + - std::to_string(n_const->sort()->bit_width()); - return str_hash_fn(bv_str); - } else { - ILA_ASSERT(n_const->is_mem()) << "Unrecognized constant type"; - return str_hash_fn(n_const->name().str()); + std::vector param_list; + for (size_t i = 0; i < expr->param_num(); i++) { + param_list.push_back(expr->param(i)); } + + return fmt::format(template_op, fmt::arg("op", GetUidExprOp(expr)), + fmt::arg("sort", GetSortHash(expr->sort())), + fmt::arg("arg_list", fmt::join(arg_list, ",")), + fmt::arg("param_list", fmt::join(param_list, ","))); } } diff --git a/src/ila/symbol.cc b/src/ila/symbol.cc index 7201825aa..f78b8b2d7 100644 --- a/src/ila/symbol.cc +++ b/src/ila/symbol.cc @@ -31,10 +31,12 @@ const char* Symbol::c_str() const { return name_.c_str(); } const std::string Symbol::format_str(const std::string& prefix, const std::string& suffix) const { std::string res = name_; - if (prefix != "") - res = prefix + "_" + res; - if (suffix != "") - res = res + "_" + suffix; + if (!prefix.empty()) { + res = prefix + "_sEp_" + res; + } + if (!suffix.empty()) { + res = res + "_sEp_" + suffix; + } return res; } diff --git a/src/ilang++.cc b/src/ilang++.cc index c17895757..8aa5dc03f 100644 --- a/src/ilang++.cc +++ b/src/ilang++.cc @@ -4,6 +4,7 @@ #include #include +#include #include #include #include @@ -694,6 +695,31 @@ void Ila::ExportToVerilog(std::ostream& fout) const { void Ila::FlattenHierarchy() { AbsKnob::FlattenIla(ptr_); } +bool Ila::ExecutePass(const std::vector& passes) const { + auto status = true; + for (const auto& id : passes) { + switch (id) { + case PassID::SIMPLIFY_SYNTACTIC: { + status &= pass::SimplifySyntactic(ptr_); + break; + } + case PassID::SIMPLIFY_SEMANTIC: { + status &= pass::SimplifySemantic(ptr_); + break; + } + case PassID::REWRITE_CONDITIONAL_STORE: { + status &= pass::RewriteConditionalStore(ptr_); + break; + } + case PassID::REWRITE_LOAD_FROM_STORE: { + status &= pass::RewriteStoreLoad(ptr_); + break; + } + }; + } + return status; +} + std::ostream& operator<<(std::ostream& out, const ExprRef& expr) { return out << expr.get(); } @@ -715,34 +741,24 @@ Ila ImportIlaPortable(const std::string& file_name) { return Ila(m); } +#ifdef SYNTH_INTERFACE Ila ImportSynthAbstraction(const std::string& file_name, const std::string& ila_name) { -#ifdef SYNTH_INTERFACE auto m = ImportSynthAbsFromFile(file_name, ila_name); return Ila(m); -#else // SYNTH_INTERFACE - auto m = Ila(ila_name); - ILA_ERROR << "Synthesis interface not built."; - ILA_ERROR << "Empty ILA " << ila_name << " is returned."; - return m; -#endif // SYNTH_INTERFACE } void ImportChildSynthAbstraction(const std::string& file_name, Ila& parent, const std::string& ila_name) { -#ifdef SYNTH_INTERFACE auto m = ImportSynthAbsFromFileHier(file_name, parent.get(), ila_name); ILA_NOT_NULL(m); return; -#else - ILA_ERROR << "Synthesis interface not built."; - ILA_ERROR << "Empty ILA " << ila_name << " is returned."; -#endif } +#endif // SYNTH_INTERFACE -void ExportSysCSim(const Ila& ila, const std::string& dir_path) { +void ExportSysCSim(const Ila& ila, const std::string& dir_path, bool opt) { auto ilator = Ilator(ila.get()); - ilator.Generate(dir_path); + ilator.Generate(dir_path, opt); } IlaZ3Unroller::IlaZ3Unroller(z3::context& ctx, const std::string& suff) @@ -752,18 +768,6 @@ IlaZ3Unroller::IlaZ3Unroller(z3::context& ctx, const std::string& suff) IlaZ3Unroller::~IlaZ3Unroller() {} -#if 0 -void IlaZ3Unroller::SetExtraSuffix(const std::string& suff) { - extra_suff_ = suff; - univ_->SetExtraSuffix(suff); -} - -void IlaZ3Unroller::ResetExtraSuffix() { - extra_suff_ = ""; - univ_->ResetExtraSuffix(); -} -#endif - z3::expr IlaZ3Unroller::UnrollMonoConn(const Ila& top, const int& k, const int& init) { auto u = std::make_shared(ctx_, extra_suff_); @@ -828,6 +832,10 @@ z3::expr IlaZ3Unroller::Equal(const ExprRef& va, const int& ta, return univ_->Equal(va.get(), ta, vb.get(), tb); } +z3::func_decl IlaZ3Unroller::GetZ3FuncDecl(const FuncRef& f) const { + return univ_->GetZ3FuncDecl(f.get()); +} + void LogLevel(const int& lvl) { SetLogLevel(lvl); } void LogPath(const std::string& path) { SetLogPath(path); } diff --git a/src/target-sc/ilator.cc b/src/target-sc/ilator.cc index a636c0877..b691f8444 100644 --- a/src/target-sc/ilator.cc +++ b/src/target-sc/ilator.cc @@ -4,9 +4,14 @@ #include #include +#include +#include +#include #include #include +#include +#include #include #include @@ -64,9 +69,9 @@ Ilator::Ilator(const InstrLvlAbsPtr& m) : m_(m) {} Ilator::~Ilator() { Reset(); } -void Ilator::Generate(const std::string& dst) { +void Ilator::Generate(const std::string& dst, bool opt) { // sanity checks and initialize - if (!SanityCheck() || !Bootstrap(dst)) { + if (!SanityCheck() || !Bootstrap(dst, opt)) { return; } @@ -84,6 +89,9 @@ void Ilator::Generate(const std::string& dst) { // constant memory status &= GenerateConstantMemory(os_portable_append_dir(dst, dir_src)); + // initial condition setup + status &= GenerateInitialSetup(os_portable_append_dir(dst, dir_src)); + // execution kernel status &= GenerateExecuteKernel(os_portable_append_dir(dst, dir_src)); @@ -134,26 +142,33 @@ bool Ilator::SanityCheck() const { return true; } -bool Ilator::Bootstrap(const std::string& root) { +bool Ilator::Bootstrap(const std::string& root, bool opt) { Reset(); + auto status = true; + + // light-weight preprocessing + if (opt) { + status &= pass::SimplifySyntactic(m_); + status &= pass::RewriteConditionalStore(m_); + } // 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) { + status &= os_portable_mkdir(root); + status &= os_portable_mkdir(os_portable_append_dir(root, dir_app)); + status &= os_portable_mkdir(os_portable_append_dir(root, dir_extern)); + status &= os_portable_mkdir(os_portable_append_dir(root, dir_include)); + status &= os_portable_mkdir(os_portable_append_dir(root, dir_src)); + if (!status) { os_portable_remove_directory(root); - ILA_ERROR << "Fail structuring simulator direcory at " << root; - return false; } - return true; + + ILA_ERROR_IF(!status) << "Fail bootstraping"; + return status; } bool Ilator::GenerateInstrContent(const InstrPtr& instr, const std::string& dir) { - fmt::memory_buffer buff; + StrBuff buff; ExprVarMap lut; // include headers @@ -176,18 +191,30 @@ bool Ilator::GenerateInstrContent(const InstrPtr& instr, auto update_func = RegisterFunction(GetUpdateFuncName(instr)); BeginFuncDef(update_func, buff); lut.clear(); + std::set visited; auto updated_states = instr->updated_states(); - for (auto& s : updated_states) { + for (const auto& s : updated_states) { + // check if visited + auto update_expr = instr->update(s); + if (auto pos = visited.find(update_expr); pos == visited.end()) { + visited.insert(update_expr); + } else { + continue; + } + + // create placeholder 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) + fmt::format_to(buff, "auto {local_var}_nxt_holder = {local_var};\n", + fmt::arg("local_var", LookUp(update_expr, lut))); + } else { // memory (one copy for performance, require special handling) if (HasLoadFromStore(update_expr)) { return false; } auto placeholder = GetLocalVar(lut); - auto [it, status] = lut.insert({update_expr, placeholder}); + auto [it, status] = lut.try_emplace(update_expr, placeholder); ILA_ASSERT(status); auto mem_update_func = RegisterMemoryUpdate(update_expr); fmt::format_to(buff, @@ -197,7 +224,7 @@ bool Ilator::GenerateInstrContent(const InstrPtr& instr, fmt::arg("mem_update_func", mem_update_func->name), fmt::arg("placeholder", placeholder)); // dummy traverse collect related memory operation - fmt::memory_buffer dummy_buff; + StrBuff dummy_buff; ExprVarMap dummy_lut; if (!RenderExpr(update_expr, dummy_buff, dummy_lut)) { return false; @@ -209,7 +236,7 @@ bool Ilator::GenerateInstrContent(const InstrPtr& instr, auto curr = instr->host()->state(s); auto next = instr->update(s); if (!curr->is_mem()) { - fmt::format_to(buff, "{current} = {next_value};\n", + fmt::format_to(buff, "{current} = {next_value}_nxt_holder;\n", fmt::arg("current", GetCxxName(curr)), fmt::arg("next_value", LookUp(next, lut))); } else { @@ -229,22 +256,52 @@ bool Ilator::GenerateInstrContent(const InstrPtr& instr, } bool Ilator::GenerateMemoryUpdate(const std::string& dir) { - fmt::memory_buffer buff; - ExprVarMap lut; + // helper for traversing memory updates + class MemUpdateVisiter { + public: + MemUpdateVisiter(Ilator* h, StrBuff& b, ExprVarMap& l) + : host(h), buff_ref(b), lut_ref(l) {} + + bool pre(const ExprPtr& expr) { + // stop traversing when reaching memory ITE (stand-alone func) + if (expr->is_mem() && expr->is_op() && + GetUidExprOp(expr) == AST_UID_EXPR_OP::ITE) { + host->DfsExpr(expr, buff_ref, lut_ref); + return true; + } else { + return false; + } + } + + void post(const ExprPtr& expr) { host->DfsExpr(expr, buff_ref, lut_ref); } + + Ilator* host; + StrBuff& buff_ref; + ExprVarMap lut_ref; + }; + + auto RenderMemUpdate = [this](const ExprPtr e, StrBuff& b, ExprVarMap& l) { + auto mem_visiter = MemUpdateVisiter(this, b, l); + e->DepthFirstVisitPrePost(mem_visiter); + }; + + // helpers for managing files int file_cnt = 0; auto GetMemUpdateFile = [&file_cnt]() { return fmt::format("memory_update_functions_{}.cc", file_cnt++); }; + StrBuff buff; auto StartNewFile = [this, &buff]() { buff.clear(); fmt::format_to(buff, "#include <{}.h>\n", GetProjectName()); }; + // start generating StartNewFile(); + ExprVarMap lut; - 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); @@ -255,33 +312,33 @@ bool Ilator::GenerateMemoryUpdate(const std::string& dir) { BeginFuncDef(mem_update_func, buff); if (auto uid = GetUidExprOp(mem); uid == AST_UID_EXPR_OP::STORE) { - status &= RenderExpr(mem, buff, lut); + RenderMemUpdate(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(); + RenderExpr(mem->arg(0), buff, lut); + auto lut_local_true = lut; + auto& lut_local_false = lut; // reuse + + fmt::format_to(buff, "if ({}) {{\n", LookUp(mem->arg(0), lut)); + RenderMemUpdate(mem->arg(1), buff, lut_local_true); fmt::format_to(buff, "}} else {{\n"); - status &= RenderExpr(mem->arg(2), buff, lut_copy); + RenderMemUpdate(mem->arg(2), buff, lut_local_false); fmt::format_to(buff, "}}\n"); } EndFuncDef(mem_update_func, buff); - if (buff.size() > 100000) { + if (buff.size() > 50000) { CommitSource(GetMemUpdateFile(), dir, buff); StartNewFile(); } } CommitSource(GetMemUpdateFile(), dir, buff); - // CommitSource("memory_update_functions.cc", dir, buff); - return status; + return true; } bool Ilator::GenerateConstantMemory(const std::string& dir) { - fmt::memory_buffer buff; + StrBuff buff; fmt::format_to(buff, "#include <{}.h>\n", GetProjectName()); for (auto& mem : const_mems_) { @@ -308,9 +365,63 @@ bool Ilator::GenerateConstantMemory(const std::string& dir) { return true; } +bool Ilator::GenerateInitialSetup(const std::string& dir) { + // conjunct all initial condition + auto init = ExprFuse::BoolConst(true); + auto ConjInit = [&init](const InstrLvlAbsCnstPtr& m) { + for (size_t i = 0; i < m->init_num(); i++) { + init = ExprFuse::And(init, m->init(i)); + } + }; + m_->DepthFirstVisit(ConjInit); + + // get value for referred vars + z3::context ctx; + z3::solver solver(ctx); + Z3ExprAdapter gen(ctx); + solver.add(gen.GetExpr(init)); + auto res = solver.check(); + if (res != z3::sat) { + ILA_ERROR << "Fail finding assignment satisfying initial condition"; + return false; + } + + std::map init_values; + auto model = solver.get_model(); + auto refer_vars = AbsKnob::GetVar(init); + for (const auto& var : refer_vars) { + auto var_value = model.eval(gen.GetExpr(var)); + try { +#ifndef Z3_LEGACY_API + auto value_holder = var_value.get_numeral_uint64(); +#else + __uint64 value_holder; + Z3_get_numeral_uint64(ctx, var_value, &value_holder); +#endif + init_values.emplace(var, value_holder); + } catch (...) { + ILA_ERROR << "Fail getting " << var_value; + return false; + } + } + + // gen file + auto init_func = RegisterFunction("setup_initial_condition"); + StrBuff buff; + fmt::format_to(buff, "#include <{}.h>\n", GetProjectName()); + BeginFuncDef(init_func, buff); + for (auto pair : init_values) { + fmt::format_to(buff, "{var_name} = {var_value};\n", + fmt::arg("var_name", GetCxxName(pair.first)), + fmt::arg("var_value", pair.second)); + } + EndFuncDef(init_func, buff); + CommitSource("setup_initial_condition.cc", dir, buff); + return true; +} + bool Ilator::GenerateExecuteKernel(const std::string& dir) { - auto kernel_func = RegisterFunction("compute"); - fmt::memory_buffer buff; + StrBuff buff; fmt::format_to( // headers buff, @@ -328,16 +439,23 @@ bool Ilator::GenerateExecuteKernel(const std::string& dir) { "}}\n", fmt::arg("project", GetProjectName())); + fmt::format_to(buff, "static bool g_initialized = false;\n"); + + auto kernel_func = RegisterFunction("compute"); BeginFuncDef(kernel_func, buff); + // setup initial condition + fmt::format_to(buff, "if (!g_initialized) {{\n" + " setup_initial_condition();\n" + " g_initialized = true;\n" + "}}\n"); + // 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( @@ -385,7 +503,7 @@ bool Ilator::GenerateExecuteKernel(const std::string& dir) { } bool Ilator::GenerateGlobalHeader(const std::string& dir) { - fmt::memory_buffer buff; + StrBuff buff; fmt::format_to(buff, "#include \n" @@ -463,17 +581,8 @@ bool Ilator::GenerateGlobalHeader(const std::string& dir) { } 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, + static const char* cmake_recipe_template = "# CMakeLists.txt for {project}\n" "cmake_minimum_required(VERSION 3.14.0)\n" "project({project} LANGUAGES CXX)\n" @@ -505,37 +614,61 @@ bool Ilator::GenerateBuildSupport(const std::string& dir) { " )\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)); + "endif()\n"; + + 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))); + } + + StrBuff buff; + fmt::format_to(buff, cmake_recipe_template, + 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 = + static const char* sim_entry_template = + "#include <{project}.h>\n\n" + "int sc_main(int argc, char* argv[]) {{\n" + " return 0; \n" + "}}\n"; + + auto entry_path = os_portable_append_dir(os_portable_append_dir(dir, dir_app), "main.cc"); - if (!os_portable_exist(app_template)) { + + if (!os_portable_exist(entry_path)) { buff.clear(); - fmt::format_to(buff, - "#include <{project}.h>\n\n" - "int sc_main(int argc, char* argv[]) {{\n" - " return 0; \n" - "}}\n", + fmt::format_to(buff, sim_entry_template, fmt::arg("project", GetProjectName())); - WriteFile(app_template, buff); + WriteFile(entry_path, buff); } return true; } bool Ilator::RenderExpr(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { + + class ExprDfsVisiter { + public: + ExprDfsVisiter(Ilator* hi, StrBuff& bi, ExprVarMap& li) + : host(hi), b(bi), l(li) {} + bool pre(const ExprPtr& e) { return l.find(e) != l.end(); } + void post(const ExprPtr& e) { host->DfsExpr(e, b, l); } + + Ilator* host; + StrBuff& b; + ExprVarMap& l; + }; + try { - auto visiter = [this, &buff, &lut](const ExprPtr& e) { - DfsExpr(e, buff, lut); - }; - expr->DepthFirstVisit(visiter); + auto visiter = ExprDfsVisiter(this, buff, lut); + expr->DepthFirstVisitPrePost(visiter); } catch (std::exception& err) { ILA_ERROR << err.what(); return false; diff --git a/src/target-sc/ilator_dfs.cc b/src/target-sc/ilator_dfs.cc index 697a1d694..3b2cf7db6 100644 --- a/src/target-sc/ilator_dfs.cc +++ b/src/target-sc/ilator_dfs.cc @@ -10,30 +10,29 @@ 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); +void Ilator::DfsExpr(const ExprPtr& e, StrBuff& buff, ExprVarMap& lut) { + if (auto pos = lut.find(e); pos == lut.end()) { + if (e->is_var()) { + DfsVar(e, buff, lut); + } else if (e->is_const()) { + DfsConst(e, buff, lut); } else { - ILA_ASSERT(expr->is_op()); - DfsOp(expr, buff, lut); + ILA_ASSERT(e->is_op()); + DfsOp(e, buff, lut); } } - ILA_ASSERT((expr->is_mem() && expr->is_op()) || - (lut.find(expr) != lut.end())); + ILA_ASSERT((e->is_mem() && e->is_op()) || (lut.find(e) != lut.end())); } void Ilator::DfsVar(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) const { - auto [it, status] = lut.insert({expr, GetCxxName(expr)}); + auto [it, status] = lut.try_emplace(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}); + auto [it, status] = lut.try_emplace(expr, local_var); ILA_ASSERT(status); // alias for constant memory @@ -122,7 +121,7 @@ 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}); + auto [it, status] = lut.try_emplace(expr, local_var); ILA_ASSERT(status); // apply uninterpreted function @@ -145,7 +144,7 @@ void Ilator::DfsOpAppFunc(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { void Ilator::DfsOpSpecial(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) { auto local_var = GetLocalVar(lut); - auto [it, status] = lut.insert({expr, local_var}); + auto [it, status] = lut.try_emplace(expr, local_var); ILA_ASSERT(status); switch (auto uid = GetUidExprOp(expr); uid) { @@ -258,7 +257,7 @@ static const std::unordered_map k_op_symbols = { void Ilator::DfsOpRegular(const ExprPtr& expr, StrBuff& buff, ExprVarMap& lut) const { auto local_var = GetLocalVar(lut); - auto [it, status] = lut.insert({expr, local_var}); + auto [it, status] = lut.try_emplace(expr, local_var); ILA_ASSERT(status); // get the corresponding operator symbol diff --git a/src/vtarget-out/vtarget_gen_yosys.cc b/src/vtarget-out/vtarget_gen_yosys.cc index 5a6d74b6a..0426fce00 100644 --- a/src/vtarget-out/vtarget_gen_yosys.cc +++ b/src/vtarget-out/vtarget_gen_yosys.cc @@ -2,15 +2,17 @@ /// the inv-syn related HC generation is located in inv_syn.cc // --- Hongce Zhang +#include + #include #include +#include + #include #include #include #include #include -#include -#include namespace ilang { @@ -242,51 +244,51 @@ VlgSglTgtGen_Yosys::VlgSglTgtGen_Yosys( ILA_CHECK(chc_target == _chc_target_t::GENERAL_PROPERTY); ILA_CHECK(target_tp == target_type_t::INVARIANTS || - target_tp == target_type_t::INSTRUCTIONS) + target_tp == target_type_t::INSTRUCTIONS) << "Unknown target type: " << target_tp; ILA_CHECK((vbackend & backend_selector::YOSYS) == backend_selector::YOSYS) << "Must use Yosys as vbackend"; ILA_CHECK(s_backend == synthesis_backend_selector::ABC || - s_backend == synthesis_backend_selector::Z3 || - s_backend == synthesis_backend_selector::GRAIN || - s_backend == synthesis_backend_selector::ELDERICA || - s_backend == synthesis_backend_selector::NOSYN); + s_backend == synthesis_backend_selector::Z3 || + s_backend == synthesis_backend_selector::GRAIN || + s_backend == synthesis_backend_selector::ELDERICA || + s_backend == synthesis_backend_selector::NOSYN); ILA_CHECK(IMPLY(s_backend == synthesis_backend_selector::GRAIN, - vtg_config.YosysSmtFlattenDatatype && - vtg_config.YosysSmtFlattenHierarchy)) + vtg_config.YosysSmtFlattenDatatype && + vtg_config.YosysSmtFlattenHierarchy)) << "Grain requires not to flatten hierarchy/datatype"; ILA_CHECK(IMPLY(s_backend == synthesis_backend_selector::ABC, - _vtg_config.AbcUseAiger)) + _vtg_config.AbcUseAiger)) << "Currently only support using AIGER"; ILA_CHECK(IMPLY(s_backend == synthesis_backend_selector::ABC, - vtg_config.YosysSmtFlattenHierarchy)) + vtg_config.YosysSmtFlattenHierarchy)) << "ABC requires to flatten hierarchy"; // This is hard-coded in the Yosys script // if not flattened, abc will be unhappy ILA_CHECK(IMPLY(s_backend == synthesis_backend_selector::ABC, - vbackend == backend_selector::ABCPDR)); + vbackend == backend_selector::ABCPDR)); ILA_CHECK(IMPLY(s_backend == synthesis_backend_selector::GRAIN, - vbackend == backend_selector::GRAIN_SYGUS && - _vtg_config.YosysSmtStateSort == _vtg_config.Datatypes)); + vbackend == backend_selector::GRAIN_SYGUS && + _vtg_config.YosysSmtStateSort == _vtg_config.Datatypes)); ILA_CHECK(IMPLY(s_backend == synthesis_backend_selector::Z3, - vbackend == backend_selector::Z3PDR)); + vbackend == backend_selector::Z3PDR)); ILA_CHECK(IMPLY(vbackend == backend_selector::BTOR_GENERIC, - s_backend == synthesis_backend_selector::NOSYN)); + s_backend == synthesis_backend_selector::NOSYN)); ILA_CHECK(s_backend != synthesis_backend_selector::ELDERICA) << "Bug : not implemented yet!"; ILA_CHECK(!(_vtg_config.YosysSmtFlattenDatatype && - _vtg_config.YosysSmtStateSort != _vtg_config.Datatypes)) + _vtg_config.YosysSmtStateSort != _vtg_config.Datatypes)) << "Must use Datatypes to encode state in order to flatten"; } // VlgSglTgtGen_Yosys @@ -571,10 +573,10 @@ void VlgSglTgtGen_Yosys::Export_script(const std::string& script_name) { ILA_CHECK(false) << "Not implemented."; } else if (s_backend == synthesis_backend_selector::NOSYN) { if (!_vtg_config.BtorGenericCmdline.empty()) { - runnable = ReplaceAll(_vtg_config.BtorGenericCmdline, "%btorfile%", prob_fname); + runnable = + ReplaceAll(_vtg_config.BtorGenericCmdline, "%btorfile%", prob_fname); options = ""; - } - else{ + } else { runnable = "echo"; options = " \"btor file is available as: " + prob_fname + "\""; } @@ -595,7 +597,7 @@ void VlgSglTgtGen_Yosys::Export_script(const std::string& script_name) { std::shared_ptr VlgSglTgtGen_Yosys::GetDesignSmtInfo() const { ILA_CHECK((_backend & backend_selector::CHC) == backend_selector::CHC && - _vtg_config.YosysSmtStateSort == _vtg_config.Datatypes) + _vtg_config.YosysSmtStateSort == _vtg_config.Datatypes) << "Only CHC target with datatypes will generate suitable smt-lib2."; ILA_CHECK(design_smt_info != nullptr); return design_smt_info; @@ -738,7 +740,7 @@ void VlgSglTgtGen_Yosys::design_only_gen_smt( write_smt2_options += "-stbv "; else ILA_CHECK(false) << "Unsupported smt state sort encoding:" - << _vtg_config.YosysSmtStateSort; + << _vtg_config.YosysSmtStateSort; ys_script_fout << "read_verilog -sv " << os_portable_append_dir(_output_path, top_file_name) diff --git a/test/t_api.cc b/test/t_api.cc index 5b8aa43b5..e2da6facf 100644 --- a/test/t_api.cc +++ b/test/t_api.cc @@ -1,12 +1,16 @@ /// \file /// Unit test for c++ API +#include + +#include +#include + #include "unit-include/config.h" #include "unit-include/eq_ilas.h" +#include "unit-include/ila_sim_test.h" #include "unit-include/simple_cpu.h" #include "unit-include/util.h" -#include -#include #define REG_NUM 16 #define REG_SIZE 8 @@ -325,6 +329,67 @@ TEST(TestApi, EntryNum) { #endif } +TEST(TestApi, OutStream) { + auto m = SimpleCpuRef("m"); + std::string msg = ""; + + // ila + GET_STDOUT_MSG((std::cout << m), msg); + EXPECT_TRUE(msg.find(m.name()) != std::string::npos); + + // state + for (size_t i = 0; i < m.state_num(); i++) { + auto state = m.state(i); + GET_STDOUT_MSG((std::cout << state), msg); + EXPECT_TRUE(msg.find(state.name()) != std::string::npos); + } + + auto pc = m.state("pc"); + + // instr + for (size_t i = 0; i < m.instr_num(); i++) { + auto instr = m.instr(i); + GET_STDOUT_MSG((std::cout << instr), msg); + EXPECT_TRUE(msg.find(instr.name()) != std::string::npos); + + GET_STDOUT_MSG((std::cout << instr.GetDecode()), msg); + EXPECT_FALSE(msg.empty()); + + auto next_pc = instr.GetUpdate(pc); + GET_STDOUT_MSG((std::cout << next_pc), msg); // not NULL + EXPECT_FALSE(msg.empty()); + } +} + +TEST(TestApi, VerilogGen) { + auto tmp_dir = GetRandomFileName(); + os_portable_mkdir(tmp_dir); + + // ila + auto m = SimpleCpuRef("m"); + auto tmp_file_ila = GetRandomFileName(tmp_dir); + std::ofstream fout(tmp_file_ila); + m.ExportToVerilog(fout); + fout.close(); + + // instr + for (size_t i = 0; i < m.instr_num(); i++) { + auto instr = m.instr(i); + + auto tmp_file_instr = GetRandomFileName(tmp_dir); + fout.open(tmp_file_instr); + instr.ExportToVerilog(fout); + fout.close(); + + auto tmp_file_instr_child = GetRandomFileName(tmp_dir); + fout.open(tmp_file_instr_child); + instr.ExportToVerilogWithChild(fout); + fout.close(); + } + + os_portable_remove_directory(tmp_dir); +} + TEST(TestApi, Unroll) { z3::context c; auto unroller = IlaZ3Unroller(c); @@ -457,6 +522,66 @@ TEST(TestApi, Log) { #endif } +TEST(TestApi, UnrollPathFreeWithFunc) { + z3::context ctx; + z3::solver solver(ctx); + + auto unroller = IlaZ3Unroller(ctx); + auto m0 = IlaSimTest("m0").model; + auto m1 = IlaSimTest("m1").model; + + // start from saem state + auto same_state = BoolConst(true); + for (size_t i = 0; i < m0.state_num(); i++) { + auto state_0 = m0.state(i); + auto state_1 = m1.state(state_0.name()); + same_state = same_state & (state_0 == state_1); + } + unroller.AddInitPred(same_state); + + // always share same input + auto same_input = BoolConst(true); + for (size_t i = 0; i < m0.input_num(); i++) { + auto input_0 = m0.input(i); + auto input_1 = m1.input(input_0.name()); + same_input = same_input & (input_0 == input_1); + } + unroller.AddGlobPred(same_input); + + // unroll instr sequence + auto seq0 = {m0.instr("WRITE_ADDRESS"), m0.instr("START_ENCRYPT")}; + auto seq1 = {m1.instr("WRITE_ADDRESS"), m1.instr("START_ENCRYPT")}; + auto path0 = unroller.UnrollPathConn(seq0); + auto path1 = unroller.UnrollPathFree(seq1); + + auto connect = ctx.bool_val(true); + for (size_t i = 0; i < m1.state_num(); i++) { + auto state = m1.state(i); + connect = connect && + (unroller.NextState(state, 0) == unroller.CurrState(state, 1)) && + (unroller.NextState(state, 1) == unroller.CurrState(state, 2)); + } + + // func + auto farg = SortRef::BV(128); + auto func = unroller.GetZ3FuncDecl(FuncRef("process128", farg, farg, farg)); + auto x = ctx.bv_const("x", 128); + auto y = ctx.bv_const("y", 128); + auto fdef = z3::forall(x, y, func(x, y) == (x + y)); // dummy + + // check length + auto to_check = unroller.Equal(m0.state("length"), 2, m1.state("length"), 2); + + // SMT query + solver.add(path0); + solver.add(path1); + solver.add(fdef); + solver.add(!to_check); + EXPECT_EQ(solver.check(), z3::sat); + solver.add(connect); + EXPECT_EQ(solver.check(), z3::unsat); +} + TEST(TestApi, Portable) { // SetToStdErr(1); EnableDebug("Portable"); diff --git a/test/t_ilator.cc b/test/t_ilator.cc index ff96ff537..ee5f72b1d 100644 --- a/test/t_ilator.cc +++ b/test/t_ilator.cc @@ -31,9 +31,14 @@ class TestIlator : public ::testing::Test { }; // TestIlator -TEST_F(TestIlator, IlaSimTest) { +TEST_F(TestIlator, Default) { IlaSimTest m; ExportSysCSim(m.model, out_dir); } +TEST_F(TestIlator, Optimize) { + IlaSimTest m; + ExportSysCSim(m.model, out_dir, true); +} + } // namespace ilang diff --git a/test/t_pass.cc b/test/t_pass.cc index e569a4344..4ef7c147a 100644 --- a/test/t_pass.cc +++ b/test/t_pass.cc @@ -12,9 +12,7 @@ namespace ilang { void ApplyPass(const std::string& dir, const std::string& file, bool simplify = true) { - // SetToStdErr(true); - - EnableDebug("PassSimpInstrUpdate"); + EnableDebug("PassSimpSemantic"); EnableDebug("PassRewrCondStore"); EnableDebug("PassRewrStoreLoad"); EnableDebug("PassInferChildProgCFG"); @@ -22,18 +20,24 @@ void ApplyPass(const std::string& dir, const std::string& file, auto file_dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, dir); auto ila_file = os_portable_append_dir(file_dir, file); - auto ila = ImportIlaPortable(ila_file).get(); + auto ila = ImportIlaPortable(ila_file); - PassSimplifyInstrUpdate(ila); + ila.ExecutePass({Ila::PassID::SIMPLIFY_SYNTACTIC, + Ila::PassID::SIMPLIFY_SEMANTIC, + Ila::PassID::REWRITE_CONDITIONAL_STORE, + Ila::PassID::REWRITE_LOAD_FROM_STORE}); - PassRewriteConditionalStore(ila); - PassRewriteStoreLoad(ila); + pass::InferChildProgCFG(ila.get()); + pass::MapChildProgEntryPoint(ila.get()); - PassInferChildProgCFG(ila); - PassMapChildProgEntryPoint(ila); + auto org = ImportIlaPortable(ila_file); + CheckIlaEqLegacy(org.get(), ila.get()); - auto out_file = "opt_" + file; - ExportIlaPortable(Ila(ila), out_file); + DisableDebug("PassSimpSemantic"); + DisableDebug("PassRewrCondStore"); + DisableDebug("PassRewrStoreLoad"); + DisableDebug("PassInferChildProgCFG"); + DisableDebug("PassMapChildProgEntry"); } TEST(TestPass, AES) { ApplyPass("aes", "aes.json"); } diff --git a/test/t_symbol.cc b/test/t_symbol.cc index fd897061c..97d8d60df 100644 --- a/test/t_symbol.cc +++ b/test/t_symbol.cc @@ -64,9 +64,9 @@ TEST(TestSymbol, Copy) { TEST(TestSymbol, Format) { Symbol sym("name"); - EXPECT_EQ("name_suf", sym.format_str("", "suf")); - EXPECT_EQ("pre_name", sym.format_str("pre", "")); - EXPECT_EQ("p_name_s", sym.format_str("p", "s")); + EXPECT_EQ("name_sEp_suf", sym.format_str("", "suf")); + EXPECT_EQ("pre_sEp_name", sym.format_str("pre", "")); + EXPECT_EQ("p_sEp_name_sEp_s", sym.format_str("p", "s")); } TEST(TestSymbol, Compare) { diff --git a/test/t_unroll_seq.cc b/test/t_unroll_seq.cc index aa2173a2f..7e85b7218 100644 --- a/test/t_unroll_seq.cc +++ b/test/t_unroll_seq.cc @@ -1,11 +1,13 @@ /// \file /// Unit test for unrolling a sequence of instruction. +#include + +#include + #include "unit-include/eq_ilas.h" #include "unit-include/simple_cpu.h" #include "unit-include/util.h" -#include -#include namespace ilang { @@ -36,7 +38,7 @@ class TestUnroll : public ::testing::Test { }; // class TestUnroll -TEST_F(TestUnroll, InsteSeqFlatSubs) { +TEST_F(TestUnroll, InstrSeqFlatSubs) { auto m = ila_gen_.GetIlaFlat1(); std::vector seq; @@ -48,7 +50,7 @@ TEST_F(TestUnroll, InsteSeqFlatSubs) { auto cstr = unroller->PathSubs(seq); } -TEST_F(TestUnroll, InsteSeqFlatAssn) { +TEST_F(TestUnroll, InstrSeqFlatAssn) { auto m = ila_gen_.GetIlaFlat1(); std::vector seq; diff --git a/test/t_vtarget_gen.cc b/test/t_vtarget_gen.cc index 7ea3cb1fa..a0ed39d58 100644 --- a/test/t_vtarget_gen.cc +++ b/test/t_vtarget_gen.cc @@ -15,39 +15,6 @@ namespace ilang { typedef std::vector P; -TEST(TestVlgTargetGen, AesIlaInfo) { - auto aes_dir = os_portable_append_dir(ILANG_TEST_DATA_DIR, "aes"); - auto aesFile = os_portable_append_dir(aes_dir, "aes_v_top.abst"); - auto aesuFile = os_portable_append_dir(aes_dir, "aes_v_child.abst"); - auto aes = ImportSynthAbstraction(aesFile, "AES").get(); - auto aesu = ImportSynthAbstraction(aesuFile, "AES_U").get(); - - // aes->AddChild(aesu); - - ILA_DLOG("TestVlgTargetGen.IlaInfo") << "No. instr:" << aes->instr_num(); - for (unsigned i = 0; i < aes->instr_num(); ++i) { - ILA_DLOG("TestVlgTargetGen.IlaInfo") << "\t" << aes->instr(i)->name().str() - << "\t" << aes->instr(i)->decode(); - } - ILA_DLOG("TestVlgTargetGen.IlaInfo") << "No. state:" << aes->state_num(); - for (unsigned i = 0; i < aes->state_num(); ++i) { - ILA_DLOG("TestVlgTargetGen.IlaInfo") << "\t" << aes->state(i)->name().str(); - } - ILA_DLOG("TestVlgTargetGen.IlaInfo") << std::endl; - - ILA_DLOG("TestVlgTargetGen.IlaInfo") << "No. instr:" << aesu->instr_num(); - for (unsigned i = 0; i < aes->instr_num(); ++i) { - ILA_DLOG("TestVlgTargetGen.IlaInfo") << "\t" << aesu->instr(i)->name().str() - << "\t" << aesu->instr(i)->decode(); - } - ILA_DLOG("TestVlgTargetGen.IlaInfo") << "No. state:" << aesu->state_num(); - for (unsigned i = 0; i < aesu->state_num(); ++i) { - ILA_DLOG("TestVlgTargetGen.IlaInfo") - << "\t" << aesu->state(i)->name().str(); - } - ILA_DLOG("TestVlgTargetGen.IlaInfo") << std::endl; -} - TEST(TestVlgTargetGen, PipeExample) { auto ila_model = SimplePipe::BuildModel(); diff --git a/test/unit-include/ila_sim_test.h b/test/unit-include/ila_sim_test.h index a9e9153e6..c291bc7cb 100644 --- a/test/unit-include/ila_sim_test.h +++ b/test/unit-include/ila_sim_test.h @@ -25,16 +25,16 @@ using namespace ilang; class IlaSimTest { public: - IlaSimTest(); + IlaSimTest(const std::string& name = "TEST"); Ila model; protected: - static ExprRef slice_read(const ExprRef ®, const ExprRef &idx, + static ExprRef slice_read(const ExprRef& reg, const ExprRef& idx, unsigned long base_addr, unsigned no_slice, unsigned slice_width); - static ExprRef slice_update(const ExprRef ®, const ExprRef &idx, - const ExprRef &input_slice, + static ExprRef slice_update(const ExprRef& reg, const ExprRef& idx, + const ExprRef& input_slice, unsigned long base_addr, unsigned no_slice, unsigned slice_width); diff --git a/test/unit-include/util.h b/test/unit-include/util.h index 4b9ef7047..442211a7b 100644 --- a/test/unit-include/util.h +++ b/test/unit-include/util.h @@ -46,7 +46,7 @@ void EndRecordLog(); cmd; \ msg = ::testing::internal::GetCapturedStderr(); -std::string GetRandomFileName(const std::string& dir); +std::string GetRandomFileName(const std::string& dir = ""); void CheckIlaEqLegacy(const InstrLvlAbsPtr& a, const InstrLvlAbsPtr& b); diff --git a/test/unit-src/ila_sim_test.cc b/test/unit-src/ila_sim_test.cc index 45db4591e..445add31e 100644 --- a/test/unit-src/ila_sim_test.cc +++ b/test/unit-src/ila_sim_test.cc @@ -1,8 +1,11 @@ -#include "../unit-include/ila_sim_test.h" -#include #include -IlaSimTest::IlaSimTest() - : model("TEST"), cmd(model.NewBvInput("cmd", 2)), + +#include + +#include "../unit-include/ila_sim_test.h" + +IlaSimTest::IlaSimTest(const std::string& name) + : model(name), cmd(model.NewBvInput("cmd", 2)), cmdaddr(model.NewBvInput("cmdaddr", 16)), cmddata(model.NewBvInput("cmddata", 8)), cmdflag(model.NewBoolInput("cmdflag")), flag(model.NewBoolState("flag")), @@ -29,10 +32,11 @@ IlaSimTest::IlaSimTest() (cmdaddr < ADDR + 2)); instr.SetUpdate( - address, Ite(is_status_idle, - Concat(Ite(cmdaddr == ADDR + 1, cmddata/cmddata, address(15, 8)), - Ite(cmdaddr == ADDR, cmddata * cmddata, address(7, 0))), - address)); + address, + Ite(is_status_idle, + Concat(Ite(cmdaddr == ADDR + 1, cmddata / cmddata, address(15, 8)), + Ite(cmdaddr == ADDR, cmddata * cmddata, address(7, 0))), + address)); instr.SetUpdate(flag, Ite(is_status_idle, flag_true, flag_false)); diff --git a/test/unit-src/util.cc b/test/unit-src/util.cc index 543d4a111..0d8c1a05f 100644 --- a/test/unit-src/util.cc +++ b/test/unit-src/util.cc @@ -28,13 +28,16 @@ std::string random_string(std::size_t length) { } std::string GetRandomFileName(const std::string& dir) { - ILA_ASSERT(fs::is_directory(dir)) << dir << " doesn't exist"; + auto root = fs::path(dir); + if (dir.empty() || !fs::is_directory(dir)) { + root = fs::temp_directory_path(); + } auto file_name = fs::path(random_string(6)); - while (fs::exists(fs::path(dir) / file_name)) { + while (fs::exists(root / file_name)) { file_name = fs::path(random_string(6)); } - return (dir / file_name).string(); + return (root / file_name).string(); } void CheckIlaEqLegacy(const InstrLvlAbsPtr& a, const InstrLvlAbsPtr& b) {