diff options
Diffstat (limited to 'Source/Doomed')
-rw-r--r-- | Source/Doomed/DoomCheck.cs | 814 | ||||
-rw-r--r-- | Source/Doomed/DoomErrorHandler.cs | 170 | ||||
-rw-r--r-- | Source/Doomed/Doomed.csproj | 378 | ||||
-rw-r--r-- | Source/Doomed/DoomedLoopUnrolling.cs | 1298 | ||||
-rw-r--r-- | Source/Doomed/DoomedStrategy.cs | 1054 | ||||
-rw-r--r-- | Source/Doomed/HasseDiagram.cs | 846 | ||||
-rw-r--r-- | Source/Doomed/VCDoomed.cs | 1652 |
7 files changed, 3106 insertions, 3106 deletions
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<Variable> lv,Dictionary<Expr, int> 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<Expr, int> 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<Expr, int> 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<int, Absy> 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<Block> 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<int, Absy>(); // This is only a dummy
- m_Evc = new Evc(check);
- Dictionary<int, Absy> 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<int, Absy>(); // This is only a dummy
- m_Evc = new Evc(check);
- Dictionary<int, Absy> 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<Block> 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<Variable> lv,Dictionary<Expr, int> 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<List<Block/*!>!>!*/>> DoomedSequences {
- get {
- Contract.Ensures(Contract.ForAll(Contract.Result<List<List<Block>>>(), 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<int, Absy> label2absy, Checker ch, out int assertionCount) {
- Contract.Requires(impl != null);
- Contract.Requires(ch != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- TypecheckingContext tc = new TypecheckingContext(null);
- impl.Typecheck(tc);
- label2absy = new Dictionary<int, Absy>();
- 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<int, Absy> label2absy,
- ProverContext proverCtxt,
- out int assertionCount)
- {
- Contract.Requires(startBlock != null);
- Contract.Requires(label2absy != null);
- Contract.Requires(proverCtxt != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();
- List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();
- 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<int, Absy> label2absy,
- Hashtable/*<Block, VCExprVar!>*/ blockVariables,
- List<VCExprLetBinding> 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<VCExpr>() != 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<VCExpr> SuccCorrectVars = new List<VCExpr>(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<Variable> lv,Dictionary<Expr, int> 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<Expr, int> 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<Expr, int> 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<int, Absy> 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<Block> 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<int, Absy>(); // This is only a dummy + m_Evc = new Evc(check); + Dictionary<int, Absy> 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<int, Absy>(); // This is only a dummy + m_Evc = new Evc(check); + Dictionary<int, Absy> 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<Block> 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<Variable> lv,Dictionary<Expr, int> 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<List<Block/*!>!>!*/>> DoomedSequences { + get { + Contract.Ensures(Contract.ForAll(Contract.Result<List<List<Block>>>(), 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<int, Absy> label2absy, Checker ch, out int assertionCount) { + Contract.Requires(impl != null); + Contract.Requires(ch != null); + Contract.Ensures(Contract.Result<VCExpr>() != null); + + TypecheckingContext tc = new TypecheckingContext(null); + impl.Typecheck(tc); + label2absy = new Dictionary<int, Absy>(); + 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<int, Absy> label2absy, + ProverContext proverCtxt, + out int assertionCount) + { + Contract.Requires(startBlock != null); + Contract.Requires(label2absy != null); + Contract.Requires(proverCtxt != null); + Contract.Ensures(Contract.Result<VCExpr>() != null); + + Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/(); + List<VCExprLetBinding> bindings = new List<VCExprLetBinding>(); + 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<int, Absy> label2absy, + Hashtable/*<Block, VCExprVar!>*/ blockVariables, + List<VCExprLetBinding> 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<VCExpr>() != 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<VCExpr> SuccCorrectVars = new List<VCExpr>(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<int, Absy> label2Absy;
- protected VerifierCallback callback;
- private List<Block> m_CurrentTrace = new List<Block>();
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(label2Absy != null);
- Contract.Invariant(callback != null);
- Contract.Invariant(cce.NonNullElements(m_CurrentTrace));
- }
-
-
- public DoomErrorHandler(Dictionary<int, Absy> 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<Absy>() != 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<Block>/*!>!*/ TraceNodes
- {
- get
- {
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
-
- return m_CurrentTrace;
- }
- }
-
- public override void OnModel(IList<string>/*!>!*/ labels, Model model, ProverInterface.Outcome proverOutcome)
- {
- // TODO: it would be better to check which reachability variables are actually set to one!
- List<Block> traceNodes = new List<Block>();
- List<AssertCmd> assertNodes = new List<AssertCmd>();
- 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<int, Absy> label2Absy; + protected VerifierCallback callback; + private List<Block> m_CurrentTrace = new List<Block>(); + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(label2Absy != null); + Contract.Invariant(callback != null); + Contract.Invariant(cce.NonNullElements(m_CurrentTrace)); + } + + + public DoomErrorHandler(Dictionary<int, Absy> 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<Absy>() != 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<Block>/*!>!*/ TraceNodes + { + get + { + Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>())); + + return m_CurrentTrace; + } + } + + public override void OnModel(IList<string>/*!>!*/ labels, Model model, ProverInterface.Outcome proverOutcome) + { + // TODO: it would be better to check which reachability variables are actually set to one! + List<Block> traceNodes = new List<Block>(); + List<AssertCmd> assertNodes = new List<AssertCmd>(); + 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..f055d2c9 100644 --- a/Source/Doomed/Doomed.csproj +++ b/Source/Doomed/Doomed.csproj @@ -1,190 +1,190 @@ -<?xml version="1.0" encoding="utf-8"?>
-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
- <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
- <PropertyGroup>
- <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
- <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
- <ProjectGuid>{884386A3-58E9-40BB-A273-B24976775553}</ProjectGuid>
- <OutputType>Library</OutputType>
- <AppDesignerFolder>Properties</AppDesignerFolder>
- <RootNamespace>Doomed</RootNamespace>
- <AssemblyName>Doomed</AssemblyName>
- <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
- <FileAlignment>512</FileAlignment>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
- <ProductVersion>12.0.0</ProductVersion>
- <SchemaVersion>2.0</SchemaVersion>
- <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <DebugType>full</DebugType>
- <Optimize>false</Optimize>
- <OutputPath>bin\Debug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>True</CodeContractsEnumObligations>
- <CodeContractsRedundantAssumptions>True</CodeContractsRedundantAssumptions>
- <CodeContractsAssertsToContractsCheckBox>True</CodeContractsAssertsToContractsCheckBox>
- <CodeContractsRedundantTests>True</CodeContractsRedundantTests>
- <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
- <CodeContractsMissingPublicEnsuresAsWarnings>False</CodeContractsMissingPublicEnsuresAsWarnings>
- <CodeContractsInferRequires>True</CodeContractsInferRequires>
- <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
- <CodeContractsInferEnsuresAutoProperties>True</CodeContractsInferEnsuresAutoProperties>
- <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
- <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
- <CodeContractsSuggestAssumptionsForCallees>False</CodeContractsSuggestAssumptionsForCallees>
- <CodeContractsSuggestRequires>False</CodeContractsSuggestRequires>
- <CodeContractsNecessaryEnsures>True</CodeContractsNecessaryEnsures>
- <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
- <CodeContractsSuggestReadonly>True</CodeContractsSuggestReadonly>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsSQLServerOption />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
- <CodeContractsSkipAnalysisIfCannotConnectToCache>False</CodeContractsSkipAnalysisIfCannotConnectToCache>
- <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
- <CodeContractsBeingOptimisticOnExternal>True</CodeContractsBeingOptimisticOnExternal>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
- <DebugType>pdbonly</DebugType>
- <Optimize>true</Optimize>
- <OutputPath>bin\Release\</OutputPath>
- <DefineConstants>TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
- <CodeContractsInferRequires>True</CodeContractsInferRequires>
- <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
- <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
- <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
- <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
- <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsSQLServerOption />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
- <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
- </PropertyGroup>
- <PropertyGroup>
- <SignAssembly>true</SignAssembly>
- </PropertyGroup>
- <PropertyGroup>
- <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|AnyCPU'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\QED\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <ItemGroup>
- <Reference Include="System" />
- <Reference Include="System.Core" />
- <Reference Include="System.Xml.Linq" />
- <Reference Include="System.Data.DataSetExtensions" />
- <Reference Include="Microsoft.CSharp" />
- <Reference Include="System.Data" />
- <Reference Include="System.Xml" />
- </ItemGroup>
- <ItemGroup>
- <Compile Include="DoomCheck.cs" />
- <Compile Include="DoomedLoopUnrolling.cs" />
- <Compile Include="DoomedStrategy.cs" />
- <Compile Include="DoomErrorHandler.cs" />
- <Compile Include="HasseDiagram.cs" />
- <Compile Include="VCDoomed.cs" />
- </ItemGroup>
- <ItemGroup>
- <ProjectReference Include="..\Basetypes\Basetypes.csproj">
- <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
- <Name>Basetypes</Name>
- </ProjectReference>
- <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">
- <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
- <Name>CodeContractsExtender</Name>
- </ProjectReference>
- <ProjectReference Include="..\Core\Core.csproj">
- <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
- <Name>Core</Name>
- </ProjectReference>
- <ProjectReference Include="..\Graph\Graph.csproj">
- <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
- <Name>Graph</Name>
- </ProjectReference>
- <ProjectReference Include="..\Model\Model.csproj">
- <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>
- <Name>Model</Name>
- </ProjectReference>
- <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
- <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
- <Name>ParserHelper</Name>
- </ProjectReference>
- <ProjectReference Include="..\VCExpr\VCExpr.csproj">
- <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
- <Name>VCExpr</Name>
- </ProjectReference>
- <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">
- <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
- <Name>VCGeneration</Name>
- </ProjectReference>
- </ItemGroup>
- <ItemGroup>
- <Folder Include="Properties\" />
- </ItemGroup>
- <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
- <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
- Other similar extension points exist, see Microsoft.Common.targets.
- <Target Name="BeforeBuild">
- </Target>
- <Target Name="AfterBuild">
- </Target>
- -->
+<?xml version="1.0" encoding="utf-8"?> +<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> + <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" /> + <PropertyGroup> + <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration> + <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform> + <ProjectGuid>{884386A3-58E9-40BB-A273-B24976775553}</ProjectGuid> + <OutputType>Library</OutputType> + <AppDesignerFolder>Properties</AppDesignerFolder> + <RootNamespace>Doomed</RootNamespace> + <AssemblyName>BoogieDoomed</AssemblyName> + <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> + <FileAlignment>512</FileAlignment> + <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile> + <ProductVersion>12.0.0</ProductVersion> + <SchemaVersion>2.0</SchemaVersion> + <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode> + </PropertyGroup> + <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' "> + <DebugSymbols>true</DebugSymbols> + <DebugType>full</DebugType> + <Optimize>false</Optimize> + <OutputPath>bin\Debug\</OutputPath> + <DefineConstants>DEBUG;TRACE</DefineConstants> + <ErrorReport>prompt</ErrorReport> + <WarningLevel>4</WarningLevel> + <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking> + <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface> + <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure> + <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires> + <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers> + <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis> + <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations> + <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations> + <CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations> + <CodeContractsEnumObligations>True</CodeContractsEnumObligations> + <CodeContractsRedundantAssumptions>True</CodeContractsRedundantAssumptions> + <CodeContractsAssertsToContractsCheckBox>True</CodeContractsAssertsToContractsCheckBox> + <CodeContractsRedundantTests>True</CodeContractsRedundantTests> + <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings> + <CodeContractsMissingPublicEnsuresAsWarnings>False</CodeContractsMissingPublicEnsuresAsWarnings> + <CodeContractsInferRequires>True</CodeContractsInferRequires> + <CodeContractsInferEnsures>False</CodeContractsInferEnsures> + <CodeContractsInferEnsuresAutoProperties>True</CodeContractsInferEnsuresAutoProperties> + <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants> + <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions> + <CodeContractsSuggestAssumptionsForCallees>False</CodeContractsSuggestAssumptionsForCallees> + <CodeContractsSuggestRequires>False</CodeContractsSuggestRequires> + <CodeContractsNecessaryEnsures>True</CodeContractsNecessaryEnsures> + <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants> + <CodeContractsSuggestReadonly>True</CodeContractsSuggestReadonly> + <CodeContractsRunInBackground>True</CodeContractsRunInBackground> + <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies> + <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine> + <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs> + <CodeContractsCustomRewriterAssembly /> + <CodeContractsCustomRewriterClass /> + <CodeContractsLibPaths /> + <CodeContractsExtraRewriteOptions /> + <CodeContractsExtraAnalysisOptions /> + <CodeContractsSQLServerOption /> + <CodeContractsBaseLineFile /> + <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults> + <CodeContractsSkipAnalysisIfCannotConnectToCache>False</CodeContractsSkipAnalysisIfCannotConnectToCache> + <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings> + <CodeContractsBeingOptimisticOnExternal>True</CodeContractsBeingOptimisticOnExternal> + <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel> + <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly> + <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel> + </PropertyGroup> + <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' "> + <DebugType>pdbonly</DebugType> + <Optimize>true</Optimize> + <OutputPath>bin\Release\</OutputPath> + <DefineConstants>TRACE</DefineConstants> + <ErrorReport>prompt</ErrorReport> + <WarningLevel>4</WarningLevel> + <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking> + <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface> + <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure> + <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires> + <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers> + <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis> + <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations> + <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations> + <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations> + <CodeContractsEnumObligations>False</CodeContractsEnumObligations> + <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions> + <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings> + <CodeContractsInferRequires>True</CodeContractsInferRequires> + <CodeContractsInferEnsures>False</CodeContractsInferEnsures> + <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants> + <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions> + <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires> + <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants> + <CodeContractsRunInBackground>True</CodeContractsRunInBackground> + <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies> + <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine> + <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs> + <CodeContractsCustomRewriterAssembly /> + <CodeContractsCustomRewriterClass /> + <CodeContractsLibPaths /> + <CodeContractsExtraRewriteOptions /> + <CodeContractsExtraAnalysisOptions /> + <CodeContractsSQLServerOption /> + <CodeContractsBaseLineFile /> + <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults> + <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings> + <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel> + <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly> + <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel> + </PropertyGroup> + <PropertyGroup> + <SignAssembly>true</SignAssembly> + </PropertyGroup> + <PropertyGroup> + <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile> + </PropertyGroup> + <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|AnyCPU'"> + <DebugSymbols>true</DebugSymbols> + <OutputPath>bin\QED\</OutputPath> + <DefineConstants>DEBUG;TRACE</DefineConstants> + <DebugType>full</DebugType> + <PlatformTarget>AnyCPU</PlatformTarget> + <ErrorReport>prompt</ErrorReport> + <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet> + </PropertyGroup> + <ItemGroup> + <Reference Include="System" /> + <Reference Include="System.Core" /> + <Reference Include="System.Xml.Linq" /> + <Reference Include="System.Data.DataSetExtensions" /> + <Reference Include="Microsoft.CSharp" /> + <Reference Include="System.Data" /> + <Reference Include="System.Xml" /> + </ItemGroup> + <ItemGroup> + <Compile Include="DoomCheck.cs" /> + <Compile Include="DoomedLoopUnrolling.cs" /> + <Compile Include="DoomedStrategy.cs" /> + <Compile Include="DoomErrorHandler.cs" /> + <Compile Include="HasseDiagram.cs" /> + <Compile Include="VCDoomed.cs" /> + </ItemGroup> + <ItemGroup> + <ProjectReference Include="..\Basetypes\Basetypes.csproj"> + <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project> + <Name>Basetypes</Name> + </ProjectReference> + <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj"> + <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project> + <Name>CodeContractsExtender</Name> + </ProjectReference> + <ProjectReference Include="..\Core\Core.csproj"> + <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project> + <Name>Core</Name> + </ProjectReference> + <ProjectReference Include="..\Graph\Graph.csproj"> + <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project> + <Name>Graph</Name> + </ProjectReference> + <ProjectReference Include="..\Model\Model.csproj"> + <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project> + <Name>Model</Name> + </ProjectReference> + <ProjectReference Include="..\ParserHelper\ParserHelper.csproj"> + <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project> + <Name>ParserHelper</Name> + </ProjectReference> + <ProjectReference Include="..\VCExpr\VCExpr.csproj"> + <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project> + <Name>VCExpr</Name> + </ProjectReference> + <ProjectReference Include="..\VCGeneration\VCGeneration.csproj"> + <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project> + <Name>VCGeneration</Name> + </ProjectReference> + </ItemGroup> + <ItemGroup> + <Folder Include="Properties\" /> + </ItemGroup> + <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" /> + <!-- To modify your build process, add your task inside one of the targets below and uncomment it. + Other similar extension points exist, see Microsoft.Common.targets. + <Target Name="BeforeBuild"> + </Target> + <Target Name="AfterBuild"> + </Target> + --> </Project>
\ 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<GraphNode> newsuc = new List<GraphNode>();
- 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<Block> loopblocks = new List<Block>();
- 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<Cmd> cs = new List<Cmd>();
- cs.Add(hcmd); cs.AddRange(b.Cmds);
- b.Cmds = cs;
- }
-
- private HavocCmd m_ComputHavocCmd(List<Block> bl, IToken tok)
- {
- Contract.Requires(bl != null);
- Contract.Requires(tok != null);
- Contract.Ensures(Contract.Result<HavocCmd>() != null);
-
- List<Variable> varsToHavoc = new List<Variable>();
- foreach (Block b in bl)
- {
- Contract.Assert(b != null);
- foreach (Cmd c in b.Cmds)
- {
- Contract.Assert(c != null);
- c.AddAssignedVariables(varsToHavoc);
- }
- }
- List<IdentifierExpr> havocExprs = new List<IdentifierExpr>();
- 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<GraphNode> backupPre = new List<GraphNode>();
- 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<GraphNode> tmp = new List<GraphNode>();
- 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<GraphNode> m_MarkLoopExitUncheckable(GraphNode g, Loop l)
- {
- List<GraphNode> ret = new List<GraphNode>();
-
- 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<GraphNode> le)
- {
- foreach (GraphNode gn in le)
- {
- if (gn.Suc.Count==1) m_GraphAnalyzer.UncheckableNodes.Add(gn);
- }
- }
-
- private void m_RemoveRegularLoopExit(Loop l)
- {
- List<GraphNode> lg = new List<GraphNode>();
- 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<GraphNode> newsuc = new List<GraphNode>();
- 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<GraphNode> UncheckableNodes = new List<GraphNode>();
-
- public Dictionary<Block, GraphNode> GraphMap = new Dictionary<Block, GraphNode>();
-
- public List<Loop> Graphloops = null;
-
- public GraphAnalyzer(List<Block> 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<GraphNode>());
- Graphloops = m_CollectLoops(GraphMap[blocks[0]], null);
-
- }
-
- public List<Block> ToImplementation(out List<Block> uncheckables)
- {
- List<Block> blocks = new List<Block>();
- uncheckables = new List<Block>();
-
- foreach (KeyValuePair<Block, GraphNode> kvp in GraphMap)
- {
- Block b = kvp.Key;
- if (UncheckableNodes.Contains(GraphMap[b])) uncheckables.Add(b);
- blocks.Add(b);
- b.Predecessors = new List<Block>();
- foreach (GraphNode p in kvp.Value.Pre) b.Predecessors.Add(p.Label);
- if (kvp.Value.Suc.Count > 0)
- {
- List<Block> bs = new List<Block>();
- 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<Cmd> cmds = new List<Cmd>(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<Block> affected = new List<Block>();
-
- foreach (KeyValuePair<Block, GraphNode> 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<GraphNode> 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<GraphNode> visited_ = new List<GraphNode>();
- visited_.AddRange(visited);
- visited_.Add(gn);
- foreach (GraphNode next in gn.Suc)
- {
- m_DetectCutPoints(next,gn,visited_);
- }
- }
-
- }
-*/
-
-
- private void m_DetectCutPoints(GraphNode gn)
- {
- List<GraphNode> todo = new List<GraphNode>();
- List<GraphNode> done = new List<GraphNode>();
- 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<GraphNode> _loopbacktracking = new List<GraphNode>();
- private bool m_isLoop(GraphNode loophead, GraphNode gn, List<GraphNode> l1, List<GraphNode> 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<Loop> m_CollectLoops(GraphNode gn, Loop lastLoop)
- {
- List<Loop> ret = new List<Loop>();
- if (gn.Visited) return ret;
- gn.Visited = true;
- List<GraphNode> loopingSucs = new List<GraphNode>();
- 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<GraphNode> Pre = new List<GraphNode>();
- public List<GraphNode> Suc = new List<GraphNode>();
- public bool IsCutpoint;
- public bool Visited = false;
- public List<GraphNode> LoopingPred = new List<GraphNode>();
-
- 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<GraphNode, GraphNode> clonemap = new Dictionary<GraphNode, GraphNode>();
- 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<GraphNode> newl = new List<GraphNode>();
- 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<GraphNode>();
- 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<GraphNode>();
- 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<GraphNode> LoopExitNodes = new List<GraphNode>();
- public List<Loop> NestedLoops = new List<Loop>();
- public List<Loop> SucLoops = new List<Loop>();
- public List<Loop> PreLoops = new List<Loop>();
- public List<GraphNode> LoopNodes = new List<GraphNode>();
- }
- #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<GraphNode> newsuc = new List<GraphNode>(); + 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<Block> loopblocks = new List<Block>(); + 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<Cmd> cs = new List<Cmd>(); + cs.Add(hcmd); cs.AddRange(b.Cmds); + b.Cmds = cs; + } + + private HavocCmd m_ComputHavocCmd(List<Block> bl, IToken tok) + { + Contract.Requires(bl != null); + Contract.Requires(tok != null); + Contract.Ensures(Contract.Result<HavocCmd>() != null); + + List<Variable> varsToHavoc = new List<Variable>(); + foreach (Block b in bl) + { + Contract.Assert(b != null); + foreach (Cmd c in b.Cmds) + { + Contract.Assert(c != null); + c.AddAssignedVariables(varsToHavoc); + } + } + List<IdentifierExpr> havocExprs = new List<IdentifierExpr>(); + 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<GraphNode> backupPre = new List<GraphNode>(); + 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<GraphNode> tmp = new List<GraphNode>(); + 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<GraphNode> m_MarkLoopExitUncheckable(GraphNode g, Loop l) + { + List<GraphNode> ret = new List<GraphNode>(); + + 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<GraphNode> le) + { + foreach (GraphNode gn in le) + { + if (gn.Suc.Count==1) m_GraphAnalyzer.UncheckableNodes.Add(gn); + } + } + + private void m_RemoveRegularLoopExit(Loop l) + { + List<GraphNode> lg = new List<GraphNode>(); + 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<GraphNode> newsuc = new List<GraphNode>(); + 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<GraphNode> UncheckableNodes = new List<GraphNode>(); + + public Dictionary<Block, GraphNode> GraphMap = new Dictionary<Block, GraphNode>(); + + public List<Loop> Graphloops = null; + + public GraphAnalyzer(List<Block> 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<GraphNode>()); + Graphloops = m_CollectLoops(GraphMap[blocks[0]], null); + + } + + public List<Block> ToImplementation(out List<Block> uncheckables) + { + List<Block> blocks = new List<Block>(); + uncheckables = new List<Block>(); + + foreach (KeyValuePair<Block, GraphNode> kvp in GraphMap) + { + Block b = kvp.Key; + if (UncheckableNodes.Contains(GraphMap[b])) uncheckables.Add(b); + blocks.Add(b); + b.Predecessors = new List<Block>(); + foreach (GraphNode p in kvp.Value.Pre) b.Predecessors.Add(p.Label); + if (kvp.Value.Suc.Count > 0) + { + List<Block> bs = new List<Block>(); + 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<Cmd> cmds = new List<Cmd>(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<Block> affected = new List<Block>(); + + foreach (KeyValuePair<Block, GraphNode> 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<GraphNode> 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<GraphNode> visited_ = new List<GraphNode>(); + visited_.AddRange(visited); + visited_.Add(gn); + foreach (GraphNode next in gn.Suc) + { + m_DetectCutPoints(next,gn,visited_); + } + } + + } +*/ + + + private void m_DetectCutPoints(GraphNode gn) + { + List<GraphNode> todo = new List<GraphNode>(); + List<GraphNode> done = new List<GraphNode>(); + 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<GraphNode> _loopbacktracking = new List<GraphNode>(); + private bool m_isLoop(GraphNode loophead, GraphNode gn, List<GraphNode> l1, List<GraphNode> 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<Loop> m_CollectLoops(GraphNode gn, Loop lastLoop) + { + List<Loop> ret = new List<Loop>(); + if (gn.Visited) return ret; + gn.Visited = true; + List<GraphNode> loopingSucs = new List<GraphNode>(); + 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<GraphNode> Pre = new List<GraphNode>(); + public List<GraphNode> Suc = new List<GraphNode>(); + public bool IsCutpoint; + public bool Visited = false; + public List<GraphNode> LoopingPred = new List<GraphNode>(); + + 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<GraphNode, GraphNode> clonemap = new Dictionary<GraphNode, GraphNode>(); + 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<GraphNode> newl = new List<GraphNode>(); + 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<GraphNode>(); + 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<GraphNode>(); + 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<GraphNode> LoopExitNodes = new List<GraphNode>(); + public List<Loop> NestedLoops = new List<Loop>(); + public List<Loop> SucLoops = new List<Loop>(); + public List<Loop> PreLoops = new List<Loop>(); + public List<GraphNode> LoopNodes = new List<GraphNode>(); + } + #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<List<Block/*!*/>/*!*/>/*!*/ DetectedBlock = new List<List<Block/*!*/>/*!*/>();
-
- private List<Block> __DEBUG_minelements = new List<Block>();
-
- // There is no default constructor, because these parameters are needed for most subclasses
- public DoomDetectionStrategy(Implementation imp, Block unifiedexit, List<Block> unreach)
- {
- m_BlockH = new BlockHierachy(imp, unifiedexit);
- __DEBUG_EQCLeaf = m_BlockH.Leaves.Count;
-
- //foreach (BlockHierachyNode bhn in m_BlockH.Leaves)
- //{
- // if (bhn.Content.Count > 0) __DEBUG_minelements.Add(bhn.Content[0]);
- //}
- //if (imp.Blocks.Count>0) m_GatherInfo(imp.Blocks[0], 0, 0,0);
-
-
- if (__DEBUGOUT)
- {
- Console.WriteLine("MaBranchingDepth {0} MaxMinPP {1} ", m_MaxBranchingDepth, m_MaxK);
-
- Console.WriteLine("AvgLeaverPerPath {0} AvgPLen {1}", 0, 0);
- }
-
- MaxBlocks = imp.Blocks.Count;
- MinBlocks = imp.Blocks.Count;
- HACK_NewCheck = false;
- __DEBUG_BlocksTotal = imp.Blocks.Count;
- }
-
- 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<Block> passBlock);
-
- // This method is called to inform about the prover outcome for the previous GetNextBlock call.
- abstract public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb);
-
- protected List<Block> m_GetErrorTraceFromCE(DoomErrorHandler cb)
- {
- BlockHierachyNode tn=null;
- List<Block> errortrace = new List<Block>();
- 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<int> __pathLength = new List<int>();
- private List<int> __leavespp = new List<int>();
- 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<Block> m_Blocks = new List<Block>();
- private int m_Current = 0;
-
- public NoStrategy(Implementation imp, Block unifiedexit, List<Block> unreach)
- : base(imp, unifiedexit, unreach)
- {
- m_Blocks = imp.Blocks;
- }
-
- override public bool GetNextBlock(out List<Block> lb)
- {
- if (m_Current < m_Blocks.Count)
- {
- lb = new List<Block>();
- 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<Variable> 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<Block> lb = new List<Block>();
- 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<Block> m_Blocks = new List<Block>();
- private List<Block> m_doomedBlocks = new List<Block>();
- private int m_Current = 0;
-
- public HierachyStrategy(Implementation imp, Block unifiedexit, List<Block> 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<Block> lb)
- {
- sw.Start();
- if (m_Current < m_Blocks.Count)
- {
- lb = new List<Block>();
- 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<Variable> 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<Block> m_Blocks = new List<Block>();
- private List<Block> m_doomedBlocks = new List<Block>();
- private Block m_Current = null;
-
- public HierachyCEStrategy(Implementation imp, Block unifiedexit, List<Block> 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<Block> lb)
- {
- m_Current = null;
- if (m_Blocks.Count > 0)
- {
- m_Current = m_Blocks[0];
- m_Blocks.Remove(m_Current);
- lb = new List<Block>();
- 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<Variable> 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<Block> 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<Block> m_Uncheckedlocks = new List<Block>();
- List<Block> m_Ignore = new List<Block>();
-
- Random m_Random = new Random();
- bool m_NoMoreMoves = false;
-
- private List<Block> m_foundBlock = new List<Block>();
-
- public PathCoverStrategy(Implementation imp, Block unifiedexit, List<Block> 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<Block> lb)
- {
- sw.Start();
-
- lb = new List<Block>();
-
- 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<Variable> 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<Block> 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<Block> m_Uncheckedlocks = new List<Block>();
- List<Block> m_Ignore = new List<Block>();
-
- Random m_Random = new Random();
- bool m_NoMoreMoves = false;
-
- private List<Block> m_foundBlock = new List<Block>();
-
- public PathCoverStrategyK(Implementation imp, Block unifiedexit, List<Block> 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<Block> lb)
- {
- sw.Start();
-
- lb = new List<Block>();
-
- 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<Variable> 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<Block> 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<List<Block/*!*/>/*!*/>/*!*/ DetectedBlock = new List<List<Block/*!*/>/*!*/>(); + + private List<Block> __DEBUG_minelements = new List<Block>(); + + // There is no default constructor, because these parameters are needed for most subclasses + public DoomDetectionStrategy(Implementation imp, Block unifiedexit, List<Block> unreach) + { + m_BlockH = new BlockHierachy(imp, unifiedexit); + __DEBUG_EQCLeaf = m_BlockH.Leaves.Count; + + //foreach (BlockHierachyNode bhn in m_BlockH.Leaves) + //{ + // if (bhn.Content.Count > 0) __DEBUG_minelements.Add(bhn.Content[0]); + //} + //if (imp.Blocks.Count>0) m_GatherInfo(imp.Blocks[0], 0, 0,0); + + + if (__DEBUGOUT) + { + Console.WriteLine("MaBranchingDepth {0} MaxMinPP {1} ", m_MaxBranchingDepth, m_MaxK); + + Console.WriteLine("AvgLeaverPerPath {0} AvgPLen {1}", 0, 0); + } + + MaxBlocks = imp.Blocks.Count; + MinBlocks = imp.Blocks.Count; + HACK_NewCheck = false; + __DEBUG_BlocksTotal = imp.Blocks.Count; + } + + 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<Block> passBlock); + + // This method is called to inform about the prover outcome for the previous GetNextBlock call. + abstract public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb); + + protected List<Block> m_GetErrorTraceFromCE(DoomErrorHandler cb) + { + BlockHierachyNode tn=null; + List<Block> errortrace = new List<Block>(); + 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<int> __pathLength = new List<int>(); + private List<int> __leavespp = new List<int>(); + 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<Block> m_Blocks = new List<Block>(); + private int m_Current = 0; + + public NoStrategy(Implementation imp, Block unifiedexit, List<Block> unreach) + : base(imp, unifiedexit, unreach) + { + m_Blocks = imp.Blocks; + } + + override public bool GetNextBlock(out List<Block> lb) + { + if (m_Current < m_Blocks.Count) + { + lb = new List<Block>(); + 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<Variable> 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<Block> lb = new List<Block>(); + 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<Block> m_Blocks = new List<Block>(); + private List<Block> m_doomedBlocks = new List<Block>(); + private int m_Current = 0; + + public HierachyStrategy(Implementation imp, Block unifiedexit, List<Block> 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<Block> lb) + { + sw.Start(); + if (m_Current < m_Blocks.Count) + { + lb = new List<Block>(); + 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<Variable> 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<Block> m_Blocks = new List<Block>(); + private List<Block> m_doomedBlocks = new List<Block>(); + private Block m_Current = null; + + public HierachyCEStrategy(Implementation imp, Block unifiedexit, List<Block> 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<Block> lb) + { + m_Current = null; + if (m_Blocks.Count > 0) + { + m_Current = m_Blocks[0]; + m_Blocks.Remove(m_Current); + lb = new List<Block>(); + 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<Variable> 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<Block> 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<Block> m_Uncheckedlocks = new List<Block>(); + List<Block> m_Ignore = new List<Block>(); + + Random m_Random = new Random(); + bool m_NoMoreMoves = false; + + private List<Block> m_foundBlock = new List<Block>(); + + public PathCoverStrategy(Implementation imp, Block unifiedexit, List<Block> 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<Block> lb) + { + sw.Start(); + + lb = new List<Block>(); + + 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<Variable> 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<Block> 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<Block> m_Uncheckedlocks = new List<Block>(); + List<Block> m_Ignore = new List<Block>(); + + Random m_Random = new Random(); + bool m_NoMoreMoves = false; + + private List<Block> m_foundBlock = new List<Block>(); + + public PathCoverStrategyK(Implementation imp, Block unifiedexit, List<Block> 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<Block> lb) + { + sw.Start(); + + lb = new List<Block>(); + + 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<Variable> 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<Block> 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<Block> Unavoidable;
- public List<Block> Content = new List<Block>();
- public List<BlockHierachyNode> Parents = new List<BlockHierachyNode>();
- public List<BlockHierachyNode> Children = new List<BlockHierachyNode>();
-
- public bool Checked, Doomed, DoubleChecked;
-
- public BlockHierachyNode(Block current, List<Block> 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<Block> tmp = new List<Block>();
- 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<BlockHierachyNode> Leaves = new List<BlockHierachyNode>();
- public readonly List<BlockHierachyNode> Roots = new List<BlockHierachyNode>();
-
- public HasseDiagram(List<BlockHierachyNode> nodes)
- {
- Dictionary<BlockHierachyNode, List<BlockHierachyNode>> largerElements = new Dictionary<BlockHierachyNode, List<BlockHierachyNode>>();
- foreach (BlockHierachyNode left in nodes)
- {
- largerElements[left] = new List<BlockHierachyNode>();
- foreach (BlockHierachyNode right in nodes)
- {
- if (left != right)
- {
- if (left < right)
- {
- largerElements[left].Add(right);
- }
- }
- }
- if (largerElements[left].Count == 0) Leaves.Add(left);
- }
-
- List<BlockHierachyNode> done = new List<BlockHierachyNode>();
- List<BlockHierachyNode> lastround = null;
-
- //Debugger.Break();
-
- // Now that we have the leaves, build the Hasse diagram
- while (done.Count < nodes.Count)
- {
- List<BlockHierachyNode> maxelements = new List<BlockHierachyNode>();
- 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<Block, BlockHierachyNode> BlockToHierachyMap = new Dictionary<Block, BlockHierachyNode>();
- readonly public Dictionary<Block, List<Block>> Dominators = new Dictionary<Block, List<Block>>();
- readonly public Dictionary<Block, List<Block>> PostDominators = new Dictionary<Block, List<Block>>();
- readonly public List<BlockHierachyNode> Leaves = new List<BlockHierachyNode>();
-
- private Implementation m_Impl;
-
- public BlockHierachy(Implementation impl, Block unifiedExit)
- {
- m_Impl = impl;
- List<Block> blocks = impl.Blocks;
- List<BlockHierachyNode> tmp_hnodes = new List<BlockHierachyNode>();
- Dictionary<Block, List<Block>> unavoidable = new Dictionary<Block, List<Block>>();
-
- BfsTraverser(blocks[0], true, Dominators);
- BfsTraverser(unifiedExit, false, PostDominators);
-
- foreach (Block b in blocks)
- {
- List<Block> l1 = Dominators[b];
- List<Block> l2 = PostDominators[b];
- unavoidable[b] = m_MergeLists(l1, l2);
-
- BlockHierachyNode bhn = new BlockHierachyNode(b, unavoidable[b]);
- bool found = false;
- foreach (KeyValuePair<Block, BlockHierachyNode> 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<Block> blocks)
- {
- m_GetMaxK(blocks);
- return (m_MaxK>0) ? m_MaxK : 1;
- }
-
- private int m_MaxK = 0;
- private void m_GetMaxK(List<Block> blocks)
- {
- m_MaxK = 0;
- Dictionary<Block, int> kstore = new Dictionary<Block, int>();
- List<Block> todo = new List<Block>();
- List<Block> done = new List<Block>();
- 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<Block> GetOtherDoomedBlocks(List<Block> doomedblocks)
- {
- List<Block> alsoDoomed = new List<Block>();
- List<BlockHierachyNode> todo = new List<BlockHierachyNode>();
- 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<string> nodes = new List<string>();
- List<string> edges = new List<string>();
-
- string nodestyle = "[shape=box];";
-
- List<BlockHierachyNode> nl = new List<BlockHierachyNode>();
- 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<Block, List<Block>> unavoidableBlocks)
- {
- List<Block> todo = new List<Block>();
- List<Block> done = new List<Block>();
- unavoidableBlocks[current] = new List<Block>();
- //Debugger.Break();
- todo.Add(current);
- while (todo.Count > 0)
- {
- current = todo[0];
- todo.Remove(current);
- List<Block> 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<Block> 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<Block>();
- unavoidableBlocks[bsuc].AddRange(unavoidableBlocks[current]);
- }
-
- }
- }
-
- }
-
- private List<Block> m_MergeLists(List<Block> lb1, List<Block> lb2)
- {
- List<Block> ret = new List<Block>();
- ret.AddRange(lb1);
- foreach (Block b in lb2)
- {
- if (!ret.Contains(b)) ret.Add(b);
- }
- return ret;
- }
-
- private List<Block> m_IntersectLists(List<Block> lb1, List<Block> lb2)
- {
- List<Block> ret = new List<Block>();
- 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<Block> 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<Block> 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<Block> Unavoidable; + public List<Block> Content = new List<Block>(); + public List<BlockHierachyNode> Parents = new List<BlockHierachyNode>(); + public List<BlockHierachyNode> Children = new List<BlockHierachyNode>(); + + public bool Checked, Doomed, DoubleChecked; + + public BlockHierachyNode(Block current, List<Block> 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<Block> tmp = new List<Block>(); + 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<BlockHierachyNode> Leaves = new List<BlockHierachyNode>(); + public readonly List<BlockHierachyNode> Roots = new List<BlockHierachyNode>(); + + public HasseDiagram(List<BlockHierachyNode> nodes) + { + Dictionary<BlockHierachyNode, List<BlockHierachyNode>> largerElements = new Dictionary<BlockHierachyNode, List<BlockHierachyNode>>(); + foreach (BlockHierachyNode left in nodes) + { + largerElements[left] = new List<BlockHierachyNode>(); + foreach (BlockHierachyNode right in nodes) + { + if (left != right) + { + if (left < right) + { + largerElements[left].Add(right); + } + } + } + if (largerElements[left].Count == 0) Leaves.Add(left); + } + + List<BlockHierachyNode> done = new List<BlockHierachyNode>(); + List<BlockHierachyNode> lastround = null; + + //Debugger.Break(); + + // Now that we have the leaves, build the Hasse diagram + while (done.Count < nodes.Count) + { + List<BlockHierachyNode> maxelements = new List<BlockHierachyNode>(); + 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<Block, BlockHierachyNode> BlockToHierachyMap = new Dictionary<Block, BlockHierachyNode>(); + readonly public Dictionary<Block, List<Block>> Dominators = new Dictionary<Block, List<Block>>(); + readonly public Dictionary<Block, List<Block>> PostDominators = new Dictionary<Block, List<Block>>(); + readonly public List<BlockHierachyNode> Leaves = new List<BlockHierachyNode>(); + + private Implementation m_Impl; + + public BlockHierachy(Implementation impl, Block unifiedExit) + { + m_Impl = impl; + List<Block> blocks = impl.Blocks; + List<BlockHierachyNode> tmp_hnodes = new List<BlockHierachyNode>(); + Dictionary<Block, List<Block>> unavoidable = new Dictionary<Block, List<Block>>(); + + BfsTraverser(blocks[0], true, Dominators); + BfsTraverser(unifiedExit, false, PostDominators); + + foreach (Block b in blocks) + { + List<Block> l1 = Dominators[b]; + List<Block> l2 = PostDominators[b]; + unavoidable[b] = m_MergeLists(l1, l2); + + BlockHierachyNode bhn = new BlockHierachyNode(b, unavoidable[b]); + bool found = false; + foreach (KeyValuePair<Block, BlockHierachyNode> 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<Block> blocks) + { + m_GetMaxK(blocks); + return (m_MaxK>0) ? m_MaxK : 1; + } + + private int m_MaxK = 0; + private void m_GetMaxK(List<Block> blocks) + { + m_MaxK = 0; + Dictionary<Block, int> kstore = new Dictionary<Block, int>(); + List<Block> todo = new List<Block>(); + List<Block> done = new List<Block>(); + 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<Block> GetOtherDoomedBlocks(List<Block> doomedblocks) + { + List<Block> alsoDoomed = new List<Block>(); + List<BlockHierachyNode> todo = new List<BlockHierachyNode>(); + 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<string> nodes = new List<string>(); + List<string> edges = new List<string>(); + + string nodestyle = "[shape=box];"; + + List<BlockHierachyNode> nl = new List<BlockHierachyNode>(); + 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<Block, List<Block>> unavoidableBlocks) + { + List<Block> todo = new List<Block>(); + List<Block> done = new List<Block>(); + unavoidableBlocks[current] = new List<Block>(); + //Debugger.Break(); + todo.Add(current); + while (todo.Count > 0) + { + current = todo[0]; + todo.Remove(current); + List<Block> 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<Block> 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<Block>(); + unavoidableBlocks[bsuc].AddRange(unavoidableBlocks[current]); + } + + } + } + + } + + private List<Block> m_MergeLists(List<Block> lb1, List<Block> lb2) + { + List<Block> ret = new List<Block>(); + ret.AddRange(lb1); + foreach (Block b in lb2) + { + if (!ret.Contains(b)) ret.Add(b); + } + return ret; + } + + private List<Block> m_IntersectLists(List<Block> lb1, List<Block> lb2) + { + List<Block> ret = new List<Block>(); + 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<Block> 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<Block> 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<Block, Variable/*!*/>/*!*/ m_BlockReachabilityMap;
- Dictionary<Block/*!*/, Block/*!*/>/*!*/ m_copiedBlocks = new Dictionary<Block/*!*/, Block/*!*/>();
- const string reachvarsuffix = "__ivebeenthere";
- List<Cmd/*!*/>/*!*/ m_doomedCmds = new List<Cmd/*!*/>();
- [ContractInvariantMethod]
- void ObjectInvariant() {
-
- }
-
- #endregion
-
-
- /// <summary>
- /// Constructor. Initializes the theorem prover.
- /// </summary>
- public DCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
- : base(program, checkers) {
- Contract.Requires(program != null);
-
- this.appendLogFile = appendLogFile;
- this.logFilePath = logFilePath;
- m_BlockReachabilityMap = new Dictionary<Block, Variable>();
- }
-
- /// <summary>
- /// Debug method that prints a dot file of the
- /// current set of blocks in impl to filename.
- /// </summary>
- private void Impl2Dot(Implementation impl, string filename) {
- Contract.Requires(impl != null);
- Contract.Requires(filename != null);
- List<string> nodes = new List<string>();
- List<string> edges = new List<string>();
-
- string nodestyle = "[shape=box];";
-
- foreach (Block b in impl.Blocks) {
- Contract.Assert(b != null);
- nodes.Add(string.Format("\"{0}\" {1}", b.Label, nodestyle));
- GotoCmd gc = b.TransferCmd as GotoCmd;
- if (gc != null)
- {
- Contract.Assert(gc.labelTargets != null);
- foreach (Block b_ in gc.labelTargets)
- {
- Contract.Assert(b_ != null);
- edges.Add(String.Format("\"{0}\" -> \"{1}\";", b.Label, b_.Label));
- }
- }
-
- //foreach (Block b_ in b.Predecessors)
- //{
- // edges.Add(String.Format("\"{0}\" -> \"{1}\";", b.Label, b_.Label));
- //}
- }
-
- using (StreamWriter sw = new StreamWriter(filename)) {
- sw.WriteLine(String.Format("digraph {0} {{", impl.Name));
- // foreach (string! s in nodes) {
- // sw.WriteLine(s);
- // }
- foreach (string s in edges) {
- Contract.Assert(s != null);
- sw.WriteLine(s);
- }
- sw.WriteLine("}}");
- sw.Close();
- }
- }
- private const string _copyPrefix = "CPY__";
-
- private List<Block> m_UncheckableBlocks = null;
-
- /// <summary>
- /// 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
- ///
- /// </summary>
- public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(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<Block> lb;
- List<Variable> lv = new List<Variable>();
-
- 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<Expr, int> 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<Block> _all = new List<Block>();
- foreach (List<Block> 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<Expr, int> m_GetPostconditionVariables(List<Block> allblock, List<Block> passBlock)
- {
- Dictionary<Expr, int> r = new Dictionary<Expr, int>();
- 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<Block, List<Cmd>> cmdbackup = new Dictionary<Block, List<Cmd>>();
-
- 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<Cmd> causals = CollectCausalStatements(impl.Blocks[0]);
- foreach (Cmd c in causals) {
- Contract.Assert(c != null);
- GenerateErrorMessage(c, causals);
- }
-
- #region Undo all modifications
- foreach (KeyValuePair<Block, List<Cmd>> 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<Cmd> 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>", 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>", 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>", 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>", 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>", Console.Out, false), 0);
- }
- Console.ForegroundColor = col;
- Console.WriteLine("--");
-
- }
- }
-
- private List<Cmd> CollectCausalStatements(Block b) {
- Contract.Requires(b != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<Cmd>>()));
-
- 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<Cmd> causals = new List<Cmd>();
- GotoCmd gc = b.TransferCmd as GotoCmd;
- if (gc != null && gc.labelTargets != null) {
- List<Cmd> 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<Block, List<Cmd>> 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<Cmd> cs = new List<Cmd>();
- 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<Cmd> backup = b.Cmds;
- Contract.Assert(backup != null);
- List<Cmd> cs = new List<Cmd>();
- 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>", 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<Block/*!*/, List<Cmd>/*!*/>/*!*/ cmdbackup,
- int startidx, int endidx) {
- Contract.Requires(cce.NonNullElements(cmdbackup));
- Contract.Requires(impl != null);
- for (int i = startidx; i <= endidx; i++) {
- List<Cmd> 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<Variable> rv = new List<Variable>();
- 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<TransferCmd, ReturnCmd> gotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();
- 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<Cmd> cc = new List<Cmd>();
- // 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<Variable, Expr> PassifyProgram(Implementation impl, ModelViewInfo mvInfo) {
- Contract.Requires(impl != null);
- Contract.Requires(mvInfo != null);
- Contract.Requires(this.exitBlock != null);
- Contract.Ensures(Contract.Result<Hashtable>() != null);
-
- CurrentLocalVariables = impl.LocVars;
- return Convert2PassiveCmd(impl, mvInfo);
- //return new Hashtable();
- }
-
- /// <summary>
- /// Add additional variable to allow checking as described in the paper
- /// "It's doomed; we can prove it"
- /// </summary>
- private List<Cmd> 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<AssignLhs> lhsl = new List<AssignLhs>();
- lhsl.Add(new SimpleAssignLhs(Token.NoToken, lhs));
- List<Expr> rhsl = new List<Expr>();
- rhsl.Add(Expr.Literal(1) );
-
-
- List<Cmd> cs = new List<Cmd> { new AssignCmd(Token.NoToken, lhsl, rhsl) };
- cs.AddRange(b.Cmds);
- b.Cmds = cs;
-
- //checkBlocks.Add(new CheckableBlock(v_,b));
- }
-
- List<Cmd> incReachVars = new List<Cmd>();
- foreach (KeyValuePair<Block, Variable> 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<Variable, Expr> m_LastReachVarIncarnation = new Dictionary<Variable, Expr>();
-
- private void Transform4DoomedCheck(Implementation impl)
- {
- variable2SequenceNumber = new Dictionary<Variable, int>();
- incarnationOriginMap = new Dictionary<Incarnation, Absy>();
- 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<Block> oldblocks = new List<Block>();
- 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<Block, Variable>();
- List<Cmd> cs = GenerateReachabilityPredicates(impl);
-
- //foreach (Block test in getTheFFinalBlock(impl.Blocks[0]))
- //{
- // test.Cmds.AddRange(cs);
- //}
-
- ResetPredecessors(impl.Blocks);
- //EmitImpl(impl,false);
-
- Dictionary<Variable, Expr> var2Expr = PassifyProgram(impl, new ModelViewInfo(program, impl));
-
- // Collect the last incarnation of each reachability variable in the passive program
- foreach (KeyValuePair<Block, Variable> kvp in m_BlockReachabilityMap)
- {
- if (var2Expr.ContainsKey(kvp.Value))
- {
- m_LastReachVarIncarnation[kvp.Value] = (Expr)var2Expr[kvp.Value];
- }
- }
- }
-
-
- List<Block> getTheFFinalBlock(Block b)
- {
- List<Block> lb = new List<Block>();
- 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<Block> DeepCopyBlocks(List<Block> lb, List<Block> uncheckables)
- {
- List<Block> clones = new List<Block>();
- List<Block> uncheck_ = new List<Block>();
- Dictionary<Block, Block> clonemap = new Dictionary<Block, Block>();
-
- 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<Block> newpreds = new List<Block>();
- 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<String> lseq = new List<String>();
- List<Block> bseq = new List<Block>();
- 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<Block, Variable/*!*/>/*!*/ m_BlockReachabilityMap; + Dictionary<Block/*!*/, Block/*!*/>/*!*/ m_copiedBlocks = new Dictionary<Block/*!*/, Block/*!*/>(); + const string reachvarsuffix = "__ivebeenthere"; + List<Cmd/*!*/>/*!*/ m_doomedCmds = new List<Cmd/*!*/>(); + [ContractInvariantMethod] + void ObjectInvariant() { + + } + + #endregion + + + /// <summary> + /// Constructor. Initializes the theorem prover. + /// </summary> + public DCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers) + : base(program, checkers) { + Contract.Requires(program != null); + + this.appendLogFile = appendLogFile; + this.logFilePath = logFilePath; + m_BlockReachabilityMap = new Dictionary<Block, Variable>(); + } + + /// <summary> + /// Debug method that prints a dot file of the + /// current set of blocks in impl to filename. + /// </summary> + private void Impl2Dot(Implementation impl, string filename) { + Contract.Requires(impl != null); + Contract.Requires(filename != null); + List<string> nodes = new List<string>(); + List<string> edges = new List<string>(); + + string nodestyle = "[shape=box];"; + + foreach (Block b in impl.Blocks) { + Contract.Assert(b != null); + nodes.Add(string.Format("\"{0}\" {1}", b.Label, nodestyle)); + GotoCmd gc = b.TransferCmd as GotoCmd; + if (gc != null) + { + Contract.Assert(gc.labelTargets != null); + foreach (Block b_ in gc.labelTargets) + { + Contract.Assert(b_ != null); + edges.Add(String.Format("\"{0}\" -> \"{1}\";", b.Label, b_.Label)); + } + } + + //foreach (Block b_ in b.Predecessors) + //{ + // edges.Add(String.Format("\"{0}\" -> \"{1}\";", b.Label, b_.Label)); + //} + } + + using (StreamWriter sw = new StreamWriter(filename)) { + sw.WriteLine(String.Format("digraph {0} {{", impl.Name)); + // foreach (string! s in nodes) { + // sw.WriteLine(s); + // } + foreach (string s in edges) { + Contract.Assert(s != null); + sw.WriteLine(s); + } + sw.WriteLine("}}"); + sw.Close(); + } + } + private const string _copyPrefix = "CPY__"; + + private List<Block> m_UncheckableBlocks = null; + + /// <summary> + /// 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 + /// + /// </summary> + public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) { + Contract.EnsuresOnThrow<UnexpectedProverOutputException>(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<Block> lb; + List<Variable> lv = new List<Variable>(); + + 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<Expr, int> 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<Block> _all = new List<Block>(); + foreach (List<Block> 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<Expr, int> m_GetPostconditionVariables(List<Block> allblock, List<Block> passBlock) + { + Dictionary<Expr, int> r = new Dictionary<Expr, int>(); + 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<Block, List<Cmd>> cmdbackup = new Dictionary<Block, List<Cmd>>(); + + 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<Cmd> causals = CollectCausalStatements(impl.Blocks[0]); + foreach (Cmd c in causals) { + Contract.Assert(c != null); + GenerateErrorMessage(c, causals); + } + + #region Undo all modifications + foreach (KeyValuePair<Block, List<Cmd>> 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<Cmd> 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>", 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>", 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>", 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>", 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>", Console.Out, false), 0); + } + Console.ForegroundColor = col; + Console.WriteLine("--"); + + } + } + + private List<Cmd> CollectCausalStatements(Block b) { + Contract.Requires(b != null); + Contract.Ensures(cce.NonNullElements(Contract.Result<List<Cmd>>())); + + 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<Cmd> causals = new List<Cmd>(); + GotoCmd gc = b.TransferCmd as GotoCmd; + if (gc != null && gc.labelTargets != null) { + List<Cmd> 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<Block, List<Cmd>> 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<Cmd> cs = new List<Cmd>(); + 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<Cmd> backup = b.Cmds; + Contract.Assert(backup != null); + List<Cmd> cs = new List<Cmd>(); + 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>", 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<Block/*!*/, List<Cmd>/*!*/>/*!*/ cmdbackup, + int startidx, int endidx) { + Contract.Requires(cce.NonNullElements(cmdbackup)); + Contract.Requires(impl != null); + for (int i = startidx; i <= endidx; i++) { + List<Cmd> 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<Variable> rv = new List<Variable>(); + 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<TransferCmd, ReturnCmd> gotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>(); + 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<Cmd> cc = new List<Cmd>(); + // 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<Variable, Expr> PassifyProgram(Implementation impl, ModelViewInfo mvInfo) { + Contract.Requires(impl != null); + Contract.Requires(mvInfo != null); + Contract.Requires(this.exitBlock != null); + Contract.Ensures(Contract.Result<Hashtable>() != null); + + CurrentLocalVariables = impl.LocVars; + return Convert2PassiveCmd(impl, mvInfo); + //return new Hashtable(); + } + + /// <summary> + /// Add additional variable to allow checking as described in the paper + /// "It's doomed; we can prove it" + /// </summary> + private List<Cmd> 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<AssignLhs> lhsl = new List<AssignLhs>(); + lhsl.Add(new SimpleAssignLhs(Token.NoToken, lhs)); + List<Expr> rhsl = new List<Expr>(); + rhsl.Add(Expr.Literal(1) ); + + + List<Cmd> cs = new List<Cmd> { new AssignCmd(Token.NoToken, lhsl, rhsl) }; + cs.AddRange(b.Cmds); + b.Cmds = cs; + + //checkBlocks.Add(new CheckableBlock(v_,b)); + } + + List<Cmd> incReachVars = new List<Cmd>(); + foreach (KeyValuePair<Block, Variable> 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<Variable, Expr> m_LastReachVarIncarnation = new Dictionary<Variable, Expr>(); + + private void Transform4DoomedCheck(Implementation impl) + { + variable2SequenceNumber = new Dictionary<Variable, int>(); + incarnationOriginMap = new Dictionary<Incarnation, Absy>(); + 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<Block> oldblocks = new List<Block>(); + 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<Block, Variable>(); + List<Cmd> cs = GenerateReachabilityPredicates(impl); + + //foreach (Block test in getTheFFinalBlock(impl.Blocks[0])) + //{ + // test.Cmds.AddRange(cs); + //} + + ResetPredecessors(impl.Blocks); + //EmitImpl(impl,false); + + Dictionary<Variable, Expr> var2Expr = PassifyProgram(impl, new ModelViewInfo(program, impl)); + + // Collect the last incarnation of each reachability variable in the passive program + foreach (KeyValuePair<Block, Variable> kvp in m_BlockReachabilityMap) + { + if (var2Expr.ContainsKey(kvp.Value)) + { + m_LastReachVarIncarnation[kvp.Value] = (Expr)var2Expr[kvp.Value]; + } + } + } + + + List<Block> getTheFFinalBlock(Block b) + { + List<Block> lb = new List<Block>(); + 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<Block> DeepCopyBlocks(List<Block> lb, List<Block> uncheckables) + { + List<Block> clones = new List<Block>(); + List<Block> uncheck_ = new List<Block>(); + Dictionary<Block, Block> clonemap = new Dictionary<Block, Block>(); + + 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<Block> newpreds = new List<Block>(); + 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<String> lseq = new List<String>(); + List<Block> bseq = new List<Block>(); + 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 + } +} |