Menu ▾ ▴

Home

Marek Trtík

Bugst

Bugst is a collection of C++ libraries whose main goal is to shorten development time of experimental tools which are necessary for evaluation of a new program analysis method. Bugst is therefore targeted to students and researchers to support their research by quick development of experiments.

The second important goal of Bugst is improving scalability of its libraries to programs used in practice, since experiments performed on such programs usually give solid experimental evidence of practical usability of the evaluated method.

Instalation

Availability

Bugst is completely free software project. It means that we put no restrictions to usage of a content downloaded from Bugst's repository. In the same time we take no responsibily in consequences caused by the usage of the downloaded content. We emphasise that one can freely read, download, modify, share, distribute, or sell any part of Bugst and freely include any original or modified part of Bugst to any software project.

Build Environment and Software Dependences

Bugst is supposed to be built on a computer with:

  • Linux or MS Windows operating system. The main development platforms are Ubuntu and Linux Mint.
  • Git distributed version control system. It is required to download Bugst from the repository at SourceForge. We recommend to install also git client SmartGit.
  • CMake build system. A minimal supported version is 2.8.
  • A C++ compiler supproting the ISO standard from 12 August 2011 (i.e. C++11). A recommended compiler on Linux platform is GCC version 4.8.2 or newer. On MS Windows the recommended compiler is the one of MS Visual Studio 2012 or newer. Note though that .vcproj and .sln files appearing in the repository of Bugst are obsolete. Use CMake to generate project files.
  • Python 2.7 or newer.
  • boost C++ Libraries A minimal supported version is 1.57. Boost is the common dependece for almost all libraries in Bugst. A user should build at least the following Boost's libraries: system, thread, chrono, filesystem, log, log_setup, and program_options.
  • Z3 theorem prover. It is required for building Bugst's library Fol. Source code and built libraries are required. The tool's binary is not enough.
  • Optional: The LLVM Compiler Infrastructure A minimal supported version is 3.5. It is required for building Bugst's library LlvmUtl and tools llvm2celllvm and celllvm2lonka. Source code and libraries are required. We highly recommend to install this package, since LLVM is a default front-end for Bugst. Without it you will have to write Lonka files (a program representation in Bugst) by hand, which is VERY tedious work.
  • Optional: CLANG C front-end for LLVM. Only its binary is required, i.e. no source code, no libraries. Bugst supports automatic translation from C programs to Lonka, using CLANG and LLVM tools. Therefore, we highly recommend install both CLANG and LLVM optional packages.
  • Optional: Redis advanced key-value cache and store and its client HIREDIS. These packages enable portfolio approach for calls to SMT solvers, see branch portfolio_approach.
  • Optional: ANTLR parser generator. It is required only for the tool atomic-C of bugst.
  • Optional: QT Creator is a recommended development IDE on both platforms (Linux and MS WIndows). It is not mandatory though. In case you decide to use it, make sure that it is equiped with CMake plugin.

Building Bugst

Here we assume that all required software (see the previous section) is installed on user's computer.

1. Clone Bugst's repository

Create a new empty directory, say bugst_repo, somewhere on the disc. Open your terminal and navigate into that directory. Then type the following command:

git clone git://git.code.sf.net/p/bugst/src .

Do not forget to include the space and the character '.' at the end of the command.

2. Building Bugst using CMake GUI

a. Start the CMake GUI application.

b. In the edit-box in the very top type the path to your bugst_repo directory.

c. Into the edit box bellow it type a path where build scripts will be stored. Typically, you specify a subdirectory build of the bugst_repo directory. If you do not created this directory yet, the CMake will later ask you whether it should create the directory for you or not. Then choose 'yes'.

d. Push the button Configure. After that CMake allows you to target choose build system (and perhaps also compliler). On Linux platform we recomend Unix Makefiles and GCC and on Windows we recomend both project files and compiler of MS Visual Studio. When the CMake finishes its work a list box above the button is filled in with several variables. Check values of the variables and fix wrong ones. The following variables are epsecially important:

  • CMAKE_BUILD_TYPE A kind of build you are interested in. Available values are: Debug, Release, RelWithDebInfo.
  • BOOST_ROOT A path to the installation directory of Boost libraries.
  • Z3_ROOT A path to the installation directory of Z3 solver.
  • LLVM_ROOT A path to the installation directory of LLVM. Note that another variable LLVM_DIR is not important. Do not modify it.
  • HREDIS_ROOT A path to the installation directory of HREDIS client.
  • ANTLR_ROOT A path to the installation directory of ANTLR parser generator.

e. Keep pushing the button Configure until no line in the list box above it is red. It usually requires two pushes. In case some lines remain red, then you have to fix their values as they are very likely wrong.

f. Once no line in the list box is red, then push the button Generate. Now you can close CMake GUI aplication, since all build scripts were generated into your build directory, i.e. typically into build_repo/build.

g. Open terminal and navigate into the build directory, e.g. into build_repo/build. Then run the build scripts. This step depends on what target build system you have chosen. In case of Unix Makefiles type:

make install

In case of project files of MS Visual Studio simply start the studio and open the solution file located in the build directory.

In all cases, when building finishes, all resulting binaries can be found in the subdirectory dist of the bugst_repo directory.

3. Building Bugst in QT Creator

This is an alternative building process to the one described above. This process is better for development.

a. Start QT Creator IDE.

b. Use Open File or Project menu option to open the file bugst_repo/CMakeLists.txt in the IDE.

c. Push Projects button on the left horizontal bar in order to swicht to the tab with project settings. There in Edit build configuration: clone the default configuration and choose a proper name for it - according to the kind of build, i.e. Debug, Release, or RelWithDebInfo.

d. Specify build directory, e.g. build_repo/build.

e. Specify CMake arguments:
- -DCMAKE_BUILD_TYPE=<build-type></build-type> Possible values are Debug, Release, RelWithDebInfo.
- -DBOOST_ROOT=<path-to-boost></path-to-boost>
- -DZ3_ROOT=<path-to-z3></path-to-z3>
- -DLLVM_ROOT=<path-to-llvm></path-to-llvm>
- -DHREDIS_ROOT=<path-to-hredis></path-to-hredis>
- -DANTLR_ROOT=<path-to-antlr></path-to-antlr>

Of course, not all variables are necessary - some dependances are optional.

Using Bugst

TODO!

Stucture of Bugst

Organisation of source code

Source code of all libraries is located in code/bugst directory. In particular, sources of each library, say X, are located in code/bugst/X directory. Organisation of files and directories inside code/bugst/X is defined by authors/maintainers of the library X.

Similarly, source code of all tools is located in code/bugst/tools directory. In particular, sources of each tool, say X, are located in code/bugst/tools/X directory. Organisation of files and directories inside code/bugst/tools/X is defined by authors/maintainers of the library X.

Finally, source code of all tools is located in code/bugst/tests directory. In particular, sources of tests of each library, say X, are located in code/bugst/tests/XTst directory, where the suffix 'Tst' is not mandatory, it is only recommended. Organisation of files and directories inside code/bugst/tests/XTst is defined by authors/maintainers of tests of the library X.

Organisation of data files

All data files are located in data directory. Data of a particular library, say X, are located in data/X directory. Similarly, data of a tool X are in data/tools/X, and data of a test data/tests/XTst directory, where the suffix 'Tst' is not mandatory, it is only recommended. Organisation of files and directories inside directories of particular libraries, tools, and tests is defined by their authors/maintainers.

Data of a general usage (like common data for several libraries, tools, or tests) are located in data/X, where X is a name of the directory where the data are stored. The name X identifies the purpose of the data.

TODO: describe file 'install.bat'

Structure of output from build

Intermediate files produced during build process (like files with object code) are located inside build directory. This directory is automatically creaded during build. Organisation of directories inside build directory exactly matches organisation of sources in code/bugst directory described above. It may happen that Visual Studion creates ipch directory in the root directory of Bugst.

Resulting files from the build are stored into dist directory. Library files are stored directly to the dist directory. Tools are stored into directories dist/tools/X, where X is the name of a tool. Similarly, tests are stored into directories dist/tests/XTst, where X is the name of a test of a particular library. Again the suffix 'Tst' is not mandatory.

TODO: describe installed data files (from 'install.bat')

Directory Sketches

Two ZIP files in the directory contain implementations of two program analyses in very limited setting. The implementations are completely independent to Bugst (they were created before Bugst). But we plan to reimplement these analyses in Bugst. When this happens, we remove the ZIP files and also whole the directory Sketches from the repository.

Getting Started

Libraries

  • lonka Internal control-flow graph based program representation.
  • fol Symbolic expressions, first-order logic formulae, and algorithms on then.
  • segy Symbolic memory supporting pointers and pointer arithmetic.
  • symtex Classic symbolic execution
  • cosymtex Compact symbolic execution
  • llvmutl High-level functions for easy access to LLVM program.
  • utils Bugst configuration, time profiler.
  • shanon Obsolete library, it will be removed.

Tools

  • llvm2celllvm Translates LLVM code to constant expression less LLVM code.
  • celllvm2lonka Translates constant expression less LLVM code to Lonka program.
  • lonkator Allows to dump individual flowgraphs of a given Lonka program in .dot and .pdf format.
  • rudla Classic and compact symbolic execution tool.

Participation

Are you interested in Bugst? Would you like to use it for implementation of your program analysis and moreover would you like to provide your implementation to other people? If so, then contact an administrator of Bugst (listed below) to get write and create access to Bugst's repository here at Sourceforge.

We also appreciate any form of feedback (especially bug-reports) related to your experience with Bugst.

Project Admins: