Skip to content
Snippets Groups Projects
Commit 6909c0f9 authored by Régis Blanc's avatar Régis Blanc
Browse files

complete hoist ite for nary expressions

parent e4b04d27
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/main/scala/leon/CallGraph.scala
+ 61
− 48
View file @ 6909c0f9
...@@ -26,22 +26,76 @@ class CallGraph(val program: Program) { ...@@ -26,22 +26,76 @@ class CallGraph(val program: Program) {
null null
} }
//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 hoistIte(expr: Expr): Expr = {
def transform(expr: Expr): Option[Expr] = expr match {
def transform(expr: Expr): Expr = expr match { case uop@UnaryOperator(IfExpr(c, t, e), op) => Some(IfExpr(c, op(t).setType(uop.getType), op(e).setType(uop.getType)).setType(uop.getType))
case ite@IfExpr(c, t, e) => ite case bop@BinaryOperator(IfExpr(c, t, e), t2, op) => Some(IfExpr(c, op(t, t2).setType(bop.getType), op(e, t2).setType(bop.getType)).setType(bop.getType))
case BinaryOperator(IfExpr(c, t, e), t2, op) => IfExpr(c, op(t, t2), op(e, t2)) case bop@BinaryOperator(t1, IfExpr(c, t, e), op) => Some(IfExpr(c, op(t1, t).setType(bop.getType), op(t1, e).setType(bop.getType)).setType(bop.getType))
case BinaryOperator(t1, IfExpr(c, t, e), op) => IfExpr(c, op(t1, t), op(t1, e)) case nop@NAryOperator(ts, op) => {
case (t: Terminal) => t val iteIndex = ts.indexWhere{ case IfExpr(_, _, _) => true case _ => false }
if(iteIndex == -1) None else {
val (beforeIte, startIte) = ts.splitAt(iteIndex)
val afterIte = startIte.tail
val IfExpr(c, t, e) = startIte.head
Some(IfExpr(c,
op(beforeIte ++ Seq(t) ++ afterIte).setType(nop.getType),
op(beforeIte ++ Seq(e) ++ afterIte).setType(nop.getType)
).setType(nop.getType))
}
}
case _ => None
} }
def fix[A](f: (A) => A, a: A): A = { def fix[A](f: (A) => A, a: A): A = {
val na = f(a) val na = f(a)
if(a == na) a else fix(f, na) if(a == na) a else fix(f, na)
} }
fix(transform, expr) 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")
// val allFuns = program.definedFunctions
// allFuns.foreach(fd => {
// val testcases = generateTestCases(fd)
// reporter.info("Running " + fd.id + " with the following testcases:\n")
// reporter.info(testcases.mkString("\n"))
// })
//}
//private def generatePathConditions(funDef: FunDef): Seq[Expr] = if(!funDef.hasImplementation) Seq() else {
// val body = funDef.body.get
// val cleanBody = expandLets(matchToIfThenElse(body))
// collectWithPathCondition(cleanBody)
//}
}
//def hoistIte(expr: Expr): (Seq[Expr] => Expr, Seq[Expr]) = expr match { //def hoistIte(expr: Expr): (Seq[Expr] => Expr, Seq[Expr]) = expr match {
// case ite@IfExpr(c, t, e) => { // case ite@IfExpr(c, t, e) => {
// val (iteThen, valsThen) = hoistIte(t) // val (iteThen, valsThen) = hoistIte(t)
...@@ -84,44 +138,3 @@ class CallGraph(val program: Program) { ...@@ -84,44 +138,3 @@ class CallGraph(val program: Program) {
// case _ => scala.sys.error("Unhandled tree in hoistIte : " + expr) // case _ => scala.sys.error("Unhandled tree in hoistIte : " + 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")
// val allFuns = program.definedFunctions
// allFuns.foreach(fd => {
// val testcases = generateTestCases(fd)
// reporter.info("Running " + fd.id + " with the following testcases:\n")
// reporter.info(testcases.mkString("\n"))
// })
//}
//private def generatePathConditions(funDef: FunDef): Seq[Expr] = if(!funDef.hasImplementation) Seq() else {
// val body = funDef.body.get
// val cleanBody = expandLets(matchToIfThenElse(body))
// collectWithPathCondition(cleanBody)
//}
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment