Fix a pinch of errors

viperproject · Jan 31, 2024 · dc28aca · dc28aca
1 parent a764da9
commit dc28aca
Show file tree

Hide file tree

Showing 3 changed files with 33 additions and 28 deletions.
diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala
@@ -2215,14 +2215,14 @@ object Desugar extends LazyLogging {
         case base: ap.FunctionKind => base match {
           case _: ap.Function | _: ap.BuiltInFunction =>
             if (isPure) {
+              if (expr.reveal && !isOpaque) {
+                violation("Cannot reveal a non-opaque function")
+              }
+
               for {
                 args <- dArgs
                 convertedArgs = convertArgs(args)
                 spec = p.maybeSpec.map(closureSpecD(ctx, info))
-
-                if (expr.reveal && !isOpaque) {
-                  violation("Cannot reveal a non-opaque function")
-                }
               } yield Right(pureFunctionCall(base, convertedArgs, spec, resT, expr.reveal))
             } else {
               for {
@@ -2237,13 +2237,18 @@ object Desugar extends LazyLogging {
             violation(info == iim.symb.context.getTypeInfo,
               "invariance in desugarer violated: interface methods can only be implicitly call in the interface itself")
             if (isPure) {
+              if (expr.reveal && !isOpaque) {
+                violation("Cannot reveal a non-opaque implicitly received interface method")
+              }
               for {
                 args <- dArgs
                 convertedArgs = convertArgs(args)
                 proxy = methodProxy(iim.id, iim.symb.context.getTypeInfo)
                 recvType = typeD(iim.symb.itfType, Addressability.receiver)(src)
                 spec = p.maybeSpec.map(closureSpecD(ctx, info))
-              } yield Right(pureMethodCall(implicitThisD(recvType)(src), proxy, args, spec, resT))
+                // I don't know whether this is fully correct, as opaque/reveal should only really be
+                // implemented for normal method calls for now (e.g., not for whatever this is)
+              } yield Right(pureMethodCall(implicitThisD(recvType)(src), proxy, args, spec, resT, expr.reveal))
             } else {
               for {
                 args <- dArgs
@@ -2283,16 +2288,16 @@ object Desugar extends LazyLogging {
             }
 
             if (isPure) {
+              if (expr.reveal && !isOpaque) {
+                violation("Cannot reveal a non-opaque method")
+              }
+
               for {
                 (recv, args) <- dRecvWithArgs
                 convertedArgs = convertArgs(args)
                 mproxy = getMethodProxy(base, recv, convertedArgs)
                 spec = p.maybeSpec.map(closureSpecD(ctx, info))
-
-                if (expr.reveal && !isOpaque) {
-                  violation("Cannot reveal a non-opaque method")
-                }
-                // I don't know whether this is fully correct, as opaque should only really be
+                // I don't know whether this is fully correct, as opaque/reveal should only really be
                 // implemented for normal method calls for now (e.g., not for closures)
               } yield Right(pureMethodCall(recv, mproxy, convertedArgs, spec, resT, expr.reveal))
             } else {

diff --git a/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultPureMethodEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultPureMethodEncoding.scala
@@ -28,6 +28,10 @@ class DefaultPureMethodEncoding extends Encoding {
 
     val (pos, info, errT) = meth.vprMeta
 
+    if (meth.isOpaque) {
+      info = VprInfo.attachOpaque(info)
+    }
+
     val vRecv = ctx.variable(meth.receiver)
     val vRecvPres = ctx.varPrecondition(meth.receiver).toVector
 
@@ -56,10 +60,6 @@ class DefaultPureMethodEncoding extends Encoding {
         )(ctx)
       })
 
-      if (meth.isOpaque) {
-        info = VprInfo.attachOpaque(info)
-      }
-
       function = vpr.Function(
         name = meth.name.uniqueName,
         formalArgs = vRecv +: vArgs,
@@ -77,6 +77,10 @@ class DefaultPureMethodEncoding extends Encoding {
 
     val (pos, info, errT) = func.vprMeta
 
+    if (func.isOpaque) {
+      info = VprInfo.attachOpaque(info)
+    }
+
     val vArgs = func.args.map(ctx.variable)
     val vArgPres = func.args.flatMap(ctx.varPrecondition)
 
@@ -102,10 +106,6 @@ class DefaultPureMethodEncoding extends Encoding {
         )(ctx)
       })
 
-      if (func.isOpaque) {
-        info = VprInfo.attachOpaque(info)
-      }
-
       function = vpr.Function(
         name = func.name.name,
         formalArgs = vArgs,

diff --git a/src/main/scala/viper/gobra/translator/encodings/typeless/CallEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/typeless/CallEncoding.scala
@@ -24,30 +24,30 @@ class CallEncoding extends Encoding {
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = {
     case x@in.PureFunctionCall(func, args, typ, reveal) =>
       val (pos, info, errT) = x.vprMeta
+
+      if (reveal) {
+        info = VprInfo.attachReveal(info)
+      }
+
       val resultType = ctx.typ(typ)
 
       for {
         vArgs <- sequence(args map ctx.expression)
-
-        if (reveal) {
-          info = VprInfo.attachReveal(info)
-        }
-
         app = vpr.FuncApp(func.name, vArgs)(pos, info, resultType, errT)
       } yield app
 
     case x@in.PureMethodCall(recv, meth, args, typ, reveal) =>
       val (pos, info, errT) = x.vprMeta
+
+      if (reveal) {
+          info = VprInfo.attachReveal(info)
+      }
+
       val resultType = ctx.typ(typ)
 
       for {
         vRecv <- ctx.expression(recv)
         vArgs <- sequence(args map ctx.expression)
-
-        if (reveal) {
-          info = VprInfo.attachReveal(info)
-        }
-
         app = vpr.FuncApp(meth.uniqueName, vRecv +: vArgs)(pos, info, resultType, errT)
       } yield app
   }