diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2012-10-03 12:32:19 -0700 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2012-10-03 12:32:19 -0700 |
| commit | 8d7686cd88736d117e37eb9bf9dd17404a294ff4 (patch) | |
| tree | 2d642b239ae7afcc7fb73fdda2881b6cbd008b64 /Source/Doomed/VCDoomed.cs | |
| parent | 2232875cd561e0ffe412cdb5cb5acd05b1ef2a3a (diff) | |
bunch of refactorings
- moved doomed and predication code into separate projects;
for doomed there is a static dependency from BoogieDriver
but for predication even that dependency has been eliminated
- deleted Provers\Simplify and Provers\Z3
- removed Provers\Z3api from the solution
- consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs
Diffstat (limited to 'Source/Doomed/VCDoomed.cs')
| -rw-r--r-- | Source/Doomed/VCDoomed.cs | 827 |
1 files changed, 827 insertions, 0 deletions
diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs new file mode 100644 index 00000000..fadb2ea7 --- /dev/null +++ b/Source/Doomed/VCDoomed.cs @@ -0,0 +1,827 @@ +//-----------------------------------------------------------------------------
+//
+// 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)
+ : base(program) {
+ 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(impl, 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(impl, 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, CmdSeq> cmdbackup = new Dictionary<Block, CmdSeq>();
+
+ 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, CmdSeq> 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, CmdSeq> 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;
+ CmdSeq cs = new CmdSeq();
+ 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
+ CmdSeq backup = b.Cmds;
+ Contract.Assert(backup != null);
+ CmdSeq cs = new CmdSeq();
+ 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/*!*/, CmdSeq/*!*/>/*!*/ cmdbackup,
+ int startidx, int endidx) {
+ Contract.Requires(cce.NonNullElements(cmdbackup));
+ Contract.Requires(impl != null);
+ for (int i = startidx; i <= endidx; i++) {
+ CmdSeq 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);
+ Hashtable gotoCmdOrigins = new Hashtable();
+ 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
+ {
+ CmdSeq cc = new CmdSeq();
+ // where clauses of global variables
+ foreach (Declaration d in program.TopLevelDeclarations) {
+ GlobalVariable gvar = d as GlobalVariable;
+ if (gvar != null && 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
+ exitBlock = InjectPostConditions(impl, exitBlock, gotoCmdOrigins);
+ }
+ #endregion
+ }
+
+
+ private Hashtable/*TransferCmd->ReturnCmd*/ 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 CmdSeq 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) );
+
+
+ CmdSeq cs = new CmdSeq(new AssignCmd(Token.NoToken, lhsl, rhsl));
+ cs.AddRange(b.Cmds);
+ b.Cmds = cs;
+
+ //checkBlocks.Add(new CheckableBlock(v_,b));
+ }
+
+ CmdSeq incReachVars = new CmdSeq();
+ 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 Hashtable/*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>();
+ CmdSeq cs = GenerateReachabilityPredicates(impl);
+
+ //foreach (Block test in getTheFFinalBlock(impl.Blocks[0]))
+ //{
+ // test.Cmds.AddRange(cs);
+ //}
+
+ ResetPredecessors(impl.Blocks);
+ //EmitImpl(impl,false);
+
+ Hashtable/*Variable->Expr*/ htbl = 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 (htbl.ContainsKey(kvp.Value))
+ {
+ m_LastReachVarIncarnation[kvp.Value] = (Expr)htbl[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)
+ {
+ BlockSeq newpreds = new BlockSeq();
+ 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)
+ {
+ StringSeq lseq = new StringSeq();
+ BlockSeq bseq = new BlockSeq();
+ 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
+ }
+}
|