changes to fit with new version of chopper

viperproject · Mar 15, 2024 · 86969a8 · 86969a8
1 parent be5c16d
commit 86969a8
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 12 deletions.
diff --git a/src/main/scala/viper/gobra/reporting/StatsCollector.scala b/src/main/scala/viper/gobra/reporting/StatsCollector.scala
@@ -14,7 +14,8 @@ import viper.gobra.frontend.Config
 import viper.gobra.frontend.info.{Info, TypeInfo}
 import viper.gobra.util.Violation
 import viper.silver.ast.{Function, Member, Method, Predicate}
-import viper.silver.ast.utility.Chopper.{Edges, Vertex}
+import viper.silver.ast.utility.chopper.{Edges, Vertices}
+import viper.silver.ast.utility.chopper.Vertices.Vertex
 import viper.silver.reporter.Time
 
 import scala.collection.concurrent.{Map, TrieMap}
@@ -162,7 +163,7 @@ case class StatsCollector(reporter: GobraReporter) extends GobraReporter {
               taskName,
               time,
               ViperNodeType.withName(viperMember.getClass.getSimpleName),
-              Edges.dependencies(viperMember).flatMap(edge => vertexToName(edge._2)).toSet,
+              EdgesImpl.dependencies(viperMember).flatMap(edge => vertexToName(edge._2)).toSet,
               success,
               cached,
               memberInfo.isImported,
@@ -193,6 +194,8 @@ case class StatsCollector(reporter: GobraReporter) extends GobraReporter {
     reporter.report(msg)
   }
 
+  private object EdgesImpl extends Edges with Vertices
+
   private def gobraMemberKey(pkgId: String,memberName: String, args: String): String = pkgId + "." + memberName + args
 
   private def viperMemberKey(taskName: String, viperMemberName: String): String = taskName + "-" + viperMemberName
@@ -241,11 +244,11 @@ case class StatsCollector(reporter: GobraReporter) extends GobraReporter {
    * for the statistics
    */
   private def vertexToName(vertex: Vertex): Option[String] = vertex match {
-    case Vertex.Method(name) => Some(name)
-    case Vertex.MethodSpec(name) => Some(name)
-    case Vertex.Function(name) => Some(name)
-    case Vertex.PredicateBody(name) => Some(name)
-    case Vertex.PredicateSig(name) => Some(name)
+    case Vertices.Method(name) => Some(name)
+    case Vertices.MethodSpec(name) => Some(name)
+    case Vertices.Function(name) => Some(name)
+    case Vertices.PredicateBody(name) => Some(name)
+    case Vertices.PredicateSig(name) => Some(name)
     case _ => None
   }
 

diff --git a/src/main/scala/viper/gobra/util/ChopperUtil.scala b/src/main/scala/viper/gobra/util/ChopperUtil.scala
@@ -12,7 +12,7 @@ import java.nio.file.Files
 import java.util.Properties
 import viper.silver.{ast => vpr}
 import viper.silver.ast.SourcePosition
-import viper.silver.ast.utility.Chopper
+import viper.silver.ast.utility.chopper
 import viper.gobra.frontend.{Config, PackageInfo}
 import viper.gobra.reporting.ChoppedViperMessage
 import viper.gobra.backend.BackendVerifier.Task
@@ -25,7 +25,7 @@ object ChopperUtil {
   def computeChoppedPrograms(task: Task, pkgInfo: PackageInfo)(config: Config): Vector[vpr.Program] = {
 
 
-    val programs = Chopper.chop(task.program)(
+    val programs = chopper.Chopper.chop(task.program)(
       selection = computeIsolateMap(config, pkgInfo),
       bound = Some(config.choppingUpperBound),
       penalty = getPenalty
@@ -71,9 +71,9 @@ object ChopperUtil {
     * then a penalty object using this configuration is created and returned.
     * Otherwise, if no configuration is present, the default configuration is returned.
     * */
-  def getPenalty: Chopper.Penalty[Chopper.Vertex] = {
+  def getPenalty: chopper.Penalty[chopper.Vertices.Vertex] = {
     import scala.io.Source
-    import viper.silver.ast.utility.Chopper.Penalty
+    import viper.silver.ast.utility.chopper.Penalty
 
     val file = new File(GobraChopperFileLocation)
     if (!file.exists()) {
@@ -90,7 +90,8 @@ object ChopperUtil {
       val penaltyConf = Penalty.PenaltyConfig(
         method          = get("method_body",      dfltConf.method),
         methodSpec      = get("method_spec",      dfltConf.methodSpec),
-        function        = get("function",         dfltConf.function),
+        function        = get("function_body",    dfltConf.function),
+        functionSig     = get("function_spec",    dfltConf.function),
         predicate       = get("predicate_body",   dfltConf.predicate),
         predicateSig    = get("predicate_spec",   dfltConf.predicateSig),
         field           = get("field",            dfltConf.field),