Make position manager return positions with unique line/column

[simon-hrabec]

This is a fix for an issue that arose in my PR https://github.com/viperproject/prusti-dev/pull/1385

@fpoli suggested solving it by changing how the position manager works.

Now position won't have a collision with line/column values which caused Viper to fail the verification.

[fpoli]

Pinging @Aurel300 since there are counterexamples failing. Should we just update the expected output?

[Aurel300]

It looks like all the failed CE tests are because extra messages were reported with the same exact values at the same positions. Maybe something in the counterexample translations was relying on positions to de-duplicate?

[simon-hrabec]

The tests fail for those 3 tests (mismatch of expected output):

    [ui] ui/counterexamples/ref.rs
    [ui] ui/counterexamples/struct-2.rs
    [ui] ui/counterexamples/union-2.rs

All 3 of those tests have the unsafe_core_proof flag set to true. In the process_entries function in prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs the difference is generated in the variables block by allowing more counterexamples to surface.

It comes from the create_mapping function in prusti-viper/src/encoder/counterexamples/mapping.rs, where "duplicities" are filtered based on identical row/column from the position struct. By making all position data unique no data is filtered out.

I am unfamiliar with counterexamples code and not sure what qualifies as a duplicate, but it seems they differ. for example:

  --> prusti-tests/tests/verify_overflow/ui/counterexamples/union-2.rs:21:5
   |
21 |     maybe.value.1 = 2;
   |     ^^^^^^^^^^^^^^^^^
note: counterexample for \"maybe\"
       value:   MaybeUninit {
            value: (
                1,
                2,
            ),
        }

with

  --> prusti-tests/tests/verify_overflow/ui/counterexamples/union-2.rs:21:5
   |
21 |     maybe.value.1 = 2;
   |     ^^^^^^^^^^^^^^^^^
note: counterexample for \"value\"
       value:   (
            1,
            2,
        )

seems to point to a slightly different thing.

Similarly

  --> prusti-tests/tests/verify_overflow/ui/counterexamples/union-2.rs:20:5
   |
20 |     maybe.value.0 = 1;
   |     ^^^^^^^^^^^^^^^^^
note: counterexample for \"maybe\"
       value:   MaybeUninit {
            value: (
                1,
                ?,
            ),
        }

with

  --> prusti-tests/tests/verify_overflow/ui/counterexamples/union-2.rs:20:5
   |
20 |     maybe.value.0 = 1;
   |     ^^^^^^^^^^^^^^^^^
note: counterexample for \"maybe\"
       value:   MaybeUninit {
            value: (
                1,
                2,
            ),
        }

If those should be skipped I think the same comparison could be made using the available spans. I am overall not sure I understand the role of the Position struct in Prusti/viper.

[fpoli]

Who wants to take this PR?

[fpoli]

Who wants to take this PR?

Vytautas said @Aurel300 :smile:

[fpoli]

Closing in favor of #1418.