diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala index 0ac7ae01aad3ef7913a80d324f2b90285d18a6ba..309c676ff872f6cd33f464982f709775e5214cbd 100644 --- a/src/main/scala/leon/codegen/CodeGeneration.scala +++ b/src/main/scala/leon/codegen/CodeGeneration.scala @@ -72,6 +72,7 @@ trait CodeGeneration { 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" def idToSafeJVMName(id: Identifier) = id.uniqueName.replaceAll("\\.", "\\$") @@ -695,6 +696,11 @@ trait CodeGeneration { ch << InvokeStatic(ChooseEntryPointClass, "invoke", "(I[Ljava/lang/Object;)Ljava/lang/Object;") mkUnbox(choose.getType, ch) + + case gv @ GenericValue(tp, int) => + val id = runtime.GenericValues.register(gv); + ch << Ldc(id) + ch << InvokeStatic(GenericValuesClass, "get", "(I)Ljava/lang/Object;") case This(ct) => ch << ALoad(0) // FIXME what if doInstrument etc diff --git a/src/main/scala/leon/codegen/runtime/GenericValues.scala b/src/main/scala/leon/codegen/runtime/GenericValues.scala new file mode 100644 index 0000000000000000000000000000000000000000..790f35a5ca64a7971d45109820e440135999534f --- /dev/null +++ b/src/main/scala/leon/codegen/runtime/GenericValues.scala @@ -0,0 +1,37 @@ +/* Copyright 2009-2014 EPFL, Lausanne */ + +package leon +package codegen.runtime + +import utils._ +import purescala.Common._ +import purescala.Definitions._ +import purescala.Trees.{Tuple => LeonTuple, _} +import purescala.TreeOps.valuateWithModel +import purescala.TypeTrees._ + +import scala.collection.immutable.{Map => ScalaMap} + +import synthesis._ + +object GenericValues { + private[this] var counter = 0; + + private[this] var gvToI = ScalaMap[GenericValue, Int]() + private[this] var iTogv = ScalaMap[Int, GenericValue]() + + def register(gv: GenericValue): Int = { + if (gvToI contains gv) { + gvToI(gv) + } else { + counter += 1; + gvToI += gv -> counter + iTogv += counter -> gv + counter + } + } + + def get(i: Int): java.lang.Object = { + iTogv(i) + } +}