search

plum-umd / pasket

Synthesizing Framework Models for Symbolic Execution
MIT License
15 stars 5 forks source link

readme

Pasket

Pasket is a pattern-based sketching tool that leverages design patterns so as to synthesize models for event-driven frameworks, such as Swing and Android.

Publications

Requirements

The main feature of this tool is to translate high-level templates into low-level ones in Sketch. Thus, you have to install it first. Download the tar ball and follow the instruction in it. You may need to set your environment variables as follows:

    export SKETCH_HOME=/path/to/sketch/runtime
    export PATH=$PATH:$SKETCH_HOME/..

A harder way is to install it from source code: front-end/back-end. In that case, build architecture-independent version of front-end via:

    <sketch-frontend> $ make assemble-noarch

and then set your environment variables as follows:

    export SKETCH_HOME=/path/to/sketch-frontend
    export PATH=$PATH:$SKETCH_HOME/target/sketch-1.7.0-noarch-launchers

There are several Java applications in this project. To build them efficiently, your system needs to have Apache Ant installed.

This tool is tested under Python 2.7.1.

Usage (Tool)

Parser Generation

Auto-generated files are not maintained under the version control. So, generate the lexer and parser first:

$ python -m grammar.gen [-g Java.g]

or

$ ./grammar/gen.py [-g Java.g]

The default ANTLR grammar file is Java.g, which is modified to allow annotations in an expression level. The command above will generate the lexer and parser in grammar/ folder.

Custom Codegen

Next, compile the custom code generator for sketch:

    $ ./run.py -c codegen

Note that your env should have variable $SKETCH_HOME as mentioned above so that the build process can refer to sketch jar file. You can also use the following commands, if preferred:

    $ cd codegen; ant; cd ..

Model Synthesis

Then, synthesize a framework model:

    $ ./run.py -c (android|gui) [-s sample] [-t template] [-p pattern] [-o result]

Inputs for synthesis are samples and templates. The default paths for samples and templates depend on the command. For example, if the command is "android", the default path for sample is sample/android/ folder. You can pass a single file, e.g.,

    $ ./run.py -s sample/android/remotedroid.txt

Otherwise, the tool will read all the samples in the given path, e.g., sample/android/*/*.txt. (sample/android/README.md explains how to use sample/android/trim.py in order to obtain such samples from apps instrumented by redexer.)

Similarly, the default paths for template are template/android/ and template/app/android/ folders. The former includes framework modelings, while the latter has client code, i.e., tutorials. You can pass multiple templates, e.g.,

    $ ./run.py -t template/android -t template/app/android

By default, the tool will try all possible design patterns. If performance does matter, you can hint which design patterns are used in the template:

    $ ./run.py -p observer -p state

Using both samples and templates, the tool will encode the problem into sketches, and those intermediate files will be left at result/(java_)sk*/ folder. The final synthesized code will be placed at result/java/ folder.

To synthesize Java GUI model, run the following command:

    $ ./run.py -c gui -p button_demo -p checkbox_demo ... [opts]

For Android model, run the following command:

    $ ./run.py -c android -p button -p checkbox ... [opts]

Notice that you need -p option for every demo you pass.

There are more options for debugging purpose:

--no-encoding: proceed without the encoding phase,
               to test manipulated sketch files
--no-sketch: examine the process without running sketch,
             rather it will use previous output)

You can simulate a certain demo using the synthesized model:

    $ ./run.py -c gui -p button_demo -p colorchooser_demo --simulate colorchooser_demo2

where the first two demos are used for synthesizing a model, and then the third one is simulated on top of that synthesized model. If you pass the same demo as synthesis input and simulation target, the tool will perform so-called sanity checking:

    $ ./run.py -c gui -p button_demo --simulate button_demo

which is just same as this:

    $ ./run.py -c gui -p button_demo --sanity

To run (deprecated) design pattern examples, use the following commands:

    $ ./run.py -c pattern -p observer
    $ ./run.py -c pattern -p state
    $ ./run.py -c pattern -p singleton

The existing examples can be tested as follows:

    $ ./test/test.py pattern observer
    $ ./test/test.py gui button_demo [checkbox_demo ...]

Usage (Model)

Swing

To run Java PathFinder (JPF) together with the synthesized model, install jpf-core, jpf-symbc, and jpf-awt first. In what follows, we assume those projects are installed under user.home/Downloads/jpf directory. Then, copy jpf-awt into jpf-awt-synth, where the synthesized model will be placed. To copy such synthesized model into that folder, run as follows:

  ...result $ ant gui

Next, go to jpf-awt-synth and build it same as other jpf-* projects.

JPF has its own event generating mechanism; refer to example/gui/src/oreilly/ch*/*Test.java Classpath to compile JPF test classes is set up in example/gui/build.xml, so place your own target in that build.xml when you add new applications. Also, generate app-specific test class accordingly. To build examples and applications, refer to example/gui/README.md.

To run jpf-symbc both with jpf-awt and jpf-awt-synth, you need to design configurations like: example/gui/src/oreilly/ch*/*.awt(-synth).jpf Then, run jpf-symbc/bin/jpf, passing paths to those configurations.

Android

To be added...

Structure