Merge

10 files changed, 114 insertions, 51 deletions

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index b3f176f8..231a21cf 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -31,6 +31,9 @@ namespace BytecodeTranslator {
     [OptionDescription("Break into debugger", ShortForm = "break")]

     public bool breakIntoDebugger = false;

 

+    [OptionDescription("Emit a 'capture state' directive after each statement, (default: false)", ShortForm = "c")]

+    public bool captureState = false;

+

     [OptionDescription("Search paths for assembly dependencies.", ShortForm = "lib")]

     public List<string> libpaths = new List<string>();

 

@@ -165,16 +168,16 @@ namespace BytecodeTranslator {
       return result;

     }

 

-    public static int TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options/*?*/ options, List<Regex> exemptionList, bool whiteList) {

+    public static int TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {

       Contract.Requires(assemblyNames != null);

       Contract.Requires(heapFactory != null);

 

-      var libPaths = options == null ? null : options.libpaths;

-      var wholeProgram = options == null ? false : options.wholeProgram;

-      var/*?*/ stubAssemblies = options == null ? null : options.stub;

-      var phoneControlsConfigFile = options == null ? null : options.phoneControls;

-      var doPhoneNav = options == null ? false : options.phoneNavigationCode;

-      var doPhoneFeedback = options == null ? false : options.phoneFeedbackCode;

+      var libPaths = options.libpaths;

+      var wholeProgram = options.wholeProgram;

+      var/*?*/ stubAssemblies = options.stub;

+      var phoneControlsConfigFile = options.phoneControls;

+      var doPhoneNav = options.phoneNavigationCode;

+      var doPhoneFeedback = options.phoneFeedbackCode;

 

       var host = new CodeContractAwareHostEnvironment(libPaths != null ? libPaths : Enumerable<string>.Empty, true, true);

       Host = host;

@@ -247,7 +250,7 @@ namespace BytecodeTranslator {
       else

         traverserFactory = new CLRSemantics();

 

-      Sink sink= new Sink(host, traverserFactory, heapFactory, exemptionList, whiteList);

+      Sink sink= new Sink(host, traverserFactory, heapFactory, options, exemptionList, whiteList);

       TranslationHelper.tmpVarCounter = 0;

       MetadataTraverser translator;

       translator= traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index b2c1177e..1427b836 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -27,10 +27,11 @@ namespace BytecodeTranslator {
       get { return this.factory; }

     }

     readonly TraverserFactory factory;

+    private readonly Options options;

     readonly bool whiteList;

     readonly List<Regex> exemptionList;

 

-    public Sink(IContractAwareHost host, TraverserFactory factory, HeapFactory heapFactory, List<Regex> exemptionList, bool whiteList) {

+    public Sink(IContractAwareHost host, TraverserFactory factory, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {

       Contract.Requires(host != null);

       Contract.Requires(factory != null);

       Contract.Requires(heapFactory != null);

@@ -38,6 +39,7 @@ namespace BytecodeTranslator {
       this.host = host;

       this.factory = factory;

       var b = heapFactory.MakeHeap(this, out this.heap, out this.TranslatedProgram); // TODO: what if it returns false?

+      this.options = options;

       this.exemptionList = exemptionList;

       this.whiteList = whiteList;

       if (this.TranslatedProgram == null) {

@@ -52,6 +54,8 @@ namespace BytecodeTranslator {
       }

     }

 

+    public Options Options { get { return this.options; } }

+

     public Heap Heap {

       get { return this.heap; }

     }

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 4c927b3e..015e57ce 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -54,6 +54,8 @@ namespace BytecodeTranslator
     public readonly Bpl.StmtListBuilder StmtBuilder = new Bpl.StmtListBuilder();

     private bool contractContext;

     internal readonly Stack<IExpression> operandStack = new Stack<IExpression>();

+    private bool captureState;

+    private static int captureStateCounter = 0;

 

     #region Constructors

     public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {

@@ -61,6 +63,7 @@ namespace BytecodeTranslator
       this.factory = sink.Factory;

       PdbReader = pdbReader;

       this.contractContext = contractContext;

+      this.captureState = sink.Options.captureState;

     }

     #endregion

 

@@ -108,6 +111,14 @@ namespace BytecodeTranslator
 

     public override void Visit(IStatement statement) {

       EmitSourceContext(statement);

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

+        var tok = statement.Token();

+        var state = String.Format("s{0}", StatementTraverser.captureStateCounter++);

+        var attrib = new Bpl.QKeyValue(tok, "captureState ", new List<object> { state }, null);

+        StmtBuilder.Add(

+          new Bpl.AssumeCmd(tok, Bpl.Expr.True, attrib)

+          );

+      }

       base.Visit(statement);

     }

 

diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
index e3da57b5..a8b5fdb2 100644
--- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs
+++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
@@ -61,7 +61,7 @@ namespace TranslationTest {
     #endregion

 

     private string ExecuteTest(string assemblyName, HeapFactory heapFactory) {

-      BCT.TranslateAssembly(new List<string>{assemblyName}, heapFactory, null, null, false);

+      BCT.TranslateAssembly(new List<string>{assemblyName}, heapFactory, new Options(), null, false);

       var fileName = Path.ChangeExtension(assemblyName, "bpl");

       var s = File.ReadAllText(fileName);

       return s;

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 098dbad2..5e2bc911 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3715,6 +3715,9 @@ namespace Microsoft.Dafny {
         return UsesSpecFeatures(e.Seq) ||

                (e.E0 != null && UsesSpecFeatures(e.E0)) ||

                (e.E1 != null && UsesSpecFeatures(e.E1));

+      } else if (expr is MultiSelectExpr) {

+        MultiSelectExpr e = (MultiSelectExpr)expr;

+        return UsesSpecFeatures(e.Array) || e.Indices.Exists(ee => UsesSpecFeatures(ee));

       } else if (expr is SeqUpdateExpr) {

         SeqUpdateExpr e = (SeqUpdateExpr)expr;

         return UsesSpecFeatures(e.Seq) ||

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 0723bcba..9a8c7541 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -419,50 +419,50 @@ Execution trace:
 Dafny program verifier finished with 3 verified, 3 errors

 

 -------------------- ResolutionErrors.dfy --------------------

-ResolutionErrors.dfy(39,13): Error: 'this' is not allowed in a 'static' context

-ResolutionErrors.dfy(100,9): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(101,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

-ResolutionErrors.dfy(105,11): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(106,9): Error: actual out-parameter 0 is required to be a ghost variable

-ResolutionErrors.dfy(113,15): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(117,23): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(124,4): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(128,21): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(129,35): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(138,9): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(144,16): Error: 'decreases *' is not allowed on ghost loops

-ResolutionErrors.dfy(185,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure

-ResolutionErrors.dfy(208,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

-ResolutionErrors.dfy(220,12): Error: trying to break out of more loop levels than there are enclosing loops

-ResolutionErrors.dfy(224,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

-ResolutionErrors.dfy(229,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context

+ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(110,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

+ResolutionErrors.dfy(114,11): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(115,9): Error: actual out-parameter 0 is required to be a ghost variable

+ResolutionErrors.dfy(122,15): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(126,23): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(133,4): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(137,21): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(138,35): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(147,9): Error: only ghost methods can be called from this context

+ResolutionErrors.dfy(153,16): Error: 'decreases *' is not allowed on ghost loops

+ResolutionErrors.dfy(194,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure

+ResolutionErrors.dfy(217,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

+ResolutionErrors.dfy(229,12): Error: trying to break out of more loop levels than there are enclosing loops

+ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

+ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

 ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops

 ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)

 ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)

 ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)

-ResolutionErrors.dfy(45,14): Error: a field must be selected via an object, not just a class name

-ResolutionErrors.dfy(46,7): Error: unresolved identifier: F

-ResolutionErrors.dfy(47,14): Error: an instance function must be selected via an object, not just a class name

-ResolutionErrors.dfy(47,7): Error: call to instance function requires an instance

-ResolutionErrors.dfy(48,7): Error: unresolved identifier: G

-ResolutionErrors.dfy(50,7): Error: unresolved identifier: M

-ResolutionErrors.dfy(51,7): Error: call to instance method requires an instance

-ResolutionErrors.dfy(52,7): Error: unresolved identifier: N

-ResolutionErrors.dfy(55,8): Error: non-function expression is called with parameters

-ResolutionErrors.dfy(56,14): Error: member z does not exist in class Global

-ResolutionErrors.dfy(75,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')

-ResolutionErrors.dfy(80,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(81,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(83,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(85,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)

-ResolutionErrors.dfy(247,4): Error: label shadows an enclosing label

-ResolutionErrors.dfy(252,2): Error: duplicate label

-ResolutionErrors.dfy(278,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

-ResolutionErrors.dfy(279,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

-ResolutionErrors.dfy(281,4): Error: a constructor is only allowed to be called when an object is being allocated

-ResolutionErrors.dfy(295,16): Error: arguments must have the same type (got int and DTD_List)

-ResolutionErrors.dfy(296,16): Error: arguments must have the same type (got DTD_List and int)

-ResolutionErrors.dfy(297,25): Error: arguments must have the same type (got bool and int)

+ResolutionErrors.dfy(54,14): Error: a field must be selected via an object, not just a class name

+ResolutionErrors.dfy(55,7): Error: unresolved identifier: F

+ResolutionErrors.dfy(56,14): Error: an instance function must be selected via an object, not just a class name

+ResolutionErrors.dfy(56,7): Error: call to instance function requires an instance

+ResolutionErrors.dfy(57,7): Error: unresolved identifier: G

+ResolutionErrors.dfy(59,7): Error: unresolved identifier: M

+ResolutionErrors.dfy(60,7): Error: call to instance method requires an instance

+ResolutionErrors.dfy(61,7): Error: unresolved identifier: N

+ResolutionErrors.dfy(64,8): Error: non-function expression is called with parameters

+ResolutionErrors.dfy(65,14): Error: member z does not exist in class Global

+ResolutionErrors.dfy(84,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')

+ResolutionErrors.dfy(89,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

+ResolutionErrors.dfy(90,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

+ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

+ResolutionErrors.dfy(94,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)

+ResolutionErrors.dfy(256,4): Error: label shadows an enclosing label

+ResolutionErrors.dfy(261,2): Error: duplicate label

+ResolutionErrors.dfy(287,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

+ResolutionErrors.dfy(288,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

+ResolutionErrors.dfy(290,4): Error: a constructor is only allowed to be called when an object is being allocated

+ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int and DTD_List)

+ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)

+ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)

 44 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index f8adaad5..1b68ad91 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -24,6 +24,15 @@ method ManyIndices<T>(a: array3<T>, b: array<T>, m: int, n: int)
   var z := b[m, n, m, n];  // error

 }

 

+method SB(b: array2<int>, s: int) returns (x: int, y: int)

+  requires b != null;

+{

+  while

+  {

+    case b[x,y] == s =>

+  }

+}

+

 // -------- name resolution

 

 class Global {

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 5ee9f921..2b60b851 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -85,7 +85,7 @@ Dafny program verifier finished with 29 verified, 0 errors
 

 -------------------- Rippling.dfy --------------------

 

-Dafny program verifier finished with 132 verified, 0 errors

+Dafny program verifier finished with 137 verified, 0 errors

 

 -------------------- Celebrity.dfy --------------------

 

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 0a4d541d..5fd87a6c 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -234,6 +234,13 @@ function sort(xs: List): List
   case Cons(y, ys) => insort(y, sort(ys))

 }

 

+function reverse(xs: List): List

+{

+  match xs

+  case Nil => Nil

+  case Cons(t, rest) => concat(reverse(rest), Cons(t, Nil))

+}

+

 // Pair list functions

 

 function zip(a: List, b: List): PList

@@ -554,3 +561,28 @@ ghost method P67()
     assert (forall x,y :: add(x, Suc(y)) == Suc(add(x,y)));

   }

 }

+

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

+

+ghost method Lemma_RevConcat(xs: List, ys: List)

+  ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));

+{

+  match (xs) {

+    case Nil =>

+      assert forall ws :: concat(ws, Nil) == ws;

+    case Cons(t, rest) =>

+      Lemma_RevConcat(rest, ys);

+      assert forall a, b, c :: concat(a, concat(b, c)) == concat(concat(a, b), c);

+  }

+}

+

+ghost method Theorem(xs: List)

+  ensures reverse(reverse(xs)) == xs;

+{

+  match (xs) {

+    case Nil =>

+    case Cons(t, rest) =>

+      Lemma_RevConcat(reverse(rest), Cons(t, Nil));

+      Theorem(rest);

+  }

+}

diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 0cd95bbd..df0f22ee 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -352,6 +352,7 @@ namespace Demo
           | "==>"

           | "<==>"

           | "#"

+          | "?" // this is not an operator, but a possible character in identifiers

           | n

           | stringLiteral

           ;