Viper data collection changes #751
Conversation
| @@ -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.", | |||
There was a problem hiding this comment.
| 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")
There was a problem hiding this comment.
Adding a sentence saying that we collect only the program and no other information would also be important.
| case CarbonBackend => "Carbon" | ||
| case SiliconBackend => "Silicon" |
There was a problem hiding this comment.
This is not exhaustive. What if we have a viper server with silicon or carbon?
There was a problem hiding this comment.
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.
| @@ -51,6 +56,8 @@ object GoVerifier { | |||
|
|
|||
| trait GoVerifier extends StrictLogging { | |||
|
|
|||
| protected var submitters: Map[String, ManualProgramSubmitter] = Map() | |||
There was a problem hiding this comment.
can you add some documentation on this? what is the purpose of this field? what are the keys and the values?
| @@ -275,6 +279,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector | |||
| case _ => Some(positions.toVector) | |||
| } | |||
| } | |||
| def allowSubmission: Boolean = submitForEvaluation && !shouldChop | |||
There was a problem hiding this comment.
why can't we submit chopped programs?
| 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 |
There was a problem hiding this comment.
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
| @@ -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 = { | |||
There was a problem hiding this comment.
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.
| s.setSuccess(result == VerifierResult.Success) | ||
| s.submit()} | ||
| ) | ||
| submitters = submitters.removed(pkgId) |
There was a problem hiding this comment.
Why are we removing this here?
| @@ -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 = { | |||
There was a problem hiding this comment.
maybe a better name would be registerSubmitter
| @@ -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 = { | |||
| if (allowSubmission) { | |||
| val submitter = new ManualProgramSubmitter(true, "", "Gobra", verifier, Array()) | |||
There was a problem hiding this comment.
are we actually submitting anything if the second parameter is always ""?
There was a problem hiding this comment.
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.
|
@Dspil is this still relevant, or shall I close it? |
|
It is, just not very high in my todo list. |
This PR contains changes to facilitate submissions to the Viper data collection server.
submitForEvaluationflag to the configGoVerifier