Chalice: Change trigger function to only take a single argument.

1 files changed, 18 insertions, 13 deletions

diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index 84a2efe8..8cc24e0b 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -204,13 +204,18 @@ class Translator {
   }

   

   def definitionAxiom(f: Function, definition: Expression): List[Decl] = {

-    val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});

-    val args = VarExpr("this") :: inArgs;

-    val formals = BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar(SecMaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar);

-    val formals2 = BVar(HeapName+"2", theap) :: BVar(MaskName+"2", tmask) :: BVar(SecMaskName+"2", tmask) :: Nil;

+    val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)})

+    val thisArg = VarExpr("this")

+    val args = thisArg :: inArgs;

+    

+    val f1 = BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar(SecMaskName, tmask) :: Nil

+    val f2 = (f.ins map Variable2BVar)

+    val f3 = BVar("this", tref)

+    val formals = f1 ::: f3 :: f2;

+    val formalsOnlyReceiver = f3 :: Nil

+    val formalsWithoutReceiver = f1 ::: f2;

     val applyF = FunctionApp(functionName(f), List(etran.Heap, etran.Mask, etran.SecMask) ::: args);

-    val trigger = FunctionApp(functionName(f)+"#trigger", List(etran.Heap, etran.Mask, etran.SecMask) ::: args);

-    val trigger2 = FunctionApp(functionName(f)+"#trigger", VarExpr(HeapName+"2") :: VarExpr(MaskName+"2") :: VarExpr(SecMaskName+"2") :: args);

+    val trigger = FunctionApp(functionName(f)+"#trigger", thisArg :: Nil);

     val pre = Preconditions(f.spec).foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b) });

 

     /** Limit application of the function by introducing a second (limited) function */

@@ -245,15 +250,15 @@ class Translator {
     (if (f.isRecursive)

       // define the limited function (even for unlimited function since its SCC might have limited functions)

       Boogie.Function(functionName(f) + "#limited", formals, BVar("$myresult", f.out.typ)) ::

-      Axiom(new Boogie.Forall(Nil,

-        formals, List(new Trigger(applyF), new Trigger(trigger)),

-        (trigger) && (applyF ==@ FunctionApp(functionName(f) + "#limited", List(etran.Heap, etran.Mask, etran.SecMask) ::: args)))) ::

+      Axiom(new Boogie.Forall(formalsOnlyReceiver,

+        new Trigger(trigger),

+        new Boogie.Forall(formalsWithoutReceiver,

+            new Trigger(applyF),

+            (applyF ==@ FunctionApp(functionName(f) + "#limited", List(etran.Heap, etran.Mask, etran.SecMask) ::: args))))) ::

       Nil

     else

       Nil) :::

-    Boogie.Function(functionName(f) + "#trigger", formals, BVar("$myresult", tbool)) ::

-    Axiom(new Boogie.Forall(formals, new Trigger(trigger), trigger ==@ true)) ::

-    Axiom(new Boogie.Forall(formals ::: formals2, new Trigger(List(trigger,trigger2)), trigger ==@ trigger2)) :: Nil

+    Boogie.Function(functionName(f) + "#trigger", formalsOnlyReceiver, BVar("$myresult", tbool)) :: Nil

   }

 

   def framingAxiom(f: Function): List[Decl] = {

@@ -2718,7 +2723,7 @@ object TranslationHelper {
       val args = for (i <- f.ins) yield {

         defaultValue(i.t)

       }

-      bassume(FunctionApp(functionName(f)+"#trigger", List(etran.Heap, etran.Mask, etran.SecMask, receiver) ::: args))

+      bassume(FunctionApp(functionName(f)+"#trigger", receiver :: Nil))

     }

   }

   def defaultValue(t: Type): Expr = {