From a9c9719f34457971bb161ae97154bd29374a8556 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Mon, 9 Mar 2015 15:02:29 +0100
Subject: [PATCH] Block positions, explicit errors from xlang features.
---
src/main/scala/leon/utils/Positions.scala | 27 +++++++++++++++
.../leon/xlang/NoXLangFeaturesChecking.scala | 33 +++++++++++++++----
src/main/scala/leon/xlang/Trees.scala | 4 +++
3 files changed, 58 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/utils/Positions.scala b/src/main/scala/leon/utils/Positions.scala
index c38d1ab53..44065df86 100644
--- a/src/main/scala/leon/utils/Positions.scala
+++ b/src/main/scala/leon/utils/Positions.scala
@@ -34,6 +34,33 @@ abstract class Position extends Ordered[Position] {
def isDefined: Boolean
}
+object Position {
+ def between(a: Position, b: Position): Position = {
+ if (a.file == b.file) {
+ if (a.line == b.line && a.col == b.col) {
+ a
+ } else {
+ val (from, to) = if (a < b) (a, b) else (b, a)
+
+ (from, to) match {
+ case (p1: OffsetPosition, p2: OffsetPosition) =>
+ RangePosition(p1.line, p1.col, p1.point, p2.line, p2.col, p2.point, p1.file)
+ case (p1: RangePosition, p2: RangePosition) =>
+ RangePosition(p1.lineFrom, p1.colFrom, p1.pointFrom, p2.lineTo, p2.colTo, p2.pointTo, p1.file)
+ case (p1: OffsetPosition, p2: RangePosition) =>
+ RangePosition(p1.line, p1.col, p1.point, p2.lineTo, p2.colTo, p2.pointTo, p1.file)
+ case (p1: RangePosition, p2: OffsetPosition) =>
+ RangePosition(p1.lineFrom, p1.colFrom, p1.pointFrom, p2.line, p2.col, p2.point, p1.file)
+ case (a,b) =>
+ a
+ }
+ }
+ } else {
+ a
+ }
+ }
+}
+
abstract class DefinedPosition extends Position {
override def toString = line+":"+col
override def fullString = file.getPath+":"+line+":"+col
diff --git a/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
index 05b9c2553..0c6f11a8d 100644
--- a/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
+++ b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
@@ -6,11 +6,13 @@ package xlang
import purescala.Common._
import purescala.TypeTrees._
import purescala.Trees._
+import purescala.TreeOps.collect
import purescala.Definitions._
import purescala.Constructors._
+import utils.Position
+
import xlang.Trees._
-import xlang.TreeOps.isXLang
object NoXLangFeaturesChecking extends UnitPhase[Program] {
@@ -18,11 +20,30 @@ object NoXLangFeaturesChecking extends UnitPhase[Program] {
val description = "Ensure and enforce that no xlang features are used"
override def apply(ctx: LeonContext, pgm: Program): Unit = {
- pgm.definedFunctions.foreach(fd => {
- if(isXLang(fd.fullBody)) {
- ctx.reporter.fatalError(fd.fullBody.getPos, "Expr is using xlang features")
- }
- })
+ val errors = pgm.definedFunctions.flatMap(fd => collect[(Position, String)]{
+ case (e: Block) =>
+ Set((e.getPos, "Block expressions require xlang desugaring"))
+ case (e: Assignment) =>
+ Set((e.getPos, "Mutating variables requires xlang desugaring"))
+ case (e: While) =>
+ Set((e.getPos, "While expressions require xlang desugaring"))
+ case (e: Epsilon) =>
+ Set((e.getPos, "Usage of epsilons requires xlang desugaring"))
+ case (e: EpsilonVariable) =>
+ Set((e.getPos, "Usage of epsilons requires xlang desugaring"))
+ case (e: LetVar) =>
+ Set((e.getPos, "Mutable variables (e.g. 'var x' instead of 'val x') require xlang desugaring"))
+ case (e: Waypoint) =>
+ Set((e.getPos, "Usage of waypoints requires xlang desugaring"))
+ case (e: ArrayUpdate) =>
+ Set((e.getPos, "In-place updates of arrays require xlang desugaring"))
+ case _ =>
+ Set()
+ }(fd.fullBody))
+
+ for ((p, msg) <- errors) {
+ ctx.reporter.error(p, msg)
+ }
}
}
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 2740b3d5c..6c3864204 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -24,6 +24,10 @@ object Trees {
Some((exprs :+ last, exprs => Block(exprs.init, exprs.last)))
}
+ override def getPos = {
+ Position.between(exprs.head.getPos, last.getPos)
+ }
+
def printWith(implicit pctx: PrinterContext) {
p"""|{
| ${nary(exprs :+ last, "\n")}
--
GitLab