Dafny: Ensures that function axioms are not being used while their consistency is being checked.

8 files changed, 162 insertions, 35 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 50433b54..253cfd12 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -207,6 +207,13 @@ function DtRank(DatatypeType) returns (int);
 

 // ---------------------------------------------------------------

 

+// used to make sure function axioms are not used while their consistency is being checked

+const $ModuleContextHeight: int;

+const $FunctionContextHeight: int;

+const $InMethodContext: bool;

+

+// ---------------------------------------------------------------

+

 type Field alpha;

 type HeapType = <alpha>[ref,Field alpha]alpha;

 

diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc
index 9963ac2d..96b756b9 100644
--- a/Source/Dafny/DafnyAst.ssc
+++ b/Source/Dafny/DafnyAst.ssc
@@ -341,6 +341,7 @@ namespace Microsoft.Dafny
     public readonly List<string!>! Imports;

     public readonly List<TopLevelDecl!>! TopLevelDecls = new List<TopLevelDecl!>();  // filled in by the parser; readonly after that

     public readonly Graph<MemberDecl!>! CallGraph = new Graph<MemberDecl!>();  // filled in during resolution

+    public int Height;  // height in the topological sorting of modules; filled in during resolution

     public ModuleDecl(Token! tok, string! name, [Captured] List<string!>! imports, Attributes attributes) {

       Imports = imports;

       base(tok, name, attributes);

diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc
index b3d5b2c3..4db4acbe 100644
--- a/Source/Dafny/Resolver.ssc
+++ b/Source/Dafny/Resolver.ssc
@@ -50,6 +50,7 @@ namespace Microsoft.Dafny {
       }

       // resolve imports and register top-level declarations

       foreach (ModuleDecl m in prog.Modules) {

+        importGraph.AddVertex(m);

         foreach (string imp in m.Imports) {

           ModuleDecl other;

           if (!modules.TryGetValue(imp, out other)) {

@@ -73,6 +74,15 @@ namespace Microsoft.Dafny {
           sep = " -> ";

         }

         Error(cycle[0], "import graph contains a cycle: {0}", cy);

+      } else {

+        // fill in module heights

+        List<ModuleDecl!> mm = importGraph.TopologicallySortedComponents();

+        assert mm.Count == prog.Modules.Count;  // follows from the fact that there are no cycles

+        int h = 0;

+        foreach (ModuleDecl m in mm) {

+          m.Height = h;

+          h++;

+        }

       }

       // resolve top-level declarations

       Graph<DatatypeDecl!> datatypeDependencies = new Graph<DatatypeDecl!>();

diff --git a/Source/Dafny/SccGraph.ssc b/Source/Dafny/SccGraph.ssc
index 6a7983a6..1ca7125b 100644
--- a/Source/Dafny/SccGraph.ssc
+++ b/Source/Dafny/SccGraph.ssc
@@ -8,8 +8,9 @@ namespace Microsoft.Dafny {
     class Vertex {

       public readonly Node N;

       public readonly List<Vertex!>! Successors = new List<Vertex!>();

-      public Vertex SccRepresentative;  // null if not computed or if the vertex represents itself

+      public Vertex SccRepresentative;  // null if not computed

       public List<Vertex!> SccMembers;  // non-null only for the representative of the SCC

+      public int SccId;  // valid only for SCC representatives; indicates position of this representative vertex in the graph's topological sort

       // the following field is used during the computation of SCCs and of reachability

       public VisitedStatus Visited;

       // the following fields are used during the computation of SCCs:

@@ -27,6 +28,15 @@ namespace Microsoft.Dafny {
     }

     Dictionary<Node, Vertex!>! vertices = new Dictionary<Node, Vertex!>();

     bool sccComputed = false;

+    List<Vertex!> topologicallySortedRepresentatives;  // computed by the SCC computation

+    invariant sccComputed ==> topologicallySortedRepresentatives != null;

+    public int SccCount {

+      get {

+        ComputeSCCs();

+        assert topologicallySortedRepresentatives != null;  // follows from postcondition of ComputeSCCs and the object invariant

+        return topologicallySortedRepresentatives.Count;

+      }

+    }

     int generation = 0;

     

     public Graph()

@@ -48,6 +58,14 @@ namespace Microsoft.Dafny {
       if (v == null) {

         v = new Vertex(n);

         vertices.Add(n, v);

+        if (sccComputed) {

+          assert topologicallySortedRepresentatives != null;  // follows from object invariant

+          v.SccRepresentative = v;

+          v.SccMembers = new List<Vertex!>();

+          v.SccMembers.Add(v);

+          v.SccId = topologicallySortedRepresentatives.Count;

+          topologicallySortedRepresentatives.Add(v);

+        }

       }

       return v;

     }

@@ -81,12 +99,38 @@ namespace Microsoft.Dafny {
     /// strongly connected component containing 'n'.

     /// </summary>

     public Node GetSCCRepresentative(Node n) {

+      return GetSCCRepr(n).N;

+    }

+    

+    /// <summary>

+    /// Idempotently adds 'n' as a vertex.  Then, returns the number of SCCs before the SCC of 'n' in the

+    /// topologically sorting of SCCs.

+    /// </summary>

+    public int GetSCCRepresentativeId(Node n) {

+      return GetSCCRepr(n).SccId;

+    }

+    

+    Vertex! GetSCCRepr(Node n) {

       Vertex v = GetVertex(n);

       ComputeSCCs();

-      return v.SccRepresentative == null ? n : v.SccRepresentative.N;

+      assert v.SccRepresentative != null;  // follows from what ComputeSCCs does

+      return v.SccRepresentative;

     }

     

     /// <summary>

+    /// Returns a list of the topologically sorted SCCs, each represented in the list by its representative node.

+    /// </summary>

+    public List<Node>! TopologicallySortedComponents() {

+      ComputeSCCs();

+      assert topologicallySortedRepresentatives != null;  // follows from object invariant

+      List<Node> nn = new List<Node>();

+      foreach (Vertex v in topologicallySortedRepresentatives) {

+        nn.Add(v.N);

+      }

+      return nn;

+    }

+

+    /// <summary>

     /// Idempotently adds 'n' as a vertex and then returns the set of Node's in the strongly connected component

     /// that contains 'n'.

     /// </summary>

@@ -94,15 +138,9 @@ namespace Microsoft.Dafny {
       Vertex v = GetVertex(n);

       ComputeSCCs();

       Vertex repr = v.SccRepresentative;

-      if (repr == null) {

-        // this is a node that has been added since the last time the SCCs were computed

-        repr = v;

-        v.SccRepresentative = v;

-        v.SccMembers = new List<Vertex!>();

-        v.SccMembers.Add(v);

-      }

+      assert repr != null && repr.SccMembers != null;  // follows from postcondition of ComputeSCCs

       List<Node> nn = new List<Node>();

-      foreach (Vertex w in (!)repr.SccMembers) {

+      foreach (Vertex w in repr.SccMembers) {

         nn.Add(w.N);

       }

       return nn;

@@ -115,10 +153,13 @@ namespace Microsoft.Dafny {
     /// As a side effect, this method may change the Visited, DfNumber, and LowLink fields

     /// of the vertices.

     /// </summary>

-    void ComputeSCCs() {

+    void ComputeSCCs()

+      ensures sccComputed;

+    {

       if (sccComputed) { return; }  // check if already computed

-      

+

       // reset all SCC information

+      topologicallySortedRepresentatives = new List<Vertex!>();

       foreach (Vertex v in vertices.Values) {

         v.Visited = VisitedStatus.Unvisited;

         v.SccMembers = null;

@@ -140,6 +181,7 @@ namespace Microsoft.Dafny {
     /// </summary>

     void SearchC(Vertex! v, Stack<Vertex!>! stack, ref int cnt)

       requires v.Visited == VisitedStatus.Unvisited;

+      requires topologicallySortedRepresentatives != null;

       ensures v.Visited != VisitedStatus.Unvisited;

     {

       v.DfNumber = cnt;

@@ -160,6 +202,8 @@ namespace Microsoft.Dafny {
       

       if (v.LowLink == v.DfNumber) {

         // The SCC containing 'v' has now been computed.

+        v.SccId = topologicallySortedRepresentatives.Count;

+        topologicallySortedRepresentatives.Add(v);

         v.SccMembers = new List<Vertex!>();

         while (true) {

           Vertex x = stack.Pop();

diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index 9bf4fd62..b5905bba 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -399,10 +399,14 @@ namespace Microsoft.Dafny {
       requires predef != null;

       requires specializationFormal == null <==> ctor == null;

       requires specializationFormal == null <==> specializationReplacementFormals == null;

+      requires f.EnclosingClass != null;

     {

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);

       

-      // axiom (forall $Heap, formals :: this != null && $IsHeap($Heap) && Pre($Heap,args) ==> f(args) == body)

+      // axiom

+      //   mh < ModuleContextHeight || (mh == ModuleContextHeight && (fh < FunctionContextHeight || InMethodContext))

+      //   ==>

+      //   (forall $Heap, formals :: this != null && $IsHeap($Heap) && Pre($Heap,args) ==> f(args) == body);

       //

       // The variables "formals" are the formals of function "f"; except, if a specialization is provided, then

       // "specializationFormal" (which is expected to be among the formals of "f") is excluded and replaced by

@@ -419,7 +423,6 @@ namespace Microsoft.Dafny {
       // allocation statement changes only an allocation bit and then re-assumes $IsGoodHeap; so if it is

       // sound after that, then it would also have been sound just before the allocation.

       //

-      // TODO: Add a CanAssumeFunctionDefs antecedent to this axiom (see Dafny lecture notes from Marktoberdorf 2008).

       Bpl.VariableSeq formals = new Bpl.VariableSeq();

       Bpl.ExprSeq args = new Bpl.ExprSeq();

       Bpl.BoundVariable bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));

@@ -460,11 +463,21 @@ namespace Microsoft.Dafny {
           args.Add(etran.TrExpr(r));

         }

       }

+

+      // mh < ModuleContextHeight || (mh == ModuleContextHeight && (fh < FunctionContextHeight || InMethodContext))

+      ModuleDecl m = f.EnclosingClass.Module;

+      Bpl.Expr activate = Bpl.Expr.Or(

+        Bpl.Expr.Lt(Bpl.Expr.Literal(m.Height), etran.ModuleContextHeight()),

+        Bpl.Expr.And(

+          Bpl.Expr.Eq(Bpl.Expr.Literal(m.Height), etran.ModuleContextHeight()),

+          Bpl.Expr.Or(

+            Bpl.Expr.Lt(Bpl.Expr.Literal(m.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()),

+            etran.InMethodContext())));

       

       Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);

       if (!f.IsStatic) {

         assert bvThisIdExpr != null;  // set to non-null value above when !f.IsStatic

-        ante = Bpl.Expr.And(Bpl.Expr.Neq(bvThisIdExpr, predef.Null), ante);

+        ante = Bpl.Expr.And(ante, Bpl.Expr.Neq(bvThisIdExpr, predef.Null));

       }

       foreach (Expression req in f.Req) {

         ante = Bpl.Expr.And(ante, etran.TrExpr(req));

@@ -480,7 +493,7 @@ namespace Microsoft.Dafny {
         body = Substitute(body, null, substMap);

       }

       Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, Bpl.Expr.Eq(funcAppl, etran.AltFunctions.TrExpr(body))));

-      return new Bpl.Axiom(f.tok, ax);

+      return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax));

     }

     

     void AddUseAxioms(Function! f)

@@ -930,6 +943,7 @@ namespace Microsoft.Dafny {
     

     void AddWellformednessCheck(Function! f)

       requires sink != null && predef != null;

+      requires f.EnclosingClass != null;

     {

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);

       // parameters of the procedure

@@ -937,7 +951,7 @@ namespace Microsoft.Dafny {
       if (!f.IsStatic) {

         Bpl.Expr wh = Bpl.Expr.And(

           Bpl.Expr.Neq(new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), predef.Null),

-          etran.GoodRef(f.tok, new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), Resolver.GetThisType(f.tok, (!)f.EnclosingClass)));

+          etran.GoodRef(f.tok, new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), Resolver.GetThisType(f.tok, f.EnclosingClass)));

         Bpl.Formal thVar = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType, wh), true);

         inParams.Add(thVar);

       }

@@ -948,8 +962,15 @@ namespace Microsoft.Dafny {
       }

       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);

       // the procedure itself

+      Bpl.RequiresSeq req = new Bpl.RequiresSeq();

+      // free requires mh < ModuleContextHeight || (mh == ModuleContextHeight && fh < FunctionContextHeight);

+      ModuleDecl m = f.EnclosingClass.Module;

+      Bpl.Expr context = Bpl.Expr.And(

+        Bpl.Expr.Eq(Bpl.Expr.Literal(m.Height), etran.ModuleContextHeight()),

+        Bpl.Expr.Eq(Bpl.Expr.Literal(m.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()));

+      req.Add(Requires(f.tok, true, context, null, null));

       Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullName, typeParams, inParams, new Bpl.VariableSeq(),

-        new Bpl.RequiresSeq(), new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq());

+        req, new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq());

       sink.TopLevelDeclarations.Add(proc);

 

       Bpl.VariableSeq locals = new Bpl.VariableSeq();

@@ -1452,6 +1473,7 @@ namespace Microsoft.Dafny {
     /// </summary>    

     Bpl.Procedure! AddMethod(Method! m, bool wellformednessProc)

       requires predef != null && sink != null;

+      requires m.EnclosingClass != null;

     {

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);

       

@@ -1460,7 +1482,7 @@ namespace Microsoft.Dafny {
       if (!m.IsStatic) {

         Bpl.Expr wh = Bpl.Expr.And(

           Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), predef.Null),

-          etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), Resolver.GetThisType(m.tok, (!)m.EnclosingClass)));

+          etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), Resolver.GetThisType(m.tok, m.EnclosingClass)));

         Bpl.Formal thVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, "this", predef.RefType, wh), true);

         inParams.Add(thVar);

       }

@@ -1478,6 +1500,11 @@ namespace Microsoft.Dafny {
       Bpl.RequiresSeq req = new Bpl.RequiresSeq();

       Bpl.IdentifierExprSeq mod = new Bpl.IdentifierExprSeq();

       Bpl.EnsuresSeq ens = new Bpl.EnsuresSeq();

+      // free requires mh == ModuleContextHeight && InMethodContext;

+      Bpl.Expr context = Bpl.Expr.And(

+        Bpl.Expr.Eq(Bpl.Expr.Literal(m.EnclosingClass.Module.Height), etran.ModuleContextHeight()),

+        etran.InMethodContext());

+      req.Add(Requires(m.tok, true, context, null, null));

       mod.Add(etran.HeapExpr);

       mod.Add(Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int));

       

@@ -2488,6 +2515,24 @@ namespace Microsoft.Dafny {
         Bpl.Type ty = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(predef.RefType), Bpl.Type.Bool);

         return new Bpl.IdentifierExpr(tok, "$_Frame", ty);

       }

+      

+      public Bpl.IdentifierExpr! ModuleContextHeight()

+        ensures result.Type != null;

+      {

+        return new Bpl.IdentifierExpr(Token.NoToken, "$ModuleContextHeight", Bpl.Type.Int);

+      }

+

+      public Bpl.IdentifierExpr! FunctionContextHeight()

+        ensures result.Type != null;

+      {

+        return new Bpl.IdentifierExpr(Token.NoToken, "$FunctionContextHeight", Bpl.Type.Int);

+      }

+

+      public Bpl.IdentifierExpr! InMethodContext()

+        ensures result.Type != null;

+      {

+        return new Bpl.IdentifierExpr(Token.NoToken, "$InMethodContext", Bpl.Type.Bool);

+      }

 

       public Bpl.Expr! TrExpr(Expression! expr)

         requires predef != null;

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index ae2aa454..f77d2fd4 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -12,23 +12,23 @@ class MyClass<T, U> {
     ensures t == t;

     ensures old(null) != this;

   {

-      x := 12;

-      while (x < 100)

-        invariant x <= 100;

-      {

-        x := x + 17;

-        if (x % 20 == 3) {

-          x := this.x + 1;

-        } else {

-          this.x := x + 0;

-        }

-        call t, u, v := M(true, lotsaObjects)

-        var to: MyClass<T,U>;

-        call to, u, v := M(true, lotsaObjects)

-        call to, u, v := to.M(true, lotsaObjects)

-        assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];

+    x := 12;

+    while (x < 100)

+      invariant x <= 100;

+    {

+      x := x + 17;

+      if (x % 20 == 3) {

+        x := this.x + 1;

+      } else {

+        this.x := x + 0;

       }

+      call t, u, v := M(true, lotsaObjects)

+      var to: MyClass<T,U>;

+      call to, u, v := M(true, lotsaObjects)

+      call to, u, v := to.M(true, lotsaObjects)

+      assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];

     }

+  }

 

   function F(x: int, y: int, h: WildData, k: WildData): WildData

   {

@@ -285,6 +285,13 @@ Execution trace:
 

 Dafny program verifier finished with 16 verified, 2 errors

 

+-------------------- BadFunction.dfy --------------------

+BadFunction.dfy(6,3): Error: failure to decrease termination measure

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 2 verified, 1 error

+

 -------------------- Queue.dfy --------------------

 

 Dafny program verifier finished with 22 verified, 0 errors

diff --git a/Test/dafny0/BadFunction.dfy b/Test/dafny0/BadFunction.dfy
new file mode 100644
index 00000000..3affaa80
--- /dev/null
+++ b/Test/dafny0/BadFunction.dfy
@@ -0,0 +1,13 @@
+// The following function gives rise to an inconsistent axiom, except

+// for its CanUseFunctionDefs antecedent, which saves the day.

+function F(x: int): int

+  decreases x;

+{

+  F(x) + 1  // error: does not decrease termination metric

+}

+

+method M()

+{

+  assert F(5) == 0;  // no error is generated here, because of the inconsistent axiom

+  assert false;  // ditto

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 003566f3..d72b0899 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -18,7 +18,7 @@ for %%f in (BQueue.bpl) do (
 )

 

 for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy

-            Modules0.dfy Modules1.dfy Queue.dfy ListCopy.dfy

+            Modules0.dfy Modules1.dfy BadFunction.dfy Queue.dfy ListCopy.dfy

             BinaryTree.dfy ListReverse.dfy ListContents.dfy

             SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy