You will have to pull this new phase (along with several other Leon-wide changes) from the sav2013-main repository. This will bootstrap your work.

You need to update your repository according to our recent changes in order to prepare for this lab (follow the instructions). It should merge, along with other sporadic changes, the following file which contains the phase you will have to implement during this lab:

• sav/ExposeTimePhase.scala

This phase runs between Extraction and Verification. If you manually modified Main.scala, pulling might create conflicts there.

In this lab, you will implement a program transformation phase that will allow Leon users to seamlessly reason about the execution time of their functions. You will have to transform the program such that every functions will also compute their execution time along with their normal return value. The execution time is computed as an integer number of steps.

Essentially, this means that you will have to implement a phase that rewrites:

f : (A,B) => C

into

f : (A,B) => (C, Int)

You will then be able to reference this extra return value in the post-conditions using a new magic variable: time.

For instance, consider the function contains on a standard List, you would, with this extra phase, be able to reason about the number of steps required by contains, in the post condition:

def contains(l: List, v: Int): Boolean = (l match {
  case Nil() => false
  case Cons(h, t) => v == h || contains(t, v)
}) ensuring { res => time <= (2 + 10*size(l)) }

The first step is to temporarily create a new program with functions updated to their new signature. These functions will have empty bodies for now.

When computing the number of steps a function takes, you will need to assign a cost to each node of the tree.

costOf(e: Expr): Int

For instance, the Tree Add(IntLiteral(1), Variable(x)) will be given a cost of:

costOf(Add(..,..)) + costOf(IntLiteral(1)) + costOf(Variable(x))

Even though we pass the full expressions to costOf, you should only have to look at the kind of the toplevel node. For instance, costOf(Add(x,y)) should return the cost of Add irregardless of x and y, since costOf will also be invoked separately on x and y.

The main part of this lab will be to transform the trees to include an execution time for each function. In order to do this, any expressions returning X in trees will have to be transformed from X to (X, T). You will have to complete the implementation of the main transformation method: transform, and its helper function tupleify.

To illustrate this transformation, we give you as example the transformation of Let expressions:

Let(i, ..value.., ..body..)

becomes:

LetTuple((ir, it), transform(v),
  LetTuple((r, t), replace(i -> ir, trasform(b)),
    Tuple((r, t + it + costOf(Let)))
  )
)

This function is also already implemented in the stubs.

The cost of the result of If depends on the branch taken. You however need to count the cost of the condition in both branches.

You need to call the new function using the map and use its second return value accordingly.

You can ignore LetTuple trees

Pattern matchin get translated to equivalent If expressions before your transformation, you can therefore ignore trees representing pattern matching.

For simplicity, you can consider than short-circuiting operators such as && and || are not short-circuiting in terms of execution time. This means that bar() && foo() will always consider the cost of both bar() and foo() in the resulting expression's cost, no matter what bar() returns.

For all other trees, you are encouraged to handle them through generic operation extractors (NAryOperator/BinaryOperator/UnaryOperator/Terminal) and using the tupleify helper. Feel free to diverge from this approach if you feel your solution is cleaner.

Leon can be picky about the types of certain trees. Make sure that you set the type to all fresh identifiers you create. If the type error includes [???], it means one of the subtree is not typed correctly. You might have to force the type to tuples you create as well.

You can use the test available in examples/TestTimes.scala to test your implementation. Every functions in this example should verify.

Please note that depending on your cost-model, it might not be able to prove certain conditions as-is, simply due to the fact that your cost model returns higher costs than the one we used. You may need to increase the constant integers in the post-conditions of the example to match your cost model.

Deadline: Friday, Apr. 5th, 23.59pm.

You must use the interface on http://larasrv05.epfl.ch/sav13 as follows:

1. Click on the “Deliverables” tab
2. Click “Deliver this version” on the commit hash corresponding to the version of your code you want to submit
3. In the dialog, make sure “Lab03 - Exposing Execution Time” is selected, write a comment if you want
4. Click on “Create Deliverable”

Note: You can deliver as many times as you want, we will only consider the last deliverable.