Automatic merge.

9 files changed, 88 insertions, 11 deletions

diff --git a/Chalice/src/main/scala/Prelude.scala b/Chalice/src/main/scala/Prelude.scala
index 857e6624..a3c7367b 100644
--- a/Chalice/src/main/scala/Prelude.scala
+++ b/Chalice/src/main/scala/Prelude.scala
@@ -140,15 +140,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/Resolver.scala b/Chalice/src/main/scala/Resolver.scala
index e802b7e7..dda5d989 100644
--- a/Chalice/src/main/scala/Resolver.scala
+++ b/Chalice/src/main/scala/Resolver.scala
@@ -232,6 +232,7 @@ object Resolver {
              if (!e.typ.IsBool) context.Error(c.pos, "where clause requires a boolean expression (found " + e.typ.FullName + ")")

            case p@Predicate(id, e) =>

              var ctx = context;

+             if (ContainsWaitlevel(e)) context.Error(e.pos, "predicate body is not allowed to mention 'waitlevel'")

              ResolveExpr(e, ctx, false, true)(true);

              if(!e.typ.IsBool) context.Error(e.pos, "predicate requires a boolean expression (found " + e.typ.FullName + ")")

            case f@Function(id, ins, out, spec, definition) =>

@@ -862,6 +863,18 @@ object Resolver {
    )

    x

  }

+ 

+ // does e contain 'waitlevel'?

+ def ContainsWaitlevel(expr: Expression): Boolean = {

+   var x: Boolean = false

+   AST.visit(expr,

+     e => e match {

+       case _:MaxLockLiteral => x = true

+       case _ =>

+     }

+   )

+   x

+ }

 

  // ResolveExpr resolves all parts of an RValue, if possible, and (always) sets the RValue's typ field

  def ResolveExpr(e: RValue, context: ProgramContext,

diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index bd94c71e..51c03b02 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))

       )

@@ -1973,7 +1973,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) =>

@@ -2045,7 +2044,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"),

@@ -2055,7 +2053,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) => 

@@ -2081,7 +2078,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
       bassume(preEtran.Heap ==@ evalHeap) ::

       bassume(submask(preEtran.Mask, evalMask))

     case uf@Unfolding(acc@Access(pred@MemberAccess(obj, f), perm), ufexpr) =>

-	  if (transferToSecMask) throw new NotSupportedException("not yet implemented")

+	  if (transferToSecMask) return Nil

       // handle unfolding like the next case, but also record permissions of the predicate

       // in the secondary mask and track the predicate in the auxilary information

       val (receiverV, receiver) = Boogie.NewBVar("predRec", tref, true)

@@ -2826,7 +2823,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")

diff --git a/Chalice/tests/examples/list-reverse.chalice b/Chalice/tests/examples/list-reverse.chalice
new file mode 100644
index 00000000..c694b4c9
--- /dev/null
+++ b/Chalice/tests/examples/list-reverse.chalice
@@ -0,0 +1,44 @@
+class Node {

+  var next : Node;

+  var val : int;

+

+  predicate list {

+    acc(next) && acc(val) && (next!=null ==> next.list)

+  }

+  

+  function vals() : seq<int>

+    requires list

+  {

+    unfolding list in (next == null ? [val] : [val] ++ next.vals())

+  }

+

+  function reverse_vals() : seq<int>

+    requires list

+  {

+    unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])

+  }

+

+  method reverse_in_place() returns (r:Node)

+    requires list;

+    ensures r != null && r.list;

+    ensures r.vals() == old(this.reverse_vals());

+  {

+    var l : Node := this;

+    r := null;

+

+    while (l != null) 

+      invariant l!=null ==> l.list;

+      invariant r!=null ==> r.list;

+      invariant old(this.reverse_vals()) == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());

+    { 

+      var y: Node;

+      unfold l.list;

+    

+      y := l.next;

+      l.next := r;

+      r := l;

+      fold r.list;

+      l := y;

+    }

+  }

+}
\ No newline at end of file
diff --git a/Chalice/tests/examples/list-reverse.output.txt b/Chalice/tests/examples/list-reverse.output.txt
new file mode 100644
index 00000000..d8e19122
--- /dev/null
+++ b/Chalice/tests/examples/list-reverse.output.txt
@@ -0,0 +1,4 @@
+Verification of list-reverse.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/regressions/workitem-10222.chalice b/Chalice/tests/regressions/workitem-10222.chalice
new file mode 100644
index 00000000..a01253c9
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10222.chalice
@@ -0,0 +1,8 @@
+class Test {
+    var t: Test;
+    
+    // previously, mentioning "waitlevel" in a predicate did not cause an error
+    predicate inv {
+        acc(t) && acc(t.mu) && t.mu << waitlevel
+    }
+}
diff --git a/Chalice/tests/regressions/workitem-10222.output.txt b/Chalice/tests/regressions/workitem-10222.output.txt
new file mode 100644
index 00000000..eac18363
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10222.output.txt
@@ -0,0 +1,4 @@
+Verification of workitem-10222.chalice using parameters="" 

+

+The program did not typecheck.

+6.9: predicate body is not allowed to mention 'waitlevel'

diff --git a/Chalice/tests/regressions/workitem-10223.chalice b/Chalice/tests/regressions/workitem-10223.chalice
new file mode 100644
index 00000000..eb4bd00b
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10223.chalice
@@ -0,0 +1,8 @@
+class Lala {
+    var next: Lala;
+    var x: int;
+    predicate inv {
+        acc(next) && acc(x) &&
+        (next != null ==> (next.inv && unfolding next.inv in this.x > next.x))
+    }
+}
diff --git a/Chalice/tests/regressions/workitem-10223.output.txt b/Chalice/tests/regressions/workitem-10223.output.txt
new file mode 100644
index 00000000..f4bfd78d
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10223.output.txt
@@ -0,0 +1,4 @@
+Verification of workitem-10223.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.