Allow non-side-effectful conversions in spec

src/main/scala/viper/gobra/frontend/Desugar.scala

@@ -20,7 +20,7 @@ import viper.gobra.reporting.{DesugaredMessage, Source}
 import viper.gobra.theory.Addressability
 import viper.gobra.translator.Names
 import viper.gobra.util.Violation.violation
-import viper.gobra.util.{Constants, DesugarWriter, TypeBounds, Violation}
+import viper.gobra.util.{Constants, DesugarWriter, Violation}
 
 import scala.annotation.{tailrec, unused}
 import scala.collection.{Iterable, SortedSet}
@@ -2805,20 +2805,18 @@ object Desugar {
       val src: Meta = meta(expr, info)
       info.resolve(expr) match {
         case Some(p: ap.FunctionLikeCall) => functionLikeCallD(ctx, info)(p, expr)(src)
-        case Some(ap.Conversion(typ, arg)) =>
+        case Some(c@ap.Conversion(typ, arg)) =>
           val typType = info.symbType(typ)
-          val argType = info.typ(arg)
-
-          (underlyingType(typType), underlyingType(argType)) match {
-            case (SliceT(IntT(TypeBounds.Byte)), StringT) =>
-              val resT = typeD(SliceT(IntT(TypeBounds.Byte)), Addressability.Exclusive)(src)
+          underlyingType(typType) match {
+            case l if info.isEffectfulConversion(c) =>
+              val resT = typeD(l, Addressability.Exclusive)(src)
               for {
                 target <- freshDeclaredExclusiveVar(resT, expr, info)(src)
                 dArg <- exprD(ctx, info)(arg)
                 conv: in.EffectfulConversion = in.EffectfulConversion(target, resT, dArg)(src)
                 _ <- write(conv)
               } yield target
-            case (t: InterfaceT, _) =>
+            case t: InterfaceT =>
               for {
                 exp <- exprD(ctx, info)(arg)
                 tD  =  typeD(t, exp.typ.addressability)(src)

src/main/scala/viper/gobra/frontend/info/TypeInfo.scala

@@ -26,6 +26,7 @@ trait TypeInfo extends ExternalTypeInfo {
   def regular(n: PIdnNode): Regular
 
   def isDef(n: PIdnUnk): Boolean
+  def isEffectfulConversion(c: AstPattern.Conversion): Boolean
 
   def resolve(n: PExpressionOrType): Option[AstPattern.Pattern]
   def exprOrType(n: PExpressionOrType): Either[PExpression, PType]

src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala

@@ -12,7 +12,7 @@ import viper.gobra.frontend.info.base.SymbolTable.{AdtDestructor, AdtDiscriminat
 import viper.gobra.frontend.info.base.Type._
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.util.TypeBounds.{BoundedIntegerKind, UnboundedInteger}
-import viper.gobra.util.{Constants, Violation}
+import viper.gobra.util.{Constants, TypeBounds, Violation}
 
 trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
 
@@ -1054,4 +1054,13 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
       case _: SequenceT | _: SetT | _: MultisetT | _: MathMapT | _: AdtT => UNTYPED_INT_CONST
       case t => violation(s"unexpected argument ${expr.exp} of type $t passed to len")
     }
+
+  override def isEffectfulConversion(c: ap.Conversion): Boolean = {
+    val fromType = underlyingType(exprType(c.arg))
+    val toType = underlyingType(typeSymbType(c.typ))
+    (fromType, toType) match {
+      case (StringT, SliceT(IntT(TypeBounds.Byte))) => true
+      case _ => false
+    }
+  }
 }

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala

@@ -360,14 +360,7 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
       // Might change at some point
       case n: PInvoke => (exprOrType(n.base), resolve(n)) match {
         case (Right(_), Some(p: ap.Conversion)) =>
-          val dstTyp = symbType(p.typ)
-          val exprTyp = typ(p.arg)
-          (underlyingType(dstTyp), underlyingType(exprTyp)) match {
-            case (SliceT(IntT(TypeBounds.Byte)), StringT) =>
-              // this is an effectful conversion which produces permissions to the resulting slice
-              false
-            case _ => go(p.arg)
-          }
+          !isEffectfulConversion(p) && go(p.arg)
         case (Left(callee), Some([email protected](f, _))) => go(callee) && p.args.forall(go) && (f match {
           case ap.Function(_, symb) => symb.isPure
           case ap.Closure(_, symb) => symb.isPure

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostWellDef.scala

@@ -129,7 +129,7 @@ trait GhostWellDef { this: TypeInfoImpl =>
       ) => error(n, "ghost error: Found ghost child expression, but expected none", !noGhostPropagationFromChildren(n))
 
     case n: PInvoke => (exprOrType(n.base), resolve(n)) match {
-      case (Right(_), Some(_: ap.Conversion)) =>  error(n, "ghost error: Found ghost child expression, but expected none", !noGhostPropagationFromChildren(n))
+      case (Right(_), Some(_: ap.Conversion)) => noMessages
       case (Left(_), Some(call: ap.FunctionCall)) => ghostAssignableToCallExpr(call)
       case (Left(_), Some(call: ap.ClosureCall)) => ghostAssignableToClosureCall(call)
       case (Left(_), Some(_: ap.PredicateCall)) => noMessages

src/test/resources/regressions/features/conversion/conversion-fail01.gobra

@@ -0,0 +1,10 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package main
+
+// Rejected, as this conversion is side-effectful, as thus
+// it is not a pure expression.
+//:: ExpectedOutput(type_error)
+ensures res === []byte(s)
+func to64(s string) (res []byte)

src/test/resources/regressions/features/conversion/conversion-simple01.gobra

@@ -0,0 +1,7 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package main
+
+ensures res == int64(i)
+func to64(i int8) (res int64)