diff options
Diffstat (limited to 'Source/Provers/SMTLib/Inspector.cs')
-rw-r--r-- | Source/Provers/SMTLib/Inspector.cs | 314 |
1 files changed, 157 insertions, 157 deletions
diff --git a/Source/Provers/SMTLib/Inspector.cs b/Source/Provers/SMTLib/Inspector.cs index 362502f3..13a2076e 100644 --- a/Source/Provers/SMTLib/Inspector.cs +++ b/Source/Provers/SMTLib/Inspector.cs @@ -1,157 +1,157 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.IO;
-using System.Diagnostics;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-//using util;
-using Microsoft.Boogie;
-using Microsoft.Basetypes;
-using Microsoft.Boogie.VCExprAST;
-
-namespace Microsoft.Boogie.SMTLib
-{
- internal class FindLabelsVisitor : TraversingVCExprVisitor<bool, bool> {
- public HashSet<string/*!*/>/*!*/ Labels = new HashSet<string/*!*/>();
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(cce.NonNull(Labels));
- }
-
-
- public static HashSet<string/*!*/>/*!*/ FindLabels(VCExpr/*!*/ expr) {
- Contract.Requires(expr != null);
- Contract.Ensures(cce.NonNull(Contract.Result<HashSet<string/*!*/>/*!*/>()));
-
- FindLabelsVisitor visitor = new FindLabelsVisitor();
- visitor.Traverse(expr, true);
- return visitor.Labels;
- }
-
- protected override bool StandardResult(VCExpr node, bool arg) {
- //Contract.Requires(node!=null);
- VCExprNAry nary = node as VCExprNAry;
- if (nary != null) {
- VCExprLabelOp lab = nary.Op as VCExprLabelOp;
- if (lab != null) {
- Labels.Add(lab.label);
- }
- }
- return true;
- }
- }
-
- internal class Inspector {
- [Rep] protected readonly Process inspector;
- [Rep] readonly TextReader fromInspector;
- [Rep] readonly TextWriter toInspector;
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(inspector!=null);
- Contract.Invariant(fromInspector!=null);
- Contract.Invariant(toInspector != null);
- }
-
-
- public Inspector(SMTLibProverOptions opts)
- {
- Contract.Requires(opts != null);
- ProcessStartInfo psi = new ProcessStartInfo(opts.Inspector);
- Contract.Assert(psi!=null);
- 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 NewProblem(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler)
- {
- Contract.Requires(descriptiveName != null);
- Contract.Requires(vc != null);
- Contract.Requires(handler != null);
- HashSet<string/*!*/>/*!*/ labels = FindLabelsVisitor.FindLabels(vc);
- Contract.Assert(labels!=null);
- toInspector.WriteLine("PROBLEM " + descriptiveName);
- toInspector.WriteLine("TOKEN BEGIN");
- foreach (string lab in labels) {
- Contract.Assert(lab!=null);
- string no = lab.Substring(1);
- Absy absy = handler.Label2Absy(no);
-
- IToken tok = absy.tok;
- AssertCmd assrt = absy as AssertCmd;
- Block blk = absy as Block;
- string val = tok.val; // might require computation, so cache it
- if (val == "foo" || tok.filename == null) continue; // no token
-
- 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 {
- Contract.Assume( false);
- }
- if (val == null || val == "assert" || val == "ensures") { val = ""; }
-
- if (absy is LoopInitAssertCmd) {
- val += " (loop entry)";
- } else if (absy is LoopInvMaintainedAssertCmd) {
- val += " (loop body)";
- } else if (val.IndexOf("#VCCERR") >= 0) {
- // skip further transformations
- } else if (absy is AssertRequiresCmd) {
- AssertRequiresCmd req = (AssertRequiresCmd)absy;
- IToken t2 = req.Requires.tok;
- string tval = t2.val;
- if (tval == "requires")
- tval = string.Format("{0}({1},{2}))", t2.filename, t2.line, t2.col);
- string call = "";
- if (val != "call") call = " in call to " + val;
- val = string.Format("precondition {0}{1}", tval, call);
- }
-
- 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)
- {
- Contract.Requires(line != null);
- toInspector.WriteLine(line);
- toInspector.Flush();
- }
- }
-}
+//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.IO; +using System.Diagnostics; +using System.Collections; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +//using util; +using Microsoft.Boogie; +using Microsoft.Basetypes; +using Microsoft.Boogie.VCExprAST; + +namespace Microsoft.Boogie.SMTLib +{ + internal class FindLabelsVisitor : TraversingVCExprVisitor<bool, bool> { + public HashSet<string/*!*/>/*!*/ Labels = new HashSet<string/*!*/>(); + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNull(Labels)); + } + + + public static HashSet<string/*!*/>/*!*/ FindLabels(VCExpr/*!*/ expr) { + Contract.Requires(expr != null); + Contract.Ensures(cce.NonNull(Contract.Result<HashSet<string/*!*/>/*!*/>())); + + FindLabelsVisitor visitor = new FindLabelsVisitor(); + visitor.Traverse(expr, true); + return visitor.Labels; + } + + protected override bool StandardResult(VCExpr node, bool arg) { + //Contract.Requires(node!=null); + VCExprNAry nary = node as VCExprNAry; + if (nary != null) { + VCExprLabelOp lab = nary.Op as VCExprLabelOp; + if (lab != null) { + Labels.Add(lab.label); + } + } + return true; + } + } + + internal class Inspector { + [Rep] protected readonly Process inspector; + [Rep] readonly TextReader fromInspector; + [Rep] readonly TextWriter toInspector; + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(inspector!=null); + Contract.Invariant(fromInspector!=null); + Contract.Invariant(toInspector != null); + } + + + public Inspector(SMTLibProverOptions opts) + { + Contract.Requires(opts != null); + ProcessStartInfo psi = new ProcessStartInfo(opts.Inspector); + Contract.Assert(psi!=null); + 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 NewProblem(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) + { + Contract.Requires(descriptiveName != null); + Contract.Requires(vc != null); + Contract.Requires(handler != null); + HashSet<string/*!*/>/*!*/ labels = FindLabelsVisitor.FindLabels(vc); + Contract.Assert(labels!=null); + toInspector.WriteLine("PROBLEM " + descriptiveName); + toInspector.WriteLine("TOKEN BEGIN"); + foreach (string lab in labels) { + Contract.Assert(lab!=null); + string no = lab.Substring(1); + Absy absy = handler.Label2Absy(no); + + IToken tok = absy.tok; + AssertCmd assrt = absy as AssertCmd; + Block blk = absy as Block; + string val = tok.val; // might require computation, so cache it + if (val == "foo" || tok.filename == null) continue; // no token + + 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 { + Contract.Assume( false); + } + if (val == null || val == "assert" || val == "ensures") { val = ""; } + + if (absy is LoopInitAssertCmd) { + val += " (loop entry)"; + } else if (absy is LoopInvMaintainedAssertCmd) { + val += " (loop body)"; + } else if (val.IndexOf("#VCCERR") >= 0) { + // skip further transformations + } else if (absy is AssertRequiresCmd) { + AssertRequiresCmd req = (AssertRequiresCmd)absy; + IToken t2 = req.Requires.tok; + string tval = t2.val; + if (tval == "requires") + tval = string.Format("{0}({1},{2}))", t2.filename, t2.line, t2.col); + string call = ""; + if (val != "call") call = " in call to " + val; + val = string.Format("precondition {0}{1}", tval, call); + } + + 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) + { + Contract.Requires(line != null); + toInspector.WriteLine(line); + toInspector.Flush(); + } + } +} |