Triggering problem due to unfolding introducing fresh snapshots under quantifiers

[viper-admin]

Created by bitbucket user fhahn on 2016-03-26 18:56 Last updated on 2016-03-28 11:41

When using unfolding to limit the range of indices of a quantified permission expression, non-nullness cannot be asserted.

#!scala

  requires forall j: Int :: 0 <= j && j < (unfolding acc(valid__Array(self$1), rd$1 / 2) in self$1.Array__len) ==> acc(loc(unfolding acc(valid__Array(self$1), rd$1 / 2) in self$1.Array__ptr, j).pval)
  requires forall j: Int :: 0 <= j && j < (unfolding acc(valid__Array(self$1), rd$1 / 2) in self$1.Array__len) ==> acc(loc(unfolding acc(valid__Array(self$1), rd$1 / 2) in self$1.Array__ptr, j).pval.Int__v)

The second precondition cannot be asserted and SIlicon raises the following error message:

Contract might not be well-formed. Receiver of loc((unfolding acc(valid__Array(self$1), rd$1 / 2) in self$1.Array__ptr), j).pval

When an integer variable is used as upper bound in j < (unfolding acc(valid__Array(self$1), rd$1 / 2) in self$1.Array__len), Silicon accepts both preconditions.

The attached test file contains both cases. Maybe related to https://github.com/viperproject/silicon/issues/61.

---

Attachments:

• 0228.sil
• test23.sil
• silicon-qp-wellformed.sil

[viper-admin]

@mschwerhoff commented on 2016-03-27 14:26

Technical problem

The unexpected verification failure is caused by a triggering problem: in the reported example, loc(unfolding ..., j) is the only possible trigger, and it mentions a snapshot whose "definition" is nested under the quantifier.

The assumption that forall j :: 0 <= j < len ==> loc(..., j) != null, which is due to inhaling permissions to loc(..., j).v, is guarded by the (only possible) trigger corresponding to loc(unfolding ..., j). The unfolding introduces two new snapshots s1 and s2 (one per conjunct in the body of valid), and the path condition that the snapshot s of chunk valid(this; s) is equal to the pair (s1, s2). s2, which is the value of this.ptr, is mentioned in the trigger loc(s2, j). Hence, the non-null quantifier is guarded by loc(s2, j), and the equation s == (s1, s2) is nested inside.

When asserting that the receiver of loc(unfolding ..., j).v is non-null (for all j), the unfolding introduces a new snapshot pair, and the equality s == (s3, s4), and the prover has to show that loc(s4, j) != null. This requires knowing that s2 == s4, which follows from s == (s3, s4) and s == (s1, s3). However, the second equation is nested under the quantifier guarded by loc(s2, j), and since that trigger is not available, the verification fails.

Workaround

Introduce a function that depends on valid(this) and that performs one of the two unfoldings nested under the quantifier. This function application will be picked as a trigger for the generated quantifiers, and since the function depends on valid(this), the function application snapshot will be s in both quantifiers (the assumed and the one to be asserted), which allows the verification to succeed.

[viper-admin]

@mschwerhoff on 2016-03-27 14:26:

• changed attachment from (none) to 0228.sil

[viper-admin]

@alexanderjsummers commented on 2016-03-27 21:11

This sounds like a fix that should ideally be automated. Maybe we should talk about how that can be done (if a solution isn't clear already - it's not to me).

Could the trigger for the non-nullity assumption be the field lookup itself? i.e. loc(..., j).v in the above? I assume that this non-nullity axiom is generated internally, and so picking the triggers in a routine way (rather than relying on the trigger generation code) would seem better, in any case, if we can find something which works reliably.

[viper-admin]

@mschwerhoff commented on 2016-03-28 11:35

The attached file demonstrates that the problem is unrelated to QPs

[viper-admin]

@mschwerhoff on 2016-03-28 11:35:

• changed attachment from (none) to test23.sil

[viper-admin]

@mschwerhoff on 2016-03-28 11:36:

• changed component from Quantified Permissions to (none)
• edited the title

[viper-admin]

@mschwerhoff commented on 2016-03-28 11:41

See also Carbon issue 124