From 9d9a369847b5392b937b135dae3a9c9e1adb91af Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 1 Jul 2024 17:19:45 +0200 Subject: [PATCH 1/9] General counterexample extraction by Raoul --- silver | 2 +- .../scala/viper/carbon/CarbonVerifier.scala | 14 +- .../boogie/BoogieModelTransformer.scala | 4 +- .../boogie/CounterexampleGenerator.scala | 1192 +++++++++++++++++ .../scala/viper/carbon/boogie/boogie.scala | 4 +- .../modules/impls/DefaultWandModule.scala | 2 +- .../carbon/verifier/BoogieInterface.scala | 1 + 7 files changed, 1211 insertions(+), 8 deletions(-) create mode 100644 src/main/scala/viper/carbon/boogie/CounterexampleGenerator.scala diff --git a/silver b/silver index 93bc9b75..1528fbe9 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 93bc9b7516a710c8f01438e430058c4a54e20512 +Subproject commit 1528fbe98a197de4e542a3d1140f54686d7c1a86 diff --git a/src/main/scala/viper/carbon/CarbonVerifier.scala b/src/main/scala/viper/carbon/CarbonVerifier.scala index fc33d06a..d1f128ee 100644 --- a/src/main/scala/viper/carbon/CarbonVerifier.scala +++ b/src/main/scala/viper/carbon/CarbonVerifier.scala @@ -6,7 +6,7 @@ package viper.carbon -import boogie.{BoogieModelTransformer, Namespace} +import boogie.{BoogieModelTransformer, CounterexampleGenerator, Namespace} import modules.impls._ import viper.silver.ast.{MagicWand, Program, Quasihavoc, Quasihavocall} import viper.silver.utility.Paths @@ -14,7 +14,7 @@ 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 /** @@ -171,9 +171,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) } @@ -237,6 +241,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 => CounterexampleGenerator.transformInteremdiateCounterexample(e, translatedNames, program, wandModule.lazyWandToShapes)) + } + case Failure(errors) if extendedCounterexample => { + errors.foreach(e => CounterexampleGenerator.transformExtendedCounterexample(e, translatedNames, program, wandModule.lazyWandToShapes)) + } case _ => result } result diff --git a/src/main/scala/viper/carbon/boogie/BoogieModelTransformer.scala b/src/main/scala/viper/carbon/boogie/BoogieModelTransformer.scala index 92fd8dc3..2195a085 100644 --- a/src/main/scala/viper/carbon/boogie/BoogieModelTransformer.scala +++ b/src/main/scala/viper/carbon/boogie/BoogieModelTransformer.scala @@ -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 diff --git a/src/main/scala/viper/carbon/boogie/CounterexampleGenerator.scala b/src/main/scala/viper/carbon/boogie/CounterexampleGenerator.scala new file mode 100644 index 00000000..890d7478 --- /dev/null +++ b/src/main/scala/viper/carbon/boogie/CounterexampleGenerator.scala @@ -0,0 +1,1192 @@ +package viper.carbon.boogie + +import scala.collection.mutable +import scala.collection.immutable._ +import viper.carbon.verifier.FailureContextImpl +import viper.silver.verifier._ +import viper.silver.ast +import viper.silver.ast.{Field, MagicWand, Member, Predicate, Resource} +import viper.silver.verifier.{AbstractError, ApplicationEntry, ConstantEntry, MapEntry, Model, ModelEntry, SimpleCounterexample, UnspecifiedEntry, ValueEntry, VerificationError} +import viper.silver.ast.{Declaration, MagicWandStructure, Program, Type} + +/** + * Transforms a counterexample returned by Boogie back to a Viper counterexample. The programmer can choose between an + * "intermediate" CE or an "extended" CE. + */ + +/** + * CounterexampleGenerator class used for generating an "extended" CE. + */ +case class CounterexampleGenerator(e: AbstractError, names: Map[String, Map[String, String]], program: Program, wandNames: Option[Map[MagicWandStructure.MagicWandStructure, Func]]) extends Counterexample { + val ve = e.asInstanceOf[VerificationError] + val errorMethod = ErrorMemberMapping.mapping.get(ve.readableMessage(true, true)).get + val imCE = IntermediateCounterexampleModel(ve, errorMethod, names, program, wandNames) + val model = imCE.originalEntries + //println(model) + + val (ceStore, refOcc) = CounterexampleGenerator.detStore(program.methodsByName.get(errorMethod.name).get.transitiveScopedDecls, imCE.basicVariables, imCE.allCollections) + val nameTranslationMap = CounterexampleGenerator.detTranslationMap(ceStore, refOcc) + var ceHeaps = imCE.allBasicHeaps.map(bh => (bh._1, CounterexampleGenerator.detHeap(imCE.workingModel, bh._2, program, imCE.allCollections, nameTranslationMap, imCE.originalEntries))).reverse + + val domainsAndFunctions = CounterexampleGenerator.detTranslatedDomains(imCE.DomainEntries, nameTranslationMap) ++ CounterexampleGenerator.detTranslatedFunctions(imCE.nonDomainFunctions, nameTranslationMap) + + override def toString: String = { + var finalString = " Extended Counterexample: \n" + finalString += " Store: \n" + if (!ceStore.storeEntries.isEmpty) + finalString += ceStore.storeEntries.map(x => x.toString).mkString("", "\n", "\n") + if (!ceHeaps.filter(y => !y._2.heapEntries.isEmpty).isEmpty) + finalString += ceHeaps.filter(y => !y._2.heapEntries.isEmpty).map(x => " " + x._1 + " Heap: \n" + x._2.toString).mkString("") + if (domainsAndFunctions.nonEmpty) { + finalString += " Domains: \n" + finalString += domainsAndFunctions.map(x => x.toString).mkString("", "\n", "\n") + } + finalString + } +} + +/** + * CounterexampleGenerator class used for generating an "interemediate" CE. + */ +case class IntermediateCounterexampleModel(ve: VerificationError, errorMethod: Member, names: Map[String, Map[String, String]], program: Program, wandNames: Option[Map[MagicWandStructure.MagicWandStructure, Func]]) extends Counterexample { + val originalEntries = ve.failureContexts(0).counterExample.get.model + val model = originalEntries + val typenamesInMethod = names.get(errorMethod.name).get.map(e => e._2 -> e._1) + val methodVarDecl = program.methodsByName.get(errorMethod.name).get.transitiveScopedDecls + + val (basicVariables, otherDeclarations) = IntermediateCounterexampleModel.detCEvariables(originalEntries.entries, typenamesInMethod, methodVarDecl) + val allSequences = IntermediateCounterexampleModel.detSequences(originalEntries) + val allSets = IntermediateCounterexampleModel.detSets(originalEntries) + val allMultisets = IntermediateCounterexampleModel.detMultisets(originalEntries) + val allCollections = allSequences ++ allSets ++ allMultisets + + val workingModel = IntermediateCounterexampleModel.buildNewModel(originalEntries.entries) + val (hmLabels, hmStates) = IntermediateCounterexampleModel.oldAndReturnHeapMask(workingModel, otherDeclarations) + val allBasicHeaps = IntermediateCounterexampleModel.detHeaps(workingModel, hmStates, originalEntries, hmLabels, program).map{case (n, bh) => if (n == "return") ("current", bh) else (n, bh)} + + val DomainEntries = IntermediateCounterexampleModel.getAllDomains(originalEntries, program) + val nonDomainFunctions = IntermediateCounterexampleModel.getAllFunctions(originalEntries, program, hmStates) + + override def toString: String = { + var finalString = " Intermediate Counterexample: \n" + finalString ++= " Local Information:\n" + if (!basicVariables.isEmpty) + finalString += basicVariables.map(x => x.toString).mkString("", "\n", "\n") + if (!allCollections.isEmpty) + finalString += allCollections.map(x => x.toString).mkString("", "\n", "\n") + if (!allBasicHeaps.filter(y => !y._2.basicHeapEntries.isEmpty).isEmpty) + finalString += allBasicHeaps.reverse.filter(y => !y._2.basicHeapEntries.isEmpty).map(x => " " + x._1 + " Heap: \n" + x._2.toString).mkString("", "\n", "\n") + if (!DomainEntries.isEmpty || !nonDomainFunctions.isEmpty) + finalString ++= " Domains:\n" + if (!DomainEntries.isEmpty) + finalString += DomainEntries.map(x => x.toString).mkString("", "\n", "\n") + if (!nonDomainFunctions.isEmpty) + finalString += nonDomainFunctions.map(x => x.toString).mkString("", "\n", "\n") + finalString + } +} + +object IntermediateCounterexampleModel { + /** + * Determines the local variables and their value. + */ + def detCEvariables(originalEntries: Map[String, ModelEntry], namesInMember: Map[String, String], variables: Seq[Declaration]): (Seq[CEVariable], Seq[Declaration]) = { + var res = Seq[CEVariable]() + var otherDeclarations = Seq[Declaration]() + val modelVariables = transformModelEntries(originalEntries, namesInMember) + for ((name, entry) <- modelVariables) { + for (temp <- variables) { + if (temp.isInstanceOf[ast.LocalVarDecl]) { + val v = temp.asInstanceOf[ast.LocalVarDecl] + if (v.name == name) { + var ent = entry + if (entry.isInstanceOf[MapEntry]) { + ent = entry.asInstanceOf[MapEntry].options.head._1(0) + } + res +:= CEVariable(v.name, ent, Some(v.typ)) + } + } else { + otherDeclarations +:= temp + } + } + } + if (originalEntries.contains("null")) { + val nullRef = originalEntries.get("null").get + if (nullRef.isInstanceOf[ConstantEntry]) { + res +:= CEVariable("null", nullRef, Some(ast.Ref)) + } + } + (res, otherDeclarations) + } + + /** + * Chooses the latest instance of a variable in the counterexample model received from the SMT solver. + */ + def transformModelEntries(originalEntries: Map[String, ModelEntry], namesInMember: Map[String, String]): mutable.Map[String, ModelEntry] = { + val newEntries = mutable.HashMap[String, ModelEntry]() + val currentEntryForName = mutable.HashMap[String, String]() + for ((vname, e) <- originalEntries) { + var originalName = vname + if (originalName.startsWith("q@")) { + originalName = originalName.substring(2) + } else if (originalName.indexOf("@@") != -1) { + originalName = originalName.substring(0, originalName.indexOf("@@")) + } else if (originalName.indexOf("@") != -1) { + originalName = originalName.substring(0, originalName.indexOf("@")) + } + if (PrettyPrinter.backMap.contains(originalName)) { + val originalViperName = PrettyPrinter.backMap.get(originalName).get + if (namesInMember.contains(originalViperName)) { + val viperName = namesInMember.get(originalViperName).get + if (!currentEntryForName.contains(viperName) || + isLaterVersion(vname, originalName, currentEntryForName.get(viperName).get)) { + newEntries.update(viperName, e) + currentEntryForName.update(viperName, vname) + } + } + } + } + newEntries + } + + def isLaterVersion(firstName: String, originalName: String, secondName: String): Boolean = { + if ((secondName == originalName || secondName == "q@" + originalName || secondName.indexOf("@@") != -1) && !"@@.*!".r.findFirstIn(firstName).isDefined) { + true + } else if (secondName.indexOf("@") != -1 && firstName.indexOf("@@") == -1 && firstName.indexOf("@") != -1) { + val firstIndex = Integer.parseInt(firstName.substring(firstName.indexOf("@") + 1)) + val secondIndex = Integer.parseInt(secondName.substring(secondName.indexOf("@") + 1)) + firstIndex > secondIndex + } else { + false + } + } + + /** + * Generates the sequences of the CE. + */ + def detSequences(model: Model): Set[CEValue] = { + var res = Map[String, Seq[String]]() + var tempMap = Map[(String, Seq[String]), String]() + for ((opName, opValues) <- model.entries) { + if (opName == "Seq#Length") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + res += (k(0).toString -> Seq.fill(v.toString.toInt)("#undefined")) + } + } + } else if (opName == "Seq#Empty") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + res += (v.toString -> Seq()) + } + } + } else if (opName == "Seq#Append" || opName == "Seq#Take" || opName == "Seq#Drop" || opName == "Seq#Index") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + tempMap += ((opName, k.map(x => x.toString)) -> v.toString) + } + } + } + } + for ((opName, opValues) <- model.entries) { + if (opName == "Seq#Singleton") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + res += (v.toString -> Seq(k(0).toString)) + } + } + } + if (opName == "Seq#Range") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + res += (v.toString -> Seq.range(k(0).toString.toInt, k(1).toString.toInt).map(x => x.toString)) + } + } + } + } + var found = true + while (found) { + found = false + for (((opName, k), v) <- tempMap) { + if (opName == "Seq#Append") { + (res.get(k(0)), res.get(k(1))) match { + case (Some(x), Some(y)) => + if (!res.contains(v)) { + res += (v -> (x ++ y)) + tempMap -= ((opName, k)) + found = true + } + case (_, _) => // + } + } else if (opName == "Seq#Take") { + res.get(k(0)) match { + case Some(x) => + res += (v -> x.take(k(1).toInt)) + tempMap -= ((opName, k)) + found = true + case None => // + } + } else if (opName == "Seq#Drop") { + res.get(k(0)) match { + case Some(x) => + res += (v -> x.drop(k(1).toInt)) + tempMap -= ((opName, k)) + found = true + case None => // + } + } else if (opName == "Seq#Index") { + res.get(k(0)) match { + case Some(x) => + if (!k(1).startsWith("(")) { + res += (k(0) -> x.updated(k(1).toInt, v)) + found = true + } + tempMap -= ((opName, k)) + case None => // + } + } + } + } + var ans = Set[CEValue]() + res.foreach { + case (n, s) => + val typ: Option[Type] = detASTTypeFromString(n.replaceAll(".*?<(.*)>.*", "$1")) match { + case Some(x) => Some(ast.SeqType(x)) + case None => None + } + var entries = Map[BigInt, String]() + var counter = 0 + for (e <- s) { + if (e != "#undefined") { + entries += (BigInt(counter) -> e) + } + counter += 1 + } + ans += CESequence(n, BigInt(s.length), entries, s, typ) + } + ans + } + + /** + * Generates the sets of the CE. + */ + def detSets(model: Model): Set[CEValue] = { + var res = Map[String, Set[String]]() + for ((opName, opValues) <- model.entries) { + if (opName == "Set#Empty") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + res += (v.toString -> Set()) + } + } else if (opValues.isInstanceOf[ConstantEntry] && opValues.asInstanceOf[ConstantEntry].value != "false" && opValues.asInstanceOf[ConstantEntry].value != "true") { + res += (opValues.asInstanceOf[ConstantEntry].value -> Set()) + } + } + if (opName == "Set#Singleton") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + res += (v.toString -> Set(k(0).toString)) + } + } + } + if (opName == "Set#Card") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + if (v.toString.startsWith("0")) { + res += (k(0).toString -> Set()) + } + } + } + } + if (opName == "MapType2Select") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + if (v.toString.toBoolean) { + if (k(1).toString.startsWith("T@U!val!")) { + res += (k(0).toString -> Set()) + } else { + res += (k(0).toString -> Set()) + } + } + } + } + } + } + var tempMap = Map[(String, Seq[String]), String]() + for ((opName, opValues) <- model.entries) { + if (opName == "Set#UnionOne" || opName == "MapType2Select") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + tempMap += ((opName, k.map(x => x.toString)) -> v.toString) + } + } + } + } + while (!tempMap.isEmpty) { + for (((opName, k), v) <- tempMap) { + if (opName == "Set#UnionOne") { + res.get(k(0)) match { + case Some(x) => + res += (v -> x.union(Set(k(1)))) + tempMap -= ((opName, k)) + case None => // + } + } else if (opName == "MapType2Select") { + res.get(k(0)) match { + case Some(x) => + if (v.toBoolean && !k(1).startsWith("T@U!val!")) { + res += (k(0) -> x.union(Set(k(1)))) + } + case None => + if (v.toBoolean && !k(1).startsWith("T@U!val!")) { + res += (k(0) -> Set(k(1))) + } else { + res += (k(0) -> Set()) + } + } + tempMap -= ((opName, k)) + } + } + } + for ((opName, opValues) <- model.entries) { + if (opName == "Set#Union" || opName== "Set#Difference" || opName == "Set#Intersection") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + tempMap += ((opName, k.map(x => x.toString)) -> v.toString) + } + } + } + } + var found = true + while (!tempMap.isEmpty && found) { + found = false + for (((opName, k), v) <- tempMap) { + val firstSet = res.get(k(0)) + val secondSet = res.get(k(1)) + if ((firstSet != None) && (secondSet != None)) { + if (opName == "Set#Union") { + res += (v -> firstSet.get.union(secondSet.get)) + tempMap -= ((opName, k)) + found = true + } else if (opName == "Set#Intersection") { + res += (v -> firstSet.get.intersect(secondSet.get)) + tempMap -= ((opName, k)) + found = true + } else if (opName == "Set#Difference") { + res += (v -> firstSet.get.diff(secondSet.get)) + tempMap -= ((opName, k)) + found = true + } + } + } + } + var ans = Set[CEValue]() + res.foreach { + case (n, s) => + val typ: Option[Type] = detASTTypeFromString(n.replaceAll(".*?<(.*)>.*", "$1")) match { + case Some(x) => Some(ast.SetType(x)) + case None => None + } + var containment = Map[String, Boolean]() + for (e <- s) { + if (e != "#undefined") { + containment += (e -> true) + } + } + ans += CESet(n, BigInt(s.size), containment, s, typ) + } + ans + } + + /** + * Generates the multisets of the CE. + */ + def detMultisets(model: Model): Set[CEValue] = { + var res = Map[String, Map[String, Int]]() + for ((opName, opValues) <- model.entries) { + if (opName == "MultiSet#Empty") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + res += (v.toString -> Map[String, Int]()) + } + } else if (opValues.isInstanceOf[ConstantEntry] && opValues.asInstanceOf[ConstantEntry].value != "false" && opValues.asInstanceOf[ConstantEntry].value != "true") { + res += (opValues.asInstanceOf[ConstantEntry].value -> Map[String, Int]()) + } + } + if (opName == "MultiSet#Singleton") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + res += (v.toString -> Map(k(0).toString -> 1)) + } + } + } + if (opName == "MultiSet#Select") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + if (!k(1).toString.startsWith("T@U!val!") && !v.toString.startsWith("0")) { + res += (k(0).toString -> res.getOrElse(k(0).toString, Map.empty).updated(k(1).toString, v.toString.toInt)) + } + } + } + } + if (opName == "MultiSet#Card") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + if (v.toString.startsWith("0")) { + res += (k(0).toString -> Map[String, Int]()) + } + } + } + } + } + var tempMap = Map[(String, Seq[String]), String]() + for ((opName, opValues) <- model.entries) { + if (opName == "MultiSet#UnionOne") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + tempMap += ((opName, k.map(x => x.toString)) -> v.toString) + } + } + } + } + while (!tempMap.isEmpty) { + for (((opName, k), v) <- tempMap) { + res.get(k(0)) match { + case Some(x) => + res += (v -> x.updated(k(1), x.getOrElse(k(1), 0)+1)) + tempMap -= ((opName, k)) + case None => // + } + } + } + for ((opName, opValues) <- model.entries) { + if (opName == "MultiSet#Union" || opName == "MultiSet#Difference" || opName == "MultiSet#Intersection") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + tempMap += ((opName, k.map(x => x.toString)) -> v.toString) + } + } + } + } + while (!tempMap.isEmpty) { + for (((opName, k), v) <- tempMap) { + val firstMultiset = res.get(k(0)) + val secondMultiset = res.get(k(1)) + if ((firstMultiset != None) && (secondMultiset != None)) { + if (opName == "MultiSet#Union") { + res += (v -> (firstMultiset.get.keySet ++ secondMultiset.get.keySet).map { key => + (key -> (firstMultiset.get.getOrElse(key, 0) + secondMultiset.get.getOrElse(key, 0))) + }.toMap) + tempMap -= ((opName, k)) + } else if (opName == "MultiSet#Intersection") { + res += (v -> (firstMultiset.get.keySet & secondMultiset.get.keySet).map { key => + key -> Math.min(firstMultiset.get.get(key).get, secondMultiset.get.get(key).get) + }.toMap) + tempMap -= ((opName, k)) + } else if (opName == "MultiSet#Difference") { + res += (v -> (firstMultiset.get.map { case (key, count) => + key -> (count - secondMultiset.get.getOrElse(key, 0)) + }.filter(_._2 > 0) ++ secondMultiset.get.filter { case (key, _) => + !firstMultiset.get.contains(key) + })) + tempMap -= ((opName, k)) + } + } + } + } + var ans = Set[CEValue]() + res.foreach { + case (n, s) => + val typ: Option[Type] = detASTTypeFromString(n.replaceAll(".*?<(.*)>.*", "$1")) match { + case Some(x) => Some(ast.SetType(x)) + case None => None + } + val size = s.values.sum + ans += CEMultiset(n, BigInt(size), s, typ) + } + ans + } + + def detASTTypeFromString(typ: String): Option[Type] = { + typ match { + case "Int" => Some(ast.Int) + case "Bool" => Some(ast.Bool) + case "Perm" => Some(ast.Perm) + case "Ref" => Some(ast.Ref) + case _ => None + } + } + + /** + * Takes the counterexample model received from the SMT solver and restructures it. + */ + def buildNewModel(originalEntries: Map[String, ModelEntry]): Map[Seq[String], String] = { + var newEntriesMapping = Map[Seq[String], String]() + for ((key, value) <- originalEntries) { + if (value.isInstanceOf[ConstantEntry]) { + val valConstEntry = value.asInstanceOf[ConstantEntry] + newEntriesMapping += (Seq(key) -> valConstEntry.toString) + } else if (value.isInstanceOf[MapEntry]) { + val tempMapping = value.asInstanceOf[MapEntry].options + for ((keyTM, valueTM) <- tempMapping) { + val tempSeq = (keyTM.map(x => x.toString)) + if (tempSeq.contains("else")) { + // + } else { + newEntriesMapping += (Seq(key) ++ tempSeq -> valueTM.toString) + } + } + } else if (value.isInstanceOf[ApplicationEntry]) { + val applEntry = value.asInstanceOf[ApplicationEntry] + newEntriesMapping += (Seq(key) -> applEntry.toString) + } else if (value.toString != UnspecifiedEntry.toString) { + println("error in buildNewModel") + } + } + newEntriesMapping + } + + /** + * Gather all the heap and mask states from the model. Then, combine them into heap instances (=> mask state + heap state) + * and order them. + */ + def oldAndReturnHeapMask(workingModel: Map[Seq[String], String], labels: Seq[Declaration]): (Map[String, (String, String)], List[(String, String, String, String)]) = { + var heapInstances = Set[(String, String)]() + var maskInstances = Set[(String, String)]() + var states = Set[(String, String)]() + for ((k, v) <- workingModel) { + if (k(0).startsWith("Heap@@")) { + heapInstances += ((k(0), v)) + } else if (k(0).startsWith("Mask@@")) { + maskInstances += ((k(0), v)) + } else if (k(0).startsWith("Heap@")) { + heapInstances += ((k(0), v)) + } else if (k(0).startsWith("Mask@")) { + maskInstances += ((k(0), v)) + } else if (k(0).startsWith("QPMask@")) { + maskInstances += ((k(0).stripPrefix("QP").trim, v)) + } else if ((k(0) == "state") && (v == "true")) { + states += ((k(1), k(2))) + } + } + + // determine all the heap and mask states (first all, then sorted and then filtered) + val hmStates = for { + (heapId, maskId) <- states + hName <- heapInstances.collect { case (name, id) if id == heapId => name } + mName <- maskInstances.collect { case (name, id) if id == maskId => name } + } yield (hName, mName, heapId, maskId) + + val sortedHMStates = hmStates.toList.sortBy { + case (heapName, maskName, _, _) => + if (heapName.startsWith("Heap@@") && maskName.startsWith("Mask@@")) { + 0 + } else if (heapName.startsWith("Heap@@")) { + val maskValue = maskName.stripPrefix("Mask@").trim.toInt + maskValue + 1 + } else if (maskName.startsWith("Mask@@")) { + val heapValue = heapName.stripPrefix("Heap@").trim.toInt + heapValue + 1 + } else { + val heapValue = heapName.stripPrefix("Heap@").trim.toInt + val maskValue = maskName.stripPrefix("Mask@").trim.toInt + heapValue + maskValue + 2 + } + } + + val filteredList = sortedHMStates.foldLeft(List.empty[(String, String, String, String)]) { + case (acc, curr@(h, m, _, _)) + if h.contains("@@") || m.contains("@@") || acc.isEmpty || acc.last._1.contains("@@") || acc.last._2.contains("@@") || (h.stripPrefix("Heap@").trim.toInt >= acc.last._1.stripPrefix("Heap@").trim.toInt && m.stripPrefix("Mask@").trim.toInt >= acc.last._2.stripPrefix("Mask@").trim.toInt) => + acc :+ curr + case (acc, _) => + acc + } + + var labelsHeapMask = Map[String, (String, String)]() + labelsHeapMask += ("old" -> (filteredList(0)._3, filteredList(0)._4)) + for (l <- labels) { + l match { + case ast.Label(n, _) => + val lhi = "Label" + n + "Heap" + val lmi = "Label" + n + "Mask" + if (workingModel.contains(Seq(lhi)) && workingModel.contains(Seq(lmi))) { + labelsHeapMask += (n -> (workingModel.get(Seq(lhi)).get, workingModel.get(Seq(lmi)).get)) + } + case _ => // + } + } + labelsHeapMask += ("return" -> (filteredList(filteredList.length-1)._3, filteredList(filteredList.length-1)._4)) + + (labelsHeapMask, filteredList) + } + + /** + * Determines all the heap resources by iterating through the heap instances: Check all the "MapType0Select" function + * for the heap state of the heap instance and check the "MapType0Select" function for the mask state of the heap + * instance. Then gather all the heap resources that occur in both functions for a specific heap instance. + * @param MapType0Select Mappings from a heap state, a reference and a field to a value. + * @param MapType0Select Mappings from a mask state, a reference and a field to a permission. + * The fields in these mappings can also be identifiers for a predicate or a magic wand. + */ + def detHeaps(opMapping: Map[Seq[String], String], hmStates: List[(String, String, String, String)], model: Model, hmLabels: Map[String, (String, String)], program: Program): Seq[(String, BasicHeap)] = { + val predByName = program.predicatesByName + var heapOp = Map[Seq[String], String]() + var maskOp = Map[Seq[String], String]() + var qpMaskSet = Set[String]() + for ((key, value) <- opMapping) { + if (key(0).startsWith("MapType0Select")) { + heapOp += (key -> value) + } else if (key(0).startsWith("MapType1Select")) { + maskOp += (key -> value) + } else if (key(0).startsWith("QPMask@")) { + qpMaskSet += value + } + } + var predContentMap = Map[String, Seq[String]]() + var predicateFinder = Map[String, String]() + for (predName <- program.predicates.map(x => x.name)) { + val predEntry = model.entries.get(predName).getOrElse(model.entries.find{ case (x, _) => (x.startsWith(predName ++ "_") && !x.contains("@"))}.getOrElse(ConstantEntry(""))) + if (predEntry.isInstanceOf[MapEntry] && !predEntry.asInstanceOf[MapEntry].options.isEmpty) { + for ((predContent, predId) <- predEntry.asInstanceOf[MapEntry].options) { + predContentMap += (predId.toString -> predContent.map(x => x.toString)) + predicateFinder += (predId.toString -> predName) + } + } + } + var mwContentMap = Map[String, Seq[String]]() + for ((k,v) <- model.entries) { + if (k == "wand" || (k.startsWith("wand" ++ "_") && !k.contains("@"))) { + if (v.isInstanceOf[MapEntry] && !v.asInstanceOf[MapEntry].options.isEmpty) { + for ((mwContent, mwId) <- v.asInstanceOf[MapEntry].options) { + mwContentMap += (mwId.toString -> mwContent.map(x => x.toString)) + } + } + } + } + val permMap = model.entries.get("U_2_real").get.asInstanceOf[MapEntry].options + var res = Seq[(String, BasicHeap)]() + for ((labelName, (labelHeap, labelMask)) <- hmLabels) { + var heapEntrySet = Set[BasicHeapEntry]() + val heapStore = model.entries.get("MapType0Store").get.asInstanceOf[MapEntry].options + val maskStore = model.entries.get("MapType1Store").get.asInstanceOf[MapEntry].options + val heapMap = recursiveBuildHeapMask(heapStore, labelHeap, Map.empty) + val maskMap = recursiveBuildHeapMask(maskStore, labelMask, Map.empty) + val commonKeys = heapMap.keys.toSet.intersect(maskMap.keys.toSet) + for (ck <- commonKeys) { + val value = heapMap.get(ck).get + val perm = maskMap.get(ck).get + val tempPerm: Option[Rational] = detHeapEntryPermission(permMap, perm._1) + val typ: HeapEntryType = detHeapType(model, qpMaskSet, ck(1), perm._2) + if (typ == FieldType || typ == QPFieldType) { + heapEntrySet += BasicHeapEntry(Seq(ck(0)), Seq(ck(1)), value._1, tempPerm, typ, None) + } else if (typ == PredicateType || typ == QPPredicateType) { + heapEntrySet += BasicHeapEntry(Seq(ck(0), ck(1)), predContentMap.get(ck(1)).getOrElse(Seq()), value._1, tempPerm, typ, Some(evalInsidePredicate(value._1, ck(1), predicateFinder, predByName, model))) + } else if (typ == MagicWandType || typ == QPMagicWandType) { + heapEntrySet += BasicHeapEntry(Seq(ck(0), ck(1)), predContentMap.get(ck(1)).getOrElse(Seq()), value._1, tempPerm, typ, None) + } + } + var startNow = false + for ((_, _, heapIdentifier, maskIdentifier) <- hmStates.reverse) { + if (heapIdentifier == labelHeap && maskIdentifier == labelMask) { + startNow = true + } + if (startNow) { + for ((maskKey, perm) <- maskOp) { + val maskId = maskKey(1) + val reference = maskKey(2) + val field = maskKey(3) + if (maskId == maskIdentifier) { + if (!heapEntrySet.exists({ + case bhe => + ((bhe.reference.length > 0) && (bhe.field.length > 0) && (bhe.reference(0) == reference) && (bhe.field(0) == field)) || + ((bhe.reference.length > 1) && (bhe.reference(0) == reference) && (bhe.reference(1) == field)) + })) { + val tempPerm: Option[Rational] = detHeapEntryPermission(permMap, perm) + val typ: HeapEntryType = detHeapType(model, qpMaskSet, field, maskId) + if (typ == FieldType || typ == QPFieldType) { + heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { + case Some(v) => heapEntrySet += BasicHeapEntry(Seq(reference), Seq(field), v, tempPerm, typ, None) + case None => heapEntrySet += BasicHeapEntry(Seq(reference), Seq(field), "#undefined", tempPerm, typ, None) + } + } else if (typ == PredicateType || typ == QPPredicateType) { + heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { + case Some(v) => heapEntrySet += BasicHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), v, tempPerm, typ, Some(evalInsidePredicate(v, field, predicateFinder, predByName, model))) + case None => heapEntrySet += BasicHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), "#undefined", tempPerm, typ, Some(Map[ast.Exp, ModelEntry]())) + } + } else if (typ == MagicWandType || typ == QPMagicWandType) { + heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { + case Some(v) => heapEntrySet += BasicHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), v, tempPerm, typ, None) + case None => heapEntrySet += BasicHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), "#undefined", tempPerm, typ, None) + } + } + } else { + heapEntrySet.find( + { case bhe => (bhe.het == FieldType || bhe.het == QPFieldType) && (bhe.reference(0) == reference) && (bhe.field(0) == field) && (bhe.valueID == "#undefined") } + ) match { + case Some(v) => + heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { + case Some(x) => + heapEntrySet += BasicHeapEntry(Seq(reference), Seq(field), x, v.perm, v.het, None) + heapEntrySet -= BasicHeapEntry(Seq(reference), Seq(field), "#undefined", v.perm, v.het, None) + case None => // + } + case None => // + } + heapEntrySet.find( + { case bhe => (bhe.het == PredicateType || bhe.het == QPPredicateType) && (bhe.reference(0) == reference) && (bhe.reference(1) == field) && (bhe.valueID == "#undefined") } + ) match { + case Some(v) => + heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { + case Some(x) => + heapEntrySet += BasicHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), x, v.perm, v.het, v.insidePredicate) + heapEntrySet -= BasicHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), "#undefined", v.perm, v.het, v.insidePredicate) + case None => // + } + case None => // + } + heapEntrySet.find( + { case bhe => (bhe.het == MagicWandType || bhe.het == QPMagicWandType) && (bhe.reference(0) == reference) && (bhe.reference(1) == field) && (bhe.valueID == "#undefined") } + ) match { + case Some(v) => + heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { + case Some(x) => + heapEntrySet += BasicHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), x, v.perm, v.het, None) + heapEntrySet -= BasicHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), "#undefined", v.perm, v.het, None) + case None => // + } + case None => // + } + } + } + } + } + } + res +:= (labelName, BasicHeap(heapEntrySet)) + } + res + } + + /** + * Evaluate the snapshot of a predicate. + */ + def evalInsidePredicate(insId: String, predId: String, predicateFinder: Map[String, String], predByName: scala.collection.immutable.Map[String, Predicate], model: Model): Map[ast.Exp, ModelEntry] = { + val frameAssign = model.entries.get("FrameFragment") + val frameCombine = model.entries.get("CombineFrames") + var ans = scala.collection.immutable.Map[ast.Exp, ModelEntry]() + if (frameAssign.isDefined && frameAssign.get.isInstanceOf[MapEntry] && frameCombine.isDefined && frameCombine.get.isInstanceOf[MapEntry]) { + val insTerm: Seq[String] = detInsideTerm(frameCombine.get.asInstanceOf[MapEntry].options.map(_.swap), insId, Seq()) + val evaluatedPredTerm = insTerm.map(ent => detInsideValue(frameAssign.get.asInstanceOf[MapEntry].options.map(_.swap), ent)) + val predName = predicateFinder.get(predId) + if (predName.isDefined && predByName.get(predName.get).isDefined) { + val astPred = predByName.get(predName.get) + if (astPred.isDefined && !astPred.get.isAbstract) { + val predBody = astPred.get.body.get + val insPred = insPredToBody(predBody, evaluatedPredTerm) + if (insPred.length > 0 && !(insPred.length == 1 && insPred(0)._2.startsWith("T@U!val!"))) { + var assignedPredBody = scala.collection.immutable.Map[ast.Exp, ModelEntry]() + for ((exp, value) <- insPred) { + if (value.startsWith("T@U!val!") || value.startsWith("(T@U!val!")) { + assignedPredBody += evalBody(exp, UnspecifiedEntry, assignedPredBody) + } else { + assignedPredBody += evalBody(exp, ConstantEntry(value), assignedPredBody) + } + } + ans = assignedPredBody + } + } + } + } + ans + } + + /** + * Compare the snapshot of a predicate to its actual body (accessed through its ast node). + */ + def evalBody(exp: ast.Exp, value: ModelEntry, lookup: Map[ast.Exp, ModelEntry]): (ast.Exp, ModelEntry) = { + exp match { + case ast.FieldAccessPredicate(predAcc, _) => (predAcc, value) + case ast.CondExp(cond, thn, els) => + if (evalExp(cond, lookup)) { + evalBody(thn, value, lookup) + } else { + evalBody(els, value, lookup) + } + case ast.Implies(left, right) => + if (evalExp(left, lookup)) { + evalBody(right, value, lookup) + } else { + (left, ConstantEntry("False")) + } + case _ => (exp, value) + } + } + + def evalExp(exp: ast.Exp, lookup: scala.collection.immutable.Map[ast.Exp, ModelEntry]): Boolean = exp match { + case ast.NeCmp(left, right) => !lookup.getOrElse(left, left.toString()).toString.equalsIgnoreCase(lookup.getOrElse(right, right.toString()).toString) + case ast.EqCmp(left, right) => (lookup.getOrElse(left, ConstantEntry(left.toString())).toString.equalsIgnoreCase(lookup.getOrElse(right, ConstantEntry(right.toString())).toString)) + case _ => false + } + + def insPredToBody(body: ast.Exp, insPred: Seq[String]): Seq[(ast.Exp, String)] = { + if (insPred.length == 0) { + Seq() + } else if (insPred.length == 1) { + Seq((body, insPred(0))) + } else { + if (body.subExps.length == 2) { + Seq((body.subExps(0), insPred(0))) ++ insPredToBody(body.subExps(1), insPred.tail) + } else { + Seq() + } + } + } + + def detInsideValue(framesAssign: Map[ValueEntry, Seq[ValueEntry]], entry: String): String = { + if (framesAssign.contains(ConstantEntry(entry))) { + detInsideValue(framesAssign, framesAssign.get(ConstantEntry(entry)).get(0).toString) + } else { + entry + } + } + + def detInsideTerm(framesCombine: Map[ValueEntry, Seq[ValueEntry]], insId: String, term: Seq[String]): Seq[String] = { + if (framesCombine.contains(ConstantEntry(insId))) { + val newterm = term ++ framesCombine.get(ConstantEntry(insId)).get.map(x => x.toString) + detInsideTerm(framesCombine, newterm(newterm.length-1), newterm) + } else { + term + } + } + + /** + * Determine the type of a heap resource. + */ + def detHeapType(model: Model, qpMaskSet: Set[String], id: String, maskId: String): HeapEntryType = { + var predIdSet = Set[String]() + if (model.entries.get("IsPredicateField").get.isInstanceOf[MapEntry]) { + for ((k, v) <- model.entries.get("IsPredicateField").get.asInstanceOf[MapEntry].options) { + if (v.toString == "true") { + predIdSet += k(0).toString + } + } + } + var mwIdSet = Set[String]() + if (model.entries.get("IsWandField").get.isInstanceOf[MapEntry]) { + for ((k, v) <- model.entries.get("IsWandField").get.asInstanceOf[MapEntry].options) { + if (v.toString == "true") { + mwIdSet += k(0).toString + } + } + } + var typ: HeapEntryType = FieldType + if (predIdSet.contains(id)) { + if (qpMaskSet.contains(maskId)) { + typ = QPPredicateType + } else { + typ = PredicateType + } + } else if (mwIdSet.contains(id)) { + if (qpMaskSet.contains(maskId)) { + typ = QPMagicWandType + } else { + typ = MagicWandType + } + } else { + if (qpMaskSet.contains(maskId)) { + typ = QPFieldType + } + } + typ + } + + def detHeapEntryPermission(permMap: Map[scala.collection.immutable.Seq[ValueEntry], ValueEntry], perm: String): Option[Rational] = { + for ((s, ve) <- permMap) { + if (s(0).toString == perm) { + if (ve.isInstanceOf[ConstantEntry]) { + return Some(Rational.apply(BigInt(ve.asInstanceOf[ConstantEntry].value.toFloat.toInt), BigInt(1))) + } else if (ve.isInstanceOf[ApplicationEntry]) { + val ae = ve.asInstanceOf[ApplicationEntry] + return Some(Rational.apply(BigInt(ae.arguments(0).asInstanceOf[ConstantEntry].value.toFloat.toInt), BigInt(ae.arguments(1).asInstanceOf[ConstantEntry].value.toFloat.toInt))) + } + } + } + None + } + + def recursiveBuildHeapMask(inputMap: Map[scala.collection.immutable.Seq[ValueEntry], ValueEntry], s: String, resultMap: Map[Seq[String], (String, String)]): Map[Seq[String], (String, String)] = { + val entries: Iterable[(Seq[ValueEntry], ValueEntry)] = inputMap.collect { + case (key, value) if value.toString == s && key.length >= 3 => (key, value) + } + if (entries.isEmpty) { + return resultMap + } + entries.foldLeft (resultMap) { + case (accMap, (entry, value)) => + val newStartString = entry(0) + val newKey = entry.tail.init.map(x => x.toString) + var newResultMap = accMap + if (!accMap.contains(newKey)) { + newResultMap += (newKey -> (entry.last.toString, value.toString)) + } + recursiveBuildHeapMask(inputMap, newStartString.toString, newResultMap) + } + } + + /** + * Extracts domains from a program. Only the ones that are used in the program... no generics. + * It also extracts all instances (translates the generics to concrete values). + */ + def getAllDomains(model: Model, program: ast.Program): Seq[BasicDomainEntry] = { + val domains = program.collect { + case a: ast.Domain => a + } + val concreteDoms = program.collect { + case ast.DomainType(n, map) => (n, map) + case d: ast.DomainFuncApp => (d.domainName, d.typVarMap) + }.filterNot(x => containsTypeVar(x._2.values.toSeq)).toSet + val doms = domains.flatMap(x => if (x.typVars == Nil) Seq((x, Map.empty[ast.TypeVar, ast.Type])) else concreteDoms.filter(_._1 == x.name).map(y => (x, y._2))) // changing the typevars to the actual ones + doms.map(x => { + val types = try { + x._1.typVars.map(x._2) + } catch { + case _: Throwable => Seq() + } + val translatedFunctions = x._1.functions.map(y => detFunction(model, y, x._2, Seq(), program, false)) + BasicDomainEntry(x._1.name, types, translatedFunctions) + }).toSeq + } + + def containsTypeVar(s: Seq[ast.Type]): Boolean = s.exists(x => x.isInstanceOf[ast.TypeVar]) + + /** + * Extract all the functions occuring inside of a domain. + */ + def getAllFunctions(model: Model, program: ast.Program, heapInstances: Seq[(String, String, String, String)]): Seq[BasicFunction] = { + val funcs = program.collect { + case f: ast.Function => f + } + funcs.map(x => detFunction(model, x, Map.empty, heapInstances, program, true)).toSeq + } + + /** + * Determine all the inputs and outputs combinations of a function occruing the counterexample model. + */ + def detFunction(model: Model, func: ast.FuncLike, genmap: scala.collection.immutable.Map[ast.TypeVar, ast.Type], heapInst: Seq[(String, String, String, String)], program: ast.Program, hd: Boolean): BasicFunction = { + val fname = func.name + val resTyp: ast.Type = func.typ + val argTyp: Seq[ast.Type] = func.formalArgs.map(x => x.typ) + model.entries.get(fname) match { + case Some(MapEntry(m, els)) => + var options = Map[Seq[String], String]() + if (hd) { + for ((k, v) <- m) { + var hName = k.head.toString + for ((h, _, i, _) <- heapInst) { + if (i == hName) { + hName = h + } + } + options += (Seq(hName) ++ k.tail.map(x => x.toString) -> v.toString) + } + } else { + for ((k, v) <- m) { + options += (k.map(x => x.toString) -> v.toString) + } + } + BasicFunction(fname, argTyp, resTyp, options, els.toString) + case Some(ConstantEntry(t)) => BasicFunction(fname, argTyp, resTyp, Map.empty, t) + case Some(ApplicationEntry(n, args)) => BasicFunction(fname, argTyp, resTyp, Map.empty, ApplicationEntry(n, args).toString) + case Some(x) => BasicFunction(fname, argTyp, resTyp, Map.empty, x.toString) + case None => BasicFunction(fname, argTyp, resTyp, Map.empty, "#undefined") + } + } + +} + +object CounterexampleGenerator { + /** + * Combine a local variable with its ast node. + */ + def detStore(store: Seq[Declaration], variables: Seq[CEVariable], collections: Set[CEValue]): (StoreCounterexample, Map[String, (String, Int)]) = { + var refOccurences = Map[String, (String, Int)]() + var ans = Seq[StoreEntry]() + for (k <- store) { + if (k.isInstanceOf[ast.LocalVarDecl]) { + val v = k.asInstanceOf[ast.LocalVarDecl] + for (vari <- variables) { + if (v.name == vari.name) { + if (v.typ == ast.Ref) { + if (refOccurences.get(vari.entryValue.toString).isDefined) { + val (n, i) = refOccurences.get(vari.entryValue.toString).get + if (n != v.name) { + refOccurences += (vari.entryValue.toString -> (v.name, i + 1)) + } + } else { + refOccurences += (vari.entryValue.toString -> (v.name, 1)) + } + } + var found = false + for (coll <- collections) { + if (vari.entryValue.toString == coll.id) { + ans +:= StoreEntry(ast.LocalVar(v.name, v.typ)(), coll) + found = true + } + } + if (!found) { + ans +:= StoreEntry(ast.LocalVar(v.name, v.typ)(), vari) + } + } + } + } + } + (StoreCounterexample(ans), refOccurences) + } + + /** + * Match the collection type for the "extended" CE. + */ + def detTranslationMap(store: StoreCounterexample, fields: Map[String, (String, Int)]): Map[String, String] = { + var namesTranslation = Map[String, String]() + for (ent <- store.storeEntries) { + ent.entry match { + case CEVariable(internalName, entryValue, _) => namesTranslation += (entryValue.toString -> ent.id.name) + case CESequence(internalName, _, _, _, _) => namesTranslation += (internalName -> (ent.id.name + " (Seq)")) + case CESet(internalName, _, _, _, _) => namesTranslation += (internalName -> (ent.id.name + " (Set)")) + case CEMultiset(internalName, _, _, _) => namesTranslation += (internalName -> (ent.id.name + " (MultiSet)")) + } + } + for ((k, v) <- fields) { + if (v._2 == 1) { + namesTranslation += (k -> v._1) + } + } + namesTranslation + } + + /** + * Match heap resources to their ast node and translate all identifiers (for fields and references) + */ + def detHeap(opMapping: Map[Seq[String], String], basicHeap: BasicHeap, program: Program, collections: Set[CEValue], translNames: Map[String, String], model: Model): HeapCounterexample = { + // choosing all the needed values from the Boogie Model + var usedIdent = Map[String, Member]() + for ((key, value) <- opMapping) { + for (fie <- program.fields) { + if (key(0) == fie.name || (key(0).startsWith(fie.name ++ "_") && !key.contains("@"))) { + usedIdent += (value -> fie) + } + } + for (pred <- program.predicates) { + if (key(0) == pred.name || (key(0).startsWith(pred.name ++ "_") && !key.contains("@"))) { + usedIdent += (value -> pred) + } + } + } + + var ans = Seq[(Resource, FinalHeapEntry)]() + for (bhe <- basicHeap.basicHeapEntries) { + bhe.het match { + case FieldType | QPFieldType=> + if (!bhe.perm.isDefined || !(bhe.perm.get == Rational.zero)) { + usedIdent.get(bhe.field(0)) match { + case Some(f) => + val fi = f.asInstanceOf[Field] + var found = false + for (coll <- collections) { + if (bhe.valueID == coll.id) { + if (translNames.get(bhe.reference.head).isDefined) { + ans +:= (fi, FieldFinalEntry(translNames.get(bhe.reference.head).get, fi.name, coll, bhe.perm, fi.typ, bhe.het)) + } else { + ans +:= (fi, FieldFinalEntry(bhe.reference.head, fi.name, coll, bhe.perm, fi.typ, bhe.het)) + } + found = true + } + } + if (!found) { + if (translNames.get(bhe.reference.head).isDefined) { + ans +:= (fi, FieldFinalEntry(translNames.get(bhe.reference.head).get, fi.name, CEVariable("#undefined", ConstantEntry(bhe.valueID), Some(fi.typ)), bhe.perm, fi.typ, bhe.het)) + } else { + ans +:= (fi, FieldFinalEntry(bhe.reference.head, fi.name, CEVariable("#undefined", ConstantEntry(bhe.valueID), Some(fi.typ)), bhe.perm, fi.typ, bhe.het)) + } + } + case None => println(s"Could not find a field node for: ${bhe.toString}") + } + } + case PredicateType | QPPredicateType => + usedIdent.get(bhe.reference(1)) match { + case Some(p) => + val pr = p.asInstanceOf[Predicate] + val refNames = bhe.field.map(x => + if (translNames.get(x).isDefined) { + translNames.get(x).get + } else { + x + }) + ans +:= (pr, PredFinalEntry(pr.name, refNames, bhe.perm, bhe.insidePredicate, bhe.het)) + case None => println(s"Could not find a predicate node for: ${bhe.toString}") + } + case MagicWandType | QPMagicWandType => + val translatedArgs = bhe.field.map(x => translNames.getOrElse(x, x)) + for ((mw, idx) <- program.magicWandStructures.zipWithIndex) { + val mwStructure = mw.structure(program, true) + val replacements: Iterable[(ast.Node, ast.Node)] = mwStructure.subexpressionsToEvaluate(program).zip(translatedArgs).map(e => e._1 -> ast.LocalVar(e._2, e._1.typ)()) + val repl: scala.collection.immutable.Map[ast.Node, ast.Node] = scala.collection.immutable.Map.from(replacements) + val transformed = mwStructure.replace(repl) + if (idx == 0) { + if (model.entries.get("wand").isDefined && model.entries.get("wand").get.isInstanceOf[MapEntry]) { + for (s <- model.entries.get("wand").get.asInstanceOf[MapEntry].options) { + if (s._2.toString == bhe.reference(1)) { + ans +:= (mw.res(program), WandFinalEntry("wand", transformed.left, transformed.right, scala.collection.immutable.Map[String, String](), bhe.perm, bhe.het)) + } + } + } + } else { + val wandName = "wand_" ++ idx.toString + if (model.entries.get(wandName).isDefined && model.entries.get(wandName).get.isInstanceOf[MapEntry]) { + for (s <- model.entries.get(wandName).get.asInstanceOf[MapEntry].options) { + if (s._2.toString == bhe.reference(1)) { + ans +:= (mw, WandFinalEntry(wandName, transformed.left, transformed.right, scala.collection.immutable.Map[String, String](), bhe.perm, bhe.het)) + } + } + } + } + } + case _ => println("This type of heap entry could not be matched correctly!") + } + } + HeapCounterexample(ans) + } + + def detTranslatedDomains(domEntries: Seq[BasicDomainEntry], namesMap: Map[String, String]) : Seq[BasicDomainEntry] = { + domEntries.map(de => BasicDomainEntry(de.name, de.types, detTranslatedFunctions(de.functions, namesMap))) + } + + def detTranslatedFunctions(funEntries: Seq[BasicFunction], namesMap: Map[String, String]) : Seq[BasicFunction] = { + funEntries.map(bf => detNameTranslationOfFunction(bf, namesMap)) + } + + def detNameTranslationOfFunction(fun: BasicFunction, namesMap: Map[String, String]) : BasicFunction = { + var tempMap = Map[String, String]() + for ((k,v) <- namesMap) { + if (k.startsWith("T@U!val!")) { + tempMap += (k -> v) + } + } + val translatedFun = fun.options.map { case (in, out) => + (in.map(intName => tempMap.getOrElse(intName, intName)), tempMap.getOrElse(out, out)) + } + val translatedEls = tempMap.getOrElse(fun.default, fun.default) + BasicFunction(fun.fname, fun.argtypes, fun.returnType, translatedFun, translatedEls) + } + + def transformInteremdiateCounterexample(e: AbstractError, names: Map[String, Map[String, String]], program: Program, wandNames: Option[Map[MagicWandStructure.MagicWandStructure, Func]]): Unit = { + if (e.isInstanceOf[VerificationError] && ErrorMemberMapping.mapping.contains(e.asInstanceOf[VerificationError].readableMessage(true, true))) { + e.asInstanceOf[VerificationError].failureContexts = scala.collection.immutable.Seq(FailureContextImpl(Some(CounterexampleGenerator(e, names, program, wandNames).imCE))) + } + } + + def transformExtendedCounterexample(e: AbstractError, names: Map[String, Map[String, String]], program: Program, wandNames: Option[Map[MagicWandStructure.MagicWandStructure, Func]]): Unit = { + if (e.isInstanceOf[VerificationError] && ErrorMemberMapping.mapping.contains(e.asInstanceOf[VerificationError].readableMessage(true, true))) { + e.asInstanceOf[VerificationError].failureContexts = scala.collection.immutable.Seq(FailureContextImpl(Some(CounterexampleGenerator(e, names, program, wandNames)))) + } + } +} \ No newline at end of file diff --git a/src/main/scala/viper/carbon/boogie/boogie.scala b/src/main/scala/viper/carbon/boogie/boogie.scala index 894cb63f..b0e3286c 100644 --- a/src/main/scala/viper/carbon/boogie/boogie.scala +++ b/src/main/scala/viper/carbon/boogie/boogie.scala @@ -314,7 +314,7 @@ case class AssertImpl(exp: Exp, error: VerificationError) extends Stmt { object ErrorMemberMapping { // The "weak" hash map is necessary to avoid leaking memory. // See issue https://github.com/viperproject/carbon/issues/444 - val mapping = mutable.WeakHashMap[VerificationError, Member]() + val mapping = mutable.HashMap[String, Member]() var currentMember : Member = null } object Assert { @@ -322,7 +322,7 @@ object Assert { if (error == null) Statements.EmptyStmt else { if (ErrorMemberMapping.currentMember != null) { - ErrorMemberMapping.mapping.update(error, ErrorMemberMapping.currentMember) + ErrorMemberMapping.mapping.update(error.readableMessage(true, true), ErrorMemberMapping.currentMember) } AssertImpl(exp, error) } diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala index 720f38d3..3dba1da0 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala @@ -28,7 +28,7 @@ DefaultWandModule(val verifier: Verifier) extends WandModule with StmtComponent //wands stored type WandShape = Func //This needs to be resettable, which is why "lazy val" is not used. See also: wandToShapes method - private var lazyWandToShapes: Option[Map[MagicWandStructure.MagicWandStructure, WandShape]] = None + /* private */ var lazyWandToShapes: Option[Map[MagicWandStructure.MagicWandStructure, WandShape]] = None /** CONSTANTS FOR TRANSFER START**/ /* denotes amount of permission to add/remove during a specific transfer */ diff --git a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala index 2f24baf8..9d664ba3 100644 --- a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala +++ b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala @@ -62,6 +62,7 @@ trait BoogieInterface { "/proverOpt:O:smt.QI.EAGER_THRESHOLD=100", "/proverOpt:O:smt.BV.REFLECT=true", "/proverOpt:O:smt.qi.max_multi_patterns=1000", + "/proverOpt:O:MODEL.PARTIAL=true", s"/proverOpt:PROVER_PATH=$z3Path") /** The (resolved) path where Boogie is supposed to be located. */ From e220e674708631d23aa5d0d2877c0789efecb492 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Mon, 1 Sep 2025 15:59:34 +0200 Subject: [PATCH 2/9] Adapting to silver changes --- silver | 2 +- .../scala/viper/carbon/CarbonGeneralCounterexampleTests.scala | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/silver b/silver index 062f25c4..5e1fda95 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 062f25c4285e0dd700d6e61e43573026f339fd96 +Subproject commit 5e1fda95105708c4a64afc011f9cc7d3f21ac134 diff --git a/src/test/scala/viper/carbon/CarbonGeneralCounterexampleTests.scala b/src/test/scala/viper/carbon/CarbonGeneralCounterexampleTests.scala index 1e2c8b1b..34fbdfa9 100644 --- a/src/test/scala/viper/carbon/CarbonGeneralCounterexampleTests.scala +++ b/src/test/scala/viper/carbon/CarbonGeneralCounterexampleTests.scala @@ -12,7 +12,7 @@ import java.nio.file.Path class GeneralCounterexampleTests extends AllTests { - override val testDirectories: Seq[String] = Seq("counterexamples") + override val testDirectories: Seq[String] = Seq("counterexample_mapped", "counterexample_general") override val commandLineArguments: Seq[String] = Seq("--counterexample=extended") From 3c76c3e3908f0f951480c8b5241ce096f2cca69a Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Mon, 13 Jul 2026 16:16:12 +0200 Subject: [PATCH 3/9] Adapting to new model names and format --- silver | 2 +- .../scala/viper/carbon/CarbonVerifier.scala | 20 +- ...ala => CarbonResolvedCounterexample.scala} | 181 ++++++++---------- .../CarbonGeneralCounterexampleTests.scala | 2 +- 4 files changed, 88 insertions(+), 117 deletions(-) rename src/main/scala/viper/carbon/boogie/{CarbonExtendedCounterexample.scala => CarbonResolvedCounterexample.scala} (87%) diff --git a/silver b/silver index 5e1fda95..2dbce504 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 5e1fda95105708c4a64afc011f9cc7d3f21ac134 +Subproject commit 2dbce504f68c0e8d58e94dc80c85f145eb6aeeaf diff --git a/src/main/scala/viper/carbon/CarbonVerifier.scala b/src/main/scala/viper/carbon/CarbonVerifier.scala index 44bb9e07..c53ea83d 100644 --- a/src/main/scala/viper/carbon/CarbonVerifier.scala +++ b/src/main/scala/viper/carbon/CarbonVerifier.scala @@ -6,7 +6,7 @@ package viper.carbon -import boogie.{BoogieModelTransformer, CarbonExtendedCounterexample, Namespace} +import boogie.{BoogieModelTransformer, CarbonResolvedCounterexample, Namespace} import modules.impls._ import viper.silver.ast.{MagicWand, Program, Quasihavoc, Quasihavocall} import viper.silver.utility.Paths @@ -14,7 +14,7 @@ import viper.silver.verifier._ import verifier.{BoogieDependency, BoogieInterface, Verifier} import java.io.{BufferedOutputStream, File, FileOutputStream, IOException} -import viper.silver.frontend.{ExtendedModel, IntermediateModel, MissingDependencyException, NativeModel, VariablesModel} +import viper.silver.frontend.{ResolvedModel, RawModel, MissingDependencyException, NativeModel, VariablesModel} import viper.silver.reporter.Reporter /** @@ -177,13 +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 + var rawCounterexample = false + var resolvedCounterexample = 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 Some(RawModel) => rawCounterexample = true + case Some(ResolvedModel) => resolvedCounterexample = true case None => case Some(v) => sys.error("Invalid option: " + v) } @@ -247,11 +247,11 @@ 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 rawCounterexample => { + errors.foreach(e => CarbonResolvedCounterexample.transformRawCounterexample(e, translatedNames, program, wandModule.lazyWandToShapes)) } - case Failure(errors) if extendedCounterexample => { - errors.foreach(e => CarbonExtendedCounterexample.transformExtendedCounterexample(e, translatedNames, program, wandModule.lazyWandToShapes)) + case Failure(errors) if resolvedCounterexample => { + errors.foreach(e => CarbonResolvedCounterexample.transformResolvedCounterexample(e, translatedNames, program, wandModule.lazyWandToShapes)) } case _ => result } diff --git a/src/main/scala/viper/carbon/boogie/CarbonExtendedCounterexample.scala b/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala similarity index 87% rename from src/main/scala/viper/carbon/boogie/CarbonExtendedCounterexample.scala rename to src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala index b673f0af..4831613c 100644 --- a/src/main/scala/viper/carbon/boogie/CarbonExtendedCounterexample.scala +++ b/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala @@ -17,24 +17,24 @@ import viper.silver.ast.{Declaration, MagicWandStructure, Program, Type} /** * CounterexampleGenerator class used for generating an "extended" CE. */ -case class CarbonExtendedCounterexample(e: AbstractError, +case class CarbonResolvedCounterexample(e: AbstractError, names: Map[String, Map[String, String]], program: Program, - wandNames: Option[Map[MagicWandStructure.MagicWandStructure, Func]]) extends Counterexample with ExtendedCounterexample { + wandNames: Option[Map[MagicWandStructure.MagicWandStructure, Func]]) extends Counterexample with ResolvedCounterexample { val ve = e.asInstanceOf[VerificationError] val errorMethod = ErrorMemberMapping.mapping(ve.readableMessage(true, true)) - val imCE = CarbonIntermediateCounterexample(ve, errorMethod, names, program, wandNames) - val model = imCE.originalEntries + val rawCE = CarbonRawCounterexample(ve, errorMethod, names, program, wandNames) + val model = rawCE.originalEntries - val (ceStore, refOcc) = CarbonExtendedCounterexample.detStore(program.methodsByName(errorMethod.name).transitiveScopedDecls, imCE.basicVariables, imCE.allCollections) - val nameTranslationMap = CarbonExtendedCounterexample.detTranslationMap(ceStore, refOcc) - val ceHeaps = imCE.allBasicHeaps.map(bh => (bh._1, CarbonExtendedCounterexample.detHeap(imCE.workingModel, bh._2, program, imCE.allCollections, nameTranslationMap, imCE.originalEntries))).reverse + val (ceStore, refOcc) = CarbonResolvedCounterexample.detStore(program.methodsByName(errorMethod.name).transitiveScopedDecls, rawCE.basicVariables, rawCE.allCollections) + val nameTranslationMap = CarbonResolvedCounterexample.detTranslationMap(rawCE.basicVariables, rawCE.allCollections, refOcc) + val ceHeaps = rawCE.allBasicHeaps.map(bh => (bh._1, CarbonResolvedCounterexample.detHeap(rawCE.workingModel, bh._2, program, rawCE.allCollections, nameTranslationMap, rawCE.originalEntries))).reverse - override val domainEntries: Seq[BasicDomainEntry] = CarbonExtendedCounterexample.detTranslatedDomains(imCE.domainEntries, nameTranslationMap) - override val functionEntries: Seq[BasicFunctionEntry] = CarbonExtendedCounterexample.detTranslatedFunctions(imCE.nonDomainFunctions, nameTranslationMap) + override val domainEntries: Seq[BasicDomainEntry] = CarbonResolvedCounterexample.detTranslatedDomains(rawCE.domainEntries, nameTranslationMap) + override val functionEntries: Seq[BasicFunctionEntry] = CarbonResolvedCounterexample.detTranslatedFunctions(rawCE.nonDomainFunctions, nameTranslationMap) override def toString: String = { - var finalString = " Extended Counterexample: \n" + var finalString = " Resolved Counterexample: \n" finalString += " Store: \n" if (!ceStore.storeEntries.isEmpty) finalString += ceStore.storeEntries.map(x => x.toString).mkString("", "\n", "\n") @@ -51,30 +51,30 @@ case class CarbonExtendedCounterexample(e: AbstractError, /** * CounterexampleGenerator class used for generating an "intermediate" CE. */ -case class CarbonIntermediateCounterexample(ve: VerificationError, +case class CarbonRawCounterexample(ve: VerificationError, errorMethod: Member, names: Map[String, Map[String, String]], program: Program, - wandNames: Option[Map[MagicWandStructure.MagicWandStructure, Func]]) extends Counterexample with IntermediateCounterexample { + wandNames: Option[Map[MagicWandStructure.MagicWandStructure, Func]]) extends Counterexample with RawCounterexample { val originalEntries = ve.failureContexts(0).counterExample.get.model val model = originalEntries val typenamesInMethod = names.get(errorMethod.name).get.map(e => e._2 -> e._1) val methodVarDecl = program.methodsByName.get(errorMethod.name).get.transitiveScopedDecls - val (basicVariables, otherDeclarations) = CarbonIntermediateCounterexample.detCEvariables(originalEntries.entries, typenamesInMethod, methodVarDecl) - val allSequences = CarbonIntermediateCounterexample.detSequences(originalEntries) - val allSets = CarbonIntermediateCounterexample.detSets(originalEntries) - val allMultisets = CarbonIntermediateCounterexample.detMultisets(originalEntries) + val (basicVariables, otherDeclarations) = CarbonRawCounterexample.detCEvariables(originalEntries.entries, typenamesInMethod, methodVarDecl) + val allSequences = CarbonRawCounterexample.detSequences(originalEntries) + val allSets = CarbonRawCounterexample.detSets(originalEntries) + val allMultisets = CarbonRawCounterexample.detMultisets(originalEntries) - val workingModel = CarbonIntermediateCounterexample.buildNewModel(originalEntries.entries) - val (hmLabels, hmStates) = CarbonIntermediateCounterexample.oldAndReturnHeapMask(workingModel, otherDeclarations) - val allBasicHeaps = CarbonIntermediateCounterexample.detHeaps(workingModel, hmStates, originalEntries, hmLabels, program).map{case (n, bh) => if (n == "return") ("current", bh) else (n, bh)} + val workingModel = CarbonRawCounterexample.buildNewModel(originalEntries.entries) + val (hmLabels, hmStates) = CarbonRawCounterexample.oldAndReturnHeapMask(workingModel, otherDeclarations) + val allBasicHeaps = CarbonRawCounterexample.detHeaps(workingModel, hmStates, originalEntries, hmLabels, program).map{case (n, bh) => if (n == "return") ("current", bh) else (n, bh)} - val domainEntries = CarbonIntermediateCounterexample.getAllDomains(originalEntries, program) - val nonDomainFunctions = CarbonIntermediateCounterexample.getAllFunctions(originalEntries, program, hmStates) + val domainEntries = CarbonRawCounterexample.getAllDomains(originalEntries, program) + val nonDomainFunctions = CarbonRawCounterexample.getAllFunctions(originalEntries, program, hmStates) override def toString: String = { - var finalString = " Intermediate Counterexample: \n" + var finalString = " Raw Counterexample: \n" finalString ++= " Local Information:\n" if (!basicVariables.isEmpty) finalString += basicVariables.map(x => x.toString).mkString("", "\n", "\n") @@ -92,7 +92,7 @@ case class CarbonIntermediateCounterexample(ve: VerificationError, } } -object CarbonIntermediateCounterexample { +object CarbonRawCounterexample { /** * Determines the local variables and their value. */ @@ -109,7 +109,7 @@ object CarbonIntermediateCounterexample { if (entry.isInstanceOf[MapEntry]) { ent = entry.asInstanceOf[MapEntry].options.head._1(0) } - res +:= CEVariable(v.name, ent, Some(v.typ)) + res +:= CEVariable(v.name, CounterexampleValue.literal(ent.toString, Some(v.typ)), Some(v.typ)) } } else { otherDeclarations +:= temp @@ -119,7 +119,7 @@ object CarbonIntermediateCounterexample { if (originalEntries.contains("null")) { val nullRef = originalEntries.get("null").get if (nullRef.isInstanceOf[ConstantEntry]) { - res +:= CEVariable("null", nullRef, Some(ast.Ref)) + res +:= CEVariable("null", CounterexampleValue.literal(nullRef.toString, Some(ast.Ref)), Some(ast.Ref)) } } (res, otherDeclarations) @@ -170,7 +170,7 @@ object CarbonIntermediateCounterexample { /** * Generates the sequences of the CE. */ - def detSequences(model: Model): Seq[CEValue] = { + def detSequences(model: Model): Seq[CECollection] = { var res = Map[String, Seq[String]]() var tempMap = Map[(String, Seq[String]), String]() for ((opName, opValues) <- model.entries) { @@ -253,22 +253,13 @@ object CarbonIntermediateCounterexample { } } } - var ans = Seq[CEValue]() + var ans = Seq[CECollection]() res.foreach { case (n, s) => - val typ: Option[Type] = detASTTypeFromString(n.replaceAll(".*?<(.*)>.*", "$1")) match { - case Some(x) => Some(ast.SeqType(x)) - case None => None - } - var entries = Map[BigInt, String]() - var counter = 0 - for (e <- s) { - if (e != "#undefined") { - entries += (BigInt(counter) -> e) - } - counter += 1 - } - ans +:= CESequence(n, BigInt(s.length), entries, s, typ) + val elemTyp: Option[Type] = detASTTypeFromString(n.replaceAll(".*?<(.*)>.*", "$1")) + val elems = s.map(e => CounterexampleValue.literal(e, elemTyp)) + val value = if (elems.isEmpty) ast.EmptySeq(elemTyp.getOrElse(ast.InternalType))() else ast.ExplicitSeq(elems)() + ans +:= CECollection(n, value) } ans } @@ -276,7 +267,7 @@ object CarbonIntermediateCounterexample { /** * Generates the sets of the CE. */ - def detSets(model: Model): Seq[CEValue] = { + def detSets(model: Model): Seq[CECollection] = { var res = Map[String, Set[String]]() for ((opName, opValues) <- model.entries) { if (opName == "Set#Empty") { @@ -386,20 +377,13 @@ object CarbonIntermediateCounterexample { } } } - var ans = Seq[CEValue]() + var ans = Seq[CECollection]() res.foreach { case (n, s) => - val typ: Option[Type] = detASTTypeFromString(n.replaceAll(".*?<(.*)>.*", "$1")) match { - case Some(x) => Some(ast.SetType(x)) - case None => None - } - var containment = Map[String, Boolean]() - for (e <- s) { - if (e != "#undefined") { - containment += (e -> true) - } - } - ans +:= CESet(n, BigInt(s.size), containment, s, typ) + val elemTyp: Option[Type] = detASTTypeFromString(n.replaceAll(".*?<(.*)>.*", "$1")) + val elems = s.filter(_ != "#undefined").toSeq.map(e => CounterexampleValue.literal(e, elemTyp)) + val value = if (elems.isEmpty) ast.EmptySet(elemTyp.getOrElse(ast.InternalType))() else ast.ExplicitSet(elems)() + ans +:= CECollection(n, value) } ans } @@ -407,7 +391,7 @@ object CarbonIntermediateCounterexample { /** * Generates the multisets of the CE. */ - def detMultisets(model: Model): Seq[CEValue] = { + def detMultisets(model: Model): Seq[CECollection] = { var res = Map[String, Map[String, Int]]() for ((opName, opValues) <- model.entries) { if (opName == "MultiSet#Empty") { @@ -500,15 +484,13 @@ object CarbonIntermediateCounterexample { } } } - var ans = Seq[CEValue]() + var ans = Seq[CECollection]() res.foreach { case (n, s) => - val typ: Option[Type] = detASTTypeFromString(n.replaceAll(".*?<(.*)>.*", "$1")) match { - case Some(x) => Some(ast.SetType(x)) - case None => None - } - val size = s.values.sum - ans +:= CEMultiset(n, BigInt(size), s, typ) + val elemTyp: Option[Type] = detASTTypeFromString(n.replaceAll(".*?<(.*)>.*", "$1")) + val elems = s.toSeq.flatMap { case (e, count) => Seq.fill(count)(CounterexampleValue.literal(e, elemTyp)) } + val value = if (elems.isEmpty) ast.EmptyMultiset(elemTyp.getOrElse(ast.InternalType))() else ast.ExplicitMultiset(elems)() + ans +:= CECollection(n, value) } ans } @@ -1014,11 +996,11 @@ object CarbonIntermediateCounterexample { } -object CarbonExtendedCounterexample { +object CarbonResolvedCounterexample { /** * Combine a local variable with its ast node. */ - def detStore(store: Seq[Declaration], variables: Seq[CEVariable], collections: Seq[CEValue]): (StoreCounterexample, Map[String, (String, Int)]) = { + def detStore(store: Seq[Declaration], variables: Seq[CEVariable], collections: Seq[CECollection]): (StoreCounterexample, Map[String, (String, Int)]) = { var refOccurences = Map[String, (String, Int)]() var ans = Seq[StoreEntry]() for (k <- store) { @@ -1027,24 +1009,24 @@ object CarbonExtendedCounterexample { for (vari <- variables) { if (v.name == vari.name) { if (v.typ == ast.Ref) { - if (refOccurences.get(vari.entryValue.toString).isDefined) { - val (n, i) = refOccurences.get(vari.entryValue.toString).get + if (refOccurences.get(vari.value.toString).isDefined) { + val (n, i) = refOccurences.get(vari.value.toString).get if (n != v.name) { - refOccurences += (vari.entryValue.toString -> (v.name, i + 1)) + refOccurences += (vari.value.toString -> (v.name, i + 1)) } } else { - refOccurences += (vari.entryValue.toString -> (v.name, 1)) + refOccurences += (vari.value.toString -> (v.name, 1)) } } var found = false for (coll <- collections) { - if (vari.entryValue.toString == coll.id) { - ans +:= StoreEntry(ast.LocalVar(v.name, v.typ)(), coll) + if (vari.value.toString == coll.id) { + ans +:= StoreEntry(ast.LocalVar(v.name, v.typ)(), coll.value) found = true } } if (!found) { - ans +:= StoreEntry(ast.LocalVar(v.name, v.typ)(), vari) + ans +:= StoreEntry(ast.LocalVar(v.name, v.typ)(), vari.value) } } } @@ -1056,14 +1038,20 @@ object CarbonExtendedCounterexample { /** * Match the collection type for the "extended" CE. */ - def detTranslationMap(store: StoreCounterexample, fields: Map[String, (String, Int)]): Map[String, String] = { + def detTranslationMap(variables: Seq[CEVariable], collections: Seq[CECollection], fields: Map[String, (String, Int)]): Map[String, String] = { var namesTranslation = Map[String, String]() - for (ent <- store.storeEntries) { - ent.entry match { - case CEVariable(internalName, entryValue, _) => namesTranslation += (entryValue.toString -> ent.id.name) - case CESequence(internalName, _, _, _, _) => namesTranslation += (internalName -> (ent.id.name + " (Seq)")) - case CESet(internalName, _, _, _, _) => namesTranslation += (internalName -> (ent.id.name + " (Set)")) - case CEMultiset(internalName, _, _, _) => namesTranslation += (internalName -> (ent.id.name + " (MultiSet)")) + for (vari <- variables) { + collections.find(_.id == vari.value.toString) match { + case Some(coll) => + val suffix = vari.typ match { + case Some(_: ast.SeqType) => " (Seq)" + case Some(_: ast.SetType) => " (Set)" + case Some(_: ast.MultisetType) => " (MultiSet)" + case _ => "" + } + namesTranslation += (coll.id -> (vari.name + suffix)) + case None => + namesTranslation += (vari.value.toString -> vari.name) } } for ((k, v) <- fields) { @@ -1077,7 +1065,7 @@ object CarbonExtendedCounterexample { /** * Match heap resources to their ast node and translate all identifiers (for fields and references) */ - def detHeap(opMapping: Map[Seq[String], String], basicHeap: BasicHeap, program: Program, collections: Seq[CEValue], translNames: Map[String, String], model: Model): HeapCounterexample = { + def detHeap(opMapping: Map[Seq[String], String], basicHeap: BasicHeap, program: Program, collections: Seq[CECollection], translNames: Map[String, String], model: Model): HeapCounterexample = { // choosing all the needed values from the Boogie Model var usedIdent = Map[String, Member]() for ((key, value) <- opMapping) { @@ -1101,23 +1089,11 @@ object CarbonExtendedCounterexample { usedIdent.get(bhe.field(0)) match { case Some(f) => val fi = f.asInstanceOf[Field] - var found = false - for (coll <- collections) { - if (bhe.valueID == coll.id) { - if (false && translNames.get(bhe.reference.head).isDefined) { - ans +:= (fi, FieldFinalEntry(translNames.get(bhe.reference.head).get, fi.name, coll, bhe.perm, fi.typ, bhe.het)) - } else { - ans +:= (fi, FieldFinalEntry(bhe.reference.head, fi.name, coll, bhe.perm, fi.typ, bhe.het)) - } - found = true - } - } - if (!found) { - if (false && translNames.get(bhe.reference.head).isDefined) { - ans +:= (fi, FieldFinalEntry(translNames.get(bhe.reference.head).get, fi.name, CEVariable("#undefined", ConstantEntry(bhe.valueID), Some(fi.typ)), bhe.perm, fi.typ, bhe.het)) - } else { - ans +:= (fi, FieldFinalEntry(bhe.reference.head, fi.name, CEVariable("#undefined", ConstantEntry(bhe.valueID), Some(fi.typ)), bhe.perm, fi.typ, bhe.het)) - } + collections.find(_.id == bhe.valueID) match { + case Some(coll) => + ans +:= (fi, FieldFinalEntry(bhe.reference.head, fi.name, coll.value, bhe.perm, fi.typ, bhe.het)) + case None => + ans +:= (fi, FieldFinalEntry(bhe.reference.head, fi.name, CounterexampleValue.literal(bhe.valueID, Some(fi.typ)), bhe.perm, fi.typ, bhe.het)) } case None => println(s"Could not find a field node for: ${bhe.toString}") @@ -1127,12 +1103,7 @@ object CarbonExtendedCounterexample { usedIdent.get(bhe.reference(1)) match { case Some(p) => val pr = p.asInstanceOf[Predicate] - val refNames = bhe.field.map(x => - if (false && translNames.get(x).isDefined) { - translNames.get(x).get - } else { - x - }) + val refNames = bhe.field ans +:= (pr, PredFinalEntry(pr.name, refNames, bhe.perm, bhe.insidePredicate, bhe.het)) case None => println(s"Could not find a predicate node for: ${bhe.toString}") @@ -1191,15 +1162,15 @@ object CarbonExtendedCounterexample { BasicFunctionEntry(fun.fname, fun.argtypes, fun.returnType, translatedFun, translatedEls) } - def transformInteremdiateCounterexample(e: AbstractError, names: Map[String, Map[String, String]], program: Program, wandNames: Option[Map[MagicWandStructure.MagicWandStructure, Func]]): Unit = { + def transformRawCounterexample(e: AbstractError, names: Map[String, Map[String, String]], program: Program, wandNames: Option[Map[MagicWandStructure.MagicWandStructure, Func]]): Unit = { if (e.isInstanceOf[VerificationError] && ErrorMemberMapping.mapping.contains(e.asInstanceOf[VerificationError].readableMessage(true, true))) { - e.asInstanceOf[VerificationError].failureContexts = scala.collection.immutable.Seq(FailureContextImpl(Some(CarbonExtendedCounterexample(e, names, program, wandNames).imCE))) + e.asInstanceOf[VerificationError].failureContexts = scala.collection.immutable.Seq(FailureContextImpl(Some(CarbonResolvedCounterexample(e, names, program, wandNames).rawCE))) } } - def transformExtendedCounterexample(e: AbstractError, names: Map[String, Map[String, String]], program: Program, wandNames: Option[Map[MagicWandStructure.MagicWandStructure, Func]]): Unit = { + def transformResolvedCounterexample(e: AbstractError, names: Map[String, Map[String, String]], program: Program, wandNames: Option[Map[MagicWandStructure.MagicWandStructure, Func]]): Unit = { if (e.isInstanceOf[VerificationError] && ErrorMemberMapping.mapping.contains(e.asInstanceOf[VerificationError].readableMessage(true, true))) { - e.asInstanceOf[VerificationError].failureContexts = scala.collection.immutable.Seq(FailureContextImpl(Some(CarbonExtendedCounterexample(e, names, program, wandNames)))) + e.asInstanceOf[VerificationError].failureContexts = scala.collection.immutable.Seq(FailureContextImpl(Some(CarbonResolvedCounterexample(e, names, program, wandNames)))) } } } \ No newline at end of file diff --git a/src/test/scala/viper/carbon/CarbonGeneralCounterexampleTests.scala b/src/test/scala/viper/carbon/CarbonGeneralCounterexampleTests.scala index 34fbdfa9..43fc4127 100644 --- a/src/test/scala/viper/carbon/CarbonGeneralCounterexampleTests.scala +++ b/src/test/scala/viper/carbon/CarbonGeneralCounterexampleTests.scala @@ -15,7 +15,7 @@ class GeneralCounterexampleTests extends AllTests { override val testDirectories: Seq[String] = Seq("counterexample_mapped", "counterexample_general") override val commandLineArguments: Seq[String] = - Seq("--counterexample=extended") + Seq("--counterexample=resolved") override def buildTestInput(file: Path, prefix: String): DefaultAnnotatedTestInput = { CounterexampleTestInput(file, prefix) From 1190c2aa7be119e3cceb76ae32681c93da4bed86 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Mon, 13 Jul 2026 16:47:41 +0200 Subject: [PATCH 4/9] Adapt to new wand model --- silver | 2 +- .../boogie/CarbonResolvedCounterexample.scala | 27 ++++--------------- 2 files changed, 6 insertions(+), 23 deletions(-) diff --git a/silver b/silver index 2dbce504..59fa417d 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 2dbce504f68c0e8d58e94dc80c85f145eb6aeeaf +Subproject commit 59fa417ddc38ae8813746e8f6cded8ab12d05e42 diff --git a/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala b/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala index 4831613c..1e9519a7 100644 --- a/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala +++ b/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala @@ -1109,29 +1109,12 @@ object CarbonResolvedCounterexample { println(s"Could not find a predicate node for: ${bhe.toString}") } case MagicWandType | QPMagicWandType => - val translatedArgs = bhe.field // .map(x => translNames.getOrElse(x, x)) TODO translNames + val argValues = bhe.field // TODO translNames: .map(x => translNames.getOrElse(x, x)) for ((mw, idx) <- program.magicWandStructures.zipWithIndex) { - val mwStructure = mw.structure(program, true) - val replacements: Iterable[(ast.Node, ast.Node)] = mwStructure.subexpressionsToEvaluate(program).zip(translatedArgs).map(e => e._1 -> ast.LocalVar(e._2, e._1.typ)()) - val repl: scala.collection.immutable.Map[ast.Node, ast.Node] = scala.collection.immutable.Map.from(replacements) - val transformed = mwStructure.replace(repl) - if (idx == 0) { - if (model.entries.get("wand").isDefined && model.entries.get("wand").get.isInstanceOf[MapEntry]) { - for (s <- model.entries.get("wand").get.asInstanceOf[MapEntry].options) { - if (s._2.toString == bhe.reference(1)) { - ans +:= (mw.res(program), WandFinalEntry("wand", transformed.left, transformed.right, scala.collection.immutable.Map[String, String](), bhe.perm, bhe.het)) - } - } - } - } else { - val wandName = "wand_" ++ idx.toString - if (model.entries.get(wandName).isDefined && model.entries.get(wandName).get.isInstanceOf[MapEntry]) { - for (s <- model.entries.get(wandName).get.asInstanceOf[MapEntry].options) { - if (s._2.toString == bhe.reference(1)) { - ans +:= (mw, WandFinalEntry(wandName, transformed.left, transformed.right, scala.collection.immutable.Map[String, String](), bhe.perm, bhe.het)) - } - } - } + val (wandName, resource): (String, Resource) = if (idx == 0) ("wand", mw.res(program)) else ("wand_" ++ idx.toString, mw) + val instances = model.entries.get(wandName).collect { case MapEntry(opts, _) => opts }.getOrElse(scala.collection.immutable.Map.empty) + if (instances.exists(_._2.toString == bhe.reference(1))) { + ans +:= (resource, WandFinalEntry.fromStructure(wandName, mw, argValues, bhe.perm, bhe.het, program)) } } case _ => println("This type of heap entry could not be matched correctly!") From d5b56f349b17ac84c2c8046f1d4e8dfe5a2b09f6 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Mon, 13 Jul 2026 17:22:46 +0200 Subject: [PATCH 5/9] Renaming --- silver | 2 +- .../boogie/CarbonResolvedCounterexample.scala | 62 +++++++++---------- 2 files changed, 32 insertions(+), 32 deletions(-) diff --git a/silver b/silver index 59fa417d..91b90acf 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 59fa417ddc38ae8813746e8f6cded8ab12d05e42 +Subproject commit 91b90acf1132dc84dacfaa74da72b2a80b8f1e53 diff --git a/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala b/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala index 1e9519a7..81f465a5 100644 --- a/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala +++ b/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala @@ -28,7 +28,7 @@ case class CarbonResolvedCounterexample(e: AbstractError, val (ceStore, refOcc) = CarbonResolvedCounterexample.detStore(program.methodsByName(errorMethod.name).transitiveScopedDecls, rawCE.basicVariables, rawCE.allCollections) val nameTranslationMap = CarbonResolvedCounterexample.detTranslationMap(rawCE.basicVariables, rawCE.allCollections, refOcc) - val ceHeaps = rawCE.allBasicHeaps.map(bh => (bh._1, CarbonResolvedCounterexample.detHeap(rawCE.workingModel, bh._2, program, rawCE.allCollections, nameTranslationMap, rawCE.originalEntries))).reverse + val ceHeaps = rawCE.allRawHeaps.map(bh => (bh._1, CarbonResolvedCounterexample.detHeap(rawCE.workingModel, bh._2, program, rawCE.allCollections, nameTranslationMap, rawCE.originalEntries))).reverse override val domainEntries: Seq[BasicDomainEntry] = CarbonResolvedCounterexample.detTranslatedDomains(rawCE.domainEntries, nameTranslationMap) override val functionEntries: Seq[BasicFunctionEntry] = CarbonResolvedCounterexample.detTranslatedFunctions(rawCE.nonDomainFunctions, nameTranslationMap) @@ -68,7 +68,7 @@ case class CarbonRawCounterexample(ve: VerificationError, val workingModel = CarbonRawCounterexample.buildNewModel(originalEntries.entries) val (hmLabels, hmStates) = CarbonRawCounterexample.oldAndReturnHeapMask(workingModel, otherDeclarations) - val allBasicHeaps = CarbonRawCounterexample.detHeaps(workingModel, hmStates, originalEntries, hmLabels, program).map{case (n, bh) => if (n == "return") ("current", bh) else (n, bh)} + val allRawHeaps = CarbonRawCounterexample.detHeaps(workingModel, hmStates, originalEntries, hmLabels, program).map{case (n, bh) => if (n == "return") ("current", bh) else (n, bh)} val domainEntries = CarbonRawCounterexample.getAllDomains(originalEntries, program) val nonDomainFunctions = CarbonRawCounterexample.getAllFunctions(originalEntries, program, hmStates) @@ -80,8 +80,8 @@ case class CarbonRawCounterexample(ve: VerificationError, finalString += basicVariables.map(x => x.toString).mkString("", "\n", "\n") if (!allCollections.isEmpty) finalString += allCollections.map(x => x.toString).mkString("", "\n", "\n") - if (!allBasicHeaps.filter(y => !y._2.basicHeapEntries.isEmpty).isEmpty) - finalString += allBasicHeaps.reverse.filter(y => !y._2.basicHeapEntries.isEmpty).map(x => " " + x._1 + " Heap: \n" + x._2.toString).mkString("", "\n", "\n") + if (!allRawHeaps.filter(y => !y._2.rawHeapEntries.isEmpty).isEmpty) + finalString += allRawHeaps.reverse.filter(y => !y._2.rawHeapEntries.isEmpty).map(x => " " + x._1 + " Heap: \n" + x._2.toString).mkString("", "\n", "\n") if (!domainEntries.isEmpty || !nonDomainFunctions.isEmpty) finalString ++= " Domains:\n" if (!domainEntries.isEmpty) @@ -621,7 +621,7 @@ object CarbonRawCounterexample { * @param MapType0Select Mappings from a mask state, a reference and a field to a permission. * The fields in these mappings can also be identifiers for a predicate or a magic wand. */ - def detHeaps(opMapping: Map[Seq[String], String], hmStates: List[(String, String, String, String)], model: Model, hmLabels: Map[String, (String, String)], program: Program): Seq[(String, BasicHeap)] = { + def detHeaps(opMapping: Map[Seq[String], String], hmStates: List[(String, String, String, String)], model: Model, hmLabels: Map[String, (String, String)], program: Program): Seq[(String, RawHeap)] = { val predByName = program.predicatesByName var heapOp = Map[Seq[String], String]() var maskOp = Map[Seq[String], String]() @@ -657,9 +657,9 @@ object CarbonRawCounterexample { } } val permMap = model.entries.get("U_2_real").get.asInstanceOf[MapEntry].options - var res = Seq[(String, BasicHeap)]() + var res = Seq[(String, RawHeap)]() for ((labelName, (labelHeap, labelMask)) <- hmLabels) { - var heapEntrySet = Set[BasicHeapEntry]() + var heapEntrySet = Set[RawHeapEntry]() val heapStore = model.entries.get("MapType0Store").get.asInstanceOf[MapEntry].options val maskStore = model.entries.get("MapType1Store").get.asInstanceOf[MapEntry].options val heapMap = recursiveBuildHeapMask(heapStore, labelHeap, Map.empty) @@ -671,11 +671,11 @@ object CarbonRawCounterexample { val tempPerm: Option[Rational] = detHeapEntryPermission(permMap, perm._1) val typ: HeapEntryType = detHeapType(model, qpMaskSet, ck(1), perm._2) if (typ == FieldType || typ == QPFieldType) { - heapEntrySet += BasicHeapEntry(Seq(ck(0)), Seq(ck(1)), value._1, tempPerm, typ, None) + heapEntrySet += RawHeapEntry(Seq(ck(0)), Seq(ck(1)), value._1, tempPerm, typ, None) } else if (typ == PredicateType || typ == QPPredicateType) { - heapEntrySet += BasicHeapEntry(Seq(ck(0), ck(1)), predContentMap.get(ck(1)).getOrElse(Seq()), value._1, tempPerm, typ, Some(evalInsidePredicate(value._1, ck(1), predicateFinder, predByName, model))) + heapEntrySet += RawHeapEntry(Seq(ck(0), ck(1)), predContentMap.get(ck(1)).getOrElse(Seq()), value._1, tempPerm, typ, Some(evalInsidePredicate(value._1, ck(1), predicateFinder, predByName, model))) } else if (typ == MagicWandType || typ == QPMagicWandType) { - heapEntrySet += BasicHeapEntry(Seq(ck(0), ck(1)), predContentMap.get(ck(1)).getOrElse(Seq()), value._1, tempPerm, typ, None) + heapEntrySet += RawHeapEntry(Seq(ck(0), ck(1)), predContentMap.get(ck(1)).getOrElse(Seq()), value._1, tempPerm, typ, None) } } var startNow = false @@ -698,18 +698,18 @@ object CarbonRawCounterexample { val typ: HeapEntryType = detHeapType(model, qpMaskSet, field, maskId) if (typ == FieldType || typ == QPFieldType) { heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { - case Some(v) => heapEntrySet += BasicHeapEntry(Seq(reference), Seq(field), v, tempPerm, typ, None) - case None => heapEntrySet += BasicHeapEntry(Seq(reference), Seq(field), "#undefined", tempPerm, typ, None) + case Some(v) => heapEntrySet += RawHeapEntry(Seq(reference), Seq(field), v, tempPerm, typ, None) + case None => heapEntrySet += RawHeapEntry(Seq(reference), Seq(field), "#undefined", tempPerm, typ, None) } } else if (typ == PredicateType || typ == QPPredicateType) { heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { - case Some(v) => heapEntrySet += BasicHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), v, tempPerm, typ, Some(evalInsidePredicate(v, field, predicateFinder, predByName, model))) - case None => heapEntrySet += BasicHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), "#undefined", tempPerm, typ, Some(Map[ast.Exp, ModelEntry]())) + case Some(v) => heapEntrySet += RawHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), v, tempPerm, typ, Some(evalInsidePredicate(v, field, predicateFinder, predByName, model))) + case None => heapEntrySet += RawHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), "#undefined", tempPerm, typ, Some(Map[ast.Exp, ModelEntry]())) } } else if (typ == MagicWandType || typ == QPMagicWandType) { heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { - case Some(v) => heapEntrySet += BasicHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), v, tempPerm, typ, None) - case None => heapEntrySet += BasicHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), "#undefined", tempPerm, typ, None) + case Some(v) => heapEntrySet += RawHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), v, tempPerm, typ, None) + case None => heapEntrySet += RawHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), "#undefined", tempPerm, typ, None) } } } else { @@ -719,8 +719,8 @@ object CarbonRawCounterexample { case Some(v) => heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { case Some(x) => - heapEntrySet += BasicHeapEntry(Seq(reference), Seq(field), x, v.perm, v.het, None) - heapEntrySet -= BasicHeapEntry(Seq(reference), Seq(field), "#undefined", v.perm, v.het, None) + heapEntrySet += RawHeapEntry(Seq(reference), Seq(field), x, v.perm, v.het, None) + heapEntrySet -= RawHeapEntry(Seq(reference), Seq(field), "#undefined", v.perm, v.het, None) case None => // } case None => // @@ -731,8 +731,8 @@ object CarbonRawCounterexample { case Some(v) => heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { case Some(x) => - heapEntrySet += BasicHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), x, v.perm, v.het, v.insidePredicate) - heapEntrySet -= BasicHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), "#undefined", v.perm, v.het, v.insidePredicate) + heapEntrySet += RawHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), x, v.perm, v.het, v.insidePredicate) + heapEntrySet -= RawHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), "#undefined", v.perm, v.het, v.insidePredicate) case None => // } case None => // @@ -743,8 +743,8 @@ object CarbonRawCounterexample { case Some(v) => heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { case Some(x) => - heapEntrySet += BasicHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), x, v.perm, v.het, None) - heapEntrySet -= BasicHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), "#undefined", v.perm, v.het, None) + heapEntrySet += RawHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), x, v.perm, v.het, None) + heapEntrySet -= RawHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), "#undefined", v.perm, v.het, None) case None => // } case None => // @@ -754,7 +754,7 @@ object CarbonRawCounterexample { } } } - res +:= (labelName, BasicHeap(heapEntrySet)) + res +:= (labelName, RawHeap(heapEntrySet)) } res } @@ -1065,7 +1065,7 @@ object CarbonResolvedCounterexample { /** * Match heap resources to their ast node and translate all identifiers (for fields and references) */ - def detHeap(opMapping: Map[Seq[String], String], basicHeap: BasicHeap, program: Program, collections: Seq[CECollection], translNames: Map[String, String], model: Model): HeapCounterexample = { + def detHeap(opMapping: Map[Seq[String], String], basicHeap: RawHeap, program: Program, collections: Seq[CECollection], translNames: Map[String, String], model: Model): HeapCounterexample = { // choosing all the needed values from the Boogie Model var usedIdent = Map[String, Member]() for ((key, value) <- opMapping) { @@ -1081,8 +1081,8 @@ object CarbonResolvedCounterexample { } } - var ans = Seq[(Resource, FinalHeapEntry)]() - for (bhe <- basicHeap.basicHeapEntries) { + var ans = Seq[(Resource, ResolvedHeapEntry)]() + for (bhe <- basicHeap.rawHeapEntries) { bhe.het match { case FieldType | QPFieldType=> if (!bhe.perm.isDefined || !(bhe.perm.get == Rational.zero)) { @@ -1091,9 +1091,9 @@ object CarbonResolvedCounterexample { val fi = f.asInstanceOf[Field] collections.find(_.id == bhe.valueID) match { case Some(coll) => - ans +:= (fi, FieldFinalEntry(bhe.reference.head, fi.name, coll.value, bhe.perm, fi.typ, bhe.het)) + ans +:= (fi, FieldResolvedEntry(bhe.reference.head, fi.name, coll.value, bhe.perm, fi.typ, bhe.het)) case None => - ans +:= (fi, FieldFinalEntry(bhe.reference.head, fi.name, CounterexampleValue.literal(bhe.valueID, Some(fi.typ)), bhe.perm, fi.typ, bhe.het)) + ans +:= (fi, FieldResolvedEntry(bhe.reference.head, fi.name, CounterexampleValue.literal(bhe.valueID, Some(fi.typ)), bhe.perm, fi.typ, bhe.het)) } case None => println(s"Could not find a field node for: ${bhe.toString}") @@ -1103,8 +1103,8 @@ object CarbonResolvedCounterexample { usedIdent.get(bhe.reference(1)) match { case Some(p) => val pr = p.asInstanceOf[Predicate] - val refNames = bhe.field - ans +:= (pr, PredFinalEntry(pr.name, refNames, bhe.perm, bhe.insidePredicate, bhe.het)) + val argExps = bhe.field.zip(pr.formalArgs).map { case (v, fa) => CounterexampleValue.literal(v, Some(fa.typ)) } + ans +:= (pr, PredResolvedEntry(pr.name, argExps, bhe.perm, bhe.insidePredicate, bhe.het)) case None => println(s"Could not find a predicate node for: ${bhe.toString}") } @@ -1114,7 +1114,7 @@ object CarbonResolvedCounterexample { val (wandName, resource): (String, Resource) = if (idx == 0) ("wand", mw.res(program)) else ("wand_" ++ idx.toString, mw) val instances = model.entries.get(wandName).collect { case MapEntry(opts, _) => opts }.getOrElse(scala.collection.immutable.Map.empty) if (instances.exists(_._2.toString == bhe.reference(1))) { - ans +:= (resource, WandFinalEntry.fromStructure(wandName, mw, argValues, bhe.perm, bhe.het, program)) + ans +:= (resource, WandResolvedEntry.fromStructure(wandName, mw, argValues, bhe.perm, bhe.het, program)) } } case _ => println("This type of heap entry could not be matched correctly!") From 714cc05a85330e2339d60d01bc859251fd1f42a5 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Mon, 13 Jul 2026 22:57:14 +0200 Subject: [PATCH 6/9] Fixed parsing of permission amounts --- silver | 2 +- .../boogie/CarbonResolvedCounterexample.scala | 26 ++++++++++++++----- 2 files changed, 21 insertions(+), 7 deletions(-) diff --git a/silver b/silver index 91b90acf..fbd51498 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 91b90acf1132dc84dacfaa74da72b2a80b8f1e53 +Subproject commit fbd514985ad17f398341fcbd8292f0b5de37bdf6 diff --git a/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala b/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala index 81f465a5..7fc5002f 100644 --- a/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala +++ b/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala @@ -895,17 +895,31 @@ object CarbonRawCounterexample { def detHeapEntryPermission(permMap: Map[scala.collection.immutable.Seq[ValueEntry], ValueEntry], perm: String): Option[Rational] = { for ((s, ve) <- permMap) { if (s(0).toString == perm) { - if (ve.isInstanceOf[ConstantEntry]) { - return Some(Rational.apply(BigInt(ve.asInstanceOf[ConstantEntry].value.toFloat.toInt), BigInt(1))) - } else if (ve.isInstanceOf[ApplicationEntry]) { - val ae = ve.asInstanceOf[ApplicationEntry] - return Some(Rational.apply(BigInt(ae.arguments(0).asInstanceOf[ConstantEntry].value.toFloat.toInt), BigInt(ae.arguments(1).asInstanceOf[ConstantEntry].value.toFloat.toInt))) - } + return Some(realToRational(ve)) } } None } + /** Converts a Boogie real value (as it appears in the U_2_real map) to an exact rational. */ + def realToRational(ve: ValueEntry): Rational = ve match { + case ConstantEntry(v) => parseDecimal(v) + case ApplicationEntry("/", Seq(num, den)) => realToRational(num) / realToRational(den) + case ApplicationEntry("-", Seq(arg)) => -realToRational(arg) + case _ => Rational.zero + } + + /** Parses a decimal literal ("1.0", "0.5", "3") to an exact rational without truncating. */ + def parseDecimal(v: String): Rational = { + try { + val bd = BigDecimal(v.trim) + if (bd.scale <= 0) Rational.apply(bd.toBigInt, BigInt(1)) + else Rational.apply(bd.bigDecimal.unscaledValue(), BigInt(10).pow(bd.scale)) + } catch { + case _: Throwable => Rational.zero + } + } + def recursiveBuildHeapMask(inputMap: Map[scala.collection.immutable.Seq[ValueEntry], ValueEntry], s: String, resultMap: Map[Seq[String], (String, String)]): Map[Seq[String], (String, String)] = { val entries: Iterable[(Seq[ValueEntry], ValueEntry)] = inputMap.collect { case (key, value) if value.toString == s && key.length >= 3 => (key, value) From a739fada46a3b0af40fad5a973ddc097f43f9e98 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Tue, 14 Jul 2026 17:52:11 +0200 Subject: [PATCH 7/9] Use Boogie's capturedState attribute to extract states for CEs --- silver | 2 +- .../boogie/CarbonResolvedCounterexample.scala | 16 +++++-- .../scala/viper/carbon/boogie/Optimizer.scala | 2 +- .../viper/carbon/boogie/PrettyPrinter.scala | 4 +- .../viper/carbon/boogie/Transformer.scala | 4 +- .../scala/viper/carbon/boogie/boogie.scala | 2 +- .../scala/viper/carbon/boogie/utility.scala | 2 +- .../modules/impls/DefaultStateModule.scala | 10 ++++- .../modules/impls/DefaultWandModule.scala | 2 +- .../modules/impls/QuantifiedPermModule.scala | 2 +- .../carbon/verifier/BoogieInterface.scala | 43 +++++++++++++++---- 11 files changed, 67 insertions(+), 22 deletions(-) diff --git a/silver b/silver index fbd51498..6e787acf 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit fbd514985ad17f398341fcbd8292f0b5de37bdf6 +Subproject commit 6e787acf8e41e504cd38e10391a2de7186bb6f86 diff --git a/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala b/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala index 7fc5002f..d024c1ea 100644 --- a/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala +++ b/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala @@ -551,8 +551,6 @@ object CarbonRawCounterexample { heapInstances += ((k(0), v)) } else if (k(0).startsWith("Mask@")) { maskInstances += ((k(0), v)) - } else if (k(0).startsWith("QPMask@")) { - maskInstances += ((k(0).stripPrefix("QP").trim, v)) } else if ((k(0) == "state") && (v == "true")) { states += ((k(1), k(2))) } @@ -610,7 +608,19 @@ object CarbonRawCounterexample { labelsHeapMask += ("return" -> (filteredList(filteredList.length - 1)._3, filteredList(filteredList.length - 1)._4)) } - (labelsHeapMask, filteredList) + // If Boogie's model view captured the state at the failing assertion (via {:captureState}, + // injected by BoogieInterface as `__captureState__current__Heap/Mask`), use its Heap and Mask + // directly as the current ("return") state. This is reliable regardless of QP masks / SSA + // naming, unlike the heuristic above. We append the captured (heap, mask) to the state list so + // detHeaps picks it up, and override the "return" label to point at it. + (workingModel.get(Seq("__captureState__current__Heap")), workingModel.get(Seq("__captureState__current__Mask"))) match { + case (Some(capturedHeap), Some(capturedMask)) => + val capturedEntry = ("Heap@captured", "Mask@captured", capturedHeap, capturedMask) + labelsHeapMask += ("return" -> (capturedHeap, capturedMask)) + (labelsHeapMask, filteredList :+ capturedEntry) + case _ => + (labelsHeapMask, filteredList) + } } /** diff --git a/src/main/scala/viper/carbon/boogie/Optimizer.scala b/src/main/scala/viper/carbon/boogie/Optimizer.scala index 6f84c243..68fa9423 100644 --- a/src/main/scala/viper/carbon/boogie/Optimizer.scala +++ b/src/main/scala/viper/carbon/boogie/Optimizer.scala @@ -141,7 +141,7 @@ object Optimizer { Statements.EmptyStmt case Assert(TrueLit(), _) => Statements.EmptyStmt - case Assume(TrueLit()) => Statements.EmptyStmt + case Assume(TrueLit(), atts) if atts.isEmpty => Statements.EmptyStmt }) } } diff --git a/src/main/scala/viper/carbon/boogie/PrettyPrinter.scala b/src/main/scala/viper/carbon/boogie/PrettyPrinter.scala index ab701748..ffd86648 100644 --- a/src/main/scala/viper/carbon/boogie/PrettyPrinter.scala +++ b/src/main/scala/viper/carbon/boogie/PrettyPrinter.scala @@ -150,8 +150,8 @@ class PrettyPrinter(n: Node) extends BracketPrettyPrinter { } } s match { - case Assume(e) => - text("assume") <+> show(quantifyOverFreeTypeVars(e)) <> char (';') + case Assume(e, atts) => + text("assume") <+> (if (atts.isEmpty) nil else showAttributes(atts) <> space) <> show(quantifyOverFreeTypeVars(e)) <> char (';') case a@Assert(e, error) => text("assert") <+> "{:msg" <+> "\" " <> showError(error, a.id) <> "\"}" <> line <> diff --git a/src/main/scala/viper/carbon/boogie/Transformer.scala b/src/main/scala/viper/carbon/boogie/Transformer.scala index 86e1ac1d..2a1d9106 100644 --- a/src/main/scala/viper/carbon/boogie/Transformer.scala +++ b/src/main/scala/viper/carbon/boogie/Transformer.scala @@ -48,7 +48,7 @@ object Transformer { ss match { case Assign(lhs, rhs) => Assign(go(lhs), go(rhs)) case Assert(e, error) => Assert(go(e), error) - case Assume(e) => Assume(go(e)) + case Assume(e, atts) => Assume(go(e), atts) case HavocImpl(es) => HavocImpl(es map go) case Comment(_) => parent case CommentBlock(s, stmt) => CommentBlock(s, go(stmt)) @@ -149,7 +149,7 @@ object DuplicatingTransformer { ss match { case Assign(lhs, rhs) => for {lhsResult <- go(lhs); rhsResult <- go(rhs)} yield Assign(lhsResult, rhsResult) case Assert(e, error) => go(e) map (Assert(_, error)) - case Assume(e) => go(e) map (Assume(_)) + case Assume(e, atts) => go(e) map (Assume(_, atts)) case HavocImpl(es) => goSeq(es) map (HavocImpl(_)) case Comment(_) => Seq(parent) case CommentBlock(s, stmt) => go(stmt) map (CommentBlock(s, _)) diff --git a/src/main/scala/viper/carbon/boogie/boogie.scala b/src/main/scala/viper/carbon/boogie/boogie.scala index b0e3286c..cfee9813 100644 --- a/src/main/scala/viper/carbon/boogie/boogie.scala +++ b/src/main/scala/viper/carbon/boogie/boogie.scala @@ -307,7 +307,7 @@ sealed trait Stmt extends Node { case class Lbl(name: Identifier) case class Goto(dests: Seq[Lbl]) extends Stmt case class Label(lbl: Lbl) extends Stmt -case class Assume(exp: Exp) extends Stmt +case class Assume(exp: Exp, attributes: Map[String, String] = Map.empty) extends Stmt case class AssertImpl(exp: Exp, error: VerificationError) extends Stmt { var id = AssertIds.next // Used for mapping errors in the output back to VerificationErrors } diff --git a/src/main/scala/viper/carbon/boogie/utility.scala b/src/main/scala/viper/carbon/boogie/utility.scala index 6022fa48..ae767350 100644 --- a/src/main/scala/viper/carbon/boogie/utility.scala +++ b/src/main/scala/viper/carbon/boogie/utility.scala @@ -106,7 +106,7 @@ object Nodes { ss match { case Assign(lhs, rhs) => Seq(lhs, rhs) case Assert(e, _) => Seq(e) - case Assume(e) => Seq(e) + case Assume(e, _) => Seq(e) case HavocImpl(es) => es case Comment(_) => Nil case CommentBlock(_, stmt) => Seq(stmt) diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultStateModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultStateModule.scala index 7ad243c7..765a0efc 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultStateModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultStateModule.scala @@ -27,8 +27,16 @@ class DefaultStateModule(val verifier: Verifier) extends StateModule { implicit val stateNamespace = verifier.freshNamespace("state") + private var captureStateCounter = 0 + override def assumeGoodState = { - Assume(currentGoodState) + // Attach a {:captureState} attribute to the good-state assumption. With Boogie's model view + // (/mv, enabled when a counterexample is requested) this makes Boogie report the values of all + // variables (in particular Heap and Mask) at this exact program point, which the counterexample + // extractor reads directly instead of guessing the current state from SSA variable names. The + // attribute is inert when /mv is off. The value is only for uniqueness (Boogie also freshens it). + captureStateCounter += 1 + Assume(currentGoodState, Map("captureState" -> ("cs_" + captureStateCounter))) } override def preamble: Seq[Decl] = { diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala index a072b8a9..e09e8e97 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala @@ -604,7 +604,7 @@ private def setupTransferableEntity(e: sil.Exp, permTransfer: Exp):(Transferable override def exchangeAssumesWithBoolean(stmt: Stmt,boolVar: LocalVar):Stmt = { stmt match { - case Assume(exp) => + case Assume(exp, _) => boolVar := (boolVar && viper.carbon.boogie.PrettyPrinter.quantifyOverFreeTypeVars(exp)) case Seqn(statements) => Seqn(statements.map(s => exchangeAssumesWithBoolean(s, boolVar))) diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala index 01a20c13..88167c93 100644 --- a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala @@ -889,7 +889,7 @@ class QuantifiedPermModule(val verifier: Verifier) } override def inhaleExp(e: sil.Exp, error: PartialVerificationError): Stmt = { - inhaleAux(e, Assume, error) + inhaleAux(e, Assume(_), error) } override def inhaleWandFt(w: sil.MagicWand): Stmt = { diff --git a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala index ee6c1a8f..5e30c76c 100644 --- a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala +++ b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala @@ -134,21 +134,48 @@ trait BoogieInterface { } var parsingModel : Option[StringBuilder] = None - var stateInitialBlock = false + // Captured states of the current model (from Boogie's {:captureState} model view), in trace + // order: label -> (variable -> value). The last one is the state at the failing assertion. We + // inject its Heap/Mask into the model as flat `__captureState__current__` entries so the + // counterexample extractor can read them directly instead of guessing the current state from + // SSA variable names. The `*** STATE` blocks must NOT leak into the model string (they are not + // valid model entries) — hence they are captured here rather than appended to `parsingModel`. + var capturedStates : collection.mutable.LinkedHashMap[String, collection.mutable.LinkedHashMap[String, String]] = null + var currentStateName : String = null + val StateStartPattern = "\\*\\*\\* STATE (.*)".r + val StateVarPattern = "\\s*(\\S+) -> (.*)".r for (l <- output.linesIterator) { l match { - case "*** END_STATE" => - stateInitialBlock = false - case "*** STATE " => - stateInitialBlock = true - case _ if stateInitialBlock => //ignore everything within state block + case "*** MODEL" if parsingModel.isEmpty => + parsingModel = Some(new StringBuilder) + capturedStates = collection.mutable.LinkedHashMap.empty case "*** END_MODEL" if parsingModel.isDefined => + if (capturedStates != null && capturedStates.nonEmpty) { + // The captured states are sparse (each lists only the variables whose current + // incarnation has a value in the partial model), so accumulate the last non-empty + // value of each variable across the states in trace order to get the state at the + // failing assertion. + val current = collection.mutable.LinkedHashMap[String, String]() + for ((_, vars) <- capturedStates; (v, value) <- vars if value.trim.nonEmpty) current(v) = value.trim + for (v <- Seq("Heap", "Mask"); value <- current.get(v)) + parsingModel.get.append(s"__captureState__current__$v -> $value\n") + } models.append(parsingModel.get.toString()) parsingModel = None + capturedStates = null + currentStateName = null + case StateStartPattern(name) if capturedStates != null => + currentStateName = name + capturedStates(name) = collection.mutable.LinkedHashMap.empty + case "*** END_STATE" => + currentStateName = null + case _ if currentStateName != null => + l match { + case StateVarPattern(v, value) => capturedStates(currentStateName)(v) = value + case _ => // ignore non-variable lines within a state block + } case _ if parsingModel.isDefined => parsingModel.get.append(l).append("\n") - case "*** MODEL" if parsingModel.isEmpty => - parsingModel = Some(new StringBuilder) case LogoPattern(version) => version_found = version case ErrorPattern(id) => From d6df9c0cac7301c84ce58aa9abefbebc172f1b33 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Wed, 15 Jul 2026 15:22:21 +0200 Subject: [PATCH 8/9] Replacing old machinery completely --- .../scala/viper/carbon/CarbonVerifier.scala | 2 +- .../boogie/CarbonResolvedCounterexample.scala | 206 +++++------------- .../modules/impls/DefaultStateModule.scala | 5 +- .../carbon/verifier/BoogieInterface.scala | 6 + 4 files changed, 60 insertions(+), 159 deletions(-) diff --git a/src/main/scala/viper/carbon/CarbonVerifier.scala b/src/main/scala/viper/carbon/CarbonVerifier.scala index c53ea83d..7970ea8f 100644 --- a/src/main/scala/viper/carbon/CarbonVerifier.scala +++ b/src/main/scala/viper/carbon/CarbonVerifier.scala @@ -178,7 +178,7 @@ case class CarbonVerifier(override val reporter: Reporter, var transformNames = false var rawCounterexample = false - var resolvedCounterexample = true + var resolvedCounterexample = false if (config == null) Seq() else config.counterexample.toOption match { case Some(NativeModel) => case Some(VariablesModel) => transformNames = true diff --git a/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala b/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala index d024c1ea..d825fc4f 100644 --- a/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala +++ b/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala @@ -67,11 +67,11 @@ case class CarbonRawCounterexample(ve: VerificationError, val allMultisets = CarbonRawCounterexample.detMultisets(originalEntries) val workingModel = CarbonRawCounterexample.buildNewModel(originalEntries.entries) - val (hmLabels, hmStates) = CarbonRawCounterexample.oldAndReturnHeapMask(workingModel, otherDeclarations) - val allRawHeaps = CarbonRawCounterexample.detHeaps(workingModel, hmStates, originalEntries, hmLabels, program).map{case (n, bh) => if (n == "return") ("current", bh) else (n, bh)} + val (hmLabels, heapInstances) = CarbonRawCounterexample.oldAndReturnHeapMask(workingModel, otherDeclarations) + val allRawHeaps = CarbonRawCounterexample.detHeaps(workingModel, originalEntries, hmLabels, program).map{case (n, bh) => if (n == "return") ("current", bh) else (n, bh)} val domainEntries = CarbonRawCounterexample.getAllDomains(originalEntries, program) - val nonDomainFunctions = CarbonRawCounterexample.getAllFunctions(originalEntries, program, hmStates) + val nonDomainFunctions = CarbonRawCounterexample.getAllFunctions(originalEntries, program, heapInstances) override def toString: String = { var finalString = " Raw Counterexample: \n" @@ -538,89 +538,35 @@ object CarbonRawCounterexample { * Gather all the heap and mask states from the model. Then, combine them into heap instances (=> mask state + heap state) * and order them. */ - def oldAndReturnHeapMask(workingModel: Map[Seq[String], String], labels: Seq[Declaration]): (Map[String, (String, String)], List[(String, String, String, String)]) = { - var heapInstances = Set[(String, String)]() - var maskInstances = Set[(String, String)]() - var states = Set[(String, String)]() - for ((k, v) <- workingModel) { - if (k(0).startsWith("Heap@@")) { - heapInstances += ((k(0), v)) - } else if (k(0).startsWith("Mask@@")) { - maskInstances += ((k(0), v)) - } else if (k(0).startsWith("Heap@")) { - heapInstances += ((k(0), v)) - } else if (k(0).startsWith("Mask@")) { - maskInstances += ((k(0), v)) - } else if ((k(0) == "state") && (v == "true")) { - states += ((k(1), k(2))) - } - } - - // determine all the heap and mask states (first all, then sorted and then filtered) - val hmStates = for { - (heapId, maskId) <- states - hName <- heapInstances.collect { case (name, id) if id == heapId => name } - mName <- maskInstances.collect { case (name, id) if id == maskId => name } - } yield (hName, mName, heapId, maskId) - - val sortedHMStates = hmStates.toList.sortBy { - case (heapName, maskName, _, _) => - if (heapName.startsWith("Heap@@") && maskName.startsWith("Mask@@")) { - 0 - } else if (heapName.startsWith("Heap@@")) { - val maskValue = maskName.stripPrefix("Mask@").trim.toInt - maskValue + 1 - } else if (maskName.startsWith("Mask@@")) { - val heapValue = heapName.stripPrefix("Heap@").trim.toInt - heapValue + 1 - } else { - val heapValue = heapName.stripPrefix("Heap@").trim.toInt - val maskValue = maskName.stripPrefix("Mask@").trim.toInt - heapValue + maskValue + 2 - } - } - - val filteredList = sortedHMStates.foldLeft(List.empty[(String, String, String, String)]) { - case (acc, curr@(h, m, _, _)) - if h.contains("@@") || m.contains("@@") || acc.isEmpty || acc.last._1.contains("@@") || acc.last._2.contains("@@") || (h.stripPrefix("Heap@").trim.toInt >= acc.last._1.stripPrefix("Heap@").trim.toInt && m.stripPrefix("Mask@").trim.toInt >= acc.last._2.stripPrefix("Mask@").trim.toInt) => - acc :+ curr - case (acc, _) => - acc - } + def oldAndReturnHeapMask(workingModel: Map[Seq[String], String], labels: Seq[Declaration]): (Map[String, (String, String)], Seq[(String, String)]) = { + // Collect the Heap@ instances (name -> value id) so that getAllFunctions can display heap-typed + // function arguments by their Boogie name instead of the raw model value id. + val heapInstances = workingModel.collect { case (k, v) if k(0).startsWith("Heap@") => (k(0), v) }.toSeq var labelsHeapMask = Map[String, (String, String)]() - if (filteredList.nonEmpty) { - if (filteredList.size > 1) { - labelsHeapMask += ("old" -> (filteredList(0)._3, filteredList(0)._4)) - } - for (l <- labels) { - l match { - case ast.Label(n, _) => - val lhi = "Label" + n + "Heap" - val lmi = "Label" + n + "Mask" - if (workingModel.contains(Seq(lhi)) && workingModel.contains(Seq(lmi))) { - labelsHeapMask += (n -> (workingModel.get(Seq(lhi)).get, workingModel.get(Seq(lmi)).get)) - } - case _ => // - } + // The (heap, mask) for each label state is read directly from Boogie's model view, captured via + // {:captureState} attributes: the pre-state under "old" (initOldState) and the state at the + // failing point under "current" (assumeGoodState). BoogieInterface injects these as flat + // `__captureState__old/current__Heap/Mask` model entries. Explicit label statements store their + // heap/mask in LabelNHeap/LabelNMask. + for (h <- workingModel.get(Seq("__captureState__old__Heap")); m <- workingModel.get(Seq("__captureState__old__Mask"))) + labelsHeapMask += ("old" -> (h, m)) + for (l <- labels) { + l match { + case ast.Label(n, _) => + val lhi = "Label" + n + "Heap" + val lmi = "Label" + n + "Mask" + if (workingModel.contains(Seq(lhi)) && workingModel.contains(Seq(lmi))) { + labelsHeapMask += (n -> (workingModel.get(Seq(lhi)).get, workingModel.get(Seq(lmi)).get)) + } + case _ => // } - labelsHeapMask += ("return" -> (filteredList(filteredList.length - 1)._3, filteredList(filteredList.length - 1)._4)) } + for (h <- workingModel.get(Seq("__captureState__current__Heap")); m <- workingModel.get(Seq("__captureState__current__Mask"))) + labelsHeapMask += ("return" -> (h, m)) - // If Boogie's model view captured the state at the failing assertion (via {:captureState}, - // injected by BoogieInterface as `__captureState__current__Heap/Mask`), use its Heap and Mask - // directly as the current ("return") state. This is reliable regardless of QP masks / SSA - // naming, unlike the heuristic above. We append the captured (heap, mask) to the state list so - // detHeaps picks it up, and override the "return" label to point at it. - (workingModel.get(Seq("__captureState__current__Heap")), workingModel.get(Seq("__captureState__current__Mask"))) match { - case (Some(capturedHeap), Some(capturedMask)) => - val capturedEntry = ("Heap@captured", "Mask@captured", capturedHeap, capturedMask) - labelsHeapMask += ("return" -> (capturedHeap, capturedMask)) - (labelsHeapMask, filteredList :+ capturedEntry) - case _ => - (labelsHeapMask, filteredList) - } + (labelsHeapMask, heapInstances) } /** @@ -631,7 +577,7 @@ object CarbonRawCounterexample { * @param MapType0Select Mappings from a mask state, a reference and a field to a permission. * The fields in these mappings can also be identifiers for a predicate or a magic wand. */ - def detHeaps(opMapping: Map[Seq[String], String], hmStates: List[(String, String, String, String)], model: Model, hmLabels: Map[String, (String, String)], program: Program): Seq[(String, RawHeap)] = { + def detHeaps(opMapping: Map[Seq[String], String], model: Model, hmLabels: Map[String, (String, String)], program: Program): Seq[(String, RawHeap)] = { val predByName = program.predicatesByName var heapOp = Map[Seq[String], String]() var maskOp = Map[Seq[String], String]() @@ -688,79 +634,25 @@ object CarbonRawCounterexample { heapEntrySet += RawHeapEntry(Seq(ck(0), ck(1)), predContentMap.get(ck(1)).getOrElse(Seq()), value._1, tempPerm, typ, None) } } - var startNow = false - for ((_, _, heapIdentifier, maskIdentifier) <- hmStates.reverse) { - if (heapIdentifier == labelHeap && maskIdentifier == labelMask) { - startNow = true - } - if (startNow) { - for ((maskKey, perm) <- maskOp) { - val maskId = maskKey(1) - val reference = maskKey(2) - val field = maskKey(3) - if (maskId == maskIdentifier) { - if (!heapEntrySet.exists({ - case bhe => - ((bhe.reference.length > 0) && (bhe.field.length > 0) && (bhe.reference(0) == reference) && (bhe.field(0) == field)) || - ((bhe.reference.length > 1) && (bhe.reference(0) == reference) && (bhe.reference(1) == field)) - })) { - val tempPerm: Option[Rational] = detHeapEntryPermission(permMap, perm) - val typ: HeapEntryType = detHeapType(model, qpMaskSet, field, maskId) - if (typ == FieldType || typ == QPFieldType) { - heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { - case Some(v) => heapEntrySet += RawHeapEntry(Seq(reference), Seq(field), v, tempPerm, typ, None) - case None => heapEntrySet += RawHeapEntry(Seq(reference), Seq(field), "#undefined", tempPerm, typ, None) - } - } else if (typ == PredicateType || typ == QPPredicateType) { - heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { - case Some(v) => heapEntrySet += RawHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), v, tempPerm, typ, Some(evalInsidePredicate(v, field, predicateFinder, predByName, model))) - case None => heapEntrySet += RawHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), "#undefined", tempPerm, typ, Some(Map[ast.Exp, ModelEntry]())) - } - } else if (typ == MagicWandType || typ == QPMagicWandType) { - heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { - case Some(v) => heapEntrySet += RawHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), v, tempPerm, typ, None) - case None => heapEntrySet += RawHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), "#undefined", tempPerm, typ, None) - } - } - } else { - heapEntrySet.find( - { case bhe => (bhe.het == FieldType || bhe.het == QPFieldType) && (bhe.reference(0) == reference) && (bhe.field(0) == field) && (bhe.valueID == "#undefined") } - ) match { - case Some(v) => - heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { - case Some(x) => - heapEntrySet += RawHeapEntry(Seq(reference), Seq(field), x, v.perm, v.het, None) - heapEntrySet -= RawHeapEntry(Seq(reference), Seq(field), "#undefined", v.perm, v.het, None) - case None => // - } - case None => // - } - heapEntrySet.find( - { case bhe => (bhe.het == PredicateType || bhe.het == QPPredicateType) && (bhe.reference(0) == reference) && (bhe.reference(1) == field) && (bhe.valueID == "#undefined") } - ) match { - case Some(v) => - heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { - case Some(x) => - heapEntrySet += RawHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), x, v.perm, v.het, v.insidePredicate) - heapEntrySet -= RawHeapEntry(Seq(reference, field), predContentMap.get(field).getOrElse(Seq()), "#undefined", v.perm, v.het, v.insidePredicate) - case None => // - } - case None => // - } - heapEntrySet.find( - { case bhe => (bhe.het == MagicWandType || bhe.het == QPMagicWandType) && (bhe.reference(0) == reference) && (bhe.reference(1) == field) && (bhe.valueID == "#undefined") } - ) match { - case Some(v) => - heapOp.get(Seq("MapType0Select", heapIdentifier, reference, field)) match { - case Some(x) => - heapEntrySet += RawHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), x, v.perm, v.het, None) - heapEntrySet -= RawHeapEntry(Seq(reference, field), mwContentMap.get(field).getOrElse(Seq()), "#undefined", v.perm, v.het, None) - case None => // - } - case None => // - } - } - } + // Add every permission entry of this label's mask (from MapType1Select) that the store-based + // pass above didn't already cover, taking the value from this label's heap. Since the label's + // (heap, mask) is the exact captured state, there is no need to walk older mask versions. + for ((maskKey, perm) <- maskOp) { + val reference = maskKey(2) + val field = maskKey(3) + if (maskKey(1) == labelMask && !heapEntrySet.exists(bhe => + (bhe.reference.nonEmpty && bhe.field.nonEmpty && bhe.reference(0) == reference && bhe.field(0) == field) || + (bhe.reference.length > 1 && bhe.reference(0) == reference && bhe.reference(1) == field))) { + val tempPerm: Option[Rational] = detHeapEntryPermission(permMap, perm) + val typ: HeapEntryType = detHeapType(model, qpMaskSet, field, labelMask) + val value = heapOp.getOrElse(Seq("MapType0Select", labelHeap, reference, field), "#undefined") + if (typ == FieldType || typ == QPFieldType) { + heapEntrySet += RawHeapEntry(Seq(reference), Seq(field), value, tempPerm, typ, None) + } else if (typ == PredicateType || typ == QPPredicateType) { + val insidePred = if (value == "#undefined") Map[ast.Exp, ModelEntry]() else evalInsidePredicate(value, field, predicateFinder, predByName, model) + heapEntrySet += RawHeapEntry(Seq(reference, field), predContentMap.getOrElse(field, Seq()), value, tempPerm, typ, Some(insidePred)) + } else if (typ == MagicWandType || typ == QPMagicWandType) { + heapEntrySet += RawHeapEntry(Seq(reference, field), mwContentMap.getOrElse(field, Seq()), value, tempPerm, typ, None) } } } @@ -978,7 +870,7 @@ object CarbonRawCounterexample { /** * Extract all the functions occuring inside of a domain. */ - def getAllFunctions(model: Model, program: ast.Program, heapInstances: Seq[(String, String, String, String)]): Seq[BasicFunctionEntry] = { + def getAllFunctions(model: Model, program: ast.Program, heapInstances: Seq[(String, String)]): Seq[BasicFunctionEntry] = { val funcs = program.collect { case f: ast.Function => f } @@ -988,7 +880,7 @@ object CarbonRawCounterexample { /** * Determine all the inputs and outputs combinations of a function occruing the counterexample model. */ - def detFunction(model: Model, func: ast.FuncLike, genmap: scala.collection.immutable.Map[ast.TypeVar, ast.Type], heapInst: Seq[(String, String, String, String)], program: ast.Program, hd: Boolean): BasicFunctionEntry = { + def detFunction(model: Model, func: ast.FuncLike, genmap: scala.collection.immutable.Map[ast.TypeVar, ast.Type], heapInst: Seq[(String, String)], program: ast.Program, hd: Boolean): BasicFunctionEntry = { val fname = func.name val resTyp: ast.Type = func.typ val argTyp: Seq[ast.Type] = func.formalArgs.map(x => x.typ) @@ -998,7 +890,7 @@ object CarbonRawCounterexample { if (hd) { for ((k, v) <- m) { var hName = k.head.toString - for ((h, _, i, _) <- heapInst) { + for ((h, i) <- heapInst) { if (i == hName) { hName = h } diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultStateModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultStateModule.scala index 765a0efc..0edcb090 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultStateModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultStateModule.scala @@ -95,7 +95,10 @@ class DefaultStateModule(val verifier: Verifier) extends StateModule { def initOldState: Stmt = { val freshSnapshot = freshTempStateKeepCurrentAux("old", true) curOldState = freshSnapshot._1 - initToCurrentStmt(freshSnapshot) + // At this point the current state (Heap, Mask) still holds the pre-state values that "old" + // refers to, so capture it under the label "old" (see assumeGoodState for how captureState is + // used). The counterexample extractor reads the pre-state heap/mask from this block. + initToCurrentStmt(freshSnapshot) ++ Assume(currentGoodState, Map("captureState" -> "old")) } diff --git a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala index 5e30c76c..f917d562 100644 --- a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala +++ b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala @@ -159,6 +159,12 @@ trait BoogieInterface { for ((_, vars) <- capturedStates; (v, value) <- vars if value.trim.nonEmpty) current(v) = value.trim for (v <- Seq("Heap", "Mask"); value <- current.get(v)) parsingModel.get.append(s"__captureState__current__$v -> $value\n") + // The pre-state ("old") is captured under a label starting with "old" (Boogie may + // freshen it to old$0 etc.; only the failing method's block is emitted, so there is at + // most one). Inject its Heap/Mask so the extractor can report the "old" heap directly. + for ((_, vars) <- capturedStates.find(_._1.startsWith("old")); + v <- Seq("Heap", "Mask"); value <- vars.get(v) if value.trim.nonEmpty) + parsingModel.get.append(s"__captureState__old__$v -> ${value.trim}\n") } models.append(parsingModel.get.toString()) parsingModel = None From d9bb6d1b6bb22ce3e5907de5165a875f22dd66d8 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Wed, 15 Jul 2026 18:12:42 +0200 Subject: [PATCH 9/9] Counterexample extraction for maps, some robustness improvements --- silver | 2 +- .../boogie/CarbonResolvedCounterexample.scala | 150 ++++++++++++++++-- 2 files changed, 142 insertions(+), 10 deletions(-) diff --git a/silver b/silver index 6e787acf..f2f1796b 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 6e787acf8e41e504cd38e10391a2de7186bb6f86 +Subproject commit f2f1796be9c3d67cb0e55d0b9e861aab40ce48ba diff --git a/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala b/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala index d825fc4f..6024290a 100644 --- a/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala +++ b/src/main/scala/viper/carbon/boogie/CarbonResolvedCounterexample.scala @@ -65,6 +65,7 @@ case class CarbonRawCounterexample(ve: VerificationError, val allSequences = CarbonRawCounterexample.detSequences(originalEntries) val allSets = CarbonRawCounterexample.detSets(originalEntries) val allMultisets = CarbonRawCounterexample.detMultisets(originalEntries) + val allMaps = CarbonRawCounterexample.detMaps(originalEntries) val workingModel = CarbonRawCounterexample.buildNewModel(originalEntries.entries) val (hmLabels, heapInstances) = CarbonRawCounterexample.oldAndReturnHeapMask(workingModel, otherDeclarations) @@ -243,7 +244,10 @@ object CarbonRawCounterexample { } else if (opName == "Seq#Index") { res.get(k(0)) match { case Some(x) => - if (!k(1).startsWith("(")) { + // Ignore indices outside the reconstructed sequence: the model can contain spurious + // Seq#Index facts (e.g. from unrelated maps sharing the encoding) whose index exceeds + // the sequence's length, which would make `updated` throw. + if (!k(1).startsWith("(") && k(1).toInt >= 0 && k(1).toInt < x.length) { res += (k(0) -> x.updated(k(1).toInt, v)) found = true } @@ -298,12 +302,13 @@ object CarbonRawCounterexample { if (opName == "MapType2Select") { if (opValues.isInstanceOf[MapEntry]) { for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { - if (v.toString.toBoolean) { - if (k(1).toString.startsWith("T@U!val!")) { - res += (k(0).toString -> Set()) - } else { - res += (k(0).toString -> Set()) - } + // MapType2Select is the Boogie select used for set membership (Set = [T]Bool), but the + // same numbered map type can be shared with other maps whose selects return non-boolean + // (boxed) values. Only a value denoting `true` (possibly a boxed boolean) marks + // membership; anything else is ignored. Using isTrueValue instead of `.toBoolean` avoids + // throwing on e.g. "T@U!val!15" while still recognising a boxed true. + if (isTrueValue(v.toString, model)) { + res += (k(0).toString -> Set()) } } } @@ -331,11 +336,11 @@ object CarbonRawCounterexample { } else if (opName == "MapType2Select") { res.get(k(0)) match { case Some(x) => - if (v.toBoolean && !k(1).startsWith("T@U!val!")) { + if (isTrueValue(v, model) && !k(1).startsWith("T@U!val!")) { res += (k(0) -> x.union(Set(k(1)))) } case None => - if (v.toBoolean && !k(1).startsWith("T@U!val!")) { + if (isTrueValue(v, model) && !k(1).startsWith("T@U!val!")) { res += (k(0) -> Set(k(1))) } else { res += (k(0) -> Set()) @@ -495,6 +500,133 @@ object CarbonRawCounterexample { ans } + /** + * Reconstructs map values from the Boogie model, analogously to [[detSets]]. A map is built up + * from the empty map `Map#Empty` by a chain of `Map#Build(m, k, v)` operations, each of which + * adds (or overwrites) the binding k -> v. Boogie map value ids carry no type information, so the + * key/value literals are inferred. + */ + def detMaps(model: Model): Seq[CECollection] = { + var res = Map[String, scala.collection.immutable.Map[String, String]]() + // Seed empty maps: Map#Empty is the empty map for some key/value type (its arguments are the + // type parameters, which we ignore), and any map whose cardinality is zero is empty as well. + for ((opName, opValues) <- model.entries) { + if (opName == "Map#Empty") { + opValues match { + case me: MapEntry => for ((_, v) <- me.options) res += (v.toString -> scala.collection.immutable.Map.empty) + case ce: ConstantEntry if ce.value != "false" && ce.value != "true" => res += (ce.value -> scala.collection.immutable.Map.empty) + case _ => + } + } + if (opName == "Map#Card") { + opValues match { + case me: MapEntry => for ((k, v) <- me.options) if (v.toString.startsWith("0")) res += (k(0).toString -> scala.collection.immutable.Map.empty) + case _ => + } + } + } + // Collect the build facts Map#Build(base, key, value) = result. + var tempMap = Map[Seq[String], String]() + for ((opName, opValues) <- model.entries) { + if (opName == "Map#Build") { + opValues match { + case me: MapEntry => for ((k, v) <- me.options) tempMap += (k.map(x => x.toString) -> v.toString) + case _ => + } + } + } + // Apply builds to a fixpoint: a result map becomes known as soon as its base map is known. + var progress = true + while (tempMap.nonEmpty && progress) { + progress = false + for ((k, v) <- tempMap) { + res.get(k(0)) match { + case Some(base) => + res += (v -> base.updated(k(1), k(2))) + tempMap -= k + progress = true + case None => // + } + } + } + // Maps that are not built from a Map#Build chain (e.g. a bare parameter constrained only via + // `m[k] == v` / `k in domain(m)`) have no entry above. Reconstruct them from `Map#Domain(m)` (a + // set) and `Map#Elements(m)` (the underlying [K]V map): a two-argument `MapType*Select(setId, k) + // == true` marks k as a domain key, and `MapType*Select(elemsId, k)` gives its value. Only keys + // in the domain that also have a value are shown (analogous to a partial set listing known + // members). The Boogie map-type numbering is program-dependent, so all `MapType*Select` + // functions are scanned. + val mapDomain = model.entries.get("Map#Domain") match { + case Some(me: MapEntry) => me.options.collect { case (k, v) if k.nonEmpty => (k(0).toString, v.toString) } + case _ => Map.empty[String, String] + } + if (mapDomain.nonEmpty) { + val mapElements = model.entries.get("Map#Elements") match { + case Some(me: MapEntry) => me.options.collect { case (k, v) if k.nonEmpty => (k(0).toString, v.toString) } + case _ => Map.empty[String, String] + } + var setMembers = Map[String, Set[String]]() + var selectVals = Map[(String, String), String]() + for ((opName, opValues) <- model.entries if opName.startsWith("MapType") && opName.endsWith("Select")) { + opValues match { + case me: MapEntry => for ((k, v) <- me.options if k.length == 2) { + selectVals += ((k(0).toString, k(1).toString) -> v.toString) + if (isTrueValue(v.toString, model)) setMembers += (k(0).toString -> (setMembers.getOrElse(k(0).toString, Set.empty) + k(1).toString)) + } + case _ => + } + } + for ((mapId, domainSetId) <- mapDomain if !res.contains(mapId)) { + val elemsMapId = mapElements.getOrElse(mapId, "") + val entries = setMembers.getOrElse(domainSetId, Set.empty).flatMap(key => + selectVals.get((elemsMapId, key)).map(value => key -> value)).toMap + res += (mapId -> entries) + } + } + var ans = Seq[CECollection]() + res.foreach { + case (n, m) => + val maplets: Seq[ast.Exp] = m.toSeq.map { case (k, v) => + ast.Maplet(CounterexampleValue.literal(decodeBoxedValue(k, model), None), + CounterexampleValue.literal(decodeBoxedValue(v, model), None))() + } + val value = if (maplets.isEmpty) ast.EmptyMap(ast.InternalType, ast.InternalType)() + else ast.ExplicitMap(maplets)() + ans +:= CECollection(n, value) + } + ans + } + + /** + * Boogie boxes values of a generic type as opaque `T@U` constants. The model records the + * correspondence via `U_2_int`/`U_2_bool` (unboxing) and `int_2_U`/`bool_2_U` (boxing). This + * decodes a boxed value to its underlying literal string when the model records it, in either + * direction. Values that are already literals, or that cannot be decoded, are returned unchanged. + */ + def decodeBoxedValue(v: String, model: Model): String = { + if (!v.startsWith("T@U!")) return v + for (fn <- Seq("U_2_int", "U_2_bool")) { + model.entries.get(fn) match { + case Some(me: MapEntry) => + me.options.collectFirst { case (k, r) if k.length == 1 && k(0).toString == v => r.toString } + .foreach(decoded => return decoded) + case _ => + } + } + for (fn <- Seq("int_2_U", "bool_2_U")) { + model.entries.get(fn) match { + case Some(me: MapEntry) => + me.options.collectFirst { case (k, r) if k.length == 1 && r.toString == v => k(0).toString } + .foreach(decoded => return decoded) + case _ => + } + } + v + } + + /** Whether a set-membership select value denotes `true`, also decoding a boxed boolean. */ + def isTrueValue(v: String, model: Model): Boolean = v == "true" || decodeBoxedValue(v, model) == "true" + def detASTTypeFromString(typ: String): Option[Type] = { typ match { case "Int" => Some(ast.Int)