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

Open
marcoeilers wants to merge 11 commits into
base: master
Choose a base branch
from
Open

Carbon implementation of new backend-independent counterexample format #574

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 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
3c76c3e
Adapting to new model names and format
marcoeilers Jul 13, 2026
1190c2a
Adapt to new wand model
marcoeilers Jul 13, 2026
d5b56f3
Renaming
marcoeilers Jul 13, 2026
714cc05
Fixed parsing of permission amounts
marcoeilers Jul 13, 2026
a739fad
Use Boogie's capturedState attribute to extract states for CEs
marcoeilers Jul 14, 2026
d6df9c0
Replacing old machinery completely
marcoeilers Jul 15, 2026
d9bb6d1
Counterexample extraction for maps, some robustness improvements
marcoeilers Jul 15, 2026
a64a34b
Merge
marcoeilers Jul 16, 2026
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 33 files
+20 −2 src/main/scala/viper/silver/ast/Expression.scala
+2 −0 src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
+5 −1 src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
+6 −0 src/main/scala/viper/silver/testing/BackendTypeTest.scala
+251 −0 src/main/scala/viper/silver/verifier/Counterexample.scala
+30 −0 src/test/resources/counterexample_general/field_permissions.vpr
+106 −0 src/test/resources/counterexample_general/field_permissions_qp.vpr
+34 −0 src/test/resources/counterexample_general/field_values.vpr
+42 −0 src/test/resources/counterexample_general/field_values_qp.vpr
+27 −0 src/test/resources/counterexample_general/local_values.vpr
+19 −0 src/test/resources/counterexample_general/magic_wands.vpr
+12 −0 src/test/resources/counterexample_general/maps.vpr
+12 −0 src/test/resources/counterexample_general/multisets.vpr
+22 −0 src/test/resources/counterexample_general/predicate_permissions.vpr
+30 −0 src/test/resources/counterexample_general/predicate_permissions_qp.vpr
+18 −0 src/test/resources/counterexample_general/qfield.vpr
+23 −0 src/test/resources/counterexample_general/qpred.vpr
+22 −0 src/test/resources/counterexample_general/sequences.vpr
+12 −0 src/test/resources/counterexample_general/sets.vpr
+26 −0 src/test/resources/counterexample_general/two_qp_same_field.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
+196 −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, CarbonResolvedCounterexample, 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.{ResolvedModel, RawModel, 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 rawCounterexample = false
var resolvedCounterexample = false
if (config == null) Seq() else config.counterexample.toOption match {
case Some(NativeModel) =>
case Some(VariablesModel) => transformNames = true
case Some(RawModel) => rawCounterexample = true
case Some(ResolvedModel) => resolvedCounterexample = 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 rawCounterexample => {
errors.foreach(e => CarbonResolvedCounterexample.transformRawCounterexample(e, translatedNames, program, wandModule.lazyWandToShapes))
}
case Failure(errors) if resolvedCounterexample => {
errors.foreach(e => CarbonResolvedCounterexample.transformResolvedCounterexample(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