Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix: Cross-modular override check #3223

Merged
merged 21 commits into from
Jan 25, 2023
Merged

fix: Cross-modular override check #3223

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
1f0d29b
skip equality generation in the check
fabiomadge Nov 24, 2022
b99bff8
delete dead code
fabiomadge Nov 24, 2022
fbedb7a
Merge branch 'master' into fix_overrides_check
fabiomadge Nov 30, 2022
342be57
hide override axiom
fabiomadge Dec 20, 2022
d37cf04
tuned
fabiomadge Dec 20, 2022
d1eb5a8
review
fabiomadge Dec 21, 2022
117585e
\n
fabiomadge Dec 21, 2022
922049d
restict substitutions to occurences where `this` is the receiver
fabiomadge Jan 4, 2023
1dc1ed4
use correct hight
fabiomadge Jan 4, 2023
4c46f74
Merge branch 'master' into fix_overrides_check
fabiomadge Jan 4, 2023
0a3d964
fix tests
fabiomadge Jan 5, 2023
2ee54f7
add tests
fabiomadge Jan 5, 2023
0c3cb41
typo
fabiomadge Jan 5, 2023
54e1cfd
remove comment
fabiomadge Jan 5, 2023
2e67b54
Merge branch 'master' into fix_overrides_check
fabiomadge Jan 5, 2023
923f38a
add comment about incompleteness of the encoding
fabiomadge Jan 5, 2023
7d8fe8f
Merge branch 'master' into fix_overrides_check
fabiomadge Jan 19, 2023
d9ae00a
weaker -> stronger
fabiomadge Jan 19, 2023
ee6c02d
document deficiency of the encoding
fabiomadge Jan 20, 2023
a86643c
rename
fabiomadge Jan 20, 2023
01b2f4b
Merge branch 'master' into fix_overrides_check
robin-aws Jan 25, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Source/DafnyCore/Compilers/Compiler-js.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2527,9 +2527,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
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1752,10 +1752,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
2 changes: 1 addition & 1 deletion Source/DafnyCore/Substituter.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ public virtual Expression Substitute(Expression expr) {
} else if (expr is WildcardExpr) {
// nothing to substitute
} else if (expr is ThisExpr) {
return receiverReplacement == null ? expr : receiverReplacement;
return receiverReplacement ?? expr;
} else if (expr is IdentifierExpr) {
IdentifierExpr e = (IdentifierExpr)expr;
Expression substExpr;
Expand Down
8 changes: 4 additions & 4 deletions Source/DafnyCore/Verifier/FunctionCallSubstituter.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@
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;
}
Expand All @@ -21,8 +21,8 @@ public override Expression Substitute(Expression expr) {
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
23 changes: 11 additions & 12 deletions Source/DafnyCore/Verifier/Translator.ClassMembers.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -213,7 +213,7 @@ 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());
heightAntecedent = Bpl.Expr.Lt(Bpl.Expr.Literal(cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf) * 2 + 1), etran.FunctionContextHeight());
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I suggest making a SCCPredecessorCountToFunctionHeight method that performs the ... * 2 + 1 computation. And I guess the + 1 should then also be controlled by a boolean, like you're doing in HeightContext, etc.

}
}

Expand Down Expand Up @@ -878,7 +878,7 @@ 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));
req.Add(Requires(f.tok, true, etran.HeightContext(f.OverriddenFunction, 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 +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 @@ -946,8 +944,9 @@ private void AddFunctionOverrideCheckImpl(Function f) {
//adding assert W <= Frame’
AddFunctionOverrideSubsetChk(f, builder, etran, localVariables, substMap, typeMap);

//adding assume Q; assert Post’;
//adding assume Q;
//adding assume J.F(ins) == C.F(ins);
//assert Post’;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These two should be in the other order. That is, it should first check that the postcondition of the trait holds, and only then should it be given the information J.F(ins) == C.F(ins).

Copy link
Collaborator Author

@fabiomadge fabiomadge Dec 20, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The comment is outdated. There is no assume anymore. (At least not of that equality.)

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
4 changes: 2 additions & 2 deletions Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -258,12 +258,12 @@ 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 reducedScope = false) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit: consider using "intermediateScope" here instead, or renaming the parameter, for consistency.

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());
Boogie.Expr.Eq(Boogie.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(m) * 2 + (reducedScope ? 0 : 1)), FunctionContextHeight());
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here's another place for that ... * 2 + 0-or-1 method.

return context;
}

Expand Down
97 changes: 36 additions & 61 deletions Source/DafnyCore/Verifier/Translator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2156,10 +2156,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 lowerBound = (f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f) + 1) * 2;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

And here, too. In this instance, it would make it clear that the + 1 is indeed placed in the right place.

Expr useViaContext = !InVerificationScope(f) ? Bpl.Expr.True : Expr.Le(Expr.Literal(lowerBound), 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 @@ -2254,15 +2253,15 @@ 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 hidden = false) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't find hidden to be such a good description. Can you make the name more descriptive? Or, if not, add a comment that describes it.

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 lowerBound = module.CallGraph.GetSCCRepresentativePredecessorCount(f) * 2 + (hidden ? 1 : 0);
return Expr.Le(Expr.Literal(lowerBound), etran.FunctionContextHeight());
} else {
return Bpl.Expr.True;
}
Expand Down Expand Up @@ -2511,7 +2510,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
ModuleDefinition mod = f.EnclosingClass.EnclosingModuleDefinition;
Bpl.Expr useViaContext = !InVerificationScope(f)
? (Bpl.Expr)Bpl.Expr.True
: Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativePredecessorCount(f)),
: Bpl.Expr.Le(Bpl.Expr.Literal((mod.CallGraph.GetSCCRepresentativePredecessorCount(f) + 1) * 2),
etran.FunctionContextHeight());
// ante := (useViaContext && typeAnte && pre)
ante = BplAnd(useViaContext, BplAnd(ante, pre));
Expand Down Expand Up @@ -3486,65 +3485,41 @@ 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)));
List<Expr> argsC = new List<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)));

Expr 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)));
builder.Add(TrAssumeCmd(f.tok, Expr.Eq(funcExpC, resultVar)));
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I know Rider keeps saying the Bpl. is not necessary. I guess it's fine to get rid of it, but I've been fine with seeing the prefix, since it reminds me that Bpl.Expr is not Expression.

}

//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)));
}
var receiver = new ImplicitThisExpr(f.tok) { Type = Resolver.GetThisType(f.tok, (TopLevelDeclWithMembers)f.EnclosingClass) };
var sub = new FunctionCallSubstituter(receiver, substMap, typeMap, f.OverriddenFunction, f);
Expression postcond = sub.Substitute(en.E);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this replaces too many occurrences of the function. For example, I suspect it will make the following override verify, but it mustn't:

trait Tr {
  function F(x: nat, other: Tr): int
    ensures x != 0 && other.F(x - 1, other) < 20 ==> F(x, other) % 2 == other.F(x - 1, other) % 2
}

class Cl extends Tr {
  function F(x: nat, other: Tr): int
    ensures 50 <= F(x, other)
}

Note that the calls other.F(x - 1, other) should not be changed by the substitution.

foreach (var s in TrSplitExpr(postcond, etran, false, out _).Where(s => s.IsChecked)) {
builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true)));
}
}
}
Expand Down Expand Up @@ -4768,7 +4743,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