diff --git a/core/src/main/scala/stainless/Component.scala b/core/src/main/scala/stainless/Component.scala index 8beff8060b..20a73344a2 100644 --- a/core/src/main/scala/stainless/Component.scala +++ b/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] } diff --git a/core/src/main/scala/stainless/MainHelpers.scala b/core/src/main/scala/stainless/MainHelpers.scala index a231f5cf45..05d44194af 100644 --- a/core/src/main/scala/stainless/MainHelpers.scala +++ b/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) diff --git a/core/src/main/scala/stainless/ast/Deconstructors.scala b/core/src/main/scala/stainless/ast/Deconstructors.scala index df9374d1d2..07ef9e03d5 100644 --- a/core/src/main/scala/stainless/ast/Deconstructors.scala +++ b/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) diff --git a/core/src/main/scala/stainless/ast/Definitions.scala b/core/src/main/scala/stainless/ast/Definitions.scala index 8d472f57e2..815d0da43e 100644 --- a/core/src/main/scala/stainless/ast/Definitions.scala +++ b/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)) { diff --git a/core/src/main/scala/stainless/ast/Expressions.scala b/core/src/main/scala/stainless/ast/Expressions.scala index 04f20d3f7f..7af690e45c 100644 --- a/core/src/main/scala/stainless/ast/Expressions.scala +++ b/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 = { diff --git a/core/src/main/scala/stainless/ast/SymbolOps.scala b/core/src/main/scala/stainless/ast/SymbolOps.scala index d44600918d..c4b4aafde5 100644 --- a/core/src/main/scala/stainless/ast/SymbolOps.scala +++ b/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 diff --git a/core/src/main/scala/stainless/ast/Trees.scala b/core/src/main/scala/stainless/ast/Trees.scala index 9fad0b062d..75997de69a 100644 --- a/core/src/main/scala/stainless/ast/Trees.scala +++ b/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 => diff --git a/core/src/main/scala/stainless/ast/TypeOps.scala b/core/src/main/scala/stainless/ast/TypeOps.scala index 995a83fd0f..3ae99cee57 100644 --- a/core/src/main/scala/stainless/ast/TypeOps.scala +++ b/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 diff --git a/core/src/main/scala/stainless/ast/Types.scala b/core/src/main/scala/stainless/ast/Types.scala new file mode 100644 index 0000000000..909e90f450 --- /dev/null +++ b/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 + +} diff --git a/core/src/main/scala/stainless/codegen/CompilationUnit.scala b/core/src/main/scala/stainless/codegen/CompilationUnit.scala index fa034f9ed5..b1d857a439 100644 --- a/core/src/main/scala/stainless/codegen/CompilationUnit.scala +++ b/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 { diff --git a/core/src/main/scala/stainless/evaluators/EvaluatorComponent.scala b/core/src/main/scala/stainless/evaluators/EvaluatorComponent.scala index 588bda51ff..9976e536e2 100644 --- a/core/src/main/scala/stainless/evaluators/EvaluatorComponent.scala +++ b/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) diff --git a/core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala b/core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala index ce58421c3f..355897aa01 100644 --- a/core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala +++ b/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)) diff --git a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala index 834cbfce47..1f53cc9952 100644 --- a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala +++ b/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. diff --git a/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala b/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala index 784ae14e49..217f2d8810 100644 --- a/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala +++ b/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,10 +220,10 @@ 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()) @@ -231,13 +231,13 @@ trait EffectsAnalyzer extends CachingPhase { 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 diff --git a/core/src/main/scala/stainless/extraction/imperative/EffectsChecker.scala b/core/src/main/scala/stainless/extraction/imperative/EffectsChecker.scala index 0fc60cf82d..dd4f0d63ea 100644 --- a/core/src/main/scala/stainless/extraction/imperative/EffectsChecker.scala +++ b/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) diff --git a/core/src/main/scala/stainless/extraction/imperative/ImperativeCleanup.scala b/core/src/main/scala/stainless/extraction/imperative/ImperativeCleanup.scala index 02244d267b..9cd3a0e484 100644 --- a/core/src/main/scala/stainless/extraction/imperative/ImperativeCleanup.scala +++ b/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) diff --git a/core/src/main/scala/stainless/extraction/imperative/package.scala b/core/src/main/scala/stainless/extraction/imperative/package.scala index b4b0018a5b..ee7104e354 100644 --- a/core/src/main/scala/stainless/extraction/imperative/package.scala +++ b/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) diff --git a/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala b/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala index c483755c74..42db4769cf 100644 --- a/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala +++ b/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala @@ -107,15 +107,15 @@ trait FunctionInlining extends CachingPhase with IdentitySorts { self => val hasInlineOnceFlag = fd.flags contains InlineOnce if (hasInlineFlag && hasInlineOnceFlag) { - throw MissformedStainlessCode(fd, "Can't annotate a function with both @inline and @inlineOnce") + throw MalformedStainlessCode(fd, "Can't annotate a function with both @inline and @inlineOnce") } if (hasInlineFlag && context.transitivelyCalls(fd, fd)) { - throw MissformedStainlessCode(fd, "Can't inline recursive function, use @inlineOnce instead") + throw MalformedStainlessCode(fd, "Can't inline recursive function, use @inlineOnce instead") } if (hasInlineFlag && exprOps.withoutSpecs(fd.fullBody).isEmpty) { - throw MissformedStainlessCode(fd, "Inlining function with empty body: not supported, use @inlineOnce instead") + throw MalformedStainlessCode(fd, "Inlining function with empty body: not supported, use @inlineOnce instead") } } diff --git a/core/src/main/scala/stainless/extraction/methods/Laws.scala b/core/src/main/scala/stainless/extraction/methods/Laws.scala index 91ddcc52cb..38a3a57e13 100644 --- a/core/src/main/scala/stainless/extraction/methods/Laws.scala +++ b/core/src/main/scala/stainless/extraction/methods/Laws.scala @@ -56,7 +56,7 @@ trait Laws args map (transform(_, env)) ).copiedFrom(e) } else { - throw MissformedStainlessCode(e, "Cannot refer to super-type law outside of proof body") + throw MalformedStainlessCode(e, "Cannot refer to super-type law outside of proof body") } case _ => super.transform(e, env) @@ -97,23 +97,23 @@ trait Laws if (fd.flags contains s.Law) { // Some sanity checks if (!fd.flags.exists { case s.IsMethodOf(_) => true case _ => false }) - throw MissformedStainlessCode(fd, "Unexpected non-method law") + throw MalformedStainlessCode(fd, "Unexpected non-method law") val cid = fd.flags.collectFirst { case s.IsMethodOf(id) => id }.get val cd = symbols.getClass(cid) if (!(cd.flags contains s.IsAbstract)) - throw MissformedStainlessCode(fd, "Unexpected law in non-abstract class") + throw MalformedStainlessCode(fd, "Unexpected law in non-abstract class") if (!symbols.isSubtypeOf(fd.returnType, s.BooleanType())) - throw MissformedStainlessCode(fd, "Unexpected non-boolean typed law") + throw MalformedStainlessCode(fd, "Unexpected non-boolean typed law") if (!s.exprOps.withoutSpecs(fd.fullBody).isDefined) - throw MissformedStainlessCode(fd, "Unexpected law without a body") + throw MalformedStainlessCode(fd, "Unexpected law without a body") if (symbols.isRecursive(fd.id)) - throw MissformedStainlessCode(fd, "Unexpected recursive law") + throw MalformedStainlessCode(fd, "Unexpected recursive law") if (symbols.firstSuper(fd.id.unsafeToSymbolIdentifier).exists { sid => val sfd = symbols.getFunction(sid) !sfd.isAbstract && !sfd.isLaw - }) throw MissformedStainlessCode(fd, "Unexpected law overriding concrete function") + }) throw MalformedStainlessCode(fd, "Unexpected law overriding concrete function") val env = Some(fd.id.unsafeToSymbolIdentifier.symbol) val ct = t.ClassType(cid, cd.typeArgs.map(transform(_, env))).setPos(fd) diff --git a/core/src/main/scala/stainless/extraction/methods/MethodLifting.scala b/core/src/main/scala/stainless/extraction/methods/MethodLifting.scala index 0da88b4090..f3f5c0e5ab 100644 --- a/core/src/main/scala/stainless/extraction/methods/MethodLifting.scala +++ b/core/src/main/scala/stainless/extraction/methods/MethodLifting.scala @@ -118,7 +118,7 @@ trait MethodLifting extends oo.ExtractionContext with oo.ExtractionCaches { self funCache.cached(fd, symbols)(default.transform(fd)) } - t.NoSymbols.withFunctions(functions.toSeq).withClasses(classes.toSeq) + t.NoSymbols.withFunctions(functions).withClasses(classes) } private[this] type Metadata = (Option[s.FunDef], Map[Identifier, Override]) @@ -205,7 +205,7 @@ trait MethodLifting extends oo.ExtractionContext with oo.ExtractionCaches { self def firstOverrides(fo: Override): Seq[(Identifier, FunDef)] = fo match { case Override(cid, Some(id), _) => Seq(cid -> symbols.getFunction(id)) - case Override(_, _, children) => children.toSeq.flatMap(firstOverrides) + case Override(_, _, children) => children.flatMap(firstOverrides) } val subCalls = (for (co <- cos) yield { diff --git a/core/src/main/scala/stainless/extraction/methods/Trees.scala b/core/src/main/scala/stainless/extraction/methods/Trees.scala index 1d286bf9db..2303009679 100644 --- a/core/src/main/scala/stainless/extraction/methods/Trees.scala +++ b/core/src/main/scala/stainless/extraction/methods/Trees.scala @@ -161,7 +161,7 @@ trait Trees extends throwing.Trees { self => fd.flags exists { case IsField(_) => true case _ => false } def isSetter: Boolean = isAccessor && fd.id.name.endsWith("_=") && fd.params.size == 1 - def isGetter: Boolean = isAccessor && fd.params.size == 0 + def isGetter: Boolean = isAccessor && fd.params.isEmpty def isFinal: Boolean = fd.flags contains Final def isAbstract: Boolean = fd.flags contains IsAbstract diff --git a/core/src/main/scala/stainless/extraction/methods/package.scala b/core/src/main/scala/stainless/extraction/methods/package.scala index 8860d7ed1d..16fb5469b4 100644 --- a/core/src/main/scala/stainless/extraction/methods/package.scala +++ b/core/src/main/scala/stainless/extraction/methods/package.scala @@ -18,7 +18,7 @@ package object methods { } class MethodsException(tree: inox.ast.Trees#Tree, msg: String) - extends MissformedStainlessCode(tree, msg) + extends MalformedStainlessCode(tree, msg) object MethodsException { def apply(tree: inox.ast.Trees#Tree, msg: String) = new MethodsException(tree, msg) diff --git a/core/src/main/scala/stainless/extraction/oo/AdtSpecialization.scala b/core/src/main/scala/stainless/extraction/oo/AdtSpecialization.scala index 88bc62e6eb..f58713c1c6 100644 --- a/core/src/main/scala/stainless/extraction/oo/AdtSpecialization.scala +++ b/core/src/main/scala/stainless/extraction/oo/AdtSpecialization.scala @@ -199,7 +199,7 @@ trait AdtSpecialization val cons = constructors(cd.id) val unapplyFunction = if (root(cd.id) != cd.id && cons != Seq(cd.id)) { Some(mkFunDef(unapplyID(cd.id), t.Unchecked, t.Synthetic, t.IsUnapply(isEmpty, get)) - (cd.typeArgs.map(_.id.name) : _*) { case tparams => + (cd.typeArgs.map(_.id.name) : _*) { tparams => val base = T(root(cd.id))(tparams : _*) def condition(e: t.Expr): t.Expr = t.orJoin(cons.map(t.IsConstructor(e, _))) diff --git a/core/src/main/scala/stainless/extraction/oo/RefinementLifting.scala b/core/src/main/scala/stainless/extraction/oo/RefinementLifting.scala index 111f7fc377..95ef9d025f 100644 --- a/core/src/main/scala/stainless/extraction/oo/RefinementLifting.scala +++ b/core/src/main/scala/stainless/extraction/oo/RefinementLifting.scala @@ -215,7 +215,7 @@ trait RefinementLifting case None => import s.dsl._ mkFunDef(FreshIdentifier("inv"))(sort.typeArgs.map(_.id.name) : _*) { - case tparams => ( + tparams => ( Seq("thiss" :: s.ADTType(sort.id, tparams).copiedFrom(sort)), s.BooleanType().copiedFrom(sort), { case Seq(thiss) => s.typeOps.instantiateType( diff --git a/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala b/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala index 1d72a2bffe..0ad109ac76 100644 --- a/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala +++ b/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala @@ -4,9 +4,6 @@ package stainless package extraction package oo -import inox.utils.Graphs._ -import java.util.concurrent.atomic.AtomicReference - trait TypeEncoding extends ExtractionPipeline with SimpleSorts diff --git a/core/src/main/scala/stainless/extraction/package.scala b/core/src/main/scala/stainless/extraction/package.scala index 93796d603c..35fa3963bf 100644 --- a/core/src/main/scala/stainless/extraction/package.scala +++ b/core/src/main/scala/stainless/extraction/package.scala @@ -82,7 +82,7 @@ package object extraction { object printer extends Printer { val trees: extraction.trees.type = extraction.trees } } - case class MissformedStainlessCode(tree: inox.ast.Trees#Tree, msg: String) + case class MalformedStainlessCode(tree: inox.ast.Trees#Tree, msg: String) extends Exception(msg) def pipeline(implicit ctx: inox.Context): StainlessPipeline = { diff --git a/core/src/main/scala/stainless/extraction/xlang/TreeSanitizer.scala b/core/src/main/scala/stainless/extraction/xlang/TreeSanitizer.scala index 9de16352de..833929eb15 100644 --- a/core/src/main/scala/stainless/extraction/xlang/TreeSanitizer.scala +++ b/core/src/main/scala/stainless/extraction/xlang/TreeSanitizer.scala @@ -10,7 +10,7 @@ trait TreeSanitizer { val trees: xlang.Trees import trees._ - /** Throw a [[MissformedStainlessCode]] exception when detecting an illegal pattern. */ + /** Throw a [[MalformedStainlessCode]] exception when detecting an illegal pattern. */ def check(symbols: Symbols)(implicit ctx: inox.Context): Unit = { val preconditions = new CheckPreconditions()(symbols, ctx) symbols.functions.values foreach preconditions.traverse @@ -25,14 +25,14 @@ trait TreeSanitizer { if !symbols.getFunction(id).isSetter sid <- symbols.firstSuper(id) if symbols.getFunction(sid).isSetter - } throw MissformedStainlessCode(symbols.getFunction(id), + } throw MalformedStainlessCode(symbols.getFunction(id), "Cannot override a `var` accessor with a non-accessor method.") // check that sealed traits have children for { cd <- symbols.classes.values if cd.isAbstract && cd.isSealed && cd.children(symbols).isEmpty - } throw MissformedStainlessCode(cd, "Illegal sealed abstract class with no children.") + } throw MalformedStainlessCode(cd, "Illegal sealed abstract class with no children.") } /* This detects both multiple `require` and `require` after `decreases`. */ @@ -58,10 +58,10 @@ trait TreeSanitizer { optInv.foreach(traverse) case e: Require => - throw MissformedStainlessCode(e, s"Unexpected `require`.") + throw MalformedStainlessCode(e, s"Unexpected `require`.") case e: Decreases => - throw MissformedStainlessCode(e, s"Unexpected `decreases`.") + throw MalformedStainlessCode(e, s"Unexpected `decreases`.") case e: LetRec => // Traverse LocalFunDef independently @@ -101,9 +101,9 @@ trait TreeSanitizer { val ct = obj.getType.asInstanceOf[ClassType] ct.getField(selector) match { case None => - throw MissformedStainlessCode(e, s"Cannot find field `${selector.asString}` of class ${ct.asString}.") + throw MalformedStainlessCode(e, s"Cannot find field `${selector.asString}` of class ${ct.asString}.") case Some(field) if field.flags contains Ignore => - throw MissformedStainlessCode(e, s"Cannot access ignored field `${selector.asString}` from non-extern context.") + throw MalformedStainlessCode(e, s"Cannot access ignored field `${selector.asString}` from non-extern context.") case _ => super.traverse(e) } @@ -114,9 +114,9 @@ trait TreeSanitizer { val ct = rec.getType.asInstanceOf[ClassType] ct.getField(id) match { case Some(field) if field.flags contains Ignore => - throw MissformedStainlessCode(e, s"Cannot access ignored field `${id.asString}` from non-extern context.") + throw MalformedStainlessCode(e, s"Cannot access ignored field `${id.asString}` from non-extern context.") case None if symbols.lookupFunction(id).exists(_.flags contains Ignore) => - throw MissformedStainlessCode(e, s"Cannot access ignored field `${id.asString}` from non-extern context.") + throw MalformedStainlessCode(e, s"Cannot access ignored field `${id.asString}` from non-extern context.") case _ => super.traverse(e) } @@ -127,11 +127,11 @@ trait TreeSanitizer { case ClassConstructor(ct, args) => ct.lookupClass match { case None => - throw MissformedStainlessCode(e, s"Cannot find class for type `${ct.asString}`.") + throw MalformedStainlessCode(e, s"Cannot find class for type `${ct.asString}`.") case Some(tcd) if tcd.fields.exists(_.flags contains Ignore) => val ignoredFields = tcd.fields.filter(_.flags contains Ignore).map(_.id.asString).mkString(", ") - throw MissformedStainlessCode(e, + throw MalformedStainlessCode(e, s"Cannot build an instance of a class with ignored fields in non-extern context " + s"(${ct.asString} has ignored fields: $ignoredFields)." ) diff --git a/core/src/main/scala/stainless/frontend/BatchedCallBack.scala b/core/src/main/scala/stainless/frontend/BatchedCallBack.scala new file mode 100644 index 0000000000..465522731f --- /dev/null +++ b/core/src/main/scala/stainless/frontend/BatchedCallBack.scala @@ -0,0 +1,47 @@ +/* Copyright 2009-2018 EPFL, Lausanne */ + +package stainless +package frontend + +import stainless.extraction.xlang.{trees => xt} + +import scala.concurrent.Await +import scala.concurrent.duration._ + +class BatchedCallBack(components: Seq[Component])(implicit val context: inox.Context) extends CallBack with StainlessReports { + private var currentClasses = Seq[xt.ClassDef]() + private var currentFunctions = Seq[xt.FunDef]() + + private var report: AbstractReport[Report] = _ + + protected val pipeline: extraction.StainlessPipeline = extraction.pipeline + private[this] val runs = components.map(_.run(pipeline)) + + def beginExtractions(): Unit = {} + + def apply(file: String, unit: xt.UnitDef, classes: Seq[xt.ClassDef], functions: Seq[xt.FunDef]): Unit = { + synchronized { + currentFunctions ++= functions + currentClasses ++= classes + } + } + + def failed(): Unit = {} + + def endExtractions(): Unit = { + val symbols = xt.NoSymbols.withClasses(currentClasses).withFunctions(currentFunctions) + val reports = runs.map { run => + RunReport(run)(Await.result(run(symbols.functions.keys.toSeq, symbols, filterSymbols = true), Duration.Inf).toReport) + } + report = Report(reports) + } + + def stop(): Unit = { + currentClasses = Seq() + currentFunctions = Seq() + } + + def join(): Unit = {} + + def getReport = Option(report) +} diff --git a/core/src/main/scala/stainless/frontend/StainlessCallBack.scala b/core/src/main/scala/stainless/frontend/StainlessCallBack.scala index 26aaa82bb2..c9c5671f47 100644 --- a/core/src/main/scala/stainless/frontend/StainlessCallBack.scala +++ b/core/src/main/scala/stainless/frontend/StainlessCallBack.scala @@ -6,9 +6,9 @@ package frontend import scala.language.existentials import extraction.xlang.{ TreeSanitizer, trees => xt } -import utils.{ CheckFilter, DependenciesFinder, JsonUtils, Registry } +import utils.{ CheckFilter, XLangDependenciesFinder, JsonUtils, Registry } -import scala.collection.mutable.{ ListBuffer, Map => MutableMap, Set => MutableSet } +import scala.collection.mutable.{ ListBuffer, Set => MutableSet } import io.circe._ import io.circe.syntax._ @@ -18,12 +18,12 @@ import scala.concurrent.{ Await, Future } import scala.concurrent.duration._ class StainlessCallBack(components: Seq[Component])(override implicit val context: inox.Context) - extends CallBack with CheckFilter { self => + extends CallBack with CheckFilter with StainlessReports { self => protected final override val trees = extraction.xlang.trees protected val pipeline: extraction.StainlessPipeline = extraction.pipeline - import context.{ options, reporter } + import context.reporter private[this] val runs = components.map(_.run(pipeline)) @@ -98,38 +98,6 @@ class StainlessCallBack(components: Seq[Component])(override implicit val contex } } - protected trait RunReport { val run: ComponentRun; val report: run.component.Report } - protected def RunReport(r: ComponentRun)(re: r.component.Report): RunReport { val run: r.type; val report: re.type } = - new RunReport { val run: r.type = r; val report: re.type = re } - - protected case class Report(reports: Seq[RunReport]) extends AbstractReport[Report] { - val name = "stainless" - - override def ~(other: Report): Report = Report( - (reports ++ other.reports).groupBy(_.run).map { - case (run, reports) => RunReport(run)(reports.map(_.report.asInstanceOf[run.component.Report]) reduce (_ ~ _)) - }.toSeq - ) - - override lazy val annotatedRows = reports.flatMap(_.report.annotatedRows: Seq[RecordRow]) - - override def emitJson = reports.map(rr => rr.run.component.name -> rr.report.emitJson).asJson - - override def filter(ids: Set[Identifier]): Report = - Report(reports.map(rr => RunReport(rr.run)(rr.report filter ids))) - - override lazy val stats: stainless.ReportStats = { - val reportStats = reports.map(_.report.stats) - ReportStats( - reportStats.map(_.total ).sum, - reportStats.map(_.time ).sum, - reportStats.map(_.valid ).sum, - reportStats.map(_.validFromCache).sum, - reportStats.map(_.invalid ).sum, - reportStats.map(_.unknown ).sum) - } - } - /** Parse a JSON value into a proper Report. We assume this doesn't fail. */ protected def parseReportCache(json: Json): Report = json.as[Seq[(String, Json)]] match { case Right(jsons) => Report(runs.flatMap { run => @@ -157,8 +125,8 @@ class StainlessCallBack(components: Seq[Component])(override implicit val contex private val registry = new Registry { override val context = self.context - override def computeDirectDependencies(fd: xt.FunDef): Set[Identifier] = new DependenciesFinder()(fd) - override def computeDirectDependencies(cd: xt.ClassDef): Set[Identifier] = new DependenciesFinder()(cd) + override def computeDirectDependencies(fd: xt.FunDef): Set[Identifier] = new XLangDependenciesFinder()(fd) + override def computeDirectDependencies(cd: xt.ClassDef): Set[Identifier] = new XLangDependenciesFinder()(cd) override def shouldBeChecked(fd: xt.FunDef): Boolean = self.shouldBeChecked(fd) } @@ -229,7 +197,7 @@ class StainlessCallBack(components: Seq[Component])(override implicit val contex try { TreeSanitizer(xt).check(funSyms) } catch { - case e: extraction.MissformedStainlessCode => + case e: extraction.MalformedStainlessCode => reportError(e.tree.getPos, e.getMessage, funSyms) } diff --git a/core/src/main/scala/stainless/frontend/StainlessReports.scala b/core/src/main/scala/stainless/frontend/StainlessReports.scala new file mode 100644 index 0000000000..16ccf71667 --- /dev/null +++ b/core/src/main/scala/stainless/frontend/StainlessReports.scala @@ -0,0 +1,42 @@ +/* Copyright 2009-2018 EPFL, Lausanne */ + +package stainless +package frontend + +import io.circe._ +import io.circe.syntax._ + +trait StainlessReports { + protected trait RunReport { val run: ComponentRun; val report: run.component.Report } + protected def RunReport(r: ComponentRun)(re: r.component.Report): RunReport { val run: r.type; val report: re.type } = + new RunReport { val run: r.type = r; val report: re.type = re } + + protected case class Report(reports: Seq[RunReport]) extends AbstractReport[Report] { + val name = "stainless" + + override def ~(other: Report): Report = Report( + (reports ++ other.reports).groupBy(_.run).map { + case (run, reports) => RunReport(run)(reports.map(_.report.asInstanceOf[run.component.Report]) reduce (_ ~ _)) + }.toSeq + ) + + override lazy val annotatedRows = reports.flatMap(_.report.annotatedRows: Seq[RecordRow]) + + override def emitJson = reports.map(rr => rr.run.component.name -> rr.report.emitJson).asJson + + override def filter(ids: Set[Identifier]): Report = + Report(reports.map(rr => RunReport(rr.run)(rr.report filter ids))) + + override lazy val stats: stainless.ReportStats = { + val reportStats = reports.map(_.report.stats) + ReportStats( + reportStats.map(_.total ).sum, + reportStats.map(_.time ).sum, + reportStats.map(_.valid ).sum, + reportStats.map(_.validFromCache).sum, + reportStats.map(_.invalid ).sum, + reportStats.map(_.unknown ).sum) + } + } + +} \ No newline at end of file diff --git a/core/src/main/scala/stainless/frontend/package.scala b/core/src/main/scala/stainless/frontend/package.scala index 670a206ed2..18dd675cab 100644 --- a/core/src/main/scala/stainless/frontend/package.scala +++ b/core/src/main/scala/stainless/frontend/package.scala @@ -5,7 +5,7 @@ package stainless package object frontend { /** An exception thrown when non-purescala compatible code is encountered. */ - sealed case class UnsupportedCodeException(val pos: inox.utils.Position, msg: String) + sealed case class UnsupportedCodeException(pos: inox.utils.Position, msg: String) extends Exception(msg) object DebugSectionExtraction extends inox.DebugSection("extraction") @@ -17,6 +17,11 @@ package object frontend { */ object optPersistentCache extends inox.FlagOptionDef("cache", false) + /** Do not use registry to create minimal partial programs, + * do a dependency analysis after collecting the whole program + */ + object optBatchedProgram extends inox.FlagOptionDef("batched", false) + /** * Given a context (with its reporter) and a frontend factory, proceed to compile, * extract, transform and verify the input programs based on the active components @@ -27,7 +32,7 @@ package object frontend { * is required to [[stop]] or [[join]] the returned compiler to free resources. */ def build(ctx: inox.Context, compilerArgs: Seq[String], factory: FrontendFactory): Frontend = { - factory(ctx, compilerArgs, getStainlessCallBack(ctx)) + factory(ctx, compilerArgs, getCallBack(ctx)) } /** @@ -38,7 +43,8 @@ package object frontend { val allComponents: Seq[Component] = Seq( verification.VerificationComponent, termination.TerminationComponent, - evaluators.EvaluatorComponent + evaluators.EvaluatorComponent, + wasmgen.WasmComponent ) /** @@ -60,9 +66,12 @@ package object frontend { } /** Get one callback for all active components. */ - def getStainlessCallBack(implicit ctx: inox.Context): CallBack = { + def getCallBack(implicit ctx: inox.Context): CallBack = { val activeComponents = getActiveComponents(ctx) - new StainlessCallBack(activeComponents) + if(ctx.options.findOptionOrDefault(optBatchedProgram)) + new BatchedCallBack(activeComponents) + else + new StainlessCallBack(activeComponents) } } diff --git a/core/src/main/scala/stainless/package.scala b/core/src/main/scala/stainless/package.scala index 128e5c9c67..72cb025218 100644 --- a/core/src/main/scala/stainless/package.scala +++ b/core/src/main/scala/stainless/package.scala @@ -1,7 +1,7 @@ /* Copyright 2009-2018 EPFL, Lausanne */ import scala.collection.parallel.ForkJoinTasks -import scala.concurrent.{ ExecutionContext, Future } +import scala.concurrent.ExecutionContext import java.util.concurrent.Executors import inox.transformers._ diff --git a/core/src/main/scala/stainless/solvers/InoxEncoder.scala b/core/src/main/scala/stainless/solvers/InoxEncoder.scala index 6157e97273..dde20f64d8 100644 --- a/core/src/main/scala/stainless/solvers/InoxEncoder.scala +++ b/core/src/main/scala/stainless/solvers/InoxEncoder.scala @@ -194,7 +194,7 @@ trait InoxEncoder extends ProgramEncoder { Seq(s.FiniteMap(elems, dflt, _, _), s.Int32Literal(size)) ) if size <= 10 => val elemsMap = elems.toMap - t.FiniteArray((0 until size).toSeq.map { + t.FiniteArray((0 until size).map { i => transform(elemsMap.getOrElse(s.Int32Literal(i).copiedFrom(e), dflt)) }, transform(base)).copiedFrom(e) diff --git a/core/src/main/scala/stainless/termination/ControlFlowAnalysis.scala b/core/src/main/scala/stainless/termination/ControlFlowAnalysis.scala index e6ac831763..01ee91b171 100644 --- a/core/src/main/scala/stainless/termination/ControlFlowAnalysis.scala +++ b/core/src/main/scala/stainless/termination/ControlFlowAnalysis.scala @@ -150,11 +150,11 @@ trait CICFA { } private def passedLambdas(vals: Set[AbsValue], env: AbsEnv): Set[Lambda] = vals.flatMap { - case Closure(lam) => variablesOf(lam).flatMap { v => passedLambdas(env.store(v), env) }.toSet + lam + case Closure(lam) => variablesOf(lam).flatMap { v => passedLambdas(env.store(v), env) } + lam case _ => Set[Lambda]() } - private def freshVars(size: Int) = (1 to size).map(i => Variable.fresh("arg" + i, Untyped, true)).toSeq + private def freshVars(size: Int) = (1 to size).map(i => Variable.fresh("arg" + i, Untyped, true)) // iteratively process functions from the worklist. // (a) at every direct function call, join the arguments passed in with the `in` fact in the summary diff --git a/core/src/main/scala/stainless/termination/StructuralSize.scala b/core/src/main/scala/stainless/termination/StructuralSize.scala index c3a12dbb21..e83a78e4ae 100644 --- a/core/src/main/scala/stainless/termination/StructuralSize.scala +++ b/core/src/main/scala/stainless/termination/StructuralSize.scala @@ -18,7 +18,7 @@ trait StructuralSize { self: SolverProvider => val s: trees.type = trees val t: trees.type = trees - def transform(s: Symbols): Symbols = s.withFunctions(functions.toSeq) + def transform(s: Symbols): Symbols = s.withFunctions(functions) }) /* Absolute value for BigInt type diff --git a/core/src/main/scala/stainless/termination/TerminationComponent.scala b/core/src/main/scala/stainless/termination/TerminationComponent.scala index de65c48458..5855f10eec 100644 --- a/core/src/main/scala/stainless/termination/TerminationComponent.scala +++ b/core/src/main/scala/stainless/termination/TerminationComponent.scala @@ -63,7 +63,7 @@ class TerminationRun(override val pipeline: extraction.StainlessPipeline) override def parse(json: Json): Report = TerminationReport.parse(json) - override def apply(functions: Seq[Identifier], symbols: trees.Symbols): Future[Analysis] = { + private[stainless] def execute(functions: Seq[Identifier], symbols: trees.Symbols): Future[Analysis] = { import trees._ import context._ diff --git a/core/src/main/scala/stainless/transformers/PartialEvaluator.scala b/core/src/main/scala/stainless/transformers/PartialEvaluator.scala index 9cea2dfac4..b25510cd68 100644 --- a/core/src/main/scala/stainless/transformers/PartialEvaluator.scala +++ b/core/src/main/scala/stainless/transformers/PartialEvaluator.scala @@ -4,20 +4,11 @@ package stainless package transformers import scala.language.existentials -import scala.concurrent.duration._ -import scala.collection.mutable.{Map => MutableMap} - -import inox.{Context, Semantics} -import inox.utils._ -import inox.solvers._ -import inox.solvers.SolverResponses._ -import inox.evaluators.EvaluationResults trait PartialEvaluator extends SimplifierWithPC { self => import trees._ - import symbols.{simplifier => _, _} + import symbols._ import exprOps._ - import dsl._ override protected def simplify(e: Expr, path: Env): (Expr, Boolean) = e match { case fi @ FunctionInvocation(id, tps, args) => diff --git a/core/src/main/scala/stainless/utils/DependenciesFinder.scala b/core/src/main/scala/stainless/utils/DependenciesFinder.scala index 180f4f5682..aa52ef4ead 100644 --- a/core/src/main/scala/stainless/utils/DependenciesFinder.scala +++ b/core/src/main/scala/stainless/utils/DependenciesFinder.scala @@ -1,80 +1,57 @@ -/* Copyright 2009-2018 EPFL, Lausanne */ - package stainless package utils -import extraction.xlang.{ trees => xt } - -import scala.collection.mutable.{ Set => MutableSet } - -/** - * [[DependenciesFinder]] find the set of dependencies for a function/class, - * it is not thread safe and is designed for one and only one run! - * - * It returns only the *direct* dependencies, without the argument itself - * although it could be a recursive function. Moreover, it doesn't capture - * the notion of class hierarchy as it doesn't know about other classes. - * - * It also does **not** handle dependencies toward class invariant/methods - * because this requires the knowledge of existing functions in addition to - * the class itself. - */ -class DependenciesFinder { - private val deps: MutableSet[Identifier] = MutableSet.empty - private val finder = new xt.SelfTreeTraverser { - override def traverse(e: xt.Expr): Unit = e match { - case xt.FunctionInvocation(id, _, _) => - deps += id - super.traverse(e) - - case xt.MethodInvocation(_, id, _, _) => - deps += id - super.traverse(e) - - case _ => super.traverse(e) - } - - override def traverse(pat: xt.Pattern): Unit = pat match { - case xt.UnapplyPattern(_, _, id, _, _) => - deps += id - super.traverse(pat) - - case _ => super.traverse(pat) +trait DefinitionIdFinder extends transformers.DefinitionTraverser { + val s: trees.Symbols + private val idsMap = { + s.functions.keys.map(id => id -> id) ++ + s.sorts.values.flatMap { s => + s.constructors.map(c => c.id -> s.id) ++ Seq(s.id -> s.id) } + }.toMap - override def traverse(tpe: xt.Type): Unit = tpe match { - case xt.ClassType(id, _) => - deps += id - super.traverse(tpe) + def initEnv = () + type Env = Unit - case _ => super.traverse(tpe) - } - - override def traverse(flag: xt.Flag): Unit = flag match { - case xt.IsMethodOf(id) => - deps += id - super.traverse(flag) - - case _ => super.traverse(flag) - } + protected var ids: Set[Identifier] = Set() + override def traverse(id: Identifier, env: Env): Unit = { + ids ++= idsMap.get(id) } - def apply(fd: xt.FunDef): Set[Identifier] = { - finder.traverse(fd) - deps -= fd.id + def doTraverse(fd: trees.FunDef): Set[Identifier] = { + ids = Set() + traverse(fd) + ids + } - deps.toSet + def doTraverse(sort: trees.ADTSort): Set[Identifier] = { + ids = Set() + traverse(sort) + ids } +} - def apply(cd: xt.ClassDef): Set[Identifier] = { - cd.tparams foreach finder.traverse - cd.parents foreach finder.traverse - cd.fields foreach finder.traverse - cd.flags foreach finder.traverse - deps -= cd.id +trait DependenciesFinder { + val t: stainless.ast.Trees + protected def traverser(s: t.Symbols): DefinitionIdFinder { val trees: t.type } + + def findDependencies(roots: Set[Identifier], s: t.Symbols): t.Symbols = { + val tr = traverser(s) + var found = Set[Identifier]() + var toExplore = roots + + while(toExplore.nonEmpty) { + val fIds = s.functions.values.view.force.filter(f => toExplore(f.id)) + .flatMap((fd: t.FunDef) => tr.doTraverse(fd)).toSet + val sIds = s.sorts.values.view.force.filter(s => toExplore(s.id)) + .flatMap((s: t.ADTSort) => tr.doTraverse(s)).toSet + found ++= toExplore + toExplore = (fIds ++ sIds) -- found + } - deps.toSet + t.NoSymbols + .withFunctions(s.functions.values.toSeq.filter(f => found(f.id))) + .withSorts(s.sorts.values.toSeq.filter(f => found(f.id))) } } - diff --git a/core/src/main/scala/stainless/utils/XLangDependenciesFinder.scala b/core/src/main/scala/stainless/utils/XLangDependenciesFinder.scala new file mode 100644 index 0000000000..1ef1fb5b87 --- /dev/null +++ b/core/src/main/scala/stainless/utils/XLangDependenciesFinder.scala @@ -0,0 +1,80 @@ +/* Copyright 2009-2018 EPFL, Lausanne */ + +package stainless +package utils + +import extraction.xlang.{ trees => xt } + +import scala.collection.mutable.{ Set => MutableSet } + +/** + * [[XLangDependenciesFinder]] find the set of dependencies for a function/class, + * it is not thread safe and is designed for one and only one run! + * + * It returns only the *direct* dependencies, without the argument itself + * although it could be a recursive function. Moreover, it doesn't capture + * the notion of class hierarchy as it doesn't know about other classes. + * + * It also does **not** handle dependencies toward class invariant/methods + * because this requires the knowledge of existing functions in addition to + * the class itself. + */ +class XLangDependenciesFinder { + private val deps: MutableSet[Identifier] = MutableSet.empty + private val finder = new xt.SelfTreeTraverser { + override def traverse(e: xt.Expr): Unit = e match { + case xt.FunctionInvocation(id, _, _) => + deps += id + super.traverse(e) + + case xt.MethodInvocation(_, id, _, _) => + deps += id + super.traverse(e) + + case _ => super.traverse(e) + } + + override def traverse(pat: xt.Pattern): Unit = pat match { + case xt.UnapplyPattern(_, _, id, _, _) => + deps += id + super.traverse(pat) + + case _ => super.traverse(pat) + } + + override def traverse(tpe: xt.Type): Unit = tpe match { + case xt.ClassType(id, _) => + deps += id + super.traverse(tpe) + + case _ => super.traverse(tpe) + } + + override def traverse(flag: xt.Flag): Unit = flag match { + case xt.IsMethodOf(id) => + deps += id + super.traverse(flag) + + case _ => super.traverse(flag) + } + } + + def apply(fd: xt.FunDef): Set[Identifier] = { + finder.traverse(fd) + deps -= fd.id + + deps.toSet + } + + def apply(cd: xt.ClassDef): Set[Identifier] = { + cd.tparams foreach finder.traverse + cd.parents foreach finder.traverse + cd.fields foreach finder.traverse + cd.flags foreach finder.traverse + deps -= cd.id + + deps.toSet + } +} + + diff --git a/core/src/main/scala/stainless/verification/DefaultTactic.scala b/core/src/main/scala/stainless/verification/DefaultTactic.scala index ee2968c29e..3c4e5a3396 100644 --- a/core/src/main/scala/stainless/verification/DefaultTactic.scala +++ b/core/src/main/scala/stainless/verification/DefaultTactic.scala @@ -51,7 +51,7 @@ trait DefaultTactic extends Tactic { def generatePostconditions(id: Identifier): Seq[VC] = { val fd = getFunction(id) (fd.postcondition, fd.body) match { - case (Some(post @ Lambda(Seq(res), _)), Some(body)) if !res.flags.exists(_ == Unchecked) => + case (Some(post @ Lambda(Seq(res), _)), Some(body)) if !res.flags.contains(Unchecked) => getPostconditions(body, post).map { vc => val vcKind = if (fd.flags.exists(_.name == "law")) VCKind.Law else VCKind.Postcondition VC(exprOps.freshenLocals(implies(fd.precOrTrue, vc)), id, vcKind, false).setPos(fd) diff --git a/core/src/main/scala/stainless/verification/VerificationComponent.scala b/core/src/main/scala/stainless/verification/VerificationComponent.scala index 154815f6b9..19c5f3e30b 100644 --- a/core/src/main/scala/stainless/verification/VerificationComponent.scala +++ b/core/src/main/scala/stainless/verification/VerificationComponent.scala @@ -49,7 +49,7 @@ class VerificationRun(override val pipeline: StainlessPipeline) implicit val debugSection = DebugSectionVerification - override def apply(functions: Seq[Identifier], symbols: trees.Symbols): Future[VerificationAnalysis] = { + private[stainless] def execute(functions: Seq[Identifier], symbols: trees.Symbols): Future[VerificationAnalysis] = { import context._ val p = inox.Program(trees)(symbols) diff --git a/core/src/main/scala/stainless/wasmgen/LibProvider.scala b/core/src/main/scala/stainless/wasmgen/LibProvider.scala new file mode 100644 index 0000000000..ab4af2d9d4 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/LibProvider.scala @@ -0,0 +1,19 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen + +trait LibProvider { + import LibProvider.libPath + + protected val trees: stainless.ast.Trees + + def fun(name: String)(implicit s: trees.Symbols): trees.FunDef = + s.lookup[trees.FunDef](libPath + name) + + def sort(name: String)(implicit s: trees.Symbols): trees.ADTSort = + s.lookup[trees.ADTSort](libPath + name) +} + +object LibProvider { + val libPath = "stainless.wasm.Runtime." +} diff --git a/core/src/main/scala/stainless/wasmgen/WasmComponent.scala b/core/src/main/scala/stainless/wasmgen/WasmComponent.scala new file mode 100644 index 0000000000..24aebfab5e --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/WasmComponent.scala @@ -0,0 +1,68 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless +package wasmgen + +import inox.Context +import inox.transformers.SymbolTransformer +import extraction.StainlessPipeline +import utils.{CheckFilter, DependenciesFinder} + +import scala.concurrent.Future + +object DebugSectionWasm extends inox.DebugSection("wasm") + +class WasmAnalysis extends AbstractAnalysis { + val name = "no analysis" + type Report = NoReport + + def toReport = new NoReport +} + +class WasmFilter(val context: Context) extends CheckFilter { + val trees: stainless.trees.type = stainless.trees + + override def shouldBeChecked(fd: trees.FunDef): Boolean = { + fd.params.isEmpty && super.shouldBeChecked(fd) + } +} + +object WasmComponent extends Component { + val name = "wasm-codegen" + val description = "Generate WebAssembly code that runs parameterless functions in the program" + type Report = NoReport + type Analysis = WasmAnalysis + + override val lowering: SymbolTransformer { + val s: extraction.trees.type + val t: extraction.trees.type + } = inox.transformers.SymbolTransformer(new transformers.TreeTransformer { + val s: extraction.trees.type = extraction.trees + val t: extraction.trees.type = extraction.trees + }) + + def run(pipeline: StainlessPipeline)(implicit context: Context) = + new WasmComponentRun(pipeline)(context) +} + +class WasmComponentRun(override val pipeline: StainlessPipeline) + (override implicit val context: Context) extends { + override val component = WasmComponent + override val trees: stainless.trees.type = stainless.trees +} with ComponentRun { + + def parse(json: io.circe.Json): NoReport = new NoReport + + override def createFilter: WasmFilter = new WasmFilter(this.context) + + override lazy val dependenciesFinder: DependenciesFinder { val t: stainless.trees.type } = new WasmDependenciesFinder + + private[stainless] def execute(functions: Seq[Identifier], symbols: trees.Symbols): Future[WasmAnalysis] = { + Future { + val intermSyms: intermediate.trees.Symbols = new intermediate.Lowering(context).transform(symbols) + val module = codegen.LinearMemoryCodeGen.transform(intermSyms, functions) + new wasm.FileWriter(module, context).writeFiles() + new WasmAnalysis + } + } +} diff --git a/core/src/main/scala/stainless/wasmgen/WasmDepFinder.scala b/core/src/main/scala/stainless/wasmgen/WasmDepFinder.scala new file mode 100644 index 0000000000..cf48d6b2ca --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/WasmDepFinder.scala @@ -0,0 +1,95 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen + +import stainless.Identifier +import stainless.trees._ +import stainless.utils.{DefinitionIdFinder, DependenciesFinder} + +class WasmDefIdFinder(val s: Symbols) extends DefinitionIdFinder { outer => + val trees = stainless.trees + private val lib: LibProvider { val trees: outer.trees.type } = new LibProvider { + protected val trees = outer.trees + } + private def fun(name: String) = lib.fun(name)(s).id + private def sort(name: String) = lib.sort(name)(s).id + private lazy val setIds = Set(sort("Set"), fun("SNil$0ToString"), fun("SCons$0ToString")) + private lazy val bagIds = Set(sort("Bag"), fun("BNil$0ToString"), fun("BCons$0ToString")) + private lazy val mapIds = Set(sort("Map"), fun("MNil$0ToString"), fun("MCons$0ToString")) + + override def traverse(expr: Expr, env: Env): Unit = { + expr match { + // Tuples + case Tuple(elems) => + ids += sort(s"Tuple${elems.size}") + case TupleSelect(tuple, _) => + val TupleType(ts) = tuple.getType(s) + ids += sort(s"Tuple${ts.size}") + // Sets + case FiniteSet(_, _) | SetAdd(_, _) => + ids += fun("setAdd") + ids ++= setIds + case ElementOfSet(_, _) => + ids += fun("elementOfSet") + ids ++= setIds + case SubsetOf(_, _) => + ids += fun("subsetOf") + ids ++= setIds + case SetIntersection(_, _) => + ids += fun("setIntersection") + ids ++= setIds + case SetUnion(_, _) => + ids += fun("setUnion") + ids ++= setIds + case SetDifference(_, _) => + ids += fun("setDifference") + ids ++= setIds + // Bags + case FiniteBag(_, _) | BagAdd(_, _) => + ids += fun("bagAdd") + ids ++= bagIds + case MultiplicityInBag(_, _) => + ids += fun("bagMultiplicity") + ids ++= bagIds + case BagIntersection(_, _) => + ids += fun("bagIntersection") + ids ++= bagIds + case BagUnion(_, _) => + ids += fun("bagUnion") + ids ++= bagIds + case BagDifference(_, _) => + ids += fun("bagDifference") + ids ++= bagIds + // Maps + case FiniteMap(_, _, _, _) | MapUpdated(_, _, _) => + ids += fun("mapUpdated") + ids ++= mapIds + case MapApply(_, _) => + ids += fun("mapApply") + ids ++= mapIds + case _ => + } + super.traverse(expr, env) + } +} + + +class WasmDependenciesFinder extends DependenciesFinder { + val t: stainless.trees.type = stainless.trees + def traverser(s: Symbols): DefinitionIdFinder { val trees: t.type } = new WasmDefIdFinder(s) + private val lib: LibProvider { val trees: t.type } = new LibProvider { + protected val trees = t + } + override def findDependencies(roots: Set[Identifier], s: Symbols): Symbols = { + super.findDependencies(roots, s) + .withFunctions(Seq( + "toString", "digitToStringL", "digitToStringI", + "i32ToString", "i64ToString", "f64ToString", + "booleanToString", "funToString", "unitToString" + ).map(lib.fun(_)(s))) + } +} + + + + diff --git a/core/src/main/scala/stainless/wasmgen/codegen/CodeGeneration.scala b/core/src/main/scala/stainless/wasmgen/codegen/CodeGeneration.scala new file mode 100644 index 0000000000..9dd4ae3956 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/codegen/CodeGeneration.scala @@ -0,0 +1,412 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless +package wasmgen +package codegen + +import intermediate.{trees => t} +import wasm._ +import Expressions.{eq => EQ, _} +import Types._ +import Definitions._ + +trait CodeGeneration { + + /* Environments */ + protected case class FunEnv( + s: t.Symbols, + gh: GlobalsHandler, + dh: DataHandler, + tab: Table + ) { + def env(lh: LocalsHandler): Env = Env(s, lh, gh, dh, tab) + } + protected case class Env( + s: t.Symbols, + lh: LocalsHandler, + gh: GlobalsHandler, + dh: DataHandler, + tab: Table + ) { + def fEnv = FunEnv(s, gh, dh, tab) + } + + // Make fresh labels using stainless identifiers + final protected def freshLabel(s: String): String = FreshIdentifier(s).uniqueName + + final protected val lib: LibProvider { val trees: t.type } = new LibProvider { + protected val trees = t + } + + /* Generate parts of the module */ + protected def mkImports(symbols: t.Symbols): Seq[Import] = { + Seq(Import("system", "printString", FunSig("_printString_", Seq(i32), void))) + } + protected def mkGlobals(s: t.Symbols): Seq[ValDef] + /* Called after the functions are created to update the initial values of the globals */ + protected def updateGlobals(env: FunEnv): Unit + protected def mkTable(s: t.Symbols) = Table( + s.functions.values.toList.filter(_.flags.contains(t.Dynamic)).map(_.id.uniqueName) + ) + protected def mkBuiltins(s: t.Symbols, toExecute: Seq[Identifier])(implicit funEnv: FunEnv): Seq[FunDef] = { + Seq( + mkMain(s, toExecute), + mkEquality(s), mkInequality(s), + mkFloatToSign(f32), mkFloatToSign(f64), + mkToString(s), mkBigIntToString, mkArrayToString, mkCharToString, + mkStringConcat, mkSubstring + ) + } + + /* Built-in functions */ + final protected val stringConcatName = "_string_concat_" + final protected val substringName = "_substring_" + final protected val refEqualityName = "_ref_eq_" + final protected val refInequalityName = "_ref_ineq_" + final protected val refToStringName = "_ref_toString_" + final protected def arrayCopyName(tpe: Type) = s"_array_copy_${tpe}_" + final protected def floatToSignName(tpe: Type) = s"_${tpe}_sign_" + protected val builtinToStrings: Set[String] + final protected def toStringName(name: String)(implicit funEnv: FunEnv): String = { + val fullName = s"${name}ToString" + if (builtinToStrings contains name) fullName + else lib.fun(fullName)(funEnv.s).id.uniqueName + } + private def mkFloatToSign(tpe: Type) = { + require(tpe == f32 || tpe == f64) + FunDef(floatToSignName(tpe), Seq(ValDef("lhs", tpe), ValDef("rhs", tpe)), i32) { implicit lh => + val lhs = GetLocal("lhs") + val rhs = GetLocal("rhs") + If( + freshLabel("label"), + gt(lhs, rhs), + I32Const(1), + If( + freshLabel("label"), + lt(lhs, rhs), + I32Const(-1), + I32Const(0) + ) + ) + } + } + private def mkMain(s: t.Symbols, toExecute: Seq[Identifier])(implicit funEnv: FunEnv): FunDef = { + FunDef("_main_", Seq(), void) { lh => + transform(t.sequence( + toExecute map { fid => + t.Output(t.StringConcat( + t.StringLiteral(s"${fid.name} = "), + t.FunctionInvocation(lib.fun("toString")(funEnv.s).id, Seq(), + Seq(t.FunctionInvocation(fid, Seq(), Seq()))) + )) + } + ))(funEnv.env(lh)) + } + } + /* Abstract builtins (related to ref. types) */ + protected def mkEquality(s: t.Symbols): FunDef + protected def mkInequality(s: t.Symbols): FunDef + protected def mkToString(s: t.Symbols)(implicit funEnv: FunEnv): FunDef + protected def mkCharToString(implicit funEnv: FunEnv): FunDef + protected def mkBigIntToString(implicit funEnv: FunEnv): FunDef + protected def mkArrayToString(implicit funEnv: FunEnv): FunDef + protected def mkStringConcat(implicit funEnv: FunEnv): FunDef + protected def mkSubstring(implicit funEnv: FunEnv): FunDef + + /** Transform a stainless Symbols into a wasm Module */ + final def transform(s: t.Symbols, toExecute: Seq[Identifier]): Module = { + val imports = mkImports(s) + val globals = mkGlobals(s) + val tab = mkTable(s) + Module("program", imports, globals, tab){ (gh, dh) => + implicit val funEnv = FunEnv(s, gh, dh, tab) + val funs = mkBuiltins(s, toExecute) ++ s.functions.values.toList.map(transform) + updateGlobals(funEnv) + funs + } + } + + /** Transform a stainless FunDef to a wasm FunDef */ + final def transform(fd: t.FunDef)(implicit env: FunEnv): FunDef = { + implicit val s = env.s + FunDef( + fd.id.uniqueName, + fd.params.map(arg => ValDef(arg.id.uniqueName, transform(arg.tpe))).filterNot(_.tpe == void), + transform(fd.returnType) + ) { lh => + transform(fd.fullBody)(env.env(lh)) + } + } + + /* Expr. Helpers */ + + final protected def typeToSign(tpe: t.Typed)(implicit s: t.Symbols): Sign = { + tpe.getType match { + case t.BVType(false, _) => Unsigned + case _ => Signed + } + } + + final protected def typeToOp(tpe: t.Typed, intOp: Sign => BinOp, floatOp: BinOp)(implicit s: t.Symbols): BinOp = { + tpe.getType match { + case t.RealType() => floatOp + case t.BVType(false, _) => intOp(Unsigned) + case _ => intOp(Signed) + } + } + + final protected def mkBin(op: BinOp, lhs: t.Expr, rhs: t.Expr)(implicit env: Env): Expr = { + op(transform(lhs), transform(rhs)) + } + + final protected def surfaceEq(lhs: Expr, rhs: Expr, tpe: t.Type): Expr = { + tpe match { + case t.RecordType(_) => + Call(refEqualityName, i32, Seq(lhs, rhs)) + case t.UnitType() => + I32Const(1) + case _ => + EQ(lhs, rhs) + } + } + final protected def surfaceIneq(lhs: Expr, rhs: Expr, tpe: t.Type): Expr = + tpe match { + case t.RecordType(_) => + Call(refInequalityName, i32, Seq(lhs, rhs)) + case t.UnitType() => + I32Const(0) + case _ => + baseTypeIneq(lhs, rhs) + } + final protected def baseTypeIneq(lhs: Expr, rhs: Expr): Expr = + lhs.getType match { + case `f32` => + Call(floatToSignName(f32), i32, Seq(lhs, rhs)) + case `f64` => + Call(floatToSignName(f64), i32, Seq(lhs, rhs)) + case `i64` => + Wrap(i32, sub(lhs, rhs)) + case `i32` => + sub(lhs, rhs) + } + + final protected def surfaceToString(arg: Expr, tpe: t.Type)(implicit funEnv: FunEnv): Expr = { + tpe match { + case t.RecordType(_) => + Call(refToStringName, i32, Seq(arg)) + case t.UnitType() => + Call(toStringName("unit"), i32, Seq()) + case t.BooleanType() => + Call(toStringName("boolean"), i32, Seq(arg)) + case t.CharType() => + Call(toStringName("char"), i32, Seq(arg)) + case t.StringType() => + arg + case t.ArrayType(_) => + Call(toStringName("array"), i32, Seq(arg)) + case t.IntegerType() => + Call(toStringName("BigInt"), i32, Seq(arg)) + case _ => + Call(toStringName(arg.getType.toString), i32, Seq(arg)) + } + } + + + /* Abstract expression constructors (related to ref. types) */ + protected def mkRecord(recordType: t.RecordType, fields: Seq[Expr])(implicit env: Env): Expr + protected def mkRecordSelector(expr: Expr, rt: t.RecordType, id: Identifier)(implicit env: Env): Expr + protected def mkCastDown(expr: Expr, subType: t.RecordType)(implicit env: Env): Expr + protected def mkCastUp(expr: Expr, superType: t.RecordType)(implicit env: Env): Expr + protected def mkNewArray(length: Expr, init: Option[Expr])(implicit env: Env): Expr + protected def mkArrayGet(array: Expr, index: Expr)(implicit env: Env): Expr + protected def mkArraySet(array: Expr, index: Expr, value: Expr)(implicit env: Env): Expr + protected def mkArrayLength(expr: Expr)(implicit env: Env): Expr + protected def mkStringLiteral(s: String)(implicit env: Env): Expr + + /** Transform a stainless Expr into a wasm Expr */ + final def transform(expr: t.Expr)(implicit env: Env): Expr = { + implicit val lh = env.lh + implicit val s = env.s + val compareId = lib.fun("compare").id + val toStringId = lib.fun("toString").id + expr match { + case t.NoTree(tpe) => + Unreachable + case t.Variable(id, tpe, flags) => + if (tpe == t.UnitType()) Nop + else GetLocal(id.uniqueName) + case t.Let(vd, value, body) => + if (vd.getType == t.UnitType()) { + Sequence(Seq(transform(value), transform(body))) + } else { + val local = lh.getFreshLocal(vd.id.uniqueName, transform(vd.getType)) + Sequence(Seq( + SetLocal(local, transform(value)), + transform(body) + )) + } + case t.Output(msg) => + Call("_printString_", void, Seq(transform(msg))) + case t.FunctionInvocation(`compareId`, _, Seq(lhs, rhs)) => + surfaceIneq(transform(lhs), transform(rhs), lhs.getType) + case t.FunctionInvocation(`toStringId`, _, Seq(arg)) => + surfaceToString(transform(arg), arg.getType)(env.fEnv) + case fi@t.FunctionInvocation(id, _, args) => + if (args.exists(_.getType == t.UnitType())) { + val (argComps, argNames) = args.map(arg => + if (arg.getType == t.UnitType()) (transform(arg), None) + else { + val tmp = lh.getFreshLocal(freshLabel("arg"), transform(arg.getType)) + (SetLocal(tmp, transform(arg)), Some(GetLocal(tmp))) + } + ).unzip + Sequence( + argComps :+ + Call(id.uniqueName, transform(fi.getType), argNames.flatten) + ) + } else { + Call(id.uniqueName, transform(fi.getType), args map transform) + } + case t.Sequence(es) => + Sequence ( es map transform ) + + case t.IfExpr(cond, thenn, elze) => + If( + freshLabel("label"), + transform(cond), + transform(thenn), + transform(elze) + ) + case t.Equals(lhs, rhs) => + surfaceEq(transform(lhs), transform(rhs), lhs.getType) + + case t.UnitLiteral() => + Nop + case bvl@t.BVLiteral(_, _, size) => + if (size <= 32) I32Const(bvl.toBigInt.toInt) + else I64Const(bvl.toBigInt.toLong) + case t.BooleanLiteral(value) => + I32Const(if (value) 1 else 0) + case t.StringLiteral(str) => + mkStringLiteral(str) + case t.CharLiteral(value) => + I32Const(value.toInt) + case t.IntegerLiteral(value) => + // TODO: Represent mathematical integers adequately + I64Const( + if (value.isValidLong) value.toLong + else if (value > Long.MaxValue) Long.MaxValue + else Long.MinValue + ) + case t.FractionLiteral(numerator, denominator) => + F64Const((BigDecimal(numerator) / BigDecimal(denominator)).toDouble) + + case t.Record(tpe, fields) => + mkRecord(tpe, fields map transform) + case rs@t.RecordSelector(record, selector) => + val rt = record.getType.asInstanceOf[t.RecordType] + mkRecordSelector(transform(record), rt, selector) + + case t.FunctionPointer(id) => + I32Const(env.tab.indexOf(id.uniqueName)) + case t.Application(callee, args) => + CallIndirect( + transform(callee.getType.asInstanceOf[t.FunctionType].to), + transform(callee), + args map transform + ) + + case t.CastDown(e, subtype) => + mkCastDown(transform(e), subtype) + case t.CastUp(e, supertype) => + mkCastUp(transform(e), supertype) + + case t.NewArray(length, init) => + mkNewArray(transform(length), init map transform) + case ag@t.ArraySelect(array, index) => + mkArrayGet(transform(array), transform(index)) + case t.ArraySet(array, index, value) => + mkArraySet(transform(array), transform(index), transform(value)) + case t.ArrayLength(array) => + mkArrayLength(transform(array)) + + case t.StringLength(expr) => + Extend(i64, Unsigned, mkArrayLength(transform(expr))) + case t.StringConcat(lhs, rhs) => + Call(stringConcatName, i32, Seq(transform(lhs), transform(rhs))) + case t.SubString(expr, start, end) => + Call(substringName, i32, Seq(transform(expr), Wrap(i32, transform(start)), Wrap(i32, transform(end)))) + + case t.Plus(lhs, rhs) => + mkBin(add, lhs, rhs) + case t.Minus(lhs, rhs) => + mkBin(sub, lhs, rhs) + case t.Times(lhs, rhs) => + mkBin(mul, lhs, rhs) + case t.Division(lhs, rhs) => + mkBin(typeToOp(lhs, div(_), div), lhs, rhs) + case t.Remainder(lhs, rhs) => + mkBin(rem(typeToSign(lhs)), lhs, rhs) + case t.Modulo(lhs, rhs) => + mkBin(rem(Unsigned), lhs, rhs) + case t.UMinus(e) => + e.getType match { + case t.RealType() => Unary(neg, transform(e)) + case tpe => + Binary(sub, zero(transform(tpe)), transform(e)) + } + case t.LessThan(lhs, rhs) => + mkBin(typeToOp(lhs, lt(_), lt), lhs, rhs) + case t.GreaterThan(lhs, rhs) => + mkBin(typeToOp(lhs, gt(_), gt), lhs, rhs) + case t.LessEquals(lhs, rhs) => + mkBin(typeToOp(lhs, le(_), le), lhs, rhs) + case t.GreaterEquals(lhs, rhs) => + mkBin(typeToOp(lhs, ge(_), ge), lhs, rhs) + + case t.BVNot(e) => + xor(zero(transform(e.getType)), transform(e)) + case t.BVAnd(lhs, rhs) => + mkBin(and, lhs, rhs) + case t.BVOr(lhs, rhs) => + mkBin(or, lhs, rhs) + case t.BVXor(lhs, rhs) => + mkBin(xor, lhs, rhs) + case t.BVShiftLeft(lhs, rhs) => + mkBin(shl, lhs, rhs) + case t.BVAShiftRight(lhs, rhs) => + mkBin(shr(Signed), lhs, rhs) + case t.BVLShiftRight(lhs, rhs) => + mkBin(shr(Unsigned), lhs, rhs) + case t.BVNarrowingCast(expr, newType) => + Wrap(transform(newType), transform(expr)) + case t.BVWideningCast(expr, newType) => + Extend(transform(newType), typeToSign(expr.getType), transform(expr)) + + case t.And(exprs) => + exprs map transform reduceRight[Expr] { case (e1, e2) => + If(freshLabel("label"), e1, e2, I32Const(0)) + } + case t.Or(exprs) => + exprs map transform reduceRight[Expr] { case (e1, e2) => + If(freshLabel("label"), e1, I32Const(1), e2) + } + case t.Not(expr) => + sub(I32Const(1), transform(expr)) + } + } + + /** Transform a stainless type to a wasm type */ + def transform(tpe: t.Type)(implicit s: t.Symbols): Type = tpe match { + case t.UnitType() => void + case t.BooleanType() | t.CharType() => i32 + case t.IntegerType() => i64 + case t.RealType() => f64 + case t.BVType(_, size) => if (size > 32) i64 else i32 + case t.FunctionType(_, _) => i32 + case t.ArrayType(_) | t.RecordType(_) | t.StringType() => + sys.error("Reference types are left abstract " + + "and have to be implemented in a subclass of wasm CodeGeneration") + } + +} diff --git a/core/src/main/scala/stainless/wasmgen/codegen/LinearMemoryCodeGen.scala b/core/src/main/scala/stainless/wasmgen/codegen/LinearMemoryCodeGen.scala new file mode 100644 index 0000000000..9842ec9575 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/codegen/LinearMemoryCodeGen.scala @@ -0,0 +1,509 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen +package codegen + +import stainless.Identifier +import intermediate.{trees => t} +import wasm.{GlobalsHandler, LocalsHandler} +import wasm.Expressions.{eq => EQ, _} +import wasm.Types._ +import wasm.Definitions._ + +/** Implements memory allocations in linear memory + * + * Global variable 0 points to the free linear memory boundary + * + */ +object LinearMemoryCodeGen extends CodeGeneration { + private val memB = "memB" + private val safeMem: Boolean = true + private val mallocName = "_malloc_" + // Checks if we can allocate a given number of bytes in memory. + // If not, tries to grow the memory and fails if it is impossible. + // Then allocates bytes and returns the **previous** free memory boundary + private def mkMalloc(implicit funEnv: FunEnv) = { + val pageShift = I32Const(16) // 64K + FunDef(mallocName, Seq(ValDef("size", i32)), i32) { implicit lh => + implicit val env = funEnv.env(lh) + implicit val gh = env.gh + val getMem = GetGlobal(memB) + val size = GetLocal("size") + val loop = freshLabel("loop") + Sequence(Seq(Loop(loop, + If( + freshLabel("label"), + gt(Unsigned)( + add(getMem, size), + shl(MemorySize, pageShift) + ), + If( + freshLabel("label"), + EQ(MemoryGrow(MemorySize), I32Const(-1)), + Sequence(Seq( + transform(t.Output(t.StringLiteral("Error: Out of memory"))), + Unreachable + )), + Br(loop) + ), + Return(Sequence(Seq( + getMem, + SetGlobal(memB, add(getMem, size)) + ))) + ) + ), I32Const(0))) // bogus, to satisfy the type checker + } + } + private def malloc(size: Expr)(implicit gh: GlobalsHandler) = { + if (safeMem) Call(mallocName, i32, Seq(size)) + else Sequence(Seq( + GetGlobal(memB), + SetGlobal(memB, add(GetGlobal(memB), size)) + )) + } + + override protected def mkImports(s: t.Symbols): Seq[Import] = + Import("system", "mem", Memory(1)) +: super.mkImports(s) + + protected def mkGlobals(s: t.Symbols) = Seq(ValDef(memB, i32)) + + protected def updateGlobals(funEnv: FunEnv): Unit = { + funEnv.gh.update(memB, I32Const(funEnv.dh.nextFree)) + } + + override def mkBuiltins(s: t.Symbols, toExecute: Seq[Identifier])(implicit funEnv: FunEnv): Seq[FunDef] = { + super.mkBuiltins(s, toExecute) ++ (if (safeMem) Seq(mkMalloc) else Seq()) + } + + /* Helpers */ + // Compute the address of an element in an array from base and offset + private def elemAddr(array: Expr, offset: Expr) = add(array, mul(add(offset, I32Const(1)), I32Const(4))) + private def strCharAddr(string: Expr, offset: Expr) = add(string, add(offset, I32Const(4))) + private def unbox(tpe: Type, ref: Expr) = Load(tpe, None, add(ref, I32Const(4))) + + protected def mkEquality(s: t.Symbols): FunDef = { + implicit val impS = s + + def boxedEq(tpe: Type, lhs: Expr, rhs: Expr)(name: String = tpe.toString): (Expr, String) = + (EQ(unbox(tpe, lhs), unbox(tpe, rhs)), name) + + def recordEq(rec: t.RecordSort, lhs: Expr, rhs: Expr): (Expr, String) = { + // We get offsets of all fields except first (typeTag) which we know is equal already + val offsets = rec.allFields.scanLeft(0)((off, fld) => off + transform(fld.getType).size).tail + val fieldEqs = rec.allFields.tail.zip(offsets).map { case (fld, off) => + val wasmTpe = transform(fld.getType) + val l = Load(wasmTpe, None, add(lhs, I32Const(off))) + val r = Load(wasmTpe, None, add(rhs, I32Const(off))) + surfaceEq(l, r, fld.getType) + } + (fieldEqs.foldRight(I32Const(1): Expr) { case (e, rest) => + If(freshLabel("label"), e, rest, I32Const(0)) + }, rec.id.uniqueName) + } + + def allEqs(lhs: Expr, rhs: Expr): Seq[(Expr, String)] = { + Seq( + (I32Const(1), "unit"), + boxedEq(i32, lhs, rhs)("boolean"), + boxedEq(i32, lhs, rhs)("char"), + boxedEq(i32, lhs, rhs)(), + boxedEq(i64, lhs, rhs)(), + boxedEq(i64, lhs, rhs)("BigInt"), + boxedEq(f64, lhs, rhs)(), + boxedEq(i32, lhs, rhs)("array"), + boxedEq(i32, lhs, rhs)("string"), + boxedEq(i32, lhs, rhs)("function") + ) ++ { + val sorts = s.records.values.toSeq.collect { case c: t.ConstructorSort => c }.sortBy(_.typeTag) + sorts map (s => recordEq(s, lhs, rhs)) + } + } + + FunDef(refEqualityName, Seq(ValDef("lhs", i32), ValDef("rhs", i32)), i32) { implicit lh => + Sequence(Seq( + If( + freshLabel("label"), + EQ(Load(i32, None, GetLocal("lhs")), Load(i32, None, GetLocal("rhs"))), { + val eqs = allEqs(GetLocal("lhs"), GetLocal("rhs")) + // We use i32 as default, whatever, should not happen + val jump = BrTable(eqs.map(_._2), eqs.head._2, Load(i32, None, GetLocal("lhs")), None) + eqs.foldLeft(jump: Expr) { case (first, (equality, label)) => + Sequence(Seq(Block(label, first), Return(equality))) + } + }, + Return(I32Const(0)) + ), + I32Const(0) + )) + } + } + + protected def mkInequality(s: t.Symbols): FunDef = { + implicit val impS = s + + def boxedIneq(tpe: Type, lhs: Expr, rhs: Expr)(name: String = tpe.toString): (Expr, String) = + (baseTypeIneq(unbox(tpe, lhs), unbox(tpe, rhs)), name) + + def recordIneq(rec: t.RecordSort, lhs: Expr, rhs: Expr, temp: String)(implicit lh: LocalsHandler): (Expr, String) = { + // We get offsets of all fields except first (typeTag) which we know is equal already + val offsets = rec.allFields.scanLeft(0)((off, fld) => off + transform(fld.getType).size).tail + val fieldIneqs = rec.allFields.tail.zip(offsets).map { case (fld, off) => + val wasmTpe = transform(fld.getType) + val l = Load(wasmTpe, None, add(lhs, I32Const(off))) + val r = Load(wasmTpe, None, add(rhs, I32Const(off))) + surfaceIneq(l, r, fld.getType) + } + (fieldIneqs.foldRight(I32Const(0): Expr) { case (e, rest) => + Sequence(Seq( + SetLocal(temp, e), + If(freshLabel("label"), eqz(GetLocal(temp)), rest, GetLocal(temp)) + )) + }, rec.id.uniqueName) + } + + def allIneqs(lhs: Expr, rhs: Expr, temp: String)(implicit lh: LocalsHandler): Seq[(Expr, String)] = { + Seq( + (I32Const(0), "unit"), + boxedIneq(i32, lhs, rhs)("boolean"), + boxedIneq(i32, lhs, rhs)("char"), + boxedIneq(i32, lhs, rhs)(), + boxedIneq(i64, lhs, rhs)(), + boxedIneq(i64, lhs, rhs)("BigInt"), + boxedIneq(f64, lhs, rhs)(), + boxedIneq(i32, lhs, rhs)("array"), + boxedIneq(i32, lhs, rhs)("string"), + boxedIneq(i32, lhs, rhs)("function") + ) ++ { + val sorts = s.records.values.toSeq.collect { case c: t.ConstructorSort => c }.sortBy(_.typeTag) + sorts map (s => recordIneq(s, lhs, rhs, temp)) + } + } + + FunDef(refInequalityName, Seq(ValDef("lhs", i32), ValDef("rhs", i32)), i32) { implicit lh => + val temp = lh.getFreshLocal("temp", i32) + lh.getFreshLocal("tempf32", f32) + lh.getFreshLocal("tempf64", f64) + Sequence(Seq( + SetLocal(temp, sub(Load(i32, None, GetLocal("lhs")), Load(i32, None, GetLocal("rhs")))), + If( + freshLabel("label"), + eqz(GetLocal(temp)), { + val ineqs = allIneqs(GetLocal("lhs"), GetLocal("rhs"), temp) + // We use i32 as default, whatever, should not happen + val jump = BrTable(ineqs.map(_._2), ineqs.head._2, Load(i32, None, GetLocal("lhs")), None) + ineqs.foldLeft(jump: Expr) { case (first, (ineq, label)) => + Sequence(Seq(Block(label, first), Return(ineq))) + } + }, + Return(GetLocal(temp)) + ), + I32Const(0) // Should never happen + )) + } + } + + + protected def mkToString(s: t.Symbols)(implicit funEnv: FunEnv): FunDef = { + + def boxedToString(tpe: Type, arg: Expr)(tpeName: String = tpe.toString): (Expr, String) = + (Call(toStringName(tpeName), i32, Seq(unbox(tpe, arg))), tpeName) + + def recordToString(rec: t.ConstructorSort, arg: Expr): (Expr, String) = { + (Call(toStringName(rec.id.uniqueName), i32, Seq(arg)), rec.id.uniqueName) + } + + def allToStrings(arg: Expr): Seq[(Expr, String)] = { + Seq( + (Call(toStringName("unit"), i32, Seq()), "unit"), + boxedToString(i32, arg)("boolean"), + boxedToString(i32, arg)("char"), + boxedToString(i32, arg)(), + boxedToString(i64, arg)(), + boxedToString(i64, arg)("BigInt"), + boxedToString(f64, arg)(), + boxedToString(i32, arg)("array"), + (unbox(i32, arg), "string"), + (Call(toStringName("fun"), i32, Seq()), "function") + ) ++ { + val sorts = s.records.values.toSeq.collect { case c: t.ConstructorSort => c }.sortBy(_.typeTag) + sorts map (s => recordToString(s, arg)) + } + } + + FunDef(refToStringName, Seq(ValDef("arg", i32)), i32) { implicit lh => + val toStrings = allToStrings(GetLocal("arg")) + // We use i32 as default, whatever, should not happen + val jump = BrTable(toStrings.map(_._2), toStrings(2)._2, Load(i32, None, GetLocal("arg")), None) + toStrings.foldLeft(jump: Expr) { case (first, (toS, label)) => + Sequence(Seq(Block(label, first), Return(toS))) + } + } + } + + protected val builtinToStrings = Set("char", "array", "BigInt") + + protected def mkCharToString(implicit funEnv: FunEnv): FunDef = { + implicit val gh = funEnv.gh + FunDef(toStringName("char"), Seq(ValDef("arg", i32)), i32){ implicit lh => + val mem = lh.getFreshLocal("mem", i32) + Sequence(Seq( + SetLocal(mem, malloc(I32Const(8))), + Store(None, GetLocal(mem), I32Const(1)), + Store(None, add(GetLocal(mem), I32Const(4)), GetLocal("arg")), + GetLocal(mem) + )) + } + } + + protected def mkBigIntToString(implicit funEnv: FunEnv): FunDef = { + FunDef(toStringName("BigInt"), Seq(ValDef("arg", i64)), i32){ implicit lh => + implicit val env = funEnv.env(lh) + Call(stringConcatName, i32, Seq( + Call(stringConcatName, i32, Seq( + transform(t.StringLiteral("BigInt(")), + Call(toStringName("i64"), i32, Seq(GetLocal("arg"))) + )), + transform(t.StringLiteral(")")) + )) + } + } + + protected def mkArrayToString(implicit funEnv: FunEnv): FunDef = { + FunDef(toStringName("array"), Seq(ValDef("array", i32)), i32) { implicit lh => + implicit val env = funEnv.env(lh) + val ind = lh.getFreshLocal(freshLabel("index"), i32) + val curr = lh.getFreshLocal(freshLabel("current"), i32) + val loop = freshLabel("loop") + + def indToPtr(e: Expr) = elemAddr(GetLocal("array"), e) + + Sequence(Seq( + SetLocal(ind, I32Const(0)), + SetLocal(curr, transform(t.StringLiteral(""))), + Loop(loop, + If( + freshLabel("label"), + lt(Unsigned)(GetLocal(ind), Load(i32, None, GetLocal("array"))), + Sequence(Seq( + SetLocal(curr, + Call(stringConcatName, i32, Seq( + GetLocal(curr), + If( + freshLabel("label"), + eqz(GetLocal(ind)), + Call(refToStringName, i32, Seq(Load(i32, None, indToPtr(GetLocal(ind))))), + Call(stringConcatName, i32, Seq( + transform(t.StringLiteral(", ")), + Call(refToStringName, i32, Seq(Load(i32, None, indToPtr(GetLocal(ind))))) + )) + ) + )) + ), + SetLocal(ind, add(GetLocal(ind), I32Const(1))), + Br(loop) + )), + Nop + ) + ), + Call(stringConcatName, i32, Seq( + transform(t.StringLiteral("Array(")), + Call(stringConcatName, i32, Seq( + GetLocal(curr), transform(t.StringLiteral(")")) + )) + )) + )) + } + } + + protected def mkStringLiteral(str: String)(implicit env: Env): Expr = { + val length = str.length + val mask = 0xFF + val l0 = length & mask + val l1 = (length >> 8) & mask + val l2 = (length >> 16) & mask + val l3 = (length >> 24) & mask + val lbytes = Seq(l0, l1, l2, l3).map(_.toByte.r) // Little endian + val content = str.map(_.toByte.f) + I32Const(env.dh.addNext(lbytes ++ content)) + } + + protected def mkSubstring(implicit funEnv: FunEnv): FunDef = { + implicit val gh = funEnv.gh + FunDef(substringName, Seq("string", "from", "to").map(ValDef(_, i32)), i32) { implicit lh => + val str = GetLocal("string") + val from = GetLocal("from") + val to = GetLocal("to") + val index = lh.getFreshLocal("index", i32) + val length = lh.getFreshLocal("length", i32) + val loop = freshLabel("loop") + val mem = lh.getFreshLocal("mem", i32) + Sequence(Seq( + SetLocal(length, sub(to, from)), + SetLocal(mem, malloc(add(GetLocal(length), I32Const(4)))), + Store(None, GetLocal(mem), GetLocal(length)), + SetLocal(index, I32Const(0)), + Loop(loop, + If( + freshLabel("label"), + lt(Unsigned)(GetLocal(index), GetLocal(length)), // index < length + Sequence(Seq( + Store(Some(i8), + strCharAddr(GetLocal(mem), GetLocal(index)), + Load(i32, Some((i8, Unsigned)), strCharAddr(str, add(from, GetLocal(index)))) + ), + SetLocal(index, add(GetLocal(index), I32Const(1))), + Br(loop) + )), + Nop + ) + ), + GetLocal(mem) + )) + } + } + + protected def mkStringConcat(implicit funEnv: FunEnv): FunDef = { + implicit val gh = funEnv.gh + FunDef(stringConcatName, Seq("lhs", "rhs").map(ValDef(_, i32)), i32) { implicit lh => + val lhs = GetLocal("lhs") + val rhs = GetLocal("rhs") + val len1 = Load(i32, None, lhs) + val len2 = Load(i32, None, rhs) + val index = lh.getFreshLocal("index", i32) + val mem = lh.getFreshLocal("mem", i32) + val loop = freshLabel("loop") + Sequence(Seq( + SetLocal(mem, malloc(add(add(len1, len2), I32Const(4)))), + Store(None, GetLocal(mem), add(len1, len2)), // concat length + SetLocal(index, I32Const(0)), + Loop(loop, + If( + freshLabel("label"), + lt(Signed)(GetLocal(index), len1), // index < length + Sequence(Seq( + Store(Some(i8), + strCharAddr(GetLocal(mem), GetLocal(index)), + Load(i32, Some((i8, Unsigned)), strCharAddr(lhs, GetLocal(index))) + ), + SetLocal(index, add(GetLocal(index), I32Const(1))), + Br(loop) + )), + Nop + ) + ), + SetLocal(index, I32Const(0)), + Loop(loop, + If( + freshLabel("label"), + lt(Signed)(GetLocal(index), len2), // index < length + Sequence(Seq( + Store(Some(i8), + strCharAddr(GetLocal(mem), add(len1, GetLocal(index))), + Load(i32, Some((i8, Unsigned)), strCharAddr(rhs, GetLocal(index))) + ), + SetLocal(index, add(GetLocal(index), I32Const(1))), + Br(loop) + )), + Nop + ) + ), + GetLocal(mem) + )) + } + } + + protected def mkRecord(recordType: t.RecordType, fields: Seq[Expr])(implicit env: Env): Expr = { + implicit val gh = env.gh + implicit val lh = env.lh + // offsets for fields, with last element being the new memory boundary + val offsets = fields.scanLeft(0)(_ + _.getType.size) + val mem = lh.getFreshLocal(freshLabel("mem"), i32) + + val mkFields = fields.zip(offsets).map { case (e, off) => + if (e.getType == void) e + else Store(None, add(GetLocal(mem), I32Const(off)), e) + } + + Sequence( + SetLocal(mem, malloc(I32Const(offsets.last))) +: + mkFields :+ + GetLocal(mem) + ) + } + + protected def mkRecordSelector(expr: Expr, rt: t.RecordType, id: Identifier)(implicit env: Env): Expr = { + implicit val s = env.s + val fields = rt.getRecord.allFields + val tpe = transform(fields.find(_.id == id).get.getType) + if (tpe == void) Nop + else { + val offset = fields + .takeWhile(_.id != id) + .map(fd => transform(fd.getType).size) + .sum + Load(tpe, None, add(expr, I32Const(offset))) + } + } + + protected def mkCastDown(expr: Expr, subType: t.RecordType)(implicit env: Env): Expr = { + expr + } + + // Up-casts are trivial + protected def mkCastUp(expr: Expr, superType: t.RecordType)(implicit env: Env): Expr = expr + + protected def mkNewArray(length: Expr, init: Option[Expr])(implicit env: Env): Expr = { + implicit val lh = env.lh + implicit val gh = env.gh + val evLength = lh.getFreshLocal(freshLabel("length"), i32) + val evInit = lh.getFreshLocal(freshLabel("init"), i32) + val mem = lh.getFreshLocal("mem", i32) + + Sequence( + Seq( + SetLocal(evLength, length), + SetLocal(mem, malloc(mul(add(GetLocal(evLength), I32Const(1)), I32Const(4)))), + Store(None, GetLocal(mem), GetLocal(evLength)) + ) ++ + init.toSeq.flatMap { elem => + val ind = lh.getFreshLocal(freshLabel("index"), i32) + val loop = freshLabel("loop") + Seq( + SetLocal(evInit, elem), + SetLocal(ind, I32Const(0)), + Loop(loop, Sequence(Seq( + If( + freshLabel("label"), + lt(Signed)(GetLocal(ind), GetLocal(evLength)), + Sequence(Seq( + Store(None, + elemAddr(GetLocal(mem), GetLocal(ind)), + GetLocal(evInit) + ), + SetLocal(ind, add(GetLocal(ind), I32Const(1))), + Br(loop) + )), + Nop + ) + ))) + ) + } ++ + Seq(GetLocal(mem)) + ) + } + + protected def mkArrayGet(array: Expr, index: Expr)(implicit env: Env): Expr = { + Load(i32, None, elemAddr(array, index)) + } + + protected def mkArraySet(array: Expr, index: Expr, value: Expr)(implicit env: Env): Expr = { + Store(None, elemAddr(array, index), value) + } + + protected def mkArrayLength(expr: Expr)(implicit env: Env): Expr = Load(i32, None, expr) + + override def transform(tpe: t.Type)(implicit s: t.Symbols): Type = tpe match { + case t.ArrayType(_) | t.RecordType(_) | t.StringType() => i32 + case _ => super.transform(tpe) + } +} diff --git a/core/src/main/scala/stainless/wasmgen/intermediate/Constructors.scala b/core/src/main/scala/stainless/wasmgen/intermediate/Constructors.scala new file mode 100644 index 0000000000..9c5e615ba6 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/intermediate/Constructors.scala @@ -0,0 +1,11 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen.intermediate + +trait Constructors extends stainless.ast.Constructors { self: Trees => + def sequence(es: Seq[Expr]): Expr = es match { + case Seq() => UnitLiteral() + case Seq(elem) => elem + case more => Sequence(more) + } +} diff --git a/core/src/main/scala/stainless/wasmgen/intermediate/Deconstructors.scala b/core/src/main/scala/stainless/wasmgen/intermediate/Deconstructors.scala new file mode 100644 index 0000000000..31981266a3 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/intermediate/Deconstructors.scala @@ -0,0 +1,86 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen.intermediate + +trait TreeDeconstructor extends stainless.ast.TreeDeconstructor { + protected val s: Trees + protected val t: Trees + + // Reminder: + // protected type Deconstructed[T <: t.Tree] = (Seq[Identifier], Seq[s.Variable], Seq[s.Expr], Seq[s.Type], Seq[s.Flag], Builder[T]) + // protected type Builder[T <: t.Tree] = (Seq[Identifier], Seq[t.Variable], Seq[t.Expr], Seq[t.Type], Seq[t.Flag]) => T + + override def deconstruct(expr: s.Expr): Deconstructed[t.Expr] = expr match { + case s.Record(tpe, fields) => ( + NoIdentifiers, NoVariables, fields, Seq(tpe), NoFlags, + (_, _, es, tpe, _) => t.Record(tpe.head.asInstanceOf[t.RecordType], es) + ) + + case s.RecordSelector(record, selector) => ( + Seq(selector), NoVariables, Seq(record), NoTypes, NoFlags, + (ids, _, es, _, _) => t.RecordSelector(es.head, ids.head) + ) + + case s.FunctionPointer(id) => ( + Seq(id), NoVariables, NoExpressions, NoTypes, NoFlags, + (ids, _, _, _, _) => t.FunctionPointer(ids.head) + ) + + case s.CastDown(e, tp) => ( + NoIdentifiers, NoVariables, Seq(e), Seq(tp), NoFlags, + (_, _, es, tps, _) => t.CastDown(es.head, tps.head.asInstanceOf[t.RecordType]) + ) + + case s.CastUp(e, tp) => ( + NoIdentifiers, NoVariables, Seq(e), Seq(tp), NoFlags, + (_, _, es, tps, _) => t.CastUp(es.head, tps.head.asInstanceOf[t.RecordType]) + ) + + case s.Output(msg) => ( + NoIdentifiers, NoVariables, Seq(msg), NoTypes, NoFlags, + (_, _, es, _, _) => t.Output(es.head) + ) + + case s.Sequence(es) => ( + NoIdentifiers, NoVariables, es, NoTypes, NoFlags, + (_, _, es1, _, _) => t.Sequence(es1) + ) + + case s.NewArray(length, init) => ( + NoIdentifiers, NoVariables, Seq(length) ++ init, Seq(), NoFlags, + (_, _, es, _, _) => t.NewArray(es(0), if (es.size > 1) Some(es(1)) else None) + ) + + case s.ArraySet(array, index, value) => ( + NoIdentifiers, NoVariables, Seq(array, index, value), NoTypes, NoFlags, + (_, _, es, _, _) => t.ArraySet(es(0), es(1), es(2)) + ) + + case _ => super.deconstruct(expr) + } + + override def deconstruct(tpe: s.Type): Deconstructed[t.Type] = tpe match { + case s.RecordType(record) => ( + Seq(record), NoVariables, NoExpressions, NoTypes, NoFlags, + (recs, _, _, tps, _) => t.RecordType(recs.head) + ) + case _ => super.deconstruct(tpe) + } +} + +trait Deconstructors extends stainless.ast.Deconstructors { self: Trees => + // FIXME: What do I have to override here? + + override def getDeconstructor(that: inox.ast.Trees): inox.ast.TreeDeconstructor { val s: self.type; val t: that.type } = that match { + case tree: Trees => new TreeDeconstructor { + protected val s: self.type = self + protected val t: tree.type = tree + }.asInstanceOf[TreeDeconstructor { val s: self.type; val t: that.type }] + + case _ => super.getDeconstructor(that) + } + + override val deconstructor: TreeDeconstructor { val s: self.type; val t: self.type } = { + getDeconstructor(self).asInstanceOf[TreeDeconstructor { val s: self.type; val t: self.type }] + } +} diff --git a/core/src/main/scala/stainless/wasmgen/intermediate/Definitions.scala b/core/src/main/scala/stainless/wasmgen/intermediate/Definitions.scala new file mode 100644 index 0000000000..0de14a71b5 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/intermediate/Definitions.scala @@ -0,0 +1,112 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen.intermediate + +import stainless.{FreshIdentifier, Identifier} + +trait Definitions extends stainless.ast.Definitions { self: Trees => + override type Symbols >: Null <: AbstractSymbols + + trait AbstractSymbols extends super.AbstractSymbols { self0: Symbols => + val records: Map[Identifier, RecordSort] + val sorts: Map[Identifier, ADTSort] = Map() + + def lookupRecord(id: Identifier): Option[RecordSort] = records.get(id) + def getRecord(id: Identifier): RecordSort = records.getOrElse(id, throw ADTLookupException(id)) + } + + /** Tags dynamically called functions */ + case object Dynamic extends Flag("dynamic", Seq.empty) + + /** A record sort represents a sequence of named fields. + * A record sort may extend another record sort. + * A record contains all the parent's fields in order, + * followed by its own defined fields. + */ + class RecordSort( + val id: Identifier, + val parent: Option[Identifier], + val fields: Seq[ValDef], + val flags: Seq[Flag] = Seq() + ) extends Definition { + + def lookupParent(implicit s: Symbols): Option[RecordSort] = { + parent.map(s.getRecord) + } + def allFields(implicit s: Symbols): Seq[ValDef] = { + lookupParent.toSeq.flatMap(_.allFields) ++ fields + } + def ancestors(implicit s: Symbols): Seq[Identifier] = { + id +: lookupParent.toSeq.flatMap(_.ancestors) + } + def conformsWith(ancestor: Identifier)(implicit s: Symbols): Boolean = ancestors.contains(ancestor) + } + + private[wasmgen] val typeTagID = FreshIdentifier("typeTag") + private[wasmgen] val typeTag = ValDef(typeTagID, Int32Type()) + private[wasmgen] val funPointerId = FreshIdentifier("fPointer") + private[wasmgen] val boxedValueId = FreshIdentifier("value") + + /** Represents the top of the record hierarchy. It is the only record sort without a parent. + * Defines only one field, which represents the type-tag of the runtime value. + */ + object AnyRefSort extends RecordSort(FreshIdentifier("anyref"), None, Seq(typeTag), Seq()) + + private def prependParamType(tpe: Type, ft: FunctionType) = + FunctionType(tpe +: ft.from, ft.to) + + /** A record which defines a single field of a function type (function pointer). + * It is used as a base of all closures for this function type. + */ + sealed class FunPointerSort(id: Identifier, ft: FunctionType) + extends RecordSort( + id, + Some(AnyRefSort.id), + Seq(ValDef(funPointerId, prependParamType(RecordType(id), ft)))) + + /** Represents a closure, containing a function pointer plus the closure's environment + */ + sealed class ClosureSort(parent: Identifier, env: Seq[ValDef]) + extends RecordSort(FreshIdentifier("closure"), Some(parent), env) + + /** Represents a record sort corresponding to an ADT of a high-level language. + * This sort will never be instantiated at runtime. + */ + sealed class RecordADTSort(id: Identifier) + extends RecordSort(id, Some(AnyRefSort.id), Seq()) + + /** Represents a record sort corresponding to an ADT constructor of a high-level language. + * Defines a unique type tag which differentiates values of this constructor at runtime. + */ + sealed class ConstructorSort( + id: Identifier, + parent: Identifier, + val typeTag: Int, + fields: Seq[ValDef] + ) extends RecordSort(id, Some(parent), fields) + + /** Represents a box containing a value of an elementary (or array) type. + * Useful to implement boxing for high-level languages with parametric polymorphism. + */ + sealed class BoxedSort(tpe: Type) + extends RecordSort( + FreshIdentifier("Boxed" + tpe.asString(PrinterOptions())), + Some(AnyRefSort.id), + Seq(ValDef(boxedValueId, tpe))) + + def typeToTag(tpe: Type): Int = tpe match { + case UnitType() => 0 + case BooleanType() => 1 + case CharType() => 2 + case BVType(_, 32) => 3 + case BVType(_, 64) => 4 + case IntegerType() => 5 + case RealType() => 6 + case ArrayType(AnyRefType) => 7 + case StringType() => 8 + case FunctionType(_, _) => 9 + } + + val lastReservedTag: Int = typeToTag(FunctionType(Seq(), Untyped)) + +} diff --git a/core/src/main/scala/stainless/wasmgen/intermediate/ExprOps.scala b/core/src/main/scala/stainless/wasmgen/intermediate/ExprOps.scala new file mode 100644 index 0000000000..6ffc1187c1 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/intermediate/ExprOps.scala @@ -0,0 +1,7 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen.intermediate + +trait ExprOps extends stainless.ast.ExprOps { + +} diff --git a/core/src/main/scala/stainless/wasmgen/intermediate/Expressions.scala b/core/src/main/scala/stainless/wasmgen/intermediate/Expressions.scala new file mode 100644 index 0000000000..7b649145a6 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/intermediate/Expressions.scala @@ -0,0 +1,101 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen.intermediate + +import inox.ast.Identifier + +trait Expressions extends stainless.ast.Expressions { self: Trees => + + /** Represents a value of a record type at runtime. + * Has to be passed arguments for all fields, + * including those defined in ``tpe``s ancestors. + */ + sealed case class Record(tpe: RecordType, fields: Seq[Expr]) extends Expr with CachingTyped { + protected def computeType(implicit s: Symbols): Type = { + checkParamTypes(fields, tpe.getRecord.allFields, tpe) + } + } + + /** Select a field of a record by name */ + sealed case class RecordSelector(record: Expr, selector: Identifier) extends Expr with CachingTyped { + protected def computeType(implicit s: Symbols) = { + record.getType match { + case RecordType(id) => + s.getRecord(id).allFields + .find(_.id == selector) + .map(_.tpe).getOrElse(Untyped) + case _ => + Untyped + } + } + } + + /** Represents a function pointer. It is the only runtime value that can have a function type */ + sealed case class FunctionPointer(id: Identifier) extends Expr with CachingTyped { + protected def computeType(implicit s: Symbols): Type = { + s.lookupFunction(id) + .map(tfd => FunctionType(tfd.params.map(_.getType), tfd.getType)) + .getOrElse(Untyped) + } + } + + /** Cast an expression to a type lower in the type hierarchy. + * If the runtime value does not conform to the cast type, + * the program will fail. + */ + sealed case class CastDown(e: Expr, subtype: RecordType) extends Expr with CachingTyped { + protected def computeType(implicit s: Symbols): Type = { + e.getType match { + case supertype: RecordType if subtype conformsWith supertype => subtype + case _ => Untyped + } + } + } + + /** Cast an expression to a type higher in its type hierarchy. + * This will never fail at runtime (if it is well-typed). + */ + sealed case class CastUp(e: Expr, supertype: RecordType) extends Expr with CachingTyped { + protected def computeType(implicit s: Symbols): Type = e.getType match { + case subtype: RecordType if subtype conformsWith supertype => supertype + case _ => Untyped + } + } + + /** Print a message to the output */ + sealed case class Output(msg: Expr) extends Expr { + def getType(implicit s: Symbols) = { + msg.getType match { + case StringType() => UnitType() + case _ => Untyped + } + } + } + + /** Execute all expressions in 'es' one after the other. All but the last have to be of UnitType. + * If you are not sure that the requirement holds use [[Constructors.sequence]] + */ + sealed case class Sequence(es: Seq[Expr]) extends Expr { + require(es.size >= 2) + def getType(implicit s: Symbols) = { + checkParamTypes(es.init, List.fill(es.size - 1)(UnitType()), es.last.getType) + } + } + + sealed case class NewArray(length: Expr, init: Option[Expr]) extends Expr { + def getType(implicit s: Symbols) = + checkParamTypes( + Seq(length) ++ init.toSeq, + Seq(Int32Type()) ++ init.toSeq.map(_ => AnyRefType), + ArrayType(AnyRefType) + ) + } + + sealed case class ArraySet(array: Expr, index: Expr, value: Expr) extends Expr { + def getType(implicit s: Symbols) = (array.getType, index.getType, value.getType) match { + case (ArrayType(base1), Int32Type(), base2) if base1 == base2 => UnitType() + case _ => Untyped + } + } + +} diff --git a/core/src/main/scala/stainless/wasmgen/intermediate/Lowering.scala b/core/src/main/scala/stainless/wasmgen/intermediate/Lowering.scala new file mode 100644 index 0000000000..456a25650c --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/intermediate/Lowering.scala @@ -0,0 +1,696 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen +package intermediate + +import inox.Context +import stainless.ast.SymbolIdentifier +import stainless.{FreshIdentifier, Identifier} + +trait Lowerer extends stainless.transformers.Transformer { + val s = stainless.trees + val t = trees + + case class Env(syms: s.Symbols, manager: SymbolsManager, generateChecks: Boolean) + + protected val lib: LibProvider { val trees: s.type } = new LibProvider { + protected val trees: s.type = s + } + + override def transform(tp: s.Type, env: Env): t.Type = { + implicit val impSyms: s.Symbols = env.syms + import t._ + tp match { + case s.ADTType(id, tps) => + RecordType(id) + + case s.FunctionType(from, to) => + RecordType(env.manager.funPointerSort( + FunctionType(Seq.fill(from.size)(AnyRefType), AnyRefType) + )) + + case s.TupleType(bases) => + RecordType(lib.sort(s"Tuple${bases.size}").id) + case s.SetType(_) => + RecordType(lib.sort("Set").id) + case s.BagType(_) => + RecordType(lib.sort("Bag").id) + case s.MapType(_, _) => + RecordType(lib.sort("Map").id) + + case s.PiType(params, to) => + transform(s.FunctionType(params.map(_.getType), to.getType), env) + case s.SigmaType(params, to) => + transform(s.TupleType(params.map(_.getType) :+ to.getType), env) + case s.RefinementType(vd, prop) => + transform(vd.getType, env) + + case s.TypeParameter(id, flags) => // Type erasure + RecordType(AnyRefSort.id) + + case s.ArrayType(base) => + ArrayType(AnyRefType) + + case _ => + // Base types, functions and strings + super.transform(tp, env) + } + } +} + +private[wasmgen] class SymbolsManager { + import trees._ + import scala.collection.mutable.{Map => MMap} + + private val functions_ : MMap[Identifier, FunDef] = MMap() + private val records_ : MMap[Identifier, RecordSort] = MMap() + private val boxedSorts: MMap[Type, Identifier] = MMap() + private val funRecords: MMap[FunctionType, Identifier] = MMap() + + def addFunction(fd: FunDef): Unit = functions_ += fd.id -> fd + + def funPointerSort(ft: FunctionType): Identifier = + funRecords.getOrElseUpdate(ft, { + val fr = new FunPointerSort(FreshIdentifier("`" + ft.asString(PrinterOptions()) + "`"), ft) + records_ += fr.id -> fr + fr.id + }) + + def closureSort(funType: FunctionType, env: Seq[ValDef]): Identifier = { + // Always make a new closure sort + val cs = new ClosureSort(funPointerSort(funType), env) + records_ += cs.id -> cs + cs.id + } + + def boxedSort(tpe: Type): Identifier = boxedSorts.getOrElseUpdate(tpe, { + val s = new BoxedSort(tpe) + records_ += s.id -> s + s.id + }) + + def functions = functions_ + def records = records_ +} + + +private [wasmgen] class ExprLowerer( + manager: SymbolsManager, + sym0: stainless.trees.Symbols, + initSorts: Map[Identifier, trees.RecordSort], + context: Context +) extends Lowerer { + import t._ + def initEnv = Env(sym0, manager, true) + + private def isRecordType(tpe: t.Type) = tpe match { + case t.RecordType(_) => true + case _ => false + } + + private def maybeBox(e: s.Expr, expected: t.Type, env: Env): t.Expr = { + implicit val impSyms = env.syms + val trType = transform(e.getType, env) + val trE = transform(e, env) + if (!isRecordType(trType) && expected == AnyRefType) + CastUp( + Record( + RecordType(env.manager.boxedSort(trType)), + Seq(Int32Literal(typeToTag(trType)), trE)), + AnyRefType + ) + else if (trType == expected) trE + else CastUp(trE, AnyRefType) + } + private def maybeUnbox(e: t.Expr, real: t.Type, expected: t.Type, env: Env): t.Expr = { + implicit val impSyms = env.syms + if (!isRecordType(expected) && real == AnyRefType) + RecordSelector( + CastDown(e, RecordType(manager.boxedSort(expected))), + boxedValueId + ) + else if (real == expected) e + else CastDown(e, expected.asInstanceOf[RecordType]) + } + + def transform(fd: s.FunDef): t.FunDef = { + new t.FunDef( + transform(fd.id, initEnv), + Seq(), + fd.params map (transform(_, initEnv)), + transform(fd.returnType, initEnv), + transform(fd.fullBody, initEnv), + fd.flags map (transform(_, initEnv)) + ).copiedFrom(fd) + } + + override def transform(e: s.Expr, env: Env): Expr = { + implicit val impSyms = env.syms + val generateChecks = env.generateChecks + + def inBounds(array: t.Expr, index: t.Expr) = { + And( + GreaterEquals(index, Int32Literal(0)), + LessThan(index, ArrayLength(array)) + ) + } + + e match { + // Misc. + case s.Annotated(body, flags) if flags contains s.Unchecked => + // Unchecked flag suppresses checks + transform(body, env.copy(generateChecks = false)) + case s.Annotated(body, _) => + transform(body, env) + case s.Error(tpe, description) => + Sequence(Seq( + Output(transform(s.StringLiteral(description), env)), + NoTree(transform(tpe, env)) + )) + + // Contracts + case s.Assume(pred, body) => + if (generateChecks) + IfExpr(transform(pred, env), transform(body, env), NoTree(transform(body.getType, env))) + else + transform(body, env) + case s.Require(pred, body) => + transform(s.Assume(pred, body), env) + case s.Ensuring(body, s.Lambda(Seq(vd), lbody)) => + if (generateChecks) { + val trV = transform(vd, env) + Let(trV, transform(body, env), + IfExpr(transform(lbody, env), trV.toVariable, NoTree(trV.tpe)) + ) + } else { + transform(body, env) + } + case s.Assert(pred, error, body) => + if (generateChecks) + IfExpr( + transform(pred, env), + transform(body, env), + transform(s.Error(body.getType, error getOrElse ""), env) + ) + else transform(body, env) + + // Higher-order + case s.Application(callee, args) => + val tCallee = transform(callee, env) + val vCallee = Variable.fresh("fun", transform(callee.getType, env)) + // All arguments are passed to lambdas and result is returned as anyref + Let(vCallee.toVal, tCallee, + maybeUnbox(Application( + RecordSelector(vCallee, funPointerId), + vCallee +: args.map( arg => maybeBox(arg, AnyRefType, env)) + ), AnyRefType, transform(e.getType, env), env) + ) + case s.Lambda(params, body) => + val boxedFunType = FunctionType( + Seq.fill(params.size)(AnyRefType), + AnyRefType + ) + val fv = (s.exprOps.variablesOf(body).map(_.toVal) -- params).toSeq.map(transform(_, env)) + + // Make/find a RecordSort for this function type, and one with the specific env. + val funRecId = manager.funPointerSort(boxedFunType) + + val freshEnv = fv.map(_.freshen) + val closureSortId = manager.closureSort(boxedFunType, freshEnv) + + val funRecordType = RecordType(funRecId) + val closureType = RecordType(closureSortId) + + val function = { + def extractEnv(env: Variable, body: Expr) = { + val castEnv = ValDef.fresh("env", closureType) + Let( + castEnv, + CastDown(env, closureType), + fv.zip(freshEnv).foldRight(body) { case ((v, envId), rest) => + Let(v, RecordSelector(castEnv.toVariable, envId.id), rest) + } + ) + } + + def unboxParams(boxedParams: Seq[ValDef], body: Expr) = { + boxedParams.zip(params).foldRight(body) { case ((boxed, unboxed), rest) => + Let(transform(unboxed, env), + maybeUnbox(boxed.toVariable, AnyRefType, transform(unboxed.getType, env), env), + rest + ) + } + } + + def boxResult(body: s.Expr) = maybeBox(body, AnyRefType, env) + + val fd = { + val envParam = ValDef.fresh("env", funRecordType) + val boxedParams = params map (p => ValDef(p.id.freshen, AnyRefType)) + new FunDef( + FreshIdentifier("lambda"), Seq(), + envParam +: boxedParams, + AnyRefType, + extractEnv( + envParam.toVariable, + unboxParams( + boxedParams, + boxResult(body))), + Seq(Dynamic) + ) + } + + manager.addFunction(fd) + fd + } + + val closure = { + CastUp( + Record( + closureType, + Int32Literal(typeToTag(boxedFunType)) +: FunctionPointer(function.id) +: fv.map(_.toVariable) + ), + funRecordType + ) + } + + closure + + // Booleans + case s.Implies(lhs, rhs) => transform(s.Or(lhs, s.Not(rhs)), env) + + // ADTs + case me: s.MatchExpr => + transform(impSyms.matchToIfThenElse(me, assumeExhaustive = !generateChecks), env) + case adt@s.ADT(id, tps, args) => + // Except constructor fields, we also store the i32 tag corresponding to this constructor + val typeTag = initSorts(id).asInstanceOf[ConstructorSort].typeTag + val formals = sym0.constructors(id).fields.map(_.getType) + val tpe = RecordType(id) + val parentType = RecordType(sym0.constructors(id).sort) + val invariant = adt.getConstructor.sort.invariant + val withoutInv = CastUp( + Record(tpe, Int32Literal(typeTag) +: args.zip(formals).map { + case (arg, formal) => maybeBox(arg, transform(formal, env), env) + }), + parentType + ) + invariant match { + case Some(inv) if generateChecks => + val binder = ValDef(FreshIdentifier(id.name.toLowerCase), parentType) + Let( + binder, withoutInv, + IfExpr( + FunctionInvocation(inv.id, Seq(), Seq(binder.toVariable)), + binder.toVariable, + transform(s.Error(adt.getType, s"Error: Invariant failed for ${adt.getConstructor.sort.id}"), env)) + ) + case _ => + withoutInv + } + case s.IsConstructor(expr, id) => + // We need to compare the constructor code of given value + // to the code corresponding to constructor 'id' + Equals( + RecordSelector(transform(expr, env), typeTagID), + Int32Literal(initSorts(id).asInstanceOf[ConstructorSort].typeTag) + ) + case as@s.ADTSelector(adt, selector) => + val s.ADTType(parent, _) = adt.getType + val (childId, formalType) = (for { + ch <- initSorts.values + if ch.parent.contains(parent) + fd <- ch.fields + if fd.id == selector + } yield (ch.id, fd.tpe)).head + if (generateChecks) { + val binder = ValDef(FreshIdentifier(childId.name.toLowerCase), RecordType(parent)) + Let(binder, transform(adt, env), + IfExpr( + Equals( + RecordSelector(binder.toVariable, typeTagID), + Int32Literal(initSorts(childId).asInstanceOf[ConstructorSort].typeTag) + ), + maybeUnbox( + RecordSelector( + CastDown(binder.toVariable, RecordType(childId)), + selector + ), + formalType, + transform(as.getType, env), + env + ), + transform(s.Error(as.getType, s"Error: Cannot cast to ${childId.name}"), env) ) ) + } else { + maybeUnbox( + RecordSelector( + CastDown(transform(adt, env), RecordType(childId)), + selector + ), + formalType, + transform(as.getType, env), + env + ) + } + + case s.FunctionInvocation(id, tps, args) => + val formals = sym0.functions(id).params.map(_.getType) + maybeUnbox( + FunctionInvocation(id, Seq(), + args zip formals map { case (arg, formal) => + maybeBox(arg, transform(formal, env), env) + } + ), + transform(sym0.functions(id).returnType, env), + transform(e.getType, env), + env + ) + + // Arrays + case s.FiniteArray(elems, base) => + val arr = Variable.fresh("array", ArrayType(AnyRefType)) + Let(arr.toVal, + NewArray(Int32Literal(elems.length), None), + sequence(elems.zipWithIndex.map { case (elem, index) => + ArraySet(arr, Int32Literal(index), maybeBox(elem, AnyRefType, env)) + } :+ arr) + ) + case s.LargeArray(elems, default, size, base) => + val arr = Variable.fresh("array", ArrayType(AnyRefType)) + Let(arr.toVal, + NewArray(transform(size, env), Some(maybeBox(default, AnyRefType, env))), + sequence( elems.toSeq.sortBy(_._1).map { case (index, elem) => + ArraySet(arr, Int32Literal(index), maybeBox(elem, AnyRefType, env)) + } :+ arr) + ) + case s.ArrayUpdated(array, index, value) => + // TODO: Copy functional arrays or analyze when we don't need to do so + val arr = Variable.fresh("array", ArrayType(AnyRefType)) + if (generateChecks) { + val ind = Variable.fresh("index", Int32Type()) + Let(arr.toVal, transform(array, env), + Let(ind.toVal, transform(index, env), + IfExpr( + inBounds(arr, ind), + Sequence(Seq( + ArraySet(arr, ind, maybeBox(value, AnyRefType, env)), + arr + )), + transform(s.Error(array.getType, "Error: Array out of bounds"), env) ))) + } else { + Let(arr.toVal, transform(array, env), + Sequence(Seq( + ArraySet(arr, transform(index, env), maybeBox(value, AnyRefType, env)), + arr + ))) + } + case s.ArraySelect(array, index) => + if (generateChecks) { + val arr = Variable.fresh("array", ArrayType(AnyRefType)) + val ind = Variable.fresh("index", Int32Type()) + Let(arr.toVal, transform(array, env), + Let(ind.toVal, transform(index, env), + IfExpr( + inBounds(arr, ind), + maybeUnbox( + ArraySelect(arr, ind), + AnyRefType, + transform(e.getType, env), + env ), + transform(s.Error(e.getType, "Error: Array out of bounds"), env) ))) + } else { + maybeUnbox( + ArraySelect(transform(array, env), transform(index, env)), + AnyRefType, + transform(e.getType, env), + env + ) + } + + // Tuples + case s.Tuple(exprs) => + transform(s.ADT( + lib.sort(s"Tuple${exprs.size}").constructors.head.id, + exprs map (_.getType), + exprs + ), env) + case s.TupleSelect(tuple, index) => + val size = tuple.getType.asInstanceOf[s.TupleType].bases.size + val constr = lib.sort(s"Tuple$size").constructors.head + val selector = constr.fields(index - 1).id + maybeUnbox( + RecordSelector(CastDown(transform(tuple, env), RecordType(constr.id)), selector), + AnyRefType, + transform(e.getType, env), + env + ) + + // Sets + case s.FiniteSet(Seq(), base) => + val empty = s.ADT( + lib.sort("Set").constructors.find(_.id.name == "SNil").get.id, + Seq(base), + Seq() + ) + transform(empty, env) + case s.FiniteSet(elements, base) => + transform( + elements.foldLeft[s.Expr](s.FiniteSet(Seq(), base)){ (rest, elem) => + s.SetAdd(rest, elem) + }, + env ) + case s.SetAdd(set, elem) => + FunctionInvocation( + lib.fun("setAdd").id, Seq(), + Seq(transform(set, env), maybeBox(elem, AnyRefType, env)) + ) + case s.ElementOfSet(element, set) => + FunctionInvocation( + lib.fun("elementOfSet").id, Seq(), + Seq(transform(set, env), maybeBox(element, AnyRefType, env)) + ) + case s.SubsetOf(lhs, rhs) => + FunctionInvocation( + lib.fun("subsetOf").id, Seq(), + Seq(transform(lhs, env), transform(rhs, env)) + ) + case s.SetIntersection(lhs, rhs) => + FunctionInvocation( + lib.fun("setIntersection").id, Seq(), + Seq(transform(lhs, env), transform(rhs, env)) + ) + case s.SetUnion(lhs, rhs) => + FunctionInvocation( + lib.fun("setUnion").id, Seq(), + Seq(transform(lhs, env), transform(rhs, env)) + ) + case s.SetDifference(lhs, rhs) => + FunctionInvocation( + lib.fun("setDifference").id, Seq(), + Seq(transform(lhs, env), transform(rhs, env)) + ) + + // Bags + case s.FiniteBag(elements, base) => + val empty = s.ADT( + lib.sort("Bag").constructors.find(_.id.name == "BNil").get.id, + Seq(base), + Seq() + ) + elements.foldLeft[Expr](transform(empty, env)) { + case (rest, (elem, mult)) => + FunctionInvocation( + lib.fun("bagAdd").id, Seq(), + Seq(rest, maybeBox(elem, AnyRefType, env), transform(mult, env)) + ) + } + case s.BagAdd(bag, elem) => + FunctionInvocation( + lib.fun("bagAdd").id, Seq(), + Seq( + transform(bag, env), + maybeBox(elem, AnyRefType, env), + transform(s.IntegerLiteral(BigInt(1)), env) + ) + ) + case s.MultiplicityInBag(element, bag) => + FunctionInvocation( + lib.fun("bagMultiplicity").id, Seq(), + Seq(transform(bag, env), maybeBox(element, AnyRefType, env)) + ) + case s.BagIntersection(lhs, rhs) => + FunctionInvocation( + lib.fun("bagIntersection").id, Seq(), + Seq(transform(lhs, env), transform(rhs, env)) + ) + case s.BagUnion(lhs, rhs) => + FunctionInvocation( + lib.fun("bagUnion").id, Seq(), + Seq(transform(lhs, env), transform(rhs, env)) + ) + case s.BagDifference(lhs, rhs) => + FunctionInvocation( + lib.fun("bagDifference").id, Seq(), + Seq(transform(lhs, env), transform(rhs, env)) + ) + + // Maps FIXME maps are wrong + case s.FiniteMap(Seq(), default, keyType, valueType) => + val empty = s.ADT( + lib.sort("Map").constructors.find(_.id.name == "MNil").get.id, + Seq(keyType, valueType), + Seq(default) + ) + transform(empty, env) + case s.FiniteMap(pairs, default, keyType, valueType) => + val empty = s.FiniteMap(Seq(), default, keyType, valueType) + transform( + pairs.foldLeft[s.Expr](empty) { case (rest, (key, value)) => + s.MapUpdated(rest, key, value) + }, + env + ) + case s.MapApply(map, key) => + FunctionInvocation( + lib.fun("mapApply").id, Seq(), + Seq(transform(map, env), maybeBox(key, AnyRefType, env)) + ) + case s.MapUpdated(map, key, value) => + FunctionInvocation( + lib.fun("mapUpdated").id, Seq(), + Seq(transform(map, env), maybeBox(key, AnyRefType, env), maybeBox(value, AnyRefType, env)) + ) + + // We do not translate these for now + case s.Forall(_, _) + | s.Choose(_, _) + | s.GenericValue(_, _) => + context.reporter.fatalError( + s"Cannot translate expression " + + e.asString(s.PrinterOptions.fromContext(context, Some(env.syms))) + + " to WebAssembly." + ) + + case _ => + // Let, Variable, IfExpr, NoTree + // other literals + // string, boolean, arithmetic operations + // ArrayLength + super.transform(e, env) + } + } +} + + +/** Lowers stainless trees to the language defined in [[stainless.wasmgen.intermediate]] + * + * The following changes take place: + * - Arrays become mutable + * - Composite types become "records", which are extensible structs in memory. See [[Definitions.RecordSort]] + * - Polymorphic types are erased and polymorphic values are boxed. + * - Maps, Bags and Sets become records based on a library implemented in stainless + * + * Limitations: + * - BigInts are approximated by Longs + * - Reals are not translated (later are approximated as Doubles) + * - ArrayUpdated does not copy, rather it does a destructive update + */ +class Lowering(context: Context) extends inox.transformers.SymbolTransformer with Lowerer { + private val sortCodes = new inox.utils.UniqueCounter[Unit] + locally { + // We want to reserve the first codes for native types + for {_ <- 0 to trees.lastReservedTag} sortCodes.nextGlobal + } + + def transform(sort: s.ADTSort, env: Env): Seq[t.RecordSort] = { + val eqId = FreshIdentifier(s"eq${sort.id.name}") + + val parent = new t.RecordADTSort(transform(sort.id, env)).copiedFrom(sort) + + val children = sort.constructors map { cons => + new t.ConstructorSort( + transform(cons.id, env), + parent.id, + sortCodes.nextGlobal, + cons.fields.map(transform(_, env)) + ).copiedFrom(cons) + } + + parent +: children + } + + private def mkToString(constr: s.ADTConstructor)(implicit sym: s.Symbols): s.FunDef = { + import s._ + val dsl = new inox.ast.DSL { val trees = s } + val sort = sym.sorts(constr.sort) + // Make toString functions searchable in the wasm runtime library + val funName = SymbolIdentifier(LibProvider.libPath + constr.id.uniqueName + "ToString") + dsl.mkFunDef(funName)(sort.tparams.map(_.id.name): _*){ tps => + (Seq(ValDef(FreshIdentifier("v"), ADTType(sort.id, tps))), StringType(), { + case Seq(arg) => + val fields = constr.typed(tps).fields + val name = if (sort.id.name matches "Tuple\\d{1,2}") "" else constr.id.name + if (fields.isEmpty) StringLiteral(name + "()") + else ( + StringLiteral(name + "(") +: + fields.zipWithIndex.flatMap { case (f, ind) => + val fieldStr = FunctionInvocation( + lib.fun("toString").id, + Seq(f.getType), + Seq(Annotated(ADTSelector(arg, f.id), Seq(Unchecked)))) + if (ind == fields.size - 1) Seq(fieldStr) + else Seq(fieldStr, StringLiteral(", ")) + } :+ + StringLiteral(")") + ).reduceLeft(StringConcat) + }) + } + } + + def transform(syms0: s.Symbols): t.Symbols = { + + // (0) Make toString's + val toStrings = { + val hasBuiltinToString = Set("SCons", "SNil", "MCons", "MNil", "BCons", "BNil") + syms0.sorts.toSeq.flatMap(_._2.constructors).filterNot( constr => + hasBuiltinToString contains constr.id.name + ).map(mkToString(_)(syms0)) + } + val syms = syms0.withFunctions(toStrings) + + // (1) Transform sorts, make them to starting symbols + val manager = new SymbolsManager + val env0 = Env(syms, manager, generateChecks = true) + val initSymbols = t.NoSymbols.withRecords(syms.sorts.values.toSeq.flatMap(transform(_, env0))) + + // (2) Transform functions in program + val tr = new ExprLowerer(manager, syms, initSymbols.records, context) + val funs = (syms.functions mapValues tr.transform).view.force + + // (3) Put it all together + val ret0 = t.Symbols( + initSymbols.records ++ manager.records + (t.AnyRefSort.id -> t.AnyRefSort), + funs ++ manager.functions + ) + + // (4) Simplify function bodies (mainly to eliminate excessive variable definitions...) + val simplifier = ret0.simplifier(inox.solvers.PurityOptions(context)) + val ret = t.Symbols( + ret0.records, + ret0.functions.mapValues{ fd => + fd.copy(fullBody = simplifier.transform(fd.fullBody, simplifier.initEnv)) + }.view.force + ) + + //Debugging + //implicit val printerOptions0 = s.PrinterOptions(printUniqueIds = true) + //syms0.functions foreach (r => println(r._2.asString)) + //implicit val printerOptions = t.PrinterOptions(printUniqueIds = true) + //ret.records foreach (r => println(r._2.asString)) + //ret.functions foreach (r => println(r._2.asString)) + //ret.functions.foreach(fn => println(ret.explainTyping(fn._2.fullBody))) + + ret + } +} + diff --git a/core/src/main/scala/stainless/wasmgen/intermediate/Printer.scala b/core/src/main/scala/stainless/wasmgen/intermediate/Printer.scala new file mode 100644 index 0000000000..04c27a1f02 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/intermediate/Printer.scala @@ -0,0 +1,47 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen.intermediate + +trait Printer extends stainless.ast.Printer { + protected val trees: Trees + import trees._ + override protected def ppBody(tree: Tree)(implicit ctx: PrinterContext): Unit = tree match { + case bvl: BVLiteral => ppBody(IntegerLiteral(bvl.toBigInt)) + + case Record(tpe, fields) => p"new $tpe($fields)" + + case RecordSelector(record, selector) => p"$record.$selector" + + case FunctionPointer(id) => p"$id" + + case CastDown(e, tp) => p"$e.asInstanceOf[$tp]" + + case CastUp(e, tp) => p"$e.asInstanceOf[$tp]" + + case Sequence(Seq(e1, e2)) => + p"""|$e1; + |$e2""" + + case Sequence(more) => + p"""|${more.head}; + |""" + ppBody(Sequence(more.tail)) + + case Output(msg) => p"println($msg)" + + case NewArray(length, init) => p"new Array($length){ ${init.getOrElse("")} }" + + case ArraySet(array, index, value) => + p"$array($index) = $value" + + case RecordType(id) => + p"$id" + + case rs: RecordSort => + p"struct ${rs.id} " + rs.parent foreach { par => p"extends $par " } + p"${nary(rs.fields, ", ", "(", ")")}" + + case _ => super.ppBody(tree) + } +} \ No newline at end of file diff --git a/core/src/main/scala/stainless/wasmgen/intermediate/SymbolOps.scala b/core/src/main/scala/stainless/wasmgen/intermediate/SymbolOps.scala new file mode 100644 index 0000000000..30df2d29d4 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/intermediate/SymbolOps.scala @@ -0,0 +1,17 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless +package wasmgen +package intermediate + +trait SymbolOps extends ast.SymbolOps { self: TypeOps => + import trees._ + + override def isImpureExpr(expr: Expr): Boolean = expr match { + case Record(_, _) | RecordSelector(_, _) | FunctionPointer(_) + | CastUp(_, _) | Sequence(_) | NewArray(_, _) => false + case CastDown(_, _) | Output(_) | ArraySet(_, _, _) => true + case other => super.isImpureExpr(other) + } + +} diff --git a/core/src/main/scala/stainless/wasmgen/intermediate/Transformer.scala b/core/src/main/scala/stainless/wasmgen/intermediate/Transformer.scala new file mode 100644 index 0000000000..999e57e068 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/intermediate/Transformer.scala @@ -0,0 +1,6 @@ +package stainless.wasmgen.intermediate + +trait Transformer extends stainless.transformers.Transformer { + val s: Trees + val t: Trees +} diff --git a/core/src/main/scala/stainless/wasmgen/intermediate/TreeOps.scala b/core/src/main/scala/stainless/wasmgen/intermediate/TreeOps.scala new file mode 100644 index 0000000000..be2bdde676 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/intermediate/TreeOps.scala @@ -0,0 +1,7 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen.intermediate + +trait TreeOps extends stainless.ast.TreeOps { self: Trees => + +} diff --git a/core/src/main/scala/stainless/wasmgen/intermediate/Trees.scala b/core/src/main/scala/stainless/wasmgen/intermediate/Trees.scala new file mode 100644 index 0000000000..22cb6809c7 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/intermediate/Trees.scala @@ -0,0 +1,19 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen.intermediate + +trait Trees + extends stainless.ast.Trees + with Definitions + with Expressions + with Types + with Constructors + with Deconstructors + with TreeOps { self => + + override val exprOps: ExprOps { val trees: Trees.this.type } = new { + protected val trees: Trees.this.type = Trees.this + } with ExprOps + + val printer: Printer { val trees: self.type } +} diff --git a/core/src/main/scala/stainless/wasmgen/intermediate/TypeOps.scala b/core/src/main/scala/stainless/wasmgen/intermediate/TypeOps.scala new file mode 100644 index 0000000000..31a637f3c3 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/intermediate/TypeOps.scala @@ -0,0 +1,6 @@ +package stainless +package wasmgen.intermediate + +trait TypeOps extends ast.TypeOps { + val trees: Trees +} diff --git a/core/src/main/scala/stainless/wasmgen/intermediate/Types.scala b/core/src/main/scala/stainless/wasmgen/intermediate/Types.scala new file mode 100644 index 0000000000..590e91012c --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/intermediate/Types.scala @@ -0,0 +1,30 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen.intermediate + +import inox.ast.Identifier + +trait Types extends inox.ast.Types { self: Trees => + /** A record type identified by the Identifier given as argument */ + sealed case class RecordType(record: Identifier) extends Type { + def lookupRecord(implicit s: Symbols): Option[RecordSort] = s.lookupRecord(record) + + def getRecord(implicit s: Symbols): RecordSort = s.getRecord(record) + + def parent(implicit s: Symbols): Option[RecordType] = { + s.getRecord(record).parent.map(RecordType) + } + + def conformsWith(superType: Type)(implicit s: Symbols): Boolean = superType match { + case RecordType(record2) => + getRecord.ancestors contains record2 + case _ => false + } + } + + /** The top of the record type hierarchy, corresponding to + * [[trees.AnyRefSort]] + */ + val AnyRefType = RecordType(AnyRefSort.id) + +} diff --git a/core/src/main/scala/stainless/wasmgen/intermediate/package.scala b/core/src/main/scala/stainless/wasmgen/intermediate/package.scala new file mode 100644 index 0000000000..ea62799719 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/intermediate/package.scala @@ -0,0 +1,137 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen + +import inox.ast.Identifier + +/** Defines a language, 'reclang', that functions as an intermediate language between stainless trees and wasm code. + * + * The main feature of reclang is that its structured types are extensible record, + * which are meant to be easily translatable both to the current memory model of wasm (linear memory) + * and the planned future extension of reference types. + * The class [[stainless.wasmgen.intermediate.Lowering]] + * is responsible for the lowering to this intermediate language. + * + * We now give an informal overview of reclang. + * In the following grammars, nonterminal symbols are given in single quotes('), + * and terminal symbols without quotes. + * + * The types of reclang are defined as follows: + * + * 'type' ::= Boolean | Char | Int | Long | Unit | Double | String | Array | ('type'*) => 'type' | 'id' + * + * where id refers to the name of a record sort defined in the program. + * There is no type polymorphism, including arrays, which always contain boxed values. + * + * A record sort is defined as follows: + * + * 'sort' ::= struct 'id' ('field'*) [extends 'id']? + * 'field' ::= 'id' : 'type' + * + * There is a single sort, called "anyref", that does not have a parent: + * struct anyref (typeTag: Int) + * anyref has a single field which represents the type tag of a given runtime value. + * anyref is the root of the record hierarchy. All other records have a parent. + * There is no subtyping in reclang, + * but there are operators which can cast one record to another, + * provided they are connected with the ancestor (transitive reflexive closure of parent) relation. + * + * At runtime, a record's representation contains a list of values + * corresponding to the fields it defines as well as all fields that its ancestors define. + * The order of fields is from the further ancestor until the current field type. + * + * The expressions of reclang are given below: + * + * 'e' ::= error | 'id' // variable, or pointer to a named function + * | val 'id' = 'e'; 'e' | println('e') + * | 'id'('e'*) // function invocation + * | 'e'; 'e' | if ('e') 'e' else 'e' | 'e' == 'e' + * | 'intconst' | 'doubleconst' | 'charconst' | 'stingliteral' + * | true | false | () + * | 'id'({'e' {, 'e'}*}?) // record constructor + * | 'e'.'id' // record field selector + * | 'e'({'e' {, 'e'}*}?) // higher-order application + * | 'e'.asInstanceOf['id'] + * + * | new Array['type']('e'{, 'e'}?) // length, optional initializer + * | 'e'('e') // array select + * | 'e'('e') = 'e' // array set + * | 'e'.length // array or string length + * | 'e'.substing('e', 'e') // string operations + * + * | 'e' 'binop' 'e' + * | ! 'e' + * + * 'binop' ::= + | - | * | / | mod | remainder + * | < | > | <= | >= | & | "|" + * | ^ | << | >> | >>> + * | (bitvector casts) + * | "||" | && | concat + * + * + * The notable typing rules are for records: + * a record constructor takes as arguments expressions of the types of + * the fields of all the ancestors of the current type. + * Also, a selector is allowed with the name of a field of an ancestor. + * Casts have to be between compatible record types, i.e., + * that are related by the ancestor relation. + * An upcast is always successful. + * A downcast to an incompatible type fails the program. + * + * The only values that can have a function type in reclang are function pointers. + * Fucntions are represented by closures, + * i.e., records containing a function pointer + * and the environment captured by the function. + * + * Polymorphism is implemented with type erasure and boxing. + * There are boxed versions of the elementary types + * (which are regular record types). + * Boxed types are records containing one additional field named "value" + * of the corresponding type. + * + * The typetag field + * (which is defined in anyref, therefore is present in every record) + * defines the type of a record value at runtime as follows: + * 0 for boxed Unit, + * 1 for boxed Boolean, + * 2 for boxed Char, + * 3 for boxed Int, + * 4 for boxed Long, + * 5 for boxed Float, + * 6 for boxed Double, + * 7 for boxed Array, + * 8 for boxed String, + * 9 for closure, + * and then as many tags as are needed for record sorts + * that are instantiated in the program. + * We differentiate between records which correspond to abstract types + * (cannot be instantiated, do not possess a tag) + * and records which correspond to constructors + * (can be instantiated, possess a tag). + * + * Two record values are equal if their type tags are equal + * and all fields defined by their tagged type are equal. + * Arrays, functions and strings are compared by reference. + * All other types are compared by value. + */ +package object intermediate { + object trees extends Trees { self => + object printer extends Printer { + val trees: self.type = self + } + case class Symbols( + records: Map[Identifier, RecordSort], + functions: Map[Identifier, FunDef] + ) extends AbstractSymbols { + def withFunctions(functions: Seq[FunDef]): Symbols = + Symbols(this.records, this.functions ++ functions.map(fd => fd.id -> fd)) + + def withSorts(sorts: Seq[ADTSort]): Symbols = this + + def withRecords(records: Seq[RecordSort]): Symbols = + Symbols(this.records ++ records.map(rec => rec.id -> rec), this.functions) + } + val NoSymbols: Symbols = Symbols(Map(), Map()) + } + +} diff --git a/core/src/main/scala/stainless/wasmgen/package.scala b/core/src/main/scala/stainless/wasmgen/package.scala new file mode 100644 index 0000000000..124052f46d --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/package.scala @@ -0,0 +1,24 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless + +/** Provides code to translate stainless ASTs to WebAssembly code. + * + * The strategy followed is to first translate to an intermediate language + * which extends stainless trees (see [[stainless.wasmgen.intermediate]]) + * and then generate WebAssembly. + * + * A partial modelling of the WebAssembly language is provided under + * [[stainless.wasmgen.wasm]]. + * + * The translation from intermediate trees to WebAssembly is under [[stainless.wasmgen.codegen]]. + * The current implementation uses linear memory to implement heap operations, + * but it is designed to easily incorporate reference types once they become available. + * See [[stainless.wasmgen.codegen.CodeGeneration]]. + * + * Current limitations: + * * BigInts and Reals are represented as i64 and f64 respectively. + * * Forall and Choose are not implemented. + * * Maps, Sets and Bags have very basic and computationally inefficient implementations. + */ +package object wasmgen \ No newline at end of file diff --git a/core/src/main/scala/stainless/wasmgen/wasm/Definitions.scala b/core/src/main/scala/stainless/wasmgen/wasm/Definitions.scala new file mode 100644 index 0000000000..b4c4074708 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/wasm/Definitions.scala @@ -0,0 +1,60 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen.wasm + +import Expressions.{Expr, Const} +import Types.Type + +/** Definitions for wasm programs */ +object Definitions { + + case class ValDef(name: Label, tpe: Type) + + case class Global(name: Label, isMutable: Boolean, private var init_ : Const) { + val tpe = init_.getType + val toVal = ValDef(name, tpe) + def update(c: Const) = { + require(c.getType == tpe) + init_ = c + } + def init = init_ + } + + case class FunDef private + (name: String, args: Seq[ValDef], returnType: Type, locals: Seq[ValDef], body: Expr) + { + override def toString: String = Printer(this) + } + + object FunDef { + /** Construct a [[FunDef]] + * + * @param codeGen A function from a [[LocalsHandler]], + * which is instantiated by this constructor with the function arguments, + * to the body of the function + */ + def apply(name: String, args: Seq[ValDef], returnType: Type)(codeGen: LocalsHandler => Expr): FunDef = { + val lh = new LocalsHandler(args) + // Make code first, as it may increment the locals in lh + val body = codeGen(lh) + FunDef(name, args, returnType, lh.locals, body) + } + } + + case class Import(extModule: Label, name: Label, tpe: ImportType) + + abstract class ImportType + case class FunSig(name: Label, args: Seq[Type], returnType: Type) extends ImportType + case class Memory(size: Int) extends ImportType + + case class Table(funs: Seq[Label]) { + def indexOf(fun: Label) = funs.indexOf(fun) + } + + case class FormattedByte(byte: Byte, formatted: Boolean) + implicit class FormatByte(byte: Byte) { + def f = FormattedByte(byte, true) + def r = FormattedByte(byte, false) + } + case class Data(offset: Int, bytes: Seq[FormattedByte]) +} diff --git a/core/src/main/scala/stainless/wasmgen/wasm/Document.scala b/core/src/main/scala/stainless/wasmgen/wasm/Document.scala new file mode 100644 index 0000000000..97496119d9 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/wasm/Document.scala @@ -0,0 +1,47 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen.wasm + +// A structured document to be printed with nice indentation +abstract class Document { + + def <:>(other: Document) = Lined(Seq(this, other)) + + def print: String = { + val sb = new StringBuffer() + + def rec(d: Document)(implicit ind: Int, first: Boolean): Unit = d match { + case Raw(s) => + if (first && s.nonEmpty) sb append (" " * ind) + sb append s + case Indented(doc) => + rec(doc)(ind + 1, first) + case Lined(Nil, _) => // skip + case Lined(docs, sep) => + rec(docs.head) + docs.tail foreach { doc => + rec(sep)(ind, false) + rec(doc)(ind, false) + } + case Stacked(Nil, _) => // skip + case Stacked(docs, emptyLines) => + rec(docs.head) + docs.tail foreach { doc => + sb append "\n" + if (emptyLines) sb append "\n" + rec(doc)(ind, true) + } + } + + rec(this)(0, true) + sb.toString + } +} +case class Indented(content: Document) extends Document +case class Stacked(docs: Seq[Document], emptyLines: Boolean = false) extends Document +case class Lined(docs: Seq[Document], separator: Document = Raw("")) extends Document +case class Raw(s: String) extends Document + +object Stacked { + def apply(docs: Document*): Stacked = Stacked(docs.toSeq) +} \ No newline at end of file diff --git a/core/src/main/scala/stainless/wasmgen/wasm/Expressions.scala b/core/src/main/scala/stainless/wasmgen/wasm/Expressions.scala new file mode 100644 index 0000000000..d72ba07799 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/wasm/Expressions.scala @@ -0,0 +1,200 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless +package wasmgen +package wasm + +import scala.language.implicitConversions +import Types._ + +// A subset of instructions defined by the WASM standard +object Expressions { self => + + abstract class Sign + case object Signed extends Sign { override def toString = "s" } + case object Unsigned extends Sign { override def toString = "u" } + + trait RelOp + trait SignedOp { + val sign: Sign + private val name = getClass.getSimpleName + + override def toString = s"${name}_$sign" + } + + abstract class UnOp { + def apply(e1: Expr) = Unary(this, e1) + } + // Int only + case object eqz extends UnOp with RelOp // Return 1 if operand is 0, 0 otherwise + // TODO: Add the rest + // Float only + case object neg extends UnOp with RelOp + // TODO: ADD the rest + + + + abstract class BinOp { + def apply(e1: Expr, e2: Expr) = Binary(this, e1, e2) + } + + // mk: This is a little hacky since we use the same names for multiple operations but oh well + // Int and float instructions + case object add extends BinOp + case object sub extends BinOp + case object mul extends BinOp + case object eq extends BinOp with RelOp + case object ne extends BinOp with RelOp + // Int only + case class div(sign: Sign) extends BinOp with SignedOp + case class rem(sign: Sign) extends BinOp with SignedOp + case object and extends BinOp + case object or extends BinOp + case object xor extends BinOp + case object shl extends BinOp + case class shr(sign: Sign) extends BinOp with SignedOp + case object rotl extends BinOp + case object rotr extends BinOp + case class lt(sign: Sign) extends BinOp with SignedOp with RelOp + case class le(sign: Sign) extends BinOp with SignedOp with RelOp + case class gt(sign: Sign) extends BinOp with SignedOp with RelOp + case class ge(sign: Sign) extends BinOp with SignedOp with RelOp + // float only + case object div extends BinOp + case object min extends BinOp + case object max extends BinOp + case object copysign extends BinOp + case object lt extends BinOp with RelOp + case object le extends BinOp with RelOp + case object gt extends BinOp with RelOp + case object ge extends BinOp with RelOp + + abstract class Expr { val getType: Type } + + // Operators + case class Binary(op: BinOp, lhs: Expr, rhs: Expr) extends Expr { + val getType = op match { + case _: RelOp => i32 + case _ => lhs.getType + } + } + case class Unary(op: UnOp, expr: Expr) extends Expr { + val getType = op match { + case _: RelOp => i32 + case _ => expr.getType + } + } + + // Conversions + case class Extend(to: Type, sign: Sign, e: Expr) extends Expr { + val getType = to + } + case class Wrap(to: Type, e: Expr) extends Expr { + val getType = to + } + case class Truncate(to: Type, sign: Sign, e: Expr) extends Expr { + val getType = to + } + + // Constants + trait Const extends Expr + case class I32Const(value: Int) extends Expr with Const { val getType = i32 } + case class I64Const(value: Long) extends Expr with Const { val getType = i64 } + case class F32Const(value: Float) extends Expr with Const { val getType = f32 } + case class F64Const(value: Double) extends Expr with Const { val getType = f64 } + + // Control instructions + case class If(label: Label, cond: Expr, thenn: Expr, elze: Expr) extends Expr { + val getType = thenn.getType + } + // A block of instructions with a label at the beginning + case class Loop(label: Label, body: Expr) extends Expr { + val getType = body.getType + } + // A block of instructions with a label at the end + case class Block(label: Label, body: Expr) extends Expr { + val getType = body.getType + } + // Jump to "label", which MUST be the label of an enclosing structure + case class Br(label: Label) extends Expr { + val getType = void + } + + case class BrIf(label: Label, cond: Expr) extends Expr { + val getType = void + } + + case class BrTable(labels: Seq[Label], default: Label, index: Expr, body: Option[Expr]) extends Expr { + val getType = body.map(_.getType).getOrElse(void) + } + + case class Call(name: Label, tpe: Type, args: Seq[Expr]) extends Expr { + val getType = tpe + } + + case class CallIndirect(tpe: Type, func: Expr, args: Seq[Expr]) extends Expr { + val getType = tpe + } + + case class Return(value: Expr) extends Expr { + val getType = void + } + case class Drop(value: Expr) extends Expr { + val getType = void + } + case object Unreachable extends Expr { + val getType = void + } + case object Nop extends Expr { + val getType = void + } + + case class Load(tpe: Type, truncate: Option[(TruncType,Sign)], address: Expr) extends Expr { + val getType = tpe + } + + case class Store(truncate: Option[TruncType], address: Expr, value: Expr) extends Expr { + val getType = void + } + + case object MemorySize extends Expr { + val getType = i32 + } + + case class MemoryGrow(size: Expr) extends Expr { + val getType: Type = i32 + } + + // Variable instructions + case class GetLocal(label: Label)(implicit lh: LocalsHandler) extends Expr { + val getType = lh.getType(label) + } + case class SetLocal(l: Label, value: Expr) extends Expr { + val getType = void + } + + case class GetGlobal(label: Label)(implicit gh: GlobalsHandler) extends Expr { + val getType = gh.getType(label) + } + case class SetGlobal(l: Label, value: Expr) extends Expr { + val getType = void + } + + // A sequence of instructions, 0 or 1 of which is allowed to leave a value on the stack + case class Sequence(es: Seq[Expr]) extends Expr { + val getType = es.map(_.getType).filter(_ != void) match { + case Seq() => void + case Seq(tpe) => tpe + case other => sys.error(s"Sequence $es contains multiple values with non-void types") + } + } + + // Helpers + def zero(tpe: Type): Const = tpe match { + case `i32` => I32Const(0) + case `i64` => I64Const(0) + case `f32` => F32Const(0) + case `f64` => F64Const(0) + } + +} diff --git a/core/src/main/scala/stainless/wasmgen/wasm/FileWriter.scala b/core/src/main/scala/stainless/wasmgen/wasm/FileWriter.scala new file mode 100644 index 0000000000..e6c395c284 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/wasm/FileWriter.scala @@ -0,0 +1,137 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen.wasm + +import java.io.{IOException, File, FileWriter => JFW} +import scala.sys.process._ +import inox.Context + +class FileWriter(module: Module, context: Context) { + private val outDirName = "wasmout" + private def withExt(ext: String) = s"$outDirName/${module.name}.$ext" + + private object Env { + trait OS + object Linux extends OS + object Windows extends OS + object Mac extends OS + + lazy val os = { + // If all fails returns Linux + val optOsName = Option(System.getProperty("os.name")) + optOsName.map(_.toLowerCase()).map { osName => + if (osName contains "linux") Linux + else if (osName contains "win") Windows + else if (osName contains "mac") Mac + else Linux + } getOrElse Linux + } + } + + private def writeWasmText(fileName: String): Unit = { + val fw = new JFW(new File(fileName)) + fw.write(Printer(module)) + fw.flush() + fw.close() + context.reporter.info(s"WebAssembly text file $fileName was generated.") + } + + private def writeWasmBinary(fileName: String, textFile: String): Unit = { + val w2wOptions = s"$textFile -o $fileName" + val wat2wasm = { + import Env._ + os match { + case Windows => "wat2wasm.exe" + case _ => "wat2wasm" + } + } + try { + s"$wat2wasm $w2wOptions".!! + context.reporter.info(s"WebAssembly binary file $fileName was generated.") + } catch { + case _: IOException => + context.reporter.error( + "wat2wasm utility was not found in system path, " + + "or did not have permission to execute. " + + "Skipping creation of wasm binary..." + ) + case e: RuntimeException => + context.reporter.internalError( + s"wat2wasm failed to translate WebAssembly text file ${withExt("wat")} to binary" + ) + } + } + + private def writeNodejsWrapper(fileName: String, moduleFile: String): Unit = { + val wrapperString = + s"""|// `Wasm` does **not** understand node buffers, but thankfully a node buffer + |// is easy to convert to a native Uint8Array. + |function toUint8Array(buf) { + | var u = new Uint8Array(buf.length); + | for (var i = 0; i < buf.length; ++i) { + | u[i] = buf[i]; + | } + | return u; + |} + |// Loads a WebAssembly dynamic library, returns a promise. + |// imports is an optional imports object + |function loadWebAssembly(filename, imports) { + | // Fetch the file and compile it + | const buffer = toUint8Array(require('fs').readFileSync(filename)) + | return WebAssembly.compile(buffer).then(module => { + | return new WebAssembly.Instance(module, imports) + | }) + |} + | + |var memory = new WebAssembly.Memory({initial:1}); + |var importObject = { + | system: { + | mem: memory, + | + | // Reads a string from linear memory and prints it to the console + | printString: function(arg) { + | var bufView = new Uint8Array(memory.buffer); + | // Reconstruct 32-bit integer length from 4 first bytes in little endian + | var len = ( + | bufView[arg] + + | bufView[arg+1] * 0x100 + + | bufView[arg+2] * 0x10000 + + | bufView[arg+3] * 0x1000000 + | ); + | var i = 0; + | var result = ""; + | while(i < len) { + | result += String.fromCharCode(bufView[arg+i+4]); + | i = i + 1 + | } + | console.log(result); + | } + | + | } + |}; + | + |loadWebAssembly('$moduleFile', importObject).then(function(instance) { + | instance.exports._main_() + |}).catch( function(error) { + | console.log("Error in wasm application: " + error) + | process.exit(1) + |}) + |""".stripMargin + val fw = new JFW(new File(fileName)) + fw.write(wrapperString) + fw.flush() + fw.close() + context.reporter.info(s"Javascript wrapper file $fileName was generated.") + } + + def writeFiles(): Unit = { + val outDir = new File(outDirName) + if (!outDir.exists()) { + outDir.mkdir() + } + writeWasmText(withExt("wat")) + writeWasmBinary(withExt("wasm"), withExt("wat")) + writeNodejsWrapper(withExt("js"), withExt("wasm")) + } + +} diff --git a/core/src/main/scala/stainless/wasmgen/wasm/Handlers.scala b/core/src/main/scala/stainless/wasmgen/wasm/Handlers.scala new file mode 100644 index 0000000000..e01deba6c0 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/wasm/Handlers.scala @@ -0,0 +1,45 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen.wasm + +import Types.Type +import Definitions._ +import Expressions.Const + +class GlobalsHandler(val globals: Seq[Global]) { + def getType(l: Label): Type = globals.find(_.name == l).get.tpe + def update(l: Label, c: Const) = { + globals.find(_.name == l).get.update(c) + } + def update(l: Label, upd: Const => Const) = { + val gl = globals.find(_.name == l).get + gl.update(upd(gl.init)) + } +} + +class LocalsHandler(args: Seq[ValDef]) { + private var locals_ = args + + def getFreshLocal(l: Label, tpe: Type): Label = { + locals_ :+= ValDef(l, tpe) + l + } + def getType(l: Label): Type = locals_.find(_.name == l).get.tpe + private[wasmgen] def locals: Seq[ValDef] = { + locals_.drop(args.size) + } +} + +class DataHandler(init: Int) { + private var data_ : Seq[Data] = Seq() + private var offset = init + def addNext(bytes: Seq[FormattedByte]): Int = { + data_ :+= Data(offset, bytes) + val current = offset + offset += bytes.length + current + } + def data = data_ + def nextFree = offset +} + diff --git a/core/src/main/scala/stainless/wasmgen/wasm/Module.scala b/core/src/main/scala/stainless/wasmgen/wasm/Module.scala new file mode 100644 index 0000000000..bb1fd31dfa --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/wasm/Module.scala @@ -0,0 +1,31 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless +package wasmgen +package wasm + +import Definitions._ +import Expressions.zero + +// A WebAssembly module +case class Module private ( + name: Label, + imports: Seq[Import], + globals: Seq[Global], + table: Table, + data: Seq[Data], + functions: Seq[FunDef] +) + +object Module { + def apply(name: Label, imports: Seq[Import], globals: Seq[ValDef], table: Table) + (funGen: (GlobalsHandler, DataHandler) => Seq[FunDef]): Module = { + val gh = new GlobalsHandler( + globals.map(g => Global(g.name, true, zero(g.tpe))) + ) + val dh = new DataHandler(0) + val funs = funGen(gh, dh) + + Module(name, imports, gh.globals, table, dh.data, funs) + } +} \ No newline at end of file diff --git a/core/src/main/scala/stainless/wasmgen/wasm/Printer.scala b/core/src/main/scala/stainless/wasmgen/wasm/Printer.scala new file mode 100644 index 0000000000..5e410cc2fb --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/wasm/Printer.scala @@ -0,0 +1,227 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen.wasm + +import scala.language.implicitConversions +import Expressions._ +import Definitions._ + +// Printer for Wasm modules +object Printer { + private implicit def s2d(s: String) = Raw(s) + + private def doc(mod: Module): Document = { + val Module(name, imports, globals, table, data, functions) = mod + Stacked( + "(module ", + Indented(Stacked(imports map doc)), + Indented(Stacked(globals map doc)), + Indented(doc(table)), + Indented(Stacked(data map doc)), + Indented(Stacked(functions map doc)), + ")", + "" + ) + } + + private def doc(g: Global): Document = { + val tpe = if (g.isMutable) s"(mut ${g.tpe})" else g.tpe.toString + s"(global $$${g.name} $tpe " <:> doc(g.init) <:> ")" + } + + private def doc(data: Data): Document = { + def formatByte(fb: FormattedByte) = { + val b = fb.byte + if (fb.formatted && b >= 0x20 && b != 0x7F && b != '"' && b != '\\') b.toChar.toString + else "\\%02X" format b + } + s"""(data (offset (i32.const ${data.offset})) "${data.bytes.map(formatByte).mkString}" )""" + } + + private def doc(t: Table): Document = { + s"(table anyfunc (elem ${t.funs.map("$" + _).mkString(" ")} ))" + } + + private def doc(imp: Import): Document = { + val Import(extModule, name, impType) = imp + val typeDoc: Document = impType match { + case FunSig(name, args, returnType) => + s"(func $$$name ${args.map(arg => s"(param $arg) ").mkString} (result $returnType))" + case Memory(size) => + s"(memory $size)" + } + s"""(import "$extModule" "$name" """ <:> typeDoc <:> ")" + } + + private def doc(fh: FunDef): Document = { + val FunDef(name, args, returnType, locals, body) = fh + val exportDoc: Document = s"""(export "$name" (func $$$name))""" + val paramsDoc: Document = + Lined(args map { case ValDef(name, tpe) => + Raw(s"(param $$$name $tpe) ") + }) + val resultDoc: Document = s"(result $returnType) " + val localsDoc: Document = + Lined(locals map { case ValDef(name, tpe) => + Raw(s"(local $$$name $tpe) ") + }) + + Stacked( + exportDoc, + s"(func $$$name " <:> paramsDoc <:> resultDoc <:> localsDoc, + Indented(Stacked(doc(body))), + ")" + ) + } + + + private def doc(expr: Expr): Document = { + expr match { + case Binary(op, lhs, rhs) => + Stacked( + s"(${lhs.getType}.$op", + Indented(doc(lhs)), + Indented(doc(rhs)), + ")" + ) + case Unary(op, e) => + Stacked( + s"(${e.getType}.$op", + Indented(doc(e)), + ")" + ) + case I32Const(value) => s"(i32.const $value)" + case I64Const(value) => s"(i64.const $value)" + case F32Const(value) => s"(f32.const $value)" + case F64Const(value) => s"(f64.const $value)" + case If(label, cond, thenn, elze) => + Stacked( + s"(if $$$label (result ${expr.getType})", + Indented(doc(cond)), + "(then", + Indented(doc(thenn)), + ") (else ", + Indented(doc(elze)), + "))" + ) + case Loop(label, body) => + Stacked( + s"(loop $$$label (result ${expr.getType})", + Indented(doc(body)), + ")" + ) + case Block(label, body) => + Stacked( + s"(block $$$label (result ${expr.getType})", + Indented(doc(body)), + ")" + ) + case Br(label) => s"(br $$$label)" + case BrIf(label, cond) => + Stacked( + s"(br_if $$$label", + Indented(doc(cond)), + ")" + ) + case BrTable(labels, default, index, body) => + Stacked( + s"(br_table ${(labels :+ default) map ("$" + _ ) mkString " "}", + Indented(doc(index)), + Indented(body map doc getOrElse Raw("")), + ")" + ) + case Call(name, _, args) => + Stacked( + s"(call $$$name", + Indented(Stacked(args map doc: _*)), + ")" + ) + case CallIndirect(_, fun, args) => + Stacked( + s"(call_indirect (param ${args.map(_.getType).mkString(" ")}) (result ${expr.getType})", + Indented(Stacked( (args :+ fun) map doc: _*)), + ")" + ) + case Load(tpe, truncate, expr) => + val ts = truncate match { + case Some((tpe, sign)) => s"${tpe.bitSize}_$sign" + case None => "" + } + Stacked( + s"($tpe.load$ts", + Indented(doc(expr)), + ")" + ) + case Store(truncate, address, value) => + val ts = truncate.map(_.bitSize.toString).getOrElse("") + Stacked( + s"(${value.getType}.store$ts", + Indented(doc(address)), + Indented(doc(value)), + ")" + ) + case MemorySize => + "(memory.size)" + case MemoryGrow(size) => + Stacked( + "(memory.grow", + Indented(doc(size)), + ")" + ) + case Return(value) => + Stacked( + "(return", + Indented(doc(value)), + ")" + ) + case Unreachable => "(unreachable)" + case Drop(expr) => + Stacked( + s"(drop", + Indented(doc(expr)), + ")" + ) + case Nop => "(nop)" + case GetLocal(label) => s"(get_local $$$label)" + case SetLocal(label, value) => + Stacked( + s"(set_local $$$label", + Indented(doc(value)), + s")" + ) + case GetGlobal(label) => s"(get_global $$$label)" + case SetGlobal(label, value) => + Stacked( + s"(set_global $$$label", + Indented(doc(value)), + s")" + ) + case Extend(to, sign, e) => + Stacked( + s"($to.extend_$sign/${e.getType}", + Indented(doc(e)), + ")" + ) + case Wrap(to, e) => + Stacked( + s"($to.wrap/${e.getType}", + Indented(doc(e)), + ")" + ) + case Truncate(to, sign, e) => + Stacked( + s"($to.trunc_$sign/${e.getType}", + Indented(doc(e)), + ")" + ) + case Sequence(es) => + Stacked(es map doc : _*) + } + + } + + def apply(mod: Module) = doc(mod).print + def apply(fh: FunDef) = doc(fh).print + def apply(expr: Expr) = doc(expr).print + +} diff --git a/core/src/main/scala/stainless/wasmgen/wasm/Types.scala b/core/src/main/scala/stainless/wasmgen/wasm/Types.scala new file mode 100644 index 0000000000..a3f05809f7 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/wasm/Types.scala @@ -0,0 +1,23 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen.wasm + +object Types { + trait AbsType { + val size: Int + def bitSize: Int = size * 8 + } + trait Type extends AbsType + trait TruncType extends AbsType + case object i32 extends Type with TruncType { val size = 4 } + case object i64 extends Type { val size = 8 } + case object f32 extends Type { val size = 4 } + case object f64 extends Type { val size = 8 } + case object void extends Type { + val size = 0 + override def toString = "" + } + + case object i8 extends TruncType { val size = 1 } + case object i16 extends TruncType { val size = 2 } +} diff --git a/core/src/main/scala/stainless/wasmgen/wasm/package.scala b/core/src/main/scala/stainless/wasmgen/wasm/package.scala new file mode 100644 index 0000000000..0eab972699 --- /dev/null +++ b/core/src/main/scala/stainless/wasmgen/wasm/package.scala @@ -0,0 +1,14 @@ +/* Copyright 2009-2019 EPFL, Lausanne */ + +package stainless.wasmgen + +/** Defines ASTs representing wasm programs. + * The definitions correspond to the text format, + * with labels represented as strings. + * + * Limitations: Not everything defined in wasm is defined here, + * only what was required for our representation. + */ +package object wasm { + type Label = String +} diff --git a/core/src/test/scala/stainless/utils/TestIncrementalCompuationalGraph.scala b/core/src/test/scala/stainless/utils/TestIncrementalComputationalGraph.scala similarity index 100% rename from core/src/test/scala/stainless/utils/TestIncrementalCompuationalGraph.scala rename to core/src/test/scala/stainless/utils/TestIncrementalComputationalGraph.scala diff --git a/frontends/common/src/it/scala/stainless/ExtractionSuite.scala b/frontends/common/src/it/scala/stainless/ExtractionSuite.scala index 3b90a6a9c2..4ba29d98a0 100644 --- a/frontends/common/src/it/scala/stainless/ExtractionSuite.scala +++ b/frontends/common/src/it/scala/stainless/ExtractionSuite.scala @@ -85,7 +85,7 @@ abstract class ExtractionSuite extends FunSpec with inox.ResourceUtils with Inpu tryPrograms foreach { case (f, tp) => tp match { // we expect a specific kind of exception: case Failure(e: stainless.frontend.UnsupportedCodeException) => assert(true) - case Failure(e: stainless.extraction.MissformedStainlessCode) => assert(true) + case Failure(e: stainless.extraction.MalformedStainlessCode) => assert(true) case Failure(e) => assert(false, s"$f was rejected with $e:\nStack trace:\n${e.getStackTrace().map(_.toString).mkString("\n")}") case Success(n) => assert(n > 0, s"$f was successfully extracted") }} diff --git a/frontends/common/src/test/scala/stainless/InputUtils.scala b/frontends/common/src/test/scala/stainless/InputUtils.scala index 5a89552247..0ad6a68072 100644 --- a/frontends/common/src/test/scala/stainless/InputUtils.scala +++ b/frontends/common/src/test/scala/stainless/InputUtils.scala @@ -6,7 +6,7 @@ import scala.language.existentials import extraction.xlang.{ trees => xt, TreeSanitizer } import frontend.CallBack -import utils.{ CheckFilter, DependenciesFinder, Registry } +import utils.{ CheckFilter, XLangDependenciesFinder, Registry } import scala.collection.mutable.ListBuffer @@ -57,9 +57,9 @@ trait InputUtils { override val context = ctx override def computeDirectDependencies(fd: xt.FunDef): Set[Identifier] = - new DependenciesFinder()(fd) + new XLangDependenciesFinder()(fd) override def computeDirectDependencies(cd: xt.ClassDef): Set[Identifier] = - new DependenciesFinder()(cd) + new XLangDependenciesFinder()(cd) override def shouldBeChecked(fd: xt.FunDef): Boolean = filterOpt map { _.shouldBeChecked(fd) } getOrElse true @@ -101,7 +101,7 @@ trait InputUtils { // Check that extracted symbols are valid TreeSanitizer(xt) check syms - (units.toSeq.sortBy(_.id.name), inox.Program(xt)(syms)) + (units.sortBy(_.id.name), inox.Program(xt)(syms)) } } diff --git a/frontends/common/src/test/scala/stainless/RegistryTestSuite.scala b/frontends/common/src/test/scala/stainless/RegistryTestSuite.scala index f8f24e5c24..6cff92a3c0 100644 --- a/frontends/common/src/test/scala/stainless/RegistryTestSuite.scala +++ b/frontends/common/src/test/scala/stainless/RegistryTestSuite.scala @@ -204,7 +204,7 @@ class RegistryTestSuite extends FunSuite { super.extract(symbols) } - override def apply(functions: Seq[Identifier], symbols: trees.Symbols): Future[Analysis] = { + override def execute(functions: Seq[Identifier], symbols: trees.Symbols): Future[Analysis] = { val report = MockReport(Set.empty, Set.empty) val analysis = MockAnalysis(report) Future.successful(analysis) diff --git a/frontends/library/stainless/annotation.scala b/frontends/library/stainless/annotation/annotations.scala similarity index 96% rename from frontends/library/stainless/annotation.scala rename to frontends/library/stainless/annotation/annotations.scala index 5835b4ceff..e050486616 100644 --- a/frontends/library/stainless/annotation.scala +++ b/frontends/library/stainless/annotation/annotations.scala @@ -3,9 +3,8 @@ package stainless package annotation -import scala.annotation.Annotation -import scala.annotation.StaticAnnotation import scala.annotation.meta._ +import scala.annotation.{Annotation, StaticAnnotation} /** The annotated symbols is not extracted at all. For internal usage only. */ class ignore extends Annotation diff --git a/frontends/library/stainless/collection/List.scala b/frontends/library/stainless/collection/List.scala index 494f511e28..3651bf987e 100644 --- a/frontends/library/stainless/collection/List.scala +++ b/frontends/library/stainless/collection/List.scala @@ -309,14 +309,13 @@ sealed abstract class List[T] { def splitAtIndex(index: BigInt) : (List[T], List[T]) = { this match { case Nil() => (Nil[T](), Nil[T]()) - case Cons(h, rest) => { + case Cons(h, rest) => if (index <= BigInt(0)) { (Nil[T](), this) } else { val (left,right) = rest.splitAtIndex(index - 1) (Cons[T](h,left), right) } - } }} ensuring { (res:(List[T],List[T])) => res._1 ++ res._2 == this && res._1 == take(index) && res._2 == drop(index) @@ -540,7 +539,7 @@ sealed abstract class List[T] { val rec = t.indexWhere(p) if (rec >= 0) rec + BigInt(1) else BigInt(-1) - }} ensuring { + }} ensuring { _ >= BigInt(0) == (this exists p) } diff --git a/frontends/library/stainless/lang/Set.scala b/frontends/library/stainless/lang/Set.scala index 0ecef0926c..26327cefbd 100644 --- a/frontends/library/stainless/lang/Set.scala +++ b/frontends/library/stainless/lang/Set.scala @@ -19,7 +19,7 @@ object Set { } @ignore -case class Set[T](val theSet: scala.collection.immutable.Set[T]) { +case class Set[T](theSet: scala.collection.immutable.Set[T]) { def +(a: T): Set[T] = new Set[T](theSet + a) def ++(a: Set[T]): Set[T] = new Set[T](theSet ++ a.theSet) def -(a: T): Set[T] = new Set[T](theSet - a) diff --git a/frontends/library/stainless/wasm/Runtime.scala b/frontends/library/stainless/wasm/Runtime.scala new file mode 100644 index 0000000000..cfdecf0378 --- /dev/null +++ b/frontends/library/stainless/wasm/Runtime.scala @@ -0,0 +1,280 @@ +package stainless.wasm + +import stainless.lang._ +import stainless.annotation.library + +/** Implements tuples, + * as well as set, map and bag operations on top of sorted lists + */ +@library +object Runtime { + + @library + sealed case class Tuple2[T1, T2](e1: T1, e2: T2) + @library + sealed case class Tuple3[T1, T2, T3](e1: T1, e2: T2, e3: T3) + @library + sealed case class Tuple4[T1, T2, T3, T4](e1: T1, e2: T2, e3: T3, e4: T4) + + /* Transforms any type to a string. Will be filled in by the code generator */ + @library + def toString[A](a: A): String = "" + + /* String transformers for basic types */ + @library + def digitToStringL(b: Long): String = { + b match { + case _ if b == 0 => "0" + case _ if b == 1 => "1" + case _ if b == 2 => "2" + case _ if b == 3 => "3" + case _ if b == 4 => "4" + case _ if b == 5 => "5" + case _ if b == 6 => "6" + case _ if b == 7 => "7" + case _ if b == 8 => "8" + case _ if b == 9 => "9" + } + } + + @library + def digitToStringI(b: Int): String = { + b match { + case _ if b == 0 => "0" + case _ if b == 1 => "1" + case _ if b == 2 => "2" + case _ if b == 3 => "3" + case _ if b == 4 => "4" + case _ if b == 5 => "5" + case _ if b == 6 => "6" + case _ if b == 7 => "7" + case _ if b == 8 => "8" + case _ if b == 9 => "9" + } + } + + @library + def i64ToString(b: Long): String = { + if (b < 0) "-" + i64ToString(-b) + else if (b <= 9) digitToStringL(b) + else i64ToString(b / 10) + digitToStringL(b % 10) + } + + @library + def i32ToString(b: Int): String = { + if (b < 0) "-" + i32ToString(-b) + else if (b <= 9) digitToStringI(b) + else i32ToString(b / 10) + digitToStringI(b % 10) + } + + + @library + def booleanToString(i: Int) = if (i == 0) "false" else "true" + @library // TODO + def f64ToString(b: Real): String = "" + @library + def funToString(): String = "" + @library + def unitToString(): String = "()" + + /* compares two elements of any type. Will be filled in by the code generator */ + @library + def compare[A](a1: A, a2: A): Int = 0 + + // We define our own lists to not have to load the entire scala lib + @library + sealed abstract class Set[A] { + @inline def ::(elem: A): Set[A] = SCons(elem, this) + } + @library + case class SCons[A](h: A, t: Set[A]) extends Set[A] + @library + case class SNil[A]() extends Set[A] + + @library + def SNil$0ToString[A](s: Set[A]) = "Set()" + @library + def SCons$0ToString[A](s: Set[A]) = { + def rec(s: Set[A]): String = s match { + case SCons(e1, s1@ SCons(_, _)) => toString[A](e1) + ", " + rec(s1) + case SCons(e1, SNil()) => toString[A](e1) + } + "Set(" + rec(s) + ")" + } + + @library + def setAdd[A](set: Set[A], elem: A): Set[A] = set match { + case SNil() => elem :: SNil() + case SCons(h, t) => + val c = compare(elem, h) + if (c < 0) elem :: h :: t + else if (c > 0) h :: setAdd(t, elem) + else h :: t + } + @library + def elementOfSet[A](set: Set[A], elem: A): Boolean = set match { + case SNil() => false + case SCons(h, t) => + val c = compare(elem, h) + if (c < 0) false + else if (c > 0) elementOfSet(t, elem) + else true + } + @library + def subsetOf[A](subset: Set[A], superset: Set[A]): Boolean = (subset, superset) match { + case (SNil(), _) => true + case (_, SNil()) => false + case (SCons(h1, t1), SCons(h2, t2)) => + val c = compare(h1, h2) + if (c < 0) false + else if (c > 0) subsetOf(subset, t2) + else subsetOf(t1, t2) + } + @library + def setIntersection[A](s1: Set[A], s2: Set[A]): Set[A] = (s1, s2) match { + case (SNil(), _) => s2 + case (_, SNil()) => s1 + case (SCons(h1, t1), SCons(h2, t2)) => + val c = compare(h1, h2) + if (c < 0) setIntersection(t1, s2) + else if (c > 0) setIntersection(s1, t2) + else h1 :: setIntersection(t1, t2) + } + @library + def setUnion[A](s1: Set[A], s2: Set[A]): Set[A] = (s1, s2) match { + case (SNil(), _) => s2 + case (_, SNil()) => s1 + case (SCons(h1, t1), SCons(h2, t2)) => + val c = compare(h1, h2) + if (c < 0) h1 :: setUnion(t1, s2) + else if (c > 0) h2 :: setUnion(s1, t2) + else h1 :: setUnion(t1, t2) + } + @library + def setDifference[A](s1: Set[A], s2: Set[A]): Set[A] = (s1, s2) match { + case (SNil(), _) => SNil() + case (_, SNil()) => s1 + case (SCons(h1, t1), SCons(h2, t2)) => + val c = compare(h1, h2) + if (c < 0) h1 :: setDifference(t1, s2) + else if (c > 0) setDifference(s1, t2) + else setDifference(t1, t2) + } + + // We define our own lists to not have to load the entire scala lib + @library + sealed abstract class Bag[A] + @library + case class BCons[A](elem: A, mult: BigInt, t: Bag[A]) extends Bag[A] + @library + case class BNil[A]() extends Bag[A] + + @library + def BNil$0ToString[A](s: Bag[A]) = "Bag()" + @library + def BCons$0ToString[A](s: Bag[A]) = { + def rec(s: Bag[A]): String = s match { + case BCons(e1, m1, b1@ BCons(_, _, _)) => toString(e1) + " -> " + toString(m1) + ", " + rec(b1) + case BCons(e1, m1, BNil()) => toString(e1) + " -> " + toString(m1) + } + "Bag(" + rec(s) + ")" + } + + @library @inline def min(b1: BigInt, b2: BigInt): BigInt = if (b1 <= b2) b1 else b2 + @library @inline def max(b1: BigInt, b2: BigInt): BigInt = if (b1 >= b2) b1 else b2 + + @library + def bagAdd[A](bag: Bag[A], elem: A, mult: BigInt): Bag[A] = bag match { + case BNil() => BCons (elem, mult, BNil()) + case BCons(h, m, t) => + val c = compare(elem, h) + if (c < 0) BCons(elem, mult, bag) + else if (c > 0) BCons(h, m, bagAdd(t, elem, mult)) + else BCons(h, m + mult, t) + } + @library + def bagMultiplicity[A](bag: Bag[A], elem: A): BigInt = bag match { + case BNil() => 0 + case BCons(h, m, t) => + val c = compare(elem, h) + if (c < 0) 0 + else if (c > 0) bagMultiplicity(t, elem) + else m + } + @library + def bagIntersection[A](b1: Bag[A], b2: Bag[A]): Bag[A] = (b1, b2) match { + case (BNil(), _) => b2 + case (_, BNil()) => b1 + case (BCons(h1, m1, t1), BCons(h2, m2, t2)) => + val c = compare(h1, h2) + if (c < 0) bagIntersection(t1, b2) + else if (c > 0) bagIntersection(b1, t2) + else BCons(h1, min(m1, m2), bagIntersection(t1, t2)) + } + @library + def bagUnion[A](b1: Bag[A], b2: Bag[A]): Bag[A] = (b1, b2) match { + case (BNil(), _) => b2 + case (_, BNil()) => b1 + case (BCons(h1, m1, t1), BCons(h2, m2, t2)) => + val c = compare(h1, h2) + if (c < 0) BCons(h1, m1, bagUnion(t1, b2)) + else if (c > 0) BCons(h2, m2, bagUnion(b1, t2)) + else BCons(h1, m1 + m2, bagUnion(t1, t2)) + } + @library + def bagDifference[A](b1: Bag[A], b2: Bag[A]): Bag[A] = (b1, b2) match { + case (BNil(), _) => BNil() + case (_, BNil()) => b1 + case (BCons(h1, m1, t1), BCons(h2, m2, t2)) => + val c = compare(h1, h2) + if (c < 0) BCons(h1, m1, bagDifference(t1, b2)) + else if (c > 0) bagDifference(b1, t2) + else BCons(h1, max(0, m1 - m2), bagDifference(t1, t2)) + } + + @library + sealed abstract class Map[K, V] { + @inline def ::(key: K, value: V): Map[K, V] = MCons(key, value, this) + } + @library + case class MCons[K, V](key: K, value: V, t: Map[K, V]) extends Map[K, V] + @library + case class MNil[K, V](default: V) extends Map[K, V] + + @library + def MNil$0ToString[K, V](s: Map[K, V]) = { + "Map()" + } + @library + def MCons$0ToString[K, V](s: Map[K, V]) = { + def vToString(v: V) = { + val s = toString(v) + s.bigSubstring(BigInt(5), s.bigLength - 1) + } + def rec(s: Map[K, V]): String = s match { + case MCons(k1, v1, m1@ MCons(_, _, _)) => + toString(k1) + " -> " + vToString(v1) + ", " + rec(m1) + case MCons(k1, v1, MNil(default)) => + toString(k1) + " -> " + vToString(v1) + } + "Map(" + rec(s) + ")" + } + + @library + def mapApply[K, V](map: Map[K, V], key: K): V = map match { + case MNil(default) => default + case MCons(k, v, t) => + if (k == key) v + else mapApply(t, key) + } + @library + def mapUpdated[K, V](map: Map[K, V], key: K, value: V): Map[K, V] = { + map match { + case MNil(default) => MCons(key, value, map) + case MCons(k, v, t) => + if (k == key) MCons(key, value, t) + else MCons(k, v, mapUpdated(t, key, value)) + } + } + +} diff --git a/frontends/scalac/src/it/scala/stainless/ComponentTestSuite.scala b/frontends/scalac/src/it/scala/stainless/ComponentTestSuite.scala index e1a2e60f59..d3fbb43d71 100644 --- a/frontends/scalac/src/it/scala/stainless/ComponentTestSuite.scala +++ b/frontends/scalac/src/it/scala/stainless/ComponentTestSuite.scala @@ -60,7 +60,7 @@ trait ComponentTestSuite extends inox.TestSuite with inox.ResourceUtils with Inp val funs = defs.filter(exProgram.symbols.functions contains _).toSeq - val report = Await.result(run.apply(funs, exProgram.symbols), Duration.Inf) + val report = Await.result(run.execute(funs, exProgram.symbols), Duration.Inf) block(report, ctx.reporter) } } else { @@ -101,7 +101,7 @@ trait ComponentTestSuite extends inox.TestSuite with inox.ResourceUtils with Inp // We have to cast the extracted symbols type as we are using two different // run instances. However, the trees types are the same so this should be safe (tm). val report = Await.result( - run.apply(funs, exSymbols.asInstanceOf[run.trees.Symbols]), + run.execute(funs, exSymbols.asInstanceOf[run.trees.Symbols]), Duration.Inf ) diff --git a/frontends/scalac/src/it/scala/stainless/LibrarySuite.scala b/frontends/scalac/src/it/scala/stainless/LibrarySuite.scala index d86e9b526b..2750ae84e1 100644 --- a/frontends/scalac/src/it/scala/stainless/LibrarySuite.scala +++ b/frontends/scalac/src/it/scala/stainless/LibrarySuite.scala @@ -28,7 +28,7 @@ class LibrarySuite extends FunSpec with InputUtils { import exProgram.trees._ val funs = exProgram.symbols.functions.values.filterNot(_.flags contains Unchecked).map(_.id).toSeq - val analysis = Await.result(run.apply(funs, exProgram.symbols), Duration.Inf) + val analysis = Await.result(run.execute(funs, exProgram.symbols), Duration.Inf) val report = analysis.toReport assert(report.totalConditions == report.totalValid, "Only " + report.totalValid + " valid out of " + report.totalConditions + "\n" + @@ -44,7 +44,7 @@ class LibrarySuite extends FunSpec with InputUtils { import exProgram.trees._ val funs = exProgram.symbols.functions.values.filterNot(_.flags contains Unchecked).map(_.id).toSeq - val analysis = Await.result(run.apply(funs, exProgram.symbols), Duration.Inf) + val analysis = Await.result(run.execute(funs, exProgram.symbols), Duration.Inf) assert( analysis.results forall { case (_, (g, _)) => g.isGuaranteed }, diff --git a/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala b/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala index fb055806e3..d4ddde9c2a 100644 --- a/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala +++ b/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala @@ -475,9 +475,8 @@ trait ASTExtractors { object ExMainFunctionDef { def unapply(dd: DefDef): Boolean = dd match { - case DefDef(_, name, tparams, vparamss, tpt, rhs) if name.toString == "main" && tparams.isEmpty && vparamss.size == 1 && vparamss.head.size == 1 => { + case DefDef(_, name, tparams, vparamss, tpt, rhs) if name.toString == "main" && tparams.isEmpty && vparamss.size == 1 && vparamss.head.size == 1 => true - } case _ => false } } @@ -491,7 +490,7 @@ trait ASTExtractors { dd.symbol.isSynthetic && dd.symbol.isImplicit && dd.symbol.isMethod && - !(getAnnotations(tpt.symbol) contains "ignore") + !(getAnnotations(tpt.symbol) exists (_._2 == "ignore")) ) || !dd.symbol.isSynthetic || canExtractSynthetic(dd.symbol) @@ -808,7 +807,7 @@ trait ASTExtractors { object ExTupleExtract { def unapply(tree: Select) : Option[(Tree,Int)] = tree match { - case Select(lhs, n) => { + case Select(lhs, n) => val methodName = n.toString if(methodName.head == '_') { val indexString = methodName.tail @@ -822,7 +821,6 @@ trait ASTExtractors { None } } else None - } case _ => None } } diff --git a/frontends/scalac/src/main/scala/stainless/frontends/scalac/StainlessPlugin.scala b/frontends/scalac/src/main/scala/stainless/frontends/scalac/StainlessPlugin.scala index 5bcb6c252f..9c529af896 100644 --- a/frontends/scalac/src/main/scala/stainless/frontends/scalac/StainlessPlugin.scala +++ b/frontends/scalac/src/main/scala/stainless/frontends/scalac/StainlessPlugin.scala @@ -27,7 +27,7 @@ class StainlessPluginComponent( val adapter = new ReporterAdapter(global.reporter, Set()) stainlessContext.copy(reporter = adapter) } - override protected val callback: CallBack = stainless.frontend.getStainlessCallBack(ctx) + override protected val callback: CallBack = stainless.frontend.getCallBack(ctx) override protected val cache: SymbolMapping = new SymbolMapping // FIXME: Mind the duplication with ScalaCompiler#stainlessExtraction. Should we extract the common bits? diff --git a/unmanaged/wasm/LICENCE b/unmanaged/wasm/LICENCE new file mode 100644 index 0000000000..3d521d8952 --- /dev/null +++ b/unmanaged/wasm/LICENCE @@ -0,0 +1,203 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright 2015 the repository authors, see AUTHORS file. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + diff --git a/unmanaged/wasm/README b/unmanaged/wasm/README new file mode 100644 index 0000000000..89439dd11a --- /dev/null +++ b/unmanaged/wasm/README @@ -0,0 +1,6 @@ +This directory contains WebAssembly utilities available under + +https://github.com/WebAssembly/wabt + +and subject to the LICENCE contained in this directory. + diff --git a/unmanaged/wasm/mac/wat2wasm b/unmanaged/wasm/mac/wat2wasm new file mode 100755 index 0000000000..b864abff28 Binary files /dev/null and b/unmanaged/wasm/mac/wat2wasm differ diff --git a/unmanaged/wasm/wat2wasm b/unmanaged/wasm/wat2wasm new file mode 100755 index 0000000000..6e54e05137 Binary files /dev/null and b/unmanaged/wasm/wat2wasm differ diff --git a/unmanaged/wasm/wat2wasm.exe b/unmanaged/wasm/wat2wasm.exe new file mode 100755 index 0000000000..7f6f998705 Binary files /dev/null and b/unmanaged/wasm/wat2wasm.exe differ