Chalice: added findFunctionAppsContaining(..) to Expression, which finds all the function applications with at least one variable in common with a given list. This is a pre-cursor to writing a trigger-generating routine for quantifiers.

Also corrected some copy-paste comments in Translator.scala

2 files changed, 19 insertions, 2 deletions

diff --git a/Chalice/src/main/scala/Ast.scala b/Chalice/src/main/scala/Ast.scala
index 74670fd5..3e4861fe 100644
--- a/Chalice/src/main/scala/Ast.scala
+++ b/Chalice/src/main/scala/Ast.scala
@@ -415,6 +415,24 @@ sealed abstract class Expression extends RValue {
   def transform(f: Expression => Option[Expression]) = AST.transform(this, f)

   def visit(f: RValue => Unit) = AST.visit(this, f)

   def visitOpt(f: RValue => Boolean) = AST.visitOpt(this, f)

+  // this is used for searching for triggers for quantifiers around this expression

+  def findFunctionAppsContaining(vs:List[Variable]): List[(Expression,Set[Variable])] = {

+    var functions: List[(Expression,Set[Variable])] = List()

+    this visit {_ match {

+      case fapp@FunctionApplication(obj, id, args) =>

+        var containedVars : Set[Variable] = Set()

+        fapp visit {_ match {

+          case ve@VariableExpr(s) =>

+            val v : Variable = ve.v

+            if (vs.contains(v)) (containedVars += v)

+          case _ =>}

+        }

+        if (!containedVars.isEmpty()) (functions = (fapp, containedVars) :: functions)

+      case _ =>}

+    }

+    functions

+  }

+

 }

 sealed abstract class Literal extends Expression

 case class IntLiteral(n: Int) extends Literal

diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index f0c00ed1..b5621e49 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -1881,8 +1881,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
       (FunctionApp(functionName(func.f), Heap :: trArgsE),trArgsL)

     }

     case uf@Unfolding(acc@Access(pred@MemberAccess(obj, f), perm), ufexpr) =>

-      // handle unfolding like the next case, but also record permissions of the predicate

-      // in the secondary mask and track the predicate in the auxilary information

+      // record extra information resulting from "peeking inside" the predicate, generating appropriate statements (this is used in Exhale of an expression)

             val (ee,ll) = trrecursive(ufexpr)

             val (receiverV, receiver) = Boogie.NewBVar("predRec", tref, true)

             val (versionV, version) = Boogie.NewBVar("predVer", tint, true)