/// <summary>
 /// Simplifies the CFG of the given implementation impl by merging each
 /// basic block with a single predecessor into that predecessor if the
 /// predecessor has a single successor.  If a uniformity analyser is
 /// being used then blocks will only be merged if they are both uniform
 /// or both non-uniform
 /// </summary>
 public static void MergeBlocksIntoPredecessors(Program prog, Implementation impl, UniformityAnalyser uni)
 {
     var blockGraph = prog.ProcessLoops(impl);
     var predMap = new Dictionary<Block, Block>();
     foreach (var block in blockGraph.Nodes)
     {
         try
         {
             var pred = blockGraph.Predecessors(block).Single();
             if (blockGraph.Successors(pred).Single() == block &&
                 (uni == null ||
                 (uni.IsUniform(impl.Name, pred) && uni.IsUniform(impl.Name, block)) ||
                 (!uni.IsUniform(impl.Name, pred) && !uni.IsUniform(impl.Name, block))))
             {
                 Block predMapping;
                 while (predMap.TryGetValue(pred, out predMapping))
                     pred = predMapping;
                 pred.Cmds.AddRange(block.Cmds);
                 pred.TransferCmd = block.TransferCmd;
                 impl.Blocks.Remove(block);
                 predMap[block] = pred;
             }
             // If Single throws an exception above (i.e. not exactly one pred/succ), skip this block.
         }
         catch (InvalidOperationException) { }
     }
 }

 /*!*/
 private static HashSet<Block/*!*/> ComputeMultiPredecessorBlocks(Implementation/*!*/ impl)
 {
     Contract.Requires(impl != null);
       Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Block>>()));
       HashSet<Block/*!*/> visitedBlocks = new HashSet<Block/*!*/>();
       HashSet<Block/*!*/> multiPredBlocks = new HashSet<Block/*!*/>();
       Stack<Block/*!*/> dfsStack = new Stack<Block/*!*/>();
       dfsStack.Push(impl.Blocks[0]);
       while (dfsStack.Count > 0) {
     Block/*!*/ b = dfsStack.Pop();
     Contract.Assert(b != null);
     if (visitedBlocks.Contains(b)) {
       multiPredBlocks.Add(b);
       continue;
     }
     visitedBlocks.Add(b);
     if (b.TransferCmd == null)
       continue;
     if (b.TransferCmd is ReturnCmd)
       continue;
     Contract.Assert(b.TransferCmd is GotoCmd);
     GotoCmd gotoCmd = (GotoCmd)b.TransferCmd;
     if (gotoCmd.labelTargets == null)
       continue;
     foreach (Block/*!*/ succ in gotoCmd.labelTargets) {
       Contract.Assert(succ != null);
       dfsStack.Push(succ);
     }
       }
       return multiPredBlocks;
 }

        public void Insert(Implementation impl, VerificationResult result)
        {
            Contract.Requires(impl != null);
              Contract.Requires(result != null);

              Cache.Set(impl.Id, result, Policy);
        }

 BlockPredicator(Program p, Implementation i, bool cci, bool upp)
 {
     prog = p;
     impl = i;
     createCandidateInvariants = cci;
     useProcedurePredicates = upp;
 }

 SmartBlockPredicator(Program p, Implementation i, Func<Procedure, bool> upp, UniformityAnalyser u) {
   prog = p;
   impl = i;
   useProcedurePredicates = upp;
   myUseProcedurePredicates = useProcedurePredicates(i.Proc);
   uni = u;
 }

        public static void Predicate(Program p,
            Func<Procedure, bool> useProcedurePredicates = null,
            UniformityAnalyser uni = null)
        {
            useProcedurePredicates = useProcedurePredicates ?? (proc => false);
            if (uni != null) {
              var oldUPP = useProcedurePredicates;
              useProcedurePredicates = proc => oldUPP(proc) && !uni.IsUniform(proc.Name);
            }

            foreach (var decl in p.TopLevelDeclarations.ToList()) {
              if (decl is Procedure || decl is Implementation) {
            var proc = decl as Procedure;
            Implementation impl = null;
            if (proc == null) {
              impl = (Implementation)decl;
              proc = impl.Proc;
            }

            bool upp = useProcedurePredicates(proc);
            if (upp) {
              var dwf = (DeclWithFormals)decl;
              var fpVar = new Formal(Token.NoToken,
                                 new TypedIdent(Token.NoToken, "_P",
                                                Microsoft.Boogie.Type.Bool),
                                 /*incoming=*/true);
              dwf.InParams = new List<Variable>(
            (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
              .ToArray());

              if (impl == null) {
            var fpIdentifierExpr = new IdentifierExpr(Token.NoToken, fpVar);
            foreach (Requires r in proc.Requires) {
              new EnabledReplacementVisitor(fpIdentifierExpr).VisitExpr(r.Condition);
              if (!QKeyValue.FindBoolAttribute(r.Attributes, "do_not_predicate")) {
                r.Condition = Expr.Imp(fpIdentifierExpr, r.Condition);
              }
            }
            foreach (Ensures e in proc.Ensures) {
              new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition);
              if (!QKeyValue.FindBoolAttribute(e.Attributes, "do_not_predicate")) {
                e.Condition = Expr.Imp(fpIdentifierExpr, e.Condition);
              }
            }
              }
            }

            if (impl != null) {
              try {
            new SmartBlockPredicator(p, impl, useProcedurePredicates, uni).PredicateImplementation();
              } catch (Program.IrreducibleLoopException) { }
            }
              }
            }
        }

 public VerificationResult Lookup(Implementation impl)
 {
     if (!NeedsToBeVerified(impl))
       {
     return Lookup(impl.Id);
       }
       else
       {
     return null;
       }
 }

 public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum)
 {
     this.moverTypeChecker = moverTypeChecker;
     this.layerNum = layerNum;
     this.enclosingProc = null;
     this.enclosingImpl = null;
     this.procMap = new Dictionary<Procedure, Procedure>();
     this.absyMap = new Dictionary<Absy, Absy>();
     this.implMap = new Dictionary<Implementation, Implementation>();
     this.yieldingProcs = new HashSet<Procedure>();
     this.impls = new List<Implementation>();
 }

        /*
         ComputePhaseIntervals :
         1.1 Input parameters : 
           1.1.1 Implementation impl : Implementation whose body is being YTS checked.
           1.1.2 int specPhaseNumImpl : Phase number in which procedure of implementation, impl, reaches its specification,{A,R,L,B}
           1.1.3 MoverTypeChecker moverTypeChecker : moverTypeChecker is the integration point of YieldTypeChecker to OG class. moverTypeChecker has functions enables YieldTypeChecker to find phaseNum and spec of procedures.

         1.2 Return value : is a list of tuples(phase interval start,phase interval end). Every tuple in this list is representing an interval formed by callCmds' phase numbers inside impl.			   
         1.3 Action : This function first traverses the blocks inside impl, collects all CallCmds inside it into a HashSet ,callCmdsInImpl. 
                *      Then it puts all these callCmds' phase numbers into a HashSet,callCmdPhaseNumSet. 
                *     After adding all callCmds' phase numbers' it adds phase number of procedure of impl into the set. 
                *     It sorts all numbers in this set and creates [-inf...n-1] [n...k-1] [k  PhaseNumProcOfImpl] disjoint intervals.
          */
        private static List<Tuple<int, int>> ComputePhaseIntervals(Implementation impl, int specPhaseNumImpl, MoverTypeChecker moverTypeChecker)
        {
            HashSet<CallCmd> callCmdsInImpl = new HashSet<CallCmd>(); //  callCmdsInImpl[Implementation] ==> Set = { call1, call2, call3 ... }
            List<Tuple<int, int>> phaseIntervals = new List<Tuple<int, int>>(); // [MinValue ph0 ] [ph0 ph1] [ph1 ph2] ..... [phk phk+1] intervals

            // Compute CallCmds inside impl
            foreach (Block b in impl.Blocks)
            {
                for (int i = 0; i < b.Cmds.Count; i++)
                {
                    CallCmd callCmd = b.Cmds[i] as CallCmd;
                    if (callCmd == null) continue;
                    callCmdsInImpl.Add(callCmd);
                }
            }

            //Collect phase numbers of CallCmds inside impl
            HashSet<int> callCmdPhaseNumSet = new HashSet<int>();
            foreach (CallCmd callCmd in callCmdsInImpl)
            {
                int tmpPhaseNum = moverTypeChecker.FindPhaseNumber(callCmd.Proc);
                callCmdPhaseNumSet.Add(tmpPhaseNum);
            }
            callCmdPhaseNumSet.Add(specPhaseNumImpl);

            List<int> callCmdPhaseNumList = callCmdPhaseNumSet.ToList();
            callCmdPhaseNumList.Sort();

            //Create Phase Intervals
            for (int i = 0; i < callCmdPhaseNumList.Count; i++)
            {
                //create the initial phase (-inf leastPhaseNum]
                if (i == 0)
                {
                    Tuple<int, int> initTuple = new Tuple<int, int>(int.MinValue, callCmdPhaseNumList[i]);
                    phaseIntervals.Add(initTuple);
                }
                else // create other phase intervals 
                {
                    Tuple<int, int> intervalToInsert = new Tuple<int, int>(callCmdPhaseNumList[i - 1] + 1, callCmdPhaseNumList[i]);
                    phaseIntervals.Add(intervalToInsert);
                }
            }
#if (DEBUG && !DEBUG_DETAIL)
            Console.Write("\n Number of phases is " + phaseIntervals.Count.ToString());
            for (int i = 0;i<phaseIntervals.Count ; i++) {
                Console.Write("\n Phase " + i.ToString() + "[" + phaseIntervals[i].Item1.ToString() + "," + phaseIntervals[i].Item2.ToString() + "]" + "\n");
            }
#endif
            return phaseIntervals;
        }

        private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> loopHeaders)
        {
            this.moverTypeChecker = moverTypeChecker;
            this.impl = impl;
            this.currLayerNum = currLayerNum;
            this.loopHeaders = loopHeaders;
            this.stateCounter = 0;
            this.absyToNode = new Dictionary<Absy, int>();
            this.initialState = 0;
            this.finalStates = new HashSet<int>();
            this.edgeLabels = new Dictionary<Tuple<int, int>, int>();

            foreach (Block block in impl.Blocks)
            {
                absyToNode[block] = stateCounter;
                stateCounter++;
                foreach (Cmd cmd in block.Cmds)
                {
                    absyToNode[cmd] = stateCounter;
                    stateCounter++;
                }
                absyToNode[block.TransferCmd] = stateCounter;
                stateCounter++;
                if (block.TransferCmd is ReturnCmd)
                {
                    finalStates.Add(absyToNode[block.TransferCmd]);
                }
            }
            foreach (Block block in impl.Blocks)
            {
                Absy blockEntry = block.Cmds.Count == 0 ? (Absy)block.TransferCmd : (Absy)block.Cmds[0];
                edgeLabels[new Tuple<int, int>(absyToNode[block], absyToNode[blockEntry])] = 'P';

                GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
                if (gotoCmd == null) continue;
                foreach (Block successor in gotoCmd.labelTargets)
                {
                    edgeLabels[new Tuple<int, int>(absyToNode[gotoCmd], absyToNode[successor])] = 'P';
                }
            }

            this.nodeToAbsy = new Dictionary<int, Absy>();
            foreach (KeyValuePair<Absy, int> state in absyToNode)
            {
                this.nodeToAbsy[state.Value] = state.Key;
            }

            ComputeGraph();
            IsYieldTypeSafe();
        }

 public int VerificationPriority(Implementation impl)
 {
     if (!Cache.ContainsKey(impl.Id))
       {
     return 3;  // high priority (has been never verified before)
       }
       else if (Cache[impl.Id].Checksum != impl.Checksum)
       {
     return 2;  // medium priority (old snapshot has been verified before)
       }
       else if (impl.DependenciesChecksum == null || Cache[impl.Id].DependeciesChecksum != impl.DependenciesChecksum)
       {
     return 1;  // low priority (the same snapshot has been verified before, but a callee has changed)
       }
       else
       {
     return int.MaxValue;  // skip verification (highest priority to get them done as soon as possible)
       }
 }

 public override Implementation VisitImplementation(Implementation node) {
   //Contract.Requires(node != null);
   Contract.Ensures(Contract.Result<Implementation>() != null);
   //Console.WriteLine("Procedure {0}", node.Name);
   Implementation/*!*/ impl = base.VisitImplementation(node);
   Contract.Assert(impl != null);
   //Console.WriteLine("Old number of local variables = {0}", impl.LocVars.Length);
   List<Variable>/*!*/ vars = new List<Variable>();
   foreach (Variable/*!*/ var in impl.LocVars) {
     Contract.Assert(var != null);
     if (_usedVars.Contains(var))
       vars.Add(var);
   }
   impl.LocVars = vars;
   //Console.WriteLine("New number of local variables = {0}", impl.LocVars.Length);
   //Console.WriteLine("---------------------------------");
   _usedVars.Clear();
   return impl;
 }

    /// <summary>
    /// Debug method that prints a dot file of the 
    /// current set of blocks in impl to filename. 
    /// </summary>
    private void Impl2Dot(Implementation impl, string filename) {
      Contract.Requires(impl != null);
      Contract.Requires(filename != null);
      List<string> nodes = new List<string>();
      List<string> edges = new List<string>();

      string nodestyle = "[shape=box];";

      foreach (Block b in impl.Blocks) {
        Contract.Assert(b != null);
        nodes.Add(string.Format("\"{0}\" {1}", b.Label, nodestyle));
        GotoCmd gc = b.TransferCmd as GotoCmd;
        if (gc != null)
        {
            Contract.Assert(gc.labelTargets != null);
            foreach (Block b_ in gc.labelTargets)
            {
                Contract.Assert(b_ != null);
                edges.Add(String.Format("\"{0}\" -> \"{1}\";", b.Label, b_.Label));
            }
        }

        //foreach (Block b_ in b.Predecessors)
        //{              
        //    edges.Add(String.Format("\"{0}\" -> \"{1}\";", b.Label, b_.Label));
        //}
      }
        
      using (StreamWriter sw = new StreamWriter(filename)) {
        sw.WriteLine(String.Format("digraph {0} {{", impl.Name));
        //            foreach (string! s in nodes) {
        //                sw.WriteLine(s);
        //            }
        foreach (string s in edges) {
          Contract.Assert(s != null);
          sw.WriteLine(s);
        }
        sw.WriteLine("}}");
        sw.Close();
      }
    }

        // There is no default constructor, because these parameters are needed for most subclasses
        public DoomDetectionStrategy(Implementation imp, Block unifiedexit, List<Block> unreach) 
        {
            m_BlockH = new BlockHierachy(imp, unifiedexit);
            __DEBUG_EQCLeaf = m_BlockH.Leaves.Count;
            
            //foreach (BlockHierachyNode bhn in m_BlockH.Leaves)
            //{
            //    if (bhn.Content.Count > 0) __DEBUG_minelements.Add(bhn.Content[0]);
            //}
            //if (imp.Blocks.Count>0) m_GatherInfo(imp.Blocks[0], 0, 0,0);


            if (__DEBUGOUT)
            {
                Console.WriteLine("MaBranchingDepth {0}  MaxMinPP {1} ", m_MaxBranchingDepth, m_MaxK);

                Console.WriteLine("AvgLeaverPerPath {0} AvgPLen {1}", 0, 0);
            }

            MaxBlocks = imp.Blocks.Count;
            MinBlocks = imp.Blocks.Count;
            HACK_NewCheck = false;
            __DEBUG_BlocksTotal = imp.Blocks.Count;
        }

        private void SetupRefinementCheck(Implementation impl, 
            out List<Variable> newLocalVars,
            out Dictionary<string, Variable> domainNameToInputVar, out Dictionary<string, Variable> domainNameToLocalVar, out Dictionary<Variable, Variable> ogOldGlobalMap)
        {
            pc = null;
            ok = null;
            alpha = null;
            beta = null;
            frame = null;

            newLocalVars = new List<Variable>();
            Program program = linearTypeChecker.program;
            ogOldGlobalMap = new Dictionary<Variable, Variable>();
            foreach (IdentifierExpr ie in globalMods)
            {
                Variable g = ie.Decl;
                LocalVariable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type));
                ogOldGlobalMap[g] = l;
                newLocalVars.Add(l);
            }

            Procedure originalProc = implMap[impl].Proc;
            ActionInfo actionInfo = civlTypeChecker.procToActionInfo[originalProc];
            if (actionInfo.createdAtLayerNum == this.layerNum)
            {
                pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool));
                newLocalVars.Add(pc);
                ok = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_ok", Type.Bool));
                newLocalVars.Add(ok);
                Dictionary<Variable, Expr> alwaysMap = new Dictionary<Variable, Expr>();
                for (int i = 0; i < originalProc.InParams.Count; i++)
                {
                    alwaysMap[originalProc.InParams[i]] = Expr.Ident(impl.InParams[i]);
                }
                for (int i = 0; i < originalProc.OutParams.Count; i++)
                {
                    alwaysMap[originalProc.OutParams[i]] = Expr.Ident(impl.OutParams[i]);
                }
                Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap);
                Dictionary<Variable, Expr> foroldMap = new Dictionary<Variable, Expr>();
                foreach (IdentifierExpr ie in globalMods)
                {
                    foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);
                }
                Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);
                frame = new HashSet<Variable>(civlTypeChecker.SharedVariables);
                foreach (Variable v in civlTypeChecker.SharedVariables)
                {
                    if (civlTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum ||
                        civlTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum)
                    {
                        frame.Remove(v);
                    }
                }
                AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
                if (atomicActionInfo == null)
                {
                    beta = Expr.True;
                    foreach (var v in frame)
                    {
                        beta = Expr.And(beta, Expr.Eq(Expr.Ident(v), foroldMap[v]));
                    }
                    alpha = Expr.True;
                }
                else
                {
                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(civlTypeChecker.program, atomicActionInfo, frame, new HashSet<Variable>())).TransitionRelationCompute(true);
                    beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr);
                    Expr alphaExpr = Expr.True;
                    foreach (AssertCmd assertCmd in atomicActionInfo.gate)
                    {
                        alphaExpr = Expr.And(alphaExpr, assertCmd.Expr);
                        alphaExpr.Type = Type.Bool;
                    }
                    alpha = Substituter.Apply(always, alphaExpr);
                }
                foreach (Variable f in impl.OutParams)
                {
                    LocalVariable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_old_{0}", f.Name), f.TypedIdent.Type));
                    newLocalVars.Add(copy);
                    ogOldGlobalMap[f] = copy;
                }
            }

            domainNameToInputVar = new Dictionary<string, Variable>();
            domainNameToLocalVar = new Dictionary<string, Variable>();
            {
                int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count;
                foreach (string domainName in linearTypeChecker.linearDomains.Keys)
                {
                    Variable inParam = impl.InParams[i];
                    domainNameToInputVar[domainName] = inParam;
                    Variable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name + "_local", inParam.TypedIdent.Type));
                    domainNameToLocalVar[domainName] = l;
                    newLocalVars.Add(l);
                    i++;
                }
            }
        }

        private void CreateYieldCheckerImpl(Implementation impl, List<List<Cmd>> yields)
        {
            if (yields.Count == 0) return;

            Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
            foreach (Variable local in impl.LocVars)
            {
                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type));
                map[local] = Expr.Ident(copy);
            }

            Program program = linearTypeChecker.program;
            List<Variable> locals = new List<Variable>();
            List<Variable> inputs = new List<Variable>();
            foreach (IdentifierExpr ie in map.Values)
            {
                locals.Add(ie.Decl);
            }
            for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
            {
                Variable inParam = impl.InParams[i];
                Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
                locals.Add(copy);
                map[impl.InParams[i]] = Expr.Ident(copy);
            }
            {
                int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count;
                foreach (string domainName in linearTypeChecker.linearDomains.Keys)
                {
                    Variable inParam = impl.InParams[i];
                    Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true);
                    inputs.Add(copy);
                    map[impl.InParams[i]] = Expr.Ident(copy);
                    i++;
                }
            }
            for (int i = 0; i < impl.OutParams.Count; i++)
            {
                Variable outParam = impl.OutParams[i];
                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type));
                locals.Add(copy);
                map[impl.OutParams[i]] = Expr.Ident(copy);
            }
            Dictionary<Variable, Expr> ogOldLocalMap = new Dictionary<Variable, Expr>();
            Dictionary<Variable, Expr> assumeMap = new Dictionary<Variable, Expr>(map);
            foreach (IdentifierExpr ie in globalMods)
            {
                Variable g = ie.Decl;
                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_local_old_{0}", g.Name), g.TypedIdent.Type));
                locals.Add(copy);
                ogOldLocalMap[g] = Expr.Ident(copy);
                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type), true);
                inputs.Add(f);
                assumeMap[g] = Expr.Ident(f);
            }

            Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap);
            Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap);
            Substitution subst = Substituter.SubstitutionFromHashtable(map);
            List<Block> yieldCheckerBlocks = new List<Block>();
            List<String> labels = new List<String>();
            List<Block> labelTargets = new List<Block>();
            Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));
            labels.Add(yieldCheckerBlock.Label);
            labelTargets.Add(yieldCheckerBlock);
            yieldCheckerBlocks.Add(yieldCheckerBlock);
            int yieldCount = 0;
            foreach (List<Cmd> cs in yields)
            {
                List<Cmd> newCmds = new List<Cmd>();
                foreach (Cmd cmd in cs)
                {
                    PredicateCmd predCmd = (PredicateCmd)cmd;
                    newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr)));
                }
                foreach (Cmd cmd in cs)
                {
                    PredicateCmd predCmd = (PredicateCmd)cmd;
                    var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);
                    if (predCmd is AssertCmd)
                    {
                        AssertCmd assertCmd = new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes);
                        assertCmd.ErrorData = "Non-interference check failed";
                        newCmds.Add(assertCmd);
                    }
                    else
                    {
                        newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));
                    }
                }
                newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
                yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken));
                labels.Add(yieldCheckerBlock.Label);
                labelTargets.Add(yieldCheckerBlock);
                yieldCheckerBlocks.Add(yieldCheckerBlock);
            }
            yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), new GotoCmd(Token.NoToken, labels, labelTargets)));

            // Create the yield checker procedure
            var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", "Impl", impl.Name);
//.........这里部分代码省略.........

 private void ProcessLoopHeaders(Implementation impl, Graph<Block> graph, HashSet<Block> yieldingHeaders, 
     Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap,
     out List<Variable> oldPcs, out List<Variable> oldOks)
 {
     oldPcs = new List<Variable>();
     oldOks = new List<Variable>();
     foreach (Block header in yieldingHeaders)
     {
         LocalVariable oldPc = null;
         LocalVariable oldOk = null;
         if (pc != null)
         {
             oldPc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", pc.Name, header.Label), Type.Bool));
             oldPcs.Add(oldPc);
             oldOk = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", ok.Name, header.Label), Type.Bool));
             oldOks.Add(oldOk);
         }
         Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(header), domainNameToInputVar);
         foreach (Block pred in header.Predecessors)
         {
             AddCallToYieldProc(header.tok, pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);
             if (pc != null && !graph.BackEdgeNodes(header).Contains(pred))
             {
                 pred.Cmds.Add(new AssignCmd(Token.NoToken, new List<AssignLhs>(
                     new AssignLhs[] { new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)), new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)) }),
                     new List<Expr>(new Expr[] { Expr.Ident(pc), Expr.Ident(ok) })));
             }
             AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
         }
         List<Cmd> newCmds = new List<Cmd>();
         if (pc != null)
         {
             AssertCmd assertCmd;
             assertCmd = new AssertCmd(header.tok, Expr.Eq(Expr.Ident(oldPc), Expr.Ident(pc)));
             assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";
             newCmds.Add(assertCmd);
             assertCmd = new AssertCmd(header.tok, Expr.Imp(Expr.Ident(oldOk), Expr.Ident(ok)));
             assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";
             newCmds.Add(assertCmd);
         }
         foreach (string domainName in linearTypeChecker.linearDomains.Keys)
         {
             newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));
         }
         foreach (Variable v in ogOldGlobalMap.Keys)
         {
             newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(v), Expr.Ident(ogOldGlobalMap[v]))));
         }
         newCmds.AddRange(header.Cmds);
         header.Cmds = newCmds;
     }
 }

        private List<List<Cmd>> CollectAndDesugarYields(Implementation impl,
            Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap)
        {
            // Collect the yield predicates and desugar yields
            List<List<Cmd>> yields = new List<List<Cmd>>();
            List<Cmd> cmds = new List<Cmd>();
            foreach (Block b in impl.Blocks)
            {
                YieldCmd yieldCmd = null;
                List<Cmd> newCmds = new List<Cmd>();
                for (int i = 0; i < b.Cmds.Count; i++)
                {
                    Cmd cmd = b.Cmds[i];
                    if (cmd is YieldCmd)
                    {
                        yieldCmd = (YieldCmd)cmd;
                        continue;
                    }
                    if (yieldCmd != null)
                    {
                        PredicateCmd pcmd = cmd as PredicateCmd;
                        if (pcmd == null)
                        {
                            DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar);
                            if (cmds.Count > 0)
                            {
                                yields.Add(cmds);
                                cmds = new List<Cmd>();
                            }
                            yieldCmd = null;
                        }
                        else
                        {
                            cmds.Add(pcmd);
                        }
                    }

                    if (cmd is CallCmd)
                    {
                        CallCmd callCmd = cmd as CallCmd;
                        if (yieldingProcs.Contains(callCmd.Proc))
                        {
                            AddCallToYieldProc(callCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
                        }
                        if (callCmd.IsAsync)
                        {
                            if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name))
                            {
                                asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>());
                            }
                            var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];
                            CallCmd dummyCallCmd = new CallCmd(callCmd.tok, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs, callCmd.Attributes);
                            dummyCallCmd.Proc = dummyAsyncTargetProc;
                            newCmds.Add(dummyCallCmd);
                        }
                        else
                        {
                            newCmds.Add(callCmd);
                        }
                        if (yieldingProcs.Contains(callCmd.Proc))
                        {
                            HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(callCmd));
                            linearTypeChecker.AddAvailableVars(callCmd, availableLinearVars);

                            if (!callCmd.IsAsync && globalMods.Count > 0 && pc != null)
                            {
                                // assume pc || alpha(i, g);
                                Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
                                assumeExpr.Type = Type.Bool;
                                newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
                            }

                            Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
                            AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
                        }
                    }
                    else if (cmd is ParCallCmd)
                    {
                        ParCallCmd parCallCmd = cmd as ParCallCmd;
                        AddCallToYieldProc(parCallCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
                        DesugarParallelCallCmd(newCmds, parCallCmd);
                        HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd));
                        linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars);

                        if (globalMods.Count > 0 && pc != null)
                        {
                            // assume pc || alpha(i, g);
                            Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
                            assumeExpr.Type = Type.Bool;
                            newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
                        }

                        Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
                        AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
                    }
                    else
                    {
                        newCmds.Add(cmd);
                    }
                }
//.........这里部分代码省略.........

 private Graph<Block> ComputeYieldingLoopHeaders(Implementation impl, out HashSet<Block> yieldingHeaders)
 {
     Graph<Block> graph;
     impl.PruneUnreachableBlocks();
     impl.ComputePredecessorsForBlocks();
     graph = Program.GraphFromImpl(impl);
     graph.ComputeLoops();
     if (!graph.Reducible)
     {
         throw new Exception("Irreducible flow graphs are unsupported.");
     }
     yieldingHeaders = new HashSet<Block>();
     IEnumerable<Block> sortedHeaders = graph.SortHeadersByDominance();
     foreach (Block header in sortedHeaders)
     {
         if (yieldingHeaders.Any(x => graph.DominatorMap.DominatedBy(x, header)))
         {
             yieldingHeaders.Add(header);
         }
         else if (IsYieldingHeader(graph, header))
         {
             yieldingHeaders.Add(header);
         }
         else
         {
             continue;
         }
     }
     return graph;
 }