• Build

  • Prerequisites
  • Default Build
  • Options

• CMake Integration

  • External
  • Embedded
  • Supporting Both

• Docker

ILAng requires CMake (3.8 or above) and compilers with CXX11 support. To install dependencies on Debian-based UNIX:

apt-get install bison flex libboost-all-dev z3 libz3-dev

To install dependencies on OSX:

brew install bison flex boost boost-python z3

• The z3 SMT solver (over 4.4.0) is required. Detailed instruction for building latest z3 can be found here.
• The Boost package is required only for building the synthesis engine and the Python API.

OS	Compiler	CMake	z3	Boost	Status
Ubuntu 14.04 (Trusty)	gcc 4.8.4	3.8.0	4.7.1	1.54
Ubuntu 16.04 (Xenial)	gcc 5.4.0	3.12.4	4.4.1	1.58
Ubuntu 16.04 (Xenial)	clang 7.0.0	3.12.4	4.4.1	1.58
Ubuntu 18.04 (Bionic)	gcc 7.3.0	3.13.1	latest	1.65
OSX 10.13.0 (High Sierra)	Xcode 9.4.1	3.11.4	4.8.4	1.68

To build ILAng with default configuration, create a build directory and execute:

mkdir -p build && cd build
cmake .. 
make -j$(nproc)

After the build complete, run unit tests and install the library.

make run_test
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_INSTALL_DEV=ON to enable installing working features.

You can use the ilang::ilang interface target in CMake. This target populates the appropriate usage requirements for include directories, linked libraries, and compile features. To use the ILAng library, ilang++.h is the file to include. (This does not include working features.)

// cxx source
#include <ilang/ilang++.h>

void foo () {
  auto m = ilang::Ila("new_ila_model");
}

To use the ILAng library from a CMake project, you can locate it directly with find_package() and use the namespaced imported target from the generated package configuration:

# CMakeLists.txt
find_package(ilang REQUIRED)
...
add_library(my_proj ...)
...
target_link_libraries(my_proj PRIVATE ilang::ilang)

ILAng also supports embedded build, but is not recommended due to its size. To embed the library directly into an existing CMake project, place the entire source tree in a subdirectory and call add_subdirectory() in your CMakeLists.txt file:

# CMakeLists.txt
add_subdirectory(ilang)
...
add_library(my_proj ...)
...
target_link_libraries(my_proj PRIVATE ilang::ilang)

To allow your project to support either an externally installed or an embedded library, you can use the following pattern:

# Top level CMakeLists.txt
project(MY_PROJ)
...
option(MY_PROJ_USE_EXTERNAL_ILANG "Use an external ILAng library" OFF)
...
add_subdirectory(externals)
...
add_library(my_proj ...)
...
target_link_libraries(my_proj PRIVATE ilang::ilang)

# externals/CMakeLists.txt
...
if(MY_PROJ_USE_EXTERNAL_ILANG)
  find_package(ilang REQUIRED)
else()
  add_subdirectory(ilang)
endif()
...

externals/ilang is then a complete copy of this source tree, if enabled.

An docker image with the ILAng platform and all dependencies can be fetched from Docker Hub.

docker pull byhuang/ilang:latest

Once the container is initiated, run

source init.sh

to initialize the environment settings. This docker image also contains the model checker CoSA with the SMT solvers z3 and Boolector.