Skip to content

Commit

Permalink
feat: Implement frame-related asserted exprs and TraitDecreases (#5542)
Browse files Browse the repository at this point in the history 
Implements `GetAssertedExpr` for Modifiable, ModifyFrameSubset, ReadFrameSubset, TraitFrame, and TraitDecreases.
  • Loading branch information
@alex-chew
alex-chew authored Jun 7, 2024
1 parent a5d600c commit f75ae71
Show file tree
Hide file tree
Showing 15 changed files with 658 additions and 75 deletions.
6 changes: 6 additions & 0 deletions Source/DafnyCore/AST/Members/MethodOrFunction.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,4 +92,10 @@ public void ResolveMethodOrFunction(INewOrOldResolver resolver) {

protected MethodOrFunction(RangeToken tok, Name name, bool hasStaticKeyword, bool isGhost, Attributes attributes, bool isRefining) : base(tok, name, hasStaticKeyword, isGhost, attributes, isRefining) {
}

public Specification<FrameExpression> Reads => this switch {
Method m => m.Reads,
Function f => f.Reads,
_ => throw new cce.UnreachableException()
};
}
133 changes: 105 additions & 28 deletions Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -278,6 +278,8 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
wfOptions = wfOptions.WithLValueContext(false);
}

var readFrames = GetContextReadsFrames();

switch (expr) {
case StaticReceiverExpr stexpr: {
if (stexpr.ObjectToDiscard != null) {
Expand Down Expand Up @@ -374,8 +376,10 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
}
}
if (!origOptions.LValueContext && wfOptions.DoReadsChecks && e.Member is Field { IsMutable: true } f) {
var requiredFrame = new FrameExpression(Token.NoToken, e.Obj, f.Name);
var desc = new PODesc.ReadFrameSubset("read field", requiredFrame, readFrames, selectExpr, etran.scope);
wfOptions.AssertSink(this, builder)(selectExpr.tok, Bpl.Expr.SelectTok(selectExpr.tok, etran.ReadsFrame(selectExpr.tok), etran.TrExpr(e.Obj), GetField(e)),
new PODesc.ReadFrameSubset("read field", selectExpr, etran.scope), wfOptions.AssertKv);
desc, wfOptions.AssertKv);
}

break;
Expand Down Expand Up @@ -429,8 +433,10 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
var i = etran.TrExpr(e.E0);
i = ConvertExpression(selectExpr.tok, i, e.E0.Type, Type.Int);
Bpl.Expr fieldName = FunctionCall(selectExpr.tok, BuiltinFunction.IndexField, null, i);
var requiredFrame = new FrameExpression(Token.NoToken, e.Seq, null);
var desc = new PODesc.ReadFrameSubset("read array element", requiredFrame, readFrames, e, etran.scope);
wfOptions.AssertSink(this, builder)(selectExpr.tok, Bpl.Expr.SelectTok(selectExpr.tok, etran.ReadsFrame(selectExpr.tok), seq, fieldName),
new PODesc.ReadFrameSubset("read array element", e, etran.scope), wfOptions.AssertKv);
desc, wfOptions.AssertKv);
} else {
Bpl.Expr lowerBound = e.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(e.E0);
Contract.Assert(eSeqType.AsArrayType.Dims == 1);
Expand All @@ -443,9 +449,9 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
var allowedToRead = Bpl.Expr.SelectTok(e.tok, etran.ReadsFrame(e.tok), seq, fieldName);
var trigger = BplTrigger(allowedToRead); // Note, the assertion we're about to produce only seems useful in the check-only mode (that is, with subsumption 0), but if it were to be assumed, we'll use this entire RHS as the trigger
var qq = new Bpl.ForallExpr(e.tok, new List<Variable> { iVar }, trigger, BplImp(range, allowedToRead));
wfOptions.AssertSink(this, builder)(selectExpr.tok, qq,
new PODesc.ReadFrameSubset("read the indicated range of array elements", e, etran.scope),
wfOptions.AssertKv);
var requiredFrame = new FrameExpression(Token.NoToken, e.Seq, null);
var desc = new PODesc.ReadFrameSubset("read the indicated range of array elements", requiredFrame, readFrames, e, etran.scope);
wfOptions.AssertSink(this, builder)(selectExpr.tok, qq, desc, wfOptions.AssertKv);
}
}

Expand Down Expand Up @@ -478,8 +484,10 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
}
if (wfOptions.DoReadsChecks) {
Bpl.Expr fieldName = etran.GetArrayIndexFieldName(e.tok, e.Indices);
var requiredFrame = new FrameExpression(Token.NoToken, e.Array, null);
var desc = new PODesc.ReadFrameSubset("read array element", requiredFrame, readFrames, selectExpr, etran.scope);
wfOptions.AssertSink(this, builder)(selectExpr.tok, Bpl.Expr.SelectTok(selectExpr.tok, etran.ReadsFrame(selectExpr.tok), array, fieldName),
new PODesc.ReadFrameSubset("read array element", selectExpr, etran.scope), wfOptions.AssertKv);
desc, wfOptions.AssertKv);
}

break;
Expand Down Expand Up @@ -586,18 +594,19 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
fnCoreType = fnCore.Type;
}

// unwrap renamed local lambdas
var unwrappedFunc = e.Function;
while (unwrappedFunc is ConcreteSyntaxExpression { ResolvedExpression: not null } cse) {
unwrappedFunc = cse.ResolvedExpression;
}
if (unwrappedFunc is IdentifierExpr { tok: var tok, DafnyName: var name }) {
unwrappedFunc = new IdentifierExpr(tok, name);
}

if (!fnCoreType.IsArrowTypeWithoutPreconditions) {
// unwrap renamed local lambdas
var funcExpr = e.Function;
while (funcExpr is ConcreteSyntaxExpression { ResolvedExpression: not null } cse) {
funcExpr = cse.ResolvedExpression;
}
if (funcExpr is IdentifierExpr ie) {
funcExpr = new IdentifierExpr(ie.tok, ie.DafnyName);
}
var dPrecond = new ApplyExpr(
Token.NoToken,
new ExprDotName(Token.NoToken, funcExpr, "requires", null),
new ExprDotName(Token.NoToken, unwrappedFunc, "requires", null),
e.Args,
Token.NoToken);

Expand All @@ -612,9 +621,20 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
Expression wrap = new BoogieWrapper(
FunctionCall(e.tok, Reads(arity), TrType(objset), args),
objset);
var reads = new FrameExpression(e.tok, wrap, null);
CheckFrameSubset(applyExpr.tok, new List<FrameExpression> { reads }, null, null,
etran, etran.ReadsFrame(applyExpr.tok), wfOptions.AssertSink(this, builder), new PODesc.ReadFrameSubset("invoke function"), wfOptions.AssertKv);
var wrappedReads = new FrameExpression(e.tok, wrap, null);

var readsCall = new ApplyExpr(
Token.NoToken,
new ExprDotName(Token.NoToken, unwrappedFunc, "reads", null),
e.Args,
Token.NoToken
);
readsCall.Type = objset;
var requiredFrame = new FrameExpression(Token.NoToken, readsCall, null);
var desc = new PODesc.ReadFrameSubset("invoke function", requiredFrame, readFrames);

CheckFrameSubset(applyExpr.tok, new List<FrameExpression> { wrappedReads }, null, null,
etran, etran.ReadsFrame(applyExpr.tok), wfOptions.AssertSink(this, builder), desc, wfOptions.AssertKv);
}

break;
Expand Down Expand Up @@ -753,8 +773,32 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
FunctionCall(expr.tok, Reads(e.Args.Count()), TrType(objset), arguments),
objset);
var reads = new FrameExpression(expr.tok, wrap, null);
List<FrameExpression> requiredFrames;
switch (e.Receiver.Resolved) {
case MemberSelectExpr { Member: MethodOrFunction readsReceiver }: {
var receiverReplacement = readsReceiver.IsStatic
? null
: new ThisExpr(readsReceiver);
var receiverSubstMap = readsReceiver.Ins.Zip(e.Args)
.ToDictionary(fa => fa.First as IVariable, fa => fa.Second);
var subst = new Substituter(receiverReplacement, receiverSubstMap, e.GetTypeArgumentSubstitutions());
requiredFrames = readsReceiver.Reads.Expressions.ConvertAll(subst.SubstFrameExpr);
break;
}
default:
var readsCall = new ApplyExpr(
Token.NoToken,
new ExprDotName(Token.NoToken, e.Receiver.Resolved, "reads", null),
e.Args,
Token.NoToken
);
readsCall.Type = objset;
requiredFrames = new() { new FrameExpression(Token.NoToken, readsCall, null) };
break;
}
var desc = new PODesc.ReadFrameSubset("invoke function", requiredFrames, readFrames);
CheckFrameSubset(expr.tok, new List<FrameExpression> { reads }, null, null,
etran, etran.ReadsFrame(expr.tok), wfOptions.AssertSink(this, builder), new PODesc.ReadFrameSubset("invoke function"), wfOptions.AssertKv);
etran, etran.ReadsFrame(expr.tok), wfOptions.AssertSink(this, builder), desc, wfOptions.AssertKv);
}

} else {
Expand Down Expand Up @@ -786,10 +830,16 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
}
if (wfOptions.DoReadsChecks) {
// check that the callee reads only what the caller is already allowed to read
var s = new Substituter(null, new Dictionary<IVariable, Expression>(), e.GetTypeArgumentSubstitutions());

// substitute actual args for parameters in description expression frames...
var requiredFrames = e.Function.Reads.Expressions.ConvertAll(directSub.SubstFrameExpr);
var desc = new PODesc.ReadFrameSubset("invoke function", requiredFrames, readFrames);

// ... but that substitution isn't needed for frames passed to CheckFrameSubset
var readsSubst = new Substituter(null, new Dictionary<IVariable, Expression>(), e.GetTypeArgumentSubstitutions());
CheckFrameSubset(callExpr.tok,
e.Function.Reads.Expressions.ConvertAll(s.SubstFrameExpr),
e.Receiver, substMap, etran, etran.ReadsFrame(callExpr.tok), wfOptions.AssertSink(this, builder), new PODesc.ReadFrameSubset("invoke function"), wfOptions.AssertKv);
e.Function.Reads.Expressions.ConvertAll(readsSubst.SubstFrameExpr),
e.Receiver, substMap, etran, etran.ReadsFrame(callExpr.tok), wfOptions.AssertSink(this, builder), desc, wfOptions.AssertKv);
}
}
Expression allowance = null;
Expand Down Expand Up @@ -889,6 +939,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
}
case UnchangedExpr unchangedExpr: {
var e = unchangedExpr;
var contextReadsFrames = GetContextReadsFrames();
foreach (var fe in e.Frame) {
CheckWellformed(fe.E, wfOptions, locals, builder, etran);

Expand All @@ -910,10 +961,11 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
}
// check that the 'unchanged' argument reads only what the context is allowed to read
if (wfOptions.DoReadsChecks) {
var desc = new PODesc.ReadFrameSubset($"read state of 'unchanged' {description}", fe, contextReadsFrames);
CheckFrameSubset(fe.E.tok,
new List<FrameExpression>() { fe },
null, new Dictionary<IVariable, Expression>(), etran, etran.ReadsFrame(fe.E.tok), wfOptions.AssertSink(this, builder),
new PODesc.ReadFrameSubset($"read state of 'unchanged' {description}"), wfOptions.AssertKv);
desc, wfOptions.AssertKv);
}
}

Expand Down Expand Up @@ -1567,9 +1619,17 @@ private void CheckElementInit(IToken tok, bool forArray, List<Expression> dims,
// check precond
var pre = FunctionCall(tok, Requires(dims.Count), Bpl.Type.Bool, args);
var q = new Bpl.ForallExpr(tok, bvs, BplImp(ante, pre));
var desc = new PODesc.IndicesInDomain(forArray ? "array" : "sequence", dims, init);
builder.Add(AssertNS(tok, q, desc));
var indicesDesc = new PODesc.IndicesInDomain(forArray ? "array" : "sequence", dims, init);
builder.Add(AssertNS(tok, q, indicesDesc));
if (!forArray && options.DoReadsChecks) {
// unwrap renamed local lambdas
var unwrappedFunc = init;
while (unwrappedFunc is ConcreteSyntaxExpression { ResolvedExpression: not null } cse) {
unwrappedFunc = cse.ResolvedExpression;
}
if (unwrappedFunc is IdentifierExpr { tok: var initTok, DafnyName: var name }) {
unwrappedFunc = new IdentifierExpr(initTok, name);
}
// check read effects
Type objset = program.SystemModuleManager.ObjectSetType();
Expression wrap = new BoogieWrapper(
Expand All @@ -1580,10 +1640,27 @@ private void CheckElementInit(IToken tok, bool forArray, List<Expression> dims,
var qe = new Bpl.ForallExpr(t, bvs, BplImp(ante, e));
options.AssertSink(this, builder)(t, qe, d, qk);
};

PODesc.Utils.MakeQuantifierVarsForDims(dims, out var indexVars, out var indexVarExprs, out var indicesRange);
var readsCall = new ApplyExpr(
Token.NoToken,
new ExprDotName(Token.NoToken, unwrappedFunc, "reads", null),
indexVarExprs,
Token.NoToken
);
readsCall.Type = objset;
var contextReads = GetContextReadsFrames();
var readsDescExpr = new ForallExpr(
Token.NoToken,
RangeToken.NoToken,
indexVars,
indicesRange,
PODesc.Utils.MakeDafnyFrameCheck(contextReads, readsCall, null),
null
);
var readsDesc = new PODesc.ReadFrameSubset("invoke the function passed as an argument to the sequence constructor", readsDescExpr);
CheckFrameSubset(tok, new List<FrameExpression> { reads }, null, null,
etran, etran.ReadsFrame(tok), maker,
new PODesc.ReadFrameSubset("invoke the function passed as an argument to the sequence constructor"),
options.AssertKv);
etran, etran.ReadsFrame(tok), maker, 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);
Expand Down
15 changes: 10 additions & 5 deletions Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1182,7 +1182,7 @@ private void AddFunctionOverrideSubsetChk(Function func, BoogieStmtListBuilder b
Bpl.Expr consequent2 = InRWClause(tok, o, f, traitFrameExps, etran, null, null);
Bpl.Expr q = new Bpl.ForallExpr(tok, new List<TypeVariable>(), new List<Variable> { oVar, fVar },
BplImp(BplAnd(ante, oInCallee), consequent2));
builder.Add(Assert(tok, q, new PODesc.TraitFrame(func.WhatKind, false), kv));
builder.Add(Assert(tok, q, new PODesc.TraitFrame(func.WhatKind, false, func.Reads.Expressions, traitFrameExps), kv));
}

private void AddFunctionOverrideReqsChk(Function f, BoogieStmtListBuilder builder, ExpressionTranslator etran,
Expand Down Expand Up @@ -1517,11 +1517,10 @@ private void AddOverrideTerminationChk(ICallable original, ICallable overryd, Bo
var caller = new List<Expr>();
var calleeDafny = new List<Expression>();
var callerDafny = new List<Expression>();
FunctionCallSubstituter sub = null;
FunctionCallSubstituter sub = new FunctionCallSubstituter(substMap, typeMap, T, I);

for (int i = 0; i < N; i++) {
Expression e0 = calleeDecreases[i];
sub ??= new FunctionCallSubstituter(substMap, typeMap, T, I);
Expression e1 = sub.Substitute(contextDecreases[i]);
if (!CompatibleDecreasesTypes(e0.Type, e1.Type)) {
N = i;
Expand Down Expand Up @@ -1565,7 +1564,13 @@ private void AddOverrideTerminationChk(ICallable original, ICallable overryd, Bo
bool allowNoChange = N == decrCountT && decrCountT <= decrCountC;
var decrChk = DecreasesCheck(toks, null, calleeDafny, callerDafny, callee, caller, null,
null, allowNoChange, false);
builder.Add(Assert(original.RangeToken, decrChk, new PODesc.TraitDecreases(original.WhatKind)));
var assertedExpr = new DecreasesToExpr(
Token.NoToken,
contextDecreases.Select(sub.Substitute).ToList(),
calleeDecreases,
true);
var desc = new PODesc.TraitDecreases(original.WhatKind, assertedExpr);
builder.Add(Assert(original.RangeToken, decrChk, desc));
}

private void AddMethodOverrideFrameSubsetChk(Method m, bool isModifies, BoogieStmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables,
Expand Down Expand Up @@ -1610,7 +1615,7 @@ private void AddMethodOverrideFrameSubsetChk(Method m, bool isModifies, BoogieSt
var consequent2 = InRWClause(tok, o, f, traitFrameExps, etran, null, null);
var q = new Boogie.ForallExpr(tok, new List<TypeVariable>(), new List<Variable> { oVar, fVar },
BplImp(BplAnd(ante, oInCallee), consequent2));
builder.Add(Assert(m.RangeToken, q, new PODesc.TraitFrame(m.WhatKind, isModifies), kv));
builder.Add(Assert(m.RangeToken, q, new PODesc.TraitFrame(m.WhatKind, isModifies, classFrameExps, traitFrameExps), kv));
}

// Return a way to know if an assertion should be converted to an assumption
Expand Down
Loading

0 comments on commit f75ae71

Please sign in to comment.