From c0f3a8d08762275bab645d666ed6a2e566701ff4 Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Mon, 9 Jul 2012 18:08:44 -0700 Subject: Dafny: added verification that replaced expressions are the same as the original --- Source/Dafny/Dafny.atg | 2 +- Source/Dafny/DafnyAst.cs | 18 ++++++++++++------ Source/Dafny/Parser.cs | 2 +- Source/Dafny/RefinementTransformer.cs | 14 +++++++------- Source/Dafny/Resolver.cs | 1 + Source/Dafny/Translator.cs | 24 +++++++++++++++--------- 6 files changed, 37 insertions(+), 24 deletions(-) (limited to 'Source') diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 958726fd..c63c5d3c 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1504,7 +1504,7 @@ NamedExpr NoUSIdent ":" Expression (. expr = e; - e = new NamedExpr(x, d, expr); .) + e = new NamedExpr(x, d.val, expr); .) . MatchExpression diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index c2a4ace3..d20d0d56 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -904,7 +904,7 @@ namespace Microsoft.Dafny { } public class DefaultModuleDecl : ModuleDefinition { - public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null, false) { + public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null, true) { } public override bool IsDefaultModule { get { @@ -3382,25 +3382,31 @@ namespace Microsoft.Dafny { } } } - + // Represents expr Name: Body + // or expr Name: (assert Body == Contract; Body) public class NamedExpr : Expression { public readonly string Name; public readonly Expression Body; - public NamedExpr(IToken tok, IToken name, Expression body) + public readonly Expression Contract; + public readonly IToken ReplacerToken; + + public NamedExpr(IToken tok, string p, Expression body) : base(tok) { - Name = name.val; + Name = p; Body = body; } - - public NamedExpr(IToken tok, string p, Expression body) + public NamedExpr(IToken tok, string p, Expression body, Expression contract, IToken token) : base(tok) { Name = p; Body = body; + Contract = contract; + ReplacerToken = token; } public override IEnumerable SubExpressions { get { yield return Body; + if (Contract != null) yield return Contract; } } } diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 6adc4df0..b8324dab 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -2658,7 +2658,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(5); Expression(out e); expr = e; - e = new NamedExpr(x, d, expr); + e = new NamedExpr(x, d.val, expr); } void CaseExpression(out MatchCaseExpr/*!*/ c) { diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 68ab2c20..d27ef13d 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -806,7 +806,7 @@ namespace Microsoft.Dafny { return nw; } - private Statement SubstituteNamedExpr(Statement s, string p, Expression E, ref int subCount) { + private Statement SubstituteNamedExpr(Statement s, IToken p, Expression E, ref int subCount) { if (s == null) { return null; } else if (s is AssertStmt) { @@ -886,15 +886,15 @@ namespace Microsoft.Dafny { } } - private Expression SubstituteNamedExpr(Expression expr, string p, Expression E, ref int subCount) { + private Expression SubstituteNamedExpr(Expression expr, IToken p, Expression E, ref int subCount) { if (expr == null) { return null; } if (expr is NamedExpr) { NamedExpr n = (NamedExpr)expr; - if (n.Name == p) { + if (n.Name == p.val) { subCount++; - return new NamedExpr(n.tok, n.Name, E); + return new NamedExpr(n.tok, n.Name, E, CloneExpr(n.Body), p); } else return new NamedExpr(n.tok, n.Name, SubstituteNamedExpr(n.Body, p, E, ref subCount)); } else if (expr is LiteralExpr || expr is WildcardExpr | expr is ThisExpr || expr is IdentifierExpr) { return expr; @@ -1021,7 +1021,7 @@ namespace Microsoft.Dafny { } } - private List SubstituteNamedExprList(List list, string p, Expression E, ref int subCount) { + private List SubstituteNamedExprList(List list, IToken p, Expression E, ref int subCount) { List res = new List(); foreach (Expression e in list) { res.Add(SubstituteNamedExpr(e, p, E, ref subCount)); @@ -1165,14 +1165,14 @@ namespace Microsoft.Dafny { // loop invariant: oldS == oldStmt.Body[j] var s = CloneStmt(oldS); if (c.NameReplacements != null) - s = SubstituteNamedExpr(s, c.NameReplacements[0].val, c.ExprReplacements[0], ref subCount); + s = SubstituteNamedExpr(s, c.NameReplacements[0], c.ExprReplacements[0], ref subCount); body.Add(s); j++; if (j == oldStmt.Body.Count) { break; } oldS = oldStmt.Body[j]; } if (c.NameReplacements != null && subCount == 0) - reporter.Error(c.NameReplacements[0], "did not find expression labeld {0}", c.NameReplacements[0].val); + reporter.Error(c.NameReplacements[0], "did not find expression labeled {0}", c.NameReplacements[0].val); } i++; diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index b226c3fe..33f86258 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -3906,6 +3906,7 @@ namespace Microsoft.Dafny { } else if (expr is NamedExpr) { var e = (NamedExpr)expr; ResolveExpression(e.Body, twoState); + if (e.Contract != null) ResolveExpression(e.Contract, twoState); e.Type = e.Body.Type; }else if (expr is QuantifierExpr) { QuantifierExpr e = (QuantifierExpr)expr; diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 5d0baaed..75b2e845 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -2050,7 +2050,11 @@ namespace Microsoft.Dafny { return BplAnd(canCall, CanCallAssumption(etran.GetSubstitutedBody(e), etran)); } else if (expr is NamedExpr) { - return CanCallAssumption(((NamedExpr)expr).Body, etran); + var e = (NamedExpr)expr; + var canCall = CanCallAssumption(e.Body, etran); + if (e.Contract != null) + return BplAnd(canCall, CanCallAssumption(e.Contract, etran)); + else return canCall; } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; var total = CanCallAssumption(e.Term, etran); @@ -2080,9 +2084,7 @@ namespace Microsoft.Dafny { total = BplAnd(total, Bpl.Expr.Imp(test, CanCallAssumption(e.Thn, etran))); total = BplAnd(total, Bpl.Expr.Imp(Bpl.Expr.Not(test), CanCallAssumption(e.Els, etran))); return total; - } else if (expr is NamedExpr) { - return CanCallAssumption(((NamedExpr)expr).Body, etran); - } else if (expr is ConcreteSyntaxExpression) { + } else if (expr is ConcreteSyntaxExpression) { var e = (ConcreteSyntaxExpression)expr; return CanCallAssumption(e.ResolvedExpression, etran); } else { @@ -2517,7 +2519,13 @@ namespace Microsoft.Dafny { result = null; } else if (expr is NamedExpr) { - CheckWellformedWithResult(((NamedExpr)expr).Body, options, result, resultType, locals, builder, etran); + var e = (NamedExpr)expr; + CheckWellformedWithResult(e.Body, options, result, resultType, locals, builder, etran); + if (e.Contract != null) { + CheckWellformedWithResult(e.Contract, options, result, resultType, locals, builder, etran); + var theSame = Bpl.Expr.Eq(etran.TrExpr(e.Body), etran.TrExpr(e.Contract)); + builder.Add(Assert(new ForceCheckToken(e.ReplacerToken), theSame, "replacement must be the same value")); + } } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; var substMap = SetupBoundVarsAsLocals(e.BoundVars, builder, locals, etran); @@ -6011,7 +6019,6 @@ namespace Microsoft.Dafny { } else if (expr is LetExpr) { var e = (LetExpr)expr; return TrExpr(GetSubstitutedBody(e)); - } else if (expr is NamedExpr) { return TrExpr(((NamedExpr)expr).Body); } else if (expr is QuantifierExpr) { @@ -7684,9 +7691,8 @@ namespace Microsoft.Dafny { } else if (expr is NamedExpr) { var e = (NamedExpr)expr; var body = Substitute(e.Body, receiverReplacement, substMap); - if (body != e.Body) { - newExpr = new NamedExpr(e.tok, e.Name, body); - } + var contract = e.Contract == null ? null : Substitute(e.Contract, receiverReplacement, substMap); + newExpr = new NamedExpr(e.tok, e.Name, body, contract, e.ReplacerToken); } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap); -- cgit v1.2.3