revised implementation of proc copy bounding

1 files 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<string, StratifiedInliningInfo>();

 

             this.GenerateVCsForStratifiedInlining(program);

@@ -112,7 +107,6 @@ namespace VC
         {

             Contract.Requires(program != null);

             Checker checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime);

-            pcbProcToCounterArgLocation = new Dictionary<string, int>();

 

             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<string, GlobalVariable> pcbProcToCounter;

-        private Dictionary<string, int> pcbProcToCounterArgLocation;

-

-        // Instrument program to introduce a counter per procedure

-        private void InstrumentForPCB(Program program)

-        {

-            pcbProcToCounter = new Dictionary<string, GlobalVariable>();

-            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<string, List<List<VCExprVar>>> interfaceVarCopies;

-        // proc name -> k -> VCExpr

-        Dictionary<string, List<VCExpr>> procVcCopies;

-        // proc name -> k -> CallSite Boolean constant

-        Dictionary<string, List<VCExprVar>> callSiteConstant;

-        // VC for ProcCopyBounding

-        VCExpr procBoundedVC;

-

-        private void CreateProcedureCopies(int K, Program program, FCallHandler calls, StratifiedCheckerInterface checker)

-        {

-            interfaceVarCopies = new Dictionary<string, List<List<VCExprVar>>>();

-            procVcCopies = new Dictionary<string, List<VCExpr>>();

-            callSiteConstant = new Dictionary<string, List<VCExprVar>>();

-            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<Tuple<string, int>, 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<string, HashSet<string>>();

-            var pred = new Dictionary<string, HashSet<string>>();

-

-            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<string>());

-                        if(!pred.ContainsKey(ccmd.callee)) pred.Add(ccmd.callee, new HashSet<string>());

-                        succ[impl.Name].Add(ccmd.callee);

-                        pred[ccmd.callee].Add(impl.Name);

-                    }

-                }

-            }

-

-            var uniqueCallEdges = new HashSet<Tuple<string, string>>();

-            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<string, List<VCExprVar>> interfaceVarCopies;

+        public Dictionary<string, List<VCExprVar>> privateVarCopies;

+        Dictionary<string, VCExpr> 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<string, List<CallSite>> calleeToCallSites;

+        Dictionary<string, List<CallSite>> callerToCallSites;

+

+        private void CreateProcedureCopies(Implementation impl, Program program, StratifiedCheckerInterface checker, VCExpr vcMain) {

+          interfaceVarCopies = new Dictionary<string, List<VCExprVar>>();

+          privateVarCopies = new Dictionary<string, List<VCExprVar>>();

+          procVcCopies = new Dictionary<string, VCExpr>();

+          calleeToCallSites = new Dictionary<string, List<CallSite>>();

+          callerToCallSites = new Dictionary<string, List<CallSite>>();

+

+          interfaceVarCopies[impl.Name] = new List<VCExprVar>();

+          privateVarCopies[impl.Name] = new List<VCExprVar>();

+          calleeToCallSites[impl.Name] = new List<CallSite>();

+          callerToCallSites[impl.Name] = new List<CallSite>();

+          foreach (var info in implName2StratifiedInliningInfo.Values) {

+            Contract.Assert(info != null);

+            interfaceVarCopies[info.impl.Name] = new List<VCExprVar>();

+            privateVarCopies[info.impl.Name] = new List<VCExprVar>();

+            calleeToCallSites[info.impl.Name] = new List<CallSite>();

+            callerToCallSites[info.impl.Name] = new List<CallSite>();

+            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<bool>

-        {

-            // proc name -> k -> interface variables

-            Dictionary<string, List<List<VCExprVar>>> interfaceVarCopies;

-            // proc name -> k -> CallSite Boolean constant

-            Dictionary<string, List<VCExprVar>> callSiteConstant;

-            // Call edges (single successor or single predecessor)

-            HashSet<Tuple<string,string>> uniqueCallEdges;

-            // proc name -> location of the counter in argument

-            Dictionary<string, int> pcbProcToCounterArgLocation;

-

-            FCallHandler calls;

-            int currId;

-            string currentProc;

-            int currCopy;

-

-            public BoundingVCMutator(HashSet<Tuple<string, string>> uniqueCallEdges,

-                VCExpressionGenerator gen, 

-                Dictionary<string, List<List<VCExprVar>>> interfaceVarCopies,

-                Dictionary<string, List<VCExprVar>> callSiteConstant,

-                Dictionary<string, int> 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<VCExpr/*!*/>/*!*/ newSubExprs,

-                                                          bool changed,

-                                                          bool arg)

-            {

-                //Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null);

-                Contract.Ensures(Contract.Result<VCExpr>() != 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<bool> {

+          StratifiedCheckerInterface checker;

+          string implName;

+          Dictionary<string, List<VCExprVar>> interfaceVarCopies;

+          Dictionary<string, List<CallSite>> calleeToCallSites;

+          Dictionary<string, List<CallSite>> callerToCallSites;

+

+          public BoundingVCMutator(

+              StratifiedCheckerInterface checker,

+              string implName,

+              Dictionary<string, List<VCExprVar>> interfaceVarCopies,

+              Dictionary<string, List<CallSite>> calleeToCallSites,

+              Dictionary<string, List<CallSite>> 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<VCExpr/*!*/>/*!*/ newSubExprs,

+                                                        bool changed,

+                                                        bool arg) {

+            Contract.Ensures(Contract.Result<VCExpr>() != 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<List<VCExprVar>>());

-            procVcCopies.Add(info.impl.Name, new List<VCExpr>());

-            callSiteConstant.Add(info.impl.Name, new List<VCExprVar>());

-

-            for (int k = 0; k < K; k++)

-            {

-                var expr = info.vcexpr;

-                // Instantiate the interface variables

-                Dictionary<VCExprVar, VCExpr> substForallDict = new Dictionary<VCExprVar, VCExpr>();

-                var ls = new List<VCExprVar>();

-                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<TypeVariable, Microsoft.Boogie.Type>());

-

-                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<VCExprVar, VCExpr> substExistsDict = new Dictionary<VCExprVar, VCExpr>();

-                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<TypeVariable, Microsoft.Boogie.Type>());

-

-                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<VCExprVar, VCExpr> substForallDict = new Dictionary<VCExprVar, VCExpr>();

+          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<TypeVariable, Microsoft.Boogie.Type>());

+          SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(Gen);

+          Contract.Assert(subst != null);

+          expr = subst.Mutate(expr, substForall);

+

+          // Instantiate and declare the private variables

+          Dictionary<VCExprVar, VCExpr> substExistsDict = new Dictionary<VCExprVar, VCExpr>();

+          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<TypeVariable, Microsoft.Boogie.Type>());

+          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<int> 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<int>();

-                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<UnexpectedProverOutputException>(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<int> 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<int>();

+            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<UnexpectedProverOutputException>(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<VCExpr> assumptions, out List<int> unsatCore) {

+            if (!UseCheckAssumptions) {

+              return base.CheckAssumptions(assumptions, out unsatCore);

             }

             

-            public override Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)

-            {

-                if (!UseCheckAssumptions)

-                {

-                    return base.CheckAssumptions(assumptions, out unsatCore);

-                }

-

-                if (assumptions.Count == 0)

-                {

-                    unsatCore = new List<int>();

-                    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<int>();

+              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<Implementation>();

-            foreach (var decl in program.TopLevelDeclarations)

-                if (decl is Implementation) impls.Add(decl as Implementation);

-            impls.Add(impl);

-

-            var callGraph = new Graph<string>();

-            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<string>.Acyclic(callGraph, impl.Name);

-        }

-

         public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback)

         {

             Contract.EnsuresOnThrow<UnexpectedProverOutputException>(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/*<int, Absy!>*/ 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<bool> {

+          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<VCExpr/*!*/>/*!*/ newSubExprs,

+                                                        bool changed,

+                                                        bool arg) {

+            Contract.Ensures(Contract.Result<VCExpr>() != 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<VCExprVar> interfaceExprVars = interfaceVarCopies[callee];

+          List<VCExprVar> privateVars = privateVarCopies[callee];

+

+          // Instantiate the "forall" variables

+          Dictionary<VCExprVar, VCExpr> substForallDict = new Dictionary<VCExprVar, VCExpr>();

+          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<TypeVariable, Microsoft.Boogie.Type>());

+          SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(Gen); 

+          expansion = subst.Mutate(expansion, substForall);

+

+          // Instantiate and declare the "exists" variables

+          Dictionary<VCExprVar, VCExpr> substExistsDict = new Dictionary<VCExprVar, VCExpr>();

+          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<TypeVariable, Microsoft.Boogie.Type>());

+          subst = new SubstitutingVCExprVisitor(Gen);

+          expansion = subst.Mutate(expansion, substExists);

+

+          Dictionary<VCExprVar, VCExpr> substCallSiteConstantDict = new Dictionary<VCExprVar, VCExpr>();

+          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<TypeVariable, Microsoft.Boogie.Type>());

+          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<VCExpr> assumptions, out HashSet<VCExprVar> 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<VCExprVar>();

+            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<int> unsatCoreIndices;

+            Outcome ret;

+            ret = checker.CheckAssumptions(assumptions, out unsatCoreIndices);

+            if (ret == Outcome.Errors) return ret;

+            unsatCore = new HashSet<VCExprVar>();

+            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<CallSite> reachableCallSites = new HashSet<CallSite>();

+            Stack<string> stack = new Stack<string>();

+            HashSet<string> set = new HashSet<string>();

+            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<CallSite> callGraph = new Graph<CallSite>();

+            foreach (CallSite cs1 in reachableCallSites) {

+              callGraph.AddSource(cs1);

+              foreach (CallSite cs2 in calleeToCallSites[cs1.callerName]) {

+                if (reachableCallSites.Contains(cs2)) {

+                  callGraph.AddEdge(cs1, cs2);

+                }

+              }

+            }

+

+            List<CallSite> sortedCallSites = new List<CallSite>();

+            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<CallSite> relevantCallSites = new HashSet<CallSite>();

+            HashSet<VCExprVar> relevantUnsatCore = new HashSet<VCExprVar>();

+            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<string> ComputeReachableImplementations(Implementation impl) {

+          Stack<string> stack = new Stack<string>();

+          HashSet<string> set = new HashSet<string>();

+          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<VCExpr>();

+            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<VCExprVar> unsatCore;

+            ret = FindUnsatCore(impl, checker, Gen, reporter, assumptions, out unsatCore);

+            

+            checker.Pop();

+

+            if (ret == Outcome.Errors) return ret;

+

+            Graph<string> callGraph = new Graph<string>();

+            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<CallSite> toBeInlined = new HashSet<CallSite>();

+              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<string> labels, ErrorModel errModel) {

+            if (unsatCoreMode) return;

+            Console.WriteLine("Error in " + mainImpl.Name);

+          }

+        }

+

         public class StratifiedInliningErrorReporter : ProverInterface.ErrorHandler

         {

             Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo;

@@ -3002,6 +2961,8 @@ namespace VC
 

             public override void OnModel(IList<string/*!*/>/*!*/ labels, ErrorModel errModel)

             {

+              //if (procBoundingMode) return; // shaz hack

+

                 candidatesToExpand = new List<int>();

 

                 //Contract.Requires(cce.NonNullElements(labels));