diff options
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 9 | ||||
| -rw-r--r-- | Source/Dafny/Cloner.cs | 25 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 10 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 151 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 10 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 25 | ||||
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 288 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 14 | ||||
| -rw-r--r-- | Source/DafnyExtension/DafnyRuntime.cs | 9 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 42 | ||||
| -rw-r--r-- | Test/dafny0/AutoReq.dfy | 288 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 |
12 files changed, 854 insertions, 19 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 3afac587..2d033b0d 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -581,6 +581,15 @@ namespace Dafny yield return true;
}
}
+ public static IEnumerable<BigInteger> AllIntegers {
+ get {
+ yield return new BigInteger(0);
+ for (var j = new BigInteger(1);; j++) {
+ yield return j;
+ yield return -j;
+ }
+ }
+ }
// pre: b != 0
// post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 7a057a62..6928d9b9 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -123,7 +123,7 @@ namespace Microsoft.Dafny }
}
- public Type CloneType(Type t) {
+ virtual public Type CloneType(Type t) {
if (t is BasicType) {
return t;
} else if (t is SetType) {
@@ -200,7 +200,9 @@ namespace Microsoft.Dafny return null;
} else if (expr is LiteralExpr) {
var e = (LiteralExpr)expr;
- if (e.Value == null) {
+ if (e is StaticReceiverExpr) {
+ return new StaticReceiverExpr(e.tok, e.Type);
+ } else if (e.Value == null) {
return new LiteralExpr(Tok(e.tok));
} else if (e.Value is bool) {
return new LiteralExpr(Tok(e.tok), (bool)e.Value);
@@ -706,4 +708,23 @@ namespace Microsoft.Dafny return base.CloneStmt(stmt);
}
}
+
+
+ class ResolvedCloner : Cloner {
+
+ public override Type CloneType(Type t) {
+ Type new_t = base.CloneType(t);
+
+ if (t is UserDefinedType) {
+ var tt = (UserDefinedType)t;
+ var new_tt = (UserDefinedType)new_t;
+
+ new_tt.ResolvedClass = tt.ResolvedClass;
+ new_tt.ResolvedParam = tt.ResolvedParam;
+ }
+
+ return new_t;
+ }
+ }
+
}
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 7ab47d7d..9382e764 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1106,14 +1106,14 @@ namespace Microsoft.Dafny { // for (BigInteger iterLimit = 5; ; iterLimit *= 2) {
// var il$0 = iterLimit;
// foreach (L l' in sq.Elements) { l = l';
- // il$0--; if (il$0 == 0) { break; }
+ // if (il$0 == 0) { break; } il$0--;
// var il$1 = iterLimit;
// foreach (K k' in st.Elements) { k = k';
- // il$1--; if (il$1 == 0) { break; }
+ // if (il$1 == 0) { break; } il$1--;
// var il$2 = iterLimit;
// j = Lo;
// for (;; j++) {
- // il$2--; if (il$2 == 0) { break; }
+ // if (il$2 == 0) { break; } il$2--;
// foreach (bool i' in Helper.AllBooleans) { i = i';
// if (R(i,j,k,l)) {
// goto ASSIGN_SUCH_THAT_<id>;
@@ -1179,6 +1179,8 @@ namespace Microsoft.Dafny { Indent(ind);
wr.WriteLine("for (;; @{0}--) {{ ", bv.CompileName);
}
+ } else if (bound is AssignSuchThatStmt.WiggleWaggleBound) {
+ wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllIntegers) {{ @{1} = {0};", tmpVar, bv.CompileName);
} else if (bound is ComprehensionExpr.SetBoundedPool) {
var b = (ComprehensionExpr.SetBoundedPool)bound;
wr.Write("foreach (var {0} in (", tmpVar);
@@ -1207,7 +1209,7 @@ namespace Microsoft.Dafny { }
if (needIterLimit) {
Indent(ind + IndentAmount);
- wr.WriteLine("{0}_{1}--; if ({0}_{1} == 0) {{ break; }}", iterLimit, i);
+ wr.WriteLine("if ({0}_{1} == 0) {{ break; }} {0}_{1}--;", iterLimit, i);
}
}
Indent(ind);
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 75b30afd..a0530a5b 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -169,6 +169,33 @@ namespace Microsoft.Dafny { return false;
}
+ /// <summary>
+ /// Checks whether a Boolean attribute has been set on the declaration itself,
+ /// the enclosing class, or any enclosing module. Settings closer to the declaration
+ /// override those further away.
+ /// </summary>
+ public static bool ContainsBoolAtAnyLevel(MemberDecl decl, string attribName) {
+ bool setting = true;
+ if (Attributes.ContainsBool(decl.Attributes, attribName, ref setting)) {
+ return setting;
+ }
+
+ if (Attributes.ContainsBool(decl.EnclosingClass.Attributes, attribName, ref setting)) {
+ return setting;
+ }
+
+ // Check the entire stack of modules
+ var mod = decl.EnclosingClass.Module;
+ while (mod != null) {
+ if (Attributes.ContainsBool(mod.Attributes, attribName, ref setting)) {
+ return setting;
+ }
+ mod = mod.Module;
+ }
+
+ return false;
+ }
+
public class Argument
{
public readonly IToken Tok;
@@ -2765,6 +2792,12 @@ namespace Microsoft.Dafny { // invariant Bounds == null || Bounds.Count == BoundVars.Count;
public List<IVariable> MissingBounds; // filled in during resolution; remains "null" if bounds can be found
// invariant Bounds == null || MissingBounds == null;
+ public class WiggleWaggleBound : ComprehensionExpr.BoundedPool
+ {
+ public override bool IsFinite {
+ get { return false; }
+ }
+ }
/// <summary>
/// "assumeToken" is allowed to be "null", in which case the verifier will check that a RHS value exists.
@@ -3939,6 +3972,24 @@ namespace Microsoft.Dafny { }
/// <summary>
+ /// Create a resolved expression for a bool b
+ /// </summary>
+ public static Expression CreateBoolLiteral(IToken tok, bool b) {
+ Contract.Requires(tok != null);
+ var lit = new LiteralExpr(tok, b);
+ lit.Type = Type.Bool; // resolve here
+ return lit;
+ }
+
+ public static Expression CreateNot(IToken tok, Expression e) {
+ Contract.Requires(tok != null);
+ Contract.Requires(e.Type is BoolType);
+ var un = new UnaryExpr(tok, UnaryExpr.Opcode.Not, e);
+ un.Type = Type.Bool; // resolve here
+ return un;
+ }
+
+ /// <summary>
/// Create a resolved expression of the form "e0 LESS e1"
/// </summary>
public static Expression CreateLess(Expression e0, Expression e1) {
@@ -4017,6 +4068,99 @@ namespace Microsoft.Dafny { ite.Type = e0.type; // resolve here
return ite;
}
+
+ /// <summary>
+ /// Create a resolved case expression for a match expression
+ /// </summary>
+ public static MatchCaseExpr CreateMatchCase(MatchCaseExpr old_case, Expression new_body) {
+ Contract.Requires(old_case != null);
+ Contract.Requires(new_body != null);
+ Contract.Ensures(Contract.Result<MatchCaseExpr>() != null);
+
+ ResolvedCloner cloner = new ResolvedCloner();
+ var newVars = old_case.Arguments.ConvertAll(cloner.CloneBoundVar);
+ new_body = VarSubstituter(old_case.Arguments, newVars, new_body);
+
+ var new_case = new MatchCaseExpr(old_case.tok, old_case.Id, newVars, new_body);
+
+ new_case.Ctor = old_case.Ctor; // resolve here
+ return new_case;
+ }
+
+ /// <summary>
+ /// Create a match expression with a resolved type
+ /// </summary>
+ public static Expression CreateMatch(IToken tok, Expression src, List<MatchCaseExpr> cases, Type type) {
+ MatchExpr e = new MatchExpr(tok, src, cases);
+ e.Type = type; // resolve here
+
+ return e;
+ }
+
+ /// <summary>
+ /// Create a let expression with a resolved type and fresh variables
+ /// </summary>
+ public static Expression CreateLet(IToken tok, List<BoundVar> vars, List<Expression> RHSs, Expression body, bool exact) {
+ Contract.Requires(tok != null);
+ Contract.Requires(vars != null && RHSs != null);
+ Contract.Requires(vars.Count == RHSs.Count);
+ Contract.Requires(body != null);
+
+ ResolvedCloner cloner = new ResolvedCloner();
+ var newVars = vars.ConvertAll(cloner.CloneBoundVar);
+ body = VarSubstituter(vars, newVars, body);
+
+ var let = new LetExpr(tok, newVars, RHSs, body, exact);
+ let.Type = body.Type; // resolve here
+ return let;
+ }
+
+ /// <summary>
+ /// Create a quantifier expression with a resolved type and fresh variables
+ /// Optionally replace the old body with the supplied argument
+ /// </summary>
+ public static Expression CreateQuantifier(QuantifierExpr expr, bool forall, Expression body = null) {
+ //(IToken tok, List<BoundVar> vars, Expression range, Expression body, Attributes attribs, Qu) {
+ Contract.Requires(expr != null);
+
+ ResolvedCloner cloner = new ResolvedCloner();
+ var newVars = expr.BoundVars.ConvertAll(cloner.CloneBoundVar);
+
+ if (body == null) {
+ body = expr.Term;
+ }
+
+ body = VarSubstituter(expr.BoundVars, newVars, body);
+
+ QuantifierExpr q;
+ if (forall) {
+ q = new ForallExpr(expr.tok, newVars, expr.Range, body, expr.Attributes);
+ } else {
+ q = new ExistsExpr(expr.tok, newVars, expr.Range, body, expr.Attributes);
+ }
+ q.Type = Type.Bool;
+
+ return q;
+ }
+
+ private static Expression VarSubstituter(List<BoundVar> oldVars, List<BoundVar> newVars, Expression e) {
+ Contract.Requires(oldVars != null && newVars != null);
+ Contract.Requires(oldVars.Count == newVars.Count);
+
+ Dictionary<IVariable, Expression/*!*/> substMap = new Dictionary<IVariable, Expression>();
+ Dictionary<TypeParameter, Type> typeMap = new Dictionary<TypeParameter, Type>();
+
+ for (int i = 0; i < oldVars.Count; i++) {
+ var id = new IdentifierExpr(newVars[i].tok, newVars[i].Name);
+ id.Var = newVars[i]; // Resolve here manually
+ id.Type = newVars[i].Type; // Resolve here manually
+ substMap.Add(oldVars[i], id);
+ }
+
+ Translator.Substituter sub = new Translator.Substituter(null, substMap, typeMap, null);
+ return sub.Substitute(e);
+ }
+
}
/// <summary>
@@ -4025,6 +4169,13 @@ namespace Microsoft.Dafny { /// </summary>
public class StaticReceiverExpr : LiteralExpr
{
+ public StaticReceiverExpr(IToken tok, Type t)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(t != null);
+ Type = t;
+ }
+
public StaticReceiverExpr(IToken tok, ClassDecl cl)
: base(tok) // constructs a LiteralExpr representing the 'null' literal
{
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index d9b6abae..e4912efc 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -36,6 +36,16 @@ namespace Microsoft.Dafny { }
}
+
+ public static string ExtendedExprToString(Expression expr) {
+ Contract.Requires(expr != null);
+ using (var wr = new System.IO.StringWriter()) {
+ var pr = new Printer(wr);
+ pr.PrintExtendedExpr(expr, 0, true, false);
+ return wr.ToString();
+ }
+ }
+
public static string IteratorClassToString(IteratorDecl iter) {
Contract.Requires(iter != null);
using (var wr = new System.IO.StringWriter()) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 0b84ed36..bd6c1d8b 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -192,6 +192,7 @@ namespace Microsoft.Dafny rewriters.Add(refinementTransformer);
rewriters.Add(new AutoContractsRewriter());
rewriters.Add(new OpaqueFunctionRewriter());
+ rewriters.Add(new AutoReqFunctionRewriter(this));
systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false);
foreach (var decl in sortedDecls) {
@@ -394,6 +395,10 @@ namespace Microsoft.Dafny void FillInDefaultDecreases(ICallable clbl) {
Contract.Requires(clbl != null);
+ if (clbl is CoPredicate) {
+ // copredicates don't have decreases clauses
+ return;
+ }
var decr = clbl.Decreases.Expressions;
if (decr.Count == 0 || (clbl is PrefixMethod && decr.Count == 1)) {
// The default for a function starts with the function's reads clause, if any
@@ -1146,7 +1151,9 @@ namespace Microsoft.Dafny return null;
} else if (expr is LiteralExpr) {
var e = (LiteralExpr)expr;
- if (e.Value == null) {
+ if (e is StaticReceiverExpr) {
+ return new StaticReceiverExpr(e.tok, e.Type);
+ } else if (e.Value == null) {
return new LiteralExpr(e.tok);
} else if (e.Value is bool) {
return new LiteralExpr(e.tok, (bool)e.Value);
@@ -4685,7 +4692,7 @@ namespace Microsoft.Dafny var missingBounds = new List<IVariable>();
CheckTypeInference(s.Expr); // we need to resolve operators before the call to DiscoverBoundsAux
- var allBounds = DiscoverBoundsAux(s.Tok, varLhss, s.Expr, true, true, missingBounds);
+ var allBounds = DiscoverBoundsAux(s.Tok, varLhss, s.Expr, true, true, true, missingBounds);
if (missingBounds.Count != 0) {
s.MissingBounds = missingBounds; // so that an error message can be produced during compilation
} else {
@@ -6879,7 +6886,7 @@ namespace Microsoft.Dafny /// For a description, see DiscoverBoundsAux.
/// </summary>
public static List<ComprehensionExpr.BoundedPool> DiscoverBounds<VT>(IToken tok, List<VT> bvars, Expression expr, bool polarity, bool returnAllBounds, List<VT> missingBounds) where VT : IVariable {
- var pairs = DiscoverBoundsAux(tok, bvars, expr, polarity, returnAllBounds, missingBounds);
+ var pairs = DiscoverBoundsAux(tok, bvars, expr, polarity, returnAllBounds, false, missingBounds);
if (pairs == null) {
return null;
}
@@ -6904,8 +6911,10 @@ namespace Microsoft.Dafny /// -- a non-null return value means that some bound were found for each variable (but, for example, perhaps one
/// variable only has lower bounds, no upper bounds)
/// Requires "expr" to be successfully resolved.
+ /// If "allowAnyIntegers", then integer variables will always be given a bound, but this bound may be WiggleWaggle if
+ /// there is no better bound.
/// </summary>
- public static List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>> DiscoverBoundsAux<VT>(IToken tok, List<VT> bvars, Expression expr, bool polarity, bool returnAllBounds, List<VT> missingBounds) where VT : IVariable {
+ public static List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>> DiscoverBoundsAux<VT>(IToken tok, List<VT> bvars, Expression expr, bool polarity, bool returnAllBounds, bool allowAnyIntegers, List<VT> missingBounds) where VT : IVariable {
Contract.Requires(tok != null);
Contract.Requires(bvars != null);
Contract.Requires(missingBounds != null);
@@ -7034,8 +7043,12 @@ namespace Microsoft.Dafny }
if (!foundBoundsForBv) {
// we have checked every conjunct in the range expression and still have not discovered good bounds
- missingBounds.Add(bv); // record failing bound variable
- foundError = true;
+ if (allowAnyIntegers && bv.Type is IntType) {
+ bounds.Add(new AssignSuchThatStmt.WiggleWaggleBound());
+ } else {
+ missingBounds.Add(bv); // record failing bound variable
+ foundError = true;
+ }
}
}
CHECK_NEXT_BOUND_VARIABLE: ; // should goto here only if the bound for the current variable has been discovered (otherwise, return with null from this method)
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 26a3a70c..601ef935 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -523,4 +523,292 @@ namespace Microsoft.Dafny }
}
}
+
+
+ /// <summary>
+ /// Automatically accumulate requires for function calls within a function body,
+ /// if requested via {:autoreq}
+ /// </summary>
+ public class AutoReqFunctionRewriter : IRewriter {
+ Function parentFunction;
+ Resolver resolver;
+ bool containsMatch; // TODO: Track this per-requirement, rather than per-function
+
+ public AutoReqFunctionRewriter(Resolver r) {
+ this.resolver = r;
+ }
+
+ public void PreResolve(ModuleDefinition m) {
+ }
+
+ public void PostResolve(ModuleDefinition m) {
+ var components = m.CallGraph.TopologicallySortedComponents();
+
+ foreach (var scComponent in components) { // Visit the call graph bottom up, so anything we call already has its prequisites calculated
+ if (scComponent is Function) {
+ Function fn = (Function)scComponent;
+ if (Attributes.ContainsBoolAtAnyLevel(fn, "autoReq")) {
+ parentFunction = fn; // Remember where the recursion started
+ containsMatch = false; // Assume no match statements are involved
+
+ List<Expression> auto_reqs = new List<Expression>();
+
+ // First handle all of the requirements' preconditions
+ foreach (Expression req in fn.Req) {
+ auto_reqs.AddRange(generateAutoReqs(req));
+ }
+
+ // Then the body itself, if any
+ if (fn.Body != null) {
+ auto_reqs.AddRange(generateAutoReqs(fn.Body));
+ }
+
+ fn.Req.InsertRange(0, auto_reqs);
+ addAutoReqToolTipInfo(fn, auto_reqs);
+ }
+ }
+ }
+ }
+
+ public void addAutoReqToolTipInfo(Function f, List<Expression> reqs) {
+ string prefix = "auto requires ";
+ string tip = "";
+
+ foreach (var req in reqs) {
+ if (containsMatch) { // Pretty print the requirements
+ tip += prefix + Printer.ExtendedExprToString(req) + ";\n";
+ } else {
+ tip += prefix + Printer.ExprToString(req) + ";\n";
+ }
+ }
+
+ if (!tip.Equals("")) {
+ resolver.ReportAdditionalInformation(f.tok, tip, f.tok.val.Length);
+ }
+ }
+
+ // Stitch a list of expressions together with logical ands
+ Expression andify(Bpl.IToken tok, List<Expression> exprs) {
+ Expression ret = Expression.CreateBoolLiteral(tok, true);
+
+ foreach (var expr in exprs) {
+ ret = Expression.CreateAnd(ret, expr);
+ }
+
+ return ret;
+ }
+
+ List<Expression> gatherReqs(Function f, List<Expression> args, Expression f_this) {
+ List<Expression> translated_f_reqs = new List<Expression>();
+
+ if (f.Req.Count > 0) {
+ Dictionary<IVariable, Expression/*!*/> substMap = new Dictionary<IVariable,Expression>();
+ Dictionary<TypeParameter, Type> typeMap = new Dictionary<TypeParameter,Type>();
+
+ for (int i = 0; i < f.Formals.Count; i++) {
+ substMap.Add(f.Formals[i], args[i]);
+ }
+
+ foreach (var req in f.Req) {
+ Translator.Substituter sub = new Translator.Substituter(f_this, substMap, typeMap, null);
+ translated_f_reqs.Add(sub.Substitute(req));
+ }
+ }
+
+ return translated_f_reqs;
+ }
+
+ List<Expression> generateAutoReqs(Expression expr) {
+ List<Expression> reqs = new List<Expression>();
+
+ if (expr is LiteralExpr) {
+ } else if (expr is ThisExpr) {
+ } else if (expr is IdentifierExpr) {
+ } else if (expr is SetDisplayExpr) {
+ SetDisplayExpr e = (SetDisplayExpr)expr;
+
+ foreach (var elt in e.Elements) {
+ reqs.AddRange(generateAutoReqs(elt));
+ }
+ } else if (expr is MultiSetDisplayExpr) {
+ MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr;
+ foreach (var elt in e.Elements) {
+ reqs.AddRange(generateAutoReqs(elt));
+ }
+ } else if (expr is SeqDisplayExpr) {
+ SeqDisplayExpr e = (SeqDisplayExpr)expr;
+ foreach (var elt in e.Elements) {
+ reqs.AddRange(generateAutoReqs(elt));
+ }
+ } else if (expr is MapDisplayExpr) {
+ MapDisplayExpr e = (MapDisplayExpr)expr;
+
+ foreach (ExpressionPair p in e.Elements) {
+ reqs.AddRange(generateAutoReqs(p.A));
+ reqs.AddRange(generateAutoReqs(p.B));
+ }
+ } else if (expr is FieldSelectExpr) {
+ FieldSelectExpr e = (FieldSelectExpr)expr;
+ Contract.Assert(e.Field != null);
+
+ reqs.AddRange(generateAutoReqs(e.Obj));
+ } else if (expr is SeqSelectExpr) {
+ SeqSelectExpr e = (SeqSelectExpr)expr;
+
+ reqs.AddRange(generateAutoReqs(e.Seq));
+ if (e.E0 != null) {
+ reqs.AddRange(generateAutoReqs(e.E0));
+ }
+
+ if (e.E1 != null) {
+ reqs.AddRange(generateAutoReqs(e.E1));
+ }
+ } else if (expr is SeqUpdateExpr) {
+ SeqUpdateExpr e = (SeqUpdateExpr)expr;
+ reqs.AddRange(generateAutoReqs(e.Seq));
+ reqs.AddRange(generateAutoReqs(e.Index));
+ reqs.AddRange(generateAutoReqs(e.Value));
+ } else if (expr is FunctionCallExpr) {
+ FunctionCallExpr e = (FunctionCallExpr)expr;
+
+ // All of the arguments need to be satisfied
+ foreach (var arg in e.Args) {
+ reqs.AddRange(generateAutoReqs(arg));
+ }
+
+ ModuleDefinition module = e.Function.EnclosingClass.Module;
+ if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(parentFunction)) {
+ // We're making a call within the same SCC, so don't descend into this function
+ } else {
+ reqs.AddRange(gatherReqs(e.Function, e.Args, e.Receiver));
+ }
+ } else if (expr is DatatypeValue) {
+ DatatypeValue dtv = (DatatypeValue)expr;
+ Contract.Assert(dtv.Ctor != null); // since dtv has been successfully resolved
+ for (int i = 0; i < dtv.Arguments.Count; i++) {
+ Expression arg = dtv.Arguments[i];
+ reqs.AddRange(generateAutoReqs(arg));
+ }
+ } else if (expr is OldExpr) {
+ } else if (expr is MatchExpr) {
+ MatchExpr e = (MatchExpr)expr;
+ containsMatch = true;
+ reqs.AddRange(generateAutoReqs(e.Source));
+
+ List<MatchCaseExpr> newMatches = new List<MatchCaseExpr>();
+ foreach (MatchCaseExpr caseExpr in e.Cases) {
+ //MatchCaseExpr c = new MatchCaseExpr(caseExpr.tok, caseExpr.Id, caseExpr.Arguments, andify(caseExpr.tok, generateAutoReqs(caseExpr.Body)));
+ //c.Ctor = caseExpr.Ctor; // resolve here
+ MatchCaseExpr c = Expression.CreateMatchCase(caseExpr, andify(caseExpr.tok, generateAutoReqs(caseExpr.Body)));
+ newMatches.Add(c);
+ }
+
+ reqs.Add(Expression.CreateMatch(e.tok, e.Source, newMatches, e.Type));
+ } else if (expr is MultiSetFormingExpr) {
+ MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
+ reqs.AddRange(generateAutoReqs(e.E));
+ } else if (expr is FreshExpr) {
+ } else if (expr is UnaryExpr) {
+ UnaryExpr e = (UnaryExpr)expr;
+ Expression arg = e.E;
+ reqs.AddRange(generateAutoReqs(arg));
+ } else if (expr is BinaryExpr) {
+ BinaryExpr e = (BinaryExpr)expr;
+
+ switch (e.ResolvedOp) {
+ case BinaryExpr.ResolvedOpcode.Imp:
+ case BinaryExpr.ResolvedOpcode.And:
+ reqs.AddRange(generateAutoReqs(e.E0));
+ foreach (var req in generateAutoReqs(e.E1)) {
+ // We only care about this req if E0 is true, since And short-circuits
+ reqs.Add(Expression.CreateImplies(e.E0, req));
+ }
+ break;
+
+ case BinaryExpr.ResolvedOpcode.Or:
+ reqs.AddRange(generateAutoReqs(e.E0));
+ foreach (var req in generateAutoReqs(e.E1)) {
+ // We only care about this req if E0 is false, since Or short-circuits
+ reqs.Add(Expression.CreateImplies(Expression.CreateNot(e.E1.tok, e.E0), req));
+ }
+ break;
+
+ default:
+ reqs.AddRange(generateAutoReqs(e.E0));
+ reqs.AddRange(generateAutoReqs(e.E1));
+ break;
+ }
+ } else if (expr is TernaryExpr) {
+ var e = (TernaryExpr)expr;
+
+ reqs.AddRange(generateAutoReqs(e.E0));
+ reqs.AddRange(generateAutoReqs(e.E1));
+ reqs.AddRange(generateAutoReqs(e.E2));
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+
+ if (e.Exact) {
+ foreach (var rhs in e.RHSs) {
+ reqs.AddRange(generateAutoReqs(rhs));
+ }
+ var new_reqs = generateAutoReqs(e.Body);
+ if (new_reqs.Count > 0) {
+ reqs.Add(Expression.CreateLet(e.tok, e.Vars, e.RHSs, andify(e.tok, new_reqs), e.Exact));
+ }
+ } else {
+ // TODO: Still need to figure out what the right choice is here:
+ // Given: var x :| g(x); f(x, y) do we:
+ // 1) Update the original statement to be: var x :| g(x) && WP(f(x,y)); f(x, y)
+ // 2) Add forall x :: g(x) ==> WP(f(x, y)) to the function's requirements
+ // 3) Current option -- do nothing. Up to the spec writer to fix
+ }
+ } else if (expr is NamedExpr) {
+ reqs.AddRange(generateAutoReqs(((NamedExpr)expr).Body));
+ } else if (expr is QuantifierExpr) {
+ QuantifierExpr e = (QuantifierExpr)expr;
+
+ // See LetExpr for issues with the e.Range
+
+ var auto_reqs = generateAutoReqs(e.Term);
+ if (auto_reqs.Count > 0) {
+ reqs.Add(Expression.CreateQuantifier(e, true, andify(e.Term.tok, auto_reqs)));
+ }
+ } else if (expr is SetComprehension) {
+ var e = (SetComprehension)expr;
+ // Translate "set xs | R :: T"
+
+ // See LetExpr for issues with the e.Range
+ //reqs.AddRange(generateAutoReqs(e.Range));
+ var auto_reqs = generateAutoReqs(e.Term);
+ if (auto_reqs.Count > 0) {
+ reqs.Add(Expression.CreateQuantifier(new ForallExpr(e.tok, e.BoundVars, e.Range, andify(e.Term.tok, auto_reqs), e.Attributes), true));
+ }
+ } else if (expr is MapComprehension) {
+ var e = (MapComprehension)expr;
+ // Translate "map x | R :: T" into
+ // See LetExpr for issues with the e.Range
+ //reqs.AddRange(generateAutoReqs(e.Range));
+ var auto_reqs = generateAutoReqs(e.Term);
+ if (auto_reqs.Count > 0) {
+ reqs.Add(Expression.CreateQuantifier(new ForallExpr(e.tok, e.BoundVars, e.Range, andify(e.Term.tok, auto_reqs), e.Attributes), true));
+ }
+ } else if (expr is StmtExpr) {
+ var e = (StmtExpr)expr;
+ reqs.AddRange(generateAutoReqs(e.E));
+ } else if (expr is ITEExpr) {
+ ITEExpr e = (ITEExpr)expr;
+ reqs.AddRange(generateAutoReqs(e.Test));
+ reqs.Add(Expression.CreateITE(e.Test, andify(e.Thn.tok, generateAutoReqs(e.Thn)), andify(e.Els.tok, generateAutoReqs(e.Els))));
+ } else if (expr is ConcreteSyntaxExpression) {
+ var e = (ConcreteSyntaxExpression)expr;
+ reqs.AddRange(generateAutoReqs(e.ResolvedExpression));
+ } else {
+ //Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
+ }
+
+ return reqs;
+ }
+ }
}
+
+
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index e5d0920d..82093900 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -10327,7 +10327,6 @@ namespace Microsoft.Dafny { public Substituter(Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap, Dictionary<TypeParameter, Type> typeMap, Translator translator) {
Contract.Requires(substMap != null);
Contract.Requires(typeMap != null);
- Contract.Requires(translator != null);
this.receiverReplacement = receiverReplacement;
this.substMap = substMap;
this.typeMap = typeMap;
@@ -10521,11 +10520,14 @@ namespace Microsoft.Dafny { return e;
}
var newLet = new LetExpr(e.tok, e.LHSs, new List<Expression>{ rhs }, body, e.Exact);
- Expression d = translator.LetDesugaring(e);
- newLet.translationDesugaring = Substitute(d);
- var info = translator.letSuchThatExprInfo[e];
- translator.letSuchThatExprInfo.Add(newLet, new LetSuchThatExprInfo(info, translator, substMap));
- newExpr = newLet;
+ if (translator != null)
+ {
+ Expression d = translator.LetDesugaring(e);
+ newLet.translationDesugaring = Substitute(d);
+ var info = translator.letSuchThatExprInfo[e];
+ translator.letSuchThatExprInfo.Add(newLet, new LetSuchThatExprInfo(info, translator, substMap));
+ }
+ newExpr = newLet;
}
} else if (expr is MatchExpr) {
diff --git a/Source/DafnyExtension/DafnyRuntime.cs b/Source/DafnyExtension/DafnyRuntime.cs index a8faafae..f61163d0 100644 --- a/Source/DafnyExtension/DafnyRuntime.cs +++ b/Source/DafnyExtension/DafnyRuntime.cs @@ -581,6 +581,15 @@ namespace Dafny yield return true;
}
}
+ public static IEnumerable<BigInteger> AllIntegers {
+ get {
+ yield return new BigInteger(0);
+ for (var j = new BigInteger(1);; j++) {
+ yield return j;
+ yield return -j;
+ }
+ }
+ }
// pre: b != 0
// post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 7da30e96..364e6c93 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -2043,6 +2043,48 @@ Dafny program verifier finished with 3 verified, 3 errors Dafny program verifier finished with 2 verified, 0 errors
+-------------------- AutoReq.dfy --------------------
+AutoReq.dfy(245,3): Error: possible violation of function precondition
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+AutoReq.dfy(11,3): Error: possible violation of function precondition
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+AutoReq.dfy(23,3): Error: possible violation of function precondition
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+AutoReq.dfy(36,12): Error: assertion violation
+AutoReq.dfy(29,13): Related location
+AutoReq.dfy(5,5): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon9_Then
+AutoReq.dfy(36,12): Error: possible violation of function precondition
+Execution trace:
+ (0,0): anon0
+ (0,0): anon9_Then
+AutoReq.dfy(38,12): Error: assertion violation
+AutoReq.dfy(29,27): Related location
+AutoReq.dfy(5,5): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon10_Then
+AutoReq.dfy(38,12): Error: possible violation of function precondition
+Execution trace:
+ (0,0): anon0
+ (0,0): anon10_Then
+AutoReq.dfy(43,12): Error: assertion violation
+AutoReq.dfy(29,13): Related location
+AutoReq.dfy(5,5): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon11_Then
+
+Dafny program verifier finished with 46 verified, 8 errors
+
-------------------- Superposition.dfy --------------------
Verifying CheckWellformed$$_0_M0.C.M ...
diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy new file mode 100644 index 00000000..684de262 --- /dev/null +++ b/Test/dafny0/AutoReq.dfy @@ -0,0 +1,288 @@ +
+function f(x:int) : bool
+ requires x > 3;
+{
+ x > 7
+}
+
+// Should cause a function-requires failure
+function g(y:int) : bool
+{
+ f(y)
+}
+
+// Should succeed thanks to auto-generation based on f's requirements
+function {:autoReq} h(y:int) : bool
+{
+ f(y)
+}
+
+// Should fail based on h's inferred requirements
+function h_tester() : bool
+{
+ h(2)
+}
+
+// Should succeed thanks to auto_reqs
+function {:autoReq} i(y:int, b:bool) : bool
+{
+ if b then f(y + 2) else f(2*y)
+}
+
+method test()
+{
+ // Function req violations (and assertion violations)
+ if (*) {
+ assert i(1, true);
+ } else if (*) {
+ assert i(0, false);
+ }
+
+ // Make sure function i's reqs can be satisfied
+ if (*) {
+ assert i(3, true); // False assertion
+ }
+ assert i(7, false); // True assertion
+}
+
+module {:autoReq} TwoLayersOfRequires {
+ function f(x:int) : bool
+ requires x > 4;
+ {
+ x > 5
+ }
+
+ function g(y:int) : bool
+ requires y < 50;
+ {
+ f(y)
+ }
+
+ function h(z:int) : bool
+ {
+ g(z)
+ }
+}
+
+module {:autoReq} QuantifierTestsSimple {
+ function byte(x:int) : bool
+ {
+ 0 <= x < 256
+ }
+
+ function f_forall(s:seq<int>) : bool
+ {
+ forall i :: 0 <= i < |s| ==> byte(s[i])
+ }
+
+ function f_exists(s:seq<int>) : bool
+ {
+ exists i :: 0 <= i < |s| && byte(s[i])
+ }
+
+ function g_forall(s:seq<int>) : bool
+ requires f_forall(s);
+ {
+ |s| > 2
+ }
+
+ function g_exists(s:seq<int>) : bool
+ requires f_exists(s);
+ {
+ |s| > 2
+ }
+
+ function h(s:seq<int>) : bool
+ {
+ g_forall(s) && g_exists(s)
+ }
+}
+
+module {:autoReq} QuantifierTestsHard {
+ function byte(x:int) : bool
+ requires 0 <= x < 256;
+ { true }
+
+ function f_forall(s:seq<int>) : bool
+ {
+ forall i :: 0 <= i < |s| ==> byte(s[i])
+ }
+
+ function f_exists(s:seq<int>) : bool
+ {
+ exists i :: 0 <= i < |s| && byte(s[i])
+ }
+
+ function g_forall(s:seq<int>) : bool
+ requires forall j :: 0 <= j < |s| ==> byte(s[j]);
+ {
+ |s| > 2
+ }
+
+ function h_forall(s:seq<int>) : bool
+ {
+ f_forall(s)
+ }
+
+ function h(s:seq<int>) : bool
+ {
+ g_forall(s)
+ }
+
+ function i(s:seq<int>) : bool
+ requires forall k :: 0 <= k < |s| ==> 0 <= s[k] < 5;
+ {
+ true
+ }
+
+ function j(s:seq<int>) : bool
+ {
+ i(s)
+ }
+
+ function m(x:int) : bool
+ function n(x:int) : bool
+
+ function f1(x:int) : bool
+ requires x > 3;
+ requires x < 16;
+
+ function variable_uniqueness_test(x:int) : bool
+ {
+ (forall y:int :: m(y))
+ &&
+ f1(x)
+ }
+}
+
+module CorrectReqOrdering {
+ function f1(x:int) : bool
+ requires x > 3;
+
+ function f2(b:bool) : bool
+ requires b;
+
+ // Should pass if done correctly.
+ // However, if Dafny incorrectly put the requires for f2 first,
+ // then the requires for f1 won't be satisfied
+ function {:autoReq} f3(z:int) : bool
+ {
+ f2(f1(z))
+ }
+
+}
+
+module ShortCircuiting {
+ function f1(x:int) : bool
+ requires x > 3;
+
+ function f2(y:int) : bool
+ requires y < 10;
+
+ function {:autoReq} test1(x':int, y':int) : bool
+ {
+ f1(x') && f2(y')
+ }
+
+ function {:autoReq} test2(x':int, y':int) : bool
+ {
+ f1(x') ==> f2(y')
+ }
+
+ function {:autoReq} test3(x':int, y':int) : bool
+ {
+ f1(x') || f2(y')
+ }
+}
+
+module Lets {
+ function f1(x:int) : bool
+ requires x > 3;
+
+ function {:autoReq} test1(x':int) : bool
+ {
+ var y' := 3*x'; f1(y')
+ }
+}
+
+// Test nested module specification of :autoReq attribute
+module {:autoReq} M1 {
+ module M2 {
+ function f(x:int) : bool
+ requires x > 3;
+ {
+ x > 7
+ }
+
+ // Should succeed thanks to auto-generation based on f's requirements
+ function {:autoReq} h(y:int) : bool
+ {
+ f(y)
+ }
+ }
+}
+
+module Datatypes {
+ datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType);
+
+ function f1(t:TheType):bool
+ requires t.TheType_builder? && t.x > 3;
+
+ function {:autoReq} test(t:TheType) : bool
+ {
+ f1(t)
+ }
+
+ function f2(x:int) : bool
+ requires forall t:TheType :: t.TheType_builder? && t.x > x;
+ {
+ true
+ }
+
+ // Should cause a function-requirement violation without autoReq
+ function f3(y:int) : bool
+ {
+ f2(y)
+ }
+
+ function {:autoReq} test2(z:int) : bool
+ {
+ f2(z)
+ }
+
+}
+
+module Matches {
+ datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType);
+
+ function f1(x:int):bool
+ requires x > 3;
+
+ function {:autoReq} basic_test(t:TheType) : bool
+ {
+ match t
+ case TheType_builder(x) => f1(x)
+ case TheType_copier(t) => true
+ }
+}
+
+// Make sure :autoReq works with static functions
+module StaticTest {
+ static function f(x:int) : bool
+ requires x > 3;
+ {
+ x > 7
+ }
+
+ static function {:autoReq} g(z:int) : bool
+ requires f(z);
+ {
+ true
+ }
+
+ // Should succeed thanks to auto-generation based on f's requirements
+ static function {:autoReq} h(y:int) : bool
+ {
+ g(y)
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index ae80dc89..3d4af611 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -29,7 +29,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy Definedness.dfy IteratorResolution.dfy Iterators.dfy
RankPos.dfy RankNeg.dfy
Computations.dfy ComputationsNeg.dfy
- Include.dfy) do (
+ Include.dfy AutoReq.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
|