From a9ea5576631ba0af2637d2d10b5e10ed5adac4e6 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Thu, 30 Nov 2023 15:13:16 +0100
Subject: [PATCH 01/22] interaction - first commit

---
 .../scala/viper/silver/frontend/SilFrontend.scala    | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index a2ee386f0..c8ee02140 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala
@@ -23,6 +23,12 @@ import viper.silver.FastMessaging
  */
 case class MissingDependencyException(msg: String) extends Exception
 
+object FrontendStateCache {
+  var resolver: Resolver = _
+  var pprogram: PProgram = _
+  var translator: Translator = _
+}
+
 trait SilFrontend extends DefaultFrontend {
 
   /**
@@ -288,6 +294,8 @@ trait SilFrontend extends DefaultFrontend {
     plugins.beforeResolve(input) match {
       case Some(inputPlugin) =>
         val r = Resolver(inputPlugin)
+        FrontendStateCache.resolver = r
+        FrontendStateCache.pprogram = inputPlugin
         val analysisResult = r.run
         val warnings = for (m <- FastMessaging.sortmessages(r.messages) if !m.error) yield {
           TypecheckerWarning(m.label, m.pos)
@@ -312,7 +320,9 @@ trait SilFrontend extends DefaultFrontend {
 
     plugins.beforeTranslate(input) match {
       case Some(modifiedInputPlugin) =>
-        Translator(modifiedInputPlugin).translate match {
+        val translator = Translator(modifiedInputPlugin)
+        FrontendStateCache.translator = translator
+        translator.translate match {
           case Some(program) =>
             Succ(program)
 

From 84c7b6882ae06c84ba0c63e12d4282fc312e3884 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Mon, 4 Dec 2023 14:59:21 +0100
Subject: [PATCH 02/22] add versioned variables to parser

---
 .../viper/silver/parser/FastParser.scala      | 17 +++++++-
 .../scala/viper/silver/parser/ParseAst.scala  | 16 +++++++-
 .../scala/viper/silver/parser/Resolver.scala  | 41 +++++++++++++++++++
 .../viper/silver/parser/Transformer.scala     |  1 +
 .../viper/silver/parser/Translator.scala      |  7 ++++
 5 files changed, 79 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index 8e6f9fcdc..d32579b1a 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -382,6 +382,8 @@ class FastParser {
   // Actual Parser starts from here
   def identContinues[$: P] = CharIn("0-9", "A-Z", "a-z", "$_")
 
+  def versionStarts[$: P] = CharIn("@")
+
   def keyword[$: P](check: String) = check ~~ !identContinues
 
   def parens[$: P, T](p: => P[T]) = "(" ~ p ~ ")"
@@ -399,7 +401,9 @@ class FastParser {
 
   // Note that `typedfuncApp` is before `"(" ~ exp ~ ")"` to ensure that the latter doesn't gobble up the brackets for the former
   // and then look like an `funcApp` up untill the `: type` part, after which we need to backtrack all the way back (or error if cut)
-  def atom(implicit ctx : P[_]) : P[PExp] = P(ParserExtension.newExpAtStart(ctx) | annotatedAtom
+  // TODO ake: versionedidnuse
+  def atom(implicit ctx : P[_]) : P[PExp] = P(ParserExtension.newExpAtStart(ctx) | versionedidnuse
+    | annotatedAtom
     | integer | booltrue | boolfalse | nul | old
     | result | unExp | typedFuncApp
     | "(" ~ exp ~ ")" | accessPred | inhaleExhale | perm | let | quant | forperm | unfolding | applying
@@ -432,13 +436,22 @@ class FastParser {
 
   def identifier[$: P]: P[Unit] = CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_").repX
 
+  def versionedIdentifier[$: P]: P[Unit] = CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_").repX ~~ CharIn("@") ~~ CharIn("0-9") ~~ CharIn("0-9")
+
   def annotationIdentifier[$: P]: P[String] = (CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_.").repX).!
 
   def ident[$: P]: P[String] = identifier.!.filter(a => !keywords.contains(a)).opaque("identifier")
 
+  def versionedIdent[$: P]: P[String] = versionedIdentifier.!.opaque("versionedIdentifier")
+
   def idnuse[$: P]: P[PIdnUse] = FP(ident).map { case (pos, id) => PIdnUse(id)(pos) }
 
-  def oldLabel[$: P]: P[PIdnUse] = idnuse | FP(LabelledOld.LhsOldLabel.!).map {
+  def versionedidnuse[$: P]: P[PVersionedIdnUse] = FP(versionedIdent).map { case (pos, id) => {
+    val parts = id.split("@")
+    PVersionedIdnUse(name=parts(0), version=parts(1))(pos)
+  } }
+
+  def oldLabel[$: P]: P[PIdnUse] = idnuse | FP(LabelledOld.LhsOldLabel.!).map { // TODO ake: oldLabel parsing
     case (pos, lhsOldLabel) => PIdnUse(lhsOldLabel)(pos)
   }
 
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
index 09b1bc8a7..be53acf08 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -164,6 +164,19 @@ case class PIdnUse(name: String)(val pos: (Position, Position)) extends PExp wit
   }
 }
 
+case class PVersionedIdnUse(name: String, version: String, separator: String = "@")(val pos: (Position, Position)) extends PExp with PIdentifier   {
+  var decl: PTypedDeclaration = null
+
+  val versionedName: String = name + separator + version
+
+  override val typeSubstitutions = List(PTypeSubstitution.id)
+
+  def forceSubstitution(ts: PTypeSubstitution) = {
+    typ = typ.substitute(ts)
+    assert(typ.isGround)
+  }
+}
+
 trait PAnyFormalArgDecl extends PNode with PUnnamedTypedDeclaration
 
 case class PUnnamedFormalArgDecl(var typ: PType)(val pos: (Position, Position)) extends PAnyFormalArgDecl
@@ -991,7 +1004,7 @@ case class POld(e: PExp)(val pos: (Position, Position)) extends POldExp {
   override val opName = "old"
 }
 
-case class PLabelledOld(label: PIdnUse, e: PExp)(val pos: (Position, Position)) extends POldExp {
+case class PLabelledOld(label: PIdnUse, e: PExp)(val pos: (Position, Position)) extends POldExp { // TODO ake: labelOld
   override val opName = "old#labeled"
 }
 
@@ -1498,6 +1511,7 @@ object Nodes {
     n match {
       case PIdnDef(_) => Nil
       case PIdnUse(_) => Nil
+      case PVersionedIdnUse(_, _, _) => Nil
       case PUnnamedFormalArgDecl(typ) => Seq(typ)
       case PFormalArgDecl(idndef, typ) => Seq(idndef, typ)
       case PFormalReturnDecl(idndef, typ) => Seq(idndef, typ)
diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
index f243a5677..589ac92c3 100644
--- a/src/main/scala/viper/silver/parser/Resolver.scala
+++ b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -360,6 +360,27 @@ case class TypeChecker(names: NameAnalyser) {
     }
   }
 
+  // TODO ake: copy pasted from above
+  def acceptAndCheckTypedEntityWithVersion[T1: ClassTag, T2: ClassTag]
+  (idnUses: Seq[PVersionedIdnUse], errorMessage: => String): Unit = {
+
+    /* TODO: Ensure that the ClassTags denote subtypes of TypedEntity */
+    val acceptedClasses = Seq[Class[_]](classTag[T1].runtimeClass, classTag[T2].runtimeClass)
+
+    idnUses.foreach { use =>
+      val decl = names.definition(curMember)(PIdnUse(use.name)(use.pos)).get
+
+      acceptedClasses.find(_.isInstance(decl)) match {
+        case Some(_) =>
+          val td = decl.asInstanceOf[PTypedDeclaration]
+          use.typ = td.typ
+          use.decl = td
+        case None =>
+          messages ++= FastMessaging.message(use, errorMessage)
+      }
+    }
+  }
+
   def check(typ: PType): Unit = {
     typ match {
       case _: PPredicateType | _: PWandType =>
@@ -725,6 +746,9 @@ case class TypeChecker(names: NameAnalyser) {
       case piu: PIdnUse =>
         acceptAndCheckTypedEntity[PAnyVarDecl, Nothing](Seq(piu), "expected variable identifier")
 
+      case pviu: PVersionedIdnUse =>
+        acceptAndCheckTypedEntityWithVersion[PAnyVarDecl, Nothing](Seq(pviu), "expected variable identifier with version") // TODO ake: versionedVar
+
       case pl@PLet(e, ns) =>
         val oldCurMember = curMember
         curMember = ns
@@ -908,6 +932,22 @@ case class NameAnalyser() {
                 }
               case _ =>
             }
+          case i@PVersionedIdnUse(name, _, _) =>
+            // look up in both maps (if we are not in a method currently, we look in the same map twice, but that is ok)
+            getCurrentMap.getOrElse(name, globalDeclarationMap.getOrElse(name, PUnknownEntity())) match {
+              case PUnknownEntity() =>
+                // domain types can also be type variables, which need not be declared
+                // goto and state labels may exist out of scope (but must exist in method, this is checked in final AST in checkIdentifiers)
+                if (i.parent.isDefined) {
+                  val parent = i.parent.get
+                  if (!parent.isInstanceOf[PDomainType] && !parent.isInstanceOf[PGoto] &&
+                    !(parent.isInstanceOf[PLabelledOld] && i == parent.asInstanceOf[PLabelledOld].label) &&
+                    !(name == LabelledOld.LhsOldLabel && parent.isInstanceOf[PLabelledOld])) {
+                    messages ++= FastMessaging.message(i, s"identifier $name not defined.")
+                  }
+                }
+              case _ =>
+            }
           case _ =>
         }
 
@@ -931,6 +971,7 @@ case class NameAnalyser() {
           case _: PDeclaration => true
           case _: PScope => true
           case _: PIdnUse => true
+          case _: PVersionedIdnUse => true // TODO ake: ???
           case _ => target.isDefined
         }
       }
diff --git a/src/main/scala/viper/silver/parser/Transformer.scala b/src/main/scala/viper/silver/parser/Transformer.scala
index 9e8fa9c7a..e9c0b5c7e 100644
--- a/src/main/scala/viper/silver/parser/Transformer.scala
+++ b/src/main/scala/viper/silver/parser/Transformer.scala
@@ -24,6 +24,7 @@ object Transformer {
       val newNode = parent match {
         case _: PIdnDef => parent
         case _: PIdnUse => parent
+        case _: PVersionedIdnUse => parent
         case p@PFormalArgDecl(idndef, typ) => PFormalArgDecl(go(idndef), go(typ))(p.pos)
         case p@PFormalReturnDecl(idndef, typ) => PFormalReturnDecl(go(idndef), go(typ))(p.pos)
         case p@PLogicalVarDecl(idndef, typ) => PLogicalVarDecl(go(idndef), go(typ))(p.pos)
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 0d098af67..699ec97f4 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -368,6 +368,13 @@ case class Translator(program: PProgram) {
           // Should have been caught by the type checker.
           case _ => sys.error("should not occur in type-checked program")
         }
+      case pviu@PVersionedIdnUse(_, _, _) =>
+        pviu.decl match {
+          case _: PAnyVarDecl => LocalVar(pviu.versionedName, ttyp(pexp.typ))(pos, info)
+          // A malformed AST where a field, function or other declaration is used as a variable.
+          // Should have been caught by the type checker.
+          case _ => sys.error("should not occur in type-checked program")
+        }
       case pbe @ PBinExp(left, op, right) =>
         val (l, r) = (exp(left), exp(right))
         op match {

From 9be3e15f91c79e6291c118ec9cec769cf49f48f2 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Thu, 7 Dec 2023 09:48:42 +0100
Subject: [PATCH 03/22] add ast.LocalVarWithVersion

---
 src/main/scala/viper/silver/ast/Expression.scala    | 7 +++++++
 src/main/scala/viper/silver/parser/FastParser.scala | 2 +-
 src/main/scala/viper/silver/parser/Resolver.scala   | 2 +-
 src/main/scala/viper/silver/parser/Translator.scala | 2 +-
 4 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 090d05228..67603226f 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -713,6 +713,13 @@ case class Result(typ: Type)(val pos: Position = NoPosition, val info: Info = No
   lazy val name = "result"
 }
 
+/** A special local variable with a version for debugging */
+case class LocalVarWithVersion(name: String, typ: Type)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AbstractLocalVar with Lhs {
+  def nameWithoutVersion = name.substring(0, name.lastIndexOf("@"))
+  override lazy val check: Seq[ConsistencyError] =
+    if (!Consistency.validUserDefinedIdentifier(name)) Seq(ConsistencyError("Local var name must be valid identifier.", pos)) else Seq()
+}
+
 // --- Mathematical sequences
 
 /**
diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index d32579b1a..d7bc87304 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -436,7 +436,7 @@ class FastParser {
 
   def identifier[$: P]: P[Unit] = CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_").repX
 
-  def versionedIdentifier[$: P]: P[Unit] = CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_").repX ~~ CharIn("@") ~~ CharIn("0-9") ~~ CharIn("0-9")
+  def versionedIdentifier[$: P]: P[Unit] = CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_").repX ~~ CharIn("@") ~~ CharIn("0-9") ~~ CharIn("0-9").repX
 
   def annotationIdentifier[$: P]: P[String] = (CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_.").repX).!
 
diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
index 589ac92c3..2a4321dd2 100644
--- a/src/main/scala/viper/silver/parser/Resolver.scala
+++ b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -747,7 +747,7 @@ case class TypeChecker(names: NameAnalyser) {
         acceptAndCheckTypedEntity[PAnyVarDecl, Nothing](Seq(piu), "expected variable identifier")
 
       case pviu: PVersionedIdnUse =>
-        acceptAndCheckTypedEntityWithVersion[PAnyVarDecl, Nothing](Seq(pviu), "expected variable identifier with version") // TODO ake: versionedVar
+        acceptAndCheckTypedEntityWithVersion[PAnyVarDecl, Nothing](Seq(pviu), "expected variable identifier with version")
 
       case pl@PLet(e, ns) =>
         val oldCurMember = curMember
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 699ec97f4..bce7b52b7 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -370,7 +370,7 @@ case class Translator(program: PProgram) {
         }
       case pviu@PVersionedIdnUse(_, _, _) =>
         pviu.decl match {
-          case _: PAnyVarDecl => LocalVar(pviu.versionedName, ttyp(pexp.typ))(pos, info)
+          case _: PAnyVarDecl => LocalVarWithVersion(pviu.versionedName, ttyp(pexp.typ))(pos, info)
           // A malformed AST where a field, function or other declaration is used as a variable.
           // Should have been caught by the type checker.
           case _ => sys.error("should not occur in type-checked program")

From a64131794dbeeea8eaff71359ea945407a0c8a78 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Sun, 10 Dec 2023 10:36:51 +0100
Subject: [PATCH 04/22] add ast.DebugLabelledOld

---
 .../scala/viper/silver/ast/Expression.scala    |  6 ++++++
 .../silver/ast/pretty/PrettyPrinter.scala      |  2 ++
 .../scala/viper/silver/parser/FastParser.scala | 18 +++++++++++++++---
 .../scala/viper/silver/parser/ParseAst.scala   |  6 +++++-
 .../scala/viper/silver/parser/Translator.scala |  2 ++
 5 files changed, 30 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 67603226f..6dfb7ac8b 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -512,6 +512,12 @@ case class LabelledOld(exp: Exp, oldLabel: String)(val pos: Position = NoPositio
       Consistency.checkPure(exp)
 }
 
+/** Old expression that are used in the debugger. */
+case class DebugLabelledOld(exp: Exp, oldLabel: String)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends OldExp {
+  override lazy val check : Seq[ConsistencyError] =
+    Consistency.checkPure(exp)
+}
+
 case object LabelledOld {
   val LhsOldLabel = "lhs"
 }
diff --git a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
index cb2896faa..99522e710 100644
--- a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
+++ b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
@@ -775,6 +775,8 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
         text("old") <> parens(show(exp))
       case LabelledOld(exp,label) =>
         text("old") <> brackets(label) <> parens(show(exp))
+      case DebugLabelledOld(exp, label) =>
+        text("old") <> brackets(label) <> parens(show(exp))
       case Let(v, exp, body) =>
         parens(text("let") <+> text(v.name) <+> "==" <> nest(defaultIndent, line <> parens(show(exp))) <+>
           "in" <> nest(defaultIndent, line <> show(body)))
diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index d7bc87304..b7b487863 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -401,8 +401,8 @@ class FastParser {
 
   // Note that `typedfuncApp` is before `"(" ~ exp ~ ")"` to ensure that the latter doesn't gobble up the brackets for the former
   // and then look like an `funcApp` up untill the `: type` part, after which we need to backtrack all the way back (or error if cut)
-  // TODO ake: versionedidnuse
   def atom(implicit ctx : P[_]) : P[PExp] = P(ParserExtension.newExpAtStart(ctx) | versionedidnuse
+    | debugOld
     | annotatedAtom
     | integer | booltrue | boolfalse | nul | old
     | result | unExp | typedFuncApp
@@ -451,11 +451,23 @@ class FastParser {
     PVersionedIdnUse(name=parts(0), version=parts(1))(pos)
   } }
 
-  def oldLabel[$: P]: P[PIdnUse] = idnuse | FP(LabelledOld.LhsOldLabel.!).map { // TODO ake: oldLabel parsing
+  def debugOldLabel[$: P]: P[String] = (StringIn("line") ~~ CharIn("@") ~~ CharIn("0-9", "A-Z", "a-z", "$_.").repX).!.opaque("debugOldLabel")
+
+  def debugOldLabelUse[$: P]: P[PVersionedIdnUse] = FP(debugOldLabel).map { case (pos, id) => {
+    val parts = id.split("@")
+    PVersionedIdnUse(name = parts(0), version = parts(1))(pos)
+  }
+  }
+
+  def debugOld[$: P]: P[PExp] = P(StringIn("old") ~ FP("[" ~ debugOldLabelUse ~ "]" ~ parens(exp)).map {
+    case (pos, (a, b)) => PDebugLabelledOld(a, b)(pos)})
+
+  def oldLabel[$: P]: P[PIdnUse] = idnuse | FP(LabelledOld.LhsOldLabel.!).map {
     case (pos, lhsOldLabel) => PIdnUse(lhsOldLabel)(pos)
   }
 
-  def old[$: P]: P[PExp] = P(StringIn("old") ~ (FP(parens(exp)).map { case (pos, e) => POld(e)(pos) } | FP("[" ~ oldLabel ~ "]" ~ parens(exp)).map {
+  def old[$: P]: P[PExp] = P(StringIn("old") ~ (FP(parens(exp)).map { case (pos, e) => POld(e)(pos) }
+    | FP("[" ~ oldLabel ~ "]" ~ parens(exp)).map {
     case (pos, (a, b)) => PLabelledOld(a, b)(pos)
   }))
 
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
index be53acf08..3ece00806 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -1004,10 +1004,14 @@ case class POld(e: PExp)(val pos: (Position, Position)) extends POldExp {
   override val opName = "old"
 }
 
-case class PLabelledOld(label: PIdnUse, e: PExp)(val pos: (Position, Position)) extends POldExp { // TODO ake: labelOld
+case class PLabelledOld(label: PIdnUse, e: PExp)(val pos: (Position, Position)) extends POldExp {
   override val opName = "old#labeled"
 }
 
+case class PDebugLabelledOld(label: PVersionedIdnUse, e: PExp)(val pos: (Position, Position)) extends POldExp {
+  override val opName = "debug#old#labeled"
+}
+
 sealed trait PCollectionLiteral extends POpApp {
   def pElementType: PType
 
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index bce7b52b7..ebe1fd0e9 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -569,6 +569,8 @@ case class Translator(program: PProgram) {
         Old(exp(e))(pos, info)
       case PLabelledOld(lbl,e) =>
         LabelledOld(exp(e),lbl.name)(pos, info)
+      case PDebugLabelledOld(lbl, e) =>
+        DebugLabelledOld(exp(e), lbl.name)(pos, info)
       case PCondExp(cond, thn, els) =>
         CondExp(exp(cond), exp(thn), exp(els))(pos, info)
       case PCurPerm(res) =>

From 77a8323b42cb838e6f3d30b8d9990e19a81d91c5 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Tue, 2 Jan 2024 16:39:50 +0100
Subject: [PATCH 05/22] typecheck variables with versions

---
 .../scala/viper/silver/parser/Resolver.scala    | 17 +++++------------
 .../scala/viper/silver/parser/Translator.scala  | 10 ++++------
 2 files changed, 9 insertions(+), 18 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
index 2a4321dd2..e819334bf 100644
--- a/src/main/scala/viper/silver/parser/Resolver.scala
+++ b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -40,6 +40,7 @@ case class TypeChecker(names: NameAnalyser) {
   var curMember: PScope = null
   var curFunction: PFunction = null
   var resultAllowed: Boolean = false
+  var debugVariableTypes: Map[String, PType] = Map.empty
 
   /** to record error messages */
   var messages: FastMessaging.Messages = Nil
@@ -360,23 +361,15 @@ case class TypeChecker(names: NameAnalyser) {
     }
   }
 
-  // TODO ake: copy pasted from above
   def acceptAndCheckTypedEntityWithVersion[T1: ClassTag, T2: ClassTag]
   (idnUses: Seq[PVersionedIdnUse], errorMessage: => String): Unit = {
 
-    /* TODO: Ensure that the ClassTags denote subtypes of TypedEntity */
-    val acceptedClasses = Seq[Class[_]](classTag[T1].runtimeClass, classTag[T2].runtimeClass)
-
     idnUses.foreach { use =>
-      val decl = names.definition(curMember)(PIdnUse(use.name)(use.pos)).get
+      val decl1 = debugVariableTypes.get(use.versionedName)
 
-      acceptedClasses.find(_.isInstance(decl)) match {
-        case Some(_) =>
-          val td = decl.asInstanceOf[PTypedDeclaration]
-          use.typ = td.typ
-          use.decl = td
-        case None =>
-          messages ++= FastMessaging.message(use, errorMessage)
+      decl1 match {
+        case Some(value) => use.typ = value // TODO ake: set use.decl?
+        case None => messages ++= FastMessaging.message(use, errorMessage)
       }
     }
   }
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index ebe1fd0e9..3a4022471 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -369,11 +369,9 @@ case class Translator(program: PProgram) {
           case _ => sys.error("should not occur in type-checked program")
         }
       case pviu@PVersionedIdnUse(_, _, _) =>
-        pviu.decl match {
-          case _: PAnyVarDecl => LocalVarWithVersion(pviu.versionedName, ttyp(pexp.typ))(pos, info)
-          // A malformed AST where a field, function or other declaration is used as a variable.
-          // Should have been caught by the type checker.
-          case _ => sys.error("should not occur in type-checked program")
+        pexp.typ match {
+          case null => sys.error("should not occur in type-checked program")
+          case _ => LocalVarWithVersion(pviu.versionedName, ttyp(pexp.typ))(pos, info)
         }
       case pbe @ PBinExp(left, op, right) =>
         val (l, r) = (exp(left), exp(right))
@@ -570,7 +568,7 @@ case class Translator(program: PProgram) {
       case PLabelledOld(lbl,e) =>
         LabelledOld(exp(e),lbl.name)(pos, info)
       case PDebugLabelledOld(lbl, e) =>
-        DebugLabelledOld(exp(e), lbl.name)(pos, info)
+        DebugLabelledOld(exp(e), lbl.versionedName)(pos, info)
       case PCondExp(cond, thn, els) =>
         CondExp(exp(cond), exp(thn), exp(els))(pos, info)
       case PCurPerm(res) =>

From 8ea35c236005b329f3e9fad8268c8d1204b13508 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Wed, 10 Jan 2024 17:27:47 +0100
Subject: [PATCH 06/22] optimize debug workflow and printing

---
 src/main/scala/viper/silver/ast/Expression.scala      |  7 +++++++
 .../scala/viper/silver/frontend/SilFrontend.scala     |  3 ++-
 src/main/scala/viper/silver/parser/Translator.scala   | 11 +++++++++--
 3 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 6dfb7ac8b..54b5cd5a7 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -11,10 +11,17 @@ import viper.silver.ast.pretty._
 import viper.silver.ast.utility._
 import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion
 import viper.silver.ast.utility.rewriter.{StrategyBuilder, Traverse}
+import viper.silver.parser.PExp
 import viper.silver.verifier.{ConsistencyError, VerificationResult}
 
 /** Expressions. */
 sealed trait Exp extends Hashable with Typed with Positioned with Infoed with TransformableErrors with PrettyExpression {
+  var sourcePExp : Option[PExp] = None
+
+  def setSourcePExp(pexp: PExp): Unit = {
+    sourcePExp = Some(pexp)
+  }
+
   lazy val isPure = Expressions.isPure(this)
   def isHeapDependent(p: Program) = Expressions.isHeapDependent(this, p)
   def isTopLevelHeapDependent(p: Program) = Expressions.isTopLevelHeapDependent(this, p)
diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index c8ee02140..0fa81c47a 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala
@@ -252,7 +252,8 @@ trait SilFrontend extends DefaultFrontend {
 
     if (state == DefaultStates.ConsistencyCheck && _errors.isEmpty) {
       filter(_program.get) match {
-        case Succ(program) => _program = Some(program)
+        case Succ(program) =>
+          _program = Some(program)
         case Fail(errors) => _errors ++= errors
       }
     }
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 3a4022471..7dcdc0d0e 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -191,7 +191,8 @@ case class Translator(program: PProgram) {
     val subInfo = NoInfo
     s match {
       case PAssign(targets, PCall(method, args, _)) if members(method.name).isInstanceOf[Method] =>
-        methodCallAssign(s, targets, ts => MethodCall(findMethod(method), args map exp, ts)(pos, info))
+        val e1 = methodCallAssign(s, targets, ts => MethodCall(findMethod(method), args map exp, ts)(pos, info))
+        e1
       case PAssign(targets, _) if targets.length != 1 =>
         sys.error(s"Found non-unary target of assignment")
       case PAssign(Seq(target), PNewExp(fieldsOpt)) =>
@@ -355,8 +356,14 @@ case class Translator(program: PProgram) {
     }
   }
 
-  /** Takes a `PExp` and turns it into an `Exp`. */
   def exp(parseExp: PExp): Exp = {
+    val e = expInternal(parseExp)
+    e.setSourcePExp(parseExp)
+    e
+  }
+
+  /** Takes a `PExp` and turns it into an `Exp`. */
+  def expInternal(parseExp: PExp): Exp = {
     val pos = parseExp
     val (pexp, annotationMap) = extractAnnotation(parseExp)
     val info = if (annotationMap.isEmpty) NoInfo else AnnotationInfo(annotationMap)

From 666a9315ae518ab1661855eb64d7f74c2a06baa7 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Wed, 17 Jan 2024 12:16:30 +0100
Subject: [PATCH 07/22] cleanup TODOs

---
 src/main/scala/viper/silver/parser/Resolver.scala   | 4 ++--
 src/main/scala/viper/silver/parser/Translator.scala | 3 +--
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
index e819334bf..df696ddf3 100644
--- a/src/main/scala/viper/silver/parser/Resolver.scala
+++ b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -368,7 +368,7 @@ case class TypeChecker(names: NameAnalyser) {
       val decl1 = debugVariableTypes.get(use.versionedName)
 
       decl1 match {
-        case Some(value) => use.typ = value // TODO ake: set use.decl?
+        case Some(value) => use.typ = value
         case None => messages ++= FastMessaging.message(use, errorMessage)
       }
     }
@@ -964,7 +964,7 @@ case class NameAnalyser() {
           case _: PDeclaration => true
           case _: PScope => true
           case _: PIdnUse => true
-          case _: PVersionedIdnUse => true // TODO ake: ???
+          case _: PVersionedIdnUse => true
           case _ => target.isDefined
         }
       }
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 7dcdc0d0e..22f9dda2c 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -191,8 +191,7 @@ case class Translator(program: PProgram) {
     val subInfo = NoInfo
     s match {
       case PAssign(targets, PCall(method, args, _)) if members(method.name).isInstanceOf[Method] =>
-        val e1 = methodCallAssign(s, targets, ts => MethodCall(findMethod(method), args map exp, ts)(pos, info))
-        e1
+        methodCallAssign(s, targets, ts => MethodCall(findMethod(method), args map exp, ts)(pos, info))
       case PAssign(targets, _) if targets.length != 1 =>
         sys.error(s"Found non-unary target of assignment")
       case PAssign(Seq(target), PNewExp(fieldsOpt)) =>

From d09e011fa313860d76316805c9c301c4540e5c6e Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Sat, 20 Jan 2024 08:35:42 +0100
Subject: [PATCH 08/22] implement sourcePNodeInfo cleanup

---
 src/main/scala/viper/silver/ast/Ast.scala          |  6 ++++++
 src/main/scala/viper/silver/ast/Expression.scala   |  5 -----
 .../scala/viper/silver/parser/Translator.scala     | 14 +++++---------
 3 files changed, 11 insertions(+), 14 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index 5478d261e..304de1bcf 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -12,6 +12,7 @@ import pretty.FastPrettyPrinter
 import utility._
 import viper.silver.ast.utility.rewriter.Traverse.Traverse
 import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder, Traverse}
+import viper.silver.parser.PNode
 import viper.silver.verifier.errors.ErrorNode
 import viper.silver.verifier.{AbstractVerificationError, ConsistencyError, ErrorReason}
 
@@ -371,6 +372,11 @@ case object NoInfo extends Info {
   override val isCached = false
 }
 
+case class SourcePNodeInfo(sourcePNode: PNode) extends Info {
+  override val comment = Nil
+  override val isCached = false
+}
+
 case class AnnotationInfo(values: Map[String, Seq[String]]) extends Info {
   override val isCached = false
   override val comment = Nil
diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 54b5cd5a7..2f6ec6526 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -16,11 +16,6 @@ import viper.silver.verifier.{ConsistencyError, VerificationResult}
 
 /** Expressions. */
 sealed trait Exp extends Hashable with Typed with Positioned with Infoed with TransformableErrors with PrettyExpression {
-  var sourcePExp : Option[PExp] = None
-
-  def setSourcePExp(pexp: PExp): Unit = {
-    sourcePExp = Some(pexp)
-  }
 
   lazy val isPure = Expressions.isPure(this)
   def isHeapDependent(p: Program) = Expressions.isHeapDependent(this, p)
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 22f9dda2c..f49d54e03 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -187,7 +187,8 @@ case class Translator(program: PProgram) {
   def stmt(pStmt: PStmt): Stmt = {
     val pos = pStmt
     val (s, annotations) = extractAnnotationFromStmt(pStmt)
-    val info = if (annotations.isEmpty) NoInfo else AnnotationInfo(annotations)
+    val sourcePNodeInfo = SourcePNodeInfo(pStmt)
+    val info = if (annotations.isEmpty) sourcePNodeInfo else ConsInfo(sourcePNodeInfo, AnnotationInfo(annotations))
     val subInfo = NoInfo
     s match {
       case PAssign(targets, PCall(method, args, _)) if members(method.name).isInstanceOf[Method] =>
@@ -355,17 +356,12 @@ case class Translator(program: PProgram) {
     }
   }
 
-  def exp(parseExp: PExp): Exp = {
-    val e = expInternal(parseExp)
-    e.setSourcePExp(parseExp)
-    e
-  }
-
   /** Takes a `PExp` and turns it into an `Exp`. */
-  def expInternal(parseExp: PExp): Exp = {
+  def exp(parseExp: PExp): Exp = {
     val pos = parseExp
     val (pexp, annotationMap) = extractAnnotation(parseExp)
-    val info = if (annotationMap.isEmpty) NoInfo else AnnotationInfo(annotationMap)
+    val sourcePNodeInfo = SourcePNodeInfo(parseExp)
+    val info = if (annotationMap.isEmpty) sourcePNodeInfo else ConsInfo(sourcePNodeInfo, AnnotationInfo(annotationMap))
     pexp match {
       case piu @ PIdnUse(name) =>
         piu.decl match {

From 88dc6f913ba7ceb835c8ba973d8995f198683611 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Fri, 26 Jan 2024 11:14:36 +0100
Subject: [PATCH 09/22] extract custom silver behavior

---
 .../scala/viper/silver/ast/Expression.scala   |  1 -
 .../viper/silver/frontend/SilFrontend.scala   |  3 +--
 .../viper/silver/parser/FastParser.scala      | 26 +------------------
 .../scala/viper/silver/parser/Resolver.scala  | 19 +-------------
 .../viper/silver/parser/Translator.scala      | 15 +++++------
 5 files changed, 10 insertions(+), 54 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 2f6ec6526..b112888cf 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -16,7 +16,6 @@ import viper.silver.verifier.{ConsistencyError, VerificationResult}
 
 /** Expressions. */
 sealed trait Exp extends Hashable with Typed with Positioned with Infoed with TransformableErrors with PrettyExpression {
-
   lazy val isPure = Expressions.isPure(this)
   def isHeapDependent(p: Program) = Expressions.isHeapDependent(this, p)
   def isTopLevelHeapDependent(p: Program) = Expressions.isTopLevelHeapDependent(this, p)
diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index 0fa81c47a..c8ee02140 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala
@@ -252,8 +252,7 @@ trait SilFrontend extends DefaultFrontend {
 
     if (state == DefaultStates.ConsistencyCheck && _errors.isEmpty) {
       filter(_program.get) match {
-        case Succ(program) =>
-          _program = Some(program)
+        case Succ(program) => _program = Some(program)
         case Fail(errors) => _errors ++= errors
       }
     }
diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index b7b487863..40d4eaeb8 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -382,8 +382,6 @@ class FastParser {
   // Actual Parser starts from here
   def identContinues[$: P] = CharIn("0-9", "A-Z", "a-z", "$_")
 
-  def versionStarts[$: P] = CharIn("@")
-
   def keyword[$: P](check: String) = check ~~ !identContinues
 
   def parens[$: P, T](p: => P[T]) = "(" ~ p ~ ")"
@@ -401,9 +399,7 @@ class FastParser {
 
   // Note that `typedfuncApp` is before `"(" ~ exp ~ ")"` to ensure that the latter doesn't gobble up the brackets for the former
   // and then look like an `funcApp` up untill the `: type` part, after which we need to backtrack all the way back (or error if cut)
-  def atom(implicit ctx : P[_]) : P[PExp] = P(ParserExtension.newExpAtStart(ctx) | versionedidnuse
-    | debugOld
-    | annotatedAtom
+  def atom(implicit ctx : P[_]) : P[PExp] = P(ParserExtension.newExpAtStart(ctx) | annotatedAtom
     | integer | booltrue | boolfalse | nul | old
     | result | unExp | typedFuncApp
     | "(" ~ exp ~ ")" | accessPred | inhaleExhale | perm | let | quant | forperm | unfolding | applying
@@ -436,32 +432,12 @@ class FastParser {
 
   def identifier[$: P]: P[Unit] = CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_").repX
 
-  def versionedIdentifier[$: P]: P[Unit] = CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_").repX ~~ CharIn("@") ~~ CharIn("0-9") ~~ CharIn("0-9").repX
-
   def annotationIdentifier[$: P]: P[String] = (CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_.").repX).!
 
   def ident[$: P]: P[String] = identifier.!.filter(a => !keywords.contains(a)).opaque("identifier")
 
-  def versionedIdent[$: P]: P[String] = versionedIdentifier.!.opaque("versionedIdentifier")
-
   def idnuse[$: P]: P[PIdnUse] = FP(ident).map { case (pos, id) => PIdnUse(id)(pos) }
 
-  def versionedidnuse[$: P]: P[PVersionedIdnUse] = FP(versionedIdent).map { case (pos, id) => {
-    val parts = id.split("@")
-    PVersionedIdnUse(name=parts(0), version=parts(1))(pos)
-  } }
-
-  def debugOldLabel[$: P]: P[String] = (StringIn("line") ~~ CharIn("@") ~~ CharIn("0-9", "A-Z", "a-z", "$_.").repX).!.opaque("debugOldLabel")
-
-  def debugOldLabelUse[$: P]: P[PVersionedIdnUse] = FP(debugOldLabel).map { case (pos, id) => {
-    val parts = id.split("@")
-    PVersionedIdnUse(name = parts(0), version = parts(1))(pos)
-  }
-  }
-
-  def debugOld[$: P]: P[PExp] = P(StringIn("old") ~ FP("[" ~ debugOldLabelUse ~ "]" ~ parens(exp)).map {
-    case (pos, (a, b)) => PDebugLabelledOld(a, b)(pos)})
-
   def oldLabel[$: P]: P[PIdnUse] = idnuse | FP(LabelledOld.LhsOldLabel.!).map {
     case (pos, lhsOldLabel) => PIdnUse(lhsOldLabel)(pos)
   }
diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
index df696ddf3..b39d8feb4 100644
--- a/src/main/scala/viper/silver/parser/Resolver.scala
+++ b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -40,7 +40,6 @@ case class TypeChecker(names: NameAnalyser) {
   var curMember: PScope = null
   var curFunction: PFunction = null
   var resultAllowed: Boolean = false
-  var debugVariableTypes: Map[String, PType] = Map.empty
 
   /** to record error messages */
   var messages: FastMessaging.Messages = Nil
@@ -361,19 +360,6 @@ case class TypeChecker(names: NameAnalyser) {
     }
   }
 
-  def acceptAndCheckTypedEntityWithVersion[T1: ClassTag, T2: ClassTag]
-  (idnUses: Seq[PVersionedIdnUse], errorMessage: => String): Unit = {
-
-    idnUses.foreach { use =>
-      val decl1 = debugVariableTypes.get(use.versionedName)
-
-      decl1 match {
-        case Some(value) => use.typ = value
-        case None => messages ++= FastMessaging.message(use, errorMessage)
-      }
-    }
-  }
-
   def check(typ: PType): Unit = {
     typ match {
       case _: PPredicateType | _: PWandType =>
@@ -739,9 +725,6 @@ case class TypeChecker(names: NameAnalyser) {
       case piu: PIdnUse =>
         acceptAndCheckTypedEntity[PAnyVarDecl, Nothing](Seq(piu), "expected variable identifier")
 
-      case pviu: PVersionedIdnUse =>
-        acceptAndCheckTypedEntityWithVersion[PAnyVarDecl, Nothing](Seq(pviu), "expected variable identifier with version")
-
       case pl@PLet(e, ns) =>
         val oldCurMember = curMember
         curMember = ns
@@ -925,7 +908,7 @@ case class NameAnalyser() {
                 }
               case _ =>
             }
-          case i@PVersionedIdnUse(name, _, _) =>
+          case i@PVersionedIdnUse(name, _, _) => // TODO ake: maybe extract to DebugTypechecker
             // look up in both maps (if we are not in a method currently, we look in the same map twice, but that is ok)
             getCurrentMap.getOrElse(name, globalDeclarationMap.getOrElse(name, PUnknownEntity())) match {
               case PUnknownEntity() =>
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index f49d54e03..51bd0f708 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -11,7 +11,9 @@ import viper.silver.ast.utility._
 import viper.silver.ast.{SourcePosition, _}
 import viper.silver.plugin.standard.adt.{Adt, AdtType}
 
+import scala.collection.mutable
 import scala.language.implicitConversions
+import scala.reflect.internal.util.NoPosition.Pos
 
 /**
  * Takes an abstract syntax tree after parsing is done and translates it into
@@ -128,7 +130,7 @@ case class Translator(program: PProgram) {
 
   private def translate(f: PFieldDecl) = findField(f.idndef)
 
-  private val members = collection.mutable.HashMap[String, Node]()
+  protected val members: mutable.Map[String, Node] = collection.mutable.HashMap[String, Node]()
   def getMembers() = members
   /**
     * Translate the signature of a member, so that it can be looked up later.
@@ -362,6 +364,10 @@ case class Translator(program: PProgram) {
     val (pexp, annotationMap) = extractAnnotation(parseExp)
     val sourcePNodeInfo = SourcePNodeInfo(parseExp)
     val info = if (annotationMap.isEmpty) sourcePNodeInfo else ConsInfo(sourcePNodeInfo, AnnotationInfo(annotationMap))
+    expInternal(pexp, pos, info)
+  }
+
+  protected def expInternal(pexp: PExp, pos: PExp, info: Info): Exp = {
     pexp match {
       case piu @ PIdnUse(name) =>
         piu.decl match {
@@ -370,11 +376,6 @@ case class Translator(program: PProgram) {
           // Should have been caught by the type checker.
           case _ => sys.error("should not occur in type-checked program")
         }
-      case pviu@PVersionedIdnUse(_, _, _) =>
-        pexp.typ match {
-          case null => sys.error("should not occur in type-checked program")
-          case _ => LocalVarWithVersion(pviu.versionedName, ttyp(pexp.typ))(pos, info)
-        }
       case pbe @ PBinExp(left, op, right) =>
         val (l, r) = (exp(left), exp(right))
         op match {
@@ -569,8 +570,6 @@ case class Translator(program: PProgram) {
         Old(exp(e))(pos, info)
       case PLabelledOld(lbl,e) =>
         LabelledOld(exp(e),lbl.name)(pos, info)
-      case PDebugLabelledOld(lbl, e) =>
-        DebugLabelledOld(exp(e), lbl.versionedName)(pos, info)
       case PCondExp(cond, thn, els) =>
         CondExp(exp(cond), exp(thn), exp(els))(pos, info)
       case PCurPerm(res) =>

From c2c46eedf29c43b3a6de8ba10a4bfc0e4ab734ac Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Sat, 27 Jan 2024 11:33:09 +0100
Subject: [PATCH 10/22] extract PType from SourcePInfo

---
 .../scala/viper/silver/cfg/silver/CfgGenerator.scala |  2 +-
 src/main/scala/viper/silver/parser/Translator.scala  | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala
index 67da54492..b1317b07c 100644
--- a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala
+++ b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala
@@ -201,7 +201,7 @@ object CfgGenerator {
       case Seqn(ss, scopedDecls) =>
         val locals = scopedDecls.collect { case l: LocalVarDecl => l }
         for (local <- locals) {
-          val decl = LocalVarDeclStmt(local)(pos = local.pos)
+          val decl = LocalVarDeclStmt(local)(pos = local.pos, info = local.info)
           addStatement(WrappedStmt(decl))
         }
         ss.foreach(run)
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 51bd0f708..128cca52c 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -205,9 +205,9 @@ case class Translator(program: PProgram) {
         }
         methodCallAssign(s, Seq(target), lv => NewStmt(lv.head, fields)(pos, info))
       case PAssign(Seq(idnuse: PIdnUse), rhs) =>
-        LocalVarAssign(LocalVar(idnuse.name, ttyp(idnuse.typ))(pos, subInfo), exp(rhs))(pos, info)
+        LocalVarAssign(LocalVar(idnuse.name, ttyp(idnuse.typ))(pos, ConsInfo(SourcePNodeInfo(idnuse), subInfo)), exp(rhs))(pos, info)
       case PAssign(Seq(field: PFieldAccess), rhs) =>
-        FieldAssign(FieldAccess(exp(field.rcv), findField(field.idnuse))(field), exp(rhs))(pos, info)
+        FieldAssign(FieldAccess(exp(field.rcv), findField(field.idnuse))(field, SourcePNodeInfo(field)), exp(rhs))(pos, info)
       case lv@PVars(vars, init) =>
         // there are no declarations in the Viper AST; rather they are part of the scope signature
         init match {
@@ -222,7 +222,7 @@ case class Translator(program: PProgram) {
           case _ => None
         }
         val locals = plocals.flatten.map {
-          case p@PVars(vars, _) => vars.map(v => LocalVarDecl(v.idndef.name, ttyp(v.typ))(p))
+          case p@PVars(vars, _) => vars.map(v => LocalVarDecl(v.idndef.name, ttyp(v.typ))(pos = p, info = SourcePNodeInfo(v)))
         }.flatten
         Seqn(ss filterNot (_.isInstanceOf[PSkip]) map stmt, locals)(pos, info)
       case PFold(e) =>
@@ -682,15 +682,15 @@ case class Translator(program: PProgram) {
 
   /** Takes a `PFormalArgDecl` and turns it into a `LocalVarDecl`. */
   def liftArgDecl(formal: PFormalArgDecl) =
-      LocalVarDecl(formal.idndef.name, ttyp(formal.typ))(formal.idndef)
+      LocalVarDecl(formal.idndef.name, ttyp(formal.typ))(pos = formal.idndef, info = SourcePNodeInfo(formal))
 
   /** Takes a `PFormalReturnDecl` and turns it into a `LocalVarDecl`. */
   def liftReturnDecl(formal: PFormalReturnDecl) =
-      LocalVarDecl(formal.idndef.name, ttyp(formal.typ))(formal.idndef)
+      LocalVarDecl(formal.idndef.name, ttyp(formal.typ))(pos = formal.idndef, info = SourcePNodeInfo(formal))
 
   /** Takes a `PLogicalVarDecl` and turns it into a `LocalVarDecl`. */
   def liftLogicalDecl(logical: PLogicalVarDecl) =
-      LocalVarDecl(logical.idndef.name, ttyp(logical.typ))(logical.idndef)
+      LocalVarDecl(logical.idndef.name, ttyp(logical.typ))(pos = logical.idndef, info = SourcePNodeInfo(logical))
 
   /** Takes a `PType` and turns it into a `Type`. */
   def ttyp(t: PType): Type = t match {

From eb9f47ceba953918404cfb951774a64d7154e2fc Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Sun, 4 Feb 2024 08:56:08 +0100
Subject: [PATCH 11/22] fix quantifiers in debug mode

---
 src/main/scala/viper/silver/parser/Resolver.scala | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
index b39d8feb4..7efcb64d2 100644
--- a/src/main/scala/viper/silver/parser/Resolver.scala
+++ b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -855,8 +855,8 @@ case class NameAnalyser() {
     }
   }
 
-  private def check(n: PNode, target: Option[PNode]): Unit = {
-    var curMember: PScope = null
+  def check(n: PNode, target: Option[PNode], initialCurMember: PScope = null): Unit = {
+    var curMember: PScope = initialCurMember
 
     def getMap(d: PNode): mutable.HashMap[String, PDeclaration] =
       d match {

From c806fb6668fc8f66fba89483ef3925e12af1a797 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Sun, 18 Feb 2024 12:58:25 +0100
Subject: [PATCH 12/22] cleanup

---
 src/main/scala/viper/silver/parser/Resolver.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
index 7efcb64d2..69e6d37a7 100644
--- a/src/main/scala/viper/silver/parser/Resolver.scala
+++ b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -908,7 +908,7 @@ case class NameAnalyser() {
                 }
               case _ =>
             }
-          case i@PVersionedIdnUse(name, _, _) => // TODO ake: maybe extract to DebugTypechecker
+          case i@PVersionedIdnUse(name, _, _) =>
             // look up in both maps (if we are not in a method currently, we look in the same map twice, but that is ok)
             getCurrentMap.getOrElse(name, globalDeclarationMap.getOrElse(name, PUnknownEntity())) match {
               case PUnknownEntity() =>

From 83b680c164869802718f3105c53b10c24d10122d Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Mon, 19 Feb 2024 19:41:33 +0100
Subject: [PATCH 13/22] add exp to Store

---
 src/main/scala/viper/silver/ast/Expression.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index b112888cf..8b74fa66b 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -126,7 +126,7 @@ case class MagicWand(left: Exp, right: Exp)(val pos: Position = NoPosition, val
   override val typ: Wand.type = Wand
 
   //maybe rename this sometime
-  def subexpressionsToEvaluate(p: Program): Seq[Exp] = {
+  def subexpressionsToEvaluate(p: Program): Seq[Exp] = { // TODO ake
     /* The code collects expressions that can/are to be evaluated in a fixed state, i.e.
      * a state that is known when this method is called.
      * Among other things, such expressions may not be heap-dependent (unless they are nested

From 1d7820fae5abc1d4f56ab702e91660f0b1ad4871 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Wed, 21 Feb 2024 10:01:37 +0100
Subject: [PATCH 14/22] cleanup

---
 src/main/scala/viper/silver/ast/Expression.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 8b74fa66b..b112888cf 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -126,7 +126,7 @@ case class MagicWand(left: Exp, right: Exp)(val pos: Position = NoPosition, val
   override val typ: Wand.type = Wand
 
   //maybe rename this sometime
-  def subexpressionsToEvaluate(p: Program): Seq[Exp] = { // TODO ake
+  def subexpressionsToEvaluate(p: Program): Seq[Exp] = {
     /* The code collects expressions that can/are to be evaluated in a fixed state, i.e.
      * a state that is known when this method is called.
      * Among other things, such expressions may not be heap-dependent (unless they are nested

From d7db0807770af7168c574690f15c603d2d34a36b Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 16 Aug 2024 12:09:04 +0200
Subject: [PATCH 15/22] Fixed signature

---
 src/main/scala/viper/silver/parser/Resolver.scala | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
index efb4f8bce..7aebc7035 100644
--- a/src/main/scala/viper/silver/parser/Resolver.scala
+++ b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -973,8 +973,8 @@ case class NameAnalyser() {
 
   private val namesInScope = mutable.Set.empty[String]
 
-  private def check(g: PNode, target: Option[PNode]): Unit = {
-    var curScope: PScope = null
+  def check(g: PNode, target: Option[PNode], initialCurScope: PScope = null): Unit = {
+    var curScope: PScope = initialCurScope
     def getMap(): DeclarationMap = Option(curScope).map(_.scopeId).map(localDeclarationMaps.get(_).get).getOrElse(globalDeclarationMap)
 
     val scopeStack = mutable.Stack[PScope]()

From 931c90aa063ac5cdd43d141b4c482144dab24e18 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 20 Aug 2024 23:15:24 +0200
Subject: [PATCH 16/22] Simplifier improvements, fixed name resolving in
 debugger context

---
 .../ast/utility/ImpureAssumeRewriter.scala    |   2 +-
 .../viper/silver/ast/utility/Simplifier.scala | 102 ++++++++++++++++--
 .../scala/viper/silver/parser/Resolver.scala  |  15 +++
 3 files changed, 107 insertions(+), 12 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala b/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala
index 39381eb8b..e3587c590 100644
--- a/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala
+++ b/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala
@@ -127,7 +127,7 @@ object ImpureAssumeRewriter {
     val conds: Seq[Exp] =
       contextWithoutRcv
         .map(c => c._1._1.replace((c._1._2 zip rcv).toMap[Exp, Exp]))
-        .map(viper.silver.ast.utility.Simplifier.simplify)
+        .map(e => viper.silver.ast.utility.Simplifier.simplify(e))
 
     if (context.isEmpty) {
       assert(conds.isEmpty)
diff --git a/src/main/scala/viper/silver/ast/utility/Simplifier.scala b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
index ae228435e..cfe011dbe 100644
--- a/src/main/scala/viper/silver/ast/utility/Simplifier.scala
+++ b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
@@ -21,13 +21,19 @@ object Simplifier {
    * 0 are not treated. Note that an expression with non-terminating evaluation due to endless recursion
    * might be transformed to terminating expression.
    */
-  def simplify[N <: Node](n: N): N = {
+  def simplify[N <: Node](n: N, assumeWelldefinedness: Boolean = false): N = {
     /* Always simplify children first, then treat parent. */
     StrategyBuilder.Slim[Node]({
       // expression simplifications
       case root @ Not(BoolLit(literal)) =>
         BoolLit(!literal)(root.pos, root.info)
       case Not(Not(single)) => single
+      case root @ Not(EqCmp(a, b)) => NeCmp(a, b)(root.pos, root.info)
+      case root @ Not(NeCmp(a, b)) => EqCmp(a, b)(root.pos, root.info)
+      case root @ Not(GtCmp(a, b)) => LeCmp(a, b)(root.pos, root.info)
+      case root @ Not(GeCmp(a, b)) => LtCmp(a, b)(root.pos, root.info)
+      case root @ Not(LtCmp(a, b)) => GeCmp(a, b)(root.pos, root.info)
+      case root @ Not(LeCmp(a, b)) => GtCmp(a, b)(root.pos, root.info)
 
       case And(TrueLit(), right) => right
       case And(left, TrueLit()) => left
@@ -40,14 +46,13 @@ object Simplifier {
       case root @ Or(_, TrueLit()) => TrueLit()(root.pos, root.info)
 
       case root @ Implies(FalseLit(), _) => TrueLit()(root.pos, root.info)
-      case root @ Implies(_, TrueLit()) => TrueLit()(root.pos, root.info)
-      case root @ Implies(TrueLit(), FalseLit()) =>
-        FalseLit()(root.pos, root.info)
+      case Implies(_, tl @ TrueLit()) if assumeWelldefinedness => tl
       case Implies(TrueLit(), consequent) => consequent
+      case root @ Implies(FalseLit(), _) => TrueLit()(root.pos, root.info)
+      case root @ Implies(l1, Implies(l2, r)) => Implies(And(l1, l2)(), r)(root.pos, root.info)
 
-      // ME: Disabled since it is not equivalent in case the expression is not well-defined.
       // TODO: Consider checking if Expressions.proofObligations(left) is empty (requires adding the program as parameter).
-      // case root @ EqCmp(left, right) if left == right => TrueLit()(root.pos, root.info)
+      case root @ EqCmp(left, right) if assumeWelldefinedness && left == right => TrueLit()(root.pos, root.info)
       case root @ EqCmp(BoolLit(left), BoolLit(right)) =>
         BoolLit(left == right)(root.pos, root.info)
       case root @ EqCmp(FalseLit(), right) => Not(right)(root.pos, root.info)
@@ -68,20 +73,19 @@ object Simplifier {
         BoolLit(left != right)(root.pos, root.info)
       case root @ NeCmp(NullLit(), NullLit()) =>
         FalseLit()(root.pos, root.info)
+      case root @ NeCmp(left, right) if assumeWelldefinedness && left == right => FalseLit()(root.pos, root.info)
 
       case CondExp(TrueLit(), ifTrue, _) => ifTrue
       case CondExp(FalseLit(), _, ifFalse) => ifFalse
-      case root @ CondExp(_, FalseLit(), FalseLit()) =>
-        FalseLit()(root.pos, root.info)
-      case root @ CondExp(_, TrueLit(), TrueLit()) =>
-        TrueLit()(root.pos, root.info)
+      case CondExp(_, ifTrue, ifFalse) if assumeWelldefinedness && ifTrue == ifFalse =>
+        ifTrue
       case root @ CondExp(condition, FalseLit(), TrueLit()) =>
         Not(condition)(root.pos, root.info)
       case CondExp(condition, TrueLit(), FalseLit()) => condition
       case root @ CondExp(condition, FalseLit(), ifFalse) =>
         And(Not(condition)(), ifFalse)(root.pos, root.info)
       case root @ CondExp(condition, TrueLit(), ifFalse) =>
-        if(ifFalse.isPure) {
+        if (ifFalse.isPure) {
           Or(condition, ifFalse)(root.pos, root.info)
         } else {
           Implies(Not(condition)(), ifFalse)(root.pos, root.info)
@@ -100,6 +104,24 @@ object Simplifier {
       case Minus(Minus(single)) => single
 
       case PermMinus(PermMinus(single)) => single
+      case PermMul(fst, FullPerm()) => fst
+      case PermMul(FullPerm(), snd) => snd
+      case PermMul(_, np @ NoPerm()) if assumeWelldefinedness => np
+      case PermMul(np @ NoPerm(), _) if assumeWelldefinedness => np
+
+      case root @ PermGeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info)
+      case root @ PermLeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info)
+      case root @ PermGtCmp(a, b) if assumeWelldefinedness && a == b => FalseLit()(root.pos, root.info)
+      case root @ PermLtCmp(a, b) if assumeWelldefinedness && a == b => FalseLit()(root.pos, root.info)
+
+      case root @ PermGtCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) > Rational(c, d))(root.pos, root.info)
+      case root @ PermGeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) >= Rational(c, d))(root.pos, root.info)
+      case root @ PermLtCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) < Rational(c, d))(root.pos, root.info)
+      case root @ PermLeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) <= Rational(c, d))(root.pos, root.info)
 
       case root @ GeCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left >= right)(root.pos, root.info)
@@ -138,4 +160,62 @@ object Simplifier {
   }
 
   private val bigIntZero = BigInt(0)
+  private val bigIntOne = BigInt(1)
+
+  object AnyPermLiteral {
+    def unapply(p: Exp): Option[(BigInt, BigInt)] = p match {
+      case FullPerm() => Some((bigIntOne, bigIntOne))
+      case NoPerm() => Some((bigIntZero, bigIntOne))
+      case FractionalPerm(IntLit(n), IntLit(d)) => Some((n, d))
+      case _ => None
+    }
+  }
+
+  final class Rational(n: BigInt, d: BigInt) extends Ordered[Rational] {
+    require(d != 0, "Denominator of Rational must not be 0.")
+
+    private val g = n.gcd(d)
+    val numerator: BigInt = n / g * d.signum
+    val denominator: BigInt = d.abs / g
+
+    def +(that: Rational): Rational = {
+      val newNum = this.numerator * that.denominator + that.numerator * this.denominator
+      val newDen = this.denominator * that.denominator
+      Rational(newNum, newDen)
+    }
+
+    def -(that: Rational): Rational = this + (-that)
+
+    def unary_- = Rational(-numerator, denominator)
+
+    def abs = Rational(numerator.abs, denominator)
+
+    def signum = Rational(numerator.signum, 1)
+
+    def *(that: Rational): Rational = Rational(this.numerator * that.numerator, this.denominator * that.denominator)
+
+    def /(that: Rational): Rational = this * that.inverse
+
+    def inverse = Rational(denominator, numerator)
+
+    def compare(that: Rational) = (this.numerator * that.denominator - that.numerator * this.denominator).signum
+
+    override def equals(obj: Any) = obj match {
+      case that: Rational => this.numerator == that.numerator && this.denominator == that.denominator
+      case _ => false
+    }
+
+    override def hashCode(): Int = viper.silver.utility.Common.generateHashCode(n, d)
+
+    override lazy val toString = s"$numerator/$denominator"
+  }
+
+  object Rational extends ((BigInt, BigInt) => Rational) {
+    val zero = Rational(0, 1)
+    val one = Rational(1, 1)
+
+    def apply(numer: BigInt, denom: BigInt) = new Rational(numer, denom)
+
+    def unapply(r: Rational) = Some(r.numerator, r.denominator)
+  }
 }
diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
index 7aebc7035..66c977e70 100644
--- a/src/main/scala/viper/silver/parser/Resolver.scala
+++ b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -1055,6 +1055,21 @@ case class NameAnalyser() {
 
     // find all declarations
     g.visit(nodeDownNameCollectorVisitor, nodeUpNameCollectorVisitor)
+
+    if (initialCurScope != null) {
+      assert(initialCurScope == curScope)
+
+      while (curScope != null) {
+        val popMap = localDeclarationMaps.get(curScope.scopeId).get
+        curScope.getAncestor[PScope] match {
+          case Some(newScope) =>
+            curScope = newScope
+          case None =>
+            curScope = null
+        }
+        getMap().merge(popMap)
+      }
+    }
   }
 
   def run(p: PProgram): Boolean = {

From 54bbafb3365a9cbeaff0a3892945ad8a31898633 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 22 Aug 2024 15:52:19 +0200
Subject: [PATCH 17/22] Fixing type checking debug old, better simplification,
 adding min expression

---
 src/main/scala/viper/silver/ast/Expression.scala     |  1 +
 src/main/scala/viper/silver/ast/Program.scala        |  1 +
 .../viper/silver/ast/pretty/PrettyPrinter.scala      |  1 +
 .../scala/viper/silver/ast/utility/Simplifier.scala  | 12 ++++++++++++
 src/main/scala/viper/silver/parser/ParseAst.scala    |  8 +++++---
 5 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index b112888cf..45b5089cb 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -360,6 +360,7 @@ case class PermAdd(left: Exp, right: Exp)(val pos: Position = NoPosition, val in
 case class PermSub(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(PermSubOp) with PermExp with ForbiddenInTrigger
 case class PermMul(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(PermMulOp) with PermExp with ForbiddenInTrigger
 case class IntPermMul(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(IntPermMulOp) with PermExp with ForbiddenInTrigger
+case class DebugPermMin(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(DebugPermMinOp) with PermExp with ForbiddenInTrigger
 
 // Comparison expressions
 case class PermLtCmp(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(PermLtOp) with ForbiddenInTrigger
diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala
index b46953b99..1ea501bef 100644
--- a/src/main/scala/viper/silver/ast/Program.scala
+++ b/src/main/scala/viper/silver/ast/Program.scala
@@ -729,6 +729,7 @@ case object ModOp extends ProdOp("%") with IntBinOp with IntDomainFunc
 case object PermAddOp extends SumOp("+") with PermBinOp with PermDomainFunc
 case object PermSubOp extends SumOp("-") with PermBinOp with PermDomainFunc
 case object PermMulOp extends ProdOp("*") with PermBinOp with PermDomainFunc
+case object DebugPermMinOp extends SumOp("min") with PermBinOp with PermDomainFunc
 case object IntPermMulOp extends ProdOp("*") with BinOp with PermDomainFunc {
   lazy val leftTyp = Int
   lazy val rightTyp = Perm
diff --git a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
index 99522e710..2003fd387 100644
--- a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
+++ b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
@@ -893,6 +893,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
 
       case null => uninitialized
       case u: PrettyUnaryExpression => showPrettyUnaryExp(u)
+      case DebugPermMin(e0, e1) => text("min") <> parens(show(e0) <> "," <+> show(e1))
       case b: PrettyBinaryExpression => showPrettyBinaryExp(b)
       case e: ExtensionExp => e.prettyPrint
       case _ => sys.error(s"unknown expression: ${e.getClass}")
diff --git a/src/main/scala/viper/silver/ast/utility/Simplifier.scala b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
index cfe011dbe..bee6565e2 100644
--- a/src/main/scala/viper/silver/ast/utility/Simplifier.scala
+++ b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
@@ -122,6 +122,18 @@ object Simplifier {
         BoolLit(Rational(a, b) < Rational(c, d))(root.pos, root.info)
       case root @ PermLeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
         BoolLit(Rational(a, b) <= Rational(c, d))(root.pos, root.info)
+      case DebugPermMin(e0@AnyPermLiteral(a, b), e1@AnyPermLiteral(c, d)) =>
+        if (Rational(a, b) < Rational(c, d)) {
+          e0
+        } else {
+          e1
+        }
+      case root @ PermSub(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        val diff = Rational(a, b) - Rational(c, d)
+        FractionalPerm(IntLit(diff.numerator)(root.pos, root.info), IntLit(diff.denominator)(root.pos, root.info))(root.pos, root.info)
+      case root @ PermAdd(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        val sum = Rational(a, b) + Rational(c, d)
+        FractionalPerm(IntLit(sum.numerator)(root.pos, root.info), IntLit(sum.denominator)(root.pos, root.info))(root.pos, root.info)
 
       case root @ GeCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left >= right)(root.pos, root.info)
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
index 7b8741d42..4e59f54c4 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -1208,10 +1208,12 @@ case class POldExp(op: PKwOp.Old, label: Option[PGrouped[PSym.Bracket, Either[PK
   override val signatures: List[PTypeSubstitution] = List(Map(POpApp.pResS -> POpApp.pArg(0)))
 }
 
-case class PDebugLabelledOldExp(op: PKwOp.Old, label: PVersionedIdnUseExp, e: PExp)(val pos: (Position, Position)) extends PExp {
-  override def typeSubstitutions = e.typeSubstitutions
+case class PDebugLabelledOldExp(op: PKwOp.Old, label: PVersionedIdnUseExp, e: PExp)(val pos: (Position, Position)) extends PCallKeyword with PHeapOpApp {
+  override val args = Seq(e)
 
-  override def forceSubstitution(ts: PTypeSubstitution): Unit = e.forceSubstitution(ts)
+  override def requirePure = args
+
+  override val signatures: List[PTypeSubstitution] = List(Map(POpApp.pResS -> POpApp.pArg(0)))
 }
 
 sealed trait PCollectionLiteral extends PCallKeyword {

From a2b79aeab1343482eca8fde31fbab6c6e8854fbf Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 28 Aug 2024 01:06:58 +0200
Subject: [PATCH 18/22] Moving Rational class to utility package

---
 .../viper/silver/ast/utility/Simplifier.scala | 49 +------------------
 .../scala/viper/silver/utility/Common.scala   | 48 ++++++++++++++++++
 2 files changed, 49 insertions(+), 48 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/Simplifier.scala b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
index bee6565e2..6af22b324 100644
--- a/src/main/scala/viper/silver/ast/utility/Simplifier.scala
+++ b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
@@ -9,6 +9,7 @@ package viper.silver.ast.utility
 import viper.silver.ast.utility.Statements.EmptyStmt
 import viper.silver.ast._
 import viper.silver.ast.utility.rewriter._
+import viper.silver.utility.Common.Rational
 
 /**
  * An implementation for simplifications on the Viper AST.
@@ -182,52 +183,4 @@ object Simplifier {
       case _ => None
     }
   }
-
-  final class Rational(n: BigInt, d: BigInt) extends Ordered[Rational] {
-    require(d != 0, "Denominator of Rational must not be 0.")
-
-    private val g = n.gcd(d)
-    val numerator: BigInt = n / g * d.signum
-    val denominator: BigInt = d.abs / g
-
-    def +(that: Rational): Rational = {
-      val newNum = this.numerator * that.denominator + that.numerator * this.denominator
-      val newDen = this.denominator * that.denominator
-      Rational(newNum, newDen)
-    }
-
-    def -(that: Rational): Rational = this + (-that)
-
-    def unary_- = Rational(-numerator, denominator)
-
-    def abs = Rational(numerator.abs, denominator)
-
-    def signum = Rational(numerator.signum, 1)
-
-    def *(that: Rational): Rational = Rational(this.numerator * that.numerator, this.denominator * that.denominator)
-
-    def /(that: Rational): Rational = this * that.inverse
-
-    def inverse = Rational(denominator, numerator)
-
-    def compare(that: Rational) = (this.numerator * that.denominator - that.numerator * this.denominator).signum
-
-    override def equals(obj: Any) = obj match {
-      case that: Rational => this.numerator == that.numerator && this.denominator == that.denominator
-      case _ => false
-    }
-
-    override def hashCode(): Int = viper.silver.utility.Common.generateHashCode(n, d)
-
-    override lazy val toString = s"$numerator/$denominator"
-  }
-
-  object Rational extends ((BigInt, BigInt) => Rational) {
-    val zero = Rational(0, 1)
-    val one = Rational(1, 1)
-
-    def apply(numer: BigInt, denom: BigInt) = new Rational(numer, denom)
-
-    def unapply(r: Rational) = Some(r.numerator, r.denominator)
-  }
 }
diff --git a/src/main/scala/viper/silver/utility/Common.scala b/src/main/scala/viper/silver/utility/Common.scala
index 3d2c9cafd..0a2abf4fd 100644
--- a/src/main/scala/viper/silver/utility/Common.scala
+++ b/src/main/scala/viper/silver/utility/Common.scala
@@ -76,4 +76,52 @@ object Common {
 
     new JPrintWriter(new JBufferedWriter(new JFileWriter(file, append)), autoFlush)
   }
+
+  final class Rational(n: BigInt, d: BigInt) extends Ordered[Rational] {
+    require(d != 0, "Denominator of Rational must not be 0.")
+
+    private val g = n.gcd(d)
+    val numerator: BigInt = n / g * d.signum
+    val denominator: BigInt = d.abs / g
+
+    def +(that: Rational): Rational = {
+      val newNum = this.numerator * that.denominator + that.numerator * this.denominator
+      val newDen = this.denominator * that.denominator
+      Rational(newNum, newDen)
+    }
+
+    def -(that: Rational): Rational = this + (-that)
+
+    def unary_- = Rational(-numerator, denominator)
+
+    def abs = Rational(numerator.abs, denominator)
+
+    def signum = Rational(numerator.signum, 1)
+
+    def *(that: Rational): Rational = Rational(this.numerator * that.numerator, this.denominator * that.denominator)
+
+    def /(that: Rational): Rational = this * that.inverse
+
+    def inverse = Rational(denominator, numerator)
+
+    def compare(that: Rational) = (this.numerator * that.denominator - that.numerator * this.denominator).signum
+
+    override def equals(obj: Any) = obj match {
+      case that: Rational => this.numerator == that.numerator && this.denominator == that.denominator
+      case _ => false
+    }
+
+    override def hashCode(): Int = viper.silver.utility.Common.generateHashCode(n, d)
+
+    override lazy val toString = s"$numerator/$denominator"
+  }
+
+  object Rational extends ((BigInt, BigInt) => Rational) {
+    val zero = Rational(0, 1)
+    val one = Rational(1, 1)
+
+    def apply(numer: BigInt, denom: BigInt) = new Rational(numer, denom)
+
+    def unapply(r: Rational) = Some(r.numerator, r.denominator)
+  }
 }

From 6326764a9e107cc23d7ac474f79519d120d54fc5 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 28 Aug 2024 02:41:23 +0200
Subject: [PATCH 19/22] Cleanup and some comments

---
 src/main/scala/viper/silver/ast/Expression.scala  | 7 ++++---
 src/main/scala/viper/silver/parser/Resolver.scala | 2 ++
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 45b5089cb..8a78dd149 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -11,7 +11,6 @@ import viper.silver.ast.pretty._
 import viper.silver.ast.utility._
 import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion
 import viper.silver.ast.utility.rewriter.{StrategyBuilder, Traverse}
-import viper.silver.parser.PExp
 import viper.silver.verifier.{ConsistencyError, VerificationResult}
 
 /** Expressions. */
@@ -360,6 +359,8 @@ case class PermAdd(left: Exp, right: Exp)(val pos: Position = NoPosition, val in
 case class PermSub(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(PermSubOp) with PermExp with ForbiddenInTrigger
 case class PermMul(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(PermMulOp) with PermExp with ForbiddenInTrigger
 case class IntPermMul(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(IntPermMulOp) with PermExp with ForbiddenInTrigger
+
+/** min expression used in the Silicon debugger */
 case class DebugPermMin(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(DebugPermMinOp) with PermExp with ForbiddenInTrigger
 
 // Comparison expressions
@@ -514,7 +515,7 @@ case class LabelledOld(exp: Exp, oldLabel: String)(val pos: Position = NoPositio
       Consistency.checkPure(exp)
 }
 
-/** Old expression that are used in the debugger. */
+/** Old expression that are used in the Silicon debugger. */
 case class DebugLabelledOld(exp: Exp, oldLabel: String)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends OldExp {
   override lazy val check : Seq[ConsistencyError] =
     Consistency.checkPure(exp)
@@ -721,7 +722,7 @@ case class Result(typ: Type)(val pos: Position = NoPosition, val info: Info = No
   lazy val name = "result"
 }
 
-/** A special local variable with a version for debugging */
+/** A special local variable with a version for Silicon debugging */
 case class LocalVarWithVersion(name: String, typ: Type)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AbstractLocalVar with Lhs {
   def nameWithoutVersion = name.substring(0, name.lastIndexOf("@"))
   override lazy val check: Seq[ConsistencyError] =
diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
index 66c977e70..4bc58e85a 100644
--- a/src/main/scala/viper/silver/parser/Resolver.scala
+++ b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -1056,6 +1056,8 @@ case class NameAnalyser() {
     // find all declarations
     g.visit(nodeDownNameCollectorVisitor, nodeUpNameCollectorVisitor)
 
+    // If we started from some inner scope, walk all the way back out to the whole program
+    // with a variation of nodeUpNameCollectorVisitor
     if (initialCurScope != null) {
       assert(initialCurScope == curScope)
 

From e0db674851819e23c7b8bc38bbe78bc7dae84053 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 29 Aug 2024 00:55:08 +0200
Subject: [PATCH 20/22] Caching simplification results

---
 .../scala/viper/silver/ast/Expression.scala   |   3 +-
 .../viper/silver/ast/utility/Simplifier.scala | 140 ++++++++++--------
 .../ast/utility/rewriter/Rewritable.scala     |   2 +-
 .../termination/TerminationASTExtension.scala |   2 +-
 4 files changed, 85 insertions(+), 62 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 8a78dd149..0d206d9ae 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -15,6 +15,7 @@ import viper.silver.verifier.{ConsistencyError, VerificationResult}
 
 /** Expressions. */
 sealed trait Exp extends Hashable with Typed with Positioned with Infoed with TransformableErrors with PrettyExpression {
+  var simplified: Option[Exp] = None
   lazy val isPure = Expressions.isPure(this)
   def isHeapDependent(p: Program) = Expressions.isHeapDependent(this, p)
   def isTopLevelHeapDependent(p: Program) = Expressions.isTopLevelHeapDependent(this, p)
@@ -47,7 +48,7 @@ sealed trait Exp extends Hashable with Typed with Positioned with Infoed with Tr
    */
  // lazy val proofObligations = Expressions.proofObligations(this)
 
-  override def toString() = {
+  override lazy val toString = {
    // Carbon relies on expression pretty-printing resulting in a string without line breaks,
    // so for the special case of directly converting an expression to a string, we remove all line breaks
    // the pretty printer might have inserted.
diff --git a/src/main/scala/viper/silver/ast/utility/Simplifier.scala b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
index 6af22b324..6730694e9 100644
--- a/src/main/scala/viper/silver/ast/utility/Simplifier.scala
+++ b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
@@ -23,105 +23,107 @@ object Simplifier {
    * might be transformed to terminating expression.
    */
   def simplify[N <: Node](n: N, assumeWelldefinedness: Boolean = false): N = {
-    /* Always simplify children first, then treat parent. */
-    StrategyBuilder.Slim[Node]({
+
+    val simplifySingle: PartialFunction[Node, Node] = {
       // expression simplifications
-      case root @ Not(BoolLit(literal)) =>
+      case root: Exp if root.simplified.isDefined =>
+        root.simplified.get
+      case root@Not(BoolLit(literal)) =>
         BoolLit(!literal)(root.pos, root.info)
       case Not(Not(single)) => single
-      case root @ Not(EqCmp(a, b)) => NeCmp(a, b)(root.pos, root.info)
-      case root @ Not(NeCmp(a, b)) => EqCmp(a, b)(root.pos, root.info)
-      case root @ Not(GtCmp(a, b)) => LeCmp(a, b)(root.pos, root.info)
-      case root @ Not(GeCmp(a, b)) => LtCmp(a, b)(root.pos, root.info)
-      case root @ Not(LtCmp(a, b)) => GeCmp(a, b)(root.pos, root.info)
-      case root @ Not(LeCmp(a, b)) => GtCmp(a, b)(root.pos, root.info)
+      case root@Not(EqCmp(a, b)) => NeCmp(a, b)(root.pos, root.info)
+      case root@Not(NeCmp(a, b)) => EqCmp(a, b)(root.pos, root.info)
+      case root@Not(GtCmp(a, b)) => LeCmp(a, b)(root.pos, root.info)
+      case root@Not(GeCmp(a, b)) => LtCmp(a, b)(root.pos, root.info)
+      case root@Not(LtCmp(a, b)) => GeCmp(a, b)(root.pos, root.info)
+      case root@Not(LeCmp(a, b)) => GtCmp(a, b)(root.pos, root.info)
 
       case And(TrueLit(), right) => right
       case And(left, TrueLit()) => left
-      case root @ And(FalseLit(), _) => FalseLit()(root.pos, root.info)
-      case root @ And(_, FalseLit()) => FalseLit()(root.pos, root.info)
+      case root@And(FalseLit(), _) => FalseLit()(root.pos, root.info)
+      case root@And(_, FalseLit()) => FalseLit()(root.pos, root.info)
 
       case Or(FalseLit(), right) => right
       case Or(left, FalseLit()) => left
-      case root @ Or(TrueLit(), _) => TrueLit()(root.pos, root.info)
-      case root @ Or(_, TrueLit()) => TrueLit()(root.pos, root.info)
+      case root@Or(TrueLit(), _) => TrueLit()(root.pos, root.info)
+      case root@Or(_, TrueLit()) => TrueLit()(root.pos, root.info)
 
-      case root @ Implies(FalseLit(), _) => TrueLit()(root.pos, root.info)
-      case Implies(_, tl @ TrueLit()) if assumeWelldefinedness => tl
+      case root@Implies(FalseLit(), _) => TrueLit()(root.pos, root.info)
+      case Implies(_, tl@TrueLit()) if assumeWelldefinedness => tl
       case Implies(TrueLit(), consequent) => consequent
-      case root @ Implies(FalseLit(), _) => TrueLit()(root.pos, root.info)
-      case root @ Implies(l1, Implies(l2, r)) => Implies(And(l1, l2)(), r)(root.pos, root.info)
+      case root@Implies(FalseLit(), _) => TrueLit()(root.pos, root.info)
+      case root@Implies(l1, Implies(l2, r)) => Implies(And(l1, l2)(), r)(root.pos, root.info)
 
       // TODO: Consider checking if Expressions.proofObligations(left) is empty (requires adding the program as parameter).
-      case root @ EqCmp(left, right) if assumeWelldefinedness && left == right => TrueLit()(root.pos, root.info)
-      case root @ EqCmp(BoolLit(left), BoolLit(right)) =>
+      case root@EqCmp(left, right) if assumeWelldefinedness && left == right => TrueLit()(root.pos, root.info)
+      case root@EqCmp(BoolLit(left), BoolLit(right)) =>
         BoolLit(left == right)(root.pos, root.info)
-      case root @ EqCmp(FalseLit(), right) => Not(right)(root.pos, root.info)
-      case root @ EqCmp(left, FalseLit()) => Not(left)(root.pos, root.info)
+      case root@EqCmp(FalseLit(), right) => Not(right)(root.pos, root.info)
+      case root@EqCmp(left, FalseLit()) => Not(left)(root.pos, root.info)
       case EqCmp(TrueLit(), right) => right
       case EqCmp(left, TrueLit()) => left
-      case root @ EqCmp(IntLit(left), IntLit(right)) =>
+      case root@EqCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left == right)(root.pos, root.info)
-      case root @ EqCmp(NullLit(), NullLit()) => TrueLit()(root.pos, root.info)
+      case root@EqCmp(NullLit(), NullLit()) => TrueLit()(root.pos, root.info)
 
-      case root @ NeCmp(BoolLit(left), BoolLit(right)) =>
+      case root@NeCmp(BoolLit(left), BoolLit(right)) =>
         BoolLit(left != right)(root.pos, root.info)
       case NeCmp(FalseLit(), right) => right
       case NeCmp(left, FalseLit()) => left
-      case root @ NeCmp(TrueLit(), right) => Not(right)(root.pos, root.info)
-      case root @ NeCmp(left, TrueLit()) => Not(left)(root.pos, root.info)
-      case root @ NeCmp(IntLit(left), IntLit(right)) =>
+      case root@NeCmp(TrueLit(), right) => Not(right)(root.pos, root.info)
+      case root@NeCmp(left, TrueLit()) => Not(left)(root.pos, root.info)
+      case root@NeCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left != right)(root.pos, root.info)
-      case root @ NeCmp(NullLit(), NullLit()) =>
+      case root@NeCmp(NullLit(), NullLit()) =>
         FalseLit()(root.pos, root.info)
-      case root @ NeCmp(left, right) if assumeWelldefinedness && left == right => FalseLit()(root.pos, root.info)
+      case root@NeCmp(left, right) if assumeWelldefinedness && left == right => FalseLit()(root.pos, root.info)
 
       case CondExp(TrueLit(), ifTrue, _) => ifTrue
       case CondExp(FalseLit(), _, ifFalse) => ifFalse
       case CondExp(_, ifTrue, ifFalse) if assumeWelldefinedness && ifTrue == ifFalse =>
         ifTrue
-      case root @ CondExp(condition, FalseLit(), TrueLit()) =>
+      case root@CondExp(condition, FalseLit(), TrueLit()) =>
         Not(condition)(root.pos, root.info)
       case CondExp(condition, TrueLit(), FalseLit()) => condition
-      case root @ CondExp(condition, FalseLit(), ifFalse) =>
+      case root@CondExp(condition, FalseLit(), ifFalse) =>
         And(Not(condition)(), ifFalse)(root.pos, root.info)
-      case root @ CondExp(condition, TrueLit(), ifFalse) =>
+      case root@CondExp(condition, TrueLit(), ifFalse) =>
         if (ifFalse.isPure) {
           Or(condition, ifFalse)(root.pos, root.info)
         } else {
           Implies(Not(condition)(), ifFalse)(root.pos, root.info)
         }
-      case root @ CondExp(condition, ifTrue, FalseLit()) =>
+      case root@CondExp(condition, ifTrue, FalseLit()) =>
         And(condition, ifTrue)(root.pos, root.info)
-      case root @ CondExp(condition, ifTrue, TrueLit()) =>
+      case root@CondExp(condition, ifTrue, TrueLit()) =>
         Implies(condition, ifTrue)(root.pos, root.info)
 
-      case root @ Forall(_, _, BoolLit(literal)) =>
+      case root@Forall(_, _, BoolLit(literal)) =>
         BoolLit(literal)(root.pos, root.info)
-      case root @ Exists(_, _, BoolLit(literal)) =>
+      case root@Exists(_, _, BoolLit(literal)) =>
         BoolLit(literal)(root.pos, root.info)
 
-      case root @ Minus(IntLit(literal)) => IntLit(-literal)(root.pos, root.info)
+      case root@Minus(IntLit(literal)) => IntLit(-literal)(root.pos, root.info)
       case Minus(Minus(single)) => single
 
       case PermMinus(PermMinus(single)) => single
       case PermMul(fst, FullPerm()) => fst
       case PermMul(FullPerm(), snd) => snd
-      case PermMul(_, np @ NoPerm()) if assumeWelldefinedness => np
-      case PermMul(np @ NoPerm(), _) if assumeWelldefinedness => np
+      case PermMul(_, np@NoPerm()) if assumeWelldefinedness => np
+      case PermMul(np@NoPerm(), _) if assumeWelldefinedness => np
 
-      case root @ PermGeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info)
-      case root @ PermLeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info)
-      case root @ PermGtCmp(a, b) if assumeWelldefinedness && a == b => FalseLit()(root.pos, root.info)
-      case root @ PermLtCmp(a, b) if assumeWelldefinedness && a == b => FalseLit()(root.pos, root.info)
+      case root@PermGeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info)
+      case root@PermLeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info)
+      case root@PermGtCmp(a, b) if assumeWelldefinedness && a == b => FalseLit()(root.pos, root.info)
+      case root@PermLtCmp(a, b) if assumeWelldefinedness && a == b => FalseLit()(root.pos, root.info)
 
-      case root @ PermGtCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+      case root@PermGtCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
         BoolLit(Rational(a, b) > Rational(c, d))(root.pos, root.info)
-      case root @ PermGeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+      case root@PermGeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
         BoolLit(Rational(a, b) >= Rational(c, d))(root.pos, root.info)
-      case root @ PermLtCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+      case root@PermLtCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
         BoolLit(Rational(a, b) < Rational(c, d))(root.pos, root.info)
-      case root @ PermLeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+      case root@PermLeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
         BoolLit(Rational(a, b) <= Rational(c, d))(root.pos, root.info)
       case DebugPermMin(e0@AnyPermLiteral(a, b), e1@AnyPermLiteral(c, d)) =>
         if (Rational(a, b) < Rational(c, d)) {
@@ -129,36 +131,36 @@ object Simplifier {
         } else {
           e1
         }
-      case root @ PermSub(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+      case root@PermSub(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
         val diff = Rational(a, b) - Rational(c, d)
         FractionalPerm(IntLit(diff.numerator)(root.pos, root.info), IntLit(diff.denominator)(root.pos, root.info))(root.pos, root.info)
-      case root @ PermAdd(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+      case root@PermAdd(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
         val sum = Rational(a, b) + Rational(c, d)
         FractionalPerm(IntLit(sum.numerator)(root.pos, root.info), IntLit(sum.denominator)(root.pos, root.info))(root.pos, root.info)
 
-      case root @ GeCmp(IntLit(left), IntLit(right)) =>
+      case root@GeCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left >= right)(root.pos, root.info)
-      case root @ GtCmp(IntLit(left), IntLit(right)) =>
+      case root@GtCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left > right)(root.pos, root.info)
-      case root @ LeCmp(IntLit(left), IntLit(right)) =>
+      case root@LeCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left <= right)(root.pos, root.info)
-      case root @ LtCmp(IntLit(left), IntLit(right)) =>
+      case root@LtCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left < right)(root.pos, root.info)
 
-      case root @ Add(IntLit(left), IntLit(right)) =>
+      case root@Add(IntLit(left), IntLit(right)) =>
         IntLit(left + right)(root.pos, root.info)
-      case root @ Sub(IntLit(left), IntLit(right)) =>
+      case root@Sub(IntLit(left), IntLit(right)) =>
         IntLit(left - right)(root.pos, root.info)
-      case root @ Mul(IntLit(left), IntLit(right)) =>
+      case root@Mul(IntLit(left), IntLit(right)) =>
         IntLit(left * right)(root.pos, root.info)
       /* In the general case, Viper uses the SMT division and modulo. Scala's division is not in-sync with SMT division.
          For nonnegative dividends and divisors, all used division and modulo definitions coincide. So, in order to not
          not make any assumptions on the SMT division, division and modulo are simplified only if the dividend and divisor
          are nonnegative. Also see Carbon PR #448.
        */
-      case root @ Div(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
+      case root@Div(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
         IntLit(left / right)(root.pos, root.info)
-      case root @ Mod(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
+      case root@Mod(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
         IntLit(left % right)(root.pos, root.info)
 
       // statement simplifications
@@ -169,7 +171,27 @@ object Simplifier {
       case If(_, EmptyStmt, EmptyStmt) => EmptyStmt // remove empty If clause
       case If(TrueLit(), thn, _) => thn // remove trivial If conditions
       case If(FalseLit(), _, els) => els // remove trivial If conditions
-    }, Traverse.BottomUp) execute n
+    }
+
+    val simplifyAndCache = new PartialFunction[Node, Node] {
+      def apply(n: Node): Node = {
+        val simplified = simplifySingle.applyOrElse(n, (nn: Node) => nn)
+        n match {
+          case e: Exp =>
+            e.simplified = Some(simplified.asInstanceOf[Exp])
+            simplified.asInstanceOf[Exp].simplified = Some(simplified.asInstanceOf[Exp])
+          case _ =>
+        }
+        simplified
+      }
+
+      def isDefinedAt(n: Node): Boolean = n.isInstanceOf[Exp] || simplifySingle.isDefinedAt(n)
+    }
+
+    /* Always simplify children first, then treat parent. */
+    StrategyBuilder.Slim[Node](simplifyAndCache, Traverse.BottomUp).recurseFunc({
+      case e: Exp if e.simplified.isDefined => Nil
+    }) execute n
   }
 
   private val bigIntZero = BigInt(0)
diff --git a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
index 78c250b9d..434c2ccf4 100644
--- a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
+++ b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
@@ -24,7 +24,7 @@ trait HasExtraVars {
   */
 trait Rewritable extends Product {
 
-  def children: Seq[Any] = productIterator.toList
+  lazy val children: Seq[Any] = productIterator.toSeq
 
   def withChildren(children: Seq[Any], pos: Option[(Position, Position)] = None, forceRewrite: Boolean = false): this.type = {
     if (!forceRewrite && this.children == children && !pos.isDefined)
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationASTExtension.scala
index 5801b95cf..2d9e1a4fa 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationASTExtension.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationASTExtension.scala
@@ -117,7 +117,7 @@ case class DecreasesSpecification(tuple: Option[DecreasesTuple],
                                   star: Option[DecreasesStar]) extends Info {
 
   // The comment of this metadata are the provided decreases clauses
-  override lazy val comment: Seq[String] = (tuple ++ wildcard ++ star).map(_.toString()).toSeq
+  override lazy val comment: Seq[String] = (tuple ++ wildcard ++ star).map(_.toString).toSeq
   override val isCached: Boolean = false
 
   /**

From 56d586013eb7a22ea51ca3f52278ba47cc1c1f5d Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 29 Aug 2024 01:31:40 +0200
Subject: [PATCH 21/22] Adapting to lazy val toString

---
 src/main/scala/viper/silver/ast/utility/Permissions.scala | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/Permissions.scala b/src/main/scala/viper/silver/ast/utility/Permissions.scala
index 0389e5eb2..858756002 100644
--- a/src/main/scala/viper/silver/ast/utility/Permissions.scala
+++ b/src/main/scala/viper/silver/ast/utility/Permissions.scala
@@ -28,8 +28,8 @@ object Permissions {
 
   def multiplyExpByPerm(e: Exp, permFactor: Exp) : Exp = {
     assert(permFactor.typ == Perm,
-           "Internal error: attempted to permission-scale expression " + e.toString() +
-               " by non-permission-typed expression " + permFactor.toString())
+           "Internal error: attempted to permission-scale expression " + e.toString +
+               " by non-permission-typed expression " + permFactor.toString)
 
     if(permFactor.isInstanceOf[FullPerm])
       e

From 54cecc4cef610c19c5718189c599cbf1ed14789c Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 30 Aug 2024 23:50:39 +0200
Subject: [PATCH 22/22] More simplification for permission expressions

---
 .../viper/silver/ast/utility/Simplifier.scala | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/src/main/scala/viper/silver/ast/utility/Simplifier.scala b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
index 6730694e9..e440383f2 100644
--- a/src/main/scala/viper/silver/ast/utility/Simplifier.scala
+++ b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
@@ -109,9 +109,15 @@ object Simplifier {
       case PermMinus(PermMinus(single)) => single
       case PermMul(fst, FullPerm()) => fst
       case PermMul(FullPerm(), snd) => snd
+      case root@PermMul(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        val product = Rational(a, b) * Rational(c, d)
+        FractionalPerm(IntLit(product.numerator)(root.pos, root.info), IntLit(product.denominator)(root.pos, root.info))(root.pos, root.info)
       case PermMul(_, np@NoPerm()) if assumeWelldefinedness => np
       case PermMul(np@NoPerm(), _) if assumeWelldefinedness => np
 
+      case PermMul(wc@WildcardPerm(), _) if assumeWelldefinedness => wc
+      case PermMul(_, wc@WildcardPerm()) if assumeWelldefinedness => wc
+
       case root@PermGeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info)
       case root@PermLeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info)
       case root@PermGtCmp(a, b) if assumeWelldefinedness && a == b => FalseLit()(root.pos, root.info)
@@ -125,6 +131,16 @@ object Simplifier {
         BoolLit(Rational(a, b) < Rational(c, d))(root.pos, root.info)
       case root@PermLeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
         BoolLit(Rational(a, b) <= Rational(c, d))(root.pos, root.info)
+      case root@EqCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) == Rational(c, d))(root.pos, root.info)
+      case root@NeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) != Rational(c, d))(root.pos, root.info)
+
+      case root@PermLeCmp(NoPerm(), WildcardPerm()) =>
+        TrueLit()(root.pos, root.info)
+      case root@NeCmp(WildcardPerm(), NoPerm()) =>
+        TrueLit()(root.pos, root.info)
+
       case DebugPermMin(e0@AnyPermLiteral(a, b), e1@AnyPermLiteral(c, d)) =>
         if (Rational(a, b) < Rational(c, d)) {
           e0
@@ -137,6 +153,9 @@ object Simplifier {
       case root@PermAdd(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
         val sum = Rational(a, b) + Rational(c, d)
         FractionalPerm(IntLit(sum.numerator)(root.pos, root.info), IntLit(sum.denominator)(root.pos, root.info))(root.pos, root.info)
+      case PermAdd(NoPerm(), rhs) => rhs
+      case PermAdd(lhs, NoPerm()) => lhs
+      case PermSub(lhs, NoPerm()) => lhs
 
       case root@GeCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left >= right)(root.pos, root.info)