/
README
95 lines (59 loc) · 4.31 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
ABC
============
The Automata Based Counter ([ABC](https://vlab.cs.ucsb.edu/ABC/)) is a **string and numeric constraint** 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.
Publications
============
ABC algorithmic details:
------------
- **ASE'19**, (Accepted, to appear in proceedings)[Subformula Caching for Model Counting and Quantitative Program Analysis](). William Eiers, Seemanta Saha, Tegan Brennan, Tevfik Bultan.
[Download experimental data and results]().
- **FSE'18**, [Parameterized Model Counting for String and Numeric Constraints](https://dl.acm.org/citation.cfm?doid=3236024.3236064). Abdulbaki Aydin, William Eiers, Lucas Bang, Tegan Brennan, Miroslav Gavrilov, Tevfik Bultan, Fang Yu.
- **CAV'15**, [Automata-based model counting for string constraints](http://www.cs.ucsb.edu/~baki/publications/cav15.pdf). Abdulbaki Aydin, Lucas Bang, and Tevfik Bultan. <br>
[Download experimental data and results.](https://vlab.cs.ucsb.edu/ABC/)
ABC use cases:
------------
- **FSE'16** [String Analysis for Side Channels with Segmented Oracles](http://www.cs.ucsb.edu/~baki/publications/fse16.pdf). Lucas Bang, Abdulbaki Aydin, Quoc-Sang Phan, Corina S. Pasareanu, and Tevfik Bultan.
Download
============
Latest version of ABC is available on GitHub:
https://github.com/vlab-cs-ucsb/ABC
A Docker image of ABC (pre-built and ready to go!) is also available through DockerHub:
TBD
Setup
============
ABC can be built for Linux and MacOS. For detailed build instructions, see [INSTALL.md](https://github.com/vlab-cs-ucsb/ABC/blob/master/INSTALL.md)
Usage
============
#### C++
You can link to dynamic library generated in your program. An example executable for mtabc is generated for you and install in your system. You can run mtabc executable at your home directory as:
$ abc -i <input_file_path>
$ abc --help #lists available command line options
E.g.,
$ abc -i <abc source folder>/test/fixtures/solver/ConstraintSolver/test_visitBegins_01.smt2
For an example of model counting a string with bound <= 5:
$ abc -i <abc source folder>/test/fixtures/solver/ConstraintSolver/test_visitBegins_01.smt2 -v 0 -bs 5
where -v 0 disables debugging output, and -bs 5 means count solutions with bound <= 5
If there are more than one string variables, you can specify which one you want to model count with the argument: --count-variable <VARIABLE_NAME>
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.
#### SPF (Symbolic Execution)
https://github.com/vlab-cs-ucsb/ABC/blob/master/spf-with-abc-readme.md
ABC Language Specification
==========================
to be prepared...
Contributing to ABC Source
==========================
####Workflow
1- Always start working on your own branch, do not directly work on master branch
2- Follow [rebase work flow whenever](https://www.atlassian.com/git/tutorials/merging-vs-rebasing) 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](https://google.github.io/styleguide/cppguide.html).