From 622632dfb0af78036ee51ade4405699935f0077e Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Thu, 28 Apr 2016 10:42:31 +0200
Subject: [PATCH] synchronized evaluator invariant cache & small fix in codegen
---
src/main/scala/leon/codegen/CompilationUnit.scala | 10 +++++++---
src/main/scala/leon/evaluators/Evaluator.scala | 5 +++--
2 files changed, 10 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 366feffaf..88f1679bc 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -213,9 +213,13 @@ class CompilationUnit(val ctx: LeonContext,
case CaseClass(cct, args) =>
caseClassConstructor(cct.classDef) match {
case Some(cons) =>
- val tpeParam = if (cct.tps.isEmpty) Seq() else Seq(cct.tps.map(registerType).toArray)
- val jvmArgs = monitor +: (tpeParam ++ args.map(valueToJVM))
- cons.newInstance(jvmArgs.toArray : _*).asInstanceOf[AnyRef]
+ try {
+ val tpeParam = if (cct.tps.isEmpty) Seq() else Seq(cct.tps.map(registerType).toArray)
+ val jvmArgs = monitor +: (tpeParam ++ args.map(valueToJVM))
+ cons.newInstance(jvmArgs.toArray : _*).asInstanceOf[AnyRef]
+ } catch {
+ case e : java.lang.reflect.InvocationTargetException => throw e.getCause
+ }
case None =>
ctx.reporter.fatalError("Case class constructor not found?!?")
}
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index 5ae1a57a6..c3d4c737f 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -138,14 +138,15 @@ object Evaluator {
case object Pending extends CheckStatus
case object NoCheck extends CheckStatus
- def invariantCheck(cc: CaseClass): CheckStatus =
+ def invariantCheck(cc: CaseClass): CheckStatus = synchronized {
if (!cc.ct.classDef.hasInvariant) Complete(true)
else checkCache.get(cc).getOrElse {
checkCache(cc) = Pending
NoCheck
}
+ }
- def invariantResult(cc: CaseClass, success: Boolean): Unit = {
+ def invariantResult(cc: CaseClass, success: Boolean): Unit = synchronized {
checkCache(cc) = Complete(success)
}
--
GitLab