Merge

9 files changed, 250 insertions, 9 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index f2f0dde5..caa2c351 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -961,8 +961,10 @@ namespace BytecodeTranslator
       Bpl.IToken cloc = creationAST.Token();

       var a = this.sink.CreateFreshLocal(creationAST.Type);

 

-      sink.AddDelegate(type.ResolvedType, methodToCall.ResolvedMethod);

-      Bpl.Constant constant = sink.FindOrCreateDelegateMethodConstant(methodToCall.ResolvedMethod);

+      ITypeDefinition unspecializedType = Microsoft.Cci.MutableContracts.ContractHelper.Unspecialized(type.ResolvedType).ResolvedType;

+      IMethodDefinition unspecializedMethod = Sink.Unspecialize(methodToCall.ResolvedMethod).ResolvedMethod;

+      sink.AddDelegate(unspecializedType, unspecializedMethod);

+      Bpl.Constant constant = sink.FindOrCreateDelegateMethodConstant(unspecializedMethod);

       Bpl.Expr methodExpr = Bpl.Expr.Ident(constant);

       Bpl.Expr instanceExpr = TranslatedExpressions.Pop();

 

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 30def4a2..73f76d52 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -83,7 +83,8 @@ namespace BytecodeTranslator {
         }

         this.sawCctor = savedSawCctor;

       } else if (typeDefinition.IsDelegate) {

-        sink.AddDelegateType(typeDefinition);

+        ITypeDefinition unspecializedType = Microsoft.Cci.MutableContracts.ContractHelper.Unspecialized(typeDefinition).ResolvedType;

+        sink.AddDelegateType(unspecializedType);

       } else if (typeDefinition.IsInterface) {

         sink.FindOrCreateType(typeDefinition);

         base.Visit(typeDefinition);

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index abb9a2c2..c138b28a 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -335,7 +335,6 @@ namespace BytecodeTranslator {
         foreach (IMethodDefinition def in PhoneNavigationCodeTraverser.NavCallers) {

           PhoneCodeHelper.addHandlerStubCaller(sink, def);

         }

-

         PhoneCodeHelper.instance().createQueriesBatchFile(sink, outputFileName);

       }

 

@@ -393,8 +392,9 @@ namespace BytecodeTranslator {
       }

 

       try {

-        IMethodDefinition unspecializedInvokeMethod = Sink.Unspecialize(invokeMethod).ResolvedMethod;

-        var decl = sink.FindOrCreateProcedure(unspecializedInvokeMethod).Decl;

+        // IMethodDefinition unspecializedInvokeMethod = Sink.Unspecialize(invokeMethod).ResolvedMethod;

+        // var decl = sink.FindOrCreateProcedure(unspecializedInvokeMethod).Decl;

+        var decl = sink.FindOrCreateProcedure(invokeMethod).Decl;

         var proc = decl as Bpl.Procedure;

         var invars = proc.InParams;

         var outvars = proc.OutParams;

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index fc98bb9f..1427b836 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -431,7 +431,7 @@ namespace BytecodeTranslator {
         string MethodName = TranslationHelper.CreateUniqueMethodName(method);

         // The method can be generic (or have a parameter whose type is a type parameter of the method's

         // containing class) and then there can be name clashes.

-        //MethodName += key.ToString();

+        MethodName += key.ToString();

 

         if (this.initiallyDeclaredProcedures.TryGetValue(MethodName, out procInfo)) return procInfo;

 

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 82c864d5..3981536f 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -360,6 +360,11 @@ 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
new file mode 100644
index 00000000..6474c8d7
--- /dev/null
+++ b/Source/Core/BitvectorAnalysis.cs
@@ -0,0 +1,224 @@
+using System;

+using System.Collections.Generic;

+using Microsoft.Boogie;

+using System.Diagnostics;

+

+namespace Microsoft.Boogie {

+  // Build an equivalence relation over the set of program expressions

+  // Assignment, equality, function calls and procedure calls are the polymorphic operations 

+  // that can be applied to both bitvectors and all other types.

+  // Otherwise all bitvector operations are separate

+  public class BitVectorAnalysis : StandardVisitor {

+    class DisjointSet {

+      DisjointSet parent;

+      int rank;

+      public DisjointSet() {

+        this.parent = this;

+        this.rank = 0;

+      }

+

+      public virtual void Union(DisjointSet that) {

+        DisjointSet xRoot = this.Find();

+        DisjointSet yRoot = that.Find();

+        if (xRoot == yRoot)

+          return;

+

+        // x and y are not already in same set. Merge them.

+        if (xRoot.rank < yRoot.rank) {

+          xRoot.parent = yRoot;

+        }

+        else if (xRoot.rank > yRoot.rank) {

+          yRoot.parent = xRoot;

+        }

+        else {

+          yRoot.parent = xRoot;

+          xRoot.rank = xRoot.rank + 1;

+        }

+      }

+

+      public DisjointSet Find() {

+        if (parent == this) {

+          return this;

+        }

+        else {

+          parent = parent.Find();

+          return parent;

+        }

+      }

+    }

+

+    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;

+      }

+      public void UnifyArgs(DisjointSet[] thatArgs) {

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

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

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

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

+          }

+          else {

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

+          }

+        }

+      }

+      public void UnifyResult(DisjointSet thatResult) {

+        if (this.result == null) {

+          this.result = thatResult;

+        }

+        else {

+          this.result.Union(thatResult);

+        }

+      }

+      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");

+

+    private DisjointSet MakeDisjointSet(Expr expr) {

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

+        if (expr.Type == null) {

+          expr.Resolve(new ResolutionContext(null));

+          expr.Typecheck(new TypecheckingContext(null));

+        }

+        MapType mapType = expr.Type as MapType;

+        if (mapType != null) {

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

+        }

+        else {

+          exprToDisjointSet[expr] = new DisjointSet();

+        }

+      }

+      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();

+        }

+      }

+      return varToDisjointSet[var];

+    }

+

+    public static void DoBitVectorAnalysis(Program program) {

+      BitVectorAnalysis bvAnalyzer = new BitVectorAnalysis();

+      bvAnalyzer.Visit(program);

+    }

+

+    public override Implementation VisitImplementation(Implementation node) {

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

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

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

+        a.Union(b);

+      }

+      return base.VisitImplementation(node);

+    }

+

+    public override Cmd VisitAssignCmd(AssignCmd node) {

+      AssignCmd simpleAssignCmd = node.AsSimpleAssignCmd;

+      List<AssignLhs> lhss = simpleAssignCmd.Lhss;

+      List<Expr> rhss = simpleAssignCmd.Rhss;

+      foreach (Expr rhs in rhss) {

+        VisitExpr(rhs);

+      }

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

+        SimpleAssignLhs lhs = (SimpleAssignLhs) lhss[i];

+        DisjointSet lhsSet = MakeDisjointSet(lhs.AsExpr);

+        lhsSet.Union(MakeDisjointSet(rhss[i]));

+      }

+      return base.VisitAssignCmd(node);

+    }

+

+    public override Cmd VisitCallCmd(CallCmd node) {

+      for (int i = 0; i < node.Ins.Count; i++) {

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

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

+        actual.Union(formal);

+      }

+      for (int i = 0; i < node.Outs.Count; i++) {

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

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

+        actual.Union(formal);

+      }

+      return base.VisitCallCmd(node);

+    }

+

+    public override Expr VisitNAryExpr(NAryExpr node) {

+      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);

+        }

+        

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

+          // unify each actual argument with uniqueBvExpr

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

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

+            actual.Union(MakeDisjointSet(uniqueBvExpr));

+          }

+        }

+      }

+      

+      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.UnifyArgs(args);

+        mapDisjointSet.UnifyResult(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.UnifyArgs(args);

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

+        mapDisjointSet.Union(MakeDisjointSet(node));

+      }

+

+      return base.VisitNAryExpr(node);

+    }

+

+    public override Expr VisitIdentifierExpr(IdentifierExpr node) {

+      DisjointSet a = MakeDisjointSet(node);

+      DisjointSet b = MakeDisjointSet(node.Decl);

+      a.Union(b);

+      return base.VisitIdentifierExpr(node);

+    }

+  }

+}

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index e1136150..c4c56f28 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -250,6 +250,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 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

 

@@ -1404,7 +1405,8 @@ 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("doModSetAnalysis", ref DoModSetAnalysis) ||

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

               ) {

               // one of the boolean flags matched

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

diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index c3ef425f..cff4f7f2 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -151,6 +151,7 @@
     <Compile Include="AbsyExpr.cs" />

     <Compile Include="AbsyQuant.cs" />

     <Compile Include="AbsyType.cs" />

+    <Compile Include="BitvectorAnalysis.cs" />

     <Compile Include="CommandLineOptions.cs" />

     <Compile Include="DeadVarElim.cs" />

     <Compile Include="Duplicator.cs" />

diff --git a/Source/ModelViewer/BCTProvider.cs b/Source/ModelViewer/BCTProvider.cs
index f7dae29e..6b48c396 100644
--- a/Source/ModelViewer/BCTProvider.cs
+++ b/Source/ModelViewer/BCTProvider.cs
@@ -32,6 +32,10 @@ namespace Microsoft.Boogie.ModelViewer.BCT {
     public BCTModel(Model m, ViewOptions opts)

       : base(m, opts) {

       f_heap_select = m.MkFunc("[3]", 3);

+

+      foreach (Model.Func fn in m.Functions) {

+

+      }

     }

 

     internal void FinishStates() {

@@ -43,7 +47,9 @@ namespace Microsoft.Boogie.ModelViewer.BCT {
     }

 

     public string GetUserVariableName(string name) {

-      if (name.StartsWith("$")) 

+      if (name == "$this")

+        return "this";

+      if (name.Contains("$")) 

         return null;

       if (name == "isControlChecked" || name == "isControlEnabled")

         return null;