diff options
-rw-r--r-- | Source/Boogie.sln | 7 | ||||
-rw-r--r-- | Source/Provers/Isabelle/AssemblyInfo.ssc | 17 | ||||
-rw-r--r-- | Source/Provers/Isabelle/Isabelle.sscproj | 99 | ||||
-rw-r--r-- | Source/Provers/Isabelle/Prover.ssc | 835 |
4 files changed, 958 insertions, 0 deletions
diff --git a/Source/Boogie.sln b/Source/Boogie.sln index 40c39af5..dda05546 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -37,6 +37,8 @@ Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "BoogieDriver", "BoogieDrive {47BC34F1-A173-40BE-84C2-9332B4418387} = {47BC34F1-A173-40BE-84C2-9332B4418387}
EndProjectSection
EndProject
+Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "Isabelle", "Provers\Isabelle\Isabelle.sscproj", "{C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}"
+EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Debug|.NET = Debug|.NET
@@ -87,6 +89,10 @@ Global {D2B98E4A-2EAB-4065-ABFA-709AC5CA7D4C}.Debug|.NET.Build.0 = Debug|.NET
{D2B98E4A-2EAB-4065-ABFA-709AC5CA7D4C}.Release|.NET.ActiveCfg = Release|.NET
{D2B98E4A-2EAB-4065-ABFA-709AC5CA7D4C}.Release|.NET.Build.0 = Release|.NET
+ {C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}.Debug|.NET.ActiveCfg = Debug|.NET
+ {C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}.Debug|.NET.Build.0 = Debug|.NET
+ {C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}.Release|.NET.ActiveCfg = Release|.NET
+ {C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36}.Release|.NET.Build.0 = Release|.NET
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
@@ -95,5 +101,6 @@ Global {F75666DE-FB56-457C-8782-09BE243450FC} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
{F75666DE-CD56-457C-8782-09BE243450FC} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
{13C3A68C-462A-4CDA-A480-738046E37C5A} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
+ {C3C3BC4F-6AEB-41AB-A649-4A085DC6FB36} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
EndGlobalSection
EndGlobal
diff --git a/Source/Provers/Isabelle/AssemblyInfo.ssc b/Source/Provers/Isabelle/AssemblyInfo.ssc new file mode 100644 index 00000000..df4952da --- /dev/null +++ b/Source/Provers/Isabelle/AssemblyInfo.ssc @@ -0,0 +1,17 @@ +// Written by Sascha Boehme, TU Muenchen, 2009
+
+using System.Reflection;
+using System.Runtime.CompilerServices;
+
+[assembly: AssemblyVersion("4.0.0.0")]
+[assembly: AssemblyFileVersion("4.0.0.0")]
+
+[assembly: AssemblyTitle("Boogie back-end for Isabelle")]
+[assembly: AssemblyDescription("Boogie back-end for the interactive"
+ + " theorem prover Isabelle")]
+[assembly: AssemblyConfiguration("Release")]
+[assembly: AssemblyCompany("TU München")]
+[assembly: AssemblyProduct("HOL-Boogie")]
+[assembly: AssemblyCopyright("Copyright © TU München 2009")]
+[assembly: AssemblyTrademark("")]
+[assembly: AssemblyCulture("")]
diff --git a/Source/Provers/Isabelle/Isabelle.sscproj b/Source/Provers/Isabelle/Isabelle.sscproj new file mode 100644 index 00000000..0e4a5c58 --- /dev/null +++ b/Source/Provers/Isabelle/Isabelle.sscproj @@ -0,0 +1,99 @@ +<?xml version="1.0" encoding="utf-8"?>
+<VisualStudioProject>
+ <XEN ProjectType="Local"
+ SchemaVersion="1.0"
+ Name="Isabelle"
+ ProjectGuid="c3c3bc4f-6aeb-41ab-a649-4a085dc6fb36"
+ >
+ <Build>
+ <Settings ApplicationIcon=""
+ AssemblyName="Provers.Isabelle"
+ OutputType="Library"
+ RootNamespace="Microsoft.Boogie.Isabelle"
+ 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="true"
+ />
+ <Reference Name="System.Data"
+ AssemblyName="System.Data"
+ Private="true"
+ />
+ <Reference Name="System.Xml"
+ AssemblyName="System.Xml"
+ 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"
+ />
+ </References>
+ </Build>
+ <Files>
+ <Include>
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="AssemblyInfo.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="Prover.ssc"
+ />
+ </Include>
+ </Files>
+ </XEN>
+</VisualStudioProject>
\ No newline at end of file diff --git a/Source/Provers/Isabelle/Prover.ssc b/Source/Provers/Isabelle/Prover.ssc new file mode 100644 index 00000000..02bd2d36 --- /dev/null +++ b/Source/Provers/Isabelle/Prover.ssc @@ -0,0 +1,835 @@ +/*
+Copyright (c) 2009, Sascha Boehme, Technische Universitaet Muenchen
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+* Redistributions of source code must retain the above copyright notice, this
+ list of conditions and the following disclaimer.
+* Redistributions in binary form must reproduce the above copyright notice,
+ this list of conditions and the following disclaimer in the documentation
+ and/or other materials provided with the distribution.
+* Neither the name of the Technische Universitaet Muenchen nor the names of
+ its contributors may be used to endorse or promote products derived from
+ this software without specific prior written permission.
+ +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE +ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE +LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR +CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF +SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS +INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN +CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) +ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +POSSIBILITY OF SUCH DAMAGE. +*/
+
+using System;
+using System.IO;
+using System.Collections.Generic;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.Isabelle
+{
+ public class IsabelleProverOptions : ProverOptions
+ {
+ private string filename = null;
+ public string! Filename = "";
+
+ public bool AllTypes = false;
+
+ protected override bool Parse(string! opt)
+ {
+ bool v2 = false;
+ return
+ ParseString(opt, "ISABELLE_INPUT", ref filename) ||
+ ParseBool(opt, "ISABELLE_FULL", ref AllTypes) ||
+ ParseBool(opt, "V2", ref v2) ||
+ base.Parse(opt);
+ }
+
+ protected override void PostParse()
+ {
+ base.PostParse();
+
+ if (filename == null)
+ {
+ ReportError("Missing ISABELLE_INPUT option. " +
+ "This option expects a filename (with extension .b2i).");
+ }
+ else if (!Path.GetExtension(filename).Equals(".b2i"))
+ {
+ filename = Path.ChangeExtension(filename, ".b2i");
+ }
+ Filename = (string!) filename;
+ }
+ }
+
+
+ public class Factory : ProverFactory
+ {
+ private static int index = 0;
+
+ public override ProverOptions! BlankProverOptions()
+ {
+ return new IsabelleProverOptions();
+ }
+
+ public override object! NewProverContext(ProverOptions! options)
+ {
+ IsabelleProverOptions opts = (IsabelleProverOptions) options;
+ string! filename = opts.Filename;
+ lock (this)
+ {
+ if (index > 0)
+ {
+ filename = Path.ChangeExtension(filename, "." + index + ".b2i");
+ }
+ index++;
+ if (File.Exists(filename)) { File.Delete(filename); }
+ }
+ return new IsabelleContext(filename, opts.AllTypes);
+ }
+
+ public override object! SpawnProver(ProverOptions! options, object! ctxt)
+ {
+ return new IsabelleInterface((ProverContext!) ctxt);
+ }
+
+ // we prefer DAG outputs over LET
+ public override bool SupportsDags { get { return true; } }
+
+ // this works well in Isabelle, but we do not get structural information
+ public override CommandLineOptions.VCVariety DefaultVCVariety
+ {
+ get { return CommandLineOptions.VCVariety.Dag; }
+ }
+ }
+
+
+ public class IsabelleInterface : ProverInterface
+ {
+ private static Dictionary<string!, int>! lastVCIndex =
+ new Dictionary<string!, int>();
+
+ private IsabelleContext! ctxt;
+
+ public IsabelleInterface(ProverContext! ctxt)
+ {
+ this.ctxt = (IsabelleContext!) ctxt;
+ }
+ public override ProverContext! Context { get { return ctxt; } }
+ public override VCExpressionGenerator! VCExprGen
+ {
+ get { return ctxt.ExprGen; }
+ }
+
+ public override void BeginCheck(string! name, VCExpr! vc, ErrorHandler! h)
+ {
+ int index;
+ lock (lastVCIndex)
+ {
+ lastVCIndex.TryGetValue(name, out index);
+ index++;
+ lastVCIndex[name] = index;
+ }
+ lock (ctxt) { ctxt.AddVC(name + " " + index, vc, h); }
+ }
+ public override Outcome CheckOutcome(ErrorHandler! handler)
+ {
+ return Outcome.Undetermined; // we will check the goal later in Isabelle
+ }
+ }
+
+
+ public class IsabelleContext : ProverContext
+ {
+ private VCExpressionGenerator! gen;
+ private Boogie2VCExprTranslator! trans;
+ private VCGenerationOptions! options;
+ private List<string!>! declaredFunctions = new List<string!>();
+ public readonly string! OutputFilename;
+ public bool IsFunctionDeclared(string! name)
+ {
+ return declaredFunctions.Contains(name);
+ }
+ public readonly bool AllTypes;
+
+ public IsabelleContext(string! outputFilename, bool allTypes)
+ {
+ List<string!>! solverAttributes = new List<string!>();
+ solverAttributes.Add("bvInt");
+ solverAttributes.Add("bvDefSem");
+ solverAttributes.Add("bvint");
+ solverAttributes.Add("bvz");
+ solverAttributes.Add("external");
+ // add more solver attributes, if needed
+ VCGenerationOptions! opts = new VCGenerationOptions(solverAttributes);
+ VCExpressionGenerator! gen = new VCExpressionGenerator();
+ trans = new Boogie2VCExprTranslator(gen, opts);
+ this.gen = gen;
+ this.options = opts;
+ this.OutputFilename = outputFilename;
+ this.AllTypes = allTypes;
+ }
+ public override VCExpressionGenerator! ExprGen { get { return gen; } }
+ public override Boogie2VCExprTranslator! BoogieExprTranslator
+ {
+ get { return trans; }
+ }
+ public override VCGenerationOptions! VCGenOptions
+ {
+ get { return options; }
+ }
+ public override object! Clone() { return this; }
+
+ public override void DeclareType(TypeCtorDecl! t, string atts)
+ {
+ B2I! b2i = new B2I(this);
+ b2i.Write(B2I.Kind.TypeDecl, t.Name + " " + t.Arity + " " +
+ B2I.CountOf(t.Attributes));
+ b2i.Indent(2);
+ b2i.Write(t.Attributes, BoogieExprTranslator);
+ b2i.Close();
+ }
+
+ public override void DeclareConstant(Constant! c, bool uniq, string atts)
+ {
+ QKeyValue attributes = c.Attributes;
+ if (c.Unique) { attributes = B2I.Add("unique", null, attributes); }
+ declaredFunctions.Add(c.Name);
+
+ B2I! b2i = new B2I(this);
+ if (AllTypes)
+ {
+ b2i.Write(B2I.Kind.FunDecl, c.Name + " 0 1 " +
+ B2I.CountOf(attributes));
+ }
+ else
+ {
+ b2i.Write(B2I.Kind.FunDecl, c.Name + " 1 " + B2I.CountOf(attributes));
+ }
+ b2i.Indent(4);
+ b2i.Write(c.TypedIdent.Type);
+ b2i.Unindent();
+ b2i.Indent(2);
+ b2i.Write(attributes, BoogieExprTranslator);
+ b2i.Close();
+ }
+
+ public override void DeclareFunction(Function! f, string atts)
+ {
+ declaredFunctions.Add(f.Name);
+
+ B2I! b2i = new B2I(this);
+ if (AllTypes)
+ {
+ b2i.Write(B2I.Kind.FunDecl, f.Name + " " + f.TypeParameters.Length +
+ " " + (f.InParams.Length + 1) + " " + B2I.CountOf(f.Attributes));
+ b2i.Indent(4);
+ foreach (TypeVariable! v in f.TypeParameters) { b2i.Write(v); }
+ b2i.Unindent();
+ }
+ else
+ {
+ b2i.Write(B2I.Kind.FunDecl, f.Name + " " + (f.InParams.Length + 1) +
+ " " + B2I.CountOf(f.Attributes));
+ }
+ b2i.Indent(4);
+ foreach (Variable! v in f.InParams) { b2i.Write(v.TypedIdent.Type); }
+ assert (f.OutParams.Length == 1);
+ b2i.Write(((Variable!) f.OutParams[0]).TypedIdent.Type);
+ b2i.Unindent();
+ b2i.Indent(2);
+ b2i.Write(f.Attributes, BoogieExprTranslator);
+ b2i.Close();
+ }
+
+ public override void AddAxiom(Axiom! a, string atts)
+ {
+ B2I! b2i = new B2I(this);
+ b2i.Write(B2I.Kind.Axiom, B2I.CountOf(a.Attributes).ToString());
+ b2i.Indent(4);
+ b2i.Write(BoogieExprTranslator.Translate(a.Expr));
+ b2i.Unindent();
+ b2i.Indent(2);
+ b2i.Write(a.Attributes, BoogieExprTranslator);
+ b2i.Close();
+ }
+
+ public override void AddAxiom(VCExpr! e)
+ {
+ B2I! b2i = new B2I(this);
+ b2i.Write(B2I.Kind.Axiom, "0");
+ b2i.Indent(4);
+ b2i.Write(e);
+ b2i.Close();
+ }
+
+ public override void DeclareGlobalVariable(GlobalVariable! v, string atts)
+ {
+ B2I! b2i = new B2I(this);
+ b2i.Write(B2I.Kind.VarDecl, v.Name + " " + B2I.CountOf(v.Attributes));
+ b2i.Indent(4);
+ b2i.Write(v.TypedIdent.Type);
+ b2i.Unindent();
+ b2i.Indent(2);
+ b2i.Write(v.Attributes, BoogieExprTranslator);
+ b2i.Close();
+ }
+
+ public void AddVC(string! name, VCExpr! vc,
+ ProverInterface.ErrorHandler! h)
+ {
+ B2I! b2i = new B2I(this);
+ b2i.Write(B2I.Kind.VC, name);
+ b2i.Indent(4);
+ b2i.Write(vc, h);
+ b2i.Close();
+ }
+ }
+
+
+ class B2I
+ {
+ private TextWriter! w;
+ private VCExprWriter! exprWriter = new VCExprWriter();
+ private VCExprOpWriter! exprOpWriter = new VCExprOpWriter();
+ private ProverInterface.ErrorHandler eh = null;
+ public ProverInterface.ErrorHandler LabelRenamer { get { return eh; } }
+ public readonly IsabelleContext! Context;
+ private Stack<int>! indents;
+ private static int[] default_indent = new int[] { 0 };
+
+ public B2I(IsabelleContext! ctxt)
+ {
+ Context = ctxt;
+ w = new StreamWriter(ctxt.OutputFilename, true);
+ indents = new Stack<int>(default_indent);
+ }
+ public void Close() { w.Close(); }
+
+ public void Indent(int indent) { indents.Push(indent + indents.Peek()); }
+ public void Unindent() { indents.Pop(); }
+
+ private void DoWrite(Kind k, string! s)
+ {
+ w.WriteLine(new String(' ', indents.Peek()) + StringOfKind(k) + s);
+ }
+ public void Write(Kind k) { DoWrite(k, ""); }
+ public void Write(Kind k, string! s) { DoWrite(k, " " + s); }
+
+ public void Write(Type! ty)
+ {
+ if (ty.IsInt) { Write(B2I.Kind.Int); }
+ else if (ty.IsBool) { Write(B2I.Kind.Bool); }
+ else if (ty.IsBv) { Write(B2I.Kind.BvType, ty.BvBits.ToString()); }
+ else if (ty.IsVariable) { Write(B2I.Kind.TypeVar, ty.AsVariable.Name); }
+ else if (ty.IsCtor)
+ {
+ CtorType! t = ty.AsCtor;
+ Write(B2I.Kind.TypeCon, t.Decl.Name + " " + t.Arguments.Length);
+ Indent(2);
+ foreach (Type! a in t.Arguments) { Write(a); }
+ Unindent();
+ }
+ else if (ty.IsMap)
+ {
+ MapType! t = ty.AsMap;
+ if (Context.AllTypes)
+ {
+ Write(B2I.Kind.Array, t.TypeParameters.Length + " " +
+ (t.Arguments.Length + 1));
+ Indent(2);
+ foreach (TypeVariable! v in t.TypeParameters) { Write(v); }
+ Unindent();
+ }
+ else { Write(B2I.Kind.Array, (t.Arguments.Length + 1).ToString()); }
+ Indent(2);
+ foreach (Type! a in t.Arguments) { Write(a); }
+ Write(t.Result);
+ Unindent();
+ }
+ }
+
+ public void Write(VCExpr! e)
+ {
+ e.Accept<bool,B2I!>(exprWriter, this);
+ }
+ public void Write(VCExpr! e, ProverInterface.ErrorHandler! h)
+ {
+ eh = h; e.Accept<bool,B2I!>(exprWriter, this); eh = null;
+ }
+ public void Write(VCExprNAry! e)
+ {
+ e.Accept<bool,B2I!>(exprOpWriter, this);
+ }
+
+ public B2I! Write(QKeyValue atts, Boogie2VCExprTranslator! tr)
+ {
+ for (QKeyValue a = atts; a != null; a = a.Next)
+ {
+ Write(B2I.Kind.Attribute, a.Key + " " + a.Params.Count);
+ Indent(2);
+ foreach (object! v in a.Params)
+ {
+ if (v is string)
+ {
+ string! s = ((string!) v).Replace("\n", " ").Replace("\r", " ")
+ .Replace("\t", "\\w");
+ Write(B2I.Kind.AttributeString, s);
+ }
+ else
+ {
+ Write(B2I.Kind.AttributeExpr);
+ Indent(2);
+ Write(tr.Translate((Expr!) v));
+ Unindent();
+ }
+ }
+ Unindent();
+ }
+ return this;
+ }
+
+ public enum Kind {
+ TypeDecl, FunDecl, VarDecl, Axiom, VC,
+ Attribute, AttributeString, AttributeExpr,
+ Type, Int, Bool, BvType, TypeVar, TypeCon, Array,
+ True, False, Not, And, Or, Implies, Distinct, Eq,
+ IntNumber, Le, Lt, Ge, Gt, Add, Sub, Mul, Div, Mod,
+ BvNumber, BvExtract, BvConcat,
+ Variable, Pat, NoPat, Forall, Exists,
+ Select, Store, HeapSucc, Subtype, Subtype3, Function, Label };
+
+ private string! StringOfKind(Kind k)
+ {
+ switch (k)
+ {
+ case Kind.TypeDecl: return "type-decl";
+ case Kind.FunDecl: return "fun-decl";
+ case Kind.VarDecl: return "var-decl";
+ case Kind.Axiom: return "axiom";
+ case Kind.VC: return "vc";
+
+ case Kind.Attribute: return "attribute";
+ case Kind.AttributeString: return "string-attr";
+ case Kind.AttributeExpr: return "expr-attr";
+
+ case Kind.Type: return "type";
+ case Kind.Int: return "int";
+ case Kind.Bool: return "bool";
+ case Kind.BvType: return "bv";
+ case Kind.TypeVar: return "type-var";
+ case Kind.TypeCon: return "type-con";
+ case Kind.Array: return "array";
+
+ case Kind.True: return "true";
+ case Kind.False: return "false";
+ case Kind.IntNumber: return "int-num";
+ case Kind.BvNumber: return "bv-num";
+ case Kind.Variable: return "var";
+
+ case Kind.Not: return "not";
+ case Kind.And: return "and";
+ case Kind.Or: return "or";
+ case Kind.Implies: return "implies";
+ case Kind.Distinct: return "distinct";
+ case Kind.Eq: return "=";
+ case Kind.Le: return "<=";
+ case Kind.Lt: return "<";
+ case Kind.Ge: return ">=";
+ case Kind.Gt: return ">";
+ case Kind.Add: return "+";
+ case Kind.Sub: return "-";
+ case Kind.Mul: return "*";
+ case Kind.Div: return "/";
+ case Kind.Mod: return "%";
+ case Kind.Select: return "select";
+ case Kind.Store: return "store";
+ case Kind.BvExtract: return "bv-extract";
+ case Kind.BvConcat: return "bv-concat";
+ case Kind.HeapSucc: return "heap-succ";
+ case Kind.Subtype: return "subtype";
+ case Kind.Subtype3: return "subtype3";
+
+ case Kind.Function: return "fun";
+
+ case Kind.Label: return "label";
+
+ case Kind.Pat: return "pat";
+ case Kind.NoPat: return "nopat";
+ case Kind.Forall: return "forall";
+ case Kind.Exists: return "exists";
+ }
+ assert false;
+ }
+
+ public static int CountOf(QKeyValue atts)
+ {
+ int i = 0;
+ for (QKeyValue a = atts; a != null; a = a.Next) { i++; }
+ return i;
+ }
+
+ public static QKeyValue! Add(string! key, string value, QKeyValue kv)
+ {
+ List<object!>! list = new List<object!>();
+ if (value != null) { list.Add(value); }
+ return new QKeyValue(Token.NoToken, key, list, kv);
+ }
+ }
+
+ class VCExprWriter : IVCExprVisitor<bool, B2I!>
+ {
+ public bool Visit(VCExprLiteral! node, B2I! b2i)
+ {
+ if (node == VCExpressionGenerator.True) { b2i.Write(B2I.Kind.True); }
+ else if (node == VCExpressionGenerator.False)
+ {
+ b2i.Write(B2I.Kind.False);
+ }
+ else if (node is VCExprIntLit)
+ {
+ b2i.Write(B2I.Kind.IntNumber, ((VCExprIntLit) node).Val.ToString());
+ }
+ else assert false;
+ return true;
+ }
+
+ public bool Visit(VCExprNAry! node, B2I! b2i)
+ {
+ b2i.Write(node);
+ return true;
+ }
+
+ public bool Visit(VCExprVar! node, B2I! b2i)
+ {
+ if (b2i.Context.IsFunctionDeclared(node.Name))
+ {
+ b2i.Write(B2I.Kind.Function, node.Name + " 0");
+ if (b2i.Context.AllTypes)
+ {
+ b2i.Indent(2);
+ b2i.Write(node.Type);
+ b2i.Unindent();
+ }
+ }
+ else
+ {
+ b2i.Write(B2I.Kind.Variable, node.Name);
+ b2i.Indent(2);
+ b2i.Write(node.Type);
+ b2i.Unindent();
+ }
+ return true;
+ }
+
+ public bool Visit(VCExprQuantifier! node, B2I! b2i)
+ {
+ QKeyValue attribs =
+ B2I.Add("qid", node.Infos.qid,
+ B2I.Add("uniqueId", node.Infos.uniqueId.ToString(),
+ B2I.Add("bvZ3Native", node.Infos.bvZ3Native.ToString(),
+ node.Infos.attributes)));
+
+ B2I.Kind all = B2I.Kind.Forall; B2I.Kind ex = B2I.Kind.Exists;
+ if (b2i.Context.AllTypes)
+ {
+ b2i.Write((node.Quan == Quantifier.ALL) ? all : ex,
+ node.TypeParameters.Count + " " + node.BoundVars.Count + " " +
+ node.Triggers.Count + " " + B2I.CountOf(attribs));
+ b2i.Indent(2);
+ foreach (TypeVariable! v in node.TypeParameters) { b2i.Write(v); }
+ b2i.Unindent();
+ }
+ else
+ {
+ b2i.Write((node.Quan == Quantifier.ALL) ? all : ex,
+ node.BoundVars.Count + " " + node.Triggers.Count + " " +
+ B2I.CountOf(attribs));
+ }
+ b2i.Indent(2);
+ foreach (VCExprVar! v in node.BoundVars)
+ {
+ b2i.Write(B2I.Kind.Variable, v.Name);
+ b2i.Indent(2);
+ b2i.Write(v.Type);
+ b2i.Unindent();
+ }
+ foreach (VCTrigger! t in node.Triggers)
+ {
+ B2I.Kind k = (t.Pos) ? B2I.Kind.Pat : B2I.Kind.NoPat;
+ b2i.Write(k, t.Exprs.Count.ToString());
+ b2i.Indent(2);
+ foreach (VCExpr! e in t.Exprs) { b2i.Write(e); }
+ b2i.Unindent();
+ }
+ b2i.Write(attribs, b2i.Context.BoogieExprTranslator);
+ b2i.Unindent();
+ b2i.Write(node.Body);
+ return true;
+ }
+
+ public bool Visit(VCExprLet! node, B2I! b2i)
+ {
+ // we do not support "let"
+ assert false;
+ return true;
+ }
+ }
+
+
+ class VCExprOpWriter : IVCExprOpVisitor<bool, B2I!>
+ {
+ private void WriteArguments(B2I! b2i, VCExprNAry! node)
+ {
+ foreach (VCExpr! e in node) { b2i.Write(e); }
+ }
+ private bool Write(B2I! b2i, B2I.Kind k, VCExprNAry! node)
+ {
+ b2i.Write(k);
+ WriteArguments(b2i, node);
+ return true;
+ }
+
+ public bool VisitNotOp(VCExprNAry! node, B2I! b2i)
+ {
+ return Write(b2i, B2I.Kind.Not, node);
+ }
+ public bool VisitEqOp(VCExprNAry! node, B2I! b2i)
+ {
+ b2i.Write(B2I.Kind.Eq);
+ if (b2i.Context.AllTypes)
+ {
+ b2i.Indent(2);
+ b2i.Write(node[0].Type);
+ b2i.Unindent();
+ }
+ WriteArguments(b2i, node);
+ return true;
+ }
+ public bool VisitNeqOp(VCExprNAry! node, B2I! b2i)
+ {
+ b2i.Write(B2I.Kind.Not);
+ b2i.Write(B2I.Kind.Eq);
+ if (b2i.Context.AllTypes)
+ {
+ b2i.Indent(2);
+ b2i.Write(node[0].Type);
+ b2i.Unindent();
+ }
+ WriteArguments(b2i, node);
+ return true;
+ }
+ private bool Unroll(B2I.Kind kind, VCExprNAry! node, B2I! b2i)
+ {
+ List<VCExpr!>! unroll = new List<VCExpr!>();
+ foreach (VCExpr! e in node) { unroll.Insert(0, e); }
+
+ List<VCExpr!>! flat = new List<VCExpr!>();
+
+ while (unroll.Count > 0)
+ {
+ VCExpr! hd = unroll[0];
+ unroll.RemoveAt(0);
+ if (hd is VCExprNAry && ((VCExprNAry) hd).Op.Equals(node.Op))
+ {
+ VCExprNAry! n = (VCExprNAry) hd;
+ foreach (VCExpr! e in n) { unroll.Insert(0, e); }
+ }
+ else { flat.Insert(0, hd); }
+ }
+
+ b2i.Write(kind, flat.Count.ToString());
+ foreach (VCExpr! e in flat) { b2i.Write(e); }
+ return true;
+ }
+ public bool VisitAndOp(VCExprNAry! node, B2I! b2i)
+ {
+ return Unroll(B2I.Kind.And, node, b2i);
+ }
+ public bool VisitOrOp(VCExprNAry! node, B2I! b2i)
+ {
+ return Unroll(B2I.Kind.Or, node, b2i);
+ }
+ public bool VisitImpliesOp(VCExprNAry! node, B2I! b2i)
+ {
+ return Write(b2i, B2I.Kind.Implies, node);
+ }
+ public bool VisitDistinctOp(VCExprNAry! node, B2I! b2i)
+ {
+ b2i.Write(B2I.Kind.Distinct, node.Length.ToString());
+ if (b2i.Context.AllTypes)
+ {
+ b2i.Indent(2);
+ b2i.Write(node[0].Type);
+ b2i.Unindent();
+ }
+ WriteArguments(b2i, node);
+ return true;
+ }
+
+ public bool VisitLabelOp(VCExprNAry! node, B2I! b2i)
+ {
+ VCExprLabelOp! op = (VCExprLabelOp!) node.Op;
+ string! label = op.label.Substring(1);
+ int ln = 0;
+ int col = 0;
+ if (b2i.LabelRenamer != null)
+ {
+ Absy! absy = b2i.LabelRenamer.Label2Absy(label);
+ if (absy.Line > 0 && absy.Col > 0) { ln = absy.Line; col = absy.Col; }
+ }
+ string! k = ((op.pos) ? "pos" : "neg");
+ b2i.Write(B2I.Kind.Label, k + " " + ln + " " + col);
+ WriteArguments(b2i, node);
+ return true;
+ }
+
+ public bool VisitSelectOp(VCExprNAry! node, B2I! b2i)
+ {
+ b2i.Write(B2I.Kind.Select, node.Length.ToString());
+ if (b2i.Context.AllTypes)
+ {
+ b2i.Indent(2);
+ foreach (VCExpr! e in node) { b2i.Write(e.Type); }
+ b2i.Unindent();
+ }
+ assert (node.Type.Equals(node[0].Type.AsMap.Result));
+ WriteArguments(b2i, node);
+ return true;
+ }
+ public bool VisitStoreOp(VCExprNAry! node, B2I! b2i)
+ {
+ b2i.Write(B2I.Kind.Store, node.Length.ToString());
+ if (b2i.Context.AllTypes)
+ {
+ b2i.Indent(2);
+ foreach (VCExpr! e in node) { b2i.Write(e.Type); }
+ b2i.Unindent();
+ }
+ assert (node.Type.Equals(node[0].Type));
+ WriteArguments(b2i, node);
+ return true;
+ }
+
+ public bool VisitBvOp(VCExprNAry! node, B2I! b2i)
+ {
+ VCExprIntLit num = node[0] as VCExprIntLit;
+ if (num == null) { assert false; }
+ b2i.Write(B2I.Kind.BvNumber, node.Type.BvBits + " " + num.Val);
+ return true;
+ }
+ public bool VisitBvExtractOp(VCExprNAry! node, B2I! b2i)
+ {
+ VCExprBvExtractOp! op = (VCExprBvExtractOp) node.Op;
+ VCExpr! child = node[0];
+ b2i.Write(B2I.Kind.BvExtract, op.End + " " + op.Start);
+ if (b2i.Context.AllTypes)
+ {
+ b2i.Indent(2);
+ b2i.Write(child.Type);
+ b2i.Write(node.Type);
+ b2i.Unindent();
+ }
+ b2i.Write(child);
+ return true;
+ }
+ public bool VisitBvConcatOp(VCExprNAry! node, B2I! b2i)
+ {
+ VCExpr! child1 = node[0];
+ VCExpr! child2 = node[1];
+ b2i.Write(B2I.Kind.BvConcat);
+ if (b2i.Context.AllTypes)
+ {
+ b2i.Indent(2);
+ b2i.Write(child1.Type);
+ b2i.Write(child2.Type);
+ b2i.Write(node.Type);
+ b2i.Unindent();
+ }
+ b2i.Write(child1);
+ b2i.Write(child2);
+ return true;
+ }
+
+ public bool VisitHeapSuccessionOp(VCExprNAry! node, B2I! b2i)
+ {
+ return Write(b2i, B2I.Kind.HeapSucc, node);
+ }
+
+ public bool VisitAddOp(VCExprNAry! node, B2I! b2i)
+ {
+ return Write(b2i, B2I.Kind.Add, node);
+ }
+ public bool VisitSubOp(VCExprNAry! node, B2I! b2i)
+ {
+ return Write(b2i, B2I.Kind.Sub, node);
+ }
+ public bool VisitMulOp(VCExprNAry! node, B2I! b2i)
+ {
+ return Write(b2i, B2I.Kind.Mul, node);
+ }
+ public bool VisitDivOp(VCExprNAry! node, B2I! b2i)
+ {
+ return Write(b2i, B2I.Kind.Div, node);
+ }
+ public bool VisitModOp(VCExprNAry! node, B2I! b2i)
+ {
+ return Write(b2i, B2I.Kind.Mod, node);
+ }
+ public bool VisitLtOp(VCExprNAry! node, B2I! b2i)
+ {
+ return Write(b2i, B2I.Kind.Lt, node);
+ }
+ public bool VisitLeOp(VCExprNAry! node, B2I! b2i)
+ {
+ return Write(b2i, B2I.Kind.Le, node);
+ }
+ public bool VisitGtOp(VCExprNAry! node, B2I! b2i)
+ {
+ return Write(b2i, B2I.Kind.Gt, node);
+ }
+ public bool VisitGeOp(VCExprNAry! node, B2I! b2i)
+ {
+ return Write(b2i, B2I.Kind.Ge, node);
+ }
+
+ public bool VisitSubtypeOp(VCExprNAry! node, B2I! b2i)
+ {
+ return Write(b2i, B2I.Kind.Subtype, node);
+ }
+ public bool VisitSubtype3Op(VCExprNAry! node, B2I! b2i)
+ {
+ return Write(b2i, B2I.Kind.Subtype3, node);
+ }
+
+ public bool VisitBoogieFunctionOp(VCExprNAry! node, B2I! b2i)
+ {
+ Function! f = ((VCExprBoogieFunctionOp!) node.Op).Func;
+ assert (f.InParams.Length == node.Length);
+ b2i.Write(B2I.Kind.Function, f.Name + " " + node.Length);
+ if (b2i.Context.AllTypes)
+ {
+ b2i.Indent(2);
+ foreach (Variable! v in f.InParams) { b2i.Write(v.TypedIdent.Type); }
+ b2i.Unindent();
+ }
+ assert (f.OutParams.Length == 1);
+ assert (f.OutParams[0] != null);
+ if (b2i.Context.AllTypes)
+ {
+ b2i.Indent(2);
+ b2i.Write(((Variable!) f.OutParams[0]).TypedIdent.Type);
+ b2i.Unindent();
+ }
+ WriteArguments(b2i, node);
+ return true;
+ }
+ }
+}
+
|