Added support in the abstract interpreter for an attribute {:identity}, which says that a function is an identity function.

3 files changed, 49 insertions, 11 deletions

diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index be62eb58..c024a62a 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -857,6 +857,14 @@ namespace Microsoft.Boogie.AbstractInterpretation
             Lo = Node.Min(lo0, lo1, false);

             Hi = Node.Max(hi0, hi1, false);

           }

+        } else if (node.Fun is FunctionCall) {

+          var call = (FunctionCall)node.Fun;

+          // See if this is an identity function, which we do by checking: that the function has

+          // exactly one argument and the function has been marked by the user with the attribute {:identity}

+          bool claimsToBeIdentity = false;

+          if (call.ArgumentCount == 1 && call.Func.CheckBooleanAttribute("identity", ref claimsToBeIdentity) && claimsToBeIdentity && node.Args[0].Type.Equals(node.Type)) {

+            VisitExpr(node.Args[0]);

+          }

         }

         return node;

       }

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index c20798b2..39343e6f 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -979,21 +979,43 @@ namespace Microsoft.Boogie {
       }

     }

 

-    // Look for {:name true} or {:name false} in list of attributes. Return result in 'result'

-    // (which is not touched if there is no attribute specified).

-    //

-    // Returns false is there was an error processing the flag, true otherwise.

+    /// <summary>

+    /// If the declaration has an attribute {:name} or {:name true}, then set "result" to "true" and return "true".

+    /// If the declaration has an attribute {:name false}, then set "result" to "false" and return "true".

+    /// Otherwise, return "false" and leave "result" unchanged (which gives the caller an easy way to indicate

+    /// a default value if the attribute is not mentioned).

+    /// If there is more than one attribute called :name, then the last attribute rules.

+    /// </summary>

     public bool CheckBooleanAttribute(string name, ref bool result) {

       Contract.Requires(name != null);

-      Expr expr = FindExprAttribute(name);

-      if (expr != null) {

-        if (expr is LiteralExpr && ((LiteralExpr)expr).isBool) {

-          result = ((LiteralExpr)expr).asBool;

-        } else {

-          return false;

+      var kv = FindAttribute(name);

+      if (kv != null) {

+        if (kv.Params.Count == 0) {

+          result = true;

+          return true;

+        } else if (kv.Params.Count == 1) {

+          var lit = kv.Params[0] as LiteralExpr;

+          if (lit != null && lit.isBool) {

+            result = lit.asBool;

+            return true;

+          }

         }

       }

-      return true;

+      return false;

+    }

+

+    /// <summary>

+    /// Find and return the last occurrence of an attribute with the name "name", if any.  If none, return null.

+    /// </summary>

+    public QKeyValue FindAttribute(string name) {

+      Contract.Requires(name != null);

+      QKeyValue res = null;

+      for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {

+        if (kv.Key == name) {

+          res = kv;

+        }

+      }

+      return res;

     }

 

     // Look for {:name expr} in list of attributes.

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index fdd4d9e3..f23eaf3b 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1506,6 +1506,14 @@ namespace Microsoft.Boogie {
        trigger annotations. Internally it works by adding {:nopats ...}

        annotations to quantifiers.

 

+     {:identity}

+     {:identity true}

+       If the function has 1 argument and the use of it has type X->X for

+       some X, then the abstract interpreter will treat the function as an

+       identity function.  Note, the abstract interpreter trusts the

+       attribute--it does not try to verify that the function really is an

+       identity function.

+

   ---- On variables ----------------------------------------------------------

 

      {:existential true}