SARL: The Symbolic Algebra and Reasoning Library is a Java library for creating, manipulating, and reasoning about symbolic expressions. The library can be used to support various applications that require symbolic reasoning, such as symbolic execution tools for program analysis, verification, or test case generation.
Key Features
Some of the features of SARL include:- Symbolic references. There is a "reference type" which has symbolic values such as r1="the i-th element of an array", or "the i-th field of the j-th element of an array of tuples". There is a method "dereference" that takes a reference value and a symbolic expression of the appropriate type and returns the subexpression specified by the reference. For example, dereference(r1, a) will return "a[i]". This make representing pointer values in a C program really easy. There is also a method assign(r, x, y), which returns the symbolic expression obtained by starting with x and modifying the component specified by r with y. This makes the symbolic execution of C statements like "*p=e" easy.
- Union types. Given any sequence of types t1,...,tn, you can form the union type t1+...+tn. The domain of this type is the union of the domains of the ti. This makes representing a heap easy, for example, let t1,...,tn be all the types that are ever malloced, let the heap type be: array of union_i(array of ti). It also useful for message queues, which are arrays that can hold various types of elements.
- Simplifications. Given a boolean-valued expression (the "context") and another symbolic expression, the simplify method returns a simplified version of the expression under the assumption that the context holds. For example, if context is "x>1" and e is "x>0" then e is simplified to "true". If the context contains a bunch of polynomial equalities, these are treated as linear expressions in the monomials and Gaussian elimination is performed to solve for any/all of those monomials. And so on. This is useful in symbolic execution, where the context is the path condition, and you can run over the whole state simplifying it, getting the state to (as close as possible to) a canonical form. This can help you decide if you have seen the state before, greatly simplifies the theorem proving queries, etc.
- Persistence. Symbolic expressions are
immutable, but they are implemented with "persistent" data
structures. These are immutable data structures that provide analogs
of all the standard mutation methods (like "set the i-th element of
the array to x") but return a whole new data structure instead of
modifying the existing one, i.e.:
PersistentArray <T> set(int index, T x); - Herbrand versions of the numeric types. In addition to the (ideal) integer and real types, there are Herbrand integer and Herbrand real types. A numerical operation involving a Herbrand type is treated as an uninterpreted function (and never simplified). Hence in one program you can mix and match: have some Herbrand and some ideal values. The Herbrands are useful, for example, for representing floating point values when you don't want to assume anything about the floating point operations.
Using SARL
SARL is meant to be used through its API, which is specified in package edu.udel.cis.vsl.sarl.IF and its sub-packages. For almost all users, this is the only part of SARL you should look at. The other packages contain the implementation code.Packages
Package
Description
This is the root package for SARL, and contains the single class
SARL.Implementation of the configuration classes specified in package
edu.udel.cis.vsl.sarl.IF.config.This package deals with the represention of boolean symbolic expressions in a
conjunctive normal form.
Implementation classes for generic symbolic expressions, symbolic expression
factories, and a comparator on symbolic expressions.
This package provides the internal interface for the representation of basic
symbolic expressions.
Implementation classes for the herbrand module.
This package provides the internal interface supporting Herbrand arithmetic,
i.e., arithmetic in which all operations are treated as uninterpreted
operations.
Implementation classes for the ideal2 module.
The ideal module supports reasoning about numerical expressions using "ideal"
mathematical reals and integers.
This package and its subpackages provide the "public interface" to SARL.
The config module provides a
SARLConfig type, which
encapsulates configuration information such as the list of available theorem
provers with information on each.The public interface package dealing with symbolic expressions.
The number package supports infinite-precision integer and rational
numbers.
The object package provides the
SymbolicObject
interface, which is the root of the symbolic object type hierarchy.The type package provides interfaces for all of the symbolic types.
A utility package supporting infinite precision integer and rational numbers,
and a variety of arithmetic operations on them.
An implementation of the
number module.Implementation of the symbolic object module, specified in
edu.udel.cis.vsl.sarl.IF.object and
edu.udel.cis.vsl.sarl.object.IF.Internal interface for the symbolic object module, providing mechanisms for
creating
SymbolicObjects.This package provides the implementation of PreUniverse module.
This package provides all of the functionality of a symbolic universe except
reasoning.
This package provides implementation classes common to all theorem provers.
This package provides implementations of the
TheoremProver and
TheoremProverFactory interfaces based on the CVC3 and CVC4 theorem provers.
Module "prove" constitutes the interface between SARL and (possibly external)
theorem provers.
This package provides implementations of the
TheoremProver and
TheoremProverFactory interfaces based on Microsoft's Z3 theorem prover.Some generic implementations of the
Reasoner interface and the interfaces of
edu.udel.cis.vsl.sarl.reason.IF.The internal interface for the "reason" module, which deals with
Reasoners --- objects used to prove
theorems and simplify symbolic expressions.Partial and full implementations of simplification interfaces specified in
edu.udel.cis.vsl.sarl.simplify.IF.Interfaces for the simplification of symbolic expressions.
This package implements the main simplifier, which is based around a Context.
Implementations of the interfaces specified in
edu.udel.cis.vsl.sarl.IF.type and
edu.udel.cis.vsl.sarl.type.IF.Internal interface for the "type" module, providing a
SymbolicTypeFactory
for producing SymbolicType
s.Implementations of
SymbolicUniverses.Internal interface for the "universe" module.
General utility classes used throughout SARL.