From 072c62a2a985fd7eb2e5865de7456da560bb6262 Mon Sep 17 00:00:00 2001
From: viper-admin <59963956+viper-admin@users.noreply.github.com>
Date: Fri, 15 Mar 2024 17:33:20 +0100
Subject: [PATCH] Update Submodules (#743)

* Updates submodules

* changes to fit with new version of chopper

* removed entry from penalty config that will is going to be necessary for the next submodule update

---------

Co-authored-by: jcp19 <6281876+jcp19@users.noreply.github.com>
Co-authored-by: Felix A. Wolf <felix.wolf@inf.ethz.ch>
---
 .../viper/gobra/reporting/StatsCollector.scala  | 17 ++++++++++-------
 .../scala/viper/gobra/util/ChopperUtil.scala    | 10 +++++-----
 viperserver                                     |  2 +-
 3 files changed, 16 insertions(+), 13 deletions(-)

diff --git a/src/main/scala/viper/gobra/reporting/StatsCollector.scala b/src/main/scala/viper/gobra/reporting/StatsCollector.scala
index 611689580..ffc915ba8 100644
--- 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
index 0489716ac..d69291bf9 100644
--- 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,7 @@ 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),
         predicate       = get("predicate_body",   dfltConf.predicate),
         predicateSig    = get("predicate_spec",   dfltConf.predicateSig),
         field           = get("field",            dfltConf.field),
diff --git a/viperserver b/viperserver
index 0c7aee077..cadcb1c5a 160000
--- a/viperserver
+++ b/viperserver
@@ -1 +1 @@
-Subproject commit 0c7aee0774190e0bfb95d04d60aa3388ab004c19
+Subproject commit cadcb1c5aa887ace1d4b0afb6586afdeca6c0da1