| [aad342c] | 1 | <html>
|
|---|
| 2 | <body>
|
|---|
| 3 |
|
|---|
| 4 | <p>
|
|---|
| 5 | <strong>SARL: The Symbolic Algebra and Reasoning Library</strong> is a
|
|---|
| 6 | Java library for creating, manipulating, and reasoning about symbolic
|
|---|
| 7 | expressions. The library can be used to support various applications
|
|---|
| 8 | that require symbolic reasoning, such as symbolic execution tools for
|
|---|
| 9 | program analysis, verification, or test case generation.
|
|---|
| 10 | </p>
|
|---|
| 11 |
|
|---|
| 12 |
|
|---|
| 13 | <h2>Key Features</h2>
|
|---|
| 14 |
|
|---|
| 15 | Some of the features of SARL include:
|
|---|
| 16 | <ul>
|
|---|
| 17 | <li><strong>Symbolic references.</strong> There is a "reference
|
|---|
| 18 | type" which has symbolic values such as r1="the i-th element of an
|
|---|
| 19 | array", or "the i-th field of the j-th element of an array of
|
|---|
| 20 | tuples". There is a method "dereference" that takes a reference value
|
|---|
| 21 | and a symbolic expression of the appropriate type and returns the
|
|---|
| 22 | subexpression specified by the reference. For example,
|
|---|
| 23 | dereference(r1, a) will return "a[i]". This make representing pointer
|
|---|
| 24 | values in a C program really easy. There is also a method assign(r,
|
|---|
| 25 | x, y), which returns the symbolic expression obtained by starting
|
|---|
| 26 | with x and modifying the component specified by r with y. This makes
|
|---|
| 27 | the symbolic execution of C statements like "*p=e" easy.</li>
|
|---|
| 28 | <li><strong>Union types.</strong> Given any sequence of types
|
|---|
| 29 | t1,...,tn, you can form the union type t1+...+tn. The domain of this
|
|---|
| 30 | type is the union of the domains of the ti. This makes representing a
|
|---|
| 31 | heap easy, for example, let t1,...,tn be all the types that are ever
|
|---|
| 32 | malloced, let the heap type be: array of union_i(array of ti). It
|
|---|
| 33 | also useful for message queues, which are arrays that can hold
|
|---|
| 34 | various types of elements.</li>
|
|---|
| 35 | <li><strong>Simplifications.</strong> Given a boolean-valued
|
|---|
| 36 | expression (the "context") and another symbolic expression, the
|
|---|
| 37 | simplify method returns a simplified version of the expression under
|
|---|
| 38 | the assumption that the context holds. For example, if context is
|
|---|
| 39 | "x>1" and e is "x>0" then e is simplified to "true". If the context
|
|---|
| 40 | contains a bunch of polynomial equalities, these are treated as
|
|---|
| 41 | linear expressions in the monomials and Gaussian elimination is
|
|---|
| 42 | performed to solve for any/all of those monomials. And so on. This is
|
|---|
| 43 | useful in symbolic execution, where the context is the path
|
|---|
| 44 | condition, and you can run over the whole state simplifying it,
|
|---|
| 45 | getting the state to (as close as possible to) a canonical form. This
|
|---|
| 46 | can help you decide if you have seen the state before, greatly
|
|---|
| 47 | simplifies the theorem proving queries, etc.</li>
|
|---|
| 48 | <li><strong>Persistence.</strong> Symbolic expressions are
|
|---|
| 49 | immutable, but they are implemented with "persistent" data
|
|---|
| 50 | structures. These are immutable data structures that provide analogs
|
|---|
| 51 | of all the standard mutation methods (like "set the i-th element of
|
|---|
| 52 | the array to x") but return a whole new data structure instead of
|
|---|
| 53 | modifying the existing one, i.e.: <code> PersistentArray
|
|---|
| 54 | <T> set(int index, T x); </code></li>
|
|---|
| 55 | <li><strong>Herbrand versions of the numeric types.</strong> In
|
|---|
| 56 | addition to the (ideal) integer and real types, there are Herbrand
|
|---|
| 57 | integer and Herbrand real types. A numerical operation involving a
|
|---|
| 58 | Herbrand type is treated as an uninterpreted function (and never
|
|---|
| 59 | simplified). Hence in one program you can mix and match: have some
|
|---|
| 60 | Herbrand and some ideal values. The Herbrands are useful, for
|
|---|
| 61 | example, for representing floating point values when you don't want
|
|---|
| 62 | to assume anything about the floating point operations.</li>
|
|---|
| 63 | </ul>
|
|---|
| 64 |
|
|---|
| 65 | <h2>Using SARL</h2>
|
|---|
| 66 |
|
|---|
| 67 | SARL is meant to be used through its API, which is specified in package
|
|---|
| 68 | <a href="dev/civl/sarl/IF/package-summary.html">dev.civl.sarl.IF</a>
|
|---|
| 69 | and its sub-packages. For almost all users, this is the only part of
|
|---|
| 70 | SARL you should look at. The other packages contain the implementation
|
|---|
| 71 | code.
|
|---|
| 72 |
|
|---|
| 73 | </body>
|
|---|
| 74 | </html>
|
|---|
