Skip to content
Snippets Groups Projects
  • Manos Koukoutos's avatar
    f9aa132c
    Support FiniteArray in CodeGen · f9aa132c
    Manos Koukoutos authored
    NonEmptyArray is required to be nonempty
    Allow arbitrary expression as length in CodeGeneration
    Handle FiniteArray in valueToJVM
    Add integration tests
    finiteArray makes EmptyArray for arrays of size 0
    Fail when z3 returns negative size array
    f9aa132c
    History
    Support FiniteArray in CodeGen
    Manos Koukoutos authored
    NonEmptyArray is required to be nonempty
    Allow arbitrary expression as length in CodeGeneration
    Handle FiniteArray in valueToJVM
    Add integration tests
    finiteArray makes EmptyArray for arrays of size 0
    Fail when z3 returns negative size array
CodeGeneration.scala 58.89 KiB
/* Copyright 2009-2015 EPFL, Lausanne */

package leon
package codegen

import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps.{simplestValue, matchToIfThenElse, collect}
import purescala.Types._
import purescala.Constructors._
import purescala.Extractors._
import purescala.Quantification._

import cafebabe._
import cafebabe.AbstractByteCodes._
import cafebabe.ByteCodes._
import cafebabe.ClassFileTypes._
import cafebabe.Defaults.constructorName
import cafebabe.Flags._

trait CodeGeneration {
  self: CompilationUnit =>

  /** A class providing information about the status of parameters in the function that is being currently compiled.
   *  vars is a mapping from local variables/ parameters to the offset of the respective JVM local register
   *  isStatic signifies if the current method is static (a function, in Leon terms)
   */
  class Locals private[codegen] (
    vars   : Map[Identifier, Int],
    args   : Map[Identifier, Int],
    fields : Map[Identifier, (String,String,String)]
  ) {
    /** Fetches the offset of a local variable/ parameter from its identifier */
    def varToLocal(v: Identifier): Option[Int] = vars.get(v)

    def varToArg(v: Identifier): Option[Int] = args.get(v)

    def varToField(v: Identifier): Option[(String,String,String)] = fields.get(v)

    /** Adds some extra variables to the mapping */
    def withVars(newVars: Map[Identifier, Int]) = new Locals(vars ++ newVars, args, fields)

    /** Adds an extra variable to the mapping */
    def withVar(nv: (Identifier, Int)) = new Locals(vars + nv, args, fields)

    def withArgs(newArgs: Map[Identifier, Int]) = new Locals(vars, args ++ newArgs, fields)

    def withFields(newFields: Map[Identifier,(String,String,String)]) = new Locals(vars, args, fields ++ newFields)
  }

  object NoLocals extends Locals(Map.empty, Map.empty, Map.empty)

  lazy val monitorID = FreshIdentifier("__$monitor")

  private[codegen] val ObjectClass               = "java/lang/Object"
  private[codegen] val BoxedIntClass             = "java/lang/Integer"
  private[codegen] val BoxedBoolClass            = "java/lang/Boolean"
  private[codegen] val BoxedCharClass            = "java/lang/Character"
  private[codegen] val BoxedArrayClass           = "leon/codegen/runtime/ArrayBox"

  private[codegen] val JavaListClass             = "java/util/List"
  private[codegen] val JavaIteratorClass         = "java/util/Iterator"

  private[codegen] val TupleClass                = "leon/codegen/runtime/Tuple"
  private[codegen] val SetClass                  = "leon/codegen/runtime/Set"
  private[codegen] val MapClass                  = "leon/codegen/runtime/Map"
  private[codegen] val BigIntClass               = "leon/codegen/runtime/BigInt"
  private[codegen] val RealClass                 = "leon/codegen/runtime/Real"
  private[codegen] val RationalClass             = "leon/codegen/runtime/Rational"
  private[codegen] val CaseClassClass            = "leon/codegen/runtime/CaseClass"
  private[codegen] val LambdaClass               = "leon/codegen/runtime/Lambda"
  private[codegen] val ErrorClass                = "leon/codegen/runtime/LeonCodeGenRuntimeException"
  private[codegen] val ImpossibleEvaluationClass = "leon/codegen/runtime/LeonCodeGenEvaluationException"
  private[codegen] val HashingClass              = "leon/codegen/runtime/LeonCodeGenRuntimeHashing"
  private[codegen] val ChooseEntryPointClass     = "leon/codegen/runtime/ChooseEntryPoint"
  private[codegen] val GenericValuesClass        = "leon/codegen/runtime/GenericValues"
  private[codegen] val MonitorClass              = "leon/codegen/runtime/LeonCodeGenRuntimeMonitor"
  private[codegen] val HenkinClass               = "leon/codegen/runtime/LeonCodeGenRuntimeHenkinMonitor"

  def idToSafeJVMName(id: Identifier) = {
    scala.reflect.NameTransformer.encode(id.uniqueName).replaceAll("\\.", "\\$")
  }
  def defToJVMName(d : Definition) : String = "Leon$CodeGen$" + idToSafeJVMName(d.id)

  /** Retrieve the name of the underlying lazy field from a lazy field accessor method */
  private[codegen] def underlyingField(lazyAccessor : String) = lazyAccessor + "$underlying"

  protected object ValueType {
    def unapply(tp: TypeTree): Boolean = tp match {
      case Int32Type | BooleanType | CharType | UnitType => true
      case _ => false
    }
  }

  /** Return the respective JVM type from a Leon type */
  def typeToJVM(tpe : TypeTree) : String = tpe match {
    case Int32Type => "I"

    case BooleanType => "Z"

    case CharType => "C"

    case UnitType => "Z"

    case c : ClassType =>
      leonClassToJVMInfo(c.classDef).map { case (n, _) => "L" + n + ";" }.getOrElse(
        throw CompilationException("Unsupported class " + c.id)
      )

    case _ : TupleType =>
      "L" + TupleClass + ";"

    case _ : SetType =>
      "L" + SetClass + ";"

    case _ : MapType =>
      "L" + MapClass + ";"

    case IntegerType =>
      "L" + BigIntClass + ";"

    case RealType =>
      "L" + RationalClass + ";"

    case _ : FunctionType =>
      "L" + LambdaClass + ";"

    case ArrayType(base) =>
      "[" + typeToJVM(base)

    case TypeParameter(_) =>
      "L" + ObjectClass + ";"

    case _ => throw CompilationException("Unsupported type : " + tpe)
  }

  /** Return the respective boxed JVM type from a Leon type */
  def typeToJVMBoxed(tpe : TypeTree) : String = tpe match {
    case Int32Type              => s"L$BoxedIntClass;"
    case BooleanType | UnitType => s"L$BoxedBoolClass;"
    case CharType               => s"L$BoxedCharClass;"
    case other                  => typeToJVM(other)
  }

  /**
   * Compiles a function/method definition.
   * @param funDef The function definition to be compiled
   * @param owner The module/class that contains `funDef`
   */
  def compileFunDef(funDef: FunDef, owner: Definition) {
    val isStatic = owner.isInstanceOf[ModuleDef]

    val cf = classes(owner)
    val (_,mn,_) = leonFunDefToJVMInfo(funDef).get

    val paramsTypes = funDef.params.map(a => typeToJVM(a.getType))

    val realParams = if (requireMonitor) {
      ("L" + MonitorClass + ";") +: paramsTypes
    } else {
      paramsTypes
    }

    val m = cf.addMethod(
      typeToJVM(funDef.returnType),
      mn,
      realParams : _*
    )
    m.setFlags((
      // FIXME Not sure about this "FINAL" now that we can have methods in inheritable classes
      if (isStatic)
        METHOD_ACC_PUBLIC |
        METHOD_ACC_FINAL  |
        METHOD_ACC_STATIC
      else
        METHOD_ACC_PUBLIC |
        METHOD_ACC_FINAL
    ).asInstanceOf[U2])

    val ch = m.codeHandler

    // An offset we introduce to the parameters:
    // 1 if this is a method, so we need "this" in position 0 of the stack
    // 1 if we are monitoring
    val idParams = (if (requireMonitor) Seq(monitorID) else Seq.empty) ++ funDef.params.map(_.id)
    val newMapping = idParams.zipWithIndex.toMap.mapValues(_ + (if (!isStatic) 1 else 0))

    val body = funDef.body.getOrElse(throw CompilationException("Can't compile a FunDef without body: "+funDef.id.name))

    val bodyWithPre = if(funDef.hasPrecondition && params.checkContracts) {
      IfExpr(funDef.precondition.get, body, Error(body.getType, "Precondition failed"))
    } else {
      body
    }

    val bodyWithPost = funDef.postcondition match {
      case Some(post) if params.checkContracts =>
        Ensuring(bodyWithPre, post).toAssert
      case _ => bodyWithPre
    }

    val locals = NoLocals.withVars(newMapping)

    if (params.recordInvocations) {
      load(monitorID, ch)(locals)
      ch << InvokeVirtual(MonitorClass, "onInvoke", "()V")
    }

    mkExpr(bodyWithPost, ch)(locals)

    funDef.returnType match {
      case ValueType() =>
        ch << IRETURN

      case _ =>
        ch << ARETURN
    }

    ch.freeze
  }

  private[codegen] val lambdaToClass = scala.collection.mutable.Map.empty[Lambda, String]
  private[codegen] val classToLambda = scala.collection.mutable.Map.empty[String, Lambda]

  private def compileLambda(l: Lambda, ch: CodeHandler)(implicit locals: Locals): Unit = {
    val (normalized, structSubst) = purescala.ExprOps.normalizeStructure(l)
    val reverseSubst = structSubst.map(p => p._2 -> p._1)
    val nl = normalized.asInstanceOf[Lambda]

    val closureIDs = purescala.ExprOps.variablesOf(nl).toSeq.sortBy(_.uniqueName)
    val closuresWithoutMonitor = closureIDs.map(id => id -> typeToJVM(id.getType))
    val closures = if (requireMonitor) {
      (monitorID -> s"L$MonitorClass;") +: closuresWithoutMonitor
    } else closuresWithoutMonitor

    val afName = lambdaToClass.getOrElse(nl, {
      val afName = "Leon$CodeGen$Lambda$" + lambdaCounter.nextGlobal
      lambdaToClass += nl -> afName
      classToLambda += afName -> nl

      val cf = new ClassFile(afName, Some(LambdaClass))

      cf.setFlags((
        CLASS_ACC_SUPER |
        CLASS_ACC_PUBLIC |
        CLASS_ACC_FINAL
      ).asInstanceOf[U2])

      if (closures.isEmpty) {
        cf.addDefaultConstructor
      } else {
        for ((id, jvmt) <- closures) {
          val fh = cf.addField(jvmt, id.uniqueName)
          fh.setFlags((
            FIELD_ACC_PUBLIC |
            FIELD_ACC_FINAL
          ).asInstanceOf[U2])
        }

        val cch = cf.addConstructor(closures.map(_._2).toList).codeHandler

        cch << ALoad(0)
        cch << InvokeSpecial(LambdaClass, constructorName, "()V")

        var c = 1
        for ((id, jvmt) <- closures) {
          cch << ALoad(0)
          cch << (jvmt match {
            case "I" | "Z" => ILoad(c)
            case _ => ALoad(c)
          })
          cch << PutField(afName, id.uniqueName, jvmt)
          c += 1
        }

        cch << RETURN
        cch.freeze
      }
      locally {
        val apm = cf.addMethod(s"L$ObjectClass;", "apply", s"[L$ObjectClass;")

        apm.setFlags((
          METHOD_ACC_PUBLIC |
          METHOD_ACC_FINAL
        ).asInstanceOf[U2])

        val argMapping = nl.args.map(_.id).zipWithIndex.toMap
        val closureMapping = closures.map { case (id, jvmt) => id -> (afName, id.uniqueName, jvmt) }.toMap

        val newLocals = locals.withArgs(argMapping).withFields(closureMapping)

        val apch = apm.codeHandler

        mkBoxedExpr(nl.body, apch)(newLocals)

        apch << ARETURN

        apch.freeze
      }

      locally {
        val emh = cf.addMethod("Z", "equals", s"L$ObjectClass;")
        emh.setFlags((
          METHOD_ACC_PUBLIC |
          METHOD_ACC_FINAL
        ).asInstanceOf[U2])

        val ech = emh.codeHandler

        val notRefEq = ech.getFreshLabel("notrefeq")
        val notEq = ech.getFreshLabel("noteq")
        val castSlot = ech.getFreshVar

        // If references are equal, trees are equal.
        ech << ALoad(0) << ALoad(1) << If_ACmpNe(notRefEq) << Ldc(1) << IRETURN << Label(notRefEq)

        // We check the type (this also checks against null)....
        ech << ALoad(1) << InstanceOf(afName) << IfEq(notEq)

        // ...finally, we compare fields one by one, shortcircuiting on disequalities.
        if(closures.nonEmpty) {
          ech << ALoad(1) << CheckCast(afName) << AStore(castSlot)

          for((id,jvmt) <- closures) {
            ech << ALoad(0) << GetField(afName, id.uniqueName, jvmt)
            ech << ALoad(castSlot) << GetField(afName, id.uniqueName, jvmt)

            jvmt match {
              case "I" | "Z" =>
                ech << If_ICmpNe(notEq)

              case ot =>
                ech << InvokeVirtual(ObjectClass, "equals", s"(L$ObjectClass;)Z") << IfEq(notEq)
            }
          }
        }

        ech << Ldc(1) << IRETURN << Label(notEq) << Ldc(0) << IRETURN
        ech.freeze
      }

      locally {
        val hashFieldName = "$leon$hashCode"
        cf.addField("I", hashFieldName).setFlags(FIELD_ACC_PRIVATE)
        val hmh = cf.addMethod("I", "hashCode", "")
        hmh.setFlags((
          METHOD_ACC_PUBLIC |
          METHOD_ACC_FINAL
        ).asInstanceOf[U2])

        val hch = hmh.codeHandler

        val wasNotCached = hch.getFreshLabel("wasNotCached")

        hch << ALoad(0) << GetField(afName, hashFieldName, "I") << DUP
        hch << IfEq(wasNotCached)
        hch << IRETURN
        hch << Label(wasNotCached) << POP

        hch << Ldc(closuresWithoutMonitor.size) << NewArray(s"$ObjectClass")
        for (((id, jvmt),i) <- closuresWithoutMonitor.zipWithIndex) {
          hch << DUP << Ldc(i)
          hch << ALoad(0) << GetField(afName, id.uniqueName, jvmt)
          mkBox(id.getType, hch)
          hch << AASTORE
        }

        hch << Ldc(afName.hashCode)
        hch << InvokeStatic(HashingClass, "seqHash", s"([L$ObjectClass;I)I") << DUP
        hch << ALoad(0) << SWAP << PutField(afName, hashFieldName, "I")
        hch << IRETURN

        hch.freeze
      }

      loader.register(cf)

      afName
    })

    val consSig = "(" + closures.map(_._2).mkString("") + ")V"

    ch << New(afName) << DUP
    for ((id,jvmt) <- closures) {
      if (id == monitorID) {
        load(monitorID, ch)
      } else {
        mkExpr(Variable(reverseSubst(id)), ch)
      }
    }
    ch << InvokeSpecial(afName, constructorName, consSig)
  }

  private val typeIdCache = scala.collection.mutable.Map.empty[TypeTree, Int]
  private[codegen] def typeId(tpe: TypeTree): Int = typeIdCache.get(tpe) match {
    case Some(id) => id
    case None =>
      val id = typeIdCache.size
      typeIdCache += tpe -> id
      id
  }

  private def compileForall(f: Forall, ch: CodeHandler)(implicit locals: Locals): Unit = {
    // make sure we have an available HenkinModel
    val monitorOk = ch.getFreshLabel("monitorOk")
    load(monitorID, ch)
    ch << InstanceOf(HenkinClass) << IfNe(monitorOk)
    ch << New(ImpossibleEvaluationClass) << DUP
    ch << Ldc("Can't evaluate foralls without domain")
    ch << InvokeSpecial(ImpossibleEvaluationClass, constructorName, "(Ljava/lang/String;)V")
    ch << ATHROW
    ch << Label(monitorOk)

    val Forall(fargs, TopLevelAnds(conjuncts)) = f
    val endLabel = ch.getFreshLabel("forallEnd")

    for (conj <- conjuncts) {
      val vars = purescala.ExprOps.variablesOf(conj)
      val args = fargs.map(_.id).filter(vars)
      val quantified = args.toSet

      val matchQuorums = extractQuorums(conj, quantified)

      val matcherIndexes = matchQuorums.flatten.distinct.zipWithIndex.toMap

      def buildLoops(
        mis: List[(Expr, Seq[Expr], Int)],
        localMapping: Map[Identifier, Int],
        pointerMapping: Map[(Int, Int), Identifier]
      ): Unit = mis match {
        case (expr, args, qidx) :: rest =>
          load(monitorID, ch)
          ch << CheckCast(HenkinClass)

          mkExpr(expr, ch)
          ch << Ldc(typeId(expr.getType))
          ch << InvokeVirtual(HenkinClass, "domain", s"(L$ObjectClass;I)L$JavaListClass;")
          ch << InvokeInterface(JavaListClass, "iterator", s"()L$JavaIteratorClass;")

          val loop = ch.getFreshLabel("loop")
          val out = ch.getFreshLabel("out")
          ch << Label(loop)
          // it
          ch << DUP
          // it, it
          ch << InvokeInterface(JavaIteratorClass, "hasNext", "()Z")
          // it, hasNext
          ch << IfEq(out) << DUP
          // it, it
          ch << InvokeInterface(JavaIteratorClass, "next", s"()L$ObjectClass;")
          // it, elem
          ch << CheckCast(TupleClass)

          val (newLoc, newPtr) = (for ((arg, aidx) <- args.zipWithIndex) yield {
            val id = FreshIdentifier("q", arg.getType, true)
            val slot = ch.getFreshVar

            ch << DUP << Ldc(aidx) << InvokeVirtual(TupleClass, "get", s"(I)L$ObjectClass;")
            mkUnbox(arg.getType, ch)
            ch << (typeToJVM(arg.getType) match {
              case "I" | "Z" => IStore(slot)
              case _ => AStore(slot)
            })

            (id -> slot, (qidx -> aidx) -> id)
          }).unzip

          ch << POP
          // it

          buildLoops(rest, localMapping ++ newLoc, pointerMapping ++ newPtr)

          ch << Goto(loop)
          ch << Label(out) << POP

        case Nil =>
          var okLabel: Option[String] = None
          for (quorum <- matchQuorums) {
            okLabel.foreach(ok => ch << Label(ok))
            okLabel = Some(ch.getFreshLabel("quorumOk"))

            var mappings: Seq[(Identifier, Int, Int)] = Seq.empty
            var constraints: Seq[(Expr, Int, Int)] = Seq.empty
            var equalities: Seq[((Int, Int), (Int, Int))] = Seq.empty

            for (q @ (expr, args) <- quorum) {
              val qidx = matcherIndexes(q)
              val (qmappings, qconstraints) = args.zipWithIndex.partition {
                case (Variable(id), aidx) => quantified(id)
                case _ => false
              }

              mappings ++= qmappings.map(p => (p._1.asInstanceOf[Variable].id, qidx, p._2))
              constraints ++= qconstraints.map(p => (p._1, qidx, p._2))
            }

            val mapping = for ((id, es) <- mappings.groupBy(_._1)) yield {
              val base :: others = es.toList.map(p => (p._2, p._3))
              equalities ++= others.map(p => base -> p)
              (id -> base)
            }

            val enabler = andJoin(constraints.map {
              case (e, qidx, aidx) => Equals(e, pointerMapping(qidx -> aidx).toVariable)
            } ++ equalities.map {
              case (k1, k2) => Equals(pointerMapping(k1).toVariable, pointerMapping(k2).toVariable)
            })

            mkExpr(enabler, ch)(locals.withVars(localMapping))
            ch << IfEq(okLabel.get)

            val varsMap = args.map(id => id -> localMapping(pointerMapping(mapping(id)))).toMap
            mkExpr(conj, ch)(locals.withVars(varsMap))
            ch << IfNe(okLabel.get)

            // -- Forall is false! --
            // POP all the iterators...
            for (_ <- List.range(0, matcherIndexes.size)) ch << POP

            // ... and return false
            ch << Ldc(0) << Goto(endLabel)
          }

          ch << Label(okLabel.get)
      }

      buildLoops(matcherIndexes.toList.map { case ((e, as), idx) => (e, as, idx) }, Map.empty, Map.empty)
    }

    ch << Ldc(1) << Label(endLabel)
  }

  private[codegen] def mkExpr(e: Expr, ch: CodeHandler, canDelegateToMkBranch: Boolean = true)(implicit locals: Locals) {
    e match {
      case Variable(id) =>
        load(id, ch)

      case Assert(cond, oerr, body) =>
        mkExpr(IfExpr(Not(cond), Error(body.getType, oerr.getOrElse("Assertion failed @"+e.getPos)), body), ch)

      case en @ Ensuring(_, _) =>
        mkExpr(en.toAssert, ch)

      case Let(i,d,b) =>
        mkExpr(d, ch)
        val slot = ch.getFreshVar
        val instr = i.getType match {
          case ValueType() => IStore(slot)
          case _ => AStore(slot)
        }
        ch << instr
        mkExpr(b, ch)(locals.withVar(i -> slot))

      case IntLiteral(v) =>
        ch << Ldc(v)

      case CharLiteral(v) =>
        ch << Ldc(v)

      case BooleanLiteral(v) =>
        ch << Ldc(if(v) 1 else 0)

      case UnitLiteral() =>
        ch << Ldc(1)

      case InfiniteIntegerLiteral(v) =>
        ch << New(BigIntClass) << DUP
        ch << Ldc(v.toString)
        ch << InvokeSpecial(BigIntClass, constructorName, "(Ljava/lang/String;)V")

      case FractionalLiteral(n, d) =>
        ch << New(RationalClass) << DUP
        ch << Ldc(n.toString)
        ch << Ldc(d.toString)
        ch << InvokeSpecial(RationalClass, constructorName, "(Ljava/lang/String;Ljava/lang/String;)V")

      // Case classes
      case CaseClass(cct, as) =>
        val (ccName, ccApplySig) = leonClassToJVMInfo(cct.classDef).getOrElse {
          throw CompilationException("Unknown class : " + cct.id)
        }
        ch << New(ccName) << DUP
        if (requireMonitor) {
          load(monitorID, ch)
        }

        for((a, vd) <- as zip cct.classDef.fields) {
          vd.getType match {
            case TypeParameter(_) =>
              mkBoxedExpr(a, ch)
            case _ =>
              mkExpr(a, ch)
          }
        }
        ch << InvokeSpecial(ccName, constructorName, ccApplySig)

      case IsInstanceOf(e, cct) =>
        val (ccName, _) = leonClassToJVMInfo(cct.classDef).getOrElse {
          throw CompilationException("Unknown class : " + cct.id)
        }
        mkExpr(e, ch)
        ch << InstanceOf(ccName)

      case AsInstanceOf(e, cct) =>
        val (ccName, _) = leonClassToJVMInfo(cct.classDef).getOrElse {
          throw CompilationException("Unknown class : " + cct.id)
        }
        mkExpr(e, ch)
        ch << CheckCast(ccName)

      case CaseClassSelector(cct, e, sid) =>
        mkExpr(e, ch)
        val (ccName, _) = leonClassToJVMInfo(cct.classDef).getOrElse {
          throw CompilationException("Unknown class : " + cct.id)
        }
        ch << CheckCast(ccName)
        instrumentedGetField(ch, cct, sid)

      // Tuples (note that instanceOf checks are in mkBranch)
      case Tuple(es) =>
        ch << New(TupleClass) << DUP
        ch << Ldc(es.size)
        ch << NewArray(s"$ObjectClass")
        for((e,i) <- es.zipWithIndex) {
          ch << DUP
          ch << Ldc(i)
          mkBoxedExpr(e, ch)
          ch << AASTORE
        }
        ch << InvokeSpecial(TupleClass, constructorName, s"([L$ObjectClass;)V")

      case TupleSelect(t, i) =>
        val TupleType(bs) = t.getType
        mkExpr(t,ch)
        ch << Ldc(i - 1)
        ch << InvokeVirtual(TupleClass, "get", s"(I)L$ObjectClass;")
        mkUnbox(bs(i - 1), ch)

      // Sets
      case FiniteSet(es, _) =>
        ch << DefaultNew(SetClass)
        for(e <- es) {
          ch << DUP
          mkBoxedExpr(e, ch)
          ch << InvokeVirtual(SetClass, "add", s"(L$ObjectClass;)V")
        }

      case ElementOfSet(e, s) =>
        mkExpr(s, ch)
        mkBoxedExpr(e, ch)
        ch << InvokeVirtual(SetClass, "contains", s"(L$ObjectClass;)Z")

      case SetCardinality(s) =>
        mkExpr(s, ch)
        ch << InvokeVirtual(SetClass, "size", "()I")

      case SubsetOf(s1, s2) =>
        mkExpr(s1, ch)
        mkExpr(s2, ch)
        ch << InvokeVirtual(SetClass, "subsetOf", s"(L$SetClass;)Z")

      case SetIntersection(s1, s2) =>
        mkExpr(s1, ch)
        mkExpr(s2, ch)
        ch << InvokeVirtual(SetClass, "intersect", s"(L$SetClass;)L$SetClass;")

      case SetUnion(s1, s2) =>
        mkExpr(s1, ch)
        mkExpr(s2, ch)
        ch << InvokeVirtual(SetClass, "union", s"(L$SetClass;)L$SetClass;")

      case SetDifference(s1, s2) =>
        mkExpr(s1, ch)
        mkExpr(s2, ch)
        ch << InvokeVirtual(SetClass, "minus", s"(L$SetClass;)L$SetClass;")

      // Maps
      case FiniteMap(ss, _, _) =>
        ch << DefaultNew(MapClass)
        for((f,t) <- ss) {
          ch << DUP
          mkBoxedExpr(f, ch)
          mkBoxedExpr(t, ch)
          ch << InvokeVirtual(MapClass, "add", s"(L$ObjectClass;L$ObjectClass;)V")
        }

      case MapApply(m, k) =>
        val MapType(_, tt) = m.getType
        mkExpr(m, ch)
        mkBoxedExpr(k, ch)
        ch << InvokeVirtual(MapClass, "get", s"(L$ObjectClass;)L$ObjectClass;")
        mkUnbox(tt, ch)

      case MapIsDefinedAt(m, k) =>
        mkExpr(m, ch)
        mkBoxedExpr(k, ch)
        ch << InvokeVirtual(MapClass, "isDefinedAt", s"(L$ObjectClass;)Z")
      case MapUnion(m1, m2) =>
        mkExpr(m1, ch)
        mkExpr(m2, ch)
        ch << InvokeVirtual(MapClass, "union", s"(L$MapClass;)L$MapClass;")

      // Branching
      case IfExpr(c, t, e) =>
        val tl = ch.getFreshLabel("then")
        val el = ch.getFreshLabel("else")
        val al = ch.getFreshLabel("after")
        mkBranch(c, tl, el, ch)
        ch << Label(tl)
        mkExpr(t, ch)
        ch << Goto(al) << Label(el)
        mkExpr(e, ch)
        ch << Label(al)

      // Strict static fields
      case FunctionInvocation(tfd, as) if tfd.fd.canBeStrictField =>
        val (className, fieldName, _) = leonFunDefToJVMInfo(tfd.fd).getOrElse {
          throw CompilationException("Unknown method : " + tfd.id)
        }

        if (requireMonitor) {
          load(monitorID, ch)
          ch << InvokeVirtual(MonitorClass, "onInvoke", "()V")
        }

        // Get static field
        ch << GetStatic(className, fieldName, typeToJVM(tfd.fd.returnType))

        // unbox field
        (tfd.fd.returnType, tfd.returnType) match {
          case (TypeParameter(_), tpe)  =>
            mkUnbox(tpe, ch)
          case _ =>
        }

      case FunctionInvocation(TypedFunDef(fd, Seq(tp)), Seq(set)) if fd == program.library.setToList.get =>

        val nil = CaseClass(CaseClassType(program.library.Nil.get, Seq(tp)), Seq())
        val cons = program.library.Cons.get
        val (consName, ccApplySig) = leonClassToJVMInfo(cons).getOrElse {
          throw CompilationException("Unknown class : " + cons)
        }

        mkExpr(nil, ch)
        mkExpr(set, ch)
        //if (params.requireMonitor) {
        //  ch << ALoad(locals.monitorIndex)
        //}

        // No dynamic dispatching/overriding in Leon,
        // so no need to take care of own vs. "super" methods
        ch << InvokeVirtual(SetClass, "getElements", s"()L$JavaIteratorClass;")

        val loop = ch.getFreshLabel("loop")
        val out = ch.getFreshLabel("out")
        ch << Label(loop)
        // list, it
        ch << DUP
        // list, it, it
        ch << InvokeInterface(JavaIteratorClass, "hasNext", "()Z")
        // list, it, hasNext
        ch << IfEq(out)
        // list, it
        ch << DUP2
        // list, it, list, it
        ch << InvokeInterface(JavaIteratorClass, "next", s"()L$ObjectClass;") << SWAP
        // list, it, elem, list
        ch << New(consName) << DUP << DUP2_X2
        // list, it, cons, cons, elem, list, cons, cons
        ch << POP << POP
        // list, it, cons, cons, elem, list

        if (requireMonitor) {
          load(monitorID, ch)
          ch << DUP_X2 << POP
        }
        ch << InvokeSpecial(consName, constructorName, ccApplySig)
        // list, it, newList
        ch << DUP_X2 << POP << SWAP << POP
        // newList, it
        ch << Goto(loop)

        ch << Label(out)
        // list, it
        ch << POP
        // list

      // Static lazy fields/ functions
      case fi @ FunctionInvocation(tfd, as) =>
        val (cn, mn, ms) = leonFunDefToJVMInfo(tfd.fd).getOrElse {
          throw CompilationException("Unknown method : " + tfd.id)
        }

        if (requireMonitor) {
          load(monitorID, ch)
        }

        for((a, vd) <- as zip tfd.fd.params) {
          vd.getType match {
            case TypeParameter(_) =>
              mkBoxedExpr(a, ch)
            case _ =>
              mkExpr(a, ch)
          }
        }

        ch << InvokeStatic(cn, mn, ms)

        (tfd.fd.returnType, tfd.returnType) match {
          case (TypeParameter(_), tpe)  =>
            mkUnbox(tpe, ch)
          case _ =>
        }

      // Strict fields are handled as fields
      case MethodInvocation(rec, _, tfd, _) if tfd.fd.canBeStrictField =>
        val (className, fieldName, _) = leonFunDefToJVMInfo(tfd.fd).getOrElse {
          throw CompilationException("Unknown method : " + tfd.id)
        }

        if (requireMonitor) {
          load(monitorID, ch)
          ch << InvokeVirtual(MonitorClass, "onInvoke", "()V")
        }
        // Load receiver
        mkExpr(rec,ch)

        // Get field
        ch << GetField(className, fieldName, typeToJVM(tfd.fd.returnType))

        // unbox field
        (tfd.fd.returnType, tfd.returnType) match {
          case (TypeParameter(_), tpe)  =>
            mkUnbox(tpe, ch)
          case _ =>
        }
      // This is for lazy fields and real methods.
      // To access a lazy field, we call its accessor function.
      case MethodInvocation(rec, cd, tfd, as) =>
        val (className, methodName, sig) = leonFunDefToJVMInfo(tfd.fd).getOrElse {
          throw CompilationException("Unknown method : " + tfd.id)
        }

        // Receiver of the method call
        mkExpr(rec,ch)

        if (requireMonitor) {
          load(monitorID, ch)
        }

        for((a, vd) <- as zip tfd.fd.params) {
          vd.getType match {
            case TypeParameter(_) =>
              mkBoxedExpr(a, ch)
            case _ =>
              mkExpr(a, ch)
          }
        }

        // No interfaces in Leon, so no need to use InvokeInterface
        ch << InvokeVirtual(className, methodName, sig)

        (tfd.fd.returnType, tfd.returnType) match {
          case (TypeParameter(_), tpe)  =>
            mkUnbox(tpe, ch)
          case _ =>
        }

      case app @ Application(caller, args) =>
        mkExpr(caller, ch)
        ch << Ldc(args.size) << NewArray(s"$ObjectClass")
        for ((arg,i) <- args.zipWithIndex) {
          ch << DUP << Ldc(i)
          mkBoxedExpr(arg, ch)
          ch << AASTORE
        }

        ch << InvokeVirtual(LambdaClass, "apply", s"([L$ObjectClass;)L$ObjectClass;")
        mkUnbox(app.getType, ch)

      case l @ Lambda(args, body) =>
        compileLambda(l, ch)

      case f @ Forall(args, body) =>
        compileForall(f, ch)

      // Arithmetic
      case Plus(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << InvokeVirtual(BigIntClass, "add", s"(L$BigIntClass;)L$BigIntClass;")

      case Minus(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << InvokeVirtual(BigIntClass, "sub", s"(L$BigIntClass;)L$BigIntClass;")

      case Times(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << InvokeVirtual(BigIntClass, "mult", s"(L$BigIntClass;)L$BigIntClass;")

      case Division(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << InvokeVirtual(BigIntClass, "div", s"(L$BigIntClass;)L$BigIntClass;")

      case Remainder(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << InvokeVirtual(BigIntClass, "rem", s"(L$BigIntClass;)L$BigIntClass;")

      case Modulo(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << InvokeVirtual(BigIntClass, "mod", s"(L$BigIntClass;)L$BigIntClass;")

      case UMinus(e) =>
        mkExpr(e, ch)
        ch << InvokeVirtual(BigIntClass, "neg", s"()L$BigIntClass;")

      case RealPlus(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << InvokeVirtual(RationalClass, "add", s"(L$RationalClass;)L$RationalClass;")

      case RealMinus(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << InvokeVirtual(RationalClass, "sub", s"(L$RationalClass;)L$RationalClass;")

      case RealTimes(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << InvokeVirtual(RationalClass, "mult", s"(L$RationalClass;)L$RationalClass;")

      case RealDivision(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << InvokeVirtual(RationalClass, "div", s"(L$RationalClass;)L$RationalClass;")

      case RealUMinus(e) =>
        mkExpr(e, ch)
        ch << InvokeVirtual(RationalClass, "neg", s"()L$RationalClass;")


      //BV arithmetic
      case BVPlus(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << IADD

      case BVMinus(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << ISUB

      case BVTimes(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << IMUL

      case BVDivision(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << IDIV

      case BVRemainder(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << IREM

      case BVUMinus(e) =>
        mkExpr(e, ch)
        ch << INEG
      case BVNot(e) =>
        mkExpr(e, ch)
        mkExpr(IntLiteral(-1), ch)
        ch << IXOR

      case BVAnd(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << IAND

      case BVOr(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << IOR

      case BVXOr(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << IXOR

      case BVShiftLeft(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << ISHL

      case BVLShiftRight(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << IUSHR

      case BVAShiftRight(l, r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        ch << ISHR

      case ArrayLength(a) =>
        mkExpr(a, ch)
        ch << ARRAYLENGTH

      case as @ ArraySelect(a,i) =>
        mkExpr(a, ch)
        mkExpr(i, ch)
        ch << (as.getType match {
          case Untyped => throw CompilationException("Cannot compile untyped array access.")
          case CharType => CALOAD
          case Int32Type => IALOAD
          case BooleanType => BALOAD
          case _ => AALOAD
        })

      case au @ ArrayUpdated(a, i, v) =>
        mkExpr(a, ch)
        ch << DUP
        ch << ARRAYLENGTH
        val storeInstr = a.getType match {
          case ArrayType(CharType) => ch << NewArray.primitive("T_CHAR"); CASTORE
          case ArrayType(Int32Type) => ch << NewArray.primitive("T_INT"); IASTORE
          case ArrayType(BooleanType) => ch << NewArray.primitive("T_BOOLEAN"); BASTORE
          case ArrayType(other) => ch << NewArray(typeToJVM(other)); AASTORE
          case other => throw CompilationException(s"Cannot compile finite array expression whose type is $other.")
        }
        //srcArrary and targetArray is on the stack
        ch << DUP_X1 //insert targetArray under srcArray
        ch << Ldc(0) << SWAP //srcArray, 0, targetArray
        ch << DUP << ARRAYLENGTH //targetArray, length on stack
        ch << Ldc(0) << SWAP //final arguments: src, 0, target, 0, length
        ch << InvokeStatic("java/lang/System", "arraycopy", s"(L$ObjectClass;IL$ObjectClass;II)V")

        //targetArray remains on the stack
        ch << DUP
        mkExpr(i, ch)
        mkExpr(v, ch)
        ch << storeInstr
        //returns targetArray

      case a @ FiniteArray(elems, default, length) =>
        mkExpr(length, ch)

        val storeInstr = a.getType match {
          case ArrayType(CharType) => ch << NewArray.primitive("T_CHAR"); CASTORE
          case ArrayType(Int32Type) => ch << NewArray.primitive("T_INT"); IASTORE
          case ArrayType(BooleanType) => ch << NewArray.primitive("T_BOOLEAN"); BASTORE
          case ArrayType(other) => ch << NewArray(typeToJVM(other)); AASTORE
          case other => throw CompilationException(s"Cannot compile finite array expression whose type is $other.")
        }

        // Fill up with default
        default foreach { df =>
          val loop = ch.getFreshLabel("array_loop")
          val loopOut = ch.getFreshLabel("array_loop_out")
          ch << Ldc(0)
          // (array, index)
          ch << Label(loop)
          ch << DUP2 << SWAP
          // (array, index, index, array)
          ch << ARRAYLENGTH
          // (array, index, index, length)
          ch << If_ICmpGe(loopOut) << DUP2
          // (array, index, array, index)
          mkExpr(df, ch)
          ch << storeInstr
          ch << Ldc(1) << IADD << Goto(loop)
          ch << Label(loopOut) << POP
        }

        // Replace present elements with correct value
        for ((i,v) <- elems ) {
          ch << DUP << Ldc(i)
          mkExpr(v, ch)
          ch << storeInstr
        }

      // Misc and boolean tests
      case Error(tpe, desc) =>
        ch << New(ErrorClass) << DUP
        ch << Ldc(desc)
        ch << InvokeSpecial(ErrorClass, constructorName, "(Ljava/lang/String;)V")
        ch << ATHROW

      case choose: Choose =>
        val prob = synthesis.Problem.fromChoose(choose)

        val id = runtime.ChooseEntryPoint.register(prob, this)
        ch << Ldc(id)

        ch << Ldc(prob.as.size)
        ch << NewArray(ObjectClass)

        for ((id, i) <- prob.as.zipWithIndex) {
          ch << DUP
          ch << Ldc(i)
          mkExpr(Variable(id), ch)
          mkBox(id.getType, ch)
          ch << AASTORE
        }

        ch << InvokeStatic(ChooseEntryPointClass, "invoke", s"(I[L$ObjectClass;)L$ObjectClass;")

        mkUnbox(choose.getType, ch)
      case gv @ GenericValue(tp, int) =>
        val id = runtime.GenericValues.register(gv)
        ch << Ldc(id)
        ch << InvokeStatic(GenericValuesClass, "get", s"(I)L$ObjectClass;")

      case nt @ NoTree( tp@ValueType() ) =>
        mkExpr(simplestValue(tp), ch)

      case NoTree(_) =>
        ch << ACONST_NULL

      case This(ct) =>
        ch << ALoad(0)

      case p : Passes =>
        mkExpr(matchToIfThenElse(p.asConstraint), ch)

      case m : MatchExpr =>
        mkExpr(matchToIfThenElse(m), ch)

      case b if b.getType == BooleanType && canDelegateToMkBranch =>
        val fl = ch.getFreshLabel("boolfalse")
        val al = ch.getFreshLabel("boolafter")
        ch << Ldc(1)
        mkBranch(b, al, fl, ch, canDelegateToMkExpr = false)
        ch << Label(fl) << POP << Ldc(0) << Label(al)

      case _ => throw CompilationException("Unsupported expr " + e + " : " + e.getClass)
    }
  }

  // Leaves on the stack a value equal to `e`, always of a type compatible with java.lang.Object.
  private[codegen] def mkBoxedExpr(e: Expr, ch: CodeHandler)(implicit locals: Locals) {
    e.getType match {
      case Int32Type =>
        ch << New(BoxedIntClass) << DUP
        mkExpr(e, ch)
        ch << InvokeSpecial(BoxedIntClass, constructorName, "(I)V")

      case BooleanType | UnitType =>
        ch << New(BoxedBoolClass) << DUP
        mkExpr(e, ch)
        ch << InvokeSpecial(BoxedBoolClass, constructorName, "(Z)V")

      case CharType =>
        ch << New(BoxedCharClass) << DUP
        mkExpr(e, ch)
        ch << InvokeSpecial(BoxedCharClass, constructorName, "(C)V")

      case at @ ArrayType(et) =>
        ch << New(BoxedArrayClass) << DUP
        mkExpr(e, ch)
        ch << InvokeSpecial(BoxedArrayClass, constructorName, s"(${typeToJVM(at)})V")

      case _ =>
        mkExpr(e, ch)
    }
  }

  // Assumes the top of the stack contains of value of the right type, and makes it
  // compatible with java.lang.Object.
  private[codegen] def mkBox(tpe: TypeTree, ch: CodeHandler)(implicit locals: Locals) {
    tpe match {
      case Int32Type =>
        ch << New(BoxedIntClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedIntClass, constructorName, "(I)V")

      case BooleanType | UnitType =>
        ch << New(BoxedBoolClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedBoolClass, constructorName, "(Z)V")

      case CharType =>
        ch << New(BoxedCharClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedCharClass, constructorName, "(C)V")

      case at @ ArrayType(et) =>
        ch << New(BoxedArrayClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedArrayClass, constructorName, s"(${typeToJVM(at)})V")
      case _ =>
    }
  }

  // Assumes that the top of the stack contains a value that should be of type `tpe`, and unboxes it to the right (JVM) type.
  private[codegen] def mkUnbox(tpe: TypeTree, ch: CodeHandler)(implicit locals: Locals) {
    tpe match {
      case Int32Type =>
        ch << CheckCast(BoxedIntClass) << InvokeVirtual(BoxedIntClass, "intValue", "()I")

      case BooleanType | UnitType =>
        ch << CheckCast(BoxedBoolClass) << InvokeVirtual(BoxedBoolClass, "booleanValue", "()Z")

      case CharType =>
        ch << CheckCast(BoxedCharClass) << InvokeVirtual(BoxedCharClass, "charValue", "()C")

      case ct : ClassType =>
        val (cn, _) = leonClassToJVMInfo(ct.classDef).getOrElse {
          throw new CompilationException("Unsupported class type : " + ct)
        }
        ch << CheckCast(cn)

      case IntegerType =>
        ch << CheckCast(BigIntClass)

      case RealType =>
        ch << CheckCast(RationalClass)

      case tt : TupleType =>
        ch << CheckCast(TupleClass)

      case st : SetType =>
        ch << CheckCast(SetClass)

      case mt : MapType =>
        ch << CheckCast(MapClass)

      case ft : FunctionType =>
        ch << CheckCast(LambdaClass)

      case tp : TypeParameter =>

      case tp : ArrayType =>
        ch << CheckCast(BoxedArrayClass) << InvokeVirtual(BoxedArrayClass, "arrayValue", s"()${typeToJVM(tp)}")
        ch << CheckCast(typeToJVM(tp))

      case _ =>
        throw new CompilationException("Unsupported type in unboxing : " + tpe)
    }
  }

  private[codegen] def mkBranch(cond: Expr, thenn: String, elze: String, ch: CodeHandler, canDelegateToMkExpr: Boolean = true)(implicit locals: Locals) {
    cond match {
      case BooleanLiteral(true) =>
        ch << Goto(thenn)

      case BooleanLiteral(false) =>
        ch << Goto(elze)

      case And(es) =>
        val fl = ch.getFreshLabel("andnext")
        mkBranch(es.head, fl, elze, ch)
        ch << Label(fl)
        mkBranch(andJoin(es.tail), thenn, elze, ch)

      case Or(es) =>
        val fl = ch.getFreshLabel("ornext")
        mkBranch(es.head, thenn, fl, ch)
        ch << Label(fl)
        mkBranch(orJoin(es.tail), thenn, elze, ch)

      case Implies(l, r) =>
        mkBranch(or(not(l), r), thenn, elze, ch)

      case Not(c) =>
        mkBranch(c, elze, thenn, ch)

      case Variable(b) =>
        load(b, ch)
        ch << IfEq(elze) << Goto(thenn)

      case Equals(l,r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        l.getType match {
          case ValueType() =>
            ch << If_ICmpEq(thenn) << Goto(elze)

          case _ =>
            ch << InvokeVirtual(s"$ObjectClass", "equals", s"(L$ObjectClass;)Z")
            ch << IfEq(elze) << Goto(thenn)
        }

      case LessThan(l,r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        l.getType match {
          case Int32Type | CharType =>
            ch << If_ICmpLt(thenn) << Goto(elze)
          case IntegerType =>
            ch << InvokeVirtual(BigIntClass, "lessThan", s"(L$BigIntClass;)Z")
            ch << IfEq(elze) << Goto(thenn)
          case RealType =>
            ch << InvokeVirtual(RationalClass, "lessThan", s"(L$RationalClass;)Z")
            ch << IfEq(elze) << Goto(thenn)
        }

      case GreaterThan(l,r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        l.getType match {
          case Int32Type | CharType =>
            ch << If_ICmpGt(thenn) << Goto(elze)
          case IntegerType =>
            ch << InvokeVirtual(BigIntClass, "greaterThan", s"(L$BigIntClass;)Z")
            ch << IfEq(elze) << Goto(thenn)
          case RealType =>
            ch << InvokeVirtual(RationalClass, "greaterThan", s"(L$RationalClass;)Z")
            ch << IfEq(elze) << Goto(thenn)
        }

      case LessEquals(l,r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        l.getType match {
          case Int32Type | CharType =>
            ch << If_ICmpLe(thenn) << Goto(elze)
          case IntegerType =>
            ch << InvokeVirtual(BigIntClass, "lessEquals", s"(L$BigIntClass;)Z")
            ch << IfEq(elze) << Goto(thenn)
          case RealType =>
            ch << InvokeVirtual(RationalClass, "lessEquals", s"(L$RationalClass;)Z")
            ch << IfEq(elze) << Goto(thenn)
        }

      case GreaterEquals(l,r) =>
        mkExpr(l, ch)
        mkExpr(r, ch)
        l.getType match {
          case Int32Type | CharType =>
            ch << If_ICmpGe(thenn) << Goto(elze)
          case IntegerType =>
            ch << InvokeVirtual(BigIntClass, "greaterEquals", s"(L$BigIntClass;)Z")
            ch << IfEq(elze) << Goto(thenn)
          case RealType =>
            ch << InvokeVirtual(RationalClass, "greaterEquals", s"(L$RationalClass;)Z")
            ch << IfEq(elze) << Goto(thenn)
        }

      case IfExpr(c, t, e) =>
        val innerThen = ch.getFreshLabel("then")
        val innerElse = ch.getFreshLabel("else")
        mkBranch(c, innerThen, innerElse, ch)
        ch << Label(innerThen)
        mkBranch(t, thenn, elze, ch)
        ch << Label(innerElse)
        mkBranch(e, thenn, elze, ch)

      case cci@IsInstanceOf(cct, e) =>
        mkExpr(cci, ch)
        ch << IfEq(elze) << Goto(thenn)

      case other if canDelegateToMkExpr =>
        mkExpr(other, ch, canDelegateToMkBranch = false)
        ch << IfEq(elze) << Goto(thenn)

      case other => throw CompilationException("Unsupported branching expr. : " + other)
    }
  }

  private def load(id: Identifier, ch: CodeHandler)(implicit locals: Locals): Unit = {
    locals.varToArg(id) match {
      case Some(slot) =>
        ch << ALoad(1) << Ldc(slot) << AALOAD
        mkUnbox(id.getType, ch)
      case None => locals.varToField(id) match {
        case Some((afName, nme, tpe)) =>
          ch << ALoad(0) << GetField(afName, nme, tpe)
        case None => locals.varToLocal(id) match {
          case Some(slot) =>
            val instr = id.getType match {
              case ValueType() => ILoad(slot)
              case _ => ALoad(slot)
            }
            ch << instr
          case None => throw CompilationException("Unknown variable : " + id)
        }
      }
    }
  }

  /** Compiles a lazy field.
    *
    * To define a lazy field, we have to add an accessor method and an underlying field.
    * The accessor method has the name of the original (Scala) lazy field and can be public.
    * The underlying field has a different name, is private, and is of a boxed type
    * to support null value (to signify uninitialized).
    *
    * @param lzy The lazy field to be compiled
    * @param owner The module/class containing `lzy`
    */
  def compileLazyField(lzy: FunDef, owner: Definition) {
    ctx.reporter.internalAssertion(lzy.canBeLazyField, s"Trying to compile non-lazy ${lzy.id.name} as a lazy field")

    val (_, accessorName, _ ) = leonFunDefToJVMInfo(lzy).get
    val cf = classes(owner)
    val cName = defToJVMName(owner)

    val isStatic = owner.isInstanceOf[ModuleDef]

    // Name of the underlying field
    val underlyingName = underlyingField(accessorName)
    // Underlying field is of boxed type
    val underlyingType = typeToJVMBoxed(lzy.returnType)

    // Underlying field. It is of a boxed type
    val fh = cf.addField(underlyingType,underlyingName)
    fh.setFlags( if (isStatic) {(
      FIELD_ACC_STATIC |
      FIELD_ACC_PRIVATE
    ).asInstanceOf[U2] } else {
      FIELD_ACC_PRIVATE
    }) // FIXME private etc?

    // accessor method
    locally {
      val parameters = if (requireMonitor) {
        Seq(monitorID -> s"L$MonitorClass;")
      } else Seq()

      val paramMapping = parameters.map(_._1).zipWithIndex.toMap.mapValues(_ + (if (isStatic) 0 else 1))
      val newLocs = NoLocals.withVars(paramMapping)

      val accM = cf.addMethod(typeToJVM(lzy.returnType), accessorName, parameters.map(_._2) : _*)
      accM.setFlags( if (isStatic) {(
        METHOD_ACC_STATIC | // FIXME other flags? Not always public?
        METHOD_ACC_PUBLIC
      ).asInstanceOf[U2] } else {
        METHOD_ACC_PUBLIC
      })
      val ch = accM.codeHandler
      val body = lzy.body.getOrElse(throw CompilationException("Lazy field without body?"))
      val initLabel = ch.getFreshLabel("isInitialized")

      if (requireMonitor) {
        load(monitorID, ch)(newLocs)
        ch << InvokeVirtual(MonitorClass, "onInvoke", "()V")
      }

      if (isStatic) {
        ch << GetStatic(cName, underlyingName, underlyingType)
      } else {
        ch << ALoad(0) << GetField(cName, underlyingName, underlyingType) // if (lzy == null)
      }
      // oldValue
      ch << DUP << IfNonNull(initLabel)
      // null
      ch << POP
      //
      mkBoxedExpr(body,ch)(newLocs) // lzy = <expr>
      ch << DUP
      // newValue, newValue
      if (isStatic) {
        ch << PutStatic(cName, underlyingName, underlyingType)
        //newValue
      }
      else {
        ch << ALoad(0) << SWAP
        // newValue, object, newValue
        ch << PutField (cName, underlyingName, underlyingType)
        //newValue
      }
      ch << Label(initLabel)  // return lzy
      //newValue
      lzy.returnType match {
        case ValueType() =>
          // Since the underlying field only has boxed types, we have to unbox them to return them
          mkUnbox(lzy.returnType, ch)(newLocs)
          ch << IRETURN
        case _ =>
          ch << ARETURN
      }
      ch.freeze
    }
  }

  /** Compile the (strict) field `field` which is owned by class `owner` */
  def compileStrictField(field : FunDef, owner : Definition) = {

    ctx.reporter.internalAssertion(field.canBeStrictField,
      s"Trying to compile ${field.id.name} as a strict field")
    val (_, fieldName, _) = leonFunDefToJVMInfo(field).get

    val cf = classes(owner)
    val fh = cf.addField(typeToJVM(field.returnType),fieldName)
    fh.setFlags( owner match {
      case _ : ModuleDef => (
        FIELD_ACC_STATIC |
        FIELD_ACC_PUBLIC | // FIXME
        FIELD_ACC_FINAL
      ).asInstanceOf[U2]
      case _ => (
        FIELD_ACC_PUBLIC | // FIXME
        FIELD_ACC_FINAL
      ).asInstanceOf[U2]
    })
  }

  /** Initializes a lazy field to null
   *  @param ch the codehandler to add the initializing code to
   *  @param className the name of the class in which the field is initialized
   *  @param lzy the lazy field to be initialized
   *  @param isStatic true if this is a static field
   */
  def initLazyField(ch: CodeHandler, className: String,  lzy: FunDef, isStatic: Boolean)(implicit locals: Locals) = {
    val (_, name, _) = leonFunDefToJVMInfo(lzy).get
    val underlyingName = underlyingField(name)
    val jvmType = typeToJVMBoxed(lzy.returnType)
    if (isStatic){
      ch << ACONST_NULL << PutStatic(className, underlyingName, jvmType)
    } else {
      ch << ALoad(0) << ACONST_NULL << PutField(className, underlyingName, jvmType)
    }
  }

  /** Initializes a (strict) field
   *  @param ch the codehandler to add the initializing code to
   *  @param className the name of the class in which the field is initialized
   *  @param field the field to be initialized
   *  @param isStatic true if this is a static field
   */
  def initStrictField(ch: CodeHandler, className: String, field: FunDef, isStatic: Boolean)(implicit locals: Locals) {
    val (_, name , _) = leonFunDefToJVMInfo(field).get
    val body = field.body.getOrElse(throw CompilationException("No body for field?"))
    val jvmType = typeToJVM(field.returnType)

    mkExpr(body, ch)

    if (isStatic){
      ch << PutStatic(className, name, jvmType)
    } else {
      ch << ALoad(0) << SWAP << PutField (className, name, jvmType)
    }
  }

  def compileAbstractClassDef(acd : AbstractClassDef) {

    val cName = defToJVMName(acd)

    val cf  = classes(acd)

    cf.setFlags((
      CLASS_ACC_SUPER |
      CLASS_ACC_PUBLIC |
      CLASS_ACC_ABSTRACT
    ).asInstanceOf[U2])

    cf.addInterface(CaseClassClass)

    // add special monitor for method invocations
    if (params.doInstrument) {
      val fh = cf.addField("I", instrumentedField)
      fh.setFlags(FIELD_ACC_PUBLIC)
    }

    val (fields, methods) = acd.methods partition { _.canBeField }
    val (strictFields, lazyFields) = fields partition { _.canBeStrictField }

    // Compile methods
    for (method <- methods) {
      compileFunDef(method,acd)
    }

    // Compile lazy fields
    for (lzy <- lazyFields) {
      compileLazyField(lzy, acd)
    }

    // Compile strict fields
    for (field <- strictFields) {
      compileStrictField(field, acd)
    }

    // definition of the constructor
    locally {
      val constrParams = if (requireMonitor) {
        Seq(monitorID -> s"L$MonitorClass;")
      } else Seq()

      val newLocs = NoLocals.withVars {
        constrParams.map(_._1).zipWithIndex.toMap.mapValues(_ + 1)
      }

      val cch = cf.addConstructor(constrParams.map(_._2) : _*).codeHandler

      for (lzy <- lazyFields) { initLazyField(cch, cName, lzy, isStatic = false)(newLocs) }
      for (field <- strictFields) { initStrictField(cch, cName, field, isStatic = false)(newLocs) }

      // Call parent constructor
      cch << ALoad(0)
      acd.parent match {
        case Some(parent) =>
          val pName = defToJVMName(parent.classDef)
          // Load monitor object
          if (requireMonitor) cch << ALoad(1)
          val constrSig = if (requireMonitor) "(L" + MonitorClass + ";)V" else "()V"
          cch << InvokeSpecial(pName, constructorName, constrSig)

        case None =>
          // Call constructor of java.lang.Object
          cch << InvokeSpecial(ObjectClass, constructorName, "()V")
      }

      // Initialize special monitor field
      if (params.doInstrument) {
        cch << ALoad(0)
        cch << Ldc(0)
        cch << PutField(cName, instrumentedField, "I")
      }

      cch << RETURN
      cch.freeze
    }

  }

  /**
   * Instrument read operations
   */
  val instrumentedField = "__read"

  def instrumentedGetField(ch: CodeHandler, cct: ClassType, id: Identifier)(implicit locals: Locals): Unit = {
    val ccd = cct.classDef
    ccd.fields.zipWithIndex.find(_._1.id == id) match {
      case Some((f, i)) =>
        val expType = cct.fields(i).getType

        val cName = defToJVMName(ccd)
        if (params.doInstrument) {
          ch << DUP << DUP
          ch << GetField(cName, instrumentedField, "I")
          ch << Ldc(1)
          ch << Ldc(i)
          ch << ISHL
          ch << IOR
          ch << PutField(cName, instrumentedField, "I")
        }
        ch << GetField(cName, f.id.name, typeToJVM(f.getType))

        f.getType match {
          case TypeParameter(_) =>
            mkUnbox(expType, ch)
          case _ =>
        }
      case None =>
        throw CompilationException("Unknown field: "+ccd.id.name+"."+id)
    }
  }

  def compileCaseClassDef(ccd: CaseClassDef) {

    val cName = defToJVMName(ccd)
    val pName = ccd.parent.map(parent => defToJVMName(parent.classDef))
    // An instantiation of ccd with its own type parameters
    val cct = CaseClassType(ccd, ccd.tparams.map(_.tp))

    val cf = classes(ccd)

    cf.setFlags((
      CLASS_ACC_SUPER |
      CLASS_ACC_PUBLIC |
      CLASS_ACC_FINAL
    ).asInstanceOf[U2])

    if(ccd.parent.isEmpty) {
      cf.addInterface(CaseClassClass)
    }

    // Case class parameters
    val fieldsTypes = ccd.fields.map { vd => (vd.id, typeToJVM(vd.getType)) }
    val constructorArgs = if (requireMonitor) {
      (monitorID -> s"L$MonitorClass;") +: fieldsTypes
    } else fieldsTypes

    val newLocs = NoLocals.withFields(constructorArgs.map {
      case (id, jvmt) => (id, (cName, id.name, jvmt))
    }.toMap)

    locally {
      val (fields, methods) = ccd.methods partition { _.canBeField }
      val (strictFields, lazyFields) = fields partition { _.canBeStrictField }

      // Compile methods
      for (method <- methods) {
        compileFunDef(method,ccd)
      }

      // Compile lazy fields
      for (lzy <- lazyFields) {
        compileLazyField(lzy, ccd)
      }

      // Compile strict fields
      for (field <- strictFields) {
        compileStrictField(field, ccd)
      }

      // definition of the constructor
      if(!params.doInstrument && !requireMonitor && ccd.fields.isEmpty && !ccd.methods.exists(_.canBeField)) {
        cf.addDefaultConstructor
      } else {
        for((id, jvmt) <- constructorArgs) {
          val fh = cf.addField(jvmt, id.name)
          fh.setFlags((
            FIELD_ACC_PUBLIC |
            FIELD_ACC_FINAL
          ).asInstanceOf[U2])
        }

        if (params.doInstrument) {
          val fh = cf.addField("I", instrumentedField)
          fh.setFlags(FIELD_ACC_PUBLIC)
        }

        val cch = cf.addConstructor(constructorArgs.map(_._2) : _*).codeHandler

        if (params.doInstrument) {
          cch << ALoad(0)
          cch << Ldc(0)
          cch << PutField(cName, instrumentedField, "I")
        }

        var c = 1
        for((id, jvmt) <- constructorArgs) {
          cch << ALoad(0)
          cch << (jvmt match {
            case "I" | "Z" => ILoad(c)
            case _ => ALoad(c)
          })
          cch << PutField(cName, id.name, jvmt)
          c += 1
        }

        // Call parent constructor AFTER initializing case class parameters
        if (ccd.parent.isDefined) {
          cch << ALoad(0)
          if (requireMonitor) {
            cch << ALoad(1)
            cch << InvokeSpecial(pName.get, constructorName, s"(L$MonitorClass;)V")
          } else {
            cch << InvokeSpecial(pName.get, constructorName, "()V")
          }
        } else {
          // Call constructor of java.lang.Object
          cch << ALoad(0)
          cch << InvokeSpecial(ObjectClass, constructorName, "()V")
        }

        // Now initialize fields
        for (lzy <- lazyFields) { initLazyField(cch, cName, lzy, isStatic = false)(newLocs) }
        for (field <- strictFields) { initStrictField(cch, cName , field, isStatic = false)(newLocs) }
        cch << RETURN
        cch.freeze
      }
    }

    locally {
      val pnm = cf.addMethod("I", "__getRead")
      pnm.setFlags((
        METHOD_ACC_PUBLIC |
        METHOD_ACC_FINAL
      ).asInstanceOf[U2])

      val pnch = pnm.codeHandler

      pnch << ALoad(0) << GetField(cName, instrumentedField, "I") << IRETURN

      pnch.freeze
    }

    locally {
      val pnm = cf.addMethod("Ljava/lang/String;", "productName")
      pnm.setFlags((
        METHOD_ACC_PUBLIC |
        METHOD_ACC_FINAL
      ).asInstanceOf[U2])

      val pnch = pnm.codeHandler

      pnch << Ldc(cName) << ARETURN

      pnch.freeze
    }

    locally {
      val pem = cf.addMethod(s"[L$ObjectClass;", "productElements")
      pem.setFlags((
        METHOD_ACC_PUBLIC |
        METHOD_ACC_FINAL
      ).asInstanceOf[U2])

      val pech = pem.codeHandler

      pech << Ldc(ccd.fields.size)
      pech << NewArray(ObjectClass)

      for ((f, i) <- ccd.fields.zipWithIndex) {
        pech << DUP
        pech << Ldc(i)
        pech << ALoad(0)
        instrumentedGetField(pech, cct, f.id)(newLocs)
        mkBox(f.getType, pech)(newLocs)
        pech << AASTORE
      }

      pech << ARETURN
      pech.freeze
    }

    // definition of equals
    locally {
      val emh = cf.addMethod("Z", "equals", s"L$ObjectClass;")
      emh.setFlags((
        METHOD_ACC_PUBLIC |
        METHOD_ACC_FINAL
      ).asInstanceOf[U2])

      val ech = emh.codeHandler

      val notRefEq = ech.getFreshLabel("notrefeq")
      val notEq = ech.getFreshLabel("noteq")
      val castSlot = ech.getFreshVar

      // If references are equal, trees are equal.
      ech << ALoad(0) << ALoad(1) << If_ACmpNe(notRefEq) << Ldc(1) << IRETURN << Label(notRefEq)

      // We check the type (this also checks against null)....
      ech << ALoad(1) << InstanceOf(cName) << IfEq(notEq)

      // ...finally, we compare fields one by one, shortcircuiting on disequalities.
      if(ccd.fields.nonEmpty) {
        ech << ALoad(1) << CheckCast(cName) << AStore(castSlot)

        for(vd <- ccd.fields) {
          ech << ALoad(0)
          instrumentedGetField(ech, cct, vd.id)(newLocs)
          ech << ALoad(castSlot)
          instrumentedGetField(ech, cct, vd.id)(newLocs)

          typeToJVM(vd.getType) match {
            case "I" | "Z" =>
              ech << If_ICmpNe(notEq)

            case ot =>
              ech << InvokeVirtual(ObjectClass, "equals", s"(L$ObjectClass;)Z") << IfEq(notEq)
          }
        }
      }

      ech << Ldc(1) << IRETURN << Label(notEq) << Ldc(0) << IRETURN
      ech.freeze
    }

    // definition of hashcode
    locally {
      val hashFieldName = "$leon$hashCode"
      cf.addField("I", hashFieldName).setFlags(FIELD_ACC_PRIVATE)
      val hmh = cf.addMethod("I", "hashCode", "")
      hmh.setFlags((
        METHOD_ACC_PUBLIC |
        METHOD_ACC_FINAL
      ).asInstanceOf[U2])

      val hch = hmh.codeHandler

      val wasNotCached = hch.getFreshLabel("wasNotCached")

      hch << ALoad(0) << GetField(cName, hashFieldName, "I") << DUP
      hch << IfEq(wasNotCached)
      hch << IRETURN
      hch << Label(wasNotCached) << POP
      hch << ALoad(0) << InvokeVirtual(cName, "productElements", s"()[L$ObjectClass;")
      hch << ALoad(0) << InvokeVirtual(cName, "productName", "()Ljava/lang/String;")
      hch << InvokeVirtual("java/lang/String", "hashCode", "()I")
      hch << InvokeStatic(HashingClass, "seqHash", s"([L$ObjectClass;I)I") << DUP
      hch << ALoad(0) << SWAP << PutField(cName, hashFieldName, "I")
      hch << IRETURN

      hch.freeze
    }

  }
}