Concolic Execution Configuration

Every concolic execution must be part of the regular execution of a Java program. Hence, the target configuration value for JPF must appear in the configuration.

In the JDart configuration, several methods can be prepared to be concolically analyzed, but only a single specific analysis can be executed per program execution. Each target method configuration must have a unique (among target method configurations) name (e.g., cm1). The JPF configuration prefix for a configuration named <name> is concolic.methods.<name> (e.g., concolic.methods.sample). In the remainder of this section, we will refer to this prefix as <prefix>.

The method to be in fact analyzed is specified by setting the concolic.method configuration to the <name> of the target method. For example:

...
concolic.method = cm1

The specification of a target method is given through its fully qualified name plus its signature (using primitive type or fully qualified class names; without return type). Parameters can optionally be prepended by a name followed by a colon (:). This specifies both that they are to be treated symbolically as well as the name used to refer to them (it is discouraged to use anything but valid Java identifiers here).

A sample target method configuration could look like this:

concolic.methods.cm1=sample.Foo.foo(a:int,b:boolean)

This triggers the concolic execution of method foo with an int and a boolean parameter of class sample.Foo. The parameters will be referred to as a and b, respectively. Note that also the following would have been valid:

concolic.methods.cm1=sample.Foo.foo(a:int,boolean)

In this case, however, the second parameter would not be treated symbolically.

Naming Scheme

The names to assign to symbolic variables are generally quite straightforward, and are mostly valid Java expressions. The names for the symbolic parameters are derived from the method specification (see above); if the method is an instance method, the target instance will be referred to as this. If an object named obj is symbolic and a field f of it is meant to be made symbolic, it will be referred to as obj.f (for example this.a). If an array variable named arr is symbolic, its elements will be referred to as arr[0], arr[1] etc. Static fields of classes which should be treated symbolically are referred to by their fully qualified name (e.g., Sample.Foo.staticField). As this complies with Java, there should be no name clashes in assigning symbolic names to variables.

In order to improve readability, deviations from this scheme occur for the following frequently used Java classes:

• java.lang.String: As there currently is no possibility to treat strings symbolically, those are never symbolic.
• java.util.ArrayList, java.util.LinkedList, java.util.Vector: The symbolic naming scheme corresponds to those for arrays; this also means that size/elementCount fields are never made symbolic.
• java.util.HashMap: The symbolic naming scheme is similar to those of arrays. However, the indices are quoted strings if the key type is string (for instance hashMap["foo"]), or a running number with a leading hash sign (hashMap[#0], hashMap[#1] etc.) if the key is of some other type.