Merge pull request #187 from Bo-Yuan-Huang/cxx17

Cxx17

.semaphore/semaphore.yml

@@ -19,7 +19,7 @@ blocks:
             - export CXX=g++-7
             - mkdir build
             - cd build
-            - cmake .. -DCMAKE_BUILD_TYPE=Debug
+            - cmake .. -DCMAKE_BUILD_TYPE=Debug -DILANG_BUILD_SYNTH=ON
             - make -j$(nproc)
             - sudo make install
             - make run_test

.travis.yml

@@ -37,24 +37,6 @@ matrix:
       after_success:
         - source $TRAVIS_BUILD_DIR/scripts/travis/submit-coverage.sh $TRAVIS_BUILD_DIR/build
 
-    - name: "linux-clang"
-      os: linux
-      dist: xenial
-      compiler: clang
-      before_install:
-        - export LD_LIBRARY_PATH=/usr/local/clang/lib:$LD_LIBRARY_PATH
-      script:
-        - source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR
-
-    - name: "osx"
-      os: osx
-      before_install:
-        - brew install bison
-        - export PATH="/usr/local/opt/bison/bin:$PATH"
-        - export LDFLAGS="-L/usr/local/opt/bison/lib"
-      script:
-        - source $TRAVIS_BUILD_DIR/scripts/travis/build-osx.sh $TRAVIS_BUILD_DIR
-
     - name: "coverity"
       os: linux
       dist: xenial
@@ -73,7 +55,6 @@ matrix:
           packages:
             - flex
             - bison
-            - libboost-all-dev
             - z3
             - libz3-dev
       before_install:
@@ -93,14 +74,6 @@ addons:
       - libboost-all-dev
       - z3
       - libz3-dev
-  homebrew:
-    update: true
-    packages:
-      - flex
-      - python
-      - boost
-      - boost-python
-      - z3
 
 notifications:
     email: false

CMakeLists.txt

@@ -11,7 +11,7 @@ endif()
 # PROJECT
 # name version language
 # ---------------------------------------------------------------------------- #
-project(ilang VERSION     1.0.3
+project(ilang VERSION     1.0.4
               LANGUAGES   CXX
 )
 
@@ -22,7 +22,7 @@ project(ilang VERSION     1.0.3
 # ---------------------------------------------------------------------------- #
 option(ILANG_FETCH_DEPS  "Fetch source of dependencies at config time."      ON)
 option(ILANG_BUILD_DOCS  "Build documentations."                            OFF)
-option(ILANG_BUILD_SYNTH "Build the synthesis engine."                       ON)
+option(ILANG_BUILD_SYNTH "Build the synthesis engine."                      OFF)
 option(ILANG_INSTALL_DEV "Install dev features."                            OFF)
 option(ILANG_EXPORT_PACKAGE "Export CMake package if enabled."              OFF)
 option(ILANG_COVERITY    "Build for Coverity static analysis."              OFF)

README.md

@@ -33,7 +33,7 @@
 
 ### Prerequisites
 
-ILAng requires CMake (3.9.6 or above) and compilers with CXX11 support.
+ILAng requires CMake (3.9.6 or above) and compilers with C++17 support.
 To install dependencies on Debian-based Linux:
 
 ```bash
@@ -53,7 +53,7 @@ brew install bison flex boost boost-python 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.
+-   The [Boost](https://www.boost.org) package is required only if you want to build the synthesis engine (default `OFF`).
 
 #### Regression Environments
 
@@ -62,12 +62,12 @@ brew install bison flex boost boost-python z3
 | 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 | 1.65  | 3.0.4 | 2.6.4  | Release |
-| OSX 10.13.6 (High Sierra) | Xcode 9.4.1  | 3.15.5 | 4.8.8 | 1.72  | 3.6.2 | 2.5.35 | Release |
-| OSX 10.14.6 (Mojave)      | Xcode 11.3.1 | 3.17.2 | 4.8.8 | 1.72  | 3.6.2 | 2.5.35 | Release |
-| OSX 10.15.4 (Catalina)    | Xcode 11.4.1 | 3.17.2 | 4.8.8 | 1.72  | 3.6.2 | 2.5.35 | 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
@@ -99,8 +99,8 @@ sudo make install
 
 -   Use `-DILANG_FETCH_DEPS=OFF` to disable config-time updating submodules for in-source dependencies.
 -   Use `-DILANG_BUILD_TEST=OFF` to disalbe building the unit tests.
--   Use `-DILANG_BUILD_SYNTH=OFF` to disable building the synthesis engine. 
--   Use `-DILANG_BUILD_INVSYN=ON` to enable building invariant synthesis feature.
+-   Use `-DILANG_BUILD_SYNTH=ON` to enable building the synthesis engine. 
+-   Use `-DILANG_BUILD_INVSYN=OFF` to disable building invariant synthesis feature.
 -   Use `-DILANG_BUILD_SWITCH=ON` to enable building [smt-switch](https://github.com/makaimann/smt-switch.git) interface support. 
 -   Use `-DILANG_INSTALL_DEV=ON` to install working features. 
 

appveyor.yml

@@ -0,0 +1,17 @@
+version: 1.0.{build}
+image: Ubuntu2004
+clone_depth: 1
+
+install:
+- sudo apt update --yes
+- sudo apt install --yes z3 libz3-dev bison flex gcc g++
+
+build_script:
+- cd $APPVEYOR_BUILD_FOLDER
+- mkdir -p build
+- cd build
+- cmake .. -DCMAKE_BUILD_TYPE=Release
+- make -j$(nproc)
+- sudo make install
+- make test
+- cmake --version

azure-pipelines.yml

@@ -7,15 +7,13 @@ pr:
 - master
 
 jobs:
-- job: macOS_Mojave
+- job: macOS_Catalina_Debug
   pool:
-    vmImage: 'macOS-10.14'
+    vmImage: 'macOS-10.15'
   steps:
   - script: |
       brew update
       brew install bison
-      brew install boost
-      brew install boost-python
       brew install z3
     displayName: 'package'
   - script: |
@@ -27,21 +25,19 @@ jobs:
       export LDFLAGS="-L/usr/local/opt/bison/lib"
       mkdir -p build
       cd build
-      cmake .. -DCMAKE_BUILD_TYPE=Release -DBoost_NO_BOOST_CMAKE=ON -DILANG_BUILD_INVSYN=OFF
+      cmake .. -DCMAKE_BUILD_TYPE=Debug
       cmake --build .
       cmake --build . --target install
       cmake --build . --target test
     displayName: 'build'
 
-- job: macOS_Catalina
+- job: macOS_Catalina_Release
   pool:
     vmImage: 'macOS-10.15'
   steps:
   - script: |
       brew update
       brew install bison
-      brew install boost
-      brew install boost-python
       brew install z3
     displayName: 'package'
   - script: |
@@ -53,10 +49,10 @@ jobs:
       export LDFLAGS="-L/usr/local/opt/bison/lib"
       mkdir -p build
       cd build
-      cmake .. -DCMAKE_BUILD_TYPE=Release -DBoost_NO_BOOST_CMAKE=ON -DILANG_BUILD_INVSYN=OFF
+      cmake .. -DCMAKE_BUILD_TYPE=Release -DILANG_BUILD_INVSYN=OFF 
       cmake --build .
       cmake --build . --target install 
-      cmake --build . --target test
+      ./test/unit_tests
     displayName: 'build'
 
 - job: Ubuntu_1604_LTS
@@ -74,7 +70,7 @@ jobs:
   - script: |
       mkdir -p build 
       cd build
-      cmake .. -DCMAKE_BUILD_TYPE=Release
+      cmake .. -DCMAKE_BUILD_TYPE=Release -DILANG_BUILD_SYNTH=ON
       cmake --build .
       sudo cmake --build . --target install 
       cmake --build . --target test
@@ -95,7 +91,7 @@ jobs:
   - script: |
       mkdir -p build
       cd build
-      cmake .. -DCMAKE_BUILD_TYPE=Release
+      cmake .. -DCMAKE_BUILD_TYPE=Release -DILANG_BUILD_SYNTH=ON
       cmake --build .
       sudo cmake --build . --target install 
       cmake --build . --target test
@@ -148,7 +144,7 @@ jobs:
       md build
       cd build
       # For building the test, we need CMAKE_MSVC_RUNTIME_LIBRARY (which will be supported in CMake 3.15+)
-      cmake .. -DILANG_BUILD_SYNTH=OFF -DILANG_BUILD_TEST=OFF -DBUILD_SHARED_LIBS=OFF -DILANG_BUILD_INVSYN=OFF -DZ3_INCLUDE_DIR=$(Build.Repository.LocalPath)/z3/include -DZ3_LIBRARY=$(Build.Repository.LocalPath)/z3/bin/libz3.lib -DZ3_EXEC=$(Build.Repository.LocalPath)/z3/bin/z3.exe
+      cmake .. -DILANG_BUILD_TEST=OFF -DBUILD_SHARED_LIBS=OFF -DILANG_BUILD_INVSYN=OFF -DZ3_INCLUDE_DIR=$(Build.Repository.LocalPath)/z3/include -DZ3_LIBRARY=$(Build.Repository.LocalPath)/z3/bin/libz3.lib -DZ3_EXEC=$(Build.Repository.LocalPath)/z3/bin/z3.exe
       cmake --build .
       cmake --build . --target install
     displayName: 'build'

include/ilang/ila/instr_lvl_abs.h

@@ -235,16 +235,6 @@ class InstrLvlAbs : public Object,
   /// \param[in] valid_expr pointer to the valid function (as an expression).
   void ForceSetValid(const ExprPtr valid_expr);
 
-  /// \brief Sanity check for the ILA (e.g. sort marching).
-  /// \return True if check pass.
-  bool Check() const;
-
-  /// \brief Merge child-ILAs, including variables, simplifier, etc.
-  void MergeChild();
-
-  /// \brief Sort instructions based on the sequencing, if any.
-  void SortInstr();
-
   /// \brief Define instruction sequencing by adding a transition edge.
   /// \param[in] src source instruction
   /// \param[in] dst target instruction (destination)

include/ilang/util/fs.h

@@ -30,6 +30,9 @@ bool os_portable_move_file_to_dir(const std::string& src,
 /// Remove one file
 bool os_portable_remove_file(const std::string& file);
 
+/// Remove one directory
+bool os_portable_remove_directory(const std::string& dir);
+
 /// Append two paths
 std::string os_portable_append_dir(const std::string& dir1,
                                    const std::string& dir2);

scripts/travis/build.sh

@@ -38,7 +38,7 @@ sudo make install
 cd $CI_BUILD_DIR
 mkdir -p build
 cd build
-cmake .. -DCMAKE_BUILD_TYPE=Debug -DILANG_BUILD_COV=ON -DILANG_BUILD_SWITCH=ON
+cmake .. -DCMAKE_BUILD_TYPE=Debug -DILANG_BUILD_COV=ON -DILANG_BUILD_SWITCH=ON -DILANG_BUILD_SYNTH=ON
 make -j$(nproc)
 sudo make install
 make run_test

src/CMakeLists.txt

@@ -26,7 +26,7 @@ endif()
 ##
 ## compile features/options
 ##
-target_compile_features(${ILANG_LIB_NAME} PUBLIC cxx_std_11)
+target_compile_features(${ILANG_LIB_NAME} PUBLIC cxx_std_17)
 
 set_property(
   TARGET ${ILANG_LIB_NAME}
@@ -57,10 +57,20 @@ target_include_directories(${ILANG_LIB_NAME}
     $<BUILD_INTERFACE:${ILANG_INCLUDE_BUILD_DIR}>
 )
 
+# check if c++17 filesystem is available
+CHECK_INCLUDE_FILE_CXX(filesystem FS_INCLUDE)
+
 # ---------------------------------------------------------------------------- #
 # LINK LIBRARIES
 # external dependencies
 # ---------------------------------------------------------------------------- #
+##
+## std::filesystem
+##
+if(NOT APPLE)
+target_link_libraries(${ILANG_LIB_NAME} PRIVATE stdc++fs)
+endif()
+
 ##
 ## gcov 
 ##

src/config.h.in

@@ -24,5 +24,7 @@
 
 #cmakedefine SMTSWITCH_YICES2_FOUND
 
+#cmakedefine FS_INCLUDE
+
 #endif // CONFIG_CMAKE_DEFINE_H__
 

src/ila/instr_lvl_abs.cc

@@ -261,34 +261,6 @@ void InstrLvlAbs::ForceSetValid(const ExprPtr valid_expr) {
   valid_ = valid;
 }
 
-bool InstrLvlAbs::Check() const {
-  ILA_WARN << "Check in InstrLvlAbs not implemented.";
-  // TODO
-  // check input
-  // check state
-  // check init
-  // check fetch
-  // check valid
-  // check instr
-  // check child-ILA?
-  // check sequencing
-  return true;
-}
-
-void InstrLvlAbs::MergeChild() {
-  ILA_WARN << "MergeChild in InstrLvlAbs not implemented.";
-  // TODO
-  // merge shared states
-  // merge simplifier
-}
-
-void InstrLvlAbs::SortInstr() {
-  ILA_WARN << "SortInstr in InstrLvlAbs not implemented.";
-  // TODO
-  // check this is a micro-ILA and has sequencing
-  // sort instructions based on the sequencing
-}
-
 void InstrLvlAbs::AddSeqTran(const InstrPtr src, const InstrPtr dst,
                              const ExprPtr cnd) {
   // XXX src, dst should already registered.