summaryrefslogtreecommitdiff
path: root/Source/Provers/Z3/Inspector.ssc
diff options
context:
space:
mode:
authorGravatar mikebarnett <unknown>2009-07-15 21:03:41 +0000
committerGravatar mikebarnett <unknown>2009-07-15 21:03:41 +0000
commitce1c2de044c91624370411e23acab13b0381949b (patch)
tree592539996fe08050ead5ee210c973801611dde40 /Source/Provers/Z3/Inspector.ssc
Initial set of files.
Diffstat (limited to 'Source/Provers/Z3/Inspector.ssc')
-rw-r--r--Source/Provers/Z3/Inspector.ssc130
1 files changed, 130 insertions, 0 deletions
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();
+ }
+ }
+}