Make functions and predicates be opaque outside the defining module -- only their specifications (e.g., ensures clauses) are exported.

7 files changed, 264 insertions, 42 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 5d2daa39..bf069ea6 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1164,34 +1164,36 @@ namespace Microsoft.Dafny {
         foreach (var p in iter.Requires) {

           if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {

             req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));

+            comment = null;

           } else {

             bool splitHappened;  // we actually don't care

-            foreach (var s in TrSplitExpr(p.E, etran, out splitHappened)) {

+            foreach (var s in TrSplitExpr(p.E, etran, kind == MethodTranslationKind.InterModuleCall ? 0 : int.MaxValue, out splitHappened)) {

               if (kind == MethodTranslationKind.IntraModuleCall && RefinementToken.IsInherited(s.E.tok, currentModule)) {

                 // this precondition was inherited into this module, so just ignore it

               } else {

-                req.Add(Requires(s.E.tok, s.IsOnlyFree, s.E, null, null));

+                req.Add(Requires(s.E.tok, s.IsOnlyFree, s.E, null, comment));

+                comment = null;

                 // the free here is not linked to the free on the original expression (this is free things generated in the splitting.)

               }

             }

           }

-          comment = null;

         }

         comment = "user-defined postconditions";

         foreach (var p in iter.Ensures) {

           if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {

             ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));

+            comment = null;

           } else {

             bool splitHappened;  // we actually don't care

-            foreach (var s in TrSplitExpr(p.E, etran, out splitHappened)) {

+            foreach (var s in TrSplitExpr(p.E, etran, kind == MethodTranslationKind.InterModuleCall ? 0 : int.MaxValue, out splitHappened)) {

               if (kind == MethodTranslationKind.Implementation && RefinementToken.IsInherited(s.E.tok, currentModule)) {

                 // this postcondition was inherited into this module, so just ignore it

               } else {

-                ens.Add(Ensures(s.E.tok, s.IsOnlyFree, s.E, null, null));

+                ens.Add(Ensures(s.E.tok, s.IsOnlyFree, s.E, null, comment));

+                comment = null;

               }

             }

           }

-          comment = null;

         }

         foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(iter.tok, iter.Modifies.Expressions, false, etran.Old, etran, etran.Old)) {

           ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));

@@ -1505,7 +1507,7 @@ namespace Microsoft.Dafny {
 

     void AddFunctionAxiom(Function/*!*/ f, Expression body, List<Expression/*!*/>/*!*/ ens, Specialization specialization, int layerOffset) {

       var vs = new List<FunctionAxiomVisibility>();

-      if (f is Predicate || f is CoPredicate) {

+      if (f is Function || f is Predicate || f is CoPredicate) {

         vs.Add(FunctionAxiomVisibility.IntraModuleOnly);

         vs.Add(FunctionAxiomVisibility.ForeignModuleOnly);

       } else {

@@ -1564,8 +1566,8 @@ namespace Microsoft.Dafny {
       //         $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&

       //         Pre($Heap,args))

       //       ==>

-      //       body-can-make-its-calls &&                         // generated only for layerOffset==0

-      //       f(args) == body &&                                                                         // (d)

+      //       body-can-make-its-calls &&                         // generated only for layerOffset==0    // (d)

+      //       f(args) == body &&                                                                         // (e)

       //       ens &&                                             // generated only for layerOffset==0

       //       f(args)-has-the-expected-type);                    // generated only for layerOffset==0

       //

@@ -1583,8 +1585,8 @@ namespace Microsoft.Dafny {
       //

       // Visibility:  The above description is for visibility==All.  If visibility==IntraModuleOnly, then

       // disjunct (a) is dropped (which also has a simplifying effect on (c)).  Finally, if visibility==ForeignModuleOnly,

-      // then disjunct (b) is dropped (which also has a simplify effect on(c)); furthermore, if f is a Predicate,

-      // then the equality in (d) is replaced by an implication.

+      // then disjunct (b) is dropped (which also has a simplify effect on(c)); also, if the definition is not

+      // publicly exported (which is a feature that is not currently supported in dafny), then (d) and (e) are dropped.

       //

       // Note, an antecedent $Heap[this,alloc] is intentionally left out:  including it would only weaken

       // the axiom.  Moreover, leaving it out does not introduce any soundness problem, because the Dafny

@@ -1716,6 +1718,8 @@ namespace Microsoft.Dafny {
       }

       if (body == null) {

         meat = Bpl.Expr.True;

+      } else if (visibility == FunctionAxiomVisibility.ForeignModuleOnly /* TODO: add 'public' feature and add: && !IsPublic(f) */) {

+        meat = Bpl.Expr.True;

       } else {

         var bodyWithSubst = Substitute(body, null, substMap);

         if (f is PrefixPredicate) {

@@ -1723,15 +1727,10 @@ namespace Microsoft.Dafny {
           bodyWithSubst = PrefixSubstitution(pp, bodyWithSubst);

         }

         if (layerOffset == 0) {

-          meat = Bpl.Expr.And(

-            CanCallAssumption(bodyWithSubst, etran),

-            visibility == FunctionAxiomVisibility.ForeignModuleOnly && (f is Predicate || f is CoPredicate) ?

-              Bpl.Expr.Imp(funcAppl, etranLimited.TrExpr(bodyWithSubst)) :

-              Bpl.Expr.Eq(funcAppl, etranLimited.TrExpr(bodyWithSubst)));

+          meat = BplAnd(CanCallAssumption(bodyWithSubst, etran),

+            Bpl.Expr.Eq(funcAppl, etranLimited.TrExpr(bodyWithSubst)));

         } else {

-          meat = visibility == FunctionAxiomVisibility.ForeignModuleOnly && (f is Predicate || f is CoPredicate) ?

-            Bpl.Expr.Imp(funcAppl, etran.TrExpr(bodyWithSubst)) :

-            Bpl.Expr.Eq(funcAppl, etran.TrExpr(bodyWithSubst));

+          meat = Bpl.Expr.Eq(funcAppl, etran.TrExpr(bodyWithSubst));

         }

       }

       if (layerOffset == 0 && lits==null) {

@@ -4185,36 +4184,37 @@ namespace Microsoft.Dafny {
         foreach (var p in m.Req) {

           if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {

             req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));

+            comment = null;

           } else {

             bool splitHappened;  // we actually don't care

-            foreach (var s in TrSplitExpr(p.E, etran, out splitHappened)) {

+            foreach (var s in TrSplitExpr(p.E, etran, kind == MethodTranslationKind.InterModuleCall ? 0 : int.MaxValue, out splitHappened)) {

               if ((kind == MethodTranslationKind.IntraModuleCall || kind == MethodTranslationKind.CoCall) && RefinementToken.IsInherited(s.E.tok, currentModule)) {

                 // this precondition was inherited into this module, so just ignore it

               } else {

-                req.Add(Requires(s.E.tok, s.IsOnlyFree, s.E, null, null));

+                req.Add(Requires(s.E.tok, s.IsOnlyFree, s.E, null, comment));

+                comment = null;

                 // the free here is not linked to the free on the original expression (this is free things generated in the splitting.)

               }

             }

           }

-          comment = null;

         }

         comment = "user-defined postconditions";

         foreach (var p in m.Ens) {

           if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {

             ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));

+            comment = null;

           } else {

-            var ss = new List<SplitExprInfo>();

-            var splitHappened/*we actually don't care*/ = TrSplitExpr(p.E, ss, true, int.MaxValue, etran);

-            foreach (var s in ss) {

+            bool splitHappened;  // we actually don't care

+            foreach (var s in TrSplitExpr(p.E, etran, kind == MethodTranslationKind.InterModuleCall ? 0 : int.MaxValue, out splitHappened)) {

               var post = s.E;

               if (kind == MethodTranslationKind.Implementation && RefinementToken.IsInherited(s.E.tok, currentModule)) {

                 // this postcondition was inherited into this module, so make it into the form "$_reverifyPost ==> s.E"

                 post = Bpl.Expr.Imp(new Bpl.IdentifierExpr(s.E.tok, "$_reverifyPost", Bpl.Type.Bool), post);

               }

-              ens.Add(Ensures(s.E.tok, s.IsOnlyFree, post, null, null));

+              ens.Add(Ensures(s.E.tok, s.IsOnlyFree, post, null, comment));

+              comment = null;

             }

           }

-          comment = null;

         }

         foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, etran.Old, etran, etran.Old)) {

           ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));

@@ -6330,6 +6330,14 @@ namespace Microsoft.Dafny {
 

       // Make the call

       Bpl.CallCmd call = new Bpl.CallCmd(tok, MethodName(callee, kind), ins, outs);

+      if (module != currentModule && tok is RefinementToken && (codeContext == null || !codeContext.MustReverify)) {

+        // we're calling a method defined in a different module and the call statement is inherited; this means that the precondition

+        // of the call has already been checked in the refined module, and the precondition has not changed (if the precondition

+        // involves a predicate, the predicate would have been treated as opaque in the inherited call, so the inherited module would

+        // have had to have checked the call precondition for all possible definitions of the predicate).  Hence, we don't need to

+        // re-check the precondition of the call here.

+        call.IsFree = true;

+      }

       builder.Add(call);

 

       // Unbox results as needed

@@ -9407,10 +9415,22 @@ namespace Microsoft.Dafny {
       return splits;

     }

 

+    List<SplitExprInfo/*!*/>/*!*/ TrSplitExpr(Expression expr, ExpressionTranslator etran, int heightLimit, out bool splitHappened)

+    {

+      Contract.Requires(expr != null);

+      Contract.Requires(etran != null);

+      Contract.Ensures(Contract.Result<List<SplitExprInfo>>() != null);

+

+      var splits = new List<SplitExprInfo>();

+      splitHappened = TrSplitExpr(expr, splits, true, heightLimit, etran);

+      return splits;

+    }

+

     /// <summary>

     /// Tries to split the expression into tactical conjuncts (if "position") or disjuncts (if "!position").

     /// If a (necessarily boolean) function call appears as a top-level conjunct, then inline the function if

-    /// if it declared in the current module and its height is less than "heightLimit".

+    /// if it declared in the current module and its height is less than "heightLimit" (if "heightLimit" is

+    /// passed in as 0, then no functions will be inlined).

     /// </summary>

     bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool position, int heightLimit, ExpressionTranslator etran) {

       Contract.Requires(expr != null);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index c1e04f2a..da6d1caa 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -624,15 +624,15 @@ Modules0.dfy(97,14): Error: Undeclared top-level type or type parameter: MyClass
 28 resolution/type errors detected in Modules0.dfy

 

 -------------------- Modules1.dfy --------------------

-Modules1.dfy(75,16): Error: assertion violation

+Modules1.dfy(76,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-Modules1.dfy(88,16): Error: assertion violation

+Modules1.dfy(89,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-Modules1.dfy(90,14): Error: assertion violation

+Modules1.dfy(91,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

@@ -1557,6 +1557,80 @@ Execution trace:
 

 Dafny program verifier finished with 9 verified, 1 error

 

+-------------------- OpaqueFunctions.dfy --------------------

+OpaqueFunctions.dfy(24,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+OpaqueFunctions.dfy(49,7): Error BP5002: A precondition for this call might not hold.

+OpaqueFunctions.dfy(21,16): Related location: This is the precondition that might not hold.

+Execution trace:

+    (0,0): anon0

+OpaqueFunctions.dfy(55,20): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+OpaqueFunctions.dfy(57,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+OpaqueFunctions.dfy(60,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Then

+OpaqueFunctions.dfy(63,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+OpaqueFunctions.dfy(74,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+OpaqueFunctions.dfy(76,9): Error BP5002: A precondition for this call might not hold.

+OpaqueFunctions.dfy[A'](21,16): Related location: This is the precondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+OpaqueFunctions.dfy(83,20): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+OpaqueFunctions.dfy(85,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+OpaqueFunctions.dfy(88,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Then

+OpaqueFunctions.dfy(91,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+OpaqueFunctions.dfy(102,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+OpaqueFunctions.dfy(104,9): Error BP5002: A precondition for this call might not hold.

+OpaqueFunctions.dfy[A'](21,16): Related location: This is the precondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+OpaqueFunctions.dfy(111,20): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+OpaqueFunctions.dfy(113,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+OpaqueFunctions.dfy(116,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Then

+OpaqueFunctions.dfy(119,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+

+Dafny program verifier finished with 32 verified, 18 errors

+

 -------------------- Maps.dfy --------------------

 Maps.dfy(76,8): Error: element may not be in domain

 Execution trace:

diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index 1f47f3b1..e9c432f3 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -64,6 +64,7 @@ method Botch1(x: int)
 module A_Visibility {

   class C {

     static predicate P(x: int)

+      ensures P(x) ==> -10 <= x;

     {

       0 <= x

     }

@@ -84,8 +85,8 @@ module B_Visibility {
   method Main() {

     var y;

     if (A.C.P(y)) {

-      assert 0 <= y;  // this much is known of C.P

-      assert 2 <= y;  // error

+      assert -10 <= y;  // this much is known of C.P

+      assert 0 <= y;  // error

     } else {

       assert A.C.P(8);  // error: C.P cannot be established outside the declaring module

     }

diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy
new file mode 100644
index 00000000..c15515d2
--- /dev/null
+++ b/Test/dafny0/OpaqueFunctions.dfy
@@ -0,0 +1,123 @@
+module A {

+  class C {

+    var x: int;

+    predicate Valid()

+      reads this;

+    {

+      0 <= x

+    }

+    function Get(): int

+      reads this;

+    {

+      x

+    }

+    constructor ()

+      modifies this;

+      ensures Valid();

+    {

+      x := 8;

+    }

+    method M()

+      requires Valid();

+    {

+      assert Get() == x;

+      assert x == 8;  // error

+    }

+  }

+}

+module A' refines A {

+  class C {

+    predicate Valid...

+    {

+      x == 8

+    }

+    method N()

+      requires Valid();

+    {

+      assert Get() == x;

+      assert x == 8;

+    }

+  }

+}

+

+module B {

+  import X as A

+  method Main() {

+    var c := new X.C();

+    c.M();  // fine

+    c.x := c.x + 1;

+    c.M();  // error, because Valid() is opaque

+  }

+  method L(c: X.C)

+    requires c != null;

+    modifies c;

+  {

+    assert c.Get() == c.x;  // error because Get() s opaque

+    if * {

+      assert c.Valid();  // error, because Valid() is opaque

+    } else if * {

+      c.x := 7;

+      assert c.Valid();  // error, because Valid() is opaque

+    } else {

+      c.x := 8;

+      assert c.Valid();  // error, because Valid() is opaque

+    }

+  }

+}

+module B_direct {

+  import X as A'

+  method Main() {

+    var c := new X.C();

+    c.M();  // fine

+    c.x := c.x + 1;

+    if * {

+      assert c.Valid();  // error, because Valid() is opaque

+    } else {

+      c.M();  // error, because Valid() is opaque

+    }

+  }

+  method L(c: X.C)

+    requires c != null;

+    modifies c;

+  {

+    assert c.Get() == c.x;  // error because Get() s opaque

+    if * {

+      assert c.Valid();  // error, because Valid() is opaque

+    } else if * {

+      c.x := 7;

+      assert c.Valid();  // error, because Valid() is opaque

+    } else {

+      c.x := 8;

+      assert c.Valid();  // error, because Valid() is opaque

+    }

+  }

+}

+module B' refines B {

+  import X = A'  // this by itself produces no more error

+  method Main'() {

+    var c := new X.C();

+    c.M();  // fine

+    c.x := c.x + 1;

+    if * {

+      assert c.Valid();  // error, because Valid() is opaque

+    } else {

+      c.M();  // error, because Valid() is opaque

+    }

+  }

+  method L'(c: X.C)

+    requires c != null;

+    modifies c;

+  {

+    assert c.Get() == c.x;  // error because Get() s opaque

+    if * {

+      assert c.Valid();  // error, because Valid() is opaque

+    } else if * {

+      c.x := 7;

+      assert c.Valid();  // error, because Valid() is opaque

+    } else {

+      c.x := 8;

+      assert c.Valid();  // error, because Valid() is opaque

+    }

+  }

+}

+

diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index 1610d8b8..d48b1a6a 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -130,7 +130,7 @@ module Tricky_Full refines Tricky_Base {
   class Tree {

     predicate Valid()

     {

-      Constrained  // this causes an error to be generated for the inherited Init

+      Constrained()  // this causes an error to be generated for the inherited Init

     }

   }

 }

diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index e5c06a5e..3c7563a0 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -101,7 +101,7 @@ module Abstract {
   class MyNumber {
     ghost var N: int;
     ghost var Repr: set<object>;
-    predicate Valid
+    predicate Valid()
       reads this, Repr;
     {
       this in Repr && null !in Repr
@@ -109,20 +109,20 @@ module Abstract {
     constructor Init()
       modifies this;
       ensures N == 0;
-      ensures Valid && fresh(Repr - {this});
+      ensures Valid() && fresh(Repr - {this});
     {
       N, Repr := 0, {this};
     }
     method Inc()
-      requires Valid;
+      requires Valid();
       modifies Repr;
       ensures N == old(N) + 1;
-      ensures Valid && fresh(Repr - old(Repr));
+      ensures Valid() && fresh(Repr - old(Repr));
     {
       N := N + 1;
     }
     method Get() returns (n: int)
-      requires Valid;
+      requires Valid();
       ensures n == N;
     {
       var k;  assume k == N;
@@ -135,7 +135,7 @@ module Concrete refines Abstract {
   class MyNumber {
     var a: int;
     var b: int;
-    predicate Valid
+    predicate Valid()
     {
       N == a - b
     }
@@ -172,7 +172,7 @@ module IncorrectConcrete refines Abstract {
   class MyNumber {
     var a: int;
     var b: int;
-    predicate Valid
+    predicate Valid()
     {
       N == 2*a - b
     }
@@ -191,3 +191,6 @@ module IncorrectConcrete refines Abstract {
     }
   }
 }
+
+// ------------- visibility checks -------------------------------
+
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 18f34345..b911625b 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -23,7 +23,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy Definedness.dfy
             LoopModifies.dfy Refinement.dfy RefinementErrors.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy

-            Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy

+            Predicates.dfy Skeletons.dfy OpaqueFunctions.dfy

+            Maps.dfy LiberalEquality.dfy

             RefinementModificationChecking.dfy TailCalls.dfy

             Calculations.dfy IteratorResolution.dfy Iterators.dfy

             RankPos.dfy RankNeg.dfy