Improve language flexibility

[JonasAlaif]

Changes the PAst and Ast to make things more flexible. The following statements are now accepted:

field n: Ref
method get_refs() returns (x: Ref, y: Ref)
method main() {
    var a: Ref, b: Ref, c: Int             // Declare multiple locals at once
    var d: Ref, e: Ref := get_refs()       // Declare and assign locals from method call
    var f: Ref := new(n)                   // Declare and initialise locals with `new`

    a, f.n := get_refs()                   // Assign field-access from method call
    f.n := new(n)                          // Assign field-access with `new`
}

In the PAst I have removed the PMethodCall (it would anyway often get parsed as PLocalVarAssign), but the corresponding Ast version MethodCall remains.

[mschwerhoff]

Why change the AST as well, instead of desugaring this from PASTs and frontends? Without good reasons, we should keep the language that hits the backends minimal.

[marcoeilers]

Also, AST changes always mean all frontends, plugins etc. will have to be adapted.
If at all possible, I agree that a parser/PAST-only implementation would be better.

[JonasAlaif]

@marcoeilers @mschwerhoff, I've scaled back the changes, however I still need to change the Ast slightly since we want a MethodCalls and NewStmts to be able to assign to an arbitrary Lhs rather than only LocalVars. This could be avoided by introducing local temporaries when translating PAst to Ast, but that seemed a bit too hacky for me imo?

[marcoeilers]

A couple of comments and questions

[fpoli]

Even after what discussed in the meeting, there are still many possible interpretations of the following program:

• Is the LHS of L1 evaluated before or after the RHS? If it's evaluated after, then the unfoldings should fail because the P(x) has been consumed by the method call.
• Are the components of the LHS evaluated at the same time, or one after the other? In the former case one might expect the evaluation of the LHS to require P(x) * P(x), in the latter just P(x).

field f: Ref

predicate P(x: Ref) { acc(x.f) }

method foo(x: Ref) returns (a: Ref, b: Ref)
    requires P(x)

method test(x: Ref)
    requires P(x) && acc((unfolding P(x) in x.f).f)
{
    (unfolding P(x) in x.f).f, (unfolding P(x) in x.f).f := foo(x); // L1
}

One definition of the semantics can be the following: there is first a viper-to-viper desugaring

e1.f1, e2.f2, ... := RHS

🡇🡇🡇

{
    let v1: ...;
    let v2: ...;
    v1 := e1;
    v2 := e2;
    ...
    v1.f1, v2.f2, ... := RHS
}

and then the verifier checks that in the desugared LHS there are no two variables with the same value using the same field, as already discussed.

(Whatever the semantics is, we should not forget to add it to the tutorial.)

[fpoli]

Oh, and should the following fail or not? The method returns the permission that is needed for the LHS.

field f: Ref

method foo(x: Ref) returns (a: Ref)
    ensures acc(x.f)

method test(x: Ref) {
    x.f := foo(x);
}

Another variant, where the method consumes the permission that is needed for the LHS. Checking well-definedness of the desugared LHS before the call would succeed, but the call would then update a field without having permission to it. That doesn't seem right.

field f: Ref

method foo(x: Ref) returns (a: Ref)
    requires acc(x.f)

method test(x: Ref)
    requires acc(x.f)
{
    x.f := foo(x);
}

My opinion is that both programs should be disallowed, because the well-definedness check of the method call should check the separating conjunction <permissions of the desugared LHS> * <permissions of the precondition>. Intuitively, it's like if the user declared that the value of the (desugared) x.f doesn't change during the call, which seems fine to me.

Anyway, I think that checking the well-definedness of the desugared LHS separately from the well-definedness of the call would be wrong. They should be done at once.

[mschwerhoff]

@JonasAlaif As mentioned earlier: is there any need for actually extending the core language or can the additional flexibility be desugared after parsing? My impression is: yes it can, and that the additional flexibility, while great for writing Viper programs by hand, is not that important for frontends. Desugaring would allow the AST to remain unchanged; otherwise, frontends, backends, transformers etc. all might have to be adapted.

[JonasAlaif]

@mschwerhoff since the de-sugaring seems possible, I've implemented that now and so the Ast remains unchanged with this PR

[JonasAlaif]

Regarding the encoding, I decided to copy that of Java

e1.f1, e2.f2, ... := RHS

encodes as

{
    let rcv1: ...;
    let tgt1: ...;
    let rcv2: ...;
    let tgt2: ...;
    ...
    rcv1 := e1;
    rcv2 := e2;
    ...
    tgt1, tgt2, ... := RHS;
    rcv1.f1 := tgt1;
    rcv2.f2 := tgt2;
    ...
}

The receiver is evaluated before the call and the assignment happens after the call. This means that

field f: Ref

method foo(x: Ref) returns (a: Ref)
    ensures acc(x.f)

method test(x: Ref) {
    x.f := foo(x);
}

is accepted. While

field f: Ref

method foo(x: Ref) returns (a: Ref)
    requires acc(x.f)

method test(x: Ref)
    requires acc(x.f)
{
    x.f := foo(x);
}

would be rejected.

[JonasAlaif]

@marcoeilers please review 😇

[marcoeilers]

A couple of suggestions mostly regarding naming, one question about what our new syntax actually allows.
Also, I think a couple of additional tests that check that we get the correct type and name resolution errors for the newly-supported stuff would be great.

[marcoeilers]

Ah wait. Before you merge this: Since it's a language change, this is still the kind of thing where it might make sense for you to show it in a Viper meeting first (at least briefly) before it's merged in, both to show the new features and to see if people find any conceptual issues or have any additional ideas.

[JonasAlaif]

The PR is now ready to be merged, just waiting for the next meeting in a week in case there are any concerns.

[JonasAlaif]

@marcoeilers I've added the error transformation, but in Silicon at least it has no effect since there's I guess a bug that Silicon just never calls transformedError and ignores the transformation.

[JonasAlaif]

@marcoeilers I was wrong, yeah I had added it before leaving. Then I think that this is ready to merge?

[marcoeilers]

Oh, I didn't realize that the CI failure was because of required changes in the backend. Yes, let's merge this then if the backends both pass.