Unclear error reporting on non-static resources in static context

[ArmborstL]

I have a class A containing a resource x. I used that resource successfully within A, e.g. as a requirement for a pure function foo:

//@ public resource x() = true;

//@ requires x();
//@ public pure boolean foo() = true;

I then tried to use it in another class in the contract of a method bar:

//@ requires A.x(); 
//@ requires A.foo();
static void bar() {}

I got "ApplicationPreCondition:AssertionFalse" on the call to foo (i.e. no error reported on A.x()), and "MethodPreConditionUnsound:MethodPreConditionFalse" on the whole method bar.
Looking at the Viper output, it reports that x and foo have the wrong parameter count. In fact, they are defined as non-static, and thus invoking them as A.x() and A.foo() means lacking an implicit this argument. Making them static resolved the issue.
I find the VerCors error messages rather misleading, as they seem to indicate a logical error (such as contradictory conditions) when it is actually a syntactic error. It would be nice if the Viper error message, which is more indicative of the real issue, could be propagated to the user.

[bobismijnnaam]

It seems there are two issues here:

1. Vercors allows non-static functions to be called in a static context (as this is not caught during typechecking)
2. The viper error (which in this case if I understand correctly is that the number of arguments at the call site of foo are plain incorrect) is turned into the methodpreconditionunsound error, which I think comes from the satcheck phase.

The first one is straightforward to fix, the second one I'm not so sure. Altough it is fixed indirectly by not letting unexpected errors propagate to the back-end. It seems that generally a faulty satcheck error indicates some error in the frontend was missed by vercors and caught by viper.

I think this happened a few times before, where some unrelated (syntax?) error in the spec triggered the method spec unsound. Maybe we should investigate if we can implement satcheck differently. One option (probably the most elegant) would be to implement refute viper, so we can implement the satcheck pass properly. If we can convince the viper team to include it in the main viper branch that would also be a good long-term solution.

Related: #469

[ArmborstL]

I agree with most of what you say. However, note that I also get "ApplicationPreCondition:AssertionFalse". So it is not just the satcheck that that has the issue, the "regular" verification also turns the viper error into an unrelated error.
I was thinking that, instead of turning any viper error in the satcheck phase into "method precondition unsound", we only do it for "assert might fail" of the false, and any other viper error is propagated to the user unchanged. I'm not sure if that is a viable option, or if it creates to much noise and confusion for the user :/
Similarly, only the "precondition might not hold" becomes the VerCors precondition error, and things like "predicate arity doesn't match" is propagated unchanged.

[pieter-bos]

Let's keep this issue for the strange error translation, I'll make a new one for the type check part.

[raulmonti]

Bob mentioned that the unsound error is also due to the way we check for preconditions unsoundness, so this issue is actually threefold.

[ArmborstL]

The decided way forward is the following:
If a pass (e.g. the sat check) encounters an unexpected error (e.g. syntax error, or wrong number of arguments), it should propagate that original error, rather than saying "my check failed, so it's unsat" and thereby replacing the error with its own error message and hiding the real issue.
However, the viper error might not be applicable directly (e.g. some transformation occurred and the error refers to something that is not in the original code, like diz). Therefore, the viper error should be wrapped, e.g. "During sat check, an unexpected error occurred in the viper backend: 'unknown argument "diz"'. If you think this is a bug in VerCors, please raise an issue at [...]." That way, users know that it is from the backend and should be treated with a grain of salt, while still getting a (hopefully) more indicative error than if it were reported as "unsat".