Skip to content

Carbon implementation of new backend-independent counterexample format #574

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
marcoeilers wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

Carbon implementation of new backend-independent counterexample format #574

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
9d9a369
General counterexample extraction by Raoul
marcoeilers Jul 1, 2024
3dbd2e6
Adding CE tests, more consistent naming
marcoeilers Sep 1, 2025
e220e67
Adapting to silver changes
marcoeilers Sep 1, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion silver
Open in desktop
Submodule silver updated 19 files
+4 −2 src/main/scala/viper/silver/ast/Expression.scala
+4 −0 src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
+6 −0 src/main/scala/viper/silver/testing/BackendTypeTest.scala
+222 −0 src/main/scala/viper/silver/verifier/Counterexample.scala
+18 −0 src/test/resources/counterexample_general/qfield.vpr
+22 −0 src/test/resources/counterexample_general/qpred.vpr
+13 −0 src/test/resources/counterexample_mapped/cyclic-ref.vpr
+17 −0 src/test/resources/counterexample_mapped/functions.vpr
+28 −0 src/test/resources/counterexample_mapped/lseg.vpr
+19 −0 src/test/resources/counterexample_mapped/method-call.vpr
+10 −0 src/test/resources/counterexample_mapped/negative.vpr
+11 −0 src/test/resources/counterexample_mapped/permissions.vpr
+27 −0 src/test/resources/counterexample_mapped/predicate.vpr
+12 −0 src/test/resources/counterexample_mapped/ref-sequence.vpr
+14 −0 src/test/resources/counterexample_mapped/sequence.vpr
+27 −0 src/test/resources/counterexample_mapped/simple-refs-rec.vpr
+21 −0 src/test/resources/counterexample_mapped/simple-refs.vpr
+0 −21 src/test/scala/CounterexampleVariablesTests.scala
+210 −0 src/test/scala/ExpectedCounterexampleAnnotation.scala
14 changes: 12 additions & 2 deletions src/main/scala/viper/carbon/CarbonVerifier.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,15 +6,15 @@

package viper.carbon

import boogie.{BoogieModelTransformer, Namespace}
import boogie.{BoogieModelTransformer, CarbonExtendedCounterexample, Namespace}
import modules.impls._
import viper.silver.ast.{MagicWand, Program, Quasihavoc, Quasihavocall}
import viper.silver.utility.Paths
import viper.silver.verifier._
import verifier.{BoogieDependency, BoogieInterface, Verifier}

import java.io.{BufferedOutputStream, File, FileOutputStream, IOException}
import viper.silver.frontend.{MissingDependencyException, NativeModel, VariablesModel}
import viper.silver.frontend.{ExtendedModel, IntermediateModel, MissingDependencyException, NativeModel, VariablesModel}
import viper.silver.reporter.Reporter

/**
Expand Down Expand Up @@ -177,9 +177,13 @@ case class CarbonVerifier(override val reporter: Reporter,
heapModule.enableAllocationEncoding = config == null || !config.disableAllocEncoding.isSupplied // NOTE: config == null happens on the build server / via sbt test

var transformNames = false
var intermediateCounterexample = false
var extendedCounterexample = true
if (config == null) Seq() else config.counterexample.toOption match {
case Some(NativeModel) =>
case Some(VariablesModel) => transformNames = true
case Some(IntermediateModel) => intermediateCounterexample = true
case Some(ExtendedModel) => extendedCounterexample = true
case None =>
case Some(v) => sys.error("Invalid option: " + v)
}
Expand Down Expand Up @@ -243,6 +247,12 @@ case class CarbonVerifier(override val reporter: Reporter,
case Failure(errors) if transformNames => {
errors.foreach(e => BoogieModelTransformer.transformCounterexample(e, translatedNames))
}
case Failure(errors) if intermediateCounterexample => {
errors.foreach(e => CarbonExtendedCounterexample.transformInteremdiateCounterexample(e, translatedNames, program, wandModule.lazyWandToShapes))
}
case Failure(errors) if extendedCounterexample => {
errors.foreach(e => CarbonExtendedCounterexample.transformExtendedCounterexample(e, translatedNames, program, wandModule.lazyWandToShapes))
}
case _ => result
}
result
Expand Down
6 changes: 3 additions & 3 deletions src/main/scala/viper/carbon/boogie/BoogieModelTransformer.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package viper.carbon.boogie

import viper.carbon.verifier.FailureContextImpl
import viper.silver.verifier.{AbstractError, Counterexample, FailureContext, Model, ModelEntry, SimpleCounterexample, VerificationError}
import viper.silver.verifier.{AbstractError, Model, ModelEntry, SimpleCounterexample, VerificationError}

import scala.collection.mutable

Expand All @@ -14,9 +14,9 @@ object BoogieModelTransformer {
* Adds a counterexample to the given error if one is available.
*/
def transformCounterexample(e: AbstractError, names: Map[String, Map[String, String]]) : Unit = {
if (e.isInstanceOf[VerificationError] && ErrorMemberMapping.mapping.contains(e.asInstanceOf[VerificationError])){
if (e.isInstanceOf[VerificationError] && ErrorMemberMapping.mapping.contains(e.asInstanceOf[VerificationError].readableMessage(true, true))){
val ve = e.asInstanceOf[VerificationError]
val methodName = ErrorMemberMapping.mapping.get(ve).get.name
val methodName = ErrorMemberMapping.mapping.get(ve.readableMessage(true, true)).get.name
val namesInMember = names.get(methodName).get.map(e => e._2 -> e._1)
val originalEntries = ve.failureContexts(0).counterExample.get.model.entries

Expand Down
Loading
Loading