silver AdtPlugin java.lang.ClassCastException

Hello! I found my way here through doing some research for Prusti and I noticed the ADT plugin got merged very recently :) This looks like a really great feature, thank you for adding it! I set my Viper IDE to nightly and took it for a spin. I managed to break something when adding a post-condition that mentions a returned ADT:

adt Test {
    A()
    B()
}

function test(): Test
    ensures result.isA
{
    A()
}

This results in the error:

Server: Issue of severity 1: [silicon] [exception] 1:1 The verification job #16 resulted in a terrible error:
java.util.concurrent.ExecutionException:
viper.server.core.ServerCrashException:
java.lang.ClassCastException:
class viper.silver.plugin.standard.adt.Adt cannot be cast to class viper.silver.ast.Domain
(viper.silver.plugin.standard.adt.Adt and viper.silver.ast.Domain are in unnamed module of loader 'app')

Everything seems to work for pre-conditions okay, as far as I can tell this error is only triggered by a post-condition that mentions an ADT result. I suspect this corner case was missed when translating from the Parser AST to the Viper AST.

May 24 '22 12:05 Pointerbender

I did a bit of investigation. I was not able to resolve it yet, but here is some additional information about the underlying issue.

The beforeResolve stage resolves without an error. Then during the resolving, it tries to translate a PResultLit() into a Result(..)

https://github.com/viperproject/silver/blob/5503e4a736a2b9b455ed279a66c34c1597907c77/src/main/scala/viper/silver/parser/Translator.scala#L369-L376

and errors here on line 586:

https://github.com/viperproject/silver/blob/5503e4a736a2b9b455ed279a66c34c1597907c77/src/main/scala/viper/silver/parser/Translator.scala#L583-L586

This is because the members map still contains an Adt instead of a Domain at this point. The Adt is not translated into a Domain until after the translation during the beforeVerify phase (initiated on line 136):

https://github.com/viperproject/silver/blob/5503e4a736a2b9b455ed279a66c34c1597907c77/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala#L132-L137

The tricky part here is, that it needs a Program in order to convert the Adts into Domains, which is not available until the PProgram has been translated into a Program. But in order to translate the PResultLit the PAdts need to have been converted back to PDomains and there we have a circular dependency :)

I'm not sure how to best tackle this. With some help I may be able to do it. One idea I have left after playing around a bit is to encode both the PAdt and PDomain at the same time under different names. Here the PAdt for adt Foo { .. } will receive the name adt_Foo and the corresponding PDomain will get the name Foo, so that user facing errors messages will reference the name originally picked by the user. Along that, because PFunction return types will hold a PDomainType, it will find to correct PDomain during translation without conflicting with the name of the PAdt. Would this be a good approach, or is there a better alternative? Thanks!

May 26 '22 19:05 Pointerbender

Actually, after sleeping on it for a night, I think I have a nicer idea: I can just translate the PResultLit to a new custom PAdtResultLit whenever it references an ADT and then write a custom translation from PAdtResultLit to Result :) Going to give that a try!

May 27 '22 07:05 Pointerbender

I created PR #582 for a quick fix for some corner cases, however, this is not a sufficient fix yet. For example, this program still crashes:

adt Test {
    A()
    B(b: Int)
}

function baz(): Test
    ensures result == A()
{
    A()
}

but with a different error:

[typechecker.error] expected identifier, but got PAdtConstructor(PIdnDef(A),List())
([email protected]) (AnnotationBasedTestSuite.scala:63)

So far I still think that creating a custom PAdtResultLit is the best way to go in order to solve all corner cases, however, I have been unsuccessful at making this work so far (the adtSubstitution is then always empty for some reason in src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala).

May 27 '22 13:05 Pointerbender

I have some extra information to share that was accumulated during a Zulip discussion with Alex Summers:

Ideally, when the transformer here:

https://github.com/viperproject/silver/blob/5503e4a736a2b9b455ed279a66c34c1597907c77/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala#L110-L129

reaches the PFunction case, it should replace the PDomainType return type with a PAdtType return type. Even though the case is not explicitly listed in the pattern matching, the default behavior should still do something similar to this:

case pf@PFunction(idndef, formalArgs, typ, pres, posts, body) =>
        PFunction(
          idndef,
          formalArgs map transformStrategy,
          transformStrategy(typ), // transforms the PDomainType to PAdtType
          pres map transformStrategy,
          posts map transformStrategy,
          body map transformStrategy
        )(pf.pos)

Even when adding this case for PFunction explicitly, the following sanity check still throws an exception:

      case pr@PResultLit() => {
        // find function and check that its return type was updated
        var par: PNode = pr.parent.get
        while (!par.isInstanceOf[PFunction]) {
          if (par == null) sys.error("cannot use 'result' outside of function")
          par = par.parent.get
        }
        par match {
          case pf@PFunction(idndef, formalArgs, typ@PDomainType(idnuse, args), pres, posts, body) if declaredAdtNames.exists(_.name == idnuse.name) =>
            throw new Exception("not transformed: " + pr + " | " + pf)
        }
        PResultLit()(pr.pos)

The weird part is, that even though the function return type is properly replaced during the PFunction case, this change is not visible in the same transformation run when going from the PResultLit child back to its PFunction ancestor (nor is it visible in the subsequent translation stage). The default traversal order is the Traverse.TopDown direction, so it visits the PFunction before the PResultLit.

Might this be an issue with the transformation code itself?

May 27 '22 19:05 Pointerbender

This hack seems to work for most corner cases:

https://github.com/viperproject/silver/blob/2fe26fb919ab67442bf102e54751df38c327541f/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala#L122-L136

However, this does not solve the corner case from this comment, still. I'm hoping that there is a better solution that fixes the transformer so that all corner cases work without any hacks, although unfortunately I was unable to spot it so far :)

May 27 '22 20:05 Pointerbender