Ghost variable not properly handled in loop

[FliegendeWurst]

Description

When using a ghost variable in a loop, KeY assumes it will always have the initial value (value before the loop is executed).

Reproducible

always

Steps to reproduce

File SetGhost.java:

import java.util.List;

public class SetGhost {
    /*@ public normal_behavior
      @ requires \invariant_for(l);
      @ ensures \result == l.seq.length;
      @*/
    static int counter(List l) {
        int listSize = l.size();
        int counter = 0;
        //@ ghost int iter;
        //@ set iter = 0;
        
        /*@ loop_invariant
          @ i >= 0 && i <= listSize && listSize == l.size()
          @  && i == counter
          @  && iter == counter
          @ ;
          @ decreases listSize - i;
          @ assignable counter,iter;
          @*/
        for (int i = 0; i < listSize; i++) {
            counter++;
            //@ set iter = iter + 1;
            //@ assert iter == 1;
            assert counter == 1;
        }
        //@ assert iter == counter;
        return counter;
    }
}

1. Load SetGhost.java
2. Run automode

Expected behavior: the proof does not close, both assertions fail to prove
Actual behavior: proof closes

Reproducer using `\seq` instead of int

In this case, the assertion's validity can be proven, but the loop invariant fails to prove (since KeY thinks values == [l.get(i)] with unknown i).

import java.util.List;

public class SetGhostSeq {
    /*@ public normal_behavior
      @ requires \invariant_for(l);
      @ ensures \result == l.seq.length;
      @*/
    static int counter(List l) {
        int listSize = l.size();
        int counter = 0;
        //@ ghost \seq values;
        //@ set values = \seq_empty;
        
        /*@ loop_invariant
          @ i >= 0 && i <= listSize && listSize == l.size()
          @  && values == l.seq[0 .. values.length]
          @  && i == counter
          @  && \invariant_for(l)
          @ ;
          @ decreases listSize - i;
          @ assignable counter,values;
          @*/
        for (int i = 0; i < listSize; i++) {
            // System.out.println("" + counter);
            counter++;
            Object x = l.get(i);
            //@ set values = \seq_concat(values, \seq_singleton(x));
            //@ assert values.length == 1;
        }
        return counter;
    }
}

Additional information

---

• Commit: 9d0379c (latest main)

cc @WolframPfeifer

[WolframPfeifer]

From the meeting, it looked like a wrong update is generated. Maybe this is related to #3224

[FliegendeWurst]

This bug is really quite severe. For example, here is a little helper method that proves that a provided list is empty. It proves automatically.

import java.util.List;

public class SetGhostFalse {
    /*@ public normal_behaviour
      @ requires \invariant_for(b);
      @ ensures b.size() == 0;
      @ assignable \nothing;
      @*/
    private static void intersectionSize(List b) {
        //@ ghost \seq values;
        //@ set values = \seq_empty;

        /*@ loop_invariant
          @  0 <= i && i <= b.size()
          @  && \invariant_for(b)
          @  && i == values.length
          @ ;
          @ decreasing b.size() - i;
          @ assignable values;
          @*/
        for (int i = 0; i < b.size(); i++) {
            //@ set values = \seq_concat(values, \seq_singleton(42));
        }
    }
}

Meaning it is essentially impossible to use ghost variables in loops without running into this broken behavior.