From 34c67454609985eb4431583de5146b6bc8879843 Mon Sep 17 00:00:00 2001 From: qadeer Date: Sun, 16 Oct 2011 12:05:48 -0700 Subject: revised implementation of proc copy bounding --- Source/VCGeneration/StratifiedVC.cs | 1233 +++++++++++++++++------------------ 1 file changed, 597 insertions(+), 636 deletions(-) diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 4fa339ee..947ed871 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -42,11 +42,6 @@ namespace VC { Contract.Requires(program != null); - if (CommandLineOptions.Clo.ProcedureCopyBound > 0) - { - InstrumentForPCB(program); - } - implName2StratifiedInliningInfo = new Dictionary(); this.GenerateVCsForStratifiedInlining(program); @@ -112,7 +107,6 @@ namespace VC { Contract.Requires(program != null); Checker checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime); - pcbProcToCounterArgLocation = new Dictionary(); foreach (Declaration decl in program.TopLevelDeclarations) { @@ -136,10 +130,6 @@ namespace VC { Contract.Assert(v != null); exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v))); - if (CommandLineOptions.Clo.ProcedureCopyBound > 0 && v.Name == pcbProcToCounter[impl.Name].Name) - { - pcbProcToCounterArgLocation.Add(impl.Name, exprs.Length - 1); - } } foreach (Variable v in proc.InParams) { @@ -163,12 +153,6 @@ namespace VC } } - if (CommandLineOptions.Clo.ProcedureCopyBound > 0) - { - Contract.Assert(pcbProcToCounterArgLocation.Count == pcbProcToCounter.Count, - "Unable to locate all PCB counters"); - } - foreach (var decl in program.TopLevelDeclarations) { var proc = decl as Procedure; @@ -199,59 +183,6 @@ namespace VC } } - private Dictionary pcbProcToCounter; - private Dictionary pcbProcToCounterArgLocation; - - // Instrument program to introduce a counter per procedure - private void InstrumentForPCB(Program program) - { - pcbProcToCounter = new Dictionary(); - foreach (Declaration decl in program.TopLevelDeclarations) - { - Implementation impl = decl as Implementation; - if (impl == null) - continue; - - Procedure proc = cce.NonNull(impl.Proc); - if (proc.FindExprAttribute("inline") == null) continue; - - var g = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, - "counter_" + proc.Name, Bpl.Type.Int)); - - pcbProcToCounter.Add(proc.Name, g); - } - - program.TopLevelDeclarations.AddRange(pcbProcToCounter.Values); - - foreach (Declaration decl in program.TopLevelDeclarations) - { - Implementation impl = decl as Implementation; - if (impl == null) - continue; - - Procedure proc = cce.NonNull(impl.Proc); - if (proc.FindExprAttribute("inline") == null) continue; - - // Each proc can modify all counters (transitively) - foreach (var g in pcbProcToCounter.Values) - { - proc.Modifies.Add(new IdentifierExpr(Token.NoToken, g)); - } - - var k = pcbProcToCounter[proc.Name]; - // free ensures k == old(k) + 1 - proc.Ensures.Add(new Ensures(true, Expr.Eq(Expr.Ident(k), - Expr.Add(Expr.Literal(1), new OldExpr(Token.NoToken, Expr.Ident(k)))))); - - // havoc counter - var cmds = new CmdSeq(); - cmds.Add(new HavocCmd(Token.NoToken, new IdentifierExprSeq(new IdentifierExpr(Token.NoToken, k)))); - cmds.AddRange(impl.Blocks[0].Cmds); - impl.Blocks[0].Cmds = cmds; - - } - } - private void GenerateVCForStratifiedInlining(Program program, StratifiedInliningInfo info, Checker checker) { Contract.Requires(program != null); @@ -309,90 +240,54 @@ namespace VC info.initialized = true; } - // proc name -> k -> interface variables - public static Dictionary>> interfaceVarCopies; - // proc name -> k -> VCExpr - Dictionary> procVcCopies; - // proc name -> k -> CallSite Boolean constant - Dictionary> callSiteConstant; - // VC for ProcCopyBounding - VCExpr procBoundedVC; - - private void CreateProcedureCopies(int K, Program program, FCallHandler calls, StratifiedCheckerInterface checker) - { - interfaceVarCopies = new Dictionary>>(); - procVcCopies = new Dictionary>(); - callSiteConstant = new Dictionary>(); - procBoundedVC = VCExpressionGenerator.True; - - // Duplicate VCs of each procedure K times - foreach (var info in implName2StratifiedInliningInfo.Values) - { - Contract.Assert(info != null); - CreateProcedureCopy(K, program, info, checker); - } - - // Change the procedure calls in each VC - int cnt = FCallHandler.pcbStartingCandidateId; - - // Build a candidate map: proc name -> k -> candidateId - calls.procCopy2Id = new Dictionary, int>(); - - foreach (var kvp in procVcCopies) - { - for (int i = 0; i < kvp.Value.Count; i++) - { - calls.procCopy2Id.Add(Tuple.Create(kvp.Key, i), cnt); - cnt++; - } - } - - // Call Graph - var succ = new Dictionary>(); - var pred = new Dictionary>(); - - foreach (var decl in program.TopLevelDeclarations) - { - var impl = decl as Implementation; - if (impl == null) continue; - foreach (var blk in impl.Blocks) - { - foreach (Cmd cmd in blk.Cmds) - { - var ccmd = cmd as CallCmd; - if (ccmd == null) continue; - if(!succ.ContainsKey(impl.Name)) succ.Add(impl.Name, new HashSet()); - if(!pred.ContainsKey(ccmd.callee)) pred.Add(ccmd.callee, new HashSet()); - succ[impl.Name].Add(ccmd.callee); - pred[ccmd.callee].Add(impl.Name); - } - } - } - - var uniqueCallEdges = new HashSet>(); - foreach (var p in succ.Keys) - { - if (succ[p].Count == 1) uniqueCallEdges.Add(Tuple.Create(p, succ[p].First())); - } - - foreach (var p in pred.Keys) - { - if (pred[p].Count == 1) uniqueCallEdges.Add(Tuple.Create(pred[p].First(), p)); - } - - foreach (var kvp in procVcCopies) - { - for (int i = 0; i < kvp.Value.Count; i++) - { - var id = calls.procCopy2Id[Tuple.Create(kvp.Key, i)]; - calls.setCurrProc(kvp.Key); - calls.currInlineCount = id; - var bm = new BoundingVCMutator(uniqueCallEdges, checker.underlyingChecker.VCExprGen, interfaceVarCopies, callSiteConstant, pcbProcToCounterArgLocation, calls, kvp.Key, i, id); - kvp.Value[i] = bm.Mutate(kvp.Value[i], true); - //checker.AddAxiom(kvp.Value[i]); - procBoundedVC = checker.underlyingChecker.VCExprGen.And(procBoundedVC, kvp.Value[i]); - } - } + public Dictionary> interfaceVarCopies; + public Dictionary> privateVarCopies; + Dictionary procVcCopies; + + public struct CallSite { + public string callerName; + public string calleeName; + public VCExprVar callSiteConstant; + public VCExprNAry callExpr; + + public CallSite(string callerName, string calleeName, VCExprVar callSiteConstant, VCExprNAry callExpr) { + this.callerName = callerName; + this.calleeName = calleeName; + this.callSiteConstant = callSiteConstant; + this.callExpr = callExpr; + } + }; + + static public int callSiteConstantCount = 0; + Dictionary> calleeToCallSites; + Dictionary> callerToCallSites; + + private void CreateProcedureCopies(Implementation impl, Program program, StratifiedCheckerInterface checker, VCExpr vcMain) { + interfaceVarCopies = new Dictionary>(); + privateVarCopies = new Dictionary>(); + procVcCopies = new Dictionary(); + calleeToCallSites = new Dictionary>(); + callerToCallSites = new Dictionary>(); + + interfaceVarCopies[impl.Name] = new List(); + privateVarCopies[impl.Name] = new List(); + calleeToCallSites[impl.Name] = new List(); + callerToCallSites[impl.Name] = new List(); + foreach (var info in implName2StratifiedInliningInfo.Values) { + Contract.Assert(info != null); + interfaceVarCopies[info.impl.Name] = new List(); + privateVarCopies[info.impl.Name] = new List(); + calleeToCallSites[info.impl.Name] = new List(); + callerToCallSites[info.impl.Name] = new List(); + CreateProcedureCopy(info, checker); + } + + BoundingVCMutator bm = new BoundingVCMutator(checker, impl.Name, interfaceVarCopies, calleeToCallSites, callerToCallSites); + procVcCopies[impl.Name] = bm.Mutate(vcMain, true); + foreach (var key in implName2StratifiedInliningInfo.Keys) { + bm = new BoundingVCMutator(checker, key, interfaceVarCopies, calleeToCallSites, callerToCallSites); + procVcCopies[key] = bm.Mutate(procVcCopies[key], true); + } } // Return i if (prefix::i) is in labels @@ -409,223 +304,115 @@ namespace VC return -1; } - public class BoundingVCMutator : MutatingVCExprVisitor - { - // proc name -> k -> interface variables - Dictionary>> interfaceVarCopies; - // proc name -> k -> CallSite Boolean constant - Dictionary> callSiteConstant; - // Call edges (single successor or single predecessor) - HashSet> uniqueCallEdges; - // proc name -> location of the counter in argument - Dictionary pcbProcToCounterArgLocation; - - FCallHandler calls; - int currId; - string currentProc; - int currCopy; - - public BoundingVCMutator(HashSet> uniqueCallEdges, - VCExpressionGenerator gen, - Dictionary>> interfaceVarCopies, - Dictionary> callSiteConstant, - Dictionary pcbProcToCounterArgLocation, - FCallHandler calls, - string currProc, int currCopy, int currId) - : base(gen) - { - Contract.Requires(gen != null); - this.interfaceVarCopies = interfaceVarCopies; - this.callSiteConstant = callSiteConstant; - this.calls = calls; - this.currId = currId; - this.uniqueCallEdges = uniqueCallEdges; - this.currentProc = currProc; - this.currCopy = currCopy; - this.pcbProcToCounterArgLocation = pcbProcToCounterArgLocation; - } - - protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, - List/*!*/ newSubExprs, - bool changed, - bool arg) - { - //Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null); - Contract.Ensures(Contract.Result() != null); - - VCExpr node; - if (changed) - node = Gen.Function(originalNode.Op, - newSubExprs, originalNode.TypeArguments); - else - node = originalNode; - - VCExprLabelOp lop = originalNode.Op as VCExprLabelOp; - if (lop == null) return node; - if (!(node is VCExprNAry)) return node; - - VCExprNAry retnary = (VCExprNAry)node; - Contract.Assert(retnary != null); - string prefix = "si_fcall_"; // from Wlp.ssc::Cmd(...) - if (lop.label.Substring(1).StartsWith(prefix)) - { - - int id = Int32.Parse(lop.label.Substring(prefix.Length + 1)); - Hashtable label2absy = calls.getLabel2absy(); - Absy cmd = label2absy[id] as Absy; - - Contract.Assert(cmd != null); - AssumeCmd acmd = cmd as AssumeCmd; - Contract.Assert(acmd != null); - NAryExpr naryExpr = acmd.Expr as NAryExpr; - Contract.Assert(naryExpr != null); + public class BoundingVCMutator : MutatingVCExprVisitor { + StratifiedCheckerInterface checker; + string implName; + Dictionary> interfaceVarCopies; + Dictionary> calleeToCallSites; + Dictionary> callerToCallSites; + + public BoundingVCMutator( + StratifiedCheckerInterface checker, + string implName, + Dictionary> interfaceVarCopies, + Dictionary> calleeToCallSites, + Dictionary> callerToCallSites) + : base(checker.underlyingChecker.VCExprGen) { + this.checker = checker; + this.implName = implName; + this.interfaceVarCopies = interfaceVarCopies; + this.calleeToCallSites = calleeToCallSites; + this.callerToCallSites = callerToCallSites; + } + + protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, + List/*!*/ newSubExprs, + bool changed, + bool arg) { + Contract.Ensures(Contract.Result() != null); + + VCExpr node; + if (changed) + node = Gen.Function(originalNode.Op, newSubExprs, originalNode.TypeArguments); + else + node = originalNode; - string calleeName = naryExpr.Fun.FunctionName; + VCExprLabelOp lop = originalNode.Op as VCExprLabelOp; + if (lop == null) return node; - VCExprNAry callExpr = retnary[0] as VCExprNAry; - Contract.Assert(callExpr != null); + string prefix = "si_fcall_"; // from Wlp.ssc::Cmd(...) + if (!lop.label.Substring(1).StartsWith(prefix)) return node; - if (interfaceVarCopies.ContainsKey(calleeName)) - { - var op = callExpr.Op as VCExprBoogieFunctionOp; - Contract.Assert(op != null); - Contract.Assert(calleeName == op.Func.Name); - - // construct a unique id for (callexpr, currId) - var bexp = new BoogieCallExpr(naryExpr, currId); - var uid = 0; - if (calls.pcbBoogieExpr2Id.ContainsKey(bexp)) uid = calls.pcbBoogieExpr2Id[bexp]; - else - { - uid = calls.pcbBoogieExpr2Id.Count; - calls.pcbBoogieExpr2Id.Add(bexp, uid); - } + VCExprNAry retnary = node as VCExprNAry; + Debug.Assert(retnary != null); - // substitute - var K = interfaceVarCopies[op.Func.Name].Count; + VCExprNAry callExpr = retnary[0] as VCExprNAry; + Debug.Assert(callExpr != null); - // only call currCopy - var onlyCurrCopy = false; - var edge = Tuple.Create(currentProc, op.Func.Name); - if (uniqueCallEdges.Contains(edge)) onlyCurrCopy = true; - - VCExpr ret = VCExpressionGenerator.False; - for (int k = 0; k < K; k++) - { - if (onlyCurrCopy && k != currCopy) continue; + VCExprBoogieFunctionOp op = callExpr.Op as VCExprBoogieFunctionOp; + if (op == null) return callExpr; - var iv = interfaceVarCopies[op.Func.Name][k]; - Contract.Assert(op.Arity == iv.Count); + if (!interfaceVarCopies.ContainsKey(op.Func.Name)) return callExpr; - VCExpr conj = VCExpressionGenerator.True; - for (int i = 0; i < iv.Count; i++) - { - var c = Gen.Eq(callExpr[i], iv[i]); - conj = Gen.And(conj, c); - } - // Add the counter - var counter = callExpr[pcbProcToCounterArgLocation[op.Func.Name]]; - conj = Gen.And(conj, Gen.Eq(counter, Gen.Integer(BigNum.FromInt(k)))); - // Add the call-site constant - conj = Gen.And(conj, callSiteConstant[op.Func.Name][k]); - - // label the conjunct - conj = Gen.LabelPos(string.Format("PCB_{0}_{1}", uid, k), conj); - ret = Gen.Or(conj, ret); - } + var constName = "pcb_callsite_constant_" + StratifiedVCGen.callSiteConstantCount++; + var constant = Gen.Variable(constName, Bpl.Type.Bool); + checker.underlyingChecker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, constName, Bpl.Type.Bool)), false, null); + CallSite cs = new CallSite(implName, op.Func.Name, constant, callExpr); + calleeToCallSites[op.Func.Name].Add(cs); + callerToCallSites[implName].Add(cs); - return ret; - } - else if (calleeName.StartsWith(recordProcName)) - { - Debug.Assert(callExpr.Length == 1); - Debug.Assert(callExpr[0] != null); - calls.recordExpr2Var[new BoogieCallExpr(naryExpr, currId)] = callExpr[0]; - return callExpr; - } - else - { - return callExpr; - } - } - - // Else, rename label - - string newLabel = calls.RenameAbsyLabel(lop.label); - if (lop.pos) - { - node = Gen.LabelPos(newLabel, retnary[0]); - } - else - { - node = Gen.LabelNeg(newLabel, retnary[0]); - } - - return node; + var iv = interfaceVarCopies[op.Func.Name]; + Contract.Assert(op.Arity == iv.Count); + VCExpr conj = VCExpressionGenerator.True; + for (int i = 0; i < iv.Count; i++) { + var c = Gen.Eq(callExpr[i], iv[i]); + conj = Gen.And(conj, c); } - } // end BoundingVCMutator - - private void CreateProcedureCopy(int K, Program program, StratifiedInliningInfo info, StratifiedCheckerInterface checker) - { - var translator = checker.underlyingChecker.TheoremProver.Context.BoogieExprTranslator; - var Gen = checker.underlyingChecker.VCExprGen; - - interfaceVarCopies.Add(info.impl.Name, new List>()); - procVcCopies.Add(info.impl.Name, new List()); - callSiteConstant.Add(info.impl.Name, new List()); - - for (int k = 0; k < K; k++) - { - var expr = info.vcexpr; - // Instantiate the interface variables - Dictionary substForallDict = new Dictionary(); - var ls = new List(); - for (int i = 0; i < info.interfaceExprVars.Count; i++) - { - var v = info.interfaceExprVars[i]; - string newName = v.Name + "_iv_" + k.ToString() + "_" + newVarCnt.ToString(); - newVarCnt++; - var vp = Gen.Variable(newName, v.Type); - substForallDict.Add(v, vp); - ls.Add(vp); - } - interfaceVarCopies[info.impl.Name].Add(ls); - VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary()); - - SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(Gen); - Contract.Assert(subst != null); - expr = subst.Mutate(expr, substForall); + return Gen.Implies(constant, conj); + } - // Instantiate and declare the private variables - Dictionary substExistsDict = new Dictionary(); - foreach (VCExprVar v in info.privateVars) - { - Contract.Assert(v != null); - string newName = v.Name + "_pv_" + k.ToString() + "_" + newVarCnt.ToString(); - newVarCnt++; - checker.underlyingChecker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null); - substExistsDict.Add(v, Gen.Variable(newName, v.Type)); - } - VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary()); - - subst = new SubstitutingVCExprVisitor(Gen); - expr = subst.Mutate(expr, substExists); - - // create a constant for call sites - string cscName = "pcb_csc_" + k.ToString() + "_" + newVarCnt.ToString(); - newVarCnt++; - checker.underlyingChecker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, cscName, Microsoft.Boogie.Type.Bool)), false, null); - var csc = Gen.Variable(cscName, Microsoft.Boogie.Type.Bool); - callSiteConstant[info.impl.Name].Add(csc); + } // end BoundingVCMutator - expr = Gen.Implies(csc, expr); - procVcCopies[info.impl.Name].Add(expr); - } + private void CreateProcedureCopy(StratifiedInliningInfo info, StratifiedCheckerInterface checker) { + var translator = checker.underlyingChecker.TheoremProver.Context.BoogieExprTranslator; + var Gen = checker.underlyingChecker.VCExprGen; + var expr = info.vcexpr; + + // Instantiate the interface variables + Dictionary substForallDict = new Dictionary(); + for (int i = 0; i < info.interfaceExprVars.Count; i++) { + var v = info.interfaceExprVars[i]; + string newName = v.Name + "_iv_" + newVarCnt.ToString(); + newVarCnt++; + var vp = Gen.Variable(newName, v.Type); + substForallDict.Add(v, vp); + interfaceVarCopies[info.impl.Name].Add(vp); + } + VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary()); + SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(Gen); + Contract.Assert(subst != null); + expr = subst.Mutate(expr, substForall); + + // Instantiate and declare the private variables + Dictionary substExistsDict = new Dictionary(); + foreach (VCExprVar v in info.privateVars) { + Contract.Assert(v != null); + string newName = v.Name + "_pv_" + newVarCnt.ToString(); + newVarCnt++; + checker.underlyingChecker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null); + var vp = Gen.Variable(newName, v.Type); + substExistsDict.Add(v, vp); + privateVarCopies[info.impl.Name].Add(vp); + } + VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary()); + subst = new SubstitutingVCExprVisitor(Gen); + expr = subst.Mutate(expr, substExists); + + procVcCopies[info.impl.Name] = expr; } - public class CoverageGraphManager { public static int timeStamp = 0; @@ -1123,128 +910,113 @@ namespace VC } - public class ApiChecker : StratifiedCheckerInterface - { - // The VC of main - private VCExpr vcMain; - // Error reporter (stores models) - private ProverInterface.ErrorHandler reporter; - // The theorem prover interface - public Checker checker; - // stores the number of axioms pushed since pervious backtracking point - private List numAxiomsPushed; - // Api-based theorem prover - private ApiProverInterface TheoremProver; - // Use checkAssumptions? - public static bool UseCheckAssumptions = true; - - public ApiChecker(VCExpr vcMain, ProverInterface.ErrorHandler reporter, Checker checker) - { - this.vcMain = vcMain; - this.reporter = reporter; - this.checker = checker; - this.underlyingChecker = checker; - numAxiomsPushed = new List(); - numQueries = 0; - TheoremProver = checker.TheoremProver as ApiProverInterface; - Debug.Assert(TheoremProver != null); - - // Add main to the TP stack - TheoremProver.Assert(vcMain, false); - } - - public override void updateMainVC(VCExpr vcMain) - { - throw new NotImplementedException("Stratified non-incremental search is not yet supported with z3api"); - } - - public override Outcome CheckVC() - { - Contract.EnsuresOnThrow(true); - - TheoremProver.AssertAxioms(); - TheoremProver.Check(); - ProverInterface.Outcome outcome = TheoremProver.CheckOutcome(reporter); - numQueries++; - - switch (outcome) - { - case ProverInterface.Outcome.Valid: - return Outcome.Correct; - case ProverInterface.Outcome.Invalid: - return Outcome.Errors; - case ProverInterface.Outcome.OutOfMemory: - return Outcome.OutOfMemory; - case ProverInterface.Outcome.TimeOut: - return Outcome.TimedOut; - case ProverInterface.Outcome.Undetermined: - return Outcome.Inconclusive; - default: - Contract.Assert(false); - throw new cce.UnreachableException(); - } - - } - - public override void Push() - { - TheoremProver.Push(); - } - - public override void Pop() - { - TheoremProver.AssertAxioms(); - TheoremProver.Pop(); - } - - public override void AddAxiom(VCExpr vc) - { - TheoremProver.Assert(vc, true); - } + public class ApiChecker : StratifiedCheckerInterface { + // The VC of main + private VCExpr vcMain; + // Error reporter (stores models) + private ProverInterface.ErrorHandler reporter; + // The theorem prover interface + public Checker checker; + // stores the number of axioms pushed since pervious backtracking point + private List numAxiomsPushed; + // Api-based theorem prover + private ApiProverInterface TheoremProver; + // Use checkAssumptions? + public static bool UseCheckAssumptions = true; + + public ApiChecker(VCExpr vcMain, ProverInterface.ErrorHandler reporter, Checker checker) { + this.vcMain = vcMain; + this.reporter = reporter; + this.checker = checker; + this.underlyingChecker = checker; + numAxiomsPushed = new List(); + numQueries = 0; + TheoremProver = checker.TheoremProver as ApiProverInterface; + Debug.Assert(TheoremProver != null); + + // Add main to the TP stack + TheoremProver.Assert(vcMain, false); + } + + public override void updateMainVC(VCExpr vcMain) { + throw new NotImplementedException("Stratified non-incremental search is not yet supported with z3api"); + } + + public override Outcome CheckVC() { + Contract.EnsuresOnThrow(true); - public override void LogComment(string str) - { - checker.TheoremProver.LogComment(str); + TheoremProver.AssertAxioms(); + TheoremProver.Check(); + ProverInterface.Outcome outcome = TheoremProver.CheckOutcome(reporter); + numQueries++; + + switch (outcome) { + case ProverInterface.Outcome.Valid: + return Outcome.Correct; + case ProverInterface.Outcome.Invalid: + return Outcome.Errors; + case ProverInterface.Outcome.OutOfMemory: + return Outcome.OutOfMemory; + case ProverInterface.Outcome.TimeOut: + return Outcome.TimedOut; + case ProverInterface.Outcome.Undetermined: + return Outcome.Inconclusive; + default: + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } + + public override void Push() { + TheoremProver.Push(); + } + + public override void Pop() { + TheoremProver.AssertAxioms(); + TheoremProver.Pop(); + } + + public override void AddAxiom(VCExpr vc) { + TheoremProver.Assert(vc, true); + } + + public override void LogComment(string str) { + checker.TheoremProver.LogComment(str); + } + + public override Outcome CheckAssumptions(List assumptions, out List unsatCore) { + if (!UseCheckAssumptions) { + return base.CheckAssumptions(assumptions, out unsatCore); } - public override Outcome CheckAssumptions(List assumptions, out List unsatCore) - { - if (!UseCheckAssumptions) - { - return base.CheckAssumptions(assumptions, out unsatCore); - } - - if (assumptions.Count == 0) - { - unsatCore = new List(); - return CheckVC(); - } - - //TheoremProver.Push(); - TheoremProver.AssertAxioms(); - TheoremProver.CheckAssumptions(assumptions, out unsatCore); - ProverInterface.Outcome outcome = TheoremProver.CheckOutcome(reporter); - //TheoremProver.Pop(); - numQueries++; - - switch (outcome) - { - case ProverInterface.Outcome.Valid: - return Outcome.Correct; - case ProverInterface.Outcome.Invalid: - return Outcome.Errors; - case ProverInterface.Outcome.OutOfMemory: - return Outcome.OutOfMemory; - case ProverInterface.Outcome.TimeOut: - return Outcome.TimedOut; - case ProverInterface.Outcome.Undetermined: - return Outcome.Inconclusive; - default: - Contract.Assert(false); - throw new cce.UnreachableException(); - } - } - + if (assumptions.Count == 0) { + unsatCore = new List(); + return CheckVC(); + } + + //TheoremProver.Push(); + TheoremProver.AssertAxioms(); + TheoremProver.CheckAssumptions(assumptions, out unsatCore); + ProverInterface.Outcome outcome = TheoremProver.CheckOutcome(reporter); + //TheoremProver.Pop(); + numQueries++; + + switch (outcome) { + case ProverInterface.Outcome.Valid: + return Outcome.Correct; + case ProverInterface.Outcome.Invalid: + return Outcome.Errors; + case ProverInterface.Outcome.OutOfMemory: + return Outcome.OutOfMemory; + case ProverInterface.Outcome.TimeOut: + return Outcome.TimedOut; + case ProverInterface.Outcome.Undetermined: + return Outcome.Inconclusive; + default: + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } } // Store important information related to a single VerifyImplementation query @@ -1515,32 +1287,6 @@ namespace VC } } - private bool checkIfRecursive(Implementation impl, Program program) - { - var impls = new List(); - foreach (var decl in program.TopLevelDeclarations) - if (decl is Implementation) impls.Add(decl as Implementation); - impls.Add(impl); - - var callGraph = new Graph(); - callGraph.AddSource(impl.Name); - - foreach (var proc in impls) - { - foreach (var blk in proc.Blocks) - { - foreach (Cmd cmd in blk.Cmds) - { - var ccmd = cmd as CallCmd; - if (ccmd == null) continue; - callGraph.AddEdge(proc.Name, ccmd.callee); - } - } - } - - return !Graph.Acyclic(callGraph, impl.Name); - } - public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback) { Contract.EnsuresOnThrow(true); @@ -1572,13 +1318,6 @@ namespace VC break; } - if (CommandLineOptions.Clo.ProcedureCopyBound > 0) - { - // We're using procedure-copy bounding. We need to eagerly generate - // VCs of all procedures - createVConDemand = false; - } - #endregion // Get the checker @@ -1597,7 +1336,7 @@ namespace VC Contract.Assert(implName2StratifiedInliningInfo != null); this.program = program; - if (!createVConDemand) + if (!createVConDemand || CommandLineOptions.Clo.ProcedureCopyBound > 0) { foreach (StratifiedInliningInfo info in implName2StratifiedInliningInfo.Values) { @@ -1610,23 +1349,12 @@ namespace VC VCExpr vc; StratifiedInliningErrorReporter reporter; Hashtable/**/ mainLabel2absy; - if (CommandLineOptions.Clo.ProcedureCopyBound > 0) - { - // Initialize all counters to 0 - Debug.Assert(pcbProcToCounter != null && pcbProcToCounter.Count == implName2StratifiedInliningInfo.Count); - - Expr expr = Expr.Literal(true); - foreach (var counter in pcbProcToCounter.Values) - { - expr = Expr.And(expr, Expr.Eq(Expr.Literal(0), Expr.Ident(counter))); - } - var cmds = new CmdSeq(); - cmds.Add(new AssumeCmd(Token.NoToken, expr)); - cmds.AddRange(impl.Blocks[0].Cmds); - impl.Blocks[0].Cmds = cmds; - } GetVC(impl, program, callback, out vc, out mainLabel2absy, out reporter); + if (CommandLineOptions.Clo.ProcedureCopyBound > 0) { + return SuperAwesomeMethod(checker, impl, vc); + } + // Find all procedure calls in vc and put labels on them FCallHandler calls = new FCallHandler(checker.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy); calls.setCurrProcAsMain(); @@ -1641,7 +1369,7 @@ namespace VC var vState = new VerificationState(vc, calls, reporter, checker); vState.vcSize += SizeComputingVisitor.ComputeSize(vc); vState.coverageManager = coverageManager; - + // We'll restore the original state of the theorem prover at the end // of this procedure vState.checker.Push(); @@ -1691,13 +1419,6 @@ namespace VC } #endregion - // Procedure-Copy-Bounding VC - if (CommandLineOptions.Clo.ProcedureCopyBound > 0) - { - if (checkIfRecursive(impl, program)) Console.WriteLine("Program is recursive!"); - CreateProcedureCopies(CommandLineOptions.Clo.ProcedureCopyBound, program, calls, vState.checker); - } - // Under-approx query is only needed if something was inlined since // the last time an under-approx query was made // TODO: introduce this @@ -1759,25 +1480,6 @@ namespace VC // Stratified Step ret = stratifiedStep(bound, vState); iters++; - // AL: temp - if (CommandLineOptions.Clo.ProcedureCopyBound > 0) - { - if (ret == Outcome.Errors) - { - done = 2; - continue; - } - else if (ret == Outcome.Correct) - { - done = 1; - continue; - } - else - { - done = 3; - continue; - } - } // Sorry, out of luck (time/memory) if (ret == Outcome.Inconclusive || ret == Outcome.OutOfMemory || ret == Outcome.TimedOut) @@ -1880,14 +1582,335 @@ namespace VC } } - if (CommandLineOptions.Clo.ProcedureCopyBound > 0) - { - Console.WriteLine("Num iters: {0}", iters); - Console.WriteLine("PCB succeeded: {0}", reporter.procBoundingMode); - } return ret; } + public class PCBInliner : MutatingVCExprVisitor { + private VCExprVar callSiteConstant; + private VCExpr expr; + + public PCBInliner(VCExpressionGenerator gen, VCExprVar callSiteConstant, VCExpr expr) + : base(gen) { + Contract.Requires(gen != null); + this.callSiteConstant = callSiteConstant; + this.expr = expr; + } + + protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, + List/*!*/ newSubExprs, + bool changed, + bool arg) { + Contract.Ensures(Contract.Result() != null); + + VCExpr ret; + if (changed) + ret = Gen.Function(originalNode.Op, newSubExprs, originalNode.TypeArguments); + else + ret = originalNode; + + VCExprNAry naryExpr = ret as VCExprNAry; + if (naryExpr == null) return ret; + if (naryExpr.Op != VCExpressionGenerator.ImpliesOp) return ret; + if (naryExpr[0] != callSiteConstant) return ret; + return expr; + } + + } // end PCBInliner + + private void InlineCallSite(CallSite cs, StratifiedCheckerInterface checker) { + var Gen = checker.underlyingChecker.VCExprGen; + var callee = cs.calleeName; + var caller = cs.callerName; + var expr = cs.callExpr; + VCExpr expansion = procVcCopies[callee]; + List interfaceExprVars = interfaceVarCopies[callee]; + List privateVars = privateVarCopies[callee]; + + // Instantiate the "forall" variables + Dictionary substForallDict = new Dictionary(); + Contract.Assert(interfaceExprVars.Count == expr.Length); + for (int i = 0; i < interfaceExprVars.Count; i++) { + substForallDict.Add(interfaceExprVars[i], expr[i]); + } + VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary()); + SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(Gen); + expansion = subst.Mutate(expansion, substForall); + + // Instantiate and declare the "exists" variables + Dictionary substExistsDict = new Dictionary(); + for (int i = 0; i < privateVars.Count; i++) { + VCExprVar v = privateVars[i]; + string newName = v.Name + "_si_" + newVarCnt.ToString(); + newVarCnt++; + checker.underlyingChecker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null); + var vp = Gen.Variable(newName, v.Type); + substExistsDict.Add(v, vp); + privateVarCopies[cs.callerName].Add(vp); + } + VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary()); + subst = new SubstitutingVCExprVisitor(Gen); + expansion = subst.Mutate(expansion, substExists); + + Dictionary substCallSiteConstantDict = new Dictionary(); + foreach (CallSite oldSite in callerToCallSites[callee]) { + var newConstName = "pcb_callsite_constant_" + StratifiedVCGen.callSiteConstantCount++; + var newConstant = Gen.Variable(newConstName, Bpl.Type.Bool); + checker.underlyingChecker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newConstName, Bpl.Type.Bool)), false, null); + substCallSiteConstantDict.Add(oldSite.callSiteConstant, newConstant); + subst = new SubstitutingVCExprVisitor(Gen); + var newCallExpr = subst.Mutate(oldSite.callExpr, substForall); + subst = new SubstitutingVCExprVisitor(Gen); + newCallExpr = subst.Mutate(newCallExpr, substExists); + var newSite = new CallSite(caller, oldSite.calleeName, newConstant, (VCExprNAry)newCallExpr); + callerToCallSites[caller].Add(newSite); + calleeToCallSites[oldSite.calleeName].Add(newSite); + } + VCExprSubstitution substCallSiteConstant = new VCExprSubstitution(substCallSiteConstantDict, new Dictionary()); + subst = new SubstitutingVCExprVisitor(Gen); + expansion = subst.Mutate(expansion, substCallSiteConstant); + + PCBInliner inliner = new PCBInliner(Gen, cs.callSiteConstant, expansion); + procVcCopies[cs.callerName] = inliner.Mutate(procVcCopies[cs.callerName], true); + + callerToCallSites[caller].Remove(cs); + calleeToCallSites[callee].Remove(cs); + } + + private Outcome FindUnsatCore(Implementation impl, StratifiedCheckerInterface checker, VCExpressionGenerator Gen, PCBErrorReporter reporter, List assumptions, out HashSet unsatCore) { + Helpers.ExtraTraceInformation("Number of assumptions = " + assumptions.Count); + + if (checker is NormalChecker) { + Outcome ret; + unsatCore = null; + for (int i = 0; i < assumptions.Count; i++) { + checker.Push(); + checker.AddAxiom(assumptions[i]); + } + + ret = checker.CheckVC(); + if (ret == Outcome.Errors) { + for (int i = 0; i < assumptions.Count; i++) { + checker.Pop(); + } + return ret; + } + + Helpers.ExtraTraceInformation("VC checked"); + + reporter.unsatCoreMode = true; + VCExpr curr = VCExpressionGenerator.True; + unsatCore = new HashSet(); + int index = assumptions.Count; + while (index > 0) { + checker.Pop(); + + checker.Push(); + checker.AddAxiom(curr); + ret = checker.CheckVC(); + checker.Pop(); + + if (ret == Outcome.Errors) { + VCExprVar assumption = (VCExprVar)assumptions[index - 1]; + curr = Gen.And(assumption, curr); + unsatCore.Add(assumption); + } + index--; + } + reporter.unsatCoreMode = false; + Helpers.ExtraTraceInformation("Number of elements in unsat core = " + unsatCore.Count); + return Outcome.Correct; + } + else { + Debug.Assert(checker is ApiChecker); + unsatCore = null; + List unsatCoreIndices; + Outcome ret; + ret = checker.CheckAssumptions(assumptions, out unsatCoreIndices); + if (ret == Outcome.Errors) return ret; + unsatCore = new HashSet(); + for (int i = 0; i < unsatCoreIndices.Count; i++) { + unsatCore.Add((VCExprVar)assumptions[unsatCoreIndices[i]]); + } + + Helpers.ExtraTraceInformation("Number of elements in unsat core = " + unsatCore.Count); + + HashSet reachableCallSites = new HashSet(); + Stack stack = new Stack(); + HashSet set = new HashSet(); + stack.Push(impl.Name); + while (stack.Count > 0) { + string caller = stack.Peek(); + stack.Pop(); + if (set.Contains(caller)) continue; + set.Add(caller); + foreach (CallSite cs in callerToCallSites[caller]) { + if (unsatCore.Contains(cs.callSiteConstant)) { + reachableCallSites.Add(cs); + stack.Push(cs.calleeName); + } + } + } + + Graph callGraph = new Graph(); + foreach (CallSite cs1 in reachableCallSites) { + callGraph.AddSource(cs1); + foreach (CallSite cs2 in calleeToCallSites[cs1.callerName]) { + if (reachableCallSites.Contains(cs2)) { + callGraph.AddEdge(cs1, cs2); + } + } + } + + List sortedCallSites = new List(); + foreach (CallSite cs in callGraph.TopologicalSort()) { + checker.Push(); + checker.AddAxiom(cs.callSiteConstant); + sortedCallSites.Add(cs); + } + + ret = checker.CheckVC(); + Debug.Assert(ret == Outcome.Correct); + + reporter.unsatCoreMode = true; + VCExpr curr = VCExpressionGenerator.True; + HashSet relevantCallSites = new HashSet(); + HashSet relevantUnsatCore = new HashSet(); + int index = sortedCallSites.Count; + int queries = 0; + while (index > 0) { + checker.Pop(); + CallSite cs = sortedCallSites[index - 1]; + //Helpers.ExtraTraceInformation("Examining callsite: " + "caller = " + cs.callerName + ", callee = " + cs.calleeName); + + bool check = (cs.callerName == impl.Name); + foreach (CallSite x in calleeToCallSites[cs.callerName]) { + check = check || relevantCallSites.Contains(x); + } + if (check) { + queries++; + checker.Push(); + checker.AddAxiom(curr); + ret = checker.CheckVC(); + checker.Pop(); + + if (ret == Outcome.Errors) { + curr = Gen.And(cs.callSiteConstant, curr); + relevantCallSites.Add(cs); + relevantUnsatCore.Add(cs.callSiteConstant); + } + } + index--; + } + reporter.unsatCoreMode = false; + + unsatCore = relevantUnsatCore; + Helpers.ExtraTraceInformation("Number of queries = " + queries); + Helpers.ExtraTraceInformation("Unsat core after pruning = " + unsatCore.Count); + return Outcome.Correct; + } + } + + HashSet ComputeReachableImplementations(Implementation impl) { + Stack stack = new Stack(); + HashSet set = new HashSet(); + stack.Push(impl.Name); + while (stack.Count > 0) { + string caller = stack.Peek(); + stack.Pop(); + if (set.Contains(caller)) continue; + set.Add(caller); + foreach (CallSite cs in callerToCallSites[caller]) { + stack.Push(cs.calleeName); + } + } + return set; + } + + private Outcome SuperAwesomeMethod(Checker underlyingChecker, Implementation impl, VCExpr vcMain) { + // Create the call graph + // while (true) + // 1. Create boolean variables for each call site + // 2. Create the implications both at the top level and at the call sites + // 3. Verify using CheckAssumptions + // 4. Traverse call graph bottom up. For each procedure, inline all incoming edges in the unsatCore and update call graph + // 5. If no node had more than one incoming edges set to true, break + + var Gen = underlyingChecker.VCExprGen; + PCBErrorReporter reporter = new PCBErrorReporter(impl); + StratifiedCheckerInterface checker; + if (underlyingChecker.TheoremProver is ApiProverInterface) { + checker = new ApiChecker(VCExpressionGenerator.False, reporter, underlyingChecker); + } + else { + checker = new NormalChecker(null, reporter, underlyingChecker); + } + CreateProcedureCopies(impl, program, checker, vcMain); + + int iter = 0; + while (true) { + Helpers.ExtraTraceInformation("Iteration number " + iter++); + + Outcome ret; + if (checker is NormalChecker) { + checker.updateMainVC(procVcCopies[impl.Name]); + } + + checker.Push(); + + var reachableImpls = ComputeReachableImplementations(impl); + var assumptions = new List(); + foreach (string name in reachableImpls) { + VCExpr expr = procVcCopies[name]; + if (name == impl.Name) { + if (checker is ApiChecker) { + checker.AddAxiom(Gen.Not(expr)); + } + continue; + } + var cscExpr = VCExpressionGenerator.False; + foreach (CallSite callSite in calleeToCallSites[name]) { + if (reachableImpls.Contains(callSite.callerName)) { + assumptions.Add(callSite.callSiteConstant); + cscExpr = Gen.Or(callSite.callSiteConstant, cscExpr); + } + } + expr = Gen.Implies(cscExpr, expr); + checker.AddAxiom(expr); + } + HashSet unsatCore; + ret = FindUnsatCore(impl, checker, Gen, reporter, assumptions, out unsatCore); + + checker.Pop(); + + if (ret == Outcome.Errors) return ret; + + Graph callGraph = new Graph(); + foreach (string name in calleeToCallSites.Keys) { + callGraph.AddSource(name); + foreach (CallSite cs in calleeToCallSites[name]) { + callGraph.AddEdge(name, cs.callerName); + } + } + + bool verified = true; + foreach (string name in callGraph.TopologicalSort()) { + HashSet toBeInlined = new HashSet(); + foreach (CallSite cs in calleeToCallSites[name]) { + if (unsatCore.Contains(cs.callSiteConstant)) { + Debug.Assert(name == cs.calleeName); + toBeInlined.Add(cs); + } + } + verified = verified && toBeInlined.Count <= 1; + foreach (CallSite cs in toBeInlined) { + InlineCallSite(cs, checker); + } + } + + if (verified) return Outcome.Correct; + } + } + // A step of the stratified inlining algorithm: both under-approx and over-approx queries private Outcome stratifiedStep(int bound, VerificationState vState) { @@ -1939,7 +1962,7 @@ namespace VC return ret; } - if (ret != Outcome.Correct && ret != Outcome.Errors) + if (ret != Outcome.Correct) { // The query ran out of memory or time, that's it, // we cannot do better. Give up! @@ -1949,77 +1972,9 @@ namespace VC // If we didn't underapproximate, then we're done if (calls.currCandidates.Count == 0) { - Contract.Assert(ret == Outcome.Correct); return ret; } - Contract.Assert(ret == Outcome.Correct); - - if (CommandLineOptions.Clo.ProcedureCopyBound > 0 && calls.currCandidates.Count > 0) - { - // Connect candidates with Proc-Copy VC - reporter.procBoundingMode = true; - checker.Push(); - // TODO: Still block candidates who have reached the recursion bound? - - var Gen = checker.underlyingChecker.VCExprGen; - VCExpr connectVC = VCExpressionGenerator.True; - foreach (var id in calls.currCandidates) - { - var disj = VCExpressionGenerator.False; - var iv_expr = calls.id2Candidate[id]; - var bop = iv_expr.Op as VCExprBoogieFunctionOp; - Contract.Assert(bop != null); - - for (int k = 0; k < CommandLineOptions.Clo.ProcedureCopyBound; k++) - { - Contract.Assert(iv_expr.Arity == interfaceVarCopies[bop.Func.Name][k].Count); - var conj = VCExpressionGenerator.True; - for (int i = 0; i < iv_expr.Arity; i++) - { - var v1 = iv_expr[i]; - var v2 = interfaceVarCopies[bop.Func.Name][k][i]; - Contract.Assert(v1 != null && v2 != null); - conj = Gen.And(conj, Gen.Eq(v1, v2)); - } - // Add the counter - var counter = iv_expr[pcbProcToCounterArgLocation[bop.Func.Name]]; - conj = Gen.And(conj, Gen.Eq(counter, Gen.Integer(BigNum.FromInt(k)))); - // Call site constant - conj = Gen.And(conj, callSiteConstant[bop.Func.Name][k]); - // label the conjunct - conj = Gen.LabelPos(string.Format("PCB_CONNECT_{0}_{1}", id, k), conj); - disj = Gen.Or(disj, conj); - } - connectVC = Gen.And(connectVC, Gen.Implies(calls.id2ControlVar[id], disj)); - } - checker.AddAxiom(Gen.And(connectVC, procBoundedVC)); - ret = checker.CheckVC(); - - checker.Pop(); - - if (ret == Outcome.Errors) - { - // don't reset reporter.procBoundingMode here - // (for statistics purposes) - return ret; - } - - reporter.procBoundingMode = false; - - // AL: temp - return ret; - - if (ret != Outcome.Correct && ret != Outcome.Errors) - { - // The query ran out of memory or time, that's it, - // we cannot do better. Give up! - return ret; - } - - Contract.Assert(ret == Outcome.Correct); - } - checker.LogComment(";;;;;;;;;;;; Overapprox mode begin ;;;;;;;;;;"); // Over-approx query @@ -2295,19 +2250,9 @@ namespace VC vc = GenerateVC(impl, null, out label2absy, checker); - /* - ErrorReporter errReporter; - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) { - errReporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, callback, implName2LazyInliningInfo, checker.TheoremProver.Context, program); - } else { - errReporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, callback, implName2LazyInliningInfo, checker.TheoremProver.Context, program); - } - */ - reporter = new StratifiedInliningErrorReporter( cce.NonNull(implName2StratifiedInliningInfo), checker.TheoremProver, callback, mvInfo, checker.TheoremProver.Context, gotoCmdOrigins, program, impl); - } @@ -2791,8 +2736,7 @@ namespace VC VCExpr ret; if (changed) - ret = Gen.Function(originalNode.Op, - newSubExprs, originalNode.TypeArguments); + ret = Gen.Function(originalNode.Op, newSubExprs, originalNode.TypeArguments); else ret = originalNode; @@ -2822,6 +2766,21 @@ namespace VC } } + public class PCBErrorReporter : ProverInterface.ErrorHandler { + public bool unsatCoreMode; + public Implementation mainImpl; + + public PCBErrorReporter(Implementation impl) { + this.unsatCoreMode = false; + this.mainImpl = impl; + } + + public override void OnModel(IList labels, ErrorModel errModel) { + if (unsatCoreMode) return; + Console.WriteLine("Error in " + mainImpl.Name); + } + } + public class StratifiedInliningErrorReporter : ProverInterface.ErrorHandler { Dictionary/*!*/ implName2StratifiedInliningInfo; @@ -3002,6 +2961,8 @@ namespace VC public override void OnModel(IList/*!*/ labels, ErrorModel errModel) { + //if (procBoundingMode) return; // shaz hack + candidatesToExpand = new List(); //Contract.Requires(cce.NonNullElements(labels)); -- cgit v1.2.3