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.

Sign up for GitHub

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

Jump to bottom

Viper data collection changes #751

Draft
wants to merge 4 commits into
base: master
Choose a base branch
from
Draft

Viper data collection changes #751

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
efdbce0
added submitter to GoVerifier, flag to config
Simon-Hostettler Dec 23, 2023
ba8eb24
updated submitter code
Simon-Hostettler Mar 2, 2024
edac923
viper data collection changes
Simon-Hostettler Mar 24, 2024
73bc773
viper data collection changes
Simon-Hostettler Mar 24, 2024
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
33 changes: 33 additions & 0 deletions src/main/scala/viper/gobra/Gobra.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand All @@ -26,7 +27,11 @@ 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 viper.silver.ast.pretty.FastPrettyPrinter
import viper.silver.utility.ManualProgramSubmitter

import java.time.format.DateTimeFormatter
import java.time.LocalTime
Expand All @@ -51,6 +56,8 @@ object GoVerifier {

trait GoVerifier extends StrictLogging {

protected var submitters: Map[String, ManualProgramSubmitter] = Map()
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

can you add some documentation on this? what is the purpose of this field? what are the keys and the values?


def name: String = {
this.getClass.getSimpleName
}
Expand Down Expand Up @@ -82,9 +89,18 @@ trait GoVerifier extends StrictLogging {
}
})

val viperBackendName: String = config.backend match {
case CarbonBackend => "Carbon"
case SiliconBackend => "Silicon"
Comment on lines +93 to +94
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is not exhaustive. What if we have a viper server with silicon or carbon?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe, we should extend the trait ViperBackend with an extra method or field of type string named name and use it instead, instead of matching on all available ones.

}

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
Copy link
Contributor

@jcp19 jcp19 Mar 30, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this looks like the wrong place for this comment. Sth like this should be in createSubmitter and and the description of what we store in keys/values should be on the declaration of submitters

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 => {
Expand All @@ -95,6 +111,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)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why are we removing this here?


result match {
case VerifierResult.Success => logger.info(s"$name found no errors")
case VerifierResult.Failure(errors) =>
Expand Down Expand Up @@ -143,6 +165,13 @@ trait GoVerifier extends StrictLogging {
if (allErrors.isEmpty) VerifierResult.Success else VerifierResult.Failure(allErrors)
}

private def createSubmitter(allowSubmission: Boolean, id: String, verifier: String): Unit = {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we should make the signature of createSubmitter by having verifier of type ViperBackend. We could obtain a the name using the name field that I suggested.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

maybe a better name would be registerSubmitter

if (allowSubmission) {
val submitter = new ManualProgramSubmitter(true, "", "Gobra", verifier, Array())
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

are we actually submitting anything if the second parameter is always ""?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Btw, I find it a bit odd that we have a flag ProgramSubmitter has a field allowSubmission. Maybe I misunderstand its purpose, but if this object was registered, it should be submitted. Otherwise, we should not register it. I don't see the need for this field.

submitters = submitters + (id -> submitter)
}
}

protected[this] def verify(pkgInfo: PackageInfo, config: Config)(implicit executor: GobraExecutionContext): Future[VerifierResult]
}

Expand All @@ -163,6 +192,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))
Expand Down
14 changes: 14 additions & 0 deletions src/main/scala/viper/gobra/frontend/Config.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,7 @@ object ConfigDefaults {
val DefaultDisableCheckTerminationPureFns: Boolean = false
val DefaultUnsafeWildcardOptimization: Boolean = false
val DefaultEnableMoreJoins: Boolean = false
val DefaultSubmitForEvaluation = false
}

// More-complete exhale modes
Expand Down Expand Up @@ -145,6 +146,7 @@ case class Config(
requireTriggers: Boolean = ConfigDefaults.DefaultRequireTriggers,
disableSetAxiomatization: Boolean = ConfigDefaults.DefaultDisableSetAxiomatization,
disableCheckTerminationPureFns: Boolean = ConfigDefaults.DefaultDisableCheckTerminationPureFns,
submitForEvaluation: Boolean = ConfigDefaults.DefaultSubmitForEvaluation,
unsafeWildcardOptimization: Boolean = ConfigDefaults.DefaultUnsafeWildcardOptimization,
enableMoreJoins: Boolean = ConfigDefaults.DefaultEnableMoreJoins,

Expand Down Expand Up @@ -200,6 +202,7 @@ case class Config(
requireTriggers = requireTriggers || other.requireTriggers,
disableSetAxiomatization = disableSetAxiomatization || other.disableSetAxiomatization,
disableCheckTerminationPureFns = disableCheckTerminationPureFns || other.disableCheckTerminationPureFns,
submitForEvaluation = submitForEvaluation || other.submitForEvaluation,
unsafeWildcardOptimization = unsafeWildcardOptimization && other.unsafeWildcardOptimization,
enableMoreJoins = enableMoreJoins || other.enableMoreJoins,
)
Expand Down Expand Up @@ -258,6 +261,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
requireTriggers: Boolean = ConfigDefaults.DefaultRequireTriggers,
disableSetAxiomatization: Boolean = ConfigDefaults.DefaultDisableSetAxiomatization,
disableCheckTerminationPureFns: Boolean = ConfigDefaults.DefaultDisableCheckTerminationPureFns,
submitForEvaluation: Boolean = ConfigDefaults.DefaultSubmitForEvaluation,
unsafeWildcardOptimization: Boolean = ConfigDefaults.DefaultUnsafeWildcardOptimization,
enableMoreJoins: Boolean = ConfigDefaults.DefaultEnableMoreJoins,
) {
Expand All @@ -275,6 +279,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
case _ => Some(positions.toVector)
}
}
def allowSubmission: Boolean = submitForEvaluation && !shouldChop
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why can't we submit chopped programs?

}

trait RawConfig {
Expand Down Expand Up @@ -320,6 +325,7 @@ trait RawConfig {
requireTriggers = baseConfig.requireTriggers,
disableSetAxiomatization = baseConfig.disableSetAxiomatization,
disableCheckTerminationPureFns = baseConfig.disableCheckTerminationPureFns,
submitForEvaluation = baseConfig.allowSubmission,
unsafeWildcardOptimization = baseConfig.unsafeWildcardOptimization,
enableMoreJoins = baseConfig.enableMoreJoins,
)
Expand Down Expand Up @@ -765,6 +771,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.",
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
descr = "Whether to allow storing the current program for future evaluation.",
descr = "Upload the verified program to Gobra's servers. This information will be used to improve Gobra.",

(I think there is already a variable for the tool name, we can use that directly instead of hardcoding "Gobra")

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Adding a sentence saying that we collect only the program and no other information would also be important.

default = Some(false),
noshort = true
)

/**
* Exception handling
*/
Expand Down Expand Up @@ -964,6 +977,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
requireTriggers = requireTriggers(),
disableSetAxiomatization = disableSetAxiomatization(),
disableCheckTerminationPureFns = disableCheckTerminationPureFns(),
submitForEvaluation = submitForEvaluation(),
unsafeWildcardOptimization = unsafeWildcardOptimization(),
enableMoreJoins = enableMoreJoins(),
)
Expand Down
Loading