WebAssembly backend

core/src/main/scala/stainless/Component.scala

@@ -2,13 +2,11 @@
 
 package stainless
 
+import utils.{CheckFilter, DefinitionIdFinder, DependenciesFinder}
 import extraction.xlang.{trees => xt}
-import utils.CheckFilter
-
 import io.circe._
 
 import scala.concurrent.Future
-
 import scala.language.existentials
 
 trait Component { self =>
@@ -72,16 +70,29 @@ trait ComponentRun { self =>
   private[this] final val extractionFilter = createFilter
 
   /** Sends the symbols through the extraction pipeline. */
-  def extract(symbols: extraction.xlang.trees.Symbols): trees.Symbols = extractionPipeline extract symbols
+  def extract(symbols: xt.Symbols): trees.Symbols = extractionPipeline extract symbols
 
   /** Sends the program's symbols through the extraction pipeline. */
-  def extract(program: inox.Program { val trees: extraction.xlang.trees.type }): inox.Program {
+  def extract(program: inox.Program { val trees: xt.type }): inox.Program {
     val trees: self.trees.type
   } = inox.Program(trees)(extract(program.symbols))
 
+  /** Override this if you need another kind of filtering */
+  protected lazy val dependenciesFinder = new DependenciesFinder {
+    val t: self.trees.type = self.trees
+    protected def traverser(symbols: t.Symbols) = new DefinitionIdFinder {
+      val trees: t.type = t
+      val s: t.Symbols = symbols
+    }
+  }
+
+  private def filter(ids: Seq[Identifier], symbols: trees.Symbols): trees.Symbols = {
+    dependenciesFinder.findDependencies(ids.toSet, symbols)
+  }
+
   /** Passes the provided symbols through the extraction pipeline and processes all
     * functions derived from the provided identifier. */
-  def apply(id: Identifier, symbols: extraction.xlang.trees.Symbols): Future[Analysis] = try {
+  def apply(ids: Seq[Identifier], symbols: xt.Symbols, filterSymbols: Boolean = false): Future[Analysis] = try {
 
     val exSymbols = extract(symbols)
 
@@ -90,7 +101,7 @@ trait ComponentRun { self =>
         .filter(_.flags.exists { case trees.Derived(id) => ids(id) case _ => false })
         .filter(extractionFilter.shouldBeChecked)
         .map(_.id)
-    } (exSymbols.lookupFunction(id).filter(extractionFilter.shouldBeChecked).map(_.id).toSet)
+    } (ids.flatMap(id => exSymbols.lookupFunction(id).toSeq).filter(extractionFilter.shouldBeChecked).map(_.id).toSet)
 
     val toProcess = toCheck.toSeq.sortBy(exSymbols.getFunction(_).getPos)
 
@@ -102,12 +113,18 @@ trait ComponentRun { self =>
       }
     }
 
-    apply(toProcess, exSymbols)
+    if (filterSymbols)
+      execute(toProcess, filter(toProcess, exSymbols))
+    else
+      execute(toProcess, exSymbols)
   } catch {
-    case extraction.MissformedStainlessCode(tree, msg) =>
+    case extraction.MalformedStainlessCode(tree, msg) =>
       reporter.fatalError(tree.getPos, msg)
   }
 
-  private[stainless] def apply(functions: Seq[Identifier], symbols: trees.Symbols): Future[Analysis]
+  def apply(id: Identifier, symbols: xt.Symbols): Future[Analysis] =
+    apply(Seq(id), symbols)
+
+  private[stainless] def execute(functions: Seq[Identifier], symbols: trees.Symbols): Future[Analysis]
 }
 

core/src/main/scala/stainless/MainHelpers.scala

@@ -3,9 +3,6 @@
 package stainless
 
 import utils.JsonUtils
-
-import scala.util.{ Failure, Success }
-
 import java.io.File
 
 import io.circe.Json
@@ -44,6 +41,7 @@ trait MainHelpers extends inox.MainHelpers {
     optWatch -> Description(General, "Re-run stainless upon file changes"),
     optCompact -> Description(General, "Print only invalid elements of summaries"),
     frontend.optPersistentCache -> Description(General, "Enable caching of program extraction & analysis"),
+    frontend.optBatchedProgram -> Description(General, "Process the whole program together, skip dependency analysis"),
     utils.Caches.optCacheDir -> Description(General, "Specify the directory in which cache files should be stored")
   ) ++ MainHelpers.components.map { component =>
     val option = inox.FlagOptionDef(component.name, default = false)

core/src/main/scala/stainless/ast/Deconstructors.scala

@@ -101,7 +101,7 @@ trait TreeDeconstructor extends inox.ast.TreeDeconstructor {
         var res = es
         var rtps = tps
         for ((hasGuard, ids, vs, es, tps, recons) <- recCases) yield {
-          var (currIds, nextIds) = rids.splitAt(ids.size)
+          val (currIds, nextIds) = rids.splitAt(ids.size)
           rids = nextIds
 
           val (currVs, nextVs) = rvs.splitAt(vs.size)

core/src/main/scala/stainless/ast/Definitions.scala

@@ -71,11 +71,11 @@ trait Definitions extends inox.ast.Definitions { self: Trees =>
         case _ => false
       }).map(_._2)
 
-      def get[T <: Definition : ClassTag](name: String): Option[T] = ({
+      def get[T <: Definition : ClassTag](name: String): Option[T] = {
         if (classTag[ADTSort].runtimeClass.isAssignableFrom(classTag[T].runtimeClass)) find(name, sorts)
         else if (classTag[FunDef].runtimeClass.isAssignableFrom(classTag[T].runtimeClass)) find(name, functions)
         else None
-      }).asInstanceOf[Option[T]]
+      }.asInstanceOf[Option[T]]
 
       def apply[T <: Definition : ClassTag](name: String): T = get[T](name).getOrElse {
         if (classTag[ADTSort].runtimeClass.isAssignableFrom(classTag[T].runtimeClass)) {

core/src/main/scala/stainless/ast/Expressions.scala

@@ -3,7 +3,7 @@
 package stainless
 package ast
 
-trait Expressions extends inox.ast.Expressions with inox.ast.Types { self: Trees =>
+trait Expressions extends inox.ast.Expressions with Types { self: Trees =>
 
   /** Stands for an undefined Expr, similar to `???` or `null`
     *
@@ -164,10 +164,10 @@ trait Expressions extends inox.ast.Expressions with inox.ast.Types { self: Trees
   protected def unapplyAccessor(unapplied: Expr, id: Identifier, up: UnapplyPattern)(implicit s: Symbols): Expr = {
     val fd = s.lookupFunction(id)
       .filter(_.params.size == 1)
-      .getOrElse(throw extraction.MissformedStainlessCode(up, "Invalid unapply accessor"))
+      .getOrElse(throw extraction.MalformedStainlessCode(up, "Invalid unapply accessor"))
     val unapp = up.getFunction
     val tpMap = s.instantiation(fd.params.head.getType, unapp.getType)
-      .getOrElse(throw extraction.MissformedStainlessCode(up, "Unapply pattern failed type instantiation"))
+      .getOrElse(throw extraction.MalformedStainlessCode(up, "Unapply pattern failed type instantiation"))
     fd.typed(fd.typeArgs map tpMap).applied(Seq(unapplied))
   }
 
@@ -177,11 +177,11 @@ trait Expressions extends inox.ast.Expressions with inox.ast.Types { self: Trees
 
     private def getIsEmpty(implicit s: Symbols): Identifier =
       getFunction.flags.collectFirst { case IsUnapply(isEmpty, _) => isEmpty }
-        .getOrElse(throw extraction.MissformedStainlessCode(this, "Unapply pattern on non-unapply method (isEmpty)"))
+        .getOrElse(throw extraction.MalformedStainlessCode(this, "Unapply pattern on non-unapply method (isEmpty)"))
 
     private def getGet(implicit s: Symbols): Identifier =
       getFunction.flags.collectFirst { case IsUnapply(_, get) => get }
-        .getOrElse(throw extraction.MissformedStainlessCode(this, "Unapply pattern on non-unapply method (get)"))
+        .getOrElse(throw extraction.MalformedStainlessCode(this, "Unapply pattern on non-unapply method (get)"))
 
     def isEmptyUnapplied(unapp: Expr)(implicit s: Symbols): Expr = unapplyAccessor(unapp, getIsEmpty, this).copiedFrom(this)
     def getUnapplied(unapp: Expr)(implicit s: Symbols): Expr = unapplyAccessor(unapp, getGet, this).copiedFrom(this)
@@ -199,8 +199,6 @@ trait Expressions extends inox.ast.Expressions with inox.ast.Types { self: Trees
 
   /* Array Operations */
 
-  sealed case class ArrayType(base: Type) extends Type
-
   /** $encodingof `Array(elems...)` */
   sealed case class FiniteArray(elems: Seq[Expr], base: Type) extends Expr with CachingTyped {
     override protected def computeType(implicit s: Symbols): Type = {

core/src/main/scala/stainless/ast/SymbolOps.scala

@@ -6,8 +6,6 @@ package ast
 import inox.utils.Position
 import inox.transformers.{TransformerOp, TransformerWithExprOp, TransformerWithTypeOp}
 
-import scala.collection.mutable.{Map => MutableMap}
-
 trait SymbolOps extends inox.ast.SymbolOps { self: TypeOps =>
   import trees._
   import trees.exprOps._
@@ -62,7 +60,7 @@ trait SymbolOps extends inox.ast.SymbolOps { self: TypeOps =>
         val tcons = getConstructor(id, tps)
         assert(tcons.fields.size == subps.size)
         val pairs = tcons.fields zip subps
-        val subTests = pairs.map(p => apply(adtSelector(in, p._1.id), p._2))
+        val subTests = pairs.map(p => apply(Annotated(adtSelector(in, p._1.id), Seq(Unchecked)), p._2))
         pp.empty withCond isCons(in, id) merge bind(ob, in) merge subTests
 
       case TuplePattern(ob, subps) =>
@@ -117,7 +115,7 @@ trait SymbolOps extends inox.ast.SymbolOps { self: TypeOps =>
         val tcons = getConstructor(id, tps)
         assert(tcons.fields.size == subps.size)
         val pairs = tcons.fields zip subps
-        val subMaps = pairs.map(p => mapForPattern(adtSelector(in, p._1.id), p._2))
+        val subMaps = pairs.map(p => mapForPattern(Annotated(adtSelector(in, p._1.id), Seq(Unchecked)), p._2))
         val together = subMaps.flatten.toMap
         bindIn(b) ++ together
 

core/src/main/scala/stainless/ast/Trees.scala

@@ -7,6 +7,7 @@ trait Trees
   extends inox.ast.Trees
      with Definitions
      with Expressions
+     with Types
      with Constructors
      with Deconstructors
      with TreeOps { self =>

core/src/main/scala/stainless/ast/TypeOps.scala

@@ -49,7 +49,7 @@ trait TypeOps extends inox.ast.TypeOps {
       ob.forall(vd => isSubtypeOf(vd.getType, in)) &&
       lookupFunction(id).exists(_.tparams.size == tps.size) && {
         val unapp = up.getFunction
-        unapp.params.size >= 1 &&
+        unapp.params.nonEmpty &&
         ob.forall(vd => isSubtypeOf(unapp.params.last.getType, vd.getType))
         (recs zip unapp.params.init).forall { case (r, vd) => isSubtypeOf(r.getType, vd.getType) } &&
         unapp.flags

core/src/main/scala/stainless/ast/Types.scala

@@ -0,0 +1,9 @@
+/* Copyright 2009-2018 EPFL, Lausanne */
+
+package stainless.ast
+
+trait Types extends inox.ast.Types { self: Trees =>
+
+  sealed case class ArrayType(base: Type) extends Type
+
+}

core/src/main/scala/stainless/codegen/CompilationUnit.scala

@@ -7,18 +7,13 @@ import inox.utils.UniqueCounter
 import runtime.Monitor
 
 import cafebabe._
-import cafebabe.AbstractByteCodes._
 import cafebabe.ByteCodes._
 import cafebabe.ClassFileTypes._
 import cafebabe.Flags._
 
-import scala.collection.JavaConverters._
-
 import java.lang.reflect.Constructor
 import java.lang.reflect.InvocationTargetException
 
-import evaluators._
-
 import scala.collection.mutable.{Map => MutableMap}
 
 trait CompilationUnit extends CodeGeneration {

core/src/main/scala/stainless/evaluators/EvaluatorComponent.scala

@@ -69,7 +69,7 @@ class EvaluatorRun(override val pipeline: extraction.StainlessPipeline)
 
   override def createFilter = EvaluatorCheckFilter(trees, context)
 
-  override def apply(functions: Seq[Identifier], symbols: Symbols): Future[Analysis] = {
+  private[stainless] def execute(functions: Seq[Identifier], symbols: Symbols): Future[Analysis] = {
     import context._
 
     val p = inox.Program(trees)(symbols)

core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala

@@ -110,7 +110,7 @@ trait RecursiveEvaluator extends inox.evaluators.RecursiveEvaluator {
 
       case (up @ UnapplyPattern(ob, rec, id, tps, subs), scrut) =>
         val eRec = rec map e
-        val unapp = e(FunctionInvocation(id, tps, eRec.toSeq :+ scrut))
+        val unapp = e(FunctionInvocation(id, tps, eRec :+ scrut))
         e(up.isEmptyUnapplied(unapp)) match {
           case BooleanLiteral(false) =>
             val extracted = e(up.getUnapplied(unapp))

core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala

@@ -174,14 +174,14 @@ trait AntiAliasing
               }
 
             for ((_, effects) <- localEffects.flatMap(_.flatMap(_._2)).groupBy(_.receiver)) {
-              val aliased = effects.toSeq.tails.flatMap {
+              val aliased = effects.tails.flatMap {
                 case e1 +: es => es.collect { case e2 if (e1 prefixOf e2) || (e2 prefixOf e1) => (e1, e2) }
                 case Nil => Nil
               }
 
               if (aliased.nonEmpty) {
                 val (e1, _) = aliased.next
-                throw MissformedStainlessCode(e1.receiver, "Illegal passing of aliased parameter")
+                throw MalformedStainlessCode(e1.receiver, "Illegal passing of aliased parameter")
               }
             }
 
@@ -265,7 +265,7 @@ trait AntiAliasing
                   val vd = ValDef(FreshIdentifier("index", true), Int32Type().copiedFrom(i)).copiedFrom(i)
                   (eBindings :+ (vd -> i), ArraySelect(eLift, vd.toVariable).copiedFrom(e))
                 case _ if effects(e).nonEmpty =>
-                  throw MissformedStainlessCode(m, "Unexpected effects in match scrutinee")
+                  throw MalformedStainlessCode(m, "Unexpected effects in match scrutinee")
                 case _ => (Seq.empty, e)
               }
 
@@ -292,7 +292,7 @@ trait AntiAliasing
               val applied = applyEffect(effect + ArrayAccessor(i), v)
               transform(Assignment(effect.receiver, applied).copiedFrom(up), env)
             } else {
-              throw MissformedStainlessCode(up, "Unsupported form of array update")
+              throw MalformedStainlessCode(up, "Unsupported form of array update")
             }
 
           case as @ FieldAssignment(o, id, v) =>
@@ -302,7 +302,7 @@ trait AntiAliasing
               val applied = applyEffect(effect + FieldAccessor(id), v)
               transform(Assignment(effect.receiver, applied).copiedFrom(as), env)
             } else {
-              throw MissformedStainlessCode(as, "Unsupported form of field assignment")
+              throw MalformedStainlessCode(as, "Unsupported form of field assignment")
             }
 
           //we need to replace local fundef by the new updated fun defs.

core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala

@@ -106,7 +106,7 @@ trait EffectsAnalyzer extends CachingPhase {
 
           val baseResult = Result(
             inners.flatMap { case (fd, inners) => inners + Outer(fd) }.map(_ -> Set.empty[Effect]).toMap,
-            inners.flatMap { case (_, inners) => inners.map(fun => fun.id -> fun) }.toMap)
+            inners.flatMap { case (_, inners) => inners.map(fun => fun.id -> fun) })
 
           val result = inox.utils.fixpoint[Result] { case res @ Result(effects, locals) =>
             Result(effects.map { case (fd, _) => fd -> functionEffects(fd, res) }, locals)
@@ -207,7 +207,7 @@ trait EffectsAnalyzer extends CachingPhase {
         case FieldAccessor(fid) +: rest =>
           rec(args(symbols.getConstructor(id).fields.indexWhere(_.id == fid)), rest)
         case _ =>
-          throw MissformedStainlessCode(expr, "Couldn't compute effect targets")
+          throw MalformedStainlessCode(expr, "Couldn't compute effect targets")
       }
       case Assert(_, _, e) => rec(e, path)
       case Annotated(e, _) => rec(e, path)
@@ -220,24 +220,24 @@ trait EffectsAnalyzer extends CachingPhase {
           Some(Effect(ee.receiver, Target(ee.target.path ++ be.target.path)))
         case (_, Some(be)) => Some(be)
         case _ =>
-          throw MissformedStainlessCode(expr, "Couldn't compute effect targets")
+          throw MalformedStainlessCode(expr, "Couldn't compute effect targets")
       }
       case _ =>
-        throw MissformedStainlessCode(expr, "Couldn't compute effect targets")
+        throw MalformedStainlessCode(expr, "Couldn't compute effect targets")
     }
 
     rec(expr, Seq())
   }
 
   def getExactEffect(expr: Expr)(implicit symbols: Symbols): Effect = getEffect(expr) match {
     case Some(effect) => effect
-    case _ => throw MissformedStainlessCode(expr, "Couldn't compute exact effect targets")
+    case _ => throw MalformedStainlessCode(expr, "Couldn't compute exact effect targets")
   }
 
   def getKnownEffect(expr: Expr)(implicit symbols: Symbols): Option[Effect] = try {
     getEffect(expr)
   } catch {
-    case _: MissformedStainlessCode => None
+    case _: MalformedStainlessCode => None
   }
 
   /** Return all effects of expr

core/src/main/scala/stainless/extraction/imperative/EffectsChecker.scala

@@ -50,7 +50,7 @@ trait EffectsChecker { self: EffectsAnalyzer =>
                 // Check if a precise effect can be computed
                 getEffect(e)
               } catch {
-                case _: MissformedStainlessCode =>
+                case _: MalformedStainlessCode =>
                   throw ImperativeEliminationException(e, "Illegal aliasing: " + e.asString)
               }
 
@@ -69,7 +69,7 @@ trait EffectsChecker { self: EffectsAnalyzer =>
             case l @ Lambda(args, body) =>
               if (isMutableType(body.getType) && !isExpressionFresh(body))
                 throw ImperativeEliminationException(l, "Illegal aliasing in lambda body")
-              if (effects(body).exists(e => !args.exists(_ == e.receiver.toVal)))
+              if (effects(body).exists(e => !args.contains(e.receiver.toVal)))
                 throw ImperativeEliminationException(l, "Illegal effects in lambda body")
               super.traverse(l)
 

core/src/main/scala/stainless/extraction/imperative/ImperativeCleanup.scala

@@ -65,16 +65,16 @@ trait ImperativeCleanup
 
   private def checkNoOld(expr: s.Expr): Unit = s.exprOps.preTraversal {
     case o @ s.Old(_) =>
-      throw MissformedStainlessCode(o, s"Stainless `old` can only occur in postconditions.")
+      throw MalformedStainlessCode(o, s"Stainless `old` can only occur in postconditions.")
     case _ => ()
   } (expr)
 
   private def checkValidOldUsage(expr: s.Expr): Unit = s.exprOps.preTraversal {
     case o @ s.Old(s.ADTSelector(v: s.Variable, id)) =>
-      throw MissformedStainlessCode(o,
+      throw MalformedStainlessCode(o,
         s"Stainless `old` can only occur on `this` and variables. Did you mean `old($v).$id`?")
     case o @ s.Old(e) =>
-      throw MissformedStainlessCode(o, s"Stainless `old` is only defined on `this` and variables.")
+      throw MalformedStainlessCode(o, s"Stainless `old` is only defined on `this` and variables.")
     case _ => ()
   } (expr)
 

core/src/main/scala/stainless/extraction/imperative/package.scala

@@ -17,7 +17,7 @@ package object imperative {
   }
 
   class ImperativeEliminationException(tree: inox.ast.Trees#Tree, msg: String)
-    extends MissformedStainlessCode(tree, msg)
+    extends MalformedStainlessCode(tree, msg)
 
   object ImperativeEliminationException {
     def apply(tree: inox.ast.Trees#Tree, msg: String) = new ImperativeEliminationException(tree, msg)