From 1634a6aa0f96cf671790f050ce37596ab6331b4e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 16 May 2012 02:30:52 +0000
Subject: [PATCH] parse and handle waypoints
---
src/main/scala/leon/CallGraph.scala | 9 ++++++---
src/main/scala/leon/Utils.scala | 3 +++
src/main/scala/leon/plugin/CodeExtraction.scala | 5 +++++
src/main/scala/leon/plugin/Extractors.scala | 13 +++++++++++++
src/main/scala/leon/purescala/Trees.scala | 4 ++--
5 files changed, 29 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/CallGraph.scala b/src/main/scala/leon/CallGraph.scala
index 16fdaf884..2da4663af 100644
--- a/src/main/scala/leon/CallGraph.scala
+++ b/src/main/scala/leon/CallGraph.scala
@@ -54,12 +54,12 @@ class CallGraph(val program: Program) {
callGraph += (startingPoint -> (transitions + ((newPoint, newTransition))))
args.foreach(arg => rec(arg, path, startingPoint))
}
- case WayPoint(e) => {
+ case way@Waypoint(i, e) => {
val transitions: Set[(ProgramPoint, TransitionLabel)] = callGraph.get(startingPoint) match {
case None => Set()
case Some(s) => s
}
- val newPoint = ExpressionPoint(expr)
+ val newPoint = ExpressionPoint(way)
val newTransition = TransitionLabel(And(path.toSeq), Map())
callGraph += (startingPoint -> (transitions + ((newPoint, newTransition))))
rec(e, List(), newPoint)
@@ -81,6 +81,9 @@ class CallGraph(val program: Program) {
callGraph
}
+ //find a path that goes through all waypoint in order
+ //def findPath
+
//guarentee that all IfExpr will be at the top level and as soon as you encounter a non-IfExpr, then no more IfExpr can be find in the sub-expressions
def hoistIte(expr: Expr): Expr = {
@@ -129,7 +132,7 @@ class CallGraph(val program: Program) {
def ppPoint(p: ProgramPoint): String = p match {
case FunctionStart(fd) => fd.id.name
- case ExpressionPoint(WayPoint(e)) => "WayPoint"
+ case ExpressionPoint(Waypoint(i, e)) => "WayPoint " + i
case _ => sys.error("Unexpected programPoint: " + p)
}
def ppLabel(l: TransitionLabel): String = {
diff --git a/src/main/scala/leon/Utils.scala b/src/main/scala/leon/Utils.scala
index ae60002b6..15006c7bc 100644
--- a/src/main/scala/leon/Utils.scala
+++ b/src/main/scala/leon/Utils.scala
@@ -16,4 +16,7 @@ object Utils {
def invariant(x: Boolean): Unit = ()
}
implicit def while2Invariant(u: Unit) = InvariantFunction
+
+
+ def waypoint[A](i: Int, expr: A): A = expr
}
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index ae7d8c0e5..b89dc39db 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -680,6 +680,11 @@ trait CodeExtraction extends Extractors {
}
Epsilon(c1).setType(pstpe).setPosInfo(epsi.pos.line, epsi.pos.column)
}
+ case ExWaypointExpression(tpe, i, tree) => {
+ val pstpe = scalaType2PureScala(unit, silent)(tpe)
+ val IntLiteral(ri) = rec(i)
+ Waypoint(ri, rec(tree)).setType(pstpe)
+ }
case ExSomeConstruction(tpe, arg) => {
// println("Got Some !" + tpe + ":" + arg)
val underlying = scalaType2PureScala(unit, silent)(tpe)
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index a3313663b..eae464827 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -174,6 +174,19 @@ trait Extractors {
case _ => None
}
}
+ object ExWaypointExpression {
+ def unapply(tree: Apply) : Option[(Type, Tree, Tree)] = tree match {
+ case Apply(
+ TypeApply(Select(Select(funcheckIdent, utilsName), waypoint), typeTree :: Nil),
+ List(i, expr)) => {
+ if (utilsName.toString == "Utils" && waypoint.toString == "waypoint")
+ Some((typeTree.tpe, i, expr))
+ else
+ None
+ }
+ case _ => None
+ }
+ }
object ExValDef {
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 871d7b4e0..fdef941c6 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -85,7 +85,7 @@ object Trees {
}
case class TupleSelect(tuple: Expr, index: Int) extends Expr
- case class WayPoint(expr: Expr) extends Expr
+ case class Waypoint(i: Int, expr: Expr) extends Expr
object MatchExpr {
def apply(scrutinee: Expr, cases: Seq[MatchCase]) : MatchExpr = {
@@ -442,7 +442,7 @@ object Trees {
case ArrayLength(a) => Some((a, ArrayLength))
case ArrayClone(a) => Some((a, ArrayClone))
case ArrayMake(t) => Some((t, ArrayMake))
- case WayPoint(t) => Some((t, WayPoint))
+ case Waypoint(i, t) => Some((t, (expr: Expr) => Waypoint(i, expr)))
case e@Epsilon(t) => Some((t, (expr: Expr) => Epsilon(expr).setType(e.getType).setPosInfo(e)))
case _ => None
}
--
GitLab