Reporting multiple errors

[fpoli]

I determined that to report multiple verification errors in the same method Silicon does not only require the position of the offending node of the error to be set, but also the position of the reason node. The following test, for example, fails if pos_1b and pos_2b are NoPosition.

@Aurel300 This is why we don't get multiple errors in Prusti: we do not always generate positions for sub-expressions, even though we always generate positions for the offending nodes (e.g. the assert statements).

Source code

// This Source Code Form is subject to the terms of the Mozilla Public
// License, v. 2.0. If a copy of the MPL was not distributed with this
// file, You can obtain one at http://mozilla.org/MPL/2.0/.
//
// Copyright (c) 2011-2023 ETH Zurich.

import org.scalatest.funsuite.AnyFunSuite
import viper.silicon.Silicon
import viper.silver.ast.{Assert, EqCmp, HasLineColumn, Int, IntLit, LineColumnPosition, LocalVar, LocalVarAssign, LocalVarDecl, Method, Program, Seqn}
import viper.silver.reporter.NoopReporter
import viper.silver.verifier.errors.AssertFailed
import viper.silver.verifier.{Failure, Success}

class SiliconMultipleErrorsTests extends AnyFunSuite {
  val silicon: Silicon = {
    val reporter = NoopReporter
    val debugInfo = ("startedBy" -> "SiliconMultipleErrorsTests") :: Nil
    new Silicon(reporter, debugInfo)
  }
  silicon.parseCommandLine(Seq("--numberOfErrorsToReport=0", "dummy.vpr"))
  silicon.start()

  test("Multiple error messages are reported") {
    val xDecl = LocalVarDecl("x", Int)()
    val x = LocalVar("x", Int)()
    val vDecl = LocalVarDecl("v", Int)()
    val v = LocalVar("v", Int)()

    val pos_1 = LineColumnPosition(100, 0)
    val pos_1b = LineColumnPosition(101, 0) // or, NoPosition
    val pos_2 = LineColumnPosition(200, 0)
    val pos_2b = LineColumnPosition(202, 0) // or, NoPosition

    val assert_1 = Assert(EqCmp(x, IntLit(0)())(pos_1b))(pos_1)
    val havoc = LocalVarAssign(x, v)()
    val assert_2 = Assert(EqCmp(x, IntLit(0)())(pos_2b))(pos_2)
    val body = Seqn(Seq(assert_1, havoc, assert_2), Seq(xDecl))()
    val method = Method("foo", Seq(vDecl), Seq(), Seq(), Seq(), Some(body))()
    val program = Program(Seq(), Seq(), Seq(), Seq(), Seq(method), Seq())()

    val verificationResult = silicon.verify(program)
    verificationResult match {
      case Success => assert(false)
      case Failure(errors) =>
        assert(errors.length == 2)

        // Check the position of the offending node of the first error
        errors(0) match {
          case AssertFailed(offending, _reason, _cached) =>
            val pos = offending.pos
            pos match {
              case posWithId: HasLineColumn =>
                assert(posWithId.line == 100)
                assert(posWithId.column == 0)
              case _ => assert(false)
            }
          case _ => assert(false)
        }

        // Check the position of the offending node of the second error
        errors(1) match {
          case AssertFailed(offending, _reason, _cached) =>
            val pos = offending.pos
            pos match {
              case posWithId: HasLineColumn =>
                assert(posWithId.line == 200)
                assert(posWithId.column == 0)
              case _ => assert(false)
            }
          case _ => assert(false)
        }
    }
  }
}

Is this intentional or is this a bug? Would it be hard to lift this requirement? As far I can observe, Carbon does not have a similar requirement, nor Silicon when configured to report one error per function.

(This is a follow-up of #732.)

[marcoeilers]

I don't agree that this is "a requirement", it's a consequence of how the filtering and the position reporting works. So if we want to change this "requirement", we'd have to change the filtering or the position reporting.

• Silicon filters errors whose message is identical (because it is likely to get the same error on multiple paths). Again, we could easily give you an option to disable this filtering from a frontend; then you'd have to get rid of the duplicates yourself. For command line usage, I think filtering based on the message makes perfect sense, since the user gains nothing from seeing two completely identical error messages.
• For failing assert statements (and similarly for exhale and inhale), the reported position is that of the asserted expression (i.e., it's override def pos = offendingNode.exp.pos, not that of the reason in general). This is determined in Silver, and I assume it's done for subjectively slightly nicer error reporting. We could also discuss whether this is what we want, but this isn't a question of error deduplication.

[fpoli]

Well, "requirement" is empirical because there is no documentation for users of the public AST interface. I now understand the steps that lead to the missing verification errors, but overall it doesn't sound like something that we want Viper users to deal with (i.e. looking up how Viper internally generates error messages to understand in which cases the position should be set).

The closest thing to a bug is that for failing assert statements Silver replaces the good position of the offending node with the bad NoPosition taken from the expression. I'd say we should either fix that, or we should decide that positions for such expressions are mandatory, adding a consistency check for those (and more?) cases. Now that I think about it, a consistency check enforcing that all statements that might fail have a position might be useful independently from this issue.

[marcoeilers]

The closest thing to a bug is that for failing assert statements Silver replaces the good position of the offending node with the bad NoPosition taken from the expression. I'd say we should either fix that, or we should decide that positions for such expressions are mandatory, adding a consistency check for those (and more?) cases. Now that I think about it, a consistency check enforcing that all statements that might fail have a position might be useful independently from this issue.

I disagree with both points.
Error positions should be the ones that best highlight where the error happens. This is a matter of taste I guess, but I think it's completely reasonable that the position of a failing assertion error is the position of the expression that may not be true.
I strongly disagree with making positions mandatory. Everything in Viper works fine with arbitrary position objects (including NoPosition). Forbidding NoPosition for specific nodes because those can cause a specific problem for a specific backend with a specific rarely-used command line option seems like a huge overreaction to me.

Again, why not just disable the deduplication when used from API? I think deduplication makes sense for command line usage, but clearly not always for API usage. IMO the problem really has nothing to do with the positions Viper reports for error messages or expectations about positions. We're just always doing a deduplication that makes sense for command line usage but may not make sense for other use cases. Let's disable it for those then.

[fpoli]

So you are saying that when frontends use --numberOfErrorsToReport they should also use a new --disableErrorFiltering, otherwise good luck to them. I'm fine with that.

[marcoeilers]

Either that or maybe we could move the deduplication to the point where errors are reported to stdout, so that it's never used from the API in the first place?