Call method with ghost variable with same name as instance variable fails

[J3173]

Calling a method with a ghost variable with the same name as an instance variable in the calling class fails with the error argument i is missing.

Example:

public class A {
  int i;

  public void main() {
    B b = new B();

    b.testA()/*@ with {a = 9;} @*/;
    b.testI()/*@ with {i = 9;} @*/;
  }
}

class B {
  /*@
    given int a;
  @*/
  public void testA() {
  }

  /*@
    given int i;
  @*/
  public void testI() {
  }
}

The call to testA works correctly, but the call to testI fails. When renaming the instance variable to x, both calls succeed.

Reported error:

At file BugTest.java from line 8 column 5 until line 8 column 13: argument i is missing

[sjcjoosten]

I'm guessing this one is related to #179

[pieter-bos]

I figured out why this is happening, but now I'm a little stuck. Obviously i is interpreted as a field of A instead of as an argument, but the logic to prevent this is almost already there: the with statement is in the AST as a BlockStatement, and BlockStatements respect method aruguments when their parent is a MethodInvokation: https://github.com/utwente-fmt/vercors/blob/e6f0a2e198ca4e0ccf1fd3e3baae3bb7421cbaec/vercors/src/main/java/vct/col/ast/ASTFrame.java#L375-L382.

However, it is decided in the very first pass java_resolve whether i should be a field or something else. At this moment, the definition of the method call is still unknown: the definition is resolved in the check pass. I tried adding a check pass before the java_resolve pass, but java_resolve solves a bunch of type errors.

in conclusion, it seems check and java_resolve are interdependent in this case. I'm open to suggestions for a solution.

[pieter-bos]

After discussion with @sjcjoosten: we should just restrict the syntax for passing given arguments, so fields etc. just cannot appear on the left-hand side of assignments in a with statement. However, I found an example where there is more complex usage of with and then, so I'm not sure whether we still want to proceed this way: https://github.com/utwente-fmt/vercors/blob/master/examples/layers/LFQ.java

[sjcjoosten]

The more complicated example shows some great use of the current power of with and then. I think the example would also go through if the with part was just used as ghost code before the call though?

[pieter-bos]

Yes, that is probably true, so we can go ahead with the proposed solution for with. Another thing though, the same issue arises when using yielded variables in then statements, what should we do about that?

[sjcjoosten]

Let's first rewrite LFQ.java s.t. it works with the proposed new syntax.

[pieter-bos]

The attached patch contains the changes required to change the with syntax. After trying to fix LFQ.java we encountered a difficult-to-diagnose issue, so we are abandoning this issue for now.

issue4.patch

[sjcjoosten]

I do have a hypothesis as to what happens: when using the with syntax, first the pre-conditions of the function are checked, and then the with block is 'executed'. Consequently, the checking of the conditions in the with block benefit from the asserts that the pre-conditions of the function give it. In the case of LFQ.java, this seems to be necessary. As Pieter said, we are not going to fix this for now. Feel free to reopen if you can make LFQ.java work without the with syntax.