From efdbce0909852b48622e1bcfeab2d16ca45c9f74 Mon Sep 17 00:00:00 2001 From: Simon Hostettler Date: Sat, 23 Dec 2023 13:53:41 +0100 Subject: [PATCH 1/2] added submitter to GoVerifier, flag to config --- src/main/scala/viper/gobra/Gobra.scala | 31 +++++++++++++++++++ .../scala/viper/gobra/frontend/Config.scala | 14 +++++++++ 2 files changed, 45 insertions(+) diff --git a/src/main/scala/viper/gobra/Gobra.scala b/src/main/scala/viper/gobra/Gobra.scala index 3b1e71757..2213e7bb6 100644 --- a/src/main/scala/viper/gobra/Gobra.scala +++ b/src/main/scala/viper/gobra/Gobra.scala @@ -17,6 +17,7 @@ import scalaz.Scalaz.futureInstance import viper.gobra.ast.internal.Program import viper.gobra.ast.internal.transform.{CGEdgesTerminationTransform, ConstantPropagation, InternalTransform, OverflowChecksTransform} import viper.gobra.backend.BackendVerifier +import viper.gobra.backend.ViperBackends.{CarbonBackend, SiliconBackend} import viper.gobra.frontend.PackageResolver.{AbstractPackage, RegularPackage} import viper.gobra.frontend.Parser.ParseResult import viper.gobra.frontend.info.{Info, TypeInfo} @@ -26,6 +27,8 @@ import viper.gobra.translator.Translator import viper.gobra.util.Violation.{KnownZ3BugException, LogicException, UglyErrorMessage} import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext} import viper.silicon.BuildInfo +import viper.silver.ast.pretty.FastPrettyPrinter +import viper.silver.utility.ManualProgramSubmitter import viper.silver.{ast => vpr} import java.time.format.DateTimeFormatter @@ -51,6 +54,8 @@ object GoVerifier { trait GoVerifier extends StrictLogging { + protected var submitters: Map[String, ManualProgramSubmitter] = Map() + def name: String = { this.getClass.getSimpleName } @@ -82,9 +87,18 @@ trait GoVerifier extends StrictLogging { } }) + val viperBackendName: String = config.backend match { + case CarbonBackend => "Carbon" + case SiliconBackend => "Silicon" + } + val timeFormatter = DateTimeFormatter.ofPattern("HH:mm:ss"); config.packageInfoInputMap.keys.foreach(pkgInfo => { val pkgId = pkgInfo.id + + //adds a submitter for this package to submitters if config.submitForEvaluation is set, key is pkgId + createSubmitter(config.submitForEvaluation, pkgId, viperBackendName) + logger.info(s"Verifying package $pkgId [${LocalTime.now().format(timeFormatter)}]") val future = verify(pkgInfo, config.copy(reporter = statsCollector, taskName = pkgId))(executor) .map(result => { @@ -95,6 +109,12 @@ trait GoVerifier extends StrictLogging { warningCount += warnings.size warnings.foreach(w => logger.debug(w)) + submitters.get(pkgId).foreach(s => { + s.setSuccess(result == VerifierResult.Success) + s.submit()} + ) + submitters = submitters.removed(pkgId) + result match { case VerifierResult.Success => logger.info(s"$name found no errors") case VerifierResult.Failure(errors) => @@ -143,6 +163,13 @@ trait GoVerifier extends StrictLogging { if (allErrors.isEmpty) VerifierResult.Success else VerifierResult.Failure(allErrors) } + private def createSubmitter(allowSubmission: Boolean, id: String, verifier: String): Unit = { + if (allowSubmission) { + val submitter = new ManualProgramSubmitter(true, id, "", "Gobra", verifier, Array()) + submitters = submitters + (id -> submitter) + } + } + protected[this] def verify(pkgInfo: PackageInfo, config: Config)(implicit executor: GobraExecutionContext): Future[VerifierResult] } @@ -163,6 +190,10 @@ class Gobra extends GoVerifier with GoIdeVerifier { viperTask <- performViperEncoding(finalConfig, pkgInfo, program) } yield (viperTask, finalConfig) + submitters.get(pkgInfo.id).foreach(s => task.bimap( + _ => s.setAllowSubmission(false), //don't submit since no viper program could be produced + { case (job, _) => s.setProgram(FastPrettyPrinter.pretty(job.program))})) + task.foldM({ case Vector() => Future(VerifierResult.Success) case errors => Future(VerifierResult.Failure(errors)) diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index fef81bce0..e548347c1 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -74,6 +74,7 @@ object ConfigDefaults { lazy val DefaultParseAndTypeCheckMode: TaskManagerMode = TaskManagerMode.Parallel lazy val DefaultRequireTriggers: Boolean = false lazy val DefaultDisableSetAxiomatization: Boolean = false + lazy val DefaultSubmitForEvaluation: Boolean = false } // More-complete exhale modes @@ -141,6 +142,7 @@ case class Config( // when enabled, all quantifiers without triggers are rejected requireTriggers: Boolean = ConfigDefaults.DefaultRequireTriggers, disableSetAxiomatization: Boolean = ConfigDefaults.DefaultDisableSetAxiomatization, + submitForEvaluation: Boolean = ConfigDefaults.DefaultSubmitForEvaluation, ) { def merge(other: Config): Config = { @@ -192,6 +194,7 @@ case class Config( parseAndTypeCheckMode = parseAndTypeCheckMode, requireTriggers = requireTriggers || other.requireTriggers, disableSetAxiomatization = disableSetAxiomatization || other.disableSetAxiomatization, + submitForEvaluation = submitForEvaluation || other.submitForEvaluation, ) } @@ -247,6 +250,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector parseAndTypeCheckMode: TaskManagerMode = ConfigDefaults.DefaultParseAndTypeCheckMode, requireTriggers: Boolean = ConfigDefaults.DefaultRequireTriggers, disableSetAxiomatization: Boolean = ConfigDefaults.DefaultDisableSetAxiomatization, + submitForEvaluation: Boolean = ConfigDefaults.DefaultSubmitForEvaluation, ) { def shouldParse: Boolean = true def shouldTypeCheck: Boolean = !shouldParseOnly @@ -262,6 +266,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector case _ => Some(positions.toVector) } } + def allowSubmission: Boolean = submitForEvaluation && !shouldChop } trait RawConfig { @@ -306,6 +311,7 @@ trait RawConfig { parseAndTypeCheckMode = baseConfig.parseAndTypeCheckMode, requireTriggers = baseConfig.requireTriggers, disableSetAxiomatization = baseConfig.disableSetAxiomatization, + submitForEvaluation = baseConfig.allowSubmission, ) } @@ -729,6 +735,13 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals default = Some(ConfigDefaults.DefaultDisableSetAxiomatization), noshort = true, ) + + val submitForEvaluation = opt[Boolean](name = "submitForEvaluation", + descr = "Whether to allow storing the current program for future evaluation.", + default = Some(false), + noshort = true + ) + /** * Exception handling */ @@ -909,5 +922,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals parseAndTypeCheckMode = parseAndTypeCheckMode(), requireTriggers = requireTriggers(), disableSetAxiomatization = disableSetAxiomatization(), + submitForEvaluation = submitForEvaluation(), ) } From ba8eb24f8e052565e19449d856eabb11ec7d914f Mon Sep 17 00:00:00 2001 From: Simon Hostettler Date: Sat, 2 Mar 2024 12:00:48 +0100 Subject: [PATCH 2/2] updated submitter code --- src/main/scala/viper/gobra/Gobra.scala | 32 +++++++++++++++++++ .../scala/viper/gobra/frontend/Config.scala | 15 +++++++++ 2 files changed, 47 insertions(+) diff --git a/src/main/scala/viper/gobra/Gobra.scala b/src/main/scala/viper/gobra/Gobra.scala index 3b1e71757..096460439 100644 --- a/src/main/scala/viper/gobra/Gobra.scala +++ b/src/main/scala/viper/gobra/Gobra.scala @@ -17,6 +17,7 @@ import scalaz.Scalaz.futureInstance import viper.gobra.ast.internal.Program import viper.gobra.ast.internal.transform.{CGEdgesTerminationTransform, ConstantPropagation, InternalTransform, OverflowChecksTransform} import viper.gobra.backend.BackendVerifier +import viper.gobra.backend.ViperBackends.{CarbonBackend, SiliconBackend} import viper.gobra.frontend.PackageResolver.{AbstractPackage, RegularPackage} import viper.gobra.frontend.Parser.ParseResult import viper.gobra.frontend.info.{Info, TypeInfo} @@ -27,6 +28,8 @@ import viper.gobra.util.Violation.{KnownZ3BugException, LogicException, UglyErro import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext} import viper.silicon.BuildInfo import viper.silver.{ast => vpr} +import viper.silver.ast.pretty.FastPrettyPrinter +import viper.silver.utility.ManualProgramSubmitter import java.time.format.DateTimeFormatter import java.time.LocalTime @@ -51,6 +54,8 @@ object GoVerifier { trait GoVerifier extends StrictLogging { + protected var submitters: Map[String, ManualProgramSubmitter] = Map() + def name: String = { this.getClass.getSimpleName } @@ -82,9 +87,18 @@ trait GoVerifier extends StrictLogging { } }) + val viperBackendName: String = config.backend match { + case CarbonBackend => "Carbon" + case SiliconBackend => "Silicon" + } + val timeFormatter = DateTimeFormatter.ofPattern("HH:mm:ss"); config.packageInfoInputMap.keys.foreach(pkgInfo => { val pkgId = pkgInfo.id + + //adds a submitter for this package to submitters if config.submitForEvaluation is set, key is pkgId + createSubmitter(config.submitForEvaluation, pkgId, viperBackendName) + logger.info(s"Verifying package $pkgId [${LocalTime.now().format(timeFormatter)}]") val future = verify(pkgInfo, config.copy(reporter = statsCollector, taskName = pkgId))(executor) .map(result => { @@ -95,6 +109,13 @@ trait GoVerifier extends StrictLogging { warningCount += warnings.size warnings.foreach(w => logger.debug(w)) + submitters.get(pkgId).foreach(s => { + s.setSuccess(result == VerifierResult.Success) + s.submit() + } + ) + submitters = submitters.removed(pkgId) + result match { case VerifierResult.Success => logger.info(s"$name found no errors") case VerifierResult.Failure(errors) => @@ -143,6 +164,13 @@ trait GoVerifier extends StrictLogging { if (allErrors.isEmpty) VerifierResult.Success else VerifierResult.Failure(allErrors) } + private def createSubmitter(allowSubmission: Boolean, id: String, verifier: String): Unit = { + if (allowSubmission) { + val submitter = new ManualProgramSubmitter(true, "", "Gobra", verifier, Array()) + submitters = submitters + (id -> submitter) + } + } + protected[this] def verify(pkgInfo: PackageInfo, config: Config)(implicit executor: GobraExecutionContext): Future[VerifierResult] } @@ -163,6 +191,10 @@ class Gobra extends GoVerifier with GoIdeVerifier { viperTask <- performViperEncoding(finalConfig, pkgInfo, program) } yield (viperTask, finalConfig) + submitters.get(pkgInfo.id).foreach(s => task.bimap( + _ => s.setAllowSubmission(false), //don't submit since no viper program could be produced + { case (job, _) => s.setProgram(FastPrettyPrinter.pretty(job.program)) })) + task.foldM({ case Vector() => Future(VerifierResult.Success) case errors => Future(VerifierResult.Failure(errors)) diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index 2d503c0f9..da126ff37 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -75,6 +75,7 @@ object ConfigDefaults { lazy val DefaultRequireTriggers: Boolean = false lazy val DefaultDisableSetAxiomatization: Boolean = false lazy val DefaultDisableCheckTerminationPureFns: Boolean = false + lazy val DefaultSubmitForEvaluation: Boolean = false } // More-complete exhale modes @@ -143,6 +144,7 @@ case class Config( requireTriggers: Boolean = ConfigDefaults.DefaultRequireTriggers, disableSetAxiomatization: Boolean = ConfigDefaults.DefaultDisableSetAxiomatization, disableCheckTerminationPureFns: Boolean = ConfigDefaults.DefaultDisableCheckTerminationPureFns, + submitForEvaluation: Boolean = ConfigDefaults.DefaultSubmitForEvaluation, ) { def merge(other: Config): Config = { @@ -195,6 +197,7 @@ case class Config( requireTriggers = requireTriggers || other.requireTriggers, disableSetAxiomatization = disableSetAxiomatization || other.disableSetAxiomatization, disableCheckTerminationPureFns = disableCheckTerminationPureFns || other.disableCheckTerminationPureFns, + submitForEvaluation = submitForEvaluation || other.submitForEvaluation, ) } @@ -251,6 +254,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector requireTriggers: Boolean = ConfigDefaults.DefaultRequireTriggers, disableSetAxiomatization: Boolean = ConfigDefaults.DefaultDisableSetAxiomatization, disableCheckTerminationPureFns: Boolean = ConfigDefaults.DefaultDisableCheckTerminationPureFns, + submitForEvaluation: Boolean = ConfigDefaults.DefaultSubmitForEvaluation, ) { def shouldParse: Boolean = true def shouldTypeCheck: Boolean = !shouldParseOnly @@ -266,6 +270,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector case _ => Some(positions.toVector) } } + def allowSubmission: Boolean = submitForEvaluation && !shouldChop } trait RawConfig { @@ -311,6 +316,7 @@ trait RawConfig { requireTriggers = baseConfig.requireTriggers, disableSetAxiomatization = baseConfig.disableSetAxiomatization, disableCheckTerminationPureFns = baseConfig.disableCheckTerminationPureFns, + submitForEvaluation = baseConfig.allowSubmission, ) } @@ -741,6 +747,14 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals default = Some(ConfigDefaults.DefaultDisableSetAxiomatization), noshort = true, ) + + val submitForEvaluation = opt[Boolean](name = "submitForEvaluation", + descr = "Whether to allow storing the current program for future evaluation.", + default = Some(false), + noshort = true + ) + + /** * Exception handling */ @@ -922,5 +936,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals requireTriggers = requireTriggers(), disableSetAxiomatization = disableSetAxiomatization(), disableCheckTerminationPureFns = disableCheckTerminationPureFns(), + submitForEvaluation = submitForEvaluation(), ) }