Software Architecture and Engineering Project 2: Program Analysis

Project Description

• weldAt - performs welding at one point, where the point is inside the range of the robot.
• weldBetween - welds continuously from the startPoint to the endPoint, where startPoint and endPoint are inside the range of the robot. Moreover, the robots can only weld from left to right, meaning that startPoint has to be strictly smaller than endPoint.

public class Robot {
    private int left, right;
    public Robot(int l, int r) {
        this.left = l;
        this.right = r;
    }
    public native void weldAt(int point);
    public native void weldBetween(int startPoint, int endPoint);
}

Property 1:

For any reachable invocation of weldAt(point) on an object r of class Robot, the following holds: r.left <= point <= r.right.

Property 2:

For any reachable invocation of weldBetween(startPoint, endPoint) on an object r of class Robot, the following holds: r.left <= startPoint < endPoint <= r.right.

Your program analyzer (see template below) must take as input the name of a test class (TEST_CLASS). The last two lines of your program analyzer's output must be:

TEST_CLASS WELD_AT_OUTCOME
TEST_CLASS WELD_BETWEEN_OUTCOME

• WELD_AT_OK, if the program is guaranteed to satisfy Property 1.
• WELD_AT_NOT_OK, if the program cannot be proven to satisfy Property 1.

• WELD_BETWEEN_OK, if the program is guaranteed to have all calls to satisfy Property 2.
• WELD_BETWEEN_NOT_OK, if the program cannot be proven to satisfy Property 2.

Example 1

public class Test_1 {
    public static void m1(int j) {
        Robot b = new Robot(-2, 6);
        if (j > 2 && j < 6) {
            b.weldAt(j - 2);
            b.weldBetween(j - 4, j + 1);			
        }		
    }
}

Test_1 WELD_AT_OK
Test_1 WELD_BETWEEN_OK

Example 2

public class Test_2 {
    public static void m2(int a) {
        Robot r = new Robot(0, 7);
        if (2*a < 9 && a >= 0) {
            r.weldBetween(a, a + 1);
            if (a > 5) {
                r.weldAt(a + 4);
            }
        }
    }
}

Test_2 WELD_AT_OK
Test_2 WELD_BETWEEN_OK

Example 3

public class Test_3 {
    public static void m3(int a, int b) {
        Robot r = new Robot(-5, 5);
        if (a * b < 5 && a * b > -5 && b != 0) {
            r.weldAt(a + 1);
        }
    }
}

Test_3 WELD_AT_NOT_OK
Test_3 WELD_BETWEEN_OK

Project structure

You can download the template here.

It contains java files:

• ch.ethz.sae.Analysis - this class performs computation until a fixpoint is reached.
• ch.ethz.sae.Verifier - the main class. You check here if the two properties are satisfied.
• Test_1, Test_2, Test_3 - examples of applications your verifier should be able to reason about.

As the first step, compile and run the template. The output of the template is initially WELD_AT_NOT_OK and WELD_BETWEEN_NOT_OK, for any test class, which is very imprecise. The goal of the project is to follow the comments in the code, such that the project becomes more precise, soundly outputing WELD_AT_OK or WELD_BETWEEN_OK for test classes where we can guarantee it.

Running the code from the template:

• Install APRON
• See build.sh for instructions how to compile.
• See run.sh for instructions how to run from command line.
• There is an eclipse project included in the template. You can use it or create your own project.

Virtual machine

We provide a virtual machine where the whole environment and dependencies for the project are pre-installed. To use the virtual machine, first install: Virtual Box. Next, download the virtual machine: : VM.ova (3.3GB). Import the virtual machine and start it with VirtualBox. The username is sae and the password is also sae. The project folder is in /home/sae/project2. The virtual machine has Eclipse installed and the project is already set up there. To start eclipse, open a terminal and run eclipse. You can also compile and run the project from the command line, using the scripts build.sh and run.sh, respectively. The run.sh script takes a test class name as an argument.

Language Fragment to handle

• Details about the Jimple language can be found here
• The language fragment to handle is:

  Jimple Construct	Meaning
  DefinitionStmt	Definition Statement: here, you only need to handle integer assignments to a local variable. That is, x = y, or x = 5 or x = EXPR, where EXPR is one of the three binary expressions below. That is, you need to be able to hande: y = x + 5 or y = x * z.
  JMulExpr	Multiplication
  JSubExpr	Substraction
  JAddExpr	Addition
  JIfStmt	Conditional Statement. You need to handle conditionals where the condition can be any of the binary boolean expressions below. These conditions can again only mention integer local variables or constants, for example: if (x > y) or if (x <= 4), etc.
  JEqExpr	==
  JGeExpr	>=
  JGtExpr	>
  JLeExpr	<=
  JLtExpr	<
  JNeExpr	!=

• Loops are also allowed in the programs. Loops are already identified and widening is performed in the template.
• Assignments of pointers of type Robot are possible, e.g. p = q where p and q are of type reference. However, those are handled by the pointer analysis and you do not need to worry in the numerical analysis about these.
• When verifying if a method satisfies the properties, you need to handle calls to the methods weldAt, weldBetween, and calls to the constructor Robot.

APRON

Soot

Implementation tips

• It is sufficient to analyze one method at a time.
• You can assume the constructor Robot takes as arguments only integer constants (never local variables), between -10000 and 10000.
• It is enough to use the polyhedra domain that APRON provides (Polka) and analyze relations over the local integer variables.
• The methods of the control applications may contain loops and branches. You do not need to handle type casts or types other than the Java int type in your analysis.
• If you see an operation for which you are not precise - do not crash, but be less precise or go to top instead so that you remain sound.
• Only local variables need to be tracked for the numerical analysis (no global variables or object fields), but for the heap you need to use the existing pointer analysis of Soot. The template already contains the invocation of the pointer analysis. You just need to make sure to use that information for checking the properties.

Deliverables

• A zip file containing 3 files (Analysis.java, AWrapper.java, Verifier.java) with your implementation. The name of the zip file should be your team name. Your project should compile with the standard javac compiler of Java 6) The main class must be ch.ethz.sae.Verifier as in the template.
• Submit your projects by email to sae-assistants@lists.inf.ethz.ch. The email body should contain the names of all the members of your team.
• You cannot use any library other than soot-2.5 which we will test with. You need to use the transformers of the APRON polyhedra domain (Polka).
• Feel free to unit test your implemetation, but your program should not depend on JUnit to run. We will not pass JUnit to the classpath when testing.
• Your program will be run using OpenJDK Java 6 under Linux (keep in mind that Java 7 has a slightly different syntax). Also, pointer analysis runs faster under Java 6 than Java 7 (likely, due to fewer classes to analyze).
• There will be a time limit of 10 seconds to verify an application. Each application will consist of at most 10 methods.
• Project deadline June 9th 2017, 18:00

Grading:

• Evaluation of your tool on our own set of programs for which we know if they are valid or not.
• We will evaluate you depending on the correctness of your program and the precision of your solution. You will not get points if your program does not satisfy the requirements. If your solution is unsound (i.e. wrong - says that an unsafe code is safe), or imprecise (says unsafe for code, which is safe) we will penalize it in the points. We will penalize unsoundness much more than imprecision.

Project Assistance

Points