Merge

src/main/scala/debugger/DebugExp.scala

@@ -8,15 +8,15 @@ package viper.silicon.debugger
 
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.decider.PathConditions
-import viper.silicon.state.terms.{And, Exists, Forall, Implies, Quantification, Term, Trigger, True, Var}
+import viper.silicon.state.terms.{And, Exists, Forall, Implies, Quantification, Term, Trigger, Var}
 import viper.silver.ast
-import viper.silver.ast.TrueLit
 import viper.silver.ast.utility.Simplifier
 
+import java.util.concurrent.atomic.AtomicInteger
 import scala.collection.mutable
 
 object DebugExp {
-  private var idCounter: Int = 0
+  private var idCounter: AtomicInteger = new AtomicInteger(0)
 
   def createInstance(description: Option[String],
                      originalExp: Option[ast.Exp],
@@ -28,8 +28,7 @@ object DebugExp {
 
     val originalExpSimplified = originalExp.map(Simplifier.simplify(_, true))
     val finalExpSimplified = finalExp.map(Simplifier.simplify(_, true))
-    val debugExp = new DebugExp(idCounter, description, originalExpSimplified, finalExpSimplified, term, isInternal_, children)
-    idCounter += 1
+    val debugExp = new DebugExp(idCounter.getAndIncrement(), description, originalExpSimplified, finalExpSimplified, term, isInternal_, children)
     debugExp
   }
 
@@ -69,8 +68,7 @@ object DebugExp {
                                 isInternal_ : Boolean,
                                 children: InsertionOrderedSet[DebugExp]
                                ): ImplicationDebugExp = {
-    val debugExp = new ImplicationDebugExp(idCounter, description, originalExp.map(Simplifier.simplify(_, true)), finalExp.map(Simplifier.simplify(_, true)), term, isInternal_, children)
-    idCounter += 1
+    val debugExp = new ImplicationDebugExp(idCounter.getAndIncrement(), description, originalExp.map(Simplifier.simplify(_, true)), finalExp.map(Simplifier.simplify(_, true)), term, isInternal_, children)
     debugExp
   }
 
@@ -83,8 +81,7 @@ object DebugExp {
                                triggers: Seq[ast.Trigger],
                                tTriggers: Seq[Trigger]
                               ): QuantifiedDebugExp ={
-    val debugExp = new QuantifiedDebugExp(idCounter, description, isInternal_, children, quantifier, qvars, tQvars, triggers, tTriggers)
-    idCounter += 1
+    val debugExp = new QuantifiedDebugExp(idCounter.getAndIncrement(), description, isInternal_, children, quantifier, qvars, tQvars, triggers, tTriggers)
     debugExp
   }
 }
@@ -139,17 +136,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] = {
@@ -198,7 +196,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"
       }
@@ -231,7 +229,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)
     }
   }
 }
@@ -243,6 +241,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 {

src/main/scala/debugger/DebugParser.scala

@@ -18,7 +18,7 @@ class DebugParser extends FastParser {
     ((pp: (Position, Position)) => PVersionedIdnUseExp(name = parts(0), version = parts(1))(pp))
   }.pos
 
-  def debugOldLabel[$: P]: P[String] = (StringIn("debug") ~~ CharIn("@") ~~ CharIn("0-9", "A-Z", "a-z", "$_.").repX).!.opaque("debugOldLabel")
+  def debugOldLabel[$: P]: P[String] = (StringIn("debug") ~~ CharIn("@") ~~ CharIn("0-9", "A-Z", "a-z", "#$_.:").repX).!.opaque("debugOldLabel")
 
   def debugOldLabelUse[$: P]: P[PVersionedIdnUseExp] = P(debugOldLabel).map { case id =>
     val parts = id.split("@")

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,17 +53,31 @@ 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 {
+          case Some(e) => s" -> ${Simplifier.simplify(e, true)}"
+          case _ => ""
+        }
         bc.resourceID match {
-          case FieldID => s"acc(${bc.argsExp.get.head}.${bc.id}, ${Simplifier.simplify(bc.permExp.get, true)})"
+          case FieldID => s"acc(${bc.argsExp.get.head}.${bc.id}, ${Simplifier.simplify(bc.permExp.get, true)})$snapExpString"
           case PredicateID => s"acc(${bc.id}(${bc.argsExp.mkString(", ")}), ${Simplifier.simplify(bc.permExp.get, true)})"
         }
       case mwc: MagicWandChunk =>
@@ -215,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())))
@@ -321,7 +336,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
         obl.copy(timeout = Some(timeoutInt))
       }
     } catch {
-      case e: NumberFormatException =>
+      case _: NumberFormatException =>
         println("Invalid timeout value.")
         obl
     }
@@ -533,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())
   }

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],
@@ -147,59 +148,8 @@ case class SiliconDebuggingFailureContext(branchConditions: Seq[(ast.Exp, ast.Ex
                                           assumptions: InsertionOrderedSet[DebugExp],
                                           failedAssertion: Term,
                                           failedAssertionExp: DebugExp) extends FailureContext {
-  lazy val branchConditionString: String = {
-    if (branchConditions.nonEmpty) {
-      val branchConditionsString =
-        branchConditions
-          .map(_._2)
-          .map(bc => s"$bc [ ${bc.pos} ] ")
-          .mkString("\t\t", " ~~> ", "")
-
-      s"\n\t\tunder branch conditions:\n$branchConditionsString"
-    } else {
-      ""
-    }
-  }
-
-  lazy val counterExampleString: String = {
-    counterExample.fold("")(ce => s"\n\t\tcounterexample:\n$ce")
-  }
-
-  lazy val reasonUnknownString: String = {
-    if (reasonUnknown.isDefined) {
-      s"\nPotential prover incompleteness: ${reasonUnknown.get}"
-    } else {
-      ""
-    }
-  }
-
-  lazy val stateString: String = {
-    if (state.isDefined){
-      s"\n\nStore:\n\t\t${state.get.g.values.mkString("\n\t\t")}\n\nHeap:\n\t\t${state.get.h.values.mkString("\n\t\t")}"
-    } else {
-      ""
-    }
-  }
-
-  lazy val allAssumptionsString: String = {
-    if (assumptions.nonEmpty) {
-      val config = new DebugExpPrintConfiguration
-      config.isPrintInternalEnabled = true
-      s"\n\nassumptions:\n\t${assumptions.tail.foldLeft[String](assumptions.head.toString(config))((s, de) => de.toString(config) + s)}"
-    } else {
-      ""
-    }
-  }
-
-  lazy val failedAssertionString: String ={
-    if (failedAssertionExp.finalExp.isDefined){
-      s"\n\nFailed Assertion:\n\t\t${failedAssertionExp.finalExp.get.toString}"
-    } else {
-      failedAssertionExp.description.get
-    }
-  }
 
-  override lazy val toString: String = branchConditionString + counterExampleString + reasonUnknownString + stateString + allAssumptionsString + failedAssertionString
+  override lazy val toString: String = ""
 }
 
 trait SiliconCounterexample extends Counterexample {

src/main/scala/interfaces/state/Chunks.scala

@@ -33,7 +33,7 @@ trait NonQuantifiedChunk extends GeneralChunk {
   override def permMinus(perm: Term, permExp: Option[ast.Exp]): NonQuantifiedChunk
   override def permPlus(perm: Term, permExp: Option[ast.Exp]): NonQuantifiedChunk
   def withPerm(perm: Term, permExp: Option[ast.Exp]): NonQuantifiedChunk
-  def withSnap(snap: Term): NonQuantifiedChunk
+  def withSnap(snap: Term, snapExp: Option[ast.Exp]): NonQuantifiedChunk
 }
 
 trait QuantifiedChunk extends GeneralChunk {

src/main/scala/logger/writer/SymbExLogReportWriter.scala

@@ -31,7 +31,7 @@ object SymbExLogReportWriter {
   }
 
   private def heapChunkToJSON(chunk: Chunk) = chunk match {
-    case BasicChunk(PredicateID, id, args, _, snap, perm, _) =>
+    case BasicChunk(PredicateID, id, args, _, snap, _, perm, _) =>
       JsObject(
         "type" -> JsString("basic_predicate_chunk"),
         "predicate" -> JsString(id.toString),
@@ -40,7 +40,7 @@ object SymbExLogReportWriter {
         "perm" -> TermWriter.toJSON(perm)
       )
 
-    case BasicChunk(FieldID, id, Seq(receiver), _, snap, perm, _) =>
+    case BasicChunk(FieldID, id, Seq(receiver), _, snap, _, perm, _) =>
       JsObject(
         "type" -> JsString("basic_field_chunk"),
         "field" -> JsString(id.toString),

src/main/scala/reporting/Converter.scala

@@ -345,10 +345,10 @@ object Converter {
   def extractHeap(h: Iterable[Chunk], model: Model): ExtractedHeap = {
     var entries: Vector[HeapEntry] = Vector()
     h foreach {
-      case c @ BasicChunk(FieldID, _, _, _, _, _, _) =>
+      case c @ BasicChunk(FieldID, _, _, _, _, _, _, _) =>
         val entry = extractField(c, model)
         entries = entries :+ entry
-      case c @ BasicChunk(PredicateID, _, _, _, _, _, _) =>
+      case c @ BasicChunk(PredicateID, _, _, _, _, _, _, _) =>
         val entry = extractPredicate(c, model)
         entries = entries :+ entry
       case c: BasicChunk =>

src/main/scala/rules/Brancher.scala

@@ -6,8 +6,6 @@
 
 package viper.silicon.rules
 
-import viper.silicon.common.collections.immutable.InsertionOrderedSet
-
 import java.util.concurrent._
 import viper.silicon.common.concurrency._
 import viper.silicon.decider.PathConditionStack