diff options
Diffstat (limited to 'Source/Dafny/Rewriter.cs')
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 273 |
1 files changed, 273 insertions, 0 deletions
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index d9db03c7..9a898cbe 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -72,6 +72,279 @@ namespace Microsoft.Dafny }
}
+ // write out the quantifier for ForallStmt
+ public class ForallStmtRewriter : IRewriter
+ {
+ public ForallStmtRewriter(ErrorReporter reporter) : base(reporter) {
+ Contract.Requires(reporter != null);
+ }
+
+ internal override void PostResolve(ModuleDefinition m) {
+ var forallvisiter = new ForAllStmtVisitor();
+ foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
+ forallvisiter.Visit(decl, true);
+ }
+ }
+
+ internal class ForAllStmtVisitor : TopDownVisitor<bool>
+ {
+ protected override bool VisitOneStmt(Statement stmt, ref bool st) {
+ Contract.Requires(stmt != null);
+ if (stmt is ForallStmt) {
+ ForallStmt s = (ForallStmt)stmt;
+ if (s.Kind == ForallStmt.ParBodyKind.Proof) {
+ Expression term = s.Ens.Count != 0 ? s.Ens[0].E : new LiteralExpr(s.Tok, true);
+ for (int i = 1; i < s.Ens.Count; i++) {
+ term = new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.And, term, s.Ens[i].E);
+ }
+ List<Expression> exprList = new List<Expression>();
+ ForallExpr expr = new ForallExpr(s.Tok, s.BoundVars, s.Range, term, s.Attributes);
+ expr.Type = Type.Bool; // resolve here
+ exprList.Add(expr);
+ s.ForallExpressions = exprList;
+ } else if (s.Kind == ForallStmt.ParBodyKind.Assign) {
+ if (s.BoundVars.Count != 0) {
+ var s0 = (AssignStmt)s.S0;
+ if (s0.Rhs is ExprRhs) {
+ List<Expression> exprList = new List<Expression>();
+ Expression Fi = null;
+ Func<Expression, Expression> lhsBuilder = null;
+ var lhs = s0.Lhs.Resolved;
+ var i = s.BoundVars[0];
+ if (s.BoundVars.Count == 1) {
+ //var lhsContext = null;
+ // Detect the following cases:
+ // 0: forall i | R(i) { F(i).f := E(i); }
+ // 1: forall i | R(i) { A[F(i)] := E(i); }
+ // 2: forall i | R(i) { F(i)[N] := E(i); }
+ if (lhs is MemberSelectExpr) {
+ var ll = (MemberSelectExpr)lhs;
+ Fi = ll.Obj;
+ lhsBuilder = e => { var l = new MemberSelectExpr(ll.tok, e, ll.MemberName); l.Member = ll.Member; l.Type = ll.Type; return l; };
+ } else if (lhs is SeqSelectExpr) {
+ var ll = (SeqSelectExpr)lhs;
+ Contract.Assert(ll.SelectOne);
+ if (!Translator.ContainsFreeVariable(ll.Seq, false, i)) {
+ Fi = ll.E0;
+ lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, ll.Seq, e, null); l.Type = ll.Type; return l; };
+ } else if (!Translator.ContainsFreeVariable(ll.E0, false, i)) {
+ Fi = ll.Seq;
+ lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, e, ll.E0, null); l.Type = ll.Type; return l; };
+ }
+ }
+ }
+ var rhs = ((ExprRhs)s0.Rhs).Expr;
+ bool usedInversion = false;
+ if (Fi != null) {
+ var j = new BoundVar(i.tok, i.Name + "#inv", Fi.Type);
+ var jj = Expression.CreateIdentExpr(j);
+ var jList = new List<BoundVar>() { j };
+ var vals = InvertExpression(i, j, s.Range, Fi);
+#if DEBUG_PRINT
+ Console.WriteLine("DEBUG: Trying to invert:");
+ Console.WriteLine("DEBUG: " + Printer.ExprToString(s.Range) + " && " + j.Name + " == " + Printer.ExprToString(Fi));
+ if (vals == null) {
+ Console.WriteLine("DEBUG: Can't");
+ } else {
+ Console.WriteLine("DEBUG: The inverse is the disjunction of the following:");
+ foreach (var val in vals) {
+ Console.WriteLine("DEBUG: " + Printer.ExprToString(val.Range) + " && " + Printer.ExprToString(val.FInverse) + " == " + i.Name);
+ }
+ }
+#endif
+ if (vals != null) {
+ foreach (var val in vals) {
+ lhs = lhsBuilder(jj);
+ Attributes attributes = new Attributes("trigger", new List<Expression>() { lhs }, s.Attributes);
+ var expr = new ForallExpr(s.Tok, jList, val.Range, new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.EqCommon, lhs, Substitute(rhs, i, val.FInverse)), attributes);
+ expr.Type = Type.Bool; //resolve here
+ exprList.Add(expr);
+ }
+ usedInversion = true;
+ }
+ }
+ if (!usedInversion) {
+ var expr = new ForallExpr(s.Tok, s.BoundVars, s.Range, new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.EqCommon, lhs, rhs), s.Attributes);
+ expr.Type = Type.Bool; // resolve here
+ exprList.Add(expr);
+ }
+ s.ForallExpressions = exprList;
+ }
+ }
+ } else if (s.Kind == ForallStmt.ParBodyKind.Call) {
+ var s0 = (CallStmt)s.S0;
+ Expression term = s0.Method.Ens.Count != 0 ? s0.Method.Ens[0].E : new LiteralExpr(s.Tok, true);
+ for (int i = 1; i < s0.Method.Ens.Count; i++) {
+ term = new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.And, term, s0.Method.Ens[i].E);
+ }
+ List<Expression> exprList = new List<Expression>();
+ ForallExpr expr = new ForallExpr(s.Tok, s.BoundVars, s.Range, term, s.Attributes);
+ expr.Type = Type.Bool; // resolve here
+ exprList.Add(expr);
+ } else {
+ Contract.Assert(false); // unexpected kind
+ }
+ }
+ return true; //visit the sub-parts with the same "st"
+ }
+
+ internal class ForallStmtTranslationValues
+ {
+ public readonly Expression Range;
+ public readonly Expression FInverse;
+ public ForallStmtTranslationValues(Expression range, Expression fInverse) {
+ Contract.Requires(range != null);
+ Contract.Requires(fInverse != null);
+ Range = range;
+ FInverse = fInverse;
+ }
+ public ForallStmtTranslationValues Subst(IVariable j, Expression e) {
+ Contract.Requires(j != null);
+ Contract.Requires(e != null);
+ Dictionary<TypeParameter, Type> typeMap = new Dictionary<TypeParameter, Type>();
+ var substMap = new Dictionary<IVariable, Expression>();
+ substMap.Add(j, e);
+ Translator.Substituter sub = new Translator.Substituter(null, substMap, typeMap, null);
+ var v = new ForallStmtTranslationValues(sub.Substitute(Range), sub.Substitute(FInverse));
+ return v;
+ }
+ }
+
+ /// <summary>
+ /// Find piecewise inverse of F under R. More precisely, find lists of expressions P and F-1
+ /// such that
+ /// R(i) && j == F(i)
+ /// holds iff the disjunction of the following predicates holds:
+ /// P_0(j) && F-1_0(j) == i
+ /// ...
+ /// P_{n-1}(j) && F-1_{n-1}(j) == i
+ /// If no such disjunction is found, return null.
+ /// If such a disjunction is found, return for each disjunct:
+ /// * The predicate P_k(j), which is an expression that may have free occurrences of j (but no free occurrences of i)
+ /// * The expression F-1_k(j), which also may have free occurrences of j but not of i
+ /// </summary>
+ private List<ForallStmtTranslationValues> InvertExpression(BoundVar i, BoundVar j, Expression R, Expression F) {
+ Contract.Requires(i != null);
+ Contract.Requires(j != null);
+ Contract.Requires(R != null);
+ Contract.Requires(F != null);
+ var vals = new List<ForallStmtTranslationValues>(InvertExpressionIter(i, j, R, F));
+ if (vals.Count == 0) {
+ return null;
+ } else {
+ return vals;
+ }
+ }
+ /// <summary>
+ /// See InvertExpression.
+ /// </summary>
+ private IEnumerable<ForallStmtTranslationValues> InvertExpressionIter(BoundVar i, BoundVar j, Expression R, Expression F) {
+ Contract.Requires(i != null);
+ Contract.Requires(j != null);
+ Contract.Requires(R != null);
+ Contract.Requires(F != null);
+ F = F.Resolved;
+ if (!Translator.ContainsFreeVariable(F, false, i)) {
+ // We're looking at R(i) && j == K.
+ // We cannot invert j == K, but if we're lucky, R(i) contains a conjunct i==G.
+ Expression r = Expression.CreateBoolLiteral(R.tok, true);
+ Expression G = null;
+ foreach (var c in Expression.Conjuncts(R)) {
+ if (G == null && c is BinaryExpr) {
+ var bin = (BinaryExpr)c;
+ if (BinaryExpr.IsEqualityOp(bin.ResolvedOp)) {
+ var id = bin.E0.Resolved as IdentifierExpr;
+ if (id != null && id.Var == i) {
+ G = bin.E1;
+ continue;
+ }
+ id = bin.E1.Resolved as IdentifierExpr;
+ if (id != null && id.Var == i) {
+ G = bin.E0;
+ continue;
+ }
+ }
+ }
+ r = Expression.CreateAnd(r, c);
+ }
+ if (G != null) {
+ var jIsK = Expression.CreateEq(Expression.CreateIdentExpr(j), F, j.Type);
+ var rr = Substitute(r, i, G);
+ yield return new ForallStmtTranslationValues(Expression.CreateAnd(rr, jIsK), G);
+ }
+ } else if (F is IdentifierExpr) {
+ var e = (IdentifierExpr)F;
+ if (e.Var == i) {
+ // We're looking at R(i) && j == i, which is particularly easy to invert: R(j) && j == i
+ var jj = Expression.CreateIdentExpr(j);
+ yield return new ForallStmtTranslationValues(Substitute(R, i, jj), jj);
+ }
+ } else if (F is BinaryExpr) {
+ var bin = (BinaryExpr)F;
+ if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) {
+ if (!Translator.ContainsFreeVariable(bin.E1, false, i)) {
+ // We're looking at: R(i) && j == f(i) + K.
+ // By a recursive call, we'll ask to invert: R(i) && j' == f(i).
+ // For each P_0(j') && f-1_0(j') == i we get back, we yield:
+ // P_0(j - K) && f-1_0(j - K) == i
+ var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E1);
+ foreach (var val in InvertExpression(i, j, R, bin.E0)) {
+ yield return val.Subst(j, jMinusK);
+ }
+ } else if (!Translator.ContainsFreeVariable(bin.E0, false, i)) {
+ // We're looking at: R(i) && j == K + f(i)
+ // Do as in previous case, but with operands reversed.
+ var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E0);
+ foreach (var val in InvertExpression(i, j, R, bin.E1)) {
+ yield return val.Subst(j, jMinusK);
+ }
+ }
+ } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) {
+ if (!Translator.ContainsFreeVariable(bin.E1, false, i)) {
+ // We're looking at: R(i) && j == f(i) - K
+ // Recurse on f(i) and then replace j := j + K
+ var jPlusK = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E1);
+ foreach (var val in InvertExpression(i, j, R, bin.E0)) {
+ yield return val.Subst(j, jPlusK);
+ }
+ } else if (!Translator.ContainsFreeVariable(bin.E0, false, i)) {
+ // We're looking at: R(i) && j == K - f(i)
+ // Recurse on f(i) and then replace j := K - j
+ var kMinusJ = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E0);
+ foreach (var val in InvertExpression(i, j, R, bin.E1)) {
+ yield return val.Subst(j, kMinusJ);
+ }
+ }
+ }
+ } else if (F is ITEExpr) {
+ var ife = (ITEExpr)F;
+ // We're looking at R(i) && j == if A(i) then B(i) else C(i), which is equivalent to the disjunction of:
+ // R(i) && A(i) && j == B(i)
+ // R(i) && !A(i) && j == C(i)
+ // We recurse on each one, yielding the results
+ var r = Expression.CreateAnd(R, ife.Test);
+ var valsThen = InvertExpression(i, j, r, ife.Thn);
+ if (valsThen != null) {
+ r = Expression.CreateAnd(R, Expression.CreateNot(ife.tok, ife.Test));
+ var valsElse = InvertExpression(i, j, r, ife.Els);
+ if (valsElse != null) {
+ foreach (var val in valsThen) { yield return val; }
+ foreach (var val in valsElse) { yield return val; }
+ }
+ }
+ }
+ }
+
+ Expression Substitute(Expression expr, IVariable v, Expression e) {
+ Dictionary<IVariable, Expression/*!*/> substMap = new Dictionary<IVariable, Expression>();
+ Dictionary<TypeParameter, Type> typeMap = new Dictionary<TypeParameter, Type>();
+ substMap.Add(v, e);
+ Translator.Substituter sub = new Translator.Substituter(null, substMap, typeMap, null);
+ return sub.Substitute(expr);
+ }
+ }
+ }
+
/// <summary>
/// AutoContracts is an experimental feature that will fill much of the dynamic-frames boilerplate
/// into a class. From the user's perspective, what needs to be done is simply:
|