From 6aea23f23f7df9544380b0b32d7422bcd107a128 Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Wed, 27 Sep 2017 11:55:28 +0200
Subject: [PATCH 1/4] Quick'n'dirty fix for SimplifierWithPC

This ensures that the trait is thread safe. Ideally, it's internal state
shouldn't be mutable and/or the critical section should be reduced to
its minimal size for better thoughput efficiency.
---
 src/main/scala/inox/transformers/SimplifierWithPC.scala | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/inox/transformers/SimplifierWithPC.scala b/src/main/scala/inox/transformers/SimplifierWithPC.scala
index 9d3322b2d..1f96df28b 100644
--- a/src/main/scala/inox/transformers/SimplifierWithPC.scala
+++ b/src/main/scala/inox/transformers/SimplifierWithPC.scala
@@ -216,11 +216,11 @@ trait SimplifierWithPC extends TransformerWithPC { self =>
     }
   }
 
-  def isPure(e: Expr, path: CNFPath): Boolean = simplify(e, path)._2
+  def isPure(e: Expr, path: CNFPath): Boolean = synchronized { simplify(e, path)._2 }
 
   private val simplifyCache = new LruCache[Expr, (CNFPath, Expr, Boolean)](100)
 
-  def simplify(e: Expr, path: CNFPath): (Expr, Boolean) = e match {
+  private def simplify(e: Expr, path: CNFPath): (Expr, Boolean) = e match {
     case e if path contains e => (BooleanLiteral(true), true)
     case e if path contains not(e) => (BooleanLiteral(false), true)
 
@@ -423,7 +423,7 @@ trait SimplifierWithPC extends TransformerWithPC { self =>
     (re, pe)
   }
 
-  override protected def rec(e: Expr, path: CNFPath): Expr = {
+  override protected def rec(e: Expr, path: CNFPath): Expr = synchronized {
     stack = if (stack.isEmpty) Nil else (stack.head + 1) :: stack.tail
     val (re, pe) = simplify(e, path)
     purity = if (stack.isEmpty) purity else pe :: purity
-- 
GitLab


From 73aafe29aa32d7f66f495f2813db09132f7d1498 Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Wed, 27 Sep 2017 18:20:06 +0200
Subject: [PATCH 2/4] Use thread local variables instead of heavy locks

---
 .../inox/transformers/SimplifierWithPC.scala  | 22 ++++++++++---------
 1 file changed, 12 insertions(+), 10 deletions(-)

diff --git a/src/main/scala/inox/transformers/SimplifierWithPC.scala b/src/main/scala/inox/transformers/SimplifierWithPC.scala
index 1f96df28b..789c4e7a9 100644
--- a/src/main/scala/inox/transformers/SimplifierWithPC.scala
+++ b/src/main/scala/inox/transformers/SimplifierWithPC.scala
@@ -4,6 +4,8 @@ package inox
 package transformers
 
 import utils._
+
+import scala.util.DynamicVariable
 import scala.collection.mutable.{Map => MutableMap}
 
 trait SimplifierWithPC extends TransformerWithPC { self =>
@@ -170,8 +172,8 @@ trait SimplifierWithPC extends TransformerWithPC { self =>
   //      (since aggressive caching of cnf computations is taking place)
   def initEnv: CNFPath = CNFPath.empty
 
-  private[this] var stack: List[Int] = Nil
-  private[this] var purity: List[Boolean] = Nil
+  private[this] var dynStack: DynamicVariable[List[Int]] = new DynamicVariable(Nil)
+  private[this] var dynPurity: DynamicVariable[List[Boolean]] = new DynamicVariable(Nil)
 
   private val pureCache: MutableMap[Identifier, Boolean] = MutableMap.empty
 
@@ -216,7 +218,7 @@ trait SimplifierWithPC extends TransformerWithPC { self =>
     }
   }
 
-  def isPure(e: Expr, path: CNFPath): Boolean = synchronized { simplify(e, path)._2 }
+  def isPure(e: Expr, path: CNFPath): Boolean = simplify(e, path)._2
 
   private val simplifyCache = new LruCache[Expr, (CNFPath, Expr, Boolean)](100)
 
@@ -407,12 +409,12 @@ trait SimplifierWithPC extends TransformerWithPC { self =>
     }
 
     case _ =>
-      stack = 0 :: stack
+      dynStack.value = 0 :: dynStack.value
       val re = super.rec(e, path)
-      val (rpure, rest) = purity.splitAt(stack.head)
+      val (rpure, rest) = dynPurity.value.splitAt(dynStack.value.head)
       val pe = rpure.foldLeft(opts.assumeChecked || !isImpureExpr(re))(_ && _)
-      stack = stack.tail
-      purity = rest
+      dynStack.value = dynStack.value.tail
+      dynPurity.value = rest
       (re, pe)
   }
 
@@ -423,10 +425,10 @@ trait SimplifierWithPC extends TransformerWithPC { self =>
     (re, pe)
   }
 
-  override protected def rec(e: Expr, path: CNFPath): Expr = synchronized {
-    stack = if (stack.isEmpty) Nil else (stack.head + 1) :: stack.tail
+  override protected def rec(e: Expr, path: CNFPath): Expr = {
+    dynStack.value = if (dynStack.value.isEmpty) Nil else (dynStack.value.head + 1) :: dynStack.value.tail
     val (re, pe) = simplify(e, path)
-    purity = if (stack.isEmpty) purity else pe :: purity
+    dynPurity.value = if (dynStack.value.isEmpty) dynPurity.value else pe :: dynPurity.value
     re
   }
 }
-- 
GitLab


From 786ab00ccf8d5c4331d464c9aa7a667bd25e48a3 Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Thu, 28 Sep 2017 10:28:41 +0200
Subject: [PATCH 3/4] Further improve thread safety of SimplifierWithPC

---
 .../inox/transformers/SimplifierWithPC.scala  | 32 ++++++++++---------
 1 file changed, 17 insertions(+), 15 deletions(-)

diff --git a/src/main/scala/inox/transformers/SimplifierWithPC.scala b/src/main/scala/inox/transformers/SimplifierWithPC.scala
index 789c4e7a9..a4813b3dc 100644
--- a/src/main/scala/inox/transformers/SimplifierWithPC.scala
+++ b/src/main/scala/inox/transformers/SimplifierWithPC.scala
@@ -177,24 +177,26 @@ trait SimplifierWithPC extends TransformerWithPC { self =>
 
   private val pureCache: MutableMap[Identifier, Boolean] = MutableMap.empty
 
-  private def isPureFunction(id: Identifier): Boolean = opts.assumeChecked || (pureCache.get(id) match {
-    case Some(b) => b
-    case None =>
-      val fd = getFunction(id)
-      if (transitivelyCalls(fd, fd)) {
-        pureCache += id -> false
-        false
-      } else {
-        pureCache += id -> true
-        if (isPure(fd.fullBody, CNFPath.empty)) {
-          true
-        } else {
+  private def isPureFunction(id: Identifier): Boolean = opts.assumeChecked || synchronized {
+    pureCache.get(id) match {
+      case Some(b) => b
+      case None =>
+        val fd = getFunction(id)
+        if (transitivelyCalls(fd, fd)) {
           pureCache += id -> false
-          transitiveCallers(fd).foreach(fd => pureCache += fd.id -> false)
           false
+        } else {
+          if (isPure(fd.fullBody, CNFPath.empty)) {
+            pureCache += id -> true
+            true
+          } else {
+            pureCache += id -> false
+            transitiveCallers(fd) foreach { pureCache += _.id -> false }
+            false
+          }
         }
-      }
-  })
+    }
+  }
 
   private def isInstanceOf(e: Expr, tpe: ADTType, path: CNFPath): Option[Boolean] = {
     val tadt = tpe.getADT
-- 
GitLab


From fd14dde0ecc81ec35ef6d9223d7fac987e1c612a Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Thu, 28 Sep 2017 14:28:41 +0200
Subject: [PATCH 4/4] Update SimplifierWithPC.isPureFunction

---
 .../inox/transformers/SimplifierWithPC.scala  | 41 ++++++++++---------
 1 file changed, 21 insertions(+), 20 deletions(-)

diff --git a/src/main/scala/inox/transformers/SimplifierWithPC.scala b/src/main/scala/inox/transformers/SimplifierWithPC.scala
index a4813b3dc..6c10d4ca6 100644
--- a/src/main/scala/inox/transformers/SimplifierWithPC.scala
+++ b/src/main/scala/inox/transformers/SimplifierWithPC.scala
@@ -175,27 +175,28 @@ trait SimplifierWithPC extends TransformerWithPC { self =>
   private[this] var dynStack: DynamicVariable[List[Int]] = new DynamicVariable(Nil)
   private[this] var dynPurity: DynamicVariable[List[Boolean]] = new DynamicVariable(Nil)
 
-  private val pureCache: MutableMap[Identifier, Boolean] = MutableMap.empty
-
-  private def isPureFunction(id: Identifier): Boolean = opts.assumeChecked || synchronized {
-    pureCache.get(id) match {
-      case Some(b) => b
+  private sealed abstract class PurityCheck
+  private case object Pure extends PurityCheck
+  private case object Impure extends PurityCheck
+  private case object Checking extends PurityCheck
+
+  private[this] val pureCache: MutableMap[Identifier, PurityCheck] = MutableMap.empty
+
+  private def isPureFunction(id: Identifier): Boolean = {
+    opts.assumeChecked ||
+    synchronized(pureCache.get(id) match {
+      case Some(Pure) => true
+      case Some(Impure) => false
+      case Some(Checking) =>
+        // Function is recursive and cycles were not pruned by the simplifier.
+        // No need to update pureCache here as the update will take place in the next branch.
+        false
       case None =>
-        val fd = getFunction(id)
-        if (transitivelyCalls(fd, fd)) {
-          pureCache += id -> false
-          false
-        } else {
-          if (isPure(fd.fullBody, CNFPath.empty)) {
-            pureCache += id -> true
-            true
-          } else {
-            pureCache += id -> false
-            transitiveCallers(fd) foreach { pureCache += _.id -> false }
-            false
-          }
-        }
-    }
+        pureCache += id -> Checking
+        val p = isPure(getFunction(id).fullBody, CNFPath.empty)
+        pureCache += id -> (if (p) Pure else Impure)
+        p
+    })
   }
 
   private def isInstanceOf(e: Expr, tpe: ADTType, path: CNFPath): Option[Boolean] = {
-- 
GitLab