AbsHoudini: Few more abstract domains

3 files changed, 284 insertions, 3 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index c7e8f0cc..77358f9b 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -882,7 +882,7 @@ namespace Microsoft.Boogie
       CommandLineOptions.Clo.ModelViewFile = "z3model";

       CommandLineOptions.Clo.UseArrayTheory = true;

       CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;

-      Houdini.AbstractDomainFactory.Initialize();

+      Houdini.AbstractDomainFactory.Initialize(program);

       var domain = Houdini.AbstractDomainFactory.GetInstance(CommandLineOptions.Clo.AbstractHoudini);

 

       // Run Abstract Houdini

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 18fe5c74..1be24e20 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -1443,6 +1443,206 @@ namespace Microsoft.Boogie.Houdini {
         }

     }

 

+    // foo(x) = x < 2^j for some j <= 16

+    public class PowDomain : IAbstractDomain

+    {

+        enum Val { FALSE, NEITHER, TRUE };

+        Val tlevel;

+        bool isBottom { get { return tlevel == Val.FALSE; } }

+        bool isTop { get { return tlevel == Val.TRUE; } }

+

+        readonly int Max = 16;

+

+        int upper; // <= Max

+

+        private PowDomain(Val tlevel) :

+            this(tlevel, 0) { }

+

+        private PowDomain(Val tlevel, int upper)

+        {

+            this.tlevel = tlevel;

+            this.upper = upper;

+        }

+

+        public static IAbstractDomain GetBottom()

+        {

+            return new PowDomain(Val.FALSE) as IAbstractDomain;

+        }

+

+        IAbstractDomain IAbstractDomain.Bottom()

+        {

+            return GetBottom();

+        }

+

+        IAbstractDomain IAbstractDomain.Join(List<Model.Element> state)

+        {

+            if (isTop) return this;

+            

+            int v = 0;

+            if (state[0] is Model.BitVector)

+                v = (state[0] as Model.BitVector).AsInt();

+            else if (state[0] is Model.Integer)

+                v = (state[0] as Model.Integer).AsInt();

+            else Debug.Assert(false);

+

+            var nupper = upper;

+            while ((1 << nupper) < v) nupper++;

+            var ntlevel = Val.NEITHER;

+            if (nupper > Max) ntlevel = Val.TRUE;

+            return new PowDomain(ntlevel, nupper);

+        }

+

+        Expr IAbstractDomain.Gamma(List<Expr> vars)

+        {

+            if (isBottom) return Expr.False;

+            if (isTop) return Expr.True;

+            var v = vars[0];

+            if (v.Type.IsBv)

+            {

+                var bits = v.Type.BvBits;

+                if (!AbstractDomainFactory.bvslt.ContainsKey(bits))

+                    throw new AbsHoudiniInternalError("No builtin function found for bv" + bits.ToString());

+                var bvslt = AbstractDomainFactory.bvslt[bits];

+                return new NAryExpr(Token.NoToken, new FunctionCall(bvslt), new ExprSeq(v,

+                    new LiteralExpr(Token.NoToken, Basetypes.BigNum.FromInt(1 << (upper+1)), 32)));

+            }

+            else

+            {

+                return Expr.Lt(v, Expr.Literal(1 << (upper+1)));

+            }

+        }

+

+        bool IAbstractDomain.TypeCheck(List<Type> argTypes, out string msg)

+        {

+            msg = "";

+            if (argTypes.Count != 1)

+            {

+                msg = "Illegal number of arguments, expecting 1";

+                return false;

+            }

+            if (argTypes.Any(tt => !tt.IsInt && !tt.IsBv))

+            {

+                msg = "Illegal type, expecting int or bv";

+                return false;

+            }

+            return true;

+        }

+    }

+

+    // foo(x_i) = all equalities that hold

+    public class EqualitiesDomain : IAbstractDomain

+    {

+        bool isBottom;

+        List<HashSet<int>> equalities;

+

+        public EqualitiesDomain(bool isBottom, List<HashSet<int>> eq)

+        {

+            this.isBottom = isBottom;

+            this.equalities = eq;

+        }

+

+        public static IAbstractDomain GetBottom()

+        {

+            return new EqualitiesDomain(true, new List<HashSet<int>>());

+        }

+

+        IAbstractDomain IAbstractDomain.Bottom()

+        {

+            return GetBottom();

+        }

+

+        IAbstractDomain IAbstractDomain.Join(List<Model.Element> state)

+        {

+            // find the guys that are equal

+            var eq = new List<HashSet<int>>();

+            for (int i = 0; i < state.Count; i++)

+            {

+                var added = false;

+                foreach (var s in eq)

+                {

+                    var sv = s.First();

+                    if (state[i].ToString() == state[sv].ToString())

+                    {

+                        s.Add(i);

+                        added = true;

+                        break;

+                    }

+                }

+                if (!added) eq.Add(new HashSet<int>(new int[] { i }));

+            }

+            

+            if (isBottom)

+            {

+                return new EqualitiesDomain(false, eq);

+            }

+

+            // intersect two partitions equalities and eq

+            var m1 = GetMap(equalities, state.Count);

+            var m2 = GetMap(eq, state.Count);

+

+            for (int i = 0; i < state.Count; i++)

+                m2[i] = new HashSet<int>(m2[i].Intersect(m1[i]));

+

+

+            // map from representative to set

+            var repToSet = new Dictionary<int, HashSet<int>>();

+

+            for (int i = 0; i < state.Count; i++)

+            {

+                var rep = m2[i].Min();

+                if (!repToSet.ContainsKey(rep))

+                    repToSet[rep] = m2[i];

+            }

+

+            var ret = new List<HashSet<int>>();

+            repToSet.Values.Iter(s => ret.Add(s));

+

+            return new EqualitiesDomain(false, ret);

+        }

+

+        Expr IAbstractDomain.Gamma(List<Expr> vars)

+        {

+            if (isBottom) return Expr.False;

+            Expr ret = Expr.True;

+            foreach (var eq in equalities.Select(hs => hs.ToList()))

+            {

+                if (eq.Count == 1) continue;

+                var prev = eq[0];

+                for (int i = 1; i < eq.Count; i++)

+                {

+                    ret = Expr.And(ret, Expr.Eq(vars[prev], vars[eq[i]]));

+                    prev = eq[i];

+                }

+            }

+            return ret;

+        }

+

+        bool IAbstractDomain.TypeCheck(List<Type> argTypes, out string msg)

+        {

+            msg = "";

+            if (argTypes.Count == 0) return true;

+            var ot = argTypes[0];

+

+            if (argTypes.Any(tt => !tt.Equals(ot)))

+            {

+                msg = string.Format("Illegal type, expecting type {0}, got {1}", ot, argTypes.First(tt => !tt.Equals(ot)));

+                return false;

+            }

+            return true;

+        }

+

+        private HashSet<int>[] GetMap(List<HashSet<int>> eq, int n)

+        {

+            var ret = new HashSet<int>[n];

+            foreach (var s in eq)

+            {

+                foreach (var i in s)

+                    ret[i] = s;

+            }

+            return ret;

+        }

+    }

+

     // foo(a,b) \in {false, \not a, a ==> b, true}

     public class ImplicationDomain : IAbstractDomain

     {

@@ -1726,6 +1926,9 @@ namespace Microsoft.Boogie.Houdini {
         // Type name -> Instance

         private static Dictionary<string, IAbstractDomain> abstractDomainInstances = new Dictionary<string, IAbstractDomain>();

         private static Dictionary<string, IAbstractDomain> abstractDomainInstancesFriendly = new Dictionary<string, IAbstractDomain>();

+        

+        // bitvector operations

+        public static Dictionary<int, Function> bvslt = new Dictionary<int, Function>();

 

         public static void Register(string friendlyName, IAbstractDomain instance)

         {

@@ -1754,7 +1957,7 @@ namespace Microsoft.Boogie.Houdini {
             return abstractDomainInstancesFriendly[friendlyName] as IAbstractDomain;

         }

 

-        public static void Initialize()

+        public static void Initialize(Program program)

         {

             // Declare abstract domains

             var domains = new List<System.Tuple<string, IAbstractDomain>>(new System.Tuple<string, IAbstractDomain>[] {

@@ -1763,14 +1966,25 @@ namespace Microsoft.Boogie.Houdini {
                   System.Tuple.Create("ConstantProp", ConstantProp.GetBottom() as IAbstractDomain),

                   System.Tuple.Create("PredicateAbs", new PredicateAbsElem() as IAbstractDomain),

                   System.Tuple.Create("ImplicationDomain", ImplicationDomain.GetBottom() as IAbstractDomain),

+                  System.Tuple.Create("PowDomain", PowDomain.GetBottom() as IAbstractDomain),

+                  System.Tuple.Create("EqualitiesDomain", EqualitiesDomain.GetBottom() as IAbstractDomain),

                   System.Tuple.Create("IA[HoudiniConst]", new IndependentAttribute<HoudiniConst>()  as IAbstractDomain),

                   System.Tuple.Create("IA[ConstantProp]", new IndependentAttribute<ConstantProp>()  as IAbstractDomain),

-                  System.Tuple.Create("IA[Intervals]", new IndependentAttribute<Intervals>()  as IAbstractDomain)

+                  System.Tuple.Create("IA[Intervals]", new IndependentAttribute<Intervals>()  as IAbstractDomain),

+                  System.Tuple.Create("IA[PowDomain]", new IndependentAttribute<PowDomain>() as IAbstractDomain),

               });

 

             domains.Iter(tup => AbstractDomainFactory.Register(tup.Item1, tup.Item2));

+            program.TopLevelDeclarations.OfType<Function>()

+                .Iter(RegisterFunction);

         }

 

+        private static void RegisterFunction(Function func)

+        {

+            var attr = QKeyValue.FindStringAttribute(func.Attributes, "builtin");

+            if (attr != null && attr == "bvslt" && func.InParams.Count == 2 && func.InParams[0].TypedIdent.Type.IsBv)

+                bvslt.Add(func.InParams[0].TypedIdent.Type.BvBits, func);

+        }

     }

 

     public interface IAbstractDomain

diff --git a/Test/AbsHoudini/multi.bpl b/Test/AbsHoudini/multi.bpl
new file mode 100644
index 00000000..a33817ac
--- /dev/null
+++ b/Test/AbsHoudini/multi.bpl
@@ -0,0 +1,67 @@
+function {:existential true} {:absdomain "ImplicationDomain"} b1(x1: bool, x2: bool) : bool;

+function {:existential true} {:absdomain "ImplicationDomain"} b2(x1: bool, x2: bool) : bool;

+function {:existential true} {:absdomain "PowDomain"} b3(x1: int) : bool;

+function {:existential true} {:absdomain "PowDomain"} b4(x1: bv32) : bool;

+function {:existential true} {:absdomain "EqualitiesDomain"} b5(x: int, y: int, z: int, w:int) : bool;

+

+function {:builtin "bvslt"} BV_SLT(x: bv32, y: bv32) : bool;

+

+var x: int;

+var flag: bool;

+

+// Test implication domain

+procedure foo ()

+  modifies x, flag;

+{

+   flag := true;

+   x := 0;

+   assert b1(flag, x == 0);

+   flag := false;

+   assert b2(flag, x == 0);

+}

+

+// Test for PowDomain(int)

+procedure bar1 ()

+  modifies x, flag;

+{

+   x := 2;

+   if(*) { x := 16; }

+   assert b3(x);

+}

+

+// Test for PowDomain(bv32)

+procedure bar2 ()

+  modifies x, flag;

+{

+  var s: bv32;

+

+  s := 2bv32;

+  if(*) { s := 16bv32; }

+  assert b4(s);

+}

+

+// Test for EqualitiesDomain

+procedure baz ()

+  modifies x, flag;

+{

+  var y: int;

+  var z: int;

+  var w: int;

+

+  assume x == y;

+  assume x == z;

+

+  if(*) {

+    x := x + 1;

+    y := y + 1;

+  } else {

+    x := x + 2;

+    y := y + 2;

+  }

+

+  assume x == w;

+

+  assert b5(x,y,z,w);

+}

+

+