fixes unit tests

koflin · Mar 9, 2023 · 5a4f353 · 5a4f353
1 parent 81ea403
commit 5a4f353
Show file tree

Hide file tree

Showing 13 changed files with 164 additions and 973 deletions.
diff --git a/src/main/scala/viper/gobra/Gobra.scala b/src/main/scala/viper/gobra/Gobra.scala
@@ -247,25 +247,11 @@ class Gobra extends GoVerifier with GoIdeVerifier {
     if (config.shouldParse) {
       val startMs = System.currentTimeMillis()
       val res = Parser.parse(config, pkgInfo)(executor)
-      val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
-      println(s"parser phase done, took ${durationS}s")
-      res
-      /*
-      val sourcesToParse = config.packageInfoInputMap(pkgInfo)
-      val res = Parser.parse(sourcesToParse, pkgInfo)(config)
-       */
-      /*
-      val parseManager = Parser.parse(pkgInfo)(config, executionContext)
-      config.typeCheckMode match {
-        case TypeCheckMode.Lazy => // don't do anything
-        case TypeCheckMode.Sequential | TypeCheckMode.Parallel =>
-          parseManager.awaitResults()
-          val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
-          println(s"parser phase done, took ${durationS}s")
-          println(s"parsed packages: ${parseManager.getResults.map{ case (pkg, _) => pkg }.mkString(", ")}")
+      logger.debug {
+        val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
+        s"parser phase done, took ${durationS}s"
       }
-      Right(parseManager)
-      */
+      res
     } else {
       Left(Vector())
     }
@@ -279,12 +265,14 @@ class Gobra extends GoVerifier with GoIdeVerifier {
     }
   }
 
-  private def performDesugaring(config: Config, typeInfo: TypeInfo)(@unused executor: GobraExecutionContext): Either[Vector[VerifierError], Program] = {
+  private def performDesugaring(config: Config, typeInfo: TypeInfo)(executor: GobraExecutionContext): Either[Vector[VerifierError], Program] = {
     if (config.shouldDesugar) {
       val startMs = System.currentTimeMillis()
-      val res = Right(Desugar.desugar(typeInfo.tree.root, typeInfo)(config))
-      val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
-      println(s"desugaring done, took ${durationS}s")
+      val res = Right(Desugar.desugar(config, typeInfo)(executor))
+      logger.debug {
+        val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
+        s"desugaring done, took ${durationS}s"
+      }
       res
     } else {
       Left(Vector())
@@ -305,18 +293,22 @@ class Gobra extends GoVerifier with GoIdeVerifier {
       transformations :+= OverflowChecksTransform
     }
     val result = transformations.foldLeft(program)((prog, transf) => transf.transform(prog))
+    logger.debug {
+      val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
+      s"internal transformations done, took ${durationS}s"
+    }
     config.reporter.report(AppliedInternalTransformsMessage(config.packageInfoInputMap(pkgInfo).map(_.name), () => result))
-    val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
-    println(s"internal transformations done, took ${durationS}s")
     Right(result)
   }
 
   private def performViperEncoding(config: Config, pkgInfo: PackageInfo, program: Program)(@unused executor: GobraExecutionContext): Either[Vector[VerifierError], BackendVerifier.Task] = {
     if (config.shouldViperEncode) {
       val startMs = System.currentTimeMillis()
       val res = Right(Translator.translate(program, pkgInfo)(config))
-      val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
-      println(s"Viper encoding done, took ${durationS}s")
+      logger.debug {
+        val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
+        s"Viper encoding done, took ${durationS}s"
+      }
       res
     } else {
       Left(Vector())

diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala
@@ -6,6 +6,7 @@
 
 package viper.gobra.frontend
 
+import com.typesafe.scalalogging.LazyLogging
 import viper.gobra.ast.frontend.{PExpression, AstPattern => ap, _}
 import viper.gobra.ast.{internal => in}
 import viper.gobra.frontend.PackageResolver.RegularImport
@@ -20,41 +21,60 @@ import viper.gobra.reporting.{DesugaredMessage, Source}
 import viper.gobra.theory.Addressability
 import viper.gobra.translator.Names
 import viper.gobra.util.Violation.violation
-import viper.gobra.util.{Constants, DesugarWriter, Violation}
+import viper.gobra.util.{Constants, DesugarWriter, GobraExecutionContext, Violation}
 
+import java.util.concurrent.atomic.AtomicLong
 import scala.annotation.{tailrec, unused}
 import scala.collection.{Iterable, SortedSet}
+import scala.concurrent.duration.Duration
+import scala.concurrent.{Await, Future}
 import scala.reflect.ClassTag
 
-object Desugar {
+object Desugar extends LazyLogging {
 
-  def desugar(pkg: PPackage, info: viper.gobra.frontend.info.TypeInfo)(config: Config): in.Program = {
+  def desugar(config: Config, info: viper.gobra.frontend.info.TypeInfo)(implicit executionContext: GobraExecutionContext): in.Program = {
+    val pkg = info.tree.root
     val importsCollector = new PackageInitSpecCollector
-    // independently desugar each imported package.
-    val importedDesugaringStartMs = System.currentTimeMillis()
-    // val importedPrograms = info.context.getContexts map { tI => {
-    // val importedPrograms = info.dependentTypeInfo.map { case (abstractPackage, tIFn) => {
-    val importedPrograms = info.getTransitiveTypeInfos.map { tI => {
+
+    val importeDesugaringDurationMs = new AtomicLong(0)
+    val importedProgramsFuts = info.getTransitiveTypeInfos(includeThis = false).toSeq.map { tI => Future {
+      val importedDesugaringStartMs = System.currentTimeMillis()
       val typeInfo = tI.getTypeInfo
-      // val typeInfo: TypeInfo = tIFn().map(_.getTypeInfo).getOrElse(Violation.violation(s"cannot desugar package $abstractPackage for which type-checking failed")) // tI.getTypeInfo
       val importedPackage = typeInfo.tree.originalRoot
       val d = new Desugarer(importedPackage.positions, typeInfo)
       // registers a package to generate proof obligations for its init code
       d.registerPackage(importedPackage, importsCollector)(config)
-      (d, d.packageD(importedPackage))
+      val res = (d, d.packageD(importedPackage))
+      importeDesugaringDurationMs.addAndGet(System.currentTimeMillis() - importedDesugaringStartMs)
+      res
     }}
-    val importedDurationS = f"${(System.currentTimeMillis() - importedDesugaringStartMs) / 1000f}%.1f"
-    println(s"desugaring imported packages done, took ${importedDurationS}s")
-
-    val desugaringStartMs = System.currentTimeMillis()
-    // desugar the main package, i.e. the package on which verification is performed:
-    val mainDesugarer = new Desugarer(pkg.positions, info)
-    // registers main package to generate proof obligations for its init code
-    mainDesugarer.registerMainPackage(pkg, importsCollector)(config)
+
+    val mainPackageFut = Future {
+      val mainDesugaringStartMs = System.currentTimeMillis()
+      // desugar the main package, i.e. the package on which verification is performed:
+      val mainDesugarer = new Desugarer(pkg.positions, info)
+      // registers main package to generate proof obligations for its init code
+      mainDesugarer.registerMainPackage(pkg, importsCollector)(config)
+      val res = (mainDesugarer, mainDesugarer.packageD(pkg))
+      logger.debug {
+        val durationS = f"${(System.currentTimeMillis() - mainDesugaringStartMs) / 1000f}%.1f"
+        s"desugaring package ${info.pkgInfo.id} done, took ${durationS}s"
+      }
+      res
+    }
+
+    // we place `mainPackageFut` at index 0
+    val allPackagesFut = Future.sequence(mainPackageFut +: importedProgramsFuts)
+    val futResults = Await.result(allPackagesFut, Duration.Inf)
+    val (mainDesugarer, mainProgram) = futResults.head
+    val importedPrograms = futResults.tail
+    logger.debug {
+      val importedDurationS = f"${importeDesugaringDurationMs.get() / 1000f}%.1f"
+      s"desugaring imported packages done, took ${importedDurationS}s"
+    }
+
     // combine all desugared results into one Viper program:
-    val internalProgram = combine(mainDesugarer, mainDesugarer.packageD(pkg), importedPrograms)
-    val durationS = f"${(System.currentTimeMillis() - desugaringStartMs) / 1000f}%.1f"
-    println(s"desugaring main package done, took ${durationS}s")
+    val internalProgram = combine(mainDesugarer, mainProgram, importedPrograms)
     config.reporter report DesugaredMessage(config.packageInfoInputMap(pkg.info).map(_.name), () => internalProgram)
     internalProgram
   }
@@ -3466,9 +3486,7 @@ object Desugar {
       pkg.imports.foreach{ imp => {
         val importedPackage = RegularImport(imp.importPath)
         Violation.violation(info.dependentTypeInfo.contains(importedPackage), s"Desugarer expects to have acess to the type information of all imported packages but could not find $importedPackage")
-        // info.context.getTypeInfo(RegularImport(imp.importPath))(config) match {
         info.dependentTypeInfo(importedPackage)() match {
-          // case Some(Right(tI)) =>
           case Right(tI) =>
             val desugaredPre = imp.importPres.map(specificationD(FunctionContext.empty(), info))
             Violation.violation(!config.enableLazyImports || desugaredPre.isEmpty, s"Import precondition found despite running with ${Config.enableLazyImportOptionPrettyPrinted}")

diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala
@@ -6,6 +6,7 @@
 
 package viper.gobra.frontend
 
+import com.typesafe.scalalogging.LazyLogging
 import org.bitbucket.inkytonik.kiama.rewriting.Cloner.{rewrite, topdown}
 import org.bitbucket.inkytonik.kiama.rewriting.PositionedRewriter.strategyWithName
 import org.bitbucket.inkytonik.kiama.rewriting.{Cloner, PositionedRewriter, Strategy}
@@ -30,7 +31,7 @@ object Parser {
 
   type ParseSuccessResult = (Vector[Source], PPackage)
   type ParseResult = Either[Vector[VerifierError], ParseSuccessResult]
-  class ParseManager(config: Config, executionContext: GobraExecutionContext) {
+  class ParseManager(config: Config, executionContext: GobraExecutionContext) extends LazyLogging {
     private val manager = new TaskManager[AbstractPackage, ParseResult](TaskManagerMode.Parallel)
 
     def parse(pkgInfo: PackageInfo): Unit = {
@@ -44,76 +45,74 @@ object Parser {
     trait ParseJob extends Job[ParseResult] {
       def pkgInfo: PackageInfo
       def pkgSources: Vector[Source]
+      def specOnly: Boolean
 
       override def compute(): ParseResult = {
         require(pkgSources.nonEmpty)
 
+        val preprocessedSources = preprocess(pkgSources)(config)
+
         val startPreambleParsingMs = System.currentTimeMillis()
-        var endPreambleParsingMs: Option[Long] = None
         // before parsing, get imports and add these parse jobs
-        fastParse(pkgSources)
-          .map(directImportTarget => {
-            if (endPreambleParsingMs.isEmpty) {
-              endPreambleParsingMs = Some(System.currentTimeMillis())
-            }
+        val imports = fastParse(preprocessedSources)
+        val preambleParsingDurationMs = System.currentTimeMillis() - startPreambleParsingMs
+        imports.foreach(directImportTarget => {
             val directImportPackage = AbstractPackage(directImportTarget)(config)
-            val pkgSources = PackageResolver.resolveSources(directImportTarget)(config)
+            val importedSources = PackageResolver.resolveSources(directImportTarget)(config)
               .getOrElse(Vector())
               .map(_.source)
-            if (pkgSources.isEmpty) {
+            if (importedSources.isEmpty) {
               manager.addIfAbsent(directImportPackage, ParseFailureJob(Vector(NotFoundError(s"No source files for package '$directImportTarget found"))))(executionContext)
             } else {
-              manager.addIfAbsent(directImportPackage, ParseSourcesJob(pkgSources, directImportPackage))(executionContext)
+              manager.addIfAbsent(directImportPackage, ParseSourcesJob(importedSources, directImportPackage))(executionContext)
             }
           })
 
         val startMs = System.currentTimeMillis()
         val res = for {
-          parsedProgram <- Parser.parse(pkgSources, pkgInfo, specOnly = true)(config)
+          parsedProgram <- Parser.process(preprocessedSources, pkgInfo, specOnly = specOnly)(config)
         } yield (pkgSources, parsedProgram)
-        val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
-        val preambleParsingRatio = f"${100f * (endPreambleParsingMs.get - startPreambleParsingMs) / (System.currentTimeMillis() - startMs)}%.1f"
-        println(s"parsing ${pkgInfo.id} done (took ${durationS}s; parsing preamble takes ${preambleParsingRatio}%)")
+
+        logger.trace {
+          val parsingDurationMs = System.currentTimeMillis() - startMs
+          val parsingDurationS = f"${parsingDurationMs / 1000f}%.1f"
+          val preambleParsingRatio = f"${100f * preambleParsingDurationMs / parsingDurationMs}%.1f"
+          s"parsing ${pkgInfo.id} done (took ${parsingDurationS}s; parsing preamble overhead is ${preambleParsingRatio}%)"
+        }
+
         res
       }
 
-      private def fastParse(sources: Vector[Source]): Set[AbstractImport] = {
-        def getImportPaths(source: Source): Set[AbstractImport] = {
-          parsePreamble(source)(config)
+      private def fastParse(preprocessedInput: Vector[Source]): Set[AbstractImport] = {
+        def getImportPaths(preprocessedSource: Source): Set[AbstractImport] = {
+          processPreamble(preprocessedSource)(config)
             .map(_.imports.toSet.map[AbstractImport](importNode => RegularImport(importNode.importPath)))
             // we do not handle parser errors here but defer this to the time point when we actually
             // parse this source
             .getOrElse(Set.empty)
         }
 
-        sources.flatMap(getImportPaths).toSet + BuiltInImport
+        preprocessedInput.flatMap(getImportPaths).toSet + BuiltInImport
       }
     }
 
+    /** this job is used to parse the package that should be verified */
     case class ParseInfoJob(override val pkgInfo: PackageInfo) extends ParseJob {
       lazy val pkgSources: Vector[Source] = config.packageInfoInputMap(pkgInfo)
+      lazy val specOnly: Boolean = false
     }
 
+    /** this job is used to parse all packages that are imported */
     case class ParseSourcesJob(override val pkgSources: Vector[Source], pkg: AbstractPackage) extends ParseJob {
       require(pkgSources.nonEmpty)
       lazy val pkgInfo: PackageInfo = Source.getPackageInfo(pkgSources.head, config.projectRoot)
+      lazy val specOnly: Boolean = true
     }
 
     case class ParseFailureJob(errs: Vector[NotFoundError]) extends Job[ParseResult] {
       override def compute(): ParseResult = Left(errs)
     }
-    /*
-    def awaitResults(): Iterable[ParseResult] = manager.getAllResults(executionContext)
 
-    def getResult(pkgInfo: PackageInfo): ParseResult =
-      getResult(RegularPackage(pkgInfo.id))
-
-    def getResult(abstractPackage: AbstractPackage): ParseResult =
-      manager.getResult(abstractPackage)
-
-    def getResults: Iterable[(AbstractPackage, ParseResult)] =
-      manager.getAllResultsWithKeys
-    */
     def getParseResults(executionContext: GobraExecutionContext): Either[Map[AbstractPackage, Vector[VerifierError]], Map[AbstractPackage, ParseSuccessResult]] = {
       val (failedResults, successfulResults) = manager.getAllResultsWithKeys(executionContext)
         .partitionMap { case (key, eitherResult) => eitherResult.fold[Either[(AbstractPackage, Vector[VerifierError]), (AbstractPackage, ParseSuccessResult)]](errs => Left((key, errs)), result => Right((key, result))) }
@@ -146,13 +145,45 @@ object Parser {
   }
 
   def parse(input: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean = false)(config: Config): Either[Vector[VerifierError], PPackage] = {
+    val preprocessedInputs = preprocess(input)(config)
+    process(preprocessedInputs, pkgInfo, specOnly = specOnly)(config)
+  }
+
+  private def preprocess(input: Vector[Source])(config: Config): Vector[Source] = {
     val sources = input.map(Gobrafier.gobrafy)
     sources.foreach { s => config.reporter report PreprocessedInputMessage(s.name, () => s.content) }
+    sources
+  }
+
+  /**
+    * Parses a source's preamble containing all (file-level) imports; This function expects that the input has already
+    * been preprocessed
+    */
+  private def processPreamble(preprocessedSource: Source)(config: Config): Either[Vector[ParserError], PPreamble] = {
+    val positions = new Positions
+    val pom = new PositionManager(positions)
+
+    def parseSource(preprocessedSource: Source): Either[Vector[ParserError], PPreamble] = {
+      val parser = new SyntaxAnalyzer[PreambleContext, PPreamble](preprocessedSource, ListBuffer.empty[ParserError], pom, specOnly = true)
+      parser.parse(parser.preamble)
+    }
+
+    def parseSourceCached(preprocessedSource: Source): Either[Vector[ParserError], PPreamble] = {
+      def parseAndStore(): Either[Vector[ParserError], PPreamble] =
+        parseSource(preprocessedSource)
+
+      preambleCache.computeIfAbsent(getCacheKey(preprocessedSource, specOnly = true), _ => parseAndStore())
+    }
+
+    if (config.cacheParser) parseSourceCached(preprocessedSource) else parseSource(preprocessedSource)
+  }
+
+  private def process(preprocessedInputs: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): Either[Vector[VerifierError], PPackage] = {
     for {
-      parseAst <- parseSources(sources, pkgInfo, specOnly)(config)
+      parseAst <- parseSources(preprocessedInputs, pkgInfo, specOnly = specOnly)(config)
       postprocessors = Seq(
         new ImportPostprocessor(parseAst.positions.positions),
-        new TerminationMeasurePostprocessor(parseAst.positions.positions, specOnly),
+        new TerminationMeasurePostprocessor(parseAst.positions.positions, specOnly = specOnly),
       )
       postprocessedAst <- postprocessors.foldLeft[Either[Vector[VerifierError], PPackage]](Right(parseAst)) {
         case (Right(ast), postprocessor) => postprocessor.postprocess(ast)(config)
@@ -286,27 +317,6 @@ object Parser {
     parser.parse(parser.sourceFile())
   }
 
-  /** parses a source's preamble containing all (file-level) imports */
-  def parsePreamble(source: Source)(config: Config): Either[Vector[ParserError], PPreamble] = {
-    // TODO: gobrafy only once
-    val positions = new Positions
-    val pom = new PositionManager(positions)
-
-    def parseSource(source: Source): Either[Vector[ParserError], PPreamble] = {
-      val parser = new SyntaxAnalyzer[PreambleContext, PPreamble](Gobrafier.gobrafy(source), ListBuffer.empty[ParserError], pom, specOnly = true)
-      parser.parse(parser.preamble)
-    }
-
-    def parseSourceCached(source: Source): Either[Vector[ParserError], PPreamble] = {
-      def parseAndStore(): Either[Vector[ParserError], PPreamble] =
-        parseSource(source)
-
-      preambleCache.computeIfAbsent(getCacheKey(source, specOnly = true), _ => parseAndStore())
-    }
-
-    if (config.cacheParser) parseSourceCached(source) else parseSource(source)
-  }
-
   def parseFunction(source: Source, specOnly: Boolean = false): Either[Vector[ParserError], PMember] = {
     val positions = new Positions
     val pom = new PositionManager(positions)

diff --git a/src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala b/src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala
@@ -23,8 +23,8 @@ trait ExternalTypeInfo {
   def pkgInfo: PackageInfo
   def dependentTypeInfo: Map[AbstractImport, () => Either[Vector[VerifierError], ExternalTypeInfo]]
 
-  /** returns this and the type information of directly and transitively dependent packages */
-  def getTransitiveTypeInfos: Set[ExternalTypeInfo]
+  /** returns this (unless disabled via parameter) and the type information of directly and transitively dependent packages */
+  def getTransitiveTypeInfos(includeThis: Boolean = true): Set[ExternalTypeInfo]
 
   /**
     * Gets called by the type checker to perform a symbol table lookup in an imported package