Merge branch 'master' into meilers_fix_seq_matching_loop

Author: marcoeilers

src/main/scala/debugger/DebugExp.scala

@@ -8,9 +8,8 @@ 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 scala.collection.mutable
@@ -139,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] = {
@@ -198,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"
       }
@@ -231,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)
     }
   }
 }
@@ -243,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 {

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

src/main/scala/rules/Evaluator.scala

@@ -203,10 +203,10 @@ object evaluator extends EvaluationRules {
 
       case fa: ast.FieldAccess if s.qpFields.contains(fa.field) =>
         eval(s, fa.rcv, pve, v)((s1, tRcvr, eRcvr, v1) => {
-          val debugOldLabel = v1.getDebugOldLabel(s1)
+          val (debugHeapName, debugLabel) = v1.getDebugOldLabel(s1, fa.pos)
           val newFa = Option.when(withExp)({
             if (s1.isEvalInOld) ast.FieldAccess(eRcvr.get, fa.field)(fa.pos, fa.info, fa.errT)
-            else ast.DebugLabelledOld(ast.FieldAccess(eRcvr.get, fa.field)(), debugOldLabel)(fa.pos, fa.info, fa.errT)
+            else ast.DebugLabelledOld(ast.FieldAccess(eRcvr.get, fa.field)(), debugLabel)(fa.pos, fa.info, fa.errT)
           })
           val (relevantChunks, _) =
             quantifiedChunkSupporter.splitHeap[QuantifiedFieldChunk](s1.h, BasicChunkIdentifier(fa.field.name))
@@ -230,7 +230,7 @@ object evaluator extends EvaluationRules {
                 val fvfLookup = Lookup(fa.field.name, fvfDef.sm, tRcvr)
                 val fr1 = s1.functionRecorder.recordSnapshot(fa, v1.decider.pcs.branchConditions, fvfLookup)
                 val s2 = s1.copy(functionRecorder = fr1)
-                val s3 = if (Verifier.config.enableDebugging() && !s2.isEvalInOld) s2.copy(oldHeaps = s2.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s2))) else s2
+                val s3 = if (Verifier.config.enableDebugging() && !s2.isEvalInOld) s2.copy(oldHeaps = s2.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s2))) else s2
                 Q(s3, fvfLookup, newFa, v1)
               } else {
                 val toAssert = IsPositive(totalPermissions.replace(`?r`, tRcvr))
@@ -245,7 +245,7 @@ object evaluator extends EvaluationRules {
                     else
                       s1.possibleTriggers
                     val s2 = s1.copy(functionRecorder = fr1, possibleTriggers = possTriggers)
-                    val s3 = if (Verifier.config.enableDebugging() && !s2.isEvalInOld) s2.copy(oldHeaps = s2.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s2))) else s2
+                    val s3 = if (Verifier.config.enableDebugging() && !s2.isEvalInOld) s2.copy(oldHeaps = s2.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s2))) else s2
                     Q(s3, fvfLookup, newFa, v1)}
               }
             case _ =>
@@ -317,12 +317,12 @@ object evaluator extends EvaluationRules {
           chunkSupporter.lookup(s1, s1.h, resource, tArgs, eArgs, ve, v1)((s2, h2, tSnap, v2) => {
             val fr = s2.functionRecorder.recordSnapshot(fa, v2.decider.pcs.branchConditions, tSnap)
             val s3 = s2.copy(h = h2, functionRecorder = fr)
-            val debugOldLabel = v2.getDebugOldLabel(s3)
+            val (debugHeapName, debugLabel) = v2.getDebugOldLabel(s3, fa.pos)
             val newFa = Option.when(withExp)({
               if (s3.isEvalInOld) ast.FieldAccess(eArgs.get.head, fa.field)(e.pos, e.info, e.errT)
-              else ast.DebugLabelledOld(ast.FieldAccess(eArgs.get.head, fa.field)(), debugOldLabel)(e.pos, e.info, e.errT)
+              else ast.DebugLabelledOld(ast.FieldAccess(eArgs.get.head, fa.field)(), debugLabel)(e.pos, e.info, e.errT)
             })
-            val s4 = if (Verifier.config.enableDebugging() && !s3.isEvalInOld) s3.copy(oldHeaps = s3.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s3))) else s3
+            val s4 = if (Verifier.config.enableDebugging() && !s3.isEvalInOld) s3.copy(oldHeaps = s3.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s3))) else s3
             Q(s4, tSnap, newFa, v1)
           })
         })
@@ -340,11 +340,15 @@ object evaluator extends EvaluationRules {
           Q(s1, t0, e0New.map(ast.Old(_)(e.pos, e.info, e.errT)), v1))
 
       case old@ast.DebugLabelledOld(e0, lbl) =>
-        s.oldHeaps.get(lbl) match {
+        val heapName = if (lbl.contains("#"))
+          lbl.substring(0, lbl.indexOf("#"))
+        else
+          lbl
+        s.oldHeaps.get(heapName) match {
           case None =>
-            createFailure(pve dueTo LabelledStateNotReached(ast.LabelledOld(e0, lbl)(old.pos, old.info, old.errT)), v, s, "labelled state reached")
+            createFailure(pve dueTo LabelledStateNotReached(ast.LabelledOld(e0, heapName)(old.pos, old.info, old.errT)), v, s, "labelled state reached")
           case _ =>
-            evalInOldState(s, lbl, e0, pve, v)((s1, t0, _, v1) =>
+            evalInOldState(s, heapName, e0, pve, v)((s1, t0, _, v1) =>
               Q(s1, t0, Some(old), v1))
         }
 
@@ -581,9 +585,11 @@ object evaluator extends EvaluationRules {
                   }
                   val currentPermAmount = PermLookup(field.name, pmDef.pm, args.head)
                   v1.decider.prover.comment(s"perm($resacc)  ~~>  assume upper permission bound")
-                  val exp = Option.when(withExp)(ast.PermLeCmp(ast.DebugLabelledOld(ast.CurrentPerm(resacc)(), v1.getDebugOldLabel(s2))(), ast.FullPerm()())())
+                  val (debugHeapName, debugLabel) = v1.getDebugOldLabel(s2, resacc.pos, Some(h))
+                  val exp = Option.when(withExp)(ast.PermLeCmp(ast.DebugLabelledOld(ast.CurrentPerm(resacc)(), debugLabel)(), ast.FullPerm()())())
                   v1.decider.assume(PermAtMost(currentPermAmount, FullPerm), exp, exp.map(s2.substituteVarsInExp(_)))
-                  (s2, currentPermAmount)
+                  val s3 = if (Verifier.config.enableDebugging()) s2.copy(oldHeaps = s2.oldHeaps + (debugHeapName -> h)) else s2
+                  (s3, currentPermAmount)
 
                 case predicate: ast.Predicate =>
                   val (relevantChunks, _) =
@@ -1102,7 +1108,6 @@ object evaluator extends EvaluationRules {
             val assertExpNew = Option.when(withExp)(ast.GeCmp(esNew.get(1), ast.IntLit(0)())(e1.pos, e1.info, e1.errT))
             v1.decider.assert(AtLeast(t1, IntLiteral(0))) {
               case true =>
-                val assertExp2 = Option.when(withExp)(ast.LtCmp(e1, ast.SeqLength(e0)())(e1.pos, e1.info, e1.errT))
                 val assertExp2New = Option.when(withExp)(ast.LtCmp(esNew.get(1), ast.SeqLength(esNew.get(0))())(e1.pos, e1.info, e1.errT))
                 v1.decider.assert(Less(t1, SeqLength(t0))) {
                   case true =>