Clean up error transformations for closures

viperproject · Jul 10, 2024 · 4ed5c4f · 4ed5c4f
1 parent 6bfc8a0
commit 4ed5c4f
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 10 deletions.
diff --git a/src/main/scala/viper/gobra/translator/encodings/closures/ClosureEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/closures/ClosureEncoding.scala
@@ -9,7 +9,7 @@ package viper.gobra.translator.encodings.closures
 import org.bitbucket.inkytonik.kiama.==>
 import viper.gobra.ast.{internal => in}
 import viper.gobra.reporting
-import viper.gobra.reporting.BackTranslator.ErrorTransformer
+import viper.gobra.reporting.BackTranslator.{ErrorTransformer, RichErrorMessage}
 import viper.gobra.reporting.Source
 import viper.gobra.theory.Addressability
 import viper.gobra.theory.Addressability.{Exclusive, Shared}
@@ -137,6 +137,7 @@ class ClosureEncoding extends LeafTypeEncoding {
     * inhale closureImplements$[spec]([closure], [params])
     */
   private def specImplementationProof(proof: in.SpecImplementationProof)(ctx: Context): CodeWriter[vpr.Stmt] = {
+    val (exhalePos, _, _) = proof.vprMeta
     val inhalePres = cl.seqns(proof.pres map (a => for {
           ass <- ctx.assertion(a)
         } yield vpr.Inhale(ass)()))
@@ -145,11 +146,10 @@ class ClosureEncoding extends LeafTypeEncoding {
         rest <- acc
         ass <- ctx.assertion (a)
       } yield vpr.And(rest, ass) ())
-    } yield vpr.Exhale(assertions)()
+    } yield vpr.Exhale(assertions)(exhalePos)
 
-    def isSubnode(sub: vpr.Node, n: vpr.Node): Boolean = (sub eq n) || n.subnodes.exists(n => isSubnode(sub, n))
     def failedExhale: ErrorTransformer = {
-      case errors.ExhaleFailed(offendingNode, reason, _) if isSubnode(offendingNode, exhalePosts.res) =>
+      case e@errors.ExhaleFailed(_, reason, _) if e causedBy exhalePosts.res =>
         val info = proof.vprMeta._2.asInstanceOf[Source.Verifier.Info]
         reason match {
           case reason: reasons.AssertionFalse => reporting.SpecImplementationPostconditionError(info, proof.spec.info.tag)

diff --git a/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala b/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala
@@ -8,7 +8,7 @@ package viper.gobra.translator.encodings.closures
 
 import viper.gobra.ast.internal.FunctionLikeMemberOrLit
 import viper.gobra.ast.{internal => in}
-import viper.gobra.reporting.BackTranslator.ErrorTransformer
+import viper.gobra.reporting.BackTranslator.{ErrorTransformer, RichErrorMessage}
 import viper.gobra.reporting.{GoCallPreconditionReason, PreconditionError, Source, SpecNotImplementedByClosure}
 import viper.gobra.theory.Addressability
 import viper.gobra.translator.Names
@@ -313,10 +313,10 @@ protected class ClosureSpecsEncoder {
   }
 
   private var implementAssertionSpecOriginToStr: Map[Source.AbstractOrigin, String] = Map.empty
-  private def doesNotImplementSpecErr(callNode: vpr.Node, closureStr: String): ErrorTransformer = {
-    case vprerr.PreconditionInCallFalse(node@Source(info), reasons.AssertionFalse(Source(assInfo)), _) if (callNode eq node) && implementAssertionSpecOriginToStr.contains(assInfo.origin) =>
+  private def doesNotImplementSpecErr(callNode: vpr.Node with vpr.Positioned, closureStr: String): ErrorTransformer = {
+    case e@vprerr.PreconditionInCallFalse(Source(info), reasons.AssertionFalse(Source(assInfo)), _) if (e causedBy callNode) && implementAssertionSpecOriginToStr.contains(assInfo.origin) =>
       PreconditionError(info).dueTo(SpecNotImplementedByClosure(info, closureStr, implementAssertionSpecOriginToStr(assInfo.origin)))
-    case vprerr.PreconditionInAppFalse(node@Source(info), reasons.AssertionFalse(Source(assInfo)), _) if (callNode eq node) && implementAssertionSpecOriginToStr.contains(assInfo.origin) =>
+    case e@vprerr.PreconditionInAppFalse(Source(info), reasons.AssertionFalse(Source(assInfo)), _) if (e causedBy callNode) && implementAssertionSpecOriginToStr.contains(assInfo.origin) =>
       PreconditionError(info).dueTo(SpecNotImplementedByClosure(info, closureStr, implementAssertionSpecOriginToStr(assInfo.origin)))
   }
 

diff --git a/src/main/scala/viper/gobra/translator/encodings/closures/MethodObjectEncoder.scala b/src/main/scala/viper/gobra/translator/encodings/closures/MethodObjectEncoder.scala
@@ -7,7 +7,7 @@
 package viper.gobra.translator.encodings.closures
 
 import viper.gobra.ast.{internal => in}
-import viper.gobra.reporting.BackTranslator.ErrorTransformer
+import viper.gobra.reporting.BackTranslator.{ErrorTransformer, RichErrorMessage}
 import viper.gobra.reporting.{InterfaceReceiverIsNilReason, MethodObjectGetterPreconditionError, Source}
 import viper.gobra.translator.Names
 import viper.gobra.translator.context.Context
@@ -102,7 +102,7 @@ class MethodObjectEncoder(domain: ClosureDomainEncoder) {
     in.MethodProxy(s"${Names.closureGetter}$$${meth.name}", s"${Names.closureGetter}$$${meth.uniqueName}")(meth.info)
 
   private def receiverNilErr(m: in.MethodObject, call: vpr.Exp): ErrorTransformer = {
-    case vprerr.PreconditionInAppFalse(offendingNode, _, _) if call eq offendingNode =>
+    case e@vprerr.PreconditionInAppFalse(_, _, _) if e causedBy call=>
       val info = m.vprMeta._2.asInstanceOf[Source.Verifier.Info]
       val recvInfo = m.recv.vprMeta._2.asInstanceOf[Source.Verifier.Info]
       MethodObjectGetterPreconditionError(info).dueTo(InterfaceReceiverIsNilReason(recvInfo))