From deac70817db80a3f203859ab9414d1c28205d4e2 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 24 Feb 2014 16:20:55 -0800 Subject: Refactored code for dealing with SCCs in the call graph. Fixed bug. --- Source/Dafny/Cloner.cs | 6 ++-- Source/Dafny/DafnyAst.cs | 35 +++++++++++++++++++ Source/Dafny/Resolver.cs | 85 ++++++++++++++++++++-------------------------- Source/Dafny/Rewriter.cs | 3 +- Source/Dafny/Translator.cs | 85 ++++++++++++++++++++++------------------------ 5 files changed, 115 insertions(+), 99 deletions(-) (limited to 'Source/Dafny') diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 452c71e4..97e88e3d 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -681,7 +681,7 @@ namespace Microsoft.Dafny var call = (CallStmt)s.ResolvedStatements[0]; var moduleCaller = context.EnclosingClass.Module; var moduleCallee = call.Method.EnclosingClass.Module; - if (call.Method is CoLemma && moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(call.Method)) { + if (call.Method is CoLemma && ModuleDefinition.InSameSCC(context, call.Method)) { // we're looking at a recursive call to a colemma var args = new List(); args.Add(k); @@ -700,9 +700,7 @@ namespace Microsoft.Dafny } else if (stmt is CallStmt) { var s = (CallStmt)stmt; if (s.Method is CoLemma) { - var moduleCaller = context.EnclosingClass.Module; - var moduleCallee = s.Method.EnclosingClass.Module; - if (s.Method is CoLemma && moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) { + if (s.Method is CoLemma && ModuleDefinition.InSameSCC(context, s.Method)) { // we're looking at a recursive call to a colemma var args = new List(); args.Add(k); diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index eee1b06f..a8c3f56d 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1105,6 +1105,41 @@ namespace Microsoft.Dafny { } } + /// + /// Determines if "a" and "b" are in the same strongly connected component of the call graph, that is, + /// if "a" and "b" are mutually recursive. + /// Assumes that CallGraph has already been filled in for the modules containing "a" and "b". + /// + public static bool InSameSCC(ICallable a, ICallable b) { + Contract.Requires(a != null); + Contract.Requires(b != null); + var module = a.EnclosingModule; + return module == b.EnclosingModule && module.CallGraph.GetSCCRepresentative(a) == module.CallGraph.GetSCCRepresentative(b); + } + + /// + /// Return the representative elements of the SCCs that contain contain any member declaration in a + /// class in "declarations". + /// Note, the representative element may in some cases be a Method, not necessarily a Function. + /// + public static IEnumerable AllFunctionSCCs(List declarations) { + var set = new HashSet(); + foreach (var d in declarations) { + var cl = d as ClassDecl; + if (cl != null) { + var module = cl.Module; + foreach (var member in cl.Members) { + var fn = member as Function; + if (fn != null) { + var repr = module.CallGraph.GetSCCRepresentative(fn); + set.Add(repr); + } + } + } + } + return set; + } + public static IEnumerable AllFunctions(List declarations) { foreach (var d in declarations) { var cl = d as ClassDecl; diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 57527202..ccbd9a29 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1469,39 +1469,40 @@ namespace Microsoft.Dafny if (ErrorCount == prevErrorCount) { // because CheckCoCalls requires the given expression to have been successfully resolved // Perform the guardedness check on co-datatypes - foreach (var fn in ModuleDefinition.AllFunctions(declarations)) { - var module = fn.EnclosingClass.Module; - if (fn.Body != null && module.CallGraph.GetSCCRepresentative(fn) == fn) { - bool dealsWithCodatatypes = false; - foreach (var m in module.CallGraph.GetSCC(fn)) { - var f = m as Function; - if (f != null && f.ResultType.InvolvesCoDatatype) { - dealsWithCodatatypes = true; - break; - } + foreach (var repr in ModuleDefinition.AllFunctionSCCs(declarations)) { + var module = repr.EnclosingModule; + bool dealsWithCodatatypes = false; + foreach (var m in module.CallGraph.GetSCC(repr)) { + var f = m as Function; + if (f != null && f.ResultType.InvolvesCoDatatype) { + dealsWithCodatatypes = true; + break; } - var coCandidates = new List(); - var hasIntraClusterCallsInDestructiveContexts = false; - foreach (var m in module.CallGraph.GetSCC(fn)) { - var f = m as Function; - if (f != null && f.Body != null) { - var checker = new CoCallResolution(f, dealsWithCodatatypes); - checker.CheckCoCalls(f.Body); - coCandidates.AddRange(checker.FinalCandidates); - hasIntraClusterCallsInDestructiveContexts |= checker.HasIntraClusterCallsInDestructiveContexts; + } + var coCandidates = new List(); + var hasIntraClusterCallsInDestructiveContexts = false; + foreach (var m in module.CallGraph.GetSCC(repr)) { + var f = m as Function; + if (f != null && f.Body != null) { + var checker = new CoCallResolution(f, dealsWithCodatatypes); + checker.CheckCoCalls(f.Body); + coCandidates.AddRange(checker.FinalCandidates); + hasIntraClusterCallsInDestructiveContexts |= checker.HasIntraClusterCallsInDestructiveContexts; + } else if (f == null) { + // the SCC contains a method, which we always consider to be a destructive context + hasIntraClusterCallsInDestructiveContexts = true; + } + } + if (coCandidates.Count != 0) { + if (hasIntraClusterCallsInDestructiveContexts) { + foreach (var c in coCandidates) { + c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsInDestructiveContext; } - } - if (coCandidates.Count != 0) { - if (hasIntraClusterCallsInDestructiveContexts) { - foreach (var c in coCandidates) { - c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsInDestructiveContext; - } - } else { - foreach (var c in coCandidates) { - c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.Yes; - c.EnclosingCoConstructor.IsCoCall = true; - ReportAdditionalInformation(c.CandidateCall.tok, "co-recursive call", c.CandidateCall.Name.Length); - } + } else { + foreach (var c in coCandidates) { + c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.Yes; + c.EnclosingCoConstructor.IsCoCall = true; + ReportAdditionalInformation(c.CandidateCall.tok, "co-recursive call", c.CandidateCall.Name.Length); } } } @@ -2070,9 +2071,7 @@ namespace Microsoft.Dafny protected override bool VisitOneExpr(Expression expr, ref CallingPosition cp) { if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; - var moduleCaller = context.EnclosingClass.Module; - var moduleCallee = e.Function.EnclosingClass.Module; - if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(e.Function)) { + if (ModuleDefinition.InSameSCC(context, e.Function)) { // we're looking at a recursive call if (!(e.Function is CoPredicate)) { Error(e, "a recursive call from a copredicate can go only to other copredicates"); @@ -2158,9 +2157,7 @@ namespace Microsoft.Dafny protected override bool VisitOneStmt(Statement stmt, ref CallingPosition st) { if (stmt is CallStmt) { var s = (CallStmt)stmt; - var moduleCaller = context.EnclosingClass.Module; - var moduleCallee = s.Method.EnclosingClass.Module; - if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) { + if (ModuleDefinition.InSameSCC(context, s.Method)) { // we're looking at a recursive call Error(stmt.Tok, "a recursive call from a copredicate can go only to other copredicates"); } @@ -2200,9 +2197,7 @@ namespace Microsoft.Dafny // all is cool } else { // the call goes from a colemma context to a non-colemma callee - var moduleCaller = context.EnclosingClass.Module; - var moduleCallee = s.Method.EnclosingClass.Module; - if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) { + if (ModuleDefinition.InSameSCC(context, s.Method)) { // we're looking at a recursive call (to a non-colemma) Error(s.Tok, "a recursive call from a colemma can go only to other colemmas and prefix lemmas"); } @@ -2214,9 +2209,7 @@ namespace Microsoft.Dafny if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; // the call goes from a colemma context to a non-colemma callee - var moduleCaller = context.EnclosingClass.Module; - var moduleCallee = e.Function.EnclosingClass.Module; - if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(e.Function)) { + if (ModuleDefinition.InSameSCC(context, e.Function)) { // we're looking at a recursive call (to a non-colemma) Error(e.tok, "a recursive call from a colemma can go only to other colemmas and prefix lemmas"); } @@ -7815,7 +7808,6 @@ namespace Microsoft.Dafny class CoCallResolution { - readonly ModuleDefinition currentModule; readonly Function currentFunction; readonly bool dealsWithCodatatypes; public bool HasIntraClusterCallsInDestructiveContexts = false; @@ -7823,7 +7815,6 @@ namespace Microsoft.Dafny public CoCallResolution(Function currentFunction, bool dealsWithCodatatypes) { Contract.Requires(currentFunction != null); - this.currentModule = currentFunction.EnclosingClass.Module; this.currentFunction = currentFunction; this.dealsWithCodatatypes = dealsWithCodatatypes; } @@ -7922,9 +7913,7 @@ namespace Microsoft.Dafny CheckCoCalls(arg, int.MaxValue, null, coCandidates); } // Second, investigate the possibility that this call itself may be a candidate co-call - var calleeModule = e.Function.EnclosingClass.Module; - if (currentModule == calleeModule && - currentModule.CallGraph.GetSCCRepresentative(currentFunction) == calleeModule.CallGraph.GetSCCRepresentative(e.Function)) { + if (ModuleDefinition.InSameSCC(currentFunction, e.Function)) { // This call goes to another function in the same recursive cluster if (destructionLevel > 0) { // a potentially destructive context diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 67fc7268..83623399 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -773,8 +773,7 @@ namespace Microsoft.Dafny reqs.AddRange(generateAutoReqs(arg)); } - ModuleDefinition module = e.Function.EnclosingClass.Module; - if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(parentFunction)) { + if (ModuleDefinition.InSameSCC(e.Function, parentFunction)) { // We're making a call within the same SCC, so don't descend into this function } else { reqs.AddRange(gatherReqs(e.Function, e.Args, e.Receiver)); diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index cb316008..c6c82193 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3633,49 +3633,46 @@ namespace Microsoft.Dafny { Bpl.Expr allowance = null; if (codeContext != null && e.CoCall != FunctionCallExpr.CoCallResolution.Yes && !(e.Function is CoPredicate)) { // check that the decreases measure goes down - ModuleDefinition module = cce.NonNull(e.Function.EnclosingClass).Module; - if (module == codeContext.EnclosingModule) { - if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(codeContext)) { - List contextDecreases = codeContext.Decreases.Expressions; - List calleeDecreases = e.Function.Decreases.Expressions; - if (e.Function == options.SelfCallsAllowance) { - allowance = Bpl.Expr.True; - if (!e.Function.IsStatic) { - allowance = BplAnd(allowance, Bpl.Expr.Eq(etran.TrExpr(e.Receiver), new Bpl.IdentifierExpr(e.tok, etran.This, predef.RefType))); - } - for (int i = 0; i < e.Args.Count; i++) { - Expression ee = e.Args[i]; - Formal ff = e.Function.Formals[i]; - allowance = BplAnd(allowance, Bpl.Expr.Eq(etran.TrExpr(ee), new Bpl.IdentifierExpr(e.tok, ff.AssignUniqueName(currentDeclaration), TrType(ff.Type)))); - } + if (ModuleDefinition.InSameSCC(e.Function, codeContext)) { + List contextDecreases = codeContext.Decreases.Expressions; + List calleeDecreases = e.Function.Decreases.Expressions; + if (e.Function == options.SelfCallsAllowance) { + allowance = Bpl.Expr.True; + if (!e.Function.IsStatic) { + allowance = BplAnd(allowance, Bpl.Expr.Eq(etran.TrExpr(e.Receiver), new Bpl.IdentifierExpr(e.tok, etran.This, predef.RefType))); } - string hint; - switch (e.CoCall) { - case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasSideEffects: - hint = "note that only functions without side effects can be called co-recursively"; - break; - case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasPostcondition: - hint = "note that only functions without any ensures clause can be called co-recursively"; - break; - case FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded: - hint = "note that the call is not sufficiently guarded to be used co-recursively"; - break; - case FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsAreNotAllowedInThisContext: - hint = "note that calls cannot be co-recursive in this context"; - break; - case FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsInDestructiveContext: - hint = "note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts"; - break; - case FunctionCallExpr.CoCallResolution.No: - hint = null; - break; - default: - Contract.Assert(false); // unexpected CoCallResolution - goto case FunctionCallExpr.CoCallResolution.No; // please the compiler + for (int i = 0; i < e.Args.Count; i++) { + Expression ee = e.Args[i]; + Formal ff = e.Function.Formals[i]; + allowance = BplAnd(allowance, Bpl.Expr.Eq(etran.TrExpr(ee), new Bpl.IdentifierExpr(e.tok, ff.AssignUniqueName(currentDeclaration), TrType(ff.Type)))); } - CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, allowance, e.Receiver, substMap, etran, etran, builder, - codeContext.InferredDecreases, hint); } + string hint; + switch (e.CoCall) { + case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasSideEffects: + hint = "note that only functions without side effects can be called co-recursively"; + break; + case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasPostcondition: + hint = "note that only functions without any ensures clause can be called co-recursively"; + break; + case FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded: + hint = "note that the call is not sufficiently guarded to be used co-recursively"; + break; + case FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsAreNotAllowedInThisContext: + hint = "note that calls cannot be co-recursive in this context"; + break; + case FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsInDestructiveContext: + hint = "note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts"; + break; + case FunctionCallExpr.CoCallResolution.No: + hint = null; + break; + default: + Contract.Assert(false); // unexpected CoCallResolution + goto case FunctionCallExpr.CoCallResolution.No; // please the compiler + } + CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, allowance, e.Receiver, substMap, etran, etran, builder, + codeContext.InferredDecreases, hint); } } // all is okay, so allow this function application access to the function's axiom, except if it was okay because of the self-call allowance. @@ -6327,7 +6324,7 @@ namespace Microsoft.Dafny { codeContext is PrefixLemma ? ((PrefixLemma)codeContext).Co : codeContext is IteratorDecl ? ((IteratorDecl)codeContext).Member_MoveNext : codeContext; - if (module.CallGraph.GetSCCRepresentative(method) == module.CallGraph.GetSCCRepresentative(cllr)) { + if (ModuleDefinition.InSameSCC(method, cllr)) { isRecursiveCall = true; } } @@ -8165,8 +8162,7 @@ namespace Microsoft.Dafny { ModuleDefinition module = e.Function.EnclosingClass.Module; if (this.applyLimited_CurrentFunction != null && this.layerIntraCluster != null && - module == applyLimited_CurrentFunction.EnclosingClass.Module && - module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(applyLimited_CurrentFunction)) { + ModuleDefinition.InSameSCC(e.Function, applyLimited_CurrentFunction)) { layerArgument = this.layerIntraCluster; } else { layerArgument = LayerN(layerInterCluster); @@ -10341,8 +10337,7 @@ namespace Microsoft.Dafny { if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; var cof = e.Function as CoPredicate; - if (cof != null && cof.EnclosingClass.Module == module && - module.CallGraph.GetSCCRepresentative(cof) == module.CallGraph.GetSCCRepresentative(coPred)) { + if (cof != null && ModuleDefinition.InSameSCC(cof, coPred)) { expr = cof.CreatePrefixPredicateCall(e, coDepth); } } -- cgit v1.2.3