Comprehensive backend-independent counterexamples

[marcoeilers]

This PR introduces a shared, backend-independent counterexample format in Silver, produced by both Silicon and Carbon. A counterexample is built in two layers:

• Raw (RawCounterexample): the information collected from the backend model in a simple form, with heap resources still identified by backend-internal (SMT) identifiers.
• Resolved (ResolvedCounterexample): the human-readable form; heap resources are bound to their AST nodes (fields, predicates, magic wands) and values are ordinary Viper AST expressions.

Values are represented as normal Viper AST expressions (ast.Exp). The two new AST nodes RefLit (a concrete reference) and BackendValueLit (an otherwise opaque backend value) cover things that have no ordinary Viper syntax.

Select the layer on the command line: --counterexample resolved (or raw). Silicon additionally requires --exhaleMode 1.

Example:

field f: Int
predicate P(this: Ref)

method m(x: Ref, s: Seq[Int])
  requires acc(x.f, 1/2) && acc(P(x))
  requires x.f == 3
  requires s == Seq(10, 20)
{
  assert x.f == s[0]   // fails: 3 != 10
}

The resolved counterexample shown to the user:

   Store:
Variable Name: s, Value: Seq(10, 20), Type: Seq[Int]
Variable Name: x, Value: $Ref!val!0, Type: Ref
   current Heap:
Field Entry: $Ref!val!0.f --> (Value: 3, Type: Int, Perm: 1/2)
Predicate Entry: P($Ref!val!0) --> (Perm: 1/1)
   old Heap:
Field Entry: $Ref!val!0.f --> (Value: 3, Type: Int, Perm: 1/2)
Predicate Entry: P($Ref!val!0) --> (Perm: 1/1)

• Store: each in-scope variable with its value. Collections are reconstructed as literals (Seq(10, #undefined), Set(1, 2, 3), Multiset(7, 7, 8), Map(1 := 100)); #undefined marks an entry the model does not pin down.
• Heap: the resources held, with their permission amounts (e.g. 1/2). Both the current heap (at the failing point) and the old heap (method entry) are shown; frontends can drop the old heap when it isn't of interest.

Other resource kinds render analogously; a magic wand appears as the wand itself, e.g. Magic Wand Entry: acc(x.f, 1/2) --* acc(x.f, 1/1) (Perm: 1/1), and (domain) function values are listed under a separate section, e.g.

domain Ma{
 fn2(Int):Int{
    4 -> 8
    else -> #unspecified
}
}
fn(Ref):Int{
    Heap@0 x -> 4
    else -> #unspecified
}

The same format is emitted by both Silicon and Carbon, so the two agree modulo backend-internal reference names ($Ref!val!0 vs T@U!val!0).

This is the result of @rvandoren's practical work project, with a bunch of additions from me.

[Aurel300]

Is this really testing anything counterexample-related to magic wands? It seems this just does the usual permission accounting and then provides a counterexample related to the permisison on L18.

[Aurel300]

For this, sets.vpr, and multisets.vpr, would this not work equally "well" for any domain? I would expect maps.vpr to have something specific to maps, not just general equality. sequences.vpr seems better, for example.

[Aurel300]

Can we also report (and test for) values of fields in folded predicates?

[Aurel300]

But the frontend accepts five different values for the counterexample kind. Are the other three not processed here?

[Copilot]

Pull request overview

This PR adds a shared, backend-independent counterexample representation (raw + resolved) and wires it into the Silver frontend/AST so both Silicon and Carbon can emit a common counterexample format, with new tests to validate reported store/heap values and permissions.

Changes:

• Introduces new counterexample data model (RawCounterexample / ResolvedCounterexample) and value parsing utilities, plus a permission Rational.
• Extends the Viper AST and pretty-printer with counterexample-only literals (RefLit, BackendValueLit) and updates magic-wand structure generation to support unique placeholder names.
• Adds expected-counterexample test annotations and a large set of .vpr regression tests covering values, permissions, collections, quantified permissions, predicates, and magic wands.

Reviewed changes

Copilot reviewed 33 out of 33 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
src/main/scala/viper/silver/verifier/Counterexample.scala	New backend-independent counterexample model types + value/permission parsing utilities.
src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala	Adds `--counterexample raw
src/main/scala/viper/silver/ast/Expression.scala	Adds counterexample-only literal nodes; updates magic-wand structure generation (optional unique naming).
src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala	Pretty-prints new counterexample literal nodes.
src/main/scala/viper/silver/testing/BackendTypeTest.scala	Adds MPL header/copyright header.
src/test/scala/ExpectedCounterexampleAnnotation.scala	New annotation + parser to assert expected resolved counterexample content in tests.
src/test/scala/CounterexampleVariablesTests.scala	Removes duplicated parser/model definitions (now shared via new test file).
src/test/resources/counterexample_mapped/simple-refs.vpr	New mapped counterexample test for reference field values.
src/test/resources/counterexample_mapped/simple-refs-rec.vpr	New mapped counterexample test for locals/returns with refs.
src/test/resources/counterexample_mapped/sequence.vpr	New mapped counterexample test for sequence updates/element equality.
src/test/resources/counterexample_mapped/ref-sequence.vpr	New mapped counterexample test for sequence field lookup on refs.
src/test/resources/counterexample_mapped/predicate.vpr	New mapped counterexample test for predicate unfolding/field values.
src/test/resources/counterexample_mapped/permissions.vpr	New mapped counterexample test for insufficient permission assignments.
src/test/resources/counterexample_mapped/negative.vpr	New mapped counterexample test for negative integer values.
src/test/resources/counterexample_mapped/method-call.vpr	New mapped counterexample test for call precondition failures.
src/test/resources/counterexample_mapped/lseg.vpr	New mapped counterexample test for list-segment unfolding/permissions.
src/test/resources/counterexample_mapped/functions.vpr	New mapped counterexample test for function applications in counterexamples.
src/test/resources/counterexample_mapped/cyclic-ref.vpr	New mapped counterexample test for cyclic reference structures.
src/test/resources/counterexample_general/two_qp_same_field.vpr	New general test for summed quantified permissions on the same location.
src/test/resources/counterexample_general/sets.vpr	New general test for set value equality reporting.
src/test/resources/counterexample_general/sequences.vpr	New general tests for sequence element-wise reporting (incl. negatives).
src/test/resources/counterexample_general/qpred.vpr	New general test for quantified predicate permissions from multiple sources.
src/test/resources/counterexample_general/qfield.vpr	New general test for quantified field values reported at specific receivers.
src/test/resources/counterexample_general/predicate_permissions.vpr	New general tests for predicate permission amounts (non-QP).
src/test/resources/counterexample_general/predicate_permissions_qp.vpr	New general tests for predicate permission amounts under quantified permissions.
src/test/resources/counterexample_general/multisets.vpr	New general test for multiset value equality reporting.
src/test/resources/counterexample_general/maps.vpr	New general test for map value equality reporting.
src/test/resources/counterexample_general/magic_wands.vpr	New general test validating counterexamples after applying magic wands.
src/test/resources/counterexample_general/local_values.vpr	New general tests for local/param values (ints, negatives, refs, reassignment).
src/test/resources/counterexample_general/field_values.vpr	New general tests for field values on one/two objects and multiple fields.
src/test/resources/counterexample_general/field_values_qp.vpr	New general tests for field values under quantified permissions (set/seq/indexed).
src/test/resources/counterexample_general/field_permissions.vpr	New general tests for fractional field permission reporting (non-QP).
src/test/resources/counterexample_general/field_permissions_qp.vpr	New general tests for fractional field permission reporting under various QP forms.

Suppressed comments (1)

src/main/scala/viper/silver/verifier/Counterexample.scala:211

• Same issue here: map(...)mkString(...) is missing a . before mkString, which will fail compilation. Add .mkString(...).

    het match {
      case PredicateType =>
        s"Heap entry: ${reference.mkString("(", ", ", ")")} + ${field.mkString("(", ", ", ")")} --> (Permission: ${perm.getOrElse("None")}) ${if (insidePredicate.isDefined && !insidePredicate.get.isEmpty) insidePredicate.get.toSeq.map(x => s"${x._1} --> ${x._2}")mkString("{\n   ", "\n   ", "\n}") else ""}"
      case _ => s"Heap entry: ${reference.mkString("(", ", ", ")")} + ${field.mkString("(", ", ", ")")} --> (Value: $valueID, Permission: ${perm.getOrElse("None")})"

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.