fix minor bugs

src/main/scala/Utils.scala

@@ -137,7 +137,8 @@ package object utils {
       exps.zip(terms).filter(t => t._2 != True).map(e => e._1)
     }
 
-    def buildIteExp(condTerm: Term, ifTerm: Term, elseTerm: Term, condExp: silver.ast.Exp, ifExp: silver.ast.Exp, elseExp: silver.ast.Exp): silver.ast.Exp ={
+    // TODO ake: find a better way to do this
+    def buildIteExp(condTerm: Term, ifTerm: Term, elseTerm: Term, condExp: silver.ast.Exp, ifExp: silver.ast.Exp, elseExp: silver.ast.Exp, typ: silver.ast.Type): silver.ast.Exp ={
       val iteTerm = Ite(condTerm, ifTerm, elseTerm)
       if(iteTerm.equals(ifTerm)){
         ifExp
@@ -148,11 +149,12 @@ package object utils {
       } else if (iteTerm.equals(Not(condTerm))) {
         silver.ast.Not(condExp)()
       }else{
-        silver.ast.And(silver.ast.Implies(condExp, ifExp)(), silver.ast.Implies(silver.ast.Not(condExp)(), elseExp)())()
+        silver.ast.FuncApp("Ite", Seq(condExp, ifExp, elseExp))(condExp.pos, condExp.info, typ, condExp.errT)
+//        silver.ast.And(silver.ast.Implies(condExp, ifExp)(), silver.ast.Implies(silver.ast.Not(condExp)(), elseExp)())() TODO ake: remove
       }
     }
 
-    def buildImpliesExp(assmptTerm: Term, rhsTerm: Term, assmptExp: silver.ast.Exp, rhsExp: silver.ast.Exp): silver.ast.Exp= {
+     def buildImpliesExp(assmptTerm: Term, rhsTerm: Term, assmptExp: silver.ast.Exp, rhsExp: silver.ast.Exp): silver.ast.Exp= {
       val implTerm = Implies(assmptTerm, rhsTerm)
       if (implTerm.equals(True)) {
         silver.ast.TrueLit()()

src/main/scala/decider/DebugExp.scala

@@ -11,6 +11,7 @@ import viper.silicon.state.terms.Term
 import viper.silver.ast
 
 import scala.annotation.unused
+import scala.math
 class DebugExp(str : Option[String],
                @unused exp : Option[ast.Exp],
                substitutedExp : Option[ast.Exp],
@@ -42,7 +43,7 @@ class DebugExp(str : Option[String],
   }
 
   def this(exp : ast.Exp, substitutedExp : ast.Exp) = {
-    this(None, Some(exp), Some(exp), InsertionOrderedSet.empty)
+    this(None, Some(exp), Some(substitutedExp), InsertionOrderedSet.empty)
   }
 
   def withTerms(newTerms : InsertionOrderedSet[Term]): DebugExp = {
@@ -53,17 +54,38 @@ class DebugExp(str : Option[String],
     terms
   }
 
+  def isInternal(): Boolean = isInternal
+
   @unused
   def termsToString: String = {
     terms.map(t => t.toString.replaceAll("@.. ", " ")).mkString(" && ")
   }
 
   override def toString: String = {
-    if(str.isDefined){
-      if(children.isEmpty) str.get
-      else str.get + ": " + children.mkString(" && ")
-    }else{
-      substitutedExp.get.toString() + (if(isImplicationLHS && children.nonEmpty) " ==> (" + children.mkString(" && ") + ")" else "")
+    toString(printInternals = true, 5)
+  }
+
+  def childrenToString(printInternals: Boolean, printChildrenDepth: Int): String = {
+    val nonInternalChildren = children.filter(de => printInternals || !de.isInternal())
+    if (nonInternalChildren.isEmpty || printChildrenDepth <= 0) ""
+    else {
+      "(" + nonInternalChildren.tail.foldLeft[String](nonInternalChildren.head.toString(printInternals, printChildrenDepth - 1))((s, de) => s + " && " + de.toString(printInternals, printChildrenDepth - 1)) + ")"
+    }
+  }
+
+  def toString(printInternals: Boolean, printChildrenDepth: Int): String = {
+    if(isInternal && !printInternals){
+      return ""
+    }
+    if (str.isDefined) {
+      val mainStr = str.get + (if (substitutedExp.isDefined) "(" + substitutedExp.get.toString() + ")" else "")
+      if (children.isEmpty || printChildrenDepth <= 0) mainStr
+      else "(" + mainStr + ": " + childrenToString(printInternals, printChildrenDepth) + ")"
+    } else {
+      if (isImplicationLHS && children.nonEmpty) {
+        "(" + substitutedExp.get.toString() + " ==> " + childrenToString(printInternals, math.max(printChildrenDepth, 1)) + ")"
+      }
+      substitutedExp.get.toString()
     }
   }
 

src/main/scala/decider/Decider.scala

@@ -212,8 +212,8 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
         }
         case None => {
           pathConditions.setCurrentBranchCondition(t, None)
-          assume(t, new DebugExp("unknown branch condition"))
-        } // TODO ake
+          assume(t, new DebugExp("unknown branch condition")) // TODO ake: branch conditions
+        }
       }
     }
 

src/main/scala/interfaces/Verification.scala

@@ -144,15 +144,16 @@ case class SiliconFailureContext(branchConditions: Seq[ast.Exp],
 
   lazy val assumptionsString: String = {
     if(assumptions.nonEmpty){
-      s"\n\nassumptions: ${assumptions.mkString(" && ")}"
+      val nonInternalAssumptions = assumptions.filter(de => !de.isInternal())
+      s"\n\nassumptions:\n${nonInternalAssumptions.tail.foldLeft[String](nonInternalAssumptions.head.toString(printInternals = false, 5))((s, de) => s + " && " + de.toString(printInternals = false, 5)) + ")"}"
     }else{
       ""
     }
   }
 
   lazy val failedAssertionString: String ={
     if(failedAssertion.isDefined){
-      s"Failed Assertion:\n\t\t${failedAssertion.get.toString()}"
+      s"\n\nFailed Assertion:\n\t\t${failedAssertion.get.toString()}"
     }else{
       ""
     }

src/main/scala/resources/NonQuantifiedPropertyInterpreter.scala

@@ -83,7 +83,7 @@ class NonQuantifiedPropertyInterpreter(heap: Iterable[Chunk], verifier: Verifier
 
   override protected def buildValueAccess(chunkPlaceholder: ChunkPlaceholder, info: Info) = {
     info.pm(chunkPlaceholder) match {
-      case c: NonQuantifiedChunk => new Pair(c.snap, ast.TrueLit()())
+      case c: NonQuantifiedChunk => new Pair(c.snap, ast.LocalVar("buildValueAccess not implemented", ast.Int)()) // TODO ake: permission
       // TODO: remove once singleton quantified chunks are not used anymore
       case c: QuantifiedBasicChunk => new Pair(c.valueAt(c.singletonArguments.get), ast.TrueLit()()) // TODO ake: qp
     }

src/main/scala/rules/ChunkSupporter.scala

@@ -178,7 +178,8 @@ object chunkSupporter extends ChunkSupportRules {
           (ConsumptionResult(PermMinus(perms, toTake), ast.PermSub(permsExp, toTakeExp)(permsExp.pos, permsExp.info, permsExp.errT), v, 0), s, newHeap, takenChunk)
         } else {
           if (v.decider.check(ch.perm !== NoPerm, Verifier.config.checkTimeout())) {
-            v.decider.assume(PermLess(perms, ch.perm), new DebugExp("Perm Less"))
+            val debugExp = ast.PermLtCmp(permsExp, ch.permExp)(permsExp.pos, permsExp.info, permsExp.errT)
+            v.decider.assume(PermLess(perms, ch.perm), new DebugExp(debugExp, s.substituteVarsInExp(debugExp)))
             val newChunk = ch.withPerm(PermMinus(ch.perm, perms), ast.PermSub(ch.permExp, permsExp)(permsExp.pos, permsExp.info, permsExp.errT))
             val takenChunk = ch.withPerm(perms, permsExp)
             val newHeap = h - ch + newChunk
@@ -203,7 +204,7 @@ object chunkSupporter extends ChunkSupportRules {
 
     // Try to merge the chunk into the heap by finding an alias.
     // In any case, property assumptions are added after the merge step.
-    val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, h, ch, v)
+    val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, s, h, ch, v)
     Q(s.copy(functionRecorder = fr1), h1, v)
   }
 

src/main/scala/rules/Consumer.scala

@@ -364,8 +364,8 @@ object consumer extends ConsumptionRules {
               val (smDef1, smCache1) =
                 quantifiedChunkSupporter.summarisingSnapshotMap(
                   s2, predicate, s2.predicateFormalVarMap(predicate), relevantChunks, v2)
-              val argsString = eArgs.map(e => s2.substituteVarsInExp(e)).mkString(", ")
-              val debugExp = new DebugExp(s"Predicate Trigger: ${predicate.name}($argsString)")
+              val argsString = eArgs.map(s2.substituteVarsInExp).mkString(", ")
+              val debugExp = new DebugExp(s"PredicateTrigger(${predicate.name}($argsString))")
               v2.decider.assume(PredicateTrigger(predicate.name, smDef1.sm, tArgs), debugExp)
               s2.copy(smCache = smCache1)
             } else {
@@ -422,9 +422,9 @@ object consumer extends ConsumptionRules {
             val (smDef1, smCache1) =
               quantifiedChunkSupporter.summarisingSnapshotMap(
                 s1, wand, formalVars, relevantChunks, v1)
-            val argsString = bodyVars.map(e => s1.substituteVarsInExp(e)).mkString(", ")
+            val argsString = bodyVars.map(s1.substituteVarsInExp).mkString(", ")
             val predName = MagicWandIdentifier(wand, s.program).toString
-            val debugExp = new DebugExp(s"Predicate Trigger: $predName($argsString)")
+            val debugExp = new DebugExp(s"PredicateTrigger($predName($argsString))")
             v1.decider.assume(PredicateTrigger(predName, smDef1.sm, tArgs), debugExp)
             s1.copy(smCache = smCache1)
           } else {

src/main/scala/rules/Evaluator.scala

@@ -173,7 +173,7 @@ object evaluator extends EvaluationRules {
 
       case _: ast.WildcardPerm =>
         val (tVar, tConstraints) = v.decider.freshARP()
-        v.decider.assume(tConstraints, new DebugExp(s"WildcardPerm Access: ${tConstraints.toString}")) // TODO ake: wildcard
+        v.decider.assume(tConstraints, new DebugExp(s"wildcard == ${tVar.toString}", true))
         /* TODO: Only record wildcards in State.constrainableARPs that are used in exhale
          *       position. Currently, wildcards used in inhale position (only) may not be removed
          *       from State.constrainableARPs (potentially inefficient, but should be sound).
@@ -462,8 +462,8 @@ object evaluator extends EvaluationRules {
                   val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v1.symbolConverter.toSort(bodyVars(i).typ)))
                   val (s2, pmDef) = if (s1.heapDependentTriggers.contains(MagicWandIdentifier(wand, s1.program))) {
                     val (s2, smDef, pmDef) = quantifiedChunkSupporter.heapSummarisingMaps(s1, wand, formalVars, relevantChunks, v1)
-                    val argsString = bodyVars.map(e => s2.substituteVarsInExp(e)).mkString(", ")
-                    val debugExp = new DebugExp(s"Predicate Trigger: ${identifier.toString}($argsString)")
+                    val argsString = bodyVars.map(s2.substituteVarsInExp).mkString(", ")
+                    val debugExp = new DebugExp(s"PredicateTrigger(${identifier.toString}($argsString))")
                     v1.decider.assume(PredicateTrigger(identifier.toString, smDef.sm, args), debugExp)
                     (s2, pmDef)
                   } else {
@@ -504,8 +504,8 @@ object evaluator extends EvaluationRules {
                       s1, predicate, s1.predicateFormalVarMap(predicate), relevantChunks, v1)
                   if (s2.heapDependentTriggers.contains(predicate)){
                     val trigger = PredicateTrigger(predicate.name, smDef.sm, args)
-                    val argsString = predicate.formalArgs.mkString(", ") // TODO ake: substitution
-                    val debugExp = new DebugExp(s"Predicate Trigger: ${predicate.name}($argsString)")
+                    val argsString = predicate.formalArgs.map(e => s2.substituteVarsInExp(e.localVar)).mkString(", ")
+                    val debugExp = new DebugExp(s"PredicateTrigger(${predicate.name}($argsString))")
                     v1.decider.assume(trigger, debugExp)
                   }
                   (s2, PredicatePermLookup(identifier.toString, pmDef.pm, args))
@@ -830,8 +830,8 @@ object evaluator extends EvaluationRules {
                          * (see 'predicateTriggers' in FunctionData.scala).
                          */
                       if (!Verifier.config.disableFunctionUnfoldTrigger()) {
-                        val eArgsString = eArgs.mkString(", ")
-                        val debugExp = new DebugExp(s"Predicate Trigger ${predicate.name}($eArgsString)")
+                        val eArgsString = eArgs.map(s.substituteVarsInExp).mkString(", ")
+                        val debugExp = new DebugExp(s"PredicateTrigger(${predicate.name}($eArgsString))")
                         v4.decider.assume(App(s.predicateData(predicate).triggerFunction, snap.convert(terms.sorts.Snap) +: tArgs), debugExp)
                       }
                       val body = predicate.body.get /* Only non-abstract predicates can be unfolded */
@@ -1433,7 +1433,7 @@ object evaluator extends EvaluationRules {
         var sJoined = entries.tail.foldLeft(entries.head.s)((sAcc, entry) =>sAcc.merge(entry.s))
         sJoined = sJoined.copy(functionRecorder = sJoined.functionRecorder.recordPathSymbol(joinSymbol))
 
-        v.decider.assume(joinDefEqs, new DebugExp("Join")) // TODO ake
+        v.decider.assume(joinDefEqs, new DebugExp("Join")) // TODO ake: join
 
         (sJoined, joinTerm)
     }

src/main/scala/rules/Executor.scala

@@ -81,7 +81,7 @@ object executor extends ExecutionRules {
   def handleOutEdge(s: State, edge: SilverEdge, v: Verifier): State = {
     edge.kind match {
       case cfg.Kind.Out =>
-        val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, s.h, s.invariantContexts.head, v)
+        val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, s, s.h, s.invariantContexts.head, v)
         val s1 = s.copy(functionRecorder = fr1, h = h1,
           invariantContexts = s.invariantContexts.tail)
         s1
@@ -540,8 +540,8 @@ object executor extends ExecutionRules {
               val (smDef1, smCache1) =
                 quantifiedChunkSupporter.summarisingSnapshotMap(
                   s2, predicate, s2.predicateFormalVarMap(predicate), relevantChunks, v2)
-              val eArgsStr = eArgs.map(e => s2.substituteVarsInExp(e)).mkString(", ")
-              val debugExp = new DebugExp(Some(s"Predicate Trigger ${predicate.name}($eArgsStr)"), Some(pa), Some(s2.substituteVarsInExp(pa)), InsertionOrderedSet.empty)
+              val eArgsStr = eArgs.map(s2.substituteVarsInExp).mkString(", ")
+              val debugExp = new DebugExp(Some(s"PredicateTrigger(${predicate.name}($eArgsStr))"), Some(pa), Some(s2.substituteVarsInExp(pa)), InsertionOrderedSet.empty)
               v2.decider.assume(PredicateTrigger(predicate.name, smDef1.sm, tArgs), debugExp)
               smCache1
             } else {

src/main/scala/rules/MagicWandSupporter.scala

@@ -438,7 +438,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
       val s3 = s2.copy(conservedPcs = conservedPcs +: s2.conservedPcs.tail, reserveHeaps = s.reserveHeaps.head +: hs2)
 
       val usedChunks = chs2.flatten
-      val (fr4, hUsed) = v2.stateConsolidator.merge(s3.functionRecorder, s2.reserveHeaps.head, Heap(usedChunks), v2)
+      val (fr4, hUsed) = v2.stateConsolidator.merge(s3.functionRecorder, s3, s2.reserveHeaps.head, Heap(usedChunks), v2)
 
       val s4 = s3.copy(functionRecorder = fr4, reserveHeaps = hUsed +: s3.reserveHeaps.tail)
 
@@ -483,7 +483,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
        * is consumed from hOps and permissions for the predicate are added to the state's
        * heap. After a statement is executed those permissions are transferred to hOps.
        */
-      val (fr, hOpsJoinUsed) = v.stateConsolidator.merge(newState.functionRecorder, newState.reserveHeaps(1), newState.h, v)
+      val (fr, hOpsJoinUsed) = v.stateConsolidator.merge(newState.functionRecorder, newState, newState.reserveHeaps(1), newState.h, v)
       newState.copy(functionRecorder = fr, h = Heap(),
           reserveHeaps = Heap() +: hOpsJoinUsed +: newState.reserveHeaps.drop(2))
     } else newState

src/main/scala/rules/MoreCompleteExhaleSupporter.scala

@@ -117,7 +117,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
     }
     val (s1, taggedSnap, snapDefs, permSum) = summariseOnly(s, relevantChunks, resource, args, v)
 
-    v.decider.assume(And(snapDefs), new DebugExp("Snapshot", true))
+    v.decider.assume(And(snapDefs), new DebugExp("Snapshot", true)) // TODO ake: hier bekommt man assumption wie z.B. n.val == 2
 //    v.decider.assume(PermAtMost(permSum, FullPerm())) /* Done in StateConsolidator instead */
 
     val s2 =
@@ -263,11 +263,11 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
               // that already exists.
               // During function verification, we should not define macros, since they could contain resullt, which is not
               // defined elsewhere.
-              val iteExp = buildIteExp(eq, PermMin(ch.perm, pNeeded), NoPerm, eqExp, buildMinExp(Seq(ch.permExp, pNeededExp), ast.Perm), ast.NoPerm()(permsExp.pos, permsExp.info, permsExp.errT))
+              val iteExp = buildIteExp(eq, PermMin(ch.perm, pNeeded), NoPerm, eqExp, buildMinExp(Seq(ch.permExp, pNeededExp), ast.Perm), ast.NoPerm()(permsExp.pos, permsExp.info, permsExp.errT), ast.Perm)
               (Ite(eq, PermMin(ch.perm, pNeeded), NoPerm), iteExp)
             } else {
               val pTakenBody = Ite(eq, PermMin(ch.perm, pNeeded), NoPerm)
-              val pTakenExp = buildIteExp(eq, PermMin(ch.perm, pNeeded), NoPerm, eqExp, buildMinExp(Seq(ch.permExp, pNeededExp), ast.Perm), ast.NoPerm()())
+              val pTakenExp = buildIteExp(eq, PermMin(ch.perm, pNeeded), NoPerm, eqExp, buildMinExp(Seq(ch.permExp, pNeededExp), ast.Perm), ast.NoPerm()(), ast.Perm)
               val pTakenArgs = additionalArgs
               val pTakenDecl = v.decider.freshMacro("mce_pTaken", pTakenArgs, pTakenBody)
               val pTakenMacro = Macro(pTakenDecl.id, pTakenDecl.args.map(_.sort), pTakenDecl.body.sort)
@@ -278,7 +278,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
             }
 
             pSum = PermPlus(pSum, Ite(eq, ch.perm, NoPerm))
-            pSumExp = ast.PermAdd(pSumExp, buildIteExp(eq, ch.perm, NoPerm, eqExp, ch.permExp, ast.NoPerm()()))()
+            pSumExp = ast.PermAdd(pSumExp, buildIteExp(eq, ch.perm, NoPerm, eqExp, ch.permExp, ast.NoPerm()(), ast.Perm))()
 
             val newChunk = ch.withPerm(PermMinus(ch.perm, pTaken), ast.PermSub(ch.permExp, pTakenExp)(permsExp.pos, permsExp.info, permsExp.errT))
             pNeeded = PermMinus(pNeeded, pTaken)
@@ -301,7 +301,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         newChunks foreach { ch =>
           val resource = Resources.resourceDescriptions(ch.resourceID)
           val pathCond = interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties)
-          pathCond.foreach(p => v.decider.assume(p.getFirst, new DebugExp(p.getSecond, p.getSecond)))
+          pathCond.foreach(p => v.decider.assume(p.getFirst, new DebugExp(p.getSecond, s.substituteVarsInExp(p.getSecond))))
         }
         val newHeap = Heap(allChunks)
 
@@ -354,10 +354,10 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         val eq = And(eqCmps)
         val eqExp = BigAnd(removeKnownToBeTrueExp(ch.argsExp.zip(argsExp).map{ case (t1, t2) => ast.EqCmp(t1, t2)(permsExp.pos, permsExp.info, permsExp.errT) }.toList, eqCmps.toList))
         val permTaken = v.decider.fresh("p", sorts.Perm)
-        val permTakenExp = ast.LocalVar(permTaken.id.name, ast.Perm)(permsExp.pos, permsExp.info, permsExp.errT)
+        val permTakenExp = ast.LocalVar(permTaken.id.name.substring(0, permTaken.id.name.lastIndexOf("@")), ast.Perm)(permsExp.pos, permsExp.info, permsExp.errT)
 
         totalPermSum = PermPlus(totalPermSum, Ite(eq, ch.perm, NoPerm))
-        totalPermSumExp = ast.PermAdd(totalPermSumExp, buildIteExp(eq, ch.perm, NoPerm, eqExp, ch.permExp, ast.NoPerm()()))(permsExp.pos, permsExp.info, permsExp.errT)
+        totalPermSumExp = ast.PermAdd(totalPermSumExp, buildIteExp(eq, ch.perm, NoPerm, eqExp, ch.permExp, ast.NoPerm()(), ast.Perm))(permsExp.pos, permsExp.info, permsExp.errT)
         totalPermTaken = PermPlus(totalPermTaken, permTaken)
         totalPermTakenExp = ast.PermAdd(totalPermTakenExp, permTakenExp)(permsExp.pos, permsExp.info, permsExp.errT)