Put Model.cs in separate assembly. Fix signing/versioning with it.

3 files changed, 626 insertions, 0 deletions

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
new file mode 100644
index 00000000..d7f78bfd
--- /dev/null
+++ b/Source/Model/Model.cs
@@ -0,0 +1,547 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+

+using System;

+using System.Collections.Generic;

+

+namespace Microsoft.Boogie

+{

+  public class Model

+  {

+    #region Elements and functions (inner classes)

+    public enum ElementKind

+    {

+      Integer,

+      BitVector,

+      Boolean,

+      Uninterpreted

+    }

+

+    abstract public class Element

+    {

+      public readonly Model Model;

+      internal List<FuncTuple> references = new List<FuncTuple>();

+      public readonly int Id;

+

+      public IEnumerable<FuncTuple> References { get { return references; } }

+      

+      public IEnumerable<FuncTuple> Names { 

+        get {

+          foreach (var f in references)

+            if (f.Result == this) yield return f;

+        } 

+      }

+

+      public IEnumerable<FuncTuple> ArgReferences

+      {

+        get

+        {

+          foreach (var f in references) {

+            if (f.Result != this)

+              yield return f;

+            else

+              foreach (var r in f.Args)

+                if (r == this) { yield return f; break; }

+          }

+        }

+      }

+

+      protected Element(Model p) { Model = p; }

+      public abstract ElementKind Kind { get; }

+      public virtual int AsInt() { throw new NotImplementedException(); }

+    }

+

+    public class Uninterpreted : Element

+    {

+      public override ElementKind Kind { get { return ElementKind.Uninterpreted; } }

+      public override string ToString() { return Name; }

+

+      internal Uninterpreted(Model p, string n) : base(p) { Name = n; }

+      public readonly string Name;

+    }

+

+    abstract public class Number : Element

+    {

+      protected Number(Model p, string n) : base(p) { Numeral = n; }

+      public readonly string Numeral;

+      public override int AsInt() { return int.Parse(Numeral); }

+    }

+

+    public class Integer : Number

+    {

+      internal Integer(Model p, string n) : base(p, n) { }

+      public override ElementKind Kind { get { return ElementKind.Integer; } }

+      public override string ToString() { return Numeral.ToString(); }

+    }

+

+    public class BitVector : Number

+    {

+      internal BitVector(Model p, string n, int sz) : base(p, n) { Size = sz; }

+      public readonly int Size;

+      public override ElementKind Kind { get { return ElementKind.BitVector; } }

+      public override string ToString() { return string.Format("{0}bv{1}", Numeral, Size); }

+    }

+

+    public class Boolean : Element

+    {

+      public bool Value;

+      internal Boolean(Model p, bool v) : base(p) { Value = v; }

+      public override ElementKind Kind { get { return ElementKind.Boolean; } }

+      public override string ToString() { return Value ? "true" : "false"; }      

+    }

+

+    public class Func

+    {

+      public readonly Model Model;

+      public readonly string Name;

+      public readonly int Arity;

+      internal readonly List<FuncTuple> apps = new List<FuncTuple>();

+      public IEnumerable<FuncTuple> Apps { get { return apps; } }

+      public int AppCount { get { return apps.Count; } }

+

+      internal Func(Model p, string n, int a) { Model = p;  Name = n; Arity = a; }

+

+      public void SetConstant(Element res)

+      {

+        if (Arity != 0 || apps.Count > 0)

+          throw new ArgumentException();

+        var t = new FuncTuple(this, res, null);

+        apps.Add(t);

+        res.references.Add(t);

+      }

+

+      public Element GetConstant()

+      {

+        if (Arity != 0)

+          throw new ArgumentException();

+        if (apps.Count == 0)

+          SetConstant(Model.MkElement("**" + Name));

+        return apps[0].Result;

+      }

+

+      public void AddApp(Element res, params Element[] args)

+      {        

+        if (Arity == 0)

+          SetConstant(res);

+        else {

+          if (args.Length != Arity)

+            throw new ArgumentException();

+          var t = new FuncTuple(this, res, (Element[])args.Clone());

+          apps.Add(t);

+          var u = new HashSet<Element>();

+          res.references.Add(t);

+          u.Add(res);

+          foreach (var a in args)

+            if (!u.Contains(a)) {

+              u.Add(a);

+              a.references.Add(t);

+            }

+        }

+      }

+    }

+

+    public class FuncTuple

+    {

+      static readonly Element[] EmptyArgs = new Element[0];

+

+      public readonly Func Func;

+      public readonly Element Result;

+      public readonly Element[] Args;

+

+      internal FuncTuple(Func func, Element res, Element[] args)

+      {

+        if (args == null) Args = EmptyArgs;

+        else Args = args;

+        Func = func;

+        Result = res;

+      }

+    }

+    #endregion

+

+    private List<Func> functions = new List<Func>();

+    private List<Element> elements = new List<Element>();

+    private List<CapturedState> states = new List<CapturedState>();

+    private Dictionary<string, Func> functionsByName = new Dictionary<string, Func>();

+    private Dictionary<string, Element> elementsByName = new Dictionary<string, Element>();

+

+    #region factory methods

+    Element ConstructElement(string name)

+    {

+      if (name.ToLower() == "true") return True;

+      if (name.ToLower() == "false") return False;

+

+      if (name.StartsWith("bv") && name.Length > 4 && Char.IsDigit(name[2]))

+        name = name.Substring(2);

+

+      if (Char.IsDigit(name[0]) || name[0] == '-') {

+        int col = name.IndexOf("bv");

+        int szi = -1;

+

+        if (name.EndsWith(":int"))

+          name = name.Substring(0, name.Length - 4);

+

+        if (col > 0) {          

+          if (int.TryParse(name.Substring(col + 2), out szi) && szi > 0) {

+            name = name.Substring(0, col);

+          } else {

+            return null;

+          }

+        } else if (name.EndsWith("]")) {

+          col = name.IndexOf("[");

+          if (col > 0 && int.TryParse(name.Substring(col + 1, name.Length - col - 2), out szi) && szi > 0) {

+            name = name.Substring(0, col);

+          } else {

+            return null;

+          }

+        }

+

+        for (int i = 1; i < name.Length; ++i)

+          if (!Char.IsDigit(name[i]))

+            return null;

+

+        if (szi > 0)

+          return new BitVector(this, name, szi);

+        else

+          return new Integer(this, name);

+      } else if (name[0] == '*' || name.StartsWith("val!")) {

+        return new Uninterpreted(this, name);

+      } else {

+        return null;

+      }

+    }

+

+    public Element TryMkElement(string name)

+    {

+      Element res;

+

+      if (elementsByName.TryGetValue(name, out res))

+        return res;

+

+      var tmp = ConstructElement(name);

+      if (tmp == null) return null;

+

+      name = tmp.ToString();

+      if (elementsByName.TryGetValue(name, out res))

+        return res;

+

+      elementsByName.Add(name, tmp);

+      elements.Add(tmp);

+      return tmp;

+    }

+

+    public Element MkElement(string name)

+    {

+      Element res = TryMkElement(name);

+      if (res == null)

+        throw new ArgumentException("invalid element name: '" + name + "'");

+      return res;

+    }

+

+    public Func MkFunc(string name, int arity)

+    {

+      Func res;

+      if (functionsByName.TryGetValue(name, out res)) {

+        if (res.Arity != arity)

+          throw new ArgumentException(string.Format("function '{0}' previously created with arity {1}, now trying to recreate with arity {2}", name, res.Arity, arity));

+        return res;

+      }

+      res = new Func(this, name, arity);

+      functionsByName.Add(name, res);

+      functions.Add(res);

+      return res;

+    }

+    #endregion

+

+    #region state management

+    public class CapturedState

+    {

+      List<string> vars = new List<string>();

+      Dictionary<string, Element> valuations = new Dictionary<string, Element>();

+      readonly CapturedState previous;

+      public readonly string Name;

+

+      public IEnumerable<string> Variables { get { return vars; } }

+      public int VariableCount { get { return vars.Count; } }

+      public Element TryGet(string varname)

+      {

+        CapturedState curr = this;

+        while (curr != null) {

+          Element res;

+          if (curr.valuations.TryGetValue(varname, out res))

+            return res;

+          curr = curr.previous;

+        }

+        return null;

+      }

+

+      public void AddBinding(string varname, Element value)

+      {

+        vars.Add(varname);

+        valuations.Add(varname, value);

+      }

+

+      internal CapturedState(string name, CapturedState prev)

+      {

+        Name = name;

+        previous = prev;

+      }

+    }

+

+    public CapturedState MkState(string name)

+    {

+      var last = states[states.Count - 1];

+      var s = new CapturedState(name, last);

+      states.Add(s);

+      return s;

+    }

+    #endregion

+

+    public Model()

+    {

+      InitialState = new CapturedState("<initial>", null);

+      states.Add(InitialState);

+      True = new Boolean(this, true);

+      False = new Boolean(this, false);

+      elements.Add(True);

+      elements.Add(False);

+      elementsByName.Add("true", True);

+      elementsByName.Add("false", False);

+    }

+

+    public IEnumerable<Func> Functions { get { return functions; } }

+    public IEnumerable<Element> Elements { get { return elements; } }

+    public IEnumerable<CapturedState> States { get { return states; } }

+    public readonly Element True, False;

+    public readonly CapturedState InitialState;

+

+    public bool HasFunc(string name)

+    {

+      return functionsByName.ContainsKey(name);

+    }

+

+    public Func TryGetFunc(string name)

+    {

+      Func res;

+      if (functionsByName.TryGetValue(name, out res))

+        return res;

+      else

+        return null;

+    }

+

+    public Func GetFunc(string name)

+    {

+      Func res = TryGetFunc(name);

+      if (res == null)

+        throw new KeyNotFoundException("function '" + name + "' undefined in the model");

+      return res;

+    }

+

+    public Element GetElement(string name)

+    {

+      Element res;

+      if (elementsByName.TryGetValue(name, out res))

+        return res;

+      else

+        throw new KeyNotFoundException("element '" + name + "' undefined in the model");

+    }

+

+    public void Write(System.IO.TextWriter wr)

+    {

+      wr.WriteLine("*** MODEL");

+      foreach (var f in Functions)

+        if (f.Arity == 0) {

+          wr.WriteLine("{0} -> {1}", f.Name, f.GetConstant());

+        }

+      foreach (var f in Functions)

+        if (f.Arity != 0) {

+          wr.WriteLine("{0} -> {1}", f.Name, "{");

+          foreach (var app in f.Apps) {

+            wr.Write("  ");

+            foreach (var a in app.Args)

+              wr.Write("{0} ", a);

+            wr.WriteLine("-> {0}", app.Result);

+          }

+          wr.WriteLine("}");

+        }

+      foreach (var s in States) {

+        if (s == InitialState && s.VariableCount == 0)

+          continue;

+        wr.WriteLine("*** STATE {0}", s.Name);

+        foreach (var v in s.Variables)

+          wr.WriteLine("  {0} -> {1}", v, s.TryGet(v));

+        wr.WriteLine("*** END_STATE", s.Name);

+      }

+      wr.WriteLine("*** END_MODEL");

+    }

+

+    class Parser

+    {

+      internal System.IO.TextReader rd;

+      string lastLine = "";

+      int lineNo;

+      bool v1model = false;

+      Dictionary<string, Element> partitionMapping = new Dictionary<string, Element>(); // only used when v1model is true

+      internal List<Model> resModels = new List<Model>();

+      Model currModel;

+

+      void BadModel(string msg)

+      {

+        throw new ArgumentException(string.Format("Invalid model: {0}, at line {1} ({2})", msg, lineNo, lastLine));

+      }

+

+      static char[] seps = new char[] { ' ' };

+

+      string[] GetWords(string line)

+      {

+        if (line == null)

+          return null;

+        var words = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);

+        return words;

+      }

+

+      string ReadLine()

+      {

+        var l = rd.ReadLine();

+        if (l != null) {

+          lineNo++;

+          lastLine = l;

+        }

+        return l;

+      }

+

+      Element GetElt(string name)

+      {

+        Element ret;

+

+        if (v1model) {

+          if (!partitionMapping.TryGetValue(name, out ret))

+            BadModel("undefined partition " + name);

+        } else {

+          ret = currModel.TryMkElement(name);

+          if (ret == null)

+            BadModel("invalid element name " + name);

+        }

+

+        return ret;

+      }

+

+      void NewModel()

+      {

+        v1model = false;

+        partitionMapping.Clear();

+        lastLine = "";

+        currModel = new Model();

+        resModels.Add(currModel);

+      }

+

+      internal void Run()

+      {

+        for (; ; ) {

+          var line = ReadLine();

+          if (line == null) break; // end of model, everything fine

+

+          if (line == "Counterexample:" || line == "Z3 error model: " || line == "*** MODEL") {

+            NewModel();

+            continue;

+          }

+

+          if (line.EndsWith(": Invalid.") || line.EndsWith(": Valid.")|| line.StartsWith("labels:"))

+            continue;

+          if (line == "END_OF_MODEL" || line == "." || line == "*** END_MODEL")

+            continue;

+          if (line == "partitions:" || line == "function interpretations:") {

+            v1model = true;

+            continue;

+          }

+

+          var words = GetWords(line);

+          if (words.Length == 0) continue;

+          var lastWord = words[words.Length - 1];

+

+          if (currModel == null)

+            BadModel("model begin marker not found");

+

+          if (line.StartsWith("*** STATE ")) {

+            var name = line.Substring(10);

+            CapturedState cs;

+            if (name == "<initial>")

+              cs = currModel.InitialState;

+            else

+              cs = currModel.MkState(name);

+            for (; ; ) {

+              var tmpline = ReadLine();

+              if (tmpline == "*** END_STATE") break;

+              var tuple = GetWords(tmpline);

+              if (tuple == null) BadModel("EOF in state table");

+              if (tuple.Length == 0) continue;

+              if (tuple.Length != 3 || tuple[1] != "->") BadModel("invalid state tuple definition");

+              cs.AddBinding(tuple[0], GetElt(tuple[2]));

+            }

+            continue;

+          }

+

+          if (v1model && words[0][0] == '*') {

+            var partName = words[0];

+            var len = words.Length;

+            Element elt;

+            if (len >= 3 && words[len - 2] == "->") {

+              elt = currModel.TryMkElement(lastWord);

+              if (elt == null) BadModel("bad parition value " + lastWord);

+              len -= 2;

+            } else {

+              elt = currModel.MkElement(words[0]);

+            }

+            partitionMapping.Add(partName, elt);

+            for (int i = 1; i < len; ++i) {

+              var name = words[i];

+              if (i == 1 && name[0] == '{')

+                name = name.Substring(1);

+              if (i == len - 1 && name.EndsWith("}"))

+                name = name.Substring(0, name.Length - 1);

+              var cnst = currModel.MkFunc(name, 0);

+              cnst.SetConstant(elt);

+            }

+

+          } else if (words.Length == 3 && words[1] == "->") {

+            Func fn = null;

+            var funName = words[0];

+

+            if (lastWord == "{") {

+              for (; ; ) {

+                var tuple = GetWords(ReadLine());

+                if (tuple == null) BadModel("EOF in function table");

+                if (tuple.Length == 0) continue;

+                if (tuple.Length == 1 && tuple[0] == "}") break;

+                if (tuple.Length < 3 || tuple[tuple.Length - 2] != "->") BadModel("invalid function tuple definition");

+                if (tuple[0] == "else") continue;

+                if (fn == null)

+                  fn = currModel.MkFunc(funName, tuple.Length - 2);

+                var args = new Element[fn.Arity];

+                for (int i = 0; i < fn.Arity; ++i)

+                  args[i] = GetElt(tuple[i]);

+                fn.AddApp(GetElt(tuple[tuple.Length - 1]), args);

+              }

+            } else {

+              fn = currModel.MkFunc(funName, 0);

+              fn.SetConstant(GetElt(lastWord));

+            }

+          } else {

+            BadModel("unidentified line");

+          }

+        }

+      }

+    }

+

+    public static List<Model> ParseModels(System.IO.TextReader rd)

+    {

+      var p = new Parser();

+      p.rd = rd;

+      p.Run();

+      return p.resModels;

+    }

+

+  }

+}

diff --git a/Source/Model/Model.csproj b/Source/Model/Model.csproj
new file mode 100644
index 00000000..24c1be1f
--- /dev/null
+++ b/Source/Model/Model.csproj
@@ -0,0 +1,56 @@
+<?xml version="1.0" encoding="utf-8"?>

+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

+  <PropertyGroup>

+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

+    <ProductVersion>8.0.30703</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

+    <ProjectGuid>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</ProjectGuid>

+    <OutputType>Library</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>Microsoft.Boogie</RootNamespace>

+    <AssemblyName>Model</AssemblyName>

+    <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+    <TargetFrameworkProfile />

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>bin\Debug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

+    <DebugType>pdbonly</DebugType>

+    <Optimize>true</Optimize>

+    <OutputPath>bin\Release\</OutputPath>

+    <DefineConstants>TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <PropertyGroup>

+    <SignAssembly>true</SignAssembly>

+  </PropertyGroup>

+  <PropertyGroup>

+    <AssemblyOriginatorKeyFile>../InterimKey.snk</AssemblyOriginatorKeyFile>

+  </PropertyGroup>

+  <ItemGroup>

+    <Reference Include="System" />

+  </ItemGroup>

+  <ItemGroup>

+    <Compile Include="Model.cs" />

+    <Compile Include="Properties\AssemblyInfo.cs" />

+    <Compile Include="..\version.cs" />

+  </ItemGroup>

+  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

+       Other similar extension points exist, see Microsoft.Common.targets.

+  <Target Name="BeforeBuild">

+  </Target>

+  <Target Name="AfterBuild">

+  </Target>

+  -->

+</Project>

diff --git a/Source/Model/Properties/AssemblyInfo.cs b/Source/Model/Properties/AssemblyInfo.cs
new file mode 100644
index 00000000..2efc049f
--- /dev/null
+++ b/Source/Model/Properties/AssemblyInfo.cs
@@ -0,0 +1,23 @@
+using System.Reflection;

+using System.Runtime.CompilerServices;

+using System.Runtime.InteropServices;

+

+// General Information about an assembly is controlled through the following 

+// set of attributes. Change these attribute values to modify the information

+// associated with an assembly.

+[assembly: AssemblyTitle("Model")]

+[assembly: AssemblyDescription("")]

+[assembly: AssemblyConfiguration("")]

+[assembly: AssemblyCompany("Microsoft")]

+[assembly: AssemblyProduct("Model")]

+[assembly: AssemblyCopyright("Copyright © Microsoft 2010")]

+[assembly: AssemblyTrademark("")]

+[assembly: AssemblyCulture("")]

+

+// Setting ComVisible to false makes the types in this assembly not visible 

+// to COM components.  If you need to access a type in this assembly from 

+// COM, set the ComVisible attribute to true on that type.

+[assembly: ComVisible(false)]

+

+// The following GUID is for the ID of the typelib if this project is exposed to COM

+[assembly: Guid("24299c94-99db-46c5-8671-5f91faac167e")]