From 20c13c968b5b5f5f312d4016d6f78944c9f8e021 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Fri, 25 Oct 2013 01:46:20 +0200
Subject: [PATCH] Bring back runtime monitors, do not compile them in unless
needed
---
.../runtime/LeonCodeGenRuntimeMonitor.java | 23 +++++++++++++++
.../leon/codegen/CodeGenEvalParams.scala | 7 -----
.../scala/leon/codegen/CodeGenParams.scala | 12 ++++++++
.../scala/leon/codegen/CodeGeneration.scala | 18 ++++++++++--
.../leon/codegen/CompilationEnvironment.scala | 18 ++++++++----
.../scala/leon/codegen/CompilationUnit.scala | 29 +++++++++++++++----
.../leon/codegen/CompiledExpression.scala | 14 +++++++--
.../scala/leon/datagen/VanuatooDataGen.scala | 2 +-
.../leon/evaluators/CodeGenEvaluator.scala | 5 ++--
.../evaluation/CodeGenExampleRunner.scala | 6 ++--
.../evaluation/EvaluationStrategy.scala | 6 ++--
.../leon/test/condabd/EvaluationTest.scala | 12 ++++----
12 files changed, 114 insertions(+), 38 deletions(-)
create mode 100644 src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeMonitor.java
delete mode 100644 src/main/scala/leon/codegen/CodeGenEvalParams.scala
create mode 100644 src/main/scala/leon/codegen/CodeGenParams.scala
diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeMonitor.java b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeMonitor.java
new file mode 100644
index 000000000..12bcc82d8
--- /dev/null
+++ b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeMonitor.java
@@ -0,0 +1,23 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon.codegen.runtime;
+
+/** Such exceptions are thrown when the evaluator encounters a runtime error,
+ * for instance `.get` with an undefined key on a map. */
+public class LeonCodeGenRuntimeMonitor {
+ private int invocationsLeft;
+
+ public LeonCodeGenRuntimeMonitor(int maxInvocations) {
+ this.invocationsLeft = maxInvocations;
+ }
+
+ public void onInvoke() throws LeonCodeGenEvaluationException {
+ if(invocationsLeft < 0) {
+ return;
+ } else if(invocationsLeft == 0) {
+ throw new LeonCodeGenEvaluationException("Maximum number of invocations reached.");
+ } else {
+ invocationsLeft--;
+ }
+ }
+}
diff --git a/src/main/scala/leon/codegen/CodeGenEvalParams.scala b/src/main/scala/leon/codegen/CodeGenEvalParams.scala
deleted file mode 100644
index 31f8c49df..000000000
--- a/src/main/scala/leon/codegen/CodeGenEvalParams.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-package leon
-package codegen
-
-case class CodeGenEvalParams (
- maxFunctionInvocations: Int = -1,
- checkContracts: Boolean = false
-)
diff --git a/src/main/scala/leon/codegen/CodeGenParams.scala b/src/main/scala/leon/codegen/CodeGenParams.scala
new file mode 100644
index 000000000..b37325747
--- /dev/null
+++ b/src/main/scala/leon/codegen/CodeGenParams.scala
@@ -0,0 +1,12 @@
+package leon
+package codegen
+
+case class CodeGenParams (
+ maxFunctionInvocations: Int = -1,
+ checkContracts: Boolean = false
+
+) {
+ val recordInvocations = maxFunctionInvocations > -1
+
+ val requireMonitor = recordInvocations
+}
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 727c6ab2b..2f3429ed0 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -26,6 +26,7 @@ object CodeGeneration {
private val ErrorClass = "leon/codegen/runtime/LeonCodeGenRuntimeException"
private val ImpossibleEvaluationClass = "leon/codegen/runtime/LeonCodeGenEvaluationException"
private val HashingClass = "leon/codegen/runtime/LeonCodeGenRuntimeHashing"
+ private[codegen] val MonitorClass = "leon/codegen/runtime/LeonCodeGenRuntimeMonitor"
def defToJVMName(d : Definition)(implicit env : CompilationEnvironment) : String = "Leon$CodeGen$" + d.id.uniqueName
@@ -57,17 +58,21 @@ object CodeGeneration {
// Assumes the CodeHandler has never received any bytecode.
// Generates method body, and freezes the handler at the end.
def compileFunDef(funDef : FunDef, ch : CodeHandler)(implicit env : CompilationEnvironment) {
- val newMapping = funDef.args.map(_.id).zipWithIndex.toMap
+ val newMapping = if (env.params.requireMonitor) {
+ funDef.args.map(_.id).zipWithIndex.toMap.mapValues(_ + 1)
+ } else {
+ funDef.args.map(_.id).zipWithIndex.toMap
+ }
val body = funDef.body.getOrElse(throw CompilationException("Can't compile a FunDef without body"))
- val bodyWithPre = if(funDef.hasPrecondition && env.compileContracts) {
+ val bodyWithPre = if(funDef.hasPrecondition && env.params.checkContracts) {
IfExpr(funDef.precondition.get, body, Error("Precondition failed"))
} else {
body
}
- val bodyWithPost = if(funDef.hasPostcondition && env.compileContracts) {
+ val bodyWithPost = if(funDef.hasPostcondition && env.params.checkContracts) {
val Some((id, post)) = funDef.postcondition
Let(id, bodyWithPre, IfExpr(post, Variable(id), Error("Postcondition failed")) )
} else {
@@ -76,6 +81,10 @@ object CodeGeneration {
val exprToCompile = purescala.TreeOps.matchToIfThenElse(bodyWithPost)
+ if (env.params.recordInvocations) {
+ ch << ALoad(0) << InvokeVirtual(MonitorClass, "onInvoke", "()V")
+ }
+
mkExpr(exprToCompile, ch)(env.withVars(newMapping))
funDef.returnType match {
@@ -268,6 +277,9 @@ object CodeGeneration {
val (cn, mn, ms) = env.funDefToMethod(fd).getOrElse {
throw CompilationException("Unknown method : " + fd.id)
}
+ if (env.params.requireMonitor) {
+ ch << ALoad(0)
+ }
for(a <- as) {
mkExpr(a, ch)
}
diff --git a/src/main/scala/leon/codegen/CompilationEnvironment.scala b/src/main/scala/leon/codegen/CompilationEnvironment.scala
index c364b7153..21732db3d 100644
--- a/src/main/scala/leon/codegen/CompilationEnvironment.scala
+++ b/src/main/scala/leon/codegen/CompilationEnvironment.scala
@@ -15,7 +15,7 @@ abstract class CompilationEnvironment() {
val program: Program
- val compileContracts: Boolean
+ val params: CodeGenParams
// Returns (JVM) name of class, and signature of constructor
def classDefToClass(classDef : ClassTypeDef) : Option[String]
@@ -29,7 +29,7 @@ abstract class CompilationEnvironment() {
def withVars(pairs : Map[Identifier,Int]) = {
new CompilationEnvironment {
val program = self.program
- val compileContracts = self.compileContracts
+ val params = self.params
def classDefToClass(classDef : ClassTypeDef) = self.classDefToClass(classDef)
def funDefToMethod(funDef : FunDef) = self.funDefToMethod(funDef)
def varToLocal(v : Identifier) = pairs.get(v).orElse(self.varToLocal(v))
@@ -38,7 +38,7 @@ abstract class CompilationEnvironment() {
}
object CompilationEnvironment {
- def fromProgram(p : Program, _compileContracts: Boolean) : CompilationEnvironment = {
+ def fromProgram(p : Program, _params: CodeGenParams) : CompilationEnvironment = {
import CodeGeneration.typeToJVM
// This should change: it should contain the case classes before
@@ -46,7 +46,7 @@ object CompilationEnvironment {
implicit val initial = new CompilationEnvironment {
val program = p
- val compileContracts = _compileContracts
+ val params = _params
private val cNames : Map[ClassTypeDef,String] =
p.definedClasses.map(c => (c, CodeGeneration.defToJVMName(c)(this))).toMap
@@ -60,8 +60,14 @@ object CompilationEnvironment {
val fs = p.definedFunctions.filter(_.hasImplementation)
+ val monitorType = if (_params.requireMonitor) {
+ "L" + CodeGeneration.MonitorClass + ";"
+ } else {
+ ""
+ }
+
val fMap : Map[FunDef,(String,String,String)] = (fs.map { fd =>
- val sig = "(" + fd.args.map(a => typeToJVM(a.tpe)).mkString("") + ")" + typeToJVM(fd.returnType)
+ val sig = "(" + monitorType + fd.args.map(a => typeToJVM(a.tpe)).mkString("") + ")" + typeToJVM(fd.returnType)
fd -> (className, fd.id.uniqueName, sig)
}).toMap
@@ -69,7 +75,7 @@ object CompilationEnvironment {
new CompilationEnvironment {
val program = p
- val compileContracts = initial.compileContracts
+ val params = initial.params
def classDefToClass(classDef : ClassTypeDef) = initial.classDefToClass(classDef)
def funDefToMethod(funDef : FunDef) = fMap.get(funDef)
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 99976d4c7..c612803e6 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -145,10 +145,18 @@ class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFi
cf.addDefaultConstructor
+ val argsTypes = args.map(a => typeToJVM(a.getType))
+
+ val realArgs = if (env.params.requireMonitor) {
+ ("L" + CodeGeneration.MonitorClass + ";") +: argsTypes
+ } else {
+ argsTypes
+ }
+
val m = cf.addMethod(
typeToJVM(e.getType),
"eval",
- args.map(a => typeToJVM(a.getType)) : _*
+ realArgs : _*
)
m.setFlags((
@@ -159,7 +167,11 @@ class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFi
val ch = m.codeHandler
- val newMapping = args.zipWithIndex.toMap
+ val newMapping = if (env.params.requireMonitor) {
+ args.zipWithIndex.toMap.mapValues(_ + 1)
+ } else {
+ args.zipWithIndex.toMap
+ }
val exprToCompile = purescala.TreeOps.matchToIfThenElse(e)
@@ -187,8 +199,8 @@ class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFi
}
object CompilationUnit {
- def compileProgram(p: Program, compileContracts: Boolean = true): Option[CompilationUnit] = {
- implicit val env = CompilationEnvironment.fromProgram(p, compileContracts)
+ def compileProgram(p: Program, params: CodeGenParams = CodeGenParams()): Option[CompilationUnit] = {
+ implicit val env = CompilationEnvironment.fromProgram(p, params)
var classes = Map[Definition, ClassFile]()
@@ -222,10 +234,17 @@ object CompilationUnit {
for(funDef <- p.definedFunctions;
(_,mn,_) <- env.funDefToMethod(funDef)) {
+ val argsTypes = funDef.args.map(a => typeToJVM(a.tpe))
+ val realArgs = if (env.params.requireMonitor) {
+ ("L" + CodeGeneration.MonitorClass + ";") +: argsTypes
+ } else {
+ argsTypes
+ }
+
val m = cf.addMethod(
typeToJVM(funDef.returnType),
mn,
- funDef.args.map(a => typeToJVM(a.tpe)) : _*
+ realArgs : _*
)
m.setFlags((
METHOD_ACC_PUBLIC |
diff --git a/src/main/scala/leon/codegen/CompiledExpression.scala b/src/main/scala/leon/codegen/CompiledExpression.scala
index d1b4bbb4d..0f4c8f855 100644
--- a/src/main/scala/leon/codegen/CompiledExpression.scala
+++ b/src/main/scala/leon/codegen/CompiledExpression.scala
@@ -14,6 +14,8 @@ import cafebabe.ByteCodes._
import cafebabe.ClassFileTypes._
import cafebabe.Flags._
+import runtime.LeonCodeGenRuntimeMonitor
+
import java.lang.reflect.InvocationTargetException
class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression : Expr, argsDecl: Seq[Identifier]) {
@@ -22,6 +24,8 @@ class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression : Expr
private val exprType = expression.getType
+ private val params = unit.env.params
+
def argsToJVM(args: Seq[Expr]): Seq[AnyRef] = {
args.map(unit.valueToJVM)
}
@@ -29,10 +33,16 @@ class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression : Expr
def evalToJVM(args: Seq[AnyRef]): AnyRef = {
assert(args.size == argsDecl.size)
- if (args.isEmpty) {
+ val realArgs = if (params.requireMonitor) {
+ new LeonCodeGenRuntimeMonitor(params.maxFunctionInvocations) +: args
+ } else {
+ args
+ }
+
+ if (realArgs.isEmpty) {
meth.invoke(null)
} else {
- meth.invoke(null, args.toArray : _*)
+ meth.invoke(null, realArgs.toArray : _*)
}
}
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 5215670e3..7a579b237 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -16,7 +16,7 @@ import vanuatoo.{Pattern => VPattern, _}
import evaluators._
class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
- val unit = CompilationUnit.compileProgram(p, compileContracts = false).get
+ val unit = CompilationUnit.compileProgram(p).get
val ints = (for (i <- Set(0, 1, 2, 3)) yield {
i -> Constructor[Expr, TypeTree](List(), Int32Type, s => IntLiteral(i), ""+i)
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index 87314546f..6d290c569 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -10,14 +10,15 @@ import purescala.Trees._
import purescala.TypeTrees._
import codegen.CompilationUnit
+import codegen.CodeGenParams
class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Evaluator(ctx, unit.program) {
val name = "codegen-eval"
val description = "Evaluator for PureScala expressions based on compilation to JVM"
/** Another constructor to make it look more like other `Evaluator`s. */
- def this(ctx : LeonContext, prog : Program) {
- this(ctx, CompilationUnit.compileProgram(prog).get) // this .get is dubious...
+ def this(ctx : LeonContext, prog : Program, params: CodeGenParams = CodeGenParams()) {
+ this(ctx, CompilationUnit.compileProgram(prog, params).get) // this .get is dubious...
}
def eval(expression : Expr, mapping : Map[Identifier,Expr]) : EvaluationResult = {
diff --git a/src/main/scala/leon/synthesis/condabd/evaluation/CodeGenExampleRunner.scala b/src/main/scala/leon/synthesis/condabd/evaluation/CodeGenExampleRunner.scala
index d6fd0911c..1dc6d1d6b 100644
--- a/src/main/scala/leon/synthesis/condabd/evaluation/CodeGenExampleRunner.scala
+++ b/src/main/scala/leon/synthesis/condabd/evaluation/CodeGenExampleRunner.scala
@@ -10,7 +10,7 @@ import leon.purescala.Trees._
import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
import leon.purescala.Common.{ Identifier, FreshIdentifier }
import leon.purescala.TreeOps
-import leon.codegen.CodeGenEvalParams
+import leon.codegen.CodeGenParams
import examples._
import ranking._
@@ -19,14 +19,14 @@ import _root_.insynth.util.logging.HasLogger
case class CodeGenExampleRunner(program: Program, funDef: FunDef, ctx: LeonContext,
candidates: Seq[Candidate], inputExamples: Seq[Example],
- params: CodeGenEvalParams = CodeGenEvalParams(maxFunctionInvocations = 200, checkContracts = true)) extends ExampleRunner(inputExamples) with HasLogger {
+ params: CodeGenParams = CodeGenParams(maxFunctionInvocations = 200, checkContracts = true)) extends ExampleRunner(inputExamples) with HasLogger {
private var _examples = ArrayBuffer(transformExamples(inputExamples): _*)
val evaluationContext = ctx
fine("building codegen evaluator with program:\n" + program)
- lazy val _evaluator = new CodeGenEvaluator(evaluationContext, program/*TODO:, params*/)
+ lazy val _evaluator = new CodeGenEvaluator(evaluationContext, program, params)
override def getEvaluator = _evaluator
def transformExamples(examples: Seq[Example]) =
diff --git a/src/main/scala/leon/synthesis/condabd/evaluation/EvaluationStrategy.scala b/src/main/scala/leon/synthesis/condabd/evaluation/EvaluationStrategy.scala
index 1ab73543a..ee0e54ff3 100644
--- a/src/main/scala/leon/synthesis/condabd/evaluation/EvaluationStrategy.scala
+++ b/src/main/scala/leon/synthesis/condabd/evaluation/EvaluationStrategy.scala
@@ -8,7 +8,7 @@ import leon.purescala.Trees._
import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
import leon.purescala.Common.{ Identifier, FreshIdentifier }
import leon.purescala.TreeOps
-import leon.codegen.CodeGenEvalParams
+import leon.codegen.CodeGenParams
import insynth.reconstruction.Output
import _root_.insynth.util.logging._
@@ -94,7 +94,7 @@ case class CodeGenEvaluationStrategy(program: Program, funDef: FunDef, ctx: Leon
finest("New program looks like: " + newProgram)
finest("Candidates look like: " + candidates.map(_.prepareExpression).mkString("\n"))
- val params = CodeGenEvalParams(maxFunctionInvocations = maxSteps, checkContracts = true)
+ val params = CodeGenParams(maxFunctionInvocations = maxSteps, checkContracts = true)
exampleRunner = CodeGenExampleRunner(newProgram, funDef, ctx, candidates, inputExamples, params)
@@ -108,4 +108,4 @@ case class CodeGenEvaluationStrategy(program: Program, funDef: FunDef, ctx: Leon
override def getExampleRunner = exampleRunner
override def getEvaluation = evaluation
-}
\ No newline at end of file
+}
diff --git a/src/test/scala/leon/test/condabd/EvaluationTest.scala b/src/test/scala/leon/test/condabd/EvaluationTest.scala
index ef7d53911..2f22361a4 100644
--- a/src/test/scala/leon/test/condabd/EvaluationTest.scala
+++ b/src/test/scala/leon/test/condabd/EvaluationTest.scala
@@ -10,7 +10,7 @@ import java.io.{ BufferedWriter, FileWriter, File }
import leon.evaluators.CodeGenEvaluator
import leon.purescala.TreeOps
import leon.purescala.Common._
-import leon.codegen.CodeGenEvalParams
+import leon.codegen.CodeGenParams
import leon.purescala.TypeTrees._
import leon.evaluators.EvaluationResults._
@@ -248,11 +248,11 @@ class EvaluationTest extends FunSuite {
val pairs = List(body1, body2) map (formExecutable(_))
val candidates = pairs map (_._1)
- val params = CodeGenEvalParams(maxFunctionInvocations = 500, checkContracts = true)
+ val params = CodeGenParams(maxFunctionInvocations = 500, checkContracts = true)
val evaluator = new CodeGenEvaluator(sctx.context,
program.copy(mainObject = program.mainObject.copy(defs = program.mainObject.defs ++ pairs.map(_._2)))
- /*, params*/)
+ , params)
val eval1 = (for (ind <- 0 until inputExamples.size) yield {
val res = evaluator.eval(candidates(0), inputExamples(ind).map)
@@ -302,11 +302,11 @@ class EvaluationTest extends FunSuite {
val pairs = List(body1, body2) map (formExecutable(_))
val candidates = pairs map (_._1)
- val params = CodeGenEvalParams(maxFunctionInvocations = 500, checkContracts = true)
+ val params = CodeGenParams(maxFunctionInvocations = 500, checkContracts = true)
val evaluator = new CodeGenEvaluator(sctx.context,
program.copy(mainObject = program.mainObject.copy(defs = program.mainObject.defs ++ pairs.map(_._2)))
- /*, params*/)
+ , params)
val eval1 = (for (ind <- 0 until inputExamples.size) yield {
val res = evaluator.eval(candidates(0), inputExamples(ind).map)
@@ -326,4 +326,4 @@ class EvaluationTest extends FunSuite {
}
}
}
-}
\ No newline at end of file
+}
--
GitLab