diff options
author | 2012-02-25 03:22:10 -0800 | |
---|---|---|
committer | 2012-02-25 03:22:10 -0800 | |
commit | 0c33796e2f4d5f5d555dd55daf58e1ce1a195fd4 (patch) | |
tree | 40e9d9953bbd3add0bcf74e0b1c7c1620a83029a /Chalice/src/main/scala/Translator.scala | |
parent | e663d52194a17a63fa1e97a727e2aad1dd0acf0d (diff) |
Chalice: Change trigger function to only take a single argument.
Diffstat (limited to 'Chalice/src/main/scala/Translator.scala')
-rw-r--r-- | Chalice/src/main/scala/Translator.scala | 31 |
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 = {
|