This is the PDSolver webpage as submitted to Spin 2010. As of 28th October 2010, later versions of PDSolver are available.
PDSovler is a tool for evaluating both mu‐calculus formulas over pushdown systems and pushdown parity games. It is an explicit state OCaml implementation of algorithms presented at Concur [Concur09] and submitted to Information and Control [I&C10]. We also extend these algorithms to support backwards modalities [Backwards10] and allow the analysis to be restricted to reachable configurations.
This tool has been submitted to SPIN 2010 [Spin10]. Below we provide examples of control flow graphs extracted, using the Soot Framework, from the DaCapo Benchmark Suite (Version 9.12). We distribute the tool with some Soot libraries. Up‐to‐date versions can be obtained from the Soot homepage. We do not distribute a copy of the DaCapo benchmarks.
This tool is maintained by Matthew Hague. Any queries/bugs/comments/&c. can be directed to Matthew Hague * comlab ox ac uk (with * = @ and spaces are .).
PDSolver requires
JimpleToPDSolver requires
Download pdsolver.tgz and run the
following commands from the directory containing pdsolver.tgz.
tar xzf pdsolver.tgz
cd PDSolver
omake
./src/main/pdsolver.opt examples/journal.pdmu
To run the examples from the SPIN submission, first download pdsolver‐examples.tgz to the
same directory as pdsolver.tgz. Then run the commands below (for
example).
tar xzf pdsolver-examples.tgz
cd PDSolver
./src/main/pdsolver.opt -o avroraReg.out -r csinit examples/avroraReg.pdmu
-o avroraReg.out specifies an output file, and
-r csinit restricts the analysis to configurations
reachable from the initial configuration <csinit, #>,
where the hash marks the bottom of the stack.
Download jimpletopdsolver.tgz and, from
the directory that contains it, run the following commands.
tar xzf jimpletopdsolver.tgz
cd JimpleToPDSolver
ant compile
./JimpleToPDSolver -f dataflow.out "<examples.Dataflow: void main(java.lang.String[])>"
dataflow.out and add
Mu Property:
!(
(nu X . (!csend &
[@def__examples_Dataflow__int_i_]ff
&
[\use__examples_Dataflow__int_i_ usedef__examples_Dataflow__int_i_]X))
&
~[\def__examples_Dataflow__int_i_ usedef__examples_Dataflow__int_i_](nu
Y.(mu Z. csend |
<@def__examples_Dataflow__int_i_>tt |
<\use__examples_Dataflow__int_i_ usedef__examples_Dataflow__int_i_>Z) &
~[\def__examples_Dataflow__int_i_ _usedef__examples_Dataflow__int_i_]Y)
)
dataflow.pdmu. This is the dataflow example
from the Spin submission. We can generate the denotation of the
property by running the file through pdsolver, as in the extended
examples section above.
unzip dacapo-9.12-bach.jar 'jar/*' -d JimpleToPDSolver/lib/
tar xzf jimpletopdsolver-examples.tgz
cd JimpleToPDSolver
ant compile
./JimpleToPDSolver -f avroraReg.out "<examples.AvroraReg: void main(java.lang.String[])>"
avroraReg.out as in the
previous example.
In the following, we assume familiarity with pushdown systems, parity games and mu‐calculus.
To obtain usage information on PDSolver, run
./src/main/pdsolver.opt --help
--output-file,
--output-format, --check-type and
--reachable.
The standard invocation command is
./src/main/pdsolver.opt -o <outfile> <infile>
outfile specifies where to write the output, and
infile where to find the input problem. The type of
problem is determined by the file extension: pdg for a
pushdown parity game, and pdmu for a pushdown system and
mu‐calculus problem. Common to both is a description of a pushdown
system. This takes the following form.
Rules:
p a -> q _;
p a -> q b;
p a -> q b c;
. . .
p
and q are control states, and a,
b and c are stack characters. Note, a word of any
length may be specified. E.g. p a -> q b c d e f;. The
stack character # is a special character denoting the
bottom of the stack. This symbol cannot be added to, or removed from
the stack.
An example pdg file (examples/Arnaud.pdg) is shown below.
Rules:
p # -> f #;
p a -> p _;
f a -> p a;
f a -> f a a;
f # -> f #;
Control States:
p Abelard 1;
f Abelard 2;
Control
State section specifies, for each control state, whether the
state is owned by Eloise or Abelard, and the
colour of the state.
Running the command
./src/main/pdsolver.opt examples/Arnaud.pdg
Done.
4 States: { q* qe (f,1) (p,1) }
Transitions:
q* -#-> { { qe } }
q* -a-> { { q* } }
(f,1) -#-> { { qe } }
(f,1) -a-> { { q* (p,1) } }
(p,1) -#-> { { qe } }
(p,1) -a-> { { (p,1) } }
Total time: 0.003 Check time: 0.003
Gather stats time: 0. Final opt time: 0.
Ma states: 4 Ma trans: 6
Max states: 0 Max trans: 0
Controls: 2 Characters: 2 Transitions: 5
Colours: 2
(f,1) and (p,1) since, for example, a
configuration <p, w> is in Eloise's winning region if
w is accepted from (p,1). As an example, take a
transition q -a-> { { q1 q2 } { q3 } }. This means the
automaton has two a transitions from the state
q. The first is an alternating transition to both
q1 and q2. The second is a standard
non‐deterministic transition to q3. The remainder of the
output shows statistics on the input, runtime, and result. Note that
the zero entries are zero because we did not specify
--gather-stats on the command line.
An example pdmu input file
(examples/journal.pdmu) follows.
Rules:
p a -> p _;
p # -> f #;
f # -> f #;
f a -> f a a;
f a -> p a;
Mu Property:
(mu Z1 . (nu Z2 . ((p & []Z1) | (f & []Z2))))
Propositions:
p a p;
p # p;
f a f;
f # f;
Propositions section, taking the following
form.
p a x y z . . .;
p and top of stack character a, the atomic
propositions x, y and z are true.
All other propositions are false.
The syntax of the mu‐calculus is described below. Note that to ensure
the correct scoping of fixed points, we recommend putting all
expressions mu Z . f and nu Z . f in
parenthesis. That is (mu Z . f) and (nu Z .
f).
x |
Atomic propositions begin with a lowercase character. |
Z |
Variables begin with an uppercase character. |
f1 & f2 |
The conjunction of formulas f1 and f2. |
f1 | f2 |
The disjunction of formulas f1 and f2. |
!f1 |
The negation of f1. |
<>f1 |
The forward diamond modality for f1. |
<@x1 x2 . . .>f1 |
The forward diamond modality for f1, parameterised
by the propositions x1, x2, &c.. |
<\x1 x2 . . .>f1 |
The forward diamond modality for f1, parameterised
by all propositions other than x1, x2, &c.. |
[]f1 |
The forward box modality for f1. |
[@x1 x2 . . .]f1 |
The forward box modality for f1, parameterised
by the propositions x1, x2, &c.. |
[\x1 x2 . . .]f1 |
The forward box modality for f1, parameterised
by all propositions other than x1, x2, &c.. |
~<>f1 |
The backward diamond modality for f1. |
~<@x1 x2 . . .>f1 |
The backward diamond modality for f1, parameterised
by the propositions x1, x2, &c.. |
~<\x1 x2 . . .>f1 |
The backward diamond modality for f1, parameterised
by all propositions other than x1, x2, &c.. |
~[]f1 |
The backward box modality for f1. |
~[@x1 x2 . . .]f1 |
The backward box modality for f1, parameterised
by the propositions x1, x2, &c.. |
~[\x1 x2 . . .]f1 |
The backward box modality for f1, parameterised
by all propositions other than x1, x2, &c.. |
(mu Z . f1) |
The least fixed point of Z in f1. |
(nu Z . f1) |
The greatest fixed point of Z in
f1. |
The JimpleToPDSolver tool provides very limited functionality. To
extract a pushdown system from a Java program, first make sure that the
program classes are available in the classpath.
export CLASSPATH="<path to program classes>:$CLASSPATH"
./JimpleToPDSolver -f dataflow.out "<examples.Dataflow: void main(java.lang.String[])>"
dataflow.out now contains a list
of pushdown rules, and a list of proposition assignments as described
above.
Rules:
csinit # -> csq cpLinit0016 #;
csq cpLinit0016 -> csq cpL_examples_Dataflow__main_ALjava_lang_String_V__11_0;
. . .
Propositions:
csq # csq #;
csq cpL_examples_Dataflow__b_V__23_12 csq cpL_examples_Dataflow__b_V__23_12 use__examples_Dataflow__int_i_ def__i1__in___examples_Dataflow__b_V_;
. . .
The initial configuration of the program is <csinit,
#>. The main control state is csq and
csend is reached when the program terminates. The alphabet
contains labels of the form
cpL_<class>__<method name>__<argument types>__<line no>_<unique id>
The generated file can be turned into a use__<var name>__in___<method info>
for any variables used (but not modified) by the program line.
Note that the method information is only present in local
variables, and specifies which method the variable is local
to,def__<var name>__in___<method info>
for any variables defined (but not used) by the program line,
andusedef__<var name>__in___<method info>
for any variables both used and defined by the program line.pdmu file with the
addition of a Mu Property section.
JimpleToPDSolver translates the Jimple representation of the program to a pushdown system. Each statement roughly corresponds to one Jimple command. All data values are ignored, so statements such as assignments simply move to the next control point, while conditional statements branch non‐deterministically to any of the possible successor points. Virtual method calls are resolved by adding a branch calling each of the implementing methods present in the program (that is, in any class mentioned in the code).
When an exception is thrown, if its type can be determined statically, execution branches to the appropriate catch block, if one occurs. Otherwise the current method returns. If the type cannot be determined, we branch to any of the available catch blocks, or return. At each return point there is a branch that assumes an exception could have been returned. Hence, as well as continuing execution, we may also branch to any available catch blocks, or return from the method.