Generate cleaner output (#927)

* drop unnecessary info output

* clean-up even more

* simplify error, info, and debug messages

* drop unnecessary package ids from error messages when verifying a single package

* improve error messages further

* address Linard's feedback

* address Linard's feedback

Author: jcp19

src/main/scala/viper/gobra/Gobra.scala

@@ -61,22 +61,27 @@ trait GoVerifier extends StrictLogging {
    * Additionally statistics are collected with the StatsCollector reporter class
    */
   def verifyAllPackages(config: Config)(executor: GobraExecutionContext): VerifierResult = {
+    def addPlural(n: Int): String = if (n != 1) "s" else ""
     val statsCollector = StatsCollector(config.reporter)
     var warningCount: Int = 0
     var allVerifierErrors: Vector[VerifierError] = Vector()
     var allTimeoutErrors: Vector[TimeoutError] = Vector()
+    val isVerifyingMultiplePackages = config.packageInfoInputMap.size != 1
 
     // write report to file on shutdown, this makes sure a report is produced even if a run is shutdown
     // by some signal.
     Runtime.getRuntime.addShutdownHook(new Thread() {
       override def run(): Unit = {
-        val statsFile = config.gobraDirectory.resolve("stats.json").toFile
-        logger.info("Writing report to " + statsFile.getPath)
-        val wroteFile = statsCollector.writeJsonReportToFile(statsFile)
-        if (!wroteFile) {
-          logger.error(s"Could not write to the file $statsFile. Check whether the permissions to the file allow writing to it.")
+        config.gobraDirectory match {
+          case Some(path) =>
+            val statsFile = path.resolve("stats.json").toFile
+            logger.info("Writing report to " + statsFile.getPath)
+            val wroteFile = statsCollector.writeJsonReportToFile(statsFile)
+            if (!wroteFile) {
+              logger.error(s"Could not write to the file $statsFile. Check whether the permissions to the file allow writing to it.")
+            }
+          case _ =>
         }
-
         // Report timeouts that were not previously reported
         statsCollector.getTimeoutErrorsForNonFinishedTasks.foreach(err => logger.error(err.formattedMessage))
       }
@@ -95,10 +100,12 @@ trait GoVerifier extends StrictLogging {
           warningCount += warnings.size
           warnings.foreach(w => logger.debug(w))
 
+          val suffix = if (isVerifyingMultiplePackages) s" in package $pkgId" else ""
           result match {
-            case VerifierResult.Success => logger.info(s"$name found no errors")
+            case VerifierResult.Success =>
+              logger.info(s"$name found 0 errors$suffix.")
             case VerifierResult.Failure(errors) =>
-              logger.error(s"$name has found ${errors.length} error(s) in package $pkgId")
+              logger.error(s"$name found ${errors.length} error${addPlural(errors.length)}$suffix.")
               if (config.noStreamErrors) {
                 errors.foreach(err => logger.error(s"\t${err.formattedMessage}"))
               }
@@ -109,7 +116,7 @@ trait GoVerifier extends StrictLogging {
         Await.result(future, config.packageTimeout)
       } catch {
         case _: TimeoutException =>
-          logger.error(s"The verification of package $pkgId got terminated after " + config.packageTimeout.toString)
+          logger.error(s"The verification of package $pkgId timed out after ${config.packageTimeout}.")
           statsCollector.report(VerificationTaskFinishedMessage(pkgId))
           val errors = statsCollector.getTimeoutErrors(pkgId)
           errors.foreach(err => logger.error(err.formattedMessage))
@@ -119,24 +126,33 @@ trait GoVerifier extends StrictLogging {
 
     // Print statistics for caching
     if(config.cacheFile.isDefined) {
-      logger.debug(s"Number of cacheable Viper member(s): ${statsCollector.getNumberOfCacheableViperMembers}")
-      logger.debug(s"Number of cached Viper member(s): ${statsCollector.getNumberOfCachedViperMembers}")
+      logger.debug(s"Number of cacheable Viper members: ${statsCollector.getNumberOfCacheableViperMembers}")
+      logger.debug(s"Number of cached Viper members: ${statsCollector.getNumberOfCachedViperMembers}")
     }
 
     // Print general statistics
-    logger.debug(s"Gobra has found ${statsCollector.getNumberOfVerifiableMembers} methods and functions" )
-    logger.debug(s"${statsCollector.getNumberOfSpecifiedMembers} have specification")
-    logger.debug(s"${statsCollector.getNumberOfSpecifiedMembersWithAssumptions} are assumed to be satisfied")
+    logger.debug(s"Gobra found ${statsCollector.getNumberOfVerifiableMembers} methods and functions." )
+    logger.debug{
+      val specMem = statsCollector.getNumberOfSpecifiedMembers
+      s"$specMem member${addPlural(specMem)} are explicitly specified."
+    }
+    logger.debug{
+      val memAssum = statsCollector.getNumberOfSpecifiedMembersWithAssumptions
+      val isOrAre = if (memAssum != 1) "are" else "is"
+      s"$memAssum specified member${addPlural(memAssum)} of the package under verification $isOrAre trusted or abstract."
+    }
 
     // Print warnings
     if(warningCount > 0) {
-      logger.info(s"$name has found $warningCount warning(s)")
+      logger.debug(s"$name reported $warningCount warning${addPlural(warningCount)}.")
     }
 
     // Print errors
-    logger.info(s"$name has found ${allVerifierErrors.size} error(s)")
+    if (isVerifyingMultiplePackages) {
+      logger.info(s"$name found ${allVerifierErrors.size} error${addPlural(allVerifierErrors.size)} across all verified packages.")
+    }
     if(allTimeoutErrors.nonEmpty) {
-      logger.info(s"The verification of ${allTimeoutErrors.size} members timed out")
+      logger.info(s"The verification of ${allTimeoutErrors.size} member${addPlural(allTimeoutErrors.size)} timed out.")
     }
 
     val allErrors = allVerifierErrors ++ allTimeoutErrors
@@ -362,7 +378,7 @@ object GobraRunner extends GobraFrontend with StrictLogging {
       }
     } catch {
       case e: UglyErrorMessage =>
-        logger.error(s"${verifier.name} has found 1 error(s): ")
+        logger.error(s"${verifier.name} has found 1 error: ")
         logger.error(s"\t${e.error.formattedMessage}")
         exitCode = 1
       case e: LogicException =>

src/main/scala/viper/gobra/frontend/Config.scala

@@ -60,7 +60,8 @@ object ConfigDefaults {
   // or when the goal is to gradually verify part of a package without having to provide an explicit list of the files
   // to verify.
   val DefaultOnlyFilesWithHeader: Boolean = false
-  lazy val DefaultGobraDirectory: Path = Path.of(".gobra")
+  // In the past, the default Gobra directory used to be Path.of(".gobra")
+  lazy val DefaultGobraDirectory: Option[Path] = None
   val DefaultTaskName: String = "gobra-task"
   val DefaultAssumeInjectivityOnInhale: Boolean = true
   val DefaultParallelizeBranches: Boolean = false
@@ -117,7 +118,7 @@ object MoreJoins {
 }
 
 case class Config(
-                   gobraDirectory: Path = ConfigDefaults.DefaultGobraDirectory,
+                   gobraDirectory: Option[Path] = ConfigDefaults.DefaultGobraDirectory,
                    // Used as an identifier of a verification task, ideally it shouldn't change between verifications
                    // because it is used as a caching key. Additionally it should be unique when using the StatsCollector
                    taskName: String = ConfigDefaults.DefaultTaskName,
@@ -261,7 +262,7 @@ object Config {
 }
 
 // have a look at `Config` to see an inline description of some of these parameters
-case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirectory,
+case class BaseConfig(gobraDirectory: Option[Path] = ConfigDefaults.DefaultGobraDirectory,
                       moduleName: String = ConfigDefaults.DefaultModuleName,
                       includeDirs: Vector[Path] = ConfigDefaults.DefaultIncludeDirs.map(_.toPath).toVector,
                       reporter: GobraReporter = ConfigDefaults.DefaultReporter,
@@ -561,7 +562,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
   val gobraDirectory: ScallopOption[Path] = opt[Path](
     name = "gobraDirectory",
     descr = "Output directory for Gobra",
-    default = Some(ConfigDefaults.DefaultGobraDirectory),
+    default = ConfigDefaults.DefaultGobraDirectory,
     short = 'g'
   )(singleArgConverter(arg => Path.of(arg)))
 
@@ -1038,7 +1039,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
   )
 
   private def baseConfig(isolate: List[(Path, List[Int])]): BaseConfig = BaseConfig(
-    gobraDirectory = gobraDirectory(),
+    gobraDirectory = gobraDirectory.toOption,
     moduleName = module(),
     includeDirs = includeDirs,
     reporter = FileWriterReporter(

src/main/scala/viper/gobra/translator/encodings/closures/ClosureDomainEncoder.scala

@@ -20,12 +20,10 @@ class ClosureDomainEncoder(specs: ClosureSpecsEncoder) {
 
   private var domainNeeded: Boolean = false
   lazy val vprType: vpr.DomainType = {
-    println("Use of closures detected: Closures are an experimental feature and may exhibit bugs.")
     domainNeeded = true
     vpr.DomainType(Names.closureDomain, Map.empty)(Vector.empty)
   }
 
-
   /** Encoding of the Closure domain. This is used to represent variables with function types. It looks as follows:
     *
     * domain Closure {