diff --git a/src/main/scala/leon/CallGraph.scala b/src/main/scala/leon/CallGraph.scala index 33627642d2535744eb7155a5f424becd3bca9bf7..00a1d916aefec03ca801d4e5d4106af2c76a1155 100644 --- a/src/main/scala/leon/CallGraph.scala +++ b/src/main/scala/leon/CallGraph.scala @@ -11,21 +11,74 @@ class CallGraph(val program: Program) { case class FunctionStart(fd: FunDef) extends ProgramPoint case class ExpressionPoint(wp: Expr) extends ProgramPoint - sealed abstract class EdgeLabel - case class ConditionLabel(expr: Expr) extends EdgeLabel { - require(expr.getType == BooleanType) - } - case class FunctionInvocLabel(fd: FunDef, args: List[Expr]) extends EdgeLabel { - require(args.zip(fd.args).forall(p => p._1.getType == p._2.getType)) - } + //sealed abstract class EdgeLabel + //case class ConditionLabel(expr: Expr) extends EdgeLabel { + // require(expr.getType == BooleanType) + //} + //case class FunctionInvocLabel(fd: FunDef, args: List[Expr]) extends EdgeLabel { + // require(args.zip(fd.args).forall(p => p._1.getType == p._2.getType)) + //} + case class TransitionLabel(cond: Expr, assignment: Map[Variable, Expr]) + + private lazy val graph: Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]] = buildGraph + - private lazy val graph: Map[ProgramPoint, Set[EdgeLabel]] = buildGraph + private def buildGraph: Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]] = { + //var fd2point: Map[FunDef, ProgramPoint] = Map() + program.definedFunctions.foreach(fd => { + val body = fd.body.get + //val cleanBody = hoistIte(expandLets(matchToIfThenElse(body))) + val cleanBody = expandLets(matchToIfThenElse(body)) + // collectWithPathCondition(cleanBody).foreach{ + // case (path, WayPoint) => + + }) - private def buildGraph: Map[ProgramPoint, Set[EdgeLabel]] = { null } + private def collectWithPathCondition(expression: Expr, startingPoint: ProgramPoint): Map[ProgramPoint, (ProgramPoint, Set[TransitionLabel])] = { + var callGraph: Map[ProgramPoint, Set[(ProgramPoint, TransitionLabel)]] = Map() + + def rec(expr: Expr, path: List[Expr], startingPoint: ProgramPoint): Unit = expr match { + case FunctionInvocation(fd, args) => { + val transitions: Set[(ProgramPoint, TransitionLabel)] = callGraph.get(startingPoint) match { + case None => Set() + case Some(s) => s + } + val newPoint = FunctionStart(fd) + val newTransition = TransitionLabel(And(path.toSeq), fd.args.zip(args).map{ case (VarDecl(id, _), arg) => (id.toVariable, arg) }.toMap) + callGraph += (startingPoint -> (transitions + (newPoint, newTransition))) + args.foreach(arg => rec(arg, startingPoint, startingPoint)) + } + case WayPoint(e) => { + val transitions: Set[(ProgramPoint, TransitionLabel)] = callGraph.get(startingPoint) match { + case None => Set() + case Some(s) => s + } + val newPoint = ExpressionPoint(expr) + val newTransition = TransitionLabel(And(path.toSeq), fd.args.zip(args).map{ case (VarDecl(id, _), arg) => (id.toVariable, arg) }.toMap) + callGraph += (startingPoint -> (transitions + (newPoint, newTransition))) + rec(e, List(), newPoint) + } + case IfExpr(cond, then, elze) => { + rec(cond, path, startingPoint) + rec(then, cond :: path, startingPoint) + rec(elze, Not(cond) :: path, startingPoint) + } + case NAryOperator(args, _) => args.foreach(rec(_, path, startingPoint)) + case BinaryOperator(t1, t2, _) => rec(t1, path, startingPoint); rec(t2, path, startingPoint) + case UnaryOperator(t, _) => rec(t, path, startingPoint) + case t : Terminal => ; + case _ => scala.sys.error("Unhandled tree in collectWithPathCondition : " + expr) + } + + rec(expression, List(), startingPoint) + callGraph + } + + //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 = { def transform(expr: Expr): Option[Expr] = expr match { @@ -54,29 +107,6 @@ class CallGraph(val program: Program) { fix(searchAndReplaceDFS(transform), expr) } - // prec: there should be no lets and no pattern-matching in this expression - //private def collectWithPathCondition(expression: Expr, cond: Seq[Expr]): Seq[Expr] = { - // var allPaths: Seq[Expr] = Seq() - - // def rec(expr: Expr, path: Seq[Expr]): Seq[Expr] = { - // expr match { - // case FunctionInvocLabel(fd, args) => - // case WayPoint(e) => - // } - // - // case IfExpr(cond, then, elze) => - // (if(!containsIfExpr(then)) Seq(And(path, cond)) else rec(then, And(cond, path))) ++ - // (if(!containsIfExpr(elze)) Seq(And(path, Not(cond))) else rec(then, And(cond, path))) - // case NAryOperator(args, _) => args.flatMap(arg => rec(arg, path)) - // case BinaryOperator(t1, t2, _) => rec(t1, path) ++ rec(t2, path) - // case UnaryOperator(t, _) => rec(t, path) - // case t : Terminal => Seq() - // case _ => scala.sys.error("Unhandled tree in collectWithPathCondition : " + expr) - // } - - // rec(expression, BooleanLiteral(true)).distinct - //} - //def analyse(program: Program) { // z3Solver.setProgram(program) // reporter.info("Running test generation")