Syntax & typing errors in translation to Viper

[icmccorm]

Viper requires that variables inside method bodies cannot be named result, and that all methods have their return value assigned to something. The frontend guarantees neither of these, which results in many errors of the following form:

Verification aborted exceptionally: 
java.util.concurrent.ExecutionException: 
java.util.concurrent.ExecutionException: 
scala.MatchError: ? && true (of class viper.silver.ast.ImpreciseExp)

Fixing these syntax and typing issues fixes the error. This can be observed when translating this incorrect program to its correct version.

[conradz]

The frontend should guarantee the latter, as a function of the type/well-formedness checker. Is this program coming from the permutor? Because I'm pretty sure it wouldn't pass the type checker in the frontend.

[conradz]

Also, if this is a problem (specifically the no return problem) introduced by the permutor, there would seem to be an even bigger issue since I would expect all permutations to have the same executable code.

[conradz]

Just took a closer look at the incorrect program, and it appears that all code paths return a value (i.e. assign $result) in all methods. Is the root problem actually only the first problem noted (that result is a reserved word)?

[hgouni]

This is a program produced by the permutor, yeah. It's entirely possible the return value assignment issue is only present in the pretty printed Viper program (not the AST node representation the frontend passes to Silicon). To be clear, the actual issue in this case is that for any method call, the return value must be assigned to a variable to pass Silver's type checker (even if the method is only being called for its side effects).

At least, this is what I had to do to get the program to pass Silver's parsing and typechecking.

[conradz]

@hemantgouni where is the missing return assignment? I don't see one in the incorrect version.

[hgouni]

All invocations of fixup_ancestors never have a return value assigned (those are the only incorrect calls).

[hgouni]

Sorry, I realized we're talking about different things, since Viper has a notion of assigning to return parameters: I'm referring to assigning the return value of a method (following a call) to some local variable at the call site.

[conradz]

Yes, I just realized that as well. I had thought you meant a code path never assigned to the method's return value, but you were in fact meaning the return value of a callee is not assigned to anything. That is #14, which I have a plan for fixing and plan to do so pretty soon.

[hgouni]

Alright, good to hear! Once that and the other issue are resolved, I think the MatchError issue we've been seeing from the permutor should be fixed (hopefully).