Error deduplication + NoPosition

[pieter-bos]

I noticed that failures returned from silicon are deduplicated, if I understand correctly with the rendered message as key:

  private def runVerifier(program: ast.Program, cfgs: Seq[SilverCfg]): List[Failure] = {
    val results = verifier.verify(program, cfgs)
    val failures =
      results.flatMap(r => r :: r.previous.toList)
        .collect{ case f: Failure => f } /* Ignore successes */
        .pipe(allResults => {
          allResults.distinctBy(failureFilterAndGroupingCriterion)
        })
        .sortBy(failureSortingCriterion)
  }

(...)

  private def failureFilterAndGroupingCriterion(f: Failure): String = {
    // create a string that identifies the given failure:
    transformedError.readableMessage(withId = true, withPosition = true)
  }

Typically when generating a viper ast from vercors, we generate nodes with pos = NoPosition, since we encode all information relevant to us into info, so this collapses errors that are from our view distinct. For example:

This results in one reported error. Would you maybe think about a different measure of error distinctness, or do you have a good hint on how we might work around this? Thanks!

[mschwerhoff]

In the Voila frontend, I've also regularly lost error messages due to missing positional information (NoPosition), and eventually decided to give each Viper AST node the positional information of the Voila source it corresponds. In contrast (and if I'm not mistaken), Nagini also places all relevant information into the info field, but also sets AST positions to a unique counter value to make sure it always differs.

That said, I'd be totally open to using a different measure — shouldn't even be too hard to allow clients to instantiate Silicon with a custom measure. Could you provide me with Scala (or Java, or pseudo-) code of the kind of measure that you'd like to use?

[pieter-bos]

I think that the failures themselves are already almost the correct measure since they're (all?) case classes, except that the offendingNode is compared structurally, so maybe something like:

class FailureGrouping(err: VerificationError) {
  override def equals(obj: Any): Boolean = obj match {
    case other: VerificationError =>
      (err.offendingNode eq other.offendingNode) && err == other
    case _ => false
  }

  override def hashCode(): Int = err.hashCode()
}

[mschwerhoff]

Comparing offendingNodes by identity is dangerous because the Viper AST is immutable, and front- and backend may perform transformations that result in (structurally) equivalent but non-identical nodes. How about taking info into account? I.e.

def equals(err1: VerificationError, err2: VerificationError): Boolean =
  err1 == err2 && err1.info == err2.info

[pieter-bos]

Yes, I think this is a good way to expose this behaviour to the viper frontends :). I imagine we will need to put a running tally or so into our Info anyway, but this is clearer from an interface standpoint. I guess for viper you also need to consider pos after all?

Probably an ideal measure indicates the place where the offendingNode occurs in the whole ast, for which .pos is a good stand-in for text input. I thought that reference equality would achieve a similar effect, since in our output two instances of assert false in different places are structurally equal but guaranteed non-identical, but I see how that can be fragile in transformations.

Maybe viper placing a running tally in info is a good default?

[mschwerhoff]

You brought up an interesting point: so far, we are not aware of a bullet-proof system that allows to uniquely locate/identify a subtree when equality is structurally defined. Tallies and similar means only achieve this if used consistently, which seems impossible to ensure, at least without severely reducing how ASTs can be created and manipulated.

We could equip some kind of default info (or pos) with a running counter, but it's unclear (to me) how much benefit this would have, since frontends often employ their own instances of the base info and positional traits. But that might be something to discuss during your visit :-)

[mschwerhoff]

I've started implementing what we've discussed: https://github.com/viperproject/silicon/tree/silicon-issue-613. Please take a look and let me know if (1) the new definition of failure equivalence, see class FailureEquivalenceWrapper, suits you, and if (2) overriding protected def failureEquivalenceWrapper in class Silicon is an option for VerCors.