Skip to content

Commit

Permalink
fix: Override checks with canCall precondition (#3479)
Browse files Browse the repository at this point in the history 
We strengthen this check by performing it on the visibility level of the
implementing function, but restricting the enabled axiom to the callers
of the trait. To achieve this, we add the canCall precondition to the
axiom. Additionally, we consider imported trait functions when computing
the visibility levels.

Fixes #2500.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
@fabiomadge
fabiomadge authored Feb 25, 2023
1 parent 6a2badc commit 993b589
Show file tree
Hide file tree
Showing 19 changed files with 247 additions and 168 deletions.
6 changes: 3 additions & 3 deletions Source/DafnyCore/Compilers/Java/Compiler-java.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1801,8 +1801,8 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) {
wr.Write($"public static{justTypeArgs} {DtT_protected} {DtCreateName(ctor)}(");
WriteFormals("", ctor.Formals, wr);
var w = wr.NewBlock(")");
w.Write($"return new {DtCtorDeclarationName(ctor, dt.TypeArgs)}({ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});");
wr.NewBlock(")")
.WriteLine($"return new {DtCtorDeclarationName(ctor, dt.TypeArgs)}({ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});");
}

if (dt.IsRecordType) {
Expand All @@ -1813,7 +1813,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
wr.Write($"public static{justTypeArgs} {DtT_protected} create_{ctor.CompileName}(");
WriteFormals("", ctor.Formals, wr);
wr.NewBlock(")")
.Write($"return create({ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});");
.WriteLine($"return create({ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});");
}

// query properties
Expand Down
3 changes: 3 additions & 0 deletions Source/DafnyCore/Resolver/CallGraphBuilder.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -295,6 +295,9 @@ public static void AddCallGraphEdge(IASTVisitorContext callingContext, ICallable
ModuleDefinition calleeModule = callable is SpecialFunction ? null : callable.EnclosingModule;
if (callerModule != calleeModule) {
// inter-module call; don't record in call graph
if (callingContext is ICallable context && callable is Function { EnclosingClass: TraitDecl }) {
callerModule.CallGraph.AddEdge(context, callable);
}
return;
}

Expand Down
46 changes: 27 additions & 19 deletions Source/DafnyCore/Verifier/FunctionCallSubstituter.cs
View file
Original file line number Diff line number Diff line change
@@ -1,30 +1,38 @@
using System.Collections.Generic;
using System.Linq;

namespace Microsoft.Dafny {
public class FunctionCallSubstituter : Substituter {
public readonly Function A, B;
public FunctionCallSubstituter(Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap, Function a, Function b)
: base(receiverReplacement, substMap, new Dictionary<TypeParameter, Type>()) {
A = a;
B = b;
public readonly TraitDecl Tr;
public readonly ClassDecl Cl;

// We replace all occurrences of the trait version of the function with the class version. This is only allowed if
// the receiver is `this`. We underapproximate this by looking for a `ThisExpr`, which misses more complex
// expressions that evaluate to one.
public FunctionCallSubstituter(Dictionary<IVariable, Expression/*!*/>/*!*/ substMap, Dictionary<TypeParameter, Type> typeMap, TraitDecl Tr, ClassDecl Cl)
: base(null, substMap, typeMap) {
this.Tr = Tr;
this.Cl = Cl;
}

public override Expression Substitute(Expression expr) {
if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
Expression receiver = Substitute(e.Receiver);
List<Expression> newArgs = SubstituteExprList(e.Args);
FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, e.CloseParen, newArgs, e.AtLabel);
if (e.Function == A) {
newFce.Function = B;
newFce.Type = e.Type; // TODO: this may not work with type parameters.
if (expr is FunctionCallExpr e) {
var receiver = Substitute(e.Receiver);
var newArgs = SubstituteExprList(e.Args);
Function function;
if ((e.Function.EnclosingClass == Tr || Tr.InheritedMembers.Contains(e.Function)) && e.Receiver is ThisExpr && receiver is ThisExpr && Cl.Members.Find(m => m.OverriddenMember == e.Function) is { } f) {
receiver = new ThisExpr((TopLevelDeclWithMembers)f.EnclosingClass);
function = (Function)f;
} else {
newFce.Function = e.Function;
newFce.Type = e.Type;
function = e.Function;
}
newFce.TypeApplication_AtEnclosingClass = e.TypeApplication_AtEnclosingClass; // resolve here
newFce.TypeApplication_JustFunction = e.TypeApplication_JustFunction; // resolve here
newFce.IsByMethodCall = e.IsByMethodCall;
return newFce;
return new FunctionCallExpr(e.tok, e.Name, receiver, e.OpenParen, e.CloseParen, newArgs, e.AtLabel) {
Function = function,
Type = e.Type, // TODO: this may not work with type parameters.
TypeApplication_AtEnclosingClass = SubstituteTypeList(e.TypeApplication_AtEnclosingClass), // resolve here
TypeApplication_JustFunction = SubstituteTypeList(e.TypeApplication_JustFunction), // resolve here
IsByMethodCall = e.IsByMethodCall
};
}
return base.Substitute(expr);
}
Expand Down
101 changes: 54 additions & 47 deletions Source/DafnyCore/Verifier/Translator.ClassMembers.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -173,7 +173,7 @@ void AddMethod_Top(Method m, bool isByMethod, bool includeAllMethods) {
AddMethodImpl(m, proc, true);
}
}
if (m.OverriddenMethod != null && InVerificationScope(m)) //method has overrided a parent method
if (m.OverriddenMethod != null && InVerificationScope(m)) //method has overridden a parent method
{
var procOverrideChk = AddMethod(m, MethodTranslationKind.OverrideCheck);
sink.AddTopLevelDeclaration(procOverrideChk);
Expand Down Expand Up @@ -877,8 +877,8 @@ private void AddFunctionOverrideCheckImpl(Function f) {
}
// the procedure itself
var req = new List<Boogie.Requires>();
// free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
req.Add(Requires(f.tok, true, etran.HeightContext(f.OverriddenFunction), null, null));
// free requires fh == FunctionContextHeight;
req.Add(Requires(f.tok, true, etran.HeightContext(f), null, null));
if (f is TwoStateFunction) {
// free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap)
var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr);
Expand Down Expand Up @@ -920,18 +920,16 @@ private void AddFunctionOverrideCheckImpl(Function f) {
}

var substMap = new Dictionary<IVariable, Expression>();
for (int i = 0; i < f.Formals.Count; i++) {
//get corresponsing formal in the class
var ie = new IdentifierExpr(f.Formals[i].tok, f.Formals[i].AssignUniqueName(f.IdGenerator));
ie.Var = f.Formals[i]; ie.Type = ie.Var.Type;
substMap.Add(f.OverriddenFunction.Formals[i], ie);
foreach (var (formal, overriddenFormal) in f.Formals.Zip(f.OverriddenFunction.Formals, Tuple.Create)) {
// get corresponding formal in the class
var ie = new IdentifierExpr(formal.tok, formal.AssignUniqueName(f.IdGenerator)) { Var = formal, Type = formal.Type };
substMap.Add(overriddenFormal, ie);
}

if (f.OverriddenFunction.Result != null) {
Contract.Assert(pOut != null);
//get corresponsing formal in the class
var ie = new IdentifierExpr(pOut.tok, pOut.AssignUniqueName(f.IdGenerator));
ie.Var = pOut; ie.Type = ie.Var.Type;
//get corresponding formal in the class
var ie = new IdentifierExpr(pOut.tok, pOut.AssignUniqueName(f.IdGenerator)) { Var = pOut, Type = pOut.Type };
substMap.Add(f.OverriddenFunction.Result, ie);
}

Expand All @@ -947,7 +945,6 @@ private void AddFunctionOverrideCheckImpl(Function f) {
AddFunctionOverrideSubsetChk(f, builder, etran, localVariables, substMap, typeMap);

//adding assume Q; assert Post’;
//adding assume J.F(ins) == C.F(ins);
AddFunctionOverrideEnsChk(f, builder, etran, substMap, typeMap, implInParams, implOutParams.Count == 0 ? null : implOutParams[0]);

var stmts = builder.Collect(f.tok);
Expand All @@ -956,9 +953,9 @@ private void AddFunctionOverrideCheckImpl(Function f) {
// emit the impl only when there are proof obligations.
QKeyValue kv = etran.TrAttributes(f.Attributes, null);

var impl = AddImplementationWithVerboseName(f.tok, proc,
Util.Concat(Util.Concat(typeInParams, inParams_Heap), implInParams),
implOutParams, localVariables, stmts, kv);
AddImplementationWithVerboseName(f.tok, proc,
Util.Concat(Util.Concat(typeInParams, inParams_Heap), implInParams),
implOutParams, localVariables, stmts, kv);
}

if (InsertChecksums) {
Expand Down Expand Up @@ -999,7 +996,7 @@ private void AddOverrideCheckTypeArgumentInstantiations(MemberDecl member, Boogi
/// 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) }
/// this != null && $Is(this, C)
/// C.F#canCall(args) || (fh < FunctionContextHeight && this != null && $Is(this, C))
/// ==>
/// 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
Expand Down Expand Up @@ -1043,27 +1040,28 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti
argsJF.AddRange(GetTypeArguments(f, overridingFunction).ConvertAll(TypeToTy));
argsCF.AddRange(GetTypeArguments(overridingFunction, null).ConvertAll(TypeToTy));

var moreArgsCF = new List<Boogie.Expr>();
Expr layer = null;

// Add the fuel argument
if (f.IsFuelAware()) {
Contract.Assert(overridingFunction.IsFuelAware()); // f.IsFuelAware() ==> overridingFunction.IsFuelAware()
var fuel = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, "$fuel", predef.LayerType));
forallFormals.Add(fuel);
var ly = new Boogie.IdentifierExpr(f.tok, fuel);
argsJF.Add(ly);
argsCF.Add(ly);
layer = new Boogie.IdentifierExpr(f.tok, fuel);
argsJF.Add(layer);
} else if (overridingFunction.IsFuelAware()) {
// We can't use a bound variable $fuel, because then one of the triggers won't be mentioning this $fuel.
// Instead, we do the next best thing: use the literal $LZ.
var ly = new Boogie.IdentifierExpr(f.tok, "$LZ", predef.LayerType); // $LZ
argsCF.Add(ly);
layer = new Boogie.IdentifierExpr(f.tok, "$LZ", predef.LayerType); // $LZ
}

// Add heap arguments
if (f is TwoStateFunction) {
Contract.Assert(bvPrevHeap != null);
forallFormals.Add(bvPrevHeap);
argsJF.Add(etran.Old.HeapExpr);
argsCF.Add(etran.Old.HeapExpr);
moreArgsCF.Add(etran.Old.HeapExpr);
}
if (AlwaysUseHeap || f.ReadsHeap || overridingFunction.ReadsHeap) {
var heap = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));
Expand All @@ -1072,7 +1070,7 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti
argsJF.Add(new Boogie.IdentifierExpr(f.tok, heap));
}
if (AlwaysUseHeap || overridingFunction.ReadsHeap) {
argsCF.Add(new Boogie.IdentifierExpr(overridingFunction.tok, heap));
moreArgsCF.Add(new Boogie.IdentifierExpr(overridingFunction.tok, heap));
}
}

Expand All @@ -1082,10 +1080,12 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti
forallFormals.Add(bvThis);
var bvThisExpr = new Boogie.IdentifierExpr(f.tok, bvThis);
argsJF.Add(bvThisExpr);
argsCF.Add(bvThisExpr);
moreArgsCF.Add(bvThisExpr);
// $Is(this, C)
var isOfSubtype = GetWhereClause(overridingFunction.tok, bvThisExpr, thisType, f is TwoStateFunction ? etran.Old : etran, IsAllocType.NEVERALLOC);

Bpl.Expr ante = Boogie.Expr.And(ReceiverNotNull(bvThisExpr), isOfSubtype);

// Add other arguments
var typeMap = GetTypeArgumentSubstitutionMap(f, overridingFunction);
foreach (Formal p in f.Formals) {
Expand All @@ -1094,13 +1094,26 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti
forallFormals.Add(bv);
var jfArg = new Boogie.IdentifierExpr(p.tok, bv);
argsJF.Add(ModeledAsBoxType(p.Type) ? BoxIfUnboxed(jfArg, pType) : jfArg);
argsCF.Add(new Boogie.IdentifierExpr(p.tok, bv));
moreArgsCF.Add(new Boogie.IdentifierExpr(p.tok, bv));
}

// useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight)
ModuleDefinition mod = f.EnclosingClass.EnclosingModuleDefinition;
Boogie.Expr useViaContext = !InVerificationScope(overridingFunction) ? (Boogie.Expr)Boogie.Expr.True :
Boogie.Expr.Neq(Boogie.Expr.Literal(mod.CallGraph.GetSCCRepresentativePredecessorCount(overridingFunction)), etran.FunctionContextHeight());
// 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);
}

argsCF = Concat(argsCF, moreArgsCF);

// ante := useViaCanCall || (useViaContext && this != null && $Is(this, C))
ante = Bpl.Expr.Or(useViaCanCall, BplAnd(useViaContext, ante));

Boogie.Expr funcAppl;
{
Expand Down Expand Up @@ -1133,8 +1146,8 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti

// The axiom
Boogie.Expr ax = BplForall(f.tok, new List<Boogie.TypeVariable>(), forallFormals, null, tr,
Boogie.Expr.Imp(Boogie.Expr.And(ReceiverNotNull(bvThisExpr), isOfSubtype), synonyms));
var activate = AxiomActivation(f, etran);
Boogie.Expr.Imp(ante, synonyms));
var activate = AxiomActivation(overridingFunction, etran);
string comment = "override axiom for " + f.FullSanitizedName + " in class " + overridingFunction.EnclosingClass.FullSanitizedName;
return new Boogie.Axiom(f.tok, Boogie.Expr.Imp(activate, ax), comment);
}
Expand Down Expand Up @@ -1192,13 +1205,11 @@ private void AddMethodOverrideEnsChk(Method m, BoogieStmtListBuilder builder, Ex
builder.Add(TrAssumeCmd(m.tok, etran.TrExpr(en.E)));
}
//generating trait post-conditions with class variables
FunctionCallSubstituter sub = null;
foreach (var en in m.OverriddenMethod.Ens) {
Expression postcond = Substitute(en.E, null, substMap, typeMap);
bool splitHappened; // we actually don't care
foreach (var s in TrSplitExpr(postcond, etran, false, out splitHappened)) {
if (s.IsChecked) {
builder.Add(Assert(m.tok, s.E, new PODesc.EnsuresStronger()));
}
sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (ClassDecl)m.EnclosingClass);
foreach (var s in TrSplitExpr(sub.Substitute(en.E), etran, false, out _).Where(s => s.IsChecked)) {
builder.Add(Assert(m.tok, s.E, new PODesc.EnsuresStronger()));
}
}
}
Expand All @@ -1211,18 +1222,14 @@ private void AddMethodOverrideReqsChk(Method m, BoogieStmtListBuilder builder, E
Contract.Requires(etran != null);
Contract.Requires(substMap != null);
//generating trait pre-conditions with class variables
FunctionCallSubstituter sub = null;
foreach (var req in m.OverriddenMethod.Req) {
Expression precond = Substitute(req.E, null, substMap, typeMap);
builder.Add(TrAssumeCmd(m.tok, etran.TrExpr(precond)));
sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (ClassDecl)m.EnclosingClass);
builder.Add(TrAssumeCmd(m.tok, etran.TrExpr(sub.Substitute(req.E))));
}
//generating class pre-conditions
foreach (var req in m.Req) {
bool splitHappened; // we actually don't care
foreach (var s in TrSplitExpr(req.E, etran, false, out splitHappened)) {
if (s.IsChecked) {
builder.Add(Assert(m.tok, s.E, new PODesc.RequiresWeaker()));
}
}
foreach (var s in m.Req.SelectMany(req => TrSplitExpr(req.E, etran, false, out _).Where(s => s.IsChecked))) {
builder.Add(Assert(m.tok, s.E, new PODesc.RequiresWeaker()));
}
}

Expand Down Expand Up @@ -1381,7 +1388,7 @@ 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, etran.HeightContext(kind == MethodTranslationKind.OverrideCheck ? m.OverriddenMethod : m), null, null));
req.Add(Requires(m.tok, true, etran.HeightContext(m), null, null));
if (m is TwoStateLemma) {
// free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap)
var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr);
Expand Down
Loading

0 comments on commit 993b589

Please sign in to comment.