From 1506a713aca6c4ed15644613b9f7b154186c102c Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 2 Dec 2013 16:33:08 +0100
Subject: [PATCH] Extract more (range) positions
---
.../frontends/scalac/CodeExtraction.scala | 24 ++++++++++---------
.../leon/frontends/scalac/ScalaCompiler.scala | 3 ++-
.../synthesis/condabd/refinement/Filter.scala | 3 +--
.../leon/verification/AnalysisPhase.scala | 2 --
.../leon/test/condabd/util/Scaffold.scala | 5 ++--
.../test/evaluators/EvaluatorsTests.scala | 3 ++-
.../scala/leon/test/purescala/DataGen.scala | 3 ++-
.../test/purescala/TransformationTests.scala | 5 ++--
.../synthesis/SynthesisRegressionSuite.scala | 2 +-
.../leon/test/synthesis/SynthesisSuite.scala | 2 +-
.../termination/TerminationRegression.scala | 2 +-
.../PureScalaVerificationRegression.scala | 2 +-
.../XLangVerificationRegression.scala | 2 +-
13 files changed, 31 insertions(+), 27 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 2fe5da3f4..23dcdd43c 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -479,7 +479,7 @@ trait CodeExtraction extends ASTExtractors {
*/
case dd @ ExFunctionDef(n, p, t, b) =>
- val funDef = extractFunSig(n, p, t).setPos(dd.pos)
+ val funDef = extractFunSig(n, p, t)
defsToDefs += (dd.symbol -> funDef)
val oldMutableVarSubst = mutableVarSubsts.toMap //take an immutable snapshot of the map
val oldCurrentFunDef = currentFunDef
@@ -540,14 +540,14 @@ trait CodeExtraction extends ASTExtractors {
case wh @ ExWhile(cond, body) =>
val condTree = extractTree(cond)
val bodyTree = extractTree(body)
- While(condTree, bodyTree).setPos(wh.pos)
+ While(condTree, bodyTree)
case wh @ ExWhileWithInvariant(cond, body, inv) =>
val condTree = extractTree(cond)
val bodyTree = extractTree(body)
val invTree = extractTree(inv)
- val w = While(condTree, bodyTree).setPos(wh.pos)
+ val w = While(condTree, bodyTree)
w.invariant = Some(invTree)
w
@@ -563,7 +563,7 @@ trait CodeExtraction extends ASTExtractors {
if(containsEpsilon(c1)) {
unsupported(epsi, "Usage of nested epsilon is not allowed")
}
- Epsilon(c1).setType(pstpe).setPos(epsi.pos)
+ Epsilon(c1).setType(pstpe)
case ExWaypointExpression(tpe, i, tree) =>
val pstpe = extractType(tpe)
@@ -592,7 +592,7 @@ trait CodeExtraction extends ASTExtractors {
val indexRec = extractTree(index)
val newValueRec = extractTree(newValue)
- ArrayUpdate(lhsRec, indexRec, newValueRec).setPos(update.pos)
+ ArrayUpdate(lhsRec, indexRec, newValueRec)
case ExInt32Literal(v) =>
IntLiteral(v)
@@ -632,7 +632,7 @@ trait CodeExtraction extends ASTExtractors {
val cBody = extractTree(body)
- Choose(vars, cBody).setPos(select.pos)
+ Choose(vars, cBody)
case ExCaseClassConstruction(tpt, args) =>
extractType(tpt.tpe) match {
@@ -839,7 +839,7 @@ trait CodeExtraction extends ASTExtractors {
MapUnion(rm, FiniteMap(Seq((rf, rt))).setType(t)).setType(t)
case t @ ArrayType(bt) =>
- ArrayUpdated(rm, rf, rt).setType(t).setPos(up.pos)
+ ArrayUpdated(rm, rf, rt).setType(t)
case _ =>
unsupported(tr, "updated can only be applied to maps.")
@@ -862,11 +862,11 @@ trait CodeExtraction extends ASTExtractors {
rlhs.getType match {
case MapType(_,tt) =>
assert(rargs.size == 1)
- MapGet(rlhs, rargs.head).setType(tt).setPos(app.pos)
+ MapGet(rlhs, rargs.head).setType(tt)
case ArrayType(bt) =>
assert(rargs.size == 1)
- ArraySelect(rlhs, rargs.head).setType(bt).setPos(app.pos)
+ ArraySelect(rlhs, rargs.head).setType(bt)
case _ =>
unsupported(tr, "apply on unexpected type")
@@ -936,14 +936,14 @@ trait CodeExtraction extends ASTExtractors {
throw ImpureCodeEncounteredException(tr)
}
val fd = defsToDefs(sy)
- FunctionInvocation(fd, ar.map(extractTree(_))).setType(fd.returnType).setPos(lc.pos)
+ FunctionInvocation(fd, ar.map(extractTree(_))).setType(fd.returnType)
}
case pm @ ExPatternMatching(sel, cses) =>
val rs = extractTree(sel)
val rc = cses.map(extractMatchCase(_))
val rt: LeonType = rc.map(_.rhs.getType).reduceLeft(leastUpperBound(_,_).get)
- MatchExpr(rs, rc).setType(rt).setPos(pm.pos)
+ MatchExpr(rs, rc).setType(rt)
// default behaviour is to complain :)
@@ -951,6 +951,8 @@ trait CodeExtraction extends ASTExtractors {
unsupported(tr, "Could not extract as PureScala")
}
+ res.setPos(current.pos)
+
rest match {
case Some(r) =>
LeonBlock(Seq(res), extractTree(r))
diff --git a/src/main/scala/leon/frontends/scalac/ScalaCompiler.scala b/src/main/scala/leon/frontends/scalac/ScalaCompiler.scala
index 2eea72237..331bc0906 100644
--- a/src/main/scala/leon/frontends/scalac/ScalaCompiler.scala
+++ b/src/main/scala/leon/frontends/scalac/ScalaCompiler.scala
@@ -4,8 +4,9 @@ package leon
package frontends.scalac
import scala.tools.nsc.{Global,Settings=>NSCSettings}
+import scala.tools.nsc.interactive.RangePositions
-class ScalaCompiler(settings : NSCSettings, ctx: LeonContext) extends Global(settings, new SimpleReporter(settings, ctx.reporter)) {
+class ScalaCompiler(settings : NSCSettings, ctx: LeonContext) extends Global(settings, new SimpleReporter(settings, ctx.reporter)) with RangePositions {
object leonExtraction extends {
val global: ScalaCompiler.this.type = ScalaCompiler.this
diff --git a/src/main/scala/leon/synthesis/condabd/refinement/Filter.scala b/src/main/scala/leon/synthesis/condabd/refinement/Filter.scala
index b524d66a4..c4f0f4009 100755
--- a/src/main/scala/leon/synthesis/condabd/refinement/Filter.scala
+++ b/src/main/scala/leon/synthesis/condabd/refinement/Filter.scala
@@ -8,7 +8,6 @@ import leon.purescala.TypeTrees._
import leon.purescala.Definitions._
import leon.purescala.Common.{ Identifier, FreshIdentifier }
import leon.purescala.TreeOps
-import leon.plugin.ExtractionPhase
import condabd.insynth.leon.loader.LeonLoader
import insynth.util.logging.HasLogger
@@ -177,4 +176,4 @@ class Filter(program: Program, holeFunDef: FunDef, refiner: VariableRefiner) ext
}
}
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 8a162e81f..905b37484 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -34,8 +34,6 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
var allVCs = Map[FunDef, List[VerificationCondition]]()
- println(purescala.ScalaPrinter(program))
-
for(funDef <- program.definedFunctions.toList.sortWith((fd1, fd2) => fd1.getPos < fd2.getPos) if (functionsToAnalyse.isEmpty || functionsToAnalyse.contains(funDef.id.name))) {
val tactic: Tactic =
diff --git a/src/test/scala/leon/test/condabd/util/Scaffold.scala b/src/test/scala/leon/test/condabd/util/Scaffold.scala
index 253fc7054..4314054eb 100644
--- a/src/test/scala/leon/test/condabd/util/Scaffold.scala
+++ b/src/test/scala/leon/test/condabd/util/Scaffold.scala
@@ -8,6 +8,7 @@ import java.io.{BufferedWriter, FileWriter, File}
import leon._
import leon.test._
+import leon.frontends._
import leon.utils._
import leon.purescala.Definitions._
import leon.purescala.Trees._
@@ -36,7 +37,7 @@ object Scaffold {
)
// Settings.showIDs = true
- val pipeline = leon.plugin.TemporaryInputPhase andThen leon.plugin.ExtractionPhase andThen SynthesisProblemExtractionPhase
+ val pipeline = TemporaryInputPhase andThen scalac.ExtractionPhase andThen SynthesisProblemExtractionPhase
val (program, results) = try {
pipeline.run(ctx)((content, Nil))
@@ -63,7 +64,7 @@ object Scaffold {
interruptManager = new InterruptManager(forProgramReporter)
)
- val pipeline = leon.plugin.ExtractionPhase andThen SynthesisProblemExtractionPhase
+ val pipeline = scalac.ExtractionPhase andThen SynthesisProblemExtractionPhase
val (program, results) = try {
pipeline.run(ctx)(file :: Nil)
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index eec8591db..972d0d732 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -7,7 +7,8 @@ import leon._
import leon.evaluators._
-import leon.plugin.{TemporaryInputPhase, ExtractionPhase}
+import leon.utils.TemporaryInputPhase
+import leon.frontends.scalac.ExtractionPhase
import leon.purescala.Common._
import leon.purescala.Definitions._
diff --git a/src/test/scala/leon/test/purescala/DataGen.scala b/src/test/scala/leon/test/purescala/DataGen.scala
index 8f73d7390..a84687ebc 100644
--- a/src/test/scala/leon/test/purescala/DataGen.scala
+++ b/src/test/scala/leon/test/purescala/DataGen.scala
@@ -4,7 +4,8 @@ package leon.test
package purescala
import leon._
-import leon.plugin.{TemporaryInputPhase,ExtractionPhase}
+import leon.utils.TemporaryInputPhase
+import leon.frontends.scalac.ExtractionPhase
import leon.purescala.Common._
import leon.purescala.Trees._
diff --git a/src/test/scala/leon/test/purescala/TransformationTests.scala b/src/test/scala/leon/test/purescala/TransformationTests.scala
index 40af1409e..79a6961ef 100644
--- a/src/test/scala/leon/test/purescala/TransformationTests.scala
+++ b/src/test/scala/leon/test/purescala/TransformationTests.scala
@@ -4,7 +4,8 @@ package leon.test
package purescala
import leon._
-import leon.plugin.{TemporaryInputPhase,ExtractionPhase}
+import leon.utils.TemporaryInputPhase
+import leon.frontends.scalac.ExtractionPhase
import leon.purescala.ScalaPrinter
import leon.purescala.Common._
@@ -15,7 +16,7 @@ import leon.purescala.TypeTrees._
class TransformationTests extends LeonTestSuite {
- val pipeline = leon.plugin.ExtractionPhase andThen leon.utils.SubtypingPhase
+ val pipeline = ExtractionPhase andThen leon.utils.SubtypingPhase
filesInResourceDir("regression/transformations").foreach { file =>
val ctx = testContext.copy(
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index 408634f9e..502679382 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -33,7 +33,7 @@ class SynthesisRegressionSuite extends LeonTestSuite {
val opts = SynthesisOptions(searchBound = Some(bound))
- val pipeline = plugin.ExtractionPhase andThen leon.utils.SubtypingPhase
+ val pipeline = frontends.scalac.ExtractionPhase andThen leon.utils.SubtypingPhase
val program = pipeline.run(ctx)(f.getAbsolutePath :: Nil)
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 16f3ce73b..eaf38ca14 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -33,7 +33,7 @@ class SynthesisSuite extends LeonTestSuite {
val opts = SynthesisOptions()
- val pipeline = leon.plugin.TemporaryInputPhase andThen leon.plugin.ExtractionPhase andThen SynthesisProblemExtractionPhase
+ val pipeline = leon.utils.TemporaryInputPhase andThen leon.frontends.scalac.ExtractionPhase andThen SynthesisProblemExtractionPhase
val (program, results) = pipeline.run(ctx)((content, Nil))
diff --git a/src/test/scala/leon/test/termination/TerminationRegression.scala b/src/test/scala/leon/test/termination/TerminationRegression.scala
index f65daf86a..160a20354 100644
--- a/src/test/scala/leon/test/termination/TerminationRegression.scala
+++ b/src/test/scala/leon/test/termination/TerminationRegression.scala
@@ -17,7 +17,7 @@ class TerminationRegression extends LeonTestSuite {
private case class Output(report : TerminationReport, reporter : Reporter)
private def mkPipeline : Pipeline[List[String],TerminationReport] =
- leon.plugin.ExtractionPhase andThen leon.utils.SubtypingPhase andThen leon.termination.TerminationPhase
+ leon.frontends.scalac.ExtractionPhase andThen leon.utils.SubtypingPhase andThen leon.termination.TerminationPhase
private def mkTest(file : File, leonOptions: Seq[LeonOption], forError: Boolean)(block: Output=>Unit) = {
val fullName = file.getPath()
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index e5692fca0..de6acd0f1 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -17,7 +17,7 @@ class PureScalaVerificationRegression extends LeonTestSuite {
private case class Output(report : VerificationReport, reporter : Reporter)
private def mkPipeline : Pipeline[List[String],VerificationReport] =
- leon.plugin.ExtractionPhase andThen leon.utils.SubtypingPhase andThen leon.verification.AnalysisPhase
+ leon.frontends.scalac.ExtractionPhase andThen leon.utils.SubtypingPhase andThen leon.verification.AnalysisPhase
private def mkTest(file : File, leonOptions : Seq[LeonOption], forError: Boolean)(block: Output=>Unit) = {
val fullName = file.getPath()
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index 6ddab4332..5492bb522 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -17,7 +17,7 @@ class XLangVerificationRegression extends LeonTestSuite {
private case class Output(report : VerificationReport, reporter : Reporter)
private def mkPipeline : Pipeline[List[String],VerificationReport] =
- leon.plugin.ExtractionPhase andThen leon.utils.SubtypingPhase andThen xlang.XlangAnalysisPhase
+ leon.frontends.scalac.ExtractionPhase andThen leon.utils.SubtypingPhase andThen xlang.XlangAnalysisPhase
private def mkTest(file : File, forError: Boolean = false)(block: Output=>Unit) = {
val fullName = file.getPath()
--
GitLab