In this lab, you will start working on the Leon codebase directly. You will have to implement a series of simple tasks that will introduce you to the important classes and structures of the Leon verification system.

Please follow the instructions on Labs Setup to get started on this lab.

If you really, really, want to use Eclipse, follow these instructions: Eclipse Instructions.

Once you cloned your git repository you will find a rather big project. Here we will give you some information about the most important classes and packages that you will need to explore:

The sources can be found in src/main/scala/leon, under which you will find:

1. Main.scala: Entry point of Leon. Creates the pipeline and process some options.
2. purescala/ : Definition of all pureScala Trees and operations on the trees.
3. solvers/ : Definition and implementation of Solvers for Leon trees.
4. verification/: Construction of VCs for the verification of programs.
5. sav/: Definitions of the phase that we will work with here.

During this lab, you will spend most of your time working with classes from the purescala and sav packages.

Leon works using a pipeline of phases. Each phase can be seen as a function from Input to Output. For instance, the phase compiling the script given as argument to a Leon Tree is the plugin.ExtractionPhase, and its signature is List[String] ⇒ Program.

For this lab, we will plug our SAV phase directly after this. Our phase will perform transformations, so it is defined as Program ⇒ Program. We can see this pipeline Main.scala's computePipeline:

plugin.ExtractionPhase andThen sav.SAVPhase

If you run Leon with this pipeline, you will see the resulting program in the output. If we wish to perform verification after the SAV transformations, we can extend this pipeline using:

plugin.ExtractionPhase andThen sav.SAVPhase andThen verification.AnalysisPhase

Leon builds its own trees out of Scala ASTs. The definitions of these trees can be found in the purescala package: trees representing programs or functions declarations are found in purescala/Definitions.scala. You can for instance find the definition for the Program class there, which is given as input to your SAV phase.

The expression trees are defined in the purescala/Trees.scala file. They represent purely function programs. Leon unifies programs and formulae by handling them using the same trees.

Another very important file is purescala/TreeOps.scala which contains all kinds of operations on trees, including substitution, lookups, transformations, catamorphisms, …

You will need sbt 0.12.1 in order to compile Leon. You can either install this specific version of sbt, or use the https://github.com/paulp/sbt-extras package which simplifies this task, by auto-detecting and running the correct sbt version. Once sbt or sbt-extras is installed, compile Leon using:

$ sbt compile script

This should compile Leon and create two scripts, leon and setupenv. You should now be able to run Leon using:

$ ./leon --help

In this assignment you will work with Leon trees and perform several modifications to them. You are encouraged to look in the purescala package for functions that may help you implement the desired functionality.

Implement the function isRecursive(fi: FunctionInvocation) in SAVPhase that checks whether the call is made to a function that is recursive.

Inlining consists of replacing the call to a function by its body. Implement the inline(fi: FunctionInvocation) function in SAVPhase that returns the inlined code corresponding to the function call.

You can ignore potential pre/post conditions.

Implement the function simplifyArith(in: Expr) in SAVPhase that should look for arithmetic expressions and simplify them when possible.

Kinds of simplifications you will have to implement:

1. 1*v ⇒ v
2. 0*x ⇒ 0
3. v/1 ⇒ v
4. v+0 ⇒ v
5. v-0 ⇒ v
6. 42+42 ⇒ 84 or any kind of arithmetic static computations.
7. (0 == 1) ⇒ false

For this you will have to implement a tree transformer, take a close look to TreeOps functions simplePreTransform and simplePostTransform, and how they can be used.

Implement the autoInline(in: Expr) function. This function should inline all function calls to non-recursive functions found in in and return the updated code.

Once this function is implemented, you will need to traverse all the defined functions in the Program and apply autoInline to all defined bodies. Note that this inlining should be done transitively on all non-recursive calls. Return the resulting Program as result of the phase.

Deadline: Friday, Mar. 8th, 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 “Lab02 - Introduction” 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.