From 23067608f2d8855abd64982cabfe7f0c7f8e4f5a Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 6 Nov 2015 13:51:08 -0800 Subject: Fix issue 99. When annotate a quantifier expr that has a SplitQuantifier, we need exclude the private terms (the ones that includes the quantifier expr's bv) from it exported terms. --- Source/Dafny/Triggers/TriggersCollector.cs | 4 ++-- Test/dafny4/Bug99.dfy | 11 +++++++++++ Test/dafny4/Bug99.dfy.expect | 2 ++ 3 files changed, 15 insertions(+), 2 deletions(-) create mode 100644 Test/dafny4/Bug99.dfy create mode 100644 Test/dafny4/Bug99.dfy.expect diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index c25f65b9..698ea3b5 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -201,8 +201,8 @@ namespace Microsoft.Dafny.Triggers { (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); - } else if (expr is QuantifierExpr && ((QuantifierExpr)expr).SplitQuantifier == null) { - annotation = AnnotateQuantifier((QuantifierExpr)expr); + } else if (expr is QuantifierExpr) { + annotation = AnnotateQuantifier((QuantifierExpr)expr); } else if (expr is LetExpr) { annotation = AnnotateLetExpr((LetExpr)expr); } else if (expr is IdentifierExpr) { diff --git a/Test/dafny4/Bug99.dfy b/Test/dafny4/Bug99.dfy new file mode 100644 index 00000000..3f95ce9f --- /dev/null +++ b/Test/dafny4/Bug99.dfy @@ -0,0 +1,11 @@ +// RUN: %dafny /autoTriggers:1 /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +predicate P(e:int, p:int) { true } +predicate Q(i:int, t:int) + +lemma Tester(x:int) +{ + assert forall i :: Q(i, x) ==> (forall p {:trigger P(i, p)} :: P(i, p)); + +} diff --git a/Test/dafny4/Bug99.dfy.expect b/Test/dafny4/Bug99.dfy.expect new file mode 100644 index 00000000..73ba063c --- /dev/null +++ b/Test/dafny4/Bug99.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 4 verified, 0 errors -- cgit v1.2.3 From 324c2f4bf8842cce7922e7ff7972216dfc06546f Mon Sep 17 00:00:00 2001 From: qunyanm Date: Tue, 10 Nov 2015 15:53:39 -0800 Subject: Fix issue 101. Instead of swapping operands for Exp opcode in BinaryExpr, swap them when the expr is first created in parser or for calcstmt. This avoids problems of operands being swapped again when the expr is copied. --- Source/Dafny/Dafny.atg | 7 +++++-- Source/Dafny/DafnyAst.cs | 17 ++++++++--------- Source/Dafny/Parser.cs | 5 +++-- Test/dafny4/Bug101.dfy | 19 +++++++++++++++++++ Test/dafny4/Bug101.dfy.expect | 8 ++++++++ 5 files changed, 43 insertions(+), 13 deletions(-) create mode 100644 Test/dafny4/Bug101.dfy create mode 100644 Test/dafny4/Bug101.dfy.expect diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 5fa1085d..ff3b75a3 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -2175,10 +2175,13 @@ ImpliesExpliesExpression ( ImpliesOp (. x = t; .) ImpliesExpression (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .) | ExpliesOp (. x = t; .) - LogicalExpression (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .) + LogicalExpression (. // The order of operands is reversed so that it can be turned into implication during resolution + e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); .) { IF(IsExpliesOp()) /* read a reverse implication as far as possible */ ExpliesOp (. x = t; .) - LogicalExpression (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .) + LogicalExpression (. //The order of operands is reversed so that it can be turned into implication during resolution + e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); + .) } ) ] diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index fdbd484e..9ed3b7e0 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -4885,7 +4885,12 @@ namespace Microsoft.Dafny { public override Expression StepExpr(Expression line0, Expression line1) { - return new BinaryExpr(line0.tok, Op, line0, line1); + if (Op == BinaryExpr.Opcode.Exp) { + // The order of operands is reversed so that it can be turned into implication during resolution + return new BinaryExpr(line0.tok, Op, line1, line0); + } else { + return new BinaryExpr(line0.tok, Op, line0, line1); + } } public override string ToString() @@ -6779,14 +6784,8 @@ namespace Microsoft.Dafny { Contract.Requires(e0 != null); Contract.Requires(e1 != null); this.Op = op; - if (op == Opcode.Exp) { - // The order of operands is reversed so that it can be turned into implication during resolution - this.E0 = e1; - this.E1 = e0; - } else { - this.E0 = e0; - this.E1 = e1; - } + this.E0 = e0; + this.E1 = e1; } /// diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 6a5f32ab..b6a59f4e 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -3267,12 +3267,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ExpliesOp(); x = t; LogicalExpression(out e1, allowSemi, allowLambda); - e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); + e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); while (IsExpliesOp()) { ExpliesOp(); x = t; LogicalExpression(out e1, allowSemi, allowLambda); - e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); + e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); + } } else SynErr(219); } diff --git a/Test/dafny4/Bug101.dfy b/Test/dafny4/Bug101.dfy new file mode 100644 index 00000000..878ed57a --- /dev/null +++ b/Test/dafny4/Bug101.dfy @@ -0,0 +1,19 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +predicate P(i:int) { true } + +lemma Tester() +{ +// forall i ensures false ==> P(i) {} + forall i ensures P(i) <== false {} + assert forall i :: P(i) ==> false; + assert P(0); + assert false; +} + + + + + + diff --git a/Test/dafny4/Bug101.dfy.expect b/Test/dafny4/Bug101.dfy.expect new file mode 100644 index 00000000..a4e5f4b3 --- /dev/null +++ b/Test/dafny4/Bug101.dfy.expect @@ -0,0 +1,8 @@ +Bug101.dfy(10,11): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon6_Else + (0,0): anon7_Then + (0,0): anon5 + +Dafny program verifier finished with 2 verified, 1 error -- cgit v1.2.3