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 | |
| 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')
| -rw-r--r-- | Source/Doomed/DoomCheck.cs | 401 | ||||
| -rw-r--r-- | Source/Doomed/DoomErrorHandler.cs | 86 | ||||
| -rw-r--r-- | Source/Doomed/Doomed.csproj | 102 | ||||
| -rw-r--r-- | Source/Doomed/DoomedLoopUnrolling.cs | 650 | ||||
| -rw-r--r-- | Source/Doomed/DoomedStrategy.cs | 528 | ||||
| -rw-r--r-- | Source/Doomed/HasseDiagram.cs | 424 | ||||
| -rw-r--r-- | Source/Doomed/VCDoomed.cs | 827 |
7 files changed, 3018 insertions, 0 deletions
diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs new file mode 100644 index 00000000..1cbbeabf --- /dev/null +++ b/Source/Doomed/DoomCheck.cs @@ -0,0 +1,401 @@ +//-----------------------------------------------------------------------------
+//
+// 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);
+ m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);
+ m_Checker.ProverDone.WaitOne();
+
+ try {
+ 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;
+ }
+ 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 Hashtable 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 Hashtable(); // This is only a dummy
+ m_Evc = new Evc(check);
+ Hashtable 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 Hashtable(); // This is only a dummy
+ m_Evc = new Evc(check);
+ Hashtable 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 Hashtable 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 Hashtable/*<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,
+ Hashtable/*<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,
+ Hashtable/*<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.Length);
+ 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 new file mode 100644 index 00000000..33d8b68e --- /dev/null +++ b/Source/Doomed/DoomErrorHandler.cs @@ -0,0 +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 Hashtable 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(Hashtable 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)
+ {
+ // 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 new file mode 100644 index 00000000..fb64b247 --- /dev/null +++ b/Source/Doomed/Doomed.csproj @@ -0,0 +1,102 @@ +<?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>Client</TargetFrameworkProfile>
+ </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>
+ </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>
+ </PropertyGroup>
+ <PropertyGroup>
+ <SignAssembly>true</SignAssembly>
+ </PropertyGroup>
+ <PropertyGroup>
+ <AssemblyOriginatorKeyFile>InterimKey.snk</AssemblyOriginatorKeyFile>
+ </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="Properties\AssemblyInfo.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>
+ <None Include="InterimKey.snk" />
+ </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 new file mode 100644 index 00000000..e65a570a --- /dev/null +++ b/Source/Doomed/DoomedLoopUnrolling.cs @@ -0,0 +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)
+ {
+ CmdSeq cs = new CmdSeq();
+ 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);
+
+ VariableSeq varsToHavoc = new VariableSeq();
+ foreach (Block b in bl)
+ {
+ Contract.Assert(b != null);
+ foreach (Cmd c in b.Cmds)
+ {
+ Contract.Assert(c != null);
+ c.AddAssignedVariables(varsToHavoc);
+ }
+ }
+ IdentifierExprSeq havocExprs = new IdentifierExprSeq();
+ foreach (Variable v in varsToHavoc)
+ {
+ Contract.Assert(v != null);
+ IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
+ if (!havocExprs.Has(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 BlockSeq();
+ foreach (GraphNode p in kvp.Value.Pre) b.Predecessors.Add(p.Label);
+ if (kvp.Value.Suc.Count > 0)
+ {
+ BlockSeq bs = new BlockSeq();
+ 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)
+ {
+ CmdSeq cmds = new CmdSeq(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 new file mode 100644 index 00000000..eb5716bb --- /dev/null +++ b/Source/Doomed/DoomedStrategy.cs @@ -0,0 +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.Length > 1) branchingdepth--;
+
+ GotoCmd gc = b.TransferCmd as GotoCmd;
+ if (__DEBUG_minelements.Contains(b)) leavespp++;
+ plen++;
+ if (gc != null && gc.labelTargets.Length>0)
+ {
+ if (gc.labelTargets.Length > 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 new file mode 100644 index 00000000..b2ece2df --- /dev/null +++ b/Source/Doomed/HasseDiagram.cs @@ -0,0 +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);
+ BlockSeq 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);
+
+ BlockSeq 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 BlockSeq 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 BlockSeq 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 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
+ }
+}
|