Comprehensive backend-independent counterexamples

src/main/scala/viper/silver/ast/Expression.scala

@@ -163,7 +163,7 @@ case class MagicWand(left: Exp, right: Exp)(val pos: Position = NoPosition, val
     collectedExpressions
   }
 
-  def structure(p: Program): MagicWandStructure = {
+  def structure(p: Program, uniqueNames: Boolean = false): MagicWandStructure = {
     /* High-level idea: take the input wand (`this`) and perform a sequence of
      * substitutions that transform the wand into a canonical form suitable for
      * checking whether or not a given state provides a particular wand.
@@ -208,10 +208,12 @@ case class MagicWand(left: Exp, right: Exp)(val pos: Position = NoPosition, val
         decl.copy(name(decl.typ, bindings(decl.name)))(decl.pos, decl.info, decl.errT))
     }
 
+    var uniqueNameIndex = -1
     val structure = StrategyBuilder.Context[Node, Bindings](
       {
         case (exp: Exp, c) if subexpressionsToEvaluate.contains(exp) =>
-          (LocalVar(exp.typ.toString(),exp.typ)(), c)
+          val varName = exp.typ.toString() + (if (uniqueNames) s"${uniqueNameIndex += 1; uniqueNameIndex}" else "")
+          (LocalVar(varName, exp.typ)(), c)
 
         case (quant: QuantifiedExp, context) =>
           /* NOTE: This case, i.e. the transformation case, is reached before the

src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala

@@ -114,6 +114,8 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     case "native" => NativeModel
     case "variables" => VariablesModel
     case "mapped" => MappedModel
+    case "extended" => ExtendedModel
+    case "intermediate" => IntermediateModel
     case i => throw new IllegalArgumentException(s"Unsupported counterexample model provided. Expected 'native', 'variables' or 'mapped' but got $i")
   }))
 
@@ -203,3 +205,5 @@ trait CounterexampleModel
 case object NativeModel extends CounterexampleModel
 case object VariablesModel extends CounterexampleModel
 case object MappedModel extends CounterexampleModel
+case object IntermediateModel extends CounterexampleModel
+case object ExtendedModel extends CounterexampleModel

src/main/scala/viper/silver/testing/BackendTypeTest.scala

@@ -1,3 +1,9 @@
+// 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-2015 ETH Zurich.
+
 package viper.silver.testing
 
 import org.scalatest.funsuite.AnyFunSuite

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

@@ -0,0 +1,222 @@
+package viper.silver.verifier
+import viper.silver.ast
+import viper.silver.ast.{AbstractLocalVar, Exp, Type, Resource}
+
+/**
+  * Classes used for to build "intermediate" and "extended" counterexamples.
+  */
+
+trait IntermediateCounterexample {
+  val basicVariables: Seq[CEVariable]
+  val allSequences: Seq[CEValue]
+  val allSets: Seq[CEValue]
+  val allMultisets: Seq[CEValue]
+  lazy val allCollections: Seq[CEValue] = allSequences ++ allSets ++ allMultisets
+  def allBasicHeaps: Seq[(String, BasicHeap)]
+
+  val domainEntries: Seq[BasicDomainEntry]
+  val nonDomainFunctions: Seq[BasicFunctionEntry]
+}
+
+trait ExtendedCounterexample {
+  val imCE: IntermediateCounterexample
+  val ceStore: StoreCounterexample
+  val ceHeaps: Seq[(String, HeapCounterexample)]
+  lazy val heapMap = ceHeaps.toMap
+  val domainEntries: Seq[BasicDomainEntry]
+  val functionEntries: Seq[BasicFunctionEntry]
+  lazy val domainsAndFunctions = domainEntries ++ functionEntries
+}
+
+case class StoreCounterexample(storeEntries: Seq[StoreEntry]) {
+  override lazy val toString = storeEntries.map(x => x.toString).mkString("", "\n", "\n")
+  lazy val asMap: Map[String, CEValue] = storeEntries.map(se => (se.id.name, se.entry)).toMap
+}
+
+case class StoreEntry(id: AbstractLocalVar, entry: CEValue) {
+  override lazy val toString = {
+    entry match {
+      case CEVariable(_, _, _) => s"Variable Name: ${id.name}, Value: ${entry.value.toString}, Type: ${id.typ.toString}"
+      case CESequence(name, length, entries, sequence, memberTypes) => s"Collection variable \"${id.name}\" of type ${id.typ.toString} with ${length} entries:${entries.map { case (k, v) => s"\n $v at index ${k.toString()}" }.mkString}"
+      case CESet(name, length, entries, sequence, memberTypes) => s"Collection variable \"${id.name}\" of type ${id.typ.toString} with ${length} entries:${entries.map { case (k, true) => s"\n $k" }.mkString}"
+      case CEMultiset(name, length, entries, memberTypes) => s"Collection variable \"${id.name}\" of type ${id.typ.toString} with ${length} entries:${entries.foreach { case (k, v) => s"\n ${v.toString} at index $k" }}"
+    }
+  }
+}
+
+case class HeapCounterexample(heapEntries: Seq[(Resource, FinalHeapEntry)]) {
+  var finalString = ""
+  var containsQP = false
+  heapEntries.foreach { case (re,he) => if (he.entryType == QPFieldType || he.entryType == QPPredicateType || he.entryType == QPMagicWandType) containsQP = true}
+  if (containsQP)
+    finalString ++= "The heap contains quantified permissions. Thus, we might own some permissions which are not shown in the counterexample.\n"
+  heapEntries.foreach { se => finalString ++= se._2.toString ++ "\n" }
+  override lazy val toString = finalString
+}
+
+sealed trait FinalHeapEntry {
+  val entryType : HeapEntryType
+}
+
+case class FieldFinalEntry(ref: String, field: String, entry: CEValue, perm: Option[Rational], typ: Type, het: HeapEntryType) extends FinalHeapEntry {
+  val entryType = het
+  override lazy val toString = s"Field Entry: $ref.$field --> (Value: ${entry.value.toString}, Type: ${typ}, Perm: ${perm.getOrElse("#undefined").toString})"
+}
+
+case class PredFinalEntry(name: String, args: Seq[String], perm: Option[Rational], insidePredicate: Option[scala.collection.immutable.Map[Exp, ModelEntry]], het: HeapEntryType) extends FinalHeapEntry {
+  val entryType = het
+  override lazy val toString = s"Predicate Entry: $name(${args.mkString("", ", ", ")")} --> (Perm: ${perm.getOrElse("#undefined").toString}) ${if (insidePredicate.isDefined && !insidePredicate.get.isEmpty) insidePredicate.get.toSeq.map(x => s"${x._1} --> ${x._2}")mkString("{\n   ", "\n   ", "\n}") else ""}"
+}
+
+case class WandFinalEntry(name: String, left: Exp, right: Exp, args: Map[String, String], perm: Option[Rational], het: HeapEntryType) extends FinalHeapEntry {
+  val entryType = het
+  override lazy val toString = s"Magic Wand Entry: $name --> (Left: ${left.toString}, Right: ${right.toString}, Perm: ${perm.getOrElse("#undefined").toString})"
+}
+
+sealed trait CEValue {
+  val id : String
+  val value : Any
+  val valueType : Option[ast.Type]
+}
+
+object CEValueOnly {
+  def apply(value: ModelEntry, typ: Option[ast.Type]): CEValue = CEVariable("#undefined", value, typ)
+  def unapply(ce: CEValue): Option[(ModelEntry, Option[ast.Type])] = ce match {
+    case CEVariable(_, entryValue, typ) => Some((entryValue, typ))
+    case _ => None
+  }
+}
+
+case class CEVariable(name: String, entryValue: ModelEntry, typ: Option[Type]) extends CEValue {
+  val id = name
+  val value = entryValue
+  val valueType = typ
+  override lazy val toString = s"Variable Name: ${name}, Value: ${value.toString}, Type: ${typ.getOrElse("None").toString}"
+}
+
+case class CESequence(name: String, length: BigInt, entries: Map[BigInt, String], sequence: Seq[String], memberTypes: Option[Type]) extends CEValue {
+  val id = name
+  val value = sequence
+  val valueType = memberTypes
+  val size = length
+  val inside = entries
+  override lazy val toString = {
+    var finalString = s"$name with size ${size.toString()} with entries:"
+    for ((k,v) <- inside)
+      finalString ++= s"\n $v at index ${k.toString()}"
+    finalString
+  }
+}
+
+case class CESet(name: String, cardinality: BigInt, containment: Map[String, Boolean], set: Set[String], memberTypes: Option[Type]) extends CEValue {
+  val id = name
+  val value = set
+  val valueType = memberTypes
+  val size = cardinality
+  val inside = containment
+  override lazy val toString = s"Set $name of size ${size.toString()} with entries: ${inside.filter(x => x._2).map(x => x._1).mkString("{", ", ", "}")}"
+}
+
+case class CEMultiset(name: String, cardinality: BigInt, containment: scala.collection.immutable.Map[String, Int], memberTypes: Option[Type]) extends CEValue {
+  val id = name
+  val value = containment
+  val valueType = memberTypes
+  val size = cardinality
+  override lazy val toString = {
+    var finalString = s"Multiset $name of size ${size.toString()} with entries:"
+    for ((k, v) <- containment)
+      finalString ++= s"\n $k occurs ${v.toString} time"
+    finalString
+  }
+}
+
+case class BasicHeap(basicHeapEntries: Set[BasicHeapEntry]) {
+  override lazy val toString = basicHeapEntries.map(x => x.toString).mkString("", "\n", "")
+}
+
+case class BasicHeapEntry(reference: Seq[String], field: Seq[String], valueID: String, perm: Option[Rational], het: HeapEntryType, insidePredicate: Option[scala.collection.immutable.Map[Exp, ModelEntry]]) {
+  override lazy val toString = {
+    het match {
+      case PredicateType =>
+        println(insidePredicate.get.toString())
+        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")})"
+    }
+  }
+}
+
+case class BasicDomainEntry(name: String, types: Seq[ast.Type], functions: Seq[BasicFunctionEntry]) {
+  override def toString: String = s"domain $valueName{\n ${functions.map(_.toString()).mkString("\n")}\n}"
+  val valueName: String = s"$name${printTypes()}"
+  private def printTypes(): String =
+    if (types.isEmpty) ""
+    else types.map(printType).mkString("[", ", ", "]")
+  private def printType(t: ast.Type): String = t match {
+    case ast.TypeVar(x) => x
+    case _ => t.toString()
+  }
+}
+
+
+case class BasicFunctionEntry(fname: String, argtypes: Seq[ast.Type], returnType: ast.Type, options: Map[Seq[String], String], default: String) {
+  override def toString: String = {
+    if (options.nonEmpty)
+      s"$fname${argtypes.mkString("(", ",", ")")}:${returnType}{\n" + options.map(o => "    " + o._1.mkString(" ") + " -> " + o._2).mkString("\n") + "\n    else -> " + default + "\n}"
+    else
+      s"$fname{\n    " + default + "\n}"
+  }
+}
+
+sealed trait HeapEntryType
+case object FieldType extends HeapEntryType
+case object PredicateType extends HeapEntryType
+case object QPFieldType extends HeapEntryType
+case object QPPredicateType extends HeapEntryType
+case object MagicWandType extends HeapEntryType
+case object QPMagicWandType extends HeapEntryType
+
+/*
+  Helper class for permissions
+ */
+
+final class Rational(n: BigInt, d: BigInt) extends Ordered[Rational] {
+  require(d != 0, "Denominator of Rational must not be 0.")
+
+  private val g = n.gcd(d)
+  val numerator: BigInt = n / g * d.signum
+  val denominator: BigInt = d.abs / g
+
+  def +(that: Rational): Rational = {
+    val newNum = this.numerator * that.denominator + that.numerator * this.denominator
+    val newDen = this.denominator * that.denominator
+    Rational(newNum, newDen)
+  }
+  def -(that: Rational): Rational = this + (-that)
+  def unary_- = Rational(-numerator, denominator)
+  def abs = Rational(numerator.abs, denominator)
+  def signum = Rational(numerator.signum, 1)
+
+  def *(that: Rational): Rational = Rational(this.numerator * that.numerator, this.denominator * that.denominator)
+  def /(that: Rational): Rational = this * that.inverse
+  def inverse = Rational(denominator, numerator)
+
+  def compare(that: Rational) = (this.numerator * that.denominator - that.numerator * this.denominator).signum
+
+  override def equals(obj: Any) = obj match {
+    case that: Rational => this.numerator == that.numerator && this.denominator == that.denominator
+    case _ => false
+  }
+
+  override def hashCode(): Int = viper.silver.utility.Common.generateHashCode(n, d)
+
+  override lazy val toString = s"$numerator/$denominator"
+}
+
+object Rational extends ((BigInt, BigInt) => Rational) {
+  val zero = Rational(0, 1)
+  val one = Rational(1, 1)
+
+  def apply(numer: BigInt, denom: BigInt) = new Rational(numer, denom)
+
+  def unapply(r: Rational) = Some(r.numerator, r.denominator)
+}

src/test/resources/counterexample_general/qfield.vpr

@@ -0,0 +1,18 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+method foo(s: Seq[Ref], i: Int, m: Int)
+  requires forall j: Int, k: Int :: 0 <= j < k < |s| ==> s[j] != s[k]
+  requires forall j: Int :: 0 <= j < |s| ==> acc(s[j].f)
+  requires forall j: Int :: 0 <= j < |s| ==> s[j].f > 0
+  requires 0 <= i < |s|
+  requires 0 <= m < |s|
+  requires i < m
+{
+   if (s[i].f < 2) {
+     //:: ExpectedCounterexample(assert.failed:assertion.false, (s[m].f == 1, s[i].f == 1))
+     assert s[m].f > 1
+   }
+}

src/test/resources/counterexample_general/qpred.vpr

@@ -0,0 +1,22 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field x: Int
+field y: Int
+
+predicate P(this: Ref, n: Int) {
+  acc(this.x) && acc(this.y) && this.x == n
+}
+
+method foo(refs: Set[Ref], r2: Ref, r3: Ref)
+  requires forall r: Ref :: r in refs ==> P(r, 3)
+  requires forall i: Int, r: Ref :: r == r2 && i == 4 ==> P(r, i)
+{
+  if (r3 in refs) {
+    assert P(r3, 3);
+    exhale acc(P(r2, 4), 1/2)
+
+    //:: ExpectedCounterexample(assert.failed:assertion.false, (acc(P(r3, 3), 1/1), acc(P(r2, 4), 1/2)))
+    assert false
+  }
+}

src/test/resources/counterexample_mapped/cyclic-ref.vpr

@@ -0,0 +1,13 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field next: Ref
+
+method foo(a: Ref, b: Ref)
+  requires acc(a.next) && acc(b.next)
+{
+  a.next := b
+  b.next := a
+  //:: ExpectedCounterexample(assert.failed:assertion.false, (a.next.next == a, b == b.next.next))
+  assert(false)
+}

src/test/resources/counterexample_mapped/functions.vpr

@@ -0,0 +1,17 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+function foo(z: Int): Int
+{
+  42
+}
+
+method bar()
+  requires foo(3) == 42
+{
+  var x: Int
+  assume x == 5
+  var y: Int := foo(x)
+  //:: ExpectedCounterexample(assert.failed:assertion.false, (x == 5, y == 42))
+  assert(false)
+}

src/test/resources/counterexample_mapped/lseg.vpr

@@ -0,0 +1,28 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field elem : Int
+field next : Ref
+
+predicate lseg(first: Ref, last: Ref, values: Seq[Int])
+{
+  first != last ==>
+    acc(first.elem) && acc(first.next) &&
+    0 < |values| &&
+    first.elem == values[0] &&
+    lseg(first.next, last, values[1..])
+}
+
+method removeFirst(first: Ref, last: Ref, values: Seq[Int]) returns  (value: Int, second: Ref)
+  requires lseg(first, last, values)
+  requires first != last
+  ensures  lseg(second, last, values[1..])
+  // we have insufficient field permissions when second is equal to last:
+  //:: ExpectedCounterexample(not.wellformed:insufficient.permission, (second == last))
+  //:: ExpectedCounterexample(postcondition.violated:assertion.false, (second == last))
+  ensures  value != unfolding lseg(second, last, values[1..]) in second.elem
+{
+  unfold lseg(first, last, values)
+  value := first.elem
+  second := first.next
+}

src/test/resources/counterexample_mapped/method-call.vpr

@@ -0,0 +1,19 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+method client(a: Ref)
+  requires acc(a.f)
+{
+  //:: ExpectedCounterexample(call.precondition:assertion.false, (a.f == 5))
+  set(a, 5)
+  a.f := 6
+}
+
+method set(x: Ref, i: Int)
+  requires acc(x.f) && x.f != i
+  ensures  acc(x.f) && x.f == i
+{
+  x.f := i
+}