improved bitvector analysis

1 files changed, 232 insertions, 233 deletions

diff --git a/Source/Core/BitvectorAnalysis.cs b/Source/Core/BitvectorAnalysis.cs
index 8dc80345..e0a1f312 100644
--- a/Source/Core/BitvectorAnalysis.cs
+++ b/Source/Core/BitvectorAnalysis.cs
@@ -95,21 +95,12 @@ namespace Microsoft.Boogie {
 

     private Dictionary<Expr, DisjointSet> exprToDisjointSet = new Dictionary<Expr, DisjointSet>();

     private Dictionary<Variable, DisjointSet> varToDisjointSet = new Dictionary<Variable, DisjointSet>();

-    private DisjointSet uniqueBv8Set = new DisjointSet();

-    private DisjointSet uniqueBv16Set = new DisjointSet();

     private DisjointSet uniqueBv32Set = new DisjointSet();

-    private DisjointSet uniqueBv64Set = new DisjointSet();

 

     public int Bits(Expr expr) {

       DisjointSet disjointSet = MakeDisjointSet(expr);

-      if (disjointSet.Find() == uniqueBv8Set.Find())

-        return 8;

-      if (disjointSet.Find() == uniqueBv16Set.Find())

-        return 16;

       if (disjointSet.Find() == uniqueBv32Set.Find())

         return 32;

-      if (disjointSet.Find() == uniqueBv64Set.Find())

-        return 64;

       return 0;

     }

 

@@ -118,34 +109,18 @@ namespace Microsoft.Boogie {
       return NewType(var.TypedIdent.Type, disjointSet);

     }

 

-    /*

-    private bool Test(DisjointSet disjointSet) {

-      DisjointSet bvRoot = uniqueBvSet.Find();

-      if (disjointSet == null)

-        return true;

-      if (disjointSet.Find() == bvRoot)

-        return false;

-      return true;

-    }

-    */

-

-    private Type Test(Type type, DisjointSet disjointSet) {

-      if (disjointSet.Find() == uniqueBv8Set.Find())

-        return new BvType(8);

-      if (disjointSet.Find() == uniqueBv16Set.Find())

-        return new BvType(16);

-      if (disjointSet.Find() == uniqueBv32Set.Find())

-        return new BvType(32);

-      if (disjointSet.Find() == uniqueBv64Set.Find())

-        return new BvType(64);

-

-      return type;

+    public bool IsBv32(Expr expr) {

+      DisjointSet disjointSet = MakeDisjointSet(expr);

+      return (disjointSet.Find() == uniqueBv32Set.Find());

     }

 

     private Type NewType(Type type, DisjointSet disjointSet) {

       MapType mapType = type as MapType;

       if (mapType == null) {

-        return Test(type, disjointSet);

+        if (disjointSet.Find() == uniqueBv32Set.Find())

+          return new BvType(32);

+        else

+          return type;

       }

       else {

         MapDisjointSet mapDisjointSet = disjointSet as MapDisjointSet;

@@ -154,8 +129,13 @@ namespace Microsoft.Boogie {
         Type result = NewType(mapType.Result, mapDisjointSet.Result);

         bool newTypeNeeded = (result != mapType.Result);

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

-          newArguments.Add(Test(mapType.Arguments[i], mapDisjointSet.Args(i)));

-          newTypeNeeded = newTypeNeeded || (newArguments[i] != mapType.Arguments[i]);

+          if (mapDisjointSet.Args(i).Find() == uniqueBv32Set.Find()) {

+            newArguments.Add(new BvType(32));

+            newTypeNeeded = true;

+          }

+          else {

+            newArguments.Add(mapType.Arguments[i]);

+          }

         }

         if (newTypeNeeded) {

           return new MapType(mapType.tok, mapType.TypeParameters, newArguments, result);

@@ -200,16 +180,9 @@ namespace Microsoft.Boogie {
 

       BitVectorAnalysis bvAnalyzer = new BitVectorAnalysis();

       bvAnalyzer.Visit(program);

-      /*

-      BvToIntRewriter bvtoIntRewriter = new BvToIntRewriter(bvAnalyzer);

-      bvtoIntRewriter.Visit(program);

-       */

       IntToBvRewriter intToBvRewriter = new IntToBvRewriter(program, bvAnalyzer);

       intToBvRewriter.Visit(program);

-      program.TopLevelDeclarations.Add(intToBvRewriter.bv8Id);

-      program.TopLevelDeclarations.Add(intToBvRewriter.bv16Id);

       program.TopLevelDeclarations.Add(intToBvRewriter.bv32Id);

-      program.TopLevelDeclarations.Add(intToBvRewriter.bv64Id);

     }

 

     public override Implementation VisitImplementation(Implementation node) {

@@ -255,6 +228,130 @@ namespace Microsoft.Boogie {
       return base.VisitCallCmd(node);

     }

 

+    public static bool IsComparisonIntegerFunction(Function func) {

+      if (func.Name == "INT_LT")

+        return true;

+      if (func.Name == "INT_ULT")

+        return true;

+      if (func.Name == "INT_LEQ")

+        return true;

+      if (func.Name == "INT_ULEQ")

+        return true;

+      if (func.Name == "INT_GT")

+        return true;

+      if (func.Name == "INT_UGT")

+        return true;

+      if (func.Name == "INT_GEQ")

+        return true;

+      if (func.Name == "INT_UGEQ")

+        return true;

+      return false;

+    }

+

+    public static bool IsIntegerFunction(Function func) {

+      if (func.Name == "INT_EQ")

+        return true;

+      if (func.Name == "INT_NEQ")

+        return true;

+      if (func.Name == "INT_ADD")

+        return true;

+      if (func.Name == "INT_SUB")

+        return true;

+      if (func.Name == "INT_MULT")

+        return true;

+      if (func.Name == "INT_DIV")

+        return true;

+      if (func.Name == "INT_LT")

+        return true;

+      if (func.Name == "INT_ULT")

+        return true;

+      if (func.Name == "INT_LEQ")

+        return true;

+      if (func.Name == "INT_ULEQ")

+        return true;

+      if (func.Name == "INT_GT")

+        return true;

+      if (func.Name == "INT_UGT")

+        return true;

+      if (func.Name == "INT_GEQ")

+        return true;

+      if (func.Name == "INT_UGEQ")

+        return true;

+      if (func.Name == "INT_AND")

+        return true;

+      if (func.Name == "INT_OR")

+        return true;

+      if (func.Name == "INT_XOR")

+        return true;

+      if (func.Name == "INT_NOT")

+        return true;

+      if (func.Name == "MINUS_BOTH_PTR_OR_BOTH_INT")

+        return true;

+      if (func.Name == "MINUS_LEFT_PTR")

+        return true;

+      if (func.Name == "PLUS")

+        return true;

+      if (func.Name == "MULT")

+        return true;

+      if (func.Name == "DIV")

+        return true;

+      if (func.Name == "BINARY_BOTH_INT")

+        return true;

+      return false;

+    }

+

+    public static bool IsBv32Function(Function func) {

+      if (func.Name == "BV32_EQ")

+        return true;

+      if (func.Name == "BV32_NEQ")

+        return true;

+      if (func.Name == "BV32_ADD")

+        return true;

+      if (func.Name == "BV32_SUB")

+        return true;

+      if (func.Name == "BV32_MULT")

+        return true;

+      if (func.Name == "BV32_DIV")

+        return true;

+      if (func.Name == "BV32_LT")

+        return true;

+      if (func.Name == "BV32_ULT")

+        return true;

+      if (func.Name == "BV32_LEQ")

+        return true;

+      if (func.Name == "BV32_ULEQ")

+        return true;

+      if (func.Name == "BV32_GT")

+        return true;

+      if (func.Name == "BV32_UGT")

+        return true;

+      if (func.Name == "BV32_GEQ")

+        return true;

+      if (func.Name == "BV32_UGEQ")

+        return true;

+      if (func.Name == "BV32_AND")

+        return true;

+      if (func.Name == "BV32_OR")

+        return true;

+      if (func.Name == "BV32_XOR")

+        return true;

+      if (func.Name == "BV32_NOT")

+        return true;

+      if (func.Name == "BV32_MINUS_BOTH_PTR_OR_BOTH_INT")

+        return true;

+      if (func.Name == "BV32_MINUS_LEFT_PTR")

+        return true;

+      if (func.Name == "BV32_PLUS")

+        return true;

+      if (func.Name == "BV32_MULT")

+        return true;

+      if (func.Name == "BV32_DIV")

+        return true;

+      if (func.Name == "BV32_BINARY_BOTH_INT")

+        return true;

+      return false;

+    }

+    

     public override Expr VisitNAryExpr(NAryExpr node) {

       BinaryOperator op = node.Fun as BinaryOperator;

       if (op != null) {

@@ -266,28 +363,27 @@ namespace Microsoft.Boogie {
       if (fcall != null) {

         Function func = fcall.Func;

 

-        // unify each actual argument with corresponding formal argument

-        for (int i = 0; i < node.Args.Length; i++) {

-          DisjointSet actual = MakeDisjointSet(node.Args[i]);

-          DisjointSet formal = MakeDisjointSet(func.InParams[i]);

-          actual.Union(formal);

-        }

-        Debug.Assert(func.OutParams.Length == 1);

-        MakeDisjointSet(node).Union(MakeDisjointSet(func.OutParams[0]));

-

-        if (func.Name == "intToBv8") {

-          Debug.Assert(node.Args.Length == 1);

-          Expr e = node.Args[0];

-          DisjointSet actual = MakeDisjointSet(e);

-          actual.Union(uniqueBv8Set);

+        if (IsIntegerFunction(func)) {

+          DisjointSet x;

+          if (IsComparisonIntegerFunction(func))

+            x = MakeDisjointSet(node.Args[0]);

+          else

+            x = MakeDisjointSet(node);

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

+            DisjointSet actual = MakeDisjointSet(node.Args[i]);

+            actual.Union(x);

+          }

         }

 

-        if (func.Name == "intToBv16") {

-          Debug.Assert(node.Args.Length == 1);

-          Expr e = node.Args[0];

-          DisjointSet actual = MakeDisjointSet(e);

-          actual.Union(uniqueBv16Set);

-        }

+        /*

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

+            DisjointSet actual = MakeDisjointSet(node.Args[i]);

+            DisjointSet formal = MakeDisjointSet(func.InParams[i]);

+            actual.Union(formal);

+          }

+          Debug.Assert(func.OutParams.Length == 1);

+          MakeDisjointSet(node).Union(MakeDisjointSet(func.OutParams[0]));

+        */

 

         if (func.Name == "intToBv32") {

           Debug.Assert(node.Args.Length == 1);

@@ -296,36 +392,11 @@ namespace Microsoft.Boogie {
           actual.Union(uniqueBv32Set);

         }

 

-        if (func.Name == "intToBv64") {

-          Debug.Assert(node.Args.Length == 1);

-          Expr e = node.Args[0];

-          DisjointSet actual = MakeDisjointSet(e);

-          actual.Union(uniqueBv64Set);

-        }

-

-        if (func.Name == "bv8ToInt") {

-          Debug.Assert(node.Args.Length == 1);

-          DisjointSet actual = MakeDisjointSet(node);

-          actual.Union(uniqueBv8Set);

-        }

-

-        if (func.Name == "bv16ToInt") {

-          Debug.Assert(node.Args.Length == 1);

-          DisjointSet actual = MakeDisjointSet(node);

-          actual.Union(uniqueBv16Set);

-        }

-

         if (func.Name == "bv32ToInt") {

           Debug.Assert(node.Args.Length == 1);

           DisjointSet actual = MakeDisjointSet(node);

           actual.Union(uniqueBv32Set);

         }

-

-        if (func.Name == "bv64ToInt") {

-          Debug.Assert(node.Args.Length == 1);

-          DisjointSet actual = MakeDisjointSet(node);

-          actual.Union(uniqueBv64Set);

-        }

       }

 

       MapSelect select = node.Fun as MapSelect;

@@ -356,89 +427,6 @@ namespace Microsoft.Boogie {
       return base.VisitNAryExpr(node);

     }

 

-    /*

-    public override Expr VisitNAryExpr(NAryExpr node) {

-      BinaryOperator op = node.Fun as BinaryOperator;

-      if (op != null) {

-        Debug.Assert(node.Args.Length == 2);

-        if (op.Op == BinaryOperator.Opcode.Eq || op.Op == BinaryOperator.Opcode.Neq) {

-          MakeDisjointSet(node.Args[0]).Union(MakeDisjointSet(node.Args[1]));

-        }

-      }

-

-      FunctionCall fcall = node.Fun as FunctionCall;

-      if (fcall != null) {

-        Function func = fcall.Func;

-

-        // unify each actual argument with corresponding formal argument

-        for (int i = 0; i < node.Args.Length; i++) {

-          DisjointSet actual = MakeDisjointSet(node.Args[i]);

-          DisjointSet formal = MakeDisjointSet(func.InParams[i]);

-          actual.Union(formal);

-        }

-        Debug.Assert(func.OutParams.Length == 1);

-        MakeDisjointSet(node).Union(MakeDisjointSet(func.OutParams[0]));

-

-        if (func.FindStringAttribute("bvbuiltin") != null) {

-          // unify each actual argument with uniqueBvExpr

-          foreach (Expr e in node.Args) {

-            DisjointSet actual = MakeDisjointSet(e);

-            actual.Union(uniqueBvSet);

-          }

-        }

-      }

-      

-      MapSelect select = node.Fun as MapSelect;

-      if (select != null) {

-        int i = 0;

-        MapDisjointSet mapDisjointSet = (MapDisjointSet) MakeDisjointSet(node.Args[i]);

-        i++;

-        DisjointSet[] args = new DisjointSet[node.Args.Length - 1];

-        for (; i < node.Args.Length; i++) {

-          args[i - 1] = MakeDisjointSet(node.Args[i]);

-        }

-        mapDisjointSet.Union(new MapDisjointSet(args, MakeDisjointSet(node)));

-      }

-

-      MapStore store = node.Fun as MapStore;

-      if (store != null) {

-        int i = 0;

-        MapDisjointSet mapDisjointSet = (MapDisjointSet) MakeDisjointSet(node.Args[i]);

-        i++;

-        DisjointSet[] args = new DisjointSet[node.Args.Length - 2];

-        for (; i < node.Args.Length - 1; i++) {

-          args[i - 1] = MakeDisjointSet(node.Args[i]);

-        }

-        mapDisjointSet.Union(new MapDisjointSet(args, MakeDisjointSet(node.Args[i])));

-        mapDisjointSet.Union(MakeDisjointSet(node));

-      }

-

-      return base.VisitNAryExpr(node);

-    }

-    

-    public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) {

-      foreach (Expr e in node.Arguments) {

-        DisjointSet actual = MakeDisjointSet(e);

-        actual.Union(uniqueBvSet);

-      }

-      return base.VisitBvConcatExpr(node);

-    }

-

-    public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node) {

-      DisjointSet disjointSet = MakeDisjointSet(node.Bitvector);

-      disjointSet.Union(uniqueBvSet);

-      return base.VisitBvExtractExpr(node);

-    }

-

-    public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {

-      if (node.Val is BvConst) {

-        DisjointSet disjointSet = MakeDisjointSet(node);

-        disjointSet.Union(uniqueBvSet);

-      }

-      return base.VisitLiteralExpr(node);

-    }

-    */

-

     public override Expr VisitIdentifierExpr(IdentifierExpr node) {

       DisjointSet a = MakeDisjointSet(node);

       DisjointSet b = MakeDisjointSet(node.Decl);

@@ -447,38 +435,6 @@ namespace Microsoft.Boogie {
     }

   }

 

-  /*

-  class BvToIntRewriter : StandardVisitor {

-    private BitVectorAnalysis bvAnalyzer;

-    public BvToIntRewriter(BitVectorAnalysis bvAnalyzer) {

-      this.bvAnalyzer = bvAnalyzer;

-    }

-    

-    public override Constant VisitConstant(Constant node) {

-      node.TypedIdent.Type = bvAnalyzer.NewType(node);

-      return node;

-    }

-    

-    public override Variable VisitVariable(Variable node) {

-      node.TypedIdent.Type = bvAnalyzer.NewType(node);

-      return node;

-    }

-

-    public override Implementation VisitImplementation(Implementation node) {

-      this.VisitVariableSeq(node.LocVars);

-      this.VisitVariableSeq(node.InParams);

-      this.VisitVariableSeq(node.OutParams);

-      return node;

-    }

-

-    public override Procedure VisitProcedure(Procedure node) {

-      this.VisitVariableSeq(node.InParams);

-      this.VisitVariableSeq(node.OutParams);

-      return node;

-    }

-  }

-  */

-

   class MyLiteralExpr : LiteralExpr {

     public MyLiteralExpr(IToken tok, bool b) : base(tok, b) { }

     public MyLiteralExpr(IToken tok, Basetypes.BigNum v) : base(tok, v) { }

@@ -509,27 +465,83 @@ namespace Microsoft.Boogie {
 

   class IntToBvRewriter : StandardVisitor {

     private BitVectorAnalysis bvAnalyzer;

-    public Function bv8Id;

-    public Function bv16Id;

     public Function bv32Id;

-    public Function bv64Id;

+    Dictionary<string, Function> intFunctions;

+    Dictionary<string, Function> bv32Functions;

+    void DiscoverIntAndBv32Functions(Program program) {

+      intFunctions = new Dictionary<string, Function>();

+      bv32Functions = new Dictionary<string, Function>();

+      foreach (Declaration d in program.TopLevelDeclarations) {

+        Function func = d as Function;

+        if (func == null) continue;

+        if (BitVectorAnalysis.IsIntegerFunction(func)) {

+          intFunctions.Add(func.Name, func);

+        }

+        if (BitVectorAnalysis.IsBv32Function(func)) {

+          bv32Functions.Add(func.Name, func);

+        }

+      }

+    }

+    string IntToBv32(string name) {

+      if (name == "INT_EQ")

+        return "BV32_EQ";

+      if (name == "INT_NEQ")

+        return "BV32_NEQ";

+      if (name == "INT_ADD")

+        return "BV32_ADD";

+      if (name == "INT_SUB")

+        return "BV32_SUB";

+      if (name == "INT_MULT")

+        return "BV32_MULT";

+      if (name == "INT_DIV")

+        return "BV32_DIV";

+      if (name == "INT_LT")

+        return "BV32_LT";

+      if (name == "INT_ULT")

+        return "BV32_ULT";

+      if (name == "INT_LEQ")

+        return "BV32_LEQ";

+      if (name == "INT_ULEQ")

+        return "BV32_ULEQ";

+      if (name == "INT_GT")

+        return "BV32_GT";

+      if (name == "INT_UGT")

+        return "BV32_UGT";

+      if (name == "INT_GEQ")

+        return "BV32_GEQ";

+      if (name == "INT_UGEQ")

+        return "BV32_UGEQ";

+      if (name == "INT_AND")

+        return "BV32_AND";

+      if (name == "INT_OR")

+        return "BV32_OR";

+      if (name == "INT_XOR")

+        return "BV32_XOR";

+      if (name == "INT_NOT")

+        return "BV32_NOT";

+      if (name == "MINUS_BOTH_PTR_OR_BOTH_INT")

+        return "BV32_MINUS_BOTH_PTR_OR_BOTH_INT";

+      if (name == "MINUS_LEFT_PTR")

+        return "BV32_MINUS_LEFT_PTR";

+      if (name == "PLUS")

+        return "BV32_PLUS";

+      if (name == "MULT")

+        return "BV32_MULT";

+      if (name == "DIV")

+        return "BV32_DIV";

+      if (name == "BINARY_BOTH_INT")

+        return "BV32_BINARY_BOTH_INT";

+      System.Diagnostics.Debug.Assert(false);

+      return "";

+    }

+  

+    Function IntToBv32(Function func) {

+      return bv32Functions[IntToBv32(func.Name)];

+    }

 

     public IntToBvRewriter(Program program, BitVectorAnalysis bvAnalyzer) {

       this.bvAnalyzer = bvAnalyzer;

-      

-      BvType bv8Type = new BvType(8);

-      VariableSeq bv8In = new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in", bv8Type), true));

-      Formal bv8Out = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out", bv8Type), false);

-      bv8Id = new Function(Token.NoToken, "bv8Id", bv8In, bv8Out);

-      bv8Id.Body = new IdentifierExpr(Token.NoToken, bv8In[0]);

-      bv8Id.AddAttribute("inline");

-

-      BvType bv16Type = new BvType(16);

-      VariableSeq bv16In = new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in", bv16Type), true));

-      Formal bv16Out = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out", bv16Type), false);

-      bv16Id = new Function(Token.NoToken, "bv16Id", bv16In, bv16Out);

-      bv16Id.Body = new IdentifierExpr(Token.NoToken, bv16In[0]);

-      bv16Id.AddAttribute("inline");

+      DiscoverIntAndBv32Functions(program);

 

       BvType bv32Type = new BvType(32);

       VariableSeq bv32In = new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in", bv32Type), true));

@@ -537,13 +549,6 @@ namespace Microsoft.Boogie {
       bv32Id = new Function(Token.NoToken, "bv32Id", bv32In, bv32Out);

       bv32Id.Body = new IdentifierExpr(Token.NoToken, bv32In[0]);

       bv32Id.AddAttribute("inline");

-

-      BvType bv64Type = new BvType(64);

-      VariableSeq bv64In = new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in", bv64Type), true));

-      Formal bv64Out = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out", bv64Type), false);

-      bv64Id = new Function(Token.NoToken, "bv64Id", bv64In, bv64Out);

-      bv64Id.Body = new IdentifierExpr(Token.NoToken, bv64In[0]);

-      bv64Id.AddAttribute("inline");

     }

 

     public override Constant VisitConstant(Constant node) {

@@ -573,17 +578,11 @@ namespace Microsoft.Boogie {
       FunctionCall fcall = node.Fun as FunctionCall;

       if (fcall != null) {

         Function func = fcall.Func;

-        if (func.Name == "intToBv8" || func.Name == "bv8ToInt") {

-          node.Fun = new FunctionCall(bv8Id);

-        }

-        if (func.Name == "intToBv16" || func.Name == "bv16ToInt") {

-          node.Fun = new FunctionCall(bv16Id);

-        }

         if (func.Name == "intToBv32" || func.Name == "bv32ToInt") {

           node.Fun = new FunctionCall(bv32Id);

         }

-        if (func.Name == "intToBv64" || func.Name == "bv64ToInt") {

-          node.Fun = new FunctionCall(bv64Id);

+        else if (BitVectorAnalysis.IsIntegerFunction(func) && bvAnalyzer.IsBv32(node.Args[0])) {

+          node.Fun = new FunctionCall(IntToBv32(func));

         }

       }

       return base.VisitNAryExpr(node);