summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Cloner.cs4
-rw-r--r--Source/Dafny/DafnyAst.cs62
-rw-r--r--Source/Dafny/Resolver.cs33
-rw-r--r--Source/Dafny/Translator.cs518
-rw-r--r--Source/DafnyExtension/IdentifierTagger.cs3
-rw-r--r--Test/dafny0/Answer28
-rw-r--r--Test/dafny0/CoPrefix.dfy115
-rw-r--r--Test/dafny0/CoResolution.dfy43
-rw-r--r--Test/dafny0/CoinductiveProofs.dfy6
-rw-r--r--Test/dafny0/runtest.bat2
10 files changed, 632 insertions, 182 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 00389ad0..4da38f51 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -375,7 +375,7 @@ namespace Microsoft.Dafny
}
}
- public Statement CloneStmt(Statement stmt) {
+ public virtual Statement CloneStmt(Statement stmt) {
if (stmt == null) {
return null;
}
@@ -539,4 +539,4 @@ namespace Microsoft.Dafny
return tok;
}
}
-} \ No newline at end of file
+}
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 4279d2bb..f69e2f22 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -961,6 +961,20 @@ namespace Microsoft.Dafny {
}
}
}
+
+ public static IEnumerable<CoMethod> AllCoMethods(List<TopLevelDecl> declarations) {
+ foreach (var d in declarations) {
+ var cl = d as ClassDecl;
+ if (cl != null) {
+ foreach (var member in cl.Members) {
+ var m = member as CoMethod;
+ if (m != null) {
+ yield return m;
+ }
+ }
+ }
+ }
+ }
}
public class DefaultModuleDecl : ModuleDefinition {
@@ -1593,6 +1607,20 @@ namespace Microsoft.Dafny {
}
/// <summary>
+ /// An ImplicitFormal is a parameter that is declared implicitly, in particular the "_k" depth parameter
+ /// of each comethod (for use in the comethod body only, not the specification).
+ /// </summary>
+ public class ImplicitFormal : Formal
+ {
+ public ImplicitFormal(IToken/*!*/ tok, string/*!*/ name, Type/*!*/ type, bool inParam, bool isGhost)
+ : base(tok, name, type, inParam, isGhost) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ Contract.Requires(type != null);
+ }
+ }
+
+ /// <summary>
/// A "ThisSurrogate" is used during translation time to make the treatment of the receiver more similar to
/// the treatment of other in-parameters.
/// </summary>
@@ -1699,14 +1727,17 @@ namespace Microsoft.Dafny {
public class PrefixPredicate : Function
{
public readonly Formal K;
+ public readonly CoPredicate Co;
public PrefixPredicate(IToken tok, string name, bool isStatic,
List<TypeParameter> typeArgs, IToken openParen, Formal k, List<Formal> formals,
List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,
- Expression body, Attributes attributes, bool signatureOmitted)
- : base(tok, name, isStatic, true, typeArgs, openParen, formals, new BoolType(), req, reads, ens, decreases, body, attributes, signatureOmitted) {
+ Expression body, Attributes attributes, CoPredicate coPred)
+ : base(tok, name, isStatic, true, typeArgs, openParen, formals, new BoolType(), req, reads, ens, decreases, body, attributes, false) {
Contract.Requires(k != null);
+ Contract.Requires(coPred != null);
Contract.Requires(formals != null && 1 <= formals.Count && formals[0] == k);
K = k;
+ Co = coPred;
}
}
@@ -1722,6 +1753,26 @@ namespace Microsoft.Dafny {
: base(tok, name, isStatic, true, typeArgs, openParen, formals, new BoolType(),
req, reads, ens, new Specification<Expression>(new List<Expression>(), null), body, attributes, signatureOmitted) {
}
+
+ /// <summary>
+ /// For the given call P(s), return P#[depth](s). The resulting expression shares some of the subexpressions
+ /// with 'fexp' (that is, what is returned is not necessarily a clone).
+ /// </summary>
+ public FunctionCallExpr CreatePrefixPredicateCall(FunctionCallExpr fexp, Expression depth) {
+ Contract.Requires(fexp != null);
+ Contract.Requires(fexp.Function == this);
+ Contract.Requires(depth != null);
+ Contract.Ensures(Contract.Result<FunctionCallExpr>() != null);
+
+ var args = new List<Expression>() { depth };
+ args.AddRange(fexp.Args);
+ var prefixPredCall = new FunctionCallExpr(fexp.tok, this.PrefixPredicate.Name, fexp.Receiver, fexp.OpenParen, args);
+ prefixPredCall.Function = this.PrefixPredicate; // resolve here
+ prefixPredCall.TypeArgumentSubstitutions = fexp.TypeArgumentSubstitutions; // resolve here
+ prefixPredCall.Type = fexp.Type; // resolve here
+ prefixPredCall.CoCall = fexp.CoCall; // resolve here
+ return prefixPredCall;
+ }
}
public class Method : MemberDecl, TypeParameter.ParentType, ICodeContext
@@ -1830,14 +1881,17 @@ namespace Microsoft.Dafny {
public class PrefixMethod : Method
{
public readonly Formal K;
+ public readonly CoMethod Co;
public PrefixMethod(IToken tok, string name, bool isStatic,
List<TypeParameter> typeArgs, Formal k, List<Formal> ins, List<Formal> outs,
List<MaybeFreeExpression> req, Specification<FrameExpression> mod, List<MaybeFreeExpression> ens, Specification<Expression> decreases,
- BlockStmt body, Attributes attributes, bool signatureOmitted)
- : base(tok, name, isStatic, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureOmitted) {
+ BlockStmt body, Attributes attributes, CoMethod co)
+ : base(tok, name, isStatic, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, false) {
Contract.Requires(k != null);
Contract.Requires(ins != null && 1 <= ins.Count && ins[0] == k);
+ Contract.Requires(co != null);
K = k;
+ Co = co;
}
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 36f99328..771ff3ee 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -647,7 +647,7 @@ namespace Microsoft.Dafny
MemberDecl extraMember;
var cloner = new Cloner();
var formals = new List<Formal>();
- var k = new Formal(m.tok, "_k", new NatType(), true, false);
+ var k = new ImplicitFormal(m.tok, "_k", new NatType(), true, false);
formals.Add(k);
if (m is CoPredicate) {
var cop = (CoPredicate)m;
@@ -657,17 +657,26 @@ namespace Microsoft.Dafny
cop.TypeArgs.ConvertAll(cloner.CloneTypeParam), cop.OpenParen, k, formals,
cop.Req.ConvertAll(cloner.CloneExpr), cop.Reads.ConvertAll(cloner.CloneFrameExpr), cop.Ens.ConvertAll(cloner.CloneExpr),
new Specification<Expression>(new List<Expression>() { new IdentifierExpr(cop.tok, k.Name) }, null),
- null /*body is filled in later*/, null, false);
+ cop.Body, null, cop);
extraMember = cop.PrefixPredicate;
} else {
var com = (CoMethod)m;
+ // _k has already been added to 'formals', so append the original formals
formals.AddRange(com.Ins.ConvertAll(cloner.CloneFormal));
- // create prefix method
+ // prepend "free requires 0 < _k;", since the postcondition of a comethod holds trivially if _k is 0
+ var req = new List<MaybeFreeExpression>();
+ req.Add(new MaybeFreeExpression(new BinaryExpr(k.tok, BinaryExpr.Opcode.Lt, new LiteralExpr(k.tok, 0), new IdentifierExpr(k.tok, k.Name)), true));
+ req.AddRange(com.Req.ConvertAll(cloner.CloneMayBeFreeExpr));
+ // prepend _k to the given decreases clause
+ var decr = new List<Expression>();
+ decr.Add(new IdentifierExpr(com.tok, k.Name));
+ decr.AddRange(com.Decreases.Expressions.ConvertAll(cloner.CloneExpr));
+ // Create prefix method. Note that the body is not cloned, but simply shared.
com.PrefixMethod = new PrefixMethod(com.tok, extraName, com.IsStatic,
com.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, com.Outs.ConvertAll(cloner.CloneFormal),
- com.Req.ConvertAll(cloner.CloneMayBeFreeExpr), cloner.CloneSpecFrameExpr(com.Mod), com.Ens.ConvertAll(cloner.CloneMayBeFreeExpr),
- new Specification<Expression>(new List<Expression>() { new IdentifierExpr(com.tok, k.Name) }, null),
- null /*body is filled in later*/, null, false);
+ req, cloner.CloneSpecFrameExpr(com.Mod), com.Ens.ConvertAll(cloner.CloneMayBeFreeExpr),
+ new Specification<Expression>(decr, null),
+ com.Body, null, com);
extraMember = com.PrefixMethod;
}
members.Add(extraName, extraMember);
@@ -2607,8 +2616,16 @@ namespace Microsoft.Dafny
}
// Resolve body
- if (m.Body != null) {
- ResolveBlockStatement(m.Body, m.IsGhost, m);
+ if (m is CoMethod) {
+ // don't resolve the body here; instead, resolve it in the scope of the corresponding
+ // prefix method's signature
+ } else if (m.Body != null) {
+ var codeContext = m;
+ if (m is PrefixMethod) {
+ // this will cause the correct edges to be inserted into the call graph
+ codeContext = ((PrefixMethod)m).Co;
+ }
+ ResolveBlockStatement(m.Body, m.IsGhost, codeContext);
}
scope.PopMarker(); // for the out-parameters and outermost-level locals
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index dd7f38c6..8dd3e387 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -592,46 +592,38 @@ namespace Microsoft.Dafny {
AddAllocationAxiom(f);
} else if (member is Function) {
- Function f = (Function)member;
- AddFunction(f);
- if (f.IsRecursive) {
- AddLimitedAxioms(f, 2);
- AddLimitedAxioms(f, 1);
- }
- for (int layerOffset = 0; layerOffset < 2; layerOffset++) {
- var body = f.Body == null ? null : f.Body.Resolved;
- if (body is MatchExpr) {
- AddFunctionAxiomCase(f, (MatchExpr)body, null, layerOffset);
- AddFunctionAxiom(f, null, f.Ens, null, layerOffset);
- } else {
- AddFunctionAxiom(f, body, f.Ens, null, layerOffset);
- }
- if (!f.IsRecursive) { break; }
- }
- AddFrameAxiom(f);
+ var f = (Function)member;
+ AddClassMember_Function(f);
AddWellformednessCheck(f);
+ var cop = f as CoPredicate;
+ if (cop != null) {
+ AddClassMember_Function(cop.PrefixPredicate);
+ // skip the well-formedness check, because it has already been done for the copredicate
+ }
} else if (member is Method) {
Method m = (Method)member;
- bool isRefinementMethod = RefinementToken.IsInherited(m.tok, m.EnclosingClass.Module);
// wellformedness check for method specification
- Bpl.Procedure proc = AddMethod(m, MethodTranslationKind.SpecWellformedness);
- sink.TopLevelDeclarations.Add(proc);
if (m.EnclosingClass is IteratorDecl && m == ((IteratorDecl)m.EnclosingClass).Member_MoveNext) {
// skip the well-formedness check, because it has already been done for the iterator
} else {
+ var proc = AddMethod(m, MethodTranslationKind.SpecWellformedness);
+ sink.TopLevelDeclarations.Add(proc);
AddMethodImpl(m, proc, true);
}
// the method spec itself
sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.InterModuleCall));
sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.IntraModuleCall));
if (m is CoMethod) {
+ // Let the CoCall and Impl forms to use m.PrefixMethod signature and specification (and
+ // note that m.PrefixMethod.Body == m.Body.
+ m = ((CoMethod)m).PrefixMethod;
sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.CoCall));
}
if (m.Body != null) {
// ...and its implementation
- proc = AddMethod(m, MethodTranslationKind.Implementation);
+ var proc = AddMethod(m, MethodTranslationKind.Implementation);
sink.TopLevelDeclarations.Add(proc);
AddMethodImpl(m, proc, false);
}
@@ -642,6 +634,25 @@ namespace Microsoft.Dafny {
}
}
+ private void AddClassMember_Function(Function f) {
+ AddFunction(f);
+ if (f.IsRecursive) {
+ AddLimitedAxioms(f, 2);
+ AddLimitedAxioms(f, 1);
+ }
+ for (int layerOffset = 0; layerOffset < 2; layerOffset++) {
+ var body = f.Body == null ? null : f.Body.Resolved;
+ if (body is MatchExpr) {
+ AddFunctionAxiomCase(f, (MatchExpr)body, null, layerOffset);
+ AddFunctionAxiom(f, null, f.Ens, null, layerOffset);
+ } else {
+ AddFunctionAxiom(f, body, f.Ens, null, layerOffset);
+ }
+ if (!f.IsRecursive) { break; }
+ }
+ AddFrameAxiom(f);
+ }
+
void AddIteratorSpecAndBody(IteratorDecl iter) {
Contract.Requires(iter != null);
@@ -696,7 +707,7 @@ namespace Microsoft.Dafny {
req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));
} else {
bool splitHappened; // we actually don't care
- foreach (var s in TrSplitExpr(p.E, etran, false, out splitHappened)) {
+ foreach (var s in TrSplitExpr(p.E, etran, null, out splitHappened)) {
if (kind == MethodTranslationKind.IntraModuleCall && RefinementToken.IsInherited(s.E.tok, currentModule)) {
// this precondition was inherited into this module, so just ignore it
} else {
@@ -713,7 +724,7 @@ namespace Microsoft.Dafny {
ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));
} else {
bool splitHappened; // we actually don't care
- foreach (var s in TrSplitExpr(p.E, etran, false, out splitHappened)) {
+ foreach (var s in TrSplitExpr(p.E, etran, null, out splitHappened)) {
if (kind == MethodTranslationKind.Implementation && RefinementToken.IsInherited(s.E.tok, currentModule)) {
// this postcondition was inherited into this module, so just ignore it
} else {
@@ -1034,6 +1045,9 @@ namespace Microsoft.Dafny {
sink.TopLevelDeclarations.Add(ax);
ax = FunctionAxiom(f, FunctionAxiomVisibility.ForeignModuleOnly, body, ens, specialization, layerOffset);
sink.TopLevelDeclarations.Add(ax);
+ if (f is CoPredicate) {
+ AddPrefixPredicateAxioms(((CoPredicate)f).PrefixPredicate);
+ }
} else {
var ax = FunctionAxiom(f, FunctionAxiomVisibility.All, body, ens, specialization, layerOffset);
sink.TopLevelDeclarations.Add(ax);
@@ -1097,15 +1111,10 @@ namespace Microsoft.Dafny {
// ante: $IsHeap($Heap) && this != null && formals-have-the-expected-types &&
Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);
- Bpl.BoundVariable bvThis;
- Bpl.Expr bvThisIdExpr;
- if (f.IsStatic) {
- bvThis = null;
- bvThisIdExpr = null;
- } else {
- bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, etran.This, predef.RefType));
+ if (!f.IsStatic) {
+ var bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, etran.This, predef.RefType));
formals.Add(bvThis);
- bvThisIdExpr = new Bpl.IdentifierExpr(f.tok, bvThis);
+ var bvThisIdExpr = new Bpl.IdentifierExpr(f.tok, bvThis);
args.Add(bvThisIdExpr);
// add well-typedness conjunct to antecedent
Type thisType = Resolver.GetReceiverType(f.tok, f);
@@ -1123,8 +1132,27 @@ namespace Microsoft.Dafny {
if (wh != null) { ante = Bpl.Expr.And(ante, wh); }
}
}
+ List<Formal> specializationFormals;
+ if (specialization == null) {
+ specializationFormals = null;
+ } else if (f is PrefixPredicate) {
+ var pp = (PrefixPredicate)f;
+ // the specialization formals are given in terms of the co-predicate formals, but we're sitting
+ // here with the prefix predicate, so lets map them over
+ var paramMap = new Dictionary<Formal, Formal>();
+ for (int i = 0; i < pp.Co.Formals.Count; i++) {
+ paramMap.Add(pp.Co.Formals[i], pp.Formals[i + 1]);
+ }
+ specializationFormals = new List<Formal>();
+ foreach (var p in specialization.Formals) {
+ specializationFormals.Add(paramMap[p]);
+ }
+ Contract.Assert(specializationFormals.Count == specialization.Formals.Count);
+ } else {
+ specializationFormals = specialization.Formals;
+ }
foreach (Formal p in f.Formals) {
- int i = specialization == null ? -1 : specialization.Formals.FindIndex(val => val == p);
+ int i = specializationFormals == null ? -1 : specializationFormals.FindIndex(val => val == p);
if (i == -1) {
bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
formals.Add(bv);
@@ -1184,7 +1212,11 @@ namespace Microsoft.Dafny {
if (body == null) {
meat = Bpl.Expr.True;
} else {
- Expression bodyWithSubst = Substitute(body, null, substMap);
+ var bodyWithSubst = Substitute(body, null, substMap);
+ if (f is PrefixPredicate) {
+ var pp = (PrefixPredicate)f;
+ bodyWithSubst = PrefixSubstitution(pp, bodyWithSubst);
+ }
if (layerOffset == 0) {
meat = Bpl.Expr.And(
CanCallAssumption(bodyWithSubst, etran),
@@ -1222,6 +1254,42 @@ namespace Microsoft.Dafny {
return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax), comment);
}
+ /// <summary>
+ /// For a copredicate P, "pp" is the prefix predicate for P (such that P = pp.Co) and
+ /// "body" is the body of P. Return what would be the body of the prefix predicate pp.
+ /// In particular, return
+ /// 0 LESS _k IMPLIES body'
+ /// where body' is body with the formals of P replaced by the corresponding
+ /// formals of pp and with corecursive calls P(s) replaced by recursive calls to
+ /// pp(_k - 1, s).
+ /// </summary>
+ Expression PrefixSubstitution(PrefixPredicate pp, Expression body) {
+ Contract.Requires(pp != null);
+
+ var paramMap = new Dictionary<IVariable, Expression>();
+ for (int i = 0; i < pp.Co.Formals.Count; i++) {
+ var replacement = pp.Formals[i + 1]; // the +1 is to skip pp's _k parameter
+ var param = new IdentifierExpr(replacement.tok, replacement.Name);
+ param.Var = replacement; // resolve here
+ param.Type = replacement.Type; // resolve here
+ paramMap.Add(pp.Co.Formals[i], param);
+ }
+
+ var k = new IdentifierExpr(pp.tok, pp.K.Name);
+ k.Var = pp.K; // resolve here
+ k.Type = pp.K.Type; // resolve here
+ var kMinusOne = CreateIntSub(pp.tok, k, CreateIntLiteral(pp.tok, 1));
+
+ var s = new PrefixCallSubstituter(null, paramMap, pp.Co, kMinusOne);
+ body = s.Substitute(body);
+
+ // add antecedent "0 < _k ==>"
+ var kIsPositive = new BinaryExpr(pp.tok, BinaryExpr.Opcode.Lt, CreateIntLiteral(pp.tok, 0), k);
+ kIsPositive.ResolvedOp = BinaryExpr.ResolvedOpcode.Lt; // resolve here
+ kIsPositive.Type = Type.Int; // resolve here
+ return DafnyImp(kIsPositive, body);
+ }
+
void AddLimitedAxioms(Function f, int fromLayer) {
Contract.Requires(f != null);
Contract.Requires(f.IsRecursive);
@@ -1267,6 +1335,79 @@ namespace Microsoft.Dafny {
}
/// <summary>
+ /// Add the axioms:
+ /// forall s :: P(s) ==> forall k: nat :: P#[k](s)
+ /// forall s :: (forall k: nat :: P#[k](s)) ==> P(s)
+ /// where "s" is "heap, formals". In more details:
+ /// forall s :: { P(s) } s-has-appropriate-values && P(s) ==> forall k { P#[k](s) } :: 0 ATMOST k ==> P#[k](s)
+ /// forall s :: { P(s) } s-has-appropriate-values && (forall k :: 0 ATMOST k ==> P#[k](s)) ==> P(s)
+ /// </summary>
+ void AddPrefixPredicateAxioms(PrefixPredicate pp) {
+ Contract.Requires(pp != null);
+ Contract.Requires(predef != null);
+ var co = pp.Co;
+ var tok = pp.tok;
+ var etran = new ExpressionTranslator(this, predef, tok);
+
+ var bvs = new Bpl.VariableSeq();
+ var coArgs = new Bpl.ExprSeq();
+ var prefixArgs = new Bpl.ExprSeq();
+ var bv = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, predef.HeapVarName, predef.HeapType));
+ bvs.Add(bv);
+ coArgs.Add(new Bpl.IdentifierExpr(tok, bv));
+ prefixArgs.Add(new Bpl.IdentifierExpr(tok, bv));
+ // ante: $IsHeap($Heap) && this != null && formals-have-the-expected-types &&
+ Bpl.Expr ante = FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);
+
+ if (!pp.IsStatic) {
+ var bvThis = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, etran.This, predef.RefType));
+ bvs.Add(bvThis);
+ var bvThisIdExpr = new Bpl.IdentifierExpr(tok, bvThis);
+ coArgs.Add(bvThisIdExpr);
+ prefixArgs.Add(bvThisIdExpr);
+ // add well-typedness conjunct to antecedent
+ Type thisType = Resolver.GetReceiverType(tok, pp);
+ Bpl.Expr wh = Bpl.Expr.And(
+ Bpl.Expr.Neq(bvThisIdExpr, predef.Null),
+ etran.GoodRef(tok, bvThisIdExpr, thisType));
+ ante = Bpl.Expr.And(ante, wh);
+ }
+
+ // add the formal _k
+ var k = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, pp.Formals[0].UniqueName, TrType(pp.Formals[0].Type)));
+ var kId = new Bpl.IdentifierExpr(tok, k);
+ prefixArgs.Add(kId);
+ var kWhere = GetWhereClause(tok, kId, pp.Formals[0].Type, etran);
+
+ foreach (var p in co.Formals) {
+ bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
+ bvs.Add(bv);
+ var formal = new Bpl.IdentifierExpr(p.tok, bv);
+ coArgs.Add(formal);
+ prefixArgs.Add(formal);
+ // add well-typedness conjunct to antecedent
+ var wh = GetWhereClause(p.tok, formal, p.Type, etran);
+ if (wh != null) { ante = Bpl.Expr.And(ante, wh); }
+ }
+
+ var funcID = new Bpl.IdentifierExpr(tok, FunctionName(co, 1), TrType(co.ResultType));
+ var coAppl = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), coArgs);
+ funcID = new Bpl.IdentifierExpr(tok, FunctionName(pp, 1), TrType(pp.ResultType));
+ var prefixAppl = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), prefixArgs);
+
+ // forall s :: { P(s) } s-has-appropriate-values && P(s) ==> forall k { P#[k](s) } :: 0 ATMOST k ==> P#[k](s)
+ var tr = new Bpl.Trigger(tok, true, new ExprSeq(prefixAppl));
+ var allK = new Bpl.ForallExpr(tok, new VariableSeq(k), tr, BplImp(kWhere, prefixAppl));
+ tr = new Bpl.Trigger(tok, true, new ExprSeq(coAppl));
+ var allS = new Bpl.ForallExpr(tok, bvs, tr, BplImp(BplAnd(ante, coAppl), allK));
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(tok, allS));
+
+ // forall s :: { P(s) } s-has-appropriate-values && (forall k :: 0 ATMOST k ==> P#[k](s)) ==> P(s)
+ allS = new Bpl.ForallExpr(tok, bvs, tr, BplImp(BplAnd(ante, allK), coAppl));
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(tok, allS));
+ }
+
+ /// <summary>
/// Returns the appropriate Boogie function for the given function. In particular:
/// Layer 2: f#2 --currently used only for induction axioms
/// Layer 1: f --this is the default name
@@ -1921,7 +2062,7 @@ namespace Microsoft.Dafny {
foreach (Expression p in f.Ens) {
var functionHeight = currentModule.CallGraph.GetSCCRepresentativeId(f);
var splits = new List<SplitExprInfo>();
- bool splitHappened/*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, 0, etran);
+ bool splitHappened/*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, null, etran);
foreach (var s in splits) {
if (s.IsChecked && !RefinementToken.IsInherited(s.E.tok, currentModule)) {
ens.Add(Ensures(s.E.tok, false, s.E, null, null));
@@ -2339,7 +2480,7 @@ namespace Microsoft.Dafny {
r = BplAnd(r, CanCallAssumption(e.Args, etran));
// get to assume canCall
Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullCompileName + "#canCall", Bpl.Type.Bool);
- ExprSeq args = etran.FunctionInvocationArguments(e);
+ ExprSeq args = etran.FunctionInvocationArguments(e, null);
Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);
r = BplAnd(r, canCallFuncAppl);
return r;
@@ -2456,6 +2597,21 @@ namespace Microsoft.Dafny {
}
}
+ Expression DafnyImp(Expression a, Expression b) {
+ Contract.Requires(a != null);
+ Contract.Requires(b != null);
+ Contract.Ensures(Contract.Result<Expression>() != null);
+
+ if (LiteralExpr.IsTrue(a) || LiteralExpr.IsTrue(b)) {
+ return b;
+ } else {
+ BinaryExpr imp = new BinaryExpr(a.tok, BinaryExpr.Opcode.Imp, a, b);
+ imp.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp; // resolve here
+ imp.Type = Type.Bool; // resolve here
+ return imp;
+ }
+ }
+
Bpl.Expr BplAnd(Bpl.Expr a, Bpl.Expr b) {
Contract.Requires(a != null);
Contract.Requires(b != null);
@@ -2790,7 +2946,7 @@ namespace Microsoft.Dafny {
}
// all is okay, so allow this function application access to the function's axiom, except if it was okay because of the self-call allowance.
Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullCompileName + "#canCall", Bpl.Type.Bool);
- ExprSeq args = etran.FunctionInvocationArguments(e);
+ ExprSeq args = etran.FunctionInvocationArguments(e, null);
Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);
builder.Add(new Bpl.AssumeCmd(expr.tok, allowance == null ? canCallFuncAppl : Bpl.Expr.Or(allowance, canCallFuncAppl)));
@@ -2893,7 +3049,7 @@ namespace Microsoft.Dafny {
CheckWellformed(e.Guard, options, locals, builder, etran);
if (e is AssertExpr || DafnyOptions.O.DisallowSoundnessCheating) {
bool splitHappened;
- var ss = TrSplitExpr(e.Guard, etran, false, out splitHappened);
+ var ss = TrSplitExpr(e.Guard, etran, null, out splitHappened);
if (!splitHappened) {
builder.Add(Assert(e.Guard.tok, etran.TrExpr(e.Guard), "condition in assert expression might not hold"));
} else {
@@ -2988,7 +3144,7 @@ namespace Microsoft.Dafny {
inferredDecreases = false;
List<Expression> decr = m.Decreases.Expressions;
- if (decr.Count == 0) {
+ if (decr.Count == 0 || (m is PrefixMethod && decr.Count == 1)) {
decr = new List<Expression>();
foreach (Formal p in m.Ins) {
if (IsOrdered(p.Type)) {
@@ -3355,10 +3511,6 @@ namespace Microsoft.Dafny {
sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, FunctionName(f, 0), args, res));
sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, FunctionName(f, 2), args, res));
}
- if (f is CoPredicate) {
- sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, f.FullCompileName + "#cert0", args, res));
- sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, f.FullCompileName + "#cert1", args, res));
- }
res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullCompileName + "#canCall", args, res);
@@ -3438,7 +3590,7 @@ namespace Microsoft.Dafny {
req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));
} else {
bool splitHappened; // we actually don't care
- foreach (var s in TrSplitExpr(p.E, etran, false, out splitHappened)) {
+ foreach (var s in TrSplitExpr(p.E, etran, null, out splitHappened)) {
if ((kind == MethodTranslationKind.IntraModuleCall || kind == MethodTranslationKind.CoCall) && RefinementToken.IsInherited(s.E.tok, currentModule)) {
// this precondition was inherited into this module, so just ignore it
} else {
@@ -3450,14 +3602,19 @@ namespace Microsoft.Dafny {
comment = null;
}
comment = "user-defined postconditions";
+ IdentifierExpr depthArgument = null;
+ if (m is PrefixMethod) {
+ var pm = (PrefixMethod)m;
+ depthArgument = new IdentifierExpr(pm.tok, pm.K.Name);
+ depthArgument.Var = pm.K; // resolve here
+ depthArgument.Type = pm.K.Type; // resolve here
+ }
foreach (var p in m.Ens) {
if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {
ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));
} else {
var ss = new List<SplitExprInfo>();
- var splitHappened/*we actually don't care*/ = TrSplitExpr(p.E, ss, true, int.MaxValue,
- kind == MethodTranslationKind.CoCall ? 2 : kind == MethodTranslationKind.Implementation && m is CoMethod ? 1 : 0,
- etran);
+ var splitHappened/*we actually don't care*/ = TrSplitExpr(p.E, ss, true, int.MaxValue, depthArgument, etran);
foreach (var s in ss) {
var post = s.E;
if (kind == MethodTranslationKind.Implementation && RefinementToken.IsInherited(s.E.tok, currentModule)) {
@@ -3534,14 +3691,14 @@ namespace Microsoft.Dafny {
req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, null));
} else {
bool splitHappened; // we actually don't care
- foreach (var s in TrSplitExpr(p.E, etran, false, out splitHappened)) {
+ foreach (var s in TrSplitExpr(p.E, etran, null, out splitHappened)) {
req.Add(Requires(s.E.tok, s.IsOnlyFree, s.E, null, null));
}
}
}
foreach (MaybeFreeExpression p in m.Ens) {
bool splitHappened; // we actually don't care
- foreach (var s in TrSplitExpr(p.E, etran, false, out splitHappened)) {
+ foreach (var s in TrSplitExpr(p.E, etran, null, out splitHappened)) {
ens.Add(Ensures(s.E.tok, s.IsOnlyFree, s.E, "Error: postcondition of refined method may be violated", null));
}
}
@@ -3632,7 +3789,7 @@ namespace Microsoft.Dafny {
foreach (var p in m.Ens) {
bool splitHappened; // we actually don't care
- foreach (var s in TrSplitExpr(p.E, etran, false, out splitHappened)) {
+ foreach (var s in TrSplitExpr(p.E, etran, null, out splitHappened)) {
var assert = new Bpl.AssertCmd(method.tok, s.E, ErrorMessageAttribute(s.E.tok, "This is the postcondition that may not hold."));
assert.ErrorData = "Error: A postcondition of the refined method may not hold.";
builder.Add(assert);
@@ -3706,7 +3863,7 @@ namespace Microsoft.Dafny {
var ens = new Bpl.EnsuresSeq();
foreach (Expression p in f.Ens) {
bool splitHappened; // we actually don't care
- foreach (var s in TrSplitExpr(p, etran, false, out splitHappened)) {
+ foreach (var s in TrSplitExpr(p, etran, null, out splitHappened)) {
if (s.IsChecked) {
ens.Add(Ensures(s.E.tok, false, s.E, null, null));
}
@@ -4122,7 +4279,7 @@ namespace Microsoft.Dafny {
enclosingToken = stmt.Tok;
}
bool splitHappened;
- var ss = TrSplitExpr(s.Expr, etran, false, out splitHappened);
+ var ss = TrSplitExpr(s.Expr, etran, null, out splitHappened);
if (!splitHappened) {
var tok = enclosingToken == null ? s.Expr.tok : new NestedToken(enclosingToken, s.Expr.tok);
builder.Add(Assert(tok, etran.TrExpr(s.Expr), "assertion violation", stmt.Tok));
@@ -4202,7 +4359,7 @@ namespace Microsoft.Dafny {
// do nothing
} else {
bool splitHappened; // actually, we don't care
- var ss = TrSplitExpr(p.E, yeEtran, false, out splitHappened);
+ var ss = TrSplitExpr(p.E, yeEtran, null, out splitHappened);
foreach (var split in ss) {
if (RefinementToken.IsInherited(split.E.tok, currentModule)) {
// this postcondition was inherited into this module, so just ignore it
@@ -4461,7 +4618,7 @@ namespace Microsoft.Dafny {
b = new Bpl.StmtListBuilder();
TrStmt(s.Hints[i], b, locals, etran);
bool splitHappened;
- var ss = TrSplitExpr(s.Steps[i], etran, false, out splitHappened);
+ var ss = TrSplitExpr(s.Steps[i], etran, null, out splitHappened);
if (!splitHappened) {
b.Add(AssertNS(s.Lines[i + 1].tok, etran.TrExpr(s.Steps[i]), "the calculation step between the previous line and this line might not hold"));
} else {
@@ -5040,7 +5197,7 @@ namespace Microsoft.Dafny {
TrStmt_CheckWellformed(ens.E, definedness, locals, etran, false);
if (!ens.IsFree) {
bool splitHappened; // we actually don't care
- foreach (var split in TrSplitExpr(ens.E, etran, false, out splitHappened)) {
+ foreach (var split in TrSplitExpr(ens.E, etran, null, out splitHappened)) {
if (split.IsChecked) {
definedness.Add(Assert(split.E.tok, split.E, "possible violation of postcondition of parallel statement"));
}
@@ -5171,7 +5328,7 @@ namespace Microsoft.Dafny {
invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));
} else {
bool splitHappened;
- var ss = TrSplitExpr(loopInv.E, etran, false, out splitHappened);
+ var ss = TrSplitExpr(loopInv.E, etran, null, out splitHappened);
if (!splitHappened) {
var wInv = Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E));
invariants.Add(Assert(loopInv.E.tok, wInv, "loop invariant violation"));
@@ -5404,13 +5561,50 @@ namespace Microsoft.Dafny {
Contract.Requires(locals != null);
Contract.Requires(etran != null);
+ // 'codeContext' can be a Method or an IteratorDecl. In case of the latter, the caller is really
+ // the iterator's MoveNext method. Computer the caller here:
+ Method caller = codeContext as Method ?? ((IteratorDecl)codeContext).Member_MoveNext;
+ // Figure out if the call is recursive or not, which will be used below to determine the need for a
+ // termination check and the need to include an implicit _k-1 argument.
+ bool isRecursiveCall = false;
+ if (method is PrefixMethod) {
+ // An explicit call to a prefix method is allowed only within the corresponding comethod's SCC, so
+ // this is really a recursive call.
+ Contract.Assert(codeContext is PrefixMethod); // sanity check
+ isRecursiveCall = true;
+ } else {
+ // consult the call graph to figure out if this is a recursive call
+ var module = method.EnclosingClass.Module;
+ if (module == currentModule) {
+ // Note, prefix methods are not recorded in the call graph, but their corresponding comethods are.
+ Method cllr = caller is PrefixMethod ? ((PrefixMethod)caller).Co : caller;
+ if (module.CallGraph.GetSCCRepresentative(method) == module.CallGraph.GetSCCRepresentative(cllr)) {
+ isRecursiveCall = true;
+ }
+ }
+ }
+
+ MethodTranslationKind kind;
+ var callee = method;
+ if (method is CoMethod && isRecursiveCall) {
+ kind = MethodTranslationKind.CoCall;
+ callee = ((CoMethod)method).PrefixMethod;
+ } else if (method is PrefixMethod) {
+ // an explicit call to a prefix method is allowed only inside the SCC of the corresponding comethod,
+ // so we consider this to be a co-call
+ kind = MethodTranslationKind.CoCall;
+ } else if (RefinementToken.IsInherited(method.tok, currentModule) && (codeContext == null || !codeContext.MustReverify)) {
+ kind = MethodTranslationKind.IntraModuleCall;
+ } else {
+ kind = MethodTranslationKind.InterModuleCall;
+ }
+
+ // Translate receiver argument, if any
Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver, dafnyReceiver.Type);
Bpl.ExprSeq ins = new Bpl.ExprSeq();
if (!method.IsStatic) {
- if (bReceiver == null) {
- if (!(dafnyReceiver is ThisExpr)) {
- CheckNonNull(dafnyReceiver.tok, dafnyReceiver, builder, etran, null);
- }
+ if (bReceiver == null && !(dafnyReceiver is ThisExpr)) {
+ CheckNonNull(dafnyReceiver.tok, dafnyReceiver, builder, etran, null);
}
ins.Add(etran.TrExpr(receiver));
}
@@ -5419,43 +5613,47 @@ namespace Microsoft.Dafny {
// but Boogie doesn't give us a hook for that. So, we set up our own local variables here to
// store the actual parameters.
// Create a local variable for each formal parameter, and assign each actual parameter to the corresponding local
- Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
- for (int i = 0; i < method.Ins.Count; i++) {
- Formal p = method.Ins[i];
- VarDecl local = new VarDecl(p.tok, p.Name + "#", p.Type, p.IsGhost);
+ var substMap = new Dictionary<IVariable, Expression>();
+ for (int i = 0; i < callee.Ins.Count; i++) {
+ var formal = callee.Ins[i];
+ var local = new VarDecl(formal.tok, formal.Name + "#", formal.Type, formal.IsGhost);
local.type = local.OptionalType; // resolve local here
- IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);
+ var ie = new IdentifierExpr(local.Tok, local.UniqueName);
ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here
- substMap.Add(p, ie);
+ substMap.Add(formal, ie);
locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));
- Bpl.IdentifierExpr param = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified?
- Expression actual = Args[i];
- TrStmt_CheckWellformed(actual, builder, locals, etran, true);
- var bActual = etran.TrExpr(actual);
- CheckSubrange(actual.tok, bActual, p.Type, builder);
- Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, param, etran.CondApplyBox(actual.tok, bActual, cce.NonNull(actual.Type), method.Ins[i].Type));
+ var param = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified?
+ Bpl.Expr bActual;
+ if (i == 0 && method is CoMethod && isRecursiveCall) {
+ // Treat this call to M(args) as a call to the corresponding prefix method M#(_k - 1, args), so insert an argument here.
+ var k = ((PrefixMethod)caller).K;
+ bActual = Bpl.Expr.Sub(new Bpl.IdentifierExpr(k.tok, k.UniqueName, Bpl.Type.Int), Bpl.Expr.Literal(1));
+ } else {
+ Expression actual;
+ if (method is CoMethod && isRecursiveCall) {
+ actual = Args[i - 1];
+ } else {
+ actual = Args[i];
+ }
+ TrStmt_CheckWellformed(actual, builder, locals, etran, true);
+ bActual = etran.CondApplyBox(actual.tok, etran.TrExpr(actual), actual.Type, formal.Type);
+ CheckSubrange(actual.tok, bActual, formal.Type, builder);
+ }
+ Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(formal.tok, param, bActual);
builder.Add(cmd);
ins.Add(param);
}
// Check modifies clause of a subcall is a subset of the current frame.
- CheckFrameSubset(tok, method.Mod.Expressions, receiver, substMap, etran, builder, "call may violate context's modifies clause", null);
+ CheckFrameSubset(tok, callee.Mod.Expressions, receiver, substMap, etran, builder, "call may violate context's modifies clause", null);
// Check termination
- ModuleDefinition module = method.EnclosingClass.Module;
- bool isRecursiveCall = false;
- if (module == currentModule) {
- var caller = codeContext is Method ? (Method)codeContext : ((IteratorDecl)codeContext).Member_MoveNext;
- if (module.CallGraph.GetSCCRepresentative(method) == module.CallGraph.GetSCCRepresentative(caller)) {
- isRecursiveCall = true;
- if (!(method is CoMethod)) {
- bool contextDecrInferred, calleeDecrInferred;
- List<Expression> contextDecreases = MethodDecreasesWithDefault(caller, out contextDecrInferred);
- List<Expression> calleeDecreases = MethodDecreasesWithDefault(method, out calleeDecrInferred);
- CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, etran, builder, contextDecrInferred, null);
- }
- }
+ if (isRecursiveCall) {
+ bool contextDecrInferred, calleeDecrInferred;
+ List<Expression> contextDecreases = MethodDecreasesWithDefault(caller, out contextDecrInferred);
+ List<Expression> calleeDecreases = MethodDecreasesWithDefault(callee, out calleeDecrInferred);
+ CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, etran, builder, contextDecrInferred, null);
}
// Create variables to hold the output parameters of the call, so that appropriate unboxes can be introduced.
@@ -5463,7 +5661,7 @@ namespace Microsoft.Dafny {
List<Bpl.IdentifierExpr> tmpOuts = new List<Bpl.IdentifierExpr>();
for (int i = 0; i < Lhss.Count; i++) {
var bLhs = Lhss[i];
- if (ExpressionTranslator.ModeledAsBoxType(method.Outs[i].Type) && !ExpressionTranslator.ModeledAsBoxType(LhsTypes[i])) {
+ if (ExpressionTranslator.ModeledAsBoxType(callee.Outs[i].Type) && !ExpressionTranslator.ModeledAsBoxType(LhsTypes[i])) {
// we need an Unbox
Bpl.LocalVariable var = new Bpl.LocalVariable(bLhs.tok, new Bpl.TypedIdent(bLhs.tok, "$tmp##" + otherTmpVarCount, predef.BoxType));
otherTmpVarCount++;
@@ -5478,15 +5676,7 @@ namespace Microsoft.Dafny {
}
// Make the call
- MethodTranslationKind kind;
- if (isRecursiveCall && method is CoMethod) {
- kind = MethodTranslationKind.CoCall;
- } else if (RefinementToken.IsInherited(method.tok, currentModule) && (codeContext == null || !codeContext.MustReverify)) {
- kind = MethodTranslationKind.IntraModuleCall;
- } else {
- kind = MethodTranslationKind.InterModuleCall;
- }
- Bpl.CallCmd call = new Bpl.CallCmd(tok, MethodName(method, kind), ins, outs);
+ Bpl.CallCmd call = new Bpl.CallCmd(tok, MethodName(callee, kind), ins, outs);
builder.Add(call);
// Unbox results as needed
@@ -6882,7 +7072,7 @@ namespace Microsoft.Dafny {
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
- return TrFunctionCallExpr(e, 0);
+ return TrFunctionCallExpr(e, null);
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
@@ -7231,39 +7421,32 @@ namespace Microsoft.Dafny {
/// <summary>
/// Return a Boogie call corresponding to "e".
- /// If certificatePrimes == 0 or the function is not a copredicate, then the usual function name is used (modulated, as
+ /// If coContextDepth is null or the function is not a copredicate, then the usual function name is used (modulated, as
/// usual, by the layer offset).
- /// Otherwise (that is, if certificatePrimes > 0 and the function is a copredicate), then the function generated will
- /// be one for a proof certificate, where certificatePrimes indicates the number of ``primes'' on the certificate.
- /// For example, for a copredicate P(s), if certificatePrimes==1, then P'(s) will be produced, and if certificatePrimes==2,
- /// then P''(s) will be produced. Note, although the ``primes'' reflect the way one might speak of these on a
- /// whiteboard, P' and P'' are actually denoted P#cert0 and P#cert1 in the Boogie file.
+ /// Otherwise (that is, if certificatePrimes != null and the function is a copredicate), then the function generated will
+ /// be one for the corresponding prefix predicate, using coContextDepth as the depth argument.
/// </summary>
- public Bpl.Expr TrFunctionCallExpr(FunctionCallExpr e, int certificatePrimes) {
+ public Bpl.Expr TrFunctionCallExpr(FunctionCallExpr e, Bpl.Expr coContextDepth) {
Contract.Requires(e != null);
- Contract.Requires(0 <= certificatePrimes && certificatePrimes < 3);
- if (e.Function.IsRecursive) {
+ var isRecursive = e.Function.IsRecursive;
+ var f = coContextDepth != null && e.Function is CoPredicate ? ((CoPredicate)e.Function).PrefixPredicate : e.Function;
+ if (isRecursive) {
Statistics_CustomLayerFunctionCount++;
}
- string nm;
- if (0 < certificatePrimes && e.Function is CoPredicate) {
- nm = e.Function.FullCompileName + "#cert" + (certificatePrimes - 1);
- } else {
- int offsetToUse = e.Function.IsRecursive ? this.layerOffset : 0;
- nm = FunctionName(e.Function, 1 + offsetToUse);
- if (this.applyLimited_CurrentFunction != null && e.Function.IsRecursive) {
- ModuleDefinition module = cce.NonNull(e.Function.EnclosingClass).Module;
- if (module == cce.NonNull(applyLimited_CurrentFunction.EnclosingClass).Module) {
- if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(applyLimited_CurrentFunction)) {
- nm = FunctionName(e.Function, 0 + offsetToUse);
- }
+ int offsetToUse = isRecursive ? this.layerOffset : 0;
+ string nm = FunctionName(f, 1 + offsetToUse);
+ if (this.applyLimited_CurrentFunction != null && isRecursive) {
+ ModuleDefinition module = cce.NonNull(f.EnclosingClass).Module;
+ if (module == cce.NonNull(applyLimited_CurrentFunction.EnclosingClass).Module) {
+ if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(applyLimited_CurrentFunction)) {
+ nm = FunctionName(e.Function, 0 + offsetToUse);
}
}
}
- Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(e.tok, nm, translator.TrType(cce.NonNull(e.Type)));
- Bpl.ExprSeq args = FunctionInvocationArguments(e);
- Bpl.Expr result = new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(id), args);
+ var id = new Bpl.IdentifierExpr(e.tok, nm, translator.TrType(e.Type));
+ var args = FunctionInvocationArguments(e, e.Function is CoPredicate ? coContextDepth : null);
+ var result = new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(id), args);
return CondApplyUnbox(e.tok, result, e.Function.ResultType, e.Type);
}
@@ -7348,7 +7531,7 @@ namespace Microsoft.Dafny {
return typeAntecedent;
}
- public ExprSeq FunctionInvocationArguments(FunctionCallExpr e) {
+ public ExprSeq FunctionInvocationArguments(FunctionCallExpr e, Bpl.Expr depthArgument) {
Contract.Requires(e != null);
Contract.Ensures(Contract.Result<ExprSeq>() != null);
@@ -7357,6 +7540,9 @@ namespace Microsoft.Dafny {
if (!e.Function.IsStatic) {
args.Add(TrExpr(e.Receiver));
}
+ if (depthArgument != null) {
+ args.Add(depthArgument);
+ }
for (int i = 0; i < e.Args.Count; i++) {
Expression ee = e.Args[i];
Type t = e.Function.Formals[i].Type;
@@ -8109,13 +8295,13 @@ namespace Microsoft.Dafny {
}
}
- List<SplitExprInfo/*!*/>/*!*/ TrSplitExpr(Expression expr, ExpressionTranslator etran, bool inCoContext, out bool splitHappened) {
+ List<SplitExprInfo/*!*/>/*!*/ TrSplitExpr(Expression expr, ExpressionTranslator etran, Expression coContextDepth, out bool splitHappened) {
Contract.Requires(expr != null);
Contract.Requires(etran != null);
Contract.Ensures(Contract.Result<List<SplitExprInfo>>() != null);
var splits = new List<SplitExprInfo>();
- splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, inCoContext ? 1 : 0, etran);
+ splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, coContextDepth, etran);
return splits;
}
@@ -8124,9 +8310,9 @@ namespace Microsoft.Dafny {
/// If a (necessarily boolean) function call appears as a top-level conjunct, then inline the function if
/// if it declared in the current module and its height is less than "heightLimit".
///
- /// If "coContextDepth > 0", then any copredicate P(s) appearing in a positive position is interpreted as
- /// a proof certificate P'(s) or P''(s) for P(s), and similarly an equality A==B on co-datatype values is
- /// interpreted as a proof certificate A ~~' B or A ~~'' B for the equality. These certificate interpretations
+ /// If "coContextDepth != null", then any copredicate P(s) appearing in a positive position is interpreted as
+ /// a prefix predicate P#[coContextDepth](s), and similarly an equality A==B on co-datatype values is
+ /// interpreted as a proof certificate A ==#[coContextDepth] B. These prefix-predicate interpretations
/// have an effect on inlining.
/// In particular, where P(s) would inline into:
/// check P(s) \/ H(s)
@@ -8146,11 +8332,10 @@ namespace Microsoft.Dafny {
/// check A ~~' B \/ A.tail ~~'' B.tail
/// free A ~~' B
/// </summary>
- bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool position, int heightLimit, int coContextDepth, ExpressionTranslator etran) {
+ bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool position, int heightLimit, Expression coContextDepth, ExpressionTranslator etran) {
Contract.Requires(expr != null);
Contract.Requires(expr.Type is BoolType || (expr is BoxingCastExpr && ((BoxingCastExpr)expr).E.Type is BoolType));
Contract.Requires(splits != null);
- Contract.Requires(0 <= coContextDepth && coContextDepth < 3);
Contract.Requires(etran != null);
if (expr is BoxingCastExpr) {
@@ -8215,6 +8400,7 @@ namespace Microsoft.Dafny {
}
}
return true;
+#if SOON
} else if (position && coContextDepth == 2 && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.EqCommon && bin.E0.Type.IsCoDatatype) {
var eq = etran.TrEquality(bin.tok, bin.E0, bin.E1, 2);
splits.Add(new SplitExprInfo(SplitExprInfo.K.Both, eq));
@@ -8250,6 +8436,7 @@ namespace Microsoft.Dafny {
splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, Bpl.Expr.Binary(new NestedToken(bin.tok, ctor.tok), BinaryOperator.Opcode.Or, eq, Bpl.Expr.Imp(lhs, rhs))));
}
return true;
+#endif
}
} else if (expr is ITEExpr) {
@@ -8307,10 +8494,16 @@ namespace Microsoft.Dafny {
var fexp = (FunctionCallExpr)expr;
var f = fexp.Function;
Contract.Assert(f != null); // filled in during resolution
+ if (f is CoPredicate && coContextDepth != null) {
+ // rewrite P(s) into P#[coContextDepth](s)
+ var cop = (CoPredicate)f;
+ var prefixPredCall = cop.CreatePrefixPredicateCall(fexp, coContextDepth);
+ return TrSplitExpr(prefixPredCall, splits, position, heightLimit, null, etran);
+ }
var module = f.EnclosingClass.Module;
var functionHeight = module.CallGraph.GetSCCRepresentativeId(f);
- if (module == currentModule && functionHeight < heightLimit && f.Body != null && !(f.Body.Resolved is MatchExpr) && coContextDepth < 2) {
+ if (module == currentModule && functionHeight < heightLimit && f.Body != null && !(f.Body.Resolved is MatchExpr)) {
if (RefinementToken.IsInherited(fexp.tok, currentModule) &&
f is Predicate && ((Predicate)f).BodyOrigin == Predicate.BodyOriginKind.DelayedDefinition &&
(codeContext == null || !codeContext.MustReverify)) {
@@ -8327,7 +8520,12 @@ namespace Microsoft.Dafny {
arg.Type = p.Type; // resolve here
substMap.Add(p, arg);
}
- Expression body = Substitute(f.Body, fexp.Receiver, substMap);
+ var body = f.Body;
+ if (f is PrefixPredicate) {
+ var pp = (PrefixPredicate)f;
+ body = PrefixSubstitution(pp, body);
+ }
+ body = Substitute(body, fexp.Receiver, substMap);
// Produce, for a "body" split into b0, b1, b2:
// free F#canCall(args) && F(args) && (b0 && b1 && b2)
@@ -8343,30 +8541,22 @@ namespace Microsoft.Dafny {
// F#canCall(args)
Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool);
- ExprSeq args = etran.FunctionInvocationArguments(fexp);
+ ExprSeq args = etran.FunctionInvocationArguments(fexp, null);
Bpl.Expr canCall = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);
Bpl.Expr fargs;
- if (coContextDepth > 0 && f is CoPredicate) {
- // F'(args)
- fargs = etran.TrFunctionCallExpr(fexp, coContextDepth);
- // F#canCall(args) && F'(args)
- var fr = Bpl.Expr.And(canCall, fargs);
- splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr));
- } else {
- // F(args)
- fargs = etran.TrExpr(fexp);
- // body
- var trBody = etran.TrExpr(body);
- trBody = etran.CondApplyUnbox(trBody.tok, trBody, f.ResultType, expr.Type);
- // F#canCall(args) && F(args) && (b0 && b1 && b2)
- var fr = Bpl.Expr.And(canCall, BplAnd(fargs, trBody));
- splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr));
- }
+ // F(args)
+ fargs = etran.TrExpr(fexp);
+ // body
+ var trBody = etran.TrExpr(body);
+ trBody = etran.CondApplyUnbox(trBody.tok, trBody, f.ResultType, expr.Type);
+ // F#canCall(args) && F(args) && (b0 && b1 && b2)
+ var fr = Bpl.Expr.And(canCall, BplAnd(fargs, trBody));
+ splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr));
// recurse on body
var ss = new List<SplitExprInfo>();
- TrSplitExpr(body, ss, position, functionHeight, coContextDepth > 0 && f is CoPredicate ? 2 : 0, etran);
+ TrSplitExpr(body, ss, position, functionHeight, null, etran);
foreach (var s in ss) {
if (s.IsChecked) {
var unboxedConjunct = etran.CondApplyUnbox(s.E.tok, s.E, f.ResultType, expr.Type);
@@ -8379,14 +8569,6 @@ namespace Microsoft.Dafny {
return true;
}
}
- // If we get here, then we're in a positive position but the inlining attempt failed. If we just fall through
- // here, then we'll get the ordinary function call (without inlining). But in co-contexts, that's not what we
- // want, because in co-contexts we are supposed to change copredicates into proof certificates about copredicates.
- // So, we do that check here.
- if (f is CoPredicate && coContextDepth > 0) {
- splits.Add(new SplitExprInfo(SplitExprInfo.K.Both, etran.TrFunctionCallExpr(fexp, coContextDepth)));
- return true;
- }
} else if ((position && expr is ForallExpr) || (!position && expr is ExistsExpr)) {
var e = (QuantifierExpr)expr;
@@ -8879,6 +9061,30 @@ namespace Microsoft.Dafny {
return base.Substitute(expr);
}
}
+ public class PrefixCallSubstituter : Substituter
+ {
+ readonly CoPredicate coPred;
+ readonly Expression coDepth;
+ readonly ModuleDefinition module;
+ public PrefixCallSubstituter(Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap, CoPredicate copred, Expression depth)
+ : base(receiverReplacement, substMap) {
+ Contract.Requires(copred != null);
+ Contract.Requires(depth != null);
+ coPred = copred;
+ coDepth = depth;
+ module = copred.EnclosingClass.Module;
+ }
+ public override Expression Substitute(Expression expr) {
+ if (expr is FunctionCallExpr) {
+ var e = (FunctionCallExpr)expr;
+ if (e.Function is CoPredicate && e.Function.EnclosingClass.Module == module &&
+ module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(coPred)) {
+ expr = coPred.CreatePrefixPredicateCall(e, coDepth);
+ }
+ }
+ return base.Substitute(expr);
+ }
+ }
public class Substituter
{
public readonly Expression receiverReplacement;
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 3b0e3ff5..b8e8805a 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -355,6 +355,9 @@ namespace DafnyLanguage
} else {
var formal = (Formal)v;
kind = formal.InParam ? "in-parameter" : "out-parameter";
+ if (formal is ImplicitFormal) {
+ kind = "implicit " + kind;
+ }
}
}
HoverText = string.Format("({2}{3}) {0}: {1}", v.DisplayName, v.Type.TypeName(context), v.IsGhost ? "ghost " : "", kind);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 072339b3..97e7c870 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1342,17 +1342,31 @@ CoResolution.dfy(41,9): Error: a call to a prefix predicate/method in this conte
CoResolution.dfy(42,4): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
13 resolution/type errors detected in CoResolution.dfy
+-------------------- CoPrefix.dfy --------------------
+CoPrefix.dfy(61,7): Error: failure to decrease termination measure
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
+ (0,0): anon6_Then
+CoPrefix.dfy(74,7): Error: failure to decrease termination measure
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
+ (0,0): anon6_Then
+CoPrefix.dfy(114,1): Error BP5003: A postcondition might not hold on this return path.
+CoPrefix.dfy(113,11): Related location: This is the postcondition that might not hold.
+CoPrefix.dfy(101,17): Related location: Related location
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 17 verified, 3 errors
+
-------------------- CoinductiveProofs.dfy --------------------
CoinductiveProofs.dfy(26,12): Error: assertion violation
CoinductiveProofs.dfy(10,17): Related location: Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-CoinductiveProofs.dfy(33,1): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(32,11): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(10,17): Related location: Related location
-Execution trace:
- (0,0): anon0
CoinductiveProofs.dfy(56,1): Error BP5003: A postcondition might not hold on this return path.
CoinductiveProofs.dfy(55,11): Related location: This is the postcondition that might not hold.
CoinductiveProofs.dfy(51,3): Related location: Related location
@@ -1380,16 +1394,14 @@ Execution trace:
(0,0): anon0
CoinductiveProofs.dfy(147,1): Error BP5003: A postcondition might not hold on this return path.
CoinductiveProofs.dfy(146,22): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(1,24): Related location: Related location
Execution trace:
(0,0): anon0
CoinductiveProofs.dfy(153,1): Error BP5003: A postcondition might not hold on this return path.
CoinductiveProofs.dfy(152,22): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(1,24): Related location: Related location
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 31 verified, 9 errors
+Dafny program verifier finished with 32 verified, 8 errors
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy
new file mode 100644
index 00000000..09dd2cc5
--- /dev/null
+++ b/Test/dafny0/CoPrefix.dfy
@@ -0,0 +1,115 @@
+// ----- Stream
+
+codatatype Stream = Nil | Cons(head: int, tail: Stream);
+
+function append(M: Stream, N: Stream): Stream
+{
+ match M
+ case Nil => N
+ case Cons(t, M') => Cons(t, append(M', N))
+}
+
+function zeros(): Stream
+{
+ Cons(0, zeros())
+}
+
+function ones(): Stream
+{
+ Cons(1, ones())
+}
+
+copredicate atmost(a: Stream, b: Stream)
+{
+ match a
+ case Nil => true
+ case Cons(h,t) => b.Cons? && h <= b.head && atmost(t, b.tail)
+}
+
+comethod Theorem0()
+ ensures atmost(zeros(), ones());
+{
+ // the following shows two equivalent ways to getting essentially the
+ // co-inductive hypothesis
+ if (*) {
+ Theorem0#[_k-1]();
+ } else {
+ Theorem0();
+ }
+}
+
+ghost method Theorem0_Manual()
+ ensures atmost(zeros(), ones());
+{
+ parallel (k: nat) {
+ Theorem0_Lemma(k);
+ }
+ assume (forall k: nat :: atmost#[k](zeros(), ones())) ==> atmost(zeros(), ones());
+}
+
+datatype Natural = Zero | Succ(Natural);
+
+comethod Theorem0_TerminationFailure_ExplicitDecreases(y: Natural)
+ ensures atmost(zeros(), ones());
+ decreases y;
+{
+ match (y) {
+ case Succ(x) =>
+ // this is just to show that the decreases clause does kick in
+ Theorem0_TerminationFailure_ExplicitDecreases#[_k](x);
+ case Zero =>
+ Theorem0_TerminationFailure_ExplicitDecreases#[_k](y); // error: failure to terminate
+ }
+ Theorem0_TerminationFailure_ExplicitDecreases#[_k-1](y);
+}
+
+comethod Theorem0_TerminationFailure_DefaultDecreases(y: Natural)
+ ensures atmost(zeros(), ones());
+{
+ match (y) {
+ case Succ(yy) =>
+ // this is just to show that the decreases clause does kick in
+ Theorem0_TerminationFailure_DefaultDecreases#[_k](yy);
+ case Zero =>
+ Theorem0_TerminationFailure_DefaultDecreases#[_k](y); // error: failure to terminate
+ }
+ Theorem0_TerminationFailure_DefaultDecreases#[_k-1](y);
+}
+
+ghost method {:induction true} Theorem0_Lemma(k: nat)
+ ensures atmost#[k](zeros(), ones());
+{
+}
+
+/** SOON
+comethod Theorem1()
+ ensures append(zeros(), ones()) == zeros();
+{
+ Theorem1();
+}
+** SOON */
+
+codatatype IList = ICons(head: int, tail: IList);
+
+function UpIList(n: int): IList
+{
+ ICons(n, UpIList(n+1))
+}
+
+copredicate Pos(s: IList)
+{
+ s.head > 0 && Pos(s.tail)
+}
+
+comethod Theorem2(n: int)
+ requires 1 <= n;
+ ensures Pos(UpIList(n));
+{
+ Theorem2(n+1);
+}
+
+comethod Theorem2_NotAProof(n: int)
+ requires 1 <= n;
+ ensures Pos(UpIList(n));
+{ // error: this is not a proof
+}
diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy
new file mode 100644
index 00000000..233a818b
--- /dev/null
+++ b/Test/dafny0/CoResolution.dfy
@@ -0,0 +1,43 @@
+copredicate P(b: bool)
+{
+ !b && Q(null)
+}
+
+copredicate Q(a: array<int>)
+{
+ a == null && P(true)
+}
+
+//copredicate A() { B() }
+//predicate B() { A() } // error: SCC of a copredicate must include only copredicates
+
+copredicate D()
+ reads this; // error: copredicates are not allowed to have a reads clause -- WHY NOT?
+{
+ true
+}
+
+copredicate S(d: set<int>)
+{
+ this.S#(d) && // error: the call to S# must give an explicit depth argument
+ S#(d) && // error: the call to S# must give an explicit depth argument
+ this.Undeclared#(d) && // error: 'Undeclared#' is undeclared, and depth argument is left implicit
+ this.Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
+ Undeclared#(d) && // error: 'Undeclared#' is undeclared, and depth argument is left implicit
+ Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
+ this.S#[5](d) &&
+ S#[5](d) &&
+ S#(5, d) && // error: the '5' here does not give the depth argument
+ S#[_k](d) // error: _k is not an identifier in scope
+}
+
+comethod CM(d: set<int>)
+{
+ var b;
+ b := this.S#[5](d) && this.S#(d + d); // error: cannot rely on implicit depth argument here
+ b := S#[5](d) && S#(d + d); // error: cannot rely on implicit depth argument here
+ this.CM#[5](d);
+ CM#[5](d);
+ this.CM#(d + d); // error: must give an explicit depth argument
+ CM#(d + d); // error: must give an explicit depth argument
+}
diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy
index c56f9b36..ddb23b5b 100644
--- a/Test/dafny0/CoinductiveProofs.dfy
+++ b/Test/dafny0/CoinductiveProofs.dfy
@@ -23,18 +23,18 @@ comethod PosLemma1(n: int)
{
PosLemma1(n + 1);
if (*) {
- assert Pos(Upward(n + 1)); // error: cannot conclude this here, because we only have a certificate
+ assert Pos(Upward(n + 1)); // error: cannot conclude this here, because we only have prefix predicates
}
}
comethod Outside_CoMethod_Caller_PosLemma(n: int)
requires 1 <= n;
ensures Pos(Upward(n));
-{ // error: this comethod is supposed to produce a certificate, but instead it establishes the real deal
- // (which currently produces a complaint from Dafny)
+{
assert Upward(n).tail == Upward(n + 1); // follows from one unrolling of the definition of Upward
PosLemma0(n + 1);
assert Pos(Upward(n+1)); // this follows directly from the previous line, because it isn't a recursive call
+ // ... and it implies the prefix predicate we're supposed to establish
}
method Outside_Method_Caller_PosLemma(n: int)
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index fd5349f4..82d4bebd 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -18,7 +18,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy
TypeParameters.dfy Datatypes.dfy
Coinductive.dfy Corecursion.dfy CoResolution.dfy
- CoinductiveProofs.dfy
+ CoPrefix.dfy CoinductiveProofs.dfy
TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy
LoopModifies.dfy Refinement.dfy RefinementErrors.dfy
ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 14:24:04 +0000