AdtPlugin java.lang.ClassCastException

[Pointerbender]

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.

[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(..)

silver/src/main/scala/viper/silver/parser/Translator.scala

Lines 369 to 376 in 5503e4a

	case p@PResultLit() =>
	// find function
	var par: PNode = p.parent.get
	while (!par.isInstanceOf[PFunction]) {
	if (par == null) sys.error("cannot use 'result' outside of function")
	par = par.parent.get
	}
	Result(ttyp(par.asInstanceOf[PFunction].typ))(pos)

and errors here on line 586:

silver/src/main/scala/viper/silver/parser/Translator.scala

Lines 583 to 586 in 5503e4a

	case PDomainType(name, args) =>
	members.get(name.name) match {
	case Some(d) =>
	val domain = d.asInstanceOf[Domain]

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):

silver/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala

Lines 132 to 137 in 5503e4a

	override def beforeVerify(input: Program): Program = {
	if (deactivated) {
	return input
	}
	new AdtEncoder(input).encode()
	}

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!

[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!

[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())
(issue-581.vpr@23.5--23.6) (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).

[Pointerbender]

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

Ideally, when the transformer here:

silver/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala

Lines 110 to 129 in 5503e4a

	def transformStrategy[T <: PNode](input: T): T = StrategyBuilder.Slim[PNode]({
	// If derives import is missing deriving info is ignored
	case pa@PAdt(idndef, typVars, constructors, _) if !derivesImported => PAdt(idndef, typVars, constructors, Seq.empty)(pa.pos)
	case pa@PDomainType(idnuse, args) if declaredAdtNames.exists(_.name == idnuse.name) => PAdtType(idnuse, args)(pa.pos)
	case pc@PCall(idnuse, args, typeAnnotated) if declaredConstructorNames.exists(_.name == idnuse.name) => PConstructorCall(idnuse, args, typeAnnotated)(pc.pos)
	// A destructor call or discriminator call might be parsed as left-hand side of a field assignment, which is illegal. Hence in this case
	// we simply treat the calls as an ordinary field access, which results in an identifier not found error.
	case pfa@PFieldAssign(fieldAcc, rhs) if declaredConstructorArgsNames.exists(_.name == fieldAcc.idnuse.name) ||
	declaredConstructorNames.exists("is" + _.name == fieldAcc.idnuse.name) =>
	PFieldAssign(PFieldAccess(transformStrategy(fieldAcc.rcv), fieldAcc.idnuse)(fieldAcc.pos), transformStrategy(rhs))(pfa.pos)
	case pfa@PFieldAccess(rcv, idnuse) if declaredConstructorArgsNames.exists(_.name == idnuse.name) => PDestructorCall(idnuse.name, rcv)(pfa.pos)
	case pfa@PFieldAccess(rcv, idnuse) if declaredConstructorNames.exists("is" + _.name == idnuse.name) => PDiscriminatorCall(PIdnUse(idnuse.name.substring(2))(idnuse.pos), rcv)(pfa.pos)
	}).recurseFunc({
	// Stop the recursion if a destructor call or discriminator call is parsed as left-hand side of a field assignment
	case PFieldAssign(fieldAcc, _) if declaredConstructorArgsNames.exists(_.name == fieldAcc.idnuse.name) ||
	declaredConstructorNames.exists("is" + _.name == fieldAcc.idnuse.name) => Seq()
	case n: PNode => n.children collect { case ar: AnyRef => ar }
	}).execute(input)
	transformStrategy(input)

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?

[Pointerbender]

This hack seems to work for most corner cases:

silver/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala

Lines 122 to 136 in 2fe26fb

	case pr@PResultLit() => {
	// The transformations applied to the return type of the parent `PFunction` are not known to the `PResultLit`.
	// This is hack to make the return type known despite that, see https://github.com/viperproject/silver/issues/581.
	var par: PNode = pr.parent.get
	while (!par.isInstanceOf[PFunction]) {
	if (par == null) sys.error("cannot use 'result' outside of function")
	val nextpar = par.parent.get
	if (nextpar.isInstanceOf[PFunction]) {
	val func = nextpar.asInstanceOf[PFunction]
	par.parent = Some(func.copy(typ = transformStrategy(func.typ))(func.pos))
	}
	par = par.parent.get
	}
	pr
	}

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 :)