Boogie: Added boolean code expressions (sans well-formedness checks on the input).

2 files changed, 31 insertions, 9 deletions

diff --git a/Source/AIFramework/Expr.ssc b/Source/AIFramework/Expr.ssc
index 42621239..1f21f84a 100644
--- a/Source/AIFramework/Expr.ssc
+++ b/Source/AIFramework/Expr.ssc
@@ -26,7 +26,7 @@ namespace Microsoft.AbstractInterpretationFramework
     ///  AST nodes as AIF expressions.

     /// 

     ///  This only serves as a place for operations on expressions.  Clients

-    ///  should implement directly either IVariable or IFunApp.

+    ///  should implement directly IVariable, IFunApp, ...

     /// </summary>

     public interface IExpr

     {

@@ -90,6 +90,14 @@ namespace Microsoft.AbstractInterpretationFramework
     }

 

     /// <summary>

+    /// An interface representing an expression that at any moment could, in principle, evaluate

+    /// to a different value.  That is, the abstract interpreter should treat these IExpr's

+    /// as unknown values.  They are used when there is no other IExpr corresponding to the

+    /// expression to be modeled.

+    /// </summary>

+    public interface IUnknown : IExpr {}

+    

+    /// <summary>

     /// An abstract class that provides an interface for expression visitors.

     /// </summary>

     public abstract class ExprVisitor

@@ -147,6 +155,10 @@ namespace Microsoft.AbstractInterpretationFramework
                 else

                     result = fun.CloneWithBody(Substitute(subst, var, fun.Body));

             }

+            else if (inexpr is IUnknown)

+            {

+                result = inexpr;

+            }

             else

             {

                 assert false;

diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.ssc b/Source/AIFramework/VariableMap/VariableMapLattice.ssc
index c0293493..ab030b59 100644
--- a/Source/AIFramework/VariableMap/VariableMapLattice.ssc
+++ b/Source/AIFramework/VariableMap/VariableMapLattice.ssc
@@ -78,7 +78,7 @@ namespace Microsoft.AbstractInterpretationFramework
 

             public bool IsBottom { 

                  get { 

-                   return this.constraints == null;
+                   return this.constraints == null;

                  } 

             }

 

@@ -89,7 +89,7 @@ namespace Microsoft.AbstractInterpretationFramework
                   requires !this.IsBottom;

                 { 

                   assume this.constraints != null;

-                  return (!) this.constraints.Keys;
+                  return (!) this.constraints.Keys;

                 } 

             }

 

@@ -117,7 +117,7 @@ namespace Microsoft.AbstractInterpretationFramework
                 requires !this.IsBottom;

                 { 

                   assume this.constraints != null;

-                  return (Element)constraints[key];
+                  return (Element)constraints[key];

                 } 

             }

 

@@ -303,7 +303,7 @@ namespace Microsoft.AbstractInterpretationFramework
             }

             Elt! join = new Elt(newMap);

         

-            // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
+            // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));

 

             return join;

         }

@@ -368,9 +368,9 @@ namespace Microsoft.AbstractInterpretationFramework
             }

             Element! widen= new Elt(newMap);

       

-            // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
+            // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));

 

-            return widen;
+            return widen;

         }

 

         internal static ISet/*<IVariable!>*/! VariablesInExpression(IExpr! e, ISet/*<IVariable!>*/! ignoreVars)

@@ -400,6 +400,10 @@ namespace Microsoft.AbstractInterpretationFramework
                 // Ignore the bound variable

                 s.AddAll(VariablesInExpression(lambda.Body, (!) Set.Union(ignoreVars, x)));

             }

+            else if (e is IUnknown)

+            {

+                // skip (actually, it would be appropriate to return the universal set of all variables)

+            }

             else

             {

                 Debug.Assert(false, "case not handled: " + e);

@@ -482,7 +486,7 @@ namespace Microsoft.AbstractInterpretationFramework
           else 

           {

             IExpr! left = (IExpr!) fun.Arguments[0];

-            IExpr! right = (IExpr!) fun.Arguments[1];
+            IExpr! right = (IExpr!) fun.Arguments[1];

 

             if(!(left is IVariable || right is IVariable))    // At least one of the two operands must be a variable

               return false;

@@ -493,7 +497,7 @@ namespace Microsoft.AbstractInterpretationFramework
                 || fun.FunctionSymbol.Equals(Int.Mul)

                 || fun.FunctionSymbol.Equals(Int.Div)

                 || fun.FunctionSymbol.Equals(Int.Mod))

-              return IsArithmeticExpr(left) && IsArithmeticExpr(right);
+              return IsArithmeticExpr(left) && IsArithmeticExpr(right);

             else 

               return false;

           } 

@@ -592,6 +596,12 @@ namespace Microsoft.AbstractInterpretationFramework
                        );

             }

 

+            // else

+            

+            if (expr is IUnknown) {

+              return expr;

+            }

+

             else

             {

                 throw