-
Notifications
You must be signed in to change notification settings - Fork 256
/
BoogieGenerator.Extremes.cs
341 lines (310 loc) · 25.2 KB
/
BoogieGenerator.Extremes.cs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
using System;
using System.Collections.Generic;
using System.Linq;
using System.Numerics;
using System.Diagnostics.Contracts;
using System.IO;
using System.Reflection;
using System.Security.Cryptography;
using Bpl = Microsoft.Boogie;
using BplParser = Microsoft.Boogie.Parser;
using System.Text;
using System.Text.RegularExpressions;
using System.Threading;
using Microsoft.Boogie;
using static Microsoft.Dafny.Util;
using Core;
using DafnyCore.Verifier;
using Microsoft.BaseTypes;
using Microsoft.Dafny.Compilers;
using Microsoft.Dafny.Triggers;
using Action = System.Action;
using PODesc = Microsoft.Dafny.ProofObligationDescription;
using static Microsoft.Dafny.GenericErrors;
namespace Microsoft.Dafny;
public partial class BoogieGenerator {
/// <summary>
/// In the following,
/// if "pp" is a greatest predicate, then QQQ and NNN and HHH and EEE stand for "forall" and "" and "==>" and REVERSE-IMPLIES, and
/// if "pp" is a least predicate, then QQQ and NNN and HHH and EEE stand for "exists" and "!" and "&&" and "==>".
/// ========== For co-predicates:
/// Add the axioms:
/// forall args :: P(args) ==> QQQ k: nat :: P#[k](args)
/// forall args :: (QQQ k: nat :: P#[k](args)) ==> P(args)
/// forall args,k :: k == 0 ==> NNN P#[k](args)
/// where "args" is "heap, formals". In more details:
/// AXIOM_ACTIVATION ==> forall args :: { P(args) } args-have-appropriate-values && P(args) ==> QQQ k { P#[k](args) } :: 0 ATMOST k HHH P#[k](args)
/// AXIOM_ACTIVATION ==> forall args :: { P(args) } args-have-appropriate-values && (QQQ k :: 0 ATMOST k HHH P#[k](args)) ==> P(args)
/// AXIOM_ACTIVATION ==> forall args,k :: args-have-appropriate-values && k == 0 ==> NNN P#0#[k](args)
/// AXIOM_ACTIVATION ==> forall args,k,m :: args-have-appropriate-values && 0 ATMOST k LESS m ==> (P#[k](args) EEE P#[m](args)) (*)
/// where
/// AXIOM_ACTIVATION
/// means:
/// mh LESS ModuleContextHeight ||
/// (mh == ModuleContextHeight && fh ATMOST FunctionContextHeight)
/// There is also a specialized version of (*) for least predicates.
/// </summary>
void AddPrefixPredicateAxioms(PrefixPredicate pp) {
Contract.Requires(pp != null);
Contract.Requires(predef != null);
var co = pp.ExtremePred;
var tok = pp.tok;
var etran = new ExpressionTranslator(this, predef, tok);
var tyvars = MkTyParamBinders(GetTypeParams(pp), out var tyexprs);
var bvs = new List<Variable>(tyvars);
var coArgs = new List<Bpl.Expr>(tyexprs);
var prefixArgs = new List<Bpl.Expr>(tyexprs);
var prefixArgsLimited = new List<Bpl.Expr>(tyexprs);
var prefixArgsLimitedM = new List<Bpl.Expr>(tyexprs);
if (pp.IsFuelAware()) {
var sV = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$ly", predef.LayerType));
var s = new Bpl.IdentifierExpr(tok, sV);
var succS = FunctionCall(tok, BuiltinFunction.LayerSucc, null, s);
bvs.Add(sV);
coArgs.Add(succS);
prefixArgs.Add(succS);
prefixArgsLimited.Add(s);
prefixArgsLimitedM.Add(s);
}
Bpl.Expr h;
if (pp.ReadsHeap) {
var heapIdent = new Bpl.TypedIdent(tok, predef.HeapVarName, predef.HeapType);
var bv = new Bpl.BoundVariable(tok, heapIdent);
h = new Bpl.IdentifierExpr(tok, bv);
bvs.Add(bv);
coArgs.Add(h);
prefixArgs.Add(h);
prefixArgsLimited.Add(h);
prefixArgsLimitedM.Add(h);
} else {
h = null;
}
// ante: $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
Bpl.Expr ante = h != null
? FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr)
: (Bpl.Expr)Bpl.Expr.True;
if (!pp.IsStatic) {
var bvThis = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, etran.This, TrReceiverType(pp)));
bvs.Add(bvThis);
var bvThisIdExpr = new Bpl.IdentifierExpr(tok, bvThis);
coArgs.Add(bvThisIdExpr);
prefixArgs.Add(bvThisIdExpr);
prefixArgsLimited.Add(bvThisIdExpr);
prefixArgsLimitedM.Add(bvThisIdExpr);
// add well-typedness conjunct to antecedent
Type thisType = ModuleResolver.GetReceiverType(tok, pp);
Bpl.Expr wh = Bpl.Expr.And(
ReceiverNotNull(bvThisIdExpr),
GetWhereClause(tok, bvThisIdExpr, thisType, etran, NOALLOC));
ante = Bpl.Expr.And(ante, wh);
}
Bpl.Expr kWhere = null, kId = null, mId = null;
Bpl.Variable k = null;
Bpl.Variable m = null;
// DR: Changed to add the pp formals instead of co (since types would otherwise be wrong)
// Note that k is not added to bvs or coArgs.
foreach (var p in pp.Formals) {
bool is_k = p == pp.Formals[0];
var bv = new Bpl.BoundVariable(p.tok,
new Bpl.TypedIdent(p.tok, p.AssignUniqueName(pp.IdGenerator), TrType(p.Type)));
var formal = new Bpl.IdentifierExpr(p.tok, bv);
if (!is_k) {
coArgs.Add(formal);
}
prefixArgs.Add(formal);
prefixArgsLimited.Add(formal);
if (is_k) {
m = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, "_m", TrType(p.Type)));
mId = new Bpl.IdentifierExpr(m.tok, m);
prefixArgsLimitedM.Add(mId);
} else {
prefixArgsLimitedM.Add(formal);
}
var wh = GetWhereClause(p.tok, formal, p.Type, etran, NOALLOC);
if (is_k) {
// add the formal _k
k = bv;
kId = formal;
kWhere = wh;
} else {
bvs.Add(bv);
if (wh != null) {
// add well-typedness conjunct to antecedent
ante = Bpl.Expr.And(ante, wh);
}
}
}
Contract.Assert(k != null && m != null); // the loop should have filled these in
var funcID = new Bpl.IdentifierExpr(tok, co.FullSanitizedName, TrType(co.ResultType));
var coAppl = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), coArgs);
funcID = new Bpl.IdentifierExpr(tok, pp.FullSanitizedName, TrType(pp.ResultType));
var prefixAppl = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), prefixArgs);
var activation = AxiomActivation(pp, etran);
// forall args :: { P(args) } args-have-appropriate-values && P(args) ==> QQQ k { P#[k](args) } :: 0 ATMOST k HHH P#[k](args)
var tr = BplTrigger(prefixAppl);
var qqqK = pp.ExtremePred is GreatestPredicate
? (Bpl.Expr)new Bpl.ForallExpr(tok, new List<Variable> { k }, tr,
kWhere == null ? prefixAppl : BplImp(kWhere, prefixAppl))
: (Bpl.Expr)new Bpl.ExistsExpr(tok, new List<Variable> { k }, tr,
kWhere == null ? prefixAppl : BplAnd(kWhere, prefixAppl));
tr = BplTriggerHeap(this, tok, coAppl, pp.ReadsHeap ? null : h);
var allS = new Bpl.ForallExpr(tok, bvs, tr, BplImp(BplAnd(ante, coAppl), qqqK));
sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, Bpl.Expr.Imp(activation, allS),
"1st prefix predicate axiom for " + pp.FullSanitizedName));
// forall args :: { P(args) } args-have-appropriate-values && (QQQ k :: 0 ATMOST k HHH P#[k](args)) ==> P(args)
allS = new Bpl.ForallExpr(tok, bvs, tr, BplImp(BplAnd(ante, qqqK), coAppl));
sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, Bpl.Expr.Imp(activation, allS),
"2nd prefix predicate axiom"));
// forall args,k :: args-have-appropriate-values && k == 0 ==> NNN P#0#[k](args)
var moreBvs = new List<Variable>();
moreBvs.AddRange(bvs);
moreBvs.Add(k);
var z = Bpl.Expr.Eq(kId,
pp.Formals[0].Type.IsBigOrdinalType
? (Bpl.Expr)FunctionCall(tok, "ORD#FromNat", predef.BigOrdinalType, Bpl.Expr.Literal(0))
: Bpl.Expr.Literal(0));
funcID = new Bpl.IdentifierExpr(tok, pp.FullSanitizedName, TrType(pp.ResultType));
Bpl.Expr prefixLimitedBody = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), prefixArgsLimited);
Bpl.Expr prefixLimited = pp.ExtremePred is LeastPredicate ? Bpl.Expr.Not(prefixLimitedBody) : prefixLimitedBody;
var trigger = BplTriggerHeap(this, prefixLimitedBody.tok, prefixLimitedBody, pp.ReadsHeap ? null : h);
var trueAtZero = new Bpl.ForallExpr(tok, moreBvs, trigger, BplImp(BplAnd(ante, z), prefixLimited));
sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, Bpl.Expr.Imp(activation, trueAtZero),
"3rd prefix predicate axiom"));
#if WILLING_TO_TAKE_THE_PERFORMANCE_HIT
// forall args,k,m :: args-have-appropriate-values && 0 <= k <= m ==> (P#[k](args) EEE P#[m](args))
moreBvs = new List<Variable>();
moreBvs.AddRange(bvs);
moreBvs.Add(k);
moreBvs.Add(m);
Bpl.Expr smaller;
if (kId.Type.IsInt) {
smaller = BplAnd(Bpl.Expr.Le(Bpl.Expr.Literal(0), kId), Bpl.Expr.Lt(kId, mId));
} else {
smaller = FunctionCall(tok, "ORD#Less", Bpl.Type.Bool, kId, mId);
}
funcID = new Bpl.IdentifierExpr(tok, pp.FullSanitizedName, TrType(pp.ResultType));
var prefixPred_K = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), prefixArgsLimited);
var prefixPred_M = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), prefixArgsLimitedM);
var direction =
pp.ExtremePred is LeastPredicate ? BplImp(prefixPred_K, prefixPred_M) : BplImp(prefixPred_M, prefixPred_K);
var trigger2 = new Bpl.Trigger(tok, true, new List<Bpl.Expr> { prefixPred_K, prefixPred_M });
var monotonicity = new Bpl.ForallExpr(tok, moreBvs, trigger2, BplImp(smaller, direction));
AddRootAxiom(new Bpl.Axiom(tok, Bpl.Expr.Imp(activation, monotonicity),
"prefix predicate monotonicity axiom"));
#endif
// A more targeted monotonicity axiom used to increase the power of automation for proving the limit case for
// least predicates that have more than one focal-predicate term.
if (pp.ExtremePred is LeastPredicate && pp.Formals[0].Type.IsBigOrdinalType) {
// forall args,k,m,limit ::
// { P#[k](args), ORD#LessThanLimit(k,limit), ORD#LessThanLimit(m,limit) }
// args-have-appropriate-values && k < m && P#[k](args) ==> P#[m](args))
var limit = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "_limit", TrType(Type.BigOrdinal)));
var limitId = new Bpl.IdentifierExpr(limit.tok, limit);
moreBvs = new List<Variable>();
moreBvs.AddRange(bvs);
moreBvs.Add(k);
moreBvs.Add(m);
moreBvs.Add(limit);
var kLessLimit = FunctionCall(tok, "ORD#LessThanLimit", Bpl.Type.Bool, kId, limitId);
var mLessLimit = FunctionCall(tok, "ORD#LessThanLimit", Bpl.Type.Bool, mId, limitId);
var kLessM = FunctionCall(tok, "ORD#Less", Bpl.Type.Bool, kId, mId);
funcID = new Bpl.IdentifierExpr(tok, pp.FullSanitizedName, TrType(pp.ResultType));
var prefixPred_K = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), prefixArgsLimited);
var prefixPred_M = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), prefixArgsLimitedM);
var direction = BplImp(prefixPred_K, prefixPred_M);
var trigger3 = new Bpl.Trigger(tok, true, new List<Bpl.Expr> { prefixPred_K, kLessLimit, mLessLimit });
var monotonicity = new Bpl.ForallExpr(tok, moreBvs, trigger3, BplImp(kLessM, direction));
sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, Bpl.Expr.Imp(activation, monotonicity),
"targeted prefix predicate monotonicity axiom"));
}
}
/// <summary>
/// For an extreme predicate P, "pp" is the prefix predicate for P (such that P = pp.ExtremePred) and
/// "body" is the body of P. Return what would be the body of the prefix predicate pp.
/// In particular, return
/// #if _k has type nat:
/// 0 LESS _k IMPLIES body' // for greatest predicates
/// 0 LESS _k AND body' // for least predicates
/// #elsif _k has type ORDINAL:
/// (0 LESS ORD#Offset(_k) IMPLIES body') AND
/// (0 == ORD#Offset(_k) IMPLIES forall _k':ORDINAL :: _k' LESS _k ==> pp(_k', args)) // for greatest predicates
/// (0 == ORD#Offset(_k) IMPLIES exists _k':ORDINAL :: _k' LESS _k && pp(_k', args)) // for least predicates
/// #endif
/// where body' is body with the formals of P replaced by the corresponding
/// formals of pp and with self-calls P(s) replaced by recursive calls to
/// pp(_k - 1, s).
/// </summary>
Expression PrefixSubstitution(PrefixPredicate pp, Expression body) {
Contract.Requires(pp != null);
var typeMap = Util.Dict<TypeParameter, Type>(pp.ExtremePred.TypeArgs, Map(pp.TypeArgs, x => new UserDefinedType(x)));
var paramMap = new Dictionary<IVariable, Expression>();
for (int i = 0; i < pp.ExtremePred.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.ExtremePred.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
Expression kMinusOne = Expression.CreateSubtract(k, Expression.CreateNatLiteral(pp.tok, 1, pp.K.Type));
var s = new PrefixCallSubstituter(null, paramMap, typeMap, pp.ExtremePred, kMinusOne);
body = s.Substitute(body);
if (pp.K.Type.IsBigOrdinalType) {
// 0 < k.Offset
Contract.Assume(program.SystemModuleManager.ORDINAL_Offset != null); // should have been filled in by the resolver
var kOffset = new MemberSelectExpr(pp.tok, k, program.SystemModuleManager.ORDINAL_Offset);
var kIsPositive = Expression.CreateLess(Expression.CreateIntLiteral(pp.tok, 0), kOffset);
var kIsLimit = Expression.CreateEq(Expression.CreateIntLiteral(pp.tok, 0), kOffset, Type.Int);
var kprimeVar = new BoundVar(pp.tok, "_k'", Type.BigOrdinal);
var kprime = new IdentifierExpr(pp.tok, kprimeVar);
var substMap = new Dictionary<IVariable, Expression>();
substMap.Add(pp.K, kprime);
Expression recursiveCallReceiver;
List<Expression> recursiveCallArgs;
pp.RecursiveCallParameters(pp.tok, pp.TypeArgs, pp.Formals, null, substMap, out recursiveCallReceiver, out recursiveCallArgs);
var ppCall = new FunctionCallExpr(pp.tok, pp.Name, recursiveCallReceiver, pp.tok, pp.tok, recursiveCallArgs);
ppCall.Function = pp;
ppCall.Type = Type.Bool;
ppCall.TypeApplication_AtEnclosingClass = pp.EnclosingClass.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp));
ppCall.TypeApplication_JustFunction = pp.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp));
Attributes triggerAttr = new Attributes("trigger", new List<Expression> { ppCall }, null);
Expression limitCalls;
if (pp.ExtremePred is GreatestPredicate) {
// forall k':ORDINAL | _k' LESS _k :: pp(_k', args)
var smaller = Expression.CreateLess(kprime, k);
limitCalls = new ForallExpr(pp.tok, pp.RangeToken, new List<BoundVar> { kprimeVar }, smaller, ppCall, triggerAttr) {
Type = Type.Bool,
Bounds = new List<ComprehensionExpr.BoundedPool>() { new ComprehensionExpr.AllocFreeBoundedPool(kprimeVar.Type) }
};
} else {
// exists k':ORDINAL | _k' LESS _k :: pp(_k', args)
// Here, instead of using the usual ORD#Less, we use the semantically equivalent ORD#LessThanLimit, because this
// allows us to write a good trigger for a targeted monotonicity axiom. That axiom, in turn, makes the
// automatic verification more powerful for least lemmas that have more than one focal-predicate term.
var smaller = new BinaryExpr(kprime.tok, BinaryExpr.Opcode.Lt, kprime, k) {
ResolvedOp = BinaryExpr.ResolvedOpcode.LessThanLimit,
Type = Type.Bool
};
limitCalls = new ExistsExpr(pp.tok, pp.RangeToken, new List<BoundVar> { kprimeVar }, smaller, ppCall, triggerAttr) {
Type = Type.Bool,
Bounds = new List<ComprehensionExpr.BoundedPool>() { new ComprehensionExpr.AllocFreeBoundedPool(kprimeVar.Type) }
};
}
var a = Expression.CreateImplies(kIsPositive, body);
var b = Expression.CreateImplies(kIsLimit, limitCalls);
return Expression.CreateAnd(a, b);
} else {
// 0 < k
var kIsPositive = Expression.CreateLess(Expression.CreateIntLiteral(pp.tok, 0), k);
if (pp.ExtremePred is GreatestPredicate) {
// add antecedent "0 < _k ==>"
return Expression.CreateImplies(kIsPositive, body);
} else {
// add initial conjunct "0 < _k &&"
return Expression.CreateAnd(kIsPositive, body);
}
}
}
}