From ba2444763ec66f016fb38063c17b3a8bb7c46898 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 1 Jul 2024 16:27:15 +0200 Subject: [PATCH 1/9] General counterexample extraction by Raoul --- silver | 2 +- .../reporting/CounterexampleGenerator.scala | 1253 +++++++++++++++++ .../scala/rules/SymbolicExecutionRules.scala | 5 +- 3 files changed, 1258 insertions(+), 2 deletions(-) create mode 100644 src/main/scala/reporting/CounterexampleGenerator.scala diff --git a/silver b/silver index 93bc9b751..1528fbe98 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 93bc9b7516a710c8f01438e430058c4a54e20512 +Subproject commit 1528fbe98a197de4e542a3d1140f54686d7c1a86 diff --git a/src/main/scala/reporting/CounterexampleGenerator.scala b/src/main/scala/reporting/CounterexampleGenerator.scala new file mode 100644 index 000000000..e3b62d2a2 --- /dev/null +++ b/src/main/scala/reporting/CounterexampleGenerator.scala @@ -0,0 +1,1253 @@ +package viper.silicon.reporting + +import viper.silver.verifier.{ApplicationEntry, ConstantEntry, MapEntry, Model, ValueEntry} +import viper.silver.ast.{CondExp, Exp, FieldAccessPredicate, LocalVar, Member, NeCmp, Predicate, Program, Resource, Type} +import viper.silver.ast + +import scala.util.Try +import viper.silicon.{Map, state => st} +import viper.silicon.interfaces.state.Chunk +import viper.silicon.resources.{FieldID, PredicateID} +import viper.silicon.state.{BasicChunk, DefaultSymbolConverter, SimpleIdentifier, State, Store, SymbolConverter} +import viper.silicon.state.terms._ +import viper.silicon.state._ +import viper.silicon.decider.TermToSMTLib2Converter +import viper.silicon.interfaces.decider.TermConverter +import viper.silicon.interfaces.SiliconCounterexample +import viper.silicon.reporting.Converter.evaluateTerm +import viper.silver.verifier._ +import viper.silver.verifier.Rational + +/** + * 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(model: Model, internalStore: Store, heap: Iterable[Chunk], oldHeaps: State.OldHeaps, program: ast.Program) extends SiliconCounterexample { + val imCE = IntermediateCounterexampleModel(model, internalStore, heap, oldHeaps, program) + + val (ceStore, refOcc) = CounterexampleGenerator.detStore(internalStore, imCE.basicVariables, imCE.allCollections) + val nameTranslationMap = CounterexampleGenerator.detTranslationMap(ceStore, refOcc) + var ceHeaps = imCE.allBasicHeaps.reverse.map(bh => (bh._1, CounterexampleGenerator.detHeap(bh._2, program, imCE.allCollections, nameTranslationMap, model))) + + 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 + } + + override def withStore(s: Store): SiliconCounterexample = { + CounterexampleGenerator(model, s, heap, oldHeaps, program) + } +} + +/** + * CounterexampleGenerator class used for generating an "interemediate" CE. + */ +case class IntermediateCounterexampleModel(model: Model, internalStore: Store, heap: Iterable[Chunk], oldHeaps: State.OldHeaps, program: ast.Program) extends SiliconCounterexample { + val basicVariables = IntermediateCounterexampleModel.detBasicVariables(model, internalStore) + val allSequences = IntermediateCounterexampleModel.detSequences(model) + val allSets = IntermediateCounterexampleModel.detSets(model) + val allMultisets = IntermediateCounterexampleModel.detMultisets(model) + val allCollections = allSequences ++ allSets ++ allMultisets + var allBasicHeaps = Seq(("current", BasicHeap(IntermediateCounterexampleModel.detHeap(model, heap, program.predicatesByName)))) + oldHeaps.foreach {case (n, h) => allBasicHeaps +:= ((n, BasicHeap(IntermediateCounterexampleModel.detHeap(model, h.values, program.predicatesByName))))} + + val DomainEntries = IntermediateCounterexampleModel.getAllDomains(model, program) + val nonDomainFunctions = IntermediateCounterexampleModel.getAllFunctions(model, program) + + 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.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 + } + + override def withStore(s: Store): SiliconCounterexample = { + CounterexampleGenerator(model, s, heap, oldHeaps, program).imCE + } +} + +object IntermediateCounterexampleModel { + + /** + * Determines the local variables and their value. + */ + def detBasicVariables(model: Model, store: Store): Seq[CEVariable] = { + var res = Seq[CEVariable]() + for ((k, v) <- store.values) { + if (v.toString.contains('@')) { + model.entries.get(v.toString) match { + case Some(x) => + var varTyp: Option[Type] = None + if (k.isInstanceOf[LocalVar]) { + varTyp = Some(k.asInstanceOf[LocalVar].typ) + } + if (x.isInstanceOf[ConstantEntry]) { + res +:= CEVariable(k.name, x, varTyp) + } else if (x.isInstanceOf[ApplicationEntry]) { + res +:= CEVariable(k.name, x, varTyp) + } else { + println(s"Couldn't find a ConstantEntry or ApplicationEntry for the Variable: ${k.name}") + } + case None => // + } + } else { + var varTyp: Option[Type] = None + if (k.isInstanceOf[LocalVar]) { + varTyp = Some(k.asInstanceOf[LocalVar].typ) + } + res +:= CEVariable(k.name, ConstantEntry(v.toString), varTyp) + } + } + if (model.entries.contains("$Ref.null")) { + val nullRef = model.entries.get("$Ref.null").get + if (nullRef.isInstanceOf[ConstantEntry]) { + res +:= CEVariable("null", nullRef, Some(ast.Ref)) + } + } + res + } + + /** + * Defines every sequence that can be extracted in the model. The entries of the sequences still consist of identifiers + * and are not assigned to their actual value. Additionally, not every sequence in the output set will be mentioned + * in the "extended" CE as only sequences that are used in the method containing the verification error will be mentioned there. + */ + 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_singleton" && opName != "Seq_range" && opName.startsWith("Seq_")) { + 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) { + if (k(0).isInstanceOf[ConstantEntry] && k(1).isInstanceOf[ConstantEntry]) { + 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) => + if (!k(1).startsWith("(")) { + res += (v -> x.take(k(1).toInt)) + } + tempMap -= ((opName, k)) + found = true + case _ => // + } + } else if (opName == "Seq_drop") { + res.get(k(0)) match { + case Some(x) => + if (!k(1).startsWith("(")) { + res += (v -> x.drop(k(1).toInt)) + } + tempMap -= ((opName, k)) + found = true + case _ => // + } + } else if (opName == "Seq_index") { + res.get(k(0)) match { + case Some(x) => + if (!k(1).startsWith("(") && (k(1).toInt < x.length)) { + res += (k(0) -> x.updated(k(1).toInt, v)) + } + tempMap -= ((opName, k)) + found = true + case _ => // + } + } else if (opName == "Seq_update") { + res.get(k(0)) match { + case Some(x) => + if (!k(1).startsWith("(")) { + res += (v -> x.updated(k(1).toInt, k(2))) + } + tempMap -= ((opName, k)) + found = true + case _ => // + } + } + } + } + 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 + } + + /** + * Defines every set that can be extracted in the model. The entries of the sets still consist of identifiers + * and are not assigned to their actual value. Additionally, not every set in the output set will be mentioned + * in the "extended" CE as only sets that are used in the method containing the verification error will be mentioned there. + */ + 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()) + } + } + } + } + } + var tempMap = Map[(String, Seq[String]), String]() + for ((opName, opValues) <- model.entries) { + if (opName == "Set_unionone" || opName == "Set_in") { + 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 == "Set_in") { + res.get(k(1)) match { + case Some(x) => + if (v.toBoolean) { + res += (k(1) -> x.union(Set(k(0)))) + } + case None => + if (v.toBoolean) { + res += (k(1) -> Set(k(0))) + } + } + 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) + } + } + } + } + while (!tempMap.isEmpty) { + for (((opName, k), v) <- tempMap) { + val firstSet = res.get(k(0)) + val secondSet = res.get(k(1)) + if (firstSet.isDefined && secondSet.isDefined) { + if (opName == "Set_union") { + res += (v -> firstSet.get.union(secondSet.get)) + tempMap -= ((opName, k)) + } else if (opName == "Set_intersection") { + res += (v -> firstSet.get.intersect(secondSet.get)) + tempMap -= ((opName, k)) + } else if (opName == "Set_difference") { + res += (v -> firstSet.get.diff(secondSet.get)) + 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 + } + var containment = Map[String, Boolean]() + for (e <- s) { + if (e != "#undefined") { + containment += ((e, true)) + } + } + ans += CESet(n, BigInt(s.size), containment, s, typ) + } + ans + } + + /** + * Defines every multiset that can be extracted in the model. The entries of the multisets still consist of identifiers + * and are not assigned to their actual value. Additionally, not every multiset in the output set will be mentioned + * in the "extended" CE as only multisets that are used in the method containing the verification error will be mentioned there. + */ + def detMultisets(model: Model): Set[CEValue] = { + var res = Map[String, scala.collection.immutable.Map[String, Int]]() + for ((opName, opValues) <- model.entries) { + if (opName == "Multiset_empty") { + if (opValues.isInstanceOf[MapEntry]) { + for ((_, 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_count") { + if (opValues.isInstanceOf[MapEntry]) { + for ((k, v) <- opValues.asInstanceOf[MapEntry].options) { + if (!v.toString.startsWith("0")) { + res += (k(0).toString -> res.getOrElse(k(0).toString, scala.collection.immutable.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 + } + + /** + * Translates a string identifier to an actual AST Viper Type. + */ + 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 + } + } + + /** + * Transforms the Heap Chunks to their Viper heap types. + */ + def detHeap(model: Model, h: Iterable[Chunk], predByName: scala.collection.immutable.Map[String, Predicate]): Set[BasicHeapEntry] = { + var heap = Set[BasicHeapEntry]() + h foreach { + case c@BasicChunk(FieldID, _, _, _, _) => + heap += detField(model, c) + case c@BasicChunk(PredicateID, _, _, _, _) => + heap += detPredicate(model, c, predByName) + case c@BasicChunk(id, _, _, _, _) => + println("This Basic Chunk couldn't be matched as a CE heap entry!") + case c: st.QuantifiedFieldChunk => + val fieldName = c.id.name + val fvf = evaluateTerm(c.snapshotMap, model) + val possiblePerm = detPermWithInv(c.perm, model) + model.entries.get(s"$$FVF.lookup_$fieldName") match { + case Some(x) => + for ((k, v) <- x.asInstanceOf[MapEntry].options) { + if (k(0).toString == fvf.toString) { + val reference = k(1) + val value = v.toString + val tempPerm = possiblePerm._2 + heap += BasicHeapEntry(Seq(reference.toString), Seq(fieldName), value, tempPerm, QPFieldType, None) + } + } + case None => //println(s"There is no QF with the snapshot: ${c.snapshotMap}") + } + case c: st.QuantifiedPredicateChunk => + val predName = c.id.name + val fvf = evaluateTerm(c.snapshotMap, model) + val possiblePerm = detPermWithInv(c.perm, model) + var fSeq: Seq[String] = Seq() + if (!possiblePerm._1.isEmpty) { + fSeq = possiblePerm._1.head.map(x => x.toString) + } + heap += BasicHeapEntry(Seq(predName), fSeq, "#undefined", possiblePerm._2, QPPredicateType, None) + case c@MagicWandChunk(_, _, _, _, _) => + heap += detMagicWand(model, c) + case _ => //println("This case is not supported in detHeap") + } + heap + } + + def detField(model: Model, chunk: BasicChunk): BasicHeapEntry = { + val recvVar = evaluateTerm(chunk.args(0), model).toString + val fieldName = chunk.id.name + val value = evaluateTerm(chunk.snap, model).toString + val perm = evalPerm(chunk.perm, model) + BasicHeapEntry(Seq(recvVar), Seq(fieldName), value, perm, FieldType, None) + } + + def detPredicate(model: Model, chunk: BasicChunk, predByName: scala.collection.immutable.Map[String, Predicate]): BasicHeapEntry = { + val predName = chunk.id.name + val references = chunk.args.map(x => evaluateTerm(x, model)) + var snap: Seq[ModelEntry] = Seq() + if (chunk.snap.isInstanceOf[First] || chunk.snap.isInstanceOf[Second] || chunk.snap.isInstanceOf[Var] || chunk.snap.isInstanceOf[Combine]) { + snap = evalSnap(chunk.snap, model: Model) + } + val astPred = predByName.get(predName) + val insidePredicateMap = evalInsidePredicate(snap, astPred) + val perm = evalPerm(chunk.perm, model) + BasicHeapEntry(Seq(predName), references.map(x => x.toString), chunk.snap.toString, perm, PredicateType, Some(insidePredicateMap)) + } + + /** + * Evaluate the snapshot of a predicate. + */ + def evalInsidePredicate(snap: Seq[ModelEntry], astPred: Option[Predicate]): scala.collection.immutable.Map[Exp, ModelEntry] = { + var ans = scala.collection.immutable.Map[Exp, ModelEntry]() + if (astPred.isDefined && !astPred.get.isAbstract) { + val predBody = astPred.get.body.get + val insPred = snapToBody(predBody, snap) + if (snap.length == 0 || (snap.length == 1 && (snap(0).toString.startsWith("$Snap") || snap(0).toString.startsWith("($Snap")))) { + ans = scala.collection.immutable.Map[Exp, ModelEntry]() + } else { + var assignedPredBody = scala.collection.immutable.Map[Exp, ModelEntry]() + for ((exp, value) <- insPred) { + if (value.toString.startsWith("$Snap") || value.toString.startsWith("($Snap")) { + assignedPredBody += evalBody(exp, UnspecifiedEntry, assignedPredBody) + } else { + assignedPredBody += evalBody(exp, value, assignedPredBody) + } + } + ans = assignedPredBody + } + } + ans + } + + /** + * Compare the snapshot of a predicate to its actual body (accessed through its ast node). + */ + def evalBody(exp: Exp, value: ModelEntry, lookup: scala.collection.immutable.Map[Exp, ModelEntry]): (Exp, ModelEntry) = { + exp match { + case FieldAccessPredicate(predAcc, _) => (predAcc, value) + case 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: Exp, lookup: scala.collection.immutable.Map[Exp, ModelEntry]): Boolean = exp match { + case NeCmp(left, right) => !(lookup.getOrElse(left, ConstantEntry(left.toString())).toString.equalsIgnoreCase(lookup.getOrElse(right, ConstantEntry(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 snapToBody(body: Exp, snap: Seq[ModelEntry]): Seq[(Exp, ModelEntry)] = { + if (snap.length == 0) { + Seq() + } else if (snap.length == 1) { + Seq((body, snap(0))) + } else { + if (body.subExps.length == 2) { + Seq((body.subExps(0), snap(0))) ++ snapToBody(body.subExps(1), snap.tail) + } else { + Seq() + } + } + } + + def evalSnap(term: Term, model: Model): Seq[ModelEntry] = term match { + case First(t) => + val subSnap = evalSnap(t, model) + if (subSnap(0).isInstanceOf[ApplicationEntry]) { + Seq(subSnap(0).asInstanceOf[ApplicationEntry].arguments(0)) + } else { + Seq(UnspecifiedEntry) + } + case Second(t) => + val subSnap = evalSnap(t, model) + if (subSnap(0).isInstanceOf[ApplicationEntry]) { + Seq(subSnap(0).asInstanceOf[ApplicationEntry].arguments(1)) + } else { + Seq(UnspecifiedEntry) + } + case Combine(t1, t2) => evalSnap(t1, model) ++ evalSnap(t2, model) + case Var(id, _, _) => Seq(model.entries.getOrElse(id.name, UnspecifiedEntry)) + case SortWrapper(t, s) => Seq(ConstantEntry(t.toString)) + case _ => Seq(UnspecifiedEntry) + } + + /** + * Function used in quantified permissions: + * Checks the validity of the permission expression for every possible combination of inputs (possible + * inputs are given in the inverse functions of the counterexample from the SMT solver. + */ + def detPermWithInv(perm: Term, model: Model): (Seq[Seq[ValueEntry]], Option[Rational]) = { + val check = "^inv@[0-9]+@[0-9]+\\([^)]*\\)$" + val (originals, replacements) = detTermReplacement(perm, check).toSeq.unzip + val newPerm = perm.replace(originals, replacements) + var allInvParameters = Map[Term, Map[Seq[ValueEntry], ValueEntry]]() + for (inv <- replacements) { + model.entries.get(inv.toString) match { + case Some(x) => + var tempMap = Map[Seq[ValueEntry], ValueEntry]() + for ((input, output) <- x.asInstanceOf[MapEntry].options) { + if (input(0).toString != "else") { + tempMap += (input -> output) + } + } + allInvParameters += (inv -> tempMap) + case None => println(s"There is no Inverse Function with the name: ${inv.toString}") + } + } + if (allInvParameters.toSeq.filter(x => x._2.isEmpty).isEmpty) { + val (tempOriginals, predicateInputs, tempReplacements) = allInvParameters.toSeq.map { case x => (x._1, x._2.head._1, Var(SimpleIdentifier(x._2.head._2.toString), x._1.sort, false)) }.unzip3 + val tempPerm = newPerm.replace(tempOriginals, tempReplacements) + val evaluatedTempPerm = evalPerm(tempPerm, model) + (predicateInputs, evaluatedTempPerm) + } else { + val predicateInputs = allInvParameters.toSeq.filter(x => !x._2.isEmpty).map(x => x._2.head._1) + val evaluatedTempPerm = Some(Rational.zero) + (predicateInputs, evaluatedTempPerm) + } + } + + def detTermReplacement(term: Term, pattern: String): Map[Term, Term] = { + if (pattern.r.matches(term.toString)) { + val outIdentifier = SimpleIdentifier(term.toString.split("\\(")(0)) + val outSort = term.asInstanceOf[App].applicable.resultSort + Map(term -> Var(outIdentifier, outSort, false)) + } else { + term.subterms.foldLeft(Map[Term, Term]()) {(acc, x) => (acc ++ detTermReplacement(x, pattern))} + } + } + + def allInvFuncCombinations(allInvParameters: Map[Term, Map[Seq[ValueEntry], ValueEntry]]): Seq[Seq[(Term, Seq[ValueEntry], ValueEntry)]] = { + if (allInvParameters.isEmpty) { + Seq(Seq()) + } else { + val (invFun, inputOutputMap) = allInvParameters.head + val remainingMap = allInvParameters.tail + val remainingCombinations = allInvFuncCombinations(remainingMap) + inputOutputMap.flatMap { inputOutput => remainingCombinations.map((invFun, inputOutput._1, inputOutput._2) +: _)}.toSeq + } + } + + def detMagicWand(model: Model, chunk: MagicWandChunk): BasicHeapEntry = { + val name = chunk.id.toString + var args = Seq[String]() + for (x <- chunk.args) { + val tempArg = evaluateTerm(x, model) + var arg = tempArg.toString + if (tempArg.isInstanceOf[OtherEntry]) { + if (evalTermToModelEntry(x, model).isDefined) { + arg = evalTermToModelEntry(x, model).get.toString + } else if (evalPerm(x, model).isDefined) { + arg = evalPerm(x, model).get.toString + } else { + arg = x.toString + } + } + args ++= Seq(arg) + } + val perm = evalPerm(chunk.perm, model) + BasicHeapEntry(Seq(name), args, "#undefined", perm, MagicWandType, None) + } + + /** + * Evaluates a Term to a Permission (which is represented by a Rational). + */ + def evalPerm(value: Term, model: Model): Option[Rational] = { + value match { + case _: Var => evaluateTerm(value, model) match { + case LitPermEntry(value) => Some(Rational.apply(value.numerator, value.denominator)) + case _ => None + } + case App(applicable, argsSeq) => None + case IntLiteral(n) => Some(Rational.apply(n, 1)) + case NoPerm => Some(Rational.zero) + case FullPerm => Some(Rational.one) + case Null => None + case a:BooleanLiteral => if (a.value) Some(Rational.apply(1, 1)) else Some(Rational.apply(0, 1)) + case _: Quantification => None //not done yet + case Plus(v1, v2) => + val pr1 = evalPerm(v1, model) + val pr2 = evalPerm(v2, model) + if (pr1 != None && pr2 != None) { + val num = pr1.get.numerator*pr2.get.denominator + pr2.get.numerator*pr1.get.denominator + val den = pr1.get.denominator*pr2.get.denominator + Some(Rational.apply(num, den)) + } else { + None + } + case Minus(v1, v2) => + val pr1 = evalPerm(v1, model) + val pr2 = evalPerm(v2, model) + if (pr1 != None && pr2 != None) { + val num = pr1.get.numerator * pr2.get.denominator - pr2.get.numerator * pr1.get.denominator + val den = pr1.get.denominator * pr2.get.denominator + Some(Rational.apply(num, den)) + } else { + None + } + case Times(v1, v2) => + val pr1 = evalPerm(v1, model) + val pr2 = evalPerm(v2, model) + if (pr1 != None && pr2 != None) { + val num = pr1.get.numerator * pr2.get.numerator + val den = pr1.get.denominator * pr2.get.denominator + Some(Rational.apply(num, den)) + } else { + None + } + case Div(v1, v2) => + val pr1 = evalPerm(v1, model) + val pr2 = evalPerm(v2, model) + if (pr1 != None && pr2 != None) { + val num = pr1.get.numerator * pr2.get.denominator + val den = pr1.get.denominator * pr2.get.numerator + Some(Rational.apply(num, den)) + } else { + None + } + case Not(v) => + val pr = evalPerm(v, model) + if (pr != None) { + Some(Rational.apply(1-pr.get.numerator, pr.get.denominator)) + } else { + None + } + case Or(t) => + val evalSeq = t.map(st => + if (evalPerm(st, model) != None) { + Some(evalPerm(st, model).get.numerator) + } else { + None + }) + if (evalSeq.contains(None)) { + None + } else if (evalSeq.contains(Some(BigInt(1)))) { + Some(Rational.one) + } else { + Some(Rational.zero) + } + case And(t) => + val evalSeq = t.map(st => + if (evalPerm(st, model) != None) { + Some(evalPerm(st, model).get.numerator) + } else { + None + }) + if (evalSeq.contains(None)) { + None + } else if (evalSeq.contains(Some(BigInt(0)))) { + Some(Rational.zero) + } else { + Some(Rational.one) + } + case FractionPermLiteral(r) => Some(Rational.apply(r.numerator, r.denominator)) + case FractionPerm(v1, v2) => if (v1.isInstanceOf[IntLiteral] && v2.isInstanceOf[IntLiteral]) Some(Rational(v1.asInstanceOf[IntLiteral].n, v2.asInstanceOf[IntLiteral].n)) else None + case IsValidPermVar(v) => evalPerm(v, model) + case IsReadPermVar(v) => evalPerm(v, model) + case Let(_) => None + case BuiltinEquals(t0, t1) => + val first = evalTermToModelEntry(t0, model) + val second = evalTermToModelEntry(t1, model) + if (first.toString == second.toString) { + Some(Rational.one) + } else { + Some(Rational.zero) + } + case Less(t0, t1) => + val first = + if (evalTermToModelEntry(t0, model).isDefined && evalTermToModelEntry(t0, model).get.toString.forall(Character.isDigit)) { + Some(evalTermToModelEntry(t0, model).get.toString.toInt) + } else { + None + } + val second = + if (evalTermToModelEntry(t1, model).isDefined && evalTermToModelEntry(t1, model).get.toString.forall(Character.isDigit)) { + Some(evalTermToModelEntry(t1, model).get.toString.toInt) + } else { + None + } + if (first.isDefined && second.isDefined && first.get < second.get) { + Some(Rational.one) + } else if (first.isDefined && second.isDefined) { + Some(Rational.zero) + } else { + None + } + case AtMost(t0, t1) => + val first = + if (evalTermToModelEntry(t0, model).isDefined && evalTermToModelEntry(t0, model).get.toString.forall(Character.isDigit)) { + Some(evalTermToModelEntry(t0, model).get.toString.toInt) + } else { + None + } + val second = + if (evalTermToModelEntry(t1, model).isDefined && evalTermToModelEntry(t1, model).get.toString.forall(Character.isDigit)) { + Some(evalTermToModelEntry(t1, model).get.toString.toInt) + } else { + None + } + if (first.isDefined && second.isDefined && first.get <= second.get) { + Some(Rational.one) + } else if (first.isDefined && second.isDefined) { + Some(Rational.zero) + } else { + None + } + case AtLeast(t0, t1) => + val first = + if (evalTermToModelEntry(t0, model).isDefined && evalTermToModelEntry(t0, model).get.toString.forall(Character.isDigit)) { + Some(evalTermToModelEntry(t0, model).get.toString.toInt) + } else { + None + } + val second = + if (evalTermToModelEntry(t1, model).isDefined && evalTermToModelEntry(t1, model).get.toString.forall(Character.isDigit)) { + Some(evalTermToModelEntry(t1, model).get.toString.toInt) + } else { + None + } + if (first.isDefined && second.isDefined && first.get >= second.get) { + Some(Rational.one) + } else if (first.isDefined && second.isDefined) { + Some(Rational.zero) + } else { + None + } + case PermTimes(v1, v2) => + evalPerm(v1, model).flatMap(x => evalPerm(v2, model).map(y => x * y)) + case IntPermTimes(v1, v2) => + evalPerm(v1, model).flatMap(x => evalPerm(v2, model).map(y => x * y)) + case PermIntDiv(v1, v2) => + evalPerm(v1, model).flatMap(x => evalPerm(v2, model).map(y => x / y)) + case PermPlus(v1, v2) => + evalPerm(v1, model).flatMap(x => evalPerm(v2, model).map(y => x + y)) + case PermMinus(v1, v2) => + evalPerm(v1, model).flatMap(x => evalPerm(v2, model).map(y => x - y)) + case PermLess(_, _) => None + case PermAtMost(_, _) => None + case PermMin(_, _) => None + case SortWrapper(t, _) => evalPerm(t, model) + case Distinct(domainFunSet) => None + case Let(bindings, body) => None + // Term cases that are not handled: MagicWandChunkTerm, MagicWandSnapshot, + // PredicateTrigger, PredicateDomain, PredicatePermLookup, PredicateLookup, + // FieldTrigger, Domain, PermLookup, Lookup, + // trait Decl, Applicable, Function + // trait SnapshotTerm + // trait SetTerm, MapTerm, MultisetTerm + case Ite(t, _, _) => evalPerm(t, model) + case SetIn(v, s) => + if (model.entries.get("Set_in").get.isInstanceOf[MapEntry]) { + val setInEntry = model.entries.get("Set_in").get.asInstanceOf[MapEntry] + val lookupEntry = Seq(ConstantEntry(model.entries.getOrElse(v.toString, v).toString), ConstantEntry(model.entries.getOrElse(s.toString, s).toString)) + if (setInEntry.options.contains(lookupEntry)) { + if (setInEntry.options.get(lookupEntry).get.toString.toBoolean) { + Some(Rational.one) + } else { + Some(Rational.zero) + } + } else { + None + } + } else { + None + } + case _ => None + } + } + + /** + * Evaluates a Term to a value of the counterexample from the SMT solver. + */ + def evalTermToModelEntry(value: Term, model: Model): Option[ModelEntry] = { + value match { + case v: Var => + if (v.id.name.contains("@")) { + model.entries.get(v.id.name) + } else { + Some(ConstantEntry(v.id.name)) + } + case a: App => + if (model.entries.get(a.applicable.id.toString).isDefined && model.entries.get(a.applicable.id.toString).get.isInstanceOf[MapEntry]) { + val tempMap = model.entries.get(a.applicable.id.toString).get.asInstanceOf[MapEntry].options + tempMap.get(a.args.map(t => ConstantEntry(t.toString))) + } else { + None + } + case SeqLength(t) => + val seqName = model.entries.get(t.toString) + val tempMap = model.entries.get("Seq_length") + if (seqName.isDefined && tempMap.isDefined && tempMap.get.isInstanceOf[MapEntry]) { + tempMap.get.asInstanceOf[MapEntry].options.get(Seq(ConstantEntry(seqName.get.toString))) + } else { + None + } + case IntLiteral(t) => Some(ConstantEntry(t.intValue.toString)) + case SeqTake(t0, t1) => + if (evalTermToModelEntry(t0, model).isDefined) { + Some(ConstantEntry(evalTermToModelEntry(t0, model).toString ++ " at idx " ++ t1.toString)) + } else { + None + } + case SeqAt(t0, t1) => None + case _ => None + } + } + + lazy val termconverter: TermConverter[String, String, String] = { + val conv = new TermToSMTLib2Converter() + conv.start() + conv + } + lazy val symbolConverter: SymbolConverter = new DefaultSymbolConverter + lazy val snapUnitId: String = termconverter.convert(Unit) + lazy val nullRefId: String = termconverter.convert(Null) + + /** + * 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 concreteDomains = program.collect { // find all definitive type instances + case ast.DomainType(n, map) => (n, map) + case d: ast.DomainFuncApp => (d.domainName, d.typVarMap) // sometimes we use a function without having an actual member of this... + + }.filterNot(x => x._2.values.toSeq.exists(y => y.isInstanceOf[ast.TypeVar])).toSet // make sure we have all possible mappings without duplicates + + val doms: Seq[(ast.Domain, scala.collection.immutable.Map[ast.TypeVar, Type])] = domains.flatMap(x => + if (x.typVars == Nil) { + Seq((x, Map.empty[ast.TypeVar, ast.Type])) + } else { + concreteDomains.filter(_._1 == x.name).map(y => (x, y._2)) + }).toSeq + var domainEntries = Seq[BasicDomainEntry]() + for ((dom, typeMap) <- doms) { + val types = try { + dom.typVars.map(typeMap) + } catch { + case _: Throwable => Seq() + } + val translatedFunctions = dom.functions.map(y => detFunction(model, y, typeMap, program, false)) + domainEntries +:= BasicDomainEntry(dom.name, types, translatedFunctions) + } + domainEntries + } + + /** + * Extract all the functions occuring inside of a domain. + */ + def getAllFunctions(model: Model, program: ast.Program): Seq[BasicFunction] = { + val funcs = program.collect { + case f: ast.Function => f + } + funcs.map(x => detFunction(model, x, Map.empty, 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], program: ast.Program, hd: Boolean): BasicFunction = { + def toSort(typ: ast.Type): Either[Throwable, Sort] = Try(symbolConverter.toSort(typ)).toEither + def toSortWithSubstitutions(typ: ast.Type, typeErrorMsg: String): Either[String, Sort] = { + toSort(typ) + .left + .flatMap(_ => typ match { + case x: ast.GenericType => toSort(x.substitute(genmap)).left.map(_ => typeErrorMsg) + case t: ast.TypeVar => toSort(genmap.apply(t)).left.map(_ => typeErrorMsg) + case _ => Left("type not resolvable") + }) + } + val fname = func.name + val resTyp: ast.Type = func.typ + val argTyp: Seq[ast.Type] = func.formalArgs.map(x => x.typ) + val keys = model.entries.keys + var (argSortErrors, argSort) = func.formalArgs + .map(x => toSortWithSubstitutions(x.typ, s"typeError in arg type ${x.typ}")) + .partitionMap(identity) + if (argSortErrors.nonEmpty) { + return BasicFunction("ERROR", argTyp, resTyp, Map.empty, s"$fname ${argSortErrors.head}") + } + val resSort = toSortWithSubstitutions(resTyp, s"typeError in return type $resTyp") + .fold(err => { + return BasicFunction("ERROR", argTyp, resTyp, Map.empty, s"$fname $err") + }, identity) + val smtfunc = func match { + case t: ast.Function => symbolConverter.toFunction(t).id + case t@ast.BackendFunc(_, _, _, _) => symbolConverter.toFunction(t, program).id + case t: ast.DomainFunc => symbolConverter.toFunction(t, argSort :+ resSort, program).id + } + val kek = smtfunc.toString + .replace("[", "<") + .replace("]", ">") + .replace(", ", "~_") + val modelfname = try { + (keys.filter(_.contains(fname + "%limited")) ++ keys.filter(_ == fname) ++ keys.filter(_ == kek)).head + } catch { + case _: Throwable => return BasicFunction("ERROR", argTyp, resTyp, Map.empty, s"$fname model function not found") + } + var heapStateList = Map[ValueEntry, String]() + var heapStateCounter = 0 + def getTranslatedEntry(x: ValueEntry) : String = { + if (x.toString.startsWith("$")) { + if (heapStateList.contains(x)) { + heapStateList.get(x).get + } else { + val heapStateName = "Heap@" + heapStateCounter.toString + heapStateCounter += 1 + heapStateList += (x -> heapStateName) + heapStateName + } + } else { + x.toString + } + } + model.entries.get(modelfname) match { + case Some(MapEntry(m, els)) => + var options = Map[Seq[String], String]() + if (hd) { + for ((k, v) <- m) { + val temp = k.tail.map(x => heapStateList.getOrElse(x, x.toString)) + options += (Seq(getTranslatedEntry(k.head)) ++ temp -> v.toString) + } + } else { + for ((k, v) <- m) { + val temp: Seq[String] = k.map(x => heapStateList.getOrElse(x, x.toString)) + options += (temp -> 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: Store, variables: Seq[CEVariable], collections: Set[CEValue]): (StoreCounterexample, Map[String, (String, Int)]) = { + var refOccurences = Map[String, (String, Int)]() + var ans = Seq[StoreEntry]() + for ((k, _) <- store.values) { + for (vari <- variables) { + if (k.name == vari.name) { + if (k.typ == ast.Ref) { + if (refOccurences.get(vari.entryValue.toString).isDefined) { + val (n, i) = refOccurences.get(vari.entryValue.toString).get + if (n != k.name) { + refOccurences += (vari.entryValue.toString -> (k.name, i + 1)) + } + } else { + refOccurences += (vari.entryValue.toString -> (k.name, 1)) + } + } + var found = false + for (coll <- collections) { + if (vari.entryValue.toString == coll.id) { + ans +:= StoreEntry(k, coll) + found = true + } + } + if (!found) { + ans +:= StoreEntry(k, 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, _, _) => namesTranslation += (internalName -> 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 + } + + def replace(expression: Exp, repl: scala.collection.immutable.Map[Exp, Exp]): Exp = { + repl.get(expression) match { + case Some(replacement) => replacement + case None => + if (expression.subExps.isEmpty) { + expression + } else { + expression + //expression.subExps.map(x => replace(x, repl)) + } + } + } + + /** + * Match heap resources to their ast node and translate all identifiers (for fields and references) + */ + def detHeap(basicHeap: BasicHeap, program: Program, collections: Set[CEValue], translNames: Map[String, String], model: Model): HeapCounterexample = { + var ans = Seq[(Resource, FinalHeapEntry)]() + for (bhe <- basicHeap.basicHeapEntries) { + bhe.het match { + case FieldType | QPFieldType => + for ((fn, fv) <- program.fieldsByName) { + if (fn == bhe.field.head) { + var found = false + for (coll <- collections) { + if (bhe.valueID == coll.id) { + if (translNames.get(bhe.reference.head).isDefined) { + ans +:= (fv, FieldFinalEntry(translNames.get(bhe.reference.head).get, bhe.field.head, coll, bhe.perm, fv.typ, bhe.het)) + } else { + ans +:= (fv, FieldFinalEntry(bhe.reference.head, bhe.field.head, coll, bhe.perm, fv.typ, bhe.het)) + } + found = true + } + } + if (!found) { + if (translNames.get(bhe.reference.head).isDefined) { + ans +:= (fv, FieldFinalEntry(translNames.get(bhe.reference.head).get, bhe.field.head, CEVariable("#undefined", ConstantEntry(bhe.valueID), Some(fv.typ)), bhe.perm, fv.typ, bhe.het)) + } else { + ans +:= (fv, FieldFinalEntry(bhe.reference.head, bhe.field.head, CEVariable("#undefined", ConstantEntry(bhe.valueID), Some(fv.typ)), bhe.perm, fv.typ, bhe.het)) + } + } + } + } + case PredicateType | QPPredicateType => + for ((pn, pv) <- program.predicatesByName) { + if (pn == bhe.reference.head) { + val refNames = bhe.field.map(x => + if (translNames.get(x).isDefined) { + translNames.get(x).get + } else { + x + }) + var translatedArgs: Option[scala.collection.immutable.Map[Exp, ModelEntry]] = bhe.insidePredicate + if (bhe.insidePredicate.isDefined) { + translatedArgs = Some(bhe.insidePredicate.get.map{case (k,v) => (k, ConstantEntry(translNames.getOrElse(v.toString, model.entries.getOrElse(v.toString, v).toString)))}) + } + ans +:= (pv, PredFinalEntry(bhe.reference.head, refNames, bhe.perm, translatedArgs, bhe.het)) + } + } + case MagicWandType | QPMagicWandType => + var translatedArgs: Seq[String] = bhe.field.map(x => translNames.getOrElse(x, x)) + for ((mw, idx) <- program.magicWandStructures.zipWithIndex) { + val wandName = "wand@" ++ idx.toString + if (bhe.reference(0) == wandName) { + val mwStructure = mw.structure(program, true) + val replacements: Iterable[(ast.Node, ast.Node)] = mwStructure.subexpressionsToEvaluate(program).zip(translatedArgs).map(e => e._1 -> 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) + 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 = { + val translatedFun = fun.options.map { case (in, out) => + (in.map(intName => namesMap.getOrElse(intName, intName)), namesMap.getOrElse(out, out)) + } + val translatedEls = namesMap.getOrElse(fun.default, fun.default) + BasicFunction(fun.fname, fun.argtypes, fun.returnType, translatedFun, translatedEls) + } +} \ No newline at end of file diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala index 243b44065..39d039fe7 100644 --- a/src/main/scala/rules/SymbolicExecutionRules.scala +++ b/src/main/scala/rules/SymbolicExecutionRules.scala @@ -7,9 +7,10 @@ package viper.silicon.rules import viper.silicon.interfaces.{Failure, SiliconFailureContext, SiliconMappedCounterexample, SiliconNativeCounterexample, SiliconVariableCounterexample} +import viper.silicon.reporting.CounterexampleGenerator import viper.silicon.state.State import viper.silicon.verifier.Verifier -import viper.silver.frontend.{MappedModel, NativeModel, VariablesModel} +import viper.silver.frontend.{ExtendedModel, IntermediateModel, MappedModel, NativeModel, VariablesModel} import viper.silver.verifier.errors.ErrorWrapperWithExampleTransformer import viper.silver.verifier.{Counterexample, CounterexampleTransformer, VerificationError} @@ -40,6 +41,8 @@ trait SymbolicExecutionRules { SiliconVariableCounterexample(s.g, nativeModel) case MappedModel => SiliconMappedCounterexample(s.g, s.h.values, s.oldHeaps, nativeModel, s.program) + case IntermediateModel => CounterexampleGenerator(nativeModel, s.g, s.h.values, s.oldHeaps, s.program).imCE + case ExtendedModel => CounterexampleGenerator(nativeModel, s.g, s.h.values, s.oldHeaps, s.program) } val finalCE = ceTrafo match { case Some(trafo) => trafo.f(ce) From 0906ba2f4413b502cc29a8611c868219813caa8f Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 1 Jul 2024 17:22:08 +0200 Subject: [PATCH 2/9] Partial models option --- src/main/resources/z3config.smt2 | 1 + 1 file changed, 1 insertion(+) diff --git a/src/main/resources/z3config.smt2 b/src/main/resources/z3config.smt2 index e76604147..945d5a6b7 100644 --- a/src/main/resources/z3config.smt2 +++ b/src/main/resources/z3config.smt2 @@ -25,6 +25,7 @@ (set-option :smt.qi.eager_threshold 100) (set-option :smt.arith.solver 2) (set-option :model.v2 true) +(set-option :model.partial true) ; We want unlimited multipatterns (set-option :smt.qi.max_multi_patterns 1000) From 59acea6de0e5681e3ed97ef0316aa8f4ad9d3935 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Wed, 12 Feb 2025 13:36:40 +0100 Subject: [PATCH 3/9] Merge --- .../scala/reporting/CounterexampleGenerator.scala | 14 +++++++------- ...Tests.scala => MappedCounterexampleTests.scala} | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) rename src/test/scala/{CounterexampleTests.scala => MappedCounterexampleTests.scala} (99%) diff --git a/src/main/scala/reporting/CounterexampleGenerator.scala b/src/main/scala/reporting/CounterexampleGenerator.scala index e3b62d2a2..90e075afc 100644 --- a/src/main/scala/reporting/CounterexampleGenerator.scala +++ b/src/main/scala/reporting/CounterexampleGenerator.scala @@ -499,11 +499,11 @@ object IntermediateCounterexampleModel { def detHeap(model: Model, h: Iterable[Chunk], predByName: scala.collection.immutable.Map[String, Predicate]): Set[BasicHeapEntry] = { var heap = Set[BasicHeapEntry]() h foreach { - case c@BasicChunk(FieldID, _, _, _, _) => + case c@BasicChunk(FieldID, _, _, _, _, _, _, _) => heap += detField(model, c) - case c@BasicChunk(PredicateID, _, _, _, _) => + case c@BasicChunk(PredicateID, _, _, _, _, _, _, _) => heap += detPredicate(model, c, predByName) - case c@BasicChunk(id, _, _, _, _) => + case c@BasicChunk(id, _, _, _, _, _, _, _) => println("This Basic Chunk couldn't be matched as a CE heap entry!") case c: st.QuantifiedFieldChunk => val fieldName = c.id.name @@ -530,7 +530,7 @@ object IntermediateCounterexampleModel { fSeq = possiblePerm._1.head.map(x => x.toString) } heap += BasicHeapEntry(Seq(predName), fSeq, "#undefined", possiblePerm._2, QPPredicateType, None) - case c@MagicWandChunk(_, _, _, _, _) => + case c@MagicWandChunk(_, _, _, _, _, _, _) => heap += detMagicWand(model, c) case _ => //println("This case is not supported in detHeap") } @@ -606,8 +606,8 @@ object IntermediateCounterexampleModel { } def evalExp(exp: Exp, lookup: scala.collection.immutable.Map[Exp, ModelEntry]): Boolean = exp match { - case NeCmp(left, right) => !(lookup.getOrElse(left, ConstantEntry(left.toString())).toString.equalsIgnoreCase(lookup.getOrElse(right, ConstantEntry(right.toString())).toString)) - case ast.EqCmp(left, right) => (lookup.getOrElse(left, ConstantEntry(left.toString())).toString.equalsIgnoreCase(lookup.getOrElse(right, ConstantEntry(right.toString())).toString)) + case NeCmp(left, right) => !(lookup.getOrElse(left, ConstantEntry(left.toString)).toString.equalsIgnoreCase(lookup.getOrElse(right, ConstantEntry(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 } @@ -816,7 +816,7 @@ object IntermediateCounterexampleModel { } case FractionPermLiteral(r) => Some(Rational.apply(r.numerator, r.denominator)) case FractionPerm(v1, v2) => if (v1.isInstanceOf[IntLiteral] && v2.isInstanceOf[IntLiteral]) Some(Rational(v1.asInstanceOf[IntLiteral].n, v2.asInstanceOf[IntLiteral].n)) else None - case IsValidPermVar(v) => evalPerm(v, model) + case IsValidPermVal(v) => evalPerm(v, model) case IsReadPermVar(v) => evalPerm(v, model) case Let(_) => None case BuiltinEquals(t0, t1) => diff --git a/src/test/scala/CounterexampleTests.scala b/src/test/scala/MappedCounterexampleTests.scala similarity index 99% rename from src/test/scala/CounterexampleTests.scala rename to src/test/scala/MappedCounterexampleTests.scala index c165f97df..616fb9a29 100644 --- a/src/test/scala/CounterexampleTests.scala +++ b/src/test/scala/MappedCounterexampleTests.scala @@ -18,7 +18,7 @@ import viper.silver.verifier.{FailureContext, VerificationError} import java.nio.file.Path -class CounterexampleTests extends SiliconTests { +class MappedCounterexampleTests extends SiliconTests { override val testDirectories: Seq[String] = Seq("counterexamples") override def configureVerifiersFromConfigMap(configMap: Map[String, Any]): Unit = { From 77cc77b6eb1a89580ada1202d418a311736d1ed3 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Fri, 29 Aug 2025 17:33:45 +0200 Subject: [PATCH 4/9] Getting tests to run --- silver | 2 +- ...tor.scala => ExtendedCounterexample.scala} | 26 +++++++++---------- .../scala/rules/SymbolicExecutionRules.scala | 6 ++--- .../scala/MappedCounterexampleTests.scala | 8 +++--- 4 files changed, 21 insertions(+), 21 deletions(-) rename src/main/scala/reporting/{CounterexampleGenerator.scala => ExtendedCounterexample.scala} (97%) diff --git a/silver b/silver index 028ab0322..469ec6691 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 028ab0322c4c99a821ae2e6b1620c6fa2d0e1b06 +Subproject commit 469ec669130fdfe731b5870d8ad2a5c0321dd6b6 diff --git a/src/main/scala/reporting/CounterexampleGenerator.scala b/src/main/scala/reporting/ExtendedCounterexample.scala similarity index 97% rename from src/main/scala/reporting/CounterexampleGenerator.scala rename to src/main/scala/reporting/ExtendedCounterexample.scala index 90e075afc..5f76fdf6a 100644 --- a/src/main/scala/reporting/CounterexampleGenerator.scala +++ b/src/main/scala/reporting/ExtendedCounterexample.scala @@ -26,14 +26,14 @@ import viper.silver.verifier.Rational /** * CounterexampleGenerator class used for generating an "extended" CE. */ -case class CounterexampleGenerator(model: Model, internalStore: Store, heap: Iterable[Chunk], oldHeaps: State.OldHeaps, program: ast.Program) extends SiliconCounterexample { +case class ExtendedCounterexample(model: Model, internalStore: Store, heap: Iterable[Chunk], oldHeaps: State.OldHeaps, program: ast.Program) extends SiliconCounterexample { val imCE = IntermediateCounterexampleModel(model, internalStore, heap, oldHeaps, program) - val (ceStore, refOcc) = CounterexampleGenerator.detStore(internalStore, imCE.basicVariables, imCE.allCollections) - val nameTranslationMap = CounterexampleGenerator.detTranslationMap(ceStore, refOcc) - var ceHeaps = imCE.allBasicHeaps.reverse.map(bh => (bh._1, CounterexampleGenerator.detHeap(bh._2, program, imCE.allCollections, nameTranslationMap, model))) - - val domainsAndFunctions = CounterexampleGenerator.detTranslatedDomains(imCE.DomainEntries, nameTranslationMap) ++ CounterexampleGenerator.detTranslatedFunctions(imCE.nonDomainFunctions, nameTranslationMap) + val (ceStore, refOcc) = ExtendedCounterexample.detStore(internalStore, imCE.basicVariables, imCE.allCollections) + val nameTranslationMap = ExtendedCounterexample.detTranslationMap(ceStore, refOcc) + val ceHeaps = imCE.allBasicHeaps.reverse.map(bh => (bh._1, ExtendedCounterexample.detHeap(bh._2, program, imCE.allCollections, nameTranslationMap, model))) + lazy val heaps = ceHeaps.toMap + val domainsAndFunctions = ExtendedCounterexample.detTranslatedDomains(imCE.DomainEntries, nameTranslationMap) ++ ExtendedCounterexample.detTranslatedFunctions(imCE.nonDomainFunctions, nameTranslationMap) override def toString: String = { var finalString = " Extended Counterexample: \n" finalString += " Store: \n" @@ -49,7 +49,7 @@ case class CounterexampleGenerator(model: Model, internalStore: Store, heap: Ite } override def withStore(s: Store): SiliconCounterexample = { - CounterexampleGenerator(model, s, heap, oldHeaps, program) + ExtendedCounterexample(model, s, heap, oldHeaps, program) } } @@ -87,7 +87,7 @@ case class IntermediateCounterexampleModel(model: Model, internalStore: Store, h } override def withStore(s: Store): SiliconCounterexample = { - CounterexampleGenerator(model, s, heap, oldHeaps, program).imCE + ExtendedCounterexample(model, s, heap, oldHeaps, program).imCE } } @@ -98,7 +98,7 @@ object IntermediateCounterexampleModel { */ def detBasicVariables(model: Model, store: Store): Seq[CEVariable] = { var res = Seq[CEVariable]() - for ((k, v) <- store.values) { + for ((k, (v, _)) <- store.values) { if (v.toString.contains('@')) { model.entries.get(v.toString) match { case Some(x) => @@ -1101,7 +1101,7 @@ object IntermediateCounterexampleModel { } } -object CounterexampleGenerator { +object ExtendedCounterexample { /** * Combine a local variable with its ast node. */ @@ -1184,7 +1184,7 @@ object CounterexampleGenerator { var found = false for (coll <- collections) { if (bhe.valueID == coll.id) { - if (translNames.get(bhe.reference.head).isDefined) { + if (false && translNames.get(bhe.reference.head).isDefined) { ans +:= (fv, FieldFinalEntry(translNames.get(bhe.reference.head).get, bhe.field.head, coll, bhe.perm, fv.typ, bhe.het)) } else { ans +:= (fv, FieldFinalEntry(bhe.reference.head, bhe.field.head, coll, bhe.perm, fv.typ, bhe.het)) @@ -1193,7 +1193,7 @@ object CounterexampleGenerator { } } if (!found) { - if (translNames.get(bhe.reference.head).isDefined) { + if (false && translNames.get(bhe.reference.head).isDefined) { ans +:= (fv, FieldFinalEntry(translNames.get(bhe.reference.head).get, bhe.field.head, CEVariable("#undefined", ConstantEntry(bhe.valueID), Some(fv.typ)), bhe.perm, fv.typ, bhe.het)) } else { ans +:= (fv, FieldFinalEntry(bhe.reference.head, bhe.field.head, CEVariable("#undefined", ConstantEntry(bhe.valueID), Some(fv.typ)), bhe.perm, fv.typ, bhe.het)) @@ -1205,7 +1205,7 @@ object CounterexampleGenerator { for ((pn, pv) <- program.predicatesByName) { if (pn == bhe.reference.head) { val refNames = bhe.field.map(x => - if (translNames.get(x).isDefined) { + if (false && translNames.get(x).isDefined) { translNames.get(x).get } else { x diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala index 6537806b5..e08925a5f 100644 --- a/src/main/scala/rules/SymbolicExecutionRules.scala +++ b/src/main/scala/rules/SymbolicExecutionRules.scala @@ -8,7 +8,7 @@ package viper.silicon.rules import viper.silicon.debugger.DebugExp import viper.silicon.interfaces.{Failure, SiliconDebuggingFailureContext, SiliconFailureContext, SiliconMappedCounterexample, SiliconNativeCounterexample, SiliconVariableCounterexample} -import viper.silicon.reporting.CounterexampleGenerator +import viper.silicon.reporting.ExtendedCounterexample import viper.silicon.state.State import viper.silicon.state.terms.{False, Term} import viper.silicon.verifier.Verifier @@ -70,8 +70,8 @@ trait SymbolicExecutionRules { SiliconVariableCounterexample(s.g, nativeModel) case MappedModel => SiliconMappedCounterexample(s.g, s.h.values, s.oldHeaps, nativeModel, s.program) - case IntermediateModel => CounterexampleGenerator(nativeModel, s.g, s.h.values, s.oldHeaps, s.program).imCE - case ExtendedModel => CounterexampleGenerator(nativeModel, s.g, s.h.values, s.oldHeaps, s.program) + case IntermediateModel => ExtendedCounterexample(nativeModel, s.g, s.h.values, s.oldHeaps, s.program).imCE + case ExtendedModel => ExtendedCounterexample(nativeModel, s.g, s.h.values, s.oldHeaps, s.program) } val finalCE = ceTrafo match { case Some(trafo) => trafo.f(ce) diff --git a/src/test/scala/MappedCounterexampleTests.scala b/src/test/scala/MappedCounterexampleTests.scala index e6029aa48..5e624f383 100644 --- a/src/test/scala/MappedCounterexampleTests.scala +++ b/src/test/scala/MappedCounterexampleTests.scala @@ -53,7 +53,7 @@ class MappedCounterexampleTests extends SiliconTests { override val outputIdPattern: String = "([^:]*)(:([^,]*))?" private def isExpectedCounterexample(annotation: String, file: Path, lineNr: Int): Option[TestAnnotation] = { - def parseExpectedCounterexample(id: OutputAnnotationId, expectedCounterexampleString: String): Option[ExpectedCounterexampleAnnotation] = { + def parseExpectedCounterexample(id: OutputAnnotationId, expectedCounterexampleString: String): Option[ExpectedMappedCounterexampleAnnotation] = { // in order to reuse as much of the existing Viper parser as possible, we have to initialize the `_file` and `_line_offset` fields: val fp = new FastParser() fp._file = file.toAbsolutePath @@ -68,7 +68,7 @@ class MappedCounterexampleTests extends SiliconTests { val cParser = new CounterexampleParser(fp) // now parsing is actually possible: fastparse.parse(expectedCounterexampleString, cParser.expectedCounterexample(_)) match { - case Parsed.Success(expectedCounterexample, _) => Some(ExpectedCounterexampleAnnotation(id, file, lineNr, expectedCounterexample)) + case Parsed.Success(expectedCounterexample, _) => Some(ExpectedMappedCounterexampleAnnotation(id, file, lineNr, expectedCounterexample)) case Parsed.Failure(_, _, extra) => println(s"Parsing expected counterexample failed in file $file: ${extra.trace().longAggregateMsg}") None @@ -88,7 +88,7 @@ class MappedCounterexampleTests extends SiliconTests { } /** represents an expected output (identified by `id`) with an associated (possibly partial) counterexample model */ -case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path, forLineNr: Int, expectedCounterexample: ExpectedCounterexample) extends CustomAnnotation { +case class ExpectedMappedCounterexampleAnnotation(id: OutputAnnotationId, file: Path, forLineNr: Int, expectedCounterexample: ExpectedCounterexample) extends CustomAnnotation { override def matches(actual: AbstractOutput): Boolean = id.matches(actual.fullId) && actual.isSameLine(file, forLineNr) && containsModel(actual) @@ -164,5 +164,5 @@ case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path, override def notFoundError: TestError = TestCustomError(s"Expected the following counterexample on line $forLineNr: $expectedCounterexample") - override def withForLineNr(line: Int = forLineNr): ExpectedCounterexampleAnnotation = ExpectedCounterexampleAnnotation(id, file, line, expectedCounterexample) + override def withForLineNr(line: Int = forLineNr): ExpectedMappedCounterexampleAnnotation = ExpectedMappedCounterexampleAnnotation(id, file, line, expectedCounterexample) } From b87c241f7d8748dabce76eea30db65f04c54e0af Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Fri, 29 Aug 2025 17:40:56 +0200 Subject: [PATCH 5/9] Adding new test class --- silver | 2 +- .../resources/counterexamples/cyclic-ref.vpr | 13 -- .../resources/counterexamples/functions.vpr | 16 -- src/test/resources/counterexamples/lseg.vpr | 27 --- .../resources/counterexamples/method-call.vpr | 19 -- .../resources/counterexamples/negative.vpr | 10 - .../resources/counterexamples/permissions.vpr | 11 - .../resources/counterexamples/predicate.vpr | 27 --- .../counterexamples/ref-sequence.vpr | 12 - .../resources/counterexamples/sequence.vpr | 14 -- .../counterexamples/simple-refs-rec.vpr | 27 --- .../resources/counterexamples/simple-refs.vpr | 21 -- .../scala/GeneralCounterexampleTests.scala | 210 ++++++++++++++++++ 13 files changed, 211 insertions(+), 198 deletions(-) delete mode 100644 src/test/resources/counterexamples/cyclic-ref.vpr delete mode 100644 src/test/resources/counterexamples/functions.vpr delete mode 100644 src/test/resources/counterexamples/lseg.vpr delete mode 100644 src/test/resources/counterexamples/method-call.vpr delete mode 100644 src/test/resources/counterexamples/negative.vpr delete mode 100644 src/test/resources/counterexamples/permissions.vpr delete mode 100644 src/test/resources/counterexamples/predicate.vpr delete mode 100644 src/test/resources/counterexamples/ref-sequence.vpr delete mode 100644 src/test/resources/counterexamples/sequence.vpr delete mode 100644 src/test/resources/counterexamples/simple-refs-rec.vpr delete mode 100644 src/test/resources/counterexamples/simple-refs.vpr create mode 100644 src/test/scala/GeneralCounterexampleTests.scala diff --git a/silver b/silver index 469ec6691..d15460f9b 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 469ec669130fdfe731b5870d8ad2a5c0321dd6b6 +Subproject commit d15460f9bc3e8b94a9d86cb266e736cc7dcb72e1 diff --git a/src/test/resources/counterexamples/cyclic-ref.vpr b/src/test/resources/counterexamples/cyclic-ref.vpr deleted file mode 100644 index d7d0ef13e..000000000 --- a/src/test/resources/counterexamples/cyclic-ref.vpr +++ /dev/null @@ -1,13 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -field next: Ref - -method foo(a: Ref, b: Ref) - requires acc(a.next) && acc(b.next) -{ - a.next := b - b.next := a - //:: ExpectedCounterexample(assert.failed:assertion.false, (a.next.next == a, b == b.next.next)) - assert(false) -} diff --git a/src/test/resources/counterexamples/functions.vpr b/src/test/resources/counterexamples/functions.vpr deleted file mode 100644 index 7cff7b254..000000000 --- a/src/test/resources/counterexamples/functions.vpr +++ /dev/null @@ -1,16 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -function foo(z: Int): Int -{ - 42 -} - -method bar() - requires foo(3) == 42 -{ - var x: Int := 5 - var y: Int := foo(x) - //:: ExpectedCounterexample(assert.failed:assertion.false, (x == 5, y == 42)) - assert(false) -} diff --git a/src/test/resources/counterexamples/lseg.vpr b/src/test/resources/counterexamples/lseg.vpr deleted file mode 100644 index 3efc72126..000000000 --- a/src/test/resources/counterexamples/lseg.vpr +++ /dev/null @@ -1,27 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -field elem : Int -field next : Ref - -predicate lseg(first: Ref, last: Ref, values: Seq[Int]) -{ - first != last ==> - acc(first.elem) && acc(first.next) && - 0 < |values| && - first.elem == values[0] && - lseg(first.next, last, values[1..]) -} - -method removeFirst(first: Ref, last: Ref, values: Seq[Int]) returns (value: Int, second: Ref) - requires lseg(first, last, values) - requires first != last - ensures lseg(second, last, values[1..]) - // we have insufficient field permissions when second is equal to last: - //:: ExpectedCounterexample(not.wellformed:insufficient.permission, (second == last)) - ensures value != unfolding lseg(second, last, values[1..]) in second.elem -{ - unfold lseg(first, last, values) - value := first.elem - second := first.next -} diff --git a/src/test/resources/counterexamples/method-call.vpr b/src/test/resources/counterexamples/method-call.vpr deleted file mode 100644 index c4a197b01..000000000 --- a/src/test/resources/counterexamples/method-call.vpr +++ /dev/null @@ -1,19 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -field f: Int - -method client(a: Ref) - requires acc(a.f) -{ - //:: ExpectedCounterexample(call.precondition:assertion.false, (a.f == 5)) - set(a, 5) - a.f := 6 -} - -method set(x: Ref, i: Int) - requires acc(x.f) && x.f != i - ensures acc(x.f) && x.f == i -{ - x.f := i -} diff --git a/src/test/resources/counterexamples/negative.vpr b/src/test/resources/counterexamples/negative.vpr deleted file mode 100644 index 036b8599b..000000000 --- a/src/test/resources/counterexamples/negative.vpr +++ /dev/null @@ -1,10 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -method fun(x:Int) - requires x == 42 -{ - var y: Int := -x - //:: ExpectedCounterexample(assert.failed:assertion.false, (x == 42, y == -42)) - assert(false) -} diff --git a/src/test/resources/counterexamples/permissions.vpr b/src/test/resources/counterexamples/permissions.vpr deleted file mode 100644 index 0a46448af..000000000 --- a/src/test/resources/counterexamples/permissions.vpr +++ /dev/null @@ -1,11 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -field f: Int - -method foo(x: Ref, y: Ref) - requires acc(x.f, 1/2) && acc(y.f, 1/2) -{ - //:: ExpectedCounterexample(assignment.failed:insufficient.permission, (acc(x.f, 1/2))) - x.f := y.f * 2 + 2 -} diff --git a/src/test/resources/counterexamples/predicate.vpr b/src/test/resources/counterexamples/predicate.vpr deleted file mode 100644 index 6d5df8aef..000000000 --- a/src/test/resources/counterexamples/predicate.vpr +++ /dev/null @@ -1,27 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -field x: Int -field y: Int - -predicate StructA(this: Ref) { - acc(this.x) && acc(this.y) -} - -predicate StructB(this: Ref) { - acc(this.x) && acc(this.y) -} - -method foo(a: Ref, b: Ref) - requires StructA(a) - requires StructB(b) - //:: ExpectedCounterexample(postcondition.violated:assertion.false, (a.x == 3)) - ensures acc(a.x) && a.x == 42 -{ - unfold StructA(a) - unfold StructB(b) - a.x := 3 - a.y := 4 - b.x := 5 - b.y := 6 -} diff --git a/src/test/resources/counterexamples/ref-sequence.vpr b/src/test/resources/counterexamples/ref-sequence.vpr deleted file mode 100644 index 858a38372..000000000 --- a/src/test/resources/counterexamples/ref-sequence.vpr +++ /dev/null @@ -1,12 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -field seq: Seq[Int] - -method foo(x: Ref) returns (value: Int) - requires acc(x.seq) && |x.seq| > 1 - //:: ExpectedCounterexample(postcondition.violated:assertion.false, (x.seq[1] == 42)) - ensures value != 42 -{ - value := x.seq[1] -} diff --git a/src/test/resources/counterexamples/sequence.vpr b/src/test/resources/counterexamples/sequence.vpr deleted file mode 100644 index 2f9770447..000000000 --- a/src/test/resources/counterexamples/sequence.vpr +++ /dev/null @@ -1,14 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -method update(values: Seq[Int]) returns (updatedValues: Seq[Int]) - requires |values| > 3 - ensures |values| == |updatedValues| - ensures updatedValues[0] != updatedValues[1] - //:: ExpectedCounterexample(postcondition.violated:assertion.false, (updatedValues[1] == 42, updatedValues[2] == 42)) - ensures updatedValues[1] != updatedValues[2] -{ - updatedValues := values[0 := 0] - updatedValues := updatedValues[1 := 42] - updatedValues := updatedValues[2 := 42] -} diff --git a/src/test/resources/counterexamples/simple-refs-rec.vpr b/src/test/resources/counterexamples/simple-refs-rec.vpr deleted file mode 100644 index 81082fab8..000000000 --- a/src/test/resources/counterexamples/simple-refs-rec.vpr +++ /dev/null @@ -1,27 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -field left: Int -field right: Int -field next: Ref -field valid: Bool - -method simple(x: Ref, y: Ref, z: Ref, r: Int) returns (n: Int) - requires acc(x.left) && acc(x.right) - requires acc(y.left) && acc(y.right) - requires acc(z.next) && acc(z.next.right) - requires acc(x.valid) && x.valid - requires r == 155 - requires y.left == 3 && y.right == 4 - requires x.left == 42 && x.right > 52 - requires z.next.right == 12 - //:: ExpectedCounterexample(postcondition.violated:assertion.false, (n == 42)) - ensures n == 1 -{ - n := x.left - var b: Bool := false - var s: Int := 99 - label ret - x.left := 101 - x.right := 201 -} diff --git a/src/test/resources/counterexamples/simple-refs.vpr b/src/test/resources/counterexamples/simple-refs.vpr deleted file mode 100644 index e098b63f4..000000000 --- a/src/test/resources/counterexamples/simple-refs.vpr +++ /dev/null @@ -1,21 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -field left: Int -field right: Int - -method simple(x: Ref, y: Ref) returns (n:Int) - requires acc(x.left) && acc(x.right) - requires acc(y.left) && acc(y.right) - requires y.left == 3 && y.right == 4 - requires x.left == 42 && x.right > 52 - ensures acc(x.left) && acc(x.right) - ensures acc(y.left) && acc(y.right) - //:: ExpectedCounterexample(postcondition.violated:assertion.false, (x.left == 84)) - ensures x.left == 42 -{ - n := x.left - label ret - x.left := x.left * 2 - x.right := 201 -} diff --git a/src/test/scala/GeneralCounterexampleTests.scala b/src/test/scala/GeneralCounterexampleTests.scala new file mode 100644 index 000000000..1404771a0 --- /dev/null +++ b/src/test/scala/GeneralCounterexampleTests.scala @@ -0,0 +1,210 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2025 ETH Zurich. + +package viper.silicon.tests + +import viper.silicon.Silicon +import viper.silver.testing.{AbstractOutput, CustomAnnotation, DefaultAnnotatedTestInput, DefaultTestInput, OutputAnnotationId, SilOutput, TestAnnotation, TestAnnotationParser, TestCustomError, TestError, TestInput} +import fastparse._ +import viper.silicon.reporting.{ExtendedCounterexample, LitIntEntry, LitPermEntry, NullRefEntry, RecursiveRefEntry, RefEntry, SeqEntry} +import viper.silver.ast +import viper.silver.parser.FastParserCompanion.whitespace +import viper.silver.parser.{FastParser, PAccPred, PBinExp, PExp, PFieldAccess, PIdnUse, PIdnUseExp, PIntLit, PLookup, PSymOp, PUnExp} +import viper.silver.verifier.{ApplicationEntry, CESequence, CEValue, CEValueOnly, CEVariable, ConstantEntry, FailureContext, FieldFinalEntry, Rational, VerificationError} + +import java.nio.file.Path + +class GeneralCounterexampleTests extends SiliconTests { + override val testDirectories: Seq[String] = Seq("counterexamples") + + override def configureVerifiersFromConfigMap(configMap: Map[String, Any]): Unit = { + val args = Silicon.optionsFromScalaTestConfigMap(prefixSpecificConfigMap(configMap).getOrElse("silicon", Map())) + val additionalArgs = Seq("--counterexample", "extended") + + silicon.parseCommandLine(args ++ additionalArgs :+ Silicon.dummyInputFilename) + } + + override def buildTestInput(file: Path, prefix: String): DefaultAnnotatedTestInput = + CounterexampleTestInput(file, prefix) + + /** we override the default annotation parser because we use special annotations to express expected counterexamples */ + object CounterexampleTestInput extends TestAnnotationParser { + /** + * Creates an annotated test input by parsing all annotations in the files + * that belong to the given test input. + */ + def apply(i: TestInput): DefaultAnnotatedTestInput = + DefaultAnnotatedTestInput(i.name, i.prefix, i.files, i.tags, + parseAnnotations(i.files)) + + def apply(file: Path, prefix: String): DefaultAnnotatedTestInput = + apply(DefaultTestInput(file, prefix)) + + override def getAnnotationFinders: Seq[(String, Path, Int) => Option[TestAnnotation]] = { + super.getAnnotationFinders :+ isExpectedCounterexample + } + + // the use of comma is excluded from value ID (i.e. after the colon) to avoid ambiguities with the model + // note that the second capturing group could be turned into a non-capturing group but this would break compatibility + // with the parent trait + override val outputIdPattern: String = "([^:]*)(:([^,]*))?" + + private def isExpectedCounterexample(annotation: String, file: Path, lineNr: Int): Option[TestAnnotation] = { + def parseExpectedCounterexample(id: OutputAnnotationId, expectedCounterexampleString: String): Option[ExpectedCounterexampleAnnotation] = { + // in order to reuse as much of the existing Viper parser as possible, we have to initialize the `_file` and `_line_offset` fields: + val fp = new FastParser() + fp._file = file.toAbsolutePath + val lines = expectedCounterexampleString.linesWithSeparators + fp._line_offset = (lines.map(_.length) ++ Seq(0)).toArray + var offset = 0 + for (i <- fp._line_offset.indices) { + val line_length = fp._line_offset(i) + fp._line_offset(i) = offset + offset += line_length + } + val cParser = new CounterexampleParser(fp) + // now parsing is actually possible: + fastparse.parse(expectedCounterexampleString, cParser.expectedCounterexample(_)) match { + case Parsed.Success(expectedCounterexample, _) => Some(ExpectedCounterexampleAnnotation(id, file, lineNr, expectedCounterexample)) + case Parsed.Failure(_, _, extra) => + println(s"Parsing expected counterexample failed in file $file: ${extra.trace().longAggregateMsg}") + None + } + } + + val regex = ("""^ExpectedCounterexample\(""" + outputIdPattern + """, (.*)\)$""").r + annotation match { + case regex(keyId, _, null, counterexample) => + parseExpectedCounterexample(OutputAnnotationId(keyId, None), counterexample) + case regex(keyId, _, valueId, counterexample) => + parseExpectedCounterexample(OutputAnnotationId(keyId, Some(valueId)), counterexample) + case _ => None + } + } + } +} + +/** represents an expected output (identified by `id`) with an associated (possibly partial) counterexample model */ +case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path, forLineNr: Int, expectedCounterexample: ExpectedCounterexample) extends CustomAnnotation { + override def matches(actual: AbstractOutput): Boolean = + id.matches(actual.fullId) && actual.isSameLine(file, forLineNr) && containsModel(actual) + + /** returns true if the expected model (i.e. class parameter) is a subset of a model given in a failure context */ + def containsModel(is: AbstractOutput): Boolean = is match { + case SilOutput(err) => err match { + case vErr: VerificationError => vErr.failureContexts.toVector.exists(containsExpectedCounterexample) + case _ => false + } + case _ => false + } + + def containsExpectedCounterexample(failureContext: FailureContext): Boolean = + failureContext.counterExample match { + case Some(ce: ExtendedCounterexample) => meetsExpectations(expectedCounterexample, ce) + case _ => false + } + + /** returns true if model2 contains at least the content expressed by model1 */ + def meetsExpectations(model1: ExpectedCounterexample, model2: ExtendedCounterexample): Boolean = { + model1.exprs.forall { + case accPred: PAccPred => containsAccessPredicate(accPred, model2) + case PBinExp(lhs, r, rhs) if r.rs == PSymOp.EqEq => containsEquality(lhs, rhs, model2) + } + } + + def containsAccessPredicate(accPred: PAccPred, model: ExtendedCounterexample): Boolean = { + resolve(Vector(accPred.loc, accPred.perm), model).exists { + case Vector((_, actualPermOpt), (expectedPermAmount, _)) => + actualPermOpt.exists(actualPermAmount => + areEqualEntries(expectedPermAmount, + CEValueOnly(ApplicationEntry("/", Seq(ConstantEntry(actualPermAmount.numerator.toString()), ConstantEntry(actualPermAmount.denominator.toString()))), Some(ast.Perm))) + ) + } + } + + def containsEquality(lhs: PExp, rhs: PExp, model: ExtendedCounterexample): Boolean = + resolveWoPerm(Vector(lhs, rhs), model).exists { case Vector(resolvedLhs, resolvedRhs) => + areEqualEntries(resolvedLhs, resolvedRhs) } + + /** resolves `expr` to a model entry in the given model. In case it's a field access, the corresponding permissions are returned as well */ + def resolve(expr: PExp, model: ExtendedCounterexample): Option[(CEValue, Option[Rational])] = expr match { + case PIntLit(value) => Some(CEValueOnly(ConstantEntry(value.toString()), Some(viper.silver.ast.Int)), None) + case PUnExp(r, PIntLit(value)) if r.rs == PSymOp.Neg => Some(CEValueOnly(ApplicationEntry("-", Seq(ConstantEntry(value.toString()))), Some(ast.Int)), None) + case PBinExp(PIntLit(n), r, PIntLit(d)) if r.rs == PSymOp.Div => + Some(CEValueOnly(ApplicationEntry("/", Seq(ConstantEntry(n.toString()), ConstantEntry(d.toString()))), Some(ast.Perm)), None) + case idnuse: PIdnUseExp => + model.ceStore.asMap.get(idnuse.name).map((_, None)) + case PFieldAccess(rcv, _, idnuse) => + val rcvValue = resolveWoPerm(rcv, model) + rcvValue.flatMap { + case CEVariable(name, entry, _) => model.heaps.get("current").flatMap(_.heapEntries.find({ + case (f: ast.Field, ffi: FieldFinalEntry) if f.name == idnuse.name && (ffi.ref == name || ffi.ref == entry.toString) => true + case _ => false + }).map(he => + (he._2.asInstanceOf[FieldFinalEntry].entry, he._2.asInstanceOf[FieldFinalEntry].perm) + )) + } + case PLookup(base, _, idx, _) => resolveWoPerm(Vector(base, idx), model).flatMap { + case Vector(s: CESequence, CEValueOnly(ConstantEntry(i), _)) => + try { + val evaluatedIdx = BigInt(i) + val elemTyp = s.valueType match { + case Some(ast.SeqType(memberType)) => Some(memberType) + case _ => None + } + if (evaluatedIdx >= 0 && evaluatedIdx < s.length) + Some((CEValueOnly(ConstantEntry(s.entries(evaluatedIdx)), elemTyp), None)) + else + None + } catch { + case _: NumberFormatException => None + } + + } + } + + def resolve(exprs: Vector[PExp], model: ExtendedCounterexample): Option[Vector[(CEValue, Option[Rational])]] = { + val entries = exprs.map(expr => resolve(expr, model)).collect{ case Some(entry) => entry } + if (exprs.size == entries.size) Some(entries) else None + } + + def resolveWoPerm(expr: PExp, model: ExtendedCounterexample): Option[CEValue] = + resolve(expr, model).map(_._1) + + def resolveWoPerm(exprs: Vector[PExp], model: ExtendedCounterexample): Option[Vector[CEValue]] = { + val entries = exprs.map(expr => resolveWoPerm(expr, model)).collect{ case Some(entry) => entry } + if (exprs.size == entries.size) Some(entries) else None + } + + def areEqualEntries(entry1: CEValue, entry2: CEValue): Boolean = (entry1, entry2) match { + case (CEValueOnly(value1, _), CEValueOnly(value2, _)) => value1 == value2 + } + + override def notFoundError: TestError = TestCustomError(s"Expected the following counterexample on line $forLineNr: $expectedCounterexample") + + override def withForLineNr(line: Int = forLineNr): ExpectedCounterexampleAnnotation = ExpectedCounterexampleAnnotation(id, file, line, expectedCounterexample) +} + +/** + * Simple input language to describe an expected counterexample with corresponding parser. + * Currently, a counterexample is expressed by a comma separated list of access predicates and equalities (using the + * same syntax as in Viper) + */ +class CounterexampleParser(fp: FastParser) { + import fp.{accessPred, eqExp} + + def expectedCounterexample[_: P]: P[ExpectedCounterexample] = + (Start ~ "(" ~ (accessPred | eqExp).rep(0, ",") ~ ")" ~ End) + .map(ExpectedCounterexample) +} + +case class ExpectedCounterexample(exprs: Seq[PExp]) { + assert(exprs.forall { + case _: PAccPred => true + case PBinExp(_, r, _) if r.rs == PSymOp.EqEq => true + case _ => false + }) +} From ea483084da58e995443256915cc5f7947d1583d3 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Fri, 29 Aug 2025 18:09:08 +0200 Subject: [PATCH 6/9] Implementing new common interface --- silver | 2 +- ...la => SiliconExtendedCounterexample.scala} | 86 +++++++++++-------- .../scala/rules/SymbolicExecutionRules.scala | 6 +- .../scala/GeneralCounterexampleTests.scala | 20 ++--- 4 files changed, 62 insertions(+), 52 deletions(-) rename src/main/scala/reporting/{ExtendedCounterexample.scala => SiliconExtendedCounterexample.scala} (92%) diff --git a/silver b/silver index d15460f9b..f6c716355 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit d15460f9bc3e8b94a9d86cb266e736cc7dcb72e1 +Subproject commit f6c716355b8fea8dfd1053a8641b23e68404da6b diff --git a/src/main/scala/reporting/ExtendedCounterexample.scala b/src/main/scala/reporting/SiliconExtendedCounterexample.scala similarity index 92% rename from src/main/scala/reporting/ExtendedCounterexample.scala rename to src/main/scala/reporting/SiliconExtendedCounterexample.scala index 5f76fdf6a..f797f2718 100644 --- a/src/main/scala/reporting/ExtendedCounterexample.scala +++ b/src/main/scala/reporting/SiliconExtendedCounterexample.scala @@ -26,14 +26,20 @@ import viper.silver.verifier.Rational /** * CounterexampleGenerator class used for generating an "extended" CE. */ -case class ExtendedCounterexample(model: Model, internalStore: Store, heap: Iterable[Chunk], oldHeaps: State.OldHeaps, program: ast.Program) extends SiliconCounterexample { - val imCE = IntermediateCounterexampleModel(model, internalStore, heap, oldHeaps, program) +case class SiliconExtendedCounterexample(model: Model, + internalStore: Store, + heap: Iterable[Chunk], + oldHeaps: State.OldHeaps, + program: ast.Program) extends SiliconCounterexample with ExtendedCounterexample { + val imCE = SiliconIntermediateCounterexample(model, internalStore, heap, oldHeaps, program) - val (ceStore, refOcc) = ExtendedCounterexample.detStore(internalStore, imCE.basicVariables, imCE.allCollections) - val nameTranslationMap = ExtendedCounterexample.detTranslationMap(ceStore, refOcc) - val ceHeaps = imCE.allBasicHeaps.reverse.map(bh => (bh._1, ExtendedCounterexample.detHeap(bh._2, program, imCE.allCollections, nameTranslationMap, model))) - lazy val heaps = ceHeaps.toMap - val domainsAndFunctions = ExtendedCounterexample.detTranslatedDomains(imCE.DomainEntries, nameTranslationMap) ++ ExtendedCounterexample.detTranslatedFunctions(imCE.nonDomainFunctions, nameTranslationMap) + val (ceStore, refOcc) = SiliconExtendedCounterexample.detStore(internalStore, imCE.basicVariables, imCE.allCollections) + val nameTranslationMap = SiliconExtendedCounterexample.detTranslationMap(ceStore, refOcc) + val ceHeaps = imCE.allBasicHeaps.reverse.map(bh => (bh._1, SiliconExtendedCounterexample.detHeap(bh._2, program, imCE.allCollections, nameTranslationMap, model))) + + val domainEntries = SiliconExtendedCounterexample.detTranslatedDomains(imCE.domainEntries, nameTranslationMap) + val functionEntries = SiliconExtendedCounterexample.detTranslatedFunctions(imCE.nonDomainFunctions, nameTranslationMap) + val domainsAndFunctions = domainEntries ++ functionEntries override def toString: String = { var finalString = " Extended Counterexample: \n" finalString += " Store: \n" @@ -49,24 +55,28 @@ case class ExtendedCounterexample(model: Model, internalStore: Store, heap: Iter } override def withStore(s: Store): SiliconCounterexample = { - ExtendedCounterexample(model, s, heap, oldHeaps, program) + SiliconExtendedCounterexample(model, s, heap, oldHeaps, program) } } /** - * CounterexampleGenerator class used for generating an "interemediate" CE. + * CounterexampleGenerator class used for generating an "intermediate" CE. */ -case class IntermediateCounterexampleModel(model: Model, internalStore: Store, heap: Iterable[Chunk], oldHeaps: State.OldHeaps, program: ast.Program) extends SiliconCounterexample { - val basicVariables = IntermediateCounterexampleModel.detBasicVariables(model, internalStore) - val allSequences = IntermediateCounterexampleModel.detSequences(model) - val allSets = IntermediateCounterexampleModel.detSets(model) - val allMultisets = IntermediateCounterexampleModel.detMultisets(model) - val allCollections = allSequences ++ allSets ++ allMultisets - var allBasicHeaps = Seq(("current", BasicHeap(IntermediateCounterexampleModel.detHeap(model, heap, program.predicatesByName)))) - oldHeaps.foreach {case (n, h) => allBasicHeaps +:= ((n, BasicHeap(IntermediateCounterexampleModel.detHeap(model, h.values, program.predicatesByName))))} +case class SiliconIntermediateCounterexample(model: Model, + internalStore: Store, + heap: Iterable[Chunk], + oldHeaps: State.OldHeaps, + program: ast.Program) extends SiliconCounterexample with IntermediateCounterexample { + val basicVariables: Seq[CEVariable] = SiliconIntermediateCounterexample.detBasicVariables(model, internalStore) + val allSequences: Seq[CEValue] = SiliconIntermediateCounterexample.detSequences(model) + val allSets: Seq[CEValue] = SiliconIntermediateCounterexample.detSets(model) + val allMultisets: Seq[CEValue] = SiliconIntermediateCounterexample.detMultisets(model) + var allBasicHeaps: Seq[(String, BasicHeap)] = Seq(("current", BasicHeap(SiliconIntermediateCounterexample.detHeap(model, heap, program.predicatesByName)))) + oldHeaps.foreach {case (n, h) => allBasicHeaps +:= ((n, BasicHeap(SiliconIntermediateCounterexample.detHeap(model, h.values, program.predicatesByName))))} - val DomainEntries = IntermediateCounterexampleModel.getAllDomains(model, program) - val nonDomainFunctions = IntermediateCounterexampleModel.getAllFunctions(model, program) + def basicHeaps: Seq[(String, BasicHeap)] = allBasicHeaps + val domainEntries: Seq[BasicDomainEntry] = SiliconIntermediateCounterexample.getAllDomains(model, program) + val nonDomainFunctions: Seq[BasicFunctionEntry] = SiliconIntermediateCounterexample.getAllFunctions(model, program) override def toString: String = { var finalString = " Intermediate Counterexample: \n" @@ -77,21 +87,21 @@ case class IntermediateCounterexampleModel(model: Model, internalStore: Store, h finalString += allCollections.map(x => x.toString).mkString("", "\n", "\n") if (!allBasicHeaps.filter(y => !y._2.basicHeapEntries.isEmpty).isEmpty) finalString += allBasicHeaps.filter(y => !y._2.basicHeapEntries.isEmpty).map(x => " " + x._1 + " Heap: \n" + x._2.toString).mkString("", "\n", "\n") - if (!DomainEntries.isEmpty || !nonDomainFunctions.isEmpty) + if (!domainEntries.isEmpty || !nonDomainFunctions.isEmpty) finalString ++= " Domains:\n" - if (!DomainEntries.isEmpty) - finalString += DomainEntries.map(x => x.toString).mkString("", "\n", "\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 } override def withStore(s: Store): SiliconCounterexample = { - ExtendedCounterexample(model, s, heap, oldHeaps, program).imCE + SiliconExtendedCounterexample(model, s, heap, oldHeaps, program).imCE } } -object IntermediateCounterexampleModel { +object SiliconIntermediateCounterexample { /** * Determines the local variables and their value. @@ -1013,7 +1023,7 @@ object IntermediateCounterexampleModel { /** * Extract all the functions occuring inside of a domain. */ - def getAllFunctions(model: Model, program: ast.Program): Seq[BasicFunction] = { + def getAllFunctions(model: Model, program: ast.Program): Seq[BasicFunctionEntry] = { val funcs = program.collect { case f: ast.Function => f } @@ -1023,7 +1033,7 @@ object IntermediateCounterexampleModel { /** * 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], program: ast.Program, hd: Boolean): BasicFunction = { + def detFunction(model: Model, func: ast.FuncLike, genmap: scala.collection.immutable.Map[ast.TypeVar, ast.Type], program: ast.Program, hd: Boolean): BasicFunctionEntry = { def toSort(typ: ast.Type): Either[Throwable, Sort] = Try(symbolConverter.toSort(typ)).toEither def toSortWithSubstitutions(typ: ast.Type, typeErrorMsg: String): Either[String, Sort] = { toSort(typ) @@ -1042,11 +1052,11 @@ object IntermediateCounterexampleModel { .map(x => toSortWithSubstitutions(x.typ, s"typeError in arg type ${x.typ}")) .partitionMap(identity) if (argSortErrors.nonEmpty) { - return BasicFunction("ERROR", argTyp, resTyp, Map.empty, s"$fname ${argSortErrors.head}") + return BasicFunctionEntry("ERROR", argTyp, resTyp, Map.empty, s"$fname ${argSortErrors.head}") } val resSort = toSortWithSubstitutions(resTyp, s"typeError in return type $resTyp") .fold(err => { - return BasicFunction("ERROR", argTyp, resTyp, Map.empty, s"$fname $err") + return BasicFunctionEntry("ERROR", argTyp, resTyp, Map.empty, s"$fname $err") }, identity) val smtfunc = func match { case t: ast.Function => symbolConverter.toFunction(t).id @@ -1060,7 +1070,7 @@ object IntermediateCounterexampleModel { val modelfname = try { (keys.filter(_.contains(fname + "%limited")) ++ keys.filter(_ == fname) ++ keys.filter(_ == kek)).head } catch { - case _: Throwable => return BasicFunction("ERROR", argTyp, resTyp, Map.empty, s"$fname model function not found") + case _: Throwable => return BasicFunctionEntry("ERROR", argTyp, resTyp, Map.empty, s"$fname model function not found") } var heapStateList = Map[ValueEntry, String]() var heapStateCounter = 0 @@ -1092,16 +1102,16 @@ object IntermediateCounterexampleModel { options += (temp -> 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") + BasicFunctionEntry(fname, argTyp, resTyp, options, els.toString) + case Some(ConstantEntry(t)) => BasicFunctionEntry(fname, argTyp, resTyp, Map.empty, t) + case Some(ApplicationEntry(n, args)) => BasicFunctionEntry(fname, argTyp, resTyp, Map.empty, ApplicationEntry(n, args).toString) + case Some(x) => BasicFunctionEntry(fname, argTyp, resTyp, Map.empty, x.toString) + case None => BasicFunctionEntry(fname, argTyp, resTyp, Map.empty, "#undefined") } } } -object ExtendedCounterexample { +object SiliconExtendedCounterexample { /** * Combine a local variable with its ast node. */ @@ -1239,15 +1249,15 @@ object ExtendedCounterexample { domEntries.map(de => BasicDomainEntry(de.name, de.types, detTranslatedFunctions(de.functions, namesMap))) } - def detTranslatedFunctions(funEntries: Seq[BasicFunction], namesMap: Map[String, String]): Seq[BasicFunction] = { + def detTranslatedFunctions(funEntries: Seq[BasicFunctionEntry], namesMap: Map[String, String]): Seq[BasicFunctionEntry] = { funEntries.map(bf => detNameTranslationOfFunction(bf, namesMap)) } - def detNameTranslationOfFunction(fun: BasicFunction, namesMap: Map[String, String]): BasicFunction = { + def detNameTranslationOfFunction(fun: BasicFunctionEntry, namesMap: Map[String, String]): BasicFunctionEntry = { val translatedFun = fun.options.map { case (in, out) => (in.map(intName => namesMap.getOrElse(intName, intName)), namesMap.getOrElse(out, out)) } val translatedEls = namesMap.getOrElse(fun.default, fun.default) - BasicFunction(fun.fname, fun.argtypes, fun.returnType, translatedFun, translatedEls) + BasicFunctionEntry(fun.fname, fun.argtypes, fun.returnType, translatedFun, translatedEls) } } \ No newline at end of file diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala index e08925a5f..021108649 100644 --- a/src/main/scala/rules/SymbolicExecutionRules.scala +++ b/src/main/scala/rules/SymbolicExecutionRules.scala @@ -8,7 +8,7 @@ package viper.silicon.rules import viper.silicon.debugger.DebugExp import viper.silicon.interfaces.{Failure, SiliconDebuggingFailureContext, SiliconFailureContext, SiliconMappedCounterexample, SiliconNativeCounterexample, SiliconVariableCounterexample} -import viper.silicon.reporting.ExtendedCounterexample +import viper.silicon.reporting.SiliconExtendedCounterexample import viper.silicon.state.State import viper.silicon.state.terms.{False, Term} import viper.silicon.verifier.Verifier @@ -70,8 +70,8 @@ trait SymbolicExecutionRules { SiliconVariableCounterexample(s.g, nativeModel) case MappedModel => SiliconMappedCounterexample(s.g, s.h.values, s.oldHeaps, nativeModel, s.program) - case IntermediateModel => ExtendedCounterexample(nativeModel, s.g, s.h.values, s.oldHeaps, s.program).imCE - case ExtendedModel => ExtendedCounterexample(nativeModel, s.g, s.h.values, s.oldHeaps, s.program) + case IntermediateModel => SiliconExtendedCounterexample(nativeModel, s.g, s.h.values, s.oldHeaps, s.program).imCE + case ExtendedModel => SiliconExtendedCounterexample(nativeModel, s.g, s.h.values, s.oldHeaps, s.program) } val finalCE = ceTrafo match { case Some(trafo) => trafo.f(ce) diff --git a/src/test/scala/GeneralCounterexampleTests.scala b/src/test/scala/GeneralCounterexampleTests.scala index 1404771a0..1a733d60b 100644 --- a/src/test/scala/GeneralCounterexampleTests.scala +++ b/src/test/scala/GeneralCounterexampleTests.scala @@ -9,7 +9,7 @@ package viper.silicon.tests import viper.silicon.Silicon import viper.silver.testing.{AbstractOutput, CustomAnnotation, DefaultAnnotatedTestInput, DefaultTestInput, OutputAnnotationId, SilOutput, TestAnnotation, TestAnnotationParser, TestCustomError, TestError, TestInput} import fastparse._ -import viper.silicon.reporting.{ExtendedCounterexample, LitIntEntry, LitPermEntry, NullRefEntry, RecursiveRefEntry, RefEntry, SeqEntry} +import viper.silicon.reporting.SiliconExtendedCounterexample import viper.silver.ast import viper.silver.parser.FastParserCompanion.whitespace import viper.silver.parser.{FastParser, PAccPred, PBinExp, PExp, PFieldAccess, PIdnUse, PIdnUseExp, PIntLit, PLookup, PSymOp, PUnExp} @@ -103,19 +103,19 @@ case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path, def containsExpectedCounterexample(failureContext: FailureContext): Boolean = failureContext.counterExample match { - case Some(ce: ExtendedCounterexample) => meetsExpectations(expectedCounterexample, ce) + case Some(ce: SiliconExtendedCounterexample) => meetsExpectations(expectedCounterexample, ce) case _ => false } /** returns true if model2 contains at least the content expressed by model1 */ - def meetsExpectations(model1: ExpectedCounterexample, model2: ExtendedCounterexample): Boolean = { + def meetsExpectations(model1: ExpectedCounterexample, model2: SiliconExtendedCounterexample): Boolean = { model1.exprs.forall { case accPred: PAccPred => containsAccessPredicate(accPred, model2) case PBinExp(lhs, r, rhs) if r.rs == PSymOp.EqEq => containsEquality(lhs, rhs, model2) } } - def containsAccessPredicate(accPred: PAccPred, model: ExtendedCounterexample): Boolean = { + def containsAccessPredicate(accPred: PAccPred, model: SiliconExtendedCounterexample): Boolean = { resolve(Vector(accPred.loc, accPred.perm), model).exists { case Vector((_, actualPermOpt), (expectedPermAmount, _)) => actualPermOpt.exists(actualPermAmount => @@ -125,12 +125,12 @@ case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path, } } - def containsEquality(lhs: PExp, rhs: PExp, model: ExtendedCounterexample): Boolean = + def containsEquality(lhs: PExp, rhs: PExp, model: SiliconExtendedCounterexample): Boolean = resolveWoPerm(Vector(lhs, rhs), model).exists { case Vector(resolvedLhs, resolvedRhs) => areEqualEntries(resolvedLhs, resolvedRhs) } /** resolves `expr` to a model entry in the given model. In case it's a field access, the corresponding permissions are returned as well */ - def resolve(expr: PExp, model: ExtendedCounterexample): Option[(CEValue, Option[Rational])] = expr match { + def resolve(expr: PExp, model: SiliconExtendedCounterexample): Option[(CEValue, Option[Rational])] = expr match { case PIntLit(value) => Some(CEValueOnly(ConstantEntry(value.toString()), Some(viper.silver.ast.Int)), None) case PUnExp(r, PIntLit(value)) if r.rs == PSymOp.Neg => Some(CEValueOnly(ApplicationEntry("-", Seq(ConstantEntry(value.toString()))), Some(ast.Int)), None) case PBinExp(PIntLit(n), r, PIntLit(d)) if r.rs == PSymOp.Div => @@ -140,7 +140,7 @@ case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path, case PFieldAccess(rcv, _, idnuse) => val rcvValue = resolveWoPerm(rcv, model) rcvValue.flatMap { - case CEVariable(name, entry, _) => model.heaps.get("current").flatMap(_.heapEntries.find({ + case CEVariable(name, entry, _) => model.heapMap.get("current").flatMap(_.heapEntries.find({ case (f: ast.Field, ffi: FieldFinalEntry) if f.name == idnuse.name && (ffi.ref == name || ffi.ref == entry.toString) => true case _ => false }).map(he => @@ -166,15 +166,15 @@ case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path, } } - def resolve(exprs: Vector[PExp], model: ExtendedCounterexample): Option[Vector[(CEValue, Option[Rational])]] = { + def resolve(exprs: Vector[PExp], model: SiliconExtendedCounterexample): Option[Vector[(CEValue, Option[Rational])]] = { val entries = exprs.map(expr => resolve(expr, model)).collect{ case Some(entry) => entry } if (exprs.size == entries.size) Some(entries) else None } - def resolveWoPerm(expr: PExp, model: ExtendedCounterexample): Option[CEValue] = + def resolveWoPerm(expr: PExp, model: SiliconExtendedCounterexample): Option[CEValue] = resolve(expr, model).map(_._1) - def resolveWoPerm(exprs: Vector[PExp], model: ExtendedCounterexample): Option[Vector[CEValue]] = { + def resolveWoPerm(exprs: Vector[PExp], model: SiliconExtendedCounterexample): Option[Vector[CEValue]] = { val entries = exprs.map(expr => resolveWoPerm(expr, model)).collect{ case Some(entry) => entry } if (exprs.size == entries.size) Some(entries) else None } From d0e4cec8c1f364d5cb1e544463da917825a55fdf Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Mon, 1 Sep 2025 14:45:36 +0200 Subject: [PATCH 7/9] Adapting to silver changes --- silver | 2 +- .../SiliconExtendedCounterexample.scala | 24 +-- .../scala/GeneralCounterexampleTests.scala | 186 +----------------- 3 files changed, 14 insertions(+), 198 deletions(-) diff --git a/silver b/silver index f6c716355..062f25c42 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit f6c716355b8fea8dfd1053a8641b23e68404da6b +Subproject commit 062f25c4285e0dd700d6e61e43573026f339fd96 diff --git a/src/main/scala/reporting/SiliconExtendedCounterexample.scala b/src/main/scala/reporting/SiliconExtendedCounterexample.scala index f797f2718..eb2e8cb45 100644 --- a/src/main/scala/reporting/SiliconExtendedCounterexample.scala +++ b/src/main/scala/reporting/SiliconExtendedCounterexample.scala @@ -39,7 +39,7 @@ case class SiliconExtendedCounterexample(model: Model, val domainEntries = SiliconExtendedCounterexample.detTranslatedDomains(imCE.domainEntries, nameTranslationMap) val functionEntries = SiliconExtendedCounterexample.detTranslatedFunctions(imCE.nonDomainFunctions, nameTranslationMap) - val domainsAndFunctions = domainEntries ++ functionEntries + override def toString: String = { var finalString = " Extended Counterexample: \n" finalString += " Store: \n" @@ -147,7 +147,7 @@ object SiliconIntermediateCounterexample { * and are not assigned to their actual value. Additionally, not every sequence in the output set will be mentioned * in the "extended" CE as only sequences that are used in the method containing the verification error will be mentioned there. */ - def detSequences(model: Model): Set[CEValue] = { + def detSequences(model: Model): Seq[CEValue] = { var res = Map[String, Seq[String]]() var tempMap = Map[(String, Seq[String]), String]() for ((opName, opValues) <- model.entries) { @@ -246,7 +246,7 @@ object SiliconIntermediateCounterexample { } } } - var ans = Set[CEValue]() + var ans = Seq[CEValue]() res.foreach { case (n, s) => val typ: Option[Type] = detASTTypeFromString(n.replaceAll(".*?<(.*)>.*", "$1")) match { @@ -261,7 +261,7 @@ object SiliconIntermediateCounterexample { } counter += 1 } - ans += CESequence(n, BigInt(s.length), entries, s, typ) + ans +:= CESequence(n, BigInt(s.length), entries, s, typ) } ans } @@ -271,7 +271,7 @@ object SiliconIntermediateCounterexample { * and are not assigned to their actual value. Additionally, not every set in the output set will be mentioned * in the "extended" CE as only sets that are used in the method containing the verification error will be mentioned there. */ - def detSets(model: Model): Set[CEValue] = { + def detSets(model: Model): Seq[CEValue] = { var res = Map[String, Set[String]]() for ((opName, opValues) <- model.entries) { if (opName == "Set_empty") { @@ -361,7 +361,7 @@ object SiliconIntermediateCounterexample { } } } - var ans = Set[CEValue]() + var ans = Seq[CEValue]() res.foreach { case (n, s) => val typ: Option[Type] = detASTTypeFromString(n.replaceAll(".*?<(.*)>.*", "$1")) match { @@ -374,7 +374,7 @@ object SiliconIntermediateCounterexample { containment += ((e, true)) } } - ans += CESet(n, BigInt(s.size), containment, s, typ) + ans +:= CESet(n, BigInt(s.size), containment, s, typ) } ans } @@ -384,7 +384,7 @@ object SiliconIntermediateCounterexample { * and are not assigned to their actual value. Additionally, not every multiset in the output set will be mentioned * in the "extended" CE as only multisets that are used in the method containing the verification error will be mentioned there. */ - def detMultisets(model: Model): Set[CEValue] = { + def detMultisets(model: Model): Seq[CEValue] = { var res = Map[String, scala.collection.immutable.Map[String, Int]]() for ((opName, opValues) <- model.entries) { if (opName == "Multiset_empty") { @@ -477,7 +477,7 @@ object SiliconIntermediateCounterexample { } } } - var ans = Set[CEValue]() + var ans = Seq[CEValue]() res.foreach { case (n, s) => val typ: Option[Type] = detASTTypeFromString(n.replaceAll(".*?<(.*)>.*", "$1")) match { @@ -485,7 +485,7 @@ object SiliconIntermediateCounterexample { case None => None } val size = s.values.sum - ans += CEMultiset(n, BigInt(size), s, typ) + ans +:= CEMultiset(n, BigInt(size), s, typ) } ans } @@ -1115,7 +1115,7 @@ object SiliconExtendedCounterexample { /** * Combine a local variable with its ast node. */ - def detStore(store: Store, variables: Seq[CEVariable], collections: Set[CEValue]): (StoreCounterexample, Map[String, (String, Int)]) = { + def detStore(store: Store, variables: Seq[CEVariable], collections: Seq[CEValue]): (StoreCounterexample, Map[String, (String, Int)]) = { var refOccurences = Map[String, (String, Int)]() var ans = Seq[StoreEntry]() for ((k, _) <- store.values) { @@ -1184,7 +1184,7 @@ object SiliconExtendedCounterexample { /** * Match heap resources to their ast node and translate all identifiers (for fields and references) */ - def detHeap(basicHeap: BasicHeap, program: Program, collections: Set[CEValue], translNames: Map[String, String], model: Model): HeapCounterexample = { + def detHeap(basicHeap: BasicHeap, program: Program, collections: Seq[CEValue], translNames: Map[String, String], model: Model): HeapCounterexample = { var ans = Seq[(Resource, FinalHeapEntry)]() for (bhe <- basicHeap.basicHeapEntries) { bhe.het match { diff --git a/src/test/scala/GeneralCounterexampleTests.scala b/src/test/scala/GeneralCounterexampleTests.scala index 1a733d60b..1f493f08c 100644 --- a/src/test/scala/GeneralCounterexampleTests.scala +++ b/src/test/scala/GeneralCounterexampleTests.scala @@ -7,13 +7,7 @@ package viper.silicon.tests import viper.silicon.Silicon -import viper.silver.testing.{AbstractOutput, CustomAnnotation, DefaultAnnotatedTestInput, DefaultTestInput, OutputAnnotationId, SilOutput, TestAnnotation, TestAnnotationParser, TestCustomError, TestError, TestInput} -import fastparse._ -import viper.silicon.reporting.SiliconExtendedCounterexample -import viper.silver.ast -import viper.silver.parser.FastParserCompanion.whitespace -import viper.silver.parser.{FastParser, PAccPred, PBinExp, PExp, PFieldAccess, PIdnUse, PIdnUseExp, PIntLit, PLookup, PSymOp, PUnExp} -import viper.silver.verifier.{ApplicationEntry, CESequence, CEValue, CEValueOnly, CEVariable, ConstantEntry, FailureContext, FieldFinalEntry, Rational, VerificationError} +import viper.silver.testing.{CounterexampleTestInput, DefaultAnnotatedTestInput} import java.nio.file.Path @@ -29,182 +23,4 @@ class GeneralCounterexampleTests extends SiliconTests { override def buildTestInput(file: Path, prefix: String): DefaultAnnotatedTestInput = CounterexampleTestInput(file, prefix) - - /** we override the default annotation parser because we use special annotations to express expected counterexamples */ - object CounterexampleTestInput extends TestAnnotationParser { - /** - * Creates an annotated test input by parsing all annotations in the files - * that belong to the given test input. - */ - def apply(i: TestInput): DefaultAnnotatedTestInput = - DefaultAnnotatedTestInput(i.name, i.prefix, i.files, i.tags, - parseAnnotations(i.files)) - - def apply(file: Path, prefix: String): DefaultAnnotatedTestInput = - apply(DefaultTestInput(file, prefix)) - - override def getAnnotationFinders: Seq[(String, Path, Int) => Option[TestAnnotation]] = { - super.getAnnotationFinders :+ isExpectedCounterexample - } - - // the use of comma is excluded from value ID (i.e. after the colon) to avoid ambiguities with the model - // note that the second capturing group could be turned into a non-capturing group but this would break compatibility - // with the parent trait - override val outputIdPattern: String = "([^:]*)(:([^,]*))?" - - private def isExpectedCounterexample(annotation: String, file: Path, lineNr: Int): Option[TestAnnotation] = { - def parseExpectedCounterexample(id: OutputAnnotationId, expectedCounterexampleString: String): Option[ExpectedCounterexampleAnnotation] = { - // in order to reuse as much of the existing Viper parser as possible, we have to initialize the `_file` and `_line_offset` fields: - val fp = new FastParser() - fp._file = file.toAbsolutePath - val lines = expectedCounterexampleString.linesWithSeparators - fp._line_offset = (lines.map(_.length) ++ Seq(0)).toArray - var offset = 0 - for (i <- fp._line_offset.indices) { - val line_length = fp._line_offset(i) - fp._line_offset(i) = offset - offset += line_length - } - val cParser = new CounterexampleParser(fp) - // now parsing is actually possible: - fastparse.parse(expectedCounterexampleString, cParser.expectedCounterexample(_)) match { - case Parsed.Success(expectedCounterexample, _) => Some(ExpectedCounterexampleAnnotation(id, file, lineNr, expectedCounterexample)) - case Parsed.Failure(_, _, extra) => - println(s"Parsing expected counterexample failed in file $file: ${extra.trace().longAggregateMsg}") - None - } - } - - val regex = ("""^ExpectedCounterexample\(""" + outputIdPattern + """, (.*)\)$""").r - annotation match { - case regex(keyId, _, null, counterexample) => - parseExpectedCounterexample(OutputAnnotationId(keyId, None), counterexample) - case regex(keyId, _, valueId, counterexample) => - parseExpectedCounterexample(OutputAnnotationId(keyId, Some(valueId)), counterexample) - case _ => None - } - } - } -} - -/** represents an expected output (identified by `id`) with an associated (possibly partial) counterexample model */ -case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path, forLineNr: Int, expectedCounterexample: ExpectedCounterexample) extends CustomAnnotation { - override def matches(actual: AbstractOutput): Boolean = - id.matches(actual.fullId) && actual.isSameLine(file, forLineNr) && containsModel(actual) - - /** returns true if the expected model (i.e. class parameter) is a subset of a model given in a failure context */ - def containsModel(is: AbstractOutput): Boolean = is match { - case SilOutput(err) => err match { - case vErr: VerificationError => vErr.failureContexts.toVector.exists(containsExpectedCounterexample) - case _ => false - } - case _ => false - } - - def containsExpectedCounterexample(failureContext: FailureContext): Boolean = - failureContext.counterExample match { - case Some(ce: SiliconExtendedCounterexample) => meetsExpectations(expectedCounterexample, ce) - case _ => false - } - - /** returns true if model2 contains at least the content expressed by model1 */ - def meetsExpectations(model1: ExpectedCounterexample, model2: SiliconExtendedCounterexample): Boolean = { - model1.exprs.forall { - case accPred: PAccPred => containsAccessPredicate(accPred, model2) - case PBinExp(lhs, r, rhs) if r.rs == PSymOp.EqEq => containsEquality(lhs, rhs, model2) - } - } - - def containsAccessPredicate(accPred: PAccPred, model: SiliconExtendedCounterexample): Boolean = { - resolve(Vector(accPred.loc, accPred.perm), model).exists { - case Vector((_, actualPermOpt), (expectedPermAmount, _)) => - actualPermOpt.exists(actualPermAmount => - areEqualEntries(expectedPermAmount, - CEValueOnly(ApplicationEntry("/", Seq(ConstantEntry(actualPermAmount.numerator.toString()), ConstantEntry(actualPermAmount.denominator.toString()))), Some(ast.Perm))) - ) - } - } - - def containsEquality(lhs: PExp, rhs: PExp, model: SiliconExtendedCounterexample): Boolean = - resolveWoPerm(Vector(lhs, rhs), model).exists { case Vector(resolvedLhs, resolvedRhs) => - areEqualEntries(resolvedLhs, resolvedRhs) } - - /** resolves `expr` to a model entry in the given model. In case it's a field access, the corresponding permissions are returned as well */ - def resolve(expr: PExp, model: SiliconExtendedCounterexample): Option[(CEValue, Option[Rational])] = expr match { - case PIntLit(value) => Some(CEValueOnly(ConstantEntry(value.toString()), Some(viper.silver.ast.Int)), None) - case PUnExp(r, PIntLit(value)) if r.rs == PSymOp.Neg => Some(CEValueOnly(ApplicationEntry("-", Seq(ConstantEntry(value.toString()))), Some(ast.Int)), None) - case PBinExp(PIntLit(n), r, PIntLit(d)) if r.rs == PSymOp.Div => - Some(CEValueOnly(ApplicationEntry("/", Seq(ConstantEntry(n.toString()), ConstantEntry(d.toString()))), Some(ast.Perm)), None) - case idnuse: PIdnUseExp => - model.ceStore.asMap.get(idnuse.name).map((_, None)) - case PFieldAccess(rcv, _, idnuse) => - val rcvValue = resolveWoPerm(rcv, model) - rcvValue.flatMap { - case CEVariable(name, entry, _) => model.heapMap.get("current").flatMap(_.heapEntries.find({ - case (f: ast.Field, ffi: FieldFinalEntry) if f.name == idnuse.name && (ffi.ref == name || ffi.ref == entry.toString) => true - case _ => false - }).map(he => - (he._2.asInstanceOf[FieldFinalEntry].entry, he._2.asInstanceOf[FieldFinalEntry].perm) - )) - } - case PLookup(base, _, idx, _) => resolveWoPerm(Vector(base, idx), model).flatMap { - case Vector(s: CESequence, CEValueOnly(ConstantEntry(i), _)) => - try { - val evaluatedIdx = BigInt(i) - val elemTyp = s.valueType match { - case Some(ast.SeqType(memberType)) => Some(memberType) - case _ => None - } - if (evaluatedIdx >= 0 && evaluatedIdx < s.length) - Some((CEValueOnly(ConstantEntry(s.entries(evaluatedIdx)), elemTyp), None)) - else - None - } catch { - case _: NumberFormatException => None - } - - } - } - - def resolve(exprs: Vector[PExp], model: SiliconExtendedCounterexample): Option[Vector[(CEValue, Option[Rational])]] = { - val entries = exprs.map(expr => resolve(expr, model)).collect{ case Some(entry) => entry } - if (exprs.size == entries.size) Some(entries) else None - } - - def resolveWoPerm(expr: PExp, model: SiliconExtendedCounterexample): Option[CEValue] = - resolve(expr, model).map(_._1) - - def resolveWoPerm(exprs: Vector[PExp], model: SiliconExtendedCounterexample): Option[Vector[CEValue]] = { - val entries = exprs.map(expr => resolveWoPerm(expr, model)).collect{ case Some(entry) => entry } - if (exprs.size == entries.size) Some(entries) else None - } - - def areEqualEntries(entry1: CEValue, entry2: CEValue): Boolean = (entry1, entry2) match { - case (CEValueOnly(value1, _), CEValueOnly(value2, _)) => value1 == value2 - } - - override def notFoundError: TestError = TestCustomError(s"Expected the following counterexample on line $forLineNr: $expectedCounterexample") - - override def withForLineNr(line: Int = forLineNr): ExpectedCounterexampleAnnotation = ExpectedCounterexampleAnnotation(id, file, line, expectedCounterexample) -} - -/** - * Simple input language to describe an expected counterexample with corresponding parser. - * Currently, a counterexample is expressed by a comma separated list of access predicates and equalities (using the - * same syntax as in Viper) - */ -class CounterexampleParser(fp: FastParser) { - import fp.{accessPred, eqExp} - - def expectedCounterexample[_: P]: P[ExpectedCounterexample] = - (Start ~ "(" ~ (accessPred | eqExp).rep(0, ",") ~ ")" ~ End) - .map(ExpectedCounterexample) -} - -case class ExpectedCounterexample(exprs: Seq[PExp]) { - assert(exprs.forall { - case _: PAccPred => true - case PBinExp(_, r, _) if r.rs == PSymOp.EqEq => true - case _ => false - }) } From 0d044e9357cbe102a99e64ad0f1e58a536104206 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Mon, 1 Sep 2025 19:28:07 +0200 Subject: [PATCH 8/9] Adapting to silver changes --- src/test/scala/GeneralCounterexampleTests.scala | 2 +- src/test/scala/MappedCounterexampleTests.scala | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/test/scala/GeneralCounterexampleTests.scala b/src/test/scala/GeneralCounterexampleTests.scala index 1f493f08c..b9b5c3888 100644 --- a/src/test/scala/GeneralCounterexampleTests.scala +++ b/src/test/scala/GeneralCounterexampleTests.scala @@ -12,7 +12,7 @@ import viper.silver.testing.{CounterexampleTestInput, DefaultAnnotatedTestInput} import java.nio.file.Path class GeneralCounterexampleTests extends SiliconTests { - override val testDirectories: Seq[String] = Seq("counterexamples") + override val testDirectories: Seq[String] = Seq("counterexample_mapped", "counterexample_general") override def configureVerifiersFromConfigMap(configMap: Map[String, Any]): Unit = { val args = Silicon.optionsFromScalaTestConfigMap(prefixSpecificConfigMap(configMap).getOrElse("silicon", Map())) diff --git a/src/test/scala/MappedCounterexampleTests.scala b/src/test/scala/MappedCounterexampleTests.scala index 5e624f383..aad2f650a 100644 --- a/src/test/scala/MappedCounterexampleTests.scala +++ b/src/test/scala/MappedCounterexampleTests.scala @@ -18,7 +18,7 @@ import viper.silver.verifier.{FailureContext, VerificationError} import java.nio.file.Path class MappedCounterexampleTests extends SiliconTests { - override val testDirectories: Seq[String] = Seq("counterexamples") + override val testDirectories: Seq[String] = Seq("counterexample_mapped") override def configureVerifiersFromConfigMap(configMap: Map[String, Any]): Unit = { val args = Silicon.optionsFromScalaTestConfigMap(prefixSpecificConfigMap(configMap).getOrElse("silicon", Map())) From e5a2de5149fe2c93bf462458bb2793f6590ceea8 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Mon, 1 Sep 2025 19:28:12 +0200 Subject: [PATCH 9/9] Adapting to silver changes --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 062f25c42..5e1fda951 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 062f25c4285e0dd700d6e61e43573026f339fd96 +Subproject commit 5e1fda95105708c4a64afc011f9cc7d3f21ac134