diff --git a/Source/DafnyCore/AST/Expressions/Expression.cs b/Source/DafnyCore/AST/Expressions/Expression.cs index 5eee105fbe0..8bc86b9aaf8 100644 --- a/Source/DafnyCore/AST/Expressions/Expression.cs +++ b/Source/DafnyCore/AST/Expressions/Expression.cs @@ -156,15 +156,41 @@ public virtual IEnumerable ComponentTypes { public virtual bool IsImplicit => false; + public static IEnumerable ConjunctsWithLetsOnOutside(Expression expr) { + foreach (var conjunct in Conjuncts(expr)) { + if (conjunct is LetExpr { Exact: true } letExpr) { + foreach (var letBodyConjunct in ConjunctsWithLetsOnOutside(letExpr.Body)) { + yield return new LetExpr(letExpr.tok, letExpr.LHSs, letExpr.RHSs, letBodyConjunct, letExpr.Exact, letExpr.Attributes) { + Type = letExpr.Type + }; + } + } else { + yield return conjunct; + } + } + } + + /// + /// Return the negation of each of the expressions in "expressions". + /// If there is just one expression in "expressions", then use the given token "tok" for the negation. + /// Otherwise, use the token from each expression. + /// + static IEnumerable NegateEach(IOrigin tok, IEnumerable expressions) { + var exprs = expressions.ToList(); + foreach (Expression e in exprs) { + yield return Expression.CreateNot(exprs.Count == 1 ? tok : e.tok, e); + } + } + public static IEnumerable Conjuncts(Expression expr) { Contract.Requires(expr != null); Contract.Requires(expr.Type.IsBoolType); Contract.Ensures(cce.NonNullElements(Contract.Result>())); expr = StripParens(expr); - if (expr is UnaryOpExpr unary && unary.Op == UnaryOpExpr.Opcode.Not) { - foreach (Expression e in Disjuncts(unary.E)) { - yield return Expression.CreateNot(e.Tok, e); + if (expr is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Not } unary) { + foreach (Expression e in NegateEach(expr.Tok, Disjuncts(unary.E))) { + yield return e; } yield break; @@ -189,18 +215,18 @@ public static IEnumerable Disjuncts(Expression expr) { Contract.Ensures(cce.NonNullElements(Contract.Result>())); expr = StripParens(expr); - if (expr is UnaryOpExpr unary && unary.Op == UnaryOpExpr.Opcode.Not) { - foreach (Expression e in Conjuncts(unary.E)) { - yield return Expression.CreateNot(e.Tok, e); + if (expr is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Not } unary) { + foreach (Expression e in NegateEach(expr.Tok, Conjuncts(unary.E))) { + yield return e; } yield break; } else if (expr is BinaryExpr bin) { if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) { - foreach (Expression e in Conjuncts(bin.E0)) { + foreach (Expression e in Disjuncts(bin.E0)) { yield return e; } - foreach (Expression e in Conjuncts(bin.E1)) { + foreach (Expression e in Disjuncts(bin.E1)) { yield return e; } yield break; @@ -208,7 +234,7 @@ public static IEnumerable Disjuncts(Expression expr) { foreach (Expression e in Conjuncts(bin.E0)) { yield return Expression.CreateNot(e.Tok, e); } - foreach (Expression e in Conjuncts(bin.E1)) { + foreach (Expression e in Disjuncts(bin.E1)) { yield return e; } yield break; diff --git a/Source/DafnyCore/CounterExampleGeneration/DafnyModel.cs b/Source/DafnyCore/CounterExampleGeneration/DafnyModel.cs index 565ccd63ab5..db9cfd2ab7a 100644 --- a/Source/DafnyCore/CounterExampleGeneration/DafnyModel.cs +++ b/Source/DafnyCore/CounterExampleGeneration/DafnyModel.cs @@ -73,7 +73,7 @@ public DafnyModel(Model model, DafnyOptions options) { fMapEmpty = new ModelFuncWrapper(this, "Map#Empty", 0, 0); fIs = new ModelFuncWrapper(this, "$Is", 2, tyArgMultiplier); fIsBox = new ModelFuncWrapper(this, "$IsBox", 2, 0); - fBox = new ModelFuncWrapper(this, "$Box", 1, tyArgMultiplier); + fBox = new ModelFuncWrapper(this, BoogieGenerator.BoxFunctionName, 1, tyArgMultiplier); fDim = new ModelFuncWrapper(this, "FDim", 1, 0); fIndexField = new ModelFuncWrapper(this, "IndexField", 1, 0); fMultiIndexField = new ModelFuncWrapper(this, "MultiIndexField", 2, 0); @@ -85,7 +85,7 @@ public DafnyModel(Model model, DafnyOptions options) { fU2Int = new ModelFuncWrapper(this, "U_2_int", 1, 0); fTag = new ModelFuncWrapper(this, "Tag", 1, 0); fBv = new ModelFuncWrapper(this, "TBitvector", 1, 0); - fUnbox = new ModelFuncWrapper(this, "$Unbox", 2, 0); + fUnbox = new ModelFuncWrapper(this, BoogieGenerator.UnboxFunctionName, 2, 0); fLs = new ModelFuncWrapper(this, "$LS", 1, 0); fLz = new ModelFuncWrapper(this, "$LZ", 0, 0); InitDataTypes(); diff --git a/Source/DafnyCore/Rewriters/InductionHeuristic.cs b/Source/DafnyCore/Rewriters/InductionHeuristic.cs index 6b0bd66fb11..6ce2202be3b 100644 --- a/Source/DafnyCore/Rewriters/InductionHeuristic.cs +++ b/Source/DafnyCore/Rewriters/InductionHeuristic.cs @@ -178,4 +178,4 @@ expr is BoxingCastExpr || return false; } } -} \ No newline at end of file +} diff --git a/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs b/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs index 77077dfc4af..fe676e017bd 100644 --- a/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs +++ b/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs @@ -171,7 +171,8 @@ string InfoFirstLineEnd(int count) { messages.Add($"Part #{splitPartIndex} is '{Comprehension.Term}'"); } if (Candidates.Any()) { - messages.Add($"Selected triggers:{InfoFirstLineEnd(Candidates.Count)}{string.Join(", ", Candidates)}"); + var subst = Util.Comma("", NamedExpressions, pair => $" where {pair.Item2} := {pair.Item1}"); + messages.Add($"Selected triggers:{InfoFirstLineEnd(Candidates.Count)}{string.Join(", ", Candidates)}{subst}"); } if (RejectedCandidates.Any()) { messages.Add($"Rejected triggers:{InfoFirstLineEnd(RejectedCandidates.Count)}{string.Join("\n ", RejectedCandidates)}"); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs b/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs index 3c790877e41..f573ffefc8a 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs @@ -155,6 +155,9 @@ enum BuiltinFunction { AtLayer } + public const string BoxFunctionName = "$Box"; + public const string UnboxFunctionName = "$Unbox"; + Bpl.Expr Lit(Bpl.Expr expr, Bpl.Type typ) { Contract.Requires(expr != null); Contract.Requires(typ != null); @@ -506,11 +509,11 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan case BuiltinFunction.Box: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation == null); - return FunctionCall(tok, "$Box", Predef.BoxType, args); + return FunctionCall(tok, BoxFunctionName, Predef.BoxType, args); case BuiltinFunction.Unbox: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation != null); - return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "$Unbox", typeInstantiation, args), typeInstantiation); + return Bpl.Expr.CoerceType(tok, FunctionCall(tok, UnboxFunctionName, typeInstantiation, args), typeInstantiation); case BuiltinFunction.RealToInt: Contract.Assume(args.Length == 1); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs index 827590a6d4d..84d2939117a 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs @@ -6,6 +6,7 @@ using Dafny; using Microsoft.BaseTypes; using Microsoft.Boogie; +using Bpl = Microsoft.Boogie; using static Microsoft.Dafny.Util; namespace Microsoft.Dafny { @@ -22,6 +23,14 @@ public Boogie.Expr HeapExpr { get { Statistics_HeapUses++; return _the_heap_expr; } } + public Boogie.Expr HeapExprForArrow(Type arrowType) { + if (arrowType.IsArrowTypeWithoutReadEffects) { + return BoogieGenerator.NewOneHeapExpr(arrowType.Tok); + } else { + return HeapExpr; + } + } + /// /// Return HeapExpr as an IdentifierExpr. /// CAUTION: This getter should be used only if the caller "knows" that HeapExpr really is an IdentifierExpr. @@ -38,7 +47,7 @@ public Boogie.IdentifierExpr HeapCastToIdentifierExpr { public readonly string This; public readonly string readsFrame; // the name of the context's frame variable for reading state. // May be null to indicate the context's reads frame is * and doesn't require any reads checks. - public readonly IFrameScope scope; // lambda, function or predicate + public readonly IFrameScope scope; // lambda, function or predicate public readonly string modifiesFrame; // the name of the context's frame variable for writing state. readonly Function applyLimited_CurrentFunction; internal readonly FuelSetting layerInterCluster; @@ -659,7 +668,7 @@ public Boogie.Expr TrExpr(Expression expr) { var applied = FunctionCall(GetToken(applyExpr), BoogieGenerator.Apply(arity), Predef.BoxType, Concat(Map(tt.TypeArgs, BoogieGenerator.TypeToTy), - Cons(HeapExpr, Cons(TrExpr(e.Function), e.Args.ConvertAll(arg => TrArg(arg)))))); + Cons(HeapExprForArrow(e.Function.Type), Cons(TrExpr(e.Function), e.Args.ConvertAll(arg => TrArg(arg)))))); return BoogieGenerator.UnboxUnlessInherentlyBoxed(applied, tt.Result); } @@ -737,7 +746,12 @@ public Boogie.Expr TrExpr(Expression expr) { case SeqConstructionExpr constructionExpr: { var e = constructionExpr; var eType = e.Type.NormalizeToAncestorType().AsSeqType.Arg.NormalizeExpand(); - return FunctionCall(GetToken(constructionExpr), "Seq#Create", Predef.SeqType, BoogieGenerator.TypeToTy(eType), HeapExpr, TrExpr(e.N), TrExpr(e.Initializer)); + var initalizerHeap = e.Initializer.Type.IsArrowType ? HeapExprForArrow(e.Initializer.Type) : HeapExpr; + return FunctionCall(GetToken(constructionExpr), "Seq#Create", Predef.SeqType, + BoogieGenerator.TypeToTy(eType), + initalizerHeap, + TrExpr(e.N), + TrExpr(e.Initializer)); } case MultiSetFormingExpr formingExpr: { MultiSetFormingExpr e = formingExpr; @@ -1566,8 +1580,9 @@ private Expr TrLambdaExpr(LambdaExpr e) { return new KeyValuePair(bv, new BoogieWrapper(unboxy, bv.Type)); }).ToDictionary(x => x.Key, x => x.Value); var su = new Substituter(null, subst, new Dictionary()); - - var et = new ExpressionTranslator(this, heap); + var et = this.HeapExpr != null + ? new ExpressionTranslator(this.BoogieGenerator, this.Predef, heap, this.Old.HeapExpr, this.scope) + : new ExpressionTranslator(this, heap); var lvars = new List(); var ly = BplBoundVar(varNameGen.FreshId("#ly#"), Predef.LayerType, lvars); et = et.WithLayer(ly); @@ -1576,9 +1591,13 @@ private Expr TrLambdaExpr(LambdaExpr e) { ebody = BoogieGenerator.BoxIfNotNormallyBoxed(ebody.tok, ebody, e.Body.Type); var isBoxes = BplAnd(ves.Zip(e.BoundVars, (ve, bv) => BoogieGenerator.MkIsBox(ve, bv.Type))); - var reqbody = e.Range == null - ? isBoxes - : BplAnd(isBoxes, et.TrExpr(BoogieGenerator.Substitute(e.Range, null, subst))); + Bpl.Expr reqbody; + if (e.Range == null) { + reqbody = isBoxes; + } else { + var range = BoogieGenerator.Substitute(e.Range, null, subst); + reqbody = BplAnd(isBoxes, BplImp(et.CanCallAssumption(range), et.TrExpr(range))); + } var rdvars = new List(); var o = BplBoundVar(varNameGen.FreshId("#o#"), Predef.RefType, rdvars); @@ -2103,7 +2122,21 @@ public Boogie.Expr GoodRef(IOrigin tok, Boogie.Expr e, Type type) { return BoogieGenerator.GetWhereClause(tok, e, type, this, ISALLOC); } - public Expr CanCallAssumption(Expression expr) { + public Expression MakeAllowance(FunctionCallExpr e, CanCallOptions cco = null) { + Expression allowance = Expression.CreateBoolLiteral(e.Tok, true); + if (!e.Function.IsStatic) { + allowance = Expression.CreateAnd(allowance, Expression.CreateEq(e.Receiver, new ThisExpr(e.Function), e.Receiver.Type)); + } + var formals = cco == null ? e.Function.Ins : cco.EnclosingFunction.Ins; + for (int i = 0; i < e.Args.Count; i++) { + Expression ee = e.Args[i]; + Formal ff = formals[i]; + allowance = Expression.CreateAnd(allowance, Expression.CreateEq(ee, Expression.CreateIdentExpr(ff), ff.Type)); + } + return allowance; + } + + public Expr CanCallAssumption(Expression expr, CanCallOptions cco = null) { Contract.Requires(expr != null); Contract.Requires(this != null); Contract.Requires(BoogieGenerator.Predef != null); @@ -2113,17 +2146,17 @@ public Expr CanCallAssumption(Expression expr) { return Boogie.Expr.True; } else if (expr is DisplayExpression) { DisplayExpression e = (DisplayExpression)expr; - return CanCallAssumption(e.Elements); + return CanCallAssumption(e.Elements, cco); } else if (expr is MapDisplayExpr) { MapDisplayExpr e = (MapDisplayExpr)expr; List l = new List(); foreach (ExpressionPair p in e.Elements) { l.Add(p.A); l.Add(p.B); } - return CanCallAssumption(l); + return CanCallAssumption(l, cco); } else if (expr is MemberSelectExpr) { MemberSelectExpr e = (MemberSelectExpr)expr; - var r = CanCallAssumption(e.Obj); + var r = CanCallAssumption(e.Obj, cco); if (e.Member is DatatypeDestructor) { var dtor = (DatatypeDestructor)e.Member; if (dtor.EnclosingCtors.Count == dtor.EnclosingCtors[0].EnclosingDatatype.Ctors.Count) { @@ -2136,77 +2169,135 @@ public Expr CanCallAssumption(Expression expr) { return r; } else if (expr is SeqSelectExpr) { SeqSelectExpr e = (SeqSelectExpr)expr; - Boogie.Expr total = CanCallAssumption(e.Seq); + Boogie.Expr total = CanCallAssumption(e.Seq, cco); if (e.E0 != null) { - total = BplAnd(total, CanCallAssumption(e.E0)); + total = BplAnd(total, CanCallAssumption(e.E0, cco)); } if (e.E1 != null) { - total = BplAnd(total, CanCallAssumption(e.E1)); + total = BplAnd(total, CanCallAssumption(e.E1, cco)); } return total; } else if (expr is MultiSelectExpr) { MultiSelectExpr e = (MultiSelectExpr)expr; - Boogie.Expr total = CanCallAssumption(e.Array); + Boogie.Expr total = CanCallAssumption(e.Array, cco); foreach (Expression idx in e.Indices) { - total = BplAnd(total, CanCallAssumption(idx)); + total = BplAnd(total, CanCallAssumption(idx, cco)); } return total; } else if (expr is SeqUpdateExpr) { SeqUpdateExpr e = (SeqUpdateExpr)expr; - Boogie.Expr total = CanCallAssumption(e.Seq); - total = BplAnd(total, CanCallAssumption(e.Index)); - total = BplAnd(total, CanCallAssumption(e.Value)); + Boogie.Expr total = CanCallAssumption(e.Seq, cco); + total = BplAnd(total, CanCallAssumption(e.Index, cco)); + total = BplAnd(total, CanCallAssumption(e.Value, cco)); return total; + } else if (expr is ApplyExpr) { ApplyExpr e = (ApplyExpr)expr; + + Func TrArg = arg => { + Boogie.Expr inner = TrExpr(arg); + if (ModeledAsBoxType(arg.Type)) { + return inner; + } else { + return BoogieGenerator.FunctionCall(arg.Tok, BuiltinFunction.Box, null, inner); + } + }; + + var args = Concat( + Map(e.Function.Type.AsArrowType.TypeArgs, BoogieGenerator.TypeToTy), + Cons(HeapExpr, + Cons(TrExpr(e.Function), + e.Args.ConvertAll(arg => TrArg(arg))))); + + var requiresk = FunctionCall(e.Tok, Requires(e.Args.Count), Boogie.Type.Bool, args); return BplAnd( - Cons(CanCallAssumption(e.Function), - e.Args.ConvertAll(ee => CanCallAssumption(ee)))); + BplAnd( + Cons(CanCallAssumption(e.Function, cco), + e.Args.ConvertAll(ee => CanCallAssumption(ee, cco)))), + requiresk); + } else if (expr is FunctionCallExpr) { FunctionCallExpr e = (FunctionCallExpr)expr; - Boogie.Expr r = CanCallAssumption(e.Receiver); - r = BplAnd(r, CanCallAssumption(e.Args)); + Boogie.Expr r = CanCallAssumption(e.Receiver, cco); + r = BplAnd(r, CanCallAssumption(e.Args, cco)); if (!(e.Function is SpecialFunction)) { - // get to assume canCall Boogie.IdentifierExpr canCallFuncID = new Boogie.IdentifierExpr(expr.Tok, e.Function.FullSanitizedName + "#canCall", Boogie.Type.Bool); List args = FunctionInvocationArguments(e, null, null); Boogie.Expr canCallFuncAppl = new Boogie.NAryExpr(BoogieGenerator.GetToken(expr), new Boogie.FunctionCall(canCallFuncID), args); - r = BplAnd(r, canCallFuncAppl); + var add = cco != null && cco.MakeAllowance(e.Function) ? Boogie.Expr.Or(TrExpr(MakeAllowance(e, cco)), canCallFuncAppl) : canCallFuncAppl; + r = BplAnd(r, add); } return r; } else if (expr is DatatypeValue) { DatatypeValue dtv = (DatatypeValue)expr; - return CanCallAssumption(dtv.Arguments); + return CanCallAssumption(dtv.Arguments, cco); } else if (expr is SeqConstructionExpr) { var e = (SeqConstructionExpr)expr; - return BplAnd(CanCallAssumption(e.N), CanCallAssumption(e.Initializer)); + // CanCallAssumption[[ seq(n, init) ]] = + // CanCallAssumption[[ n ]] && + // CanCallAssumption[[ init ]] && + // var initF := init; // necessary, in order to use init(i) in trigger, since it may contain quantifiers + // (forall i: int + // { initF(i) } + // 0 <= i < n ==> + // CanCallAssumption[[ init(i) ]]) + + var varNameGen = BoogieGenerator.CurrentIdGenerator.NestedFreshIdGenerator("seqinit$"); + var indexVar = new Bpl.BoundVariable(e.Tok, new Bpl.TypedIdent(e.Tok, varNameGen.FreshId("#i"), Bpl.Type.Int)); + var index = new Bpl.IdentifierExpr(e.Tok, indexVar); + var indexRange = BplAnd(Bpl.Expr.Le(Bpl.Expr.Literal(0), index), Bpl.Expr.Lt(index, TrExpr(e.N))); + var initFVar = new Bpl.BoundVariable(e.Tok, new Bpl.TypedIdent(e.Tok, varNameGen.FreshId("#f"), Predef.HandleType)); + + var initF = new Bpl.IdentifierExpr(e.Tok, initFVar); + + var dafnyInitApplication = new ApplyExpr(e.Tok, e.Initializer, + new List() { new BoogieWrapper(index, Type.Int) }, + Token.NoToken) { + Type = e.Initializer.Type.AsArrowType.Result + }; + var canCall = CanCallAssumption(dafnyInitApplication); + + dafnyInitApplication = new ApplyExpr(e.Tok, new BoogieWrapper(initF, e.Initializer.Type), + new List() { new BoogieWrapper(index, Type.Int) }, + Token.NoToken) { + Type = e.Initializer.Type.AsArrowType.Result + }; + var apply = TrExpr(dafnyInitApplication); + + var tr = new Bpl.Trigger(e.Tok, true, new List { apply }); + var ccaInit = new Bpl.ForallExpr(e.Tok, new List() { indexVar }, tr, BplImp(indexRange, canCall)); + var rhsAppliedToIndex = new Bpl.LetExpr(e.Tok, new List() { initFVar }, + new List() { TrExpr(e.Initializer) }, null, ccaInit); + + return BplAnd(BplAnd(CanCallAssumption(e.N, cco), CanCallAssumption(e.Initializer, cco)), rhsAppliedToIndex); + } else if (expr is MultiSetFormingExpr) { MultiSetFormingExpr e = (MultiSetFormingExpr)expr; - return CanCallAssumption(e.E); + return CanCallAssumption(e.E, cco); } else if (expr is OldExpr) { var e = (OldExpr)expr; - return OldAt(e.AtLabel).CanCallAssumption(e.E); + return OldAt(e.AtLabel).CanCallAssumption(e.E, cco); } else if (expr is UnchangedExpr) { var e = (UnchangedExpr)expr; Boogie.Expr be = Boogie.Expr.True; foreach (var fe in e.Frame) { - be = BplAnd(be, CanCallAssumption(fe.E)); + be = BplAnd(be, CanCallAssumption(fe.E, cco)); } return be; } else if (expr is UnaryExpr) { var e = (UnaryExpr)expr; - return CanCallAssumption(e.E); + return CanCallAssumption(e.E, cco); } else if (expr is BinaryExpr) { // The short-circuiting boolean operators &&, ||, and ==> end up duplicating their // left argument. Therefore, we first try to re-associate the expression to make // left arguments smaller. if (BoogieGenerator.ReAssociateToTheRight(ref expr)) { - return CanCallAssumption(expr); + return CanCallAssumption(expr, cco); } var e = (BinaryExpr)expr; - Boogie.Expr t0 = CanCallAssumption(e.E0); - Boogie.Expr t1 = CanCallAssumption(e.E1); + Boogie.Expr t0 = CanCallAssumption(e.E0, cco); + Boogie.Expr t1 = CanCallAssumption(e.E1, cco); switch (e.ResolvedOp) { case BinaryExpr.ResolvedOpcode.And: case BinaryExpr.ResolvedOpcode.Imp: @@ -2218,13 +2309,15 @@ public Expr CanCallAssumption(Expression expr) { case BinaryExpr.ResolvedOpcode.EqCommon: case BinaryExpr.ResolvedOpcode.NeqCommon: { Boogie.Expr r = Boogie.Expr.True; - if (e.E0 is { Type: { AsDatatype: { } dt0 }, Resolved: not DatatypeValue }) { - var funcID = new Boogie.FunctionCall(new Boogie.IdentifierExpr(expr.Tok, "$IsA#" + dt0.FullSanitizedName, Boogie.Type.Bool)); - r = BplAnd(r, new Boogie.NAryExpr(expr.Tok, funcID, new List { TrExpr(e.E0) })); - } - if (e.E1 is { Type: { AsDatatype: { } dt1 }, Resolved: not DatatypeValue }) { - var funcID = new Boogie.FunctionCall(new Boogie.IdentifierExpr(expr.Tok, "$IsA#" + dt1.FullSanitizedName, Boogie.Type.Bool)); - r = BplAnd(r, new Boogie.NAryExpr(expr.Tok, funcID, new List { TrExpr(e.E1) })); + if (cco is not { SkipIsA: true }) { + if (e.E0 is { Type: { AsDatatype: { } dt0 }, Resolved: not DatatypeValue }) { + var funcID = new Boogie.FunctionCall(new Boogie.IdentifierExpr(expr.Tok, "$IsA#" + dt0.FullSanitizedName, Boogie.Type.Bool)); + r = BplAnd(r, new Boogie.NAryExpr(expr.Tok, funcID, new List { TrExpr(e.E0) })); + } + if (e.E1 is { Type: { AsDatatype: { } dt1 }, Resolved: not DatatypeValue }) { + var funcID = new Boogie.FunctionCall(new Boogie.IdentifierExpr(expr.Tok, "$IsA#" + dt1.FullSanitizedName, Boogie.Type.Bool)); + r = BplAnd(r, new Boogie.NAryExpr(expr.Tok, funcID, new List { TrExpr(e.E1) })); + } } return BplAnd(r, BplAnd(t0, t1)); } @@ -2261,10 +2354,11 @@ public Expr CanCallAssumption(Expression expr) { return BplAnd(t0, t1); } else if (expr is TernaryExpr) { var e = (TernaryExpr)expr; - return BplAnd(CanCallAssumption(e.E0), BplAnd(CanCallAssumption(e.E1), CanCallAssumption(e.E2))); + return BplAnd(CanCallAssumption(e.E0, cco), BplAnd(CanCallAssumption(e.E1, cco), CanCallAssumption(e.E2, cco))); } else if (expr is LetExpr letExpr) { - return LetCanCallAssumption(letExpr); + return LetCanCallAssumption(letExpr, cco); + } else if (expr is LambdaExpr) { var e = (LambdaExpr)expr; @@ -2272,7 +2366,9 @@ public Expr CanCallAssumption(Expression expr) { var varNameGen = BoogieGenerator.CurrentIdGenerator.NestedFreshIdGenerator("$l#"); Boogie.Expr heap; var hVar = BplBoundVar(varNameGen.FreshId("#heap#"), BoogieGenerator.Predef.HeapType, out heap); - var et = new ExpressionTranslator(this, heap); + var et = this.HeapExpr != null + ? new ExpressionTranslator(this.BoogieGenerator, this.Predef, heap, this.Old.HeapExpr, this.scope) + : new ExpressionTranslator(this, heap); Dictionary subst = new Dictionary(); foreach (var bv in e.BoundVars) { @@ -2282,10 +2378,10 @@ public Expr CanCallAssumption(Expression expr) { subst[bv] = new BoogieWrapper(ve, bv.Type); } - var canCall = et.CanCallAssumption(Substitute(e.Body, null, subst)); + var canCall = et.CanCallAssumption(Substitute(e.Body, null, subst), cco); if (e.Range != null) { var range = Substitute(e.Range, null, subst); - canCall = BplAnd(CanCallAssumption(range), BplImp(TrExpr(range), canCall)); + canCall = BplAnd(CanCallAssumption(range, cco), BplImp(TrExpr(range), canCall)); } // It's important to add the heap last to "bvarsAndAntecedents", because the heap may occur in the antecedents of @@ -2301,16 +2397,16 @@ public Expr CanCallAssumption(Expression expr) { } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; if (e is QuantifierExpr q && q.SplitQuantifier != null) { - return CanCallAssumption(q.SplitQuantifierExpression); + return CanCallAssumption(q.SplitQuantifierExpression, cco); } // Determine the CanCall's for the range and term - var canCall = CanCallAssumption(e.Term); + var canCall = CanCallAssumption(e.Term, cco); if (e.Range != null) { - canCall = BplAnd(CanCallAssumption(e.Range), BplImp(TrExpr(e.Range), canCall)); + canCall = BplAnd(CanCallAssumption(e.Range, cco), BplImp(TrExpr(e.Range), canCall)); } if (expr is MapComprehension mc && mc.IsGeneralMapComprehension) { - canCall = BplAnd(canCall, CanCallAssumption(mc.TermLeft)); + canCall = BplAnd(canCall, CanCallAssumption(mc.TermLeft, cco)); // The translation of "map x,y | R(x,y) :: F(x,y) := G(x,y)" makes use of projection // functions project_x,project_y. These are functions defined here by the following axiom: @@ -2350,42 +2446,42 @@ public Expr CanCallAssumption(Expression expr) { } else if (expr is StmtExpr) { var e = (StmtExpr)expr; - return CanCallAssumption(e.E); + return CanCallAssumption(e.E, cco); } else if (expr is ITEExpr) { ITEExpr e = (ITEExpr)expr; - Boogie.Expr total = CanCallAssumption(e.Test); + Boogie.Expr total = CanCallAssumption(e.Test, cco); Boogie.Expr test = TrExpr(e.Test); - total = BplAnd(total, BplImp(test, CanCallAssumption(e.Thn))); - total = BplAnd(total, BplImp(Boogie.Expr.Not(test), CanCallAssumption(e.Els))); + total = BplAnd(total, BplImp(test, CanCallAssumption(e.Thn, cco))); + total = BplAnd(total, BplImp(Boogie.Expr.Not(test), CanCallAssumption(e.Els, cco))); return total; } else if (expr is ConcreteSyntaxExpression) { var e = (ConcreteSyntaxExpression)expr; - return CanCallAssumption(e.ResolvedExpression); + return CanCallAssumption(e.ResolvedExpression, cco); } else if (expr is NestedMatchExpr nestedMatchExpr) { - return CanCallAssumption(nestedMatchExpr.Flattened); + return CanCallAssumption(nestedMatchExpr.Flattened, cco); } else if (expr is BoogieFunctionCall) { var e = (BoogieFunctionCall)expr; - return CanCallAssumption(e.Args); + return CanCallAssumption(e.Args, cco); } else if (expr is MatchExpr) { var e = (MatchExpr)expr; var ite = DesugarMatchExpr(e); - return CanCallAssumption(ite); + return CanCallAssumption(ite, cco); } else if (expr is BoxingCastExpr) { var e = (BoxingCastExpr)expr; - return CanCallAssumption(e.E); + return CanCallAssumption(e.E, cco); } else if (expr is UnboxingCastExpr) { var e = (UnboxingCastExpr)expr; - return CanCallAssumption(e.E); + return CanCallAssumption(e.E, cco); } else if (expr is DecreasesToExpr decreasesToExpr) { - var oldCanCall = CanCallAssumption(decreasesToExpr.OldExpressions.ToList()); - var newCanCall = CanCallAssumption(decreasesToExpr.NewExpressions.ToList()); + var oldCanCall = CanCallAssumption(decreasesToExpr.OldExpressions.ToList(), cco); + var newCanCall = CanCallAssumption(decreasesToExpr.NewExpressions.ToList(), cco); return BplAnd(oldCanCall, newCanCall); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression } } - public Expr /*!*/ CanCallAssumption(List exprs /*!*/ /*!*/) { + public Expr CanCallAssumption(List exprs, CanCallOptions cco) { Contract.Requires(this != null); Contract.Requires(exprs != null); Contract.Ensures(Contract.Result() != null); @@ -2393,10 +2489,30 @@ public Expr CanCallAssumption(Expression expr) { Boogie.Expr total = Boogie.Expr.True; foreach (Expression e in exprs) { Contract.Assert(e != null); - total = BplAnd(total, CanCallAssumption(e)); + total = BplAnd(total, CanCallAssumption(e, cco)); } return total; } } + + public class CanCallOptions { + public bool SkipIsA; + + public readonly Function EnclosingFunction; // self-call allowance is applied to the enclosing function + public readonly bool SelfCallAllowanceAlsoForOverride; + + public bool MakeAllowance(Function f) { + return f == EnclosingFunction || (SelfCallAllowanceAlsoForOverride && f == EnclosingFunction.OverriddenFunction); + } + + public CanCallOptions(bool skipIsA, Function enclosingFunction, bool selfCallAllowanceAlsoForOverride = false) { + Contract.Assert(!selfCallAllowanceAlsoForOverride || + (enclosingFunction.OverriddenFunction != null && + enclosingFunction.Ins.Count == enclosingFunction.OverriddenFunction.Ins.Count)); + this.SkipIsA = skipIsA; + this.EnclosingFunction = enclosingFunction; + this.SelfCallAllowanceAlsoForOverride = selfCallAllowanceAlsoForOverride; + } + } } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 777fa6adc9b..79dbe57e16b 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -159,6 +159,7 @@ public void CheckWellformedAndAssume(Expression expr, WFOptions wfOptions, Varia CheckWellformedAndAssume(e.E0, wfOptions, locals, bAnd, etran, comment); CheckWellformedAndAssume(e.E1, wfOptions, locals, bAnd, etran, comment); var bImp = new BoogieStmtListBuilder(this, options, builder.Context); + bImp.Add(TrAssumeCmd(expr.Tok, etran.CanCallAssumption(expr))); bImp.Add(TrAssumeCmdWithDependencies(etran, expr.Tok, expr, comment)); builder.Add(new Bpl.IfCmd(expr.Tok, null, bAnd.Collect(expr.Tok), null, bImp.Collect(expr.Tok))); } @@ -173,6 +174,7 @@ public void CheckWellformedAndAssume(Expression expr, WFOptions wfOptions, Varia var b0 = new BoogieStmtListBuilder(this, options, builder.Context); CheckWellformedAndAssume(e.E0, wfOptions, locals, b0, etran, comment); var b1 = new BoogieStmtListBuilder(this, options, builder.Context); + b1.Add(TrAssumeCmd(expr.Tok, etran.CanCallAssumption(e.E0))); b1.Add(TrAssumeCmdWithDependenciesAndExtend(etran, expr.Tok, e.E0, Expr.Not, comment)); CheckWellformedAndAssume(e.E1, wfOptions, locals, b1, etran, comment); builder.Add(new Bpl.IfCmd(expr.Tok, null, b0.Collect(expr.Tok), null, b1.Collect(expr.Tok))); @@ -194,6 +196,7 @@ public void CheckWellformedAndAssume(Expression expr, WFOptions wfOptions, Varia CheckWellformedAndAssume(e.Test, wfOptions, locals, bThn, etran, comment); CheckWellformedAndAssume(e.Thn, wfOptions, locals, bThn, etran, comment); var bEls = new BoogieStmtListBuilder(this, options, builder.Context); + bEls.Add(TrAssumeCmd(expr.Tok, etran.CanCallAssumption(e.Test))); bEls.Add(TrAssumeCmdWithDependenciesAndExtend(etran, expr.Tok, e.Test, Expr.Not, comment)); CheckWellformedAndAssume(e.Els, wfOptions, locals, bEls, etran, comment); builder.Add(new Bpl.IfCmd(expr.Tok, null, bThn.Collect(expr.Tok), null, bEls.Collect(expr.Tok))); @@ -643,7 +646,7 @@ public void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, var desc = new ReadFrameSubset("invoke function", requiredFrame, readFrames); CheckFrameSubset(applyExpr.Tok, new List { wrappedReads }, null, null, - etran, etran.ReadsFrame(applyExpr.Tok), wfOptions.AssertSink(this, builder), desc, wfOptions.AssertKv); + etran, etran.ReadsFrame(applyExpr.Tok), wfOptions.AssertSink(this, builder), (ta, qa) => builder.Add(new Bpl.AssumeCmd(ta, qa)), desc, wfOptions.AssertKv); } break; @@ -808,7 +811,7 @@ public void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, } var desc = new ReadFrameSubset("invoke function", requiredFrames, readFrames); CheckFrameSubset(expr.Tok, new List { reads }, null, null, - etran, etran.ReadsFrame(expr.Tok), wfOptions.AssertSink(this, builder), desc, wfOptions.AssertKv); + etran, etran.ReadsFrame(expr.Tok), wfOptions.AssertSink(this, builder), (ta, qa) => builder.Add(new Bpl.AssumeCmd(ta, qa)), desc, wfOptions.AssertKv); } } else { @@ -816,10 +819,11 @@ public void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, var argSubstMap = e.Function.Ins.Zip(e.Args).ToDictionary(fa => fa.First as IVariable, fa => fa.Second); var directSub = new Substituter(e.Receiver, argSubstMap, e.GetTypeArgumentSubstitutions()); - foreach (AttributedExpression p in e.Function.Req) { + foreach (AttributedExpression p in ConjunctsOf(e.Function.Req)) { var directPrecond = directSub.Substitute(p.E); Expression precond = Substitute(p.E, e.Receiver, substMap, e.GetTypeArgumentSubstitutions()); + builder.Add(TrAssumeCmd(precond.Tok, etran.CanCallAssumption(precond))); var (errorMessage, successMessage) = CustomErrorMessage(p.Attributes); foreach (var ss in TrSplitExpr(builder.Context, precond, etran, true, out _)) { if (ss.IsChecked) { @@ -849,7 +853,7 @@ public void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, var readsSubst = new Substituter(null, new Dictionary(), e.GetTypeArgumentSubstitutions()); CheckFrameSubset(callExpr.Tok, e.Function.Reads.Expressions.ConvertAll(readsSubst.SubstFrameExpr), - e.Receiver, substMap, etran, etran.ReadsFrame(callExpr.Tok), wfOptions.AssertSink(this, builder), desc, wfOptions.AssertKv); + e.Receiver, substMap, etran, etran.ReadsFrame(callExpr.Tok), wfOptions.AssertSink(this, builder), (ta, qa) => builder.Add(new Bpl.AssumeCmd(ta, qa)), desc, wfOptions.AssertKv); } } Expression allowance = null; @@ -861,8 +865,6 @@ public void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, if (wfOptions.DoOnlyCoarseGrainedTerminationChecks) { builder.Add(Assert(GetToken(expr), Bpl.Expr.False, new IsNonRecursive(), builder.Context)); } else { - List contextDecreases = codeContext.Decreases.Expressions; - List calleeDecreases = e.Function.Decreases.Expressions; if (e.Function == wfOptions.SelfCallsAllowance) { allowance = Expression.CreateBoolLiteral(e.Tok, true); if (!e.Function.IsStatic) { @@ -898,9 +900,15 @@ public void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Contract.Assert(false); // unexpected CoCallResolution goto case FunctionCallExpr.CoCallResolution.No; // please the compiler } + + if (e.Function == wfOptions.SelfCallsAllowance) { + allowance = etran.MakeAllowance(e); + } if (e.CoCallHint != null) { hint = hint == null ? e.CoCallHint : string.Format("{0}; {1}", hint, e.CoCallHint); } + List contextDecreases = codeContext.Decreases.Expressions; + List calleeDecreases = e.Function.Decreases.Expressions; CheckCallTermination(callExpr.Tok, contextDecreases, calleeDecreases, allowance, e.Receiver, substMap, directSubstMap, e.GetTypeArgumentSubstitutions(), etran, false, builder, codeContext.InferredDecreases, hint); } @@ -976,6 +984,7 @@ public void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, CheckFrameSubset(fe.E.Tok, new List() { fe }, null, new Dictionary(), etran, etran.ReadsFrame(fe.E.Tok), wfOptions.AssertSink(this, builder), + (ta, qa) => builder.Add(new Bpl.AssumeCmd(ta, qa)), desc, wfOptions.AssertKv); } } @@ -1244,16 +1253,24 @@ void AddResultCommands(BoogieStmtListBuilder returnBuilder, Expression result) { Contract.Assert(substMapPrime != null); Contract.Assert(bodyLeftPrime != null); Contract.Assert(bodyPrime != null); + Bpl.Expr guardPrimeCanCall = null; Bpl.Expr guardPrime = null; if (guard != null) { Contract.Assert(e.Range != null); var rangePrime = Substitute(e.Range, null, substMapPrime); + guardPrimeCanCall = comprehensionEtran.CanCallAssumption(rangePrime); guardPrime = comprehensionEtran.TrExpr(rangePrime); } BplIfIf(e.Tok, guard != null, BplAnd(guard, guardPrime), newBuilder, b => { + var canCalls = guardPrimeCanCall ?? Bpl.Expr.True; + canCalls = BplAnd(canCalls, comprehensionEtran.CanCallAssumption(bodyLeft)); + canCalls = BplAnd(canCalls, comprehensionEtran.CanCallAssumption(bodyLeftPrime)); + canCalls = BplAnd(canCalls, comprehensionEtran.CanCallAssumption(body)); + canCalls = BplAnd(canCalls, comprehensionEtran.CanCallAssumption(bodyPrime)); var different = BplOr( Bpl.Expr.Neq(comprehensionEtran.TrExpr(bodyLeft), comprehensionEtran.TrExpr(bodyLeftPrime)), Bpl.Expr.Eq(comprehensionEtran.TrExpr(body), comprehensionEtran.TrExpr(bodyPrime))); + b.Add(new AssumeCmd(mc.TermLeft.Tok, canCalls)); b.Add(Assert(GetToken(mc.TermLeft), different, new ComprehensionNoAlias(mc.BoundVars, mc.Range, mc.TermLeft, mc.Term), builder.Context)); }); @@ -1286,6 +1303,7 @@ void AddResultCommands(BoogieStmtListBuilder returnBuilder, Expression result) { } builder.Add(new Bpl.CommentCmd("End Comprehension WF check")); + builder.Add(TrAssumeCmd(expr.Tok, etran.CanCallAssumption(expr))); break; } case StmtExpr stmtExpr: @@ -1363,7 +1381,6 @@ void AddResultCommands(BoogieStmtListBuilder returnBuilder, Expression result) { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression } - addResultCommands?.Invoke(builder, expr); } @@ -1371,11 +1388,11 @@ public void CheckSubsetType(ExpressionTranslator etran, Expression expr, Bpl.Exp BoogieStmtListBuilder builder, string comment) { Contract.Assert(resultType != null); + builder.Add(TrAssumeCmd(expr.Tok, etran.CanCallAssumption(expr))); var bResult = etran.TrExpr(expr); CheckSubrange(expr.Tok, bResult, expr.Type, resultType, expr, builder); builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, expr.Tok, expr, e => Bpl.Expr.Eq(selfCall, AdaptBoxing(expr.Tok, e, expr.Type, resultType)), comment)); - builder.Add(TrAssumeCmd(expr.Tok, etran.CanCallAssumption(expr))); builder.Add(new CommentCmd("CheckWellformedWithResult: any expression")); builder.Add(TrAssumeCmd(expr.Tok, MkIs(selfCall, resultType))); } @@ -1656,7 +1673,7 @@ private void CheckElementInit(IOrigin tok, bool forArray, List dims, ); var readsDesc = new ReadFrameSubset("invoke the function passed as an argument to the sequence constructor", readsDescExpr); CheckFrameSubset(tok, new List { reads }, null, null, - etran, etran.ReadsFrame(tok), maker, readsDesc, options.AssertKv); + etran, etran.ReadsFrame(tok), maker, (ta, qa) => builder.Add(new Bpl.AssumeCmd(ta, qa)), readsDesc, options.AssertKv); } // Check that the values coming out of the function satisfy any appropriate subset-type constraints var apply = UnboxUnlessInherentlyBoxed(FunctionCall(tok, Apply(dims.Count), TrType(elementType), args), elementType); @@ -1673,12 +1690,20 @@ private void CheckElementInit(IOrigin tok, bool forArray, List dims, if (forArray) { // Assume that array elements have initial values according to the given initialization function. That is: // assume (forall i0,i1,i2,... :: { nw[i0,i1,i2,...] } - // 0 <= i0 < ... && ... ==> nw[i0,i1,i2,...] == init.requires(i0,i1,i2,...)); + // 0 <= i0 < ... && ... ==> + // CanCallAssumptions[[ init(i0,i1,i2,...) ]] && + // nw[i0,i1,i2,...] == init.requires(i0,i1,i2,...)); + var dafnyInitApplication = new ApplyExpr(tok, init, + bvs.ConvertAll(indexBv => (Expression)new BoogieWrapper(new Bpl.IdentifierExpr(indexBv.tok, indexBv), Type.Int)).ToList(), + Token.NoToken) { + Type = sourceType.Result + }; + var canCall = etran.CanCallAssumption(dafnyInitApplication); + var ai = ReadHeap(tok, etran.HeapExpr, nw, GetArrayIndexFieldName(tok, indices)); var ai_prime = UnboxUnlessBoxType(tok, ai, elementType); var tr = new Bpl.Trigger(tok, true, new List { ai }); - q = new Bpl.ForallExpr(tok, bvs, tr, - BplImp(ante, Bpl.Expr.Eq(ai_prime, apply))); // TODO: use a more general Equality translation + q = new Bpl.ForallExpr(tok, bvs, tr, BplImp(ante, BplAnd(canCall, Bpl.Expr.Eq(ai_prime, apply)))); builder.Add(new Bpl.AssumeCmd(tok, q)); } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs index adb95ca68a7..398945d28f0 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs @@ -189,10 +189,9 @@ void AddWellformednessCheck(ConstantField decl) { // the procedure itself var req = new List(); // free requires mh == ModuleContextHeight && fh == TypeContextHeight; - req.Add(Requires(decl.Tok, true, null, etran.HeightContext(decl), null, null, null)); - + req.Add(FreeRequires(decl.Tok, etran.HeightContext(decl), null)); foreach (var typeBoundAxiom in TypeBoundAxioms(decl.Tok, decl.EnclosingClass.TypeArgs)) { - req.Add(Requires(decl.Tok, true, null, typeBoundAxiom, null, null, null)); + req.Add(FreeRequires(decl.Tok, typeBoundAxiom, null)); } var heapVar = new Bpl.IdentifierExpr(decl.Tok, "$Heap", false); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index 1ac970c8b93..da0aaa2a16f 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -43,11 +43,13 @@ public void Check(Function f) { var context = new BodyTranslationContext(f.ContainsHide); var ens = new List(); - foreach (AttributedExpression ensures in f.Ens) { + foreach (AttributedExpression ensures in ConjunctsOf(f.Ens)) { var functionHeight = generator.currentModule.CallGraph.GetSCCRepresentativePredecessorCount(f); var splits = new List(); bool splitHappened /*we actually don't care*/ = generator.TrSplitExpr(context, ensures.E, splits, true, functionHeight, true, etran); var (errorMessage, successMessage) = generator.CustomErrorMessage(ensures.Attributes); + var canCalls = etran.CanCallAssumption(ensures.E, new CanCallOptions(true, f)); + generator.AddEnsures(ens, generator.FreeEnsures(ensures.E.Tok, canCalls, null, true)); foreach (var s in splits) { if (s.IsChecked && !s.Tok.IsInherited(generator.currentModule)) { generator.AddEnsures(ens, generator.EnsuresWithDependencies(s.Tok, false, ensures.E, s.E, errorMessage, successMessage, null)); @@ -119,7 +121,7 @@ public void Check(Function f) { // of them), do the postponed reads checks. delayer.DoWithDelayedReadsChecks(false, wfo => { builder.Add(new CommentCmd("Check well-formedness of preconditions, and then assume them")); - foreach (AttributedExpression require in f.Req) { + foreach (AttributedExpression require in ConjunctsOf(f.Req)) { if (require.Label != null) { require.Label.E = (f is TwoStateFunction ? ordinaryEtran : etran.Old).TrExpr(require.E); generator.CheckWellformed(require.E, wfo, locals, builder, etran); @@ -371,7 +373,7 @@ private List GetWellformednessProcedureOutParameters(Function f, Expre private List GetWellformednessProcedureRequires(Function f, ExpressionTranslator etran) { var requires = new List(); // free requires mh == ModuleContextHeight && fh == FunctionContextHeight; - requires.Add(generator.Requires(f.Tok, true, null, etran.HeightContext(f), null, null, null)); + requires.Add(generator.FreeRequires(f.Tok, etran.HeightContext(f), null)); foreach (var typeBoundAxiom in generator.TypeBoundAxioms(f.Tok, Concat(f.EnclosingClass.TypeArgs, f.TypeArgs))) { requires.Add(generator.Requires(f.Tok, true, null, typeBoundAxiom, null, null, null)); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs index 6d2c3792d10..1a745c00b4d 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs @@ -230,7 +230,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis } Bpl.Expr pre = Bpl.Expr.True; - foreach (AttributedExpression req in f.Req) { + foreach (AttributedExpression req in ConjunctsOf(f.Req)) { pre = BplAnd(pre, etran.TrExpr(req.E)); } // useViaContext: fh < FunctionContextHeight @@ -238,15 +238,14 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis ? Bpl.Expr.True : Bpl.Expr.Lt(Expr.Literal(forModule.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight()); // useViaCanCall: f#canCall(args) - Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.Tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool); - Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.Tok, new Bpl.FunctionCall(canCallFuncID), Concat(tyargs, args)); + var canCallFuncID = new Bpl.IdentifierExpr(f.Tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool); + var useViaCanCall = new Bpl.NAryExpr(f.Tok, new Bpl.FunctionCall(canCallFuncID), Concat(tyargs, args)); - // ante := useViaCanCall || (useViaContext && typeAnte && pre) - ante = BplOr(useViaCanCall, BplAnd(useViaContext, BplAnd(ante, pre))); - anteIsAlloc = BplOr(useViaCanCall, BplAnd(useViaContext, BplAnd(anteIsAlloc, pre))); + // ante := useViaCanCall + ante = useViaCanCall; + anteIsAlloc = useViaCanCall; - Bpl.Trigger tr = BplTriggerHeap(this, f.Tok, funcAppl, - (f.ReadsHeap || !readsHeap) ? null : etran.HeapExpr); + var tr = BplTriggerHeap(this, f.Tok, funcAppl, (f.ReadsHeap || !readsHeap) ? null : etran.HeapExpr); Bpl.Expr post = Bpl.Expr.True; // substitute function return value with the function call. var substMap = new Dictionary(); @@ -254,7 +253,10 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis substMap.Add(f.Result, new BoogieWrapper(funcAppl, f.ResultType)); } foreach (AttributedExpression p in ens) { - Bpl.Expr q = etran.TrExpr(Substitute(p.E, null, substMap)); + var bodyWithSubst = Substitute(p.E, null, substMap); + var canCallEns = etran.CanCallAssumption(bodyWithSubst); + post = BplAnd(post, canCallEns); + var q = etran.TrExpr(bodyWithSubst); post = BplAnd(post, q); } var (olderParameterCount, olderCondition) = OlderCondition(f, funcAppl, olderInParams); @@ -267,11 +269,9 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis Bpl.Expr axBody = BplImp(ante, post); Bpl.Expr ax = BplForall(f.Tok, new List(), formals, null, tr, axBody); var activate = AxiomActivation(f, etran); - string comment = "consequence axiom for " + f.FullSanitizedName; if (RemoveLit(axBody) != Bpl.Expr.True) { - var consequenceExpr = BplImp(activate, ax); - var consequenceAxiom = new Bpl.Axiom(f.Tok, consequenceExpr, comment); - AddOtherDefinition(boogieFunction, consequenceAxiom); + AddOtherDefinition(boogieFunction, new Bpl.Axiom(f.Tok, BplImp(activate, ax), + "consequence axiom for " + f.FullSanitizedName)); } if (f.ResultType.MayInvolveReferences) { @@ -289,7 +289,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis ax = BplForall(f.Tok, new List(), formals, null, BplTrigger(whr), axBody); if (RemoveLit(axBody) != Bpl.Expr.True) { - comment = "alloc consequence axiom for " + f.FullSanitizedName; + var comment = "alloc consequence axiom for " + f.FullSanitizedName; var allocConsequenceAxiom = new Bpl.Axiom(f.Tok, BplImp(activate, ax), comment); AddOtherDefinition(boogieFunction, allocConsequenceAxiom); } @@ -376,9 +376,9 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { f.ReadsHeap ? new Bpl.IdentifierExpr(f.Tok, Predef.HeapVarName, Predef.HeapType) : null, new Bpl.IdentifierExpr(f.Tok, bvPrevHeap), f); } else { - etran = readsHeap + etran = f.ReadsHeap ? new ExpressionTranslator(this, Predef, f.Tok, f) - : new ExpressionTranslator(this, Predef, (Bpl.Expr)null, f); + : new ExpressionTranslator(this, Predef, readsHeap ? NewOneHeapExpr(f.Tok) : null, f); } // quantify over the type arguments, and add them first to the arguments @@ -421,26 +421,19 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { ante = BplAnd(ante, FunctionCall(f.Tok, BuiltinFunction.IsGoodHeap, null, etran.Old.HeapExpr)); } - Bpl.Expr goodHeap = null; - var bv = new Bpl.BoundVariable(f.Tok, new Bpl.TypedIdent(f.Tok, Predef.HeapVarName, Predef.HeapType)); if (f.ReadsHeap) { + var bv = new Bpl.BoundVariable(f.Tok, new Bpl.TypedIdent(f.Tok, Predef.HeapVarName, Predef.HeapType)); funcFormals.Add(bv); - } - - if (f.ReadsHeap) { args.Add(new Bpl.IdentifierExpr(f.Tok, bv)); reqFuncArguments.Add(new Bpl.IdentifierExpr(f.Tok, bv)); - } - // ante: $IsGoodHeap($Heap) && $HeapSucc($prevHeap, $Heap) && this != null && formals-have-the-expected-types && - if (readsHeap) { + // ante: $IsGoodHeap($Heap) && $HeapSucc($prevHeap, $Heap) && this != null && formals-have-the-expected-types && forallFormals.Add(bv); - goodHeap = FunctionCall(f.Tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr); + var goodHeap = FunctionCall(f.Tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr); ante = BplAnd(ante, goodHeap); - } - - if (f is TwoStateFunction && f.ReadsHeap) { - ante = BplAnd(ante, HeapSucc(etran.Old.HeapExpr, etran.HeapExpr)); + if (f is TwoStateFunction) { + ante = BplAnd(ante, HeapSucc(etran.Old.HeapExpr, etran.HeapExpr)); + } } // ante: conditions on bounded type parameters @@ -479,7 +472,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { var substMap = new Dictionary(); foreach (Formal p in f.Ins) { var pType = p.Type.Subst(typeMap); - bv = new Bpl.BoundVariable(p.Tok, + var bv = new Bpl.BoundVariable(p.Tok, new Bpl.TypedIdent(p.Tok, p.AssignUniqueName(CurrentDeclaration.IdGenerator), TrType(pType))); forallFormals.Add(bv); funcFormals.Add(bv); @@ -510,7 +503,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { } Bpl.Expr pre = Bpl.Expr.True; - foreach (AttributedExpression req in f.Req) { + foreach (AttributedExpression req in ConjunctsOf(f.Req)) { pre = BplAnd(pre, etran.TrExpr(Substitute(req.E, receiverReplacement, substMap))); } @@ -531,6 +524,9 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { preReqAxiom = BplAnd(preRA, pre); } + var canCallFuncID = new Bpl.IdentifierExpr(f.Tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool); + var useViaCanCall = new Bpl.NAryExpr(f.Tok, new Bpl.FunctionCall(canCallFuncID), Concat(tyargs, args)); + // Add the precondition function and its axiom (which is equivalent to the anteReqAxiom) if (body == null || (RevealedInScope(f) && lits == null)) { var precondF = new Bpl.Function(f.Tok, @@ -540,31 +536,23 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { sink.AddTopLevelDeclaration(precondF); var appl = FunctionCall(f.Tok, RequiresName(f), Bpl.Type.Bool, reqFuncArguments); - Bpl.Trigger trig = BplTriggerHeap(this, f.Tok, appl, readsHeap ? etran.HeapExpr : null); + Bpl.Trigger trig = BplTriggerHeap(this, f.Tok, appl, f.ReadsHeap ? etran.HeapExpr : null); // axiom (forall params :: { f#requires(params) } ante ==> f#requires(params) == pre); AddOtherDefinition(precondF, new Axiom(f.Tok, BplForall(forallFormals, trig, BplImp(anteReqAxiom, Bpl.Expr.Eq(appl, preReqAxiom))), "#requires axiom for " + f.FullSanitizedName)); + + AddOtherDefinition(precondF, new Bpl.Axiom(f.Tok, + BplForall(f.Tok, new List(), forallFormals, null, trig, Bpl.Expr.Imp(appl, useViaCanCall)), + "#requires ==> #canCall for " + f.FullSanitizedName)) ; } if (body == null || !RevealedInScope(f)) { return null; } - // useViaContext: fh < FunctionContextHeight - ModuleDefinition mod = f.EnclosingClass.EnclosingModuleDefinition; - Bpl.Expr useViaContext = !InVerificationScope(f) - ? Bpl.Expr.True - : Bpl.Expr.Lt(Bpl.Expr.Literal(forModule.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight()); - // ante := (useViaContext && typeAnte && pre) - ante = BplAnd(useViaContext, BplAnd(ante, pre)); - // useViaCanCall: f#canCall(args) - Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.Tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool); - Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.Tok, new Bpl.FunctionCall(canCallFuncID), Concat(tyargs, args)); - - // ante := useViaCanCall || (useViaContext && typeAnte && pre) - ante = BplOr(useViaCanCall, ante); + ante = useViaCanCall; Bpl.Expr funcAppl; { @@ -588,7 +576,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { funcAppl = new Bpl.NAryExpr(f.Tok, new Bpl.FunctionCall(funcID), funcArgs); } - Bpl.Trigger tr = BplTriggerHeap(this, f.Tok, funcAppl, readsHeap ? etran.HeapExpr : null); + Bpl.Trigger tr = BplTriggerHeap(this, f.Tok, funcAppl, f.ReadsHeap ? etran.HeapExpr : null); Bpl.Expr tastyVegetarianOption; // a.k.a. the "meat" of the operation :) if (!RevealedInScope(f)) { tastyVegetarianOption = Bpl.Expr.True; @@ -954,13 +942,26 @@ void AddFrameAxiom(Function f) { Bpl.Expr formal = new Bpl.IdentifierExpr(p.Tok, bv); f0args.Add(formal); f1args.Add(formal); f0argsCanCall.Add(formal); f1argsCanCall.Add(formal); Bpl.Expr wh = GetWhereClause(p.Tok, formal, p.Type, etran0, useAlloc); - if (wh != null) { fwf0 = BplAnd(fwf0, wh); } + if (wh != null) { + fwf0 = BplAnd(fwf0, wh); + } + wh = GetWhereClause(p.Tok, formal, p.Type, etran1, useAlloc); + if (wh != null) { + fwf1 = BplAnd(fwf1, wh); + } } var canCall = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.Tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool)); - wellFormed = BplAnd(wellFormed, BplAnd( - BplOr(new Bpl.NAryExpr(f.Tok, canCall, f0argsCanCall), fwf0), - BplOr(new Bpl.NAryExpr(f.Tok, canCall, f1argsCanCall), fwf1))); - + var f0canCall = new Bpl.NAryExpr(f.Tok, canCall, f0argsCanCall); + var f1canCall = new Bpl.NAryExpr(f.Tok, canCall, f1argsCanCall); + wellFormed = BplAnd(wellFormed, Bpl.Expr.Or( + BplOr(f0canCall, fwf0), + BplOr(f1canCall, fwf1))); + /* + JA: I conjecture that we don't need fwf0 or fwf1 here. But, we + will need both can calls, + i.e., + wellFormed = BplAnd(wellFormed, BplOr(f0canCall, f1canCall)) + */ /* DR: I conjecture that this should be enough, as the requires is preserved when the frame is: @@ -972,7 +973,7 @@ void AddFrameAxiom(Function f) { var fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.Tok, f.FullSanitizedName, TrType(f.ResultType))); var F0 = new Bpl.NAryExpr(f.Tok, fn, f0args); var F1 = new Bpl.NAryExpr(f.Tok, fn, f1args); - var eq = Bpl.Expr.Eq(F0, F1); + var eq = BplAnd(Bpl.Expr.Eq(F0, F1), Bpl.Expr.Eq(f0canCall, f1canCall)); var tr = new Bpl.Trigger(f.Tok, true, new List { h0IsHeapAnchor, heapSucc, F1 }); var ax = new Bpl.ForallExpr(f.Tok, new List(), bvars, null, tr, diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs index 208841755a6..1b78051ed2a 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs @@ -81,7 +81,7 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) { // FREE PRECONDITIONS if (kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation) { // the other cases have no need for a free precondition // free requires mh == ModuleContextHeight && fh = FunctionContextHeight; - req.Add(Requires(iter.Tok, true, null, etran.HeightContext(iter), null, null, null)); + req.Add(FreeRequires(iter.Tok, etran.HeightContext(iter), null)); } mod.Add(etran.HeapCastToIdentifierExpr); @@ -89,6 +89,7 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) { // USER-DEFINED SPECIFICATIONS var comment = "user-defined preconditions"; foreach (var p in iter.Requires) { + req.Add(FreeRequires(p.E.Tok, etran.CanCallAssumption(p.E), comment, true)); var (errorMessage, successMessage) = CustomErrorMessage(p.Attributes); if (p.Label != null && kind == MethodTranslationKind.Implementation) { // don't include this precondition here, but record it for later use @@ -107,6 +108,9 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) { } comment = "user-defined postconditions"; foreach (var p in iter.Ensures) { + var canCalls = etran.CanCallAssumption(p.E); + AddEnsures(ens, FreeEnsures(p.E.Tok, canCalls, comment, true)); + foreach (var split in TrSplitExprForMethodSpec(new BodyTranslationContext(false), p.E, etran, kind)) { if (kind == MethodTranslationKind.Implementation && split.Tok.IsInherited(currentModule)) { // this postcondition was inherited into this module, so just ignore it @@ -175,7 +179,7 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) { } // Next, we assume about this.* whatever we said that the iterator constructor promises - foreach (var p in iter.Member_Init.Ens) { + foreach (var p in ConjunctsOf(iter.Member_Init.Ens)) { builder.Add(TrAssumeCmdWithDependencies(etran, p.E.Tok, p.E, "iterator ensures clause")); } @@ -289,7 +293,7 @@ void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) { // add locals for the yield-history variables and the extra variables // Assume the precondition and postconditions of the iterator constructor method - foreach (var p in iter.Member_Init.Req) { + foreach (var p in ConjunctsOf(iter.Member_Init.Req)) { if (p.Label != null) { // don't include this precondition here Contract.Assert(p.Label.E != null); // it should already have been recorded @@ -297,7 +301,7 @@ void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) { builder.Add(TrAssumeCmdWithDependencies(etran, p.E.Tok, p.E, "iterator constructor requires clause")); } } - foreach (var p in iter.Member_Init.Ens) { + foreach (var p in ConjunctsOf(iter.Member_Init.Ens)) { // these postconditions are two-state predicates, but that's okay, because we haven't changed anything yet builder.Add(TrAssumeCmdWithDependencies(etran, p.E.Tok, p.E, "iterator constructor ensures clause")); } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs b/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs index 53ed8f87027..b3c41aacccd 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs @@ -17,7 +17,7 @@ namespace Microsoft.Dafny { public partial class BoogieGenerator { public partial class ExpressionTranslator { - private Expr LetCanCallAssumption(LetExpr expr) { + private Expr LetCanCallAssumption(LetExpr expr, CanCallOptions cco) { if (!expr.Exact) { // CanCall[[ var b0,b1 :| RHS(b0,b1,g); Body(b0,b1,g,h) ]] = // $let$canCall(g) && @@ -35,7 +35,7 @@ private Expr LetCanCallAssumption(LetExpr expr) { substMap.Add(bv, call); } var p = Substitute(expr.Body, null, substMap); - var cc = BplAnd(canCall, CanCallAssumption(p)); + var cc = BplAnd(canCall, CanCallAssumption(p, cco)); return cc; } else { // CanCall[[ var b := RHS(g); Body(b,g,h) ]] = @@ -43,7 +43,7 @@ private Expr LetCanCallAssumption(LetExpr expr) { // (var lhs0,lhs1,... := rhs0,rhs1,...; CanCall[[ Body ]]) Boogie.Expr canCallRHS = Boogie.Expr.True; foreach (var rhs in expr.RHSs) { - canCallRHS = BplAnd(canCallRHS, CanCallAssumption(rhs)); + canCallRHS = BplAnd(canCallRHS, CanCallAssumption(rhs, cco)); } var bodyCanCall = CanCallAssumption(expr.Body); @@ -249,7 +249,7 @@ private void AddLetSuchThenCanCallAxiom(LetExpr e, LetSuchThatExprInfo info, Bpl var call = FunctionCall(e.Tok, info.SkolemFunctionName(bv), BoogieGenerator.TrType(bv.Type), gExprs); tr = new Bpl.Trigger(e.Tok, true, new List { call }, tr); substMap.Add(bv, new BoogieWrapper(call, bv.Type)); - if (!(bv.Type.IsTypeParameter)) { + if (!bv.Type.IsTypeParameter) { Bpl.Expr wh = BoogieGenerator.GetWhereClause(bv.Tok, call, bv.Type, etranCC, NOALLOC); if (wh != null) { antecedent = BplAnd(antecedent, wh); @@ -274,7 +274,8 @@ private void AddLetSuchThenCanCallAxiom(LetExpr e, LetSuchThatExprInfo info, Bpl var canCall = FunctionCall(e.Tok, info.CanCallFunctionName(), Bpl.Type.Bool, gExprs); var p = Substitute(e.RHSs[0], receiverReplacement, substMap); - Bpl.Expr ax = BplImp(canCall, BplAnd(antecedent, etranCC.TrExpr(p))); + var canCallBody = etranCC.CanCallAssumption(p); + Bpl.Expr ax = BplImp(canCall, BplAnd(antecedent, BplAnd(canCallBody, etranCC.TrExpr(p)))); ax = BplForall(gg, tr, ax); BoogieGenerator.AddOtherDefinition(canCallFunction, new Bpl.Axiom(e.Tok, ax)); } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index 3f692eafaac..b4a0efb67f0 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -612,7 +612,7 @@ private StmtList TrMethodContractWellformednessCheck(Method m, ExpressionTransla // check well-formedness of the preconditions, and then assume each one of them readsCheckDelayer.DoWithDelayedReadsChecks(false, wfo => { - foreach (AttributedExpression p in m.Req) { + foreach (AttributedExpression p in ConjunctsOf(m.Req)) { CheckWellformedAndAssume(p.E, wfo, localVariables, builder, etran, "method requires clause"); } }); @@ -684,7 +684,7 @@ private StmtList TrMethodContractWellformednessCheck(Method m, ExpressionTransla } // check wellformedness of postconditions - foreach (AttributedExpression p in m.Ens) { + foreach (AttributedExpression p in ConjunctsOf(m.Ens)) { CheckWellformedAndAssume(p.E, wfOptions, localVariables, builder, etran, "method ensures clause"); } @@ -779,18 +779,21 @@ private StmtList TrMethodBody(Method m, BoogieStmtListBuilder builder, Variables var decrCaller = new List(); var decrCalleeDafny = new List(); var decrCallerDafny = new List(); + Bpl.Expr canCalls = Bpl.Expr.True; foreach (var ee in m.Decreases.Expressions) { decrToks.Add(ee.Tok); decrTypes.Add(ee.Type.NormalizeExpand()); decrCallerDafny.Add(ee); + canCalls = BplAnd(canCalls, exprTran.CanCallAssumption(ee)); decrCaller.Add(exprTran.TrExpr(ee)); Expression es = Substitute(ee, receiverSubst, substMap); es = Substitute(es, null, decrSubstMap); decrCalleeDafny.Add(es); + canCalls = BplAnd(canCalls, exprTran.CanCallAssumption(ee)); decrCallee.Add(exprTran.TrExpr(es)); } - return DecreasesCheck(decrToks, null, decrCalleeDafny, decrCallerDafny, decrCallee, decrCaller, - null, null, false, true); + return BplImp(canCalls, + DecreasesCheck(decrToks, null, decrCalleeDafny, decrCallerDafny, decrCallee, decrCaller, null, null, false, true)); }; var triggers = m.Attributes.AsEnumerable() @@ -806,7 +809,7 @@ private StmtList TrMethodBody(Method m, BoogieStmtListBuilder builder, Variables builder.Add(new Bpl.IfCmd(m.Tok, null, definedness.Collect(m.Tok), null, exporter.Collect(m.Tok))); #else TrForallStmtCall(m.Tok, parBoundVars, parBounds, parRange, decrCheck, null, triggers, recursiveCall, null, - builder, localVariables, etran); + builder, localVariables, etran, includeCanCalls: true); #endif } // translate the body of the method @@ -999,13 +1002,13 @@ private void AddFunctionOverrideCheckImpl(Function f) { // the procedure itself var req = new List(); // free requires fh == FunctionContextHeight; - req.Add(Requires(f.Tok, true, null, etran.HeightContext(f), null, null, null)); + req.Add(FreeRequires(f.Tok, etran.HeightContext(f), null)); if (f is TwoStateFunction) { // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap) var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr); var a1 = HeapSucc(prevHeap, currHeap); var a2 = FunctionCall(f.Tok, BuiltinFunction.IsGoodHeap, null, currHeap); - req.Add(Requires(f.Tok, true, null, BplAnd(a0, BplAnd(a1, a2)), null, null, null)); + req.Add(FreeRequires(f.Tok, BplAnd(a0, BplAnd(a1, a2)), null)); } foreach (var typeBoundAxiom in TypeBoundAxioms(f.Tok, Concat(f.EnclosingClass.TypeArgs, f.TypeArgs))) { req.Add(Requires(f.Tok, true, null, typeBoundAxiom, null, null, null)); @@ -1099,8 +1102,10 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder Bpl.Variable/*?*/ resultVariable) { Contract.Requires(f.Ins.Count <= implInParams.Count); + var cco = new CanCallOptions(true, f); //generating class post-conditions - foreach (var en in f.Ens) { + foreach (var en in ConjunctsOf(f.Ens)) { + builder.Add(TrAssumeCmd(f.Tok, etran.CanCallAssumption(en.E, cco))); builder.Add(TrAssumeCmdWithDependencies(etran, f.Tok, en.E, "overridden function ensures clause")); } @@ -1141,11 +1146,13 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder .Select(e => e.E) .Aggregate((e0, e1) => new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, e0, e1)); //generating trait post-conditions with class variables + cco = new CanCallOptions(true, f, true); FunctionCallSubstituter sub = null; - foreach (var en in f.OverriddenFunction.Ens) { + foreach (var en in ConjunctsOf(f.OverriddenFunction.Ens)) { sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (TopLevelDeclWithMembers)f.EnclosingClass); var subEn = sub.Substitute(en.E); - foreach (var s in TrSplitExpr(new BodyTranslationContext(false), sub.Substitute(en.E), etran, false, out _).Where(s => s.IsChecked)) { + foreach (var s in TrSplitExpr(new BodyTranslationContext(false), subEn, etran, false, out _).Where(s => s.IsChecked)) { + builder.Add(TrAssumeCmd(f.Tok, etran.CanCallAssumption(subEn, cco))); var constraint = allOverrideEns == null ? null : new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Imp, allOverrideEns, subEn); @@ -1231,19 +1238,23 @@ private void AddFunctionOverrideReqsChk(Function f, BoogieStmtListBuilder builde Contract.Requires(etran != null); Contract.Requires(substMap != null); //generating trait pre-conditions with class variables + var cco = new CanCallOptions(true, f, true); FunctionCallSubstituter sub = null; var subReqs = new List(); - foreach (var req in f.OverriddenFunction.Req) { + foreach (var req in ConjunctsOf(f.OverriddenFunction.Req)) { sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (TopLevelDeclWithMembers)f.EnclosingClass); var subReq = sub.Substitute(req.E); + builder.Add(TrAssumeCmd(f.Tok, etran.CanCallAssumption(subReq, cco))); builder.Add(TrAssumeCmdWithDependencies(etran, f.Tok, subReq, "overridden function requires clause")); subReqs.Add(subReq); } var allTraitReqs = subReqs.Count == 0 ? null : subReqs .Aggregate((e0, e1) => new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, e0, e1)); //generating class pre-conditions - foreach (var req in f.Req) { + cco = new CanCallOptions(true, f); + foreach (var req in ConjunctsOf(f.Req)) { foreach (var s in TrSplitExpr(new BodyTranslationContext(false), req.E, etran, false, out _).Where(s => s.IsChecked)) { + builder.Add(TrAssumeCmd(f.Tok, etran.CanCallAssumption(req.E, cco))); var constraint = allTraitReqs == null ? null : new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Imp, allTraitReqs, req.E); @@ -1257,8 +1268,9 @@ private void AddFunctionOverrideReqsChk(Function f, BoogieStmtListBuilder builde /// axiom (forall $heap: HeapType, typeArgs: Ty, this: ref, x#0: int, fuel: LayerType :: /// { J.F(fuel, $heap, G(typeArgs), this, x#0), C.F(fuel, $heap, typeArgs, this, x#0) } /// { J.F(fuel, $heap, G(typeArgs), this, x#0), $Is(this, C) } - /// C.F#canCall(args) || (fh < FunctionContextHeight && this != null && $Is(this, C)) + /// C.F#canCall(args) || (J.F#canCall(args) && $Is(this, C)) /// ==> + /// (J.F#canCall(args) ==> C.F#canCall(args)) && /// J.F(fuel, $heap, G(typeArgs), this, x#0) == C.F(fuel, $heap, typeArgs, this, x#0)); /// (without the other usual antecedents). Essentially, the override gives a part of the body of the /// trait's function, so we call FunctionAxiom to generate a conditional axiom (that is, we pass in the "overridingFunction" @@ -1295,14 +1307,23 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti // argsCF are the arguments to C.F (the overriding function) var forallFormals = new List(); var argsJF = new List(); + var argsJFCanCall = new List(); var argsCF = new List(); + var argsCFCanCall = new List(); // Add type arguments forallFormals.AddRange(MkTyParamBinders(GetTypeParams(overridingFunction), out _)); - argsJF.AddRange(GetTypeArguments(f, overridingFunction).ConvertAll(TypeToTy)); - argsCF.AddRange(GetTypeArguments(overridingFunction, null).ConvertAll(TypeToTy)); + { + var typeArguments = GetTypeArguments(f, overridingFunction).ConvertAll(TypeToTy); + argsJF.AddRange(typeArguments); + argsJFCanCall.AddRange(typeArguments); + typeArguments = GetTypeArguments(overridingFunction, null).ConvertAll(TypeToTy); + argsCF.AddRange(typeArguments); + argsCFCanCall.AddRange(typeArguments); + } - var moreArgsCF = new List(); + var moreArgsJF = new List(); // non-type-parameters, non-fuel, non-reveal arguments + var moreArgsCF = new List(); // non-type-parameters, non-fuel, non-reveal arguments Expr layer = null; Expr reveal = null; @@ -1333,14 +1354,14 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti if (f is TwoStateFunction) { Contract.Assert(bvPrevHeap != null); forallFormals.Add(bvPrevHeap); - argsJF.Add(etran.Old.HeapExpr); + moreArgsJF.Add(etran.Old.HeapExpr); moreArgsCF.Add(etran.Old.HeapExpr); } if (f.ReadsHeap || overridingFunction.ReadsHeap) { var heap = new Boogie.BoundVariable(f.Tok, new Boogie.TypedIdent(f.Tok, Predef.HeapVarName, Predef.HeapType)); forallFormals.Add(heap); if (f.ReadsHeap) { - argsJF.Add(new Boogie.IdentifierExpr(f.Tok, heap)); + moreArgsJF.Add(new Boogie.IdentifierExpr(f.Tok, heap)); } if (overridingFunction.ReadsHeap) { moreArgsCF.Add(new Boogie.IdentifierExpr(overridingFunction.Tok, heap)); @@ -1352,14 +1373,12 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti var bvThis = new Boogie.BoundVariable(f.Tok, new Boogie.TypedIdent(f.Tok, etran.This, TrType(thisType))); forallFormals.Add(bvThis); var bvThisExpr = new Boogie.IdentifierExpr(f.Tok, bvThis); - argsJF.Add(BoxifyForTraitParent(f.Tok, bvThisExpr, f, thisType)); + moreArgsJF.Add(BoxifyForTraitParent(f.Tok, bvThisExpr, f, thisType)); moreArgsCF.Add(bvThisExpr); // $Is(this, C) var isOfSubtype = GetWhereClause(overridingFunction.Tok, bvThisExpr, thisType, f is TwoStateFunction ? etran.Old : etran, IsAllocType.NEVERALLOC, alwaysUseSymbolicName: true); - Bpl.Expr ante = BplAnd(ReceiverNotNull(bvThisExpr), isOfSubtype); - // Add other arguments var typeMap = GetTypeArgumentSubstitutionMap(f, overridingFunction); foreach (Formal p in f.Ins) { @@ -1367,19 +1386,10 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti var bv = new Boogie.BoundVariable(p.Tok, new Boogie.TypedIdent(p.Tok, p.AssignUniqueName(CurrentDeclaration.IdGenerator), TrType(pType))); forallFormals.Add(bv); var jfArg = new Boogie.IdentifierExpr(p.Tok, bv); - argsJF.Add(ModeledAsBoxType(p.Type) ? BoxIfNotNormallyBoxed(p.Tok, jfArg, pType) : jfArg); + moreArgsJF.Add(ModeledAsBoxType(p.Type) ? BoxIfNotNormallyBoxed(p.Tok, jfArg, pType) : jfArg); moreArgsCF.Add(new Boogie.IdentifierExpr(p.Tok, bv)); } - // useViaContext: fh < FunctionContextHeight - Boogie.Expr useViaContext = !InVerificationScope(overridingFunction) - ? Boogie.Expr.True - : Boogie.Expr.Lt(Boogie.Expr.Literal(forModule.CallGraph.GetSCCRepresentativePredecessorCount(overridingFunction)), etran.FunctionContextHeight()); - - // useViaCanCall: C.F#canCall(args) - Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(overridingFunction.Tok, overridingFunction.FullSanitizedName + "#canCall", Bpl.Type.Bool); - Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.Tok, new Bpl.FunctionCall(canCallFuncID), Concat(argsCF, moreArgsCF)); - if (layer != null) { argsCF.Add(layer); } @@ -1388,10 +1398,24 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti argsCF.Add(reveal); } + argsJF = Concat(argsJF, moreArgsJF); + argsJFCanCall = Concat(argsJFCanCall, moreArgsJF); argsCF = Concat(argsCF, moreArgsCF); + argsCFCanCall = Concat(argsCFCanCall, moreArgsCF); - // ante := useViaCanCall || (useViaContext && this != null && $Is(this, C)) - ante = BplOr(useViaCanCall, BplAnd(useViaContext, ante)); + Bpl.Expr canCallFunc, canCallOverridingFunc; + { + var callName = new Bpl.IdentifierExpr(f.Tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool); + canCallFunc = new Bpl.NAryExpr(f.Tok, new Bpl.FunctionCall(callName), argsJFCanCall); + callName = new Bpl.IdentifierExpr(overridingFunction.Tok, overridingFunction.FullSanitizedName + "#canCall", Bpl.Type.Bool); + canCallOverridingFunc = new Bpl.NAryExpr(f.Tok, new Bpl.FunctionCall(callName), argsCFCanCall); + } + + // useViaCanCall: C.F#canCall(args) + Bpl.Expr useViaCanCall = canCallFunc; + + // ante := C.F#canCall(args) || (J.F#canCall(args) && $Is(this, C)) + var ante = BplOr(canCallOverridingFunc, BplAnd(canCallFunc, isOfSubtype)); Boogie.Expr funcAppl; { @@ -1405,11 +1429,10 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti } // Build the triggers - // { f(Succ(s), args), f'(Succ(s), args') } + // { f'(Succ(s), args') } Boogie.Trigger tr = BplTriggerHeap(this, overridingFunction.Tok, - funcAppl, - readsHeap ? etran.HeapExpr : null, - overridingFuncAppl); + overridingFuncAppl, + readsHeap ? etran.HeapExpr : null); // { f(Succ(s), args), $Is(this, T') } var exprs = new List() { funcAppl, isOfSubtype }; if (readsHeap) { @@ -1421,12 +1444,14 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti var synonyms = Boogie.Expr.Eq( funcAppl, ModeledAsBoxType(f.ResultType) ? BoxIfNotNormallyBoxed(overridingFunction.Tok, overridingFuncAppl, overridingFunction.ResultType) : overridingFuncAppl); + // add overridingFunction#canCall ==> f#canCall to the axiom + var canCallImp = BplImp(canCallFunc, canCallOverridingFunc); // The axiom Boogie.Expr ax = BplForall(f.Tok, new List(), forallFormals, null, tr, - BplImp(ante, synonyms)); + BplImp(ante, BplAnd(canCallImp, synonyms))); var activate = AxiomActivation(overridingFunction, etran); - string comment = "override axiom for " + f.FullSanitizedName + " in class " + overridingFunction.EnclosingClass.FullSanitizedName; + var comment = $"override axiom for {f.FullSanitizedName} in {overridingFunction.EnclosingClass.WhatKind} {overridingFunction.EnclosingClass.FullSanitizedName}"; return new Boogie.Axiom(f.Tok, BplImp(activate, ax), comment); } @@ -1479,7 +1504,8 @@ private void AddMethodOverrideEnsChk(Method m, BoogieStmtListBuilder builder, Ex Contract.Requires(etran != null); Contract.Requires(substMap != null); //generating class post-conditions - foreach (var en in m.Ens) { + foreach (var en in ConjunctsOf(m.Ens)) { + builder.Add(TrAssumeCmd(m.Tok, etran.CanCallAssumption(en.E))); builder.Add(TrAssumeCmdWithDependencies(etran, m.Tok, en.E, "overridden ensures clause")); } // conjunction of class post-conditions @@ -1488,10 +1514,11 @@ private void AddMethodOverrideEnsChk(Method m, BoogieStmtListBuilder builder, Ex .Aggregate((e0, e1) => new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, e0, e1)); //generating trait post-conditions with class variables FunctionCallSubstituter sub = null; - foreach (var en in m.OverriddenMethod.Ens) { + foreach (var en in ConjunctsOf(m.OverriddenMethod.Ens)) { sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (TopLevelDeclWithMembers)m.EnclosingClass); var subEn = sub.Substitute(en.E); foreach (var s in TrSplitExpr(new BodyTranslationContext(false), subEn, etran, false, out _).Where(s => s.IsChecked)) { + builder.Add(TrAssumeCmd(m.OverriddenMethod.Tok, etran.CanCallAssumption(subEn))); var constraint = allOverrideEns == null ? null : new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Imp, allOverrideEns, subEn); @@ -1510,17 +1537,19 @@ private void AddMethodOverrideReqsChk(Method m, BoogieStmtListBuilder builder, E //generating trait pre-conditions with class variables FunctionCallSubstituter sub = null; var subReqs = new List(); - foreach (var req in m.OverriddenMethod.Req) { + foreach (var req in ConjunctsOf(m.OverriddenMethod.Req)) { sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (TopLevelDeclWithMembers)m.EnclosingClass); var subReq = sub.Substitute(req.E); + builder.Add(TrAssumeCmd(m.OverriddenMethod.Tok, etran.CanCallAssumption(subReq))); builder.Add(TrAssumeCmdWithDependencies(etran, m.Tok, subReq, "overridden requires clause")); subReqs.Add(subReq); } var allTraitReqs = subReqs.Count == 0 ? null : subReqs .Aggregate((e0, e1) => new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, e0, e1)); //generating class pre-conditions - foreach (var req in m.Req) { + foreach (var req in ConjunctsOf(m.Req)) { foreach (var s in TrSplitExpr(new BodyTranslationContext(false), req.E, etran, false, out _).Where(s => s.IsChecked)) { + builder.Add(TrAssumeCmd(m.Tok, etran.CanCallAssumption(req.E))); var constraint = allTraitReqs == null ? null : new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Imp, allTraitReqs, req.E); @@ -1759,13 +1788,13 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { // FREE PRECONDITIONS if (kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation || kind == MethodTranslationKind.OverrideCheck) { // the other cases have no need for a free precondition // free requires mh == ModuleContextHeight && fh == FunctionContextHeight; - req.Add(Requires(m.Tok, true, null, etran.HeightContext(m), null, null, null)); + req.Add(FreeRequires(m.Tok, etran.HeightContext(m), null)); if (m is TwoStateLemma) { // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap) var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr); var a1 = HeapSucc(prevHeap, currHeap); var a2 = FunctionCall(m.Tok, BuiltinFunction.IsGoodHeap, null, currHeap); - req.Add(Requires(m.Tok, true, null, BplAnd(a0, BplAnd(a1, a2)), null, null, null)); + req.Add(FreeRequires(m.Tok, BplAnd(a0, BplAnd(a1, a2)), null)); } foreach (var typeBoundAxiom in TypeBoundAxioms(m.Tok, Concat(m.EnclosingClass.TypeArgs, m.TypeArgs))) { @@ -1798,8 +1827,10 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { // USER-DEFINED SPECIFICATIONS var comment = "user-defined preconditions"; - foreach (var p in m.Req) { + foreach (var p in ConjunctsOf(m.Req)) { var (errorMessage, successMessage) = CustomErrorMessage(p.Attributes); + req.Add(FreeRequires(p.E.Tok, etran.CanCallAssumption(p.E), comment, true)); + comment = null; if (p.Label != null && kind == MethodTranslationKind.Implementation) { // don't include this precondition here, but record it for later use p.Label.E = (m is TwoStateLemma ? ordinaryEtran : etran.Old).TrExpr(p.E); @@ -1811,14 +1842,20 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { } else if (s.IsOnlyFree && !bodyKind) { // don't include in split -- it would be ignored, anyhow } else { - req.Add( - RequiresWithDependencies(s.Tok, s.IsOnlyFree, p.E, s.E, errorMessage, successMessage, comment)); - comment = null; + req.Add(RequiresWithDependencies(s.Tok, s.IsOnlyFree, p.E, s.E, errorMessage, successMessage, null)); // the free here is not linked to the free on the original expression (this is free things generated in the splitting.) } } } } + + // assume can-call conditions for the modifies clause + comment = "user-defined frame expressions"; + foreach (var frameExpression in m.Mod.Expressions) { + req.Add(FreeRequires(frameExpression.Tok, etran.CanCallAssumption(frameExpression.E), comment, true)); + comment = null; + } + return req; } @@ -1830,9 +1867,9 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { // USER-DEFINED SPECIFICATIONS var comment = "user-defined postconditions"; - foreach (var p in m.Ens) { + foreach (var p in ConjunctsOf(m.Ens)) { var (errorMessage, successMessage) = CustomErrorMessage(p.Attributes); - AddEnsures(ens, Ensures(p.E.Tok, true, p.E, etran.CanCallAssumption(p.E), errorMessage, successMessage, comment)); + AddEnsures(ens, FreeEnsures(p.E.Tok, etran.CanCallAssumption(p.E), comment, true)); comment = null; foreach (var split in TrSplitExprForMethodSpec(new BodyTranslationContext(m.ContainsHide), p.E, etran, kind)) { var post = split.E; @@ -1863,13 +1900,11 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { // add the fuel assumption for the reveal method of a opaque method if (IsOpaqueRevealLemma(m)) { List args = Attributes.FindExpressions(m.Attributes, "revealedFunction"); - if (args == null) { - return ens; - } - - if (args[0].Resolved is MemberSelectExpr selectExpr) { - Function f = selectExpr.Member as Function; - AddEnsures(ens, Ensures(m.Tok, true, null, GetRevealConstant(f), null, null, null)); + if (args != null) { + if (args[0].Resolved is MemberSelectExpr selectExpr) { + Function f = selectExpr.Member as Function; + AddEnsures(ens, FreeEnsures(m.Tok, GetRevealConstant(f), null)); + } } } return ens; diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs b/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs index 1349ec2303d..d9ac17362d5 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs @@ -321,6 +321,7 @@ bool TrSplitExpr(BodyTranslationContext context, Expression expr, List bvars = new List(); Bpl.Expr typeAntecedent = etran.TrBoundVariables(kvars, bvars); // no need to use allocation antecedent here, because the well-founded less-than ordering assures kk are allocated diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs index d4ebf8fdf75..29c71119c50 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs @@ -643,7 +643,10 @@ private void GenerateAndCheckGuesses(IOrigin tok, List bvars, List freeOfAlloc = BoundedPool.HasBounds(bounds, BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc); var bvs = new List(); @@ -952,80 +955,108 @@ void AddTypeDecl(SubsetTypeDecl dd) { this.fuelContext = oldFuelContext; } - /** - * Example: - // _System.object: subset type $Is - axiom (forall c#0: ref :: - { $Is(c#0, Tclass._System.object()) } - $Is(c#0, Tclass._System.object()) - <==> $Is(c#0, Tclass._System.object?()) && c#0 != null); - - // _System.object: subset type $IsAlloc - axiom (forall c#0: ref, $h: Heap :: - { $IsAlloc(c#0, Tclass._System.object(), $h) } - $IsAlloc(c#0, Tclass._System.object(), $h) - <==> $IsAlloc(c#0, Tclass._System.object?(), $h)); - */ - void AddRedirectingTypeDeclAxioms(bool is_alloc, T dd, string fullName) + /// + /// Generate $Is (if "!generateIsAlloc") or $IsAlloc (if "generateIsAlloc") axioms for the newtype/subset-type "dd", + /// whose printable name is "fullName". + /// + /// Given that the type "dd" is + /// + /// (new)type dd = x: Base | constraint + /// + /// the $Is axioms have the form + /// + /// axiom (forall o: dd :: + /// { $Is(o, Tclass.dd) } + /// $Is(o, Tclass.dd) ==> + /// $Is(o, Tclass.Base) && constraintCanCall && constraint); + /// axiom (forall o: dd :: + /// { $Is(o, Tclass.dd) } + /// $Is(o, Tclass.Base) && (constraintCanCall ==> constraint) ==> + /// $Is(o, Tclass.dd)); + /// + /// and the $IsAlloc axiom has the form + /// + /// axiom (forall o: dd, $h: Heap :: + /// { $IsAlloc(o, Tclass.dd, $h) } + /// $IsAlloc(o, Tclass.dd, $h) <==> $IsAlloc(o, Tclass.Base, $h)); + /// + void AddRedirectingTypeDeclAxioms(bool generateIsAlloc, T dd, string fullName) where T : TopLevelDecl, RedirectingTypeDecl { Contract.Requires(dd != null); Contract.Requires((dd.Var != null && dd.Constraint != null) || dd is NewtypeDecl); Contract.Requires(fullName != null); - List typeArgs; - var vars = MkTyParamBinders(dd.TypeArgs, out typeArgs); - var o_ty = ClassTyCon(dd, typeArgs); + var vars = MkTyParamBinders(dd.TypeArgs, out var typeArgs); + var typeTerm = ClassTyCon(dd, typeArgs); var baseType = dd.Var != null ? dd.Var.Type : ((NewtypeDecl)(object)dd).BaseType; var oBplType = TrType(baseType); var c = new BoundVar(dd.Tok, CurrentIdGenerator.FreshId("c"), baseType); var o = BplBoundVar((dd.Var ?? c).AssignUniqueName((dd.IdGenerator)), oBplType, vars); - Bpl.Expr body, is_o; - string comment; - Trigger trigger; - - if (is_alloc) { - comment = $"$IsAlloc axiom for {dd.WhatKind} {fullName}"; + if (generateIsAlloc) { var h = BplBoundVar("$h", Predef.HeapType, vars); // $IsAlloc(o, ..) - is_o = MkIsAlloc(o, o_ty, h, ModeledAsBoxType(baseType)); - trigger = BplTrigger(is_o); + var isAlloc = MkIsAlloc(o, typeTerm, h, ModeledAsBoxType(baseType)); + Bpl.Expr body; + var trigger = BplTrigger(isAlloc); if (baseType.IsNumericBased() || baseType.IsBitVectorType || baseType.IsBoolType || baseType.IsCharType) { - body = is_o; + body = isAlloc; } else { Bpl.Expr rhs = MkIsAlloc(o, baseType, h); if (dd is NonNullTypeDecl) { trigger.Next = BplTrigger(rhs); } - body = BplIff(is_o, rhs); + body = BplIff(isAlloc, rhs); } + + var comment = $"$IsAlloc axiom for {dd.WhatKind} {fullName}"; + var axiom = new Bpl.Axiom(dd.Tok, BplForall(vars, BplTrigger(isAlloc), body), comment); + AddOtherDefinition(GetOrCreateTypeConstructor(dd), axiom); + } else { - comment = $"$Is axiom for {dd.WhatKind} {fullName}"; // $Is(o, ..) - is_o = MkIs(o, o_ty, ModeledAsBoxType(baseType)); - trigger = BplTrigger(is_o); + var isPredicate = MkIs(o, typeTerm, ModeledAsBoxType(baseType)); + var trigger = BplTrigger(isPredicate); var etran = new ExpressionTranslator(this, Predef, NewOneHeapExpr(dd.Tok), null); - Bpl.Expr parentConstraint, constraint; + Bpl.Expr parentConstraint; + Expression condition; if (baseType.IsNumericBased() || baseType.IsBitVectorType || baseType.IsBoolType || baseType.IsCharType) { // optimize this to only use the numeric/bitvector constraint, not the whole $Is thing on the base type parentConstraint = Bpl.Expr.True; var udt = UserDefinedType.FromTopLevelDecl(dd.Tok, dd); - var substitutee = Expression.CreateIdentExpr(dd.Var ?? c); - constraint = etran.TrExpr(ModuleResolver.GetImpliedTypeConstraint(substitutee, udt)); + var idExpr = Expression.CreateIdentExpr(dd.Var ?? c); + condition = ModuleResolver.GetImpliedTypeConstraint(idExpr, udt); } else { parentConstraint = MkIs(o, baseType); if (dd is NonNullTypeDecl) { trigger.Next = BplTrigger(parentConstraint); } - // conjoin the constraint - constraint = etran.TrExpr(dd.Constraint ?? Expression.CreateBoolLiteral(dd.Tok, true)); + condition = dd.Constraint ?? Expression.CreateBoolLiteral(dd.Tok, true); } - body = BplIff(is_o, BplAnd(parentConstraint, constraint)); - } - var axiom = new Bpl.Axiom(dd.Tok, BplForall(vars, trigger, body), comment); - AddOtherDefinition(GetOrCreateTypeConstructor(dd), axiom); + var constraintCanCall = etran.CanCallAssumption(condition); + if (ArrowType.IsPartialArrowTypeName(dd.Name)) { + // Hack for now. TODO: The resolver currently sets up the constraint of a partial arrow as being + // a total arrow such that "forall bx: Box :: f(bx) == {}". However, it ought to be + // "forall bx: Box :: f.requires(bx) ==> f(bx) == {}". When that gets fixed, the hack here is no longer needed. + constraintCanCall = Bpl.Expr.True; + } + var canCallIsJustTrue = constraintCanCall == Bpl.Expr.True; + var constraint = etran.TrExpr(condition); + var comment = $"$Is axiom{(canCallIsJustTrue ? "" : "s")} for {dd.WhatKind} {fullName}"; + + var rhs = BplAnd(parentConstraint, BplAnd(constraintCanCall, constraint)); + var body = canCallIsJustTrue ? BplIff(isPredicate, rhs) : BplImp(isPredicate, rhs); + var axiom = new Bpl.Axiom(dd.Tok, BplForall(vars, trigger, body), comment); + AddOtherDefinition(GetOrCreateTypeConstructor(dd), axiom); + + if (!canCallIsJustTrue) { + body = BplImp(BplAnd(parentConstraint, BplImp(constraintCanCall, constraint)), isPredicate); + axiom = new Bpl.Axiom(dd.Tok, BplForall(vars, BplTrigger(isPredicate), body), null); + AddOtherDefinition(GetOrCreateTypeConstructor(dd), axiom); + } + } } @@ -1413,8 +1444,11 @@ void CheckResultToBeInType_Aux(IOrigin tok, Expression boogieExpr, Expression or // TODO: use TrSplitExpr var typeMap = TypeParameter.SubstitutionMap(rdt.TypeArgs, udt.TypeArgs); var dafnyConstraint = Substitute(rdt.Constraint, null, new() { { rdt.Var, origExpr } }, typeMap); - var boogieConstraint = etran.TrExpr(Substitute(rdt.Constraint, null, new() { { rdt.Var, boogieExpr } }, typeMap)); - builder.Add(Assert(tok, boogieConstraint, new ConversionSatisfiesConstraints(errorMsgPrefix, kind, rdt.Name, dafnyConstraint), builder.Context)); + var boogieConstraint = Substitute(rdt.Constraint, null, new() { { rdt.Var, boogieExpr } }, typeMap); + + var canCall = etran.CanCallAssumption(boogieConstraint); + var constraint = etran.TrExpr(boogieConstraint); + builder.Add(Assert(tok, BplImp(canCall, constraint), new ConversionSatisfiesConstraints(errorMsgPrefix, kind, rdt.Name, dafnyConstraint), builder.Context)); } } @@ -1454,7 +1488,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { // the procedure itself var req = new List(); // free requires mh == ModuleContextHeight && fh == TypeContextHeight; - req.Add(Requires(decl.Tok, true, null, etran.HeightContext(decl), null, null, null)); + req.Add(FreeRequires(decl.Tok, etran.HeightContext(decl), null)); // modifies $Heap var mod = new List { etran.HeapCastToIdentifierExpr, diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 0f1c766d0e6..3c4d08f915c 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -1445,6 +1445,11 @@ public static Bpl.QKeyValue InlineAttribute(Bpl.IToken tok, Bpl.QKeyValue/*?*/ n return new QKeyValue(tok, "inline", new List(), next); } + public static Bpl.QKeyValue AlwaysAssumeAttribute(Bpl.IToken tok, Bpl.QKeyValue next = null) { + Contract.Requires(tok != null); + return new QKeyValue(tok, "always_assume", new List(), next); + } + class Specialization { public readonly List Formals; public readonly List ReplacementExprs; @@ -1559,13 +1564,16 @@ public Specialization(IVariable formal, MatchCase mc, Specialization prev, Boogi return (olderParameterCount, olderCondition); } - Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran) { + Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran, bool strict = false) { Contract.Requires(f != null); Contract.Requires(etran != null); Contract.Requires(VisibleInScope(f)); if (InVerificationScope(f)) { - return - Bpl.Expr.Le(Bpl.Expr.Literal(forModule.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight()); + if (strict) { + return Bpl.Expr.Lt(Bpl.Expr.Literal(forModule.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight()); + } else { + return Bpl.Expr.Le(Bpl.Expr.Literal(forModule.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight()); + } } else { return Bpl.Expr.True; } @@ -2092,13 +2100,16 @@ public void CheckFrameSubset(IOrigin tok, List calleeFrame, ProofObligationDescription desc, Bpl.QKeyValue kv) { CheckFrameSubset(tok, calleeFrame, receiverReplacement, substMap, etran, enclosingFrame, - (t, e, d, q) => builder.Add(Assert(t, e, d, builder.Context, q)), desc, kv); + (t, e, d, q) => builder.Add(Assert(t, e, d, builder.Context, q)), + (t, e) => builder.Add(TrAssumeCmd(t, e)), + desc, kv); } void CheckFrameSubset(IOrigin tok, List calleeFrame, Expression receiverReplacement, Dictionary substMap, ExpressionTranslator/*!*/ etran, Boogie.IdentifierExpr /*!*/ enclosingFrame, Action makeAssert, + Action makeAssume, ProofObligationDescription desc, Bpl.QKeyValue kv) { Contract.Requires(tok != null); @@ -2108,6 +2119,11 @@ void CheckFrameSubset(IOrigin tok, List calleeFrame, Contract.Requires(makeAssert != null); Contract.Requires(Predef != null); + foreach (var frameExpression in calleeFrame) { + var e = substMap != null ? Substitute(frameExpression.E, receiverReplacement, substMap) : frameExpression.E; + makeAssume(frameExpression.Tok, etran.CanCallAssumption(e)); + } + // emit: assert (forall o: ref, f: Field :: o != null && $Heap[o,alloc] && (o,f) in subFrame ==> enclosingFrame[o,f]); var oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", Predef.RefType)); var o = new Bpl.IdentifierExpr(tok, oVar); @@ -3174,7 +3190,7 @@ public Bpl.Expr CondApplyBox(Bpl.IToken tok, Bpl.Expr e, Type fromType, Type toT if (e is Bpl.NAryExpr { Fun: Bpl.TypeCoercion } coerce) { Contract.Assert(coerce.Args.Count == 1); Contract.Assert(Bpl.Type.Equals(((Bpl.TypeCoercion)coerce.Fun).Type, TrType(fromType))); - if (coerce.Args[0] is Bpl.NAryExpr { Fun: Bpl.FunctionCall { FunctionName: "$Unbox" } } call) { + if (coerce.Args[0] is Bpl.NAryExpr { Fun: Bpl.FunctionCall { FunctionName: UnboxFunctionName } } call) { Contract.Assert(call.Args.Count == 1); return call.Args[0]; } @@ -3227,7 +3243,7 @@ public Bpl.Expr BoxIfNotNormallyBoxed(Bpl.IToken tok, Bpl.Expr e, Type t) { public Bpl.Expr ApplyBox(Bpl.IToken tok, Bpl.Expr e) { Contract.Assert(tok != null); Contract.Assert(e != null); - if (e.Type == Predef.BoxType || e is NAryExpr { Fun.FunctionName: "$Box" }) { + if (e.Type == Predef.BoxType || e is NAryExpr { Fun.FunctionName: BoxFunctionName }) { return e; } return FunctionCall(tok, BuiltinFunction.Box, null, e); @@ -3236,7 +3252,6 @@ public Bpl.Expr ApplyBox(Bpl.IToken tok, Bpl.Expr e) { /// /// If the expression is boxed, but the type is not boxed, this unboxes it. /// For lambda functions. - /// KRML: The name of this method is really confusing. It seems it should be named something like UnboxUnlessInherentlyBoxed. /// public Bpl.Expr UnboxUnlessInherentlyBoxed(Bpl.Expr e, Type t) { if (!ModeledAsBoxType(t)) { @@ -3285,6 +3300,17 @@ public static bool ModeledAsBoxType(Type t) { return res; } + /// + /// This method returns "expr" are stripping off any type coercions and box/unbox functions. + /// + public static Boogie.Expr StripBoxAdjustments(Boogie.Expr expr) { + while (expr is Boogie.NAryExpr { Fun: Boogie.FunctionCall { FunctionName: BoxFunctionName or UnboxFunctionName } or Boogie.TypeCoercion } nAryExpr) { + Contract.Assert(nAryExpr.Args.Count == 1); + expr = nAryExpr.Args[0]; + } + return expr; + } + // ----- Statement ---------------------------------------------------------------------------- /// @@ -3372,14 +3398,19 @@ Bpl.Ensures EnsuresWithDependencies(IOrigin tok, bool free, Expression dafnyCond proofDependencies?.AddProofDependencyId(ens, tok, new EnsuresDependency(tok, dafnyCondition)); return ens; } + Bpl.Ensures FreeEnsures(IOrigin tok, Bpl.Expr condition, string comment, bool alwaysAssume = false) { + var kv = alwaysAssume ? AlwaysAssumeAttribute(tok) : null; + return Ensures(tok, true, null, condition, null, null, comment, kv); + } + - Bpl.Ensures Ensures(IOrigin tok, bool free, Expression dafnyCondition, Bpl.Expr condition, string errorMessage, string successMessage, string comment) { + Bpl.Ensures Ensures(IOrigin tok, bool free, Expression dafnyCondition, Bpl.Expr condition, string errorMessage, string successMessage, string comment, QKeyValue kv = null) { Contract.Requires(tok != null); Contract.Requires(condition != null); Contract.Ensures(Contract.Result() != null); var unwrappedToken = ForceCheckOrigin.Unwrap(tok); - Bpl.Ensures ens = new Bpl.Ensures(unwrappedToken, free, condition, comment); + Bpl.Ensures ens = new Bpl.Ensures(unwrappedToken, free, condition, comment, kv); var description = new EnsuresDescription(dafnyCondition, errorMessage, successMessage); ens.Description = description; if (!free) { @@ -3397,12 +3428,16 @@ Bpl.Requires RequiresWithDependencies(IOrigin tok, bool free, Expression dafnyCo proofDependencies?.AddProofDependencyId(req, tok, new RequiresDependency(tok, dafnyCondition)); return req; } + Bpl.Requires FreeRequires(IOrigin tok, Bpl.Expr bCondition, string comment, bool alwaysAssume = false) { + var kv = alwaysAssume ? AlwaysAssumeAttribute(tok) : null; + return Requires(tok, true, null, bCondition, null, null, comment, kv); + } - Bpl.Requires Requires(IOrigin tok, bool free, Expression dafnyCondition, Bpl.Expr bCondition, string errorMessage, string successMessage, string comment) { + Bpl.Requires Requires(IOrigin tok, bool free, Expression dafnyCondition, Bpl.Expr bCondition, string errorMessage, string successMessage, string comment, QKeyValue kv = null) { Contract.Requires(tok != null); Contract.Requires(bCondition != null); Contract.Ensures(Contract.Result() != null); - Bpl.Requires req = new Bpl.Requires(ForceCheckOrigin.Unwrap(tok), free, bCondition, comment); + Bpl.Requires req = new Bpl.Requires(ForceCheckOrigin.Unwrap(tok), free, bCondition, comment, kv); req.Description = new RequiresDescription(dafnyCondition, errorMessage, successMessage); return req; } @@ -4469,6 +4504,22 @@ public static bool DetermineDisableNonLinearArithmetic(ModuleDefinition module, return dafnyOptions.DisableNLarith; } + /// + /// Return the conjuncts of "attributedExpressions". + /// + public static IEnumerable ConjunctsOf(List attributedExpressions) { + foreach (var attrExpr in attributedExpressions) { + if (attrExpr.Label != null) { + // don't mess with labeled expressions + yield return attrExpr; + } else { + foreach (var conjunct in Expression.ConjunctsWithLetsOnOutside(attrExpr.E)) { + yield return new AttributedExpression(conjunct, attrExpr.Attributes); + } + } + } + } + List /*!*/ TrSplitExpr(BodyTranslationContext context, Expression expr, ExpressionTranslator etran, bool applyInduction, out bool splitHappened) { Contract.Requires(expr != null); @@ -4499,11 +4550,13 @@ Bpl.Trigger TrTrigger(ExpressionTranslator etran, Attributes attribs, IOrigin to foreach (var trigger in attribs.AsEnumerable().Where(aa => aa.Name == "trigger").Select(aa => aa.Args)) { List tt = new List(); foreach (var arg in trigger) { + Bpl.Expr term; if (substMap == null) { - tt.Add(argsEtran.TrExpr(arg)); + term = argsEtran.TrExpr(arg); } else { - tt.Add(argsEtran.TrExpr(Substitute(arg, null, substMap))); + term = argsEtran.TrExpr(Substitute(arg, null, substMap)); } + tt.Add(StripBoxAdjustments(term)); } tr = new Bpl.Trigger(tok, true, tt, tr); } @@ -4538,11 +4591,13 @@ Bpl.Trigger TrTrigger(ExpressionTranslator etran, Attributes attribs, IOrigin to foreach (var trigger in attribs.AsEnumerable().Where(aa => aa.Name == "trigger")) { List tt = new List(); foreach (var arg in trigger.Args) { + Bpl.Expr term; if (substMap == null) { - tt.Add(argsEtran.TrExpr(arg)); + term = argsEtran.TrExpr(arg); } else { - tt.Add(argsEtran.TrExpr(Substitute(arg, null, substMap, typeMap))); + term = argsEtran.TrExpr(Substitute(arg, null, substMap, typeMap)); } + tt.Add(StripBoxAdjustments(term)); } if (useHeapAsQuantifier) { tt.Add(FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, argsEtran.HeapExpr)); diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs index a580ce21671..a9a21921f4d 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs @@ -74,7 +74,8 @@ private void TrForallStmt(BoogieStmtListBuilder builder, Variables locals, Expre void TrForallStmtCall(IOrigin tok, List boundVars, List bounds, Expression range, ExpressionConverter additionalRange, List forallExpressions, List> triggers, CallStmt s0, - BoogieStmtListBuilder definedness, BoogieStmtListBuilder exporter, Variables locals, ExpressionTranslator etran) { + BoogieStmtListBuilder definedness, BoogieStmtListBuilder exporter, Variables locals, ExpressionTranslator etran, + bool includeCanCalls = true) { Contract.Requires(tok != null); Contract.Requires(boundVars != null); Contract.Requires(bounds != null); @@ -168,7 +169,7 @@ void TrForallStmtCall(IOrigin tok, List boundVars, List b var argsSubstMap = new Dictionary(); // maps formal arguments to actuals Contract.Assert(s0.Method.Ins.Count == s0.Args.Count); var callEtran = new ExpressionTranslator(this, Predef, etran.HeapExpr, initHeap, etran.scope); - Bpl.Expr ante; + Bpl.Expr anteCanCalls, ante; Bpl.Expr post = Bpl.Expr.True; Bpl.Trigger tr; if (forallExpressions != null) { @@ -182,18 +183,23 @@ void TrForallStmtCall(IOrigin tok, List boundVars, List b tr = TrTrigger(callEtran, expr.Attributes, expr.Tok, bvars, substMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents()); var p = Substitute(expr.Range, null, substMap); + anteCanCalls = initEtran.CanCallAssumption(p); ante = BplAnd(ante, initEtran.TrExpr(p)); if (additionalRange != null) { ante = BplAnd(ante, additionalRange(substMap, initEtran)); } - tr = TrTrigger(callEtran, expr.Attributes, expr.Tok, bvars, substMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents()); - post = callEtran.TrExpr(Substitute(expr.Term, null, substMap)); + p = Substitute(expr.Term, null, substMap); + post = BplAnd(post, callEtran.CanCallAssumption(p)); + post = BplAnd(post, callEtran.TrExpr(p)); + } else { ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap); var p = Substitute(range, null, substMap); + anteCanCalls = initEtran.CanCallAssumption(p); ante = BplAnd(ante, initEtran.TrExpr(p)); if (additionalRange != null) { + // additionalRange produces something of the form canCallAssumptions ==> TrExpr ante = BplAnd(ante, additionalRange(substMap, initEtran)); } @@ -202,8 +208,11 @@ void TrForallStmtCall(IOrigin tok, List boundVars, List b var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents()); // substitute the renamed bound variables for the declared ones argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type)); } - foreach (var ens in s0.Method.Ens) { + foreach (var ens in ConjunctsOf(s0.Method.Ens)) { p = Substitute(ens.E, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents()); // substitute the call's actuals for the method's formals + if (includeCanCalls) { + post = BplAnd(post, callEtran.CanCallAssumption(p)); + } post = BplAnd(post, callEtran.TrExpr(p)); } @@ -223,7 +232,11 @@ void TrForallStmtCall(IOrigin tok, List boundVars, List b // TRIG (forall $ih#s0#0: Seq :: $Is($ih#s0#0, TSeq(TChar)) && $IsAlloc($ih#s0#0, TSeq(TChar), $initHeapForallStmt#0) && Seq#Length($ih#s0#0) != 0 && Seq#Rank($ih#s0#0) < Seq#Rank(s#0) ==> (forall i#2: int :: true ==> LitInt(0) <= i#2 && i#2 < Seq#Length($ih#s0#0) ==> char#ToInt(_module.CharChar.MinChar($LS($LZ), $Heap, this, $ih#s0#0)) <= char#ToInt($Unbox(Seq#Index($ih#s0#0, i#2)): char))) // TRIG (forall $ih#pat0#0: Seq, $ih#a0#0: Seq :: $Is($ih#pat0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#pat0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && $Is($ih#a0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#a0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && Seq#Length($ih#pat0#0) <= Seq#Length($ih#a0#0) && Seq#SameUntil($ih#pat0#0, $ih#a0#0, Seq#Length($ih#pat0#0)) && (Seq#Rank($ih#pat0#0) < Seq#Rank(pat#0) || (Seq#Rank($ih#pat0#0) == Seq#Rank(pat#0) && Seq#Rank($ih#a0#0) < Seq#Rank(a#0))) ==> _module.__default.IsRelaxedPrefixAux(_module._default.Same0$T, $LS($LZ), $Heap, $ih#pat0#0, $ih#a0#0, LitInt(1)))' // TRIG (forall $ih#m0#0: DatatypeType, $ih#n0#0: DatatypeType :: $Is($ih#m0#0, Tclass._module.Nat()) && $IsAlloc($ih#m0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && $Is($ih#n0#0, Tclass._module.Nat()) && $IsAlloc($ih#n0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && Lit(true) && (DtRank($ih#m0#0) < DtRank(m#0) || (DtRank($ih#m0#0) == DtRank(m#0) && DtRank($ih#n0#0) < DtRank(n#0))) ==> _module.__default.mult($LS($LZ), $Heap, $ih#m0#0, _module.__default.plus($LS($LZ), $Heap, $ih#n0#0, $ih#n0#0)) == _module.__default.mult($LS($LZ), $Heap, _module.__default.plus($LS($LZ), $Heap, $ih#m0#0, $ih#m0#0), $ih#n0#0)) - var qq = new Bpl.ForallExpr(tok, bvars, tr, BplImp(ante, post)); // TODO: Add a SMART_TRIGGER here. If we can't find one, abort the attempt to do induction automatically + var body = BplImp(ante, post); + if (includeCanCalls) { + body = BplAnd(anteCanCalls, body); + } + var qq = new Bpl.ForallExpr(tok, bvars, tr, body); exporter.Add(TrAssumeCmd(tok, qq)); } } @@ -421,8 +434,9 @@ void TrForallAssign(ForallStmt s, SingleAssignStmt s0, /// /// Generate: - /// assume (forall x,y :: Range(x,y)[$Heap:=oldHeap] ==> - /// $Heap[ Object(x,y)[$Heap:=oldHeap], Field(x,y)[$Heap:=oldHeap] ] == G[$Heap:=oldHeap] )); + /// assume (forall x,y :: Range#canCall AND + /// (Range(x,y)[$Heap:=oldHeap] ==> + /// $Heap[ Object(x,y)[$Heap:=oldHeap], Field(x,y)[$Heap:=oldHeap] ] == G[$Heap:=oldHeap]))); /// where /// x,y represent boundVars /// Object(x,y) is the first part of lhs @@ -465,7 +479,12 @@ private Bpl.Expr TrForall_NewValueAssumption(IOrigin tok, List boundVa tr = new Bpl.Trigger(tok, true, tt, tr); } } - return new Bpl.ForallExpr(tok, xBvars, tr, BplImp(xAnte, Bpl.Expr.Eq(xHeapOF, g))); + var canCalls = BplAnd(prevEtran.CanCallAssumption(lhs), prevEtran.CanCallAssumption(rhs)); + var canCallRange = prevEtran.CanCallAssumption(range); + var body = BplAnd(canCalls, Bpl.Expr.Eq(xHeapOF, g)); + body = BplImp(xAnte, body); + body = BplAnd(canCallRange, body); + return new Bpl.ForallExpr(tok, xBvars, tr, body); } IEnumerable TransitiveSubstatements(Statement s) { @@ -517,7 +536,7 @@ void TrForallProof(ForallStmt forallStmt, BoogieStmtListBuilder definedness, Boo definedness.Add(TrAssumeCmdWithDependencies(etran, forallStmt.Range.Tok, forallStmt.Range, "forall statement range")); var ensuresDefinedness = new BoogieStmtListBuilder(this, options, definedness.Context); - foreach (var ens in forallStmt.Ens) { + foreach (var ens in ConjunctsOf(forallStmt.Ens)) { TrStmt_CheckWellformed(ens.E, ensuresDefinedness, locals, etran, false); ensuresDefinedness.Add(TrAssumeCmdWithDependencies(etran, ens.E.Tok, ens.E, "forall statement ensures clause")); } @@ -527,7 +546,9 @@ void TrForallProof(ForallStmt forallStmt, BoogieStmtListBuilder definedness, Boo TrStmt(forallStmt.Body, definedness, locals, etran); // check that postconditions hold - foreach (var ens in forallStmt.Ens) { + foreach (var ens in ConjunctsOf(forallStmt.Ens)) { + definedness.Add(TrAssumeCmd(ens.E.Tok, etran.CanCallAssumption(ens.E))); + foreach (var split in TrSplitExpr(definedness.Context, ens.E, etran, true, out var splitHappened)) { if (split.IsChecked) { definedness.Add(Assert(split.Tok, split.E, new ForallPostcondition(ens.E), definedness.Context)); @@ -544,6 +565,7 @@ void TrForallProof(ForallStmt forallStmt, BoogieStmtListBuilder definedness, Boo var se = forallStmt.Body == null ? Bpl.Expr.True : TrFunctionSideEffect(forallStmt.Body, etran); var substMap = new Dictionary(); var p = Substitute(forallStmt.EffectiveEnsuresClauses[0], null, substMap); + exporter.Add(TrAssumeCmd(forallStmt.Tok, etran.CanCallAssumption(p))); var qq = etran.TrExpr(p); if (forallStmt.BoundVars.Count != 0) { exporter.Add(TrAssumeCmd(forallStmt.Tok, BplAnd(se, qq))); diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrLoop.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrLoop.cs index 5834131aba6..90471ae557e 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrLoop.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrLoop.cs @@ -238,6 +238,7 @@ void TrLoop(LoopStmt loop, Expression Guard, BodyTranslator/*?*/ bodyTr, TrStmt_CheckWellformed(loopInv.E, invDefinednessBuilder, locals, etran, false); invDefinednessBuilder.Add(TrAssumeCmdWithDependencies(etran, loopInv.E.Tok, loopInv.E, "loop invariant")); + builder.Add(TrAssumeCmd(loopInv.E.Tok, BplImp(w, etran.CanCallAssumption(loopInv.E)))); invariants.Add(TrAssumeCmd(loopInv.E.Tok, BplImp(w, etran.CanCallAssumption(loopInv.E)))); var ss = TrSplitExpr(builder.Context, loopInv.E, etran, false, out var splitHappened); if (!splitHappened) { @@ -258,6 +259,7 @@ void TrLoop(LoopStmt loop, Expression Guard, BodyTranslator/*?*/ bodyTr, } // check definedness of decreases clause foreach (Expression e in theDecreases) { + builder.Add(TrAssumeCmd(e.Tok, Bpl.Expr.Imp(w, etran.CanCallAssumption(e)))); TrStmt_CheckWellformed(e, invDefinednessBuilder, locals, etran, true); } if (codeContext is IMethodCodeContext) { @@ -349,6 +351,9 @@ void TrLoop(LoopStmt loop, Expression Guard, BodyTranslator/*?*/ bodyTr, // omit termination checking for this loop bodyTr(loopBodyBuilder, updatedFrameEtran); } else { + foreach (Expression e in theDecreases) { + loopBodyBuilder.Add(TrAssumeCmd(e.Tok, BplImp(w, etran.CanCallAssumption(e)))); + } List oldBfs = RecordDecreasesValue(theDecreases, loopBodyBuilder, locals, etran, "$decr$" + suffix); // time for the actual loop body bodyTr(loopBodyBuilder, updatedFrameEtran); @@ -367,6 +372,8 @@ void TrLoop(LoopStmt loop, Expression Guard, BodyTranslator/*?*/ bodyTr, prevGhostLocals.AddRange(prevVars); initDecrsDafny.Add(eInit); decrs.Add(etran.TrExpr(e)); + // need to add can calls again because the actual loop body updates the variables + loopBodyBuilder.Add(TrAssumeCmd(e.Tok, BplImp(w, etran.CanCallAssumption(e)))); } if (includeTerminationCheck) { AddComment(loopBodyBuilder, loop, "loop termination check"); diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs index eec7f7b59a7..3657c39f89f 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs @@ -526,6 +526,7 @@ private void TrCalcStmt(CalcStmt stmt, BoogieStmtListBuilder builder, Variables assert line op line; assume false; } + assume CanCallAssumptions for line<0> and line; assume line<0> op line; */ Contract.Assert(stmt.Steps.Count == stmt.Hints.Count); // established by the resolver @@ -597,6 +598,7 @@ private void TrCalcStmt(CalcStmt stmt, BoogieStmtListBuilder builder, Variables builder.Add(ifCmd); // assume result: if (stmt.Steps.Count > 1) { + builder.Add(TrAssumeCmd(stmt.Tok, etran.CanCallAssumption(stmt.Result))); builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Result, "calc statement result")); } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass4.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass4.dfy index cc8ce7abcff..61a5804b897 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass4.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass4.dfy @@ -3,7 +3,9 @@ class Ref { var inner: Ref - constructor() + constructor() { + inner := this; + } } function myf(o: Ref): () @@ -14,7 +16,6 @@ function myf(o: Ref): () } method M() - ensures false { var outer := new Ref(); @@ -23,12 +24,14 @@ method M() var inner1 := new Ref(); outer.inner := inner1; - var reads1 := myh.reads(outer); - assert reads1 == {inner1}; // Error: assertion might not hold + var reads1 := myg.reads(outer); + var reads2 := myh.reads(outer); + assert reads1 == reads2; + assert reads2 == {inner1}; // Error: assertion might not hold + assert false; // we don't know what the reads clause is, because the precondition of myf does not hold. } method M2() - ensures false { var outer := new Ref(); @@ -39,4 +42,5 @@ method M2() outer.inner := inner2; var reads2 := myh.reads(outer); assert reads2 == {inner2}; // Error: assertion might not hold + assert false; // we don't know what the reads clause is, because the precondition of myf does not hold. } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass4.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass4.dfy.expect index 676b23d73cf..b44a826c790 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass4.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass4.dfy.expect @@ -1,4 +1,6 @@ -ReadPreconditionBypass4.dfy(27,16): Error: assertion might not hold -ReadPreconditionBypass4.dfy(41,16): Error: assertion might not hold +ReadPreconditionBypass4.dfy(30,16): Error: assertion might not hold +ReadPreconditionBypass4.dfy(31,9): Error: assertion might not hold +ReadPreconditionBypass4.dfy(44,16): Error: assertion might not hold +ReadPreconditionBypass4.dfy(45,9): Error: assertion might not hold -Dafny program verifier finished with 1 verified, 2 errors +Dafny program verifier finished with 2 verified, 4 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/blogposts/TestGenerationNoInliningEnumerativeDefinitions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/blogposts/TestGenerationNoInliningEnumerativeDefinitions.dfy index b97f6ac832b..c172dac73c7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/blogposts/TestGenerationNoInliningEnumerativeDefinitions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/blogposts/TestGenerationNoInliningEnumerativeDefinitions.dfy @@ -1,20 +1,20 @@ // Generating and Running Block-Based Tests: // RUN: %baredafny generate-tests %args Block %S/TestGenerationNoInliningEnumerativeDefinitions.dfy > %t-tests.dfy -// RUN: %baredafny test %args --target:cs "%t-tests.dfy" >> "%t" +// RUN: %baredafny test %args --target:cs "%t-tests.dfy" > "%t" // Generating and Running Path-Based Tests: // RUN: %baredafny generate-tests %args Path %S/TestGenerationNoInliningEnumerativeDefinitions.dfy > %t-tests.dfy // RUN: %baredafny test %args --target:cs "%t-tests.dfy" >> "%t" // RUN: %OutputCheck --file-to-check "%t" "%s" -// CHECK: .*Dafny program verifier finished with 2 verified, 0 errors* -// CHECK: .*Evaluating the position: checked=no, checkmate=no* -// CHECK: .*Evaluating the position: checked=yes, checkmate=yes* -// CHECK: .*Dafny program verifier finished with 3 verified, 0 errors* -// CHECK: .*Evaluating the position: checked=yes, checkmate=yes* -// CHECK: .*Evaluating the position: checked=yes, checkmate=no* -// CHECK: .*Evaluating the position: checked=no, checkmate=no* +// CHECK: .*Dafny program verifier finished with 2 verified, 0 errors.* +// CHECK: .*Evaluating the position: checked=no, checkmate=no.* +// CHECK: .*Evaluating the position: checked=yes, checkmate=yes.* +// CHECK: .*Dafny program verifier finished with 3 verified, 0 errors.* +// CHECK: .*Evaluating the position: checked=yes, checkmate=yes.* +// CHECK: .*Evaluating the position: checked=yes, checkmate=no.* +// CHECK: .*Evaluating the position: checked=no, checkmate=no.* include "Inputs/TestGenerationShared.dfy" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/06-ThreadOwnership.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/06-ThreadOwnership.dfy index c5146ec389b..6137755bf13 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/06-ThreadOwnership.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/06-ThreadOwnership.dfy @@ -75,7 +75,7 @@ trait Object { // This should really be a constant, but I don't know how to do that while factoring out join below, // because traits can't have constructors. const universe: Universe - + // Base invariant: we're in the universe, and the universe satisfies its base. ghost predicate baseInv() reads * { this in universe.content && universe.globalBaseInv() } @@ -114,7 +114,7 @@ trait Object { ghost predicate inv() ensures inv() ==> localInv() reads * twostate predicate inv2() ensures inv2() ==> localInv2() reads * twostate lemma admissibility(running: Thread) requires goodPreAndLegalChanges(running) ensures inv2() && inv() - + // To prevent a class from extending both OwnedObject and NonOwnedObject ghost predicate instanceOfOwnedObject() } @@ -243,7 +243,7 @@ class EmptyType extends OwnedObject { twostate predicate userFieldsUnchanged() reads * { true } - + ghost predicate baseUserInv() reads * { && true } @@ -322,7 +322,7 @@ class AtomicCounter extends OwnedObject { //modifies running ensures objectGlobalInv() && universe.globalInv2() // The following might not always be needed - ensures this.universe == universe && this.owner == running && this.value == initialValue && this.closed == false + ensures this.universe == universe && this.owner == running && this.value == initialValue && this.closed == false //ensures running.ownedObjects == old(running.ownedObjects) + { this } ensures universe.content == old(universe.content) + { this } { @@ -359,7 +359,7 @@ class DoubleReadMethod extends OwnedObject { && old(initial_value) == initial_value && old(final_value) == final_value } - + ghost predicate baseUserInv() reads * { && counter in universe.content && counter.universe == universe } @@ -412,7 +412,7 @@ class DoubleReadMethod extends OwnedObject { universe.lci(running); } - method Run(ghost running: Thread) + method {:resource_limit "1e9"} Run(ghost running: Thread) requires this.objectGlobalInv() && running.universe == universe && running.inv() requires programCounter == 0 && closed && this.owner == running // Special requirements of Run modifies universe, universe.content, this diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy index 0b931ef0ae4..6a534428f33 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy @@ -886,7 +886,7 @@ class MutexGuardU32 extends OwnedObject { } // MutexGuardU32 - constructor {:isolate_assertions} (ghost universe: Universe, ghost running: Thread, ghost scope: Lifetime, mutex: Mutex, ghost mutexScope: Lifetime) + constructor {:isolate_assertions} {:resource_limit "1e9"} (ghost universe: Universe, ghost running: Thread, ghost scope: Lifetime, mutex: Mutex, ghost mutexScope: Lifetime) requires universe.globalInv() && { running, scope, mutex, mutexScope } <= universe.content requires scope.owner == running && mutexScope.owner == running && scope != mutexScope requires universe.outlives(mutex.lifetime, mutexScope) && universe.outlives(mutexScope, scope) && scope.unused() @@ -921,32 +921,52 @@ class MutexGuardU32 extends OwnedObject { this.mutex := mutex; this.data := mutex.data; new; - join(); + hide *; + join() by { + assert baseFieldsInv() by { + reveal baseFieldsInv(); + assert objectFields() <= universe.content by { + reveal objectFields(); + assert objectUserFields() <= universe.content by { + reveal *; + } + } + } + } lifetime.elements := lifetime.elements + { this }; // Acquire the lock this.mutex.locked := true; this.mutex.guards := { this }; // Transfer ownership of `this.mutex.data` from `this.mutex` to `this`. - this.mutex.data.owner := this; + this.mutex.data.owner := this by { + reveal *; + } this.mutex.data.nonvolatileVersion := Bump(this.mutex.data.nonvolatileVersion); // We don't need to bump this.mutex.nonvolatileVersion, because it uses volatileOwns. - universe.FrameOutlives@lci_l2(); - assert universe.outlives(mutex.lifetime, mutexScope) && universe.outlives(mutexScope, this.lifetime); // needed - assert universe.outlives(mutex.lifetime, this.lifetime); // needed - assert lifetime.alive(); // helps dafny - assert mutex.owner != null; // helps dafny - assert this.localUserInv(); - assert this.userInv(); - assert this.inv(); - assert this.mutex.inv(); - assert this.mutex.data.inv(); - universe.lci@lci_l2(running); - assert {:split_here} true; + universe.FrameOutlives@lci_l2() by { + reveal *; + } + + universe.lci@lci_l2(running) by { + reveal *; + assert universe.outlives(mutex.lifetime, mutexScope) && universe.outlives(mutexScope, this.lifetime); // needed + assert universe.outlives(mutex.lifetime, this.lifetime); // needed + assert lifetime.alive(); // helps dafny + assert mutex.owner != null; // helps dafny + assert this.localUserInv(); + assert this.userInv(); + assert this.inv(); + assert this.mutex.inv(); + assert this.mutex.data.inv(); + } label lci_l3: scope.owner := null; universe.FrameOutlives@lci_l3(); - universe.lci@lci_l3(running); - assert {:split_here} true; + universe.lci@lci_l3(running) by { + reveal *; + } + + reveal *; } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect index 79537616855..7271da1866c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 434 verified, 0 errors +Dafny program verifier finished with 385 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoContracts.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoContracts.dfy.expect index d046a3ece47..5a6a5301c17 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoContracts.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoContracts.dfy.expect @@ -573,12 +573,12 @@ module N2 refines N1 { */ } AutoContracts.dfy(17,4): Error: a postcondition could not be proved on this return path -AutoContracts.dfy(12,20): Related location: this proposition could not be proved AutoContracts.dfy(17,4): Error: a postcondition could not be proved on this return path AutoContracts.dfy(12,20): Related location: this proposition could not be proved AutoContracts.dfy(17,4): Error: a postcondition could not be proved on this return path AutoContracts.dfy(12,20): Related location: this proposition could not be proved AutoContracts.dfy(17,4): Error: a postcondition could not be proved on this return path +AutoContracts.dfy(12,20): Related location: this proposition could not be proved AutoContracts.dfy(17,4): Error: a postcondition could not be proved on this return path AutoContracts.dfy(12,20): Related location: this proposition could not be proved AutoContracts.dfy(5,25): Related location: this proposition could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CanCall.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CanCall.dfy new file mode 100644 index 00000000000..41f3de002d5 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CanCall.dfy @@ -0,0 +1,96 @@ +// RUN: %testDafnyForEachResolver "%s" + + +module ModifiesCallee { + ghost function Wrap(S: set): set { + S + } + + method DoWrapped(S: set) + modifies Wrap(S) + { + DoOne(S); + } + + method DoOne(S: set) + modifies S + { + } +} + +module ModifiesCaller { + ghost function Wrap(S: set): set { + S + } + + method DoWrapped(S: set) + modifies Wrap(S) + { + } + + method DoOne(S: set) + modifies S + { + DoWrapped(S); + } +} + +module ArraySeqInit { + function F(a: int): int { + 45 + } + + method TestArrayF() { + var m := new int[3](F); + assert m[0] == 45; + } + + method TestArrayLambda() { + var m := new int[3](_ => 45); + assert m[0] == 45; + } + + method TestSeqF() { + var m := seq(3, F); + assert m[0] == 45; + } + + method TestSeqLambda() { + var m := seq(3, _ => 45); + assert m[0] == 45; + } + +} + +module QuantifierBeforeOtherConjunct { + datatype List = Nil | Cons(head: T, tail: List) + + function Length(list: List): nat { + match list + case Nil => 0 + case Cons(_, tl) => 1 + Length(tl) + } + + function Occurrences(x: int, list: List): nat + { + match list + case Nil => 0 + case Cons(y, tl) => (if x == y then 1 else 0) + Occurrences(x, tl) + } + + function Partition(x: int, l: List): (result: (List, List)) + ensures + && (forall y :: Occurrences(y, result.0) == if y <= x then Occurrences(y, l) else 0) + && Length(l) == Length(result.0) + Length(result.1) + + lemma CallPartition(x: int, l: List) returns (aaa: List, bbb: List) + requires l.Cons? && l.head <= x + ensures + && (forall y :: Occurrences(y, aaa) == if y <= x then Occurrences(y, l) else 0) + && Length(l) == Length(aaa) + Length(bbb) + { + var (lo, hi) := Partition(x, l.tail); + aaa := Cons(l.head, lo); + bbb := hi; + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CanCall.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CanCall.dfy.expect new file mode 100644 index 00000000000..ccc01c35f48 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CanCall.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 11 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect index 1c87811a450..1e4f86d4af0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect @@ -31,5 +31,5 @@ CoinductiveProofs.dfy(208,21): Related location: this is the postcondition that CoinductiveProofs.dfy(4,23): Related location: this proposition could not be proved Dafny program verifier finished with 23 verified, 12 errors -Total resources used is 777634 -Max resources used by VC is 66829 +Total resources used is 746289 +Max resources used by VC is 59810 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Datatypes.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Datatypes.dfy index 6d3f2849253..eed09adb30c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Datatypes.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Datatypes.dfy @@ -399,7 +399,7 @@ module Exhaustiveness { } else if c == B { } else if c == C { } else { - assert false; // used to fails :(, but now works :) + assert false; // used to fail :(, but now works :) } } @@ -418,7 +418,7 @@ module Exhaustiveness { { var c := s[i]; if c != A && c != B && c != C { - assert false; // used to fails :(, but now works :) + assert false; // used to fail :(, but now works :) } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy index aef6047d1ea..91e3ea6426e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy @@ -9,8 +9,8 @@ module TestModule1 { } method test(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert pos(z) == 0; assert pos(-1) == 0; @@ -46,8 +46,8 @@ module TestModule2 { } method test(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert pos1(z) == 0; assert pos1(-1) == 0; @@ -58,21 +58,21 @@ module TestModule2 { assert pos2(-1) == 0; assert pos2(y) == 3 + pos2(y - 3); assert pos2(y) == 4 + pos2(y - 4); - - if (*) { + } + method test3(y: int) requires y > 5 { + if * { assert pos3(y) == 5 + pos3(y - 5); // Just enough fuel to get here } else { assert pos3(y) == 6 + pos3(y - 6); // error: Should fail even with a boost, since boost is too small } - - if (*) { + } + method test4(y: int, z: int) requires y > 5 requires z < 0 { + if * { assert pos4(z) == 0; // error: Fuel shouldn't overcome opaque } else { reveal pos4(); assert pos4(y) == 5 + pos4(y - 5); // With reveal, everything should work as above } - - } } @@ -86,8 +86,8 @@ module TestModule3 { } method test(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert pos(z) == 0; // error: Opaque setting hides body assert pos(-1) == 0; // error: Lits also obey opaque now @@ -105,8 +105,8 @@ module TestModule4 { // Should pass method {:fuel pos,3} test1(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert pos(z) == 0; assert pos(-1) == 0; @@ -114,8 +114,8 @@ module TestModule4 { } method {:fuel pos,0,0} test2(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert pos(z) == 0; // error: Should fail due to "opaque" fuel setting assert pos(-1) == 0; // error: Should fail due to "opaque" fuel setting. Even Lits obey opaque @@ -123,12 +123,12 @@ module TestModule4 { } method test3(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert {:fuel pos,0,0} pos(z) == 0; // error: fuel can't be decreased assert pos(-1) == 0; - if (*) { + if * { assert pos(y) == 3 + pos(y - 3); // error: Should fail without extra fuel setting assert pos(y) == 6 + pos(y - 6); // error: Should fail even with previous assert turned into assume } else { @@ -138,16 +138,16 @@ module TestModule4 { } method test4(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { forall t:int {:fuel pos,3} | t > 0 - ensures true; + ensures true { assert pos(y) == 3 + pos(y - 3); // Expected to pass, due to local fuel boost } - if (*) { + if * { calc {:fuel pos,3} { pos(y); 3 + pos(y - 3); @@ -172,8 +172,8 @@ module TestModule5 { } method test(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert pos(z) == 0; assert pos(-1) == 0; @@ -182,8 +182,8 @@ module TestModule5 { } method test(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert TestModule5aiA.pos(z) == 0; assert TestModule5aiA.pos(-1) == 0; @@ -192,8 +192,8 @@ module TestModule5 { } method test(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert TestModule5ai.TestModule5aiA.pos(z) == 0; assert TestModule5ai.TestModule5aiA.pos(-1) == 0; @@ -211,8 +211,8 @@ module TestModule5 { } method test(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert pos(z) == 0; assert pos(-1) == 0; @@ -232,15 +232,15 @@ module TestModule6 { } ghost function neg(x:int) : int - decreases 1 - x; + decreases 1 - x { if x > 0 then 0 else 1 + neg(x + 1) } method test1(y:int, z:int) - requires y > 5; - requires z < 5; + requires y > 5 + requires z < 5 { assert pos(y) == 3 + pos(y - 3); // error: Should fail, due to lack of fuel @@ -248,8 +248,8 @@ module TestModule6 { } method {:fuel pos,3} {:fuel neg,4} test2(y:int, z:int) - requires y > 5; - requires z < -5; + requires y > 5 + requires z < -5 { assert pos(y) == 3 + pos(y - 3); @@ -266,23 +266,23 @@ module TestModule7 { } ghost function {:fuel 0,0} neg(x:int) : int - decreases 1 - x; + decreases 1 - x { if x > 0 then 0 else 1 + neg(x + 1) } method {:fuel neg,4} {:fuel pos,0,0} test1(y:int, z:int) - requires y > 5; - requires z < -5; + requires y > 5 + requires z < -5 { - if (*) { + if * { assert pos(y) == 3 + pos(y - 3); // error: Method fuel should override function fuel, so this should fail assert neg(z) == 3 + neg(z + 3); // Method fuel should override function fuel, so this succeeds } forall t:int {:fuel pos,3} | t > 0 - ensures true; + ensures true { assert pos(y) == 3 + pos(y - 3); // Statement fuel should override method fuel, so this should succeed } @@ -321,15 +321,15 @@ module TestModule8 { function CRequest_grammar() : G { GTaggedUnion([ GTuple([EndPoint_grammar(), GUint64, CAppMessage_grammar()]), GUint64]) } function parse_EndPoint(val:V) : EndPoint - requires ValInGrammar(val, EndPoint_grammar()); + requires ValInGrammar(val, EndPoint_grammar()) type CAppMessage function CAppMessage_grammar() : G { GTaggedUnion([GUint64, GUint64, GUint64]) } function parse_AppMessage(val:V) : CAppMessage - requires ValInGrammar(val, CAppMessage_grammar()); + requires ValInGrammar(val, CAppMessage_grammar()) function {:fuel ValInGrammar,1} parse_Request1(val:V) : CRequest - requires ValInGrammar(val, CRequest_grammar()); + requires ValInGrammar(val, CRequest_grammar()) { if val.c == 0 then var ep := parse_EndPoint(val.val.t[0]); // With default fuel, error: function precondition (6x), destructor, index @@ -339,7 +339,7 @@ module TestModule8 { } function parse_Request2(val:V) : CRequest - requires ValInGrammar(val, CRequest_grammar()); + requires ValInGrammar(val, CRequest_grammar()) { if val.c == 0 then var ep := parse_EndPoint(val.val.t[0]); // With fuel boosted to 2 this succeeds @@ -349,7 +349,7 @@ module TestModule8 { } function {:fuel ValInGrammar,3} parse_Request3(val:V) : CRequest - requires ValInGrammar(val, CRequest_grammar()); + requires ValInGrammar(val, CRequest_grammar()) { if val.c == 0 then var ep := parse_EndPoint(val.val.t[0]); @@ -360,7 +360,7 @@ module TestModule8 { // With the method, everything succeeds with one less fuel boost (i.e., 2, rather than 3, as in parse_Request3) method parse_Request4(val:V) returns (req:CRequest) - requires ValInGrammar(val, CRequest_grammar()); + requires ValInGrammar(val, CRequest_grammar()) { if val.c == 0 { var ep := parse_EndPoint(val.val.t[0]); @@ -381,8 +381,8 @@ module TestModule9 { // All should pass. method test1(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert abs(z) == -1*z; assert abs(y) == y; @@ -391,8 +391,8 @@ module TestModule9 { // Method-level fuel override method {:fuel abs,0,0} test2(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert abs(z) == -1*z; // error: Cannot see the body of abs assert abs(y) == y; // error: Cannot see the body of abs @@ -401,8 +401,8 @@ module TestModule9 { // Statement-level fuel override method test3(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert {:fuel abs,0,0} abs(z) == -1*z; // error: fuel can't be decreased assert abs(y) == y; // Normal success @@ -412,8 +412,8 @@ module TestModule9 { // Giving more fuel to a non-recursive function won't help, // but it shouldn't hurt either. method {:fuel abs,5,6} test4(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert abs(z) == -1*z; assert abs(y) == y; @@ -429,8 +429,8 @@ module TestModule10 { } method test1(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert abs(z) == -1*z; // error: Cannot see the body of abs assert abs(y) == y; // error: Cannot see the body of abs @@ -451,8 +451,8 @@ module TestModule11 { } method test1(y:int, z:int) - requires y > 5; - requires z < 0; + requires y > 5 + requires z < 0 { assert abs'(z) == -1*z; // Annotation on abs' only applies locally, so we see the body of abs assert abs'(y) == y; // Annotation on abs' only applies locally, so we see the body of abs @@ -474,7 +474,7 @@ module TestModule12 { } method {:fuel pos3,2,3} {:fuel pos4,2,3} test (y:int) - requires y > 3; + requires y > 3 { assert pos3(y) == 3 + pos4(y - 3); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect index 522dd947e44..c5a06552f28 100755 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect @@ -1,8 +1,8 @@ Fuel.legacy.dfy(129,8): Error: Fuel can only increase within a given scope. Fuel.legacy.dfy(407,8): Error: Fuel can only increase within a given scope. Fuel.legacy.dfy(17,22): Error: assertion might not hold -Fuel.legacy.dfy(65,27): Error: assertion might not hold -Fuel.legacy.dfy(69,27): Error: assertion might not hold +Fuel.legacy.dfy(66,27): Error: assertion might not hold +Fuel.legacy.dfy(71,27): Error: assertion might not hold Fuel.legacy.dfy(92,22): Error: assertion might not hold Fuel.legacy.dfy(93,23): Error: assertion might not hold Fuel.legacy.dfy(94,22): Error: assertion might not hold @@ -18,22 +18,22 @@ Fuel.legacy.dfy(247,22): Error: assertion might not hold Fuel.legacy.dfy(280,26): Error: assertion might not hold Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(314,93): Related location +Fuel.legacy.dfy(313,41): Related location Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(312,43): Related location +Fuel.legacy.dfy(314,72): Related location Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(312,58): Related location +Fuel.legacy.dfy(314,93): Related location Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(313,41): Related location +Fuel.legacy.dfy(314,46): Related location Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(314,46): Related location +Fuel.legacy.dfy(312,43): Related location Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(314,72): Related location +Fuel.legacy.dfy(312,58): Related location Fuel.legacy.dfy(335,49): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple' Fuel.legacy.dfy(335,50): Error: index out of range Fuel.legacy.dfy(336,38): Error: index out of range @@ -43,16 +43,16 @@ Fuel.legacy.dfy(329,21): Related location Fuel.legacy.dfy(311,43): Related location Fuel.legacy.dfy(336,45): Error: function precondition could not be proved Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(313,41): Related location +Fuel.legacy.dfy(314,93): Related location Fuel.legacy.dfy(336,45): Error: function precondition could not be proved Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(314,72): Related location +Fuel.legacy.dfy(312,58): Related location Fuel.legacy.dfy(336,45): Error: function precondition could not be proved Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(314,93): Related location +Fuel.legacy.dfy(313,41): Related location Fuel.legacy.dfy(336,45): Error: function precondition could not be proved Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(312,58): Related location +Fuel.legacy.dfy(314,72): Related location Fuel.legacy.dfy(336,45): Error: function precondition could not be proved Fuel.legacy.dfy(329,21): Related location Fuel.legacy.dfy(312,43): Related location @@ -64,4 +64,4 @@ Fuel.legacy.dfy(435,22): Error: assertion might not hold Fuel.legacy.dfy(436,22): Error: assertion might not hold Fuel.legacy.dfy(437,23): Error: assertion might not hold -Dafny program verifier finished with 30 verified, 39 errors +Dafny program verifier finished with 31 verified, 39 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/FunctionSpecifications.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/FunctionSpecifications.dfy index 24322e665b3..e661001140d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/FunctionSpecifications.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/FunctionSpecifications.dfy @@ -36,9 +36,8 @@ ghost function SumBad(a: List): int } ghost function FibWithExtraPost(n: int): int - ensures 2 <= n ==> 0 <= FibWithExtraPost(n-1) // This is fine, because the definition of the function is discovered via canCall - ensures 1 <= n ==> 0 <= FibWithExtraPost(n-1) // Error: In the current implementation of Dafny, one needs to actually call the - // function in order to benefit from canCall. This may be improved in the future. + ensures 2 <= n ==> 0 <= FibWithExtraPost(n-1) // This tests that Dafny generates the appropriate CanCall + ensures 1 <= n ==> 0 <= FibWithExtraPost(n-1) // Same here. (Before CanCalls everywhere, this postcondition was not verified.) ensures 0 <= FibWithExtraPost(n) { if n < 0 then 0 else @@ -46,12 +45,13 @@ ghost function FibWithExtraPost(n: int): int FibWithExtraPost(n-2) + FibWithExtraPost(n-1) } + ghost function GoodPost(n: int): int requires 0 <= n ensures 1 <= n ==> GoodPost(n-1) == GoodPost(n-1) ensures GoodPost(2*n - n) == GoodPost(2*(n+5) - 10 - n) // these are legal ways to denote the result value of the function { - assert 2*n - n == 2*(n+5) - 10 - n; + assert n == 2*n - n == 2*(n+5) - 10 - n; if n < 2 then n else GoodPost(n-2) + GoodPost(n-1) } @@ -91,13 +91,13 @@ ghost method M() { ghost function IncB(i: nat): nat { - var n :| n>i; n + var n :| n > i; n } ghost function IncC(i: nat): int ensures IncC(i)>=0 { - var n :| n>i; n + var n :| n > i; n } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/FunctionSpecifications.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/FunctionSpecifications.dfy.expect index b20a56e2f1c..ccbfac16cf3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/FunctionSpecifications.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/FunctionSpecifications.dfy.expect @@ -1,7 +1,5 @@ FunctionSpecifications.dfy(35,45): Error: a postcondition could not be proved on this return path FunctionSpecifications.dfy(31,12): Related location: this is the postcondition that could not be proved -FunctionSpecifications.dfy(45,16): Error: a postcondition could not be proved on this return path -FunctionSpecifications.dfy(40,23): Related location: this is the postcondition that could not be proved FunctionSpecifications.dfy(61,10): Error: cannot prove termination; try supplying a decreases clause FunctionSpecifications.dfy(71,4): Error: a postcondition could not be proved on this return path FunctionSpecifications.dfy(69,21): Related location: this is the postcondition that could not be proved @@ -15,4 +13,4 @@ FunctionSpecifications.dfy(155,2): Error: decreases clause might not decrease FunctionSpecifications.dfy(162,2): Error: decreases clause might not decrease FunctionSpecifications.dfy(167,2): Error: cannot prove termination; try supplying a decreases clause -Dafny program verifier finished with 10 verified, 12 errors +Dafny program verifier finished with 11 verified, 11 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/InductivePredicates.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/InductivePredicates.dfy index dbf275ef822..a46a18dd769 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/InductivePredicates.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/InductivePredicates.dfy @@ -263,6 +263,16 @@ module SomeCoolDisjunctionTests { requires P(x) || Q(x) ensures false // fine { + // The following proof should not be necessary. This lemma used to verify + // automatically, but after a change with CanCall, it stopped verifying. + // The problem may be due to https://github.com/Z3Prover/z3/issues/7444. + // After it is fixed, we should try removing the following lines again. + assert !_k.IsLimit; + if P#[_k](x) { + assert P#[_k](x) == Q#[_k - 1](x); + } else { + assert Q#[_k](x); + } } least predicate Pn[nat](x: int) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Strings.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Strings.dfy index b1b2260ec8c..cfce8478458 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Strings.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Strings.dfy @@ -143,8 +143,8 @@ method WeirdChars() returns (c: char, d: char) method AllCharsTest() { var allChars := set c: char {:trigger Identity(c)} | true :: Identity(c); - var allUTF16CodeUnits := set cp: int {:trigger Identity(cp)} | 0 <= cp < 0x1_0000 :: Identity(cp as char); - assert forall c: char {:trigger Identity(c)} :: 0 <= Identity(c as int) < 0x1_0000; + var allUTF16CodeUnits := set cp: int {:trigger Identity(cp as char)} | 0 <= cp < 0x1_0000 :: Identity(cp as char); + assert forall c: char {:trigger Identity(c)} :: 0 <= Identity(c) as int < 0x1_0000; assert forall c: char :: Identity(c) in allChars; assert allChars == allUTF16CodeUnits; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect index a80d2f3dd26..57f3ebb12af 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect @@ -91,5 +91,5 @@ SubsetTypes.dfy(459,15): Error: assertion might not hold SubsetTypes.dfy(464,13): Error: assertion might not hold Dafny program verifier finished with 13 verified, 91 errors -Total resources used is 740400 -Max resources used by VC is 82700 +Total resources used is 922000 +Max resources used by VC is 132800 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/Induction.legacy.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/Induction.legacy.dfy index a7309c89a8f..473f418e3d3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/Induction.legacy.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/Induction.legacy.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /compile:0 /deprecation:0 /induction:3 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 4 %dafny /compile:0 /deprecation:0 /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" class IntegerInduction { @@ -9,13 +9,13 @@ class IntegerInduction { // SumOfCubes(n) == Gauss(n) * Gauss(n) ghost function SumOfCubes(n: int): int - requires 0 <= n; + requires 0 <= n { if n == 0 then 0 else SumOfCubes(n-1) + n*n*n } ghost function Gauss(n: int): int - requires 0 <= n; + requires 0 <= n { if n == 0 then 0 else Gauss(n-1) + n } @@ -23,39 +23,39 @@ class IntegerInduction { // Here is one proof. It uses a lemma, which is proved separately. lemma Theorem0(n: int) - requires 0 <= n; - ensures SumOfCubes(n) == Gauss(n) * Gauss(n); + requires 0 <= n + ensures SumOfCubes(n) == Gauss(n) * Gauss(n) { - if (n != 0) { + if n != 0 { Theorem0(n-1); Lemma(n-1); } } lemma Lemma(n: int) - requires 0 <= n; - ensures 2 * Gauss(n) == n*(n+1); + requires 0 <= n + ensures 2 * Gauss(n) == n*(n+1) { - if (n != 0) { Lemma(n-1); } + if n != 0 { Lemma(n-1); } } // Here is another proof. It states the lemma as part of the theorem, and // thus proves the two together. lemma Theorem1(n: int) - requires 0 <= n; - ensures SumOfCubes(n) == Gauss(n) * Gauss(n); - ensures 2 * Gauss(n) == n*(n+1); + requires 0 <= n + ensures SumOfCubes(n) == Gauss(n) * Gauss(n) + ensures 2 * Gauss(n) == n*(n+1) { - if (n != 0) { + if n != 0 { Theorem1(n-1); } } lemma DoItAllInOneGo() - ensures (forall n {:split false} :: 0 <= n ==> // WISH reenable quantifier splitting here. This will only work once we generate induction hypotheses at the Dafny level. + ensures forall n {:induction} {:split false} :: 0 <= n ==> // WISH reenable quantifier splitting here. This will only work once we generate induction hypotheses at the Dafny level. SumOfCubes(n) == Gauss(n) * Gauss(n) && - 2 * Gauss(n) == n*(n+1)); + 2 * Gauss(n) == n*(n+1) { } @@ -64,15 +64,15 @@ class IntegerInduction { // Dafny's ghost-method induction tactic). lemma Lemma_Auto(n: int) - requires 0 <= n; - ensures 2 * Gauss(n) == n*(n+1); + requires 0 <= n + ensures 2 * Gauss(n) == n*(n+1) { } lemma Theorem1_Auto(n: int) - requires 0 <= n; - ensures SumOfCubes(n) == Gauss(n) * Gauss(n); - ensures 2 * Gauss(n) == n*(n+1); + requires 0 <= n + ensures SumOfCubes(n) == Gauss(n) * Gauss(n) + ensures 2 * Gauss(n) == n*(n+1) { } @@ -80,37 +80,37 @@ class IntegerInduction { // prove the lemma. lemma Theorem2(n: int) - requires 0 <= n; - ensures SumOfCubes(n) == Gauss(n) * Gauss(n); + requires 0 <= n + ensures SumOfCubes(n) == Gauss(n) * Gauss(n) { - if (n != 0) { + if n != 0 { Theorem2(n-1); - assert (forall m :: 0 <= m ==> 2 * Gauss(m) == m*(m+1)); + assert forall m {:induction} :: 0 <= m ==> 2 * Gauss(m) == m*(m+1); } } lemma M(n: int) - requires 0 <= n; + requires 0 <= n { - assume (forall k :: 0 <= k && k < n ==> 2 * Gauss(k) == k*(k+1)); // manually assume the induction hypothesis + assume forall k :: 0 <= k && k < n ==> 2 * Gauss(k) == k*(k+1); // manually assume the induction hypothesis assert 2 * Gauss(n) == n*(n+1); } // Another way to prove the lemma is to supply a postcondition on the Gauss function lemma Theorem3(n: int) - requires 0 <= n; - ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n); + requires 0 <= n + ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n) { - if (n != 0) { + if n != 0 { Theorem3(n-1); } } ghost function GaussWithPost(n: int): int - requires 0 <= n; - ensures 2 * GaussWithPost(n) == n*(n+1); + requires 0 <= n + ensures 2 * GaussWithPost(n) == n*(n+1) { if n == 0 then 0 else GaussWithPost(n-1) + n } @@ -118,19 +118,19 @@ class IntegerInduction { // Finally, with the postcondition of GaussWithPost, one can prove the entire theorem by induction lemma Theorem4() - ensures (forall n :: 0 <= n ==> - SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n)); + ensures forall n {:induction} :: 0 <= n ==> + SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n) { // look ma, no hints! } lemma Theorem5(n: int) - requires 0 <= n; - ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n); + requires 0 <= n + ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n) { // the postcondition is a simple consequence of these quantified versions of the theorem: - if (*) { - assert (forall m :: 0 <= m ==> SumOfCubes(m) == GaussWithPost(m) * GaussWithPost(m)); + if * { + assert forall m {:induction} :: 0 <= m ==> SumOfCubes(m) == GaussWithPost(m) * GaussWithPost(m); } else { Theorem4(); } @@ -149,10 +149,10 @@ class IntegerInduction { // The example uses an attribute that requests induction on just "j". However, the proof also // goes through by applying induction on both bound variables. function IsSorted(s: seq): bool //WISH remove autotriggers false - ensures IsSorted(s) ==> (forall i,j {:induction j} {:autotriggers false} :: 0 <= i < j < |s| ==> s[i] <= s[j]); - ensures (forall i,j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) ==> IsSorted(s); + ensures IsSorted(s) ==> forall i,j {:induction j} {:autotriggers false} :: 0 <= i < j < |s| ==> s[i] <= s[j] + ensures (forall i,j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) ==> IsSorted(s) { - (forall i {:nowarn} {:matchinglooprewrite false}:: 1 <= i && i < |s| ==> s[i-1] <= s[i]) + forall i {:nowarn} {:matchinglooprewrite false} :: 1 <= i && i < |s| ==> s[i-1] <= s[i] } } @@ -167,9 +167,9 @@ class DatatypeInduction { } method Theorem0(tree: Tree) - ensures 1 <= LeafCount(tree); + ensures 1 <= LeafCount(tree) { - assert (forall t: Tree :: 1 <= LeafCount(t)); + assert forall t: Tree {:induction} :: 1 <= LeafCount(t); } // see also Test/dafny0/DTypes.dfy for more variations of this example @@ -182,7 +182,7 @@ class DatatypeInduction { } method RegressionTest(tree: Tree) // the translation of the following line once crashed Dafny - requires forall y :: 0 <= OccurrenceCount(tree, y); + requires forall y :: 0 <= OccurrenceCount(tree, y) { } @@ -195,7 +195,7 @@ class DatatypeInduction { datatype D = Nothing | Something(D) ghost function FooD(n: nat, d: D): int - ensures 10 <= FooD(n, d); + ensures 10 <= FooD(n, d) { match d case Nothing => diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect index 4511620644e..81afb14df05 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect @@ -1,4 +1,4 @@ Dafny program verifier finished with 272 verified, 0 errors -Total resources used is 29132185 -Max resources used by VC is 2079032 +Total resources used is 27987600 +Max resources used by VC is 1817957 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect index 31b8bf886ee..3f5bab87c1f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect @@ -1,4 +1,4 @@ Dafny program verifier finished with 276 verified, 0 errors -Total resources used is 34463182 -Max resources used by VC is 6990729 +Total resources used is 27733327 +Max resources used by VC is 1227140 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Filter.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Filter.dfy index d6ea16031cf..2c9725bb596 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Filter.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Filter.dfy @@ -221,7 +221,7 @@ lemma FS_Pong(s: Stream, P: Predicate, x: T, k: nat) } } else { assert fs == Filter(s.tail, P); // reminder of where we are - //FS_Pong(s.tail, h, x, k-1); + FS_Pong(s.tail, P, x, k-1); } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/SimpleInduction.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/SimpleInduction.dfy index 82270e29727..0ffe9e2fbe4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/SimpleInduction.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/SimpleInduction.dfy @@ -1,4 +1,4 @@ -// RUN: %testDafnyForEachResolver "%s" -- --allow-deprecation +// RUN: %testDafnyForEachResolver "%s" /* @@ -10,14 +10,14 @@ */ ghost function Fib(n: nat): nat - decreases n; + decreases n { if n < 2 then n else Fib(n-2) + Fib(n-1) } lemma FibLemma(n: nat) - ensures Fib(n) % 2 == 0 <==> n % 3 == 0; - decreases n; + ensures Fib(n) % 2 == 0 <==> n % 3 == 0 + decreases n { - if (n < 2) { + if n < 2 { } else { FibLemma(n-2); FibLemma(n-1); @@ -31,7 +31,7 @@ lemma FibLemma(n: nat) */ lemma FibLemma_Alternative(n: nat) - ensures Fib(n) % 2 == 0 <==> n % 3 == 0; + ensures Fib(n) % 2 == 0 <==> n % 3 == 0 { forall k | 0 <= k < n { FibLemma_Alternative(k); @@ -39,7 +39,7 @@ lemma FibLemma_Alternative(n: nat) } lemma FibLemma_All() - ensures forall n :: 0 <= n ==> (Fib(n) % 2 == 0 <==> n % 3 == 0); + ensures forall n :: 0 <= n ==> (Fib(n) % 2 == 0 <==> n % 3 == 0) { forall n | 0 <= n { FibLemma(n); @@ -59,7 +59,7 @@ lemma FibLemma_All() datatype List = Nil | Cons(head: T, tail: List) ghost function Append(xs: List, ys: List): List - decreases xs; + decreases xs { match xs case Nil => ys @@ -69,8 +69,8 @@ ghost function Append(xs: List, ys: List): List // The {:induction false} attribute disables automatic induction tactic, // so we can make the proof explicit. lemma {:induction false} AppendIsAssociative(xs: List, ys: List, zs: List) - ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs)); - decreases xs; + ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs)) + decreases xs { match (xs) { case Nil => @@ -82,7 +82,6 @@ lemma {:induction false} AppendIsAssociative(xs: List, ys: List, zs: List) // Here the proof is fully automatic - the body of the method is empty, // yet still verifies. lemma AppendIsAssociative_Auto(xs: List, ys: List, zs: List) - ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs)); + ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs)) { } - diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy index 0d3eca21e51..f7da86e8718 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy @@ -1,4 +1,4 @@ -// RUN: %verify --allow-deprecation --solver-option="O:smt.qi.eager_threshold=30" "%s" > "%t" +// RUN: %verify --solver-option="O:smt.qi.eager_threshold=30" "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This is the Extractor Problem from section 11.8 of the ACL2 book, @@ -25,7 +25,7 @@ ghost opaque function nth(n: int, xs: List): T } ghost function nthWorker(n: int, xs: List): T - requires 0 <= n < length(xs); + requires 0 <= n < length(xs) { if n == 0 then xs.head else nthWorker(n-1, xs.tail) } @@ -57,7 +57,7 @@ ghost function xtr(mp: List, lst: List): List } lemma ExtractorTheorem(xs: List) - ensures xtr(nats(length(xs)), xs) == rev(xs); + ensures xtr(nats(length(xs)), xs) == rev(xs) { var a, b := xtr(nats(length(xs)), xs), rev(xs); calc { @@ -73,7 +73,7 @@ lemma ExtractorTheorem(xs: List) length(b); } forall i | 0 <= i < length(xs) - ensures nth(i, a) == nth(i, b); + ensures nth(i, a) == nth(i, b) { reveal nth(); ExtractorLemma(i, xs); @@ -86,22 +86,22 @@ lemma ExtractorTheorem(xs: List) // lemmas about length lemma XtrLength(mp: List, lst: List) - ensures length(xtr(mp, lst)) == length(mp); + ensures length(xtr(mp, lst)) == length(mp) { } lemma NatsLength(n: nat) - ensures length(nats(n)) == n; + ensures length(nats(n)) == n { } lemma AppendLength(xs: List, ys: List) - ensures length(append(xs, ys)) == length(xs) + length(ys); + ensures length(append(xs, ys)) == length(xs) + length(ys) { } lemma RevLength(xs: List) - ensures length(rev(xs)) == length(xs); + ensures length(rev(xs)) == length(xs) { match xs { case Nil => @@ -142,8 +142,8 @@ lemma EqualElementsMakeEqualLists(xs: List, ys: List) // here is the theorem, but applied to the ith element lemma {:isolate_assertions} ExtractorLemma(i: int, xs: List) - requires 0 <= i < length(xs); - ensures nth(i, xtr(nats(length(xs)), xs)) == nth(i, rev(xs)); + requires 0 <= i < length(xs) + ensures nth(i, xtr(nats(length(xs)), xs)) == nth(i, rev(xs)) { calc { nth(i, xtr(nats(length(xs)), xs)); @@ -160,8 +160,8 @@ lemma {:isolate_assertions} ExtractorLemma(i: int, xs: List) // lemmas about what nth gives on certain lists lemma NthXtr(i: int, mp: List, lst: List) - requires 0 <= i < length(mp); - ensures nth(i, xtr(mp, lst)) == nth(nth(i, mp), lst); + requires 0 <= i < length(mp) + ensures nth(i, xtr(mp, lst)) == nth(nth(i, mp), lst) { reveal nth(); XtrLength(mp, lst); @@ -179,8 +179,8 @@ lemma NthXtr(i: int, mp: List, lst: List) } lemma NthNats(i: int, n: nat) - requires 0 <= i < n; - ensures nth(i, nats(n)) == n - 1 - i; + requires 0 <= i < n + ensures nth(i, nats(n)) == n - 1 - i { reveal nth(); NatsLength(n); @@ -188,14 +188,14 @@ lemma NthNats(i: int, n: nat) } lemma NthNatsWorker(i: int, n: nat) - requires 0 <= i < n && length(nats(n)) == n; - ensures nthWorker(i, nats(n)) == n - 1 - i; + requires 0 <= i < n && length(nats(n)) == n + ensures nthWorker(i, nats(n)) == n - 1 - i { } lemma NthRev(i: int, xs: List) - requires 0 <= i < length(xs) == length(rev(xs)); - ensures nthWorker(i, rev(xs)) == nthWorker(length(xs) - 1 - i, xs); + requires 0 <= i < length(xs) == length(rev(xs)) + ensures nthWorker(i, rev(xs)) == nthWorker(length(xs) - 1 - i, xs) { reveal nth(); assert xs.Cons?; @@ -236,8 +236,8 @@ lemma NthRev(i: int, xs: List) } lemma NthAppendA(i: int, xs: List, ys: List) - requires 0 <= i < length(xs); - ensures nth(i, append(xs, ys)) == nth(i, xs); + requires 0 <= i < length(xs) + ensures nth(i, append(xs, ys)) == nth(i, xs) { reveal nth(); if i == 0 { @@ -258,8 +258,8 @@ lemma NthAppendA(i: int, xs: List, ys: List) } lemma NthAppendB(i: int, xs: List, ys: List) - requires length(xs) <= i < length(xs) + length(ys); - ensures nth(i, append(xs, ys)) == nth(i - length(xs), ys); + requires length(xs) <= i < length(xs) + length(ys) + ensures nth(i, append(xs, ys)) == nth(i - length(xs), ys) { reveal nth(); AppendLength(xs, ys); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy index bd80b089d5c..4463e4a41a6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy @@ -382,8 +382,10 @@ lemma sorted_reverse(xs: List, ys: List) { match xs case Nil => - case Cons(x, rest) => + case Cons(x, rest) => { sorted_reverse(rest, Cons(x, ys)); + assert forall a,b :: a in multiset_of(xs) && b in multiset_of(ys) ==> Below(a, b); + } } lemma sorted_insertInMiddle(xs: List, a: G, ys: List) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy index 41baa0682b7..6241e717e7e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy @@ -240,7 +240,7 @@ method test_factorial1() var n10 := S(S(S(S(n6)))); var n12 := S(S(n10)); - assert factorial(n5)==mult(n10, n12); + assert {:split_here} factorial(n5)==mult(n10, n12); } method test_factorial1_old() diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect index e7cc92d0e90..35e54b59f6f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect @@ -1,3 +1,3 @@ SoftwareFoundations-Basics.dfy(41,11): Error: assertion might not hold -Dafny program verifier finished with 52 verified, 1 error +Dafny program verifier finished with 53 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/gcd.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/gcd.dfy index c4307d30918..ad026ef48f9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/gcd.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/gcd.dfy @@ -21,8 +21,8 @@ ghost function Factors(x: pos): set { // The following lemma proves that the conjunct "p <= x" in the // definition of Factors does not reduce the elements in the set. -lemma FactorsHasAllFactors(x: pos) - ensures forall n :: n in Factors(x) <==> n in iset p: pos | IsFactor(p, x) +lemma FactorIsInFactors(p: pos, x: pos) + ensures p in Factors(x) <==> IsFactor (p, x) { } @@ -133,16 +133,28 @@ lemma GcdIdempotent(x: pos) assert x in Factors(x) * Factors(x); } -lemma GcdSubtract(x: pos, y: pos) +lemma {:isolate_assertions} GcdSubtract (x: pos, y: pos) requires x < y ensures Gcd(x, y) == Gcd(x, y - x) { var p := Gcd(x, y); + assert IsFactor (p, x) by { + reveal Gcd(); + assert p in Factors(x); + FactorIsInFactors(p, x); + } + + assert IsFactor (p, y) by { + reveal Gcd(); + assert p in Factors(y); + FactorIsInFactors(p, y); + } + // By the definition of `Gcd`, we know that p is a factor of both x and y, // We now show that p is also a factor of y - x. - assert IsFactor(p, y - x) by { - reveal Gcd(); + assert IsFactor(p, y - x) by + { var a :| p * a == x; var b :| p * b == y; calc { @@ -156,15 +168,15 @@ lemma GcdSubtract(x: pos, y: pos) // Hence, p is a common factor of x and y - x var common := Factors(x) * Factors(y - x); - assert p in common by { reveal Gcd(); } + assert p in common; // It remains to show that, among the common factors of x and // y - x, p is the greatest forall q | q in common ensures q <= p { - // q is a factor of both x and y - x, so a and b exist: reveal Gcd(); + // q is a factor of both x and y - x, so a and b exist: var a :| q * a == x; var b :| q * b == y - x; assert IsFactor(q, y) by { @@ -182,7 +194,7 @@ lemma GcdSubtract(x: pos, y: pos) assert q in Factors(x) * Factors(y); // By the definition of Gcd(x, y), we then have that q <= p. } - assert Gcd(x, y) == Gcd(x, y - x) by { reveal Gcd(); } + assert Gcd(x, y) == Gcd(x, y - x) by {reveal Gcd();} } method EuclidGcd(X: pos, Y: pos) returns (gcd: pos) @@ -222,28 +234,36 @@ lemma {:isolate_assertions} GcdSubtractAlt(x: pos, y: pos) GcdSymmetric(x, y); // this is the difference from GcdSubtract above var p := Gcd(x, y); - assert IsFactor(p, y - x) by { + assert IsFactor (p, x) by { + reveal Gcd(); + assert p in Factors(x); + FactorIsInFactors(p, x); + } + + assert IsFactor (p, y) by { reveal Gcd(); + assert p in Factors(y); + FactorIsInFactors(p, y); + } + + assert IsFactor(p, y - x) by { var a :| p * a == x; var b :| p * b == y; - calc { - y - x; - == - p * b - p * a; - == - p * (b - a); + assert y - x == p * (b - a) by { + assert p * b - p * a == p * (b - a); } } var common := Factors(x) * Factors(y - x); - assert p in common by { reveal Gcd(); } + assert p in common; + forall q | q in common ensures q <= p { reveal Gcd(); var a :| q * a == x; var b :| q * b == y - x; - assert IsFactor(q, y) by { + assert IsFactor(q, y) by { calc { y; == diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect index 802b5ada1dc..101c6a5a397 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect @@ -7,13 +7,13 @@ git-issue-2299.dfy(21,4): Related location: this proposition could not be proved git-issue-2299.dfy(67,13): Error: assertion might not hold git-issue-2299.dfy(21,4): Related location: this proposition could not be proved git-issue-2299.dfy(81,11): Error: assertion might not hold -git-issue-2299.dfy(27,4): Related location: this proposition could not be proved -git-issue-2299.dfy(10,11): Related location: this proposition could not be proved +git-issue-2299.dfy(27,18): Related location: this proposition could not be proved +git-issue-2299.dfy(16,4): Related location: this proposition could not be proved git-issue-2299.dfy(81,11): Error: assertion might not hold git-issue-2299.dfy(27,32): Related location: this proposition could not be proved git-issue-2299.dfy(21,4): Related location: this proposition could not be proved git-issue-2299.dfy(81,11): Error: assertion might not hold -git-issue-2299.dfy(27,18): Related location: this proposition could not be proved -git-issue-2299.dfy(16,4): Related location: this proposition could not be proved +git-issue-2299.dfy(27,4): Related location: this proposition could not be proved +git-issue-2299.dfy(10,11): Related location: this proposition could not be proved Dafny program verifier finished with 7 verified, 7 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2500.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2500.dfy index ffd3895cead..b59730c4dd2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2500.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2500.dfy @@ -31,7 +31,7 @@ class Cl extends M.Tr { ensures ActuallyTrue() { true } predicate ActuallyTrue''() - // This is logically correct, but the disguised receiver in the Tr spec prevents the override check from passing. + // This is logically correct. (Before CanCall, the disguised receiver in the Tr spec had prevented the override check from passing.) ensures ActuallyTrue''() { true } predicate Other(x: nat, free: M.Tr) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2500.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2500.dfy.expect index 64fcebbc922..6360ffa291f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2500.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2500.dfy.expect @@ -1,6 +1,5 @@ git-issue-2500.dfy(21,12): Error: the function must provide an equal or more detailed postcondition than in its parent trait git-issue-2500.dfy(24,12): Error: the function must provide an equal or more detailed postcondition than in its parent trait -git-issue-2500.dfy(33,12): Error: the function must provide an equal or more detailed postcondition than in its parent trait git-issue-2500.dfy(37,12): Error: the function must provide an equal or more detailed postcondition than in its parent trait -Dafny program verifier finished with 26 verified, 4 errors +Dafny program verifier finished with 27 verified, 3 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-370.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-370.dfy index 662b94a697e..f81c4baef3b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-370.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-370.dfy @@ -10,6 +10,9 @@ // to be good, so this test file is meant to alert us to any changes, in // case we then want to revisit this issue in some way. +// UPDATE: With the full implementation of CanCall, this test gives just +// 1 error. + datatype T = T(x: int) datatype S = S(u: int, v: int, w: int, x: int, y: int, z: int) @@ -34,14 +37,14 @@ ghost predicate Good(s: S) { && s.z == 5 } -ghost function {:opaque} GetT(): T { +opaque ghost function GetT(): T { T(5) } lemma foo() ensures var t := GetT(); - && WellFormed(t) // error (1x) - && Good(Func(t)) // error (5x, but only 4 of these are reported, due to the limit of 5 errors per method) + && WellFormed(t) // error + && Good(Func(t)) { reveal GetT(); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-370.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-370.dfy.expect index 6b5ee927f45..cac47f16163 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-370.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-370.dfy.expect @@ -1,17 +1,5 @@ -git-issue-370.dfy(45,0): Error: a postcondition could not be proved on this return path -git-issue-370.dfy(43,7): Related location: this is the postcondition that could not be proved -git-issue-370.dfy(19,5): Related location: this proposition could not be proved -git-issue-370.dfy(45,0): Error: a postcondition could not be proved on this return path -git-issue-370.dfy(44,7): Related location: this is the postcondition that could not be proved -git-issue-370.dfy(29,9): Related location: this proposition could not be proved -git-issue-370.dfy(45,0): Error: a postcondition could not be proved on this return path -git-issue-370.dfy(44,7): Related location: this is the postcondition that could not be proved -git-issue-370.dfy(30,9): Related location: this proposition could not be proved -git-issue-370.dfy(45,0): Error: a postcondition could not be proved on this return path -git-issue-370.dfy(44,7): Related location: this is the postcondition that could not be proved -git-issue-370.dfy(31,9): Related location: this proposition could not be proved -git-issue-370.dfy(45,0): Error: a postcondition could not be proved on this return path -git-issue-370.dfy(44,7): Related location: this is the postcondition that could not be proved -git-issue-370.dfy(32,9): Related location: this proposition could not be proved +git-issue-370.dfy(48,0): Error: a postcondition could not be proved on this return path +git-issue-370.dfy(46,7): Related location: this is the postcondition that could not be proved +git-issue-370.dfy(22,5): Related location: this proposition could not be proved -Dafny program verifier finished with 1 verified, 5 errors +Dafny program verifier finished with 1 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-370b.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-370b.dfy deleted file mode 100644 index f6f30563061..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-370b.dfy +++ /dev/null @@ -1,47 +0,0 @@ -// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" - - -// Issue 370 reported a situation where there were 6 errors, but only 5 of -// them are reported, since there's a limit of 5 error messages per method. -// The confusing part was that the omitted error was the first of the 6, -// which makes it appear as if there's no problem with postcondition -// WellFormed(t) of foo(). While the ordering of error messages is not -// guaranteed to be deterministic, the current behavior for this test happens -// to be good, so this test file is meant to alert us to any changes, in -// case we then want to revisit this issue in some way. - -datatype T = T(x: int) -datatype S = S(u: int, v: int, w: int, x: int, y: int, z: int) - -predicate a(t: T) - -predicate WellFormed(t: T) { - && a(t) -} - -function Func(t: T): S - requires WellFormed(t) // Note, there should be NO complaint about this precondition in foo() below. -{ - S(t.x, t.x, t.x, t.x, t.x, t.x) -} - -predicate Good(s: S) { - && s.u == 5 - && s.v == 5 - && s.w == 5 - && s.x == 5 - && s.y == 5 - && s.z == 5 -} - -opaque function GetT(): T { - T(5) -} - -lemma foo() - ensures var t := GetT(); - && WellFormed(t) // error (1x) - && Good(Func(t)) // error (5x, but only 4 of these are reported, due to the limit of 5 errors per method) -{ - reveal GetT(); -} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-370b.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-370b.dfy.expect deleted file mode 100644 index 15d49a042a5..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-370b.dfy.expect +++ /dev/null @@ -1,17 +0,0 @@ -git-issue-370b.dfy(45,0): Error: a postcondition could not be proved on this return path -git-issue-370b.dfy(43,7): Related location: this is the postcondition that could not be proved -git-issue-370b.dfy(19,5): Related location: this proposition could not be proved -git-issue-370b.dfy(45,0): Error: a postcondition could not be proved on this return path -git-issue-370b.dfy(44,7): Related location: this is the postcondition that could not be proved -git-issue-370b.dfy(29,9): Related location: this proposition could not be proved -git-issue-370b.dfy(45,0): Error: a postcondition could not be proved on this return path -git-issue-370b.dfy(44,7): Related location: this is the postcondition that could not be proved -git-issue-370b.dfy(30,9): Related location: this proposition could not be proved -git-issue-370b.dfy(45,0): Error: a postcondition could not be proved on this return path -git-issue-370b.dfy(44,7): Related location: this is the postcondition that could not be proved -git-issue-370b.dfy(31,9): Related location: this proposition could not be proved -git-issue-370b.dfy(45,0): Error: a postcondition could not be proved on this return path -git-issue-370b.dfy(44,7): Related location: this is the postcondition that could not be proved -git-issue-370b.dfy(32,9): Related location: this proposition could not be proved - -Dafny program verifier finished with 1 verified, 5 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3995.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3995.dfy index fa2d4210fd6..6ccf8a0b99c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3995.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3995.dfy @@ -32,4 +32,17 @@ class C extends T { predicate {:opaque} Valid(x: int) { true } method MyMethod(x: int) requires Valid(x) { } -} \ No newline at end of file +} + +// The following two types make sure that the override axiom is produced with the correct +// parameters to the CanCall function. + +trait TT { + opaque predicate Valid(x: int, y: Y) +} + +class CC extends TT { + opaque predicate Valid(x: int, z: Z) { + if 0 < x then Valid(x - 1, z) else true + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3995.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3995.dfy.expect index ccc01c35f48..023f9ca2415 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3995.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3995.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 11 verified, 0 errors +Dafny program verifier finished with 13 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5331.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5331.dfy index c3d29769fdd..9780cf41b4a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5331.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5331.dfy @@ -1,17 +1,19 @@ -// RUN: %baredafny verify %args --type-system-refresh "%s" > "%t" +// RUN: %baredafny verify %args --type-system-refresh --general-traits=datatype "%s" > "%t" // RUN: %diff "%s.expect" "%t" trait Ins { - function step(s:State):State //requires safe?(s) + function step(s: State): State } type Code = seq datatype State = S( - clock:nat + clock: nat ) { - function fetch_():Ins + function fetch_(): Ins const fetch := fetch_() const step := fetch.step(this) - function run():State decreases clock { + function run(): State + decreases clock + { if clock == 0 then this else step.(clock := clock - 1).run() } -} \ No newline at end of file +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5331.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5331.dfy.expect index ebe2328e072..823a60a105c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5331.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5331.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 2 verified, 0 errors +Dafny program verifier finished with 1 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect index e5b6841d23d..00645d652d1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect @@ -392,7 +392,7 @@ method {:testEntry} FalseAntecedentEnsuresClauseMethod(x: int) returns (r: int) ensures r > 0 { if x < 0 - then x - 1 // unreachable + then x - 1 // unreachable else x + 1 } @@ -414,7 +414,7 @@ function {:testEntry} ObviouslyUnreachableMatchExpressionCaseFunction(t: T): (r: ensures r > 1 // alt: r > 0 { match t { - case A => 1 // unreachable + case A => 1 // unreachable case B => 2 } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect index 53730d6858a..eb4f242deee 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect @@ -343,11 +343,11 @@ method {:testEntry} MultiPartContradictoryRequiresMethod(x: int, y: int) returns function {:testEntry} ContradictoryEnsuresClauseFunc(x: int): (r: int) requires x > 1 - ensures r > x && r < 0 + ensures r > x && r < 0 method {:testEntry} ContradictoryEnsuresClauseMethod(x: int) returns (r: int) requires x > 1 - ensures r > x && r < 0 + ensures r > x && r < 0 // Call function that has contradictory ensures clauses. function {:testEntry} CallContradictoryFunctionFunc(x: int): (r: int) @@ -392,8 +392,8 @@ method {:testEntry} FalseAntecedentEnsuresClauseMethod(x: int) returns (r: int) ensures r > 0 { if x < 0 - then x - 1 // unreachable - else x + 1 + then x - 1 // unreachable + else x + 1 } method {:testEntry} ObviouslyUnreachableIfStatementBranchMethod(x: int) returns (r:int) @@ -414,8 +414,8 @@ function {:testEntry} ObviouslyUnreachableMatchExpressionCaseFunction(t: T): (r: ensures r > 1 // alt: r > 0 { match t { - case A => 1 // unreachable - case B => 2 + case A => 1 // unreachable + case B => 2 } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect index a953198340b..c270958150a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_tests_expected.html.expect @@ -392,8 +392,8 @@ function {:testEntry} ObviouslyUnreachableIfExpressionBranchFunc(x: int): (r:int ensures r > 0 { if x < 0 - then x - 1 // unreachable - else x + 1 + then x - 1 // unreachable + else x + 1 } method {:testEntry} ObviouslyUnreachableIfStatementBranchMethod(x: int) returns (r:int) @@ -414,8 +414,8 @@ function {:testEntry} ObviouslyUnreachableIfExpressionBranchFunc(x: int): (r:int ensures r > 1 // alt: r > 0 { match t { - case A => 1 // unreachable - case B => 2 + case A => 1 // unreachable + case B => 2 } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect index 3e334e1e315..821708a44f9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect @@ -343,11 +343,11 @@ method {:testEntry} MultiPartContradictoryRequiresMethod(x: int, y: int) returns function {:testEntry} ContradictoryEnsuresClauseFunc(x: int): (r: int) requires x > 1 - ensures r > x && r < 0 + ensures r > x && r < 0 method {:testEntry} ContradictoryEnsuresClauseMethod(x: int) returns (r: int) requires x > 1 - ensures r > x && r < 0 + ensures r > x && r < 0 // Call function that has contradictory ensures clauses. function {:testEntry} CallContradictoryFunctionFunc(x: int): (r: int) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/let-expressions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/let-expressions.dfy.expect index c2731da3a7c..43c6c5c9d54 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/let-expressions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/let-expressions.dfy.expect @@ -1,6 +1,6 @@ let-expressions.dfy(6,8): Info: Selected triggers: {s[i]} let-expressions.dfy(7,8): Info: Selected triggers: {s[i]} -let-expressions.dfy(8,8): Info: Selected triggers: {s[_t#0], s[i]} -let-expressions.dfy(9,8): Info: Selected triggers: {s[_t#0], s[i]} +let-expressions.dfy(8,8): Info: Selected triggers: {s[_t#0], s[i]} where _t#0 := i + 1 +let-expressions.dfy(9,8): Info: Selected triggers: {s[_t#0], s[i]} where _t#0 := i + 1 Dafny program verifier finished with 1 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-is-not-too-strict.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-is-not-too-strict.dfy.expect index aef0837895c..4c9f454a9c4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-is-not-too-strict.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-is-not-too-strict.dfy.expect @@ -2,14 +2,14 @@ loop-detection-is-not-too-strict.dfy(15,9): Info: Selected triggers: {P(y, x)}, {P(x, y)} loop-detection-is-not-too-strict.dfy(18,9): Info: Selected triggers: {P(y, x)}, {P(x, y)} -loop-detection-is-not-too-strict.dfy(21,9): Info: Selected triggers: {P(x, _t#0), P(x, y)} +loop-detection-is-not-too-strict.dfy(21,9): Info: Selected triggers: {P(x, _t#0), P(x, y)} where _t#0 := y + 1 loop-detection-is-not-too-strict.dfy(26,9): Info: Selected triggers: {Q(x)} loop-detection-is-not-too-strict.dfy(27,9): Info: Selected triggers: {Q(x)} loop-detection-is-not-too-strict.dfy(28,9): Info: Selected triggers: {P(x, z)}, {P(x, 1)} loop-detection-is-not-too-strict.dfy(33,9): Info: Selected triggers: {Q(x)} loop-detection-is-not-too-strict.dfy(34,9): Info: Selected triggers: {Q(x)} -loop-detection-is-not-too-strict.dfy(36,9): Info: Selected triggers: {Q(_t#0), Q(x)} -loop-detection-is-not-too-strict.dfy(40,9): Info: Selected triggers: {Q(_t#0), Q(x)} +loop-detection-is-not-too-strict.dfy(36,9): Info: Selected triggers: {Q(_t#0), Q(x)} where _t#0 := if z > 1 then x else 3 * z + 1 +loop-detection-is-not-too-strict.dfy(40,9): Info: Selected triggers: {Q(_t#0), Q(x)} where _t#0 := x + 1 Dafny program verifier finished with 1 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-looks-at-ranges-too.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-looks-at-ranges-too.dfy.expect index a6679d8c1ea..992d2e551f2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-looks-at-ranges-too.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-looks-at-ranges-too.dfy.expect @@ -1,4 +1,4 @@ -loop-detection-looks-at-ranges-too.dfy(11,17): Info: Selected triggers: {P(_t#0), P(x)} -loop-detection-looks-at-ranges-too.dfy(13,17): Info: Selected triggers: {P(x), P(_t#0)} +loop-detection-looks-at-ranges-too.dfy(11,17): Info: Selected triggers: {P(_t#0), P(x)} where _t#0 := x + 1 +loop-detection-looks-at-ranges-too.dfy(13,17): Info: Selected triggers: {P(x), P(_t#0)} where _t#0 := x + 1 Dafny program verifier finished with 1 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy.expect index 374f02b7f9b..3d8d9a1765e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy.expect @@ -1,21 +1,21 @@ loop-detection-messages--unit-tests.dfy(11,9): Info: Selected triggers: {f(f(i))} Rejected triggers: {f(i)} (may loop with "f(f(i))") -loop-detection-messages--unit-tests.dfy(12,9): Info: Selected triggers: {f(_t#0), f(i)} -loop-detection-messages--unit-tests.dfy(13,9): Info: Selected triggers: {f(_t#0), f(i)} +loop-detection-messages--unit-tests.dfy(12,9): Info: Selected triggers: {f(_t#0), f(i)} where _t#0 := i + 1 +loop-detection-messages--unit-tests.dfy(13,9): Info: Selected triggers: {f(_t#0), f(i)} where _t#0 := i + 1 loop-detection-messages--unit-tests.dfy(15,9): Info: Quantifier was split into 2 parts. Better verification performance and error reporting may be obtained by splitting the quantifier in source. For more information, see the section quantifier instantiation rules in the reference manual. loop-detection-messages--unit-tests.dfy(15,9): Info: Part #0 is 'false ==> f(i) == f(_t#0)' - Selected triggers: {f(_t#0), f(i)} + Selected triggers: {f(_t#0), f(i)} where _t#0 := i + 1 loop-detection-messages--unit-tests.dfy(15,9): Info: Part #1 is 'false ==> f(i) == g(i)' Selected triggers: {g(i)}, {f(i)} loop-detection-messages--unit-tests.dfy(16,9): Info: Quantifier was split into 2 parts. Better verification performance and error reporting may be obtained by splitting the quantifier in source. For more information, see the section quantifier instantiation rules in the reference manual. loop-detection-messages--unit-tests.dfy(16,9): Info: Part #0 is 'false ==> f(i) == f(_t#0)' - Selected triggers: {f(_t#0), f(i)} + Selected triggers: {f(_t#0), f(i)} where _t#0 := i + 1 loop-detection-messages--unit-tests.dfy(16,9): Info: Part #1 is 'false ==> f(i) == f(i)' Selected triggers: {f(i)} loop-detection-messages--unit-tests.dfy(17,9): Info: Quantifier was split into 2 parts. Better verification performance and error reporting may be obtained by splitting the quantifier in source. For more information, see the section quantifier instantiation rules in the reference manual. loop-detection-messages--unit-tests.dfy(17,9): Info: Part #0 is 'false ==> f(i) == f(_t#0)' - Selected triggers: {f(_t#0), f(i)} + Selected triggers: {f(_t#0), f(i)} where _t#0 := i + 1 loop-detection-messages--unit-tests.dfy(17,9): Info: Part #1 is 'false ==> f(i) == f(i)' Selected triggers: {f(i)} loop-detection-messages--unit-tests.dfy(19,9): Info: Selected triggers: {f(i)} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/matrix-accesses-are-triggers.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/matrix-accesses-are-triggers.dfy.expect index 4dc44f54ccf..4de25509099 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/matrix-accesses-are-triggers.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/matrix-accesses-are-triggers.dfy.expect @@ -1,4 +1,4 @@ -matrix-accesses-are-triggers.dfy(7,11): Info: Selected triggers: {m[j, _t#0], m[i, j]} +matrix-accesses-are-triggers.dfy(7,11): Info: Selected triggers: {m[j, _t#0], m[i, j]} where _t#0 := i + 1 matrix-accesses-are-triggers.dfy(7,82): Error: index 0 out of range matrix-accesses-are-triggers.dfy(7,86): Error: index 1 out of range diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect index 592b2b34dcd..ccd871551da 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect @@ -1,9 +1,9 @@ -some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Info: Selected triggers: {s[_t#0], s[x]} +some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Info: Selected triggers: {s[_t#0], s[x]} where _t#0 := x + 1 some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Info: Quantifier was split into 2 parts. Better verification performance and error reporting may be obtained by splitting the quantifier in source. For more information, see the section quantifier instantiation rules in the reference manual. some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Info: Part #0 is 'x in s ==> s[_t#0] > 0' - Selected triggers: {s[_t#0], s[x]} + Selected triggers: {s[_t#0], s[x]} where _t#0 := x + 1 some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Info: Part #1 is 'x in s ==> _t#0 !in s' - Selected triggers: {s[_t#0], s[x]} + Selected triggers: {s[_t#0], s[x]} where _t#0 := x + 2 some-terms-do-not-look-like-the-triggers-they-match.dfy(24,18): Info: Selected triggers: {x in s + t} some-terms-do-not-look-like-the-triggers-they-match.dfy(25,18): Info: Selected triggers: {x in t}, {x in s} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-recovers-expressivity.dfy.expect index e66366bd3ec..b06c081fc7a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-recovers-expressivity.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-recovers-expressivity.dfy.expect @@ -1,7 +1,7 @@ splitting-triggers-recovers-expressivity.dfy(12,10): Info: Selected triggers: - {P(_t#0), Q(i)}, {P(_t#0), P(i)} + {P(_t#0), Q(i)}, {P(_t#0), P(i)} where _t#0 := i + 1 splitting-triggers-recovers-expressivity.dfy(17,11): Info: Selected triggers: - {P(_t#0), Q(j)}, {P(_t#0), P(j)} + {P(_t#0), Q(j)}, {P(_t#0), P(j)} where _t#0 := j + 1 splitting-triggers-recovers-expressivity.dfy(26,10): Info: Selected triggers: {Q(i)} Rejected triggers: {P(i)} (may loop with "P(i + 1)") splitting-triggers-recovers-expressivity.dfy(33,11): Info: Selected triggers: {Q(j)} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy.expect index 4abcebe8941..80c6a424512 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy.expect @@ -5,7 +5,7 @@ suppressing-warnings-behaves-properly.dfy(14,9): Info: Selected triggers: {f(n)} suppressing-warnings-behaves-properly.dfy(15,9): Info: Selected triggers: {f(n)} suppressing-warnings-behaves-properly.dfy(16,9): Info: The attribute {:autotriggers false} may cause brittle verification. It's better to remove this attribute, or as a second option, manually define a trigger using {:trigger}. For more information, see the section quantifier instantiation rules in the reference manual. suppressing-warnings-behaves-properly.dfy(18,9): Info: Selected triggers: - {g(n), f(_t#0)}, {f(_t#0), f(n)} + {g(n), f(_t#0)}, {f(_t#0), f(n)} where _t#0 := n + 1 suppressing-warnings-behaves-properly.dfy(19,9): Info: Selected triggers: {f(n)} suppressing-warnings-behaves-properly.dfy(20,9): Info: The attribute {:autotriggers false} may cause brittle verification. It's better to remove this attribute, or as a second option, manually define a trigger using {:trigger}. For more information, see the section quantifier instantiation rules in the reference manual. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy index 79489ae4c5e..b983fa44e16 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy @@ -1,4 +1,4 @@ -// RUN: %testDafnyForEachResolver "%s" -- --allow-deprecation +// RUN: %testDafnyForEachResolver "%s" class BreadthFirstSearch @@ -32,18 +32,18 @@ class BreadthFirstSearch BFS(source: Vertex, dest: Vertex, ghost AllVertices: set) returns (d: int, ghost path: List) // source and dest are among AllVertices - requires source in AllVertices && dest in AllVertices; + requires source in AllVertices && dest in AllVertices // AllVertices is closed under Succ - requires IsClosed(AllVertices); + requires IsClosed(AllVertices) // This method has two basic outcomes, as indicated by the sign of "d". // More precisely, "d" is non-negative iff "source" can reach "dest". // The following postcondition says that under the "0 <= d" outcome, // "path" denotes a path of length "d" from "source" to "dest": - ensures 0 <= d ==> IsPath(source, dest, path) && length(path) == d; + ensures 0 <= d ==> IsPath(source, dest, path) && length(path) == d // Moreover, that path is as short as any path from "source" to "dest": - ensures 0 <= d ==> forall p :: IsPath(source, dest, p) ==> length(path) <= length(p); + ensures 0 <= d ==> forall p :: IsPath(source, dest, p) ==> length(path) <= length(p) // Finally, under the outcome "d < 0", there is no path from "source" to "dest": - ensures d < 0 ==> !exists p :: IsPath(source, dest, p); + ensures d < 0 ==> !exists p :: IsPath(source, dest, p) { path := Nil; // avoid indefinite assignment errors var V, C, N := {source}, {source}, {}; @@ -63,30 +63,30 @@ class BreadthFirstSearch assert {:split_here} true; while C != {} // V, Processed, C, N are all subsets of AllVertices: - invariant V <= AllVertices && Processed <= AllVertices && C <= AllVertices && N <= AllVertices; + invariant V <= AllVertices && Processed <= AllVertices && C <= AllVertices && N <= AllVertices // source is encountered: - invariant source in V; + invariant source in V // V is the disjoint union of Processed, C, and N: - invariant V == Processed + C + N; - invariant Processed !! C !! N; // Processed, C, and N are mutually disjoint + invariant V == Processed + C + N + invariant Processed !! C !! N // Processed, C, and N are mutually disjoint // "paths" records a path for every encountered vertex - invariant ValidMap(source, paths); - invariant V == paths.Keys; + invariant ValidMap(source, paths) + invariant V == paths.Keys // shortest paths for vertices in C have length d, and for vertices in N // have length d+1 - invariant forall x :: x in C ==> length(Find(source, x, paths)) == d; - invariant forall x :: x in N ==> length(Find(source, x, paths)) == d + 1; + invariant forall x :: x in C ==> length(Find(source, x, paths)) == d + invariant forall x :: x in N ==> length(Find(source, x, paths)) == d + 1 // "dest" is not reachable for any smaller value of "d": - invariant dest in R(source, d, AllVertices) ==> dest in C; - invariant d != 0 ==> dest !in R(source, d-1, AllVertices); + invariant dest in R(source, d, AllVertices) ==> dest in C + invariant d != 0 ==> dest !in R(source, d-1, AllVertices) // together, Processed and C are all the vertices reachable in at most d steps: - invariant Processed + C == R(source, d, AllVertices); + invariant Processed + C == R(source, d, AllVertices) // N are the successors of Processed that are not reachable within d steps: - invariant N == Successors(Processed, AllVertices) - R(source, d, AllVertices); + invariant N == Successors(Processed, AllVertices) - R(source, d, AllVertices) // if we have exhausted C, then we have also exhausted N: - invariant C == {} ==> N == {}; + invariant C == {} ==> N == {} // variant: - decreases AllVertices - Processed; + decreases AllVertices - Processed { // remove a vertex "v" from "C" var v :| v in C; @@ -97,7 +97,7 @@ class BreadthFirstSearch if v == dest { forall p | IsPath(source, dest, p) - ensures length(pathToV) <= length(p); + ensures length(pathToV) <= length(p) { reveal R(); Lemma_IsPath_R(source, dest, p, AllVertices); @@ -134,7 +134,7 @@ class BreadthFirstSearch // show that "dest" in not in any reachability set, no matter // how many successors one follows forall n: nat - ensures dest !in R(source, n, AllVertices); + ensures dest !in R(source, n, AllVertices) { reveal R(); if n < d { @@ -149,7 +149,7 @@ class BreadthFirstSearch forall p | IsPath(source, dest, p) // this and the previous two lines will establish the // absurdity of a "p" satisfying IsPath(source, dest, p) - ensures false; + ensures false { reveal R(); Lemma_IsPath_R(source, dest, p, AllVertices); @@ -165,8 +165,8 @@ class BreadthFirstSearch lemma Lemma_IsPath_Closure(source: Vertex, dest: Vertex, p: List, AllVertices: set) - requires IsPath(source, dest, p) && source in AllVertices && IsClosed(AllVertices); - ensures dest in AllVertices && forall v :: v in elements(p) ==> v in AllVertices; + requires IsPath(source, dest, p) && source in AllVertices && IsClosed(AllVertices) + ensures dest in AllVertices && forall v :: v in elements(p) ==> v in AllVertices { match p { case Nil => @@ -189,9 +189,9 @@ class BreadthFirstSearch } lemma RMonotonicity(source: Vertex, m: nat, n: nat, AllVertices: set) - requires m <= n; - ensures R(source, m, AllVertices) <= R(source, n, AllVertices); - decreases n - m; + requires m <= n + ensures R(source, m, AllVertices) <= R(source, n, AllVertices) + decreases n - m { reveal R(); if m < n { @@ -200,10 +200,10 @@ class BreadthFirstSearch } lemma {:isolate_assertions} IsReachFixpoint(source: Vertex, m: nat, n: nat, AllVertices: set) - requires R(source, m, AllVertices) == R(source, m+1, AllVertices); - requires m <= n; - ensures R(source, m, AllVertices) == R(source, n, AllVertices); - decreases n - m; + requires R(source, m, AllVertices) == R(source, m+1, AllVertices) + requires m <= n + ensures R(source, m, AllVertices) == R(source, n, AllVertices) + decreases n - m { reveal R(); if m < n { @@ -212,8 +212,8 @@ class BreadthFirstSearch } lemma Lemma_IsPath_R(source: Vertex, x: Vertex, p: List, AllVertices: set) - requires IsPath(source, x, p) && source in AllVertices && IsClosed(AllVertices); - ensures x in R(source, length(p), AllVertices); + requires IsPath(source, x, p) && source in AllVertices && IsClosed(AllVertices) + ensures x in R(source, length(p), AllVertices) { reveal R(); match p { @@ -232,8 +232,8 @@ class BreadthFirstSearch } ghost function Find(source: Vertex, x: Vertex, m: map>): List - requires ValidMap(source, m) && x in m; - ensures IsPath(source, x, Find(source, x, m)); + requires ValidMap(source, m) && x in m + ensures IsPath(source, x, Find(source, x, m)) { m[x] } @@ -241,13 +241,13 @@ class BreadthFirstSearch ghost method UpdatePaths(vSuccs: set, source: Vertex, paths: map>, v: Vertex, pathToV: List) returns (newPaths: map>) - requires ValidMap(source, paths); - requires vSuccs !! paths.Keys; - requires forall succ :: succ in vSuccs ==> IsPath(source, succ, Cons(v, pathToV)); - ensures ValidMap(source, newPaths) && newPaths.Keys == paths.Keys + vSuccs; + requires ValidMap(source, paths) + requires vSuccs !! paths.Keys + requires forall succ :: succ in vSuccs ==> IsPath(source, succ, Cons(v, pathToV)) + ensures ValidMap(source, newPaths) && newPaths.Keys == paths.Keys + vSuccs ensures forall x :: x in paths ==> - Find(source, x, paths) == Find(source, x, newPaths); - ensures forall x :: x in vSuccs ==> Find(source, x, newPaths) == Cons(v, pathToV); + Find(source, x, paths) == Find(source, x, newPaths) + ensures forall x :: x in vSuccs ==> Find(source, x, newPaths) == Cons(v, pathToV) { if vSuccs == {} { newPaths := paths;