When is the Position of an AST node mandatory?

[fpoli]

In Prusti, we only generate Position instances (with a unique line, column and ID) for the AST nodes that we know might be the offending node of a verification error. Sometimes, we also generate positions for the AST nodes that we know might be the reason of a verification error. For any other AST node we generate a dummy position where the line and column are zero.

This worked well so far when using Silicon configured to report one verification error per method. However, when we configure Silicon to report multiple verification errors we still only receive one verification error per method. Aurel found that by removing .distinctBy(failureFilterAndGroupingCriterion) we actually get all the errors that we expect, but I then wonder why the deduplication is there in the first place.

I have a few questions about this:

• What are the AST nodes from which Silicon takes the position used to deduplicate verification errors?
• In general, what is the minimum set of AST nodes for which a frontend should generate unique positions?
• Why is there a deduplication of verification errors in Silicon? Is it perhaps no longer needed?

[marcoeilers]

• Why is there a deduplication of verification errors in Silicon? Is it perhaps no longer needed?

My guess would be that deduplication is used because you're likely to get the exact same error on multiple paths (because you reach e.g. the same assert statement that fails on different paths).

• What are the AST nodes from which Silicon takes the position used to deduplicate verification errors?

It seems to be the position that would be reported for the error, which as far as I can see is always the position of the offendingNode. What AST node is used for that will depend on the type of error, so that question doesn't have a short answer.

• In general, what is the minimum set of AST nodes for which a frontend should generate unique positions?

I don't think that question has an answer. Silicon works (as in, doesn't crash or do anything unsound) without unique positions, as you see, it just filters out all errors that would have the same exact error message.
Obviously we could add a switch to disable error deduplication (that seems to make a lot of sense in general) or somehow make error deduplication more configurable.

What I don't understand is this:
If your errors are filtered out, then that must mean that they have the same position, so the offendingNodes must have the same position, which suggests that actually they don't have unique positions (or at least the string version of the positions is not unique).

[fpoli]

If your errors are filtered out, then that must mean that they have the same position, so the offendingNodes must have the same position, which suggests that actually they don't have unique positions (or at least the string version of the positions is not unique).

Yes, which means that we are generating dummy positions for AST nodes for which we should instead generate unique positions. Knowing that those are the offendingNodes helps, thanks!

Last question, then we can close:

• Are positions with the same line number but different IDs considered different? From the distinctBy that I linked it seems yes, but we noticed that the behavior of Silicon changes if we also make the line number unique instead of just the ID. To be precise, we get duplicate counterexamples when we make the line numbers unique (Make position manager return positions with unique line/column prusti-dev#1389).

[marcoeilers]

My impression was that the important thing is that position.toString() is unique. So if the string representation contains line, column, and ID, then making any of those unique would suffice. But I guess the ID is something Prusti-specific? I think that's not a part of a standard Viper position. So I don't know what the implementation of toString for your Position class does.

[fpoli]

Are you sure that it's the toString of a position that is used to deduplicate the errors? I thought that failureFilterAndGroupingCriterion, by calling readableMessage(withId = true, withPosition = true), always uses the implementation at AbstractVerificationError::readableMessage, which should always take into account the ID.

All positions constructed by Prusti are instances of Silver's IdentifierPosition; by ID I always mean that identifier. I now notice that IdentifierPosition does not override the toString defined in HasLineColumn, so the resulting string does not depend on the ID stored in IdentifierPosition. However, I think that this does not affect the deduplication.

[marcoeilers]

I assumed withId referred to the ID of the type of error, e.g., assert.failed:insufficient.permission. Since positions in general don't have an ID.

[fpoli]

Oooh, you mean that withId in readableMessage(withId = true, withPosition = true) refers to the "assert.failed:insufficient.permission" ID and not to the ID of IdentifierPosition instances. That explains a lot of weird things!