From 86969a8a8c254c3ef8a1a1760477245f1728bd30 Mon Sep 17 00:00:00 2001 From: "Felix A. Wolf" Date: Fri, 15 Mar 2024 15:37:46 +0100 Subject: [PATCH 1/2] changes to fit with new version of chopper --- .../viper/gobra/reporting/StatsCollector.scala | 17 ++++++++++------- .../scala/viper/gobra/util/ChopperUtil.scala | 11 ++++++----- 2 files changed, 16 insertions(+), 12 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..0a76b24eb 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,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), From 5d0fc77726ba180ad8534b48c3ac404e4b5d74b3 Mon Sep 17 00:00:00 2001 From: jcp19 <6281876+jcp19@users.noreply.github.com> Date: Mon, 25 Mar 2024 13:09:00 +0000 Subject: [PATCH 2/2] Updates submodules --- viperserver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/viperserver b/viperserver index b70fa9522..9ba8d2b0f 160000 --- a/viperserver +++ b/viperserver @@ -1 +1 @@ -Subproject commit b70fa95224a7f5ae3e3de8579e28d685eaf93f6e +Subproject commit 9ba8d2b0fe1f466f9ab301e2fb87d80b205a69df