From 53877d7a90e870d6d95d08dfd86209e315101e09 Mon Sep 17 00:00:00 2001 From: qadeer Date: Sat, 28 Apr 2012 17:11:48 -0700 Subject: removed proccopybounding code stratified inliinig is now run always with /doNotUseLabels --- Source/Core/CommandLineOptions.cs | 7 - Source/Provers/SMTLib/ProverInterface.cs | 2 +- Source/VCGeneration/StratifiedVC.cs | 812 +------------------------------ Test/stratifiedinline/runtest.bat | 20 +- 4 files changed, 12 insertions(+), 829 deletions(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index d9213c47..f2148158 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -559,7 +559,6 @@ namespace Microsoft.Boogie { public Inlining ProcedureInlining = Inlining.Assume; public bool PrintInlined = false; public bool ExtractLoops = false; - public int ProcedureCopyBound = 0; public int StratifiedInlining = 0; public int StratifiedInliningOption = 0; public bool StratifiedInliningWithoutModels = false; // disable model generation for SI @@ -976,12 +975,6 @@ namespace Microsoft.Boogie { } return true; - case "procCopyBound": - if (ps.ConfirmArgumentCount(1)) { - ProcedureCopyBound = Int32.Parse(args[ps.i]); - } - return true; - case "stratifiedInline": if (ps.ConfirmArgumentCount(1)) { switch (args[ps.i]) { diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 014af458..48791385 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -85,7 +85,7 @@ namespace Microsoft.Boogie.SMTLib { currentLogFile = OpenOutputFile(""); } - if (CommandLineOptions.Clo.ProcedureCopyBound > 0 || CommandLineOptions.Clo.ContractInfer) + if (CommandLineOptions.Clo.ContractInfer) { SendThisVC("(set-option :produce-unsat-cores true)"); this.usingUnsatCore = true; diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 3bbe92a1..18ff4c87 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -115,7 +115,6 @@ namespace VC public Function function; public Variable controlFlowVariable; public List interfaceVars; - public List> interfaceVarCopies; public Expr assertExpr; public VCExpr vcexpr; public List privateVars; @@ -199,16 +198,6 @@ namespace VC this.function = new Function(Token.NoToken, proc.Name, functionInterfaceVars, returnVar); ctxt.DeclareFunction(this.function, ""); - interfaceVarCopies = new List>(); - int temp = 0; - for (int i = 0; i < CommandLineOptions.Clo.ProcedureCopyBound; i++) { - interfaceVarCopies.Add(new List()); - foreach (Variable v in interfaceVars) { - Constant constant = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, v.Name + temp++, v.TypedIdent.Type)); - interfaceVarCopies[i].Add(constant); - } - } - inline_cnt = 0; privateVars = new List(); interfaceExprVars = new List(); @@ -362,10 +351,6 @@ namespace VC info.initialized = true; } - public Dictionary> interfaceVarCopies; - public Dictionary> privateVarCopies; - Dictionary procVcCopies; - public struct CallSite { public string callerName; public string calleeName; @@ -380,52 +365,6 @@ namespace VC } }; - static public int callSiteConstantCount = 0; - Dictionary> calleeToCallSites; - Dictionary> callerToCallSites; - - private void CreateProcedureCopies(Implementation impl, Program program, ApiChecker 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 - public static int pcbFindLabel(IList labels, string prefix) - { - foreach (var s in labels) - { - if (s.StartsWith(prefix)) - { - return Int32.Parse(s.Substring(prefix.Length)); - } - } - Contract.Assert(false); - return -1; - } - public class SummaryComputation { // The verification state @@ -667,124 +606,12 @@ namespace VC ret.Add(root); return ret; } - - } - - public class BoundingVCMutator : MutatingVCExprVisitor { - ApiChecker checker; - string implName; - Dictionary> interfaceVarCopies; - Dictionary> calleeToCallSites; - Dictionary> callerToCallSites; - - public BoundingVCMutator( - ApiChecker 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; - - VCExprLabelOp lop = originalNode.Op as VCExprLabelOp; - if (lop == null) return node; - - string prefix = "si_fcall_"; // from Wlp.ssc::Cmd(...) - if (!lop.label.Substring(1).StartsWith(prefix)) return node; - - VCExprNAry retnary = node as VCExprNAry; - Debug.Assert(retnary != null); - - VCExprNAry callExpr = retnary[0] as VCExprNAry; - Debug.Assert(callExpr != null); - - VCExprBoogieFunctionOp op = callExpr.Op as VCExprBoogieFunctionOp; - if (op == null) return callExpr; - - if (!interfaceVarCopies.ContainsKey(op.Func.Name)) return callExpr; - - 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); - - 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); - } - - return Gen.Implies(constant, conj); - } - - } // end BoundingVCMutator - - private void CreateProcedureCopy(StratifiedInliningInfo info, ApiChecker 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; - public class Task { public enum TaskType { NONE, STEP, INLINE, BLOCK, REACHABLE }; @@ -1629,7 +1456,7 @@ namespace VC Contract.Assert(implName2StratifiedInliningInfo != null); this.program = program; - if (!createVConDemand || CommandLineOptions.Clo.ProcedureCopyBound > 0) + if (!createVConDemand) { foreach (StratifiedInliningInfo info in implName2StratifiedInliningInfo.Values) { @@ -1937,347 +1764,6 @@ namespace VC 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, ApiChecker checker) - { - var Gen = checker.underlyingChecker.VCExprGen; - var callee = cs.calleeName; - var caller = cs.callerName; - Helpers.ExtraTraceInformation("inlining call from " + caller + "to " + callee); - 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); - } - -#if SuperAwesomeMethod - private Outcome FindUnsatCoreInMainCallees(Implementation impl, ApiChecker checker, VCExpressionGenerator Gen, PCBErrorReporter reporter, List assumptions, out HashSet unsatCore) - { - 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(); - HashSet implCallees = new HashSet(); - foreach (CallSite cs in callerToCallSites[impl.Name]) { - implCallees.Add(cs.callSiteConstant); - } - for (int i = 0; i < unsatCoreIndices.Count; i++) { - VCExprVar assumption = (VCExprVar)assumptions[unsatCoreIndices[i]]; - if (implCallees.Contains(assumption)) { - unsatCore.Add(assumption); - } - } - return Outcome.Correct; - } - - private Outcome FindUnsatCore(Implementation impl, ApiChecker checker, VCExpressionGenerator Gen, PCBErrorReporter reporter, List assumptions, out HashSet unsatCore) - { - Helpers.ExtraTraceInformation("Number of assumptions = " + assumptions.Count); - 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(); - index--; - CallSite cs = sortedCallSites[index]; - bool check = (cs.callerName == impl.Name); - foreach (CallSite x in calleeToCallSites[cs.callerName]) { - check = check || relevantCallSites.Contains(x); - } - if (!check) continue; - bool relevant = (cs.callerName != impl.Name); - foreach (CallSite x in calleeToCallSites[cs.calleeName]) { - if (x.callSiteConstant == cs.callSiteConstant) continue; - relevant = relevant && !reachableCallSites.Contains(x); - } - if (relevant) { - curr = Gen.And(cs.callSiteConstant, curr); - relevantCallSites.Add(cs); - relevantUnsatCore.Add(cs.callSiteConstant); - continue; - } - - queries++; - checker.Push(); - checker.AddAxiom(curr); - ret = checker.CheckVC(); - checker.Pop(); - - if (ret == Outcome.Errors || ret == Outcome.TimedOut) { - curr = Gen.And(cs.callSiteConstant, curr); - relevantCallSites.Add(cs); - relevantUnsatCore.Add(cs.callSiteConstant); - } - } - 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 bool Verified(HashSet unsatCore) { - bool verified = true; - foreach (string name in calleeToCallSites.Keys) { - int numInlined = 0; - foreach (CallSite cs in calleeToCallSites[name]) { - if (unsatCore.Contains(cs.callSiteConstant)) - numInlined++; - } - if (numInlined > 1) { - Helpers.ExtraTraceInformation("callee name = " + name); - Helpers.ExtraTraceInformation("number of inlines = " + numInlined); - verified = false; - } - } - return verified; - } - - private void InlineBottomUp(ApiChecker checker, HashSet unsatCore) - { - Graph callGraph = new Graph(); - foreach (string name in calleeToCallSites.Keys) { - callGraph.AddSource(name); - foreach (CallSite cs in calleeToCallSites[name]) { - callGraph.AddEdge(name, cs.callerName); - } - } - 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); - } - } - foreach (CallSite cs in toBeInlined) { - InlineCallSite(cs, checker); - } - } - } - - private void InlineIntoMain(ApiChecker checker, Implementation impl, HashSet unsatCore) - { - HashSet toBeInlined = new HashSet(); - foreach (CallSite cs in callerToCallSites[impl.Name]) { - if (unsatCore.Contains(cs.callSiteConstant)) { - toBeInlined.Add(cs); - } - } - foreach (CallSite cs in toBeInlined) { - InlineCallSite(cs, checker); - } - } - - 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); - ApiChecker checker; - checker = new ApiChecker(VCExpressionGenerator.False, reporter, underlyingChecker, null); - CreateProcedureCopies(impl, program, checker, vcMain); - - int iter = 0; - while (true) { - Helpers.ExtraTraceInformation("Iteration number " + iter++); - Outcome ret; - - checker.Push(); - - var reachableImpls = ComputeReachableImplementations(impl); - var assumptions = new List(); - foreach (string name in reachableImpls) { - VCExpr expr = procVcCopies[name]; - if (name == impl.Name) { - 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; - - if (Verified(unsatCore)) - return Outcome.Correct; - - //InlineBottomUp(checker, unsatCore); - InlineIntoMain(checker, impl, unsatCore); - } - } -#endif - // A step of the stratified inlining algorithm: both under-approx and over-approx queries private Outcome stratifiedStep(int bound, VerificationState vState, HashSet block) { @@ -3234,21 +2720,6 @@ 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; @@ -3428,13 +2899,6 @@ namespace VC } public override void OnModel(IList labels, ErrorModel errModel) { - if (CommandLineOptions.Clo.UseLabels) - OnModelOld(labels, errModel); - else - OnModelNew(labels, errModel); - } - - private void OnModelNew(IList labels, ErrorModel errModel) { List absyList = new List(); foreach (var label in labels) { absyList.Add(Label2Absy(label)); @@ -3550,280 +3014,6 @@ namespace VC return newCounterexample; } - public void OnModelOld(IList/*!*/ labels, ErrorModel errModel) - { - Contract.Assert(CommandLineOptions.Clo.StratifiedInliningWithoutModels || errModel != null); - - candidatesToExpand = new List(); - - Model model = null; - if (errModel != null) model = errModel.ToModel(); - - if (underapproximationMode) - { - var cex = GenerateTraceMain(labels, model, mvInfo); - Debug.Assert(candidatesToExpand.All(calls.isSkipped)); - if (cex != null) { - GetModelWithStates(model); - callback.OnCounterexample(cex, null); - this.PrintModel(model); - } - return; - } - - Contract.Assert(calls != null); - - GenerateTraceMain(labels, model, mvInfo); - } - - // Construct the interprocedural trace - private Counterexample GenerateTraceMain(IList/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo) - { - Contract.Requires(cce.NonNullElements(labels)); - if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) - { - errModel.Write(ErrorReporter.ModelWriter); - ErrorReporter.ModelWriter.Flush(); - } - - orderedStateIds = new List>(); - Counterexample newCounterexample = - GenerateTrace(labels, errModel, 0, mainImpl); - - if (newCounterexample == null) - return null; - - #region Map passive program errors back to original program errors - ReturnCounterexample returnExample = newCounterexample as ReturnCounterexample; - if (returnExample != null && gotoCmdOrigins != null) - { - foreach (Block b in returnExample.Trace) - { - Contract.Assert(b != null); - Contract.Assume(b.TransferCmd != null); - ReturnCmd cmd = (ReturnCmd)gotoCmdOrigins[b.TransferCmd]; - if (cmd != null) - { - returnExample.FailingReturn = cmd; - break; - } - } - } - #endregion - - return newCounterexample; - } - - private Counterexample GenerateTrace(IList/*!*/ labels, Model/*!*/ errModel, - int candidateId, Implementation procImpl) - { - Contract.Requires(cce.NonNullElements(labels)); - Contract.Requires(procImpl != null); - - Hashtable traceNodes = new Hashtable(); - //string procPrefix = "si_inline_" + candidateId.ToString() + "_"; - - //Console.WriteLine("GenerateTrace: {0}", procImpl.Name); - foreach (string s in labels) - { - Contract.Assert(s != null); - var absylabel = calls.ParseRenamedAbsyLabel(s, candidateId); - - if (absylabel == null) continue; - - Absy absy; - - if (candidateId == 0) - { - absy = Label2Absy(absylabel); - } - else - { - absy = Label2Absy(procImpl.Name, absylabel); - } - - if (traceNodes.ContainsKey(absy)) - System.Console.WriteLine("Warning: duplicate label: " + s + " read while tracing nodes"); - else - traceNodes.Add(absy, null); - } - - BlockSeq trace = new BlockSeq(); - Block entryBlock = cce.NonNull(procImpl.Blocks[0]); - Contract.Assert(entryBlock != null); - Contract.Assert(traceNodes.Contains(entryBlock)); - trace.Add(entryBlock); - - var calleeCounterexamples = new Dictionary(); - Counterexample newCounterexample = GenerateTraceRec(labels, errModel, mvInfo, candidateId, entryBlock, traceNodes, trace, calleeCounterexamples); - - return newCounterexample; - } - - private Counterexample GenerateTraceRec( - IList/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo, - int candidateId, - Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace, - Dictionary/*!*/ calleeCounterexamples) - { - Contract.Requires(cce.NonNullElements(labels)); - Contract.Requires(b != null); - Contract.Requires(traceNodes != null); - Contract.Requires(trace != null); - Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples)); - // After translation, all potential errors come from asserts. - while (true) - { - CmdSeq cmds = b.Cmds; - TransferCmd transferCmd = cce.NonNull(b.TransferCmd); - for (int i = 0; i < cmds.Length; i++) - { - Cmd cmd = cce.NonNull(cmds[i]); - - // Skip if 'cmd' not contained in the trace or not an assert - if (cmd is AssertCmd && traceNodes.Contains(cmd)) - { - Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, context); - newCounterexample.AddCalleeCounterexample(calleeCounterexamples); - return newCounterexample; - } - - // Counterexample generation for inlined procedures - AssumeCmd assumeCmd = cmd as AssumeCmd; - if (assumeCmd == null) - continue; - NAryExpr naryExpr = assumeCmd.Expr as NAryExpr; - if (naryExpr == null) - continue; - string calleeName = naryExpr.Fun.FunctionName; - Contract.Assert(calleeName != null); - - BinaryOperator binOp = naryExpr.Fun as BinaryOperator; - if (binOp != null && binOp.Op == BinaryOperator.Opcode.And) { - Expr expr = naryExpr.Args[0]; - NAryExpr mvStateExpr = expr as NAryExpr; - if (mvStateExpr != null && mvStateExpr.Fun.FunctionName == ModelViewInfo.MVState_FunctionDef.Name) { - LiteralExpr x = mvStateExpr.Args[1] as LiteralExpr; - orderedStateIds.Add(new Tuple(candidateId, x.asBigNum.ToInt)); - } - } - - if (calleeName.StartsWith(recordProcName) && errModel != null) - { - var expr = calls.recordExpr2Var[new BoogieCallExpr(naryExpr, candidateId)]; - - // Record concrete value of the argument to this procedure - var args = new List(); - if (expr is VCExprIntLit) - { - args.Add(errModel.MkElement((expr as VCExprIntLit).Val.ToString())); - } - else if (expr == VCExpressionGenerator.True) - { - args.Add(errModel.MkElement("true")); - } - else if (expr == VCExpressionGenerator.False) - { - args.Add(errModel.MkElement("false")); - } - else if (expr is VCExprVar) - { - var idExpr = expr as VCExprVar; - string name = context.Lookup(idExpr); - Contract.Assert(name != null); - Model.Func f = errModel.TryGetFunc(name); - if (f != null) - { - args.Add(f.GetConstant()); - } - } - else - { - Contract.Assert(false); - } - calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] = - new CalleeCounterexampleInfo(null, args); - continue; - } - - if (!implName2StratifiedInliningInfo.ContainsKey(calleeName)) - continue; - - Contract.Assert(calls != null); - - if (calls.isPCBCandidate(candidateId)) - { - Contract.Assert(procBoundingMode); - // We're already inside PCB VCs. The lookup for procedure calls - // is different here - var uid = calls.pcbBoogieExpr2Id[new BoogieCallExpr(naryExpr, candidateId)]; - var pcopy = pcbFindLabel(labels, string.Format("PCB_{0}_", uid)); - var actualId = calls.procCopy2Id[Tuple.Create(calleeName, pcopy)]; - - orderedStateIds.Add(new Tuple(actualId, StratifiedInliningErrorReporter.CALL)); - calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] = - new CalleeCounterexampleInfo( - cce.NonNull(GenerateTrace(labels, errModel, actualId, implName2StratifiedInliningInfo[calleeName].impl)), - new List()); - orderedStateIds.Add(new Tuple(candidateId, StratifiedInliningErrorReporter.RETURN)); - } - else - { - int calleeId = calls.boogieExpr2Id[new BoogieCallExpr(naryExpr, candidateId)]; - - if (calls.currCandidates.Contains(calleeId)) { - if (procBoundingMode) { - // Entering PCB VCs - var pcopy = pcbFindLabel(labels, string.Format("PCB_CONNECT_{0}_", calleeId)); - Contract.Assert(pcopy >= 0 && pcopy < CommandLineOptions.Clo.ProcedureCopyBound); - var actualId = calls.procCopy2Id[Tuple.Create(calleeName, pcopy)]; - - orderedStateIds.Add(new Tuple(actualId, StratifiedInliningErrorReporter.CALL)); - calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] = - new CalleeCounterexampleInfo( - cce.NonNull(GenerateTrace(labels, errModel, actualId, implName2StratifiedInliningInfo[calleeName].impl)), - new List()); - orderedStateIds.Add(new Tuple(candidateId, StratifiedInliningErrorReporter.RETURN)); - } - else { - candidatesToExpand.Add(calleeId); - } - } - else { - orderedStateIds.Add(new Tuple(calleeId, StratifiedInliningErrorReporter.CALL)); - calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] = - new CalleeCounterexampleInfo( - cce.NonNull(GenerateTrace(labels, errModel, calleeId, implName2StratifiedInliningInfo[calleeName].impl)), - new List()); - orderedStateIds.Add(new Tuple(candidateId, StratifiedInliningErrorReporter.RETURN)); - } - } - } - - GotoCmd gotoCmd = transferCmd as GotoCmd; - if (gotoCmd != null) - { - b = null; - foreach (Block bb in cce.NonNull(gotoCmd.labelTargets)) - { - Contract.Assert(bb != null); - if (traceNodes.Contains(bb)) - { - trace.Add(bb); - b = bb; - break; - //return GenerateTraceRec(labels, errModel, candidateId, bb, traceNodes, trace, calleeCounterexamples); - } - } - if (b != null) continue; - } - return null; - } - - //return null; - - } - public override Absy Label2Absy(string label) { //Contract.Requires(label != null); diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat index 3ba74096..2bb3cbd5 100644 --- a/Test/stratifiedinline/runtest.bat +++ b/Test/stratifiedinline/runtest.bat @@ -5,33 +5,33 @@ set BGEXE=..\..\Binaries\Boogie.exe rem set BGEXE=mono ..\..\Binaries\Boogie.exe echo ----- Running regression test bar1.bpl -%BGEXE% %* /noinfer /stratifiedInline:1 bar1.bpl +%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar1.bpl echo ----- echo ----- Running regression test bar2.bpl -%BGEXE% %* /noinfer /stratifiedInline:1 bar2.bpl +%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar2.bpl echo ----- echo ----- Running regression test bar3.bpl -%BGEXE% %* /noinfer /stratifiedInline:1 bar3.bpl +%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar3.bpl echo ----- echo ----- Running regression test bar4.bpl -%BGEXE% %* /noinfer /stratifiedInline:1 bar4.bpl +%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar4.bpl echo ----- echo ----- Running regression test bar6.bpl -%BGEXE% %* /noinfer /stratifiedInline:1 bar6.bpl +%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar6.bpl echo ----- echo ----- Running regression test bar7.bpl -%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar7.bpl +%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /nonUniformUnfolding bar7.bpl echo ----- echo ----- Running regression test bar8.bpl -%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar8.bpl +%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /nonUniformUnfolding bar8.bpl echo ----- echo ----- Running regression test bar9.bpl -%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar9.bpl +%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /nonUniformUnfolding bar9.bpl echo ----- echo ----- Running regression test bar10.bpl -%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar10.bpl +%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /nonUniformUnfolding bar10.bpl echo ----- echo ----- Running regression test bar11.bpl -%BGEXE% %* /noinfer /stratifiedInline:1 bar11.bpl +%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar11.bpl echo ----- -- cgit v1.2.3