From bc35ffd1950c83ec63c59fe17f847c904cfb331d Mon Sep 17 00:00:00 2001 From: Naum-Tomov Date: Thu, 12 Oct 2023 14:10:25 +0200 Subject: [PATCH] fixed more None.get-s --- src/col/vct/col/origin/Blame.scala | 38 +++++++++---------- src/col/vct/col/origin/ExpectedError.scala | 2 +- src/col/vct/col/origin/Origin.scala | 8 ++++ .../vct/parsers/transform/JavaToCol.scala | 2 +- .../vct/rewrite/InlineApplicables.scala | 6 +-- .../viper/api/backend/silicon/Silicon.scala | 2 +- .../backend/silicon/SiliconLogListener.scala | 2 +- 7 files changed, 34 insertions(+), 26 deletions(-) diff --git a/src/col/vct/col/origin/Blame.scala b/src/col/vct/col/origin/Blame.scala index 6ae45d03cc..ea82f64189 100644 --- a/src/col/vct/col/origin/Blame.scala +++ b/src/col/vct/col/origin/Blame.scala @@ -15,17 +15,17 @@ sealed trait ContractFailure { case class ContractFalse(node: Expr[_]) extends ContractFailure { override def code: String = "false" override def descCompletion: String = "this expression may be false" - override def inlineDescCompletion: String = s"`${node.o.getInlineContext.get.inlineContext}` may be false" + override def inlineDescCompletion: String = s"`${node.o.getInlineContextOrElse()}` may be false" } case class InsufficientPermissionToExhale(node: Expr[_]) extends ContractFailure { override def code: String = "perm" override def descCompletion: String = "there might not be enough permission to exhale this amount" - override def inlineDescCompletion: String = s"there might be insufficient permission for `${node.o.getInlineContext.get.inlineContext}`" + override def inlineDescCompletion: String = s"there might be insufficient permission for `${node.o.getInlineContextOrElse()}`" } case class NegativePermissionValue(node: Expr[_]) extends ContractFailure { override def code: String = "negativePermValue" override def descCompletion: String = "the amount of permission in this permission predicate may be negative" - override def inlineDescCompletion: String = s"`${node.o.getInlineContext.get.inlineContext}` may be a negative permission amount" + override def inlineDescCompletion: String = s"`${node.o.getInlineContextOrElse()}` may be a negative permission amount" } trait VerificationFailure { @@ -76,9 +76,9 @@ trait NodeVerificationFailure extends VerificationFailure { def descInContext: String def inlineDescWithSource(source: String): String - override def position: String = node.o.getShortPosition.get.shortPosition + override def position: String = node.o.getShortPositionOrElse() override def desc: String = node.o.messageInContext(descInContext + errUrl) - override def inlineDesc: String = inlineDescWithSource(node.o.getInlineContext.get.inlineContext) + override def inlineDesc: String = inlineDescWithSource(node.o.getInlineContextOrElse()) } trait WithContractFailure extends VerificationFailure { @@ -89,7 +89,7 @@ trait WithContractFailure extends VerificationFailure { def descInContext: String def inlineDescWithSource(node: String, failure: String): String - override def position: String = node.o.getShortPosition.get.shortPosition + override def position: String = node.o.getShortPositionOrElse() override def code: String = s"$baseCode:${failure.code}" @@ -100,7 +100,7 @@ trait WithContractFailure extends VerificationFailure { )) override def inlineDesc: String = - inlineDescWithSource(node.o.getInlineContext.get.inlineContext, failure.inlineDescCompletion) + inlineDescWithSource(node.o.getInlineContextOrElse(), failure.inlineDescCompletion) } sealed trait ExpectedErrorFailure extends VerificationFailure { @@ -109,14 +109,14 @@ sealed trait ExpectedErrorFailure extends VerificationFailure { case class ExpectedErrorTrippedTwice(err: ExpectedError, left: VerificationFailure, right: VerificationFailure) extends ExpectedErrorFailure { override def code: String = "trippedTwice" - override def position: String = err.errorRegion.getShortPosition.get.shortPosition + override def position: String = err.errorRegion.getShortPositionOrElse() override def desc: String = err.errorRegion.messageInContext(s"The expected error with code `${err.errorCode}` occurred multiple times." + errUrl) override def inlineDesc: String = s"The expected error with code `${err.errorCode}` occurred multiple times." } case class ExpectedErrorNotTripped(err: ExpectedError) extends ExpectedErrorFailure { override def code: String = "notTripped" - override def position: String = err.errorRegion.getShortPosition.get.shortPosition + override def position: String = err.errorRegion.getShortPositionOrElse() override def desc: String = err.errorRegion.messageInContext(s"The expected error with code `${err.errorCode}` was not encountered." + errUrl) override def inlineDesc: String = s"The expected error with code `${err.errorCode}` was not encountered." } @@ -217,14 +217,14 @@ case class PostconditionFailed(path: Seq[AccountedDirection], failure: ContractF } case class TerminationMeasureFailed(applicable: ContractApplicable[_], apply: Invocation[_], measure: DecreasesClause[_]) extends ContractedFailure with VerificationFailure { override def code: String = "decreasesFailed" - override def position: String = measure.o.getShortPosition.get.shortPosition + override def position: String = measure.o.getShortPositionOrElse() override def desc: String = Origin.messagesInContext(Seq( applicable.o -> "Applicable may not terminate, since ...", apply.o -> "... from this invocation ...", measure.o -> "... this measure may not be bounded, or may not decrease.", )) override def inlineDesc: String = - s"`${apply.o.getInlineContext.get.inlineContext}` may not terminate, since `${measure.o.getInlineContext.get.inlineContext}` is not decreased or not bounded" + s"`${apply.o.getInlineContextOrElse()}` may not terminate, since `${measure.o.getInlineContextOrElse()}` is not decreased or not bounded" } case class ContextEverywhereFailedInPost(failure: ContractFailure, node: ContractApplicable[_]) extends ContractedFailure with WithContractFailure { override def baseCode: String = "contextPostFailed" @@ -254,9 +254,9 @@ case class LoopInvariantNotMaintained(failure: ContractFailure, node: LoopInvari } case class LoopTerminationMeasureFailed(node: DecreasesClause[_]) extends LoopInvariantFailure with NodeVerificationFailure { override def code: String = "loopDecreasesFailed" - override def position: String = node.o.getShortPosition.get.shortPosition + override def position: String = node.o.getShortPositionOrElse() override def descInContext: String = "Loop may not terminate, since this measure may not be bounded, or may not decrease." - override def inlineDescWithSource(source: String): String = s"Loop may not terminate, since `${node.o.getInlineContext.get.inlineContext}` may be unbounded or nondecreasing" + override def inlineDescWithSource(source: String): String = s"Loop may not terminate, since `${node.o.getInlineContextOrElse()}` may be unbounded or nondecreasing" } case class ReceiverNotInjective(quantifier: Starall[_], resource: Expr[_]) extends VerificationFailure with AnyStarError { override def code: String = "notInjective" @@ -264,9 +264,9 @@ case class ReceiverNotInjective(quantifier: Starall[_], resource: Expr[_]) exten quantifier.o -> "This quantifier causes the resources in its body to be quantified, ...", resource.o -> "... but this resource may not be unique with regards to the quantified variables.", )) - override def inlineDesc: String = s"The location of the permission predicate in `${resource.o.getInlineContext.get.inlineContext}` may not be unique with regards to the quantified variables." + override def inlineDesc: String = s"The location of the permission predicate in `${resource.o.getInlineContextOrElse()}` may not be unique with regards to the quantified variables." - override def position: String = resource.o.getShortPosition.get.shortPosition + override def position: String = resource.o.getShortPositionOrElse() } case class DivByZero(node: DividingExpr[_]) extends NodeVerificationFailure { override def code: String = "divByZero" @@ -356,7 +356,7 @@ case class KernelPostconditionFailed(failure: ContractFailure, node: CGpgpuKerne } case class KernelPredicateNotInjective(kernel: CGpgpuKernelSpecifier[_], predicate: Expr[_]) extends KernelFailure { override def code: String = "kernelNotInjective" - override def position: String = predicate.o.getShortPosition.get.shortPosition + override def position: String = predicate.o.getShortPositionOrElse() override def desc: String = Origin.messagesInContext(Seq( @@ -365,7 +365,7 @@ case class KernelPredicateNotInjective(kernel: CGpgpuKernelSpecifier[_], predica )) override def inlineDesc: String = - s"`${predicate.o.getInlineContext.get.inlineContext}` does not have a unique location for every thread, and it could not be simplified away." + s"`${predicate.o.getInlineContextOrElse()}` does not have a unique location for every thread, and it could not be simplified away." } sealed trait KernelBarrierFailure extends VerificationFailure @@ -420,7 +420,7 @@ case class ParBarrierInvariantBroken(failure: ContractFailure, node: ParBarrier[ sealed trait ParBlockFailure extends VerificationFailure case class ParPredicateNotInjective(block: ParBlock[_], predicate: Expr[_]) extends ParBlockFailure { override def code: String = "parNotInjective" - override def position: String = predicate.o.getShortPosition.get.shortPosition + override def position: String = predicate.o.getShortPositionOrElse() override def desc: String = Origin.messagesInContext(Seq( (block.o, "This parallel block causes the formulas in its body to be quantified over all threads, ..."), @@ -428,7 +428,7 @@ case class ParPredicateNotInjective(block: ParBlock[_], predicate: Expr[_]) exte )) override def inlineDesc: String = - s"`${predicate.o.getInlineContext.get.inlineContext}` does not have a unique location for every thread, and it could not be simplified away." + s"`${predicate.o.getInlineContextOrElse()}` does not have a unique location for every thread, and it could not be simplified away." } sealed trait ParBlockContractFailure extends ParBlockFailure diff --git a/src/col/vct/col/origin/ExpectedError.scala b/src/col/vct/col/origin/ExpectedError.scala index 85d53a17dc..6e658fd743 100644 --- a/src/col/vct/col/origin/ExpectedError.scala +++ b/src/col/vct/col/origin/ExpectedError.scala @@ -13,7 +13,7 @@ class ExpectedError(val errorCode: String, val errorRegion: Origin, val blame: B def trip(failure: VerificationFailure): Unit = tripped match { case None => - logger.debug(s"Swallowing error code $errorCode at ${errorRegion.getShortPosition.get.shortPosition}") + logger.debug(s"Swallowing error code $errorCode at ${errorRegion.getShortPositionOrElse()}") tripped = Some(failure) case Some(leftFailure) => blame.blame(ExpectedErrorTrippedTwice(this, leftFailure, failure)) diff --git a/src/col/vct/col/origin/Origin.scala b/src/col/vct/col/origin/Origin.scala index f2ac24402d..37bca786db 100644 --- a/src/col/vct/col/origin/Origin.scala +++ b/src/col/vct/col/origin/Origin.scala @@ -142,6 +142,10 @@ case class Origin(originContents: Seq[OriginContent]) extends Blame[Verification } } + def getInlineContextOrElse(ctx: String = "[unkonwn inline context]"): String = { + getInlineContext.getOrElse(InlineContext(ctx)).inlineContext + } + def getInlineBipContext: Option[InlineBipContext] = { originContents.flatMap { case InlineBipContext(any) => Seq(InlineBipContext(any)) @@ -172,6 +176,10 @@ case class Origin(originContents: Seq[OriginContent]) extends Blame[Verification } } + def getShortPositionOrElse(shortPos: String = "[unknown position]"): String = { + getShortPosition.getOrElse(ShortPosition(shortPos)).shortPosition + } + def getStartEndLines: Option[StartEndLines] = { originContents.flatMap { case StartEndLines(any) => Seq(StartEndLines(any)) diff --git a/src/parsers/vct/parsers/transform/JavaToCol.scala b/src/parsers/vct/parsers/transform/JavaToCol.scala index 28eee37920..b14ea062e7 100644 --- a/src/parsers/vct/parsers/transform/JavaToCol.scala +++ b/src/parsers/vct/parsers/transform/JavaToCol.scala @@ -138,7 +138,7 @@ case class JavaToCol[G](override val baseOrigin: Origin, def convert(implicit pair: ElementValuePairContext): Option[(String, Expr[G])] = pair match { case ElementValuePair0(name, _, ElementValue0(expr)) => - logger.warn(s"Annotation array initializer at ${OriginProvider(pair).getShortPosition.get.shortPosition} is discarded") + logger.warn(s"Annotation array initializer at ${OriginProvider(pair).getShortPositionOrElse()} is discarded") None case ElementValuePair0(name, _, ElementValue1(expr)) => Some((convert(name), convert(expr))) case x => ??(x) diff --git a/src/rewrite/vct/rewrite/InlineApplicables.scala b/src/rewrite/vct/rewrite/InlineApplicables.scala index 2d169b360c..1bc74e5327 100644 --- a/src/rewrite/vct/rewrite/InlineApplicables.scala +++ b/src/rewrite/vct/rewrite/InlineApplicables.scala @@ -64,7 +64,7 @@ case object InlineApplicables extends RewriterBuilder { private def InlinedOrigin(definition: Origin, usages: Seq[Apply[_]]): Origin = Origin( Seq( PreferredName(definition.getPreferredNameOrElse()), - ShortPosition(usages.head.o.getShortPosition.get.shortPosition), + ShortPosition(usages.head.o.getShortPositionOrElse()), Context(usages.map(_.o.getContext.get.context).mkString( start = " Inlined from:\n" + Origin.HR, sep = Origin.HR + " ...Then inlined from:\n" + Origin.HR, @@ -72,8 +72,8 @@ case object InlineApplicables extends RewriterBuilder { ) + Origin.HR + " In definition:\n" + Origin.HR + definition.getContext.get.context), - InlineContext(s"${definition.getInlineContext.get.inlineContext} [inlined from] " + - s"${usages.head.o.getInlineContext.get.inlineContext}") + InlineContext(s"${definition.getInlineContextOrElse()} [inlined from] " + + s"${usages.head.o.getInlineContextOrElse()}") ) ) diff --git a/src/viper/viper/api/backend/silicon/Silicon.scala b/src/viper/viper/api/backend/silicon/Silicon.scala index e87dbbd448..8c41ab5c1f 100644 --- a/src/viper/viper/api/backend/silicon/Silicon.scala +++ b/src/viper/viper/api/backend/silicon/Silicon.scala @@ -186,7 +186,7 @@ case class Silicon( report.e match { case Right(e) => val o = e.o - logger.info(s"${o.getShortPosition.get.shortPosition}: inst: ${report.instances} (gen: ${report.maxGeneration}, cost: ${report.maxCost})") + logger.info(s"${o.getShortPositionOrElse()}: inst: ${report.instances} (gen: ${report.maxGeneration}, cost: ${report.maxCost})") case Left(n) => logger.info(s"$n: inst: ${report.instances} (gen: ${report.maxGeneration}, cost: ${report.maxCost})") } diff --git a/src/viper/viper/api/backend/silicon/SiliconLogListener.scala b/src/viper/viper/api/backend/silicon/SiliconLogListener.scala index 2076992443..1c411f5bb3 100644 --- a/src/viper/viper/api/backend/silicon/SiliconLogListener.scala +++ b/src/viper/viper/api/backend/silicon/SiliconLogListener.scala @@ -82,7 +82,7 @@ class SiliconMemberLogListener(log: SiliconLogListener, member: Member, pcs: Pat currentTaskStack = updateTaskStack(currentTaskStack, superTask.get, Nil, Nil) } - def where(node: Node): Option[String] = Util.getOrigin(node).map(_.getShortPosition.get.shortPosition) + def where(node: Node): Option[String] = Util.getOrigin(node).map(_.getShortPositionOrElse()) def printRecords(records: mutable.Map[Int, DataRecord], excludedBy: Map[Int, Int]): Unit = { for(record <- records.values.toSeq.sortBy(_.id)) {