From c30399af4efff99373f901bd914e8b3d8bb811dc Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Thu, 5 Jul 2012 11:41:10 -0700
Subject: Dafny: disallow importing ghost modules into physical ones.

---
 Source/Dafny/DafnyAst.cs |  1 +
 Source/Dafny/Resolver.cs | 18 +++++++++++++++---
 2 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 709074f1..e6a693fa 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -844,6 +844,7 @@ namespace Microsoft.Dafny {
     public ModuleDefinition ModuleDef; // Note: this is null if this signature does not correspond to a specific definition (i.e.
                                        // it is abstract). Otherwise, it points to that definition.
     public ModuleSignature Refines;
+    public bool IsGhost = false;
     public ModuleSignature() {}
 
     public bool FindSubmodule(string name, out ModuleSignature pp) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 6f9d5dae..1463c4c0 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -227,7 +227,7 @@ namespace Microsoft.Dafny {
       // resolve
       var datatypeDependencies = new Graph<IndDatatypeDecl>();
       int prevErrorCount = ErrorCount;
-      ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);
+      ResolveTopLevelDecls_Signatures(m, m.TopLevelDecls, datatypeDependencies);
       if (ErrorCount == prevErrorCount)
         ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);
     }
@@ -373,6 +373,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(moduleDef != null);
       var sig = new ModuleSignature();
       sig.ModuleDef = moduleDef;
+      sig.IsGhost = moduleDef.IsGhost;
       List<TopLevelDecl> declarations = moduleDef.TopLevelDecls;
 
       foreach (TopLevelDecl d in declarations) {
@@ -806,7 +807,7 @@ namespace Microsoft.Dafny {
       }
       return i == Path.Count;
     }
-    public void ResolveTopLevelDecls_Signatures(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<IndDatatypeDecl/*!*/>/*!*/ datatypeDependencies) {
+    public void ResolveTopLevelDecls_Signatures(ModuleDefinition def, List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<IndDatatypeDecl/*!*/>/*!*/ datatypeDependencies) {
       Contract.Requires(declarations != null);
       Contract.Requires(datatypeDependencies != null);  // more expensive check: Contract.Requires(cce.NonNullElements(datatypeDependencies));
       foreach (TopLevelDecl d in declarations) {
@@ -818,7 +819,18 @@ namespace Microsoft.Dafny {
         } else if (d is ClassDecl) {
           ResolveClassMemberTypes((ClassDecl)d);
         } else if (d is ModuleDecl) {
-          // TODO: what goes here?
+          var decl = (ModuleDecl)d;
+          if (!def.IsGhost) {
+            if (decl.Signature.IsGhost) {
+              if (!(def.IsDefaultModule)) // _module is allowed to contain ghost modules, but not by ghost itself. Note this presents a challenge to 
+                                          // trusted verification, as toplevels can't be trusted if they invoke ghost module members.
+                Error(d.tok, "ghost modules can only be imported into other ghost modules, not physical ones.");
+            } else {
+              // physical modules are allowed everywhere
+            }
+          } else {
+            // everything is allowed in a ghost module
+          }
         } else {
           ResolveCtorTypes((DatatypeDecl)d, datatypeDependencies);
         }
-- 
cgit v1.2.3