Merge pull request #196 from Bo-Yuan-Huang/unroll

ILAtor and z3 unroll

.travis.yml

@@ -8,27 +8,26 @@ git:
   depth: 1
   submodules: false
 
-sudo: required
-
 language: cpp
 
 env:
   global:
    - secure: "RwHto3MzZ2KTsGK2LiCKCxdN/xzuWiCTO+2+zhfPjVujGMx84QdMHC5fRu94VoJ5PdZ5QHwoWy3jqQ0f2PJE7oRQe28w/ENY32yDl/ziRjY1U6k4p2pcfgYQtsyyof60mL+yG6Yzz4hlJ74uQ+arhdvyAYYvliyvUiHkLgp4XvJhmsqpogkL89pERAeZ32Xg22ajzXZD5tcWQ7CbCDVKOE0KrwktU3UG08VxMmgfjKG+rU1MKj5R8rXtwZrMzqEAzosTEK0miZYJcgO0pVStCeAC2UAZllEpWXaR2EW5plb/hXRmFjRSlWflasGzJ7VB6mZ95w4xm2DICKYgcrwPWgiMnwoEByrJBh0M7xBzU1MTFmbiqB5wSSsWfVA7zv+SLmD4mCww4HKxAkE2cDJ3MOAvK8bp1vCULBCMMmbVFNGQgBprZKoxUlpQLNn+y9C6pQoaCej9/KVdkyiSQ8SM2vXDoS4/CGnoeaOAoNpu5mkPmDk7RRjIPjdS7by9xycYXAoUVVty/EZideCrYswe1KvH87GK6Fd91XITHuhuc/Aw4Jg0zXjxx6dcHbjZKuYN5MgNMx4IWK+lNiKPyLGO1/AnFG1UP+CpOC6QE8XZNhcnvn3q4r6c+v/QbeoEE7O/XOXqJDSEumJ5b2psBuoktl52azKgUqMtDzuTWjv6BvY="
+   - MATRIX_EVAL="CC=gcc-7 && CXX=g++-7"
 
 
 cache:
   directories:
     - $HOME/_cache
 
-matrix:
+jobs:
   include:
-    - name: "linux-gcc"
+    - name: "xenial"
       os: linux
       dist: xenial
-      compiler: gcc
       before_install:
         - gem install coveralls-lcov
+        - eval "${MATRIX_EVAL}"
       before_script:
         - mkdir -p $TRAVIS_BUILD_DIR/build 
         - source $TRAVIS_BUILD_DIR/scripts/travis/clean-coverage.sh $TRAVIS_BUILD_DIR/build
@@ -40,7 +39,6 @@ matrix:
     - name: "coverity"
       os: linux
       dist: xenial
-      compiler: gcc
       addons:
         coverity_scan:
           project:
@@ -52,28 +50,35 @@ matrix:
           branch_pattern: coverity_scan
         apt:
           update: true
+          sources:
+            - ubuntu-toolchain-r-test
           packages:
             - flex
             - bison
             - z3
             - libz3-dev
+            - g++-7
       before_install:
-        - echo -n | openssl s_client -connect https://scan.coverity.com:443 | sed -ne '/-BEGIN CERTIFICATE-/,/-END CERTIFICATE-/p' | sudo tee -a /etc/ssl/certs/ca- 
+        - echo -n | openssl s_client -connect https://scan.coverity.com:443 | sed -ne '/-BEGIN CERTIFICATE-/,/-END CERTIFICATE-/p' | sudo tee -a /etc/ssl/certs/ca-
       before_script:
+        - eval "${MATRIX_EVAL}"
         - source $TRAVIS_BUILD_DIR/scripts/travis/install-externs.sh $TRAVIS_BUILD_DIR
       script:
         - source $TRAVIS_BUILD_DIR/scripts/travis/build-static.sh $TRAVIS_BUILD_DIR
 
 addons:
   apt:
     update: true
+    sources:
+      - ubuntu-toolchain-r-test
     packages:
       - lcov
       - flex
       - bison
       - libboost-all-dev
       - z3
       - libz3-dev
+      - g++-7
 
 notifications:
     email: false

CMakeLists.txt

@@ -11,7 +11,7 @@ endif()
 # PROJECT
 # name version language
 # ---------------------------------------------------------------------------- #
-project(ilang VERSION     1.0.5
+project(ilang VERSION     1.1.0
               LANGUAGES   CXX
 )
 
@@ -115,7 +115,7 @@ add_subdirectory(src)
 include(CMakePackageConfigHelpers)
 write_basic_package_version_file(
   ${ILANG_CMAKE_VERSION_CONFIG_FILE} 
-  COMPATIBILITY SameMajorVersion # AnyNewVersion
+  COMPATIBILITY AnyNewerVersion
 )
 
 ##

README.md

@@ -37,38 +37,38 @@ ILAng requires CMake (3.9.6 or above) and compilers with C++17 support.
 To install dependencies on Debian-based Linux:
 
 ```bash
-apt-get install bison flex libboost-all-dev z3 libz3-dev
+apt-get install bison flex z3 libz3-dev
 ```
 
 To install dependencies (except z3) on Fedora-based Linux:
 
 ```bash
-yum install bison flex boost boost-python boost-devel
+yum install bison flex
 ```
 
 To install dependencies on OSX:
 
 ```bash
-brew install bison flex boost boost-python z3
+brew install bison flex z3
 ```
 
 -   The [z3](https://github.com/Z3Prover/z3) SMT solver (over 4.4.0) is required. Detailed instruction for building latest z3 can be found [here](https://github.com/Z3prover/z3#building-z3-using-make-and-gccclang).
 -   The [Boost](https://www.boost.org) package is required only if you want to build the synthesis engine (default `OFF`).
 
-#### Regression Environments
-
-| OS                        | Compiler     | CMake  | z3    | Boost | Bison | Flex   | Build   |
-| ------------------------- | ------------ | ------ | ----- | ----- | ----- | ------ | ------- |
-| Ubuntu 16.04 (Xenial)     | clang 7.0.0  | 3.12.4 | 4.4.1 | 1.58  | 3.0.4 | 2.6.0  | Debug   |
-| Ubuntu 16.04 (Xenial)     | gcc 5.4.0    | 3.12.4 | 4.4.1 | 1.58  | 3.0.4 | 2.6.0  | Debug   |
-| Ubuntu 16.04 (Xenial)     | gcc 5.4.0    | 3.17.0 | 4.4.1 | 1.58  | 3.0.4 | 2.6.0  | Release |
-| Ubuntu 18.04 (Bionic)     | clang 6.0.0  | 3.10.2 | 4.4.1 | 1.65  | 3.0.4 | 2.6.4  | Debug   |
-| Ubuntu 18.04 (Bionic)     | gcc 7.5.0    | 3.10.2 | 4.4.1 | 1.65  | 3.0.4 | 2.6.4  | Debug   |
-| Ubuntu 18.04 (Bionic)     | gcc 7.5.0    | 3.17.0 | 4.4.1 | 1.65  | 3.0.4 | 2.6.4  | Release |
-| Ubuntu 20.04 (Focal Fosa) | gcc 7.4.0    | 3.17.0 | 4.4.1 | -     | 3.0.4 | 2.6.4  | Release |
-| OSX 10.15.4 (Catalina)    | Xcode 11.4.1 | 3.17.2 | 4.8.8 | -     | 3.6.2 | 2.5.35 | Debug   |
-| OSX 10.15.4 (Catalina)    | Xcode 11.4.1 | 3.17.2 | 4.8.8 | -     | 3.6.2 | 2.5.35 | Release |
-| Windows Server 2016       | VS 2017      | 3.17.2 | 4.8.8 | -     | 3.3.2 | 2.6.4  | Release |
+#### CI Environments
+
+| OS                        | Compiler     | CMake  | z3    | Bison | Flex   | Build   |
+| ------------------------- | ------------ | ------ | ----- | ----- | ------ | ------- |
+| Ubuntu 16.04 (Xenial)     | clang 7.0.0  | 3.12.4 | 4.4.1 | 3.0.4 | 2.6.0  | Debug   |
+| Ubuntu 16.04 (Xenial)     | gcc 7.5.0    | 3.12.4 | 4.4.1 | 3.0.4 | 2.6.0  | Debug   |
+| Ubuntu 16.04 (Xenial)     | gcc 7.5.0    | 3.17.0 | 4.4.1 | 3.0.4 | 2.6.0  | Release |
+| Ubuntu 18.04 (Bionic)     | clang 6.0.0  | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4  | Debug   |
+| Ubuntu 18.04 (Bionic)     | gcc 7.5.0    | 3.10.2 | 4.4.1 | 3.0.4 | 2.6.4  | Debug   |
+| Ubuntu 18.04 (Bionic)     | gcc 7.5.0    | 3.17.0 | 4.4.1 | 3.0.4 | 2.6.4  | Release |
+| Ubuntu 20.04 (Focal Fosa) | gcc 7.4.0    | 3.17.0 | 4.4.1 | 3.0.4 | 2.6.4  | Release |
+| OSX 10.15.4 (Catalina)    | Xcode 11.4.1 | 3.17.2 | 4.8.8 | 3.6.2 | 2.5.35 | Debug   |
+| OSX 10.15.4 (Catalina)    | Xcode 11.4.1 | 3.17.2 | 4.8.8 | 3.6.2 | 2.5.35 | Release |
+| Windows Server 2016       | VS 2017      | 3.17.2 | 4.8.8 | 3.3.2 | 2.6.4  | Release |
 
 ### Default Build
 

azure-pipelines.yml

@@ -70,7 +70,7 @@ jobs:
   - script: |
       mkdir -p build 
       cd build
-      cmake .. -DCMAKE_BUILD_TYPE=Release -DILANG_BUILD_SYNTH=ON
+      cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_COMPILER=g++-7
       cmake --build .
       sudo cmake --build . --target install 
       cmake --build . --target test
@@ -91,7 +91,7 @@ jobs:
   - script: |
       mkdir -p build
       cd build
-      cmake .. -DCMAKE_BUILD_TYPE=Release -DILANG_BUILD_SYNTH=ON
+      cmake .. -DCMAKE_BUILD_TYPE=Release
       cmake --build .
       sudo cmake --build . --target install 
       cmake --build . --target test

include/ilang/ilang++.h

@@ -112,6 +112,8 @@ class ExprRef {
   int addr_width() const;
   /// Return the data bit-width if is memory; return -1 otherwise.
   int data_width() const;
+  /// Return the expression name as std::string.
+  std::string name() const;
 
   // ------------------------- METHODS -------------------------------------- //
   /****************************************************************************/
@@ -393,6 +395,10 @@ class FuncRef {
   /// Default destructor.
   ~FuncRef();
 
+  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
+  /// Return the function name as std::string.
+  std::string name() const;
+
   // ------------------------- METHODS -------------------------------------- //
   /// Apply the function with no argument.
   ExprRef operator()() const;
@@ -461,6 +467,9 @@ class InstrRef {
   /// Return the wrapped ILA pointer.
   inline InstrPtr get() const { return ptr_; }
 
+  /// Return the instruction name as std::string.
+  std::string name() const;
+
 }; // class InstrRef
 
 /// \brief The wrapper of InstrLvlAbs (ILA).
@@ -523,11 +532,6 @@ class Ila {
   /// \param[in] name child-ILA name.
   Ila NewChild(const std::string& name);
 
-  // ------------------------- GENERATORS --------------------------------- //
-  /// \brief Export an ILA as Verilog
-  /// \param[in] fout the output stream of the generated Verilog source.
-  void ExportToVerilog(std::ostream& fout) const;
-
   // ------------------------- ACCESSORS/MUTATORS --------------------------- //
   /// Return the number of input variables.
   size_t input_num() const;
@@ -570,6 +574,15 @@ class Ila {
   /// Return the wrapped ILA pointer.
   inline IlaPtr get() const { return ptr_; }
 
+  // ------------------------- UTILITIES ------------------------------------ //
+  /// \brief Export an ILA as Verilog
+  /// \param[in] fout the output stream of the generated Verilog source.
+  void ExportToVerilog(std::ostream& fout) const;
+
+  /// \brief Flatten the hierarchy by lifting child-instructions as the
+  /// top-level parent instructions.
+  void FlattenHierarchy();
+
 }; // class Ila
 
 /******************************************************************************/
@@ -608,6 +621,9 @@ Ila ImportSynthAbstraction(const std::string& file_name,
 void ImportChildSynthAbstraction(const std::string& file_name, Ila& parent,
                                  const std::string& ila_name);
 
+/// \brief Generate the SystemC simulator.
+void ExportSysCSim(const Ila& ila, const std::string& dir_path);
+
 /******************************************************************************/
 // Verification.
 /******************************************************************************/
@@ -654,6 +670,12 @@ class IlaZ3Unroller {
   z3::expr UnrollPathConn(const std::vector<InstrRef>& path,
                           const int& init = 0);
 
+  /// \brief Unroll a path with each step connected with rewriting.
+  /// \param[in] path the sequence of instructions.
+  /// \param[in] init the starting time frame.
+  z3::expr UnrollPathSubs(const std::vector<InstrRef>& path,
+                          const int& init = 0);
+
   /// \brief Unroll a path with each step freely defined.
   /// \param[in] path the sequence of instructions.
   /// \param[in] init the starting time frame.