scala.MatchError: Quantified resource might not be injective

[JLedelay]

The following input:

class C {
  /*@
  requires arr != null;
  requires Value(arr[*]);
  requires (\forall* int k = 0 .. arr.length; Value(arr[k].arr[*]));
  pure int mySum2(D[] arr) = 0;

  requires arr != null;
  requires Value(arr[*]);
  requires (\forall int k = 0 .. arr.length; arr[k].arr != null);
  pure int mySum(D[] arr) = mySum2(arr);
  @*/
}

class D {
  final int[] arr;
}

Gives the following output:

[ERROR] Unrecoverable error: Quantified resource aloc(opt_get1(arr(aloc(opt_get1(arr1), k).ref)), i).int might not be injective. (of class viper.silver.verifier.reasons$QPAssertionNotInjective)
scala.MatchError: Quantified resource aloc(opt_get1(arr(aloc(opt_get1(arr1), k).ref)), i).int might not be injective. (of class viper.silver.verifier.reasons$QPAssertionNotInjective)
        at viper.api.backend.SilverBackend.getFailure(SilverBackend.scala:279)
        at viper.api.backend.SilverBackend.getFailure$(SilverBackend.scala:279)
        at viper.api.backend.silicon.Silicon.getFailure(Silicon.scala:41)
        at viper.api.backend.SilverBackend.processError(SilverBackend.scala:143)
        at viper.api.backend.SilverBackend.processError$(SilverBackend.scala:118)
        at viper.api.backend.silicon.Silicon.processError(Silicon.scala:41)
        at viper.api.backend.SilverBackend.$anonfun$submit$9(SilverBackend.scala:108)
        at viper.api.backend.SilverBackend.$anonfun$submit$9$adapted(SilverBackend.scala:108)
        at scala.collection.immutable.List.foreach(List.scala:333)
        at viper.api.backend.SilverBackend.submit(SilverBackend.scala:108)
        at viper.api.backend.SilverBackend.submit$(SilverBackend.scala:59)
        at viper.api.backend.silicon.Silicon.submit(Silicon.scala:41)
        at vct.main.stages.SilverBackend.verify(Backend.scala:115)
        ...
Exception in thread "main" scala.MatchError: Quantified resource aloc(opt_get1(arr(aloc(opt_get1(arr1), k).ref)), i).int might not be injective. (of class viper.silver.verifier.reasons$QPAssertionNotInjective)
        at viper.api.backend.SilverBackend.getFailure(SilverBackend.scala:279)
        at viper.api.backend.SilverBackend.getFailure$(SilverBackend.scala:279)
        at viper.api.backend.silicon.Silicon.getFailure(Silicon.scala:41)
        at viper.api.backend.SilverBackend.processError(SilverBackend.scala:143)
        at viper.api.backend.SilverBackend.processError$(SilverBackend.scala:118)
        at viper.api.backend.silicon.Silicon.processError(Silicon.scala:41)
        at viper.api.backend.SilverBackend.$anonfun$submit$9(SilverBackend.scala:108)
        at viper.api.backend.SilverBackend.$anonfun$submit$9$adapted(SilverBackend.scala:108)
        at scala.collection.immutable.List.foreach(List.scala:333)
        at viper.api.backend.SilverBackend.submit(SilverBackend.scala:108)
        at viper.api.backend.SilverBackend.submit$(SilverBackend.scala:59)
        at viper.api.backend.silicon.Silicon.submit(Silicon.scala:41)
        at vct.main.stages.SilverBackend.verify(Backend.scala:115)
        ...

[ArmborstL]

Viper requires that all forall with permission expressions (forall* in VerCors) are injective. That means that different k must point to different heap chunks. For you concretely, that means that for i != j, you must have arr[i] != arr[j]. And also that arr[i].arr != arr[j].arr (since D.arr is a reference, so they might otherwise all point to the same inner array). With that (and some additional null-checks), you should be able to get your program to verify.

However, we should work on the error reporting there. VerCors should not crash, and instead gracefully terminate and report what the issue is.

[pieter-bos]

The problem is as such:

• VerCors makes a distinction between errors that are a well-formedness problem (such as division by zero, having insufficient permission for a dereference) and errors that indicate an assertion is falsey (such as asserting false, or Perm that you don't have).
• Typically a well-formedness problem is reported multiple times: at the definition, and at usages of the malformed definition. In such cases the error is de-duplicated.
• Less typically, at the usage site we could make more progress than at the definition, because we have local knowledge that makes the otherwise ill-framed expression evaluate normally.
• If the error is different as above, the error is reported in both places. VerCors does not know what to do with error reasons that are a well-formedness problem in positions where it expects a falsey reason (here: the precondition is false, because the location is not injective (??))

Here mySum2 does not verify because the contract is not well-formed: arr[k].arr may be null. At the usage in mySum we know that this is not the case, and instead we get stuck on the fact that arr[k].arr[_] might not be injective: the error viper reports is "the precondition of mySum2 might be false, since arr[k].arr[_] might not be injective."