diff options
39 files changed, 333 insertions, 67 deletions
@@ -9,6 +9,11 @@ Test/([^/]*)/([^/]*)\.sx ^Test/sandbox/.*
^Test/.*\.csv
Package/.*
+Test/.*/flycheck_.*
+.*\.orig
+Test/.*\.bpl
+Test/.*/axiom-profiler.html
+Test/.*/z3.log
syntax: glob
*.exe
*.pdb
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 35c6cec4..c7aae173 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -4796,7 +4796,7 @@ namespace Microsoft.Dafny { }
public override IEnumerable<Expression> SubExpressions
{
- get {
+ get { // FIXME: This can return duplicates; this could confuse BottomUpVisitors that modify the AST in place
foreach (var e in base.SubExpressions) { yield return e; }
foreach (var e in Attributes.SubExpressions(Attributes)) { yield return e; }
@@ -5182,6 +5182,7 @@ namespace Microsoft.Dafny { return s;
}
+
/// <summary>
/// Create a resolved expression of the form "CVT(e0) - CVT(e1)", where "CVT" is either "int" (if
/// e0.Type is an integer-based numeric type) or "real" (if e0.Type is a real-based numeric type).
@@ -5195,13 +5196,21 @@ namespace Microsoft.Dafny { Contract.Ensures(Contract.Result<Expression>() != null);
Type toType = e0.Type.IsNumericBased(Type.NumericPersuation.Int) ? (Type)Type.Int : Type.Real;
- e0 = new ConversionExpr(e0.tok, e0, toType);
- e0.Type = toType;
- e1 = new ConversionExpr(e1.tok, e1, toType);
- e1.Type = toType;
+ e0 = CastIfNeeded(e0, toType);
+ e1 = CastIfNeeded(e1, toType);
return CreateSubtract(e0, e1);
}
+ private static Expression CastIfNeeded(Expression expr, Type toType) {
+ if (!expr.Type.Equals(toType)) {
+ var cast = new ConversionExpr(expr.tok, expr, toType);
+ cast.Type = toType;
+ return cast;
+ } else {
+ return expr;
+ }
+ }
+
/// <summary>
/// Create a resolved expression of the form "e0 - e1"
/// </summary>
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 557eee93..9bc24c30 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -68,6 +68,7 @@ namespace Microsoft.Dafny foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
splitter.Visit(decl);
}
+ splitter.Commit();
}
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 524466c9..09ca32e0 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4885,16 +4885,17 @@ namespace Microsoft.Dafny { MultiSelectExpr e = (MultiSelectExpr)expr;
CheckWellformed(e.Array, options, locals, builder, etran);
Bpl.Expr array = etran.TrExpr(e.Array);
- int i = 0;
- foreach (Expression idx in e.Indices) {
+ for (int idxId = 0; idxId < e.Indices.Count; idxId++) {
+ var idx = e.Indices[idxId];
CheckWellformed(idx, options, locals, builder, etran);
- Bpl.Expr index = etran.TrExpr(idx);
- Bpl.Expr lower = Bpl.Expr.Le(Bpl.Expr.Literal(0), index);
- Bpl.Expr length = ArrayLength(idx.tok, array, e.Indices.Count, i);
- Bpl.Expr upper = Bpl.Expr.Lt(index, length);
- builder.Add(Assert(idx.tok, Bpl.Expr.And(lower, upper), "index " + i + " out of range", options.AssertKv));
- i++;
+ var index = etran.TrExpr(idx);
+ var lower = Bpl.Expr.Le(Bpl.Expr.Literal(0), index);
+ var length = ArrayLength(idx.tok, array, e.Indices.Count, idxId);
+ var upper = Bpl.Expr.Lt(index, length);
+ var tok = idx is IdentifierExpr ? e.tok : idx.tok; // TODO: Reusing the token of an identifier expression would underline its definition. but this is still not perfect.
+
+ builder.Add(Assert(tok, Bpl.Expr.And(lower, upper), String.Format("index {0} out of range", idxId), options.AssertKv));
}
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index c50bc9c6..865aa33e 100644 --- a/Source/Dafny/Triggers/QuantifierSplitter.cs +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -1,11 +1,19 @@ using Microsoft.Boogie;
using System;
using System.Collections.Generic;
+using System.Diagnostics.Contracts;
using System.Linq;
using System.Text;
namespace Microsoft.Dafny.Triggers {
class QuantifierSplitter : BottomUpVisitor {
+ /// This cache was introduced because some statements (notably calc) return the same SubExpression multiple times.
+ /// This ended up causing an inconsistent situation when the calc statement's subexpressions contained the same quantifier
+ /// twice: on the first pass that quantifier got its SplitQuantifiers generated, and on the the second pass these
+ /// split quantifiers got re-split, creating a situation where the direct children of a split quantifier were
+ /// also split quantifiers.
+ private Dictionary<QuantifierExpr, List<Expression>> splits = new Dictionary<QuantifierExpr, List<Expression>>();
+
private static BinaryExpr.Opcode FlipOpcode(BinaryExpr.Opcode opCode) {
if (opCode == BinaryExpr.Opcode.And) {
return BinaryExpr.Opcode.Or;
@@ -24,8 +32,15 @@ namespace Microsoft.Dafny.Triggers { // forall x :: P(x) ==> (Q(x) && R(x))
private static UnaryOpExpr Not(Expression expr) {
- var not = new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr) { Type = expr.Type };
- return not;
+ return new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr) { Type = expr.Type };
+ }
+
+ private static Attributes CopyAttributes(Attributes source) {
+ if (source == null) {
+ return null;
+ } else {
+ return new Attributes(source.Name, source.Args, CopyAttributes(source.Prev));
+ }
}
internal static IEnumerable<Expression> SplitExpr(Expression expr, BinaryExpr.Opcode separator) {
@@ -48,7 +63,8 @@ namespace Microsoft.Dafny.Triggers { internal static IEnumerable<Expression> SplitAndStich(BinaryExpr pair, BinaryExpr.Opcode separator) {
foreach (var e1 in SplitExpr(pair.E1, separator)) {
- yield return new BinaryExpr(pair.tok, pair.Op, pair.E0, e1) { ResolvedOp = pair.ResolvedOp, Type = pair.Type };
+ // Notice the token. This makes triggers/splitting-picks-the-right-tokens.dfy possible
+ yield return new BinaryExpr(e1.tok, pair.Op, pair.E0, e1) { ResolvedOp = pair.ResolvedOp, Type = pair.Type };
}
}
@@ -65,7 +81,7 @@ namespace Microsoft.Dafny.Triggers { }
foreach (var e in stream) {
var tok = new NestedToken(quantifier.tok, e.tok);
- yield return new ForallExpr(tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type };
+ yield return new ForallExpr(tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, e, CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type };
}
} else if (quantifier is ExistsExpr) {
IEnumerable<Expression> stream;
@@ -76,22 +92,35 @@ namespace Microsoft.Dafny.Triggers { }
foreach (var e in stream) {
var tok = new NestedToken(quantifier.tok, e.tok);
- yield return new ExistsExpr(tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type };
+ yield return new ExistsExpr(tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, e, CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type };
}
} else {
yield return quantifier;
}
}
+
+ private static bool AllowsSplitting(QuantifierExpr quantifier) {
+ bool splitAttr = true;
+ return !Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr;
+ }
protected override void VisitOneExpr(Expression expr) {
var quantifier = expr as QuantifierExpr;
- if (quantifier != null && quantifier.SplitQuantifier == null) {
- bool splitAttr = true;
- if (!Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr) {
- var split = SplitQuantifier(quantifier).ToList();
- quantifier.SplitQuantifier = split;
+ if (quantifier != null) {
+ Contract.Assert(quantifier.SplitQuantifier == null);
+ if (!splits.ContainsKey(quantifier) && AllowsSplitting(quantifier)) {
+ splits[quantifier] = SplitQuantifier(quantifier).ToList();
}
}
}
+
+ /// <summary>
+ /// See comments above definition of splits for reason why this method exists
+ /// </summary>
+ internal void Commit() {
+ foreach (var quantifier in splits.Keys) {
+ quantifier.SplitQuantifier = splits[quantifier];
+ }
+ }
}
}
diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index 1d5625cd..6555b52a 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -34,6 +34,7 @@ namespace Microsoft.Dafny.Triggers { readonly List<QuantifierWithTriggers> quantifiers;
internal QuantifiersCollection(IEnumerable<QuantifierExpr> quantifiers, ErrorReporter reporter) {
+ Contract.Requires(quantifiers.All(q => q.SplitQuantifier == null));
this.reporter = reporter;
this.quantifiers = quantifiers.Select(q => new QuantifierWithTriggers(q)).ToList();
}
@@ -118,7 +119,7 @@ namespace Microsoft.Dafny.Triggers { (candidate, loopingSubterms) => !loopingSubterms.Any(),
(candidate, loopingSubterms) => {
looping.Add(candidate);
- candidate.Annotation = "loops with " + loopingSubterms.MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", ");
+ candidate.Annotation = "may loop with " + loopingSubterms.MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", ");
}).ToList();
q.CouldSuppressLoops = safe.Count > 0;
diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs index 3385f36e..1f37dcfa 100644 --- a/Source/Dafny/Triggers/QuantifiersCollector.cs +++ b/Source/Dafny/Triggers/QuantifiersCollector.cs @@ -26,7 +26,7 @@ namespace Microsoft.Dafny.Triggers { if (quantifier.SplitQuantifier != null) {
var collection = quantifier.SplitQuantifier.Select(q => q as QuantifierExpr).Where(q => q != null);
quantifierCollections.Add(new QuantifiersCollection(collection, reporter));
- foreach (var q in quantifier.SplitQuantifier) { quantifiers.Add(q); }
+ quantifiers.UnionWith(quantifier.SplitQuantifier);
} else {
quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter));
}
diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs index 02deb92f..71414eee 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -121,7 +121,7 @@ namespace Microsoft.Dafny.Triggers { }
internal static IEnumerable<TriggerMatch> SubexpressionsMatchingTrigger(this QuantifierExpr quantifier, Expression trigger) {
- return quantifier.Term.AllSubExpressions(true, false) //FIXME should loop detection actually pass true here?
+ return quantifier.AllSubExpressions(true, true)
.Select(e => TriggerUtils.PrepareExprForInclusionInTrigger(e).MatchAgainst(trigger, quantifier.BoundVars, e))
.Where(e => e.HasValue).Select(e => e.Value);
}
diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 11860404..69c47d90 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -185,7 +185,8 @@ namespace Microsoft.Dafny.Triggers { expr.SubExpressions.Iter(e => Annotate(e));
TriggerAnnotation annotation; // TODO: Using ApplySuffix fixes the unresolved members problem in GenericSort
- if (expr is FunctionCallExpr || expr is SeqSelectExpr || expr is MemberSelectExpr || expr is OldExpr || expr is ApplyExpr || expr is DisplayExpression ||
+ if (expr is FunctionCallExpr || expr is SeqSelectExpr || expr is MultiSelectExpr || expr is MemberSelectExpr ||
+ expr is OldExpr || expr is ApplyExpr || expr is DisplayExpression ||
(expr is UnaryOpExpr && (((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Cardinality)) || // FIXME || ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh doesn't work, as fresh is a pretty tricky predicate when it's not about datatypes. See translator.cs:10944
(expr is BinaryExpr && (((BinaryExpr)expr).Op == BinaryExpr.Opcode.NotIn || ((BinaryExpr)expr).Op == BinaryExpr.Opcode.In))) {
annotation = AnnotatePotentialCandidate(expr);
diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy index acfe6b8d..d7c87e6d 100644 --- a/Test/dafny0/AutoReq.dfy +++ b/Test/dafny0/AutoReq.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function f(x:int) : bool
@@ -313,3 +313,8 @@ module OpaqueTest { }
}
+
+// autoTriggers added because it causes an extra error message related to
+// violated preconditions to appear. That extra message is due to the extra
+// precondition involving a split quantifier: the user now gets two traces, one
+// for each conjunct.
diff --git a/Test/dafny0/AutoReq.dfy.expect b/Test/dafny0/AutoReq.dfy.expect index b4b34e14..25f00797 100644 --- a/Test/dafny0/AutoReq.dfy.expect +++ b/Test/dafny0/AutoReq.dfy.expect @@ -1,5 +1,12 @@ AutoReq.dfy(247,4): Error: possible violation of function precondition
AutoReq.dfy(239,13): Related location
+AutoReq.dfy(239,59): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Else
+AutoReq.dfy(247,4): Error: possible violation of function precondition
+AutoReq.dfy(239,13): Related location
+AutoReq.dfy(239,35): Related location
Execution trace:
(0,0): anon0
(0,0): anon4_Else
@@ -42,4 +49,4 @@ Execution trace: (0,0): anon0
(0,0): anon11_Then
-Dafny program verifier finished with 52 verified, 8 errors
+Dafny program verifier finished with 52 verified, 9 errors
diff --git a/Test/dafny0/Inverses.dfy b/Test/dafny0/Inverses.dfy index 7995255a..b424cfd9 100644 --- a/Test/dafny0/Inverses.dfy +++ b/Test/dafny0/Inverses.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This identity function is used to so that if the occurrence of i below
@@ -110,3 +110,6 @@ method RotateD<T>(a: array<T>) returns (r: array<T>) r[if a.Length - 1 == i then 0 else i + 1] := a[Id(i)]; // yes, Dafny can invert this one
}
}
+
+// autoTriggers added because it causes a slight rephrasing of an error
+// message.
diff --git a/Test/dafny0/Inverses.dfy.expect b/Test/dafny0/Inverses.dfy.expect index 29c67e5d..b9530e3f 100644 --- a/Test/dafny0/Inverses.dfy.expect +++ b/Test/dafny0/Inverses.dfy.expect @@ -1,10 +1,12 @@ Inverses.dfy(70,0): Error BP5003: A postcondition might not hold on this return path.
Inverses.dfy(69,10): Related location: This is the postcondition that might not hold.
+Inverses.dfy(69,66): Related location
Execution trace:
(0,0): anon0
(0,0): anon6_Else
Inverses.dfy(83,0): Error BP5003: A postcondition might not hold on this return path.
Inverses.dfy(82,10): Related location: This is the postcondition that might not hold.
+Inverses.dfy(82,66): Related location
Execution trace:
(0,0): anon0
(0,0): anon9_Else
diff --git a/Test/dafny0/Matrix-OOB.dfy b/Test/dafny0/Matrix-OOB.dfy new file mode 100644 index 00000000..2e5c0366 --- /dev/null +++ b/Test/dafny0/Matrix-OOB.dfy @@ -0,0 +1,13 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This is a regression test: OOB errors for matrices used to be reported on the
+// quantifier that introduced the variables that constituted the invalid indices.
+
+// WISH: It would be even better to report the error on the variables inside the
+// array instead of the array itself.
+
+method M(m: array2<int>)
+ requires m != null
+ ensures forall i, j :: m[i, j] == 0
+{ }
diff --git a/Test/dafny0/Matrix-OOB.dfy.expect b/Test/dafny0/Matrix-OOB.dfy.expect new file mode 100644 index 00000000..94e77aa4 --- /dev/null +++ b/Test/dafny0/Matrix-OOB.dfy.expect @@ -0,0 +1,12 @@ +Matrix-OOB.dfy(12,26): Error: index 0 out of range
+Execution trace:
+ (0,0): anon0
+Matrix-OOB.dfy(12,26): Error: index 1 out of range
+Execution trace:
+ (0,0): anon0
+Matrix-OOB.dfy(13,0): Error BP5003: A postcondition might not hold on this return path.
+Matrix-OOB.dfy(12,10): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 0 verified, 3 errors
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy index 05dbced0..7b207d74 100644 --- a/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy @@ -17,9 +17,9 @@ method M() }
else
{
- assert (exists b: bool :: b || !b) || 4 != 4;
+ assert (exists b: bool :: true) || 4 != 4;
}
- assert (exists b: bool :: b || !b) || 5 != 5;
+ assert (exists b: bool :: true) || 5 != 5;
}
diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy.expect b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect index 2ad73416..8148a8cf 100644 --- a/Test/dafny0/snapshots/Snapshots5.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect @@ -18,9 +18,9 @@ Processing command (at Snapshots5.v1.dfy(12,4)) assert (forall<alpha> $o: ref, $ >>> MarkAsFullyVerified
Processing command (at Snapshots5.v1.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;
>>> MarkAsFullyVerified
-Processing command (at Snapshots5.v1.dfy(20,40)) assert (exists b#5: bool :: b#5 || !b#5) || 4 != 4;
+Processing command (at Snapshots5.v1.dfy(20,37)) assert (exists b#5: bool :: Lit(true)) || 4 != 4;
>>> DoNothingToAssert
-Processing command (at Snapshots5.v1.dfy(22,38)) assert (exists b#7: bool :: b#7 || !b#7) || 5 != 5;
+Processing command (at Snapshots5.v1.dfy(22,35)) assert (exists b#7: bool :: Lit(true)) || 5 != 5;
>>> DoNothingToAssert
Dafny program verifier finished with 3 verified, 0 errors
diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect index 270f7e57..6f5ed3d7 100644 --- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect +++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect @@ -2,7 +2,7 @@ loop-detection-is-not-too-strict.dfy(14,9): Info: Selected triggers: {P(y, x)}, {P(x, y)}
loop-detection-is-not-too-strict.dfy(17,9): Info: Selected triggers:
{P(y, x)}, {P(x, y)}
-loop-detection-is-not-too-strict.dfy(20,9): Warning: Selected triggers: {P(x, y)} (loops with {P(x, y + 1)})
+loop-detection-is-not-too-strict.dfy(20,9): Warning: Selected triggers: {P(x, y)} (may loop with {P(x, y + 1)})
(!) Suppressing loops would leave this expression without triggers.
Dafny program verifier finished with 3 verified, 0 errors
diff --git a/Test/triggers/loop-detection-looks-at-ranges-too.dfy b/Test/triggers/loop-detection-looks-at-ranges-too.dfy new file mode 100644 index 00000000..7a99ea2d --- /dev/null +++ b/Test/triggers/loop-detection-looks-at-ranges-too.dfy @@ -0,0 +1,14 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file checks that loops between the range and the term of a quantifier
+// are properly detected.
+
+predicate P(x: int)
+
+method M(x: int) {
+ // This will be flagged as a loop even without looking at the range
+ assert true || forall x: int | P(x) :: P(x+1);
+ // This requires checking the range for looping terms
+ assert true || forall x: int | P(x+1) :: P(x);
+}
diff --git a/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect new file mode 100644 index 00000000..ce62d868 --- /dev/null +++ b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect @@ -0,0 +1,6 @@ +loop-detection-looks-at-ranges-too.dfy(11,17): Warning: Selected triggers: {P(x)} (may loop with {P(x + 1)})
+ (!) Suppressing loops would leave this expression without triggers.
+loop-detection-looks-at-ranges-too.dfy(13,17): Warning: Selected triggers: {P(x)} (may loop with {P(x + 1)})
+ (!) Suppressing loops would leave this expression without triggers.
+
+Dafny program verifier finished with 3 verified, 0 errors
diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect index 89d7265c..804a0116 100644 --- a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect +++ b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect @@ -1,21 +1,21 @@ loop-detection-messages--unit-tests.dfy(11,9): Info: Selected triggers: {f(f(i))}
- Rejected triggers: {f(i)} (loops with {f(f(i))})
-loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (loops with {f(i + 1)})
+ Rejected triggers: {f(i)} (may loop with {f(f(i))})
+loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (may loop with {f(i + 1)})
(!) Suppressing loops would leave this expression without triggers.
-loop-detection-messages--unit-tests.dfy(13,9): Info: Selected triggers: {f(i)} (loops with {f(i + 1)})
+loop-detection-messages--unit-tests.dfy(13,9): Info: Selected triggers: {f(i)} (may loop with {f(i + 1)})
loop-detection-messages--unit-tests.dfy(15,9): Info: For expression {false ==> f(i) == f(i + 1)}:
Selected triggers: {g(i)}
- Rejected triggers: {f(i)} (loops with {f(i + 1)})
+ Rejected triggers: {f(i)} (may loop with {f(i + 1)})
loop-detection-messages--unit-tests.dfy(15,9): Info: For expression {false ==> f(i) == g(i)}:
Selected triggers:
{g(i)}, {f(i)}
loop-detection-messages--unit-tests.dfy(16,9): Warning: For expression {false ==> f(i) == f(i + 1)}:
- Selected triggers: {f(i)} (loops with {f(i + 1)})
+ Selected triggers: {f(i)} (may loop with {f(i + 1)})
(!) Suppressing loops would leave this expression without triggers.
loop-detection-messages--unit-tests.dfy(16,9): Info: For expression {false ==> f(i) == f(i)}:
Selected triggers: {f(i)}
loop-detection-messages--unit-tests.dfy(17,9): Info: For expression {false ==> f(i) == f(i + 1)}:
- Selected triggers: {f(i)} (loops with {f(i + 1)})
+ Selected triggers: {f(i)} (may loop with {f(i + 1)})
loop-detection-messages--unit-tests.dfy(17,9): Info: For expression {false ==> f(i) == f(i)}:
Selected triggers: {f(i)}
loop-detection-messages--unit-tests.dfy(19,9): Info: Selected triggers: {f(i)}
diff --git a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect index c0eebdba..58094110 100644 --- a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect +++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect @@ -1,10 +1,10 @@ looping-is-hard-to-decide-modulo-equality.dfy(21,9): Info: Selected triggers:
{h(h(c, j), j)}, {h(c, i)}, {c in sc}
- Rejected triggers: {h(c, j)} (loops with {h(h(c, j), j)})
+ Rejected triggers: {h(c, j)} (may loop with {h(h(c, j), j)})
looping-is-hard-to-decide-modulo-equality.dfy(26,9): Info: Selected triggers: {f(x)}
Rejected triggers: {g(f(x))} (more specific than {f(x)})
looping-is-hard-to-decide-modulo-equality.dfy(31,9): Info: Selected triggers:
{old(f(f(c)))}, {f(c)}, {c in sc}
- Rejected triggers: {old(f(c))} (loops with {old(f(f(c)))})
+ Rejected triggers: {old(f(c))} (may loop with {old(f(f(c)))})
Dafny program verifier finished with 9 verified, 0 errors
diff --git a/Test/triggers/matrix-accesses-are-triggers.dfy b/Test/triggers/matrix-accesses-are-triggers.dfy new file mode 100644 index 00000000..630fab9d --- /dev/null +++ b/Test/triggers/matrix-accesses-are-triggers.dfy @@ -0,0 +1,9 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file checks that multi-dimensional array accesses yield trigger candidates
+
+method M(m: array2<int>)
+ requires m != null
+ requires forall i, j | 0 <= i < m.Length0 && 0 <= j < m.Length1 :: m[i, j] == m[j, i+1] {
+}
diff --git a/Test/triggers/matrix-accesses-are-triggers.dfy.expect b/Test/triggers/matrix-accesses-are-triggers.dfy.expect new file mode 100644 index 00000000..35df02f5 --- /dev/null +++ b/Test/triggers/matrix-accesses-are-triggers.dfy.expect @@ -0,0 +1,12 @@ +matrix-accesses-are-triggers.dfy(8,11): Warning: Selected triggers: {m[i, j]} (may loop with {m[j, i + 1]})
+ (!) Suppressing loops would leave this expression without triggers.
+matrix-accesses-are-triggers.dfy(8,81): Error: index 0 out of range
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Then
+matrix-accesses-are-triggers.dfy(8,86): Error: index 1 out of range
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Then
+
+Dafny program verifier finished with 1 verified, 2 errors
diff --git a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect index 23ec089d..313d7c16 100644 --- a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect +++ b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect @@ -2,14 +2,14 @@ old-is-a-special-case-for-triggers.dfy(15,10): Info: Selected triggers: {old(f(c))}, {c in sc}
old-is-a-special-case-for-triggers.dfy(20,10): Info: Selected triggers:
{old(f(f(c)))}, {f(c)}, {c in sc}
- Rejected triggers: {old(f(c))} (loops with {old(f(f(c)))})
+ Rejected triggers: {old(f(c))} (may loop with {old(f(f(c)))})
old-is-a-special-case-for-triggers.dfy(21,10): Info: Selected triggers:
{f(g(c))}, {g(f(c))}, {old(f(g(c)))}, {old(g(f(c)))}, {old(f(f(c)))}, {c in sc}
Rejected triggers:
- {g(c)} (loops with {g(f(c))})
- {f(c)} (loops with {f(g(c))})
- {old(g(c))} (loops with {old(g(f(c)))})
- {old(f(c))} (loops with {old(f(f(c)))}, {old(f(g(c)))})
+ {g(c)} (may loop with {g(f(c))})
+ {f(c)} (may loop with {f(g(c))})
+ {old(g(c))} (may loop with {old(g(f(c)))})
+ {old(f(c))} (may loop with {old(f(f(c)))}, {old(f(g(c)))})
old-is-a-special-case-for-triggers.dfy(25,10): Info: Selected triggers:
{old(f(c))}, {f(c)}, {c in sc}
Rejected triggers: {old(g(f(c)))} (more specific than {old(f(c))})
diff --git a/Test/triggers/regression-tests.dfy b/Test/triggers/regression-tests.dfy new file mode 100644 index 00000000..263e424a --- /dev/null +++ b/Test/triggers/regression-tests.dfy @@ -0,0 +1,20 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This tests checks that quantifier splitting is resilient to the fact that +// certain statements (like calc) can return duplicate subexpressions. This was +// once a problem, because a quantifier that got returned twice would get split +// on the first pass over it, and would have its nely created children re-split +// on the second pass. This created a split quantifier whose children were split +// quantifiers, which violated an invariant of spliit quantifiers. + +abstract module Base { } + +module Blah refines Base { + lemma A() { + calc { + forall b :: b; + } + } +} + diff --git a/Test/triggers/regression-tests.dfy.expect b/Test/triggers/regression-tests.dfy.expect new file mode 100644 index 00000000..a03810fb --- /dev/null +++ b/Test/triggers/regression-tests.dfy.expect @@ -0,0 +1,3 @@ +regression-tests.dfy(16,5): Warning: (!) No terms found to trigger on.
+
+Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect index 83648626..f5e47454 100644 --- a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect +++ b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect @@ -1,10 +1,10 @@ -some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (loops with {s[x + 1]})
+some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (may loop with {s[x + 1]})
(!) Suppressing loops would leave this expression without triggers.
some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression {x in s ==> s[x + 1] > 0}:
- Selected triggers: {s[x]} (loops with {s[x + 1]})
+ Selected triggers: {s[x]} (may loop with {s[x + 1]})
(!) Suppressing loops would leave this expression without triggers.
some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression {x in s ==> x + 2 !in s}:
- Selected triggers: {s[x]} (loops with {x + 2 !in s})
+ Selected triggers: {s[x]} (may loop with {x + 2 !in s})
(!) Suppressing loops would leave this expression without triggers.
Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/triggers/splitting-picks-the-right-tokens.dfy b/Test/triggers/splitting-picks-the-right-tokens.dfy new file mode 100644 index 00000000..76065eca --- /dev/null +++ b/Test/triggers/splitting-picks-the-right-tokens.dfy @@ -0,0 +1,24 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file ensures that trigger splitting picks the right tokens
+
+function Id(i: int): int { i }
+
+method MSuchThat()
+ requires forall x | x > 0 :: Id(x) > 1 && x > 2 && x > -1 { }
+
+method MImplies()
+ // The bodies of the two terms that are produced here are both
+ // BinaryExpressions(==>); the token they use, however, is that of the RHS
+ // terms of these implications; otherwise, error messages would get stacked on
+ // the ==> sign
+ requires forall x :: x > 0 ==> Id(x) > 1 && x > 2 && x > -1 { }
+
+method M() {
+ if * {
+ MImplies();
+ } else {
+ MSuchThat();
+ }
+}
diff --git a/Test/triggers/splitting-picks-the-right-tokens.dfy.expect b/Test/triggers/splitting-picks-the-right-tokens.dfy.expect new file mode 100644 index 00000000..af274e75 --- /dev/null +++ b/Test/triggers/splitting-picks-the-right-tokens.dfy.expect @@ -0,0 +1,38 @@ +splitting-picks-the-right-tokens.dfy(9,11): Info: For expression {Id(x) > 1}:
+ Selected triggers: {Id(x)}
+splitting-picks-the-right-tokens.dfy(9,11): Info: For expression {x > 2}:
+ Selected triggers: {Id(x)}
+splitting-picks-the-right-tokens.dfy(9,11): Info: For expression {x > -1}:
+ Selected triggers: {Id(x)}
+splitting-picks-the-right-tokens.dfy(16,11): Info: For expression {x > 0 ==> Id(x) > 1}:
+ Selected triggers: {Id(x)}
+splitting-picks-the-right-tokens.dfy(16,11): Info: For expression {x > 0 ==> x > 2}:
+ Selected triggers: {Id(x)}
+splitting-picks-the-right-tokens.dfy(16,11): Info: For expression {x > 0 ==> x > -1}:
+ Selected triggers: {Id(x)}
+splitting-picks-the-right-tokens.dfy(20,12): Error BP5002: A precondition for this call might not hold.
+splitting-picks-the-right-tokens.dfy(16,11): Related location: This is the precondition that might not hold.
+splitting-picks-the-right-tokens.dfy(16,48): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+splitting-picks-the-right-tokens.dfy(20,12): Error BP5002: A precondition for this call might not hold.
+splitting-picks-the-right-tokens.dfy(16,11): Related location: This is the precondition that might not hold.
+splitting-picks-the-right-tokens.dfy(16,39): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+splitting-picks-the-right-tokens.dfy(22,13): Error BP5002: A precondition for this call might not hold.
+splitting-picks-the-right-tokens.dfy(9,11): Related location: This is the precondition that might not hold.
+splitting-picks-the-right-tokens.dfy(9,46): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+splitting-picks-the-right-tokens.dfy(22,13): Error BP5002: A precondition for this call might not hold.
+splitting-picks-the-right-tokens.dfy(9,11): Related location: This is the precondition that might not hold.
+splitting-picks-the-right-tokens.dfy(9,37): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+
+Dafny program verifier finished with 6 verified, 4 errors
diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect index 63cbc476..58c8dd2b 100644 --- a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect +++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect @@ -1,11 +1,11 @@ splitting-triggers-recovers-expressivity.dfy(12,10): Info: Selected triggers: {Q(i)}
- Rejected triggers: {P(i)} (loops with {P(i + 1)})
+ Rejected triggers: {P(i)} (may loop with {P(i + 1)})
splitting-triggers-recovers-expressivity.dfy(17,11): Info: Selected triggers: {Q(j)}
- Rejected triggers: {P(j)} (loops with {P(j + 1)})
+ Rejected triggers: {P(j)} (may loop with {P(j + 1)})
splitting-triggers-recovers-expressivity.dfy(26,10): Info: Selected triggers: {Q(i)}
- Rejected triggers: {P(i)} (loops with {P(i + 1)})
+ Rejected triggers: {P(i)} (may loop with {P(i + 1)})
splitting-triggers-recovers-expressivity.dfy(33,11): Info: Selected triggers: {Q(j)}
- Rejected triggers: {P(j)} (loops with {P(j + 1)})
+ Rejected triggers: {P(j)} (may loop with {P(j + 1)})
splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i)}:
Selected triggers:
{Q(i)}, {P(i)}
@@ -14,19 +14,19 @@ splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {!Q(i) {Q(i)}, {P(i)}
splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i + 1)}:
Selected triggers: {Q(i)}
- Rejected triggers: {P(i)} (loops with {P(i + 1)})
+ Rejected triggers: {P(i)} (may loop with {P(i + 1)})
splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression {j >= 0 ==> P(j)}:
Selected triggers:
{Q(j)}, {P(j)}
splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression {j >= 0 ==> Q(j) ==> P(j + 1)}:
Selected triggers: {Q(j)}
- Rejected triggers: {P(j)} (loops with {P(j + 1)})
+ Rejected triggers: {P(j)} (may loop with {P(j + 1)})
splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression {i >= 0 ==> Q(i)}:
Selected triggers:
{P(i)}, {Q(i)}
splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression {i >= 0 ==> P(i) ==> P(i + 1)}:
Selected triggers:
- {P(i)} (loops with {P(i + 1)}), {Q(i)}
+ {P(i)} (may loop with {P(i + 1)}), {Q(i)}
splitting-triggers-recovers-expressivity.dfy(12,63): Error BP5003: A postcondition might not hold on this return path.
splitting-triggers-recovers-expressivity.dfy(12,10): Related location: This is the postcondition that might not hold.
Execution trace:
diff --git a/Test/triggers/useless-triggers-are-removed.dfy.expect b/Test/triggers/useless-triggers-are-removed.dfy.expect index a526e517..2e9bbedf 100644 --- a/Test/triggers/useless-triggers-are-removed.dfy.expect +++ b/Test/triggers/useless-triggers-are-removed.dfy.expect @@ -5,11 +5,11 @@ useless-triggers-are-removed.dfy(16,11): Info: Selected triggers: {f(x)} {h(f(x))} (more specific than {f(x)})
{g(f(x))} (more specific than {f(x)})
useless-triggers-are-removed.dfy(20,11): Info: Selected triggers: {f(f(x))}
- Rejected triggers: {f(x)} (loops with {f(f(x))})
+ Rejected triggers: {f(x)} (may loop with {f(f(x))})
useless-triggers-are-removed.dfy(23,11): Info: Selected triggers:
{g(f(x)), g(y)}, {f(y), f(x)}
Rejected triggers:
- {g(y), f(x)} (loops with {g(f(y))}, {g(f(x))})
+ {g(y), f(x)} (may loop with {g(f(y))}, {g(f(x))})
{g(f(x)), g(f(y))} (more specific than {g(f(x)), f(y)}, {g(f(y)), f(x)}, {f(y), f(x)})
{g(f(x)), f(y)} (more specific than {f(y), f(x)})
{g(f(y)), f(x)} (more specific than {f(y), f(x)})
diff --git a/Test/tutorial/maximum.dfy.expect b/Test/tutorial/maximum.dfy.expect index 70768304..16a67088 100644 --- a/Test/tutorial/maximum.dfy.expect +++ b/Test/tutorial/maximum.dfy.expect @@ -1,7 +1,7 @@ -maximum.dfy(11,10): Info: Selected triggers: {values[i]} -maximum.dfy(18,14): Info: Selected triggers: {values[j]} -maximum.dfy(28,27): Info: Selected triggers: {values[i]} -maximum.dfy(29,27): Info: Selected triggers: {values[i]} -maximum.dfy(15,2): Info: decreases int(|values|) - int(idx) - -Dafny program verifier finished with 4 verified, 0 errors +maximum.dfy(11,10): Info: Selected triggers: {values[i]}
+maximum.dfy(18,14): Info: Selected triggers: {values[j]}
+maximum.dfy(28,27): Info: Selected triggers: {values[i]}
+maximum.dfy(29,27): Info: Selected triggers: {values[i]}
+maximum.dfy(15,2): Info: decreases |values| - idx
+
+Dafny program verifier finished with 4 verified, 0 errors
diff --git a/Test/wishlist/exists-b-exists-not-b.dfy b/Test/wishlist/exists-b-exists-not-b.dfy new file mode 100644 index 00000000..711c5611 --- /dev/null +++ b/Test/wishlist/exists-b-exists-not-b.dfy @@ -0,0 +1,10 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// It would be great if Dafny was able to verify the following statements;
+// otherwise, trigger splitting prevents `exists b :: b || not b` from verifying
+
+method M() {
+ assert exists b: bool :: b; // WISH
+ assert exists b: bool :: !b; // WISH
+}
diff --git a/Test/wishlist/exists-b-exists-not-b.dfy.expect b/Test/wishlist/exists-b-exists-not-b.dfy.expect new file mode 100644 index 00000000..c785ee97 --- /dev/null +++ b/Test/wishlist/exists-b-exists-not-b.dfy.expect @@ -0,0 +1,8 @@ +exists-b-exists-not-b.dfy(8,9): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+exists-b-exists-not-b.dfy(9,9): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 1 verified, 2 errors
diff --git a/Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy b/Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy new file mode 100644 index 00000000..9b002d47 --- /dev/null +++ b/Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy @@ -0,0 +1,9 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method M() {
+ var pos := 10;
+ while (pos > 0) { // This shouldn't print int(pos) - int(0); pos - 0 would be better
+ pos := pos - 1;
+ }
+}
diff --git a/Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy.expect b/Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy.expect new file mode 100644 index 00000000..36d7e6b8 --- /dev/null +++ b/Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy.expect @@ -0,0 +1,3 @@ +useless-casts-in-decreases-clauses.dfy(6,2): Info: decreases pos - 0
+
+Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/wishlist/naked-function-in-recursive-setting.dfy b/Test/wishlist/naked-function-in-recursive-setting.dfy new file mode 100644 index 00000000..650fc4c3 --- /dev/null +++ b/Test/wishlist/naked-function-in-recursive-setting.dfy @@ -0,0 +1,13 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function fact(n: int): int
+ requires n >= 0
+{
+ if n == 0 then
+ 1
+ else (
+ assert fact.requires(n-1); //WISH
+ n * fact(n-1)
+ )
+}
diff --git a/Test/wishlist/naked-function-in-recursive-setting.dfy.expect b/Test/wishlist/naked-function-in-recursive-setting.dfy.expect new file mode 100644 index 00000000..4b1691b4 --- /dev/null +++ b/Test/wishlist/naked-function-in-recursive-setting.dfy.expect @@ -0,0 +1,8 @@ +naked-function-in-recursive-setting.dfy(4,9): Info: decreases n
+naked-function-in-recursive-setting.dfy(10,11): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Execution trace:
+ (0,0): anon0
+ (0,0): anon7_Else
+ (0,0): anon8_Else
+
+Dafny program verifier finished with 0 verified, 1 error
|