Chalice: Improve code to generate triggers for framing axiom.

2 files changed, 27 insertions, 24 deletions

diff --git a/Chalice/src/main/scala/Chalice.scala b/Chalice/src/main/scala/Chalice.scala
index 6d7b2f54..2514d6b1 100644
--- a/Chalice/src/main/scala/Chalice.scala
+++ b/Chalice/src/main/scala/Chalice.scala
@@ -366,26 +366,7 @@ object Chalice {
       tmpTime = System.nanoTime

       

       // write to out.bpl

-      val ss = """

-function IsGoodExhaleState(eh: HeapType, h: HeapType,

-                           m: MaskType, sm: MaskType) returns (bool)

-{

-  (forall<T> o: ref, f: Field T :: { eh[o, f] }  CanRead(m, sm, o, f) ==> eh[o, f] == h[o, f]) &&

-  (forall o: ref :: { eh[o, held] }  (0<eh[o, held]) == (0<h[o, held])) &&

-  (forall o: ref :: { eh[o, rdheld] }  eh[o, rdheld] == h[o, rdheld]) &&

-  (forall o: ref :: { h[o, held] }  (0<h[o, held]) ==> eh[o, mu] == h[o, mu]) &&

-  (forall o: ref :: { h[o, rdheld] }  h[o, rdheld] ==> eh[o, mu] == h[o, mu]) &&

-  (forall o: ref :: { h[o, forkK] } { eh[o, forkK] } h[o, forkK] == eh[o, forkK]) &&

-  (forall o: ref :: { h[o, held] } { eh[o, held] } h[o, held] == eh[o, held]) &&

-  (forall o: ref, f: Field int :: { eh[o, f], PredicateField(f) } PredicateField(f) ==> h[o, f] <= eh[o, f]) &&

-  (forall o: ref, f: Field int :: { h[o, predicateMaskField(f)], PredicateField(f) } { eh[o, predicateMaskField(f)], PredicateField(f) } { m[o, predicateMaskField(f)], PredicateField(f) } """

-    val ss2 =  (TranslatorPrelude.preds map (x => "{ #"+x.FullName+"#trigger(o), PredicateField(f) }")).mkString(" ")

-    val ss3 = """ PredicateField(f) && CanRead(m, sm, o, f) ==>

-      (forall<T> o2: ref, f2: Field T :: { h[o2, f2] } { eh[o2, f2] } { m[o2, f2] }  h[o, predicateMaskField(f)][o2, f2] ==> eh[o2, f2] == h[o2, f2])) &&

-  (forall o: ref, f: Field int :: { PredicateField(f), eh[o, predicateMaskField(f)] } PredicateField(f) && CanRead(m, sm, o, f) ==> eh[o, predicateMaskField(f)] == h[o, predicateMaskField(f)])

-}

-      """

-      val bplText = TranslatorPrelude.P + ss + ss2 + ss3 + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b };

+      val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b };

       val bplFilename = if (vsMode) "c:\\tmp\\out.bpl" else (if (params.noBplFile) "stdin.bpl" else params.bplFile)

       if (!params.noBplFile) writeFile(bplFilename, bplText);

       // run Boogie.exe on out.bpl

diff --git a/Chalice/src/main/scala/Prelude.scala b/Chalice/src/main/scala/Prelude.scala
index 3a75f3e5..fc98a36c 100644
--- a/Chalice/src/main/scala/Prelude.scala
+++ b/Chalice/src/main/scala/Prelude.scala
@@ -25,10 +25,12 @@ object TranslatorPrelude {
     components --= c

   }

 

+  // records that a predicate occurs in the program (used for generating the

+  // correct triggers for an axiom in the prelude)

   def addPredicate(p: Predicate*): Unit = {

-    preds ++= p

+    predicates ++= p

   }

-  val preds: Set[Predicate] = Set()

+  val predicates: Set[Predicate] = Set()

   

   // default components

   private val components: Set[PreludeComponent] = Set(CopyrightPL, TypesPL, PermissionTypesAndConstantsPL, CreditsAndMuPL, PermissionFunctionsAndAxiomsPL, IfThenElsePL, ArithmeticPL, StringPL)

@@ -142,7 +144,8 @@ axiom 0 < predicateK && 1000*predicateK < Fractions(1);
 axiom predicateK == channelK && channelK == monitorK;"""

 }

 object CreditsAndMuPL extends PreludeComponent {

-  val text = """

+  def text = {

+    val base = """

 var Credits: CreditsType;

 

 function combine(PartialHeapType, PartialHeapType) returns (PartialHeapType);

@@ -200,7 +203,26 @@ function IsGoodExhalePredicateState(eh: HeapType, h: HeapType, pm: PMaskType) re
   (forall<T> o: ref, f: Field T :: { eh[o, f] }  pm[o, f] ==> eh[o, f] == h[o, f])

 }

 function predicateMaskField<T>(f: Field T): Field PMaskType;

-"""

+function IsGoodExhaleState(eh: HeapType, h: HeapType,

+                           m: MaskType, sm: MaskType) returns (bool)

+{

+  (forall<T> o: ref, f: Field T :: { eh[o, f] }  CanRead(m, sm, o, f) ==> eh[o, f] == h[o, f]) &&

+  (forall o: ref :: { eh[o, held] }  (0<eh[o, held]) == (0<h[o, held])) &&

+  (forall o: ref :: { eh[o, rdheld] }  eh[o, rdheld] == h[o, rdheld]) &&

+  (forall o: ref :: { h[o, held] }  (0<h[o, held]) ==> eh[o, mu] == h[o, mu]) &&

+  (forall o: ref :: { h[o, rdheld] }  h[o, rdheld] ==> eh[o, mu] == h[o, mu]) &&

+  (forall o: ref :: { h[o, forkK] } { eh[o, forkK] } h[o, forkK] == eh[o, forkK]) &&

+  (forall o: ref :: { h[o, held] } { eh[o, held] } h[o, held] == eh[o, held]) &&

+  (forall o: ref, f: Field int :: { eh[o, f], PredicateField(f) } PredicateField(f) ==> h[o, f] <= eh[o, f]) &&

+  (forall o: ref, f: Field int :: { h[o, predicateMaskField(f)], PredicateField(f) } { eh[o, predicateMaskField(f)], PredicateField(f) } { m[o, predicateMaskField(f)], PredicateField(f) } """

+    val triggers =  (TranslatorPrelude.predicates map (x => "{ #"+x.FullName+"#trigger(o), PredicateField(f) }")).mkString(" ")

+    val rest = """ PredicateField(f) && CanRead(m, sm, o, f) ==>

+      (forall<T> o2: ref, f2: Field T :: { h[o2, f2] } { eh[o2, f2] } { m[o2, f2] }  h[o, predicateMaskField(f)][o2, f2] ==> eh[o2, f2] == h[o2, f2])) &&

+  (forall o: ref, f: Field int :: { PredicateField(f), eh[o, predicateMaskField(f)] } PredicateField(f) && CanRead(m, sm, o, f) ==> eh[o, predicateMaskField(f)] == h[o, predicateMaskField(f)])

+}

+      """

+    base + triggers + rest

+  }

 }

 object PermissionFunctionsAndAxiomsPL extends PreludeComponent {

   val text = """