Fixing unsoundness for functions

src/main/scala/rules/MoreCompleteExhaleSupporter.scala

@@ -444,8 +444,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         val eqCmps = ch.args.zip(args).map { case (t1, t2) => t1 === t2 }
         val eq = And(eqCmps)
         val eqExp = permsExp.map(pe => BigAnd(removeKnownToBeTrueExp(ch.argsExp.get.zip(argsExp.get).map{ case (t1, t2) => ast.EqCmp(t1, t2)(pe.pos, pe.info, pe.errT) }.toList, eqCmps.toList)))
-        val permTaken = v.decider.fresh("p", sorts.Perm, Option.when(withExp)(PPrimitiv(PReserved(PKw.Perm)((ast.NoPosition, ast.NoPosition)))()))
-        val permTakenExp = permsExp.map(pe => ast.LocalVar(simplifyVariableName(permTaken.id.name), ast.Perm)(pe.pos, pe.info, pe.errT))
+        val permTaken = v.decider.appliedFresh("p", sorts.Perm, s.functionRecorderQuantifiedVariables().map(_._1))
+        val permTakenExp = permsExp.map(pe => ast.LocalVar(simplifyVariableName(permTaken.applicable.id.name), ast.Perm)(pe.pos, pe.info, pe.errT))
 
         totalPermSum = PermPlus(totalPermSum, Ite(eq, ch.perm, NoPerm))
         totalPermSumExp = totalPermSumExp.map(tps => ast.PermAdd(tps, ast.CondExp(eqExp.get, ch.permExp.get, ast.NoPerm()())(eqExp.get.pos, eqExp.get.info, eqExp.get.errT))(permsExp.get.pos, permsExp.get.info, permsExp.get.errT))
@@ -464,7 +464,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
 
         v.decider.assume(constraint, Option.when(withExp)(DebugExp.createInstance(constraintExp, constraintExp)))
-        newFr = newFr.recordConstrainedVar(permTaken, constraint)
+
+        newFr = newFr.recordPathSymbol(permTaken.applicable.asInstanceOf[Function]).recordConstraint(constraint)
 
         ch.withPerm(PermMinus(ch.perm, permTaken), permsExp.map(pe => ast.PermSub(ch.permExp.get, permTakenExp.get)(pe.pos, pe.info, pe.errT)))
       })

src/main/scala/state/Terms.scala

@@ -1263,13 +1263,13 @@ object FractionPerm extends CondFlyweightFactory[(Term, Term), Permissions, Frac
   override def actualCreate(args: (Term, Term)): FractionPerm = new FractionPerm(args._1, args._2)
 }
 
-class IsValidPermVar private[terms] (val v: Var) extends BooleanTerm with ConditionalFlyweight[Var, IsValidPermVar] {
-  override val equalityDefiningMembers: Var = v
-  override lazy val toString = s"PVar($v)"
+class IsValidPermVar private[terms] (val t: Term) extends BooleanTerm with ConditionalFlyweight[Term, IsValidPermVar] {
+  override val equalityDefiningMembers: Term = t
+  override lazy val toString = s"PVar($t)"
 }
 
-object IsValidPermVar extends CondFlyweightTermFactory[Var, IsValidPermVar] {
-  override def actualCreate(args: Var): IsValidPermVar = new IsValidPermVar((args))
+object IsValidPermVar extends CondFlyweightTermFactory[Term, IsValidPermVar] {
+  override def actualCreate(args: Term): IsValidPermVar = new IsValidPermVar((args))
 }
 
 class IsReadPermVar private[terms] (val v: Var) extends BooleanTerm with ConditionalFlyweight[Var, IsReadPermVar] {

src/main/scala/state/Utils.scala

@@ -108,7 +108,7 @@ package object utils {
     case or: Or => or.ts
     case _: PermLiteral => Nil
     case fp: FractionPerm => List(fp.n, fp.d)
-    case ivp: IsValidPermVar => List(ivp.v)
+    case ivp: IsValidPermVar => List(ivp.t)
     case irp: IsReadPermVar => List(irp.v)
     case app: Application[_] => app.args
     case sr: SeqRanged => List(sr.p0, sr.p1)

src/main/scala/supporters/functions/FunctionRecorder.scala

@@ -202,7 +202,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
     else this
 
   def recordPathSymbol(symbol: Function): ActualFunctionRecorder =
-    if (depth <= 1) copy(freshPathSymbols = freshPathSymbols + symbol)
+    if (depth <= 2) copy(freshPathSymbols = freshPathSymbols + symbol)
     else this
 
   def recordFreshMacro(decl: MacroDecl): FunctionRecorder =