From 081cd2a97d3952b5bf99b1506bec9c99f163316c Mon Sep 17 00:00:00 2001
From: "Felix A. Wolf" <felix.wolf@inf.ethz.ch>
Date: Wed, 20 Jul 2022 21:07:35 +0200
Subject: [PATCH] fix #491

---
 .../DefaultErrorBackTranslator.scala          |  2 +-
 .../viper/gobra/reporting/VerifierError.scala |  7 ++++++-
 .../encodings/PointerEncoding.scala           | 13 ++++++++++--
 .../resources/regressions/issues/000491.gobra | 20 +++++++++++++++++++
 4 files changed, 38 insertions(+), 4 deletions(-)
 create mode 100644 src/test/resources/regressions/issues/000491.gobra

diff --git a/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala b/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala
index feb8bf20e..a8a3fa134 100644
--- a/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala
+++ b/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala
@@ -84,7 +84,7 @@ object DefaultErrorBackTranslator {
 
     val transformVerificationErrorReason: VerificationErrorReason => VerificationErrorReason = {
       case AssertionFalseError(info / OverflowCheckAnnotation) => OverflowErrorReason(info)
-      case AssertionFalseError(info / ReceiverNotNilCheckAnnotation) => InterfaceReceiverIsNilReason(info)
+      case AssertionFalseError(info / ReceiverNotNilCheckAnnotation) => ReceiverIsNilReason(info)
       case x => x
     }
 
diff --git a/src/main/scala/viper/gobra/reporting/VerifierError.scala b/src/main/scala/viper/gobra/reporting/VerifierError.scala
index 38c8bb8be..52810a99e 100644
--- a/src/main/scala/viper/gobra/reporting/VerifierError.scala
+++ b/src/main/scala/viper/gobra/reporting/VerifierError.scala
@@ -155,6 +155,11 @@ case class CallError(info: Source.Verifier.Info) extends VerificationError {
   override def localMessage: String = "Call might fail"
 }
 
+case class DerefError(info: Source.Verifier.Info) extends VerificationError {
+  override def localId: String = "dereference_error"
+  override def localMessage: String = "Dereference 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"
@@ -381,7 +386,7 @@ case class OverflowErrorReason(node: Source.Verifier.Info) extends VerificationE
   override def message: String = s"Expression ${node.origin.tag.trim} might cause integer overflow."
 }
 
-case class InterfaceReceiverIsNilReason(node: Source.Verifier.Info) extends VerificationErrorReason {
+case class ReceiverIsNilReason(node: Source.Verifier.Info) extends VerificationErrorReason {
   override def id: String = "receiver_is_nil_error"
   override def message: String = s"The receiver might be nil"
 }
diff --git a/src/main/scala/viper/gobra/translator/encodings/PointerEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/PointerEncoding.scala
index 9b94bafae..4be5002da 100644
--- a/src/main/scala/viper/gobra/translator/encodings/PointerEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/PointerEncoding.scala
@@ -8,14 +8,17 @@ package viper.gobra.translator.encodings
 
 import org.bitbucket.inkytonik.kiama.==>
 import viper.gobra.ast.{internal => in}
+import viper.gobra.reporting.{DerefError, ReceiverIsNilReason, Source}
 import viper.gobra.theory.Addressability.{Exclusive, Shared}
 import viper.gobra.translator.encodings.combinators.LeafTypeEncoding
 import viper.gobra.translator.context.Context
 import viper.gobra.translator.util.ViperWriter.CodeWriter
+import viper.silver.verifier.ErrorReason
 import viper.silver.{ast => vpr}
 
 class PointerEncoding extends LeafTypeEncoding {
 
+  import viper.gobra.translator.util.ViperWriter.CodeLevel._
   import viper.gobra.translator.util.TypePatterns._
 
   /**
@@ -69,10 +72,16 @@ class PointerEncoding extends LeafTypeEncoding {
     * To avoid conflicts with other encodings, an encoding for type T should be defined at shared operations on type T.
     * Super implements shared variables with [[variable]].
     *
-    * Ref[*e] -> [e]
+    * Ref[*e] -> assert [e != nil]; [e]
     */
   override def reference(ctx: Context): in.Location ==> CodeWriter[vpr.Exp] = default(super.reference(ctx)){
     case (loc: in.Deref) :: _ / Shared =>
-      ctx.expression(loc.exp)
+      val errorT = (x: Source.Verifier.Info, _: ErrorReason) =>
+        DerefError(x).dueTo(ReceiverIsNilReason(x))
+      for {
+        e <- ctx.expression(loc.exp)
+        cond <- ctx.expression(in.UneqCmp(loc.exp, in.NilLit(loc.exp.typ)(loc.info))(loc.info))
+        res <- assert(cond, e, errorT)(ctx)
+      } yield res
   }
 }
diff --git a/src/test/resources/regressions/issues/000491.gobra b/src/test/resources/regressions/issues/000491.gobra
new file mode 100644
index 000000000..61bf4b78e
--- /dev/null
+++ b/src/test/resources/regressions/issues/000491.gobra
@@ -0,0 +1,20 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package main
+
+type A struct {
+	x int
+}
+
+func foo() {
+	var x *A
+	//:: ExpectedOutput(dereference_error:receiver_is_nil_error)
+	var y *A = &(*x)
+}
+
+func bar() {
+	var x *[3]int
+	//:: ExpectedOutput(dereference_error:receiver_is_nil_error)
+	var y []int = (*x)[:]
+}