diff options
author | qadeer <qadeer@microsoft.com> | 2011-08-04 18:31:23 -0700 |
---|---|---|
committer | qadeer <qadeer@microsoft.com> | 2011-08-04 18:31:23 -0700 |
commit | ae2d46b87b118669030e8720b166017eeed99231 (patch) | |
tree | 641d2fbe9263ecdc495bf5bc7a8311edae6f4c18 | |
parent | 7d683795bba785bed77e9357e0bfd7754226f643 (diff) | |
parent | 3901e6e672eb3c85472aa2750084ac4aba63d710 (diff) |
Merge
-rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 19 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 6 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/StatementTraverser.cs | 11 | ||||
-rw-r--r-- | BCT/RegressionTests/TranslationTest/UnitTest0.cs | 2 | ||||
-rw-r--r-- | Source/Dafny/Resolver.cs | 3 | ||||
-rw-r--r-- | Test/dafny0/Answer | 80 | ||||
-rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 9 | ||||
-rw-r--r-- | Test/dafny1/Answer | 2 | ||||
-rw-r--r-- | Test/dafny1/Rippling.dfy | 32 | ||||
-rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 1 |
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
;
|