Fix issue 491

src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala

@@ -594,6 +594,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case DfltVal(typ) => "dflt" <> brackets(showType(typ))
     case Tuple(args) => parens(showExprList(args))
     case Deref(exp, _) => "*" <> showExpr(exp)
+    case UncheckedRef(ref, _) => "&" <> showAddressable(ref)
     case Ref(ref, _) => "&" <> showAddressable(ref)
     case FieldRef(recv, field) => showExpr(recv) <> "."  <> field.name
     case StructUpdate(base, field, newVal) => showExpr(base) <> brackets(showField(field) <+> ":=" <+> showExpr(newVal))

src/main/scala/viper/gobra/ast/internal/Program.scala

@@ -1001,7 +1001,18 @@ case class Deref(exp: Expr, underlyingTypeExpr: Type)(val info: Source.Parser.In
   override val typ: Type = underlyingTypeExpr.asInstanceOf[PointerT].t
 }
 
-case class Ref(ref: Addressable, typ: PointerT)(val info: Source.Parser.Info) extends Expr with Location
+/** Only used internally to separate the type encodings. Should not be created by the desugarer. */
+case class UncheckedRef(ref: Addressable, typ: PointerT)(val info: Source.Parser.Info) extends Expr {
+  def checked: Ref = Ref(ref, typ)(info)
+}
+
+object UncheckedRef {
+  def apply(exp: Expr)(info: Source.Parser.Info): UncheckedRef = Ref(exp)(info).unchecked
+}
+
+case class Ref(ref: Addressable, typ: PointerT)(val info: Source.Parser.Info) extends Expr {
+  def unchecked: UncheckedRef = UncheckedRef(ref, typ)(info)
+}
 
 object Ref {
   def apply(ref: Expr)(info: Source.Parser.Info): Ref = {

src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala

@@ -95,7 +95,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
     }
 

src/main/scala/viper/gobra/reporting/VerifierError.scala

@@ -483,9 +483,9 @@ 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"
+  override def message: String = s"The receiver ${node.origin.tag.trim} might be nil"
 }
 
 case class DynamicValueNotASubtypeReason(node: Source.Verifier.Info) extends VerificationErrorReason {

src/main/scala/viper/gobra/translator/context/Context.scala

@@ -99,6 +99,8 @@ trait Context {
 
   def reference(x: in.Location): CodeWriter[vpr.Exp] = typeEncoding.reference(this)(x)
 
+  def safeReference(x: in.Location): CodeWriter[vpr.Exp] = typeEncoding.safeReference(this)(x)
+
   def value(x: in.Expr): CodeWriter[vpr.Exp] = typeEncoding.value(this)(x)
 
   def footprint(x: in.Location, perm: in.Expr): CodeWriter[vpr.Exp] = typeEncoding.addressFootprint(this)(x, perm)
@@ -138,15 +140,14 @@ trait Context {
   }
 
   // mapping
-
   def addVars(vars: vpr.LocalVarDecl*): Context
 
   // fresh variable counter
   /** publicly exposed infinite iterator providing fresh names */
   def freshNames: Iterator[String] = internalFreshNames
 
   /** internal fresh name iterator that additionally provides a getter function for its counter value */
-  protected def internalFreshNames: FreshNameIterator
+  protected def internalFreshNames: Context.FreshNameIterator
 
   /** copy constructor */
   def :=(
@@ -165,7 +166,28 @@ trait Context {
           unknownValueN: UnknownValues = unknownValue,
           typeEncodingN: TypeEncoding = typeEncoding,
           defaultEncodingN: DefaultEncoding = defaultEncoding,
-          initialFreshCounterValueN: Int = internalFreshNames.getValue
+          initialFreshCounterValueN: Option[Int] = None,
+        ): Context = {
+    update(fieldN, arrayN, seqToSetN, seqToMultisetN, seqMultiplicityN, optionN, optionToSeqN, sliceN, fixpointN, tupleN, equalityN, conditionN, unknownValueN, typeEncodingN, defaultEncodingN, initialFreshCounterValueN)
+  }
+
+  protected def update(
+          fieldN: Fields,
+          arrayN: Arrays,
+          seqToSetN: SeqToSet,
+          seqToMultisetN: SeqToMultiset,
+          seqMultiplicityN: SeqMultiplicity,
+          optionN: Options,
+          optionToSeqN: OptionToSeq,
+          sliceN: Slices,
+          fixpointN: Fixpoint,
+          tupleN: Tuples,
+          equalityN: Equality,
+          conditionN: Conditions,
+          unknownValueN: UnknownValues,
+          typeEncodingN: TypeEncoding,
+          defaultEncodingN: DefaultEncoding,
+          initialFreshCounterValueN: Option[Int],
         ): Context
 
 
@@ -189,8 +211,10 @@ trait Context {
     col.finalize(typeEncoding)
   }
 
+}
+
+object Context {
   trait FreshNameIterator extends Iterator[String] {
     def getValue: Int
   }
-
 }

src/main/scala/viper/gobra/translator/context/ContextImpl.scala

@@ -22,25 +22,25 @@ import viper.gobra.translator.library.tuples.Tuples
 import viper.gobra.translator.library.unknowns.UnknownValues
 import viper.silver.ast.LocalVarDecl
 
-case class ContextImpl(
-                        field: Fields,
-                        array: Arrays,
-                        seqToSet: SeqToSet,
-                        seqToMultiset: SeqToMultiset,
-                        seqMultiplicity: SeqMultiplicity,
-                        option: Options,
-                        optionToSeq: OptionToSeq,
-                        slice: Slices,
-                        fixpoint: Fixpoint,
-                        tuple: Tuples,
-                        equality: Equality,
-                        condition: Conditions,
-                        unknownValue: UnknownValues,
-                        typeEncoding: TypeEncoding,
-                        defaultEncoding: DefaultEncoding,
-                        table: LookupTable,
-                        initialFreshCounterValue: Int = 0
-                      ) extends Context {
+class ContextImpl(
+                   override val field: Fields,
+                   override val array: Arrays,
+                   override val seqToSet: SeqToSet,
+                   override val seqToMultiset: SeqToMultiset,
+                   override val seqMultiplicity: SeqMultiplicity,
+                   override val option: Options,
+                   override val optionToSeq: OptionToSeq,
+                   override val slice: Slices,
+                   override val fixpoint: Fixpoint,
+                   override val tuple: Tuples,
+                   override val equality: Equality,
+                   override val condition: Conditions,
+                   override val unknownValue: UnknownValues,
+                   override val typeEncoding: TypeEncoding,
+                   override val defaultEncoding: DefaultEncoding,
+                   override val table: LookupTable,
+                   override val internalFreshNames: Context.FreshNameIterator = ContextImpl.FreshNameIteratorImpl(0),
+                 ) extends Context {
 
   def this(conf: TranslatorConfig, table: LookupTable) = {
     this(
@@ -64,24 +64,24 @@ case class ContextImpl(
   }
 
   /** copy constructor */
-  override def :=(
-                   fieldN: Fields = field,
-                   arrayN: Arrays = array,
-                   seqToSetN: SeqToSet = seqToSet,
-                   seqToMultisetN: SeqToMultiset = seqToMultiset,
-                   seqMultiplicityN: SeqMultiplicity = seqMultiplicity,
-                   optionN: Options = option,
-                   optionToSeqN: OptionToSeq = optionToSeq,
-                   sliceN: Slices = slice,
-                   fixpointN: Fixpoint = fixpoint,
-                   tupleN: Tuples = tuple,
-                   equalityN: Equality = equality,
-                   conditionN: Conditions = condition,
-                   unknownValueN: UnknownValues = unknownValue,
-                   typeEncodingN: TypeEncoding = typeEncoding,
-                   defaultEncodingN: DefaultEncoding = defaultEncoding,
-                   initialFreshCounterValueN: Int = internalFreshNames.getValue
-                 ): Context = copy(
+  override def update(
+                   fieldN: Fields,
+                   arrayN: Arrays,
+                   seqToSetN: SeqToSet,
+                   seqToMultisetN: SeqToMultiset,
+                   seqMultiplicityN: SeqMultiplicity,
+                   optionN: Options,
+                   optionToSeqN: OptionToSeq,
+                   sliceN: Slices,
+                   fixpointN: Fixpoint,
+                   tupleN: Tuples,
+                   equalityN: Equality,
+                   conditionN: Conditions,
+                   unknownValueN: UnknownValues,
+                   typeEncodingN: TypeEncoding,
+                   defaultEncodingN: DefaultEncoding,
+                   initialFreshCounterValueN: Option[Int],
+                 ): Context = new ContextImpl(
     fieldN,
     arrayN,
     seqToSetN,
@@ -97,14 +97,18 @@ case class ContextImpl(
     unknownValueN,
     typeEncodingN,
     defaultEncodingN,
-    initialFreshCounterValue = initialFreshCounterValueN
+    table,
+    initialFreshCounterValueN match {
+      case None => internalFreshNames
+      case Some(n) => ContextImpl.FreshNameIteratorImpl(n)
+    },
   )
 
   override def addVars(vars: LocalVarDecl*): Context = this
+}
 
-  override val internalFreshNames: FreshNameIteratorImpl = FreshNameIteratorImpl(initialFreshCounterValue)
-
-  case class FreshNameIteratorImpl(private val initialValue: Int) extends FreshNameIterator {
+object ContextImpl {
+  case class FreshNameIteratorImpl(private val initialValue: Int) extends Context.FreshNameIterator {
     private var currentValue: Int = initialValue
 
     override def hasNext: Boolean = true
@@ -117,5 +121,4 @@ case class ContextImpl(
 
     override def getValue: Int = currentValue
   }
-
 }

src/main/scala/viper/gobra/translator/encodings/PointerEncoding.scala

@@ -72,7 +72,6 @@ class PointerEncoding extends LeafTypeEncoding {
     * Ref[*e] -> [e]
     */
   override def reference(ctx: Context): in.Location ==> CodeWriter[vpr.Exp] = default(super.reference(ctx)){
-    case (loc: in.Deref) :: _ / Shared =>
-      ctx.expression(loc.exp)
+    case (loc: in.Deref) :: _ / Shared => ctx.expression(loc.exp)
   }
 }

src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala

@@ -145,7 +145,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
     * R[ mset(e: [n]T) ] -> seqToMultiset(ex_array_toSeq([e]))
     * R[ x in (e: [n]T) ] -> [x] in ex_array_toSeq([e])
     * R[ x # (e: [n]T) ] -> [x] # ex_array_toSeq([e])
-    * R[ loc: ([n]T)@ ] -> arrayConversion(L[loc])
+    * R[ loc: ([n]T)@ ] -> arrayConversion(Ref[loc]) // assert [&loc != nil] if [n]T has size zero
     */
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = default(super.expression(ctx)){
     case (loc@ in.IndexedExp(base :: ctx.Array(len, t), idx, _)) :: _ / Exclusive =>
@@ -175,7 +175,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
     case n@ in.Length(e :: ctx.Array(len, t) / m) =>
       m match {
         case Exclusive => ctx.expression(e).map(ex.length(_, cptParam(len, t)(ctx))(n)(ctx))
-        case Shared => ctx.reference(e.asInstanceOf[in.Location]).map(sh.length(_, cptParam(len, t)(ctx))(n)(ctx))
+        case Shared => ctx.safeReference(e.asInstanceOf[in.Location]).map(sh.length(_, cptParam(len, t)(ctx))(n)(ctx))
       }
 
     case in.Length(exp :: ctx.*(t: in.ArrayT)) =>
@@ -221,7 +221,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
         vE <- ctx.expression(e)
       } yield ctx.seqMultiplicity.create(vX, ex.toSeq(vE, cptParam(len, t)(ctx))(n)(ctx))(pos, info, errT)
 
-    case (loc: in.Location) :: ctx.Array(len, t) / Shared =>
+    case (loc: in.Location) :: ctx.NoZeroSize(ctx.Array(len, t)) / Shared =>
       val (pos, info, errT) = loc.vprMeta
       for {
         arg <- ctx.reference(loc)
@@ -260,12 +260,15 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
     * i.e. all permissions involved in converting the shared location to an exclusive r-value.
     * An encoding for type T should be defined at all shared locations of type T.
     *
+    * The default implements:
+    * Footprint[loc: T@ if sizeOf(T) == 0] -> [&loc != nil: *T°]
+    *
     * Footprint[loc: [n]T] -> forall idx :: {trigger} 0 <= idx < n ==> Footprint[ loc[idx] ]
     *   where trigger = sh_array_get(Ref[loc], idx, n)
     *
     * We do not use let because (at the moment) Viper does not accept quantified permissions with let expressions.
     */
-  override def addressFootprint(ctx: Context): (in.Location, in.Expr) ==> CodeWriter[vpr.Exp] = {
+  override def addressFootprint(ctx: Context): (in.Location, in.Expr) ==> CodeWriter[vpr.Exp] = super.addressFootprint(ctx).orElse {
     case (loc :: ctx.Array(len, t) / Shared, perm) =>
       val (pos, info, errT) = loc.vprMeta
       val typ = underlyingType(loc.typ)(ctx)
@@ -311,13 +314,16 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
     * */
   private val conversionFunc: FunctionGenerator[ComponentParameter] = new FunctionGenerator[ComponentParameter]{
     def genFunction(t: ComponentParameter)(ctx: Context): vpr.Function = {
+      val info = Source.Parser.Internal
+
       val argType = t.arrayT(Shared)
       // variable name does not matter because it is the only argument
-      val x = in.LocalVar("x", argType)(Source.Parser.Internal)
+      val x = in.LocalVar("x", argType)(info)
+
       val resultType = argType.withAddressability(Exclusive)
       val vResultType = typ(ctx)(resultType)
       // variable name does not matter because it is turned into a vpr.Result
-      val resultVar = in.LocalVar("res", resultType)(Source.Parser.Internal)
+      val resultVar = in.LocalVar("res", resultType)(info)
       val post = pure(equal(ctx)(x, resultVar, x))(ctx).res
         // replace resultVar with vpr.Result
         .transform{ case v: vpr.LocalVar if v.name == resultVar.id => vpr.Result(vResultType)() }
@@ -327,7 +333,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
         formalArgs = Vector(variable(ctx)(x)),
         typ = vResultType,
         pres = Vector(
-          pure(addressFootprint(ctx)(x, in.WildcardPerm(Source.Parser.Internal)))(ctx).res,
+          pure(addressFootprint(ctx)(x, in.WildcardPerm(info)))(ctx).res,
           synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate")
         ),
         posts = Vector(post),

src/main/scala/viper/gobra/translator/encodings/closures/MethodObjectEncoder.scala

@@ -8,7 +8,7 @@ package viper.gobra.translator.encodings.closures
 
 import viper.gobra.ast.{internal => in}
 import viper.gobra.reporting.BackTranslator.{ErrorTransformer, RichErrorMessage}
-import viper.gobra.reporting.{InterfaceReceiverIsNilReason, MethodObjectGetterPreconditionError, Source}
+import viper.gobra.reporting.{ReceiverIsNilReason, MethodObjectGetterPreconditionError, Source}
 import viper.gobra.translator.Names
 import viper.gobra.translator.context.Context
 import viper.gobra.translator.encodings.interfaces.{InterfaceComponent, InterfaceComponentImpl, InterfaceUtils, PolymorphValueComponent, PolymorphValueComponentImpl, TypeComponent, TypeComponentImpl}
@@ -105,6 +105,6 @@ class MethodObjectEncoder(domain: ClosureDomainEncoder) {
     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))
+      MethodObjectGetterPreconditionError(info).dueTo(ReceiverIsNilReason(recvInfo))
   }
 }