Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Reduce Function Call Graph Computations for Termination Plugin #719

Merged
merged 4 commits into from
Jul 12, 2023
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
removes memoization as it's useless due to the closure
  • Loading branch information
ArquintL committed Jul 12, 2023
commit 243a193a58cfaf3bda8892512a70db10001450bd
32 changes: 15 additions & 17 deletions src/main/scala/viper/silver/ast/utility/Functions.scala
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,6 @@ import org.jgrapht.alg.connectivity.GabowStrongConnectivityInspector
import org.jgrapht.graph.{DefaultDirectedGraph, DefaultEdge}
import org.jgrapht.traverse.TopologicalOrderIterator

import scala.collection.mutable
import scala.collection.mutable.{ListBuffer, Set => MSet}
import scala.jdk.CollectionConverters._

Expand Down Expand Up @@ -46,31 +45,30 @@ object Functions {
subexpressions
}

val functionCallGraphCache: mutable.Map[(Program, Function => Seq[Exp]), DefaultDirectedGraph[Function, DefaultEdge]] = mutable.SeqMap.empty
/** Returns the call graph of a given program (also considering specifications as calls). Call graphs are memoized.
*
* TODO: Memoize invocations of `getFunctionCallgraph`. Note that it's unclear how to derive a useful key from `subs`
*/
def getFunctionCallgraph(program: Program, subs: Function => Seq[Exp] = allSubexpressions)
: DefaultDirectedGraph[Function, DefaultEdge] = {
functionCallGraphCache.getOrElseUpdate((program, subs), {
val graph = new DefaultDirectedGraph[Function, DefaultEdge](classOf[DefaultEdge])
val graph = new DefaultDirectedGraph[Function, DefaultEdge](classOf[DefaultEdge])

for (f <- program.functions) {
graph.addVertex(f)
}
for (f <- program.functions) {
graph.addVertex(f)
}

def process(f: Function, e: Exp): Unit = {
e visit {
case FuncApp(f2name, _) =>
graph.addEdge(f, program.findFunction(f2name))
}
def process(f: Function, e: Exp): Unit = {
e visit {
case FuncApp(f2name, _) =>
graph.addEdge(f, program.findFunction(f2name))
}
}

for (f <- program.functions) {
subs(f) foreach (process(f, _))
}
for (f <- program.functions) {
subs(f) foreach (process(f, _))
}

graph
})
graph
}
/**
* Computes the height of every function. If the height h1 of a function f1 is
Expand Down