SyPet

What is SyPet?

Are you tired of spending countless hours learning how to use existing Java libraries? Wouldn't it be nice if this process could be automated? SyPet is a program synthesis tool that helps programmers to use Java libraries. The programmer provides SyPet: (1) a signature of the method to be synthesized, (2) a set of test cases, and (3) a set of Java libraries. SyPet will automatically find a sequence of API calls from these Java libraries that will pass all test cases provided by the programmer. Stop wasting precious time and start using SyPet today!

Scalable

SyPet can handle libraries with thousands of APIs.

Fast

SyPet can synthesize most tasks in a few seconds.

Generic

SyPet can solve problems from different domains and supports arbitrary Java libraries.

Paper

For technical details see our POPL'17 publication: Component-Based Synthesis for Complex APIs. Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, Thomas W. Reps.

Usage

Requirements

Unix-like system (OS X or Linux)
Java 7 or higher
Apache Ant

Installation

Clone the source code of SyPet from the GitHub repository at the UToPiA research group:

                    
$ git clone https://github.com/utopia-group/sypet.git

Compile SyPet with Apache Ant:

                    
$ ant

Configuration Json file

To run SyPet the user must provide a Json file with the configuration of the tool and the information of the benchmark. The Json file contains the following parameters:

Id: an integer id for the benchmark.
methodName: the method name for the synthesized function.
paramNames: names for the arguments of the synthesized function.
srcTypes: the full quantified Java type of each paramNames.
tgtType: the full quantified Java type of the goal.
packages: which packages should be used to search for the APIs that will transform srcTypes into tgtType. The user can specify any granularity of the package. A more specific granularity will lead to a smaller search space and better performance for SyPet.
Libs: the location of the Java libraries that contain the described packages.
testPath: the location of the test function.

Consider a programmer, Bob, who wants to implement functionality for rotating a 2-dimensional geometric object. Specifically, Bob has the following signature in mind:

                    
Area rotate(Area obj, Point2D pt, double angle)

Here, the rotate method should take a 2-dimensional object called obj and return a new object that is the same as obj except that it has been rotated by the specified angle around the specified point pt. The types Area and Point2D are defined in the java.awt.geom library. Here is an example of a Json file to run SyPet on this problem:

    
{
  "id": 13,
  "methodName": "rotate",
  "paramNames": [
    "sypet_arg0",
    "sypet_arg1",
    "sypet_arg2"
  ],
  "srcTypes": [
    "java.awt.geom.Area",
    "java.awt.geom.Point2D",
    "double"
  ],
  "tgtType": "java.awt.geom.Area",
  "packages": [
    "java.awt.geom"
  ],
  "libs": [
    "./lib/rt7.jar"
  ],
  "testPath": "benchmarks/geometry/13/TestSource.java"
}

Test file

The testPath parameter contains the location of the test file. This file should be a Java file containing a set of test cases such that:

The following method must exist in this Java file:

                
public static boolean test() throws Throwable { }

All types should be fully quantified.

An example of a test file for the rotate method can be seen here:


public static boolean test() throws Throwable {
  return test0() && test1();
}
public static boolean test0() throws Throwable {
  java.awt.geom.Area a1 = new java.awt.geom.Area(new java.awt.geom.Rectangle2D.Double(0, 0, 10, 2));
  java.awt.geom.Area a2 = new java.awt.geom.Area(new java.awt.geom.Rectangle2D.Double(-2, 0, 2, 10));
  java.awt.geom.Point2D p = new java.awt.geom.Point2D.Double(0, 0);
  java.awt.geom.Area a3 = rotate(a1, p, Math.PI / 2);
  return a2.equals(a3);
}
public static boolean test1() throws Throwable {
  java.awt.geom.Area a1 = new java.awt.geom.Area(new java.awt.geom.Rectangle2D.Double(10, 20, 10, 2));
  java.awt.geom.Area a2 = new java.awt.geom.Area(new java.awt.geom.Rectangle2D.Double(8, 20, 2, 10));
  java.awt.geom.Point2D p = new java.awt.geom.Point2D.Double(10, 20);
  java.awt.geom.Area a3 = rotate(a1, p, Math.PI / 2);
  return a2.equals(a3);
}

Running SyPet

After creating the Example.json file, the user can run SyPet with the following command line:

                    
$ ./run-sypet.sh Example.json

SyPet will synthesize the following code that rotates a rectangle by a given angle:


import java.awt.geom.AffineTransform;
import java.awt.geom.Area;
import java.awt.geom.Point2D;

public class Solution {
  public static Area rotate(Area arg0, Point2D arg1, double arg2) {
    double v1 = arg1.getX();
    double v2 = arg1.getY();
    AffineTransform v3 = AffineTransform.getRotateInstance(arg2, v1, v2);
    Area v4 = arg0.createTransformedArea(v3);
    return v4;
  }
}

Architecture

SyPet starts by building a compact Petri-net representation of the relationships between API components from the initial set of Java libraries. In this kind of Petri-net, places (nodes) correspond to types, transitions represent methods, and tokens denote the number of program variables of a given type.

In our approach, a reachable path in the Petri-net model corresponds to a program sketch rather than a complete executable program. In particular, to keep the underlying Petri net representation compact, our algorithm deliberately decomposes the synthesis task into two separate sketch-generation and sketch-completion phases. Hence, after we perform reachability analysis on the Petri net, we must still complete the sketch by determining what arguments to provide for each procedure. Toward this goal, our algorithm generates constraints that encode various syntactic and semantic requirements on the synthesized program, and uses a SAT solver to find a model. The satisfying assignment produced by the solver is then used to generate a candidate implementation that can be tested. If the synthesized program fails any test case, our algorithm backtracks and generates a different implementation, either by finding another model of the SAT formula or by exploring a different reachable path in the Petri net. The programs synthesized by our algorithm are guaranteed to type check and pass all test cases provided by the user.

For further technical details we refer the interested reader to the POPL'17 paper: Component-Based Synthesis for Complex APIs. Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, Thomas W. Reps.

Contact

SyPet was developed by the UToPiA research group lead by Isil Dillig at UT Austin.

SyPet is maintained by Ruben Martins at CMU and Yu Feng at UT Austin.