From 4eab947c49ad6219bcaa3616cb0edb64a264647c Mon Sep 17 00:00:00 2001 From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch> Date: Mon, 23 Nov 2015 14:35:05 +0100 Subject: [PATCH] Improvements --- .../invariant/structure/FunctionUtils.scala | 11 +++----- .../scala/leon/invariant/util/CallGraph.scala | 28 ++++++------------- .../scala/leon/purescala/Extractors.scala | 14 ++++------ 3 files changed, 18 insertions(+), 35 deletions(-) diff --git a/src/main/scala/leon/invariant/structure/FunctionUtils.scala b/src/main/scala/leon/invariant/structure/FunctionUtils.scala index a0acdcda7..565a6f9f4 100644 --- a/src/main/scala/leon/invariant/structure/FunctionUtils.scala +++ b/src/main/scala/leon/invariant/structure/FunctionUtils.scala @@ -5,13 +5,11 @@ import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ import purescala.ExprOps._ -import purescala.Extractors._ import purescala.Types._ import invariant.factories._ import invariant.util._ import Util._ import PredicateUtil._ -import ProgramUtil._ import scala.language.implicitConversions /** @@ -37,8 +35,8 @@ object FunctionUtils { def isTemplateInvocation(finv: Expr) = { finv match { case FunctionInvocation(funInv, args) => - (funInv.id.name == "tmpl" && funInv.returnType == BooleanType && - args.size == 1 && args(0).isInstanceOf[Lambda]) + funInv.id.name == "tmpl" && funInv.returnType == BooleanType && + args.size == 1 && args(0).isInstanceOf[Lambda] case _ => false } @@ -46,8 +44,7 @@ object FunctionUtils { def isQMark(e: Expr) = e match { case FunctionInvocation(TypedFunDef(fd, Seq()), args) => - (fd.id.name == "?" && fd.returnType == IntegerType && - args.size <= 1) + fd.id.name == "?" && fd.returnType == IntegerType && args.size <= 1 case _ => false } @@ -104,7 +101,7 @@ object FunctionUtils { val Lambda(_, postBody) = fd.postcondition.get // collect all terms with question marks and convert them to a template val postWoQmarks = postBody match { - case And(args) if args.exists(exists(isQMark) _) => + case And(args) if args.exists(exists(isQMark)) => val (tempExprs, otherPreds) = args.partition { case a if exists(isQMark)(a) => true case _ => false diff --git a/src/main/scala/leon/invariant/util/CallGraph.scala b/src/main/scala/leon/invariant/util/CallGraph.scala index 23f87d5bc..5e93c4512 100644 --- a/src/main/scala/leon/invariant/util/CallGraph.scala +++ b/src/main/scala/leon/invariant/util/CallGraph.scala @@ -1,15 +1,10 @@ package leon package invariant.util -import purescala._ -import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ import purescala.ExprOps._ -import purescala.Extractors._ -import purescala.Types._ import ProgramUtil._ -import Util._ import invariant.structure.FunctionUtils._ import invariant.datastructure._ @@ -71,7 +66,7 @@ class CallGraph { graph.getNodes.toList.foreach((f) => { var inserted = false var index = 0 - for (i <- 0 to funcList.length - 1) { + for (i <- funcList.indices) { if (!inserted && this.transitivelyCalls(funcList(i), f)) { index = i inserted = true @@ -97,7 +92,6 @@ class CallGraph { object CallGraphUtil { def constructCallGraph(prog: Program, onlyBody: Boolean = false, withTemplates: Boolean = false): CallGraph = { -// // println("Constructing call graph") val cg = new CallGraph() functionsWOFields(prog.definedFunctions).foreach((fd) => { @@ -125,17 +119,11 @@ object CallGraphUtil { cg } - def getCallees(expr: Expr): Set[FunDef] = { - var callees = Set[FunDef]() - simplePostTransform((expr) => expr match { - //note: do not consider field invocations - case FunctionInvocation(TypedFunDef(callee, _), args) - if callee.isRealFunction => { - callees += callee - expr - } - case _ => expr - })(expr) - callees - } + def getCallees(expr: Expr): Set[FunDef] = collect { + case expr@FunctionInvocation(TypedFunDef(callee, _), _) if callee.isRealFunction => + Set(callee) + case _ => + Set[FunDef]() + }(expr) + } \ No newline at end of file diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala index 1337e74d0..c8cf8f118 100644 --- a/src/main/scala/leon/purescala/Extractors.scala +++ b/src/main/scala/leon/purescala/Extractors.scala @@ -357,22 +357,20 @@ object Extractors { } def unapply(me : MatchExpr) : Option[(Pattern, Expr, Expr)] = { - if (me eq null) None else { me match { + Option(me) collect { case MatchExpr(scrut, List(SimpleCase(pattern, body))) if !aliased(pattern.binders, variablesOf(scrut)) => - Some(( pattern, scrut, body )) - case _ => None - }} + ( pattern, scrut, body ) + } } } object LetTuple { def unapply(me : MatchExpr) : Option[(Seq[Identifier], Expr, Expr)] = { - if (me eq null) None else { me match { + Option(me) collect { case LetPattern(TuplePattern(None,subPatts), value, body) if subPatts forall { case WildcardPattern(Some(_)) => true; case _ => false } => - Some((subPatts map { _.binder.get }, value, body )) - case _ => None - }} + (subPatts map { _.binder.get }, value, body ) + } } } -- GitLab