Merge pull request #197 from Bo-Yuan-Huang/cleanup

[v1.1.1] Bug fix and clean up

.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

.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

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
 )
 

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 |

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

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

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<ExprPtr(const ExprPtr)> Rewr);
+bool RewriteGeneric(const InstrLvlAbsPtr& m,
+                    std::function<ExprPtr(const ExprPtr)> 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
 

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<ExprPtr> 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<ExprPtr> ValidCondStack;
+
   /// ILA mapping.
   IlaMap ila_map_;
   /// Expr mapping.

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.

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 -------------------------------------- //

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<ExprMngr> ExprMngrPtr;
+
   // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
   /// Default constructor.
   ExprMngr();
   /// Default destructor.
   ~ExprMngr();
 
-  /// Pointer type for passing shared ast simplifier.
-  typedef std::shared_ptr<ExprMngr> ExprMngrPtr;
-  /// Type for cacheing the AST node hashing.
-  typedef std::unordered_map<size_t, const ExprPtr> 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<std::string, ExprPtr> map_;
 
   // ------------------------- HELPER FUNCTIONS ----------------------------- //
   /// Hash function.
-  size_t Hash(const ExprPtr node) const;
+  static std::string Hash(const ExprPtr& node);
 
 }; // class ExprMngr
 

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<ExprRef>& 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<PassID>& 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 -------------------------------------- //

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,14 +75,16 @@ 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);
   /// Special handle for memory updates.
   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;