From 076a19dcb301759813af468478a36e530183b76e Mon Sep 17 00:00:00 2001 From: tabarbe Date: Thu, 22 Jul 2010 21:25:01 +0000 Subject: Boogie: Committing my port of the SMTLib project --- Source/Provers/SMTLib/ProverInterface.cs | 172 +++++++++++++++++++++---------- 1 file changed, 119 insertions(+), 53 deletions(-) (limited to 'Source/Provers/SMTLib/ProverInterface.cs') diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index b55cc403..4b4d7431 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -8,9 +8,9 @@ using System.Collections; using System.Collections.Generic; using System.Threading; using System.IO; -using ExternalProver; +//using ExternalProver; using System.Diagnostics; -using Microsoft.Contracts; +using System.Diagnostics.Contracts; using Microsoft.Boogie.AbstractInterpretation; using Microsoft.Boogie; using Microsoft.Boogie.VCExprAST; @@ -22,17 +22,35 @@ namespace Microsoft.Boogie.SMTLib { public class SMTLibProcessTheoremProver : LogProverInterface { - private readonly DeclFreeProverContext! ctx; + private readonly DeclFreeProverContext ctx; + [ContractInvariantMethod] +void ObjectInvariant() +{ + Contract.Invariant(ctx!=null); + Contract.Invariant(AxBuilder != null); + Contract.Invariant(Namer != null); + Contract.Invariant(DeclCollector != null); + Contract.Invariant(BadBenchmarkWords != null); + Contract.Invariant(cce.NonNullElements(Axioms)); + Contract.Invariant(cce.NonNullElements(TypeDecls)); + Contract.Invariant(_backgroundPredicates != null); + +} + + [NotDelayed] - public SMTLibProcessTheoremProver(ProverOptions! options, VCExpressionGenerator! gen, - DeclFreeProverContext! ctx) + public SMTLibProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen, + DeclFreeProverContext ctx):base(options, "", "", "", "", gen) { + Contract.Requires(options != null); + Contract.Requires(gen != null); + Contract.Requires(ctx != null); InitializeGlobalInformation("UnivBackPred2.smt"); this.ctx = ctx; - TypeAxiomBuilder! axBuilder; + TypeAxiomBuilder axBuilder; switch (CommandLineOptions.Clo.TypeEncodingMethod) { case CommandLineOptions.TypeEncoding.Arguments: axBuilder = new TypeAxiomBuilderArguments (gen); @@ -46,27 +64,36 @@ namespace Microsoft.Boogie.SMTLib UniqueNamer namer = new UniqueNamer (); Namer = namer; this.DeclCollector = new TypeDeclCollector (namer); - base(options, "", "", "", "", gen); + } - public override ProverContext! Context { get { + public override ProverContext Context { get { + Contract.Ensures(Contract.Result() != null); + return ctx; } } - private readonly TypeAxiomBuilder! AxBuilder; - private readonly UniqueNamer! Namer; - private readonly TypeDeclCollector! DeclCollector; + private readonly TypeAxiomBuilder AxBuilder; + private readonly UniqueNamer Namer; + private readonly TypeDeclCollector DeclCollector; private void FeedTypeDeclsToProver() { - foreach (string! s in DeclCollector.GetNewDeclarations()) + foreach (string s in DeclCollector.GetNewDeclarations()) + { + Contract.Assert(s!=null); AddTypeDecl(s); - } + }} - public override void BeginCheck(string! descriptiveName, VCExpr! vc, ErrorHandler! handler) { - TextWriter! output = OpenOutputFile(descriptiveName); + public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) { + Contract.Requires(descriptiveName != null); + Contract.Requires(vc != null); + Contract.Requires(handler != null); + TextWriter output = OpenOutputFile(descriptiveName); + Contract.Assert(output!=null); - string! name = + string name = MakeBenchmarkNameSafe(SMTLibExprLineariser.MakeIdPrintable(descriptiveName)); + Contract.Assert(name!=null); WriteLineAndLog(output, "(benchmark " + name); WriteLineAndLog(output, _backgroundPredicates); @@ -76,13 +103,16 @@ namespace Microsoft.Boogie.SMTLib } string vcString = ":formula (not " + VCExpr2String(vc, 1) + ")"; - string! prelude = ctx.GetProverCommands(true); + string prelude = ctx.GetProverCommands(true); + Contract.Assert(prelude!=null); WriteLineAndLog(output, prelude); - foreach (string! s in TypeDecls) { + foreach (string s in TypeDecls) { + Contract.Assert(s!=null); WriteLineAndLog(output, s); } - foreach (string! s in Axioms) { + foreach (string s in Axioms) { + Contract.Assert(s!=null); WriteLineAndLog(output, ":assumption"); WriteLineAndLog(output, s); } @@ -95,41 +125,53 @@ namespace Microsoft.Boogie.SMTLib // certain words that should not occur in the name of a benchmark // because some solvers don't like them - private readonly static List! BadBenchmarkWords = new List (); + private readonly static List!*/> BadBenchmarkWords = new List (); static SMTLibProcessTheoremProver() { BadBenchmarkWords.Add("Array"); BadBenchmarkWords.Add("Arrray"); } - private string! MakeBenchmarkNameSafe(string! name) { + private string MakeBenchmarkNameSafe(string name) { + Contract.Requires(name != null); + Contract.Ensures(Contract.Result() != null); + 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) { + private TextWriter OpenOutputFile(string descriptiveName) { + Contract.Requires(descriptiveName != null); + Contract.Ensures(Contract.Result() != null); + string filename = CommandLineOptions.Clo.SMTLibOutputPath; - filename = Helpers.SubstituteAtPROC(descriptiveName, (!)filename); + filename = Helpers.SubstituteAtPROC(descriptiveName, cce.NonNull(filename)); return new StreamWriter(filename, false); } - private void WriteLineAndLog(TextWriter! output, string! msg) { + private void WriteLineAndLog(TextWriter output, string msg) { + Contract.Requires(output != null); + Contract.Requires(msg != null); LogActivity(msg); output.WriteLine(msg); } [NoDefaultContract] - public override Outcome CheckOutcome(ErrorHandler! handler) - throws UnexpectedProverOutputException; { + public override Outcome CheckOutcome(ErrorHandler handler) + {Contract.Requires(handler != null); + Contract.EnsuresOnThrow(true); return Outcome.Undetermined; } - protected string! VCExpr2String(VCExpr! expr, int polarity) { + protected string VCExpr2String(VCExpr expr, int polarity) { + Contract.Requires(expr != null); + Contract.Ensures(Contract.Result() != null); + DateTime start = DateTime.Now; if (CommandLineOptions.Clo.Trace) Console.Write("Linearising ... "); // handle the types in the VCExpr - TypeEraser! eraser; + TypeEraser eraser; switch (CommandLineOptions.Clo.TypeEncodingMethod) { case CommandLineOptions.TypeEncoding.Arguments: eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, gen); @@ -138,18 +180,24 @@ namespace Microsoft.Boogie.SMTLib eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, gen); break; } - VCExpr! exprWithoutTypes = eraser.Erase(expr, polarity); + Contract.Assert(eraser!=null); + VCExpr exprWithoutTypes = eraser.Erase(expr, polarity); + Contract.Assert(exprWithoutTypes!=null); - LetBindingSorter! letSorter = new LetBindingSorter(gen); - VCExpr! sortedExpr = letSorter.Mutate(exprWithoutTypes, true); - VCExpr! sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true); + LetBindingSorter letSorter = new LetBindingSorter(gen); + Contract.Assert(letSorter!=null); + VCExpr sortedExpr = letSorter.Mutate(exprWithoutTypes, true); + Contract.Assert(sortedExpr!=null); + VCExpr sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true); + Contract.Assert(sortedAxioms!=null); DeclCollector.Collect(sortedAxioms); DeclCollector.Collect(sortedExpr); FeedTypeDeclsToProver(); AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer)); - string! res = SMTLibExprLineariser.ToString(sortedExpr, Namer); + string res = SMTLibExprLineariser.ToString(sortedExpr, Namer); + Contract.Assert(res!=null); if (CommandLineOptions.Clo.Trace) { DateTime end = DateTime.Now; @@ -161,13 +209,17 @@ namespace Microsoft.Boogie.SMTLib // the list of all known axioms, where have to be included in each // verification condition - private readonly List! Axioms = new List (); + private readonly List!*/> Axioms = new List (); private bool AxiomsAreSetup = false; + + + // similarly, a list of function/predicate declarations - private readonly List! TypeDecls = new List (); + private readonly List!*/> TypeDecls = new List (); - protected void AddAxiom(string! axiom) { + protected void AddAxiom(string axiom) { + Contract.Requires(axiom != null); Axioms.Add(axiom); // if (thmProver != null) { // LogActivity(":assume " + axiom); @@ -175,7 +227,8 @@ namespace Microsoft.Boogie.SMTLib // } } - protected void AddTypeDecl(string! decl) { + protected void AddTypeDecl(string decl) { + Contract.Requires(decl != null); TypeDecls.Add(decl); // if (thmProver != null) { // LogActivity(decl); @@ -185,15 +238,15 @@ namespace Microsoft.Boogie.SMTLib //////////////////////////////////////////////////////////////////////////// - private static string! _backgroundPredicates; + private static string _backgroundPredicates; - static void InitializeGlobalInformation(string! backgroundPred) - ensures _backgroundPredicates != null; + static void InitializeGlobalInformation(string backgroundPred) + {Contract.Requires(backgroundPred != null); + Contract.Ensures(_backgroundPredicates != null); //throws ProverException, System.IO.FileNotFoundException; - { if (_backgroundPredicates == null) { - string! codebaseString = - (!) Path.GetDirectoryName((!)System.Reflection.Assembly.GetExecutingAssembly().Location); + string codebaseString = + cce.NonNull(Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location))); // Initialize '_backgroundPredicates' string univBackPredPath = Path.Combine(codebaseString, backgroundPred); @@ -208,32 +261,45 @@ namespace Microsoft.Boogie.SMTLib public class Factory : ProverFactory { - public override object! SpawnProver(ProverOptions! options, object! ctxt) + public override object SpawnProver(ProverOptions options, object ctxt) { + Contract.Requires(ctxt != null); + Contract.Requires(options != null); + Contract.Ensures(Contract.Result() != null); + return this.SpawnProver(options, - ((DeclFreeProverContext!)ctxt).ExprGen, - (DeclFreeProverContext!)ctxt); + cce.NonNull((DeclFreeProverContext)ctxt).ExprGen, + cce.NonNull((DeclFreeProverContext)ctxt)); } - public override object! NewProverContext(ProverOptions! options) { + public override object NewProverContext(ProverOptions options) { + Contract.Requires(options != null); + Contract.Ensures(Contract.Result() != null); + if (CommandLineOptions.Clo.BracketIdsInVC < 0) { CommandLineOptions.Clo.BracketIdsInVC = 0; } - VCExpressionGenerator! gen = new VCExpressionGenerator (); - List! proverCommands = new List (); + VCExpressionGenerator gen = new VCExpressionGenerator (); + List/*!>!*/ proverCommands = new List (); // TODO: what is supported? // proverCommands.Add("all"); // proverCommands.Add("simplify"); // proverCommands.Add("simplifyLike"); - VCGenerationOptions! genOptions = new VCGenerationOptions(proverCommands); + VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands); + Contract.Assert(genOptions!=null); return new DeclFreeProverContext(gen, genOptions); } - protected virtual SMTLibProcessTheoremProver! SpawnProver(ProverOptions! options, - VCExpressionGenerator! gen, - DeclFreeProverContext! ctx) { + protected virtual SMTLibProcessTheoremProver SpawnProver(ProverOptions options, + VCExpressionGenerator gen, + DeclFreeProverContext ctx) { + Contract.Requires(options != null); + Contract.Requires(gen != null); + Contract.Requires(ctx != null); + Contract.Ensures(Contract.Result() != null); + return new SMTLibProcessTheoremProver(options, gen, ctx); } } -- cgit v1.2.3