combine {:autocontracts} and refinement

1 files changed, 62 insertions, 56 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index c95be2f4..f248fae2 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -90,6 +90,11 @@ namespace Microsoft.Dafny
       foreach (var member in cl.Members) {

         bool sayYes = true;

         if (Attributes.ContainsBool(member.Attributes, "autocontracts", ref sayYes) && !sayYes) {

+          // the user has excluded this member

+          continue;

+        }

+        if (member.RefinementBase != null) {

+          // member is inherited from a module where it was already processed

           continue;

         }

         Boogie.IToken tok = new AutoGeneratedToken(member.tok);

@@ -188,17 +193,24 @@ namespace Microsoft.Dafny
         if (member is Function && member.Name == "Valid" && !member.IsStatic) {

           var valid = (Function)member;

           if (valid.IsGhost && valid.ResultType is BoolType) {

-            var c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, self, Repr);  // this in Repr

-            var c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NotInSet, cNull, Repr);  // null !in Repr

-            var c = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c0, c1);

+            Expression c;

+            if (valid.RefinementBase == null) {

+              var c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, self, Repr);  // this in Repr

+              var c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NotInSet, cNull, Repr);  // null !in Repr

+              c = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c0, c1);

+            } else {

+              c = new LiteralExpr(tok, true);

+              c.Type = Type.Bool;

+            }

 

             foreach (var ff in subobjects) {

-              var F = new FieldSelectExpr(tok, implicitSelf, ff.Item1.Name);

-              F.Field = ff.Item1;

-              F.Type = ff.Item1.Type;

-

-              c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NeqCommon, F, cNull);

-              c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, F, Repr);

+              if (ff.Item1.RefinementBase != null) {

+                // the field has been inherited from a refined module, so don't include it here

+                continue;

+              }

+              var F = Resolver.NewFieldSelectExpr(tok, implicitSelf, ff.Item1, null);

+              var c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NeqCommon, F, cNull);

+              var c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, F, Repr);

               if (ff.Item2 == null) {

                 // F != null ==> F in Repr  (so, nothing else to do)

               } else {

@@ -222,46 +234,44 @@ namespace Microsoft.Dafny
 

         } else if (member is Constructor) {

           var ctor = (Constructor)member;

-          if (ctor.Body == null) {

-            ctor.Body = new BlockStmt(tok, new List<Statement>());

-          }

-          // TODO: these assignments should be included on every return path

-          var bodyStatements = ((BlockStmt)ctor.Body).Body;

-          // Repr := {this};

-          var e = new SetDisplayExpr(tok, new List<Expression>() { self });

-          e.Type = new SetType(new ObjectType());

-          Statement s = new AssignStmt(tok, Repr, new ExprRhs(e));

-          s.IsGhost = true;

-          bodyStatements.Add(s);

+          if (ctor.Body != null) {

+            var bodyStatements = ((BlockStmt)ctor.Body).Body;

+            // Repr := {this};

+            var e = new SetDisplayExpr(tok, new List<Expression>() { self });

+            e.Type = new SetType(new ObjectType());

+            Statement s = new AssignStmt(tok, Repr, new ExprRhs(e));

+            s.IsGhost = true;

+            bodyStatements.Add(s);

 

-          AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);

+            AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);

+          }

 

         } else if (member is Method && !member.IsStatic) {

           var m = (Method)member;

           if (Valid != null && !IsSimpleQueryMethod(m)) {

-            // modifies Repr;

-            m.Mod.Expressions.Add(new FrameExpression(Repr.tok, Repr, null));

-            // ensures Valid();

-            var valid = new FunctionCallExpr(tok, "Valid", implicitSelf, tok, new List<Expression>());

-            valid.Function = Valid;

-            valid.Type = Type.Bool;

-            m.Ens.Insert(0, new MaybeFreeExpression(valid));

-            // ensures fresh(Repr - old(Repr));

-            var e0 = new OldExpr(tok, Repr);

-            e0.Type = Repr.Type;

-            var e1 = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, Repr, e0);

-            e1.ResolvedOp = BinaryExpr.ResolvedOpcode.SetDifference;

-            e1.Type = Repr.Type;

-            var freshness = new FreshExpr(tok, e1);

-            freshness.Type = Type.Bool;

-            m.Ens.Insert(1, new MaybeFreeExpression(freshness));

+            if (member.RefinementBase == null) {

+              // modifies Repr;

+              m.Mod.Expressions.Add(new FrameExpression(Repr.tok, Repr, null));

+              // ensures Valid();

+              var valid = new FunctionCallExpr(tok, "Valid", implicitSelf, tok, new List<Expression>());

+              valid.Function = Valid;

+              valid.Type = Type.Bool;

+              m.Ens.Insert(0, new MaybeFreeExpression(valid));

+              // ensures fresh(Repr - old(Repr));

+              var e0 = new OldExpr(tok, Repr);

+              e0.Type = Repr.Type;

+              var e1 = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, Repr, e0);

+              e1.ResolvedOp = BinaryExpr.ResolvedOpcode.SetDifference;

+              e1.Type = Repr.Type;

+              var freshness = new FreshExpr(tok, e1);

+              freshness.Type = Type.Bool;

+              m.Ens.Insert(1, new MaybeFreeExpression(freshness));

+            }

 

-            if (m.Body == null) {

-              m.Body = new BlockStmt(tok, new List<Statement>());

+            if (m.Body != null) {

+              var bodyStatements = ((BlockStmt)m.Body).Body;

+              AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);

             }

-            // TODO: these assignments should be included on every return path

-            var bodyStatements = ((BlockStmt)m.Body).Body;

-            AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);

           }

         }

       }

@@ -269,27 +279,23 @@ namespace Microsoft.Dafny
 

     void AddSubobjectReprs(Boogie.IToken tok, List<Tuple<Field, Field>> subobjects, List<Statement> bodyStatements,

       Expression self, Expression implicitSelf, Expression cNull, Expression Repr) {

+      // TODO: these assignments should be included on every return path

 

       foreach (var ff in subobjects) {

-        var F = new FieldSelectExpr(tok, implicitSelf, ff.Item1.Name);

-        F.Field = ff.Item1;

-        F.Type = ff.Item1.Type;

-

+        var F = Resolver.NewFieldSelectExpr(tok, implicitSelf, ff.Item1, null);  // create a resolved FieldSelectExpr

         Expression e = new SetDisplayExpr(tok, new List<Expression>() { F });

-        e.Type = new SetType(new ObjectType());

+        e.Type = new SetType(new ObjectType());  // resolve here

         var rhs = new BinaryExpr(tok, BinaryExpr.Opcode.Add, Repr, e);

-        rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Union;

-        rhs.Type = Repr.Type;

+        rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Union;  // resolve here

+        rhs.Type = Repr.Type;  // resolve here

         if (ff.Item2 == null) {

           // Repr := Repr + {F}  (so, nothing else to do)

         } else {

           // Repr := Repr + {F} + F.Repr

-          var FRepr = new FieldSelectExpr(tok, F, ff.Item2.Name);

-          FRepr.Field = ff.Item2;

-          FRepr.Type = ff.Item2.Type;

+          var FRepr = Resolver.NewFieldSelectExpr(tok, F, ff.Item2, null);  // create resolved FieldSelectExpr

           rhs = new BinaryExpr(tok, BinaryExpr.Opcode.Add, rhs, FRepr);

-          rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Union;

-          rhs.Type = Repr.Type;

+          rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Union;  // resolve here

+          rhs.Type = Repr.Type;  // resolve here

         }

         // Repr := Repr + ...;

         Statement s = new AssignStmt(tok, Repr, new ExprRhs(rhs));

@@ -334,8 +340,8 @@ namespace Microsoft.Dafny
 

     public static BinaryExpr BinBoolExpr(Boogie.IToken tok, BinaryExpr.ResolvedOpcode rop, Expression e0, Expression e1) {

       var p = new BinaryExpr(tok, BinaryExpr.ResolvedOp2SyntacticOp(rop), e0, e1);

-      p.ResolvedOp = rop;

-      p.Type = Type.Bool;

+      p.ResolvedOp = rop;  // resolve here

+      p.Type = Type.Bool;  // resolve here

       return p;

     }

   }