Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Experiment: Less duplication, more aggressive let simplification #860

Open
wants to merge 2 commits into
base: scala-2
Choose a base branch
from
Open

Experiment: Less duplication, more aggressive let simplification #860

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c5edcdf
Experiment: Less duplication, more aggressive let simplification
gsps Nov 19, 2020
85b59cb
Fix Streams example by adding exceptions to new AssertionInjector beh…
gsps Nov 20, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion core/src/main/scala/stainless/ast/Deconstructors.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -199,7 +199,8 @@ trait TreeDeconstructor extends inox.ast.TreeDeconstructor {
case s.RecursiveType(id, tps, e) => (Seq(id), Seq(), Seq(e), tps, Seq(), (ids, _, es, ntps, _) => t.RecursiveType(ids(0), ntps, es(0)))
case s.ValueType(tpe) => (Seq(), Seq(), Seq(), Seq(tpe), Seq(), (_, _, _, tps, _) => t.ValueType(tps(0)))
case s.AnnotatedType(tpe, flags) =>
(Seq(), Seq(), Seq(), Seq(tpe), flags, (_, _, _, tps, flags) => t.AnnotatedType(tps(0), flags))
(Seq(), Seq(), Seq(), Seq(tpe), flags,
(_, _, _, tps, flags) => if (flags.nonEmpty) t.AnnotatedType(tps(0), flags) else tps(0))
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We usually try not to simplify within the Deconstructor to make sure transformations are as predictable as possible. You could add the corresponding transformation within one of the various simplify procedures.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay, I'll see if I can find some simplification that's already applied anyways. I guess I'd still like to add an assertion in AnnotatedType that ensures we never end up with an empty list of annotations (which is impossible to spot in the pretty-printed tree!).

case _ => super.deconstruct(tpe)
}

Expand Down
7 changes: 4 additions & 3 deletions core/src/main/scala/stainless/ast/SymbolOps.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -144,9 +144,10 @@ trait SymbolOps extends inox.ast.SymbolOps { self: TypeOps =>

def rewritePM(e: Expr): Option[Expr] = e match {
case m @ MatchExpr(scrut, cases) =>
val scrutVd = ValDef.fresh("scrut", scrut.getType).setPos(m)
val condsAndRhs = for (cse <- cases) yield {
val map = mapForPattern(scrut, cse.pattern)
val patCond = conditionForPattern[Path](scrut, cse.pattern, includeBinders = false)
val map = mapForPattern(scrutVd.toVariable, cse.pattern)
val patCond = conditionForPattern[Path](scrutVd.toVariable, cse.pattern, includeBinders = false)
val realCond = cse.optGuard match {
case Some(g) => patCond withCond replaceFromSymbols(map, g)
case None => patCond
Expand All @@ -170,7 +171,7 @@ trait SymbolOps extends inox.ast.SymbolOps { self: TypeOps =>
}
})

Some(bigIte)
Some(Let(scrutVd, scrut, bigIte).setPos(m))

case _ => None
}
Expand Down
44 changes: 44 additions & 0 deletions core/src/main/scala/stainless/solvers/InoxEncoder.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,50 @@ trait InoxEncoder extends ProgramEncoder {
import sourceProgram._
import sourceProgram.symbols._

// Lowering to Inox erases various trees, which provides many opportunities for let simplifications.
override def transform(fd: s.FunDef): t.FunDef = {
import t._
import exprOps._

def singleOccurences(expr: Expr): Set[Identifier] = {
import collection.mutable.HashMap
val counts = HashMap.empty[Identifier, Int]
preTraversal {
case v: Variable => counts.update(v.id, counts.getOrElse(v.id, 0) + 1)
case _ =>
} (expr)
counts.iterator.collect { case (id, 1) => id } .toSet
}

// Copied from Inox's SymbolOps. Doesn't really depend on symbols!
def simplifyLetsExt(expr: Expr, forced: Set[Identifier]): Expr = preMap({
case l1 @ Let(v1, Let(v2, e2, b2), b1) => Some(Let(v2, e2, Let(v1, b2, b1).copiedFrom(l1)).copiedFrom(l1))

case Let(v, e, v2) if v.toVariable == v2 => Some(e)

case Let(v, ts @ (
(_: Variable) |
TupleSelect(_: Variable, _) |
ADTSelector(_: Variable, _) |
FiniteMap(Seq(), _, _, _) |
FiniteBag(Seq(), _) |
FiniteSet(Seq(), _) |
IsConstructor(_: Variable, _)
), b) => Some(replaceFromSymbols(Map(v -> ts), b))

case Let(v, e, b) if forced.contains(v.id) => Some(replaceFromSymbols(Map(v -> e), b))

case _ => None
}, applyRec = true)(expr)

val newFd = super.transform(fd)

timers.verification.simplify.run {
val simplBody = simplifyLetsExt(newFd.fullBody, singleOccurences(newFd.fullBody))
newFd.copy(fullBody = simplBody)
}
}

override def transform(e: s.Expr): t.Expr = e match {
case m: s.MatchExpr =>
transform(matchToIfThenElse(m))
Expand Down
36 changes: 30 additions & 6 deletions core/src/main/scala/stainless/verification/AssertionInjector.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,12 @@ package verification
*/
trait AssertionInjector extends transformers.TreeTransformer {
val s: ast.Trees
val t: ast.Trees
val t: s.type

implicit val symbols: s.Symbols

import t.dsl._

val strictArithmetic: Boolean

private[this] var inWrappingMode: Boolean = false
Expand Down Expand Up @@ -53,11 +55,33 @@ trait AssertionInjector extends transformers.TreeTransformer {
).copiedFrom(i), transform(v)).copiedFrom(e)

case sel @ s.ADTSelector(expr, _) =>
t.Assert(
t.IsConstructor(transform(expr), sel.constructor.id).copiedFrom(e),
Some("Cast error"),
super.transform(e)
).copiedFrom(e)
def isIndexedType(tpe: s.Type) =
tpe match {
case _: s.RecursiveType => true
case _ => false
}
val hasIndexedType = expr match {
case v: s.Variable => isIndexedType(v.tpe)
case fi: s.FunctionInvocation => isIndexedType(fi.tfd.returnType)
case _ => false
}

// NOTE(gsps): Keeping the old, code-duplicating behavior here, since index annotations on
// types are not propagated through `expr.getType`, breaking the Streams example.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess an alternative would be to replicate part of the type inference logic from the type checker. In the long run, it probably makes more sense to move all the assertion checks there anyway.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You mean add the assertion check for ADTSelector in TypeChecker directly?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, all of the assertion checks injected in this class, really. It's not quite as good in terms of separation of concerns, but it makes sense to centralize all the checking.

Using let-bindings with type inference would also be reasonable and possibly not that difficult to implement. Actually, it would be great if we could add a simple locale type inference phrase to Stainless to compensate a bit for the lack of dependent types in Scala.

if (hasIndexedType)
t.Assert(
t.IsConstructor(transform(expr), sel.constructor.id).copiedFrom(e),
Some("Cast error"),
super.transform(e)
).copiedFrom(e)
else
let("recv" :: expr.getType, transform(expr)) { recv =>
t.Assert(
t.IsConstructor(recv, sel.constructor.id).copiedFrom(e),
Some("Cast error"),
super.transform(sel.copy(adt = recv).copiedFrom(e))
).copiedFrom(e)
}.copiedFrom(e)

case BVTyped(true, size, e0 @ s.Plus(lhs0, rhs0)) if checkOverflow =>
val lhs = transform(lhs0)
Expand Down