Skip to content

Commit

Permalink
addresses several unit test errors
Browse files Browse the repository at this point in the history
  • Loading branch information
ArquintL committed Jun 30, 2023
1 parent 8d24c01 commit 6f41997
Show file tree
Hide file tree
Showing 6 changed files with 30 additions and 22 deletions.
8 changes: 5 additions & 3 deletions src/main/scala/viper/gobra/Gobra.scala
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
for {
finalConfig <- getAndMergeInFileConfig(config, pkgInfo)
_ = setLogLevel(finalConfig)
parseResults = performParsing(finalConfig, pkgInfo)(executor)
parseResults <- performParsing(finalConfig, pkgInfo)(executor)
typeInfo <- performTypeChecking(finalConfig, pkgInfo, parseResults)(executor)
program <- performDesugaring(finalConfig, typeInfo)(executor)
program <- performInternalTransformations(finalConfig, pkgInfo, program)(executor)
Expand Down Expand Up @@ -243,7 +243,9 @@ class Gobra extends GoVerifier with GoIdeVerifier {
.setLevel(config.logLevel)
}

private def performParsing(config: Config, pkgInfo: PackageInfo)(executor: GobraExecutionContext): Map[AbstractPackage, ParseResult] = {
// returns `Left(...)` if parsing of the package identified by `pkgInfo` failed. Note that `Right(...)` does not imply
// that all imported packages have been parsed successfully (this is only checked during type-checking)
private def performParsing(config: Config, pkgInfo: PackageInfo)(executor: GobraExecutionContext): Either[Vector[VerifierError], Map[AbstractPackage, ParseResult]] = {
if (config.shouldParse) {
val startMs = System.currentTimeMillis()
val res = Parser.parse(config, pkgInfo)(executor)
Expand All @@ -253,7 +255,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
}
res
} else {
Map.empty
Left(Vector.empty)
}
}

Expand Down
11 changes: 8 additions & 3 deletions src/main/scala/viper/gobra/frontend/Parser.scala
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ import org.antlr.v4.runtime.atn.PredictionMode
import org.antlr.v4.runtime.misc.ParseCancellationException
import viper.gobra.frontend.GobraParser.{ExprOnlyContext, ImportDeclContext, PreambleContext, SourceFileContext, SpecMemberContext, StmtOnlyContext, TypeOnlyContext}
import viper.gobra.frontend.PackageResolver.{AbstractImport, AbstractPackage, BuiltInImport, RegularImport, RegularPackage}
import viper.gobra.util.GobraExecutionContext
import viper.gobra.util.{GobraExecutionContext, Violation}
import viper.silver.ast.SourcePosition

import scala.collection.mutable.ListBuffer
Expand Down Expand Up @@ -186,10 +186,15 @@ object Parser {
*
*/

def parse(config: Config, pkgInfo: PackageInfo)(executionContext: GobraExecutionContext): Map[AbstractPackage, ParseResult] = {
def parse(config: Config, pkgInfo: PackageInfo)(executionContext: GobraExecutionContext): Either[Vector[ParserError], Map[AbstractPackage, ParseResult]] = {
val parseManager = new ParseManager(config, executionContext)
parseManager.parse(pkgInfo)
parseManager.getResults
val results = parseManager.getResults
results.get(RegularPackage(pkgInfo.id)) match {
case Some(Right(_)) => Right(results)
case Some(Left(errs)) => Left(errs)
case _ => Violation.violation(s"No parse result for package '$pkgInfo' found")
}
}

def parse(input: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean = false)(config: Config): Either[Vector[VerifierError], PPackage] = {
Expand Down
11 changes: 6 additions & 5 deletions src/main/scala/viper/gobra/frontend/info/Info.scala
Original file line number Diff line number Diff line change
Expand Up @@ -228,18 +228,19 @@ object Info extends LazyLogging {
}

def check(config: Config, abstractPackage: AbstractPackage, parseResults: Map[AbstractPackage, ParseResult])(executionContext: GobraExecutionContext): TypeCheckResult = {
// check for cycles
// val cyclicErrors = new CycleChecker(config, parseResults).check(abstractPackage)
for {
successParseResult <- new CycleChecker(config, parseResults).check(abstractPackage)
// check whether parsing of this package was successful:
parseResult <- parseResults(abstractPackage)
// check whether there are any import cycles:
cycleResult <- new CycleChecker(config, parseResults).check(abstractPackage)
.left.map(errs => {
val (sources, pkg) = parseResults(abstractPackage).right.get
val (sources, pkg) = parseResult
val sourceNames = sources.map(_.name)
config.reporter report TypeCheckFailureMessage(sourceNames, pkg.packageClause.id.name, () => pkg, errs)
errs
})
typeCheckingStartMs = System.currentTimeMillis()
context = new Context(config, successParseResult)(executionContext)
context = new Context(config, cycleResult)(executionContext)
typeInfo <- context.typeCheck(abstractPackage)
_ = logger.debug {
val durationS = f"${(System.currentTimeMillis() - typeCheckingStartMs) / 1000f}%.1f"
Expand Down
18 changes: 9 additions & 9 deletions src/test/resources/regressions/features/import/import1.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -4,27 +4,27 @@
package main

import fmt "fmt"
//:: ExpectedOutput(parser_error)
//:: ExpectedOutput(type_error)
import a "a";
//:: ExpectedOutput(parser_error)
//:: ExpectedOutput(type_error)
import (b "b")
//:: ExpectedOutput(parser_error)
//:: ExpectedOutput(type_error)
import (c "c");
import (
//:: ExpectedOutput(parser_error)
//:: ExpectedOutput(type_error)
d "d"
//:: ExpectedOutput(parser_error)
//:: ExpectedOutput(type_error)
e "e")
import (
//:: ExpectedOutput(parser_error)
//:: ExpectedOutput(type_error)
f "f"
//:: ExpectedOutput(parser_error)
//:: ExpectedOutput(type_error)
g "g"
)

//:: ExpectedOutput(parser_error)
//:: ExpectedOutput(type_error)
import m "lib/mathm" // wrong package name used on purpose such that this test case does not potentially depend on the configured Go path
//:: ExpectedOutput(parser_error)
//:: ExpectedOutput(type_error)
import . "lib/mathn"

func test() {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

package main

//:: ExpectedOutput(parser_error)
//:: ExpectedOutput(type_error)
import math "lib/mathm" // wrong package name used on purpose such that this test case does not potentially depend on the configured Go path

type cell struct{
Expand Down
2 changes: 1 addition & 1 deletion src/test/scala/viper/gobra/DetailedBenchmarkTests.scala
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ class DetailedBenchmarkTests extends BenchmarkTests {
val c = config.get
assert(c.packageInfoInputMap.size == 1)
val pkgInfo = c.packageInfoInputMap.keys.head
Right(Parser.parse(c, pkgInfo)(executor))
Parser.parse(c, pkgInfo)(executor)
})

private val typeChecking: NextStep[Map[AbstractPackage, ParseResult], TypeInfo, Vector[VerifierError]] =
Expand Down

0 comments on commit 6f41997

Please sign in to comment.