Merge

11 files changed, 142 insertions, 57 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index b2d23777..19af68d9 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -687,8 +687,10 @@ namespace BytecodeTranslator
           this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(lhs, fromUnion));

         }

 

-        Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));

-        this.StmtTraverser.RaiseException(expr);

+        if (this.sink.Options.modelExceptions) {

+          Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));

+          this.StmtTraverser.RaiseException(expr);

+        }

       } finally {

         // TODO move away phone related code from the translation, it would be better to have 2 or more translation phases

         if (PhoneCodeHelper.instance().PhonePlugin != null) {

@@ -1215,22 +1217,24 @@ namespace BytecodeTranslator
         } else {

           Bpl.Expr x = null;

           Bpl.IdentifierExpr temp = null;

-          if (target.Instance != null) {

-            this.Traverse(target.Instance);

-            x = this.TranslatedExpressions.Pop();

-            if (pushTargetRValue) {

+          if (pushTargetRValue) {

+            if (target.Instance != null) {

+              this.Traverse(target.Instance);

+              x = this.TranslatedExpressions.Pop();

               AssertOrAssumeNonNull(tok, x);

               var e2 = this.sink.Heap.ReadHeap(x, f, TranslationHelper.IsStruct(field.ContainingType) ? AccessType.Struct : AccessType.Heap, boogieTypeOfField);

               this.TranslatedExpressions.Push(e2);

-

-              if (!treatAsStatement && resultIsInitialTargetRValue) {

-                var loc = this.sink.CreateFreshLocal(source.Type);

-                temp = Bpl.Expr.Ident(loc);

-                var e3 = this.TranslatedExpressions.Pop();

-                var cmd = Bpl.Cmd.SimpleAssign(tok, temp, e3);

-                this.StmtTraverser.StmtBuilder.Add(cmd);

-                this.TranslatedExpressions.Push(temp);

-              }

+            } else {

+              TranslatedExpressions.Push(f);

+            }

+            

+            if (!treatAsStatement && resultIsInitialTargetRValue) {

+              var loc = this.sink.CreateFreshLocal(source.Type);

+              temp = Bpl.Expr.Ident(loc);

+              var e3 = this.TranslatedExpressions.Pop();

+              var cmd = Bpl.Cmd.SimpleAssign(tok, temp, e3);

+              this.StmtTraverser.StmtBuilder.Add(cmd);

+              this.TranslatedExpressions.Push(temp);

             }

           }

           sourceTraverser(source);

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index e65ef6a9..c95d69e5 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -532,7 +532,8 @@ namespace BytecodeTranslator {
         foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {

           vars.Add(v);

         }

-        vars.Add(procInfo.LocalExcVariable);

+        if (this.sink.Options.modelExceptions)

+          vars.Add(procInfo.LocalExcVariable);

         vars.Add(procInfo.LabelVariable);

         Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());

         #endregion

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index ffee13eb..81f630aa 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -38,6 +38,9 @@ namespace BytecodeTranslator {
     [OptionDescription("Emit a 'capture state' directive after each statement, (default: false)", ShortForm = "c")]

     public bool captureState = false;

 

+    [OptionDescription("Model exceptional control flow, (default: true)", ShortForm = "e")]

+    public bool modelExceptions = true;

+

     [OptionDescription("Translation should be done for Get Me Here functionality, (default: false)", ShortForm = "gmh")]

     public bool getMeHere = false;

 

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 49f932ec..745c2fff 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -518,6 +518,14 @@ namespace BytecodeTranslator
     }

 

     public override void TraverseChildren(ITryCatchFinallyStatement tryCatchFinallyStatement) {

+

+      if (!this.sink.Options.modelExceptions) {

+        this.Traverse(tryCatchFinallyStatement.TryBody);

+        if (tryCatchFinallyStatement.FinallyBody != null)

+          this.Traverse(tryCatchFinallyStatement.FinallyBody);

+        return;

+      }

+

       this.sink.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, Sink.TryCatchFinallyContext>(tryCatchFinallyStatement, Sink.TryCatchFinallyContext.InTry));

       this.Traverse(tryCatchFinallyStatement.TryBody);

       StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)));

@@ -572,6 +580,10 @@ namespace BytecodeTranslator
     }

 

     public override void TraverseChildren(IThrowStatement throwStatement) {

+      if (!this.sink.Options.modelExceptions) {

+        StmtBuilder.Add(new Bpl.AssumeCmd(throwStatement.Token(), Bpl.Expr.False));

+        return;

+      }

       ExpressionTraverser exceptionTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);

       exceptionTraverser.Traverse(throwStatement.Exception);

       StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), exceptionTraverser.TranslatedExpressions.Pop()));

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 0fe003ae..0a2a515a 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -997,6 +997,36 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this:
 

 

 

+implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref)

+{

+  var xs: Ref;

+  var $localExc: Ref;

+  var $label: int;

+

+    xs := xs$in;

+    assume {:breadcrumb 13} true;

+    if (xs != null)

+    {

+    }

+    else

+    {

+    }

+

+    if ((if xs != null then $ArrayLength(xs) > 0 else false))

+    {

+        assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;

+        assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;

+        assume $this != null;

+        assume xs != null;

+        $ArrayContents := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][0 := Int2Union(Union2Int($ArrayContents[xs][0]))]];

+    }

+    else

+    {

+    }

+}

+

+

+

 procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref);

   free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 5dfc582e..b552ee36 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -983,6 +983,36 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this:
 

 

 

+implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref)

+{

+  var xs: Ref;

+  var $localExc: Ref;

+  var $label: int;

+

+    xs := xs$in;

+    assume {:breadcrumb 13} true;

+    if (xs != null)

+    {

+    }

+    else

+    {

+    }

+

+    if ((if xs != null then $ArrayLength(xs) > 0 else false))

+    {

+        assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;

+        assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;

+        assume $this != null;

+        assume xs != null;

+        $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][0 := Int2Union(Union2Int($ArrayContents[xs][0]))]];

+    }

+    else

+    {

+    }

+}

+

+

+

 procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref);

   free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);

 

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 0dcbcf11..8ea17a52 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1545,6 +1545,7 @@ namespace Microsoft.Dafny {
   public class Method : MemberDecl, TypeParameter.ParentType

   {

     public readonly bool SignatureIsOmitted;

+    public bool MustReverify;

     public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;

     public readonly List<Formal/*!*/>/*!*/ Ins;

     public readonly List<Formal/*!*/>/*!*/ Outs;

@@ -1593,6 +1594,7 @@ namespace Microsoft.Dafny {
       this.Decreases = decreases;

       this.Body = body;

       this.SignatureIsOmitted = signatureOmitted;

+      MustReverify = false;

     }

   }

 

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 008bf616..e0f12246 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -66,6 +66,7 @@ namespace Microsoft.Dafny
     private ModuleDefinition moduleUnderConstruction;  // non-null for the duration of Construct calls

     private Queue<Action> postTasks = new Queue<Action>();  // empty whenever moduleUnderConstruction==null, these tasks are for the post-resolve phase of module moduleUnderConstruction

     public Queue<Tuple<Method, Method>> translationMethodChecks = new Queue<Tuple<Method, Method>>();  // contains all the methods that need to be checked for structural refinement.

+    private Method currentMethod;

 

     public void PreResolve(ModuleDefinition m) {

 

@@ -388,35 +389,35 @@ namespace Microsoft.Dafny
       

     }

     // Check that two resolved types are the same in a similar context (the same type parameters, method, class, etc.)

-    // Assumes that a is in a previous refinement, and b is in a refinement.

-    public static bool ResolvedTypesAreTheSame(Type a, Type b) {

-      Contract.Requires(a != null);

-      Contract.Requires(b != null);

-      if (a is TypeProxy || b is TypeProxy)

+    // Assumes that prev is in a previous refinement, and next is in some refinement. Note this is not communative.

+    public static bool ResolvedTypesAreTheSame(Type prev, Type next) {

+      Contract.Requires(prev != null);

+      Contract.Requires(next != null);

+      if (prev is TypeProxy || next is TypeProxy)

         return false;

 

-      if (a is BoolType) {

-        return b is BoolType;

-      } else if (a is IntType) {

-        if (b is IntType) {

-          return (a is NatType) == (b is NatType);

+      if (prev is BoolType) {

+        return next is BoolType;

+      } else if (prev is IntType) {

+        if (next is IntType) {

+          return (prev is NatType) == (next is NatType);

         } else return false;

-      } else if (a is ObjectType) {

-        return b is ObjectType;

-      } else if (a is SetType) {

-        return b is SetType && ResolvedTypesAreTheSame(((SetType)a).Arg, ((SetType)b).Arg);

-      } else if (a is MultiSetType) {

-        return b is MultiSetType && ResolvedTypesAreTheSame(((MultiSetType)a).Arg, ((MultiSetType)b).Arg);

-      } else if (a is MapType) {

-        return b is MapType && ResolvedTypesAreTheSame(((MapType)a).Domain, ((MapType)b).Domain) && ResolvedTypesAreTheSame(((MapType)a).Range, ((MapType)b).Range);

-      } else if (a is SeqType) {

-        return b is SeqType && ResolvedTypesAreTheSame(((SeqType)a).Arg, ((SeqType)b).Arg);

-      } else if (a is UserDefinedType) {

-        if (!(b is UserDefinedType)) {

+      } else if (prev is ObjectType) {

+        return next is ObjectType;

+      } else if (prev is SetType) {

+        return next is SetType && ResolvedTypesAreTheSame(((SetType)prev).Arg, ((SetType)next).Arg);

+      } else if (prev is MultiSetType) {

+        return next is MultiSetType && ResolvedTypesAreTheSame(((MultiSetType)prev).Arg, ((MultiSetType)next).Arg);

+      } else if (prev is MapType) {

+        return next is MapType && ResolvedTypesAreTheSame(((MapType)prev).Domain, ((MapType)next).Domain) && ResolvedTypesAreTheSame(((MapType)prev).Range, ((MapType)next).Range);

+      } else if (prev is SeqType) {

+        return next is SeqType && ResolvedTypesAreTheSame(((SeqType)prev).Arg, ((SeqType)next).Arg);

+      } else if (prev is UserDefinedType) {

+        if (!(next is UserDefinedType)) {

           return false;

         }

-        UserDefinedType aa = (UserDefinedType)a;

-        UserDefinedType bb = (UserDefinedType)b;

+        UserDefinedType aa = (UserDefinedType)prev;

+        UserDefinedType bb = (UserDefinedType)next;

         if (aa.ResolvedClass != null && aa.ResolvedClass.Name == bb.ResolvedClass.Name) {

           // these are both resolved class/datatype types

           Contract.Assert(aa.TypeArgs.Count == bb.TypeArgs.Count);

@@ -634,7 +635,7 @@ namespace Microsoft.Dafny
                 CheckAgreement_Parameters(m.tok, prevMethod.Ins, m.Ins, m.Name, "method", "in-parameter");

                 CheckAgreement_Parameters(m.tok, prevMethod.Outs, m.Outs, m.Name, "method", "out-parameter");

               }

-

+              currentMethod = m;

               var replacementBody = m.Body;

               if (replacementBody != null) {

                 if (prevMethod.Body == null) {

@@ -1223,7 +1224,7 @@ namespace Microsoft.Dafny
     }

 

     // Checks that statement stmt, defined in the constructed module m, is a refinement of skip in the parent module

-    private void CheckIsOkayUpdateStmt(ConcreteUpdateStatement stmt, ModuleDefinition m, ResolutionErrorReporter reporter) {

+    private bool CheckIsOkayUpdateStmt(ConcreteUpdateStatement stmt, ModuleDefinition m, ResolutionErrorReporter reporter) {

       foreach (var lhs in stmt.Lhss) {

         var l = lhs.Resolved;

         if (l is IdentifierExpr) {

@@ -1232,23 +1233,25 @@ namespace Microsoft.Dafny
           if ((ident.Var is VarDecl && RefinementToken.IsInherited(((VarDecl)ident.Var).Tok, m)) || ident.Var is Formal) {

             // for some reason, formals are not considered to be inherited.

             reporter.Error(l.tok, "cannot assign to variable defined previously");

+            return false;

           }

         } else if (l is FieldSelectExpr) {

           if (RefinementToken.IsInherited(((FieldSelectExpr)l).Field.tok, m)) {

-            reporter.Error(l.tok, "cannot assign to field defined previously");

+            return false;

           }

         } else {

-          reporter.Error(lhs.tok, "cannot assign to something which could exist in the previous refinement");

+          return false;

         }

       }

       if (stmt is UpdateStmt) {

         var s = (UpdateStmt)stmt;

         foreach (var rhs in s.Rhss) {

           if (s.Rhss[0].CanAffectPreviouslyKnownExpressions) {

-            reporter.Error(s.Rhss[0].Tok, "cannot have method call which can affect the heap");

+            return false;

           }

         }

       }

+      return true;

     }

     // ---------------------- additional methods -----------------------------------------------------------------------------

 

@@ -1293,7 +1296,7 @@ namespace Microsoft.Dafny
       SubstitutionsMade = new SortedSet<string>();

       this.c = c;

     }

-    new public Expression CloneExpr(Expression expr) {

+    public override Expression CloneExpr(Expression expr) {

       if (expr is NamedExpr) {

         NamedExpr n = (NamedExpr)expr;

         Expression E;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a8541293..2e322029 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3595,7 +3595,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(errorMessage != null);

       Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);

 

-      if (RefinementToken.IsInherited(refinesToken, currentModule)) {

+      if (RefinementToken.IsInherited(refinesToken, currentModule) && (currentMethod == null || !currentMethod.MustReverify)) {

         // produce an assume instead

         return new Bpl.AssumeCmd(tok, condition);

       } else {

@@ -3614,7 +3614,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(condition != null);

       Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);

 

-      if (RefinementToken.IsInherited(refinesTok, currentModule)) {

+      if (RefinementToken.IsInherited(refinesTok, currentModule) && (currentMethod == null || !currentMethod.MustReverify)) {

         // produce a "skip" instead

         return new Bpl.AssumeCmd(tok, Bpl.Expr.True);

       } else {

@@ -3634,7 +3634,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(condition != null);

       Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);

 

-      if (RefinementToken.IsInherited(tok, currentModule)) {

+      if (RefinementToken.IsInherited(tok, currentModule) && (currentMethod == null || !currentMethod.MustReverify)) {

         // produce an assume instead

         return new Bpl.AssumeCmd(tok, condition, kv);

       } else {

@@ -4762,7 +4762,7 @@ namespace Microsoft.Dafny {
 

       // Make the call

       string name;

-      if (RefinementToken.IsInherited(method.tok, currentModule)) {

+      if (RefinementToken.IsInherited(method.tok, currentModule) && (currentMethod == null || !currentMethod.MustReverify)) {

         name = string.Format("RefinementCall_{0}$${1}", currentModule.Name, method.FullCompileName);

       } else {

         name = method.FullCompileName;

@@ -7479,7 +7479,7 @@ namespace Microsoft.Dafny {
         translatedExpression = etran.TrExpr(expr);

         splitHappened = etran.Statistics_CustomLayerFunctionCount != 0;  // return true if the LayerOffset(1) came into play

       }

-      if (RefinementToken.IsInherited(expr.tok, currentModule) && RefinementTransformer.ContainsChange(expr, currentModule)) {

+      if (RefinementToken.IsInherited(expr.tok, currentModule) && (currentMethod == null || !currentMethod.MustReverify) && RefinementTransformer.ContainsChange(expr, currentModule)) {

         // If "expr" contains a subexpression that has changed from the inherited expression, we'll destructively

         // change the token of the translated expression to make it look like it's not inherited.  This will cause "e" to

         // be verified again in the refining module.

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 3899b6df..70527966 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1599,10 +1599,9 @@ LiberalEquality.dfy(52,14): Error: arguments must have the same type (got array<
 3 resolution/type errors detected in LiberalEquality.dfy

 

 -------------------- RefinementModificationChecking.dfy --------------------

-RefinementModificationChecking.dfy(16,4): Error: cannot assign to variable defined previously

 RefinementModificationChecking.dfy(17,4): Error: cannot assign to variable defined previously

-RefinementModificationChecking.dfy(18,4): Error: cannot assign to field defined previously

-3 resolution/type errors detected in RefinementModificationChecking.dfy

+RefinementModificationChecking.dfy(18,4): Error: cannot assign to variable defined previously

+2 resolution/type errors detected in RefinementModificationChecking.dfy

 

 -------------------- SmallTests.dfy --------------------

 SmallTests.dfy(30,11): Error: index out of range

diff --git a/Test/dafny0/RefinementModificationChecking.dfy b/Test/dafny0/RefinementModificationChecking.dfy
index 887c3595..dbf39106 100644
--- a/Test/dafny0/RefinementModificationChecking.dfy
+++ b/Test/dafny0/RefinementModificationChecking.dfy
@@ -2,6 +2,7 @@
 ghost module R1 {

   var f: int;

   method m(y: set<int>) returns (r: int)

+    modifies this;

   {

     var t := y;

   }

@@ -13,9 +14,9 @@ ghost module R2 refines R1 {
   {

     ...;

     var x := 3;

-    t := {1}; // bad: previous local

-    r := 3; // bad: out parameter

-    f := 4; // bad: previous field

+    t := {1}; // error: previous local

+    r := 3; // error: out parameter

+    f := 4; // fine: all fields, will cause re-verification

     x := 6; // fine: new local

     g := 34;// fine: new field

   }