From a7c176f56690fec8b6b68205c2f66aa5609d7eb5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com> Date: Wed, 16 May 2012 09:52:21 +0200 Subject: [PATCH] find one path among multiple waypoints --- src/main/scala/leon/CallGraph.scala | 14 +++++++++++++- src/main/scala/leon/TestGeneration.scala | 5 ++++- 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/src/main/scala/leon/CallGraph.scala b/src/main/scala/leon/CallGraph.scala index b3402d39a..eaff99e67 100644 --- a/src/main/scala/leon/CallGraph.scala +++ b/src/main/scala/leon/CallGraph.scala @@ -84,13 +84,25 @@ class CallGraph(val program: Program) { callGraph } + //given a path, follow the path to build the logical constraint that need to be satisfiable + def pathConstraint(path: Seq[(ProgramPoint, ProgramPoint, TransitionLabel)], assigns: List[Map[Expr, Expr]] = List()): Expr = { + if(path.isEmpty) BooleanLiteral(true) else { + val (_, _, TransitionLabel(cond, assign)) = path.head + val finalCond = assigns.foldRight(cond)((map, acc) => replace(map, acc)) + And(finalCond, pathConstraint(path.tail, assign.asInstanceOf[Map[Expr, Expr]] :: assigns)) + } + } + 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))) + Set( + sortedWaypoints.zip(sortedWaypoints.tail).foldLeft(Seq[(ProgramPoint, ProgramPoint, TransitionLabel)]())((path, waypoint) => + path ++ findPath(waypoint._1, waypoint._2)) + ) } //find a path that goes through all waypoint in order diff --git a/src/main/scala/leon/TestGeneration.scala b/src/main/scala/leon/TestGeneration.scala index 469c91fdd..a469ee54c 100644 --- a/src/main/scala/leon/TestGeneration.scala +++ b/src/main/scala/leon/TestGeneration.scala @@ -18,7 +18,10 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) { def analyse(program: Program) { val callGraph = new CallGraph(program) println(callGraph.toDotString) - println(callGraph.findAllPathes) + callGraph.findAllPathes.foreach(path => { + println("Path is: " + path) + println("constraint is: " + callGraph.pathConstraint(path)) + }) //z3Solver.setProgram(program) //reporter.info("Running test generation") //val allFuns = program.definedFunctions -- GitLab