SymbolicAbstraction

Code

File Layout

• core/ holds base class definitions for abstract and concrete states as well as logic formulas.
• domains/ holds definitions for particular abstract domains.
• algorithms/ contains the algorithms acting on core/ classes (currently RSY and bilateral algorithms for symbolic abstraction).
• frontend/ contains a simple two-operand language for which abstract transformers can be automatically derived via the symbolic abstraction algorithms.
• tests/ holds PyTest unit tests.

High-Level Organization

Each abstract domain is associated with at least three classes:

• A subclass of ConjunctiveDomain which implements methods such as gamma_hat, alpha_hat, and join (essentially, it implements operations on abstract states and interfaces with the SMT solver).
• A subclass of AbstractState which represents a single abstract state in the corresponding domain. Note that this contains the entire program state, so often a separate "individual variable state" class will be written as well (for example, IntervalAbstractState is made up of Intervals, one for each variable).
• A subclass of ConcreteState, which represents (usually) a concrete set of variable assignments.

Currently, all of our abstract domains inheret from Z3VariablesDomain which implements the ConcreteState and handles calls to the SMT solver when the underlying concrete semantics and variable types can be described in Z3.

Note that this has been extracted from a larger system with more complex domains. We have attempted to pare it down to a minimal expository subset, but if you catch anything that seems unnecessary or could be significantly simplified please open an issue and we can remove it!

Running Tests

A docker container is provided to run tests, which can be executed by the following make rule:

make docker-test

Alternatively, if you have an up-to-date version of Python 3 installed you can run

pip3 install --user pytest z3-solver
python3 -m pytest tests

Examples

Test Cases

The test cases in tests/ demonstrate usage of most of the individual functionality.

Entire Example Program

An example program is available in example_program.py which demonstrates how Symbolic Abstraction can be used to automatically compute an abstract transformer for a straight-line program.

Reduced Product

The test case in tests/test_reduced_product_domain/test_reduce.py shows how Symbolic Abstraction can be used to automatically compute the reduced product of two abstract domains.

About

People

Code written by Matthew Sotoudeh (contact [email protected]), advised and reviewed by Professor Aditya Thakur (contact [email protected]). For more information, please see the Davis Automated Reasoning Group.

Papers, Citation

The algorithms used here are adapted from:

Thakur, A. V. (2014, August). Symbolic Abstraction: Algorithms and Applications
(Ph.D. dissertation). Computer Sciences Department, University of Wisconsin,
Madison.

The dissertation is available here.

To cite the dissertation, please use the following bibtex:

@phdthesis{thakur_PHD14,
    author = {Thakur, Aditya V.},
    title = {Symbolic Abstraction: Algorithms and Applications},
    school = {Computer Sciences Department, University of Wisconsin, Madison},
    type = {Ph.D. dissertation},
    month = aug,
    year = {2014}
}