diff options
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 2 | ||||
-rw-r--r-- | Source/Dafny/Rewriter.cs | 1 | ||||
-rw-r--r-- | Source/Dafny/Triggers/QuantifierSplitter.cs | 42 | ||||
-rw-r--r-- | Test/triggers/regression-tests.dfy | 20 | ||||
-rw-r--r-- | Test/triggers/regression-tests.dfy.expect | 3 |
5 files changed, 60 insertions, 8 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index c4ea0a5a..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; }
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/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index 83059f8d..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) {
@@ -83,16 +98,29 @@ namespace Microsoft.Dafny.Triggers { 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/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
|