From 9b0fa71f68d196ec55c857e54aa66f29e6f765f6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 16 May 2012 05:42:45 +0000
Subject: [PATCH] find a path between two point
---
src/main/scala/leon/CallGraph.scala | 47 ++++++++++++++++++-
src/main/scala/leon/TestGeneration.scala | 1 +
.../scala/leon/purescala/PrettyPrinter.scala | 6 +++
3 files changed, 53 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/CallGraph.scala b/src/main/scala/leon/CallGraph.scala
index 2da4663af..ad78bfa11 100644
--- a/src/main/scala/leon/CallGraph.scala
+++ b/src/main/scala/leon/CallGraph.scala
@@ -21,6 +21,9 @@ class CallGraph(val program: Program) {
case class TransitionLabel(cond: Expr, assignment: Map[Variable, Expr])
private lazy val graph: Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]] = buildGraph
+ private lazy val programPoints: Set[ProgramPoint] = {
+ graph.flatMap(pair => pair._2.map(edge => edge._1).toSet + pair._1).toSet
+ }
private def buildGraph: Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]] = {
var callGraph: Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]] = Map()
@@ -81,9 +84,51 @@ class CallGraph(val program: Program) {
callGraph
}
+ def findAllPathes: Set[Seq[(ProgramPoint, ProgramPoint, TransitionLabel)]] = {
+ val waypoints: Set[ProgramPoint] = programPoints.filter{ case ExpressionPoint(_) => true case _ => false }
+ val sortedWaypoints: Seq[ProgramPoint] = waypoints.toSeq.sortWith((p1, p2) => {
+ val (ExpressionPoint(Waypoint(i1, _)), ExpressionPoint(Waypoint(i2, _))) = (p1, p2)
+ i1 <= i2
+ })
+ Set(findPath(sortedWaypoints(0), sortedWaypoints(1)))
+ }
+
//find a path that goes through all waypoint in order
- //def findPath
+ def findPath(from: ProgramPoint, to: ProgramPoint): Seq[(ProgramPoint, ProgramPoint, TransitionLabel)] = {
+ var visitedPoints: Set[ProgramPoint] = Set()
+ var history: Map[ProgramPoint, (ProgramPoint, TransitionLabel)] = Map()
+ var toVisit: List[ProgramPoint] = List(from)
+ var currentPoint: ProgramPoint = null
+ while(!toVisit.isEmpty && currentPoint != to) {
+ currentPoint = toVisit.head
+ if(currentPoint != to) {
+ visitedPoints += currentPoint
+ toVisit = toVisit.tail
+ graph.get(currentPoint).foreach(edges => edges.foreach{
+ case (neighbour, transition) =>
+ if(!visitedPoints.contains(neighbour) && !toVisit.contains(neighbour)) {
+ toVisit ::= neighbour
+ history += (neighbour -> ((currentPoint, transition)))
+ }
+ })
+ }
+ }
+
+ def rebuildPath(point: ProgramPoint, path: List[(ProgramPoint, ProgramPoint, TransitionLabel)]): Seq[(ProgramPoint, ProgramPoint, TransitionLabel)] = {
+ if(point == from) path else {
+ val (previousPoint, transition) = history(point)
+ val newPath = (previousPoint, point, transition) :: path
+ rebuildPath(previousPoint, newPath)
+ }
+ }
+
+ //TODO: handle case where the target node is not found
+ println(history)
+ println(from)
+ println(to)
+ rebuildPath(to, List())
+ }
//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 = {
diff --git a/src/main/scala/leon/TestGeneration.scala b/src/main/scala/leon/TestGeneration.scala
index 421d4dec3..469c91fdd 100644
--- a/src/main/scala/leon/TestGeneration.scala
+++ b/src/main/scala/leon/TestGeneration.scala
@@ -18,6 +18,7 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
def analyse(program: Program) {
val callGraph = new CallGraph(program)
println(callGraph.toDotString)
+ println(callGraph.findAllPathes)
//z3Solver.setProgram(program)
//reporter.info("Running test generation")
//val allFuns = program.definedFunctions
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 21a9393b1..b7b5bd343 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -154,6 +154,12 @@ object PrettyPrinter {
nsb
}
+ case Waypoint(i, expr) => {
+ sb.append("waypoint_" + i + "(")
+ pp(expr, sb, lvl)
+ sb.append(")")
+ }
+
case OptionSome(a) => {
var nsb = sb
nsb.append("Some(")
--
GitLab