viperproject / gobra

Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
https://gobra.ethz.ch
Other
111 stars 28 forks source link

Improves Error Messages for Assignments #746

Closed Felalolf closed 7 months ago

Felalolf commented 7 months ago

Check #745 for an example. As shown by the added file, the error messages are not perfect:

The following snippet causes an assignment error,

var @x, y int
exhale acc(&x)
y = x

whereas the next snippet causes a load error,

var @x, y [5]int
exhale acc(&x)
y = x

The issue is caused by how Viper reports errors. The first snippets encodes to a field access whereas the second snippets encodes to a call. The call error is swapped with a load error. The field access error is a reason and not an error, so it cannot be swapped easily.

Solutions are:

Both solutions have drawbacks. The call encoding adds more complexity, which from my experience scales poorely for expressions that are all over the place. Overwriting reasons is rather error prone. Consider the encoding of x = y, which encodes x the same as y = x. If we overwrite errors, either both cause the same error message, i.e. a read/load error, or we need to remove the overwriting reasons somehow in one of the cases.

Long story short, in my opinion, the changes described above are not worth it. If we want these improvement, I am in favor of merging this PR and creating a new issue.