Method Calls in Loops

[DavePearce]

(@utting @leavens keeping you in the loop)

The following program generates a strange error message indeed:

method g(&int p) -> (int r):
    return 0

method f(&int p, int[] xs):
    //
    for i in 0..|xs|:
        g(p)

UPDATE: this is related to debug=true in the wy.toml file.

[DavePearce]

Summary:

• When debug=true this example doesn't verify because of a generated loop invariant involving HEAP for p
• Since the loop invariant was generated, there is no source information --- hence why the error is wierd.

But why doesn't it fail when debug=false ?

[DavePearce]

When debug=true loop invariant is:

   invariant (forall r:Ref :: Ref#within(HEAP$173,r,p) || (HEAP$173[r] == Void) || (HEAP$173[r] == HEAP[r]));

When debug=false we have:

   invariant (forall r:Ref :: Ref#within(HEAP$173,r,p$78) || (HEAP$173[r] == Void) || (HEAP$173[r] == HEAP[r]));

Hmmm that's not it

[DavePearce]

Ok, here we go:

When debug=true we have this for g():

free ensures (forall p:Ref :: Ref#within(old(HEAP),p,p) || ...);

When debug=false we have this:

free ensures (forall p:Ref :: Ref#within(old(HEAP),p,p$23) || ...);

These are not equivalent.

[utting]

In the earlier version of the translator to Boogie, I used a weaker version of this 'debug' name mapping, maintained a map from each fully qualified name to its 'printable' name.

For example, for a base name of 'p', the first printable name would be just 'p', then other fully qualified variants of it would be mapped to 'p1', 'p2', etc. (a separate counter for each base name). This allows the most common cases (identifiers that appear only once) to retain their original names, but it still disambiguates other names when needed, with a short and readable name.

(One could make this even more sophisticated by taking detailed scopes into consideration, but a simple version that has just two levels of scope, global and local, would work pretty well I think).

[DavePearce]

Hey,

In general, expressions are already associated with a unique identifier and I typically use this. Not sure what's going wrong here. Its not a ideal, but not a big drama now I know the problem.