Adding an option to print the term representation of store, heap, ass…

…umptions and branch conditions
viperproject · Dec 4, 2024 · 0a24eac · 0a24eac
1 parent b20c9a5
commit 0a24eac
Show file tree

Hide file tree

Showing 4 changed files with 36 additions and 15 deletions.
diff --git a/src/main/scala/debugger/DebugExp.scala b/src/main/scala/debugger/DebugExp.scala
@@ -138,17 +138,18 @@ 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("")
   }
 
 
   def toString(currDepth: Int, maxDepth: Int, config: DebugExpPrintConfiguration): String = {
     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
@@ -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
@@ -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
@@ -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 {