"cannot translate wildcard at an arbitrary position" when multiplying with wildcard

[bobismijnnaam]

I have a problem similar to #169, where a runtime exception is thrown with the error:

Exception in thread "main" java.lang.RuntimeException: cannot translate wildcard at an arbitrary position (should only occur directly in an accessibility predicate)

It happens on carbon master with the following input:

//  a field 
field Node_rank: Int

method Main_parrallel_region_main_1_Sequence$Node$_EncodedGlobalVariables(diz: Ref, nodes: Seq[Ref])
  requires 0 < |nodes| ==> (forall j: Int :: { nodes[j].Node_rank } 0 <= j && j < |nodes| ==> acc(nodes[j].Node_rank, |nodes| * wildcard))
{
  inhale false
}

Silicon seems to verify it without problems. Will multiplication with wildcards be unsupported in the future, or is this an instance of #169?

[gauravpartha]

I don't think it's an instance of #169, but rather an instance of #85. It seems that Carbon only supports multiplication of wildcards if it can be trivially determined that the other factor is strictly positive. I'll bring this topic up in the next meeting with the Viper team (which is next month) and then report here on whether this should be supported or not.

It would be interesting to know why such multiplications show up in your encoding and whether you have feasible workarounds. Could you elaborate on that, please?

[bobismijnnaam]

This specific contract is the result of a parallel block. It starts a |nodes| number of threads, where each of the threads gets wildcard permission for nodes[j].rank. This gets aggregated into the contract you see here.

We could add simplification rules that simplifies the |nodes| part of the multiplication away to just wildcard, but of course that workaround won't cover all cases. Besides that, another workaround is to avoid wildcards, but they make the code a lot more readable so whenever that happens it is a sad occasion... Finally, we could require from the user to only use wildcard standalone, and then special case our transformation to take that into account and generate different code (I guess in my example the multiplication could've been left out with the guaranteed restricted use of wildcard), but we haven't looked into that yet.