Workaround in error back-translation

[viper-admin]

Created by bitbucket user Wytse Oortwijn on 2020-09-11 08:30

The error back-translation implementation contains a workaround for what I think might be a problem in Silver and/or Silicon. See (not sure how to better link to files/lines in particular commits in Bitbucket):

https://bitbucket.org/Felale/gobra-one/src/e7e58d00b4e831073ac3e495577e8074649d9ac4/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala#lines-121

The reason for this workaround is a bit technical. It appears that Viper internally sometimes negates conditions of if-statements, or generates extra if-statements for user-written if-statements but with the original conditions negated. However, these negations don't seem to preserve any source information, which could lead to stack traces in Gobra. Those particular scenarios are prevented by this workaround, but we eventually want a nicer solution.

[Felalolf]

Here is a client that shows the transformation:

      import viper.silver.{ast => vpr}
      import viper.silicon.Silicon
      import viper.silver.reporter.NoopReporter
      import viper.silver.verifier.{Failure, Success}
      import viper.silver.verifier.{AbstractVerificationError, errors => vprerr, reasons => vprrea}

      val v = vpr.LocalVarDecl("x", vpr.Int)()
      val b = vpr.EqCmp(vpr.Div(v.localVar, vpr.IntLit(0)())(), vpr.IntLit(42)())()
      val p = vpr.Program(
        Seq.empty,
        Seq.empty,
        Seq.empty,
        Seq.empty,
        Seq(vpr.Method(
          "foo",
          Seq(v),
          Seq.empty,
          Seq.empty,
          Seq.empty,
          Some(vpr.Seqn(Seq(vpr.If(b, vpr.Seqn(Seq.empty, Seq.empty)(), vpr.Seqn(Seq.empty, Seq.empty)())()), Seq.empty)())
        )()),
        Seq.empty,
      )()

      val silicon = Silicon.fromPartialCommandLineArguments(Seq.empty, NoopReporter)
      silicon.start()
      val res = silicon.verify(p)
      silicon.stop()

      res match {
        case Failure(Seq(vprerr.IfFailed(offendingNode, _, _))) =>
          print("1: "); println(offendingNode == b) // false
          print("2: "); println(offendingNode == vpr.Not(vpr.EqCmp(vpr.Div(v.localVar, vpr.IntLit(0)())(), vpr.IntLit(42)())())()) // true
          println(offendingNode)
      }

[marcoeilers]

The underlying issue in Viper should be fixed (https://github.com/viperproject/silver/pull/649).