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 functions unrelated to local variables? For example foo(3) == 42 here?

[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?