diff options
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.ssc | 240 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLib.sscproj | 116 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.ssc | 635 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/TypeDeclCollector.ssc | 107 | ||||
| -rw-r--r-- | Source/Provers/Simplify/Let2ImpliesVisitor.ssc | 183 | ||||
| -rw-r--r-- | Source/Provers/Simplify/Prover.ssc | 606 | ||||
| -rw-r--r-- | Source/Provers/Simplify/ProverInterface.ssc | 633 | ||||
| -rw-r--r-- | Source/Provers/Simplify/Simplify.sscproj | 135 | ||||
| -rw-r--r-- | Source/Provers/Z3/Inspector.ssc | 130 | ||||
| -rw-r--r-- | Source/Provers/Z3/Prover.ssc | 870 | ||||
| -rw-r--r-- | Source/Provers/Z3/ProverInterface.ssc | 320 | ||||
| -rw-r--r-- | Source/Provers/Z3/TypeDeclCollector.ssc | 212 | ||||
| -rw-r--r-- | Source/Provers/Z3/Z3.sscproj | 140 |
13 files changed, 4327 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.ssc b/Source/Provers/SMTLib/ProverInterface.ssc new file mode 100644 index 00000000..b55cc403 --- /dev/null +++ b/Source/Provers/SMTLib/ProverInterface.ssc @@ -0,0 +1,240 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using ExternalProver;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie;
+using Microsoft.Boogie.VCExprAST;
+using Microsoft.Boogie.Clustering;
+using Microsoft.Boogie.TypeErasure;
+using Microsoft.Boogie.Simplify;
+
+namespace Microsoft.Boogie.SMTLib
+{
+ public class SMTLibProcessTheoremProver : LogProverInterface
+ {
+ private readonly DeclFreeProverContext! ctx;
+
+ [NotDelayed]
+ public SMTLibProcessTheoremProver(ProverOptions! options, VCExpressionGenerator! gen,
+ DeclFreeProverContext! ctx)
+ {
+ InitializeGlobalInformation("UnivBackPred2.smt");
+
+ this.ctx = ctx;
+
+ TypeAxiomBuilder! axBuilder;
+ switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+ case CommandLineOptions.TypeEncoding.Arguments:
+ axBuilder = new TypeAxiomBuilderArguments (gen);
+ break;
+ default:
+ axBuilder = new TypeAxiomBuilderPremisses (gen);
+ break;
+ }
+ axBuilder.Setup();
+ AxBuilder = axBuilder;
+ UniqueNamer namer = new UniqueNamer ();
+ Namer = namer;
+ this.DeclCollector = new TypeDeclCollector (namer);
+ base(options, "", "", "", "", gen);
+ }
+
+ public override ProverContext! Context { get {
+ return ctx;
+ } }
+
+ private readonly TypeAxiomBuilder! AxBuilder;
+ private readonly UniqueNamer! Namer;
+ private readonly TypeDeclCollector! DeclCollector;
+
+ private void FeedTypeDeclsToProver() {
+ foreach (string! s in DeclCollector.GetNewDeclarations())
+ AddTypeDecl(s);
+ }
+
+ public override void BeginCheck(string! descriptiveName, VCExpr! vc, ErrorHandler! handler) {
+ TextWriter! output = OpenOutputFile(descriptiveName);
+
+ string! name =
+ MakeBenchmarkNameSafe(SMTLibExprLineariser.MakeIdPrintable(descriptiveName));
+ WriteLineAndLog(output, "(benchmark " + name);
+ WriteLineAndLog(output, _backgroundPredicates);
+
+ if (!AxiomsAreSetup) {
+ AddAxiom(VCExpr2String(ctx.Axioms, -1));
+ AxiomsAreSetup = true;
+ }
+
+ string vcString = ":formula (not " + VCExpr2String(vc, 1) + ")";
+ string! prelude = ctx.GetProverCommands(true);
+ WriteLineAndLog(output, prelude);
+
+ foreach (string! s in TypeDecls) {
+ WriteLineAndLog(output, s);
+ }
+ foreach (string! s in Axioms) {
+ WriteLineAndLog(output, ":assumption");
+ WriteLineAndLog(output, s);
+ }
+
+ WriteLineAndLog(output, vcString);
+ WriteLineAndLog(output, ")");
+
+ output.Close();
+ }
+
+ // certain words that should not occur in the name of a benchmark
+ // because some solvers don't like them
+ private readonly static List<string!>! BadBenchmarkWords = new List<string!> ();
+ static SMTLibProcessTheoremProver() {
+ BadBenchmarkWords.Add("Array"); BadBenchmarkWords.Add("Arrray");
+ }
+
+ private string! MakeBenchmarkNameSafe(string! name) {
+ for (int i = 0; i < BadBenchmarkWords.Count; i = i + 2)
+ name = name.Replace(BadBenchmarkWords[i], BadBenchmarkWords[i+1]);
+ return name;
+ }
+
+ private TextWriter! OpenOutputFile(string! descriptiveName) {
+ string filename = CommandLineOptions.Clo.SMTLibOutputPath;
+ filename = Helpers.SubstituteAtPROC(descriptiveName, (!)filename);
+ return new StreamWriter(filename, false);
+ }
+
+ private void WriteLineAndLog(TextWriter! output, string! msg) {
+ LogActivity(msg);
+ output.WriteLine(msg);
+ }
+
+ [NoDefaultContract]
+ public override Outcome CheckOutcome(ErrorHandler! handler)
+ throws UnexpectedProverOutputException; {
+ return Outcome.Undetermined;
+ }
+
+ protected string! VCExpr2String(VCExpr! expr, int polarity) {
+ DateTime start = DateTime.Now;
+ if (CommandLineOptions.Clo.Trace)
+ Console.Write("Linearising ... ");
+
+ // handle the types in the VCExpr
+ TypeEraser! eraser;
+ switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+ case CommandLineOptions.TypeEncoding.Arguments:
+ eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, gen);
+ break;
+ default:
+ eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, gen);
+ break;
+ }
+ VCExpr! exprWithoutTypes = eraser.Erase(expr, polarity);
+
+ LetBindingSorter! letSorter = new LetBindingSorter(gen);
+ VCExpr! sortedExpr = letSorter.Mutate(exprWithoutTypes, true);
+ VCExpr! sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);
+
+ DeclCollector.Collect(sortedAxioms);
+ DeclCollector.Collect(sortedExpr);
+ FeedTypeDeclsToProver();
+
+ AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer));
+ string! res = SMTLibExprLineariser.ToString(sortedExpr, Namer);
+
+ if (CommandLineOptions.Clo.Trace) {
+ DateTime end = DateTime.Now;
+ TimeSpan elapsed = end - start;
+ Console.WriteLine("finished [{0} s] ", elapsed.TotalSeconds);
+ }
+ return res;
+ }
+
+ // the list of all known axioms, where have to be included in each
+ // verification condition
+ private readonly List<string!>! Axioms = new List<string!> ();
+ private bool AxiomsAreSetup = false;
+
+ // similarly, a list of function/predicate declarations
+ private readonly List<string!>! TypeDecls = new List<string!> ();
+
+ protected void AddAxiom(string! axiom) {
+ Axioms.Add(axiom);
+// if (thmProver != null) {
+// LogActivity(":assume " + axiom);
+// thmProver.AddAxioms(axiom);
+// }
+ }
+
+ protected void AddTypeDecl(string! decl) {
+ TypeDecls.Add(decl);
+ // if (thmProver != null) {
+ // LogActivity(decl);
+ // thmProver.Feed(decl, 0);
+ // }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ private static string! _backgroundPredicates;
+
+ static void InitializeGlobalInformation(string! backgroundPred)
+ ensures _backgroundPredicates != null;
+ //throws ProverException, System.IO.FileNotFoundException;
+ {
+ if (_backgroundPredicates == null) {
+ string! codebaseString =
+ (!) Path.GetDirectoryName((!)System.Reflection.Assembly.GetExecutingAssembly().Location);
+
+ // Initialize '_backgroundPredicates'
+ string univBackPredPath = Path.Combine(codebaseString, backgroundPred);
+ using (StreamReader reader = new System.IO.StreamReader(univBackPredPath))
+ {
+ _backgroundPredicates = reader.ReadToEnd();
+ }
+ }
+ }
+ }
+
+ public class Factory : ProverFactory
+ {
+
+ public override object! SpawnProver(ProverOptions! options, object! ctxt)
+ {
+ return this.SpawnProver(options,
+ ((DeclFreeProverContext!)ctxt).ExprGen,
+ (DeclFreeProverContext!)ctxt);
+ }
+
+ public override object! NewProverContext(ProverOptions! options) {
+ if (CommandLineOptions.Clo.BracketIdsInVC < 0) {
+ CommandLineOptions.Clo.BracketIdsInVC = 0;
+ }
+
+ VCExpressionGenerator! gen = new VCExpressionGenerator ();
+ List<string!>! proverCommands = new List<string!> ();
+// TODO: what is supported?
+// proverCommands.Add("all");
+// proverCommands.Add("simplify");
+// proverCommands.Add("simplifyLike");
+ VCGenerationOptions! genOptions = new VCGenerationOptions(proverCommands);
+
+ return new DeclFreeProverContext(gen, genOptions);
+ }
+
+ protected virtual SMTLibProcessTheoremProver! SpawnProver(ProverOptions! options,
+ VCExpressionGenerator! gen,
+ DeclFreeProverContext! ctx) {
+ return new SMTLibProcessTheoremProver(options, gen, ctx);
+ }
+ }
+}
diff --git a/Source/Provers/SMTLib/SMTLib.sscproj b/Source/Provers/SMTLib/SMTLib.sscproj new file mode 100644 index 00000000..d618b0dd --- /dev/null +++ b/Source/Provers/SMTLib/SMTLib.sscproj @@ -0,0 +1,116 @@ +<?xml version="1.0" encoding="utf-8"?>
+<VisualStudioProject>
+ <XEN ProjectType="Local"
+ SchemaVersion="1.0"
+ Name="SMTLib"
+ ProjectGuid="13c3a68c-462a-4cda-a480-738046e37c5a"
+ >
+ <Build>
+ <Settings ApplicationIcon=""
+ AssemblyName="Provers.SMTLib"
+ OutputType="Library"
+ RootNamespace="Microsoft.Boogie.SMTLib"
+ 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"
+ 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"
+ CheckContractAdmissibility="True"
+ CheckPurity="False"
+ />
+ </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="Basetypes"
+ Project="{0C692837-77EC-415F-BF04-395E3ED06E9A}"
+ Private="true"
+ />
+ <Reference Name="Core"
+ Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"
+ Private="true"
+ />
+ <Reference Name="VCExpr"
+ Project="{CF42B700-10AA-4DA9-8992-48A800251C11}"
+ Private="true"
+ />
+ <Reference Name="VCGeneration"
+ Project="{F65666DE-FB56-457C-8782-09BE243450FC}"
+ Private="true"
+ />
+ <Reference Name="Mscorlib.Contracts"
+ AssemblyName="Mscorlib.Contracts"
+ Private="false"
+ HintPath="../../../Binaries/Mscorlib.Contracts.dll"
+ />
+ <Reference Name="Simplify"
+ Project="{F75666DE-FB56-457C-8782-09BE243450FC}"
+ Private="true"
+ />
+ </References>
+ </Build>
+ <Files>
+ <Include>
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="ProverInterface.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="SMTLibLineariser.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="TypeDeclCollector.ssc"
+ />
+ </Include>
+ </Files>
+ </XEN>
+</VisualStudioProject>
\ No newline at end of file diff --git a/Source/Provers/SMTLib/SMTLibLineariser.ssc b/Source/Provers/SMTLib/SMTLibLineariser.ssc new file mode 100644 index 00000000..cbf69107 --- /dev/null +++ b/Source/Provers/SMTLib/SMTLibLineariser.ssc @@ -0,0 +1,635 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using Microsoft.Contracts;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+// Method to turn VCExprs into strings that can be fed into SMT
+// solvers. This is currently quite similar to the
+// SimplifyLikeLineariser (but the code is independent)
+
+namespace Microsoft.Boogie.SMTLib
+{
+
+ // Options for the linearisation
+ public class LineariserOptions {
+
+ public readonly bool AsTerm;
+ public LineariserOptions! SetAsTerm(bool newVal) {
+ if (newVal)
+ return DefaultTerm;
+ else
+ return Default;
+ }
+
+ internal LineariserOptions(bool asTerm) {
+ this.AsTerm = asTerm;
+ }
+
+ public static readonly LineariserOptions! Default = new LineariserOptions (false);
+ internal static readonly LineariserOptions! DefaultTerm = new LineariserOptions (true);
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////////////////
+
+ // Lineariser for expressions. The result (bool) is currently not used for anything
+ public class SMTLibExprLineariser : IVCExprVisitor<bool, LineariserOptions!> {
+
+ public static string! ToString(VCExpr! e, UniqueNamer! namer) {
+ StringWriter sw = new StringWriter();
+ SMTLibExprLineariser! lin = new SMTLibExprLineariser (sw, namer);
+ lin.Linearise(e, LineariserOptions.Default);
+ return (!)sw.ToString();
+ }
+
+ ////////////////////////////////////////////////////////////////////////////////////////
+
+ private readonly TextWriter! wr;
+ private SMTLibOpLineariser OpLinObject = null;
+ private IVCExprOpVisitor<bool, LineariserOptions!>! OpLineariser { get {
+ if (OpLinObject == null)
+ OpLinObject = new SMTLibOpLineariser (this, wr);
+ return OpLinObject;
+ } }
+
+ internal readonly UniqueNamer! Namer;
+
+ public SMTLibExprLineariser(TextWriter! wr, UniqueNamer! namer) {
+ this.wr = wr;
+ this.Namer = namer;
+ }
+
+ public void Linearise(VCExpr! expr, LineariserOptions! options) {
+ expr.Accept<bool, LineariserOptions!>(this, options);
+ }
+
+ public void LineariseAsTerm(VCExpr! expr, LineariserOptions! options) {
+ Linearise(expr, options.SetAsTerm(true));
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ internal static string! TypeToString(Type! t) {
+ if (t.IsBool)
+ return "TermBool";
+ else if (t.IsInt)
+ return "Int";
+ else if (t.IsBv)
+ assert false; // bitvectors are currently not handled for SMT-Lib solvers
+ else {
+ // at this point, only the types U, T should be left
+ System.IO.StringWriter buffer = new System.IO.StringWriter();
+ using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
+ t.Emit(stream);
+ }
+ return "boogie" + buffer.ToString();
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public static string! MakeIdPrintable(string! s) {
+ // make sure that no keywords are used as identifiers
+ switch(s) {
+ case andName:
+ case orName:
+ case notName:
+ case impliesName:
+ case iffName:
+ case eqName:
+ case distinctName:
+ case TRUEName:
+ case FALSEName:
+ case "Array":
+ s = "nonkeyword_" + s;
+ break;
+ }
+
+ string! newS = "";
+ foreach (char ch in s) {
+ if (Char.IsLetterOrDigit(ch) || ch == '.' || ch == '\'' || ch == '_')
+ newS = newS + ch;
+ else
+ // replace everything else with a .
+ newS = newS + '.';
+ }
+
+ // ensure that the first character is not . or _ (some SMT-solvers do
+ // not like that, e.g., yices and cvc3)
+ if (newS[0] == '.' || newS[0] == '_')
+ newS = "x" + newS;
+
+ return newS;
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ /// <summary>
+ /// The name for logical conjunction in Simplify
+ /// </summary>
+ internal const string! andName = "and"; // conjunction
+ internal const string! orName = "or"; // disjunction
+ internal const string! notName = "not"; // negation
+ internal const string! impliesName = "implies"; // implication
+ internal const string! iffName = "iff"; // logical equivalence
+ internal const string! eqName = "="; // equality
+ internal const string! lessName = "<";
+ internal const string! greaterName = ">";
+ internal const string! atmostName = "<=";
+ internal const string! atleastName = ">=";
+ internal const string! TRUEName = "true"; // nullary predicate that is always true
+ internal const string! FALSEName = "false"; // nullary predicate that is always false
+ internal const string! subtypeName = "UOrdering2";
+ internal const string! subtypeArgsName = "UOrdering3";
+
+ internal const string! distinctName = "distinct";
+
+ internal const string! boolTrueName = "boolTrue";
+ internal const string! boolFalseName = "boolFalse";
+ internal const string! boolAndName = "boolAnd";
+ internal const string! boolOrName = "boolOr";
+ internal const string! boolNotName = "boolNot";
+ internal const string! boolIffName = "boolIff";
+ internal const string! boolImpliesName = "boolImplies";
+ internal const string! termUEqual = "UEqual";
+ internal const string! termTEqual = "TEqual";
+ internal const string! termIntEqual = "IntEqual";
+ internal const string! termLessName = "intLess";
+ internal const string! termGreaterName = "intGreater";
+ internal const string! termAtmostName = "intAtMost";
+ internal const string! termAtleastName = "intAtLeast";
+ internal const string! intAddName = "+";
+ internal const string! intSubName = "-";
+ internal const string! intMulName = "*";
+ internal const string! intDivName = "boogieIntDiv";
+ internal const string! intModName = "boogieIntMod";
+
+ internal void AssertAsTerm(string! x, LineariserOptions! options) {
+ if (!options.AsTerm)
+ System.Diagnostics.Debug.Fail("One should never write " + x + " as a formula!");
+ }
+
+ internal void AssertAsFormula(string! x, LineariserOptions! options) {
+ if (options.AsTerm)
+ System.Diagnostics.Debug.Fail("One should never write " + x + " as a term!");
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprLiteral! node, LineariserOptions! options) {
+ if (options.AsTerm) {
+
+ if (node == VCExpressionGenerator.True)
+ wr.Write("{0}", boolTrueName);
+ else if (node == VCExpressionGenerator.False)
+ wr.Write("{0}", boolFalseName);
+ else if (node is VCExprIntLit) {
+ // some SMT-solvers do not understand negative literals
+ // (e.g., yices)
+ BigNum lit = ((VCExprIntLit)node).Val;
+ if (lit.IsNegative)
+ wr.Write("({0} 0 {1})", intSubName, lit.Abs);
+ else
+ wr.Write(lit);
+ } else
+ assert false;
+
+ } else {
+
+ if (node == VCExpressionGenerator.True)
+ wr.Write("{0}", TRUEName);
+ else if (node == VCExpressionGenerator.False)
+ wr.Write("{0}", FALSEName);
+ else if (node is VCExprIntLit) {
+ System.Diagnostics.Debug.Fail("One should never write IntLit as a predicate!");
+ } else
+ assert false;
+
+ }
+
+ return true;
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprNAry! node, LineariserOptions! options) {
+ VCExprOp! op = node.Op;
+
+ if (!options.AsTerm &&
+ (op.Equals(VCExpressionGenerator.AndOp) ||
+ op.Equals(VCExpressionGenerator.OrOp))) {
+ // handle these operators without recursion
+
+ wr.Write("({0}",
+ op.Equals(VCExpressionGenerator.AndOp) ? andName : orName);
+ IEnumerator! enumerator = new VCExprNAryUniformOpEnumerator (node);
+ while (enumerator.MoveNext()) {
+ VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
+ if (naryExpr == null || !naryExpr.Op.Equals(op)) {
+ wr.Write(" ");
+ Linearise((VCExpr!)enumerator.Current, options);
+ }
+ }
+
+ wr.Write(")");
+
+ return true;
+ }
+
+ return node.Accept<bool, LineariserOptions!>(OpLineariser, options);
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprVar! node, LineariserOptions! options) {
+ string! printedName = Namer.GetName(node, MakeIdPrintable(node.Name));
+
+ if (options.AsTerm ||
+ // formula variables are easy to identify in SMT-Lib
+ printedName[0] == '$')
+ wr.Write("{0}", printedName);
+ else
+ wr.Write("({0} {1} {2})", eqName, printedName, boolTrueName);
+
+ return true;
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprQuantifier! node, LineariserOptions! options) {
+ AssertAsFormula(node.Quan.ToString(), options);
+ assert node.TypeParameters.Count == 0;
+
+ Namer.PushScope(); try {
+
+ string! kind = node.Quan == Quantifier.ALL ? "forall" : "exists";
+ wr.Write("({0} ", kind);
+
+ for (int i = 0; i < node.BoundVars.Count; i++)
+ {
+ VCExprVar! var = node.BoundVars[i];
+ // ensure that the variable name starts with ?
+ string! printedName = Namer.GetLocalName(var, "?" + MakeIdPrintable(var.Name));
+ assert printedName[0] == '?';
+ wr.Write("({0} {1}) ", printedName, TypeToString(var.Type));
+ }
+
+ /* if (options.QuantifierIds) {
+ // only needed for Z3
+ VCQuantifierInfos! infos = node.Infos;
+ if (infos.qid != null) {
+ wr.Write("(QID ");
+ wr.Write(infos.qid);
+ wr.Write(") ");
+ }
+ if (0 <= infos.uniqueId) {
+ wr.Write("(SKOLEMID ");
+ wr.Write(infos.uniqueId);
+ wr.Write(") ");
+ }
+ } */
+
+ Linearise(node.Body, options);
+
+ WriteTriggers(node.Triggers, options);
+ wr.Write(")");
+
+ return true;
+
+ } finally {
+ Namer.PopScope();
+ }
+ }
+
+ private void WriteTriggers(List<VCTrigger!>! triggers, LineariserOptions! options) {
+ // first, count how many neg/pos triggers there are
+ int negTriggers = 0;
+ int posTriggers = 0;
+ foreach (VCTrigger! vcTrig in triggers) {
+ if (vcTrig.Pos) {
+ posTriggers++;
+ } else {
+ negTriggers++;
+ }
+ }
+
+ if (posTriggers > 0) {
+ foreach (VCTrigger! vcTrig in triggers) {
+ if (vcTrig.Pos) {
+ wr.Write(" :pat {");
+ foreach (VCExpr! e in vcTrig.Exprs) {
+ wr.Write(" ");
+ LineariseAsTerm(e, options);
+ }
+ wr.Write(" } ");
+ }
+ }
+ } else if (negTriggers > 0) {
+ // if also positive triggers are given, the SMT solver (at least Z3)
+ // will ignore the negative patterns and output a warning. Therefore
+ // we never specify both negative and positive triggers
+ foreach (VCTrigger! vcTrig in triggers) {
+ if (!vcTrig.Pos) {
+ wr.Write(" :nopat { ");
+ assert vcTrig.Exprs.Count == 1;
+ wr.Write(" ");
+ LineariseAsTerm(vcTrig.Exprs[0], options);
+ wr.Write(" } ");
+ }
+ }
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprLet! node, LineariserOptions! options) {
+ Namer.PushScope(); try {
+
+ foreach (VCExprLetBinding! b in node) {
+ bool formula = b.V.Type.IsBool;
+
+ wr.Write("({0} (", formula ? "flet" : "let");
+ string! printedName = Namer.GetLocalName(b.V, "$" + MakeIdPrintable(b.V.Name));
+ assert printedName[0] == '$';
+
+ wr.Write("{0} ", printedName);
+ Linearise(b.E, options.SetAsTerm(!formula));
+ wr.Write(") ");
+ }
+ Linearise(node.Body, options);
+
+ for (int i = 0; i < node.Length; ++i)
+ wr.Write(")");
+
+ return true;
+
+ } finally {
+ Namer.PopScope();
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ // Lineariser for operator terms. The result (bool) is currently not used for anything
+ internal class SMTLibOpLineariser : IVCExprOpVisitor<bool, LineariserOptions!> {
+ private readonly SMTLibExprLineariser! ExprLineariser;
+ private readonly TextWriter! wr;
+
+ public SMTLibOpLineariser(SMTLibExprLineariser! ExprLineariser, TextWriter! wr) {
+ this.ExprLineariser = ExprLineariser;
+ this.wr = wr;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ private void WriteApplication(string! op, IEnumerable<VCExpr!>! args,
+ LineariserOptions! options,
+ bool argsAsTerms) {
+ WriteApplication(op, op, args, options, argsAsTerms);
+ }
+
+ private void WriteApplication(string! op, IEnumerable<VCExpr!>! args,
+ LineariserOptions! options) {
+ WriteApplication(op, op, args, options, options.AsTerm);
+ }
+
+ private void WriteTermApplication(string! op, IEnumerable<VCExpr!>! args,
+ LineariserOptions! options) {
+ ExprLineariser.AssertAsTerm(op, options);
+ WriteApplication(op, op, args, options, options.AsTerm);
+ }
+
+ private void WriteApplication(string! termOp, string! predOp,
+ IEnumerable<VCExpr!>! args, LineariserOptions! options) {
+ WriteApplication(termOp, predOp, args, options, options.AsTerm);
+ }
+
+ private void WriteApplication(string! termOp, string! predOp,
+ IEnumerable<VCExpr!>! args, LineariserOptions! options,
+ // change the AsTerm option for the arguments?
+ bool argsAsTerms) {
+ string! opName = options.AsTerm ? termOp : predOp;
+ LineariserOptions! newOptions = options.SetAsTerm(argsAsTerms);
+
+ bool hasArgs = false;
+ foreach (VCExpr! e in args) {
+ if (!hasArgs)
+ wr.Write("({0}", opName);
+ wr.Write(" ");
+ ExprLineariser.Linearise(e, newOptions);
+ hasArgs = true;
+ }
+
+ if (hasArgs)
+ wr.Write(")");
+ else
+ wr.Write("{0}", opName);
+ }
+
+ // write an application that can only be a term.
+ // if the expression is supposed to be printed as a formula,
+ // it is turned into an equation (EQ (f args) |@true|)
+ private void WriteApplicationTermOnly(string! termOp,
+ IEnumerable<VCExpr!>! args, LineariserOptions! options) {
+ if (!options.AsTerm)
+ // Write: (EQ (f args) |@true|)
+ // where "args" are written as terms
+ wr.Write("({0} ", eqName);
+
+ WriteApplication(termOp, args, options, true);
+
+ if (!options.AsTerm)
+ wr.Write(" {0})", boolTrueName);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ public bool VisitNotOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(boolNotName, notName, node, options); // arguments can be both terms and formulas
+ return true;
+ }
+
+ private bool PrintEq(VCExprNAry! node, LineariserOptions! options) {
+ if (options.AsTerm) {
+ // use equality on terms, also if the arguments have type bool
+ assert node[0].Type.Equals(node[1].Type);
+ if (node[0].Type.IsBool) {
+ WriteApplication(boolIffName, node, options);
+ } else if (node[0].Type.IsInt) {
+ WriteApplication(termIntEqual, node, options);
+ } else {
+ // TODO: make this less hackish
+ CtorType t = node[0].Type as CtorType;
+ if (t != null && t.Decl.Name.Equals("U")) {
+ WriteApplication(termUEqual, node, options);
+ } else if (t != null && t.Decl.Name.Equals("T")) {
+ WriteApplication(termTEqual, node, options);
+ } else {
+ assert false; // unknown type
+ }
+ }
+ } else {
+ if (node[0].Type.IsBool) {
+ assert node[1].Type.IsBool;
+ // use equivalence
+ WriteApplication(iffName, node, options);
+ } else {
+ // use equality and write the arguments as terms
+ WriteApplication(eqName, node, options, true);
+ }
+ }
+
+ return true;
+ }
+
+ public bool VisitEqOp (VCExprNAry! node, LineariserOptions! options) {
+ return PrintEq(node, options);
+ }
+
+ public bool VisitNeqOp (VCExprNAry! node, LineariserOptions! options) {
+ wr.Write("({0} ", options.AsTerm ? boolNotName : notName);
+ PrintEq(node, options);
+ wr.Write(")");
+ return true;
+ }
+
+ public bool VisitAndOp (VCExprNAry! node, LineariserOptions! options) {
+ assert options.AsTerm;
+ WriteApplication(boolAndName, andName, node, options);
+ return true;
+ }
+
+ public bool VisitOrOp (VCExprNAry! node, LineariserOptions! options) {
+ assert options.AsTerm;
+ WriteApplication(boolOrName, orName, node, options);
+ return true;
+ }
+
+ public bool VisitImpliesOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(boolImpliesName, impliesName, node, options);
+ return true;
+ }
+
+ public bool VisitDistinctOp (VCExprNAry! node, LineariserOptions! options) {
+ ExprLineariser.AssertAsFormula(distinctName, options);
+
+ if (node.Length < 2) {
+ ExprLineariser.Linearise(VCExpressionGenerator.True, options);
+ } else {
+ wr.Write("({0}", distinctName);
+ foreach (VCExpr! e in node) {
+ wr.Write(" ");
+ ExprLineariser.LineariseAsTerm(e, options);
+ }
+ wr.Write(")");
+ }
+
+ return true;
+ }
+
+ public bool VisitLabelOp (VCExprNAry! node, LineariserOptions! options) {
+ // VCExprLabelOp! op = (VCExprLabelOp)node.Op;
+ // TODO
+ // wr.Write(String.Format("({0} |{1}| ", op.pos ? "LBLPOS" : "LBLNEG", op.label));
+ ExprLineariser.Linearise(node[0], options);
+ // wr.Write(")");
+ return true;
+ }
+
+ public bool VisitSelectOp (VCExprNAry! node, LineariserOptions! options) {
+ assert false; // should not occur in the output
+ }
+
+ public bool VisitStoreOp (VCExprNAry! node, LineariserOptions! options) {
+ assert false; // should not occur in the output
+ }
+
+ public bool VisitBvOp (VCExprNAry! node, LineariserOptions! options) {
+ assert false; // TODO
+ }
+
+ public bool VisitBvExtractOp(VCExprNAry! node, LineariserOptions! options) {
+ assert false; // TODO
+ }
+
+ public bool VisitBvConcatOp (VCExprNAry! node, LineariserOptions! options) {
+ assert false; // TODO
+ }
+
+ public bool VisitAddOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteTermApplication(intAddName, node, options);
+ return true;
+ }
+
+ public bool VisitSubOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteTermApplication(intSubName, node, options);
+ return true;
+ }
+
+ public bool VisitMulOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteTermApplication(intMulName, node, options);
+ return true;
+ }
+
+ public bool VisitDivOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteTermApplication(intDivName, node, options);
+ return true;
+ }
+
+ public bool VisitModOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteTermApplication(intModName, node, options);
+ return true;
+ }
+
+ public bool VisitLtOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(termLessName, lessName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitLeOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(termAtmostName, atmostName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitGtOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(termGreaterName, greaterName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitGeOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(termAtleastName, atleastName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitSubtypeOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(subtypeName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitSubtype3Op (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(subtypeArgsName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitBoogieFunctionOp (VCExprNAry! node, LineariserOptions! options) {
+ VCExprBoogieFunctionOp! op = (VCExprBoogieFunctionOp)node.Op;
+ string! printedName = ExprLineariser.Namer.GetName(op.Func, MakeIdPrintable(op.Func.Name));
+
+ // arguments are always terms
+ WriteApplicationTermOnly(printedName, node, options);
+ return true;
+ }
+
+ }
+ }
+
+}
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.ssc b/Source/Provers/SMTLib/TypeDeclCollector.ssc new file mode 100644 index 00000000..08c0e6a3 --- /dev/null +++ b/Source/Provers/SMTLib/TypeDeclCollector.ssc @@ -0,0 +1,107 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.SMTLib
+{
+ // Visitor for collecting the occurring function symbols in a VCExpr,
+ // and for creating the corresponding declarations
+
+ public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
+
+ private readonly UniqueNamer! Namer;
+
+ public TypeDeclCollector(UniqueNamer! namer) {
+ this.Namer = namer;
+ }
+
+ // not used
+ protected override bool StandardResult(VCExpr! node, bool arg) {
+ return true;
+ }
+
+ private readonly List<string!>! AllDecls = new List<string!> ();
+ private readonly List<string!>! IncDecls = new List<string!> ();
+
+ private readonly IDictionary<Function!, bool>! KnownFunctions =
+ new Dictionary<Function!, bool> ();
+ private readonly IDictionary<VCExprVar!, bool>! KnownVariables =
+ new Dictionary<VCExprVar!, bool> ();
+
+ public List<string!>! AllDeclarations { get {
+ List<string!>! res = new List<string!> ();
+ res.AddRange(AllDecls);
+ return res;
+ } }
+
+ public List<string!>! GetNewDeclarations() {
+ List<string!>! res = new List<string!> ();
+ res.AddRange(IncDecls);
+ IncDecls.Clear();
+ return res;
+ }
+
+ private void AddDeclaration(string! decl) {
+ AllDecls.Add(decl);
+ IncDecls.Add(decl);
+ }
+
+ public void Collect(VCExpr! expr) {
+ Traverse(expr, true);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+
+ private static string! TypeToString(Type! t) {
+ return SMTLibExprLineariser.TypeToString(t);
+ }
+
+ public override bool Visit(VCExprNAry! node, bool arg) {
+ // there are a couple of cases where operators have to be
+ // registered by generating appropriate statements
+
+ VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;
+ if (op != null && !KnownFunctions.ContainsKey(op.Func)) {
+ Function! f = op.Func;
+ string! printedName = Namer.GetName(f, SMTLibExprLineariser.MakeIdPrintable(f.Name));
+ string! decl = ":extrafuns ((" + printedName;
+
+ foreach (Variable! v in f.InParams) {
+ decl += " " + TypeToString(v.TypedIdent.Type);
+ }
+ assert f.OutParams.Length == 1;
+ foreach (Variable! v in f.OutParams) {
+ decl += " " + TypeToString(v.TypedIdent.Type);
+ }
+
+ decl += "))";
+
+ AddDeclaration(decl);
+ KnownFunctions.Add(f, true);
+ }
+
+ return base.Visit(node, arg);
+ }
+
+ public override bool Visit(VCExprVar! node, bool arg) {
+ if (!BoundTermVars.Contains(node) && !KnownVariables.ContainsKey(node)) {
+ string! printedName = Namer.GetName(node, SMTLibExprLineariser.MakeIdPrintable(node.Name));
+ string! decl =
+ ":extrafuns ((" + printedName + " " + TypeToString(node.Type) + "))";
+ AddDeclaration(decl);
+ KnownVariables.Add(node, true);
+ }
+
+ return base.Visit(node, arg);
+ }
+ }
+
+}
\ No newline at end of file diff --git a/Source/Provers/Simplify/Let2ImpliesVisitor.ssc b/Source/Provers/Simplify/Let2ImpliesVisitor.ssc new file mode 100644 index 00000000..8443d950 --- /dev/null +++ b/Source/Provers/Simplify/Let2ImpliesVisitor.ssc @@ -0,0 +1,183 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.Simplify
+{
+ // Simplify does not understand the LET operator, so we have to replace
+ // it with implications (previously, this was done in the VCExprGenerator), or
+ // we have to apply the let as a substitution (in the case of terms)
+
+ // This visitor expects that let-bindings are sorted, so that bound
+ // variables only occur after their declaration
+
+ public class Let2ImpliesMutator : SubstitutingVCExprVisitor {
+
+ public Let2ImpliesMutator(VCExpressionGenerator! gen) {
+ base(gen);
+ }
+
+ public VCExpr! Mutate(VCExpr! expr) {
+ return Mutate(expr, new VCExprSubstitution ());
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ private int polarity = 1; // 1 for positive, -1 for negative, 0 for both
+
+ // we also track which variables occur in positive, negative, or
+ // in both positions (to decide whether implications or equations
+ // have to be used to define such a variable)
+ private enum OccurrenceTypes { None, Pos, Neg, PosNeg };
+ private OccurrenceTypes Union(OccurrenceTypes o1, OccurrenceTypes o2) {
+ switch(o1) {
+ case OccurrenceTypes.None: return o2;
+ case OccurrenceTypes.Pos:
+ switch(o2) {
+ case OccurrenceTypes.None:
+ case OccurrenceTypes.Pos:
+ return OccurrenceTypes.Pos;
+ default:
+ return OccurrenceTypes.PosNeg;
+ }
+ case OccurrenceTypes.Neg:
+ switch(o2) {
+ case OccurrenceTypes.None:
+ case OccurrenceTypes.Neg:
+ return OccurrenceTypes.Neg;
+ default:
+ return OccurrenceTypes.PosNeg;
+ }
+ default:
+ return OccurrenceTypes.PosNeg;
+ }
+ }
+
+ private IDictionary<VCExprVar!, OccurrenceTypes>! VarOccurrences =
+ new Dictionary<VCExprVar!, OccurrenceTypes>();
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public override VCExpr! Visit(VCExprVar! node,
+ VCExprSubstitution! substitution) {
+ VCExpr! res = base.Visit(node, substitution);
+
+ VCExprVar resAsVar = res as VCExprVar;
+ if (resAsVar != null) {
+ OccurrenceTypes occ;
+ if (polarity > 0)
+ occ = OccurrenceTypes.Pos;
+ else if (polarity < 0)
+ occ = OccurrenceTypes.Neg;
+ else
+ occ = OccurrenceTypes.PosNeg;
+
+ OccurrenceTypes oldOcc;
+ if (VarOccurrences.TryGetValue(resAsVar, out oldOcc))
+ occ = Union(occ, oldOcc);
+ VarOccurrences[resAsVar] = occ;
+ }
+
+ return res;
+ }
+
+ public override VCExpr! Visit(VCExprNAry! node,
+ VCExprSubstitution! substitution) {
+ // track the polarity to ensure that no implications are introduced
+ // in negative positions
+ // UGLY: the code for tracking polarities should be factored out
+ // (similar code is used in the TypeEraser)
+
+ VCExpr! res;
+ if (node.Op.Equals(VCExpressionGenerator.NotOp)) {
+ polarity = -polarity;
+ res = base.Visit(node, substitution);
+ polarity = -polarity;
+ } else if (node.Op.Equals(VCExpressionGenerator.ImpliesOp)) {
+ polarity = -polarity;
+ VCExpr! newArg0 = Mutate(node[0], substitution);
+ polarity = -polarity;
+ VCExpr! newArg1 = Mutate(node[1], substitution);
+
+ res = Gen.Implies(newArg0, newArg1);
+ } else if (!node.Op.Equals(VCExpressionGenerator.AndOp) &&
+ !node.Op.Equals(VCExpressionGenerator.OrOp) &&
+ !(node.Op is VCExprLabelOp)) {
+ // standard is to set the polarity to 0 (fits most operators)
+ int oldPolarity = polarity;
+ polarity = 0;
+ res = base.Visit(node, substitution);
+ polarity = oldPolarity;
+ } else {
+ res = base.Visit(node, substitution);
+ }
+
+ return res;
+ }
+
+ public override VCExpr! Visit(VCExprLet! originalNode,
+ VCExprSubstitution! substitution) {
+ // first sort the bindings to be able to apply substitutions
+ LetBindingSorter! letSorter = new LetBindingSorter (Gen);
+ VCExpr! newNode = letSorter.Mutate(originalNode, true);
+ VCExprLet node = newNode as VCExprLet;
+
+ if (node == null)
+ // it can happen that the complete let-expressions gets eliminated by the
+ // sorter, which also checks whether let-bindings are actually used
+ return newNode;
+
+ substitution.PushScope(); try {
+
+ // the bindings that remain and that are later handled using an implication
+ List<VCExprLetBinding!>! bindings = new List<VCExprLetBinding!> ();
+
+ foreach (VCExprLetBinding! binding in node) {
+ // in all cases we apply the substitution up to this point
+ // to the bound formula
+ VCExpr! newE = Mutate(binding.E, substitution);
+
+ if (binding.V.Type.IsBool) {
+ // a bound formula is handled using an implication; we introduce
+ // a fresh variable to avoid clashes
+ assert polarity > 0;
+
+ VCExprVar! newVar = Gen.Variable(binding.V.Name, Type.Bool);
+ substitution[binding.V] = newVar;
+
+ bindings.Add(Gen.LetBinding(newVar, newE));
+ } else {
+ // a bound term is substituted
+ substitution[binding.V] = newE;
+ }
+ }
+
+ VCExpr! newBody = Mutate(node.Body, substitution);
+
+ // Depending on the places where the variable occurs, we would
+ // have to introduce implications or equations to define the
+ // bound variables. For the time being, we just assert that all
+ // occurrences are positive
+ foreach (VCExprLetBinding! b in bindings) {
+ OccurrenceTypes occ;
+ if (VarOccurrences.TryGetValue(b.V, out occ))
+ assert occ == OccurrenceTypes.None || occ == OccurrenceTypes.Pos;
+ }
+
+ return Gen.Implies(Gen.AsImplications(bindings), newBody);
+
+ } finally {
+ substitution.PopScope();
+ }
+ }
+ }
+
+}
\ No newline at end of file diff --git a/Source/Provers/Simplify/Prover.ssc b/Source/Provers/Simplify/Prover.ssc new file mode 100644 index 00000000..f89d6a42 --- /dev/null +++ b/Source/Provers/Simplify/Prover.ssc @@ -0,0 +1,606 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.IO;
+using System.Diagnostics;
+using System.Collections;
+using System.Collections.Generic;
+using util;
+using Microsoft.Contracts;
+using Microsoft.Boogie;
+
+// Simplified interface to an external prover like Simplify or the z3 process, taken from Bird.
+namespace Microsoft.Boogie.Simplify
+{
+ /// <summary>
+ /// An interface to Simplify theorem prover.
+ /// </summary>
+ public abstract class ProverProcess
+ {
+ [Rep]
+ protected readonly Process! simplify;
+
+ [Rep] readonly TextReader! fromSimplify;
+ [Rep] readonly TextWriter! toSimplify;
+ [Rep] readonly TextReader! fromStdError;
+
+ protected bool readTimedOut;
+
+ int nFormulasChecked = 0;
+ public int NumFormulasChecked {
+ get { return nFormulasChecked; }
+ }
+
+ // Note: In the Everett build (.NET framework < 2.0), Process.PeakVirtualMemorySize64
+ // is not defined, but rather a version that returns an 'int' rather than a 'long'.
+ public long PeakVirtualMemorySize {
+ [NoDefaultContract]
+ get
+ requires IsPeerConsistent;
+ modifies this.*;
+ {
+ expose (this) {
+ simplify.Refresh();
+#if WHIDBEY
+ return simplify.PeakVirtualMemorySize64;
+#else
+ return simplify.PeakPagedMemorySize64;
+#endif
+ }
+ }
+ }
+
+ public bool HasExited {
+ get { return simplify.HasExited; }
+ }
+
+ public ProverProcess(ProcessStartInfo! psi, string! proverPath)
+ { // throws ProverException
+ try
+ {
+ Process simplify = Process.Start(psi);
+ this.simplify = simplify;
+ fromSimplify = simplify.StandardOutput;
+ toSimplify = simplify.StandardInput;
+ fromStdError = simplify.StandardError;
+ }
+ catch (System.ComponentModel.Win32Exception e)
+ {
+ throw new ProverException(string.Format("Unable to start the process {0}: {1}", proverPath, e.Message));
+ }
+ // base();
+ }
+
+ public abstract string! OptionComments();
+ [Pure(false)]
+ public virtual IEnumerable<string!>! ParameterSettings { get { yield break; } }
+
+ public void Close()
+ modifies this.*;
+ {
+ expose (this) {
+ toSimplify.Flush();
+ if (this.simplify != null)
+ {
+ if (!simplify.HasExited)
+ {
+ this.Kill();
+ }
+ simplify.Close();
+ }
+ }
+ }
+
+ [NoDefaultContract] // this method assumes nothing about the object, other than that it has been constructed (which means simplify!=null)
+ [Verify(false)] // The call simplify.Kill will require simplify.IsPeerConsistent, but since we don't know the state of "this" and "simplify", we cannot afford the run-time check that an assume statement here would impose
+ public void Kill() {
+ try {
+ if (CommandLineOptions.Clo.ProverShutdownLimit > 0) {
+ toSimplify.Close();
+ for (int i = 0; !simplify.HasExited && i <= CommandLineOptions.Clo.ProverShutdownLimit * 1000; i += 100)
+ {
+ System.Threading.Thread.Sleep(100);
+ }
+ }
+ if (!simplify.HasExited) { simplify.Kill(); }
+ } catch (InvalidOperationException) { /* already exited */ }
+ catch (System.ComponentModel.Win32Exception) { /* already exiting */ }
+ }
+
+ public static void ReportWarning(string! w)
+ modifies Console.Out.*, Console.Error.*;
+ {
+ switch (CommandLineOptions.Clo.PrintProverWarnings) {
+ case CommandLineOptions.ProverWarnings.None:
+ break;
+ case CommandLineOptions.ProverWarnings.Stdout:
+ Console.WriteLine("Prover warning: " + w);
+ break;
+ case CommandLineOptions.ProverWarnings.Stderr:
+ Console.Error.WriteLine("Prover warning: " + w);
+ break;
+ default:
+ assume false; // unexpected case
+ }
+ }
+
+ public virtual void AddAxioms(string! s)
+ modifies this.*;
+ modifies Console.Out.*, Console.Error.*;
+ throws UnexpectedProverOutputException;
+ {
+ expose (this) {
+ toSimplify.Write("(BG_PUSH ");
+ toSimplify.Write(s);
+ toSimplify.WriteLine(")");
+ }
+ }
+
+ public virtual void Feed(string! s, int statementCount)
+ modifies this.*;
+ modifies Console.Out.*, Console.Error.*;
+ throws UnexpectedProverOutputException;
+ {
+ expose (this) {
+ toSimplify.Write(s);
+ }
+ }
+
+ public virtual void PopAxioms()
+ modifies this.*;
+ modifies Console.Out.*, Console.Error.*;
+ throws UnexpectedProverOutputException;
+ {
+ expose (this) {
+ toSimplify.WriteLine("(BG_POP)");
+ }
+ }
+
+ public void ToFlush()
+ modifies this.*;
+ {
+ expose (this) {
+ toSimplify.Flush();
+ }
+ }
+
+ public enum ProverOutcome { Valid, NotValid, TimeOut, OutOfMemory, Inconclusive }
+
+ /// <summary>
+ /// Passes the formula to Simplify.
+ /// </summary>
+ public void BeginCheck(string! descriptiveName, string! formula)
+ modifies this.*;
+ modifies Console.Out.*, Console.Error.*;
+ {
+ DoBeginCheck(descriptiveName, formula);
+ nFormulasChecked++;
+ }
+
+ /// <summary>
+ /// Reports the outcome of formula checking. If the outcome is Invalid,
+ /// then the "handler" is invoked with each counterexample.
+ /// </summary>
+ public abstract ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler! handler)
+ modifies this.**;
+ modifies Console.Out.*, Console.Error.*;
+ modifies handler.*;
+ throws UnexpectedProverOutputException;
+
+ protected abstract void DoBeginCheck(string! descriptiveName, string! formula)
+ modifies this.*;
+ modifies Console.Out.*, Console.Error.*;
+
+ /// <summary>
+ /// Returns an array of the labels in "labels", with "|" brackets (if any)
+ /// stripped off.
+ /// Assumes that every label begins with "|+" or "|@", or just "+" or "@",
+ /// and ends with "|" if it started with one, and that these "|" brackets are
+ /// the only "|"s in "labels".
+ /// </summary>
+ protected static List<string!>! ParseLabels(string! labels)
+ {
+ List<string!> list = new List<string!>();
+ int j = 0;
+ while (true)
+ // invariant: j is the number of characters of "labels" consumed so far
+ // invariant: an even number of '|' characters remain in "labels"
+ invariant 0 <= j && j <= labels.Length;
+ {
+ j = labels.IndexOfAny(new char[]{'|', '+', '@'}, j);
+ if (j < 0) {
+ // no more labels
+ return list;
+ }
+ char ch = labels[j];
+ if (ch == '|') {
+ j++; // skip the '|'
+ assume j < labels.Length; // there should now be a '+' or '@'
+ ch = labels[j];
+ }
+ assume ch == '+' || ch == '@';
+ j++; // skip the '+' or '@'
+ int k = labels.IndexOfAny(new char[]{'|', ' ', ')'}, j);
+ assume j+2 <= k;
+ string s = labels.Substring(j, k-j);
+ list.Add(s);
+ j = k+1;
+ }
+ }
+
+ [Rep] char[] expectBuffer = null;
+
+ /// <summary>
+ /// Expects s[0]==ch and the next s.Length-1 characters of the input to be s[1,..]
+ /// If not, more characters may be read from "fromSimplify" to provide additional context
+ /// for the UnexpectedProverOutputException exception that will be thrown.
+ /// </summary>
+ protected void Expect(int ch, string! s)
+ requires 1 <= s.Length;
+ modifies this.*;
+ throws UnexpectedProverOutputException;
+ {
+ if (ch == -1) {
+ // a return of -1 from FromReadChar means that there is no StdOutput
+ // to treat this we can return the error message we get from Z3 on StdError and then
+ // declare this case to be inconclusive
+ string str = FromStdErrorAll();
+ if (str == "") {
+ throw new ProverDiedException();
+ } else {
+ throw new UnexpectedProverOutputException("Expected \"" + s + "\", found:\r\n<<<start>>>\r\n" + str + "<<<end>>>");
+ }
+ }
+
+ string badInputPrefix;
+ if (ch != s[0])
+ {
+ badInputPrefix = Char.ToString((char)ch);
+ }
+ else
+ {
+ int len = s.Length - 1;
+ if (expectBuffer == null || expectBuffer.Length < len)
+ {
+ expose (this) {
+ expectBuffer = new char[len];
+ }
+ }
+ try
+ {
+ string s0;
+ expose (this) {
+ fromSimplify.ReadBlock(expectBuffer, 0, len);
+ s0 = new string(expectBuffer, 0, len);
+ }
+ string s1 = s.Substring(1, len);
+ if (s0.CompareTo(s1) == 0)
+ {
+ badInputPrefix = null; // no error
+ }
+ else
+ {
+ badInputPrefix = (char)ch + s0;
+ }
+ }
+ catch (IOException)
+ {
+ throw new UnexpectedProverOutputException("Expected \"" + s + "\", encountered IO exception.");
+ }
+ }
+
+ if (badInputPrefix != null)
+ {
+ // Read the rest of the available input, without blocking!
+ // Despite the confusing documentation for the Read method, it seems
+ // that Read does block. It if didn't, I would have written:
+ // string remaining = "";
+ // char[] buf = new char[1024];
+ // while (true) {
+ // int len = fromSimplify.Read(buf, 0, buf.Length);
+ // remaining += new String(buf, 0, len);
+ // if (len != buf.Length) {
+ // break;
+ // }
+ // }
+ // But instead, I'll just hope that one line of input is available and read
+ // it.
+ string remaining = fromSimplify.ReadLine() + "\r\n";
+ throw new UnexpectedProverOutputException("Expected \"" + s + "\", found:\r\n<<<start>>>\r\n" + badInputPrefix + remaining + "<<<end>>>");
+ }
+ }
+
+ protected int FromReadChar()
+ modifies this.*;
+ {
+ expose (this) {
+ return fromSimplify.Read();
+ }
+ }
+
+ private void KillProver(object state)
+ {
+ expose (this) {
+ this.readTimedOut = true;
+ simplify.Kill();
+ }
+ }
+
+ protected int FromReadChar(int timeout)
+ requires -1 <= timeout;
+ modifies this.*;
+ {
+ expose (this) {
+ this.readTimedOut = false;
+ System.Threading.Timer t = new System.Threading.Timer(this.KillProver, null, timeout, System.Threading.Timeout.Infinite);
+ int ch = fromSimplify.Read();
+ t.Change(System.Threading.Timeout.Infinite, System.Threading.Timeout.Infinite);
+ t.Dispose();
+ return ch;
+ }
+ }
+
+ protected string! FromReadLine()
+ modifies this.*;
+ {
+ expose (this) {
+ string s = fromSimplify.ReadLine();
+ if (s == null) {
+ // this is what ReadLine returns if all characters have been read
+ s = "";
+ }
+ return s;
+ }
+ }
+
+ protected string! FromStdErrorAll ()
+ modifies this.*;
+ {
+ expose (this) {
+ if (fromStdError != null) {
+ string s = fromStdError.ReadToEnd();
+ if (s == null) {
+ // this is what ReadLine returns if all characters have been read
+ s = "";
+ }
+ return s;
+ }
+ // there is no StdErrorReader available
+ else {
+ return "";
+ }
+ }
+ }
+
+ protected void ToWriteLine(string! s)
+ modifies this.*;
+ {
+ expose (this) {
+ toSimplify.WriteLine(s);
+ }
+ }
+ }
+
+ // derived by Z3ProverProcess
+ public class SimplifyProverProcess : ProverProcess {
+ public SimplifyProverProcess(string! proverPath, bool dummy)
+ { // throws ProverException
+ ProcessStartInfo psi = new ProcessStartInfo(proverPath, "-labelsonly");
+ psi.CreateNoWindow = true;
+ psi.UseShellExecute = false;
+ psi.RedirectStandardInput = true;
+ psi.RedirectStandardOutput = true;
+ psi.RedirectStandardError = true;
+ assume psi.EnvironmentVariables != null; // by inspecting the code through Reflector; the documentation says this property is "null by default", whatever that means --KRML
+ if (0 <= CommandLineOptions.Clo.ProverKillTime) {
+ psi.EnvironmentVariables["PROVER_KILL_TIME"] = CommandLineOptions.Clo.ProverKillTime.ToString();
+ }
+ if (0 <= CommandLineOptions.Clo.SimplifyProverMatchDepth) {
+ psi.EnvironmentVariables["PROVER_MATCH_DEPTH"] = CommandLineOptions.Clo.SimplifyProverMatchDepth.ToString();
+ }
+ if (0 <= CommandLineOptions.Clo.ProverCCLimit) {
+ psi.EnvironmentVariables["PROVER_CC_LIMIT"] = CommandLineOptions.Clo.ProverCCLimit.ToString();
+ }
+
+ base(psi, proverPath);
+ }
+
+ public override string! OptionComments()
+ {
+ // would we want the timeout stuff here?
+ return "";
+ }
+
+ [NotDelayed]
+ // TODO it complains about things not beeing peer consistent upon call to EatPrompt()
+ // not sure what is it about... --micmo
+ [Verify(false)]
+ public SimplifyProverProcess(string! proverPath)
+ modifies Console.Out.*, Console.Error.*;
+ throws UnexpectedProverOutputException;
+ {
+ this(proverPath, true);
+ EatPrompt();
+ }
+
+ private void EatPrompt()
+ modifies this.*;
+ modifies Console.Out.*, Console.Error.*;
+ throws UnexpectedProverOutputException;
+ {
+ // skips text matching the regular expression: (white space)* ">\t"
+ ToFlush();
+
+ int ch = 0;
+ do {
+ ch = FromReadChar();
+ } while (Char.IsWhiteSpace((char)ch));
+
+ while (ch == 'W') {
+ ch = ConsumeWarnings(ch);
+ }
+
+ Expect(ch, ">\t");
+ }
+
+ public override void AddAxioms(string! s)
+ throws UnexpectedProverOutputException;
+ {
+ //ToWriteLine("(PROMPT_OFF)");
+ base.AddAxioms(s);
+ //ToWriteLine("(PROMPT_ON)");
+ EatPrompt();
+ }
+
+ public override void Feed(string! s, int statementCount)
+ throws UnexpectedProverOutputException;
+ {
+ //ToWriteLine("(PROMPT_OFF)");
+ base.Feed(s, statementCount);
+ //ToWriteLine("(PROMPT_ON)");
+ for (int i = 0; i < statementCount; i++) {
+ EatPrompt();
+ }
+ }
+
+ public override void PopAxioms()
+ throws UnexpectedProverOutputException;
+ {
+ base.PopAxioms();
+ EatPrompt();
+ }
+
+ protected override void DoBeginCheck(string! descriptiveName, string! formula)
+ {
+ //simplify.Refresh();
+ //this.Comment("@@@@ Virtual Memory: " + simplify.PeakVirtualMemorySize64);
+ //this.Comment("@@@@ Working Set: " + simplify.PeakWorkingSet64);
+ //this.Comment("@@@@ Paged Memory: " + simplify.PeakPagedMemorySize64);
+
+ ToWriteLine(formula);
+ ToFlush();
+ }
+
+ public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler! handler)
+ throws UnexpectedProverOutputException;
+ {
+ ProverOutcome outcome;
+
+ if (this.simplify == null) {
+ return ProverOutcome.Inconclusive;
+ }
+
+ int ch = FromReadChar();
+ while (ch == 'W')
+ {
+ ch = ConsumeWarnings(ch);
+ }
+ if (ch == 'E')
+ {
+ Expect(ch, "Exceeded PROVER_KILL_TIME -- discontinuing search for counterexamples.");
+ FromReadLine();
+ ch = FromReadChar();
+ if (ch == '\n')
+ {
+ ch = FromReadChar();
+ }
+ Expect(ch, " labels:");
+ FromReadLine();
+ ch = FromReadChar();
+ ch = FromReadChar();
+ ch = FromReadChar();
+ FromReadLine();
+ ch = FromReadChar();
+ ch = FromReadChar();
+ ch = FromReadChar();
+ return ProverOutcome.TimeOut;
+ }
+ if ('0' <= ch && ch <= '9')
+ {
+ // Valid!
+ do {
+ ch = FromReadChar();
+ } while ('0' <= ch && ch <= '9');
+ Expect(ch, ": Valid.");
+ outcome = ProverOutcome.Valid;
+ ToWriteLine(String.Format("; FORMULA {0} IS VALID!", NumFormulasChecked + 1 /*Simplify starts at 1*/));
+ }
+ else
+ {
+ // now we expect one or more counterexample contexts, each proving a list of labels
+ do {
+ List<string!> labels = ReadLabels(ch);
+ handler.OnModel(labels, null);
+ ch = FromReadChar();
+ } while (ch == 'C');
+ // now we expect "<N>: Invalid" where <N> is some number
+ while ('0' <= ch && ch <= '9')
+ {
+ ch = FromReadChar();
+ }
+ Expect(ch, ": Invalid.");
+ outcome = ProverOutcome.NotValid;
+ ToWriteLine(String.Format("; FORMULA {0} IS INVALID", NumFormulasChecked + 1 /*Simplify starts at 1*/));
+ }
+
+ EatPrompt();
+ return outcome;
+ }
+
+ List<string!>! ReadLabels(int ch)
+ modifies this.*;
+ throws UnexpectedProverOutputException;
+ {
+ Expect(ch, "Counterexample:\n"); // FIX! ? Is there a problem with \r\n here?
+ ch = FromReadChar();
+ List<string!> theLabels;
+ if (ch == ' ')
+ {
+ // there are labels
+ Expect(ch, " labels: ");
+ string labels = FromReadLine(); // reads "(A B C ...)\n"
+ theLabels = ParseLabels(labels);
+ ch = FromReadChar();
+ }
+ else
+ {
+ theLabels = new List<string!>();
+ }
+ Expect(ch, "\n"); // empty line
+
+ return theLabels;
+ }
+
+ int ConsumeWarnings(int ch)
+ requires ch == 'W';
+ modifies this.*;
+ modifies Console.Out.*, Console.Error.*;
+ throws UnexpectedProverOutputException;
+ {
+ Expect(ch, "Warning: ");
+ string w = FromReadLine();
+ if (w.StartsWith("triggerless quantifier body")) {
+ FromReadLine(); // blank line
+ w = "triggerless quantifier body: " + FromReadLine(); // expression (body)
+ FromReadLine(); // blank line
+ FromReadLine(); // "with X pattern variable(s)...
+ FromReadLine(); // blank line
+ FromReadLine(); // expression (entire quantifier)
+ }
+ ReportWarning(w);
+ ch = FromReadChar();
+ if (ch == '\n')
+ {
+ // make up for a poorly designed ReadLine routine (only the first
+ // character of the DOS end-of-line sequence "\r\n" is read)
+ ch = FromReadChar();
+ }
+ return ch;
+ }
+ }
+
+}
+
diff --git a/Source/Provers/Simplify/ProverInterface.ssc b/Source/Provers/Simplify/ProverInterface.ssc new file mode 100644 index 00000000..df7f86d6 --- /dev/null +++ b/Source/Provers/Simplify/ProverInterface.ssc @@ -0,0 +1,633 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie.Simplify;
+using Microsoft.Boogie.VCExprAST;
+using Microsoft.Boogie.TypeErasure;
+
+namespace Microsoft.Boogie.Simplify
+{
+ public abstract class LogProverInterface : ProverInterface
+ {
+ [NotDelayed]
+ protected LogProverInterface(ProverOptions! options,
+ string! openComment, string! closeComment,
+ string! openActivity, string! closeActivity,
+ VCExpressionGenerator! gen)
+ ensures this.gen == gen;
+ {
+ if (options.SeparateLogFiles) {
+ this.commonPrefix = new List<string!> ();
+ } else {
+ this.logFileWriter = options.OpenLog(null);
+ }
+ this.openCommentString = openComment;
+ this.closeCommentString = closeComment;
+ this.openActivityString = openActivity;
+ this.closeActivityString = closeActivity;
+ this.gen = gen;
+ this.options = options;
+ base();
+
+ if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never) {
+ // Emit version comment in the log
+ LogCommonComment(CommandLineOptions.Clo.Version);
+ LogCommonComment(CommandLineOptions.Clo.Environment);
+ }
+ }
+
+ [StrictReadonly][Additive]
+ protected readonly VCExpressionGenerator! gen;
+
+ private TextWriter/*?*/ logFileWriter;
+ [Microsoft.Contracts.StrictReadonly]
+ private readonly string! openCommentString;
+ [Microsoft.Contracts.StrictReadonly]
+ private readonly string! closeCommentString;
+ [Microsoft.Contracts.StrictReadonly]
+ private readonly string! openActivityString;
+ [Microsoft.Contracts.StrictReadonly]
+ private readonly string! closeActivityString;
+ [Microsoft.Contracts.StrictReadonly]
+ protected readonly ProverOptions! options;
+ [Microsoft.Contracts.StrictReadonly]
+ private readonly List<string!>/*?*/ commonPrefix;
+
+ public void LogActivity(string! s) {
+ LogActivity(s, false);
+ }
+
+ public void LogCommon(string! s) {
+ LogActivity(s, true);
+ }
+
+ private void LogActivity(string! s, bool common) {
+ assume common || !options.SeparateLogFiles || logFileWriter != null;
+ if (logFileWriter != null) {
+ logFileWriter.Write(openActivityString);
+ logFileWriter.Write(s);
+ logFileWriter.WriteLine(closeActivityString);
+ logFileWriter.Flush();
+ }
+ if (common && commonPrefix != null) {
+ commonPrefix.Add(openActivityString + s + closeActivityString);
+ }
+ }
+
+ /// <summary>
+ /// Write "comment" to logfile, if any, formatted as a comment for the theorem prover at hand.
+ /// Assumes that "comment" does not contain any characters that would prematurely terminate
+ /// the comment (like, perhaps, a newline or "*/").
+ /// </summary>
+ public override void LogComment(string! comment)
+ {
+ LogComment(comment, false);
+ }
+
+ public void LogCommonComment(string! comment)
+ {
+ LogComment(comment, true);
+ }
+
+ private void LogComment(string! comment, bool common)
+ {
+ assume common || !options.SeparateLogFiles || logFileWriter != null;
+ if (logFileWriter != null) {
+ logFileWriter.Write(openCommentString);
+ logFileWriter.Write(comment);
+ logFileWriter.WriteLine(closeCommentString);
+ logFileWriter.Flush();
+ }
+ if (common && commonPrefix != null) {
+ commonPrefix.Add(openCommentString + comment + closeCommentString);
+ }
+ }
+
+ public virtual void NewProblem(string! descName)
+ {
+ if (commonPrefix != null) {
+ if (logFileWriter != null) {
+ logFileWriter.Close();
+ }
+ logFileWriter = options.OpenLog(descName);
+ if (logFileWriter != null) {
+ foreach (string! s in commonPrefix)
+ logFileWriter.WriteLine(s);
+ }
+ }
+ LogComment("Proof obligation: " + descName);
+ }
+
+ public override void Close() {
+ if (logFileWriter != null) {
+ logFileWriter.Close();
+ logFileWriter = null;
+ }
+ }
+
+ public override VCExpressionGenerator! VCExprGen
+ {
+ get { return this.gen; }
+ }
+ }
+
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+
+ public abstract class ProcessTheoremProver : LogProverInterface
+ {
+ private static string! _proverPath;
+
+ protected AxiomVCExprTranslator! vcExprTranslator { get {
+ return (AxiomVCExprTranslator!)ctx.exprTranslator;
+ } }
+
+ protected abstract AxiomVCExprTranslator! SpawnVCExprTranslator();
+
+ protected void FeedNewAxiomsDecls2Prover() throws UnexpectedProverOutputException; {
+ if (thmProver == null)
+ return;
+ foreach (string! s in vcExprTranslator.NewTypeDecls) {
+ LogCommon(s);
+ thmProver.Feed(s, 0);
+ }
+ foreach (string! s in vcExprTranslator.NewAxioms) {
+ LogBgPush(s);
+ thmProver.AddAxioms(s);
+ }
+ }
+
+ protected static string! CodebaseString() {
+ return Path.GetDirectoryName((!)System.Reflection.Assembly.GetExecutingAssembly().Location);
+ }
+
+ private static IDictionary<string!, string!>! BackgroundPredicates =
+ new Dictionary<string!, string!> ();
+
+ protected static string! GetBackgroundPredicate(string! filename) {
+ string res;
+ if (!BackgroundPredicates.TryGetValue(filename, out res)) {
+ // do we have to lock/synchronise anything?
+ string univBackPredPath = Path.Combine(CodebaseString(), filename);
+ using (StreamReader reader = new System.IO.StreamReader(univBackPredPath))
+ {
+ res = reader.ReadToEnd();
+ }
+ BackgroundPredicates.Add(filename, res);
+ }
+ return (!)res;
+ }
+
+ static void InitializeGlobalInformation(string! proverExe)
+ ensures _proverPath != null;
+ //throws ProverException, System.IO.FileNotFoundException;
+ {
+ if (_proverPath == null) {
+ // Initialize '_proverPath'
+ _proverPath = Path.Combine(CodebaseString(), proverExe);
+ if (!File.Exists(_proverPath))
+ {
+ _proverPath = Path.Combine(@"c:\Program Files\Microsoft Research\Z3-2.0\bin", proverExe);
+ }
+ if (!File.Exists(_proverPath))
+ {
+ throw new ProverException("Cannot find executable: " + _proverPath);
+ }
+ }
+ }
+
+ [Rep] protected internal ProverProcess thmProver;
+ bool currentProverHasBeenABadBoy = false;
+ // invariant currentProverHasBeenABadBoy ==> thmProver != null;
+ protected int restarts = 0;
+ protected DeclFreeProverContext! ctx;
+ protected string! BackgroundPredFilename;
+ protected ConsoleCancelEventHandler? cancelEvent;
+
+ [NotDelayed]
+ public ProcessTheoremProver(ProverOptions! options, VCExpressionGenerator! gen, DeclFreeProverContext! ctx,
+ string! proverExe, string! backgroundPred)
+ throws UnexpectedProverOutputException;
+ {
+ BackgroundPredFilename = backgroundPred;
+ InitializeGlobalInformation(proverExe);
+ this.ctx = ctx;
+ base(options, "; ", "", "", "", gen);
+
+ // ensure that a VCExprTranslator is available
+ // if none exists so far, we have to create a new one
+ // from scratch and feed the axioms to it
+ if (ctx.exprTranslator == null) {
+ AxiomVCExprTranslator tl = SpawnVCExprTranslator();
+ ctx.exprTranslator = tl;
+ tl.AddAxiom(tl.translate(ctx.Axioms, -1));
+ // we clear the lists with new axioms and declarations;
+ // they are not needed at this point
+ List<string!> x = tl.NewAxioms;
+ x = x; // make the compiler happy: somebody uses the value of x
+ x = tl.NewTypeDecls;
+ }
+ }
+
+ /// <summary>
+ /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)
+ /// </summary>
+ public override void PushVCExpression(VCExpr! vc)
+ {
+ vcExprTranslator.AddAxiom( vcExprTranslator.translate(vc,1) );
+ }
+
+ [NoDefaultContract] // important, since we have no idea what state the object might be in when this handler is invoked
+ void ControlCHandler(object o, ConsoleCancelEventArgs a)
+ {
+ if (thmProver != null) {
+ thmProver.Kill();
+ }
+ }
+
+ public override void Close() {
+ if (cancelEvent != null) {
+ Console.CancelKeyPress -= cancelEvent;
+ cancelEvent = null;
+ }
+ if (thmProver != null) {
+ expose (this) {
+ thmProver.Close();
+ thmProver = null;
+ currentProverHasBeenABadBoy = false;
+ }
+ }
+ base.Close();
+ }
+
+ private UnexpectedProverOutputException proverException;
+
+ public override void BeginCheck(string! descriptiveName, VCExpr! vc, ErrorHandler! handler)
+ {
+ this.NewProblem(descriptiveName);
+ this.proverException = null;
+
+ try {
+ this.ResurrectProver();
+
+ string vcString = vcExprTranslator.translate(vc, 1);
+
+ Helpers.ExtraTraceInformation("Sending data to theorem prover");
+
+ FeedNewAxiomsDecls2Prover();
+ string! prelude = ctx.GetProverCommands(false);
+ vcString = prelude + vcString;
+ LogActivity(vcString);
+
+ assert thmProver != null;
+ thmProver.BeginCheck(descriptiveName, vcString);
+
+ if (CommandLineOptions.Clo.RestartProverPerVC) {
+ LogComment("Will restart the prover due to /restartProver option");
+ currentProverHasBeenABadBoy = true;
+ }
+ } catch (UnexpectedProverOutputException e) {
+ proverException = e;
+ }
+ }
+
+ public override Outcome CheckOutcome(ErrorHandler! handler)
+ throws UnexpectedProverOutputException;
+ {
+ if (this.thmProver == null) {
+ return Outcome.Undetermined;
+ }
+
+ if (proverException == null) {
+ try {
+ ProverProcess.ProverOutcome result = thmProver.CheckOutcome(handler);
+
+ if (options.ForceLogStatus) {
+ switch (result) {
+ case ProverProcess.ProverOutcome.Valid:
+ LogActivity("DBG_WAS_VALID");
+ break;
+ case ProverProcess.ProverOutcome.NotValid:
+ LogActivity("DBG_WAS_INVALID");
+ break;
+ }
+ }
+
+ switch (result) {
+ case ProverProcess.ProverOutcome.Valid:
+ return Outcome.Valid;
+ case ProverProcess.ProverOutcome.TimeOut:
+ return Outcome.TimeOut;
+ case ProverProcess.ProverOutcome.OutOfMemory:
+ return Outcome.OutOfMemory;
+ case ProverProcess.ProverOutcome.Inconclusive:
+ return Outcome.Undetermined;
+ case ProverProcess.ProverOutcome.NotValid:
+ return Outcome.Invalid;
+ }
+ } catch (UnexpectedProverOutputException e) {
+ proverException = e;
+ }
+ }
+
+ assume proverException != null;
+ LogComment("***** Unexpected prover output");
+ expose (this) {
+ currentProverHasBeenABadBoy = true; // this will cause the next resurrect to restart the prover
+ }
+ throw proverException;
+ }
+
+ protected virtual void ResurrectProver()
+ throws UnexpectedProverOutputException;
+ {
+ expose (this) {
+ if (thmProver != null) {
+ if (thmProver.HasExited) {
+ DateTime now = DateTime.Now;
+ LogComment("***** Prover Crashed at or before " + now.ToString("G"));
+
+ } else if (CommandLineOptions.Clo.MaxProverMemory > 0 &&
+ thmProver.NumFormulasChecked > CommandLineOptions.Clo.MinNumOfProverCalls &&
+ thmProver.PeakVirtualMemorySize > CommandLineOptions.Clo.MaxProverMemory)
+ {
+ LogComment("***** Exceeded memory limit. Peak memory usage so far: " +
+ thmProver.PeakVirtualMemorySize / CommandLineOptions.Megabyte + "MB");
+
+ } else if (!currentProverHasBeenABadBoy) {
+ // prover is ready to go
+ return;
+ }
+
+ thmProver.Close();
+ thmProver = null;
+ currentProverHasBeenABadBoy = false;
+ restarts++;
+ }
+ FireUpNewProver();
+ }
+ }
+
+ protected abstract ProverProcess! CreateProverProcess(string! proverPath);
+
+ public void LogBgPush(string! s) {
+ LogCommon("(BG_PUSH ");
+ LogCommon(s);
+ LogCommon(")");
+ }
+
+ [NoDefaultContract]
+ private void FireUpNewProver()
+ requires IsExposed;
+ requires thmProver == null;
+ throws UnexpectedProverOutputException;
+ {
+ if (cancelEvent == null && CommandLineOptions.Clo.RunningBoogieFromCommandLine) {
+ cancelEvent = new ConsoleCancelEventHandler(ControlCHandler);
+ Console.CancelKeyPress += cancelEvent;
+ }
+ thmProver = CreateProverProcess(_proverPath);
+ if (restarts == 0) {
+ foreach (string! s in thmProver.OptionComments().Split('\n')) {
+ LogCommonComment(s);
+ }
+ foreach (string! parmsetting in thmProver.ParameterSettings) {
+ LogCommon(parmsetting);
+ }
+ }
+ foreach (string! parmsetting in thmProver.ParameterSettings) {
+ thmProver.Feed(parmsetting, 0);
+ }
+ thmProver.Feed(GetBackgroundPredicate(BackgroundPredFilename), 3);
+ string! incProverCommands = ctx.GetProverCommands(false);
+ string! proverCommands = ctx.GetProverCommands(true);
+ string! prelude = ctx.GetProverCommands(false);
+
+ if (restarts == 0) {
+ // log the stuff before feeding it into the prover, so when it dies
+ // and takes Boogie with it, we know what happened
+ LogCommon(GetBackgroundPredicate(BackgroundPredFilename));
+ LogCommon(prelude);
+ LogCommon(proverCommands);
+
+ foreach (string! s in vcExprTranslator.AllTypeDecls)
+ LogCommon(s);
+ foreach (string! s in vcExprTranslator.AllAxioms)
+ LogBgPush(s);
+
+ LogCommonComment("Initialized all axioms.");
+ } else {
+ LogCommon(incProverCommands);
+ }
+
+ thmProver.Feed(prelude, 0);
+ thmProver.Feed(proverCommands, 0);
+
+ foreach (string! s in vcExprTranslator.AllTypeDecls)
+ thmProver.Feed(s, 0);
+ foreach (string! s in vcExprTranslator.AllAxioms)
+ thmProver.AddAxioms(s);
+
+ // we have sent everything to the prover and can clear the lists with
+ // new axioms and declarations
+ List<string!> x = vcExprTranslator.NewAxioms;
+ x = x; // make the compiler happy: somebody uses the value of x
+ x = vcExprTranslator.NewTypeDecls;
+ }
+
+ public override ProverContext! Context
+ {
+ get { return this.ctx; }
+ }
+ }
+
+ public class SimplifyTheoremProver : ProcessTheoremProver
+ {
+ [NotDelayed]
+ public SimplifyTheoremProver(ProverOptions! options, VCExpressionGenerator! gen, DeclFreeProverContext! ctx)
+ throws UnexpectedProverOutputException;
+ {
+ base(options, gen, ctx, "simplify.exe", "UnivBackPred2.sx");
+ }
+
+ protected override ProverProcess! CreateProverProcess(string! proverPath) {
+ return new SimplifyProverProcess(proverPath);
+ }
+
+ protected override AxiomVCExprTranslator! SpawnVCExprTranslator() {
+ return new SimplifyVCExprTranslator(gen);
+ }
+ }
+
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+
+ public abstract class AxiomVCExprTranslator : VCExprTranslator {
+ protected AxiomVCExprTranslator() {
+ AllAxioms = new List<string!> ();
+ NewAxiomsAttr = new List<string!> ();
+ AllTypeDecls = new List<string!> ();
+ NewTypeDeclsAttr = new List<string!> ();
+ }
+
+ protected AxiomVCExprTranslator(AxiomVCExprTranslator! tl) {
+ AllAxioms = new List<string!> (tl.AllAxioms);
+ NewAxiomsAttr = new List<string!> (tl.NewAxiomsAttr);
+ AllTypeDecls = new List<string!> (tl.AllTypeDecls);
+ NewTypeDeclsAttr = new List<string!> (tl.NewTypeDeclsAttr);
+ }
+
+ // we store all typing-related axioms that have been sent to the prover
+ // so that the prover can be re-initialised in case it dies
+ public readonly List<string!>! AllAxioms;
+ private List<string!>! NewAxiomsAttr;
+
+ public List<string!>! NewAxioms { get {
+ List<string!>! res = NewAxiomsAttr;
+ NewAxiomsAttr = new List<string!> ();
+ return res;
+ } }
+
+ // similarly, a list of declarations that have been sent to the prover
+ public readonly List<string!>! AllTypeDecls;
+ private List<string!>! NewTypeDeclsAttr;
+
+ public List<string!>! NewTypeDecls { get {
+ List<string!>! res = NewTypeDeclsAttr;
+ NewTypeDeclsAttr = new List<string!> ();
+ return res;
+ } }
+
+ public void AddAxiom(string! axiom) {
+ AllAxioms.Add(axiom);
+ NewAxiomsAttr.Add(axiom);
+ }
+
+ public void AddTypeDecl(string! typeDecl) {
+ AllTypeDecls.Add(typeDecl);
+ NewTypeDeclsAttr.Add(typeDecl);
+ }
+ }
+
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+
+ public class SimplifyVCExprTranslator : AxiomVCExprTranslator {
+ public SimplifyVCExprTranslator(VCExpressionGenerator! gen) {
+ Gen = gen;
+ TypeAxiomBuilder! axBuilder;
+ switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+ case CommandLineOptions.TypeEncoding.Arguments:
+ axBuilder = new TypeAxiomBuilderArguments (gen);
+ break;
+ default:
+ axBuilder = new TypeAxiomBuilderPremisses (gen);
+ break;
+ }
+ axBuilder.Setup();
+ AxBuilder = axBuilder;
+ Namer = new UniqueNamer ();
+ LitAbstracter = new BigLiteralAbstracter (gen);
+ }
+
+ private SimplifyVCExprTranslator(SimplifyVCExprTranslator! tl) {
+ base(tl);
+ Gen = tl.Gen;
+ AxBuilder = (TypeAxiomBuilder)tl.AxBuilder.Clone();
+ Namer = (UniqueNamer)tl.Namer.Clone();
+ LitAbstracter = (BigLiteralAbstracter)tl.LitAbstracter.Clone();
+ }
+
+ public override Object! Clone() {
+ return new SimplifyVCExprTranslator(this);
+ }
+
+ private readonly VCExpressionGenerator! Gen;
+ private readonly TypeAxiomBuilder! AxBuilder;
+ private readonly UniqueNamer! Namer;
+ private readonly BigLiteralAbstracter! LitAbstracter;
+
+ public override string! translate(VCExpr! expr, int polarity) {
+ Let2ImpliesMutator! letImplier = new Let2ImpliesMutator (Gen);
+
+ // handle the types in the VCExpr
+ TypeEraser! eraser;
+ switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+ case CommandLineOptions.TypeEncoding.Arguments:
+ eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, Gen);
+ break;
+ default:
+ eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);
+ break;
+ }
+ VCExpr! exprWithoutTypes = eraser.Erase(expr, polarity);
+
+ TermFormulaFlattener! flattener = new TermFormulaFlattener (Gen);
+ VCExpr! exprWithLet = flattener.Flatten(exprWithoutTypes);
+ VCExpr! exprWithoutLet = letImplier.Mutate(exprWithLet);
+
+ // big integer literals
+ VCExpr! exprWithoutBigLits = LitAbstracter.Abstract(exprWithoutLet);
+ AddAxiom(SimplifyLikeExprLineariser.ToSimplifyString(LitAbstracter.GetNewAxioms(),
+ Namer));
+
+ // type axioms
+ VCExpr! axiomsWithLet = flattener.Flatten(AxBuilder.GetNewAxioms());
+ VCExpr! axiomsWithoutLet = letImplier.Mutate(axiomsWithLet);
+
+ AddAxiom(SimplifyLikeExprLineariser.ToSimplifyString(axiomsWithoutLet, Namer));
+ return SimplifyLikeExprLineariser.ToSimplifyString(exprWithoutBigLits, Namer);
+ }
+ }
+
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+
+ public class Factory : ProverFactory
+ {
+ public override object! SpawnProver(ProverOptions! options, object! ctxt)
+ {
+ return new SimplifyTheoremProver(options,
+ ((DeclFreeProverContext!)ctxt).ExprGen,
+ (DeclFreeProverContext!)ctxt);
+ }
+
+ public override object! NewProverContext(ProverOptions! options) {
+ if (CommandLineOptions.Clo.BracketIdsInVC < 0) {
+ CommandLineOptions.Clo.BracketIdsInVC = 1;
+ }
+ VCExpressionGenerator! gen = new VCExpressionGenerator();
+ List<string!>! proverCommands = new List<string!> ();
+ proverCommands.Add("all");
+ proverCommands.Add("simplify");
+ proverCommands.Add("simplifyLike");
+ return new DeclFreeProverContext(gen, new VCGenerationOptions(proverCommands));
+ }
+
+ public override CommandLineOptions.VCVariety DefaultVCVariety
+ {
+ get { return CommandLineOptions.VCVariety.BlockNested; }
+ }
+
+ // needed to make test7 pass
+ public override bool SupportsDags
+ {
+ get { return true; }
+ }
+ }
+}
diff --git a/Source/Provers/Simplify/Simplify.sscproj b/Source/Provers/Simplify/Simplify.sscproj new file mode 100644 index 00000000..675a766b --- /dev/null +++ b/Source/Provers/Simplify/Simplify.sscproj @@ -0,0 +1,135 @@ +<?xml version="1.0" encoding="utf-8"?>
+<VisualStudioProject>
+ <XEN ProjectType="Local"
+ SchemaVersion="1.0"
+ Name="Simplify"
+ ProjectGuid="f75666de-fb56-457c-8782-09be243450fc"
+ >
+ <Build>
+ <Settings ApplicationIcon=""
+ AssemblyName="Provers.Simplify"
+ OutputType="Library"
+ RootNamespace="Microsoft.Boogie.Simplify"
+ StartupObject=""
+ StandardLibraryLocation=""
+ TargetPlatform="v2"
+ TargetPlatformLocation=""
+ ShadowedAssembly=""
+ NoStandardLibraries="False"
+ >
+ <Config Name="Debug"
+ AllowUnsafeBlocks="False"
+ BaseAddress="285212672"
+ CheckForOverflowUnderflow="False"
+ ConfigurationOverrideFile=""
+ DefineConstants="DEBUG;TRACE"
+ DocumentationFile=""
+ DebugSymbols="True"
+ FileAlignment="4096"
+ IncrementalBuild="True"
+ Optimize="False"
+ OutputPath="bin\debug"
+ RegisterForComInterop="False"
+ RemoveIntegerChecks="false"
+ TreatWarningsAsErrors="False"
+ WarningLevel="4"
+ ReferenceTypesAreNonNullByDefault="False"
+ RunProgramVerifier="False"
+ RunProgramVerifierWhileEditing="False"
+ ProgramVerifierCommandLineOptions=""
+ AllowPointersToManagedStructures="False"
+ CheckContractAdmissibility="True"
+ CheckPurity="False"
+ />
+ <Config Name="Release"
+ AllowUnsafeBlocks="false"
+ BaseAddress="285212672"
+ CheckForOverflowUnderflow="false"
+ ConfigurationOverrideFile=""
+ DefineConstants="TRACE"
+ DocumentationFile=""
+ DebugSymbols="false"
+ FileAlignment="4096"
+ IncrementalBuild="false"
+ Optimize="true"
+ OutputPath="bin\release"
+ RegisterForComInterop="false"
+ RemoveIntegerChecks="false"
+ TreatWarningsAsErrors="false"
+ WarningLevel="4"
+ />
+ </Settings>
+ <References>
+ <Reference Name="System"
+ AssemblyName="System"
+ Private="false"
+ />
+ <Reference Name="System.Data"
+ AssemblyName="System.Data"
+ Private="false"
+ />
+ <Reference Name="System.Xml"
+ AssemblyName="System.Xml"
+ Private="false"
+ />
+ <Reference Name="Core"
+ Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"
+ Private="true"
+ />
+ <Reference Name="AIFramework"
+ Project="{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"
+ Private="true"
+ />
+ <Reference Name="Graph"
+ Project="{4C28FB90-630E-4B55-A937-11A011B79765}"
+ Private="true"
+ />
+ <Reference Name="Mscorlib.Contracts"
+ AssemblyName="Mscorlib.Contracts"
+ Private="false"
+ HintPath="../../../Binaries/Mscorlib.Contracts.dll"
+ />
+ <Reference Name="System.Contracts"
+ AssemblyName="System.Contracts"
+ Private="false"
+ HintPath="../../../Binaries/System.Contracts.dll"
+ />
+ <Reference Name="VCGeneration"
+ Project="{F65666DE-FB56-457C-8782-09BE243450FC}"
+ Private="true"
+ />
+ <Reference Name="Basetypes"
+ Project="{0C692837-77EC-415F-BF04-395E3ED06E9A}"
+ Private="true"
+ />
+ <Reference Name="VCExpr"
+ Project="{CF42B700-10AA-4DA9-8992-48A800251C11}"
+ Private="true"
+ />
+ </References>
+ </Build>
+ <Files>
+ <Include>
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="Prover.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="ProverInterface.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="..\..\version.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="Let2ImpliesVisitor.ssc"
+ />
+ </Include>
+ </Files>
+ <Target Name="AfterBuild"
+ >
+ </Target>
+ </XEN>
+</VisualStudioProject>
\ No newline at end of file diff --git a/Source/Provers/Z3/Inspector.ssc b/Source/Provers/Z3/Inspector.ssc new file mode 100644 index 00000000..ca7fc084 --- /dev/null +++ b/Source/Provers/Z3/Inspector.ssc @@ -0,0 +1,130 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.IO;
+using System.Diagnostics;
+using System.Collections;
+using System.Collections.Generic;
+using util;
+using Microsoft.Contracts;
+using Microsoft.Boogie;
+using Microsoft.Boogie.Simplify;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.Z3
+{
+ internal class FindLabelsVisitor : TraversingVCExprVisitor<bool, bool> {
+ public Dictionary<string!,bool>! Labels = new Dictionary<string!,bool>();
+
+ public static Dictionary<string!,bool>! FindLabels(VCExpr! expr) {
+ FindLabelsVisitor! visitor = new FindLabelsVisitor();
+ visitor.Traverse(expr, true);
+ return visitor.Labels;
+ }
+
+ protected override bool StandardResult(VCExpr! node, bool arg) {
+ VCExprNAry nary = node as VCExprNAry;
+ if (nary != null) {
+ VCExprLabelOp lab = nary.Op as VCExprLabelOp;
+ if (lab != null) {
+ Labels[lab.label] = lab.pos;
+ }
+ }
+ return true;
+ }
+ }
+
+ internal class Inspector {
+ [Rep] protected readonly Process! inspector;
+ [Rep] readonly TextReader! fromInspector;
+ [Rep] readonly TextWriter! toInspector;
+
+ public Inspector(Z3InstanceOptions! opts)
+ {
+ ProcessStartInfo! psi = new ProcessStartInfo(opts.Inspector);
+ psi.CreateNoWindow = true;
+ psi.UseShellExecute = false;
+ psi.RedirectStandardInput = true;
+ psi.RedirectStandardOutput = true;
+ psi.RedirectStandardError = false;
+
+ try
+ {
+ Process inspector = Process.Start(psi);
+ this.inspector = inspector;
+ fromInspector = inspector.StandardOutput;
+ toInspector = inspector.StandardInput;
+ }
+ catch (System.ComponentModel.Win32Exception e)
+ {
+ throw new Exception(string.Format("Unable to start the inspector process {0}: {1}", opts.Inspector, e.Message));
+ }
+ }
+
+ public void NewProver()
+ {
+ }
+
+ public void NewProblem(string! descriptiveName, VCExpr! vc, ProverInterface.ErrorHandler! handler)
+ {
+ Dictionary<string!,bool>! labels = FindLabelsVisitor.FindLabels(vc);
+ toInspector.WriteLine("PROBLEM " + descriptiveName);
+ toInspector.WriteLine("TOKEN BEGIN");
+ foreach (string! lab in labels.Keys) {
+ string! no = lab.Substring(1);
+ Absy! absy = handler.Label2Absy(no);
+ IToken tok = absy.tok;
+ AssertCmd assrt = absy as AssertCmd;
+ Block blk = absy as Block;
+ string val = tok.val; // might require computation, so cache it
+ if (val == "foo" || tok.filename == null) continue; // no token
+ if (!val.Contains(" ")) val = null;
+
+ toInspector.Write("TOKEN ");
+ toInspector.Write(lab);
+ toInspector.Write(" ");
+
+ if (assrt != null) {
+ toInspector.Write("ASSERT");
+ string errData = assrt.ErrorData as string;
+ if (errData != null) {
+ val = errData;
+ } else if (assrt.ErrorMessage != null) {
+ val = assrt.ErrorMessage;
+ }
+ } else if (blk != null) {
+ toInspector.Write("BLOCK ");
+ toInspector.Write(blk.Label);
+ } else {
+ assume false;
+ }
+ if (val == null) { val = ""; }
+
+ if (absy is LoopInitAssertCmd) {
+ val += " (loop entry)";
+ } else if (absy is LoopInvMaintainedAssertCmd) {
+ val += " (loop body)";
+ } else if (absy is AssertRequiresCmd && val == "") {
+ AssertRequiresCmd req = (AssertRequiresCmd)absy;
+ IToken t2 = req.Requires.tok;
+ val = string.Format("precondition {0}({1},{2})", t2.filename, t2.line, t2.col);
+ }
+
+ val = val.Replace("\r", "").Replace("\n", " ");
+
+ toInspector.WriteLine(string.Format(" {0} {1} :@:{2}:@:{3}", tok.line, tok.col, tok.filename, val));
+ }
+ toInspector.WriteLine("TOKEN END");
+ }
+
+ public void StatsLine(string! line)
+ {
+ toInspector.WriteLine(line);
+ toInspector.Flush();
+ }
+ }
+}
diff --git a/Source/Provers/Z3/Prover.ssc b/Source/Provers/Z3/Prover.ssc new file mode 100644 index 00000000..d3212a9c --- /dev/null +++ b/Source/Provers/Z3/Prover.ssc @@ -0,0 +1,870 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.IO;
+using System.Diagnostics;
+using System.Collections;
+using System.Collections.Generic;
+using System.Text;
+using util;
+using Microsoft.Contracts;
+using Microsoft.Boogie;
+using Microsoft.Boogie.Simplify;
+using Microsoft.Basetypes;
+
+// Simplified interface to an external prover like Simplify or the z3 process, taken from Bird.
+namespace Microsoft.Boogie.Z3
+{
+ internal class Z3ProverProcess : ProverProcess {
+ [Peer] private Z3InstanceOptions! opts;
+ [Peer] private readonly Inspector? inspector;
+ private readonly bool expectingModel = false;
+
+ private string! cmdLineArgs = "";
+ class OptionValue {
+ public readonly string! Option;
+ public readonly string! Value;
+ public OptionValue(string! option, string! value) { Option = option; Value = value; }
+ }
+ static void AddOption(List<OptionValue!>! parms, string! option, string! value)
+ modifies parms.*;
+ {
+ OptionValue ov = new OptionValue(option, value);
+ Owner.AssignSame(ov, Owner.ElementProxy(parms));
+ parms.Add(ov);
+ }
+ private List<OptionValue!>! parameterSettings;
+
+ // [NotDelayed]
+ [Captured]
+ public Z3ProverProcess(Z3InstanceOptions! opts, Inspector? inspector)
+ requires inspector != null ==> Owner.Same(opts, inspector);
+ { // throws ProverException
+ 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");
+
+ // 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 (0 <= CommandLineOptions.Clo.ProverCCLimit) {
+ z3args += " " + OptionChar() + "@ " +
+ 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) {
+ z3args += " " + OptionChar() + "m";
+ expectingModel = 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) {
+ 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;
+
+ string exePath = opts.ExeName;
+ if (!File.Exists(exePath)){
+ exePath = @"c:\Program Files\Microsoft Research\Z3-2.0\bin";
+ }
+
+ ProcessStartInfo! psi = new ProcessStartInfo(exePath, z3args);
+ 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;
+ }
+
+ public override string! OptionComments()
+ {
+ 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) {
+ sb.Append(" ").Append(opt);
+ }
+ sb.AppendFormat("\nProver options: {0}\n", opts.ToString());
+ return sb.ToString();
+ }
+
+ [Pure(false)]
+ public override IEnumerable<string!>! ParameterSettings {
+ get {
+ if (opts.V2) {
+ foreach (OptionValue opt in parameterSettings) {
+ yield return "(SETPARAMETER " + opt.Option + " " + opt.Value + ")";
+ }
+ }
+ }
+ }
+
+ // z3 uses different magic characters for options on linux/unix and on windows
+ private static string! OptionChar() {
+ assume Environment.OSVersion != null;
+ switch (Environment.OSVersion.Platform) {
+ case PlatformID.Unix:
+ return "-";
+ default:
+ return "/";
+ }
+ }
+
+ protected override void DoBeginCheck(string! descriptiveName, string! formula)
+ {
+ ToWriteLine(formula);
+ ToWriteLine(String.Format("; END OF FORMULA {0} - {1}", NumFormulasChecked.ToString(), descriptiveName));
+ ToFlush();
+ }
+
+ protected int TimedFromReadChar()
+ {
+ if (opts.Timeout > 0)
+ return FromReadChar((opts.Timeout + 1) * 1000);
+ else
+ return FromReadChar();
+ }
+
+ private void Trace(string! msg)
+ {
+ Console.WriteLine("Z3: " + msg);
+ }
+
+ public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler! handler)
+ throws UnexpectedProverOutputException;
+ {
+ ProverOutcome outcome;
+ bool isInvalid = false;
+
+ if (this.simplify == null) {
+ return ProverOutcome.Inconclusive;
+ }
+
+
+ while (true) {
+ int ch = TimedFromReadChar();
+ if (ch == -1 && this.readTimedOut) {
+ handler.OnResourceExceeded("timeout (forced)");
+ return ProverOutcome.TimeOut;
+ }
+
+ string line = new string((char)ch, 1) + FromReadLine();
+
+ if (line.StartsWith("STATS ")) {
+ if (inspector != null) {
+ inspector.StatsLine(line);
+ }
+ continue;
+ }
+
+ if (opts.Verbosity > 2) {
+ Trace("INPUT: " + line);
+ }
+
+ if (line.StartsWith("WARNING: Out of allocated virtual memory.")) {
+ handler.OnResourceExceeded("memory");
+ return ProverOutcome.OutOfMemory;
+ }
+
+
+ if (line.StartsWith("WARNING: ")) {
+ string w = line.Substring(9);
+ ReportWarning(w);
+ continue;
+ }
+
+ if (line.ToUpper().StartsWith("ERROR")) {
+ Console.WriteLine("Z3 returns the following error:");
+ Console.WriteLine(" " + line);
+ return ProverOutcome.Inconclusive;
+ }
+
+ int beg = 0;
+ while (beg < line.Length && '0' <= line[beg] && line[beg] <= '9')
+ invariant beg <= line.Length;
+ {
+ beg++;
+ }
+
+ if (beg > 0 && line.Substring(beg).StartsWith(": ")) {
+ string status = line.Substring(beg + 2);
+
+ if (status.StartsWith("Valid")) {
+ return ProverOutcome.Valid;
+ }
+
+ if (status.StartsWith("Timeout")) {
+ handler.OnResourceExceeded("timeout");
+ return ProverOutcome.TimeOut;
+ }
+
+ if (status.StartsWith("Inconclusive")) {
+ return ProverOutcome.Inconclusive;
+ }
+
+ if (status.StartsWith("Invalid")) {
+ isInvalid = true;
+ continue;
+ }
+ }
+
+ if (isInvalid && line == ".") {
+ return ProverOutcome.NotValid;
+ }
+
+ if (isInvalid && line.StartsWith("labels: (")) {
+ List<string!>! l = ParseLabels(line);
+ Z3ErrorModel errModel = null;
+ if (expectingModel) {
+ if (opts.Verbosity > 2) {
+ Trace("waiting for model");
+ }
+ line = FromReadLine();
+ if (line.StartsWith("partitions:")) {
+ line = ParseModel(out errModel);
+ if (opts.Verbosity > 2) {
+ Trace("model parsed, final line " + line);
+ }
+ // Z3 always ends the model with END_OF_MODEL, not with labels: or .
+ assume line == "END_OF_MODEL";
+ } else {
+ throw new UnexpectedProverOutputException(string.Format("evil input from z3 (expecting partitions): '{0}'", line));
+ }
+ }
+ handler.OnModel(l, errModel);
+ continue;
+ }
+
+ throw new UnexpectedProverOutputException(string.Format("evil input from z3: '{0}'", line));
+ }
+ }
+
+ /* ----------------------------------------------------------------------------
+ BNF Grammar to parse Z3 output, including the model generated when using the /m /si switch:
+
+ Output ::= VC*
+ VC ::= number ": " "Valid." | number ": " "Inconclusive" | VCI
+ VCI ::= number ": " "Invalid"
+ ("labels: " "(" ID* ")"
+ [MODEL] "END_OF_MODEL")+
+ "."
+ MODEL ::= MBOOL MFUNC
+ MBOOL ::= "boolean assignment:"
+ "partitions:"
+ MAPPING*
+ MAPPING ::= ZID ["{" ID+"}"] ["->" "(" (number | false | true | BITVECTOR) ")"]
+ BITVECTOR ::= ulong ":bv" int
+ MFUNC ::= "function interpretations:"
+ F*
+ F ::= Id "->" "{"
+ MAPLET*
+ "else" "->" ZID
+ "}"
+ MAPLET ::= ZID* "->" ZID
+
+ -----------------------------------------------------------------------------*/
+ private string! ParseModel(out Z3ErrorModel errModel)
+ modifies this.*;
+ ensures result == "." || result.StartsWith("labels: (") || result == "END_OF_MODEL";
+ throws UnexpectedProverOutputException;
+ {
+ //Format in the grammar:
+ // ZID ["{" ID+"}"] ["->" "(" (number | false | true) ")"]
+ // storing the model:
+ // map each ID (a string) to the corresping ZID (an integer) in a dictionary:
+ Dictionary<string!, int> identifierToPartition = new Dictionary<string!, int>();
+ // map each ZID to the set (in list form) of IDs belonging to it (possibly empty):
+ List<List<string!>> partitionToIdentifiers = new List<List<string!>>();
+ // map each ZID to the number or boolean given, if any:
+ List<Object> partitionToValue = new List<Object>();
+ // map each value (number or boolean) to the ZID, reverse map of partitionToValue
+ Dictionary<Object, int> valueToPartition = new Dictionary<Object, int>();
+ Owner.AssignSame(Owner.ElementProxy(partitionToValue), Owner.ElementProxy(valueToPartition));
+
+ int ch;
+
+ // read the MAPPING
+ for (int zID = 0; true; zID++)
+ {
+ ch = FromReadChar();
+ if (ch == 'f') {
+ break;
+ }
+ ParseModelMapping(zID, identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition);
+ }// end MAPPING
+
+ // add the fake partition for the 'else -> #undefined' clause
+ List<string!> emptyList = new List<string!>();
+ Owner.AssignSame(emptyList, Owner.ElementProxy(partitionToIdentifiers));
+ partitionToIdentifiers.Add(emptyList);
+ partitionToValue.Add(null);
+
+ // continue in ParseModelFunctions, which breaks up this long method and enables its verification
+ return ParseModelFunctions(ch, out errModel, identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition);
+ }
+
+ private void ParseModelMapping(int zID,
+ Dictionary<string!, int>! identifierToPartition,
+ List<List<string!>>! partitionToIdentifiers,
+ List<Object>! partitionToValue,
+ Dictionary<Object, int>! valueToPartition)
+ requires Owner.Same(Owner.ElementProxy(partitionToValue), Owner.ElementProxy(valueToPartition));
+ modifies this.*, identifierToPartition.*, partitionToIdentifiers.*, partitionToValue.*, valueToPartition.*;
+ {
+ string s = FromReadLine();
+ {
+ // sanity check
+ int pos = s.IndexOf(' ');
+ string n = s;
+ int k;
+ if (pos >= 0) {
+ n = s.Substring(0,pos);
+ }
+ if (! (int.TryParse(n, out k) && zID == k)) {
+ System.Console.WriteLine("mismatch: {0}!={1} '{2}'", zID, k, s);
+ assume false;
+ }
+ }
+
+ int j = ParseModelZidAndIdentifiers(zID, s, identifierToPartition, partitionToIdentifiers);
+
+ j = s.IndexOf(" -> ", j);
+ if (0 <= j) {
+ j += 4;
+ }
+ 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
+ valueToPartition.Add("nullObject", zID);
+ // In this case partitionToValue (as the reverse of valueToPartition) should include
+ // a map from zID -> "nullObject", but doing that breaks printing out the model as
+ // it is printed out by Z3. Also, that information is not required, valueToPartition
+ // works well enough by itself.
+ }
+
+ } else if (s[j] == 't'/*rue*/) {
+ partitionToValue.Add(true);
+ object boxedTrue = true;
+ 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));
+ partitionToValue.Add(boxedFalse);
+ 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 {
+ string numberOrBv = s.Substring(j);
+ // make number an int, then store it:
+ BigNum bvVal;
+ int bvSize;
+ string number, type;
+
+ int l = numberOrBv.IndexOf(':', 0);
+ if (0 <= l) {
+ number = numberOrBv.Substring(0, l);
+ type = numberOrBv.Substring(l + 1);
+ } else {
+ l = numberOrBv.IndexOf('[', 0);
+ if (0 <= l) {
+ number = numberOrBv.Substring(2, l-2);
+ int closingBracePosition = numberOrBv.IndexOf(']', l);
+ if (l < closingBracePosition)
+ type = "bv" + numberOrBv.Substring(l + 1, closingBracePosition - l - 1);
+ else type = "int";
+ } else {
+ number = numberOrBv;
+ type = "int";
+ }
+ }
+
+ if (type == "int") {
+ object boxedN = BigNum.FromString(number);
+ assume Owner.None(boxedN);
+ Owner.AssignSame(boxedN, Owner.ElementProxy(partitionToValue));
+ partitionToValue.Add(boxedN);
+ 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));
+ partitionToValue.Add(bitV);
+ 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;
+ }
+
+ }
+ }
+
+ 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;
+ {
+ List<string!> identifiers = new List<string!>();
+ int j = s.IndexOf('{', 0) + 1; // skip the '{', if present, and set j to 0 otherwise
+ if (1 <= j) {
+ // There is a list of ID's.
+ 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;
+ {
+ int k = s.IndexOfAny(new char[]{' ', '}'}, j);
+ 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
+ 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
+ }//end ID*
+ }
+ Owner.AssignSame(identifiers, Owner.ElementProxy(partitionToIdentifiers));
+ partitionToIdentifiers.Add(identifiers);
+ return j;
+ }
+
+ private string! ParseModelFunctions(int ch, out Z3ErrorModel errModel,
+ Dictionary<string!, int>! identifierToPartition,
+ List<List<string!>>! partitionToIdentifiers,
+ List<Object>! partitionToValue,
+ Dictionary<Object, int>! valueToPartition
+ )
+ modifies this.*;
+ ensures result == "." || result.StartsWith("labels: (") || result == "END_OF_MODEL";
+ throws UnexpectedProverOutputException;
+ {
+ // read the function F
+ Expect(ch, "function interpretations:");
+ FromReadLine();
+
+ // mapping of function names to function definitions
+ Dictionary<string!, List<List<int>>!> definedFunctions = new Dictionary<string!, List<List<int>>!>();
+ // function definition given as list of 'pointwise definitions' in the form of the arguments and result
+ // the last element here will always be a list with just one entry which corresponds to the else case
+ List<List<int>> functionDefinition = new List<List<int>>();
+ // list of arguments, followed by the result, the last element of this list is always the result
+ List<int> argumentsAndResult = new List<int>();
+
+ // read F
+ while (true)
+ {
+ functionDefinition = new List<List<int>>();
+ string s = FromReadLine();
+ // end of F, "END_OF_MODEL" ends model, '.' ends whole VC, 'l' starts a new set of labels and model
+ // whenever there is a model this will end with "END_OF_MODEL", the other cases can only
+ // happen when there is no model printed!
+ if (s == "." || s.StartsWith("labels: (") || s == "END_OF_MODEL") {
+ errModel = new Z3ErrorModel(identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition, definedFunctions);
+ return s;
+ }
+ int j = s.IndexOf(' ', 0);
+ assume 0 <= j;
+ string id = s.Substring(0, j);
+ // id is stored into definedFunctions once the function definition for it has
+ // been completely parsed,
+
+ // just ignore the "-> {" by dropping string s
+ string zIDstring;
+
+ // MAPLET
+ while (true)
+ {
+ argumentsAndResult = new List<int>();
+ // remove the 2 spaces that are here
+ FromReadChar();
+ FromReadChar();
+ s = FromReadLine();
+ if (s.StartsWith("else ->")) break;
+ j = 0;
+
+ //ZID*
+ while(true)
+ invariant 0 <= j && j <= s.Length;
+ {
+ j = s.IndexOfAny(new Char[]{'*', '-'}, j);
+ // true because this always ends with a "->":
+ assume 0 <= j;
+
+ // reading -> means end of ZID*
+ if (s[j] == '-'/*>*/) break;
+
+ // start reading the ZID* with the number, not the *
+ j = j + 1;
+ // by input string format:
+ assume j < s.Length;
+ int k = s.IndexOf(' ', j);
+ // by input string format:
+ assume j <= k;
+ zIDstring = s.Substring(j, k-j);
+ // add the arguments
+ argumentsAndResult.Add(int.Parse(zIDstring));
+ j = k;
+ }// end ZID*
+
+ // j is the beginning of "-> *", we want the first character after this
+ j = j + 4;
+ // by input string format:
+ assume j <= s.Length;
+ zIDstring = s.Substring(j);
+ // add the result
+ argumentsAndResult.Add(int.Parse(zIDstring));
+ // add the input line as another 'pointwise defined' element to the functions definition
+ functionDefinition.Add(argumentsAndResult);
+ }// end MAPLET
+
+ // this is the 'else -> #unspecified' case
+ // by input string format:
+ 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));
+ functionDefinition.Add(argumentsAndResult);
+
+ /*
+ // this is the 'else -> *' case, that string is already in s
+ j = s.IndexOf('*', 0) + 1;
+ // by input string format:
+ assume 0 < j && j < s.Length;
+ zIDstring = s.Substring(j);
+ // this stores the else line as another argumentsAndResult list
+ argumentsAndResult = new List<int>();
+ argumentsAndResult.Add(int.Parse(zIDstring));
+ // which is then added to the function definition, which is now complete
+ functionDefinition.Add(argumentsAndResult); */
+
+ // and therefore added to the map of defined functions, together with the name 'id'
+ // which had been extracted before
+ assume !definedFunctions.ContainsKey(id); // each function name in the model is listed only once
+ definedFunctions.Add(id, functionDefinition);
+
+ // read the line with "}"
+ ch = FromReadChar();
+ Expect(ch, "}");
+ FromReadLine();
+ }// end F
+ }
+
+ }
+
+
+ public class Z3ErrorModel : ErrorModel
+ {
+ public Z3ErrorModel(Dictionary<string!, int>! identifierToPartition, List<List<string!>>! partitionToIdentifiers, List<Object>! partitionToValue, Dictionary<object, int>! valueToPartition, Dictionary<string!, List<List<int>>!>! definedFunctions)
+ : base(identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition, definedFunctions)
+ {
+ this.partitionNames = new string?[partitionToIdentifiers.Count];
+ this.prevPartitionNames = new string?[partitionToIdentifiers.Count];
+ }
+
+ private string?[]! partitionNames;
+ private string?[]! prevPartitionNames;
+
+ private void SetNames()
+ {
+ int len = partitionToIdentifiers.Count;
+ for (int i = 0; i < 3; ++i) { // let the names stabilize a bit
+ prevPartitionNames = partitionNames;
+ partitionNames = new string?[len];
+ for (int pos = 0; pos < len; ++pos)
+ GetPartitionName(pos);
+ }
+ }
+
+ private int NameBadness(string! name)
+ {
+ int badness = name.Length;
+ if (name.StartsWith("call") && name.IndexOf("formal@") > 0)
+ badness += 1000;
+ if (name.IndexOf ("(") > 0)
+ badness += 500;
+ return badness;
+ }
+
+ private string! GetPartitionName(int pos)
+ {
+ string name = partitionNames[pos];
+ if (name != null) {
+ return name;
+ }
+
+ object tmp = partitionToValue[pos];
+ if (tmp != null) {
+ partitionNames[pos] = tmp is BvConst ? ((BvConst)tmp).ToReadableString() : tmp.ToString();
+ } else {
+ List<string!>! possible_names = new List<string!>();
+ List<string!> pti = partitionToIdentifiers[pos];
+
+ // make sure we're not called recursively
+ string prevName = prevPartitionNames[pos];
+ if (prevName == null) prevName = "*" + pos;
+ partitionNames[pos] = prevName;
+
+ if (pti != null && pti.Count > 0) {
+ // add identifiers
+ foreach (string! name in pti)
+ possible_names.Add(name);
+ }
+
+ // 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) {
+ if (parms.Count > 1 && parms[parms.Count - 1] == pos) {
+ string! s = kv.Key + "(";
+ for (int i = 0; i < parms.Count - 1; ++i) {
+ if (i != 0) s += ", ";
+ s += GetPartitionName(parms[i]);
+ }
+ s += ")";
+ possible_names.Add(s);
+ }
+ }
+ }
+
+ // choose the shortest possible name
+ if (possible_names.Count > 0) {
+ string! best = possible_names[0];
+ foreach (string! s in possible_names)
+ if (NameBadness(s) < NameBadness(best)) best = s;
+ if (best.Length < 120)
+ partitionNames[pos] = best;
+ }
+ }
+
+ return (!)partitionNames[pos];
+ }
+
+ private void PrintReadableModel (TextWriter! writer) {
+ writer.WriteLine("Z3 error model: ");
+ SetNames();
+ writer.WriteLine("partitions:");
+ 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];
+ if (pti != null && (pti.Count > 1 || (pti.Count == 1 && partitionToValue[i] != null))) {
+ writer.Write("{");
+ for (int k = 0; k < pti.Count - 1; k ++) {
+ writer.Write(pti[k] + " ");
+ }
+ //extra work to make sure no " " is at the end of the list of identifiers
+ if (pti.Count != 0) {
+ writer.Write(pti[pti.Count - 1]);
+ }
+ writer.Write("}");
+ }
+ writer.WriteLine();
+ }
+
+ writer.WriteLine();
+ writer.WriteLine("function interpretations:");
+ List<string!> funNames = new List<string!>(definedFunctions.Keys);
+ funNames.Sort();
+ foreach (string! name in funNames) {
+ if (definedFunctions[name].Count == 1) continue; // skip functions with only the else-> clause
+ foreach (List<int>! parms in definedFunctions[name]) {
+ string! s = name + "(";
+ if (parms.Count == 1) {
+ continue;
+ // s += "*";
+ } else {
+ for (int i = 0; i < parms.Count - 1; ++i) {
+ if (i != 0) s += ", ";
+ s += GetPartitionName(parms[i]);
+ }
+ }
+ s += ")";
+ string! res = GetPartitionName(parms[parms.Count - 1]);
+ if (res == s)
+ res = "*" + parms[parms.Count - 1] + " (SELF)";
+ writer.WriteLine("{0} = {1}", s, res);
+ }
+ writer.WriteLine();
+ }
+ writer.WriteLine("The end.");
+ writer.WriteLine();
+ }
+
+ public override void Print (TextWriter! writer) {
+ if (CommandLineOptions.Clo.PrintErrorModel == 4) {
+ PrintReadableModel(writer);
+ return;
+ }
+
+ writer.WriteLine("Z3 error model: ");
+
+ writer.WriteLine("partitions:");
+ assert partitionToIdentifiers.Count == partitionToValue.Count;
+ for (int i = 0; i < partitionToIdentifiers.Count; i++){
+ writer.Write("*"+i);
+ List<string!> pti = partitionToIdentifiers[i];
+ if (pti != null && pti.Count != 0) {
+ writer.Write(" {");
+ for (int k = 0; k < pti.Count - 1; k ++) {
+ writer.Write(pti[k] + " ");
+ }
+ //extra work to make sure no " " is at the end of the list of identifiers
+ if (pti.Count != 0) {
+ writer.Write(pti[pti.Count - 1]);
+ }
+ writer.Write("}");
+ }
+ // temp object needed for non-null checking
+ object tempPTVI = partitionToValue[i];
+ if (tempPTVI != null) {
+ if (tempPTVI.ToString() == "True") {
+ writer.Write(" -> " + "true" + "");
+ } else if (tempPTVI.ToString() == "False") {
+ writer.Write(" -> " + "false" + "");
+ } else if (tempPTVI is BigNum) {
+ writer.Write(" -> " + tempPTVI + ":int");
+ } else {
+ writer.Write(" -> " + tempPTVI + "");
+ }
+ } else {
+ writer.Write(" ");
+ }
+ writer.WriteLine();
+ }
+
+ writer.WriteLine("function interpretations:");
+ foreach (KeyValuePair<string!, List<List<int>>!> kvp in definedFunctions) {
+ writer.WriteLine(kvp.Key + " -> {");
+ List<List<int>> kvpValue = kvp.Value;
+ if (kvpValue != null) {
+ foreach(List<int> l in kvpValue) {
+ writer.Write(" ");
+ if (l != null) {
+ for (int i = 0; i < l.Count - 1; i++) {
+ writer.Write("*"+l[i] + " ");
+ }
+ if (l.Count == 1) {
+ writer.WriteLine("else -> #unspecified");
+ } else {
+ writer.WriteLine("-> "+ "*" + l[l.Count - 1]);
+ }
+ }
+ }
+ }
+ writer.WriteLine("}");
+ }
+ writer.WriteLine("END_OF_MODEL");
+ writer.WriteLine(".");
+
+ if (CommandLineOptions.Clo.PrintErrorModel >= 2) {
+ writer.WriteLine("identifierToPartition:");
+ foreach (KeyValuePair<string!, int> kvp in identifierToPartition) {
+ writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);
+ }
+
+ writer.WriteLine("valueToPartition:");
+ foreach (KeyValuePair<object, int> kvp in valueToPartition) {
+ writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);
+ }
+ writer.WriteLine("End of model.");
+ }
+ }
+ }
+
+
+}
+
+
diff --git a/Source/Provers/Z3/ProverInterface.ssc b/Source/Provers/Z3/ProverInterface.ssc new file mode 100644 index 00000000..02b4f505 --- /dev/null +++ b/Source/Provers/Z3/ProverInterface.ssc @@ -0,0 +1,320 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.IO;
+using System.Text;
+using ExternalProver;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie;
+using Microsoft.Boogie.VCExprAST;
+using Microsoft.Boogie.Clustering;
+using Microsoft.Boogie.TypeErasure;
+using Microsoft.Boogie.Z3;
+using Microsoft.Boogie.Simplify;
+
+namespace Microsoft.Boogie.Z3
+{
+ public class Z3ProcessTheoremProver : ProcessTheoremProver
+ {
+ private Z3InstanceOptions! opts;
+ private Inspector inspector;
+
+ [NotDelayed]
+ public Z3ProcessTheoremProver(VCExpressionGenerator! gen,
+ DeclFreeProverContext! ctx, Z3InstanceOptions! opts)
+ throws UnexpectedProverOutputException;
+ {
+ this.opts = opts;
+ string! backPred = opts.Typed ? "TypedUnivBackPred2.sx" : "UnivBackPred2.sx";
+ base(opts, gen, ctx, opts.ExeName, backPred);
+ }
+
+ private void FireUpInspector()
+ {
+ if (inspector == null && opts.Inspector != null) {
+ inspector = new Inspector(opts);
+ }
+ }
+
+ protected override Microsoft.Boogie.Simplify.ProverProcess! CreateProverProcess(string! proverPath) {
+ opts.ExeName = proverPath;
+ FireUpInspector();
+ if (inspector != null) {
+ inspector.NewProver();
+ }
+ return new Z3ProverProcess(opts, inspector);
+ }
+
+ protected override AxiomVCExprTranslator! SpawnVCExprTranslator() {
+ return new Z3VCExprTranslator(gen, opts);
+ }
+
+ public override void BeginCheck(string! descriptiveName, VCExpr! vc, ErrorHandler! handler)
+ {
+ FireUpInspector();
+ if (inspector != null) {
+ inspector.NewProblem(descriptiveName, vc, handler);
+ }
+ base.BeginCheck(descriptiveName, vc, handler);
+ }
+ }
+
+ public class Z3InstanceOptions : ProverOptions
+ {
+ public int Timeout { get { return TimeLimit / 1000; } }
+ public bool Typed {
+ get {
+ return CommandLineOptions.Clo.Z3types || BitVectors == CommandLineOptions.BvHandling.Z3Native;
+ }
+ }
+ public bool V1 = false;
+ public bool V2 = false; // default set in PostParse
+ public bool DistZ3 = false;
+ public string! ExeName = "z3.exe";
+ public bool InverseImplies = false;
+ public string? Inspector = null;
+
+ protected override bool Parse(string! opt)
+ {
+ return ParseBool(opt, "V1", ref V1) ||
+ ParseBool(opt, "V2", ref V2) ||
+ ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||
+ ParseString(opt, "INSPECTOR", ref Inspector) ||
+ ParseBool(opt, "DIST", ref DistZ3) ||
+ base.Parse(opt);
+ }
+
+ protected override void PostParse()
+ {
+ base.PostParse();
+
+ if (!V1 && !V2) {
+ V2 = true; // default
+ } else if (V1 && V2) {
+ ReportError("V1 and V2 requested at the same time");
+ } else if (V1 && DistZ3) {
+ ReportError("V1 and DistZ3 requested at the same time");
+ }
+ if (V1) {
+ ExeName = "z3-v1.3.exe";
+ }
+ if (DistZ3) {
+ ExeName = "z3-dist.exe";
+ CommandLineOptions.Clo.RestartProverPerVC = true;
+ }
+
+ }
+ }
+
+ internal class Z3LineariserOptions : LineariserOptions {
+ private readonly Z3InstanceOptions! opts;
+
+ public override CommandLineOptions.BvHandling Bitvectors { get {
+ return opts.BitVectors;
+ } }
+
+ internal Z3LineariserOptions(bool asTerm, Z3InstanceOptions !opts, List<VCExprVar!>! letVariables) {
+ base(asTerm);
+ this.opts = opts;
+ this.LetVariablesAttr = letVariables;
+ }
+
+ public override bool UseWeights { get {
+ return opts.V2;
+ } }
+
+ public override bool UseTypes { get {
+ return opts.Typed;
+ } }
+
+ public override bool QuantifierIds { get {
+ return true;
+ } }
+
+ public override bool InverseImplies { get {
+ return opts.InverseImplies;
+ } }
+
+ public override LineariserOptions! SetAsTerm(bool newVal) {
+ if (newVal == AsTerm)
+ return this;
+ return new Z3LineariserOptions(newVal, opts, LetVariables);
+ }
+
+ // variables representing formulas in let-bindings have to be
+ // printed in a different way than other variables
+ private readonly List<VCExprVar!>! LetVariablesAttr;
+ public override List<VCExprVar!>! LetVariables { get {
+ return LetVariablesAttr;
+ } }
+
+ public override LineariserOptions! AddLetVariable(VCExprVar! furtherVar) {
+ List<VCExprVar!>! allVars = new List<VCExprVar!> ();
+ allVars.AddRange(LetVariables);
+ allVars.Add(furtherVar);
+ return new Z3LineariserOptions(AsTerm, opts, allVars);
+ }
+ }
+
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+
+ public class Z3VCExprTranslator : AxiomVCExprTranslator {
+ public Z3VCExprTranslator(VCExpressionGenerator! gen, Z3InstanceOptions! opts) {
+ Gen = gen;
+ Opts = opts;
+ TypeAxiomBuilder! axBuilder;
+ switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+ case CommandLineOptions.TypeEncoding.Arguments:
+ axBuilder = new TypeAxiomBuilderArguments (gen);
+ break;
+ default:
+ axBuilder = new TypeAxiomBuilderPremisses (gen);
+ break;
+ }
+ axBuilder.Setup();
+ AxBuilder = axBuilder;
+ UniqueNamer namer = new UniqueNamer ();
+ Namer = namer;
+ this.DeclCollector =
+ new TypeDeclCollector (namer, opts.BitVectors == CommandLineOptions.BvHandling.Z3Native);
+ }
+
+ private Z3VCExprTranslator(Z3VCExprTranslator! tl) {
+ base(tl);
+ Gen = tl.Gen;
+ Opts = tl.Opts; // we assume that the options have not changed
+ AxBuilder = (TypeAxiomBuilder)tl.AxBuilder.Clone();
+ UniqueNamer namer = (UniqueNamer)tl.Namer.Clone();
+ Namer = namer;
+ DeclCollector = new TypeDeclCollector (namer, tl.DeclCollector);
+ }
+
+ public override Object! Clone() {
+ return new Z3VCExprTranslator(this);
+ }
+
+ private readonly Z3InstanceOptions! Opts;
+ private readonly VCExpressionGenerator! Gen;
+ private readonly TypeAxiomBuilder! AxBuilder;
+ private readonly UniqueNamer! Namer;
+ private readonly TypeDeclCollector! DeclCollector;
+
+ public override string! translate(VCExpr! expr, int polarity) {
+ DateTime start = DateTime.Now;
+ if (CommandLineOptions.Clo.Trace)
+ Console.Write("Linearising ... ");
+
+ // handle the types in the VCExpr
+ TypeEraser eraser;
+ switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+ case CommandLineOptions.TypeEncoding.Arguments:
+ eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, Gen);
+ break;
+ case CommandLineOptions.TypeEncoding.Monomorphic:
+ eraser = null;
+ break;
+ default:
+ eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);
+ break;
+ }
+
+ VCExpr! exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;
+
+ LetBindingSorter! letSorter = new LetBindingSorter(Gen);
+ VCExpr! sortedExpr = letSorter.Mutate(exprWithoutTypes, true);
+ VCExpr! sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);
+
+ if (Opts.Typed) {
+ DeclCollector.Collect(sortedAxioms);
+ DeclCollector.Collect(sortedExpr);
+ FeedTypeDeclsToProver();
+ } else {
+ TermFormulaFlattener! flattener = new TermFormulaFlattener (Gen);
+ sortedExpr = flattener.Flatten(sortedExpr);
+ sortedAxioms = flattener.Flatten(sortedAxioms);
+ }
+
+ //////////////////////////////////////////////////////////////////////////
+ //SubtermCollector! coll = new SubtermCollector (gen);
+ //coll.Traverse(sortedExpr, true);
+ //coll.Traverse(sortedAxioms, true);
+ //coll.UnifyClusters();
+ //Console.WriteLine(coll);
+ //////////////////////////////////////////////////////////////////////////
+
+ LineariserOptions linOptions = new Z3LineariserOptions(false, Opts, new List<VCExprVar!>());
+
+ AddAxiom(SimplifyLikeExprLineariser.ToString(sortedAxioms, linOptions, Namer));
+
+ string! res = SimplifyLikeExprLineariser.ToString(sortedExpr, linOptions, Namer);
+
+ if (CommandLineOptions.Clo.Trace) {
+ TimeSpan elapsed = DateTime.Now - start;
+ Console.WriteLine("finished [{0} s] ", elapsed.TotalSeconds);
+ }
+ return res;
+ }
+
+ private void FeedTypeDeclsToProver() {
+ foreach (string! s in DeclCollector.GetNewDeclarations())
+ AddTypeDecl(s);
+ }
+ }
+
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+ // -----------------------------------------------------------------------------------------------
+
+ public class Factory : ProverFactory
+ {
+
+ public override object! SpawnProver(ProverOptions! popts, object! ctxt)
+ {
+ Z3InstanceOptions opts = (Z3InstanceOptions!)popts;
+ return this.SpawnProver(((DeclFreeProverContext!)ctxt).ExprGen,
+ (DeclFreeProverContext!)ctxt,
+ opts);
+ }
+
+ public override object! NewProverContext(ProverOptions! options) {
+ if (CommandLineOptions.Clo.BracketIdsInVC < 0) {
+ CommandLineOptions.Clo.BracketIdsInVC = 0;
+ }
+
+ Z3InstanceOptions opts = (Z3InstanceOptions!)options;
+ VCExpressionGenerator! gen = new VCExpressionGenerator ();
+ List<string!>! proverCommands = new List<string!> ();
+ proverCommands.Add("all");
+ proverCommands.Add("z3");
+ proverCommands.Add("simplifyLike");
+ if (opts.BitVectors == CommandLineOptions.BvHandling.Z3Native)
+ proverCommands.Add("bvDefSem");
+ if (opts.BitVectors == CommandLineOptions.BvHandling.ToInt)
+ proverCommands.Add("bvInt");
+ VCGenerationOptions! genOptions = new VCGenerationOptions(proverCommands);
+
+ return new DeclFreeProverContext(gen, genOptions);
+ }
+
+ public override ProverOptions! BlankProverOptions()
+ {
+ return new Z3InstanceOptions();
+ }
+
+ protected virtual Z3ProcessTheoremProver! SpawnProver(VCExpressionGenerator! gen,
+ DeclFreeProverContext! ctx,
+ Z3InstanceOptions! opts) {
+ return new Z3ProcessTheoremProver(gen, ctx, opts);
+ }
+ }
+}
diff --git a/Source/Provers/Z3/TypeDeclCollector.ssc b/Source/Provers/Z3/TypeDeclCollector.ssc new file mode 100644 index 00000000..86307b45 --- /dev/null +++ b/Source/Provers/Z3/TypeDeclCollector.ssc @@ -0,0 +1,212 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using Microsoft.Contracts;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.Z3
+{
+ // Visitor for collecting the occurring function symbols in a VCExpr,
+ // and for creating the corresponding declarations that can be fed into
+ // Z3
+
+ // (should this be rather done by Context.DeclareFunction? right now,
+ // the TypeErasure visitor introduces new function symbols that are
+ // not passed to this method)
+
+ public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
+
+ private readonly UniqueNamer! Namer;
+
+ private readonly bool NativeBv;
+
+ public TypeDeclCollector(UniqueNamer! namer, bool nativeBv) {
+ 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> ();
+ }
+
+ internal TypeDeclCollector(UniqueNamer! namer, TypeDeclCollector! coll) {
+ 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);
+ }
+
+ // not used
+ protected override bool StandardResult(VCExpr! node, bool arg) {
+ return true;
+ }
+
+ private readonly List<string!>! AllDecls;
+ private readonly List<string!>! IncDecls;
+
+ 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;
+
+ // the names of registered BvConcatOps and BvExtractOps
+ private readonly IDictionary<string!, bool>! KnownBvOps;
+
+ public List<string!>! AllDeclarations { get {
+ List<string!>! res = new List<string!> ();
+ res.AddRange(AllDecls);
+ return res;
+ } }
+
+ public List<string!>! GetNewDeclarations() {
+ List<string!>! res = new List<string!> ();
+ res.AddRange(IncDecls);
+ IncDecls.Clear();
+ return res;
+ }
+
+ private void AddDeclaration(string! decl) {
+ AllDecls.Add(decl);
+ IncDecls.Add(decl);
+ }
+
+ public void Collect(VCExpr! expr) {
+ Traverse(expr, true);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+
+ private static string! TypeToString(Type! t) {
+ return SimplifyLikeExprLineariser.TypeToString(t);
+ }
+
+ private void RegisterType(Type! type)
+ {
+ if (!type.IsBv || !NativeBv) return;
+
+ if (!KnownTypes.ContainsKey(type)) {
+ int bits = type.BvBits;
+ string name = TypeToString(type);
+
+ AddDeclaration("(DEFTYPE " + name + " :BUILTIN BitVec " + bits + ")");
+ // If we add the BUILTIN then the conversion axiom does not work
+ AddDeclaration("(DEFOP " + name + "_to_int " + name + " $int)"); // :BUILTIN bv2int $int)");
+ AddDeclaration("(DEFOP $make_bv" + bits + " $int " + name + " :BUILTIN int2bv " + bits + ")");
+ string! expr = "($make_bv" + bits + " (" + name + "_to_int x))";
+ AddDeclaration("(BG_PUSH (FORALL (x :TYPE " + name + ") (PATS "
+ + expr + ") (QID bvconv" + bits + ") (EQ " + expr + " x)))");
+
+ KnownTypes.Add(type, true);
+ }
+ }
+
+ public override bool Visit(VCExprNAry! node, bool arg) {
+ // there are a couple of cases where operators have to be
+ // registered by generating appropriate Z3 statements
+
+ if (node.Op.Equals(VCExpressionGenerator.BvConcatOp)) {
+ //
+ if (NativeBv) {
+ RegisterType(node[0].Type);
+ RegisterType(node[1].Type);
+ RegisterType(node.Type);
+
+ string name = SimplifyLikeExprLineariser.BvConcatOpName(node);
+ if (!KnownBvOps.ContainsKey(name)) {
+ AddDeclaration("(DEFOP " + name +
+ " " + TypeToString(node[0].Type) +
+ " " + TypeToString(node[1].Type) +
+ " " + TypeToString(node.Type) +
+ " :BUILTIN concat)");
+ KnownBvOps.Add(name, true);
+ }
+ }
+ //
+ } else if (node.Op is VCExprBvExtractOp) {
+ //
+ if (NativeBv) {
+ RegisterType(node[0].Type);
+ RegisterType(node.Type);
+
+ VCExprBvExtractOp! op = (VCExprBvExtractOp)node.Op;
+ string name = SimplifyLikeExprLineariser.BvExtractOpName(node);
+ if (!KnownBvOps.ContainsKey(name)) {
+ AddDeclaration("(DEFOP " + name +
+ " " + TypeToString(node[0].Type) +
+ " " + TypeToString(node.Type) +
+ " :BUILTIN extract " +
+ (op.End - 1) + " " + op.Start + ")");
+ KnownBvOps.Add(name, true);
+ }
+ }
+ //
+ } else {
+ //
+ 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) {
+ decl += " " + TypeToString(v.TypedIdent.Type);
+ RegisterType(v.TypedIdent.Type);
+ }
+ assert f.OutParams.Length == 1;
+ foreach (Variable! v in f.OutParams) {
+ decl += " " + TypeToString(v.TypedIdent.Type);
+ RegisterType(v.TypedIdent.Type);
+ }
+
+ string? builtin = ExtractBuiltin(f);
+ if (builtin != null)
+ decl += " :BUILTIN " + builtin;
+
+ decl += ")";
+
+ AddDeclaration(decl);
+ KnownFunctions.Add(f, true);
+ }
+ //
+ }
+
+ return base.Visit(node, arg);
+ }
+
+ private string? ExtractBuiltin(Function! f) {
+ if (NativeBv) {
+ return f.FindStringAttribute("bvbuiltin");
+ } else {
+ return null;
+ }
+ }
+
+ public override bool Visit(VCExprVar! node, bool arg) {
+ if (!BoundTermVars.Contains(node) && !KnownVariables.ContainsKey(node)) {
+ RegisterType(node.Type);
+ string! printedName = Namer.GetName(node, node.Name);
+ string! decl =
+ "(DEFOP " + SimplifyLikeExprLineariser.MakeIdPrintable(printedName)
+ + " " + TypeToString(node.Type) + ")";
+ AddDeclaration(decl);
+ KnownVariables.Add(node, true);
+ }
+
+ return base.Visit(node, arg);
+ }
+ }
+
+}
\ No newline at end of file diff --git a/Source/Provers/Z3/Z3.sscproj b/Source/Provers/Z3/Z3.sscproj new file mode 100644 index 00000000..5370a640 --- /dev/null +++ b/Source/Provers/Z3/Z3.sscproj @@ -0,0 +1,140 @@ +<?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"
+ />
+ </Include>
+ </Files>
+ </XEN>
+</VisualStudioProject>
\ No newline at end of file |