about

This project is a specialized shape analysis tool based on the parametric 3-valued logic abstraction, as defined by Sagiv, Reps and Wilhelm in their TOPLAS '02 paper and implemented in TVLA. It provides a fixed, generic abstraction for analyzing the heap behavior of programs written in modern imperative languages like Java. Several novelties include the use of structure-based refinement, the definition and implementation of loose embedding, and the graph-based 3-valued structure implementation. It also contains reference implementations of several TVLA abstract domain algorithms—like meet, join, structural embedding, and transitive closure—and their underlying graph-theoretic foundations. It was designed and implemented from scratch with efficiency in mind, and written in C.

examples

The analyzer takes as input a stripped-down CFG-style representation of an imperative program, adopted from TVLA. It then parses the program, generating a 3-valued logic abstract domain for it, and then runs a fixed-point computation to find the abstract descriptors for heap states at any program point, as well as a graphical representation of the CFG. Following are two examples used in the paper and tech report, and their output in human-readable graphical format (generated with GraphViz). Both are derived from Java programs used as TVLA benchmarks.

Program	Input	CFG	Output
Singly-linked list traversal	sll-loop.ltva	cfg-sll-loop.ps.gz	out-sll-loop.ps.gz
Doubly-linked list traversal in pairs	dll-pairs.ltva	cfg-dll-pairs.ps.gz	out-dll-pairs.ps.gz

papers

The project was motivated by the work on meet of 3-valued abstractions that I did in Tel-Aviv University, which was published in my master's thesis, a tech report, and the VMCAI '06 paper. The contributions of this project are presented in the SAS '06 paper. This tech report has more details about the design and implementation of the analyzer.

code

The analyzer is publicly available via anonymous CVS access. Login to the server by

  cvs -d :pserver:anonymous@play.cs.berkeley.edu:/cvsroot login

using an empty password (hit Enter). Then checkout the sources by

  cvs -d :pserver:anonymous@play.cs.berkeley.edu:/cvsroot co ltva

The distribution includes the analyzer sources (build with make) and several benchmarks. Here's a precompiled analyzer (linux-i686) that you can run directly with the above examples.

contact

Author: Gilad Arnold, UC Berkeley