Skip to content

Commit

Permalink
fix: Cross-modular override check (dafny-lang#3223)
Browse files Browse the repository at this point in the history 
Fixes 2500.

To achieve this, we first give the override axiom the visibility of the
overriding function. To ensure we only use the axiom in case we pass the
check, we introduce an intermediate visibility level. The ensures clause
of the overridden function can reference the underlying function, so we
need to substitute the overridden function by the overriding function in
the override check.

Co-authored-by: Robin Salkeld <[email protected]>
  • Loading branch information
@fabiomadge @robin-aws @atomb
2 people authored and atomb committed Feb 1, 2023
1 parent ec9f762 commit 3e8a10e
Show file tree
Hide file tree
Showing 14 changed files with 133 additions and 116 deletions.
2 changes: 1 addition & 1 deletion Source/DafnyCore/Compilers/Compiler-js.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2535,9 +2535,9 @@ bool SendToNewNodeProcess(string dafnyProgramName, string targetProgramText, str

var psi = new ProcessStartInfo("node", "") {
RedirectStandardInput = true,
StandardInputEncoding = Encoding.UTF8,
RedirectStandardOutput = true,
RedirectStandardError = true,
StandardInputEncoding = Encoding.UTF8,
};

try {
Expand Down
5 changes: 1 addition & 4 deletions Source/DafnyCore/Compilers/Compiler-python.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1768,10 +1768,7 @@ private static string FindModuleName(string externFilename) {
}
}
rd.Close();
if (externFilename.EndsWith(".py")) {
return externFilename.Substring(0, externFilename.Length - 3);
}
return null;
return externFilename.EndsWith(".py") ? externFilename[..^3] : null;
}

static bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram, TextWriter outputWriter) {
Expand Down
20 changes: 10 additions & 10 deletions Source/DafnyCore/Verifier/FunctionCallSubstituter.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,26 +3,26 @@
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>()) {
public FunctionCallSubstituter(Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap, Dictionary<TypeParameter, Type> typeMap, Function a, Function b)
: base(receiverReplacement, substMap, typeMap) {
A = a;
B = b;
}
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) {
if (expr is FunctionCallExpr e) {
var receiver = Substitute(e.Receiver);
var newArgs = SubstituteExprList(e.Args);
var newFce = new FunctionCallExpr(e.tok, e.Name, receiver, e.OpenParen, e.CloseParen, newArgs, e.AtLabel);
if (e.Function == A && e.Receiver is ThisExpr && receiver is ThisExpr) {
newFce.Function = B;
newFce.Type = e.Type; // TODO: this may not work with type parameters.
receiver.Type = Resolver.GetThisType(B.tok, (TopLevelDeclWithMembers)B.EnclosingClass);
} else {
newFce.Function = e.Function;
newFce.Type = e.Type;
}
newFce.TypeApplication_AtEnclosingClass = e.TypeApplication_AtEnclosingClass; // resolve here
newFce.TypeApplication_JustFunction = e.TypeApplication_JustFunction; // resolve here
newFce.TypeApplication_AtEnclosingClass = SubstituteTypeList(e.TypeApplication_AtEnclosingClass); // resolve here
newFce.TypeApplication_JustFunction = SubstituteTypeList(e.TypeApplication_JustFunction); // resolve here
newFce.IsByMethodCall = e.IsByMethodCall;
return newFce;
}
Expand Down
27 changes: 13 additions & 14 deletions Source/DafnyCore/Verifier/Translator.ClassMembers.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -213,7 +213,8 @@ private void AddAllocationAxiom(Boogie.Declaration fieldDeclaration, Field f, To
AddWellformednessCheck(cf);
if (InVerificationScope(cf)) {
var etran = new ExpressionTranslator(this, predef, f.tok);
heightAntecedent = Bpl.Expr.Lt(Bpl.Expr.Literal(cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf)), etran.FunctionContextHeight());
var visibilityLevel = cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf);
heightAntecedent = Bpl.Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight());
}
}

Expand Down Expand Up @@ -877,8 +878,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, true), 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 +921,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 @@ -946,8 +945,8 @@ private void AddFunctionOverrideCheckImpl(Function f) {
//adding assert W <= Frame’
AddFunctionOverrideSubsetChk(f, builder, etran, localVariables, substMap, typeMap);

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

var stmts = builder.Collect(f.tok);
Expand Down Expand Up @@ -1134,7 +1133,7 @@ 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);
var activate = AxiomActivation(overridingFunction, etran, true);
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
7 changes: 3 additions & 4 deletions Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -258,12 +258,11 @@ public Boogie.IdentifierExpr FunctionContextHeight() {
return new Boogie.IdentifierExpr(Token.NoToken, "$FunctionContextHeight", Boogie.Type.Int);
}

public Boogie.Expr HeightContext(ICallable m) {
public Boogie.Expr HeightContext(ICallable m, bool intermediateScope = false) {
Contract.Requires(m != null);
// free requires fh == FunctionContextHeight;
var module = m.EnclosingModule;
Boogie.Expr context =
Boogie.Expr.Eq(Boogie.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(m)), FunctionContextHeight());
var visibilityLevel = m.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(m);
Boogie.Expr context = Boogie.Expr.Eq(MkFunctionHeight(visibilityLevel, intermediateScope), FunctionContextHeight());
return context;
}

Expand Down
116 changes: 49 additions & 67 deletions Source/DafnyCore/Verifier/Translator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2054,7 +2054,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
// (mh == ModuleContextHeight && fh <= FunctionContextHeight)
//
// USE_VIA_CONTEXT
// (mh != ModuleContextHeight || fh != FunctionContextHeight) &&
// fh < FunctionContextHeight &&
// GOOD_PARAMETERS
// where GOOD_PARAMETERS means:
// $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
Expand Down Expand Up @@ -2157,10 +2157,9 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
foreach (AttributedExpression req in f.Req) {
pre = BplAnd(pre, etran.TrExpr(Substitute(req.E, null, substMap)));
}
// useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight)
var mod = f.EnclosingClass.EnclosingModuleDefinition;
Bpl.Expr useViaContext = !InVerificationScope(f) ? Bpl.Expr.True :
(Bpl.Expr)Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight());
// useViaContext: fh < FunctionContextHeight
var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f.OverriddenFunction ?? f);
Expr useViaContext = Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight());
// useViaCanCall: f#canCall(args)
Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool);
Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), Concat(tyargs, args));
Expand Down Expand Up @@ -2255,15 +2254,14 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
return (olderParameterCount, olderCondition);
}

Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran) {
Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran, bool requiresFullScope = false) {
Contract.Requires(f != null);
Contract.Requires(etran != null);
Contract.Requires(VisibleInScope(f));
var module = f.EnclosingClass.EnclosingModuleDefinition;

if (InVerificationScope(f)) {
return
Bpl.Expr.Le(Bpl.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight());
var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f);
return Expr.Le(MkFunctionHeight(visibilityLevel, !requiresFullScope), etran.FunctionContextHeight());
} else {
return Bpl.Expr.True;
}
Expand Down Expand Up @@ -2303,7 +2301,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
// for visibility==ForeignModuleOnly, means:
// GOOD_PARAMETERS
// for visibility==IntraModuleOnly, means:
// fh != FunctionContextHeight &&
// fh < FunctionContextHeight &&
// GOOD_PARAMETERS
// where GOOD_PARAMETERS means:
// $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
Expand Down Expand Up @@ -2508,12 +2506,11 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
return null;
}

// useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight)
ModuleDefinition mod = f.EnclosingClass.EnclosingModuleDefinition;
// useViaContext: fh < FunctionContextHeight
var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f);
Bpl.Expr useViaContext = !InVerificationScope(f)
? (Bpl.Expr)Bpl.Expr.True
: Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativePredecessorCount(f)),
etran.FunctionContextHeight());
? Bpl.Expr.True
: Bpl.Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight());
// ante := (useViaContext && typeAnte && pre)
ante = BplAnd(useViaContext, BplAnd(ante, pre));

Expand Down Expand Up @@ -3483,65 +3480,42 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder
builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(en.E)));
}

//generating assume J.F(ins) == C.F(ins)
Bpl.FunctionCall funcIdC = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
Bpl.FunctionCall funcIdT = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.OverriddenFunction.tok, f.OverriddenFunction.FullSanitizedName, TrType(f.OverriddenFunction.ResultType)));
List<Bpl.Expr> argsC = new List<Bpl.Expr>();
List<Bpl.Expr> argsT = new List<Bpl.Expr>();
// add type arguments
argsT.AddRange(GetTypeArguments(f.OverriddenFunction, f).ConvertAll(TypeToTy));
argsC.AddRange(GetTypeArguments(f, null).ConvertAll(TypeToTy));
// add fuel arguments
if (f.IsFuelAware()) {
argsC.Add(etran.layerInterCluster.GetFunctionFuel(f));
}
if (f.OverriddenFunction.IsFuelAware()) {
argsT.Add(etran.layerInterCluster.GetFunctionFuel(f));
}
// add heap arguments
if (f is TwoStateFunction) {
argsC.Add(etran.Old.HeapExpr);
argsT.Add(etran.Old.HeapExpr);
}
if (AlwaysUseHeap || f.ReadsHeap) {
argsC.Add(etran.HeapExpr);
}
if (AlwaysUseHeap || f.OverriddenFunction.ReadsHeap) {
argsT.Add(etran.HeapExpr);
}
// add "ordinary" parameters (including "this", if any)
var prefixCount = implInParams.Count - f.Formals.Count;
for (var i = 0; i < implInParams.Count; i++) {
Bpl.Expr cParam = new Bpl.IdentifierExpr(f.tok, implInParams[i]);
Bpl.Expr tParam = new Bpl.IdentifierExpr(f.OverriddenFunction.tok, implInParams[i]);
if (prefixCount <= i && ModeledAsBoxType(f.OverriddenFunction.Formals[i - prefixCount].Type)) {
tParam = BoxIfNecessary(f.tok, tParam, f.Formals[i - prefixCount].Type);
}
argsC.Add(cParam);
argsT.Add(tParam);
}
Bpl.Expr funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);
Bpl.Expr funcExpT = new Bpl.NAryExpr(f.OverriddenFunction.tok, funcIdT, argsT);
var funcExpCPossiblyBoxed = funcExpC;
if (ModeledAsBoxType(f.OverriddenFunction.ResultType)) {
funcExpCPossiblyBoxed = BoxIfUnboxed(funcExpCPossiblyBoxed, f.ResultType);
}
builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpCPossiblyBoxed, funcExpT)));

//generating assume C.F(ins) == out, if a result variable was given
if (resultVariable != null) {
var funcIdC = new FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
var argsC = new List<Bpl.Expr>();

// add type arguments
argsC.AddRange(GetTypeArguments(f, null).ConvertAll(TypeToTy));

// add fuel arguments
if (f.IsFuelAware()) {
argsC.Add(etran.layerInterCluster.GetFunctionFuel(f));
}

// add heap arguments
if (f is TwoStateFunction) {
argsC.Add(etran.Old.HeapExpr);
}
if (AlwaysUseHeap || f.ReadsHeap) {
argsC.Add(etran.HeapExpr);
}

argsC.AddRange(implInParams.Select(var => new Bpl.IdentifierExpr(f.tok, var)));

var funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);
var resultVar = new Bpl.IdentifierExpr(resultVariable.tok, resultVariable);
builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, resultVar)));
}

//generating trait post-conditions with class variables
foreach (var en in f.OverriddenFunction.Ens) {
Expression postcond = Substitute(en.E, null, substMap, typeMap);
bool splitHappened; // we don't actually care
foreach (var s in TrSplitExpr(postcond, etran, false, out splitHappened)) {
if (s.IsChecked) {
builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true)));
}
// 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.
var sub = new FunctionCallSubstituter(null, substMap, typeMap, f.OverriddenFunction, f);
foreach (var s in TrSplitExpr(sub.Substitute(en.E), etran, false, out _).Where(s => s.IsChecked)) {
builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true)));
}
}
}
Expand Down Expand Up @@ -4765,7 +4739,7 @@ Bpl.Expr CanCallAssumption(Expression expr, ExpressionTranslator etran) {
Contract.Requires(predef != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) {
if (expr is LiteralExpr or ThisExpr or IdentifierExpr or WildcardExpr or BoogieWrapper) {
return Bpl.Expr.True;
} else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
Expand Down Expand Up @@ -10752,6 +10726,14 @@ List<Variable> MkTyParamFormals(List<TypeParameter> args, bool includeWhereClaus
return null;
}

// We use the $FunctionContextHeight to restrict the applicability of certain axioms. The entity at the end of a
// dependency chain has the highest number. To get more granular control over the visibility, we extend every
// visibility level by a precursory intermediate level. This additional level is helpful for proofs that would be
// disturbed by axioms that are visible the the final level.
static Bpl.Expr MkFunctionHeight(int visibilityLevel, bool intermediateScope = false) {
return Expr.Literal(visibilityLevel * 2 + (intermediateScope ? 0 : 1));
}

public static void MapM<A>(IEnumerable<A> xs, Action<A> K) {
Contract.Requires(xs != null);
Contract.Requires(K != null);
Expand Down
4 changes: 2 additions & 2 deletions Test/concurrency/10-SequenceInvariant.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -256,7 +256,7 @@ class Thread extends Object {
}
twostate lemma baseFieldsInvMonotonicity() requires old(baseFieldsInv()) && old(universe.content) <= universe.content && unchanged(this) ensures baseFieldsInv() {}

predicate localInv() reads * {
predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
&& objectGlobalBaseInv()
}
predicate inv() reads * ensures inv() ==> localInv() {
Expand Down Expand Up @@ -322,7 +322,7 @@ trait OwnedObject extends Object {
assert owner in universe.content;
}

predicate localInv() reads * {
predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
&& objectGlobalBaseInv()
&& localUserInv()
}
Expand Down
4 changes: 2 additions & 2 deletions Test/concurrency/11-MutexGuard2.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -261,7 +261,7 @@ class Thread extends Object {
}
twostate lemma baseFieldsInvMonotonicity() requires old(baseFieldsInv()) && old(universe.content) <= universe.content && unchanged(this) ensures baseFieldsInv() {}

predicate localInv() reads * {
predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
&& objectGlobalBaseInv()
}
predicate inv() reads * ensures inv() ==> localInv() {
Expand Down Expand Up @@ -332,7 +332,7 @@ trait OwnedObject extends Object {
&& unchangedNonvolatileUserFields()
}

predicate localInv() reads * {
predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
&& objectGlobalBaseInv()
&& localUserInv()
}
Expand Down
4 changes: 2 additions & 2 deletions Test/concurrency/12-MutexLifetime-short.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -365,7 +365,7 @@ class Thread extends Object {
}
twostate lemma baseFieldsInvMonotonicity() requires old(baseFieldsInv()) && old(universe.content) <= universe.content && unchanged(this) ensures baseFieldsInv() {}

predicate localInv() reads * {
predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
&& objectGlobalBaseInv()
}
predicate inv() reads * ensures inv() ==> localInv() {
Expand Down Expand Up @@ -439,7 +439,7 @@ trait OwnedObject extends Object {
&& unchangedNonvolatileUserFields()
}

predicate localInv() reads * {
predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
&& objectGlobalBaseInv()
&& this in lifetime.elements
&& (lifetime.alive() ==> owner != null)
Expand Down
Loading

0 comments on commit 3e8a10e

Please sign in to comment.