From 0a24eac7646f2984ed574190238c0832f6ebb706 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Wed, 4 Dec 2024 21:06:25 +0100 Subject: [PATCH] Adding an option to print the term representation of store, heap, assumptions and branch conditions --- src/main/scala/debugger/DebugExp.scala | 14 ++++---- src/main/scala/debugger/SiliconDebugger.scala | 32 +++++++++++++++---- src/main/scala/interfaces/Verification.scala | 3 +- .../scala/rules/SymbolicExecutionRules.scala | 2 +- 4 files changed, 36 insertions(+), 15 deletions(-) diff --git a/src/main/scala/debugger/DebugExp.scala b/src/main/scala/debugger/DebugExp.scala index 0971b62e4..cbde4fb58 100644 --- a/src/main/scala/debugger/DebugExp.scala +++ b/src/main/scala/debugger/DebugExp.scala @@ -138,9 +138,10 @@ class DebugExp(val id: Int, } } - def getTopLevelString(currDepth: Int): String = { - val delimiter = if (finalExp.isDefined && description.isDefined) ": " else "" - "\n\t" + ("\t"*currDepth) + "[" + id + "] " + description.getOrElse("") + delimiter + finalExp.getOrElse("") + def getTopLevelString(currDepth: Int, config: DebugExpPrintConfiguration): String = { + val toDisplay = if (config.printInternalTermRepresentation) term else finalExp + val delimiter = if (toDisplay.isDefined && description.isDefined) ": " else "" + "\n\t" + ("\t"*currDepth) + "[" + id + "] " + description.getOrElse("") + delimiter + toDisplay.getOrElse("") } @@ -148,7 +149,7 @@ class DebugExp(val id: Int, if (isInternal_ && !config.isPrintInternalEnabled){ return "" } - getTopLevelString(currDepth) + childrenToString(currDepth, math.max(maxDepth, config.nodeToHierarchyLevelMap.getOrElse(id, 0)), config) + getTopLevelString(currDepth, config) + childrenToString(currDepth, math.max(maxDepth, config.nodeToHierarchyLevelMap.getOrElse(id, 0)), config) } def getExpWithId(id: Int, visited: mutable.HashSet[DebugExp]): Option[DebugExp] = { @@ -197,7 +198,7 @@ class ImplicationDebugExp(id: Int, } if (children.nonEmpty) { - getTopLevelString(currDepth) + " ==> " + childrenToString(currDepth, math.max(maxDepth, config.nodeToHierarchyLevelMap.getOrElse(id, 0)), config) + getTopLevelString(currDepth, config) + " ==> " + childrenToString(currDepth, math.max(maxDepth, config.nodeToHierarchyLevelMap.getOrElse(id, 0)), config) } else { "true" } @@ -230,7 +231,7 @@ class QuantifiedDebugExp(id: Int, if (qvars.nonEmpty) { "\n\t" + ("\t"*currDepth) + "[" + id + "] " + (if (quantifier == "QA") "forall" else "exists") + " " + qvars.mkString(", ") + " :: " + childrenToString(currDepth, math.max(maxDepth, config.nodeToHierarchyLevelMap.getOrElse(id, 0)), config) } else { - getTopLevelString(currDepth) + getTopLevelString(currDepth, config) } } } @@ -242,6 +243,7 @@ class DebugExpPrintConfiguration { var printHierarchyLevel: Int = 2 var nodeToHierarchyLevelMap: Map[Int, Int] = Map.empty var isPrintAxiomsEnabled: Boolean = false + var printInternalTermRepresentation: Boolean = false def setPrintHierarchyLevel(level: String): Unit ={ printHierarchyLevel = level match { diff --git a/src/main/scala/debugger/SiliconDebugger.scala b/src/main/scala/debugger/SiliconDebugger.scala index 719acfb10..9151ba603 100644 --- a/src/main/scala/debugger/SiliconDebugger.scala +++ b/src/main/scala/debugger/SiliconDebugger.scala @@ -6,7 +6,7 @@ import viper.silicon.interfaces.state.Chunk import viper.silicon.interfaces.{Failure, SiliconDebuggingFailureContext, Success, VerificationResult} import viper.silicon.resources.{FieldID, PredicateID} import viper.silicon.rules.evaluator -import viper.silicon.state.terms.Term +import viper.silicon.state.terms.{Term, True} import viper.silicon.state.{BasicChunk, IdentifierFactory, MagicWandChunk, QuantifiedFieldChunk, QuantifiedMagicWandChunk, QuantifiedPredicateChunk, State} import viper.silicon.utils.ast.simplifyVariableName import viper.silicon.verifier.{MainVerifier, Verifier, WorkerVerifier} @@ -26,7 +26,8 @@ case class ProofObligation(s: State, v: Verifier, proverEmits: Seq[String], preambleAssumptions: Seq[DebugAxiom], - branchConditions: Seq[(ast.Exp, ast.Exp)], + branchConditions: Seq[Term], + branchConditionExps: Seq[(ast.Exp, ast.Exp)], assumptionsExp: InsertionOrderedSet[DebugExp], assertion: Term, eAssertion: DebugExp, @@ -52,13 +53,23 @@ case class ProofObligation(s: State, }) + s"\n\t\t${originalErrorReason.readableMessage}\n\n" - private lazy val stateString: String = - s"Store:\n\t\t${s.g.values.map(v => s"${v._1} -> ${v._2._2.get}").mkString("\n\t\t")}\n\nHeap:\n\t\t${s.h.values.map(chunkString).mkString("\n\t\t")}\n\n" + private lazy val stateString: String = { + if (printConfig.printInternalTermRepresentation) + s"Store:\n\t\t${s.g.values.map(v => s"${v._1} -> ${v._2._1}").mkString("\n\t\t")}\n\nHeap:\n\t\t${s.h.values.map(chunkString).mkString("\n\t\t")}\n\n" + else + s"Store:\n\t\t${s.g.values.map(v => s"${v._1} -> ${v._2._2.get}").mkString("\n\t\t")}\n\nHeap:\n\t\t${s.h.values.map(chunkString).mkString("\n\t\t")}\n\n" + } - private lazy val branchConditionString: String = - s"Branch Conditions:\n\t\t${branchConditions.map(bc => Simplifier.simplify(bc._2, true)).filter(bc => bc != ast.TrueLit()()).mkString("\n\t\t")}\n\n" + private lazy val branchConditionString: String = { + if (printConfig.printInternalTermRepresentation) + s"Branch Conditions:\n\t\t${branchConditions.filter(bc => bc != True).mkString("\n\t\t")}\n\n" + else + s"Branch Conditions:\n\t\t${branchConditionExps.map(bc => Simplifier.simplify(bc._2, true)).filter(bc => bc != ast.TrueLit()()).mkString("\n\t\t")}\n\n" + } private def chunkString(c: Chunk): String = { + if (printConfig.printInternalTermRepresentation) + return c.toString val res = c match { case bc: BasicChunk => val snapExpString = bc.snapExp match { @@ -219,7 +230,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult], } val obl = Some(ProofObligation(failureContext.state.get, failureContext.verifier.get, failureContext.proverDecls, failureContext.preambleAssumptions, - failureContext.branchConditions, failureContext.assumptions, + failureContext.branchConditions, failureContext.branchConditionExps, failureContext.assumptions, failureContext.failedAssertion, failureContext.failedAssertionExp, None, new DebugExpPrintConfiguration, currResult.message.reason, new DebugResolver(this.pprogram, this.resolver.names), new DebugTranslator(this.pprogram, translator.getMembers()))) @@ -537,6 +548,13 @@ class SiliconDebugger(verificationResults: List[VerificationResult], case _ => } + println(s"Enter the new value for printInternalTermRepresentation:") + readLine().toLowerCase match { + case "true" | "1" | "t" => obl.printConfig.printInternalTermRepresentation = true + case "false" | "0" | "f" => obl.printConfig.printInternalTermRepresentation = false + case _ => + } + //println(s"Enter the new value for nodeToHierarchyLevelMap:") //obl.printConfig.addHierarchyLevelForId(readLine()) } diff --git a/src/main/scala/interfaces/Verification.scala b/src/main/scala/interfaces/Verification.scala index dbe953c25..ad52d3bf2 100644 --- a/src/main/scala/interfaces/Verification.scala +++ b/src/main/scala/interfaces/Verification.scala @@ -135,7 +135,8 @@ case class SiliconFailureContext(branchConditions: Seq[ast.Exp], override lazy val toString: String = branchConditionString + counterExampleString + reasonUnknownString } -case class SiliconDebuggingFailureContext(branchConditions: Seq[(ast.Exp, ast.Exp)], +case class SiliconDebuggingFailureContext(branchConditions: Seq[Term], + branchConditionExps: Seq[(ast.Exp, ast.Exp)], counterExample: Option[Counterexample], reasonUnknown: Option[String], state: Option[State], diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala index 888028133..6f18728d5 100644 --- a/src/main/scala/rules/SymbolicExecutionRules.scala +++ b/src/main/scala/rules/SymbolicExecutionRules.scala @@ -96,7 +96,7 @@ trait SymbolicExecutionRules { if (Verifier.config.enableDebugging()){ val assumptions = v.decider.pcs.assumptionExps - res.failureContexts = Seq(SiliconDebuggingFailureContext(v.decider.pcs.branchConditionExps.map(bce => bce._1 -> bce._2.get), + res.failureContexts = Seq(SiliconDebuggingFailureContext(v.decider.pcs.branchConditions, v.decider.pcs.branchConditionExps.map(bce => bce._1 -> bce._2.get), counterexample, reasonUnknown, Some(s), Some(v), v.decider.prover.getAllEmits(), v.decider.prover.preambleAssumptions, v.decider.macroDecls, v.decider.functionDecls, assumptions, failedAssert, failedAssertExp.get)) } else {