Add state sequence API and creation, still untested

2 files changed, 153 insertions, 17 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index a449dc82..48b982bf 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -206,6 +206,63 @@ namespace Microsoft.Boogie {
       }

     }

 

+    public Model GetModelWithStates()

+    {

+      if (Model == null) return null;

+

+      Model m = Model.ToModel();

+

+      var mvstates = m.TryGetFunc("@MV_state");

+      if (MvInfo == null || mvstates == null)

+        return m;

+

+      Contract.Assert(mvstates.Arity == 1);

+

+      foreach (Variable v in MvInfo.AllVariables) {

+        var fn = m.TryGetFunc(v.Name);

+        if (fn != null && fn.Arity == 0) {

+          m.InitialState.AddBinding(v.Name, fn.GetConstant());

+        }

+      }

+

+      var states = new List<int>();

+      foreach (var t in mvstates.Apps)

+        states.Add(t.Args[0].AsInt());

+

+      states.Sort();

+

+      foreach (int s in states) {

+        if (0 <= s && s < MvInfo.CapturePoints.Count) {

+          VC.ModelViewInfo.Mapping map = MvInfo.CapturePoints[s];

+          var cs = m.MkState(map.Description);

+

+          foreach (Variable v in MvInfo.AllVariables) {

+            var e = (Expr)map.IncarnationMap[v];

+            if (e == null) continue;

+

+            Model.Element elt;

+

+            if (e is IdentifierExpr) {

+              IdentifierExpr ide = (IdentifierExpr)e;

+              elt = m.GetFunc(ide.Decl.Name).GetConstant();

+            } else if (e is LiteralExpr) {

+              LiteralExpr lit = (LiteralExpr)e;

+              elt = m.MkElement(lit.Val.ToString());

+            } else {

+              elt = m.MkFunc(e.ToString(), 0).GetConstant();

+            }

+

+            cs.AddBinding(v.Name, elt);

+          }

+

+        } else {

+          Contract.Assume(false);

+        }

+      }

+

+      return m;

+    }

+

     void PrintCapturedState(int indent, Hashtable/*Variable -> Expr*/ incarnations) {

       Contract.Requires(0 <= indent);

       Contract.Requires(Model != null && MvInfo != null);

diff --git a/Source/VCGeneration/Model.cs b/Source/VCGeneration/Model.cs
index 0668a9f1..43a6346c 100644
--- a/Source/VCGeneration/Model.cs
+++ b/Source/VCGeneration/Model.cs
@@ -1,4 +1,9 @@
-using System;

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

+//

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

+//

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

+using System;

 using System.Collections.Generic;

 

 namespace Microsoft.Boogie

@@ -45,6 +50,7 @@ namespace Microsoft.Boogie
 

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

       public abstract ElementKind Kind { get; }

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

     }

 

     public class Uninterpreted : Element

@@ -60,6 +66,7 @@ namespace Microsoft.Boogie
     {

       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

@@ -87,12 +94,13 @@ namespace Microsoft.Boogie
 

     public class Func

     {

+      private readonly Model Parent;

       public readonly string Name;

       public readonly int Arity;

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

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

 

-      internal Func(string n, int a) { Name = n; Arity = a; }

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

 

       public void SetConstant(Element res)

       {

@@ -103,6 +111,15 @@ namespace Microsoft.Boogie
         res.references.Add(t);

       }

 

+      public Element GetConstant()

+      {

+        if (Arity != 0)

+          throw new ArgumentException();

+        if (apps.Count == 0)

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

+        return apps[0].Result;

+      }

+

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

       {        

         if (Arity == 0)

@@ -144,6 +161,7 @@ namespace Microsoft.Boogie
 

     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>();

 

@@ -193,30 +211,31 @@ namespace Microsoft.Boogie
       }

     }

 

-    public bool TryMkElement(string name, out Element res)

+    public Element TryMkElement(string name)

     {

+      Element res;

+

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

-        return true;

+        return res;

 

       var tmp = ConstructElement(name);

-      if (tmp == null) return false;

+      if (tmp == null) return null;

 

       name = tmp.ToString();

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

-        return true;

+        return res;

 

-      res = tmp;

-      elementsByName.Add(name, res);

-      elements.Add(res);

-      return true;

+      elementsByName.Add(name, tmp);

+      elements.Add(tmp);

+      return tmp;

     }

 

     public Element MkElement(string name)

     {

-      Element res;

-      if (TryMkElement(name, out res))

-        return res;

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

+      Element res = TryMkElement(name);

+      if (res == null)

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

+      return res;

     }

 

     public Func MkFunc(string name, int arity)

@@ -227,15 +246,60 @@ namespace Microsoft.Boogie
           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(name, arity);

+      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 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);

       True = new Boolean(this, true);

       False = new Boolean(this, false);

       elements.Add(True);

@@ -246,15 +310,30 @@ namespace Microsoft.Boogie
 

     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 Func GetFunc(string name)

+    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

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

+        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)