Performance improvements in BVD

3 files changed, 88 insertions, 29 deletions

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index f54ebbef..643a6b03 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -241,6 +241,31 @@ namespace Microsoft.Boogie
       /// </summary>

       public Element TryEval(params Element[] args)

       {

+        for (int i = 0; i < args.Length; ++i)

+          if(args[i]==null)

+            throw new ArgumentException();

+

+        if (apps.Count > 10) {

+          var best = apps;

+          for (int i = 0; i < args.Length; ++i)

+            if (args[i].references.Count < best.Count)

+              best = args[i].references;

+          if (best != apps) {

+            foreach (var tpl in best) {

+              bool same = true;

+              if (tpl.Func != this)

+                continue;

+              for (int i = 0; i < args.Length; ++i)

+                if (tpl.Args[i] != args[i]) {

+                  same = false;

+                  break;

+                }

+              if (same) return tpl.Result;

+            }

+            return null;

+          }

+        }

+

         foreach (var tpl in apps) {

           bool same = true;

           for (int i = 0; i < args.Length; ++i)

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index 922859f2..fce9522d 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -204,12 +204,15 @@ namespace Microsoft.Boogie.ModelViewer
 

     static ulong GetNumber(string s, int beg)

     {

-      var end = beg;

-      while (end < s.Length && char.IsDigit(s[end]))

-        end++;

-      ulong res;

-      if (!ulong.TryParse(s.Substring(beg, end - beg), out res))

-        return 0;

+      ulong res = 0;

+      while (beg < s.Length) {

+        var c = s[beg];

+        if ('0' <= c && c <= '9') {

+          res *= 10;

+          res += (uint)c - (uint)'0';

+        }

+        beg++;

+      }

       return res;

     }

 

@@ -225,11 +228,13 @@ namespace Microsoft.Boogie.ModelViewer
       var len = Math.Min(f1.Length, f2.Length);

       var numberPos = -1;

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

-        if (char.IsDigit(f1[i]) && char.IsDigit(f2[i])) {

+        var c1 = f1[i];

+        var c2 = f2[i];

+        if ('0' <= c1 && c1 <= '9' && '0' <= c2 && c2 <= '9') {
           numberPos = i;

           break;

         }

-        if (f1[i] != f2[i])

+        if (c1 != c2)

           break;

       }

 

@@ -477,6 +482,7 @@ namespace Microsoft.Boogie.ModelViewer
 

     ILanguageSpecificModel langModel;

     string format;

+    string cachedName;

     Model.Element[] args;

 

     public EdgeName(ILanguageSpecificModel n, string format, params Model.Element[] args)

@@ -493,7 +499,10 @@ namespace Microsoft.Boogie.ModelViewer
 

     public override string ToString()

     {

-      return Format();

+      if (cachedName != null)

+        return cachedName;

+      cachedName = Format();

+      return cachedName;

     }

 

     public override int GetHashCode()

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 8d2ece08..b406a824 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -44,6 +44,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     public readonly Model.Element elt_me, elt_null;

     Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();

     Dictionary<Model.Element, string> literalName = new Dictionary<Model.Element, string>();

+    Dictionary<Model.Element, Model.Element> guessedType = new Dictionary<Model.Element,Model.Element>();

     public List<StateNode> states = new List<StateNode>();

     public Dictionary<string, string> localVariableNames = new Dictionary<string, string>();

 

@@ -557,7 +558,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
             name = name.Substring(dotIdx + 1);

           }

           if (name.Contains('#')) score -= 1;

-        } else if (synthethic_fields.Contains(t.Func.Name)) {

+        } else if (t.Func.Name.StartsWith("$f_") && synthethic_fields.Contains(t.Func.Name)) {

           name = string.Format("{0}<{1}>", t.Func.Name.Substring(3).Replace("root", "alloc_root"), TypeName(t.Args[0]));

           score = 5;

         }

@@ -584,6 +585,16 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

     Model.Element GuessType(Model.Element element)

     {

+      Model.Element res;

+      if (!guessedType.TryGetValue(element, out res)) {

+        res = GuessTypeCore(element);

+        guessedType[element] = res;

+      }

+      return res;

+    }

+

+    Model.Element GuessTypeCore(Model.Element element)

+    {

       if (element is Model.Boolean)

         return tp_bool;

 

@@ -887,7 +898,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
           heap = f_heap.TryEval(heap);

         var addresses = new HashSet<Model.Element>();

 

-        if (heap != null) {

+        if (heap != null && elt != null) {

           foreach (var fld in f_select_field.AppsWithArg(0, heap)) {

             var val = f_select_value.TryEval(fld.Result, elt);

             if (val != null) {

@@ -992,12 +1003,23 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         var curState = state.State.TryGet("$s");

 

         foreach (var tupl in elt.References) {

-          if (!tupl.Args.Contains(elt)) continue; // not looking for aliases (maybe we should?)

-          if (tupl.Args.Any(IsSomeState) && !tupl.Args.Any(s => IsThisState(curState, s)))

-            continue;

+          {

+            var seenSelf = false;

+            var seenState = false;

+            var seenThisState = false;

+            var args = tupl.Args;

+            for (int i = 0; i < args.Length; ++i) {

+              if (args[i] == elt) seenSelf = true;

+              else if (IsThisState(curState, args[i])) seenThisState = true;

+              else if (IsSomeState(args[i])) seenState = true;

+            }

+            if (!seenSelf) continue; // not looking for aliases (maybe we should?)

+            if (seenState && !seenThisState) continue;

+          }

+

           var argsFmt = new StringBuilder();

           var name = tupl.Func.Name;

-          

+

           var score = FunctionScore(name);

           if (score >= viewOpts.ViewLevel)

             continue;

@@ -1030,22 +1052,25 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
             }

           }

 

-          argsFmt.Append(name).Append("(");

-          var args = new List<Model.Element>();

-          foreach (var a in tupl.Args) {

-            if (IsThisState(curState, a))

-              argsFmt.Append("\\now, ");

-            else if (a == elt)

-              argsFmt.Append(selfMarker + ", ");

-            else {

-              argsFmt.AppendFormat("%{0}, ", args.Count);

-              args.Add(a);

+          {

+            argsFmt.Append(name).Append("(");

+            var args = new List<Model.Element>();

+            foreach (var a in tupl.Args) {

+              if (IsThisState(curState, a))

+                argsFmt.Append("\\now, ");

+              else if (a == elt)

+                argsFmt.Append(selfMarker + ", ");

+              else {

+                argsFmt.AppendFormat("%{0}, ", args.Count);

+                args.Add(a);

+              }

             }

+            argsFmt.Length -= 2;

+            argsFmt.Append(")");

+            var edgeName = new EdgeName(this, argsFmt.ToString(), args.ToArray());

+            result.Add(new MapletNode(state, edgeName, retVal, retTp) { ViewLevel = score, Category = cat });

           }

-          argsFmt.Length -= 2;

-          argsFmt.Append(")");

-          var edgeName = new EdgeName(this, argsFmt.ToString(), args.ToArray());

-          result.Add(new MapletNode(state, edgeName, retVal, retTp) { ViewLevel = score, Category = cat });

+

         }

       }