Merge branch 'master' of github.com:Bo-Yuan-Huang/ILA-Tools into cove…

…r-up

.github/ISSUE_TEMPLATE/bug_report.md

@@ -1,4 +1,5 @@
 ---
+
 name: Bug report
 about: Create a report to help us improve
 
@@ -11,25 +12,19 @@ A clear and concise description of what the bug is.
 Steps to reproduce the behavior:
 1. Go to '...'
 2. Click on '....'
-3. Scroll down to '....'
-4. See error
+3. See error
 
 **Expected behavior**
 A clear and concise description of what you expected to happen.
 
 **Screenshots**
 If applicable, add screenshots to help explain your problem.
 
-**Desktop (please complete the following information):**
- - OS: [e.g. iOS]
- - Browser [e.g. chrome, safari]
- - Version [e.g. 22]
+**Environment (please complete the following information):**
 
-**Smartphone (please complete the following information):**
- - Device: [e.g. iPhone6]
- - OS: [e.g. iOS8.1]
- - Browser [e.g. stock browser, safari]
- - Version [e.g. 22]
+-   OS: [e.g. Ubuntu 18.04]
+-   Compiler [e.g. gcc 7.3.0, clang 6.0.0]
+-   Other dependencies [e.g. z3 4.4.1, boost 1.65.0]
 
 **Additional context**
 Add any other context about the problem here.

.github/ISSUE_TEMPLATE/feature_request.md

@@ -1,4 +1,5 @@
 ---
+
 name: Feature request
 about: Suggest an idea for this project
 

.gitmodules

@@ -1,6 +1,3 @@
-[submodule "examples/RISC-V/simulator"]
-	path = examples/RISC-V/simulator
-	url = https://github.com/zhanghongce/riscv-ila-sim.git
 [submodule "extern/glog"]
 	path = extern/glog
 	url = https://github.com/google/glog.git

.lgtm.yml

@@ -0,0 +1,38 @@
+path_classifiers:
+  test:
+    - tests
+
+  external:
+    - extern
+
+  docs:
+    - docs
+
+  script:
+    - scripts
+
+  example:
+    - apps
+    - examples
+
+extraction:
+  cpp:
+    prepare:
+      packages:
+        - build-essential
+        - libboost-all-dev
+        - bison
+        - flex
+        - z3
+        - libz3-dev
+
+    configure:
+      command:
+        - mkdir -p build
+        - cd build
+        - cmake ..
+
+    index:
+      build_command:
+        - cd build # cwd is set to LGTM_SRC at the start of each build step
+        - make -j$(nproc)

.travis.yml

@@ -2,6 +2,7 @@ branches:
   only:
     - master
     - travis
+    - pre-release
 
 git:
   depth: 1
@@ -11,6 +12,10 @@ sudo: required
 
 language: cpp
 
+cache:
+  directories:
+    - $HOME/_cache
+
 matrix:
   include:
     - name: "linux-gcc"
@@ -21,9 +26,9 @@ matrix:
         - gem install coveralls-lcov
       before_script:
         - mkdir -p $TRAVIS_BUILD_DIR/build 
-        - source $TRAVIS_BUILD_DIR/scripts/clean-coverage.sh $TRAVIS_BUILD_DIR/build
+        - source $TRAVIS_BUILD_DIR/scripts/travis/clean-coverage.sh $TRAVIS_BUILD_DIR/build 
       after_success:
-        - source $TRAVIS_BUILD_DIR/scripts/submit-coverage.sh $TRAVIS_BUILD_DIR/build
+        - source $TRAVIS_BUILD_DIR/scripts/travis/submit-coverage.sh $TRAVIS_BUILD_DIR/build 
 
     - name: "linux-clang"
       os: linux
@@ -44,17 +49,28 @@ matrix:
             - flex
             - bison
             - libboost-all-dev
+            - z3
+            - libz3-dev
       env:
         - MATRIX_EVAL="CC=gcc-4.9 && CXX=g++-4.9"
       before_install:
         - eval "${MATRIX_EVAL}"
 
     - 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"
+      #before_install:
+        #- brew install bison
+        #- export PATH="/usr/local/opt/bison/bin:$PATH"
+        #- export LDFLAGS="-L/usr/local/opt/bison/lib"
+      install:
+        - export BISON_CACHED="$(find $HOME/_cache -name bison | grep -c "bison")"
+        - if [ $BISON_CACHED == "0" ] ; then mkdir -p $HOME/_cache/bison ; fi 
+        - if [ $BISON_CACHED == "0" ] ; then wget http://ftp.gnu.org/gnu/bison/bison-3.2.4.tar.gz ; fi 
+        - if [ $BISON_CACHED == "0" ] ; then tar zxvf bison-3.2.4.tar.gz -C $HOME/_cache/bison --strip-components 1 ; fi 
+        - cd $HOME/_cache/bison
+        - if [ $BISON_CACHED == "0" ] ; then ./configure ; fi
+        - if [ $BISON_CACHED == "0" ] ; then make ; fi
+        - sudo make install
 
 addons:
   apt:
@@ -64,32 +80,16 @@ addons:
       - flex
       - bison
       - libboost-all-dev
+      - z3
+      - libz3-dev
   homebrew:
     update: true
     packages:
       - flex
       - python
       - boost
       - boost-python
-
-cache:
-  directories:
-    - $HOME/_cache
-
-install: 
-  - mkdir -p $HOME/_cache
-  - export Z3_CACHED="$(find $HOME/_cache/ -name z3 | grep -c "z3")"
-  - cd $HOME/_cache
-  - if [[ "$Z3_CACHED" == "0" ]] ; then git clone https://github.com/Z3Prover/z3.git ; fi
-  - cd z3
-  - if [[ "$Z3_CACHED" == "0" ]] ; then git checkout tags/z3-4.8.4 -b v484 ; fi
-  - if [[ "$Z3_CACHED" == "0" ]] ; then python scripts/mk_make.py ; fi
-  - if [[ "$Z3_CACHED" == "0" && "$TRAVIS_COMPILER" == "clang" ]] ; then CXX=clang++ CC=clang python scripts/mk_make.py ; fi
-  - cd build
-  - if [[ "$Z3_CACHED" == "0" ]] ; then make -j$(nproc) ; fi
-  - sudo make install
-  - which z3
-  - z3 --version
+      - z3
 
 script:
   - cd $TRAVIS_BUILD_DIR

CMakeLists.txt

@@ -11,7 +11,7 @@ endif()
 # PROJECT
 # name version language
 # ---------------------------------------------------------------------------- #
-project(ilang VERSION     1.0.0
+project(ilang VERSION     0.9.0
               LANGUAGES   CXX
 )
 

LICENSE

@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2017
+Copyright (c) 2019
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

README.md

@@ -1,13 +1,16 @@
-<img src="https://raw.githubusercontent.com/Bo-Yuan-Huang/ILAng/master/docs/pics/ilang-logo.png" alt="ILAng Logo" height="225"/>
+[![ILAng](https://raw.githubusercontent.com/Bo-Yuan-Huang/ILAng/master/docs/pics/ilang-logo.png)](https://bo-yuan-huang.gitbook.io/ilang/)
 
 [![Build Status](https://travis-ci.org/Bo-Yuan-Huang/ILAng.svg?branch=master)](https://travis-ci.org/Bo-Yuan-Huang/ILAng)
 [![Build Status](https://semaphoreci.com/api/v1/bo-yuan-huang/ilang/branches/master/shields_badge.svg)](https://semaphoreci.com/bo-yuan-huang/ilang)
 [![Build status](https://ci.appveyor.com/api/projects/status/cwhlq09513art6hw/branch/master?svg=true)](https://ci.appveyor.com/project/Bo-Yuan-Huang/ilang/branch/master)
 [![Coverage Status](https://coveralls.io/repos/github/Bo-Yuan-Huang/ILAng/badge.svg?branch=master)](https://coveralls.io/github/Bo-Yuan-Huang/ILAng?branch=master)
 [![Codacy Badge](https://api.codacy.com/project/badge/Grade/b120e2527cc04d4aacd1dc11581e2f30)](https://www.codacy.com/app/Bo-Yuan-Huang/ILAng?utm_source=github.com&utm_medium=referral&utm_content=Bo-Yuan-Huang/ILAng&utm_campaign=Badge_Grade)
+[![Language grade: C/C++](https://img.shields.io/lgtm/grade/cpp/g/Bo-Yuan-Huang/ILAng.svg?logo=lgtm&logoWidth=18)](https://lgtm.com/projects/g/Bo-Yuan-Huang/ILAng/context:cpp)
 [![Percentage of issues still open](http://isitmaintained.com/badge/open/bo-yuan-huang/ilang.svg)](http://isitmaintained.com/project/bo-yuan-huang/ilang "Percentage of issues still open")
-[![Average time to resolve an issue](http://isitmaintained.com/badge/resolution/bo-yuan-huang/ilang.svg)](http://isitmaintained.com/project/bo-yuan-huang/ilang "Average time to resolve an issue")
-[![license](https://img.shields.io/github/license/mashape/apistatus.svg)](https://github.com/Bo-Yuan-Huang/ILA-Tools/blob/master/LICENSE)
+[![license](https://img.shields.io/github/license/bo-yuan-huang/ilang.svg?style=flat)](https://github.com/Bo-Yuan-Huang/ILA-Tools/blob/master/LICENSE)
+[![Documentation](https://img.shields.io/badge/docs-manual-blue.svg)](https://bo-yuan-huang.gitbook.io/ilang/)
+[![Documentation](https://img.shields.io/badge/docs-doxygen-blue.svg)](https://bo-yuan-huang.github.io/ILAng-Doc/doxygen-output-html/namespaceilang.html)
+[![docker](https://images.microbadger.com/badges/image/byhuang/ilang.svg)](https://hub.docker.com/r/byhuang/ilang)
 
 -   [Build](#build)
     -   [Prerequisites](#prerequisites)
@@ -19,56 +22,37 @@
     -   [Embedded](#embedded)
     -   [Supporting Both](#supporting-both)
 
--   [Examples](#examples)
-    -   [Modeling](#modeling)
-    -   [Verification Target Generation](#verification-target-generation)
-
--   [Download](#download)
-
--   [Documentations](#documentations)
+-   [Docker](#docker-image)
 
 ## Build
 
 ### Prerequisites
 
 ILAng requires CMake (3.8 or above) and compilers with CXX11 support.
-To install dependencies on Debian-based UNIX, execute:
+To install dependencies on Debian-based UNIX:
 
 ```bash
-apt-get install bison flex libboost-all-dev 
+apt-get install bison flex libboost-all-dev z3 libz3-dev
 ```
 
-For OSX, execute:
+To install dependencies on OSX:
 
 ```bash
-brew install bison flex boost boost-python
+brew install bison flex boost boost-python z3
 ```
 
-Note that the [Boost](https://www.boost.org) package is required only for building the synthesis engine and the Python API. 
-
-#### z3
-
-The [z3](https://github.com/Z3Prover/z3) SMT solver is required (including lib and header). 
-Detailed instructions for building z3 can be found [here](https://github.com/Z3Prover/z3).
-
-```bash
-git clone https://github.com/Z3Prover/z3.git
-cd z3
-python scripts/mk_make.py
-cd build
-make -j$(nproc)
-sudo make install
-```
+-   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 for building the synthesis engine and the Python API. 
 
 #### Tested Environments
 
-| OS                        | Compiler    | CMake  | z3     | Boost | Status                                                                                                                                                                        |
-| ------------------------- | ----------- | ------ | ------ | ----- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
-| Ubuntu 14.04 (Trusty)     | gcc 4.8.4   | 3.8.0  | 4.7.1  | 1.54  | [![Build Status](https://semaphoreci.com/api/v1/bo-yuan-huang/ilang/branches/master/shields_badge.svg)](https://semaphoreci.com/bo-yuan-huang/ilang)                          |
-| Ubuntu 16.04 (Xenial)     | gcc 5.4.0   | 3.12.4 | 4.8.4  | 1.58  | [![Build Status](https://travis-ci.org/Bo-Yuan-Huang/ILAng.svg?branch=master)](https://travis-ci.org/Bo-Yuan-Huang/ILAng)                                                     |
-| Ubuntu 16.04 (Xenial)     | clang 7.0.0 | 3.12.4 | 4.8.4  | 1.58  | [![Build Status](https://travis-ci.org/Bo-Yuan-Huang/ILAng.svg?branch=master)](https://travis-ci.org/Bo-Yuan-Huang/ILAng)                                                     |
-| Ubuntu 18.04 (Bionic)     | gcc 7.3.0   | 3.13.1 | latest | 1.65  | [![Build status](https://ci.appveyor.com/api/projects/status/4jsh32isd8r89g3l/branch/master?svg=true)](https://ci.appveyor.com/project/Bo-Yuan-Huang/ila-tools/branch/master) |
-| OSX 10.13.0 (High Sierra) | Xcode 9.4.1 | 3.11.4 | 4.8.4  | 1.68  | [![Build Status](https://travis-ci.org/Bo-Yuan-Huang/ILAng.svg?branch=master)](https://travis-ci.org/Bo-Yuan-Huang/ILAng)                                                     |
+| OS                        | Compiler    | CMake  | z3     | Boost | Status                                                                                                                                                                    |
+| ------------------------- | ----------- | ------ | ------ | ----- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
+| Ubuntu 14.04 (Trusty)     | gcc 4.8.4   | 3.8.0  | 4.7.1  | 1.54  | [![Build Status](https://semaphoreci.com/api/v1/bo-yuan-huang/ilang/branches/master/shields_badge.svg)](https://semaphoreci.com/bo-yuan-huang/ilang)                      |
+| Ubuntu 16.04 (Xenial)     | gcc 5.4.0   | 3.12.4 | 4.4.1  | 1.58  | [![Build Status](https://travis-ci.org/Bo-Yuan-Huang/ILAng.svg?branch=master)](https://travis-ci.org/Bo-Yuan-Huang/ILAng)                                                 |
+| Ubuntu 16.04 (Xenial)     | clang 7.0.0 | 3.12.4 | 4.4.1  | 1.58  | [![Build Status](https://travis-ci.org/Bo-Yuan-Huang/ILAng.svg?branch=master)](https://travis-ci.org/Bo-Yuan-Huang/ILAng)                                                 |
+| Ubuntu 18.04 (Bionic)     | gcc 7.3.0   | 3.13.1 | latest | 1.65  | [![Build status](https://ci.appveyor.com/api/projects/status/cwhlq09513art6hw/branch/master?svg=true)](https://ci.appveyor.com/project/Bo-Yuan-Huang/ilang/branch/master) |
+| OSX 10.13.0 (High Sierra) | Xcode 9.4.1 | 3.11.4 | 4.8.4  | 1.68  | [![Build Status](https://travis-ci.org/Bo-Yuan-Huang/ILAng.svg?branch=master)](https://travis-ci.org/Bo-Yuan-Huang/ILAng)                                                 |
 
 ### Default Build
 
@@ -167,15 +151,13 @@ endif()
 
 `externals/ilang` is then a complete copy of this source tree, if enabled.
 
-## Examples
-
-### Modeling
+## Docker Image
 
-### Verification Target Generation
+[![docker-io](http://dockeri.co/image/byhuang/ilang)](https://hub.docker.com/r/byhuang/ilang)
+[![docker-image](https://images.microbadger.com/badges/image/byhuang/ilang.svg)](https://microbadger.com/images/byhuang/ilang "Get your own image badge on microbadger.com")
+[![docker-version](https://images.microbadger.com/badges/version/byhuang/ilang.svg)](https://microbadger.com/images/byhuang/ilang "Get your own version badge on microbadger.com")
 
-## Download
-
-An docker image with the ILAng platform and all dependencies can be fetched from [Docker Hub](https://cloud.docker.com/u/byhuang/repository/docker/byhuang/ilang).
+An docker image with the ILAng platform and all dependencies can be fetched from [Docker Hub](https://hub.docker.com/r/byhuang/ilang).
 
 ```bash
 docker pull byhuang/ilang:latest
@@ -189,8 +171,3 @@ source init.sh
 
 to initialize the environment settings. 
 This docker image also contains the model checker [CoSA](https://github.com/cristian-mattarei/CoSA) with the SMT solvers [z3](https://github.com/Z3Prover/z3) and [Boolector](https://github.com/Boolector/boolector).
-
-## Documentations
-
--   A list of related papers can be found in the [ILAng main page](https://bo-yuan-huang.github.io/ILAng/).
--   Link to the C++ implementation annotation (powered by Doxygen). \[[LINK](https://bo-yuan-huang.github.io/ILAng/doxygen-html/namespaceilang.html)]