The Automata Based Counter (ABC) is a string and numeric constriant solver and model counter. ABC provides solutions to systems of string and numeric constraints in the form of a deterministic finite automaton. In addition ABC produces symbolic representation of the number of strings and integers within a length bound, k, that satisfy a set of constraints. ABC can also output the number of satisfying solutions given a bound.
###ABC algorithmic details:
- A new publication is coming with improvements over CAV'15 version of ABC.
- CAV'15, Automata-based model counting for string constraints. Abdulbaki Aydin, Lucas Bang, and Tevfik Bultan.
Download experimental data and results.
###ABC use cases:
- FSE'16 String Analysis for Side Channels with Segmented Oracles. Lucas Bang, Abdulbaki Aydin, Quoc-Sang Phan, Corina S. Pasareanu, and Tevfik Bultan.
ABC is a C++ executable and a C++ shared library with JNI interfaces. You can use it as a static or dynamic lib or you can run it from command line.
###Download
$ cd <your home directory or a preferred directory>
$ git clone --recursive git@github.com:vlab-cs-ucsb/ABC.git ABC # or use https://github.com/vlab-cs-ucsb/ABC.git
ABC testing depends on googletest and googlemock as subprojects. It is important to clone with --recursive option.
###Easy(Automated) Setup
- ABC. Clone ABC source and run build script. It automatically tries to install required system packages and dependent projects; Glog and Mona. After installing dependencies, it installs ABC. If script does not work please try step-by-step guide or contact us. (That script is tested with Linux machines. You can still use build script in other posix systems if you resolve system dependencies manually.)
$ cd ABC/build
$ ./install-build-deps.py
###Step-by-Step(Semi-automated) Setup ####System Dependencies
- C++ compiler with C++14 support. Latest ABC compilation is tested with g++ 5.4.0 on Ubuntu 16.04.
- Git
$ sudo apt install git
- ABC is an autotools project, you need to setup autotools in your system. Please make sure you have installed all the tools below.
$ sudo apt install build-essential autoconf automake libtool intltool
- Lex and Yacc. ABC is tested with Flex 2.6.0 and Bison 3.0.4.
$ sudo apt install flex bison
- Python (optional). A short installation script is written in pyhton.
$ sudo apt install python
####Project Dependencies
- Glog logging library for C++. It is an autotools project. Please follow the instructions in their website if the below shortcut doesn't work for you. Don't forget to apply patch as below:
$ cd <your home directory or a preferred directory>
$ git clone https://github.com/google/glog.git
$ cd glog
$ git apply <ABC_ROOT_DIR>/external/glog/glog_abc_autotools.patch
$ libtoolize && aclocal && automake --gnu --add-missing && autoreconf -ivf
$ ./configure
$ make all
$ sudo make install
$ sudo ldconfig
You should have glog libraries installed at /usr/local/lib and headers installed at /usr/local/include/glog/ after running above commands.
- Mona is used for symbolic representation of automata. Don't forget to apply patch as below:
$ cd <your home directory or a preferred directory>
$ git clone https://github.com/cs-au-dk/MONA.git
$ cd MONA
$ git apply <ABC_ROOT_DIR>/external/mona/mona_abc.patch
$ libtoolize && aclocal && automake --gnu --add-missing && autoreconf -ivf
$ ./configure
$ make all
$ sudo make install
$ sudo ldconfig
You should have mona libraries installed at /usr/local/lib and headers installed at /usr/local/include/mona/ after running above commands.
####ABC Installation
- ABC.
$ cd <your home directory or a preferred directory>
$ git clone --recursive git@github.com:vlab-cs-ucsb/ABC.git ABC // or use https://github.com/vlab-cs-ucsb/ABC.git
$ cd ABC
$ ./autogen.sh
$ ./configure
$ make all
$ sudo make install
$ sudo ldconfig
If you want to use ABC with JAVA programs, make sure JAVA_HOME environment variable is set and has a valid Java installation path before running ./configure command.
At this point you should have all necessary libraries installed at /usr/local/lib directory. You should also have all necessary header files at
/usr/local/include/glog,
/usr/local/include/mona,
/usr/local/include/abc
directories.
####C++
You can link to dynamic library generated in your program. An example executable for abc is generated for you and install in your system. You can run abc executable at your home directory as:
$ abc -i <input_file_path>
$ abc --help #lists available command line options
You can find example constraints at <abc source folder>/test/fixtures.
You can take a look at <abc source folder>/src/main.cpp to see how abc is used in a C++ program as a shared library.
(More documentation on ABC input language and format will be provided, please see <abc-source-folder>/test/fixtures folder for examples)
####JAVA
You have to compile ABC with your JAVA_HOME path is set to a valid java path. Once you set your JAVA_HOME path, you need to install/re-install ABC on your system.
You need to set Java VM argument java.library.path to path where your shared libraries are install, or alternatively you can set LD_LIBRARY_PATH environment variable to that path.
You can use <abc-source-folder>/lib/ABCJava as an example Java program that calls abc.
In your Java project all you have to do is to include the contents of <abc-source-folder>/lib/ABCJava/src/. vlab.cs.ucsb.edu.DriverProxy.java class is the class that makes abc calls.
to be prepared...
####Workflow
1- Always start working on your own branch, do not directly work on master branch
2- Follow rebase work flow whenever possible
3- If you are not sure how to merge/rebase with/onto master, create a fresh branch out of master and first try to merge/rebase using that branch.
####Coding Style
Please follow Google C++ Style Guide.