Chalice: Remove IsGoodState as it is not needed and causes problems in certain cases.

2 files changed, 2 insertions, 10 deletions

diff --git a/Chalice/src/main/scala/Prelude.scala b/Chalice/src/main/scala/Prelude.scala
index 721b0131..f54cee2c 100644
--- a/Chalice/src/main/scala/Prelude.scala
+++ b/Chalice/src/main/scala/Prelude.scala
@@ -137,15 +137,11 @@ object CreditsAndMuPL extends PreludeComponent {
   val text = """

 var Credits: CreditsType;

 

-function IsGoodState(PartialHeapType) returns (bool);

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

 function heapFragment<T>(T) returns (PartialHeapType);

 type PartialHeapType;

 const emptyPartialHeap: PartialHeapType;

 

-axiom (forall a: PartialHeapType, b: PartialHeapType :: {IsGoodState(combine(a, b))} IsGoodState(combine(a, b)) <==> IsGoodState(a) && IsGoodState(b));

-axiom IsGoodState(emptyPartialHeap);

-

 type ModuleName;

 const CurrentModule: ModuleName;

 type TypeName;

diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index 469714f7..94d44d9e 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -265,7 +265,7 @@ class Translator {
       // Encoding with heapFragment and combine

       /* function ##C.f(state, ref, t_1, ..., t_n) returns (t);

          axiom (forall h: HeapType, m, sm: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::

-            wf(h, m, sm) && IsGoodState(partialHeap) ==> #C.f(h, m, sm, this, x_1, ..., x_n) ==  ##C.f(partialHeap, this, x_1, ..., x_n))

+            wf(h, m, sm) ==> #C.f(h, m, sm, this, x_1, ..., x_n) ==  ##C.f(partialHeap, this, x_1, ..., x_n))

       */

       val partialHeap = functionDependencies(pre, etran);

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

@@ -280,7 +280,7 @@ class Translator {
       Axiom(new Boogie.Forall(

         BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar(SecMaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),

         new Trigger(List(applyF, wellformed)),

-          (wellformed && IsGoodState(partialHeap) && CanAssumeFunctionDefs)

+          (wellformed && CanAssumeFunctionDefs)

           ==>

           (applyF ==@ applyFrameFunction))

       )

@@ -1959,7 +1959,6 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
       (if(e.isPredicate) Nil else List(bassume(TypeInformation(new Boogie.MapSelect(Heap, trE, memberName), e.f.typ.typ)))) :::

       InhalePermission(perm, trE, memberName, currentK, (if (transferToSecMask) SecMask else Mask)) :::

       bassume(AreGoodMasks(Mask, SecMask)) ::

-      bassume(IsGoodState(heapFragment(new Boogie.MapSelect(ih, trE, memberName)))) ::

       bassume(wf(Heap, Mask, SecMask)) ::

       bassume(wf(ih, Mask, SecMask))

     case acc @ AccessSeq(s, Some(member), perm) =>

@@ -2031,7 +2030,6 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
          bassert(nonNull(trE), holds.pos, "The target of the holds predicate might be null.")

        else Nil) :::

       bassume(AreGoodMasks(Mask, SecMask)) ::

-      bassume(IsGoodState(heapFragment(new Boogie.MapSelect(ih, trE, "held")))) ::

       bassume(wf(Heap, Mask, SecMask)) ::

       bassume(wf(ih, Mask, SecMask)) ::

       new Boogie.MapUpdate(Heap, trE, VarExpr("held"),

@@ -2041,7 +2039,6 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
       bassume(new Boogie.MapSelect(ih, trE, "mu") !=@ bLockBottom) ::

       bassume(wf(Heap, Mask, SecMask)) ::

       bassume(AreGoodMasks(Mask, SecMask)) ::

-      bassume(IsGoodState(heapFragment(new Boogie.MapSelect(ih, trE, "held")))) ::

       bassume(wf(Heap, Mask, SecMask)) ::

       bassume(wf(ih, Mask, SecMask))

     case Eval(h, e) => 

@@ -2761,7 +2758,6 @@ object TranslationHelper {
   def monitorK = "monitorK";

   def predicateK = "predicateK";

   def CurrentModule = VarExpr("CurrentModule");

-  def IsGoodState(e: Expr) = FunctionApp("IsGoodState", List(e));

   def dtype(e: Expr) = FunctionApp("dtype", List(e))

   def functionName(f: Function) = "#" + f.FullName;

   def className(cl: Class) = Boogie.VarExpr(cl.id + "#t")