diff options
| -rw-r--r-- | Source/Boogie.sln | 26 | ||||
| -rw-r--r-- | Source/Provers/Z3/Inspector.cs | 63 | ||||
| -rw-r--r-- | Source/Provers/Z3/Prover.cs | 509 | ||||
| -rw-r--r-- | Source/Provers/Z3/ProverInterface.cs | 207 | ||||
| -rw-r--r-- | Source/Provers/Z3/TypeDeclCollector.cs | 155 | ||||
| -rw-r--r-- | Source/Provers/Z3/Z3.csproj | 269 |
6 files changed, 785 insertions, 444 deletions
diff --git a/Source/Boogie.sln b/Source/Boogie.sln index 85d07466..5ef78532 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -5,8 +5,6 @@ Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Provers", "Provers", "{B758 EndProject
Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "Simplify", "Provers\Simplify\Simplify.sscproj", "{F75666DE-FB56-457C-8782-09BE243450FC}"
EndProject
-Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "Z3", "Provers\Z3\Z3.sscproj", "{F75666DE-CD56-457C-8782-09BE243450FC}"
-EndProject
Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "SMTLib", "Provers\SMTLib\SMTLib.sscproj", "{13C3A68C-462A-4CDA-A480-738046E37C5A}"
EndProject
Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "AIFramework", "AIFramework\AIFramework.sscproj", "{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"
@@ -27,6 +25,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Isabelle", "Provers\Isabell EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbsInt", "AbsInt\AbsInt.csproj", "{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}"
EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Z3", "Provers\Z3\Z3.csproj", "{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}"
+EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Debug|.NET = Debug|.NET
@@ -47,16 +47,6 @@ Global {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
- {F75666DE-CD56-457C-8782-09BE243450FC}.Debug|.NET.ActiveCfg = Debug|.NET
- {F75666DE-CD56-457C-8782-09BE243450FC}.Debug|.NET.Build.0 = Debug|.NET
- {F75666DE-CD56-457C-8782-09BE243450FC}.Debug|Any CPU.ActiveCfg = Debug|.NET
- {F75666DE-CD56-457C-8782-09BE243450FC}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET
- {F75666DE-CD56-457C-8782-09BE243450FC}.Debug|Mixed Platforms.Build.0 = Debug|.NET
- {F75666DE-CD56-457C-8782-09BE243450FC}.Release|.NET.ActiveCfg = Release|.NET
- {F75666DE-CD56-457C-8782-09BE243450FC}.Release|.NET.Build.0 = Release|.NET
- {F75666DE-CD56-457C-8782-09BE243450FC}.Release|Any CPU.ActiveCfg = Release|.NET
- {F75666DE-CD56-457C-8782-09BE243450FC}.Release|Mixed Platforms.ActiveCfg = Release|.NET
- {F75666DE-CD56-457C-8782-09BE243450FC}.Release|Mixed Platforms.Build.0 = Release|.NET
{13C3A68C-462A-4CDA-A480-738046E37C5A}.Debug|.NET.ActiveCfg = Debug|.NET
{13C3A68C-462A-4CDA-A480-738046E37C5A}.Debug|.NET.Build.0 = Debug|.NET
{13C3A68C-462A-4CDA-A480-738046E37C5A}.Debug|Any CPU.ActiveCfg = Debug|.NET
@@ -159,14 +149,24 @@ Global {0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Release|Any CPU.Build.0 = Release|Any CPU
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|.NET.ActiveCfg = Release|Any CPU
+ {BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|Any CPU.Build.0 = Release|Any CPU
+ {BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.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}
- {F75666DE-CD56-457C-8782-09BE243450FC} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
{13C3A68C-462A-4CDA-A480-738046E37C5A} = {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}
EndGlobalSection
EndGlobal
diff --git a/Source/Provers/Z3/Inspector.cs b/Source/Provers/Z3/Inspector.cs index fa1b844e..90284358 100644 --- a/Source/Provers/Z3/Inspector.cs +++ b/Source/Provers/Z3/Inspector.cs @@ -8,8 +8,8 @@ using System.IO; using System.Diagnostics;
using System.Collections;
using System.Collections.Generic;
-using util;
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
+//using util;
using Microsoft.Boogie;
using Microsoft.Boogie.Simplify;
using Microsoft.Basetypes;
@@ -18,15 +18,25 @@ using Microsoft.Boogie.VCExprAST; namespace Microsoft.Boogie.Z3
{
internal class FindLabelsVisitor : TraversingVCExprVisitor<bool, bool> {
- public Dictionary<string!,bool>! Labels = new Dictionary<string!,bool>();
+ public Dictionary<string/*!*/,bool>/*!*/ Labels = new Dictionary<string/*!*/,bool>();
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(Labels!=null&&cce.NonNullElements(Labels.Keys));
+}
+
+
+ public static Dictionary<string/*!*/,bool>/*!*/ FindLabels(VCExpr/*!*/ expr) {
+ Contract.Requires(expr != null);
+ Contract.Ensures(Contract.Result<Dictionary<string/*!*/,bool>/*!*/>() != null&&cce.NonNullElements(Contract.Result<Dictionary<string/*!*/,bool>/*!*/>().Keys));
- public static Dictionary<string!,bool>! FindLabels(VCExpr! expr) {
- FindLabelsVisitor! visitor = new FindLabelsVisitor();
+ FindLabelsVisitor visitor = new FindLabelsVisitor();
visitor.Traverse(expr, true);
return visitor.Labels;
}
- protected override bool StandardResult(VCExpr! node, bool arg) {
+ 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;
@@ -39,13 +49,23 @@ namespace Microsoft.Boogie.Z3 }
internal class Inspector {
- [Rep] protected readonly Process! inspector;
- [Rep] readonly TextReader! fromInspector;
- [Rep] readonly TextWriter! toInspector;
+ [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)
+ public Inspector(Z3InstanceOptions opts)
{
- ProcessStartInfo! psi = new ProcessStartInfo(opts.Inspector);
+ Contract.Requires(opts != null);
+ ProcessStartInfo psi = new ProcessStartInfo(opts.Inspector);
+ Contract.Assert(psi!=null);
psi.CreateNoWindow = true;
psi.UseShellExecute = false;
psi.RedirectStandardInput = true;
@@ -69,14 +89,20 @@ namespace Microsoft.Boogie.Z3 {
}
- public void NewProblem(string! descriptiveName, VCExpr! vc, ProverInterface.ErrorHandler! handler)
+ public void NewProblem(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler)
{
- Dictionary<string!,bool>! labels = FindLabelsVisitor.FindLabels(vc);
+ Contract.Requires(descriptiveName != null);
+ Contract.Requires(vc != null);
+ Contract.Requires(handler != null);
+ Dictionary<string/*!*/,bool>/*!*/ labels = FindLabelsVisitor.FindLabels(vc);
+ Contract.Assert(labels!=null);
toInspector.WriteLine("PROBLEM " + descriptiveName);
toInspector.WriteLine("TOKEN BEGIN");
- foreach (string! lab in labels.Keys) {
- string! no = lab.Substring(1);
- Absy! absy = handler.Label2Absy(no);
+ foreach (string lab in labels.Keys) {
+ 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;
@@ -99,7 +125,7 @@ namespace Microsoft.Boogie.Z3 toInspector.Write("BLOCK ");
toInspector.Write(blk.Label);
} else {
- assume false;
+ Contract.Assume( false);
}
if (val == null || val == "assert" || val == "ensures") { val = ""; }
@@ -127,8 +153,9 @@ namespace Microsoft.Boogie.Z3 toInspector.WriteLine("TOKEN END");
}
- public void StatsLine(string! line)
+ 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 index dbf23a8a..14b551df 100644 --- a/Source/Provers/Z3/Prover.cs +++ b/Source/Provers/Z3/Prover.cs @@ -8,9 +8,9 @@ using System.IO; using System.Diagnostics;
using System.Collections;
using System.Collections.Generic;
+using System.Diagnostics.Contracts;
using System.Text;
-using util;
-using Microsoft.Contracts;
+//using util;
using Microsoft.Boogie;
using Microsoft.Boogie.Simplify;
using Microsoft.Basetypes;
@@ -19,32 +19,178 @@ using Microsoft.Basetypes; namespace Microsoft.Boogie.Z3
{
internal class Z3ProverProcess : ProverProcess {
- [Peer] private Z3InstanceOptions! opts;
- [Peer] private readonly Inspector? inspector;
+ [Peer] private Z3InstanceOptions opts;
+ [Peer] private readonly Inspector/*?*/ inspector;
private readonly bool expectingModel = false;
- private string! cmdLineArgs = "";
+ private string cmdLineArgs = "";
+
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(cmdLineArgs!=null);
+ Contract.Invariant(opts != null);
+ Contract.Invariant(cce.NonNullElements(parameterSettings));
+ }
+
+
class OptionValue {
- public readonly string! Option;
- public readonly string! Value;
- public OptionValue(string! option, string! value) { Option = option; Value = value; }
+ 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.*;
+ 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);
- Owner.AssignSame(ov, Owner.ElementProxy(parms));
+ cce.Owner.AssignSame(ov, cce.Owner.ElementProxy(parms));
parms.Add(ov);
}
- private List<OptionValue!>! parameterSettings;
- // [NotDelayed]
+ private List<OptionValue/*!>!*/> parameterSettings;
+
+ //[NotDelayed]
[Captured]
- public Z3ProverProcess(Z3InstanceOptions! opts, Inspector? inspector)
- requires inspector != null ==> Owner.Same(opts, inspector);
+ public Z3ProverProcess(Z3InstanceOptions opts, Inspector inspector)
+ : base(ComputeProcessStartInfo(opts), opts.ExeName)
{ // throws ProverException
- string! z3args = OptionChar() + "si";
- List<OptionValue!> parms = new List<OptionValue!>();
+ Contract.Requires(opts != null);
+ Contract.Requires(inspector == null || cce.Owner.Same(opts, inspector));
+ string z3args = OptionChar() + "si";
+ List<OptionValue/*!*/> parms = new List<OptionValue/*!*/>();
+
+ if (opts.V2) {
+ AddOption(parms, "MODEL_PARTIAL", "true");
+ AddOption(parms, "MODEL_VALUE_COMPLETION", "false");
+ AddOption(parms, "MODEL_HIDE_UNUSED_PARTITIONS", "false");
+ AddOption(parms, "MODEL_V1", "true");
+ AddOption(parms, "ASYNC_COMMANDS", "false");
+ } else {
+ AddOption(parms, "PARTIAL_MODELS", "true");
+ AddOption(parms, "MODEL_VALUE_COMPLETION", "false");
+ AddOption(parms, "HIDE_UNUSED_PARTITIONS", "false");
+ }
+
+ if (opts.V2) {
+ // 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(parms, "PHASE_SELECTION", "0");
+ AddOption(parms, "RESTART_STRATEGY", "0");
+ AddOption(parms, "RESTART_FACTOR", "|1.5|");
+
+ // 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(parms, "NNF_SK_HACK", "true");
+
+ // More or less like MAM=0.
+ AddOption(parms, "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(parms, "QI_COST", "|\"(+ weight generation)\"|");
+
+ // Make the integer model more diverse by default, speeds up some benchmarks a lot.
+ AddOption(parms, "ARITH_RANDOM_INITIAL_VALUE", "true");
+
+ // The left-to-right structural case-splitting strategy.
+ AddOption(parms, "SORT_AND_OR", "false");
+ AddOption(parms, "CASE_SPLIT", "3");
+
+ // In addition delay adding unit conflicts.
+ AddOption(parms, "DELAY_UNITS", "true");
+ AddOption(parms, "DELAY_UNITS_THRESHOLD", "16");
+
+ if (opts.Inspector != null) {
+ AddOption(parms, "PROGRESS_SAMPLING_FREQ", "100");
+ }
+ } else {
+ z3args += " " + OptionChar() + "mam:" + CommandLineOptions.Clo.Z3mam;
+ }
+
+ if (CommandLineOptions.Clo.z3AtFlag) {
+ z3args += " " + OptionChar() + "@ ";
+ }
+ if (0 <= CommandLineOptions.Clo.ProverCCLimit) {
+ z3args += " " + OptionChar() + "cex:" + CommandLineOptions.Clo.ProverCCLimit;
+ }
+ if (0 <= opts.Timeout) {
+ z3args += " " + OptionChar() + "t:" + opts.Timeout;
+ }
+ if (opts.Typed) {
+ AddOption(parms, "TYPE_CHECK", "true");
+ if (opts.BitVectors == CommandLineOptions.BvHandling.Z3Native) {
+ if (opts.V2) {
+ AddOption(parms, "BV_REFLECT", "true");
+ } else {
+ AddOption(parms, "REFLECT_BV_OPS", "true");
+ }
+ }
+ }
+ if (CommandLineOptions.Clo.PrintErrorModel >= 1 ||
+ CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||
+ CommandLineOptions.Clo.ContractInfer ||
+ CommandLineOptions.Clo.LazyInlining > 0 ||
+ CommandLineOptions.Clo.StratifiedInlining > 0) {
+ z3args += " " + OptionChar() + "m";
+ expectingModel = true;
+ }
+ if (CommandLineOptions.Clo.LazyInlining == 2) {
+ z3args += " " + OptionChar() + "nw";
+ AddOption(parms, "MACRO_EXPANSION", "true");
+ }
+
+ // Z3 version 1.3 does not support SETPARAMETER in the input, so we tack on the OPTION=value pairs to z3args
+ if (opts.V1) {
+ foreach (OptionValue opt in parms) {
+ z3args += string.Format(" \"{0}={1}\"", opt.Option, opt.Value);
+ }
+ }
+
+ 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(parms, opt.Substring(0, eq), opt.Substring(eq + 1));
+ }
+ z3args += " \"" + opt + "\"";
+ }
+
+
+ cmdLineArgs = z3args;
+ parameterSettings = parms;
+
+ // ProcessStartInfo psi = new ProcessStartInfo(opts.ExeName, z3args);
+ // Contract.Assert(psi!=null);
+ // psi.CreateNoWindow = true;
+ // psi.UseShellExecute = false;
+ // psi.RedirectStandardInput = true;
+ // psi.RedirectStandardOutput = true;
+ // psi.RedirectStandardError = true;
+
+ //base(psi, opts.ExeName);
+
+ cce.Owner.AssignSame(this, opts);
+ this.opts = opts;
+ this.inspector = inspector;
+ }
+
+ private static ProcessStartInfo ComputeProcessStartInfo(Z3InstanceOptions opts) {
+ string z3args = OptionChar() + "si";
+ List<OptionValue/*!*/> parms = new List<OptionValue/*!*/>();
if (opts.V2) {
AddOption(parms, "MODEL_PARTIAL", "true");
@@ -72,7 +218,7 @@ namespace Microsoft.Boogie.Z3 // More or less like MAM=0.
AddOption(parms, "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(parms, "QI_COST", "|\"(+ weight generation)\"|");
@@ -93,10 +239,10 @@ namespace Microsoft.Boogie.Z3 } else {
z3args += " " + OptionChar() + "mam:" + CommandLineOptions.Clo.Z3mam;
}
-
+
if (CommandLineOptions.Clo.z3AtFlag) {
- z3args += " " + OptionChar() + "@ ";
- }
+ z3args += " " + OptionChar() + "@ ";
+ }
if (0 <= CommandLineOptions.Clo.ProverCCLimit) {
z3args += " " + OptionChar() + "cex:" + CommandLineOptions.Clo.ProverCCLimit;
}
@@ -113,27 +259,28 @@ namespace Microsoft.Boogie.Z3 }
}
}
- if (CommandLineOptions.Clo.PrintErrorModel >= 1 ||
- CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||
+ if (CommandLineOptions.Clo.PrintErrorModel >= 1 ||
+ CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||
CommandLineOptions.Clo.ContractInfer ||
CommandLineOptions.Clo.LazyInlining > 0 ||
CommandLineOptions.Clo.StratifiedInlining > 0) {
z3args += " " + OptionChar() + "m";
- expectingModel = true;
+ //expectingModel = true;
}
if (CommandLineOptions.Clo.LazyInlining == 2) {
z3args += " " + OptionChar() + "nw";
AddOption(parms, "MACRO_EXPANSION", "true");
}
-
+
// Z3 version 1.3 does not support SETPARAMETER in the input, so we tack on the OPTION=value pairs to z3args
if (opts.V1) {
foreach (OptionValue opt in parms) {
z3args += string.Format(" \"{0}={1}\"", opt.Option, opt.Value);
}
}
-
- foreach (string! opt in CommandLineOptions.Clo.Z3Options) {
+
+ 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
@@ -145,40 +292,42 @@ namespace Microsoft.Boogie.Z3 z3args += " \"" + opt + "\"";
}
-
- cmdLineArgs = z3args;
- parameterSettings = parms;
-
- ProcessStartInfo! psi = new ProcessStartInfo(opts.ExeName, z3args);
+
+ //cmdLineArgs = z3args;
+ //parameterSettings = parms;
+
+ ProcessStartInfo psi = new ProcessStartInfo(opts.ExeName, z3args);
+ Contract.Assert(psi != null);
psi.CreateNoWindow = true;
psi.UseShellExecute = false;
psi.RedirectStandardInput = true;
psi.RedirectStandardOutput = true;
psi.RedirectStandardError = true;
-
- base(psi, opts.ExeName);
- Owner.AssignSame(this, opts);
- this.opts = opts;
- this.inspector = inspector;
+ return psi;
}
- public override string! OptionComments()
+ 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, cmdLineArgs);
- assume CommandLineOptions.Clo.IsPeerConsistent;
- foreach (string! opt in CommandLineOptions.Clo.Z3Options) {
+ 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 {
+ //[Pure(false)]
+ public override IEnumerable<string/*!>!*/> ParameterSettings {
get {
+ Contract.Ensures(cce.NonNullElements( Contract.Result<IEnumerable<string>>()));
+
if (opts.V2) {
foreach (OptionValue opt in parameterSettings) {
yield return "(SETPARAMETER " + opt.Option + " " + opt.Value + ")";
@@ -188,8 +337,10 @@ namespace Microsoft.Boogie.Z3 }
// z3 uses different magic characters for options on linux/unix and on windows
- private static string! OptionChar() {
- assume Environment.OSVersion != null;
+ private static string OptionChar() {
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ Contract.Assume( Environment.OSVersion != null);
switch (Environment.OSVersion.Platform) {
case PlatformID.Unix:
return "-";
@@ -198,8 +349,10 @@ namespace Microsoft.Boogie.Z3 }
}
- protected override void DoBeginCheck(string! descriptiveName, string! formula)
+ 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();
@@ -213,15 +366,17 @@ namespace Microsoft.Boogie.Z3 return FromReadChar();
}
- private void Trace(string! msg)
+ private void Trace(string msg)
{
+ Contract.Requires(msg != null);
Console.WriteLine("Z3: " + msg);
}
- public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler! handler)
- throws UnexpectedProverOutputException;
+ public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler handler)
{
- ProverOutcome outcome;
+ Contract.Requires(handler != null);
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ //ProverOutcome outcome;
bool isInvalid = false;
if (this.simplify == null) {
@@ -269,8 +424,8 @@ namespace Microsoft.Boogie.Z3 int beg = 0;
while (beg < line.Length && '0' <= line[beg] && line[beg] <= '9')
- invariant beg <= line.Length;
{
+ cce.LoopInvariant(beg <= line.Length);
beg++;
}
@@ -306,7 +461,8 @@ namespace Microsoft.Boogie.Z3 }
if (isInvalid && line.StartsWith("labels: (")) {
- List<string!>! l = ParseLabels(line);
+ List<string/*!*/>/*!*/ l = ParseLabels(line);
+ Contract.Assert(cce.NonNullElements(l));
Z3ErrorModel errModel = null;
if (expectingModel) {
if (opts.Verbosity > 2) {
@@ -319,7 +475,7 @@ namespace Microsoft.Boogie.Z3 Trace("model parsed, final line " + line);
}
// Z3 always ends the model with END_OF_MODEL, not with labels: or .
- assume line == "END_OF_MODEL";
+ Contract.Assume( line == "END_OF_MODEL");
} else {
throw new UnexpectedProverOutputException(string.Format("evil input from z3 (expecting partitions): '{0}'", line));
}
@@ -356,23 +512,25 @@ namespace Microsoft.Boogie.Z3 MAPLET ::= ZID* "->" ZID
-----------------------------------------------------------------------------*/
- private string! ParseModel(out Z3ErrorModel errModel)
- modifies this.*;
- ensures result == "." || result.StartsWith("labels: (") || result == "END_OF_MODEL";
- throws UnexpectedProverOutputException;
+ private string ParseModel(out Z3ErrorModel errModel)
+ //TODO: 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);
+
//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>();
+ 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!>>();
+ 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>();
- Owner.AssignSame(Owner.ElementProxy(partitionToValue), Owner.ElementProxy(valueToPartition));
+ cce.Owner.AssignSame(cce.Owner.ElementProxy(partitionToValue), cce.Owner.ElementProxy(valueToPartition));
int ch;
@@ -387,8 +545,8 @@ namespace Microsoft.Boogie.Z3 }// end MAPPING
// add the fake partition for the 'else -> #undefined' clause
- List<string!> emptyList = new List<string!>();
- Owner.AssignSame(emptyList, Owner.ElementProxy(partitionToIdentifiers));
+ List<string/*!*/> emptyList = new List<string/*!*/>();
+ cce.Owner.AssignSame(emptyList, cce.Owner.ElementProxy(partitionToIdentifiers));
partitionToIdentifiers.Add(emptyList);
partitionToValue.Add(null);
@@ -397,13 +555,17 @@ namespace Microsoft.Boogie.Z3 }
private void ParseModelMapping(int zID,
- Dictionary<string!, int>! identifierToPartition,
- List<List<string!>>! partitionToIdentifiers,
- List<Object>! partitionToValue,
- Dictionary<Object, int>! valueToPartition)
- requires Owner.Same(Owner.ElementProxy(partitionToValue), Owner.ElementProxy(valueToPartition));
- modifies this.*, identifierToPartition.*, partitionToIdentifiers.*, partitionToValue.*, valueToPartition.*;
+ Dictionary<string/*!*/, int>/*!*/ identifierToPartition,
+ List<List<string/*!*/>>/*!*/ partitionToIdentifiers,
+ List<Object>/*!*/ partitionToValue,
+ Dictionary<Object, int>/*!*/ valueToPartition)
+ //TODO: modifies this.*, identifierToPartition.*, partitionToIdentifiers.*, partitionToValue.*, valueToPartition.*;
{
+ Contract.Requires(partitionToValue != null);
+ Contract.Requires(valueToPartition != null);
+ Contract.Requires(cce.NonNullElements(identifierToPartition));
+ Contract.Requires(cce.NonNullElements(partitionToIdentifiers));
+ Contract.Requires(cce.Owner.Same(cce.Owner.ElementProxy(partitionToValue), cce.Owner.ElementProxy(valueToPartition)));
string s = FromReadLine();
{
// sanity check
@@ -415,7 +577,7 @@ namespace Microsoft.Boogie.Z3 }
if (! (int.TryParse(n, out k) && zID == k)) {
System.Console.WriteLine("mismatch: {0}!={1} '{2}'", zID, k, s);
- assume false;
+ Contract.Assume( false);
}
}
@@ -425,13 +587,13 @@ namespace Microsoft.Boogie.Z3 if (0 <= j) {
j += 4;
}
- assume j == -1 || j < s.Length; // if ' -> ' is present, then more should remain of the line
+ 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) {
- assume !valueToPartition.ContainsKey("nullObject"); // a RHS value should occur only once in the Z3 output
+ 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
@@ -442,20 +604,21 @@ namespace Microsoft.Boogie.Z3 } else if (s[j] == 't'/*rue*/) {
partitionToValue.Add(true);
object boxedTrue = true;
- assume !valueToPartition.ContainsKey(boxedTrue); // a RHS value should occur only once in the Z3 output
+ 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;
- Owner.AssignSame(boxedFalse, Owner.ElementProxy(partitionToValue));
+ cce.Owner.AssignSame(boxedFalse, cce.Owner.ElementProxy(partitionToValue));
partitionToValue.Add(boxedFalse);
- assume !valueToPartition.ContainsKey(boxedFalse); // a RHS value should occur only once in the Z3 output
+ 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>!>();
+ List<List<int>/*!*/> arrayModel = new List<List<int>/*!*/>();
+ Contract.Assert(Contract.ForAll(arrayModel,a=>cce.NonNullElements(a)));
string array = s.Substring(j+1);
int index1, index2;
string from, to;
@@ -474,7 +637,7 @@ namespace Microsoft.Boogie.Z3 arrayModel.Add(tuple);
tuple = new List<int>();
}
- assert array.StartsWith("else ->");
+ Contract.Assert(array.StartsWith("else ->"));
index1 = array.IndexOf('*') + 1;
index2 = array.IndexOf('}');
to = array.Substring(index1, index2-index1);
@@ -508,80 +671,90 @@ namespace Microsoft.Boogie.Z3 if (type == "int") {
object boxedN = BigNum.FromString(number);
- assume Owner.None(boxedN);
- Owner.AssignSame(boxedN, Owner.ElementProxy(partitionToValue));
+ Contract.Assume( cce.Owner.None(boxedN));
+ cce.Owner.AssignSame(boxedN, cce.Owner.ElementProxy(partitionToValue));
partitionToValue.Add(boxedN);
- assume !valueToPartition.ContainsKey(boxedN); // a RHS value should occur only once in the Z3 output
+ 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);
- Owner.AssignSame(bitV, Owner.ElementProxy(partitionToValue));
+ cce.Owner.AssignSame(bitV, cce.Owner.ElementProxy(partitionToValue));
partitionToValue.Add(bitV);
- assume !valueToPartition.ContainsKey(bitV); // a RHS value should occur only once in the Z3 output
+ 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);
- assume false;
+ Contract.Assume( false);
}
}
}
- private static int ParseModelZidAndIdentifiers(int zID, string! s,
- Dictionary<string!, int>! identifierToPartition,
- List<List<string!>>! partitionToIdentifiers)
- modifies identifierToPartition.*, partitionToIdentifiers.*;
- ensures 0 <= result && result <= s.Length;
+ private static int ParseModelZidAndIdentifiers(int zID, string s,
+ Dictionary<string/*!*/, int>/*!*/ identifierToPartition,
+ List<List<string/*!*/>>/*!*/ partitionToIdentifiers)
+ //TODO: modifies identifierToPartition.*, partitionToIdentifiers.*;
+ //TODO: Find all modifies statements
{
- List<string!> identifiers = new List<string!>();
+ 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('>');
- assert 0 < arrowIndex;
+ 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.
- assume j < s.Length; // there should be more characters; the ending '}', for one
+ Contract.Assume( j < s.Length); // there should be more characters; the ending '}', for one
//ID*
while (true)
- invariant identifiers.IsPeerConsistent && identifierToPartition.IsPeerConsistent && partitionToIdentifiers.IsPeerConsistent;
- invariant 0 <= j && j < s.Length;
- {
+ {Contract.Invariant(cce.IsPeerConsistent( identifiers) && cce.IsPeerConsistent(identifierToPartition) && cce.IsPeerConsistent(partitionToIdentifiers));
+ Contract.Invariant(0 <= j && j < s.Length);
int k = s.IndexOfAny(new char[]{' ', '}'}, j);
- assume j <= k;
+ Contract.Assume( j <= k);
string id = s.Substring(j, k-j);
j = k+1;
- assume !identifierToPartition.ContainsKey(id); // an ID is listed only once in this list, and an ID can only belong to one ZID equivalence class
+ 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;
}
- assume j < s.Length; // there should be more characters; the ending '}', for one
+ Contract.Assume( j < s.Length); // there should be more characters; the ending '}', for one
}//end ID*
} else {
j = 0;
}
- Owner.AssignSame(identifiers, Owner.ElementProxy(partitionToIdentifiers));
+ 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
+ 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.*;
- ensures result == "." || result.StartsWith("labels: (") || result == "END_OF_MODEL";
- throws UnexpectedProverOutputException;
+ //TODO: 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>>!>();
+ 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>>();
@@ -601,7 +774,7 @@ namespace Microsoft.Boogie.Z3 return s;
}
int j = s.IndexOf(' ', 0);
- assume 0 <= j;
+ 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.
@@ -635,11 +808,11 @@ namespace Microsoft.Boogie.Z3 //ZID*
while(true)
- invariant 0 <= j && j <= s.Length;
- {
+ {Contract.Invariant( 0 <= j && j <= s.Length);
+
j = s.IndexOfAny(new Char[]{'*', '-'}, j);
// true because this always ends with a "->":
- assume 0 <= j;
+ Contract.Assume( 0 <= j);
// reading -> means end of ZID*
if (s[j] == '-'/*>*/) break;
@@ -647,10 +820,10 @@ namespace Microsoft.Boogie.Z3 // start reading the ZID* with the number, not the *
j = j + 1;
// by input string format:
- assume j < s.Length;
+ Contract.Assume( j < s.Length);
int k = s.IndexOf(' ', j);
// by input string format:
- assume j <= k;
+ Contract.Assume( j <= k);
zIDstring = s.Substring(j, k-j);
// add the arguments
argumentsAndResult.Add(int.Parse(zIDstring));
@@ -660,7 +833,7 @@ namespace Microsoft.Boogie.Z3 // j is the beginning of "-> *", we want the first character after this
j = j + 4;
// by input string format:
- assume j <= s.Length;
+ Contract.Assume( j <= s.Length);
zIDstring = s.Substring(j);
// add the result
argumentsAndResult.Add(int.Parse(zIDstring));
@@ -670,12 +843,12 @@ namespace Microsoft.Boogie.Z3 // this is the 'else -> #unspecified' case
// by input string format:
- assume s.IndexOf("#unspec") >= 0;
+ 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
- Owner.AssignSame(argumentsAndResult, Owner.ElementProxy(functionDefinition));
+ cce.Owner.AssignSame(argumentsAndResult, cce.Owner.ElementProxy(functionDefinition));
functionDefinition.Add(argumentsAndResult);
/*
@@ -692,7 +865,7 @@ namespace Microsoft.Boogie.Z3 // and therefore added to the map of defined functions, together with the name 'id'
// which had been extracted before
- assume !definedFunctions.ContainsKey(id); // each function name in the model is listed only once
+ Contract.Assume( !definedFunctions.ContainsKey(id)); // each function name in the model is listed only once
definedFunctions.Add(id, functionDefinition);
// read the line with "}"
@@ -707,29 +880,48 @@ namespace Microsoft.Boogie.Z3 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)
+ 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)
{
- this.partitionNames = new string?[partitionToIdentifiers.Count];
- this.prevPartitionNames = new string?[partitionToIdentifiers.Count];
+ 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;
+ 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];
+ partitionNames = new string[len];
for (int pos = 0; pos < len; ++pos)
GetPartitionName(pos);
}
}
- private int NameBadness(string! name)
+ private int NameBadness(string name)
{
+ Contract.Requires(name!=null);
int badness = name.Length;
if (name.StartsWith("call") && name.IndexOf("formal@") > 0)
badness += 1000;
@@ -738,8 +930,10 @@ namespace Microsoft.Boogie.Z3 return badness;
}
- private string! GetPartitionName(int pos)
+ private string GetPartitionName(int pos)
{
+ Contract.Ensures(Contract.Result<string>() != null);
+
string name = partitionNames[pos];
if (name != null) {
return name;
@@ -749,8 +943,9 @@ namespace Microsoft.Boogie.Z3 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];
+ 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];
@@ -759,16 +954,20 @@ namespace Microsoft.Boogie.Z3 if (pti != null && pti.Count > 0) {
// add identifiers
- foreach (string! name in pti)
- possible_names.Add(name);
+ 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) {
- foreach (List<int>! parms in kv.Value) {
+ 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 + "(";
+ string s = kv.Key + "(";
for (int i = 0; i < parms.Count - 1; ++i) {
if (i != 0) s += ", ";
s += GetPartitionName(parms[i]);
@@ -781,25 +980,28 @@ namespace Microsoft.Boogie.Z3 // choose the shortest possible name
if (possible_names.Count > 0) {
- string! best = possible_names[0];
- foreach (string! s in possible_names)
- if (NameBadness(s) < NameBadness(best)) best = s;
+ 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 (!)partitionNames[pos];
+ return cce.NonNull(partitionNames[pos]);
}
- private void PrintReadableModel (TextWriter! writer) {
+ private void PrintReadableModel (TextWriter writer) {
+ Contract.Requires(writer!=null);
writer.WriteLine("Z3 error model: ");
SetNames();
writer.WriteLine("partitions:");
- assert partitionToIdentifiers.Count == partitionToValue.Count;
+ 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];
+ 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 ++) {
@@ -816,12 +1018,14 @@ namespace Microsoft.Boogie.Z3 writer.WriteLine();
writer.WriteLine("function interpretations:");
- List<string!> funNames = new List<string!>(definedFunctions.Keys);
+ List<string> funNames = new List<string>(definedFunctions.Keys);
funNames.Sort();
- foreach (string! name in funNames) {
+ 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]) {
- string! s = name + "(";
+ foreach (List<int> parms in definedFunctions[name]) {
+ Contract.Assert(parms!=null);
+ string s = name + "(";
if (parms.Count == 1) {
continue;
// s += "*";
@@ -832,7 +1036,7 @@ namespace Microsoft.Boogie.Z3 }
}
s += ")";
- string! res = GetPartitionName(parms[parms.Count - 1]);
+ string res = GetPartitionName(parms[parms.Count - 1]);
if (res == s)
res = "*" + parms[parms.Count - 1] + " (SELF)";
writer.WriteLine("{0} = {1}", s, res);
@@ -843,7 +1047,8 @@ namespace Microsoft.Boogie.Z3 writer.WriteLine();
}
- public override void Print (TextWriter! writer) {
+ public override void Print (TextWriter writer) {
+ Contract.Requires(writer!=null);
if (CommandLineOptions.Clo.PrintErrorModel == 4) {
PrintReadableModel(writer);
return;
@@ -852,10 +1057,10 @@ namespace Microsoft.Boogie.Z3 writer.WriteLine("Z3 error model: ");
writer.WriteLine("partitions:");
- assert partitionToIdentifiers.Count == partitionToValue.Count;
+ Contract.Assert(partitionToIdentifiers.Count == partitionToValue.Count);
for (int i = 0; i < partitionToIdentifiers.Count; i++){
writer.Write("*"+i);
- List<string!> pti = partitionToIdentifiers[i];
+ List<string> pti = partitionToIdentifiers[i];
if (pti != null && pti.Count != 0) {
writer.Write(" {");
for (int k = 0; k < pti.Count - 1; k ++) {
@@ -876,15 +1081,15 @@ namespace Microsoft.Boogie.Z3 writer.Write(" -> " + "false" + "");
} else if (tempPTVI is BigNum) {
writer.Write(" -> " + tempPTVI + ":int");
- } else if (tempPTVI is List<List<int>!>) {
- List<List<int>!> array = tempPTVI as List<List<int>!>;
- assume array != null;
+ } else if (tempPTVI is List<List<int>>) {
+ List<List<int>> array = tempPTVI as List<List<int>>;
+ Contract.Assume( array != null);
writer.Write(" -> {");
foreach(List<int> l in array) {
if (l.Count == 2) {
writer.Write("*"+l[0] + " -> " + "*"+l[1] + "; ");
} else {
- assert (l.Count == 1);
+ Contract.Assert((l.Count == 1));
writer.Write("else -> *"+l[0]+"}");
}
}
@@ -898,7 +1103,8 @@ namespace Microsoft.Boogie.Z3 }
writer.WriteLine("function interpretations:");
- foreach (KeyValuePair<string!, List<List<int>>!> kvp in definedFunctions) {
+ foreach (KeyValuePair<string, List<List<int>>> kvp in definedFunctions) {
+ Contract.Assert(kvp.Key!=null);
writer.WriteLine(kvp.Key + " -> {");
List<List<int>> kvpValue = kvp.Value;
if (kvpValue != null) {
@@ -923,7 +1129,8 @@ namespace Microsoft.Boogie.Z3 if (CommandLineOptions.Clo.PrintErrorModel >= 2) {
writer.WriteLine("identifierToPartition:");
- foreach (KeyValuePair<string!, int> kvp in identifierToPartition) {
+ foreach (KeyValuePair<string, int> kvp in identifierToPartition) {
+ Contract.Assert(kvp.Key!=null);
writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);
}
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs index 3473a139..824dabd4 100644 --- a/Source/Provers/Z3/ProverInterface.cs +++ b/Source/Provers/Z3/ProverInterface.cs @@ -4,14 +4,14 @@ //
//-----------------------------------------------------------------------------
using System;
-using System.Collections;
+//using System.Collections;
using System.Collections.Generic;
using System.Threading;
-using System.IO;
+//using System.IO;
using System.Text;
-using ExternalProver;
+//using ExternalProver;
using System.Diagnostics;
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
using Microsoft.Boogie.AbstractInterpretation;
using Microsoft.Boogie;
using Microsoft.Boogie.VCExprAST;
@@ -24,17 +24,25 @@ namespace Microsoft.Boogie.Z3 {
public class Z3ProcessTheoremProver : ProcessTheoremProver
{
- private Z3InstanceOptions! opts;
+ private Z3InstanceOptions opts;
private Inspector inspector;
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(opts!=null);
+}
+
[NotDelayed]
- public Z3ProcessTheoremProver(VCExpressionGenerator! gen,
- DeclFreeProverContext! ctx, Z3InstanceOptions! opts)
- throws UnexpectedProverOutputException;
+ public Z3ProcessTheoremProver(VCExpressionGenerator gen,
+ DeclFreeProverContext ctx, Z3InstanceOptions opts):base(opts, gen, ctx, opts.ExeName,opts.Typed ? "TypedUnivBackPred2.sx" : "UnivBackPred2.sx")
{
+ Contract.Requires(gen != null);
+ Contract.Requires(ctx != null);
+ Contract.Requires(opts != null);
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
this.opts = opts;
- string! backPred = opts.Typed ? "TypedUnivBackPred2.sx" : "UnivBackPred2.sx";
- base(opts, gen, ctx, opts.ExeName, backPred);
+
}
private void FireUpInspector()
@@ -44,7 +52,11 @@ namespace Microsoft.Boogie.Z3 }
}
- protected override Microsoft.Boogie.Simplify.ProverProcess! CreateProverProcess(string! proverPath) {
+ 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) {
@@ -53,12 +65,17 @@ namespace Microsoft.Boogie.Z3 return new Z3ProverProcess(opts, inspector);
}
- protected override AxiomVCExprTranslator! SpawnVCExprTranslator() {
+ protected override AxiomVCExprTranslator SpawnVCExprTranslator() {
+ Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);
+
return new Z3VCExprTranslator(gen, opts);
}
- 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);
FireUpInspector();
if (inspector != null) {
inspector.NewProblem(descriptiveName, vc, handler);
@@ -77,20 +94,27 @@ namespace Microsoft.Boogie.Z3 }
public int Lets {
get
- ensures 0 <= result && result < 4;
- {
+ {
+ Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() < 4);
return CommandLineOptions.Clo.Z3lets;
}
}
public bool V1 = false;
public bool V2 = false; // default set in PostParse
public bool DistZ3 = false;
- public string! ExeName = "z3.exe";
+ public string ExeName = "z3.exe";
public bool InverseImplies = false;
- public string? Inspector = null;
+ public string Inspector = null;
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(ExeName!=null);
+}
+
- protected override bool Parse(string! opt)
+ protected override bool Parse(string opt)
{
+ Contract.Requires(opt!=null);
return ParseBool(opt, "V1", ref V1) ||
ParseBool(opt, "V2", ref V2) ||
ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||
@@ -122,14 +146,23 @@ namespace Microsoft.Boogie.Z3 }
internal class Z3LineariserOptions : LineariserOptions {
- private readonly Z3InstanceOptions! opts;
+ private readonly Z3InstanceOptions opts;
+
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(opts!=null);
+}
+
public override CommandLineOptions.BvHandling Bitvectors { get {
return opts.BitVectors;
} }
- internal Z3LineariserOptions(bool asTerm, Z3InstanceOptions! opts, List<VCExprVar!>! letVariables) {
- base(asTerm);
+ internal 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;
}
@@ -150,7 +183,9 @@ namespace Microsoft.Boogie.Z3 return opts.InverseImplies;
} }
- public override LineariserOptions! SetAsTerm(bool newVal) {
+ public override LineariserOptions SetAsTerm(bool newVal) {
+ Contract.Ensures(Contract.Result<LineariserOptions>() != null);
+
if (newVal == AsTerm)
return this;
return new Z3LineariserOptions(newVal, opts, LetVariables);
@@ -158,20 +193,28 @@ namespace Microsoft.Boogie.Z3 // 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 {
+ 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) {
- List<VCExprVar!>! allVars = new List<VCExprVar!> ();
+ 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) {
- List<VCExprVar!>! allVars = new List<VCExprVar!> ();
+ 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);
@@ -183,10 +226,12 @@ namespace Microsoft.Boogie.Z3 // -----------------------------------------------------------------------------------------------
public class Z3VCExprTranslator : AxiomVCExprTranslator {
- public Z3VCExprTranslator(VCExpressionGenerator! gen, Z3InstanceOptions! opts) {
+ public Z3VCExprTranslator(VCExpressionGenerator gen, Z3InstanceOptions opts) {
+ Contract.Requires(gen != null);
+ Contract.Requires(opts != null);
Gen = gen;
Opts = opts;
- TypeAxiomBuilder! axBuilder;
+ TypeAxiomBuilder axBuilder;
switch (CommandLineOptions.Clo.TypeEncodingMethod) {
case CommandLineOptions.TypeEncoding.Arguments:
axBuilder = new TypeAxiomBuilderArguments (gen);
@@ -203,8 +248,8 @@ namespace Microsoft.Boogie.Z3 new TypeDeclCollector (namer, opts.BitVectors == CommandLineOptions.BvHandling.Z3Native);
}
- private Z3VCExprTranslator(Z3VCExprTranslator! tl) {
- base(tl);
+ 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();
@@ -213,22 +258,40 @@ namespace Microsoft.Boogie.Z3 DeclCollector = new TypeDeclCollector (namer, tl.DeclCollector);
}
- public override Object! Clone() {
+ public override Object Clone() {
+ Contract.Ensures(Contract.Result<Object>() != null);
+
return new Z3VCExprTranslator(this);
}
- private readonly Z3InstanceOptions! Opts;
- private readonly VCExpressionGenerator! Gen;
- private readonly TypeAxiomBuilder! AxBuilder;
- private readonly UniqueNamer! Namer;
- private readonly TypeDeclCollector! DeclCollector;
+[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)
+ public override string Lookup(VCExprVar var)
{
+ Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+
return Namer.Lookup(var);
}
- public override string! translate(VCExpr! expr, int polarity) {
+ public override string translate(VCExpr expr, int polarity) {
+ Contract.Requires(expr != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+
DateTime start = DateTime.Now;
if (CommandLineOptions.Clo.Trace)
Console.Write("Linearising ... ");
@@ -246,18 +309,23 @@ namespace Microsoft.Boogie.Z3 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);
- LetBindingSorter! letSorter = new LetBindingSorter(Gen);
- VCExpr! sortedExpr = letSorter.Mutate(exprWithoutTypes, true);
- VCExpr! sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);
+ 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);
if (Opts.Typed) {
DeclCollector.Collect(sortedAxioms);
DeclCollector.Collect(sortedExpr);
FeedTypeDeclsToProver();
} else {
- TermFormulaFlattener! flattener = new TermFormulaFlattener (Gen);
+ TermFormulaFlattener flattener = new TermFormulaFlattener (Gen);
+ Contract.Assert(flattener!=null);
sortedExpr = flattener.Flatten(sortedExpr);
sortedAxioms = flattener.Flatten(sortedAxioms);
}
@@ -276,11 +344,12 @@ namespace Microsoft.Boogie.Z3 //Console.WriteLine(coll);
//////////////////////////////////////////////////////////////////////////
- LineariserOptions linOptions = new Z3LineariserOptions(false, Opts, new List<VCExprVar!>());
+ LineariserOptions linOptions = new Z3LineariserOptions(false, Opts, new List<VCExprVar/*!*/>());
AddAxiom(SimplifyLikeExprLineariser.ToString(sortedAxioms, linOptions, Namer));
- string! res = SimplifyLikeExprLineariser.ToString(sortedExpr, linOptions, Namer);
+ string res = SimplifyLikeExprLineariser.ToString(sortedExpr, linOptions, Namer);
+ Contract.Assert(res!=null);
if (CommandLineOptions.Clo.Trace) {
TimeSpan elapsed = DateTime.Now - start;
@@ -290,8 +359,10 @@ namespace Microsoft.Boogie.Z3 }
private void FeedTypeDeclsToProver() {
- foreach (string! s in DeclCollector.GetNewDeclarations())
+ foreach (string s in DeclCollector.GetNewDeclarations()) {
+ Contract.Assert(s != null);
AddTypeDecl(s);
+ }
}
}
@@ -302,22 +373,29 @@ namespace Microsoft.Boogie.Z3 public class Factory : ProverFactory
{
- public override object! SpawnProver(ProverOptions! popts, object! ctxt)
+ public override object SpawnProver(ProverOptions popts, object ctxt)
{
- Z3InstanceOptions opts = (Z3InstanceOptions!)popts;
- return this.SpawnProver(((DeclFreeProverContext!)ctxt).ExprGen,
- (DeclFreeProverContext!)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) {
+ 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 = (Z3InstanceOptions!)options;
- VCExpressionGenerator! gen = new VCExpressionGenerator ();
- List<string!>! proverCommands = new List<string!> ();
+ Z3InstanceOptions opts = cce.NonNull((Z3InstanceOptions)options);
+ VCExpressionGenerator gen = new VCExpressionGenerator ();
+ List<string/*!>!*/> proverCommands = new List<string/*!*/> ();
proverCommands.Add("all");
proverCommands.Add("z3");
proverCommands.Add("simplifyLike");
@@ -325,19 +403,26 @@ namespace Microsoft.Boogie.Z3 proverCommands.Add("bvDefSem");
if (opts.BitVectors == CommandLineOptions.BvHandling.ToInt)
proverCommands.Add("bvInt");
- VCGenerationOptions! genOptions = new VCGenerationOptions(proverCommands);
+ VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands);
+
return new DeclFreeProverContext(gen, genOptions);
}
- public override ProverOptions! BlankProverOptions()
+ public override ProverOptions BlankProverOptions()
{
+ Contract.Ensures(Contract.Result<ProverOptions>() != null);
return new Z3InstanceOptions();
}
- protected virtual Z3ProcessTheoremProver! SpawnProver(VCExpressionGenerator! gen,
- DeclFreeProverContext! ctx,
- Z3InstanceOptions! opts) {
+ 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);
}
}
diff --git a/Source/Provers/Z3/TypeDeclCollector.cs b/Source/Provers/Z3/TypeDeclCollector.cs index 4d6accaf..d972eba2 100644 --- a/Source/Provers/Z3/TypeDeclCollector.cs +++ b/Source/Provers/Z3/TypeDeclCollector.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.Z3
@@ -22,97 +22,126 @@ namespace Microsoft.Boogie.Z3 public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
- private readonly UniqueNamer! Namer;
+ private readonly UniqueNamer Namer;
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(Namer!=null);
+ Contract.Invariant(AllDecls != null);
+ Contract.Invariant(IncDecls != null);
+ Contract.Invariant(cce.NonNullElements(KnownFunctions));
+ Contract.Invariant(cce.NonNullElements(KnownVariables));
+ Contract.Invariant(cce.NonNullElements(KnownTypes));
+ Contract.Invariant(cce.NonNullElements(KnownBvOps));
+ Contract.Invariant(cce.NonNullElements(KnownSelectFunctions));
+ Contract.Invariant(cce.NonNullElements(KnownStoreFunctions));
+}
+
private readonly bool NativeBv;
- public TypeDeclCollector(UniqueNamer! namer, 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 Dictionary<Function!, bool> ();
- KnownVariables = new Dictionary<VCExprVar!, bool> ();
- KnownTypes = new Dictionary<Type!, bool> ();
- KnownBvOps = new Dictionary<string!, bool> ();
+ AllDecls = new List<string/*!*/> ();
+ IncDecls = new List<string/*!*/> ();
+ KnownFunctions = new Dictionary<Function/*!*/, bool> ();
+ KnownVariables = new Dictionary<VCExprVar/*!*/, bool> ();
+ KnownTypes = new Dictionary<Type/*!*/, bool> ();
+ KnownBvOps = new Dictionary<string/*!*/, bool> ();
- KnownStoreFunctions = new Dictionary<string!, bool> ();
- KnownSelectFunctions = new Dictionary<string!, bool> ();
+ KnownStoreFunctions = new Dictionary<string/*!*/, bool>();
+ KnownSelectFunctions = new Dictionary<string/*!*/, bool>();
}
- internal TypeDeclCollector(UniqueNamer! namer, TypeDeclCollector! coll) {
+ 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 Dictionary<Function!, bool> (coll.KnownFunctions);
- KnownVariables = new Dictionary<VCExprVar!, bool> (coll.KnownVariables);
- KnownTypes = new Dictionary<Type!, bool> (coll.KnownTypes);
- KnownBvOps = new Dictionary<string!, bool> (coll.KnownBvOps);
+ AllDecls = new List<string/*!*/> (coll.AllDecls);
+ IncDecls = new List<string/*!*/> (coll.IncDecls);
+ KnownFunctions = new Dictionary<Function/*!*/, bool> (coll.KnownFunctions);
+ KnownVariables = new Dictionary<VCExprVar/*!*/, bool> (coll.KnownVariables);
+ KnownTypes = new Dictionary<Type/*!*/, bool> (coll.KnownTypes);
+ KnownBvOps = new Dictionary<string/*!*/, bool> (coll.KnownBvOps);
- KnownStoreFunctions = new Dictionary<string!, bool> (coll.KnownStoreFunctions);
- KnownSelectFunctions = new Dictionary<string!, bool> (coll.KnownSelectFunctions);
+ KnownStoreFunctions = new Dictionary<string/*!*/, bool> (coll.KnownStoreFunctions);
+ KnownSelectFunctions = new Dictionary<string/*!*/, bool> (coll.KnownSelectFunctions);
}
// not used
- protected override bool StandardResult(VCExpr! node, bool arg) {
+ 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 List<string/*!>!*/> AllDecls;
+ private readonly List<string/*!>!*/> IncDecls;
- private readonly IDictionary<Function!, bool>! KnownFunctions;
- private readonly IDictionary<VCExprVar!, bool>! KnownVariables;
+ private readonly IDictionary<Function/*!*/, bool>/*!*/ KnownFunctions;
+ private readonly IDictionary<VCExprVar/*!*/, bool>/*!*/ KnownVariables;
// bitvector types have to be registered as well
- private readonly IDictionary<Type!, bool>! KnownTypes;
+ private readonly IDictionary<Type/*!*/, bool>/*!*/ KnownTypes;
// the names of registered BvConcatOps and BvExtractOps
- private readonly IDictionary<string!, bool>! KnownBvOps;
+ private readonly IDictionary<string/*!*/, bool>/*!*/ KnownBvOps;
+
+ private readonly IDictionary<string/*!*/, bool>/*!*/ KnownStoreFunctions;
+ private readonly IDictionary<string/*!*/, bool>/*!*/ KnownSelectFunctions;
- private readonly IDictionary<string!, bool>! KnownStoreFunctions;
- private readonly IDictionary<string!, bool>! KnownSelectFunctions;
+ public List<string/*!>!*/> AllDeclarations { get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<string>>()));
- public List<string!>! AllDeclarations { get {
- List<string!>! res = new List<string!> ();
+ List<string/*!>!*/> res = new List<string/*!*/> ();
res.AddRange(AllDecls);
return res;
} }
- public List<string!>! GetNewDeclarations() {
- List<string!>! res = new List<string!> ();
+ 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) {
+ private void AddDeclaration(string decl) {
+ Contract.Requires(decl != null);
AllDecls.Add(decl);
IncDecls.Add(decl);
}
- public void Collect(VCExpr! expr) {
+ public void Collect(VCExpr expr) {
+ Contract.Requires(expr != null);
Traverse(expr, true);
}
///////////////////////////////////////////////////////////////////////////
- private static string! TypeToString(Type! t) {
+ 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)
+ private void RegisterType(Type type)
{
+ Contract.Requires(type != null);
if (KnownTypes.ContainsKey(type)) return;
if (type.IsMap && CommandLineOptions.Clo.UseArrayTheory) {
KnownTypes.Add(type, true);
string declString = "";
- MapType! mapType = type.AsMap;
+ MapType mapType = type.AsMap;
+ Contract.Assert(mapType!=null);
declString += "(DEFTYPE " + TypeToString(type) + " :BUILTIN Array ";
- foreach (Type! t in mapType.Arguments) {
+ foreach (Type t in mapType.Arguments) {
+ Contract.Assert(t!=null);
RegisterType(t);
declString += TypeToString(t);
declString += " ";
@@ -132,7 +161,7 @@ namespace Microsoft.Boogie.Z3 // 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))";
+ string expr = "($make_bv" + bits + " (" + name + "_to_int x))";
AddDeclaration("(BG_PUSH (FORALL (x :TYPE " + name + ") (PATS "
+ expr + ") (QID bvconv" + bits + ") (EQ " + expr + " x)))");
@@ -140,7 +169,8 @@ namespace Microsoft.Boogie.Z3 }
}
- public override bool Visit(VCExprNAry! node, bool arg) {
+ 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
@@ -168,7 +198,8 @@ namespace Microsoft.Boogie.Z3 RegisterType(node[0].Type);
RegisterType(node.Type);
- VCExprBvExtractOp! op = (VCExprBvExtractOp)node.Op;
+ VCExprBvExtractOp op = (VCExprBvExtractOp)node.Op;
+ Contract.Assert(op!=null);
string name = SimplifyLikeExprLineariser.BvExtractOpName(node);
if (!KnownBvOps.ContainsKey(name)) {
AddDeclaration("(DEFOP " + name +
@@ -216,21 +247,25 @@ namespace Microsoft.Boogie.Z3 //
VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;
if (op != null && !KnownFunctions.ContainsKey(op.Func)) {
- Function! f = op.Func;
- string! printedName = Namer.GetName(f, f.Name);
- string! decl = "(DEFOP " + SimplifyLikeExprLineariser.MakeIdPrintable(printedName);
-
- foreach (Variable! v in f.InParams) {
+ 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);
}
- assert f.OutParams.Length == 1;
- foreach (Variable! v in f.OutParams) {
+ 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);
+ string builtin = ExtractBuiltin(f);
if (builtin != null)
decl += " :BUILTIN " + builtin;
@@ -245,8 +280,9 @@ namespace Microsoft.Boogie.Z3 return base.Visit(node, arg);
}
- private string? ExtractBuiltin(Function! f) {
- string? retVal = null;
+ private string ExtractBuiltin(Function f) {
+ Contract.Requires(f != null);
+ string retVal = null;
if (NativeBv) {
retVal = f.FindStringAttribute("bvbuiltin");
}
@@ -256,11 +292,13 @@ namespace Microsoft.Boogie.Z3 return retVal;
}
- public override bool Visit(VCExprVar! node, bool arg) {
+ public override bool Visit(VCExprVar node, bool arg) {
+ Contract.Requires(node != null);
if (!BoundTermVars.Contains(node) && !KnownVariables.ContainsKey(node)) {
RegisterType(node.Type);
- string! printedName = Namer.GetName(node, node.Name);
- string! decl =
+ string printedName = Namer.GetName(node, node.Name);
+ Contract.Assert(printedName!=null);
+ string decl =
"(DEFOP " + SimplifyLikeExprLineariser.MakeIdPrintable(printedName)
+ " " + TypeToString(node.Type) + ")";
AddDeclaration(decl);
@@ -270,9 +308,12 @@ namespace Microsoft.Boogie.Z3 return base.Visit(node, arg);
}
- public override bool Visit(VCExprQuantifier! node, bool arg) {
- foreach (VCExprVar! v in node.BoundVars)
+ 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);
}
diff --git a/Source/Provers/Z3/Z3.csproj b/Source/Provers/Z3/Z3.csproj index 4d7b3ee6..e6518833 100644 --- a/Source/Provers/Z3/Z3.csproj +++ b/Source/Provers/Z3/Z3.csproj @@ -1,144 +1,125 @@ -<?xml version="1.0" encoding="utf-8"?>
-<VisualStudioProject>
- <XEN ProjectType="Local"
- SchemaVersion="1.0"
- Name="Z3"
- ProjectGuid="f75666de-cd56-457c-8782-09be243450fc"
- >
- <Build>
- <Settings ApplicationIcon=""
- AssemblyName="Provers.Z3"
- OutputType="Library"
- RootNamespace="Microsoft.Boogie.Z3"
- 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="Simplify"
- Project="{F75666DE-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="TypeDeclCollector.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="Inspector.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="AssemblyInfo.ssc"
- />
- </Include>
- </Files>
- </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>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>Provers.Z3</RootNamespace>
+ <AssemblyName>Z3</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>
+ </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>..\..\AIFramework\bin\debug\AIFramework.dll</HintPath>
+ </Reference>
+ <Reference Include="Basetypes, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\Basetypes\bin\debug\Basetypes.dll</HintPath>
+ </Reference>
+ <Reference Include="Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\Core\bin\Debug\Core.dll</HintPath>
+ </Reference>
+ <Reference Include="Graph, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\Graph\bin\debug\Graph.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <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>
+ <HintPath>..\..\..\Binaries\System.Compiler.Runtime.dll</HintPath>
+ </Reference>
+ <Reference Include="System.Core">
+ <RequiredTargetFramework>3.5</RequiredTargetFramework>
+ </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>..\..\VCExpr\bin\debug\VCExpr.dll</HintPath>
+ </Reference>
+ <Reference Include="VCGeneration, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\VCGeneration\bin\debug\VCGeneration.dll</HintPath>
+ </Reference>
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="cce.cs" />
+ <Compile Include="Inspector.cs" />
+ <Compile Include="Prover.cs" />
+ <Compile Include="ProverInterface.cs" />
+ <Compile Include="TypeDeclCollector.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 |