Fixes #745 (#746)

viperproject · Mar 20, 2024 · cc786c5 · cc786c5
1 parent c5457c8
commit cc786c5
Show file tree

Hide file tree

Showing 7 changed files with 68 additions and 6 deletions.
diff --git a/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala b/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala
@@ -6,8 +6,7 @@
 
 package viper.gobra.reporting
 
-import viper.gobra.reporting.Source.{AutoImplProofAnnotation, CertainSource, CertainSynthesized, ImportPreNotEstablished, MainPreNotEstablished, OverflowCheckAnnotation, ReceiverNotNilCheckAnnotation, InsufficientPermissionToRangeExpressionAnnotation, LoopInvariantNotEstablishedAnnotation}
-
+import viper.gobra.reporting.Source.{AutoImplProofAnnotation, CertainSource, CertainSynthesized, ImportPreNotEstablished, InsufficientPermissionToRangeExpressionAnnotation, LoopInvariantNotEstablishedAnnotation, MainPreNotEstablished, OverflowCheckAnnotation, OverwriteErrorAnnotation, ReceiverNotNilCheckAnnotation}
 import viper.gobra.reporting.Source.Verifier./
 import viper.silver
 import viper.silver.ast.Not
@@ -163,6 +162,8 @@ class DefaultErrorBackTranslator(
     }
 
     val transformAnnotatedError: VerificationError => VerificationError = x => x.info match {
+      case _ / (an: OverwriteErrorAnnotation) => an(x)
+
       case _ / OverflowCheckAnnotation =>
         x.reasons.foldLeft(OverflowError(x.info): VerificationError){ case (err, reason) => err dueTo reason }
 

diff --git a/src/main/scala/viper/gobra/reporting/Source.scala b/src/main/scala/viper/gobra/reporting/Source.scala
@@ -33,6 +33,16 @@ object Source {
   case class NoPermissionToRangeExpressionAnnotation() extends Annotation
   case class InsufficientPermissionToRangeExpressionAnnotation() extends Annotation
   case class AutoImplProofAnnotation(subT: String, superT: String) extends Annotation
+  class OverwriteErrorAnnotation(
+                                  newError: VerificationError => VerificationError,
+                                  attachReasons: Boolean = true
+                                ) extends Annotation {
+    def apply(err: VerificationError): VerificationError = {
+      if (attachReasons) {
+        err.reasons.foldLeft(newError(err)){ case (err, reason) => err dueTo reason }
+      } else newError(err)
+    }
+  }
 
   object Parser {
 

diff --git a/src/main/scala/viper/gobra/reporting/VerifierError.scala b/src/main/scala/viper/gobra/reporting/VerifierError.scala
@@ -161,6 +161,11 @@ case class CallError(info: Source.Verifier.Info) extends VerificationError {
   override def localMessage: String = "Call might fail"
 }
 
+case class LoadError(info: Source.Verifier.Info) extends VerificationError {
+  override def localId: String = "load_error"
+  override def localMessage: String = "Reading might fail"
+}
+
 case class PostconditionError(info: Source.Verifier.Info) extends VerificationError {
   override def localId: String = "postcondition_error"
   override def localMessage: String = "Postcondition might not hold"

diff --git a/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala
@@ -8,7 +8,7 @@ package viper.gobra.translator.encodings.arrays
 
 import org.bitbucket.inkytonik.kiama.==>
 import viper.gobra.ast.{internal => in}
-import viper.gobra.reporting.Source
+import viper.gobra.reporting.{LoadError, InsufficientPermissionError, Source}
 import viper.gobra.theory.Addressability
 import viper.gobra.theory.Addressability.{Exclusive, Shared}
 import viper.gobra.translator.Names
@@ -230,7 +230,11 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
       val (pos, info, errT) = loc.vprMeta
       for {
         arg <- ctx.reference(loc)
-      } yield conversionFunc(Vector(arg), cptParam(len, t)(ctx))(pos, info, errT)(ctx)
+        res <- funcAppPrecondition(
+          conversionFunc(Vector(arg), cptParam(len, t)(ctx))(pos, info, errT)(ctx),
+          { case (info, _) => LoadError(info) dueTo InsufficientPermissionError(info) }
+        )
+      } yield res
   }
 
   /**

diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
@@ -10,7 +10,7 @@ import org.bitbucket.inkytonik.kiama.==>
 import viper.gobra.ast.{internal => in}
 import viper.gobra.ast.internal.theory.Comparability
 import viper.gobra.reporting.BackTranslator.{ErrorTransformer, RichErrorMessage}
-import viper.gobra.reporting.{DefaultErrorBackTranslator, LoopInvariantNotWellFormedError, MethodContractNotWellFormedError, NoPermissionToRangeExpressionError, Source}
+import viper.gobra.reporting.{AssignmentError, DefaultErrorBackTranslator, LoopInvariantNotWellFormedError, MethodContractNotWellFormedError, NoPermissionToRangeExpressionError, Source}
 import viper.gobra.theory.Addressability.{Exclusive, Shared}
 import viper.gobra.translator.library.Generator
 import viper.gobra.translator.context.Context
@@ -175,7 +175,7 @@ trait TypeEncoding extends Generator {
         for {
           footprint <- addressFootprint(ctx)(loc, in.FullPerm(loc.info))
           eq <- ctx.equal(loc, rhs)(src)
-          _ <- write(vpr.Exhale(footprint)(pos, info, errT))
+          _ <- exhaleWithDefaultReason(footprint, AssignmentError)
           inhale = vpr.Inhale(vpr.And(footprint, eq)(pos, info, errT))(pos, info, errT)
         } yield inhale
       )

diff --git a/src/main/scala/viper/gobra/translator/util/ViperWriter.scala b/src/main/scala/viper/gobra/translator/util/ViperWriter.scala
@@ -408,6 +408,16 @@ object ViperWriter {
       }
     }
 
+    /* Can be used in expressions. */
+    def funcAppPrecondition(call: vpr.FuncApp, reasonT: (Source.Verifier.Info, ErrorReason) => VerificationError): Writer[vpr.Exp] = {
+      for {
+        _ <- errorT({
+          case e@vprerr.PreconditionInAppFalse(Source(info), reason, _) if e causedBy call =>
+            reasonT(info, reason)
+        })
+      } yield call
+    }
+
     /* Emits Viper statements. */
     def assert(cond: vpr.Exp, reasonT: (Source.Verifier.Info, ErrorReason) => VerificationError): Writer[Unit] = {
       val res = vpr.Assert(cond)(cond.pos, cond.info, cond.errT)

diff --git a/src/test/resources/regressions/issues/000745.gobra b/src/test/resources/regressions/issues/000745.gobra
@@ -0,0 +1,32 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue000745
+
+func assignment() int {
+    var x@, y [10]int
+    exhale acc(&x)
+    //:: ExpectedOutput(assignment_error:permission_error)
+    x = y
+}
+
+func load0() int {
+    var x@, y int
+    exhale acc(&x)
+    //:: ExpectedOutput(assignment_error:permission_error)
+    y = x
+}
+
+func load1() int {
+    var x@, y struct{ f,g int }
+    exhale acc(&x)
+    //:: ExpectedOutput(assignment_error:permission_error)
+    y = x
+}
+
+func load2() int {
+    var x@, y [10]int
+    exhale acc(&x)
+    //:: ExpectedOutput(load_error:permission_error)
+    y = x
+}