From f1ad586e7619b0a9269c2d1d00a21a810f6eb45c Mon Sep 17 00:00:00 2001 From: tabarbe Date: Tue, 20 Jul 2010 22:53:45 +0000 Subject: Boogie: Committing ported version of Z3. --- Source/Provers/Z3/Inspector.cs | 63 ++-- Source/Provers/Z3/Prover.cs | 509 +++++++++++++++++++++++---------- Source/Provers/Z3/ProverInterface.cs | 207 ++++++++++---- Source/Provers/Z3/TypeDeclCollector.cs | 155 ++++++---- Source/Provers/Z3/Z3.csproj | 269 ++++++++--------- 5 files changed, 772 insertions(+), 431 deletions(-) (limited to 'Source/Provers/Z3') 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 { - public Dictionary! Labels = new Dictionary(); + public Dictionary/*!*/ Labels = new Dictionary(); + [ContractInvariantMethod] +void ObjectInvariant() +{ + Contract.Invariant(Labels!=null&&cce.NonNullElements(Labels.Keys)); +} + + + public static Dictionary/*!*/ FindLabels(VCExpr/*!*/ expr) { + Contract.Requires(expr != null); + Contract.Ensures(Contract.Result/*!*/>() != null&&cce.NonNullElements(Contract.Result/*!*/>().Keys)); - public static Dictionary! 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! labels = FindLabelsVisitor.FindLabels(vc); + Contract.Requires(descriptiveName != null); + Contract.Requires(vc != null); + Contract.Requires(handler != null); + Dictionary/*!*/ 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! parms, string! option, string! value) - modifies parms.*; + static void AddOption(List 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! parameterSettings; - // [NotDelayed] + private List!*/> 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 parms = new List(); + Contract.Requires(opts != null); + Contract.Requires(inspector == null || cce.Owner.Same(opts, inspector)); + string z3args = OptionChar() + "si"; + List parms = new List(); + + 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 parms = new List(); 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() != 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! ParameterSettings { + //[Pure(false)] + public override IEnumerable!*/> ParameterSettings { get { + Contract.Ensures(cce.NonNullElements( Contract.Result>())); + 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() != 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(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! l = ParseLabels(line); + List/*!*/ 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() == "." || Contract.Result().StartsWith("labels: (") || Contract.Result() == "END_OF_MODEL"); + Contract.Ensures(Contract.Result() != 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 identifierToPartition = new Dictionary(); + Dictionary identifierToPartition = new Dictionary(); // map each ZID to the set (in list form) of IDs belonging to it (possibly empty): - List> partitionToIdentifiers = new List>(); + List> partitionToIdentifiers = new List>(); // map each ZID to the number or boolean given, if any: List partitionToValue = new List(); // map each value (number or boolean) to the ZID, reverse map of partitionToValue Dictionary valueToPartition = new Dictionary(); - 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 emptyList = new List(); - Owner.AssignSame(emptyList, Owner.ElementProxy(partitionToIdentifiers)); + List emptyList = new List(); + 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! identifierToPartition, - List>! partitionToIdentifiers, - List! partitionToValue, - Dictionary! valueToPartition) - requires Owner.Same(Owner.ElementProxy(partitionToValue), Owner.ElementProxy(valueToPartition)); - modifies this.*, identifierToPartition.*, partitionToIdentifiers.*, partitionToValue.*, valueToPartition.*; + Dictionary/*!*/ identifierToPartition, + List>/*!*/ partitionToIdentifiers, + List/*!*/ partitionToValue, + Dictionary/*!*/ 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!> arrayModel = new List!>(); + List/*!*/> arrayModel = new List/*!*/>(); + 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(); } - 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! identifierToPartition, - List>! partitionToIdentifiers) - modifies identifierToPartition.*, partitionToIdentifiers.*; - ensures 0 <= result && result <= s.Length; + private static int ParseModelZidAndIdentifiers(int zID, string s, + Dictionary/*!*/ identifierToPartition, + List>/*!*/ partitionToIdentifiers) + //TODO: modifies identifierToPartition.*, partitionToIdentifiers.*; + //TODO: Find all modifies statements { - List identifiers = new List(); + 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() && Contract.Result() <= s.Length); + + List identifiers = new List(); 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! identifierToPartition, - List>! partitionToIdentifiers, - List! partitionToValue, - Dictionary! valueToPartition + private string ParseModelFunctions(int ch, out Z3ErrorModel errModel, + Dictionary/*!*/ identifierToPartition, + List>/*!*/ partitionToIdentifiers, + List/*!*/ partitionToValue, + Dictionary/*!*/ 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() != null); + Contract.Ensures(Contract.Result() == "." || Contract.Result().StartsWith("labels: (") || Contract.Result() == "END_OF_MODEL"); + Contract.EnsuresOnThrow(true); // read the function F Expect(ch, "function interpretations:"); FromReadLine(); // mapping of function names to function definitions - Dictionary>!> definedFunctions = new Dictionary>!>(); + Dictionary>/*!*/> definedFunctions = new Dictionary>/*!*/>(); // 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> functionDefinition = new List>(); @@ -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(); 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! identifierToPartition, List>! partitionToIdentifiers, List! partitionToValue, Dictionary! valueToPartition, Dictionary>!>! definedFunctions) + public Z3ErrorModel(Dictionary/*!*/ identifierToPartition, + List>/*!*/ partitionToIdentifiers, + List/*!*/ partitionToValue, + Dictionary/*!*/ valueToPartition, + Dictionary>/*!*/>/*!*/ 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() != 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! possible_names = new List(); - List pti = partitionToIdentifiers[pos]; + List/*!*/ possible_names = new List(); + List 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>!> kv in definedFunctions) { - foreach (List! parms in kv.Value) { + foreach (KeyValuePair>/*!*/> kv in definedFunctions) { + Contract.Assert(kv.Key!=null); + Contract.Assert(kv.Value!=null); + foreach (List 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 pti = partitionToIdentifiers[i]; + List 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 funNames = new List(definedFunctions.Keys); + List funNames = new List(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! parms in definedFunctions[name]) { - string! s = name + "("; + foreach (List 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 pti = partitionToIdentifiers[i]; + List 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!> array = tempPTVI as List!>; - assume array != null; + } else if (tempPTVI is List>) { + List> array = tempPTVI as List>; + Contract.Assume( array != null); writer.Write(" -> {"); foreach(List 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>!> kvp in definedFunctions) { + foreach (KeyValuePair>> kvp in definedFunctions) { + Contract.Assert(kvp.Key!=null); writer.WriteLine(kvp.Key + " -> {"); List> kvpValue = kvp.Value; if (kvpValue != null) { @@ -923,7 +1129,8 @@ namespace Microsoft.Boogie.Z3 if (CommandLineOptions.Clo.PrintErrorModel >= 2) { writer.WriteLine("identifierToPartition:"); - foreach (KeyValuePair kvp in identifierToPartition) { + foreach (KeyValuePair 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(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() != 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() != 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() && Contract.Result() < 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! letVariables) { - base(asTerm); + internal Z3LineariserOptions(bool asTerm, Z3InstanceOptions opts, List!*/> 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() != 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! LetVariablesAttr; - public override List! LetVariables { get { + private readonly List!*/> LetVariablesAttr; + public override List!*/> LetVariables { get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return LetVariablesAttr; } } - public override LineariserOptions! AddLetVariable(VCExprVar! furtherVar) { - List! allVars = new List (); + public override LineariserOptions AddLetVariable(VCExprVar furtherVar) { + Contract.Requires(furtherVar != null); + Contract.Ensures(Contract.Result() != null); + + List!*/> allVars = new List(); allVars.AddRange(LetVariables); allVars.Add(furtherVar); return new Z3LineariserOptions(AsTerm, opts, allVars); } - public override LineariserOptions! AddLetVariables(List! furtherVars) { - List! allVars = new List (); + public override LineariserOptions AddLetVariables(List!*/> furtherVars) { + Contract.Requires(furtherVars != null); + Contract.Ensures(Contract.Result() != null); + + List!*/> allVars = new List (); 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() != 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() != 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() != 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()); + LineariserOptions linOptions = new Z3LineariserOptions(false, Opts, new List()); 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() != 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() != null); + if (CommandLineOptions.Clo.BracketIdsInVC < 0) { CommandLineOptions.Clo.BracketIdsInVC = 0; } - Z3InstanceOptions opts = (Z3InstanceOptions!)options; - VCExpressionGenerator! gen = new VCExpressionGenerator (); - List! proverCommands = new List (); + Z3InstanceOptions opts = cce.NonNull((Z3InstanceOptions)options); + VCExpressionGenerator gen = new VCExpressionGenerator (); + List!*/> proverCommands = new List (); 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() != 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() != 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 { - 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 (); - IncDecls = new List (); - KnownFunctions = new Dictionary (); - KnownVariables = new Dictionary (); - KnownTypes = new Dictionary (); - KnownBvOps = new Dictionary (); + AllDecls = new List (); + IncDecls = new List (); + KnownFunctions = new Dictionary (); + KnownVariables = new Dictionary (); + KnownTypes = new Dictionary (); + KnownBvOps = new Dictionary (); - KnownStoreFunctions = new Dictionary (); - KnownSelectFunctions = new Dictionary (); + KnownStoreFunctions = new Dictionary(); + KnownSelectFunctions = new Dictionary(); } - 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 (coll.AllDecls); - IncDecls = new List (coll.IncDecls); - KnownFunctions = new Dictionary (coll.KnownFunctions); - KnownVariables = new Dictionary (coll.KnownVariables); - KnownTypes = new Dictionary (coll.KnownTypes); - KnownBvOps = new Dictionary (coll.KnownBvOps); + AllDecls = new List (coll.AllDecls); + IncDecls = new List (coll.IncDecls); + KnownFunctions = new Dictionary (coll.KnownFunctions); + KnownVariables = new Dictionary (coll.KnownVariables); + KnownTypes = new Dictionary (coll.KnownTypes); + KnownBvOps = new Dictionary (coll.KnownBvOps); - KnownStoreFunctions = new Dictionary (coll.KnownStoreFunctions); - KnownSelectFunctions = new Dictionary (coll.KnownSelectFunctions); + KnownStoreFunctions = new Dictionary (coll.KnownStoreFunctions); + KnownSelectFunctions = new Dictionary (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! AllDecls; - private readonly List! IncDecls; + private readonly List!*/> AllDecls; + private readonly List!*/> IncDecls; - private readonly IDictionary! KnownFunctions; - private readonly IDictionary! KnownVariables; + private readonly IDictionary/*!*/ KnownFunctions; + private readonly IDictionary/*!*/ KnownVariables; // bitvector types have to be registered as well - private readonly IDictionary! KnownTypes; + private readonly IDictionary/*!*/ KnownTypes; // the names of registered BvConcatOps and BvExtractOps - private readonly IDictionary! KnownBvOps; + private readonly IDictionary/*!*/ KnownBvOps; + + private readonly IDictionary/*!*/ KnownStoreFunctions; + private readonly IDictionary/*!*/ KnownSelectFunctions; - private readonly IDictionary! KnownStoreFunctions; - private readonly IDictionary! KnownSelectFunctions; + public List!*/> AllDeclarations { get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); - public List! AllDeclarations { get { - List! res = new List (); + List!*/> res = new List (); res.AddRange(AllDecls); return res; } } - public List! GetNewDeclarations() { - List! res = new List (); + public List!*/> GetNewDeclarations() { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + List!*/> res = new List (); 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() != 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 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - \ No newline at end of file + + + + Debug + AnyCPU + 9.0.30729 + 2.0 + {BB49B90B-BE21-4BE8-85BA-359FDB55F4DF} + Library + Properties + Provers.Z3 + Z3 + v3.5 + 512 + 0 + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + False + False + True + False + False + False + False + False + False + False + False + True + False + False + False + + + + + + + + + + + + + Full + %28none%29 + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + + + + False + ..\..\AIFramework\bin\debug\AIFramework.dll + + + False + ..\..\Basetypes\bin\debug\Basetypes.dll + + + False + ..\..\Core\bin\Debug\Core.dll + + + False + ..\..\Graph\bin\debug\Graph.dll + + + False + ..\..\..\..\Binaries\Microsoft.Contracts.dll + + + False + ..\Simplify\bin\debug\Provers.Simplify.dll + + + + False + ..\..\..\Binaries\System.Compiler.Runtime.dll + + + 3.5 + + + + + False + ..\..\VCExpr\bin\debug\VCExpr.dll + + + False + ..\..\VCGeneration\bin\debug\VCGeneration.dll + + + + + + + + + + + + + + + \ No newline at end of file -- cgit v1.2.3