From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: Normalise line endings using a .gitattributes file. Unfortunately this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. --- Source/Doomed/DoomCheck.cs | 814 ++++++++--------- Source/Doomed/DoomErrorHandler.cs | 170 ++-- Source/Doomed/Doomed.csproj | 378 ++++---- Source/Doomed/DoomedLoopUnrolling.cs | 1298 +++++++++++++------------- Source/Doomed/DoomedStrategy.cs | 1054 +++++++++++----------- Source/Doomed/HasseDiagram.cs | 846 ++++++++--------- Source/Doomed/VCDoomed.cs | 1652 +++++++++++++++++----------------- 7 files changed, 3106 insertions(+), 3106 deletions(-) (limited to 'Source/Doomed') diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs index 83de03ff..c1d6736f 100644 --- a/Source/Doomed/DoomCheck.cs +++ b/Source/Doomed/DoomCheck.cs @@ -1,407 +1,407 @@ -//----------------------------------------------------------------------------- -// -// 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 -{ - internal class Evc { - - public DoomErrorHandler ErrorHandler { - set { - m_ErrorHandler = value; - } - } - - [ContractInvariantMethod] -void ObjectInvariant() -{ - Contract.Invariant(m_Checker!=null); -} - - private Checker m_Checker; - private DoomErrorHandler m_ErrorHandler; - - [NotDelayed] - public Evc(Checker check) { - Contract.Requires(check != null); - m_Checker = check; - - } - - public void Initialize(VCExpr evc) { - Contract.Requires(evc != null); - m_Checker.PushVCExpr(evc); - } - - - public bool CheckReachvar(List lv,Dictionary finalreachvars, - int k, int l, bool usenew , out ProverInterface.Outcome outcome) { - Contract.Requires(lv != null); - - VCExpr vc = VCExpressionGenerator.False; - if (usenew ) - { - foreach (Variable v in lv) - { - - vc = m_Checker.VCExprGen.Or( - m_Checker.VCExprGen.Neq( - m_Checker.VCExprGen.Integer(BigNum.ZERO), - m_Checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(v)), - vc); - } - //Console.WriteLine("TPQuery k={0}, l={1}, |Sp|={2}", k, l, finalreachvars.Count); - - VCExpr vc21 = m_Checker.VCExprGen.Integer(BigNum.ZERO); // Ask: is the necessary or can we use the same instance term in two inequalities? - VCExpr vc22 = m_Checker.VCExprGen.Integer(BigNum.ZERO); - - foreach (KeyValuePair kvp in finalreachvars) - { - - vc21 = m_Checker.VCExprGen.Add(vc21, m_Checker.TheoremProver.Context.BoogieExprTranslator.Translate(kvp.Key)); - vc22 = m_Checker.VCExprGen.Add(vc22, m_Checker.TheoremProver.Context.BoogieExprTranslator.Translate(kvp.Key)); - } - - VCExpr post = m_Checker.VCExprGen.Gt(m_Checker.VCExprGen.Integer(BigNum.FromInt(l)), vc21); - - if (k != -1) - { - post = m_Checker.VCExprGen.Or( - post, m_Checker.VCExprGen.Gt(vc22, m_Checker.VCExprGen.Integer(BigNum.FromInt(k))) - ); - } - vc = (m_Checker.VCExprGen.Or(vc, (post) )); - - } - else - { - - foreach (Variable v in lv) - { - - vc = m_Checker.VCExprGen.Or( - m_Checker.VCExprGen.Eq( - m_Checker.VCExprGen.Integer(BigNum.ONE), - m_Checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(v)), - vc); - } - Contract.Assert(vc != null); - - // Add the desired outcome of the reachability variables - foreach (KeyValuePair kvp in finalreachvars) - { - vc = m_Checker.VCExprGen.Or( - m_Checker.VCExprGen.Neq( - m_Checker.VCExprGen.Integer(BigNum.FromInt(kvp.Value)), - m_Checker.TheoremProver.Context.BoogieExprTranslator.Translate(kvp.Key)), - vc); - } - - } - - // Todo: Check if vc is trivial true or false - outcome = ProverInterface.Outcome.Undetermined; - Contract.Assert(m_ErrorHandler != null); - try - { - m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler); - m_Checker.ProverTask.Wait(); - outcome = m_Checker.ReadOutcome(); - } - catch (UnexpectedProverOutputException e) - { - if (CommandLineOptions.Clo.TraceVerify) - { - Console.WriteLine("Prover is unable to check {0}! Reason:", lv[0].Name); - Console.WriteLine(e.ToString()); - } - return false; - } - finally - { - m_Checker.GoBackToIdle(); - } - return true; - } - } - - internal class DoomCheck { - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(Label2Absy!=null); - Contract.Invariant(m_Check != null); - Contract.Invariant(m_Evc != null); - Contract.Invariant(m_Order != null); - } - - #region Attributes - public Dictionary Label2Absy; - public DoomErrorHandler ErrorHandler { - set { - m_ErrHandler = value; - m_Evc.ErrorHandler = value; - } - - get { - return m_ErrHandler; - } - } - - private DoomErrorHandler m_ErrHandler; - private Checker m_Check; - private DoomDetectionStrategy m_Order; - private Evc m_Evc; - #endregion - - public void __DEBUG_PrintStatistics() - { - Console.WriteLine("Checked/Total: Bl {0} / {1} EQ {2} / {3} {4} Tr {5} {6} / {7}", m_Order.__DEBUG_BlocksChecked, m_Order.__DEBUG_BlocksTotal, m_Order.__DEBUG_EQCChecked, m_Order.__DEBUG_EQCTotal, m_Order.__DEBUG_EQCLeaf, m_Order.__DEBUG_TracesChecked, m_Order.__DEBUG_InfeasibleTraces, m_Order.__DEBUG_TracesTotal); - } - - [NotDelayed] - public DoomCheck (Implementation passive_impl, Block unifiedExit, Checker check, List uncheckable, out int assertionCount) { - Contract.Requires(passive_impl != null); - Contract.Requires(check != null); - Contract.Requires(uncheckable != null); - m_Check = check; - - int replaceThisByCmdLineOption = CommandLineOptions.Clo.DoomStrategy ; - if (CommandLineOptions.Clo.DoomStrategy!=-1) Console.Write("Running experiments using {0} /", replaceThisByCmdLineOption); - switch (replaceThisByCmdLineOption) - { - default: - { - if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("Path Cover specialK Strategy"); - m_Order = new PathCoverStrategyK(passive_impl, unifiedExit, uncheckable); - break; - } - case 1: - { - if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("Path Cover L Strategy"); - m_Order = new PathCoverStrategy(passive_impl, unifiedExit, uncheckable); - break; - } - case 2: - { - if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("hasse strategy"); - m_Order = new HierachyStrategy(passive_impl, unifiedExit, uncheckable); - - break; - } - case 3: - { - if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("hasse+ce strategy"); - m_Order = new HierachyCEStrategy(passive_impl, unifiedExit, uncheckable); - break; - } - case 4: - { - if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("no strategy"); - m_Order = new NoStrategy(passive_impl, unifiedExit, uncheckable); - break; - } - - } - - Label2Absy = new Dictionary(); // This is only a dummy - m_Evc = new Evc(check); - Dictionary l2a = null; - VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount); - Contract.Assert(vce != null); - Contract.Assert( l2a!=null); - Label2Absy = l2a; - - m_Evc.Initialize(vce); - } - - - public void RespawnChecker(Implementation passive_impl, Checker check) - { - Contract.Requires(check != null); - m_Check = check; - Label2Absy = new Dictionary(); // This is only a dummy - m_Evc = new Evc(check); - Dictionary l2a = null; - int assertionCount; // compute and then ignore - VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount); - Contract.Assert(vce != null); - Contract.Assert(l2a != null); - Label2Absy = l2a; - - m_Evc.Initialize(vce); - } - - /* - Set b to the next block that needs to be checked. - - Returns false and set b to null if all blocks are checked. - - Has to be alternated with CheckLabel; might crash otherwise - */ - public bool GetNextBlock(out List lb) - { - return m_Order.GetNextBlock(out lb); - } - - public Stopwatch DEBUG_ProverTime = new Stopwatch(); - - /* - Checking a label means to ask the prover if |= ( rvar=false -> vc ) holds. - - outcome is set to Outcome.Invalid if the Block denoted by reachvar is doomed. - - returns false if the theorem prover throws an exception, otherwise true. - */ - public bool CheckLabel(List lv,Dictionary finalreachvars, out ProverInterface.Outcome outcome) { - Contract.Requires(lv != null); - outcome = ProverInterface.Outcome.Undetermined; - DEBUG_ProverTime.Reset(); - DEBUG_ProverTime.Start(); - if (m_Evc.CheckReachvar(lv,finalreachvars,m_Order.MaxBlocks,m_Order.MinBlocks,m_Order.HACK_NewCheck, out outcome) ) { - DEBUG_ProverTime.Stop(); - if (!m_Order.SetCurrentResult(lv, outcome, m_ErrHandler)) { - outcome = ProverInterface.Outcome.Undetermined; - } - return true; - } else { - DEBUG_ProverTime.Stop(); - Console.WriteLine(outcome); - m_Order.SetCurrentResult(lv, ProverInterface.Outcome.Undetermined, m_ErrHandler); - return false; - } - } - - public List!>!*/>> DoomedSequences { - get { - Contract.Ensures(Contract.ForAll(Contract.Result>>(), i=> cce.NonNullElements(i))); - - return m_Order.DetectedBlock; - } - } - - - #region Error Verification Condition Generation - /* - #region _TESTING_NEW_STUFF_ - CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Block; - //VCExpr wp = Wlp.Block(block, SuccCorrect, context); // Computes wp.S.true - - CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Doomed; - #endregion - - */ - - VCExpr GenerateEVC(Implementation impl, out Dictionary label2absy, Checker ch, out int assertionCount) { - Contract.Requires(impl != null); - Contract.Requires(ch != null); - Contract.Ensures(Contract.Result() != null); - - TypecheckingContext tc = new TypecheckingContext(null); - impl.Typecheck(tc); - label2absy = new Dictionary(); - VCExpr vc; - switch (CommandLineOptions.Clo.vcVariety) { - case CommandLineOptions.VCVariety.Doomed: - vc = LetVC(cce.NonNull(impl.Blocks[0]), label2absy, ch.TheoremProver.Context, out assertionCount); - break; - - default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected enumeration value - } - return vc; - } - - public VCExpr LetVC(Block startBlock, - Dictionary label2absy, - ProverContext proverCtxt, - out int assertionCount) - { - Contract.Requires(startBlock != null); - Contract.Requires(label2absy != null); - Contract.Requires(proverCtxt != null); - Contract.Ensures(Contract.Result() != null); - - Hashtable/**/ blockVariables = new Hashtable/**/(); - List bindings = new List(); - VCExpr startCorrect = LetVC(startBlock, label2absy, blockVariables, bindings, proverCtxt, out assertionCount); - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { - return proverCtxt.ExprGen.Let(bindings, proverCtxt.ExprGen.Not(startCorrect) ); - } else { - return proverCtxt.ExprGen.Let(bindings, startCorrect ); - } - } - - VCExpr LetVC(Block block, - Dictionary label2absy, - Hashtable/**/ blockVariables, - List bindings, - ProverContext proverCtxt, - out int assertionCount) - { - Contract.Requires(label2absy != null); - Contract.Requires(blockVariables != null); - Contract.Requires(proverCtxt != null); - Contract.Requires(cce.NonNullElements(bindings)); - Contract.Ensures(Contract.Result() != null); - - assertionCount = 0; - VCExpressionGenerator gen = proverCtxt.ExprGen; - Contract.Assert(gen != null); - VCExprVar v = (VCExprVar)blockVariables[block]; - if (v == null) { - /* - * For block A (= block), generate: - * LET_binding A_correct = wp(A_body, (/\ S \in Successors(A) :: S_correct)) - * with the side effect of adding the let bindings to "bindings" for any - * successor not yet visited. - */ - VCExpr SuccCorrect; - GotoCmd gotocmd = block.TransferCmd as GotoCmd; - if (gotocmd == null) { - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { - SuccCorrect = VCExpressionGenerator.False; - } else { - SuccCorrect = VCExpressionGenerator.True; - } - } else { - Contract.Assert( gotocmd.labelTargets != null); - List SuccCorrectVars = new List(gotocmd.labelTargets.Count); - foreach (Block successor in gotocmd.labelTargets) { - Contract.Assert(successor != null); - int ac; - VCExpr s = LetVC(successor, label2absy, blockVariables, bindings, proverCtxt, out ac); - assertionCount += ac; - SuccCorrectVars.Add(s); - } - SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars); - } - - VCContext context = new VCContext(label2absy, proverCtxt); - // m_Context = context; - - VCExpr vc = Wlp.Block(block, SuccCorrect, context); - assertionCount += context.AssertionCount; - v = gen.Variable(block.Label + "_correct", Microsoft.Boogie.Type.Bool); - - bindings.Add(gen.LetBinding(v, vc)); - blockVariables.Add(block, v); - } - return v; - } - - - #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 +{ + internal class Evc { + + public DoomErrorHandler ErrorHandler { + set { + m_ErrorHandler = value; + } + } + + [ContractInvariantMethod] +void ObjectInvariant() +{ + Contract.Invariant(m_Checker!=null); +} + + private Checker m_Checker; + private DoomErrorHandler m_ErrorHandler; + + [NotDelayed] + public Evc(Checker check) { + Contract.Requires(check != null); + m_Checker = check; + + } + + public void Initialize(VCExpr evc) { + Contract.Requires(evc != null); + m_Checker.PushVCExpr(evc); + } + + + public bool CheckReachvar(List lv,Dictionary finalreachvars, + int k, int l, bool usenew , out ProverInterface.Outcome outcome) { + Contract.Requires(lv != null); + + VCExpr vc = VCExpressionGenerator.False; + if (usenew ) + { + foreach (Variable v in lv) + { + + vc = m_Checker.VCExprGen.Or( + m_Checker.VCExprGen.Neq( + m_Checker.VCExprGen.Integer(BigNum.ZERO), + m_Checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(v)), + vc); + } + //Console.WriteLine("TPQuery k={0}, l={1}, |Sp|={2}", k, l, finalreachvars.Count); + + VCExpr vc21 = m_Checker.VCExprGen.Integer(BigNum.ZERO); // Ask: is the necessary or can we use the same instance term in two inequalities? + VCExpr vc22 = m_Checker.VCExprGen.Integer(BigNum.ZERO); + + foreach (KeyValuePair kvp in finalreachvars) + { + + vc21 = m_Checker.VCExprGen.Add(vc21, m_Checker.TheoremProver.Context.BoogieExprTranslator.Translate(kvp.Key)); + vc22 = m_Checker.VCExprGen.Add(vc22, m_Checker.TheoremProver.Context.BoogieExprTranslator.Translate(kvp.Key)); + } + + VCExpr post = m_Checker.VCExprGen.Gt(m_Checker.VCExprGen.Integer(BigNum.FromInt(l)), vc21); + + if (k != -1) + { + post = m_Checker.VCExprGen.Or( + post, m_Checker.VCExprGen.Gt(vc22, m_Checker.VCExprGen.Integer(BigNum.FromInt(k))) + ); + } + vc = (m_Checker.VCExprGen.Or(vc, (post) )); + + } + else + { + + foreach (Variable v in lv) + { + + vc = m_Checker.VCExprGen.Or( + m_Checker.VCExprGen.Eq( + m_Checker.VCExprGen.Integer(BigNum.ONE), + m_Checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(v)), + vc); + } + Contract.Assert(vc != null); + + // Add the desired outcome of the reachability variables + foreach (KeyValuePair kvp in finalreachvars) + { + vc = m_Checker.VCExprGen.Or( + m_Checker.VCExprGen.Neq( + m_Checker.VCExprGen.Integer(BigNum.FromInt(kvp.Value)), + m_Checker.TheoremProver.Context.BoogieExprTranslator.Translate(kvp.Key)), + vc); + } + + } + + // Todo: Check if vc is trivial true or false + outcome = ProverInterface.Outcome.Undetermined; + Contract.Assert(m_ErrorHandler != null); + try + { + m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler); + m_Checker.ProverTask.Wait(); + outcome = m_Checker.ReadOutcome(); + } + catch (UnexpectedProverOutputException e) + { + if (CommandLineOptions.Clo.TraceVerify) + { + Console.WriteLine("Prover is unable to check {0}! Reason:", lv[0].Name); + Console.WriteLine(e.ToString()); + } + return false; + } + finally + { + m_Checker.GoBackToIdle(); + } + return true; + } + } + + internal class DoomCheck { + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(Label2Absy!=null); + Contract.Invariant(m_Check != null); + Contract.Invariant(m_Evc != null); + Contract.Invariant(m_Order != null); + } + + #region Attributes + public Dictionary Label2Absy; + public DoomErrorHandler ErrorHandler { + set { + m_ErrHandler = value; + m_Evc.ErrorHandler = value; + } + + get { + return m_ErrHandler; + } + } + + private DoomErrorHandler m_ErrHandler; + private Checker m_Check; + private DoomDetectionStrategy m_Order; + private Evc m_Evc; + #endregion + + public void __DEBUG_PrintStatistics() + { + Console.WriteLine("Checked/Total: Bl {0} / {1} EQ {2} / {3} {4} Tr {5} {6} / {7}", m_Order.__DEBUG_BlocksChecked, m_Order.__DEBUG_BlocksTotal, m_Order.__DEBUG_EQCChecked, m_Order.__DEBUG_EQCTotal, m_Order.__DEBUG_EQCLeaf, m_Order.__DEBUG_TracesChecked, m_Order.__DEBUG_InfeasibleTraces, m_Order.__DEBUG_TracesTotal); + } + + [NotDelayed] + public DoomCheck (Implementation passive_impl, Block unifiedExit, Checker check, List uncheckable, out int assertionCount) { + Contract.Requires(passive_impl != null); + Contract.Requires(check != null); + Contract.Requires(uncheckable != null); + m_Check = check; + + int replaceThisByCmdLineOption = CommandLineOptions.Clo.DoomStrategy ; + if (CommandLineOptions.Clo.DoomStrategy!=-1) Console.Write("Running experiments using {0} /", replaceThisByCmdLineOption); + switch (replaceThisByCmdLineOption) + { + default: + { + if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("Path Cover specialK Strategy"); + m_Order = new PathCoverStrategyK(passive_impl, unifiedExit, uncheckable); + break; + } + case 1: + { + if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("Path Cover L Strategy"); + m_Order = new PathCoverStrategy(passive_impl, unifiedExit, uncheckable); + break; + } + case 2: + { + if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("hasse strategy"); + m_Order = new HierachyStrategy(passive_impl, unifiedExit, uncheckable); + + break; + } + case 3: + { + if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("hasse+ce strategy"); + m_Order = new HierachyCEStrategy(passive_impl, unifiedExit, uncheckable); + break; + } + case 4: + { + if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("no strategy"); + m_Order = new NoStrategy(passive_impl, unifiedExit, uncheckable); + break; + } + + } + + Label2Absy = new Dictionary(); // This is only a dummy + m_Evc = new Evc(check); + Dictionary l2a = null; + VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount); + Contract.Assert(vce != null); + Contract.Assert( l2a!=null); + Label2Absy = l2a; + + m_Evc.Initialize(vce); + } + + + public void RespawnChecker(Implementation passive_impl, Checker check) + { + Contract.Requires(check != null); + m_Check = check; + Label2Absy = new Dictionary(); // This is only a dummy + m_Evc = new Evc(check); + Dictionary l2a = null; + int assertionCount; // compute and then ignore + VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount); + Contract.Assert(vce != null); + Contract.Assert(l2a != null); + Label2Absy = l2a; + + m_Evc.Initialize(vce); + } + + /* - Set b to the next block that needs to be checked. + - Returns false and set b to null if all blocks are checked. + - Has to be alternated with CheckLabel; might crash otherwise + */ + public bool GetNextBlock(out List lb) + { + return m_Order.GetNextBlock(out lb); + } + + public Stopwatch DEBUG_ProverTime = new Stopwatch(); + + /* - Checking a label means to ask the prover if |= ( rvar=false -> vc ) holds. + - outcome is set to Outcome.Invalid if the Block denoted by reachvar is doomed. + - returns false if the theorem prover throws an exception, otherwise true. + */ + public bool CheckLabel(List lv,Dictionary finalreachvars, out ProverInterface.Outcome outcome) { + Contract.Requires(lv != null); + outcome = ProverInterface.Outcome.Undetermined; + DEBUG_ProverTime.Reset(); + DEBUG_ProverTime.Start(); + if (m_Evc.CheckReachvar(lv,finalreachvars,m_Order.MaxBlocks,m_Order.MinBlocks,m_Order.HACK_NewCheck, out outcome) ) { + DEBUG_ProverTime.Stop(); + if (!m_Order.SetCurrentResult(lv, outcome, m_ErrHandler)) { + outcome = ProverInterface.Outcome.Undetermined; + } + return true; + } else { + DEBUG_ProverTime.Stop(); + Console.WriteLine(outcome); + m_Order.SetCurrentResult(lv, ProverInterface.Outcome.Undetermined, m_ErrHandler); + return false; + } + } + + public List!>!*/>> DoomedSequences { + get { + Contract.Ensures(Contract.ForAll(Contract.Result>>(), i=> cce.NonNullElements(i))); + + return m_Order.DetectedBlock; + } + } + + + #region Error Verification Condition Generation + /* + #region _TESTING_NEW_STUFF_ + CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Block; + //VCExpr wp = Wlp.Block(block, SuccCorrect, context); // Computes wp.S.true + + CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Doomed; + #endregion + + */ + + VCExpr GenerateEVC(Implementation impl, out Dictionary label2absy, Checker ch, out int assertionCount) { + Contract.Requires(impl != null); + Contract.Requires(ch != null); + Contract.Ensures(Contract.Result() != null); + + TypecheckingContext tc = new TypecheckingContext(null); + impl.Typecheck(tc); + label2absy = new Dictionary(); + VCExpr vc; + switch (CommandLineOptions.Clo.vcVariety) { + case CommandLineOptions.VCVariety.Doomed: + vc = LetVC(cce.NonNull(impl.Blocks[0]), label2absy, ch.TheoremProver.Context, out assertionCount); + break; + + default: + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected enumeration value + } + return vc; + } + + public VCExpr LetVC(Block startBlock, + Dictionary label2absy, + ProverContext proverCtxt, + out int assertionCount) + { + Contract.Requires(startBlock != null); + Contract.Requires(label2absy != null); + Contract.Requires(proverCtxt != null); + Contract.Ensures(Contract.Result() != null); + + Hashtable/**/ blockVariables = new Hashtable/**/(); + List bindings = new List(); + VCExpr startCorrect = LetVC(startBlock, label2absy, blockVariables, bindings, proverCtxt, out assertionCount); + if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { + return proverCtxt.ExprGen.Let(bindings, proverCtxt.ExprGen.Not(startCorrect) ); + } else { + return proverCtxt.ExprGen.Let(bindings, startCorrect ); + } + } + + VCExpr LetVC(Block block, + Dictionary label2absy, + Hashtable/**/ blockVariables, + List bindings, + ProverContext proverCtxt, + out int assertionCount) + { + Contract.Requires(label2absy != null); + Contract.Requires(blockVariables != null); + Contract.Requires(proverCtxt != null); + Contract.Requires(cce.NonNullElements(bindings)); + Contract.Ensures(Contract.Result() != null); + + assertionCount = 0; + VCExpressionGenerator gen = proverCtxt.ExprGen; + Contract.Assert(gen != null); + VCExprVar v = (VCExprVar)blockVariables[block]; + if (v == null) { + /* + * For block A (= block), generate: + * LET_binding A_correct = wp(A_body, (/\ S \in Successors(A) :: S_correct)) + * with the side effect of adding the let bindings to "bindings" for any + * successor not yet visited. + */ + VCExpr SuccCorrect; + GotoCmd gotocmd = block.TransferCmd as GotoCmd; + if (gotocmd == null) { + if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { + SuccCorrect = VCExpressionGenerator.False; + } else { + SuccCorrect = VCExpressionGenerator.True; + } + } else { + Contract.Assert( gotocmd.labelTargets != null); + List SuccCorrectVars = new List(gotocmd.labelTargets.Count); + foreach (Block successor in gotocmd.labelTargets) { + Contract.Assert(successor != null); + int ac; + VCExpr s = LetVC(successor, label2absy, blockVariables, bindings, proverCtxt, out ac); + assertionCount += ac; + SuccCorrectVars.Add(s); + } + SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars); + } + + VCContext context = new VCContext(label2absy, proverCtxt); + // m_Context = context; + + VCExpr vc = Wlp.Block(block, SuccCorrect, context); + assertionCount += context.AssertionCount; + v = gen.Variable(block.Label + "_correct", Microsoft.Boogie.Type.Bool); + + bindings.Add(gen.LetBinding(v, vc)); + blockVariables.Add(block, v); + } + return v; + } + + + #endregion + + } + +} diff --git a/Source/Doomed/DoomErrorHandler.cs b/Source/Doomed/DoomErrorHandler.cs index 8d89bae3..ce14ff73 100644 --- a/Source/Doomed/DoomErrorHandler.cs +++ b/Source/Doomed/DoomErrorHandler.cs @@ -1,86 +1,86 @@ -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 -{ - internal class DoomErrorHandler : ProverInterface.ErrorHandler - { - - protected Dictionary label2Absy; - protected VerifierCallback callback; - private List m_CurrentTrace = new List(); - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(label2Absy != null); - Contract.Invariant(callback != null); - Contract.Invariant(cce.NonNullElements(m_CurrentTrace)); - } - - - public DoomErrorHandler(Dictionary label2Absy, VerifierCallback callback) - { - Contract.Requires(label2Absy != null); - Contract.Requires(callback != null); - this.label2Absy = label2Absy; - this.callback = callback; - } - - public override Absy Label2Absy(string label) - { - //Contract.Requires(label != null); - Contract.Ensures(Contract.Result() != null); - - int id = int.Parse(label); - return cce.NonNull((Absy)label2Absy[id]); - } - - public override void OnProverWarning(string msg) - { - //Contract.Requires(msg != null); - this.callback.OnWarning(msg); - } - - - public List/*!>!*/ TraceNodes - { - get - { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - - return m_CurrentTrace; - } - } - - public override void OnModel(IList/*!>!*/ labels, Model model, ProverInterface.Outcome proverOutcome) - { - // TODO: it would be better to check which reachability variables are actually set to one! - List traceNodes = new List(); - List assertNodes = new List(); - foreach (string s in labels) - { - Contract.Assert(s != null); - Absy node = Label2Absy(s); - if (node is Block) - { - Block b = (Block)node; - traceNodes.Add(b); - //Console.Write("{0}, ", b.Label); - } - } - m_CurrentTrace.AddRange(traceNodes); - } - - } - +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 +{ + internal class DoomErrorHandler : ProverInterface.ErrorHandler + { + + protected Dictionary label2Absy; + protected VerifierCallback callback; + private List m_CurrentTrace = new List(); + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(label2Absy != null); + Contract.Invariant(callback != null); + Contract.Invariant(cce.NonNullElements(m_CurrentTrace)); + } + + + public DoomErrorHandler(Dictionary label2Absy, VerifierCallback callback) + { + Contract.Requires(label2Absy != null); + Contract.Requires(callback != null); + this.label2Absy = label2Absy; + this.callback = callback; + } + + public override Absy Label2Absy(string label) + { + //Contract.Requires(label != null); + Contract.Ensures(Contract.Result() != null); + + int id = int.Parse(label); + return cce.NonNull((Absy)label2Absy[id]); + } + + public override void OnProverWarning(string msg) + { + //Contract.Requires(msg != null); + this.callback.OnWarning(msg); + } + + + public List/*!>!*/ TraceNodes + { + get + { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + + return m_CurrentTrace; + } + } + + public override void OnModel(IList/*!>!*/ labels, Model model, ProverInterface.Outcome proverOutcome) + { + // TODO: it would be better to check which reachability variables are actually set to one! + List traceNodes = new List(); + List assertNodes = new List(); + foreach (string s in labels) + { + Contract.Assert(s != null); + Absy node = Label2Absy(s); + if (node is Block) + { + Block b = (Block)node; + traceNodes.Add(b); + //Console.Write("{0}, ", b.Label); + } + } + m_CurrentTrace.AddRange(traceNodes); + } + + } + } \ No newline at end of file diff --git a/Source/Doomed/Doomed.csproj b/Source/Doomed/Doomed.csproj index 77713080..c8fb83ad 100644 --- a/Source/Doomed/Doomed.csproj +++ b/Source/Doomed/Doomed.csproj @@ -1,190 +1,190 @@ - - - - - Debug - AnyCPU - {884386A3-58E9-40BB-A273-B24976775553} - Library - Properties - Doomed - Doomed - v4.0 - 512 - Client - 12.0.0 - 2.0 - 0 - - - true - full - false - bin\Debug\ - DEBUG;TRACE - prompt - 4 - False - False - True - False - False - False - True - True - True - True - True - True - True - True - False - True - False - True - False - False - False - False - True - False - True - True - True - False - False - - - - - - - - True - False - False - True - Full - DoNotBuild - 0 - - - pdbonly - true - bin\Release\ - TRACE - prompt - 4 - False - False - True - False - False - False - True - True - False - False - False - True - True - False - False - False - True - False - True - True - False - False - - - - - - - - True - False - Full - DoNotBuild - 0 - - - true - - - ..\InterimKey.snk - - - true - bin\QED\ - DEBUG;TRACE - full - AnyCPU - prompt - MinimumRecommendedRules.ruleset - - - - - - - - - - - - - - - - - - - - - {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} - Basetypes - - - {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} - CodeContractsExtender - - - {B230A69C-C466-4065-B9C1-84D80E76D802} - Core - - - {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} - Graph - - - {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83} - Model - - - {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} - ParserHelper - - - {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1} - VCExpr - - - {E1F10180-C7B9-4147-B51F-FA1B701966DC} - VCGeneration - - - - - - - + + + + + Debug + AnyCPU + {884386A3-58E9-40BB-A273-B24976775553} + Library + Properties + Doomed + Doomed + v4.0 + 512 + Client + 12.0.0 + 2.0 + 0 + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + False + False + True + False + False + False + True + True + True + True + True + True + True + True + False + True + False + True + False + False + False + False + True + False + True + True + True + False + False + + + + + + + + True + False + False + True + Full + DoNotBuild + 0 + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + False + False + True + False + False + False + True + True + False + False + False + True + True + False + False + False + True + False + True + True + False + False + + + + + + + + True + False + Full + DoNotBuild + 0 + + + true + + + ..\InterimKey.snk + + + true + bin\QED\ + DEBUG;TRACE + full + AnyCPU + prompt + MinimumRecommendedRules.ruleset + + + + + + + + + + + + + + + + + + + + + {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} + Basetypes + + + {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} + CodeContractsExtender + + + {B230A69C-C466-4065-B9C1-84D80E76D802} + Core + + + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} + Graph + + + {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83} + Model + + + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} + ParserHelper + + + {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1} + VCExpr + + + {E1F10180-C7B9-4147-B51F-FA1B701966DC} + VCGeneration + + + + + + + \ No newline at end of file diff --git a/Source/Doomed/DoomedLoopUnrolling.cs b/Source/Doomed/DoomedLoopUnrolling.cs index 38fa99ac..0905deed 100644 --- a/Source/Doomed/DoomedLoopUnrolling.cs +++ b/Source/Doomed/DoomedLoopUnrolling.cs @@ -1,650 +1,650 @@ -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 -{ - #region Loop handeling for doomed code detection - - #region Loop Remover - internal class LoopRemover - { - GraphAnalyzer m_GraphAnalyzer; - - public LoopRemover(GraphAnalyzer ga) - { - m_GraphAnalyzer = ga; - } - - private void m_RemoveBackEdge(Loop l) - { - // first remove the backedges of the nested loops - foreach (Loop c in l.NestedLoops) m_RemoveBackEdge(c); - //Debugger.Break(); - GraphNode loopSkip = null; - foreach (GraphNode gn in l.Cutpoint.Suc) - { - if (l.LoopExitNodes.Contains(gn)) - { - loopSkip = gn; break; - } - } - if (loopSkip == null) - { // We didn't find a loop exit node. There must be a bug - Debugger.Break(); - } - foreach (GraphNode gn in l.Cutpoint.LoopingPred) - { - List newsuc = new List(); - foreach (GraphNode s in gn.Suc) - { - if (s == l.Cutpoint) newsuc.Add(loopSkip); - else newsuc.Add(s); - } - gn.Suc = newsuc; - } - } - - private void m_AbstractLoop(Loop l) - { - foreach (Loop c in l.NestedLoops) m_AbstractLoop(c); - m_HavocLoopBody(l); - m_RemoveBackEdge(l); - } - - public void AbstractLoopUnrolling() - { - foreach (Loop l in m_GraphAnalyzer.Graphloops) - { - m_MarkLoopExitUncheckable(l); - m_AbstractLoopUnrolling(l,null, "",true); - } - } - - private void m_HavocLoopBody(Loop l) - { - List loopblocks = new List(); - foreach (GraphNode g in l.LoopNodes) loopblocks.Add(g.Label); - HavocCmd hcmd = m_ComputHavocCmd(loopblocks, l.Cutpoint.Label.tok); - - //Add Havoc before and after the loop body - foreach (GraphNode g in l.Cutpoint.Suc) // before - { - if (l.LoopNodes.Contains(g)) m_AddHavocCmdToFront(g.Label, hcmd); - } - foreach (GraphNode g in l.Cutpoint.Pre) // and after - { - if (l.LoopNodes.Contains(g)) m_AddHavocCmdToFront(g.Label, hcmd); - } - } - - private void m_AddHavocCmdToFront(Block b, HavocCmd hcmd) - { - List cs = new List(); - cs.Add(hcmd); cs.AddRange(b.Cmds); - b.Cmds = cs; - } - - private HavocCmd m_ComputHavocCmd(List bl, IToken tok) - { - Contract.Requires(bl != null); - Contract.Requires(tok != null); - Contract.Ensures(Contract.Result() != null); - - List varsToHavoc = new List(); - foreach (Block b in bl) - { - Contract.Assert(b != null); - foreach (Cmd c in b.Cmds) - { - Contract.Assert(c != null); - c.AddAssignedVariables(varsToHavoc); - } - } - List havocExprs = new List(); - foreach (Variable v in varsToHavoc) - { - Contract.Assert(v != null); - IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); - if (!havocExprs.Contains(ie)) - havocExprs.Add(ie); - } - // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct - // the source location for this later on - return new HavocCmd(tok, havocExprs); - } - - private void m_AbstractLoopUnrolling(Loop l, Loop parent, string prefix, bool unfold) - { - //Debugger.Break(); - if (unfold) - { - - Loop first = new Loop(l, m_GraphAnalyzer,prefix+"FI_"); - Loop last = new Loop(l, m_GraphAnalyzer,prefix+"LA_"); - Loop abs = new Loop(l, m_GraphAnalyzer, prefix + "AB_"); - foreach (Loop c in first.NestedLoops) m_AbstractLoopUnrolling(c, first, prefix + "FI_", false); - foreach (Loop c in last.NestedLoops) m_AbstractLoopUnrolling(c, last, prefix + "LA_", false); - foreach (Loop c in abs.NestedLoops) m_AbstractLoopUnrolling(c, abs, prefix + "AB_", true); - - //Debugger.Break(); - - if (parent != null) - { - foreach (GraphNode gn in l.LoopNodes) - { - if (parent.LoopNodes.Contains(gn)) parent.LoopNodes.Remove(gn); - } - foreach (GraphNode gn in abs.LoopNodes) - { - if (!parent.LoopNodes.Contains(gn)) parent.LoopNodes.Add(gn); - } - foreach (GraphNode gn in first.LoopNodes) - { - if (!parent.LoopNodes.Contains(gn)) parent.LoopNodes.Add(gn); - } - foreach (GraphNode gn in last.LoopNodes) - { - if (!parent.LoopNodes.Contains(gn)) parent.LoopNodes.Add(gn); - } - } - - m_HavocLoopBody(abs); - List backupPre = new List(); - backupPre.AddRange(l.Cutpoint.Pre); - foreach (GraphNode pre in backupPre) - { - if (!l.Cutpoint.LoopingPred.Contains(pre)) - { - pre.RemoveEdgeTo(l.Cutpoint); - pre.RemoveEdgeTo(abs.Cutpoint); - pre.AddEdgeTo(first.Cutpoint); - } - } - - m_RemoveRegularLoopExit(last); - m_RemoveRegularLoopExit(abs); - - m_ReplaceBackEdge(first, abs.Cutpoint); - m_ReplaceBackEdge(abs, last.Cutpoint); - foreach (GraphNode gn in first.Cutpoint.Suc) - { - if (!first.LoopNodes.Contains(gn)) - { - m_ReplaceBackEdge(last, gn); - break; - } - } - - // Remove all remaining connections to the original loop - foreach (GraphNode gn in l.LoopExitNodes) - { - List tmp = new List(); - tmp.AddRange(gn.Pre); - foreach (GraphNode g in tmp) - { - if (l.LoopNodes.Contains(g)) - { - //Debugger.Break(); - g.RemoveEdgeTo(gn); - } - } - } - foreach (GraphNode gn in l.LoopNodes) - { - m_GraphAnalyzer.DeleteGraphNode(gn); - } - foreach (GraphNode gn in first.LoopNodes) - { - if (gn != first.Cutpoint && !m_GraphAnalyzer.UncheckableNodes.Contains(gn) ) - m_GraphAnalyzer.UncheckableNodes.Add(gn); - } - foreach (GraphNode gn in last.LoopNodes) - { - if (gn != last.Cutpoint && !m_GraphAnalyzer.UncheckableNodes.Contains(gn)) - m_GraphAnalyzer.UncheckableNodes.Add(gn); - } - MakeLoopExitUncheckable(last.LoopExitNodes); - } - else - { - foreach (Loop c in l.NestedLoops) m_AbstractLoopUnrolling(c, l, prefix, false); - m_AbstractLoop(l); - //MakeLoopExitUncheckable(l.LoopExitNodes); - } - } - - // the loop exit has to be marked uncheckable because otherwise - // while(true) would report unreachable code. - private void m_MarkLoopExitUncheckable(Loop l) - { - - foreach (GraphNode g in l.Cutpoint.Suc) - { - if (!l.LoopNodes.Contains(g)) - { - foreach (GraphNode g_ in m_MarkLoopExitUncheckable(g, l)) - { - if (!m_GraphAnalyzer.UncheckableNodes.Contains(g_)) - m_GraphAnalyzer.UncheckableNodes.Add(g_); - } - } - } - } - - private List m_MarkLoopExitUncheckable(GraphNode g, Loop l) - { - List ret = new List(); - - if (g.Pre.Count > 1) return ret; - ret.Add(g); - foreach (GraphNode gn in g.Suc) - { - ret.AddRange(m_MarkLoopExitUncheckable(gn, l)); - } - - return ret; - } - - // to avoid problems with unreachable code after while(true) {}, try to make the loopexit nodes uncheckable. - private void MakeLoopExitUncheckable(List le) - { - foreach (GraphNode gn in le) - { - if (gn.Suc.Count==1) m_GraphAnalyzer.UncheckableNodes.Add(gn); - } - } - - private void m_RemoveRegularLoopExit(Loop l) - { - List lg = new List(); - lg.AddRange( l.Cutpoint.Suc ); - foreach (GraphNode gn in lg) - { - if (l.LoopExitNodes.Contains(gn)) - { - l.Cutpoint.RemoveEdgeTo(gn); - l.LoopExitNodes.Remove(gn); - } - } - } - - private void m_ReplaceBackEdge(Loop l, GraphNode loopSkip) - { - - foreach (GraphNode gn in l.Cutpoint.LoopingPred) - { - List newsuc = new List(); - foreach (GraphNode s in gn.Suc) - { - if (s == l.Cutpoint) newsuc.Add(loopSkip); - else newsuc.Add(s); - } - gn.Suc = newsuc; - } - } - - - } - #endregion - - #region Graph Analyzer - internal class GraphAnalyzer - { - public List UncheckableNodes = new List(); - - public Dictionary GraphMap = new Dictionary(); - - public List Graphloops = null; - - public GraphAnalyzer(List blocks) - { - //ExitBlock = dedicatedExitBlock; - if (blocks.Count < 1) return; - foreach (Block b in blocks) GraphMap[b] = new GraphNode(b); - foreach (Block b in blocks) - { - foreach (Block pre in b.Predecessors) GraphMap[b].Pre.Add(GraphMap[pre]); - GotoCmd gc = b.TransferCmd as GotoCmd; - if (gc != null) - { - foreach (Block suc in gc.labelTargets) GraphMap[b].Suc.Add(GraphMap[suc]); - } - } - - - m_DetectCutPoints(GraphMap[blocks[0]]); - - //m_DetectCutPoints(GraphMap[blocks[0]], null, new List()); - Graphloops = m_CollectLoops(GraphMap[blocks[0]], null); - - } - - public List ToImplementation(out List uncheckables) - { - List blocks = new List(); - uncheckables = new List(); - - foreach (KeyValuePair kvp in GraphMap) - { - Block b = kvp.Key; - if (UncheckableNodes.Contains(GraphMap[b])) uncheckables.Add(b); - blocks.Add(b); - b.Predecessors = new List(); - foreach (GraphNode p in kvp.Value.Pre) b.Predecessors.Add(p.Label); - if (kvp.Value.Suc.Count > 0) - { - List bs = new List(); - foreach (GraphNode s in kvp.Value.Suc) bs.Add(s.Label); - b.TransferCmd = new GotoCmd(b.tok, bs); - } - else - { - b.TransferCmd = new ReturnCmd(b.tok); - } - } - - return blocks; - } - - public GraphNode CloneGraphNode(GraphNode gn, string prefix) - { - List cmds = new List(gn.Label.Cmds); - - Block b = new Block(gn.Label.tok, prefix+gn.Label.Label, cmds, gn.Label.TransferCmd); - GraphNode clone = new GraphNode(b); - clone.IsCutpoint = gn.IsCutpoint; - clone.Suc.AddRange(gn.Suc); - clone.Pre.AddRange(gn.Pre); - clone.LoopingPred.AddRange(gn.LoopingPred); - GraphMap[b] = clone; - //if (gn.Label == ExitBlock) ExitBlock = b; - return clone; - } - - public void DeleteGraphNode(GraphNode gn) - { - List affected = new List(); - - foreach (KeyValuePair kvp in GraphMap) - { - if (kvp.Value == gn && !affected.Contains(kvp.Key)) affected.Add(kvp.Key); - } - foreach (Block b in affected) - { - GraphMap.Remove(b); - } - } -/* - private void m_DetectCutPoints(GraphNode gn, GraphNode pred, List visited ) - { - if (visited.Contains(gn) ) - { - if (pred != null && !gn.LoopingPred.Contains(pred)) gn.LoopingPred.Add(pred); - gn.IsCutpoint = true; - Console.WriteLine("Normal RootNode {0}", gn.Label.Label); - return; - } - else - { - List visited_ = new List(); - visited_.AddRange(visited); - visited_.Add(gn); - foreach (GraphNode next in gn.Suc) - { - m_DetectCutPoints(next,gn,visited_); - } - } - - } -*/ - - - private void m_DetectCutPoints(GraphNode gn) - { - List todo = new List(); - List done = new List(); - todo.Add(gn); - - GraphNode current = null; - todo[0].Index = 0; - - while (todo.Count > 0) - { - current = todo[0]; - todo.Remove(current); - - bool ready = true; - foreach (GraphNode p in current.Pre) - { - if (!done.Contains(p) ) - { - _loopbacktracking.Clear(); - if (!m_isLoop(current, p, todo, done)) - { - todo.Add(current); - ready = false; - break; - } - else - { - if (!current.LoopingPred.Contains(p)) current.LoopingPred.Add(p); - current.IsCutpoint = true; - } - } - } - if (!ready) continue; - done.Add(current); - foreach (GraphNode s in current.Suc) - { - if (!todo.Contains(s) && !done.Contains(s)) todo.Add(s); - } - } - - } - - List _loopbacktracking = new List(); - private bool m_isLoop(GraphNode loophead, GraphNode gn, List l1, List l2) - { - if (loophead == gn) return true; - if (l1.Contains(gn) || l2.Contains(gn) || _loopbacktracking.Contains(gn)) return false; - _loopbacktracking.Add(gn); - foreach (GraphNode p in gn.Pre) - { - if (m_isLoop(loophead, p, l1, l2)) return true; - } - return false; - } - - private List m_CollectLoops(GraphNode gn, Loop lastLoop) - { - List ret = new List(); - if (gn.Visited) return ret; - gn.Visited = true; - List loopingSucs = new List(); - if (gn.IsCutpoint) - { - Loop l = new Loop(gn); - if (lastLoop != null) - { - lastLoop.SucLoops.Add(l); - l.PreLoops.Add(lastLoop); - } - loopingSucs = l.LoopNodes; - lastLoop = l; - ret.Add(lastLoop); - } - foreach (GraphNode suc in gn.Suc) - { - if (!loopingSucs.Contains(suc)) ret.AddRange(m_CollectLoops(suc, lastLoop)); - } - //Debugger.Break(); - return ret; - } - } - #endregion - - #region GraphNodeStructure - internal class GraphNode - { - public int Index = -1; // Used for scc detection - public int LowLink = -1; // Used for scc detection - - public GraphNode(Block b) - { - Label = b; IsCutpoint = false; - } - public Block Label; - public List Pre = new List(); - public List Suc = new List(); - public bool IsCutpoint; - public bool Visited = false; - public List LoopingPred = new List(); - - public void AddEdgeTo(GraphNode other) - { - if (!this.Suc.Contains(other)) this.Suc.Add(other); - if (!other.Pre.Contains(this)) other.Pre.Add(this); - } - - public void RemoveEdgeTo(GraphNode other) - { - if (this.Suc.Contains(other)) this.Suc.Remove(other); - if (other.Pre.Contains(this)) other.Pre.Remove(this); - } - - } - #endregion - - #region LoopStructure - internal class Loop - { - public Loop(GraphNode cutpoint) - { - if (!cutpoint.IsCutpoint) - { - Debugger.Break(); - } - Cutpoint = cutpoint; - LoopNodes.Add(Cutpoint); - foreach (GraphNode gn in Cutpoint.LoopingPred) - { - CollectLoopBody(gn); - } - CollectLoopExitNodes(); - } - - // Copy Constructor - public Loop(Loop l, GraphAnalyzer ga, string prefix) - { - - Dictionary clonemap = new Dictionary(); - GraphNode clonecutpoint = null; - foreach (GraphNode gn in l.LoopNodes) - { - clonemap[gn] = ga.CloneGraphNode(gn, prefix); - if (gn == l.Cutpoint) clonecutpoint = clonemap[gn]; - } - - if (clonecutpoint == null) - { - Debugger.Break(); - return; - } - // Replace the pre and post nodes by the corresponding clone - foreach (GraphNode gn in l.LoopNodes) - { - List newl = new List(); - foreach (GraphNode g in clonemap[gn].Pre) - { - if (clonemap.ContainsKey(g)) newl.Add(clonemap[g]); - else newl.Add(g); - } - clonemap[gn].Pre = newl; - newl = new List(); - foreach (GraphNode g in clonemap[gn].Suc) - { - if (clonemap.ContainsKey(g)) newl.Add(clonemap[g]); - else newl.Add(g); - } - clonemap[gn].Suc = newl; - newl = new List(); - foreach (GraphNode g in clonemap[gn].LoopingPred) - { - if (clonemap.ContainsKey(g)) newl.Add(clonemap[g]); - else newl.Add(g); - } - clonemap[gn].LoopingPred = newl; - } - - foreach (GraphNode gn in l.Cutpoint.LoopingPred) - { - clonecutpoint.LoopingPred.Remove(gn); - clonecutpoint.LoopingPred.Add(clonemap[gn]); - } - - - - SucLoops.AddRange(l.SucLoops); - PreLoops.AddRange(l.PreLoops); - Cutpoint = clonecutpoint; - LoopNodes.Add(Cutpoint); - foreach (GraphNode gn in Cutpoint.LoopingPred) - { - CollectLoopBody(gn); - } - CollectLoopExitNodes(); - } - - private void CollectLoopBody(GraphNode gn) - { - if (gn == Cutpoint) return; - if (!LoopNodes.Contains(gn)) - { - if (gn.IsCutpoint) // nested loop found - { - Loop lo = new Loop(gn); - foreach (GraphNode lgn in lo.LoopNodes) - { - if (!LoopNodes.Contains(lgn)) LoopNodes.Add(lgn); - } - NestedLoops.Add(lo); - } - else - { - LoopNodes.Add(gn); - } - foreach (GraphNode pre in gn.Pre) if (!gn.LoopingPred.Contains(pre)) CollectLoopBody(pre); - } - } - - private void CollectLoopExitNodes() - { - foreach (GraphNode gn in LoopNodes) - { - foreach (GraphNode gn_ in gn.Suc) - { - if (!LoopNodes.Contains(gn_) && !LoopExitNodes.Contains(gn_)) LoopExitNodes.Add(gn_); - } - } - } - - public GraphNode Cutpoint; - public List LoopExitNodes = new List(); - public List NestedLoops = new List(); - public List SucLoops = new List(); - public List PreLoops = new List(); - public List LoopNodes = new List(); - } - #endregion - - #endregion +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 +{ + #region Loop handeling for doomed code detection + + #region Loop Remover + internal class LoopRemover + { + GraphAnalyzer m_GraphAnalyzer; + + public LoopRemover(GraphAnalyzer ga) + { + m_GraphAnalyzer = ga; + } + + private void m_RemoveBackEdge(Loop l) + { + // first remove the backedges of the nested loops + foreach (Loop c in l.NestedLoops) m_RemoveBackEdge(c); + //Debugger.Break(); + GraphNode loopSkip = null; + foreach (GraphNode gn in l.Cutpoint.Suc) + { + if (l.LoopExitNodes.Contains(gn)) + { + loopSkip = gn; break; + } + } + if (loopSkip == null) + { // We didn't find a loop exit node. There must be a bug + Debugger.Break(); + } + foreach (GraphNode gn in l.Cutpoint.LoopingPred) + { + List newsuc = new List(); + foreach (GraphNode s in gn.Suc) + { + if (s == l.Cutpoint) newsuc.Add(loopSkip); + else newsuc.Add(s); + } + gn.Suc = newsuc; + } + } + + private void m_AbstractLoop(Loop l) + { + foreach (Loop c in l.NestedLoops) m_AbstractLoop(c); + m_HavocLoopBody(l); + m_RemoveBackEdge(l); + } + + public void AbstractLoopUnrolling() + { + foreach (Loop l in m_GraphAnalyzer.Graphloops) + { + m_MarkLoopExitUncheckable(l); + m_AbstractLoopUnrolling(l,null, "",true); + } + } + + private void m_HavocLoopBody(Loop l) + { + List loopblocks = new List(); + foreach (GraphNode g in l.LoopNodes) loopblocks.Add(g.Label); + HavocCmd hcmd = m_ComputHavocCmd(loopblocks, l.Cutpoint.Label.tok); + + //Add Havoc before and after the loop body + foreach (GraphNode g in l.Cutpoint.Suc) // before + { + if (l.LoopNodes.Contains(g)) m_AddHavocCmdToFront(g.Label, hcmd); + } + foreach (GraphNode g in l.Cutpoint.Pre) // and after + { + if (l.LoopNodes.Contains(g)) m_AddHavocCmdToFront(g.Label, hcmd); + } + } + + private void m_AddHavocCmdToFront(Block b, HavocCmd hcmd) + { + List cs = new List(); + cs.Add(hcmd); cs.AddRange(b.Cmds); + b.Cmds = cs; + } + + private HavocCmd m_ComputHavocCmd(List bl, IToken tok) + { + Contract.Requires(bl != null); + Contract.Requires(tok != null); + Contract.Ensures(Contract.Result() != null); + + List varsToHavoc = new List(); + foreach (Block b in bl) + { + Contract.Assert(b != null); + foreach (Cmd c in b.Cmds) + { + Contract.Assert(c != null); + c.AddAssignedVariables(varsToHavoc); + } + } + List havocExprs = new List(); + foreach (Variable v in varsToHavoc) + { + Contract.Assert(v != null); + IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); + if (!havocExprs.Contains(ie)) + havocExprs.Add(ie); + } + // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct + // the source location for this later on + return new HavocCmd(tok, havocExprs); + } + + private void m_AbstractLoopUnrolling(Loop l, Loop parent, string prefix, bool unfold) + { + //Debugger.Break(); + if (unfold) + { + + Loop first = new Loop(l, m_GraphAnalyzer,prefix+"FI_"); + Loop last = new Loop(l, m_GraphAnalyzer,prefix+"LA_"); + Loop abs = new Loop(l, m_GraphAnalyzer, prefix + "AB_"); + foreach (Loop c in first.NestedLoops) m_AbstractLoopUnrolling(c, first, prefix + "FI_", false); + foreach (Loop c in last.NestedLoops) m_AbstractLoopUnrolling(c, last, prefix + "LA_", false); + foreach (Loop c in abs.NestedLoops) m_AbstractLoopUnrolling(c, abs, prefix + "AB_", true); + + //Debugger.Break(); + + if (parent != null) + { + foreach (GraphNode gn in l.LoopNodes) + { + if (parent.LoopNodes.Contains(gn)) parent.LoopNodes.Remove(gn); + } + foreach (GraphNode gn in abs.LoopNodes) + { + if (!parent.LoopNodes.Contains(gn)) parent.LoopNodes.Add(gn); + } + foreach (GraphNode gn in first.LoopNodes) + { + if (!parent.LoopNodes.Contains(gn)) parent.LoopNodes.Add(gn); + } + foreach (GraphNode gn in last.LoopNodes) + { + if (!parent.LoopNodes.Contains(gn)) parent.LoopNodes.Add(gn); + } + } + + m_HavocLoopBody(abs); + List backupPre = new List(); + backupPre.AddRange(l.Cutpoint.Pre); + foreach (GraphNode pre in backupPre) + { + if (!l.Cutpoint.LoopingPred.Contains(pre)) + { + pre.RemoveEdgeTo(l.Cutpoint); + pre.RemoveEdgeTo(abs.Cutpoint); + pre.AddEdgeTo(first.Cutpoint); + } + } + + m_RemoveRegularLoopExit(last); + m_RemoveRegularLoopExit(abs); + + m_ReplaceBackEdge(first, abs.Cutpoint); + m_ReplaceBackEdge(abs, last.Cutpoint); + foreach (GraphNode gn in first.Cutpoint.Suc) + { + if (!first.LoopNodes.Contains(gn)) + { + m_ReplaceBackEdge(last, gn); + break; + } + } + + // Remove all remaining connections to the original loop + foreach (GraphNode gn in l.LoopExitNodes) + { + List tmp = new List(); + tmp.AddRange(gn.Pre); + foreach (GraphNode g in tmp) + { + if (l.LoopNodes.Contains(g)) + { + //Debugger.Break(); + g.RemoveEdgeTo(gn); + } + } + } + foreach (GraphNode gn in l.LoopNodes) + { + m_GraphAnalyzer.DeleteGraphNode(gn); + } + foreach (GraphNode gn in first.LoopNodes) + { + if (gn != first.Cutpoint && !m_GraphAnalyzer.UncheckableNodes.Contains(gn) ) + m_GraphAnalyzer.UncheckableNodes.Add(gn); + } + foreach (GraphNode gn in last.LoopNodes) + { + if (gn != last.Cutpoint && !m_GraphAnalyzer.UncheckableNodes.Contains(gn)) + m_GraphAnalyzer.UncheckableNodes.Add(gn); + } + MakeLoopExitUncheckable(last.LoopExitNodes); + } + else + { + foreach (Loop c in l.NestedLoops) m_AbstractLoopUnrolling(c, l, prefix, false); + m_AbstractLoop(l); + //MakeLoopExitUncheckable(l.LoopExitNodes); + } + } + + // the loop exit has to be marked uncheckable because otherwise + // while(true) would report unreachable code. + private void m_MarkLoopExitUncheckable(Loop l) + { + + foreach (GraphNode g in l.Cutpoint.Suc) + { + if (!l.LoopNodes.Contains(g)) + { + foreach (GraphNode g_ in m_MarkLoopExitUncheckable(g, l)) + { + if (!m_GraphAnalyzer.UncheckableNodes.Contains(g_)) + m_GraphAnalyzer.UncheckableNodes.Add(g_); + } + } + } + } + + private List m_MarkLoopExitUncheckable(GraphNode g, Loop l) + { + List ret = new List(); + + if (g.Pre.Count > 1) return ret; + ret.Add(g); + foreach (GraphNode gn in g.Suc) + { + ret.AddRange(m_MarkLoopExitUncheckable(gn, l)); + } + + return ret; + } + + // to avoid problems with unreachable code after while(true) {}, try to make the loopexit nodes uncheckable. + private void MakeLoopExitUncheckable(List le) + { + foreach (GraphNode gn in le) + { + if (gn.Suc.Count==1) m_GraphAnalyzer.UncheckableNodes.Add(gn); + } + } + + private void m_RemoveRegularLoopExit(Loop l) + { + List lg = new List(); + lg.AddRange( l.Cutpoint.Suc ); + foreach (GraphNode gn in lg) + { + if (l.LoopExitNodes.Contains(gn)) + { + l.Cutpoint.RemoveEdgeTo(gn); + l.LoopExitNodes.Remove(gn); + } + } + } + + private void m_ReplaceBackEdge(Loop l, GraphNode loopSkip) + { + + foreach (GraphNode gn in l.Cutpoint.LoopingPred) + { + List newsuc = new List(); + foreach (GraphNode s in gn.Suc) + { + if (s == l.Cutpoint) newsuc.Add(loopSkip); + else newsuc.Add(s); + } + gn.Suc = newsuc; + } + } + + + } + #endregion + + #region Graph Analyzer + internal class GraphAnalyzer + { + public List UncheckableNodes = new List(); + + public Dictionary GraphMap = new Dictionary(); + + public List Graphloops = null; + + public GraphAnalyzer(List blocks) + { + //ExitBlock = dedicatedExitBlock; + if (blocks.Count < 1) return; + foreach (Block b in blocks) GraphMap[b] = new GraphNode(b); + foreach (Block b in blocks) + { + foreach (Block pre in b.Predecessors) GraphMap[b].Pre.Add(GraphMap[pre]); + GotoCmd gc = b.TransferCmd as GotoCmd; + if (gc != null) + { + foreach (Block suc in gc.labelTargets) GraphMap[b].Suc.Add(GraphMap[suc]); + } + } + + + m_DetectCutPoints(GraphMap[blocks[0]]); + + //m_DetectCutPoints(GraphMap[blocks[0]], null, new List()); + Graphloops = m_CollectLoops(GraphMap[blocks[0]], null); + + } + + public List ToImplementation(out List uncheckables) + { + List blocks = new List(); + uncheckables = new List(); + + foreach (KeyValuePair kvp in GraphMap) + { + Block b = kvp.Key; + if (UncheckableNodes.Contains(GraphMap[b])) uncheckables.Add(b); + blocks.Add(b); + b.Predecessors = new List(); + foreach (GraphNode p in kvp.Value.Pre) b.Predecessors.Add(p.Label); + if (kvp.Value.Suc.Count > 0) + { + List bs = new List(); + foreach (GraphNode s in kvp.Value.Suc) bs.Add(s.Label); + b.TransferCmd = new GotoCmd(b.tok, bs); + } + else + { + b.TransferCmd = new ReturnCmd(b.tok); + } + } + + return blocks; + } + + public GraphNode CloneGraphNode(GraphNode gn, string prefix) + { + List cmds = new List(gn.Label.Cmds); + + Block b = new Block(gn.Label.tok, prefix+gn.Label.Label, cmds, gn.Label.TransferCmd); + GraphNode clone = new GraphNode(b); + clone.IsCutpoint = gn.IsCutpoint; + clone.Suc.AddRange(gn.Suc); + clone.Pre.AddRange(gn.Pre); + clone.LoopingPred.AddRange(gn.LoopingPred); + GraphMap[b] = clone; + //if (gn.Label == ExitBlock) ExitBlock = b; + return clone; + } + + public void DeleteGraphNode(GraphNode gn) + { + List affected = new List(); + + foreach (KeyValuePair kvp in GraphMap) + { + if (kvp.Value == gn && !affected.Contains(kvp.Key)) affected.Add(kvp.Key); + } + foreach (Block b in affected) + { + GraphMap.Remove(b); + } + } +/* + private void m_DetectCutPoints(GraphNode gn, GraphNode pred, List visited ) + { + if (visited.Contains(gn) ) + { + if (pred != null && !gn.LoopingPred.Contains(pred)) gn.LoopingPred.Add(pred); + gn.IsCutpoint = true; + Console.WriteLine("Normal RootNode {0}", gn.Label.Label); + return; + } + else + { + List visited_ = new List(); + visited_.AddRange(visited); + visited_.Add(gn); + foreach (GraphNode next in gn.Suc) + { + m_DetectCutPoints(next,gn,visited_); + } + } + + } +*/ + + + private void m_DetectCutPoints(GraphNode gn) + { + List todo = new List(); + List done = new List(); + todo.Add(gn); + + GraphNode current = null; + todo[0].Index = 0; + + while (todo.Count > 0) + { + current = todo[0]; + todo.Remove(current); + + bool ready = true; + foreach (GraphNode p in current.Pre) + { + if (!done.Contains(p) ) + { + _loopbacktracking.Clear(); + if (!m_isLoop(current, p, todo, done)) + { + todo.Add(current); + ready = false; + break; + } + else + { + if (!current.LoopingPred.Contains(p)) current.LoopingPred.Add(p); + current.IsCutpoint = true; + } + } + } + if (!ready) continue; + done.Add(current); + foreach (GraphNode s in current.Suc) + { + if (!todo.Contains(s) && !done.Contains(s)) todo.Add(s); + } + } + + } + + List _loopbacktracking = new List(); + private bool m_isLoop(GraphNode loophead, GraphNode gn, List l1, List l2) + { + if (loophead == gn) return true; + if (l1.Contains(gn) || l2.Contains(gn) || _loopbacktracking.Contains(gn)) return false; + _loopbacktracking.Add(gn); + foreach (GraphNode p in gn.Pre) + { + if (m_isLoop(loophead, p, l1, l2)) return true; + } + return false; + } + + private List m_CollectLoops(GraphNode gn, Loop lastLoop) + { + List ret = new List(); + if (gn.Visited) return ret; + gn.Visited = true; + List loopingSucs = new List(); + if (gn.IsCutpoint) + { + Loop l = new Loop(gn); + if (lastLoop != null) + { + lastLoop.SucLoops.Add(l); + l.PreLoops.Add(lastLoop); + } + loopingSucs = l.LoopNodes; + lastLoop = l; + ret.Add(lastLoop); + } + foreach (GraphNode suc in gn.Suc) + { + if (!loopingSucs.Contains(suc)) ret.AddRange(m_CollectLoops(suc, lastLoop)); + } + //Debugger.Break(); + return ret; + } + } + #endregion + + #region GraphNodeStructure + internal class GraphNode + { + public int Index = -1; // Used for scc detection + public int LowLink = -1; // Used for scc detection + + public GraphNode(Block b) + { + Label = b; IsCutpoint = false; + } + public Block Label; + public List Pre = new List(); + public List Suc = new List(); + public bool IsCutpoint; + public bool Visited = false; + public List LoopingPred = new List(); + + public void AddEdgeTo(GraphNode other) + { + if (!this.Suc.Contains(other)) this.Suc.Add(other); + if (!other.Pre.Contains(this)) other.Pre.Add(this); + } + + public void RemoveEdgeTo(GraphNode other) + { + if (this.Suc.Contains(other)) this.Suc.Remove(other); + if (other.Pre.Contains(this)) other.Pre.Remove(this); + } + + } + #endregion + + #region LoopStructure + internal class Loop + { + public Loop(GraphNode cutpoint) + { + if (!cutpoint.IsCutpoint) + { + Debugger.Break(); + } + Cutpoint = cutpoint; + LoopNodes.Add(Cutpoint); + foreach (GraphNode gn in Cutpoint.LoopingPred) + { + CollectLoopBody(gn); + } + CollectLoopExitNodes(); + } + + // Copy Constructor + public Loop(Loop l, GraphAnalyzer ga, string prefix) + { + + Dictionary clonemap = new Dictionary(); + GraphNode clonecutpoint = null; + foreach (GraphNode gn in l.LoopNodes) + { + clonemap[gn] = ga.CloneGraphNode(gn, prefix); + if (gn == l.Cutpoint) clonecutpoint = clonemap[gn]; + } + + if (clonecutpoint == null) + { + Debugger.Break(); + return; + } + // Replace the pre and post nodes by the corresponding clone + foreach (GraphNode gn in l.LoopNodes) + { + List newl = new List(); + foreach (GraphNode g in clonemap[gn].Pre) + { + if (clonemap.ContainsKey(g)) newl.Add(clonemap[g]); + else newl.Add(g); + } + clonemap[gn].Pre = newl; + newl = new List(); + foreach (GraphNode g in clonemap[gn].Suc) + { + if (clonemap.ContainsKey(g)) newl.Add(clonemap[g]); + else newl.Add(g); + } + clonemap[gn].Suc = newl; + newl = new List(); + foreach (GraphNode g in clonemap[gn].LoopingPred) + { + if (clonemap.ContainsKey(g)) newl.Add(clonemap[g]); + else newl.Add(g); + } + clonemap[gn].LoopingPred = newl; + } + + foreach (GraphNode gn in l.Cutpoint.LoopingPred) + { + clonecutpoint.LoopingPred.Remove(gn); + clonecutpoint.LoopingPred.Add(clonemap[gn]); + } + + + + SucLoops.AddRange(l.SucLoops); + PreLoops.AddRange(l.PreLoops); + Cutpoint = clonecutpoint; + LoopNodes.Add(Cutpoint); + foreach (GraphNode gn in Cutpoint.LoopingPred) + { + CollectLoopBody(gn); + } + CollectLoopExitNodes(); + } + + private void CollectLoopBody(GraphNode gn) + { + if (gn == Cutpoint) return; + if (!LoopNodes.Contains(gn)) + { + if (gn.IsCutpoint) // nested loop found + { + Loop lo = new Loop(gn); + foreach (GraphNode lgn in lo.LoopNodes) + { + if (!LoopNodes.Contains(lgn)) LoopNodes.Add(lgn); + } + NestedLoops.Add(lo); + } + else + { + LoopNodes.Add(gn); + } + foreach (GraphNode pre in gn.Pre) if (!gn.LoopingPred.Contains(pre)) CollectLoopBody(pre); + } + } + + private void CollectLoopExitNodes() + { + foreach (GraphNode gn in LoopNodes) + { + foreach (GraphNode gn_ in gn.Suc) + { + if (!LoopNodes.Contains(gn_) && !LoopExitNodes.Contains(gn_)) LoopExitNodes.Add(gn_); + } + } + } + + public GraphNode Cutpoint; + public List LoopExitNodes = new List(); + public List NestedLoops = new List(); + public List SucLoops = new List(); + public List PreLoops = new List(); + public List LoopNodes = new List(); + } + #endregion + + #endregion } \ No newline at end of file diff --git a/Source/Doomed/DoomedStrategy.cs b/Source/Doomed/DoomedStrategy.cs index 9e280873..76261827 100644 --- a/Source/Doomed/DoomedStrategy.cs +++ b/Source/Doomed/DoomedStrategy.cs @@ -1,528 +1,528 @@ -//----------------------------------------------------------------------------- -// -// 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 -{ - #region SuperClass for different doomed code detection strategies - abstract internal class DoomDetectionStrategy - { - public int __DEBUG_BlocksChecked = 0; - public int __DEBUG_BlocksTotal = 0; - public int __DEBUG_InfeasibleTraces = 0; - public int __DEBUG_TracesChecked = 0; - public int __DEBUG_TracesTotal = 0; - public int __DEBUG_EQCTotal = 0; - public int __DEBUG_EQCLeaf = 0; - public int __DEBUG_EQCChecked = 0; - - //Please use this one to toggle your Debug output - protected bool __DEBUGOUT = CommandLineOptions.Clo.DoomStrategy != -1; - - protected Implementation impl; - protected BlockHierachy m_BlockH = null; - - protected int m_MaxBranchingDepth = 0; - protected int m_MaxK = 0; - - protected Stopwatch sw = new Stopwatch(); - - - // This is the List with all detected doomed program points. This List is used by VCDoomed.cs to - // create an error message - public List/*!*/>/*!*/ DetectedBlock = new List/*!*/>(); - - private List __DEBUG_minelements = new List(); - - // There is no default constructor, because these parameters are needed for most subclasses - public DoomDetectionStrategy(Implementation imp, Block unifiedexit, List 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; - } - - public int MaxBlocks, MinBlocks; - public bool HACK_NewCheck; - - // This method is called by the prover while it returns true. The prover checks for each - // List lb if - // |= !lb_1 /\ ... /\ !lb_n => wlp(Program, false) - // and passes the result to SetCurrentResult - abstract public bool GetNextBlock(out List passBlock); - - // This method is called to inform about the prover outcome for the previous GetNextBlock call. - abstract public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb); - - protected List m_GetErrorTraceFromCE(DoomErrorHandler cb) - { - BlockHierachyNode tn=null; - List errortrace = new List(); - foreach (Block b in cb.TraceNodes) - { - if (errortrace.Contains(b)) continue; - if (m_BlockH.BlockToHierachyMap.TryGetValue(b, out tn)) - { - foreach (Block b_ in tn.Unavoidable) - { - if (!errortrace.Contains(b_)) errortrace.Add(b_); - } - foreach (Block b_ in tn.Content) - { - if (!errortrace.Contains(b_)) errortrace.Add(b_); - } - } - } - return errortrace; - } - - private List __pathLength = new List(); - private List __leavespp = new List(); - protected void m_GatherInfo(Block b, int branchingdepth, int leavespp, int plen) - { - if (b.Predecessors.Count > 1) branchingdepth--; - - GotoCmd gc = b.TransferCmd as GotoCmd; - if (__DEBUG_minelements.Contains(b)) leavespp++; - plen++; - if (gc != null && gc.labelTargets.Count>0) - { - if (gc.labelTargets.Count > 1) branchingdepth++; - m_MaxBranchingDepth = (branchingdepth > m_MaxBranchingDepth) ? branchingdepth : m_MaxBranchingDepth; - foreach (Block s in gc.labelTargets) - { - m_GatherInfo(s, branchingdepth, leavespp,plen); - } - } - else - { - __pathLength.Add(plen); - __leavespp.Add(leavespp); - m_MaxK = (m_MaxK > leavespp) ? m_MaxK : leavespp; - } - } - - - - } - #endregion - - #region BruteForce Strategy - internal class NoStrategy : DoomDetectionStrategy - { - private List m_Blocks = new List(); - private int m_Current = 0; - - public NoStrategy(Implementation imp, Block unifiedexit, List unreach) - : base(imp, unifiedexit, unreach) - { - m_Blocks = imp.Blocks; - } - - override public bool GetNextBlock(out List lb) - { - if (m_Current < m_Blocks.Count) - { - lb = new List(); - lb.Add(m_Blocks[m_Current]); - m_Current++; - return true; - } - lb = null; - return false; - } - - // This method is called to inform about the prover outcome for the previous GetNextBlock call. - override public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) - { - this.__DEBUG_BlocksChecked++; - // outcome==Valid means that there is no feasible execution for the current block/path (i.e., might be doomed) - if (outcome == ProverInterface.Outcome.Valid && m_Current <= m_Blocks.Count) - { - List lb = new List(); - lb.Add(m_Blocks[m_Current - 1]); - DetectedBlock.Add(lb); - } - return true; - } - } - #endregion - - #region Only check the minimal elements of the Hasse diagram - internal class HierachyStrategy : DoomDetectionStrategy - { - private List m_Blocks = new List(); - private List m_doomedBlocks = new List(); - private int m_Current = 0; - - public HierachyStrategy(Implementation imp, Block unifiedexit, List unreach) - : base(imp, unifiedexit, unreach) - { - foreach (BlockHierachyNode bhn in m_BlockH.Leaves) - { - if (bhn.Content.Count > 0) - { - m_Blocks.Add(bhn.Content[0]); - } - } - } - - override public bool GetNextBlock(out List lb) - { - sw.Start(); - if (m_Current < m_Blocks.Count) - { - lb = new List(); - lb.Add(m_Blocks[m_Current]); - m_Current++; - return true; - } - else - { - DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_doomedBlocks)); - } - lb = null; - return false; - } - - // This method is called to inform about the prover outcome for the previous GetNextBlock call. - override public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) - { - this.__DEBUG_BlocksChecked++; - // outcome==Valid means that there is no feasible execution for the current block/path (i.e., might be doomed) - if (outcome == ProverInterface.Outcome.Valid && m_Current <= m_Blocks.Count) - { - m_doomedBlocks.Add(m_Blocks[m_Current - 1]); - } - if (__DEBUGOUT) Console.WriteLine("K := {0,3} , out {1,8}, time {2,12}", MaxBlocks, outcome, sw.ElapsedTicks); - sw.Stop(); - sw.Reset(); - - return true; - } - } - #endregion - - #region Only check the minimal elements of the Hasse diagram and use CEs - internal class HierachyCEStrategy : DoomDetectionStrategy - { - private List m_Blocks = new List(); - private List m_doomedBlocks = new List(); - private Block m_Current = null; - - public HierachyCEStrategy(Implementation imp, Block unifiedexit, List unreach) - : base(imp, unifiedexit, unreach) - { - foreach (BlockHierachyNode bhn in m_BlockH.Leaves) - { - if (bhn.Content.Count > 0) - { - m_Blocks.Add(bhn.Content[0]); - } - } - } - - override public bool GetNextBlock(out List lb) - { - m_Current = null; - if (m_Blocks.Count > 0) - { - m_Current = m_Blocks[0]; - m_Blocks.Remove(m_Current); - lb = new List(); - lb.Add(m_Current); - return true; - } - else - { - DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_doomedBlocks)); - } - lb = null; - return false; - } - - // This method is called to inform about the prover outcome for the previous GetNextBlock call. - override public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) - { - this.__DEBUG_BlocksChecked++; - // outcome==Valid means that there is no feasible execution for the current block/path (i.e., might be doomed) - if (outcome == ProverInterface.Outcome.Valid && m_Current != null) - { - m_doomedBlocks.Add(m_Current); - } - else if (outcome == ProverInterface.Outcome.Invalid) - { - List errortrace = m_GetErrorTraceFromCE(cb); - foreach (Block b in errortrace) - { - if (m_Blocks.Contains(b)) - { - m_Blocks.Remove(b); - } - } - cb.TraceNodes.Clear(); - } - return true; - } - } - #endregion - - #region Path Cover Optimization with L - internal class PathCoverStrategy : DoomDetectionStrategy - { - List m_Uncheckedlocks = new List(); - List m_Ignore = new List(); - - Random m_Random = new Random(); - bool m_NoMoreMoves = false; - - private List m_foundBlock = new List(); - - public PathCoverStrategy(Implementation imp, Block unifiedexit, List unreach) - : base(imp, unifiedexit, unreach) - { - m_Ignore = unreach; - HACK_NewCheck = true; - impl = imp; - foreach (BlockHierachyNode bhn in m_BlockH.Leaves) - { - if (bhn.Content.Count > 0) - { - m_Uncheckedlocks.Add(bhn.Content[0]); - } - - } - m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks); - MinBlocks = m_MaxK / 2 + (m_MaxK % 2 > 0 ? 1 : 0); - MaxBlocks = -1; - } - - override public bool GetNextBlock(out List lb) - { - sw.Start(); - - lb = new List(); - - if (m_Uncheckedlocks.Count == 0 || m_NoMoreMoves) - { - if (m_Uncheckedlocks.Count > 0) - { - DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_Uncheckedlocks)); - } - - return false; - } - - lb.AddRange(m_Uncheckedlocks); - - return true; - } - - override public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) - { - this.__DEBUG_BlocksChecked++; - // Valid means infeasible... - int oldl = MinBlocks; - int oldsize = m_Uncheckedlocks.Count; - - - if (outcome == ProverInterface.Outcome.Valid) - { - this.__DEBUG_InfeasibleTraces++; - if (MinBlocks == 1) - { - m_NoMoreMoves = true; - } - else - { - MinBlocks = 1; - } - } - else if (outcome == ProverInterface.Outcome.Invalid) - { - this.__DEBUG_TracesChecked++; - - List errortrace = m_GetErrorTraceFromCE(cb); - foreach (Block b in errortrace) - { - if (m_Uncheckedlocks.Contains(b)) - { - m_Uncheckedlocks.Remove(b); - } - } - cb.TraceNodes.Clear(); - m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks); - if (m_MaxK < 1) - { - m_NoMoreMoves = true; m_Uncheckedlocks.Clear(); - } - MinBlocks = m_MaxK / 2 + (m_MaxK % 2 > 0 ? 1 : 0); - //if (MinBlocks > m_MaxK) MinBlocks = m_MaxK; - - } - else - { - m_NoMoreMoves = true; m_Uncheckedlocks.Clear(); - } - if (__DEBUGOUT) - Console.WriteLine("K := {0,3}, L := {1,3}, deltaSp {2,3}, out {3,8}, time {4,8}", MaxBlocks, oldl, (oldsize - m_Uncheckedlocks.Count), outcome, sw.ElapsedTicks); - sw.Stop(); - sw.Reset(); - return true; - } - - - } - #endregion - - #region Path Cover Optimization with K - internal class PathCoverStrategyK : DoomDetectionStrategy - { - List m_Uncheckedlocks = new List(); - List m_Ignore = new List(); - - Random m_Random = new Random(); - bool m_NoMoreMoves = false; - - private List m_foundBlock = new List(); - - public PathCoverStrategyK(Implementation imp, Block unifiedexit, List unreach) - : base(imp, unifiedexit, unreach) - { - m_Ignore = unreach; - HACK_NewCheck = true; - impl = imp; - foreach (BlockHierachyNode bhn in m_BlockH.Leaves) - { - if (bhn.Content.Count > 0) - { - m_Uncheckedlocks.Add(bhn.Content[0]); - } - - } - - m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks); - - MaxBlocks = m_Uncheckedlocks.Count; - if (m_MaxK < m_Uncheckedlocks.Count && m_MaxK > 0) - { - MaxBlocks = m_MaxK; - } - else if (m_MaxK >= m_Uncheckedlocks.Count) - { - MaxBlocks = m_Uncheckedlocks.Count; - } - else - { - MaxBlocks = 1; - } - //Console.WriteLine("InitK {0}, Max {1}", m_MaxK, MaxBlocks); - } - - override public bool GetNextBlock(out List lb) - { - sw.Start(); - - lb = new List(); - - if (m_Uncheckedlocks.Count == 0 || m_NoMoreMoves) - { - if (m_Uncheckedlocks.Count > 0) - { - DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_Uncheckedlocks)); - } - - return false; - } - - lb.AddRange(m_Uncheckedlocks); - - MaxBlocks = MaxBlocks > m_Uncheckedlocks.Count ? m_Uncheckedlocks.Count : MaxBlocks; - MinBlocks = MaxBlocks / 2 + (MaxBlocks % 2 > 0 ? 1 : 0); - return true; - } - - override public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) - { - this.__DEBUG_BlocksChecked++; - // Valid means infeasible... - int oldk = MaxBlocks; - int oldl = MinBlocks; - int oldsize = m_Uncheckedlocks.Count; - - if (outcome == ProverInterface.Outcome.Valid) - { - this.__DEBUG_InfeasibleTraces++; - if (MaxBlocks == 1) - { - m_NoMoreMoves = true; - } - else - { - MaxBlocks /= 2; - } - } - else if (outcome == ProverInterface.Outcome.Invalid) - { - this.__DEBUG_TracesChecked++; - - List errortrace = m_GetErrorTraceFromCE(cb); - foreach (Block b in errortrace) - { - if (m_Uncheckedlocks.Contains(b)) - { - m_Uncheckedlocks.Remove(b); - } - } - cb.TraceNodes.Clear(); - - int k = m_BlockH.GetMaxK(m_Uncheckedlocks); - MaxBlocks = (k > MaxBlocks) ? MaxBlocks : k; - } - else - { - m_NoMoreMoves = true; m_Uncheckedlocks.Clear(); - } - if (__DEBUGOUT) - Console.WriteLine("K := {0,3}, L := {1,3}, deltaSp {2,3}, out {3,8}, time {4,8}", oldk, oldl, (oldsize - m_Uncheckedlocks.Count), outcome, sw.ElapsedTicks); - sw.Stop(); - sw.Reset(); - return true; - } - - - } - #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 +{ + #region SuperClass for different doomed code detection strategies + abstract internal class DoomDetectionStrategy + { + public int __DEBUG_BlocksChecked = 0; + public int __DEBUG_BlocksTotal = 0; + public int __DEBUG_InfeasibleTraces = 0; + public int __DEBUG_TracesChecked = 0; + public int __DEBUG_TracesTotal = 0; + public int __DEBUG_EQCTotal = 0; + public int __DEBUG_EQCLeaf = 0; + public int __DEBUG_EQCChecked = 0; + + //Please use this one to toggle your Debug output + protected bool __DEBUGOUT = CommandLineOptions.Clo.DoomStrategy != -1; + + protected Implementation impl; + protected BlockHierachy m_BlockH = null; + + protected int m_MaxBranchingDepth = 0; + protected int m_MaxK = 0; + + protected Stopwatch sw = new Stopwatch(); + + + // This is the List with all detected doomed program points. This List is used by VCDoomed.cs to + // create an error message + public List/*!*/>/*!*/ DetectedBlock = new List/*!*/>(); + + private List __DEBUG_minelements = new List(); + + // There is no default constructor, because these parameters are needed for most subclasses + public DoomDetectionStrategy(Implementation imp, Block unifiedexit, List 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; + } + + public int MaxBlocks, MinBlocks; + public bool HACK_NewCheck; + + // This method is called by the prover while it returns true. The prover checks for each + // List lb if + // |= !lb_1 /\ ... /\ !lb_n => wlp(Program, false) + // and passes the result to SetCurrentResult + abstract public bool GetNextBlock(out List passBlock); + + // This method is called to inform about the prover outcome for the previous GetNextBlock call. + abstract public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb); + + protected List m_GetErrorTraceFromCE(DoomErrorHandler cb) + { + BlockHierachyNode tn=null; + List errortrace = new List(); + foreach (Block b in cb.TraceNodes) + { + if (errortrace.Contains(b)) continue; + if (m_BlockH.BlockToHierachyMap.TryGetValue(b, out tn)) + { + foreach (Block b_ in tn.Unavoidable) + { + if (!errortrace.Contains(b_)) errortrace.Add(b_); + } + foreach (Block b_ in tn.Content) + { + if (!errortrace.Contains(b_)) errortrace.Add(b_); + } + } + } + return errortrace; + } + + private List __pathLength = new List(); + private List __leavespp = new List(); + protected void m_GatherInfo(Block b, int branchingdepth, int leavespp, int plen) + { + if (b.Predecessors.Count > 1) branchingdepth--; + + GotoCmd gc = b.TransferCmd as GotoCmd; + if (__DEBUG_minelements.Contains(b)) leavespp++; + plen++; + if (gc != null && gc.labelTargets.Count>0) + { + if (gc.labelTargets.Count > 1) branchingdepth++; + m_MaxBranchingDepth = (branchingdepth > m_MaxBranchingDepth) ? branchingdepth : m_MaxBranchingDepth; + foreach (Block s in gc.labelTargets) + { + m_GatherInfo(s, branchingdepth, leavespp,plen); + } + } + else + { + __pathLength.Add(plen); + __leavespp.Add(leavespp); + m_MaxK = (m_MaxK > leavespp) ? m_MaxK : leavespp; + } + } + + + + } + #endregion + + #region BruteForce Strategy + internal class NoStrategy : DoomDetectionStrategy + { + private List m_Blocks = new List(); + private int m_Current = 0; + + public NoStrategy(Implementation imp, Block unifiedexit, List unreach) + : base(imp, unifiedexit, unreach) + { + m_Blocks = imp.Blocks; + } + + override public bool GetNextBlock(out List lb) + { + if (m_Current < m_Blocks.Count) + { + lb = new List(); + lb.Add(m_Blocks[m_Current]); + m_Current++; + return true; + } + lb = null; + return false; + } + + // This method is called to inform about the prover outcome for the previous GetNextBlock call. + override public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) + { + this.__DEBUG_BlocksChecked++; + // outcome==Valid means that there is no feasible execution for the current block/path (i.e., might be doomed) + if (outcome == ProverInterface.Outcome.Valid && m_Current <= m_Blocks.Count) + { + List lb = new List(); + lb.Add(m_Blocks[m_Current - 1]); + DetectedBlock.Add(lb); + } + return true; + } + } + #endregion + + #region Only check the minimal elements of the Hasse diagram + internal class HierachyStrategy : DoomDetectionStrategy + { + private List m_Blocks = new List(); + private List m_doomedBlocks = new List(); + private int m_Current = 0; + + public HierachyStrategy(Implementation imp, Block unifiedexit, List unreach) + : base(imp, unifiedexit, unreach) + { + foreach (BlockHierachyNode bhn in m_BlockH.Leaves) + { + if (bhn.Content.Count > 0) + { + m_Blocks.Add(bhn.Content[0]); + } + } + } + + override public bool GetNextBlock(out List lb) + { + sw.Start(); + if (m_Current < m_Blocks.Count) + { + lb = new List(); + lb.Add(m_Blocks[m_Current]); + m_Current++; + return true; + } + else + { + DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_doomedBlocks)); + } + lb = null; + return false; + } + + // This method is called to inform about the prover outcome for the previous GetNextBlock call. + override public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) + { + this.__DEBUG_BlocksChecked++; + // outcome==Valid means that there is no feasible execution for the current block/path (i.e., might be doomed) + if (outcome == ProverInterface.Outcome.Valid && m_Current <= m_Blocks.Count) + { + m_doomedBlocks.Add(m_Blocks[m_Current - 1]); + } + if (__DEBUGOUT) Console.WriteLine("K := {0,3} , out {1,8}, time {2,12}", MaxBlocks, outcome, sw.ElapsedTicks); + sw.Stop(); + sw.Reset(); + + return true; + } + } + #endregion + + #region Only check the minimal elements of the Hasse diagram and use CEs + internal class HierachyCEStrategy : DoomDetectionStrategy + { + private List m_Blocks = new List(); + private List m_doomedBlocks = new List(); + private Block m_Current = null; + + public HierachyCEStrategy(Implementation imp, Block unifiedexit, List unreach) + : base(imp, unifiedexit, unreach) + { + foreach (BlockHierachyNode bhn in m_BlockH.Leaves) + { + if (bhn.Content.Count > 0) + { + m_Blocks.Add(bhn.Content[0]); + } + } + } + + override public bool GetNextBlock(out List lb) + { + m_Current = null; + if (m_Blocks.Count > 0) + { + m_Current = m_Blocks[0]; + m_Blocks.Remove(m_Current); + lb = new List(); + lb.Add(m_Current); + return true; + } + else + { + DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_doomedBlocks)); + } + lb = null; + return false; + } + + // This method is called to inform about the prover outcome for the previous GetNextBlock call. + override public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) + { + this.__DEBUG_BlocksChecked++; + // outcome==Valid means that there is no feasible execution for the current block/path (i.e., might be doomed) + if (outcome == ProverInterface.Outcome.Valid && m_Current != null) + { + m_doomedBlocks.Add(m_Current); + } + else if (outcome == ProverInterface.Outcome.Invalid) + { + List errortrace = m_GetErrorTraceFromCE(cb); + foreach (Block b in errortrace) + { + if (m_Blocks.Contains(b)) + { + m_Blocks.Remove(b); + } + } + cb.TraceNodes.Clear(); + } + return true; + } + } + #endregion + + #region Path Cover Optimization with L + internal class PathCoverStrategy : DoomDetectionStrategy + { + List m_Uncheckedlocks = new List(); + List m_Ignore = new List(); + + Random m_Random = new Random(); + bool m_NoMoreMoves = false; + + private List m_foundBlock = new List(); + + public PathCoverStrategy(Implementation imp, Block unifiedexit, List unreach) + : base(imp, unifiedexit, unreach) + { + m_Ignore = unreach; + HACK_NewCheck = true; + impl = imp; + foreach (BlockHierachyNode bhn in m_BlockH.Leaves) + { + if (bhn.Content.Count > 0) + { + m_Uncheckedlocks.Add(bhn.Content[0]); + } + + } + m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks); + MinBlocks = m_MaxK / 2 + (m_MaxK % 2 > 0 ? 1 : 0); + MaxBlocks = -1; + } + + override public bool GetNextBlock(out List lb) + { + sw.Start(); + + lb = new List(); + + if (m_Uncheckedlocks.Count == 0 || m_NoMoreMoves) + { + if (m_Uncheckedlocks.Count > 0) + { + DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_Uncheckedlocks)); + } + + return false; + } + + lb.AddRange(m_Uncheckedlocks); + + return true; + } + + override public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) + { + this.__DEBUG_BlocksChecked++; + // Valid means infeasible... + int oldl = MinBlocks; + int oldsize = m_Uncheckedlocks.Count; + + + if (outcome == ProverInterface.Outcome.Valid) + { + this.__DEBUG_InfeasibleTraces++; + if (MinBlocks == 1) + { + m_NoMoreMoves = true; + } + else + { + MinBlocks = 1; + } + } + else if (outcome == ProverInterface.Outcome.Invalid) + { + this.__DEBUG_TracesChecked++; + + List errortrace = m_GetErrorTraceFromCE(cb); + foreach (Block b in errortrace) + { + if (m_Uncheckedlocks.Contains(b)) + { + m_Uncheckedlocks.Remove(b); + } + } + cb.TraceNodes.Clear(); + m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks); + if (m_MaxK < 1) + { + m_NoMoreMoves = true; m_Uncheckedlocks.Clear(); + } + MinBlocks = m_MaxK / 2 + (m_MaxK % 2 > 0 ? 1 : 0); + //if (MinBlocks > m_MaxK) MinBlocks = m_MaxK; + + } + else + { + m_NoMoreMoves = true; m_Uncheckedlocks.Clear(); + } + if (__DEBUGOUT) + Console.WriteLine("K := {0,3}, L := {1,3}, deltaSp {2,3}, out {3,8}, time {4,8}", MaxBlocks, oldl, (oldsize - m_Uncheckedlocks.Count), outcome, sw.ElapsedTicks); + sw.Stop(); + sw.Reset(); + return true; + } + + + } + #endregion + + #region Path Cover Optimization with K + internal class PathCoverStrategyK : DoomDetectionStrategy + { + List m_Uncheckedlocks = new List(); + List m_Ignore = new List(); + + Random m_Random = new Random(); + bool m_NoMoreMoves = false; + + private List m_foundBlock = new List(); + + public PathCoverStrategyK(Implementation imp, Block unifiedexit, List unreach) + : base(imp, unifiedexit, unreach) + { + m_Ignore = unreach; + HACK_NewCheck = true; + impl = imp; + foreach (BlockHierachyNode bhn in m_BlockH.Leaves) + { + if (bhn.Content.Count > 0) + { + m_Uncheckedlocks.Add(bhn.Content[0]); + } + + } + + m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks); + + MaxBlocks = m_Uncheckedlocks.Count; + if (m_MaxK < m_Uncheckedlocks.Count && m_MaxK > 0) + { + MaxBlocks = m_MaxK; + } + else if (m_MaxK >= m_Uncheckedlocks.Count) + { + MaxBlocks = m_Uncheckedlocks.Count; + } + else + { + MaxBlocks = 1; + } + //Console.WriteLine("InitK {0}, Max {1}", m_MaxK, MaxBlocks); + } + + override public bool GetNextBlock(out List lb) + { + sw.Start(); + + lb = new List(); + + if (m_Uncheckedlocks.Count == 0 || m_NoMoreMoves) + { + if (m_Uncheckedlocks.Count > 0) + { + DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_Uncheckedlocks)); + } + + return false; + } + + lb.AddRange(m_Uncheckedlocks); + + MaxBlocks = MaxBlocks > m_Uncheckedlocks.Count ? m_Uncheckedlocks.Count : MaxBlocks; + MinBlocks = MaxBlocks / 2 + (MaxBlocks % 2 > 0 ? 1 : 0); + return true; + } + + override public bool SetCurrentResult(List reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) + { + this.__DEBUG_BlocksChecked++; + // Valid means infeasible... + int oldk = MaxBlocks; + int oldl = MinBlocks; + int oldsize = m_Uncheckedlocks.Count; + + if (outcome == ProverInterface.Outcome.Valid) + { + this.__DEBUG_InfeasibleTraces++; + if (MaxBlocks == 1) + { + m_NoMoreMoves = true; + } + else + { + MaxBlocks /= 2; + } + } + else if (outcome == ProverInterface.Outcome.Invalid) + { + this.__DEBUG_TracesChecked++; + + List errortrace = m_GetErrorTraceFromCE(cb); + foreach (Block b in errortrace) + { + if (m_Uncheckedlocks.Contains(b)) + { + m_Uncheckedlocks.Remove(b); + } + } + cb.TraceNodes.Clear(); + + int k = m_BlockH.GetMaxK(m_Uncheckedlocks); + MaxBlocks = (k > MaxBlocks) ? MaxBlocks : k; + } + else + { + m_NoMoreMoves = true; m_Uncheckedlocks.Clear(); + } + if (__DEBUGOUT) + Console.WriteLine("K := {0,3}, L := {1,3}, deltaSp {2,3}, out {3,8}, time {4,8}", oldk, oldl, (oldsize - m_Uncheckedlocks.Count), outcome, sw.ElapsedTicks); + sw.Stop(); + sw.Reset(); + return true; + } + + + } + #endregion + } \ No newline at end of file diff --git a/Source/Doomed/HasseDiagram.cs b/Source/Doomed/HasseDiagram.cs index ad3d487e..c866662e 100644 --- a/Source/Doomed/HasseDiagram.cs +++ b/Source/Doomed/HasseDiagram.cs @@ -1,424 +1,424 @@ -//----------------------------------------------------------------------------- -// -// 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 -{ - internal class BlockHierachyNode - { - public List Unavoidable; - public List Content = new List(); - public List Parents = new List(); - public List Children = new List(); - - public bool Checked, Doomed, DoubleChecked; - - public BlockHierachyNode(Block current, List unavoidable) - { - Checked = false; Doomed = false; DoubleChecked = false; - Unavoidable = unavoidable; - Content.Add(current); - } - - public static bool operator <(BlockHierachyNode left, BlockHierachyNode right) - { - return Compare(left,right)>0; - } - - public static bool operator >(BlockHierachyNode left, BlockHierachyNode right) - { - return Compare(left, right) < 0; - } - - // Compare the unavoidable blocks of two BlockHierachyNodes. - // returns 0 if sets have the same size, -1 if l2 has an element - // that is not in l1, otherwise the size of the intersection. - public static int Compare(BlockHierachyNode l1, BlockHierachyNode l2) - { - List tmp = new List(); - tmp.AddRange(l2.Unavoidable); - foreach (Block b in l1.Unavoidable) - { - if (tmp.Contains(b)) tmp.Remove(b); - else return -1; - } - return tmp.Count; - } - } - - internal class HasseDiagram - { - public readonly List Leaves = new List(); - public readonly List Roots = new List(); - - public HasseDiagram(List nodes) - { - Dictionary> largerElements = new Dictionary>(); - foreach (BlockHierachyNode left in nodes) - { - largerElements[left] = new List(); - foreach (BlockHierachyNode right in nodes) - { - if (left != right) - { - if (left < right) - { - largerElements[left].Add(right); - } - } - } - if (largerElements[left].Count == 0) Leaves.Add(left); - } - - List done = new List(); - List lastround = null; - - //Debugger.Break(); - - // Now that we have the leaves, build the Hasse diagram - while (done.Count < nodes.Count) - { - List maxelements = new List(); - maxelements.AddRange(nodes); - foreach (BlockHierachyNode bhn in nodes) - { - if (!done.Contains(bhn)) - { - foreach (BlockHierachyNode tmp in largerElements[bhn]) - { - if (maxelements.Contains(tmp)) maxelements.Remove(tmp); - } - } - else - { - maxelements.Remove(bhn); - } - } - - done.AddRange(maxelements); - - if (lastround != null) - { - foreach (BlockHierachyNode tmp in lastround) - { - foreach (BlockHierachyNode tmp2 in maxelements) - { - if (largerElements[tmp].Contains(tmp2)) - { - if (!tmp.Children.Contains(tmp2)) tmp.Children.Add(tmp2); - if (!tmp2.Parents.Contains(tmp)) tmp2.Parents.Add(tmp); - } - } - } - } - else - { - Roots.AddRange(maxelements); - } - lastround = maxelements; - } - } - - - } - - internal class BlockHierachy - { - public BlockHierachyNode RootNode = null; - readonly public Dictionary BlockToHierachyMap = new Dictionary(); - readonly public Dictionary> Dominators = new Dictionary>(); - readonly public Dictionary> PostDominators = new Dictionary>(); - readonly public List Leaves = new List(); - - private Implementation m_Impl; - - public BlockHierachy(Implementation impl, Block unifiedExit) - { - m_Impl = impl; - List blocks = impl.Blocks; - List tmp_hnodes = new List(); - Dictionary> unavoidable = new Dictionary>(); - - BfsTraverser(blocks[0], true, Dominators); - BfsTraverser(unifiedExit, false, PostDominators); - - foreach (Block b in blocks) - { - List l1 = Dominators[b]; - List l2 = PostDominators[b]; - unavoidable[b] = m_MergeLists(l1, l2); - - BlockHierachyNode bhn = new BlockHierachyNode(b, unavoidable[b]); - bool found = false; - foreach (KeyValuePair kvp in BlockToHierachyMap) - { - if (BlockHierachyNode.Compare(kvp.Value, bhn) == 0) // using the overloaded compare operator - { - kvp.Value.Content.AddRange(bhn.Content); - BlockToHierachyMap[b] = kvp.Value; - found = true; - break; - } - } - if (!found) - { - BlockToHierachyMap[b] = bhn; - tmp_hnodes.Add(bhn); - } - } - - HasseDiagram hd = new HasseDiagram(tmp_hnodes); - Leaves = hd.Leaves; - } - - public int GetMaxK(List blocks) - { - m_GetMaxK(blocks); - return (m_MaxK>0) ? m_MaxK : 1; - } - - private int m_MaxK = 0; - private void m_GetMaxK(List blocks) - { - m_MaxK = 0; - Dictionary kstore = new Dictionary(); - List todo = new List(); - List done = new List(); - todo.Add(m_Impl.Blocks[0]); - kstore[m_Impl.Blocks[0]] = 0; - int localmax; - Block current = null; - while (todo.Count > 0) - { - current = todo[0]; - todo.Remove(current); - bool ready = true; - localmax = 0; - if (current.Predecessors!=null) { - foreach (Block p in current.Predecessors) - { - if (!done.Contains(p)) - { - ready = false; break; - } - else localmax = (localmax > kstore[p]) ? localmax : kstore[p]; - } - } - if (!ready) - { - todo.Add(current); continue; - } - done.Add(current); - kstore[current] = (blocks.Contains(current)) ? localmax +1 : localmax; - - m_MaxK = (kstore[current] > m_MaxK) ? kstore[current] : m_MaxK; - - GotoCmd gc = current.TransferCmd as GotoCmd; - if (gc != null) - { - foreach (Block s in gc.labelTargets) - { - if (!todo.Contains(s)) todo.Add(s); - } - } - } - - } - - public List GetOtherDoomedBlocks(List doomedblocks) - { - List alsoDoomed = new List(); - List todo = new List(); - foreach (Block b in doomedblocks) - { - BlockToHierachyMap[b].Doomed = true; - todo.Add(BlockToHierachyMap[b]); - } - - while (todo.Count > 0) - { - BlockHierachyNode current = todo[0]; - todo.Remove(current); - if (!current.Doomed && current.Children.Count > 0) - { - bool childrenDoomed = true; - foreach (BlockHierachyNode c in current.Children) - { - if (!c.Doomed) { childrenDoomed = false; break; } - } - if (childrenDoomed) current.Doomed = true; - } - - if (current.Doomed) - { - foreach (BlockHierachyNode p in current.Parents) - { - if (!todo.Contains(p)) todo.Add(p); - } - foreach (Block b in current.Content) - { - if (!alsoDoomed.Contains(b)) alsoDoomed.Add(b); - } - } - } - - return alsoDoomed; - } - - public void Impl2Dot(string filename) - { - - Contract.Requires(filename != null); - List nodes = new List(); - List edges = new List(); - - string nodestyle = "[shape=box];"; - - List nl = new List(); - foreach (BlockHierachyNode h in BlockToHierachyMap.Values) if (!nl.Contains(h)) nl.Add(h); - - - foreach (BlockHierachyNode b in nl) - { - String l1 = ""; - foreach (Block bl in b.Content) l1 = String.Format("{0}_{1}", l1, bl.Label); - - Contract.Assert(b != null); - nodes.Add(string.Format("\"{0}\" {1}", l1, nodestyle)); - foreach (BlockHierachyNode b_ in b.Children) - { - - String l2 = ""; - foreach (Block bl in b_.Content) l2 = String.Format("{0}_{1}", l2, bl.Label); - edges.Add(String.Format("\"{0}\" -> \"{1}\";", l1, l2)); - } - - } - - using (StreamWriter sw = new StreamWriter(filename)) - { - sw.WriteLine(String.Format("digraph {0} {{", "DISCO")); - // 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 void BfsTraverser(Block current, bool forward, Dictionary> unavoidableBlocks) - { - List todo = new List(); - List done = new List(); - unavoidableBlocks[current] = new List(); - //Debugger.Break(); - todo.Add(current); - while (todo.Count > 0) - { - current = todo[0]; - todo.Remove(current); - List pre = m_Predecessors(current, forward); - bool ready = true; - if (pre != null) - { - foreach (Block bpre in pre) - { - if (!done.Contains(bpre)) - { - ready = false; - break; - } - } - } - if (!ready) - { - todo.Add(current); - continue; - } - done.Add(current); - unavoidableBlocks[current].Add(current); - - List suc = m_Succecessors(current, forward); - if (suc == null) continue; - foreach (Block bsuc in suc) - { - if (unavoidableBlocks.ContainsKey(bsuc)) - { - unavoidableBlocks[bsuc] = m_IntersectLists(unavoidableBlocks[bsuc], unavoidableBlocks[current]); - } - else - { - todo.Add(bsuc); - unavoidableBlocks[bsuc] = new List(); - unavoidableBlocks[bsuc].AddRange(unavoidableBlocks[current]); - } - - } - } - - } - - private List m_MergeLists(List lb1, List lb2) - { - List ret = new List(); - ret.AddRange(lb1); - foreach (Block b in lb2) - { - if (!ret.Contains(b)) ret.Add(b); - } - return ret; - } - - private List m_IntersectLists(List lb1, List lb2) - { - List ret = new List(); - ret.AddRange(lb1); - foreach (Block b in lb2) - { - if (!lb1.Contains(b)) ret.Remove(b); - } - foreach (Block b in lb1) - { - if (ret.Contains(b) && !lb2.Contains(b)) ret.Remove(b); - } - return ret; - } - - private List m_Predecessors(Block b, bool forward) - { - if (forward) return b.Predecessors; - GotoCmd gc = b.TransferCmd as GotoCmd; - if (gc != null) - { - return gc.labelTargets; - } - return null; - } - - private List m_Succecessors(Block b, bool forward) - { - return m_Predecessors(b, !forward); - } - - - } - +//----------------------------------------------------------------------------- +// +// 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 +{ + internal class BlockHierachyNode + { + public List Unavoidable; + public List Content = new List(); + public List Parents = new List(); + public List Children = new List(); + + public bool Checked, Doomed, DoubleChecked; + + public BlockHierachyNode(Block current, List unavoidable) + { + Checked = false; Doomed = false; DoubleChecked = false; + Unavoidable = unavoidable; + Content.Add(current); + } + + public static bool operator <(BlockHierachyNode left, BlockHierachyNode right) + { + return Compare(left,right)>0; + } + + public static bool operator >(BlockHierachyNode left, BlockHierachyNode right) + { + return Compare(left, right) < 0; + } + + // Compare the unavoidable blocks of two BlockHierachyNodes. + // returns 0 if sets have the same size, -1 if l2 has an element + // that is not in l1, otherwise the size of the intersection. + public static int Compare(BlockHierachyNode l1, BlockHierachyNode l2) + { + List tmp = new List(); + tmp.AddRange(l2.Unavoidable); + foreach (Block b in l1.Unavoidable) + { + if (tmp.Contains(b)) tmp.Remove(b); + else return -1; + } + return tmp.Count; + } + } + + internal class HasseDiagram + { + public readonly List Leaves = new List(); + public readonly List Roots = new List(); + + public HasseDiagram(List nodes) + { + Dictionary> largerElements = new Dictionary>(); + foreach (BlockHierachyNode left in nodes) + { + largerElements[left] = new List(); + foreach (BlockHierachyNode right in nodes) + { + if (left != right) + { + if (left < right) + { + largerElements[left].Add(right); + } + } + } + if (largerElements[left].Count == 0) Leaves.Add(left); + } + + List done = new List(); + List lastround = null; + + //Debugger.Break(); + + // Now that we have the leaves, build the Hasse diagram + while (done.Count < nodes.Count) + { + List maxelements = new List(); + maxelements.AddRange(nodes); + foreach (BlockHierachyNode bhn in nodes) + { + if (!done.Contains(bhn)) + { + foreach (BlockHierachyNode tmp in largerElements[bhn]) + { + if (maxelements.Contains(tmp)) maxelements.Remove(tmp); + } + } + else + { + maxelements.Remove(bhn); + } + } + + done.AddRange(maxelements); + + if (lastround != null) + { + foreach (BlockHierachyNode tmp in lastround) + { + foreach (BlockHierachyNode tmp2 in maxelements) + { + if (largerElements[tmp].Contains(tmp2)) + { + if (!tmp.Children.Contains(tmp2)) tmp.Children.Add(tmp2); + if (!tmp2.Parents.Contains(tmp)) tmp2.Parents.Add(tmp); + } + } + } + } + else + { + Roots.AddRange(maxelements); + } + lastround = maxelements; + } + } + + + } + + internal class BlockHierachy + { + public BlockHierachyNode RootNode = null; + readonly public Dictionary BlockToHierachyMap = new Dictionary(); + readonly public Dictionary> Dominators = new Dictionary>(); + readonly public Dictionary> PostDominators = new Dictionary>(); + readonly public List Leaves = new List(); + + private Implementation m_Impl; + + public BlockHierachy(Implementation impl, Block unifiedExit) + { + m_Impl = impl; + List blocks = impl.Blocks; + List tmp_hnodes = new List(); + Dictionary> unavoidable = new Dictionary>(); + + BfsTraverser(blocks[0], true, Dominators); + BfsTraverser(unifiedExit, false, PostDominators); + + foreach (Block b in blocks) + { + List l1 = Dominators[b]; + List l2 = PostDominators[b]; + unavoidable[b] = m_MergeLists(l1, l2); + + BlockHierachyNode bhn = new BlockHierachyNode(b, unavoidable[b]); + bool found = false; + foreach (KeyValuePair kvp in BlockToHierachyMap) + { + if (BlockHierachyNode.Compare(kvp.Value, bhn) == 0) // using the overloaded compare operator + { + kvp.Value.Content.AddRange(bhn.Content); + BlockToHierachyMap[b] = kvp.Value; + found = true; + break; + } + } + if (!found) + { + BlockToHierachyMap[b] = bhn; + tmp_hnodes.Add(bhn); + } + } + + HasseDiagram hd = new HasseDiagram(tmp_hnodes); + Leaves = hd.Leaves; + } + + public int GetMaxK(List blocks) + { + m_GetMaxK(blocks); + return (m_MaxK>0) ? m_MaxK : 1; + } + + private int m_MaxK = 0; + private void m_GetMaxK(List blocks) + { + m_MaxK = 0; + Dictionary kstore = new Dictionary(); + List todo = new List(); + List done = new List(); + todo.Add(m_Impl.Blocks[0]); + kstore[m_Impl.Blocks[0]] = 0; + int localmax; + Block current = null; + while (todo.Count > 0) + { + current = todo[0]; + todo.Remove(current); + bool ready = true; + localmax = 0; + if (current.Predecessors!=null) { + foreach (Block p in current.Predecessors) + { + if (!done.Contains(p)) + { + ready = false; break; + } + else localmax = (localmax > kstore[p]) ? localmax : kstore[p]; + } + } + if (!ready) + { + todo.Add(current); continue; + } + done.Add(current); + kstore[current] = (blocks.Contains(current)) ? localmax +1 : localmax; + + m_MaxK = (kstore[current] > m_MaxK) ? kstore[current] : m_MaxK; + + GotoCmd gc = current.TransferCmd as GotoCmd; + if (gc != null) + { + foreach (Block s in gc.labelTargets) + { + if (!todo.Contains(s)) todo.Add(s); + } + } + } + + } + + public List GetOtherDoomedBlocks(List doomedblocks) + { + List alsoDoomed = new List(); + List todo = new List(); + foreach (Block b in doomedblocks) + { + BlockToHierachyMap[b].Doomed = true; + todo.Add(BlockToHierachyMap[b]); + } + + while (todo.Count > 0) + { + BlockHierachyNode current = todo[0]; + todo.Remove(current); + if (!current.Doomed && current.Children.Count > 0) + { + bool childrenDoomed = true; + foreach (BlockHierachyNode c in current.Children) + { + if (!c.Doomed) { childrenDoomed = false; break; } + } + if (childrenDoomed) current.Doomed = true; + } + + if (current.Doomed) + { + foreach (BlockHierachyNode p in current.Parents) + { + if (!todo.Contains(p)) todo.Add(p); + } + foreach (Block b in current.Content) + { + if (!alsoDoomed.Contains(b)) alsoDoomed.Add(b); + } + } + } + + return alsoDoomed; + } + + public void Impl2Dot(string filename) + { + + Contract.Requires(filename != null); + List nodes = new List(); + List edges = new List(); + + string nodestyle = "[shape=box];"; + + List nl = new List(); + foreach (BlockHierachyNode h in BlockToHierachyMap.Values) if (!nl.Contains(h)) nl.Add(h); + + + foreach (BlockHierachyNode b in nl) + { + String l1 = ""; + foreach (Block bl in b.Content) l1 = String.Format("{0}_{1}", l1, bl.Label); + + Contract.Assert(b != null); + nodes.Add(string.Format("\"{0}\" {1}", l1, nodestyle)); + foreach (BlockHierachyNode b_ in b.Children) + { + + String l2 = ""; + foreach (Block bl in b_.Content) l2 = String.Format("{0}_{1}", l2, bl.Label); + edges.Add(String.Format("\"{0}\" -> \"{1}\";", l1, l2)); + } + + } + + using (StreamWriter sw = new StreamWriter(filename)) + { + sw.WriteLine(String.Format("digraph {0} {{", "DISCO")); + // 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 void BfsTraverser(Block current, bool forward, Dictionary> unavoidableBlocks) + { + List todo = new List(); + List done = new List(); + unavoidableBlocks[current] = new List(); + //Debugger.Break(); + todo.Add(current); + while (todo.Count > 0) + { + current = todo[0]; + todo.Remove(current); + List pre = m_Predecessors(current, forward); + bool ready = true; + if (pre != null) + { + foreach (Block bpre in pre) + { + if (!done.Contains(bpre)) + { + ready = false; + break; + } + } + } + if (!ready) + { + todo.Add(current); + continue; + } + done.Add(current); + unavoidableBlocks[current].Add(current); + + List suc = m_Succecessors(current, forward); + if (suc == null) continue; + foreach (Block bsuc in suc) + { + if (unavoidableBlocks.ContainsKey(bsuc)) + { + unavoidableBlocks[bsuc] = m_IntersectLists(unavoidableBlocks[bsuc], unavoidableBlocks[current]); + } + else + { + todo.Add(bsuc); + unavoidableBlocks[bsuc] = new List(); + unavoidableBlocks[bsuc].AddRange(unavoidableBlocks[current]); + } + + } + } + + } + + private List m_MergeLists(List lb1, List lb2) + { + List ret = new List(); + ret.AddRange(lb1); + foreach (Block b in lb2) + { + if (!ret.Contains(b)) ret.Add(b); + } + return ret; + } + + private List m_IntersectLists(List lb1, List lb2) + { + List ret = new List(); + ret.AddRange(lb1); + foreach (Block b in lb2) + { + if (!lb1.Contains(b)) ret.Remove(b); + } + foreach (Block b in lb1) + { + if (ret.Contains(b) && !lb2.Contains(b)) ret.Remove(b); + } + return ret; + } + + private List m_Predecessors(Block b, bool forward) + { + if (forward) return b.Predecessors; + GotoCmd gc = b.TransferCmd as GotoCmd; + if (gc != null) + { + return gc.labelTargets; + } + return null; + } + + private List m_Succecessors(Block b, bool forward) + { + return m_Predecessors(b, !forward); + } + + + } + } \ No newline at end of file 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