summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2012-10-03 12:32:19 -0700
committerGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2012-10-03 12:32:19 -0700
commit8d7686cd88736d117e37eb9bf9dd17404a294ff4 (patch)
tree2d642b239ae7afcc7fb73fdda2881b6cbd008b64
parent2232875cd561e0ffe412cdb5cb5acd05b1ef2a3a (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
-rw-r--r--Source/Boogie.sln81
-rw-r--r--Source/BoogieDriver/BoogieDriver.cs11
-rw-r--r--Source/BoogieDriver/BoogieDriver.csproj8
-rw-r--r--Source/Core/Absy.cs2
-rw-r--r--Source/Core/CommandLineOptions.cs5
-rw-r--r--Source/Core/Core.csproj1
-rw-r--r--Source/Core/DeadVarElim.cs4
-rw-r--r--Source/Core/GraphAlgorithms.cs244
-rw-r--r--Source/Core/LoopUnroll.cs1
-rw-r--r--Source/DafnyDriver/DafnyDriver.cs8
-rw-r--r--Source/Doomed/DoomCheck.cs (renamed from Source/VCGeneration/DoomCheck.cs)2
-rw-r--r--Source/Doomed/DoomErrorHandler.cs (renamed from Source/VCGeneration/DoomErrorHandler.cs)2
-rw-r--r--Source/Doomed/Doomed.csproj102
-rw-r--r--Source/Doomed/DoomedLoopUnrolling.cs (renamed from Source/VCGeneration/DoomedLoopUnrolling.cs)2
-rw-r--r--Source/Doomed/DoomedStrategy.cs (renamed from Source/VCGeneration/DoomedStrategy.cs)2
-rw-r--r--Source/Doomed/HasseDiagram.cs (renamed from Source/VCGeneration/HasseDiagram.cs)2
-rw-r--r--Source/Doomed/VCDoomed.cs (renamed from Source/VCGeneration/VCDoomed.cs)2
-rw-r--r--Source/Graph/Graph.cs419
-rw-r--r--Source/Houdini/Houdini.cs2
-rw-r--r--Source/Predication/BlockPredicator.cs (renamed from Source/VCGeneration/BlockPredicator.cs)2
-rw-r--r--Source/Predication/Predication.csproj87
-rw-r--r--Source/Predication/SmartBlockPredicator.cs (renamed from Source/VCGeneration/SmartBlockPredicator.cs)1044
-rw-r--r--Source/Predication/UniformityAnalyser.cs (renamed from Source/VCGeneration/UniformityAnalyser.cs)1055
-rw-r--r--Source/Provers/Simplify/Let2ImpliesVisitor.cs236
-rw-r--r--Source/Provers/Simplify/Prover.cs656
-rw-r--r--Source/Provers/Simplify/ProverInterface.cs868
-rw-r--r--Source/Provers/Simplify/Simplify.csproj210
-rw-r--r--Source/Provers/Simplify/cce.cs193
-rw-r--r--Source/Provers/Z3/Inspector.cs162
-rw-r--r--Source/Provers/Z3/Prover.cs937
-rw-r--r--Source/Provers/Z3/ProverInterface.cs427
-rw-r--r--Source/Provers/Z3/TypeDeclCollector.cs398
-rw-r--r--Source/Provers/Z3/Z3.csproj218
-rw-r--r--Source/Provers/Z3/cce.cs193
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs2
-rw-r--r--Source/VCGeneration/GraphAlgorithms.cs127
-rw-r--r--Source/VCGeneration/StratifiedVC.cs2
-rw-r--r--Source/VCGeneration/VC.cs38
-rw-r--r--Source/VCGeneration/VCGeneration.csproj10
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs6
40 files changed, 1753 insertions, 6018 deletions
diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index 106a9b74..f3f068d7 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -1,6 +1,6 @@

-Microsoft Visual Studio Solution File, Format Version 11.00
-# Visual Studio 2010
+Microsoft Visual Studio Solution File, Format Version 12.00
+# Visual Studio 2012
Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Provers", "Provers", "{B758C1E3-824A-439F-AA2F-0BA1143E8C8D}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BoogieDriver", "BoogieDriver\BoogieDriver.csproj", "{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}"
@@ -15,8 +15,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "VCExpr\VCExpr.csp
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Core", "Core\Core.csproj", "{B230A69C-C466-4065-B9C1-84D80E76D802}"
EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Z3api", "Provers\Z3api\Z3api.csproj", "{966DD87B-A29D-4F3C-9406-F680A61DC0E0}"
-EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "Graph\Graph.csproj", "{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Basetypes", "Basetypes\Basetypes.csproj", "{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}"
@@ -31,6 +29,10 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ParserHelper", "ParserHelpe
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "Houdini\Houdini.csproj", "{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}"
EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Predication", "Predication\Predication.csproj", "{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Doomed", "Doomed\Doomed.csproj", "{884386A3-58E9-40BB-A273-B24976775553}"
+EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Checked|.NET = Checked|.NET
@@ -205,28 +207,6 @@ Global
{B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
{B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Checked|.NET.ActiveCfg = Checked|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Checked|Any CPU.Build.0 = Checked|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Checked|x86.ActiveCfg = Checked|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|x86.ActiveCfg = Debug|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|.NET.ActiveCfg = Release|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|Any CPU.Build.0 = Release|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|x86.ActiveCfg = Release|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|Mixed Platforms.ActiveCfg = z3apidebug|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|Mixed Platforms.Build.0 = z3apidebug|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Checked|.NET.ActiveCfg = Checked|Any CPU
{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -401,12 +381,59 @@ Global
{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|x86.ActiveCfg = Release|Any CPU
{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|x86.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|.NET.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Any CPU.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Any CPU.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|x86.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|.NET.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Any CPU.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|x86.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|x86.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|.NET.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|Any CPU.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|Any CPU.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|x86.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|.NET.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|Any CPU.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|x86.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|x86.ActiveCfg = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
EndGlobalSection
GlobalSection(NestedProjects) = preSolution
{9B163AA3-36BC-4AFB-88AB-79BC9E97E401} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
- {966DD87B-A29D-4F3C-9406-F680A61DC0E0} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
EndGlobalSection
EndGlobal
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 75ba7372..402b5c68 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -594,15 +594,6 @@ namespace Microsoft.Boogie {
program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);
}
- if (CommandLineOptions.Clo.DoPredication && CommandLineOptions.Clo.StratifiedInlining > 0) {
- BlockPredicator.Predicate(program, false, false);
- if (CommandLineOptions.Clo.PrintInstrumented) {
- using (TokenTextWriter writer = new TokenTextWriter(Console.Out)) {
- program.Emit(writer);
- }
- }
- }
-
Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo = null;
if (CommandLineOptions.Clo.ExtractLoops)
{
@@ -668,7 +659,7 @@ namespace Microsoft.Boogie {
try {
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
- } else if(CommandLineOptions.Clo.StratifiedInlining > 0) {
+ } else if (CommandLineOptions.Clo.StratifiedInlining > 0) {
vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
} else {
vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index 9edd2df7..36795a68 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -226,6 +226,10 @@
<Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
<Name>Core</Name>
</ProjectReference>
+ <ProjectReference Include="..\Doomed\Doomed.csproj">
+ <Project>{884386a3-58e9-40bb-a273-b24976775553}</Project>
+ <Name>Doomed</Name>
+ </ProjectReference>
<ProjectReference Include="..\Graph\Graph.csproj">
<Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
<Name>Graph</Name>
@@ -238,6 +242,10 @@
<Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
<Name>ParserHelper</Name>
</ProjectReference>
+ <ProjectReference Include="..\Predication\Predication.csproj">
+ <Project>{afaa5ce1-c41b-44f0-88f8-fd8a43826d44}</Project>
+ <Name>Predication</Name>
+ </ProjectReference>
<ProjectReference Include="..\Provers\SMTLib\SMTLib.csproj">
<Project>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</Project>
<Name>SMTLib</Name>
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index b64a9e5e..c8c052b7 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -77,7 +77,7 @@ namespace Microsoft.Boogie {
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using Microsoft.Boogie.AbstractInterpretation;
- using Graphing;
+ using Microsoft.Boogie.GraphUtil;
using Set = GSet<object>;
[ContractClass(typeof(AbsyContracts))]
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 8b567edd..4192259d 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -575,8 +575,6 @@ namespace Microsoft.Boogie {
public string CoverageReporterPath = null;
public Process coverageReporter = null; // used internally for debugging
- public bool DoPredication = false;
-
public enum TypeEncoding {
None,
Predicates,
@@ -1203,8 +1201,7 @@ namespace Microsoft.Boogie {
ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||
ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||
ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
- ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||
- ps.CheckBooleanFlag("predicate", ref DoPredication)
+ ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops)
) {
// one of the boolean flags matched
return true;
diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index 3a2f421a..49639822 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -155,7 +155,6 @@
<Compile Include="CommandLineOptions.cs" />
<Compile Include="DeadVarElim.cs" />
<Compile Include="Duplicator.cs" />
- <Compile Include="GraphAlgorithms.cs" />
<Compile Include="Inline.cs" />
<Compile Include="LambdaHelper.cs" />
<Compile Include="LoopUnroll.cs" />
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 1376245a..5bf306b6 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -1,6 +1,6 @@
using System;
using System.Collections.Generic;
-using Graphing;
+using Microsoft.Boogie.GraphUtil;
using PureCollections;
using System.Diagnostics.Contracts;
@@ -355,7 +355,7 @@ namespace Microsoft.Boogie {
public static void ComputeLiveVariables(Implementation impl) {
Contract.Requires(impl != null);
Microsoft.Boogie.Helpers.ExtraTraceInformation("Starting live variable analysis");
- Graphing.Graph<Block> dag = new Graph<Block>();
+ Graph<Block> dag = new Graph<Block>();
dag.AddSource(cce.NonNull(impl.Blocks[0])); // there is always at least one node in the graph
foreach (Block b in impl.Blocks) {
GotoCmd gtc = b.TransferCmd as GotoCmd;
diff --git a/Source/Core/GraphAlgorithms.cs b/Source/Core/GraphAlgorithms.cs
deleted file mode 100644
index a19cf96c..00000000
--- a/Source/Core/GraphAlgorithms.cs
+++ /dev/null
@@ -1,244 +0,0 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-
-namespace Microsoft.Boogie {
- public delegate System.Collections.IEnumerable/*<Node!>*//*!*/ Adjacency<T>(T/*!*/ node);
-
-
- // An SCC is a set of nodes
- public sealed class SCC<Node> : ICollection<Node> {
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(nodesMap != null);
- }
-
- private IDictionary<Node, object>/*!*/ nodesMap = new Dictionary<Node, object>();
- private ICollection<Node>/*!*/ nodes {
- get {
- return cce.NonNull(nodesMap.Keys);
- }
- }
-
- [Pure]
- [GlobalAccess(false)]
- [Escapes(true, false)]
- System.Collections.IEnumerator/*!*/ System.Collections.IEnumerable.GetEnumerator() {
- Contract.Ensures(Contract.Result<System.Collections.IEnumerator>() != null);
-
- return ((System.Collections.IEnumerable)nodes).GetEnumerator();
- }
-
- [Pure]
- [GlobalAccess(false)]
- [Escapes(true, false)]
- IEnumerator<Node>/*!*/ IEnumerable<Node>.GetEnumerator() {
- Contract.Ensures(Contract.Result<IEnumerator<Node>>() != null);
-
- return ((IEnumerable<Node>)nodes).GetEnumerator();
- }
-
- public int Count {
- get {
- return nodes.Count;
- }
- }
- public bool IsReadOnly {
- get {
- return nodesMap.IsReadOnly;
- }
- }
- public void Add(Node item) {
- nodesMap.Add(item, null);
- }
- public void Clear() {
- nodesMap.Clear();
- }
- [Pure]
- public bool Contains(Node item) {
- return nodesMap.ContainsKey(item);
- }
- public void CopyTo(Node[] array, int arrayIndex) {
- //Contract.Requires(array != null);
- nodes.CopyTo(array, arrayIndex);
- }
- public bool Remove(Node item) {
- return nodesMap.Remove(item);
- }
- }
-
- public sealed class StronglyConnectedComponents<Node> : IEnumerable<SCC<Node>/*!*/> where Node : class {
- private readonly IDictionary<Node/*!*/, object>/*!*/ graph;
- [ContractInvariantMethod]
- void graphInvariantMethod() {
- Contract.Invariant(Contract.ForAll(graph, entry => entry.Key != null));
- Contract.Invariant(preds != null);
- Contract.Invariant(succs != null);
- }
- private readonly Adjacency<Node>/*!*/ preds;
- private readonly Adjacency<Node>/*!*/ succs;
-
- private bool computed = false;
- public bool Computed {
- get {
- return computed;
- }
- }
-
- [NotDelayed]
- public StronglyConnectedComponents(System.Collections.IEnumerable/*<Node!>*/ graph, Adjacency<Node> preds, Adjacency<Node> succs)
- : base() {//BASEMOVE DANGER
- Contract.Requires(succs != null);
- Contract.Requires(preds != null);
- Contract.Requires(graph != null);
- Contract.Ensures(!Computed);
- IDictionary<Node/*!*/, object>/*!*/ dict = new Dictionary<Node/*!*/, object>();
- foreach (Node/*!*/ n in graph) {
- Contract.Assert(n != null);
- dict.Add(n, null);
- }
-
- this.graph = dict;
- this.preds = preds;
- this.succs = succs;
- //:base();
- }
-
- [Pure]
- [GlobalAccess(false)]
- [Escapes(true, false)]
- System.Collections.IEnumerator/*!*/ System.Collections.IEnumerable.GetEnumerator() {
- Contract.Ensures(Contract.Result<System.Collections.IEnumerator>() != null);
-
- return ((System.Collections.IEnumerable)sccs).GetEnumerator();
- }
-
- [Pure]
- [GlobalAccess(false)]
- [Escapes(true, false)]
- IEnumerator<SCC<Node>/*!*/>/*!*/ IEnumerable<SCC<Node>/*!*/>.GetEnumerator() {
- Contract.Ensures(Contract.Result<IEnumerator<SCC<Node>>>() != null);
-
- Contract.Assume(Computed);
- Contract.Assert(cce.NonNullElements((IEnumerable<SCC<Node>/*!*/>)sccs));//REVIEW
- return ((IEnumerable<SCC<Node>/*!*/>)sccs).GetEnumerator();
- }
-
- private readonly IList<SCC<Node>/*!*/>/*!*/ sccs = new List<SCC<Node>/*!*/>();
- [ContractInvariantMethod]
- void sccsInvariant() {
- Contract.Invariant(cce.NonNullElements(sccs));
- }
-
-
- public void Compute() {
- Contract.Requires(!Computed);
- Contract.Ensures(Computed);
- // Compute post times on graph with edges reversed
- this.dfsNext = this.preds;
- foreach (Node/*!*/ n in cce.NonNull(graph.Keys)) {
- Contract.Assert(n != null);
- if (!seen.ContainsKey(n)) {
- OrderNodes(n);
- }
- }
-
- // Clear seen
- seen.Clear();
-
- // Compute SCCs
- this.dfsNext = this.succs;
- while (postOrder.Count > 0) {
- Node/*!*/ n = postOrder.Pop();
- Contract.Assert(n != null);
-
- if (!seen.ContainsKey(n)) {
- SCC<Node>/*!*/ curr = new SCC<Node>();
- FindSCCs(n, curr);
- sccs.Add(curr);
- }
- }
-
- // Clear seen
- seen.Clear();
-
- this.computed = true;
- }
-
- private Adjacency<Node>/*?*/ dfsNext = null;
-
- private readonly IDictionary<Node/*!*/, object>/*!*/ seen = new Dictionary<Node/*!*/, object>();
- private readonly Stack<Node/*!*/>/*!*/ postOrder = new Stack<Node/*!*/>();
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(seen != null);
- Contract.Invariant(cce.NonNullElements(postOrder));
- }
-
-
- // DFS to order nodes by post times
- private void OrderNodes(Node node) {
- Contract.Requires(node != null);
- seen.Add(node, null);
-
- Contract.Assert(dfsNext != null);
- System.Collections.IEnumerable/*!*/ nexts = dfsNext(node);
- Contract.Assert(nexts != null);
- foreach (Node/*!*/ n in nexts) {
- Contract.Assert(n != null);
- if (graph.ContainsKey(n) && !seen.ContainsKey(n)) {
- OrderNodes(n);
- }
- }
-
- postOrder.Push(node);
- }
-
- // DFS to compute SCCs
- private void FindSCCs(Node node, SCC<Node> currSCC) {
- Contract.Requires(currSCC != null);
- Contract.Requires(node != null);
- //modifies currSCC.*;
- seen.Add(node, null);
- currSCC.Add(node);
-
- Contract.Assert(dfsNext != null);
- System.Collections.IEnumerable/*!*/ nexts = dfsNext(node);
- Contract.Assert(nexts != null);
- foreach (Node/*!*/ n in nexts) {
- Contract.Assert(n != null);
- if (graph.ContainsKey(n) && !seen.ContainsKey(n)) {
- FindSCCs(n, currSCC);
- }
- }
- }
-
- [Pure]
- public override string ToString() {
- Contract.Ensures(Contract.Result<string>() != null);
- string outStr = "";
- int i = 0;
-
- foreach (ICollection<Node> component in this) {
- string/*!*/ tmp = System.String.Format("\nComponent #{0} = ", i++);
- Contract.Assert(tmp != null);
- outStr += tmp;
-
- bool firstInRow = true;
-
- foreach (Node b in component) {
- string/*!*/ tmpComponent = System.String.Format("{0}{1}", firstInRow ? "" : ", ", b);
- Contract.Assert(tmpComponent != null);
- outStr += tmpComponent;
- firstInRow = false;
- }
- }
- return outStr;
- }
-
- }
-}
diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs
index 3b61ad3e..580cbdc5 100644
--- a/Source/Core/LoopUnroll.cs
+++ b/Source/Core/LoopUnroll.cs
@@ -6,6 +6,7 @@
using System.Diagnostics.Contracts;
using System.Collections.Generic;
using Bpl = Microsoft.Boogie;
+using Microsoft.Boogie.GraphUtil;
namespace Microsoft.Boogie {
public class LoopUnroll {
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 39733c8e..80f78d16 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -571,13 +571,7 @@ namespace Microsoft.Dafny
ConditionGeneration vcgen = null;
try
{
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
- {
- vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
- } else
- {
- vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
- }
+ vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
}
catch (ProverException e)
{
diff --git a/Source/VCGeneration/DoomCheck.cs b/Source/Doomed/DoomCheck.cs
index d7e297cd..1cbbeabf 100644
--- a/Source/VCGeneration/DoomCheck.cs
+++ b/Source/Doomed/DoomCheck.cs
@@ -11,7 +11,7 @@ using System.Diagnostics;
using System.Threading;
using System.IO;
using Microsoft.Boogie;
-using Graphing;
+using Microsoft.Boogie.GraphUtil;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
diff --git a/Source/VCGeneration/DoomErrorHandler.cs b/Source/Doomed/DoomErrorHandler.cs
index 5f00a3cf..33d8b68e 100644
--- a/Source/VCGeneration/DoomErrorHandler.cs
+++ b/Source/Doomed/DoomErrorHandler.cs
@@ -5,7 +5,7 @@ using System.Diagnostics;
using System.Threading;
using System.IO;
using Microsoft.Boogie;
-using Graphing;
+using Microsoft.Boogie.GraphUtil;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
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/VCGeneration/DoomedLoopUnrolling.cs b/Source/Doomed/DoomedLoopUnrolling.cs
index 5469a1db..e65a570a 100644
--- a/Source/VCGeneration/DoomedLoopUnrolling.cs
+++ b/Source/Doomed/DoomedLoopUnrolling.cs
@@ -5,7 +5,7 @@ using System.Diagnostics;
using System.Threading;
using System.IO;
using Microsoft.Boogie;
-using Graphing;
+using Microsoft.Boogie.GraphUtil;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
diff --git a/Source/VCGeneration/DoomedStrategy.cs b/Source/Doomed/DoomedStrategy.cs
index c08662b1..eb5716bb 100644
--- a/Source/VCGeneration/DoomedStrategy.cs
+++ b/Source/Doomed/DoomedStrategy.cs
@@ -10,7 +10,7 @@ using System.Diagnostics;
using System.Threading;
using System.IO;
using Microsoft.Boogie;
-using Graphing;
+using Microsoft.Boogie.GraphUtil;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
diff --git a/Source/VCGeneration/HasseDiagram.cs b/Source/Doomed/HasseDiagram.cs
index d5fdfb66..b2ece2df 100644
--- a/Source/VCGeneration/HasseDiagram.cs
+++ b/Source/Doomed/HasseDiagram.cs
@@ -10,7 +10,7 @@ using System.Diagnostics;
using System.Threading;
using System.IO;
using Microsoft.Boogie;
-using Graphing;
+using Microsoft.Boogie.GraphUtil;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/Doomed/VCDoomed.cs
index 962f9f26..fadb2ea7 100644
--- a/Source/VCGeneration/VCDoomed.cs
+++ b/Source/Doomed/VCDoomed.cs
@@ -10,7 +10,7 @@ using System.Diagnostics;
using System.Threading;
using System.IO;
using Microsoft.Boogie;
-using Graphing;
+using Microsoft.Boogie.GraphUtil;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs
index 2d2eb90b..947a5882 100644
--- a/Source/Graph/Graph.cs
+++ b/Source/Graph/Graph.cs
@@ -3,11 +3,12 @@
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
-using System;
+using System;
+using System.Linq;
using System.Collections.Generic;
using System.Text; // for StringBuilder
using System.Diagnostics.Contracts;
-namespace Graphing {
+namespace Microsoft.Boogie.GraphUtil {
internal static class Util {
private static string/*!*/ ListToString<T>(IEnumerable<T> xs) {
@@ -873,7 +874,419 @@ namespace Graphing {
s.AppendLine("}");
return s.ToString();
}
- } // end: class Graph
+ } // end: class Graph
+
+ public static class GraphAlgorithms
+ {
+
+ public static Graph<Node> Dual<Node>(this Graph<Node> g, Node dummySource)
+ {
+ var exits = g.Nodes.Where(n => g.Successors(n).Count() == 0).ToList();
+ if (exits.Count == 0)
+ return null;
+ var dual = new Graph<Node>(new HashSet<Tuple<Node, Node>>(g.Edges.Select(e => new Tuple<Node, Node>(e.Item2, e.Item1))));
+ if (exits.Count == 1)
+ dual.AddSource(exits[0]);
+ else
+ {
+ dual.AddSource(dummySource);
+ foreach (var exit in exits)
+ dual.AddEdge(dummySource, exit);
+ }
+ return dual;
+ }
+
+ public static List<Tuple<Node, bool>> LoopyTopSort<Node>(this Graph<Node> g)
+ {
+ Contract.Assert(g.Reducible);
+
+ int n = g.Nodes.Count;
+ var nodeToNumber = new Dictionary<Node, int>(n);
+ var numberToNode = new Node[n];
+ var allNodes = new List<int>();
+ int counter = 0;
+ foreach (Node node in g.Nodes)
+ {
+ numberToNode[counter] = node;
+ nodeToNumber[node] = counter;
+ allNodes.Add(counter);
+ counter++;
+ }
+
+ var loops = new List<int>[n];
+ foreach (var h in g.Headers)
+ {
+ var loopNodes = new HashSet<Node>();
+ foreach (var b in g.BackEdgeNodes(h))
+ loopNodes.UnionWith(g.NaturalLoops(h, b));
+ loops[nodeToNumber[h]] =
+ new List<int>(loopNodes.Select(node => nodeToNumber[node]));
+ }
+
+ var successors = new List<int>[n];
+ int[] incomingEdges = new int[n];
+
+ foreach (var e in g.Edges)
+ {
+ Contract.Assert(e.Item1 != null);
+ Contract.Assert(e.Item2 != null);
+ int source = nodeToNumber[e.Item1], target = nodeToNumber[e.Item2];
+ if (loops[target] == null || !loops[target].Contains(source))
+ {
+ if (successors[source] == null)
+ successors[source] = new List<int>();
+ successors[source].Add(target);
+ incomingEdges[target]++;
+ }
+ }
+
+ var sortedNodes = new List<Tuple<Node, bool>>();
+
+ var regionStack = new Stack<Tuple<Node, List<int>>>();
+ regionStack.Push(new Tuple<Node, List<int>>(default(Node), allNodes));
+
+ while (regionStack.Count != 0)
+ {
+ int rootIndex = -1;
+ foreach (var i in regionStack.Peek().Item2)
+ {
+ if (incomingEdges[i] == 0)
+ {
+ rootIndex = i;
+ break;
+ }
+ }
+ if (rootIndex == -1)
+ {
+ var region = regionStack.Pop();
+ if (regionStack.Count != 0)
+ sortedNodes.Add(new Tuple<Node, bool>(region.Item1, true));
+ continue;
+ }
+ incomingEdges[rootIndex] = -1;
+ sortedNodes.Add(new Tuple<Node, bool>(numberToNode[rootIndex], false));
+ if (successors[rootIndex] != null)
+ foreach (int s in successors[rootIndex])
+ incomingEdges[s]--;
+ if (loops[rootIndex] != null)
+ regionStack.Push(new Tuple<Node, List<int>>(numberToNode[rootIndex],
+ loops[rootIndex]));
+ }
+
+ return sortedNodes;
+ }
+
+ // Algorithm from Jeanne Ferrante, Karl J. Ottenstein, Joe D. Warren,
+ // "The Program Dependence Graph and Its Use in Optimization"
+ public static Dictionary<Node, HashSet<Node>> ControlDependence<Node>(this Graph<Node> g) where Node : class, new()
+ {
+ Graph<Node> dual = g.Dual(new Node());
+ DomRelation<Node> pdom = dual.DominatorMap;
+ var result = new Dictionary<Node, HashSet<Node>>();
+
+ var S = g.Edges.Where(e => !pdom.DominatedBy(e.Item1, e.Item2));
+ foreach (var edge in S)
+ {
+ var L = pdom.LeastCommonAncestor(edge.Item1, edge.Item2);
+ var deps = new List<Node>();
+ if (L == edge.Item1)
+ {
+ pdom.DominatedBy(edge.Item2, edge.Item1, deps);
+ deps.Add(edge.Item2);
+ deps.Add(edge.Item1);
+ }
+ else
+ {
+ pdom.DominatedBy(edge.Item2, L, deps);
+ deps.Add(edge.Item2);
+ }
+ if (result.ContainsKey(edge.Item1))
+ {
+ result[edge.Item1].UnionWith(deps);
+ }
+ else
+ {
+ result[edge.Item1] = new HashSet<Node>(deps);
+ }
+ }
+ return result;
+ }
+
+ }
+
+ public delegate System.Collections.IEnumerable/*<Node!>*//*!*/ Adjacency<T>(T/*!*/ node);
+
+
+ // An SCC is a set of nodes
+ public sealed class SCC<Node> : ICollection<Node>
+ {
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(nodesMap != null);
+ }
+
+ private IDictionary<Node, object>/*!*/ nodesMap = new Dictionary<Node, object>();
+ private ICollection<Node>/*!*/ nodes
+ {
+ get
+ {
+ return cce.NonNull(nodesMap.Keys);
+ }
+ }
+
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ System.Collections.IEnumerator/*!*/ System.Collections.IEnumerable.GetEnumerator()
+ {
+ Contract.Ensures(Contract.Result<System.Collections.IEnumerator>() != null);
+
+ return ((System.Collections.IEnumerable)nodes).GetEnumerator();
+ }
+
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ IEnumerator<Node>/*!*/ IEnumerable<Node>.GetEnumerator()
+ {
+ Contract.Ensures(Contract.Result<IEnumerator<Node>>() != null);
+
+ return ((IEnumerable<Node>)nodes).GetEnumerator();
+ }
+
+ public int Count
+ {
+ get
+ {
+ return nodes.Count;
+ }
+ }
+ public bool IsReadOnly
+ {
+ get
+ {
+ return nodesMap.IsReadOnly;
+ }
+ }
+ public void Add(Node item)
+ {
+ nodesMap.Add(item, null);
+ }
+ public void Clear()
+ {
+ nodesMap.Clear();
+ }
+ [Pure]
+ public bool Contains(Node item)
+ {
+ return nodesMap.ContainsKey(item);
+ }
+ public void CopyTo(Node[] array, int arrayIndex)
+ {
+ //Contract.Requires(array != null);
+ nodes.CopyTo(array, arrayIndex);
+ }
+ public bool Remove(Node item)
+ {
+ return nodesMap.Remove(item);
+ }
+ }
+
+ public sealed class StronglyConnectedComponents<Node> : IEnumerable<SCC<Node>/*!*/> where Node : class
+ {
+ private readonly IDictionary<Node/*!*/, object>/*!*/ graph;
+ [ContractInvariantMethod]
+ void graphInvariantMethod()
+ {
+ Contract.Invariant(Contract.ForAll(graph, entry => entry.Key != null));
+ Contract.Invariant(preds != null);
+ Contract.Invariant(succs != null);
+ }
+ private readonly Adjacency<Node>/*!*/ preds;
+ private readonly Adjacency<Node>/*!*/ succs;
+
+ private bool computed = false;
+ public bool Computed
+ {
+ get
+ {
+ return computed;
+ }
+ }
+
+ [NotDelayed]
+ public StronglyConnectedComponents(System.Collections.IEnumerable/*<Node!>*/ graph, Adjacency<Node> preds, Adjacency<Node> succs)
+ : base()
+ {//BASEMOVE DANGER
+ Contract.Requires(succs != null);
+ Contract.Requires(preds != null);
+ Contract.Requires(graph != null);
+ Contract.Ensures(!Computed);
+ IDictionary<Node/*!*/, object>/*!*/ dict = new Dictionary<Node/*!*/, object>();
+ foreach (Node/*!*/ n in graph)
+ {
+ Contract.Assert(n != null);
+ dict.Add(n, null);
+ }
+
+ this.graph = dict;
+ this.preds = preds;
+ this.succs = succs;
+ //:base();
+ }
+
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ System.Collections.IEnumerator/*!*/ System.Collections.IEnumerable.GetEnumerator()
+ {
+ Contract.Ensures(Contract.Result<System.Collections.IEnumerator>() != null);
+
+ return ((System.Collections.IEnumerable)sccs).GetEnumerator();
+ }
+
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ IEnumerator<SCC<Node>/*!*/>/*!*/ IEnumerable<SCC<Node>/*!*/>.GetEnumerator()
+ {
+ Contract.Ensures(Contract.Result<IEnumerator<SCC<Node>>>() != null);
+
+ Contract.Assume(Computed);
+ Contract.Assert(cce.NonNullElements((IEnumerable<SCC<Node>/*!*/>)sccs));//REVIEW
+ return ((IEnumerable<SCC<Node>/*!*/>)sccs).GetEnumerator();
+ }
+
+ private readonly IList<SCC<Node>/*!*/>/*!*/ sccs = new List<SCC<Node>/*!*/>();
+ [ContractInvariantMethod]
+ void sccsInvariant()
+ {
+ Contract.Invariant(cce.NonNullElements(sccs));
+ }
+
+
+ public void Compute()
+ {
+ Contract.Requires(!Computed);
+ Contract.Ensures(Computed);
+ // Compute post times on graph with edges reversed
+ this.dfsNext = this.preds;
+ foreach (Node/*!*/ n in cce.NonNull(graph.Keys))
+ {
+ Contract.Assert(n != null);
+ if (!seen.ContainsKey(n))
+ {
+ OrderNodes(n);
+ }
+ }
+
+ // Clear seen
+ seen.Clear();
+
+ // Compute SCCs
+ this.dfsNext = this.succs;
+ while (postOrder.Count > 0)
+ {
+ Node/*!*/ n = postOrder.Pop();
+ Contract.Assert(n != null);
+
+ if (!seen.ContainsKey(n))
+ {
+ SCC<Node>/*!*/ curr = new SCC<Node>();
+ FindSCCs(n, curr);
+ sccs.Add(curr);
+ }
+ }
+
+ // Clear seen
+ seen.Clear();
+
+ this.computed = true;
+ }
+
+ private Adjacency<Node>/*?*/ dfsNext = null;
+
+ private readonly IDictionary<Node/*!*/, object>/*!*/ seen = new Dictionary<Node/*!*/, object>();
+ private readonly Stack<Node/*!*/>/*!*/ postOrder = new Stack<Node/*!*/>();
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(seen != null);
+ Contract.Invariant(cce.NonNullElements(postOrder));
+ }
+
+
+ // DFS to order nodes by post times
+ private void OrderNodes(Node node)
+ {
+ Contract.Requires(node != null);
+ seen.Add(node, null);
+
+ Contract.Assert(dfsNext != null);
+ System.Collections.IEnumerable/*!*/ nexts = dfsNext(node);
+ Contract.Assert(nexts != null);
+ foreach (Node/*!*/ n in nexts)
+ {
+ Contract.Assert(n != null);
+ if (graph.ContainsKey(n) && !seen.ContainsKey(n))
+ {
+ OrderNodes(n);
+ }
+ }
+
+ postOrder.Push(node);
+ }
+
+ // DFS to compute SCCs
+ private void FindSCCs(Node node, SCC<Node> currSCC)
+ {
+ Contract.Requires(currSCC != null);
+ Contract.Requires(node != null);
+ //modifies currSCC.*;
+ seen.Add(node, null);
+ currSCC.Add(node);
+
+ Contract.Assert(dfsNext != null);
+ System.Collections.IEnumerable/*!*/ nexts = dfsNext(node);
+ Contract.Assert(nexts != null);
+ foreach (Node/*!*/ n in nexts)
+ {
+ Contract.Assert(n != null);
+ if (graph.ContainsKey(n) && !seen.ContainsKey(n))
+ {
+ FindSCCs(n, currSCC);
+ }
+ }
+ }
+
+ [Pure]
+ public override string ToString()
+ {
+ Contract.Ensures(Contract.Result<string>() != null);
+ string outStr = "";
+ int i = 0;
+
+ foreach (ICollection<Node> component in this)
+ {
+ string/*!*/ tmp = System.String.Format("\nComponent #{0} = ", i++);
+ Contract.Assert(tmp != null);
+ outStr += tmp;
+
+ bool firstInRow = true;
+
+ foreach (Node b in component)
+ {
+ string/*!*/ tmpComponent = System.String.Format("{0}{1}", firstInRow ? "" : ", ", b);
+ Contract.Assert(tmpComponent != null);
+ outStr += tmpComponent;
+ firstInRow = false;
+ }
+ }
+ return outStr;
+ }
+
+ }
public class GraphProgram {
static void TestGraph<T>(T/*!*/ source, params Tuple<T/*!*/, T/*!*/>[] edges) {
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index f27cd410..5271a6a3 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -11,7 +11,7 @@ using Microsoft.Boogie.VCExprAST;
using VC;
using System.Collections;
using System.IO;
-using Graphing;
+using Microsoft.Boogie.GraphUtil;
namespace Microsoft.Boogie.Houdini {
diff --git a/Source/VCGeneration/BlockPredicator.cs b/Source/Predication/BlockPredicator.cs
index 9df1c086..8419471e 100644
--- a/Source/VCGeneration/BlockPredicator.cs
+++ b/Source/Predication/BlockPredicator.cs
@@ -1,4 +1,4 @@
-using Graphing;
+using Microsoft.Boogie.GraphUtil;
using System;
using System.Collections.Generic;
using System.Diagnostics;
diff --git a/Source/Predication/Predication.csproj b/Source/Predication/Predication.csproj
new file mode 100644
index 00000000..d5ed2a9e
--- /dev/null
+++ b/Source/Predication/Predication.csproj
@@ -0,0 +1,87 @@
+<?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>{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>Predication</RootNamespace>
+ <AssemblyName>Predication</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="BlockPredicator.cs" />
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ <Compile Include="SmartBlockPredicator.cs" />
+ <Compile Include="UniformityAnalyser.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\Basetypes\Basetypes.csproj">
+ <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>
+ <Name>Basetypes</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="..\ParserHelper\ParserHelper.csproj">
+ <Project>{fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5}</Project>
+ <Name>ParserHelper</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/VCGeneration/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs
index b4f5a3df..9478595b 100644
--- a/Source/VCGeneration/SmartBlockPredicator.cs
+++ b/Source/Predication/SmartBlockPredicator.cs
@@ -1,528 +1,528 @@
-using Graphing;
-using System;
-using System.Collections.Generic;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using System.Linq;
-
-namespace Microsoft.Boogie {
-
-public class SmartBlockPredicator {
-
- Program prog;
- Implementation impl;
- Graph<Block> blockGraph;
- List<Tuple<Block, bool>> sortedBlocks;
-
- Func<Procedure, bool> useProcedurePredicates;
-
- Dictionary<Block, Variable> predMap, defMap;
- Dictionary<Block, HashSet<Variable>> ownedMap;
- Dictionary<Block, Block> parentMap;
- Dictionary<Block, PartInfo> partInfo;
-
- IdentifierExpr fp;
- Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars =
- new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>();
- Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>();
- HashSet<Block> doneBlocks = new HashSet<Block>();
- bool myUseProcedurePredicates;
- UniformityAnalyser uni;
-
- SmartBlockPredicator(Program p, Implementation i, Func<Procedure, bool> upp, UniformityAnalyser u) {
- prog = p;
- impl = i;
- useProcedurePredicates = upp;
- myUseProcedurePredicates = useProcedurePredicates(i.Proc);
- uni = u;
- }
-
- void PredicateCmd(Expr p, List<Block> blocks, Block block, Cmd cmd, out Block nextBlock) {
- var cCmd = cmd as CallCmd;
- if (cCmd != null && !useProcedurePredicates(cCmd.Proc)) {
- if (p == null) {
- block.Cmds.Add(cmd);
- nextBlock = block;
- return;
- }
-
- var trueBlock = new Block();
- blocks.Add(trueBlock);
- trueBlock.Label = block.Label + ".call.true";
- trueBlock.Cmds.Add(new AssumeCmd(Token.NoToken, p));
- trueBlock.Cmds.Add(cmd);
-
- var falseBlock = new Block();
- blocks.Add(falseBlock);
- falseBlock.Label = block.Label + ".call.false";
- falseBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(p)));
-
- var contBlock = new Block();
- blocks.Add(contBlock);
- contBlock.Label = block.Label + ".call.cont";
-
- block.TransferCmd =
- new GotoCmd(Token.NoToken, new BlockSeq(trueBlock, falseBlock));
- trueBlock.TransferCmd = falseBlock.TransferCmd =
- new GotoCmd(Token.NoToken, new BlockSeq(contBlock));
- nextBlock = contBlock;
- } else {
- PredicateCmd(p, block.Cmds, cmd);
- nextBlock = block;
- }
- }
-
- void PredicateCmd(Expr p, CmdSeq cmdSeq, Cmd cmd) {
- if (cmd is CallCmd) {
- var cCmd = (CallCmd)cmd;
- Debug.Assert(useProcedurePredicates(cCmd.Proc));
- cCmd.Ins.Insert(0, p != null ? p : Expr.True);
- cmdSeq.Add(cCmd);
- } else if (p == null) {
- cmdSeq.Add(cmd);
- } else if (cmd is AssignCmd) {
- var aCmd = (AssignCmd)cmd;
- cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,
- new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>
- new NAryExpr(Token.NoToken,
- new IfThenElse(Token.NoToken),
- new ExprSeq(p, rhs, lhs.AsExpr))))));
- } else if (cmd is AssertCmd) {
- var aCmd = (AssertCmd)cmd;
- Expr newExpr = new EnabledReplacementVisitor(p).VisitExpr(aCmd.Expr);
- aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(p, newExpr);
- cmdSeq.Add(aCmd);
- } else if (cmd is AssumeCmd) {
- var aCmd = (AssumeCmd)cmd;
- cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
- } else if (cmd is HavocCmd) {
- var hCmd = (HavocCmd)cmd;
- foreach (IdentifierExpr v in hCmd.Vars) {
- Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type;
- Contract.Assert(type != null);
-
- IdentifierExpr havocTempExpr;
- if (havocVars.ContainsKey(type)) {
- havocTempExpr = havocVars[type];
- } else {
- var havocVar = new LocalVariable(Token.NoToken,
- new TypedIdent(Token.NoToken,
- "_HAVOC_" + type.ToString(), type));
- impl.LocVars.Add(havocVar);
- havocVars[type] = havocTempExpr =
- new IdentifierExpr(Token.NoToken, havocVar);
- }
- cmdSeq.Add(new HavocCmd(Token.NoToken,
- new IdentifierExprSeq(havocTempExpr)));
- cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
- new NAryExpr(Token.NoToken,
- new IfThenElse(Token.NoToken),
- new ExprSeq(p, havocTempExpr, v))));
- }
- } else if (cmd is CommentCmd) {
- // skip
- } else if (cmd is StateCmd) {
- var sCmd = (StateCmd)cmd;
- var newCmdSeq = new CmdSeq();
- foreach (Cmd c in sCmd.Cmds)
- PredicateCmd(p, newCmdSeq, c);
- sCmd.Cmds = newCmdSeq;
- cmdSeq.Add(sCmd);
- } else {
- Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
- }
- }
-
- // hasPredicatedRegion is true iff the block or its targets are predicated
- // (i.e. we enter, stay within or exit a predicated region).
- void PredicateTransferCmd(Expr p, Block src, CmdSeq cmdSeq, TransferCmd cmd, out bool hasPredicatedRegion) {
- hasPredicatedRegion = predMap.ContainsKey(src);
-
- if (cmd is GotoCmd) {
- var gCmd = (GotoCmd)cmd;
-
- hasPredicatedRegion = hasPredicatedRegion ||
- gCmd.labelTargets.Cast<Block>().Any(b => predMap.ContainsKey(b));
-
- if (gCmd.labelTargets.Length == 1) {
- if (defMap.ContainsKey(gCmd.labelTargets[0]))
- PredicateCmd(p, cmdSeq,
- Cmd.SimpleAssign(Token.NoToken,
- Expr.Ident(predMap[gCmd.labelTargets[0]]), Expr.True));
- } else {
- Debug.Assert(gCmd.labelTargets.Length > 1);
- Debug.Assert(gCmd.labelTargets.Cast<Block>().All(t => uni.IsUniform(impl.Name, t) ||
- partInfo.ContainsKey(t)));
- foreach (Block target in gCmd.labelTargets) {
- if (!partInfo.ContainsKey(target))
- continue;
-
- var part = partInfo[target];
- if (defMap.ContainsKey(part.realDest))
- PredicateCmd(p, cmdSeq,
- Cmd.SimpleAssign(Token.NoToken,
- Expr.Ident(predMap[part.realDest]), part.pred));
- var predsExitingLoop = new Dictionary<Block, List<Expr>>();
- foreach (Block exit in LoopsExited(src, target)) {
- List<Expr> predList;
- if (!predsExitingLoop.ContainsKey(exit))
- predList = predsExitingLoop[exit] = new List<Expr>();
- else
- predList = predsExitingLoop[exit];
- predList.Add(part.pred);
- }
- foreach (var pred in predsExitingLoop) {
- PredicateCmd(p, cmdSeq,
- Cmd.SimpleAssign(Token.NoToken,
- Expr.Ident(predMap[pred.Key]),
- Expr.Not(pred.Value.Aggregate(Expr.Or))));
- }
- }
- }
- } else if (cmd is ReturnCmd) {
- // Blocks which end in a return will never share a predicate with a block
- // which appears after it. Furthermore, such a block cannot be part of a
- // loop. So it is safe to do nothing here.
- } else {
- Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
- }
- }
-
- Variable FreshPredicate(ref int predCount) {
- var pVar = new LocalVariable(Token.NoToken,
- new TypedIdent(Token.NoToken,
- "p" + predCount++,
- Microsoft.Boogie.Type.Bool));
- impl.LocVars.Add(pVar);
- return pVar;
- }
-
- void AssignPredicates(Graph<Block> blockGraph,
- DomRelation<Block> dom,
- DomRelation<Block> pdom,
- IEnumerator<Tuple<Block, bool>> i,
- Variable headPredicate,
- ref int predCount) {
- var header = i.Current.Item1;
- var regionPreds = new List<Tuple<Block, Variable>>();
- var ownedPreds = new HashSet<Variable>();
- ownedMap[header] = ownedPreds;
-
- if (headPredicate != null) {
- predMap[header] = headPredicate;
- defMap[header] = headPredicate;
- regionPreds.Add(new Tuple<Block, Variable>(header, headPredicate));
- }
-
- while (i.MoveNext()) {
- var block = i.Current;
- if (uni != null && uni.IsUniform(impl.Name, block.Item1))
- continue;
- if (block.Item2) {
- if (block.Item1 == header)
- return;
- } else {
- if (blockGraph.Headers.Contains(block.Item1)) {
- parentMap[block.Item1] = header;
- var loopPred = FreshPredicate(ref predCount);
- ownedPreds.Add(loopPred);
- AssignPredicates(blockGraph, dom, pdom, i, loopPred, ref predCount);
- } else {
- bool foundExisting = false;
- foreach (var regionPred in regionPreds) {
- if (dom.DominatedBy(block.Item1, regionPred.Item1) &&
- pdom.DominatedBy(regionPred.Item1, block.Item1)) {
- predMap[block.Item1] = regionPred.Item2;
- foundExisting = true;
- break;
- }
- }
- if (!foundExisting) {
- var condPred = FreshPredicate(ref predCount);
- predMap[block.Item1] = condPred;
- defMap[block.Item1] = condPred;
- ownedPreds.Add(condPred);
- regionPreds.Add(new Tuple<Block, Variable>(block.Item1, condPred));
- }
- }
- }
- }
- }
-
- void AssignPredicates() {
- DomRelation<Block> dom = blockGraph.DominatorMap;
-
- Graph<Block> dualGraph = blockGraph.Dual(new Block());
- DomRelation<Block> pdom = dualGraph.DominatorMap;
-
- var iter = sortedBlocks.GetEnumerator();
- if (!iter.MoveNext()) {
- predMap = defMap = null;
- ownedMap = null;
- return;
- }
-
- int predCount = 0;
- predMap = new Dictionary<Block, Variable>();
- defMap = new Dictionary<Block, Variable>();
- ownedMap = new Dictionary<Block, HashSet<Variable>>();
- parentMap = new Dictionary<Block, Block>();
- AssignPredicates(blockGraph, dom, pdom, iter,
- myUseProcedurePredicates ? impl.InParams[0] : null,
- ref predCount);
- }
-
- IEnumerable<Block> LoopsExited(Block src, Block dest) {
- var i = sortedBlocks.GetEnumerator();
- while (i.MoveNext()) {
- var b = i.Current;
- if (b.Item1 == src) {
- return LoopsExitedForwardEdge(dest, i);
- } else if (b.Item1 == dest) {
- return LoopsExitedBackEdge(src, i);
- }
- }
- Debug.Assert(false);
- return null;
- }
-
- private IEnumerable<Block> LoopsExitedBackEdge(Block src, IEnumerator<Tuple<Block, bool>> i) {
- var headsSeen = new HashSet<Block>();
- while (i.MoveNext()) {
- var b = i.Current;
- if (!b.Item2 && blockGraph.Headers.Contains(b.Item1))
- headsSeen.Add(b.Item1);
- else if (b.Item2)
- headsSeen.Remove(b.Item1);
- if (b.Item1 == src)
- return headsSeen;
- }
- Debug.Assert(false);
- return null;
- }
-
- private IEnumerable<Block> LoopsExitedForwardEdge(Block dest, IEnumerator<Tuple<Block, bool>> i) {
- var headsSeen = new HashSet<Block>();
- while (i.MoveNext()) {
- var b = i.Current;
- if (b.Item1 == dest)
- yield break;
- else if (!b.Item2 && blockGraph.Headers.Contains(b.Item1))
- headsSeen.Add(b.Item1);
- else if (b.Item2 && !headsSeen.Contains(b.Item1))
- yield return b.Item1;
- }
- Debug.Assert(false);
- }
-
- class PartInfo {
- public PartInfo(Expr p, Block r) { pred = p; realDest = r; }
- public Expr pred;
- public Block realDest;
- }
-
- Dictionary<Block, PartInfo> BuildPartitionInfo() {
- var partInfo = new Dictionary<Block, PartInfo>();
- foreach (var block in blockGraph.Nodes) {
- if (uni.IsUniform(impl.Name, block))
- continue;
-
- var parts = block.Cmds.Cast<Cmd>().TakeWhile(
- c => c is AssumeCmd &&
- QKeyValue.FindBoolAttribute(((AssumeCmd)c).Attributes, "partition"));
-
- Expr pred = null;
- if (parts.Count() > 0) {
- pred = parts.Select(a => ((AssumeCmd)a).Expr).Aggregate(Expr.And);
- block.Cmds =
- new CmdSeq(block.Cmds.Cast<Cmd>().Skip(parts.Count()).ToArray());
- } else {
- continue;
- }
-
- Block realDest = block;
- if (block.Cmds.Length == 0) {
- var gc = block.TransferCmd as GotoCmd;
- if (gc != null && gc.labelTargets.Length == 1)
- realDest = gc.labelTargets[0];
- }
- partInfo[block] = new PartInfo(pred, realDest);
- }
-
- return partInfo;
- }
-
- void PredicateImplementation() {
- blockGraph = prog.ProcessLoops(impl);
- sortedBlocks = blockGraph.LoopyTopSort();
-
- AssignPredicates();
- partInfo = BuildPartitionInfo();
-
- if (myUseProcedurePredicates)
- fp = Expr.Ident(impl.InParams[0]);
-
- var newBlocks = new List<Block>();
- Block prevBlock = null;
- foreach (var n in sortedBlocks) {
- if (predMap.ContainsKey(n.Item1)) {
- var p = predMap[n.Item1];
- var pExpr = Expr.Ident(p);
-
- if (n.Item2) {
- var backedgeBlock = new Block();
+using Microsoft.Boogie.GraphUtil;
+using System;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+using System.Linq;
+
+namespace Microsoft.Boogie {
+
+public class SmartBlockPredicator {
+
+ Program prog;
+ Implementation impl;
+ Graph<Block> blockGraph;
+ List<Tuple<Block, bool>> sortedBlocks;
+
+ Func<Procedure, bool> useProcedurePredicates;
+
+ Dictionary<Block, Variable> predMap, defMap;
+ Dictionary<Block, HashSet<Variable>> ownedMap;
+ Dictionary<Block, Block> parentMap;
+ Dictionary<Block, PartInfo> partInfo;
+
+ IdentifierExpr fp;
+ Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars =
+ new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>();
+ Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>();
+ HashSet<Block> doneBlocks = new HashSet<Block>();
+ bool myUseProcedurePredicates;
+ UniformityAnalyser uni;
+
+ SmartBlockPredicator(Program p, Implementation i, Func<Procedure, bool> upp, UniformityAnalyser u) {
+ prog = p;
+ impl = i;
+ useProcedurePredicates = upp;
+ myUseProcedurePredicates = useProcedurePredicates(i.Proc);
+ uni = u;
+ }
+
+ void PredicateCmd(Expr p, List<Block> blocks, Block block, Cmd cmd, out Block nextBlock) {
+ var cCmd = cmd as CallCmd;
+ if (cCmd != null && !useProcedurePredicates(cCmd.Proc)) {
+ if (p == null) {
+ block.Cmds.Add(cmd);
+ nextBlock = block;
+ return;
+ }
+
+ var trueBlock = new Block();
+ blocks.Add(trueBlock);
+ trueBlock.Label = block.Label + ".call.true";
+ trueBlock.Cmds.Add(new AssumeCmd(Token.NoToken, p));
+ trueBlock.Cmds.Add(cmd);
+
+ var falseBlock = new Block();
+ blocks.Add(falseBlock);
+ falseBlock.Label = block.Label + ".call.false";
+ falseBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(p)));
+
+ var contBlock = new Block();
+ blocks.Add(contBlock);
+ contBlock.Label = block.Label + ".call.cont";
+
+ block.TransferCmd =
+ new GotoCmd(Token.NoToken, new BlockSeq(trueBlock, falseBlock));
+ trueBlock.TransferCmd = falseBlock.TransferCmd =
+ new GotoCmd(Token.NoToken, new BlockSeq(contBlock));
+ nextBlock = contBlock;
+ } else {
+ PredicateCmd(p, block.Cmds, cmd);
+ nextBlock = block;
+ }
+ }
+
+ void PredicateCmd(Expr p, CmdSeq cmdSeq, Cmd cmd) {
+ if (cmd is CallCmd) {
+ var cCmd = (CallCmd)cmd;
+ Debug.Assert(useProcedurePredicates(cCmd.Proc));
+ cCmd.Ins.Insert(0, p != null ? p : Expr.True);
+ cmdSeq.Add(cCmd);
+ } else if (p == null) {
+ cmdSeq.Add(cmd);
+ } else if (cmd is AssignCmd) {
+ var aCmd = (AssignCmd)cmd;
+ cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,
+ new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>
+ new NAryExpr(Token.NoToken,
+ new IfThenElse(Token.NoToken),
+ new ExprSeq(p, rhs, lhs.AsExpr))))));
+ } else if (cmd is AssertCmd) {
+ var aCmd = (AssertCmd)cmd;
+ Expr newExpr = new EnabledReplacementVisitor(p).VisitExpr(aCmd.Expr);
+ aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(p, newExpr);
+ cmdSeq.Add(aCmd);
+ } else if (cmd is AssumeCmd) {
+ var aCmd = (AssumeCmd)cmd;
+ cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
+ } else if (cmd is HavocCmd) {
+ var hCmd = (HavocCmd)cmd;
+ foreach (IdentifierExpr v in hCmd.Vars) {
+ Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type;
+ Contract.Assert(type != null);
+
+ IdentifierExpr havocTempExpr;
+ if (havocVars.ContainsKey(type)) {
+ havocTempExpr = havocVars[type];
+ } else {
+ var havocVar = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken,
+ "_HAVOC_" + type.ToString(), type));
+ impl.LocVars.Add(havocVar);
+ havocVars[type] = havocTempExpr =
+ new IdentifierExpr(Token.NoToken, havocVar);
+ }
+ cmdSeq.Add(new HavocCmd(Token.NoToken,
+ new IdentifierExprSeq(havocTempExpr)));
+ cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
+ new NAryExpr(Token.NoToken,
+ new IfThenElse(Token.NoToken),
+ new ExprSeq(p, havocTempExpr, v))));
+ }
+ } else if (cmd is CommentCmd) {
+ // skip
+ } else if (cmd is StateCmd) {
+ var sCmd = (StateCmd)cmd;
+ var newCmdSeq = new CmdSeq();
+ foreach (Cmd c in sCmd.Cmds)
+ PredicateCmd(p, newCmdSeq, c);
+ sCmd.Cmds = newCmdSeq;
+ cmdSeq.Add(sCmd);
+ } else {
+ Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
+ }
+ }
+
+ // hasPredicatedRegion is true iff the block or its targets are predicated
+ // (i.e. we enter, stay within or exit a predicated region).
+ void PredicateTransferCmd(Expr p, Block src, CmdSeq cmdSeq, TransferCmd cmd, out bool hasPredicatedRegion) {
+ hasPredicatedRegion = predMap.ContainsKey(src);
+
+ if (cmd is GotoCmd) {
+ var gCmd = (GotoCmd)cmd;
+
+ hasPredicatedRegion = hasPredicatedRegion ||
+ gCmd.labelTargets.Cast<Block>().Any(b => predMap.ContainsKey(b));
+
+ if (gCmd.labelTargets.Length == 1) {
+ if (defMap.ContainsKey(gCmd.labelTargets[0]))
+ PredicateCmd(p, cmdSeq,
+ Cmd.SimpleAssign(Token.NoToken,
+ Expr.Ident(predMap[gCmd.labelTargets[0]]), Expr.True));
+ } else {
+ Debug.Assert(gCmd.labelTargets.Length > 1);
+ Debug.Assert(gCmd.labelTargets.Cast<Block>().All(t => uni.IsUniform(impl.Name, t) ||
+ partInfo.ContainsKey(t)));
+ foreach (Block target in gCmd.labelTargets) {
+ if (!partInfo.ContainsKey(target))
+ continue;
+
+ var part = partInfo[target];
+ if (defMap.ContainsKey(part.realDest))
+ PredicateCmd(p, cmdSeq,
+ Cmd.SimpleAssign(Token.NoToken,
+ Expr.Ident(predMap[part.realDest]), part.pred));
+ var predsExitingLoop = new Dictionary<Block, List<Expr>>();
+ foreach (Block exit in LoopsExited(src, target)) {
+ List<Expr> predList;
+ if (!predsExitingLoop.ContainsKey(exit))
+ predList = predsExitingLoop[exit] = new List<Expr>();
+ else
+ predList = predsExitingLoop[exit];
+ predList.Add(part.pred);
+ }
+ foreach (var pred in predsExitingLoop) {
+ PredicateCmd(p, cmdSeq,
+ Cmd.SimpleAssign(Token.NoToken,
+ Expr.Ident(predMap[pred.Key]),
+ Expr.Not(pred.Value.Aggregate(Expr.Or))));
+ }
+ }
+ }
+ } else if (cmd is ReturnCmd) {
+ // Blocks which end in a return will never share a predicate with a block
+ // which appears after it. Furthermore, such a block cannot be part of a
+ // loop. So it is safe to do nothing here.
+ } else {
+ Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
+ }
+ }
+
+ Variable FreshPredicate(ref int predCount) {
+ var pVar = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken,
+ "p" + predCount++,
+ Microsoft.Boogie.Type.Bool));
+ impl.LocVars.Add(pVar);
+ return pVar;
+ }
+
+ void AssignPredicates(Graph<Block> blockGraph,
+ DomRelation<Block> dom,
+ DomRelation<Block> pdom,
+ IEnumerator<Tuple<Block, bool>> i,
+ Variable headPredicate,
+ ref int predCount) {
+ var header = i.Current.Item1;
+ var regionPreds = new List<Tuple<Block, Variable>>();
+ var ownedPreds = new HashSet<Variable>();
+ ownedMap[header] = ownedPreds;
+
+ if (headPredicate != null) {
+ predMap[header] = headPredicate;
+ defMap[header] = headPredicate;
+ regionPreds.Add(new Tuple<Block, Variable>(header, headPredicate));
+ }
+
+ while (i.MoveNext()) {
+ var block = i.Current;
+ if (uni != null && uni.IsUniform(impl.Name, block.Item1))
+ continue;
+ if (block.Item2) {
+ if (block.Item1 == header)
+ return;
+ } else {
+ if (blockGraph.Headers.Contains(block.Item1)) {
+ parentMap[block.Item1] = header;
+ var loopPred = FreshPredicate(ref predCount);
+ ownedPreds.Add(loopPred);
+ AssignPredicates(blockGraph, dom, pdom, i, loopPred, ref predCount);
+ } else {
+ bool foundExisting = false;
+ foreach (var regionPred in regionPreds) {
+ if (dom.DominatedBy(block.Item1, regionPred.Item1) &&
+ pdom.DominatedBy(regionPred.Item1, block.Item1)) {
+ predMap[block.Item1] = regionPred.Item2;
+ foundExisting = true;
+ break;
+ }
+ }
+ if (!foundExisting) {
+ var condPred = FreshPredicate(ref predCount);
+ predMap[block.Item1] = condPred;
+ defMap[block.Item1] = condPred;
+ ownedPreds.Add(condPred);
+ regionPreds.Add(new Tuple<Block, Variable>(block.Item1, condPred));
+ }
+ }
+ }
+ }
+ }
+
+ void AssignPredicates() {
+ DomRelation<Block> dom = blockGraph.DominatorMap;
+
+ Graph<Block> dualGraph = blockGraph.Dual(new Block());
+ DomRelation<Block> pdom = dualGraph.DominatorMap;
+
+ var iter = sortedBlocks.GetEnumerator();
+ if (!iter.MoveNext()) {
+ predMap = defMap = null;
+ ownedMap = null;
+ return;
+ }
+
+ int predCount = 0;
+ predMap = new Dictionary<Block, Variable>();
+ defMap = new Dictionary<Block, Variable>();
+ ownedMap = new Dictionary<Block, HashSet<Variable>>();
+ parentMap = new Dictionary<Block, Block>();
+ AssignPredicates(blockGraph, dom, pdom, iter,
+ myUseProcedurePredicates ? impl.InParams[0] : null,
+ ref predCount);
+ }
+
+ IEnumerable<Block> LoopsExited(Block src, Block dest) {
+ var i = sortedBlocks.GetEnumerator();
+ while (i.MoveNext()) {
+ var b = i.Current;
+ if (b.Item1 == src) {
+ return LoopsExitedForwardEdge(dest, i);
+ } else if (b.Item1 == dest) {
+ return LoopsExitedBackEdge(src, i);
+ }
+ }
+ Debug.Assert(false);
+ return null;
+ }
+
+ private IEnumerable<Block> LoopsExitedBackEdge(Block src, IEnumerator<Tuple<Block, bool>> i) {
+ var headsSeen = new HashSet<Block>();
+ while (i.MoveNext()) {
+ var b = i.Current;
+ if (!b.Item2 && blockGraph.Headers.Contains(b.Item1))
+ headsSeen.Add(b.Item1);
+ else if (b.Item2)
+ headsSeen.Remove(b.Item1);
+ if (b.Item1 == src)
+ return headsSeen;
+ }
+ Debug.Assert(false);
+ return null;
+ }
+
+ private IEnumerable<Block> LoopsExitedForwardEdge(Block dest, IEnumerator<Tuple<Block, bool>> i) {
+ var headsSeen = new HashSet<Block>();
+ while (i.MoveNext()) {
+ var b = i.Current;
+ if (b.Item1 == dest)
+ yield break;
+ else if (!b.Item2 && blockGraph.Headers.Contains(b.Item1))
+ headsSeen.Add(b.Item1);
+ else if (b.Item2 && !headsSeen.Contains(b.Item1))
+ yield return b.Item1;
+ }
+ Debug.Assert(false);
+ }
+
+ class PartInfo {
+ public PartInfo(Expr p, Block r) { pred = p; realDest = r; }
+ public Expr pred;
+ public Block realDest;
+ }
+
+ Dictionary<Block, PartInfo> BuildPartitionInfo() {
+ var partInfo = new Dictionary<Block, PartInfo>();
+ foreach (var block in blockGraph.Nodes) {
+ if (uni.IsUniform(impl.Name, block))
+ continue;
+
+ var parts = block.Cmds.Cast<Cmd>().TakeWhile(
+ c => c is AssumeCmd &&
+ QKeyValue.FindBoolAttribute(((AssumeCmd)c).Attributes, "partition"));
+
+ Expr pred = null;
+ if (parts.Count() > 0) {
+ pred = parts.Select(a => ((AssumeCmd)a).Expr).Aggregate(Expr.And);
+ block.Cmds =
+ new CmdSeq(block.Cmds.Cast<Cmd>().Skip(parts.Count()).ToArray());
+ } else {
+ continue;
+ }
+
+ Block realDest = block;
+ if (block.Cmds.Length == 0) {
+ var gc = block.TransferCmd as GotoCmd;
+ if (gc != null && gc.labelTargets.Length == 1)
+ realDest = gc.labelTargets[0];
+ }
+ partInfo[block] = new PartInfo(pred, realDest);
+ }
+
+ return partInfo;
+ }
+
+ void PredicateImplementation() {
+ blockGraph = prog.ProcessLoops(impl);
+ sortedBlocks = blockGraph.LoopyTopSort();
+
+ AssignPredicates();
+ partInfo = BuildPartitionInfo();
+
+ if (myUseProcedurePredicates)
+ fp = Expr.Ident(impl.InParams[0]);
+
+ var newBlocks = new List<Block>();
+ Block prevBlock = null;
+ foreach (var n in sortedBlocks) {
+ if (predMap.ContainsKey(n.Item1)) {
+ var p = predMap[n.Item1];
+ var pExpr = Expr.Ident(p);
+
+ if (n.Item2) {
+ var backedgeBlock = new Block();
newBlocks.Add(backedgeBlock);
-
- backedgeBlock.Label = n.Item1.Label + ".backedge";
- backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, pExpr,
- new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)));
- backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,
- new BlockSeq(n.Item1));
-
- var tailBlock = new Block();
- newBlocks.Add(tailBlock);
-
- tailBlock.Label = n.Item1.Label + ".tail";
- tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
+
+ backedgeBlock.Label = n.Item1.Label + ".backedge";
+ backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, pExpr,
+ new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)));
+ backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,
+ new BlockSeq(n.Item1));
+
+ var tailBlock = new Block();
+ newBlocks.Add(tailBlock);
+
+ tailBlock.Label = n.Item1.Label + ".tail";
+ tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
Expr.Not(pExpr)));
if (uni != null && !uni.IsUniform(impl.Name, n.Item1)) {
uni.AddNonUniform(impl.Name, backedgeBlock);
uni.AddNonUniform(impl.Name, tailBlock);
- }
-
- if (prevBlock != null)
- prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
- new BlockSeq(backedgeBlock, tailBlock));
- prevBlock = tailBlock;
- } else {
- PredicateBlock(pExpr, n.Item1, newBlocks, ref prevBlock);
- }
- } else {
- if (!n.Item2) {
- PredicateBlock(null, n.Item1, newBlocks, ref prevBlock);
- }
- }
- }
-
- if (prevBlock != null)
- prevBlock.TransferCmd = new ReturnCmd(Token.NoToken);
-
- impl.Blocks = newBlocks;
- }
-
- private void PredicateBlock(Expr pExpr, Block block, List<Block> newBlocks, ref Block prevBlock) {
- var firstBlock = block;
-
- var oldCmdSeq = block.Cmds;
- block.Cmds = new CmdSeq();
- newBlocks.Add(block);
- if (prevBlock != null) {
- prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq(block));
- }
-
- if (parentMap.ContainsKey(block)) {
- var parent = parentMap[block];
- if (predMap.ContainsKey(parent)) {
- var parentPred = predMap[parent];
- if (parentPred != null) {
- block.Cmds.Add(new AssertCmd(Token.NoToken,
- pExpr != null ? (Expr)Expr.Imp(pExpr, Expr.Ident(parentPred))
- : Expr.Ident(parentPred)));
- }
- }
- }
-
- var transferCmd = block.TransferCmd;
- foreach (Cmd cmd in oldCmdSeq)
- PredicateCmd(pExpr, newBlocks, block, cmd, out block);
-
- if (ownedMap.ContainsKey(firstBlock)) {
- var owned = ownedMap[firstBlock];
- foreach (var v in owned)
- block.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, Expr.Ident(v), Expr.False));
- }
-
- bool hasPredicatedRegion;
- PredicateTransferCmd(pExpr, block, block.Cmds, transferCmd, out hasPredicatedRegion);
-
- if (hasPredicatedRegion)
- prevBlock = block;
- else
- prevBlock = null;
-
- doneBlocks.Add(block);
- }
-
- private Expr CreateIfFPThenElse(Expr then, Expr eElse) {
- if (myUseProcedurePredicates) {
- return new NAryExpr(Token.NoToken,
- new IfThenElse(Token.NoToken),
- new ExprSeq(fp, then, eElse));
- } else {
- return then;
- }
- }
-
- public static void Predicate(Program p,
- Func<Procedure, bool> useProcedurePredicates = null,
- UniformityAnalyser uni = null) {
- useProcedurePredicates = useProcedurePredicates ?? (proc => false);
- if (uni != null) {
- var oldUPP = useProcedurePredicates;
- useProcedurePredicates = proc => oldUPP(proc) && !uni.IsUniform(proc.Name);
- }
-
- foreach (var decl in p.TopLevelDeclarations.ToList()) {
- if (decl is Procedure || decl is Implementation) {
- var proc = decl as Procedure;
- Implementation impl = null;
- if (proc == null) {
- impl = (Implementation)decl;
- proc = impl.Proc;
- }
-
- bool upp = useProcedurePredicates(proc);
- if (upp) {
- var dwf = (DeclWithFormals)decl;
- var fpVar = new Formal(Token.NoToken,
- new TypedIdent(Token.NoToken, "_P",
- Microsoft.Boogie.Type.Bool),
- /*incoming=*/true);
- dwf.InParams = new VariableSeq(
- (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
- .ToArray());
-
- if (impl == null) {
- var newRequires = new RequiresSeq();
- foreach (Requires r in proc.Requires) {
- newRequires.Add(new Requires(r.Free,
- new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition)));
- }
- var newEnsures = new EnsuresSeq();
- foreach (Ensures e in proc.Ensures) {
- newEnsures.Add(new Ensures(e.Free,
- new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition)));
- }
- }
- }
-
- if (impl != null) {
- try {
- new SmartBlockPredicator(p, impl, useProcedurePredicates, uni).PredicateImplementation();
- } catch (Program.IrreducibleLoopException) { }
- }
- }
- }
- }
-
- public static void Predicate(Program p, Implementation impl) {
- try {
- new SmartBlockPredicator(p, impl, proc => false, null).PredicateImplementation();
- }
- catch (Program.IrreducibleLoopException) { }
- }
-
-}
-
-}
+ }
+
+ if (prevBlock != null)
+ prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
+ new BlockSeq(backedgeBlock, tailBlock));
+ prevBlock = tailBlock;
+ } else {
+ PredicateBlock(pExpr, n.Item1, newBlocks, ref prevBlock);
+ }
+ } else {
+ if (!n.Item2) {
+ PredicateBlock(null, n.Item1, newBlocks, ref prevBlock);
+ }
+ }
+ }
+
+ if (prevBlock != null)
+ prevBlock.TransferCmd = new ReturnCmd(Token.NoToken);
+
+ impl.Blocks = newBlocks;
+ }
+
+ private void PredicateBlock(Expr pExpr, Block block, List<Block> newBlocks, ref Block prevBlock) {
+ var firstBlock = block;
+
+ var oldCmdSeq = block.Cmds;
+ block.Cmds = new CmdSeq();
+ newBlocks.Add(block);
+ if (prevBlock != null) {
+ prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq(block));
+ }
+
+ if (parentMap.ContainsKey(block)) {
+ var parent = parentMap[block];
+ if (predMap.ContainsKey(parent)) {
+ var parentPred = predMap[parent];
+ if (parentPred != null) {
+ block.Cmds.Add(new AssertCmd(Token.NoToken,
+ pExpr != null ? (Expr)Expr.Imp(pExpr, Expr.Ident(parentPred))
+ : Expr.Ident(parentPred)));
+ }
+ }
+ }
+
+ var transferCmd = block.TransferCmd;
+ foreach (Cmd cmd in oldCmdSeq)
+ PredicateCmd(pExpr, newBlocks, block, cmd, out block);
+
+ if (ownedMap.ContainsKey(firstBlock)) {
+ var owned = ownedMap[firstBlock];
+ foreach (var v in owned)
+ block.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, Expr.Ident(v), Expr.False));
+ }
+
+ bool hasPredicatedRegion;
+ PredicateTransferCmd(pExpr, block, block.Cmds, transferCmd, out hasPredicatedRegion);
+
+ if (hasPredicatedRegion)
+ prevBlock = block;
+ else
+ prevBlock = null;
+
+ doneBlocks.Add(block);
+ }
+
+ private Expr CreateIfFPThenElse(Expr then, Expr eElse) {
+ if (myUseProcedurePredicates) {
+ return new NAryExpr(Token.NoToken,
+ new IfThenElse(Token.NoToken),
+ new ExprSeq(fp, then, eElse));
+ } else {
+ return then;
+ }
+ }
+
+ public static void Predicate(Program p,
+ Func<Procedure, bool> useProcedurePredicates = null,
+ UniformityAnalyser uni = null) {
+ useProcedurePredicates = useProcedurePredicates ?? (proc => false);
+ if (uni != null) {
+ var oldUPP = useProcedurePredicates;
+ useProcedurePredicates = proc => oldUPP(proc) && !uni.IsUniform(proc.Name);
+ }
+
+ foreach (var decl in p.TopLevelDeclarations.ToList()) {
+ if (decl is Procedure || decl is Implementation) {
+ var proc = decl as Procedure;
+ Implementation impl = null;
+ if (proc == null) {
+ impl = (Implementation)decl;
+ proc = impl.Proc;
+ }
+
+ bool upp = useProcedurePredicates(proc);
+ if (upp) {
+ var dwf = (DeclWithFormals)decl;
+ var fpVar = new Formal(Token.NoToken,
+ new TypedIdent(Token.NoToken, "_P",
+ Microsoft.Boogie.Type.Bool),
+ /*incoming=*/true);
+ dwf.InParams = new VariableSeq(
+ (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
+ .ToArray());
+
+ if (impl == null) {
+ var newRequires = new RequiresSeq();
+ foreach (Requires r in proc.Requires) {
+ newRequires.Add(new Requires(r.Free,
+ new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition)));
+ }
+ var newEnsures = new EnsuresSeq();
+ foreach (Ensures e in proc.Ensures) {
+ newEnsures.Add(new Ensures(e.Free,
+ new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition)));
+ }
+ }
+ }
+
+ if (impl != null) {
+ try {
+ new SmartBlockPredicator(p, impl, useProcedurePredicates, uni).PredicateImplementation();
+ } catch (Program.IrreducibleLoopException) { }
+ }
+ }
+ }
+ }
+
+ public static void Predicate(Program p, Implementation impl) {
+ try {
+ new SmartBlockPredicator(p, impl, proc => false, null).PredicateImplementation();
+ }
+ catch (Program.IrreducibleLoopException) { }
+ }
+
+}
+
+}
diff --git a/Source/VCGeneration/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs
index 802ee2d2..3408d88b 100644
--- a/Source/VCGeneration/UniformityAnalyser.cs
+++ b/Source/Predication/UniformityAnalyser.cs
@@ -1,160 +1,195 @@
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using Microsoft.Boogie;
-using System.Diagnostics;
-using Graphing;
-
-namespace Microsoft.Boogie
-{
-
- public class UniformityAnalyser
- {
- private Program prog;
-
- private bool doAnalysis, unstructured;
-
- private ISet<Implementation> entryPoints;
-
- private IEnumerable<Variable> nonUniformVars;
-
- private bool ProcedureChanged;
-
- private Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>> uniformityInfo;
-
- private Dictionary<string, HashSet<int>> nonUniformLoops;
-
- private Dictionary<string, HashSet<Block>> nonUniformBlocks;
-
- private Dictionary<string, HashSet<int>> loopsWithNonuniformReturn;
-
- private Dictionary<string, List<string>> inParameters;
-
- private Dictionary<string, List<string>> outParameters;
-
- private List<WhileCmd> loopStack;
-
- private bool hitNonuniformReturn;
-
- public UniformityAnalyser(Program prog, bool doAnalysis, bool unstructured, ISet<Implementation> entryPoints, IEnumerable<Variable> nonUniformVars)
- {
- this.prog = prog;
- this.doAnalysis = doAnalysis;
- this.unstructured = unstructured;
- this.entryPoints = entryPoints;
- this.nonUniformVars = nonUniformVars;
- uniformityInfo = new Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>>();
- nonUniformLoops = new Dictionary<string, HashSet<int>>();
- nonUniformBlocks = new Dictionary<string, HashSet<Block>>();
- loopsWithNonuniformReturn = new Dictionary<string, HashSet<int>>();
- inParameters = new Dictionary<string, List<string>>();
- outParameters = new Dictionary<string, List<string>>();
- loopStack = new List<WhileCmd>();
- }
-
- public void Analyse()
- {
- var impls = prog.TopLevelDeclarations.OfType<Implementation>();
-
- foreach (var Impl in impls)
- {
- bool uniformProcedure = doAnalysis || entryPoints.Contains(Impl);
-
- uniformityInfo.Add(Impl.Name, new KeyValuePair<bool, Dictionary<string, bool>>
- (uniformProcedure, new Dictionary<string, bool> ()));
-
- nonUniformLoops.Add(Impl.Name, new HashSet<int>());
- loopsWithNonuniformReturn.Add(Impl.Name, new HashSet<int>());
-
- foreach (var v in nonUniformVars)
- SetNonUniform(Impl.Name, v.Name);
-
- foreach (Variable v in Impl.LocVars)
- {
- if (doAnalysis)
- {
- SetUniform(Impl.Name, v.Name);
- }
- else
- {
- SetNonUniform(Impl.Name, v.Name);
- }
- }
-
- inParameters[Impl.Name] = new List<string>();
-
- foreach (Variable v in Impl.InParams)
- {
- inParameters[Impl.Name].Add(v.Name);
- if (doAnalysis)
- {
- SetUniform(Impl.Name, v.Name);
- }
- else
- {
- SetNonUniform(Impl.Name, v.Name);
- }
- }
-
- outParameters[Impl.Name] = new List<string>();
- foreach (Variable v in Impl.OutParams)
- {
- outParameters[Impl.Name].Add(v.Name);
- if (doAnalysis)
- {
- SetUniform(Impl.Name, v.Name);
- }
- else
- {
- SetNonUniform(Impl.Name, v.Name);
- }
- }
-
- ProcedureChanged = true;
- }
-
- if (doAnalysis)
- {
- while (ProcedureChanged)
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics;
+using Microsoft.Boogie.GraphUtil;
+
+namespace Microsoft.Boogie
+{
+
+ public class UniformityAnalyser
+ {
+ private Program prog;
+
+ private bool doAnalysis, unstructured;
+
+ private ISet<Implementation> entryPoints;
+
+ private IEnumerable<Variable> nonUniformVars;
+
+ private bool ProcedureChanged;
+
+ private Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>> uniformityInfo;
+
+ private Dictionary<string, HashSet<int>> nonUniformLoops;
+
+ private Dictionary<string, HashSet<Block>> nonUniformBlocks;
+
+ private Dictionary<string, HashSet<int>> loopsWithNonuniformReturn;
+
+ private Dictionary<string, List<string>> inParameters;
+
+ private Dictionary<string, List<string>> outParameters;
+
+ private List<WhileCmd> loopStack;
+
+ private bool hitNonuniformReturn;
+
+ /// <summary>
+ /// Simplifies the CFG of the given implementation impl by merging each
+ /// basic block with a single predecessor into that predecessor if the
+ /// predecessor has a single successor. If a uniformity analyser is
+ /// being used then block will only be merged if they are both uniform
+ /// or both non-uniform
+ /// </summary>
+ public static void MergeBlocksIntoPredecessors(Program prog, Implementation impl, UniformityAnalyser uni)
+ {
+ var blockGraph = prog.ProcessLoops(impl);
+ var predMap = new Dictionary<Block, Block>();
+ foreach (var block in blockGraph.Nodes)
+ {
+ try
+ {
+ var pred = blockGraph.Predecessors(block).Single();
+ if (blockGraph.Successors(pred).Single() == block &&
+ (uni == null ||
+ (uni.IsUniform(impl.Name, pred) && uni.IsUniform(impl.Name, block)) ||
+ (!uni.IsUniform(impl.Name, pred) && !uni.IsUniform(impl.Name, block))))
+ {
+ Block predMapping;
+ while (predMap.TryGetValue(pred, out predMapping))
+ pred = predMapping;
+ pred.Cmds.AddRange(block.Cmds);
+ pred.TransferCmd = block.TransferCmd;
+ impl.Blocks.Remove(block);
+ predMap[block] = pred;
+ }
+ // If Single throws an exception above (i.e. not exactly one pred/succ), skip this block.
+ }
+ catch (InvalidOperationException) { }
+ }
+ }
+
+ public UniformityAnalyser(Program prog, bool doAnalysis, bool unstructured, ISet<Implementation> entryPoints, IEnumerable<Variable> nonUniformVars)
+ {
+ this.prog = prog;
+ this.doAnalysis = doAnalysis;
+ this.unstructured = unstructured;
+ this.entryPoints = entryPoints;
+ this.nonUniformVars = nonUniformVars;
+ uniformityInfo = new Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>>();
+ nonUniformLoops = new Dictionary<string, HashSet<int>>();
+ nonUniformBlocks = new Dictionary<string, HashSet<Block>>();
+ loopsWithNonuniformReturn = new Dictionary<string, HashSet<int>>();
+ inParameters = new Dictionary<string, List<string>>();
+ outParameters = new Dictionary<string, List<string>>();
+ loopStack = new List<WhileCmd>();
+ }
+
+ public void Analyse()
+ {
+ var impls = prog.TopLevelDeclarations.OfType<Implementation>();
+
+ foreach (var Impl in impls)
+ {
+ bool uniformProcedure = doAnalysis || entryPoints.Contains(Impl);
+
+ uniformityInfo.Add(Impl.Name, new KeyValuePair<bool, Dictionary<string, bool>>
+ (uniformProcedure, new Dictionary<string, bool> ()));
+
+ nonUniformLoops.Add(Impl.Name, new HashSet<int>());
+ loopsWithNonuniformReturn.Add(Impl.Name, new HashSet<int>());
+
+ foreach (var v in nonUniformVars)
+ SetNonUniform(Impl.Name, v.Name);
+
+ foreach (Variable v in Impl.LocVars)
+ {
+ if (doAnalysis)
+ {
+ SetUniform(Impl.Name, v.Name);
+ }
+ else
+ {
+ SetNonUniform(Impl.Name, v.Name);
+ }
+ }
+
+ inParameters[Impl.Name] = new List<string>();
+
+ foreach (Variable v in Impl.InParams)
+ {
+ inParameters[Impl.Name].Add(v.Name);
+ if (doAnalysis)
+ {
+ SetUniform(Impl.Name, v.Name);
+ }
+ else
+ {
+ SetNonUniform(Impl.Name, v.Name);
+ }
+ }
+
+ outParameters[Impl.Name] = new List<string>();
+ foreach (Variable v in Impl.OutParams)
+ {
+ outParameters[Impl.Name].Add(v.Name);
+ if (doAnalysis)
+ {
+ SetUniform(Impl.Name, v.Name);
+ }
+ else
+ {
+ SetNonUniform(Impl.Name, v.Name);
+ }
+ }
+
+ ProcedureChanged = true;
+ }
+
+ if (doAnalysis)
+ {
+ while (ProcedureChanged)
+ {
+ ProcedureChanged = false;
+
+ foreach (var Impl in impls)
+ {
+ hitNonuniformReturn = false;
+ Analyse(Impl, uniformityInfo[Impl.Name].Key);
+ }
+ }
+ }
+
+ foreach (var Impl in impls)
+ {
+ if (!IsUniform (Impl.Name))
{
- ProcedureChanged = false;
-
- foreach (var Impl in impls)
- {
- hitNonuniformReturn = false;
- Analyse(Impl, uniformityInfo[Impl.Name].Key);
- }
- }
- }
-
- foreach (var Impl in impls)
- {
- if (!IsUniform (Impl.Name))
- {
- List<string> newIns = new List<String>();
- newIns.Add("_P");
- foreach (string s in inParameters[Impl.Name])
- {
- newIns.Add(s);
- }
- inParameters[Impl.Name] = newIns;
- }
- }
- }
-
- private void Analyse(Implementation Impl, bool ControlFlowIsUniform)
- {
- if (unstructured)
+ List<string> newIns = new List<String>();
+ newIns.Add("_P");
+ foreach (string s in inParameters[Impl.Name])
+ {
+ newIns.Add(s);
+ }
+ inParameters[Impl.Name] = newIns;
+ }
+ }
+ }
+
+ private void Analyse(Implementation Impl, bool ControlFlowIsUniform)
+ {
+ if (unstructured)
{
- if (!ControlFlowIsUniform)
- {
- nonUniformBlocks[Impl.Name] = new HashSet<Block>(Impl.Blocks);
-
- foreach (Variable v in Impl.LocVars) {
- if (IsUniform(Impl.Name, v.Name)) {
- SetNonUniform(Impl.Name, v.Name);
- }
+ if (!ControlFlowIsUniform)
+ {
+ nonUniformBlocks[Impl.Name] = new HashSet<Block>(Impl.Blocks);
+
+ foreach (Variable v in Impl.LocVars) {
+ if (IsUniform(Impl.Name, v.Name)) {
+ SetNonUniform(Impl.Name, v.Name);
+ }
}
foreach (Variable v in Impl.InParams) {
@@ -168,35 +203,35 @@ namespace Microsoft.Boogie
SetNonUniform(Impl.Name, v.Name);
}
}
-
- return;
- }
-
- Graph<Block> blockGraph = prog.ProcessLoops(Impl);
- var ctrlDep = blockGraph.ControlDependence();
-
- // Compute transitive closure of control dependence info.
- bool changed;
- do
- {
- changed = false;
- foreach (var depEntry in ctrlDep)
- {
- var newDepSet = new HashSet<Block>(depEntry.Value);
- foreach (var dep in depEntry.Value)
- {
- if (ctrlDep.ContainsKey(dep))
- newDepSet.UnionWith(ctrlDep[dep]);
- }
- if (newDepSet.Count != depEntry.Value.Count)
- {
- depEntry.Value.UnionWith(newDepSet);
- changed = true;
- }
- }
- } while (changed);
-
- var nonUniformBlockSet = new HashSet<Block>();
+
+ return;
+ }
+
+ Graph<Block> blockGraph = prog.ProcessLoops(Impl);
+ var ctrlDep = blockGraph.ControlDependence();
+
+ // Compute transitive closure of control dependence info.
+ bool changed;
+ do
+ {
+ changed = false;
+ foreach (var depEntry in ctrlDep)
+ {
+ var newDepSet = new HashSet<Block>(depEntry.Value);
+ foreach (var dep in depEntry.Value)
+ {
+ if (ctrlDep.ContainsKey(dep))
+ newDepSet.UnionWith(ctrlDep[dep]);
+ }
+ if (newDepSet.Count != depEntry.Value.Count)
+ {
+ depEntry.Value.UnionWith(newDepSet);
+ changed = true;
+ }
+ }
+ } while (changed);
+
+ var nonUniformBlockSet = new HashSet<Block>();
nonUniformBlocks[Impl.Name] = nonUniformBlockSet;
do {
@@ -213,323 +248,323 @@ namespace Microsoft.Boogie
}
}
} while (changed);
- }
- else
- {
- Analyse(Impl, Impl.StructuredStmts, ControlFlowIsUniform);
- }
- }
-
-
- private void Analyse(Implementation impl, StmtList stmtList, bool ControlFlowIsUniform)
- {
- ControlFlowIsUniform &= !hitNonuniformReturn;
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- Analyse(impl, bb, ControlFlowIsUniform);
- }
- }
-
- private Implementation GetImplementation(string procedureName)
- {
- foreach (Declaration D in prog.TopLevelDeclarations)
- {
- if (D is Implementation && ((D as Implementation).Name == procedureName))
- {
- return D as Implementation;
- }
- }
- return null;
- }
-
- private void Analyse(Implementation impl, BigBlock bb, bool ControlFlowIsUniform)
- {
- ControlFlowIsUniform &= !hitNonuniformReturn;
- Analyse(impl, bb.simpleCmds, ControlFlowIsUniform);
-
- if (bb.ec is WhileCmd)
- {
- WhileCmd wc = bb.ec as WhileCmd;
- loopStack.Add(wc);
- Analyse(impl, wc.Body, ControlFlowIsUniform && IsUniform(impl.Name, wc.Guard) &&
- !nonUniformLoops[impl.Name].Contains(GetLoopId(wc)));
- loopStack.RemoveAt(loopStack.Count - 1);
- }
- else if (bb.ec is IfCmd)
- {
- IfCmd ifCmd = bb.ec as IfCmd;
- Analyse(impl, ifCmd.thn, ControlFlowIsUniform && IsUniform(impl.Name, ifCmd.Guard));
- if (ifCmd.elseBlock != null)
- {
- Analyse(impl, ifCmd.elseBlock, ControlFlowIsUniform && IsUniform(impl.Name, ifCmd.Guard));
- }
- Debug.Assert(ifCmd.elseIf == null);
- }
- else if (bb.ec is BreakCmd)
- {
- if (!ControlFlowIsUniform && !nonUniformLoops[impl.Name].Contains(GetLoopId(loopStack[loopStack.Count - 1])))
- {
- SetNonUniform(impl.Name, loopStack[loopStack.Count - 1]);
- }
- }
-
- if (bb.tc is ReturnCmd && !ControlFlowIsUniform)
- {
- hitNonuniformReturn = true;
- if (loopStack.Count > 0 && !nonUniformLoops[impl.Name].Contains(GetLoopId(loopStack[0])))
- {
- SetNonUniform(impl.Name, loopStack[0]);
- loopsWithNonuniformReturn[impl.Name].Add(GetLoopId(loopStack[0]));
- }
- }
-
-
- }
-
- private bool Analyse(Implementation impl, CmdSeq cmdSeq, bool ControlFlowIsUniform)
- {
- foreach (Cmd c in cmdSeq)
- {
- if (c is AssignCmd)
- {
- AssignCmd assignCmd = c as AssignCmd;
- foreach (var a in assignCmd.Lhss.Zip(assignCmd.Rhss))
+ }
+ else
+ {
+ Analyse(Impl, Impl.StructuredStmts, ControlFlowIsUniform);
+ }
+ }
+
+
+ private void Analyse(Implementation impl, StmtList stmtList, bool ControlFlowIsUniform)
+ {
+ ControlFlowIsUniform &= !hitNonuniformReturn;
+ foreach (BigBlock bb in stmtList.BigBlocks)
+ {
+ Analyse(impl, bb, ControlFlowIsUniform);
+ }
+ }
+
+ private Implementation GetImplementation(string procedureName)
+ {
+ foreach (Declaration D in prog.TopLevelDeclarations)
+ {
+ if (D is Implementation && ((D as Implementation).Name == procedureName))
+ {
+ return D as Implementation;
+ }
+ }
+ return null;
+ }
+
+ private void Analyse(Implementation impl, BigBlock bb, bool ControlFlowIsUniform)
+ {
+ ControlFlowIsUniform &= !hitNonuniformReturn;
+ Analyse(impl, bb.simpleCmds, ControlFlowIsUniform);
+
+ if (bb.ec is WhileCmd)
+ {
+ WhileCmd wc = bb.ec as WhileCmd;
+ loopStack.Add(wc);
+ Analyse(impl, wc.Body, ControlFlowIsUniform && IsUniform(impl.Name, wc.Guard) &&
+ !nonUniformLoops[impl.Name].Contains(GetLoopId(wc)));
+ loopStack.RemoveAt(loopStack.Count - 1);
+ }
+ else if (bb.ec is IfCmd)
+ {
+ IfCmd ifCmd = bb.ec as IfCmd;
+ Analyse(impl, ifCmd.thn, ControlFlowIsUniform && IsUniform(impl.Name, ifCmd.Guard));
+ if (ifCmd.elseBlock != null)
+ {
+ Analyse(impl, ifCmd.elseBlock, ControlFlowIsUniform && IsUniform(impl.Name, ifCmd.Guard));
+ }
+ Debug.Assert(ifCmd.elseIf == null);
+ }
+ else if (bb.ec is BreakCmd)
+ {
+ if (!ControlFlowIsUniform && !nonUniformLoops[impl.Name].Contains(GetLoopId(loopStack[loopStack.Count - 1])))
+ {
+ SetNonUniform(impl.Name, loopStack[loopStack.Count - 1]);
+ }
+ }
+
+ if (bb.tc is ReturnCmd && !ControlFlowIsUniform)
+ {
+ hitNonuniformReturn = true;
+ if (loopStack.Count > 0 && !nonUniformLoops[impl.Name].Contains(GetLoopId(loopStack[0])))
+ {
+ SetNonUniform(impl.Name, loopStack[0]);
+ loopsWithNonuniformReturn[impl.Name].Add(GetLoopId(loopStack[0]));
+ }
+ }
+
+
+ }
+
+ private bool Analyse(Implementation impl, CmdSeq cmdSeq, bool ControlFlowIsUniform)
+ {
+ foreach (Cmd c in cmdSeq)
+ {
+ if (c is AssignCmd)
+ {
+ AssignCmd assignCmd = c as AssignCmd;
+ foreach (var a in assignCmd.Lhss.Zip(assignCmd.Rhss))
{
-
- if (a.Item1 is SimpleAssignLhs)
- {
+
+ if (a.Item1 is SimpleAssignLhs)
+ {
SimpleAssignLhs lhs = a.Item1 as SimpleAssignLhs;
Expr rhs = a.Item2;
- if (IsUniform(impl.Name, lhs.AssignedVariable.Name) &&
- (!ControlFlowIsUniform || !IsUniform(impl.Name, rhs)))
+ if (IsUniform(impl.Name, lhs.AssignedVariable.Name) &&
+ (!ControlFlowIsUniform || !IsUniform(impl.Name, rhs)))
{
- SetNonUniform(impl.Name, lhs.AssignedVariable.Name);
+ SetNonUniform(impl.Name, lhs.AssignedVariable.Name);
}
- }
- }
- }
- else if (c is HavocCmd)
- {
- HavocCmd havocCmd = c as HavocCmd;
- foreach(IdentifierExpr ie in havocCmd.Vars)
- {
- if(IsUniform(impl.Name, ie.Decl.Name)) {
- SetNonUniform(impl.Name, ie.Decl.Name);
- }
- }
- }
- else if (c is CallCmd)
- {
- CallCmd callCmd = c as CallCmd;
- Implementation CalleeImplementation = GetImplementation(callCmd.callee);
-
- if (CalleeImplementation != null)
- {
-
- if (!ControlFlowIsUniform)
- {
- if (IsUniform(callCmd.callee))
- {
- SetNonUniform(callCmd.callee);
- }
- }
- for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
- {
- if (IsUniform(callCmd.callee, CalleeImplementation.InParams[i].Name)
- && !IsUniform(impl.Name, callCmd.Ins[i]))
- {
- SetNonUniform(callCmd.callee, CalleeImplementation.InParams[i].Name);
- }
- }
-
- for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
- {
- if (IsUniform(impl.Name, callCmd.Outs[i].Name)
- && !IsUniform(callCmd.callee, CalleeImplementation.OutParams[i].Name))
- {
- SetNonUniform(impl.Name, callCmd.Outs[i].Name);
- }
- }
-
- }
- }
- else if (c is AssumeCmd)
- {
- var ac = (AssumeCmd)c;
- if (ControlFlowIsUniform && QKeyValue.FindBoolAttribute(ac.Attributes, "partition") &&
- !IsUniform(impl.Name, ac.Expr))
+ }
+ }
+ }
+ else if (c is HavocCmd)
+ {
+ HavocCmd havocCmd = c as HavocCmd;
+ foreach(IdentifierExpr ie in havocCmd.Vars)
+ {
+ if(IsUniform(impl.Name, ie.Decl.Name)) {
+ SetNonUniform(impl.Name, ie.Decl.Name);
+ }
+ }
+ }
+ else if (c is CallCmd)
+ {
+ CallCmd callCmd = c as CallCmd;
+ Implementation CalleeImplementation = GetImplementation(callCmd.callee);
+
+ if (CalleeImplementation != null)
+ {
+
+ if (!ControlFlowIsUniform)
+ {
+ if (IsUniform(callCmd.callee))
+ {
+ SetNonUniform(callCmd.callee);
+ }
+ }
+ for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
+ {
+ if (IsUniform(callCmd.callee, CalleeImplementation.InParams[i].Name)
+ && !IsUniform(impl.Name, callCmd.Ins[i]))
+ {
+ SetNonUniform(callCmd.callee, CalleeImplementation.InParams[i].Name);
+ }
+ }
+
+ for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
+ {
+ if (IsUniform(impl.Name, callCmd.Outs[i].Name)
+ && !IsUniform(callCmd.callee, CalleeImplementation.OutParams[i].Name))
+ {
+ SetNonUniform(impl.Name, callCmd.Outs[i].Name);
+ }
+ }
+
+ }
+ }
+ else if (c is AssumeCmd)
+ {
+ var ac = (AssumeCmd)c;
+ if (ControlFlowIsUniform && QKeyValue.FindBoolAttribute(ac.Attributes, "partition") &&
+ !IsUniform(impl.Name, ac.Expr))
{
ControlFlowIsUniform = false;
- }
- }
- }
-
- return ControlFlowIsUniform;
- }
-
- private int GetLoopId(WhileCmd wc)
- {
- AssertCmd inv = wc.Invariants[0] as AssertCmd;
- Debug.Assert(inv.Attributes.Key.Contains("loophead_"));
- return Convert.ToInt32(inv.Attributes.Key.Substring("loophead_".Length));
- }
-
- private void SetNonUniform(string procedureName)
- {
- uniformityInfo[procedureName] = new KeyValuePair<bool,Dictionary<string,bool>>
- (false, uniformityInfo[procedureName].Value);
- RecordProcedureChanged();
- }
-
- private void SetNonUniform(string procedureName, WhileCmd wc)
- {
- nonUniformLoops[procedureName].Add(GetLoopId(wc));
- RecordProcedureChanged();
- }
-
- public bool IsUniform(string procedureName)
- {
- if (!uniformityInfo.ContainsKey(procedureName))
- {
- return false;
- }
- return uniformityInfo[procedureName].Key;
- }
-
- public bool IsUniform(string procedureName, Block b)
- {
- if (!nonUniformBlocks.ContainsKey(procedureName))
- {
- return false;
- }
- return !nonUniformBlocks[procedureName].Contains(b);
- }
-
- class UniformExpressionAnalysisVisitor : StandardVisitor {
-
- private bool isUniform = true;
- private Dictionary<string, bool> uniformityInfo;
-
- public UniformExpressionAnalysisVisitor(Dictionary<string, bool> uniformityInfo) {
- this.uniformityInfo = uniformityInfo;
- }
-
- public override Variable VisitVariable(Variable v) {
- if (!uniformityInfo.ContainsKey(v.Name)) {
- isUniform = isUniform && (v is Constant);
- } else if (!uniformityInfo[v.Name]) {
- isUniform = false;
- }
-
- return v;
- }
-
- internal bool IsUniform() {
- return isUniform;
- }
- }
-
- public bool IsUniform(string procedureName, Expr expr)
- {
- UniformExpressionAnalysisVisitor visitor = new UniformExpressionAnalysisVisitor(uniformityInfo[procedureName].Value);
- visitor.VisitExpr(expr);
- return visitor.IsUniform();
- }
-
- public bool IsUniform(string procedureName, string v)
- {
- if (!uniformityInfo.ContainsKey(procedureName))
- {
- return false;
- }
-
- if (!uniformityInfo[procedureName].Value.ContainsKey(v))
- {
- return false;
- }
- return uniformityInfo[procedureName].Value[v];
- }
-
- private void SetUniform(string procedureName, string v)
- {
- uniformityInfo[procedureName].Value[v] = true;
- RecordProcedureChanged();
- }
-
- private void RecordProcedureChanged()
- {
- ProcedureChanged = true;
- }
-
- private void SetNonUniform(string procedureName, string v)
- {
- uniformityInfo[procedureName].Value[v] = false;
- RecordProcedureChanged();
- }
-
- public void dump()
- {
- foreach (string p in uniformityInfo.Keys)
- {
- Console.WriteLine("Procedure " + p + ": "
- + (uniformityInfo[p].Key ? "uniform" : "nonuniform"));
- foreach (string v in uniformityInfo[p].Value.Keys)
- {
- Console.WriteLine(" " + v + ": " +
- (uniformityInfo[p].Value[v] ? "uniform" : "nonuniform"));
- }
- Console.Write("Ins [");
- for (int i = 0; i < inParameters[p].Count; i++)
- {
- Console.Write((i == 0 ? "" : ", ") + inParameters[p][i]);
- }
- Console.WriteLine("]");
- Console.Write("Outs [");
- for (int i = 0; i < outParameters[p].Count; i++)
- {
- Console.Write((i == 0 ? "" : ", ") + outParameters[p][i]);
- }
- Console.WriteLine("]");
- Console.Write("Non-uniform loops:");
- foreach (int l in nonUniformLoops[p])
- {
- Console.Write(" " + l);
- }
- Console.WriteLine();
- Console.Write("Non-uniform blocks:");
- foreach (Block b in nonUniformBlocks[p])
- {
- Console.Write(" " + b.Label);
- }
- Console.WriteLine();
- }
- }
-
-
- public string GetInParameter(string procName, int i)
- {
- return inParameters[procName][i];
- }
-
- public string GetOutParameter(string procName, int i)
- {
- return outParameters[procName][i];
- }
-
-
- public bool knowsOf(string p)
- {
- return uniformityInfo.ContainsKey(p);
- }
-
- public void AddNonUniform(string proc, string v)
- {
- if (uniformityInfo.ContainsKey(proc))
- {
- Debug.Assert(!uniformityInfo[proc].Value.ContainsKey(v));
- uniformityInfo[proc].Value[v] = false;
- }
+ }
+ }
+ }
+
+ return ControlFlowIsUniform;
+ }
+
+ private int GetLoopId(WhileCmd wc)
+ {
+ AssertCmd inv = wc.Invariants[0] as AssertCmd;
+ Debug.Assert(inv.Attributes.Key.Contains("loophead_"));
+ return Convert.ToInt32(inv.Attributes.Key.Substring("loophead_".Length));
+ }
+
+ private void SetNonUniform(string procedureName)
+ {
+ uniformityInfo[procedureName] = new KeyValuePair<bool,Dictionary<string,bool>>
+ (false, uniformityInfo[procedureName].Value);
+ RecordProcedureChanged();
+ }
+
+ private void SetNonUniform(string procedureName, WhileCmd wc)
+ {
+ nonUniformLoops[procedureName].Add(GetLoopId(wc));
+ RecordProcedureChanged();
+ }
+
+ public bool IsUniform(string procedureName)
+ {
+ if (!uniformityInfo.ContainsKey(procedureName))
+ {
+ return false;
+ }
+ return uniformityInfo[procedureName].Key;
+ }
+
+ public bool IsUniform(string procedureName, Block b)
+ {
+ if (!nonUniformBlocks.ContainsKey(procedureName))
+ {
+ return false;
+ }
+ return !nonUniformBlocks[procedureName].Contains(b);
+ }
+
+ class UniformExpressionAnalysisVisitor : StandardVisitor {
+
+ private bool isUniform = true;
+ private Dictionary<string, bool> uniformityInfo;
+
+ public UniformExpressionAnalysisVisitor(Dictionary<string, bool> uniformityInfo) {
+ this.uniformityInfo = uniformityInfo;
+ }
+
+ public override Variable VisitVariable(Variable v) {
+ if (!uniformityInfo.ContainsKey(v.Name)) {
+ isUniform = isUniform && (v is Constant);
+ } else if (!uniformityInfo[v.Name]) {
+ isUniform = false;
+ }
+
+ return v;
+ }
+
+ internal bool IsUniform() {
+ return isUniform;
+ }
+ }
+
+ public bool IsUniform(string procedureName, Expr expr)
+ {
+ UniformExpressionAnalysisVisitor visitor = new UniformExpressionAnalysisVisitor(uniformityInfo[procedureName].Value);
+ visitor.VisitExpr(expr);
+ return visitor.IsUniform();
+ }
+
+ public bool IsUniform(string procedureName, string v)
+ {
+ if (!uniformityInfo.ContainsKey(procedureName))
+ {
+ return false;
+ }
+
+ if (!uniformityInfo[procedureName].Value.ContainsKey(v))
+ {
+ return false;
+ }
+ return uniformityInfo[procedureName].Value[v];
+ }
+
+ private void SetUniform(string procedureName, string v)
+ {
+ uniformityInfo[procedureName].Value[v] = true;
+ RecordProcedureChanged();
+ }
+
+ private void RecordProcedureChanged()
+ {
+ ProcedureChanged = true;
+ }
+
+ private void SetNonUniform(string procedureName, string v)
+ {
+ uniformityInfo[procedureName].Value[v] = false;
+ RecordProcedureChanged();
+ }
+
+ public void dump()
+ {
+ foreach (string p in uniformityInfo.Keys)
+ {
+ Console.WriteLine("Procedure " + p + ": "
+ + (uniformityInfo[p].Key ? "uniform" : "nonuniform"));
+ foreach (string v in uniformityInfo[p].Value.Keys)
+ {
+ Console.WriteLine(" " + v + ": " +
+ (uniformityInfo[p].Value[v] ? "uniform" : "nonuniform"));
+ }
+ Console.Write("Ins [");
+ for (int i = 0; i < inParameters[p].Count; i++)
+ {
+ Console.Write((i == 0 ? "" : ", ") + inParameters[p][i]);
+ }
+ Console.WriteLine("]");
+ Console.Write("Outs [");
+ for (int i = 0; i < outParameters[p].Count; i++)
+ {
+ Console.Write((i == 0 ? "" : ", ") + outParameters[p][i]);
+ }
+ Console.WriteLine("]");
+ Console.Write("Non-uniform loops:");
+ foreach (int l in nonUniformLoops[p])
+ {
+ Console.Write(" " + l);
+ }
+ Console.WriteLine();
+ Console.Write("Non-uniform blocks:");
+ foreach (Block b in nonUniformBlocks[p])
+ {
+ Console.Write(" " + b.Label);
+ }
+ Console.WriteLine();
+ }
+ }
+
+
+ public string GetInParameter(string procName, int i)
+ {
+ return inParameters[procName][i];
+ }
+
+ public string GetOutParameter(string procName, int i)
+ {
+ return outParameters[procName][i];
+ }
+
+
+ public bool knowsOf(string p)
+ {
+ return uniformityInfo.ContainsKey(p);
+ }
+
+ public void AddNonUniform(string proc, string v)
+ {
+ if (uniformityInfo.ContainsKey(proc))
+ {
+ Debug.Assert(!uniformityInfo[proc].Value.ContainsKey(v));
+ uniformityInfo[proc].Value[v] = false;
+ }
}
public void AddNonUniform(string proc, Block b) {
@@ -537,20 +572,20 @@ namespace Microsoft.Boogie
Debug.Assert(!nonUniformBlocks[proc].Contains(b));
nonUniformBlocks[proc].Add(b);
}
- }
-
- public bool IsUniform(string proc, WhileCmd wc)
- {
- if (unstructured)
- return false;
-
- return !nonUniformLoops[proc].Contains(GetLoopId(wc));
- }
-
- public bool HasNonuniformReturn(string proc, WhileCmd whileCmd)
- {
- return loopsWithNonuniformReturn[proc].Contains(GetLoopId(whileCmd));
- }
- }
-
-}
+ }
+
+ public bool IsUniform(string proc, WhileCmd wc)
+ {
+ if (unstructured)
+ return false;
+
+ return !nonUniformLoops[proc].Contains(GetLoopId(wc));
+ }
+
+ public bool HasNonuniformReturn(string proc, WhileCmd whileCmd)
+ {
+ return loopsWithNonuniformReturn[proc].Contains(GetLoopId(whileCmd));
+ }
+ }
+
+}
diff --git a/Source/Provers/Simplify/Let2ImpliesVisitor.cs b/Source/Provers/Simplify/Let2ImpliesVisitor.cs
deleted file mode 100644
index 9b8328d1..00000000
--- a/Source/Provers/Simplify/Let2ImpliesVisitor.cs
+++ /dev/null
@@ -1,236 +0,0 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using Microsoft.Boogie.VCExprAST;
-
-namespace Microsoft.Boogie.Simplify
-{
- // Simplify does not understand the LET operator, so we have to replace
- // it with implications (previously, this was done in the VCExprGenerator), or
- // we have to apply the let as a substitution (in the case of terms)
-
- // This visitor expects that let-bindings are sorted, so that bound
- // variables only occur after their declaration
-
- public class Let2ImpliesMutator : SubstitutingVCExprVisitor {
-
- public Let2ImpliesMutator(VCExpressionGenerator gen) :base(gen) {
- Contract.Requires(gen!=null);
- this.keepLetFormula = this.keepLetTerm = false;
- }
-
- public Let2ImpliesMutator(VCExpressionGenerator gen, bool keepLetTerm, bool keepLetFormula):base(gen) {
- Contract.Requires(gen!=null);
-
- this.keepLetTerm = keepLetTerm;
- this.keepLetFormula = keepLetFormula;
- }
-
- readonly bool keepLetTerm;
- readonly bool keepLetFormula;
-
- public VCExpr Mutate(VCExpr expr) {
- Contract.Requires(expr != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- return Mutate(expr, new VCExprSubstitution ());
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
- private int polarity = 1; // 1 for positive, -1 for negative, 0 for both
-
- // we also track which variables occur in positive, negative, or
- // in both positions (to decide whether implications or equations
- // have to be used to define such a variable)
- private enum OccurrenceTypes { None, Pos, Neg, PosNeg };
- private OccurrenceTypes Union(OccurrenceTypes o1, OccurrenceTypes o2) {
- switch(o1) {
- case OccurrenceTypes.None: return o2;
- case OccurrenceTypes.Pos:
- switch(o2) {
- case OccurrenceTypes.None:
- case OccurrenceTypes.Pos:
- return OccurrenceTypes.Pos;
- default:
- return OccurrenceTypes.PosNeg;
- }
- case OccurrenceTypes.Neg:
- switch(o2) {
- case OccurrenceTypes.None:
- case OccurrenceTypes.Neg:
- return OccurrenceTypes.Neg;
- default:
- return OccurrenceTypes.PosNeg;
- }
- default:
- return OccurrenceTypes.PosNeg;
- }
- }
-
- private IDictionary<VCExprVar/*!*/, OccurrenceTypes>/*!*/ VarOccurrences =
- new Dictionary<VCExprVar/*!*/, OccurrenceTypes>();
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(VarOccurrences != null);
-}
-
- ////////////////////////////////////////////////////////////////////////////
-
- public override VCExpr Visit(VCExprVar node,
- VCExprSubstitution substitution) {
- Contract.Requires(node!= null);
- Contract.Requires(substitution != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- VCExpr res = base.Visit(node, substitution);
- Contract.Assert(res!=null);
-
- VCExprVar resAsVar = res as VCExprVar;
- if (resAsVar != null) {
- OccurrenceTypes occ;
- if (polarity > 0)
- occ = OccurrenceTypes.Pos;
- else if (polarity < 0)
- occ = OccurrenceTypes.Neg;
- else
- occ = OccurrenceTypes.PosNeg;
-
- OccurrenceTypes oldOcc;
- if (VarOccurrences.TryGetValue(resAsVar, out oldOcc))
- occ = Union(occ, oldOcc);
- VarOccurrences[resAsVar] = occ;
- }
-
- return res;
- }
-
- public override VCExpr Visit(VCExprNAry node,
- VCExprSubstitution substitution) {
- Contract.Requires(node != null);
- Contract.Requires(substitution != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- // track the polarity to ensure that no implications are introduced
- // in negative positions
- // UGLY: the code for tracking polarities should be factored out
- // (similar code is used in the TypeEraser)
-
- VCExpr res;
- if (node.Op.Equals(VCExpressionGenerator.NotOp)) {
- polarity = -polarity;
- res = base.Visit(node, substitution);
- polarity = -polarity;
- } else if (node.Op.Equals(VCExpressionGenerator.ImpliesOp)) {
- polarity = -polarity;
- VCExpr newArg0 = Mutate(node[0], substitution);
- Contract.Assert(newArg0 != null);
- polarity = -polarity;
- VCExpr newArg1 = Mutate(node[1], substitution);
- Contract.Assert(newArg1 != null);
-
- res = Gen.Implies(newArg0, newArg1);
- } else if (!node.Op.Equals(VCExpressionGenerator.AndOp) &&
- !node.Op.Equals(VCExpressionGenerator.OrOp) &&
- !(node.Op is VCExprLabelOp)) {
- // standard is to set the polarity to 0 (fits most operators)
- int oldPolarity = polarity;
- polarity = 0;
- res = base.Visit(node, substitution);
- polarity = oldPolarity;
- } else {
- res = base.Visit(node, substitution);
- }
-
- return res;
- }
-
- public override VCExpr Visit(VCExprLet originalNode,
- VCExprSubstitution substitution) {
- Contract.Requires(originalNode != null);
- Contract.Requires(substitution != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- // first sort the bindings to be able to apply substitutions
- LetBindingSorter letSorter = new LetBindingSorter (Gen);
- Contract.Assert(letSorter != null);
- VCExpr newNode = letSorter.Mutate(originalNode, true);
- Contract.Assert(newNode != null);
- VCExprLet node = newNode as VCExprLet;
-
- if (node == null)
- // it can happen that the complete let-expressions gets eliminated by the
- // sorter, which also checks whether let-bindings are actually used
- return newNode;
-
- substitution.PushScope(); try {
-
- // the bindings that remain and that are later handled using an implication
- List<VCExprLetBinding> bindings = new List<VCExprLetBinding> ();
- List<VCExprLetBinding> keepBindings = new List<VCExprLetBinding> ();
-
- foreach (VCExprLetBinding binding in node) {
- Contract.Assert(binding != null);
- // in all cases we apply the substitution up to this point
- // to the bound formula
- VCExpr newE = Mutate(binding.E, substitution);
- Contract.Assert(newE != null);
- if (binding.V.Type.IsBool) {
- // a bound formula is handled using an implication; we introduce
- // a fresh variable to avoid clashes
- Contract.Assert( polarity > 0);
-
- if (keepLetFormula) {
- keepBindings.Add(Gen.LetBinding(binding.V, newE));
-
- } else {
- VCExprVar newVar = Gen.Variable(binding.V.Name, Type.Bool);
- Contract.Assert(newVar != null);
- substitution[binding.V] = newVar;
-
- bindings.Add(Gen.LetBinding(newVar, newE));
- }
- } else {
- if (keepLetTerm) {
- keepBindings.Add(Gen.LetBinding(binding.V, newE));
- } else {
- // a bound term is substituted
- substitution[binding.V] = newE;
- }
- }
- }
-
- VCExpr newBody = Mutate(node.Body, substitution);
- Contract.Assert(newBody != null);
- if (keepBindings.Count > 0) {
- newBody = Gen.Let(keepBindings, newBody);
- }
-
- // Depending on the places where the variable occurs, we would
- // have to introduce implications or equations to define the
- // bound variables. For the time being, we just assert that all
- // occurrences are positive
- foreach (VCExprLetBinding b in bindings) {
- Contract.Assert(b != null);
- OccurrenceTypes occ;
- if (VarOccurrences.TryGetValue(b.V, out occ))
- Contract.Assert( occ == OccurrenceTypes.None || occ == OccurrenceTypes.Pos);
- }
-
- return Gen.ImpliesSimp(Gen.AsImplications(bindings), newBody);
-
- } finally {
- substitution.PopScope();
- }
- }
- }
-
-} \ No newline at end of file
diff --git a/Source/Provers/Simplify/Prover.cs b/Source/Provers/Simplify/Prover.cs
deleted file mode 100644
index 3faa18e1..00000000
--- a/Source/Provers/Simplify/Prover.cs
+++ /dev/null
@@ -1,656 +0,0 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.IO;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using System.Collections;
-using System.Collections.Generic;
-//using util;
-using Microsoft.Boogie;
-
-// Simplified interface to an external prover like Simplify or the z3 process, taken from Bird.
-namespace Microsoft.Boogie.Simplify {
- /// <summary>
- /// An interface to Simplify theorem prover.
- /// </summary>
- ///
- [ContractClass(typeof(ProverProcessContracts))]
- public abstract class ProverProcess {
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(simplify != null);
- Contract.Invariant(fromSimplify != null);
- Contract.Invariant(toSimplify != null);
- Contract.Invariant(fromStdError != null);
- }
-
- [Rep]
- protected readonly Process simplify;
-
- [Rep]
- readonly TextReader fromSimplify;
- [Rep]
- readonly TextWriter toSimplify;
- [Rep]
- readonly TextReader fromStdError;
-
- protected bool readTimedOut;
-
- int nFormulasChecked = 0;
- public int NumFormulasChecked {
- get {
- return nFormulasChecked;
- }
- }
-
- // Note: In the Everett build (.NET framework < 2.0), Process.PeakVirtualMemorySize64
- // is not defined, but rather a version that returns an 'int' rather than a 'long'.
- public long PeakVirtualMemorySize {
- [NoDefaultContract]
- get
- //modifies this.*;
- {
- Contract.Requires(cce.IsPeerConsistent(this));
- try {
- cce.BeginExpose(this);
- simplify.Refresh();
-#if WHIDBEY
- return simplify.PeakVirtualMemorySize64;
-#else
- return simplify.PeakPagedMemorySize64;
-#endif
- } finally {
- cce.EndExpose();
- }
- }
- }
-
- public bool HasExited {
- get {
- return simplify.HasExited;
- }
- }
-
- public ProverProcess(ProcessStartInfo psi, string proverPath) { // throws ProverException
- Contract.Requires(psi != null);
- Contract.Requires(proverPath != null);
- try {
- Process simplify = Process.Start(psi);
- this.simplify = simplify;
- fromSimplify = simplify.StandardOutput;
- toSimplify = simplify.StandardInput;
- fromStdError = simplify.StandardError;
- } catch (System.ComponentModel.Win32Exception e) {
- throw new ProverException(string.Format("Unable to start the process {0}: {1}", proverPath, e.Message));
- }
- // base();
- }
-
- public abstract string OptionComments();
-
- //[Pure(false)]
- public virtual IEnumerable<string/*!>!*/> ParameterSettings {
- get {
- yield break;
- }
- }
-
- public void Close()
- //modifies this.*;
- {
- cce.BeginExpose(this);
- {
- toSimplify.Flush();
- if (this.simplify != null) {
- if (!simplify.HasExited) {
- this.Kill();
- }
- simplify.Close();
- }
- }
- cce.EndExpose();
- }
-
- [NoDefaultContract] // this method assumes nothing about the object, other than that it has been constructed (which means simplify!=null)
- [Verify(false)] // The call simplify.Kill will require simplify.IsPeerConsistent, but since we don't know the state of "this" and "simplify", we cannot afford the run-time check that an assume statement here would impose
- public void Kill() {
- try {
- if (CommandLineOptions.Clo.ProverShutdownLimit > 0) {
- toSimplify.Close();
- for (int i = 0; !simplify.HasExited && i <= CommandLineOptions.Clo.ProverShutdownLimit * 1000; i += 100) {
- System.Threading.Thread.Sleep(100);
- }
- }
- if (!simplify.HasExited) {
- simplify.Kill();
- }
- } catch (InvalidOperationException) { /* already exited */
- } catch (System.ComponentModel.Win32Exception) { /* already exiting */
- }
- }
-
- public virtual void AddAxioms(string s)
- //modifies this.*;
- //modifies Console.Out.*, Console.Error.*;
- {
- Contract.Requires(s != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- cce.BeginExpose(this);
- toSimplify.Write("(BG_PUSH ");
- toSimplify.Write(s);
- toSimplify.WriteLine(")");
- cce.EndExpose();
- }
-
- public virtual void Feed(string s, int statementCount)
- //modifies this.*;
- //modifies Console.Out.*, Console.Error.*;
- {
- Contract.Requires(s != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- cce.BeginExpose(this);
- {
- toSimplify.Write(s);
- }
- cce.EndExpose();
- }
-
- public virtual void PopAxioms()
- //modifies this.*;
- //modifies Console.Out.*, Console.Error.*;
- {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- cce.BeginExpose(this);
- {
- toSimplify.WriteLine("(BG_POP)");
- }
- cce.EndExpose();
- }
-
- public void ToFlush()
- //modifies this.*;
- {
- cce.BeginExpose(this);
- {
- toSimplify.Flush();
- }
- cce.EndExpose();
- }
-
- public enum ProverOutcome {
- Valid,
- NotValid,
- TimeOut,
- OutOfMemory,
- Inconclusive
- }
-
- /// <summary>
- /// Passes the formula to Simplify.
- /// </summary>
- public void BeginCheck(string descriptiveName, string formula)
- //modifies this.*;
- //modifies Console.Out.*, Console.Error.*;
- {
- Contract.Requires(descriptiveName != null);
- Contract.Requires(formula != null);
- DoBeginCheck(descriptiveName, formula);
- nFormulasChecked++;
- }
-
- /// <summary>
- /// Reports the outcome of formula checking. If the outcome is Invalid,
- /// then the "handler" is invoked with each counterexample.
- /// </summary>
- public abstract ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler handler);
- //modifies this.**;
- //modifies Console.Out.*, Console.Error.*;
- //modifies handler.*;
-
- protected abstract void DoBeginCheck(string descriptiveName, string formula);
- //modifies this.*;
- //modifies Console.Out.*, Console.Error.*;
-
- /// <summary>
- /// Returns an array of the labels in "labels", with "|" brackets (if any)
- /// stripped off.
- /// Assumes that every label begins with "|+" or "|@", or just "+" or "@",
- /// and ends with "|" if it started with one, and that these "|" brackets are
- /// the only "|"s in "labels".
- /// </summary>
- protected static List<string/*!>!*/> ParseLabels(string labels) {
- Contract.Requires(labels != null);
- Contract.Ensures(Contract.Result<List<string>>() != null);
-
- List<string> list = new List<string>();
- int j = 0;
- while (true)
- // invariant: j is the number of characters of "labels" consumed so far
- // invariant: an even number of '|' characters remain in "labels"
- {
- cce.LoopInvariant(0 <= j && j <= labels.Length);
- j = labels.IndexOfAny(new char[] { '|', '+', '@' }, j);
- if (j < 0) {
- // no more labels
- return list;
- }
- char ch = labels[j];
- if (ch == '|') {
- j++; // skip the '|'
- Contract.Assume(j < labels.Length); // there should now be a '+' or '@'
- ch = labels[j];
- }
- Contract.Assume(ch == '+' || ch == '@');
- j++; // skip the '+' or '@'
- int k = labels.IndexOfAny(new char[] { '|', ' ', ')' }, j);
- Contract.Assume(j + 2 <= k);
- string s = labels.Substring(j, k - j);
- list.Add(s);
- j = k + 1;
- }
- }
-
- [Rep]
- char[] expectBuffer = null;
-
- /// <summary>
- /// Expects s[0]==ch and the next s.Length-1 characters of the input to be s[1,..]
- /// If not, more characters may be read from "fromSimplify" to provide additional context
- /// for the UnexpectedProverOutputException exception that will be thrown.
- /// </summary>
- protected void Expect(int ch, string s)
- //modifies this.*;
- {
- Contract.Requires(s != null);
- Contract.Requires(1 <= s.Length);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- if (ch == -1) {
- // a return of -1 from FromReadChar means that there is no StdOutput
- // to treat this we can return the error message we get from Z3 on StdError and then
- // declare this case to be inconclusive
- string str = FromStdErrorAll();
- if (str == "") {
- throw new ProverDiedException();
- } else {
- throw new UnexpectedProverOutputException("Expected \"" + s + "\", found:\r\n<<<start>>>\r\n" + str + "<<<end>>>");
- }
- }
-
- string badInputPrefix;
- if (ch != s[0]) {
- badInputPrefix = Char.ToString((char)ch);
- } else {
- int len = s.Length - 1;
- if (expectBuffer == null || expectBuffer.Length < len) {
- cce.BeginExpose(this);
- {
- expectBuffer = new char[len];
- }
- cce.EndExpose();
- }
- try {
- string s0;
- cce.BeginExpose(this);
- {
- fromSimplify.ReadBlock(expectBuffer, 0, len);
- s0 = new string(expectBuffer, 0, len);
- }
- cce.EndExpose();
- string s1 = s.Substring(1, len);
- if (s0.CompareTo(s1) == 0) {
- badInputPrefix = null; // no error
- } else {
- badInputPrefix = (char)ch + s0;
- }
- } catch (IOException) {
- throw new UnexpectedProverOutputException("Expected \"" + s + "\", encountered IO exception.");
- }
- }
-
- if (badInputPrefix != null) {
- // Read the rest of the available input, without blocking!
- // Despite the confusing documentation for the Read method, it seems
- // that Read does block. It if didn't, I would have written:
- // string remaining = "";
- // char[] buf = new char[1024];
- // while (true) {
- // int len = fromSimplify.Read(buf, 0, buf.Length);
- // remaining += new String(buf, 0, len);
- // if (len != buf.Length) {
- // break;
- // }
- // }
- // But instead, I'll just hope that one line of input is available and read
- // it.
- string remaining = fromSimplify.ReadLine() + "\r\n";
- throw new UnexpectedProverOutputException("Expected \"" + s + "\", found:\r\n<<<start>>>\r\n" + badInputPrefix + remaining + "<<<end>>>");
- }
- }
-
- protected int FromReadChar()
- //modifies this.*;
- {
- try {
- cce.BeginExpose(this);
- return fromSimplify.Read();
- } finally {
- cce.EndExpose();
- }
- }
-
- private void KillProver(object state) {
- cce.BeginExpose(this);
- {
- this.readTimedOut = true;
- simplify.Kill();
- }
- cce.EndExpose();
- }
-
- protected int FromReadChar(int timeout)
- //modifies this.*;
- {
- Contract.Requires(-1 <= timeout);
- try {
- cce.BeginExpose(this);
- this.readTimedOut = false;
- System.Threading.Timer t = new System.Threading.Timer(this.KillProver, null, timeout, System.Threading.Timeout.Infinite);
- int ch = fromSimplify.Read();
- t.Change(System.Threading.Timeout.Infinite, System.Threading.Timeout.Infinite);
- t.Dispose();
- return ch;
- } finally {
- cce.EndExpose();
- }
- }
-
- protected string FromReadLine()
- //modifies this.*;
- {
- Contract.Ensures(Contract.Result<string>() != null);
- try {
- cce.BeginExpose(this);
- string s = fromSimplify.ReadLine();
- if (s == null) {
- // this is what ReadLine returns if all characters have been read
- s = "";
- }
- return s;
- } finally {
- cce.EndExpose();
- }
- }
-
- protected string FromStdErrorAll()
- //modifies this.*;
- {
- Contract.Ensures(Contract.Result<string>() != null);
-
- try {
- cce.BeginExpose(this);
- if (fromStdError != null) {
- string s = fromStdError.ReadToEnd();
- if (s == null) {
- // this is what ReadLine returns if all characters have been read
- s = "";
- }
- return s;
- } else {
- // there is no StdErrorReader available
- return "";
- }
- } finally {
- cce.EndExpose();
- }
- }
-
- protected void ToWriteLine(string s)
- //modifies this.*;
- {
- Contract.Requires(s != null);
- cce.BeginExpose(this);
- {
- toSimplify.WriteLine(s);
- }
- cce.EndExpose();
- }
- }
- [ContractClassFor(typeof(ProverProcess))]
- public abstract class ProverProcessContracts : ProverProcess {
- private ProverProcessContracts() : base(null, null) { }
- public override string OptionComments() {
- Contract.Ensures(Contract.Result<string>() != null);
- throw new NotImplementedException();
- }
-
- public override ProverProcess.ProverOutcome CheckOutcome(ProverInterface.ErrorHandler handler) {
- Contract.Requires(handler != null);
- throw new NotImplementedException();
- }
-
- protected override void DoBeginCheck(string descriptiveName, string formula) {
- Contract.Requires(descriptiveName != null);
- Contract.Requires(formula != null);
- throw new NotImplementedException();
- }
- }
- // derived by Z3ProverProcess
- public class SimplifyProverProcess : ProverProcess {
- public SimplifyProverProcess(string proverPath, bool dummy) :base(getPSI(proverPath),proverPath) {
- Contract.Requires(proverPath != null);
- // throws ProverException
- }
- private static ProcessStartInfo getPSI(string proverPath){ProcessStartInfo psi = new ProcessStartInfo(proverPath, "-labelsonly");
- psi.CreateNoWindow = true;
- psi.UseShellExecute = false;
- psi.RedirectStandardInput = true;
- psi.RedirectStandardOutput = true;
- psi.RedirectStandardError = true;
- Contract.Assume(psi.EnvironmentVariables != null); // by inspecting the code through Reflector; the documentation says this property is "null by default", whatever that means --KRML
- if (0 <= CommandLineOptions.Clo.ProverKillTime) {
- psi.EnvironmentVariables["PROVER_KILL_TIME"] = CommandLineOptions.Clo.ProverKillTime.ToString();
- }
- if (0 <= CommandLineOptions.Clo.SimplifyProverMatchDepth) {
- psi.EnvironmentVariables["PROVER_MATCH_DEPTH"] = CommandLineOptions.Clo.SimplifyProverMatchDepth.ToString();
- }
- if (0 <= CommandLineOptions.Clo.ProverCCLimit) {
- psi.EnvironmentVariables["PROVER_CC_LIMIT"] = CommandLineOptions.Clo.ProverCCLimit.ToString();
- }
- return psi;
- }
-
-
- public override string OptionComments() {
- Contract.Ensures(Contract.Result<string>() != null);
-
- // would we want the timeout stuff here?
- return "";
- }
-
- [NotDelayed]
- // TODO it complains about things not beeing peer consistent upon call to EatPrompt()
- // not sure what is it about... --micmo
- [Verify(false)]
- public SimplifyProverProcess(string proverPath):base(getPSI(proverPath),proverPath)
- //modifies Console.Out.*, Console.Error.*;
- {
- Contract.Requires(proverPath != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- EatPrompt();
- }
-
- private void EatPrompt()
- //modifies this.*;
- //modifies Console.Out.*, Console.Error.*;
- {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- // skips text matching the regular expression: (white space)* ">\t"
- ToFlush();
-
- int ch = 0;
- do {
- ch = FromReadChar();
- } while (Char.IsWhiteSpace((char)ch));
-
- while (ch == 'W') {
- ch = ConsumeWarnings(ch, null);
- }
-
- Expect(ch, ">\t");
- }
-
- public override void AddAxioms(string s) {
- //Contract.Requires(s != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- //ToWriteLine("(PROMPT_OFF)");
- base.AddAxioms(s);
- //ToWriteLine("(PROMPT_ON)");
- EatPrompt();
- }
-
- public override void Feed(string s, int statementCount) {
- //Contract.Requires(s != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- //ToWriteLine("(PROMPT_OFF)");
- base.Feed(s, statementCount);
- //ToWriteLine("(PROMPT_ON)");
- for (int i = 0; i < statementCount; i++) {
- EatPrompt();
- }
- }
-
- public override void PopAxioms() {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- base.PopAxioms();
- EatPrompt();
- }
-
- protected override void DoBeginCheck(string descriptiveName, string formula) {
- //Contract.Requires(descriptiveName != null);
- //Contract.Requires(formula != null);
- //simplify.Refresh();
- //this.Comment("@@@@ Virtual Memory: " + simplify.PeakVirtualMemorySize64);
- //this.Comment("@@@@ Working Set: " + simplify.PeakWorkingSet64);
- //this.Comment("@@@@ Paged Memory: " + simplify.PeakPagedMemorySize64);
-
- ToWriteLine(formula);
- ToFlush();
- }
-
- public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler handler) {
- //Contract.Requires(handler != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- ProverOutcome outcome;
-
- if (this.simplify == null) {
- return ProverOutcome.Inconclusive;
- }
-
- int ch = FromReadChar();
- while (ch == 'W') {
- ch = ConsumeWarnings(ch, handler);
- }
- if (ch == 'E') {
- Expect(ch, "Exceeded PROVER_KILL_TIME -- discontinuing search for counterexamples.");
- FromReadLine();
- ch = FromReadChar();
- if (ch == '\n') {
- ch = FromReadChar();
- }
- Expect(ch, " labels:");
- FromReadLine();
- ch = FromReadChar();
- ch = FromReadChar();
- ch = FromReadChar();
- FromReadLine();
- ch = FromReadChar();
- ch = FromReadChar();
- ch = FromReadChar();
- return ProverOutcome.TimeOut;
- }
- if ('0' <= ch && ch <= '9') {
- // Valid!
- do {
- ch = FromReadChar();
- } while ('0' <= ch && ch <= '9');
- Expect(ch, ": Valid.");
- outcome = ProverOutcome.Valid;
- ToWriteLine(String.Format("; FORMULA {0} IS VALID!", NumFormulasChecked + 1 /*Simplify starts at 1*/));
- } else {
- // now we expect one or more counterexample contexts, each proving a list of labels
- do {
- List<string> labels = ReadLabels(ch);
- handler.OnModel(labels, null);
- ch = FromReadChar();
- } while (ch == 'C');
- // now we expect "<N>: Invalid" where <N> is some number
- while ('0' <= ch && ch <= '9') {
- ch = FromReadChar();
- }
- Expect(ch, ": Invalid.");
- outcome = ProverOutcome.NotValid;
- ToWriteLine(String.Format("; FORMULA {0} IS INVALID", NumFormulasChecked + 1 /*Simplify starts at 1*/));
- }
-
- EatPrompt();
- return outcome;
- }
-
- List<string/*!>!*/> ReadLabels(int ch)
- //modifies this.*;
- {
- Contract.Ensures(Contract.Result<List<string>>() != null);
-
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- Expect(ch, "Counterexample:\n"); // FIX! ? Is there a problem with \r\n here?
- ch = FromReadChar();
- List<string> theLabels;
- if (ch == ' ') {
- // there are labels
- Expect(ch, " labels: ");
- string labels = FromReadLine(); // reads "(A B C ...)\n"
- theLabels = ParseLabels(labels);
- ch = FromReadChar();
- } else {
- theLabels = new List<string>();
- }
- Expect(ch, "\n"); // empty line
-
- return theLabels;
- }
-
- int ConsumeWarnings(int ch, Microsoft.Boogie.ProverInterface.ErrorHandler handler)
- //modifies this.*;
- //modifies Console.Out.*, Console.Error.*;
- {
- Contract.Requires(ch == 'W');
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- Expect(ch, "Warning: ");
- string w = FromReadLine();
- if (w.StartsWith("triggerless quantifier body")) {
- FromReadLine(); // blank line
- w = "triggerless quantifier body: " + FromReadLine(); // expression (body)
- FromReadLine(); // blank line
- FromReadLine(); // "with X pattern variable(s)...
- FromReadLine(); // blank line
- FromReadLine(); // expression (entire quantifier)
- }
-
- if (handler != null)
- handler.OnProverWarning(w);
-
- ch = FromReadChar();
- if (ch == '\n') {
- // make up for a poorly designed ReadLine routine (only the first
- // character of the DOS end-of-line sequence "\r\n" is read)
- ch = FromReadChar();
- }
- return ch;
- }
- }
-
-} \ No newline at end of file
diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs
deleted file mode 100644
index 4584b2e7..00000000
--- a/Source/Provers/Simplify/ProverInterface.cs
+++ /dev/null
@@ -1,868 +0,0 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Threading;
-using System.IO;
-using System.Text;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using Microsoft.Boogie.AbstractInterpretation;
-using Microsoft.Boogie.Simplify;
-using Microsoft.Boogie.VCExprAST;
-using Microsoft.Boogie.TypeErasure;
-using System.Text.RegularExpressions;
-
-namespace Microsoft.Boogie.Simplify {
- public abstract class LogProverInterface : ProverInterface {
- [NotDelayed]
- protected LogProverInterface(ProverOptions options,
- string openComment, string closeComment,
- string openActivity, string closeActivity,
- VCExpressionGenerator gen) {
- Contract.Requires(options != null);
- Contract.Requires(openComment != null);
- Contract.Requires(closeComment != null);
- Contract.Requires(openActivity != null);
- Contract.Requires(closeActivity != null);
- Contract.Requires(gen != null);
- Contract.Ensures(this.gen == gen);
- if (options.SeparateLogFiles) {
- this.commonPrefix = new List<string>();
- } else {
- this.logFileWriter = options.OpenLog(null);
- }
- this.openCommentString = openComment;
- this.closeCommentString = closeComment;
- this.openActivityString = openActivity;
- this.closeActivityString = closeActivity;
- this.gen = gen;
- this.options = options;
-
- if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never) {
- // Emit version comment in the log
- LogCommonComment(CommandLineOptions.Clo.Version);
- LogCommonComment(CommandLineOptions.Clo.Environment);
- }
- }
-
- [StrictReadonly]
- [Additive]
- protected readonly VCExpressionGenerator gen;
-
- private TextWriter/*?*/ logFileWriter;
- [StrictReadonly]
- private readonly string openCommentString;
- [StrictReadonly]
- private readonly string closeCommentString;
- [StrictReadonly]
- private readonly string openActivityString;
- [StrictReadonly]
- private readonly string closeActivityString;
- [StrictReadonly]
- protected readonly ProverOptions options;
- [StrictReadonly]
- private readonly List<string>/*?*/ commonPrefix;
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(openCommentString != null);
- Contract.Invariant(closeCommentString != null);
- Contract.Invariant(openActivityString != null);
- Contract.Invariant(closeActivityString != null);
- Contract.Invariant(options != null);
- Contract.Invariant(commonPrefix == null || cce.NonNullElements(commonPrefix));
- }
-
-
- public void LogActivity(string s) {
- Contract.Requires(s != null);
- LogActivity(s, false);
- }
-
- public void LogCommon(string s) {
- Contract.Requires(s != null);
- LogActivity(s, true);
- }
-
- private void LogActivity(string s, bool common) {
- Contract.Requires(s != null);
- Contract.Assume(common || !options.SeparateLogFiles || logFileWriter != null);
- if (logFileWriter != null) {
- logFileWriter.Write(openActivityString);
- logFileWriter.Write(s);
- logFileWriter.WriteLine(closeActivityString);
- logFileWriter.Flush();
- }
- if (common && commonPrefix != null) {
- commonPrefix.Add(openActivityString + s + closeActivityString);
- }
- }
-
- /// <summary>
- /// Write "comment" to logfile, if any, formatted as a comment for the theorem prover at hand.
- /// Assumes that "comment" does not contain any characters that would prematurely terminate
- /// the comment (like, perhaps, a newline or "*/").
- /// </summary>
- public override void LogComment(string comment) {
- //Contract.Requires(comment != null);
- LogComment(comment, false);
- }
-
- public void LogCommonComment(string comment) {
- Contract.Requires(comment != null);
- LogComment(comment, true);
- }
-
- private void LogComment(string comment, bool common) {
- Contract.Requires(comment != null);
- Contract.Assume(common || !options.SeparateLogFiles || logFileWriter != null);
- if (logFileWriter != null) {
- logFileWriter.Write(openCommentString);
- logFileWriter.Write(comment);
- logFileWriter.WriteLine(closeCommentString);
- logFileWriter.Flush();
- }
- if (common && commonPrefix != null) {
- commonPrefix.Add(openCommentString + comment + closeCommentString);
- }
- }
-
- public virtual void NewProblem(string descName) {
- Contract.Requires(descName != null);
- if (commonPrefix != null) {
- if (logFileWriter != null) {
- logFileWriter.Close();
- }
- logFileWriter = options.OpenLog(descName);
- if (logFileWriter != null) {
- foreach (string s in commonPrefix) {
- Contract.Assert(s != null);
- logFileWriter.WriteLine(s);
- }
- }
- }
- LogComment("Proof obligation: " + descName);
- }
-
- public override void Close() {
- if (logFileWriter != null) {
- logFileWriter.Close();
- logFileWriter = null;
- }
- }
-
- public override VCExpressionGenerator VCExprGen {
- get {
- Contract.Ensures(Contract.Result<VCExpressionGenerator>() != null);
- return this.gen;
- }
- }
- }
-
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- [ContractClass(typeof(ProcessTheoremProverContracts))]
- public abstract class ProcessTheoremProver : LogProverInterface {
- private static string _proverPath;
-
- protected AxiomVCExprTranslator vcExprTranslator {
- get {
- Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);
-
- return cce.NonNull((AxiomVCExprTranslator)ctx.exprTranslator);
- }
- }
-
- protected abstract AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions p);
-
- // Return the number of axioms pushed to the theorem prover
- protected int FeedNewAxiomsDecls2Prover() {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- if (thmProver == null)
- return 0;
- int ret = 0;
- foreach (string s in vcExprTranslator.NewTypeDecls) {
- Contract.Assert(s != null);
- LogCommon(s);
- thmProver.Feed(s, 0);
- }
- foreach (string s in vcExprTranslator.NewAxioms) {
- Contract.Assert(s != null);
- LogBgPush(s);
- thmProver.AddAxioms(s);
- ret++;
- }
- return ret;
- }
-
- protected static string CodebaseString() {
- Contract.Ensures(Contract.Result<string>() != null);
-
- return Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location));
- }
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(cce.NonNullDictionaryAndValues(BackgroundPredicates));
- Contract.Invariant(BackgroundPredFilename != null);
- Contract.Invariant(ctx != null);
- }
-
- private static IDictionary<string/*!*/, string/*!>!*/> BackgroundPredicates =
- new Dictionary<string/*!*/, string/*!*/>();
-
- protected static string GetBackgroundPredicate(string filename) {
- Contract.Requires(filename != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- string res;
- if (!BackgroundPredicates.TryGetValue(filename, out res)) {
- // do we have to lock/synchronise anything?
- string univBackPredPath = Path.Combine(CodebaseString(), filename);
- using (StreamReader reader = new System.IO.StreamReader(univBackPredPath)) {
- res = reader.ReadToEnd();
- }
- BackgroundPredicates.Add(filename, res);
- }
- return cce.NonNull(res);
- }
-
- static void InitializeGlobalInformation(string proverExe)
- // throws ProverException, System.IO.FileNotFoundException;
- {
- Contract.Requires(proverExe != null);
- Contract.Ensures(_proverPath != null);
-
- if (CommandLineOptions.Clo.Z3ExecutablePath != null) {
- _proverPath = CommandLineOptions.Clo.Z3ExecutablePath;
- }
-
- if (_proverPath == null) {
- // Initialize '_proverPath'
- _proverPath = Path.Combine(CodebaseString(), proverExe);
- string firstTry = _proverPath;
-
- if (File.Exists(firstTry))
- return;
-
- string programFiles = Environment.GetEnvironmentVariable("ProgramFiles");
- Contract.Assert(programFiles != null);
- string programFilesX86 = Environment.GetEnvironmentVariable("ProgramFiles(x86)");
- if (programFiles.Equals(programFilesX86)) {
- // If both %ProgramFiles% and %ProgramFiles(x86)% point to "ProgramFiles (x86)", use %ProgramW6432% instead.
- programFiles = Environment.GetEnvironmentVariable("ProgramW6432");
- }
-
-
- List<string> z3Dirs = new List<string>();
- if (Directory.Exists(programFiles + @"\Microsoft Research\")) {
- string msrDir = programFiles + @"\Microsoft Research\";
- z3Dirs.AddRange(Directory.GetDirectories(msrDir, "Z3-*"));
- }
- if (Directory.Exists(programFilesX86 + @"\Microsoft Research\")) {
- string msrDir = programFilesX86 + @"\Microsoft Research\";
- z3Dirs.AddRange(Directory.GetDirectories(msrDir, "Z3-*"));
- }
-
- // Look for the most recent version of Z3.
- int minor = 0, major = 0;
- string winner = null;
- Regex r = new Regex(@"^Z3-(\d+)\.(\d+)$");
- foreach (string d in z3Dirs) {
- string name = new DirectoryInfo(d).Name;
- foreach (Match m in r.Matches(name)) {
- int ma, mi;
- ma = int.Parse(m.Groups[1].ToString());
- mi = int.Parse(m.Groups[2].ToString());
- if (major < ma || (major == ma && minor < mi)) {
- major = ma;
- minor = mi;
- winner = d;
- }
- }
- }
-
- if (major == 0 && minor == 0) {
- throw new ProverException("Cannot find executable: " + firstTry);
- }
- Contract.Assert(winner != null);
-
- _proverPath = Path.Combine(Path.Combine(winner, "bin"), proverExe);
- if (!File.Exists(_proverPath)) {
- throw new ProverException("Cannot find prover: " + _proverPath);
- }
-
- if (CommandLineOptions.Clo.Trace) {
- Console.WriteLine("[TRACE] Using prover: " + _proverPath);
- }
- }
- }
-
- [Rep]
- protected internal ProverProcess thmProver;
- bool currentProverHasBeenABadBoy = false;
- // invariant currentProverHasBeenABadBoy ==> thmProver != null;
- protected int restarts = 0;
- protected DeclFreeProverContext ctx;
- protected string BackgroundPredFilename;
- protected ConsoleCancelEventHandler cancelEvent;
-
- [NotDelayed]
- public ProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen, DeclFreeProverContext ctx,
- string proverExe, string backgroundPred)
- : base(options, "; ", "", "", "", gen) {
- Contract.Requires(options != null);
- Contract.Requires(gen != null);
- Contract.Requires(ctx != null);
- Contract.Requires(proverExe != null);
- Contract.Requires(backgroundPred != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- BackgroundPredFilename = backgroundPred;
- InitializeGlobalInformation(proverExe);
- this.ctx = ctx;
-
-
- // ensure that a VCExprTranslator is available
- // if none exists so far, we have to create a new one
- // from scratch and feed the axioms to it
- if (ctx.exprTranslator == null) {
- AxiomVCExprTranslator tl = SpawnVCExprTranslator(options);
- ctx.exprTranslator = tl;
- tl.AddAxiom(tl.translate(ctx.Axioms, -1));
- // we clear the lists with new axioms and declarations;
- // they are not needed at this point
- List<string> x = tl.NewAxioms;
- //x = x; // make the compiler happy: somebody uses the value of x
- x = tl.NewTypeDecls;
- }
- }
-
- /// <summary>
- /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)
- /// </summary>
- public override void PushVCExpression(VCExpr vc) {
- //Contract.Requires(vc != null);
- vcExprTranslator.AddAxiom(vcExprTranslator.translate(vc, 1));
- }
-
- public override string VCExpressionToString(VCExpr vc) {
- //Contract.Requires(vc != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- return vcExprTranslator.translate(vc, 1);
- }
-
- // Number of axioms pushed since the last call to Check
- public override int NumAxiomsPushed() {
- return vcExprTranslator.NewAxiomsCount;
- }
-
- // Feed the axioms pushed since the last call to Check to the theorem prover
- public override int FlushAxiomsToTheoremProver() {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- return FeedNewAxiomsDecls2Prover();
- }
-
- public override void Pop() {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- Contract.Assert(thmProver != null);
- LogCommon("(BG_POP)");
- thmProver.PopAxioms();
- }
-
- [NoDefaultContract] // important, since we have no idea what state the object might be in when this handler is invoked
- void ControlCHandler(object o, ConsoleCancelEventArgs a) {
- if (thmProver != null) {
- thmProver.Kill();
- }
- }
-
- public override void Close() {
- if (cancelEvent != null) {
- Console.CancelKeyPress -= cancelEvent;
- cancelEvent = null;
- }
- if (thmProver != null) {
- cce.BeginExpose(this);
- {
- thmProver.Close();
- thmProver = null;
- currentProverHasBeenABadBoy = false;
- }
- cce.EndExpose();
- }
- base.Close();
- }
-
- private UnexpectedProverOutputException proverException;
-
- public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) {
- //Contract.Requires(descriptiveName != null);
- //Contract.Requires(vc != null);
- //Contract.Requires(handler != null);
- this.NewProblem(descriptiveName);
- this.proverException = null;
-
- try {
- this.ResurrectProver();
-
- string vcString = vcExprTranslator.translate(vc, 1);
-
- Helpers.ExtraTraceInformation("Sending data to theorem prover");
-
- int num_axioms_pushed =
- FeedNewAxiomsDecls2Prover();
-
- LogActivity(vcString);
-
- Contract.Assert(thmProver != null);
- thmProver.BeginCheck(descriptiveName, vcString);
-
- if (CommandLineOptions.Clo.StratifiedInlining > 0) {
- // Pop all the axioms that were pushed by FeedNewAxiomsDecls2Prover
- for (int i = 0; i < num_axioms_pushed; i++) {
- LogBgPop();
- thmProver.PopAxioms();
- }
- }
-
- if (CommandLineOptions.Clo.RestartProverPerVC) {
- LogComment("Will restart the prover due to /restartProver option");
- currentProverHasBeenABadBoy = true;
- }
- } catch (UnexpectedProverOutputException e) {
- proverException = e;
- }
- }
-
- public override Outcome CheckOutcome(ErrorHandler handler) {
- //Contract.Requires(handler != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
-
- if (this.thmProver == null) {
- return Outcome.Undetermined;
- }
-
- if (proverException == null) {
- try {
- ProverProcess.ProverOutcome result = thmProver.CheckOutcome(handler);
-
- if (options.ForceLogStatus) {
- switch (result) {
- case ProverProcess.ProverOutcome.Valid:
- LogActivity("DBG_WAS_VALID");
- break;
- case ProverProcess.ProverOutcome.NotValid:
- LogActivity("DBG_WAS_INVALID");
- break;
- }
- }
-
- switch (result) {
- case ProverProcess.ProverOutcome.Valid:
- return Outcome.Valid;
- case ProverProcess.ProverOutcome.TimeOut:
- return Outcome.TimeOut;
- case ProverProcess.ProverOutcome.OutOfMemory:
- return Outcome.OutOfMemory;
- case ProverProcess.ProverOutcome.Inconclusive:
- return Outcome.Undetermined;
- case ProverProcess.ProverOutcome.NotValid:
- return Outcome.Invalid;
- }
- } catch (UnexpectedProverOutputException e) {
- proverException = e;
- }
- }
-
- Contract.Assume(proverException != null);
- LogComment("***** Unexpected prover output");
- cce.BeginExpose(this);
- {
- currentProverHasBeenABadBoy = true; // this will cause the next resurrect to restart the prover
- }
- cce.EndExpose();
- throw proverException;
- }
-
- protected virtual void ResurrectProver() {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- cce.BeginExpose(this);
- {
- if (thmProver != null) {
- if (thmProver.HasExited) {
- DateTime now = DateTime.Now;
- LogComment("***** Prover Crashed at or before " + now.ToString("G"));
-
- } else if (CommandLineOptions.Clo.MaxProverMemory > 0 &&
- thmProver.NumFormulasChecked > CommandLineOptions.Clo.MinNumOfProverCalls &&
- thmProver.PeakVirtualMemorySize > CommandLineOptions.Clo.MaxProverMemory) {
- LogComment("***** Exceeded memory limit. Peak memory usage so far: " +
- thmProver.PeakVirtualMemorySize / CommandLineOptions.Megabyte + "MB");
-
- } else if (!currentProverHasBeenABadBoy) {
- // prover is ready to go
- return;
- }
-
- thmProver.Close();
- thmProver = null;
- currentProverHasBeenABadBoy = false;
- restarts++;
-
- if (CommandLineOptions.Clo.StratifiedInlining > 0)
- {
- Console.WriteLine("Warning: restarting theorem prover. Context could be lost");
- }
- }
-
- FireUpNewProver();
- }
- cce.EndExpose();
- }
-
- protected abstract ProverProcess CreateProverProcess(string proverPath);
-
- public void LogBgPush(string s) {
- Contract.Requires(s != null);
- LogCommon("(BG_PUSH ");
- LogCommon(s);
- LogCommon(")");
- }
-
- public void LogBgPop() {
- LogCommon("(BG_POP)");
- }
-
- [NoDefaultContract]
- private void FireUpNewProver()
- {
- Contract.Requires( cce.IsExposed(this));
- Contract.Requires( thmProver == null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
-
- if (cancelEvent == null && CommandLineOptions.Clo.RunningBoogieFromCommandLine) {
- cancelEvent = new ConsoleCancelEventHandler(ControlCHandler);
- Console.CancelKeyPress += cancelEvent;
- }
- thmProver = CreateProverProcess(_proverPath);
- if (restarts == 0) {
- foreach (string s in thmProver.OptionComments().Split('\n')) {Contract.Assert(s != null);
- LogCommonComment(s);
- }
- foreach (string parmsetting in thmProver.ParameterSettings) {Contract.Assert(parmsetting != null);
- LogCommon(parmsetting);
- }
- }
- foreach (string parmsetting in thmProver.ParameterSettings) {Contract.Assert(parmsetting != null);
- thmProver.Feed(parmsetting, 0);
- }
- thmProver.Feed(GetBackgroundPredicate(BackgroundPredFilename), 3);
-
- if (restarts == 0) {
- // log the stuff before feeding it into the prover, so when it dies
- // and takes Boogie with it, we know what happened
- LogCommon(GetBackgroundPredicate(BackgroundPredFilename));
-
- foreach (string s in vcExprTranslator.AllTypeDecls){Contract.Assert(s != null);
- LogCommon(s);}
- foreach (string s in vcExprTranslator.AllAxioms){Contract.Assert(s != null);
- LogBgPush(s);}
-
- LogCommonComment("Initialized all axioms.");
- }
-
- foreach (string s in vcExprTranslator.AllTypeDecls){Contract.Assert(s != null);
- thmProver.Feed(s, 0);}
- foreach (string s in vcExprTranslator.AllAxioms){Contract.Assert(s != null);
- thmProver.AddAxioms(s);}
-
- // we have sent everything to the prover and can clear the lists with
- // new axioms and declarations
- List<string> x = vcExprTranslator.NewAxioms;
- //x = x; // make the compiler happy: somebody uses the value of x
- x = vcExprTranslator.NewTypeDecls;
- }
-
- public override ProverContext Context {
- get {
- Contract.Ensures(Contract.Result<ProverContext>() != null);
- return this.ctx;
- }
- }
- }
- [ContractClassFor(typeof(ProcessTheoremProver))]
- public abstract class ProcessTheoremProverContracts :ProcessTheoremProver{
- protected override AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions p) {
- Contract.Requires(p != null);
- Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);
- throw new NotImplementedException();
-
- }
- protected override ProverProcess CreateProverProcess(string proverPath) {
- Contract.Requires(proverPath != null);
- Contract.Ensures(Contract.Result<ProverProcess>() != null);
- throw new NotImplementedException();
- }
- [NotDelayed]
- public ProcessTheoremProverContracts(ProverOptions options, VCExpressionGenerator gen, DeclFreeProverContext ctx,
- string proverExe, string backgroundPred):base(options,gen,ctx,proverExe,backgroundPred)
- {throw new NotImplementedException();}
- }
-
- public class SimplifyTheoremProver : ProcessTheoremProver {
- [NotDelayed]
- public SimplifyTheoremProver(ProverOptions options, VCExpressionGenerator gen, DeclFreeProverContext ctx)
- : base(options, gen, ctx, "simplify.exe", "UnivBackPred2.sx") {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- }
-
- protected override ProverProcess CreateProverProcess(string proverPath) {
- //Contract.Requires(proverPath != null);
- Contract.Ensures(Contract.Result<ProverProcess>() != null);
-
- return new SimplifyProverProcess(proverPath);
- }
-
- protected override AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions opts) {
- //Contract.Requires(opts!=null);
- Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);
-
- return new SimplifyVCExprTranslator(gen);
- }
- }
-
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
-
- public abstract class AxiomVCExprTranslator : VCExprTranslator {
- protected AxiomVCExprTranslator() {
- AllAxioms = new List<string> ();
- NewAxiomsAttr = new List<string> ();
- AllTypeDecls = new List<string> ();
- NewTypeDeclsAttr = new List<string> ();
- }
-
- protected AxiomVCExprTranslator(AxiomVCExprTranslator tl) {
- Contract.Requires(tl != null);
- AllAxioms = new List<string>(tl.AllAxioms);
- NewAxiomsAttr = new List<string>(tl.NewAxiomsAttr);
- AllTypeDecls = new List<string>(tl.AllTypeDecls);
- NewTypeDeclsAttr = new List<string>(tl.NewTypeDeclsAttr);
- }
-
- // we store all typing-related axioms that have been sent to the prover
- // so that the prover can be re-initialised in case it dies
- public readonly List<string/*!>!*/> AllAxioms;
- private List<string/*!>!*/> NewAxiomsAttr;
-
- // The length of the list NewAxiomsAttr
- public int NewAxiomsCount {
- get {
- return NewAxiomsAttr.Count;
- }
- }
-
- public List<string/*!>!*/> NewAxioms {
- get {
- Contract.Ensures(Contract.Result<List<string>>() != null);
-
- List<string/*!>!*/> res = NewAxiomsAttr;
- NewAxiomsAttr = new List<string>();
- return res;
- }
- }
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(AllAxioms != null);
- Contract.Invariant(NewAxiomsAttr != null);
- Contract.Invariant(AllTypeDecls != null);
- Contract.Invariant(NewTypeDeclsAttr != null);
- }
-
-
- // similarly, a list of declarations that have been sent to the prover
- public readonly List<string/*!>!*/> AllTypeDecls;
- private List<string/*!>!*/> NewTypeDeclsAttr;
-
- public List<string>/*!>!*/ NewTypeDecls {
- get {
- List<string/*!>!*/> res = NewTypeDeclsAttr;
- NewTypeDeclsAttr = new List<string/*!*/>();
- return res;
- }
- }
-
- public void AddAxiom(string axiom) {
- Contract.Requires(axiom != null);
- AllAxioms.Add(axiom);
- NewAxiomsAttr.Add(axiom);
- }
-
- public void AddTypeDecl(string typeDecl) {
- Contract.Requires(typeDecl != null);
- AllTypeDecls.Add(typeDecl);
- NewTypeDeclsAttr.Add(typeDecl);
- }
- }
-
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
-
- public class SimplifyVCExprTranslator : AxiomVCExprTranslator {
- public SimplifyVCExprTranslator(VCExpressionGenerator gen) {
- Contract.Requires(gen != null);
- Gen = gen;
- TypeAxiomBuilder axBuilder;
- switch (CommandLineOptions.Clo.TypeEncodingMethod) {
- case CommandLineOptions.TypeEncoding.Arguments:
- axBuilder = new TypeAxiomBuilderArguments(gen);
- break;
- default:
- axBuilder = new TypeAxiomBuilderPremisses(gen);
- break;
- }
- axBuilder.Setup();
- AxBuilder = axBuilder;
- Namer = new UniqueNamer();
- LitAbstracter = new BigLiteralAbstracter(gen);
- }
-
- private SimplifyVCExprTranslator(SimplifyVCExprTranslator tl)
- : base(tl) {
- Contract.Requires(tl != null);
- Gen = tl.Gen;
- AxBuilder = (TypeAxiomBuilder)tl.AxBuilder.Clone();
- Namer = (UniqueNamer)tl.Namer.Clone();
- LitAbstracter = (BigLiteralAbstracter)tl.LitAbstracter.Clone();
- }
-
- public override Object Clone() {
- Contract.Ensures(Contract.Result<object>() != null);
-
- return new SimplifyVCExprTranslator(this);
- }
-
- private readonly VCExpressionGenerator Gen;
- private readonly TypeAxiomBuilder AxBuilder;
- private readonly UniqueNamer Namer;
- private readonly BigLiteralAbstracter LitAbstracter;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(Gen != null);
- Contract.Invariant(AxBuilder != null);
- Contract.Invariant(Namer != null);
- Contract.Invariant(LitAbstracter != null);
- }
-
-
- public override string Lookup(VCExprVar var) {
- //Contract.Requires(var != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- VCExprVar v = AxBuilder.TryTyped2Untyped(var);
- if (v != null) {
- var = v;
- }
- return Namer.Lookup(var);
- }
-
- public override string translate(VCExpr expr, int polarity) {
- //Contract.Requires(expr != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- Let2ImpliesMutator letImplier = new Let2ImpliesMutator(Gen);
- Contract.Assert(letImplier != null);
-
- // handle the types in the VCExpr
- TypeEraser eraser;
- switch (CommandLineOptions.Clo.TypeEncodingMethod) {
- case CommandLineOptions.TypeEncoding.Arguments:
- eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, Gen);
- break;
- case CommandLineOptions.TypeEncoding.Monomorphic:
- eraser = null;
- break;
- default:
- eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);
- break;
- }
- VCExpr exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;
- Contract.Assert(exprWithoutTypes != null);
-
- TermFormulaFlattener flattener = new TermFormulaFlattener(Gen);
- Contract.Assert(flattener != null);
- VCExpr exprWithLet = flattener.Flatten(exprWithoutTypes);
- Contract.Assert(exprWithLet != null);
- VCExpr exprWithoutLet = letImplier.Mutate(exprWithLet);
- Contract.Assert(exprWithoutLet != null);
-
- // big integer literals
- VCExpr exprWithoutBigLits = LitAbstracter.Abstract(exprWithoutLet);
- Contract.Assert(exprWithoutBigLits != null);
- AddAxiom(SimplifyLikeExprLineariser.ToSimplifyString(LitAbstracter.GetNewAxioms(),
- Namer));
-
- // type axioms
- VCExpr axiomsWithLet = flattener.Flatten(AxBuilder.GetNewAxioms());
- Contract.Assert(axiomsWithLet != null);
- VCExpr axiomsWithoutLet = letImplier.Mutate(axiomsWithLet);
- Contract.Assert(axiomsWithoutLet != null);
-
- AddAxiom(SimplifyLikeExprLineariser.ToSimplifyString(axiomsWithoutLet, Namer));
- return SimplifyLikeExprLineariser.ToSimplifyString(exprWithoutBigLits, Namer);
- }
- }
-
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
-
- public class Factory : ProverFactory {
- public override object SpawnProver(ProverOptions options, object ctxt) {
- //Contract.Requires(options != null);
- //Contract.Requires(ctxt != null);
- Contract.Ensures(Contract.Result<object>() != null);
-
- return new SimplifyTheoremProver(options,
- cce.NonNull((DeclFreeProverContext)ctxt).ExprGen,
- cce.NonNull((DeclFreeProverContext)ctxt));
- }
-
- public override object NewProverContext(ProverOptions options) {
- //Contract.Requires(options != null);
- Contract.Ensures(Contract.Result<object>() != null);
-
- if (CommandLineOptions.Clo.BracketIdsInVC < 0) {
- CommandLineOptions.Clo.BracketIdsInVC = 1;
- }
- VCExpressionGenerator gen = new VCExpressionGenerator();
- Contract.Assert(gen != null);
- List<string>/*!>!*/ proverCommands = new List<string> ();
- Contract.Assert(cce.NonNullElements(proverCommands));
- proverCommands.Add("simplify");
- return new DeclFreeProverContext(gen, new VCGenerationOptions(proverCommands));
- }
-
- public override CommandLineOptions.VCVariety DefaultVCVariety {
- get {
- return CommandLineOptions.VCVariety.BlockNested;
- }
- }
-
- // needed to make test7 pass
- public override bool SupportsDags {
- get {
- return true;
- }
- }
- }
-}
diff --git a/Source/Provers/Simplify/Simplify.csproj b/Source/Provers/Simplify/Simplify.csproj
deleted file mode 100644
index 81d2f90a..00000000
--- a/Source/Provers/Simplify/Simplify.csproj
+++ /dev/null
@@ -1,210 +0,0 @@
-<?xml version="1.0" encoding="utf-8"?>
-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
- <PropertyGroup>
- <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
- <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
- <ProductVersion>9.0.21022</ProductVersion>
- <SchemaVersion>2.0</SchemaVersion>
- <ProjectGuid>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</ProjectGuid>
- <OutputType>Library</OutputType>
- <AppDesignerFolder>Properties</AppDesignerFolder>
- <RootNamespace>Microsoft.Boogie.Simplify</RootNamespace>
- <AssemblyName>Provers.Simplify</AssemblyName>
- <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
- <FileAlignment>512</FileAlignment>
- <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
- <SignAssembly>true</SignAssembly>
- <AssemblyOriginatorKeyFile>..\..\InterimKey.snk</AssemblyOriginatorKeyFile>
- <FileUpgradeFlags>
- </FileUpgradeFlags>
- <OldToolsVersion>3.5</OldToolsVersion>
- <UpgradeBackupLocation />
- <PublishUrl>publish\</PublishUrl>
- <Install>true</Install>
- <InstallFrom>Disk</InstallFrom>
- <UpdateEnabled>false</UpdateEnabled>
- <UpdateMode>Foreground</UpdateMode>
- <UpdateInterval>7</UpdateInterval>
- <UpdateIntervalUnits>Days</UpdateIntervalUnits>
- <UpdatePeriodically>false</UpdatePeriodically>
- <UpdateRequired>false</UpdateRequired>
- <MapFileExtensions>true</MapFileExtensions>
- <ApplicationRevision>0</ApplicationRevision>
- <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
- <IsWebBootstrapper>false</IsWebBootstrapper>
- <UseApplicationTrust>false</UseApplicationTrust>
- <BootstrapperEnabled>true</BootstrapperEnabled>
- <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>
- <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly>
- </CodeContractsCustomRewriterAssembly>
- <CodeContractsCustomRewriterClass>
- </CodeContractsCustomRewriterClass>
- <CodeContractsLibPaths>
- </CodeContractsLibPaths>
- <CodeContractsExtraRewriteOptions>
- </CodeContractsExtraRewriteOptions>
- <CodeContractsExtraAnalysisOptions>
- </CodeContractsExtraAnalysisOptions>
- <CodeContractsBaseLineFile>
- </CodeContractsBaseLineFile>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </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>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\z3apidebug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisRuleAssemblies>
- </CodeAnalysisRuleAssemblies>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>Migrated rules for Simplify.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\Checked\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisLogFile>bin\Debug\Provers.Simplify.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
- <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
- </PropertyGroup>
- <ItemGroup>
- <Reference Include="System" />
- <Reference Include="System.Data" />
- <Reference Include="System.Xml" />
- </ItemGroup>
- <ItemGroup>
- <Compile Include="Let2ImpliesVisitor.cs" />
- <Compile Include="Prover.cs" />
- <Compile Include="ProverInterface.cs" />
- <Compile Include="..\..\version.cs" />
- </ItemGroup>
- <ItemGroup>
- <ProjectReference Include="..\..\AIFramework\AIFramework.csproj">
- <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
- <Name>AIFramework</Name>
- </ProjectReference>
- <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="..\..\VCExpr\VCExpr.csproj">
- <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
- <Name>VCExpr</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\VCGeneration\VCGeneration.csproj">
- <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
- <Name>VCGeneration</Name>
- </ProjectReference>
- </ItemGroup>
- <ItemGroup>
- <Folder Include="Properties\" />
- </ItemGroup>
- <ItemGroup>
- <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
- <Install>false</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
- <Visible>False</Visible>
- <ProductName>Windows Installer 3.1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- </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/Provers/Simplify/cce.cs b/Source/Provers/Simplify/cce.cs
deleted file mode 100644
index ef594484..00000000
--- a/Source/Provers/Simplify/cce.cs
+++ /dev/null
@@ -1,193 +0,0 @@
-using System;
-using SA=System.Attribute;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.Text;
-//using Microsoft.Boogie;
-
-/// <summary>
-/// A class containing static methods to extend the functionality of Code Contracts
-/// </summary>
-
-public static class cce {
- //[Pure]
- //public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {
- // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());
- //}
- [Pure]
- public static T NonNull<T>(T t) {
- Contract.Assert(t != null);
- return t;
- }
- [Pure]
- public static bool NonNullElements<T>(IEnumerable<T> collection) {
- return collection != null && Contract.ForAll(collection, c => c != null);
- }
- [Pure]
- public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {
- return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair));
- }
- //[Pure]
- //public static bool NonNullElements(VariableSeq collection) {
- // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);
- //}
- /// <summary>
- /// For possibly-null lists of non-null elements
- /// </summary>
- /// <typeparam name="T"></typeparam>
- /// <param name="collection"></param>
- /// <param name="nullability">If true, the collection is treated as an IEnumerable&lt;T!&gt;?, rather than an IEnumerable&lt;T!&gt;!</param>
- /// <returns></returns>
- [Pure]
- public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) {
- return (nullability && collection == null) || cce.NonNullElements(collection);
- //Should be the same as:
- /*if(nullability&&collection==null)
- * return true;
- * return cce.NonNullElements(collection)
- */
-
- }
- [Pure]
- public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {
- return kvp.Key != null && kvp.Value != null;
- }
- [Pure]
- public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {
- return iEnumerator != null;
- }
- //[Pure]
- //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {
- // return cce.NonNullElements(graph.TopologicalSort());
- //}
- [Pure]
- public static void BeginExpose(object o) {
- }
- [Pure]
- public static void EndExpose() {
- }
- [Pure]
- public static bool IsPeerConsistent(object o) {
- return true;
- }
- [Pure]
- public static bool IsConsistent(object o) {
- return true;
- }
- [Pure]
- public static bool IsExposable(object o) {
- return true;
- }
- [Pure]
- public static bool IsExposed(object o) {
- return true;
- }
- [Pure]
- public static bool IsNew(object o) {
- return true;
- }
- public static class Owner {
- [Pure]
- public static bool Same(object o, object p) {
- return true;
- }
- [Pure]
- public static void AssignSame(object o, object p) {
- }
- [Pure]
- public static object ElementProxy(object o) {
- return o;
- }
- [Pure]
- public static bool None(object o) {
- return true;
- }
- [Pure]
- public static bool Different(object o, object p) {
- return true;
- }
- [Pure]
- public static bool New(object o) {
- return true;
- }
- }
- [Pure]
- public static void LoopInvariant(bool p) {
- Contract.Assert(p);
- }
- public class UnreachableException : Exception {
- public UnreachableException() {
- }
- }
- //[Pure]
- //public static bool IsValid(Microsoft.Dafny.Expression expression) {
- // return true;
- //}
- //public static List<T> toList<T>(PureCollections.Sequence s) {
- // List<T> toRet = new List<T>();
- // foreach (T t in s.elems)
- // if(t!=null)
- // toRet.Add(t);
- // return toRet;
- //}
-
- //internal static bool NonNullElements(Set set) {
- // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);
- //}
-}
-
-public class PeerAttribute : SA {
-}
-public class RepAttribute : SA {
-}
-public class CapturedAttribute : SA {
-}
-public class NotDelayedAttribute : SA {
-}
-public class NoDefaultContractAttribute : SA {
-}
-public class VerifyAttribute : SA {
- public VerifyAttribute(bool b) {
-
- }
-}
-public class StrictReadonlyAttribute : SA {
-}
-public class AdditiveAttribute : SA {
-}
-public class ReadsAttribute : SA {
- public enum Reads {
- Nothing,
- Everything,
- };
- public ReadsAttribute(object o) {
- }
-}
-public class GlobalAccessAttribute : SA {
- public GlobalAccessAttribute(bool b) {
- }
-}
-public class EscapesAttribute : SA {
- public EscapesAttribute(bool b, bool b_2) {
- }
-}
-public class NeedsContractsAttribute : SA {
- public NeedsContractsAttribute() {
- }
- public NeedsContractsAttribute(bool ret, bool parameters) {
- }
- public NeedsContractsAttribute(bool ret, int[] parameters) {
- }
-}
-public class ImmutableAttribute : SA {
-}
-public class InsideAttribute : SA {
-}
-public class SpecPublicAttribute : SA {
-}
-public class ElementsPeerAttribute : SA {
-}
-public class ResultNotNewlyAllocatedAttribute : SA {
-}
-public class OnceAttribute : SA {
-} \ No newline at end of file
diff --git a/Source/Provers/Z3/Inspector.cs b/Source/Provers/Z3/Inspector.cs
deleted file mode 100644
index c9bdfa31..00000000
--- a/Source/Provers/Z3/Inspector.cs
+++ /dev/null
@@ -1,162 +0,0 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.IO;
-using System.Diagnostics;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-//using util;
-using Microsoft.Boogie;
-using Microsoft.Boogie.Simplify;
-using Microsoft.Basetypes;
-using Microsoft.Boogie.VCExprAST;
-
-namespace Microsoft.Boogie.Z3
-{
- internal class FindLabelsVisitor : TraversingVCExprVisitor<bool, bool> {
- public HashSet<string/*!*/>/*!*/ Labels = new HashSet<string/*!*/>();
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(cce.NonNull(Labels));
- }
-
-
- public static HashSet<string/*!*/>/*!*/ FindLabels(VCExpr/*!*/ expr) {
- Contract.Requires(expr != null);
- Contract.Ensures(cce.NonNull(Contract.Result<HashSet<string/*!*/>/*!*/>()));
-
- FindLabelsVisitor visitor = new FindLabelsVisitor();
- visitor.Traverse(expr, true);
- return visitor.Labels;
- }
-
- protected override bool StandardResult(VCExpr node, bool arg) {
- //Contract.Requires(node!=null);
- VCExprNAry nary = node as VCExprNAry;
- if (nary != null) {
- VCExprLabelOp lab = nary.Op as VCExprLabelOp;
- if (lab != null) {
- Labels.Add(lab.label);
- }
- }
- return true;
- }
- }
-
- internal class Inspector {
- [Rep] protected readonly Process inspector;
- [Rep] readonly TextReader fromInspector;
- [Rep] readonly TextWriter toInspector;
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(inspector!=null);
- Contract.Invariant(fromInspector!=null);
- Contract.Invariant(toInspector != null);
- }
-
-
- public Inspector(Z3InstanceOptions opts)
- {
- Contract.Requires(opts != null);
- ProcessStartInfo psi = new ProcessStartInfo(opts.Inspector);
- Contract.Assert(psi!=null);
- psi.CreateNoWindow = true;
- psi.UseShellExecute = false;
- psi.RedirectStandardInput = true;
- psi.RedirectStandardOutput = true;
- psi.RedirectStandardError = false;
-
- try
- {
- Process inspector = Process.Start(psi);
- this.inspector = inspector;
- fromInspector = inspector.StandardOutput;
- toInspector = inspector.StandardInput;
- }
- catch (System.ComponentModel.Win32Exception e)
- {
- throw new Exception(string.Format("Unable to start the inspector process {0}: {1}", opts.Inspector, e.Message));
- }
- }
-
- public void NewProver()
- {
- }
-
- public void NewProblem(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler)
- {
- Contract.Requires(descriptiveName != null);
- Contract.Requires(vc != null);
- Contract.Requires(handler != null);
- HashSet<string/*!*/>/*!*/ labels = FindLabelsVisitor.FindLabels(vc);
- Contract.Assert(labels!=null);
- toInspector.WriteLine("PROBLEM " + descriptiveName);
- toInspector.WriteLine("TOKEN BEGIN");
- foreach (string lab in labels) {
- Contract.Assert(lab!=null);
- string no = lab.Substring(1);
- Absy absy = handler.Label2Absy(no);
-
- IToken tok = absy.tok;
- AssertCmd assrt = absy as AssertCmd;
- Block blk = absy as Block;
- string val = tok.val; // might require computation, so cache it
- if (val == "foo" || tok.filename == null) continue; // no token
-
- toInspector.Write("TOKEN ");
- toInspector.Write(lab);
- toInspector.Write(" ");
-
- if (assrt != null) {
- toInspector.Write("ASSERT");
- string errData = assrt.ErrorData as string;
- if (errData != null) {
- val = errData;
- } else if (assrt.ErrorMessage != null) {
- val = assrt.ErrorMessage;
- }
- } else if (blk != null) {
- toInspector.Write("BLOCK ");
- toInspector.Write(blk.Label);
- } else {
- Contract.Assume( false);
- }
- if (val == null || val == "assert" || val == "ensures") { val = ""; }
-
- if (absy is LoopInitAssertCmd) {
- val += " (loop entry)";
- } else if (absy is LoopInvMaintainedAssertCmd) {
- val += " (loop body)";
- } else if (val.IndexOf("#VCCERR") >= 0) {
- // skip further transformations
- } else if (absy is AssertRequiresCmd) {
- AssertRequiresCmd req = (AssertRequiresCmd)absy;
- IToken t2 = req.Requires.tok;
- string tval = t2.val;
- if (tval == "requires")
- tval = string.Format("{0}({1},{2}))", t2.filename, t2.line, t2.col);
- string call = "";
- if (val != "call") call = " in call to " + val;
- val = string.Format("precondition {0}{1}", tval, call);
- }
-
- val = val.Replace("\r", "").Replace("\n", " ");
-
- toInspector.WriteLine(string.Format(" {0} {1} :@:{2}:@:{3}", tok.line, tok.col, tok.filename, val));
- }
- toInspector.WriteLine("TOKEN END");
- }
-
- public void StatsLine(string line)
- {
- Contract.Requires(line != null);
- toInspector.WriteLine(line);
- toInspector.Flush();
- }
- }
-}
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
deleted file mode 100644
index 6a066f1f..00000000
--- a/Source/Provers/Z3/Prover.cs
+++ /dev/null
@@ -1,937 +0,0 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-
-// #define RECENT_Z3 // 2.20 or newer
-
-using System;
-using System.IO;
-using System.Diagnostics;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.Text;
-//using util;
-using Microsoft.Boogie;
-using Microsoft.Boogie.Simplify;
-using Microsoft.Basetypes;
-
-// Simplified interface to an external prover like Simplify or the z3 process, taken from Bird.
-namespace Microsoft.Boogie.Z3
-{
- internal class Z3ProverProcess : ProverProcess
- {
- [Peer]
- private Z3InstanceOptions opts;
- [Peer]
- private readonly Inspector/*?*/ inspector;
- private readonly bool expectingModel = false;
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(opts != null);
- Contract.Invariant(cce.NonNullElements(parameterSettings));
- }
-
- class OptionValue
- {
- public readonly string Option;
- public readonly string Value;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(Option != null);
- Contract.Invariant(Value != null);
- }
-
- public OptionValue(string option, string value) { Contract.Requires(option != null); Contract.Requires(value != null); Option = option; Value = value; }
- }
-
- static void AddOption(List<OptionValue> parms, string option, string value)
- //modifies parms.*; TODO:
- {
- Contract.Requires(option != null);
- Contract.Requires(value != null);
- Contract.Requires(cce.NonNullElements(parms));
- OptionValue ov = new OptionValue(option, value);
- cce.Owner.AssignSame(ov, cce.Owner.ElementProxy(parms));
- parms.Add(ov);
- }
-
- private List<OptionValue/*!>!*/> parameterSettings;
-
- static void AppendCmdLineOption(StringBuilder cmdLineBldr, string name, object value) {
- cmdLineBldr.Append(' ').Append(OptionChar()).Append(name).Append(':').Append(value);
- }
-
- static void AppendCmdLineOption(StringBuilder cmdLineBldr, string name) {
- cmdLineBldr.Append(' ').Append(OptionChar()).Append(name);
- }
-
- static bool ExpectingModel()
- {
- return CommandLineOptions.Clo.PrintErrorModel >= 1 ||
- CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||
- CommandLineOptions.Clo.ModelViewFile != null ||
- CommandLineOptions.Clo.ContractInfer ||
- CommandLineOptions.Clo.LazyInlining > 0 ||
- CommandLineOptions.Clo.StratifiedInlining > 0;
- }
-
- static string/*!*/ CreateCommandLineArgsForOptions(Z3InstanceOptions opts)
- {
- StringBuilder cmdLineArgsBldr = new StringBuilder();
- AppendCmdLineOption(cmdLineArgsBldr, "si");
-
- if (CommandLineOptions.Clo.z3AtFlag)
- AppendCmdLineOption(cmdLineArgsBldr, "@");
-
- if (0 <= CommandLineOptions.Clo.ProverCCLimit)
- AppendCmdLineOption(cmdLineArgsBldr, "cex", CommandLineOptions.Clo.ProverCCLimit);
-
- if (0 <= opts.Timeout)
- AppendCmdLineOption(cmdLineArgsBldr, "t", opts.Timeout);
-
- if (ExpectingModel())
- AppendCmdLineOption(cmdLineArgsBldr, "m");
-
- foreach (string opt in CommandLineOptions.Clo.Z3Options) {
- Contract.Assert(opt != null);
- cmdLineArgsBldr.Append(" \"").Append(opt).Append('\"');
- }
-
- return cmdLineArgsBldr.ToString();
- }
-
- static List<OptionValue/*!*/>/*!*/ CreateParameterListForOptions(Z3InstanceOptions opts, Inspector inspector)
- {
- List<OptionValue/*!*/>/*!*/ result = new List<OptionValue/*!*/>();
-
- AddOption(result, "MODEL_PARTIAL", "true");
-
- AddOption(result, "MODEL_HIDE_UNUSED_PARTITIONS", "false");
- AddOption(result, "MODEL_V1", "true");
- AddOption(result, "ASYNC_COMMANDS", "false");
-
-#if RECENT_Z3
- AddOption(result, "AUTO_CONFIG", "false");
- AddOption(result, "MBQI", "false");
-#else
- AddOption(result, "MODEL_VALUE_COMPLETION", "false");
-#endif
-
- if (!opts.OptimizeForBv) {
- // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
- // The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.
- AddOption(result, "PHASE_SELECTION", "0");
- AddOption(result, "RESTART_STRATEGY", "0");
- AddOption(result, "RESTART_FACTOR", "|1.5|");
-
- // Make the integer model more diverse by default, speeds up some benchmarks a lot.
- AddOption(result, "ARITH_RANDOM_INITIAL_VALUE", "true");
-
- // The left-to-right structural case-splitting strategy.
-#if !RECENT_Z3
- AddOption(result, "SORT_AND_OR", "false");
-#endif
- AddOption(result, "CASE_SPLIT", "3");
-
- // In addition delay adding unit conflicts.
- AddOption(result, "DELAY_UNITS", "true");
- AddOption(result, "DELAY_UNITS_THRESHOLD", "16");
- }
-
- // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,
- // the foo(x0) will be activated for e-matching when x is skolemized to x0.
- AddOption(result, "NNF_SK_HACK", "true");
-
- // More or less like MAM=0.
- AddOption(result, "QI_EAGER_THRESHOLD", "100");
- // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.
-
- // the following will make the :weight option more usable
- AddOption(result, "QI_COST", "|\"(+ weight generation)\"|");
-
- if (opts.Inspector != null)
- AddOption(result, "PROGRESS_SAMPLING_FREQ", "100");
-
- AddOption(result, "TYPE_CHECK", "true");
- AddOption(result, "BV_REFLECT", "true");
-
- foreach (string opt in CommandLineOptions.Clo.Z3Options) {
- Contract.Assert(opt != null);
- int eq = opt.IndexOf("=");
- // we add them both to command line and the input file:
- // - allow for overriding default options
- // - some options (like TRACE) work only from command line
- // Also options with spaces do not work with (SETPARAMETER ...)
- if (eq > 0 && opt.IndexOf(" ") < 0 && 'A' <= opt[0] && opt[0] <= 'Z') {
- AddOption(result, opt.Substring(0, eq), opt.Substring(eq + 1));
- }
- }
-
- return result;
- }
-
- //[NotDelayed]
- [Captured]
- public Z3ProverProcess(Z3InstanceOptions opts, Inspector inspector)
- : base(ComputeProcessStartInfo(opts), opts.ExeName) { // throws ProverException
- Contract.Requires(opts != null);
- Contract.Requires(inspector == null || cce.Owner.Same(opts, inspector));
- this.parameterSettings = CreateParameterListForOptions(opts, inspector);
- cce.Owner.AssignSame(this, opts);
- this.opts = opts;
- this.inspector = inspector;
- this.expectingModel = ExpectingModel();
- }
-
- private static ProcessStartInfo ComputeProcessStartInfo(Z3InstanceOptions opts)
- {
- return new ProcessStartInfo(opts.ExeName, CreateCommandLineArgsForOptions(opts))
- {
- CreateNoWindow = true,
- UseShellExecute = false,
- RedirectStandardInput = true,
- RedirectStandardOutput = true,
- RedirectStandardError = true
- };
- }
-
- public override string OptionComments() {
- Contract.Ensures(Contract.Result<string>() != null);
-
- StringBuilder sb = new StringBuilder();
- sb.AppendFormat("Z3 command line: {0} {1}\nUser supplied Z3 options:",
- opts.ExeName, this.simplify.StartInfo.Arguments);
- Contract.Assume(cce.IsPeerConsistent(CommandLineOptions.Clo));
- foreach (string opt in CommandLineOptions.Clo.Z3Options) {
- Contract.Assert(opt != null);
- sb.Append(" ").Append(opt);
- }
- sb.AppendFormat("\nProver options: {0}\n", opts.ToString());
- return sb.ToString();
- }
-
- //[Pure(false)]
- public override IEnumerable<string/*!>!*/> ParameterSettings {
- get {
- Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<string>>()));
- foreach (OptionValue opt in parameterSettings) {
- yield return "(SETPARAMETER " + opt.Option + " " + opt.Value + ")";
- }
- }
- }
-
- // z3 uses different magic characters for options on linux/unix and on windows
- private static string OptionChar() {
- Contract.Ensures(Contract.Result<string>() != null);
-
- Contract.Assume(Environment.OSVersion != null);
- switch (Environment.OSVersion.Platform) {
- case PlatformID.Unix:
- return "-";
- default:
- return "/";
- }
- }
-
- protected override void DoBeginCheck(string descriptiveName, string formula) {
- //Contract.Requires(descriptiveName != null);
- //Contract.Requires(formula != null);
- ToWriteLine(formula);
- ToWriteLine(String.Format("; END OF FORMULA {0} - {1}", NumFormulasChecked.ToString(), descriptiveName));
- ToFlush();
- }
-
- protected int TimedFromReadChar() {
- if (opts.Timeout > 0)
- return FromReadChar((opts.Timeout + 1) * 1000);
- else
- return FromReadChar();
- }
-
- private void Trace(string msg) {
- Contract.Requires(msg != null);
- Console.WriteLine("Z3: " + msg);
- }
-
- public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler handler) {
- //Contract.Requires(handler != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- //ProverOutcome outcome;
- bool isInvalid = false;
-
- if (this.simplify == null) {
- return ProverOutcome.Inconclusive;
- }
-
-
- while (true) {
- int ch = TimedFromReadChar();
- if (ch == -1 && this.readTimedOut) {
- handler.OnResourceExceeded("timeout (forced)");
- return ProverOutcome.TimeOut;
- }
-
- if (ch == -1)
- throw new UnexpectedProverOutputException("z3 crashed and produced no output");
-
- string line = new string((char)ch, 1) + FromReadLine();
-
- if (line.StartsWith("STATS ")) {
- if (inspector != null) {
- inspector.StatsLine(line);
- }
- continue;
- }
-
- if (opts.Verbosity > 2) {
- Trace("INPUT: " + line);
- }
-
- if (line.StartsWith("WARNING: Out of allocated virtual memory.")) {
- handler.OnResourceExceeded("memory");
- return ProverOutcome.OutOfMemory;
- }
-
-
- if (line.StartsWith("WARNING: ")) {
- string w = line.Substring(9);
- handler.OnProverWarning(w);
- continue;
- }
-
- if (line.ToUpper().StartsWith("ERROR")) {
- Console.WriteLine("Z3 returns the following error:");
- Console.WriteLine(" " + line);
- return ProverOutcome.Inconclusive;
- }
-
- int beg = 0;
- while (beg < line.Length && '0' <= line[beg] && line[beg] <= '9') {
- cce.LoopInvariant(beg <= line.Length);
- beg++;
- }
-
- if (beg > 0 && line.Substring(beg).StartsWith(": ")) {
- string status = line.Substring(beg + 2);
-
- if (status.StartsWith("Valid")) {
- return ProverOutcome.Valid;
- }
-
- if (status.StartsWith("Timeout")) {
- handler.OnResourceExceeded("timeout");
- return ProverOutcome.TimeOut;
- }
-
- if (status.StartsWith("Inconclusive")) {
- return ProverOutcome.Inconclusive;
- }
-
- if (status.StartsWith("Memout")) {
- handler.OnResourceExceeded("memory");
- return ProverOutcome.OutOfMemory;
- }
-
- if (status.StartsWith("Invalid")) {
- isInvalid = true;
- continue;
- }
- }
-
- if (isInvalid && line == ".") {
- return ProverOutcome.NotValid;
- }
-
- if (isInvalid && line.StartsWith("labels: (")) {
- List<string/*!*/>/*!*/ l = ParseLabels(line);
- Contract.Assert(cce.NonNullElements(l));
- Z3ErrorModel errModel = null;
- if (expectingModel) {
- if (opts.Verbosity > 2) {
- Trace("waiting for model");
- }
- line = FromReadLine();
- if (line.StartsWith("partitions:")) {
- line = ParseModel(out errModel);
- if (opts.Verbosity > 2) {
- Trace("model parsed, final line " + line);
- }
- // Z3 always ends the model with END_OF_MODEL, not with labels: or .
- Contract.Assume(line == "END_OF_MODEL");
- } else {
- throw new UnexpectedProverOutputException(string.Format("evil input from z3 (expecting partitions): '{0}'", line));
- }
- }
- handler.OnModel(l, errModel);
- continue;
- }
-
- throw new UnexpectedProverOutputException(string.Format("evil input from z3: '{0}'", line));
- }
- }
-
- /* ----------------------------------------------------------------------------
- BNF Grammar to parse Z3 output, including the model generated when using the /m /si switch:
-
- Output ::= VC*
- VC ::= number ": " "Valid." | number ": " "Inconclusive" | VCI
- VCI ::= number ": " "Invalid"
- ("labels: " "(" ID* ")"
- [MODEL] "END_OF_MODEL")+
- "."
- MODEL ::= MBOOL MFUNC
- MBOOL ::= "boolean assignment:"
- "partitions:"
- MAPPING*
- MAPPING ::= ZID ["{" ID+"}"] ["->" "(" (number | false | true | BITVECTOR) ")"]
- BITVECTOR ::= ulong ":bv" int
- MFUNC ::= "function interpretations:"
- F*
- F ::= Id "->" "{"
- MAPLET*
- "else" "->" ZID
- "}"
- MAPLET ::= ZID* "->" ZID
-
- -----------------------------------------------------------------------------*/
- private string ParseModel(out Z3ErrorModel errModel)
- //modifies this.*;
- //throws UnexpectedProverOutputException;
- {
- Contract.Ensures(Contract.Result<string>() == "." || Contract.Result<string>().StartsWith("labels: (") || Contract.Result<string>() == "END_OF_MODEL");
- Contract.Ensures(Contract.Result<string>() != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
-
- //Format in the grammar:
- // ZID ["{" ID+"}"] ["->" "(" (number | false | true) ")"]
- // storing the model:
- // map each ID (a string) to the corresping ZID (an integer) in a dictionary:
- Dictionary<string/*!*/, int> identifierToPartition = new Dictionary<string/*!*/, int>();
- // map each ZID to the set (in list form) of IDs belonging to it (possibly empty):
- List<List<string/*!*/>> partitionToIdentifiers = new List<List<string/*!*/>>();
- // map each ZID to the number or boolean given, if any:
- List<Object> partitionToValue = new List<Object>();
- // map each value (number or boolean) to the ZID, reverse map of partitionToValue
- Dictionary<Object, int> valueToPartition = new Dictionary<Object, int>();
- cce.Owner.AssignSame(cce.Owner.ElementProxy(partitionToValue), cce.Owner.ElementProxy(valueToPartition));
-
- int ch;
-
- // read the MAPPING
- for (int zID = 0; true; zID++) {
- ch = FromReadChar();
- if (ch == 'f') {
- break;
- }
- ParseModelMapping(zID, identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition);
- }// end MAPPING
-
- // add the fake partition for the 'else -> #undefined' clause
- List<string/*!*/> emptyList = new List<string/*!*/>();
- cce.Owner.AssignSame(emptyList, cce.Owner.ElementProxy(partitionToIdentifiers));
- partitionToIdentifiers.Add(emptyList);
- partitionToValue.Add(null);
-
- // continue in ParseModelFunctions, which breaks up this long method and enables its verification
- return ParseModelFunctions(ch, out errModel, identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition);
- }
-
- private void ParseModelMapping(int zID,
- Dictionary<string/*!*/, int>/*!*/ identifierToPartition,
- List<List<string/*!*/>>/*!*/ partitionToIdentifiers,
- List<Object>/*!*/ partitionToValue,
- Dictionary<Object, int>/*!*/ valueToPartition)
- //modifies this.*, identifierToPartition.*, partitionToIdentifiers.*, partitionToValue.*, valueToPartition.*;
- {
- Contract.Requires(partitionToValue != null);
- Contract.Requires(valueToPartition != null);
- Contract.Requires(identifierToPartition != null);
- Contract.Requires(cce.NonNullElements(partitionToIdentifiers));
- Contract.Requires(cce.Owner.Same(cce.Owner.ElementProxy(partitionToValue), cce.Owner.ElementProxy(valueToPartition)));
- string s = FromReadLine();
- {
- // sanity check
- int pos = s.IndexOf(' ');
- string n = s;
- int k;
- if (pos >= 0) {
- n = s.Substring(0, pos);
- }
- if (!(int.TryParse(n, out k) && zID == k)) {
- System.Console.WriteLine("mismatch: {0}!={1} '{2}'", zID, k, s);
- Contract.Assume(false);
- }
- }
-
- int j = ParseModelZidAndIdentifiers(zID, s, identifierToPartition, partitionToIdentifiers);
-
- j = s.IndexOf(" -> ", j);
- if (0 <= j) {
- j += 4;
- }
- Contract.Assume(j == -1 || j < s.Length); // if ' -> ' is present, then more should remain of the line
- if (j == -1) {
- // no "-> " found, end of this line, store that there is no value:
- partitionToValue.Add(null);
- int idForNull;
- if (identifierToPartition.TryGetValue("nullObject", out idForNull) && idForNull == zID) {
- Contract.Assume(!valueToPartition.ContainsKey("nullObject")); // a RHS value should occur only once in the Z3 output
- valueToPartition.Add("nullObject", zID);
- // In this case partitionToValue (as the reverse of valueToPartition) should include
- // a map from zID -> "nullObject", but doing that breaks printing out the model as
- // it is printed out by Z3. Also, that information is not required, valueToPartition
- // works well enough by itself.
- }
-
- } else if (s[j] == 't'/*rue*/) {
- partitionToValue.Add(true);
- object boxedTrue = true;
- Contract.Assume(!valueToPartition.ContainsKey(boxedTrue)); // a RHS value should occur only once in the Z3 output
- valueToPartition.Add(boxedTrue, zID);
- } else if (s[j] == 'f'/*alse*/) {
- object boxedFalse = false;
- cce.Owner.AssignSame(boxedFalse, cce.Owner.ElementProxy(partitionToValue));
- partitionToValue.Add(boxedFalse);
- Contract.Assume(!valueToPartition.ContainsKey(boxedFalse)); // a RHS value should occur only once in the Z3 output
- valueToPartition.Add(boxedFalse, zID);
- } else if (s[j] == 'v') {
- // -> val!..., i.e. no value
- partitionToValue.Add(null);
- } else if (s[j] == '{') {
- // array
- List<List<int>/*!*/> arrayModel = new List<List<int>/*!*/>();
- Contract.Assert(Contract.ForAll(arrayModel, a => a != null));
- string array = s.Substring(j + 1);
- int index1, index2;
- string from, to;
- List<int> tuple = new List<int>();
- while (0 <= array.IndexOf(';')) {
- index1 = array.IndexOf('*') + 1;
- index2 = array.IndexOf(' ');
- from = array.Substring(index1, index2 - index1);
- tuple.Add(int.Parse(from));
- array = array.Substring(index2);
- index1 = array.IndexOf('*') + 1;
- index2 = array.IndexOf(';');
- to = array.Substring(index1, index2 - index1);
- array = array.Substring(index2 + 2);
- tuple.Add(int.Parse(to));
- arrayModel.Add(tuple);
- tuple = new List<int>();
- }
- Contract.Assert(array.StartsWith("else ->"));
- index1 = array.IndexOf('*') + 1;
- index2 = array.IndexOf('}');
- to = array.Substring(index1, index2 - index1);
- tuple.Add(int.Parse(to));
- arrayModel.Add(tuple);
- partitionToValue.Add(arrayModel);
- } else {
- string numberOrBv = s.Substring(j);
- // make number an int, then store it:
- BigNum bvVal;
- int bvSize;
- string number, type;
-
- int l = numberOrBv.IndexOf(':', 0);
- if (0 <= l) {
- number = numberOrBv.Substring(0, l);
- type = numberOrBv.Substring(l + 1);
- } else {
- l = numberOrBv.IndexOf('[', 0);
- if (0 <= l) {
- number = numberOrBv.Substring(2, l - 2);
- int closingBracePosition = numberOrBv.IndexOf(']', l);
- if (l < closingBracePosition)
- type = "bv" + numberOrBv.Substring(l + 1, closingBracePosition - l - 1);
- else type = "int";
- } else {
- number = numberOrBv;
- type = "int";
- }
- }
-
- if (type == "int") {
- object boxedN = BigNum.FromString(number);
- Contract.Assume(cce.Owner.None(boxedN));
- cce.Owner.AssignSame(boxedN, cce.Owner.ElementProxy(partitionToValue));
- partitionToValue.Add(boxedN);
- Contract.Assume(!valueToPartition.ContainsKey(boxedN)); // a RHS value should occur only once in the Z3 output
- valueToPartition.Add(boxedN, zID);
- } else if (type.StartsWith("bv") && BigNum.TryParse(number, out bvVal) && int.TryParse(type.Substring(2), out bvSize)) {
- BvConst bitV = new BvConst(bvVal, bvSize);
- cce.Owner.AssignSame(bitV, cce.Owner.ElementProxy(partitionToValue));
- partitionToValue.Add(bitV);
- Contract.Assume(!valueToPartition.ContainsKey(bitV)); // a RHS value should occur only once in the Z3 output
- valueToPartition.Add(bitV, zID);
- } else {
- System.Console.WriteLine("cannot parse type: '{0}':'{1}'", number, type);
- Contract.Assume(false);
- }
-
- }
- }
-
- private static int ParseModelZidAndIdentifiers(int zID, string s,
- Dictionary<string/*!*/, int>/*!*/ identifierToPartition,
- List<List<string/*!*/>>/*!*/ partitionToIdentifiers)
- //modifies identifierToPartition.*, partitionToIdentifiers.*;
- {
- Contract.Requires(identifierToPartition != null && cce.NonNullElements(identifierToPartition.Keys));
- Contract.Requires(partitionToIdentifiers != null && Contract.ForAll(partitionToIdentifiers, identifier => cce.NonNullElements(identifier)));
- Contract.Requires(s != null);
- Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() <= s.Length);
-
- List<string/*!*/> identifiers = new List<string/*!*/>();
- int arrowIndex = s.IndexOf('>');
- Contract.Assert(0 < arrowIndex);
- int j = s.IndexOf('{', 0) + 1; // skip the '{', if present, and set j to 0 otherwise
- if (1 <= j && j < arrowIndex) {
- // There is a list of ID's.
- Contract.Assume(j < s.Length); // there should be more characters; the ending '}', for one
- //ID*
- while (true) {
- cce.LoopInvariant(cce.IsPeerConsistent(identifiers) && cce.IsPeerConsistent(identifierToPartition) && cce.IsPeerConsistent(partitionToIdentifiers));
- cce.LoopInvariant(0 <= j && j < s.Length);
- int k = s.IndexOfAny(new char[] { ' ', '}' }, j);
- Contract.Assume(j <= k);
- string id = s.Substring(j, k - j);
- j = k + 1;
- Contract.Assume(!identifierToPartition.ContainsKey(id)); // an ID is listed only once in this list, and an ID can only belong to one ZID equivalence class
- identifierToPartition.Add(id, zID);
- identifiers.Add(id);
- if (s[k] == '}') {
- // end of reading ID*
- break;
- }
- Contract.Assume(j < s.Length); // there should be more characters; the ending '}', for one
- }//end ID*
- } else {
- j = 0;
- }
- cce.Owner.AssignSame(identifiers, cce.Owner.ElementProxy(partitionToIdentifiers));
- partitionToIdentifiers.Add(identifiers);
- return j;
- }
-
- private string ParseModelFunctions(int ch, out Z3ErrorModel errModel,
- Dictionary<string/*!*/, int>/*!*/ identifierToPartition,
- List<List<string/*!*/>>/*!*/ partitionToIdentifiers,
- List<Object>/*!*/ partitionToValue,
- Dictionary<Object, int>/*!*/ valueToPartition
- )
- //modifies this.*;
- {
- Contract.Requires(identifierToPartition != null && cce.NonNullElements(identifierToPartition.Keys));
- Contract.Requires(partitionToIdentifiers != null && Contract.ForAll(partitionToIdentifiers, identifier => cce.NonNullElements(identifier)));
- Contract.Requires(partitionToValue != null);
- Contract.Requires(valueToPartition != null);
- Contract.Ensures(Contract.Result<string>() != null);
- Contract.Ensures(Contract.Result<string>() == "." || Contract.Result<string>().StartsWith("labels: (") || Contract.Result<string>() == "END_OF_MODEL");
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- // read the function F
- Expect(ch, "function interpretations:");
- FromReadLine();
-
- // mapping of function names to function definitions
- Dictionary<string/*!*/, List<List<int>>/*!*/> definedFunctions = new Dictionary<string/*!*/, List<List<int>>/*!*/>();
- // function definition given as list of 'pointwise definitions' in the form of the arguments and result
- // the last element here will always be a list with just one entry which corresponds to the else case
- List<List<int>> functionDefinition = new List<List<int>>();
- // list of arguments, followed by the result, the last element of this list is always the result
- List<int> argumentsAndResult = new List<int>();
-
- // read F
- while (true) {
- functionDefinition = new List<List<int>>();
- string s = FromReadLine();
- // end of F, "END_OF_MODEL" ends model, '.' ends whole VC, 'l' starts a new set of labels and model
- // whenever there is a model this will end with "END_OF_MODEL", the other cases can only
- // happen when there is no model printed!
- if (s == "." || s.StartsWith("labels: (") || s == "END_OF_MODEL") {
- errModel = new Z3ErrorModel(identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition, definedFunctions);
- return s;
- }
- int j = s.IndexOf(' ', 0);
- Contract.Assume(0 <= j);
- string id = s.Substring(0, j);
- // id is stored into definedFunctions once the function definition for it has
- // been completely parsed.
-
- if (s.IndexOf("-> {") < 0) {
- // This function was a macro and we are not parsing its definition currently.
- // Just move on to the next function.
- while (true) {
- s = FromReadLine();
- if (0 <= s.IndexOf("{" + id + "}"))
- break;
- }
- continue;
- }
-
- // just ignore the "-> {" by dropping string s
- string zIDstring;
-
- // MAPLET
- while (true) {
- argumentsAndResult = new List<int>();
- // remove the 2 spaces that are here
- FromReadChar();
- FromReadChar();
- s = FromReadLine();
- if (s.StartsWith("else ->")) break;
- j = 0;
-
- //ZID*
- while (true) {
- cce.LoopInvariant(0 <= j && j <= s.Length);
-
- j = s.IndexOfAny(new Char[] { '*', '-' }, j);
- // true because this always ends with a "->":
- Contract.Assume(0 <= j);
-
- // reading -> means end of ZID*
- if (s[j] == '-'/*>*/) break;
-
- // start reading the ZID* with the number, not the *
- j = j + 1;
- // by input string format:
- Contract.Assume(j < s.Length);
- int k = s.IndexOf(' ', j);
- // by input string format:
- Contract.Assume(j <= k);
- zIDstring = s.Substring(j, k - j);
- // add the arguments
- argumentsAndResult.Add(int.Parse(zIDstring));
- j = k;
- }// end ZID*
-
- // j is the beginning of "-> *", we want the first character after this
- j = j + 4;
- // by input string format:
- Contract.Assume(j <= s.Length);
- zIDstring = s.Substring(j);
- // add the result
- argumentsAndResult.Add(int.Parse(zIDstring));
- // add the input line as another 'pointwise defined' element to the functions definition
- functionDefinition.Add(argumentsAndResult);
- }// end MAPLET
-
- // this is the 'else -> #unspecified' case
- // by input string format:
- Contract.Assume(s.IndexOf("#unspec") >= 0);
- // this stores the else line as another argumentsAndResult list
- argumentsAndResult = new List<int>();
- argumentsAndResult.Add(partitionToIdentifiers.Count - 1); // use the fake partition we have created before
- // which is then added to the function definition, which is now complete
- cce.Owner.AssignSame(argumentsAndResult, cce.Owner.ElementProxy(functionDefinition));
- functionDefinition.Add(argumentsAndResult);
-
- /*
- // this is the 'else -> *' case, that string is already in s
- j = s.IndexOf('*', 0) + 1;
- // by input string format:
- assume 0 < j && j < s.Length;
- zIDstring = s.Substring(j);
- // this stores the else line as another argumentsAndResult list
- argumentsAndResult = new List<int>();
- argumentsAndResult.Add(int.Parse(zIDstring));
- // which is then added to the function definition, which is now complete
- functionDefinition.Add(argumentsAndResult); */
-
- // and therefore added to the map of defined functions, together with the name 'id'
- // which had been extracted before
- Contract.Assume(!definedFunctions.ContainsKey(id)); // each function name in the model is listed only once
- definedFunctions.Add(id, functionDefinition);
-
- // read the line with "}"
- ch = FromReadChar();
- Expect(ch, "}");
- FromReadLine();
- }// end F
- }
-
- }
-
-
- public class Z3ErrorModel : ErrorModel
- {
- public Z3ErrorModel(Dictionary<string/*!*/, int>/*!*/ identifierToPartition,
- List<List<string/*!*/>>/*!*/ partitionToIdentifiers,
- List<Object>/*!*/ partitionToValue,
- Dictionary<object, int>/*!*/ valueToPartition,
- Dictionary<string/*!*/, List<List<int>>/*!*/>/*!*/ definedFunctions)
- : base(identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition, definedFunctions) {
- Contract.Requires(identifierToPartition != null && cce.NonNullElements(identifierToPartition.Keys));
- Contract.Requires(partitionToIdentifiers != null && Contract.ForAll(partitionToIdentifiers, x => cce.NonNullElements(x)));
- Contract.Requires(partitionToValue != null);
- Contract.Requires(valueToPartition != null);
- Contract.Requires(definedFunctions != null && cce.NonNullElements(definedFunctions.Keys) && cce.NonNullElements(definedFunctions.Values));
-
- this.partitionNames = new string/*?*/[partitionToIdentifiers.Count];
- this.prevPartitionNames = new string/*?*/[partitionToIdentifiers.Count];
- }
-
- private string/*?*/[]/*!*/ partitionNames;
- private string/*?*/[]/*!*/ prevPartitionNames;
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(partitionNames != null);
- Contract.Invariant(prevPartitionNames != null);
- }
-
-
- private void SetNames() {
- int len = partitionToIdentifiers.Count;
- for (int i = 0; i < 3; ++i) { // let the names stabilize a bit
- prevPartitionNames = partitionNames;
- partitionNames = new string[len];
- for (int pos = 0; pos < len; ++pos)
- GetPartitionName(pos);
- }
- }
-
- private int NameBadness(string name) {
- Contract.Requires(name != null);
- int badness = name.Length;
- if (name.StartsWith("call") && name.IndexOf("formal@") > 0)
- badness += 1000;
- if (name.IndexOf("(") > 0)
- badness += 500;
- return badness;
- }
-
- private string GetPartitionName(int pos) {
- Contract.Ensures(Contract.Result<string>() != null);
-
- string name = partitionNames[pos];
- if (name != null) {
- return name;
- }
-
- object tmp = partitionToValue[pos];
- if (tmp != null) {
- partitionNames[pos] = tmp is BvConst ? ((BvConst)tmp).ToReadableString() : tmp.ToString();
- } else {
- List<string/*!*/>/*!*/ possible_names = new List<string/*!*/>();
- List<string/*!*/> pti = partitionToIdentifiers[pos];
- Contract.Assert(cce.NonNullElements(pti));
-
- // make sure we're not called recursively
- string prevName = prevPartitionNames[pos];
- if (prevName == null) prevName = "*" + pos;
- partitionNames[pos] = prevName;
-
- if (pti != null && pti.Count > 0) {
- // add identifiers
- foreach (string n in pti) {
- Contract.Assert(n != null);
- possible_names.Add(n);
- }
- }
-
- // Then also look for functions,
- // and then collect possible functional definitions
- foreach (KeyValuePair<string/*!*/, List<List<int>>/*!*/> kv in definedFunctions) {
- Contract.Assert(kv.Key != null);
- Contract.Assert(kv.Value != null);
- foreach (List<int> parms in kv.Value) {
- if (parms.Count > 1 && parms[parms.Count - 1] == pos) {
- string s = kv.Key + "(";
- for (int i = 0; i < parms.Count - 1; ++i) {
- if (i != 0) s += ", ";
- s += GetPartitionName(parms[i]);
- }
- s += ")";
- possible_names.Add(s);
- }
- }
- }
-
- // choose the shortest possible name
- if (possible_names.Count > 0) {
- string best = possible_names[0];
- foreach (string s in possible_names) {
- Contract.Assert(s != null);
- if (NameBadness(s) < NameBadness(best)) best = s;
- }
- if (best.Length < 120)
- partitionNames[pos] = best;
- }
- }
-
- return cce.NonNull(partitionNames[pos]);
- }
-
- private void PrintReadableModel(TextWriter writer) {
- Contract.Requires(writer != null);
- writer.WriteLine("Z3 error model: ");
- SetNames();
- writer.WriteLine("partitions:");
- Contract.Assert(partitionToIdentifiers.Count == partitionToValue.Count);
- for (int i = 0; i < partitionToIdentifiers.Count; i++) {
- writer.Write("{0,5}: {1} ", "*" + i, GetPartitionName(i));
- List<string/*!*/> pti = partitionToIdentifiers[i];
- Contract.Assert(cce.NonNullElements(pti));
- if (pti != null && (pti.Count > 1 || (pti.Count == 1 && partitionToValue[i] != null))) {
- writer.Write("{");
- for (int k = 0; k < pti.Count - 1; k++) {
- writer.Write(pti[k] + " ");
- }
- //extra work to make sure no " " is at the end of the list of identifiers
- if (pti.Count != 0) {
- writer.Write(pti[pti.Count - 1]);
- }
- writer.Write("}");
- }
- writer.WriteLine();
- }
-
- writer.WriteLine();
- writer.WriteLine("function interpretations:");
- List<string> funNames = new List<string>(definedFunctions.Keys);
- funNames.Sort();
- foreach (string name in funNames) {
- Contract.Assert(name != null);
- if (definedFunctions[name].Count == 1) continue; // skip functions with only the else-> clause
- foreach (List<int> parms in definedFunctions[name]) {
- Contract.Assert(parms != null);
- string s = name + "(";
- if (parms.Count == 1) {
- continue;
- // s += "*";
- } else {
- for (int i = 0; i < parms.Count - 1; ++i) {
- if (i != 0) s += ", ";
- s += GetPartitionName(parms[i]);
- }
- }
- s += ")";
- string res = GetPartitionName(parms[parms.Count - 1]);
- if (res == s)
- res = "*" + parms[parms.Count - 1] + " (SELF)";
- writer.WriteLine("{0} = {1}", s, res);
- }
- writer.WriteLine();
- }
- writer.WriteLine("The end.");
- writer.WriteLine();
- }
-
- public override void Print(TextWriter writer) {
- //Contract.Requires(writer != null);
- if (CommandLineOptions.Clo.PrintErrorModel == 4) {
- PrintReadableModel(writer);
- } else {
- base.Print(writer);
- }
- }
- }
-}
-
-
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
deleted file mode 100644
index 3718372b..00000000
--- a/Source/Provers/Z3/ProverInterface.cs
+++ /dev/null
@@ -1,427 +0,0 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-//using System.Collections;
-using System.Collections.Generic;
-using System.Threading;
-//using System.IO;
-using System.Text;
-//using ExternalProver;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using Microsoft.Boogie.AbstractInterpretation;
-using Microsoft.Boogie;
-using Microsoft.Boogie.VCExprAST;
-using Microsoft.Boogie.Clustering;
-using Microsoft.Boogie.TypeErasure;
-using Microsoft.Boogie.Z3;
-using Microsoft.Boogie.Simplify;
-
-namespace Microsoft.Boogie.Z3
-{
- public class Z3ProcessTheoremProver : ProcessTheoremProver
- {
- private Z3InstanceOptions opts;
- private Inspector inspector;
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(opts!=null);
-}
-
-
- [NotDelayed]
- public Z3ProcessTheoremProver(VCExpressionGenerator gen,
- DeclFreeProverContext ctx, Z3InstanceOptions opts):base(opts, gen, ctx, opts.ExeName, "TypedUnivBackPred2.sx")
- {
- Contract.Requires(gen != null);
- Contract.Requires(ctx != null);
- Contract.Requires(opts != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- this.opts = opts;
-
- }
-
- private void FireUpInspector()
- {
- if (inspector == null && opts.Inspector != null) {
- inspector = new Inspector(opts);
- }
- }
-
- protected override Microsoft.Boogie.Simplify.ProverProcess CreateProverProcess(string proverPath) {
- //Contract.Requires(proverPath!= null);
- Contract.Ensures(Contract.Result<Microsoft.Boogie.Simplify.ProverProcess>() != null);
-
-
- opts.ExeName = proverPath;
- FireUpInspector();
- if (inspector != null) {
- inspector.NewProver();
- }
- return new Z3ProverProcess(opts, inspector);
- }
-
- protected override AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions opts) {
- //Contract.Requires(opts != null);
- Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);
-
- return new Z3VCExprTranslator(gen, (Z3InstanceOptions) opts);
- }
-
- public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
- {
- //Contract.Requires(descriptiveName != null);
- //Contract.Requires(vc != null);
- //Contract.Requires(handler != null);
- FireUpInspector();
- if (inspector != null) {
- inspector.NewProblem(descriptiveName, vc, handler);
- }
- base.BeginCheck(descriptiveName, vc, handler);
- }
- }
-
- public class Z3InstanceOptions : ProverOptions
- {
- public int Timeout { get { return TimeLimit / 1000; } }
- public int Lets {
- get
- {
- Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() < 4);
- return CommandLineOptions.Clo.Z3lets;
- }
- }
- public bool DistZ3 = false;
- public string ExeName = "z3.exe";
- public bool InverseImplies = false;
- public string Inspector = null;
- public bool OptimizeForBv = false;
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(ExeName!=null);
- }
-
- protected override bool Parse(string opt)
- {
- //Contract.Requires(opt!=null);
- return ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||
- ParseString(opt, "INSPECTOR", ref Inspector) ||
- ParseBool(opt, "DIST", ref DistZ3) ||
- ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||
- base.Parse(opt);
- }
-
- public override void PostParse()
- {
- base.PostParse();
-
- if (DistZ3) {
- ExeName = "z3-dist.exe";
- CommandLineOptions.Clo.RestartProverPerVC = true;
- }
- }
-
- public override string Help
- {
- get
- {
- return
-@"
-Z3-specific options:
-~~~~~~~~~~~~~~~~~~~~
-INSPECTOR=<string> Use the specified Z3Inspector binary.
-OPTIMIZE_FOR_BV=<bool> Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.
-
-Obscure options:
-~~~~~~~~~~~~~~~~
-DIST=<bool> Use z3-dist.exe binary.
-REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
-
-" + base.Help;
- // DIST requires non-public binaries
- }
- }
- }
-
- public class Z3LineariserOptions : LineariserOptions {
- private readonly Z3InstanceOptions opts;
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(opts!=null);
- }
-
-
- public Z3LineariserOptions(bool asTerm, Z3InstanceOptions opts, List<VCExprVar/*!>!*/> letVariables):base(asTerm) {
- Contract.Requires(opts != null);
- Contract.Requires(cce.NonNullElements(letVariables));
-
- this.opts = opts;
- this.LetVariablesAttr = letVariables;
- }
-
- public override bool UseWeights { get {
- return true;
- } }
-
- public override bool UseTypes { get {
- return true;
- } }
-
- public override bool QuantifierIds { get {
- return true;
- } }
-
- public override bool InverseImplies { get {
- return opts.InverseImplies;
- } }
-
- public override LineariserOptions SetAsTerm(bool newVal) {
- Contract.Ensures(Contract.Result<LineariserOptions>() != null);
-
- if (newVal == AsTerm)
- return this;
- return new Z3LineariserOptions(newVal, opts, LetVariables);
- }
-
- // variables representing formulas in let-bindings have to be
- // printed in a different way than other variables
- private readonly List<VCExprVar/*!>!*/> LetVariablesAttr;
- public override List<VCExprVar/*!>!*/> LetVariables { get {
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
-
- return LetVariablesAttr;
- } }
-
- public override LineariserOptions AddLetVariable(VCExprVar furtherVar) {
- //Contract.Requires(furtherVar != null);
- Contract.Ensures(Contract.Result<LineariserOptions>() != null);
-
- List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>();
- allVars.AddRange(LetVariables);
- allVars.Add(furtherVar);
- return new Z3LineariserOptions(AsTerm, opts, allVars);
- }
-
- public override LineariserOptions AddLetVariables(List<VCExprVar/*!>!*/> furtherVars) {
- //Contract.Requires(furtherVars != null);
- Contract.Ensures(Contract.Result<LineariserOptions>() != null);
-
- List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/> ();
- allVars.AddRange(LetVariables);
- allVars.AddRange(furtherVars);
- return new Z3LineariserOptions(AsTerm, opts, allVars);
- }
- }
-
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
-
- public class Z3VCExprTranslator : AxiomVCExprTranslator {
- public Z3VCExprTranslator(VCExpressionGenerator gen, Z3InstanceOptions opts) {
- Contract.Requires(gen != null);
- Contract.Requires(opts != null);
- Gen = gen;
- Opts = opts;
- TypeAxiomBuilder axBuilder;
- switch (CommandLineOptions.Clo.TypeEncodingMethod) {
- case CommandLineOptions.TypeEncoding.Arguments:
- axBuilder = new TypeAxiomBuilderArguments (gen);
- break;
- default:
- axBuilder = new TypeAxiomBuilderPremisses (gen);
- break;
- }
- axBuilder.Setup();
- AxBuilder = axBuilder;
- UniqueNamer namer = new UniqueNamer ();
- Namer = namer;
- this.DeclCollector =
- new TypeDeclCollector (namer, true);
- }
-
- private Z3VCExprTranslator(Z3VCExprTranslator tl) :base(tl){
- Contract.Requires(tl!=null);
- Gen = tl.Gen;
- Opts = tl.Opts; // we assume that the options have not changed
- AxBuilder = (TypeAxiomBuilder)tl.AxBuilder.Clone();
- UniqueNamer namer = (UniqueNamer)tl.Namer.Clone();
- Namer = namer;
- DeclCollector = new TypeDeclCollector (namer, tl.DeclCollector);
- }
-
- public override Object Clone() {
- Contract.Ensures(Contract.Result<Object>() != null);
-
- return new Z3VCExprTranslator(this);
- }
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(Opts!=null);
- Contract.Invariant(Gen != null);
- Contract.Invariant(AxBuilder != null);
- Contract.Invariant(Namer != null);
- Contract.Invariant(DeclCollector != null);
- }
-
- private readonly Z3InstanceOptions Opts;
- private readonly VCExpressionGenerator Gen;
- private readonly TypeAxiomBuilder AxBuilder;
- private readonly UniqueNamer Namer;
- private readonly TypeDeclCollector DeclCollector;
-
- public override string Lookup(VCExprVar var)
- {
- //Contract.Requires(var != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- VCExprVar v = AxBuilder.TryTyped2Untyped(var);
- if (v != null) {
- var = v;
- }
- return Namer.Lookup(var);
- }
-
- public override string translate(VCExpr expr, int polarity) {
- //Contract.Requires(expr != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- DateTime start = DateTime.UtcNow;
- if (CommandLineOptions.Clo.Trace)
- Console.Write("Linearising ... ");
-
- // handle the types in the VCExpr
- TypeEraser eraser;
- switch (CommandLineOptions.Clo.TypeEncodingMethod) {
- case CommandLineOptions.TypeEncoding.Arguments:
- eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, Gen);
- break;
- case CommandLineOptions.TypeEncoding.Monomorphic:
- eraser = null;
- break;
- default:
- eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);
- break;
- }
- VCExpr exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;
- Contract.Assert(exprWithoutTypes!=null);
-
- LetBindingSorter letSorter = new LetBindingSorter(Gen);
- Contract.Assert(letSorter!=null);
- VCExpr sortedExpr = letSorter.Mutate(exprWithoutTypes, true);
- Contract.Assert(sortedExpr!=null);
- VCExpr sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);
- Contract.Assert(sortedAxioms!=null);
-
- DeclCollector.Collect(sortedAxioms);
- DeclCollector.Collect(sortedExpr);
- FeedTypeDeclsToProver();
- if (Opts.Lets != 3) {
- // replace let expressions with implies
- Let2ImpliesMutator letImplier = new Let2ImpliesMutator(Gen, Opts.Lets == 1, Opts.Lets == 2);
- sortedExpr = letImplier.Mutate(sortedExpr);
- sortedAxioms = letImplier.Mutate(sortedAxioms);
- }
-
- //////////////////////////////////////////////////////////////////////////
- //SubtermCollector! coll = new SubtermCollector (gen);
- //coll.Traverse(sortedExpr, true);
- //coll.Traverse(sortedAxioms, true);
- //coll.UnifyClusters();
- //Console.WriteLine(coll);
- //////////////////////////////////////////////////////////////////////////
-
- LineariserOptions linOptions = new Z3LineariserOptions(false, Opts, new List<VCExprVar/*!*/>());
-
- AddAxiom(SimplifyLikeExprLineariser.ToString(sortedAxioms, linOptions, Namer));
-
- string res = SimplifyLikeExprLineariser.ToString(sortedExpr, linOptions, Namer);
- Contract.Assert(res!=null);
-
- if (CommandLineOptions.Clo.Trace) {
- TimeSpan elapsed = DateTime.UtcNow - start;
- Console.WriteLine("finished [{0} s]", elapsed.TotalSeconds);
- }
- return res;
- }
-
- private void FeedTypeDeclsToProver() {
- foreach (string s in DeclCollector.GetNewDeclarations()) {
- Contract.Assert(s != null);
- AddTypeDecl(s);
- }
- }
- }
-
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
-
- public class Factory : ProverFactory
- {
-
- public override object SpawnProver(ProverOptions popts, object ctxt)
- {
- //Contract.Requires(popts != null);
- //Contract.Requires(ctxt != null);
- Contract.Ensures(Contract.Result<object>() != null);
-
- Z3InstanceOptions opts = cce.NonNull((Z3InstanceOptions)popts);
- return this.SpawnProver(cce.NonNull((DeclFreeProverContext)ctxt).ExprGen,
- cce.NonNull((DeclFreeProverContext)ctxt),
- opts);
- }
-
- public override object NewProverContext(ProverOptions options) {
- //Contract.Requires(options != null);
- //Contract.Ensures(Contract.Result<object>() != null);
-
- if (CommandLineOptions.Clo.BracketIdsInVC < 0) {
- CommandLineOptions.Clo.BracketIdsInVC = 0;
- }
-
- Z3InstanceOptions opts = cce.NonNull((Z3InstanceOptions)options);
- VCExpressionGenerator gen = new VCExpressionGenerator ();
- List<string/*!>!*/> proverCommands = new List<string/*!*/> ();
- proverCommands.Add("z3");
- proverCommands.Add("simplifyLike");
- VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands);
-
- return NewProverContext(gen, genOptions, opts);
- }
-
- public override ProverOptions BlankProverOptions()
- {
- Contract.Ensures(Contract.Result<ProverOptions>() != null);
- return new Z3InstanceOptions();
- }
-
- protected virtual Z3ProcessTheoremProver SpawnProver(VCExpressionGenerator gen,
- DeclFreeProverContext ctx,
- Z3InstanceOptions opts) {
- Contract.Requires(gen != null);
- Contract.Requires(ctx != null);
- Contract.Requires(opts != null);
- Contract.Ensures(Contract.Result<Z3ProcessTheoremProver>() != null);
-
- return new Z3ProcessTheoremProver(gen, ctx, opts);
- }
-
- protected virtual DeclFreeProverContext NewProverContext(VCExpressionGenerator gen,
- VCGenerationOptions genOptions,
- Z3InstanceOptions opts)
- {
- return new DeclFreeProverContext(gen, genOptions);
- }
- }
-}
diff --git a/Source/Provers/Z3/TypeDeclCollector.cs b/Source/Provers/Z3/TypeDeclCollector.cs
deleted file mode 100644
index 19c88409..00000000
--- a/Source/Provers/Z3/TypeDeclCollector.cs
+++ /dev/null
@@ -1,398 +0,0 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using Microsoft.Boogie.VCExprAST;
-
-namespace Microsoft.Boogie.Z3
-{
- // Visitor for collecting the occurring function symbols in a VCExpr,
- // and for creating the corresponding declarations that can be fed into
- // Z3
-
- // (should this be rather done by Context.DeclareFunction? right now,
- // the TypeErasure visitor introduces new function symbols that are
- // not passed to this method)
-
- public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
-
- private readonly UniqueNamer Namer;
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(Namer!=null);
- Contract.Invariant(AllDecls != null);
- Contract.Invariant(IncDecls != null);
- Contract.Invariant(cce.NonNull(KnownFunctions));
- Contract.Invariant(cce.NonNull(KnownVariables));
- Contract.Invariant(cce.NonNull(KnownTypes));
- Contract.Invariant(cce.NonNull(KnownBvOps));
- Contract.Invariant(cce.NonNull(KnownSelectFunctions));
- Contract.Invariant(cce.NonNull(KnownStoreFunctions));
-}
-
-
- private readonly bool NativeBv;
-
- public TypeDeclCollector(UniqueNamer namer, bool nativeBv) {
- Contract.Requires(namer != null);
- this.Namer = namer;
- this.NativeBv = nativeBv;
- AllDecls = new List<string/*!*/> ();
- IncDecls = new List<string/*!*/> ();
- KnownFunctions = new HashSet<Function/*!*/>();
- KnownVariables = new HashSet<VCExprVar/*!*/>();
- KnownTypes = new HashSet<Type/*!*/>();
- KnownBvOps = new HashSet<string/*!*/>();
-
- KnownStoreFunctions = new HashSet<string/*!*/>();
- KnownSelectFunctions = new HashSet<string/*!*/>();
- }
-
- internal TypeDeclCollector(UniqueNamer namer, TypeDeclCollector coll) {
- Contract.Requires(namer!=null);
- Contract.Requires(coll!=null);
- this.Namer = namer;
- this.NativeBv = coll.NativeBv;
- AllDecls = new List<string/*!*/> (coll.AllDecls);
- IncDecls = new List<string/*!*/> (coll.IncDecls);
- KnownFunctions = new HashSet<Function/*!*/>(coll.KnownFunctions);
- KnownVariables = new HashSet<VCExprVar/*!*/>(coll.KnownVariables);
- KnownTypes = new HashSet<Type/*!*/>(coll.KnownTypes);
- KnownBvOps = new HashSet<string/*!*/>(coll.KnownBvOps);
-
- KnownStoreFunctions = new HashSet<string/*!*/>(coll.KnownStoreFunctions);
- KnownSelectFunctions = new HashSet<string/*!*/>(coll.KnownSelectFunctions);
- }
-
- // not used
- protected override bool StandardResult(VCExpr node, bool arg) {
- //Contract.Requires(node != null);
- return true;
- }
-
- private readonly List<string/*!>!*/> AllDecls;
- private readonly List<string/*!>!*/> IncDecls;
-
- private readonly HashSet<Function/*!*/>/*!*/ KnownFunctions;
- private readonly HashSet<VCExprVar/*!*/>/*!*/ KnownVariables;
-
- // bitvector types have to be registered as well
- private readonly HashSet<Type/*!*/>/*!*/ KnownTypes;
-
- // the names of registered BvConcatOps and BvExtractOps
- private readonly HashSet<string/*!*/>/*!*/ KnownBvOps;
-
- private readonly HashSet<string/*!*/>/*!*/ KnownStoreFunctions;
- private readonly HashSet<string/*!*/>/*!*/ KnownSelectFunctions;
-
- public List<string/*!>!*/> AllDeclarations { get {
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<string>>()));
-
- List<string/*!>!*/> res = new List<string/*!*/> ();
- res.AddRange(AllDecls);
- return res;
- } }
-
- public List<string/*!>!*/> GetNewDeclarations() {
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<string>>()));
- List<string/*!>!*/> res = new List<string/*!*/> ();
- res.AddRange(IncDecls);
- IncDecls.Clear();
- return res;
- }
-
- private void AddDeclaration(string decl) {
- Contract.Requires(decl != null);
- AllDecls.Add(decl);
- IncDecls.Add(decl);
- }
-
- public void Collect(VCExpr expr) {
- Contract.Requires(expr != null);
- Traverse(expr, true);
- }
-
- ///////////////////////////////////////////////////////////////////////////
-
- private static string TypeToString(Type t) {
- Contract.Requires(t!= null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- return SimplifyLikeExprLineariser.TypeToString(t);
- }
-
- private void RegisterType(Type type)
- {
- Contract.Requires(type != null);
- if (KnownTypes.Contains(type)) return;
-
- if (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays) {
- KnownTypes.Add(type);
- string declString = "";
- MapType mapType = type.AsMap;
- Contract.Assert(mapType != null);
-
- foreach (Type t in mapType.Arguments) {
- Contract.Assert(t != null);
- RegisterType(t);
- }
- RegisterType(mapType.Result);
-
- declString += "(DEFTYPE " + TypeToString(type);
-
- if (CommandLineOptions.Clo.UseArrayTheory) {
- declString += " :BUILTIN Array ";
- foreach (Type t in mapType.Arguments) {
- declString += TypeToString(t);
- declString += " ";
- }
- declString += TypeToString(mapType.Result);
- }
-
- declString += ")";
- AddDeclaration(declString);
- return;
- }
-
- if (type.IsBv && NativeBv) {
- int bits = type.BvBits;
- string name = TypeToString(type);
-
- AddDeclaration("(DEFTYPE " + name + " :BUILTIN BitVec " + bits + ")");
- // If we add the BUILTIN then the conversion axiom does not work
- AddDeclaration("(DEFOP " + name + "_to_int " + name + " $int)"); // :BUILTIN bv2int $int)");
- AddDeclaration("(DEFOP $make_bv" + bits + " $int " + name + " :BUILTIN int2bv " + bits + ")");
- string expr = "($make_bv" + bits + " (" + name + "_to_int x))";
- AddDeclaration("(BG_PUSH (FORALL (x :TYPE " + name + ") (PATS "
- + expr + ") (QID bvconv" + bits + ") (EQ " + expr + " x)))");
-
- KnownTypes.Add(type);
- return;
- }
-
- if (type.IsBool || type.IsInt)
- return;
-
- if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic) {
- AddDeclaration("(DEFTYPE " + TypeToString(type) + ")");
- KnownTypes.Add(type);
- return;
- }
-
- }
-
- public override bool Visit(VCExprNAry node, bool arg) {
- Contract.Requires(node != null);
- // there are a couple cases where operators have to be
- // registered by generating appropriate Z3 statements
-
- if (node.Op is VCExprBvOp) {
- if (NativeBv) {
- RegisterType(node[0].Type);
- RegisterType(node.Type);
- }
- } else if (node.Op is VCExprBvConcatOp) {
- //
- if (NativeBv) {
- RegisterType(node[0].Type);
- RegisterType(node[1].Type);
- RegisterType(node.Type);
-
- string name = SimplifyLikeExprLineariser.BvConcatOpName(node);
- if (!KnownBvOps.Contains(name)) {
- AddDeclaration("(DEFOP " + name +
- " " + TypeToString(node[0].Type) +
- " " + TypeToString(node[1].Type) +
- " " + TypeToString(node.Type) +
- " :BUILTIN concat)");
- KnownBvOps.Add(name);
- }
- }
- //
- } else if (node.Op is VCExprBvExtractOp) {
- //
- if (NativeBv) {
- RegisterType(node[0].Type);
- RegisterType(node.Type);
-
- VCExprBvExtractOp op = (VCExprBvExtractOp)node.Op;
- Contract.Assert(op!=null);
- string name = SimplifyLikeExprLineariser.BvExtractOpName(node);
- if (!KnownBvOps.Contains(name)) {
- AddDeclaration("(DEFOP " + name +
- " " + TypeToString(node[0].Type) +
- " " + TypeToString(node.Type) +
- " :BUILTIN extract " +
- (op.End - 1) + " " + op.Start + ")");
- KnownBvOps.Add(name);
- }
- }
- //
- } else if (node.Op is VCExprStoreOp) {
- RegisterType(node.Type); // this is the map type, registering it should register also the index and value types
- string name = SimplifyLikeExprLineariser.StoreOpName(node);
- if (!KnownStoreFunctions.Contains(name)) {
- string decl = "(DEFOP " + name;
-
- foreach (VCExpr ch in node) {
- decl += " " + TypeToString(ch.Type);
- }
- decl += " " + TypeToString(node.Type);
-
- if (CommandLineOptions.Clo.UseArrayTheory)
- decl += " :BUILTIN store";
- decl += ")";
- AddDeclaration(decl);
-
- if (CommandLineOptions.Clo.MonomorphicArrays && !CommandLineOptions.Clo.UseArrayTheory) {
- var sel = SimplifyLikeExprLineariser.SelectOpName(node);
-
- if (!KnownSelectFunctions.Contains(name)) {
- // need to declare it before reference
- string seldecl = "(DEFOP " + sel;
- foreach (VCExpr ch in node) {
- seldecl += " " + TypeToString(ch.Type);
- }
- AddDeclaration(seldecl + ")");
- KnownSelectFunctions.Add(name);
- }
-
- var eq = "EQ";
- if (node[node.Arity - 1].Type.IsBool)
- eq = "IFF";
-
- string ax1 = "(BG_PUSH (FORALL (";
- string ax2 = "(BG_PUSH (FORALL (";
- string argX = "", argY = "";
- string dist = "";
- for (int i = 0; i < node.Arity; i++) {
- var t = " :TYPE " + TypeToString(node[i].Type);
- var x = " x" + i;
- var y = " y" + i;
- ax1 += x + t;
- ax2 += x + t;
- if (i != 0 && i != node.Arity - 1) {
- argX += x;
- argY += y;
- ax2 += y + t;
- dist += " (NEQ" + x + y + ")";
- }
- }
- string v = " x" + (node.Arity - 1);
- ax1 += ") ";
- ax1 += "(" + eq + " (" + sel + " (" + name + " x0" + argX + v + ")" + argX + ") " + v + ")";
- ax1 += "))";
-
- ax2 += ") ";
- ax2 += "(IMPLIES (OR " + dist + ") (" + eq + " (" + sel + " (" + name + " x0" + argX + v + ")" + argY + ") (" + sel + " x0" + argY + ")))";
- ax2 += "))";
-
- AddDeclaration(ax1);
- AddDeclaration(ax2);
- }
-
- KnownStoreFunctions.Add(name);
- }
- //
- } else if (node.Op is VCExprSelectOp) {
- //
- RegisterType(node[0].Type);
- string name = SimplifyLikeExprLineariser.SelectOpName(node);
- if (!KnownSelectFunctions.Contains(name)) {
- string decl = "(DEFOP " + name;
-
- foreach (VCExpr ch in node) {
- decl += " " + TypeToString(ch.Type);
- }
- decl += " " + TypeToString(node.Type);
-
- if (CommandLineOptions.Clo.UseArrayTheory)
- decl += " :BUILTIN select";
- decl += ")";
- AddDeclaration(decl);
- KnownSelectFunctions.Add(name);
- }
- //
- } else {
- //
- VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;
- if (op != null && !KnownFunctions.Contains(op.Func)) {
- Function f = op.Func;
- Contract.Assert(f!=null);
- string printedName = Namer.GetName(f, f.Name);
- Contract.Assert(printedName!=null);
- string decl = "(DEFOP " + SimplifyLikeExprLineariser.MakeIdPrintable(printedName);
-
- foreach (Variable v in f.InParams) {
- Contract.Assert(v!=null);
- decl += " " + TypeToString(v.TypedIdent.Type);
- RegisterType(v.TypedIdent.Type);
- }
- Contract.Assert(f.OutParams.Length == 1);
- foreach (Variable v in f.OutParams) {
- Contract.Assert(v!=null);
- decl += " " + TypeToString(v.TypedIdent.Type);
- RegisterType(v.TypedIdent.Type);
- }
-
- string builtin = ExtractBuiltin(f);
- if (builtin != null)
- decl += " :BUILTIN " + builtin;
-
- decl += ")";
-
- AddDeclaration(decl);
- KnownFunctions.Add(f);
- }
- //
- }
-
- return base.Visit(node, arg);
- }
-
- private string ExtractBuiltin(Function f) {
- Contract.Requires(f != null);
- string retVal = null;
- if (NativeBv) {
- retVal = f.FindStringAttribute("bvbuiltin");
- }
- if (retVal == null) {
- retVal = f.FindStringAttribute("builtin");
- }
- return retVal;
- }
-
- public override bool Visit(VCExprVar node, bool arg) {
- Contract.Requires(node != null);
- if (!BoundTermVars.Contains(node) && !KnownVariables.Contains(node)) {
- RegisterType(node.Type);
- string printedName = Namer.GetName(node, node.Name);
- Contract.Assert(printedName!=null);
- string decl =
- "(DEFOP " + SimplifyLikeExprLineariser.MakeIdPrintable(printedName)
- + " " + TypeToString(node.Type) + ")";
- AddDeclaration(decl);
- KnownVariables.Add(node);
- }
-
- return base.Visit(node, arg);
- }
-
- public override bool Visit(VCExprQuantifier node, bool arg) {
- Contract.Requires(node != null);
- foreach (VCExprVar v in node.BoundVars) {
- Contract.Assert(v != null);
- RegisterType(v.Type);
- }
-
- return base.Visit(node, arg);
- }
- }
-} \ No newline at end of file
diff --git a/Source/Provers/Z3/Z3.csproj b/Source/Provers/Z3/Z3.csproj
deleted file mode 100644
index e559b663..00000000
--- a/Source/Provers/Z3/Z3.csproj
+++ /dev/null
@@ -1,218 +0,0 @@
-<?xml version="1.0" encoding="utf-8"?>
-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
- <PropertyGroup>
- <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
- <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
- <ProductVersion>9.0.21022</ProductVersion>
- <SchemaVersion>2.0</SchemaVersion>
- <ProjectGuid>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</ProjectGuid>
- <OutputType>Library</OutputType>
- <AppDesignerFolder>Properties</AppDesignerFolder>
- <RootNamespace>Microsoft.Boogie.Z3</RootNamespace>
- <AssemblyName>Provers.Z3</AssemblyName>
- <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
- <FileAlignment>512</FileAlignment>
- <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
- <SignAssembly>true</SignAssembly>
- <AssemblyOriginatorKeyFile>..\..\InterimKey.snk</AssemblyOriginatorKeyFile>
- <FileUpgradeFlags>
- </FileUpgradeFlags>
- <OldToolsVersion>3.5</OldToolsVersion>
- <UpgradeBackupLocation />
- <PublishUrl>publish\</PublishUrl>
- <Install>true</Install>
- <InstallFrom>Disk</InstallFrom>
- <UpdateEnabled>false</UpdateEnabled>
- <UpdateMode>Foreground</UpdateMode>
- <UpdateInterval>7</UpdateInterval>
- <UpdateIntervalUnits>Days</UpdateIntervalUnits>
- <UpdatePeriodically>false</UpdatePeriodically>
- <UpdateRequired>false</UpdateRequired>
- <MapFileExtensions>true</MapFileExtensions>
- <ApplicationRevision>0</ApplicationRevision>
- <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
- <IsWebBootstrapper>false</IsWebBootstrapper>
- <UseApplicationTrust>false</UseApplicationTrust>
- <BootstrapperEnabled>true</BootstrapperEnabled>
- <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>
- <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly>
- </CodeContractsCustomRewriterAssembly>
- <CodeContractsCustomRewriterClass>
- </CodeContractsCustomRewriterClass>
- <CodeContractsLibPaths>
- </CodeContractsLibPaths>
- <CodeContractsExtraRewriteOptions>
- </CodeContractsExtraRewriteOptions>
- <CodeContractsExtraAnalysisOptions>
- </CodeContractsExtraAnalysisOptions>
- <CodeContractsBaseLineFile>
- </CodeContractsBaseLineFile>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </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>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\z3apidebug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisRuleAssemblies>
- </CodeAnalysisRuleAssemblies>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>Migrated rules for Z3.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\Checked\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisLogFile>bin\Debug\Provers.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
- <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
- </PropertyGroup>
- <ItemGroup>
- <Reference Include="System" />
- <Reference Include="System.Core">
- <RequiredTargetFramework>3.5</RequiredTargetFramework>
- </Reference>
- <Reference Include="System.Data" />
- <Reference Include="System.Xml" />
- </ItemGroup>
- <ItemGroup>
- <Compile Include="Inspector.cs" />
- <Compile Include="Prover.cs" />
- <Compile Include="ProverInterface.cs" />
- <Compile Include="TypeDeclCollector.cs" />
- <Compile Include="..\..\version.cs" />
- </ItemGroup>
- <ItemGroup>
- <ProjectReference Include="..\..\AIFramework\AIFramework.csproj">
- <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
- <Name>AIFramework</Name>
- </ProjectReference>
- <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="..\..\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>
- <ProjectReference Include="..\Simplify\Simplify.csproj">
- <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>
- <Name>Simplify</Name>
- </ProjectReference>
- </ItemGroup>
- <ItemGroup>
- <Folder Include="Properties\" />
- </ItemGroup>
- <ItemGroup>
- <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
- <Install>false</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
- <Visible>False</Visible>
- <ProductName>Windows Installer 3.1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- </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/Provers/Z3/cce.cs b/Source/Provers/Z3/cce.cs
deleted file mode 100644
index ef594484..00000000
--- a/Source/Provers/Z3/cce.cs
+++ /dev/null
@@ -1,193 +0,0 @@
-using System;
-using SA=System.Attribute;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.Text;
-//using Microsoft.Boogie;
-
-/// <summary>
-/// A class containing static methods to extend the functionality of Code Contracts
-/// </summary>
-
-public static class cce {
- //[Pure]
- //public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {
- // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());
- //}
- [Pure]
- public static T NonNull<T>(T t) {
- Contract.Assert(t != null);
- return t;
- }
- [Pure]
- public static bool NonNullElements<T>(IEnumerable<T> collection) {
- return collection != null && Contract.ForAll(collection, c => c != null);
- }
- [Pure]
- public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {
- return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair));
- }
- //[Pure]
- //public static bool NonNullElements(VariableSeq collection) {
- // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);
- //}
- /// <summary>
- /// For possibly-null lists of non-null elements
- /// </summary>
- /// <typeparam name="T"></typeparam>
- /// <param name="collection"></param>
- /// <param name="nullability">If true, the collection is treated as an IEnumerable&lt;T!&gt;?, rather than an IEnumerable&lt;T!&gt;!</param>
- /// <returns></returns>
- [Pure]
- public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) {
- return (nullability && collection == null) || cce.NonNullElements(collection);
- //Should be the same as:
- /*if(nullability&&collection==null)
- * return true;
- * return cce.NonNullElements(collection)
- */
-
- }
- [Pure]
- public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {
- return kvp.Key != null && kvp.Value != null;
- }
- [Pure]
- public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {
- return iEnumerator != null;
- }
- //[Pure]
- //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {
- // return cce.NonNullElements(graph.TopologicalSort());
- //}
- [Pure]
- public static void BeginExpose(object o) {
- }
- [Pure]
- public static void EndExpose() {
- }
- [Pure]
- public static bool IsPeerConsistent(object o) {
- return true;
- }
- [Pure]
- public static bool IsConsistent(object o) {
- return true;
- }
- [Pure]
- public static bool IsExposable(object o) {
- return true;
- }
- [Pure]
- public static bool IsExposed(object o) {
- return true;
- }
- [Pure]
- public static bool IsNew(object o) {
- return true;
- }
- public static class Owner {
- [Pure]
- public static bool Same(object o, object p) {
- return true;
- }
- [Pure]
- public static void AssignSame(object o, object p) {
- }
- [Pure]
- public static object ElementProxy(object o) {
- return o;
- }
- [Pure]
- public static bool None(object o) {
- return true;
- }
- [Pure]
- public static bool Different(object o, object p) {
- return true;
- }
- [Pure]
- public static bool New(object o) {
- return true;
- }
- }
- [Pure]
- public static void LoopInvariant(bool p) {
- Contract.Assert(p);
- }
- public class UnreachableException : Exception {
- public UnreachableException() {
- }
- }
- //[Pure]
- //public static bool IsValid(Microsoft.Dafny.Expression expression) {
- // return true;
- //}
- //public static List<T> toList<T>(PureCollections.Sequence s) {
- // List<T> toRet = new List<T>();
- // foreach (T t in s.elems)
- // if(t!=null)
- // toRet.Add(t);
- // return toRet;
- //}
-
- //internal static bool NonNullElements(Set set) {
- // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);
- //}
-}
-
-public class PeerAttribute : SA {
-}
-public class RepAttribute : SA {
-}
-public class CapturedAttribute : SA {
-}
-public class NotDelayedAttribute : SA {
-}
-public class NoDefaultContractAttribute : SA {
-}
-public class VerifyAttribute : SA {
- public VerifyAttribute(bool b) {
-
- }
-}
-public class StrictReadonlyAttribute : SA {
-}
-public class AdditiveAttribute : SA {
-}
-public class ReadsAttribute : SA {
- public enum Reads {
- Nothing,
- Everything,
- };
- public ReadsAttribute(object o) {
- }
-}
-public class GlobalAccessAttribute : SA {
- public GlobalAccessAttribute(bool b) {
- }
-}
-public class EscapesAttribute : SA {
- public EscapesAttribute(bool b, bool b_2) {
- }
-}
-public class NeedsContractsAttribute : SA {
- public NeedsContractsAttribute() {
- }
- public NeedsContractsAttribute(bool ret, bool parameters) {
- }
- public NeedsContractsAttribute(bool ret, int[] parameters) {
- }
-}
-public class ImmutableAttribute : SA {
-}
-public class InsideAttribute : SA {
-}
-public class SpecPublicAttribute : SA {
-}
-public class ElementsPeerAttribute : SA {
-}
-public class ResultNotNewlyAllocatedAttribute : SA {
-}
-public class OnceAttribute : SA {
-} \ No newline at end of file
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index ca0c0e59..795fc9ca 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -10,7 +10,7 @@ using System.Diagnostics;
using System.Threading;
using System.IO;
using Microsoft.Boogie;
-using Graphing;
+using Microsoft.Boogie.GraphUtil;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
diff --git a/Source/VCGeneration/GraphAlgorithms.cs b/Source/VCGeneration/GraphAlgorithms.cs
deleted file mode 100644
index 006a923f..00000000
--- a/Source/VCGeneration/GraphAlgorithms.cs
+++ /dev/null
@@ -1,127 +0,0 @@
-using Graphing;
-using System;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.Linq;
-
-namespace Microsoft.Boogie {
-
-public static class GraphAlgorithms {
-
- public static Graph<Node> Dual<Node>(this Graph<Node> g, Node dummySource) {
- var exits = g.Nodes.Where(n => g.Successors(n).Count() == 0).ToList();
- if (exits.Count == 0)
- return null;
- var dual = new Graph<Node>(new HashSet<Tuple<Node, Node>>(g.Edges.Select(e => new Tuple<Node, Node>(e.Item2, e.Item1))));
- if (exits.Count == 1)
- dual.AddSource(exits[0]);
- else {
- dual.AddSource(dummySource);
- foreach (var exit in exits)
- dual.AddEdge(dummySource, exit);
- }
- return dual;
- }
-
- public static List<Tuple<Node, bool>> LoopyTopSort<Node>(this Graph<Node> g) {
- Contract.Assert(g.Reducible);
-
- int n = g.Nodes.Count;
- var nodeToNumber = new Dictionary<Node, int>(n);
- var numberToNode = new Node[n];
- var allNodes = new List<int>();
- int counter = 0;
- foreach (Node node in g.Nodes) {
- numberToNode[counter] = node;
- nodeToNumber[node] = counter;
- allNodes.Add(counter);
- counter++;
- }
-
- var loops = new List<int>[n];
- foreach (var h in g.Headers) {
- var loopNodes = new HashSet<Node>();
- foreach (var b in g.BackEdgeNodes(h))
- loopNodes.UnionWith(g.NaturalLoops(h, b));
- loops[nodeToNumber[h]] =
- new List<int>(loopNodes.Select(node => nodeToNumber[node]));
- }
-
- var successors = new List<int>[n];
- int[] incomingEdges = new int[n];
-
- foreach (var e in g.Edges) {
- Contract.Assert(e.Item1 != null);
- Contract.Assert(e.Item2 != null);
- int source = nodeToNumber[e.Item1], target = nodeToNumber[e.Item2];
- if (loops[target] == null || !loops[target].Contains(source)) {
- if (successors[source] == null)
- successors[source] = new List<int>();
- successors[source].Add(target);
- incomingEdges[target]++;
- }
- }
-
- var sortedNodes = new List<Tuple<Node, bool>>();
-
- var regionStack = new Stack<Tuple<Node, List<int>>>();
- regionStack.Push(new Tuple<Node, List<int>>(default(Node), allNodes));
-
- while (regionStack.Count != 0) {
- int rootIndex = -1;
- foreach (var i in regionStack.Peek().Item2) {
- if (incomingEdges[i] == 0) {
- rootIndex = i;
- break;
- }
- }
- if (rootIndex == -1) {
- var region = regionStack.Pop();
- if (regionStack.Count != 0)
- sortedNodes.Add(new Tuple<Node, bool>(region.Item1, true));
- continue;
- }
- incomingEdges[rootIndex] = -1;
- sortedNodes.Add(new Tuple<Node, bool>(numberToNode[rootIndex], false));
- if (successors[rootIndex] != null)
- foreach (int s in successors[rootIndex])
- incomingEdges[s]--;
- if (loops[rootIndex] != null)
- regionStack.Push(new Tuple<Node, List<int>>(numberToNode[rootIndex],
- loops[rootIndex]));
- }
-
- return sortedNodes;
- }
-
- // Algorithm from Jeanne Ferrante, Karl J. Ottenstein, Joe D. Warren,
- // "The Program Dependence Graph and Its Use in Optimization"
- public static Dictionary<Node, HashSet<Node>> ControlDependence<Node>(this Graph<Node> g) where Node : class, new() {
- Graph<Node> dual = g.Dual(new Node());
- DomRelation<Node> pdom = dual.DominatorMap;
- var result = new Dictionary<Node, HashSet<Node>>();
-
- var S = g.Edges.Where(e => !pdom.DominatedBy(e.Item1, e.Item2));
- foreach (var edge in S) {
- var L = pdom.LeastCommonAncestor(edge.Item1, edge.Item2);
- var deps = new List<Node>();
- if (L == edge.Item1) {
- pdom.DominatedBy(edge.Item2, edge.Item1, deps);
- deps.Add(edge.Item2);
- deps.Add(edge.Item1);
- } else {
- pdom.DominatedBy(edge.Item2, L, deps);
- deps.Add(edge.Item2);
- }
- if (result.ContainsKey(edge.Item1)) {
- result[edge.Item1].UnionWith(deps);
- } else {
- result[edge.Item1] = new HashSet<Node>(deps);
- }
- }
- return result;
- }
-
-}
-
-}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 5c6a5f68..6ad97141 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -7,7 +7,7 @@ using System.Linq;
using System.Text;
using System.IO;
using Microsoft.Boogie;
-using Graphing;
+using Microsoft.Boogie.GraphUtil;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 6efae58c..b13b7e35 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -11,7 +11,7 @@ using System.Linq;
using System.Threading;
using System.IO;
using Microsoft.Boogie;
-using Graphing;
+using Microsoft.Boogie.GraphUtil;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
@@ -2058,12 +2058,6 @@ namespace VC {
}
#endregion
- if (CommandLineOptions.Clo.DoPredication && CommandLineOptions.Clo.StratifiedInlining == 0) {
- DesugarCalls(impl);
- BlockPredicator.Predicate(program, impl);
- impl.ComputePredecessorsForBlocks();
- }
-
if (CommandLineOptions.Clo.LiveVariableAnalysis > 0) {
Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);
}
@@ -3038,36 +3032,6 @@ namespace VC {
}
}
- /// <summary>
- /// Simplifies the CFG of the given implementation impl by merging each
- /// basic block with a single predecessor into that predecessor if the
- /// predecessor has a single successor. If a uniformity analyser is
- /// being used then block will only be merged if they are both uniform
- /// or both non-uniform
- /// </summary>
- public static void MergeBlocksIntoPredecessors(Program prog, Implementation impl, UniformityAnalyser uni) {
- var blockGraph = prog.ProcessLoops(impl);
- var predMap = new Dictionary<Block, Block>();
- foreach (var block in blockGraph.Nodes) {
- try {
- var pred = blockGraph.Predecessors(block).Single();
- if (blockGraph.Successors(pred).Single() == block &&
- (uni == null ||
- (uni.IsUniform(impl.Name, pred) && uni.IsUniform(impl.Name, block)) ||
- (!uni.IsUniform(impl.Name, pred) && !uni.IsUniform(impl.Name, block)))) {
- Block predMapping;
- while (predMap.TryGetValue(pred, out predMapping))
- pred = predMapping;
- pred.Cmds.AddRange(block.Cmds);
- pred.TransferCmd = block.TransferCmd;
- impl.Blocks.Remove(block);
- predMap[block] = pred;
- }
- // If Single throws an exception above (i.e. not exactly one pred/succ), skip this block.
- } catch (InvalidOperationException) {}
- }
- }
-
static void DumpMap(Hashtable /*Variable->Expr*/ map) {
Contract.Requires(map != null);
foreach (DictionaryEntry de in map) {
diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj
index 98958c66..0c98a891 100644
--- a/Source/VCGeneration/VCGeneration.csproj
+++ b/Source/VCGeneration/VCGeneration.csproj
@@ -144,22 +144,12 @@
<Reference Include="System.Xml" />
</ItemGroup>
<ItemGroup>
- <Compile Include="BlockPredicator.cs" />
<Compile Include="Check.cs" />
<Compile Include="ConditionGeneration.cs" />
<Compile Include="Context.cs" />
- <Compile Include="DoomCheck.cs" />
- <Compile Include="DoomedLoopUnrolling.cs" />
- <Compile Include="DoomedStrategy.cs" />
- <Compile Include="DoomErrorHandler.cs" />
- <Compile Include="GraphAlgorithms.cs" />
- <Compile Include="HasseDiagram.cs" />
<Compile Include="OrderingAxioms.cs" />
- <Compile Include="SmartBlockPredicator.cs" />
<Compile Include="StratifiedVC.cs" />
- <Compile Include="UniformityAnalyser.cs" />
<Compile Include="VC.cs" />
- <Compile Include="VCDoomed.cs" />
<Compile Include="..\version.cs" />
<Compile Include="Wlp.cs" />
</ItemGroup>
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
index c691d9da..39829bb0 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
@@ -255,11 +255,7 @@ namespace DafnyLanguage
ConditionGeneration vcgen = null;
try {
- if (Bpl.CommandLineOptions.Clo.vcVariety == Bpl.CommandLineOptions.VCVariety.Doomed) {
- vcgen = new DCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);
- } else {
- vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);
- }
+ vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);
} catch (Bpl.ProverException) {
return PipelineOutcome.FatalError;
}