Software Architecture and Engineering Project 2: Static Analysis

Project Scores

Project Description

• setSpeed(v) - sets the speed of the car to value v.

public class Car {    
    public native void setSpeed(int v);
}

Example 1

public class Example1 {
    public static Car test(int i) {	
        Car car = new Car();
        if (i < 5) {
            car.setSpeed(i);
        }
        return car;
    }
}

4

Example 2

public class Example2 {
    public static Car m1(int j) {
        Car car = new Car();
        return car;	
    }
}

NO SPEED SET

Example 3

public class Example3 {
    public static Car m1(int j) {
        Car car = new Car();
        car.setSpeed(j);
        return car;
    }
}

2147483647

Example 4

public class Example4 {
    public static Car m1(int j) {
        Car b = new Car();
        if (j == 2*j + 1) {
            b.setSpeed(j);
        } else {
            b.setSpeed(-2);
        }
        Car c = b;
        return c;
    }
}

-1

Example 5

public class Example5 {
    public static Car m1(int j) {
        Car b = new Car();
        if (j == j + 1) {
            b.setSpeed(j);
        }
        return b;
    }
}

NO SPEED SET

Project structure

The project consists of the following java files:

• ch.ethz.sae.Analysis - this class performs computation until a fixpoint is reached, using Soot and Apron.
• ch.ethz.sae.Verifier - the main class. You check here if the two properties are satisfied.
• Example1, Example2, Example3, Example4, Example5 - examples given above.

As the first step, compile and run the template. The output of the template is initially NO SPEED SET for any test class. The goal of the project is to soundly output upper bounds or NO SPEED SET for test classes where we can guarantee it.

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: : SAE-2018.ova (5GB). 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/project-2018/. The virtual machine has Eclipse installed and the project is already set up there. 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 (e.g. ./run.sh Example1).

If you do not want to use the VM, follow the instructions here.

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	!=
  JInvokeStmt	Method invocation (only setSpeed(v))
  JReturnStmt	Return statement

• Loops are also allowed in the programs. Loops are already identified and widening is performed in the template.
• Assignments of pointers of type Car are possible, e.g. p = q where p and q are objects of class Car. 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 analyse invocations of the method setSpeed and return statements.

APRON

Soot

Implementation tips

• It is sufficient to analyze one test method at a time. There are no recursive method calls. The only types of method calls in a test method are setSpeed and the Car constructor.
• It is enough to use the polyhedra domain that APRON provides (Polka) and analyze relations over the local integer variables.
• The polyhedra domain is imprecise when handling the != operation, because polyhedra elements do not contain disjunctions. For some cases, you can look for a simple workaround for this limitation.
• 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 when computing the upper bound. The pointer analysis in flow insensitive.
• There are no null pointer dereferences in the test methods and the return value of test methods is always different than null.
• The test methods are always static methods.

Deliverables

• A zip file containing the src folder of your project (including Analysis.java, AWrapper.java, Verifier.java). 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 VM.
• 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 5 seconds to verify a test class.
• Project deadline June 1st, 2018. 5pm

Grading:

• Evaluation of your tool on our own set of programs for which we know a precise upper bound.
• 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 - the output is not an upper bound), or imprecise (the returned bound is imprecise) we will penalize it in the points. We will penalize unsoundness much more than imprecision.

Project Assistance