patched ghost checking

3 files changed, 52 insertions, 2 deletions

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 907f7397..c407a7b9 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -474,6 +474,15 @@ namespace Microsoft.Boogie
             }

             if (errorCount > 0) return;

             this.VisitProgram(program);

+            foreach (Procedure proc in program.Procedures)

+            {

+                if (procToActionInfo.ContainsKey(proc)) continue;

+                foreach (var ie in proc.Modifies)

+                {

+                    if (!SharedVariables.Contains(ie.Decl)) continue;

+                    Error(proc, "A ghost procedure must not modify a global variable with layer annotation");

+                }

+            }

             if (errorCount > 0) return;

             YieldTypeChecker.PerformYieldSafeCheck(this);

             new LayerEraser().VisitProgram(program);

@@ -549,12 +558,24 @@ namespace Microsoft.Boogie
                 {

                     Error(node, "The callee is not available in the caller procedure");

                 }

+                return base.VisitCallCmd(node);

             }

             else

             {

-                Error(node, "Yielding procedure can call only a yielding procedure");

+                foreach (var ie in node.Outs)

+                {

+                    if (ghostVars.Contains(ie.Decl)) continue;

+                    Error(node, "The output of a ghost procedure must be assigned to a ghost variable");

+                }

+                bool savedCanAccessSharedVars = canAccessSharedVars;

+                bool savedCanAccessAuxVars = canAccessGhostVars;

+                canAccessSharedVars = true;

+                canAccessGhostVars = true;

+                var retVal = base.VisitCallCmd(node);

+                canAccessSharedVars = savedCanAccessSharedVars;

+                canAccessGhostVars = savedCanAccessAuxVars;

+                return retVal;

             }

-            return base.VisitCallCmd(node);

         }

 

         public override Cmd VisitParCallCmd(ParCallCmd node)

diff --git a/Test/og/ghost.bpl b/Test/og/ghost.bpl
new file mode 100644
index 00000000..ef40a232
--- /dev/null
+++ b/Test/og/ghost.bpl
@@ -0,0 +1,27 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0} x: int;
+
+procedure {:yields} {:layer 0,1} Incr();
+ensures {:right} |{ A: x := x + 1; return true; }|;
+
+procedure ghost(y: int) returns (z: int)
+requires y == 1;
+ensures z == 2;
+{
+  z := y + 1;
+}
+
+procedure {:yields} {:layer 1,2} Incr2() 
+ensures {:right} |{ A: x := x + 2; return true; }|;
+{
+  var {:ghost} a: int;
+  var {:ghost} b: int;
+
+  yield;
+  call a := ghost(1);
+  assert {:layer 1} a == 2;
+  par Incr() | Incr();
+  yield;
+}
+
diff --git a/Test/og/ghost.bpl.expect b/Test/og/ghost.bpl.expect
new file mode 100644
index 00000000..41374b00
--- /dev/null
+++ b/Test/og/ghost.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 2 verified, 0 errors