diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 77b34d64ea330dce8ff7f9f3e5c0a4444a00750c..e5bb4b2af730bb0002887daf2e64e7333a5dc9e1 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -566,7 +566,7 @@ trait CodeGeneration {
mkUnbox(app.getType, ch)
case l @ Lambda(args, body) =>
- val afName = "Leon$CodeGen$Lambda$" + CompilationUnit.nextLambdaId
+ val afName = "Leon$CodeGen$Lambda$" + lambdaCounter.nextGlobal
lambdas += afName -> l
val cf = new ClassFile(afName, Some(LambdaClass))
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 54e3485d6cad2520f8d5dd03b64c9e3fedc60ce9..c852e50b61cd2aa62447ff9827aca69164ac63cf 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -10,6 +10,7 @@ import purescala.Types._
import purescala.Extractors._
import purescala.Constructors._
import codegen.runtime.LeonCodeGenRuntimeMonitor
+import utils.UniqueCounter
import cafebabe._
import cafebabe.AbstractByteCodes._
@@ -119,10 +120,13 @@ class CompilationUnit(val ctx: LeonContext,
conss.last
}
- // Currently, this method is only used to prepare arguments to reflective calls.
- // This means it is safe to return AnyRef (as opposed to primitive types), because
- // reflection needs this anyway.
- def exprToJVM(e: Expr)(implicit monitor : LeonCodeGenRuntimeMonitor): AnyRef = e match {
+ /** Translates Leon values (not generic expressions) to JVM compatible objects.
+ *
+ * Currently, this method is only used to prepare arguments to reflective calls.
+ * This means it is safe to return AnyRef (as opposed to primitive types), because
+ * reflection needs this anyway.
+ */
+ def valueToJVM(e: Expr)(implicit monitor: LeonCodeGenRuntimeMonitor): AnyRef = e match {
case IntLiteral(v) =>
new java.lang.Integer(v)
@@ -136,12 +140,12 @@ class CompilationUnit(val ctx: LeonContext,
e
case Tuple(elems) =>
- tupleConstructor.newInstance(elems.map(exprToJVM).toArray).asInstanceOf[AnyRef]
+ tupleConstructor.newInstance(elems.map(valueToJVM).toArray).asInstanceOf[AnyRef]
case CaseClass(cct, args) =>
caseClassConstructor(cct.classDef) match {
case Some(cons) =>
- val realArgs = if (params.requireMonitor) monitor +: args.map(exprToJVM) else args.map(exprToJVM)
+ val realArgs = if (params.requireMonitor) monitor +: args.map(valueToJVM) else args.map(valueToJVM)
cons.newInstance(realArgs.toArray : _*).asInstanceOf[AnyRef]
case None =>
ctx.reporter.fatalError("Case class constructor not found?!?")
@@ -155,39 +159,39 @@ class CompilationUnit(val ctx: LeonContext,
case s @ FiniteSet(els, _) =>
val s = new leon.codegen.runtime.Set()
for (e <- els) {
- s.add(exprToJVM(e))
+ s.add(valueToJVM(e))
}
s
case m @ FiniteMap(els, _, _) =>
val m = new leon.codegen.runtime.Map()
for ((k,v) <- els) {
- m.add(exprToJVM(k), exprToJVM(v))
+ m.add(valueToJVM(k), valueToJVM(v))
}
m
case f @ purescala.Extractors.FiniteLambda(dflt, els) =>
- val l = new leon.codegen.runtime.FiniteLambda(exprToJVM(dflt))
+ val l = new leon.codegen.runtime.FiniteLambda(valueToJVM(dflt))
for ((k,v) <- els) {
val ks = unwrapTuple(k, f.getType.asInstanceOf[FunctionType].from.size)
// Force tuple even with 1/0 elems.
- val kJvm = tupleConstructor.newInstance(ks.map(exprToJVM).toArray).asInstanceOf[leon.codegen.runtime.Tuple]
- val vJvm = exprToJVM(v)
+ val kJvm = tupleConstructor.newInstance(ks.map(valueToJVM).toArray).asInstanceOf[leon.codegen.runtime.Tuple]
+ val vJvm = valueToJVM(v)
l.add(kJvm,vJvm)
}
l
case _ =>
- throw LeonFatalError("Unexpected expression in exprToJVM")
+ throw CompilationException(s"Unexpected expression $e in valueToJVM")
// Just slightly overkill...
//case _ =>
// compileExpression(e, Seq()).evalToJVM(Seq(),monitor)
}
-
- // Note that this may produce untyped expressions! (typically: sets, maps)
- def jvmToExpr(e: AnyRef, tpe: TypeTree): Expr = (e, tpe) match {
+
+ /** Translates JVM objects back to Leon values of the appropriate type */
+ def jvmToValue(e: AnyRef, tpe: TypeTree): Expr = (e, tpe) match {
case (i: Integer, Int32Type) =>
IntLiteral(i.toInt)
@@ -197,7 +201,6 @@ class CompilationUnit(val ctx: LeonContext,
case (c: runtime.Real, RealType) =>
RealLiteral(BigDecimal(c.underlying))
-
case (b: java.lang.Boolean, BooleanType) =>
BooleanLiteral(b.booleanValue)
@@ -221,12 +224,12 @@ class CompilationUnit(val ctx: LeonContext,
}
}
- CaseClass(cct, (fields zip cct.fieldsTypes).map { case (e, tpe) => jvmToExpr(e, tpe) })
+ CaseClass(cct, (fields zip cct.fieldsTypes).map { case (e, tpe) => jvmToValue(e, tpe) })
case (tpl: runtime.Tuple, tpe) =>
val stpe = unwrapTupleType(tpe, tpl.getArity)
val elems = stpe.zipWithIndex.map { case (tpe, i) =>
- jvmToExpr(tpl.get(i), tpe)
+ jvmToValue(tpl.get(i), tpe)
}
tupleWrap(elems)
@@ -235,12 +238,12 @@ class CompilationUnit(val ctx: LeonContext,
else GenericValue(tp, id).copiedFrom(gv)
case (set: runtime.Set, SetType(b)) =>
- FiniteSet(set.getElements.asScala.map(jvmToExpr(_, b)).toSet, b)
+ FiniteSet(set.getElements.asScala.map(jvmToValue(_, b)).toSet, b)
case (map: runtime.Map, MapType(from, to)) =>
val pairs = map.getElements.asScala.map { entry =>
- val k = jvmToExpr(entry.getKey, from)
- val v = jvmToExpr(entry.getValue, to)
+ val k = jvmToValue(entry.getKey, from)
+ val v = jvmToValue(entry.getValue, to)
(k, v)
}
FiniteMap(pairs.toSeq, from, to)
@@ -252,7 +255,7 @@ class CompilationUnit(val ctx: LeonContext,
val closures = purescala.ExprOps.variablesOf(l).toSeq.sortBy(_.uniqueName)
val closureVals = closures.map { id =>
val fieldVal = lambda.getClass.getField(id.name).get(lambda)
- jvmToExpr(fieldVal, id.getType)
+ jvmToValue(fieldVal, id.getType)
}
purescala.ExprOps.replaceFromIDs((closures zip closureVals).toMap, l)
@@ -265,7 +268,7 @@ class CompilationUnit(val ctx: LeonContext,
EmptyArray(base)
} else {
val elems = for ((e: AnyRef, i) <- ar.zipWithIndex) yield {
- i -> jvmToExpr(e, base)
+ i -> jvmToValue(e, base)
}
NonemptyArray(elems.toMap, None)
@@ -284,7 +287,7 @@ class CompilationUnit(val ctx: LeonContext,
compiledN += 1
- val id = CompilationUnit.nextExprId
+ val id = exprCounter.nextGlobal
val cName = "Leon$CodeGen$Expr$"+id
@@ -347,15 +350,7 @@ class CompilationUnit(val ctx: LeonContext,
CLASS_ACC_PUBLIC |
CLASS_ACC_FINAL
).asInstanceOf[U2])
-
- /*if (false) {
- // currently we do not handle object fields
- // this treats all fields as functions
- for (fun <- module.definedFunctions) {
- compileFunDef(fun, module)
- }
- } else {*/
-
+
val (fields, functions) = module.definedFunctions partition { _.canBeField }
val (strictFields, lazyFields) = fields partition { _.canBeStrictField }
@@ -468,17 +463,5 @@ class CompilationUnit(val ctx: LeonContext,
compile()
}
-object CompilationUnit {
- private var _nextExprId = 0
- private[codegen] def nextExprId = synchronized {
- _nextExprId += 1
- _nextExprId
- }
-
- private var _nextLambdaId = 0
- private[codegen] def nextLambdaId = synchronized {
- _nextLambdaId += 1
- _nextLambdaId
- }
-}
-
+private [codegen] object exprCounter extends UniqueCounter[Unit]
+private [codegen] object lambdaCounter extends UniqueCounter[Unit]
diff --git a/src/main/scala/leon/codegen/CompiledExpression.scala b/src/main/scala/leon/codegen/CompiledExpression.scala
index 22ff5e564be1dccbcd9a654b9ccb8640d477fc49..e31e28e92922875a72a3a9cd233fade73a25223c 100644
--- a/src/main/scala/leon/codegen/CompiledExpression.scala
+++ b/src/main/scala/leon/codegen/CompiledExpression.scala
@@ -22,7 +22,7 @@ class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression : Expr
private val params = unit.params
def argsToJVM(args: Seq[Expr], monitor: LM): Seq[AnyRef] = {
- args.map(unit.exprToJVM(_)(monitor))
+ args.map(unit.valueToJVM(_)(monitor))
}
def evalToJVM(args: Seq[AnyRef], monitor: LM): AnyRef = {
@@ -45,7 +45,7 @@ class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression : Expr
// We also need to reattach a type in some cases (sets, maps).
def evalFromJVM(args: Seq[AnyRef], monitor: LM) : Expr = {
try {
- unit.jvmToExpr(evalToJVM(args, monitor), exprType)
+ unit.jvmToValue(evalToJVM(args, monitor), exprType)
} catch {
case ite : InvocationTargetException => throw ite.getCause
}
diff --git a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
index e8b38e5ba82f81fa9d5d174b9dbf43650cbcf54e..2824b3f9794f6e7fda04642d7df10e3f1a90e870 100644
--- a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
+++ b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
@@ -84,7 +84,7 @@ object ChooseEntryPoint {
val inputsMap = (p.as zip inputs).map {
case (id, v) =>
- Equals(Variable(id), unit.jvmToExpr(v, id.getType))
+ Equals(Variable(id), unit.jvmToValue(v, id.getType))
}
solver.assertCnstr(andJoin(Seq(p.pc, p.phi) ++ inputsMap))
@@ -104,7 +104,7 @@ object ChooseEntryPoint {
ctx.reporter.debug("Synthesis took "+total+"ms")
ctx.reporter.debug("Finished synthesis with "+leonRes.asString(ctx))
- val obj = unit.exprToJVM(leonRes)(new LeonCodeGenRuntimeMonitor(unit.params.maxFunctionInvocations))
+ val obj = unit.valueToJVM(leonRes)(new LeonCodeGenRuntimeMonitor(unit.params.maxFunctionInvocations))
chCache += is -> obj
obj
case Some(false) =>
diff --git a/src/main/scala/leon/evaluators/DualEvaluator.scala b/src/main/scala/leon/evaluators/DualEvaluator.scala
index 98c1060a13366cf2025b1a4de7dfbcf7986d90d5..a058dd3a04fe53700aa71265ba5952b9fc82f6ce 100644
--- a/src/main/scala/leon/evaluators/DualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DualEvaluator.scala
@@ -116,9 +116,9 @@ class DualEvaluator(ctx: LeonContext, prog: Program, params: CodeGenParams) exte
case RawObject(obj, _) if returnJVMRef =>
e
case RawObject(obj, _) if !returnJVMRef =>
- unit.jvmToExpr(obj, e.getType)
+ unit.jvmToValue(obj, e.getType)
case e if returnJVMRef =>
- RawObject(unit.exprToJVM(e)(monitor), e.getType)
+ RawObject(unit.valueToJVM(e)(monitor), e.getType)
case e if !returnJVMRef =>
e
}
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index f04cbc99fa2b14391d8982ef108eb9b2ea47a868..5c630e4f69589d575c3d76fbd599da5d158a695e 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -78,40 +78,31 @@ object Common {
}
}
- private object UniqueCounter {
- private var globalId = -1
- private var nameIds = Map[String, Int]().withDefaultValue(-1)
-
- def next(name: String): Int = synchronized {
- nameIds += name -> (1+nameIds(name))
- nameIds(name)
- }
-
- def nextGlobal = synchronized {
- globalId += 1
- globalId
- }
- }
-
object FreshIdentifier {
+ private val uniqueCounter = new UniqueCounter[String]()
+
// Replace $opcode inside a string with the symbolic operator name
private def decode(s: String) =
scala.reflect.NameTransformer.decode(s)
/** Builds a fresh identifier
+ *
* @param name The name of the identifier
* @param tpe The type of the identifier
- * @param alwaysShowUniqueID If the unique ID should always be shown */
+ * @param alwaysShowUniqueID If the unique ID should always be shown
+ */
def apply(name: String, tpe: TypeTree = Untyped, alwaysShowUniqueID: Boolean = false) : Identifier =
- new Identifier(decode(name), UniqueCounter.nextGlobal, UniqueCounter.next(name), tpe, alwaysShowUniqueID)
+ new Identifier(decode(name), uniqueCounter.nextGlobal, uniqueCounter.next(name), tpe, alwaysShowUniqueID)
/** Builds a fresh identifier, whose ID is always shown
+ *
* @param name The name of the identifier
* @param forceId The forced ID of the identifier
- * @param tpe The type of the identifier */
+ * @param tpe The type of the identifier
+ */
def apply(name: String, forceId: Int, tpe: TypeTree): Identifier =
- new Identifier(decode(name), UniqueCounter.nextGlobal, forceId, tpe, true)
+ new Identifier(decode(name), uniqueCounter.nextGlobal, forceId, tpe, alwaysShowUniqueID = true)
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 29540f2f4cbb255dbd1f58d1070ef16b37620b69..e90749e95c50764626d3b57cd3a9776087a8a6a7 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -50,7 +50,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
/* Printing VCs */
protected lazy val out: Option[java.io.FileWriter] = if (reporter.isDebugEnabled) Some {
val file = context.files.headOption.map(_.getName).getOrElse("NA")
- val n = VCNumbers.getNext(targetName+file)
+ val n = VCNumbers.next(targetName+file)
val dir = new java.io.File("smt-sessions")
@@ -794,11 +794,4 @@ abstract class SMTLIBSolver(val context: LeonContext,
}
// Unique numbers
-protected object VCNumbers {
- private var nexts = Map[String, Int]().withDefaultValue(0)
- def getNext(id: String) = {
- val n = nexts(id)+1
- nexts += id -> n
- n
- }
-}
+private [smtlib] object VCNumbers extends UniqueCounter[String]
diff --git a/src/main/scala/leon/synthesis/rules/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
index 9d9e360e246e8533f3f85b1792079f8268f6425c..2bc58307fb66449e13d889fceab03b45bb4c868f 100644
--- a/src/main/scala/leon/synthesis/rules/TEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
@@ -5,19 +5,12 @@ package synthesis
package rules
import purescala.Expressions._
-import purescala.Definitions._
import purescala.Types._
import purescala.Constructors._
-import solvers._
import datagen._
-
import evaluators._
import codegen.CodeGenParams
-
-import utils._
-import leon.utils._
-
import grammars._
import scala.collection.mutable.{HashMap => MutableMap}
@@ -32,16 +25,11 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
reorderInterval: Int = 50
)
- private class Counter(private var v: Int = 0) {
- def inc() = v += 1
- def value() = v
- }
-
def getParams(sctx: SynthesisContext, p: Problem): TegisParams
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- return Nil;
+ return Nil
List(new RuleInstantiation(this.name) {
def apply(hctx: SearchContext): RuleApplication = {
@@ -78,7 +66,7 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
gi.iterator
}
- var tests = p.eb.valids.map(_.ins).distinct.map(t => (t, new Counter(0)))
+ var tests = p.eb.valids.map(_.ins).distinct
if (gi.nonEmpty) {
diff --git a/src/main/scala/leon/utils/UniqueCounter.scala b/src/main/scala/leon/utils/UniqueCounter.scala
new file mode 100644
index 0000000000000000000000000000000000000000..06a6c0bb4b1badd63df38c3285c5fd8514d249fb
--- /dev/null
+++ b/src/main/scala/leon/utils/UniqueCounter.scala
@@ -0,0 +1,20 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.utils
+
+class UniqueCounter[K] {
+
+ private var globalId = -1
+ private var nameIds = Map[K, Int]().withDefaultValue(-1)
+
+ def next(key: K): Int = synchronized {
+ nameIds += key -> (1+nameIds(key))
+ nameIds(key)
+ }
+
+ def nextGlobal = synchronized {
+ globalId += 1
+ globalId
+ }
+
+}