diff options
| -rw-r--r-- | Source/Boogie.sln | 26 | ||||
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.csproj | 4 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLib.csproj | 10 | ||||
| -rw-r--r-- | Source/Provers/Simplify/Let2ImpliesVisitor.cs | 92 | ||||
| -rw-r--r-- | Source/Provers/Simplify/Prover.cs | 489 | ||||
| -rw-r--r-- | Source/Provers/Simplify/ProverInterface.cs | 650 | ||||
| -rw-r--r-- | Source/Provers/Simplify/Simplify.csproj | 252 |
7 files changed, 854 insertions, 669 deletions
diff --git a/Source/Boogie.sln b/Source/Boogie.sln index 364fd29c..0a3f8adb 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -3,8 +3,6 @@ Microsoft Visual Studio Solution File, Format Version 10.00 # Visual Studio 2008
Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Provers", "Provers", "{B758C1E3-824A-439F-AA2F-0BA1143E8C8D}"
EndProject
-Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "Simplify", "Provers\Simplify\Simplify.sscproj", "{F75666DE-FB56-457C-8782-09BE243450FC}"
-EndProject
Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "AIFramework", "AIFramework\AIFramework.sscproj", "{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"
EndProject
Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "Basetypes", "Basetypes\Basetypes.sscproj", "{0C692837-77EC-415F-BF04-395E3ED06E9A}"
@@ -27,6 +25,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Z3", "Provers\Z3\Z3.csproj" EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "Provers\SMTLib\SMTLib.csproj", "{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}"
EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Simplify", "Provers\Simplify\Simplify.csproj", "{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}"
+EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Debug|.NET = Debug|.NET
@@ -37,16 +37,6 @@ Global Release|Mixed Platforms = Release|Mixed Platforms
EndGlobalSection
GlobalSection(ProjectConfigurationPlatforms) = postSolution
- {F75666DE-FB56-457C-8782-09BE243450FC}.Debug|.NET.ActiveCfg = Debug|.NET
- {F75666DE-FB56-457C-8782-09BE243450FC}.Debug|.NET.Build.0 = Debug|.NET
- {F75666DE-FB56-457C-8782-09BE243450FC}.Debug|Any CPU.ActiveCfg = Debug|.NET
- {F75666DE-FB56-457C-8782-09BE243450FC}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET
- {F75666DE-FB56-457C-8782-09BE243450FC}.Debug|Mixed Platforms.Build.0 = Debug|.NET
- {F75666DE-FB56-457C-8782-09BE243450FC}.Release|.NET.ActiveCfg = Release|.NET
- {F75666DE-FB56-457C-8782-09BE243450FC}.Release|.NET.Build.0 = Release|.NET
- {F75666DE-FB56-457C-8782-09BE243450FC}.Release|Any CPU.ActiveCfg = Release|.NET
- {F75666DE-FB56-457C-8782-09BE243450FC}.Release|Mixed Platforms.ActiveCfg = Release|.NET
- {F75666DE-FB56-457C-8782-09BE243450FC}.Release|Mixed Platforms.Build.0 = Release|.NET
{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Debug|.NET.ActiveCfg = Debug|.NET
{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Debug|.NET.Build.0 = Debug|.NET
{24B55172-AD8B-47D1-8952-5A95CFDB9B31}.Debug|Any CPU.ActiveCfg = Debug|.NET
@@ -159,14 +149,24 @@ Global {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Any CPU.Build.0 = Release|Any CPU
{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|.NET.ActiveCfg = Release|Any CPU
+ {FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|Any CPU.Build.0 = Release|Any CPU
+ {FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|Mixed Platforms.Build.0 = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
EndGlobalSection
GlobalSection(NestedProjects) = preSolution
- {F75666DE-FB56-457C-8782-09BE243450FC} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
{435D5BD0-6F62-49F8-BB24-33E2257519AD} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
{9B163AA3-36BC-4AFB-88AB-79BC9E97E401} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
+ {FEE9F01B-9722-4A76-A24B-72A4016DFA8E} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
EndGlobalSection
EndGlobal
diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index a036c7e5..5a0f4ef1 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -113,8 +113,8 @@ <Project>{435D5BD0-6F62-49F8-BB24-33E2257519AD}</Project>
<Name>Isabelle</Name>
</ProjectReference>
- <ProjectReference Include="..\Provers\Simplify\Simplify.sscproj">
- <Project>{F75666DE-FB56-457C-8782-09BE243450FC}</Project>
+ <ProjectReference Include="..\Provers\Simplify\Simplify.csproj">
+ <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>
<Name>Simplify</Name>
</ProjectReference>
<ProjectReference Include="..\Provers\SMTLib\SMTLib.csproj">
diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj index 37ea2536..235a99ca 100644 --- a/Source/Provers/SMTLib/SMTLib.csproj +++ b/Source/Provers/SMTLib/SMTLib.csproj @@ -77,10 +77,6 @@ <SpecificVersion>False</SpecificVersion>
<HintPath>..\..\..\Binaries\Microsoft.Contracts.dll</HintPath>
</Reference>
- <Reference Include="Provers.Simplify, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>..\Simplify\bin\debug\Provers.Simplify.dll</HintPath>
- </Reference>
<Reference Include="System" />
<Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
<SpecificVersion>False</SpecificVersion>
@@ -107,6 +103,12 @@ <Compile Include="TypeDeclCollector.cs" />
</ItemGroup>
<ItemGroup>
+ <ProjectReference Include="..\Simplify\Simplify.csproj">
+ <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>
+ <Name>Simplify</Name>
+ </ProjectReference>
+ </ItemGroup>
+ <ItemGroup>
<Folder Include="Properties\" />
</ItemGroup>
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
diff --git a/Source/Provers/Simplify/Let2ImpliesVisitor.cs b/Source/Provers/Simplify/Let2ImpliesVisitor.cs index 0dc52516..960a0a8d 100644 --- a/Source/Provers/Simplify/Let2ImpliesVisitor.cs +++ b/Source/Provers/Simplify/Let2ImpliesVisitor.cs @@ -7,7 +7,7 @@ using System; using System.Collections;
using System.Collections.Generic;
using System.Diagnostics;
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
using Microsoft.Boogie.VCExprAST;
namespace Microsoft.Boogie.Simplify
@@ -21,11 +21,14 @@ namespace Microsoft.Boogie.Simplify public class Let2ImpliesMutator : SubstitutingVCExprVisitor {
- public Let2ImpliesMutator(VCExpressionGenerator! gen) {
- this(gen, false, false);
+ 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);
+
+ public Let2ImpliesMutator(VCExpressionGenerator gen, bool keepLetTerm, bool keepLetFormula):base(gen) {
+ Contract.Requires(gen!=null);
+
this.keepLetTerm = keepLetTerm;
this.keepLetFormula = keepLetFormula;
}
@@ -33,7 +36,10 @@ namespace Microsoft.Boogie.Simplify readonly bool keepLetTerm;
readonly bool keepLetFormula;
- public VCExpr! Mutate(VCExpr! expr) {
+ public VCExpr Mutate(VCExpr expr) {
+ Contract.Requires(expr != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
return Mutate(expr, new VCExprSubstitution ());
}
@@ -69,14 +75,24 @@ namespace Microsoft.Boogie.Simplify }
}
- private IDictionary<VCExprVar!, OccurrenceTypes>! VarOccurrences =
- new Dictionary<VCExprVar!, OccurrenceTypes>();
+ private IDictionary<VCExprVar/*!*/, OccurrenceTypes>/*!*/ VarOccurrences =
+ new Dictionary<VCExprVar/*!*/, OccurrenceTypes>();
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(cce.NonNullElements(VarOccurrences));
+}
////////////////////////////////////////////////////////////////////////////
- public override VCExpr! Visit(VCExprVar! node,
- VCExprSubstitution! substitution) {
- VCExpr! res = base.Visit(node, substitution);
+ 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) {
@@ -97,23 +113,29 @@ namespace Microsoft.Boogie.Simplify return res;
}
- public override VCExpr! Visit(VCExprNAry! node,
- VCExprSubstitution! substitution) {
+ 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;
+ 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);
+ VCExpr newArg0 = Mutate(node[0], substitution);
+ Contract.Assert(newArg0 != null);
polarity = -polarity;
- VCExpr! newArg1 = Mutate(node[1], substitution);
+ VCExpr newArg1 = Mutate(node[1], substitution);
+ Contract.Assert(newArg1 != null);
res = Gen.Implies(newArg0, newArg1);
} else if (!node.Op.Equals(VCExpressionGenerator.AndOp) &&
@@ -131,11 +153,17 @@ namespace Microsoft.Boogie.Simplify return res;
}
- public override VCExpr! Visit(VCExprLet! originalNode,
- VCExprSubstitution! substitution) {
+ 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);
- VCExpr! newNode = letSorter.Mutate(originalNode, true);
+ 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)
@@ -146,24 +174,26 @@ namespace Microsoft.Boogie.Simplify 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!> ();
+ List<VCExprLetBinding> bindings = new List<VCExprLetBinding> ();
+ List<VCExprLetBinding> keepBindings = new List<VCExprLetBinding> ();
- foreach (VCExprLetBinding! binding in node) {
+ 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);
-
+ 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
- assert polarity > 0;
+ Contract.Assert( polarity > 0);
if (keepLetFormula) {
keepBindings.Add(Gen.LetBinding(binding.V, newE));
} else {
- VCExprVar! newVar = Gen.Variable(binding.V.Name, Type.Bool);
+ VCExprVar newVar = Gen.Variable(binding.V.Name, Type.Bool);
+ Contract.Assert(newVar != null);
substitution[binding.V] = newVar;
bindings.Add(Gen.LetBinding(newVar, newE));
@@ -178,7 +208,8 @@ namespace Microsoft.Boogie.Simplify }
}
- VCExpr! newBody = Mutate(node.Body, substitution);
+ VCExpr newBody = Mutate(node.Body, substitution);
+ Contract.Assert(newBody != null);
if (keepBindings.Count > 0) {
newBody = Gen.Let(keepBindings, newBody);
}
@@ -187,10 +218,11 @@ namespace Microsoft.Boogie.Simplify // 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) {
+ foreach (VCExprLetBinding b in bindings) {
+ Contract.Assert(b != null);
OccurrenceTypes occ;
if (VarOccurrences.TryGetValue(b.V, out occ))
- assert occ == OccurrenceTypes.None || occ == OccurrenceTypes.Pos;
+ Contract.Assert( occ == OccurrenceTypes.None || occ == OccurrenceTypes.Pos);
}
return Gen.ImpliesSimp(Gen.AsImplications(bindings), newBody);
diff --git a/Source/Provers/Simplify/Prover.cs b/Source/Provers/Simplify/Prover.cs index 641c81f4..6db18cb4 100644 --- a/Source/Provers/Simplify/Prover.cs +++ b/Source/Provers/Simplify/Prover.cs @@ -6,176 +6,212 @@ using System;
using System.IO;
using System.Diagnostics;
+using System.Diagnostics.Contracts;
using System.Collections;
using System.Collections.Generic;
-using util;
-using Microsoft.Contracts;
+//using util;
using Microsoft.Boogie;
// Simplified interface to an external prover like Simplify or the z3 process, taken from Bird.
-namespace Microsoft.Boogie.Simplify
-{
+namespace Microsoft.Boogie.Simplify {
/// <summary>
/// An interface to Simplify theorem prover.
/// </summary>
- public abstract class ProverProcess
- {
+ 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 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; }
+ 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
- requires IsPeerConsistent;
- modifies this.*;
+ //modifies this.*;
{
- expose (this) {
+ Contract.Requires(cce.IsPeerConsistent(this));
+ cce.BeginExpose(this);
+ {
simplify.Refresh();
#if WHIDBEY
return simplify.PeakVirtualMemorySize64;
#else
- return simplify.PeakPagedMemorySize64;
+ return simplify.PeakPagedMemorySize64;
#endif
}
+ cce.EndExpose();
}
}
-
+
public bool HasExited {
- get { return simplify.HasExited; }
+ get {
+ return simplify.HasExited;
+ }
}
-
- public ProverProcess(ProcessStartInfo! psi, string! proverPath)
- { // throws ProverException
- try
- {
+
+ 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)
- {
+ } 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 abstract string OptionComments();
+
+ //[Pure(false)]
+ public virtual IEnumerable<string/*!>!*/> ParameterSettings {
+ get {
+ yield break;
+ }
+ }
+
public void Close()
- modifies this.*;
+ //modifies this.*;
{
- expose (this) {
+ cce.BeginExpose(this);
+ {
toSimplify.Flush();
- if (this.simplify != null)
- {
- if (!simplify.HasExited)
- {
+ 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);
- }
+ 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 */ }
+ 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.*;
- throws UnexpectedProverOutputException;
+ public virtual void AddAxioms(string s)
+ //modifies this.*;
+ //modifies Console.Out.*, Console.Error.*;
{
- expose (this) {
- toSimplify.Write("(BG_PUSH ");
- toSimplify.Write(s);
- toSimplify.WriteLine(")");
- }
+ 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.*;
- throws UnexpectedProverOutputException;
+ public virtual void Feed(string s, int statementCount)
+ //modifies this.*;
+ //modifies Console.Out.*, Console.Error.*;
{
- expose (this) {
+ 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.*;
- throws UnexpectedProverOutputException;
+ public virtual void PopAxioms()
+ //modifies this.*;
+ //modifies Console.Out.*, Console.Error.*;
{
- expose (this) {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ cce.BeginExpose(this);
+ {
toSimplify.WriteLine("(BG_POP)");
}
+ cce.EndExpose();
}
public void ToFlush()
- modifies this.*;
+ //modifies this.*;
{
- expose (this) {
+ cce.BeginExpose(this);
+ {
toSimplify.Flush();
}
+ cce.EndExpose();
+ }
+
+ public enum ProverOutcome {
+ Valid,
+ NotValid,
+ TimeOut,
+ OutOfMemory,
+ Inconclusive
}
- 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.*;
+ 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.*;
- throws UnexpectedProverOutputException;
-
- protected abstract void DoBeginCheck(string! descriptiveName, string! formula)
- modifies this.*;
- modifies Console.Out.*, Console.Error.*;
+ public abstract ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler handler);
+ //modifies this.**;
+ //modifies Console.Out.*, Console.Error.*;
+ //modifies handler.*;
+ //TODO: Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+
+ 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)
@@ -184,16 +220,18 @@ namespace Microsoft.Boogie.Simplify /// 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)
- {
- List<string!> list = new List<string!>();
+ 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"
- invariant 0 <= j && j <= labels.Length;
+ // invariant: j is the number of characters of "labels" consumed so far
+ // invariant: an even number of '|' characters remain in "labels"
{
- j = labels.IndexOfAny(new char[]{'|', '+', '@'}, j);
+ cce.LoopInvariant(0 <= j && j <= labels.Length);
+ j = labels.IndexOfAny(new char[] { '|', '+', '@' }, j);
if (j < 0) {
// no more labels
return list;
@@ -201,31 +239,33 @@ namespace Microsoft.Boogie.Simplify char ch = labels[j];
if (ch == '|') {
j++; // skip the '|'
- assume j < labels.Length; // there should now be a '+' or '@'
+ Contract.Assume(j < labels.Length); // there should now be a '+' or '@'
ch = labels[j];
}
- assume ch == '+' || ch == '@';
+ Contract.Assume(ch == '+' || ch == '@');
j++; // skip the '+' or '@'
- int k = labels.IndexOfAny(new char[]{'|', ' ', ')'}, j);
- assume j+2 <= k;
- string s = labels.Substring(j, k-j);
+ 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;
+ j = k + 1;
}
}
- [Rep] char[] expectBuffer = null;
+ [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)
- requires 1 <= s.Length;
- modifies this.*;
- throws UnexpectedProverOutputException;
- {
+ 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
@@ -237,46 +277,39 @@ namespace Microsoft.Boogie.Simplify throw new UnexpectedProverOutputException("Expected \"" + s + "\", found:\r\n<<<start>>>\r\n" + str + "<<<end>>>");
}
}
-
+
string badInputPrefix;
- if (ch != s[0])
- {
+ if (ch != s[0]) {
badInputPrefix = Char.ToString((char)ch);
- }
- else
- {
+ } else {
int len = s.Length - 1;
- if (expectBuffer == null || expectBuffer.Length < len)
- {
- expose (this) {
+ if (expectBuffer == null || expectBuffer.Length < len) {
+ cce.BeginExpose(this);
+ {
expectBuffer = new char[len];
}
+ cce.EndExpose();
}
- try
- {
+ try {
string s0;
- expose (this) {
+ 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)
- {
+ if (s0.CompareTo(s1) == 0) {
badInputPrefix = null; // no error
- }
- else
- {
+ } else {
badInputPrefix = (char)ch + s0;
}
- }
- catch (IOException)
- {
+ } catch (IOException) {
throw new UnexpectedProverOutputException("Expected \"" + s + "\", encountered IO exception.");
}
}
- if (badInputPrefix != null)
- {
+ 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:
@@ -295,28 +328,32 @@ namespace Microsoft.Boogie.Simplify throw new UnexpectedProverOutputException("Expected \"" + s + "\", found:\r\n<<<start>>>\r\n" + badInputPrefix + remaining + "<<<end>>>");
}
}
-
+
protected int FromReadChar()
- modifies this.*;
+ //modifies this.*;
{
- expose (this) {
+ cce.BeginExpose(this);
+ {
return fromSimplify.Read();
}
+ cce.EndExpose();
}
- private void KillProver(object state)
- {
- expose (this) {
+ private void KillProver(object state) {
+ cce.BeginExpose(this);
+ {
this.readTimedOut = true;
simplify.Kill();
}
+ cce.EndExpose();
}
-
+
protected int FromReadChar(int timeout)
- requires -1 <= timeout;
- modifies this.*;
+ //modifies this.*;
{
- expose (this) {
+ Contract.Requires(-1 <= timeout);
+ 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();
@@ -324,12 +361,15 @@ namespace Microsoft.Boogie.Simplify t.Dispose();
return ch;
}
+ cce.EndExpose();
}
-
- protected string! FromReadLine()
- modifies this.*;
+
+ protected string FromReadLine()
+ //modifies this.*;
{
- expose (this) {
+ Contract.Ensures(Contract.Result<string>() != null);
+ cce.BeginExpose(this);
+ {
string s = fromSimplify.ReadLine();
if (s == null) {
// this is what ReadLine returns if all characters have been read
@@ -337,12 +377,16 @@ namespace Microsoft.Boogie.Simplify }
return s;
}
+ cce.EndExpose();
}
-
- protected string! FromStdErrorAll ()
- modifies this.*;
+
+ protected string FromStdErrorAll()
+ //modifies this.*;
{
- expose (this) {
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ cce.BeginExpose(this);
+ {
if (fromStdError != null) {
string s = fromStdError.ReadToEnd();
if (s == null) {
@@ -351,33 +395,39 @@ namespace Microsoft.Boogie.Simplify }
return s;
}
- // there is no StdErrorReader available
+ // there is no StdErrorReader available
else {
return "";
}
}
+ cce.EndExpose();
}
-
- protected void ToWriteLine(string! s)
- modifies this.*;
+
+ protected void ToWriteLine(string s)
+ //modifies this.*;
{
- expose (this) {
+ Contract.Requires(s != null);
+ cce.BeginExpose(this);
+ {
toSimplify.WriteLine(s);
}
+ cce.EndExpose();
}
}
-
+
// derived by Z3ProverProcess
public class SimplifyProverProcess : ProverProcess {
- public SimplifyProverProcess(string! proverPath, bool dummy)
- { // throws ProverException
- ProcessStartInfo psi = new ProcessStartInfo(proverPath, "-labelsonly");
+ 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;
- assume psi.EnvironmentVariables != null; // by inspecting the code through Reflector; the documentation says this property is "null by default", whatever that means --KRML
+ 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();
}
@@ -387,12 +437,13 @@ namespace Microsoft.Boogie.Simplify if (0 <= CommandLineOptions.Clo.ProverCCLimit) {
psi.EnvironmentVariables["PROVER_CC_LIMIT"] = CommandLineOptions.Clo.ProverCCLimit.ToString();
}
-
- base(psi, proverPath);
+ return psi;
}
+
+
+ public override string OptionComments() {
+ Contract.Ensures(Contract.Result<string>() != null);
- public override string! OptionComments()
- {
// would we want the timeout stuff here?
return "";
}
@@ -400,20 +451,20 @@ namespace Microsoft.Boogie.Simplify [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)
- modifies Console.Out.*, Console.Error.*;
- throws UnexpectedProverOutputException;
+ [Verify(false)]
+ public SimplifyProverProcess(string proverPath):base(getPSI(proverPath),proverPath)
+ //modifies Console.Out.*, Console.Error.*;
{
- this(proverPath, true);
+ Contract.Requires(proverPath != null);
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
EatPrompt();
}
- private void EatPrompt()
- modifies this.*;
- modifies Console.Out.*, Console.Error.*;
- throws UnexpectedProverOutputException;
+ private void EatPrompt()
+ //modifies this.*;
+ //modifies Console.Out.*, Console.Error.*;
{
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
// skips text matching the regular expression: (white space)* ">\t"
ToFlush();
@@ -421,26 +472,26 @@ namespace Microsoft.Boogie.Simplify do {
ch = FromReadChar();
} while (Char.IsWhiteSpace((char)ch));
-
+
while (ch == 'W') {
ch = ConsumeWarnings(ch, null);
}
-
+
Expect(ch, ">\t");
}
-
- public override void AddAxioms(string! s)
- throws UnexpectedProverOutputException;
- {
+
+ 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)
- throws UnexpectedProverOutputException;
- {
+
+ 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)");
@@ -448,46 +499,43 @@ namespace Microsoft.Boogie.Simplify EatPrompt();
}
}
-
- public override void PopAxioms()
- throws UnexpectedProverOutputException;
- {
+
+ public override void PopAxioms() {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
base.PopAxioms();
EatPrompt();
}
- protected override void DoBeginCheck(string! descriptiveName, string! formula)
- {
+ 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)
- throws UnexpectedProverOutputException;
- {
+ 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')
- {
+ while (ch == 'W') {
ch = ConsumeWarnings(ch, handler);
}
- if (ch == 'E')
- {
+ if (ch == 'E') {
Expect(ch, "Exceeded PROVER_KILL_TIME -- discontinuing search for counterexamples.");
FromReadLine();
ch = FromReadChar();
- if (ch == '\n')
- {
+ if (ch == '\n') {
ch = FromReadChar();
}
Expect(ch, " labels:");
@@ -501,8 +549,7 @@ namespace Microsoft.Boogie.Simplify ch = FromReadChar();
return ProverOutcome.TimeOut;
}
- if ('0' <= ch && ch <= '9')
- {
+ if ('0' <= ch && ch <= '9') {
// Valid!
do {
ch = FromReadChar();
@@ -510,18 +557,15 @@ namespace Microsoft.Boogie.Simplify Expect(ch, ": Valid.");
outcome = ProverOutcome.Valid;
ToWriteLine(String.Format("; FORMULA {0} IS VALID!", NumFormulasChecked + 1 /*Simplify starts at 1*/));
- }
- else
- {
+ } else {
// now we expect one or more counterexample contexts, each proving a list of labels
do {
- List<string!> labels = ReadLabels(ch);
+ 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')
- {
+ while ('0' <= ch && ch <= '9') {
ch = FromReadChar();
}
Expect(ch, ": Invalid.");
@@ -533,36 +577,35 @@ namespace Microsoft.Boogie.Simplify return outcome;
}
- List<string!>! ReadLabels(int ch)
- modifies this.*;
- throws UnexpectedProverOutputException;
+ 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 == ' ')
- {
+ 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!>();
+ } else {
+ theLabels = new List<string>();
}
Expect(ch, "\n"); // empty line
return theLabels;
}
-
+
int ConsumeWarnings(int ch, Microsoft.Boogie.ProverInterface.ErrorHandler handler)
- requires ch == 'W';
- modifies this.*;
- modifies Console.Out.*, Console.Error.*;
- throws UnexpectedProverOutputException;
+ //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")) {
@@ -573,12 +616,12 @@ namespace Microsoft.Boogie.Simplify FromReadLine(); // blank line
FromReadLine(); // expression (entire quantifier)
}
-
- if (handler != null) handler.OnProverWarning(w);
-
+
+ if (handler != null)
+ handler.OnProverWarning(w);
+
ch = FromReadChar();
- if (ch == '\n')
- {
+ 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();
@@ -586,6 +629,6 @@ namespace Microsoft.Boogie.Simplify return ch;
}
}
-
+
}
diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs index dbd3ac19..923a62ef 100644 --- a/Source/Provers/Simplify/ProverInterface.cs +++ b/Source/Provers/Simplify/ProverInterface.cs @@ -10,25 +10,28 @@ using System.Threading; using System.IO;
using System.Text;
using System.Diagnostics;
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
using Microsoft.Boogie.AbstractInterpretation;
using Microsoft.Boogie.Simplify;
using Microsoft.Boogie.VCExprAST;
using Microsoft.Boogie.TypeErasure;
-namespace Microsoft.Boogie.Simplify
-{
- public abstract class LogProverInterface : ProverInterface
- {
+namespace Microsoft.Boogie.Simplify {
+ public abstract class LogProverInterface : ProverInterface {
[NotDelayed]
- protected LogProverInterface(ProverOptions! options,
- string! openComment, string! closeComment,
- string! openActivity, string! closeActivity,
- VCExpressionGenerator! gen)
- ensures this.gen == gen;
- {
+ 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!> ();
+ this.commonPrefix = new List<string>();
} else {
this.logFileWriter = options.OpenLog(null);
}
@@ -38,7 +41,6 @@ namespace Microsoft.Boogie.Simplify this.closeActivityString = closeActivity;
this.gen = gen;
this.options = options;
- base();
if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never) {
// Emit version comment in the log
@@ -46,34 +48,49 @@ namespace Microsoft.Boogie.Simplify LogCommonComment(CommandLineOptions.Clo.Environment);
}
}
-
- [StrictReadonly][Additive]
- protected readonly VCExpressionGenerator! gen;
+
+ [StrictReadonly]
+ [Additive]
+ protected readonly VCExpressionGenerator gen;
private TextWriter/*?*/ logFileWriter;
- [Microsoft.Contracts.StrictReadonly]
- private readonly string! openCommentString;
- [Microsoft.Contracts.StrictReadonly]
- private readonly string! closeCommentString;
- [Microsoft.Contracts.StrictReadonly]
- private readonly string! openActivityString;
- [Microsoft.Contracts.StrictReadonly]
- private readonly string! closeActivityString;
- [Microsoft.Contracts.StrictReadonly]
- protected readonly ProverOptions! options;
- [Microsoft.Contracts.StrictReadonly]
- private readonly List<string!>/*?*/ commonPrefix;
-
- public void LogActivity(string! s) {
+ [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(cce.NonNullElements(commonPrefix));
+ }
+
+
+ public void LogActivity(string s) {
+ Contract.Requires(s != null);
LogActivity(s, false);
}
- public void LogCommon(string! s) {
+ public void LogCommon(string s) {
+ Contract.Requires(s != null);
LogActivity(s, true);
}
- private void LogActivity(string! s, bool common) {
- assume common || !options.SeparateLogFiles || logFileWriter != null;
+ 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);
@@ -90,19 +107,19 @@ namespace Microsoft.Boogie.Simplify /// 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)
- {
+ public override void LogComment(string comment) {
+ Contract.Requires(comment != null);
LogComment(comment, false);
}
- public void LogCommonComment(string! comment)
- {
+ public void LogCommonComment(string comment) {
+ Contract.Requires(comment != null);
LogComment(comment, true);
}
- private void LogComment(string! comment, bool common)
- {
- assume common || !options.SeparateLogFiles || logFileWriter != null;
+ 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);
@@ -114,16 +131,18 @@ namespace Microsoft.Boogie.Simplify }
}
- public virtual void NewProblem(string! descName)
- {
+ 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)
+ foreach (string s in commonPrefix) {
+ Contract.Assert(s != null);
logFileWriter.WriteLine(s);
+ }
}
}
LogComment("Proof obligation: " + descName);
@@ -136,82 +155,104 @@ namespace Microsoft.Boogie.Simplify }
}
- public override VCExpressionGenerator! VCExprGen
- {
- get { return this.gen; }
+ 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;
- public abstract class ProcessTheoremProver : LogProverInterface
- {
- private static string! _proverPath;
+ protected AxiomVCExprTranslator vcExprTranslator {
+ get {
+ Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);
- protected AxiomVCExprTranslator! vcExprTranslator { get {
- return (AxiomVCExprTranslator!)ctx.exprTranslator;
- } }
+ return cce.NonNull((AxiomVCExprTranslator)ctx.exprTranslator);
+ }
+ }
- protected abstract AxiomVCExprTranslator! SpawnVCExprTranslator(ProverOptions! p);
+ protected abstract AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions p);
// Return the number of axioms pushed to the theorem prover
- protected int FeedNewAxiomsDecls2Prover() throws UnexpectedProverOutputException; {
+ protected int FeedNewAxiomsDecls2Prover() {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
if (thmProver == null)
return 0;
int ret = 0;
- foreach (string! s in vcExprTranslator.NewTypeDecls) {
+ foreach (string s in vcExprTranslator.NewTypeDecls) {
+ Contract.Assert(s != null);
LogCommon(s);
thmProver.Feed(s, 0);
}
- foreach (string! s in vcExprTranslator.NewAxioms) {
+ foreach (string s in vcExprTranslator.NewAxioms) {
+ Contract.Assert(s != null);
LogBgPush(s);
thmProver.AddAxioms(s);
- ret ++;
+ ret++;
}
return ret;
}
- protected static string! CodebaseString() {
- return Path.GetDirectoryName((!)System.Reflection.Assembly.GetExecutingAssembly().Location);
+ 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.NonNullElements(BackgroundPredicates));
+ Contract.Invariant(BackgroundPredFilename != null);
+ Contract.Invariant(ctx != null);
}
- private static IDictionary<string!, string!>! BackgroundPredicates =
- new Dictionary<string!, string!> ();
+ 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);
- protected static string! GetBackgroundPredicate(string! filename) {
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))
- {
+ using (StreamReader reader = new System.IO.StreamReader(univBackPredPath)) {
res = reader.ReadToEnd();
}
BackgroundPredicates.Add(filename, res);
}
- return (!)res;
+ return cce.NonNull(res);
}
- static void InitializeGlobalInformation(string! proverExe)
- ensures _proverPath != null;
+ static void InitializeGlobalInformation(string proverExe)
+
//throws ProverException, System.IO.FileNotFoundException;
{
+
+ Contract.Requires(proverExe != null);
+ Contract.Ensures(_proverPath != null);
if (_proverPath == null) {
// Initialize '_proverPath'
_proverPath = Path.Combine(CodebaseString(), proverExe);
string firstTry = _proverPath;
string programFiles = Environment.GetEnvironmentVariable("ProgramFiles");
- assert programFiles != null;
+ 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!> attempts = new List<string!>();
+ List<string> attempts = new List<string>();
for (int minorVersion = 15; true; minorVersion--) {
if (File.Exists(_proverPath)) {
break; // all seems good
@@ -242,24 +283,30 @@ namespace Microsoft.Boogie.Simplify }
}
- [Rep] protected internal ProverProcess thmProver;
+ [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;
-
+ protected DeclFreeProverContext ctx;
+ protected string BackgroundPredFilename;
+ protected ConsoleCancelEventHandler cancelEvent;
+
[NotDelayed]
- public ProcessTheoremProver(ProverOptions! options, VCExpressionGenerator! gen, DeclFreeProverContext! ctx,
- string! proverExe, string! backgroundPred)
- throws UnexpectedProverOutputException;
- {
+ 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;
- base(options, "; ", "", "", "", gen);
-
+
+
// 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
@@ -269,8 +316,8 @@ namespace Microsoft.Boogie.Simplify 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
+ List<string> x = tl.NewAxioms;
+ //x = x; // make the compiler happy: somebody uses the value of x
x = tl.NewTypeDecls;
}
}
@@ -278,40 +325,38 @@ namespace Microsoft.Boogie.Simplify /// <summary>
/// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)
/// </summary>
- public override void PushVCExpression(VCExpr! vc)
- {
- vcExprTranslator.AddAxiom( vcExprTranslator.translate(vc,1) );
+ public override void PushVCExpression(VCExpr vc) {
+ Contract.Requires(vc != null);
+ vcExprTranslator.AddAxiom(vcExprTranslator.translate(vc, 1));
}
-
- public override string! VCExpressionToString(VCExpr! vc)
- {
+
+ 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;
+ 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()
- throws UnexpectedProverOutputException;
- {
- return FeedNewAxiomsDecls2Prover();
+ public override int FlushAxiomsToTheoremProver() {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ return FeedNewAxiomsDecls2Prover();
}
- public override void Pop()
- throws UnexpectedProverOutputException;
- {
- assert thmProver != null;
- LogCommon("(BG_POP)");
- thmProver.PopAxioms();
+ 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)
- {
+ void ControlCHandler(object o, ConsoleCancelEventArgs a) {
if (thmProver != null) {
thmProver.Kill();
}
@@ -323,46 +368,50 @@ namespace Microsoft.Boogie.Simplify cancelEvent = null;
}
if (thmProver != null) {
- expose (this) {
+ 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)
- {
+ 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 =
+ int num_axioms_pushed =
FeedNewAxiomsDecls2Prover();
-
- string! prelude = ctx.GetProverCommands(false);
+
+ string prelude = ctx.GetProverCommands(false);
+ Contract.Assert(prelude != null);
vcString = prelude + vcString;
LogActivity(vcString);
- assert thmProver != null;
+ 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.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) {
@@ -374,9 +423,10 @@ namespace Microsoft.Boogie.Simplify }
}
- public override Outcome CheckOutcome(ErrorHandler! handler)
- throws UnexpectedProverOutputException;
- {
+ public override Outcome CheckOutcome(ErrorHandler handler) {
+ Contract.Requires(handler != null);
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+
if (this.thmProver == null) {
return Outcome.Undetermined;
}
@@ -387,61 +437,62 @@ namespace Microsoft.Boogie.Simplify if (options.ForceLogStatus) {
switch (result) {
- case ProverProcess.ProverOutcome.Valid:
- LogActivity("DBG_WAS_VALID");
- break;
- case ProverProcess.ProverOutcome.NotValid:
- LogActivity("DBG_WAS_INVALID");
- break;
+ 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;
+ 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;
}
}
- assume proverException != null;
+ Contract.Assume(proverException != null);
LogComment("***** Unexpected prover output");
- expose (this) {
+ cce.BeginExpose(this);
+ {
currentProverHasBeenABadBoy = true; // this will cause the next resurrect to restart the prover
}
+ cce.EndExpose();
throw proverException;
}
- protected virtual void ResurrectProver()
- throws UnexpectedProverOutputException;
- {
- expose (this) {
+ 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)
- {
+ 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;
@@ -449,11 +500,13 @@ namespace Microsoft.Boogie.Simplify }
FireUpNewProver();
}
+ cce.EndExpose();
}
-
- protected abstract ProverProcess! CreateProverProcess(string! proverPath);
-
- public void LogBgPush(string! s) {
+
+ protected abstract ProverProcess CreateProverProcess(string proverPath);
+
+ public void LogBgPush(string s) {
+ Contract.Requires(s != null);
LogCommon("(BG_PUSH ");
LogCommon(s);
LogCommon(")");
@@ -462,33 +515,37 @@ namespace Microsoft.Boogie.Simplify public void LogBgPop() {
LogCommon("(BG_POP)");
}
-
+
[NoDefaultContract]
private void FireUpNewProver()
- requires IsExposed;
- requires thmProver == null;
- throws UnexpectedProverOutputException;
{
+ 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')) {
+ foreach (string s in thmProver.OptionComments().Split('\n')) {Contract.Assert(s != null);
LogCommonComment(s);
}
- foreach (string! parmsetting in thmProver.ParameterSettings) {
+ foreach (string parmsetting in thmProver.ParameterSettings) {Contract.Assert(parmsetting != null);
LogCommon(parmsetting);
}
}
- foreach (string! parmsetting in thmProver.ParameterSettings) {
+ foreach (string parmsetting in thmProver.ParameterSettings) {Contract.Assert(parmsetting != null);
thmProver.Feed(parmsetting, 0);
}
thmProver.Feed(GetBackgroundPredicate(BackgroundPredFilename), 3);
- string! incProverCommands = ctx.GetProverCommands(false);
- string! proverCommands = ctx.GetProverCommands(true);
- string! prelude = ctx.GetProverCommands(false);
+ string incProverCommands = ctx.GetProverCommands(false);
+ Contract.Assert(incProverCommands != null);
+ string proverCommands = ctx.GetProverCommands(true);
+ Contract.Assert(proverCommands != null);
+ string prelude = ctx.GetProverCommands(false);
+ Contract.Assert(prelude != null);
if (restarts == 0) {
// log the stuff before feeding it into the prover, so when it dies
@@ -497,10 +554,10 @@ namespace Microsoft.Boogie.Simplify LogCommon(prelude);
LogCommon(proverCommands);
- foreach (string! s in vcExprTranslator.AllTypeDecls)
- LogCommon(s);
- foreach (string! s in vcExprTranslator.AllAxioms)
- LogBgPush(s);
+ 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.");
} else {
@@ -510,38 +567,62 @@ namespace Microsoft.Boogie.Simplify thmProver.Feed(prelude, 0);
thmProver.Feed(proverCommands, 0);
- foreach (string! s in vcExprTranslator.AllTypeDecls)
- thmProver.Feed(s, 0);
- foreach (string! s in vcExprTranslator.AllAxioms)
- thmProver.AddAxioms(s);
+ 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
+ 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 { return this.ctx; }
+ public override ProverContext Context {
+ get {
+ Contract.Ensures(Contract.Result<ProverContext>() != null);
+ return this.ctx;
+ }
}
}
-
- public class SimplifyTheoremProver : ProcessTheoremProver
- {
+ [ContractClassFor(typeof(ProcessTheoremProver))]
+ public 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 SimplifyTheoremProver(ProverOptions! options, VCExpressionGenerator! gen, DeclFreeProverContext! ctx)
- throws UnexpectedProverOutputException;
- {
- base(options, gen, ctx, "simplify.exe", "UnivBackPred2.sx");
+ 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) {
+
+ 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) {
+ protected override AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions opts) {
+ Contract.Requires(opts!=null);
+ Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);
+
return new SimplifyVCExprTranslator(gen);
}
}
@@ -552,51 +633,70 @@ namespace Microsoft.Boogie.Simplify public abstract class AxiomVCExprTranslator : VCExprTranslator {
protected AxiomVCExprTranslator() {
- AllAxioms = new List<string!> ();
- NewAxiomsAttr = new List<string!> ();
- AllTypeDecls = new List<string!> ();
- NewTypeDeclsAttr = new List<string!> ();
+ AllAxioms = new List<string> ();
+ NewAxiomsAttr = new List<string> ();
+ AllTypeDecls = new List<string> ();
+ NewTypeDeclsAttr = new List<string> ();
}
- protected AxiomVCExprTranslator(AxiomVCExprTranslator! tl) {
- AllAxioms = new List<string!> (tl.AllAxioms);
- NewAxiomsAttr = new List<string!> (tl.NewAxiomsAttr);
- AllTypeDecls = new List<string!> (tl.AllTypeDecls);
- NewTypeDeclsAttr = new List<string!> (tl.NewTypeDeclsAttr);
+ 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;
+ public readonly List<string/*!>!*/> AllAxioms;
+ private List<string/*!>!*/> NewAxiomsAttr;
// The length of the list NewAxiomsAttr
- public int NewAxiomsCount { get {
- return NewAxiomsAttr.Count;
- } }
+ public int NewAxiomsCount {
+ get {
+ return NewAxiomsAttr.Count;
+ }
+ }
- public List<string!>! NewAxioms { get {
- List<string!>! res = NewAxiomsAttr;
- NewAxiomsAttr = new List<string!> ();
- return res;
- } }
+ 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;
- } }
+ // 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) {
+ public void AddAxiom(string axiom) {
+ Contract.Requires(axiom != null);
AllAxioms.Add(axiom);
NewAxiomsAttr.Add(axiom);
}
- public void AddTypeDecl(string! typeDecl) {
+ public void AddTypeDecl(string typeDecl) {
+ Contract.Requires(typeDecl != null);
AllTypeDecls.Add(typeDecl);
NewTypeDeclsAttr.Add(typeDecl);
}
@@ -607,47 +707,65 @@ namespace Microsoft.Boogie.Simplify // -----------------------------------------------------------------------------------------------
public class SimplifyVCExprTranslator : AxiomVCExprTranslator {
- public SimplifyVCExprTranslator(VCExpressionGenerator! gen) {
+ public SimplifyVCExprTranslator(VCExpressionGenerator gen) {
+ Contract.Requires(gen != null);
Gen = gen;
- TypeAxiomBuilder! axBuilder;
+ TypeAxiomBuilder axBuilder;
switch (CommandLineOptions.Clo.TypeEncodingMethod) {
case CommandLineOptions.TypeEncoding.Arguments:
- axBuilder = new TypeAxiomBuilderArguments (gen);
+ axBuilder = new TypeAxiomBuilderArguments(gen);
break;
default:
- axBuilder = new TypeAxiomBuilderPremisses (gen);
+ axBuilder = new TypeAxiomBuilderPremisses(gen);
break;
}
axBuilder.Setup();
AxBuilder = axBuilder;
- Namer = new UniqueNamer ();
- LitAbstracter = new BigLiteralAbstracter (gen);
+ Namer = new UniqueNamer();
+ LitAbstracter = new BigLiteralAbstracter(gen);
}
- private SimplifyVCExprTranslator(SimplifyVCExprTranslator! tl) {
- base(tl);
+ 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() {
+ 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;
+ 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);
- public override string! Lookup(VCExprVar! var)
- {
return Namer.Lookup(var);
}
-
- public override string! translate(VCExpr! expr, int polarity) {
- Let2ImpliesMutator! letImplier = new Let2ImpliesMutator(Gen);
+
+ 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;
@@ -662,20 +780,27 @@ namespace Microsoft.Boogie.Simplify eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);
break;
}
- VCExpr! exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;
+ VCExpr exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;
+ Contract.Assert(exprWithoutTypes != null);
- TermFormulaFlattener! flattener = new TermFormulaFlattener(Gen);
- VCExpr! exprWithLet = flattener.Flatten(exprWithoutTypes);
- VCExpr! exprWithoutLet = letImplier.Mutate(exprWithLet);
+ 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);
+ VCExpr exprWithoutBigLits = LitAbstracter.Abstract(exprWithoutLet);
+ Contract.Assert(exprWithoutBigLits != null);
AddAxiom(SimplifyLikeExprLineariser.ToSimplifyString(LitAbstracter.GetNewAxioms(),
Namer));
// type axioms
- VCExpr! axiomsWithLet = flattener.Flatten(AxBuilder.GetNewAxioms());
- VCExpr! axiomsWithoutLet = letImplier.Mutate(axiomsWithLet);
+ 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);
@@ -686,36 +811,45 @@ namespace Microsoft.Boogie.Simplify // -----------------------------------------------------------------------------------------------
// -----------------------------------------------------------------------------------------------
- public class Factory : ProverFactory
- {
- public override object! SpawnProver(ProverOptions! options, object! ctxt)
- {
+ 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,
- ((DeclFreeProverContext!)ctxt).ExprGen,
- (DeclFreeProverContext!)ctxt);
+ cce.NonNull((DeclFreeProverContext)ctxt).ExprGen,
+ cce.NonNull((DeclFreeProverContext)ctxt));
}
- public override object! NewProverContext(ProverOptions! options) {
+ 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();
- List<string!>! proverCommands = new List<string!> ();
+ VCExpressionGenerator gen = new VCExpressionGenerator();
+ Contract.Assert(gen != null);
+ List<string>/*!>!*/ proverCommands = new List<string> ();
+ Contract.Assert(cce.NonNullElements(proverCommands));
proverCommands.Add("all");
proverCommands.Add("simplify");
proverCommands.Add("simplifyLike");
return new DeclFreeProverContext(gen, new VCGenerationOptions(proverCommands));
}
- public override CommandLineOptions.VCVariety DefaultVCVariety
- {
- get { return CommandLineOptions.VCVariety.BlockNested; }
+ public override CommandLineOptions.VCVariety DefaultVCVariety {
+ get {
+ return CommandLineOptions.VCVariety.BlockNested;
+ }
}
// needed to make test7 pass
- public override bool SupportsDags
- {
- get { return true; }
+ public override bool SupportsDags {
+ get {
+ return true;
+ }
}
}
}
diff --git a/Source/Provers/Simplify/Simplify.csproj b/Source/Provers/Simplify/Simplify.csproj index c8b416f4..f47fa50f 100644 --- a/Source/Provers/Simplify/Simplify.csproj +++ b/Source/Provers/Simplify/Simplify.csproj @@ -1,139 +1,113 @@ -<?xml version="1.0" encoding="utf-8"?>
-<VisualStudioProject>
- <XEN ProjectType="Local"
- SchemaVersion="1.0"
- Name="Simplify"
- ProjectGuid="f75666de-fb56-457c-8782-09be243450fc"
- >
- <Build>
- <Settings ApplicationIcon=""
- AssemblyName="Provers.Simplify"
- OutputType="Library"
- RootNamespace="Microsoft.Boogie.Simplify"
- StartupObject=""
- StandardLibraryLocation=""
- TargetPlatform="v2"
- TargetPlatformLocation=""
- ShadowedAssembly=""
- NoStandardLibraries="False"
- >
- <Config Name="Debug"
- AllowUnsafeBlocks="False"
- BaseAddress="285212672"
- CheckForOverflowUnderflow="False"
- ConfigurationOverrideFile=""
- DefineConstants="DEBUG;TRACE"
- DocumentationFile=""
- DebugSymbols="True"
- FileAlignment="4096"
- IncrementalBuild="True"
- Optimize="False"
- OutputPath="bin\debug"
- RegisterForComInterop="False"
- RemoveIntegerChecks="false"
- TreatWarningsAsErrors="False"
- WarningLevel="4"
- ReferenceTypesAreNonNullByDefault="False"
- RunProgramVerifier="False"
- RunProgramVerifierWhileEditing="False"
- ProgramVerifierCommandLineOptions=""
- AllowPointersToManagedStructures="False"
- CheckContractAdmissibility="True"
- CheckPurity="False"
- />
- <Config Name="Release"
- AllowUnsafeBlocks="false"
- BaseAddress="285212672"
- CheckForOverflowUnderflow="false"
- ConfigurationOverrideFile=""
- DefineConstants="TRACE"
- DocumentationFile=""
- DebugSymbols="false"
- FileAlignment="4096"
- IncrementalBuild="false"
- Optimize="true"
- OutputPath="bin\release"
- RegisterForComInterop="false"
- RemoveIntegerChecks="false"
- TreatWarningsAsErrors="false"
- WarningLevel="4"
- />
- </Settings>
- <References>
- <Reference Name="System"
- AssemblyName="System"
- Private="false"
- />
- <Reference Name="System.Data"
- AssemblyName="System.Data"
- Private="false"
- />
- <Reference Name="System.Xml"
- AssemblyName="System.Xml"
- Private="false"
- />
- <Reference Name="Core"
- Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"
- Private="true"
- />
- <Reference Name="AIFramework"
- Project="{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"
- Private="true"
- />
- <Reference Name="Graph"
- Project="{4C28FB90-630E-4B55-A937-11A011B79765}"
- Private="true"
- />
- <Reference Name="Mscorlib.Contracts"
- AssemblyName="Mscorlib.Contracts"
- Private="false"
- HintPath="../../../Binaries/Mscorlib.Contracts.dll"
- />
- <Reference Name="System.Contracts"
- AssemblyName="System.Contracts"
- Private="false"
- HintPath="../../../Binaries/System.Contracts.dll"
- />
- <Reference Name="VCGeneration"
- Project="{F65666DE-FB56-457C-8782-09BE243450FC}"
- Private="true"
- />
- <Reference Name="Basetypes"
- Project="{0C692837-77EC-415F-BF04-395E3ED06E9A}"
- Private="true"
- />
- <Reference Name="VCExpr"
- Project="{CF42B700-10AA-4DA9-8992-48A800251C11}"
- Private="true"
- />
- </References>
- </Build>
- <Files>
- <Include>
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="Prover.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="ProverInterface.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="..\..\version.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="Let2ImpliesVisitor.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="AssemblyInfo.ssc"
- />
- </Include>
- </Files>
- <Target Name="AfterBuild"
- >
- </Target>
- </XEN>
-</VisualStudioProject>
\ No newline at end of file +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="3.5" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <ProductVersion>9.0.30729</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>v3.5</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <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>/ignore:CC1002</CodeContractsExtraRewriteOptions>
+ <CodeContractsExtraAnalysisOptions>
+ </CodeContractsExtraAnalysisOptions>
+ <CodeContractsBaseLineFile>
+ </CodeContractsBaseLineFile>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
+ </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>
+ <ItemGroup>
+ <Reference Include="AIFramework, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\Binaries\AIFramework.dll</HintPath>
+ </Reference>
+ <Reference Include="Basetypes, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\Binaries\Basetypes.dll</HintPath>
+ </Reference>
+ <Reference Include="Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\Binaries\Core.dll</HintPath>
+ </Reference>
+ <Reference Include="Graph, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\Binaries\Graph.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL" />
+ <Reference Include="System" />
+ <Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\Binaries\System.Compiler.Runtime.dll</HintPath>
+ </Reference>
+ <Reference Include="System.Data" />
+ <Reference Include="System.Xml" />
+ <Reference Include="VCExpr, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\Binaries\VCExpr.dll</HintPath>
+ </Reference>
+ <Reference Include="VCGeneration, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\Binaries\VCGeneration.dll</HintPath>
+ </Reference>
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="cce.cs" />
+ <Compile Include="Let2ImpliesVisitor.cs" />
+ <Compile Include="Prover.cs" />
+ <Compile Include="ProverInterface.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <Folder Include="Properties\" />
+ </ItemGroup>
+ <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+ <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
+ Other similar extension points exist, see Microsoft.Common.targets.
+ <Target Name="BeforeBuild">
+ </Target>
+ <Target Name="AfterBuild">
+ </Target>
+ -->
+</Project>
\ No newline at end of file |