Fixing variable counterexamples and adding tests (#915)

Author: marcoeilers

silver

@@ -10,7 +10,7 @@ import viper.silicon.debugger.{DebugAxiom, DebugExp, DebugExpPrintConfiguration}
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.interfaces.state.Chunk
 import viper.silicon.reporting._
-import viper.silicon.state.terms.{FunctionDecl, MacroDecl, Term}
+import viper.silicon.state.terms.{BooleanLiteral, FunctionDecl, IntLiteral, MacroDecl, Term, Var}
 import viper.silicon.state.{State, Store}
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
@@ -166,11 +166,22 @@ case class SiliconNativeCounterexample(internalStore: Store, heap: Iterable[Chun
 
 case class SiliconVariableCounterexample(internalStore: Store, nativeModel: Model) extends SiliconCounterexample {
   override val model: Model = {
-    Model(internalStore.values.filter{
-      case (_,v) => nativeModel.entries.contains(v.toString)
-    }.map{
-      case (k, v) => k.name -> nativeModel.entries(v.toString)
-    })
+    val variableValues = internalStore.values.filter {
+      case (_, (v: Var, _)) => nativeModel.entries.contains(v.toString)
+      case _ => false
+    }.map {
+      case (k, (v, _)) => k.name -> nativeModel.entries(v.toString)
+    }
+    val constantValues = internalStore.values.filter {
+      case (_, (_: IntLiteral, _)) => true
+      case (_, (_: BooleanLiteral, _)) => true
+      case _ => false
+    }.map {
+      case (k, (i: IntLiteral, _)) => k.name -> ConstantEntry(i.toString)
+      case (k, (b: BooleanLiteral, _)) => k.name -> ConstantEntry(b.toString)
+    }
+
+    Model(variableValues ++ constantValues)
   }
 
   override def withStore(s: Store): SiliconCounterexample = {

src/main/scala/interfaces/Verification.scala

@@ -7,11 +7,10 @@
 package viper.silicon.tests
 
 import viper.silicon.Silicon
-import viper.silver.testing.{AbstractOutput, CustomAnnotation, DefaultAnnotatedTestInput, DefaultTestInput, OutputAnnotationId, SilOutput, TestAnnotation, TestAnnotationParser, TestCustomError, TestError, TestInput}
+import viper.silver.testing.{AbstractOutput, CounterexampleParser, CustomAnnotation, DefaultAnnotatedTestInput, DefaultTestInput, ExpectedCounterexample, OutputAnnotationId, SilOutput, TestAnnotation, TestAnnotationParser, TestCustomError, TestError, TestInput}
 import fastparse._
 import viper.silicon.interfaces.SiliconMappedCounterexample
 import viper.silicon.reporting.{ExtractedModel, ExtractedModelEntry, LitIntEntry, LitPermEntry, NullRefEntry, RecursiveRefEntry, RefEntry, SeqEntry}
-import viper.silver.parser.FastParserCompanion.whitespace
 import viper.silver.parser.{FastParser, PAccPred, PBinExp, PExp, PFieldAccess, PIdnUseExp, PIntLit, PLookup, PSymOp, PUnExp}
 import viper.silver.utility.Common.Rational
 import viper.silver.verifier.{FailureContext, VerificationError}
@@ -167,24 +166,3 @@ case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path,
 
   override def withForLineNr(line: Int = forLineNr): ExpectedCounterexampleAnnotation = ExpectedCounterexampleAnnotation(id, file, line, expectedCounterexample)
 }
-
-/**
-  * Simple input language to describe an expected counterexample with corresponding parser.
-  * Currently, a counterexample is expressed by a comma separated list of access predicates and equalities (using the
-  * same syntax as in Viper)
-  */
-class CounterexampleParser(fp: FastParser) {
-  import fp.{accessPred, eqExp}
-
-  def expectedCounterexample[_: P]: P[ExpectedCounterexample] =
-    (Start ~ "(" ~ (accessPred | eqExp).rep(0, ",") ~ ")" ~ End)
-      .map(ExpectedCounterexample)
-}
-
-case class ExpectedCounterexample(exprs: Seq[PExp]) {
-  assert(exprs.forall {
-    case _: PAccPred => true
-    case PBinExp(_, r, _) if r.rs == PSymOp.EqEq => true
-    case _ => false
-  })
-}

src/test/scala/CounterexampleTests.scala

@@ -0,0 +1,42 @@
+// 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-2025 ETH Zurich.
+
+package viper.silicon.tests
+
+import viper.silicon.Silicon
+import viper.silver.testing.{CounterexampleComparison, CounterexampleVariablesTests, ExpectedCounterexample, ExpectedValuesCounterexampleAnnotation, OutputAnnotationId, TestCustomError, TestError}
+import viper.silicon.interfaces.SiliconVariableCounterexample
+import viper.silver.verifier.FailureContext
+
+import java.nio.file.Path
+
+class SiliconCounterexampleVariablesTests extends SiliconTests with CounterexampleVariablesTests {
+
+  override def configureVerifiersFromConfigMap(configMap: Map[String, Any]): Unit = {
+    val args = Silicon.optionsFromScalaTestConfigMap(prefixSpecificConfigMap(configMap).getOrElse("silicon", Map()))
+    val additionalArgs = Seq("--counterexample=variables", "--exhaleMode=1")
+
+    silicon.parseCommandLine(args ++ additionalArgs :+ Silicon.dummyInputFilename)
+  }
+
+  override def createExpectedValuesCounterexampleAnnotation(id: OutputAnnotationId, file: Path, forLineNr: Int, expectedCounterexample: ExpectedCounterexample): ExpectedValuesCounterexampleAnnotation =
+    SiliconExpectedValuesCounterexampleAnnotation(id, file, forLineNr, expectedCounterexample)
+}
+
+/** represents an expected output (identified by `id`) with an associated (possibly partial) counterexample model */
+case class SiliconExpectedValuesCounterexampleAnnotation(id: OutputAnnotationId, file: Path, forLineNr: Int, expectedCounterexample: ExpectedCounterexample) extends
+  ExpectedValuesCounterexampleAnnotation(id, file, forLineNr, expectedCounterexample) {
+
+  def containsExpectedCounterexample(failureContext: FailureContext): Boolean =
+    failureContext.counterExample match {
+      case Some(silCounterexample: SiliconVariableCounterexample) => CounterexampleComparison.meetsExpectations(expectedCounterexample, silCounterexample.model)
+      case _ => false
+    }
+
+  override def notFoundError: TestError = TestCustomError(s"Expected the following counterexample on line $forLineNr: $expectedCounterexample")
+
+  override def withForLineNr(line: Int = forLineNr): ExpectedValuesCounterexampleAnnotation = SiliconExpectedValuesCounterexampleAnnotation(id, file, line, expectedCounterexample)
+}