further updates to bit vector analysis

3 files changed, 150 insertions, 67 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 3981536f..8262f749 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -155,6 +155,13 @@ namespace Microsoft.Boogie {
           return;

         //BoogiePL.Errors.count = 0;

 

+        // Do bitvector analysis

+        if (CommandLineOptions.Clo.DoBitVectorAnalysis) {

+          Microsoft.Boogie.BitVectorAnalysis.DoBitVectorAnalysis(program);

+          PrintBplFile(CommandLineOptions.Clo.BitVectorAnalysisOutputBplFile, program, false);

+          return;

+        }

+

         oc = EliminateDeadVariablesAndInline(program);

         //BoogiePL.Errors.count = 0;

 

@@ -360,11 +367,6 @@ namespace Microsoft.Boogie {
       // Eliminate dead variables

       Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);

 

-      // Do bitvector analysis

-      if (CommandLineOptions.Clo.DoBitVectorAnalysis) {

-        Microsoft.Boogie.BitVectorAnalysis.DoBitVectorAnalysis(program);

-      }

-

       // Collect mod sets

       if (CommandLineOptions.Clo.DoModSetAnalysis) {

         Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);

diff --git a/Source/Core/BitvectorAnalysis.cs b/Source/Core/BitvectorAnalysis.cs
index 2c7a1674..4b6a32e8 100644
--- a/Source/Core/BitvectorAnalysis.cs
+++ b/Source/Core/BitvectorAnalysis.cs
@@ -48,74 +48,127 @@ namespace Microsoft.Boogie {
     }

 

     class MapDisjointSet : DisjointSet {

-      DisjointSet[] args;

-      DisjointSet result;

-      public MapDisjointSet(int arity) 

-      : base() {

-        args = new DisjointSet[arity];

-        for (int i = 0; i < arity; i++) {

-          args[i] = null;

-        }

-        result = null;

+      private DisjointSet[] args;

+      public DisjointSet Args(int i) {

+        return args[i];

+      }

+      

+      private DisjointSet result;

+      public DisjointSet Result { get { return result; } }

+

+      public MapDisjointSet(DisjointSet[] args, DisjointSet result) {

+        this.args = args;

+        this.result = result;

       }

-      public void UnifyArgs(DisjointSet[] thatArgs) {

-        Debug.Assert(this.args.Length == thatArgs.Length);

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

+      

+      public override void Union(DisjointSet that) {

+        base.Union(that);

+        MapDisjointSet thatMap = that as MapDisjointSet;

+        Debug.Assert(thatMap != null);

+        Debug.Assert(this.args.Length == thatMap.args.Length);

+        

+        // unify args

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

           if (this.args[i] == null) {

-            this.args[i] = thatArgs[i];

+            this.args[i] = thatMap.args[i];

+          }

+          else if (thatMap.args[i] == null) {

+            thatMap.args[i] = this.args[i];

           }

           else {

-            this.args[i].Union(thatArgs[i]);

+            this.args[i].Union(thatMap.args[i]);

           }

         }

-      }

-      public void UnifyResult(DisjointSet thatResult) {

+

+        // unify result

         if (this.result == null) {

-          this.result = thatResult;

+          this.result = thatMap.Result;

+        }

+        else if (thatMap.result == null) {

+          thatMap.result = this.result;

         }

         else {

-          this.result.Union(thatResult);

+          this.result.Union(thatMap.result);

         }

       }

-      public override void Union(DisjointSet that) {

-        base.Union(that);

-        MapDisjointSet thatMap = that as MapDisjointSet;

-        Debug.Assert(thatMap != null);

-        thatMap.UnifyArgs(this.args);

-        thatMap.UnifyResult(this.result);

-      }

     }

 

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

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

-    private Expr uniqueBvExpr = new IdentifierExpr(Token.NoToken, "UniqueBvExpr");

-    public Type UpdatedType(Variable var) {

-      return null;

+    private DisjointSet uniqueBvSet = new DisjointSet();

+

+    public Type NewType(Variable var) {

+      DisjointSet disjointSet = MakeDisjointSet(var);

+      return NewType(var.TypedIdent.Type, disjointSet);

     }

 

-    private DisjointSet MakeDisjointSet(Expr expr) {

-      if (!exprToDisjointSet.ContainsKey(expr)) {

-        Debug.Assert(expr.Type != null);

-        MapType mapType = expr.Type as MapType;

-        if (mapType != null) {

-          exprToDisjointSet[expr] = new MapDisjointSet(mapType.Arguments.Length);

+    private bool Test(DisjointSet disjointSet) {

+      DisjointSet bvRoot = uniqueBvSet.Find();

+      if (disjointSet == null)

+        return true;

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

+        return false;

+      return true;

+    }

+

+    private Type NewType(Type type, DisjointSet disjointSet) {

+      MapType mapType = type as MapType;

+      if (mapType == null) {

+        if (type is BvType && Test(disjointSet)) {

+          return Type.Int;

+        }

+        else {

+          return type;

+        }

+      }

+      else {

+        MapDisjointSet mapDisjointSet = disjointSet as MapDisjointSet;

+        Debug.Assert(mapDisjointSet != null);

+        TypeSeq newArguments = new TypeSeq();

+        Type result = NewType(mapType.Result, mapDisjointSet.Result);

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

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

+          if (mapType.Arguments[i] is BvType && Test(mapDisjointSet.Args(i))) {

+            newArguments.Add(Type.Int);

+            newTypeNeeded = true;

+          }

+          else {

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

+          }

+        }

+        if (newTypeNeeded) {

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

         }

         else {

-          exprToDisjointSet[expr] = new DisjointSet();

+          return mapType;

         }

       }

+    }

+

+    private DisjointSet MakeDisjointSet(Type type) {

+      MapType mapType = type as MapType;

+      if (mapType == null) {

+        return new DisjointSet();

+      }

+      DisjointSet[] args = new DisjointSet[mapType.Arguments.Length];

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

+        args[i] = MakeDisjointSet(mapType.Arguments[i]);

+      }

+      DisjointSet result = MakeDisjointSet(mapType.Result);

+      return new MapDisjointSet(args, result);

+    }

+

+    private DisjointSet MakeDisjointSet(Expr expr) {

+      if (!exprToDisjointSet.ContainsKey(expr)) {

+        Debug.Assert(expr.Type != null);

+        exprToDisjointSet[expr] = MakeDisjointSet(expr.Type);

+      }

       return exprToDisjointSet[expr];

     }

 

     private DisjointSet MakeDisjointSet(Variable var) {

       if (!varToDisjointSet.ContainsKey(var)) {

-        MapType mapType = var.TypedIdent.Type as MapType;

-        if (mapType != null) {

-          varToDisjointSet[var] = new MapDisjointSet(mapType.Arguments.Length);

-        }

-        else {

-          varToDisjointSet[var] = new DisjointSet();

-        }

+        varToDisjointSet[var] = MakeDisjointSet(var.TypedIdent.Type);

       }

       return varToDisjointSet[var];

     }

@@ -133,6 +186,11 @@ namespace Microsoft.Boogie {
         DisjointSet b = MakeDisjointSet(node.Proc.InParams[i]);

         a.Union(b);

       }

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

+        DisjointSet a = MakeDisjointSet(node.OutParams[i]);

+        DisjointSet b = MakeDisjointSet(node.Proc.OutParams[i]);

+        a.Union(b);

+      }

       return base.VisitImplementation(node);

     }

 

@@ -166,6 +224,14 @@ namespace Microsoft.Boogie {
     }

 

     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;

@@ -176,12 +242,14 @@ namespace Microsoft.Boogie {
           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(MakeDisjointSet(uniqueBvExpr));

+            actual.Union(uniqueBvSet);

           }

         }

       }

@@ -195,8 +263,7 @@ namespace Microsoft.Boogie {
         for (; i < node.Args.Length; i++) {

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

         }

-        mapDisjointSet.UnifyArgs(args);

-        mapDisjointSet.UnifyResult(MakeDisjointSet(node));

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

       }

 

       MapStore store = node.Fun as MapStore;

@@ -208,8 +275,7 @@ namespace Microsoft.Boogie {
         for (; i < node.Args.Length - 1; i++) {

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

         }

-        mapDisjointSet.UnifyArgs(args);

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

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

         mapDisjointSet.Union(MakeDisjointSet(node));

       }

 

@@ -219,21 +285,21 @@ namespace Microsoft.Boogie {
     public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) {

       foreach (Expr e in node.Arguments) {

         DisjointSet actual = MakeDisjointSet(e);

-        actual.Union(MakeDisjointSet(uniqueBvExpr));

+        actual.Union(uniqueBvSet);

       }

       return base.VisitBvConcatExpr(node);

     }

 

     public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node) {

       DisjointSet disjointSet = MakeDisjointSet(node.Bitvector);

-      disjointSet.Union(MakeDisjointSet(uniqueBvExpr));

+      disjointSet.Union(uniqueBvSet);

       return base.VisitBvExtractExpr(node);

     }

 

     public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {

       if (node.Val is BvConst) {

         DisjointSet disjointSet = MakeDisjointSet(node);

-        disjointSet.Union(MakeDisjointSet(uniqueBvExpr));

+        disjointSet.Union(uniqueBvSet);

       }

       return base.VisitLiteralExpr(node);

     }

@@ -251,21 +317,28 @@ namespace Microsoft.Boogie {
     public BvToIntRewriter(BitVectorAnalysis bvAnalyzer) {

       this.bvAnalyzer = bvAnalyzer;

     }

+    

     public override Constant VisitConstant(Constant node) {

-      return base.VisitConstant(node);

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

+      return node;

     }

-

-    public override GlobalVariable VisitGlobalVariable(GlobalVariable node) {

-      return base.VisitGlobalVariable(node);

+    

+    public override Variable VisitVariable(Variable node) {

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

+      return node;

     }

 

-    public override Formal VisitFormal(Formal node) {

-      return base.VisitFormal(node);

+    public override Implementation VisitImplementation(Implementation node) {

+      this.VisitVariableSeq(node.LocVars);

+      this.VisitVariableSeq(node.InParams);

+      this.VisitVariableSeq(node.OutParams);

+      return node;

     }

 

-    public override LocalVariable VisitLocalVariable(LocalVariable node) {

-      return base.VisitLocalVariable(node);

+    public override Procedure VisitProcedure(Procedure node) {

+      this.VisitVariableSeq(node.InParams);

+      this.VisitVariableSeq(node.OutParams);

+      return node;

     }

-

   }

 }

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index c4c56f28..edca934c 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -251,6 +251,7 @@ namespace Microsoft.Boogie {
     public bool ExpandLambdas = true; // not useful from command line, only to be set to false programatically

     public bool DoModSetAnalysis = false;

     public bool DoBitVectorAnalysis = false;

+    public string BitVectorAnalysisOutputBplFile = null;

     public bool UseAbstractInterpretation = true;          // true iff the user want to use abstract interpretation

     public int  /*0..9*/StepsBeforeWidening = 0;           // The number of steps that must be done before applying a widen operator

 

@@ -1364,6 +1365,14 @@ namespace Microsoft.Boogie {
             }

             break;

 

+          case "-doBitVectorAnalysis":

+          case "/doBitVectorAnalysis":

+            DoBitVectorAnalysis = true;

+            if (ps.ConfirmArgumentCount(1)) {

+              BitVectorAnalysisOutputBplFile = args[ps.i];

+            }

+            break;

+

           default:

             Contract.Assume(true);

             bool option = false;

@@ -1405,8 +1414,7 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||

               ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||

               ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ||

-              ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||

-              ps.CheckBooleanFlag("doBitVectorAnalysis", ref DoBitVectorAnalysis)

+              ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis)

               ) {

               // one of the boolean flags matched

             } else if (ps.s.StartsWith("-") || ps.s.StartsWith("/")) {