Skip to content

Commit

Permalink
fixes compilation errors
Browse files Browse the repository at this point in the history
  • Loading branch information
@ArquintL
ArquintL committed Jun 30, 2023
1 parent cda37bc commit 52317a4
Show file tree
Hide file tree
Showing 3 changed files with 116 additions and 87 deletions.
177 changes: 104 additions & 73 deletions src/test/scala/viper/gobra/BenchmarkTests.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ import org.rogach.scallop.throwError

import java.nio.file.Path
import org.scalatest.{ConfigMap, DoNotDiscover}
import scalaz.EitherT
import scalaz.Scalaz.futureInstance
import viper.gobra.frontend.{Config, PackageResolver, ScallopGobraConfig}
import viper.gobra.reporting.{NoopReporter, VerifierError, VerifierResult}
import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext, Violation}
Expand All @@ -19,6 +21,10 @@ import viper.silver.testing.StatisticalTestSuite
import viper.silver.verifier.{NoVerifier, Verifier}
import viper.silver.{verifier => vpr}

import java.util.concurrent.TimeUnit
import scala.concurrent.duration.Duration
import scala.concurrent.{Await, Future}

@DoNotDiscover
trait BenchmarkTests extends StatisticalTestSuite {

Expand Down Expand Up @@ -50,94 +56,119 @@ trait BenchmarkTests extends StatisticalTestSuite {
super.afterAll(configMap)
gobraFrontend.terminate()
}
}

trait GobraFrontendForTesting extends Frontend {
val z3PropertyName = "GOBRATESTS_Z3_EXE"
val z3Exe: Option[String] = Option(System.getProperty(z3PropertyName))
trait GobraFrontendForTesting extends Frontend {
val z3PropertyName = "GOBRATESTS_Z3_EXE"
val z3Exe: Option[String] = Option(System.getProperty(z3PropertyName))

protected implicit val executor: GobraExecutionContext = new DefaultGobraExecutionContext()
protected var config: Option[Config] = None
protected implicit val executor: GobraExecutionContext = new DefaultGobraExecutionContext()
protected var config: Option[Config] = None

/** Initialize this translator with a given verifier. Only meant to be called once. */
override def init(verifier: Verifier): Unit = () // ignore verifier argument as we reuse the Gobra / Parser / TypeChecker / etc. instances for all tests
/** Initialize this translator with a given verifier. Only meant to be called once. */
override def init(verifier: Verifier): Unit = () // ignore verifier argument as we reuse the Gobra / Parser / TypeChecker / etc. instances for all tests

override def reset(files: Seq[Path]): Unit =
createConfig(Array("-i", files.toVector.mkString(" ")))
override def reset(files: Seq[Path]): Unit =
createConfig(Array("-i", files.toVector.mkString(" ")))


private def createConfig(args: Array[String]): Config = {
// set throwError to true: Scallop will throw an exception instead of terminating the program in case an
// exception occurs (e.g. a validation failure)
throwError.value = true
// Simulate pick of package, Gobra normally does
val config = new ScallopGobraConfig(args.toSeq).config
Violation.violation(config.isRight, "creating the config has failed")
config.toOption.get.copy(reporter = NoopReporter, z3Exe = z3Exe)
}
private def createConfig(args: Array[String]): Config = {
// set throwError to true: Scallop will throw an exception instead of terminating the program in case an
// exception occurs (e.g. a validation failure)
throwError.value = true
// Simulate pick of package, Gobra normally does
val config = new ScallopGobraConfig(args.toSeq).config
Violation.violation(config.isRight, "creating the config has failed")
config.toOption.get.copy(reporter = NoopReporter, z3Exe = z3Exe)
}

def gobraResult: VerifierResult

/**
* The result of the verification attempt (only available after parse, typecheck, translate and
* verify have been called).
*/
override def result: vpr.VerificationResult = {
// transform Gobra errors back to vpr.AbstractError such that the benchmarking framework automatically handles them
gobraResult match {
case VerifierResult.Success => vpr.Success
case VerifierResult.Failure(errors) => vpr.Failure(errors.map(GobraTestError))
def gobraResult: VerifierResult

/**
* The result of the verification attempt (only available after parse, typecheck, translate and
* verify have been called).
*/
override def result: vpr.VerificationResult = {
// transform Gobra errors back to vpr.AbstractError such that the benchmarking framework automatically handles them
gobraResult match {
case VerifierResult.Success => vpr.Success
case VerifierResult.Failure(errors) => vpr.Failure(errors.map(GobraTestError))
}
}
}

def terminate(): Unit = {
executor.terminateAndAssertInexistanceOfTimeout()
}
def terminate(): Unit = {
executor.terminateAndAssertInexistanceOfTimeout()
}

/**
* Represents a phase in Gobra producing a result of type Either[E, O].
* As Phase is a case class defined in Frontend, this trait has to be defined here (instead of external to the Gobra frontent)
*/
trait Step[O, E] {
def res: Option[Either[E, O]]
def phase: Phase
def phases: Seq[Phase]
def reset(): Unit
}
/**
* Represents a phase in Gobra producing a result of type Either[E, O].
* As Phase is a case class defined in Frontend, this trait has to be defined here (instead of external to the Gobra frontend)
*/
trait Step[O, E] {
def res: Option[Either[E, O]]
def phase: Phase
def phases: Seq[Phase]
def reset(): Unit
}

case class InitialStep[E, O](name: String, fn: () => Either[E, O]) extends Step[O, E] {
var res: Option[Either[E, O]] = None
override val phase: Phase = Phase(name, () => {
res = Some(fn())
})
override def phases: Seq[Phase] = Seq(phase)
override def reset(): Unit =
case class InitialStep[E, O](name: String, fn: () => Either[E, O]) extends Step[O, E] {
var res: Option[Either[E, O]] = None
override val phase: Phase = Phase(name, () => {
res = Some(fn())
})
override def phases: Seq[Phase] = Seq(phase)
override def reset(): Unit =
res = None
}

case class InitialStepEitherT[E, O](name: String, fn: () => EitherT[E, Future, O]) extends Step[O, E] {
var res: Option[Either[E, O]] = None
override val phase: Phase = Phase(name, () => {
res = Some(Await.result(fn().toEither, Duration(timeoutSec, TimeUnit.SECONDS)))
})
override def phases: Seq[Phase] = Seq(phase)
override def reset(): Unit =
res = None
}

case class NextStep[I, E, O](name: String, prevStep: Step[I, E], fn: I => Either[E, O]) extends Step[O, E] {
var res: Option[Either[E, O]] = None
override val phase: Phase = Phase(name, () => {
assert(prevStep.res.isDefined)
res = prevStep.res match {
case Some(Right(output)) => Some(fn(output))
case Some(Left(errs)) => Some(Left(errs)) // propagate errors
}
})
override def phases: Seq[Phase] = prevStep.phases :+ phase
override def reset(): Unit =
prevStep.reset()
res = None
}
}

case class NextStep[I, O, E](name: String, prevStep: Step[I, E], fn: I => Either[E, O]) extends Step[O, E] {
var res: Option[Either[E, O]] = None
override val phase: Phase = Phase(name, () => {
assert(prevStep.res.isDefined)
res = prevStep.res match {
case Some(Right(output)) => Some(fn(output))
case Some(Left(errs)) => Some(Left(errs)) // propagate errors
}
})
override def phases: Seq[Phase] = prevStep.phases :+ phase
override def reset(): Unit =
prevStep.reset()
res = None
}
case class NextStepEitherT[I, E, O](name: String, prevStep: Step[I, E], fn: I => EitherT[E, Future, O]) extends Step[O, E] {
var res: Option[Either[E, O]] = None
override val phase: Phase = Phase(name, () => {
assert(prevStep.res.isDefined)
res = prevStep.res match {
case Some(Right(output)) => Some(Await.result(fn(output).toEither, Duration(timeoutSec, TimeUnit.SECONDS)))
case Some(Left(errs)) => Some(Left(errs)) // propagate errors
}
})
override def phases: Seq[Phase] = prevStep.phases :+ phase
override def reset(): Unit =
prevStep.reset()
res = None
}

case class GobraTestError(error: VerifierError) extends vpr.AbstractError {
/** The position where the error occured. */
override def pos: Position = error.position.getOrElse(NoPosition)
case class GobraTestError(error: VerifierError) extends vpr.AbstractError {
/** The position where the error occured. */
override def pos: Position = error.position.getOrElse(NoPosition)

/** A short and unique identifier for this error. */
override def fullId: String = error.id
/** A short and unique identifier for this error. */
override def fullId: String = error.id

/** A readable message describing the error. */
override def readableMessage: String = error.formattedMessage
/** A readable message describing the error. */
override def readableMessage: String = error.formattedMessage
}
}
}
21 changes: 10 additions & 11 deletions src/test/scala/viper/gobra/DetailedBenchmarkTests.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,9 @@
package viper.gobra

import java.nio.file.Path
import java.util.concurrent.TimeUnit
import org.scalatest.DoNotDiscover
import scalaz.EitherT
import scalaz.Scalaz.futureInstance
import viper.gobra.ast.internal.Program
import viper.gobra.ast.internal.transform.OverflowChecksTransform
import viper.gobra.backend.BackendVerifier
Expand All @@ -19,8 +20,7 @@ import viper.gobra.frontend.{Desugar, Parser}
import viper.gobra.reporting.{AppliedInternalTransformsMessage, BackTranslator, VerifierError, VerifierResult}
import viper.gobra.translator.Translator

import scala.concurrent.Await
import scala.concurrent.duration.Duration
import scala.concurrent.Future

/**
* Tool for benchmarking Gobra's performance split into its individual steps (wrapped as a ScalaTest).
Expand Down Expand Up @@ -100,24 +100,23 @@ class DetailedBenchmarkTests extends BenchmarkTests {
config = gobra.getAndMergeInFileConfig(c, pkgInfo).toOption
}

private val parsing = InitialStep[Vector[VerifierError], Map[AbstractPackage, ParseResult]]("parsing", () => {
private val parsing = InitialStepEitherT("parsing", () => {
assert(config.isDefined)
val c = config.get
assert(c.packageInfoInputMap.size == 1)
val pkgInfo = c.packageInfoInputMap.keys.head
Parser.parse(c, pkgInfo)(executor)
})

private val typeChecking: NextStep[Map[AbstractPackage, ParseResult], TypeInfo, Vector[VerifierError]] =
NextStep("type-checking", parsing, (parseResults: Map[AbstractPackage, ParseResult]) => {
private val typeChecking = NextStepEitherT("type-checking", parsing, (parseResults: Map[AbstractPackage, ParseResult]) => {
assert(config.isDefined)
val c = config.get
assert(c.packageInfoInputMap.size == 1)
val pkgInfo = c.packageInfoInputMap.keys.head
Info.check(c, RegularPackage(pkgInfo.id), parseResults)(executor)
})

private val desugaring: NextStep[TypeInfo, Program, Vector[VerifierError]] =
private val desugaring: NextStep[TypeInfo, Vector[VerifierError], Program] =
NextStep("desugaring", typeChecking, { case (typeInfo: TypeInfo) =>
assert(config.isDefined)
val c = config.get
Expand Down Expand Up @@ -146,14 +145,14 @@ class DetailedBenchmarkTests extends BenchmarkTests {
Right(Translator.translate(program, pkgInfo)(c))
})

private val verifying = NextStep("Viper verification", encoding, (viperTask: BackendVerifier.Task) => {
private val verifying = NextStepEitherT("Viper verification", encoding, (viperTask: BackendVerifier.Task) => {
assert(config.isDefined)
val c = config.get
assert(c.packageInfoInputMap.size == 1)
val pkgInfo = c.packageInfoInputMap.keys.head
val resultFuture = BackendVerifier.verify(viperTask, pkgInfo)(c)(executor)
.map(BackTranslator.backTranslate(_)(c))(executor)
Right(Await.result(resultFuture, Duration(timeoutSec, TimeUnit.SECONDS)))
val resultFuture: Future[Either[Vector[VerifierError], VerifierResult]] = BackendVerifier.verify(viperTask, pkgInfo)(c)
.map(res => Right(BackTranslator.backTranslate(res)(c)))
EitherT.fromEither(resultFuture)
})

private val lastStep = verifying
Expand Down
5 changes: 2 additions & 3 deletions src/test/scala/viper/gobra/GobraTests.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ import org.scalatest.{Args, BeforeAndAfterAll, Status}
import scalaz.Scalaz.futureInstance
import viper.gobra.frontend.PackageResolver.RegularPackage
import viper.gobra.frontend.Source.FromFileSource
import viper.gobra.frontend.TaskManagerMode.{Lazy, Parallel}
import viper.gobra.frontend.info.Info
import viper.gobra.frontend.{Config, PackageResolver, Parser, Source}
import viper.gobra.reporting.VerifierResult.{Failure, Success}
Expand Down Expand Up @@ -66,9 +65,9 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
val config = getConfig(source)
val pkgInfo = config.packageInfoInputMap.keys.head
val fut = for {
parseResult <- Parser.parseFut(config, pkgInfo)
parseResult <- Parser.parse(config, pkgInfo)
pkg = RegularPackage(pkgInfo.id)
typeCheckResult <- Info.checkFut(config, pkg, parseResult)
typeCheckResult <- Info.check(config, pkg, parseResult)
} yield typeCheckResult
fut.toEither
})
Expand Down

0 comments on commit 52317a4

Please sign in to comment.