Transformation for return keyword #923
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,171 @@ | ||
| /* Copyright 2009-2021 EPFL, Lausanne */ | ||
|
|
||
| package stainless | ||
| package extraction | ||
| package imperative | ||
|
|
||
| trait ReturnElimination | ||
| extends oo.CachingPhase | ||
| with IdentitySorts | ||
| with SimplyCachedFunctions | ||
| with SimpleFunctions | ||
| with oo.IdentityTypeDefs | ||
| with oo.IdentityClasses | ||
| with utils.SyntheticSorts { self => | ||
|
|
||
| val s: Trees | ||
| val t: s.type | ||
|
|
||
| import s._ | ||
|
|
||
| protected class TransformerContext(val symbols: Symbols) { | ||
| // we precompute the set of expressions that contain a return | ||
| val exprHasReturn = collection.mutable.Set[Expr]() | ||
| for (fd <- symbols.functions.values) { | ||
| exprOps.postTraversal { | ||
| case e @ Return(_) => exprHasReturn += e | ||
| case e @ Operator(es, _) if (es.exists(exprHasReturn)) => exprHasReturn += e | ||
| case _ => () | ||
| }(fd.fullBody) | ||
| } | ||
|
|
||
| val funHasReturn: Set[Identifier] = symbols.functions.values.collect { | ||
| case fd if exprHasReturn(fd.fullBody) => fd.id | ||
| }.toSet | ||
| } | ||
|
|
||
| override protected def getContext(symbols: Symbols) = new TransformerContext(symbols) | ||
|
|
||
| protected def extractFunction(tc: TransformerContext, fd: FunDef): FunDef = { | ||
| implicit val symboms = tc.symbols | ||
|
|
||
| if (tc.funHasReturn(fd.id)) { | ||
| val specced = exprOps.BodyWithSpecs(fd.fullBody) | ||
| val retType = fd.returnType | ||
|
|
||
| object ReturnTransformer extends TransformerWithType { | ||
| override val s: self.s.type = self.s | ||
| override val t: self.s.type = self.s | ||
| override val symbols: s.Symbols = tc.symbols | ||
|
|
||
| private def proceedOrTransform(expr: Expr, currentType: Type): Expr = { | ||
| if (tc.exprHasReturn(expr)) transform(expr, currentType) | ||
| else ControlFlowSort.proceed(retType, currentType, expr) | ||
| } | ||
|
|
||
| private def proceedOrTransform(mc: MatchCase, currentType: Type): MatchCase = { | ||
| val MatchCase(pattern, optGuard, rhs) = mc | ||
| MatchCase(pattern, optGuard, proceedOrTransform(rhs, currentType)) | ||
| } | ||
|
|
||
| override def transform(expr: Expr, currentType: Type): Expr = expr match { | ||
| case _ if !tc.exprHasReturn(expr) => expr | ||
|
|
||
| case Return(e) if !tc.exprHasReturn(e) => ControlFlowSort.ret(retType, currentType, e) | ||
|
|
||
| case IfExpr(cond, e1, e2) if !tc.exprHasReturn(cond) => | ||
| IfExpr(cond, proceedOrTransform(e1, currentType), proceedOrTransform(e2, currentType)) | ||
|
|
||
| case MatchExpr(scrut, cases) if !tc.exprHasReturn(scrut) => | ||
| MatchExpr(scrut, | ||
| cases.map(proceedOrTransform(_, currentType)) | ||
| ) | ||
|
|
||
| case Let(vd, e, body) if tc.exprHasReturn(e) => | ||
| val firstType = vd.tpe | ||
| val controlFlowVal = | ||
| ValDef.fresh("cf", ControlFlowSort.controlFlow(retType, firstType)).setPos(e) | ||
|
|
||
| Let( | ||
| controlFlowVal, | ||
| transform(e, firstType), | ||
| ControlFlowSort.andThen( | ||
| retType, firstType, currentType, | ||
| controlFlowVal.toVariable, | ||
| v => exprOps.replaceFromSymbols(Map(vd -> v), proceedOrTransform(body, currentType)), | ||
| body.getPos | ||
| ) | ||
| ).setPos(expr) | ||
|
|
||
| case Let(vd, e, body) => | ||
| Let(vd, e, transform(body, currentType)) | ||
|
|
||
| case Block(es, last) => | ||
| def processBlockExpressions(es: Seq[Expr]): Expr = es match { | ||
| case Seq(e) => transform(e, currentType) | ||
|
|
||
| case e +: rest if (tc.exprHasReturn(e)) => | ||
| val firstType = e.getType | ||
| val controlFlowVal = | ||
| ValDef.fresh("cf", ControlFlowSort.controlFlow(retType, firstType)).setPos(e) | ||
| val transformedRest = processBlockExpressions(rest) | ||
|
|
||
| if (rest.exists(tc.exprHasReturn)) { | ||
|
There was a problem hiding this comment. Nit: this would probably be more readable if you pushed the if-expression down to the |
||
| Let( | ||
| controlFlowVal, | ||
| transform(e, firstType), | ||
| ControlFlowSort.andThen( | ||
| retType, firstType, currentType, | ||
| controlFlowVal.toVariable, | ||
| _ => transformedRest, | ||
| rest.head.getPos | ||
| ) | ||
| ).setPos(e) | ||
| } else { | ||
| Let( | ||
| controlFlowVal, | ||
| transform(e, firstType), | ||
| ControlFlowSort.andThen( | ||
| retType, firstType, currentType, | ||
| controlFlowVal.toVariable, | ||
| _ => ControlFlowSort.proceed(retType, currentType, transformedRest), | ||
| rest.head.getPos | ||
| ) | ||
| ).setPos(e) | ||
| } | ||
|
|
||
| case e +: rest => | ||
| val unusedVal = ValDef.fresh("unused", e.getType) | ||
|
There was a problem hiding this comment. You could preserve the case es =>
val nonReturnEs = es.takeWhile(e => !tc.hasExprReturn(e))
Block(nonReturnEs, processBlockExpressions(es.drop(nonReturnEs.size()))).copiedFrom(expr)You'll probably need to handle the case where |
||
| Let(unusedVal, e, processBlockExpressions(rest)) | ||
| } | ||
| processBlockExpressions(es :+ last) | ||
|
|
||
| case _ => | ||
| context.reporter.fatalError(expr.getPos, s"Keyword `return` is not supported in expression ${expr.asString}") | ||
| } | ||
| } | ||
|
|
||
| val newBody = specced.bodyOpt.map { body => | ||
| val topLevelCF = ValDef.fresh("topLevelCF", ControlFlowSort.controlFlow(retType, retType)).setPos(fd.fullBody) | ||
| Let(topLevelCF, ReturnTransformer.transform(body), | ||
| ControlFlowSort.buildMatch(retType, retType, topLevelCF.toVariable, | ||
| v => v, | ||
| v => v, | ||
| body.getPos | ||
| ) | ||
| ).setPos(body) | ||
| } | ||
| fd.copy(fullBody = specced.withBody(newBody, retType).reconstructed).setPos(fd) | ||
| } | ||
| else fd | ||
| } | ||
|
|
||
| override protected def extractSymbols(context: TransformerContext, symbols: s.Symbols): t.Symbols = { | ||
| if (symbols.functions.values.exists(fd => context.funHasReturn(fd.id))) | ||
| super.extractSymbols(context, symbols) | ||
| .withSorts(Seq(ControlFlowSort.syntheticControlFlow)) | ||
| else | ||
| super.extractSymbols(context, symbols) | ||
| } | ||
| } | ||
|
|
||
| object ReturnElimination { | ||
| def apply(trees: Trees)(implicit ctx: inox.Context): ExtractionPipeline { | ||
| val s: trees.type | ||
| val t: trees.type | ||
| } = new ReturnElimination { | ||
| override val s: trees.type = trees | ||
| override val t: trees.type = trees | ||
| override val context = ctx | ||
| } | ||
| } | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,28 @@ | ||
| import stainless.lang._ | ||
|
|
||
| object ControlFlow2 { | ||
|
|
||
| def foo(x: Option[BigInt], a: Boolean, b: Boolean): BigInt = { | ||
| if (a && b) { | ||
| return 1 | ||
| } | ||
|
|
||
| val y = x match { | ||
| case None() => return 0 | ||
| case Some(x) if a => return x + 1 | ||
| case Some(x) if b => return x + 2 | ||
| case Some(x) => x | ||
| }; | ||
|
|
||
| -y | ||
| } | ||
|
|
||
| def testFoo: Unit = { | ||
| assert(foo(None(), false, false) == 0) | ||
| assert(foo(Some(10), true, true) == 1) | ||
| assert(foo(Some(10), true, false) == 11) | ||
| assert(foo(Some(10), false, true) == 12) | ||
| assert(foo(Some(10), false, false) == -10) | ||
| } | ||
|
|
||
| } |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Your transformation isn't checking all trees (e.g. a
returninside a type refinement wouldn't be rejected).In general, it's safer to keep
sandttypes potentially distinct so the (Scala) type checker will make sure you visit all trees in your transformation.