diff --git a/src/main/scala/leon/purescala/CheckADTFieldsTypes.scala b/src/main/scala/leon/purescala/CheckADTFieldsTypes.scala
index 9de511180a260f6bf1fd04d1b04188d085b0b71a..ee78b4b5f3daadaea5ef7222105c13eaefc35401 100644
--- a/src/main/scala/leon/purescala/CheckADTFieldsTypes.scala
+++ b/src/main/scala/leon/purescala/CheckADTFieldsTypes.scala
@@ -3,11 +3,8 @@
package leon
package purescala
-import Common._
import Definitions._
-import Types._
import TypeOps._
-import Expressions._
object CheckADTFieldsTypes extends UnitPhase[Program] {
@@ -20,7 +17,9 @@ object CheckADTFieldsTypes extends UnitPhase[Program] {
for(vd <- ccd.fields) {
val tpe = vd.getType
if (bestRealType(tpe) != tpe) {
- ctx.reporter.warning("Definition of "+ccd.id+" has a field of a sub-type ("+vd+"): this type is not supported as-is by solvers and will be up-casted. This may cause issues such as crashes.")
+ ctx.reporter.warning("Definition of "+ccd.id+" has a field of a sub-type ("+vd+"): " +
+ "this type is not supported as-is by solvers and will be up-cast. " +
+ "This may cause issues such as crashes.")
}
}
case _ =>
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 1809ba00e66815cf0aec252d91340693ec1964ff..90f9d82b671f25fdee27e292768a56c17eeac2ad 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -157,9 +157,8 @@ object ExprOps {
val rec = postMap(f, applyRec) _
val Operator(es, builder) = e
+ val newEs = es.map(rec)
val newV = {
- val newEs = es.map(rec)
-
if ((newEs zip es).exists { case (bef, aft) => aft ne bef }) {
builder(newEs).copiedFrom(e)
} else {
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index dfa87a993fde5eb4df3a418c4f018b4f97a7f19b..c283a1be7665a7bed4f084a9a4f47421e44ef681 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -4,49 +4,32 @@ package leon.xlang
import leon.UnitPhase
import leon.LeonContext
-import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Expressions._
+import leon.purescala.ExprOps.simplePostTransform
+import leon.purescala.Extractors.IsTyped
+import leon.purescala.Types.ArrayType
import leon.xlang.Expressions._
-import leon.purescala.Extractors._
-import leon.purescala.Types._
object ArrayTransformation extends UnitPhase[Program] {
val name = "Array Transformation"
- val description = "Add bound checking for array access and remove array update with side effect"
+ val description = "Remove side-effectful array updates"
def apply(ctx: LeonContext, pgm: Program) = {
- pgm.definedFunctions.foreach(fd => {
- fd.fullBody = transform(fd.fullBody)(Map())
- })
+ pgm.definedFunctions.foreach(fd =>
+ fd.fullBody = simplePostTransform {
+ case up@ArrayUpdate(a, i, v) =>
+ val ra@Variable(id) = a
+ Assignment(id, ArrayUpdated(ra, i, v).setPos(up)).setPos(up)
+
+ case l@Let(i, IsTyped(v, ArrayType(_)), b) =>
+ LetVar(i, v, b).setPos(l)
+
+ case e =>
+ e
+ }(fd.fullBody)
+ )
}
- def transform(expr: Expr)(implicit env: Map[Identifier, Identifier]): Expr = (expr match {
- case up@ArrayUpdate(a, i, v) => {
- val ra = transform(a)
- val ri = transform(i)
- val rv = transform(v)
- val Variable(id) = ra
- Assignment(id, ArrayUpdated(ra, ri, rv).setPos(up))
- }
- case Let(i, v, b) => {
- v.getType match {
- case ArrayType(_) => {
- val freshIdentifier = FreshIdentifier("t", i.getType)
- val newEnv = env + (i -> freshIdentifier)
- LetVar(freshIdentifier, transform(v)(newEnv), transform(b)(newEnv))
- }
- case _ => Let(i, transform(v), transform(b))
- }
- }
- case v@Variable(i) => {
- Variable(env.getOrElse(i, i))
- }
-
- case Operator(args, recons) => recons(args.map(transform))
-
- case unhandled => scala.sys.error("Non-terminal case should be handled in ArrayTransformation: " + unhandled)
- }).setPos(expr)
-
}
diff --git a/src/main/scala/leon/xlang/EpsilonElimination.scala b/src/main/scala/leon/xlang/EpsilonElimination.scala
index 91b39ad5bf104583025e9791ea97196a517fc7d3..37775688971c77cb604285bb5f29e750c6a91ba9 100644
--- a/src/main/scala/leon/xlang/EpsilonElimination.scala
+++ b/src/main/scala/leon/xlang/EpsilonElimination.scala
@@ -2,7 +2,7 @@
package leon.xlang
-import leon.{UnitPhase, TransformationPhase, LeonContext}
+import leon.{UnitPhase, LeonContext}
import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Expressions._
diff --git a/src/main/scala/leon/xlang/FixReportLabels.scala b/src/main/scala/leon/xlang/FixReportLabels.scala
index 6346402c2985855bfcc9e2973fdd6a6babc8a427..9f18a2646915c9e1d6c624f55a0ef924f4685a28 100644
--- a/src/main/scala/leon/xlang/FixReportLabels.scala
+++ b/src/main/scala/leon/xlang/FixReportLabels.scala
@@ -4,14 +4,18 @@ package leon
package xlang
import leon.purescala.Definitions.IsLoop
-import leon.verification.{VC, VCKinds, VerificationReport}
-import leon.xlang.XLangAnalysisPhase.VCXLangKinds._
+import leon.verification._
object FixReportLabels extends LeonPhase[VerificationReport, VerificationReport]{
override val name: String = "fixReportLabels"
override val description: String = "Fix verification report labels to reflect the original imperative VCs"
+ // TODO: something of this sort should be included
+ // case object InvariantEntry extends VCKind("invariant init", "inv. init.")
+ case object InvariantPost extends VCKind("invariant postcondition", "inv. post.")
+ case object InvariantInd extends VCKind("invariant inductive", "inv. ind.")
+
def run(ctx: LeonContext)(vr: VerificationReport): VerificationReport = {
//this is enough to convert invariant postcondition and inductive conditions. However the initial validity
//of the invariant (before entering the loop) will still appear as a regular function precondition
diff --git a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
index 5d154854f56038d8317b08abb0ce3e3d1f05fce1..470c0d38990ceaad3a0a9fffb1fe9625b227ac0c 100644
--- a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
@@ -5,26 +5,19 @@ package xlang
import purescala.Definitions.Program
import purescala.FunctionClosure
-import verification._
object XLangAnalysisPhase extends TransformationPhase {
- val name = "xlang analysis"
- val description = "apply analysis on xlang"
-
- object VCXLangKinds {
- // TODO: something of this sort should be included
- // case object InvariantEntry extends VCKind("invariant init", "inv. init.")
- case object InvariantPost extends VCKind("invariant postcondition", "inv. post.")
- case object InvariantInd extends VCKind("invariant inductive", "inv. ind.")
- }
+ val name = "xlang desugaring"
+ val description = "Desugar xlang features into PureScala"
def apply(ctx: LeonContext, pgm: Program): Program = {
- ArrayTransformation(ctx, pgm) // In-place
- EpsilonElimination(ctx, pgm) // In-place
- (ImperativeCodeElimination andThen FunctionClosure).run(ctx)(pgm)
+ val phases =
+ ArrayTransformation andThen
+ EpsilonElimination andThen
+ ImperativeCodeElimination andThen
+ FunctionClosure
+ phases.run(ctx)(pgm)
}
-
-
}