From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Doomed/VCDoomed.cs | 1652 ++++++++++++++++++++++----------------------- 1 file changed, 826 insertions(+), 826 deletions(-) (limited to 'Source/Doomed/VCDoomed.cs') diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs index d4d4db21..822fb9c0 100644 --- a/Source/Doomed/VCDoomed.cs +++ b/Source/Doomed/VCDoomed.cs @@ -1,826 +1,826 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Collections; -using System.Collections.Generic; -using System.Diagnostics; -using System.Threading; -using System.IO; -using Microsoft.Boogie; -using Microsoft.Boogie.GraphUtil; -using System.Diagnostics.Contracts; -using Microsoft.Basetypes; -using Microsoft.Boogie.VCExprAST; - -namespace VC { - public partial class DCGen : ConditionGeneration { - private bool _print_time = CommandLineOptions.Clo.DoomStrategy!=-1; - #region Attributes - static private Dictionary/*!*/ m_BlockReachabilityMap; - Dictionary/*!*/ m_copiedBlocks = new Dictionary(); - const string reachvarsuffix = "__ivebeenthere"; - List/*!*/ m_doomedCmds = new List(); - [ContractInvariantMethod] - void ObjectInvariant() { - - } - - #endregion - - - /// - /// Constructor. Initializes the theorem prover. - /// - public DCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List checkers) - : base(program, checkers) { - Contract.Requires(program != null); - - this.appendLogFile = appendLogFile; - this.logFilePath = logFilePath; - m_BlockReachabilityMap = new Dictionary(); - } - - /// - /// Debug method that prints a dot file of the - /// current set of blocks in impl to filename. - /// - private void Impl2Dot(Implementation impl, string filename) { - Contract.Requires(impl != null); - Contract.Requires(filename != null); - List nodes = new List(); - List edges = new List(); - - 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(); - } - } - private const string _copyPrefix = "CPY__"; - - private List m_UncheckableBlocks = null; - - /// - /// MSchaef: - /// - remove loops and add reach variables - /// - make it a passive program - /// - compute the wlp for each block - /// - check if |= (reach=false) => wlp.S.false holds for each reach - /// - /// - public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) { - Contract.EnsuresOnThrow(true); - - Console.WriteLine(); - Console.WriteLine("Checking function {0}", impl.Name); - callback.OnProgress("doomdetector", 0, 0, 0); - - bool restartTP = CommandLineOptions.Clo.DoomRestartTP ; - - //Impl2Dot(impl, String.Format("c:/dot/{0}_orig.dot", impl.Name)); - - Transform4DoomedCheck(impl); - - //Impl2Dot(impl, String.Format("c:/dot/{0}_fin.dot", impl.Name)); - - Checker checker = FindCheckerFor(1000); - Contract.Assert(checker != null); - int assertionCount; - DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks, out assertionCount); - CumulativeAssertionCount += assertionCount; - - //EmitImpl(impl, false); - - int _totalchecks = 0; - - ProverInterface.Outcome outcome; - dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback); - - System.TimeSpan ts = new TimeSpan(); - - if (_print_time) Console.WriteLine("Total number of blocks {0}", impl.Blocks.Count); - - List lb; - List lv = new List(); - - while (dc.GetNextBlock(out lb)) - { - Contract.Assert(lb != null); - outcome = ProverInterface.Outcome.Undetermined; - - Variable v = null; - lv.Clear(); - - foreach (Block b_ in lb) - { - if (!m_BlockReachabilityMap.TryGetValue(b_, out v)) - { - // This should cause an error - continue; - } - //Console.Write("{0}, ",b_.Label); - lv.Add(v); - } - //Console.WriteLine(); - Dictionary finalreachvars = m_GetPostconditionVariables(impl.Blocks,lb); - if (lv.Count < 1) - { - - continue; - } - - Contract.Assert(lv != null); - _totalchecks++; - - - if (!dc.CheckLabel(lv,finalreachvars, out outcome)) { - return Outcome.Inconclusive; - } - ts += dc.DEBUG_ProverTime.Elapsed; - - if (restartTP) - { - checker.Close(); - checker = FindCheckerFor(1000); - dc.RespawnChecker(impl, checker); - dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback); - } - - } - checker.Close(); - - if (_print_time) - { - Console.WriteLine("Number of Checkes / #Blocks: {0} of {1}", _totalchecks, impl.Blocks.Count); - dc.__DEBUG_PrintStatistics(); - Console.WriteLine("Total time for this method: {0}", ts.ToString()); - } - #region Try to produce a counter example (brute force) - if (dc.DoomedSequences.Count > 0) { - int counter = 0; - List _all = new List(); - foreach (List lb_ in dc.DoomedSequences) - { - foreach (Block b_ in lb_) - { - if (!_all.Contains(b_) && !m_UncheckableBlocks.Contains(b_)) - { - _all.Add(b_); counter++; - if (!_print_time) Console.WriteLine(b_.Label); - } - } - } - if (_all.Count > 0) - { - Console.WriteLine("#Dead Blocks found: {0}: ", counter); - return Outcome.Errors; - } - } - #endregion - - - return Outcome.Correct; - } - - private Dictionary m_GetPostconditionVariables(List allblock, List passBlock) - { - Dictionary r = new Dictionary(); - foreach (Block b in allblock) - { - Variable v; - if (m_BlockReachabilityMap.TryGetValue(b, out v)) - { - if (passBlock.Contains(b)) r[m_LastReachVarIncarnation[v]] = 1; - } - else - { - Console.WriteLine("there is no reachability variable for {0}", b.Label); - } - } - return r; - } - -#if false - #region Error message construction - private void SearchCounterexample(Implementation impl, DoomErrorHandler errh, VerifierCallback callback) { - Contract.Requires(impl != null); - Contract.Requires(errh != null); - Contract.Requires(callback != null); - Contract.Requires(errh.m_Reachvar != null); - //if (errh.m_Reachvar==null) { - // Contract.Assert(false);throw new cce.UnreachableException(); - //} - m_doomedCmds.Clear(); - - Dictionary> cmdbackup = new Dictionary>(); - - BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, 0, impl.Blocks.Count / 2 - 1); - BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, impl.Blocks.Count / 2, impl.Blocks.Count - 1); - - List causals = CollectCausalStatements(impl.Blocks[0]); - foreach (Cmd c in causals) { - Contract.Assert(c != null); - GenerateErrorMessage(c, causals); - } - - #region Undo all modifications - foreach (KeyValuePair> kvp in cmdbackup) { - Contract.Assert(kvp.Key != null); - Contract.Assert(kvp.Value != null); - kvp.Key.Cmds = kvp.Value; - } - #endregion - } - - #region Causal Statement Tree - - private void GenerateErrorMessage(Cmd causalStatement, List causals) { - Contract.Requires(causalStatement != null); - Contract.Requires(cce.NonNullElements(causals)); - AssumeCmd uc = causalStatement as AssumeCmd; - AssertCmd ac = causalStatement as AssertCmd; - ConsoleColor col = Console.ForegroundColor; - - // Trivial case. Must be either assume or assert false - if (m_doomedCmds.Count == 1) { - Console.WriteLine("Found a trivial error:"); - if (uc != null) { - Console.Write("Trivial false assumption: "); - Console.Write("({0};{1}):", uc.tok.line, uc.tok.col); - } - if (ac != null) { - Console.Write("Trivial false assertion: "); - Console.Write("({0};{1}):", ac.tok.line, ac.tok.col); - } - causalStatement.Emit(new TokenTextWriter("", Console.Out, false), 0); - } else { - // Safety error - if (ac != null) { - Console.ForegroundColor = ConsoleColor.Red; - Console.WriteLine("Safety error:"); - Console.ForegroundColor = col; - Console.Write("This assertion is violated: "); - Console.Write("({0};{1}):", ac.tok.line, ac.tok.col); - ac.Emit(new TokenTextWriter("", Console.Out, false), 0); - } - if (uc != null) { - bool containsAssert = false; - foreach (Cmd c in m_doomedCmds) { - Contract.Assert(c != null); - if (causals.Contains(c)) { - continue; - } - AssertCmd asrt = c as AssertCmd; - if (asrt != null) { - containsAssert = true; - break; - } - } - // Plausibility error - if (containsAssert) { - Console.ForegroundColor = ConsoleColor.Yellow; - Console.WriteLine("Plausibility error:"); - Console.ForegroundColor = col; - Console.Write("There is no legal exeuction passing: "); - Console.Write("({0};{1})", uc.tok.line, uc.tok.col); - uc.Emit(new TokenTextWriter("", Console.Out, false), 0); - } else { // Reachability error - Console.ForegroundColor = ConsoleColor.DarkRed; - Console.WriteLine("Reachability error:"); - Console.ForegroundColor = col; - Console.Write("No execution can reach: "); - Console.Write("({0};{1})", uc.tok.line, uc.tok.col); - uc.Emit(new TokenTextWriter("", Console.Out, false), 0); - } - - } - - Console.ForegroundColor = ConsoleColor.White; - Console.WriteLine("...on any execution passing through:"); - foreach (Cmd c in m_doomedCmds) { - Contract.Assert(c != null); - if (causals.Contains(c)) { - continue; - } - Console.ForegroundColor = col; - Console.Write("In ({0};{1}): ", c.tok.line, c.tok.col); - Console.ForegroundColor = ConsoleColor.DarkYellow; - c.Emit(new TokenTextWriter("", Console.Out, false), 0); - } - Console.ForegroundColor = col; - Console.WriteLine("--"); - - } - } - - private List CollectCausalStatements(Block b) { - Contract.Requires(b != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - - Cmd lastCausal = null; - foreach (Cmd c in b.Cmds) { - Contract.Assert(c != null); - AssertCmd ac = c as AssertCmd; - AssumeCmd uc = c as AssumeCmd; - if (ac != null && !ContainsReachVariable(ac)) { - if (ac.Expr != Expr.True) { - lastCausal = c; - } - } else if (uc != null && !ContainsReachVariable(uc)) { - lastCausal = c; - } - } - - List causals = new List(); - GotoCmd gc = b.TransferCmd as GotoCmd; - if (gc != null && gc.labelTargets != null) { - List tmp; - //bool allcausal = true; - foreach (Block b_ in gc.labelTargets) { - Contract.Assert(b_ != null); - tmp = CollectCausalStatements(b_); - - foreach (Cmd cau in tmp) { - if (!causals.Contains(cau)) - causals.Add(cau); - } - } - //if (allcausal) - if (causals.Count > 0) - return causals; - } - if (lastCausal != null) - causals.Add(lastCausal); - return causals; - } - - #endregion - - bool BruteForceCESearch(Variable reachvar, Implementation impl, VerifierCallback callback, - Dictionary> cmdbackup, int startidx, int endidx) { - Contract.Requires(reachvar != null); - Contract.Requires(impl != null); - Contract.Requires(callback != null); - Contract.Requires(cce.NonNullElements(cmdbackup)); - #region Modify implementation - for (int i = startidx; i <= endidx; i++) { - if (_copiedBlock.Contains(impl.Blocks[i])) - continue; - List cs = new List(); - cmdbackup.Add(impl.Blocks[i], impl.Blocks[i].Cmds); - foreach (Cmd c in impl.Blocks[i].Cmds) { - Contract.Assert(c != null); - if (ContainsReachVariable(c)) { - cs.Add(c); - continue; - } - AssertCmd ac = c as AssertCmd; - AssumeCmd uc = c as AssumeCmd; - if (ac != null) { - cs.Add(new AssertCmd(ac.tok, Expr.True)); - } else if (uc != null) { - cs.Add(new AssertCmd(uc.tok, Expr.True)); - } else { - cs.Add(c); - } - } - impl.Blocks[i].Cmds = cs; - } - #endregion - - ProverInterface.Outcome outcome = ProverInterface.Outcome.Undetermined; - if (!ReCheckImpl(reachvar, impl, callback, out outcome)) { - UndoBlockModifications(impl, cmdbackup, startidx, endidx); - return false; - } - if (outcome == ProverInterface.Outcome.Valid) { - return true; - } else if (outcome == ProverInterface.Outcome.Invalid) { - UndoBlockModifications(impl, cmdbackup, startidx, endidx); - int mid = startidx + (endidx - startidx) / 2; - if (startidx >= endidx) { - // Now we found an interesting Block and we have to - // search for the interesting statements. - int cmdcount = impl.Blocks[endidx].Cmds.Length; - BruteForceCmd(impl.Blocks[endidx], 0, cmdcount / 2 - 1, reachvar, impl, callback); - BruteForceCmd(impl.Blocks[endidx], cmdcount / 2, cmdcount - 1, reachvar, impl, callback); - return true; - } else { - BruteForceCESearch(reachvar, impl, callback, cmdbackup, startidx, mid); - BruteForceCESearch(reachvar, impl, callback, cmdbackup, mid + 1, endidx); - return true; - } - } else { - UndoBlockModifications(impl, cmdbackup, startidx, endidx); - return false; - } - } - - bool BruteForceCmd(Block b, int startidx, int endidx, Variable reachvar, - Implementation impl, VerifierCallback callback) { - Contract.Requires(b != null); - Contract.Requires(reachvar != null); - Contract.Requires(impl != null); - Contract.Requires(callback != null); - #region Modify Cmds - List backup = b.Cmds; - Contract.Assert(backup != null); - List cs = new List(); - for (int i = 0; i < startidx; i++) { - cs.Add(b.Cmds[i]); - } - for (int i = startidx; i <= endidx; i++) { - Cmd c = b.Cmds[i]; - if (ContainsReachVariable(c)) { - cs.Add(c); - continue; - } - cs.Add(new AssertCmd(c.tok, Expr.True)); - } - for (int i = endidx + 1; i < b.Cmds.Length; i++) { - cs.Add(b.Cmds[i]); - } - - b.Cmds = cs; - #endregion - - #region Recheck - ProverInterface.Outcome outcome = ProverInterface.Outcome.Undetermined; - if (!ReCheckImpl(reachvar, impl, callback, out outcome)) { - b.Cmds = backup; - return false; - } - #endregion - - if (outcome == ProverInterface.Outcome.Valid) { - return true; - } else if (outcome == ProverInterface.Outcome.Invalid) { - b.Cmds = backup; - if (startidx >= endidx) { - if (!ContainsReachVariable(b.Cmds[endidx])) { - // Console.Write(" Witness ("); - // - // ConsoleColor col = Console.ForegroundColor; - // Console.ForegroundColor = ConsoleColor.White; - // Console.Write("{0};{1}", b.Cmds[endidx].tok.line, b.Cmds[endidx].tok.col ); - // Console.ForegroundColor = col; - // Console.Write("): "); - // Console.ForegroundColor = ConsoleColor.Yellow; - // b.Cmds[endidx].Emit(new TokenTextWriter("", Console.Out, false), 0); - // Console.ForegroundColor = col; - - m_doomedCmds.Add(b.Cmds[endidx]); - return true; - } else { - return false; - } - } else { - int mid = startidx + (endidx - startidx) / 2; - BruteForceCmd(b, startidx, mid, reachvar, impl, callback); - BruteForceCmd(b, mid + 1, endidx, reachvar, impl, callback); - return false; // This is pure random - } - } else { - b.Cmds = backup; - return false; - } - } - - void UndoBlockModifications(Implementation impl, Dictionary/*!*/>/*!*/ cmdbackup, - int startidx, int endidx) { - Contract.Requires(cce.NonNullElements(cmdbackup)); - Contract.Requires(impl != null); - for (int i = startidx; i <= endidx; i++) { - List cs = null; - if (cmdbackup.TryGetValue(impl.Blocks[i], out cs)) { - Contract.Assert(cs != null); - impl.Blocks[i].Cmds = cs; - cmdbackup.Remove(impl.Blocks[i]); - } - } - } - - bool ReCheckImpl(Variable reachvar, Implementation impl, VerifierCallback callback, - out ProverInterface.Outcome outcome) { - Contract.Requires(reachvar != null); - Contract.Requires(impl != null); - Contract.Requires(callback != null); - Checker checker = FindCheckerFor(impl, 1000); - Contract.Assert(checker != null); - DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks); - dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback); - outcome = ProverInterface.Outcome.Undetermined; - List rv = new List(); - rv.Add(reachvar); - if (!dc.CheckLabel(rv,null, out outcome)) { - checker.Close(); - return false; - } - checker.Close(); - return true; - } - - - - bool ContainsReachVariable(Cmd c) { - Contract.Requires(c != null); - AssertCmd artc = c as AssertCmd; - AssumeCmd amec = c as AssumeCmd; - Expr e; - if (artc != null) { - e = artc.Expr; - } else if (amec != null) { - e = amec.Expr; - } else { - return false; - } - Set freevars = new Set(); - e.ComputeFreeVariables(freevars); - foreach (Variable v in freevars) { - Contract.Assert(v != null); - if (v.Name.Contains(reachvarsuffix)) - return true; - } - return false; - } -#endregion -#endif - - - Block exitBlock; - - #region Program Passification - private void GenerateHelperBlocks(Implementation impl) { - Contract.Requires(impl != null); - Dictionary gotoCmdOrigins = new Dictionary(); - exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins); - Contract.Assert(exitBlock != null); - - AddBlocksBetween(impl.Blocks); - - #region Insert pre- and post-conditions and where clauses as assume and assert statements - { - List cc = new List(); - // where clauses of global variables - foreach (var gvar in program.GlobalVariables) { - if (gvar.TypedIdent.WhereExpr != null) { - Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr); - cc.Add(c); - } - } - // where clauses of in- and out-parameters - cc.AddRange(GetParamWhereClauses(impl)); - // where clauses of local variables - foreach (Variable lvar in impl.LocVars) { - Contract.Assert(lvar != null); - if (lvar.TypedIdent.WhereExpr != null) { - Cmd c = new AssumeCmd(lvar.tok, lvar.TypedIdent.WhereExpr); - cc.Add(c); - } - } - - // add cc and the preconditions to new blocks preceding impl.Blocks[0] - InjectPreconditions(impl, cc); - - // append postconditions, starting in exitBlock and continuing into other blocks, if needed - InjectPostConditions(impl, exitBlock, gotoCmdOrigins); - } - #endregion - } - - - private Dictionary PassifyProgram(Implementation impl, ModelViewInfo mvInfo) { - Contract.Requires(impl != null); - Contract.Requires(mvInfo != null); - Contract.Requires(this.exitBlock != null); - Contract.Ensures(Contract.Result() != null); - - CurrentLocalVariables = impl.LocVars; - return Convert2PassiveCmd(impl, mvInfo); - //return new Hashtable(); - } - - /// - /// Add additional variable to allow checking as described in the paper - /// "It's doomed; we can prove it" - /// - private List GenerateReachabilityPredicates(Implementation impl) - { - Contract.Requires(impl != null); - - foreach (Block b in impl.Blocks) - { - Contract.Assert(b != null); - //if (b.Predecessors.Length==0) continue; - //if (b.Cmds.Length == 0 ) continue; - - Variable v_ = new LocalVariable(Token.NoToken, - new TypedIdent(b.tok, b.Label + reachvarsuffix, new BasicType(SimpleType.Int ))); - - impl.LocVars.Add(v_); - - m_BlockReachabilityMap[b] = v_; - - IdentifierExpr lhs = new IdentifierExpr(b.tok, v_); - Contract.Assert(lhs != null); - - impl.Proc.Modifies.Add(lhs); - - List lhsl = new List(); - lhsl.Add(new SimpleAssignLhs(Token.NoToken, lhs)); - List rhsl = new List(); - rhsl.Add(Expr.Literal(1) ); - - - List cs = new List { new AssignCmd(Token.NoToken, lhsl, rhsl) }; - cs.AddRange(b.Cmds); - b.Cmds = cs; - - //checkBlocks.Add(new CheckableBlock(v_,b)); - } - - List incReachVars = new List(); - foreach (KeyValuePair kvp in m_BlockReachabilityMap) - { - IdentifierExpr lhs = new IdentifierExpr(Token.NoToken, kvp.Value); - impl.Proc.Modifies.Add(lhs); - incReachVars.Add(new AssumeCmd(Token.NoToken, Expr.Le(lhs, Expr.Literal(1)))); - } - - return incReachVars; - } - - #endregion - - #region Compute loop-free approximation - - // this might be redundant, but I didn't find a better place to get this information. - private Dictionary m_LastReachVarIncarnation = new Dictionary(); - - private void Transform4DoomedCheck(Implementation impl) - { - variable2SequenceNumber = new Dictionary(); - incarnationOriginMap = new Dictionary(); - if (impl.Blocks.Count < 1) return; - - impl.PruneUnreachableBlocks(); - AddBlocksBetween(impl.Blocks); - ResetPredecessors(impl.Blocks); - - GraphAnalyzer ga = new GraphAnalyzer(impl.Blocks); - LoopRemover lr = new LoopRemover(ga); - lr.AbstractLoopUnrolling(); - - impl.Blocks = ga.ToImplementation(out m_UncheckableBlocks); - ResetPredecessors(impl.Blocks); - - // Check for the "BlocksBetween" if all their successors are in m_UncheckableBlocks - List oldblocks = new List(); - oldblocks.AddRange(impl.Blocks); - GenerateHelperBlocks(impl); - #region Check for the "BlocksBetween" if all their successors are in m_UncheckableBlocks - foreach (Block b in impl.Blocks) - { - if (oldblocks.Contains(b)) continue; - GotoCmd gc = b.TransferCmd as GotoCmd; - if (gc != null) - { - bool allsuccUncheckable = true; - foreach (Block _b in gc.labelTargets) - { - if (!m_UncheckableBlocks.Contains(_b)) - { - allsuccUncheckable = false; break; - } - } - if (allsuccUncheckable && !m_UncheckableBlocks.Contains(b)) m_UncheckableBlocks.Add(b); - } - } - #endregion - - impl.Blocks = DeepCopyBlocks(impl.Blocks, m_UncheckableBlocks); - - m_BlockReachabilityMap = new Dictionary(); - List cs = GenerateReachabilityPredicates(impl); - - //foreach (Block test in getTheFFinalBlock(impl.Blocks[0])) - //{ - // test.Cmds.AddRange(cs); - //} - - ResetPredecessors(impl.Blocks); - //EmitImpl(impl,false); - - Dictionary var2Expr = PassifyProgram(impl, new ModelViewInfo(program, impl)); - - // Collect the last incarnation of each reachability variable in the passive program - foreach (KeyValuePair kvp in m_BlockReachabilityMap) - { - if (var2Expr.ContainsKey(kvp.Value)) - { - m_LastReachVarIncarnation[kvp.Value] = (Expr)var2Expr[kvp.Value]; - } - } - } - - - List getTheFFinalBlock(Block b) - { - List lb = new List(); - GotoCmd gc = b.TransferCmd as GotoCmd; - if (gc == null) lb.Add(b); - else - { - foreach (Block s in gc.labelTargets) - { - foreach (Block r in getTheFFinalBlock(s)) if (!lb.Contains(r)) lb.Add(r); - } - } - return lb; - } - - - private List DeepCopyBlocks(List lb, List uncheckables) - { - List clones = new List(); - List uncheck_ = new List(); - Dictionary clonemap = new Dictionary(); - - foreach (Block b in lb) - { - Block clone = CloneBlock(b); - clones.Add(clone); - clonemap[b] = clone; - if (uncheckables.Contains(b)) uncheck_.Add(clone); - } - uncheckables.Clear(); - uncheckables.AddRange(uncheck_); - // update the successors and predecessors - foreach (Block b in lb) - { - List newpreds = new List(); - foreach (Block b_ in b.Predecessors) - { - newpreds.Add(clonemap[b_]); - } - clonemap[b].Predecessors = newpreds; - GotoCmd gc = b.TransferCmd as GotoCmd; - ReturnCmd rc = b.TransferCmd as ReturnCmd; - if (gc != null) - { - List lseq = new List(); - List bseq = new List(); - foreach (string s in gc.labelNames) lseq.Add(s); - foreach (Block b_ in gc.labelTargets) bseq.Add(clonemap[b_]); - GotoCmd tcmd = new GotoCmd(gc.tok, lseq, bseq); - clonemap[b].TransferCmd = tcmd; - } - else if (rc != null) - { - clonemap[b].TransferCmd = new ReturnCmd(rc.tok); - } - } - return clones; - } - - private Block CloneBlock(Block b) - { - Block clone = new Block(b.tok, b.Label, b.Cmds, b.TransferCmd); - if (this.exitBlock == b) this.exitBlock = clone; - return clone; - } - #endregion - } -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Collections; +using System.Collections.Generic; +using System.Diagnostics; +using System.Threading; +using System.IO; +using Microsoft.Boogie; +using Microsoft.Boogie.GraphUtil; +using System.Diagnostics.Contracts; +using Microsoft.Basetypes; +using Microsoft.Boogie.VCExprAST; + +namespace VC { + public partial class DCGen : ConditionGeneration { + private bool _print_time = CommandLineOptions.Clo.DoomStrategy!=-1; + #region Attributes + static private Dictionary/*!*/ m_BlockReachabilityMap; + Dictionary/*!*/ m_copiedBlocks = new Dictionary(); + const string reachvarsuffix = "__ivebeenthere"; + List/*!*/ m_doomedCmds = new List(); + [ContractInvariantMethod] + void ObjectInvariant() { + + } + + #endregion + + + /// + /// Constructor. Initializes the theorem prover. + /// + public DCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List checkers) + : base(program, checkers) { + Contract.Requires(program != null); + + this.appendLogFile = appendLogFile; + this.logFilePath = logFilePath; + m_BlockReachabilityMap = new Dictionary(); + } + + /// + /// Debug method that prints a dot file of the + /// current set of blocks in impl to filename. + /// + private void Impl2Dot(Implementation impl, string filename) { + Contract.Requires(impl != null); + Contract.Requires(filename != null); + List nodes = new List(); + List edges = new List(); + + 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(); + } + } + private const string _copyPrefix = "CPY__"; + + private List m_UncheckableBlocks = null; + + /// + /// MSchaef: + /// - remove loops and add reach variables + /// - make it a passive program + /// - compute the wlp for each block + /// - check if |= (reach=false) => wlp.S.false holds for each reach + /// + /// + public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) { + Contract.EnsuresOnThrow(true); + + Console.WriteLine(); + Console.WriteLine("Checking function {0}", impl.Name); + callback.OnProgress("doomdetector", 0, 0, 0); + + bool restartTP = CommandLineOptions.Clo.DoomRestartTP ; + + //Impl2Dot(impl, String.Format("c:/dot/{0}_orig.dot", impl.Name)); + + Transform4DoomedCheck(impl); + + //Impl2Dot(impl, String.Format("c:/dot/{0}_fin.dot", impl.Name)); + + Checker checker = FindCheckerFor(1000); + Contract.Assert(checker != null); + int assertionCount; + DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks, out assertionCount); + CumulativeAssertionCount += assertionCount; + + //EmitImpl(impl, false); + + int _totalchecks = 0; + + ProverInterface.Outcome outcome; + dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback); + + System.TimeSpan ts = new TimeSpan(); + + if (_print_time) Console.WriteLine("Total number of blocks {0}", impl.Blocks.Count); + + List lb; + List lv = new List(); + + while (dc.GetNextBlock(out lb)) + { + Contract.Assert(lb != null); + outcome = ProverInterface.Outcome.Undetermined; + + Variable v = null; + lv.Clear(); + + foreach (Block b_ in lb) + { + if (!m_BlockReachabilityMap.TryGetValue(b_, out v)) + { + // This should cause an error + continue; + } + //Console.Write("{0}, ",b_.Label); + lv.Add(v); + } + //Console.WriteLine(); + Dictionary finalreachvars = m_GetPostconditionVariables(impl.Blocks,lb); + if (lv.Count < 1) + { + + continue; + } + + Contract.Assert(lv != null); + _totalchecks++; + + + if (!dc.CheckLabel(lv,finalreachvars, out outcome)) { + return Outcome.Inconclusive; + } + ts += dc.DEBUG_ProverTime.Elapsed; + + if (restartTP) + { + checker.Close(); + checker = FindCheckerFor(1000); + dc.RespawnChecker(impl, checker); + dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback); + } + + } + checker.Close(); + + if (_print_time) + { + Console.WriteLine("Number of Checkes / #Blocks: {0} of {1}", _totalchecks, impl.Blocks.Count); + dc.__DEBUG_PrintStatistics(); + Console.WriteLine("Total time for this method: {0}", ts.ToString()); + } + #region Try to produce a counter example (brute force) + if (dc.DoomedSequences.Count > 0) { + int counter = 0; + List _all = new List(); + foreach (List lb_ in dc.DoomedSequences) + { + foreach (Block b_ in lb_) + { + if (!_all.Contains(b_) && !m_UncheckableBlocks.Contains(b_)) + { + _all.Add(b_); counter++; + if (!_print_time) Console.WriteLine(b_.Label); + } + } + } + if (_all.Count > 0) + { + Console.WriteLine("#Dead Blocks found: {0}: ", counter); + return Outcome.Errors; + } + } + #endregion + + + return Outcome.Correct; + } + + private Dictionary m_GetPostconditionVariables(List allblock, List passBlock) + { + Dictionary r = new Dictionary(); + foreach (Block b in allblock) + { + Variable v; + if (m_BlockReachabilityMap.TryGetValue(b, out v)) + { + if (passBlock.Contains(b)) r[m_LastReachVarIncarnation[v]] = 1; + } + else + { + Console.WriteLine("there is no reachability variable for {0}", b.Label); + } + } + return r; + } + +#if false + #region Error message construction + private void SearchCounterexample(Implementation impl, DoomErrorHandler errh, VerifierCallback callback) { + Contract.Requires(impl != null); + Contract.Requires(errh != null); + Contract.Requires(callback != null); + Contract.Requires(errh.m_Reachvar != null); + //if (errh.m_Reachvar==null) { + // Contract.Assert(false);throw new cce.UnreachableException(); + //} + m_doomedCmds.Clear(); + + Dictionary> cmdbackup = new Dictionary>(); + + BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, 0, impl.Blocks.Count / 2 - 1); + BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, impl.Blocks.Count / 2, impl.Blocks.Count - 1); + + List causals = CollectCausalStatements(impl.Blocks[0]); + foreach (Cmd c in causals) { + Contract.Assert(c != null); + GenerateErrorMessage(c, causals); + } + + #region Undo all modifications + foreach (KeyValuePair> kvp in cmdbackup) { + Contract.Assert(kvp.Key != null); + Contract.Assert(kvp.Value != null); + kvp.Key.Cmds = kvp.Value; + } + #endregion + } + + #region Causal Statement Tree + + private void GenerateErrorMessage(Cmd causalStatement, List causals) { + Contract.Requires(causalStatement != null); + Contract.Requires(cce.NonNullElements(causals)); + AssumeCmd uc = causalStatement as AssumeCmd; + AssertCmd ac = causalStatement as AssertCmd; + ConsoleColor col = Console.ForegroundColor; + + // Trivial case. Must be either assume or assert false + if (m_doomedCmds.Count == 1) { + Console.WriteLine("Found a trivial error:"); + if (uc != null) { + Console.Write("Trivial false assumption: "); + Console.Write("({0};{1}):", uc.tok.line, uc.tok.col); + } + if (ac != null) { + Console.Write("Trivial false assertion: "); + Console.Write("({0};{1}):", ac.tok.line, ac.tok.col); + } + causalStatement.Emit(new TokenTextWriter("", Console.Out, false), 0); + } else { + // Safety error + if (ac != null) { + Console.ForegroundColor = ConsoleColor.Red; + Console.WriteLine("Safety error:"); + Console.ForegroundColor = col; + Console.Write("This assertion is violated: "); + Console.Write("({0};{1}):", ac.tok.line, ac.tok.col); + ac.Emit(new TokenTextWriter("", Console.Out, false), 0); + } + if (uc != null) { + bool containsAssert = false; + foreach (Cmd c in m_doomedCmds) { + Contract.Assert(c != null); + if (causals.Contains(c)) { + continue; + } + AssertCmd asrt = c as AssertCmd; + if (asrt != null) { + containsAssert = true; + break; + } + } + // Plausibility error + if (containsAssert) { + Console.ForegroundColor = ConsoleColor.Yellow; + Console.WriteLine("Plausibility error:"); + Console.ForegroundColor = col; + Console.Write("There is no legal exeuction passing: "); + Console.Write("({0};{1})", uc.tok.line, uc.tok.col); + uc.Emit(new TokenTextWriter("", Console.Out, false), 0); + } else { // Reachability error + Console.ForegroundColor = ConsoleColor.DarkRed; + Console.WriteLine("Reachability error:"); + Console.ForegroundColor = col; + Console.Write("No execution can reach: "); + Console.Write("({0};{1})", uc.tok.line, uc.tok.col); + uc.Emit(new TokenTextWriter("", Console.Out, false), 0); + } + + } + + Console.ForegroundColor = ConsoleColor.White; + Console.WriteLine("...on any execution passing through:"); + foreach (Cmd c in m_doomedCmds) { + Contract.Assert(c != null); + if (causals.Contains(c)) { + continue; + } + Console.ForegroundColor = col; + Console.Write("In ({0};{1}): ", c.tok.line, c.tok.col); + Console.ForegroundColor = ConsoleColor.DarkYellow; + c.Emit(new TokenTextWriter("", Console.Out, false), 0); + } + Console.ForegroundColor = col; + Console.WriteLine("--"); + + } + } + + private List CollectCausalStatements(Block b) { + Contract.Requires(b != null); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + + Cmd lastCausal = null; + foreach (Cmd c in b.Cmds) { + Contract.Assert(c != null); + AssertCmd ac = c as AssertCmd; + AssumeCmd uc = c as AssumeCmd; + if (ac != null && !ContainsReachVariable(ac)) { + if (ac.Expr != Expr.True) { + lastCausal = c; + } + } else if (uc != null && !ContainsReachVariable(uc)) { + lastCausal = c; + } + } + + List causals = new List(); + GotoCmd gc = b.TransferCmd as GotoCmd; + if (gc != null && gc.labelTargets != null) { + List tmp; + //bool allcausal = true; + foreach (Block b_ in gc.labelTargets) { + Contract.Assert(b_ != null); + tmp = CollectCausalStatements(b_); + + foreach (Cmd cau in tmp) { + if (!causals.Contains(cau)) + causals.Add(cau); + } + } + //if (allcausal) + if (causals.Count > 0) + return causals; + } + if (lastCausal != null) + causals.Add(lastCausal); + return causals; + } + + #endregion + + bool BruteForceCESearch(Variable reachvar, Implementation impl, VerifierCallback callback, + Dictionary> cmdbackup, int startidx, int endidx) { + Contract.Requires(reachvar != null); + Contract.Requires(impl != null); + Contract.Requires(callback != null); + Contract.Requires(cce.NonNullElements(cmdbackup)); + #region Modify implementation + for (int i = startidx; i <= endidx; i++) { + if (_copiedBlock.Contains(impl.Blocks[i])) + continue; + List cs = new List(); + cmdbackup.Add(impl.Blocks[i], impl.Blocks[i].Cmds); + foreach (Cmd c in impl.Blocks[i].Cmds) { + Contract.Assert(c != null); + if (ContainsReachVariable(c)) { + cs.Add(c); + continue; + } + AssertCmd ac = c as AssertCmd; + AssumeCmd uc = c as AssumeCmd; + if (ac != null) { + cs.Add(new AssertCmd(ac.tok, Expr.True)); + } else if (uc != null) { + cs.Add(new AssertCmd(uc.tok, Expr.True)); + } else { + cs.Add(c); + } + } + impl.Blocks[i].Cmds = cs; + } + #endregion + + ProverInterface.Outcome outcome = ProverInterface.Outcome.Undetermined; + if (!ReCheckImpl(reachvar, impl, callback, out outcome)) { + UndoBlockModifications(impl, cmdbackup, startidx, endidx); + return false; + } + if (outcome == ProverInterface.Outcome.Valid) { + return true; + } else if (outcome == ProverInterface.Outcome.Invalid) { + UndoBlockModifications(impl, cmdbackup, startidx, endidx); + int mid = startidx + (endidx - startidx) / 2; + if (startidx >= endidx) { + // Now we found an interesting Block and we have to + // search for the interesting statements. + int cmdcount = impl.Blocks[endidx].Cmds.Length; + BruteForceCmd(impl.Blocks[endidx], 0, cmdcount / 2 - 1, reachvar, impl, callback); + BruteForceCmd(impl.Blocks[endidx], cmdcount / 2, cmdcount - 1, reachvar, impl, callback); + return true; + } else { + BruteForceCESearch(reachvar, impl, callback, cmdbackup, startidx, mid); + BruteForceCESearch(reachvar, impl, callback, cmdbackup, mid + 1, endidx); + return true; + } + } else { + UndoBlockModifications(impl, cmdbackup, startidx, endidx); + return false; + } + } + + bool BruteForceCmd(Block b, int startidx, int endidx, Variable reachvar, + Implementation impl, VerifierCallback callback) { + Contract.Requires(b != null); + Contract.Requires(reachvar != null); + Contract.Requires(impl != null); + Contract.Requires(callback != null); + #region Modify Cmds + List backup = b.Cmds; + Contract.Assert(backup != null); + List cs = new List(); + for (int i = 0; i < startidx; i++) { + cs.Add(b.Cmds[i]); + } + for (int i = startidx; i <= endidx; i++) { + Cmd c = b.Cmds[i]; + if (ContainsReachVariable(c)) { + cs.Add(c); + continue; + } + cs.Add(new AssertCmd(c.tok, Expr.True)); + } + for (int i = endidx + 1; i < b.Cmds.Length; i++) { + cs.Add(b.Cmds[i]); + } + + b.Cmds = cs; + #endregion + + #region Recheck + ProverInterface.Outcome outcome = ProverInterface.Outcome.Undetermined; + if (!ReCheckImpl(reachvar, impl, callback, out outcome)) { + b.Cmds = backup; + return false; + } + #endregion + + if (outcome == ProverInterface.Outcome.Valid) { + return true; + } else if (outcome == ProverInterface.Outcome.Invalid) { + b.Cmds = backup; + if (startidx >= endidx) { + if (!ContainsReachVariable(b.Cmds[endidx])) { + // Console.Write(" Witness ("); + // + // ConsoleColor col = Console.ForegroundColor; + // Console.ForegroundColor = ConsoleColor.White; + // Console.Write("{0};{1}", b.Cmds[endidx].tok.line, b.Cmds[endidx].tok.col ); + // Console.ForegroundColor = col; + // Console.Write("): "); + // Console.ForegroundColor = ConsoleColor.Yellow; + // b.Cmds[endidx].Emit(new TokenTextWriter("", Console.Out, false), 0); + // Console.ForegroundColor = col; + + m_doomedCmds.Add(b.Cmds[endidx]); + return true; + } else { + return false; + } + } else { + int mid = startidx + (endidx - startidx) / 2; + BruteForceCmd(b, startidx, mid, reachvar, impl, callback); + BruteForceCmd(b, mid + 1, endidx, reachvar, impl, callback); + return false; // This is pure random + } + } else { + b.Cmds = backup; + return false; + } + } + + void UndoBlockModifications(Implementation impl, Dictionary/*!*/>/*!*/ cmdbackup, + int startidx, int endidx) { + Contract.Requires(cce.NonNullElements(cmdbackup)); + Contract.Requires(impl != null); + for (int i = startidx; i <= endidx; i++) { + List cs = null; + if (cmdbackup.TryGetValue(impl.Blocks[i], out cs)) { + Contract.Assert(cs != null); + impl.Blocks[i].Cmds = cs; + cmdbackup.Remove(impl.Blocks[i]); + } + } + } + + bool ReCheckImpl(Variable reachvar, Implementation impl, VerifierCallback callback, + out ProverInterface.Outcome outcome) { + Contract.Requires(reachvar != null); + Contract.Requires(impl != null); + Contract.Requires(callback != null); + Checker checker = FindCheckerFor(impl, 1000); + Contract.Assert(checker != null); + DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks); + dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback); + outcome = ProverInterface.Outcome.Undetermined; + List rv = new List(); + rv.Add(reachvar); + if (!dc.CheckLabel(rv,null, out outcome)) { + checker.Close(); + return false; + } + checker.Close(); + return true; + } + + + + bool ContainsReachVariable(Cmd c) { + Contract.Requires(c != null); + AssertCmd artc = c as AssertCmd; + AssumeCmd amec = c as AssumeCmd; + Expr e; + if (artc != null) { + e = artc.Expr; + } else if (amec != null) { + e = amec.Expr; + } else { + return false; + } + Set freevars = new Set(); + e.ComputeFreeVariables(freevars); + foreach (Variable v in freevars) { + Contract.Assert(v != null); + if (v.Name.Contains(reachvarsuffix)) + return true; + } + return false; + } +#endregion +#endif + + + Block exitBlock; + + #region Program Passification + private void GenerateHelperBlocks(Implementation impl) { + Contract.Requires(impl != null); + Dictionary gotoCmdOrigins = new Dictionary(); + exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins); + Contract.Assert(exitBlock != null); + + AddBlocksBetween(impl.Blocks); + + #region Insert pre- and post-conditions and where clauses as assume and assert statements + { + List cc = new List(); + // where clauses of global variables + foreach (var gvar in program.GlobalVariables) { + if (gvar.TypedIdent.WhereExpr != null) { + Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr); + cc.Add(c); + } + } + // where clauses of in- and out-parameters + cc.AddRange(GetParamWhereClauses(impl)); + // where clauses of local variables + foreach (Variable lvar in impl.LocVars) { + Contract.Assert(lvar != null); + if (lvar.TypedIdent.WhereExpr != null) { + Cmd c = new AssumeCmd(lvar.tok, lvar.TypedIdent.WhereExpr); + cc.Add(c); + } + } + + // add cc and the preconditions to new blocks preceding impl.Blocks[0] + InjectPreconditions(impl, cc); + + // append postconditions, starting in exitBlock and continuing into other blocks, if needed + InjectPostConditions(impl, exitBlock, gotoCmdOrigins); + } + #endregion + } + + + private Dictionary PassifyProgram(Implementation impl, ModelViewInfo mvInfo) { + Contract.Requires(impl != null); + Contract.Requires(mvInfo != null); + Contract.Requires(this.exitBlock != null); + Contract.Ensures(Contract.Result() != null); + + CurrentLocalVariables = impl.LocVars; + return Convert2PassiveCmd(impl, mvInfo); + //return new Hashtable(); + } + + /// + /// Add additional variable to allow checking as described in the paper + /// "It's doomed; we can prove it" + /// + private List GenerateReachabilityPredicates(Implementation impl) + { + Contract.Requires(impl != null); + + foreach (Block b in impl.Blocks) + { + Contract.Assert(b != null); + //if (b.Predecessors.Length==0) continue; + //if (b.Cmds.Length == 0 ) continue; + + Variable v_ = new LocalVariable(Token.NoToken, + new TypedIdent(b.tok, b.Label + reachvarsuffix, new BasicType(SimpleType.Int ))); + + impl.LocVars.Add(v_); + + m_BlockReachabilityMap[b] = v_; + + IdentifierExpr lhs = new IdentifierExpr(b.tok, v_); + Contract.Assert(lhs != null); + + impl.Proc.Modifies.Add(lhs); + + List lhsl = new List(); + lhsl.Add(new SimpleAssignLhs(Token.NoToken, lhs)); + List rhsl = new List(); + rhsl.Add(Expr.Literal(1) ); + + + List cs = new List { new AssignCmd(Token.NoToken, lhsl, rhsl) }; + cs.AddRange(b.Cmds); + b.Cmds = cs; + + //checkBlocks.Add(new CheckableBlock(v_,b)); + } + + List incReachVars = new List(); + foreach (KeyValuePair kvp in m_BlockReachabilityMap) + { + IdentifierExpr lhs = new IdentifierExpr(Token.NoToken, kvp.Value); + impl.Proc.Modifies.Add(lhs); + incReachVars.Add(new AssumeCmd(Token.NoToken, Expr.Le(lhs, Expr.Literal(1)))); + } + + return incReachVars; + } + + #endregion + + #region Compute loop-free approximation + + // this might be redundant, but I didn't find a better place to get this information. + private Dictionary m_LastReachVarIncarnation = new Dictionary(); + + private void Transform4DoomedCheck(Implementation impl) + { + variable2SequenceNumber = new Dictionary(); + incarnationOriginMap = new Dictionary(); + if (impl.Blocks.Count < 1) return; + + impl.PruneUnreachableBlocks(); + AddBlocksBetween(impl.Blocks); + ResetPredecessors(impl.Blocks); + + GraphAnalyzer ga = new GraphAnalyzer(impl.Blocks); + LoopRemover lr = new LoopRemover(ga); + lr.AbstractLoopUnrolling(); + + impl.Blocks = ga.ToImplementation(out m_UncheckableBlocks); + ResetPredecessors(impl.Blocks); + + // Check for the "BlocksBetween" if all their successors are in m_UncheckableBlocks + List oldblocks = new List(); + oldblocks.AddRange(impl.Blocks); + GenerateHelperBlocks(impl); + #region Check for the "BlocksBetween" if all their successors are in m_UncheckableBlocks + foreach (Block b in impl.Blocks) + { + if (oldblocks.Contains(b)) continue; + GotoCmd gc = b.TransferCmd as GotoCmd; + if (gc != null) + { + bool allsuccUncheckable = true; + foreach (Block _b in gc.labelTargets) + { + if (!m_UncheckableBlocks.Contains(_b)) + { + allsuccUncheckable = false; break; + } + } + if (allsuccUncheckable && !m_UncheckableBlocks.Contains(b)) m_UncheckableBlocks.Add(b); + } + } + #endregion + + impl.Blocks = DeepCopyBlocks(impl.Blocks, m_UncheckableBlocks); + + m_BlockReachabilityMap = new Dictionary(); + List cs = GenerateReachabilityPredicates(impl); + + //foreach (Block test in getTheFFinalBlock(impl.Blocks[0])) + //{ + // test.Cmds.AddRange(cs); + //} + + ResetPredecessors(impl.Blocks); + //EmitImpl(impl,false); + + Dictionary var2Expr = PassifyProgram(impl, new ModelViewInfo(program, impl)); + + // Collect the last incarnation of each reachability variable in the passive program + foreach (KeyValuePair kvp in m_BlockReachabilityMap) + { + if (var2Expr.ContainsKey(kvp.Value)) + { + m_LastReachVarIncarnation[kvp.Value] = (Expr)var2Expr[kvp.Value]; + } + } + } + + + List getTheFFinalBlock(Block b) + { + List lb = new List(); + GotoCmd gc = b.TransferCmd as GotoCmd; + if (gc == null) lb.Add(b); + else + { + foreach (Block s in gc.labelTargets) + { + foreach (Block r in getTheFFinalBlock(s)) if (!lb.Contains(r)) lb.Add(r); + } + } + return lb; + } + + + private List DeepCopyBlocks(List lb, List uncheckables) + { + List clones = new List(); + List uncheck_ = new List(); + Dictionary clonemap = new Dictionary(); + + foreach (Block b in lb) + { + Block clone = CloneBlock(b); + clones.Add(clone); + clonemap[b] = clone; + if (uncheckables.Contains(b)) uncheck_.Add(clone); + } + uncheckables.Clear(); + uncheckables.AddRange(uncheck_); + // update the successors and predecessors + foreach (Block b in lb) + { + List newpreds = new List(); + foreach (Block b_ in b.Predecessors) + { + newpreds.Add(clonemap[b_]); + } + clonemap[b].Predecessors = newpreds; + GotoCmd gc = b.TransferCmd as GotoCmd; + ReturnCmd rc = b.TransferCmd as ReturnCmd; + if (gc != null) + { + List lseq = new List(); + List bseq = new List(); + foreach (string s in gc.labelNames) lseq.Add(s); + foreach (Block b_ in gc.labelTargets) bseq.Add(clonemap[b_]); + GotoCmd tcmd = new GotoCmd(gc.tok, lseq, bseq); + clonemap[b].TransferCmd = tcmd; + } + else if (rc != null) + { + clonemap[b].TransferCmd = new ReturnCmd(rc.tok); + } + } + return clones; + } + + private Block CloneBlock(Block b) + { + Block clone = new Block(b.tok, b.Label, b.Cmds, b.TransferCmd); + if (this.exitBlock == b) this.exitBlock = clone; + return clone; + } + #endregion + } +} -- cgit v1.2.3