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.