From c18701c1cffb29672d42f1d2c6a0e6a740daeaa9 Mon Sep 17 00:00:00 2001
From: stefanheule <unknown>
Date: Sat, 25 Feb 2012 03:23:07 -0800
Subject: Chalice: Change the Chalice function triggering mechanism to use a
 function per predicate (instead of a function per function).

---
 Chalice/src/main/scala/Ast.scala        | 15 +++++++++++++++
 Chalice/src/main/scala/Translator.scala | 15 ++++++---------
 2 files changed, 21 insertions(+), 9 deletions(-)

(limited to 'Chalice/src/main')

diff --git a/Chalice/src/main/scala/Ast.scala b/Chalice/src/main/scala/Ast.scala
index e84c2fde..943e83b2 100644
--- a/Chalice/src/main/scala/Ast.scala
+++ b/Chalice/src/main/scala/Ast.scala
@@ -191,6 +191,21 @@ case class Predicate(id: String, private val rawDefinition: Expression) extends
   }
 }
 case class Function(id: String, ins: List[Variable], out: Type, spec: List[Specification], definition: Option[Expression]) extends NamedMember(id) {
+  // list of predicates that this function possibly depends on (that is, predicates
+  // that are mentioned in the functions precondition)
+  def dependentPredicates: List[Predicate] = {
+    var predicates: List[Predicate] = List()
+    spec foreach {
+      case Precondition(e) =>
+        e visit {_ match {
+          case pred@MemberAccess(e, p) if pred.isPredicate =>
+            predicates = pred.predicate :: predicates
+          case _ =>}
+        }
+      case _ =>
+    }
+    predicates
+  }
   def apply(rec: Expression, args: List[Expression]): FunctionApplication = {
     val result = FunctionApplication(rec, id, args);
     result.f = this;
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index a943e923..d370813e 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -218,7 +218,7 @@ class Translator {
     val formalsWithoutReceiver = f1 ::: f1b ::: f2;
     val applyF = FunctionApp(functionName(f), List(etran.Heap) ::: args);
     val limitedApplyF = FunctionApp(functionName(f) + "#limited", List(etran.Heap) ::: args)
-    val trigger = FunctionApp(functionName(f)+"#trigger", thisArg :: Nil);
+    val triggers = f.dependentPredicates map (p => new Trigger(FunctionApp("#" + p.FullName+"#trigger", thisArg :: Nil)))
     val pre = Preconditions(f.spec).foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b) });
     val wellformed = wf(VarExpr(HeapName), VarExpr(MaskName), VarExpr(SecMaskName))
 
@@ -257,8 +257,8 @@ class Translator {
       Axiom(new Boogie.Forall(formals,
             new Trigger(List(applyF,wellformed)),
             (wellformed ==> (applyF ==@ limitedApplyF)))) ::
-      Axiom(new Boogie.Forall(formalsOnlyReceiver,
-        new Trigger(trigger),
+      Axiom(new Boogie.Forall(Nil, formalsOnlyReceiver,
+        triggers,
         new Boogie.Forall(formalsWithoutReceiver,
             new Trigger(List(limitedApplyF,wellformed)),
             (applyF ==@ limitedApplyF)))) ::
@@ -356,6 +356,8 @@ class Translator {
     Const(pred.FullName, true, FieldType(tint)) ::
     // axiom PredicateField(f);
     Axiom(PredicateField(pred.FullName)) ::
+    // trigger function to unfold function definitions
+    Boogie.Function("#" + pred.FullName + "#trigger", BVar("this", tref) :: Nil, BVar("$myresult", tbool)) ::
     // check definedness of predicate body
     Proc(pred.FullName + "$checkDefinedness",
       List(NewBVarWhere("this", new Type(currentClass))),
@@ -2732,12 +2734,7 @@ object TranslationHelper {
   // output a dummy function assumption that serves as trigger for the function
   // definition axiom.
   def functionTrigger(receiver: Expr, predicate: Predicate): List[Stmt] = {
-    for (f <- predicate.dependentFunctions) yield {
-      val args = for (i <- f.ins) yield {
-        defaultValue(i.t)
-      }
-      bassume(FunctionApp(functionName(f)+"#trigger", receiver :: Nil))
-    }
+    bassume(FunctionApp("#" + predicate.FullName+"#trigger", receiver :: Nil)) :: Nil
   }
   def defaultValue(t: Type): Expr = {
     t match {
-- 
cgit v1.2.3