epfl-lara · jad-hamza · Feb 23, 2021 · Feb 18, 2021 · Feb 19, 2021 · Feb 19, 2021
diff --git a/build.sbt b/build.sbt
@@ -31,7 +31,7 @@ lazy val nParallel = {
   }
 }
 
-val SupportedScalaVersions = Seq("2.12.9")
+val SupportedScalaVersions = Seq("2.12.13")
 
 lazy val frontendClass = settingKey[String]("The name of the compiler wrapper used to extract stainless trees")
 
@@ -83,13 +83,8 @@ lazy val commonSettings: Seq[Setting[_]] = artifactSettings ++ Seq(
     "-feature"
   ),
 
-  // unmanagedJars in Runtime += {
-  //   root.base / "unmanaged" / s"scalaz3-$osName-$osArch-${scalaBinaryVersion.value}.jar"
-  // },
-
   resolvers ++= Seq(
-    Resolver.sonatypeRepo("releases"),
-    Resolver.bintrayRepo("epfl-lara", "maven"),
+    Resolver.sonatypeRepo("releases").withAllowInsecureProtocol(true),
     ("uuverifiers" at "http://logicrunch.research.it.uu.se/maven").withAllowInsecureProtocol(true),
   ),
 
@@ -222,7 +217,7 @@ val scriptSettings: Seq[Setting[_]] = Seq(
 def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
 
 // lazy val inox = RootProject(file("../inox"))
-lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "5ff41439402ae7543675ab2976163a6d3785a608")
+lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "1b17cb4d38dfddf16286e3346929b7a05267c380")
 //lazy val dotty = ghProject("git://github.com/lampepfl/dotty.git", "b3194406d8e1a28690faee12257b53f9dcf49506")
 
 // Allow integration test to use facilities from regular tests

diff --git a/core/src/main/scala/stainless/genc/CAST.scala b/core/src/main/scala/stainless/genc/CAST.scala
@@ -216,7 +216,7 @@ object CAST { // C Abstract Syntax Tree
   /* ---------------------------------------------------------- Helpers ----- */
   // Flatten blocks together and remove `()` literals
   def buildBlock(exprs: Seq[Expr]): Block = {
-    val block = (Seq[Expr]() /: (exprs filterNot isUnitLit)) {
+    val block = (exprs filterNot isUnitLit).foldLeft(Seq.empty[Expr]) {
       case (acc, e) => e match {
         case Block(exprs) => acc ++ exprs
         case expr => acc :+ expr

diff --git a/core/src/main/scala/stainless/genc/ir/IR.scala b/core/src/main/scala/stainless/genc/ir/IR.scala
@@ -305,7 +305,7 @@ private[genc] sealed trait IR { ir =>
   def buildBlock(exprs: Seq[Expr]): Block = {
     require(exprs.nonEmpty)
 
-    val block = (Seq[Expr]() /: exprs) {
+    val block = exprs.foldLeft(Seq[Expr]()) {
       case (acc, e) => e match {
         case Block(exprs) => acc ++ exprs
         case expr => acc :+ expr

diff --git a/core/src/main/scala/stainless/genc/ir/Normaliser.scala b/core/src/main/scala/stainless/genc/ir/Normaliser.scala
@@ -246,7 +246,7 @@ final class Normaliser(val ctx: inox.Context) extends Transformer(CIR, NIR) with
   //  - the arguments themselves
   private def flattenAll(args0: Expr*)(implicit env: Env): (Seq[Seq[to.Expr]], Seq[to.Expr]) = {
     val empty = (Seq[Seq[to.Expr]](), Seq[to.Expr]()) // initSS + lastS
-    val (initss1, args1) = (empty /: args0) { case ((initss, lasts), e) =>
+    val (initss1, args1) = args0.foldLeft(empty) { case ((initss, lasts), e) =>
       val (init, last) = flatten(e)
       (initss :+ init, lasts :+ last)
     }

diff --git a/core/src/main/scala/stainless/genc/ir/Transformer.scala b/core/src/main/scala/stainless/genc/ir/Transformer.scala
@@ -80,7 +80,7 @@ abstract class Transformer[From <: IR, To <: IR](final val from: From, final val
       val acc2 = acc + (current -> transformed)
       val subs = current.getDirectChildren
 
-      (acc2 /: subs) { case (acc3, sub) => topDown(Some(transformed), sub, acc3) }
+      subs.foldLeft(acc2) { case (acc3, sub) => topDown(Some(transformed), sub, acc3) }
     }
 
     val top = cd.hierarchyTop

diff --git a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala
@@ -326,7 +326,7 @@ private class S2IRImpl(val ctx: inox.Context, val ctxDB: FunCtxDB, val deps: Dep
     }
 
     // Combine all cases, using a foldRight
-    val patmat = (cases.init :\ last) { case (caze, acc) =>
+    val patmat = cases.init.foldRight(last) { case (caze, acc) =>
       CIR.IfElse(caze.fullCondition, caze.body, acc)
     }
 
@@ -554,11 +554,13 @@ private class S2IRImpl(val ctx: inox.Context, val ctxDB: FunCtxDB, val deps: Dep
     def recTopDown(ct: ClassType, parent: Option[CIR.ClassDef], acc: Translation): Translation = {
       val tcd = ct.tcd
       val cd = tcd.cd
+      val id = buildId(ct)
+
       if (cd.isDropped || cd.isManuallyTyped)
-        ctx.reporter.fatalError(ct.getPos, s"${ct.id} is not convertible to ClassDef in GenC")
+        ctx.reporter.fatalError(ct.getPos, s"${ct.id.asString} is not convertible to ClassDef in GenC")
 
-      val id = buildId(ct)
-      assert(!cd.isCaseObject)
+      if (cd.isCaseObject)
+        ctx.reporter.fatalError(ct.getPos, s"Case objects (${ct.id.asString}) are not convertible to ClassDef in GenC")
 
       // Use the class definition id, not the typed one as they might not match.
       val nonGhostFields = tcd.fields.filter(!_.flags.contains(Ghost))
@@ -571,7 +573,7 @@ private class S2IRImpl(val ctx: inox.Context, val ctxDB: FunCtxDB, val deps: Dep
 
       // Recurse down
       val children = cd.children map { _.typed(ct.tps) }
-      (newAcc /: children) { case (currentAcc, child) => recTopDown(child.toType, Some(clazz), currentAcc) }
+      children.foldLeft(newAcc) { case (currentAcc, child) => recTopDown(child.toType, Some(clazz), currentAcc) }
     }
 
     val translation = recTopDown(syms.getClass(root(ct.id)).typed(ct.tps).toType, None, Map.empty)

diff --git a/core/src/main/scala/stainless/verification/VerificationComponent.scala b/core/src/main/scala/stainless/verification/VerificationComponent.scala
@@ -113,7 +113,9 @@ class VerificationRun(override val pipeline: StainlessPipeline)
         reporter.debug(s"Generating VCs for those functions: ${functions map { _.uniqueName } mkString ", "}")
 
       val vcs = if (context.options.findOptionOrDefault(optTypeChecker))
-        TypeChecker(assertionEncoder.targetProgram, context).checkFunctionsAndADTs(functions)
+        context.timers.verification.get("type-checker").run {
+          TypeChecker(assertionEncoder.targetProgram, context).checkFunctionsAndADTs(functions)
+        }
       else
         VerificationGenerator.gen(assertionEncoder.targetProgram, context)(functions)
 

diff --git a/frontends/library/stainless/collection/ConcRope.scala b/frontends/library/stainless/collection/ConcRope.scala
@@ -2,7 +2,6 @@
 
 package stainless.collection
 
-import stainless.collection._
 import stainless.lang._
 import stainless.proof._
 import stainless.lang.StaticChecks._
@@ -68,7 +67,6 @@ object ConcRope {
 
   @library
   sealed abstract class Conc[T] {
-    import Conc._
 
     def isEmpty: Boolean = {
       this == Empty[T]()

diff --git a/frontends/library/stainless/collection/List.scala b/frontends/library/stainless/collection/List.scala
@@ -3,14 +3,11 @@
 package stainless.collection
 
 import scala.annotation.tailrec
-import scala.language.implicitConversions
 import scala.collection.immutable.{List => ScalaList}
 
-import stainless._
 import stainless.lang._
 import stainless.lang.StaticChecks._
 import stainless.annotation._
-import stainless.math._
 import stainless.proof._
 
 @library

diff --git a/frontends/library/stainless/io/FileInputStream.scala b/frontends/library/stainless/io/FileInputStream.scala
@@ -2,8 +2,6 @@
 
 package stainless.io
 
-import scala.language.implicitConversions
-
 import stainless.lang._
 import stainless.annotation._
 import stainless.lang.StaticChecks._

diff --git a/frontends/library/stainless/io/FileOutputStream.scala b/frontends/library/stainless/io/FileOutputStream.scala
@@ -2,8 +2,6 @@
 
 package stainless.io
 
-import scala.language.implicitConversions
-
 import stainless.lang._
 import stainless.annotation._
 import stainless.lang.StaticChecks._

diff --git a/frontends/library/stainless/io/StdIn.scala b/frontends/library/stainless/io/StdIn.scala
@@ -2,8 +2,6 @@
 
 package stainless.io
 
-import scala.language.implicitConversions
-
 import stainless.annotation._
 import stainless.lang.StaticChecks._
 

diff --git a/frontends/library/stainless/io/StdOut.scala b/frontends/library/stainless/io/StdOut.scala
@@ -2,10 +2,7 @@
 
 package stainless.io
 
-import scala.language.implicitConversions
-
 import stainless.annotation._
-import stainless.lang.StaticChecks._
 import stainless.math.BitVectors._
 
 object StdOut {

diff --git a/frontends/library/stainless/io/package.scala b/frontends/library/stainless/io/package.scala
@@ -2,10 +2,7 @@
 
 package stainless
 
-import scala.language.implicitConversions
-
 import stainless.annotation._
-import stainless.lang.StaticChecks._
 
 package object io {
 

diff --git a/frontends/library/stainless/lang/Bag.scala b/frontends/library/stainless/lang/Bag.scala
@@ -2,11 +2,7 @@
 
 package stainless.lang
 
-import scala.language.implicitConversions
-
 import stainless.annotation._
-import stainless.lang.StaticChecks._
-
 
 object Bag {
   @library @inline

diff --git a/frontends/library/stainless/lang/Either.scala b/frontends/library/stainless/lang/Either.scala
@@ -2,8 +2,6 @@
 
 package stainless.lang
 
-import scala.language.implicitConversions
-
 import stainless.annotation._
 import stainless.lang.StaticChecks._
 

diff --git a/frontends/library/stainless/lang/Map.scala b/frontends/library/stainless/lang/Map.scala
@@ -2,7 +2,6 @@
 
 package stainless.lang
 
-import scala.language.implicitConversions
 import scala.collection.immutable.{Map => ScalaMap}
 
 import StaticChecks._

diff --git a/frontends/library/stainless/lang/MutableMap.scala b/frontends/library/stainless/lang/MutableMap.scala
@@ -3,7 +3,6 @@
 package stainless.lang
 
 import stainless.annotation._
-import stainless.lang.StaticChecks._
 
 object MutableMap {
   @extern @library

diff --git a/frontends/library/stainless/lang/Option.scala b/frontends/library/stainless/lang/Option.scala
@@ -2,8 +2,6 @@
 
 package stainless.lang
 
-import scala.language.implicitConversions
-
 import stainless.annotation._
 import stainless.lang.StaticChecks._
 

diff --git a/frontends/library/stainless/lang/PartialFunction.scala b/frontends/library/stainless/lang/PartialFunction.scala
@@ -3,8 +3,6 @@
 package stainless
 package lang
 
-import scala.language.implicitConversions
-
 import annotation._
 import stainless.lang.StaticChecks._
 

diff --git a/frontends/library/stainless/lang/Real.scala b/frontends/library/stainless/lang/Real.scala
@@ -3,9 +3,6 @@
 package stainless.lang
 
 import stainless.annotation._
-import stainless.lang.StaticChecks._
-
-import scala.language.implicitConversions
 
 @ignore
 class Real(val theReal: scala.math.BigDecimal) {

diff --git a/frontends/library/stainless/lang/Set.scala b/frontends/library/stainless/lang/Set.scala
@@ -6,7 +6,6 @@ import StaticChecks._
 import stainless.annotation._
 import stainless.collection.{List, ListOps}
 
-import scala.language.implicitConversions
 import scala.collection.immutable.{Set => ScalaSet}
 
 object Set {

diff --git a/frontends/library/stainless/lang/StaticChecks.scala b/frontends/library/stainless/lang/StaticChecks.scala
@@ -1,7 +1,6 @@
 package stainless.lang
 
 import stainless.annotation._
-import scala.language.implicitConversions
 
 object StaticChecks {
 

diff --git a/frontends/library/stainless/lang/StrOps.scala b/frontends/library/stainless/lang/StrOps.scala
@@ -2,10 +2,7 @@
 
 package stainless.lang
 
-import scala.language.implicitConversions
-
 import stainless.annotation._
-import stainless.lang.StaticChecks._
 
 /**
  * @author Mikael

diff --git a/frontends/library/stainless/lang/package.scala b/frontends/library/stainless/lang/package.scala
@@ -5,10 +5,7 @@ package stainless
 import stainless.annotation._
 import stainless.lang.StaticChecks._
 
-import scala.language.implicitConversions
-
 package object lang {
-  import stainless.proof._
 
   @library
   def ghost[A](@ghost value: A): Unit = ()

diff --git a/frontends/library/stainless/math/BitVectors.scala b/frontends/library/stainless/math/BitVectors.scala
@@ -4,14 +4,9 @@ package stainless
 package math
 
 import stainless.annotation._
-import stainless.lang._
-import stainless.lang.StaticChecks._
 import scala.collection.immutable.BitSet
-
-import scala.language.higherKinds
 import scala.language.implicitConversions
 
-
 // TODO: write the Scala implementation
 
 @library

diff --git a/frontends/library/stainless/proof/Internal.scala b/frontends/library/stainless/proof/Internal.scala
@@ -6,8 +6,6 @@ import stainless.lang._
 import stainless.annotation._
 import stainless.lang.StaticChecks._
 
-import scala.language.implicitConversions
-
 /** Internal helper classes and methods for the 'proof' package. */
 object Internal {
 

diff --git a/frontends/library/stainless/util/Random.scala b/frontends/library/stainless/util/Random.scala
@@ -2,8 +2,6 @@
 
 package stainless.util
 
-import scala.language.implicitConversions
-
 import stainless.annotation._
 import stainless.lang.StaticChecks._
 import stainless.io._

diff --git a/frontends/scalac/src/it/scala/stainless/GhostRewriteSuite.scala b/frontends/scalac/src/it/scala/stainless/GhostRewriteSuite.scala
@@ -9,14 +9,14 @@ import org.scalatest._
 import stainless.frontends.scalac.StainlessPlugin
 
 class GhostRewriteSuite extends FunSpec {
-  val reporter = new StoreReporter
+  val settings = new Settings()
+  settings.stopAfter.value = List("refchecks")
+  settings.usejavacp.value = false
+  settings.classpath.value = Main.extraClasspath
 
-  def newCompiler: CheckingGlobal = {
-    val settings = new Settings()
-    settings.stopAfter.value = List("refchecks")
-    settings.usejavacp.value = false
-    settings.classpath.value = Main.extraClasspath
+  val reporter = new StoreReporter(settings)
 
+  def newCompiler: CheckingGlobal = {
     new CheckingGlobal(settings)
   }
 
@@ -51,7 +51,7 @@ class GhostRewriteSuite extends FunSpec {
     }
   }
 
-  def ignoreError(i: reporter.Info) = {
+  def ignoreError(i: StoreReporter.Info) = {
     val s = i.toString
 
     s.contains("The Z3 native interface is not available") ||